Ответ 1
Интересная вещь случается, если вы рекламируете типы, индексированные продвинутыми типами. Представьте, что мы строим
data Nat = Ze | Su Nat
а затем
data Vec :: Nat -> * -> * where
VNil :: Vec Ze x
VCons :: x -> Vec n x -> Vec (Su n) x
За кулисами внутренние типы конструкторов представляют собой инстанцированные возвращаемые индексы с помощью ограничений, как если бы мы написали
data Vec (n :: Nat) (a :: *)
= n ~ Ze => VNil
| forall k. n ~ Su k => VCons a (Vec k a)
Теперь, если нам разрешили что-то вроде
data Elem :: forall n a. a -> Vec n a -> * where
Top :: Elem x (VCons x xs)
Pop :: Elem x xs -> Elem x (VCons y xs)
перевод во внутреннюю форму должен быть чем-то вроде
data Elem (x :: a) (zs :: Vec n a)
= forall (k :: Nat), (xs :: Vec k a). (n ~ Su k, zs ~ VCons x xs) =>
Top
| forall (k :: Nat), (xs :: Vec k s), (y :: a). (n ~ Su k, zs ~ VCons y xs) =>
Pop (Elem x xs)
но посмотрите на второе ограничение в каждом случае! Мы имеем
zs :: Vec n a
но
VCons x xs, VCons y xs :: Vec (Su k) a
Но в System FC, как тогда определено, ограничения равенства должны иметь типы одного и того же типа с обеих сторон, поэтому этот пример не является проблематичным.
В одном исправлении используется доказательство того, что первое ограничение фиксирует второе, но тогда нам понадобятся зависимые ограничения
(q1 :: n ~ Su k, zs |> q1 ~ VCons x xs)
Другое решение состоит в том, чтобы разрешить гетерогенные уравнения, как это было в теории зависимых типов пятнадцать лет назад. Там неизбежно будут уравнения между вещами, чьи виды равны таким образом, которые не являются синтаксически очевидными.
Это последний план, который в настоящее время пользуется преимуществом. Насколько я понимаю, упомянутая вами политика была принята в качестве холдинговой позиции до тех пор, пока не будет разработан проект для основного языка с гетерогенным равенством (предложенный Вейрихом и его коллегами). Мы живем в интересные моменты.