¿Qué significa esta 'Variable de tipo ambiguo' a` en la restricción '?

Question

En este código, estoy intentando que el primer parámetro en mi función de trabajador go sea del tipo 'tipo familia'. Veo que en el tipo type families documentation una función similar insert pertenece a la clase de tipo, mientras que en mi ejemplo a continuación no.

Soy nuevo para escribir familias, así que tal vez las estoy usando incorrectamente, pero ¿qué significa este error?

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

ambiguo variable de tipo `a' de la restricción:

`K a' 

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

solución probable: añadir una firma tipo que fija estas variables (s) Tipo de

Answer 1

Esto compila :

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

¿Qué he cambiado y por qué?

En primer lugar, asumí que quería la restricción en M, así que utilicé una forma de definición de tipo que impone la restricción y la pone a disposición en los sitios de uso, un GADT.

En segundo lugar, el problema que su GHC se quejó, la ambigüedad. El punto es que no hay forma de que el compilador deduzca quemkI debería usar, así que tenemos que decirlo. Para eso, debemos traer las variables de tipo utilizadas en el alcance y luego decirle al compilador en la firma local qué tipo de instancia usar.