Haskell无法统一类型实例方程
我试图用（偶/奇）奇偶类标记规范的Nat数据类型，看看我们是否可以得到任何自由定理。 代码如下：
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
-- Use DataKind promotion with type function for even-odd
module EvenOdd where
data Parity = Even | Odd
-- Parity is promoted to kind level Parity.
-- Even & Odd to type level 'Even & 'Odd of kind Parity
-- We define type-function opp to establish the relation that
-- type 'Even is opposite of 'Odd, and vice-versa
type family Opp (n :: Parity) :: Parity
type instance Opp 'Even = 'Odd
type instance Opp 'Odd = 'Even
-- We tag natural number with the type of its parity
data Nat :: Parity -> * where
Zero :: Nat 'Even
Succ :: Nat p -> Nat (Opp p)
-- Now we (should) get free theorems.
-- 1. Plus of two even numbers is even
evenPlus :: Nat 'Even -> Nat 'Even -> Nat 'Even
evenPlus Zero n2 = n2 -- Line 31
evenPlus (Succ (Succ n1)) n2 = Succ (Succ (evenPlus n1 n2))
但是，GHC抛出类型错误：
Could not deduce (p1 ~ 'Even)
from the context ('Even ~ Opp p)
bound by a pattern with constructor
Succ :: forall (p :: Parity). Nat p -> Nat (Opp p),
in an equation for `evenPlus'
at even-odd.hs:31:13-26
or from (p ~ Opp p1)
bound by a pattern with constructor
Succ :: forall (p :: Parity). Nat p -> Nat (Opp p),
in an equation for `evenPlus'
at even-odd.hs:31:19-25
`p1' is a rigid type variable bound by
a pattern with constructor
Succ :: forall (p :: Parity). Nat p -> Nat (Opp p),
in an equation for `evenPlus'
at even-odd.hs:31:19
Expected type: Nat 'Even
Actual type: Nat p
In the first argument of `evenPlus', namely `n1'
In the first argument of `Succ', namely `(evenPlus n1 n2)'
据我了解，上述错误的要点在于当上下文具有等式：（（Opp（Opp p1））〜'Even）时，GHC无法推断（p1〜'Even）。
为什么会发生？ 我的方法有什么问题吗？
我不认为GADT模式匹配细化以这种方式进行。 你有Opp p作为构造函数的结果类型。 所以如果你写了类似的东西
f :: Nat 'Even -> ...
f (Succ n) = ...
那么类型检查者知道Nat (Opp t) ~ Nat 'Even ，因此Opp t ~ 'Even 。 但为了解决这个问题，类型检查器必须反转功能Opp ，这是非常重要的。
我建议你改变Nat的定义来说：
data Nat :: Parity -> * where
Zero :: Nat 'Even
Succ :: Nat (Opp p) -> Nat p
这应该只是工作。
编辑
其实，让我稍微扩大一点。
上面的建议不是没有（小）价格。 你失去了一些类型推断。 例如， Succ Zero的类型现在是Succ Zero :: Opp p ~ 'Even => Nat p而不是Nat 'Odd 。 使用明确的类型注释，它可以解决问题。
您可以通过向Succ添加一个约束来改善此问题，这需要Opp是自逆的。 Parity的唯一两个元素是Even和Odd ，对于这些约束成立，所以它不应该导致任何问题：
data Nat :: Parity -> * where
Zero :: Nat 'Even
Succ :: (Opp (Opp p) ~ p) => Nat (Opp p) -> Nat p
现在Succ Zero被推断为类型Nat 'Odd ，以及模式匹配仍然有效。