Fix de Bruijn indices in LetRecs

[lukaszcz]

• Closes The de Bruijn indices in the types in LetRecs are all messed up #2226

For the program

module letrec;

import Stdlib.Prelude open;

myfun : {A : Type} -> (A -> A) -> A -> A;
myfun {A} f a :=
      let
        go : Nat -> A -> A;
        go' : Nat -> A -> A;

        go zero a := a;
        go (suc n) a := f (go' n a);

        go' zero a := a;
        go' (suc n) a := f (go n a);
      in
      go 5 a;

main : Nat;
main := myfun ((+) 1) 7;

after translating to Core and lambda-lifting we got the incorrect indices in types of the let-bindings.

def myfun : Π A : Type, (A$0 → A$1) → A$1 → A$2 :=
  λ(A : Type)
    λ(f : A$0 → A$1)
      λ(a : A$1)
        let go' : Int → a$1 → a$2 := go'_9 A$2 f$1 in
        let go : Int → a$2 → a$3 := go_10 A$3 f$2 in
        go$0 5 a$2;

The indices have been corrected in this PR.

[janmasrovira]

Is it possible to add a test that has been fixed by this?

[lukaszcz]

Is it possible to add a test that has been fixed by this?

It's really hard because I can't produce an example that actually makes things crash with the old code, because currently the indices in types are mostly ignored.

[lukaszcz]

Is it possible to add a test that has been fixed by this?

It's really hard because I can't produce an example that actually makes things crash with the old code, because currently the indices in types are mostly ignored.

Any test looking at the output instead would be very unstable, and I don't think we should add it.

[janmasrovira]

Is it possible to add a test that has been fixed by this?

It's really hard because I can't produce an example that actually makes things crash with the old code, because currently the indices in types are mostly ignored.

That's fine, then please, paste the output (before and after the fix) here as a comment