Muster-Synonym kann Typen in Typenliste nicht vereinheitlichen

Question

Ich erhalte einen Fehler beim Versuch, ein Muster-Synonym basierend auf einem GADT, das eine Typenliste hat, zu definieren.

schaffte ich es zu kochen dieses Beispiel unten:

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

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

pattern LUnit = L() 

Gebe ich:

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() 

Ist das ein Bug, oder bin ich etwas falsch?

Answer 1

Dank dfeuer's comment und this ticket konnte ich mein Beispiel-Code erhalten, indem das Hinzufügen einer Art Signatur an die Musterdefinition zu kompilieren:

{-# 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() 

Welche polymorphe Muster verallgemeinert schön auch

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

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