This is a very different rule indeed! And one which gives a strict semantic to the initial offender.

But there are holes in it: if I `let (x, y) = blah in …` and `x` is at an unlifted type, the pattern _needs_ to be strict (this is solved by the current rule as described by Richard) despite the rhs being at a lifted type. That's because binding `x` forces the pattern anyway, by definition. There are questions about nested patterns, as well. What about `let (U x, y) = blah in …`, where `U` is some unlifted type. Is the nested `U x` pattern strict? or is it lazy? There is no corresponding right-hand side.

This is all a tad tricky, I must say.