fix: fixes #448

src/library/compiler/eager_lambda_lifting.cpp

@@ -139,13 +139,17 @@ class eager_lambda_lifting_fn {
                             ok = false;
                             return false;
                         } else {
-                            if (!collect_fvars_core(d.get_type(), collected, fvars))
+                            if (!collect_fvars_core(d.get_type(), collected, fvars)) {
+                                ok = false;
                                 return false;
+                            }
                             if (m_closed_fvars.contains(fvar_name(x))) {
                                 /* If x only depends on global constants and other variables in m_closed_fvars.
                                    Then, we also collect the other variables at m_closed_fvars. */
-                                if (!collect_fvars_core(*d.get_value(), collected, fvars))
+                                if (!collect_fvars_core(*d.get_value(), collected, fvars)) {
+                                    ok = false;
                                     return false;
+                                }
                             }
                             fvars.push_back(x);
                         }

tests/lean/448.lean

@@ -0,0 +1,35 @@
+namespace TryCatchWithAutolift
+
+structure M (α : Type) where
+  σ : ExceptT String IO α
+
+instance : Monad M where
+  pure x   := { σ := pure x }
+  bind x f := { σ := do (f (← x.σ)).σ }
+  map f x  := { σ := do f (← x.σ) }
+
+instance : MonadLiftT IO M where
+  monadLift {α : Type} (act : IO α) : M α :=
+    { σ := monadLift act }
+
+instance : MonadFinally M where
+  tryFinally' := fun x h => M.mk do
+    tryFinally' x.σ fun e => (h e).σ
+
+def t : M Unit := do
+  liftM $ IO.println "bad"
+  try do pure () -- Error
+  catch ex : IO.Error => do pure ()
+  finally do pure ()
+
+instance : MonadExceptOf IO.Error M where
+  throw e := { σ := throwThe IO.Error e }
+  tryCatch x handle := { σ := tryCatchThe IO.Error x.σ fun e => handle e |>.σ }
+
+def t2 : M Unit := do
+  liftM $ IO.println "bad"
+  try do pure ()
+  catch ex : IO.Error => do pure ()
+  finally do pure ()
+
+end TryCatchWithAutolift

tests/lean/448.lean.expected.out

@@ -0,0 +1,2 @@
+448.lean:21:2-23:20: error: failed to synthesize instance
+  MonadExceptOf IO.Error M