为什么不能在 GHC 中强制超功能？

Question

我有以下类型，基于论文Coroutining folds with hyperfunctions：

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

它的第一个参数是逆变的，第二个参数是协变的，所以它是一个profunctor：

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

我不认为这是一个错误；相反，这是用于推断类型安全强制的算法的限制。在描述该算法的the paper 中，承认类型检查递归新类型可能会发散，并且“按设计”行为是减少计数器将检测循环并报告错误。 （例如，参见第 27 页。）在第 30 页上进一步指出，“事实上，我们知道它对递归新类型的处理......算法是不完整的”（即，存在无法推断的类型安全强制实现的算法）。您可能还想浏览 issue #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 b c 和Hyper 的第二个参数的代表角色派生Coercible (Hyper a b) (Hyper a c)。

不幸的是，整个算法都是语法导向的，所以新类型总是会以这种方式展开，并且没有办法让 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 是要走的路。