simp_lemmas assertion violation

Stream: general

[Mario Carneiro]

I'm getting several dozen assertion violations like this in recent versions of lean + mathlib:

LEAN ASSERTION VIOLATION
File: /home/mario/Documents/lean/lean/src/library/tactic/simp_lemmas.cpp
Line: 853
Task: /home/mario/Documents/lean/mathlib/src/data/fin.lean: fin.val_eq_coe
is_eq(type, lhs, rhs)
LEAN ASSERTION VIOLATION
File: /home/mario/Documents/lean/lean/src/library/tactic/simp_lemmas.cpp
Line: 853
Task: /home/mario/Documents/lean/mathlib/src/data/fin.lean: fin.zero_succ_above
is_eq(type, lhs, rhs)
LEAN ASSERTION VIOLATION
File: /home/mario/Documents/lean/lean/src/library/tactic/simp_lemmas.cpp
Line: 853
Task: /home/mario/Documents/lean/mathlib/src/data/finset/basic.lean: finset.attach_val
is_eq(type, lhs, rhs)
...

I'm juggling multiple versions of lean though so it might be a configuration problem on my end, so I would like to know if anyone else has seen such errors recently.

[Gabriel Ebner]

This is super weird. It complains that the type of fin.val_eq_coe is not ∀ ..., ... = .... If you get a chance to hook up a debugger and look at the value of type, it should be pretty clear what the problem is.