Renaming a variable also renames another variable
Opened this issue · 3 comments
Prerequisites
- Put an X between the brackets on this line if you have done all of the following:
- Check that your issue is not already filed.
- Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.
Description
In the following code:
namespace Nat
inductive AnInductive: Nat → Type where
| OptionA: Nat → AnInductive zero
| OptionB: Nat → AnInductive zero
def AnInductive.foo (w0: AnInductive n): Nat :=
match w0 with
| OptionA natA => natA
| OptionB natB => natB
end Nat
renaming the variable natA
also renames the last occurence of natB
.
Steps to Reproduce
Position your caret inside an occurence of variable natA
and rename the variable (F2, then enter a new name).
I believe the same issue is also reproducible in https://live.lean-lang.org/, even though the online editor does not
allow renaming variables -- position your care inside the latter occurence of natA
(the former only works some
of the time for me), and the highlighted variables will include the last occurence of natB
Expected behavior: Only the variable natA
is renamed
Actual behavior: Renaming natA
to eg. asdf
results in:
| OptionA asdf => asdf
| OptionB natB => asdf
Versions
Lean: 4.4.0-rc1
OS: Ubuntu 22.04.4 LTS;
Also reproducible on https://live.lean-lang.org/ as of posting.
Impact
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
Another variation:
inductive AnInductive: Nat → Type where
| OptionA: Unit → AnInductive 0
def AnInductive.foo {n} (w0: AnInductive n): Unit :=
match w0 with
| OptionA natA => natA
Using go-to-def on the second occurrence of natA
leads to the {n}
binder.
It looks like an issue in the name generator (or the way it is used): In the above example the {n}
has an FVarAlias
node added to the info tree referring to _fvar.N
, but when the pattern match runs (noting that the new n
is eliminated due to the index equality), it "un-creates" the copied n
variable, including rewinding the name generator state to N-1
. So the next variable to be created is the pattern variable natA
, which is given the name _fvar.N
as well, meaning that now the info tree appears to say that natA
is an alias of {n}
.
I'm not sure if this is a separate issue or not, but I suspect it might be related. In the following code:
inductive HasFalse: Prop
| WithFalse (f: False)
inductive AnInductive: Nat → Nat → Prop where
| OptionA: AnInductive a b → AnInductive a b
| OptionB: HasFalse → AnInductive b b
def AnInductive.isFunctional
(w0: AnInductive arg a)
(w1: AnInductive arg b)
:
a = b
:=
match w0, w1 with
| OptionA isIncrA, OptionA isIncrB =>
isFunctional isIncrA isIncrB ▸ rfl
-- Remove the next line to make the issue disappear
| OptionB _, OptionB _ => rfl
| OptionB hasFalse, OptionA _ =>
match hasFalse with
| HasFalse.WithFalse eq => False.elim eq
The definition AnInductive.isFunctional
is reported as using sorry despite that there is no sorry anywhere. Also the latter occurence of hasFalse
is treated as if it was isIncrA
.
When the line under the comment is removed, both issues disappear.