使用类型类约束重写规则

Question

有一些关于具有类型类约束的重写规则的previousquestions，但它们似乎涉及更高级别的多态性。在这里，我有一个更“普通”的情况，没有更高级别的类型和类型类约束，实际上应该已经由左侧的类型满足：

class C a where
    op :: a -> a

newtype Foo tag w = Foo{ runFoo :: w }

instance (Monoid w) => C (Foo tag w) where
    op = id

opSpecial :: (Monoid w) => Foo () w -> Foo () w
opSpecial _ = Foo mempty

{-# RULES
      "op/special" forall w. forall. op @(Foo () w) = opSpecial
  #-}

（这是一个非常简单的例子，想象一下

opSpecial

是外延上等价的，但操作上优于通用

op

）

重写规则无法进行类型检查，并显示以下错误消息：

rewrite-context.hs:13:55: error: [GHC-39999]
    • Could not deduce ‘Monoid w’ arising from a use of ‘opSpecial’
      from the context: C (Foo () w)
        bound by the RULE "op/special" at rewrite-context.hs:13:7-63
      Possible fix:
        add (Monoid w) to the context of the RULE "op/special"
    • In the expression: opSpecial
      When checking the rewrite rule "op/special"
   |
13 |       "op/special" forall w. forall. op @(Foo () w) = opSpecial

请注意，

Monoid w

已经是对多态实例

forall w. C (Foo tag w)

的约束，因此我希望每次调用

op @(Foo () w)

都能满足它。但是好吧，也许可能存在一些重叠/不连贯的实例，而没有该约束。然而，将约束添加到重写规则的语法是什么？ GHC 手册中有关重写规则的部分似乎没有描述任何将 添加（ing）

Monoid w

到

RULE

上下文的方式。

Answer 1

我发现的一个解决方法（实际上我还不是 100% 清楚它是解决方法还是正确的解决方案）是通过顶级函数定义通用

op

，使其

Monoid w

上下文直接：

instance (Monoid w) => C (Foo tag w) where
    op = opGeneric

{-# NOINLINE opGeneric #-}
opGeneric :: (Monoid w) => Foo tag w -> Foo tag w
opGeneric = id

（我们必须标记

opGeneric

NOINLINE

，以便重写规则有机会触发）

然后，可以更改重写规则以提及

opGeneric

而不是其 LHS 上重载的

op

：

opSpecial :: (Monoid w) => Foo () w -> Foo () w
opSpecial _ = Foo mempty

{-# RULES
      "op/special" forall w. forall. opGeneric @w @() = opSpecial
  #-}