Trivial partial type signature kills type inference in the presence of GADTs
Suppose we have
data G a where G1 :: G Char G2 :: G Bool
If I now write
foo x = case x of G1 -> 'z' G2 -> True
I rightly get an error around untouchable variables.
If I add the type signature
foo :: G a -> a
all is well again. So far, so good.
Now, I write
foo :: forall a. G a -> a foo x = ((case x of G1 -> 'z' G2 -> True) :: _)
and I get those untouchable errors again. Untouchable-variable errors usually arise when there are multiple possible answers to the type inference problem. Yet, that isn't the case here:
_ must stand for
Solution: mumble mumble bidirectional type inference mumble mumble.
Part of the problem comes from Note [Partial expression signatures] in TcExpr, which states
here is a guiding principile e :: ty should behave like let x :: ty x = e in x
Indeed, if we behave like that, the untouchable-variable errors are to be expected. But I also think that it would be a nice principle to say that
:: _ is always a no-op.
This is not an idle nice-to-have: if we fix this,
singletons will continue to work with GHC. Right now, it doesn't: https://github.com/goldfirere/singletons/issues/357