diff --git a/src/library/compiler/eager_lambda_lifting.cpp b/src/library/compiler/eager_lambda_lifting.cpp
index b950d693bb..b97f2b10d8 100644
--- a/src/library/compiler/eager_lambda_lifting.cpp
+++ b/src/library/compiler/eager_lambda_lifting.cpp
@@ -189,51 +189,57 @@ class eager_lambda_lifting_fn {
     }
 
     expr lift_lambda(expr e, bool apply_simp) {
-        lean_assert(is_lambda(e));
-        buffer<expr> fvars;
-        if (!collect_fvars(e, fvars)) {
+        /* Hack: We use `try` here because previous compilation steps may have
+           produced type incorrect terms. */
+        try {
+            lean_assert(is_lambda(e));
+            buffer<expr> fvars;
+            if (!collect_fvars(e, fvars)) {
+                return e;
+            }
+            buffer<expr> params;
+            while (is_lambda(e)) {
+                expr param_type = instantiate_rev(binding_domain(e), params.size(), params.data());
+                expr param      = m_lctx.mk_local_decl(ngen(), binding_name(e), param_type, binding_info(e));
+                params.push_back(param);
+                e = binding_body(e);
+            }
+            e = instantiate_rev(e, params.size(), params.data());
+            buffer<expr> new_params, to_copy;
+            split_fvars(fvars, params, new_params, to_copy);
+            /*
+              Variables in `to_copy` only depend on global constants
+              and other variables in `to_copy`. Moreover, `params` do not depend on them.
+              It is wasteful to pass them as new parameters to the new lifted declaration.
+              We can just copy them. The code duplication is not problematic because later at `extract_closed`
+              we will create global names for closed terms, and eliminate the redundancy.
+            */
+            e = m_lctx.mk_lambda(to_copy, e);
+            e = m_lctx.mk_lambda(params, e);
+            expr code = abstract(e, new_params.size(), new_params.data());
+            unsigned i = new_params.size();
+            while (i > 0) {
+                --i;
+                local_decl const & decl = m_lctx.get_local_decl(new_params[i]);
+                expr type = abstract(decl.get_type(), i, new_params.data());
+                code = ::lean::mk_lambda(decl.get_user_name(), type, code);
+            }
+            if (apply_simp) {
+                code = csimp(env(), code, m_cfg);
+            }
+            expr type = cheap_beta_reduce(type_checker(m_st).infer(code));
+            name n    = next_name();
+            /* We add the auxiliary declaration `n` as a "meta" axiom to the environment.
+               This is a hack to make sure we can use `csimp` to simplify `code` and
+               other definitions that use `n`.
+               We used a similar hack at `specialize.cpp`. */
+            declaration aux_ax = mk_axiom(n, names(), type, true /* meta */);
+            m_st.env() = env().add(aux_ax, false);
+            m_new_decls.push_back(comp_decl(n, code));
+            return mk_app(mk_constant(n), new_params);
+        } catch (exception &) {
             return e;
         }
-        buffer<expr> params;
-        while (is_lambda(e)) {
-            expr param_type = instantiate_rev(binding_domain(e), params.size(), params.data());
-            expr param      = m_lctx.mk_local_decl(ngen(), binding_name(e), param_type, binding_info(e));
-            params.push_back(param);
-            e = binding_body(e);
-        }
-        e = instantiate_rev(e, params.size(), params.data());
-        buffer<expr> new_params, to_copy;
-        split_fvars(fvars, params, new_params, to_copy);
-        /*
-          Variables in `to_copy` only depend on global constants
-          and other variables in `to_copy`. Moreover, `params` do not depend on them.
-          It is wasteful to pass them as new parameters to the new lifted declaration.
-          We can just copy them. The code duplication is not problematic because later at `extract_closed`
-          we will create global names for closed terms, and eliminate the redundancy.
-        */
-        e = m_lctx.mk_lambda(to_copy, e);
-        e = m_lctx.mk_lambda(params, e);
-        expr code = abstract(e, new_params.size(), new_params.data());
-        unsigned i = new_params.size();
-        while (i > 0) {
-            --i;
-            local_decl const & decl = m_lctx.get_local_decl(new_params[i]);
-            expr type = abstract(decl.get_type(), i, new_params.data());
-            code = ::lean::mk_lambda(decl.get_user_name(), type, code);
-        }
-        if (apply_simp) {
-            code = csimp(env(), code, m_cfg);
-        }
-        expr type = cheap_beta_reduce(type_checker(m_st).infer(code));
-        name n    = next_name();
-        /* We add the auxiliary declaration `n` as a "meta" axiom to the environment.
-           This is a hack to make sure we can use `csimp` to simplify `code` and
-           other definitions that use `n`.
-           We used a similar hack at `specialize.cpp`. */
-        declaration aux_ax = mk_axiom(n, names(), type, true /* meta */);
-        m_st.env() = env().add(aux_ax, false);
-        m_new_decls.push_back(comp_decl(n, code));
-        return mk_app(mk_constant(n), new_params);
     }
 
     /* Given a free variable `x`, follow let-decls and return a pair `(x, v)`.
diff --git a/tests/lean/run/341.lean b/tests/lean/run/341.lean
new file mode 100644
index 0000000000..531f212bf3
--- /dev/null
+++ b/tests/lean/run/341.lean
@@ -0,0 +1,124 @@
+section
+  variable (G : Type 1) (T : Type 1) (Tm : Type 1)
+           (EG : G → G → Type) (ET : T → T → Type) (ETm : Tm → Tm → Type)
+           (getCtx : T → G) (getTy : Tm → T)
+  inductive CtxSyntaxLayer where
+    | emp : CtxSyntaxLayer
+    | snoc : (Γ : G) → (t : T) → EG Γ (getCtx t) → CtxSyntaxLayer
+end
+section
+  variable (G : Type 1) (T : Type 1) (Tm : Type 1)
+           (EG : G → G → Type) (ET : T → T → Type) (ETm : Tm → Tm → Type)
+           (getCtx : T → G) (getTy : Tm → T)
+           (GAlgebra : CtxSyntaxLayer G T EG getCtx → G)
+
+  inductive TySyntaxLayer where
+  | top : {Γ : G} → TySyntaxLayer
+  | bot : {Γ : G} → TySyntaxLayer
+  | nat : {Γ : G} → TySyntaxLayer
+  | arrow : {Γ : G} → (A B : T) → EG Γ (getCtx A) → EG Γ (getCtx B) → TySyntaxLayer
+
+  def getCtxStep : TySyntaxLayer G T EG getCtx → G
+    | TySyntaxLayer.top (Γ := Γ) .. => Γ
+    | TySyntaxLayer.bot (Γ := Γ) .. => Γ
+    | TySyntaxLayer.nat (Γ := Γ) .. => Γ
+    | TySyntaxLayer.arrow (Γ := Γ) .. => Γ
+end
+section
+  variable (G : Type 1) (T : Type 1) (Tm : Type 1)
+           (EG : G → G → Type) (ET : T → T → Type) (ETm : Tm → Tm → Type)
+           (EGrfl : ∀ {Γ}, EG Γ Γ)
+           (getCtx : T → G) (getTy : Tm → T)
+           (GAlgebra : CtxSyntaxLayer G T EG getCtx → G) (TAlgebra : TySyntaxLayer G T EG getCtx → T)
+
+  inductive TmSyntaxLayer where
+    | tt : {Γ : G} → TmSyntaxLayer
+    | zero : {Γ : G} → TmSyntaxLayer
+    | succ : {Γ : G} → TmSyntaxLayer
+    | app : {Γ : G} → (A B : T) → (Actx : EG Γ (getCtx A)) → (Bctx : EG Γ (getCtx B))
+        → (f x : Tm)
+        → ET (getTy f) (TAlgebra (TySyntaxLayer.arrow A B Actx Bctx))
+        → ET (getTy x) A
+        → TmSyntaxLayer
+  -- set options for debugging "(kernel) declaration has metavariables" errors
+  --set_option trace.Elab.definition true
+  --set_option pp.explicit true
+  def getTyStep : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra → T
+    | TmSyntaxLayer.tt (Γ:=Γ) .. => TAlgebra (TySyntaxLayer.top (Γ:=Γ))
+    | TmSyntaxLayer.zero (Γ:=Γ) .. => TAlgebra (TySyntaxLayer.nat (Γ:=Γ))
+    | TmSyntaxLayer.succ (Γ:=Γ) .. => TAlgebra (TySyntaxLayer.arrow (TAlgebra (TySyntaxLayer.nat (Γ:=Γ))) (TAlgebra (TySyntaxLayer.nat (Γ:=Γ))) EGrfl EGrfl)
+    | TmSyntaxLayer.app (B:=B) .. => B
+end
+
+structure SyntaxModel where
+  Ctx : Type 1
+  Ty : Type 1
+  Tm : Type 1
+  EC : Ctx → Ctx → Type
+  ETy : Ty → Ty → Type
+  ETm : Tm → Tm → Type
+  getCtx : Ty → Ctx
+  getTy : Tm → Ty
+  interpCStep : CtxSyntaxLayer Ctx Ty EC getCtx → Ctx
+  interpTyStep : TySyntaxLayer Ctx Ty EC getCtx → Ty
+  interpTmStep : TmSyntaxLayer Ctx Ty Tm EC ETy getCtx getTy interpTyStep → Tm
+
+namespace SetModel
+  def Ctx := Type
+  structure Ty where
+    ctx : Ctx
+    ty : ctx → Type
+  structure Tm where
+    ty : Ty
+    tm : ∀ {Γ}, ty.ty Γ
+
+  def ECtx : Ctx → Ctx → Type := (PLift $ · = ·)
+  def ETy  : Ty  → Ty  → Type := (PLift $ · = ·)
+  def ETm  : Tm  → Tm  → Type := (PLift $ · = ·)
+
+  def interpCStep : CtxSyntaxLayer Ctx Ty ECtx Ty.ctx → Ctx
+    | CtxSyntaxLayer.emp => Unit
+    | CtxSyntaxLayer.snoc _ T (PLift.up rfl) => Σ γ : _, T.ty γ
+
+  def Ty.inj Γ T := Ty.mk Γ (λ _ => T)
+  def Ty.Unit {Γ} := Ty.inj Γ _root_.Unit
+  def Ty.Empty {Γ} := Ty.inj Γ _root_.Empty
+  def Ty.Nat {Γ} := Ty.inj Γ _root_.Nat
+
+  def Tm.inj Γ {T} (t : T) := Tm.mk (Ty.inj Γ T) t
+
+  def interpTyStep : TySyntaxLayer Ctx Ty ECtx Ty.ctx → Ty
+    | TySyntaxLayer.top (Γ:=Γ) => Ty.Unit (Γ:=Γ)
+    | TySyntaxLayer.bot (Γ:=Γ) => Ty.Empty (Γ:=Γ)
+    | TySyntaxLayer.nat (Γ:=Γ) => Ty.Nat (Γ:=Γ)
+    | TySyntaxLayer.arrow (Γ:=Γ) A B (PLift.up Actx) (PLift.up Bctx) => Ty.mk Γ (λ γ => A.ty (cast Actx γ) → B.ty (cast Bctx γ))
+
+  def interpTmStep : TmSyntaxLayer Ctx Ty Tm ECtx ETy Ty.ctx Tm.ty interpTyStep → Tm
+    | TmSyntaxLayer.tt (Γ:=Γ) => Tm.inj Γ Unit.unit
+    | TmSyntaxLayer.zero (Γ:=Γ) => Tm.inj Γ (0 : Nat)
+    | TmSyntaxLayer.succ (Γ:=Γ) => Tm.inj Γ Nat.succ
+    | TmSyntaxLayer.app (Γ:=Γ) A B (PLift.up Actx) (PLift.up Bctx) (Tm.mk fty ftm) (Tm.mk (Ty.mk xctx xty) xtm) (PLift.up fTy) (PLift.up xTy)
+        => { ty := B
+           , tm := fun {γ} =>
+                     (by
+                       simp at fTy xTy; subst fTy xTy; simp at Actx Bctx; subst Actx Bctx
+                       simp [interpTyStep, cast] at *
+                       exact (ftm xtm)
+                     )
+               }
+
+  def Model : SyntaxModel :=
+    {
+      Ctx := Ctx
+    , Ty := Ty
+    , Tm := Tm
+    , EC := ECtx
+    , ETy := ETy
+    , ETm := ETm
+    , getCtx := Ty.ctx
+    , getTy := Tm.ty
+    , interpCStep := interpCStep
+    , interpTyStep := interpTyStep
+    , interpTmStep := interpTmStep
+    }
+end SetModel