使用PolyKinds和类型系列时有种歧义

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')

这正好和实例f有k1 ~ Type,a ~ Char和p ~ Maybe

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

怎么办？好吧,我还需要G (F Char :: k2) ~ [String],但是它G是一个非内射类型的家族,所以不知道它的论点k2和 - F Char :: k2应该是什么.因此,定义x是错误的; k2是模糊的,不可能推断它的实例化.

然而,你可以很清楚地看到,没有任何的使用f将永远能够推断k2.理由是k2只出现在f非内射型家庭应用程序下面的类型中(另一个"坏位置"是a的LHS =>).它永远不会出现在可以推断的位置.因此,没有扩展名一样TypeApplications,f是无用的,没有提出这个错误不能被提及.GHC会检测到这一点,并在定义而不是用法中引发错误.您看到的错误消息与您尝试的错误相同:

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

这产生相同的类型不匹配,因为没有理由k20的f0,必须在比赛k2中f1.

您可以f通过启用AllowAmbiguousTypes来清除定义中的错误,这会禁用对所有定义的无用性检查.但是,仅此一项,这只会将错误推送到每次使用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,但除了在更高级别的背景下,这几乎已经过时了.(即便如此,一旦我们拥有类型lambda的东西,它真的会失去它的作用.)