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

fix: reset set of stuck mvars after reporting they are stuck

Browse source 
This bug produced the doubled error message at issue #337
This commit is contained in:
Leonardo de Moura 2021-03-08 12:40:05 -08:00
parent 5d3f0606d2
commit f321ad213f
2 changed files with 2 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -163,8 +163,8 @@ private def synthesizeUsingDefault : TermElabM Bool := do
/-- Report an error for each synthetic metavariable that could not be resolved. -/
private def reportStuckSyntheticMVars : TermElabM Unit := do
let s ← get
for mvarSyntheticDecl in s.syntheticMVars do
let syntheticMVars ← modifyGet fun s => (s.syntheticMVars, { s with syntheticMVars := [] })
for mvarSyntheticDecl in syntheticMVars do
withRef mvarSyntheticDecl.stx do
match mvarSyntheticDecl.kind with
| SyntheticMVarKind.typeClass =>

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

@ -1,6 +1,4 @@
297.lean:1:10-1:11: error: typeclass instance problem is stuck, it is often due to metavariables
OfNat (Sort ?u) 0
297.lean:1:13-3:1: error: invalid universe level, u_1 is not greater than 0
297.lean:1:10-1:11: error: failed to synthesize instance
OfNat (Sort u_1) 0
297.lean:1:8-1:9: error: (kernel) declaration has metavariables 'r'