Eta-expand constructors immediately

[favonia]

[favonia]

@jonsterling loop should be elaborated into extlam i -> loop i immediately and then there is no need to have a special elaboration for spines.

[favonia]

This also gives us the ability to write loop directly.

[jonsterling]

I don't like this solution, because it actually requires elaborating it to not this lambda, but a type annotated one. This will disrupt overloading of constructors, so it is a non-starter.

Instead, IMO, we really should continue to use the whole spine (sorry!), but maybe we can find a cleaner way to do it.

Separately, we should find a way to provide the functionality of just writing loop, or maybe to avoid ambiguity, s1.loop (as in Coq, written @loop).

[jonsterling]

(Sorry if my comment was difficult to understand, I am very sleepy. Will revisit tomorrow/today.)

[favonia]

It is fine. Just that I did not know overloading is one of our goals.

[jonsterling]

I'll think about it agian when I'm more awake. it may be possible to do what you want without disrupting anything...

[favonia]

I don't like this solution, because it actually requires elaborating it to not this lambda, but a type annotated one. This will disrupt overloading of constructors, so it is a non-starter.

I have to study the elaboration of constructors more carefully, but one hacky proposal is to grab the tip of the "arrows". For example, during the elaboration of loop, its type should be blah0 -> blah1 -> ... -> s1 and then we know it is about s1.

[jonsterling]

@favonia For some reason I'm worried about that idea, but I don't know why :laughing: I'll think it over.