Casts, rules, and parametricity

Pedro wrote this long message about the way that his generic-programming was not optimising as it should:

My reply was in two parts. The first was fairly simple. The second I reproduce below because it highlights a tricky ineraction between RULES and casts, which I don't know how to solve.

Pedro wondered why it made a difference whether you said

   instance GEnum Nat where
     genum = map to genum'
or
   instance GEnum Nat    -- Fill in from default method

Well, it turns out that the difference is largely accidental. Here are the types of the functions involved:

	to :: Representable a => Rep a -> a
	genum' :: GEnum' a => [a]

	type instance Rep Nat = RepNat
   	type RepNat = U :+: (Rec Nat)

Consider the instance definition

     genum = map to genum'

There are two different ways of typing it:

(A)	map @RepNat @Nat (to @Nat dReprNat |> g1) (genum' @RepNat dGEnum'_RepNat)
        where 
	    g1 :: Rep Nat -> Nat ~ RepNat -> Nat
          dReprNat :: Representable Nat
          dGEnum'Nat :: GEnum' RepNat

or

(B)	map @(Rep Nat) @Nat (to @Nat dReprNat) (genum' @(Rep Nat) dGEnum'_Rep_Nat)
        where 
           dReprNat :: Representable Nat
           dGEnum'Nat :: GEnum' (Rep Nat)

Which of these is chosen depends on accidental things in the constraint solver; it's not supposed to matter.

But it DOES affect whether the map/(|||) rule fires.

{-# RULES "ft |||" forall f a b. map f (a ||| b) = map f a ||| map f b #-}

It makes a difference because in (A) we have an instance for GEnum' RepNat that uses ||| directly,

	instance (GEnum' f, GEnum' g) => GEnum' (f :+: g) where
 	   genum' = map L genum' ||| map R genum'

so we get

	map ... (blah1 ||| blah2)

But in (B) we need an instance for GEnum' (Rep Nat) and that has an extra cast, so we get

	map ... ((blah1 ||| blah2) |> g)

And the cast stops the RULE for map/(|||) firing.

Parametricity to the rescue

Note that (|||) :: [a] -> [a] -> [a]. So by parametricity we know that

	if g :: [T1] ~ [T2]
then
	((|||) @T1 xs ys |> g)
       =
 	((|||) @T2 (xs |> g) (ys |> g)

If we used that to push the cast inwards, the RULE would match.

Likewise, map is polymorphic: map :: (a->b) -> [a] -> [b] So by parametricity

	if :: [T1] -> [T2]
   then
 	map @T2 @TR f (xs |> g)]
      =
	map @T1 @TR (f |> sym (right g) -> TR) xs

If we used that to move the cast out of the way, the RULE would match too.

But GHC is nowhere near clever enough to do either of these things. And it's far from obvious what to do in general.

Bottom line

The choices made by the constraint solver can affect exactly where casts are inserted into the code. GHC knows how to move casts around to stop them getting in the way of its own transformations, but is helpless if they get in the way of RULES.

I am really not sure how to deal with this. But it is very interesting!

Simon

Trac metadata

Trac field	Value
Version	7.4.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture