[GHC] #13733: Simplify constraints on RULES LHS

[GHC]

#13733: Simplify constraints on RULES LHS
-------------------------------------+-------------------------------------
           Reporter:  nomeata        |             Owner:  (none)
               Type:  feature        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.3
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 TL;DR: Rewrite rules should be able to match instance methods.

 I know that the interaction of rewrite rules and classes/instances/methods
 is unsatisfying, and probably will be for the forseeable future given the
 current design. But we might still improve little bits.

 Consider this code:

 {{{
 {-# RULES
     "[Integer] Eq Refl" forall (xs :: [Integer]). xs == xs = True
 #-}
 }}}

 This is the best I can to express the intention of “dear compile, this is
 a rule for the equality on lists if the elements are integers”. But what I
 get is

 {{{
 "[Integer] Eq Refl" [ALWAYS]
     forall ($dEq_a1Jv :: Eq [Integer]) (xs_a1Hd :: [Integer]).
       == @ [Integer] $dEq_a1Jv xs_a1Hd xs_a1Hd
       = GHC.Types.True
 }}}

 which is a rule about the method `==` applied to ''any'' evidence of
 equality about lists. This works in the most obvious cases, such as

 {{{
 alwaysTrue :: [Integer]-> Bool
 alwaysTrue xs = xs == xs
 }}}

 but it does not fire with

 {{{
 delayedId :: a -> a
 delayedId x = x
 {-# INLINE [0] delayedId #-}

 alwaysTrue :: [Integer]-> Bool
 alwaysTrue xs = xs == delayedId xs
 {-# NOINLINE alwaysTrue #-}
 }}}

 The reason is that directly after the simplifier, in the former case, the
 Core looks like this

 {{{
 $dEq_a1HH :: Eq [Integer]
 [LclId, Str=DmdType]
 $dEq_a1HH = GHC.Classes.$fEq[] @ Integer integer-
 gmp-1.0.0.1:GHC.Integer.Type.$fEqInteger

 alwaysTrue [InlPrag=NOINLINE] :: [Integer] -> Bool
 [LclIdX, Str=DmdType]
 alwaysTrue = \ (xs_aGT :: [Integer]) -> == @ [Integer] $dEq_a1HH xs_aGT
 xs_aGT
 }}}

 which matches the rule, but in the latter case, by the time the
 `delayedId` is out of the way, we have

 {{{
 alwaysTrue [InlPrag=NOINLINE] :: [Integer] -> Bool
 [LclIdX, Arity=1, Str=DmdType <S,U>]
 alwaysTrue =
   \ (xs_aGT :: [Integer]) ->
     GHC.Classes.$fEq[]_$c==
       @ Integer
       integer-gmp-1.0.0.1:GHC.Integer.Type.$fEqInteger
       xs_aGT
       xs_aGT
 }}}

 One possible way forward would be to simplify the wanted constraints on
 the LHS of the rule using the instances in scope:
 {{{
 "[Integer] Eq Refl" [ALWAYS]
     forall (xs_a1Hd :: [Integer]).
     GHC.Classes.$fEq[]_$c==
       @ Integer
       integer-gmp-1.0.0.1:GHC.Integer.Type.$fEqInteger
       xs_a1Hd
       xs_a1Hd
     = True
 }}}

 This might be tricky, of course, as this requires not only help from the
 type checker, but also some careful tuned simplification of the LHS
 afterwards (e.g. unfold dictionary accessors)).

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