In practice, this came up when compiling my ghengin
package with a newer GHC. I thought of reporting it since it was quite confusing at first why things that were linear before were no longer accepted. Not sure how many programs using linear types exist in the wild though.
The good thing is you now have to explicitly use y
linearly (which you do by calling error on it). If y
is something which must definitely be freed before the program terminates, it’s great we are forced to handle it explicitly — instead of y
being completely lost/dropped if the match fails.
An artificial example: say y
is a seat “token” in some remote cluster, and you need to explicitly free the seat up for someone else to use the cluster. If your program matched False
, it would call fail “e.g. Pattern match failed in do notation”
and the token seat lost as the program abruptly ends. In your reply, you are forced to match on (y, False)
and ignore y
(the token) using error. (Note how fail :: String -> m ()
, no mention of the y
type at all)
My guess is that this wasn’t an intended change, but rather a consequence of desugaring do notation in a more correct way (@ani’s work).