Open pandaman64 opened 4 weeks ago
Looks like this is triggered by the new GetElem
structure fields added in https://github.com/leanprover/lean4/commit/0963f3476c74312ba95ea67a786c203ed19e48ef.
Inlining and minimizing:
def get (_ : Nat) : Nat := Nat.zero
class GH4418 (idx : Type v) where
getElem (i : idx) : Nat
getElem? (i : idx) : Option Nat :=
if True then Option.some (getElem i) else @Option.none Nat
getElem?2 (i : idx) (_ : Nat) : Option Nat :=
if True then Option.some (getElem i) else @Option.none Nat
-- "unknown free variable: _kernel_fresh.19" at instance
instance : GH4418 Nat where
getElem := get
Note that this while this also triggers the issue:
getElem? (i : idx) : List Nat :=
if True then [getElem i] else []
getElem?2 (i : idx) (_ : Nat) : List Nat :=
if True then [getElem i] else []
this (a mix of the two) does not:
getElem? (i : idx) : List Nat :=
if True then [getElem i] else []
getElem?2 (i : idx) (_ : Nat) : Option Nat :=
if True then Option.some (getElem i) else @Option.none Nat
i.e. getElem?
and getElem2?
have to be similar
This is a bug in the common-case-eliminator in the old code generator.
Prerequisites
Please put an X between the brackets as you perform the following steps:
Description
Hi. I updated my project to v4.8.0 from v4.6.0 and started to get an
unknown free variable: _kernel_fresh.19
error. It seems the nightly also has the issue. Here is the MWE:Spelling out all arguments of
getElem
likegetElem nfa i h := get nfa i h
seems to fix the issue though.Context
Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/unknown.20free.20variable.20in.20v4.2E8.2E0/near/443754071
Original code that could be compiled with v4.6.0 can be found at: https://github.com/pandaman64/lean-regex/blob/64d23c5d3ed30eff3267e8dd6280577ad7f3b321/Regex/NFA/Basic.lean#L124-L125
Steps to Reproduce
Create a project with
leanprover/lean4:v4.8.0
and paste the code above.Expected behavior: the instance definition should compile without an error.
Actual behavior: the instance definition fails with
unknown free variable: _kernel_fresh.19
.Versions
I'm using Windows 11, but the issue reproduced with the web editor.
Impact
Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.