Consider

foo = case id of id' -> (id' 'x', id' True)

Should this be accepted or rejected? GHC currently rejects. But simply by changing this line to use tcInferSigma instead of tcInferRho, the program is accepted. (That's really it! Try it at home!)

Should we make this change? It makes our language more expressive. It also gets us closer to the Platonic ideal of a Hindley-Milner language design, in that users should never have to think about instantiation or generalization. And ML does it. If I write

let ex = match fun x -> x with
           | f -> (f 'x', f true)

then ocamlc accepts without complaint. Actually, this ML example is even more interesting: not only does it preserve the polymorphism in the scrutinee, it actually generalizes. Really, if Damas and Milner had been examining a language with case, they would have said that we need generalization at let and at case.

Of course, we could use tcInferSigma (enabling the Haskell example) but not to generalization. That means that foo would be accepted, but this bar would be rejected:

bar = case \x -> x of id' -> (id' 'x', id' True)

That's a bit of a shame.

This ticket is to track this small design decision.