GADT 和 ScopedTypeVariables/PatternSignatures 之间的交互

如何解决GADT 和 ScopedTypeVariables/PatternSignatures 之间的交互

我正在探索长度索引向量的“陈词滥调”示例，代码改编自 Richard Eisenberg's thesis 第 3.1 节

{-# LANGUAGE  GADTs,TypeFamilies,DataKinds,KindSignatures,TypeOperators,ScopedTypeVariables  #-}
                          -- PatternSignatures  -- deprecated

import GHC.Types (Type)

data Nat = Zero | Succ Nat
data Vec :: Type -> Nat -> Type  where
  Nil :: Vec a Zero                       -- E has 'Zero
  (:>) :: a -> Vec a n -> Vec a (Succ n)  -- E has 'Succ
infixr 5 :>

type family (+) (n :: Nat) (m :: Nat) :: Nat  where
  (+) Zero      m = m
  (+) (Succ n') m = Succ (n' + m)

append :: Vec a n -> Vec a m -> Vec a (n + m)
append (Nil     :: Vec aa Zero) (w :: Vec aa mm) = w :: Vec aa (Zero + mm)
append (x :> (v :: Vec a n'))   (w :: Vec a m)   = x :> ((append v w) :: Vec a (n' + m))

拒绝 append Nil ... 方程 (GHC 8.6.5)

* Couldn't match type `m' with `n + m'
  `m' is a rigid type variable bound by
    the type signature for:
      append :: forall a (n :: Nat) (m :: Nat).
                Vec a n -> Vec a m -> Vec a (n + m)
    at ...
  Expected type: Vec a (n + m)
    Actual type: Vec a ('Zero + m)

将结果类型指定为 :: Vec aa mm 也被拒绝。

  Expected type: Vec a (n + m)
    Actual type: Vec a m

很奇怪，因为这是被接受的（见下文）。

我真正想做的是使用 PatternSignatures 作为 append 的参数。但该扩展已被弃用，我必须使用 ScopedTypeVariables。这意味着 append 的签名中的 tyvars 在方程的范围内。所以我使用了新鲜的 tyvar 名称。

GADT 给出 Nil :: Vec a Zero，因此我将其作为其模式签名（带有新的 aa）。但似乎 GHC 无法将 n 签名中的 append 与 Zero 统一起来。如果我将该等式更改为其中任何一个，都会很高兴：

append (Nil     :: Vec aa nn) (w :: Vec aa mm) = w :: Vec aa (nn + mm)

append (Nil     :: Vec aa nn) (w :: Vec aa mm) = w :: Vec aa (mm)

为了验证这些，GHC 必须从 Nil :: Vec a Zero 的类型族方程中找出 Zero + m = m 和 +。那么为什么对带有 Zero 的模式签名不满意？

（我最初试图纯粹用 append 给出 PatternSignatures 的方程，看看 GHC 是否可以推断出签名。那没有开始。）