GADTs don't refine hole types
Apologies if this is a dupe. I did look!
{-# LANGUAGE GADTs #-}
data T a where
I :: T Int
f :: T a -> a
f I = _
This gives the type error:
• Found hole: _ :: a
Where: ‘a’ is a rigid type variable bound by
the type signature for:
f :: forall a. T a -> a
at test.hs:6:6
• In the expression: _
In an equation for ‘f’: f I = _
• Relevant bindings include f :: T a -> a (bound at test.hs:7:1)
It should say something about a
being Int
in this branch.
I'm using GHC 8.0.1 on OSX El Capitan. I think this may be a regression; I have a vague memory of it working with GHC 7.10.
Trac metadata
Trac field | Value |
---|---|
Version | 8.0.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | MacOS X |
Architecture |