== Notes on the implementation of rewrite RULEs in GHC ==

=== Looking through lets ===

We recently made the rule-matcher able to "look through" lets, thus
{{{
   RULE f (g x) = rhs

   Expression:  f (let v = e in g v)
}}}
  The rule will still match, giving
{{{
   let v = e in rhs[v/x]
}}}

=== Dictionaries ===

Suppose we have
{{{
  RULE f (g x) = rhs

  f :: Ord a => a -> a

  foo :: Int -> Int
  foo x = f (g x)
}}}
Then we tend to get
{{{
  f_79 :: Int -> Int
  f_79 = f Int dOrdInt

  foo :: Int -> Int
  foo = \x -> f_79 (g x)
}}}
Lo, the f/g RULE cannot fire. 

Current solution: use {{{-fno-method-sharing}}} to get
{{{
  foo :: Int -> Int
  foo = \x -> f Int dOrdInt (g x)
}}}
But we found other examples where this wasn't enough.  Code is below.  The solution is: use {{{-fdicts-cheap}}}, which makes dictionary construction look really cheap.

Example of when -fno-method-sharing isn't enough.
{{{
module Foo where

data UArr a = UArr [a]

class UA a where
  ua :: [a] -> [a]

instance UA Int where
  ua xs = xs

class DT a where
  foo :: a -> a
  bar :: a -> a

instance DT Int where
  foo x = x
  bar x = x

instance (DT a, DT b) => DT (a,b) where
  foo x = x
  bar x = x

instance UA a => DT (UArr a) where
  foo x = x
  bar x = x

data Dist a = Dist a

mapD :: (DT a, DT b) => (a -> b) -> Dist a -> Dist b
{-# INLINE [1] mapD #-}
mapD f (Dist x) = Dist (f x)

zipWithD :: (DT a, DT b, DT c) => (a -> b -> c) -> Dist a -> Dist b ->
Dist c
{-# INLINE zipWithD #-}
zipWithD f (Dist x) (Dist y) = mapD (uncurry f) (Dist (x,y))

splitD :: UA a => UArr a -> Dist (UArr a)
{-# INLINE [1] splitD #-}
splitD x = zipWithD const (Dist x) (Dist x)

joinD :: UA a => Dist (UArr a) -> UArr a
{-# INLINE [1] joinD #-}
joinD (Dist x) = x

{-# RULES

"split/join" forall x.
  splitD (joinD x) = x

 #-}

------

module Bar where

import Foo

foo :: Dist (UArr Int) -> Dist (UArr Int)
foo = splitD . joinD

------

Compared to the previous version, the important differences are

  - the class UA and the instance DT (UArr a) which builds a DT 
    dictionary from an UA one,
  - splitD . joinD instead of splitD (joinD x) in foo.

With this, we get

------

15 splitD :: UA a => UArr a -> Dist (UArr a)
     {- Arity: 1 HasNoCafRefs Strictness: A Inline: [1]
	Unfolding: (__inline_me (\ @ a $dUA :: UA a ->
				 let {
				   $dDT :: DT (UArr a) = $f1 @ a $dUA
				 } in
				 \ x :: UArr a ->
				 zipWithD
				   @ (UArr a)
				   @ (UArr a)
				   @ (UArr a)
				   $dDT
				   $dDT
				   $dDT
				   (GHC.Base.const @ (UArr a) @ (UArr a))
				   (Dist @ (UArr a) x)
				   (Dist @ (UArr a) x))) -}

------

and the rule doesn't fire. Nor does it with

  foo x = splitD $ joinD x

But it *does* fire with

  foo x = splitD (joinD x)

despite the arity of splitD. Very strange...

Roman
}}}