#2110: Rules to eliminate casted id's -------------------------------------+------------------------------------ Reporter: igloo | Owner: Type: feature request | Status: new Priority: lowest | Milestone: 7.6.2 Component: Compiler | Version: 6.8.2 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): Please allow me to use this as a notepad; this way I (or someone else) can easily find the thoughts later. With `Coercible` in GHC, one might want that {{{ {-# RULES "myMap/coerce" myMap coerce = coerce #-} }}} will be a usable rule that would also fire in {{{ foo :: [Int] -> [Age] foo = myMap Age }}} At the moment, it does not do that yet. Here is the rule (as shown by `-ddump-rules`, with `-O`): {{{ ==================== Tidy Core rules ==================== "myMap/coerce" [ALWAYS] forall (@ t) (@ t1) ($dCoercible :: GHC.Types.Coercible t t1). Test.myMap @ t @ t1 (GHC.Prim.coerce @ t @ t1 $dCoercible) = GHC.Prim.coerce @ [t] @ [t1] (case $dCoercible of _ { GHC.Types.MkCoercible ds -> GHC.Types.MkCoercible @ [t] @ [t1] @~ [ds]_R }) }}} and here is the Core code the rule needs to match (`-ddump-simpl`, with `-O`): {{{ Test.foo1 :: GHC.Types.Int -> GHC.Types.Int [GblId, Arity=1, Caf=NoCafRefs, Str=DmdType <S,1*U(U)>m, Unf=Unf{Src=InlineStable, TopLvl=True, Arity=1, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=ALWAYS_IF(unsat_ok=True,boring_ok=True) Tmpl= \ (tpl_B1 [Occ=Once] :: GHC.Types.Int) -> tpl_B1}] Test.foo1 = \ (tpl_B1 :: GHC.Types.Int) -> tpl_B1 Test.foo :: [GHC.Types.Int] -> [Test.Age] [GblId, Arity=1, Str=DmdType, Unf=Unf{Src=<vanilla>, TopLvl=True, Arity=0, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 20 60}] Test.foo = Test.foo_myMap @ GHC.Types.Int @ Test.Age (Test.foo1 `cast` (<GHC.Types.Int>_R -> Sym Test.NTCo:Age[0] :: (GHC.Types.Int -> GHC.Types.Int) ~# (GHC.Types.Int -> Test.Age))) }}} Note that in the rule’s LHS, `coerce` was not unfolded, while it is in the core. Also note that the rule talks about a `Coercion` value that we do not have. Here is one plan that might work. If a rule has a binder `$d` of type `Coercible a b`, then the rule is changed to have a binder `c` of type `a ~R# b`, and every occurrence of `$d` is replaced by `MkCoercible a b c`. So the rule above, (after simplification of the RHS) would read {{{ "myMap/coerce" [ALWAYS] forall (@ t) (@ t1) (c :: t ~R# t1). Test.myMap @ t @ t1 (GHC.Prim.coerce @ t @ t1 (GHC.Types.MkCoercible @ t @ t1 @~ c) = GHC.Prim.coerce @ [t] @ [t1] (GHC.Types.MkCoercible @ [t] @ [t1] @~ [c]_R) }}} The next step is to simplify occurrences of `coerce @ a @ b (MkCoercible @ a @ b @~ c)` and replace them by (id `cast` c): {{{ "myMap/coerce" [ALWAYS] forall (@ t) (@ t1) (c :: t ~R# t1). Test.myMap @ t @ t1 (id `cast` c) = GHC.Prim.coerce @ [t] @ [t1] (GHC.Types.MkCoercible @ [t] @ [t1] @~ [c]_R) }}} which (possibly after inlining id) with some reasonable hope matches the actual code. I especially like how the specializing of `Coercible` values to `~R#` values allows to use the matched coercion (which could even come from a `unsafeCoerce`!) in the RHS of the rule, instead of completely throwing it away and firing only if the coercion on the RHS can be found by the type checker. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/2110#comment:36> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler