Семейства типов и инъективность в подмножестве индексов

Question

У меня есть следующий тип семьи:

{-# LANGUAGE TypeFamilyDependencies #-}

type family Const arr r = ret | ret -> r where
  Const (_ -> a) r = Const a r
  Const _  r = r

Это просто Const замаскированная функция, но проверка на приемистость GHC 8.2.1 не распознает ее как инъективную по отношению к на его второй аргумент:

    * Type family equation violates injectivity annotation.
      RHS of injective type family equation cannot be a type family:
        Const (_ -> a) r = Const a r
    * In the equations for closed type family `Const'
      In the type family declaration for `Const'
  |
4 |       Const (_ -> a) r = Const a r
  |       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Если вы пропустите первый случай, он сработает, что наводит меня на мысль, что функциональность есть, но еще не совсем зрелая.

Могу ли я сформулировать это как-то иначе, чтобы GHC распознал инъективность? Это на самом деле для этого чуть более сложного случая (так arr действительно используется):

{-# LANGUAGE TypeFamilyDependencies #-}

type family ReplaceRet arr r = ret | ret -> r where
  ReplaceRet (a -> b) r = a -> ReplaceRet b r
  ReplaceRet _  r = r

Answer 1

Вы предлагаете

type family ReplaceRet arr r = ret | ret -> r where
  ReplaceRet (a -> b) r = a -> ReplaceRet b r
  ReplaceRet _  r = r

но

ReplaceRet (Int -> Bool) Char = Int -> Char
ReplaceRet Bool (Int -> Char) = Int -> Char

Таким образом, это не правда, что с учетом retмы можем вывести r, Мы не можем иметь ret -> r зависимость.

Мы могли бы иметь arr ret -> r вместо этого, но, насколько мне известно, GHC (пока?) не поддерживает такого рода зависимости от семейств типов.

Const a b выглядит так, как будто это уважает ret -> b, Однако обнаружение этого требует индуктивного доказательства, и GHC не настолько умен, чтобы это делать. Решить вопрос об инъективности на самом деле довольно сложно: см. Неуклюжие случаи в статье, в разделе 4.1, для нескольких сюрпризов. Чтобы преодолеть эти проблемы, GHC должен был быть разработан, чтобы быть консервативным в том, что он принимает.