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

chore: improve error message

Browse source
This commit is contained in:
Leonardo de Moura 2021-02-05 09:30:05 -08:00
parent c17a1c382f
commit 09de37e8e5
3 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -211,7 +211,7 @@ private def reportStuckSyntheticMVars : TermElabM Unit := do
withMVarContext mvarSyntheticDecl.mvarId do
let mvarDecl ← getMVarDecl mvarSyntheticDecl.mvarId
unless (← get).messages.hasErrors do
logError <| "typeclass instance problem contains metavariables" ++ indentExpr mvarDecl.type
logError <| "typeclass instance problem is stuck, it is often due to metavariables" ++ indentExpr mvarDecl.type
| SyntheticMVarKind.coe header expectedType eType e f? =>
withMVarContext mvarSyntheticDecl.mvarId do
let mvarDecl ← getMVarDecl mvarSyntheticDecl.mvarId

2
tests/lean/297.lean.expected.out
View file

@ -1,4 +1,4 @@
297.lean:1:10-1:11: error: typeclass instance problem contains metavariables
297.lean:1:10-1:11: error: typeclass instance problem is stuck, it is often due to metavariables
OfNat (Sort ?u) 0
297.lean:2:0-2:1: error: failed to synthesize instance
OfNat (Id PUnit) 0

2
tests/lean/defaultInstance.lean.expected.out
View file

@ -1,4 +1,4 @@
defaultInstance.lean:20:20-20:23: error: failed to synthesize instance
Foo Bool (?m x)
defaultInstance.lean:22:35-22:38: error: typeclass instance problem contains metavariables
defaultInstance.lean:22:35-22:38: error: typeclass instance problem is stuck, it is often due to metavariables
Foo Bool (?m x)