[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      |       Difficulty:  Unknown
       Test Case:                    |       Blocked By:
        Blocking:                    |  Related Tickets:
-------------------------------------+------------------------------------

Comment (by nomeata):

 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"
 }}}

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