[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):

 I looked into this and further cleaned up the branch. But I just cannot
 get it to optimize `map unsafeCoerce` away, and the problem seems to be
 not enough eta-expansion in the simplifier.

 So here is the rule as desugared; it has the shape that we want it to have
 {{{
 ------ Local rules for imported ids --------
 "map/coerce" [ALWAYS]
     forall (@ a) (@ b) ($r$dCoercible :: a GHC.Prim.~R# b).
       GHC.Base.map @ a
                    @ b
                    ((\ (tpl :: a) -> tpl)
                     `cast` (<a>_R -> ($r$dCoercible) :: (a -> a) ~# (a ->
 b)))
       = (\ (tpl :: [a]) -> tpl)
         `cast` (<[a]>_R -> [($r$dCoercible)]_R
                 :: ([a] -> [a]) ~# ([a] -> [b]))
 }}}

 And here is the Core that we want it to match:
 {{{
   GHC.Base.map
     @ GHC.Types.Int
     @ Test.Age
     ((Unsafe.Coerce.unsafeCoerce1 @ GHC.Types.Int @ Test.Age)
      `cast` (<GHC.Types.Int>_R
              -> UnivCo representational GHC.Types.Int Test.Age
              :: (GHC.Types.Int -> GHC.Types.Int)
                   ~#
                 (GHC.Types.Int -> Test.Age)))
 }}}

 And for reference, here is the information on `unsafeCoerce1`:
 {{{
   unsafeCoerce1 :: forall a b. a -> a
     {- Arity: 1, HasNoCafRefs, Strictness: <S,1*U>,
        Unfolding: (\ @ a @ b x :: a -> x) -}
 }}}

 When trying to match, the matcher successfully matches the casts and then
 tries to match
 {{{
     \ (tpl{v} [lid] :: a{tv aMF} [tv]) -> tpl{v} [lid]
 }}}
 against
 {{{
     base:Unsafe.Coerce.unsafeCoerce1{v rKi} [gid]
       @ ghc-prim:GHC.Types.Int{(w) tc 3J} @ main:Test.Age{tc rM6}
 }}}

 It eta-expands both sides to match
 {{{
     tpl{v} [lid]
 }}}
 against
 {{{
     base:Unsafe.Coerce.unsafeCoerce1{v rKi} [gid]
       @ ghc-prim:GHC.Types.Int{(w) tc 3J}
       @ main:Test.Age{tc rM6}
       tpl{v} [lid]
 }}}
 and there it fails.

 Possible solutions: If GHC would inline `unsafeCoerce1` even though it is
 undersaturated, we’d be matching
 {{{
   GHC.Base.map
     @ GHC.Types.Int
     @ Test.Age
     ((\ x :: GHC.Types.Int -> x)
      `cast` (<GHC.Types.Int>_R
              -> UnivCo representational GHC.Types.Int Test.Age
              :: (GHC.Types.Int -> GHC.Types.Int)
                   ~#
                 (GHC.Types.Int -> Test.Age)))
 }}}
 which would succeed (this is also the shape we get from `map Age`). But I
 did not manage to define `unsafeCoerce` in a way that this happens.

 Alternatively, the matching code could, after eta-expanding, simplify the
 expression, so that the unfolding would happen here.

 Otherwise, my code is ready for review, see branch `wip/nomeata-T2110`.

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