Skip to content

Allow `case` in LHS of RULE

Consider

{-# LANGUAGE MagicHash #-}

import GHC.Exts
import Data.Int

{-# RULES
  "blah" forall x . case f x of (I# a, _) -> e = case sf x of a -> e
#-}

f :: Int -> (Int, Int)
f x = (sum [0..x], sum [1..2*x])
{-# NOINLINE f #-}

sf :: Int -> Int#
sf x = case sum [0..x] of I# a -> a
{-# NOINLINE sf #-}

g :: Int
g = case f 42 of (a, _) -> a + 1

A sort of manual version of the idea #16335. GHC rejects, because the LHS of the RULE is not just an App with a top-level variable in its head:

test.hs:9:3: error:
    Rule "blah":
      Illegal expression: case f x of { (I# a, _) -> e }
      in left-hand side: case f x of { (I# a, _) -> e }
    LHS must be of form (f e1 .. en) where f is not forall'd
  |
9 |   "blah" forall x . case f x of (I# a, _) -> e = case sf x of a -> e
  |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

I want to loosen that restriction. IMO, it makes perfect sense to allow these kind of generalised call contexts:

  1. \e -> case e of alts has similar operational meaning as e x. (Church encoding even converts the former context into the latter.)
  2. Both contexts have counterparts as (sub-)demands: \e -> case e of alts puts e under a product demand P(...), whereas \e -> e x puts e under call demand C(...).

Thus, I propose that we say instead

    LHS must be of form `case f e1 .. en of ... -> e` where f is not forall'd

Note that the pattern ... may nest arbitrarily deep, but may only consist of constructor patterns, variable patterns or wildcards.

A wildcard, in my example above, means "This binder is dead". In terms of demands, it means that the RULE may only match in scenarios where the field binder has absent demand.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information