
Basically, I want to rewrite `g (f x)` with `h x` where it's valid to do so (i.e. appropriate instances of `h` exist). The code I've put below is a silly example just to illustrate the issue. I guess the tricky thing is that whether the rewrite rule can fire depends on the result of `g (f x)`, not just x itself. Does anyone know how to adjust this so the rewrite rule fires? {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeApplications #-} module Main where 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 main = ((g (f (2 :: Int))) :: Char) `seq` return () {-# RULES "myrule" forall (x :: H a => T a). g' (f x) = h @a x #-}