[Haskell-cafe] Getting a rewrite rule to fire

[Clinton Mead]

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
    #-}
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20170218/3274daec/attachment.html>