[fuzz-tested] Kernel error: in a mutual block, a sibling’s universe parameter leaks into bar.induct
Maintainers usually reply within 1 day
Nobody has claimed this yet.
Assessment
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Newbie friendliness
- 43/100
- Issue type
- Bug
- Clarity
- Mostly clear
- Activity status
- Active
- Domain
- compilers
Research direction
Start by reproducing the mutual block and checking @bar.induct in Lean 4. Trace how universe parameters from sibling definitions are carried into generated induction principles; the report is complete when the example checks without the undefined universe level error.
Written by the indexing model from the issue text.
Description
The following code:
mutual
def my_eq {A : Type _} (a b : A) : Prop := True
def bar : Nat → { _n : Nat // True }
| 0 => ⟨0, trivial⟩
| n + 1 =>
let r := bar n
⟨r.1, r.2⟩
end
#check @bar.induct
Resulted in this output:
error: (kernel) invalid reference to undefined universe level parameter 'u_1'
Expected: no error.
- Dominant language
- Lean
- Stars
- 9.6k
- Forks
- 1.1k
- Avg merge
- 1d 17m
- Merged PRs (30d)
- 296
Getting set up
- No Dockerfile or Docker Compose file
- Has a pull request template
- Read the contributing guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from leanprover/lean4
-
bug
Difficulty 1/5 Under an hour Newbie friendliness 85/100
leanprover/lean4#15925 ·
Maintainers usually reply within 1 day
-
`IO.appPath` fails when `/proc` belongs to another PID namespacePossibly taken @treiher claimed this 6 days ago. Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
leanprover/lean4#15692 · 3 reactions ·
Maintainers usually reply within 1 day
-
`IO.FS.realPath` reports every failure as `noFileOrDirectory` instead of classifying by `errno`Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 66/100
leanprover/lean4#15683 ·
Maintainers usually reply within 1 day
-
`Child.pid` leaks the `Child` and its pipe file descriptors (owned argument treated as borrowed)Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 70/100
leanprover/lean4#15681 ·
Maintainers usually reply within 1 day
-
bug
Difficulty 2/5 1-3 hours Newbie friendliness 76/100
leanprover/lean4#15677 ·
Maintainers usually reply within 1 day
All issues in leanprover/lean4
Similar issues
-
area:codegen backend:cuda backend:hip bug direction:input
Difficulty 2/5 1-3 hours Newbie friendliness 78/100
CrossGL/crosstl#3061 · 1 comment ·
Maintainers usually reply within 1 day
-
bug
Difficulty 2/5 1-3 hours Newbie friendliness 85/100
-
build
Difficulty 2/5 1-3 hours Newbie friendliness 65/100
AOMediaCodec/SVT-AV1#2500 ·
-
Difficulty 2/5 1-3 hours Newbie friendliness 75/100
rescript-lang/rescript#9037 ·
Maintainers usually reply within 1 day
-
bug goto-symex
Difficulty 2/5 1-3 hours Newbie friendliness 83/100
Maintainers usually reply within 1 day