On Fri, Sep 4, 2020 at 5:47 PM Iavor Diatchki <iavor.diatchki@gmail.com> wrote:

Interesting. Thanks.

Personally, I don’t really know how to resolve the tension between the outer pattern saying: I really want to be lazy; and uniformity with the unlifted-variable-binding case.

The point about b

b = let ~(MkX z) = undefined in ()

Is that it cannot do anything else than force the pattern. Because b is an unlifted variable, it doesn’t contain a thunk. In other words, we can read it as the pattern being lazy, but it being immediately forced. Pretty much as in:

let (x,y) = undefined in x `seq` ()

My intuition would be that

let (x, (# #)) = (1, undefined) in ()

converges, while

let (x, (# #)) = (1, undefined) in x `seq` ()

diverges.

But I’m not exactly sure how to explain this rule succinctly. And I’m not sure it would be quite as intuitive to anybody. For starters, it seems to depart significantly from Iavor’s intuition.