書き換えルールにコンテキストを追加する

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 
#-} 

アンこれは誤りである：ここで

は、いくつかのサンプルコードですadd (H a) to the context of the RULE "myrule"：

• 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" 

可能性の修正に注意してください。これは仕事をするようですが、私は実際にこれを行う方法がわかりません。 aはルールにも言及されていないので、が何も参照していないときにH 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です。 Tは単射ではないかもしれないので、この場合ではないかなり作業を行い今

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

、のようなもの。幸い、私はTypeApplicationsは私たちに私たちはxの種類T aでa変数の型がhにおけるものと同じであることをGHCに通知することを可能にすることによって、この問題から抜け出す方法を与えると思う：

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

... 

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

は行っておりませんScopedTypeVariablesを有効にする必要があります（aが同じであることを確認する場合でも）。これは、デフォルトでは書き換えルールでオンになっているためです。