haskell - 带有类型家族的歧义类型

Question

我遇到了 GHC 无法匹配的问题 Foo t和 Foo t0 ，在我看来它绝对像 t ~ t0 .这是一个最小的例子:

{-# LANGUAGE GADTs          #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies   #-}

data Foobar :: * -> * where
  Foobar :: Foo t -> Foobar t

type family Foo a :: *

class Bar t where
  f :: Foobar t
  g :: Foo t
--  f = Foobar g

取消注释最后一行时，GHC 提示:

Couldn't match expected type ‘Foo t’ with actual type ‘Foo t0’
NB: ‘Foo’ is a type function, and may not be injective
The type variable ‘t0’ is ambiguous
Relevant bindings include f :: Foobar t (bound at test.hs:13:3)
In the first argument of ‘Foobar’, namely ‘g’
In the expression: Foobar g

我明白 Foo不是单射的，但根据我的分析，GHC 从未被要求提出 t来自 Foo t .似乎是类型 t丢失于 Foobar g ，所以它不能匹配首字母 Foo t和新 Foo t0 .这里的上下文还不够吗？我是否错过了一个案例，其中 f = Foobar g无法产生正确的结果？

任何帮助表示赞赏!

注意: ScopedTypeVariables和显式类型签名似乎没有帮助。添加约束 a ~ Foo t并使用 a而是作为 g 的类型在 Foobar g也不起作用。

看起来很像: ambiguous type error when using type families, and STV is not helping .我考虑使用 Proxy ，但我觉得在这种情况下 GHC 应该能够弄清楚。

Answer 1

I understand that Foo is not injective, but from my analysis GHC is never asked to come up with t from Foo t.

所以，你意识到了歧义。让我们明确:

type instance Foo ()   = Bool
type instance Foo Char = Bool

instance Bar () where
   -- I omit the declaration for f
   g = True
instance Bar Char where
   g = False

main = print (g :: Bool)

您的问题在 f = Foobar g与歧义有关。

关键是:定义 f = Foobar g并不意味着 g在与 f 相同的实例中选择更多.它可以指不同的实例!

考虑

show (x,y) = "(" ++ show x ++ ", " ++ show y ++ ")"

以上，RHS 使用 show来自与 LHS show 所在的实例不同的实例是。

在您的 f = Foobar g行，GHC 推断 g :: Foo t哪里 t与 f 的索引相同实例。然而，这还不足以为 g 选择一个实例。 !事实上，我们可能有 Foo t ~ Foo t0对于其他一些 t0 ，因此 g可以引用 g在 t0例如，导致歧义错误。

请注意，即使最后一行被注释掉，您的代码也会被 GHC 8 拒绝，因为 g 的类型本质上是模棱两可的:

• Couldn't match expected type ‘Foo t’ with actual type ‘Foo t0’
  NB: ‘Foo’ is a type function, and may not be injective
  The type variable ‘t0’ is ambiguous
• In the ambiguity check for ‘g’
  To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
  When checking the class method: g :: forall t. Bar t => Foo t
  In the class declaration for ‘Bar’

我们可以按照建议让 GHC 8 更宽松，就像 GHC 7。这将使您的代码类型检查，直到我们取消最后一行的注释。

• Couldn't match expected type ‘Foo t’ with actual type ‘Foo t0’
      NB: ‘Foo’ is a type function, and may not be injective
      The type variable ‘t0’ is ambiguous

这与您在 GHC 7 中看到的错误相同。
在 GHC 8 中，我们还有一个奢侈:我们可以明确选择 t为 g如下:

class Bar t where
  f :: Foobar t
  f = Foobar (g @ t)
  g :: Foo t

当然，这需要打开更多扩展。在 GHC 7 中，您需要一个代理才能明确地选择一个实例。