Possible bug: "unknown free variable"

Stream: lean4

[Artie Khovanov]

I've isolated some weird/inconsistent behaviour. Is this a known bug? What is going on?

import Mathlib

variable [CommRing R]

def R_copy_1 : AddSubmonoid R where /- compiles -/
  carrier := {z : R | ∃ x, z = x}
  zero_mem' := by aesop
  add_mem' := fun ⟨x₁, eqw⟩ ⟨x₂, eqz⟩ => by aesop?

def R_copy_2 : Submonoid R where /- compiles -/
  carrier := {z : R | ∃ x, z = x}
  one_mem' := by aesop
  mul_mem' := fun ⟨x₁, eqw⟩ ⟨x₂, eqz⟩ => by aesop

def R_copy_3 : Subsemiring R where /- unknown free variable '_fvar.5727' -/
  carrier := {z : R | ∃ x, z = x}
  zero_mem' := by aesop
  add_mem' := fun ⟨x₁, eqw⟩ ⟨x₂, eqz⟩ => by aesop
  one_mem' := by aesop
  mul_mem' := fun ⟨x₁, eqw⟩ ⟨x₂, eqz⟩ => by aesop

def R_copy_4 : Subsemiring R where /- compiles -/
  carrier := {z : R | ∃ x, z = x}
  zero_mem' := by aesop
  add_mem' := by aesop
  one_mem' := by aesop
  mul_mem' := fun ⟨x₁, eqw⟩ ⟨x₂, eqz⟩ => by aesop

[Eric Wieser]

The aesops can all be replaced with sorry and the bug remains, which is good new for Jannis Limperg :)

[Eric Wieser]

A slight minimization:

import Mathlib

variable [NonAssocSemiring R]

def R_copy_3 : Subsemiring R where /- (kernel) declaration has metavariables 'R_copy_3' -/
  carrier := {z : R | ∃ x, z = x}
  zero_mem' := sorry
  one_mem' := by sorry -- remove the `by` and this works
  add_mem' := fun ⟨x₁, eqw⟩ => sorry
  mul_mem' := sorry

[Eric Wieser]

(I guess strictly this is a different error)

[Artie Khovanov]

Oh that's so weird I didn't even think to do that
Yeah to be clear the error is due to the pattern match in fun
if you remove that it all works
like fun x => by obtain ...

[Artie Khovanov]

Looks like lean4#6354

[Bhavik Mehta]

Looks like we now have 5 independent people getting this bug!

[Mario Carneiro]

and how many dependent people?

[Kevin Buzzard]

I guess I cut and pasted the code and observed the error too, so at least one...

[Kyle Miller]

Now at least 5 independent and 2 dependent people have come across this bug now :-)

I think lean4#6414 fixes it. The issue was triggered by having a synthetic metavariable (like a not-yet-evaluated tactic block) in the expected type of a match expression, which caused some meta code to create an invalid expression. Fixing that fixes the issues in lean4#6354, but I haven't tested it on the examples from this thread — waiting on it and mathlib to build first.

[Mauricio Collares]

Why did so many people hit this bug now, when the minimized example fails even in v4.0.0?

[Artie Khovanov]

Mauricio Collares said:

Why did so many people hit this bug now, when the minimized example fails even in v4.0.0?

I hit the bug while trying to pattern match within a lambda. Maybe this feature is more well known now?

[Kyle Miller]

Yeah, it's curious — I'm wondering if people have run into this frequently but either blamed themselves or figured this part of Lean isn't particularly stable so just worked around it. Maybe it's a combination of people being more confident that this should work and this part of Lean becoming more stable, so the bug stuck out more?

[Artie Khovanov]

Yeah I mean I run into janky stuff all the time, and it's hard to tell if the reason is deep or not, so I generally just rejig the proof so it works. Not sure if that's the "right" approach but...