Termination checking doesn't work with local lets

[lukaszcz]

Typechecking

module termRec;

import Stdlib.Prelude open;

type MyList A :=
  | myNil
  | myCons@{
      elem : A;
      next : MyList A;
    };

go {A B} (f : A -> B) : MyList A -> MyList B
  | myNil := myNil
  | myCons@{elem; next} := myCons@{elem := f elem; next := go f next};

gives the error

/Users/heliax/Documents/progs/juvix/termRec.juvix:9-12:7-3: error:
The following functions fail the termination checker:
• next
• go

But the following type-checks:

go {A B} (f : A -> B) : MyList A -> MyList B
  | myNil := myNil
  | myCons@{elem; next} := myCons (f elem) (go f next);

Termination checking needs to be adapted to deal with record creation/update syntax (or whatever it is desugared to in Internal).

[janmasrovira]

myCons@{elem := f elem; next := go f next};

desugars to

let var1 = f elem
    var2 = go f next
in myCons var1 var2

[lukaszcz]

Yes, termination fails also when explicitly desugared. Typechecking:

go {A B} (f : A -> B) : MyList A -> MyList B
  | myNil := myNil
  | myCons@{elem; next} :=
    let var1 := f elem;
        var2 := go f next;
    in myCons var1 var2;

gives:

The following functions fail the termination checker:
• var2
• go

[lukaszcz]

Even this fails:

go {A B} (f : A -> B) : MyList A -> MyList B
  | myNil := myNil
  | (myCons elem next) :=
    let var1 := f elem;
        var2 := go f next;
    in myCons var1 var2;

So the problem is, weirdly, with the let, not with record syntax as such.

[lukaszcz]

I think this is the problem:

-- NOTE that we forget about the arguments of the hosting function
scanLetClause :: (Members '[State CallMap] r) => LetClause -> Sem r ()