variable elaboration going wrong

Stream: lean4

[Patrick Massot]

Is the following trap already documented?

class Bar (R : Type _) :=
(op : R → R)

variable {R : Type _} [Bar R]

namespace Foo

def Bar : Nat := 0

-- Uncomment the next line to get an error on line 4
-- #check Bar
end Foo

[Eric Wieser]

Another manifestation:

def foo := 1
variable (h : foo ≠ 2) -- this is redundant but fine, we defined foo = 1

namespace Foo

def foo := 2

-- oops
example : False := h rfl

end Foo

[Patrick Massot]

Let me clarify for casual readers that Eric's example isn't a soundness issue. It's simply a confusing example where we inadvertently give Lean a contradictory set of assumptions to work with.

[Sebastian Ullrich]

This is https://github.com/leanprover/lean4/issues/1876

[Sebastian Ullrich]

Did I complain about variable before?

[Kyle Miller]

Just to summarize what's going on with this trap, the way variables works is that it does a check and then saves the syntax of the binders. Then each command after that re-elaborates all the saved binder syntax each time.

[Kyle Miller]

Changes to what's in scope can break it (like here) but also changes to available instances, macros, or elaborators can as well.