assertion violation when using rfl to define instance

[kbuzzard]

Prerequisites

• [X ] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Assertion violation in Lean

Steps to Reproduce

Run the one-liner

instance foo (α : Type) : group α := { mul_assoc := λ x y z, rfl }

Expected behavior: [What you expect to happen]

invalid structure value { ... }, field 'mul' was not provided (etc etc)

Actual behavior: [What actually happens]

LEAN ASSERTION VIOLATION
File: /home/travis/build/leanprover/lean/src/frontends/lean/elaborator.cpp
Line: 3167
Task: /home/buzzard/test.lean: foo
m_ctx.match(e, *val2)

Reproduces how often: [What percentage of the time does it reproduce?]

100%

Versions

Lean (version 3.3.1, commit 28f4143be31b, Release) (on Ubuntu 16.04)

Additional Information

I have seen this issue several times now, which is why I'm reporting it. I usually trigger it with an over-optimistic rfl when attempting to define fields of an instance of a structure.

[Kha]

For reference

[...] a case where type_context::is_def_eq is not idempotent, i.e. it returns first true, then false on equivalent pairs of terms, which makes the structure notation assert (https://github.com/leanprover/lean/blob/76843717c486e29d6dc270df587165325478f85e/src/frontends/lean/elaborator.cpp#L3167):

structure presheaf_of_types (α : Type*) :=
(F : Π U : set α,  Type*)
(res : ∀ (U V : set α) ,
  (F U) → (F V))
(Hidem : ∀ U : set α, res U U = (res U U) ∘ (res U U))

set_option trace.type_context.is_def_eq true
set_option trace.type_context.is_def_eq_detail true

definition presheaf_of_types_pushforward
  {β : Type*}
  : presheaf_of_types β :=
  { Hidem := λ U, rfl,
}

    [type_context.is_def_eq] ∀ (U : set β), ?m_2[U] = ?m_2[U] =?= ∀ (U : set ?m_3), ?res U U = ?res U U ∘ ?res U U ... success  (approximate mode)
...
    [type_context.is_def_eq_detail] Type mismatch when assigning ?Hidem := λ (U : set β), rfl
    >> ∀ (U : set ?m_1), ?res U U = ?res U U ∘ ?res U U =?= ∀ (U : set β), ⁇ U U ∘ ⁇ U U = ⁇ U U ∘ ⁇ U U
    [type_context.is_def_eq] ?Hidem =?= λ (U : set β), rfl ... failed 
    13   3 error           'unreachable' code was reached (lean-checker)

The failed type is equal to the successful type after inserting mvars
The culprit seems to be elim_delayed_abstraction, which, via revert, may accidentally reassign mvars:

    [type_context.is_def_eq_detail] eliminated delayed abstraction:
    ?m_1[U]
    ====>
    ?m_2 U
    [type_context.is_def_eq_detail] process_assignment ?m_1 U := ⁇ U U
    [type_context.is_def_eq_detail] eliminated delayed abstraction:
    ?m_1[U]
    ====>
    ?m_2 U
    [type_context.is_def_eq_detail] process_assignment ?m_1 U := ⁇ U → ⁇ U
    [type_context.is_def_eq_detail] assign: ?m_1 := λ (U : set β), ⁇ U → ⁇ U
    [type_context.is_def_eq_detail] assign: ?m_1 := λ (U : set β), ⁇ U U