为什么不能在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页上进一步指出：“的确，我们知道通过对递归新类型的处理……该算法是不完整的”（即，存在无法由类型推断出的类型安全强制）实施的算法）。您可能还希望浏览问题#15928中有关类似循环的讨论。

这里发生的是，GHC首先通过拆开新类型以产生新目标来尝试解决Coercible (Hyper a b) (Hyper a c)：

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

[这需要GHC首先解开新类型以产生新目标的Coercible (Hyper b a) (Hyper c a)：

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是解决之道。