From fc79b794bad2f717ea4298a2c92831cb88b6ebed Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 5 Mar 2021 17:20:04 -0800 Subject: [PATCH] fix: missing error messages Issue reported by @JasonGross --- src/Lean/Elab/App.lean | 5 +- src/Lean/Elab/Term.lean | 2 +- src/Lean/Expr.lean | 10 +++ tests/lean/holes.lean.expected.out | 6 ++ tests/lean/jason1.lean | 50 +++++++++++ tests/lean/jason1.lean.expected.out | 133 ++++++++++++++++++++++++++++ tests/lean/jason2.lean | 4 + tests/lean/jason2.lean.expected.out | 8 ++ 8 files changed, 214 insertions(+), 4 deletions(-) create mode 100644 tests/lean/jason1.lean create mode 100644 tests/lean/jason1.lean.expected.out create mode 100644 tests/lean/jason2.lean create mode 100644 tests/lean/jason2.lean.expected.out diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 7db42af393..3e0026283b 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -317,7 +317,7 @@ private def addEtaArg (k : M Expr) : M Expr := do /- This method execute after all application arguments have been processed. -/ private def finalize : M Expr := do let s ← get - let mut e := s.f + let mut e := s.f -- all user explicit arguments have been consumed trace[Elab.app.finalize]! e let ref ← getRef @@ -344,8 +344,7 @@ private def finalize : M Expr := do private def addImplicitArg (k : M Expr) : M Expr := do let argType ← getArgExpectedType let arg ← mkFreshExprMVar argType - if (← isTypeFormer arg) then - modify fun s => { s with toSetErrorCtx := s.toSetErrorCtx.push arg.mvarId! } + modify fun s => { s with toSetErrorCtx := s.toSetErrorCtx.push arg.mvarId! } addNewArg arg k diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 076bdab497..1aa3abdc78 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -415,7 +415,7 @@ def MVarErrorInfo.logError (mvarErrorInfo : MVarErrorInfo) (extraMsg? : Option M match mvarErrorInfo.kind with | MVarErrorKind.implicitArg app => do let app ← instantiateMVars app - let msg : MessageData := m!"don't know how to synthesize implicit argument{indentExpr app.setAppPPExplicit}" + let msg : MessageData := m!"don't know how to synthesize implicit argument{indentExpr app.setAppPPExplicitForExposingMVars}" let msg := msg ++ Format.line ++ "context:" ++ Format.line ++ MessageData.ofGoal mvarErrorInfo.mvarId logErrorAt mvarErrorInfo.ref (appendExtra msg) | MVarErrorKind.hole => do diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index aa4c1a4e02..f76fdf6b91 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -986,6 +986,16 @@ def setAppPPExplicit (e : Expr) : Expr := mkAppN f args |>.setPPExplicit true | _ => e +/- Similar for `setAppPPExplicit`, but only annotate children with `pp.explicit := false` if + `e` does not contain metavariables. -/ +def setAppPPExplicitForExposingMVars (e : Expr) : Expr := + match e with + | app .. => + let f := e.getAppFn.setPPExplicit false + let args := e.getAppArgs.map fun arg => if arg.hasMVar then arg else arg.setPPExplicit false + mkAppN f args |>.setPPExplicit true + | _ => e + end Expr def mkAnnotation (kind : Name) (e : Expr) : Expr := diff --git a/tests/lean/holes.lean.expected.out b/tests/lean/holes.lean.expected.out index 2817656f87..bbeb370539 100644 --- a/tests/lean/holes.lean.expected.out +++ b/tests/lean/holes.lean.expected.out @@ -22,6 +22,12 @@ x : Nat ⊢ Type holes.lean:13:7-13:8: error: failed to infer binder type holes.lean:15:16-15:17: error: failed to infer binder type +holes.lean:19:0-19:3: error: don't know how to synthesize implicit argument + @f Nat (?m a) a +context: +a : Nat +f : {α : Type} → {β : ?m a} → α → α := fun {α : Type} (a : α) => a +⊢ ?m a holes.lean:18:6-18:7: error: failed to infer binder type holes.lean:21:25-22:4: error: failed to infer definition type holes.lean:25:8-25:9: error: failed to infer 'let rec' declaration type diff --git a/tests/lean/jason1.lean b/tests/lean/jason1.lean new file mode 100644 index 0000000000..0e1f132ffd --- /dev/null +++ b/tests/lean/jason1.lean @@ -0,0 +1,50 @@ +section + variable (G : Type) (T : Type) (Tm : Type) + (EG : G → G → Type) (ET : T → T → Type) (ETm : Tm → Tm → Type) + (getCtx : T → G) (getTy : Tm → T) + inductive CtxSyntaxLayer where + | emp : CtxSyntaxLayer + | snoc : (Γ : G) → (t : T) → EG Γ (getCtx t) → CtxSyntaxLayer +end +section + variable (G : Type) (T : Type) (Tm : Type) + (EG : G → G → Type) (ET : T → T → Type) (ETm : Tm → Tm → Type) + (getCtx : T → G) (getTy : Tm → T) +-- : CtxSyntaxLayer G T EG getCtx → G) + + inductive TySyntaxLayer where + | top : {Γ : G} → TySyntaxLayer + | bot : {Γ : G} → TySyntaxLayer + | nat : {Γ : G} → TySyntaxLayer + | arrow : {Γ : G} → (A B : T) → EG Γ (getCtx A) → EG Γ (getCtx B) → TySyntaxLayer + + def getCtxStep : TySyntaxLayer G T EG getCtx → G + | TySyntaxLayer.top (Γ := Γ) .. => Γ + | TySyntaxLayer.bot (Γ := Γ) .. => Γ + | TySyntaxLayer.nat (Γ := Γ) .. => Γ + | TySyntaxLayer.arrow (Γ := Γ) .. => Γ +end +section + variable (G : Type) (T : Type) (Tm : Type) + (EG : G → G → Type) (ET : T → T → Type) (ETm : Tm → Tm → Type) + (EGrfl : ∀ {Γ}, EG Γ Γ) + (getCtx : T → G) (getTy : Tm → T) + (GAlgebra : CtxSyntaxLayer G T EG getCtx → G) (TAlgebra : TySyntaxLayer G T EG getCtx → T) + + inductive TmSyntaxLayer where + | tt : {Γ : G} → TmSyntaxLayer + | zero : {Γ : G} → TmSyntaxLayer + | succ : {Γ : G} → TmSyntaxLayer + | app : {Γ : G} → (A B : T) → (Actx : EG Γ (getCtx A)) → (Bctx : EG Γ (getCtx B)) + → (f x : Tm) + → ET (TAlgebra (TySyntaxLayer.arrow A B Actx Bctx)) (getTy f) + → ET A (getTy x) + → TmSyntaxLayer + + set_option pp.all true + def getTyStep : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra → T + | TmSyntaxLayer.tt .. => TAlgebra TySyntaxLayer.top + | TmSyntaxLayer.zero .. => TAlgebra TySyntaxLayer.nat + | TmSyntaxLayer.succ .. => TAlgebra (TySyntaxLayer.arrow (TAlgebra TySyntaxLayer.nat) (TAlgebra TySyntaxLayer.nat) EGrfl EGrfl) + | TmSyntaxLayer.app (B:=B) .. => B +end diff --git a/tests/lean/jason1.lean.expected.out b/tests/lean/jason1.lean.expected.out new file mode 100644 index 0000000000..2af7ac48fb --- /dev/null +++ b/tests/lean/jason1.lean.expected.out @@ -0,0 +1,133 @@ +jason1.lean:48:41-48:130: error: don't know how to synthesize implicit argument + @TySyntaxLayer.arrow G T EG getCtx + (getCtx + (TAlgebra + (@TySyntaxLayer.nat G T EG getCtx + (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))) + (TAlgebra + (@TySyntaxLayer.nat G T EG getCtx + (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))) + (TAlgebra + (@TySyntaxLayer.nat G T EG getCtx + (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))) + (@EGrfl + (getCtx + (TAlgebra + (@TySyntaxLayer.nat G T EG getCtx + (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))))) + (@EGrfl + (getCtx + (TAlgebra + (@TySyntaxLayer.nat G T EG getCtx + (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))))) +context: +G T Tm : Type +EG : G → G → Type +ET : T → T → Type +ETm : Tm → Tm → Type +EGrfl : {Γ : G} → EG Γ Γ +getCtx : T → G +getTy : Tm → T +GAlgebra : CtxSyntaxLayer G T EG getCtx → G +TAlgebra : TySyntaxLayer G T EG getCtx → T +x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra +x✝ : G +⊢ G +jason1.lean:48:125-48:130: error: don't know how to synthesize implicit argument + @EGrfl + (getCtx + (TAlgebra + (@TySyntaxLayer.nat G T EG getCtx + (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))) +context: +G T Tm : Type +EG : G → G → Type +ET : T → T → Type +ETm : Tm → Tm → Type +EGrfl : {Γ : G} → EG Γ Γ +getCtx : T → G +getTy : Tm → T +GAlgebra : CtxSyntaxLayer G T EG getCtx → G +TAlgebra : TySyntaxLayer G T EG getCtx → T +x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra +x✝ : G +⊢ G +jason1.lean:48:119-48:124: error: don't know how to synthesize implicit argument + @EGrfl + (getCtx + (TAlgebra + (@TySyntaxLayer.nat G T EG getCtx + (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))) +context: +G T Tm : Type +EG : G → G → Type +ET : T → T → Type +ETm : Tm → Tm → Type +EGrfl : {Γ : G} → EG Γ Γ +getCtx : T → G +getTy : Tm → T +GAlgebra : CtxSyntaxLayer G T EG getCtx → G +TAlgebra : TySyntaxLayer G T EG getCtx → T +x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra +x✝ : G +⊢ G +jason1.lean:48:100-48:117: error: don't know how to synthesize implicit argument + @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝) +context: +G T Tm : Type +EG : G → G → Type +ET : T → T → Type +ETm : Tm → Tm → Type +EGrfl : {Γ : G} → EG Γ Γ +getCtx : T → G +getTy : Tm → T +GAlgebra : CtxSyntaxLayer G T EG getCtx → G +TAlgebra : TySyntaxLayer G T EG getCtx → T +x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra +x✝ : G +⊢ G +jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument + @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝) +context: +G T Tm : Type +EG : G → G → Type +ET : T → T → Type +ETm : Tm → Tm → Type +EGrfl : {Γ : G} → EG Γ Γ +getCtx : T → G +getTy : Tm → T +GAlgebra : CtxSyntaxLayer G T EG getCtx → G +TAlgebra : TySyntaxLayer G T EG getCtx → T +x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra +x✝ : G +⊢ G +jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument + @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝) +context: +G T Tm : Type +EG : G → G → Type +ET : T → T → Type +ETm : Tm → Tm → Type +EGrfl : {Γ : G} → EG Γ Γ +getCtx : T → G +getTy : Tm → T +GAlgebra : CtxSyntaxLayer G T EG getCtx → G +TAlgebra : TySyntaxLayer G T EG getCtx → T +x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra +x✝ : G +⊢ G +jason1.lean:46:40-46:57: error: don't know how to synthesize implicit argument + @TySyntaxLayer.top G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝) +context: +G T Tm : Type +EG : G → G → Type +ET : T → T → Type +ETm : Tm → Tm → Type +EGrfl : {Γ : G} → EG Γ Γ +getCtx : T → G +getTy : Tm → T +GAlgebra : CtxSyntaxLayer G T EG getCtx → G +TAlgebra : TySyntaxLayer G T EG getCtx → T +x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra +x✝ : G +⊢ G diff --git a/tests/lean/jason2.lean b/tests/lean/jason2.lean new file mode 100644 index 0000000000..fd5fad04f8 --- /dev/null +++ b/tests/lean/jason2.lean @@ -0,0 +1,4 @@ +inductive Foo {x : Nat} : Type where + | foo : Foo + +def bar := (fun _ : Foo => 0) Foo.foo diff --git a/tests/lean/jason2.lean.expected.out b/tests/lean/jason2.lean.expected.out new file mode 100644 index 0000000000..20d01eabe5 --- /dev/null +++ b/tests/lean/jason2.lean.expected.out @@ -0,0 +1,8 @@ +jason2.lean:4:30-4:37: error: don't know how to synthesize implicit argument + @Foo.foo ?m +context: +⊢ Nat +jason2.lean:4:20-4:23: error: don't know how to synthesize implicit argument + @Foo ?m +context: +⊢ Nat