Что означает эта переменная типа «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 

неоднозначных тип переменной `а» в ограничении:

`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, двусмысленность. Дело в том, что компилятор не может вывести , которыйmkI он должен использовать, поэтому мы должны это рассказать. Для этого мы должны принести переменные типа, используемые в области видимости, а затем сообщить компилятору в локальной сигнатуре, которая использует экземпляр типа.