Почему GHC считает, что переменная этого типа не является инъективной?

У меня есть эта часть кода:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, KindSignatures, GADTs, FlexibleInstances, FlexibleContexts #-}

class Monad m => Effect p e r m | p e m -> r where
  fin :: p e m -> e -> m r

data ErrorEff :: * -> (* -> *) -> * where 
  CatchError :: (e -> m a) -> ErrorEff ((e -> m a) -> m a) m

instance Monad m => Effect ErrorEff ((e -> m a) -> m a) a m where
  fin (CatchError h) = \f -> f h

Это не скомпилируется с этой ошибкой типа в последней строке:

Could not deduce (a1 ~ a)
from the context (Monad m)
[...]
or from (((e -> m a) -> m a) ~ ((e1 -> m a1) -> m a1))
[...]

Если я изменяю m на [], он компилируется отлично, поэтому, по-видимому, GHC считает, что m не является инъективным. (Хотя он не предупреждает об инъективности, как это происходит с семействами типов.)

Моя версия GHC - это 7.2.1.

Изменить: если я изменяю (e -> m a) на e, он работает, если я его изменяю на m a, это не так, и ни для (m a -> e).

Ответ 1

Это не совсем ошибка, но это долгая история...

История

В 7.0 существовал конструктор coercion под названием right, который работал следующим образом:

g : f a ~ f b
---------------
right g : a ~ b

То есть, если g является принуждением между f a и f b, тогда right g является принуждением между a и b. Это звучит только тогда, когда f гарантированно будет инъективным: иначе мы могли бы законно иметь, скажем, f Int ~ f Char, а затем мы могли бы заключить Int ~ Char, что было бы плохо.

Но, конечно, синонимы типов и семейства типов не обязательно являются инъективными; например:

type T a = Int

type family F a :: *
type instance F Int  = Bool
type instance F Char = Bool

Итак, как эта гарантия возможна? Ну, именно по этой причине частичные приложения синонимов типов и семейств типов не допускаются. Частичные применения синонимов типов и семейств типов могут быть неинъективными, но насыщенные приложения (даже те, которые приводят к более высокому виду) всегда.

Конечно, ограничение на частичные приложения раздражает. Таким образом, в 7.2, пытаясь двигаться в направлении разрешения частичного приложения (и потому, что это упрощает теорию и реализацию языка принуждения), конструктор right был заменен конструктором nth, с сопровождающим правилом

g : T a1 .. an ~ T b1 .. bn
---------------------------
nth i g : ai ~ bi

То есть, nth применяется только к принуждению g, которое находится между двумя типами, которые, как известно, являются насыщенными приложениями конструктора типов T. Теоретически это допускает частичное применение синонимов типов и семейств, поскольку мы не можем разлагать равенства, пока не узнаем, что они находятся между приложениями конструктора типа (обязательно инъективного). В частности, nth не применяется к принуждению f a ~ f b, потому что f является переменной типа, а не конструктором типа.

Было подумано, что в момент изменения никто не заметил бы, но, очевидно, это было неправильно!

Интересно, что трюк Олегана, описанный в сообщении haskell-cafe от Daniel Schüssler, показывает, что внедрение семейств типов не было соответствующим образом изменено! Проблема в том, что определение типа

type family Arg fa
type instance Arg (f a) = a

не допускается, если f может быть неинъективным; в этом случае определение даже не имеет смысла.

Следующие шаги

Я думаю, что правильная вещь - восстановить right (или что-то подобное), поскольку люди явно этого хотят! Надеюсь, это будет сделано в ближайшее время.

Тем временем было бы действительно здорово разрешить частично применяемые синонимы типов и семьи. Кажется, правильный способ (tm) сделать это будет для отслеживания инъективности в системе вида: то есть каждый вид стрелки будет аннотирован с его инъективностью. Таким образом, когда мы сталкиваемся с равенством f a ~ f b, мы можем посмотреть на тип f, чтобы определить, можно ли его разложить в равенство a ~ b. Не случайно, в настоящее время я пытаюсь разработать дизайн такой системы. =)

Ответ 2

Я не уверен в этой причине, но я уменьшил ваш тестовый файл до:

{-# LANGUAGE GADTs #-}

data ErrorEff x where
  CatchError :: m a -> ErrorEff (m a)

fin :: ErrorEff (m a) -> m a
fin (CatchError h) = h

который компилируется в GHC 7.0.3, но не 7.3.20111021.

Это определенно ошибка компилятора.

Скомпилируется после изменения:

data ErrorEff x where
  CatchError :: x -> ErrorEff x

И функция "fin" может быть восстановлена с помощью синтаксиса записи:

data ErrorEff x where
  CatchError :: { fin :: m a } -> ErrorEff (m a)