Infer multiplicity of case expression
Motivation
As it stands, the following expression
case u of {…}is always understood by the typechecker as consuming u with multiplicity Many. This was done in the first iteration of patch in order to ensure being fully compatible with regular Haskell without having to delve too much into inference issue.
This applies to case expressions and to pattern guards creating a pattern:
| pat <- u, … = …here u is also consumed with multiplicity Many.
(In a \case or a function definition by equations, the multiplicity is decided by the type that it is checked against, if any. So it may be any multiplicity.)
Core is already equipped to deal with arbitrary multiplicities here.
Proposal
These expressions should infer the appropriate multiplicity. So typechecking such a case expression should emit a multiplicity variable instead of choosing Many systematically.
One somewhat subtle point to keep in mind is that some patterns require that the scrutinee be consumed unrestrictedly. That's the case, for instance, of wildcard patterns (_). I believe that the current implementation will handle a variable for the pattern's multiplicity smoothly (see checkManyPattern in GHC.Tc.Gen.Pat (currently). But it's worth double-checking.
For pattern guard the relevant code is the BindStmt case of tcGuardStmt in GHC.Tc.Gen.Match.
cc @monoidal