Cosa significa questa 'Variabile di tipo ambiguo `a` nel vincolo'?

Question

In questo codice sto cercando di fare in modo che il primo parametro nella mia funzione di lavoro go sia un tipo "famiglia di tipi".Vedo che nella documentazione delle famiglie di tipi type una funzione insert simile appartiene alla classe type, mentre nel mio esempio qui sottonon è così.

Sono nuovo nella digitazione delle famiglie, quindi forse le sto usando in modo sbagliato, ma cosa significa questo errore?

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

Variabile di tipo ambiguo "a" nel vincolo:

`K a'

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

Probabile correzione: aggiungi una firma del tipo che risolva queste variabili di tipo

Answer 1

Questo 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

Cosa ho cambiato e perché?

Innanzitutto, ho pensato che volessi il vincolo su M, quindi ho utilizzato una forma di definizione del tipo che impone il vincolo e lo rende disponibile nei siti di utilizzo, un GADT.

In secondo luogo, il problema di cui si è lamentato il tuo GHC, l'ambiguità.Il punto è che non c'è modo per il compilatore di dedurre quale mkI dovrebbe usare, quindi dobbiamo dirlo.Per questo, dobbiamo portare le variabili di tipo usate nello scope e poi dire al compilatore nella firma locale quale istanza di tipo usare.