Renaming a variable also renames another variable

mik-jozef commented 1 week ago

Prerequisites

[x] 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 :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

digama0 commented 1 week ago

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.

digama0 commented 1 week ago

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}.

mik-jozef commented 1 week ago

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.

leanprover / lean4