模式同義詞不能統一類型級別列表中的類型

嘗試在具有類型級別列表的GADT上基於定義模式同義詞時出現錯誤。模式同義詞不能統一類型級別列表中的類型

我設法熬下來到這個例子：

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

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

pattern LUnit = L()

給我：

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

這是一個錯誤，還是我做錯了什麼？

來源

2016-03-30 rampion

我認爲你至少需要一個模式簽名，但是文檔似乎沒有清楚地說明是否可以將GADT構造函數的類型同義爲多態作爲構造函數本身。 – dfeuer

dfeuer：啊哈，謝謝 – rampion

感謝dfeuer's comment和this ticket，我能得到我的示例代碼中加入一個類型簽名模式定義編譯：

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

這也很好地推廣到多態模式

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

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

來源

2016-03-30 22:44:27 rampion

模式同義詞不能統一類型級別列表中的類型

回答

相關問題