feat: improve error messages for unassigned metavariables

cc @Kha

src/Lean/Elab/App.lean

@@ -206,7 +206,7 @@ private partial def elabAppArgsAux : ElabAppArgsCtx → Expr → Expr → TermEl
       pure ()
     };
     synthesizeAppInstMVars ctx.instMVars;
-    ctx.toSetErrorCtx.forM fun mvarId => registerMVarErrorContext mvarId ctx.ref e;
+    ctx.toSetErrorCtx.forM fun mvarId => registerMVarErrorImplicitArgInfo mvarId ctx.ref e;
     pure e
   };
   eType ← whnfForall eType;

src/Lean/Elab/Binders.lean

@@ -126,6 +126,9 @@ match stx with
     throwUnsupportedSyntax
 | _ => throwUnsupportedSyntax
 
+private def registerFailedToInferBinderTypeInfo (type : Expr) (ref : Syntax) : TermElabM Unit :=
+registerCustomErrorIfMVar type ref "failed to infer binder type"
+
 private partial def elabBinderViews (binderViews : Array BinderView)
     : Nat → Array Expr → LocalContext → LocalInstances → TermElabM (Array Expr × LocalContext × LocalInstances)
 | i, fvars, lctx, localInsts =>
@@ -133,6 +136,7 @@ private partial def elabBinderViews (binderViews : Array BinderView)
     let binderView := binderViews.get ⟨i, h⟩;
     withRef binderView.type $ withLCtx lctx localInsts $ do
       type       ← elabType binderView.type;
+      registerFailedToInferBinderTypeInfo type binderView.type;
       fvarId     ← mkFreshFVarId;
       let fvar  := mkFVar fvarId;
       let fvars := fvars.push fvar;
@@ -316,6 +320,7 @@ private partial def elabFunBinderViews (binderViews : Array BinderView) : Nat
     let binderView := binderViews.get ⟨i, h⟩;
     withRef binderView.type $ withLCtx s.lctx s.localInsts $ do
       type       ← elabType binderView.type;
+      registerFailedToInferBinderTypeInfo type binderView.type;
       checkNoOptAutoParam type;
       fvarId ← mkFreshFVarId;
       let fvar  := mkFVar fvarId;
@@ -447,6 +452,7 @@ def elabLetDeclAux (n : Name) (binders : Array Syntax) (typeStx : Syntax) (valSt
     (expectedType? : Option Expr) (useLetExpr : Bool) : TermElabM Expr := do
 (type, val) ← elabBinders binders $ fun xs => do {
   type ← elabType typeStx;
+  registerCustomErrorIfMVar type typeStx "failed to infer 'let' declaration type";
   val  ← elabTermEnsuringType valStx type;
   type ← mkForallFVars xs type;
   val  ← mkLambdaFVars xs val;

src/Lean/Elab/LetRec.lean

@@ -46,6 +46,7 @@ decls ← (letRec.getArg 1).getArgs.getSepElems.mapM fun attrDeclStx => do {
     let typeStx := expandOptType decl (decl.getArg 2);
     (type, numParams) ← elabBinders binders fun xs => do {
         type ← elabType typeStx;
+        registerCustomErrorIfMVar type typeStx "failed to infer 'let rec' declaration type";
         type ← mkForallFVars xs type;
         pure (type, xs.size)
     };

src/Lean/Elab/MutualDef.lean

@@ -74,16 +74,21 @@ if h : 0 < prevHeaders.size then
 else
   pure ()
 
-private def elabFunType (ref : Syntax) (xs : Array Expr) (view : DefView) : TermElabM Expr :=
+private def registerFailedToInferDefTypeInfo (type : Expr) (ref : Syntax) : TermElabM Unit :=
+registerCustomErrorIfMVar type ref "failed to infer definition type"
+
+private def elabFunType (ref : Syntax) (xs : Array Expr) (view : DefView) : TermElabM Expr := do
 match view.type? with
 | some typeStx => do
   type ← elabType typeStx;
   synthesizeSyntheticMVarsNoPostponing;
   type ← instantiateMVars type;
+  registerFailedToInferDefTypeInfo type typeStx;
   mkForallFVars xs type
 | none => do
   let hole := mkHole ref;
   type ← elabType hole;
+  registerFailedToInferDefTypeInfo type ref;
   mkForallFVars xs type
 
 private def elabHeaders (views : Array DefView) : TermElabM (Array DefViewElabHeader) :=

src/Lean/Elab/PreDefinition/Main.lean

@@ -47,7 +47,7 @@ pure s.result
 
 private def ensureNoUnassignedMVarsAtPreDef (preDef : PreDefinition) : TermElabM Unit := do
 pendingMVarIds ← liftMetaM $ getMVarsAtPreDef preDef;
-foundError ← logUnassignedUsingErrorContext pendingMVarIds;
+foundError ← logUnassignedUsingErrorInfos pendingMVarIds;
 when foundError throwAbort
 
 def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := do

src/Lean/Elab/Tactic/Basic.lean

@@ -176,7 +176,7 @@ pure mvarDecl.userName
 def ensureHasNoMVars (e : Expr) : TacticM Unit := do
 e ← instantiateMVars e;
 pendingMVars ← getMVars e;
-liftM $ Term.logUnassignedUsingErrorContext pendingMVars;
+liftM $ Term.logUnassignedUsingErrorInfos pendingMVars;
 when e.hasExprMVar $ throwError ("tactic failed, resulting expression contains metavariables" ++ indentExpr e)
 
 def withMainMVarContext {α} (x : TacticM α) : TacticM α := do

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -52,7 +52,7 @@ newMVarIds ←
     else do {
       naturalMVarIds ← newMVarIds.filterM fun mvarId => do { mvarDecl ← getMVarDecl mvarId; pure mvarDecl.kind.isNatural };
       syntheticMVarIds ← newMVarIds.filterM fun mvarId => do { mvarDecl ← getMVarDecl mvarId; pure $ !mvarDecl.kind.isNatural };
-      liftM $ Term.logUnassignedUsingErrorContext naturalMVarIds;
+      liftM $ Term.logUnassignedUsingErrorInfos naturalMVarIds;
       pure syntheticMVarIds.toList
     };
 tag ← getMainTag;

src/Lean/Elab/Term.lean

@@ -112,10 +112,15 @@ inductive SyntheticMVarKind
 structure SyntheticMVarDecl :=
 (mvarId : MVarId) (stx : Syntax) (kind : SyntheticMVarKind)
 
-structure MVarErrorContext :=
-(mvarId : MVarId)
-(ref    : Syntax)
-(ctx?   : Option Expr := none)
+inductive MVarErrorKind
+| implicitArg (ctx : Expr)
+| hole
+| custom (msgData : MessageData)
+
+structure MVarErrorInfo :=
+(mvarId    : MVarId)
+(ref       : Syntax)
+(kind      : MVarErrorKind)
 
 structure LetRecToLift :=
 (ref            : Syntax)
@@ -131,7 +136,7 @@ structure LetRecToLift :=
 
 structure State :=
 (syntheticMVars    : List SyntheticMVarDecl := [])
-(mvarErrorContexts : List MVarErrorContext := [])
+(mvarErrorInfos    : List MVarErrorInfo := [])
 (messages          : MessageLog := {})
 (letRecsToLift     : List LetRecToLift := [])
 
@@ -333,59 +338,74 @@ def registerSyntheticMVarWithCurrRef (mvarId : MVarId) (kind : SyntheticMVarKind
 ref ← getRef;
 registerSyntheticMVar ref mvarId kind
 
-def registerMVarErrorContext (mvarId : MVarId) (ref : Syntax) (ctx? : Option Expr := none) : TermElabM Unit := do
-modify fun s => { s with mvarErrorContexts := { mvarId := mvarId, ref := ref, ctx? := ctx? } :: s.mvarErrorContexts }
+def registerMVarErrorHoleInfo (mvarId : MVarId) (ref : Syntax) : TermElabM Unit := do
+modify fun s => { s with mvarErrorInfos := { mvarId := mvarId, ref := ref, kind := MVarErrorKind.hole } :: s.mvarErrorInfos }
 
-def MVarErrorContext.logError (mvarErrorContext : MVarErrorContext) : TermElabM Unit := do
-let optionExprToMessageData (e? : Option Expr) : TermElabM MessageData :=
-  match e? with
-  | none   => pure Format.nil
-  | some e => do {
-    e ← instantiateMVars e;
-    if e.isApp then
-      let f    := e.getAppFn;
-      let args := e.getAppArgs;
-      let msg  := args.foldl
-        (fun (msg : MessageData) (arg : Expr) =>
-          if arg.getAppFn.isMVar then
-            msg ++ " " ++ arg.getAppFn
-          else
-            msg ++ " …")
-        ("@" ++ MessageData.ofExpr f);
-      pure $ MessageData.nestD (Format.line ++ msg)
-    else
-      pure e
-};
-let msg : MessageData := "don't know how to synthesize placeholder";
-ctx ← optionExprToMessageData mvarErrorContext.ctx?;
-let msg := msg ++ ctx;
-let msg := msg ++ Format.line ++ "context:" ++ Format.line ++ MessageData.ofGoal mvarErrorContext.mvarId;
-logErrorAt mvarErrorContext.ref msg
+def registerMVarErrorImplicitArgInfo (mvarId : MVarId) (ref : Syntax) (app : Expr) : TermElabM Unit := do
+modify fun s => { s with mvarErrorInfos := { mvarId := mvarId, ref := ref, kind := MVarErrorKind.implicitArg app } :: s.mvarErrorInfos }
+
+def registerMVarErrorCustomInfo (mvarId : MVarId) (ref : Syntax) (msgData : MessageData) : TermElabM Unit := do
+modify fun s => { s with mvarErrorInfos := { mvarId := mvarId, ref := ref, kind := MVarErrorKind.custom msgData } :: s.mvarErrorInfos }
+
+def registerCustomErrorIfMVar (e : Expr) (ref : Syntax) (msgData : MessageData) : TermElabM Unit :=
+match e.getAppFn with
+| Expr.mvar mvarId _ => registerMVarErrorCustomInfo mvarId ref msgData
+| _ => pure ()
+
+def MVarErrorInfo.logError (mvarErrorInfo : MVarErrorInfo) : TermElabM Unit := do
+match mvarErrorInfo.kind with
+| MVarErrorKind.implicitArg app => do
+  app ← instantiateMVars app;
+  let f    := app.getAppFn;
+  let args := app.getAppArgs;
+  let msg  := args.foldl
+    (fun (msg : MessageData) (arg : Expr) =>
+      if arg.getAppFn.isMVar then
+        msg ++ " " ++ arg.getAppFn
+      else
+        msg ++ " …")
+    ("@" ++ MessageData.ofExpr f);
+  let msg : MessageData := "don't know how to synthesize implicit argument" ++ indentD msg;
+  let msg := msg ++ Format.line ++ "context:" ++ Format.line ++ MessageData.ofGoal mvarErrorInfo.mvarId;
+  logErrorAt mvarErrorInfo.ref msg
+| MVarErrorKind.hole => do
+  let msg : MessageData := "don't know how to synthesize placeholder";
+  let msg := msg ++ Format.line ++ "context:" ++ Format.line ++ MessageData.ofGoal mvarErrorInfo.mvarId;
+  logErrorAt mvarErrorInfo.ref msg
+| MVarErrorKind.custom msgData =>
+  logErrorAt mvarErrorInfo.ref msgData
 
 /--
   Try to log errors for the unassigned metavariables `pendingMVarIds`.
   Return `true` if at least one error was logged.
   Remark: This method only succeeds if we have information for at least one given metavariable
-  at `mvarErrorContexts`. -/
-def logUnassignedUsingErrorContext (pendingMVarIds : Array MVarId) : TermElabM Bool := do
+  at `mvarErrorInfos`. -/
+def logUnassignedUsingErrorInfos (pendingMVarIds : Array MVarId) : TermElabM Bool := do
 s ← get;
-let errorCtxs := s.mvarErrorContexts;
-errorCtxs.foldlM
-  (fun foundError mvarErrorContext => do
-    /- The metavariable `mvarErrorContext.mvarId` may have been assigned or
-       delayed assigned to another metavariable that is unassigned. -/
-    mvarDeps ← getMVars (mkMVar mvarErrorContext.mvarId);
-    if mvarDeps.any pendingMVarIds.contains then do
-      mvarErrorContext.logError;
-      pure true
-    else
-      pure foundError)
-  false
+let errorInfos := s.mvarErrorInfos;
+(foundErrors, _) ← errorInfos.foldlM
+  (fun (acc : Bool × NameSet) mvarErrorInfo => do
+    let (foundErrors, alreadyVisited) := acc;
+    let mvarId := mvarErrorInfo.mvarId;
+    if alreadyVisited.contains mvarId then
+      pure acc
+    else do
+      let alreadyVisited := alreadyVisited.insert mvarId;
+      /- The metavariable `mvarErrorInfo.mvarId` may have been assigned or
+         delayed assigned to another metavariable that is unassigned. -/
+      mvarDeps ← getMVars (mkMVar mvarId);
+      if mvarDeps.any pendingMVarIds.contains then do
+        mvarErrorInfo.logError;
+        pure (true, alreadyVisited)
+      else
+        pure (foundErrors, alreadyVisited))
+  (false, {});
+pure foundErrors
 
-/-- Ensure metavariables registered using `registerMVarErrorContext` (and used in the given declaration) have been assigned. -/
+/-- Ensure metavariables registered using `registerMVarErrorInfos` (and used in the given declaration) have been assigned. -/
 def ensureNoUnassignedMVars (decl : Declaration) : TermElabM Unit := do
 pendingMVarIds ← getMVarsAtDecl decl;
-foundError ← logUnassignedUsingErrorContext pendingMVarIds;
+foundError ← logUnassignedUsingErrorInfos pendingMVarIds;
 when foundError throwAbort
 
 /-
@@ -995,7 +1015,7 @@ fun stx _ => do
 @[builtinTermElab «hole»] def elabHole : TermElab :=
 fun stx expectedType? => do
   mvar ← mkFreshExprMVar expectedType?;
-  registerMVarErrorContext mvar.mvarId! stx;
+  registerMVarErrorHoleInfo mvar.mvarId! stx;
   pure mvar
 
 @[builtinTermElab «syntheticHole»] def elabSyntheticHole : TermElab :=
@@ -1004,7 +1024,7 @@ fun stx expectedType? => do
   let userName := if arg.isIdent then arg.getId else Name.anonymous;
   let mkNewHole : Unit → TermElabM Expr := fun _ => do {
     mvar ← mkFreshExprMVar expectedType? MetavarKind.syntheticOpaque userName;
-    registerMVarErrorContext mvar.mvarId! stx;
+    registerMVarErrorHoleInfo mvar.mvarId! stx;
     pure mvar
   };
   if userName.isAnonymous then

tests/lean/evalWithMVar.lean.expected.out

@@ -1,9 +1,9 @@
 Sum.someRight c : Option Nat
-evalWithMVar.lean:13:6: error: don't know how to synthesize placeholder
+evalWithMVar.lean:13:6: error: don't know how to synthesize implicit argument
   @Sum.someRight ?m … …
 context:
 ⊢ Type _
-evalWithMVar.lean:13:20: error: don't know how to synthesize placeholder
+evalWithMVar.lean:13:20: error: don't know how to synthesize implicit argument
   @c ?m
 context:
 ⊢ Type _

tests/lean/holeErrors.lean

@@ -0,0 +1,20 @@
+new_frontend
+
+def f1 := id
+
+def f2 : _ := id
+
+def f3 :=
+let x := id;
+x
+
+def f4 (x) := x
+
+def f5 (x : _) := x
+
+def f6 :=
+fun x => x
+
+def f7 :=
+let rec x := id;
+10

tests/lean/holeErrors.lean.expected.out

@@ -0,0 +1,28 @@
+holeErrors.lean:3:10: error: don't know how to synthesize implicit argument
+  @id ?m
+context:
+⊢ Sort u_1
+holeErrors.lean:3:7: error: failed to infer definition type
+holeErrors.lean:5:14: error: don't know how to synthesize implicit argument
+  @id ?m
+context:
+⊢ Sort u_1
+holeErrors.lean:5:9: error: failed to infer definition type
+holeErrors.lean:8:9: error: don't know how to synthesize implicit argument
+  @id ?m
+context:
+⊢ Sort u_1
+holeErrors.lean:8:4: error: failed to infer 'let' declaration type
+holeErrors.lean:7:7: error: failed to infer definition type
+holeErrors.lean:11:11: error: failed to infer definition type
+holeErrors.lean:11:7: error: failed to infer binder type
+holeErrors.lean:13:15: error: failed to infer definition type
+holeErrors.lean:13:12: error: failed to infer binder type
+holeErrors.lean:16:4: error: failed to infer binder type
+holeErrors.lean:15:7: error: failed to infer definition type
+holeErrors.lean:19:13: error: don't know how to synthesize implicit argument
+  @id ?m
+context:
+x : ?m → ?m := f7.x
+⊢ Sort u_1
+holeErrors.lean:19:8: error: failed to infer 'let rec' declaration type

tests/lean/holes.lean.expected.out

@@ -10,40 +10,24 @@ context:
 x : Nat
 y : Nat := g x + g x
 ⊢ Nat
-holes.lean:10:15: error: don't know how to synthesize placeholder
+holes.lean:10:15: error: don't know how to synthesize implicit argument
   @g … ?m …
 context:
 x : Nat
 ⊢ Type
-holes.lean:10:9: error: don't know how to synthesize placeholder
+holes.lean:10:9: error: don't know how to synthesize implicit argument
   @g … ?m …
 context:
 x : Nat
 ⊢ Type
-holes.lean:13:7: error: don't know how to synthesize placeholder
-context:
-α : Sort u_1
-⊢ Sort _
-holes.lean:15:16: error: don't know how to synthesize placeholder
-context:
-α : Sort u_1
-⊢ Sort _
-holes.lean:19:0: error: don't know how to synthesize placeholder
+holes.lean:13:7: error: failed to infer binder type
+holes.lean:15:16: error: failed to infer binder type
+holes.lean:19:0: error: don't know how to synthesize implicit argument
   @_uniq.125 … ?m …
 context:
 a : Nat
 f : {α : Type} → {β : ?m a} → α → α := fun {α : Type} (a_1 : α) => a_1
 ⊢ ?m a
-holes.lean:18:6: error: don't know how to synthesize placeholder
-context:
-a : Nat
-α : Type
-⊢ Sort _
-holes.lean:21:25: error: don't know how to synthesize placeholder
-context:
-x : Nat
-⊢ Sort _
-holes.lean:25:8: error: don't know how to synthesize placeholder
-context:
-x y : Nat
-⊢ Sort _
+holes.lean:18:6: error: failed to infer binder type
+holes.lean:21:25: error: failed to infer definition type
+holes.lean:25:8: error: failed to infer 'let rec' declaration type

tests/lean/macroStack.lean.expected.out

@@ -7,9 +7,7 @@ while expanding
 while expanding
   if h : (x > 0) then 1 else 0
 macroStack.lean:11:9: error: invalid use of `(<- ...)`, must be nested inside a 'do' expression
-macroStack.lean:11:6: error: don't know how to synthesize placeholder
-context:
-⊢ Sort u_1
+macroStack.lean:11:6: error: failed to infer definition type
 macroStack.lean:17:0: error: application type mismatch
   x + x✝¹ + x✝
 argument