将此视为@chi 答案的附录，以提供对单例方法的更多解释...
如果您还没有这样做，我建议您阅读Hasochism paper。特别是，在该论文的第 3.1 节中，他们恰好处理了这个问题，并将其用作隐式单例参数时的激励示例（@chi 的答案的SingI，以及 Hasochism 论文中的NATTY 类型类) 是必要的，而不仅仅是方便。
因为它适用于您的代码，主要问题是 pure 需要运行时表示它应该生成的向量的长度，而类型级变量 n 不适合账单。解决方案是引入一个新的 GADT，一个“单例”，它提供与提升的类型 Next 和 Zero 直接对应的运行时值：
data Natty (n :: Nat) where
ZeroTy :: Natty Zero
NextTy :: Natty n -> Natty (Next n)
我尝试使用与论文大致相同的命名约定：Natty 相同，ZeroTy 和 NextTy 对应论文的 Zy 和 Sy。
就其本身而言，这个显式单例很有用。例如，见论文中vchop的定义。此外，我们可以轻松编写 pure 的变体，它采用显式单例来完成其工作：
vcopies :: Natty n -> a -> Vector n a
vcopies ZeroTy _ = Empty
vcopies (NextTy n) x = Construct x (vcopies n x)
不过，我们还不能使用它来定义pure，因为pure 的签名是由Applicative 类型类确定的，我们无法将显式单例Natty n 压缩到其中.
解决方案是引入隐式单例，它允许我们在需要时通过natty 函数在以下类型类的上下文中检索显式单例：
class NATTY n where
natty :: Natty n
instance NATTY Zero where
natty = ZeroTy
instance NATTY n => NATTY (Next n) where
natty = NextTy natty
现在，如果我们在 NATTY n 上下文中，我们可以调用 vcopies natty 以提供 vcopies 及其显式 natty 参数，这允许我们编写：
instance NATTY n => Applicative (Vector n) where
(<*>) = vapp
pure = vcopies natty
使用上面vcopies和natty的定义，以及下面vapp的定义：
vapp :: Vector n (a -> b) -> Vector n a -> Vector n b
vapp Empty Empty = Empty
vapp (Construct f c) (Construct x d) = Construct (f x) (vapp c d)
注意一个奇怪的地方。我们需要引入这个vapp 辅助函数，原因不明。以下实例没有 NATTY 匹配您基于case 的定义和类型检查正常：
instance Applicative (Vector n) where
Empty <*> Empty = Empty
Construct f c <*> Construct x d = Construct (f x) (c <*> d)
pure = error "Argh! No NATTY!"
如果我们添加NATTY 约束来定义pure：
instance NATTY n => Applicative (Vector n) where
Empty <*> Empty = Empty
Construct f c <*> Construct x d = Construct (f x) (c <*> d)
pure = vcopies natty
(<*>) 的定义不再进行类型检查。问题是第二个(<*>) 案例左侧的NATTY n 约束不会自动暗示右侧的NATTY n1 约束（其中Next n ~ n1），所以GHC 不会想让我们在右边打电话给(<*>)。在这种情况下，由于第一次使用该约束后实际上并不需要该约束，因此没有NATTY 约束的辅助函数，即vapp，可以解决该问题。
@chi 在natty 和辅助函数withSingI 上使用大小写匹配作为替代解决方法。这里的等效代码将使用一个辅助函数，将显式单例转换为隐式 NATTY 上下文：
withNATTY :: Natty n -> (NATTY n => a) -> a
withNATTY ZeroTy a = a
withNATTY (NextTy n) a = withNATTY n a
允许我们写：
instance NATTY n => Applicative (Vector n) where
Empty <*> Empty = Empty
Construct f c <*> Construct x d = case (natty :: Natty n) of
NextTy n -> withNATTY n $ Construct (f x) (c <*> d)
pure x = case (natty :: Natty n) of
ZeroTy -> Empty
NextTy n -> Construct x (withNATTY n $ pure x)
这需要ScopedTypeVariables 和RankNTypes。
无论如何，坚持使用辅助函数，完整的程序如下所示：
{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}
module Vector where
data Nat = Next Nat | Zero
data Vector :: Nat -> * -> * where
Construct :: t -> Vector n t -> Vector ('Next n) t
Empty :: Vector 'Zero t
data Natty (n :: Nat) where
ZeroTy :: Natty Zero
NextTy :: Natty n -> Natty (Next n)
class NATTY n where
natty :: Natty n
instance NATTY Zero where
natty = ZeroTy
instance NATTY n => NATTY (Next n) where
natty = NextTy natty
instance Functor (Vector n) where
fmap f a =
case a of
Construct x b -> Construct (f x) (fmap f b)
Empty -> Empty
instance NATTY n => Applicative (Vector n) where
(<*>) = vapp
pure = vcopies natty
vapp :: Vector n (a -> b) -> Vector n a -> Vector n b
vapp Empty Empty = Empty
vapp (Construct f c) (Construct x d) = Construct (f x) (vapp c d)
vcopies :: Natty n -> a -> Vector n a
vcopies ZeroTy _ = Empty
vcopies (NextTy n) x = Construct x (vcopies n x)
与singletons库的对应关系是：
$(singletons [d|
data Nat = Next Nat | Zero
|])
自动生成单例（使用构造函数SZero 和SNat 代替ZeroTy 和NatTy；使用类型SNat 代替Natty）和隐式单例类（改为SingI的NATTY 并使用函数sing 而不是natty)，给出完整的程序：
{-# LANGUAGE DataKinds, GADTs, KindSignatures, TemplateHaskell, TypeFamilies #-}
module Vector where
import Data.Singletons
import Data.Singletons.TH
$(singletons [d|
data Nat = Next Nat | Zero
|])
data Vector :: Nat -> * -> * where
Construct :: t -> Vector n t -> Vector ('Next n) t
Empty :: Vector 'Zero t
instance Functor (Vector n) where
fmap f a =
case a of
Construct x b -> Construct (f x) (fmap f b)
Empty -> Empty
instance SingI n => Applicative (Vector n) where
(<*>) = vapp
pure = vcopies sing
vapp :: Vector n (a -> b) -> Vector n a -> Vector n b
vapp Empty Empty = Empty
vapp (Construct f c) (Construct x d) = Construct (f x) (vapp c d)
vcopies :: SNat n -> a -> Vector n a
vcopies SZero _ = Empty
vcopies (SNext n) x = Construct x (vcopies n x)
有关singletons 库的功能及其构建方式的更多信息，我建议阅读Introduction to Singletons。