[Haskell-cafe] Getting a rewrite rule to fire

[David Feuer]

I'm pretty sure this *won't* work. First off, there are known issues
with class methods showing up anywhere in RULES. But more
fundamentally, the whole instance resolution mechanism drops away
after type checking. The simplifier, which is responsible for applying
RULES, has no idea whether a type is an instance of a class.

On Fri, Feb 17, 2017 at 4:57 PM, Clinton Mead <clintonmead at gmail.com> wrote:
> 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
>     #-}
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.