RewriteRules.hs

{-# LANGUAGE BangPatterns #-}
module Main where

main :: IO ()
main = putStrLn (show $ foo [1..10000000000])

-- without the bang assoc is not recursed
-- but it is recursed with the ! even with the rewrite Rule
withProof :: a -> () -> a 
withProof x !_ = x 

foo :: [Int] -> Int
foo xs = head xs `withProof` assoc xs [] [] 

assoc :: [a] -> [a] -> [a] -> () 
assoc [] _ _ = () 
assoc (x:xs) ys zs = assoc xs ys zs 

{-# RULES "assoc/runtime"  forall xs ys zs. assoc xs ys zs = () #-}
{-# NOINLINE  assoc #-}