diff --git a/AsyncRattus.cabal b/AsyncRattus.cabal
new file mode 100644
--- /dev/null
+++ b/AsyncRattus.cabal
@@ -0,0 +1,187 @@
+cabal-version:       1.18
+name:                AsyncRattus
+version:             0.1
+category:            FRP
+synopsis:            An asynchronous modal FRP language
+description:
+
+            This library implements the Async Rattus programming
+            language as an embedded DSL. To this end the library
+            provides a GHC plugin that checks the stricter typing
+            rules of Async Rattus.
+            
+            
+            What follows is a brief introduction to the language and
+            its usage. A more detailed introduction can be found in
+            this <src/docs/paper.pdf paper>.
+            
+            .
+            
+            Async Rattus is a functional reactive programming (FRP)
+            language that uses modal types to express temporal
+            dependencies. In return the language will guarantee that
+            programs are productive (in each computation step, the
+            program makes progress), causal (output depends only on
+            current and earlier input), and have no space leaks
+            (programs do not implicitly retain memory over time).
+            
+            .
+            
+            The modal type constructor @O@ (pronounced "later") is
+            used to express the passage 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@ modal type constructor. 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@.
+
+            .
+
+            For example, the type of signals is defined as
+
+            .
+
+            > data Sig a = a ::: (O (Sig a))
+
+            .
+
+            So the current value of the signal is available now, but
+            its future state is only available in the next time
+            step. Writing a @map@ function for this type of streams,
+            requires us to use the @Box@ modality:
+
+            .
+
+            > map :: Box (a -> b) -> Sig a -> Sig b
+            > map f (x ::: xs) = unbox f x ::: delay (map f (adv xs))
+
+            .
+
+            This makes sure that the function @f@ that we give to
+            @map@ is available at any time in the future.
+
+            .
+
+            The core of the language is defined in the module
+            "AsyncRattus.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 Async Rattus programs,
+            you must enable this plugin via the GHC option
+            @-fplugin=AsyncRattus.Plugin@, e.g. by including the following
+            line in the source file:
+            
+            .
+            
+            > {-# OPTIONS -fplugin=AsyncRattus.Plugin #-}
+            
+            .
+
+            In addition, you have to annotate functions that are
+            written in Async Rattus:
+
+            .
+            
+            > {-# ANN myFunction AsyncRattus #-}
+
+            .
+
+            You can also annotate the whole module as an Async Rattus module:
+            
+            .
+
+            > {-# ANN module AsyncRattus #-}
+
+            .
+
+            Below is a minimal Async Rattus program using the
+            "AsyncRattus.Signal" module for programming with signals:
+
+            .
+
+            > {-# OPTIONS -fplugin=AsyncRattus.Plugin #-}
+            >     
+            > import AsyncRattus
+            > import AsyncRattus.Signal
+            > 
+            > {-# ANN sums AsyncRattus #-}
+            > sums :: Sig Int -> Sig Int
+            > sums = scan (box (+)) 0
+
+            .
+
+            The <docs/src/AsyncRattus.Signal.html source code of the AsyncRattus.Signal module>
+            provides more examples on how to program in Async Rattus.
+            An example project using Async Rattus can be found
+            <https://github.com/pa-ba/AsyncRattus/tree/master/examples/console here>.
+
+homepage:            https://github.com/pa-ba/AsyncRattus/
+bug-reports:         https://github.com/pa-ba/AsyncRattus/issues
+License:             BSD3
+License-file:        LICENSE
+copyright:           Copyright (C) 2023 Emil Houlborg, Gregers Rørdam, Patrick Bahr
+Author:              Emil Houlborg, Gregers Rørdam, 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  && < 4
+
+
+library
+  exposed-modules:     AsyncRattus
+                       AsyncRattus.Signal
+                       AsyncRattus.Future
+                       AsyncRattus.Strict
+                       AsyncRattus.Plugin
+                       AsyncRattus.Primitives
+                       AsyncRattus.InternalPrimitives
+                       AsyncRattus.Channels
+                       AsyncRattus.Plugin.Annotation
+                                              
+  other-modules:       AsyncRattus.Plugin.ScopeCheck
+                       AsyncRattus.Plugin.SingleTick
+                       AsyncRattus.Plugin.CheckClockCompatibility
+                       AsyncRattus.Plugin.Strictify
+                       AsyncRattus.Plugin.Utils
+                       AsyncRattus.Plugin.Dependency
+                       AsyncRattus.Plugin.StableSolver
+                       AsyncRattus.Plugin.Transform
+                       AsyncRattus.Plugin.PrimExpr
+  build-depends:       base >=4.16 && <5,
+                       containers >= 0.6.5 && < 0.8,
+                       ghc >= 9.2 && < 9.7,
+                       hashtables >= 1.3.1 && < 1.4,
+                       simple-affine-space >= 0.2.1 && < 0.3,
+                       transformers >= 0.5.6 && < 0.7
+  hs-source-dirs:      src
+  default-language:    Haskell2010
+  ghc-options:         -W
+
+
+
+Test-Suite ill-typed
+  type:                exitcode-stdio-1.0
+  main-is:             test/IllTyped.hs
+  default-language:    Haskell2010
+  build-depends:       AsyncRattus, base
+  ghc-options:         -fplugin=AsyncRattus.Plugin
+
+
+Test-Suite well-typed
+  type:                exitcode-stdio-1.0
+  main-is:             WellTyped.hs
+  hs-source-dirs:      test
+  default-language:    Haskell2010
+  build-depends:       AsyncRattus, base, containers
+  ghc-options:         -fplugin=AsyncRattus.Plugin
+
diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,3 @@
+# 0.1
+
+First release.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2023 Emil Houlborg, Gregers Rørdam, 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/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/AsyncRattus.hs b/src/AsyncRattus.hs
new file mode 100644
--- /dev/null
+++ b/src/AsyncRattus.hs
@@ -0,0 +1,26 @@
+{-# OPTIONS -fplugin=AsyncRattus.Plugin #-}
+
+
+-- | The bare-bones Asynchronous Rattus language. To program with streams,
+-- you can use "AsyncRattus.Stream".
+
+module AsyncRattus (
+  -- * Asynchronous Rattus language primitives
+  module AsyncRattus.Primitives,
+  -- * Strict data types
+  module AsyncRattus.Strict,
+  -- * Annotation
+  AsyncRattus(..),
+  -- * other
+  mapO
+  )
+  where
+
+import AsyncRattus.Plugin
+import AsyncRattus.Strict
+import AsyncRattus.Primitives
+
+{-# ANN module AsyncRattus #-}
+
+mapO :: Box (a -> b) -> O a -> O b
+mapO f later = delay (unbox f (adv later))
diff --git a/src/AsyncRattus/Channels.hs b/src/AsyncRattus/Channels.hs
new file mode 100644
--- /dev/null
+++ b/src/AsyncRattus/Channels.hs
@@ -0,0 +1,169 @@
+{-# OPTIONS -fplugin=AsyncRattus.Plugin #-}
+
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE GADTs #-}
+
+-- | This module is meant for library authors that want to build APIs
+-- for interacting with asynchronous resources, e.g. a GUI framework. 
+
+module AsyncRattus.Channels (
+  getInput,
+  setOutput,
+  mkInput,
+  startEventLoop,
+  timer,
+  Producer (..),
+) where
+
+import AsyncRattus.InternalPrimitives
+
+import AsyncRattus.Plugin.Annotation
+import AsyncRattus.Strict
+import Control.Concurrent.MVar
+import Control.Monad
+import System.IO.Unsafe
+import Data.IORef
+import Unsafe.Coerce
+import qualified Data.HashTable.IO as H
+import Data.HashTable.IO (BasicHashTable)
+import qualified Data.IntSet as IntSet
+import Control.Concurrent
+
+-- | A type @p@ satisfying @Producer p a@ is essentially a signal that
+-- produces values of type @a@ but it might not produce such values at
+-- each tick.
+class Producer p a | p -> a where
+  -- | Get the current value of the producer if any.
+  getCurrent :: p -> Maybe' a
+  -- | Get the next state of the producer. Morally, the type of this
+  -- method should be
+  --
+  -- > getNext :: p -> (exists q. Producer q a => O q)
+  --
+  -- We encode the existential type using continuation-passing style.
+  getNext :: p -> (forall q. Producer q a => O q -> b) -> b
+
+{-# ANN module AsyncRattus #-}
+{-# ANN module AllowLazyData #-}
+
+instance Producer p a => Producer (O p) a where
+  getCurrent _ = Nothing'
+  getNext p cb = cb p
+
+instance Producer p a => Producer (Box p) a where
+  getCurrent p = getCurrent (unbox p)
+  getNext p cb = getNext (unbox p) cb
+
+
+{-# NOINLINE nextFreshChannel #-}
+nextFreshChannel :: IORef InputChannelIdentifier
+nextFreshChannel = unsafePerformIO (newIORef (-1))
+
+
+{-# NOINLINE input #-}
+input :: MVar InputValue
+input = unsafePerformIO newEmptyMVar
+
+data OutputChannel where
+  OutputChannel :: Producer p a => !(O p) -> !(a -> IO ()) -> OutputChannel
+
+
+{-# NOINLINE output #-}
+output :: BasicHashTable InputChannelIdentifier (List (IORef (Maybe' OutputChannel)))
+output = unsafePerformIO (H.new)
+
+{-# NOINLINE eventLoopStarted #-}
+eventLoopStarted :: IORef Bool
+eventLoopStarted = unsafePerformIO (newIORef False)
+
+
+-- | This function can be used to implement input signals. It returns
+-- a boxed delayed computation @s@ and a callback function @cb@. The
+-- signal @mkSig s@ will produce a new value @v@ whenever the callback
+-- function @cb@ is called with argument @v@.
+getInput :: IO (Box (O a) :* (a -> IO ()))
+getInput = do ch <- atomicModifyIORef nextFreshChannel (\ x -> (x - 1, x))
+              return ((box (Delay (singletonClock ch) (\ (InputValue _ v) -> unsafeCoerce v)))
+                       :* \ x -> putMVar input (InputValue ch x))
+
+setOutput' :: Producer p a => (a -> IO ()) -> O p -> IO ()
+setOutput' cb !sig = do
+  ref <- newIORef (Just' (OutputChannel sig cb))
+  let upd Nothing = (Just (ref :! Nil),())
+      upd (Just ls) = (Just (ref :! ls),())
+  let upd' ch Nothing = do
+        forkIO (threadDelay ch >> putMVar input (InputValue ch ()))
+        return (Just (ref :! Nil),())
+      upd' _ (Just ls) = return (Just (ref :! ls),())
+  let run pre ch =
+        if ch > 0 then
+          pre >> H.mutateIO output ch (upd' ch)
+        else 
+          pre >> H.mutate output ch upd
+  IntSet.foldl' run (return ()) (extractClock sig)
+
+
+-- | This function can be used to produces outputs. Given a signal @s@
+-- and function @f@, the call @setOutput s f@ registers @f@ as a
+-- callback function that is called with argument @v@ whenever the
+-- signal produces a new value @v@. For this function to work,
+-- 'startEventLoop' must be called.
+setOutput :: Producer p a => p -> (a -> IO ()) -> IO ()
+setOutput !sig cb = do
+  case getCurrent sig of
+    Just' cur' -> cb cur'
+    Nothing' -> return ()
+  getNext sig (setOutput' cb)
+
+-- | This function is essentially the composition of 'getInput' and
+-- 'setOutput'. It turns any producer into a signal.
+mkInput :: Producer p a => p -> IO (Box (O a))
+mkInput p = do (out :* cb) <- getInput
+               setOutput p cb
+               return out
+
+-- | @timer n@ produces a delayed computation that ticks every @n@
+-- milliseconds. In particular @mkSig (timer n)@ is a signal that
+-- produces a new value every #n# milliseconds.
+timer :: Int -> Box (O ())
+timer d = Box (Delay (singletonClock (d `max` 10)) (\ _ -> ()))
+
+
+update :: InputValue -> IORef (Maybe' OutputChannel) -> IO ()
+update inp ref = do
+  mout <- readIORef ref
+  case mout of
+    Nothing' -> return ()
+    Just' (OutputChannel (Delay _ sigf) cb) -> do
+      writeIORef ref Nothing'
+      let new = sigf inp
+      case getCurrent new of
+        Just' w' -> cb w'
+        Nothing' -> return ()
+      getNext new (setOutput' cb)
+
+
+{-# ANN eventLoop NotAsyncRattus #-}
+
+eventLoop :: IO ()
+eventLoop = do inp@(InputValue ch _) <- takeMVar input
+               res <- H.lookup output ch
+               case res of
+                 Nothing -> return ()
+                 Just ls -> do
+                   H.delete output ch
+                   mapM_ (update inp) ls
+               eventLoop
+
+-- | In order for 'setOutput' to work, this IO action must be invoked.
+
+startEventLoop :: IO ()
+startEventLoop = do
+  started <- atomicModifyIORef eventLoopStarted (\b -> (True,b))
+  when (not started) eventLoop
diff --git a/src/AsyncRattus/Future.hs b/src/AsyncRattus/Future.hs
new file mode 100644
--- /dev/null
+++ b/src/AsyncRattus/Future.hs
@@ -0,0 +1,221 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeOperators #-}
+{-# OPTIONS -fplugin=AsyncRattus.Plugin #-}
+
+
+-- | Programming with futures.
+
+module AsyncRattus.Future
+  ( F(..)
+  , SigF(..)
+  , mkSigF
+  , mkSigF'
+  , current
+  , future
+  , bindF
+  , mapF
+  , sync
+  , syncF
+  , switchAwait
+  , switch
+  , switchS
+  , filterMap
+  , filterMapAwait
+  , filterAwait
+  , filter
+  , trigger
+  , triggerAwait
+  , map
+  , mapAwait
+  , zipWith
+  , zipWithAwait
+  , fromSig
+  , scan
+  , scanAwait
+  )
+
+where
+
+import AsyncRattus
+import AsyncRattus.Signal (Sig(..))
+import Prelude hiding (map, filter, zipWith)
+import AsyncRattus.Channels
+
+{-# ANN module AsyncRattus #-}
+
+newtype OneShot a = OneShot (F a)
+
+instance Producer (OneShot a) a where
+  getCurrent (OneShot (Now x)) = Just' x
+  getCurrent (OneShot (Wait _)) = Nothing'
+
+  getNext (OneShot (Now _)) cb = cb (never :: O (OneShot a))
+  getNext (OneShot (Wait x)) cb = cb (delay (OneShot (adv x)))
+
+instance Producer p a => Producer (F p) a where
+  getCurrent (Now x) = getCurrent x
+  getCurrent (Wait _) = Nothing'
+  
+  getNext (Now x) cb = getNext x cb
+  getNext (Wait x) cb = cb x
+
+instance Producer (SigF a) a where
+  getCurrent (x :>: _) = Just' x
+  getNext (_ :>: xs) cb = cb xs
+
+
+
+-- | @F a@ will produces a value of type @a@ after zero or more ticks
+-- of some clocks
+data F a = Now !a | Wait !(O (F a))
+
+
+
+bindF :: F a -> Box (a -> F b) -> F b
+bindF (Now x) f = unbox f x
+bindF (Wait x) f = Wait (delay (bindF (adv x) f))
+
+mapF :: Box (a -> b) -> F a -> F b
+mapF f d = d `bindF` (box (\ x -> Now (unbox f x)))
+
+
+sync :: O (F a) -> O (F b) -> O (F a :* F b)
+sync x y = delay (case select x y of
+                     Fst x' y' -> (x' :* Wait y')
+                     Snd x' y' -> (Wait x' :* y')
+                     Both x' y' -> (x' :* y'))
+
+syncF :: (Stable a, Stable b) => F a -> F b -> F (a :* b)
+syncF (Now x) (Now y) = Now (x :* y)
+syncF (Wait x) (Now y) = Wait (delay (syncA (adv x) y))
+syncF (Now x) (Wait y) = Wait (delay (syncB x (adv y)))
+syncF (Wait x) (Wait y) = Wait (delay (case select x y of
+                                         Fst x' y' -> syncF x' (Wait y')
+                                         Snd x' y' -> syncF (Wait x') y'
+                                         Both x' y' -> syncF x' y'
+                                      )) 
+
+syncA :: (Stable b) => F a -> b -> F (a :* b)
+syncA (Now x) y = Now (x :* y)
+syncA (Wait x) y = Wait (delay (syncA (adv x) y))
+
+
+syncB :: (Stable a) => a -> F b -> F (a :* b)
+syncB x (Now y) = Now (x :* y)
+syncB x (Wait y) = Wait (delay (syncB x (adv y)))
+
+
+-- | @SigF a@ is a signal of values of type @a@. In contrast to 'Sig',
+-- 'SigF' supports the 'filter' and 'filterMap' functions.
+data SigF a = !a :>: !(O (F (SigF a)))
+
+
+-- | Get the current value of a signal.
+current :: SigF a -> a
+current (x :>: _) = x
+
+
+-- | Get the future the signal.
+future :: SigF a -> O (F (SigF a))
+future (_ :>: xs) = xs
+
+
+mkSigF :: Box (O a) -> F (SigF a)
+mkSigF b = Wait (mkSigF' b) where
+
+mkSigF' :: Box (O a) -> O (F (SigF a))
+mkSigF' b = delay (Now (adv (unbox b) :>: mkSigF' b))
+
+
+fromSig :: Sig a -> SigF a
+fromSig (x ::: xs) = x :>: delay (Now (fromSig (adv xs)))
+
+  
+switchAwait :: F (SigF a) -> F (SigF a) -> F(SigF a)
+switchAwait _ (Now ys) = Now ys
+switchAwait (Now (x :>: xs)) (Wait ys) = Now (x :>: delay (uncurry' switchAwait (adv (sync xs ys)) ))
+switchAwait (Wait xs) (Wait ys) = Wait (delay (uncurry' switchAwait (adv (sync xs ys)) ))
+
+switch :: SigF a -> F (SigF a) -> SigF a
+switch _ (Now ys) = ys
+switch (x :>: xs) (Wait ys) = x :>: delay (uncurry' switchAwait (adv (sync xs ys)))
+
+switchS :: Stable a => SigF a -> F (a -> SigF a) -> SigF a
+switchS (x :>: _) (Now f) = f x
+switchS (x :>: xs) (Wait ys) = x :>: delay (uncurry' (switchAwaitS x) (adv (sync xs ys)))
+
+switchAwaitS :: Stable a => a -> F (SigF a) -> F (a -> SigF a) -> F (SigF a)
+switchAwaitS _ (Now (x :>: _)) (Now f) = Now (f x)
+switchAwaitS _ (Now (x :>: xs)) (Wait ys) =
+  Now (x :>: delay (uncurry' (switchAwaitS x) (adv (sync xs ys))))
+switchAwaitS x (Wait _) (Now f) = Now (f x)
+switchAwaitS x (Wait xs) (Wait ys) = Wait (delay (uncurry' (switchAwaitS x) (adv (sync xs ys))))
+
+
+
+filterMapAwait :: Box (a -> Maybe' b) -> F(SigF a) -> F (SigF b)
+filterMapAwait f (Wait xs) = Wait (delay (filterMapAwait f (adv xs)))
+filterMapAwait f (Now (x :>: xs)) = case unbox f x of
+                                     Just' y  -> Now (y :>: delay (filterMapAwait f (adv xs)))
+                                     Nothing' -> Wait (delay (filterMapAwait f (adv xs)))
+
+filterMap :: Box (a -> Maybe' b) -> SigF a -> F (SigF b)
+filterMap f xs = filterMapAwait f (Now xs)
+
+
+filterAwait :: Box (a -> Bool) -> F( SigF a) -> F (SigF a)
+filterAwait p = filterMapAwait (box (\ x -> if unbox p x then Just' x else Nothing'))
+
+filter :: Box (a -> Bool) -> SigF a -> F (SigF a)
+filter p = filterMap (box (\ x -> if unbox p x then Just' x else Nothing'))
+
+trigger :: Stable b => Box (a -> b -> c) -> SigF a -> SigF b -> SigF c
+trigger f (a :>: as) (b :>: bs) =
+  unbox f a b :>:
+  delay (uncurry' (trigger' b f) (adv (sync as bs)))
+
+triggerAwait :: Stable b => Box (a -> b -> c) -> F (SigF a) -> SigF b -> F (SigF c)
+triggerAwait f (Now (a :>: as)) (b :>: bs)
+  = Now (unbox f a b :>: delay (uncurry' (trigger' b f) (adv (sync as bs))))
+triggerAwait f (Wait as) (b :>: bs)
+  = Wait (delay (uncurry' (trigger' b f) (adv (sync as bs))))
+
+trigger' :: Stable b => b -> Box (a -> b -> c) -> F (SigF a) -> F (SigF b) -> F (SigF c)
+trigger' b f (Now (a :>: as)) (Wait bs) =
+  Now (unbox f a b :>: delay (uncurry' (trigger' b f) (adv (sync as bs))))
+trigger' _ f (Now (a :>: as)) (Now (b :>: bs)) =
+  Now (unbox f a b :>: delay (uncurry' (trigger' b f) (adv (sync as bs))))
+trigger' b f (Wait as) (Wait bs) =
+  Wait (delay (uncurry' (trigger' b f) (adv (sync as bs))))
+trigger' _ f (Wait as) (Now (b :>: bs)) =
+  Wait (delay (uncurry' (trigger' b f) (adv (sync as bs))))
+
+
+mapAwait :: Box (a -> b) -> F (SigF a) -> F (SigF b)
+mapAwait f (Now (x :>: xs)) = Now (unbox f x :>: delay (mapAwait f (adv xs)))
+mapAwait f (Wait xs) = Wait (delay (mapAwait f (adv xs)))
+
+map :: Box (a -> b) -> SigF a -> SigF b
+map f (x :>: xs) = unbox f x :>: delay (mapAwait f (adv xs))
+
+
+
+zipWith :: (Stable a, Stable b) => Box(a -> b -> c) -> SigF a -> SigF b -> SigF c
+zipWith f (a :>: as) (b :>: bs) = unbox f a b :>: delay (uncurry' (zipWithAwait f a b) (adv (sync as bs)))
+
+zipWithAwait :: (Stable a, Stable b) => Box(a -> b -> c) -> a -> b -> F (SigF a) -> F (SigF b) -> F (SigF c)
+zipWithAwait f _ _ (Now (a :>: as)) (Now (b :>: bs)) = Now (unbox f a b :>: delay (uncurry' (zipWithAwait f a b) (adv (sync as bs))))
+zipWithAwait f _ b (Now (a :>: as)) (Wait bs) = Now (unbox f a b :>: delay (uncurry' (zipWithAwait f a b) (adv (sync as bs))))
+zipWithAwait f a _ (Wait as) (Now (b :>: bs)) = Now (unbox f a b :>: delay (uncurry' (zipWithAwait f a b) (adv (sync as bs))))
+zipWithAwait f a b (Wait as) (Wait bs) = Wait (delay (uncurry' (zipWithAwait f a b) (adv (sync as bs))))
+
+scan :: (Stable b) => Box(b -> a -> b) -> b -> SigF a -> SigF b
+scan f acc (a :>: as) = acc' :>: delay (scanAwait f acc' (adv as))
+  where acc' = unbox f acc a
+
+scanAwait :: (Stable b) => Box (b -> a -> b) -> b -> F (SigF a) -> F (SigF b)
+scanAwait f acc (Now (a :>: as)) = Now (acc' :>: delay (scanAwait f acc' (adv as)))
+  where acc' = unbox f acc a
+scanAwait f acc (Wait as) = Wait (delay (scanAwait f acc (adv as)))
diff --git a/src/AsyncRattus/InternalPrimitives.hs b/src/AsyncRattus/InternalPrimitives.hs
new file mode 100644
--- /dev/null
+++ b/src/AsyncRattus/InternalPrimitives.hs
@@ -0,0 +1,172 @@
+{-# LANGUAGE GADTs #-}
+
+module AsyncRattus.InternalPrimitives where
+
+import Prelude hiding (Left, Right)
+import Data.IntSet (IntSet)
+import qualified Data.IntSet as IntSet
+
+-- An input channel is identified by an integer. The programmer should not know about it.
+type InputChannelIdentifier = Int
+
+type Clock = IntSet
+
+singletonClock :: InputChannelIdentifier -> Clock
+singletonClock = IntSet.singleton
+
+clockUnion :: Clock -> Clock -> Clock
+clockUnion = IntSet.union
+
+channelMember :: InputChannelIdentifier -> Clock -> Bool
+channelMember = IntSet.member
+
+data InputValue where
+  InputValue :: !InputChannelIdentifier -> !a -> InputValue
+
+
+-- | The "later" type modality. A value @v@ of type @O 𝜏@ consists of
+-- two components: Its clock, denoted @cl(v)@, and a delayed
+-- computation that will produce a value of type @𝜏@ as soon as the
+-- clock @cl(v)@ ticks. The clock @cl(v)@ is only used for type
+-- checking and is not directly accessible, whereas the delayed
+-- computation is accessible via 'adv' and 'select'.
+
+data O a = Delay !Clock (InputValue -> a)
+
+-- | The return type of the 'select' primitive.
+data Select a b = Fst !a !(O b) | Snd !(O a) !b | Both !a !b
+
+asyncRattusError pr = error (pr ++ ": Did you forget to mark this as Async Rattus code?")
+
+-- | This is the constructor for the "later" modality 'O':
+--
+-- >     Γ ✓θ ⊢ t :: 𝜏
+-- > --------------------
+-- >  Γ ⊢ delay t :: O 𝜏
+--
+-- The typing rule requires that its argument @t@ typecheck with an
+-- additional tick @✓θ@ of some clock @θ@.
+{-# INLINE [1] delay #-}
+delay :: a -> O a
+delay _ = asyncRattusError "delay"
+
+extractClock :: O a -> Clock
+extractClock (Delay cl _) = cl
+
+{-# INLINE [1] adv' #-}
+adv' :: O a -> InputValue -> a
+adv' (Delay _ f) inp = f inp
+
+
+-- | This is the eliminator for the "later" modality 'O':
+--
+-- >   Γ ⊢ t :: O 𝜏     Γ' tick-free
+-- > ---------------------------------
+-- >     Γ ✓cl(t) Γ' ⊢ adv t :: 𝜏
+--
+-- It requires that a tick @✓θ@ is in the context whose clock matches
+-- exactly the clock of @t@, i.e. @θ = cl(t)@.
+
+{-# INLINE [1] adv #-}
+adv :: O a -> a
+adv _ = asyncRattusError "adv"
+
+-- | If we want to eliminate more than one delayed computation, i.e.\
+-- two @s :: O σ@ and @t :: O 𝜏@, we need to use 'select' instead of
+-- just 'adv'.
+--
+-- >   Γ ⊢ s :: O σ     Γ ⊢ t :: O 𝜏     Γ' tick-free
+-- > --------------------------------------------------
+-- >    Γ ✓cl(s)⊔cl(t) Γ' ⊢ select s t :: Select σ 𝜏
+--
+-- It requires that we have a tick @✓θ@ in the context whose clock
+-- matches the union of the clocks of @s@ and @t@, i.e. @θ =
+-- cl(s)⊔cl(t)@. The union of two clocks ticks whenever either of the
+-- two clocks ticks, i.e. @cl(s)⊔cl(t)@, whenever @cl(s)@ or @cl(t)@
+-- ticks.
+--
+-- That means there are three possible outcomes, which are reflected
+-- in the result type of @select s t@. A value of @Select σ 𝜏@ is
+-- either
+--
+--   * a value of type @σ@ and a delayed computation of type @O 𝜏@, if
+--     @cl(s)@ ticks before @cl(t)@,
+--
+--   * a value of type @𝜏@ and a delayed computation of type @O σ@, if
+--     @cl(t)@ ticks before @cl(s)@, or
+--
+--   * a value of type @σ@ and a value of type @𝜏@, if @cl(s)@ and
+--   * @cl(s)@ tick simultaneously.
+
+
+{-# INLINE [1] select #-}
+select :: O a -> O b -> Select a b
+select _ _ = asyncRattusError "select"
+
+select' :: O a -> O b -> InputValue -> Select a b
+select' a@(Delay clA inpFA) b@(Delay clB inpFB) inputValue@(InputValue chId _)
+  = if chId `channelMember` clA then
+      if chId `channelMember` clB then Both (inpFA inputValue) (inpFB inputValue)
+      else Fst (inpFA inputValue) b
+    else Snd a (inpFB inputValue)
+
+
+-- | The clock of @never :: O 𝜏@ will never tick, i.e. it will never
+-- produce a value of type @𝜏@. With 'never' we can for example
+-- implement the constant signal @x ::: never@ of type @Sig a@ for any @x ::
+-- a@.
+never :: O a
+never = Delay IntSet.empty (error "Trying to adv on the 'never' delayed computation")
+
+-- | 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 (Sig a -> Sig b)@.
+--
+-- But these types are not stable: @[Int]@ (because the list type is
+-- not strict), @Int -> Int@, (function type is not stable), @O
+-- Int@, @Sig Int@.
+
+class  Stable a  where
+
+
+
+-- | 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 "stable" modality 'Box':
+--
+-- >     Γ☐ ⊢ t :: 𝜏
+-- > --------------------
+-- >  Γ ⊢ box t :: Box 𝜏
+--
+-- where Γ☐ is obtained from Γ by removing all ticks and all variables
+-- @x :: 𝜏@, where 𝜏 is not a stable type.
+
+{-# INLINE [1] box #-}
+box :: a -> Box a
+box x = Box x
+
+
+-- | This is the eliminator for the "stable" modality  'Box':
+--
+-- >   Γ ⊢ 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
+    #-}
diff --git a/src/AsyncRattus/Plugin.hs b/src/AsyncRattus/Plugin.hs
new file mode 100644
--- /dev/null
+++ b/src/AsyncRattus/Plugin.hs
@@ -0,0 +1,166 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE CPP #-}
+
+
+-- | The plugin to make it all work.
+
+module AsyncRattus.Plugin (plugin, AsyncRattus(..)) where
+import AsyncRattus.Plugin.StableSolver
+import AsyncRattus.Plugin.ScopeCheck
+import AsyncRattus.Plugin.Strictify
+import AsyncRattus.Plugin.SingleTick
+import AsyncRattus.Plugin.CheckClockCompatibility
+import AsyncRattus.Plugin.Utils
+import AsyncRattus.Plugin.Annotation
+import AsyncRattus.Plugin.Transform
+
+import Prelude hiding ((<>))
+
+import Control.Monad
+import Data.Maybe
+import Data.List
+import Data.Data hiding (tyConName)
+import qualified Data.Set as Set
+import Data.Set (Set)
+
+#if __GLASGOW_HASKELL__ >= 900
+import GHC.Plugins
+import GHC.Tc.Types
+#else
+import GhcPlugins
+import TcRnTypes
+#endif
+
+-- | Use this to enable Asynchronous Rattus' plugin, either by supplying the option
+-- @-fplugin=AsyncRattus.Plugin@ directly to GHC, or by including the
+-- following pragma in each source file:
+-- 
+-- > {-# OPTIONS -fplugin=AsyncRattus.Plugin #-}
+plugin :: Plugin
+plugin = defaultPlugin {
+  installCoreToDos = install,
+  pluginRecompile = purePlugin,
+  typeCheckResultAction = typechecked,
+  tcPlugin = tcStable
+  }
+
+
+data Options = Options {debugMode :: Bool}
+
+typechecked :: [CommandLineOption] -> ModSummary -> TcGblEnv -> TcM TcGblEnv
+typechecked _ _ env = checkAll env >> return env
+
+install :: [CommandLineOption] -> [CoreToDo] -> CoreM [CoreToDo]
+install opts todo = case find findSamePass todo of       -- check that we don't run the transformation twice
+                      Nothing -> return (strPass : todo) -- (e.g. if the "-fplugin" option is used twice)
+                      _ -> return todo
+    where name = "Async Rattus strictify"
+          strPass = CoreDoPluginPass name (strictifyProgram Options{debugMode = dmode})
+          dmode = "debug" `elem` opts
+          findSamePass (CoreDoPluginPass s _) = s == name
+          findSamePass _ = False
+          
+
+-- | Apply the following operations to all Asynchronous Rattus definitions in the
+-- program:
+--
+-- * Transform into single tick form (see SingleTick module)
+-- * Check whether lazy data types are used (see Strictify module)
+-- * Transform into call-by-value form (see Strictify module)
+
+strictifyProgram :: Options -> ModGuts -> CoreM ModGuts
+strictifyProgram opts guts = do
+  newBinds <- mapM (strictify opts guts) (mg_binds guts)
+  return guts { mg_binds = newBinds }
+
+strictify :: Options -> ModGuts -> CoreBind -> CoreM CoreBind
+strictify opts guts b@(Rec bs) = do
+  let debug = debugMode opts
+  tr <- liftM or (mapM (shouldProcessCore guts . fst) bs)
+  if tr then do
+    let vs = map fst bs
+    es' <- mapM (\ (v,e) -> do
+      processCore <- shouldProcessCore guts v
+      if not processCore
+      then do
+        when debug $ putMsg $ text "Skipping binding: " <> ppr v
+        return e
+      else checkAndTransform guts (Set.fromList vs) debug v e
+      ) bs
+    when debug $ putMsg $ "Plugin | result of transformation: " <> ppr es'
+    return (Rec (zip vs es'))
+  else return b
+strictify opts guts b@(NonRec v e) = do
+    let debug = debugMode opts
+    when debug $ putMsg $ text "Processing binding: " <> ppr v <> text " | Non-recursive binding"
+    when debug $ putMsg $ text "Expr: " <> ppr e
+    processCore <- shouldProcessCore guts v
+    if not processCore then do
+      when debug $ putMsg $ text "Skipping binding: " <> ppr v
+      return b
+    else do
+      transformed <- checkAndTransform guts Set.empty debug v e
+      when debug $ putMsg $ "Plugin | result of transformation: " <> ppr transformed
+      return $ NonRec v transformed
+
+checkAndTransform :: ModGuts -> Set Var -> Bool -> Var -> CoreExpr -> CoreM CoreExpr
+checkAndTransform guts recursiveSet debug v e = do
+  when debug $ putMsg $ text "Processing binding: " <> ppr v
+  when debug $ putMsg $ text "Expr: " <> ppr e
+  allowRec <- allowRecursion guts v
+  singleTick <- toSingleTick e
+  when debug $ putMsg $ text "Single-tick: " <> ppr singleTick
+  lazy <- allowLazyData guts v
+  strict <- strictifyExpr (SCxt (nameSrcSpan $ getName v) (not lazy)) singleTick
+  when debug $ putMsg $ text "Strict single-tick: " <> ppr strict
+  checkExpr CheckExpr{ recursiveSet = recursiveSet, oldExpr = e,
+                        verbose = debug,
+                        allowRecExp = allowRec} strict
+  transform strict
+
+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
+
+
+
+
+allowLazyData :: ModGuts -> CoreBndr -> CoreM Bool
+allowLazyData guts bndr = do
+  l <- annotationsOn guts bndr :: CoreM [AsyncRattus]
+  return (AllowLazyData `elem` l)
+
+allowRecursion :: ModGuts -> CoreBndr -> CoreM Bool
+allowRecursion guts bndr = do
+  l <- annotationsOn guts bndr :: CoreM [AsyncRattus]
+  return (AllowRecursion `elem` l)
+
+expectError :: ModGuts -> CoreBndr -> CoreM Bool
+expectError guts bndr = do
+  l <- annotationsOn guts bndr :: CoreM [InternalAnn]
+  return $ ExpectError `elem` l
+
+
+shouldProcessCore :: ModGuts -> CoreBndr -> CoreM Bool
+shouldProcessCore guts bndr = do
+  l <- annotationsOn guts bndr :: CoreM [AsyncRattus]
+  expectScopeError <- expectError guts bndr
+  return (AsyncRattus `elem` l && notElem NotAsyncRattus l && userFunction bndr && not expectScopeError)
+
+annotationsOn :: (Data a) => ModGuts -> CoreBndr -> CoreM [a]
+annotationsOn guts bndr = do
+#if __GLASGOW_HASKELL__ >= 900
+  (_,anns)  <- getAnnotations deserializeWithData guts
+  return $
+    lookupWithDefaultUFM anns [] (varName bndr) ++
+    getModuleAnnotations guts
+#else    
+  anns <- getAnnotations deserializeWithData guts
+  return $
+    lookupWithDefaultUFM anns [] (varUnique bndr) ++
+    getModuleAnnotations guts
+#endif
diff --git a/src/AsyncRattus/Plugin/Annotation.hs b/src/AsyncRattus/Plugin/Annotation.hs
new file mode 100644
--- /dev/null
+++ b/src/AsyncRattus/Plugin/Annotation.hs
@@ -0,0 +1,40 @@
+{-# LANGUAGE DeriveDataTypeable #-}
+module AsyncRattus.Plugin.Annotation (AsyncRattus(..), InternalAnn (..)) where
+
+import Data.Data
+
+-- | Use this type to mark a Haskell function definition as an
+-- Asynchronous Rattus function:
+--
+-- > {-# ANN myFunction AsyncRattus #-}
+-- 
+-- Or mark a whole module as consisting of Asynchronous Rattus functions only:
+--
+-- > {-# ANN module AsyncRattus #-}
+--
+-- 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 NotAsyncRattus #-}
+--
+-- By default all Asynchronous 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 #-}
+--
+-- Asynchronous Rattus only allows guarded recursion, i.e. recursive calls must
+-- occur in the scope of a tick. Structural recursion over strict data
+-- types is safe as well, but is currently not checked. To disable the
+-- guarded recursion check, annotate the module or function with
+-- 'AllowRecursion'.
+
+data AsyncRattus = AsyncRattus | NotAsyncRattus | AllowLazyData | AllowRecursion deriving (Typeable, Data, Show, Ord, Eq)
+
+
+-- | This annotation type is for internal use only.
+data InternalAnn = ExpectError | ExpectWarning deriving (Typeable, Data, Show, Eq, Ord)
diff --git a/src/AsyncRattus/Plugin/CheckClockCompatibility.hs b/src/AsyncRattus/Plugin/CheckClockCompatibility.hs
new file mode 100644
--- /dev/null
+++ b/src/AsyncRattus/Plugin/CheckClockCompatibility.hs
@@ -0,0 +1,268 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE CPP #-}
+
+-- | This module implements the check that the transformed code is
+-- typable in the single tick calculus.
+
+module AsyncRattus.Plugin.CheckClockCompatibility
+  (checkExpr, CheckExpr (..)) where
+
+#if __GLASGOW_HASKELL__ >= 902
+import GHC.Types.Tickish
+#endif
+
+#if __GLASGOW_HASKELL__ >= 900
+import GHC.Plugins
+#else
+import GhcPlugins
+#endif
+
+import AsyncRattus.Plugin.Utils
+import qualified AsyncRattus.Plugin.PrimExpr as Prim
+import Prelude hiding ((<>))
+import Data.Set (Set)
+import qualified Data.Set as Set
+import Data.Map (Map)
+import qualified Data.Map as Map
+import Data.Maybe (isJust)
+import Control.Monad (foldM, when)
+import Control.Applicative ((<|>))
+import System.Exit (exitFailure)
+
+type LCtx = Set Var
+data HiddenReason = BoxApp | AdvApp | NestedRec Var | FunDef | DelayApp
+type Hidden = Map Var HiddenReason
+
+data TypeError = TypeError SrcSpan SDoc
+
+
+data Ctx = Ctx
+  { current :: LCtx,
+    hidden :: Hidden,
+    earlier :: Maybe LCtx,
+    srcLoc :: SrcSpan,
+    recDef :: Set Var, -- ^ recursively defined variables 
+    stableTypes :: Set Var,
+    allowRecursion :: Bool,
+    allowGuardedRec :: Bool
+    }
+
+hasTick :: Ctx -> Bool
+hasTick = isJust . earlier
+
+stabilize :: HiddenReason -> Ctx -> Ctx
+stabilize hr c = c
+  {current = Set.empty,
+   earlier = Nothing,
+   hidden = hidden c `Map.union` Map.fromSet (const hr) ctxHid,
+   allowGuardedRec = False
+  }
+  where ctxHid = maybe (current c) (Set.union (current c)) (earlier c)
+
+data Scope = Hidden SDoc | Visible
+
+getScope  :: Ctx -> Var -> Scope
+getScope c v =
+    if v `Set.member` recDef c then
+      if allowGuardedRec c || allowRecursion c || typeClassFunction v then Visible
+      else Hidden ("(Mutually) recursive call to " <> ppr v <> " must occur under delay")
+    else case Map.lookup v (hidden c) of
+      Just reason ->
+        if (isStable (stableTypes c) (varType v)) then Visible
+        else case reason of
+          NestedRec rv ->
+            if allowRecursion c then Visible
+            else Hidden ("Variable " <> ppr v <> " is no longer in scope:"
+                         $$ "It appears in a local recursive definition (namely of " <> ppr rv <> ")"
+                         $$ "and is of type " <> ppr (varType v) <> ", which is not stable.")
+          BoxApp -> 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.")
+          AdvApp -> Hidden ("Variable " <> ppr v <> " is no longer in scope: It occurs under adv.")
+
+          FunDef -> 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")
+          DelayApp -> Hidden ("Variable " <> ppr v <> " is no longer in scope: It occurs under two occurrences of delay and is a of a non-stable type " <> ppr (varType v))
+      Nothing
+          | maybe False (Set.member v) (earlier c) ->
+            if isStable (stableTypes c) (varType v) then Visible
+            else Hidden ("Variable " <> ppr v <> " is no longer in scope:" $$
+                         "It occurs under delay" $$ "and is of type " <> ppr (varType v) <> ", which is not stable.")
+          | Set.member v (current c) -> Visible
+          | otherwise -> Visible
+
+
+
+pickFirst :: SrcSpan -> SrcSpan -> SrcSpan
+pickFirst s@RealSrcSpan{} _ = s
+pickFirst _ s = s
+
+typeError :: Ctx -> Var -> SDoc -> TypeError
+typeError ctx var = TypeError (pickFirst (srcLoc ctx) (nameSrcSpan (varName var)))
+
+instance Outputable TypeError where
+  ppr (TypeError srcLoc sdoc) = text "TypeError at " <> ppr srcLoc <> text ": " <> ppr sdoc
+
+emptyCtx :: CheckExpr -> Ctx
+emptyCtx c =
+  Ctx { current =  Set.empty,
+        earlier = Nothing,
+        hidden = Map.empty,
+        srcLoc = noLocationInfo,
+        recDef = recursiveSet c,
+        stableTypes = Set.empty,
+        allowRecursion = allowRecExp c,
+        allowGuardedRec = False
+        }
+
+stabilizeLater :: Ctx -> Ctx
+stabilizeLater c =
+  case earlier c of
+    Just earl -> c {earlier = Nothing,
+                    hidden = hidden c `Map.union` Map.fromSet (const FunDef) earl}
+    Nothing -> c
+
+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
+
+-- should be equatable
+type SymbolicClock = Set Var
+
+mkClock1 :: Var -> SymbolicClock
+mkClock1 = Set.singleton
+
+mkClock2 :: Var -> Var -> SymbolicClock
+mkClock2 v1 v2 = Set.fromList [v1, v2]
+
+newtype CheckResult = CheckResult{
+  -- if present, contains the variable of the primitive applied so we can report its position
+  -- in case of an error, and the clock for the primitive
+  prim :: Maybe (Var, SymbolicClock)
+}
+
+instance Outputable CheckResult where
+  ppr (CheckResult prim) = text "CheckResult {prim = " <> ppr prim <> text "}"
+
+emptyCheckResult :: CheckResult
+emptyCheckResult = CheckResult {prim = Nothing}
+
+data CheckExpr = CheckExpr{
+  recursiveSet :: Set Var,
+  oldExpr :: Expr Var,
+  verbose :: Bool,
+  allowRecExp :: Bool
+  }
+
+checkExpr :: CheckExpr -> Expr Var -> CoreM ()
+checkExpr c e = do
+  when (verbose c) $ putMsg $ text "checkExpr: " <> ppr e
+  res <- checkExpr' (emptyCtx c) e
+  case res of
+    Right _ -> do when (verbose c) $ putMsgS "checkExpr succeeded."
+    Left (TypeError src doc) ->
+      let printErrMsg = if verbose c
+          then do
+            printMessage SevError src ("Internal error in Async Rattus Plugin: single tick transformation did not preserve typing." $$ doc)
+            putMsgS "-------- old --------"
+            putMsg $ ppr (oldExpr c)
+            putMsgS "-------- new --------"
+            putMsg (ppr e)
+            
+          else do
+            printMessage SevError noSrcSpan ("Internal error in Async Rattus Plugin: single tick transformation did not preserve typing." $$
+                                  "Compile with flags \"-fplugin-opt AsyncRattus.Plugin:debug\" and \"-g2\" for detailed information")
+      in do
+        printErrMsg
+        liftIO exitFailure
+
+
+checkExpr' :: Ctx -> Expr Var -> CoreM (Either TypeError CheckResult)
+checkExpr' c (App e e') | isType e' || (not $ tcIsLiftedTypeKind $ typeKind $ exprType e')
+  = checkExpr' c e
+checkExpr' c@Ctx{current = cur, earlier = earl} expr@(App e e') =
+  case Prim.isPrimExpr expr of
+    Just (Prim.BoxApp _) ->
+      checkExpr' (stabilize BoxApp c) e'
+    Just (Prim.DelayApp f _) -> do
+      let c' = case earl of
+                 Nothing -> c{current = Set.empty, earlier = Just cur, allowGuardedRec = True}
+                 Just earl' -> c{ current = Set.empty, earlier = Just cur, allowGuardedRec = True,
+                                  hidden = hidden c `Map.union` Map.fromSet (const DelayApp) earl'}
+      eRes <- checkExpr' c' e'
+      case eRes of
+        Left err -> return $ Left err
+        Right (CheckResult {prim = Nothing}) -> return $ Left $ typeError c f (text "Each delay must contain an adv or select")
+        Right _ -> return $ Right emptyCheckResult
+    Just (Prim.AdvApp f _) | not (hasTick c) -> return $ Left $ typeError c f (text "can only use adv under delay")
+    Just (Prim.AdvApp f (arg, _)) -> return $ Right $ CheckResult {prim = Just (f, mkClock1 arg)}
+    Just (Prim.SelectApp f _ _) | not (hasTick c) -> return $ Left $ typeError c f (text "can only use select under delay")
+    Just (Prim.SelectApp f (arg1, _) (arg2, _))-> return $ Right $ CheckResult {prim = Just (f, mkClock2 arg1 arg2)}
+    Nothing -> checkBoth c e e'
+checkExpr' c (Case e v _ alts) = do
+    res <- checkExpr' c' e
+    resAll <- mapM (\(Alt _ _ altE) -> checkExpr' c altE) alts
+    foldM (fmap return . combine c) res resAll
+  where c' = addVars [v] c
+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] (stabilizeLater c)) e
+checkExpr' _ (Type _)  = return $ Right emptyCheckResult
+checkExpr' _ (Lit _)  = return $ Right emptyCheckResult
+checkExpr' _ (Coercion _)  = return $ Right emptyCheckResult
+checkExpr' c (Tick (SourceNote span _name) e) =
+  checkExpr' c{srcLoc = fromRealSrcSpan span} e
+checkExpr' c (Tick _ e) = checkExpr' c e
+checkExpr' c (Cast e _) = checkExpr' c e
+checkExpr' c (Let (NonRec _ e1) e2) = do
+  res1 <- checkExpr' c e1
+  res2 <- checkExpr' c e2
+  return $ combine c res1 res2
+checkExpr' c (Let (Rec binds) e2) = do
+    resAll <- mapM (\ (v,e) -> checkExpr' (c' v) e) binds
+    res <- checkExpr' (addVars vs c) e2
+    foldM (fmap return . combine c) res resAll
+  where vs = map fst binds
+        ctxHid = maybe (current c) (Set.union (current c)) (earlier c)
+        c' v = c {current = Set.empty,
+                  earlier = Nothing,
+                  hidden =  hidden c `Map.union`
+                   Map.fromSet (const (NestedRec v)) ctxHid,
+                  recDef = recDef c `Set.union` Set.fromList vs }
+checkExpr' c  (Var v)
+  | tcIsLiftedTypeKind $ typeKind $ varType v =  case getScope c v of
+             Hidden reason -> return $ Left $ typeError c v reason
+             Visible -> return $ Right emptyCheckResult
+  | otherwise = return $ Right emptyCheckResult
+
+addVars :: [Var] -> Ctx -> Ctx
+addVars v c = c{current = Set.fromList v `Set.union` current c }
+
+checkBoth :: Ctx -> CoreExpr -> CoreExpr -> CoreM (Either TypeError CheckResult)
+checkBoth c e e' = do
+  c1 <- checkExpr' c e
+  c2 <- checkExpr' c e'
+  return $ combine c c1 c2
+
+-- Combines two CheckResults such that the clocks therein are compatible.
+-- If both CheckResults have PrimVars, one is picked arbitrarily.
+combine :: Ctx -> Either TypeError CheckResult -> Either TypeError CheckResult -> Either TypeError CheckResult
+combine c eRes1 eRes2 = do
+  res1 <- eRes1
+  res2 <- eRes2
+  case (res1, res2) of
+    (CheckResult (Just (_, cl1)), CheckResult (Just (_, cl2))) | cl1 == cl2 -> Right res2
+    (CheckResult (Just _), CheckResult (Just (p, _))) -> Left $ typeError c p "Only one adv/select allowed in a delay"
+    (CheckResult maybeP, CheckResult maybeP') -> Right $ CheckResult {prim = maybeP <|> maybeP'}
diff --git a/src/AsyncRattus/Plugin/Dependency.hs b/src/AsyncRattus/Plugin/Dependency.hs
new file mode 100644
--- /dev/null
+++ b/src/AsyncRattus/Plugin/Dependency.hs
@@ -0,0 +1,503 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE GADTs #-}
+
+-- | This module is used to perform a dependency analysis of top-level
+-- function definitions, i.e. to find out which defintions are
+-- (mutual) recursive. To this end, this module also provides
+-- functions to compute, bound variables and variable occurrences.
+
+module AsyncRattus.Plugin.Dependency (dependency, HasBV (..),printBinds) where
+
+#if __GLASGOW_HASKELL__ >= 900
+import GHC.Plugins
+import GHC.Data.Bag
+import GHC.Hs.Type
+#else
+import GhcPlugins
+import Bag
+#if __GLASGOW_HASKELL__ >= 810
+import GHC.Hs.Types
+#else
+import HsTypes
+#endif
+#endif
+
+#if __GLASGOW_HASKELL__ >= 810
+import GHC.Hs.Extension
+import GHC.Hs.Expr
+import GHC.Hs.Pat
+import GHC.Hs.Binds
+#else 
+import HsExtension
+import HsExpr
+import HsPat
+import HsBinds
+#endif
+
+#if __GLASGOW_HASKELL__ >= 904
+import GHC.Parser.Annotation
+#elif __GLASGOW_HASKELL__ >= 902
+import Language.Haskell.Syntax.Extension
+import GHC.Parser.Annotation
+#endif
+
+
+import Data.Set (Set)
+import qualified Data.Set as Set
+import Data.Graph
+import Data.Maybe
+import Data.Either
+import Prelude hiding ((<>))
+
+
+
+-- | Compute the dependencies of a bag of bindings, returning a list
+-- of the strongly-connected components.
+dependency :: Bag (LHsBindLR GhcTc GhcTc) -> [SCC (LHsBindLR GhcTc GhcTc, Set Var)]
+dependency binds = map AcyclicSCC noDeps ++ catMaybes (map filterJust (stronglyConnComp (concat deps)))
+  where (deps,noDeps) = partitionEithers $ map mkDep $ bagToList binds
+        mkDep :: GenLocated l (HsBindLR GhcTc GhcTc) ->
+                 Either [(Maybe (GenLocated l (HsBindLR GhcTc GhcTc), Set Var), Name, [Name])]
+                 (GenLocated l (HsBindLR GhcTc GhcTc), Set Var)
+        mkDep b =
+          let dep = map varName $ Set.toList (getFV b)
+              vars = getBV b in
+          case Set.toList vars of
+            (v:vs) -> Left ((Just (b,vars), varName v , dep) : map (\ v' -> (Nothing, varName v' , dep)) vs)
+            [] -> Right (b,vars)
+        filterJust (AcyclicSCC Nothing) = Nothing -- this should not happen
+        filterJust (AcyclicSCC (Just b)) = Just (AcyclicSCC b)
+        filterJust (CyclicSCC bs) = Just (CyclicSCC (catMaybes bs))
+
+
+printBinds (AcyclicSCC bind) = liftIO (putStr "acyclic bind: ") >> printBind (fst bind) >> liftIO (putStrLn "") 
+printBinds (CyclicSCC binds) = liftIO (putStr "cyclic binds: ") >> mapM_ (printBind . fst) binds >> liftIO (putStrLn "") 
+
+
+printBind (L _ FunBind{fun_id = L _ name}) = 
+  liftIO $ putStr $ (getOccString name ++ " ")
+printBind (L _ (VarBind {var_id = name})) =   liftIO $ putStr $ (getOccString name ++ " ")
+#if __GLASGOW_HASKELL__ < 904
+printBind (L _ (AbsBinds {abs_exports = exp})) = 
+#else
+printBind (L _ (XHsBindsLR (AbsBinds {abs_exports = exp}))) = 
+#endif
+  mapM_ (\ e -> liftIO $ putStr $ ((getOccString $ abe_poly e)  ++ " ")) exp
+printBind _ = return ()
+
+
+-- | Computes the variables that are bound by a given piece of syntax.
+
+class HasBV a where
+  getBV :: a -> Set Var
+
+instance HasBV (HsBindLR GhcTc GhcTc) where
+  getBV (FunBind{fun_id = L _ v}) = Set.singleton v
+  getBV (PatBind {pat_lhs = pat}) = getBV pat
+  getBV (VarBind {var_id = v}) = Set.singleton v
+  getBV PatSynBind{} = Set.empty
+#if __GLASGOW_HASKELL__ < 900
+  getBV (XHsBindsLR e) = getBV e
+  getBV (AbsBinds {abs_exports = es}) = Set.fromList (map abe_poly es)
+#elif __GLASGOW_HASKELL__ < 904
+  getBV (AbsBinds {abs_exports = es}) = Set.fromList (map abe_poly es)
+#else
+  getBV (XHsBindsLR (AbsBinds {abs_exports = es})) = Set.fromList (map abe_poly es)
+#endif
+  
+instance HasBV a => HasBV (GenLocated b a) where
+  getBV (L _ e) = getBV e
+
+instance HasBV a => HasBV [a] where
+  getBV ps = foldl (\s p -> getBV p `Set.union` s) Set.empty ps
+
+#if __GLASGOW_HASKELL__ >= 904
+getRecFieldRhs = hfbRHS
+#else
+getRecFieldRhs = hsRecFieldArg
+#endif
+
+#if __GLASGOW_HASKELL__ >= 902
+getConBV (PrefixCon _ ps) = getBV ps
+#else
+getConBV (PrefixCon ps) = getBV ps
+#endif
+getConBV (InfixCon p p') = getBV p `Set.union` getBV p'
+getConBV (RecCon (HsRecFields {rec_flds = fs})) = foldl run Set.empty fs
+      where run s (L _ f) = getBV (getRecFieldRhs f) `Set.union` s
+
+#if __GLASGOW_HASKELL__ >= 900 && __GLASGOW_HASKELL__ < 904
+instance HasBV CoPat where
+  getBV CoPat {co_pat_inner = p} = getBV p
+#elif __GLASGOW_HASKELL__ >= 904
+instance HasBV XXPatGhcTc where
+  getBV CoPat {co_pat_inner = p} = getBV p
+  getBV (ExpansionPat _ p) = getBV p
+#endif
+
+instance HasBV (Pat GhcTc) where
+  getBV (VarPat _ (L _ v)) = Set.singleton v
+  getBV (LazyPat _ p) = getBV p
+#if __GLASGOW_HASKELL__ >= 906
+  getBV (AsPat _ (L _ v) _ p) = Set.insert v (getBV p)
+#else
+  getBV (AsPat _ (L _ v) p) = Set.insert v (getBV p)
+#endif
+  getBV (BangPat _ p) = getBV p
+  getBV (ListPat _ ps) = getBV ps
+  getBV (TuplePat _ ps _) = getBV ps
+  getBV (SumPat _ p _ _) = getBV p
+  getBV (ViewPat _ _ p) = getBV p
+
+  getBV (SplicePat _ sp) =
+    case sp of
+#if __GLASGOW_HASKELL__ < 906
+      HsTypedSplice _ _ v _ -> Set.singleton v
+      HsSpliced _ _ (HsSplicedPat p) -> getBV p
+      HsUntypedSplice _ _ v _ ->  Set.singleton v
+      HsQuasiQuote _ p p' _ _ -> Set.fromList [p,p']
+      _ -> Set.empty
+#else
+      HsUntypedSpliceExpr _ e -> getFV e
+      HsQuasiQuote _ v _  -> Set.singleton v
+#endif
+
+  getBV (NPlusKPat _ (L _ v) _ _ _ _) = Set.singleton v
+  getBV (NPat {}) = Set.empty
+  getBV (XPat p) = getBV p
+  getBV (WildPat {}) = Set.empty
+  getBV (LitPat {}) = Set.empty
+#if __GLASGOW_HASKELL__ >= 904  
+  getBV (ParPat _ _ p _) = getBV p
+#else
+  getBV (ParPat _ p) = getBV p
+#endif
+#if __GLASGOW_HASKELL__ >= 900
+  getBV (ConPat {pat_args = con}) = getConBV con
+#else
+  getBV (ConPatIn (L _ v) con) = Set.insert v (getConBV con)
+  getBV (ConPatOut {pat_args = con}) = getConBV con
+  getBV (CoPat _ _ p _) = getBV p
+#endif
+#if __GLASGOW_HASKELL__ >= 808
+  getBV (SigPat _ p _) = getBV p
+#else
+  getBV (SigPat _ p)   = getBV p
+#endif
+
+#if __GLASGOW_HASKELL__ >= 904
+
+#elif __GLASGOW_HASKELL__ >= 810
+instance HasBV NoExtCon where
+#else
+instance HasBV NoExt where
+#endif
+#if __GLASGOW_HASKELL__ < 904
+  getBV _ = Set.empty
+#endif
+
+-- | Syntax that may contain variables.
+class HasFV a where
+  -- | Compute the set of variables occurring in the given piece of
+  -- syntax.  The name falsely suggests that returns free variables,
+  -- but in fact it returns all variable occurrences, no matter
+  -- whether they are free or bound.
+  getFV :: a -> Set Var 
+
+instance HasFV a => HasFV (GenLocated b a) where
+  getFV (L _ e) = getFV e
+  
+instance HasFV a => HasFV [a] where
+  getFV es = foldMap getFV es
+
+instance HasFV a => HasFV (Bag a) where
+  getFV es = foldMap getFV es
+
+instance HasFV Var where
+  getFV v = Set.singleton v
+
+instance HasFV a => HasFV (MatchGroup GhcTc a) where
+  getFV MG {mg_alts = alts} = getFV alts
+#if __GLASGOW_HASKELL__ < 900
+  getFV (XMatchGroup e) = getFV e
+#endif
+  
+instance HasFV a => HasFV (Match GhcTc a) where
+  getFV Match {m_grhss = rhss} = getFV rhss
+#if __GLASGOW_HASKELL__ < 900
+  getFV (XMatch e) = getFV e
+#endif
+
+instance HasFV (HsTupArg GhcTc) where
+  getFV (Present _ e) = getFV e
+  getFV Missing {} = Set.empty
+#if __GLASGOW_HASKELL__ < 900
+  getFV (XTupArg e) = getFV e
+#endif
+
+instance HasFV a => HasFV (GRHS GhcTc a) where
+  getFV (GRHS _ g b) = getFV g `Set.union` getFV b
+#if __GLASGOW_HASKELL__ < 900
+  getFV (XGRHS e) = getFV e
+#endif
+
+instance HasFV a => HasFV (GRHSs GhcTc a) where
+  getFV GRHSs {grhssGRHSs = rhs, grhssLocalBinds = lbs} =
+    getFV rhs `Set.union` getFV lbs
+#if __GLASGOW_HASKELL__ < 900
+  getFV (XGRHSs e) = getFV e
+#endif
+
+
+instance HasFV (HsLocalBindsLR GhcTc GhcTc) where
+  getFV (HsValBinds _ bs) = getFV bs
+  getFV (HsIPBinds _ bs) = getFV bs
+  getFV EmptyLocalBinds {} = Set.empty
+#if __GLASGOW_HASKELL__ < 900
+  getFV (XHsLocalBindsLR e) = getFV e
+#endif
+  
+instance HasFV (HsValBindsLR GhcTc GhcTc) where
+  getFV (ValBinds _ b _) = getFV b
+  getFV (XValBindsLR b) = getFV b
+
+instance HasFV (NHsValBindsLR GhcTc) where
+  getFV (NValBinds bs _) = foldMap (getFV . snd) bs
+
+instance HasFV (HsBindLR GhcTc GhcTc) where
+  getFV FunBind {fun_matches = ms} = getFV ms
+  getFV PatBind {pat_rhs = rhs} = getFV rhs
+  getFV VarBind {var_rhs = rhs} = getFV rhs
+  getFV PatSynBind {} = Set.empty
+#if __GLASGOW_HASKELL__ < 904
+  getFV AbsBinds {abs_binds = bs} = getFV bs
+#else
+  getFV (XHsBindsLR AbsBinds {abs_binds = bs}) = getFV bs
+#endif
+#if __GLASGOW_HASKELL__ < 900
+  getFV (XHsBindsLR e) = getFV e
+#endif
+
+instance HasFV (IPBind GhcTc) where
+  getFV (IPBind _ _ e) = getFV e
+#if __GLASGOW_HASKELL__ < 900
+  getFV (XIPBind e) = getFV e
+#endif
+
+instance HasFV (HsIPBinds GhcTc) where
+  getFV (IPBinds _ bs) = getFV bs
+#if __GLASGOW_HASKELL__ < 900
+  getFV (XHsIPBinds e) = getFV e
+#endif
+  
+instance HasFV (ApplicativeArg GhcTc) where
+#if __GLASGOW_HASKELL__ >= 810
+  getFV ApplicativeArgOne { arg_expr = e }     = getFV e
+  getFV ApplicativeArgMany {app_stmts = es, final_expr = e} = getFV es `Set.union` getFV e
+#else
+  getFV (ApplicativeArgOne _ _ e _) = getFV e
+  getFV (ApplicativeArgMany _ es e _) = getFV es `Set.union` getFV e
+#endif
+#if __GLASGOW_HASKELL__ < 900
+  getFV (XApplicativeArg e) = getFV e
+#endif
+
+instance HasFV (ParStmtBlock GhcTc GhcTc) where
+  getFV (ParStmtBlock _ es _ _) = getFV es
+#if __GLASGOW_HASKELL__ < 900
+  getFV (XParStmtBlock e) = getFV e
+#endif
+  
+instance HasFV a => HasFV (StmtLR GhcTc GhcTc a) where
+  getFV (LastStmt _ e _ _) = getFV e
+#if __GLASGOW_HASKELL__ >= 900
+  getFV (BindStmt _ _ e) = getFV e
+#else
+  getFV (BindStmt _ _ e _ _) = getFV e
+#endif
+  getFV (ApplicativeStmt _ args _) = foldMap (getFV . snd) args
+  getFV (BodyStmt _ e _ _) = getFV e
+  getFV (LetStmt _ bs) = getFV bs
+  getFV (ParStmt _ stms e _) = getFV stms `Set.union` getFV e
+  getFV TransStmt{} = Set.empty -- TODO
+  getFV RecStmt{} = Set.empty -- TODO
+#if __GLASGOW_HASKELL__ < 900
+  getFV (XStmtLR e) = getFV e
+#endif
+
+#if __GLASGOW_HASKELL__ >= 902
+instance HasFV (HsRecFields GhcTc (GenLocated SrcSpanAnnA (HsExpr GhcTc))) where
+#else
+instance HasFV (HsRecordBinds GhcTc) where
+#endif
+  getFV HsRecFields{rec_flds = fs} = getFV fs
+
+#if __GLASGOW_HASKELL__ >= 904
+instance HasFV (HsFieldBind o (GenLocated SrcSpanAnnA (HsExpr GhcTc))) where
+#elif __GLASGOW_HASKELL__ >= 902
+instance HasFV (HsRecField' o (GenLocated SrcSpanAnnA (HsExpr GhcTc))) where
+#else
+instance HasFV (HsRecField' o (LHsExpr GhcTc)) where
+#endif
+  getFV rf  = getFV (getRecFieldRhs rf)
+
+instance HasFV (ArithSeqInfo GhcTc) where
+  getFV (From e) = getFV e
+  getFV (FromThen e1 e2) = getFV e1 `Set.union` getFV e2
+  getFV (FromTo e1 e2) = getFV e1 `Set.union` getFV e2
+  getFV (FromThenTo e1 e2 e3) = getFV e1 `Set.union` getFV e2 `Set.union` getFV e3
+  
+#if __GLASGOW_HASKELL__ >= 904
+instance HasFV (HsQuote GhcTc) where
+#else
+instance HasFV (HsBracket GhcTc) where
+#endif
+  getFV (ExpBr _ e) = getFV e
+  getFV (VarBr _ _ e) = getFV e
+  getFV _ = Set.empty
+
+instance HasFV (HsCmd GhcTc) where
+  getFV (HsCmdArrApp _ e1 e2 _ _) = getFV e1 `Set.union` getFV e2
+  getFV (HsCmdArrForm _ e _ _ cmd) = getFV e `Set.union` getFV cmd
+  getFV (HsCmdApp _ e1 e2) = getFV e1 `Set.union` getFV e2
+  getFV (HsCmdLam _ l) = getFV l
+  getFV (HsCmdCase _ _ mg) = getFV mg
+  getFV (HsCmdIf _ _ e1 e2 e3) = getFV e1 `Set.union` getFV e2 `Set.union` getFV e3
+  getFV (HsCmdDo _ cmd) = getFV cmd
+#if __GLASGOW_HASKELL__ >= 904
+  getFV (HsCmdPar _ _ cmd _) = getFV cmd
+  getFV (HsCmdLet _ _ bs _ _) = getFV bs
+#else
+  getFV (HsCmdPar _ cmd) = getFV cmd
+  getFV (HsCmdLet _ bs _) = getFV bs
+#endif
+#if __GLASGOW_HASKELL__ >= 904
+  getFV (HsCmdLamCase _ _ mg) = getFV mg
+#elif __GLASGOW_HASKELL__ >= 900
+  getFV (HsCmdLamCase _ mg) = getFV mg
+#else
+  getFV (HsCmdWrap _ _ cmd) = getFV cmd
+#endif
+  getFV (XCmd e) = getFV e
+  
+
+instance HasFV (HsCmdTop GhcTc) where
+  getFV (HsCmdTop _ cmd) = getFV cmd
+#if __GLASGOW_HASKELL__ < 900
+  getFV (XCmdTop e) = getFV e
+#endif
+
+instance HasFV (HsExpr GhcTc) where
+  getFV (HsVar _ v) = getFV v
+  getFV HsUnboundVar {} = Set.empty
+  getFV HsOverLabel {} = Set.empty
+  getFV HsIPVar {} = Set.empty
+  getFV HsOverLit {} = Set.empty
+  getFV HsLit {} = Set.empty
+  getFV (HsLam _ mg) = getFV mg
+  getFV (HsApp _ e1 e2) = getFV e1 `Set.union` getFV e2      
+  getFV (OpApp _ e1 e2 e3) = getFV e1 `Set.union` getFV e2 `Set.union` getFV e3
+  getFV (NegApp _ e _) = getFV e
+  getFV (SectionL _ e1 e2) = getFV e1 `Set.union` getFV e2
+  getFV (SectionR _ e1 e2) = getFV e1 `Set.union` getFV e2
+  getFV (ExplicitTuple _ es _) = getFV es
+  getFV (ExplicitSum _ _ _ e) = getFV e
+  getFV (HsCase _ e mg) = getFV e  `Set.union` getFV mg
+  getFV (HsMultiIf _ es) = getFV es
+  getFV (HsDo _ _ e) = getFV e
+#if __GLASGOW_HASKELL__ >= 902
+  getFV HsProjection {} = Set.empty
+  getFV HsGetField {gf_expr = e} = getFV e
+  getFV (ExplicitList _ es) = getFV es
+  getFV (RecordUpd {rupd_expr = e, rupd_flds = fs}) =
+    getFV e `Set.union` either getFV getFV fs
+#else
+  getFV (ExplicitList _ _ es) = getFV es
+  getFV (RecordUpd {rupd_expr = e, rupd_flds = fs}) = getFV e `Set.union` getFV fs
+#endif
+  getFV (RecordCon {rcon_flds = fs}) = getFV fs
+  getFV (ArithSeq _ _ e) = getFV e
+#if __GLASGOW_HASKELL__ >= 906
+  getFV HsTypedSplice{} = Set.empty
+  getFV HsUntypedSplice{} = Set.empty
+#else
+  getFV HsSpliceE{} = Set.empty
+#endif
+  getFV (HsProc _ _ e) = getFV e
+  getFV (HsStatic _ e) = getFV e
+  getFV (XExpr e) = getFV e
+#if __GLASGOW_HASKELL__ >= 904
+  getFV (HsPar _ _ e _) = getFV e  
+  getFV (HsLamCase _ _ mg) = getFV mg
+  getFV (HsLet _ _ bs _ e) = getFV bs `Set.union` getFV e
+  getFV HsRecSel {} = Set.empty
+  getFV (HsTypedBracket _ e) = getFV e
+  getFV (HsUntypedBracket _ e) = getFV e
+#else  
+  getFV (HsBinTick _ _ _ e) = getFV e
+  getFV (HsTick _ _ e) = getFV e
+  getFV (HsLet _ bs e) = getFV bs `Set.union` getFV e
+  getFV (HsPar _ e) = getFV e
+  getFV (HsLamCase _ mg) = getFV mg
+  getFV HsConLikeOut {} = Set.empty
+  getFV HsRecFld {} = Set.empty
+  getFV (HsBracket _ e) = getFV e
+  getFV HsRnBracketOut {} = Set.empty
+  getFV HsTcBracketOut {} = Set.empty
+#endif
+
+#if __GLASGOW_HASKELL__ >= 906
+  getFV (HsAppType _ e _ _) = getFV e
+  getFV (ExprWithTySig _ e _) = getFV e  
+#elif __GLASGOW_HASKELL__ >= 808
+  getFV (HsAppType _ e _) = getFV e
+  getFV (ExprWithTySig _ e _) = getFV e  
+#else
+  getFV (ExprWithTySig _ e)   = getFV e
+  getFV (HsAppType _ e)   = getFV e
+#endif
+
+#if __GLASGOW_HASKELL__ >= 900
+  getFV (HsIf _ e1 e2 e3) = getFV e1 `Set.union` getFV e2 `Set.union` getFV e3
+  getFV (HsPragE _ _ e) = getFV e
+#else
+  getFV (HsIf _ _ e1 e2 e3) = getFV e1 `Set.union` getFV e2 `Set.union` getFV e3
+  getFV (HsSCC _ _ _ e) = getFV e
+  getFV (HsCoreAnn _ _ _ e) = getFV e
+  getFV (HsTickPragma _ _ _ _ e) = getFV e
+  getFV (HsWrap _ _ e) = getFV e
+#endif
+
+#if __GLASGOW_HASKELL__ < 810  
+  getFV (HsArrApp _ e1 e2 _ _) = getFV e1 `Set.union` getFV e2
+  getFV (HsArrForm _ e _ cmd) = getFV e `Set.union` getFV cmd
+  getFV EWildPat {} = Set.empty
+  getFV (EAsPat _ e1 e2) = getFV e1 `Set.union` getFV e2
+  getFV (EViewPat _ e1 e2) = getFV e1 `Set.union` getFV e2
+  getFV (ELazyPat _ e) = getFV e
+#endif
+
+
+#if __GLASGOW_HASKELL__ >= 900
+instance HasFV XXExprGhcTc where
+  getFV (WrapExpr e) = getFV e
+  getFV (ExpansionExpr (HsExpanded _e1 e2)) = getFV e2
+#if __GLASGOW_HASKELL__ >= 904  
+  getFV (HsTick _ e) = getFV e
+  getFV (HsBinTick _ _ e) = getFV e
+  getFV ConLikeTc{} = Set.empty
+#endif
+
+
+instance HasFV (e GhcTc) => HasFV (HsWrap e) where
+  getFV (HsWrap _ e) = getFV e
+#elif __GLASGOW_HASKELL__ >= 810
+instance HasFV NoExtCon where
+  getFV _ = Set.empty
+#else
+instance HasFV NoExt where
+  getFV _ = Set.empty
+#endif
diff --git a/src/AsyncRattus/Plugin/PrimExpr.hs b/src/AsyncRattus/Plugin/PrimExpr.hs
new file mode 100644
--- /dev/null
+++ b/src/AsyncRattus/Plugin/PrimExpr.hs
@@ -0,0 +1,110 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module AsyncRattus.Plugin.PrimExpr (
+    Prim (..),
+    PrimInfo (..),
+    function,
+    prim,
+    isPrimExpr
+) where
+
+import Data.Map (Map)
+import qualified Data.Map as Map
+import GHC.Plugins
+import AsyncRattus.Plugin.Utils
+import Prelude hiding ((<>))
+
+data Prim = Delay | Adv | Box | Select
+
+-- DelayApp has the following fields: Var = delay f, T1 = value type, T2 = later type (O v a)
+-- AdvApp has the following fields: Var = adv f, TypedArg = var and type for arg
+data PrimInfo = DelayApp Var Type | AdvApp Var TypedArg | BoxApp Var | SelectApp Var TypedArg TypedArg
+
+type TypedArg = (Var, Type)
+
+data PartialPrimInfo = PartialPrimInfo {
+  primPart :: Prim,
+  functionPart :: Var,
+  args :: [Var],
+  typeArgs :: [Type]
+}
+
+instance Outputable PartialPrimInfo where
+  ppr (PartialPrimInfo Delay f _ typeArgs) = text "PartialPrimInfo { prim = Delay, function = " <> ppr f <> text "args = (not printing since it should be undefined) , typeArgs = " <> ppr typeArgs 
+  ppr (PartialPrimInfo prim f args typeArgs) = text "PartialPrimInfo { prim = " <> ppr prim <> text ", function = " <> ppr f <> text ", args = " <> ppr args <> text ", typeArgs = " <> ppr typeArgs
+
+instance Outputable Prim where
+  ppr Delay = "delay"
+  ppr Adv = "adv"
+  ppr Select = "select"
+  ppr Box = "box"
+
+instance Outputable PrimInfo where
+  ppr (DelayApp f _) = text "DelayApp - function " <> ppr f 
+  ppr (BoxApp f) = text "BoxApp - function " <> ppr f
+  ppr (AdvApp f arg) = text "AdvApp - function " <> ppr f <> text " | arg " <> ppr arg
+  ppr (SelectApp f arg arg2) = text "SelectApp - function " <> ppr f <> text " | arg " <> ppr arg <> text " | arg2 " <> ppr arg2
+  
+primMap :: Map FastString Prim
+primMap = Map.fromList
+  [("delay", Delay),
+   ("adv", Adv),
+   ("select", Select),
+   ("box", Box)
+   ]
+
+
+isPrim :: Var -> Maybe Prim
+isPrim v = case getNameModule v of
+    Just (name, mod) | isRattModule mod -> Map.lookup name primMap
+    _ -> Nothing
+
+createPartialPrimInfo :: Prim -> Var -> PartialPrimInfo
+createPartialPrimInfo prim function =
+  PartialPrimInfo {
+    primPart = prim,
+    functionPart = function,
+    args = [],
+    typeArgs = []
+  }
+
+function :: PrimInfo -> Var
+function (DelayApp f _) = f
+function (BoxApp f) = f
+function (AdvApp f _) = f
+function (SelectApp f _ _) = f
+
+prim :: PrimInfo -> Prim
+prim (DelayApp {}) = Delay
+prim (BoxApp _) = Box
+prim (AdvApp {}) = Adv
+prim (SelectApp {}) = Select
+
+validatePartialPrimInfo :: PartialPrimInfo -> Maybe PrimInfo
+validatePartialPrimInfo (PartialPrimInfo Select f [arg2V, argV] [arg2T, argT]) = Just $ SelectApp f (argV, argT) (arg2V, arg2T)
+validatePartialPrimInfo (PartialPrimInfo Delay f [_] [argT]) = Just $ DelayApp f argT
+validatePartialPrimInfo (PartialPrimInfo {primPart = Box, functionPart = f}) = Just $ BoxApp f
+validatePartialPrimInfo (PartialPrimInfo Adv f [argV] [argT]) = Just $ AdvApp f (argV, argT)
+validatePartialPrimInfo _ = Nothing
+
+isPrimExpr :: Expr Var -> Maybe PrimInfo
+isPrimExpr expr = isPrimExpr' expr >>= validatePartialPrimInfo
+
+-- App (App (App (App f type) arg) Type2) arg2
+isPrimExpr' :: Expr Var -> Maybe PartialPrimInfo
+isPrimExpr' (App e (Type t)) = case mPPI of
+  Just pPI@(PartialPrimInfo {typeArgs = tArgs}) -> Just pPI {typeArgs = t : tArgs}
+  Nothing -> Nothing
+  where mPPI = isPrimExpr' e
+isPrimExpr' (App e e') =
+  case isPrimExpr' e of
+    Just partPrimInfo@(PartialPrimInfo { primPart = Delay, args = args}) -> Just partPrimInfo {args = undefined : args}
+    Just partPrimInfo@(PartialPrimInfo { args = args}) -> Just partPrimInfo {args = maybe args (:args) (getMaybeVar e')}
+    _ -> Nothing
+isPrimExpr' (Var v) = case isPrim v of
+  Just p ->  Just $ createPartialPrimInfo p v
+  Nothing -> Nothing
+isPrimExpr' (Tick _ e) = isPrimExpr' e
+isPrimExpr' (Lam v e)
+  | isTyVar v || (not $ tcIsLiftedTypeKind $ typeKind $ varType v) = isPrimExpr' e
+isPrimExpr' _ = Nothing
diff --git a/src/AsyncRattus/Plugin/ScopeCheck.hs b/src/AsyncRattus/Plugin/ScopeCheck.hs
new file mode 100644
--- /dev/null
+++ b/src/AsyncRattus/Plugin/ScopeCheck.hs
@@ -0,0 +1,963 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE CPP #-}
+
+
+
+-- | This module implements the source plugin that checks the variable
+-- scope of of Async Rattus programs.
+
+module AsyncRattus.Plugin.ScopeCheck (checkAll) where
+
+import AsyncRattus.Plugin.Utils
+import AsyncRattus.Plugin.Dependency
+import AsyncRattus.Plugin.Annotation
+
+import Control.Monad.Trans.State.Strict
+import Data.IORef
+
+import Prelude hiding ((<>))
+
+#if __GLASGOW_HASKELL__ >= 902
+import GHC.Parser.Annotation
+#endif
+
+#if __GLASGOW_HASKELL__ >= 900
+import GHC.Plugins
+import GHC.Tc.Types
+import GHC.Data.Bag
+import GHC.Tc.Types.Evidence
+#else
+import GhcPlugins
+import TcRnTypes
+import TcEvidence
+import Bag
+#endif
+
+#if __GLASGOW_HASKELL__ >= 810
+import GHC.Hs.Extension
+import GHC.Hs.Expr
+import GHC.Hs.Pat
+import GHC.Hs.Binds
+#else 
+import HsExtension
+import HsExpr
+import HsPat
+import HsBinds
+#endif
+
+import Data.Graph
+import qualified Data.Set as Set
+import qualified Data.Map as Map
+import Data.Set (Set)
+import Data.Map (Map)
+import Data.List
+import Data.List.NonEmpty (NonEmpty(..),(<|),nonEmpty)
+import System.Exit
+import Data.Either
+import Data.Maybe
+
+import Data.Data hiding (tyConName)
+
+import Control.Monad
+
+type ErrorMsg = (Severity,SrcSpan,SDoc)
+type ErrorMsgsRef = IORef [ErrorMsg]
+
+-- | The current context for scope checking
+data Ctxt = Ctxt
+  {
+    errorMsgs :: ErrorMsgsRef,
+    -- | Variables that are in scope now (i.e. occurring in the typing
+    -- context but not to the left of a tick)
+    current :: LCtxt,
+    -- | Variables that are in the typing context, but to the left of a
+    -- tick
+    earlier :: Either NoTickReason (NonEmpty LCtxt),
+    -- | Variables that have fallen out of scope. The map contains the
+    -- reason why they have fallen out of scope.
+    hidden :: Hidden,
+    -- -- | Same as 'hidden' but for recursive variables.
+    -- hiddenRec :: Hidden,
+    -- | The current location information.
+    srcLoc :: SrcSpan,
+    -- | If we are in the body of a recursively defined function, this
+    -- field contains the variables that are defined recursively
+    -- (could be more than one due to mutual recursion or because of a
+    -- recursive pattern definition) and the location of the recursive
+    -- definition.
+    recDef :: Maybe RecDef,
+    -- | Type variables with a 'Stable' constraint attached to them.
+    stableTypes :: Set Var,
+    -- | A mapping from variables to the primitives that they are
+    -- defined equal to. For example, a program could contain @let
+    -- mydel = delay in mydel 1@, in which case @mydel@ is mapped to
+    -- 'Delay'.
+    primAlias :: Map Var Prim,
+    -- | Allow general recursion.
+    allowRecursion :: Bool}
+
+
+
+-- | The starting context for checking a top-level definition. For
+-- non-recursive definitions, the argument is @Nothing@. Otherwise, it
+-- contains the recursively defined variables along with the location
+-- of the recursive definition.
+emptyCtxt :: ErrorMsgsRef -> Maybe (Set Var,SrcSpan) -> Bool -> Ctxt
+emptyCtxt em mvar allowRec =
+  Ctxt { errorMsgs = em,
+         current =  Set.empty,
+         earlier = Left NoDelay,
+         hidden = Map.empty,
+         srcLoc = noLocationInfo,
+         recDef = mvar,
+         primAlias = Map.empty,
+         stableTypes = Set.empty,
+         allowRecursion = allowRec}
+
+-- | A local context, consisting of a set of variables.
+type LCtxt = Set Var
+
+-- | The recursively defined variables + the position where the
+-- recursive definition starts
+type RecDef = (Set Var, SrcSpan)
+
+
+
+
+data StableReason = StableRec SrcSpan | StableBox deriving Show
+
+-- | Indicates, why a variable has fallen out of scope.
+data HiddenReason = Stabilize StableReason | FunDef | DelayApp | AdvApp | SelectApp deriving Show
+
+-- | Indicates, why there is no tick
+data NoTickReason = NoDelay | TickHidden HiddenReason deriving Show
+
+-- | Hidden context, containing variables that have fallen out of
+-- context along with the reason why they have.
+type Hidden = Map Var HiddenReason
+
+-- | The 5 primitive Asynchronous Rattus operations.
+data Prim = Delay | Adv | Select | Box | Unbox deriving Show
+
+-- | This constraint is used to pass along the context implicitly via
+-- an implicit parameter.
+type GetCtxt = ?ctxt :: Ctxt
+
+
+type CheckM = StateT ([Maybe (Prim, SrcSpan)]) TcM
+
+-- | This type class is implemented for each AST type @a@ for which we
+-- can check whether it adheres to the scoping rules of Asynchronous Rattus.
+class Scope a where
+  -- | Check whether the argument is a scope correct piece of syntax
+  -- in the given context.
+  check :: GetCtxt => a -> CheckM Bool
+
+-- | This is a variant of 'Scope' for syntax that can also bind
+-- variables.
+class ScopeBind a where
+  -- | 'checkBind' checks whether its argument is scope-correct and in
+  -- addition returns the the set of variables bound by it.
+  checkBind :: GetCtxt => a -> CheckM (Bool,Set Var)
+
+
+-- | set the current context.
+setCtxt :: Ctxt -> (GetCtxt => a) -> a 
+setCtxt c a = let ?ctxt = c in a
+
+
+-- | modify the current context.
+modifyCtxt :: (Ctxt -> Ctxt) -> (GetCtxt => a) -> (GetCtxt => a)
+modifyCtxt f a =
+  let newc = f ?ctxt in
+  let ?ctxt = newc in a
+
+
+
+#if __GLASGOW_HASKELL__ >= 902
+getLocAnn' :: SrcSpanAnn' b -> SrcSpan
+getLocAnn' = locA
+
+
+updateLoc :: SrcSpanAnn' b -> (GetCtxt => a) -> (GetCtxt => a)
+updateLoc src = modifyCtxt (\c -> c {srcLoc = getLocAnn' src})
+
+#else
+getLocAnn' :: SrcSpan -> SrcSpan
+getLocAnn' s = s
+
+
+updateLoc :: SrcSpan -> (GetCtxt => a) -> (GetCtxt => a)
+updateLoc src = modifyCtxt (\c -> c {srcLoc = src})
+#endif
+
+-- | Check all definitions in the given module. If Scope errors are
+-- found, the current execution is halted with 'exitFailure'.
+checkAll :: TcGblEnv -> TcM ()
+checkAll env = do
+  let dep = dependency (tcg_binds env)
+  let bindDep = filter (filterBinds (tcg_mod env) (tcg_ann_env env)) dep
+  result <- mapM (checkSCC' (tcg_mod env) (tcg_ann_env env)) bindDep
+  let (res,msgs) = foldl' (\(b,l) (b',l') -> (b && b', l ++ l')) (True,[]) result
+  printAccErrMsgs msgs
+  if res then return () else liftIO exitFailure
+
+
+printAccErrMsgs :: [ErrorMsg] -> TcM ()
+printAccErrMsgs msgs = mapM_ printMsg (sortOn (\(_,l,_)->l) msgs)
+  where printMsg (sev,loc,doc) = printMessage sev loc doc
+
+
+-- | This function checks whether a given top-level definition (either
+-- a single non-recursive definition or a group of mutual recursive
+-- definitions) is marked as Asynchronous Rattus code (via an annotation). In a
+-- group of mutual recursive definitions, the whole group is
+-- considered Asynchronous Rattus code if at least one of its constituents is
+-- marked as such.
+filterBinds :: Module -> AnnEnv -> SCC (LHsBindLR  GhcTc GhcTc, Set Var) -> Bool
+filterBinds mod anEnv scc =
+  case scc of
+    (AcyclicSCC (_,vs)) -> any checkVar vs
+    (CyclicSCC bs) -> any (any checkVar . snd) bs
+  where checkVar :: Var -> Bool
+        checkVar v =
+          let anns = findAnns deserializeWithData anEnv (NamedTarget name) :: [AsyncRattus]
+              annsMod = findAnns deserializeWithData anEnv (ModuleTarget mod) :: [AsyncRattus]
+              name :: Name
+              name = varName v
+          in AsyncRattus `elem` anns || (not (NotAsyncRattus `elem` anns)  && AsyncRattus `elem` annsMod)
+
+
+
+instance Scope a => Scope (GenLocated SrcSpan a) where
+  check (L l x) =  (\c -> c {srcLoc = l}) `modifyCtxt` check x
+
+
+#if __GLASGOW_HASKELL__ >= 902
+instance Scope a => Scope (GenLocated (SrcSpanAnn' b) a) where
+  check (L l x) =  updateLoc l $ check x
+#endif
+
+  
+instance Scope a => Scope (Bag a) where
+  check bs = fmap and (mapM check (bagToList bs))
+
+instance Scope a => Scope [a] where
+  check ls = fmap and (mapM check ls)
+
+
+instance Scope (Match GhcTc (GenLocated SrcAnno (HsExpr GhcTc))) where
+  check Match{m_pats=ps,m_grhss=rhs} = addVars (getBV ps) `modifyCtxt` check rhs
+#if __GLASGOW_HASKELL__ < 900
+  check XMatch{} = return True
+#endif
+
+instance Scope (Match GhcTc (GenLocated SrcAnno (HsCmd GhcTc))) where
+  check Match{m_pats=ps,m_grhss=rhs} = addVars (getBV ps) `modifyCtxt` check rhs
+#if __GLASGOW_HASKELL__ < 900
+  check XMatch{} = return True
+#endif
+
+
+instance Scope (MatchGroup GhcTc (GenLocated SrcAnno (HsExpr GhcTc))) where
+  check MG {mg_alts = alts} = check alts
+#if __GLASGOW_HASKELL__ < 900
+  check XMatchGroup {} = return True
+#endif
+
+
+instance Scope (MatchGroup GhcTc (GenLocated SrcAnno (HsCmd GhcTc))) where
+  check MG {mg_alts = alts} = check alts
+#if __GLASGOW_HASKELL__ < 900
+  check XMatchGroup {} = return True
+#endif
+
+
+instance Scope a => ScopeBind (StmtLR GhcTc GhcTc a) where
+  checkBind (LastStmt _ b _ _) =  ( , Set.empty) <$> check b
+#if __GLASGOW_HASKELL__ >= 900
+  checkBind (BindStmt _ p b) = do
+#else
+  checkBind (BindStmt _ p b _ _) = do
+#endif
+    let vs = getBV p
+    let c' = addVars vs ?ctxt
+    r <- setCtxt c' (check b)
+    return (r,vs)
+  checkBind (BodyStmt _ b _ _) = ( , Set.empty) <$> check b
+  checkBind (LetStmt _ bs) = checkBind bs
+  checkBind ParStmt{} = notSupported "monad comprehensions"
+  checkBind TransStmt{} = notSupported "monad comprehensions"
+  checkBind ApplicativeStmt{} = notSupported "applicative do notation"
+  checkBind RecStmt{} = notSupported "recursive do notation"
+#if __GLASGOW_HASKELL__ < 900
+  checkBind XStmtLR {} = return (True,Set.empty)
+#endif
+
+instance ScopeBind a => ScopeBind [a] where
+  checkBind [] = return (True,Set.empty)
+  checkBind (x:xs) = do
+    (r,vs) <- checkBind x
+    (r',vs') <- addVars vs `modifyCtxt` (checkBind xs)
+    return (r && r',vs `Set.union` vs')
+
+instance ScopeBind a => ScopeBind (GenLocated SrcSpan a) where
+  checkBind (L l x) =  (\c -> c {srcLoc = l}) `modifyCtxt` checkBind x
+
+#if __GLASGOW_HASKELL__ >= 902
+instance ScopeBind a => ScopeBind (GenLocated (SrcSpanAnn' b) a) where
+  checkBind (L l x) =  updateLoc l $ checkBind x
+#endif
+
+instance Scope a => Scope (GRHS GhcTc a) where
+  check (GRHS _ gs b) = do
+    (r, vs) <- checkBind gs
+    r' <- addVars vs `modifyCtxt`  (check b)
+    return (r && r')
+#if __GLASGOW_HASKELL__ < 900
+  check XGRHS{} = return True
+#endif
+
+checkRec :: GetCtxt => LHsBindLR GhcTc GhcTc -> CheckM Bool
+checkRec b =  liftM2 (&&) (checkPatBind b) (check b)
+
+checkPatBind :: GetCtxt => LHsBindLR GhcTc GhcTc -> CheckM Bool
+checkPatBind (L l b) = updateLoc l $ checkPatBind' b
+
+checkPatBind' :: GetCtxt => HsBindLR GhcTc GhcTc -> CheckM Bool
+checkPatBind' PatBind{} = do
+  printMessage' SevError ("(Mutual) recursive pattern binding definitions are not supported in Asynchronous Rattus")
+  return False
+#if __GLASGOW_HASKELL__ < 904
+checkPatBind' AbsBinds {abs_binds = binds} = 
+#else
+checkPatBind' (XHsBindsLR AbsBinds {abs_binds = binds}) = 
+#endif
+  liftM and (mapM checkPatBind (bagToList binds))
+
+checkPatBind' _ = return True
+
+
+-- | Check the scope of a list of (mutual) recursive bindings. The
+-- second argument is the set of variables defined by the (mutual)
+-- recursive bindings
+checkRecursiveBinds :: GetCtxt => [LHsBindLR GhcTc GhcTc] -> Set Var -> CheckM (Bool, Set Var)
+checkRecursiveBinds bs vs = do
+    res <- fmap and (mapM check' bs)
+    return (res, vs)
+    where check' b@(L l _) = fc (getLocAnn' l) `modifyCtxt` checkRec b
+          fc l c = let
+            ctxHid = either (const $ current c) (Set.union (current c) . Set.unions) (earlier c)
+            in c {current = Set.empty,
+                  earlier = Left (TickHidden $ Stabilize $ StableRec l),
+                  hidden =  hidden c `Map.union`
+                            (Map.fromSet (const (Stabilize (StableRec l))) ctxHid),
+                  recDef = maybe (Just (vs,l)) (\(vs',_) -> Just (Set.union vs' vs,l)) (recDef c)
+                   -- TODO fix location info of recDef (needs one location for each var)
+                   }          
+
+
+#if __GLASGOW_HASKELL__ >= 902
+instance ScopeBind (SCC (GenLocated SrcSpanAnnA (HsBindLR  GhcTc GhcTc), Set Var)) where
+#else
+instance ScopeBind (SCC (LHsBindLR GhcTc GhcTc, Set Var)) where
+#endif
+  checkBind (AcyclicSCC (b,vs)) = (, vs) <$> check b
+  checkBind (CyclicSCC bs) = checkRecursiveBinds (map fst bs) (foldMap snd bs)
+  
+instance ScopeBind (HsValBindsLR GhcTc GhcTc) where
+  checkBind (ValBinds _ bs _) = checkBind (dependency bs)
+  
+  checkBind (XValBindsLR (NValBinds binds _)) = checkBind binds
+
+
+instance ScopeBind (HsBindLR GhcTc GhcTc) where
+  checkBind b = (, getBV b) <$> check b
+
+
+-- | Compute the set of variables defined by the given Haskell binder.
+getAllBV :: GenLocated l (HsBindLR GhcTc GhcTc) -> Set Var
+getAllBV (L _ b) = getAllBV' b where
+  getAllBV' (FunBind{fun_id = L _ v}) = Set.singleton v
+#if __GLASGOW_HASKELL__ < 904
+  getAllBV' (AbsBinds {abs_exports = es, abs_binds = bs}) = Set.fromList (map abe_poly es) `Set.union` foldMap getBV bs
+  getAllBV' XHsBindsLR{} = Set.empty
+#else
+  getAllBV' (XHsBindsLR (AbsBinds {abs_exports = es, abs_binds = bs})) = Set.fromList (map abe_poly es) `Set.union` foldMap getBV bs
+#endif
+  getAllBV' (PatBind {pat_lhs = pat}) = getBV pat
+  getAllBV' (VarBind {var_id = v}) = Set.singleton v
+  getAllBV' PatSynBind{} = Set.empty
+
+
+-- Check nested bindings
+#if __GLASGOW_HASKELL__ >= 902
+instance ScopeBind (RecFlag, Bag (GenLocated SrcSpanAnnA (HsBindLR GhcTc GhcTc))) where
+#else
+instance ScopeBind (RecFlag, LHsBinds GhcTc) where
+#endif
+  checkBind (NonRecursive, bs)  = checkBind $ bagToList bs
+  checkBind (Recursive, bs) = checkRecursiveBinds bs' (foldMap getAllBV bs')
+    where bs' = bagToList bs
+
+
+instance ScopeBind (HsLocalBindsLR GhcTc GhcTc) where
+  checkBind (HsValBinds _ bs) = checkBind bs
+  checkBind HsIPBinds {} = notSupported "implicit parameters"
+  checkBind EmptyLocalBinds{} = return (True,Set.empty)
+#if __GLASGOW_HASKELL__ < 900
+  checkBind XHsLocalBindsLR{} = return (True,Set.empty)
+#endif
+
+#if __GLASGOW_HASKELL__ >= 902
+type SrcAnno = SrcSpanAnnA
+#else
+type SrcAnno = SrcSpan
+#endif
+  
+instance Scope (GRHSs GhcTc (GenLocated SrcAnno (HsExpr GhcTc))) where
+  check GRHSs{grhssGRHSs = rhs, grhssLocalBinds = lbinds} = do
+    (l,vs) <- checkBind lbinds
+    r <- addVars vs `modifyCtxt` (check rhs)
+    return (r && l)
+#if __GLASGOW_HASKELL__ < 900
+  check XGRHSs{} = return True
+#endif
+
+instance Scope (GRHSs GhcTc (GenLocated SrcAnno (HsCmd GhcTc))) where
+  check GRHSs{grhssGRHSs = rhs, grhssLocalBinds = lbinds} = do
+    (l,vs) <- checkBind lbinds
+    r <- addVars vs `modifyCtxt` (check rhs)
+    return (r && l)
+#if __GLASGOW_HASKELL__ < 900
+  check XGRHSs{} = return True
+#endif
+
+instance Show Var where
+  show v = getOccString v
+
+
+tickHidden :: HiddenReason -> SDoc
+tickHidden FunDef = "a function definition"
+tickHidden DelayApp = "a nested application of delay"
+tickHidden AdvApp = "an application of adv"
+tickHidden SelectApp = "an application of select"
+tickHidden (Stabilize StableBox) = "an application of box"
+tickHidden (Stabilize (StableRec src)) = "a nested recursive definition (at " <> ppr src <> ")"
+
+isSelect :: GetCtxt => LHsExpr GhcTc -> Bool
+isSelect e =
+  case isPrimExpr e of
+    Just (Select, _) -> True
+    _ -> False
+
+instance Scope (HsExpr GhcTc) where
+  check (HsVar _ (L _ v))
+    | Just p <- isPrim v =
+        case p of
+          Unbox -> return True
+          _ -> printMessageCheck SevError ("Defining an alias for " <> ppr v <> " is not allowed")
+    | otherwise = case getScope v of
+             Hidden reason -> printMessageCheck SevError reason
+             Visible -> return True
+             ImplUnboxed -> return True
+               -- printMessageCheck SevWarning
+               --  (ppr v <> text " is an external temporal function used under delay, which may cause time leaks.")
+  check (HsApp _ (L _ (HsApp _ f arg)) arg2) | isSelect f =
+    case earlier ?ctxt of
+      Right (er :| ers) -> do
+        res <- get
+        case res of
+            Just _ : _ -> printMessageCheck SevError ("only one adv or select may be used in the scope of a delay.")
+            Nothing : pre -> do put pre
+                                b1 <- mod `modifyCtxt` check arg
+                                b2 <- mod `modifyCtxt` check arg2
+                                modify (Just (Select, srcLoc ?ctxt) :)
+                                return $ b1 && b2
+            _ -> error "Asynchronous Rattus: internal error"
+        where mod c =  c{earlier = case nonEmpty ers of
+                                    Nothing -> Left $ TickHidden SelectApp
+                                    Just ers' -> Right ers',
+                        current = er,
+                        hidden = hidden ?ctxt `Map.union`
+                        Map.fromSet (const SelectApp) (current ?ctxt)}
+      Left NoDelay -> printMessageCheck SevError "select may only be used in the scope of a delay."
+      Left (TickHidden hr) -> printMessageCheck SevError ("select may only be used in the scope of a delay. "
+                        <> " There is a delay, but its scope is interrupted by " <> tickHidden hr <> ".")
+  check (HsApp _ e1 e2) =
+    case isPrimExpr e1 of
+    Just (p,_) -> case p of
+      Box -> do
+        ch <- stabilize StableBox `modifyCtxt` check e2
+        return ch
+      Unbox -> check e2
+      Delay -> do modify (Nothing :)
+                  b <- (\c -> c{current = Set.empty,
+                           earlier = case earlier c of
+                                      Left _ -> Right (current c :| [])
+                                      Right cs -> Right (current c <| cs)})
+                     `modifyCtxt` check e2
+                  res <- get
+                  case res of
+                    Nothing : _ -> printMessageCheck SevError "No adv or select found in the scope of this occurrence of delay"
+                    _ : pre -> put pre >> return b
+                    _ -> error "Asynchronous Rattus: internal error"
+      Adv -> case earlier ?ctxt of
+        Right (er :| ers) -> do
+          res <- get
+          case res of
+            Just _ : _ -> printMessageCheck SevError ("only one adv or select may be used in the scope of a delay.")
+            Nothing : pre -> do put pre
+                                b <- mod `modifyCtxt` check e2
+                                modify (Just (Adv,srcLoc ?ctxt) :)
+                                return b
+            _ -> error "Asynchronous Rattus: internal error"
+          where mod c =  c{earlier = case nonEmpty ers of
+                                       Nothing -> Left $ TickHidden AdvApp
+                                       Just ers' -> Right ers',
+                           current = er,
+                           hidden = hidden ?ctxt `Map.union`
+                            Map.fromSet (const AdvApp) (current ?ctxt)}
+        Left NoDelay -> printMessageCheck SevError ("adv may only be used in the scope of a delay.")
+        Left (TickHidden hr) -> printMessageCheck SevError ("adv may only be used in the scope of a delay. "
+                            <> " There is a delay, but its scope is interrupted by " <> tickHidden hr <> ".")
+      Select -> printMessageCheck SevError ("select must be fully applied")
+    _ -> liftM2 (&&) (check e1)  (check e2)
+  check HsUnboundVar{}  = return True
+#if __GLASGOW_HASKELL__ >= 904
+  check (HsPar _ _ e _) = check e
+  check (HsLamCase _ _ mg) = check mg
+  check HsRecSel{} = return True
+  check HsTypedBracket{} = notSupported "MetaHaskell"
+  check HsUntypedBracket{} = notSupported "MetaHaskell"
+#else
+  check HsConLikeOut{} = return True
+  check HsRecFld{} = return True
+  check (HsPar _ e) = check e
+  check (HsLamCase _ mg) = check mg
+  check HsBracket{} = notSupported "MetaHaskell"
+  check (HsTick _ _ e) = check e
+  check (HsBinTick _ _ _ e) = check e
+  check HsRnBracketOut{} = notSupported "MetaHaskell"
+  check HsTcBracketOut{} = notSupported "MetaHaskell"
+#endif
+#if __GLASGOW_HASKELL__ >= 904
+  check (HsLet _ _ bs _ e) = do
+#else
+  check (HsLet _ bs e) = do
+#endif
+    (l,vs) <- checkBind bs
+    r <- addVars vs `modifyCtxt` (check e)
+    return (r && l)
+         
+  check HsOverLabel{} = return True
+  check HsIPVar{} = notSupported "implicit parameters"
+  check HsOverLit{} = return True  
+  check HsLit{} = return True
+  check (OpApp _ e1 e2 e3) = and <$> mapM check [e1,e2,e3]
+  check (HsLam _ mg) = check mg
+  check (HsCase _ e1 e2) = (&&) <$> check e1 <*> check e2
+  check (SectionL _ e1 e2) = (&&) <$> check e1 <*> check e2
+  check (SectionR _ e1 e2) = (&&) <$> check e1 <*> check e2
+  check (ExplicitTuple _ e _) = check e
+  check (NegApp _ e _) = check e
+  check (ExplicitSum _ _ _ e) = check e
+  check (HsMultiIf _ e) = check e
+#if __GLASGOW_HASKELL__ >= 902
+  check (ExplicitList _ e) = check e
+  check RecordUpd { rupd_expr = e, rupd_flds = fs} = (&&) <$> check e <*> either check check fs
+  check HsProjection {} = return True
+  check HsGetField {gf_expr = e} = check e
+#else
+  check (ExplicitList _ _ e) = check e
+  check RecordUpd { rupd_expr = e, rupd_flds = fs} = (&&) <$> check e <*> check fs
+#endif
+  check RecordCon { rcon_flds = f} = check f
+  check (ArithSeq _ _ e) = check e
+#if __GLASGOW_HASKELL__ >= 906
+  check HsTypedSplice{} = notSupported "Template Haskell"
+  check HsUntypedSplice{} = notSupported "Template Haskell"
+#else
+  check HsSpliceE{} = notSupported "Template Haskell"
+#endif
+  check (HsProc _ _ e) = check e
+  check (HsStatic _ e) = check e
+  check (HsDo _ _ e) = fst <$> checkBind e
+  check (XExpr e) = check e
+#if __GLASGOW_HASKELL__ >= 906
+  check (HsAppType _ e _ _) = check e
+  check (ExprWithTySig _ e _) = check e
+#elif __GLASGOW_HASKELL__ >= 808
+  check (HsAppType _ e _) = check e
+  check (ExprWithTySig _ e _) = check e
+#else
+  check (HsAppType _ e)  = check e
+  check (ExprWithTySig _ e) = check e
+#endif
+
+#if __GLASGOW_HASKELL__ >= 900
+  check (HsPragE _ _ e) = check e
+  check (HsIf _ e1 e2 e3) = and <$> mapM check [e1,e2,e3]
+#else
+  check (HsSCC _ _ _ e) = check e
+  check (HsCoreAnn _ _ _ e) = check e
+  check (HsTickPragma _ _ _ _ e) = check e
+  check (HsWrap _ _ e) = check e
+  check (HsIf _ _ e1 e2 e3) = and <$> mapM check [e1,e2,e3]
+#endif
+#if __GLASGOW_HASKELL__ < 810
+  check HsArrApp{} = impossible
+  check HsArrForm{} = impossible
+  check EWildPat{} = impossible
+  check EAsPat{} = impossible
+  check EViewPat{} = impossible
+  check ELazyPat{} = impossible
+
+impossible :: GetCtxt => TcM Bool
+impossible = printMessageCheck SevError "This syntax should never occur after typechecking"
+#endif
+
+#if __GLASGOW_HASKELL__ >= 900
+instance Scope XXExprGhcTc where
+  check (WrapExpr (HsWrap _ e)) = check e
+  check (ExpansionExpr (HsExpanded _ e)) = check e
+#if __GLASGOW_HASKELL__ >= 904
+  check ConLikeTc{} = return True
+  check (HsTick _ e) = check e
+  check (HsBinTick _ _ e) = check e
+#endif
+#elif __GLASGOW_HASKELL__ >= 810
+instance Scope NoExtCon where
+  check _ = return True
+#else
+instance Scope NoExt where
+  check _ = return True
+#endif
+
+instance Scope (HsCmdTop GhcTc) where
+  check (HsCmdTop _ e) = check e
+#if __GLASGOW_HASKELL__ < 900
+  check XCmdTop{} = return True
+#endif
+  
+instance Scope (HsCmd GhcTc) where
+  check (HsCmdArrApp _ e1 e2 _ _) = (&&) <$> check e1 <*> check e2
+  check (HsCmdDo _ e) = fst <$> checkBind e
+  check (HsCmdArrForm _ e1 _ _ e2) = (&&) <$> check e1 <*> check e2
+  check (HsCmdApp _ e1 e2) = (&&) <$> check e1 <*> check e2
+  check (HsCmdLam _ e) = check e
+#if __GLASGOW_HASKELL__ >= 904
+  check (HsCmdPar _ _ e _) = check e
+  check (HsCmdLamCase _ _ e) = check e  
+  check (HsCmdLet _ _ bs _ e) = do
+#else
+  check (HsCmdPar _ e) = check e
+#if __GLASGOW_HASKELL__ >= 900
+  check (HsCmdLamCase _ e) = check e
+#endif
+  check (HsCmdLet _ bs e) = do
+#endif
+    (l,vs) <- checkBind bs
+    r <- addVars vs `modifyCtxt` (check e)
+    return (r && l)
+
+  check (HsCmdCase _ e1 e2) = (&&) <$> check e1 <*> check e2
+  check (HsCmdIf _ _ e1 e2 e3) = (&&) <$> ((&&) <$> check e1 <*> check e2) <*> check e3
+#if __GLASGOW_HASKELL__ >= 900
+  check (XCmd (HsWrap _ e)) = check e
+#else
+  check (HsCmdWrap _ _ e) = check e
+  check XCmd{} = return True
+#endif
+
+
+instance Scope (ArithSeqInfo GhcTc) where
+  check (From e) = check e
+  check (FromThen e1 e2) = (&&) <$> check e1 <*> check e2
+  check (FromTo e1 e2) = (&&) <$> check e1 <*> check e2
+  check (FromThenTo e1 e2 e3) = (&&) <$> ((&&) <$> check e1 <*> check e2) <*> check e3
+
+instance Scope a => Scope (HsRecFields GhcTc a) where
+  check HsRecFields {rec_flds = fs} = check fs
+
+
+
+#if __GLASGOW_HASKELL__ >= 904
+instance Scope b => Scope (HsFieldBind a b) where
+  check HsFieldBind{hfbRHS = a} = check a
+#else
+instance Scope b => Scope (HsRecField' a b) where
+  check HsRecField{hsRecFieldArg = a} = check a
+#endif
+
+instance Scope (HsTupArg GhcTc) where
+  check (Present _ e) = check e
+  check Missing{} = return True
+#if __GLASGOW_HASKELL__ < 900
+  check XTupArg{} = return True
+#endif
+
+instance Scope (HsBindLR GhcTc GhcTc) where
+#if __GLASGOW_HASKELL__ >= 904
+  check (XHsBindsLR AbsBinds {abs_binds = binds, abs_ev_vars  = ev})
+#else
+  check AbsBinds {abs_binds = binds, abs_ev_vars  = ev}
+#endif
+    = mod `modifyCtxt` check binds
+      where mod c = c { stableTypes= stableTypes c `Set.union`
+                        Set.fromList (mapMaybe (isStableConstr . varType) ev)}
+  check FunBind{fun_matches= matches, fun_id = L _ v,
+#if __GLASGOW_HASKELL__ >= 900
+                fun_ext = wrapper} =
+#else
+                fun_co_fn = wrapper} =
+#endif
+      mod `modifyCtxt` check matches
+    where mod c = c { stableTypes= stableTypes c `Set.union`
+                      Set.fromList (stableConstrFromWrapper' wrapper)  `Set.union`
+                      Set.fromList (extractStableConstr (varType v))}
+  check PatBind{pat_lhs = lhs, pat_rhs=rhs} = addVars (getBV lhs) `modifyCtxt` check rhs
+  check VarBind{var_rhs = rhs} = check rhs
+  check PatSynBind {} = return True -- pattern synonyms are not supported
+#if __GLASGOW_HASKELL__ < 900
+  check XHsBindsLR {} = return True
+#endif
+
+
+-- | Checks whether the given type is a type constraint of the form
+-- @Stable a@ for some type variable @a@. In that case it returns the
+-- type variable @a@.
+isStableConstr :: Type -> Maybe TyVar
+isStableConstr t = 
+  case splitTyConApp_maybe t of
+    Just (con,[args]) ->
+      case getNameModule con of
+        Just (name, mod) ->
+          if isRattModule mod && name == "Stable"
+          then (getTyVar_maybe args)
+          else Nothing
+        _ -> Nothing                           
+    _ ->  Nothing
+
+
+
+#if __GLASGOW_HASKELL__ >= 906
+stableConstrFromWrapper' :: (HsWrapper , a) -> [TyVar]
+stableConstrFromWrapper' (x , _) = stableConstrFromWrapper x
+#else
+stableConstrFromWrapper' :: HsWrapper -> [TyVar]
+stableConstrFromWrapper' = stableConstrFromWrapper
+#endif
+
+stableConstrFromWrapper :: HsWrapper -> [TyVar]
+stableConstrFromWrapper (WpCompose v w) = stableConstrFromWrapper v ++ stableConstrFromWrapper w
+stableConstrFromWrapper (WpEvLam v) = maybeToList $ isStableConstr (varType v)
+stableConstrFromWrapper _ = []
+
+
+-- | Given a type @(C1, ... Cn) => t@, this function returns the list
+-- of type variables @[a1,...,am]@ for which there is a constraint
+-- @Stable ai@ among @C1, ... Cn@.
+extractStableConstr :: Type -> [TyVar]
+#if __GLASGOW_HASKELL__ >= 900
+extractStableConstr  = mapMaybe isStableConstr . map irrelevantMult . fst . splitFunTys . snd . splitForAllTys'
+#else
+extractStableConstr  = mapMaybe isStableConstr . fst . splitFunTys . snd . splitForAllTys'
+#endif
+
+
+getSCCLoc :: SCC (LHsBindLR  GhcTc GhcTc, Set Var) -> SrcSpan
+getSCCLoc (AcyclicSCC (L l _ ,_)) = getLocAnn' l
+getSCCLoc (CyclicSCC ((L l _,_ ) : _)) = getLocAnn' l
+getSCCLoc _ = noLocationInfo
+
+checkSCC' ::  Module -> AnnEnv -> SCC (LHsBindLR  GhcTc GhcTc, Set Var) -> TcM (Bool, [ErrorMsg])
+checkSCC' mod anEnv scc = do
+  err <- liftIO (newIORef [])
+  let allowRec = AllowRecursion `Set.member` getAnn mod anEnv scc
+  res <- checkSCC allowRec err scc
+  msgs <- liftIO (readIORef err)
+  let anns = getAnn mod anEnv scc
+  if ExpectWarning `Set.member` anns 
+    then if ExpectError `Set.member` anns
+         then return (False,[(SevError, getSCCLoc scc, "Annotation to expect both warning and error is not allowed.")])
+         else if any (\(s,_,_) -> case s of SevWarning -> True; _ -> False) msgs
+              then return (res, filter (\(s,_,_) -> case s of SevWarning -> False; _ -> True) msgs)
+              else return (False,[(SevError, getSCCLoc scc, "Warning was expected, but typechecking produced no warning.")])
+    else if ExpectError `Set.member` anns
+         then if res
+              then return (False,[(SevError, getSCCLoc scc, "Error was expected, but typechecking produced no error.")])
+              else return (True,[])
+         else return (res, msgs)
+getAnn :: forall a . (Data a, Ord a) => Module -> AnnEnv -> SCC (LHsBindLR  GhcTc GhcTc, Set Var) -> Set a
+getAnn mod anEnv scc =
+  case scc of
+    (AcyclicSCC (_,vs)) -> Set.unions $ Set.map checkVar vs
+    (CyclicSCC bs) -> Set.unions $ map (Set.unions . Set.map checkVar . snd) bs
+  where checkVar :: Var -> Set a
+        checkVar v =
+          let anns = findAnns deserializeWithData anEnv (NamedTarget name) :: [a]
+              annsMod = findAnns deserializeWithData anEnv (ModuleTarget mod) :: [a]
+              name :: Name
+              name = varName v
+          in Set.fromList anns `Set.union` Set.fromList annsMod
+
+
+
+-- | Checks a top-level definition group, which is either a single
+-- non-recursive definition or a group of (mutual) recursive
+-- definitions.
+
+checkSCC :: Bool -> ErrorMsgsRef -> SCC (LHsBindLR  GhcTc GhcTc, Set Var) -> TcM Bool
+checkSCC allowRec errm (AcyclicSCC (b,_)) = setCtxt (emptyCtxt errm Nothing allowRec) (evalStateT (check b) [])
+
+checkSCC allowRec errm (CyclicSCC bs) = (fmap and (mapM check' bs'))
+  where bs' = map fst bs
+        vs = foldMap snd bs
+        check' b@(L l _) = setCtxt (emptyCtxt errm (Just (vs,getLocAnn' l)) allowRec) (evalStateT (checkRec b) [])
+
+-- | Stabilizes the given context, i.e. remove all non-stable types
+-- and any tick. This is performed on checking 'box', and
+-- guarded recursive definitions. To provide better error messages a
+-- reason has to be given as well.
+stabilize :: StableReason -> Ctxt -> Ctxt
+stabilize sr c = c
+  {current = Set.empty,
+   earlier = Left $ TickHidden hr,
+   hidden = hidden c `Map.union` Map.fromSet (const hr) ctxHid}
+  where ctxHid = either (const $ current c) (foldl' Set.union (current c)) (earlier c)
+        hr = Stabilize sr
+
+data VarScope = Hidden SDoc | Visible | ImplUnboxed
+
+
+-- | This function checks whether the given variable is in scope.
+getScope  :: GetCtxt => Var -> VarScope
+getScope v =
+  case ?ctxt of
+    Ctxt{recDef = Just (vs,_), earlier = e, allowRecursion = allowRec} | v `Set.member` vs ->
+     if allowRec then Visible else
+        case e of
+          Right _ -> Visible
+          Left NoDelay -> Hidden ("The (mutually) recursive call to " <> ppr v <> " must occur in the scope of a delay")
+          Left (TickHidden hr) -> Hidden ("The (mutually) recursive call to " <> ppr v <> " must occur in the scope of a delay. "
+                            <> "There is a delay, but its scope is interrupted by " <> tickHidden hr <> ".")
+    _ ->  case Map.lookup v (hidden ?ctxt) of
+            Just (Stabilize (StableRec rv)) ->
+              if (isStable (stableTypes ?ctxt) (varType v)) || allowRecursion ?ctxt then Visible
+              else Hidden ("Variable " <> ppr v <> " is no longer in scope:" $$
+                       "It appears in a local recursive definition (at " <> ppr rv <> ")"
+                       $$ "and is of type " <> ppr (varType v) <> ", which is not stable.")
+            Just (Stabilize StableBox) ->
+              if (isStable (stableTypes ?ctxt) (varType v)) then Visible
+              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 SelectApp -> Hidden ("Variable " <> ppr v <> " is no longer in scope: It occurs under select.")
+            Just DelayApp -> Hidden ("Variable " <> ppr v <> " is no longer in scope due to repeated application of delay")
+            Just FunDef -> if (isStable (stableTypes ?ctxt) (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
+              | either (const False) (any (Set.member v)) (earlier ?ctxt) ->
+                if isStable (stableTypes ?ctxt) (varType v) then Visible
+                else Hidden ("Variable " <> ppr v <> " is no longer in scope:" $$
+                         "It occurs under delay" $$ "and is of type " <> ppr (varType v) <> ", which is not stable.")
+              | Set.member v (current ?ctxt) -> Visible
+              | isTemporal (varType v) && isRight (earlier ?ctxt) && userFunction v
+                -> ImplUnboxed
+              | otherwise -> Visible
+
+-- | A map from the syntax of a primitive of Asynchronous Rattus to 'Prim'.
+primMap :: Map FastString Prim
+primMap = Map.fromList
+  [("Delay", Delay),
+   ("delay", Delay),
+   ("adv", Adv),
+   ("select", Select),
+   ("box", Box),
+   ("unbox", Unbox)]
+
+
+-- | Checks whether a given variable is in fact an Asynchronous Rattus primitive.
+isPrim :: GetCtxt => Var -> Maybe Prim
+isPrim v
+  | Just p <- Map.lookup v (primAlias ?ctxt) = Just p
+  | otherwise = do
+  (name,mod) <- getNameModule v
+  if isRattModule mod then Map.lookup name primMap
+  else Nothing
+
+
+-- | Checks whether a given expression is in fact a Asynchronous Rattus primitive.
+isPrimExpr :: GetCtxt => LHsExpr GhcTc -> Maybe (Prim,Var)
+isPrimExpr (L _ e) = isPrimExpr' e where
+  isPrimExpr' :: GetCtxt => HsExpr GhcTc -> Maybe (Prim,Var)
+  isPrimExpr' (HsVar _ (L _ v)) = fmap (,v) (isPrim v)
+#if __GLASGOW_HASKELL__ >= 906
+  isPrimExpr' (HsAppType _ e _ _) = isPrimExpr e
+#elif __GLASGOW_HASKELL__ >= 808
+  isPrimExpr' (HsAppType _ e _) = isPrimExpr e
+#else
+  isPrimExpr' (HsAppType _ e)   = isPrimExpr e
+#endif
+
+#if __GLASGOW_HASKELL__ < 900
+  isPrimExpr' (HsSCC _ _ _ e) = isPrimExpr e
+  isPrimExpr' (HsCoreAnn _ _ _ e) = isPrimExpr e
+  isPrimExpr' (HsTickPragma _ _ _ _ e) = isPrimExpr e
+  isPrimExpr' (HsWrap _ _ e) = isPrimExpr' e
+#else
+  isPrimExpr' (XExpr (WrapExpr (HsWrap _ e))) = isPrimExpr' e
+  isPrimExpr' (XExpr (ExpansionExpr (HsExpanded _ e))) = isPrimExpr' e
+  isPrimExpr' (HsPragE _ _ e) = isPrimExpr e
+#endif
+#if __GLASGOW_HASKELL__ < 904
+  isPrimExpr' (HsTick _ _ e) = isPrimExpr e
+  isPrimExpr' (HsBinTick _ _ _ e) = isPrimExpr e
+  isPrimExpr' (HsPar _ e) = isPrimExpr e
+#else
+  isPrimExpr' (XExpr (HsTick _ e)) = isPrimExpr e
+  isPrimExpr' (XExpr (HsBinTick _ _ e)) = isPrimExpr e
+  isPrimExpr' (HsPar _ _ e _) = isPrimExpr e
+#endif
+
+  isPrimExpr' _ = Nothing
+
+
+-- | This type class provides default implementations for 'check' and
+-- 'checkBind' for Haskell syntax that is not supported. These default
+-- implementations simply print an error message.
+class NotSupported a where
+  notSupported :: GetCtxt => SDoc -> CheckM a
+
+instance NotSupported Bool where
+  notSupported doc = printMessageCheck SevError ("Asynchronous Rattus does not support " <> doc)
+
+instance NotSupported (Bool,Set Var) where
+  notSupported doc = (,Set.empty) <$> notSupported doc
+
+
+-- | Add variables to the current context.
+addVars :: Set Var -> Ctxt -> Ctxt
+addVars vs c = c{current = vs `Set.union` current c }
+
+-- | Print a message with the current location.
+printMessage' :: GetCtxt => Severity -> SDoc ->  CheckM ()
+printMessage' sev doc =
+  liftIO (modifyIORef (errorMsgs ?ctxt) ((sev ,srcLoc ?ctxt, doc) :))
+
+-- | Print a message with the current location. Returns 'False', if
+-- the severity is 'SevError' and otherwise 'True.
+printMessageCheck :: GetCtxt =>  Severity -> SDoc -> CheckM Bool
+printMessageCheck sev doc = printMessage' sev doc >>
+  case sev of
+    SevError -> return False
+    _ -> return True
diff --git a/src/AsyncRattus/Plugin/SingleTick.hs b/src/AsyncRattus/Plugin/SingleTick.hs
new file mode 100644
--- /dev/null
+++ b/src/AsyncRattus/Plugin/SingleTick.hs
@@ -0,0 +1,226 @@
+-- | This module implements the translation from the multi-tick
+-- calculus to the single tick calculus.
+
+{-# LANGUAGE CPP #-}
+
+module AsyncRattus.Plugin.SingleTick
+  (toSingleTick) where
+
+#if __GLASGOW_HASKELL__ >= 900
+import GHC.Plugins
+#else
+import GhcPlugins
+#endif
+
+  
+import AsyncRattus.Plugin.Utils
+import Prelude hiding ((<>))
+import Control.Monad.Trans.Writer.Strict
+import Control.Monad.Trans.Class
+import Data.List
+
+-- | Transform the given expression from the multi-tick calculus into
+-- the single tick calculus form.
+toSingleTick :: CoreExpr -> CoreM CoreExpr
+toSingleTick (Let (Rec bs) e) = do
+  e' <- toSingleTick e
+  bs' <- mapM (mapM toSingleTick) bs
+  return (Let (Rec bs') e')
+toSingleTick (Let (NonRec b e1) e2) = do
+  e1' <- toSingleTick e1
+  e2' <- toSingleTick e2
+  return (Let (NonRec b e1') e2')
+toSingleTick (Case e b ty alts) = do
+  e' <- toSingleTick e
+  alts' <- mapM ((\ (c,bs,f) -> fmap (\ x -> mkAlt c bs x) (toSingleTick f)) . getAlt) alts
+  return (Case e' b ty alts')
+toSingleTick (Cast e c) = do
+  e' <- toSingleTick e
+  return (Cast e' c)
+toSingleTick (Tick t e) = do
+  e' <- toSingleTick e
+  return (Tick t e')
+toSingleTick (Lam x e) = do
+  (e', advs) <- runWriterT (extractAdv' e)
+  advs' <- mapM (\ (x,a,b) -> fmap (\b' -> (x,a,b')) (toSingleTick b)) advs
+  return (foldLets' advs' (Lam x e'))
+toSingleTick (App e1 e2)
+  | isDelayApp e1 = do
+      (e2', advs) <- runWriterT (extractAdv e2)
+      advs' <- mapM (mapM toSingleTick) advs
+      return (foldLets advs' (App e1 e2'))
+  | otherwise = do
+      e1' <- toSingleTick e1
+      e2' <- toSingleTick e2
+      return (App e1' e2')
+
+toSingleTick e@Type{} = return e
+toSingleTick e@Var{} = return e
+toSingleTick e@Lit{} = return e
+toSingleTick e@Coercion{} = return e
+
+foldLets :: [(Id,CoreExpr)] -> CoreExpr -> CoreExpr
+foldLets ls e = foldl' (\e' (x,b) -> Let (NonRec x b) e') e ls
+
+foldLets' :: [(Id,CoreExpr,CoreExpr)] -> CoreExpr -> CoreExpr
+foldLets' ls e = foldl' (\e' (x,a,b) -> Let (NonRec x (App a b)) e') e ls
+
+extractAdvApp :: CoreExpr -> CoreExpr -> WriterT [(Id,CoreExpr)] CoreM CoreExpr
+extractAdvApp e1 e2
+  | isVar e2 = return (App e1 e2)
+  | otherwise = do
+  x <- lift (mkSysLocalFromExpr (fsLit "adv") e2)
+  tell [(x,e2)]
+  return (App e1 (Var x))
+
+-- removes casts and ticks from a tree
+filterTree :: CoreExpr -> CoreExpr
+filterTree (Cast e _) = filterTree e
+filterTree (Tick _ e) = filterTree e
+filterTree e = e
+
+
+extractSelectApp :: CoreExpr -> CoreExpr -> WriterT [(Id,CoreExpr)] CoreM CoreExpr
+extractSelectApp e1 e2
+  | isVar e' && isVar e2 = return (App e1 e2)
+  | isVar e2 = do
+    x <- lift (mkSysLocalFromExpr (fsLit "selectFreshVar") e')
+    tell [(x, e')]
+    return (App (App e (Var x)) e2)
+  | isVar e' = do
+    x <- lift (mkSysLocalFromExpr (fsLit "selectFreshVar") e2)
+    tell [(x, e2)]
+    return (App e1 (Var x))
+  | otherwise = do
+    x <- lift (mkSysLocalFromExpr (fsLit "selectFreshVar") e')
+    y <- lift (mkSysLocalFromExpr (fsLit "selectFreshVar") e2)
+    tell [(x, e')]
+    tell [(y, e2)]
+    return (App (App e (Var x)) (Var y))
+  where (App e e') = filterTree e1
+
+
+-- This is used to pull adv out of delayed terms. The writer monad
+-- returns mappings from fresh variables to terms that occur as
+-- argument of adv.
+-- 
+-- That is, occurrences of @adv t@ are replaced with @adv x@ (for some
+-- fresh variable @x@) and the pair @(x,t)@ is returned in the
+-- writer monad.
+extractAdv :: CoreExpr -> WriterT [(Id,CoreExpr)] CoreM CoreExpr
+extractAdv (App expr@(App e _) e2) | isSelectApp e = extractSelectApp expr e2
+extractAdv e@(App e1 e2)
+  | isAdvApp e1 = extractAdvApp e1 e2
+  | isSelectApp e1 = extractSelectApp e1 e2
+  | isDelayApp e1 = do
+      (e2', advs) <- lift $ runWriterT (extractAdv e2)
+      advs' <- mapM (mapM extractAdv) advs
+      return (foldLets advs' (App e1 e2'))
+  | isBoxApp e1 = lift $ toSingleTick e
+  | otherwise = do
+      e1' <- extractAdv e1
+      e2' <- extractAdv e2
+      return (App e1' e2')
+extractAdv (Lam x e) = do
+  (e', advs) <- lift $ runWriterT (extractAdv' e)
+  advs' <- mapM (\ (x,a,b) -> fmap (\b' -> (x,b')) (extractAdvApp a b)) advs
+  return (foldLets advs' (Lam x e'))
+extractAdv (Case e b ty alts) = do
+  e' <- extractAdv e
+  alts' <- mapM ((\ (c,bs,f) -> fmap (\ x -> mkAlt c bs x) (extractAdv f)) . getAlt) alts
+  return (Case e' b ty alts')
+extractAdv (Cast e c) = do
+  e' <- extractAdv e
+  return (Cast e' c)
+extractAdv (Tick t e) = do
+  e' <- extractAdv e
+  return (Tick t e')
+extractAdv e@(Let Rec{} _) = lift $ toSingleTick e
+extractAdv (Let (NonRec b e1) e2) = do
+  e1' <- extractAdv e1
+  e2' <- extractAdv e2
+  return (Let (NonRec b e1') e2')
+extractAdv e@Type{} = return e
+extractAdv e@Var{} = return e
+extractAdv e@Lit{} = return e
+extractAdv e@Coercion{} = return e
+
+-- This is used to pull adv out of lambdas. The writer monad returns
+-- mappings from fresh variables to occurrences of adv and the term it
+-- is applied to.
+-- 
+-- That is occurrences of @adv t@ are replaced with a fresh variable
+-- @x@ and the triple @(x,adv,t)@ is returned in the writer monad.
+-- For select a b, the triple @(x, select a, b) is returned in the writer monad.
+extractAdv' :: CoreExpr -> WriterT [(Id,CoreExpr,CoreExpr)] CoreM CoreExpr
+extractAdv' e@(App e1 e2)
+  | isAdvApp e1 = do
+       x <- lift (mkSysLocalFromExpr (fsLit "adv") e)
+       tell [(x,e1,e2)]
+       return (Var x)
+  | isSelectApp e1 = do
+      x <- lift (mkSysLocalFromExpr (fsLit "select") e)
+      tell [(x,e1,e2)]
+      return (Var x)
+  | isDelayApp e1 = do
+      (e2', advs) <- lift $ runWriterT (extractAdv e2)
+      advs' <- mapM (mapM extractAdv') advs
+      return (foldLets advs' (App e1 e2'))
+  | isBoxApp e1 = lift $ toSingleTick e
+  | otherwise = do
+      e1' <- extractAdv' e1
+      e2' <- extractAdv' e2
+      return (App e1' e2')
+extractAdv' (Lam x e) = do
+  e' <- extractAdv' e
+  return (Lam x e')
+extractAdv' (Case e b ty alts) = do
+  e' <- extractAdv' e
+  alts' <- mapM ((\ (c,bs,f) -> fmap (\ x -> mkAlt c bs x) (extractAdv' f)) . getAlt) alts
+  return (Case e' b ty alts')
+extractAdv' (Cast e c) = do
+  e' <- extractAdv' e
+  return (Cast e' c)
+extractAdv' (Tick t e) = do
+  e' <- extractAdv' e
+  return (Tick t e')
+extractAdv' e@(Let Rec{} _) = lift $ toSingleTick e
+extractAdv' (Let (NonRec b e1) e2) = do
+  e1' <- extractAdv' e1
+  e2' <- extractAdv' e2
+  return (Let (NonRec b e1') e2')
+extractAdv' e@Type{} = return e
+extractAdv' e@Var{} = return e
+extractAdv' e@Lit{} = return e
+extractAdv' e@Coercion{} = return e
+
+
+
+isDelayApp :: CoreExpr -> Bool
+isDelayApp = isPrimApp (== "delay")
+
+isBoxApp :: CoreExpr -> Bool
+isBoxApp = isPrimApp (\occ -> occ == "Box" || occ == "box")
+
+isAdvApp :: CoreExpr -> Bool
+isAdvApp = isPrimApp (== "adv")
+
+isSelectApp :: CoreExpr -> Bool
+isSelectApp = isPrimApp (== "select")
+
+isPrimApp :: (String -> Bool) -> CoreExpr -> Bool
+isPrimApp p (App e e')
+  | isType e' || not  (tcIsLiftedTypeKind(typeKind (exprType e'))) = isPrimApp p e
+  | otherwise = False
+isPrimApp p (Cast e _) = isPrimApp p e
+isPrimApp p (Tick _ e) = isPrimApp p e
+isPrimApp p (Var v) = isPrimVar p v
+isPrimApp _ _ = False
+
+isPrimVar :: (String -> Bool) -> Var -> Bool
+isPrimVar p v = maybe False id $ do
+  let name = varName v
+  mod <- nameModule_maybe name
+  let occ = getOccString name
+  return (p occ
+          && moduleNameString (moduleName mod) == "AsyncRattus.InternalPrimitives")
diff --git a/src/AsyncRattus/Plugin/StableSolver.hs b/src/AsyncRattus/Plugin/StableSolver.hs
new file mode 100644
--- /dev/null
+++ b/src/AsyncRattus/Plugin/StableSolver.hs
@@ -0,0 +1,93 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE CPP #-}
+
+
+-- | This module implements a constraint solver plugin for the
+-- 'Stable' type class.
+
+module AsyncRattus.Plugin.StableSolver (tcStable) where
+
+import AsyncRattus.Plugin.Utils
+    ( getNameModule, isRattModule, isStable )
+
+import Prelude hiding ((<>))
+
+#if __GLASGOW_HASKELL__ >= 900
+import GHC.Plugins
+  (Type, Var, CommandLineOption,tyConSingleDataCon,
+   mkCoreConApps,getTyVar_maybe)
+import GHC.Core
+import GHC.Tc.Types.Evidence
+import GHC.Core.Class
+import GHC.Tc.Types
+#else
+import GhcPlugins
+  (Type, Var, CommandLineOption,tyConSingleDataCon,
+   mkCoreConApps,getTyVar_maybe)
+import CoreSyn
+import TcEvidence
+import Class
+import TcRnTypes
+#endif
+
+#if __GLASGOW_HASKELL__ >= 900
+import GHC.Tc.Types.Constraint
+#elif __GLASGOW_HASKELL__ >= 810
+import Constraint
+#endif
+
+import Data.Set (Set)
+import qualified Data.Set as Set
+#if __GLASGOW_HASKELL__ >= 904
+import GHC.Types.Unique.FM
+#endif
+
+
+
+-- | Constraint solver plugin for the 'Stable' type class.
+tcStable :: [CommandLineOption] -> Maybe TcPlugin
+tcStable _ = Just $ TcPlugin
+  { tcPluginInit = return ()
+  , tcPluginSolve = \ () -> stableSolver
+  , tcPluginStop = \ () -> return ()
+#if __GLASGOW_HASKELL__ >= 904
+  , tcPluginRewrite = \ () -> emptyUFM
+#endif
+  }
+
+
+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
+
+#if __GLASGOW_HASKELL__ >= 904
+stableSolver :: EvBindsVar -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult
+stableSolver _ given wanted = do
+#else
+stableSolver :: [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult
+stableSolver given _derived wanted = do
+#endif
+
+  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/AsyncRattus/Plugin/Strictify.hs b/src/AsyncRattus/Plugin/Strictify.hs
new file mode 100644
--- /dev/null
+++ b/src/AsyncRattus/Plugin/Strictify.hs
@@ -0,0 +1,86 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE CPP #-}
+module AsyncRattus.Plugin.Strictify
+  (strictifyExpr, SCxt (..)) where
+import Prelude hiding ((<>))
+import AsyncRattus.Plugin.Utils
+
+#if __GLASGOW_HASKELL__ >= 900
+import GHC.Plugins
+#else
+import GhcPlugins
+#endif
+
+#if __GLASGOW_HASKELL__ >= 902
+import GHC.Types.Tickish
+#endif
+
+data SCxt = SCxt {srcSpan :: SrcSpan, checkStrictData :: Bool}
+
+-- | Transforms all functions into strict functions. If the
+-- 'checkStrictData' field of the 'SCxt' argument is set to @True@,
+-- then this function also checks for use of non-strict data types and
+-- produces warnings if it finds any.
+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) [mkAlt DEFAULT [] e2' ])
+strictifyExpr ss (Case e b t alts) = do
+  e' <- strictifyExpr ss e
+  alts' <- mapM ((\(c,args,e) -> fmap (\e' -> mkAlt c args e' ) (strictifyExpr ss e)) . getAlt) alts
+  return (Case e' b t alts')
+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 ss (Lam b e)
+   | not (isCoVar b) && not (isTyVar b) && tcIsLiftedTypeKind(typeKind (varType b))
+    = do
+       e' <- strictifyExpr ss e
+       b' <- mkSysLocalFromVar (fsLit "strict") b
+       return (Lam b' (Case (varToCoreExpr b') b (exprType e) [mkAlt 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 ss (Tick t@(SourceNote span _) e) = do
+  e' <- strictifyExpr (ss{srcSpan = fromRealSrcSpan span}) e
+  return (Tick t e')
+strictifyExpr ss (App e1 e2@Lit{}) =
+  do e1' <- strictifyExpr ss e1
+     return (App e1' e2)
+strictifyExpr ss (App e1 e2)
+  | (checkStrictData ss && not (isType e2) && tcIsLiftedTypeKind(typeKind (exprType e2))
+        && not (isStrict (exprType e2))) = 
+      if isDeepseqForce e2 || isLit e2 then
+        do e1' <- strictifyExpr ss e1
+           e2' <- strictifyExpr ss e2
+           return (App e1' e2')
+      else
+        do (printMessage SevWarning (srcSpan ss)
+               (text "The use of lazy type " <> ppr (exprType e2) <> " may lead to memory leaks. Use Control.DeepSeq.force on lazy types."))
+           e1' <- strictifyExpr ss{checkStrictData = False} e1
+           e2' <- strictifyExpr ss{checkStrictData = False} e2
+           return (App e1' e2')
+  | otherwise = do
+      e1' <- strictifyExpr ss e1
+      e2' <- strictifyExpr ss e2
+      return (App e1' e2')
+strictifyExpr _ss e = return e
+
+isLit :: CoreExpr -> Bool
+isLit Lit{} = True
+isLit (App (Var v) Lit{}) 
+  | Just (name,mod) <- getNameModule v = mod == "GHC.CString" && name == "unpackCString#"
+isLit _ = False
+
+
+isDeepseqForce :: CoreExpr -> Bool
+isDeepseqForce (App (App (App (Var v) _) _) _) =
+  case getNameModule v of
+    Just (name, mod) -> mod == "Control.DeepSeq" && name == "force"
+    _ -> False
+isDeepseqForce _ = False
diff --git a/src/AsyncRattus/Plugin/Transform.hs b/src/AsyncRattus/Plugin/Transform.hs
new file mode 100644
--- /dev/null
+++ b/src/AsyncRattus/Plugin/Transform.hs
@@ -0,0 +1,144 @@
+{-# LANGUAGE TupleSections #-}
+module AsyncRattus.Plugin.Transform (
+    transform
+) where
+
+import GHC.Core.Opt.Monad
+import GHC.Plugins
+import AsyncRattus.Plugin.PrimExpr
+import AsyncRattus.Plugin.Utils
+import Data.Maybe (fromJust)
+import Prelude hiding ((<>))
+import Data.Functor ((<&>))
+import Control.Applicative ((<|>))
+import Data.Tuple (swap)
+
+data Ctx = Ctx {
+    fresh :: Maybe Var
+}
+
+emptyCtx :: Ctx
+emptyCtx = Ctx {
+    fresh = Nothing
+}
+
+replaceVar :: Var -> Var -> Expr Var ->  Expr Var
+replaceVar match rep (Var v) = if v == match then Var rep else Var v
+replaceVar match rep (App e e') = App (replaceVar match rep e) (replaceVar match rep e')
+replaceVar match rep (Tick _ e) = replaceVar match rep e
+replaceVar match rep (Lam v e) = Lam (if v == match then rep else v) (replaceVar match rep e)
+replaceVar match rep (Let (NonRec b e') e) =
+  Let (NonRec newB (replaceVar  match rep e')) (replaceVar match rep e)
+  where newB = if b == match then rep else b
+replaceVar match rep (Cast e _) = replaceVar match rep e
+replaceVar match rep (Case e b t alts) =
+  Case newExpr newB t (map (\(Alt con binds expr) -> Alt con (map (\v -> if v == match then rep else v) binds) (replaceVar match rep expr)) alts)
+  where newExpr = replaceVar match rep e
+        newB = if b == match then rep else b
+replaceVar _ _ e = e
+
+transformPrim :: Ctx -> Expr Var -> CoreM (Expr Var, PrimInfo)
+transformPrim ctx expr@(App e e') = case isPrimExpr expr of
+  Just primInfo@(AdvApp f _) -> do
+    varAdv' <- adv'Var
+    let newE = replaceVar f varAdv' e
+    return (App (App newE e') (Var (fromJust $ fresh ctx)), primInfo)
+  Just primInfo@(SelectApp f _ _) -> do
+    varSelect' <- select'Var
+    let newE = replaceVar f varSelect' e
+    return (App (App newE e') (Var (fromJust $ fresh ctx)), primInfo)
+  Just (DelayApp _ t) -> do
+    bigDelayVar <- bigDelay
+    inputValueV <- inputValueVar
+    let inputValueType = mkTyConTy inputValueV 
+    inpVar <- mkSysLocalM (fsLit "inpV") inputValueType inputValueType
+    let ctx' = ctx {fresh = Just inpVar}
+    (newExpr, maybePrimInfo) <- transform' ctx' e'
+    let primInfo = fromJust maybePrimInfo
+    let lambdaExpr = Lam inpVar newExpr
+    clockCode <- constructClockExtractionCode primInfo
+    return (App (App (App (Var bigDelayVar) (Type t)) clockCode) lambdaExpr, primInfo)
+  Just primInfo -> do
+        error $ showSDocUnsafe $ text "transformPrim: Cannot transform " <> ppr (prim primInfo)
+  Nothing -> error "Cannot transform non-prim applications"
+transformPrim _ _ = do
+  error "Cannot transform anything else than prim applications"
+
+
+transform :: CoreExpr -> CoreM CoreExpr
+transform expr = fst <$> transform' emptyCtx expr
+
+transform' :: Ctx -> CoreExpr -> CoreM (CoreExpr, Maybe PrimInfo)
+transform' ctx expr@(App e e') = case isPrimExpr expr of
+    Just (BoxApp _) -> do
+        (newExpr, primInfo) <- transform' ctx e'
+        return (App e newExpr, primInfo)
+    Just _ -> do
+        (newExpr, primInfo) <- transformPrim ctx expr
+        return (newExpr, Just primInfo)
+    Nothing -> do
+        (newExpr, primInfo) <- transform' ctx e
+        (newExpr', primInfo') <- transform' ctx e'
+        return (App newExpr newExpr', primInfo <|> primInfo')
+transform' ctx (Lam b rhs) = do
+    (newExpr, primInfo) <- transform' ctx rhs
+    return (Lam b newExpr, primInfo)
+transform' ctx (Let (NonRec b rhs) e) = do
+    (newRhs, primInfo) <- transform' ctx rhs
+    (newExpr, primInfo') <- transform' ctx e
+    return (Let (NonRec b newRhs) newExpr, primInfo <|> primInfo')
+transform' ctx (Let (Rec binds) e) = do
+    transformedBinds <- mapM (\(b, bindE) -> fmap (b,) (transform' ctx bindE)) binds
+    (e', mPi) <- transform' ctx e
+    let primInfos = map (\(_, (_, p)) -> p) transformedBinds
+    let firstPrimInfo = foldl (<|>) mPi primInfos
+    newBinds <- mapM (\(b, (e, _)) -> return (b, e)) transformedBinds
+    return (Let (Rec newBinds) e', firstPrimInfo)
+transform' ctx (Case e b t alts) = do
+    -- The checking pass has ensured that there are not advances on different
+    -- clocks. Thus we can just pick the first PrimInfo we find.
+    (expr, primInfo) <- transform' ctx e
+
+    -- For each alternative, transform it and save the maybePrimInfo-value
+    transformed <- mapM (\(Alt con binds expr) -> transform' ctx expr <&> fmap (Alt con binds) . swap) alts
+
+    -- Of all the primInfos we have, pick the first one. This is safe because
+    -- the checking pass has ensured that the clocks of all primitives.
+    let firstPrimInfo = foldl (\acc (p, _) -> acc <|> p) primInfo transformed
+    let alts' = map snd transformed
+    return (Case expr b t alts', firstPrimInfo)
+transform' ctx (Cast e _) = transform' ctx e
+transform' ctx (Tick _ e) = transform' ctx e
+transform' _ e = return (e, Nothing)
+
+constructClockExtractionCode :: PrimInfo -> CoreM CoreExpr
+constructClockExtractionCode (AdvApp _ arg) = createClockCode arg
+constructClockExtractionCode (SelectApp _ arg arg2) =
+    clockUnion arg arg2
+constructClockExtractionCode primInfo = error $ "Cannot construct clock for prim " ++ showSDocUnsafe (ppr (prim primInfo))
+
+
+createClockCode :: (Var, Type) -> CoreM CoreExpr
+createClockCode (argV, argT) = do
+    extractClock <- extractClockVar
+    return $ App (App (Var extractClock) (Type argT)) (Var argV)
+
+-- Generate code for union of two clocks.
+-- clockUnion (aVar, aType) (bVar, bType) returns the AST for:
+--  Set.union (extractClock aVar) (extractClock bVar)
+
+clockUnion :: (Var,Type) -> (Var, Type) -> CoreM CoreExpr
+clockUnion arg arg2 = do
+    clock1Code <- createClockCode arg
+    clock2Code <- createClockCode arg2
+    unionVar' <- unionVar
+    return $
+        App
+        (
+            App
+            (
+                   (Var unionVar')
+            )
+            clock1Code
+        )
+        clock2Code
diff --git a/src/AsyncRattus/Plugin/Utils.hs b/src/AsyncRattus/Plugin/Utils.hs
new file mode 100644
--- /dev/null
+++ b/src/AsyncRattus/Plugin/Utils.hs
@@ -0,0 +1,430 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE CPP #-}
+
+module AsyncRattus.Plugin.Utils (
+  printMessage,
+  Severity(..),
+  isRattModule,
+  adv'Var,
+  select'Var,
+  bigDelay,
+  inputValueVar,
+  extractClockVar,
+  unionVar,
+  isGhcModule,
+  getNameModule,
+  isStable,
+  isStrict,
+  isTemporal,
+  userFunction,
+  typeClassFunction,
+  getVar,
+  getMaybeVar,
+  getModuleFS,
+  isVar,
+  isType,
+  mkSysLocalFromVar,
+  mkSysLocalFromExpr,
+  fromRealSrcSpan,
+  noLocationInfo,
+  mkAlt,
+  getAlt,
+  splitForAllTys')
+  where
+#if __GLASGOW_HASKELL__ >= 906
+import GHC.Builtin.Types.Prim
+import GHC.Tc.Utils.TcType
+#endif
+#if __GLASGOW_HASKELL__ >= 904
+import qualified GHC.Data.Strict as Strict
+import Control.Concurrent.MVar (readMVar)
+#else
+import Data.IORef (readIORef)
+#endif  
+#if __GLASGOW_HASKELL__ >= 902
+
+import GHC.Utils.Logger
+#endif
+
+#if __GLASGOW_HASKELL__ >= 900
+import GHC.Plugins
+import GHC.Utils.Error
+import GHC.Utils.Monad
+#else
+import GhcPlugins
+import ErrUtils
+import MonadUtils
+#endif
+
+
+import GHC.Types.Name.Cache (NameCache(nsNames), lookupOrigNameCache, OrigNameCache)
+import qualified GHC.Types.Name.Occurrence as Occurrence
+import GHC.Types.TyThing
+
+import Prelude hiding ((<>))
+import Data.Set (Set)
+import qualified Data.Set as Set
+import Data.Char
+import Data.Maybe
+
+
+getMaybeVar :: CoreExpr -> Maybe Var
+getMaybeVar (App e e')
+  | isType e' || not  (tcIsLiftedTypeKind (typeKind (exprType e'))) = getMaybeVar e
+  | otherwise = Nothing
+getMaybeVar (Cast e _) = getMaybeVar e
+getMaybeVar (Tick _ e) = getMaybeVar e
+getMaybeVar (Var v) = Just v
+getMaybeVar _ = Nothing
+
+getVar :: CoreExpr -> Var
+getVar = fromJust . getMaybeVar
+
+isVar :: CoreExpr -> Bool
+isVar = isJust . getMaybeVar
+
+isType Type {} = True
+isType (App e _) = isType e
+isType (Cast e _) = isType e
+isType (Tick _ e) = isType e
+isType _ = False
+
+#if __GLASGOW_HASKELL__ >= 906
+isFunTyCon = isArrowTyCon
+repSplitAppTys = splitAppTysNoView
+#endif
+ 
+#if __GLASGOW_HASKELL__ >= 902
+printMessage :: (HasDynFlags m, MonadIO m, HasLogger m) =>
+                Severity -> SrcSpan -> SDoc -> m ()
+#else
+printMessage :: (HasDynFlags m, MonadIO m) =>
+                Severity -> SrcSpan -> MsgDoc -> m ()
+#endif
+
+printMessage sev loc doc = do
+#if __GLASGOW_HASKELL__ >= 906
+  logger <- getLogger
+  liftIO $ putLogMsg logger (logFlags logger)
+    (MCDiagnostic sev (if sev == SevError then ErrorWithoutFlag else WarningWithoutFlag) Nothing) loc doc
+#elif __GLASGOW_HASKELL__ >= 904
+  logger <- getLogger
+  liftIO $ putLogMsg logger (logFlags logger)
+    (MCDiagnostic sev (if sev == SevError then ErrorWithoutFlag else WarningWithoutFlag)) loc doc
+#elif __GLASGOW_HASKELL__ >= 902
+   dflags <- getDynFlags
+   logger <- getLogger
+   liftIO $ putLogMsg logger dflags NoReason sev loc doc
+#elif __GLASGOW_HASKELL__ >= 900  
+  dflags <- getDynFlags
+  liftIO $ putLogMsg dflags NoReason sev loc doc
+#else
+  dflags <- getDynFlags
+  let sty = case sev of
+              SevError   -> defaultErrStyle dflags
+              SevWarning -> defaultErrStyle dflags
+              SevDump    -> defaultDumpStyle dflags
+              _          -> defaultUserStyle dflags
+  liftIO $ putLogMsg dflags NoReason sev loc sty doc
+#endif
+
+#if __GLASGOW_HASKELL__ >= 902
+instance Ord FastString where
+   compare = uniqCompareFS
+#endif
+
+{-
+******************************************************
+*             Extracting variables                   *
+******************************************************
+-}
+
+
+origNameCache :: CoreM OrigNameCache
+origNameCache = do
+  hscEnv <- getHscEnv
+#if __GLASGOW_HASKELL__ >= 904
+  let nameCache = hsc_NC hscEnv
+  liftIO $ readMVar (nsNames nameCache)
+#else
+  nameCache <- liftIO $ readIORef (hsc_NC hscEnv)
+  return $ nsNames nameCache
+#endif
+
+
+getNamedThingFromModuleAndOccName :: String -> OccName -> CoreM TyThing
+getNamedThingFromModuleAndOccName moduleName occName = do
+  origNameCache <- origNameCache
+  let [mod] = filter ((moduleName ==) . unpackFS . getModuleFS) (moduleEnvKeys origNameCache)
+  let name = fromJust $ lookupOrigNameCache origNameCache mod occName
+  lookupThing name
+
+getVarFromModule :: String -> String -> CoreM Var
+getVarFromModule moduleName = fmap tyThingId . getNamedThingFromModuleAndOccName moduleName . mkOccName Occurrence.varName
+
+getTyConFromModule :: String -> String -> CoreM TyCon
+getTyConFromModule moduleName = fmap tyThingTyCon . getNamedThingFromModuleAndOccName moduleName . mkOccName Occurrence.tcName
+
+adv'Var :: CoreM Var
+adv'Var = getVarFromModule "AsyncRattus.InternalPrimitives" "adv'"
+
+select'Var :: CoreM Var
+select'Var = getVarFromModule "AsyncRattus.InternalPrimitives" "select'"
+
+bigDelay :: CoreM Var
+bigDelay = getVarFromModule "AsyncRattus.InternalPrimitives" "Delay"
+
+inputValueVar :: CoreM TyCon
+inputValueVar = getTyConFromModule "AsyncRattus.InternalPrimitives" "InputValue"
+
+extractClockVar :: CoreM Var
+extractClockVar = getVarFromModule "AsyncRattus.InternalPrimitives" "extractClock"
+
+unionVar :: CoreM Var
+unionVar = getVarFromModule "AsyncRattus.InternalPrimitives" "clockUnion"
+
+rattModules :: Set FastString
+rattModules = Set.fromList ["AsyncRattus.InternalPrimitives","AsyncRattus.Channels"]
+
+getModuleFS :: Module -> FastString
+getModuleFS = moduleNameFS . moduleName
+
+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", "IO"]
+
+isGhcStableType :: FastString -> Bool
+isGhcStableType = (`Set.member` ghcStableTypes)
+
+
+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 -> isGhcStableType name
+          {- 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
+
+
+
+isStrict :: Type -> Bool
+isStrict t = isStrictRec 0 Set.empty t
+
+#if __GLASGOW_HASKELL__ >= 902
+splitForAllTys' :: Type -> ([TyCoVar], Type)
+splitForAllTys' = splitForAllTyCoVars
+#else
+splitForAllTys' = splitForAllTys
+#endif
+
+-- | 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)
+          | mod == "GHC.Num.Integer" && name == "Integer" -> True
+          | mod == "Data.Text.Internal" && name == "Text" -> True
+          -- If it's a Rattus type constructor check if it's a box
+          | isRattModule mod && (name == "Box" || name == "O" || name == "Output") -> True
+            -- If its a built-in type check the set of stable built-in types
+          | isGhcModule mod -> isGhcStableType name
+          {- 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 (areSrcStrict 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
+              NewTyCon {nt_rhs = ty} -> isStrictRec (d+1) pr' ty
+              _ -> False
+          | otherwise -> False
+
+
+
+
+
+areSrcStrict :: [Type] -> DataCon -> Bool
+areSrcStrict args con = and (zipWith check tys (dataConSrcBangs con))
+  where (_, _,tys) = dataConInstSig con args
+        check _ b = isSrcStrict' b
+
+isSrcStrict' :: HsSrcBang -> Bool
+isSrcStrict' (HsSrcBang _ _ SrcStrict) = True
+isSrcStrict' (HsSrcBang _ SrcUnpack _) = True
+isSrcStrict' _ =  False
+
+
+userFunction :: Var -> Bool
+userFunction v
+  | typeClassFunction v = True
+  | otherwise = 
+    case getOccString (getName v) of
+      (c : _)
+        | isUpper c || c == '$' || c == ':' -> False
+        | otherwise -> True
+      _ -> False
+
+typeClassFunction :: Var -> Bool
+typeClassFunction v =
+  case getOccString (getName v) of
+    ('$' : 'c' : _) -> True
+    ('$' : 'f' : _) -> True
+    _ -> False
+
+mkSysLocalFromVar :: MonadUnique m => FastString -> Var -> m Id
+#if __GLASGOW_HASKELL__ >= 900
+
+mkSysLocalFromVar lit v = mkSysLocalM lit (varMult v) (varType v)
+#else
+mkSysLocalFromVar lit v = mkSysLocalM lit (varType v)
+#endif
+ 
+mkSysLocalFromExpr :: MonadUnique m => FastString -> CoreExpr -> m Id
+#if __GLASGOW_HASKELL__ >= 900
+mkSysLocalFromExpr lit e = mkSysLocalM lit oneDataConTy (exprType e)
+#else
+mkSysLocalFromExpr lit e = mkSysLocalM lit (exprType e)
+#endif
+ 
+ 
+fromRealSrcSpan :: RealSrcSpan -> SrcSpan
+#if __GLASGOW_HASKELL__ >= 904
+fromRealSrcSpan span = RealSrcSpan span Strict.Nothing
+#elif __GLASGOW_HASKELL__ >= 900
+fromRealSrcSpan span = RealSrcSpan span Nothing
+#else
+fromRealSrcSpan span = RealSrcSpan span
+#endif
+
+#if __GLASGOW_HASKELL__ >= 900
+instance Ord SrcSpan where
+  compare (RealSrcSpan s _) (RealSrcSpan t _) = compare s t
+  compare RealSrcSpan{} _ = LT
+  compare _ _ = GT
+#endif
+
+noLocationInfo :: SrcSpan
+#if __GLASGOW_HASKELL__ >= 900
+noLocationInfo = UnhelpfulSpan UnhelpfulNoLocationInfo
+#else         
+noLocationInfo = UnhelpfulSpan "<no location info>"
+#endif
+
+#if __GLASGOW_HASKELL__ >= 902
+mkAlt c args e = Alt c args e
+getAlt (Alt c args e) = (c, args, e)
+#else
+mkAlt c args e = (c, args, e)
+getAlt alt = alt
+#endif
diff --git a/src/AsyncRattus/Primitives.hs b/src/AsyncRattus/Primitives.hs
new file mode 100644
--- /dev/null
+++ b/src/AsyncRattus/Primitives.hs
@@ -0,0 +1,19 @@
+-- | The language primitives of Async Rattus. Note that the typing
+--  rules for 'delay', 'adv','select' and 'box' are more restrictive
+--  than the Haskell types that are indicated. The stricter Async
+--  Rattus typing rules for these primitives are given below.
+
+{-# LANGUAGE TypeOperators #-}
+module AsyncRattus.Primitives
+  (O
+  ,Box
+  ,Select(..)
+  ,delay
+  ,adv
+  ,box
+  ,unbox
+  ,select
+  ,never
+  ,Stable
+  ) where
+import AsyncRattus.InternalPrimitives
diff --git a/src/AsyncRattus/Signal.hs b/src/AsyncRattus/Signal.hs
new file mode 100644
--- /dev/null
+++ b/src/AsyncRattus/Signal.hs
@@ -0,0 +1,368 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# OPTIONS -fplugin=AsyncRattus.Plugin #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE CPP #-}
+
+
+-- | Programming with signals.
+
+module AsyncRattus.Signal
+  ( map
+  , mkInputSig
+  , getInputSig
+  , filterMap
+  , filterMapAwait
+  , filter
+  , filterAwait
+  , trigger
+  , triggerAwait
+  , mapAwait
+  , switch
+  , switchS
+  , switchAwait
+  , interleave
+  , mkSig
+  , mkBoxSig
+  , current
+  , future
+  , const
+  , scan
+  , scanAwait
+  , scanMap
+  , Sig(..)
+  , zipWith
+  , zipWith3
+  , zip
+  , cond
+  , integral
+  , derivative
+  )
+
+where
+
+import AsyncRattus
+import AsyncRattus.Channels
+import Prelude hiding (map, const, zipWith, zipWith3, zip, filter)
+import Data.VectorSpace
+import Data.Ratio ((%))
+
+infixr 5 :::
+
+-- | @Sig a@ is a stream of values of type @a@.
+data Sig a = !a ::: !(O (Sig a))
+
+instance Producer (Sig a) a where
+  getCurrent p = Just' (current p)
+  getNext p cb = cb (future p)
+
+newtype SigMaybe a = SigMaybe (Sig (Maybe' a))
+
+instance Producer (SigMaybe a) a where
+  getCurrent (SigMaybe p) = current p
+  getNext (SigMaybe p) cb = cb (delay (SigMaybe (adv (future p))))
+
+
+
+{-# ANN module AsyncRattus #-}
+
+-- | Get the current value of a signal.
+current :: Sig a -> a
+current (x ::: _) = x
+
+
+-- | Get the future the signal.
+future :: Sig a -> O (Sig a)
+future (_ ::: xs) = xs
+
+-- | Apply a function to the value of a signal.
+map :: Box (a -> b) -> Sig a -> Sig b
+map f (x ::: xs) = unbox f x ::: delay (map f (adv xs))
+
+-- | Variant of 'getInput' that returns a signal instead of a boxed
+-- delayed computation.
+getInputSig :: IO (Box (O (Sig a)) :* (a -> IO ()))
+getInputSig = do (s :* cb) <- getInput
+                 return (mkBoxSig s :* cb)
+
+-- | Turn a producer into a signal. This is a variant of 'mkInput'
+-- that returns a signal instead of a boxed delayed computation.
+mkInputSig :: Producer p a => p -> IO (Box (O (Sig a)))
+mkInputSig p = mkBoxSig <$> mkInput p
+
+
+-- | This function is essentially the composition of 'filter' with
+-- 'map'. The signal produced by @filterMap f s@ has the value @v@
+-- whenever @s@ has the value @u@ such that @unbox f u = Just' v@.
+filterMap :: Box (a -> Maybe' b) -> Sig a -> IO (Box (O (Sig b)))
+filterMap f s = mkInputSig (SigMaybe (map f s))
+
+-- | This function is similar to 'filterMap' but takes a delayed
+-- signal (type @O (Sig a)@) as an argument instead of a signal (@Sig
+-- a@).
+filterMapAwait :: Box (a -> Maybe' b) -> O (Sig a) -> IO (Box (O (Sig b)))
+filterMapAwait f s = mkInputSig (delay (SigMaybe (map f (adv s))))
+
+-- | Filter the given signal using a predicate. The signal produced by
+-- @filter p s@ contains only values from @s@ that satisfy the
+-- predicate @p@.
+filter :: Box (a -> Bool) -> Sig a -> IO (Box (O (Sig a)))
+filter p = filterMap (box (\ x -> if unbox p x then Just' x else Nothing'))
+
+-- | This function is similar to 'filter' but takes a delayed signal
+-- (type @O (Sig a)@) as an argument instead of a signal (@Sig a@).
+filterAwait :: Box (a -> Bool) -> O (Sig a) -> IO (Box (O (Sig a)))
+filterAwait p = filterMapAwait (box (\ x -> if unbox p x then Just' x else Nothing'))
+
+
+-- | This function is a variant of 'zipWith'. Whereas @zipWith f xs
+-- ys@ produces a new value whenever @xs@ or @ys@ produce a new value,
+-- @trigger f xs ys@ only produces a new value when xs produces a new
+-- value.
+--
+-- Example:
+--
+-- >                      xs:  1 2 3     2
+-- >                      ys:  1     0 5 2
+-- >
+-- > zipWith (box (+)) xs ys:  2 3 4 3 8 4
+-- > trigger (box (+)) xy ys:  2     3 8 4
+
+trigger :: (Stable a, Stable b) => Box (a -> b -> c) -> Sig a -> Sig b -> IO (Box (Sig c))
+trigger f (a ::: as) bs@(b:::_) = do s <- triggerAwait f as bs
+                                     return (box (unbox f a b ::: unbox s))
+-- | This function is similar to 'trigger' but takes a delayed signal
+-- (type @O (Sig a)@) as an argument instead of a signal (@Sig a@).
+triggerAwait :: Stable b => Box (a -> b -> c) -> O (Sig a) -> Sig b -> IO (Box (O (Sig c)))
+triggerAwait f as bs = mkBoxSig <$> mkInput (box SigMaybe `mapO` (trig f as bs)) where
+  trig :: Stable b => Box (a -> b -> c) -> O (Sig a) -> Sig b -> O (Sig (Maybe' c))
+  trig f as (b ::: bs) =
+    delay (case select as bs of
+            Fst (a' ::: as') bs' -> Just' (unbox f a' b) ::: trig f as' (b ::: bs')
+            Snd as' bs' -> Nothing' ::: trig f as' bs'
+            Both (a' ::: as') (b' ::: bs') -> Just' (unbox f a' b') ::: trig f as' (b' ::: bs')
+          )
+
+-- | A version of @map@ for delayed signals.
+mapAwait :: Box (a -> b) -> O (Sig a) -> O (Sig b)
+mapAwait f d = delay (map f (adv d))
+
+-- | Turns a boxed delayed computation into a delayed signal.
+mkSig :: Box (O a) -> O (Sig a)
+mkSig b = delay (adv (unbox b) ::: mkSig b)
+
+-- | Variant of 'mkSig' that returns a boxed delayed signal
+mkBoxSig :: Box (O a) -> Box (O (Sig a))
+mkBoxSig b = box (mkSig b)
+
+
+-- | Construct a constant signal that never updates.
+const :: a -> Sig a
+const x = x ::: never
+
+-- | Construct a signal by repeatedly applying a function to a given
+-- start element. That is, @unfold (box f) x@ will produce the signal
+-- @x ::: f x ::: f (f x) ::: ...@
+-- unfold :: Stable a => Box (a -> a) -> a -> Sig 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 -> Sig a -> Sig b
+scan f acc (a ::: as) = acc' ::: delay (scan f acc' (adv as))
+  where acc' = unbox f acc a
+
+-- Like 'scan', but uses a delayed signal.
+scanAwait :: (Stable b) => Box (b -> a -> b) -> b -> O (Sig a) -> Sig b
+scanAwait f acc as = acc ::: delay (scan f acc (adv as))
+
+-- | '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 -> Sig a -> Sig c
+scanMap f p acc (a ::: as) =  unbox p acc' ::: delay (scanMap f p acc' (adv as))
+  where acc' = unbox f acc a
+
+-- | This function allows to switch from one signal to another one
+-- dynamically. The signal defined by @switch xs ys@ first behaves
+-- like @xs@, but as soon as @ys@ produces a new value, @switch xs ys@
+-- behaves like @ys@.
+--
+-- Example:
+--
+-- >           xs: 1 2 3 4 5   6 7 8   9
+-- >           ys:         1 2   3 4 5 6
+-- >
+-- > switch xs ys: 1 2 3 1 2 4   3 4 5 6
+switch :: Sig a -> O (Sig a) -> Sig a
+switch (x ::: xs) d = x ::: delay (case select xs d of
+                                     Fst   xs'  d'  -> switch xs' d'
+                                     Snd   _    d'  -> d'
+                                     Both  _    d'  -> d')
+
+-- | This function is similar to 'switch', but the (future) second
+-- signal may depend on the last value of the first signal.
+switchS :: Stable a => Sig a -> O (a -> Sig a) -> Sig a
+switchS (x ::: xs) d = x ::: delay (case select xs d of
+                                     Fst   xs'  d'  -> switchS xs' d'
+                                     Snd   _    f  -> f x
+                                     Both  _    f  -> f x)
+
+-- | This function is similar to 'switch' but works on delayed signals
+-- instead of signals.
+switchAwait :: O (Sig a) -> O (Sig a) -> O (Sig a)
+switchAwait xs ys = delay (case select xs ys of
+                                  Fst  xs'  d'  -> switch xs' d'
+                                  Snd  _    d'  -> d'
+                                  Both _    d'  -> d')
+
+-- | This function interleaves two signals producing a new value @v@
+-- whenever either input stream produces a new value @v@. In case the
+-- input signals produce a new value simultaneously, the function
+-- argument is used break ties, i.e. to compute the new output value based
+-- on the two new input values
+--
+-- Example:
+--
+-- >                         xs: 1 3   5 3 1 3
+-- >                         ys:   0 2   4
+-- >
+-- > interleave (box (+)) xs ys: 1 3 2 5 7 1 3
+interleave :: Box (a -> a -> a) -> O (Sig a) -> O (Sig a) -> O (Sig a)
+interleave f xs ys = delay (case select xs ys of
+                              Fst (x ::: xs') ys' -> x ::: interleave f xs' ys'
+                              Snd xs' (y ::: ys') -> y ::: interleave f xs' ys'
+                              Both (x ::: xs') (y ::: ys') -> unbox f x y ::: interleave f xs' ys')
+
+
+-- | This function is a variant of combines the values of two signals
+-- using the function argument. @zipWith f xs ys@ produces a new value
+-- @unbox f x y@ whenever @xs@ or @ys@ produce a new value, where @x@
+-- and @y@ are the current values of @xs@ and @ys@, respectively.
+--
+-- Example:
+--
+-- >                      xs:  1 2 3     2
+-- >                      ys:  1     0 5 2
+-- >
+-- > zipWith (box (+)) xs ys:  2 3 4 3 8 4
+
+zipWith :: (Stable a, Stable b) => Box(a -> b -> c) -> Sig a -> Sig b -> Sig c
+zipWith f (a ::: as) (b ::: bs) = unbox f a b ::: delay (
+    case select as bs of
+      Fst as' lbs -> zipWith f as' (b ::: lbs)
+      Snd las bs' -> zipWith f (a ::: las) bs'
+      Both as' bs' -> zipWith f as' bs'
+  )
+
+-- | Variant of 'zipWith' with three signals.
+zipWith3 :: forall a b c d. (Stable a, Stable b, Stable c) => Box(a -> b -> c -> d) -> Sig a -> Sig b -> Sig c -> Sig d
+zipWith3 f as bs cs = zipWith (box (\f x -> unbox f x)) cds cs
+  where cds :: Sig (Box (c -> d))
+        cds = zipWith (box (\a b -> box (\ c -> unbox f a b c))) as bs
+
+-- | If-then-else lifted to signals. @cond bs xs ys@ produces a stream
+-- whose value is taken from @xs@ whenever @bs@ is true and from @ys@
+-- otherwise.
+cond :: Stable a => Sig Bool -> Sig a -> Sig a -> Sig a
+cond = zipWith3 (box (\b x y -> if b then x else y))
+
+
+-- | This is a special case of 'zipWith' using the tupling
+-- function. That is,
+--
+-- > zip = zipWith (box (:*))
+zip :: (Stable a, Stable b) => Sig a -> Sig b -> Sig (a:*b)
+zip = zipWith (box (:*))
+
+-- | Sampling interval (in microseconds) for the 'integral' and
+-- 'derivative' functions.
+
+dt :: Int
+dt = 20000
+
+-- | @integral x xs@ computes the integral of the signal @xs@ with the
+-- constant @x@. For example, if @xs@ is the velocity of an object,
+-- the signal @integral 0 xs@ describes the distance travelled by that
+-- object.
+integral :: forall a v . (VectorSpace v a, Eq v, Fractional a, Stable v, Stable a)
+  => v -> Sig v -> Sig v
+integral = int 
+  where int cur (x ::: xs)
+          | x == zeroVector = cur ::: delay (int cur (adv xs))
+          | otherwise = cur ::: delay (
+              case select xs (unbox (timer dt)) of
+                Fst xs' _ -> int cur xs'
+                Snd xs' () -> int (dtf *^ (cur ^+^ x)) (x ::: xs')
+                Both (x' ::: xs') () ->  int (dtf *^ (cur ^+^ x')) (x'::: xs'))
+         -- sampling interval in seconds
+        dtf :: a
+        dtf = fromRational (fromIntegral dt % 1000000)
+                
+-- | Compute the derivative of a signal. For example, if @xs@ is the
+-- velocity of an object, the signal @derivative xs@ describes the
+-- acceleration travelled by that object.
+derivative :: forall a v . (VectorSpace v a, Eq v, Fractional a, Stable v, Stable a)
+  => Sig v -> Sig v
+derivative xs = der zeroVector (current xs) xs where
+  -- inverse sampling interval in seconds
+  dtf :: a
+  dtf = fromIntegral dt * 0.000001
+
+  der :: v -> v -> Sig v -> Sig v
+  der d last (x:::xs)
+    | d == zeroVector = zeroVector ::: delay
+                        (let x' ::: xs' = adv xs
+                         in der ((x' ^-^ x) ^/ dtf) x (x' ::: xs'))
+    | otherwise = d ::: delay (
+        case select xs (unbox (timer dt)) of
+          Fst xs' _ -> der d last xs'
+          Snd xs' () -> der ((x ^-^ last) ^/ dtf) x (x ::: xs')
+          Both (x' ::: xs') () ->  der ((x' ^-^ last) ^/ dtf) x' (x' ::: xs'))
+
+-- Prevent functions from being inlined too early for the rewrite
+-- rules to fire.
+
+{-# NOINLINE [1] map #-}
+{-# NOINLINE [1] const #-}
+{-# NOINLINE [1] scan #-}
+{-# NOINLINE [1] scanMap #-}
+{-# NOINLINE [1] zip #-}
+
+
+{-# 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 ;
+
+  "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
+#-}
+
+
+#if __GLASGOW_HASKELL__ >= 808
+{-# RULES
+  "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 ;
+
+#-}
+#endif
diff --git a/src/AsyncRattus/Strict.hs b/src/AsyncRattus/Strict.hs
new file mode 100644
--- /dev/null
+++ b/src/AsyncRattus/Strict.hs
@@ -0,0 +1,206 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | This module contains strict versions of some standard data
+-- structures.
+
+
+
+module AsyncRattus.Strict
+  ( List(..),
+    singleton,
+    fromList,
+    toList,
+    init',
+    reverse',
+    (+++),
+    listToMaybe',
+    map',
+    zip',
+    zipWith',
+    mapMaybe',
+    (:*)(..),
+    Maybe'(..),
+    maybe',
+    fromMaybe',
+    fst',
+    snd',
+    curry',
+    uncurry'
+  )where
+
+import Prelude hiding (map)
+import Data.VectorSpace
+
+infixr 2 :*
+infixr 8 :!
+
+-- | Strict list type.
+data List a = Nil | !a :! !(List a)
+
+singleton :: a -> List a
+singleton x = x :! Nil
+
+fromList :: [a] -> List a
+fromList [] = Nil
+fromList (x : xs) = x :! fromList xs
+
+toList :: List a -> [a]
+toList Nil = []
+toList (x :! xs) = x : toList xs
+
+-- | Remove the last element from a list if there is one, otherwise
+-- return 'Nil'.
+init' :: List a -> List a
+init' Nil = Nil
+init' (_ :! Nil) = Nil
+init' (x :! xs) = x :! init' xs
+
+-- | 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)
+    
+-- | Returns @'Nothing''@ on an empty list or @'Just'' a@ where @a@ is the
+-- first element of the list.
+listToMaybe' :: List a -> Maybe' a
+listToMaybe' Nil = Nothing'
+listToMaybe' (x :! _) = Just' x
+
+-- | Append two lists.
+(+++) :: List a -> List a -> List a
+(+++) Nil     ys = ys
+(+++) (x:!xs) ys = x :! xs +++ ys
+
+
+map' :: (a -> b) -> List a -> List b
+map' _ Nil = Nil
+map' f (x :! xs) = f x :! map' f xs
+
+zip' :: List a -> List b -> List (a :* b)
+zip' Nil _ = Nil
+zip' _ Nil = Nil
+zip' (x :! xs) (y :! ys) = (x :* y) :! zip' xs ys
+
+zipWith' :: (a -> b -> c) -> List a -> List b -> List c
+zipWith' _ Nil _ = Nil
+zipWith' _ _ Nil = Nil
+zipWith' f (x :! xs) (y :! ys) = f x y :! zipWith' f 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
+    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 = map'
+
+instance Eq a => Eq (List a) where
+  Nil == Nil = True
+  Nil == _ = False
+  _ == Nil = False
+  (x :! xs) == (y :! ys) = if x == y then xs == ys else False
+
+instance Show a => Show (List a) where
+  show Nil = "Nil"
+  show (x :! xs) = show x ++ " :! " ++ show xs
+
+-- | Strict variant of 'Maybe'.
+data Maybe' a = Just' !a | Nothing'
+
+instance Eq a => Eq (Maybe' a) where
+  Nothing' == Nothing' = True
+  Just' x == Just' y = x == y
+  _ == _ = False
+
+instance Show a => Show (Maybe' a) where
+  show Nothing' = "Nothing'"
+  show (Just' x) = "Just' " ++ show x
+
+-- | 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
+
+fromMaybe' :: a -> Maybe' a -> a
+fromMaybe' _ (Just' x) = x
+fromMaybe' d Nothing' = d
+
+-- | 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
+
+curry' :: ((a :* b) -> c) -> a -> b -> c
+curry' f x y = f (x :* y)
+
+uncurry' :: (a -> b -> c) -> (a :* b) -> c
+uncurry' f (x :* y) = f x y
+
+
+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 ++ ")"
+
+instance (Eq a, Eq b) => Eq (a :* b) where
+  (x1 :* y1) == (x2 :* y2) = x1 == x2 && y1 == y2
+
+
+instance (VectorSpace v a, VectorSpace w a, Floating a, Eq a) => VectorSpace (v :* w) a where
+  zeroVector = zeroVector :* zeroVector
+
+  a *^ (x :* y) = (a *^ x) :* (a *^ y)
+
+  (x :* y) ^/ a = (x ^/ a) :* (y ^/ a)
+
+  negateVector (x :* y) = (negateVector x) :* (negateVector y)
+
+  (x1 :* y1) ^+^ (x2 :* y2) = (x1 ^+^ x2) :* (y1 ^+^ y2)
+
+  (x1 :* y1) ^-^ (x2 :* y2) = (x1 ^-^ x2) :* (y1 ^-^ y2)
+
+  (x1 :* y1) `dot` (x2 :* y2) = (x1 `dot` x2) + (y1 `dot` y2)
+
+  
diff --git a/test/IllTyped.hs b/test/IllTyped.hs
new file mode 100644
--- /dev/null
+++ b/test/IllTyped.hs
@@ -0,0 +1,170 @@
+{-# LANGUAGE RebindableSyntax #-}
+
+module Main (module Main) where
+
+import AsyncRattus
+import AsyncRattus.Signal as S
+import Prelude
+import AsyncRattus.Plugin.Annotation (InternalAnn (..))
+
+
+{-# ANN module AsyncRattus #-}
+
+
+{-# ANN loopIndirect ExpectError #-}
+loopIndirect :: Sig Int
+loopIndirect = run
+  where run :: Sig Int
+        run = loopIndirect
+
+{-# ANN loopIndirect' ExpectError #-}
+loopIndirect' :: Sig Int
+loopIndirect' = let run = loopIndirect' in run
+
+{-# ANN nestedUnguard ExpectError #-}
+nestedUnguard :: Sig Int
+nestedUnguard = run 0
+  where run :: Int -> Sig Int
+        run 0 = nestedUnguard
+        run n = n ::: delay (run (n-1))
+
+{-# ANN advDelay ExpectError #-}
+advDelay :: O (O a) -> O a
+advDelay y = delay (let x = adv y in adv x)
+
+{-# ANN advDelay' ExpectError #-}
+advDelay' :: O a -> a
+advDelay' y = let x = adv y in x
+
+{-# ANN dblAdv ExpectError #-}
+dblAdv :: O (O a) -> O a
+dblAdv y = delay (adv (adv y))
+
+{-# ANN advScope ExpectError #-}
+advScope :: O (O Int -> Int)
+advScope = delay (\x -> adv x)
+
+{-# ANN advScope' ExpectError #-}
+advScope' :: O (Int -> Int)
+advScope' = delay (let f x =  adv (delay x) in f)
+
+{-# ANN grec ExpectError #-}
+grec :: a
+grec = grec
+
+{-# ANN boxStream ExpectError #-}
+boxStream :: Sig Int -> Box (Sig Int)
+boxStream s = box (0 ::: future s)
+
+{-# ANN boxStream' ExpectError #-}
+boxStream' :: Sig Int -> Box (Sig Int)
+boxStream' s = box s
+
+{-# ANN intDelay ExpectError #-}
+intDelay :: Int -> O Int
+intDelay = delay
+
+{-# ANN intAdv ExpectError #-}
+intAdv :: O Int -> Int
+intAdv = adv
+
+
+{-# ANN newDelay ExpectError #-}
+newDelay :: a -> O a
+newDelay x = delay x
+
+{-# ANN mutualLoop ExpectError #-}
+mutualLoop :: a
+mutualLoop = mutualLoop'
+
+{-# ANN mutualLoop' ExpectError #-}
+mutualLoop' :: a
+mutualLoop' = mutualLoop
+
+{-# ANN constUnstable ExpectError #-}
+constUnstable :: a -> Sig a
+constUnstable a = run
+  where run = a ::: delay run
+
+{-# ANN mapUnboxed ExpectError #-}
+mapUnboxed :: (a -> b) -> Sig a -> Sig b
+mapUnboxed f = run
+  where run (x ::: xs) = f x ::: delay (run (adv xs))
+
+{-# ANN mapUnboxedMutual ExpectError #-}
+mapUnboxedMutual :: (a -> b) -> Sig a -> Sig b
+mapUnboxedMutual f = run
+  where run (x ::: xs) = f x ::: delay (run' (adv xs))
+        run' (x ::: xs) = f x ::: delay (run (adv xs))
+
+-- mutual recursive pattern definitions are not supported
+-- foo1,foo2 :: Box (a -> b) -> Sig a -> Sig b
+-- (foo1,foo2) = (\ f (x ::: xs) -> unbox f x ::: (delay (foo2 f) <#> xs),
+--                \ f (x ::: xs) -> unbox f x ::: (delay (foo1 f) <#> xs))
+
+{-# ANN nestedPattern ExpectError #-}
+nestedPattern :: Box (a -> b) -> Sig a -> Sig b
+nestedPattern = foo1 where
+  foo1,foo2 :: Box (a -> b) -> Sig a -> Sig b
+  (foo1,foo2) = (\ f (x ::: xs) -> unbox f x ::: (delay (foo2 f (adv xs))),
+                 \ f (x ::: xs) -> unbox f x ::: (delay (foo1 f (adv xs))))
+
+
+data Input = Input {jump :: !Bool, move :: Move}
+data Move = StartLeft | EndLeft | StartRight | EndRight | NoMove
+
+{-# ANN constS ExpectError #-}
+-- Input is not a stable type (it is not strict). Therefore this
+-- should not type check.
+constS :: Input -> Sig Input
+constS a = a ::: delay (constS a)
+
+
+{-# ANN incompatibleAdv ExpectError #-}
+incompatibleAdv :: O Int -> O Int -> O Int
+incompatibleAdv li lk = delay (adv li + adv lk)
+
+{-# ANN incompatibleAdvSelect ExpectError #-}
+incompatibleAdvSelect :: O Int -> O Int -> O Int
+incompatibleAdvSelect li lk = delay (select li lk `seq` adv li)
+
+{-# ANN intPlusOne ExpectError #-}
+intPlusOne :: O Int -> Int
+intPlusOne laterI = adv laterI + 1
+
+{-# ANN weirdPlusTwo ExpectError #-}
+weirdPlusTwo :: O Int -> O Int
+weirdPlusTwo x = delay (
+        let doAdd = box ((+) 1)
+            x' = x
+            newLater = delay (unbox doAdd (adv x'))
+        in unbox doAdd (adv newLater)
+    )
+
+{-# ANN stutter ExpectError #-}
+stutter :: Int -> Sig Int
+stutter n = n ::: delay (n ::: delay (stutter (n+1)))
+
+{-# ANN advAlias ExpectError #-}
+advAlias :: O a -> a
+advAlias = adv
+
+{-# ANN selectAlias ExpectError #-}
+selectAlias :: O a -> O b -> Select a b
+selectAlias = select
+
+{-# ANN partialSelectApp ExpectError #-}
+partialSelectApp :: O a -> (O b -> Select a b)
+partialSelectApp l = select l
+
+{-# ANN doubleAdv ExpectError #-}
+doubleAdv :: O Int -> O Int
+doubleAdv li =  delay (adv li + adv li)
+
+{-# ANN addDelay ExpectError #-}
+addDelay :: O Int -> O Int -> O Int
+addDelay x y = delay (adv x + adv y)
+
+
+{-# ANN main NotAsyncRattus #-}
+main = putStrLn "This file should not type check"
diff --git a/test/WellTyped.hs b/test/WellTyped.hs
new file mode 100644
--- /dev/null
+++ b/test/WellTyped.hs
@@ -0,0 +1,138 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE StrictData #-}
+{-# OPTIONS -fplugin=AsyncRattus.Plugin #-}
+
+module Main (module Main) where
+
+import AsyncRattus
+import AsyncRattus.Signal
+import Data.Set as Set
+
+
+
+{-# ANN module AsyncRattus #-}
+
+boxedInt :: Box Int
+boxedInt = box 8
+
+
+lambdaUnderDelay :: O Int -> O ((Int -> Int -> Int) :* Int)
+lambdaUnderDelay d = delay ((\x _ -> x) :* adv d)
+
+sneakyLambdaUnderDelay :: O Int -> O ((Int -> Int -> Int) :* Int)
+sneakyLambdaUnderDelay d = delay (let f x _ =  x in f :* adv d)
+
+
+lambdaUnderDelay' :: Int -> O Int -> O ((Int -> Int) :* Int)
+lambdaUnderDelay' x d = delay ((\_ -> x) :* adv d)
+
+sneakyLambdaUnderDelay' :: Int -> O Int -> O ((Int -> Int) :* Int)
+sneakyLambdaUnderDelay' x d = delay ((let f _ =  x in f) :* adv d)
+
+
+scanBox :: Box(b -> a -> Box b) -> b -> Sig a -> Sig b
+scanBox f acc (a ::: as) =  unbox acc' ::: delay (scanBox f (unbox acc') (adv as))
+  where acc' = unbox f acc a
+
+sumBox :: Sig Int -> Sig Int
+sumBox = scanBox (box (\x y -> box (x + y))) 0
+
+strMap :: Box (a -> b) -> Sig a -> Sig b
+strMap f (x ::: xs) = unbox f x ::: delay (strMap f (adv xs))
+
+strMap' :: Box (a -> b) -> Sig a -> Sig b
+strMap' f = run
+  where run (x ::: xs) = unbox f x ::: delay (run (adv xs))
+
+
+
+-- local mutual recursive definition
+nestedMutual :: Sig Int -> Sig Int
+nestedMutual = lbar1 (box (+1))
+  where lbar1 :: Box (a -> b) -> Sig a -> Sig b
+        lbar1 f (x ::: xs) = unbox f x ::: (delay (lbar2 f (adv xs)))
+
+        lbar2 :: Box (a -> b) -> Sig a -> Sig b
+        lbar2 f  (x ::: xs) = unbox f x ::: (delay (lbar1 f (adv xs)))
+
+
+
+-- mutual recursive definition
+bar1 :: Box (a -> b) -> Sig a -> Sig b
+bar1 f (x ::: xs) = unbox f x ::: delay (bar2 f (adv xs))
+
+bar2 :: Box (a -> b) -> Sig a -> Sig b
+bar2 f  (x ::: xs) = unbox f x ::: delay (bar1 f (adv xs))
+
+stableDelay :: Stable a => Box (a -> a -> a) -> a -> O a -> O a
+stableDelay f v l = delay (unbox f v (adv l))
+
+patternBinding :: Sig Int -> Sig Int
+patternBinding str = (x + 1) ::: (delay (patternBinding (adv xs)))
+  where (x ::: xs) = sumBox str
+
+
+data Input a = Input {jump :: !a, move :: !Move}
+data Move = StartLeft | EndLeft | StartRight | EndRight | NoMove
+
+
+
+-- The compiler plugin should detect that Input is a stable type and
+-- thus remains in scope under the delay.
+constS :: Stable a => Input a -> O Int -> Sig (Int :* Input a)
+constS a l = (0 :* a) ::: delay ((adv l :* a) ::: never)
+
+-- make sure that unit is recognized as stable
+constU :: () -> O () -> Sig (() :* ())
+constU a l = (() :* a) ::: delay ((adv l :* a) ::: never)
+
+
+scan1 :: (Stable b) => Box(b -> a -> b) -> b -> Sig a -> Sig 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 -> Sig a -> Sig b
+scan2 f = run
+  where run acc (a ::: as) = let acc' = unbox f acc a
+                             in acc' ::: delay (run acc' (adv as))
+
+scanSet :: Sig Int -> Sig (Set Int)
+scanSet = scan1 (box (\ s x -> Set.insert x s)) Set.empty
+
+myMap :: Sig Int -> Sig Int
+myMap (x ::: xs) = (x + 1) ::: delay (fst' (myMap (adv xs) :* nats never))
+
+nats :: O Int -> Sig Int
+nats l = 0 ::: delay (let (n ::: ns) = myMap (nats never) in (adv l + n) ::: ns)
+
+nestedDelay :: Sig a -> Sig a
+nestedDelay (a ::: as) = a ::: delay (let x ::: xs = adv as in x ::: delay (nestedDelay (adv xs)))
+
+
+naiveIf :: Bool -> O a -> O a -> O (Bool :* a)
+naiveIf b x y = delay (b :* adv (if b then x else y))
+
+naiveIf' :: Bool -> O a -> O a -> O (Bool :* a)
+naiveIf' b x y = delay (b :* adv later)
+    where
+        later = case b of
+            True -> x
+            False -> y
+
+advUnderLambda :: O Int -> O (a -> Int)
+advUnderLambda y = delay (\_ -> adv y)
+
+
+dblAdv :: O (O a) -> O (O a)
+dblAdv y = delay (delay (adv (adv y)))
+
+delayAdvUnderLambda :: O () -> O (O Int -> O Int)
+delayAdvUnderLambda d = delay (adv d `seq` \x -> delay (adv x))
+
+-- This function is leaky unless the single tick transformation is
+-- performed
+leaky :: Sig () -> (() -> Bool) -> Sig Bool
+leaky (() ::: d) p = p () ::: delay (let d' = adv d in (leaky d' (\ _ -> current (leaky d' (\ _ -> True)))))
+
+{-# ANN main NotAsyncRattus #-}
+main = putStrLn "This file should just type check"