PolyKinds的不明确类型

Question

以下编译没有 PolyKinds:

{-# LANGUAGE TypeFamilies, GADTs #-}

type family Modulus zq

type family Foo zq q

data Bar :: (* -> *) where
    Bar :: (zq' ~ Foo zq (Modulus zq)) => Bar (zq -> zq')

所有外观zq都是某种类型(种类*)代表模数运算模型q.用它Nats来表示这些模量很方便.如果我PolyKinds在类型族中添加和多样化模数:

{-# LANGUAGE TypeFamilies, GADTs, PolyKinds #-}

type family Modulus zq :: k

type family Foo zq (q :: k)

data Bar :: (* -> *) where
    Bar :: (zq' ~ Foo zq (Modulus zq)) => Bar (zq -> zq')

GHC 7.8抱怨:

Could not deduce (zq' ~ Foo zq (Modulus zq))
...
In the ambiguity check for:
  forall zq' zq. zq' ~ Foo zq (Modulus zq) => Bar (zq -> zq')
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the definition of data constructor ‘Bar’

添加PolyKinds 真的让这个含糊不清吗？歧义在哪里？还有关系:什么时候-XAllowAmbiguousTypes合适？

如果我向GHC抛出一个骨骼并添加AllowAmbiguousTypes错误从GADT的声明移动到使用 GADT(没有添加扩展名的建议):

bar :: (zq' ~ Foo zq (Modulus zq))
  => Bar (zq -> zq')
bar = Bar

这让我觉得使用的AllowAmbiguousTypes是GHC红鲱鱼.

编辑

为了澄清,上面的类型可以实例化如下:

newtype Zq q = Zq Int

然后zq ~ (Zq 3),q ~ 3和Modulus (Zq 3) ~ 3,Foo (Zq 3) 3 ~ (Zq 3)(我将这项工作从Foo类型系列中剥离出来,因此将其视为身份.)

Answer 1

让我们暂时限制zq论证*:

type family Modulus (zq :: *) :: k

type family Foo (zq :: *) (q :: k)

然后你得到一个稍好的错误信息,可以通过说-fprint-explicit-kinds(假设GHC 7.8)进一步改进:

Could not deduce ((~) * zq' (Foo k0 zq (Modulus k0 zq)))
from the context ((~) * zq' (Foo k zq (Modulus k zq)))

所以问题在于Modulus它的输出类型Foo是多态的,并且在其输入类型中是多态的.没有什么可以解决这种中间类型,所以它仍然是模棱两可的.修复它的一个选择是使用Proxy:

import Data.Proxy

...

data Bar :: (* -> *) where
    Bar :: (m ~ Modulus zq, zq' ~ Foo zq m) => Proxy m -> Bar (zq -> zq')

现在你甚至可以删除和再次*注释,它仍然可以工作.ModulusFoo