`case` needn't instantiate its scrutinee
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.