#5974: Casts, rules, and parametricity
-+--
Reporter: simonpj | Owner:
Type: bug | Status: new
Priority: normal| Milestone:
Component: Compiler | Version: 7.4.1
Keywords:| Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: None/Unknown
Difficulty: Unknown |Testcase:
Blockedby:|Blocking:
Related:|
-+--
Pedro wrote this
[http://www.haskell.org/pipermail/generics/2012-February/000513.html long
message] about the way that his generic-programming was not optimising as
it should:
My reply was in two parts. The
[http://www.haskell.org/pipermail/generics/2012-March/000516.html first]
was fairly simple. The
[http://www.haskell.org/pipermail/generics/2012-March/000517.html 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
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/5974
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler
___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
