unknown free variable in VSCode info view

Stream: lean4

[Snir Broshi]

image.png

Is it useful for me to minimize this and open an issue, or should I ignore it?

[Aaron Liu]

yeah this is probably a bug somewhere

[Snir Broshi]

yes but is it worth the effort?

[Kim Morrison]

That's up to you, of course. But I would probably attempt to minimize if I encountered this. Errors that only exhibit via rpc are a bit weird!

[Jovan Gerbscheid]

This is probably an error in delaboration since the error is in the place of the tactic state. Last time I saw this, it was related to the max/min delaborator that I wrote.

[Snir Broshi]

Okay, minimized without Mathlib:

def Set (α : Type) := α → Prop

@[ext]
theorem Set.ext {α : Type} {a b : Set α} (h : ∀ x, a x ↔ b x) : a = b :=
  funext (propext <| h ·)

def space : Type :=
  Quot (α := Bool) fun _ _ ↦ True

def subset : Set space :=
  fun _ ↦ True

def subspace : Type :=
  {x // subset x}

theorem foo (s : Set subspace) : s = s := by
  ext ⟨⟨x⟩, h⟩
  sorry

Place the cursor right before the h in the ext call (line 17 column 13), and it shows:

Error updating: Error fetching goals: Rpc error: InternalError: unknown free variable `_fvar.227`. Try again.

[Aaron Liu]

oh

[Aaron Liu]

I had a thread

[Snir Broshi]

Now the question is whether to report in lean4 or vscode-lean4

[Aaron Liu]

lemme find it real quick

[Aaron Liu]

I'm 95% sure this is the same or at least a related bug

[Aaron Liu]

here it is #lean4 > unknown free variable on `obtain`

[Jovan Gerbscheid]

Yeah I've minimized it a bit more to rcases/obtain:

def Set (α : Type) := α → Prop

@[ext]
theorem Set.ext {α : Type} {a b : Set α} (h : ∀ x, a x ↔ b x) : a = b :=
  funext (propext <| h ·)

def space : Type :=
  Quot (α := Bool) fun _ _ ↦ True

def subspace : Type :=
  {x : space // x = x}

theorem foo (h : subspace) : True := by
  rcases h with ⟨⟨x⟩, h⟩
  sorry

[Snir Broshi]

So this bug is not related to quotients?

[Snir Broshi]

They do look similar

[Jovan Gerbscheid]

The rcases/obtain tactic creates a tactic state for you to look at when you place your cursor there. And apparently it can create an invalid tactic state.