다시 쓰기 규칙에 컨텍스트 추가

Question

다음 코드에서 가능한 경우 g . f을 h으로 다시 작성하려고합니다. 경우가있을 수 있습니다 h 클래스의 인스턴스를 가지고 있지만 가능하면 재 작성을하고 싶습니다. 이것이 가능하다는 오류 메시지가 나타나지만 정확히 무엇을 변경해야하는지 확신 할 수 없습니다.

• 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"이 오류 인

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

: 여기

일부 샘플 코드이다. 이것은 일을 할 것처럼 보이지만, 실제로 어떻게하는지 잘 모르겠습니다. 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 #-} 

비슷 해요. 다행히, 나는 h에 x의 T a 유형의 형태 변수 a가 된 것과 동일하다는 것을 GHC를 알리기 위해 우리를 허용하여 TypeApplications이 문제에서 우리에게 방법을 제공합니다 생각 :

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

... 

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

우리는하지 않습니다 ScopedTypeVariables을 활성화해야합니다 (비록 우리가 a이 같은지 확인하기를 원한다고하더라도). 다시 쓰기 규칙에서 기본적으로 켜져 있기 때문입니다.