content: {-# RULES
  "fold/build" forall k z (g :: forall b. (a -> b -> b) -> b -> b).
    foldr k z (build g) =
      g k z
  "foldr/augment" forall k z xs (g :: forall b. (a -> b -> b) -> b -> b).
    foldr k z (augment g xs) =
      g k (foldr k z xs)
  "foldr/id" foldr (:) [] = \x -> x
  "foldr/app" [1] forall ys. foldr (:) ys = \xs -> xs ++ ys
  -- Only activate this from phase 1, because that's
  -- when we disable the rule that expands (++) into foldr
  
  -- The foldr/cons rule looks nice, but it can give disastrously
  -- bloated code when commpiling
  --      array (a,b) [(1,2), (2,2), (3,2), ...very long list... ]
  -- i.e. when there are very very long literal lists
  -- So I've disabled it for now. We could have special cases
  -- for short lists, I suppose.
  -- "foldr/cons" forall k z x xs. foldr k z (x:xs) = k x (foldr k z xs)
  
  "foldr/single" forall k z x. foldr k z [x] = k x z
  "foldr/nil" forall k z. foldr k z [] = z
  "augment/build" forall
    (g :: forall b. (a -> b -> b) -> b -> b)
    (h :: forall b. (a -> b -> b) -> b -> b).
    augment g (build h) =
      build (\c n -> g c (h c n))
  "augment/nil" forall (g :: forall b. (a -> b -> b) -> b -> b).
    augment g [] =
      build g
    #-}
  