kernel metavariable bug

Stream: mathlib4

[Yongyi Chen]

MWE:

import Mathlib.GroupTheory.Subgroup.Basic

def what_happened [Group G] : Subgroup G where
  carrier := { g | g : G }
  mul_mem' := by sorry
  one_mem' := sorry
  inv_mem' | ⟨a, b⟩ => sorry

Replace the by sorry with sorry and the bug disappears. Weird.

[Jireh Loreaux]

I'm not sure what you are doing with inv_mem', but that's definitely the cause of the problem.

[Jireh Loreaux]

What inductive type are you trying to destruct there?

[Yongyi Chen]

I had a more complicated carrier but reduced it for the purposes of the MWE. Deconstruction works here still: a has type G and b has type a = x✝.

[Jireh Loreaux]

Oh, I see, you're using the alternate set notation. I misread that the first time. I'm betting it's a bug in the elaborator for that notation. I'll see if I can hunt it down.

[Jireh Loreaux]

Hmmm... I don't see the problem. I think @Kyle Miller has played a bit with binder predicates and this kind of thing before though, so perhaps he has an idea.