Confusing note on semantics of rewrite rules in users guide
Summary
The last bullet point in the GHC user's guide section 6.19.1.2 about the semantics of rewrite rules
A rule that has a forall binder with a polymorphic type, is likely to fail to fire. E. g.,
{-# RULES forall (x :: forall a. Num a => a -> a). f x = blah #-}
Here x has a polymorphic type. This applies to a forall’d binder with a type class constraint, such as:
{-# RULES forall @m (x :: KnownNat m => Proxy m). g x = blah #-}
See #21093 (closed) for discussion.
This has a number of flaws:
- It uses the term "forall binder" where "pattern variable" is meant (confusingly we call these template variables in the source code)
- The second part, from "This applies" onwards, threw me off.
- The second rewrite rule uses @m syntax for one of the pattern variables, which is invalid syntax.
- The rules lack names
Proposed improvements or changes
-
A rule that has a pattern variable with a polymorphic type, is likely to fail to fire. E. g.,
{-# RULES "f" forall (x :: forall a. Num a => a -> a). f x = blah #-}
Here x has a polymorphic type. The same holds for rules that have a pattern variable with a type class constraint, such as:
{-# RULES "g" forall m. forall (x :: KnownNat m => Proxy m). g x = blah #-}
See #21093 (closed) for discussion.