Почему в GHC нельзя принудить гиперфункции?

Question

У меня есть следующий тип, который основан на бумажной свертке Coroutining с гиперфункциями:

newtype Hyper a b = Hyper { invoke :: Hyper b a -> b }

Он контравариантен по первому аргументу и ковариантен по второму, так что это профунктор:

instance Profunctor Hyper where
  lmap f = go where
    go (Hyper h) = Hyper $ \(Hyper k) -> h $ Hyper $ f . k . go

  rmap g = go where
    go (Hyper h) = Hyper $ \(Hyper k) -> g $ h $ Hyper $ k . go

  dimap f g = go where
    go (Hyper h) = Hyper $ \(Hyper k) -> g $ h $ Hyper $ f . k . go

Я также хочу реализовать (потенциально небезопасные) операторы приведения:

  -- (#.) :: Coercible c b => q b c -> Hyper a b -> Hyper a c
  (#.) _ = coerce

  -- (.#) :: Coercible b a => Hyper b c -> q a b -> Hyper a c
  (.#) = const . coerce

Однако при этом я получаю следующее сообщение об ошибке:

   • Reduction stack overflow; size = 201
     When simplifying the following type:
       Coercible (Hyper a b) (Hyper a c)
     Use -freduction-depth=0 to disable this check
     (any upper bound you could choose might fail unpredictably with
      minor updates to GHC, so disabling the check is recommended if
      you're sure that type checking should terminate)
   • In the expression: coerce
     In an equation for ‘#.’: (#.) _ = coerce

Я думаю, он пытается проверить Coercible (Hyper a b) (Hyper a c), что требует Coercible b c а также Coerrcible (Hyper c a) (Hyper b a), а последнее требует Coercible (Hyper a b) (Hyper a c), но идет бесконечный цикл.

Есть идеи, какие аннотации я бы использовал, чтобы исправить это, если таковые имеются? Или я должен просто укусить пулю и использоватьunsafeCoerce?

Answer 1

Я полагаю ясно, что Profunctor экземпляры здесь не играют никакой роли, поэтому следующая автономная программа выдает ту же ошибку:

import Data.Coerce
newtype Hyper a b = Hyper { invoke :: Hyper b a -> b }
(#.) :: (Coercible c b) => q b c -> Hyper a b -> Hyper a c
(#.) _ = coerce

Я не думаю, что это ошибка; скорее, это ограничение алгоритма, используемого для вывода типобезопасных приведений. В документе, описывающем алгоритм, признается, что рекурсивные новые типы проверки типов могут расходиться, а поведение "как задумано" заключается в том, что счетчик сокращения обнаруживает цикл и сообщает об ошибке. (См., Например, стр. 27). Далее на стр. 30 отмечается, что "действительно, мы знаем, что с его обработкой рекурсивных новых типов... алгоритм является неполным" (т. Е. Что есть типобезопасные приведения, которые не могут быть выведены с помощью алгоритм в том виде, в котором он реализован). Вы также можете просмотреть обсуждение в выпуске № 15928 относительно аналогичного цикла.

Здесь происходит то, что GHC пытается решить Coercible (Hyper a b) (Hyper a c) сначала развернув новые типы, чтобы достичь новой цели:

Coercible (Hyper b a -> b) (Hyper c a -> c)

Это требует Coercible (Hyper b a) (Hyper c a) который GHC пытается решить, сначала разворачивая новые типы, чтобы достичь новой цели:

Coercible (Hyper a b -> a) (Hyper a c -> a)

что требует Coercible (Hyper a b) (Hyper a c), и мы попали в петлю.

Как и в примере с проблемой #15928, это связано с поведением разворачивания новых типов. Если вы переключите новый тип наdata, он работает нормально, поскольку GHC не пытается развернуть и вместо этого может получить Coercible (Hyper a b) (Hyper a c) прямо из Coercible b c и репрезентативная роль HyperВторой параметр.

К сожалению, весь алгоритм ориентирован на синтаксис, поэтому новые типы всегда будут разворачиваться таким образом, и нет никакого способа заставить GHC "отложить" развертывание и попробовать альтернативное доказательство.

За исключением того, что есть... Новые типы разворачиваются только в том случае, если конструктор входит в область видимости, поэтому вы можете разделить его на два модуля:

-- HyperFunction.hs
module HyperFunction where
newtype Hyper a b = Hyper { invoke :: Hyper b a -> b }

-- HyperCoerce.hs
module HyperCoerce where
import HyperFunction (Hyper)  -- don't import constructor!
import Data.Coerce
(#.) :: (Coercible c b) => q b c -> Hyper a b -> Hyper a c
(#.) _ = coerce

и он типа проверяет нормально.

Если это слишком некрасиво или вызывает другие проблемы, я думаю unsafeCoerce это путь.