#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