From 7c8f264e0d799d87920d7c3aca2ba0f2d11c3dfc Mon Sep 17 00:00:00 2001
From: "Brian R. Murphy" <132495859+brmataptos@users.noreply.github.com>
Date: Tue, 24 Sep 2024 12:26:00 -0700
Subject: [PATCH 1/6] fix #14633: fix error messages for lambdas, identify
 change points for more complete lambda implementation

---
 .../src/bytecode_generator.rs                 |  28 +-
 .../src/env_pipeline/function_checker.rs      |  34 +-
 .../src/env_pipeline/lambda_lifter.rs         |   4 +-
 .../env_pipeline/recursive_struct_checker.rs  |   2 +-
 .../src/env_pipeline/unused_params_checker.rs |  10 +-
 .../move/move-compiler-v2/src/experiments.rs  |  25 +
 .../file_format_generator/module_generator.rs |  15 +-
 .../tests/bytecode-generator/assign.exp       |   2 +-
 .../borrow_deref_optimize.exp                 |   4 +-
 .../bug_14471_receiver_inference.exp          |   8 +-
 .../bytecode-generator/escape_autoref.exp     |   4 +-
 .../tests/bytecode-generator/fields.exp       |   4 +-
 .../bytecode-generator/fields_invalid.exp     |   2 +-
 .../tests/bytecode-generator/globals.exp      |   4 +-
 .../matching_ability_err.exp                  |   6 +-
 .../matching_coverage_err.exp                 |   6 +-
 .../tests/bytecode-generator/matching_ok.exp  |   8 +-
 .../mutate_immutable_cmp.exp                  |   2 +-
 .../tests/bytecode-generator/pack_unpack.exp  |   2 +-
 .../bytecode-generator/spec_construct.exp     |   2 +-
 .../use_struct_overlap_with_module.exp        |   4 +-
 .../abilities/v1/ability_constraints.exp      |   6 +-
 .../v1/phantom_param_op_abilities.exp         |  12 +-
 .../phantom_params_constraint_abilities.exp   |  24 +-
 .../v1/phantom_params_field_abilities.exp     |  16 +-
 .../checking/access_specifiers/access_ok.exp  |  18 +-
 .../acquires_list_generic.exp                 |   2 +-
 .../tests/checking/dotdot/dotdot_valid.exp    |  16 +-
 .../tests/checking/indexing/examples_book.exp |   2 +-
 .../tests/checking/inlining/lambda3.exp       |  24 +
 .../tests/checking/inlining/lambda3.move      |  99 ++++
 .../tests/checking/inlining/lambda4.exp       |  13 +
 .../tests/checking/inlining/lambda4.move      |  99 ++++
 .../tests/checking/inlining/lambda5.exp       |   7 +
 .../tests/checking/inlining/lambda5.move      |  99 ++++
 .../checking/inlining/non_lambda_arg.exp      |   4 +-
 .../checking/inlining/resources_valid.exp     |   2 +-
 .../naming/duplicate_acquires_list_item.exp   |  16 +-
 .../global_builtin_one_type_argument.exp      |   2 +-
 .../naming/unused_type_parameter_struct.exp   |   8 +-
 .../checking/naming/warning_dependency.exp    |   8 +-
 .../positional_fields/assign_field.exp        |  10 +-
 .../bind_anonymous_field.exp                  |   6 +-
 .../checking/positional_fields/decl_ok.exp    |   4 +-
 .../named_tuple_ability_decl_ok.exp           |  10 +-
 .../named_tuple_construct_ok.exp              |   4 +-
 .../variant_ability_decl_ok.exp               |   4 +-
 .../tests/checking/receiver/decl_errors.exp   |   4 +-
 .../tests/checking/receiver/generic_calls.exp |   2 +-
 .../checking/receiver/generic_calls_typed.exp |   2 +-
 .../tests/checking/specs/invariants_ok.exp    |   2 +-
 .../specs/move_function_in_spec_ok.exp        |   2 +-
 .../tests/checking/specs/schemas_ok.exp       |   2 +-
 .../tests/checking/specs/structs_ok.exp       |   4 +-
 .../checking/typing/borrow_field_chain.exp    |   4 +-
 .../typing/decl_unpack_references.exp         |   4 +-
 .../tests/checking/typing/derefrence.exp      |   2 +-
 .../tests/checking/typing/dummy_field.exp     |   4 +-
 .../tests/checking/typing/eq.exp              |   2 +-
 .../tests/checking/typing/exp_list.exp        |   2 +-
 .../tests/checking/typing/global_builtins.exp |   4 +-
 .../typing/global_builtins_inferred.exp       |   2 +-
 .../implicit_deref_borrow_field_chain.exp     |   4 +-
 .../tests/checking/typing/lambda.exp          |   8 +
 .../tests/checking/typing/lambda2.exp         |  25 +
 .../tests/checking/typing/lambda2.move        | 100 ++++
 .../tests/checking/typing/lambda_typed.exp    |   8 +
 .../typing/main_arguments_various_caes.exp    |   2 +-
 .../typing/move_from_type_argument.exp        |   2 +-
 .../checking/typing/mutable_eq_and_neq.exp    |   4 +-
 .../tests/checking/typing/neq.exp             |   2 +-
 .../checking/typing/nested_post_process.exp   |   6 +-
 .../typing/phantom_param_struct_decl.exp      |  10 +-
 .../typing/type_variable_join_single_pack.exp |   4 +-
 .../type_variable_join_single_unpack.exp      |   4 +-
 ...ype_variable_join_single_unpack_assign.exp |   4 +-
 .../type_variable_join_threaded_pack.exp      |   6 +-
 .../multi_pool_money_market_token.exp         |  40 +-
 .../v1-examples/simple_money_market_token.exp |  36 +-
 .../variants_test_no_parenthesis_ok.exp       |   2 +-
 .../checking/variants/variants_test_ok.exp    |   2 +-
 ...mutually_recursive_non_generic_type_ok.exp |   2 +-
 .../infinite_instantiations_valid.exp         |   2 +-
 .../tests/lambda-lifting/basic.exp            | 258 ++++++++++
 .../tests/lambda-lifting/modify.exp           | 457 ++++++++++++++++++
 .../tests/lambda-lifting/nested.exp           | 180 +++++++
 .../tests/lambda-lifting/pattern.exp          | 220 ++++++++-
 .../parser/spec_parsing_fun_type_fail.exp     |   2 +-
 .../tests/op-equal/valid0.exp                 |   4 +-
 .../tests/op-equal/valid1.exp                 |   4 +-
 .../assign_unpack_references.exp              |   4 +-
 .../move/move-compiler-v2/tests/testsuite.rs  |  13 +-
 .../tests/move_check/typing/lambda2.exp       |  30 ++
 .../tests/move_check/typing/lambda2.move      | 100 ++++
 .../move-model/src/builder/model_builder.rs   |   5 +-
 .../move-model/src/builder/module_builder.rs  |   3 +
 third_party/move/move-model/src/model.rs      |  20 +-
 third_party/move/move-model/src/ty.rs         |  43 +-
 98 files changed, 2101 insertions(+), 248 deletions(-)
 create mode 100644 third_party/move/move-compiler-v2/tests/checking/inlining/lambda3.exp
 create mode 100644 third_party/move/move-compiler-v2/tests/checking/inlining/lambda3.move
 create mode 100644 third_party/move/move-compiler-v2/tests/checking/inlining/lambda4.exp
 create mode 100644 third_party/move/move-compiler-v2/tests/checking/inlining/lambda4.move
 create mode 100644 third_party/move/move-compiler-v2/tests/checking/inlining/lambda5.exp
 create mode 100644 third_party/move/move-compiler-v2/tests/checking/inlining/lambda5.move
 create mode 100644 third_party/move/move-compiler-v2/tests/checking/typing/lambda2.exp
 create mode 100644 third_party/move/move-compiler-v2/tests/checking/typing/lambda2.move
 create mode 100644 third_party/move/move-compiler/tests/move_check/typing/lambda2.exp
 create mode 100644 third_party/move/move-compiler/tests/move_check/typing/lambda2.move

diff --git a/third_party/move/move-compiler-v2/src/bytecode_generator.rs b/third_party/move/move-compiler-v2/src/bytecode_generator.rs
index 16248e056d369..2b024cb47991d 100644
--- a/third_party/move/move-compiler-v2/src/bytecode_generator.rs
+++ b/third_party/move/move-compiler-v2/src/bytecode_generator.rs
@@ -406,9 +406,12 @@ impl<'env> Generator<'env> {
                         ),
                     );
                 }
-                self.emit_call(*id, targets, BytecodeOperation::WriteRef, vec![
-                    lhs_temp, rhs_temp,
-                ])
+                self.emit_call(
+                    *id,
+                    targets,
+                    BytecodeOperation::WriteRef,
+                    vec![lhs_temp, rhs_temp],
+                )
             },
             ExpData::Assign(id, lhs, rhs) => self.gen_assign(*id, lhs, rhs, None),
             ExpData::Return(id, exp) => {
@@ -479,9 +482,16 @@ impl<'env> Generator<'env> {
                     .rewrite_spec_descent(&SpecBlockTarget::Inline, spec);
                 self.emit_with(*id, |attr| Bytecode::SpecBlock(attr, spec));
             },
-            ExpData::Invoke(id, _, _) | ExpData::Lambda(id, _, _) => {
-                self.internal_error(*id, format!("not yet implemented: {:?}", exp))
-            },
+            // TODO(LAMBDA)
+            ExpData::Lambda(id, _, _) => self.error(
+                *id,
+                "Function-typed values not yet supported except as parameters to calls to inline functions",
+            ),
+            // TODO(LAMBDA)
+            ExpData::Invoke(_, exp, _) => self.error(
+                exp.as_ref().node_id(),
+                "Calls to function values other than inline function parameters not yet supported",
+            ),
             ExpData::Quant(id, _, _, _, _, _) => {
                 self.internal_error(*id, "unsupported specification construct")
             },
@@ -806,7 +816,11 @@ impl<'env> Generator<'env> {
 
             Operation::NoOp => {}, // do nothing
 
-            Operation::Closure(..) => self.internal_error(id, "closure not yet implemented"),
+            // TODO(LAMBDA)
+            Operation::Closure(..) => self.error(
+                id,
+                "Function-typed values not yet supported except as parameters to calls to inline functions",
+            ),
 
             // Non-supported specification related operations
             Operation::Exists(Some(_))
diff --git a/third_party/move/move-compiler-v2/src/env_pipeline/function_checker.rs b/third_party/move/move-compiler-v2/src/env_pipeline/function_checker.rs
index 57a9976ed3635..05e86f37e82be 100644
--- a/third_party/move/move-compiler-v2/src/env_pipeline/function_checker.rs
+++ b/third_party/move/move-compiler-v2/src/env_pipeline/function_checker.rs
@@ -3,7 +3,7 @@
 
 //! Do a few checks of functions and function calls.
 
-use crate::Options;
+use crate::{experiments::Experiment, Options};
 use codespan_reporting::diagnostic::Severity;
 use move_binary_format::file_format::Visibility;
 use move_model::{
@@ -17,17 +17,44 @@ type QualifiedFunId = QualifiedId<FunId>;
 
 /// check that non-inline function parameters do not have function type.
 pub fn check_for_function_typed_parameters(env: &mut GlobalEnv) {
+    let options = env
+        .get_extension::<Options>()
+        .expect("Options is available");
+    let lambda_params_ok = options.experiment_on(Experiment::LAMBDA_PARAMS);
+    let lambda_return_ok = options.experiment_on(Experiment::LAMBDA_RESULTS);
+    if lambda_params_ok && lambda_return_ok {
+        return;
+    }
+
     for caller_module in env.get_modules() {
         if caller_module.is_primary_target() {
             for caller_func in caller_module.get_functions() {
+                // Check that no functions have function return type
+                if !lambda_return_ok {
+                    let caller_name = caller_func.get_full_name_str();
+                    let return_type = caller_func.get_result_type();
+                    let has_function_value =
+                        return_type.clone().flatten().iter().any(Type::is_function);
+                    if has_function_value {
+                        let type_display_ctx = caller_func.get_type_display_ctx();
+                        env.diag(
+                            Severity::Error,
+                            &caller_func.get_id_loc(),
+                            &format!("Functions may not return function-typed values, but function `{}` return type is `{}`:",
+                                     caller_name,
+                                     return_type.display(&type_display_ctx)),
+                        );
+                    }
+                }
                 // Check that non-inline function parameters don't have function type
-                if !caller_func.is_inline() {
+                if !caller_func.is_inline() && !lambda_params_ok {
                     let parameters = caller_func.get_parameters();
                     let bad_params: Vec<_> = parameters
                         .iter()
                         .filter(|param| matches!(param.1, Type::Fun(_, _)))
                         .collect();
                     if !bad_params.is_empty() {
+                        let type_display_ctx = caller_func.get_type_display_ctx();
                         let caller_name = caller_func.get_full_name_str();
                         let reasons: Vec<(Loc, String)> = bad_params
                             .iter()
@@ -35,8 +62,9 @@ pub fn check_for_function_typed_parameters(env: &mut GlobalEnv) {
                                 (
                                     param.2.clone(),
                                     format!(
-                                        "Parameter `{}` has a function type.",
+                                        "Parameter `{}` has function-valued type `{}`.",
                                         param.0.display(env.symbol_pool()),
+                                        param.1.display(&type_display_ctx)
                                     ),
                                 )
                             })
diff --git a/third_party/move/move-compiler-v2/src/env_pipeline/lambda_lifter.rs b/third_party/move/move-compiler-v2/src/env_pipeline/lambda_lifter.rs
index cb11736440a66..8326c3e8af618 100644
--- a/third_party/move/move-compiler-v2/src/env_pipeline/lambda_lifter.rs
+++ b/third_party/move/move-compiler-v2/src/env_pipeline/lambda_lifter.rs
@@ -309,7 +309,7 @@ impl<'a> ExpRewriterFunctions for LambdaLifter<'a> {
                 env.error(
                     &loc,
                     &format!(
-                        "captured variable `{}` cannot be modified inside of a lambda",
+                        "captured variable `{}` cannot be modified inside of a lambda", // TODO(LAMBDA)
                         name.display(env.symbol_pool())
                     ),
                 );
@@ -327,7 +327,7 @@ impl<'a> ExpRewriterFunctions for LambdaLifter<'a> {
                 env.error(
                     &loc,
                     &format!(
-                        "captured variable `{}` cannot be modified inside of a lambda",
+                        "captured variable `{}` cannot be modified inside of a lambda", // TODO(LAMBDA)
                         name.display(env.symbol_pool())
                     ),
                 );
diff --git a/third_party/move/move-compiler-v2/src/env_pipeline/recursive_struct_checker.rs b/third_party/move/move-compiler-v2/src/env_pipeline/recursive_struct_checker.rs
index 29c5a6b299bca..1246ac0ea5ba0 100644
--- a/third_party/move/move-compiler-v2/src/env_pipeline/recursive_struct_checker.rs
+++ b/third_party/move/move-compiler-v2/src/env_pipeline/recursive_struct_checker.rs
@@ -101,7 +101,7 @@ impl<'a> RecursiveStructChecker<'a> {
                         self.report_invalid_field(&struct_env, &field_env);
                     }
                 },
-                Type::Primitive(_) | Type::TypeParameter(_) => {},
+                Type::Primitive(_) | Type::TypeParameter(_) | Type::Fun(..) => {},
                 _ => unreachable!("invalid field type"),
             }
             path.pop();
diff --git a/third_party/move/move-compiler-v2/src/env_pipeline/unused_params_checker.rs b/third_party/move/move-compiler-v2/src/env_pipeline/unused_params_checker.rs
index 276b8dc3d675c..e9da0d5cbb053 100644
--- a/third_party/move/move-compiler-v2/src/env_pipeline/unused_params_checker.rs
+++ b/third_party/move/move-compiler-v2/src/env_pipeline/unused_params_checker.rs
@@ -55,12 +55,16 @@ fn used_type_parameters_in_fields(struct_env: &StructEnv) -> BTreeSet<u16> {
 fn used_type_parameters_in_ty(ty: &Type) -> BTreeSet<u16> {
     match ty {
         Type::Primitive(_) => BTreeSet::new(),
-        Type::Struct(_, _, tys) => tys.iter().flat_map(used_type_parameters_in_ty).collect(),
+        Type::Tuple(tys) | Type::Struct(_, _, tys) => {
+            tys.iter().flat_map(used_type_parameters_in_ty).collect()
+        },
         Type::TypeParameter(i) => BTreeSet::from([*i]),
         Type::Vector(ty) => used_type_parameters_in_ty(ty),
+        Type::Fun(t1, t2) => [t1, t2]
+            .iter()
+            .flat_map(|t| used_type_parameters_in_ty(t))
+            .collect(),
         Type::Reference(..)
-        | Type::Fun(..)
-        | Type::Tuple(..)
         | Type::TypeDomain(..)
         | Type::ResourceDomain(..)
         | Type::Error
diff --git a/third_party/move/move-compiler-v2/src/experiments.rs b/third_party/move/move-compiler-v2/src/experiments.rs
index d7bdf7820c00e..c067d2f243ee1 100644
--- a/third_party/move/move-compiler-v2/src/experiments.rs
+++ b/third_party/move/move-compiler-v2/src/experiments.rs
@@ -111,11 +111,32 @@ pub static EXPERIMENTS: Lazy<BTreeMap<String, Experiment>> = Lazy::new(|| {
             description: "Turns on or off specification rewriting".to_string(),
             default: Given(false),
         },
+        Experiment {
+            name: Experiment::LAMBDA_FIELDS.to_string(),
+            description: "Turns on or off function values in struct fields".to_string(),
+            default: Given(false),
+        },
         Experiment {
             name: Experiment::LAMBDA_LIFTING.to_string(),
             description: "Turns on or off lambda lifting".to_string(),
             default: Given(false),
         },
+        Experiment {
+            name: Experiment::LAMBDA_PARAMS.to_string(),
+            description: "Turns on or off function values as parameters to non-inline functions"
+                .to_string(),
+            default: Given(false),
+        },
+        Experiment {
+            name: Experiment::LAMBDA_RESULTS.to_string(),
+            description: "Turns on or off function values in function results".to_string(),
+            default: Given(false),
+        },
+        Experiment {
+            name: Experiment::LAMBDA_VALUES.to_string(),
+            description: "Turns on or off first-class function values".to_string(),
+            default: Given(false),
+        },
         Experiment {
             name: Experiment::RECURSIVE_TYPE_CHECK.to_string(),
             description: "Turns on or off checking of recursive structs and type instantiations"
@@ -275,7 +296,11 @@ impl Experiment {
     pub const INLINING: &'static str = "inlining";
     pub const KEEP_INLINE_FUNS: &'static str = "keep-inline-funs";
     pub const KEEP_UNINIT_ANNOTATIONS: &'static str = "keep-uninit-annotations";
+    pub const LAMBDA_FIELDS: &'static str = "lambda-fields";
     pub const LAMBDA_LIFTING: &'static str = "lambda-lifting";
+    pub const LAMBDA_PARAMS: &'static str = "lambda-params";
+    pub const LAMBDA_RESULTS: &'static str = "lambda-results";
+    pub const LAMBDA_VALUES: &'static str = "lambda-values";
     pub const LINT_CHECKS: &'static str = "lint-checks";
     pub const OPTIMIZE: &'static str = "optimize";
     pub const OPTIMIZE_EXTRA: &'static str = "optimize-extra";
diff --git a/third_party/move/move-compiler-v2/src/file_format_generator/module_generator.rs b/third_party/move/move-compiler-v2/src/file_format_generator/module_generator.rs
index 4fd794aca6c6b..b371d7f17cf2e 100644
--- a/third_party/move/move-compiler-v2/src/file_format_generator/module_generator.rs
+++ b/third_party/move/move-compiler-v2/src/file_format_generator/module_generator.rs
@@ -365,7 +365,20 @@ impl ModuleGenerator {
                     ReferenceKind::Mutable => FF::SignatureToken::MutableReference(target_ty),
                 }
             },
-            Fun(_, _) | TypeDomain(_) | ResourceDomain(_, _, _) | Error | Var(_) => {
+            Fun(_param_ty, _result_ty) => {
+                // let _param_ty = Box::new(self.signature_token(ctx, loc, param_ty));
+                // let _result_ty = Box::new(self.signature_token(ctx, loc, result_ty));
+                // TODO(LAMBDA)
+                ctx.error(
+                    loc,
+                    format!(
+                        "Unexpected type: {}",
+                        ty.display(&ctx.env.get_type_display_ctx())
+                    ),
+                );
+                FF::SignatureToken::Bool
+            },
+            TypeDomain(_) | ResourceDomain(_, _, _) | Error | Var(_) => {
                 ctx.internal_error(
                     loc,
                     format!(
diff --git a/third_party/move/move-compiler-v2/tests/bytecode-generator/assign.exp b/third_party/move/move-compiler-v2/tests/bytecode-generator/assign.exp
index deeab73004ab4..19a38d4478a92 100644
--- a/third_party/move/move-compiler-v2/tests/bytecode-generator/assign.exp
+++ b/third_party/move/move-compiler-v2/tests/bytecode-generator/assign.exp
@@ -5,7 +5,7 @@ module 0x42::assign {
     }
     struct S {
         f: u64,
-        g: 0x42::assign::T,
+        g: T,
     }
     private fun assign_field(s: &mut S,f: u64) {
         select assign::S.f<&mut S>(s) = f;
diff --git a/third_party/move/move-compiler-v2/tests/bytecode-generator/borrow_deref_optimize.exp b/third_party/move/move-compiler-v2/tests/bytecode-generator/borrow_deref_optimize.exp
index ae6515bb0501c..bc23929966e0e 100644
--- a/third_party/move/move-compiler-v2/tests/bytecode-generator/borrow_deref_optimize.exp
+++ b/third_party/move/move-compiler-v2/tests/bytecode-generator/borrow_deref_optimize.exp
@@ -4,7 +4,7 @@ module 0x42::test {
         value: bool,
     }
     private fun no_optimize_resource(): bool
-        acquires 0x42::test::X(*)
+        acquires X(*)
      {
         {
           let x: &mut X = Borrow(Mutable)(Deref(BorrowGlobal(Immutable)<X>(0x1)));
@@ -18,7 +18,7 @@ module 0x42::test {
         }
     }
     private fun optimize_resource(): bool
-        acquires 0x42::test::X(*)
+        acquires X(*)
      {
         {
           let x: &X = Borrow(Immutable)(Deref(BorrowGlobal(Immutable)<X>(0x1)));
diff --git a/third_party/move/move-compiler-v2/tests/bytecode-generator/bug_14471_receiver_inference.exp b/third_party/move/move-compiler-v2/tests/bytecode-generator/bug_14471_receiver_inference.exp
index e89103eda02a7..23007e7bf4d5e 100644
--- a/third_party/move/move-compiler-v2/tests/bytecode-generator/bug_14471_receiver_inference.exp
+++ b/third_party/move/move-compiler-v2/tests/bytecode-generator/bug_14471_receiver_inference.exp
@@ -1,11 +1,11 @@
 // -- Model dump before bytecode pipeline
 module 0x815::m {
     struct MyMap {
-        table: 0x815::m::Table<address, 0x815::m::ValueWrap>,
+        table: Table<address, ValueWrap>,
     }
     struct Table {
-        x: #0,
-        y: #1,
+        x: T1,
+        y: T2,
     }
     struct ValueWrap {
         val: u64,
@@ -17,7 +17,7 @@ module 0x815::m {
         Tuple()
     }
     public fun add_when_missing(key: address,val: u64)
-        acquires 0x815::m::MyMap(*)
+        acquires MyMap(*)
      {
         {
           let my_map: &mut MyMap = BorrowGlobal(Mutable)<MyMap>(0x815);
diff --git a/third_party/move/move-compiler-v2/tests/bytecode-generator/escape_autoref.exp b/third_party/move/move-compiler-v2/tests/bytecode-generator/escape_autoref.exp
index 9b8e310000ede..aae0dcbebfe42 100644
--- a/third_party/move/move-compiler-v2/tests/bytecode-generator/escape_autoref.exp
+++ b/third_party/move/move-compiler-v2/tests/bytecode-generator/escape_autoref.exp
@@ -10,7 +10,7 @@ module 0x42::m {
         Abort(0)
     }
     private fun owner_correct(o: Object): address
-        acquires 0x42::m::ObjectCore(*)
+        acquires ObjectCore(*)
      {
         {
           let addr: address = select m::Object.inner<Object>(o);
@@ -18,7 +18,7 @@ module 0x42::m {
         }
     }
     private fun owner_read_ref_missing(o: Object): address
-        acquires 0x42::m::ObjectCore(*)
+        acquires ObjectCore(*)
      {
         select m::ObjectCore.owner<&ObjectCore>(BorrowGlobal(Immutable)<ObjectCore>(select m::Object.inner<Object>(o)))
     }
diff --git a/third_party/move/move-compiler-v2/tests/bytecode-generator/fields.exp b/third_party/move/move-compiler-v2/tests/bytecode-generator/fields.exp
index 8806b10eaaeaf..4c2478d70c7e5 100644
--- a/third_party/move/move-compiler-v2/tests/bytecode-generator/fields.exp
+++ b/third_party/move/move-compiler-v2/tests/bytecode-generator/fields.exp
@@ -4,11 +4,11 @@ module 0x42::fields {
         h: u64,
     }
     struct G {
-        f: #0,
+        f: X,
     }
     struct S {
         f: u64,
-        g: 0x42::fields::T,
+        g: T,
     }
     private fun read_generic_val(x: G<u64>): u64 {
         select fields::G.f<G<u64>>(x)
diff --git a/third_party/move/move-compiler-v2/tests/bytecode-generator/fields_invalid.exp b/third_party/move/move-compiler-v2/tests/bytecode-generator/fields_invalid.exp
index 4911ab49100bf..91fc860a9e2da 100644
--- a/third_party/move/move-compiler-v2/tests/bytecode-generator/fields_invalid.exp
+++ b/third_party/move/move-compiler-v2/tests/bytecode-generator/fields_invalid.exp
@@ -5,7 +5,7 @@ module 0x42::fields {
     }
     struct S {
         f: u64,
-        g: 0x42::fields::T,
+        g: T,
     }
     private fun write_ref(x: &S) {
         select fields::T.h<T>(select fields::S.g<&S>(x)) = 42;
diff --git a/third_party/move/move-compiler-v2/tests/bytecode-generator/globals.exp b/third_party/move/move-compiler-v2/tests/bytecode-generator/globals.exp
index 60f8155f1393d..58f17e58316dc 100644
--- a/third_party/move/move-compiler-v2/tests/bytecode-generator/globals.exp
+++ b/third_party/move/move-compiler-v2/tests/bytecode-generator/globals.exp
@@ -19,7 +19,7 @@ module 0x42::globals {
         Tuple()
     }
     private fun read(a: address): u64
-        acquires 0x42::globals::R(*)
+        acquires R(*)
      {
         {
           let r: &R = BorrowGlobal(Immutable)<R>(a);
@@ -27,7 +27,7 @@ module 0x42::globals {
         }
     }
     private fun write(a: address,x: u64): u64
-        acquires 0x42::globals::R(*)
+        acquires R(*)
      {
         {
           let r: &mut R = BorrowGlobal(Mutable)<R>(a);
diff --git a/third_party/move/move-compiler-v2/tests/bytecode-generator/matching_ability_err.exp b/third_party/move/move-compiler-v2/tests/bytecode-generator/matching_ability_err.exp
index a3dfa3d3f7cab..06001c73b254d 100644
--- a/third_party/move/move-compiler-v2/tests/bytecode-generator/matching_ability_err.exp
+++ b/third_party/move/move-compiler-v2/tests/bytecode-generator/matching_ability_err.exp
@@ -15,11 +15,11 @@ module 0xc0ffee::m {
     enum Outer {
         None,
         One {
-            i: 0xc0ffee::m::Inner,
+            i: Inner,
         }
         Two {
-            i: 0xc0ffee::m::Inner,
-            b: 0xc0ffee::m::Box,
+            i: Inner,
+            b: Box,
         }
     }
     public fun condition_requires_copy(o: Outer): Outer {
diff --git a/third_party/move/move-compiler-v2/tests/bytecode-generator/matching_coverage_err.exp b/third_party/move/move-compiler-v2/tests/bytecode-generator/matching_coverage_err.exp
index 805678cbb5cf7..cebf2819486bb 100644
--- a/third_party/move/move-compiler-v2/tests/bytecode-generator/matching_coverage_err.exp
+++ b/third_party/move/move-compiler-v2/tests/bytecode-generator/matching_coverage_err.exp
@@ -15,11 +15,11 @@ module 0xc0ffee::m {
     enum Outer {
         None,
         One {
-            i: 0xc0ffee::m::Inner,
+            i: Inner,
         }
         Two {
-            i: 0xc0ffee::m::Inner,
-            b: 0xc0ffee::m::Box,
+            i: Inner,
+            b: Box,
         }
     }
     public fun exhaustive_tuple(i: &Inner) {
diff --git a/third_party/move/move-compiler-v2/tests/bytecode-generator/matching_ok.exp b/third_party/move/move-compiler-v2/tests/bytecode-generator/matching_ok.exp
index c7116654488be..a271791a51a0b 100644
--- a/third_party/move/move-compiler-v2/tests/bytecode-generator/matching_ok.exp
+++ b/third_party/move/move-compiler-v2/tests/bytecode-generator/matching_ok.exp
@@ -42,17 +42,17 @@ module 0xc0ffee::m {
     enum Option {
         None,
         Some {
-            value: #0,
+            value: A,
         }
     }
     enum Outer {
         None,
         One {
-            i: 0xc0ffee::m::Inner,
+            i: Inner,
         }
         Two {
-            i: 0xc0ffee::m::Inner,
-            b: 0xc0ffee::m::Box,
+            i: Inner,
+            b: Box,
         }
     }
     public fun inner_value(self: Inner): u64 {
diff --git a/third_party/move/move-compiler-v2/tests/bytecode-generator/mutate_immutable_cmp.exp b/third_party/move/move-compiler-v2/tests/bytecode-generator/mutate_immutable_cmp.exp
index f78da5ffeca47..bd21055b8ac2e 100644
--- a/third_party/move/move-compiler-v2/tests/bytecode-generator/mutate_immutable_cmp.exp
+++ b/third_party/move/move-compiler-v2/tests/bytecode-generator/mutate_immutable_cmp.exp
@@ -1,7 +1,7 @@
 // -- Model dump before bytecode pipeline
 module 0x8675309::M {
     struct T {
-        s: 0x8675309::M::S,
+        s: S,
     }
     struct G {
         dummy_field: bool,
diff --git a/third_party/move/move-compiler-v2/tests/bytecode-generator/pack_unpack.exp b/third_party/move/move-compiler-v2/tests/bytecode-generator/pack_unpack.exp
index 50897a53c5ba0..17e454f6177ee 100644
--- a/third_party/move/move-compiler-v2/tests/bytecode-generator/pack_unpack.exp
+++ b/third_party/move/move-compiler-v2/tests/bytecode-generator/pack_unpack.exp
@@ -5,7 +5,7 @@ module 0x42::pack_unpack {
     }
     struct S {
         f: u64,
-        g: 0x42::pack_unpack::T,
+        g: T,
     }
     private fun pack(x: u64,y: u64): S {
         pack pack_unpack::S(x, pack pack_unpack::T(y))
diff --git a/third_party/move/move-compiler-v2/tests/bytecode-generator/spec_construct.exp b/third_party/move/move-compiler-v2/tests/bytecode-generator/spec_construct.exp
index 906f7604749fa..6108d5abdaa96 100644
--- a/third_party/move/move-compiler-v2/tests/bytecode-generator/spec_construct.exp
+++ b/third_party/move/move-compiler-v2/tests/bytecode-generator/spec_construct.exp
@@ -5,7 +5,7 @@ module 0x42::m {
         k: u8,
     }
     struct S {
-        data: vector<0x42::m::E>,
+        data: vector<E>,
     }
     public fun foo(v: &S): u8 {
         select m::E.k<&E>(vector::borrow<E>(Borrow(Immutable)(select m::S.data<&S>(v)), 0))
diff --git a/third_party/move/move-compiler-v2/tests/checking-lang-v1/use_struct_overlap_with_module.exp b/third_party/move/move-compiler-v2/tests/checking-lang-v1/use_struct_overlap_with_module.exp
index e9e0328eb51f1..e554327c1f4f0 100644
--- a/third_party/move/move-compiler-v2/tests/checking-lang-v1/use_struct_overlap_with_module.exp
+++ b/third_party/move/move-compiler-v2/tests/checking-lang-v1/use_struct_overlap_with_module.exp
@@ -7,8 +7,8 @@ module 0x2::X {
 module 0x2::M {
     use 0x2::X::{Self, S as X}; // resolved as: 0x2::X
     struct A {
-        f1: 0x2::X::S,
-        f2: 0x2::X::S,
+        f1: X::S,
+        f2: X::S,
     }
 } // end 0x2::M
 
diff --git a/third_party/move/move-compiler-v2/tests/checking/abilities/v1/ability_constraints.exp b/third_party/move/move-compiler-v2/tests/checking/abilities/v1/ability_constraints.exp
index dcaf90f90259f..55f8fe820c1e2 100644
--- a/third_party/move/move-compiler-v2/tests/checking/abilities/v1/ability_constraints.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/abilities/v1/ability_constraints.exp
@@ -1,11 +1,11 @@
 // -- Model dump before bytecode pipeline
 module 0x42::M {
     struct Box {
-        f: #0,
+        f: T,
     }
     struct Pair {
-        f1: #0,
-        f2: #1,
+        f1: T1,
+        f2: T2,
     }
     struct R {
         dummy_field: bool,
diff --git a/third_party/move/move-compiler-v2/tests/checking/abilities/v1/phantom_param_op_abilities.exp b/third_party/move/move-compiler-v2/tests/checking/abilities/v1/phantom_param_op_abilities.exp
index 21ea211538722..01ca296b54601 100644
--- a/third_party/move/move-compiler-v2/tests/checking/abilities/v1/phantom_param_op_abilities.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/abilities/v1/phantom_param_op_abilities.exp
@@ -1,22 +1,22 @@
 // -- Model dump before bytecode pipeline
 module 0x42::M {
     struct HasCopy {
-        a: #1,
+        a: T2,
     }
     struct HasDrop {
-        a: #1,
+        a: T2,
     }
     struct HasKey {
-        a: #1,
+        a: T2,
     }
     struct HasStore {
-        a: #1,
+        a: T2,
     }
     struct NoAbilities {
         dummy_field: bool,
     }
     struct RequireStore {
-        a: #0,
+        a: T,
     }
     private fun f1(ref: &mut HasDrop<NoAbilities, u64>) {
         ref = pack M::HasDrop<NoAbilities, u64>(1);
@@ -37,7 +37,7 @@ module 0x42::M {
         Tuple()
     }
     private fun f6(): HasKey<NoAbilities, u64>
-        acquires 0x42::M::HasKey(*)
+        acquires HasKey(*)
      {
         MoveFrom<HasKey<NoAbilities, u64>>(0x0)
     }
diff --git a/third_party/move/move-compiler-v2/tests/checking/abilities/v1/phantom_params_constraint_abilities.exp b/third_party/move/move-compiler-v2/tests/checking/abilities/v1/phantom_params_constraint_abilities.exp
index 5666042391855..278c608e4dbf9 100644
--- a/third_party/move/move-compiler-v2/tests/checking/abilities/v1/phantom_params_constraint_abilities.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/abilities/v1/phantom_params_constraint_abilities.exp
@@ -1,37 +1,37 @@
 // -- Model dump before bytecode pipeline
 module 0x42::M {
     struct HasAbilities {
-        a: #1,
+        a: T2,
     }
     struct HasCopy {
-        a: #1,
+        a: T2,
     }
     struct HasDrop {
-        a: #1,
+        a: T2,
     }
     struct HasKey {
-        a: #1,
+        a: T2,
     }
     struct HasStore {
-        a: #1,
+        a: T2,
     }
     struct NoAbilities {
         a: bool,
     }
     struct S1 {
-        a: #0,
+        a: T,
     }
     struct S2 {
-        a: 0x42::M::S1<0x42::M::HasAbilities<0x42::M::NoAbilities, u64>>,
+        a: S1<HasAbilities<NoAbilities, u64>>,
     }
     struct S3 {
-        a: #0,
-        b: #1,
-        c: #2,
-        d: #3,
+        a: T1,
+        b: T2,
+        c: T3,
+        d: T4,
     }
     struct S4 {
-        a: 0x42::M::S3<0x42::M::HasDrop<0x42::M::NoAbilities, u64>, 0x42::M::HasCopy<0x42::M::NoAbilities, u64>, 0x42::M::HasStore<0x42::M::NoAbilities, u64>, 0x42::M::HasKey<0x42::M::NoAbilities, u64>>,
+        a: S3<HasDrop<NoAbilities, u64>, HasCopy<NoAbilities, u64>, HasStore<NoAbilities, u64>, HasKey<NoAbilities, u64>>,
     }
     private fun f1<T>() {
         Tuple()
diff --git a/third_party/move/move-compiler-v2/tests/checking/abilities/v1/phantom_params_field_abilities.exp b/third_party/move/move-compiler-v2/tests/checking/abilities/v1/phantom_params_field_abilities.exp
index c9c9943eb3973..2631fcfd257a1 100644
--- a/third_party/move/move-compiler-v2/tests/checking/abilities/v1/phantom_params_field_abilities.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/abilities/v1/phantom_params_field_abilities.exp
@@ -1,31 +1,31 @@
 // -- Model dump before bytecode pipeline
 module 0x42::M {
     struct HasCopy {
-        a: #1,
+        a: T2,
     }
     struct HasDrop {
-        a: #1,
+        a: T2,
     }
     struct HasKey {
-        a: #1,
+        a: T2,
     }
     struct HasStore {
-        a: #1,
+        a: T2,
     }
     struct NoAbilities {
         dummy_field: bool,
     }
     struct S1 {
-        a: 0x42::M::HasDrop<0x42::M::NoAbilities, u64>,
+        a: HasDrop<NoAbilities, u64>,
     }
     struct S2 {
-        a: 0x42::M::HasCopy<0x42::M::NoAbilities, u64>,
+        a: HasCopy<NoAbilities, u64>,
     }
     struct S3 {
-        a: 0x42::M::HasStore<0x42::M::NoAbilities, u64>,
+        a: HasStore<NoAbilities, u64>,
     }
     struct S4 {
-        a: 0x42::M::HasStore<0x42::M::NoAbilities, u64>,
+        a: HasStore<NoAbilities, u64>,
     }
 } // end 0x42::M
 
diff --git a/third_party/move/move-compiler-v2/tests/checking/access_specifiers/access_ok.exp b/third_party/move/move-compiler-v2/tests/checking/access_specifiers/access_ok.exp
index 6482442cfa288..1d58dcea66e0f 100644
--- a/third_party/move/move-compiler-v2/tests/checking/access_specifiers/access_ok.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/access_specifiers/access_ok.exp
@@ -33,7 +33,7 @@ module 0x42::m {
         dummy_field: bool,
     }
     private fun f1()
-        acquires 0x42::m::S(*)
+        acquires S(*)
      {
         Tuple()
     }
@@ -53,17 +53,17 @@ module 0x42::m {
         Tuple()
     }
     private fun f2()
-        reads 0x42::m::S(*)
+        reads S(*)
      {
         Tuple()
     }
     private fun f3()
-        writes 0x42::m::S(*)
+        writes S(*)
      {
         Tuple()
     }
     private fun f4()
-        acquires 0x42::m::S(*)
+        acquires S(*)
      {
         Tuple()
     }
@@ -93,11 +93,11 @@ module 0x42::m {
         Tuple()
     }
     private fun f_multiple()
-        acquires 0x42::m::R(*)
-        reads 0x42::m::R(*)
-        writes 0x42::m::T(*)
-        writes 0x42::m::S(*)
-        reads 0x42::m::G<u64>(*)
+        acquires R(*)
+        reads R(*)
+        writes T(*)
+        writes S(*)
+        reads G<u64>(*)
      {
         Tuple()
     }
diff --git a/third_party/move/move-compiler-v2/tests/checking/access_specifiers/acquires_list_generic.exp b/third_party/move/move-compiler-v2/tests/checking/access_specifiers/acquires_list_generic.exp
index 1c78e50c8f0b2..d6f4603030fd1 100644
--- a/third_party/move/move-compiler-v2/tests/checking/access_specifiers/acquires_list_generic.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/access_specifiers/acquires_list_generic.exp
@@ -10,7 +10,7 @@ module 0x42::M {
         dummy_field: bool,
     }
     private fun foo()
-        acquires 0x42::M::B<0x42::M::CupC<0x42::M::R>>(*)
+        acquires B<CupC<R>>(*)
      {
         Abort(0)
     }
diff --git a/third_party/move/move-compiler-v2/tests/checking/dotdot/dotdot_valid.exp b/third_party/move/move-compiler-v2/tests/checking/dotdot/dotdot_valid.exp
index 8de9c715617c4..e0c1f7c341512 100644
--- a/third_party/move/move-compiler-v2/tests/checking/dotdot/dotdot_valid.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/dotdot/dotdot_valid.exp
@@ -10,7 +10,7 @@ module 0x42::test {
         }
         C {
             x: u8,
-            y: 0x42::test::S1,
+            y: S1,
         }
     }
     struct S0 {
@@ -21,23 +21,23 @@ module 0x42::test {
     }
     struct S2 {
         0: bool,
-        1: 0x42::test::S0,
+        1: S0,
     }
     struct S3 {
         x: bool,
         y: u8,
     }
     struct S4 {
-        x: #0,
-        y: 0x42::test::S3,
+        x: T,
+        y: S3,
     }
     struct S5 {
-        0: #0,
-        1: #1,
+        0: T,
+        1: U,
     }
     struct S6 {
-        x: #0,
-        y: #1,
+        x: T,
+        y: U,
     }
     struct S7 {
         0: u8,
diff --git a/third_party/move/move-compiler-v2/tests/checking/indexing/examples_book.exp b/third_party/move/move-compiler-v2/tests/checking/indexing/examples_book.exp
index 225201e7eb6d2..979ec749c6216 100644
--- a/third_party/move/move-compiler-v2/tests/checking/indexing/examples_book.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/indexing/examples_book.exp
@@ -4,7 +4,7 @@ module 0x1::m {
         value: bool,
     }
     private fun f1()
-        acquires 0x1::m::R(*)
+        acquires R(*)
      {
         {
           let x: &mut R = BorrowGlobal(Mutable)<R>(0x1);
diff --git a/third_party/move/move-compiler-v2/tests/checking/inlining/lambda3.exp b/third_party/move/move-compiler-v2/tests/checking/inlining/lambda3.exp
new file mode 100644
index 0000000000000..7d3fd078fd386
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/checking/inlining/lambda3.exp
@@ -0,0 +1,24 @@
+// -- Model dump before bytecode pipeline
+module 0x8675309::M {
+    public fun lambda_not_allowed() {
+        {
+          let _x: |u64|u64 = |i: u64| Add<u64>(i, 1);
+          Tuple()
+        }
+    }
+} // end 0x8675309::M
+
+// -- Sourcified model before bytecode pipeline
+module 0x8675309::M {
+    public fun lambda_not_allowed() {
+        let _x = |i| i + 1;
+    }
+}
+
+
+Diagnostics:
+error: Function-typed values not yet supported except as parameters to calls to inline functions
+   ┌─ tests/checking/inlining/lambda3.move:77:18
+   │
+77 │         let _x = |i| i + 1; // expected lambda not allowed
+   │                  ^^^^^^^^^
diff --git a/third_party/move/move-compiler-v2/tests/checking/inlining/lambda3.move b/third_party/move/move-compiler-v2/tests/checking/inlining/lambda3.move
new file mode 100644
index 0000000000000..5450bac87c1cb
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/checking/inlining/lambda3.move
@@ -0,0 +1,99 @@
+module 0x8675309::M {
+    // use 0x1::XVector;
+
+    // public inline fun foreach<T>(v: &vector<T>, action: |&T|) { // expected to be not implemented
+    //     let i = 0;
+    //     while (i < XVector::length(v)) {
+    //         action(XVector::borrow(v, i));
+    //         i = i + 1;
+    //     }
+    // }
+
+    // public inline fun reduce<R, T>(v: vector<T>, accu: R, reducer: |T, R|R): R {
+    //     while (!XVector::is_empty(&v)) {
+    //         accu = reducer(XVector::pop_back(&mut v), accu);
+    //     };
+    //     accu
+    // }
+
+
+    // public fun correct_foreach() {
+    //     let v = vector[1, 2, 3];
+    //     let sum = 0;
+    //     foreach(&v, |e| sum = sum + *e) // expected to be not implemented
+    // }
+
+    // public fun correct_reduce(): u64 {
+    //     let v = vector[1, 2, 3];
+    //     reduce(v, 0, |t, r| t + r)
+    // }
+
+    // public fun corrected_nested() {
+    //     let v = vector[vector[1,2], vector[3]];
+    //     let sum = 0;
+    //     foreach(&v, |e| sum = sum + reduce!(*e, 0, |t, r| t + r));
+    // }
+
+    // public inline fun wrong_local_call_arg_count<T>(v: &vector<T>, action: |&T|) {
+    //     let i = 0;
+    //     while (i < XVector::length(v)) {
+    //         action(XVector::borrow(v, i), i); // expected to have wrong argument count
+    //         i = i + 1;
+    //     }
+    // }
+
+    // public inline fun wrong_local_call_arg_type<T>(v: &vector<T>, action: |&T|) {
+    //     let i = 0;
+    //     while (i < XVector::length(v)) {
+    //         action(i); // expected to have wrong argument type
+    //         i = i + 1;
+    //     }
+    // }
+
+    // public inline fun wrong_local_call_result_type<T>(v: &vector<T>, action: |&T|) {
+    //     let i = 0;
+    //     while (i < XVector::length(v)) {
+    //         i = i + action(XVector::borrow(v, i)); // expected to have wrong result type
+    //     }
+    // }
+
+    // public fun wrong_local_call_no_fun(x: u64) {
+    //     x(1) // expected to be not a function
+    // }
+
+    // public fun wrong_lambda_inferred_type() {
+    //     let v = vector[1, 2, 3];
+    //     let sum = 0;
+    //     foreach(&v, |e| sum = sum + e) // expected to cannot infer type
+    // }
+
+    // public fun wrong_lambda_result_type() {
+    //     let v = vector[1, 2, 3];
+    //     let sum = 0;
+    //     foreach(&v, |e| { sum = sum + *e; *e }) // expected to have wrong result type of lambda
+    // }
+
+    public fun lambda_not_allowed() {
+        let _x = |i| i + 1; // expected lambda not allowed
+    }
+
+    // struct FieldFunNotAllowed {
+    //     f: |u64|u64, // expected lambda not allowed
+    // }
+
+    // public fun fun_arg_lambda_not_allowed(x: |u64|) {} // expected lambda not allowed
+
+    // public inline fun macro_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
+    //     abort (1)
+    // }
+    // public fun fun_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
+    //     abort (1)
+    // }
+}
+
+// module 0x1::XVector {
+//     public fun length<T>(v: &vector<T>): u64 { abort(1) }
+//     public fun is_empty<T>(v: &vector<T>): bool { abort(1) }
+//     public fun borrow<T>(v: &vector<T>, i: u64): &T { abort(1) }
+//     public fun pop_back<T>(v: &mut vector<T>): T { abort(1) }
+// }
diff --git a/third_party/move/move-compiler-v2/tests/checking/inlining/lambda4.exp b/third_party/move/move-compiler-v2/tests/checking/inlining/lambda4.exp
new file mode 100644
index 0000000000000..7a6fd81d69593
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/checking/inlining/lambda4.exp
@@ -0,0 +1,13 @@
+
+Diagnostics:
+error: Functions may not return function-typed values, but function `M::macro_result_lambda_not_allowed` return type is `|u64|`:
+   ┌─ tests/checking/inlining/lambda4.move:86:23
+   │
+86 │     public inline fun macro_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
+   │                       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+error: Functions may not return function-typed values, but function `M::fun_result_lambda_not_allowed` return type is `|u64|`:
+   ┌─ tests/checking/inlining/lambda4.move:89:16
+   │
+89 │     public fun fun_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
+   │                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
diff --git a/third_party/move/move-compiler-v2/tests/checking/inlining/lambda4.move b/third_party/move/move-compiler-v2/tests/checking/inlining/lambda4.move
new file mode 100644
index 0000000000000..4a378b7e14b10
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/checking/inlining/lambda4.move
@@ -0,0 +1,99 @@
+module 0x8675309::M {
+    // use 0x1::XVector;
+
+    // public inline fun foreach<T>(v: &vector<T>, action: |&T|) { // expected to be not implemented
+    //     let i = 0;
+    //     while (i < XVector::length(v)) {
+    //         action(XVector::borrow(v, i));
+    //         i = i + 1;
+    //     }
+    // }
+
+    // public inline fun reduce<R, T>(v: vector<T>, accu: R, reducer: |T, R|R): R {
+    //     while (!XVector::is_empty(&v)) {
+    //         accu = reducer(XVector::pop_back(&mut v), accu);
+    //     };
+    //     accu
+    // }
+
+
+    // public fun correct_foreach() {
+    //     let v = vector[1, 2, 3];
+    //     let sum = 0;
+    //     foreach(&v, |e| sum = sum + *e) // expected to be not implemented
+    // }
+
+    // public fun correct_reduce(): u64 {
+    //     let v = vector[1, 2, 3];
+    //     reduce(v, 0, |t, r| t + r)
+    // }
+
+    // public fun corrected_nested() {
+    //     let v = vector[vector[1,2], vector[3]];
+    //     let sum = 0;
+    //     foreach(&v, |e| sum = sum + reduce!(*e, 0, |t, r| t + r));
+    // }
+
+    // public inline fun wrong_local_call_arg_count<T>(v: &vector<T>, action: |&T|) {
+    //     let i = 0;
+    //     while (i < XVector::length(v)) {
+    //         action(XVector::borrow(v, i), i); // expected to have wrong argument count
+    //         i = i + 1;
+    //     }
+    // }
+
+    // public inline fun wrong_local_call_arg_type<T>(v: &vector<T>, action: |&T|) {
+    //     let i = 0;
+    //     while (i < XVector::length(v)) {
+    //         action(i); // expected to have wrong argument type
+    //         i = i + 1;
+    //     }
+    // }
+
+    // public inline fun wrong_local_call_result_type<T>(v: &vector<T>, action: |&T|) {
+    //     let i = 0;
+    //     while (i < XVector::length(v)) {
+    //         i = i + action(XVector::borrow(v, i)); // expected to have wrong result type
+    //     }
+    // }
+
+    // public fun wrong_local_call_no_fun(x: u64) {
+    //     x(1) // expected to be not a function
+    // }
+
+    // public fun wrong_lambda_inferred_type() {
+    //     let v = vector[1, 2, 3];
+    //     let sum = 0;
+    //     foreach(&v, |e| sum = sum + e) // expected to cannot infer type
+    // }
+
+    // public fun wrong_lambda_result_type() {
+    //     let v = vector[1, 2, 3];
+    //     let sum = 0;
+    //     foreach(&v, |e| { sum = sum + *e; *e }) // expected to have wrong result type of lambda
+    // }
+
+    // public fun lambda_not_allowed() {
+    //     let _x = |i| i + 1; // expected lambda not allowed
+    // }
+
+    // struct FieldFunNotAllowed {
+    //     f: |u64|u64, // expected lambda not allowed
+    // }
+
+    // public fun fun_arg_lambda_not_allowed(x: |u64|) {} // expected lambda not allowed
+
+    public inline fun macro_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
+        abort (1)
+    }
+    public fun fun_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
+        abort (1)
+    }
+}
+
+// module 0x1::XVector {
+//     public fun length<T>(v: &vector<T>): u64 { abort(1) }
+//     public fun is_empty<T>(v: &vector<T>): bool { abort(1) }
+//     public fun borrow<T>(v: &vector<T>, i: u64): &T { abort(1) }
+//     public fun pop_back<T>(v: &mut vector<T>): T { abort(1) }
+// }
diff --git a/third_party/move/move-compiler-v2/tests/checking/inlining/lambda5.exp b/third_party/move/move-compiler-v2/tests/checking/inlining/lambda5.exp
new file mode 100644
index 0000000000000..8dc25cb601fb4
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/checking/inlining/lambda5.exp
@@ -0,0 +1,7 @@
+
+Diagnostics:
+error: Functions may not return function-typed values, but function `M::macro_result_lambda_not_allowed` return type is `|u64|`:
+   ┌─ tests/checking/inlining/lambda5.move:86:23
+   │
+86 │     public inline fun macro_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
+   │                       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
diff --git a/third_party/move/move-compiler-v2/tests/checking/inlining/lambda5.move b/third_party/move/move-compiler-v2/tests/checking/inlining/lambda5.move
new file mode 100644
index 0000000000000..291c8e5cab61f
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/checking/inlining/lambda5.move
@@ -0,0 +1,99 @@
+module 0x8675309::M {
+    // use 0x1::XVector;
+
+    // public inline fun foreach<T>(v: &vector<T>, action: |&T|) { // expected to be not implemented
+    //     let i = 0;
+    //     while (i < XVector::length(v)) {
+    //         action(XVector::borrow(v, i));
+    //         i = i + 1;
+    //     }
+    // }
+
+    // public inline fun reduce<R, T>(v: vector<T>, accu: R, reducer: |T, R|R): R {
+    //     while (!XVector::is_empty(&v)) {
+    //         accu = reducer(XVector::pop_back(&mut v), accu);
+    //     };
+    //     accu
+    // }
+
+
+    // public fun correct_foreach() {
+    //     let v = vector[1, 2, 3];
+    //     let sum = 0;
+    //     foreach(&v, |e| sum = sum + *e) // expected to be not implemented
+    // }
+
+    // public fun correct_reduce(): u64 {
+    //     let v = vector[1, 2, 3];
+    //     reduce(v, 0, |t, r| t + r)
+    // }
+
+    // public fun corrected_nested() {
+    //     let v = vector[vector[1,2], vector[3]];
+    //     let sum = 0;
+    //     foreach(&v, |e| sum = sum + reduce!(*e, 0, |t, r| t + r));
+    // }
+
+    // public inline fun wrong_local_call_arg_count<T>(v: &vector<T>, action: |&T|) {
+    //     let i = 0;
+    //     while (i < XVector::length(v)) {
+    //         action(XVector::borrow(v, i), i); // expected to have wrong argument count
+    //         i = i + 1;
+    //     }
+    // }
+
+    // public inline fun wrong_local_call_arg_type<T>(v: &vector<T>, action: |&T|) {
+    //     let i = 0;
+    //     while (i < XVector::length(v)) {
+    //         action(i); // expected to have wrong argument type
+    //         i = i + 1;
+    //     }
+    // }
+
+    // public inline fun wrong_local_call_result_type<T>(v: &vector<T>, action: |&T|) {
+    //     let i = 0;
+    //     while (i < XVector::length(v)) {
+    //         i = i + action(XVector::borrow(v, i)); // expected to have wrong result type
+    //     }
+    // }
+
+    // public fun wrong_local_call_no_fun(x: u64) {
+    //     x(1) // expected to be not a function
+    // }
+
+    // public fun wrong_lambda_inferred_type() {
+    //     let v = vector[1, 2, 3];
+    //     let sum = 0;
+    //     foreach(&v, |e| sum = sum + e) // expected to cannot infer type
+    // }
+
+    // public fun wrong_lambda_result_type() {
+    //     let v = vector[1, 2, 3];
+    //     let sum = 0;
+    //     foreach(&v, |e| { sum = sum + *e; *e }) // expected to have wrong result type of lambda
+    // }
+
+    // public fun lambda_not_allowed() {
+    //     let _x = |i| i + 1; // expected lambda not allowed
+    // }
+
+    // struct FieldFunNotAllowed {
+    //     f: |u64|u64, // expected lambda not allowed
+    // }
+
+    // public fun fun_arg_lambda_not_allowed(x: |u64|) {} // expected lambda not allowed
+
+    public inline fun macro_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
+        abort (1)
+    }
+    // public fun fun_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
+    //     abort (1)
+    // }
+}
+
+// module 0x1::XVector {
+//     public fun length<T>(v: &vector<T>): u64 { abort(1) }
+//     public fun is_empty<T>(v: &vector<T>): bool { abort(1) }
+//     public fun borrow<T>(v: &vector<T>, i: u64): &T { abort(1) }
+//     public fun pop_back<T>(v: &mut vector<T>): T { abort(1) }
+// }
diff --git a/third_party/move/move-compiler-v2/tests/checking/inlining/non_lambda_arg.exp b/third_party/move/move-compiler-v2/tests/checking/inlining/non_lambda_arg.exp
index aa83fbc21a0bd..88cfe01e12e08 100644
--- a/third_party/move/move-compiler-v2/tests/checking/inlining/non_lambda_arg.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/inlining/non_lambda_arg.exp
@@ -4,10 +4,10 @@ error: Only inline functions may have function-typed parameters, but non-inline
   ┌─ tests/checking/inlining/non_lambda_arg.move:4:16
   │
 4 │     public fun incorrect_sort<T: copy>(arr: &mut vector<T>, a_less_b: |T, T| bool) {
-  │                ^^^^^^^^^^^^^^                               -------- Parameter `a_less_b` has a function type.
+  │                ^^^^^^^^^^^^^^                               -------- Parameter `a_less_b` has function-valued type `|(T, T)|bool`.
 
 error: Only inline functions may have function-typed parameters, but non-inline function `sort::incorrect_sort_recursive` has a function parameter:
   ┌─ tests/checking/inlining/non_lambda_arg.move:9:16
   │
 9 │     public fun incorrect_sort_recursive<T: copy>(arr: &mut vector<T>, low: u64, high: u64, a_less_b: |T, T| bool) {
-  │                ^^^^^^^^^^^^^^^^^^^^^^^^                                                    -------- Parameter `a_less_b` has a function type.
+  │                ^^^^^^^^^^^^^^^^^^^^^^^^                                                    -------- Parameter `a_less_b` has function-valued type `|(T, T)|bool`.
diff --git a/third_party/move/move-compiler-v2/tests/checking/inlining/resources_valid.exp b/third_party/move/move-compiler-v2/tests/checking/inlining/resources_valid.exp
index 1a3c18119c4dd..67888d34bf208 100644
--- a/third_party/move/move-compiler-v2/tests/checking/inlining/resources_valid.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/inlining/resources_valid.exp
@@ -16,7 +16,7 @@ module 0x42::token {
         val: u64,
     }
     public fun get_value(ref: &objects::ReaderRef<Token>): u64
-        acquires 0x42::token::Token(*)
+        acquires Token(*)
      {
         select token::Token.val<&Token>({
           let (ref: &objects::ReaderRef<Token>): (&objects::ReaderRef<Token>) = Tuple(ref);
diff --git a/third_party/move/move-compiler-v2/tests/checking/naming/duplicate_acquires_list_item.exp b/third_party/move/move-compiler-v2/tests/checking/naming/duplicate_acquires_list_item.exp
index e09b6408ae260..3a1b5c04d51a4 100644
--- a/third_party/move/move-compiler-v2/tests/checking/naming/duplicate_acquires_list_item.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/naming/duplicate_acquires_list_item.exp
@@ -7,20 +7,20 @@ module 0x8675309::M {
         dummy_field: bool,
     }
     private fun t0()
-        acquires 0x8675309::M::R(*)
-        acquires 0x8675309::M::X(*)
-        acquires 0x8675309::M::R(*)
+        acquires R(*)
+        acquires X(*)
+        acquires R(*)
      {
         BorrowGlobal(Mutable)<R>(0x1);
         BorrowGlobal(Mutable)<X>(0x1);
         Tuple()
     }
     private fun t1()
-        acquires 0x8675309::M::R(*)
-        acquires 0x8675309::M::X(*)
-        acquires 0x8675309::M::R(*)
-        acquires 0x8675309::M::R(*)
-        acquires 0x8675309::M::R(*)
+        acquires R(*)
+        acquires X(*)
+        acquires R(*)
+        acquires R(*)
+        acquires R(*)
      {
         BorrowGlobal(Mutable)<R>(0x1);
         BorrowGlobal(Mutable)<X>(0x1);
diff --git a/third_party/move/move-compiler-v2/tests/checking/naming/global_builtin_one_type_argument.exp b/third_party/move/move-compiler-v2/tests/checking/naming/global_builtin_one_type_argument.exp
index 85a59aab9e4b2..b2fecf533bafc 100644
--- a/third_party/move/move-compiler-v2/tests/checking/naming/global_builtin_one_type_argument.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/naming/global_builtin_one_type_argument.exp
@@ -4,7 +4,7 @@ module 0x8675309::M {
         dummy_field: bool,
     }
     private fun t(account: &signer)
-        acquires 0x8675309::M::R(*)
+        acquires R(*)
      {
         {
           let _: bool = exists<R>(0x0);
diff --git a/third_party/move/move-compiler-v2/tests/checking/naming/unused_type_parameter_struct.exp b/third_party/move/move-compiler-v2/tests/checking/naming/unused_type_parameter_struct.exp
index 3ae2e7bdc83b2..26343bf96eaf1 100644
--- a/third_party/move/move-compiler-v2/tests/checking/naming/unused_type_parameter_struct.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/naming/unused_type_parameter_struct.exp
@@ -49,17 +49,17 @@ module 0x42::test {
         dummy_field: bool,
     }
     struct S2 {
-        f: 0x42::test::S3<#1>,
+        f: S3<T2>,
     }
     struct S3 {
         dummy_field: bool,
     }
     struct S4 {
-        f: vector<#0>,
+        f: vector<T>,
     }
     struct S5 {
-        f: vector<#0>,
-        g: vector<#1>,
+        f: vector<T>,
+        g: vector<U>,
     }
 } // end 0x42::test
 
diff --git a/third_party/move/move-compiler-v2/tests/checking/naming/warning_dependency.exp b/third_party/move/move-compiler-v2/tests/checking/naming/warning_dependency.exp
index af81d60312b4a..406c3d29e1725 100644
--- a/third_party/move/move-compiler-v2/tests/checking/naming/warning_dependency.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/naming/warning_dependency.exp
@@ -18,17 +18,17 @@ module 0x42::test {
         dummy_field: bool,
     }
     struct S2 {
-        f: 0x42::test::S3<#1>,
+        f: S3<T2>,
     }
     struct S3 {
         dummy_field: bool,
     }
     struct S4 {
-        f: vector<#0>,
+        f: vector<T>,
     }
     struct S5 {
-        f: vector<#0>,
-        g: vector<#1>,
+        f: vector<T>,
+        g: vector<U>,
     }
 } // end 0x42::test
 
diff --git a/third_party/move/move-compiler-v2/tests/checking/positional_fields/assign_field.exp b/third_party/move/move-compiler-v2/tests/checking/positional_fields/assign_field.exp
index 81f20a0b029dc..c84034b0a95a8 100644
--- a/third_party/move/move-compiler-v2/tests/checking/positional_fields/assign_field.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/positional_fields/assign_field.exp
@@ -6,7 +6,7 @@ module 0x42::test {
             1: bool,
         }
         V2 {
-            0: 0x42::test::S3,
+            0: S3,
         }
     }
     struct S0 {
@@ -17,13 +17,13 @@ module 0x42::test {
         1: bool,
     }
     struct S2 {
-        0: 0x42::test::S0,
+        0: S0,
         1: u8,
     }
     struct S3 {
-        0: 0x42::test::S2,
-        1: 0x42::test::S0,
-        2: 0x42::test::S2,
+        0: S2,
+        1: S0,
+        2: S2,
     }
     private fun assign0(a: u64,b: bool) {
         {
diff --git a/third_party/move/move-compiler-v2/tests/checking/positional_fields/bind_anonymous_field.exp b/third_party/move/move-compiler-v2/tests/checking/positional_fields/bind_anonymous_field.exp
index 1a0b7be9954d6..f0ef1a992ba40 100644
--- a/third_party/move/move-compiler-v2/tests/checking/positional_fields/bind_anonymous_field.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/positional_fields/bind_anonymous_field.exp
@@ -2,10 +2,10 @@
 module 0x42::test {
     enum E1 {
         V1 {
-            0: 0x42::test::S0,
+            0: S0,
         }
         V2 {
-            0: 0x42::test::S1,
+            0: S1,
         }
     }
     struct S0 {
@@ -13,7 +13,7 @@ module 0x42::test {
     }
     struct S1 {
         0: bool,
-        1: 0x42::test::S0,
+        1: S0,
     }
     private fun match(x: E1) {
         match (x) {
diff --git a/third_party/move/move-compiler-v2/tests/checking/positional_fields/decl_ok.exp b/third_party/move/move-compiler-v2/tests/checking/positional_fields/decl_ok.exp
index d0188cbba98fb..28e3ab2edd260 100644
--- a/third_party/move/move-compiler-v2/tests/checking/positional_fields/decl_ok.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/positional_fields/decl_ok.exp
@@ -16,9 +16,9 @@ module 0x42::test {
         1: bool,
     }
     struct S3 {
-        0: #1,
+        0: T2,
         1: u8,
-        2: #0,
+        2: T1,
     }
     private fun bar(x: S2) {
         select test::S2.0<S2>(x);
diff --git a/third_party/move/move-compiler-v2/tests/checking/positional_fields/named_tuple_ability_decl_ok.exp b/third_party/move/move-compiler-v2/tests/checking/positional_fields/named_tuple_ability_decl_ok.exp
index 298a8f310f809..16d650a1c6cb3 100644
--- a/third_party/move/move-compiler-v2/tests/checking/positional_fields/named_tuple_ability_decl_ok.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/positional_fields/named_tuple_ability_decl_ok.exp
@@ -7,20 +7,20 @@ module 0x42::test {
         0: u8,
     }
     struct S2 {
-        0: #0,
+        0: T,
         1: u8,
     }
     struct S3 {
-        0: #0,
+        0: T,
         1: u8,
     }
     struct S4 {
         x: u8,
-        y: #0,
+        y: T,
     }
     struct S5 {
-        0: #0,
-        1: 0x42::test::S3<#0>,
+        0: T,
+        1: S3<T>,
     }
     struct S6 {
         dummy_field: bool,
diff --git a/third_party/move/move-compiler-v2/tests/checking/positional_fields/named_tuple_construct_ok.exp b/third_party/move/move-compiler-v2/tests/checking/positional_fields/named_tuple_construct_ok.exp
index 30bd1a8bb884a..f92c198d33961 100644
--- a/third_party/move/move-compiler-v2/tests/checking/positional_fields/named_tuple_construct_ok.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/positional_fields/named_tuple_construct_ok.exp
@@ -19,14 +19,14 @@ module 0x42::test {
         1: bool,
     }
     struct S3 {
-        0: #0,
+        0: T,
         1: u8,
     }
     struct S4 {
         dummy_field: bool,
     }
     struct S5 {
-        x: #0,
+        x: T,
         y: u8,
     }
     private fun S0_inhabited(): S0 {
diff --git a/third_party/move/move-compiler-v2/tests/checking/positional_fields/variant_ability_decl_ok.exp b/third_party/move/move-compiler-v2/tests/checking/positional_fields/variant_ability_decl_ok.exp
index 07b4274a25e4b..bb7c323f0c533 100644
--- a/third_party/move/move-compiler-v2/tests/checking/positional_fields/variant_ability_decl_ok.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/positional_fields/variant_ability_decl_ok.exp
@@ -2,7 +2,7 @@
 module 0x42::test {
     enum Bar {
         A {
-            0: #0,
+            0: T,
         }
         B {
             0: u8,
@@ -11,7 +11,7 @@ module 0x42::test {
     }
     enum Foo {
         A {
-            0: #0,
+            0: T,
         }
         B {
             0: u8,
diff --git a/third_party/move/move-compiler-v2/tests/checking/receiver/decl_errors.exp b/third_party/move/move-compiler-v2/tests/checking/receiver/decl_errors.exp
index 4f4835bda6621..4042ecbb69c1e 100644
--- a/third_party/move/move-compiler-v2/tests/checking/receiver/decl_errors.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/receiver/decl_errors.exp
@@ -39,8 +39,8 @@ module 0x42::n {
 module 0x42::m {
     use 0x42::n::{T}; // resolved as: 0x42::n
     struct G {
-        x: #0,
-        y: #1,
+        x: T,
+        y: R,
     }
     struct S {
         x: u64,
diff --git a/third_party/move/move-compiler-v2/tests/checking/receiver/generic_calls.exp b/third_party/move/move-compiler-v2/tests/checking/receiver/generic_calls.exp
index 2c10daec390de..51a0d9cb03185 100644
--- a/third_party/move/move-compiler-v2/tests/checking/receiver/generic_calls.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/receiver/generic_calls.exp
@@ -1,7 +1,7 @@
 // -- Model dump before bytecode pipeline
 module 0x42::m {
     struct S {
-        x: #0,
+        x: T,
     }
     private fun id<T>(self: S<T>): S<T> {
         self
diff --git a/third_party/move/move-compiler-v2/tests/checking/receiver/generic_calls_typed.exp b/third_party/move/move-compiler-v2/tests/checking/receiver/generic_calls_typed.exp
index 2c10daec390de..51a0d9cb03185 100644
--- a/third_party/move/move-compiler-v2/tests/checking/receiver/generic_calls_typed.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/receiver/generic_calls_typed.exp
@@ -1,7 +1,7 @@
 // -- Model dump before bytecode pipeline
 module 0x42::m {
     struct S {
-        x: #0,
+        x: T,
     }
     private fun id<T>(self: S<T>): S<T> {
         self
diff --git a/third_party/move/move-compiler-v2/tests/checking/specs/invariants_ok.exp b/third_party/move/move-compiler-v2/tests/checking/specs/invariants_ok.exp
index a7059c9346e06..00ce3b6b54444 100644
--- a/third_party/move/move-compiler-v2/tests/checking/specs/invariants_ok.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/specs/invariants_ok.exp
@@ -1,7 +1,7 @@
 // -- Model dump before bytecode pipeline
 module 0x42::M {
     struct R {
-        s: 0x42::M::S,
+        s: S,
     }
     spec {
       invariant M::less10(true, select M::S.x<0x42::M::S>(select M::R.s()));
diff --git a/third_party/move/move-compiler-v2/tests/checking/specs/move_function_in_spec_ok.exp b/third_party/move/move-compiler-v2/tests/checking/specs/move_function_in_spec_ok.exp
index 983ba541a7124..4ba45bf526215 100644
--- a/third_party/move/move-compiler-v2/tests/checking/specs/move_function_in_spec_ok.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/specs/move_function_in_spec_ok.exp
@@ -18,7 +18,7 @@ module 0x42::move_function_in_spec {
         }
     }
     public fun no_change(target: address,new_addr: address): bool
-        acquires 0x42::move_function_in_spec::TypeInfo(*)
+        acquires TypeInfo(*)
      {
         {
           let ty: &TypeInfo = BorrowGlobal(Immutable)<TypeInfo>(target);
diff --git a/third_party/move/move-compiler-v2/tests/checking/specs/schemas_ok.exp b/third_party/move/move-compiler-v2/tests/checking/specs/schemas_ok.exp
index 4c8215291a695..6f6473ed8e14c 100644
--- a/third_party/move/move-compiler-v2/tests/checking/specs/schemas_ok.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/specs/schemas_ok.exp
@@ -53,7 +53,7 @@ note: unused schema M::SchemaExp
 // -- Model dump before bytecode pipeline
 module 0x42::M {
     struct S {
-        x: #0,
+        x: X,
     }
     private fun add(x: u64): u64 {
         Add<u64>(x, 1)
diff --git a/third_party/move/move-compiler-v2/tests/checking/specs/structs_ok.exp b/third_party/move/move-compiler-v2/tests/checking/specs/structs_ok.exp
index 43214d6022fa7..ad89e14bcd352 100644
--- a/third_party/move/move-compiler-v2/tests/checking/specs/structs_ok.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/specs/structs_ok.exp
@@ -4,11 +4,11 @@ module 0x42::M {
         x: u64,
     }
     struct G {
-        x: #0,
+        x: T,
         y: bool,
     }
     struct R {
-        s: 0x42::M::S,
+        s: S,
     }
     struct S {
         x: u64,
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/borrow_field_chain.exp b/third_party/move/move-compiler-v2/tests/checking/typing/borrow_field_chain.exp
index 70d4ba0fd60ae..460c8c1455365 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/borrow_field_chain.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/borrow_field_chain.exp
@@ -1,10 +1,10 @@
 // -- Model dump before bytecode pipeline
 module 0x8675309::M {
     struct X1 {
-        x2: 0x8675309::M::X2,
+        x2: X2,
     }
     struct X2 {
-        x3: 0x8675309::M::X3,
+        x3: X3,
     }
     struct X3 {
         f: u64,
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/decl_unpack_references.exp b/third_party/move/move-compiler-v2/tests/checking/typing/decl_unpack_references.exp
index d6881be7a2b73..dac518a528414 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/decl_unpack_references.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/decl_unpack_references.exp
@@ -1,8 +1,8 @@
 // -- Model dump before bytecode pipeline
 module 0x8675309::M {
     struct R {
-        s1: 0x8675309::M::S,
-        s2: 0x8675309::M::S,
+        s1: S,
+        s2: S,
     }
     struct S {
         f: u64,
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/derefrence.exp b/third_party/move/move-compiler-v2/tests/checking/typing/derefrence.exp
index 8c7a6c1aceb7b..b31e5493c2008 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/derefrence.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/derefrence.exp
@@ -2,7 +2,7 @@
 module 0x8675309::M {
     struct S {
         f: u64,
-        x: 0x8675309::M::X,
+        x: X,
     }
     struct X {
         dummy_field: bool,
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/dummy_field.exp b/third_party/move/move-compiler-v2/tests/checking/typing/dummy_field.exp
index 56d305e825796..83cbf7d25cbf8 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/dummy_field.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/dummy_field.exp
@@ -7,7 +7,7 @@ module 0x42::test {
         dummy_field: bool,
     }
     public entry fun test(addr: address)
-        acquires 0x42::test::R(*)
+        acquires R(*)
      {
         {
           let test::R{ dummy_field: _dummy_field } = MoveFrom<R>(addr);
@@ -21,7 +21,7 @@ module 0x42::test {
         }
     }
     public entry fun test3(addr: address)
-        acquires 0x42::test::T(*)
+        acquires T(*)
      {
         {
           let test::T{ dummy_field: _ } = MoveFrom<T>(addr);
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/eq.exp b/third_party/move/move-compiler-v2/tests/checking/typing/eq.exp
index 0f6289490929e..4b6348bd2482d 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/eq.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/eq.exp
@@ -1,7 +1,7 @@
 // -- Model dump before bytecode pipeline
 module 0x8675309::M {
     struct G {
-        f: #0,
+        f: T,
     }
     struct R {
         f: u64,
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/exp_list.exp b/third_party/move/move-compiler-v2/tests/checking/typing/exp_list.exp
index 423fbbc8ff7f7..59bda651fd09c 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/exp_list.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/exp_list.exp
@@ -1,7 +1,7 @@
 // -- Model dump before bytecode pipeline
 module 0x8675309::M {
     struct R {
-        f: #0,
+        f: T,
     }
     struct S {
         dummy_field: bool,
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/global_builtins.exp b/third_party/move/move-compiler-v2/tests/checking/typing/global_builtins.exp
index 04b8d2231d938..4a0650b38a25c 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/global_builtins.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/global_builtins.exp
@@ -4,7 +4,7 @@ module 0x8675309::M {
         dummy_field: bool,
     }
     private fun t0(a: &signer)
-        acquires 0x8675309::M::R(*)
+        acquires R(*)
      {
         {
           let _: bool = exists<R>(0x0);
@@ -24,7 +24,7 @@ module 0x8675309::M {
         }
     }
     private fun t1(a: &signer)
-        acquires 0x8675309::M::R(*)
+        acquires R(*)
      {
         {
           let _: bool = exists<R>(0x0);
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/global_builtins_inferred.exp b/third_party/move/move-compiler-v2/tests/checking/typing/global_builtins_inferred.exp
index f8c0150058c56..8491eba0f62c7 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/global_builtins_inferred.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/global_builtins_inferred.exp
@@ -4,7 +4,7 @@ module 0x42::m {
         addr: address,
     }
     public fun foo(input: address): address
-        acquires 0x42::m::A(*)
+        acquires A(*)
      {
         {
           let a: A = MoveFrom<A>(input);
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/implicit_deref_borrow_field_chain.exp b/third_party/move/move-compiler-v2/tests/checking/typing/implicit_deref_borrow_field_chain.exp
index 5f505db3a6d37..5b32bfee85bac 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/implicit_deref_borrow_field_chain.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/implicit_deref_borrow_field_chain.exp
@@ -1,10 +1,10 @@
 // -- Model dump before bytecode pipeline
 module 0x8675309::M {
     struct X1 {
-        x2: 0x8675309::M::X2,
+        x2: X2,
     }
     struct X2 {
-        x3: 0x8675309::M::X3,
+        x3: X3,
     }
     struct X3 {
         f: u64,
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/lambda.exp b/third_party/move/move-compiler-v2/tests/checking/typing/lambda.exp
index c3d568872e95c..ebcdc1fcfcfdb 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/lambda.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/lambda.exp
@@ -48,3 +48,11 @@ error: tuple type `()` is not allowed as a type argument (type was inferred)
    │                                     ^
    │
    = required by instantiating type parameter `T` of function `foreach`
+
+error: function type `|u64|u64` is not allowed as a field type
+   ┌─ tests/checking/typing/lambda.move:81:12
+   │
+81 │         f: |u64|u64, // expected lambda not allowed
+   │            ^^^^^^^^
+   │
+   = required by declaration of field `f`
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/lambda2.exp b/third_party/move/move-compiler-v2/tests/checking/typing/lambda2.exp
new file mode 100644
index 0000000000000..3488e91208849
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/lambda2.exp
@@ -0,0 +1,25 @@
+
+Diagnostics:
+error: Only inline functions may have function-typed parameters, but non-inline function `M::fun_arg_lambda_not_allowed` has a function parameter:
+   ┌─ tests/checking/typing/lambda2.move:84:16
+   │
+84 │     public fun fun_arg_lambda_not_allowed(x: |u64|) {} // expected lambda not allowed
+   │                ^^^^^^^^^^^^^^^^^^^^^^^^^^ - Parameter `x` has function-valued type `|u64|`.
+
+warning: Unused parameter `x`. Consider removing or prefixing with an underscore: `_x`
+   ┌─ tests/checking/typing/lambda2.move:84:43
+   │
+84 │     public fun fun_arg_lambda_not_allowed(x: |u64|) {} // expected lambda not allowed
+   │                                           ^
+
+error: Functions may not return function-typed values, but function `M::macro_result_lambda_not_allowed` return type is `|u64|`:
+   ┌─ tests/checking/typing/lambda2.move:86:23
+   │
+86 │     public inline fun macro_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
+   │                       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+error: Functions may not return function-typed values, but function `M::fun_result_lambda_not_allowed` return type is `|u64|`:
+   ┌─ tests/checking/typing/lambda2.move:89:16
+   │
+89 │     public fun fun_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
+   │                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/lambda2.move b/third_party/move/move-compiler-v2/tests/checking/typing/lambda2.move
new file mode 100644
index 0000000000000..5d7cc52daf2ae
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/lambda2.move
@@ -0,0 +1,100 @@
+module 0x8675309::M {
+    // use 0x1::XVector;
+
+    // public inline fun foreach<T>(v: &vector<T>, action: |&T|) { // expected to be not implemented
+    //     let i = 0;
+    //     while (i < XVector::length(v)) {
+    //         action(XVector::borrow(v, i));
+    //         i = i + 1;
+    //     }
+    // }
+
+    // public inline fun reduce<R, T>(v: vector<T>, accu: R, reducer: |T, R|R): R {
+    //     while (!XVector::is_empty(&v)) {
+    //         accu = reducer(XVector::pop_back(&mut v), accu);
+    //     };
+    //     accu
+    // }
+
+
+    // public fun correct_foreach() {
+    //     let v = vector[1, 2, 3];
+    //     let sum = 0;
+    //     foreach(&v, |e| sum = sum + *e) // expected to be not implemented
+    // }
+
+    // public fun correct_reduce(): u64 {
+    //     let v = vector[1, 2, 3];
+    //     reduce(v, 0, |t, r| t + r)
+    // }
+
+    // public fun corrected_nested() {
+    //     let v = vector[vector[1,2], vector[3]];
+    //     let sum = 0;
+    //     foreach(&v, |e| sum = sum + reduce!(*e, 0, |t, r| t + r));
+    // }
+
+    // public inline fun wrong_local_call_arg_count<T>(v: &vector<T>, action: |&T|) {
+    //     let i = 0;
+    //     while (i < XVector::length(v)) {
+    //         action(XVector::borrow(v, i), i); // expected to have wrong argument count
+    //         i = i + 1;
+    //     }
+    // }
+
+    // public inline fun wrong_local_call_arg_type<T>(v: &vector<T>, action: |&T|) {
+    //     let i = 0;
+    //     while (i < XVector::length(v)) {
+    //         action(i); // expected to have wrong argument type
+    //         i = i + 1;
+    //     }
+    // }
+
+    // public inline fun wrong_local_call_result_type<T>(v: &vector<T>, action: |&T|) {
+    //     let i = 0;
+    //     while (i < XVector::length(v)) {
+    //         i = i + action(XVector::borrow(v, i)); // expected to have wrong result type
+    //     }
+    // }
+
+    // public fun wrong_local_call_no_fun(x: u64) {
+    //     x(1) // expected to be not a function
+    // }
+
+    // public fun wrong_lambda_inferred_type() {
+    //     let v = vector[1, 2, 3];
+    //     let sum = 0;
+    //     foreach(&v, |e| sum = sum + e) // expected to cannot infer type
+    // }
+
+    // public fun wrong_lambda_result_type() {
+    //     let v = vector[1, 2, 3];
+    //     let sum = 0;
+    //     foreach(&v, |e| { sum = sum + *e; *e }) // expected to have wrong result type of lambda
+    // }
+
+    public fun lambda_not_allowed() {
+        let _x = |i| i + 1; // expected lambda not allowed
+    }
+
+    // struct FieldFunNotAllowed {
+    //     f: |u64|u64, // expected lambda not allowed
+    // }
+
+    public fun fun_arg_lambda_not_allowed(x: |u64|) {} // expected lambda not allowed
+
+    public inline fun macro_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
+        abort (1)
+    }
+    public fun fun_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
+        abort (1)
+    }
+
+}
+
+// module 0x1::XVector {
+//     public fun length<T>(v: &vector<T>): u64 { abort(1) }
+//     public fun is_empty<T>(v: &vector<T>): bool { abort(1) }
+//     public fun borrow<T>(v: &vector<T>, i: u64): &T { abort(1) }
+//     public fun pop_back<T>(v: &mut vector<T>): T { abort(1) }
+// }
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/lambda_typed.exp b/third_party/move/move-compiler-v2/tests/checking/typing/lambda_typed.exp
index 351d607a7b2b7..7817686444d8f 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/lambda_typed.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/lambda_typed.exp
@@ -35,3 +35,11 @@ error: cannot pass `|&u64|u64` to a function which expects argument of type `|&u
    │
 73 │         foreach(&v, |e: &u64| { sum = sum + *e; *e }) // expected to have wrong result type of lambda
    │                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+error: function type `|u64|u64` is not allowed as a field type
+   ┌─ tests/checking/typing/lambda_typed.move:81:12
+   │
+81 │         f: |u64|u64, // expected lambda not allowed
+   │            ^^^^^^^^
+   │
+   = required by declaration of field `f`
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/main_arguments_various_caes.exp b/third_party/move/move-compiler-v2/tests/checking/typing/main_arguments_various_caes.exp
index ebd403606785e..95f64c5db9620 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/main_arguments_various_caes.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/main_arguments_various_caes.exp
@@ -1,7 +1,7 @@
 // -- Model dump before bytecode pipeline
 module 0x42::M {
     struct Cup {
-        f1: #0,
+        f1: T,
     }
     struct R {
         dummy_field: bool,
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/move_from_type_argument.exp b/third_party/move/move-compiler-v2/tests/checking/typing/move_from_type_argument.exp
index f8c0150058c56..8491eba0f62c7 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/move_from_type_argument.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/move_from_type_argument.exp
@@ -4,7 +4,7 @@ module 0x42::m {
         addr: address,
     }
     public fun foo(input: address): address
-        acquires 0x42::m::A(*)
+        acquires A(*)
      {
         {
           let a: A = MoveFrom<A>(input);
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/mutable_eq_and_neq.exp b/third_party/move/move-compiler-v2/tests/checking/typing/mutable_eq_and_neq.exp
index adc57ec46e5eb..1de8c0247dc61 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/mutable_eq_and_neq.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/mutable_eq_and_neq.exp
@@ -4,8 +4,8 @@ module 0x8675309::M {
         f: bool,
     }
     struct P {
-        b1: 0x8675309::M::B,
-        b2: 0x8675309::M::B,
+        b1: B,
+        b2: B,
     }
     struct S {
         f: u64,
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/neq.exp b/third_party/move/move-compiler-v2/tests/checking/typing/neq.exp
index f1976389c8105..17f2f53d747ed 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/neq.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/neq.exp
@@ -1,7 +1,7 @@
 // -- Model dump before bytecode pipeline
 module 0x8675309::M {
     struct G {
-        f: #0,
+        f: T,
     }
     struct R {
         f: u64,
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/nested_post_process.exp b/third_party/move/move-compiler-v2/tests/checking/typing/nested_post_process.exp
index f962be66efbfa..716b2a43d829e 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/nested_post_process.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/nested_post_process.exp
@@ -4,11 +4,11 @@ module 0x42::simple_map {
     use std::option;
     use std::vector;
     struct Element {
-        key: #0,
-        value: #1,
+        key: Key,
+        value: Value,
     }
     struct SimpleMap {
-        data: vector<0x42::simple_map::Element<#0, #1>>,
+        data: vector<Element<Key, Value>>,
     }
     public fun borrow<Key,Value>(map: &SimpleMap<Key, Value>,key: &Key): &Value {
         {
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/phantom_param_struct_decl.exp b/third_party/move/move-compiler-v2/tests/checking/typing/phantom_param_struct_decl.exp
index 9397cd73cadd2..d905413abacbd 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/phantom_param_struct_decl.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/phantom_param_struct_decl.exp
@@ -4,18 +4,18 @@ module 0x42::M1 {
         a: u64,
     }
     struct S2 {
-        a: 0x42::M1::S1<#0>,
-        b: vector<0x42::M1::S1<#0>>,
+        a: S1<T>,
+        b: vector<S1<T>>,
     }
     struct S3 {
-        a: #1,
-        b: #3,
+        a: T2,
+        b: T4,
     }
     struct S4 {
         a: u64,
     }
     struct S5 {
-        a: 0x42::M1::S4<#0>,
+        a: S4<T>,
     }
 } // end 0x42::M1
 
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_single_pack.exp b/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_single_pack.exp
index ab361d197f9af..97821d320fdd9 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_single_pack.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_single_pack.exp
@@ -1,8 +1,8 @@
 // -- Model dump before bytecode pipeline
 module 0x42::M {
     struct Box {
-        f1: #0,
-        f2: #0,
+        f1: T,
+        f2: T,
     }
     private fun t0() {
         {
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_single_unpack.exp b/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_single_unpack.exp
index ebfb56730b924..70569d59c43d5 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_single_unpack.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_single_unpack.exp
@@ -1,8 +1,8 @@
 // -- Model dump before bytecode pipeline
 module 0x8675309::M {
     struct Box {
-        f1: #0,
-        f2: #0,
+        f1: T,
+        f2: T,
     }
     private fun new<T>(): Box<T> {
         Abort(0)
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_single_unpack_assign.exp b/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_single_unpack_assign.exp
index 73269d41aa3c1..34faa633aadeb 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_single_unpack_assign.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_single_unpack_assign.exp
@@ -1,8 +1,8 @@
 // -- Model dump before bytecode pipeline
 module 0x8675309::M {
     struct Box {
-        f1: #0,
-        f2: #0,
+        f1: T,
+        f2: T,
     }
     private fun new<T>(): Box<T> {
         Abort(0)
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_threaded_pack.exp b/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_threaded_pack.exp
index cb79ee03e4703..5d4c04ccafe73 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_threaded_pack.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_threaded_pack.exp
@@ -1,7 +1,7 @@
 // -- Model dump before bytecode pipeline
 module 0x2::Container {
     struct T {
-        f: #0,
+        f: V,
     }
     public fun get<V>(_self: &T<V>): V {
         Abort(0)
@@ -16,8 +16,8 @@ module 0x2::Container {
 module 0x2::M {
     use 0x2::Container; // resolved as: 0x2::Container
     struct Box {
-        f1: #0,
-        f2: #0,
+        f1: T,
+        f2: T,
     }
     private fun t0(): Box<u64> {
         {
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/v1-examples/multi_pool_money_market_token.exp b/third_party/move/move-compiler-v2/tests/checking/typing/v1-examples/multi_pool_money_market_token.exp
index f4e0e789dbb91..ba2cb34b4ef5d 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/v1-examples/multi_pool_money_market_token.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/v1-examples/multi_pool_money_market_token.exp
@@ -19,7 +19,7 @@ warning: unused type parameter
 // -- Model dump before bytecode pipeline
 module 0x2::Token {
     struct Coin {
-        type: #0,
+        type: AssetType,
         value: u64,
     }
     public fun create<ATy>(type: ATy,value: u64): Coin<ATy> {
@@ -85,22 +85,22 @@ module 0x3::OneToOneMarket {
     use 0x2::Map; // resolved as: 0x2::Map
     use 0x2::Token; // resolved as: 0x2::Token
     struct BorrowRecord {
-        record: 0x2::Map::T<address, u64>,
+        record: Map::T<address, u64>,
     }
     struct DepositRecord {
-        record: 0x2::Map::T<address, u64>,
+        record: Map::T<address, u64>,
     }
     struct Pool {
-        coin: 0x2::Token::Coin<#0>,
+        coin: Token::Coin<AssetType>,
     }
     struct Price {
         price: u64,
     }
     public fun borrow<In,Out>(account: &signer,pool_owner: address,amount: u64): Token::Coin<Out>
-        acquires 0x3::OneToOneMarket::Price(*)
-        acquires 0x3::OneToOneMarket::Pool(*)
-        acquires 0x3::OneToOneMarket::DepositRecord(*)
-        acquires 0x3::OneToOneMarket::BorrowRecord(*)
+        acquires Price(*)
+        acquires Pool(*)
+        acquires DepositRecord(*)
+        acquires BorrowRecord(*)
      {
         if Le<u64>(amount, OneToOneMarket::max_borrow_amount<In, Out>(account, pool_owner)) {
           Tuple()
@@ -114,8 +114,8 @@ module 0x3::OneToOneMarket {
         }
     }
     public fun deposit<In,Out>(account: &signer,pool_owner: address,coin: Token::Coin<In>)
-        acquires 0x3::OneToOneMarket::Pool(*)
-        acquires 0x3::OneToOneMarket::DepositRecord(*)
+        acquires Pool(*)
+        acquires DepositRecord(*)
      {
         {
           let amount: u64 = Token::value<In>(Borrow(Immutable)(coin));
@@ -138,7 +138,7 @@ module 0x3::OneToOneMarket {
         }
     }
     private fun borrowed_amount<In,Out>(account: &signer,pool_owner: address): u64
-        acquires 0x3::OneToOneMarket::BorrowRecord(*)
+        acquires BorrowRecord(*)
      {
         {
           let sender: address = signer::address_of(account);
@@ -158,7 +158,7 @@ module 0x3::OneToOneMarket {
         }
     }
     private fun deposited_amount<In,Out>(account: &signer,pool_owner: address): u64
-        acquires 0x3::OneToOneMarket::DepositRecord(*)
+        acquires DepositRecord(*)
      {
         {
           let sender: address = signer::address_of(account);
@@ -178,10 +178,10 @@ module 0x3::OneToOneMarket {
         }
     }
     private fun max_borrow_amount<In,Out>(account: &signer,pool_owner: address): u64
-        acquires 0x3::OneToOneMarket::Price(*)
-        acquires 0x3::OneToOneMarket::Pool(*)
-        acquires 0x3::OneToOneMarket::DepositRecord(*)
-        acquires 0x3::OneToOneMarket::BorrowRecord(*)
+        acquires Price(*)
+        acquires Pool(*)
+        acquires DepositRecord(*)
+        acquires BorrowRecord(*)
      {
         {
           let input_deposited: u64 = OneToOneMarket::deposited_amount<In, Out>(account, pool_owner);
@@ -217,7 +217,7 @@ module 0x3::OneToOneMarket {
         MoveTo<Price<In, Out>>(account, pack OneToOneMarket::Price<In, Out>(price))
     }
     private fun update_borrow_record<In,Out>(account: &signer,pool_owner: address,amount: u64)
-        acquires 0x3::OneToOneMarket::BorrowRecord(*)
+        acquires BorrowRecord(*)
      {
         {
           let sender: address = signer::address_of(account);
@@ -242,7 +242,7 @@ module 0x3::OneToOneMarket {
         }
     }
     private fun update_deposit_record<In,Out>(account: &signer,pool_owner: address,amount: u64)
-        acquires 0x3::OneToOneMarket::DepositRecord(*)
+        acquires DepositRecord(*)
      {
         {
           let sender: address = signer::address_of(account);
@@ -274,7 +274,7 @@ module 0x70dd::ToddNickels {
         dummy_field: bool,
     }
     struct Wallet {
-        nickels: 0x2::Token::Coin<0x70dd::ToddNickels::T>,
+        nickels: Token::Coin<T>,
     }
     public fun init(account: &signer) {
         if Eq<address>(signer::address_of(account), 0x70dd) {
@@ -285,7 +285,7 @@ module 0x70dd::ToddNickels {
         MoveTo<Wallet>(account, pack ToddNickels::Wallet(Token::create<T>(pack ToddNickels::T(false), 0)))
     }
     public fun destroy(c: Token::Coin<T>)
-        acquires 0x70dd::ToddNickels::Wallet(*)
+        acquires Wallet(*)
      {
         Token::deposit<T>(Borrow(Mutable)(select ToddNickels::Wallet.nickels<&mut Wallet>(BorrowGlobal(Mutable)<Wallet>(0x70dd))), c)
     }
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/v1-examples/simple_money_market_token.exp b/third_party/move/move-compiler-v2/tests/checking/typing/v1-examples/simple_money_market_token.exp
index f28f09f7ddb92..249b9cfb67776 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/v1-examples/simple_money_market_token.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/v1-examples/simple_money_market_token.exp
@@ -1,7 +1,7 @@
 // -- Model dump before bytecode pipeline
 module 0x2::Token {
     struct Coin {
-        type: #0,
+        type: AssetType,
         value: u64,
     }
     public fun create<ATy>(type: ATy,value: u64): Coin<ATy> {
@@ -59,7 +59,7 @@ module 0x70dd::ToddNickels {
         dummy_field: bool,
     }
     struct Wallet {
-        nickels: 0x2::Token::Coin<0x70dd::ToddNickels::T>,
+        nickels: Token::Coin<T>,
     }
     public fun init(account: &signer) {
         if Eq<address>(signer::address_of(account), 0x70dd) {
@@ -70,7 +70,7 @@ module 0x70dd::ToddNickels {
         MoveTo<Wallet>(account, pack ToddNickels::Wallet(Token::create<T>(pack ToddNickels::T(false), 0)))
     }
     public fun destroy(c: Token::Coin<T>)
-        acquires 0x70dd::ToddNickels::Wallet(*)
+        acquires Wallet(*)
      {
         Token::deposit<T>(Borrow(Mutable)(select ToddNickels::Wallet.nickels<&mut Wallet>(BorrowGlobal(Mutable)<Wallet>(0x70dd))), c)
     }
@@ -93,16 +93,16 @@ module 0xb055::OneToOneMarket {
         record: u64,
     }
     struct Pool {
-        coin: 0x2::Token::Coin<#0>,
+        coin: Token::Coin<AssetType>,
     }
     struct Price {
         price: u64,
     }
     public fun borrow<In,Out>(account: &signer,amount: u64): Token::Coin<Out>
-        acquires 0xb055::OneToOneMarket::Price(*)
-        acquires 0xb055::OneToOneMarket::Pool(*)
-        acquires 0xb055::OneToOneMarket::DepositRecord(*)
-        acquires 0xb055::OneToOneMarket::BorrowRecord(*)
+        acquires Price(*)
+        acquires Pool(*)
+        acquires DepositRecord(*)
+        acquires BorrowRecord(*)
      {
         if Le<u64>(amount, OneToOneMarket::max_borrow_amount<In, Out>(account)) {
           Tuple()
@@ -116,8 +116,8 @@ module 0xb055::OneToOneMarket {
         }
     }
     public fun deposit<In,Out>(account: &signer,coin: Token::Coin<In>)
-        acquires 0xb055::OneToOneMarket::Pool(*)
-        acquires 0xb055::OneToOneMarket::DepositRecord(*)
+        acquires Pool(*)
+        acquires DepositRecord(*)
      {
         {
           let amount: u64 = Token::value<In>(Borrow(Immutable)(coin));
@@ -140,7 +140,7 @@ module 0xb055::OneToOneMarket {
         }
     }
     private fun borrowed_amount<In,Out>(account: &signer): u64
-        acquires 0xb055::OneToOneMarket::BorrowRecord(*)
+        acquires BorrowRecord(*)
      {
         {
           let sender: address = signer::address_of(account);
@@ -153,7 +153,7 @@ module 0xb055::OneToOneMarket {
         }
     }
     private fun deposited_amount<In,Out>(account: &signer): u64
-        acquires 0xb055::OneToOneMarket::DepositRecord(*)
+        acquires DepositRecord(*)
      {
         {
           let sender: address = signer::address_of(account);
@@ -166,10 +166,10 @@ module 0xb055::OneToOneMarket {
         }
     }
     private fun max_borrow_amount<In,Out>(account: &signer): u64
-        acquires 0xb055::OneToOneMarket::Price(*)
-        acquires 0xb055::OneToOneMarket::Pool(*)
-        acquires 0xb055::OneToOneMarket::DepositRecord(*)
-        acquires 0xb055::OneToOneMarket::BorrowRecord(*)
+        acquires Price(*)
+        acquires Pool(*)
+        acquires DepositRecord(*)
+        acquires BorrowRecord(*)
      {
         {
           let input_deposited: u64 = OneToOneMarket::deposited_amount<In, Out>(account);
@@ -213,7 +213,7 @@ module 0xb055::OneToOneMarket {
         }
     }
     private fun update_borrow_record<In,Out>(account: &signer,amount: u64)
-        acquires 0xb055::OneToOneMarket::BorrowRecord(*)
+        acquires BorrowRecord(*)
      {
         {
           let sender: address = signer::address_of(account);
@@ -229,7 +229,7 @@ module 0xb055::OneToOneMarket {
         }
     }
     private fun update_deposit_record<In,Out>(account: &signer,amount: u64)
-        acquires 0xb055::OneToOneMarket::DepositRecord(*)
+        acquires DepositRecord(*)
      {
         {
           let sender: address = signer::address_of(account);
diff --git a/third_party/move/move-compiler-v2/tests/checking/variants/variants_test_no_parenthesis_ok.exp b/third_party/move/move-compiler-v2/tests/checking/variants/variants_test_no_parenthesis_ok.exp
index 97f7cc058eebf..2c1d803d68857 100644
--- a/third_party/move/move-compiler-v2/tests/checking/variants/variants_test_no_parenthesis_ok.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/variants/variants_test_no_parenthesis_ok.exp
@@ -11,7 +11,7 @@ module 0x815::m {
     }
     enum Generic {
         Foo {
-            0: #0,
+            0: T,
         }
         Bar {
             0: u64,
diff --git a/third_party/move/move-compiler-v2/tests/checking/variants/variants_test_ok.exp b/third_party/move/move-compiler-v2/tests/checking/variants/variants_test_ok.exp
index 97f7cc058eebf..2c1d803d68857 100644
--- a/third_party/move/move-compiler-v2/tests/checking/variants/variants_test_ok.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/variants/variants_test_ok.exp
@@ -11,7 +11,7 @@ module 0x815::m {
     }
     enum Generic {
         Foo {
-            0: #0,
+            0: T,
         }
         Bar {
             0: u64,
diff --git a/third_party/move/move-compiler-v2/tests/cyclic-instantiation-checker/v1-tests/mutually_recursive_non_generic_type_ok.exp b/third_party/move/move-compiler-v2/tests/cyclic-instantiation-checker/v1-tests/mutually_recursive_non_generic_type_ok.exp
index ee9f393b3f473..2df7cde6d2f7c 100644
--- a/third_party/move/move-compiler-v2/tests/cyclic-instantiation-checker/v1-tests/mutually_recursive_non_generic_type_ok.exp
+++ b/third_party/move/move-compiler-v2/tests/cyclic-instantiation-checker/v1-tests/mutually_recursive_non_generic_type_ok.exp
@@ -1,7 +1,7 @@
 // -- Model dump before bytecode pipeline
 module 0x8675309::M {
     struct S {
-        f: #0,
+        f: T,
     }
     private fun f<T>() {
         M::g<S<T>>()
diff --git a/third_party/move/move-compiler-v2/tests/cyclic-instantiation-checker/v1-typing/infinite_instantiations_valid.exp b/third_party/move/move-compiler-v2/tests/cyclic-instantiation-checker/v1-typing/infinite_instantiations_valid.exp
index d986f83593d1a..0d98ba2f0f67f 100644
--- a/third_party/move/move-compiler-v2/tests/cyclic-instantiation-checker/v1-typing/infinite_instantiations_valid.exp
+++ b/third_party/move/move-compiler-v2/tests/cyclic-instantiation-checker/v1-typing/infinite_instantiations_valid.exp
@@ -1,7 +1,7 @@
 // -- Model dump before bytecode pipeline
 module 0x42::M {
     struct Box {
-        f: #0,
+        f: T,
     }
     public fun t0<T>() {
         M::t1<T>();
diff --git a/third_party/move/move-compiler-v2/tests/lambda-lifting/basic.exp b/third_party/move/move-compiler-v2/tests/lambda-lifting/basic.exp
index 560bf63d49ec9..cd8a217423ba1 100644
--- a/third_party/move/move-compiler-v2/tests/lambda-lifting/basic.exp
+++ b/third_party/move/move-compiler-v2/tests/lambda-lifting/basic.exp
@@ -18,6 +18,206 @@ module 0xcafe::m {
 } // end 0xcafe::m
 
 
+// -- Model dump after env processor unused checks:
+module 0xcafe::m {
+    private fun map(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun no_name_clash(x: u64,c: u64): u64 {
+        m::map(x, |y: u64| Add<u64>(y, c))
+    }
+    private fun with_name_clash1(x: u64,c: u64): u64 {
+        m::map(x, |x: u64| Add<u64>(x, c))
+    }
+    private fun with_name_clash2(x: u64,c: u64): u64 {
+        m::map(x, |x: u64| Add<u64>({
+          let x: u64 = Add<u64>(c, 1);
+          x
+        }, x))
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor type parameter check:
+module 0xcafe::m {
+    private fun map(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun no_name_clash(x: u64,c: u64): u64 {
+        m::map(x, |y: u64| Add<u64>(y, c))
+    }
+    private fun with_name_clash1(x: u64,c: u64): u64 {
+        m::map(x, |x: u64| Add<u64>(x, c))
+    }
+    private fun with_name_clash2(x: u64,c: u64): u64 {
+        m::map(x, |x: u64| Add<u64>({
+          let x: u64 = Add<u64>(c, 1);
+          x
+        }, x))
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor check recursive struct definition:
+module 0xcafe::m {
+    private fun map(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun no_name_clash(x: u64,c: u64): u64 {
+        m::map(x, |y: u64| Add<u64>(y, c))
+    }
+    private fun with_name_clash1(x: u64,c: u64): u64 {
+        m::map(x, |x: u64| Add<u64>(x, c))
+    }
+    private fun with_name_clash2(x: u64,c: u64): u64 {
+        m::map(x, |x: u64| Add<u64>({
+          let x: u64 = Add<u64>(c, 1);
+          x
+        }, x))
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor check cyclic type instantiation:
+module 0xcafe::m {
+    private fun map(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun no_name_clash(x: u64,c: u64): u64 {
+        m::map(x, |y: u64| Add<u64>(y, c))
+    }
+    private fun with_name_clash1(x: u64,c: u64): u64 {
+        m::map(x, |x: u64| Add<u64>(x, c))
+    }
+    private fun with_name_clash2(x: u64,c: u64): u64 {
+        m::map(x, |x: u64| Add<u64>({
+          let x: u64 = Add<u64>(c, 1);
+          x
+        }, x))
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor unused struct params check:
+module 0xcafe::m {
+    private fun map(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun no_name_clash(x: u64,c: u64): u64 {
+        m::map(x, |y: u64| Add<u64>(y, c))
+    }
+    private fun with_name_clash1(x: u64,c: u64): u64 {
+        m::map(x, |x: u64| Add<u64>(x, c))
+    }
+    private fun with_name_clash2(x: u64,c: u64): u64 {
+        m::map(x, |x: u64| Add<u64>({
+          let x: u64 = Add<u64>(c, 1);
+          x
+        }, x))
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor access and use check before inlining:
+module 0xcafe::m {
+    private fun map(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun no_name_clash(x: u64,c: u64): u64 {
+        m::map(x, |y: u64| Add<u64>(y, c))
+    }
+    private fun with_name_clash1(x: u64,c: u64): u64 {
+        m::map(x, |x: u64| Add<u64>(x, c))
+    }
+    private fun with_name_clash2(x: u64,c: u64): u64 {
+        m::map(x, |x: u64| Add<u64>({
+          let x: u64 = Add<u64>(c, 1);
+          x
+        }, x))
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor inlining:
+module 0xcafe::m {
+    private fun map(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun no_name_clash(x: u64,c: u64): u64 {
+        m::map(x, |y: u64| Add<u64>(y, c))
+    }
+    private fun with_name_clash1(x: u64,c: u64): u64 {
+        m::map(x, |x: u64| Add<u64>(x, c))
+    }
+    private fun with_name_clash2(x: u64,c: u64): u64 {
+        m::map(x, |x: u64| Add<u64>({
+          let x: u64 = Add<u64>(c, 1);
+          x
+        }, x))
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor access and use check after inlining:
+module 0xcafe::m {
+    private fun map(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun no_name_clash(x: u64,c: u64): u64 {
+        m::map(x, |y: u64| Add<u64>(y, c))
+    }
+    private fun with_name_clash1(x: u64,c: u64): u64 {
+        m::map(x, |x: u64| Add<u64>(x, c))
+    }
+    private fun with_name_clash2(x: u64,c: u64): u64 {
+        m::map(x, |x: u64| Add<u64>({
+          let x: u64 = Add<u64>(c, 1);
+          x
+        }, x))
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor acquires check:
+module 0xcafe::m {
+    private fun map(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun no_name_clash(x: u64,c: u64): u64 {
+        m::map(x, |y: u64| Add<u64>(y, c))
+    }
+    private fun with_name_clash1(x: u64,c: u64): u64 {
+        m::map(x, |x: u64| Add<u64>(x, c))
+    }
+    private fun with_name_clash2(x: u64,c: u64): u64 {
+        m::map(x, |x: u64| Add<u64>({
+          let x: u64 = Add<u64>(c, 1);
+          x
+        }, x))
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor simplifier:
+module 0xcafe::m {
+    private fun map(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun no_name_clash(x: u64,c: u64): u64 {
+        m::map(x, |y: u64| Add<u64>(y, c))
+    }
+    private fun with_name_clash1(x: u64,c: u64): u64 {
+        m::map(x, |x: u64| Add<u64>(x, c))
+    }
+    private fun with_name_clash2(x: u64,c: u64): u64 {
+        m::map(x, |x: u64| Add<u64>({
+          let x: u64 = Add<u64>(c, 1);
+          x
+        }, x))
+    }
+} // end 0xcafe::m
+
+
 // -- Model dump after env processor lambda-lifting:
 module 0xcafe::m {
     private fun map(x: u64,f: |u64|u64): u64 {
@@ -45,3 +245,61 @@ module 0xcafe::m {
         }, x)
     }
 } // end 0xcafe::m
+
+
+// -- Model dump after env processor specification checker:
+module 0xcafe::m {
+    private fun map(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun no_name_clash(x: u64,c: u64): u64 {
+        m::map(x, closure m::no_name_clash$lambda$1(c))
+    }
+    private fun with_name_clash1(x: u64,c: u64): u64 {
+        m::map(x, closure m::with_name_clash1$lambda$1(c))
+    }
+    private fun with_name_clash2(x: u64,c: u64): u64 {
+        m::map(x, closure m::with_name_clash2$lambda$1(c))
+    }
+    private fun no_name_clash$lambda$1(c: u64,y: u64): u64 {
+        Add<u64>(y, c)
+    }
+    private fun with_name_clash1$lambda$1(c: u64,x: u64): u64 {
+        Add<u64>(x, c)
+    }
+    private fun with_name_clash2$lambda$1(c: u64,x: u64): u64 {
+        Add<u64>({
+          let x: u64 = Add<u64>(c, 1);
+          x
+        }, x)
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor specification rewriter:
+module 0xcafe::m {
+    private fun map(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun no_name_clash(x: u64,c: u64): u64 {
+        m::map(x, closure m::no_name_clash$lambda$1(c))
+    }
+    private fun with_name_clash1(x: u64,c: u64): u64 {
+        m::map(x, closure m::with_name_clash1$lambda$1(c))
+    }
+    private fun with_name_clash2(x: u64,c: u64): u64 {
+        m::map(x, closure m::with_name_clash2$lambda$1(c))
+    }
+    private fun no_name_clash$lambda$1(c: u64,y: u64): u64 {
+        Add<u64>(y, c)
+    }
+    private fun with_name_clash1$lambda$1(c: u64,x: u64): u64 {
+        Add<u64>(x, c)
+    }
+    private fun with_name_clash2$lambda$1(c: u64,x: u64): u64 {
+        Add<u64>({
+          let x: u64 = Add<u64>(c, 1);
+          x
+        }, x)
+    }
+} // end 0xcafe::m
diff --git a/third_party/move/move-compiler-v2/tests/lambda-lifting/modify.exp b/third_party/move/move-compiler-v2/tests/lambda-lifting/modify.exp
index 9b00da4dfeba8..3664bd2e163bb 100644
--- a/third_party/move/move-compiler-v2/tests/lambda-lifting/modify.exp
+++ b/third_party/move/move-compiler-v2/tests/lambda-lifting/modify.exp
@@ -44,6 +44,463 @@ module 0xcafe::m {
 } // end 0xcafe::m
 
 
+// -- Model dump after env processor unused checks:
+module 0xcafe::m {
+    struct S {
+        x: u64,
+    }
+    private fun map(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun assigns_local(x: u64,c: u64): u64 {
+        {
+          let z: u64 = 1;
+          m::map(x, |y: u64| z: u64 = 2;
+          Add<u64>(y, c))
+        }
+    }
+    private fun assigns_param(x: u64,c: u64): u64 {
+        m::map(x, |y: u64| x: u64 = 2;
+        Add<u64>(y, c))
+    }
+    private fun borrows_local(x: u64): u64 {
+        {
+          let z: u64 = 1;
+          m::map(x, |y: u64| {
+            let r: &mut u64 = Borrow(Mutable)(z);
+            Add<u64>(y, Deref(r))
+          })
+        }
+    }
+    private fun borrows_param(x: u64,c: u64): u64 {
+        m::map(x, |y: u64| {
+          let r: &mut u64 = Borrow(Mutable)(c);
+          Add<u64>(y, Deref(r))
+        })
+    }
+    private fun immutable_borrow_ok(x: u64): u64 {
+        {
+          let z: u64 = 1;
+          m::map(x, |y: u64| {
+            let r: &u64 = Borrow(Immutable)(z);
+            Add<u64>(y, Deref(r))
+          })
+        }
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor type parameter check:
+module 0xcafe::m {
+    struct S {
+        x: u64,
+    }
+    private fun map(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun assigns_local(x: u64,c: u64): u64 {
+        {
+          let z: u64 = 1;
+          m::map(x, |y: u64| z: u64 = 2;
+          Add<u64>(y, c))
+        }
+    }
+    private fun assigns_param(x: u64,c: u64): u64 {
+        m::map(x, |y: u64| x: u64 = 2;
+        Add<u64>(y, c))
+    }
+    private fun borrows_local(x: u64): u64 {
+        {
+          let z: u64 = 1;
+          m::map(x, |y: u64| {
+            let r: &mut u64 = Borrow(Mutable)(z);
+            Add<u64>(y, Deref(r))
+          })
+        }
+    }
+    private fun borrows_param(x: u64,c: u64): u64 {
+        m::map(x, |y: u64| {
+          let r: &mut u64 = Borrow(Mutable)(c);
+          Add<u64>(y, Deref(r))
+        })
+    }
+    private fun immutable_borrow_ok(x: u64): u64 {
+        {
+          let z: u64 = 1;
+          m::map(x, |y: u64| {
+            let r: &u64 = Borrow(Immutable)(z);
+            Add<u64>(y, Deref(r))
+          })
+        }
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor check recursive struct definition:
+module 0xcafe::m {
+    struct S {
+        x: u64,
+    }
+    private fun map(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun assigns_local(x: u64,c: u64): u64 {
+        {
+          let z: u64 = 1;
+          m::map(x, |y: u64| z: u64 = 2;
+          Add<u64>(y, c))
+        }
+    }
+    private fun assigns_param(x: u64,c: u64): u64 {
+        m::map(x, |y: u64| x: u64 = 2;
+        Add<u64>(y, c))
+    }
+    private fun borrows_local(x: u64): u64 {
+        {
+          let z: u64 = 1;
+          m::map(x, |y: u64| {
+            let r: &mut u64 = Borrow(Mutable)(z);
+            Add<u64>(y, Deref(r))
+          })
+        }
+    }
+    private fun borrows_param(x: u64,c: u64): u64 {
+        m::map(x, |y: u64| {
+          let r: &mut u64 = Borrow(Mutable)(c);
+          Add<u64>(y, Deref(r))
+        })
+    }
+    private fun immutable_borrow_ok(x: u64): u64 {
+        {
+          let z: u64 = 1;
+          m::map(x, |y: u64| {
+            let r: &u64 = Borrow(Immutable)(z);
+            Add<u64>(y, Deref(r))
+          })
+        }
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor check cyclic type instantiation:
+module 0xcafe::m {
+    struct S {
+        x: u64,
+    }
+    private fun map(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun assigns_local(x: u64,c: u64): u64 {
+        {
+          let z: u64 = 1;
+          m::map(x, |y: u64| z: u64 = 2;
+          Add<u64>(y, c))
+        }
+    }
+    private fun assigns_param(x: u64,c: u64): u64 {
+        m::map(x, |y: u64| x: u64 = 2;
+        Add<u64>(y, c))
+    }
+    private fun borrows_local(x: u64): u64 {
+        {
+          let z: u64 = 1;
+          m::map(x, |y: u64| {
+            let r: &mut u64 = Borrow(Mutable)(z);
+            Add<u64>(y, Deref(r))
+          })
+        }
+    }
+    private fun borrows_param(x: u64,c: u64): u64 {
+        m::map(x, |y: u64| {
+          let r: &mut u64 = Borrow(Mutable)(c);
+          Add<u64>(y, Deref(r))
+        })
+    }
+    private fun immutable_borrow_ok(x: u64): u64 {
+        {
+          let z: u64 = 1;
+          m::map(x, |y: u64| {
+            let r: &u64 = Borrow(Immutable)(z);
+            Add<u64>(y, Deref(r))
+          })
+        }
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor unused struct params check:
+module 0xcafe::m {
+    struct S {
+        x: u64,
+    }
+    private fun map(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun assigns_local(x: u64,c: u64): u64 {
+        {
+          let z: u64 = 1;
+          m::map(x, |y: u64| z: u64 = 2;
+          Add<u64>(y, c))
+        }
+    }
+    private fun assigns_param(x: u64,c: u64): u64 {
+        m::map(x, |y: u64| x: u64 = 2;
+        Add<u64>(y, c))
+    }
+    private fun borrows_local(x: u64): u64 {
+        {
+          let z: u64 = 1;
+          m::map(x, |y: u64| {
+            let r: &mut u64 = Borrow(Mutable)(z);
+            Add<u64>(y, Deref(r))
+          })
+        }
+    }
+    private fun borrows_param(x: u64,c: u64): u64 {
+        m::map(x, |y: u64| {
+          let r: &mut u64 = Borrow(Mutable)(c);
+          Add<u64>(y, Deref(r))
+        })
+    }
+    private fun immutable_borrow_ok(x: u64): u64 {
+        {
+          let z: u64 = 1;
+          m::map(x, |y: u64| {
+            let r: &u64 = Borrow(Immutable)(z);
+            Add<u64>(y, Deref(r))
+          })
+        }
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor access and use check before inlining:
+module 0xcafe::m {
+    struct S {
+        x: u64,
+    }
+    private fun map(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun assigns_local(x: u64,c: u64): u64 {
+        {
+          let z: u64 = 1;
+          m::map(x, |y: u64| z: u64 = 2;
+          Add<u64>(y, c))
+        }
+    }
+    private fun assigns_param(x: u64,c: u64): u64 {
+        m::map(x, |y: u64| x: u64 = 2;
+        Add<u64>(y, c))
+    }
+    private fun borrows_local(x: u64): u64 {
+        {
+          let z: u64 = 1;
+          m::map(x, |y: u64| {
+            let r: &mut u64 = Borrow(Mutable)(z);
+            Add<u64>(y, Deref(r))
+          })
+        }
+    }
+    private fun borrows_param(x: u64,c: u64): u64 {
+        m::map(x, |y: u64| {
+          let r: &mut u64 = Borrow(Mutable)(c);
+          Add<u64>(y, Deref(r))
+        })
+    }
+    private fun immutable_borrow_ok(x: u64): u64 {
+        {
+          let z: u64 = 1;
+          m::map(x, |y: u64| {
+            let r: &u64 = Borrow(Immutable)(z);
+            Add<u64>(y, Deref(r))
+          })
+        }
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor inlining:
+module 0xcafe::m {
+    struct S {
+        x: u64,
+    }
+    private fun map(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun assigns_local(x: u64,c: u64): u64 {
+        {
+          let z: u64 = 1;
+          m::map(x, |y: u64| z: u64 = 2;
+          Add<u64>(y, c))
+        }
+    }
+    private fun assigns_param(x: u64,c: u64): u64 {
+        m::map(x, |y: u64| x: u64 = 2;
+        Add<u64>(y, c))
+    }
+    private fun borrows_local(x: u64): u64 {
+        {
+          let z: u64 = 1;
+          m::map(x, |y: u64| {
+            let r: &mut u64 = Borrow(Mutable)(z);
+            Add<u64>(y, Deref(r))
+          })
+        }
+    }
+    private fun borrows_param(x: u64,c: u64): u64 {
+        m::map(x, |y: u64| {
+          let r: &mut u64 = Borrow(Mutable)(c);
+          Add<u64>(y, Deref(r))
+        })
+    }
+    private fun immutable_borrow_ok(x: u64): u64 {
+        {
+          let z: u64 = 1;
+          m::map(x, |y: u64| {
+            let r: &u64 = Borrow(Immutable)(z);
+            Add<u64>(y, Deref(r))
+          })
+        }
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor access and use check after inlining:
+module 0xcafe::m {
+    struct S {
+        x: u64,
+    }
+    private fun map(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun assigns_local(x: u64,c: u64): u64 {
+        {
+          let z: u64 = 1;
+          m::map(x, |y: u64| z: u64 = 2;
+          Add<u64>(y, c))
+        }
+    }
+    private fun assigns_param(x: u64,c: u64): u64 {
+        m::map(x, |y: u64| x: u64 = 2;
+        Add<u64>(y, c))
+    }
+    private fun borrows_local(x: u64): u64 {
+        {
+          let z: u64 = 1;
+          m::map(x, |y: u64| {
+            let r: &mut u64 = Borrow(Mutable)(z);
+            Add<u64>(y, Deref(r))
+          })
+        }
+    }
+    private fun borrows_param(x: u64,c: u64): u64 {
+        m::map(x, |y: u64| {
+          let r: &mut u64 = Borrow(Mutable)(c);
+          Add<u64>(y, Deref(r))
+        })
+    }
+    private fun immutable_borrow_ok(x: u64): u64 {
+        {
+          let z: u64 = 1;
+          m::map(x, |y: u64| {
+            let r: &u64 = Borrow(Immutable)(z);
+            Add<u64>(y, Deref(r))
+          })
+        }
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor acquires check:
+module 0xcafe::m {
+    struct S {
+        x: u64,
+    }
+    private fun map(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun assigns_local(x: u64,c: u64): u64 {
+        {
+          let z: u64 = 1;
+          m::map(x, |y: u64| z: u64 = 2;
+          Add<u64>(y, c))
+        }
+    }
+    private fun assigns_param(x: u64,c: u64): u64 {
+        m::map(x, |y: u64| x: u64 = 2;
+        Add<u64>(y, c))
+    }
+    private fun borrows_local(x: u64): u64 {
+        {
+          let z: u64 = 1;
+          m::map(x, |y: u64| {
+            let r: &mut u64 = Borrow(Mutable)(z);
+            Add<u64>(y, Deref(r))
+          })
+        }
+    }
+    private fun borrows_param(x: u64,c: u64): u64 {
+        m::map(x, |y: u64| {
+          let r: &mut u64 = Borrow(Mutable)(c);
+          Add<u64>(y, Deref(r))
+        })
+    }
+    private fun immutable_borrow_ok(x: u64): u64 {
+        {
+          let z: u64 = 1;
+          m::map(x, |y: u64| {
+            let r: &u64 = Borrow(Immutable)(z);
+            Add<u64>(y, Deref(r))
+          })
+        }
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor simplifier:
+module 0xcafe::m {
+    struct S {
+        x: u64,
+    }
+    private fun map(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun assigns_local(x: u64,c: u64): u64 {
+        {
+          let z: u64 = 1;
+          m::map(x, |y: u64| z: u64 = 2;
+          Add<u64>(y, c))
+        }
+    }
+    private fun assigns_param(x: u64,c: u64): u64 {
+        m::map(x, |y: u64| x: u64 = 2;
+        Add<u64>(y, c))
+    }
+    private fun borrows_local(x: u64): u64 {
+        {
+          let z: u64 = 1;
+          m::map(x, |y: u64| {
+            let r: &mut u64 = Borrow(Mutable)(z);
+            Add<u64>(y, Deref(r))
+          })
+        }
+    }
+    private fun borrows_param(x: u64,c: u64): u64 {
+        m::map(x, |y: u64| {
+          let r: &mut u64 = Borrow(Mutable)(c);
+          Add<u64>(y, Deref(r))
+        })
+    }
+    private fun immutable_borrow_ok(x: u64): u64 {
+        m::map(x, |y: u64| {
+          let r: &u64 = Borrow(Immutable)(1);
+          Add<u64>(y, Deref(r))
+        })
+    }
+} // end 0xcafe::m
+
+
 
 Diagnostics:
 error: captured variable `x` cannot be modified inside of a lambda
diff --git a/third_party/move/move-compiler-v2/tests/lambda-lifting/nested.exp b/third_party/move/move-compiler-v2/tests/lambda-lifting/nested.exp
index 9ddfd3b736119..6da5f81560227 100644
--- a/third_party/move/move-compiler-v2/tests/lambda-lifting/nested.exp
+++ b/third_party/move/move-compiler-v2/tests/lambda-lifting/nested.exp
@@ -12,6 +12,146 @@ module 0xcafe::m {
 } // end 0xcafe::m
 
 
+// -- Model dump after env processor unused checks:
+module 0xcafe::m {
+    private fun map1(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun map2(x: u8,f: |u8|u8): u8 {
+        (f)(x)
+    }
+    private fun nested(x: u64,c: u64): u64 {
+        m::map1(x, |y: u64| Cast<u64>(m::map2(Cast<u8>(Sub<u64>(y, c)), |y: u8| Add<u8>(y, Cast<u8>(c)))))
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor type parameter check:
+module 0xcafe::m {
+    private fun map1(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun map2(x: u8,f: |u8|u8): u8 {
+        (f)(x)
+    }
+    private fun nested(x: u64,c: u64): u64 {
+        m::map1(x, |y: u64| Cast<u64>(m::map2(Cast<u8>(Sub<u64>(y, c)), |y: u8| Add<u8>(y, Cast<u8>(c)))))
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor check recursive struct definition:
+module 0xcafe::m {
+    private fun map1(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun map2(x: u8,f: |u8|u8): u8 {
+        (f)(x)
+    }
+    private fun nested(x: u64,c: u64): u64 {
+        m::map1(x, |y: u64| Cast<u64>(m::map2(Cast<u8>(Sub<u64>(y, c)), |y: u8| Add<u8>(y, Cast<u8>(c)))))
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor check cyclic type instantiation:
+module 0xcafe::m {
+    private fun map1(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun map2(x: u8,f: |u8|u8): u8 {
+        (f)(x)
+    }
+    private fun nested(x: u64,c: u64): u64 {
+        m::map1(x, |y: u64| Cast<u64>(m::map2(Cast<u8>(Sub<u64>(y, c)), |y: u8| Add<u8>(y, Cast<u8>(c)))))
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor unused struct params check:
+module 0xcafe::m {
+    private fun map1(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun map2(x: u8,f: |u8|u8): u8 {
+        (f)(x)
+    }
+    private fun nested(x: u64,c: u64): u64 {
+        m::map1(x, |y: u64| Cast<u64>(m::map2(Cast<u8>(Sub<u64>(y, c)), |y: u8| Add<u8>(y, Cast<u8>(c)))))
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor access and use check before inlining:
+module 0xcafe::m {
+    private fun map1(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun map2(x: u8,f: |u8|u8): u8 {
+        (f)(x)
+    }
+    private fun nested(x: u64,c: u64): u64 {
+        m::map1(x, |y: u64| Cast<u64>(m::map2(Cast<u8>(Sub<u64>(y, c)), |y: u8| Add<u8>(y, Cast<u8>(c)))))
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor inlining:
+module 0xcafe::m {
+    private fun map1(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun map2(x: u8,f: |u8|u8): u8 {
+        (f)(x)
+    }
+    private fun nested(x: u64,c: u64): u64 {
+        m::map1(x, |y: u64| Cast<u64>(m::map2(Cast<u8>(Sub<u64>(y, c)), |y: u8| Add<u8>(y, Cast<u8>(c)))))
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor access and use check after inlining:
+module 0xcafe::m {
+    private fun map1(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun map2(x: u8,f: |u8|u8): u8 {
+        (f)(x)
+    }
+    private fun nested(x: u64,c: u64): u64 {
+        m::map1(x, |y: u64| Cast<u64>(m::map2(Cast<u8>(Sub<u64>(y, c)), |y: u8| Add<u8>(y, Cast<u8>(c)))))
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor acquires check:
+module 0xcafe::m {
+    private fun map1(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun map2(x: u8,f: |u8|u8): u8 {
+        (f)(x)
+    }
+    private fun nested(x: u64,c: u64): u64 {
+        m::map1(x, |y: u64| Cast<u64>(m::map2(Cast<u8>(Sub<u64>(y, c)), |y: u8| Add<u8>(y, Cast<u8>(c)))))
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor simplifier:
+module 0xcafe::m {
+    private fun map1(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun map2(x: u8,f: |u8|u8): u8 {
+        (f)(x)
+    }
+    private fun nested(x: u64,c: u64): u64 {
+        m::map1(x, |y: u64| Cast<u64>(m::map2(Cast<u8>(Sub<u64>(y, c)), |y: u8| Add<u8>(y, Cast<u8>(c)))))
+    }
+} // end 0xcafe::m
+
+
 // -- Model dump after env processor lambda-lifting:
 module 0xcafe::m {
     private fun map1(x: u64,f: |u64|u64): u64 {
@@ -30,3 +170,43 @@ module 0xcafe::m {
         Cast<u64>(m::map2(Cast<u8>(Sub<u64>(y, c)), closure m::nested$lambda$1(c)))
     }
 } // end 0xcafe::m
+
+
+// -- Model dump after env processor specification checker:
+module 0xcafe::m {
+    private fun map1(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun map2(x: u8,f: |u8|u8): u8 {
+        (f)(x)
+    }
+    private fun nested(x: u64,c: u64): u64 {
+        m::map1(x, closure m::nested$lambda$2(c))
+    }
+    private fun nested$lambda$1(c: u64,y: u8): u8 {
+        Add<u8>(y, Cast<u8>(c))
+    }
+    private fun nested$lambda$2(c: u64,y: u64): u64 {
+        Cast<u64>(m::map2(Cast<u8>(Sub<u64>(y, c)), closure m::nested$lambda$1(c)))
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor specification rewriter:
+module 0xcafe::m {
+    private fun map1(x: u64,f: |u64|u64): u64 {
+        (f)(x)
+    }
+    private fun map2(x: u8,f: |u8|u8): u8 {
+        (f)(x)
+    }
+    private fun nested(x: u64,c: u64): u64 {
+        m::map1(x, closure m::nested$lambda$2(c))
+    }
+    private fun nested$lambda$1(c: u64,y: u8): u8 {
+        Add<u8>(y, Cast<u8>(c))
+    }
+    private fun nested$lambda$2(c: u64,y: u64): u64 {
+        Cast<u64>(m::map2(Cast<u8>(Sub<u64>(y, c)), closure m::nested$lambda$1(c)))
+    }
+} // end 0xcafe::m
diff --git a/third_party/move/move-compiler-v2/tests/lambda-lifting/pattern.exp b/third_party/move/move-compiler-v2/tests/lambda-lifting/pattern.exp
index 0b9d7af753a8c..8aa1ebc4aa0a9 100644
--- a/third_party/move/move-compiler-v2/tests/lambda-lifting/pattern.exp
+++ b/third_party/move/move-compiler-v2/tests/lambda-lifting/pattern.exp
@@ -1,7 +1,177 @@
 // -- Model dump before env processor pipeline:
 module 0xcafe::m {
     struct S {
-        x: #0,
+        x: T,
+    }
+    private fun consume<T>(s: S<T>,x: T,f: |(S<T>, T)|T): T {
+        (f)(s, x)
+    }
+    private fun pattern(s: S<u64>,x: u64): u64 {
+        m::consume<u64>(s, x, |(m::S<u64>{ x }, _y: u64): (S<u64>, u64)| {
+          let y: u64 = x;
+          Add<u64>(x, y)
+        })
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor unused checks:
+module 0xcafe::m {
+    struct S {
+        x: T,
+    }
+    private fun consume<T>(s: S<T>,x: T,f: |(S<T>, T)|T): T {
+        (f)(s, x)
+    }
+    private fun pattern(s: S<u64>,x: u64): u64 {
+        m::consume<u64>(s, x, |(m::S<u64>{ x }, _y: u64): (S<u64>, u64)| {
+          let y: u64 = x;
+          Add<u64>(x, y)
+        })
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor type parameter check:
+module 0xcafe::m {
+    struct S {
+        x: T,
+    }
+    private fun consume<T>(s: S<T>,x: T,f: |(S<T>, T)|T): T {
+        (f)(s, x)
+    }
+    private fun pattern(s: S<u64>,x: u64): u64 {
+        m::consume<u64>(s, x, |(m::S<u64>{ x }, _y: u64): (S<u64>, u64)| {
+          let y: u64 = x;
+          Add<u64>(x, y)
+        })
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor check recursive struct definition:
+module 0xcafe::m {
+    struct S {
+        x: T,
+    }
+    private fun consume<T>(s: S<T>,x: T,f: |(S<T>, T)|T): T {
+        (f)(s, x)
+    }
+    private fun pattern(s: S<u64>,x: u64): u64 {
+        m::consume<u64>(s, x, |(m::S<u64>{ x }, _y: u64): (S<u64>, u64)| {
+          let y: u64 = x;
+          Add<u64>(x, y)
+        })
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor check cyclic type instantiation:
+module 0xcafe::m {
+    struct S {
+        x: T,
+    }
+    private fun consume<T>(s: S<T>,x: T,f: |(S<T>, T)|T): T {
+        (f)(s, x)
+    }
+    private fun pattern(s: S<u64>,x: u64): u64 {
+        m::consume<u64>(s, x, |(m::S<u64>{ x }, _y: u64): (S<u64>, u64)| {
+          let y: u64 = x;
+          Add<u64>(x, y)
+        })
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor unused struct params check:
+module 0xcafe::m {
+    struct S {
+        x: T,
+    }
+    private fun consume<T>(s: S<T>,x: T,f: |(S<T>, T)|T): T {
+        (f)(s, x)
+    }
+    private fun pattern(s: S<u64>,x: u64): u64 {
+        m::consume<u64>(s, x, |(m::S<u64>{ x }, _y: u64): (S<u64>, u64)| {
+          let y: u64 = x;
+          Add<u64>(x, y)
+        })
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor access and use check before inlining:
+module 0xcafe::m {
+    struct S {
+        x: T,
+    }
+    private fun consume<T>(s: S<T>,x: T,f: |(S<T>, T)|T): T {
+        (f)(s, x)
+    }
+    private fun pattern(s: S<u64>,x: u64): u64 {
+        m::consume<u64>(s, x, |(m::S<u64>{ x }, _y: u64): (S<u64>, u64)| {
+          let y: u64 = x;
+          Add<u64>(x, y)
+        })
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor inlining:
+module 0xcafe::m {
+    struct S {
+        x: T,
+    }
+    private fun consume<T>(s: S<T>,x: T,f: |(S<T>, T)|T): T {
+        (f)(s, x)
+    }
+    private fun pattern(s: S<u64>,x: u64): u64 {
+        m::consume<u64>(s, x, |(m::S<u64>{ x }, _y: u64): (S<u64>, u64)| {
+          let y: u64 = x;
+          Add<u64>(x, y)
+        })
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor access and use check after inlining:
+module 0xcafe::m {
+    struct S {
+        x: T,
+    }
+    private fun consume<T>(s: S<T>,x: T,f: |(S<T>, T)|T): T {
+        (f)(s, x)
+    }
+    private fun pattern(s: S<u64>,x: u64): u64 {
+        m::consume<u64>(s, x, |(m::S<u64>{ x }, _y: u64): (S<u64>, u64)| {
+          let y: u64 = x;
+          Add<u64>(x, y)
+        })
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor acquires check:
+module 0xcafe::m {
+    struct S {
+        x: T,
+    }
+    private fun consume<T>(s: S<T>,x: T,f: |(S<T>, T)|T): T {
+        (f)(s, x)
+    }
+    private fun pattern(s: S<u64>,x: u64): u64 {
+        m::consume<u64>(s, x, |(m::S<u64>{ x }, _y: u64): (S<u64>, u64)| {
+          let y: u64 = x;
+          Add<u64>(x, y)
+        })
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor simplifier:
+module 0xcafe::m {
+    struct S {
+        x: T,
     }
     private fun consume<T>(s: S<T>,x: T,f: |(S<T>, T)|T): T {
         (f)(s, x)
@@ -18,7 +188,53 @@ module 0xcafe::m {
 // -- Model dump after env processor lambda-lifting:
 module 0xcafe::m {
     struct S {
-        x: #0,
+        x: T,
+    }
+    private fun consume<T>(s: S<T>,x: T,f: |(S<T>, T)|T): T {
+        (f)(s, x)
+    }
+    private fun pattern(s: S<u64>,x: u64): u64 {
+        m::consume<u64>(s, x, closure m::pattern$lambda$1())
+    }
+    private fun pattern$lambda$1(param$0: S<u64>,_y: u64): u64 {
+        {
+          let m::S<u64>{ x } = param$0;
+          {
+            let y: u64 = x;
+            Add<u64>(x, y)
+          }
+        }
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor specification checker:
+module 0xcafe::m {
+    struct S {
+        x: T,
+    }
+    private fun consume<T>(s: S<T>,x: T,f: |(S<T>, T)|T): T {
+        (f)(s, x)
+    }
+    private fun pattern(s: S<u64>,x: u64): u64 {
+        m::consume<u64>(s, x, closure m::pattern$lambda$1())
+    }
+    private fun pattern$lambda$1(param$0: S<u64>,_y: u64): u64 {
+        {
+          let m::S<u64>{ x } = param$0;
+          {
+            let y: u64 = x;
+            Add<u64>(x, y)
+          }
+        }
+    }
+} // end 0xcafe::m
+
+
+// -- Model dump after env processor specification rewriter:
+module 0xcafe::m {
+    struct S {
+        x: T,
     }
     private fun consume<T>(s: S<T>,x: T,f: |(S<T>, T)|T): T {
         (f)(s, x)
diff --git a/third_party/move/move-compiler-v2/tests/more-v1/parser/spec_parsing_fun_type_fail.exp b/third_party/move/move-compiler-v2/tests/more-v1/parser/spec_parsing_fun_type_fail.exp
index f5a92a3579cfe..e023799381a93 100644
--- a/third_party/move/move-compiler-v2/tests/more-v1/parser/spec_parsing_fun_type_fail.exp
+++ b/third_party/move/move-compiler-v2/tests/more-v1/parser/spec_parsing_fun_type_fail.exp
@@ -4,7 +4,7 @@ error: Only inline functions may have function-typed parameters, but non-inline
   ┌─ tests/more-v1/parser/spec_parsing_fun_type_fail.move:2:9
   │
 2 │     fun fun_type_in_prog(p: |u64|u64) {
-  │         ^^^^^^^^^^^^^^^^ - Parameter `p` has a function type.
+  │         ^^^^^^^^^^^^^^^^ - Parameter `p` has function-valued type `|u64|u64`.
 
 warning: Unused parameter `p`. Consider removing or prefixing with an underscore: `_p`
   ┌─ tests/more-v1/parser/spec_parsing_fun_type_fail.move:2:26
diff --git a/third_party/move/move-compiler-v2/tests/op-equal/valid0.exp b/third_party/move/move-compiler-v2/tests/op-equal/valid0.exp
index 3d819831e8a3e..398c192cb062b 100644
--- a/third_party/move/move-compiler-v2/tests/op-equal/valid0.exp
+++ b/third_party/move/move-compiler-v2/tests/op-equal/valid0.exp
@@ -4,7 +4,7 @@ module 0x42::test {
         0: u256,
     }
     struct Wrapper {
-        0: #0,
+        0: T,
     }
     private fun add1_new(x: u256): u256 {
         x: u256 = Add<u256>(x, 1);
@@ -40,7 +40,7 @@ module 0x42::test {
         }
     }
     private fun inc_coin_at(addr: address)
-        acquires 0x42::test::Coin(*)
+        acquires Coin(*)
      {
         {
           let coin: &mut Coin = BorrowGlobal(Mutable)<Coin>(addr);
diff --git a/third_party/move/move-compiler-v2/tests/op-equal/valid1.exp b/third_party/move/move-compiler-v2/tests/op-equal/valid1.exp
index 1369ebdbc51c5..a4c1156bf0a66 100644
--- a/third_party/move/move-compiler-v2/tests/op-equal/valid1.exp
+++ b/third_party/move/move-compiler-v2/tests/op-equal/valid1.exp
@@ -4,7 +4,7 @@ module 0x42::test {
         0: u256,
     }
     struct Wrapper {
-        0: #0,
+        0: T,
     }
     private fun bitand_vec_coin_new(x: vector<Coin>,index: u64) {
         {
@@ -49,7 +49,7 @@ module 0x42::test {
         Tuple()
     }
     private fun shr_coin_at(addr: address)
-        acquires 0x42::test::Coin(*)
+        acquires Coin(*)
      {
         {
           let coin: &mut Coin = BorrowGlobal(Mutable)<Coin>(addr);
diff --git a/third_party/move/move-compiler-v2/tests/simplifier-elimination/assign_unpack_references.exp b/third_party/move/move-compiler-v2/tests/simplifier-elimination/assign_unpack_references.exp
index ecbeecf5320d2..b14d08d9ae98f 100644
--- a/third_party/move/move-compiler-v2/tests/simplifier-elimination/assign_unpack_references.exp
+++ b/third_party/move/move-compiler-v2/tests/simplifier-elimination/assign_unpack_references.exp
@@ -1,8 +1,8 @@
 // -- Model dump before bytecode pipeline
 module 0x8675309::M {
     struct R {
-        s1: 0x8675309::M::S,
-        s2: 0x8675309::M::S,
+        s1: S,
+        s2: S,
     }
     struct S {
         f: u64,
diff --git a/third_party/move/move-compiler-v2/tests/testsuite.rs b/third_party/move/move-compiler-v2/tests/testsuite.rs
index ba34279b86a38..0bb94585d77ba 100644
--- a/third_party/move/move-compiler-v2/tests/testsuite.rs
+++ b/third_party/move/move-compiler-v2/tests/testsuite.rs
@@ -169,15 +169,10 @@ const TEST_CONFIGS: Lazy<BTreeMap<&str, TestConfig>> = Lazy::new(|| {
             exp_suffix: None,
             options: opts
                 .clone()
-                // Need to turn off usage checks because they complain about
-                // lambda parameters outside of inline functions. Other checks
-                // also turned off for now since they mess up baseline.
-                .set_experiment(Experiment::CHECKS, false)
-                .set_experiment(Experiment::OPTIMIZE, false)
-                .set_experiment(Experiment::OPTIMIZE_WAITING_FOR_COMPARE_TESTS, false)
-                .set_experiment(Experiment::INLINING, false)
-                .set_experiment(Experiment::RECURSIVE_TYPE_CHECK, false)
-                .set_experiment(Experiment::SPEC_REWRITE, false)
+                .set_experiment(Experiment::LAMBDA_FIELDS, true)
+                .set_experiment(Experiment::LAMBDA_PARAMS, true)
+                .set_experiment(Experiment::LAMBDA_RESULTS, true)
+                .set_experiment(Experiment::LAMBDA_VALUES, true)
                 .set_experiment(Experiment::LAMBDA_LIFTING, true),
             stop_after: StopAfter::AstPipeline,
             dump_ast: DumpLevel::AllStages,
diff --git a/third_party/move/move-compiler/tests/move_check/typing/lambda2.exp b/third_party/move/move-compiler/tests/move_check/typing/lambda2.exp
new file mode 100644
index 0000000000000..073ed797528e3
--- /dev/null
+++ b/third_party/move/move-compiler/tests/move_check/typing/lambda2.exp
@@ -0,0 +1,30 @@
+error[E04024]: invalid usage of function type
+   ┌─ tests/move_check/typing/lambda2.move:77:18
+   │
+77 │         let _x = |i| i + 1; // expected lambda not allowed
+   │                  ^^^^^^^^^ function type only allowed for inline function arguments
+
+error[E04024]: invalid usage of function type
+   ┌─ tests/move_check/typing/lambda2.move:81:12
+   │
+81 │         f: |u64|u64, // expected lambda not allowed
+   │            ^^^^^^^^ function type only allowed for inline function arguments
+
+error[E04024]: invalid usage of function type
+   ┌─ tests/move_check/typing/lambda2.move:84:46
+   │
+84 │     public fun fun_arg_lambda_not_allowed(x: |u64|) {} // expected lambda not allowed
+   │                                              ^^^^^ function type only allowed for inline function arguments
+
+error[E04024]: invalid usage of function type
+   ┌─ tests/move_check/typing/lambda2.move:86:58
+   │
+86 │     public inline fun macro_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
+   │                                                          ^^^^^ function type only allowed for inline function arguments
+
+error[E04024]: invalid usage of function type
+   ┌─ tests/move_check/typing/lambda2.move:89:49
+   │
+89 │     public fun fun_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
+   │                                                 ^^^^^ function type only allowed for inline function arguments
+
diff --git a/third_party/move/move-compiler/tests/move_check/typing/lambda2.move b/third_party/move/move-compiler/tests/move_check/typing/lambda2.move
new file mode 100644
index 0000000000000..50bdd1270ce25
--- /dev/null
+++ b/third_party/move/move-compiler/tests/move_check/typing/lambda2.move
@@ -0,0 +1,100 @@
+module 0x8675309::M {
+    // use 0x1::XVector;
+
+    // public inline fun foreach<T>(v: &vector<T>, action: |&T|) { // expected to be not implemented
+    //     let i = 0;
+    //     while (i < XVector::length(v)) {
+    //         action(XVector::borrow(v, i));
+    //         i = i + 1;
+    //     }
+    // }
+
+    // public inline fun reduce<R, T>(v: vector<T>, accu: R, reducer: |T, R|R): R {
+    //     while (!XVector::is_empty(&v)) {
+    //         accu = reducer(XVector::pop_back(&mut v), accu);
+    //     };
+    //     accu
+    // }
+
+
+    // public fun correct_foreach() {
+    //     let v = vector[1, 2, 3];
+    //     let sum = 0;
+    //     foreach(&v, |e| sum = sum + *e) // expected to be not implemented
+    // }
+
+    // public fun correct_reduce(): u64 {
+    //     let v = vector[1, 2, 3];
+    //     reduce(v, 0, |t, r| t + r)
+    // }
+
+    // public fun corrected_nested() {
+    //     let v = vector[vector[1,2], vector[3]];
+    //     let sum = 0;
+    //     foreach(&v, |e| sum = sum + reduce!(*e, 0, |t, r| t + r));
+    // }
+
+    // public inline fun wrong_local_call_arg_count<T>(v: &vector<T>, action: |&T|) {
+    //     let i = 0;
+    //     while (i < XVector::length(v)) {
+    //         action(XVector::borrow(v, i), i); // expected to have wrong argument count
+    //         i = i + 1;
+    //     }
+    // }
+
+    // public inline fun wrong_local_call_arg_type<T>(v: &vector<T>, action: |&T|) {
+    //     let i = 0;
+    //     while (i < XVector::length(v)) {
+    //         action(i); // expected to have wrong argument type
+    //         i = i + 1;
+    //     }
+    // }
+
+    // public inline fun wrong_local_call_result_type<T>(v: &vector<T>, action: |&T|) {
+    //     let i = 0;
+    //     while (i < XVector::length(v)) {
+    //         i = i + action(XVector::borrow(v, i)); // expected to have wrong result type
+    //     }
+    // }
+
+    // public fun wrong_local_call_no_fun(x: u64) {
+    //     x(1) // expected to be not a function
+    // }
+
+    // public fun wrong_lambda_inferred_type() {
+    //     let v = vector[1, 2, 3];
+    //     let sum = 0;
+    //     foreach(&v, |e| sum = sum + e) // expected to cannot infer type
+    // }
+
+    // public fun wrong_lambda_result_type() {
+    //     let v = vector[1, 2, 3];
+    //     let sum = 0;
+    //     foreach(&v, |e| { sum = sum + *e; *e }) // expected to have wrong result type of lambda
+    // }
+
+    public fun lambda_not_allowed() {
+        let _x = |i| i + 1; // expected lambda not allowed
+    }
+
+    struct FieldFunNotAllowed {
+        f: |u64|u64, // expected lambda not allowed
+    }
+
+    public fun fun_arg_lambda_not_allowed(x: |u64|) {} // expected lambda not allowed
+
+    public inline fun macro_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
+        abort (1)
+    }
+    public fun fun_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
+        abort (1)
+    }
+
+}
+
+// module 0x1::XVector {
+//     public fun length<T>(v: &vector<T>): u64 { abort(1) }
+//     public fun is_empty<T>(v: &vector<T>): bool { abort(1) }
+//     public fun borrow<T>(v: &vector<T>, i: u64): &T { abort(1) }
+//     public fun pop_back<T>(v: &mut vector<T>): T { abort(1) }
+// }
diff --git a/third_party/move/move-model/src/builder/model_builder.rs b/third_party/move/move-model/src/builder/model_builder.rs
index 3fb7e1afa5322..7faa85f057f97 100644
--- a/third_party/move/move-model/src/builder/model_builder.rs
+++ b/third_party/move/move-model/src/builder/model_builder.rs
@@ -151,8 +151,9 @@ pub(crate) struct StructVariant {
 /// A declaration of a function.
 #[derive(Debug, Clone)]
 pub(crate) struct FunEntry {
-    pub loc: Loc,      // location of the entire function span
-    pub name_loc: Loc, // location of just the function name
+    pub loc: Loc,             // location of the entire function span
+    pub name_loc: Loc,        // location of just the function name
+    pub result_type_loc: Loc, // location of the result type declaration
     pub module_id: ModuleId,
     pub fun_id: FunId,
     pub visibility: Visibility,
diff --git a/third_party/move/move-model/src/builder/module_builder.rs b/third_party/move/move-model/src/builder/module_builder.rs
index 8b4d7133ae2b1..815908e1f4e81 100644
--- a/third_party/move/move-model/src/builder/module_builder.rs
+++ b/third_party/move/move-model/src/builder/module_builder.rs
@@ -568,9 +568,11 @@ impl<'env, 'translator> ModuleBuilder<'env, 'translator> {
         let is_native = matches!(def.body.value, EA::FunctionBody_::Native);
         let def_loc = et.to_loc(&def.loc);
         let name_loc = et.to_loc(&name.loc());
+        let result_type_loc = et.to_loc(&def.signature.return_type.loc);
         et.parent.parent.define_fun(qsym.clone(), FunEntry {
             loc: def_loc.clone(),
             name_loc,
+            result_type_loc,
             module_id: et.parent.module_id,
             fun_id,
             visibility,
@@ -3685,6 +3687,7 @@ impl<'env, 'translator> ModuleBuilder<'env, 'translator> {
                 name: name.symbol,
                 loc: entry.loc.clone(),
                 id_loc: entry.name_loc.clone(),
+                result_type_loc: entry.result_type_loc.clone(),
                 def_idx: None,
                 handle_idx: None,
                 visibility: entry.visibility,
diff --git a/third_party/move/move-model/src/model.rs b/third_party/move/move-model/src/model.rs
index c32fe3781f105..b41e6c2f8f8b2 100644
--- a/third_party/move/move-model/src/model.rs
+++ b/third_party/move/move-model/src/model.rs
@@ -1876,7 +1876,8 @@ impl GlobalEnv {
         let data = FunctionData {
             name,
             loc: loc.clone(),
-            id_loc: loc,
+            id_loc: loc.clone(),
+            result_type_loc: loc,
             def_idx: None,
             handle_idx: None,
             visibility,
@@ -2374,7 +2375,6 @@ impl GlobalEnv {
 
     pub fn internal_dump_env(&self, all: bool) -> String {
         let spool = self.symbol_pool();
-        let tctx = &self.get_type_display_ctx();
         let writer = CodeWriter::new(self.internal_loc());
         for module in self.get_modules() {
             if !all && !module.is_target() {
@@ -2428,6 +2428,7 @@ impl GlobalEnv {
                 emitln!(writer, "{}", self.display(&*module_spec));
             }
             for str in module.get_structs() {
+                let tctx = str.get_type_display_ctx();
                 if str.has_variants() {
                     emitln!(writer, "enum {} {{", str.get_name().display(spool));
                     writer.indent();
@@ -2438,7 +2439,7 @@ impl GlobalEnv {
                             emitln!(writer, " {");
                             writer.indent();
                             for fld in fields {
-                                emitln!(writer, "{},", self.dump_field(tctx, &fld))
+                                emitln!(writer, "{},", self.dump_field(&tctx, &fld))
                             }
                             writer.unindent();
                             emitln!(writer, "}")
@@ -2450,7 +2451,7 @@ impl GlobalEnv {
                     emitln!(writer, "struct {} {{", str.get_name().display(spool));
                     writer.indent();
                     for fld in str.get_fields() {
-                        emitln!(writer, "{},", self.dump_field(tctx, &fld))
+                        emitln!(writer, "{},", self.dump_field(&tctx, &fld))
                     }
                 }
                 writer.unindent();
@@ -2461,7 +2462,8 @@ impl GlobalEnv {
                 }
             }
             for fun in module.get_functions() {
-                self.dump_fun_internal(&writer, tctx, &fun);
+                let tctx = fun.get_type_display_ctx();
+                self.dump_fun_internal(&writer, &tctx, &fun);
             }
             for (_, fun) in module.get_spec_funs() {
                 emit!(
@@ -4020,6 +4022,9 @@ pub struct FunctionData {
     /// Location of the function identifier, suitable for error messages alluding to the function.
     pub(crate) id_loc: Loc,
 
+    /// Location of the function result type, suitable for error messages alluding to the result type.
+    pub(crate) result_type_loc: Loc,
+
     /// The definition index of this function in its bytecode module, if a bytecode module
     /// is attached to the parent module data.
     pub(crate) def_idx: Option<FunctionDefinitionIndex>,
@@ -4162,6 +4167,11 @@ impl<'env> FunctionEnv<'env> {
         self.data.id_loc.clone()
     }
 
+    /// Returns the location of the function identifier.
+    pub fn get_result_type_loc(&self) -> Loc {
+        self.data.result_type_loc.clone()
+    }
+
     /// Returns the attributes of this function.
     pub fn get_attributes(&self) -> &[Attribute] {
         &self.data.attributes
diff --git a/third_party/move/move-model/src/ty.rs b/third_party/move/move-model/src/ty.rs
index 97434c3fb8716..5829675c6d29b 100644
--- a/third_party/move/move-model/src/ty.rs
+++ b/third_party/move/move-model/src/ty.rs
@@ -155,6 +155,9 @@ pub enum Constraint {
     /// a pseudo constraint which never fails, but used to generate a default for
     /// inference.
     WithDefault(Type),
+    /// The type must not be function because it is used as the type of some field or
+    /// as a type argument.
+    NoFunction,
 }
 
 /// A type to describe the context from where a constraint stems. Used for
@@ -384,7 +387,10 @@ impl Constraint {
     /// for internal constraints which would be mostly confusing to users.
     pub fn hidden(&self) -> bool {
         use Constraint::*;
-        matches!(self, NoPhantom | NoReference | NoTuple | WithDefault(..))
+        matches!(
+            self,
+            NoPhantom | NoReference | NoTuple | NoFunction | WithDefault(..)
+        )
     }
 
     /// Returns true if this context is accumulating. When adding a new constraint
@@ -402,6 +408,7 @@ impl Constraint {
                 | Constraint::NoPhantom
                 | Constraint::NoTuple
                 | Constraint::NoReference
+                | Constraint::NoFunction
         )
     }
 
@@ -420,7 +427,10 @@ impl Constraint {
     /// the same type.
     pub fn report_only_once(&self) -> bool {
         use Constraint::*;
-        matches!(self, HasAbilities(..) | NoReference | NoPhantom | NoTuple)
+        matches!(
+            self,
+            HasAbilities(..) | NoReference | NoFunction | NoPhantom | NoTuple
+        )
     }
 
     /// Joins the two constraints. If they are incompatible, produces a type unification error.
@@ -505,6 +515,7 @@ impl Constraint {
                     ))
                 }
             },
+            (Constraint::NoFunction, Constraint::NoFunction) => Ok(true),
             (Constraint::NoReference, Constraint::NoReference) => Ok(true),
             (Constraint::NoTuple, Constraint::NoTuple) => Ok(true),
             (Constraint::NoPhantom, Constraint::NoPhantom) => Ok(true),
@@ -528,7 +539,11 @@ impl Constraint {
     /// type parameter. This creates NoReference, NoTuple, NoPhantom unless the type parameter is
     /// phantom, and HasAbilities if any abilities need to be met.
     pub fn for_type_parameter(param: &TypeParameter) -> Vec<Constraint> {
-        let mut result = vec![Constraint::NoReference, Constraint::NoTuple];
+        let mut result = vec![
+            Constraint::NoReference,
+            Constraint::NoTuple,
+            Constraint::NoFunction,
+        ];
         let TypeParameter(
             _,
             TypeParameterKind {
@@ -552,6 +567,7 @@ impl Constraint {
             Constraint::NoPhantom,
             Constraint::NoReference,
             Constraint::NoTuple,
+            Constraint::NoFunction,
         ]
     }
 
@@ -562,6 +578,7 @@ impl Constraint {
             Constraint::NoPhantom,
             Constraint::NoTuple,
             Constraint::NoReference,
+            Constraint::NoFunction,
         ];
         let abilities = if !field_ty.depends_from_type_parameter() {
             if struct_abilities.has_ability(Ability::Key) {
@@ -632,6 +649,7 @@ impl Constraint {
                 )
             },
             Constraint::NoReference => "no-ref".to_string(),
+            Constraint::NoFunction => "no-func".to_string(),
             Constraint::NoTuple => "no-tuple".to_string(),
             Constraint::NoPhantom => "no-phantom".to_string(),
             Constraint::HasAbilities(required_abilities) => {
@@ -806,6 +824,11 @@ impl Type {
         matches!(self, Type::Reference(_, _))
     }
 
+    /// Determines whether this is a function.
+    pub fn is_function(&self) -> bool {
+        matches!(self, Type::Fun(..))
+    }
+
     /// If this is a reference, return the kind of the reference, otherwise None.
     pub fn ref_kind(&self) -> Option<ReferenceKind> {
         if let Type::Reference(kind, _) = self {
@@ -1774,6 +1797,13 @@ impl Substitution {
                         Ok(())
                     }
                 },
+                (Constraint::NoFunction, ty) => {
+                    if ty.is_function() {
+                        constraint_unsatisfied_error()
+                    } else {
+                        Ok(())
+                    }
+                },
                 (Constraint::NoTuple, ty) => {
                     if ty.is_tuple() {
                         constraint_unsatisfied_error()
@@ -2944,6 +2974,13 @@ impl TypeUnificationError {
                             item_name()
                         )
                     },
+                    Constraint::NoFunction => {
+                        format!(
+                            "function type `{}` is not allowed {}",
+                            ty.display(display_context),
+                            item_name()
+                        )
+                    },
                     Constraint::NoPhantom => {
                         format!(
                             "phantom type `{}` can only be used as an argument for another phantom type parameter",

From b64a50c850f5c62013e44e3c6d1e9e0d1c5f10a0 Mon Sep 17 00:00:00 2001
From: "Brian R. Murphy" <132495859+brmataptos@users.noreply.github.com>
Date: Fri, 27 Sep 2024 14:54:12 -0700
Subject: [PATCH 2/6] Response to Vineeth's review

---
 .../src/env_pipeline/function_checker.rs      | 205 +++++++++++++-----
 .../move/move-compiler-v2/src/experiments.rs  |  10 +-
 .../tests/checking/inlining/lambda4.exp       |  12 +-
 .../tests/checking/inlining/lambda5.exp       |   6 +-
 .../tests/checking/typing/lambda.move         |  11 +-
 .../tests/checking/typing/lambda2.exp         |  14 +-
 .../tests/checking/typing/lambda2.move        |  29 ++-
 .../tests/checking/typing/lambda3.exp         |  17 ++
 .../tests/checking/typing/lambda3.move        |  99 +++++++++
 .../typing/lambda_returning_lambda.exp        |   7 +
 .../typing/lambda_returning_lambda.move       |  28 +++
 .../typing/lambda_returning_lambda2.exp       |   7 +
 .../typing/lambda_returning_lambda2.move      |  12 +
 .../move/move-compiler-v2/tests/testsuite.rs  |   8 +-
 .../move/move-compiler/src/typing/core.rs     |   2 +-
 .../move_check/inlining/non_lambda_arg.exp    |   4 +-
 .../parser/spec_parsing_fun_type_fail.exp     |   2 +-
 .../tests/move_check/typing/lambda.exp        |  22 +-
 .../tests/move_check/typing/lambda.move       |  11 +-
 .../tests/move_check/typing/lambda2.exp       |  14 +-
 .../tests/move_check/typing/lambda2.move      |  33 ++-
 .../tests/move_check/typing/lambda3.exp       |   6 +
 .../tests/move_check/typing/lambda3.move      |  99 +++++++++
 .../typing/lambda_returning_lambda.exp        |   6 +
 .../typing/lambda_returning_lambda.move       |  28 +++
 .../typing/lambda_returning_lambda2.exp       |  12 +
 .../typing/lambda_returning_lambda2.move      |  12 +
 .../move-model/src/builder/module_builder.rs  |  14 +-
 third_party/move/move-model/src/model.rs      |  35 +--
 third_party/move/move-model/src/ty.rs         |  10 +-
 30 files changed, 608 insertions(+), 167 deletions(-)
 create mode 100644 third_party/move/move-compiler-v2/tests/checking/typing/lambda3.exp
 create mode 100644 third_party/move/move-compiler-v2/tests/checking/typing/lambda3.move
 create mode 100644 third_party/move/move-compiler-v2/tests/checking/typing/lambda_returning_lambda.exp
 create mode 100644 third_party/move/move-compiler-v2/tests/checking/typing/lambda_returning_lambda.move
 create mode 100644 third_party/move/move-compiler-v2/tests/checking/typing/lambda_returning_lambda2.exp
 create mode 100644 third_party/move/move-compiler-v2/tests/checking/typing/lambda_returning_lambda2.move
 create mode 100644 third_party/move/move-compiler/tests/move_check/typing/lambda3.exp
 create mode 100644 third_party/move/move-compiler/tests/move_check/typing/lambda3.move
 create mode 100644 third_party/move/move-compiler/tests/move_check/typing/lambda_returning_lambda.exp
 create mode 100644 third_party/move/move-compiler/tests/move_check/typing/lambda_returning_lambda.move
 create mode 100644 third_party/move/move-compiler/tests/move_check/typing/lambda_returning_lambda2.exp
 create mode 100644 third_party/move/move-compiler/tests/move_check/typing/lambda_returning_lambda2.move

diff --git a/third_party/move/move-compiler-v2/src/env_pipeline/function_checker.rs b/third_party/move/move-compiler-v2/src/env_pipeline/function_checker.rs
index 05e86f37e82be..c70cc293aeb7a 100644
--- a/third_party/move/move-compiler-v2/src/env_pipeline/function_checker.rs
+++ b/third_party/move/move-compiler-v2/src/env_pipeline/function_checker.rs
@@ -8,20 +8,72 @@ use codespan_reporting::diagnostic::Severity;
 use move_binary_format::file_format::Visibility;
 use move_model::{
     ast::{ExpData, Operation, Pattern},
-    model::{FunId, FunctionEnv, GlobalEnv, Loc, ModuleEnv, NodeId, QualifiedId},
+    model::{FunId, FunctionEnv, GlobalEnv, Loc, ModuleEnv, NodeId, Parameter, QualifiedId},
     ty::Type,
 };
-use std::{collections::BTreeSet, iter::Iterator, vec::Vec};
+use std::{collections::BTreeSet, iter::Iterator, ops::Deref, vec::Vec};
 
 type QualifiedFunId = QualifiedId<FunId>;
 
-/// check that non-inline function parameters do not have function type.
+fn type_has_function(ty: &Type) -> bool {
+    match ty {
+        Type::Tuple(tys) => tys.iter().any(|ty| ty.is_function()),
+        Type::Fun(..) => true,
+        _ => false,
+    }
+}
+
+// Takes a list of function types, returns those which have a function type in their argument type
+fn identify_function_types_with_functions_in_args(func_returns: Vec<Type>) -> Vec<Type> {
+    func_returns
+        .into_iter()
+        .filter_map(|ty| {
+            if let Type::Fun(argt, _) = &ty {
+                if type_has_function(argt.deref()) {
+                    Some(ty)
+                } else {
+                    None
+                }
+            } else {
+                None
+            }
+        })
+        .collect()
+}
+
+// Takes a list of function-typed parameters, along with argument and result type
+// Returns a list of any parameters whose result type has a function value, along with that result type.
+fn identify_function_typed_params_with_functions_in_rets<'a>(
+    func_params: Vec<&'a Parameter>,
+) -> Vec<(&'a Parameter, &'a Type)> {
+    func_params
+        .iter()
+        .filter_map(|param| {
+            if let Type::Fun(_argt, rest) = &param.1 {
+                let rest_unboxed = rest.deref();
+                if type_has_function(rest_unboxed) {
+                    Some((*param, rest_unboxed))
+                } else {
+                    None
+                }
+            } else {
+                None
+            }
+        })
+        .collect()
+}
+
+/// check that function parameters/results do not have function type unless allowed.
+/// (1) is there a function type arg at the top level?  This is allowed for inline or LAMBDA_IN_PARAMS
+/// (2) is there a function type result at the top level?  This is allowed only for LAMBDA_IN_RETURNS
+/// (3) is there *any* function type with function type in an arg? This is allowed only for LAMBDA_IN_PARAMS
+/// (4) is there *any* function type with function type in a result? This is allowed only for LAMBDA_IN_RETURNS
 pub fn check_for_function_typed_parameters(env: &mut GlobalEnv) {
     let options = env
         .get_extension::<Options>()
         .expect("Options is available");
-    let lambda_params_ok = options.experiment_on(Experiment::LAMBDA_PARAMS);
-    let lambda_return_ok = options.experiment_on(Experiment::LAMBDA_RESULTS);
+    let lambda_params_ok = options.experiment_on(Experiment::LAMBDA_IN_PARAMS);
+    let lambda_return_ok = options.experiment_on(Experiment::LAMBDA_IN_RETURNS);
     if lambda_params_ok && lambda_return_ok {
         return;
     }
@@ -29,57 +81,112 @@ pub fn check_for_function_typed_parameters(env: &mut GlobalEnv) {
     for caller_module in env.get_modules() {
         if caller_module.is_primary_target() {
             for caller_func in caller_module.get_functions() {
-                // Check that no functions have function return type
-                if !lambda_return_ok {
+                if !lambda_params_ok || !lambda_return_ok {
                     let caller_name = caller_func.get_full_name_str();
                     let return_type = caller_func.get_result_type();
-                    let has_function_value =
-                        return_type.clone().flatten().iter().any(Type::is_function);
-                    if has_function_value {
-                        let type_display_ctx = caller_func.get_type_display_ctx();
-                        env.diag(
-                            Severity::Error,
-                            &caller_func.get_id_loc(),
-                            &format!("Functions may not return function-typed values, but function `{}` return type is `{}`:",
-                                     caller_name,
-                                     return_type.display(&type_display_ctx)),
-                        );
+                    let func_returns: Vec<_> = return_type
+                        .clone()
+                        .flatten()
+                        .into_iter()
+                        .filter(|t| t.is_function())
+                        .collect();
+                    let type_display_ctx = caller_func.get_type_display_ctx();
+                    if !func_returns.is_empty() {
+                        // (2) is there a function type result at the top level?  This is allowed
+                        // only for LAMBDA_IN_RETURNS
+                        if !lambda_return_ok {
+                            if !func_returns.is_empty() {
+                                env.diag(
+                                    Severity::Error,
+                                    &caller_func.get_result_type_loc(),
+                                    &format!("Functions may not return function-typed values, but function `{}` return type is the function type `{}`:",
+                                             &caller_name,
+                                             return_type.display(&type_display_ctx)),
+                                )
+                            }
+                        }
+                        if !lambda_params_ok {
+                            // (3) is there *any* function type with function type in an arg? This
+                            // is allowed only for LAMBDA_IN_PARAMS
+                            let bad_returns =
+                                identify_function_types_with_functions_in_args(func_returns);
+                            if !bad_returns.is_empty() {
+                                env.diag(
+                                    Severity::Error,
+                                    &caller_func.get_result_type_loc(),
+                                    &format!("Non-inline functions may not take function-typed parameters, but function `{}` return type is `{}`, which has a function type taking a function parameter:",
+                                             &caller_name,
+                                             return_type.display(&type_display_ctx)),
+                                )
+                            }
+                        }
                     }
-                }
-                // Check that non-inline function parameters don't have function type
-                if !caller_func.is_inline() && !lambda_params_ok {
-                    let parameters = caller_func.get_parameters();
-                    let bad_params: Vec<_> = parameters
+
+                    let parameters = caller_func.get_parameters_ref();
+                    let func_params: Vec<_> = parameters
                         .iter()
-                        .filter(|param| matches!(param.1, Type::Fun(_, _)))
+                        .filter(|param| matches!(param.1, Type::Fun(..)))
                         .collect();
-                    if !bad_params.is_empty() {
-                        let type_display_ctx = caller_func.get_type_display_ctx();
-                        let caller_name = caller_func.get_full_name_str();
-                        let reasons: Vec<(Loc, String)> = bad_params
-                            .iter()
-                            .map(|param| {
-                                (
-                                    param.2.clone(),
-                                    format!(
-                                        "Parameter `{}` has function-valued type `{}`.",
-                                        param.0.display(env.symbol_pool()),
-                                        param.1.display(&type_display_ctx)
+                    if !func_params.is_empty() {
+                        // (1) is there a function type arg at the top level?  This is allowed for
+                        // inline or LAMBDA_IN_PARAMS
+                        if !caller_func.is_inline() && !lambda_params_ok {
+                            let reasons: Vec<(Loc, String)> = func_params
+                                .iter()
+                                .map(|param| {
+                                    (
+                                        param.2.clone(),
+                                        format!(
+                                            "Parameter `{}` has function-valued type `{}`.",
+                                            param.0.display(env.symbol_pool()),
+                                            param.1.display(&type_display_ctx)
+                                        ),
+                                    )
+                                })
+                                .collect();
+                            env.diag_with_labels(
+                                Severity::Error,
+                                &caller_func.get_id_loc(),
+                                &format!("Only inline functions may have function-typed parameters, but non-inline function `{}` has {}:",
+                                         caller_name,
+                                         if reasons.len() > 1 { "function parameters" } else { "a function parameter" },
+                                ),
+                                reasons,
+                            );
+                        }
+                        if !lambda_return_ok {
+                            // (4) is there *any* function type with function type in its result? This is
+                            // allowed only for LAMBDA_IN_RETURNS
+                            let bad_params =
+                                identify_function_typed_params_with_functions_in_rets(func_params);
+                            if !bad_params.is_empty() {
+                                let reasons: Vec<(Loc, String)> = bad_params
+                                    .iter()
+                                    .map(|(param, ty)| {
+                                        (
+                                            param.2.clone(),
+                                            format!(
+                                                "Parameter `{}` has type `{}`, which has function type `{}` as a function result type",
+                                                param.0.display(env.symbol_pool()),
+                                                param.1.display(&type_display_ctx),
+                                                ty.display(&type_display_ctx),
+                                            ),
+                                        )
+                                    })
+                                    .collect();
+                                env.diag_with_labels(
+                                    Severity::Error,
+                                    &caller_func.get_id_loc(),
+                                    &format!("Functions may not return function-typed values, but function `{}` has {} of function type with function-typed result:",
+                                             caller_name,
+                                             if reasons.len() > 1 { "parameters" } else { "a parameter" },
                                     ),
-                                )
-                            })
-                            .collect();
-                        env.diag_with_labels(
-                            Severity::Error,
-                            &caller_func.get_id_loc(),
-                            &format!("Only inline functions may have function-typed parameters, but non-inline function `{}` has {}:",
-                                     caller_name,
-                                     if reasons.len() > 1 { "function parameters" } else { "a function parameter" },
-                            ),
-                            reasons,
-                        );
+                                    reasons,
+                                );
+                            }
+                        }
                     }
-                }
+                };
             }
         }
     }
diff --git a/third_party/move/move-compiler-v2/src/experiments.rs b/third_party/move/move-compiler-v2/src/experiments.rs
index c067d2f243ee1..ceea7b65d8403 100644
--- a/third_party/move/move-compiler-v2/src/experiments.rs
+++ b/third_party/move/move-compiler-v2/src/experiments.rs
@@ -122,14 +122,14 @@ pub static EXPERIMENTS: Lazy<BTreeMap<String, Experiment>> = Lazy::new(|| {
             default: Given(false),
         },
         Experiment {
-            name: Experiment::LAMBDA_PARAMS.to_string(),
+            name: Experiment::LAMBDA_IN_PARAMS.to_string(),
             description: "Turns on or off function values as parameters to non-inline functions"
                 .to_string(),
             default: Given(false),
         },
         Experiment {
-            name: Experiment::LAMBDA_RESULTS.to_string(),
-            description: "Turns on or off function values in function results".to_string(),
+            name: Experiment::LAMBDA_IN_RETURNS.to_string(),
+            description: "Turns on or off function values in function return values".to_string(),
             default: Given(false),
         },
         Experiment {
@@ -297,9 +297,9 @@ impl Experiment {
     pub const KEEP_INLINE_FUNS: &'static str = "keep-inline-funs";
     pub const KEEP_UNINIT_ANNOTATIONS: &'static str = "keep-uninit-annotations";
     pub const LAMBDA_FIELDS: &'static str = "lambda-fields";
+    pub const LAMBDA_IN_PARAMS: &'static str = "lambda-in-params";
+    pub const LAMBDA_IN_RETURNS: &'static str = "lambda-in-returns";
     pub const LAMBDA_LIFTING: &'static str = "lambda-lifting";
-    pub const LAMBDA_PARAMS: &'static str = "lambda-params";
-    pub const LAMBDA_RESULTS: &'static str = "lambda-results";
     pub const LAMBDA_VALUES: &'static str = "lambda-values";
     pub const LINT_CHECKS: &'static str = "lint-checks";
     pub const OPTIMIZE: &'static str = "optimize";
diff --git a/third_party/move/move-compiler-v2/tests/checking/inlining/lambda4.exp b/third_party/move/move-compiler-v2/tests/checking/inlining/lambda4.exp
index 7a6fd81d69593..14e896bb69ca5 100644
--- a/third_party/move/move-compiler-v2/tests/checking/inlining/lambda4.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/inlining/lambda4.exp
@@ -1,13 +1,13 @@
 
 Diagnostics:
-error: Functions may not return function-typed values, but function `M::macro_result_lambda_not_allowed` return type is `|u64|`:
-   ┌─ tests/checking/inlining/lambda4.move:86:23
+error: Functions may not return function-typed values, but function `M::macro_result_lambda_not_allowed` return type is the function type `|u64|`:
+   ┌─ tests/checking/inlining/lambda4.move:86:58
    │
 86 │     public inline fun macro_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
-   │                       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   │                                                          ^^^^^
 
-error: Functions may not return function-typed values, but function `M::fun_result_lambda_not_allowed` return type is `|u64|`:
-   ┌─ tests/checking/inlining/lambda4.move:89:16
+error: Functions may not return function-typed values, but function `M::fun_result_lambda_not_allowed` return type is the function type `|u64|`:
+   ┌─ tests/checking/inlining/lambda4.move:89:49
    │
 89 │     public fun fun_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
-   │                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   │                                                 ^^^^^
diff --git a/third_party/move/move-compiler-v2/tests/checking/inlining/lambda5.exp b/third_party/move/move-compiler-v2/tests/checking/inlining/lambda5.exp
index 8dc25cb601fb4..78669969275c4 100644
--- a/third_party/move/move-compiler-v2/tests/checking/inlining/lambda5.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/inlining/lambda5.exp
@@ -1,7 +1,7 @@
 
 Diagnostics:
-error: Functions may not return function-typed values, but function `M::macro_result_lambda_not_allowed` return type is `|u64|`:
-   ┌─ tests/checking/inlining/lambda5.move:86:23
+error: Functions may not return function-typed values, but function `M::macro_result_lambda_not_allowed` return type is the function type `|u64|`:
+   ┌─ tests/checking/inlining/lambda5.move:86:58
    │
 86 │     public inline fun macro_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
-   │                       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   │                                                          ^^^^^
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/lambda.move b/third_party/move/move-compiler-v2/tests/checking/typing/lambda.move
index c5e29275c3d28..92e24c0c36a90 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/lambda.move
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/lambda.move
@@ -83,18 +83,17 @@ module 0x8675309::M {
 
     public fun fun_arg_lambda_not_allowed(x: |u64|) {} // expected lambda not allowed
 
-    public inline fun macro_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
+    public inline fun inline_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
         abort (1)
     }
     public fun fun_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
         abort (1)
     }
-
 }
 
 module 0x1::XVector {
-    public fun length<T>(v: &vector<T>): u64 { abort(1) }
-    public fun is_empty<T>(v: &vector<T>): bool { abort(1) }
-    public fun borrow<T>(v: &vector<T>, i: u64): &T { abort(1) }
-    public fun pop_back<T>(v: &mut vector<T>): T { abort(1) }
+    public fun length<T>(_v: &vector<T>): u64 { abort(1) }
+    public fun is_empty<T>(_v: &vector<T>): bool { abort(1) }
+    public fun borrow<T>(_v: &vector<T>, _i: u64): &T { abort(1) }
+    public fun pop_back<T>(_v: &mut vector<T>): T { abort(1) }
 }
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/lambda2.exp b/third_party/move/move-compiler-v2/tests/checking/typing/lambda2.exp
index 3488e91208849..4f27955dd4e6f 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/lambda2.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/lambda2.exp
@@ -12,14 +12,14 @@ warning: Unused parameter `x`. Consider removing or prefixing with an underscore
 84 │     public fun fun_arg_lambda_not_allowed(x: |u64|) {} // expected lambda not allowed
    │                                           ^
 
-error: Functions may not return function-typed values, but function `M::macro_result_lambda_not_allowed` return type is `|u64|`:
-   ┌─ tests/checking/typing/lambda2.move:86:23
+error: Functions may not return function-typed values, but function `M::inline_result_lambda_not_allowed` return type is the function type `|u64|`:
+   ┌─ tests/checking/typing/lambda2.move:86:59
    │
-86 │     public inline fun macro_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
-   │                       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+86 │     public inline fun inline_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
+   │                                                           ^^^^^
 
-error: Functions may not return function-typed values, but function `M::fun_result_lambda_not_allowed` return type is `|u64|`:
-   ┌─ tests/checking/typing/lambda2.move:89:16
+error: Functions may not return function-typed values, but function `M::fun_result_lambda_not_allowed` return type is the function type `|u64|`:
+   ┌─ tests/checking/typing/lambda2.move:89:49
    │
 89 │     public fun fun_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
-   │                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   │                                                 ^^^^^
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/lambda2.move b/third_party/move/move-compiler-v2/tests/checking/typing/lambda2.move
index 5d7cc52daf2ae..ccaa472c2e2c2 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/lambda2.move
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/lambda2.move
@@ -1,5 +1,13 @@
 module 0x8675309::M {
-    // use 0x1::XVector;
+
+    // *** NOTE: THIS TEST FILE IS DERIVED FROM lambda.move by commenting out code which has errors
+    //     successfully flagged by move-compiler-v2, so that we can check for errors on other lines
+    //     which may be shadowed by those errors.
+    //
+    //     We keep the commented code so that the error line numbers line up.
+    //
+    //
+    //     ... code removed here to allow above message ...
 
     // public inline fun foreach<T>(v: &vector<T>, action: |&T|) { // expected to be not implemented
     //     let i = 0;
@@ -9,14 +17,6 @@ module 0x8675309::M {
     //     }
     // }
 
-    // public inline fun reduce<R, T>(v: vector<T>, accu: R, reducer: |T, R|R): R {
-    //     while (!XVector::is_empty(&v)) {
-    //         accu = reducer(XVector::pop_back(&mut v), accu);
-    //     };
-    //     accu
-    // }
-
-
     // public fun correct_foreach() {
     //     let v = vector[1, 2, 3];
     //     let sum = 0;
@@ -83,18 +83,17 @@ module 0x8675309::M {
 
     public fun fun_arg_lambda_not_allowed(x: |u64|) {} // expected lambda not allowed
 
-    public inline fun macro_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
+    public inline fun inline_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
         abort (1)
     }
     public fun fun_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
         abort (1)
     }
-
 }
 
 // module 0x1::XVector {
-//     public fun length<T>(v: &vector<T>): u64 { abort(1) }
-//     public fun is_empty<T>(v: &vector<T>): bool { abort(1) }
-//     public fun borrow<T>(v: &vector<T>, i: u64): &T { abort(1) }
-//     public fun pop_back<T>(v: &mut vector<T>): T { abort(1) }
+//     public fun length<T>(_v: &vector<T>): u64 { abort(1) }
+//     public fun is_empty<T>(_v: &vector<T>): bool { abort(1) }
+//     public fun borrow<T>(_v: &vector<T>, _i: u64): &T { abort(1) }
+//     public fun pop_back<T>(_v: &mut vector<T>): T { abort(1) }
 // }
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/lambda3.exp b/third_party/move/move-compiler-v2/tests/checking/typing/lambda3.exp
new file mode 100644
index 0000000000000..a629fb8ec36d9
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/lambda3.exp
@@ -0,0 +1,17 @@
+// -- Model dump before bytecode pipeline
+module 0x8675309::M {
+    public fun lambda_not_allowed() {
+        {
+          let _x: |u64|u64 = |i: u64| Add<u64>(i, 1);
+          Tuple()
+        }
+    }
+} // end 0x8675309::M
+
+
+Diagnostics:
+error: Function-typed values not yet supported except as parameters to calls to inline functions
+   ┌─ tests/checking/typing/lambda3.move:77:18
+   │
+77 │         let _x = |i| i + 1; // expected lambda not allowed
+   │                  ^^^^^^^^^
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/lambda3.move b/third_party/move/move-compiler-v2/tests/checking/typing/lambda3.move
new file mode 100644
index 0000000000000..bc302cc3ee3be
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/lambda3.move
@@ -0,0 +1,99 @@
+module 0x8675309::M {
+
+    // *** NOTE: THIS TEST FILE IS DERIVED FROM lambda2.move by commenting out code which has errors
+    //     successfully flagged by move-compiler-v2, so that we can check for errors on other lines
+    //     which may be shadowed by those errors.
+    //
+    //     We keep the commented code so that the error line numbers line up.
+    //
+    //
+    //     ... code removed here to allow above message ...
+
+    // public inline fun foreach<T>(v: &vector<T>, action: |&T|) { // expected to be not implemented
+    //     let i = 0;
+    //     while (i < XVector::length(v)) {
+    //         action(XVector::borrow(v, i));
+    //         i = i + 1;
+    //     }
+    // }
+
+    // public fun correct_foreach() {
+    //     let v = vector[1, 2, 3];
+    //     let sum = 0;
+    //     foreach(&v, |e| sum = sum + *e) // expected to be not implemented
+    // }
+
+    // public fun correct_reduce(): u64 {
+    //     let v = vector[1, 2, 3];
+    //     reduce(v, 0, |t, r| t + r)
+    // }
+
+    // public fun corrected_nested() {
+    //     let v = vector[vector[1,2], vector[3]];
+    //     let sum = 0;
+    //     foreach(&v, |e| sum = sum + reduce!(*e, 0, |t, r| t + r));
+    // }
+
+    // public inline fun wrong_local_call_arg_count<T>(v: &vector<T>, action: |&T|) {
+    //     let i = 0;
+    //     while (i < XVector::length(v)) {
+    //         action(XVector::borrow(v, i), i); // expected to have wrong argument count
+    //         i = i + 1;
+    //     }
+    // }
+
+    // public inline fun wrong_local_call_arg_type<T>(v: &vector<T>, action: |&T|) {
+    //     let i = 0;
+    //     while (i < XVector::length(v)) {
+    //         action(i); // expected to have wrong argument type
+    //         i = i + 1;
+    //     }
+    // }
+
+    // public inline fun wrong_local_call_result_type<T>(v: &vector<T>, action: |&T|) {
+    //     let i = 0;
+    //     while (i < XVector::length(v)) {
+    //         i = i + action(XVector::borrow(v, i)); // expected to have wrong result type
+    //     }
+    // }
+
+    // public fun wrong_local_call_no_fun(x: u64) {
+    //     x(1) // expected to be not a function
+    // }
+
+    // public fun wrong_lambda_inferred_type() {
+    //     let v = vector[1, 2, 3];
+    //     let sum = 0;
+    //     foreach(&v, |e| sum = sum + e) // expected to cannot infer type
+    // }
+
+    // public fun wrong_lambda_result_type() {
+    //     let v = vector[1, 2, 3];
+    //     let sum = 0;
+    //     foreach(&v, |e| { sum = sum + *e; *e }) // expected to have wrong result type of lambda
+    // }
+
+    public fun lambda_not_allowed() {
+        let _x = |i| i + 1; // expected lambda not allowed
+    }
+
+    // struct FieldFunNotAllowed {
+    //     f: |u64|u64, // expected lambda not allowed
+    // }
+
+    // public fun fun_arg_lambda_not_allowed(x: |u64|) {} // expected lambda not allowed
+
+    // public inline fun macro_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
+    //     abort (1)
+    // }
+    // public fun fun_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
+    //     abort (1)
+    // }
+}
+
+// module 0x1::XVector {
+//     public fun length<T>(_v: &vector<T>): u64 { abort(1) }
+//     public fun is_empty<T>(_v: &vector<T>): bool { abort(1) }
+//     public fun borrow<T>(_v: &vector<T>, _i: u64): &T { abort(1) }
+//     public fun pop_back<T>(_v: &mut vector<T>): T { abort(1) }
+// }
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/lambda_returning_lambda.exp b/third_party/move/move-compiler-v2/tests/checking/typing/lambda_returning_lambda.exp
new file mode 100644
index 0000000000000..d16f979db0562
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/lambda_returning_lambda.exp
@@ -0,0 +1,7 @@
+
+Diagnostics:
+error: Functions may not return function-typed values, but function `M::foreach_caller` has a parameter of function type with function-typed result:
+   ┌─ tests/checking/typing/lambda_returning_lambda.move:12:23
+   │
+12 │     public inline fun foreach_caller<T>(v: &vector<T>, action: ||(|&T|)) {
+   │                       ^^^^^^^^^^^^^^                   ------ Parameter `action` has type `|()||&T|`, which has function type `|&T|` as a function result type
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/lambda_returning_lambda.move b/third_party/move/move-compiler-v2/tests/checking/typing/lambda_returning_lambda.move
new file mode 100644
index 0000000000000..bd93f64575ac6
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/lambda_returning_lambda.move
@@ -0,0 +1,28 @@
+module 0x8675309::M {
+    use 0x1::XVector;
+
+    public inline fun foreach<T>(v: &vector<T>, action: |&T|) { // expected to be not implemented
+        let i = 0;
+        while (i < XVector::length(v)) {
+            action(XVector::borrow(v, i));
+            i = i + 1;
+        }
+    }
+
+    public inline fun foreach_caller<T>(v: &vector<T>, action: ||(|&T|)) {
+        foreach<T>(v, action())
+    }
+
+    public fun whacky_foreach() {
+        let v = vector[1, 2, 3];
+        let sum = 0;
+        foreach_caller(&v, ||(|e| sum = sum + *e)) // expected to be not implemented
+    }
+}
+
+module 0x1::XVector {
+    public fun length<T>(_v: &vector<T>): u64 { abort(1) }
+    public fun is_empty<T>(_v: &vector<T>): bool { abort(1) }
+    public fun borrow<T>(_v: &vector<T>, _i: u64): &T { abort(1) }
+    public fun pop_back<T>(_v: &mut vector<T>): T { abort(1) }
+}
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/lambda_returning_lambda2.exp b/third_party/move/move-compiler-v2/tests/checking/typing/lambda_returning_lambda2.exp
new file mode 100644
index 0000000000000..7fccdd1f60f5f
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/lambda_returning_lambda2.exp
@@ -0,0 +1,7 @@
+
+Diagnostics:
+error: Functions may not return function-typed values, but function `M::foreach_caller2` has a parameter of function type with function-typed result:
+  ┌─ tests/checking/typing/lambda_returning_lambda2.move:3:23
+  │
+3 │     public inline fun foreach_caller2<T>(_v: &vector<T>, _action: ||(|&T|)) {
+  │                       ^^^^^^^^^^^^^^^                    ------- Parameter `_action` has type `|()||&T|`, which has function type `|&T|` as a function result type
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/lambda_returning_lambda2.move b/third_party/move/move-compiler-v2/tests/checking/typing/lambda_returning_lambda2.move
new file mode 100644
index 0000000000000..a77ab5421fcd8
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/lambda_returning_lambda2.move
@@ -0,0 +1,12 @@
+module 0x8675309::M {
+
+    public inline fun foreach_caller2<T>(_v: &vector<T>, _action: ||(|&T|)) {
+        abort(1)
+    }
+
+    public fun whacky_foreach2() {
+        let v = vector[1, 2, 3];
+        let sum = 0;
+        foreach_caller2(&v, ||(|e| sum = sum + *e)) // expected to be not implemented
+    }
+}
diff --git a/third_party/move/move-compiler-v2/tests/testsuite.rs b/third_party/move/move-compiler-v2/tests/testsuite.rs
index 0bb94585d77ba..3bd4ea13694d8 100644
--- a/third_party/move/move-compiler-v2/tests/testsuite.rs
+++ b/third_party/move/move-compiler-v2/tests/testsuite.rs
@@ -127,9 +127,9 @@ const TEST_CONFIGS: Lazy<BTreeMap<&str, TestConfig>> = Lazy::new(|| {
             options: opts
                 .clone()
                 .set_experiment(Experiment::ACQUIRES_CHECK, false),
-            stop_after: StopAfter::BytecodeGen,
+            stop_after: StopAfter::BytecodeGen, // FileFormat,
             dump_ast: DumpLevel::EndStage,
-            dump_bytecode: DumpLevel::None,
+            dump_bytecode: DumpLevel::None, // EndStage,
             dump_bytecode_filter: None,
         },
         // Tests for checking v2 language features only supported if v2
@@ -170,8 +170,8 @@ const TEST_CONFIGS: Lazy<BTreeMap<&str, TestConfig>> = Lazy::new(|| {
             options: opts
                 .clone()
                 .set_experiment(Experiment::LAMBDA_FIELDS, true)
-                .set_experiment(Experiment::LAMBDA_PARAMS, true)
-                .set_experiment(Experiment::LAMBDA_RESULTS, true)
+                .set_experiment(Experiment::LAMBDA_IN_PARAMS, true)
+                .set_experiment(Experiment::LAMBDA_IN_RETURNS, true)
                 .set_experiment(Experiment::LAMBDA_VALUES, true)
                 .set_experiment(Experiment::LAMBDA_LIFTING, true),
             stop_after: StopAfter::AstPipeline,
diff --git a/third_party/move/move-compiler/src/typing/core.rs b/third_party/move/move-compiler/src/typing/core.rs
index 1b1c196e57f3a..df4bf1dae52c6 100644
--- a/third_party/move/move-compiler/src/typing/core.rs
+++ b/third_party/move/move-compiler/src/typing/core.rs
@@ -1664,7 +1664,7 @@ pub fn check_non_fun(context: &mut Context, ty: &Type) {
             TypeSafety::InvalidFunctionType,
             (
                 *loc,
-                "function type only allowed for inline function arguments"
+                "function-typed values only allowed for inline function arguments"
             )
         ))
     }
diff --git a/third_party/move/move-compiler/tests/move_check/inlining/non_lambda_arg.exp b/third_party/move/move-compiler/tests/move_check/inlining/non_lambda_arg.exp
index 51dfb276b5342..b0d908310701a 100644
--- a/third_party/move/move-compiler/tests/move_check/inlining/non_lambda_arg.exp
+++ b/third_party/move/move-compiler/tests/move_check/inlining/non_lambda_arg.exp
@@ -2,11 +2,11 @@ error[E04024]: invalid usage of function type
   ┌─ tests/move_check/inlining/non_lambda_arg.move:4:71
   │
 4 │     public fun incorrect_sort<T: copy>(arr: &mut vector<T>, a_less_b: |T, T| bool) {
-  │                                                                       ^^^^^^^^^^^ function type only allowed for inline function arguments
+  │                                                                       ^^^^^^^^^^^ function-typed values only allowed for inline function arguments
 
 error[E04024]: invalid usage of function type
   ┌─ tests/move_check/inlining/non_lambda_arg.move:9:102
   │
 9 │     public fun incorrect_sort_recursive<T: copy>(arr: &mut vector<T>, low: u64, high: u64, a_less_b: |T, T| bool) {
-  │                                                                                                      ^^^^^^^^^^^ function type only allowed for inline function arguments
+  │                                                                                                      ^^^^^^^^^^^ function-typed values only allowed for inline function arguments
 
diff --git a/third_party/move/move-compiler/tests/move_check/parser/spec_parsing_fun_type_fail.exp b/third_party/move/move-compiler/tests/move_check/parser/spec_parsing_fun_type_fail.exp
index e305bdc9c047b..8f5acce33805a 100644
--- a/third_party/move/move-compiler/tests/move_check/parser/spec_parsing_fun_type_fail.exp
+++ b/third_party/move/move-compiler/tests/move_check/parser/spec_parsing_fun_type_fail.exp
@@ -2,5 +2,5 @@ error[E04024]: invalid usage of function type
   ┌─ tests/move_check/parser/spec_parsing_fun_type_fail.move:2:29
   │
 2 │     fun fun_type_in_prog(p: |u64|u64) {
-  │                             ^^^^^^^^ function type only allowed for inline function arguments
+  │                             ^^^^^^^^ function-typed values only allowed for inline function arguments
 
diff --git a/third_party/move/move-compiler/tests/move_check/typing/lambda.exp b/third_party/move/move-compiler/tests/move_check/typing/lambda.exp
index e59ad1ba145cf..f3bf11a387c2c 100644
--- a/third_party/move/move-compiler/tests/move_check/typing/lambda.exp
+++ b/third_party/move/move-compiler/tests/move_check/typing/lambda.exp
@@ -22,8 +22,8 @@ error[E04007]: incompatible types
 48 │             action(i); // expected to have wrong argument type
    │             ^^^^^^^^^ Invalid call of 'action'. Invalid argument type
    ·
-96 │     public fun length<T>(v: &vector<T>): u64 { abort(1) }
-   │                                          --- Given: 'u64'
+95 │     public fun length<T>(_v: &vector<T>): u64 { abort(1) }
+   │                                           --- Given: 'u64'
 
 error[E04007]: incompatible types
    ┌─ tests/move_check/typing/lambda.move:56:19
@@ -34,8 +34,8 @@ error[E04007]: incompatible types
 56 │             i = i + action(XVector::borrow(v, i)); // expected to have wrong result type
    │                   ^ Incompatible arguments to '+'
    ·
-96 │     public fun length<T>(v: &vector<T>): u64 { abort(1) }
-   │                                          --- Found: 'u64'. It is not compatible with the other type.
+95 │     public fun length<T>(_v: &vector<T>): u64 { abort(1) }
+   │                                           --- Found: 'u64'. It is not compatible with the other type.
 
 error[E04007]: incompatible types
    ┌─ tests/move_check/typing/lambda.move:61:9
@@ -71,29 +71,29 @@ error[E04024]: invalid usage of function type
    ┌─ tests/move_check/typing/lambda.move:77:18
    │
 77 │         let _x = |i| i + 1; // expected lambda not allowed
-   │                  ^^^^^^^^^ function type only allowed for inline function arguments
+   │                  ^^^^^^^^^ function-typed values only allowed for inline function arguments
 
 error[E04024]: invalid usage of function type
    ┌─ tests/move_check/typing/lambda.move:81:12
    │
 81 │         f: |u64|u64, // expected lambda not allowed
-   │            ^^^^^^^^ function type only allowed for inline function arguments
+   │            ^^^^^^^^ function-typed values only allowed for inline function arguments
 
 error[E04024]: invalid usage of function type
    ┌─ tests/move_check/typing/lambda.move:84:46
    │
 84 │     public fun fun_arg_lambda_not_allowed(x: |u64|) {} // expected lambda not allowed
-   │                                              ^^^^^ function type only allowed for inline function arguments
+   │                                              ^^^^^ function-typed values only allowed for inline function arguments
 
 error[E04024]: invalid usage of function type
-   ┌─ tests/move_check/typing/lambda.move:86:58
+   ┌─ tests/move_check/typing/lambda.move:86:59
    │
-86 │     public inline fun macro_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
-   │                                                          ^^^^^ function type only allowed for inline function arguments
+86 │     public inline fun inline_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
+   │                                                           ^^^^^ function-typed values only allowed for inline function arguments
 
 error[E04024]: invalid usage of function type
    ┌─ tests/move_check/typing/lambda.move:89:49
    │
 89 │     public fun fun_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
-   │                                                 ^^^^^ function type only allowed for inline function arguments
+   │                                                 ^^^^^ function-typed values only allowed for inline function arguments
 
diff --git a/third_party/move/move-compiler/tests/move_check/typing/lambda.move b/third_party/move/move-compiler/tests/move_check/typing/lambda.move
index c5e29275c3d28..92e24c0c36a90 100644
--- a/third_party/move/move-compiler/tests/move_check/typing/lambda.move
+++ b/third_party/move/move-compiler/tests/move_check/typing/lambda.move
@@ -83,18 +83,17 @@ module 0x8675309::M {
 
     public fun fun_arg_lambda_not_allowed(x: |u64|) {} // expected lambda not allowed
 
-    public inline fun macro_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
+    public inline fun inline_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
         abort (1)
     }
     public fun fun_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
         abort (1)
     }
-
 }
 
 module 0x1::XVector {
-    public fun length<T>(v: &vector<T>): u64 { abort(1) }
-    public fun is_empty<T>(v: &vector<T>): bool { abort(1) }
-    public fun borrow<T>(v: &vector<T>, i: u64): &T { abort(1) }
-    public fun pop_back<T>(v: &mut vector<T>): T { abort(1) }
+    public fun length<T>(_v: &vector<T>): u64 { abort(1) }
+    public fun is_empty<T>(_v: &vector<T>): bool { abort(1) }
+    public fun borrow<T>(_v: &vector<T>, _i: u64): &T { abort(1) }
+    public fun pop_back<T>(_v: &mut vector<T>): T { abort(1) }
 }
diff --git a/third_party/move/move-compiler/tests/move_check/typing/lambda2.exp b/third_party/move/move-compiler/tests/move_check/typing/lambda2.exp
index 073ed797528e3..6a329bd27c5d2 100644
--- a/third_party/move/move-compiler/tests/move_check/typing/lambda2.exp
+++ b/third_party/move/move-compiler/tests/move_check/typing/lambda2.exp
@@ -2,29 +2,23 @@ error[E04024]: invalid usage of function type
    ┌─ tests/move_check/typing/lambda2.move:77:18
    │
 77 │         let _x = |i| i + 1; // expected lambda not allowed
-   │                  ^^^^^^^^^ function type only allowed for inline function arguments
-
-error[E04024]: invalid usage of function type
-   ┌─ tests/move_check/typing/lambda2.move:81:12
-   │
-81 │         f: |u64|u64, // expected lambda not allowed
-   │            ^^^^^^^^ function type only allowed for inline function arguments
+   │                  ^^^^^^^^^ function-typed values only allowed for inline function arguments
 
 error[E04024]: invalid usage of function type
    ┌─ tests/move_check/typing/lambda2.move:84:46
    │
 84 │     public fun fun_arg_lambda_not_allowed(x: |u64|) {} // expected lambda not allowed
-   │                                              ^^^^^ function type only allowed for inline function arguments
+   │                                              ^^^^^ function-typed values only allowed for inline function arguments
 
 error[E04024]: invalid usage of function type
    ┌─ tests/move_check/typing/lambda2.move:86:58
    │
 86 │     public inline fun macro_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
-   │                                                          ^^^^^ function type only allowed for inline function arguments
+   │                                                          ^^^^^ function-typed values only allowed for inline function arguments
 
 error[E04024]: invalid usage of function type
    ┌─ tests/move_check/typing/lambda2.move:89:49
    │
 89 │     public fun fun_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
-   │                                                 ^^^^^ function type only allowed for inline function arguments
+   │                                                 ^^^^^ function-typed values only allowed for inline function arguments
 
diff --git a/third_party/move/move-compiler/tests/move_check/typing/lambda2.move b/third_party/move/move-compiler/tests/move_check/typing/lambda2.move
index 50bdd1270ce25..0a3ede2f22a19 100644
--- a/third_party/move/move-compiler/tests/move_check/typing/lambda2.move
+++ b/third_party/move/move-compiler/tests/move_check/typing/lambda2.move
@@ -1,5 +1,13 @@
 module 0x8675309::M {
-    // use 0x1::XVector;
+
+    // *** NOTE: THIS TEST FILE IS DERIVED FROM lambda.move by commenting out code which has errors
+    //     successfully flagged by move-compiler-v2, so that we can check for errors on other lines
+    //     which may be shadowed by those errors.
+    //
+    //     We keep the commented code so that the error line numbers line up.
+    //
+    //
+    //     ... code removed here to allow above message ...
 
     // public inline fun foreach<T>(v: &vector<T>, action: |&T|) { // expected to be not implemented
     //     let i = 0;
@@ -9,14 +17,6 @@ module 0x8675309::M {
     //     }
     // }
 
-    // public inline fun reduce<R, T>(v: vector<T>, accu: R, reducer: |T, R|R): R {
-    //     while (!XVector::is_empty(&v)) {
-    //         accu = reducer(XVector::pop_back(&mut v), accu);
-    //     };
-    //     accu
-    // }
-
-
     // public fun correct_foreach() {
     //     let v = vector[1, 2, 3];
     //     let sum = 0;
@@ -77,9 +77,9 @@ module 0x8675309::M {
         let _x = |i| i + 1; // expected lambda not allowed
     }
 
-    struct FieldFunNotAllowed {
-        f: |u64|u64, // expected lambda not allowed
-    }
+    // struct FieldFunNotAllowed {
+    //     f: |u64|u64, // expected lambda not allowed
+    // }
 
     public fun fun_arg_lambda_not_allowed(x: |u64|) {} // expected lambda not allowed
 
@@ -89,12 +89,11 @@ module 0x8675309::M {
     public fun fun_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
         abort (1)
     }
-
 }
 
 // module 0x1::XVector {
-//     public fun length<T>(v: &vector<T>): u64 { abort(1) }
-//     public fun is_empty<T>(v: &vector<T>): bool { abort(1) }
-//     public fun borrow<T>(v: &vector<T>, i: u64): &T { abort(1) }
-//     public fun pop_back<T>(v: &mut vector<T>): T { abort(1) }
+//     public fun length<T>(_v: &vector<T>): u64 { abort(1) }
+//     public fun is_empty<T>(_v: &vector<T>): bool { abort(1) }
+//     public fun borrow<T>(_v: &vector<T>, _i: u64): &T { abort(1) }
+//     public fun pop_back<T>(_v: &mut vector<T>): T { abort(1) }
 // }
diff --git a/third_party/move/move-compiler/tests/move_check/typing/lambda3.exp b/third_party/move/move-compiler/tests/move_check/typing/lambda3.exp
new file mode 100644
index 0000000000000..fcc8ff722d396
--- /dev/null
+++ b/third_party/move/move-compiler/tests/move_check/typing/lambda3.exp
@@ -0,0 +1,6 @@
+error[E04024]: invalid usage of function type
+   ┌─ tests/move_check/typing/lambda3.move:77:18
+   │
+77 │         let _x = |i| i + 1; // expected lambda not allowed
+   │                  ^^^^^^^^^ function-typed values only allowed for inline function arguments
+
diff --git a/third_party/move/move-compiler/tests/move_check/typing/lambda3.move b/third_party/move/move-compiler/tests/move_check/typing/lambda3.move
new file mode 100644
index 0000000000000..bc302cc3ee3be
--- /dev/null
+++ b/third_party/move/move-compiler/tests/move_check/typing/lambda3.move
@@ -0,0 +1,99 @@
+module 0x8675309::M {
+
+    // *** NOTE: THIS TEST FILE IS DERIVED FROM lambda2.move by commenting out code which has errors
+    //     successfully flagged by move-compiler-v2, so that we can check for errors on other lines
+    //     which may be shadowed by those errors.
+    //
+    //     We keep the commented code so that the error line numbers line up.
+    //
+    //
+    //     ... code removed here to allow above message ...
+
+    // public inline fun foreach<T>(v: &vector<T>, action: |&T|) { // expected to be not implemented
+    //     let i = 0;
+    //     while (i < XVector::length(v)) {
+    //         action(XVector::borrow(v, i));
+    //         i = i + 1;
+    //     }
+    // }
+
+    // public fun correct_foreach() {
+    //     let v = vector[1, 2, 3];
+    //     let sum = 0;
+    //     foreach(&v, |e| sum = sum + *e) // expected to be not implemented
+    // }
+
+    // public fun correct_reduce(): u64 {
+    //     let v = vector[1, 2, 3];
+    //     reduce(v, 0, |t, r| t + r)
+    // }
+
+    // public fun corrected_nested() {
+    //     let v = vector[vector[1,2], vector[3]];
+    //     let sum = 0;
+    //     foreach(&v, |e| sum = sum + reduce!(*e, 0, |t, r| t + r));
+    // }
+
+    // public inline fun wrong_local_call_arg_count<T>(v: &vector<T>, action: |&T|) {
+    //     let i = 0;
+    //     while (i < XVector::length(v)) {
+    //         action(XVector::borrow(v, i), i); // expected to have wrong argument count
+    //         i = i + 1;
+    //     }
+    // }
+
+    // public inline fun wrong_local_call_arg_type<T>(v: &vector<T>, action: |&T|) {
+    //     let i = 0;
+    //     while (i < XVector::length(v)) {
+    //         action(i); // expected to have wrong argument type
+    //         i = i + 1;
+    //     }
+    // }
+
+    // public inline fun wrong_local_call_result_type<T>(v: &vector<T>, action: |&T|) {
+    //     let i = 0;
+    //     while (i < XVector::length(v)) {
+    //         i = i + action(XVector::borrow(v, i)); // expected to have wrong result type
+    //     }
+    // }
+
+    // public fun wrong_local_call_no_fun(x: u64) {
+    //     x(1) // expected to be not a function
+    // }
+
+    // public fun wrong_lambda_inferred_type() {
+    //     let v = vector[1, 2, 3];
+    //     let sum = 0;
+    //     foreach(&v, |e| sum = sum + e) // expected to cannot infer type
+    // }
+
+    // public fun wrong_lambda_result_type() {
+    //     let v = vector[1, 2, 3];
+    //     let sum = 0;
+    //     foreach(&v, |e| { sum = sum + *e; *e }) // expected to have wrong result type of lambda
+    // }
+
+    public fun lambda_not_allowed() {
+        let _x = |i| i + 1; // expected lambda not allowed
+    }
+
+    // struct FieldFunNotAllowed {
+    //     f: |u64|u64, // expected lambda not allowed
+    // }
+
+    // public fun fun_arg_lambda_not_allowed(x: |u64|) {} // expected lambda not allowed
+
+    // public inline fun macro_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
+    //     abort (1)
+    // }
+    // public fun fun_result_lambda_not_allowed(): |u64| {  // expected lambda not allowed
+    //     abort (1)
+    // }
+}
+
+// module 0x1::XVector {
+//     public fun length<T>(_v: &vector<T>): u64 { abort(1) }
+//     public fun is_empty<T>(_v: &vector<T>): bool { abort(1) }
+//     public fun borrow<T>(_v: &vector<T>, _i: u64): &T { abort(1) }
+//     public fun pop_back<T>(_v: &mut vector<T>): T { abort(1) }
+// }
diff --git a/third_party/move/move-compiler/tests/move_check/typing/lambda_returning_lambda.exp b/third_party/move/move-compiler/tests/move_check/typing/lambda_returning_lambda.exp
new file mode 100644
index 0000000000000..7e44d487754e8
--- /dev/null
+++ b/third_party/move/move-compiler/tests/move_check/typing/lambda_returning_lambda.exp
@@ -0,0 +1,6 @@
+error[E14003]: feature not supported in inlined functions
+   ┌─ tests/move_check/typing/lambda_returning_lambda.move:13:23
+   │
+13 │         foreach<T>(v, action())
+   │                       ^^^^^^^^ Inlined function-typed parameter currently must be a literal lambda expression
+
diff --git a/third_party/move/move-compiler/tests/move_check/typing/lambda_returning_lambda.move b/third_party/move/move-compiler/tests/move_check/typing/lambda_returning_lambda.move
new file mode 100644
index 0000000000000..bd93f64575ac6
--- /dev/null
+++ b/third_party/move/move-compiler/tests/move_check/typing/lambda_returning_lambda.move
@@ -0,0 +1,28 @@
+module 0x8675309::M {
+    use 0x1::XVector;
+
+    public inline fun foreach<T>(v: &vector<T>, action: |&T|) { // expected to be not implemented
+        let i = 0;
+        while (i < XVector::length(v)) {
+            action(XVector::borrow(v, i));
+            i = i + 1;
+        }
+    }
+
+    public inline fun foreach_caller<T>(v: &vector<T>, action: ||(|&T|)) {
+        foreach<T>(v, action())
+    }
+
+    public fun whacky_foreach() {
+        let v = vector[1, 2, 3];
+        let sum = 0;
+        foreach_caller(&v, ||(|e| sum = sum + *e)) // expected to be not implemented
+    }
+}
+
+module 0x1::XVector {
+    public fun length<T>(_v: &vector<T>): u64 { abort(1) }
+    public fun is_empty<T>(_v: &vector<T>): bool { abort(1) }
+    public fun borrow<T>(_v: &vector<T>, _i: u64): &T { abort(1) }
+    public fun pop_back<T>(_v: &mut vector<T>): T { abort(1) }
+}
diff --git a/third_party/move/move-compiler/tests/move_check/typing/lambda_returning_lambda2.exp b/third_party/move/move-compiler/tests/move_check/typing/lambda_returning_lambda2.exp
new file mode 100644
index 0000000000000..3c0588535c6aa
--- /dev/null
+++ b/third_party/move/move-compiler/tests/move_check/typing/lambda_returning_lambda2.exp
@@ -0,0 +1,12 @@
+error[E04007]: incompatible types
+   ┌─ tests/move_check/typing/lambda_returning_lambda2.move:10:9
+   │
+ 3 │     public inline fun foreach_caller2<T>(_v: &vector<T>, _action: ||(u64)) {
+   │                                                                     ----- Expected: 'u64'
+   ·
+10 │         foreach_caller2(&v, ||(|e| sum = sum + *e)) // expected to be not implemented
+   │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   │         │                     │
+   │         │                     Given: '|&{integer}|()'
+   │         Invalid call of '0x8675309::M::foreach_caller2'. Invalid argument for parameter '_action'
+
diff --git a/third_party/move/move-compiler/tests/move_check/typing/lambda_returning_lambda2.move b/third_party/move/move-compiler/tests/move_check/typing/lambda_returning_lambda2.move
new file mode 100644
index 0000000000000..a77ab5421fcd8
--- /dev/null
+++ b/third_party/move/move-compiler/tests/move_check/typing/lambda_returning_lambda2.move
@@ -0,0 +1,12 @@
+module 0x8675309::M {
+
+    public inline fun foreach_caller2<T>(_v: &vector<T>, _action: ||(|&T|)) {
+        abort(1)
+    }
+
+    public fun whacky_foreach2() {
+        let v = vector[1, 2, 3];
+        let sum = 0;
+        foreach_caller2(&v, ||(|e| sum = sum + *e)) // expected to be not implemented
+    }
+}
diff --git a/third_party/move/move-model/src/builder/module_builder.rs b/third_party/move/move-model/src/builder/module_builder.rs
index 815908e1f4e81..5b5cdaeae904c 100644
--- a/third_party/move/move-model/src/builder/module_builder.rs
+++ b/third_party/move/move-model/src/builder/module_builder.rs
@@ -20,9 +20,9 @@ use crate::{
     intrinsics::process_intrinsic_declaration,
     model,
     model::{
-        EqIgnoringLoc, FieldData, FieldId, FunId, FunctionData, FunctionKind, Loc, ModuleId,
-        MoveIrLoc, NamedConstantData, NamedConstantId, NodeId, Parameter, SchemaId, SpecFunId,
-        SpecVarId, StructData, StructId, TypeParameter, TypeParameterKind,
+        EqIgnoringLoc, FieldData, FieldId, FunId, FunctionData, FunctionKind, FunctionLoc, Loc,
+        ModuleId, MoveIrLoc, NamedConstantData, NamedConstantId, NodeId, Parameter, SchemaId,
+        SpecFunId, SpecVarId, StructData, StructId, TypeParameter, TypeParameterKind,
     },
     options::ModelBuilderOptions,
     pragmas::{
@@ -3685,9 +3685,11 @@ impl<'env, 'translator> ModuleBuilder<'env, 'translator> {
             let fun_id = FunId::new(name.symbol);
             let data = FunctionData {
                 name: name.symbol,
-                loc: entry.loc.clone(),
-                id_loc: entry.name_loc.clone(),
-                result_type_loc: entry.result_type_loc.clone(),
+                loc: FunctionLoc {
+                    full: entry.loc.clone(),
+                    id_loc: entry.name_loc.clone(),
+                    result_type_loc: entry.result_type_loc.clone(),
+                },
                 def_idx: None,
                 handle_idx: None,
                 visibility: entry.visibility,
diff --git a/third_party/move/move-model/src/model.rs b/third_party/move/move-model/src/model.rs
index b41e6c2f8f8b2..ba2f65c96b995 100644
--- a/third_party/move/move-model/src/model.rs
+++ b/third_party/move/move-model/src/model.rs
@@ -1875,9 +1875,11 @@ impl GlobalEnv {
         let called_funs = def.called_funs();
         let data = FunctionData {
             name,
-            loc: loc.clone(),
-            id_loc: loc.clone(),
-            result_type_loc: loc,
+            loc: FunctionLoc {
+                full: loc.clone(),
+                id_loc: loc.clone(),
+                result_type_loc: loc,
+            },
             def_idx: None,
             handle_idx: None,
             visibility,
@@ -4011,19 +4013,26 @@ impl EqIgnoringLoc for Parameter {
     }
 }
 
-#[derive(Debug)]
-pub struct FunctionData {
-    /// Name of this function.
-    pub(crate) name: Symbol,
-
+/// Represents source code locations associated with a function.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub struct FunctionLoc {
     /// Location of this function.
-    pub(crate) loc: Loc,
+    pub(crate) full: Loc,
 
     /// Location of the function identifier, suitable for error messages alluding to the function.
     pub(crate) id_loc: Loc,
 
     /// Location of the function result type, suitable for error messages alluding to the result type.
     pub(crate) result_type_loc: Loc,
+}
+
+#[derive(Debug)]
+pub struct FunctionData {
+    /// Name of this function.
+    pub(crate) name: Symbol,
+
+    /// Locations of this function.
+    pub(crate) loc: FunctionLoc,
 
     /// The definition index of this function in its bytecode module, if a bytecode module
     /// is attached to the parent module data.
@@ -4144,7 +4153,7 @@ impl<'env> FunctionEnv<'env> {
 
     /// Get documentation associated with this function.
     pub fn get_doc(&self) -> &str {
-        self.module_env.env.get_doc(&self.data.loc)
+        self.module_env.env.get_doc(&self.data.loc.full)
     }
 
     /// Gets the definition index of this function.
@@ -4159,17 +4168,17 @@ impl<'env> FunctionEnv<'env> {
 
     /// Returns the location of this function.
     pub fn get_loc(&self) -> Loc {
-        self.data.loc.clone()
+        self.data.loc.full.clone()
     }
 
     /// Returns the location of the function identifier.
     pub fn get_id_loc(&self) -> Loc {
-        self.data.id_loc.clone()
+        self.data.loc.id_loc.clone()
     }
 
     /// Returns the location of the function identifier.
     pub fn get_result_type_loc(&self) -> Loc {
-        self.data.result_type_loc.clone()
+        self.data.loc.result_type_loc.clone()
     }
 
     /// Returns the attributes of this function.
diff --git a/third_party/move/move-model/src/ty.rs b/third_party/move/move-model/src/ty.rs
index 5829675c6d29b..8dd977323dcb9 100644
--- a/third_party/move/move-model/src/ty.rs
+++ b/third_party/move/move-model/src/ty.rs
@@ -535,14 +535,14 @@ impl Constraint {
         }
     }
 
-    /// Returns the constraints which need to be satisfied to instantiate the given
-    /// type parameter. This creates NoReference, NoTuple, NoPhantom unless the type parameter is
-    /// phantom, and HasAbilities if any abilities need to be met.
+    /// Returns the constraints which need to be satisfied to instantiate the given type
+    /// parameter. This creates NoReference, NoFunction, NoTuple, NoPhantom unless the type
+    /// parameter is phantom, and HasAbilities if any abilities need to be met.
     pub fn for_type_parameter(param: &TypeParameter) -> Vec<Constraint> {
         let mut result = vec![
             Constraint::NoReference,
             Constraint::NoTuple,
-            Constraint::NoFunction,
+            Constraint::NoFunction, // TODO(LAMBDA) - remove when implement LAMBDA_AS_TYPE_PARAMETERS
         ];
         let TypeParameter(
             _,
@@ -567,7 +567,7 @@ impl Constraint {
             Constraint::NoPhantom,
             Constraint::NoReference,
             Constraint::NoTuple,
-            Constraint::NoFunction,
+            Constraint::NoFunction, // TODO(LAMBDA) - remove when we implement LAMBDA_IN_VECTORS
         ]
     }
 

From c427bf615926d94f4df011e00277940eed7bd40f Mon Sep 17 00:00:00 2001
From: "Brian R. Murphy" <132495859+brmataptos@users.noreply.github.com>
Date: Fri, 27 Sep 2024 15:26:12 -0700
Subject: [PATCH 3/6] Final response to Vineeth's review

---
 .../tests/type_safety/gerbens_test.exp           |  2 +-
 .../src/env_pipeline/function_checker.rs         |  6 +++---
 .../src/env_pipeline/recursive_struct_checker.rs | 13 ++++++-------
 .../file_format_generator/module_generator.rs    |  2 --
 .../typing/lambda_returning_lambda2.exp          | 16 +++++-----------
 5 files changed, 15 insertions(+), 24 deletions(-)

diff --git a/third_party/move/move-bytecode-verifier/transactional-tests/tests/type_safety/gerbens_test.exp b/third_party/move/move-bytecode-verifier/transactional-tests/tests/type_safety/gerbens_test.exp
index 21191ffa107a6..739b14b80441d 100644
--- a/third_party/move/move-bytecode-verifier/transactional-tests/tests/type_safety/gerbens_test.exp
+++ b/third_party/move/move-bytecode-verifier/transactional-tests/tests/type_safety/gerbens_test.exp
@@ -5,6 +5,6 @@ Error: error[E04024]: invalid usage of function type
   ┌─ TEMPFILE:9:62
   │
 9 │     public fun for_each_ref<Element>(v: &vector<Element>, f: |&Element|) {
-  │                                                              ^^^^^^^^^^ function type only allowed for inline function arguments
+  │                                                              ^^^^^^^^^^ function-typed values only allowed for inline function arguments
 
 
diff --git a/third_party/move/move-compiler-v2/src/env_pipeline/function_checker.rs b/third_party/move/move-compiler-v2/src/env_pipeline/function_checker.rs
index c70cc293aeb7a..16e04625ed8fb 100644
--- a/third_party/move/move-compiler-v2/src/env_pipeline/function_checker.rs
+++ b/third_party/move/move-compiler-v2/src/env_pipeline/function_checker.rs
@@ -43,9 +43,9 @@ fn identify_function_types_with_functions_in_args(func_returns: Vec<Type>) -> Ve
 
 // Takes a list of function-typed parameters, along with argument and result type
 // Returns a list of any parameters whose result type has a function value, along with that result type.
-fn identify_function_typed_params_with_functions_in_rets<'a>(
-    func_params: Vec<&'a Parameter>,
-) -> Vec<(&'a Parameter, &'a Type)> {
+fn identify_function_typed_params_with_functions_in_rets(
+    func_params: Vec<&Parameter>,
+) -> Vec<(&Parameter, &Type)> {
     func_params
         .iter()
         .filter_map(|param| {
diff --git a/third_party/move/move-compiler-v2/src/env_pipeline/recursive_struct_checker.rs b/third_party/move/move-compiler-v2/src/env_pipeline/recursive_struct_checker.rs
index 1246ac0ea5ba0..987a182f663d5 100644
--- a/third_party/move/move-compiler-v2/src/env_pipeline/recursive_struct_checker.rs
+++ b/third_party/move/move-compiler-v2/src/env_pipeline/recursive_struct_checker.rs
@@ -117,12 +117,11 @@ impl<'a> RecursiveStructChecker<'a> {
             struct_name,
             struct_name,
         );
-        self.mod_env
-            .env
-            .error_with_labels(&struct_env.get_loc(), "cyclic data", vec![(
-                field_env.get_loc().clone(),
-                note,
-            )]);
+        self.mod_env.env.error_with_labels(
+            &struct_env.get_loc(),
+            "cyclic data",
+            vec![(field_env.get_loc().clone(), note)],
+        );
     }
 
     /// Report cyclic dependency of structs
@@ -195,7 +194,7 @@ impl<'a> RecursiveStructChecker<'a> {
                     .iter()
                     .any(|ty| self.ty_contains_struct(path, ty, loc.clone(), struct_id, checked))
             },
-            Type::Primitive(_) | Type::TypeParameter(_) => false,
+            Type::Primitive(_) | Type::TypeParameter(_) | Type::Fun(..) => false,
             _ => panic!("ICE: {:?} used as a type parameter", ty),
         }
     }
diff --git a/third_party/move/move-compiler-v2/src/file_format_generator/module_generator.rs b/third_party/move/move-compiler-v2/src/file_format_generator/module_generator.rs
index b371d7f17cf2e..483020e61a99e 100644
--- a/third_party/move/move-compiler-v2/src/file_format_generator/module_generator.rs
+++ b/third_party/move/move-compiler-v2/src/file_format_generator/module_generator.rs
@@ -366,8 +366,6 @@ impl ModuleGenerator {
                 }
             },
             Fun(_param_ty, _result_ty) => {
-                // let _param_ty = Box::new(self.signature_token(ctx, loc, param_ty));
-                // let _result_ty = Box::new(self.signature_token(ctx, loc, result_ty));
                 // TODO(LAMBDA)
                 ctx.error(
                     loc,
diff --git a/third_party/move/move-compiler/tests/move_check/typing/lambda_returning_lambda2.exp b/third_party/move/move-compiler/tests/move_check/typing/lambda_returning_lambda2.exp
index 3c0588535c6aa..a14e1a5ff0d5c 100644
--- a/third_party/move/move-compiler/tests/move_check/typing/lambda_returning_lambda2.exp
+++ b/third_party/move/move-compiler/tests/move_check/typing/lambda_returning_lambda2.exp
@@ -1,12 +1,6 @@
-error[E04007]: incompatible types
-   ┌─ tests/move_check/typing/lambda_returning_lambda2.move:10:9
-   │
- 3 │     public inline fun foreach_caller2<T>(_v: &vector<T>, _action: ||(u64)) {
-   │                                                                     ----- Expected: 'u64'
-   ·
-10 │         foreach_caller2(&v, ||(|e| sum = sum + *e)) // expected to be not implemented
-   │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-   │         │                     │
-   │         │                     Given: '|&{integer}|()'
-   │         Invalid call of '0x8675309::M::foreach_caller2'. Invalid argument for parameter '_action'
+warning[W09003]: unused assignment
+  ┌─ tests/move_check/typing/lambda_returning_lambda2.move:9:13
+  │
+9 │         let sum = 0;
+  │             ^^^ Unused assignment or binding for local 'sum'. Consider removing, replacing with '_', or prefixing with '_' (e.g., '_sum')
 

From f8612d6732d525946c59e19013cad6af53725c34 Mon Sep 17 00:00:00 2001
From: "Brian R. Murphy" <132495859+brmataptos@users.noreply.github.com>
Date: Mon, 30 Sep 2024 10:07:53 -0700
Subject: [PATCH 4/6] fix lint

---
 .../src/env_pipeline/function_checker.rs       | 18 ++++++++----------
 1 file changed, 8 insertions(+), 10 deletions(-)

diff --git a/third_party/move/move-compiler-v2/src/env_pipeline/function_checker.rs b/third_party/move/move-compiler-v2/src/env_pipeline/function_checker.rs
index 16e04625ed8fb..8085c408fb6c1 100644
--- a/third_party/move/move-compiler-v2/src/env_pipeline/function_checker.rs
+++ b/third_party/move/move-compiler-v2/src/env_pipeline/function_checker.rs
@@ -94,16 +94,14 @@ pub fn check_for_function_typed_parameters(env: &mut GlobalEnv) {
                     if !func_returns.is_empty() {
                         // (2) is there a function type result at the top level?  This is allowed
                         // only for LAMBDA_IN_RETURNS
-                        if !lambda_return_ok {
-                            if !func_returns.is_empty() {
-                                env.diag(
-                                    Severity::Error,
-                                    &caller_func.get_result_type_loc(),
-                                    &format!("Functions may not return function-typed values, but function `{}` return type is the function type `{}`:",
-                                             &caller_name,
-                                             return_type.display(&type_display_ctx)),
-                                )
-                            }
+                        if !lambda_return_ok && !func_returns.is_empty() {
+                            env.diag(
+                                Severity::Error,
+                                &caller_func.get_result_type_loc(),
+                                &format!("Functions may not return function-typed values, but function `{}` return type is the function type `{}`:",
+                                         &caller_name,
+                                         return_type.display(&type_display_ctx)),
+                            )
                         }
                         if !lambda_params_ok {
                             // (3) is there *any* function type with function type in an arg? This

From fa2ff8bcce6e8bf772e2bf56ec5e210eb23f8cca Mon Sep 17 00:00:00 2001
From: "Brian R. Murphy" <132495859+brmataptos@users.noreply.github.com>
Date: Mon, 30 Sep 2024 11:21:26 -0700
Subject: [PATCH 5/6] move type_has_function into Type as has_function, as
 suggested by Vineeth.

---
 .../src/env_pipeline/function_checker.rs      | 20 ++++++-------------
 .../env_pipeline/recursive_struct_checker.rs  | 11 +++++-----
 third_party/move/move-model/src/ty.rs         | 20 ++++++++++++++-----
 3 files changed, 27 insertions(+), 24 deletions(-)

diff --git a/third_party/move/move-compiler-v2/src/env_pipeline/function_checker.rs b/third_party/move/move-compiler-v2/src/env_pipeline/function_checker.rs
index 8085c408fb6c1..d7dbcc3cfce2b 100644
--- a/third_party/move/move-compiler-v2/src/env_pipeline/function_checker.rs
+++ b/third_party/move/move-compiler-v2/src/env_pipeline/function_checker.rs
@@ -15,21 +15,13 @@ use std::{collections::BTreeSet, iter::Iterator, ops::Deref, vec::Vec};
 
 type QualifiedFunId = QualifiedId<FunId>;
 
-fn type_has_function(ty: &Type) -> bool {
-    match ty {
-        Type::Tuple(tys) => tys.iter().any(|ty| ty.is_function()),
-        Type::Fun(..) => true,
-        _ => false,
-    }
-}
-
 // Takes a list of function types, returns those which have a function type in their argument type
-fn identify_function_types_with_functions_in_args(func_returns: Vec<Type>) -> Vec<Type> {
-    func_returns
+fn identify_function_types_with_functions_in_args(func_types: Vec<Type>) -> Vec<Type> {
+    func_types
         .into_iter()
         .filter_map(|ty| {
             if let Type::Fun(argt, _) = &ty {
-                if type_has_function(argt.deref()) {
+                if argt.deref().has_function() {
                     Some(ty)
                 } else {
                     None
@@ -44,14 +36,14 @@ fn identify_function_types_with_functions_in_args(func_returns: Vec<Type>) -> Ve
 // Takes a list of function-typed parameters, along with argument and result type
 // Returns a list of any parameters whose result type has a function value, along with that result type.
 fn identify_function_typed_params_with_functions_in_rets(
-    func_params: Vec<&Parameter>,
+    func_types: Vec<&Parameter>,
 ) -> Vec<(&Parameter, &Type)> {
-    func_params
+    func_types
         .iter()
         .filter_map(|param| {
             if let Type::Fun(_argt, rest) = &param.1 {
                 let rest_unboxed = rest.deref();
-                if type_has_function(rest_unboxed) {
+                if rest_unboxed.has_function() {
                     Some((*param, rest_unboxed))
                 } else {
                     None
diff --git a/third_party/move/move-compiler-v2/src/env_pipeline/recursive_struct_checker.rs b/third_party/move/move-compiler-v2/src/env_pipeline/recursive_struct_checker.rs
index 987a182f663d5..9f4d51838ff56 100644
--- a/third_party/move/move-compiler-v2/src/env_pipeline/recursive_struct_checker.rs
+++ b/third_party/move/move-compiler-v2/src/env_pipeline/recursive_struct_checker.rs
@@ -117,11 +117,12 @@ impl<'a> RecursiveStructChecker<'a> {
             struct_name,
             struct_name,
         );
-        self.mod_env.env.error_with_labels(
-            &struct_env.get_loc(),
-            "cyclic data",
-            vec![(field_env.get_loc().clone(), note)],
-        );
+        self.mod_env
+            .env
+            .error_with_labels(&struct_env.get_loc(), "cyclic data", vec![(
+                field_env.get_loc().clone(),
+                note,
+            )]);
     }
 
     /// Report cyclic dependency of structs
diff --git a/third_party/move/move-model/src/ty.rs b/third_party/move/move-model/src/ty.rs
index 8dd977323dcb9..07ee9d11abba8 100644
--- a/third_party/move/move-model/src/ty.rs
+++ b/third_party/move/move-model/src/ty.rs
@@ -819,16 +819,26 @@ impl Type {
         matches!(self, Type::Primitive(_))
     }
 
-    /// Determines whether this is a reference.
-    pub fn is_reference(&self) -> bool {
-        matches!(self, Type::Reference(_, _))
-    }
-
     /// Determines whether this is a function.
     pub fn is_function(&self) -> bool {
         matches!(self, Type::Fun(..))
     }
 
+    /// Determines whether this is a function or a tuple with a function;
+    /// this is useful to test a function parameter/return type for function values.
+    pub fn has_function(&self) -> bool {
+        match self {
+            Type::Tuple(tys) => tys.iter().any(|ty| ty.is_function()),
+            Type::Fun(..) => true,
+            _ => false,
+        }
+    }
+
+    /// Determines whether this is a reference.
+    pub fn is_reference(&self) -> bool {
+        matches!(self, Type::Reference(_, _))
+    }
+
     /// If this is a reference, return the kind of the reference, otherwise None.
     pub fn ref_kind(&self) -> Option<ReferenceKind> {
         if let Type::Reference(kind, _) = self {

From f72846fa63678a0cfb7ea0c682b1aa9c4fa2b48b Mon Sep 17 00:00:00 2001
From: "Brian R. Murphy" <132495859+brmataptos@users.noreply.github.com>
Date: Wed, 2 Oct 2024 21:40:33 -0700
Subject: [PATCH 6/6] add type param list for struct in dump

---
 .../bug_14471_receiver_inference.exp          |  2 +-
 .../tests/bytecode-generator/fields.exp       |  2 +-
 .../tests/bytecode-generator/matching_ok.exp  |  2 +-
 .../abilities/v1/ability_constraints.exp      | 16 +++++------
 .../v1/phantom_param_op_abilities.exp         | 10 +++----
 .../phantom_params_constraint_abilities.exp   | 14 +++++-----
 .../v1/phantom_params_field_abilities.exp     |  8 +++---
 .../checking/access_specifiers/access_ok.exp  |  2 +-
 .../acquires_list_generic.exp                 |  4 +--
 .../tests/checking/dotdot/dotdot_valid.exp    |  6 ++--
 .../checking/inlining/resources_valid.exp     |  2 +-
 .../naming/unused_type_parameter_struct.exp   | 12 ++++----
 .../checking/naming/warning_dependency.exp    | 12 ++++----
 .../checking/positional_fields/decl_ok.exp    |  2 +-
 .../named_tuple_ability_decl_ok.exp           | 10 +++----
 .../named_tuple_construct_ok.exp              |  4 +--
 .../variant_ability_decl_ok.exp               |  4 +--
 .../tests/checking/receiver/decl_errors.exp   |  2 +-
 .../tests/checking/receiver/generic_calls.exp |  2 +-
 .../checking/receiver/generic_calls_typed.exp |  2 +-
 .../checking/specs/intrinsic_decl_ok.exp      |  4 +--
 .../tests/checking/specs/schemas_ok.exp       |  2 +-
 .../tests/checking/specs/structs_ok.exp       |  2 +-
 .../tests/checking/typing/eq.exp              |  2 +-
 .../tests/checking/typing/exp_list.exp        |  2 +-
 .../tests/checking/typing/lambda3.exp         |  7 +++++
 .../typing/main_arguments_various_caes.exp    |  2 +-
 .../tests/checking/typing/neq.exp             |  2 +-
 .../checking/typing/nested_post_process.exp   |  4 +--
 .../typing/phantom_param_struct_decl.exp      | 10 +++----
 .../typing/type_variable_join_single_pack.exp |  2 +-
 .../type_variable_join_single_unpack.exp      |  2 +-
 ...ype_variable_join_single_unpack_assign.exp |  2 +-
 .../type_variable_join_threaded_pack.exp      |  4 +--
 .../multi_pool_money_market_token.exp         | 12 ++++----
 .../v1-examples/simple_money_market_token.exp | 10 +++----
 .../variants_test_no_parenthesis_ok.exp       |  2 +-
 .../checking/variants/variants_test_ok.exp    |  2 +-
 ...mutually_recursive_non_generic_type_ok.exp |  2 +-
 .../infinite_instantiations_valid.exp         |  2 +-
 .../tests/lambda-lifting/pattern.exp          | 28 +++++++++----------
 .../tests/op-equal/valid0.exp                 |  2 +-
 .../tests/op-equal/valid1.exp                 |  2 +-
 third_party/move/move-model/src/model.rs      | 26 +++++++++++++++--
 44 files changed, 141 insertions(+), 112 deletions(-)

diff --git a/third_party/move/move-compiler-v2/tests/bytecode-generator/bug_14471_receiver_inference.exp b/third_party/move/move-compiler-v2/tests/bytecode-generator/bug_14471_receiver_inference.exp
index 23007e7bf4d5e..693daacb1ff71 100644
--- a/third_party/move/move-compiler-v2/tests/bytecode-generator/bug_14471_receiver_inference.exp
+++ b/third_party/move/move-compiler-v2/tests/bytecode-generator/bug_14471_receiver_inference.exp
@@ -3,7 +3,7 @@ module 0x815::m {
     struct MyMap {
         table: Table<address, ValueWrap>,
     }
-    struct Table {
+    struct Table<T1,T2> {
         x: T1,
         y: T2,
     }
diff --git a/third_party/move/move-compiler-v2/tests/bytecode-generator/fields.exp b/third_party/move/move-compiler-v2/tests/bytecode-generator/fields.exp
index 4c2478d70c7e5..72ad2c417ca09 100644
--- a/third_party/move/move-compiler-v2/tests/bytecode-generator/fields.exp
+++ b/third_party/move/move-compiler-v2/tests/bytecode-generator/fields.exp
@@ -3,7 +3,7 @@ module 0x42::fields {
     struct T {
         h: u64,
     }
-    struct G {
+    struct G<X> {
         f: X,
     }
     struct S {
diff --git a/third_party/move/move-compiler-v2/tests/bytecode-generator/matching_ok.exp b/third_party/move/move-compiler-v2/tests/bytecode-generator/matching_ok.exp
index a271791a51a0b..a49fde8a4b9a3 100644
--- a/third_party/move/move-compiler-v2/tests/bytecode-generator/matching_ok.exp
+++ b/third_party/move/move-compiler-v2/tests/bytecode-generator/matching_ok.exp
@@ -39,7 +39,7 @@ module 0xc0ffee::m {
             y: u64,
         }
     }
-    enum Option {
+    enum Option<A> {
         None,
         Some {
             value: A,
diff --git a/third_party/move/move-compiler-v2/tests/checking/abilities/v1/ability_constraints.exp b/third_party/move/move-compiler-v2/tests/checking/abilities/v1/ability_constraints.exp
index 55f8fe820c1e2..f749653a7f251 100644
--- a/third_party/move/move-compiler-v2/tests/checking/abilities/v1/ability_constraints.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/abilities/v1/ability_constraints.exp
@@ -1,9 +1,9 @@
 // -- Model dump before bytecode pipeline
 module 0x42::M {
-    struct Box {
+    struct Box<T> {
         f: T,
     }
-    struct Pair {
+    struct Pair<T1,T2> {
         f1: T1,
         f2: T2,
     }
@@ -13,22 +13,22 @@ module 0x42::M {
     struct S {
         dummy_field: bool,
     }
-    struct Sc {
+    struct Sc<T> {
         dummy_field: bool,
     }
-    struct Scds {
+    struct Scds<T> {
         dummy_field: bool,
     }
-    struct Sd {
+    struct Sd<T> {
         dummy_field: bool,
     }
-    struct Sk {
+    struct Sk<T> {
         dummy_field: bool,
     }
-    struct Ss {
+    struct Ss<T> {
         dummy_field: bool,
     }
-    struct Ssk {
+    struct Ssk<T> {
         dummy_field: bool,
     }
     private fun c<T>() {
diff --git a/third_party/move/move-compiler-v2/tests/checking/abilities/v1/phantom_param_op_abilities.exp b/third_party/move/move-compiler-v2/tests/checking/abilities/v1/phantom_param_op_abilities.exp
index 01ca296b54601..0e83fb52e54e8 100644
--- a/third_party/move/move-compiler-v2/tests/checking/abilities/v1/phantom_param_op_abilities.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/abilities/v1/phantom_param_op_abilities.exp
@@ -1,21 +1,21 @@
 // -- Model dump before bytecode pipeline
 module 0x42::M {
-    struct HasCopy {
+    struct HasCopy<T1,T2> {
         a: T2,
     }
-    struct HasDrop {
+    struct HasDrop<T1,T2> {
         a: T2,
     }
-    struct HasKey {
+    struct HasKey<T1,T2> {
         a: T2,
     }
-    struct HasStore {
+    struct HasStore<T1,T2> {
         a: T2,
     }
     struct NoAbilities {
         dummy_field: bool,
     }
-    struct RequireStore {
+    struct RequireStore<T> {
         a: T,
     }
     private fun f1(ref: &mut HasDrop<NoAbilities, u64>) {
diff --git a/third_party/move/move-compiler-v2/tests/checking/abilities/v1/phantom_params_constraint_abilities.exp b/third_party/move/move-compiler-v2/tests/checking/abilities/v1/phantom_params_constraint_abilities.exp
index 278c608e4dbf9..ff67e3db96804 100644
--- a/third_party/move/move-compiler-v2/tests/checking/abilities/v1/phantom_params_constraint_abilities.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/abilities/v1/phantom_params_constraint_abilities.exp
@@ -1,30 +1,30 @@
 // -- Model dump before bytecode pipeline
 module 0x42::M {
-    struct HasAbilities {
+    struct HasAbilities<T1,T2> {
         a: T2,
     }
-    struct HasCopy {
+    struct HasCopy<T1,T2> {
         a: T2,
     }
-    struct HasDrop {
+    struct HasDrop<T1,T2> {
         a: T2,
     }
-    struct HasKey {
+    struct HasKey<T1,T2> {
         a: T2,
     }
-    struct HasStore {
+    struct HasStore<T1,T2> {
         a: T2,
     }
     struct NoAbilities {
         a: bool,
     }
-    struct S1 {
+    struct S1<T> {
         a: T,
     }
     struct S2 {
         a: S1<HasAbilities<NoAbilities, u64>>,
     }
-    struct S3 {
+    struct S3<T1,T2,T3,T4> {
         a: T1,
         b: T2,
         c: T3,
diff --git a/third_party/move/move-compiler-v2/tests/checking/abilities/v1/phantom_params_field_abilities.exp b/third_party/move/move-compiler-v2/tests/checking/abilities/v1/phantom_params_field_abilities.exp
index 2631fcfd257a1..b7bc1372321de 100644
--- a/third_party/move/move-compiler-v2/tests/checking/abilities/v1/phantom_params_field_abilities.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/abilities/v1/phantom_params_field_abilities.exp
@@ -1,15 +1,15 @@
 // -- Model dump before bytecode pipeline
 module 0x42::M {
-    struct HasCopy {
+    struct HasCopy<T1,T2> {
         a: T2,
     }
-    struct HasDrop {
+    struct HasDrop<T1,T2> {
         a: T2,
     }
-    struct HasKey {
+    struct HasKey<T1,T2> {
         a: T2,
     }
-    struct HasStore {
+    struct HasStore<T1,T2> {
         a: T2,
     }
     struct NoAbilities {
diff --git a/third_party/move/move-compiler-v2/tests/checking/access_specifiers/access_ok.exp b/third_party/move/move-compiler-v2/tests/checking/access_specifiers/access_ok.exp
index 1d58dcea66e0f..8298da9baae10 100644
--- a/third_party/move/move-compiler-v2/tests/checking/access_specifiers/access_ok.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/access_specifiers/access_ok.exp
@@ -23,7 +23,7 @@ module 0x42::m {
     struct T {
         dummy_field: bool,
     }
-    struct G {
+    struct G<T> {
         dummy_field: bool,
     }
     struct R {
diff --git a/third_party/move/move-compiler-v2/tests/checking/access_specifiers/acquires_list_generic.exp b/third_party/move/move-compiler-v2/tests/checking/access_specifiers/acquires_list_generic.exp
index d6f4603030fd1..82e8a78a2518a 100644
--- a/third_party/move/move-compiler-v2/tests/checking/access_specifiers/acquires_list_generic.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/access_specifiers/acquires_list_generic.exp
@@ -1,9 +1,9 @@
 // -- Model dump before bytecode pipeline
 module 0x42::M {
-    struct B {
+    struct B<T> {
         dummy_field: bool,
     }
-    struct CupC {
+    struct CupC<T> {
         dummy_field: bool,
     }
     struct R {
diff --git a/third_party/move/move-compiler-v2/tests/checking/dotdot/dotdot_valid.exp b/third_party/move/move-compiler-v2/tests/checking/dotdot/dotdot_valid.exp
index e0c1f7c341512..6b25517efe372 100644
--- a/third_party/move/move-compiler-v2/tests/checking/dotdot/dotdot_valid.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/dotdot/dotdot_valid.exp
@@ -27,15 +27,15 @@ module 0x42::test {
         x: bool,
         y: u8,
     }
-    struct S4 {
+    struct S4<T> {
         x: T,
         y: S3,
     }
-    struct S5 {
+    struct S5<T,U> {
         0: T,
         1: U,
     }
-    struct S6 {
+    struct S6<T,U> {
         x: T,
         y: U,
     }
diff --git a/third_party/move/move-compiler-v2/tests/checking/inlining/resources_valid.exp b/third_party/move/move-compiler-v2/tests/checking/inlining/resources_valid.exp
index 67888d34bf208..36dc07fcb1f05 100644
--- a/third_party/move/move-compiler-v2/tests/checking/inlining/resources_valid.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/inlining/resources_valid.exp
@@ -1,6 +1,6 @@
 // -- Model dump before bytecode pipeline
 module 0x42::objects {
-    struct ReaderRef {
+    struct ReaderRef<T> {
         addr: address,
     }
     public fun get_addr<T>(ref: &ReaderRef<T>): address {
diff --git a/third_party/move/move-compiler-v2/tests/checking/naming/unused_type_parameter_struct.exp b/third_party/move/move-compiler-v2/tests/checking/naming/unused_type_parameter_struct.exp
index 26343bf96eaf1..68d6effb7bd3f 100644
--- a/third_party/move/move-compiler-v2/tests/checking/naming/unused_type_parameter_struct.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/naming/unused_type_parameter_struct.exp
@@ -42,22 +42,22 @@ warning: unused type parameter
 
 // -- Model dump before bytecode pipeline
 module 0x42::test {
-    struct S0 {
+    struct S0<T> {
         dummy_field: bool,
     }
-    struct S1 {
+    struct S1<T1,T2> {
         dummy_field: bool,
     }
-    struct S2 {
+    struct S2<T1,T2> {
         f: S3<T2>,
     }
-    struct S3 {
+    struct S3<T> {
         dummy_field: bool,
     }
-    struct S4 {
+    struct S4<T,U> {
         f: vector<T>,
     }
-    struct S5 {
+    struct S5<T,U> {
         f: vector<T>,
         g: vector<U>,
     }
diff --git a/third_party/move/move-compiler-v2/tests/checking/naming/warning_dependency.exp b/third_party/move/move-compiler-v2/tests/checking/naming/warning_dependency.exp
index 406c3d29e1725..2c4e4059c504f 100644
--- a/third_party/move/move-compiler-v2/tests/checking/naming/warning_dependency.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/naming/warning_dependency.exp
@@ -11,22 +11,22 @@ module 0x42::dependency {
     use 0x42::test::{S0};
 } // end 0x42::dependency
 module 0x42::test {
-    struct S0 {
+    struct S0<T> {
         dummy_field: bool,
     }
-    struct S1 {
+    struct S1<T1,T2> {
         dummy_field: bool,
     }
-    struct S2 {
+    struct S2<T1,T2> {
         f: S3<T2>,
     }
-    struct S3 {
+    struct S3<T> {
         dummy_field: bool,
     }
-    struct S4 {
+    struct S4<T,U> {
         f: vector<T>,
     }
-    struct S5 {
+    struct S5<T,U> {
         f: vector<T>,
         g: vector<U>,
     }
diff --git a/third_party/move/move-compiler-v2/tests/checking/positional_fields/decl_ok.exp b/third_party/move/move-compiler-v2/tests/checking/positional_fields/decl_ok.exp
index 28e3ab2edd260..69f0be3a2e1ee 100644
--- a/third_party/move/move-compiler-v2/tests/checking/positional_fields/decl_ok.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/positional_fields/decl_ok.exp
@@ -15,7 +15,7 @@ module 0x42::test {
         0: u8,
         1: bool,
     }
-    struct S3 {
+    struct S3<T1,T2> {
         0: T2,
         1: u8,
         2: T1,
diff --git a/third_party/move/move-compiler-v2/tests/checking/positional_fields/named_tuple_ability_decl_ok.exp b/third_party/move/move-compiler-v2/tests/checking/positional_fields/named_tuple_ability_decl_ok.exp
index 16d650a1c6cb3..5b6703568a6ab 100644
--- a/third_party/move/move-compiler-v2/tests/checking/positional_fields/named_tuple_ability_decl_ok.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/positional_fields/named_tuple_ability_decl_ok.exp
@@ -6,23 +6,23 @@ module 0x42::test {
     struct S1 {
         0: u8,
     }
-    struct S2 {
+    struct S2<T> {
         0: T,
         1: u8,
     }
-    struct S3 {
+    struct S3<T> {
         0: T,
         1: u8,
     }
-    struct S4 {
+    struct S4<T> {
         x: u8,
         y: T,
     }
-    struct S5 {
+    struct S5<T> {
         0: T,
         1: S3<T>,
     }
-    struct S6 {
+    struct S6<T> {
         dummy_field: bool,
     }
 } // end 0x42::test
diff --git a/third_party/move/move-compiler-v2/tests/checking/positional_fields/named_tuple_construct_ok.exp b/third_party/move/move-compiler-v2/tests/checking/positional_fields/named_tuple_construct_ok.exp
index f92c198d33961..faaf3481933e0 100644
--- a/third_party/move/move-compiler-v2/tests/checking/positional_fields/named_tuple_construct_ok.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/positional_fields/named_tuple_construct_ok.exp
@@ -18,14 +18,14 @@ module 0x42::test {
         0: u8,
         1: bool,
     }
-    struct S3 {
+    struct S3<T> {
         0: T,
         1: u8,
     }
     struct S4 {
         dummy_field: bool,
     }
-    struct S5 {
+    struct S5<T> {
         x: T,
         y: u8,
     }
diff --git a/third_party/move/move-compiler-v2/tests/checking/positional_fields/variant_ability_decl_ok.exp b/third_party/move/move-compiler-v2/tests/checking/positional_fields/variant_ability_decl_ok.exp
index bb7c323f0c533..ee8fd6fdb431b 100644
--- a/third_party/move/move-compiler-v2/tests/checking/positional_fields/variant_ability_decl_ok.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/positional_fields/variant_ability_decl_ok.exp
@@ -1,6 +1,6 @@
 // -- Model dump before bytecode pipeline
 module 0x42::test {
-    enum Bar {
+    enum Bar<T> {
         A {
             0: T,
         }
@@ -9,7 +9,7 @@ module 0x42::test {
             1: bool,
         }
     }
-    enum Foo {
+    enum Foo<T> {
         A {
             0: T,
         }
diff --git a/third_party/move/move-compiler-v2/tests/checking/receiver/decl_errors.exp b/third_party/move/move-compiler-v2/tests/checking/receiver/decl_errors.exp
index 4042ecbb69c1e..4cbfc158da8cb 100644
--- a/third_party/move/move-compiler-v2/tests/checking/receiver/decl_errors.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/receiver/decl_errors.exp
@@ -38,7 +38,7 @@ module 0x42::n {
 } // end 0x42::n
 module 0x42::m {
     use 0x42::n::{T}; // resolved as: 0x42::n
-    struct G {
+    struct G<T,R> {
         x: T,
         y: R,
     }
diff --git a/third_party/move/move-compiler-v2/tests/checking/receiver/generic_calls.exp b/third_party/move/move-compiler-v2/tests/checking/receiver/generic_calls.exp
index 51a0d9cb03185..765d427973c0e 100644
--- a/third_party/move/move-compiler-v2/tests/checking/receiver/generic_calls.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/receiver/generic_calls.exp
@@ -1,6 +1,6 @@
 // -- Model dump before bytecode pipeline
 module 0x42::m {
-    struct S {
+    struct S<T> {
         x: T,
     }
     private fun id<T>(self: S<T>): S<T> {
diff --git a/third_party/move/move-compiler-v2/tests/checking/receiver/generic_calls_typed.exp b/third_party/move/move-compiler-v2/tests/checking/receiver/generic_calls_typed.exp
index 51a0d9cb03185..765d427973c0e 100644
--- a/third_party/move/move-compiler-v2/tests/checking/receiver/generic_calls_typed.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/receiver/generic_calls_typed.exp
@@ -1,6 +1,6 @@
 // -- Model dump before bytecode pipeline
 module 0x42::m {
-    struct S {
+    struct S<T> {
         x: T,
     }
     private fun id<T>(self: S<T>): S<T> {
diff --git a/third_party/move/move-compiler-v2/tests/checking/specs/intrinsic_decl_ok.exp b/third_party/move/move-compiler-v2/tests/checking/specs/intrinsic_decl_ok.exp
index 04ca7c2e62df2..c6ba5637c6bcf 100644
--- a/third_party/move/move-compiler-v2/tests/checking/specs/intrinsic_decl_ok.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/specs/intrinsic_decl_ok.exp
@@ -1,12 +1,12 @@
 // -- Model dump before bytecode pipeline
 module 0x42::M {
-    struct MyTable1 {
+    struct MyTable1<K,V> {
         dummy_field: bool,
     }
     spec {
     }
 
-    struct MyTable2 {
+    struct MyTable2<K,V> {
         dummy_field: bool,
     }
     spec {
diff --git a/third_party/move/move-compiler-v2/tests/checking/specs/schemas_ok.exp b/third_party/move/move-compiler-v2/tests/checking/specs/schemas_ok.exp
index 6f6473ed8e14c..efd869ab6d011 100644
--- a/third_party/move/move-compiler-v2/tests/checking/specs/schemas_ok.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/specs/schemas_ok.exp
@@ -52,7 +52,7 @@ note: unused schema M::SchemaExp
 
 // -- Model dump before bytecode pipeline
 module 0x42::M {
-    struct S {
+    struct S<X> {
         x: X,
     }
     private fun add(x: u64): u64 {
diff --git a/third_party/move/move-compiler-v2/tests/checking/specs/structs_ok.exp b/third_party/move/move-compiler-v2/tests/checking/specs/structs_ok.exp
index ad89e14bcd352..69ded91a3a375 100644
--- a/third_party/move/move-compiler-v2/tests/checking/specs/structs_ok.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/specs/structs_ok.exp
@@ -3,7 +3,7 @@ module 0x42::M {
     struct T {
         x: u64,
     }
-    struct G {
+    struct G<T> {
         x: T,
         y: bool,
     }
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/eq.exp b/third_party/move/move-compiler-v2/tests/checking/typing/eq.exp
index 4b6348bd2482d..66f11852a5790 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/eq.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/eq.exp
@@ -1,6 +1,6 @@
 // -- Model dump before bytecode pipeline
 module 0x8675309::M {
-    struct G {
+    struct G<T> {
         f: T,
     }
     struct R {
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/exp_list.exp b/third_party/move/move-compiler-v2/tests/checking/typing/exp_list.exp
index 59bda651fd09c..4cc3f57c1d1fe 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/exp_list.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/exp_list.exp
@@ -1,6 +1,6 @@
 // -- Model dump before bytecode pipeline
 module 0x8675309::M {
-    struct R {
+    struct R<T> {
         f: T,
     }
     struct S {
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/lambda3.exp b/third_party/move/move-compiler-v2/tests/checking/typing/lambda3.exp
index a629fb8ec36d9..f89935a0c3358 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/lambda3.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/lambda3.exp
@@ -8,6 +8,13 @@ module 0x8675309::M {
     }
 } // end 0x8675309::M
 
+// -- Sourcified model before bytecode pipeline
+module 0x8675309::M {
+    public fun lambda_not_allowed() {
+        let _x = |i| i + 1;
+    }
+}
+
 
 Diagnostics:
 error: Function-typed values not yet supported except as parameters to calls to inline functions
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/main_arguments_various_caes.exp b/third_party/move/move-compiler-v2/tests/checking/typing/main_arguments_various_caes.exp
index 95f64c5db9620..96d0c3ab89dd8 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/main_arguments_various_caes.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/main_arguments_various_caes.exp
@@ -1,6 +1,6 @@
 // -- Model dump before bytecode pipeline
 module 0x42::M {
-    struct Cup {
+    struct Cup<T> {
         f1: T,
     }
     struct R {
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/neq.exp b/third_party/move/move-compiler-v2/tests/checking/typing/neq.exp
index 17f2f53d747ed..00367877ed612 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/neq.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/neq.exp
@@ -1,6 +1,6 @@
 // -- Model dump before bytecode pipeline
 module 0x8675309::M {
-    struct G {
+    struct G<T> {
         f: T,
     }
     struct R {
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/nested_post_process.exp b/third_party/move/move-compiler-v2/tests/checking/typing/nested_post_process.exp
index 716b2a43d829e..302baa8097a2f 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/nested_post_process.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/nested_post_process.exp
@@ -3,11 +3,11 @@ module 0x42::simple_map {
     use std::error;
     use std::option;
     use std::vector;
-    struct Element {
+    struct Element<Key,Value> {
         key: Key,
         value: Value,
     }
-    struct SimpleMap {
+    struct SimpleMap<Key,Value> {
         data: vector<Element<Key, Value>>,
     }
     public fun borrow<Key,Value>(map: &SimpleMap<Key, Value>,key: &Key): &Value {
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/phantom_param_struct_decl.exp b/third_party/move/move-compiler-v2/tests/checking/typing/phantom_param_struct_decl.exp
index d905413abacbd..478578a6eacaf 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/phantom_param_struct_decl.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/phantom_param_struct_decl.exp
@@ -1,20 +1,20 @@
 // -- Model dump before bytecode pipeline
 module 0x42::M1 {
-    struct S1 {
+    struct S1<T> {
         a: u64,
     }
-    struct S2 {
+    struct S2<T> {
         a: S1<T>,
         b: vector<S1<T>>,
     }
-    struct S3 {
+    struct S3<T1,T2,T3,T4> {
         a: T2,
         b: T4,
     }
-    struct S4 {
+    struct S4<T> {
         a: u64,
     }
-    struct S5 {
+    struct S5<T> {
         a: S4<T>,
     }
 } // end 0x42::M1
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_single_pack.exp b/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_single_pack.exp
index 97821d320fdd9..fa31994614be4 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_single_pack.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_single_pack.exp
@@ -1,6 +1,6 @@
 // -- Model dump before bytecode pipeline
 module 0x42::M {
-    struct Box {
+    struct Box<T> {
         f1: T,
         f2: T,
     }
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_single_unpack.exp b/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_single_unpack.exp
index 70569d59c43d5..fd5056c8e617a 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_single_unpack.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_single_unpack.exp
@@ -1,6 +1,6 @@
 // -- Model dump before bytecode pipeline
 module 0x8675309::M {
-    struct Box {
+    struct Box<T> {
         f1: T,
         f2: T,
     }
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_single_unpack_assign.exp b/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_single_unpack_assign.exp
index 34faa633aadeb..e1f2fc3e1a998 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_single_unpack_assign.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_single_unpack_assign.exp
@@ -1,6 +1,6 @@
 // -- Model dump before bytecode pipeline
 module 0x8675309::M {
-    struct Box {
+    struct Box<T> {
         f1: T,
         f2: T,
     }
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_threaded_pack.exp b/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_threaded_pack.exp
index 5d4c04ccafe73..66848a8d97a42 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_threaded_pack.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/type_variable_join_threaded_pack.exp
@@ -1,6 +1,6 @@
 // -- Model dump before bytecode pipeline
 module 0x2::Container {
-    struct T {
+    struct T<V> {
         f: V,
     }
     public fun get<V>(_self: &T<V>): V {
@@ -15,7 +15,7 @@ module 0x2::Container {
 } // end 0x2::Container
 module 0x2::M {
     use 0x2::Container; // resolved as: 0x2::Container
-    struct Box {
+    struct Box<T> {
         f1: T,
         f2: T,
     }
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/v1-examples/multi_pool_money_market_token.exp b/third_party/move/move-compiler-v2/tests/checking/typing/v1-examples/multi_pool_money_market_token.exp
index ba2cb34b4ef5d..438c492d624f6 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/v1-examples/multi_pool_money_market_token.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/v1-examples/multi_pool_money_market_token.exp
@@ -18,7 +18,7 @@ warning: unused type parameter
 
 // -- Model dump before bytecode pipeline
 module 0x2::Token {
-    struct Coin {
+    struct Coin<AssetType> {
         type: AssetType,
         value: u64,
     }
@@ -71,7 +71,7 @@ module 0x2::Token {
     }
 } // end 0x2::Token
 module 0x2::Map {
-    struct T {
+    struct T<K,V> {
     }
     public native fun empty<K,V>(): T<K, V>;
     public native fun remove<K,V>(m: &T<K, V>,k: &K): V;
@@ -84,16 +84,16 @@ module 0x3::OneToOneMarket {
     use std::signer;
     use 0x2::Map; // resolved as: 0x2::Map
     use 0x2::Token; // resolved as: 0x2::Token
-    struct BorrowRecord {
+    struct BorrowRecord<InputAsset,OutputAsset> {
         record: Map::T<address, u64>,
     }
-    struct DepositRecord {
+    struct DepositRecord<InputAsset,OutputAsset> {
         record: Map::T<address, u64>,
     }
-    struct Pool {
+    struct Pool<AssetType> {
         coin: Token::Coin<AssetType>,
     }
-    struct Price {
+    struct Price<InputAsset,OutputAsset> {
         price: u64,
     }
     public fun borrow<In,Out>(account: &signer,pool_owner: address,amount: u64): Token::Coin<Out>
diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/v1-examples/simple_money_market_token.exp b/third_party/move/move-compiler-v2/tests/checking/typing/v1-examples/simple_money_market_token.exp
index 249b9cfb67776..3749e13a8d819 100644
--- a/third_party/move/move-compiler-v2/tests/checking/typing/v1-examples/simple_money_market_token.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/typing/v1-examples/simple_money_market_token.exp
@@ -1,6 +1,6 @@
 // -- Model dump before bytecode pipeline
 module 0x2::Token {
-    struct Coin {
+    struct Coin<AssetType> {
         type: AssetType,
         value: u64,
     }
@@ -86,16 +86,16 @@ module 0x70dd::ToddNickels {
 module 0xb055::OneToOneMarket {
     use std::signer;
     use 0x2::Token; // resolved as: 0x2::Token
-    struct BorrowRecord {
+    struct BorrowRecord<InputAsset,OutputAsset> {
         record: u64,
     }
-    struct DepositRecord {
+    struct DepositRecord<InputAsset,OutputAsset> {
         record: u64,
     }
-    struct Pool {
+    struct Pool<AssetType> {
         coin: Token::Coin<AssetType>,
     }
-    struct Price {
+    struct Price<InputAsset,OutputAsset> {
         price: u64,
     }
     public fun borrow<In,Out>(account: &signer,amount: u64): Token::Coin<Out>
diff --git a/third_party/move/move-compiler-v2/tests/checking/variants/variants_test_no_parenthesis_ok.exp b/third_party/move/move-compiler-v2/tests/checking/variants/variants_test_no_parenthesis_ok.exp
index 2c1d803d68857..da04961916c62 100644
--- a/third_party/move/move-compiler-v2/tests/checking/variants/variants_test_no_parenthesis_ok.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/variants/variants_test_no_parenthesis_ok.exp
@@ -9,7 +9,7 @@ module 0x815::m {
         Red,
         Blue,
     }
-    enum Generic {
+    enum Generic<T> {
         Foo {
             0: T,
         }
diff --git a/third_party/move/move-compiler-v2/tests/checking/variants/variants_test_ok.exp b/third_party/move/move-compiler-v2/tests/checking/variants/variants_test_ok.exp
index 2c1d803d68857..da04961916c62 100644
--- a/third_party/move/move-compiler-v2/tests/checking/variants/variants_test_ok.exp
+++ b/third_party/move/move-compiler-v2/tests/checking/variants/variants_test_ok.exp
@@ -9,7 +9,7 @@ module 0x815::m {
         Red,
         Blue,
     }
-    enum Generic {
+    enum Generic<T> {
         Foo {
             0: T,
         }
diff --git a/third_party/move/move-compiler-v2/tests/cyclic-instantiation-checker/v1-tests/mutually_recursive_non_generic_type_ok.exp b/third_party/move/move-compiler-v2/tests/cyclic-instantiation-checker/v1-tests/mutually_recursive_non_generic_type_ok.exp
index 2df7cde6d2f7c..fe2891c695b11 100644
--- a/third_party/move/move-compiler-v2/tests/cyclic-instantiation-checker/v1-tests/mutually_recursive_non_generic_type_ok.exp
+++ b/third_party/move/move-compiler-v2/tests/cyclic-instantiation-checker/v1-tests/mutually_recursive_non_generic_type_ok.exp
@@ -1,6 +1,6 @@
 // -- Model dump before bytecode pipeline
 module 0x8675309::M {
-    struct S {
+    struct S<T> {
         f: T,
     }
     private fun f<T>() {
diff --git a/third_party/move/move-compiler-v2/tests/cyclic-instantiation-checker/v1-typing/infinite_instantiations_valid.exp b/third_party/move/move-compiler-v2/tests/cyclic-instantiation-checker/v1-typing/infinite_instantiations_valid.exp
index 0d98ba2f0f67f..62dc89568b814 100644
--- a/third_party/move/move-compiler-v2/tests/cyclic-instantiation-checker/v1-typing/infinite_instantiations_valid.exp
+++ b/third_party/move/move-compiler-v2/tests/cyclic-instantiation-checker/v1-typing/infinite_instantiations_valid.exp
@@ -1,6 +1,6 @@
 // -- Model dump before bytecode pipeline
 module 0x42::M {
-    struct Box {
+    struct Box<T> {
         f: T,
     }
     public fun t0<T>() {
diff --git a/third_party/move/move-compiler-v2/tests/lambda-lifting/pattern.exp b/third_party/move/move-compiler-v2/tests/lambda-lifting/pattern.exp
index 8aa1ebc4aa0a9..9b6c76f186bb0 100644
--- a/third_party/move/move-compiler-v2/tests/lambda-lifting/pattern.exp
+++ b/third_party/move/move-compiler-v2/tests/lambda-lifting/pattern.exp
@@ -1,6 +1,6 @@
 // -- Model dump before env processor pipeline:
 module 0xcafe::m {
-    struct S {
+    struct S<T> {
         x: T,
     }
     private fun consume<T>(s: S<T>,x: T,f: |(S<T>, T)|T): T {
@@ -17,7 +17,7 @@ module 0xcafe::m {
 
 // -- Model dump after env processor unused checks:
 module 0xcafe::m {
-    struct S {
+    struct S<T> {
         x: T,
     }
     private fun consume<T>(s: S<T>,x: T,f: |(S<T>, T)|T): T {
@@ -34,7 +34,7 @@ module 0xcafe::m {
 
 // -- Model dump after env processor type parameter check:
 module 0xcafe::m {
-    struct S {
+    struct S<T> {
         x: T,
     }
     private fun consume<T>(s: S<T>,x: T,f: |(S<T>, T)|T): T {
@@ -51,7 +51,7 @@ module 0xcafe::m {
 
 // -- Model dump after env processor check recursive struct definition:
 module 0xcafe::m {
-    struct S {
+    struct S<T> {
         x: T,
     }
     private fun consume<T>(s: S<T>,x: T,f: |(S<T>, T)|T): T {
@@ -68,7 +68,7 @@ module 0xcafe::m {
 
 // -- Model dump after env processor check cyclic type instantiation:
 module 0xcafe::m {
-    struct S {
+    struct S<T> {
         x: T,
     }
     private fun consume<T>(s: S<T>,x: T,f: |(S<T>, T)|T): T {
@@ -85,7 +85,7 @@ module 0xcafe::m {
 
 // -- Model dump after env processor unused struct params check:
 module 0xcafe::m {
-    struct S {
+    struct S<T> {
         x: T,
     }
     private fun consume<T>(s: S<T>,x: T,f: |(S<T>, T)|T): T {
@@ -102,7 +102,7 @@ module 0xcafe::m {
 
 // -- Model dump after env processor access and use check before inlining:
 module 0xcafe::m {
-    struct S {
+    struct S<T> {
         x: T,
     }
     private fun consume<T>(s: S<T>,x: T,f: |(S<T>, T)|T): T {
@@ -119,7 +119,7 @@ module 0xcafe::m {
 
 // -- Model dump after env processor inlining:
 module 0xcafe::m {
-    struct S {
+    struct S<T> {
         x: T,
     }
     private fun consume<T>(s: S<T>,x: T,f: |(S<T>, T)|T): T {
@@ -136,7 +136,7 @@ module 0xcafe::m {
 
 // -- Model dump after env processor access and use check after inlining:
 module 0xcafe::m {
-    struct S {
+    struct S<T> {
         x: T,
     }
     private fun consume<T>(s: S<T>,x: T,f: |(S<T>, T)|T): T {
@@ -153,7 +153,7 @@ module 0xcafe::m {
 
 // -- Model dump after env processor acquires check:
 module 0xcafe::m {
-    struct S {
+    struct S<T> {
         x: T,
     }
     private fun consume<T>(s: S<T>,x: T,f: |(S<T>, T)|T): T {
@@ -170,7 +170,7 @@ module 0xcafe::m {
 
 // -- Model dump after env processor simplifier:
 module 0xcafe::m {
-    struct S {
+    struct S<T> {
         x: T,
     }
     private fun consume<T>(s: S<T>,x: T,f: |(S<T>, T)|T): T {
@@ -187,7 +187,7 @@ module 0xcafe::m {
 
 // -- Model dump after env processor lambda-lifting:
 module 0xcafe::m {
-    struct S {
+    struct S<T> {
         x: T,
     }
     private fun consume<T>(s: S<T>,x: T,f: |(S<T>, T)|T): T {
@@ -210,7 +210,7 @@ module 0xcafe::m {
 
 // -- Model dump after env processor specification checker:
 module 0xcafe::m {
-    struct S {
+    struct S<T> {
         x: T,
     }
     private fun consume<T>(s: S<T>,x: T,f: |(S<T>, T)|T): T {
@@ -233,7 +233,7 @@ module 0xcafe::m {
 
 // -- Model dump after env processor specification rewriter:
 module 0xcafe::m {
-    struct S {
+    struct S<T> {
         x: T,
     }
     private fun consume<T>(s: S<T>,x: T,f: |(S<T>, T)|T): T {
diff --git a/third_party/move/move-compiler-v2/tests/op-equal/valid0.exp b/third_party/move/move-compiler-v2/tests/op-equal/valid0.exp
index 398c192cb062b..e3a00fa6e9edf 100644
--- a/third_party/move/move-compiler-v2/tests/op-equal/valid0.exp
+++ b/third_party/move/move-compiler-v2/tests/op-equal/valid0.exp
@@ -3,7 +3,7 @@ module 0x42::test {
     struct Coin {
         0: u256,
     }
-    struct Wrapper {
+    struct Wrapper<T> {
         0: T,
     }
     private fun add1_new(x: u256): u256 {
diff --git a/third_party/move/move-compiler-v2/tests/op-equal/valid1.exp b/third_party/move/move-compiler-v2/tests/op-equal/valid1.exp
index a4c1156bf0a66..d75c575a32c78 100644
--- a/third_party/move/move-compiler-v2/tests/op-equal/valid1.exp
+++ b/third_party/move/move-compiler-v2/tests/op-equal/valid1.exp
@@ -3,7 +3,7 @@ module 0x42::test {
     struct Coin {
         0: u256,
     }
-    struct Wrapper {
+    struct Wrapper<T> {
         0: T,
     }
     private fun bitand_vec_coin_new(x: vector<Coin>,index: u64) {
diff --git a/third_party/move/move-model/src/model.rs b/third_party/move/move-model/src/model.rs
index ba2f65c96b995..752f6da29f2ba 100644
--- a/third_party/move/move-model/src/model.rs
+++ b/third_party/move/move-model/src/model.rs
@@ -2431,8 +2431,25 @@ impl GlobalEnv {
             }
             for str in module.get_structs() {
                 let tctx = str.get_type_display_ctx();
+                let type_params = str.get_type_parameters();
+                let type_params_str = if !type_params.is_empty() {
+                    format!(
+                        "<{}>",
+                        type_params
+                            .iter()
+                            .map(|p| p.0.display(spool).to_string())
+                            .join(",")
+                    )
+                } else {
+                    "".to_owned()
+                };
                 if str.has_variants() {
-                    emitln!(writer, "enum {} {{", str.get_name().display(spool));
+                    emitln!(
+                        writer,
+                        "enum {}{} {{",
+                        str.get_name().display(spool),
+                        type_params_str
+                    );
                     writer.indent();
                     for variant in str.get_variants() {
                         emit!(writer, "{}", variant.display(spool));
@@ -2450,7 +2467,12 @@ impl GlobalEnv {
                         }
                     }
                 } else {
-                    emitln!(writer, "struct {} {{", str.get_name().display(spool));
+                    emitln!(
+                        writer,
+                        "struct {}{} {{",
+                        str.get_name().display(spool),
+                        type_params_str
+                    );
                     writer.indent();
                     for fld in str.get_fields() {
                         emitln!(writer, "{},", self.dump_field(&tctx, &fld))