2016-03-30 16 views
8

Viene visualizzato un errore quando si tenta di definire un sinonimo di modello basato su su un GADT che ha un elenco di tipo livello.Il sinonimo di Pattern non può unificare i tipi all'interno dell'elenco a livello di tipo

sono riuscito a bollire fino a questo esempio:

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

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

pattern LUnit = L() 

Mi dà:

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

Questo è un bug, o sto facendo qualcosa di sbagliato?

+3

Penso che tu abbia almeno bisogno di una firma di modello, ma la documentazione non sembra rendere molto chiaro se sia possibile rendere il tipo di un sinonimo di modello per un costruttore GADT come polimorfico come il costruttore stesso. – dfeuer

+0

dfeuer: aha, grazie – rampion

risposta

7

Grazie a dfeuer's comment e this ticket, sono stato in grado di ottenere il mio codice di esempio per compilare con l'aggiunta di una firma di tipo alla definizione modello:

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

che generalizza anche ben a modelli polimorfici

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

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