What does this 'Ambiguous type variable `a` in the constraint' mean?

Question

In this code I am trying to have the first parameter in my worker function go be a 'type family' type. I see that in the type type families documentation a similar insert function belongs to the type class, while in my example below it does not.

I am new to type families so maybe I am using them wrong, but what does this error mean?

{-# 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

Ambiguous type variable `a' in the constraint:

`K a'

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

Probable fix: add a type signature that fixes these type variable(s)

Answer 1

This compiles:

{-# 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

What have I changed and why?

First, I assumed that you wanted the constraint on M, so I used a form of type definition that enforces the constraint and makes it available at use sites, a GADT.

Second, the problem your GHC complained about, the ambiguity. The point is that there's no way for the compiler to deduce which mkI it should use, so we have to tell it. For that, we must bring the type variables used into scope and then tell the compiler in the local signature which type instance to use.