Proof fails after alpha-renaming

[ndmitchell]

Given the code at the bottom of this issue, using Idris 1.0, if I comment out the line marked -- WORKS and uncomment the -- BREAKS one the code stops type checking. Specifically shadowing a variable n seems to break the proof, which surprises me as alpha-equivalence means they should be equivalent. I was wondering if this was a free-variable-clash bug? (I'm an Idris beginner, so this might just be me misunderstanding Idris.)

fibb : Nat -> Nat
fibb Z = 0
fibb (S Z) = 1
fibb (S (S n)) = fibb (S n) + fibb n

fib_tail' : Nat -> Nat -> Nat -> Nat
fib_tail' n a b = case n of
    Z => b
    S n' => fib_tail' n' (a + b) a -- WORKS
    -- S n => fib_tail' n (a + b) a -- BREAKS

fib_tail : Nat -> Nat
fib_tail n = fib_tail' n 1 0

fib_tail_correct' : (d : Nat) -> (u : Nat) -> fib_tail' d (fibb (S u)) (fibb u) = fibb (d+u)
fib_tail_correct' Z u = Refl
fib_tail_correct' (S d) u = ?todo

[ahmadsalim]

Thanks for reporting the issue. It does seem like a bug indeed.

[david-christiansen]

I have a guess as to what's happening here.

Case expressions are lifted to top-level pattern-matching during elaboration. When they do that, they abstract over all free variables. So we end up with something like:

mutual
  fib_tail_helper : Nat -> Nat -> Nat -> Nat -> Nat
  fib_tail_helper n a b Z = b
  fib_tail_helper n a b (S n) = fib_tail' n (a + b) a

  fib_tail' : Nat -> Nat -> Nat -> Nat
  fib_tail' n a b = fib_tail_helper n a b n

There does indeed seem to be an issue here. The TT for the second case in version of the helper that works is:

pat n' : Prelude.Nat.Nat.
 pat a : Prelude.Nat.Nat.
  pat b : Prelude.Nat.Nat.
   pat n : Prelude.Nat.Nat.
    Main.case block in fib_tail' at n.idr:8:24 (Prelude.Nat.S n') a b n
    ↦
    Main.fib_tail' n' (Prelude.Interfaces.+ Prelude.Nat.Nat Prelude.Nat.Nat implementation of Prelude.Interfaces.Num a b) a

and the TT for the version that does not work is:

pat n : Prelude.Nat.Nat.
 pat a : Prelude.Nat.Nat.
  pat b : Prelude.Nat.Nat.
   pat {scvar_507} : Prelude.Nat.Nat.
    Main.case block in fib_tail' at n.idr:8:24 (Prelude.Nat.S n) a b {scvar_507},
    ↦
    Main.fib_tail' n (Prelude.Interfaces.+ Prelude.Nat.Nat Prelude.Nat.Nat implementation of Prelude.Interfaces.Num a b) a

Note that the inner pattern variable n is identified with the outer one, which it should not be.