haskell - 使用通用量化约束重写规则/特化类型错误

Question

我正在尝试实现一些特定于类型的特化 一些与 Prisms 一起使用的功能，我在使用时遇到了困难 GHC 8。(我遇到了 GHC < 8 的不同问题，但那就是 另一个问题)。

问题的(人为的)最小示例:

foo :: Prism' s a -> Prism' s a
foo = id

{-# RULES "foo/foo'" foo = foo' #-}
foo' :: Prism' Char Bool -> Prism' Char Bool
foo' = id

这会导致编译器错误:

error:
• Couldn't match type ‘p0 Bool (f0 Bool) -> p0 Char (f0 Char)’
                 with ‘forall (p :: * -> * -> *) (f :: * -> *).
                       (Choice p, Applicative f) =>
                       p Bool (f Bool) -> p Char (f Char)’
  Expected type: Prism' Char Bool
    Actual type: p0 Bool (f0 Bool) -> p0 Char (f0 Char)
• In the expression: foo'
  When checking the transformation rule "foo/foo'"

在我看来，这就像重写规则类型检查的一方面 “忘记”它的上下文。这里究竟发生了什么以及如何发生 我能让 GHC 高兴吗？

Answer 1

这本质上是一个老问题，即 N 级类型没有形成适当的层次结构来确定哪种类型更通用，哪种类型不太通用。看起来这个特定情况可以可以解决，但是肯定不可能为一般的 N 级函数编写重写规则。

幸运的是，这对于镜头和 friend 来说并不是什么大问题，因为它们始终有可用的单态版本!

foo₀ :: APrism' s a -> APrism' s a
foo₀ = id

{-# RULES "foo/foo'" foo₀ = foo' #-}
foo' :: APrism' Char Bool -> APrism' Char Bool
foo' = id

foo :: Prism' s a -> Prism' s a
foo p = clonePrism $ foo₀ (clonePrism p)