#5974: Casts, rules, and parametricity
-------------------------------------+-------------------------------------
Reporter: simonpj | Owner:
Type: bug | Status: new
Priority: normal | Milestone: ⊥
Component: Compiler | Version: 7.4.1
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by nomeata):
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) ->