Dependent elimination failed/Unused variable in dependent pattern matching
Open
Nobody has claimed this yet.
bug
P-low
- Dominant language
- Lean
- Stars
- 9.2k
- Forks
- 990
- Avg merge
- 1d 17h
- Merged PRs (30d)
- 175
Description
Steps to Reproduce
Given
inductive LamTerm
| bvar : Nat → LamTerm
structure LamJudge where
lctx : Nat → Nat
rterm : LamTerm
rty : Nat
inductive LamWF : LamJudge → Type
| ofBVar {lctx : Nat → Nat} (n : Nat) : LamWF ⟨lctx, .bvar n, lctx n⟩
The following command gives "unused variable lctxTy"
def LamWF.interp.{u}
(tyVal : Nat → Type u) :
(lctxTy : Nat → Nat) → (lctxTerm : ∀ n, tyVal <| lctxTy n) →
(lwf : LamWF ⟨lctxTy, t, rty⟩) → tyVal rty
| lctxTy, lctxTerm, .ofBVar n => lctxTerm n
while if we replace "lctxTy" with "_", it gives "Dependent elimination failed: ...":
def LamWF.interp.{u}
(tyVal : Nat → Type u) :
(lctxTy : Nat → Nat) → (lctxTerm : ∀ n, tyVal <| lctxTy n) →
(lwf : LamWF ⟨lctxTy, t, rty⟩) → tyVal rty
| _, lctxTerm, .ofBVar n => lctxTerm n
Versions
4.22.0-rc3
Contributor 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.
Research direction
Start by reproducing the LamWF.interp definition with Lean 4.22.0-rc3, comparing the lctxTy pattern with the underscore pattern. Trace the dependent elimination and unused-variable diagnostics; done means the valid definition elaborates without the erroneous warning or dependent-elimination failure.
Written by the indexing model from the issue text.
Assessment
- Domain
- compilers
- Issue type
- Bug
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Quiet
- Clarity
- Mostly clear
- Newbie friendliness
- 45/100