feat: report errors for unassigned metavariables

We were not reporting unassigned metavariables due to
1- `_`
2- Named holes (e.g., `?x`)
3- Implicit arguments

src/Lean/Elab/App.lean

@@ -99,6 +99,7 @@ structure ElabAppArgsCtx :=
 (namedArgs     : Array NamedArg)      -- remaining named arguments to be processed
 (instMVars     : Array MVarId := #[]) -- metavariables for the instance implicit arguments that have already been processed
 (typeMVars     : Array MVarId := #[]) -- metavariables for implicit arguments of the form `{α : Sort u}` that have already been processed
+(toSetErrorCtx : Array MVarId := #[]) -- metavariables that we need the set the error context using the application being built
 (foundExplicit : Bool := false)       -- true if an explicit argument has already been processed
 
 /- Auxiliary function for retrieving the resulting type of a function application.
@@ -208,6 +209,7 @@ private partial def elabAppArgsAux : ElabAppArgsCtx → Expr → Expr → TermEl
       pure ()
     };
     synthesizeAppInstMVars ctx.instMVars;
+    ctx.toSetErrorCtx.forM fun mvarId => registerMVarErrorContext mvarId ctx.ref e;
     pure e
   };
   eType ← whnfForall eType;
@@ -258,8 +260,7 @@ private partial def elabAppArgsAux : ElabAppArgsCtx → Expr → Expr → TermEl
           else do
             a ← mkFreshExprMVar d;
             typeMVars ← condM (isTypeFormer a) (pure $ ctx.typeMVars.push a.mvarId!) (pure ctx.typeMVars);
-            elabAppArgsAux { ctx with typeMVars := typeMVars } (mkApp e a) (b.instantiate1 a)
-
+            elabAppArgsAux { ctx with typeMVars := typeMVars, toSetErrorCtx := ctx.toSetErrorCtx.push a.mvarId! } (mkApp e a) (b.instantiate1 a)
         | BinderInfo.instImplicit =>
           if ctx.explicit && nextArgIsHole ctx then do
             /- Recall that if '@' has been used, and the argument is '_', then we still use

src/Lean/Elab/Command.lean

@@ -243,14 +243,16 @@ s ← get; liftTermElabM declName? (Term.elabBinders (getVarDecls s) elabFn)
 def logException (ex : Exception) : CommandElabM Unit := do
 match ex with
 | Exception.error ref msg => withRef ref $ logError msg
-| Exception.internal id   => do
-  name ← liftIO $ id.getName;
-  logError ("internal exception: " ++ name)
+| Exception.internal id   =>
+  unless (id == abortExceptionId) do
+    name ← liftIO $ id.getName;
+    logError ("internal exception: " ++ name)
 
 @[inline] def withLogging (x : CommandElabM Unit) : CommandElabM Unit :=
-catch x (fun ex => match ex with
-  | Exception.error _ _ => do logException ex; pure ()
-  | _                   => unreachable!)
+catch x
+  (fun ex => match ex with
+    | Exception.error _ _  => logException ex
+    | Exception.internal _ => pure ()) -- ignore internal exceptions
 
 @[inline] def catchExceptions (x : CommandElabM Unit) : CommandElabCoreM Empty Unit :=
 fun ctx ref => EIO.catchExceptions (withLogging x ctx ref) (fun _ => pure ())
@@ -508,7 +510,7 @@ fun stx => do
   let term := stx.getArg 1;
   withoutModifyingEnv $ runTermElabM (some `_check) $ fun _ => do
     e    ← Term.elabTerm term none;
-    Term.synthesizeSyntheticMVars false;
+    Term.synthesizeSyntheticMVarsNoPostponing;
     type ← inferType e;
     logInfo (e ++ " : " ++ type);
     pure ()
@@ -556,7 +558,7 @@ fun stx => withoutModifyingEnv do
   let elabMetaEval : CommandElabM Unit := do {
     act : IO Environment ← runTermElabM (some n) fun _ => do {
       e    ← Term.elabTerm term none;
-      Term.synthesizeSyntheticMVars false;
+      Term.synthesizeSyntheticMVarsNoPostponing;
         e ← withLocalDeclD `env (mkConst `Lean.Environment) fun env =>
           withLocalDeclD `opts (mkConst `Lean.Options) fun opts => do {
             e ← mkAppM `Lean.MetaHasEval.eval #[env, opts, e, toExpr false];
@@ -580,7 +582,7 @@ fun stx => withoutModifyingEnv do
     -- modify e to `HasEval.eval (hideUnit := false) e`
     act : IO Unit ← runTermElabM (some n) fun _ => do {
       e    ← Term.elabTerm term none;
-      Term.synthesizeSyntheticMVars false;
+      Term.synthesizeSyntheticMVarsNoPostponing;
       e ← mkAppM `Lean.HasEval.eval #[e, toExpr false];
       addAndCompile e;
       env ← getEnv;
@@ -607,7 +609,7 @@ fun stx => do
   let term := stx.getArg 1;
   withoutModifyingEnv $ runTermElabM `_synth_cmd $ fun _ => do
     inst ← Term.elabTerm term none;
-    Term.synthesizeSyntheticMVars false;
+    Term.synthesizeSyntheticMVarsNoPostponing;
     inst ← instantiateMVars inst;
     val  ← synthInstance inst;
     logInfo val;

src/Lean/Elab/Declaration.lean

@@ -88,7 +88,7 @@ withDeclId declId $ fun name => do
   runTermElabM declName $ fun vars => Term.elabBinders binders.getArgs $ fun xs => do
     applyAttributes declName modifiers.attrs AttributeApplicationTime.beforeElaboration;
     type ← Term.elabType typeStx;
-    Term.synthesizeSyntheticMVars false;
+    Term.synthesizeSyntheticMVarsNoPostponing;
     type ← instantiateMVars type;
     type ← mkForallFVars xs type;
     (type, _) ← mkForallUsedOnly vars type;
@@ -103,7 +103,7 @@ withDeclId declId $ fun name => do
         type     := type,
         isUnsafe := modifiers.isUnsafe
       };
-      -- ensureNoUnassignedMVars decl; -- TODO
+      Term.ensureNoUnassignedMVars decl;
       addDecl decl;
       applyAttributes declName modifiers.attrs AttributeApplicationTime.afterTypeChecking;
       applyAttributes declName modifiers.attrs AttributeApplicationTime.afterCompilation

src/Lean/Elab/Definition.lean

@@ -66,7 +66,7 @@ def mkDef? (view : DefView) (declName : Name) (scopeLevelNames allUserLevelNames
 withRef view.ref do
 Term.synthesizeSyntheticMVars;
 val     ← withRef view.val $ Term.ensureHasType type val;
-Term.synthesizeSyntheticMVars false;
+Term.synthesizeSyntheticMVarsNoPostponing;
 type    ← instantiateMVars type;
 val     ← instantiateMVars val;
 if view.kind.isExample then pure none
@@ -132,7 +132,7 @@ withDeclId view.declId $ fun name => do
     decl? ← match view.type? with
       | some typeStx => do
         type ← Term.elabType typeStx;
-        Term.synthesizeSyntheticMVars false;
+        Term.synthesizeSyntheticMVarsNoPostponing;
         type ← instantiateMVars type;
         withUsedWhen' vars xs type view.kind.isTheorem $ fun vars => do
           val  ← elabDefVal view.val type;
@@ -145,7 +145,7 @@ withDeclId view.declId $ fun name => do
     match decl? with
     | none      => pure ()
     | some decl => do
-      -- ensureNoUnassignedMVars decl; -- TODO
+      Term.ensureNoUnassignedMVars decl;
       addDecl decl;
       applyAttributes declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking;
       compileDecl decl;

src/Lean/Elab/Exception.lean

@@ -20,12 +20,21 @@ registerInternalExceptionId `unsupportedSyntax
 @[init registerUnsupportedSyntaxId]
 constant unsupportedSyntaxExceptionId : InternalExceptionId := arbitrary _
 
+def registerAbortElabId : IO InternalExceptionId :=
+registerInternalExceptionId `abortElab
+@[init registerAbortElabId]
+constant abortExceptionId : InternalExceptionId := arbitrary _
+
 def throwPostpone {α m} [MonadExcept Exception m] : m α :=
 throw $ Exception.internal postponeExceptionId
 
 def throwUnsupportedSyntax {α m} [MonadExcept Exception m] : m α :=
 throw $ Exception.internal unsupportedSyntaxExceptionId
 
+-- Throw exception to abort elaboration without producing any error message
+def throwAbort {α m} [MonadExcept Exception m] : m α :=
+throw $ Exception.internal abortExceptionId
+
 def mkMessageCore (fileName : String) (fileMap : FileMap) (msgData : MessageData) (severity : MessageSeverity) (pos : String.Pos) : Message :=
 let pos := fileMap.toPosition pos;
 { fileName := fileName, pos := pos, data := msgData, severity := severity }

src/Lean/Elab/Inductive.lean

@@ -469,7 +469,7 @@ adaptReader (fun (ctx : Term.Context) => { ctx with levelNames := allUserLevelNa
         pure (indType :: indTypes))
       [];
     let indTypes := indTypes.reverse;
-    Term.synthesizeSyntheticMVars false;  -- resolve pending
+    Term.synthesizeSyntheticMVarsNoPostponing;
     u ← getResultingUniverse indTypes;
     inferLevel ← shouldInferResultUniverse u;
     withUsed vars indTypes $ fun vars => do
@@ -484,7 +484,7 @@ adaptReader (fun (ctx : Term.Context) => { ctx with levelNames := allUserLevelNa
         indTypes ← replaceIndFVarsWithConsts views indFVars levelParams numParams indTypes;
         let indTypes := applyInferMod views numParams indTypes;
         let decl := Declaration.inductDecl levelParams numParams indTypes isUnsafe;
-        -- ensureNoUnassignedMVars decl -- TODO
+        Term.ensureNoUnassignedMVars decl;
         addDecl decl;
         mkAuxConstructions views;
         -- We need to invoke `applyAttributes` because `class` is implemented as an attribute.

src/Lean/Elab/LetRec.lean

@@ -108,7 +108,7 @@ decls ← withSynthesize do {
   headers ← mkLetRecDeclHeaders view;
   withAuxLocalDecls headers fun _ => do
     values ← elabLetRecDeclValues view headers;
-    synthesizeSyntheticMVars false;
+    synthesizeSyntheticMVarsNoPostponing;
     -- We abort if there are synthetic sorry's
     values.forM abortIfContainsSyntheticSorry;
     headers.forM fun header => abortIfContainsSyntheticSorry header.type;

src/Lean/Elab/Structure.lean

@@ -454,7 +454,7 @@ unless (validStructType type) $ throwErrorAt view.type "expected Type";
 withRef view.ref do
 withParents view 0 #[] fun fieldInfos =>
 withFields view.fields 0 fieldInfos fun fieldInfos => do
-  Term.synthesizeSyntheticMVars false;  -- resolve pending
+  Term.synthesizeSyntheticMVarsNoPostponing;
   u ← getResultUniverse type;
   inferLevel ← shouldInferResultUniverse u;
   withUsed view.scopeVars view.params fieldInfos $ fun scopeVars => do
@@ -471,7 +471,7 @@ withFields view.fields 0 fieldInfos fun fieldInfos => do
       type ← instantiateMVars type;
       let indType := { name := view.declName, type := type, ctors := [ctor] : InductiveType };
       let decl    := Declaration.inductDecl levelParams params.size [indType] view.modifiers.isUnsafe;
-      -- ensureNoUnassignedMVars decl -- TODO
+      Term.ensureNoUnassignedMVars decl;
       addDecl decl;
       let projInfos := (fieldInfos.filter fun (info : StructFieldInfo) => !info.isFromParent).toList.map fun (info : StructFieldInfo) =>
         { declName := info.declName, inferMod := info.inferMod : ProjectionInfo };

src/Lean/Elab/SyntheticMVars.lean

@@ -233,7 +233,7 @@ modify fun s => { s with syntheticMVars := [] };
 finally
   (do
      a ← k;
-     synthesizeSyntheticMVars false;
+     synthesizeSyntheticMVarsNoPostponing;
      pure a)
   (modify fun s => { s with syntheticMVars := s.syntheticMVars ++ syntheticMVarsSaved })
 

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -62,7 +62,7 @@ fun stx => match_syntax stx with
       decl ← getMVarDecl g;
       val  ← elabTerm e none true;
       gs'  ← liftMetaM $ Meta.apply g val;
-      liftTermElabM $ Term.synthesizeSyntheticMVars false;
+      liftTermElabM $ Term.synthesizeSyntheticMVarsNoPostponing;
       pure gs'
     };
     -- TODO: handle optParam and autoParam

src/Lean/Elab/Term.lean

@@ -8,6 +8,7 @@ import Lean.Structure
 import Lean.Meta.ExprDefEq
 import Lean.Meta.AppBuilder
 import Lean.Meta.SynthInstance
+import Lean.Meta.CollectMVars
 import Lean.Meta.Tactic.Util
 import Lean.Hygiene
 import Lean.Util.RecDepth
@@ -61,12 +62,18 @@ inductive SyntheticMVarKind
 structure SyntheticMVarDecl :=
 (mvarId : MVarId) (stx : Syntax) (kind : SyntheticMVarKind)
 
+structure MVarErrorContext :=
+(mvarId : MVarId)
+(ref    : Syntax)
+(ctx?   : Option Expr := none)
+
 structure State :=
-(syntheticMVars  : List SyntheticMVarDecl := [])
-(messages        : MessageLog := {})
-(instImplicitIdx : Nat := 1)
-(anonymousIdx    : Nat := 1)
-(nextMacroScope  : Nat := firstFrontendMacroScope + 1)
+(syntheticMVars    : List SyntheticMVarDecl := [])
+(mvarErrorContexts : List MVarErrorContext := [])
+(messages          : MessageLog := {})
+(instImplicitIdx   : Nat := 1)
+(anonymousIdx      : Nat := 1)
+(nextMacroScope    : Nat := firstFrontendMacroScope + 1)
 
 instance State.inhabited : Inhabited State := ⟨{}⟩
 
@@ -287,6 +294,53 @@ 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 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;
+withRef mvarErrorContext.ref $ logError msg
+
+/-- Ensure metavariables registered using `registerMVarErrorContext` (and used in the given declaration) have been assigned. -/
+def ensureNoUnassignedMVars (decl : Declaration) : TermElabM Unit := do
+pendingMVarIds ← getMVarsAtDecl decl;
+s ← get;
+let errorCtxs := s.mvarErrorContexts;
+foundError ← 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;
+when foundError throwAbort
+
 /-
   Execute `x` without allowing it to postpone elaboration tasks.
   That is, `tryPostpone` is a noop. -/
@@ -644,9 +698,10 @@ match expectedType? with
 def logException (ex : Exception) : TermElabM Unit := do
 match ex with
 | Exception.error ref msg => withRef ref $ logError msg
-| Exception.internal id   => do
-  name ← liftIO $ id.getName;
-  logError ("internal exception: " ++ name)
+| Exception.internal id   =>
+  unless (id == abortExceptionId) do
+    name ← liftIO $ id.getName;
+    logError ("internal exception: " ++ name)
 
 private def exceptionToSorry (ex : Exception) (expectedType? : Option Expr) : TermElabM Expr := do
 expectedType : Expr ← match expectedType? with
@@ -930,12 +985,17 @@ fun stx _ => do
   pure $ mkSort (mkLevelSucc u)
 
 @[builtinTermElab «hole»] def elabHole : TermElab :=
-fun stx expectedType? => mkFreshExprMVar expectedType?
+fun stx expectedType? => do
+  mvar ← mkFreshExprMVar expectedType?;
+  registerMVarErrorContext mvar.mvarId! stx;
+  pure mvar
 
 @[builtinTermElab «namedHole»] def elabNamedHole : TermElab :=
-fun stx expectedType? =>
+fun stx expectedType? => do
   let name := stx.getIdAt 1;
-  mkFreshExprMVar expectedType? MetavarKind.syntheticOpaque name
+  mvar ← mkFreshExprMVar expectedType? MetavarKind.syntheticOpaque name;
+  registerMVarErrorContext mvar.mvarId! stx;
+  pure mvar
 
 def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr := do
 mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque `main;

tests/lean/doSeqRightIssue.lean.expected.out

@@ -1,3 +1,40 @@
 doSeqRightIssue.lean:5:24: error: unknown universe level v
 doSeqRightIssue.lean:5:24: error: unknown universe level v
-doSeqRightIssue.lean:7:8: error: (kernel) declaration has metavariables ex
+doSeqRightIssue.lean:7:8: error: don't know how to synthesize placeholder
+context:
+p₁ p₂ : (sorryAx (Sort u_1))
+h₁ : (sorryAx ?m.319)=(sorryAx ?m.319)
+h : (sorryAx (?m.320 _))≅_
+_a_1 _a_2 : (sorryAx (Sort u_1))
+_a_3 : (sorryAx ?m.319)=(sorryAx ?m.319)
+⊢ Prop
+doSeqRightIssue.lean:7:8: error: don't know how to synthesize placeholder
+context:
+p₁ p₂ : (sorryAx (Sort u_1))
+h₁ : (sorryAx ?m.319)=(sorryAx ?m.319)
+h : (sorryAx (?m.320 _))≅_
+_a_1 _a_2 : (sorryAx (Sort u_1))
+⊢ Prop
+doSeqRightIssue.lean:7:66: error: don't know how to synthesize placeholder
+  @HEq ?m.320 … … …
+context:
+α : Type u
+β : α → (sorryAx (Sort ?))
+p₁ p₂ : (sorryAx (Sort u_1))
+h₁ : (sorryAx ?m.319)=(sorryAx ?m.319)
+⊢ Prop
+doSeqRightIssue.lean:7:66: error: don't know how to synthesize placeholder
+  @HEq ?m.320 … … …
+context:
+α : Type u
+β : α → (sorryAx (Sort ?))
+p₁ p₂ : (sorryAx (Sort u_1))
+h₁ : (sorryAx ?m.319)=(sorryAx ?m.319)
+⊢ Prop
+doSeqRightIssue.lean:7:48: error: don't know how to synthesize placeholder
+  @Eq ?m.319 … …
+context:
+α : Type u
+β : α → (sorryAx (Sort ?))
+p₁ p₂ : (sorryAx (Sort u_1))
+⊢ Sort u_2

tests/lean/holes.lean

@@ -2,3 +2,10 @@ new_frontend
 
 def f (x : Nat) : Nat :=
 id (_ x)
+
+def g {α β : Type} (a : α) : α :=
+a
+
+def f3 (x : Nat) : Nat :=
+let y := g x + g x;
+y + _ + ?hole

tests/lean/holes.lean.expected.out

@@ -1 +1,22 @@
 holes.lean:4:4: error: placeholders '_' cannot be used where a function is expected
+holes.lean:11:8: error: don't know how to synthesize placeholder
+context:
+case hole
+x : Nat
+y : Nat := g x+g x
+⊢ Nat
+holes.lean:11:4: error: don't know how to synthesize placeholder
+context:
+x : Nat
+y : Nat := g x+g x
+⊢ Nat
+holes.lean:10:15: error: don't know how to synthesize placeholder
+  @g … ?m.39 …
+context:
+x : Nat
+⊢ Type
+holes.lean:10:9: error: don't know how to synthesize placeholder
+  @g … ?m.38 …
+context:
+x : Nat
+⊢ Type