你定义的向量类型，正如你已经指出的，是同构的。你不能真正使用forall将同构类型转换为异构类型，因为这不是它的真正用途。
相反，我们真正需要的是一个异构的向量类型。首先，让我们把形式摆在一边。我们将需要一个 * 很多 * 的GHC扩展到这结束时，所以在这里，我们去。

{-# LANGUAGE GADTs, DataKinds, TypeOperators, KindSignatures, TypeFamilies,
             MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances,
             UndecidableInstances #-}

我假设您使用的Nat类型来自GHC.TypeLits，而Type类型来自Data.Kind。

import Data.Kind
import GHC.TypeLits

现在你的原始向量类型看起来像这样。

data Vector :: Nat -> Type -> Type where
  VNil  :: Vector 0 a
  VCons :: a -> Vector n a -> Vector (n + 1) a

我提议用这个代替。

data Vector (n :: Nat) (xs :: [Type]) where
  VNil :: Vector 0 '[]
  VCons :: t -> Vector n ts -> Vector (n + 1) (t ': ts)

infixr 9 `VCons`

而不是有一个 * 单一 * 类型的元素，我们有一个元素类型的列表。请注意，xs是类型（从Data.Kind到Type）的列表（如内置的[]类型）。Haskell中定义的每一个类型都可以提升到类型级别。你已经看到了如何提升自然数的字面量（这是一个特殊的情况，因为它们周围的特殊语法），但我们可以对列表做同样的事情。
VNil只对长度为零和空类型列表有效，而VCons对长度为n + 1的 * 非空 * 列表有效，并且由元素t（类型级别列表t ': ts的头部）和尾部Vector n ts组成。
在构造函数的前面有撇号，我们正在从值级别提升到类型级别。'[]只是值构造器[]（即空列表）提升到类型级别。在没有引号的情况下，在类型上下文中，[]是* -> *类型的类型构造函数，因此我们必须提升它以修复二义性。这样做通常是很好的做法，即使它不是模棱两可的。
我还将VCons定义为在中缀形式中使用时是右结合的，这将使实际构建这些向量 * 稍微 * 容易一些。
现在，我建议我们完全忽略n参数。你可以用n参数做我在这里建议的几乎所有事情，但是因为我们也有列表，我们仍然知道我们的向量静态地有多长。所以我建议

data Vector (xs :: [Type]) where
  VNil :: Vector '[]
  VCons :: t -> Vector ts -> Vector (t ': ts)

infixr 9 `VCons`

我们可以使用类型级函数恢复类型级的长度。实际上，这将是hMap的一个很好的实践，所以让我们把它写出来。
当我们想写一个递归一个复杂的GADT类型的函数时，我们通常是这样做的，作为一个类型类。在本例中，我们需要一个名为VectorLength的类型级函数，因此我们将编写一个定义type family的类型类来给予我们结果。
在普通值级别的Haskell中，您编写类型签名，然后编写要进行模式匹配的case。我们在类型级Haskell中做同样的事情。然而，我们的“类型签名”是class，我们的case是instance s。这是我们的签名

class HasLength (ts :: [Type]) where
    type VectorLength ts :: Nat

现在我们的基本情况是空列表类型级别值'[]的示例。把这句话再读一遍，确保你明白我在这里重载了什么。

instance HasLength '[] where
    type VectorLength '[] = 0

最后是递归的例子。

instance HasLength xs => HasLength (x ': xs) where
    type VectorLength (x ': xs) = 1 + VectorLength xs

如果尾部（包含xs）有长度，则包含(x ': xs)的向量有长度。具体来说，长度是1 + VectorLength xs。您可以将示例的上下文（本例中为HasLength xs）视为函数的一种依赖列表。我们的函数需要调用VectorLength xs，所以我们必须在instance头文件中声明。
现在让我们写hMap。这也将在类型类中，但它将是一个常规的Haskell函数，而不是类型家族，因为我们希望在值级别上操作。它仍然必须是一个类型类，因为我们要在类型级别（即我们的组成类型列表）上进行 * 分派 *。
这是类型签名

class CanHMap (fs :: [Type]) (a :: Type) (bs :: [Type]) | fs -> bs where
    hMap :: Vector fs -> a -> Vector bs

竖线|后面的那个有趣的小语法叫做functional dependency，它确实有助于类型推断。如果我知道fs的值（函数），那么我可以推导出bs的值（这些函数的结果）。
现在我们来写一个基本案例。

instance CanHMap '[] a '[] where
    hMap VNil _ = VNil

空的函数列表可以被hMap填充到空的结果列表中，中间的类型a无关紧要。具体来说，这个Map将VNilMap到VNil。
继续我们的递归案例。

instance CanHMap fs a bs => CanHMap ((a -> b) ': fs) a (b ': bs) where
    hMap (VCons f fs) a = VCons (f a) (hMap fs a)

如果我们可以使用a类型的输入将fs转换为bs，那么我们也可以使用a类型的输入将((a -> b) ': fs)转换为(b ': bs)。
这里的巧妙之处在于，在完成了所有疯狂的类型级别的杂耍之后，函数体实际上非常简单和美丽。
我们来测试一下。这里有一些功能。

myFunctions :: Vector '[Int -> Int, Int -> String, Int -> ()]
myFunctions = (\n -> n + 1) `VCons` show `VCons` (\_ -> ()) `VCons` VNil

这就是为什么我在前面声明了infixr声明：所以我们可以在这里链接VCons调用。
下面是我们将这些函数应用于0时的结果列表。

myVector :: Vector [Int, String, ()]
myVector = hMap myFunctions (0 :: Int)

这是一种技术，但它有效吗？为了解决这个问题，我们需要编写一些快速的Show示例来打印它们。

-- I ignore the precedence parameter here. Feel free
-- to fill that in on your own time. :)

instance Show (Vector '[]) where
    showsPrec _ VNil = ("VNil" ++)

instance (Show x, Show (Vector xs)) => Show (Vector (x ': xs)) where
    showsPrec _ (VCons x xs) = ("VCons " ++) . shows x . (" (" ++) . shows xs . (")" ++)

最后

main :: IO ()
main = print myVector

判决结果呢

$ runhaskell example.hs
VCons 1 (VCons "0" (VCons () (VNil)))

成功啦！

您可以在Try it online上看到此代码的完整工作示例！