使用 PolyKind 和类型族时的种类歧义

Question

我有两个类型家族，其中一个将一种类型映射到另一种不同类型和多态函数的类型：

{-# LANGUAGE PolyKinds, TypeFamilies, FlexibleContexts, ScopedTypeVariables #-} 

type family F (a :: k1) :: k2
type family G (a :: k2) :: *

f :: forall k1 k2 (a :: k1) (p :: k1 -> *) . p (a :: k1) -> G (F (a :: k1) :: k2)
f = undefined

此代码未进行类型检查并出现以下错误消息：

• Couldn't match type ‘G k20 (F k20 k1 a)’ with ‘G k2 (F k2 k1 a)’
  Expected type: p a -> G k2 (F k2 k1 a)
    Actual type: p a -> G k20 (F k20 k1 a)
  NB: ‘G’ is a non-injective type family

但我不明白歧义从何而来，我该如何指定缺失的种类？

当我只使用一种类型时，它起作用了：

g :: forall k1 k2 (a :: k1) (p :: k1 -> *) (q :: k2 -> *). p (a :: k1) -> q (F (a :: k1) :: k2)
g = undefined

Answer 1

f :: forall k1 k2 (a :: k1) (p :: k1 -> *). p a -> G (F a :: k2)

让我试着说：

x :: [String]
x = f (Just 'a')

这将使用 k1 ~ Type、a ~ Char 和 p ~ Maybe

实例化 f

f :: forall k2. Maybe Char -> G (F Char :: k2)

现在呢？好吧，我还需要 G (F Char :: k2) ~ [String]，但是 G 是一个非单射类型族，所以不知道它的参数——k2 和 F Char :: k2——应该是什么。所以，x的定义是错误的； k2 是不明确的，不可能为它推断实例化。

但是，您可以非常清楚地看到没有 f 的用法 ever 能够推断出 k2.原因是 k2 只出现在非单射类型家族应用程序下面的 f 类型中（另一个 "bad position" 是 => 的 LHS）。它从不出现在可以推断的位置。因此，如果没有像 TypeApplications 这样的扩展名，f 是 无用的 ，并且永远不会在不引发此错误的情况下提及。 GHC 检测到这一点并在定义而不是用法上引发错误。您看到的错误消息与您尝试时遇到的错误大致相同：

f0 :: forall k10 k20 (a :: k10) (p0 :: k10 -> *). p0 a0 -> G (F a0 :: k20)
f0 = f

这会产生相同类型的不匹配，因为没有理由 f0 的 k20 必须匹配 f1 的 k2。

您可以通过启用 AllowAmbiguousTypes 来消除 f 定义中的错误，这会禁用对所有定义的无用性检查。但是，仅此一项，这只会将错误推向 f 的每次使用。为了实际调用 f，您应该启用 TypeApplications:

f0 :: forall k10 k20 (a :: k10) (p0 :: k10 -> *). p0 a0 -> G (F a0 :: k20)
f0 = f @k10 @k20 @a0 @p0

TypeApplications 的替代方法类似于 Data.Proxy.Proxy，但它几乎已经过时了，除了在更高级别的上下文中。（即便如此，一旦我们有了 type-lambdas 之类的东西，它就真的无法工作了。）

Answer 2

歧义检查最初是为了拒绝无法调用的函数，因为类型参数和约束无法从显式函数参数中推断出来。

然而，从 GHC 8.6.x 开始，就没有这样的函数了，因为一切都可以通过 TypeApplications 明确化。我建议只启用 AllowAmbiguousTypes 和 TypeApplications。 GHC 关于模棱两可类型的警告本身并不是很有用，因为它拒绝了类型应用程序的许多有效用例。

使用 PolyKind 和类型族时的种类歧义

Kind ambiguity when using PolyKinds and type families

haskell

type-families

polykinds