模式同义词不能统一类型级列表中的类型答案

【问题标题】：Pattern synonym can't unify types within type-level list模式同义词不能统一类型级列表中的类型
【发布时间】：2016-07-19 03:55:44
【问题描述】：

我在尝试定义基于模式同义词时遇到错误在具有类型级别列表的 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 ()

这是一个错误，还是我做错了什么？

【问题讨论】：

我认为您至少需要一个模式签名，但文档似乎并没有很清楚地说明是否可以将 GADT 构造函数的模式同义词类型与构造函数一样多态本身。

标签： haskell data-kinds pattern-synonyms

【解决方案1】：

感谢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)

【讨论】：