From b6860968ff3436824221d6ec74c45abd531fecba Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 12 Jul 2022 18:39:30 -0700
Subject: [PATCH] fix: catch exception at `elabMutualDef`

closes #1301
---
 src/Lean/Elab/MutualDef.lean          |  11 ++-
 tests/lean/343.lean.expected.out      |   6 ++
 tests/lean/infoTree.lean.expected.out | 118 ++++++++++++++------------
 tests/lean/rewrite.lean               |   2 +-
 tests/lean/typeMismatch.lean          |   2 +-
 5 files changed, 79 insertions(+), 60 deletions(-)

diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index ca704343cf..7d0eccf1c1 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -777,9 +777,14 @@ where
     withFunLocalDecls headers fun funFVars => do
       for view in views, funFVar in funFVars do
         addLocalVarInfo view.declId funFVar
-      let values ← elabFunValues headers
-      Term.synthesizeSyntheticMVarsNoPostponing
-      let values ← values.mapM (instantiateMVars ·)
+      let values ←
+        try
+          let values ← elabFunValues headers
+          Term.synthesizeSyntheticMVarsNoPostponing
+          values.mapM (instantiateMVars ·)
+        catch ex =>
+          logException ex
+          headers.mapM fun header => mkSorry header.type (synthetic := true)
       let headers ← headers.mapM instantiateMVarsAtHeader
       let letRecsToLift ← getLetRecsToLift
       let letRecsToLift ← letRecsToLift.mapM instantiateMVarsAtLetRecToLift
diff --git a/tests/lean/343.lean.expected.out b/tests/lean/343.lean.expected.out
index dfab828576..b6c0daaf99 100644
--- a/tests/lean/343.lean.expected.out
+++ b/tests/lean/343.lean.expected.out
@@ -5,3 +5,9 @@ while trying to unify
   Catish.Obj Catish.Obj
 with
   CatIsh.{max ?u ?u, max (?u + 1) (?u + 1)}
+343.lean:30:0-30:54: error: failed to solve universe constraint
+  max (?u+1) (?u+1) =?= max (?u+1) (?u+1)
+while trying to unify
+  Catish.Obj : Type (max ((max (u_1 + 1) (u_2 + 1)) + 1) ((max u_3 u_4) + 1))
+with
+  CatIsh : Type (max ((max u_4 u_3) + 1) ((max (u_4 + 1) (u_3 + 1)) + 1))
diff --git a/tests/lean/infoTree.lean.expected.out b/tests/lean/infoTree.lean.expected.out
index f4e8b2d541..4bcbf427f7 100644
--- a/tests/lean/infoTree.lean.expected.out
+++ b/tests/lean/infoTree.lean.expected.out
@@ -388,94 +388,102 @@ bitwise bne
       xor : Nat → Nat → Nat @ ⟨38, 7⟩-⟨38, 10⟩
     command @ ⟨37, 0⟩†-⟨38, 10⟩† @ Lean.Elab.Command.elabEnd
 infoTree.lean:41:0: error: expected identifier or term
-[Elab.info] command @ ⟨39, 0⟩-⟨39, 30⟩ @ no_elab
+[Elab.info] command @ ⟨39, 0⟩-⟨39, 30⟩ @ Lean.Elab.Command.elabDeclaration
+  Inhabited Nat : Type @ ⟨39, 11⟩-⟨39, 24⟩ @ Lean.Elab.Term.elabApp
+    [.] `Inhabited : some Sort.{?_uniq.1173} @ ⟨39, 11⟩-⟨39, 20⟩
+    Inhabited : Type → Type @ ⟨39, 11⟩-⟨39, 20⟩
+    Nat : Type @ ⟨39, 21⟩-⟨39, 24⟩ @ Lean.Elab.Term.elabIdent
+      [.] `Nat : some Sort.{?_uniq.1174} @ ⟨39, 21⟩-⟨39, 24⟩
+      Nat : Type @ ⟨39, 21⟩-⟨39, 24⟩
+  instInhabitedNat_1 (isBinder := true) : Inhabited Nat @ ⟨39, 0⟩†-⟨39, 30⟩†
+  instInhabitedNat_1 (isBinder := true) : Inhabited Nat @ ⟨39, 0⟩-⟨39, 8⟩
 infoTree.lean:44:0: error: expected stx
 [Elab.info] command @ ⟨41, 0⟩-⟨41, 5⟩ @ no_elab
 [Elab.info] command @ ⟨44, 0⟩-⟨44, 22⟩ @ Lean.Elab.Command.elabSetOption
   [.] (Command.set_option "set_option" `pp.raw) @ ⟨44, 0⟩-⟨44, 17⟩
 [Elab.info] command @ ⟨45, 0⟩-⟨47, 8⟩ @ Lean.Elab.Command.elabDeclaration
   Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ @ Lean.Elab.Term.elabIdent
-    [.] `Nat : some Sort.{?_uniq.1173} @ ⟨45, 14⟩-⟨45, 17⟩
+    [.] `Nat : some Sort.{?_uniq.1177} @ ⟨45, 14⟩-⟨45, 17⟩
     Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩
-  _uniq.1174 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
+  _uniq.1178 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
   Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ @ Lean.Elab.Term.elabIdent
-    [.] `Nat : some Sort.{?_uniq.1175} @ ⟨45, 14⟩-⟨45, 17⟩
+    [.] `Nat : some Sort.{?_uniq.1179} @ ⟨45, 14⟩-⟨45, 17⟩
     Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩
-  _uniq.1176 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
-  Eq.{1} Nat _uniq.1174 _uniq.1174 : Prop @ ⟨45, 21⟩-⟨45, 26⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
+  _uniq.1180 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
+  Eq.{1} Nat _uniq.1178 _uniq.1178 : Prop @ ⟨45, 21⟩-⟨45, 26⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
     Macro expansion
     («term_=_» `x "=" `x)
     ===>
-    (Term.binrel "binrel%" `Eq._@.infoTree._hyg.180 `x `x)
-      Eq.{1} Nat _uniq.1174 _uniq.1174 : Prop @ ⟨45, 21⟩†-⟨45, 26⟩ @ Lean.Elab.Term.BinOp.elabBinRel
-        [.] `Eq._@.infoTree._hyg.180 : none @ ⟨45, 21⟩†-⟨45, 26⟩†
-        _uniq.1174 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ @ Lean.Elab.Term.elabIdent
+    (Term.binrel "binrel%" `Eq._@.infoTree._hyg.182 `x `x)
+      Eq.{1} Nat _uniq.1178 _uniq.1178 : Prop @ ⟨45, 21⟩†-⟨45, 26⟩ @ Lean.Elab.Term.BinOp.elabBinRel
+        [.] `Eq._@.infoTree._hyg.182 : none @ ⟨45, 21⟩†-⟨45, 26⟩†
+        _uniq.1178 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ @ Lean.Elab.Term.elabIdent
           [.] `x : none @ ⟨45, 21⟩-⟨45, 22⟩
-          _uniq.1174 : Nat @ ⟨45, 21⟩-⟨45, 22⟩
-        _uniq.1174 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ @ Lean.Elab.Term.elabIdent
+          _uniq.1178 : Nat @ ⟨45, 21⟩-⟨45, 22⟩
+        _uniq.1178 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ @ Lean.Elab.Term.elabIdent
           [.] `x : none @ ⟨45, 25⟩-⟨45, 26⟩
-          _uniq.1174 : Nat @ ⟨45, 25⟩-⟨45, 26⟩
-  _uniq.1180 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨45, 4⟩-⟨45, 6⟩
-  _uniq.1181 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
-  _uniq.1182 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
-  (fun (f7 : forall (x : Nat), Nat -> (Eq.{1} Nat x x)) => [mdata _recApp: f7 _uniq.1181 _uniq.1182]) f6.f7 : Eq.{1} Nat _uniq.1181 _uniq.1181 @ ⟨46, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabLetRec
+          _uniq.1178 : Nat @ ⟨45, 25⟩-⟨45, 26⟩
+  _uniq.1184 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨45, 4⟩-⟨45, 6⟩
+  _uniq.1185 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
+  _uniq.1186 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
+  (fun (f7 : forall (x : Nat), Nat -> (Eq.{1} Nat x x)) => [mdata _recApp: f7 _uniq.1185 _uniq.1186]) f6.f7 : Eq.{1} Nat _uniq.1185 _uniq.1185 @ ⟨46, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabLetRec
     Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ @ Lean.Elab.Term.elabIdent
-      [.] `Nat : some Sort.{?_uniq.1183} @ ⟨46, 20⟩-⟨46, 23⟩
+      [.] `Nat : some Sort.{?_uniq.1187} @ ⟨46, 20⟩-⟨46, 23⟩
       Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩
-    _uniq.1184 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
+    _uniq.1188 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
     Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ @ Lean.Elab.Term.elabIdent
-      [.] `Nat : some Sort.{?_uniq.1185} @ ⟨46, 20⟩-⟨46, 23⟩
+      [.] `Nat : some Sort.{?_uniq.1189} @ ⟨46, 20⟩-⟨46, 23⟩
       Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩
-    _uniq.1186 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
-    Eq.{1} Nat _uniq.1184 _uniq.1184 : Prop @ ⟨46, 27⟩-⟨46, 32⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
+    _uniq.1190 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
+    Eq.{1} Nat _uniq.1188 _uniq.1188 : Prop @ ⟨46, 27⟩-⟨46, 32⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
       Macro expansion
       («term_=_» `x "=" `x)
       ===>
-      (Term.binrel "binrel%" `Eq._@.infoTree._hyg.188 `x `x)
-        Eq.{1} Nat _uniq.1184 _uniq.1184 : Prop @ ⟨46, 27⟩†-⟨46, 32⟩ @ Lean.Elab.Term.BinOp.elabBinRel
-          [.] `Eq._@.infoTree._hyg.188 : none @ ⟨46, 27⟩†-⟨46, 32⟩†
-          _uniq.1184 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ @ Lean.Elab.Term.elabIdent
+      (Term.binrel "binrel%" `Eq._@.infoTree._hyg.190 `x `x)
+        Eq.{1} Nat _uniq.1188 _uniq.1188 : Prop @ ⟨46, 27⟩†-⟨46, 32⟩ @ Lean.Elab.Term.BinOp.elabBinRel
+          [.] `Eq._@.infoTree._hyg.190 : none @ ⟨46, 27⟩†-⟨46, 32⟩†
+          _uniq.1188 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ @ Lean.Elab.Term.elabIdent
             [.] `x : none @ ⟨46, 27⟩-⟨46, 28⟩
-            _uniq.1184 : Nat @ ⟨46, 27⟩-⟨46, 28⟩
-          _uniq.1184 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ @ Lean.Elab.Term.elabIdent
+            _uniq.1188 : Nat @ ⟨46, 27⟩-⟨46, 28⟩
+          _uniq.1188 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ @ Lean.Elab.Term.elabIdent
             [.] `x : none @ ⟨46, 31⟩-⟨46, 32⟩
-            _uniq.1184 : Nat @ ⟨46, 31⟩-⟨46, 32⟩
-    _uniq.1191 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩
-    _uniq.1192 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
-    _uniq.1193 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
-    Eq.refl.{1} Nat _uniq.1192 : Eq.{1} Nat _uniq.1192 _uniq.1192 @ ⟨46, 36⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabApp
-      [.] `Eq.refl : some Eq.{?_uniq.1188} Nat _uniq.1192 _uniq.1192 @ ⟨46, 36⟩-⟨46, 43⟩
+            _uniq.1188 : Nat @ ⟨46, 31⟩-⟨46, 32⟩
+    _uniq.1195 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩
+    _uniq.1196 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
+    _uniq.1197 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
+    Eq.refl.{1} Nat _uniq.1196 : Eq.{1} Nat _uniq.1196 _uniq.1196 @ ⟨46, 36⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabApp
+      [.] `Eq.refl : some Eq.{?_uniq.1192} Nat _uniq.1196 _uniq.1196 @ ⟨46, 36⟩-⟨46, 43⟩
       Eq.refl.{1} : forall {α : Type} (a : α), Eq.{1} α a a @ ⟨46, 36⟩-⟨46, 43⟩
-      _uniq.1192 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabIdent
-        [.] `x : some ?_uniq.1195 @ ⟨46, 44⟩-⟨46, 45⟩
-        _uniq.1192 : Nat @ ⟨46, 44⟩-⟨46, 45⟩
-    [mdata _recApp: _uniq.1191 _uniq.1181 _uniq.1182] : Eq.{1} Nat _uniq.1181 _uniq.1181 @ ⟨47, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabApp
-      [.] `f7 : some Eq.{1} Nat _uniq.1181 _uniq.1181 @ ⟨47, 2⟩-⟨47, 4⟩
-      _uniq.1191 : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨47, 2⟩-⟨47, 4⟩
-      _uniq.1181 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ @ Lean.Elab.Term.elabIdent
+      _uniq.1196 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabIdent
+        [.] `x : some ?_uniq.1199 @ ⟨46, 44⟩-⟨46, 45⟩
+        _uniq.1196 : Nat @ ⟨46, 44⟩-⟨46, 45⟩
+    [mdata _recApp: _uniq.1195 _uniq.1185 _uniq.1186] : Eq.{1} Nat _uniq.1185 _uniq.1185 @ ⟨47, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabApp
+      [.] `f7 : some Eq.{1} Nat _uniq.1185 _uniq.1185 @ ⟨47, 2⟩-⟨47, 4⟩
+      _uniq.1195 : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨47, 2⟩-⟨47, 4⟩
+      _uniq.1185 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ @ Lean.Elab.Term.elabIdent
         [.] `x : some Nat @ ⟨47, 5⟩-⟨47, 6⟩
-        _uniq.1181 : Nat @ ⟨47, 5⟩-⟨47, 6⟩
-      _uniq.1182 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabIdent
+        _uniq.1185 : Nat @ ⟨47, 5⟩-⟨47, 6⟩
+      _uniq.1186 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabIdent
         [.] `y : some Nat @ ⟨47, 7⟩-⟨47, 8⟩
-        _uniq.1182 : Nat @ ⟨47, 7⟩-⟨47, 8⟩
+        _uniq.1186 : Nat @ ⟨47, 7⟩-⟨47, 8⟩
   f6.f7 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩
   f6 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨45, 4⟩-⟨45, 6⟩
 [Elab.info] command @ ⟨50, 0⟩-⟨50, 32⟩ @ Lean.Elab.Command.elabDeclaration
   B : Type @ ⟨50, 12⟩-⟨50, 13⟩ @ Lean.Elab.Term.elabIdent
-    [.] `B : some Sort.{?_uniq.1215} @ ⟨50, 12⟩-⟨50, 13⟩
+    [.] `B : some Sort.{?_uniq.1219} @ ⟨50, 12⟩-⟨50, 13⟩
     B : Type @ ⟨50, 12⟩-⟨50, 13⟩
-  _uniq.1216 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
+  _uniq.1220 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
   B : Type @ ⟨50, 17⟩-⟨50, 18⟩ @ Lean.Elab.Term.elabIdent
-    [.] `B : some Sort.{?_uniq.1217} @ ⟨50, 17⟩-⟨50, 18⟩
+    [.] `B : some Sort.{?_uniq.1221} @ ⟨50, 17⟩-⟨50, 18⟩
     B : Type @ ⟨50, 17⟩-⟨50, 18⟩
-  _uniq.1218 (isBinder := true) : B -> B @ ⟨50, 4⟩-⟨50, 6⟩
-  _uniq.1219 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
-  B.mk (B.pair _uniq.1219) : B @ ⟨50, 22⟩-⟨50, 32⟩ @ Lean.Elab.Term.StructInst.elabStructInst
-    _uniq.1219 : B @ ⟨50, 24⟩-⟨50, 25⟩
-    B.pair _uniq.1219 : Prod.{0 0} A A @ ⟨50, 24⟩-⟨50, 25⟩† @ Lean.Elab.Term.elabProj
+  _uniq.1222 (isBinder := true) : B -> B @ ⟨50, 4⟩-⟨50, 6⟩
+  _uniq.1223 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
+  B.mk (B.pair _uniq.1223) : B @ ⟨50, 22⟩-⟨50, 32⟩ @ Lean.Elab.Term.StructInst.elabStructInst
+    _uniq.1223 : B @ ⟨50, 24⟩-⟨50, 25⟩
+    B.pair _uniq.1223 : Prod.{0 0} A A @ ⟨50, 24⟩-⟨50, 25⟩† @ Lean.Elab.Term.elabProj
       [.] `b : some Prod.{0 0} A A @ ⟨50, 24⟩-⟨50, 25⟩
-      _uniq.1219 : B @ ⟨50, 24⟩-⟨50, 25⟩
-      [.] _uniq.1219 : B @ ⟨50, 24⟩-⟨50, 25⟩ : some Prod.{0 0} A A
+      _uniq.1223 : B @ ⟨50, 24⟩-⟨50, 25⟩
+      [.] _uniq.1223 : B @ ⟨50, 24⟩-⟨50, 25⟩ : some Prod.{0 0} A A
       B.pair : B -> (Prod.{0 0} A A) @ ⟨50, 24⟩†-⟨50, 25⟩†
-    pair : Prod.{0 0} A A := B.pair _uniq.1219 @ ⟨50, 22⟩†-⟨50, 32⟩
+    pair : Prod.{0 0} A A := B.pair _uniq.1223 @ ⟨50, 22⟩†-⟨50, 32⟩
   f7 (isBinder := true) : B -> B @ ⟨50, 4⟩-⟨50, 6⟩
diff --git a/tests/lean/rewrite.lean b/tests/lean/rewrite.lean
index d49f2b4bec..446dae0ad4 100644
--- a/tests/lean/rewrite.lean
+++ b/tests/lean/rewrite.lean
@@ -14,7 +14,7 @@ done
 
 axiom zeroAdd (x : Nat) : 0 + x = x
 
-theorem ex2 (x y z) (h₁ : 0 + x = y) (h₂ : 0 + y = z) : x = z := by
+theorem ex2a (x y z) (h₁ : 0 + x = y) (h₂ : 0 + y = z) : x = z := by
 rewrite [zeroAdd] at h₁ h₂;
 trace_state;
 subst x;
diff --git a/tests/lean/typeMismatch.lean b/tests/lean/typeMismatch.lean
index a8e9bdd539..0f34c20315 100644
--- a/tests/lean/typeMismatch.lean
+++ b/tests/lean/typeMismatch.lean
@@ -8,5 +8,5 @@ IO.println ""
 
 open Lean
 
-def test (x : Expr) : MetaM Unit :=
+def test2 (x : Expr) : MetaM Unit :=
 Meta.isDefEq x x