[GHC] #13733: Simplify constraints on RULES LHS
#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
#13733: Simplify constraints on RULES LHS -------------------------------------+------------------------------------- Reporter: nomeata | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13733#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13733: Simplify constraints on RULES LHS -------------------------------------+------------------------------------- Reporter: nomeata | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by nomeata): 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13733#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13733: Simplify constraints on RULES LHS -------------------------------------+------------------------------------- Reporter: nomeata | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13733#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13733: Simplify constraints on RULES LHS -------------------------------------+------------------------------------- Reporter: nomeata | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by nomeata): 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13733#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC