Opened 8 years ago

Last modified 3 years ago

## #5974 new bug

# Casts, rules, and parametricity

Reported by: | simonpj | Owned by: | |
---|---|---|---|

Priority: | normal | Milestone: | ⊥ |

Component: | Compiler | Version: | 7.4.1 |

Keywords: | Cc: | ||

Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |

Type of failure: | None/Unknown | Test Case: | |

Blocked By: | Blocking: | ||

Related Tickets: | Differential Rev(s): | ||

Wiki Page: |

### Description

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

### Change History (4)

### comment:1 Changed 8 years ago by

### comment:2 Changed 7 years ago by

Milestone: | → _|_ |
---|

### comment:3 Changed 6 years ago by

When matching a lambda `(\x -> g x)`

against an expression `(\y -> f y) |> γ`

, since [a27b2985] it will push the coercion γ inside the lambda, see `pushCoercionIntoLambda`

in source:compiler/coreSyn/CoreSubst.lhs. Similar pushing around could help in other cases where RULES fail to match due to coercions.

Also, the ability to mention `coerce`

in a RULE (and have it match all kind of coercions) could help with the issues of this tickets.

A rule `{-# RULES "foo" forall (f:: y -> z) (xs :: [x]) . map f (coerce xs) = map (coerce f) xs #-}`

would possibly help here, but needs more power in the type checker, namely the deconstruction of `Coercible`

constraints:

T5974.hs:4:76: Could not coerce from ‛y’ to ‛x’ because ‛y’ and ‛x’ are different types. arising from a use of ‛coerce’ from the context (Coercible [x] [y]) bound by the RULE "foo" at T5974.hs:4:11-87 In the first argument of ‛map’, namely ‛(coerce f)’ In the expression: map (coerce f) xs When checking the transformation rule "foo"

### comment:4 Changed 3 years ago by

Just a small remark: The rule

{-# RULES "foo" forall (f:: y -> z) (xs :: [x]) . map f (coerce xs) = map (coerce f) xs #-}

mentioned above is accepted by GHC-8, and takes this form in Core:

"foo" [ALWAYS] forall (@ y_axE) (@ z_axF) (@ x_axG) ($r$dCoercible_dJK :: ([x_axG] :: *) ~R# ([y_axE] :: *)) (f_axC :: y_axE -> z_axF) (xs_axD :: [x_axG]). map @ y_axE @ z_axF f_axC (xs_axD `cast` ($r$dCoercible_dJK :: ([x_axG] :: *) ~R# ([y_axE] :: *))) = map @ x_axG @ z_axF (f_axC `cast` (Nth:0 (Sym $r$dCoercible_dJK) -> <z_axF>_R :: ((y_axE -> z_axF) :: *) ~R# ((x_axG -> z_axF) :: *))) xs_axD

which looks somewhat nice.

**Note:**See TracTickets for help on using tickets.

See also #2110