Synonim wzorca nie może ujednolicić typów na liście poziomu typów

Question

Otrzymuję błąd podczas próby zdefiniowania synonimu wzorca opartego na na GADT, który ma listę poziomu.

udało mi się gotować w dół do tego przykładu:

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE TypeOperators #-} 
{-# LANGUAGE PatternSynonyms #-} 
module Example where 

data L (as :: [*]) where 
    L :: a -> L '[a] 

pattern LUnit = L() 

daje mi:

Example.hs:11:17: 
    Couldn't match type ‘a’ with ‘()’ 
     ‘a’ is a rigid type variable bound by 
      the type signature for Example.$bLUnit :: (t ~ '[a]) => L t 
      at Example.hs:11:17 
    Expected type: L t 
     Actual type: L '[()] 
    In the expression: L() 
    In an equation for ‘$bLUnit’: $bLUnit = L() 

Example.hs:11:19: 
    Could not deduce (a ~()) 
    from the context (t ~ '[a]) 
     bound by a pattern with constructor 
       L :: forall a. a -> L '[a], 
       in a pattern synonym declaration 
     at Example.hs:11:17-20 
     ‘a’ is a rigid type variable bound by 
      a pattern with constructor 
      L :: forall a. a -> L '[a], 
      in a pattern synonym declaration 
      at Example.hs:11:17 
    In the pattern:() 
    In the pattern: L() 

Jest to błąd, czy robię coś źle?

Answer 1

Dzięki dfeuer's comment i this ticket, udało mi się dostać mój przykładowy kod do kompilacji dodając podpis typu definicji wzoru:

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE TypeOperators #-} 
{-# LANGUAGE PatternSynonyms #-} 
module Example where 

data L (as :: [*]) where 
    L :: a -> L '[a] 

pattern LUnit :: L '[()] 
pattern LUnit = L() 

który również uogólnia ładnie polimorficznych wzorców

data F (fs :: [* -> *]) a where 
    F :: f a -> F '[f] a 

pattern FId :: a -> F '[Identity] a 
pattern FId a = F (Identity a)