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

collect_univ_params_ignoring_tactics isn't called on anonymous instances #146

Closed
bryangingechen opened this issue Mar 11, 2020 · 0 comments · Fixed by #189
Closed

collect_univ_params_ignoring_tactics isn't called on anonymous instances #146

bryangingechen opened this issue Mar 11, 2020 · 0 comments · Fixed by #189
Milestone

Comments

@bryangingechen
Copy link
Collaborator

Bug identified by @jcommelin and @digama0 in this zulip thread.

Example:

universes u v

class foo (C : Type u) : Type (max u (v+1)) := (A : Type v)

variables (C : Type u) [foo C]

def bar : Type u := C
kernel failed to type check declaration 'bar' this is usually due to a buggy tactic or a bug in the builtin elaborator
elaborated type:
  Π (C : Type u) [_inst_1 : foo C], Type u
elaborated value:
  λ (C : Type u) [_inst_1 : foo C], C
nested exception message:
invalid reference to undefined universe level parameter 'u_1'

"I think it pulled in _inst_1 : foo.{u u_1} C but forgot to also pull in u_1"

@Kha pointed out that the issue was in collect_univ_params_ignoring_tactics.

@gebner gebner added this to the Lean 3.8 milestone Mar 12, 2020
@gebner gebner modified the milestones: Lean 3.8, Lean 3.9 Apr 8, 2020
rwbarton added a commit to rwbarton/lean-1 that referenced this issue Apr 13, 2020
Fixes leanprover-community#146.

This fixes a headache that arises throughout mathlib's category theory library.
rwbarton added a commit to rwbarton/lean-1 that referenced this issue Apr 13, 2020
Fixes leanprover-community#146.

This fixes a headache that arises throughout mathlib's category theory library.
rwbarton added a commit to rwbarton/lean-1 that referenced this issue Apr 13, 2020
Fixes leanprover-community#146.

This fixes a headache that arises throughout mathlib's category theory library.
gebner pushed a commit that referenced this issue Apr 14, 2020
* fix(doc/fixing_tests): fix typo

* chore(frontends/lean/util): remove dead code

* fix(frontends/lean/decl_util): collect univ params of implicit instances

Fixes #146.

This fixes a headache that arises throughout mathlib's category theory library.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants