diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,16 @@
+0.5
+---
+
+The typing rules for delay, functions, and guarded recursion have been
+simplified and generalised. Instead of just one tick, Rattus now
+allows an arbitrary number of ticks as well as function definitions in
+the scope of ticks. In practical terms, this means the following:
+
+- As before, delays can be nested arbitrarily and function definitions
+  may occur under arbitrarily many delays.
+- But now the scope of a delay is no longer interrupted by a nested
+  delay or function definition.
+
 0.4
 ---
 
diff --git a/Rattus.cabal b/Rattus.cabal
--- a/Rattus.cabal
+++ b/Rattus.cabal
@@ -1,6 +1,6 @@
 cabal-version:       1.18
 name:                Rattus
-version:             0.4
+version:             0.5
 category:            FRP
 synopsis:            A modal FRP language
 description:
@@ -146,14 +146,16 @@
                        Rattus.Plugin
                        Rattus.Arrow
                        Rattus.Primitives
-                       
-  other-modules:       Rattus.Plugin.ScopeCheck
                        Rattus.Plugin.Annotation
+                                              
+  other-modules:       Rattus.Plugin.ScopeCheck
+                       Rattus.Plugin.SingleTick
+                       Rattus.Plugin.CheckSingleTick
                        Rattus.Plugin.Strictify
                        Rattus.Plugin.Utils
                        Rattus.Plugin.Dependency
                        Rattus.Plugin.StableSolver
-  build-depends:       base >=4.12 && <5, containers, ghc >= 8.6 && < 8.11, ghc-prim, simple-affine-space
+  build-depends:       base >=4.12 && <5, containers, ghc >= 8.6 && < 9.1, ghc-prim, simple-affine-space, transformers
   hs-source-dirs:      src
   default-language:    Haskell2010
   ghc-options:         -W
diff --git a/docs/paper.pdf b/docs/paper.pdf
Binary files a/docs/paper.pdf and b/docs/paper.pdf differ
diff --git a/src/Rattus/Plugin.hs b/src/Rattus/Plugin.hs
--- a/src/Rattus/Plugin.hs
+++ b/src/Rattus/Plugin.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE CPP #-}
 
 
 -- | The plugin to make it all work.
@@ -8,20 +9,25 @@
 import Rattus.Plugin.StableSolver
 import Rattus.Plugin.ScopeCheck
 import Rattus.Plugin.Strictify
+import Rattus.Plugin.SingleTick
+import Rattus.Plugin.CheckSingleTick
 import Rattus.Plugin.Utils
 import Rattus.Plugin.Annotation
 
 import Prelude hiding ((<>))
-import GhcPlugins
-import TcRnTypes
 
-
 import Control.Monad
 import Data.Maybe
 import Data.Data hiding (tyConName)
-
-
+import qualified Data.Set as Set
 
+#if __GLASGOW_HASKELL__ >= 900
+import GHC.Plugins
+import GHC.Tc.Types
+#else
+import GhcPlugins
+import TcRnTypes
+#endif
 
 -- | Use this to enable Rattus' plugin, either by supplying the option
 -- @-fplugin=Rattus.Plugin@ directly to GHC. or by including the
@@ -37,34 +43,55 @@
   }
 
 
+data Options = Options {debugMode :: Bool}
+
 typechecked :: [CommandLineOption] -> ModSummary -> TcGblEnv -> TcM TcGblEnv
 typechecked _ _ env = checkAll env >> return env
 
 install :: [CommandLineOption] -> [CoreToDo] -> CoreM [CoreToDo]
-install _ todo = return (strPass : todo)
-    where strPass = CoreDoPluginPass "Rattus strictify" strictifyProgram
+install opts todo = return (strPass : todo)
+    where strPass = CoreDoPluginPass "Rattus strictify" (strictifyProgram Options{debugMode = dmode})
+          dmode = "debug" `elem` opts
 
-strictifyProgram :: ModGuts -> CoreM ModGuts
-strictifyProgram guts = do
-  newBinds <- mapM (strictify guts) (mg_binds guts)
+-- | Apply the following operations to all 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 :: ModGuts -> CoreBind -> CoreM (CoreBind)
-strictify guts b@(Rec bs) = do
+strictify :: Options -> ModGuts -> CoreBind -> CoreM (CoreBind)
+strictify opts guts b@(Rec bs) = do
   tr <- liftM or (mapM (shouldTransform guts . fst) bs)
   if tr then do
     let vs = map fst bs
     es' <- mapM (\ (v,e) -> do
+                    e' <- toSingleTick e
                     lazy <- allowLazyData guts v
-                    strictifyExpr (SCxt (nameSrcSpan $ getName v) (not lazy))e) bs
+                    e'' <- strictifyExpr (SCxt (nameSrcSpan $ getName v) (not lazy))e'
+                    checkExpr CheckExpr{ recursiveSet = Set.fromList vs, oldExpr = e,
+                                         fatalError = False, verbose = debugMode opts} e''
+                    return e'') bs
     return (Rec (zip vs es'))
   else return b
-strictify guts b@(NonRec v e) = do
+strictify opts guts b@(NonRec v e) = do
     tr <- shouldTransform guts v
     if tr then do
+      -- liftIO $ putStrLn "-------- old --------"
+      -- liftIO $ putStrLn (showSDocUnsafe (ppr e))
+      e' <- toSingleTick e
+      -- liftIO $ putStrLn "-------- new --------"
+      -- liftIO $ putStrLn (showSDocUnsafe (ppr e'))
       lazy <- allowLazyData guts v
-      e' <- strictifyExpr (SCxt (nameSrcSpan $ getName v) (not lazy)) e
-      return (NonRec v e')
+      e'' <- strictifyExpr (SCxt (nameSrcSpan $ getName v) (not lazy)) e'
+      checkExpr CheckExpr{ recursiveSet = Set.empty, oldExpr = e,
+                           fatalError = False, verbose = debugMode opts} e''
+      return (NonRec v e'')
     else return b
 
 getModuleAnnotations :: Data a => ModGuts -> [a]
@@ -86,12 +113,19 @@
 shouldTransform :: ModGuts -> CoreBndr -> CoreM Bool
 shouldTransform guts bndr = do
   l <- annotationsOn guts bndr :: CoreM [Rattus]
-  return (Rattus `elem` l && not (NotRattus `elem` l) && userFunction bndr)
+  l' <- annotationsOn guts bndr :: CoreM [InternalAnn]
+  return ((Rattus `elem` l && not (NotRattus `elem` l) && userFunction bndr) && not (ExpectError `elem` l'))
 
 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/Rattus/Plugin/Annotation.hs b/src/Rattus/Plugin/Annotation.hs
--- a/src/Rattus/Plugin/Annotation.hs
+++ b/src/Rattus/Plugin/Annotation.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE DeriveDataTypeable #-}
-module Rattus.Plugin.Annotation (Rattus(..)) where
+module Rattus.Plugin.Annotation (Rattus(..), InternalAnn (..)) where
 
 import Data.Data
 
@@ -28,3 +28,7 @@
 -- > {-# ANN module AllowLazyData #-}
 
 data Rattus = Rattus | NotRattus | AllowLazyData deriving (Typeable, Data, Show, Eq)
+
+
+-- | This annotation type is for internal use only.
+data InternalAnn = ExpectError | ExpectWarning deriving (Typeable, Data, Show, Eq, Ord)
diff --git a/src/Rattus/Plugin/CheckSingleTick.hs b/src/Rattus/Plugin/CheckSingleTick.hs
new file mode 100644
--- /dev/null
+++ b/src/Rattus/Plugin/CheckSingleTick.hs
@@ -0,0 +1,251 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE CPP #-}
+
+-- | This module implements the check that the transformed code is
+-- typable in the single tick calculus.
+
+module Rattus.Plugin.CheckSingleTick
+  (checkExpr, CheckExpr (..)) where
+
+#if __GLASGOW_HASKELL__ >= 900
+import GHC.Plugins
+#else
+import GhcPlugins
+#endif
+
+import Rattus.Plugin.Utils 
+
+import Prelude hiding ((<>))
+import Control.Monad
+import Data.Set (Set)
+import qualified Data.Set as Set
+import Data.Map (Map)
+import qualified Data.Map as Map
+import Control.Applicative
+import Data.Foldable
+
+type LCtx = Set Var
+data HiddenReason = BoxApp | AdvApp | NestedRec Var | FunDef | DelayApp
+type Hidden = Map Var HiddenReason
+
+data Prim = Delay | Adv | Box | Arr
+
+data TypeError = TypeError SrcSpan SDoc
+
+instance Outputable Prim where
+  ppr Delay = "delay"
+  ppr Adv = "adv"
+  ppr Box = "box"
+  ppr Arr = "arr"
+  
+data Ctx = Ctx
+  { current :: LCtx,
+    hidden :: Hidden,
+    earlier :: Maybe LCtx,
+    srcLoc :: SrcSpan,
+    recDef :: Set Var, -- ^ recursively defined variables 
+    stableTypes :: Set Var,
+    primAlias :: Map Var Prim,
+    -- number of ticks (for recursive calls). This is to allow
+    -- recursive definitions of the form @f = delay (delay (adv f))@.
+    ticks :: Int} 
+
+primMap :: Map FastString Prim
+primMap = Map.fromList
+  [("delay", Delay),
+   ("adv", Adv),
+   ("box", Box),
+   ("arr", Arr)
+   ]
+
+
+isPrim :: Ctx -> Var -> Maybe Prim
+isPrim c v
+  | Just p <- Map.lookup v (primAlias c) = Just p
+  | otherwise = do
+  (name,mod) <- getNameModule v
+  if isRattModule mod then Map.lookup name primMap
+  else Nothing
+
+
+
+stabilize :: HiddenReason -> Ctx -> Ctx
+stabilize hr c = c
+  {current = Set.empty,
+   earlier = Nothing,
+   hidden = hidden c `Map.union` Map.fromSet (const hr) ctxHid,
+   ticks = 0}
+  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 ticks c > 0 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 -> 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 -> CoreM (Maybe TypeError)
+typeError cxt var doc =
+  return (Just (TypeError (pickFirst (srcLoc cxt) (nameSrcSpan (varName var))) doc))
+
+
+emptyCtx :: Set Var -> Ctx
+emptyCtx vars =
+  Ctx { current =  Set.empty,
+        earlier = Nothing,
+        hidden = Map.empty,
+        srcLoc = noLocationInfo,
+        recDef = vars,
+        primAlias = Map.empty,
+        stableTypes = Set.empty,
+        ticks = 0}
+
+
+isPrimExpr :: Ctx -> Expr Var -> Maybe (Prim,Var)
+isPrimExpr c (App e (Type _)) = isPrimExpr c e
+isPrimExpr c (App e e') | not $ tcIsLiftedTypeKind $ typeKind $ exprType e' = isPrimExpr c e
+isPrimExpr c (Var v) = fmap (,v) (isPrim c v)
+isPrimExpr c (Tick _ e) = isPrimExpr c e
+isPrimExpr c (Lam v e)
+  | isTyVar v || (not $ tcIsLiftedTypeKind $ typeKind $ varType v) = isPrimExpr c e
+isPrimExpr _ _ = Nothing
+
+
+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
+
+
+data CheckExpr = CheckExpr{
+  recursiveSet :: Set Var,
+  oldExpr :: Expr Var,
+  fatalError :: Bool,
+  verbose :: Bool
+  }
+
+checkExpr :: CheckExpr -> Expr Var -> CoreM ()
+checkExpr c e = do
+  res <- checkExpr' (emptyCtx (recursiveSet c)) e
+  case res of
+    Nothing -> return ()
+    Just (TypeError src doc) ->
+      let sev = if fatalError c then SevError else SevWarning
+      in if verbose c then do
+        printMessage sev src ("Internal error in Rattus Plugin: single tick transformation did not preserve typing." $$ doc)
+        liftIO $ putStrLn "-------- old --------"
+        liftIO $ putStrLn (showSDocUnsafe (ppr (oldExpr c)))
+        liftIO $ putStrLn "-------- new --------"
+        liftIO $ putStrLn (showSDocUnsafe (ppr e))
+         else
+        printMessage sev noSrcSpan ("Internal error in Rattus Plugin: single tick transformation did not preserve typing." $$
+                             "Compile with flags \"-fplugin-opt Rattus.Plugin:debug\" and \"-g2\" for detailed information")
+
+checkExpr' :: Ctx -> Expr Var -> CoreM (Maybe TypeError)
+checkExpr' c (App e e') | isType e' || (not $ tcIsLiftedTypeKind $ typeKind $ exprType e')
+  = checkExpr' c e
+checkExpr' c@Ctx{current = cur, hidden = hid, earlier = earl} (App e1 e2) =
+  case isPrimExpr c e1 of
+    Just (p,v) -> case p of
+      Box -> do
+        checkExpr' (stabilize BoxApp c) e2
+      Arr -> do
+        checkExpr' (stabilize BoxApp c) e2
+
+      Delay -> case earl of
+        Just earl' ->
+          checkExpr' c{current = Set.empty, earlier = Just cur,
+                      ticks = ticks c + 1, hidden = hidden c `Map.union` Map.fromSet (const DelayApp) earl'} e2
+        Nothing -> checkExpr' c{current = Set.empty, earlier = Just cur, ticks = ticks c + 1} e2
+      Adv -> case earl of
+        Just er -> checkExpr' c{earlier = Nothing, current = er, ticks = ticks c - 1,
+                               hidden = hid `Map.union` Map.fromSet (const AdvApp) cur} e2
+        Nothing -> typeError c v (text "can only advance under delay")
+    _ -> liftM2 (<|>) (checkExpr' c e1)  (checkExpr' c e2)
+checkExpr' c (Case e v _ alts) =
+    liftM2 (<|>) (checkExpr' c e) (liftM (foldl' (<|>) Nothing) (mapM (\ (_,vs,e)-> checkExpr' (addVars vs c') e) alts))
+  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 Nothing
+checkExpr' _ (Lit _)  = return Nothing
+checkExpr' _ (Coercion _)  = return Nothing
+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 v e1) e2) =
+  case isPrimExpr c e1 of
+    Just (p,_) -> (checkExpr' (c{primAlias = Map.insert v p (primAlias c)}) e2)
+    Nothing -> liftM2 (<|>) (checkExpr' c e1)  (checkExpr' (addVars [v] c) e2)
+checkExpr' _ (Let (Rec ([])) _) = return Nothing
+checkExpr' c (Let (Rec binds) e2) = do
+    r1 <- mapM (\ (v,e) -> checkExpr' (c' v) e) binds
+    r2 <- checkExpr' (addVars vs c) e2
+    return (foldl' (<|>) Nothing r1 <|> r2)  
+  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 -> typeError c v reason
+             Visible -> return Nothing
+  | otherwise = return Nothing
+
+
+
+addVars :: [Var] -> Ctx -> Ctx
+addVars v c = c{current = Set.fromList v `Set.union` current c }
diff --git a/src/Rattus/Plugin/Dependency.hs b/src/Rattus/Plugin/Dependency.hs
--- a/src/Rattus/Plugin/Dependency.hs
+++ b/src/Rattus/Plugin/Dependency.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE CPP #-}
 
 -- | This module is used to perform a dependency analysis of top-level
@@ -9,23 +10,30 @@
 
 module Rattus.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
-import GHC.Hs.Types
 #else 
 import HsExtension
 import HsExpr
 import HsPat
 import HsBinds
-import HsTypes
 #endif
 
 import Data.Set (Set)
@@ -37,8 +45,6 @@
 
 
 
-
-
 -- | 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)]
@@ -80,8 +86,10 @@
   getBV (PatBind {pat_lhs = pat}) = getBV pat
   getBV (VarBind {var_id = v}) = Set.singleton v
   getBV PatSynBind{} = Set.empty
-  getBV XHsBindsLR{} = Set.empty
-
+#if __GLASGOW_HASKELL__ < 900
+  getBV (XHsBindsLR e) = getBV e
+#endif
+  
 instance HasBV a => HasBV (GenLocated b a) where
   getBV (L _ e) = getBV e
 
@@ -95,6 +103,11 @@
 getConBV (RecCon (HsRecFields {rec_flds = fs})) = foldl run Set.empty fs
       where run s (L _ f) = getBV (hsRecFieldArg f) `Set.union` s
 
+#if __GLASGOW_HASKELL__ >= 900
+instance HasBV CoPat where
+  getBV CoPat {co_pat_inner = p} = getBV p
+#endif
+
 instance HasBV (Pat GhcTc) where
   getBV (VarPat _ (L _ v)) = Set.singleton v
   getBV (LazyPat _ p) = getBV p
@@ -104,8 +117,6 @@
   getBV (ListPat _ ps) = getBV ps
   getBV (TuplePat _ ps _) = getBV ps
   getBV (SumPat _ p _ _) = getBV p
-  getBV (ConPatIn (L _ v) con) = Set.insert v (getConBV con)
-  getBV (ConPatOut {pat_args = con}) = getConBV con
   getBV (ViewPat _ _ p) = getBV p
   getBV (SplicePat _ sp) =
     case sp of
@@ -115,19 +126,24 @@
       HsSpliced _ _ (HsSplicedPat p) -> getBV p
       _ -> Set.empty
   getBV (NPlusKPat _ (L _ v) _ _ _ _) = Set.singleton v
-  getBV (CoPat _ _ p _) = getBV p
   getBV (NPat {}) = Set.empty
   getBV (XPat p) = getBV p
   getBV (WildPat {}) = Set.empty
   getBV (LitPat {}) = Set.empty
-
+#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 (SigPat _ p _) = getBV p
 #else
-  getBV (SigPat _ p) =
+  getBV (SigPat _ p)   = getBV p
 #endif
-    getBV p
 
+
 #if __GLASGOW_HASKELL__ >= 810
 instance HasBV NoExtCon where
 #else
@@ -158,32 +174,45 @@
 
 instance HasFV a => HasFV (MatchGroup GhcTc a) where
   getFV MG {mg_alts = alts} = getFV alts
-  getFV XMatchGroup{} = Set.empty
-
+#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
-  getFV XMatch{} = Set.empty
+#if __GLASGOW_HASKELL__ < 900
+  getFV (XMatch e) = getFV e
+#endif
 
 instance HasFV (HsTupArg GhcTc) where
   getFV (Present _ e) = getFV e
-  getFV _ = Set.empty
-
+  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
-  getFV XGRHS{} = Set.empty
+#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
-  getFV _ = Set.empty
+#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 _ = Set.empty
-
+  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
@@ -196,41 +225,57 @@
   getFV PatBind {pat_rhs = rhs} = getFV rhs
   getFV VarBind {var_rhs = rhs} = getFV rhs
   getFV AbsBinds {abs_binds = bs} = getFV bs
-  getFV _ = Set.empty
-
+  getFV PatSynBind {} = Set.empty
+#if __GLASGOW_HASKELL__ < 900
+  getFV (XHsBindsLR e) = getFV e
+#endif
 
 instance HasFV (IPBind GhcTc) where
   getFV (IPBind _ _ e) = getFV e
-  getFV _ = Set.empty
+#if __GLASGOW_HASKELL__ < 900
+  getFV (XIPBind e) = getFV e
+#endif
 
 instance HasFV (HsIPBinds GhcTc) where
   getFV (IPBinds _ bs) = getFV bs
-  getFV _ = Set.empty
-
+#if __GLASGOW_HASKELL__ < 900
+  getFV (XHsIPBinds e) = getFV e
+#endif
+  
 instance HasFV (ApplicativeArg GhcTc) where
 #if __GLASGOW_HASKELL__ >= 810
-  getFV (ApplicativeArgOne _ _ e _ _)
+  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 _)
-#endif
-    = getFV e
+  getFV (ApplicativeArgOne _ _ e _) = getFV e
   getFV (ApplicativeArgMany _ es e _) = getFV es `Set.union` getFV e
-  getFV XApplicativeArg{} = Set.empty
+#endif
+#if __GLASGOW_HASKELL__ < 900
+  getFV (XApplicativeArg e) = getFV e
+#endif
 
 instance HasFV (ParStmtBlock GhcTc GhcTc) where
   getFV (ParStmtBlock _ es _ _) = getFV es
-  getFV XParStmtBlock{} = Set.empty
-
+#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
-  getFV XStmtLR{} = Set.empty
+#if __GLASGOW_HASKELL__ < 900
+  getFV (XStmtLR e) = getFV e
+#endif
 
 instance HasFV (HsRecordBinds GhcTc) where
   getFV HsRecFields{rec_flds = fs} = getFV fs
@@ -259,13 +304,19 @@
   getFV (HsCmdIf _ _ e1 e2 e3) = getFV e1 `Set.union` getFV e2 `Set.union` getFV e3
   getFV (HsCmdLet _ bs _) = getFV bs
   getFV (HsCmdDo _ cmd) = getFV cmd
+#if __GLASGOW_HASKELL__ >= 900
+  getFV (HsCmdLamCase _ mg) = getFV mg
+#else
   getFV (HsCmdWrap _ _ cmd) = getFV cmd
-  getFV XCmd{} = Set.empty
+#endif
+  getFV (XCmd e) = getFV e
   
 
 instance HasFV (HsCmdTop GhcTc) where
   getFV (HsCmdTop _ cmd) = getFV cmd
-  getFV XCmdTop{} = Set.empty
+#if __GLASGOW_HASKELL__ < 900
+  getFV (XCmdTop e) = getFV e
+#endif
 
 instance HasFV (HsExpr GhcTc) where
   getFV (HsVar _ v) = getFV v
@@ -278,15 +329,7 @@
   getFV HsLit {} = Set.empty
   getFV (HsLam _ mg) = getFV mg
   getFV (HsLamCase _ mg) = getFV mg
-  getFV (HsApp _ e1 e2) = getFV e1 `Set.union` getFV e2
-
-#if __GLASGOW_HASKELL__ >= 808
-  getFV (HsAppType _ e _)
-#else
-  getFV (HsAppType _ e)
-#endif
-    = getFV e
-      
+  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 (HsPar _ e) = getFV e
@@ -295,31 +338,42 @@
   getFV (ExplicitTuple _ es _) = getFV es
   getFV (ExplicitSum _ _ _ e) = getFV e
   getFV (HsCase _ e mg) = getFV e  `Set.union` getFV mg
-  getFV (HsIf _ _ e1 e2 e3) = getFV e1 `Set.union` getFV e2 `Set.union` getFV e3
   getFV (HsMultiIf _ es) = getFV es
   getFV (HsLet _ bs e) = getFV bs `Set.union` getFV e
   getFV (HsDo _ _ e) = getFV e
   getFV (ExplicitList _ _ es) = getFV es
   getFV (RecordCon {rcon_flds = fs}) = getFV fs
   getFV (RecordUpd {rupd_expr = e, rupd_flds = fs}) = getFV e `Set.union` getFV fs
-
-#if __GLASGOW_HASKELL__ >= 808
-  getFV (ExprWithTySig _ e _)
-#else
-  getFV (ExprWithTySig _ e)
-#endif
-    = getFV e
-
   getFV (ArithSeq _ _ e) = getFV e
-  getFV (HsSCC _ _ _ e) = getFV e
-  getFV (HsCoreAnn _ _ _ e) = getFV e
   getFV (HsBracket _ e) = getFV e
   getFV HsRnBracketOut {} = Set.empty
   getFV HsTcBracketOut {} = Set.empty
   getFV HsSpliceE{} = Set.empty
   getFV (HsProc _ _ e) = getFV e
-  getFV (HsStatic _ e) = getFV e
+  getFV (HsStatic _ e) = getFV e  
+  getFV (HsTick _ _ e) = getFV e
+  getFV (HsBinTick _ _ _ e) = getFV e
+  getFV (XExpr e) = getFV e
+  
+#if __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
@@ -328,10 +382,19 @@
   getFV (EViewPat _ e1 e2) = getFV e1 `Set.union` getFV e2
   getFV (ELazyPat _ e) = getFV e
 #endif
-  
-  getFV (HsTick _ _ e) = getFV e
-  getFV (HsBinTick _ _ _ e) = getFV e
-  getFV (HsTickPragma _ _ _ _ e) = getFV e
-  getFV (HsWrap _ _ e) = getFV e
-  getFV XExpr{} = Set.empty
 
+
+#if __GLASGOW_HASKELL__ >= 900
+instance HasFV XXExprGhcTc where
+  getFV (WrapExpr e) = getFV e
+  getFV (ExpansionExpr (HsExpanded _e1 e2)) = getFV e2
+
+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/Rattus/Plugin/ScopeCheck.hs b/src/Rattus/Plugin/ScopeCheck.hs
--- a/src/Rattus/Plugin/ScopeCheck.hs
+++ b/src/Rattus/Plugin/ScopeCheck.hs
@@ -22,9 +22,18 @@
 import Data.IORef
 
 import Prelude hiding ((<>))
+
+#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
@@ -44,6 +53,7 @@
 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
@@ -62,7 +72,7 @@
     current :: LCtxt,
     -- | Variables that are in the typing context, but to the left of a
     -- tick
-    earlier :: Either NoTickReason LCtxt,
+    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,
@@ -100,7 +110,7 @@
          current =  Set.empty,
          earlier = Left NoDelay,
          hidden = Map.empty,
-         srcLoc = UnhelpfulSpan "<no location info>",
+         srcLoc = noLocationInfo,
          recDef = mvar,
          primAlias = Map.empty,
          stableTypes = Set.empty,
@@ -171,11 +181,10 @@
 checkAll env = do
   let dep = dependency (tcg_binds env)
   let bindDep = filter (filterBinds (tcg_mod env) (tcg_ann_env env)) dep
-  err <- liftIO (newIORef [])
-  res <- mapM (checkSCC err) bindDep
-  msgs <- liftIO (readIORef err)
+  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 and res then return () else liftIO exitFailure
+  if res then return () else liftIO exitFailure
 
 
 printAccErrMsgs :: [ErrorMsg] -> TcM ()
@@ -215,17 +224,25 @@
 
 
 instance Scope a => Scope (Match GhcTc a) where
-  check Match{m_pats=ps,m_grhss=rhs} = mod `modifyCtxt` check rhs
-    where mod c = addVars (getBV ps) (if null ps then c else stabilizeLater FunDef c)
+  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 a => Scope (MatchGroup GhcTc a) 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)
@@ -236,8 +253,9 @@
   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)
@@ -255,11 +273,25 @@
     (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 -> TcM Bool
+checkRec b =  liftM2 (&&) (checkPatBind b) (check b)
 
+checkPatBind :: GetCtxt => LHsBindLR GhcTc GhcTc -> TcM Bool
+checkPatBind (L l b) = (\c -> c {srcLoc = l}) `modifyCtxt` checkPatBind' b
 
+checkPatBind' :: GetCtxt => HsBindLR GhcTc GhcTc -> TcM Bool
+checkPatBind' PatBind{} = do
+  printMessage' SevError ("(Mutual) recursive pattern binding definitions are not supported in Rattus")
+  return False
+         
+checkPatBind' AbsBinds {abs_binds = binds} = 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
@@ -270,9 +302,9 @@
       Just reason | res ->
         (printMessage' SevWarning (recReason reason <> " can cause time leaks")) >> return (res, vs)
       _ -> return (res, vs)
-    where check' b@(L l _) = fc l `modifyCtxt` check b
+    where check' b@(L l _) = fc l `modifyCtxt` checkRec b
           fc l c = let
-            ctxHid = either (const $ current c) (Set.union (current c)) (earlier c)
+            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`
@@ -324,15 +356,19 @@
   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
+  
 instance Scope a => Scope (GRHSs GhcTc a) 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
 
@@ -383,11 +419,17 @@
           _ -> return ch
 
       Unbox -> check e2
-      Delay ->  ((\c -> c{current = Set.empty, earlier = Right (current ?ctxt)}) . stabilizeLater DelayApp)
+      Delay ->  ((\c -> c{current = Set.empty,
+                          earlier = case earlier c of
+                                      Left _ -> Right (current c :| [])
+                                      Right cs -> Right (current c <| cs)}))
                   `modifyCtxt` check  e2
       Adv -> case earlier ?ctxt of
-        Right er -> mod `modifyCtxt` check e2
-          where mod c =  c{earlier = Left $ TickHidden AdvApp, current = er,
+        Right (er :| ers) -> mod `modifyCtxt` check e2
+          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.")
@@ -399,26 +441,14 @@
   check HsRecFld{} = return True
   check HsOverLabel{} = return True
   check HsIPVar{} = notSupported "implicit parameters"
-  check HsOverLit{} = return True
-
-  
-#if __GLASGOW_HASKELL__ >= 808
-  check (HsAppType _ e _)
-#else
-  check (HsAppType _ e)
-#endif
-    = check e
-  
+  check HsOverLit{} = return True  
   check (HsTick _ _ e) = check e
   check (HsBinTick _ _ _ e) = check e  
-  check (HsSCC _ _ _ e) = check e
   check (HsPar _ e) = check e
-  check (HsWrap _ _ e) = check e
   check HsLit{} = return True
   check (OpApp _ e1 e2 e3) = and <$> mapM check [e1,e2,e3]
-  check (HsLam _ mg) = stabilizeLater FunDef `modifyCtxt` check mg
-  check (HsLamCase _ mg) = stabilizeLater FunDef `modifyCtxt` check mg
-  check (HsIf _ _ e1 e2 e3) = and <$> mapM check [e1,e2,e3]
+  check (HsLam _ mg) = check mg
+  check (HsLamCase _ 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
@@ -433,12 +463,6 @@
   check (ExplicitList _ _ e) = check e
   check RecordCon { rcon_flds = f} = check f
   check RecordUpd { rupd_expr = e, rupd_flds = fs} = (&&) <$> check e <*> check fs
-#if __GLASGOW_HASKELL__ >= 808
-  check (ExprWithTySig _ e _)
-#else
-  check (ExprWithTySig _ e)
-#endif
-    = check e
   check (ArithSeq _ _ e) = check e
   check HsBracket{} = notSupported "MetaHaskell"
   check HsRnBracketOut{} = notSupported "MetaHaskell"
@@ -448,9 +472,25 @@
     where mod c = addVars (getBV p) (stabilize StableArr c)
   check (HsStatic _ e) = check e
   check (HsDo _ _ e) = fst <$> checkBind e
+  check (XExpr e) = check e
+#if __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 XExpr {} = return True
+  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
@@ -463,11 +503,24 @@
 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
+#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
@@ -481,20 +534,13 @@
     (l,vs) <- checkBind bs
     r <- addVars vs `modifyCtxt` (check e)
     return (r && l)
+#if __GLASGOW_HASKELL__ >= 900
+  check (XCmd (HsWrap _ e)) = check e
+  check (HsCmdLamCase _ e) = check e
+#else
   check (HsCmdWrap _ _ e) = check e
   check XCmd{} = return True
-
-
--- | This is used when checking function definitions. If the context
--- is not ticked, it stays the same. Otherwise, it is stabilized
--- (similar to 'box').
-stabilizeLater :: HiddenReason -> Ctxt -> Ctxt
-stabilizeLater reason c =
-  case earlier c of
-    Left _ -> c
-    Right earl ->
-      c {earlier = Left $ TickHidden reason,
-         hidden = Map.union (hidden c) $ Map.fromSet (const reason) earl}
+#endif
 
 
 instance Scope (ArithSeqInfo GhcTc) where
@@ -512,19 +558,30 @@
 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
   check AbsBinds {abs_binds = binds, abs_ev_vars  = ev} = 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} = mod `modifyCtxt` check matches
+  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
@@ -543,13 +600,63 @@
     _ ->  Nothing
 
 
+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 _ ,_)) = l
+getSCCLoc (CyclicSCC ((L l _,_ ) : _)) = l
+getSCCLoc _ = noLocationInfo
+
+
+checkSCC' ::  Module -> AnnEnv -> SCC (LHsBindLR  GhcTc GhcTc, Set Var) -> TcM (Bool, [ErrorMsg])
+checkSCC' mod anEnv scc = do
+  err <- liftIO (newIORef [])
+  res <- checkSCC err scc
+  msgs <- liftIO (readIORef err)
+  let anns = getInternalAnn 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)
+
+
+getInternalAnn :: Module -> AnnEnv -> SCC (LHsBindLR  GhcTc GhcTc, Set Var) -> Set InternalAnn
+getInternalAnn 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 InternalAnn
+        checkVar v =
+          let anns = findAnns deserializeWithData anEnv (NamedTarget name) :: [InternalAnn]
+              annsMod = findAnns deserializeWithData anEnv (ModuleTarget mod) :: [InternalAnn]
+              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.
@@ -560,7 +667,7 @@
 checkSCC 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,l))) (check b)
+        check' b@(L l _) = setCtxt (emptyCtxt errm (Just (vs,l))) (checkRec b)
 
 -- | Stabilizes the given context, i.e. remove all non-stable types
 -- and any tick. This is performed on checking 'box', 'arr' and
@@ -572,7 +679,7 @@
    earlier = Left $ TickHidden hr,
    hidden = hidden c `Map.union` Map.fromSet (const hr) ctxHid,
    stabilized = Just sr}
-  where ctxHid = either (const $ current c) (Set.union (current c)) (earlier c)
+  where ctxHid = either (const $ current c) (foldl' Set.union (current c)) (earlier c)
         hr = Stabilize sr
 
 data VarScope = Hidden SDoc | Visible | ImplUnboxed
@@ -608,7 +715,7 @@
             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) (Set.member v) (earlier ?ctxt) ->
+              | 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.")
@@ -643,18 +750,26 @@
 isPrimExpr (L _ e) = isPrimExpr' e where
   isPrimExpr' :: GetCtxt => HsExpr GhcTc -> Maybe (Prim,Var)
   isPrimExpr' (HsVar _ (L _ v)) = fmap (,v) (isPrim v)
-  
 #if __GLASGOW_HASKELL__ >= 808
-  isPrimExpr' (HsAppType _ e _)
+  isPrimExpr' (HsAppType _ e _) = isPrimExpr e
 #else
-  isPrimExpr' (HsAppType _ e)
+  isPrimExpr' (HsAppType _ e)   = isPrimExpr e
 #endif
-    = isPrimExpr e
-  isPrimExpr' (HsTick _ _ e) = isPrimExpr e
-  isPrimExpr' (HsBinTick _ _ _ e) = isPrimExpr e  
+
+#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
+  isPrimExpr' (HsTick _ _ e) = isPrimExpr e
+  isPrimExpr' (HsBinTick _ _ _ e) = isPrimExpr e  
   isPrimExpr' (HsPar _ e) = isPrimExpr e
+
   isPrimExpr' _ = Nothing
 
 
diff --git a/src/Rattus/Plugin/SingleTick.hs b/src/Rattus/Plugin/SingleTick.hs
new file mode 100644
--- /dev/null
+++ b/src/Rattus/Plugin/SingleTick.hs
@@ -0,0 +1,201 @@
+-- | This module implements the translation from the multi-tick
+-- calculus to the single tick calculus.
+
+{-# LANGUAGE CPP #-}
+
+module Rattus.Plugin.SingleTick
+  (toSingleTick) where
+
+#if __GLASGOW_HASKELL__ >= 900
+import GHC.Plugins
+#else
+import GhcPlugins
+#endif
+
+  
+import Rattus.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 ->(c,bs,x)) (toSingleTick f)) 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
+
+isVar :: CoreExpr -> Bool
+isVar (App e e')
+  | isType e' || not  (tcIsLiftedTypeKind(typeKind (exprType e'))) = isVar e
+  | otherwise = False
+isVar (Cast e _) = isVar e
+isVar (Tick _ e) = isVar e
+isVar (Var _) = True
+isVar _ = False
+
+
+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))
+
+-- 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 e@(App e1 e2)
+  | isAdvApp e1 = extractAdvApp 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 ->(c,bs,x)) (extractAdv f)) 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.
+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)
+  | 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 ->(c,bs,x)) (extractAdv' f)) 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 (\occ -> occ == "delay")
+
+isBoxApp :: CoreExpr -> Bool
+isBoxApp = isPrimApp (\occ -> occ == "Box" || occ == "box")
+
+isAdvApp :: CoreExpr -> Bool
+isAdvApp = isPrimApp (\occ -> occ == "adv")
+
+
+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) == "Rattus.Internal") ||
+          moduleNameString (moduleName mod) == "Rattus.Primitives"))
diff --git a/src/Rattus/Plugin/StableSolver.hs b/src/Rattus/Plugin/StableSolver.hs
--- a/src/Rattus/Plugin/StableSolver.hs
+++ b/src/Rattus/Plugin/StableSolver.hs
@@ -10,14 +10,28 @@
 import Rattus.Plugin.Utils
 
 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__ >= 810
+#if __GLASGOW_HASKELL__ >= 900
+import GHC.Tc.Types.Constraint
+#elif __GLASGOW_HASKELL__ >= 810
 import Constraint
 #endif
 
@@ -25,7 +39,7 @@
 import qualified Data.Set as Set
 
 
-import TcRnTypes
+
 
 
 -- | Constraint solver plugin for the 'Stable' type class.
diff --git a/src/Rattus/Plugin/Strictify.hs b/src/Rattus/Plugin/Strictify.hs
--- a/src/Rattus/Plugin/Strictify.hs
+++ b/src/Rattus/Plugin/Strictify.hs
@@ -1,10 +1,15 @@
 {-# LANGUAGE OverloadedStrings #-}
-
-module Rattus.Plugin.Strictify where
+{-# LANGUAGE CPP #-}
+module Rattus.Plugin.Strictify
+  (strictifyExpr, SCxt (..)) where
 import Prelude hiding ((<>))
 import Rattus.Plugin.Utils
-import GhcPlugins
 
+#if __GLASGOW_HASKELL__ >= 900
+import GHC.Plugins
+#else
+import GhcPlugins
+#endif
 
 data SCxt = SCxt {srcSpan :: SrcSpan, checkStrictData :: Bool}
 
@@ -29,7 +34,7 @@
    | not (isCoVar b) && not (isTyVar b) && tcIsLiftedTypeKind(typeKind (varType b))
     = do
        e' <- strictifyExpr ss e
-       b' <- mkSysLocalM (fsLit "strict") (varType b)
+       b' <- mkSysLocalFromVar (fsLit "strict") b
        return (Lam b' (Case (varToCoreExpr b') b (exprType e) [(DEFAULT,[],e')]))
    | otherwise = do
        e' <- strictifyExpr ss e
@@ -38,7 +43,7 @@
   e' <- strictifyExpr ss e
   return (Cast e' c)
 strictifyExpr ss (Tick t@(SourceNote span _) e) = do
-  e' <- strictifyExpr (ss{srcSpan = RealSrcSpan span}) e
+  e' <- strictifyExpr (ss{srcSpan = fromRealSrcSpan span}) e
   return (Tick t e')
 strictifyExpr ss (App e1 e2)
   | (checkStrictData ss && not (isType e2) && tcIsLiftedTypeKind(typeKind (exprType e2))
@@ -53,34 +58,3 @@
       e2' <- strictifyExpr ss e2
       return (App e1' e2')
 strictifyExpr _ss e = return e
-
-
-isDelayApp (App e _) = isDelayApp e
-isDelayApp (Cast e _) = isDelayApp e
-isDelayApp (Tick _ e) = isDelayApp e
-isDelayApp (Var v) = isDelayVar v
-isDelayApp _ = False
-
-
-
-
-isDelayVar :: Var -> Bool
-isDelayVar v = maybe False id $ do
-  let name = varName v
-  mod <- nameModule_maybe name
-  let occ = getOccString name
-  return ((occ == "Delay" || occ == "delay") || (occ == "Box" || occ == "delay")
-          && ((moduleNameString (moduleName mod) == "Rattus.Internal") ||
-          moduleNameString (moduleName mod) == "Rattus.Primitives"))
-
-isCase Case{} = True
-isCase (Tick _ e) = isCase e
-isCase (Cast e _) = isCase e
-isCase Lam {} = True
-isCase e = isType e
-
-isTophandler (App e1 e2) = isTophandler e1 || isTophandler e2
-isTophandler (Cast e _) = isTophandler e
-isTophandler (Tick _ e) = isTophandler e
-isTophandler e = showSDocUnsafe (ppr e) == "GHC.TopHandler.runMainIO"
-
diff --git a/src/Rattus/Plugin/Utils.hs b/src/Rattus/Plugin/Utils.hs
--- a/src/Rattus/Plugin/Utils.hs
+++ b/src/Rattus/Plugin/Utils.hs
@@ -1,6 +1,8 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE DeriveFunctor #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE CPP #-}
+
 module Rattus.Plugin.Utils (
   printMessage,
   Severity(..),
@@ -11,17 +13,29 @@
   isStrict,
   isTemporal,
   userFunction,
-  isType)
+  isType,
+  mkSysLocalFromVar,
+  mkSysLocalFromExpr,
+  fromRealSrcSpan,
+  noLocationInfo)
   where
 
+#if __GLASGOW_HASKELL__ >= 900
+import GHC.Plugins
+import GHC.Utils.Error
+import GHC.Utils.Monad
+#else
+import GhcPlugins
 import ErrUtils
+import MonadUtils
+#endif
+
 import Prelude hiding ((<>))
-import GhcPlugins
+
 import Data.Set (Set)
 import qualified Data.Set as Set
 import Data.Char
 import Data.Maybe
-import MonadUtils
 
 isType Type {} = True
 isType (App e _) = isType e
@@ -29,16 +43,23 @@
 isType (Tick _ e) = isType e
 isType _ = False
 
+
+
 printMessage :: (HasDynFlags m, MonadIO m) =>
                 Severity -> SrcSpan -> MsgDoc -> m ()
 printMessage sev loc doc = do
+#if __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
+              SevError   -> defaultErrStyle dflags
+              SevWarning -> defaultErrStyle dflags
+              SevDump    -> defaultDumpStyle dflags
+              _          -> defaultUserStyle dflags
   liftIO $ putLogMsg dflags NoReason sev loc sty doc
+#endif
 
 
 
@@ -214,3 +235,42 @@
       | isUpper c || c == '$' || c == ':' -> False
       | otherwise -> 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 One (exprType e)
+#else
+mkSysLocalFromExpr lit e = mkSysLocalM lit (exprType e)
+#endif
+
+
+fromRealSrcSpan :: RealSrcSpan -> SrcSpan
+#if __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
diff --git a/src/Rattus/Stream.hs b/src/Rattus/Stream.hs
--- a/src/Rattus/Stream.hs
+++ b/src/Rattus/Stream.hs
@@ -30,7 +30,7 @@
 import Data.VectorSpace
 
 -- | @Str a@ is a stream of values of type @a@.
-data Str a = ! a ::: !(O (Str a))
+data Str a = !a ::: !(O (Str a))
 
 -- all functions in this module are in Rattus 
 {-# ANN module Rattus #-}
diff --git a/src/Rattus/Strict.hs b/src/Rattus/Strict.hs
--- a/src/Rattus/Strict.hs
+++ b/src/Rattus/Strict.hs
@@ -84,7 +84,7 @@
 
 
 -- | Strict variant of 'Maybe'.
-data Maybe' a = Just' ! a | Nothing'
+data Maybe' a = Just' !a | Nothing'
 
 -- | takes a default value, a function, and a 'Maybe'' value.  If the
 -- 'Maybe'' value is 'Nothing'', the function returns the default
diff --git a/src/Rattus/Yampa.hs b/src/Rattus/Yampa.hs
--- a/src/Rattus/Yampa.hs
+++ b/src/Rattus/Yampa.hs
@@ -46,7 +46,7 @@
 -- | Signal functions from inputs of type @a@ to outputs of type @b@.
 data SF a b = SF{
   -- | Run a signal function for one step.
-  stepSF :: ! (DTime -> a -> (O(SF a b) :* b))}
+  stepSF :: !(DTime -> a -> (O(SF a b) :* b))}
 
 -- | The identity signal function that does nothing.
 identity :: SF a a
diff --git a/test/IllTyped.hs b/test/IllTyped.hs
--- a/test/IllTyped.hs
+++ b/test/IllTyped.hs
@@ -7,98 +7,121 @@
 import Rattus.Stream as S
 import Rattus.Yampa
 import Prelude
+import Rattus.Plugin.Annotation (InternalAnn (..))
 
--- Uncomment the annotation below to check that the definitions in
--- this module don't type check
 
--- {-# ANN module Rattus #-}
+{-# ANN module Rattus #-}
 
 
 
+{-# ANN loopIndirect ExpectError #-}
 loopIndirect :: Str Int
 loopIndirect = run
   where run :: Str Int
         run = loopIndirect
 
-        
+{-# ANN loopIndirect' ExpectError #-}
 loopIndirect' :: Str Int
 loopIndirect' = let run = loopIndirect' in run
 
-
+{-# ANN nestedUnguard ExpectError #-}
 nestedUnguard :: Str Int
 nestedUnguard = run 0
   where run :: Int -> Str Int
         run 0 = nestedUnguard
         run n = n ::: delay (run (n-1))
 
+{-# ANN sfLeak ExpectError #-}
 sfLeak :: O Int -> SF () (O Int)
 sfLeak  x = proc _ -> do
   returnA -< x
-  
+
+{-# 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))
 
-dblAdv' :: O (O a) -> O (O a)
-dblAdv' y = delay (delay (adv (adv y)))
-
-lambdaUnderDelay :: O (O Int -> Int -> Int)
-lambdaUnderDelay = delay (\x _ -> adv x)
-
-sneakyLambdaUnderDelay :: O (Int -> Int)
-sneakyLambdaUnderDelay = delay (let f _ =  adv (delay 1) in f)
+{-# ANN advScope ExpectError #-}
+advScope :: O (O Int -> Int)
+advScope = delay (\x -> adv x)
 
-leaky :: (() -> Bool) -> Str Bool
-leaky p = p () ::: delay (leaky (\ _ -> hd (leaky (\ _ -> True))))
+{-# 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 :: Str Int -> Box (Str Int)
 boxStream s = box (0 ::: tl s)
 
+{-# ANN boxStream' ExpectError #-}
 boxStream' :: Str Int -> Box (Str 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 -> Str a
 constUnstable a = run
   where run = a ::: delay run
 
+{-# ANN mapUnboxed ExpectError #-}
 mapUnboxed :: (a -> b) -> Str a -> Str b
 mapUnboxed f = run
   where run (x ::: xs) = f x ::: delay (run (adv xs))
-  
+
+{-# ANN mapUnboxedMutual ExpectError #-}
 mapUnboxedMutual :: (a -> b) -> Str a -> Str b
 mapUnboxedMutual f = run
   where run (x ::: xs) = f x ::: delay (run' (adv xs))
         run' (x ::: xs) = f x ::: delay (run (adv xs))
 
+-- mutual recursive pattern definitions are not supported
+-- foo1,foo2 :: Box (a -> b) -> Str a -> Str 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) -> Str a -> Str b
+nestedPattern = foo1 where
+  foo1,foo2 :: Box (a -> b) -> Str a -> Str b
+  (foo1,foo2) = (\ f (x ::: xs) -> unbox f x ::: (delay (foo2 f) <#> xs),
+                 \ f (x ::: xs) -> unbox f x ::: (delay (foo1 f) <#> 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 -> Str Input
diff --git a/test/MemoryLeak.hs b/test/MemoryLeak.hs
--- a/test/MemoryLeak.hs
+++ b/test/MemoryLeak.hs
@@ -25,7 +25,7 @@
 -- If we Haskell's (lazy) pair types, we get a memory leak:
 
 type Lazy a = ((),a)
-
+{-# ANN leakyLazy AllowLazyData #-}
 leakyLazy :: Str (Lazy Int) -> Str (Lazy Int)
 leakyLazy ((_,x):::xs) = ((),1) ::: delay (leakyLazy  (fmap ((+) x) (hd (adv xs)) ::: (tl (adv xs))))
 
diff --git a/test/NewlyTyped.hs b/test/NewlyTyped.hs
--- a/test/NewlyTyped.hs
+++ b/test/NewlyTyped.hs
@@ -6,13 +6,14 @@
 import Rattus
 import Rattus.Stream as S
 import Prelude
+import Rattus.Plugin.Annotation (InternalAnn (..))
 
 -- All of these examples should typecheck with the more relaxed typing
 -- rules of Rattus that allows functions and delays under tick.
 
 {-# ANN module Rattus #-}
 
-
+{-# ANN recBox ExpectWarning #-}
 recBox :: Str Int
 recBox = 0 ::: unbox (box (delay recBox))
 
@@ -21,32 +22,48 @@
 dblDelay = delay (delay 1)
 
 
+dblAdv :: O (O a) -> O (O a)
+dblAdv y = delay (delay (adv (adv y)))
+
+
 lambdaUnderDelay :: O (Int -> Int)
 lambdaUnderDelay = delay (\x -> x)
 
-advUnderLambda :: O (O Int -> O Int)
-advUnderLambda = delay (\x -> delay (adv x))
+delayAdvUnderLambda :: O (O Int -> O Int)
+delayAdvUnderLambda = delay (\x -> delay (adv x))
 
+sneakyLambdaUnderDelay' :: O (a -> Bool)
+sneakyLambdaUnderDelay' = delay (let f _ =  adv (delay True) in f)
+
+advUnderLambda :: O Int -> O (a -> Int)
+advUnderLambda y = delay (\x -> adv y)
+
 sneakyLambdaUnderDelay :: O (Int -> Int)
 sneakyLambdaUnderDelay = delay (let f x = x in f)
 
+-- This function is leaky unless the single tick transformation is
+-- performed
+leaky :: (() -> Bool) -> Str Bool
+leaky p = p () ::: delay (leaky (\ _ -> hd (leaky (\ _ -> True))))
+
+{-# ANN zeros ExpectWarning #-}
 zeros :: Box (Str Int)
 zeros = box (0 ::: delay (unbox zeros))
 
 oneTwo :: Str Int
 oneTwo = 1 ::: delay (2 ::: delay oneTwo)
 
-data FStr a = Cons ! a ! (O (a -> O (FStr a)))
+data FStr a = Cons !a !(O (a -> O (FStr a)))
 
 recFun :: Int -> FStr Int 
 recFun n = Cons n (delay (\ x -> delay (recFun x)))
 
+{-# ANN nestedRec ExpectWarning #-}
 nestedRec :: Str Int
 nestedRec = run 10
   where run :: Int -> Str Int
         run 0 = 0 ::: delay (nestedRec)
         run n = n ::: delay (run (n-1))
-
 
 {-# ANN main NotRattus #-}
 main = putStrLn "This file should type check"
diff --git a/test/TimeLeak.hs b/test/TimeLeak.hs
--- a/test/TimeLeak.hs
+++ b/test/TimeLeak.hs
@@ -5,6 +5,7 @@
 import Rattus
 import Rattus.Stream as Str
 import Rattus.ToHaskell
+import Rattus.Plugin.Annotation (InternalAnn (..))
 
 {-# ANN module Rattus #-}
 
@@ -19,15 +20,14 @@
     where from :: Int -> Str Int
           from n = n ::: delay (from (n+1))
 
--- This function should cause a warning.
+  -- This function should cause a warning.
+{-# ANN leakyNats ExpectWarning #-}
 leakyNats :: Str Int
 leakyNats = 0 ::: delay (Str.map (box (+1)) leakyNats)
 
 inc :: Str Int -> Str Int
 inc = Str.map (box ((+)1))
 
--- This function should cause a warning.
-
 leakyNats' :: Str Int
 leakyNats' = 0 ::: delay (inc leakyNats')
 
@@ -37,21 +37,22 @@
 altMap f g (x ::: xs) = unbox f x ::: delay (altMap g f (adv xs))
 
 -- This function should cause a warning.
+{-# ANN leakyAlt ExpectWarning #-}
 leakyAlt :: Str Int
 leakyAlt = 0 ::: delay (altMap (box ((+)1)) (box ((+)2)) leakyAlt)
 
-
--- This function should cause a warning.
 mapMap :: Box (a -> a) -> Box (a -> a) -> Str a -> Str a
 mapMap f g (x ::: xs) = unbox f x ::: delay (Str.map g (mapMap g f (adv xs)))
 
 -- This function should cause a warning.
+{-# ANN leakyMap ExpectWarning #-}
 leakyMap :: Str Int
 leakyMap = 0 ::: delay (mapMap (box ((+)1)) (box ((+)2)) leakyMap)
 
 
 
 -- This function should cause a warning.
+{-# ANN boxLeaky ExpectWarning #-}
 boxLeaky :: Str Int
 boxLeaky = run (box (\() -> 1)) 1
   where run :: Box (() -> Int) -> Int -> Str Int
@@ -59,16 +60,19 @@
                   ::: delay (run (box (\ () -> (unbox f () + 1))) a)
 
 -- This function should cause a warning.
+{-# ANN boxLeaky' ExpectWarning #-}
 boxLeaky' :: Str Int -> Str Int
 boxLeaky' = run (box (\() -> 1)) 1
   where run :: Box (() -> Int) -> Int -> Str Int -> Str Int
         run f a (x ::: xs) = (if a == 0 then unbox f () else a) ::: delay (run (box (\ () -> (unbox f () + x))) a (adv xs))
 
 -- This function should cause a warning.
+{-# ANN natsTrans ExpectWarning #-}
 natsTrans :: Str Int -> Str Int
 natsTrans (x ::: xs) = x ::: delay (Str.map (box ((+)x)) $ natsTrans $ adv xs)
 
 -- This function should cause a warning.
+{-# ANN leakySum ExpectWarning #-}
 leakySum :: Box (Int -> Int) -> Str Int -> Str Int
 leakySum f (x ::: xs) = unbox f x ::: (delay (leakySum (box (\ y -> unbox f (y + x)))) <#> xs)
 
diff --git a/test/WellTyped.hs b/test/WellTyped.hs
--- a/test/WellTyped.hs
+++ b/test/WellTyped.hs
@@ -81,18 +81,16 @@
 bar2 f  (x ::: xs) = unbox f x ::: (delay (bar1 f) <#> xs)
 
 
--- mutual recursive definition
-foo1,foo2 :: Box (a -> b) -> Str a -> Str b
-(foo1,foo2) = (\ f (x ::: xs) -> unbox f x ::: (delay (foo2 f) <#> xs),
-               \ f (x ::: xs) -> unbox f x ::: (delay (foo1 f) <#> xs))
-
-
 applyDelay :: O (O (a -> b)) -> O (O a) -> O (O b)
 applyDelay f x = delay (adv f <#> adv x)
 
 
 stableDelay :: Stable a => a -> O a
 stableDelay x = delay x
+
+patternBinding :: Str Int -> Str Int
+patternBinding str = (x + 1) ::: (delay patternBinding <#> xs)
+  where (x ::: xs) = sumBox str
 
 
 data Input a = Input {jump :: !a, move :: !Move}