diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,3 @@
+0.1.0.0
+-------
+initial release
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2020 Patrick Bahr
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright
+   notice, this list of conditions and the following disclaimer in the
+   documentation and/or other materials provided with the distribution.
+
+3. Neither the name of the author nor the names of his contributors
+   may be used to endorse or promote products derived from this software
+   without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS OR
+IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED.  IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR
+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,
+STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
+ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+POSSIBILITY OF SUCH DAMAGE.
diff --git a/Rattus.cabal b/Rattus.cabal
new file mode 100644
--- /dev/null
+++ b/Rattus.cabal
@@ -0,0 +1,159 @@
+cabal-version:       1.18
+name:                Rattus
+version:             0.1.0.0
+category:            FRP
+synopsis:            A modal FRP language
+description:
+
+            This library implements the Rattus programming language as
+            an embedded DSL. To this end the library provides a GHC
+            plugin that performs the additional checks that are
+            necessary for Rattus. What follows is a brief
+            introduction to the language and its usage. A more
+            detailed introduction can be found in this
+            <docs/paper.pdf paper>.
+            
+            .
+            
+            Rattus is a functional reactive programming (FRP) language
+            that uses modal types to ensure operational properties
+            that are crucial for reactive programs: productivity (in
+            each computation step, the program makes progress),
+            causality (output depends only on current and earlier
+            input), and no implicit space leaks (programs do not
+            implicitly retain memory over time).
+            
+            .
+            
+            To ensure these properties, Rattus uses the type modality
+            @O@ to express the concept of time at the type
+            level. Intuitively speaking, a value of type @O a@
+            represents a computation that will produce a value of type
+            @a@ in the next time step. Additionally, the language also
+            features the @Box@ type modality. A value of type @Box a@
+            is a time-independent computation that can be executed at
+            any time to produce a value of type @a@.
+
+            .
+
+            The core of the language is defined in the module
+            "Rattus.Primitives". Note that the operations on @O@ and
+            @Box@ have non-standard typing rules. Therefore, this
+            library provides a compiler plugin that checks these
+            non-standard typing rules. To write Rattus programs, one
+            must enable this plugin via the GHC option
+            @-fplugin=Rattus.Plugin@, e.g. by including the following
+            line in the source file (for better error messages we also
+            suggest using the option @-g2@):
+            
+            .
+            
+            > {-# OPTIONS -fplugin=Rattus.Plugin #-}
+            
+            .
+
+            In addition, one must mark the functions that are written
+            in Rattus:
+
+            .
+            
+            > {-# ANN myFunction Rattus #-}
+
+            .
+
+            Or mark the whole module as a Rattus module:
+            
+            .
+
+            > {-# ANN module Rattus #-}
+
+            .
+
+            Below is a minimal Rattus program using the
+            "Rattus.Stream" module for programming with streams:
+
+            .
+
+            > {-# OPTIONS -fplugin=Rattus.Plugin #-}
+            >     
+            > import Rattus
+            > import Rattus.Stream
+            > 
+            > {-# ANN sums Rattus #-}
+            > sums :: Str Int -> Str Int
+            > sums = scan (box (+)) 0
+
+homepage:            https://github.com/pa-ba/Rattus
+License:             BSD3
+License-file:        LICENSE
+copyright:           Copyright (C) 2020 Patrick Bahr
+Author:              Patrick Bahr
+maintainer:          Patrick Bahr <paba@itu.dk>
+stability:           experimental
+
+build-type:          Custom
+
+extra-source-files:  CHANGELOG.md
+
+extra-doc-files:     docs/paper.pdf
+                     
+custom-setup
+  setup-depends:
+    base  >= 4.5 && < 5,
+    Cabal >= 1.18
+
+
+library
+  exposed-modules:     Rattus
+                       Rattus.Stream
+                       Rattus.Strict
+                       Rattus.Event
+                       Rattus.Events
+                       Rattus.ToHaskell
+                       Rattus.Yampa
+                       
+                       Rattus.Plugin
+                       Rattus.Arrow
+                       Rattus.Primitives
+                       
+  other-modules:       Rattus.Plugin.ScopeCheck
+                       Rattus.Plugin.Strictify
+                       Rattus.Plugin.Utils
+                       Rattus.Plugin.StableSolver
+  build-depends:       base >=4.12 && <5, containers, simple-affine-space, ghc >= 8.6
+  hs-source-dirs:      src
+  default-language:    Haskell2010
+  ghc-options: -W -g2
+  
+Test-Suite memory-leak
+  type:                exitcode-stdio-1.0
+  main-is:             MemoryLeak.hs
+  hs-source-dirs:      test
+  default-language:    Haskell2010
+  build-depends:       Rattus, base
+  ghc-options:         -fplugin=Rattus.Plugin -rtsopts -g2
+
+Test-Suite time-leak
+  type:                exitcode-stdio-1.0
+  main-is:             TimeLeak.hs
+  hs-source-dirs:      test
+  default-language:    Haskell2010
+  build-depends:       Rattus, base
+  ghc-options:         -fplugin=Rattus.Plugin -rtsopts -g2
+  
+Test-Suite ill-typed
+  type:                exitcode-stdio-1.0
+  main-is:             test/IllTyped.hs
+  default-language:    Haskell2010
+  build-depends:       Rattus, base
+  ghc-options:         -fplugin=Rattus.Plugin -rtsopts -g2
+
+
+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
+
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,29 @@
+{-
+Disable some errors and warnings during the haddock pass
+  (caused by compiler plugins and hs-boot)
+ -}
+{-# OPTIONS_GHC -Wall #-}
+module Main (main) where
+
+import Distribution.Simple
+import Distribution.Simple.Setup
+
+main :: IO ()
+main = defaultMainWithHooks simpleUserHooks
+  { confHook = \a -> confHook simpleUserHooks a . tweakFlags }
+
+tweakFlags :: ConfigFlags -> ConfigFlags
+tweakFlags flags = flags
+  { configProgramArgs = addHaddockArgs (configProgramArgs flags) }
+
+addHaddockArgs :: [(String, [String])] -> [(String, [String])]
+addHaddockArgs []
+  = [("haddock", newHaddockGhcArgs)]
+addHaddockArgs (("haddock", args):otherProgsArgs)
+  = ("haddock", args ++ newHaddockGhcArgs) : otherProgsArgs
+addHaddockArgs (progArgs:otherProgsArgs)
+  = progArgs : addHaddockArgs otherProgsArgs
+
+newHaddockGhcArgs :: [String]
+newHaddockGhcArgs =
+  [ "--optghc=-fobject-code" ]
diff --git a/docs/paper.pdf b/docs/paper.pdf
new file mode 100644
Binary files /dev/null and b/docs/paper.pdf differ
diff --git a/src/Rattus.hs b/src/Rattus.hs
new file mode 100644
--- /dev/null
+++ b/src/Rattus.hs
@@ -0,0 +1,43 @@
+{-# OPTIONS -fplugin=Rattus.Plugin #-}
+
+
+-- | 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".
+
+module Rattus (
+  module Rattus.Primitives,
+  module Rattus.Strict,
+  Rattus(..),
+  (|*|),
+  (|**),
+  (<*>),
+  (<**))
+  where
+
+import Rattus.Plugin
+import Rattus.Strict
+import Rattus.Primitives
+
+
+import Prelude hiding ((<*>))
+
+-- all functions in this module are in Rattus 
+{-# ANN module Rattus #-}
+
+
+-- | Applicative operator for 'O'.
+(<*>) :: O (a -> b) -> O a -> O b
+f <*> x = delay (adv f (adv x))
+
+-- | Variant of '(<*>)' where the argument is of a stable type..
+(<**) :: Stable a => O (a -> b) -> a -> O b
+f <** x = delay (adv f x)
+
+-- | Applicative operator for 'Box'.
+(|*|) :: Box (a -> b) -> Box a -> Box b
+f |*| x = box (unbox f (unbox x))
+
+-- | Variant of '(|*|)' where the argument is of a stable type..
+(|**) :: Stable a => Box (a -> b) -> a -> Box b
+f |** x = box (unbox f x)
diff --git a/src/Rattus/Arrow.hs b/src/Rattus/Arrow.hs
new file mode 100644
--- /dev/null
+++ b/src/Rattus/Arrow.hs
@@ -0,0 +1,66 @@
+-- | This module provides a variant of the standard
+-- 'Control.Arrow.Arrow' type class with a different
+-- 'Control.Arrow.arr' method so that it can be implemented for signal
+-- functions in Rattus.
+
+module Rattus.Arrow where
+
+import Prelude hiding (id)
+import Rattus.Primitives
+import Control.Category
+
+-- | Variant of the standard 'Control.Arrow.Arrow' type class with a
+-- different 'Control.Arrow.arr' method so that it can be implemented
+-- for signal functions in Rattus.
+class Category a => Arrow a where
+    {-# MINIMAL arrBox, (first | (***)) #-}
+
+    -- | Lift a function to an arrow. It is here the definition of the
+    -- 'Arrow' class differs from the standard one. The function to be
+    -- lifted has to be boxed.
+    -- 
+    arrBox :: Box (b -> c) -> a b c
+
+    -- | Send the first component of the input through the argument
+    --   arrow, and copy the rest unchanged to the output.
+    first :: a b c -> a (b,d) (c,d)
+    first = (*** id)
+
+    -- | A mirror image of 'first'.
+    --
+    --   The default definition may be overridden with a more efficient
+    --   version if desired.
+    second :: a b c -> a (d,b) (d,c)
+    second = (id ***)
+
+    -- | Split the input between the two argument arrows and combine
+    --   their output.  Note that this is in general not a functor.
+    (***) :: a b c -> a b' c' -> a (b,b') (c,c')
+    f *** g = first f >>> arr swap >>> first g >>> arr swap
+      where swap ~(x,y) = (y,x)
+
+    -- | Fanout: send the input to both argument arrows and combine
+    --   their output.
+    --
+    --   The default definition may be overridden with a more efficient
+    --   version if desired.
+    (&&&) :: a b c -> a b c' -> a b (c,c')
+    f &&& g = arr (\b -> (b,b)) >>> f *** g
+
+
+-- | This combinator is subject to the same restrictions as the 'box'
+-- primitive of Rattus. That is,
+--
+-- >   Γ☐ ⊢ t :: b -> c
+-- > --------------------
+-- >  Γ ⊢ arr t :: a b c
+--
+-- where Γ☐ is obtained from Γ by removing ✓ and any variables @x ::
+-- 𝜏@, where 𝜏 is not a stable type.
+
+arr :: Arrow a => (b -> c) -> a b c
+arr f = arrBox (box f)
+
+-- | The identity arrow, which plays the role of 'return' in arrow notation.
+returnA :: Arrow a => a b b
+returnA = arrBox (box id)
diff --git a/src/Rattus/Event.hs b/src/Rattus/Event.hs
new file mode 100644
--- /dev/null
+++ b/src/Rattus/Event.hs
@@ -0,0 +1,107 @@
+{-# OPTIONS -fplugin=Rattus.Plugin #-}
+{-# LANGUAGE TypeOperators #-}
+
+-- | Programing with single shot events, i.e. events that may occur at
+-- most once.
+
+module Rattus.Event
+  ( map
+  , never
+  , switch
+  , switchTrans
+  , whenJust
+  , Event(..)
+  , await
+  , trigger
+  , triggerMap
+  )
+
+where
+
+import Rattus
+import Rattus.Stream hiding (map)
+
+import Prelude hiding ((<*>), map)
+
+
+-- | An event may either occur now or later.
+data Event a = Now !a | Wait (O (Event a))
+
+-- all functions in this module are in Rattus 
+{-# ANN module Rattus #-}
+
+-- | Apply a function to the value of the event (if it ever occurs).
+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)
+
+-- | An event that will never occur.
+never :: Event a
+never = Wait (delay never)
+
+
+-- | @switch s e@ will behave like @s@ until the event @e@ occurs with
+-- value @s'@, in which case it will behave as @s'@.
+switch :: Str a -> Event (Str a) -> Str a
+switch (x ::: xs) (Wait fas) = x ::: (delay switch <*> xs <*> fas)
+switch _xs        (Now ys)   = ys 
+
+-- | Turn a stream of 'Maybe''s into an event. The event will occur
+-- whenever the stream has a value of the form @Just' v@, and the
+-- event then has value @v@.
+firstJust :: Str (Maybe' a) -> Event a
+firstJust (Just' x ::: _) = Now x
+firstJust (Nothing' ::: xs) = Wait (delay firstJust <*> xs)
+
+-- | Turn a stream of 'Maybe''s into a stream of events. Each such
+-- event behaves as if created by 'firstJust'.
+whenJust :: Str (Maybe' a) -> Str (Event a)
+whenJust cur@(_ ::: xs) = firstJust cur ::: (delay whenJust <*> xs)
+
+
+-- | Like 'switch' but works on stream functions instead of
+-- streams. That is, @switchTrans s e@ will behave like @s@ until the
+-- event @e@ occurs with value @s'@, in which case it will behave as
+-- @s'@.
+switchTrans :: (Str a -> Str b) -> Event (Str a -> Str b) -> (Str a -> Str b)
+switchTrans f es as = switchTrans' (f as) es as
+
+-- | Helper function for 'switchTrans'.
+switchTrans' :: Str b -> Event (Str a -> Str b) -> Str a -> Str b
+switchTrans' (x ::: xs) (Wait fas) (_:::is) = x ::: (delay switchTrans' <*> xs <*> fas <*> is)
+switchTrans' _xs        (Now ys)   is = ys is
+
+-- | Helper function for 'await'.
+await1 :: Stable a => a -> Event b -> Event (a :* b)
+await1 a (Wait eb) = Wait (delay await1 <** a <*> eb)
+await1 a (Now  b)  = Now  (a :* b)
+
+-- | Helper function for 'await'.
+await2 :: Stable b => b -> Event a -> Event (a :* b)
+await2 b (Wait ea) = Wait (delay await2 <** b <*> ea)
+await2 b (Now  a)  = Now  (a :* b)
+
+-- | Synchronize two events. The resulting event occurs after both
+-- events have occurred (coinciding with whichever event occurred
+-- last.
+await :: (Stable a, Stable b) => Event a -> Event b -> Event(a :* b)
+await (Wait ea) (Wait eb)  = Wait (delay await <*> ea <*> eb)
+await (Now a)   eb         = await1 a eb
+await ea        (Now b)    = await2 b ea
+
+-- | Trigger an event as soon as the given predicate turns true on the
+-- given stream. The value of the event is the same as that of the
+-- stream at that time.
+trigger :: Box (a -> Bool) -> Str a -> Event a
+trigger p (x ::: xs)
+  | unbox p x  = Now x
+  | otherwise  = Wait (delay (trigger p) <*> xs)
+
+
+-- | Trigger an event as soon as the given function produces a 'Just''
+-- value.
+triggerMap :: Box (a -> Maybe' b) -> Str a -> Event b
+triggerMap f (x ::: xs) =
+  case unbox f x of
+    Just' y  -> Now y
+    Nothing' -> Wait (delay (triggerMap f) <*> xs)
diff --git a/src/Rattus/Events.hs b/src/Rattus/Events.hs
new file mode 100644
--- /dev/null
+++ b/src/Rattus/Events.hs
@@ -0,0 +1,71 @@
+{-# OPTIONS -fplugin=Rattus.Plugin #-}
+
+-- | Programing with many-shot events, i.e. events that may occur zero
+-- or more times.
+
+
+module Rattus.Events
+  ( map
+  , never
+  , switch
+  , switchTrans
+  , Events
+  , trigger
+  , triggerMap
+  )
+
+where
+
+import Rattus
+import Rattus.Stream hiding (map)
+import qualified Rattus.Stream as S
+
+import Prelude hiding ((<*>), map)
+
+-- | Events are simply streams of 'Maybe''s.
+type Events a = Str (Maybe' a)
+
+-- all functions in this module are in Rattus 
+{-# ANN module Rattus #-}
+
+-- | Apply a function to the values of the event (every time it occurs).
+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))
+
+-- | An event that will never occur.
+never :: Events a
+never = Nothing' ::: delay never
+
+-- | @switch s e@ will behave like @s@ but switches to @s'$ every time
+-- the event 'e' occurs with some value @s'@.
+switch :: Str a -> Events (Str a) -> Str a
+switch (x ::: xs) (Nothing' ::: fas) = x ::: delay (switch (adv xs)  (adv fas))
+switch  _xs       (Just' (a ::: as) ::: fas)   = a ::: (delay switch <*> as <*> fas)
+
+
+-- | Like 'switch' but works on stream functions instead of
+-- streams. That is, @switchTrans s e@ will behave like @s@ but
+-- switches to @s'$ every time the event 'e' occurs with some value
+-- @s'@.
+switchTrans :: (Str a -> Str b) -> Events (Str a -> Str b) -> (Str a -> Str b)
+switchTrans f es as = switchTrans' (f as) es as
+
+-- | Helper function for 'switchTrans'.
+switchTrans' :: Str b -> Events (Str a -> Str b) -> Str a -> Str b
+switchTrans' (b ::: bs) (Nothing' ::: fs) (_:::as) = b ::: (delay switchTrans' <*> bs <*> fs <*> as)
+switchTrans' _xs        (Just' f ::: fs)  as@(_:::as') = b' ::: (delay switchTrans' <*> bs' <*> fs <*> as')
+  where (b' ::: bs') = f as
+
+
+-- | Trigger an event as every time the given predicate turns true on
+-- the given stream. The value of the event is the same as that of the
+-- stream at that time.
+trigger :: Box (a -> Bool) -> Str a -> Events a
+trigger p (x ::: xs) = x' ::: (delay (trigger p) <*> xs)
+  where x' = if unbox p x then Just' x else Nothing'
+
+-- | Trigger an event every time the given function produces a 'Just''
+-- value.
+triggerMap :: Box (a -> Maybe' b) -> Str a -> Events b
+triggerMap = S.map
diff --git a/src/Rattus/Plugin.hs b/src/Rattus/Plugin.hs
new file mode 100644
--- /dev/null
+++ b/src/Rattus/Plugin.hs
@@ -0,0 +1,117 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+
+
+-- | The plugin to make it all work.
+
+module Rattus.Plugin (plugin, Rattus(..)) where
+import Rattus.Plugin.StableSolver
+import Rattus.Plugin.ScopeCheck
+import Rattus.Plugin.Strictify
+import Rattus.Plugin.Utils
+
+import Prelude hiding ((<>))
+import GhcPlugins
+
+import Control.Monad
+import Data.Maybe
+import Data.Data hiding (tyConName)
+
+import System.Exit
+
+
+-- | Use this type to mark a Haskell function definition as a Rattus
+-- function:
+--
+-- > {-# ANN myFunction Rattus #-}
+-- 
+-- Or mark a whole module as consisting of Rattus functions only:
+--
+-- > {-# ANN module Rattus #-}
+--
+-- If you use the latter option, you can mark exceptions
+-- (i.e. functions that should be treated as ordinary Haskell function
+-- definitions) as follows:
+--
+-- > {-# ANN myFunction NotRattus #-}
+
+data Rattus = Rattus | NotRattus 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
+-- following pragma in each source file:
+-- 
+-- > {-# OPTIONS -fplugin=Rattus.Plugin #-}
+plugin :: Plugin
+plugin = defaultPlugin {
+  installCoreToDos = install,
+  tcPlugin = tcStable
+  }
+
+
+install :: [CommandLineOption] -> [CoreToDo] -> CoreM [CoreToDo]
+install _ todo = do
+  return (CoreDoPluginPass "Rattus" transformProgram : todo)
+
+
+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 }
+
+
+transform :: ModGuts -> CoreBind -> CoreM (Maybe CoreBind)
+transform guts b@(Rec bs) = do
+  tr <- liftM or (mapM (shouldTransform guts . fst) bs)
+  if tr then
+    case bs of
+      [(v,e)] -> do
+          --putMsg (text "check Rattus definition: " <> ppr v)
+          --putMsg (ppr e)
+          valid <- checkExpr (emptyCtx (Just v)) e
+          if valid then do
+            e' <- strictifyExpr e
+            return (Just $ Rec [(v,e')])
+          else return Nothing
+      (v,_):_ -> do
+        printMessage SevError (nameSrcSpan (varName v)) (
+          text "mutual recursive definitions not supported in Rattus")
+        return Nothing
+      _ -> return (Just $ Rec [])
+  else return (Just b)
+transform guts b@(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)
+
+getModuleAnnotations :: Data a => ModGuts -> [a]
+getModuleAnnotations guts = anns'
+  where anns = filter (\a-> case ann_target a of
+                         ModuleTarget m -> m == (mg_module guts)
+                         _ -> False) (mg_anns guts)
+        anns' = mapMaybe (fromSerialized deserializeWithData . ann_value) anns
+  
+
+
+
+shouldTransform :: ModGuts -> CoreBndr -> CoreM Bool
+shouldTransform guts bndr = do
+  l <- annotationsOn guts bndr :: CoreM [Rattus]
+  return (Rattus `elem` l && not (NotRattus `elem` l) && userFunction bndr)
+
+annotationsOn :: (Data a) => ModGuts -> CoreBndr -> CoreM [a]
+annotationsOn guts bndr = do
+  anns <- getAnnotations deserializeWithData guts
+  return $
+    lookupWithDefaultUFM anns [] (varUnique bndr) ++
+    getModuleAnnotations guts
+
diff --git a/src/Rattus/Plugin/ScopeCheck.hs b/src/Rattus/Plugin/ScopeCheck.hs
new file mode 100644
--- /dev/null
+++ b/src/Rattus/Plugin/ScopeCheck.hs
@@ -0,0 +1,250 @@
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE OverloadedStrings #-}
+module Rattus.Plugin.ScopeCheck (checkExpr, emptyCtx) where
+
+import Rattus.Plugin.Utils 
+
+import Prelude hiding ((<>))
+import GhcPlugins
+import Control.Monad
+import Data.Set (Set)
+import qualified Data.Set as Set
+import Data.Map (Map)
+import qualified Data.Map as Map
+import Data.Maybe
+
+type LCtx = Set Var
+type Hidden = Set Var
+
+data Prim = Prim1 Prim1 | Prim2 Prim2
+data Prim1 = Delay | Adv | Box | Unbox | Arr
+data Prim2 = DApp | BApp | DAppP | BAppP
+
+instance Outputable Prim1 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 = Var
+
+data Ctx = Ctx
+  { current :: LCtx,
+    hidden :: Hidden,
+    earlier :: Maybe LCtx,
+    srcLoc :: SrcSpan,
+    recDef :: Maybe RecDef,
+    hiddenRecs :: Set Var,
+    stableTypes :: Set Var,
+    primAlias :: Map Var Prim,
+    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)
+   ]
+
+
+isPrim :: Ctx -> Var -> Maybe Prim
+isPrim c v
+  | Just p <- Map.lookup v (primAlias c) = Just p
+  | otherwise = do
+  (name,mod) <- getNameModule v
+  if isRattModule mod then Map.lookup name primMap
+  else Nothing
+
+
+
+stabilize :: Ctx -> Ctx
+stabilize c = c
+  {current = Set.empty,
+   earlier = Nothing,
+   hidden = maybe (current c) (Set.union (current c)) (earlier c),
+   recDef = Nothing,
+   stabilized = True}
+
+
+data Scope = Hidden | Visible | ImplUnboxed
+
+getScope  :: Ctx -> Var -> Scope
+getScope Ctx{recDef = Just v, earlier = Just _} v'
+  -- recursive call under delay
+  | v' == v = Visible
+getScope Ctx{hiddenRecs = h} v
+  -- recursive call that is out of scope
+  | (Set.member v h) = Hidden
+getScope c v =
+  if Set.member v (hidden c) || maybe False (Set.member v) (earlier c)
+  then if (isStable (stableTypes c)) (varType v) then Visible
+       else Hidden
+  else if Set.member v (current c) then Visible
+       else if isTemporal (varType v) && isJust (earlier c) && userFunction v
+            then ImplUnboxed
+            else Visible
+
+
+
+pickFirst :: SrcSpan -> SrcSpan -> SrcSpan
+pickFirst s@RealSrcSpan{} _ = s
+pickFirst _ s = s
+
+printMessage' :: Severity -> Ctx -> Var -> SDoc -> CoreM ()
+printMessage' sev cxt var doc =
+  printMessage sev (pickFirst (srcLoc cxt) (nameSrcSpan (varName var))) doc
+
+printMessageCheck :: Severity -> Ctx -> Var -> SDoc -> CoreM Bool
+printMessageCheck sev cxt var doc = printMessage' sev cxt var doc >>
+  case sev of
+    SevError -> return False
+    _ -> return True
+
+
+
+emptyCtx :: Maybe Var -> Ctx
+emptyCtx mvar=
+  Ctx { current =  Set.empty,
+        earlier = Nothing,
+        hidden = Set.empty,
+        srcLoc = UnhelpfulSpan "<no location info>",
+        recDef = mvar,
+        hiddenRecs = maybe Set.empty Set.singleton mvar,
+        primAlias = Map.empty,
+        stableTypes = Set.empty,
+        stabilized = isJust mvar}
+
+
+isPrimExpr :: Ctx -> Expr Var -> Maybe (Prim,Var)
+isPrimExpr c (App e (Type _)) = isPrimExpr c e
+isPrimExpr c (App e e') | not $ tcIsLiftedTypeKind $ typeKind $ exprType e' = isPrimExpr c e
+isPrimExpr c (Var v) = fmap (,v) (isPrim c v)
+isPrimExpr c (Tick _ e) = isPrimExpr c e
+isPrimExpr c (Lam v e)
+  | isTyVar v || (not $ tcIsLiftedTypeKind $ typeKind $ varType v) = isPrimExpr c e
+isPrimExpr _ _ = Nothing
+
+
+isStableConstr :: Type -> CoreM (Maybe Var)
+isStableConstr t = 
+  case splitTyConApp_maybe t of
+    Just (con,[args]) ->
+      case getNameModule con of
+        Just (name, mod) ->
+          if isRattModule mod && name == "Stable"
+          then return (getTyVar_maybe args)
+          else return Nothing
+        _ -> return Nothing                           
+    _ ->  return Nothing
+
+checkExpr :: Ctx -> Expr Var -> CoreM Bool
+checkExpr c (App e e') | isType e' || (not $ tcIsLiftedTypeKind $ typeKind $ exprType e')
+  = 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
+      Box -> do
+        when (stabilized c)  (printMessage' SevWarning c v
+          (text "box nested inside another box or recursive definition can cause time leaks"))
+        checkExpr (stabilize c) e2
+      Arr -> do
+        when (stabilized c)  (printMessage' SevWarning c v
+          (text "arr nested inside a box or recursive definition can cause time leaks"))
+        checkExpr (stabilize c) e2
+      Unbox -> checkExpr c e2
+      Delay -> case earl of
+        Just _ -> printMessageCheck SevError c v (text "cannot delay more than once")
+        Nothing -> checkExpr c{current = Set.empty, earlier = Just cur} e2
+      Adv -> case earl of
+        Just er -> checkExpr c{earlier = Nothing, current = er,
+                               hidden = hid `Set.union` cur} e2
+        Nothing -> printMessageCheck SevError c v (text "can only advance under delay")
+    _ -> liftM2 (&&) (checkExpr c e1)  (checkExpr c e2)
+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 "lambdas may not appear under delay")
+checkExpr c (Lam v e)
+  | isTyVar v || (not $ tcIsLiftedTypeKind $ typeKind $ varType v) = do
+      is <- isStableConstr (varType v)
+      let c' = case is of
+            Nothing -> c
+            Just t -> c{stableTypes = Set.insert t (stableTypes c)}
+      checkExpr c' e
+  | otherwise = checkExpr (addVars [v] c) e
+checkExpr _ (Type _)  = return True
+checkExpr _ (Lit _)  = return True
+checkExpr _ (Coercion _)  = return True
+checkExpr c (Tick (SourceNote span _name) e) =
+  checkExpr c{srcLoc = RealSrcSpan span} e
+checkExpr c (Tick _ e) = checkExpr c e
+checkExpr c (Cast e _) = checkExpr c e
+checkExpr c (Let (NonRec v e1) e2) =
+  case isPrimExpr c e1 of
+    Just (p,_) -> (checkExpr (c{primAlias = Map.insert v p (primAlias c)}) e2)
+    Nothing -> liftM2 (&&) (checkExpr c e1)  (checkExpr (addVars [v] c) e2)
+checkExpr _ (Let (Rec ([])) _) = return True
+checkExpr c (Let (Rec ([(v,e1)])) e2) = do
+    when (stabilized c) (printMessage' SevWarning c v
+          (text "recursive definition nested inside a box or annother recursive definition can cause time leaks"))
+    r1 <- checkExpr c' e1
+    r2 <- checkExpr (addVars [v] c) e2
+    return (r1 && r2)
+  where c' = c {current = Set.empty,
+                earlier = Nothing,
+                hidden = Set.insert v (maybe (current c) (Set.union (current c)) (earlier c)),
+                hiddenRecs = Set.insert v (hiddenRecs c),
+                recDef = Just v,
+                stabilized = True}
+checkExpr c (Let (Rec ((v,_):_)) _) =
+          printMessageCheck SevError c v (text "mutual recursive definitions not supported in Rattus")
+checkExpr c@Ctx{earlier = earl}  (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
+      _ -> case getScope c v of
+             Hidden -> printMessageCheck SevError c v (ppr v <> text " is out of scope")
+             Visible -> return True
+             ImplUnboxed -> printMessageCheck SevWarning c v
+                (ppr v <> text " is an external temporal function used under delay, which may cause time leaks")
+
+  | otherwise = return True
+
+
+
+
+
+addVars :: [Var] -> Ctx -> Ctx
+addVars v c = c{current = Set.fromList v `Set.union` current c }
+
diff --git a/src/Rattus/Plugin/StableSolver.hs b/src/Rattus/Plugin/StableSolver.hs
new file mode 100644
--- /dev/null
+++ b/src/Rattus/Plugin/StableSolver.hs
@@ -0,0 +1,63 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE CPP #-}
+
+module Rattus.Plugin.StableSolver (tcStable) where
+
+import Rattus.Plugin.Utils
+
+import Prelude hiding ((<>))
+import GhcPlugins
+  (Type, Var, CommandLineOption,tyConSingleDataCon,
+   mkCoreConApps,getTyVar_maybe)
+import CoreSyn
+import TcEvidence
+import Class
+
+#if __GLASGOW_HASKELL__ >= 810
+import Constraint
+#endif
+
+import Data.Set (Set)
+import qualified Data.Set as Set
+
+
+import TcRnTypes
+
+
+
+tcStable :: [CommandLineOption] -> Maybe TcPlugin
+tcStable _ = Just $ TcPlugin
+  { tcPluginInit = return ()
+  , tcPluginSolve = \ () -> stableSolver
+  , tcPluginStop = \ () -> return ()
+  }
+
+wrap :: Class -> Type -> EvTerm
+wrap cls ty = EvExpr appDc
+  where
+    tyCon = classTyCon cls
+    dc = tyConSingleDataCon tyCon
+    appDc = mkCoreConApps dc [Type ty]
+
+solveStable :: Set Var -> (Type, (Ct,Class)) -> Maybe (EvTerm, Ct)
+solveStable c (ty,(ct,cl))
+  | isStable c ty = Just (wrap cl ty, ct)
+  | otherwise = Nothing
+
+stableSolver :: [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult
+stableSolver given _derived wanted = do
+  let chSt = concatMap filterCt wanted
+  let haveSt = Set.fromList $ concatMap (filterTypeVar . fst) $ concatMap filterCt given
+  case mapM (solveStable haveSt) chSt of
+    Just evs -> return $ TcPluginOk evs []
+    Nothing -> return $ TcPluginOk [] []
+
+  where filterCt ct@(CDictCan {cc_class = cl, cc_tyargs = [ty]})
+          = case getNameModule cl of
+              Just (name,mod)
+                | isRattModule mod && name == "Stable" -> [(ty,(ct,cl))]
+              _ -> []
+        filterCt _ = []
+        filterTypeVar ty = case getTyVar_maybe ty of
+          Just v -> [v]
+          Nothing -> []
diff --git a/src/Rattus/Plugin/Strictify.hs b/src/Rattus/Plugin/Strictify.hs
new file mode 100644
--- /dev/null
+++ b/src/Rattus/Plugin/Strictify.hs
@@ -0,0 +1,72 @@
+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
+  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
+  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
+  return (Cast e' c)
+strictifyExpr (Tick t e) = do
+  e' <- strictifyExpr 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))]
+  | otherwise = do
+  e1' <- strictifyExpr e1
+  e2' <- strictifyExpr e2
+  return (App e1' e2')
+strictifyExpr e = return e
+
+
+
+isDelayApp (App e _) = isDelayApp e
+isDelayApp (Cast e _) = isDelayApp e
+isDelayApp (Tick _ e) = isDelayApp e
+isDelayApp (Var v) = isDelayVar v
+isDelayApp _ = False
+
+
+
+
+isDelayVar :: Var -> Bool
+isDelayVar v = maybe False id $ do
+  let name = varName v
+  mod <- nameModule_maybe name
+  let occ = getOccString name
+  return ((occ == "Delay" || occ == "delay") || (occ == "Box" || occ == "delay")
+          && ((moduleNameString (moduleName mod) == "Rattus.Internal") ||
+          moduleNameString (moduleName mod) == "Rattus.Primitives"))
+
+isCase Case{} = True
+isCase (Tick _ e) = isCase e
+isCase (Cast e _) = isCase e
+isCase Lam {} = True
+isCase e = isType e
+
+isTophandler (App e1 e2) = isTophandler e1 || isTophandler e2
+isTophandler (Cast e _) = isTophandler e
+isTophandler (Tick _ e) = isTophandler e
+isTophandler e = showSDocUnsafe (ppr e) == "GHC.TopHandler.runMainIO"
+
diff --git a/src/Rattus/Plugin/Utils.hs b/src/Rattus/Plugin/Utils.hs
new file mode 100644
--- /dev/null
+++ b/src/Rattus/Plugin/Utils.hs
@@ -0,0 +1,180 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+module Rattus.Plugin.Utils (
+  printMessage,
+  Severity(..),
+  isRattModule,
+  isGhcModule,
+  getNameModule,
+  isStable,
+  isTemporal,
+  userFunction,
+  isType)
+  where
+
+import ErrUtils
+import Prelude hiding ((<>))
+import GhcPlugins
+import Data.Set (Set)
+import qualified Data.Set as Set
+import Data.Char
+
+isType Type {} = True
+isType (App e _) = isType e
+isType (Cast e _) = isType e
+isType (Tick _ e) = isType e
+isType _ = False
+
+
+
+-- printMessage :: Severity -> SDoc -> CoreM ()
+-- printMessage sev doc =
+--   case sev of
+--     Error -> errorMsg doc
+--     Warning -> warnMsg doc
+
+
+-- printMessageV :: Severity -> Var -> SDoc -> CoreM ()
+-- printMessageV sev var doc =
+--   let loc = nameSrcLoc (varName var)
+--       doc' = ppr loc <> text ": " <> doc
+--   in case sev of
+--     Error -> errorMsg doc'
+--     Warning -> warnMsg doc'
+
+
+printMessage :: Severity -> SrcSpan -> SDoc -> CoreM ()
+printMessage sev loc doc = do
+  dflags <- getDynFlags
+  unqual <- getPrintUnqualified
+  let sty = case sev of
+                     SevError   -> err_sty
+                     SevWarning -> err_sty
+                     SevDump    -> dump_sty
+                     _          -> user_sty
+      err_sty  = mkErrStyle dflags unqual
+      user_sty = mkUserStyle dflags unqual AllTheWay
+      dump_sty = mkDumpStyle dflags unqual
+  liftIO $ putLogMsg dflags NoReason sev loc sty doc
+
+
+
+rattModules :: Set FastString
+rattModules = Set.fromList ["Rattus.Internal","Rattus.Primitives"
+                           ,"Rattus.Stable", "Rattus.Arrow"]
+
+isRattModule :: FastString -> Bool
+isRattModule = (`Set.member` rattModules)
+
+isGhcModule :: FastString -> Bool
+isGhcModule = (== "GHC.Types")
+
+
+getNameModule :: NamedThing a => a -> Maybe (FastString, FastString)
+getNameModule v = do
+  let name = getName v
+  mod <- nameModule_maybe name
+  return (getOccFS name,moduleNameFS (moduleName mod))
+
+
+-- | The set of stable built-in types.
+ghcStableTypes :: Set FastString
+ghcStableTypes = Set.fromList ["Int","Bool","Float","Double","Char"]
+
+
+newtype TypeCmp = TC Type
+
+instance Eq TypeCmp where
+  (TC t1) == (TC t2) = eqType t1 t2
+
+instance Ord TypeCmp where
+  compare (TC t1) (TC t2) = nonDetCmpType t1 t2
+
+isTemporal :: Type -> Bool
+isTemporal t = isTemporalRec 0 Set.empty t
+
+
+isTemporalRec :: Int -> Set TypeCmp -> Type -> Bool
+isTemporalRec d _ _ | d == 100 = False
+isTemporalRec _ pr t | Set.member (TC t) pr = False
+isTemporalRec d pr t = do
+  let pr' = Set.insert (TC t) pr
+  case splitTyConApp_maybe t of
+    Nothing -> False
+    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
+          | isFunTyCon con -> or (map (isTemporalRec (d+1) pr') args)
+          | isAlgTyCon con -> 
+            case algTyConRhs con of
+              DataTyCon {data_cons = cons} -> or (map check cons)
+                where check con = case dataConInstSig con args of
+                        (_, _,tys) -> or (map (isTemporalRec (d+1) pr') tys)
+              _ -> or (map (isTemporalRec (d+1) pr') args)
+        _ -> False
+
+
+-- | Check whether the given type is stable. This check may use
+-- 'Stable' constraints from the context.
+
+isStable :: Set Var -> Type -> Bool
+isStable c t = isStableRec c 0 Set.empty t
+
+-- | Check whether the given type is stable. This check may use
+-- 'Stable' constraints from the context.
+
+isStableRec :: Set Var -> 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.
+isStableRec _ d _ _ | d == 100 = True
+isStableRec _ _ pr t | Set.member (TC t) pr = True
+isStableRec c d pr t = do
+  let pr' = Set.insert (TC t) pr
+  case splitTyConApp_maybe t of
+    Nothing -> case getTyVar_maybe t of
+      Just v -> -- if it's a type variable, check the context
+        v `Set.member` c
+      Nothing -> False
+    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" -> 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 ->
+             isStableRec c (d+1) pr' (substTy (extendTvSubstList emptySubst subst) ty) -}
+          | isAlgTyCon con -> 
+            case algTyConRhs con of
+              DataTyCon {data_cons = cons, is_enum = enum}
+                | enum -> True
+                | and $ concatMap (map isSrcStrict'
+                                   . dataConSrcBangs) $ cons ->
+                  and  (map check cons)
+                | otherwise -> False
+                where check con = case dataConInstSig con args of
+                        (_, _,tys) -> and (map (isStableRec c (d+1) pr') tys)
+              TupleTyCon {} -> null args
+              _ -> False
+        _ -> False
+
+
+          
+isSrcStrict' (HsSrcBang _ _ SrcStrict) = True
+isSrcStrict' _ = False
+
+
+userFunction :: Var -> Bool
+userFunction v =
+  case getOccString (getName v) of
+    (c : _)
+      | isUpper c || c == '$' || c == ':' -> False
+      | otherwise -> True
+    _ -> False
diff --git a/src/Rattus/Primitives.hs b/src/Rattus/Primitives.hs
new file mode 100644
--- /dev/null
+++ b/src/Rattus/Primitives.hs
@@ -0,0 +1,88 @@
+-- | The language primitives of Rattus. Note that the Rattus types
+--  'delay', 'adv', and 'box' are more restrictive that the Haskell
+--  types that are indicated. The more stricter Rattus typing rules
+--  for these primitives are given. To ensure that your program
+--  adheres to these stricter typing rules, use the plugin in
+--  "Rattus.Plugin" so that GHC will check these stricter typing
+--  rules.
+
+module Rattus.Primitives
+  (O
+  ,Box
+  ,delay
+  ,adv
+  ,box
+  ,unbox
+  ,Stable
+  ) 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@.
+--
+-- For example, these types are stable: @Int@, @Box (a -> b)@, @Box (O
+-- Int)@, @Box (Str a -> Str b)@.
+--
+-- But these types are not stable: @[Int]@ (because the list type ist
+-- not strict), @Int -> Int@, (function type is not stable), @O
+-- Delay@, @Str Int@.
+class StableInternal a => 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
+-- 'delay' and 'adv' to construct and consume 'O'-types.
+data O a = Delay a
+
+-- | The "stable" type modality. A value of type @Box a@ is a
+-- time-independent computation that produces a value of type @a@.
+-- Use 'box' and 'unbox' to construct and consume 'Box'-types.
+data Box a = Box a
+
+-- | This is the constructor for the "later" modality 'O':
+--
+-- >     Γ ✓ ⊢ t :: 𝜏
+-- > --------------------
+-- >  Γ ⊢ delay t :: O 𝜏
+--
+delay :: a -> O a
+delay x = Delay x
+
+
+-- | This is the eliminator for the "later" modality 'O':
+--
+-- >     Γ ⊢ t :: O 𝜏
+-- > ---------------------
+-- >  Γ ✓ Γ' ⊢ adv t :: 𝜏
+--
+adv :: O a -> a
+adv (Delay x) = x
+
+
+-- | This is the contructor for the "stable" modality 'Box':
+--
+-- >     Γ☐ ⊢ t :: 𝜏
+-- > --------------------
+-- >  Γ ⊢ box t :: Box 𝜏
+--
+-- where Γ☐ is obtained from Γ by removing ✓ and any variables @x ::
+-- 𝜏@, where 𝜏 is not a stable type.
+
+
+box :: a -> Box a
+box x = Box x
+
+
+
+-- | This is the eliminator for the "stable" modality  'Box':
+--
+-- >   Γ ⊢ t :: Box 𝜏
+-- > ------------------
+-- >  Γ ⊢ unbox t :: 𝜏
+
+unbox :: Box a -> a
+unbox (Box d) = d
diff --git a/src/Rattus/Stream.hs b/src/Rattus/Stream.hs
new file mode 100644
--- /dev/null
+++ b/src/Rattus/Stream.hs
@@ -0,0 +1,131 @@
+{-# OPTIONS -fplugin=Rattus.Plugin #-}
+{-# LANGUAGE TypeOperators #-}
+
+-- | Programming with streams.
+
+module Rattus.Stream
+  ( map
+  , hd
+  , tl
+  , const
+  , constBox
+  , shift
+  , shiftMany
+  , scan
+  , scanMap
+  , scanMap2
+  , Str(..)
+  , zipWith
+  , zip
+  , unfold
+  , filter
+  , integral
+  )
+
+where
+
+import Rattus
+import Prelude hiding (map, const, zipWith, zip, filter)
+
+import Data.VectorSpace
+
+-- | @Str a@ is a stream of values of type @a@.
+data Str a = ! a ::: (O (Str a))
+
+-- all functions in this module are in Rattus 
+{-# ANN module Rattus #-}
+
+-- | Get the first element (= head) of a stream.
+hd :: Str a -> a
+hd (x ::: _) = x
+
+
+-- | Get the tail of a stream, i.e. the remainder after removing the
+-- first element.
+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
+map f (x ::: xs) = unbox f x ::: delay (map f (adv xs))
+
+-- | Construct a stream that has the same given value at each step.
+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.
+constBox :: Box a -> Str a
+constBox a = unbox a ::: delay (constBox a)
+
+-- | Construct a stream by repeatedly applying a function to a given
+-- start element. That is, @unfold (box f) x@ will produce the stream
+-- @x ::: f x ::: f (f x) ::: ...@
+unfold :: Stable a => Box (a -> a) -> a -> Str a
+unfold f x = x ::: delay (unfold f (unbox f x))
+
+-- | Similar to Haskell's 'scanl'.
+--
+-- > 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@.
+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
+
+-- | 'scanMap' is a composition of 'map' and 'scan':
+--
+-- > scanMap f g x === map g . scan f x
+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) =
+    unbox p acc' ::: delay (scanMap2 f p acc' (adv as1) (adv as2))
+  where acc' = unbox f acc a1 a2
+
+-- | Similar to 'Prelude.zipWith' on Haskell lists.
+zipWith :: Box(a -> b -> c) -> Str a -> Str b -> Str c
+zipWith f (a ::: as) (b ::: bs) = unbox f a b ::: delay (zipWith f (adv as) (adv bs))
+
+-- | Similar to 'Prelude.zip' on Haskell lists.
+zip :: Str a -> Str b -> Str (a:*b)
+zip (a ::: as) (b ::: bs) =  (a :* b) ::: delay (zip (adv as) (adv bs))
+
+
+-- | Filter out elements from a stream according to a predicate.
+filter :: Box(a -> Bool) -> Str a -> Str(Maybe' a)
+filter p = map (box (\a -> if unbox p a then Just' a else Nothing'))
+
+{-| Given a value a and a stream as, this function produces a stream
+  that behaves like -}
+shift :: Stable a => a -> Str a -> Str a
+shift a (x ::: xs) = a ::: delay (shift x (adv xs))
+
+
+{-| Given a list @[a1, ..., an]@ of elements and a stream @xs@ this
+  function constructs a stream that starts with the elements @a1, ...,
+  an@, and then proceeds as @xs@. In particular, this means that the
+  ith element of the original stream @xs@ is the (i+n)th element of
+  the new stream. In other words @shiftMany@ behaves like reapeatedly
+  applying @shift@ for each element in the list. -}
+shiftMany :: Stable a => List a -> Str a -> Str a
+shiftMany l xs = run l Nil xs where
+  run :: Stable a => List a -> List a -> Str a -> Str a
+  run (b :! bs) buf (x ::: xs) = b ::: delay (run bs (x :! buf) (adv xs))
+  run Nil buf (x ::: xs) =
+    case reverse' buf of
+      b :! bs -> b ::: delay (run bs (x :! Nil) (adv xs))
+      Nil -> x ::: xs
+    
+-- | Calculates an approximation of an integral of the stream of type
+-- @Str a@ (the y-axis), where the stream of type @Str s@ provides the
+-- distance between measurements (i.e. the distance along the y axis).
+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)
diff --git a/src/Rattus/Strict.hs b/src/Rattus/Strict.hs
new file mode 100644
--- /dev/null
+++ b/src/Rattus/Strict.hs
@@ -0,0 +1,91 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+-- | This module contains strict versions of some standard data
+-- structures.
+
+
+
+module Rattus.Strict
+  ( List(..),
+    reverse',
+    (:*)(..),
+    Maybe'(..),
+   fst',
+   snd',
+  )where
+
+import Data.VectorSpace
+
+infixr 2 :*
+
+-- | Strict list type.
+data List a = Nil | !a :! !(List a)
+
+-- | Reverse a list.
+reverse' :: List a -> List a
+reverse' l =  rev l Nil
+  where
+    rev Nil     a = a
+    rev (x:!xs) a = rev xs (x:!a)
+
+instance Foldable List where
+  
+  foldMap f = run where
+    run Nil = mempty
+    run (x :! xs) = f x <> run xs
+  foldr f = run where
+    run b Nil = b
+    run b (a :! as) = (run $! (f a b)) as
+  foldl f = run where
+    run a Nil = a
+    run a (b :! bs) = (run $! (f a b)) bs
+  elem a = run where
+    run Nil = False
+    run (x :! xs)
+      | a == x = True
+      | otherwise = run xs
+    
+  
+instance Functor List where
+  fmap f = run where
+    run Nil = Nil
+    run (x :! xs) = f x :! run xs
+
+
+-- | Strict variant of 'Maybe'.
+data Maybe' a = Just' ! a | Nothing'
+
+-- | Strict pair type.
+data a :* b = !a :* !b
+
+-- | First projection function.
+fst' :: (a :* b) -> a
+fst' (a:*_) = a
+
+-- | Second projection function.
+snd' :: (a :* b) -> b
+snd' (_:*b) = b
+
+
+instance RealFloat a => VectorSpace (a :* a) a where
+    zeroVector = 0 :* 0
+
+    a *^ (x :* y) = (a * x) :* (a * y)
+
+    (x :* y) ^/ a = (x / a) :* (y / a)
+
+    negateVector (x :* y) = (-x) :* (-y)
+
+    (x1 :* y1) ^+^ (x2 :* y2) = (x1 + x2) :* (y1 + y2)
+
+    (x1 :* y1) ^-^ (x2 :* y2) = (x1 - x2) :* (y1 - y2)
+
+    (x1 :* y1) `dot` (x2 :* y2) = x1 * x2 + y1 * y2
+
+instance Functor ((:*) a) where
+  fmap f (x:*y) = (x :* f y)
+  
+instance (Show a, Show b) => Show (a:*b) where
+  show (a :* b) = "(" ++ show a ++ " :* " ++ show b ++ ")"
diff --git a/src/Rattus/ToHaskell.hs b/src/Rattus/ToHaskell.hs
new file mode 100644
--- /dev/null
+++ b/src/Rattus/ToHaskell.hs
@@ -0,0 +1,55 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+
+-- | Helper functions to convert streams and signal functions from
+-- Rattus into Haskell.
+
+module Rattus.ToHaskell
+  (runTransducer,
+   runSF,
+   fromStr,
+   toStr,
+   Trans(..)
+  ) where
+
+import System.IO.Unsafe
+import Data.IORef
+import Rattus.Primitives
+import Rattus.Stream
+import Rattus.Yampa
+
+
+-- | A state machine that takes inputs of type @a@ and produces output
+-- of type @b@. In addition to the ouptut of type @b@ the underlying
+-- function also returns the new state of the state machine.
+data Trans a b = Trans (a -> (b, Trans a b))
+
+-- | Turn a stream function into a state machine.
+runTransducer :: (Str a -> Str b) -> Trans a b
+runTransducer tr = Trans run
+  where run a = unsafePerformIO $ do
+          asR <- newIORef undefined
+          as <- unsafeInterleaveIO $ readIORef asR
+          let b ::: bs = tr (a ::: delay as)
+          return (b, Trans (run' (adv bs) asR))
+        run' bs asR a = unsafePerformIO $ do
+          asR' <- newIORef undefined
+          as' <- unsafeInterleaveIO $ readIORef asR'
+          writeIORef asR (a ::: delay as')
+          let b ::: bs' = bs
+          return (b, Trans (run' (adv bs') asR'))
+
+-- | 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)))
+
+
+-- | Turns a lazy infinite list into a stream.
+toStr :: [a] -> Str a
+toStr (x : xs) = x ::: delay (toStr xs)
+toStr _ = error "runRatt: input terminated"
+
+-- | Turns a stream into a lazy infinite list.
+fromStr :: Str a -> [a]
+fromStr (x ::: xs) = x : fromStr (adv xs)
diff --git a/src/Rattus/Yampa.hs b/src/Rattus/Yampa.hs
new file mode 100644
--- /dev/null
+++ b/src/Rattus/Yampa.hs
@@ -0,0 +1,207 @@
+{-# OPTIONS -fplugin=Rattus.Plugin #-}
+{-# LANGUAGE Arrows #-}
+{-# LANGUAGE RebindableSyntax #-}
+
+-- | A simply Yampa-like library for signal functions.
+
+module Rattus.Yampa (
+  SF,
+  identity,
+  compose,
+  switch,
+  rSwitch,
+  constant,
+  loopPre,
+  stepSF,
+  initially,
+  integral,
+  (-->),
+  (-:>),
+  (>--),
+  (-=>),
+  (>=-),
+  (^>>),
+  (>>^),
+  (<<^),
+  (^<<),
+  module Rattus.Arrow, (>>>)) where
+
+import Rattus.Primitives
+import Rattus.Plugin
+import Rattus.Strict
+
+import GHC.Float
+import Control.Category
+import Rattus.Arrow
+import Prelude hiding (id)
+
+import Data.VectorSpace
+
+-- all functions in this module are in Rattus 
+{-# ANN module Rattus #-}
+
+type DTime = Double 
+
+-- | 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)}
+
+-- | The identity signal function that does nothing.
+identity :: SF a a
+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)
+
+-- | 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')
+
+-- | @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 sf) f = SF sf'
+  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)
+
+-- | @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 sf) = SF sf'
+  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)
+
+-- | Constant signal function.
+constant :: Stable b => b -> SF a b
+constant x = run
+  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)
+
+-- | Insert a sample in the output, and from that point on, behave
+-- like the given signal function.
+--
+-- Note: The type of -:> is different from Yampa's: The second
+-- argument must be delayed (or boxed).
+(-:>) :: b -> O (SF a b) -> SF a b
+b -:> sf = SF sf'
+  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.
+(>--) :: a -> SF a b -> SF a b
+a >-- (SF sf) = SF sf'
+  where sf' d _a = sf d a
+
+
+-- | Apply a function to the first output value at time
+-- 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)
+                     
+-- | Apply a function to the first input value at time
+-- zero.
+(>=-) :: (a -> a) -> SF a b -> SF a b
+f >=- (SF sf) = SF sf'
+  where sf' d a = sf d (f a)
+
+-- | Override initial value of input signal.
+
+initially :: a -> SF a a
+initially = (--> identity)
+
+-- | Lift a function to a signal function (applied pointwise).
+-- 
+-- Note: The type of is different from Yampa's: The function argument
+-- must be boxed.
+arrPrim :: Box (a -> b) -> SF a b
+arrPrim f = run where
+  run = SF (\ _d a -> (delay run, unbox f a ))
+
+
+-- | 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))
+
+-- | 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))
+
+
+-- | 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))
+
+-- | 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))
+
+instance Category SF where
+  id = identity
+  (.) = compose
+
+instance Arrow SF where
+  arrBox = arrPrim
+  first = firstPrim
+  second = secondPrim
+  (***) = parSplitPrim
+  (&&&) = parFanOutPrim
+
+
+-- | Loop with an initial value for the signal being fed back.
+-- 
+-- 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 sf) = SF sf'
+  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.
+(^>>) :: Arrow a => Box (b -> c) -> a c d -> a b d
+f ^>> a = arrBox f >>> a
+
+-- | Postcomposition with a pure function.
+(>>^) :: Arrow a => a b c -> Box (c -> d) -> a b d
+a >>^ f = a >>> arrBox f
+
+-- | Precomposition with a pure function (right-to-left variant).
+(<<^) :: Arrow a => a c d -> Box (b -> c) -> a b d
+a <<^ f = a <<< arrBox f
+
+-- | Postcomposition with a pure function (right-to-left variant).
+(^<<) :: Arrow a => Box (c -> d) -> a b c -> a b d
+f ^<< a = arrBox f <<< a
diff --git a/test/IllTyped.hs b/test/IllTyped.hs
new file mode 100644
--- /dev/null
+++ b/test/IllTyped.hs
@@ -0,0 +1,62 @@
+
+module Main (module Main) where
+
+import Rattus
+import Rattus.Stream
+import Prelude hiding ((<*>), map, const)
+
+-- Uncomment the annotation below to check that the definitions in
+-- this module don't type check
+
+-- {-# ANN module Rattus #-}
+
+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)
+
+
+dblDelay :: Box (O (O Int))
+dblDelay = box (delay (delay 1))
+
+lambdaUnderDelay :: Box (O (O Int -> Int -> Int))
+lambdaUnderDelay = box (delay (\x _ -> adv x))
+
+leaky :: (() -> Bool) -> Str Bool
+leaky p = p () ::: delay (leaky (\ _ -> hd (leaky (\ _ -> True))))
+
+grec :: Int
+grec = grec
+
+zeros :: Box (Str Int)
+zeros = box (0 ::: delay (unbox zeros))
+
+constUnstable :: a -> Str a
+constUnstable a = run
+  where run = a ::: delay run
+
+mapUnboxed :: (a -> b) -> Str a -> Str b
+mapUnboxed f = run
+  where run (x ::: xs) = f x ::: delay (run (adv xs))
+
+
+data Input = Input {jump :: !Bool, move :: Move}
+data Move = StartLeft | EndLeft | StartRight | EndRight | NoMove
+
+-- Input is not a stable type (it is not strict). Therefore this
+-- should not type check.
+constS :: Input -> Str Input
+constS a = a ::: delay (constS a)
+
+
+-- Since Input is not strict, we cannot instantiate the 'const'
+-- function.
+-- Uncomment the definition below to check this.
+
+-- constS' :: Input -> Str Input
+-- constS' = const
+
+
+{-# ANN main NotRattus #-}
+main = putStrLn "This file should not type check"
diff --git a/test/MemoryLeak.hs b/test/MemoryLeak.hs
new file mode 100644
--- /dev/null
+++ b/test/MemoryLeak.hs
@@ -0,0 +1,84 @@
+{-# LANGUAGE TypeOperators #-}
+module Main (module Main) where
+
+import Rattus
+import Rattus.Stream
+import Rattus.ToHaskell
+
+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)
+  where acc' = unbox f acc a
+
+
+-- Unless the strictification transformation is applied this function
+-- will leak memory.
+test1 :: Int -> Str (Int) -> Str (Int)
+test1 = scan3 (box (+)) (box (== 0))
+
+
+
+-- 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 pair types, we get a memory leak:
+
+leaky :: Str (Lazy Int) -> Str (Lazy Int)
+leaky ((_,x):::xs) = ((),1) ::: delay (leaky  (fmap ((+) x) (hd (adv xs)) ::: (tl (adv xs))))
+
+
+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))))
+
+
+buffer :: Stable a => Str a -> Str (List a)
+buffer = scan (box (flip (:!))) Nil
+
+
+{-# ANN recurse NotRattus #-}
+recurse 0 (x : _) = print x
+recurse n (_ : xs) = recurse (n-1) xs
+recurse _ [] = putStrLn "the impossible happened: stream terminated"
+
+{-# ANN main NotRattus #-}
+main = do  
+  let x =  fromStr $ test1 1 (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..])
+  recurse 10000000 x
+  
+--   -- for comparison the Haskell code below does leak
+--   let x = scan2 (+) (1::Int) [1,1..]
+--   recurse 10000000 x
+
+-- {-# ANN scan2 NotRattus #-}
+-- scan2 :: (Int -> Int -> Int) -> Int -> [Int] -> [Int]
+-- scan2 f acc (a : as) =  (if a == 0 then acc else 0) : scan2 f (f acc a) as
diff --git a/test/TimeLeak.hs b/test/TimeLeak.hs
new file mode 100644
--- /dev/null
+++ b/test/TimeLeak.hs
@@ -0,0 +1,106 @@
+{-# LANGUAGE TypeOperators #-}
+module Main (module Main) where
+
+import Rattus
+import Rattus.Stream
+import Rattus.ToHaskell
+
+import Prelude hiding ((<*>), map)
+
+
+{-# ANN module Rattus #-}
+
+
+nats' :: Str Int
+nats' = unfold (box ((+) 1)) 0
+
+
+nats :: Str Int
+nats = from  0
+    where from :: Int -> Str Int
+          from n = n ::: delay (from (n+1))
+
+-- This function should cause a warning.
+leakyNats :: Str Int
+leakyNats = 0 ::: delay (map (box (+1)) leakyNats)
+
+inc :: Str Int -> Str Int
+inc = map (box ((+)1))
+
+-- This function should cause a warning.
+
+leakyNats' :: Str Int
+leakyNats' = 0 ::: delay (inc leakyNats')
+
+
+
+altMap :: Box (a -> b) -> Box (a -> b) -> Str a -> Str b
+altMap f g (x ::: xs) = unbox f x ::: delay (altMap g f (adv xs))
+
+-- This function should cause a warning.
+leakyAlt :: Str Int
+leakyAlt = 0 ::: delay (altMap (box ((+)1)) (box ((+)2)) leakyAlt)
+
+
+
+mapMap :: Box (a -> a) -> Box (a -> a) -> Str a -> Str a
+mapMap f g (x ::: xs) = unbox f x ::: delay (map g (mapMap g f (adv xs)))
+
+-- This function should cause a warning.
+leakyMap :: Str Int
+leakyMap = 0 ::: delay (mapMap (box ((+)1)) (box ((+)2)) leakyMap)
+
+
+
+-- This function should cause a warning.
+boxLeaky :: Str Int
+boxLeaky = run (box (\() -> 1)) 1
+  where run :: Box (() -> Int) -> Int -> Str Int
+        run f a = (if a == 0 then unbox f () else a)
+                  ::: delay (run (box (\ () -> (unbox f () + 1))) a)
+
+-- This function should cause a warning.
+boxLeaky' :: Str Int -> Str Int
+boxLeaky' = run (box (\() -> 1)) 1
+  where run :: Box (() -> Int) -> Int -> Str Int -> Str Int
+        run f a (x ::: xs) = (if a == 0 then unbox f () else a) ::: delay (run (box (\ () -> (unbox f () + x))) a (adv xs))
+
+
+natsTrans :: Str Int -> Str Int
+natsTrans (x ::: xs) = x ::: delay (map (box ((+)x)) $ natsTrans $ adv xs)
+ 
+leakySum :: Box (Int -> Int) -> Str Int -> Str Int
+leakySum f (x ::: xs) = unbox f x ::: (delay (leakySum (box (\ y -> unbox f (y + x)))) <*> xs)
+
+
+{-# ANN recurse NotRattus #-}
+recurse 0 (x : _) = print x
+recurse n (_ : xs) = recurse (n-1) xs
+recurse _ [] = putStrLn "the impossible happened: stream terminated"
+
+{-# ANN main NotRattus #-}
+main = do
+  let x = fromStr nats
+  recurse 10000000 x
+    
+  let x = fromStr leakyNats
+  recurse 10000000 x
+
+  let x = fromStr leakyNats'
+  recurse 10000000 x
+
+  let x = fromStr leakyAlt
+  recurse 10000000 x
+
+  let x = fromStr leakyMap
+  recurse 10000 x
+
+  let x = fromStr $ natsTrans (toStr [1..])
+  recurse 10000 x
+
+  let x = fromStr $ boxLeaky' (toStr [1..])
+  recurse 10000000 x
+
+  let x = fromStr boxLeaky
+  recurse 10000000 x
+  
diff --git a/test/WellTyped.hs b/test/WellTyped.hs
new file mode 100644
--- /dev/null
+++ b/test/WellTyped.hs
@@ -0,0 +1,75 @@
+module Main (module Main) where
+
+import Rattus
+import Rattus.Stream
+import Prelude hiding ((<*>))
+import Data.Set
+import qualified Data.Set as Set
+
+
+{-# ANN module Rattus #-}
+
+map1 :: Box (a -> b) -> Str a -> Str b
+map1 f (x ::: xs) = unbox f x ::: delay (map1 f (adv xs))
+
+map2 :: Box (a -> b) -> Str a -> Str b
+map2 f (x ::: xs) = unbox f x ::: (delay map2 <** f <*> xs)
+
+map3 :: Box (a -> b) -> Str a -> Str b
+map3 f = run
+  where run (x ::: xs) = unbox f x ::: (delay run <*> xs)
+
+
+data Input a = Input {jump :: !a, move :: !Move}
+data Move = StartLeft | EndLeft | StartRight | EndRight | NoMove
+
+type Inp a b = Input a
+
+
+
+-- The compiler plugin should detect that Input is a stable type and
+-- thus remains in scope under the delay.
+constS :: Stable a => (Inp a b) -> Str (Inp a b)
+constS a = a ::: delay (constS a)
+
+-- The constraint solver plugin should detect that Input is a stable
+-- type and thus 'const1' can be instantiated.
+constS' :: Stable a => Inp a b -> Str (Inp a b)
+constS' = const1
+
+-- make sure that unit is recognized as stable
+constU :: () -> Str ()
+constU a = a ::: delay (constU a)
+
+constU' :: () -> Str ()
+constU' = const1
+
+
+const1 :: Stable a => a -> Str a
+const1 a = a ::: delay (const1 a)
+
+const2 :: Stable a => a -> Str a
+const2 a = run
+  where run = a ::: delay run
+
+scan1 :: (Stable b) => Box(b -> a -> b) -> b -> Str a -> Str b
+scan1 f acc (a ::: as) =  acc' ::: delay (scan1 f acc' (adv as))
+  where acc' = unbox f acc a
+
+scan2 :: (Stable b) => Box(b -> a -> b) -> b -> Str a -> Str b
+scan2 f = run
+  where run acc (a ::: as) = let acc' = unbox f acc a
+                             in acc' ::: delay (run acc' (adv as))
+
+scanSet :: Str Int -> Str (Set Int)
+scanSet = scan1 (box (\ s x -> Set.insert x s)) Set.empty
+
+from :: Int -> Str Int
+from n  = n ::: delay (from (n+1))
+
+alt :: Int -> Int -> Str Int
+alt n m = n ::: delay (alt m n)
+
+
+{-# ANN main NotRattus #-}
+main = putStrLn "This file should just type check"