Simplify constraints on RULES LHS

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)).

Trac metadata

Trac field	Value
Version	8.3
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tfeature request Trac import labels

The problem is that the built-in rule that rewrites

GHC.Classes.$fEq[] @ Integer GHC.Integer.Type.$fEqInteger
---->
GHC.Classes.$fEq[]_$c== @ Integer GHC.Integer.Type.$fEqInteger

is firing before your user-defined rule has a chance to fire. The basic problem is that two overlapping rules are competing, and it's a fluke which "wins". Monkeying around with solving constraints on rule LHSs might be a sticking plaster, but it won't tackle the underlying issue.

Possible solution: make the built-in rule fire in phase 2,1,0, but not in the initial "gentle" phase.

Of course, not firing the built-in class-op rule means that other things won't happen as early as they otherwise might, so I don't know what the knock-on effects might be. But I think this is the path to follow if you want to pursue this.

Something similar happens for the inlining for data constructor wrappers.

I'm sure there is a ticket about this stuff already. Maybe more than one.

Another view is that the problem is that the user cannot even specify the desired rule, namely one that matches

GHC.Classes.$fEq[]_$c== @ Integer GHC.Integer.Type.$fEqInteger

and maybe the problem should be attacked from this angle.

There is precedent in the way coerce works on the LHS of a rule: If it appears on the LHS, the compiler assumes the user wants to match any Core-level cast (x |> c), and thus inlines coerce, and even changes the free variable of the rule so that it can match unlifted coercions (see Note [Getting the map/coerce RULE to work]).

In that sense, solving constraints on the LHS is not really monkeying or a plaster, but it is what what we have to do to allow the user to write rules that match a specific instance method.

user cannot even specify the desired rule,

Certainly you can!

isntance Eq T where
  (==) = eqT

eqT :: T -> T -> T
{-# NOINLINE [1] eqT #-}
{-# RULES eqT x x = True #-}

All fine!

I have no clear understanding of what you are proposing. Perhaps you can lay it out? What's wrong with the approach I suggest? It seems simple and direct. Really the only thing that's tricky here is that the "class-op rules" are built-in so you can't control their competition with rules you want to write.

Oh, yes, the library author can! But someone downstream does not have the ability to change the

instance Eq [a] where
  x == y = rhs

to the above format.

Similarly if they want to write

data T = … deriving Show

In both cases I would consider consider your approach an work-around that, well, works around the fact that an instance method does not have a Haskell-adressable name.

So what am I proposing?… now, before I propose something, let me phrase clearly what I want to achieve: **I want to write rules that apply to an instance method.**

(Your approach does not quite achieve that. What it does achieve is that I no longer want to address instance methods, as I can now adress eqT, which works fine in many cases. But this does not work if the instance declaration is out of my control.)

There may be several ways of achieving this goal. One way would be: **Simplify constraints of rules with the current instances and apply class-op rules on the LHS of rules.**

This way, the user’s rule

forall (xs :: [Integer]). xs == xs = True

gets desugared to

    forall (xs_a1Hd :: [Integer]).
      == @ [Integer] ($fEq[] @ Integer $fEqInteger) xs_a1Hd xs_a1Hd
      = GHC.Types.True

(compare that with the rule above, which has a pattern variable $dEq_a1Jv for the Eq [Integer] dictionary), and then gentle simplification (including class-op) on the left turns this into

  forall (xs_a1Hd :: [Integer]).
    GHC.Classes.$fEq[]_$c== @Integer $fEqInteger xs_a1Hd xs_a1Hd
      = GHC.Types.True

which – how convenient – is precisely the code we want to match, in the form the simplifier puts it.

This machinery should allow the rule author to address any concrete instance method, in his module or an imported module, by using the class method with a sufficiently precise type.

added broken test label

added Pnormal label