<div dir="ltr"><div>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. <br><br>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. </div><div><br></div><div>Does anyone know how to adjust this so the rewrite rule fires?</div><div><br></div><div>    {-# LANGUAGE TypeFamilies #-}</div><div>    {-# LANGUAGE TypeApplications #-}</div><div>    </div><div>    module Main where</div><div>        </div><div>    data D a</div><div>    </div><div>    {-# INLINE [1] f #-}</div><div>    f :: a -> D a</div><div>    f = undefined</div><div>    </div><div>    type family T a</div><div>    type instance T Char = Int</div><div>    </div><div>    {-# INLINE [1] g' #-}</div><div>    g' :: (G a) => D (T a) -> a</div><div>    g' = undefined</div><div>    </div><div>    class G a where</div><div>      g :: D (T a) -> a</div><div>      g = g'</div><div>    </div><div>    instance G Char</div><div>    </div><div>    class H a where</div><div>      h :: T a -> a</div><div><br></div><div>    main = ((g (f (2 :: Int))) :: Char) `seq` return () </div><div>    </div><div>    {-# RULES</div><div>      "myrule" forall (x :: H a => T a). g' (f x) = h @a x</div><div>    #-}</div><div><br></div></div>