[GHC] #2110: Rules to eliminate casted id's

[GHC]

#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