Ответ 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. Не случайно, в настоящее время я пытаюсь разработать дизайн такой системы. =)