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 a.

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

Trac metadata

Trac field	Value
Version	8.6.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture