Skip to content

Rework the RULES story for `elem`.

Andreas Klebinger requested to merge wip/andreask/elem_rule_fix into master

The old elem rule was

"elem/build"    forall x (g :: forall b . Eq a => (a -> b -> b) -> b -> b)
    . elem x (build g) = g (\ y r -> (x == y) || r) False

This rule will ALMOST NEVER FIRE. The argument g of build g has type forall b. (a->b->b) -> b -> b. But the rule asks the rule-matcher to produce a g with that overloaded type. So it compiles to:

"elem/build"
    forall (@ a)
           ($dEq :: Eq a)
           ($dEq1 :: Eq a)
           (x :: a)
           (g :: forall b. Eq a => (a -> b -> b) -> b -> b).
      myelem @ a $dEq x (build @ a (\ (@ b) -> g @ b $dEq1))
      = g @ Bool
          $dEq
          (\ (y :: a) (r :: Bool) -> || (== @ a $dEq x y) r)
          False

Whereas the right rule, as pointed out by Oleg should be:

{-# RULES
"elem/build2"    forall x (g :: forall b . (a -> b -> b) -> b -> b)
   . elem x (build g) = g (\ y r -> (x == y) || r) False
 #-}

which compiles to:

"elem/build2"
    forall (@ a)
           ($dEq :: Eq a)
           (x :: a)
           (g :: forall b. (a -> b -> b) -> b -> b).
      myelem @ a $dEq x (build @ a g)
      = g @ Bool (\ (y :: a) (r :: Bool) -> || (== @ a $dEq x y) r) False

That is simpler, faster to match, and (crucially) applies much more often!

Thanks @phadej for spotting this.

However there is trouble! For strings this leads to suboptimal code:

  = \ (c_aA5 :: Char) ->
      unpackFoldrCString#
        @Bool
        "abcdefh"#
        (\ (y_a1ln :: Char) (r_a1lo :: Bool) -> case eqChar c_aA5 ... ) -- Too late, already allocated
        GHC.Types.False

We sidestep this by adding a built in rule which transforms patterns like x `elem` "abc" into case statements which fires before the elem fusion rule.

Edited by Andreas Klebinger

Merge request reports