Kernel failed to typecheck error with `include`

Stream: general

[Anne Baanen]

Here's a MWE of an interesting bug in Lean 3:

variables (a : ℕ)
variables (ha : a = a)

include ha

theorem ex (a : ℕ) : a = a := rfl

/-
error:
kernel failed to type check declaration 'ex' this is usually due to a buggy tactic or a bug in the builtin elaborator
elaborated type:
  a = a → ℕ → ∀ (a : ℕ), a = a
elaborated value:
  λ (ha : a = a) (a a : ℕ), rfl
nested exception message:
failed to add declaration to environment, it contains local constants
-/

[Anne Baanen]

I think the conditions are:

• two variables, one depending on another
• the dependent one is included, transitively includeing its dependency
• there is a local variable with the same name as the dependency
• the included variables are not used in the declaration

[Eric Wieser]

I assume the problem goes away if you avoid the name collision

[Anne Baanen]

If I replace include ha with include a, or replace ex (a : ℕ) : a = a with ex (b : ℕ) : b = b (or ex (b : ℕ) : a = a), everything works.

[Eric Wieser]

Probably worth making a github issue so this doesn't get forgotten

[Anne Baanen]

lean#751

[Eric Wieser]

Here's a version without include:

lemma foo [has_add ℕ] : true :=
begin
  sorry,
end
--^ failed to add declaration to environment, it contains local constants

[Eric Wieser]

Weirder yet:

example [has_zero ℕ] : true :=
by trivial  -- ok

example [has_one ℕ] : true :=
by trivial  -- fails

[Kevin Buzzard]

Presumably changing the order of the examples doesn't change the errors? This is a great one :-)

[Kevin Buzzard]

Is it the same bug as Anne's above?

[Eric Wieser]

Yep, changing the order make no difference

[Eric Wieser]

I don't think it's quite the same, Anne gets a longer error message than I do

[Kevin Buzzard]

Can you reproduce in lean 4?

[Eric Wieser]

No

[Kevin Buzzard]

Looks like this might be a wontfix then?

[Eric Wieser]

As minimal as I can get it:

prelude
import init.meta.tactic

example [has_zero nat] : true := by tactic.admit  -- ok
example [has_one nat] : true := by tactic.admit  -- fails
example [has_add nat] : true := by tactic.admit  -- fails
example [has_mul nat] : true := by tactic.admit  -- ok
example [has_pow nat nat] : true := by tactic.admit  -- ok

[Eric Wieser]

This looks like a hashing bug of some kind