On Fri, Sep 4, 2020 at 5:47 PM Iavor Diatchki
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.