Pattern synonyms and kind-polymorphism
There's a strange interaction between pattern synonyms, GADTs, kind polymorphism and data kinds.
The following module fails to compile with ghc-7.8.1-rc2, but I think it should:
{-# LANGUAGE PolyKinds, KindSignatures, PatternSynonyms, DataKinds, GADTs #-}
data NQ :: [k] -> * where
D :: NQ '[a]
pattern Q = D
I get the following error:
KindPat.hs:6:13:
Could not deduce (a ~ a0)
from the context (t ~ '[a])
bound by the type signature for (Main.$WQ) :: t ~ '[a] => NQ t
at KindPat.hs:6:9
‘a’ is a rigid type variable bound by
the type signature for (Main.$WQ) :: t ~ '[a] => NQ t
at KindPat.hs:6:13
Expected type: NQ t
Actual type: NQ '[a0]
In the expression: D
In an equation for ‘$WQ’: ($WQ) = D
Trac metadata
Trac field | Value |
---|---|
Version | 7.8.1-rc2 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |