Блог

В синонимах связанного типа (Чакраварти, Келлер, Джонс) в документе, по-видимому, указывается, что допустимо следующее:

 class C a where
  type S a (k :: * -> *) :: *
  

Однако, когда я пытаюсь запустить это, я получаю ошибку компилятора (с -XTypeFamilies ):

 Not in scope: type variable `k'
  

Я что-то упускаю, или фактическая реализация в GHC не совпадает с тем, что упоминается в документе?

Как вы уже выяснили, это невозможно в GHC:

Точно так же, как и в случае объявления связанных данных, именованные параметры типа должны быть перестановкой подмножества параметров класса. Примеры

 class C a b c where { type T c a :: * }   -- OK
class D a where { type T a x :: * }       -- No: x is not a class parameter
class D a where { type T a :: * -> * }    -- OK
  

Тикет, на который вы ссылались, на самом деле объясняет причину невозможности определить что-то вроде S . Это работает, если вы делаете это следующим образом:

 class C a where
    type S a :: (* -> *) -> *
data TupK a k = TupK (a, k a)
instance C [a] where
    type S [a] = TupK a
  

Однако теперь вы застряли с новым типом данных. Использование синонимов типов не будет работать («Синоним типа `TupK’ должен иметь 2 аргумента»), и добавление дополнительных параметров к S не поможет («Количество параметров должно соответствовать объявлению семейства; ожидается 1»), как задокументировано в заявке.

Нет, но вы можете использовать менее мощный:

 class C a where
  type S a :: (k :: * -> *) -> *
  

… который мог бы служить той же цели, если вам не нужна дополнительная мощность.