Type inference in GADT pattern matches

When pattern matching against GADT constructors, GHC seems to have issues with inferring the type of the resulting expression.

Minimal example: Assume the datatype:

data D a where D :: D ()

A simple function that pattern matches on it:

a D = ()

It is expected to have type D a -> () (Note: not D () -> (), existence of a D should ensure (), not the type signature), but instead it errors:

error:
    Couldn't match expected type ‘t’ with actual type ‘()’
      ‘t’ is untouchable
        inside the constraints: t1 ~ ()
        bound by a pattern with constructor: D :: D (),
                 in an equation for ‘a’
    ‘t’ is a rigid type variable bound by
        the inferred type of a :: D t1 -> t

Note that the error goes away when we annotate the type of the function:

b :: D a -> () -- no error
b D = ()

Or if we supply another branch that clarifies the type:

c D = () -- no error
c _ = ()

But it reappears if the other branch doesn't provide anything to infer from:

d D = () -- error
d _ = undefined

The same issue happens in case:

e x = case x of D -> () -- error

But only when the value being matched comes from outside:

f = case D of D -> () -- no error

This behavior is reprooducible and identical in 7.8.4.

Trac metadata

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