Dependent default values

[janmasrovira]

• Closes Allow default values to refer to previous arguments #2445

[janmasrovira]

It is possible to enter an infinite loop when inserting default arguments.

E.g.

fun {a : Nat := fun} : Nat := a * a;

main : Nat := fun;

In order to prevent this problem, we need dependency information for default arguments before translating to Internal. I didn't want to delay this pr further, so I'll work on a patch separately. Also, this is a problem with default arguments in general, not only for dependent default values.

[janmasrovira]

It is possible to enter an infinite loop when inserting default arguments.

E.g.

fun {a : Nat := fun} : Nat := a * a;

main : Nat := fun;

In order to prevent this problem, we need dependency information for default arguments before translating to Internal. I didn't want to delay this pr further, so I'll work on a patch separately. Also, this is a problem with default arguments in general, not only for dependent default values.

this has been fixed in e886aa2

[lukaszcz]

Address the comments. I think SimpleLambda can be removed, but not completely sure.