添加上下文以重写规则

Question

在下面的代码中，我想尽可能将g . f 重写为h。可能有些情况h 没有类的实例，但我想在可能的情况下进行重写。我收到一条错误消息，提示这是可以实现的，但我不确定我需要更改什么。

这里是一些示例代码：

{-# LANGUAGE TypeFamilies #-}

main = return ()

data D a

f :: a -> D a
f = undefined

type family T a

class G a where
  g :: D (T a) -> a

class H a where
  h :: T a -> a

{-# RULES
  "myrule" forall x. g (f x) = h x
#-}

这是错误：

• Could not deduce (H a) arising from a use of ‘h’
  from the context: G a
    bound by the RULE "myrule" at trickyrewrite.hs:19:3-34
  Possible fix: add (H a) to the context of the RULE "myrule"
• In the expression: h x
  When checking the transformation rule "myrule"

注意可能的修复方法：add (H a) to the context of the RULE "myrule"。这似乎可以完成这项工作，但我不确定如何实际做到这一点。 a 甚至没有在规则中提及，所以我不确定当 a 不涉及任何内容时添加 H a 会有什么帮助。

如果有什么不同，我控制的唯一代码是类H。我无法更改G。我的代码当然比这更复杂，但是如果我能看到一个如何让这个简化的例子工作的例子，我应该能够计算出我认为的代码。

尝试失败：

我在下面尝试了@Alec 的建议，但它似乎不起作用，重写规则没有被触发。这是我尝试过的代码：

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeApplications #-}

module Main where

main = ((g (f (2 :: Int))) :: Char) `seq` return () 

data D a

{-# INLINE [1] f #-}
f :: a -> D a
f = undefined

type family T a
type instance T Char = Int

{-# INLINE [1] g' #-}
g' :: (G a) => D (T a) -> a
g' = undefined

class G a where
  g :: D (T a) -> a
  g = g'

instance G Char

class H a where
  h :: T a -> a

{-# RULES
  "myrule" forall (x :: H a => T a). g' (f x) = h @a x
#-}

Answer 1

通常，one can add type signatures to the variables in the forall。类似的东西

{-# RULES "myrule" forall (x :: H a => T a). g (f x) = h x #-}

现在，这在这种情况下完全不起作用，因为T 可能不是单射的。幸运的是，我认为TypeApplications 为我们提供了解决这个问题的方法，它允许我们通知 GHC，x 的类型 T a 中的类型变量 a 与 h 中的变量相同：

{-# LANGUAGE TypeFamilies, TypeApplications, AllowAmbiguousTypes #-}

 ...

{-# RULES "myrule" forall (x :: H a => T a). g (f x) = h @a x #-}

我们不需要启用ScopedTypeVariables（即使我们依赖它来确保as 相同），因为它在重写规则中默认处于启用状态。