[GHC] #8966: Pattern synonyms and kind-polymorphism

[GHC]

#8966: Pattern synonyms and kind-polymorphism
-------------------------------------+-------------------------------------
       Reporter:  kosmikus           |             Owner:
           Type:  bug                |            Status:  new
       Priority:  normal             |         Milestone:
      Component:  Compiler (Type     |           Version:  7.8.1-rc2
  checker)                           |  Operating System:  Unknown/Multiple
       Keywords:                     |   Type of failure:  GHC rejects
   Architecture:  Unknown/Multiple   |  valid program
     Difficulty:  Unknown            |         Test Case:
     Blocked By:                     |          Blocking:
Related Tickets:                     |
-------------------------------------+-------------------------------------
 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
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8966>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler