添加上下文以重寫規則

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是相同的），因爲它在默認情況下在重寫規則中處於打開狀態。