Skip to content

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
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information