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 |