fix Meta.trySynthInstance

Auto/Lib/MetaExtra.lean

@@ -44,13 +44,13 @@ def Meta.trySynthInhabited (e : Expr) : MetaM (Option Expr) := do
   try
     if let .some inh ← Meta.synthInstance? e then
       return .some inh
+    if let .some inh ← Meta.synthInstance? (Lean.mkApp (.const ``Inhabited [lvl]) e) then
+      return .some (Lean.mkApp2 (.const ``Inhabited.default [lvl]) e inh)
+    if let .some inh ← Meta.synthInstance? (Lean.mkApp (.const ``Nonempty [lvl]) e) then
+      return .some (Lean.mkApp2 (.const ``Classical.choice [lvl]) e inh)
+    return .none
   catch _ =>
-    pure .unit
-  if let .some inh ← Meta.synthInstance? (Lean.mkApp (.const ``Inhabited [lvl]) e) then
-    return .some (Lean.mkApp2 (.const ``Inhabited.default [lvl]) e inh)
-  if let .some inh ← Meta.synthInstance? (Lean.mkApp (.const ``Nonempty [lvl]) e) then
-    return .some (Lean.mkApp2 (.const ``Classical.choice [lvl]) e inh)
-  return .none
+    return .none
 
 syntax (name := fromMetaTactic) "fromMetaTactic" "[" ident "]" : tactic
 
@@ -119,4 +119,4 @@ def Meta.isTypeCorrectCore (e : Expr) : MetaM Bool := do
     trace[auto.metaExtra] msg
     pure false
 
-end Auto
+end Auto

Test/Bugs.lean

@@ -26,6 +26,3 @@ set_option trace.auto.mono true
 
 example (h1 : ∀ x : Nat, x > 0 → ∃ y : Fin x, y.1 = 0) (h2 : 3 > 0) : ∃ z : Fin 3, z.1 = 0 := by
   auto
-
-example : @Auto.Embedding.forallF Nat = @Auto.Embedding.forallF Nat := by
-  auto