[GHC] #5974: Casts, rules, and parametricity

[GHC]

#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) -> <z_axF>_R
                    :: ((y_axE -> z_axF) :: *) ~R# ((x_axG -> z_axF) ::
 *)))
           xs_axD
 }}}
 which looks somewhat nice.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/5974#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler