Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Kernel failed to type-check due to name collision involving include #751

Open
1 task done
Vierkantor opened this issue Jul 29, 2022 · 0 comments
Open
1 task done
Labels
bug Something isn't working

Comments

@Vierkantor
Copy link
Collaborator

Prerequisites

  • Put an X between the brackets on this line if you have done all of the following:
    • Checked that your issue isn't already filed.
    • Reduced the issue to a self-contained, reproducible test case.

Description

Under the following conditions, we get an error in the kernel:

  • 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

Steps to Reproduce

The following code errors:

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
-/

Expected behavior: No errors in the kernel, like when there's no name clash.

Actual behavior: An error:

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

Reproduces how often: always

Versions

Lean (version 3.45.0, commit 22b09be, Release)

@Vierkantor Vierkantor added the bug Something isn't working label Jul 29, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

1 participant