fix: register new metavariables created when applying default instance

closes #353

src/Lean/Elab/SyntheticMVars.lean

@@ -95,7 +95,11 @@ private def synthesizePendingCoeInstMVar
       | Exception.error _ msg => throwTypeMismatchError errorMsgHeader? expectedType eType e f? msg
       | _                     => unreachable!
 
-private def tryToSynthesizeUsingDefaultInstance (mvarId : MVarId) (defaultInstance : Name) : MetaM (Option (List SyntheticMVarDecl)) :=
+/--
+  Try to synthesize a value for `mvarId` using the given default instance.
+  Return `some (val, mvarDecls)` if successful, where `val` is the value assigned to `mvarId`, and `mvarDecls` is a list of new type class instances that need to be synthesized.
+-/
+private def tryToSynthesizeUsingDefaultInstance (mvarId : MVarId) (defaultInstance : Name) : TermElabM (Option (Expr × List SyntheticMVarDecl)) :=
   commitWhenSome? do
     let constInfo ← getConstInfo defaultInstance
     let candidate := Lean.mkConst defaultInstance (← mkFreshLevelMVars constInfo.levelParams.length)
@@ -109,11 +113,11 @@ private def tryToSynthesizeUsingDefaultInstance (mvarId : MVarId) (defaultInstan
         if bis[i] == BinderInfo.instImplicit then
            result := { mvarId := mvars[i].mvarId!, stx := (← getRef), kind := SyntheticMVarKind.typeClass } :: result
       trace[Elab.resume] "worked"
-      return some result
+      return some (candidate, result)
     else
       return none
 
-private def tryToSynthesizeUsingDefaultInstances (mvarId : MVarId) (prio : Nat) : MetaM (Option (List SyntheticMVarDecl)) :=
+private def tryToSynthesizeUsingDefaultInstances (mvarId : MVarId) (prio : Nat) : TermElabM (Option (Expr × List SyntheticMVarDecl)) :=
   withMVarContext mvarId do
     let mvarType := (← Meta.getMVarDecl mvarId).type
     match (← isClass? mvarType) with
@@ -125,7 +129,7 @@ private def tryToSynthesizeUsingDefaultInstances (mvarId : MVarId) (prio : Nat)
         for (defaultInstance, instPrio) in defaultInstances do
           if instPrio == prio then
             match (← tryToSynthesizeUsingDefaultInstance mvarId defaultInstance) with
-            | some newMVarDecls => return some newMVarDecls
+            | some result => return some result
             | none => continue
         return none
 
@@ -139,7 +143,10 @@ private def synthesizeUsingDefaultPrio (prio : Nat) : TermElabM Bool := do
       | SyntheticMVarKind.typeClass =>
         match (← withRef mvarDecl.stx <| tryToSynthesizeUsingDefaultInstances mvarDecl.mvarId prio) with
         | none => visit mvarDecls (mvarDecl :: syntheticMVarsNew)
-        | some newMVarDecls =>
+        | some (val, newMVarDecls) =>
+          for newMVarDecl in newMVarDecls do
+            -- Register that `newMVarDecl.mvarId`s are implicit arguments of the value assigned to `mvarDecl.mvarId`
+            registerMVarErrorImplicitArgInfo newMVarDecl.mvarId (← getRef) val
           let syntheticMVarsNew := newMVarDecls ++ syntheticMVarsNew
           let syntheticMVarsNew := mvarDecls.reverse ++ syntheticMVarsNew
           modify fun s => { s with syntheticMVars := syntheticMVarsNew }

tests/lean/353.lean

@@ -0,0 +1,13 @@
+class ArrSort (α : Sort u1) where
+  Arr : α → α → Sort u2
+class Arr (α : Sort u1) (γ : Sort u2) where
+  Arr : α → α → γ
+infix:70 " ~> " => Arr.Arr
+@[defaultInstance]
+instance inst1 {α : Sort _} [ArrSort α] : Arr α (Sort _) := { Arr := ArrSort.Arr }
+instance inst2 : ArrSort Prop := { Arr := λ a b => a → b }
+
+set_option pp.all true
+set_option trace.Meta.debug true
+structure Function' where
+  map : ∀ {a₁ a₂ : Bool}, (a₁ ~> a₂) ~> (a₁ ~> a₂)

tests/lean/353.lean.expected.out

@@ -0,0 +1,4 @@
+353.lean:13:27-13:35: error: failed to synthesize instance
+  ArrSort.{1, ?u} Bool
+353.lean:13:41-13:49: error: failed to synthesize instance
+  Arr.{1, ?u + 1} Bool (Sort ?u)