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

Question

我有以下类型，它基于论文Cooutining 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

我不认为这是一个错误；相反，这是用于推断类型安全强制的算法的限制。在描述该算法的论文中，承认类型检查递归新类型可能会发散，并且“按设计”行为是归约计数器将检测循环并报告错误。（例如，参见第 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 的示例中所示，这是因为新类型的展开行为。如果将新类型切换为 a data，它可以正常工作，因为 GHC 不会尝试解包，而是可以Coercible (Hyper a b) (Hyper a c)直接从的第二个参数Coercible b c的代表性角色派生。Hyper

不幸的是，整个算法是语法控制的，因此新类型总是以这种方式展开，并且没有办法让 GHC “推迟”展开并尝试替代证明。

除了... Newtypes 仅在构造函数在范围内时才会展开，因此您可以将其分成两个模块：

-- 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这就是要走的路。