这个“约束中的歧义类型变量‘a’”是什么意思？

Question

在这段代码中，我试图让工作函数go 中的第一个参数成为“类型族”类型。我看到在type families documentation 类型中，类似的insert 函数属于类型类，而在下面的示例中它不属于。

我是类型族的新手，所以也许我用错了，但是这个错误是什么意思？

{-# LANGUAGE TypeFamilies #-}

-- | key
class K a where
  -- | iterator for key
  type I a :: *
  mkI :: a -> I a

--| A map
data (K a) => M a b = M a b

insert :: (K a) => a -> b -> M a b -> M a b
insert = go mkI    -- <<< PROBLEM
  where
    go o a b m = m

约束中的模糊类型变量“a”：

`K a'

  arising from an expression type signature at Data/Map2.hs:167:10-33

可能的修复：添加修复的类型签名 这些类型变量

Answer 1

这样编译：

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

-- | key
class K a where
  -- | iterator for key
  type I a :: *
  mkI :: a -> I a

-- | A map
data M x y where
    M :: K a => a -> b -> M a b

insert :: forall a b. (K a) => a -> b -> M a b -> M a b
insert = go mkI
  where
    go :: (a -> I a) -> a -> b -> M a b -> M a b
    go o a b m = m

我改变了什么？为什么？

首先，我假设您想要M 上的约束，所以我使用了一种类型定义形式来强制约束并使其在使用站点上可用，即GADT。

其次，您的 GHC 抱怨的问题是模棱两可。关键是编译器无法推断它应该使用 which mkI，所以我们必须告诉它。为此，我们必须将使用的类型变量带入作用域，然后在本地签名中告诉编译器要使用哪个类型实例。