很抱歉简化函数的第一个版本搞砸了，我希望下面更新的第二个版本更有意义。也很抱歉非标准符号，但我不太关心辅助类型 Nat，并且更喜欢为我的"标量向量"保存一些类型(对于我的下一个问题，我保证会更重视读者的理智，并在发布前调整我的代码)。
我使用的向量类型与几个小时前的问题一样被限制为具有 $2^n$ 元素：
{-# LANGUAGE GADTs, DataKinds, FlexibleInstances, FlexibleContexts #-}
data Nat = Z | N Nat
data Vector n t where
S :: t -> Vector Z t
V :: Vector n t -> Vector n t -> Vector (N n) t
instance Functor (Vector n) where
fmap f (S t ) = S (f t)
fmap f (V t t') = V (fmap f t) (fmap f t')
instance Applicative (Vector Z) where
pure = S
S f <*> S a = S (f a)
instance Applicative (Vector n) => Applicative (Vector (N n)) where
pure a = let a' = pure a in V a' a'
V f f' <*> V a a' = V (f <*> a) (f' <*> a')
instance (Num t, Applicative (Vector n)) => Num (Vector n t) where
v + v' = (+) <$> v <*> v'
v * v' = (*) <$> v <*> v'
abs = fmap abs
signum = fmap signum
fromInteger = pure . fromInteger
negate = fmap negate
现在我未能实现一个相当复杂的递归函数，我无法在这里重现，但我问题的本质可以在这个更简单的函数中看到(这没有多大意义，抱歉)：
dummy :: Applicative (Vector n) => Vector n Int -> Vector n Int -> Int
dummy (S a) (S b) = a + b
dummy (V a a') (V b b') = dummy (a*b) (a'*b')
我的编译器(ghci，仍然是Windows 7上的Haskell平台8.0.2-a)给我的错误消息是(略微缩短)：
• Could not deduce (Applicative (Vector n2))
arising from a use of ‘dummy’
from the context: Applicative (Vector n)
bound by the type signature for:
dummy :: Applicative (Vector n) =>
Vector n Int -> Vector n Int -> Int
at ...
or from: n ~ 'N n2
bound by a pattern with constructor:
V :: forall t (n :: Nat).
Vector n t -> Vector n t -> Vector ('N n) t,
in an equation for ‘dummy’
at ...
• In the expression: dummy (a * b) (a' * b')
In an equation for ‘dummy’:
dummy (V a a') (V b b') = dummy (a * b) (a' * b')
对我来说，它看起来与这个问题中的问题相似。
我尝试通过单独定义来绕过它
dummy :: Applicative (Vector Z) => Vector n Int -> Vector n Int -> Int
dummy = ...
和
dummy :: Applicative (Vector n) => Vector (N n) Int -> Vector (N n) Int -> Int
dummy = ...
但随后编译器抱怨
...: error:
Duplicate type signatures for ‘dummy’
at ...
我是否必须使用唯一的函数虚拟定义一个类型类，然后创建它的Vector Z和(Vector (N n))实例？
class Dummy d where
dummy :: d -> d -> Int
instance Dummy (Vector Z Int) where
dummy (S a) (S b) = a + b
instance (Applicative (Vector n), Dummy (Vector n Int)) => Dummy (Vector (N n) Int) where
dummy (V a a') (V b b') = dummy (a*b) (a'*b')
编译器会接受它，但没有更好的方法吗？
我想dfeuer的答案包含更好的解决方案，但我无法使其适应我对Nat的定义(还)。
好问题！一种方法是及时恢复Applicative实例，当我们发现需要它时，它会递归树的脊椎。所以：
{-# LANGUAGE RankNTypes #-}
withApplicative :: Vector n t -> (Applicative (Vector n) => a) -> a
withApplicative S{} a = a
withApplicative (V v _) a = withApplicative v a
有了这个，我们可以调用适当的实例，而无需将其放在我们的上下文中：
dummy :: Vector n Int -> Vector n Int -> Int
dummy (S a) (S b) = a + b
dummy (V a a') (V b b') = withApplicative a (dummy (a*b) (a'*b'))
由于withApplicative树的深度是线性的，并且我们在每个深度调用withApplicative一次，因此这将添加一个在树的深度中是二次的运行时组件，以构建适当的Applicative字典。通过一些工作，应该可以在递归调用之间共享字典，以将深度成本降低到线性;但是由于计算本身在深度上已经是指数级的，也许额外的二次成本已经足够小了。
withApplicative是怎么回事？
好的，我们手里有一Vector n t。现在，我们精心设置了Vector，使其只接受n的Nat值，我们聪明的程序员知道Nat是将N应用于最终Z的长序列。但是编译器不知道*，它只知道它具有某种类型的nNat。因此，由于它不知道它是一堆应用于ZN，它不知道如何构建一个Applicative实例——因为所有ApplicativeVector实例都要求VectorNat参数明显地Z或N _。类型变量n都不是这些。这就是我们要解决的问题。
或者，你可以对问题进行这种替代描述：即使我们告诉编译器我们有一个用于Vector n的Applicative实例，一旦我们发现n ~ N n'(例如，通过Vector上的模式匹配并看到它有一个V构造函数)，我们又回到了递归调用的原点， 因为我们还没有告诉编译器我们有一个Applicative实例用于Vector n'。因此，另一种思考解决方案的方式是，我们希望有某种方式说，如果我们有一个Vector n的Applicative实例，我们必须有一个Applicative实例用于n的所有前身(所有"较小的"Nat)。
但是等等！我们有一个诡计。我们在Vector中存储了一些信息，通过模式匹配，让我们确切地弄清楚n变量Nat是什么！即：S _向量有n ~ Z，V _ _向量有n ~ N n'(那么我们必须递归才能弄清楚n'是什么)。因此，如果我们以某种方式能够一直到S进行模式匹配，我们将同时使类型检查器知道n的值，一直到Z。然后它可以向上工作，为Z构建Applicative实例，然后N Z，然后N (N Z)，依此类推，一直回到它现在知道的值n。
所以这就是计划：如果我们需要一个Applicative实例来计算一个东西，模式匹配V的应用程序一直到一个S，以了解Z有多少N应用程序;然后利用这些知识来构建实例。
这就是直觉。让我们来看看机制。
withApplicative :: Vector n t -> (Applicative (Vector n) => a) -> a
这个类型签名说：假设你需要一个Applicative实例来计算一个事物——具体来说，是一个a的事物。也就是说，假设您有一个类型Applicative (Vector n) => a的计算。如果您也有Vector n t，我可以在该Vector上进行模式匹配，以了解n的值并构建Applicative实例，这样我就可以为您提供已经使用Applicative实例并且不再需要它的a东西。比较此类型：
withFoo :: Foo -> (Foo -> a) -> a
"如果你有东西要靠Foo，有Foo，我可以给你相应的东西。"而这种类型：
withComputedFoo :: Bar -> (Foo -> a) -> a
"如果你有东西要靠Foo，我就可以做个Foo递给我，就算你给我一个Bar。"(例如，withComputedFoo可能包含类型Bar -> Foo的函数，该函数应用于您为其提供Bar。现在重新审视我们的类型：
withApplicative :: Vector n t -> (Applicative (Vector n) => a) -> a
"如果你有东西需要一本Applicative (Vector n)字典，如果你递给我一个Vector n t我会为你制作字典，并给你相应的东西。
好吧，但它是如何工作的？
withApplicative S{} a = a
如果你递给我一个构造函数为S的向量，那么我知道n是Z的。所以现在我学会了，以前我有a :: Applicative (Vector n) => a，现在我有a :: Applicative (Vector Z) => a。由于全局范围内有一个Applicative (Vector Z)实例，我可以使用它，所以我也可以给它类型a :: a.这个案子完了！
withApplicative (V v _) a = withApplicative v a
如果你递给我一个构造函数是V的向量，那么我知道n实际上是N n'了某些n'(而且至关重要的是，v :: Vector n' t)。所以现在我以前有a :: Applicative (Vector n) => a，现在我有a :: Applicative (Vector (N n')) => a.啊！但是我们在全局范围内Applicative (Vector n) => Applicative Vector (N n)了一个实例，因此可以将此约束简化为a :: Applicative (Vector n') => a。由于我们有一个长度n'向量 - 即v- 现在我们可以递归，尽管请注意递归调用中的Nat-kinded类型已更改！现在我们用v :: Vector n' t和a :: Applicative (Vector n') => a来称呼withApplicative，也就是用n的前身n'。
这就是她写的全部内容！递归负责为前一个构建字典，我们使用全局可用的实例为n构建稍大的字典，我们正在路上。
* 编译器不知道它，因为它实际上不是真的。我们在骗自己。但它足够接近真实，可以成为一个有用的心智模型。
以下是对该问题先前版本的回答。
如果我只是省略Applicative约束，您的dummy对我来说编译得很好：
dummy :: Vector n Int -> Vector n Int -> Int
dummy (S a) (S b) = a + b
dummy (V a a') (V b b') = let c = dummy a b
c' = dummy a' b'
in c + c'
(也许你需要让你的激励例子稍微复杂一点，才能真正抓住你的问题的难点......？
为了我的理智，我将重命名您的构造函数。
data Nat = Z | S Nat
data Vector n a where
Leaf :: a -> Vector 'Z a
Branch :: Vector n a -> Vector n a -> Vector ('S n) a
问题在于递归情况。知道Applicative ('S n)不会给你Applicative n;为此，只能使用超类约束，而不能使用实例约束。原因是实例约束只是说如何构造字典;它没有说明其中的内容。
我怀疑你可能想要的是一种非常常见的民俗机制，使用"单例"类型。
data SNat n where
SZ :: SNat 'Z
SS :: SNat n -> SNat ('S n)
class KnownNat n where
known :: SNat n
instance Known 'Z where
known = SZ
instance Known n => Known ('S n) where
known = SS known
现在，您可以编写适用于SNat的函数，以及隐式适用于KnownNat的函数。
dummy :: KnownNat n => Vector n Int -> Vector n Int -> Int
dummy = dummy' known
dummy' :: SNat n -> Vector n Int -> Vector n Int -> Int
注意：如果您查看我对上一个问题的回答，您会发现只有pureApplicative方法是与大小相关的。因此，如果您不需要pure，则可以完全拉动约束。