diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,14 @@
+0.2
+---
+
+- the use of lazy data structures will now cause a warning (can be
+  disabled by 'AllowLazyData' annotation); this check for lazy data is
+  rather ad hoc and needs to be refined
+- allow functions under ticks (but with limitations, see paper)
+- strictness transformation is now similar to the 'Strict' language
+  extension
+- optimisations using custom rewrite rules
+
 0.1.1.0
 -------
 
diff --git a/Rattus.cabal b/Rattus.cabal
--- a/Rattus.cabal
+++ b/Rattus.cabal
@@ -1,6 +1,6 @@
 cabal-version:       1.18
 name:                Rattus
-version:             0.1.1.0
+version:             0.2
 category:            FRP
 synopsis:            A modal FRP language
 description:
@@ -115,6 +115,7 @@
             provides more examples on how to program in Rattus.
 
 homepage:            https://github.com/pa-ba/Rattus
+bug-reports:         https://github.com/pa-ba/Rattus/issues
 License:             BSD3
 License-file:        LICENSE
 copyright:           Copyright (C) 2020 Patrick Bahr
@@ -164,6 +165,7 @@
   build-depends:       Rattus, base
   ghc-options:         -fplugin=Rattus.Plugin -rtsopts -g2
 
+
 Test-Suite time-leak
   type:                exitcode-stdio-1.0
   main-is:             TimeLeak.hs
@@ -183,6 +185,15 @@
 Test-Suite well-typed
   type:                exitcode-stdio-1.0
   main-is:             WellTyped.hs
+  hs-source-dirs:      test
+  default-language:    Haskell2010
+  build-depends:       Rattus, base, containers
+  ghc-options:         -fplugin=Rattus.Plugin -rtsopts -g2
+
+
+Test-Suite rewrite
+  type:                exitcode-stdio-1.0
+  main-is:             Rewrite.hs
   hs-source-dirs:      test
   default-language:    Haskell2010
   build-depends:       Rattus, base, containers
diff --git a/docs/paper.pdf b/docs/paper.pdf
Binary files a/docs/paper.pdf and b/docs/paper.pdf differ
diff --git a/src/Rattus.hs b/src/Rattus.hs
--- a/src/Rattus.hs
+++ b/src/Rattus.hs
@@ -2,13 +2,17 @@
 
 
 -- | The bare-bones Rattus language. To program with streams and
--- events import "Rattus.Stream" and "Rattus.Events"; to program with
--- Yampa-style signal functions import "Rattus.Yampa".
+-- events, you can use "Rattus.Stream" and "Rattus.Events"; to program with
+-- Yampa-style signal functions, you can use "Rattus.Yampa".
 
 module Rattus (
+  -- * Rattus language primitives
   module Rattus.Primitives,
+  -- * Strict data types
   module Rattus.Strict,
+  -- * Annotation
   Rattus(..),
+  -- * Applicative operators
   (|*|),
   (|**),
   (<*>),
@@ -27,17 +31,21 @@
 
 
 -- | Applicative operator for 'O'.
+{-# INLINE (<*>) #-}
 (<*>) :: O (a -> b) -> O a -> O b
 f <*> x = delay (adv f (adv x))
 
--- | Variant of '(<*>)' where the argument is of a stable type..
+-- | Variant of '<*>' where the argument is of a stable type..
+{-# INLINE (<**) #-}
 (<**) :: Stable a => O (a -> b) -> a -> O b
 f <** x = delay (adv f x)
 
 -- | Applicative operator for 'Box'.
+{-# INLINE (|*|) #-}
 (|*|) :: Box (a -> b) -> Box a -> Box b
 f |*| x = box (unbox f (unbox x))
 
--- | Variant of '(|*|)' where the argument is of a stable type..
+-- | Variant of '|*|' where the argument is of a stable type..
+{-# INLINE (|**) #-}
 (|**) :: Stable a => Box (a -> b) -> a -> Box b
 f |** x = box (unbox f x)
diff --git a/src/Rattus/Event.hs b/src/Rattus/Event.hs
--- a/src/Rattus/Event.hs
+++ b/src/Rattus/Event.hs
@@ -31,6 +31,7 @@
 {-# ANN module Rattus #-}
 
 -- | Apply a function to the value of the event (if it ever occurs).
+{-# NOINLINE [1] map #-}
 map :: Box (a -> b) -> Event a -> Event b
 map f (Now x) = Now (unbox f x)
 map f (Wait x) = Wait (delay (map f) <*> x)
@@ -105,3 +106,10 @@
   case unbox f x of
     Just' y  -> Now y
     Nothing' -> Wait (delay (triggerMap f) <*> xs)
+
+{-# RULES
+
+  "map/map" forall f g xs.
+    map f (map g xs) = map (box (unbox f . unbox g)) xs ;
+
+#-}
diff --git a/src/Rattus/Events.hs b/src/Rattus/Events.hs
--- a/src/Rattus/Events.hs
+++ b/src/Rattus/Events.hs
@@ -29,6 +29,7 @@
 {-# ANN module Rattus #-}
 
 -- | Apply a function to the values of the event (every time it occurs).
+{-# NOINLINE [1] map #-}
 map :: Box (a -> b) -> Events a -> Events b
 map f (Just' x ::: xs) =  (Just' (unbox f x)) ::: delay (map f (adv xs))
 map f (Nothing' ::: xs) = Nothing' ::: delay (map f (adv xs))
@@ -69,3 +70,12 @@
 -- value.
 triggerMap :: Box (a -> Maybe' b) -> Str a -> Events b
 triggerMap = S.map
+
+
+
+{-# RULES
+
+  "map/map" forall f g xs.
+    map f (map g xs) = map (box (unbox f . unbox g)) xs ;
+
+#-}
diff --git a/src/Rattus/Plugin.hs b/src/Rattus/Plugin.hs
--- a/src/Rattus/Plugin.hs
+++ b/src/Rattus/Plugin.hs
@@ -35,8 +35,17 @@
 -- definitions) as follows:
 --
 -- > {-# ANN myFunction NotRattus #-}
+--
+-- By default all Rattus functions are checked for use of lazy data
+-- types, since these may cause memory leaks. If any lazy data types
+-- are used, a warning is issued. These warnings can be disabled by
+-- annotating the module or the function with 'AllowLazyData'
+--
+-- > {-# ANN myFunction AllowLazyData #-}
+-- >
+-- > {-# ANN module AllowLazyData #-}
 
-data Rattus = Rattus | NotRattus deriving (Typeable, Data, Show, Eq)
+data Rattus = Rattus | NotRattus | AllowLazyData deriving (Typeable, Data, Show, Eq)
 
 -- | Use this to enable Rattus' plugin, either by supplying the option
 -- @-fplugin=Rattus.Plugin@ directly to GHC. or by including the
@@ -46,51 +55,63 @@
 plugin :: Plugin
 plugin = defaultPlugin {
   installCoreToDos = install,
-  tcPlugin = tcStable
+  tcPlugin = tcStable,
+  pluginRecompile = purePlugin
   }
 
 
-install :: [CommandLineOption] -> [CoreToDo] -> CoreM [CoreToDo]
-install _ todo = do
-  return (CoreDoPluginPass "Rattus" transformProgram : todo)
 
+install :: [CommandLineOption] -> [CoreToDo] -> CoreM [CoreToDo]
+install _ todo = return (scPass : strPass : todo)
+    where scPass = CoreDoPluginPass "Rattus scopecheck" scopecheckProgram
 
-transformProgram :: ModGuts -> CoreM ModGuts
-transformProgram guts = do
-  newBindsM <- mapM (transform guts) (mg_binds guts)
-  case sequence newBindsM of
-    Nothing -> liftIO exitFailure
-    Just newBinds -> return $ guts { mg_binds = newBinds }
+          strPass = CoreDoPluginPass "Rattus strictify" strictifyProgram
 
+strictifyProgram :: ModGuts -> CoreM ModGuts
+strictifyProgram guts = do
+  newBinds <- mapM (strictify guts) (mg_binds guts)
+  return guts { mg_binds = newBinds }
 
-transform :: ModGuts -> CoreBind -> CoreM (Maybe CoreBind)
-transform guts b@(Rec bs) = do
+strictify :: ModGuts -> CoreBind -> CoreM (CoreBind)
+strictify guts b@(Rec bs) = do
   tr <- liftM or (mapM (shouldTransform guts . fst) bs)
-  if tr then
-    case bs of
-      [] -> return (Just $ Rec [])
-      binds -> do
-          let vs = map fst binds
-          let es = map snd binds
-          let vs' = Set.fromList vs
-          valid <- mapM (\ (v,e) -> checkExpr (emptyCtx (Just (vs', v))) e) binds
-          if and valid then do
-            es' <- mapM strictifyExpr es
-            return (Just $ Rec (zip vs es'))
-          else return Nothing
+  if tr then do
+    let vs = map fst bs
+    es' <- mapM (\ (v,e) -> do
+                    lazy <- allowLazyData guts v
+                    strictifyExpr (SCxt (nameSrcSpan $ getName v) (not lazy))e) bs
+    return (Rec (zip vs es'))
+  else return b
+strictify guts b@(NonRec v e) = do
+    tr <- shouldTransform guts v
+    if tr then do
+      lazy <- allowLazyData guts v
+      e' <- strictifyExpr (SCxt (nameSrcSpan $ getName v) (not lazy)) e
+      return (NonRec v e')
+    else return b
 
-  else return (Just b)
-transform guts b@(NonRec v e) = do
+
+scopecheckProgram :: ModGuts -> CoreM ModGuts
+scopecheckProgram guts = do
+  res <- mapM (scopecheck guts) (mg_binds guts)
+  if and res then return guts else liftIO exitFailure
+
+
+scopecheck :: ModGuts -> CoreBind -> CoreM Bool
+scopecheck guts (Rec bs) = do
+  tr <- liftM or (mapM (shouldTransform guts . fst) bs)
+  if tr then do
+    let vs = map fst bs
+    let vs' = Set.fromList vs
+    valid <- mapM (\ (v,e) -> checkExpr (emptyCtx (Just vs') v) e) bs
+    return (and valid)
+  else return True
+scopecheck guts (NonRec v e) = do
     tr <- shouldTransform guts v
     if tr then do
-      --putMsg (text "check Rattus definition: " <> ppr v)
-      --putMsg (ppr e)
-      valid <- checkExpr (emptyCtx Nothing) e
-      if valid then do
-        e' <- strictifyExpr e
-        return (Just $ NonRec v e')
-      else return Nothing
-    else return (Just b)
+      valid <- checkExpr (emptyCtx Nothing v) e
+      return valid
+    else return True
 
 getModuleAnnotations :: Data a => ModGuts -> [a]
 getModuleAnnotations guts = anns'
@@ -100,6 +121,12 @@
         anns' = mapMaybe (fromSerialized deserializeWithData . ann_value) anns
   
 
+
+
+allowLazyData :: ModGuts -> CoreBndr -> CoreM Bool
+allowLazyData guts bndr = do
+  l <- annotationsOn guts bndr :: CoreM [Rattus]
+  return (AllowLazyData `elem` l)
 
 
 shouldTransform :: ModGuts -> CoreBndr -> CoreM Bool
diff --git a/src/Rattus/Plugin/ScopeCheck.hs b/src/Rattus/Plugin/ScopeCheck.hs
--- a/src/Rattus/Plugin/ScopeCheck.hs
+++ b/src/Rattus/Plugin/ScopeCheck.hs
@@ -14,30 +14,19 @@
 import Data.Maybe
 
 type LCtx = Set Var
-data HiddenReason = BoxApp | AdvApp | NestedRec Var
+data HiddenReason = BoxApp | AdvApp | NestedRec Var | FunDef
 type Hidden = Map Var HiddenReason
 
-data Prim = Prim1 Prim1 | Prim2 Prim2
-data Prim1 = Delay | Adv | Box | Unbox | Arr
-data Prim2 = DApp | BApp | DAppP | BAppP
+data Prim = Delay | Adv | Box | Unbox | Arr
 
-instance Outputable Prim1 where
+instance Outputable Prim where
   ppr Delay = "delay"
   ppr Adv = "adv"
   ppr Box = "box"
   ppr Unbox = "unbox"
   ppr Arr = "arr"
   
-instance Outputable Prim2 where
-  ppr DApp = "<*>"
-  ppr BApp = "|*|"
-  ppr DAppP = "<**"
-  ppr BAppP = "|**"
 
-instance Outputable Prim where
-  ppr (Prim1 p) = ppr p
-  ppr (Prim2 p) = ppr p
-
 type RecDef = Set Var
 
 data Ctx = Ctx
@@ -46,24 +35,20 @@
     hiddenRec :: Hidden,
     earlier :: Maybe LCtx,
     srcLoc :: SrcSpan,
-    recDef :: Maybe (RecDef,Var),
+    recDef :: Maybe RecDef,
     stableTypes :: Set Var,
     primAlias :: Map Var Prim,
+    funDef :: Var,
     stabilized :: Bool}
 
 primMap :: Map FastString Prim
 primMap = Map.fromList
-  [("Delay", Prim1 Delay),
-   ("delay", Prim1 Delay),
-   ("adv", Prim1 Adv),
-   ("box", Prim1 Box),
-   ("arr", Prim1 Arr),
-   ("unbox", Prim1 Unbox),
-   ("<*>", Prim2 DApp),
-   ("<**", Prim2 DAppP),
-   ("|*|", Prim2 BApp),
-   ("|**", Prim2 BAppP)
-   ]
+  [("Delay", Delay),
+   ("delay", Delay),
+   ("adv", Adv),
+   ("box", Box),
+   ("arr", Arr),
+   ("unbox", Unbox)]
 
 
 isPrim :: Ctx -> Var -> Maybe Prim
@@ -74,6 +59,16 @@
   if isRattModule mod then Map.lookup name primMap
   else Nothing
 
+stabilizeLater :: Ctx -> Ctx
+stabilizeLater c =
+  if isJust (earlier c)
+  then c {earlier = Nothing,
+          hidden = hid,
+          hiddenRec = maybe (hiddenRec c) (Map.union (hidden c) . Map.fromSet (const FunDef)) (recDef c),
+          recDef = Nothing}
+  else c {earlier = Nothing,
+          hidden = hid}
+  where hid = maybe (hidden c) (Map.union (hidden c) . Map.fromSet (const FunDef)) (earlier c)
 
 
 stabilize :: HiddenReason -> Ctx -> Ctx
@@ -81,7 +76,7 @@
   {current = Set.empty,
    earlier = Nothing,
    hidden = hidden c `Map.union` Map.fromSet (const hr) ctxHid,
-   hiddenRec = hiddenRec c `Map.union` maybe Map.empty (Map.fromSet (const hr) . fst) (recDef c),
+   hiddenRec = hiddenRec c `Map.union` maybe Map.empty (Map.fromSet (const hr)) (recDef c),
    recDef = Nothing,
    stabilized = True}
   where ctxHid = maybe (current c) (Set.union (current c)) (earlier c)
@@ -90,7 +85,7 @@
 data Scope = Hidden SDoc | Visible | ImplUnboxed
 
 getScope  :: Ctx -> Var -> Scope
-getScope Ctx{recDef = Just (vs, recV), earlier = e} v
+getScope Ctx{recDef = Just (vs), funDef = recV, earlier = e} v
   | v `Set.member` vs =
     case e of
       Just _ -> Visible
@@ -105,7 +100,8 @@
   case Map.lookup v (hiddenRec c) of
     Just (NestedRec rv) -> Hidden ("Recursive call to" <> ppr v <>
                             " is not allowed as it occurs in a local recursive definiton (namely of " <> ppr rv <> ")")
-    Just BoxApp -> Hidden ("Recursive call to " <> ppr v <> " is not allowed since it occurs under a box")
+    Just BoxApp -> Hidden ("Recursive call to " <> ppr v <> " is not allowed here, since it occurs under a box")
+    Just FunDef -> Hidden ("Recursive call to " <> ppr v <> " is not allowed here, since it occurs in a function that is defined under delay")
     Just AdvApp -> Hidden ("This should not happen: recursive call to " <> ppr v <> " is out of scope due to adv")
     Nothing -> 
       case Map.lookup v (hidden c) of
@@ -119,6 +115,8 @@
           else Hidden ("Variable " <> ppr v <> " is no longer in scope:" $$
                        "It occurs under " <> keyword "box" $$ "and is of type " <> ppr (varType v) <> ", which is not stable.")
         Just AdvApp -> Hidden ("Variable " <> ppr v <> " is no longer in scope: It occurs under adv.")
+        Just FunDef -> if (isStable (stableTypes c) (varType v)) then Visible
+          else Hidden ("Variable " <> ppr v <> " is no longer in scope: It occurs in a function that is defined under a delay, is a of a non-stable type " <> ppr (varType v) <> ", and is bound outside delay")
         Nothing
           | maybe False (Set.member v) (earlier c) ->
             if isStable (stableTypes c) (varType v) then Visible
@@ -147,14 +145,15 @@
 
 
 
-emptyCtx :: Maybe (Set Var,Var) -> Ctx
-emptyCtx mvar =
+emptyCtx :: Maybe (Set Var) -> Var -> Ctx
+emptyCtx mvar fun =
   Ctx { current =  Set.empty,
         earlier = Nothing,
         hidden = Map.empty,
         hiddenRec = Map.empty,
         srcLoc = UnhelpfulSpan "<no location info>",
         recDef = mvar,
+        funDef = fun,
         primAlias = Map.empty,
         stableTypes = Set.empty,
         stabilized = isJust mvar}
@@ -187,18 +186,20 @@
   = checkExpr c e
 checkExpr c@Ctx{current = cur, hidden = hid, earlier = earl} (App e1 e2) =
   case isPrimExpr c e1 of
-    Just (Prim1 p,v) -> case p of
+    Just (p,v) -> case p of
       Box -> do
         ch <- checkExpr (stabilize BoxApp c) e2
         -- don't bother with a warning if the scopecheck fails
-        when (ch && stabilized c)  (printMessage' SevWarning c v
-          (text "box nested inside another box or recursive definition can cause time leaks"))
+        when (ch && stabilized c && not (isStable (stableTypes c) (exprType e2)))
+          (printMessage' SevWarning c v
+           (text "When box is used inside another box or a recursive definition, it can cause time leaks unless applied to an expression of stable type"))
         return ch
       Arr -> do
         ch <- checkExpr (stabilize BoxApp c) e2
         -- don't bother with a warning if the scopecheck fails
-        when (ch && stabilized c)  (printMessage' SevWarning c v
-          (text "arr nested inside a box or recursive definition can cause time leaks"))
+        when (ch && stabilized c && not (isStable (stableTypes c) (exprType e2)))
+          (printMessage' SevWarning c v
+            (text "When arr is used inside box or a recursive definition, it can cause time leaks unless applied to an expression of stable type"))
         return ch
 
       Unbox -> checkExpr c e2
@@ -213,9 +214,6 @@
 checkExpr c (Case e v _ alts) =
     liftM2 (&&) (checkExpr c e) (liftM and (mapM (\ (_,vs,e)-> checkExpr (addVars vs c') e) alts))
   where c' = addVars [v] c
-checkExpr c@Ctx{earlier = Just _} (Lam v _) =
-  printMessageCheck SevError c v (text "Functions may not be defined under delay."
-                                  $$ "In order to define a function under delay, you have to wrap it in box.")
 checkExpr c (Lam v e)
   | isTyVar v || (not $ tcIsLiftedTypeKind $ typeKind $ varType v) = do
       is <- isStableConstr (varType v)
@@ -223,7 +221,7 @@
             Nothing -> c
             Just t -> c{stableTypes = Set.insert t (stableTypes c)}
       checkExpr c' e
-  | otherwise = checkExpr (addVars [v] c) e
+  | otherwise = checkExpr (addVars [v] (stabilizeLater c)) e
 checkExpr _ (Type _)  = return True
 checkExpr _ (Lit _)  = return True
 checkExpr _ (Coercion _)  = return True
@@ -246,29 +244,21 @@
   where vs = map fst binds
         vs' = Set.fromList vs
         ctxHid = maybe (current c) (Set.union (current c)) (earlier c)
-        recHid = maybe ctxHid (Set.union ctxHid . fst) (recDef c)
+        recHid = maybe ctxHid (Set.union ctxHid) (recDef c)
         c' v = c {current = Set.empty,
                   earlier = Nothing,
                   hidden =  hidden c `Map.union`
                    (Map.fromSet (const (NestedRec v)) recHid),
-                  recDef = Just (vs',v),
+                  recDef = Just (vs'),
+                  funDef = v,
                   stabilized = True}
-checkExpr c@Ctx{earlier = earl}  (Var v)
+checkExpr c (Var v)
   | tcIsLiftedTypeKind $ typeKind $ varType v =
     case isPrim c v of
-      Just (Prim1 _) ->
-        printMessageCheck SevError c v (ppr v <> text " must be applied to an argument")
-      Just (Prim2 p) ->
-        let dapp = case earl of
-              Just _ ->
-                printMessageCheck SevError c v (ppr v <> text " may not be used under delay")
-              _ -> return True
- 
-        in case p of
-             DApp -> dapp
-             DAppP -> dapp
-             BApp -> return True
-             BAppP -> return True
+      Just p ->
+        case p of
+          Unbox -> return True
+          _ -> printMessage SevError (nameSrcSpan (varName (funDef c))) ("Defining an alias for " <> ppr v <> " is not allowed") >> return False
       _ -> case getScope c v of
              Hidden reason -> printMessageCheck SevError c v reason
              Visible -> return True
@@ -276,8 +266,6 @@
                 (ppr v <> text " is an external temporal function used under delay, which may cause time leaks")
 
   | otherwise = return True
-
-
 
 
 
diff --git a/src/Rattus/Plugin/Strictify.hs b/src/Rattus/Plugin/Strictify.hs
--- a/src/Rattus/Plugin/Strictify.hs
+++ b/src/Rattus/Plugin/Strictify.hs
@@ -1,44 +1,55 @@
+{-# LANGUAGE OverloadedStrings #-}
+
 module Rattus.Plugin.Strictify where
 import Prelude hiding ((<>))
 import Rattus.Plugin.Utils
 import GhcPlugins
 
 
-strictifyExpr :: CoreExpr -> CoreM CoreExpr
-strictifyExpr (Let (NonRec b e1) e2) = do
-  e1' <- strictifyExpr e1
-  e2' <- strictifyExpr e2
-  return (Let (NonRec b e1') e2')
-strictifyExpr (Case e b t alts) = do
-  e' <- strictifyExpr e
-  alts' <- mapM (\(c,args,e) -> fmap (\e' -> (c,args,e')) (strictifyExpr e)) alts
+data SCxt = SCxt {srcSpan :: SrcSpan, checkStrictData :: Bool}
+
+
+strictifyExpr :: SCxt -> CoreExpr -> CoreM CoreExpr
+strictifyExpr ss (Let (NonRec b e1) e2) = do
+  e1' <- strictifyExpr ss e1
+  e2' <- strictifyExpr ss e2
+  return (Case e1' b (exprType e2) [(DEFAULT, [], e2')])
+strictifyExpr ss (Case e b t alts) = do
+  e' <- strictifyExpr ss e
+  alts' <- mapM (\(c,args,e) -> fmap (\e' -> (c,args,e')) (strictifyExpr ss e)) alts
   return (Case e' b t alts')
-strictifyExpr (Let (Rec es) e) = do
-  es' <- mapM (\ (b,e) -> strictifyExpr e >>= \e'-> return (b,e')) es
-  e' <- strictifyExpr e
+strictifyExpr ss (Let (Rec es) e) = do
+  es' <- mapM (\ (b,e) -> strictifyExpr ss e >>= \e'-> return (b,e')) es
+  e' <- strictifyExpr ss e
   return (Let (Rec es') e')
-strictifyExpr (Lam b e) = do
-  e' <- strictifyExpr e
-  return (Lam b e')
-strictifyExpr (Cast e c) = do
-  e' <- strictifyExpr e
+strictifyExpr ss (Lam b e)
+   | not (isCoVar b) && not (isTyVar b) && tcIsLiftedTypeKind(typeKind (varType b))
+    = do
+       e' <- strictifyExpr ss e
+       b' <- mkSysLocalM (fsLit "strict") (varType b)
+       return (Lam b' (Case (varToCoreExpr b') b (exprType e) [(DEFAULT,[],e')]))
+   | otherwise = do
+       e' <- strictifyExpr ss e
+       return (Lam b e')
+strictifyExpr ss (Cast e c) = do
+  e' <- strictifyExpr ss e
   return (Cast e' c)
-strictifyExpr (Tick t e) = do
-  e' <- strictifyExpr e
+strictifyExpr ss (Tick t@(SourceNote span _) e) = do
+  e' <- strictifyExpr (ss{srcSpan = RealSrcSpan span}) e
   return (Tick t e')
-strictifyExpr e@(App e1 e2)
-  | not (isType e2) && tcIsLiftedTypeKind(typeKind (exprType e2)) && not (isDelayApp e1)
-    && not (isDelayApp e2) = do
-  e1' <- strictifyExpr e1
-  e2' <- strictifyExpr e2
-  b <- mkSysLocalM (fsLit "strict") (exprType e2)
-  return $ Case e2' b (exprType e) [(DEFAULT, [], App e1' (Var b))]
+strictifyExpr ss (App e1 e2)
+  | (checkStrictData ss && not (isType e2) && tcIsLiftedTypeKind(typeKind (exprType e2))
+        && not (isStrict (exprType e2))) = do
+      (printMessage SevWarning (srcSpan ss)
+         (text "The use of lazy type " <> ppr (exprType e2) <> " may lead to memory leaks"))
+      e1' <- strictifyExpr ss{checkStrictData = False} e1
+      e2' <- strictifyExpr ss{checkStrictData = False} e2
+      return (App e1' e2')
   | otherwise = do
-  e1' <- strictifyExpr e1
-  e2' <- strictifyExpr e2
-  return (App e1' e2')
-strictifyExpr e = return e
-
+      e1' <- strictifyExpr ss e1
+      e2' <- strictifyExpr ss e2
+      return (App e1' e2')
+strictifyExpr _ss e = return e
 
 
 isDelayApp (App e _) = isDelayApp e
diff --git a/src/Rattus/Plugin/Utils.hs b/src/Rattus/Plugin/Utils.hs
--- a/src/Rattus/Plugin/Utils.hs
+++ b/src/Rattus/Plugin/Utils.hs
@@ -8,6 +8,7 @@
   isGhcModule,
   getNameModule,
   isStable,
+  isStrict,
   isTemporal,
   userFunction,
   isType)
@@ -19,6 +20,7 @@
 import Data.Set (Set)
 import qualified Data.Set as Set
 import Data.Char
+import Data.Maybe
 
 isType Type {} = True
 isType (App e _) = isType e
@@ -80,7 +82,7 @@
 
 -- | The set of stable built-in types.
 ghcStableTypes :: Set FastString
-ghcStableTypes = Set.fromList ["Int","Bool","Float","Double","Char"]
+ghcStableTypes = Set.fromList ["Int","Bool","Float","Double","Char", "IO"]
 
 
 newtype TypeCmp = TC Type
@@ -166,7 +168,66 @@
         _ -> False
 
 
-          
+
+isStrict :: Type -> Bool
+isStrict t = isStrictRec 0 Set.empty t
+
+-- | Check whether the given type is stable. This check may use
+-- 'Stable' constraints from the context.
+
+isStrictRec :: Int -> Set TypeCmp -> Type -> Bool
+-- To prevent infinite recursion (when checking recursive types) we
+-- keep track of previously checked types. This, however, is not
+-- enough for non-regular data types. Hence we also have a counter.
+isStrictRec d _ _ | d == 100 = True
+isStrictRec _ pr t | Set.member (TC t) pr = True
+isStrictRec d pr t = do
+  let pr' = Set.insert (TC t) pr
+  let (_,t') = splitForAllTys t
+  let (c, tys) = repSplitAppTys t'
+  if isJust (getTyVar_maybe c) then and (map (isStrictRec (d+1) pr') tys)
+  else  case splitTyConApp_maybe t' of
+    Nothing -> isJust (getTyVar_maybe t)
+    Just (con,args) ->
+      case getNameModule con of
+        Nothing -> False
+        Just (name,mod)
+          -- If it's a Rattus type constructor check if it's a box
+          | isRattModule mod && (name == "Box" || name == "O") -> True
+            -- If its a built-in type check the set of stable built-in types
+          | isGhcModule mod -> name `Set.member` ghcStableTypes
+          {- deal with type synonyms (does not seem to be necessary (??))
+           | Just (subst,ty,[]) <- expandSynTyCon_maybe con args ->
+             isStrictRec c (d+1) pr' (substTy (extendTvSubstList emptySubst subst) ty) -}
+          | isFunTyCon con -> True
+          | isAlgTyCon con -> 
+            case algTyConRhs con of
+              DataTyCon {data_cons = cons, is_enum = enum}
+                | enum -> True
+                | and $ (map (isSrcStrictOrDelay args)) $ cons ->
+                  and  (map check cons)
+                | otherwise -> False
+                where check con = case dataConInstSig con args of
+                        (_, _,tys) -> and (map (isStrictRec (d+1) pr') tys)
+              TupleTyCon {} -> null args
+              _ -> False
+          | otherwise -> False
+            
+
+
+
+
+isSrcStrictOrDelay :: [Type] -> DataCon -> Bool
+isSrcStrictOrDelay args con = and (zipWith check tys (dataConSrcBangs con))
+  where (_, _,tys) = dataConInstSig con args 
+        check ty b = isSrcStrict' b || isDelay ty
+        isDelay ty = case splitTyConApp_maybe ty of
+                       Just (con,_) ->
+                         case getNameModule con of
+                           Just (name,mod) | isRattModule mod && name == "O" -> True
+                           _ -> False
+                       _ -> False
+
 isSrcStrict' (HsSrcBang _ _ SrcStrict) = True
 isSrcStrict' _ = False
 
diff --git a/src/Rattus/Primitives.hs b/src/Rattus/Primitives.hs
--- a/src/Rattus/Primitives.hs
+++ b/src/Rattus/Primitives.hs
@@ -17,11 +17,6 @@
   ) where
 
 
--- | To prevent the user from declaring instances of Stable, we do not
--- export the 'StableInternal' class it depends on.
-
-class StableInternal a where
-
 -- | A type is @Stable@ if it is a strict type and the later modality
 -- @O@ and function types only occur under @Box@.
 --
@@ -32,7 +27,7 @@
 -- not strict), @Int -> Int@, (function type is not stable), @O
 -- Int@, @Str Int@.
 
-class StableInternal a => Stable a  where
+class  Stable a  where
 
 -- | The "later" type modality. A value of type @O a@ is a computation
 -- that produces a value of type @a@ in the next time step. Use
@@ -50,16 +45,19 @@
 -- > --------------------
 -- >  Γ ⊢ delay t :: O 𝜏
 --
+{-# INLINE [1] delay #-}
 delay :: a -> O a
 delay x = Delay x
 
 
+
 -- | This is the eliminator for the "later" modality 'O':
 --
 -- >     Γ ⊢ t :: O 𝜏
 -- > ---------------------
 -- >  Γ ✓ Γ' ⊢ adv t :: 𝜏
 --
+{-# INLINE [1] adv #-}
 adv :: O a -> a
 adv (Delay x) = x
 
@@ -73,7 +71,7 @@
 -- where Γ☐ is obtained from Γ by removing ✓ and any variables @x ::
 -- 𝜏@, where 𝜏 is not a stable type.
 
-
+{-# INLINE [1] box #-}
 box :: a -> Box a
 box x = Box x
 
@@ -84,6 +82,25 @@
 -- >   Γ ⊢ t :: Box 𝜏
 -- > ------------------
 -- >  Γ ⊢ unbox t :: 𝜏
-
+{-# INLINE [1] unbox #-}
 unbox :: Box a -> a
 unbox (Box d) = d
+
+
+{-# RULES
+  "unbox/box"    forall x. unbox (box x) = x
+    #-}
+
+
+{-# RULES
+  "box/unbox"    forall x. box (unbox x) = x
+    #-}
+
+                
+{-# RULES
+  "adv/delay"    forall x. adv (delay x) = x
+    #-}
+                
+{-# RULES
+  "delay/adv"    forall x. delay (adv x) = x
+    #-}
diff --git a/src/Rattus/Stream.hs b/src/Rattus/Stream.hs
--- a/src/Rattus/Stream.hs
+++ b/src/Rattus/Stream.hs
@@ -45,17 +45,20 @@
 tl :: Str a -> O (Str a)
 tl (_ ::: xs) = xs
 
-
 -- | Apply a function to each element of a stream.
 map :: Box (a -> b) -> Str a -> Str b
+{-# NOINLINE [1] map #-}
 map f (x ::: xs) = unbox f x ::: delay (map f (adv xs))
 
+
 -- | Construct a stream that has the same given value at each step.
+{-# NOINLINE [1] const #-}
 const :: Stable a => a -> Str a
 const a = a ::: delay (const a)
 
 -- | Variant of 'const' that allows any type @a@ as argument as long
 -- as it is boxed.
+{-# NOINLINE [1] constBox #-}
 constBox :: Box a -> Str a
 constBox a = unbox a ::: delay (constBox a)
 
@@ -70,6 +73,7 @@
 -- > scan (box f) x (v1 ::: v2 ::: v3 ::: ... ) == (x `f` v1) ::: ((x `f` v1) `f` v2) ::: ...
 --
 -- Note: Unlike 'scanl', 'scan' starts with @x `f` v1@, not @x@.
+{-# NOINLINE [1] scan #-}
 scan :: (Stable b) => Box(b -> a -> b) -> b -> Str a -> Str b
 scan f acc (a ::: as) =  acc' ::: delay (scan f acc' (adv as))
   where acc' = unbox f acc a
@@ -77,12 +81,12 @@
 -- | 'scanMap' is a composition of 'map' and 'scan':
 --
 -- > scanMap f g x === map g . scan f x
+{-# NOINLINE [1] scanMap #-}
 scanMap :: (Stable b) => Box(b -> a -> b) -> Box (b -> c) -> b -> Str a -> Str c
 scanMap f p acc (a ::: as) =  unbox p acc' ::: delay (scanMap f p acc' (adv as))
   where acc' = unbox f acc a
 
 
-
 -- | 'scanMap2' is similar to 'scanMap' but takes two input streams.
 scanMap2 :: (Stable b) => Box(b -> a1 -> a2 -> b) -> Box (b -> c) -> b -> Str a1 -> Str a2 -> Str c
 scanMap2 f p acc (a1 ::: as1) (a2 ::: as2) =
@@ -94,6 +98,7 @@
 zipWith f (a ::: as) (b ::: bs) = unbox f a b ::: delay (zipWith f (adv as) (adv bs))
 
 -- | Similar to 'Prelude.zip' on Haskell lists.
+{-# NOINLINE [1] zip #-}
 zip :: Str a -> Str b -> Str (a:*b)
 zip (a ::: as) (b ::: bs) =  (a :* b) ::: delay (zip (adv as) (adv bs))
 
@@ -129,3 +134,30 @@
 integral :: (Stable a, VectorSpace a s) => a -> Str s -> Str a -> Str a
 integral acc (t ::: ts) (a ::: as) = acc' ::: delay (integral acc' (adv ts) (adv as))
   where acc' = acc ^+^ (t *^ a)
+
+
+
+{-# RULES
+
+  "const/map" forall (f :: Stable b => Box (a -> b))  x.
+    map f (const x) = let x' = unbox f x in const x' ;
+
+  "map/map" forall f g xs.
+    map f (map g xs) = map (box (unbox f . unbox g)) xs ;
+
+  "map/scan" forall f p acc as.
+    map p (scan f acc as) = scanMap f p acc as ;
+
+  "scan/scan" forall f g b c as.
+    scan g c (scan f b as) =
+      let f' = unbox f; g' = unbox g in
+      scanMap (box (\ (b:*c) a -> let b' = f' b a in (b':* g' c b'))) (box snd') (b:*c) as ;
+
+  "scan/scanMap" forall f g p b c as.
+    scan g c (scanMap f p b as) =
+      let f' = unbox f; g' = unbox g; p' = unbox p in
+      scanMap (box (\ (b:*c) a -> let b' = f' (p' b) a in (b':* g' c b'))) (box snd') (b:*c) as ;
+
+  "zip/map" forall xs ys f.
+    map f (zip xs ys) = let f' = unbox f in zipWith (box (\ x y -> f' (x :* y))) xs ys
+#-}
diff --git a/src/Rattus/Strict.hs b/src/Rattus/Strict.hs
--- a/src/Rattus/Strict.hs
+++ b/src/Rattus/Strict.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
@@ -10,8 +11,12 @@
 module Rattus.Strict
   ( List(..),
     reverse',
+    (+++),
+    listToMaybe',
+    mapMaybe',
     (:*)(..),
     Maybe'(..),
+    maybe',
    fst',
    snd',
   )where
@@ -19,6 +24,7 @@
 import Data.VectorSpace
 
 infixr 2 :*
+infixr 8 :!
 
 -- | Strict list type.
 data List a = Nil | !a :! !(List a)
@@ -29,7 +35,30 @@
   where
     rev Nil     a = a
     rev (x:!xs) a = rev xs (x:!a)
+    
+-- | Returns @'Nothing''@ on an empty list or @'Just'' a@ where @a@ is the
+-- first element of the list.
+listToMaybe' :: List a -> Maybe' a
+listToMaybe' = foldr (const . Just') Nothing'
 
+-- | Append two lists.
+(+++) :: List a -> List a -> List a
+(+++) Nil     ys = ys
+(+++) (x:!xs) ys = x :! xs +++ ys
+
+
+-- | A version of 'map' which can throw out elements.  In particular,
+-- the function argument returns something of type @'Maybe'' b@.  If
+-- this is 'Nothing'', no element is added on to the result list.  If
+-- it is @'Just'' b@, then @b@ is included in the result list.
+mapMaybe'          :: (a -> Maybe' b) -> List a -> List b
+mapMaybe' _ Nil     = Nil
+mapMaybe' f (x:!xs) =
+ let rs = mapMaybe' f xs in
+ case f x of
+  Nothing' -> rs
+  Just' r  -> r:!rs
+
 instance Foldable List where
   
   foldMap f = run where
@@ -56,6 +85,14 @@
 
 -- | Strict variant of 'Maybe'.
 data Maybe' a = Just' ! a | Nothing'
+
+-- | takes a default value, a function, and a 'Maybe'' value.  If the
+-- 'Maybe'' value is 'Nothing'', the function returns the default
+-- value.  Otherwise, it applies the function to the value inside the
+-- 'Just'' and returns the result.
+maybe' :: b -> (a -> b) -> Maybe' a -> b
+maybe' n _ Nothing'  = n
+maybe' _ f (Just' x) = f x
 
 -- | Strict pair type.
 data a :* b = !a :* !b
diff --git a/src/Rattus/ToHaskell.hs b/src/Rattus/ToHaskell.hs
--- a/src/Rattus/ToHaskell.hs
+++ b/src/Rattus/ToHaskell.hs
@@ -17,6 +17,7 @@
 import Rattus.Primitives
 import Rattus.Stream
 import Rattus.Yampa
+import Rattus.Strict
 
 
 -- | A state machine that takes inputs of type @a@ and produces output
@@ -42,7 +43,7 @@
 -- | Turn a signal function into a state machine from inputs of type
 -- @a@ and time (since last input) to output of type @b@.
 runSF :: SF a b -> Trans (a, Double) b
-runSF sf = Trans (\(a,t) -> let (s, b) = stepSF sf t a in (b, runSF (adv s)))
+runSF sf = Trans (\(a,t) -> let (s:* b) = stepSF sf t a in (b, runSF (adv s)))
 
 
 -- | Turns a lazy infinite list into a stream.
diff --git a/src/Rattus/Yampa.hs b/src/Rattus/Yampa.hs
--- a/src/Rattus/Yampa.hs
+++ b/src/Rattus/Yampa.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE TypeOperators #-}
 {-# OPTIONS -fplugin=Rattus.Plugin #-}
 {-# LANGUAGE Arrows #-}
 {-# LANGUAGE RebindableSyntax #-}
@@ -45,58 +46,58 @@
 -- | Signal functions from inputs of type @a@ to outputs of type @b@.
 data SF a b = SF{
   -- | Run a signal function for one step.
-  stepSF :: DTime -> a -> (O(SF a b), b)}
+  stepSF :: ! (DTime -> a -> (O(SF a b) :* b))}
 
 -- | The identity signal function that does nothing.
 identity :: SF a a
-identity = SF (\ _ x -> (delay identity,x))
+identity = SF (\ _ x -> (delay identity :* x))
 
 -- | Compose two signal functions.
 compose :: SF b c -> SF a b -> SF a c
 compose (SF sf2) (SF sf1) = SF sf
-  where sf d a = let (r1, b) = sf1 d a
-                     (r2, c) = sf2 d b
-                 in (delay (compose (adv r2) (adv r1)), c)
+  where sf d a = let (r1 :* b) = sf1 d a
+                     (r2 :* c) = sf2 d b
+                 in (delay (compose (adv r2) (adv r1)) :* c)
 
 -- | Compute the integral of a signal. The first argument is the
 -- offset.
 integral :: (Stable a, VectorSpace a s) => a -> SF a a
 integral acc = SF sf'
   where sf' t a = let acc' = acc ^+^ (realToFrac t *^ a)
-                  in (delay (integral acc'), acc')
+                  in (delay (integral acc') :* acc')
 
 -- | @switch s f@ behaves like @s@ composed with @arr fst@ until @s@
 -- produces a value of the form @Just' c@ in the second
 -- component. From then on it behaves like $f c@.
-switch :: SF a (b, Maybe' c) -> Box (c -> SF a b) -> SF a b
+switch :: SF a (b :* Maybe' c) -> Box (c -> SF a b) -> SF a b
 switch (SF sf) f = SF sf'
-  where sf' t a = let (nxt, (b,c')) =  sf t a
+  where sf' t a = let (nxt :* (b :* c')) =  sf t a
                   in case c' of
                        Just' c -> stepSF (unbox f c) t a
-                       Nothing' -> (delay (switch (adv nxt) f), b)
+                       Nothing' -> (delay (switch (adv nxt) f):* b)
 
 -- | @rSwitch s@ behaves like @s@, but every time the second input is
 -- of the form @Just' s'@ it will change behaviour to @s'@.
-rSwitch :: SF a b -> SF (a, Maybe' (SF a b)) b
+rSwitch :: SF a b -> SF (a :* Maybe' (SF a b)) b
 rSwitch (SF sf) = SF sf'
-  where sf' t (a,m) = case m of
+  where sf' t (a :* m) = case m of
                         Just' (SF newSf) ->
-                           let (nxt, b) = newSf t a
-                           in (delay (rSwitch (adv nxt)),b)
-                        Nothing' -> let (nxt, b) = sf t a
-                                   in (delay (rSwitch (adv nxt)),b)
+                           let (nxt :* b) = newSf t a
+                           in (delay (rSwitch (adv nxt)) :* b)
+                        Nothing' -> let (nxt :* b) = sf t a
+                                   in (delay (rSwitch (adv nxt)) :* b)
 
 -- | Constant signal function.
 constant :: Stable b => b -> SF a b
 constant x = run
-  where run = SF (\ _ _ -> (delay run,x))
+  where run = SF (\ _ _ -> (delay run :* x))
 
 -- | The output at time zero is the first argument, and from that
 -- point on it behaves like the signal function passed as second
 -- argument.
 (-->) :: b -> SF a b -> SF a b
 b --> (SF sf) = SF sf'
-  where sf' d x = (fst (sf d x),b)
+  where sf' d x = (fst' (sf d x) :* b)
 
 -- | Insert a sample in the output, and from that point on, behave
 -- like the given signal function.
@@ -105,7 +106,7 @@
 -- argument must be delayed (or boxed).
 (-:>) :: b -> O (SF a b) -> SF a b
 b -:> sf = SF sf'
-  where sf' _d _x = (sf,b)
+  where sf' _d _x = (sf :* b)
 
 -- | The input at time zero is the first argument, and from that point
 -- on it behaves like the signal function passed as second argument.
@@ -118,8 +119,8 @@
 -- zero.
 (-=>) :: (b -> b) -> SF a b -> SF a b
 f -=> (SF sf) = SF sf'
-  where sf' d a = let (r,b) = sf d a
-                  in (r,f b)
+  where sf' d a = let (r:*b) = sf d a
+                  in (r:*f b)
                      
 -- | Apply a function to the first input value at time
 -- zero.
@@ -138,35 +139,38 @@
 -- must be boxed.
 arrPrim :: Box (a -> b) -> SF a b
 arrPrim f = run where
-  run = SF (\ _d a -> (delay run, unbox f a ))
+  run = SF (\ _d a -> (delay run:* unbox f a ))
 
 
+{-# ANN firstPrim AllowLazyData #-}
 -- | Apply a signal function to the first component.
 firstPrim :: SF a b -> SF (a,c) (b,c)
 firstPrim (SF sf) = SF sf'
-  where sf' d (a,c) = let (r, b) = sf d a
-                      in (delay (firstPrim (adv r)), (b,c))
+  where sf' d (a,c) = let (r:* b) = sf d a
+                       in (delay (firstPrim (adv r)):* (b,c))
 
+{-# ANN secondPrim AllowLazyData #-}
 -- | Apply a signal function to the second component.
 secondPrim :: SF a b -> SF (c,a) (c,b)
 secondPrim (SF sf) = SF sf'
-  where sf' d (c,a) = let (r, b) = sf d a
-                      in (delay (secondPrim (adv r)), (c,b))
-
+  where sf' d (c,a) = let (r:* b) = sf d a
+                       in (delay (secondPrim (adv r)):* (c,b))
 
+{-# ANN parSplitPrim AllowLazyData #-}
 -- | Apply two signal functions in parallel.
 parSplitPrim :: SF a b -> SF c d  -> SF (a,c) (b,d)
 parSplitPrim (SF sf1) (SF sf2) = SF sf'
-  where sf' dt (a,c) = let (r1, b) = sf1 dt a
-                           (r2, d) = sf2 dt c
-                       in (delay (parSplitPrim (adv r1) (adv r2)), (b,d))
+  where sf' dt (a,c) = let (r1:* b) = sf1 dt a
+                           (r2:* d) = sf2 dt c
+                       in (delay (parSplitPrim (adv r1) (adv r2)):* (b,d))
 
+{-# ANN parFanOutPrim AllowLazyData #-}
 -- | Apply two signal functions in parallel on the same input.
 parFanOutPrim :: SF a b -> SF a c -> SF a (b, c)
 parFanOutPrim (SF sf1) (SF sf2) = SF sf'
-  where sf' dt a = let (r1, b) = sf1 dt a
-                       (r2, c) = sf2 dt a
-                   in (delay (parFanOutPrim (adv r1) (adv r2)), (b,c))
+  where sf' dt a = let (r1:* b) = sf1 dt a
+                       (r2:* c) = sf2 dt a
+                   in (delay (parFanOutPrim (adv r1) (adv r2)):* (b,c))
 
 instance Category SF where
   id = identity
@@ -184,10 +188,10 @@
 -- 
 -- Note: The type of @loopPre@ is different from Yampa's as we need
 -- the @O@ type here.
-loopPre :: c -> SF (a,c) (b,O c) -> SF a b
+loopPre :: c -> SF (a:*c) (b:*O c) -> SF a b
 loopPre c (SF sf) = SF sf'
-  where sf' d a = let (r, (b,c')) = sf d (a,c)
-                  in (delay (loopPre (adv c') (adv r)), b)
+  where sf' d a = let (r:* (b:*c')) = sf d (a:*c)
+                  in (delay (loopPre (adv c') (adv r)):* b)
 
 
 -- | Precomposition with a pure function.
diff --git a/test/IllTyped.hs b/test/IllTyped.hs
--- a/test/IllTyped.hs
+++ b/test/IllTyped.hs
@@ -11,15 +11,28 @@
 -- {-# ANN module Rattus #-}
 
 
-dblDelay :: Box (O (O Int))
-dblDelay = box (delay (delay 1))
+-- This function will produce a confusing scoping error message since
+-- GHC will inline the let-binding before Rattus' scope checker gets
+-- to see it.
+advDelay :: O (O a) -> O a
+advDelay y = delay (let x = adv y in adv x)
 
-lambdaUnderDelay :: Box (O (O Int -> Int -> Int))
-lambdaUnderDelay = box (delay (\x _ -> adv x))
+dblDelay :: O (O Int)
+dblDelay = delay (delay 1)
 
-sneakyLambdaUnderDelay :: Box (O (O Int -> Int -> Int))
-sneakyLambdaUnderDelay = box (delay (let f x _ =  adv x in f))
+lambdaUnderDelay :: O (O Int -> Int -> Int)
+lambdaUnderDelay = delay (\x _ -> adv x)
 
+sneakyLambdaUnderDelay :: O (O Int -> Int -> Int)
+sneakyLambdaUnderDelay = delay (let f x _ =  adv x in f)
+
+
+lambdaUnderDelay' :: O Int -> O (Int -> O Int)
+lambdaUnderDelay' x = delay (\_ -> x)
+
+sneakyLambdaUnderDelay' :: O Int -> O (Int -> O Int)
+sneakyLambdaUnderDelay' x = delay (let f _ =  x in f)
+
 leaky :: (() -> Bool) -> Str Bool
 leaky p = p () ::: delay (leaky (\ _ -> hd (leaky (\ _ -> True))))
 
@@ -29,6 +42,21 @@
 boxStream :: Str Int -> Box (Str Int)
 boxStream s = box (0 ::: tl s)
 
+boxStream' :: Str Int -> Box (Str Int)
+boxStream' s = box s
+
+
+intDelay :: Int -> O Int
+intDelay = delay
+
+intAdv :: O Int -> Int
+intAdv = adv
+
+
+newDelay :: a -> O a
+newDelay x = delay x
+
+
 mutualLoop :: a
 mutualLoop = mutualLoop'
 
@@ -45,7 +73,11 @@
 mapUnboxed :: (a -> b) -> Str a -> Str b
 mapUnboxed f = run
   where run (x ::: xs) = f x ::: delay (run (adv xs))
-
+  
+mapUnboxedMutual :: (a -> b) -> Str a -> Str b
+mapUnboxedMutual f = run
+  where run (x ::: xs) = f x ::: delay (run' (adv xs))
+        run' (x ::: xs) = f x ::: delay (run (adv xs))
 
 data Input = Input {jump :: !Bool, move :: Move}
 data Move = StartLeft | EndLeft | StartRight | EndRight | NoMove
diff --git a/test/MemoryLeak.hs b/test/MemoryLeak.hs
--- a/test/MemoryLeak.hs
+++ b/test/MemoryLeak.hs
@@ -8,20 +8,9 @@
 import qualified Prelude
 import Prelude hiding ((<*>), map)
 
--- If we make pairs stable, we get a memory leak:
--- cannot do this anymore. We dissallow user-supplied Stable instances
--- instance (Stable a, Stable b) => Stable (a,b)
 
-
-type Lazy a = ((),a)
-
 {-# ANN module Rattus #-}
 
-
-lazyAdd :: (a, Int) -> ((), Int) -> ((), Int)
-lazyAdd = (\ (_,x) y -> fmap (+x) y )
-
-
 scan3 :: (Stable a) => Box(a -> a -> a) -> Box (a -> Bool) -> a -> Str a -> Str a
 scan3 f p acc (a ::: as) =  (if unbox p a then acc else a)
       ::: (delay (scan3 f p acc') <*> as)
@@ -35,25 +24,27 @@
 
 
 
--- Unless the strictification transformation is applied this function
--- will leak memory. In addition, since it uses a lazy data structure,
--- it would also leak memory unless progres/promote evaluate to normal
--- form (using deepseq).
--- test2 :: Lazy Int -> Str (Lazy Int) -> Str (Lazy Int)
--- test2 = scan3 (box lazyAdd) (box (\ (_,x) -> x == 0))
+-- If we Haskell's (lazy) pair types, we get a memory leak:
 
--- If we Haskell's pair types, we get a memory leak:
+type Lazy a = ((),a)
 
-leaky :: Str (Lazy Int) -> Str (Lazy Int)
-leaky ((_,x):::xs) = ((),1) ::: delay (leaky  (fmap ((+) x) (hd (adv xs)) ::: (tl (adv xs))))
+leakyLazy :: Str (Lazy Int) -> Str (Lazy Int)
+leakyLazy ((_,x):::xs) = ((),1) ::: delay (leakyLazy  (fmap ((+) x) (hd (adv xs)) ::: (tl (adv xs))))
 
 
+-- If we use a strict pair type, we avoid the memory leak
+
 type Strict a = (():*a)
 
 leakyStrict :: Str (Strict Int) -> Str (Strict Int)
 leakyStrict ((_:*x):::xs) = (():*11) ::: delay (leakyStrict  (fmap ((+) x) (hd (adv xs)) ::: (tl (adv xs))))
 
 
+-- Unless the strictification transformation is applied this function
+-- will leak memory.
+leaky :: Str (Int) -> Str (Int)
+leaky (x:::xs) = 1 ::: delay (leaky  ((x +  hd (adv xs)) ::: (tl (adv xs))))
+
 buffer :: Stable a => Str a -> Str (List a)
 buffer = scan (box (flip (:!))) Nil
 
@@ -64,16 +55,20 @@
 recurse _ [] = putStrLn "the impossible happened: stream terminated"
 
 {-# ANN main NotRattus #-}
-main = do  
+main  = do  
   let x =  fromStr $ test1 1 (toStr [1..])
   recurse 10000000 x
+
+  let x = fromStr $ leaky (toStr $ [1..])
+  recurse 10000000 x
   
   let x = fromStr $ leakyStrict  (toStr $ Prelude.map (\ x-> (():*x)) [1..])
   recurse 10000000 x
 
-
-  let x = fromStr $ leaky (toStr $ Prelude.map (\ x-> ((),x)) [1..])
+  -- This will leak du to lazy data structure
+  let x = fromStr $ leakyLazy (toStr $ Prelude.map (\ x-> ((),x)) [1..])
   recurse 10000000 x
+
   
 --   -- for comparison the Haskell code below does leak
 --   let x = scan2 (+) (1::Int) [1,1..]
diff --git a/test/Rewrite.hs b/test/Rewrite.hs
new file mode 100644
--- /dev/null
+++ b/test/Rewrite.hs
@@ -0,0 +1,43 @@
+{-# LANGUAGE TypeOperators #-}
+
+module Main (module Main) where
+
+import Rattus
+import Rattus.Stream
+import Prelude hiding ((<*>), map,zip,const)
+
+{-# ANN module Rattus #-}
+
+twice :: Str Int -> Str Int
+twice = map (box (+1)) . map (box (+1))
+
+scanAndMap :: Str Int -> Str Int
+scanAndMap xs = map (box (+1)) (scan (box (+)) 0 xs)
+
+sums :: Str Int -> Str Int
+sums xs = scan (box (+)) 0 xs
+
+twiceScan :: Str Int -> Str Int
+twiceScan xs = scan (box (+)) 0  (scan (box (+)) 0 xs)
+
+twiceScanMap :: Str Int -> Str Int
+twiceScanMap xs = scan (box (+)) 0  (scanMap (box (+)) (box (+1)) 0 xs)
+
+zipMap :: Str Int -> Str Int -> Str Int
+zipMap xs ys = map (box (\ (x:*y) -> x + y)) (zip xs ys)
+
+constMap :: Str Int
+constMap = map (box (+1)) (const 5)
+
+
+
+apply :: O (Int -> Int -> Int) -> O Int -> O Int -> O Int
+apply f x y = f <*> x <*> y
+
+
+apply' :: O (Int -> Int -> Int) -> Int -> O Int -> O Int
+apply' f x y = f <** x <*> y
+
+
+{-# ANN main NotRattus #-}
+main = putStrLn "This is just to test the rewrite rules"
diff --git a/test/WellTyped.hs b/test/WellTyped.hs
--- a/test/WellTyped.hs
+++ b/test/WellTyped.hs
@@ -9,6 +9,28 @@
 
 {-# ANN module Rattus #-}
 
+
+lambdaUnderDelay :: O (Int -> Int -> Int)
+lambdaUnderDelay = delay (\x _ -> x)
+
+sneakyLambdaUnderDelay :: O (Int -> Int -> Int)
+sneakyLambdaUnderDelay = delay (let f x _ =  x in f)
+
+
+lambdaUnderDelay' :: Int -> O (Int -> Int)
+lambdaUnderDelay' x = delay (\_ -> x)
+
+sneakyLambdaUnderDelay' :: Int -> O (Int -> Int)
+sneakyLambdaUnderDelay' x = delay (let f _ =  x in f)
+
+scanBox :: Box(b -> a -> Box b) -> b -> Str a -> Str b
+scanBox f acc (a ::: as) =  unbox acc' ::: delay (scanBox f (unbox acc') (adv as))
+  where acc' = unbox f acc a
+
+
+sumBox :: Str Int -> Str Int
+sumBox = scanBox (box (\x y -> box (x + y))) 0
+
 map1 :: Box (a -> b) -> Str a -> Str b
 map1 f (x ::: xs) = unbox f x ::: delay (map1 f (adv xs))
 
@@ -19,13 +41,21 @@
 map3 f = run
   where run (x ::: xs) = unbox f x ::: (delay run <*> xs)
 
-
 -- mutual recursive definition
 bar1 :: Box (a -> b) -> Str a -> Str b
 bar1 f (x ::: xs) = unbox f x ::: (delay (bar2 f) <*> xs)
 
 bar2 :: Box (a -> b) -> Str a -> Str b
 bar2 f  (x ::: xs) = unbox f x ::: (delay (bar1 f) <*> xs)
+
+
+applyDelay :: O (O (a -> b)) -> O (O a) -> O (O b)
+applyDelay f x = delay (adv f <*> adv x)
+
+
+stableDelay :: Stable a => a -> O a
+stableDelay x = delay x
+
 
 data Input a = Input {jump :: !a, move :: !Move}
 data Move = StartLeft | EndLeft | StartRight | EndRight | NoMove