From 0fe705f3a1609d523c291cedceb4b801a3130488 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 29 Sep 2020 17:18:03 -0700 Subject: [PATCH] feat: improve error messages for unassigned metavariables cc @Kha --- src/Lean/Elab/App.lean | 2 +- src/Lean/Elab/Binders.lean | 6 ++ src/Lean/Elab/LetRec.lean | 1 + src/Lean/Elab/MutualDef.lean | 7 +- src/Lean/Elab/PreDefinition/Main.lean | 2 +- src/Lean/Elab/Tactic/Basic.lean | 2 +- src/Lean/Elab/Tactic/ElabTerm.lean | 2 +- src/Lean/Elab/Term.lean | 120 +++++++++++++--------- tests/lean/evalWithMVar.lean.expected.out | 4 +- tests/lean/holeErrors.lean | 20 ++++ tests/lean/holeErrors.lean.expected.out | 28 +++++ tests/lean/holes.lean.expected.out | 32 ++---- tests/lean/macroStack.lean.expected.out | 4 +- 13 files changed, 146 insertions(+), 84 deletions(-) create mode 100644 tests/lean/holeErrors.lean create mode 100644 tests/lean/holeErrors.lean.expected.out diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 5cc1eb15aa..01614eab1d 100644 --- a/src/Lean/Elab/App.lean +++ b/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; diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean index 84a8e6fd89..0a7fbb2496 100644 --- a/src/Lean/Elab/Binders.lean +++ b/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; diff --git a/src/Lean/Elab/LetRec.lean b/src/Lean/Elab/LetRec.lean index 8f078b659e..babffc7b41 100644 --- a/src/Lean/Elab/LetRec.lean +++ b/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) }; diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index c021eeb655..d11e06cbc2 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/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) := diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean index 9d331a35e5..813ea23d2f 100644 --- a/src/Lean/Elab/PreDefinition/Main.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index 8f78d5b79a..edf36d5129 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean index 10674834c2..ece241580f 100644 --- a/src/Lean/Elab/Tactic/ElabTerm.lean +++ b/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; diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 1490ccee67..6cdbedf96c 100644 --- a/src/Lean/Elab/Term.lean +++ b/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 diff --git a/tests/lean/evalWithMVar.lean.expected.out b/tests/lean/evalWithMVar.lean.expected.out index 73777b608d..d36f5d5238 100644 --- a/tests/lean/evalWithMVar.lean.expected.out +++ b/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 _ diff --git a/tests/lean/holeErrors.lean b/tests/lean/holeErrors.lean new file mode 100644 index 0000000000..9f56ae5d6e --- /dev/null +++ b/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 diff --git a/tests/lean/holeErrors.lean.expected.out b/tests/lean/holeErrors.lean.expected.out new file mode 100644 index 0000000000..1dbf15c7e3 --- /dev/null +++ b/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 diff --git a/tests/lean/holes.lean.expected.out b/tests/lean/holes.lean.expected.out index ffd9df7dd1..64620033d1 100644 --- a/tests/lean/holes.lean.expected.out +++ b/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 diff --git a/tests/lean/macroStack.lean.expected.out b/tests/lean/macroStack.lean.expected.out index 30fd29c30d..8d3d2b35b6 100644 --- a/tests/lean/macroStack.lean.expected.out +++ b/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