Добавление контекста для перезаписи правил

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, что переменная a типа в типе T a из x такой же, как тот, в h:

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

... 

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

Мы не необходимо включить ScopedTypeVariables (даже если мы полагаемся на него, чтобы убедиться, что a s одинаковы), поскольку он включен по умолчанию в правилах перезаписи.