添加上下文以重写规则

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，所以我不知道H a如何在a没有引用任何内容时有所帮助。

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

失败的尝试：

我已经试过以下@亚历克的建议，但它似乎没有工作，重写规则不被触发。以下是我试过的代码：

{-# 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，在类型的xT a类型变量a是一样的一个在h：

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

... 

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

我们不需要启用ScopedTypeVariables（即使我们依靠它来确保a是相同的），因为它在默认情况下在重写规则中处于打开状态。