max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: missing error messages

Browse source 
Issue reported by @JasonGross
This commit is contained in:
Leonardo de Moura 2021-03-05 17:20:04 -08:00
parent 0fa6e733c1
commit fc79b794ba
8 changed files with 214 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Elab/App.lean
View file

@ -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

2
src/Lean/Elab/Term.lean
View file

@ -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

10
src/Lean/Expr.lean
View file

@ -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 :=

6
tests/lean/holes.lean.expected.out
View file

@ -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

50
tests/lean/jason1.lean Normal file
View file

@ -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

133
tests/lean/jason1.lean.expected.out Normal file
View file

@ -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

4
tests/lean/jason2.lean Normal file
View file

@ -0,0 +1,4 @@
inductive Foo {x : Nat} : Type where
| foo : Foo
def bar := (fun _ : Foo => 0) Foo.foo

8
tests/lean/jason2.lean.expected.out Normal file
View file

@ -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