diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,10 @@
 # Changelog for the [`clash-lib`](http://hackage.haskell.org/package/clash-lib) package
 
+## 0.5.11 *September 7th 2015*
+* Fixes bugs:
+  * Clash running out of memory on Simple-ish project [#70](https://github.com/clash-lang/clash-compiler/issues/70)
+  * `CLaSH.Sized.Vector.:>` was not allowed as a function argument to HO-primitives
+
 ## 0.5.10 *August 2nd 2015*
 * Fixes bugs:
   * Make testbench generation deterministic
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,2 +1,29 @@
-# `clash-lib`
+# `clash-lib` - CλaSH compiler, as a library
+
   * See the LICENSE file for license and copyright details
+
+# CλaSH - A functional hardware description language
+CλaSH (pronounced ‘clash’) is a functional hardware description language that
+borrows both its syntax and semantics from the functional programming language
+Haskell. The CλaSH compiler transforms these high-level descriptions to
+low-level synthesizable VHDL, Verilog, or SystemVerilog.
+
+Features of CλaSH:
+
+  * Strongly typed (like VHDL), yet with a very high degree of type inference,
+    which enables both safe and fast prototying using consise descriptions (like
+    Verilog)
+
+  * Interactive REPL: load your designs in an interpreter and easily test all
+    your component without needing to setup a test bench.
+
+  * Higher-order functions, with type inference, result in designs that are
+    fully parametric by default.
+
+  * Synchronous sequential circuit design based on streams of values, called
+    `Signal`s.
+
+  * Support for multiple clock domains, with type safe clock domain crossing.
+
+# Support
+For updates and questions join the mailing list clash-language+subscribe@googlegroups.com or read the [forum](https://groups.google.com/d/forum/clash-language)
diff --git a/clash-lib.cabal b/clash-lib.cabal
--- a/clash-lib.cabal
+++ b/clash-lib.cabal
@@ -1,14 +1,30 @@
 Name:                 clash-lib
-Version:              0.5.10
+Version:              0.5.11
 Synopsis:             CAES Language for Synchronous Hardware - As a Library
 Description:
   CλaSH (pronounced ‘clash’) is a functional hardware description language that
   borrows both its syntax and semantics from the functional programming language
-  Haskell. The merits of using a functional language to describe hardware comes
-  from the fact that combinational circuits can be directly modelled as
-  mathematical functions and that functional languages lend themselves very well
-  at describing and (de-)composing mathematical functions.
+  Haskell. The CλaSH compiler transforms these high-level descriptions to
+  low-level synthesizable VHDL, Verilog, or SystemVerilog.
   .
+  Features of CλaSH:
+  .
+  * Strongly typed (like VHDL), yet with a very high degree of type inference,
+    which enables both safe and fast prototying using consise descriptions (like
+    Verilog)
+  .
+  * Interactive REPL: load your designs in an interpreter and easily test all
+    your component without needing to setup a test bench.
+  .
+  * Higher-order functions, with type inference, result in designs that are
+    fully parametric by default.
+  .
+  * Synchronous sequential circuit design based on streams of values, called
+    @Signal@s.
+  .
+  * Support for multiple clock domains, with type safe clock domain crossing.
+  .
+  .
   This package provides:
   .
   * The CoreHW internal language: SystemF + Letrec + Case-decomposition
@@ -21,11 +37,11 @@
   .
   Front-ends (for: parsing, typecheck, etc.) are provided by separate packages:
   .
-  * <https://github.com/christiaanb/Idris-dev Idris Frontend>
-  .
   * <http://hackage.haskell.org/package/clash-ghc GHC/Haskell Frontend>
   .
+  * <https://github.com/christiaanb/Idris-dev Idris Frontend>
   .
+  .
   Prelude library: <http://hackage.haskell.org/package/clash-prelude>
 Homepage:             http://www.clash-lang.org/
 bug-reports:          http://github.com/clash-lang/clash-compiler/issues
@@ -52,6 +68,22 @@
   default-language:   Haskell2010
   ghc-options:        -Wall
   CPP-Options:        -DCABAL
+
+  other-extensions:   CPP
+                      DeriveAnyClass
+                      DeriveGeneric
+                      FlexibleContexts
+                      FlexibleInstances
+                      GeneralizedNewtypeDeriving
+                      LambdaCase
+                      MultiParamTypeClasses
+                      OverloadedStrings
+                      Rank2Types
+                      RecordWildCards
+                      ScopedTypeVariables
+                      TemplateHaskell
+                      TupleSections
+                      ViewPatterns
 
   Build-depends:      aeson                   >= 0.6.2.0,
                       attoparsec              >= 0.10.4.0,
diff --git a/src/CLaSH/Core/DataCon.hs b/src/CLaSH/Core/DataCon.hs
--- a/src/CLaSH/Core/DataCon.hs
+++ b/src/CLaSH/Core/DataCon.hs
@@ -24,9 +24,9 @@
 -- | Data Constructor
 data DataCon
   = MkData
-  { dcName       :: DcName   -- ^ Name of the DataCon
-  , dcTag        :: ConTag   -- ^ Syntactical position in the type definition
-  , dcType       :: Type     -- ^ Type of the 'DataCon
+  { dcName       :: !DcName  -- ^ Name of the DataCon
+  , dcTag        :: !ConTag  -- ^ Syntactical position in the type definition
+  , dcType       :: !Type    -- ^ Type of the 'DataCon
   , dcUnivTyVars :: [TyName] -- ^ Universally quantified type-variables,
                              -- these type variables are also part of the
                              -- result type of the DataCon
diff --git a/src/CLaSH/Core/Literal.hs b/src/CLaSH/Core/Literal.hs
--- a/src/CLaSH/Core/Literal.hs
+++ b/src/CLaSH/Core/Literal.hs
@@ -20,9 +20,9 @@
 
 -- | Term Literal
 data Literal
-  = IntegerLiteral  Integer
-  | StringLiteral   String
-  | RationalLiteral Rational
+  = IntegerLiteral  !Integer
+  | StringLiteral   !String
+  | RationalLiteral !Rational
   deriving (Eq,Ord,Show,Generic,NFData)
 
 instance Alpha Literal where
diff --git a/src/CLaSH/Core/Pretty.hs b/src/CLaSH/Core/Pretty.hs
--- a/src/CLaSH/Core/Pretty.hs
+++ b/src/CLaSH/Core/Pretty.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE PatternGuards     #-}
 {-# LANGUAGE TemplateHaskell   #-}
 {-# LANGUAGE ViewPatterns      #-}
 -- | Pretty printing class and instances for CoreHW
diff --git a/src/CLaSH/Core/Term.hs b/src/CLaSH/Core/Term.hs
--- a/src/CLaSH/Core/Term.hs
+++ b/src/CLaSH/Core/Term.hs
@@ -30,17 +30,17 @@
 
 -- | Term representation in the CoreHW language: System F + LetRec + Case
 data Term
-  = Var     Type TmName                    -- ^ Variable reference
-  | Data    DataCon                        -- ^ Datatype constructor
-  | Literal Literal                        -- ^ Literal
-  | Prim    Text Type                      -- ^ Primitive
-  | Lam     (Bind Id Term)                 -- ^ Term-abstraction
-  | TyLam   (Bind TyVar Term)              -- ^ Type-abstraction
-  | App     Term Term                      -- ^ Application
-  | TyApp   Term Type                      -- ^ Type-application
-  | Letrec  (Bind (Rec [LetBinding]) Term) -- ^ Recursive let-binding
-  | Case    Term Type [Bind Pat Term]      -- ^ Case-expression: subject, type of
-                                           -- alternatives, list of alternatives
+  = Var     !Type !TmName                   -- ^ Variable reference
+  | Data    !DataCon                        -- ^ Datatype constructor
+  | Literal !Literal                        -- ^ Literal
+  | Prim    !Text !Type                     -- ^ Primitive
+  | Lam     !(Bind Id Term)                 -- ^ Term-abstraction
+  | TyLam   !(Bind TyVar Term)              -- ^ Type-abstraction
+  | App     !Term !Term                     -- ^ Application
+  | TyApp   !Term !Type                     -- ^ Type-application
+  | Letrec  !(Bind (Rec [LetBinding]) Term) -- ^ Recursive let-binding
+  | Case    !Term !Type [Bind Pat Term]     -- ^ Case-expression: subject, type of
+                                            -- alternatives, list of alternatives
   deriving (Show,Generic,NFData)
 
 -- | Term reference
@@ -50,10 +50,10 @@
 
 -- | Patterns in the LHS of a case-decomposition
 data Pat
-  = DataPat (Embed DataCon) (Rebind [TyVar] [Id])
+  = DataPat !(Embed DataCon) !(Rebind [TyVar] [Id])
   -- ^ Datatype pattern, '[TyVar]' bind existentially-quantified
   -- type-variables of a DataCon
-  | LitPat  (Embed Literal)
+  | LitPat  !(Embed Literal)
   -- ^ Literal pattern
   | DefaultPat
   -- ^ Default pattern
diff --git a/src/CLaSH/Core/TyCon.hs b/src/CLaSH/Core/TyCon.hs
--- a/src/CLaSH/Core/TyCon.hs
+++ b/src/CLaSH/Core/TyCon.hs
@@ -30,27 +30,27 @@
 data TyCon
   -- | Algorithmic DataCons
   = AlgTyCon
-  { tyConName   :: TyConName   -- ^ Name of the TyCon
-  , tyConKind   :: Kind        -- ^ Kind of the TyCon
-  , tyConArity  :: Int         -- ^ Number of type arguments
-  , algTcRhs    :: AlgTyConRhs -- ^ DataCon definitions
+  { tyConName   :: !TyConName   -- ^ Name of the TyCon
+  , tyConKind   :: !Kind        -- ^ Kind of the TyCon
+  , tyConArity  :: !Int         -- ^ Number of type arguments
+  , algTcRhs    :: !AlgTyConRhs -- ^ DataCon definitions
   }
   -- | Function TyCons (e.g. type families)
   | FunTyCon
-  { tyConName   :: TyConName       -- ^ Name of the TyCon
-  , tyConKind   :: Kind            -- ^ Kind of the TyCon
-  , tyConArity  :: Int             -- ^ Number of type arguments
+  { tyConName   :: !TyConName      -- ^ Name of the TyCon
+  , tyConKind   :: !Kind           -- ^ Kind of the TyCon
+  , tyConArity  :: !Int            -- ^ Number of type arguments
   , tyConSubst  :: [([Type],Type)] -- ^ List of: ([LHS match types], RHS type)
   }
   -- | Primitive TyCons
   | PrimTyCon
-  { tyConName    :: TyConName  -- ^ Name of the TyCon
-  , tyConKind    :: Kind       -- ^ Kind of the TyCon
-  , tyConArity   :: Int        -- ^ Number of type arguments
+  { tyConName    :: !TyConName  -- ^ Name of the TyCon
+  , tyConKind    :: !Kind       -- ^ Kind of the TyCon
+  , tyConArity   :: !Int        -- ^ Number of type arguments
   }
   -- | To close the loop on the type hierarchy
   | SuperKindTyCon
-  { tyConName :: TyConName     -- ^ Name of the TyCon
+  { tyConName :: !TyConName     -- ^ Name of the TyCon
   }
   deriving (Generic,NFData)
 
@@ -75,7 +75,7 @@
   { dataCons :: [DataCon]        -- ^ The DataCons of a TyCon
   }
   | NewTyCon
-  { dataCon   :: DataCon         -- ^ The newtype DataCon
+  { dataCon   :: !DataCon        -- ^ The newtype DataCon
   , ntEtadRhs :: ([TyName],Type) -- ^ The argument type of the newtype
                                  -- DataCon in eta-reduced form, which is
                                  -- just the representation of the TyCon.
diff --git a/src/CLaSH/Core/Type.hs b/src/CLaSH/Core/Type.hs
--- a/src/CLaSH/Core/Type.hs
+++ b/src/CLaSH/Core/Type.hs
@@ -65,30 +65,30 @@
 
 -- | Types in CoreHW: function and polymorphic types
 data Type
-  = VarTy    Kind TyName       -- ^ Type variable
-  | ConstTy  ConstTy           -- ^ Type constant
-  | ForAllTy (Bind TyVar Type) -- ^ Polymorphic Type
-  | AppTy    Type Type         -- ^ Type Application
-  | LitTy    LitTy             -- ^ Type literal
+  = VarTy    !Kind !TyName      -- ^ Type variable
+  | ConstTy  !ConstTy           -- ^ Type constant
+  | ForAllTy !(Bind TyVar Type) -- ^ Polymorphic Type
+  | AppTy    !Type !Type        -- ^ Type Application
+  | LitTy    !LitTy             -- ^ Type literal
   deriving (Show,Generic,NFData)
 
 -- | An easier view on types
 data TypeView
-  = FunTy    Type  Type       -- ^ Function type
-  | TyConApp TyConName [Type] -- ^ Applied TyCon
-  | OtherType Type            -- ^ Neither of the above
+  = FunTy    !Type  !Type      -- ^ Function type
+  | TyConApp !TyConName [Type] -- ^ Applied TyCon
+  | OtherType !Type            -- ^ Neither of the above
   deriving Show
 
 -- | Type Constants
 data ConstTy
-  = TyCon TyConName -- ^ TyCon type
-  | Arrow           -- ^ Function type
+  = TyCon !TyConName -- ^ TyCon type
+  | Arrow            -- ^ Function type
   deriving (Show,Generic,NFData,Alpha)
 
 -- | Literal Types
 data LitTy
-  = NumTy Int
-  | SymTy String
+  = NumTy !Int
+  | SymTy !String
   deriving (Show,Generic,NFData,Alpha)
 
 -- | The level above types
diff --git a/src/CLaSH/Core/Type.hs-boot b/src/CLaSH/Core/Type.hs-boot
--- a/src/CLaSH/Core/Type.hs-boot
+++ b/src/CLaSH/Core/Type.hs-boot
@@ -1,4 +1,3 @@
-{-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 
 {-# OPTIONS_GHC -fno-warn-missing-methods #-}
diff --git a/src/CLaSH/Core/Var.hs b/src/CLaSH/Core/Var.hs
--- a/src/CLaSH/Core/Var.hs
+++ b/src/CLaSH/Core/Var.hs
@@ -1,12 +1,6 @@
-{-# LANGUAGE CPP                   #-}
 {-# LANGUAGE DeriveAnyClass        #-}
 {-# LANGUAGE DeriveGeneric         #-}
-{-# LANGUAGE FlexibleContexts      #-}
-{-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE ScopedTypeVariables   #-}
-{-# LANGUAGE TemplateHaskell       #-}
-{-# LANGUAGE UndecidableInstances  #-}
 
 -- | Variables in CoreHW
 module CLaSH.Core.Var
diff --git a/src/CLaSH/Netlist.hs b/src/CLaSH/Netlist.hs
--- a/src/CLaSH/Netlist.hs
+++ b/src/CLaSH/Netlist.hs
@@ -6,8 +6,8 @@
 
 import           Control.Lens                     ((.=), (<<%=))
 import qualified Control.Lens                     as Lens
-import           Control.Monad.State              (runStateT)
-import           Control.Monad.Writer             (listen, runWriterT, tell)
+import           Control.Monad.State.Strict       (runStateT)
+import           Control.Monad.Writer.Strict      (listen, runWriterT, tell)
 import           Data.Either                      (lefts,partitionEithers)
 import           Data.HashMap.Lazy                (HashMap)
 import qualified Data.HashMap.Lazy                as HashMap
diff --git a/src/CLaSH/Netlist/BlackBox.hs b/src/CLaSH/Netlist/BlackBox.hs
--- a/src/CLaSH/Netlist/BlackBox.hs
+++ b/src/CLaSH/Netlist/BlackBox.hs
@@ -224,6 +224,11 @@
                       dcApp  = DataCon resHTy (DC (resHTy,0)) dcInps
                       dcAss  = Assignment (pack "~RESULT") dcApp
                   return (Right dcAss)
+                Just resHTy@(Vector _ _) -> do
+                  let dcInps = [ Identifier (pack ("~ARG[" ++ show x ++ "]")) Nothing | x <- [(0::Int)..1] ]
+                      dcApp  = DataCon resHTy (DC (resHTy,1)) dcInps
+                      dcAss  = Assignment (pack "~RESULT") dcApp
+                  return (Right dcAss)
                 _ -> error $ $(curLoc) ++ "Cannot make function input for: " ++ showDoc e
             Var _ fun -> do
               normalized <- Lens.use bindings
diff --git a/src/CLaSH/Netlist/BlackBox/Types.hs b/src/CLaSH/Netlist/BlackBox/Types.hs
--- a/src/CLaSH/Netlist/BlackBox/Types.hs
+++ b/src/CLaSH/Netlist/BlackBox/Types.hs
@@ -7,27 +7,27 @@
 type BlackBoxTemplate = [Element]
 
 -- | Elements of a blackbox context
-data Element = C   Text          -- ^ Constant
-             | D   Decl          -- ^ Component instantiation hole
+data Element = C   !Text         -- ^ Constant
+             | D   !Decl         -- ^ Component instantiation hole
              | O                 -- ^ Output hole
-             | I   Int           -- ^ Input hole
-             | L   Int           -- ^ Literal hole
-             | Sym Int           -- ^ Symbol hole
-             | Clk (Maybe Int)   -- ^ Clock hole (Maybe clk corresponding to
+             | I   !Int          -- ^ Input hole
+             | L   !Int          -- ^ Literal hole
+             | Sym !Int          -- ^ Symbol hole
+             | Clk !(Maybe Int)  -- ^ Clock hole (Maybe clk corresponding to
                                  -- input, clk corresponding to output if Nothing)
-             | Rst (Maybe Int)   -- ^ Reset hole
-             | Typ (Maybe Int)   -- ^ Type declaration hole
-             | TypM (Maybe Int)  -- ^ Type root hole
-             | Err (Maybe Int)   -- ^ Error value hole
-             | TypElem Element   -- ^ Select element type from a vector type
+             | Rst !(Maybe Int)  -- ^ Reset hole
+             | Typ !(Maybe Int)  -- ^ Type declaration hole
+             | TypM !(Maybe Int) -- ^ Type root hole
+             | Err !(Maybe Int)  -- ^ Error value hole
+             | TypElem !Element  -- ^ Select element type from a vector type
              | CompName          -- ^ Hole for the name of the component in which
                                  -- the blackbox is instantiated
-             | Size Element      -- ^ Size of a type hole
-             | Length Element    -- ^ Length of a vector hole
-             | FilePath Element  -- ^ Hole containing a filepath for a data file
-             | Gen Bool          -- ^ Hole marking beginning (True) or end (False)
+             | Size !Element     -- ^ Size of a type hole
+             | Length !Element   -- ^ Length of a vector hole
+             | FilePath !Element -- ^ Hole containing a filepath for a data file
+             | Gen !Bool         -- ^ Hole marking beginning (True) or end (False)
                                  -- of a generative construct
-             | SigD [Element] (Maybe Int)
+             | SigD [Element] !(Maybe Int)
   deriving Show
 
 -- | Component instantiation hole. First argument indicates which function argument
@@ -37,5 +37,5 @@
 --
 -- The LHS of the tuple is the name of the signal, while the RHS of the tuple
 -- is the type of the signal
-data Decl = Decl Int [(BlackBoxTemplate,BlackBoxTemplate)]
+data Decl = Decl !Int [(BlackBoxTemplate,BlackBoxTemplate)]
   deriving Show
diff --git a/src/CLaSH/Netlist/BlackBox/Util.hs b/src/CLaSH/Netlist/BlackBox/Util.hs
--- a/src/CLaSH/Netlist/BlackBox/Util.hs
+++ b/src/CLaSH/Netlist/BlackBox/Util.hs
@@ -10,7 +10,7 @@
 import           Control.Lens                         (at, use, (%=), (+=), _1,
                                                        _2)
 import           Control.Monad.State                  (State, runState)
-import           Control.Monad.Writer                 (MonadWriter, tell)
+import           Control.Monad.Writer.Strict          (MonadWriter, tell)
 import           Data.Foldable                        (foldrM)
 import qualified Data.IntMap                          as IntMap
 import           Data.List                            (mapAccumL)
diff --git a/src/CLaSH/Netlist/Types.hs b/src/CLaSH/Netlist/Types.hs
--- a/src/CLaSH/Netlist/Types.hs
+++ b/src/CLaSH/Netlist/Types.hs
@@ -6,8 +6,8 @@
 module CLaSH.Netlist.Types where
 
 import Control.DeepSeq
-import Control.Monad.State                  (MonadIO, MonadState, StateT)
-import Control.Monad.Writer                 (MonadWriter, WriterT)
+import Control.Monad.State.Strict           (MonadIO, MonadState, StateT)
+import Control.Monad.Writer.Strict          (MonadWriter, WriterT)
 import Data.Hashable
 import Data.HashMap.Lazy                    (HashMap)
 import Data.IntMap.Lazy                     (IntMap, empty)
@@ -41,14 +41,14 @@
   = NetlistState
   { _bindings       :: HashMap TmName (Type,Term) -- ^ Global binders
   , _varEnv         :: Gamma -- ^ Type environment/context
-  , _varCount       :: Int -- ^ Number of signal declarations
-  , _cmpCount       :: Int -- ^ Number of create components
+  , _varCount       :: !Int -- ^ Number of signal declarations
+  , _cmpCount       :: !Int -- ^ Number of create components
   , _components     :: HashMap TmName Component -- ^ Cached components
   , _primitives     :: PrimMap -- ^ Primitive Definitions
   , _typeTranslator :: HashMap TyConName TyCon -> Type -> Maybe (Either String HWType) -- ^ Hardcoded Type -> HWType translator
   , _tcCache        :: HashMap TyConName TyCon -- ^ TyCon cache
-  , _modNm          :: String -- ^ Name of the module containing the @topEntity@
-  , _curCompNm      :: Identifier
+  , _modNm          :: !String -- ^ Name of the module containing the @topEntity@
+  , _curCompNm      :: !Identifier
   , _dataFiles      :: [(String,FilePath)]
   }
 
@@ -58,7 +58,7 @@
 -- | Component: base unit of a Netlist
 data Component
   = Component
-  { componentName :: Identifier -- ^ Name of the component
+  { componentName :: !Identifier -- ^ Name of the component
   , hiddenPorts   :: [(Identifier,HWType)] -- ^ Ports that have no correspondence the original function definition
   , inputs        :: [(Identifier,HWType)] -- ^ Input ports
   , outputs       :: [(Identifier,HWType)] -- ^ Output ports
@@ -79,16 +79,16 @@
   = Void -- ^ Empty type
   | Bool -- ^ Boolean type
   | Integer -- ^ Integer type
-  | BitVector Size -- ^ BitVector of a specified size
-  | Index    Size -- ^ Unsigned integer with specified (exclusive) upper bounder
-  | Signed   Size -- ^ Signed integer of a specified size
-  | Unsigned Size -- ^ Unsigned integer of a specified size
-  | Vector   Size       HWType -- ^ Vector type
-  | Sum      Identifier [Identifier] -- ^ Sum type: Name and Constructor names
-  | Product  Identifier [HWType] -- ^ Product type: Name and field types
-  | SP       Identifier [(Identifier,[HWType])] -- ^ Sum-of-Product type: Name and Constructor names + field types
-  | Clock    Identifier Int -- ^ Clock type with specified name and period
-  | Reset    Identifier Int -- ^ Reset type corresponding to clock with a specified name and period
+  | BitVector !Size -- ^ BitVector of a specified size
+  | Index    !Size -- ^ Unsigned integer with specified (exclusive) upper bounder
+  | Signed   !Size -- ^ Signed integer of a specified size
+  | Unsigned !Size -- ^ Unsigned integer of a specified size
+  | Vector   !Size       !HWType -- ^ Vector type
+  | Sum      !Identifier [Identifier] -- ^ Sum type: Name and Constructor names
+  | Product  !Identifier [HWType] -- ^ Product type: Name and field types
+  | SP       !Identifier [(Identifier,[HWType])] -- ^ Sum-of-Product type: Name and Constructor names + field types
+  | Clock    !Identifier !Int -- ^ Clock type with specified name and period
+  | Reset    !Identifier !Int -- ^ Reset type corresponding to clock with a specified name and period
   deriving (Eq,Ord,Show,Generic)
 
 instance Hashable HWType
@@ -96,13 +96,13 @@
 
 -- | Internals of a Component
 data Declaration
-  = Assignment Identifier Expr
+  = Assignment !Identifier !Expr
   -- ^ Signal assignment:
   --
   -- * Signal to assign
   --
   -- * Assigned expression
-  | CondAssignment Identifier HWType Expr [(Maybe Expr,Expr)]
+  | CondAssignment !Identifier !HWType !Expr [(Maybe Expr,Expr)]
   -- ^ Conditional signal assignment:
   --
   -- * Signal to assign
@@ -112,9 +112,9 @@
   -- * Scrutinized expression
   --
   -- * List of: (Maybe expression scrutinized expression is compared with,RHS of alternative)
-  | InstDecl Identifier Identifier [(Identifier,Expr)] -- ^ Instantiation of another component
-  | BlackBoxD S.Text BlackBoxTemplate BlackBoxContext -- ^ Instantiation of blackbox declaration
-  | NetDecl Identifier HWType -- ^ Signal declaration
+  | InstDecl !Identifier !Identifier [(Identifier,Expr)] -- ^ Instantiation of another component
+  | BlackBoxD !S.Text !BlackBoxTemplate BlackBoxContext -- ^ Instantiation of blackbox declaration
+  | NetDecl !Identifier !HWType -- ^ Signal declaration
   deriving Show
 
 instance NFData Declaration where
@@ -129,20 +129,20 @@
 
 -- | Expression used in RHS of a declaration
 data Expr
-  = Literal    (Maybe (HWType,Size)) Literal -- ^ Literal expression
-  | DataCon    HWType       Modifier  [Expr] -- ^ DataCon application
-  | Identifier Identifier   (Maybe Modifier) -- ^ Signal reference
-  | DataTag    HWType       (Either Identifier Identifier) -- ^ @Left e@: tagToEnum#, @Right e@: dataToTag#
-  | BlackBoxE S.Text BlackBoxTemplate BlackBoxContext Bool -- ^ Instantiation of a BlackBox expression
+  = Literal    !(Maybe (HWType,Size)) !Literal -- ^ Literal expression
+  | DataCon    !HWType       !Modifier  [Expr] -- ^ DataCon application
+  | Identifier !Identifier   !(Maybe Modifier) -- ^ Signal reference
+  | DataTag    !HWType       !(Either Identifier Identifier) -- ^ @Left e@: tagToEnum#, @Right e@: dataToTag#
+  | BlackBoxE !S.Text !BlackBoxTemplate !BlackBoxContext !Bool -- ^ Instantiation of a BlackBox expression
   deriving Show
 
 -- | Literals used in an expression
 data Literal
-  = NumLit    Integer   -- ^ Number literal
-  | BitLit    Bit       -- ^ Bit literal
-  | BoolLit   Bool      -- ^ Boolean literal
+  = NumLit    !Integer   -- ^ Number literal
+  | BitLit    !Bit       -- ^ Bit literal
+  | BoolLit   !Bool      -- ^ Boolean literal
   | VecLit    [Literal] -- ^ Vector literal
-  | StringLit String    -- ^ String literal
+  | StringLit !String    -- ^ String literal
   deriving Show
 
 -- | Bit literal
diff --git a/src/CLaSH/Normalize.hs b/src/CLaSH/Normalize.hs
--- a/src/CLaSH/Normalize.hs
+++ b/src/CLaSH/Normalize.hs
@@ -6,7 +6,6 @@
 import           Control.Concurrent.Supply        (Supply)
 import           Control.Lens                     ((.=))
 import qualified Control.Lens                     as Lens
-import qualified Control.Monad.State              as State
 import           Data.Either                      (partitionEithers)
 import           Data.HashMap.Strict              (HashMap)
 import qualified Data.HashMap.Strict              as HashMap
@@ -34,9 +33,10 @@
 import           CLaSH.Normalize.Types
 import           CLaSH.Normalize.Util
 import           CLaSH.Rewrite.Combinators        ((>->),(!->),repeatR,topdownR)
-import           CLaSH.Rewrite.Types              (DebugLevel (..), RewriteState (..),
-                                                   bindings, dbgLevel, tcCache)
-import           CLaSH.Rewrite.Util               (liftRS, runRewrite,
+import           CLaSH.Rewrite.Types              (DebugLevel (..), RewriteEnv (..), RewriteState (..),
+                                                   bindings, curFun, dbgLevel,
+                                                   tcCache, extra)
+import           CLaSH.Rewrite.Util               (runRewrite,
                                                    runRewriteSession)
 import           CLaSH.Util
 
@@ -57,10 +57,22 @@
                  -- ^ NormalizeSession to run
                  -> a
 runNormalization opts supply globals typeTrans tcm eval
-  = flip State.evalState normState
-  . runRewriteSession (opt_dbgLevel opts) rwState
+  = runRewriteSession rwEnv rwState
   where
-    rwState   = RewriteState 0 globals supply typeTrans tcm eval
+    rwEnv     = RewriteEnv
+                  (opt_dbgLevel opts)
+                  typeTrans
+                  tcm
+                  eval
+
+    rwState   = RewriteState
+                  0
+                  globals
+                  supply
+                  (error $ $(curLoc) ++ "Report as bug: no curFun")
+                  0
+                  normState
+
     normState = NormalizeState
                   HashMap.empty
                   Map.empty
@@ -69,7 +81,6 @@
                   HashMap.empty
                   (opt_inlineLimit opts)
                   (opt_inlineBelow opts)
-                  (error $ $(curLoc) ++ "Report as bug: no curFun")
 
 
 normalize :: [TmName]
@@ -87,17 +98,17 @@
   let nmS = showDoc nm
   case exprM of
     Just (_,tm) -> do
-      tmNorm <- makeCachedT3S nm normalized $ do
-                  liftRS $ curFun .= nm
+      tmNorm <- makeCached nm (extra.normalized) $ do
+                  curFun .= nm
                   tm' <- rewriteExpr ("normalization",normalization) (nmS,tm)
-                  tcm <- Lens.use tcCache
+                  tcm <- Lens.view tcCache
                   ty' <- termType tcm tm'
                   return (ty',tm')
       let usedBndrs = Lens.toListOf termFreeIds (snd tmNorm)
       traceIf (nm `elem` usedBndrs)
               ($(curLoc) ++ "Expr belonging to bndr: " ++ nmS ++ " (:: " ++ showDoc (fst tmNorm) ++ ") remains recursive after normalization:\n" ++ showDoc (snd tmNorm))
               (return ())
-      prevNorm <- fmap HashMap.keys $ liftRS $ Lens.use normalized
+      prevNorm <- fmap HashMap.keys $ Lens.use (extra.normalized)
       let toNormalize = filter (`notElem` (nm:prevNorm)) usedBndrs
       return (toNormalize,(nm,tmNorm))
     Nothing -> error $ $(curLoc) ++ "Expr belonging to bndr: " ++ nmS ++ " not found"
@@ -179,7 +190,7 @@
 flattenNode :: CallTree
             -> NormalizeSession (Either CallTree ((TmName,Term),[CallTree]))
 flattenNode c@(CLeaf (nm,(_,e))) = do
-  tcm  <- Lens.use tcCache
+  tcm  <- Lens.view tcCache
   norm <- splitNormalized tcm e
   case norm of
     Right (ids,[(_,bExpr)],_) -> do
@@ -189,7 +200,7 @@
         Nothing        -> return (Left c)
     _ -> return (Left c)
 flattenNode b@(CBranch (nm,(_,e)) us) = do
-  tcm  <- Lens.use tcCache
+  tcm  <- Lens.view tcCache
   norm <- splitNormalized tcm e
   case norm of
     Right (ids,[(_,bExpr)],_) -> do
diff --git a/src/CLaSH/Normalize/Strategy.hs b/src/CLaSH/Normalize/Strategy.hs
--- a/src/CLaSH/Normalize/Strategy.hs
+++ b/src/CLaSH/Normalize/Strategy.hs
@@ -9,7 +9,8 @@
 
 -- | Normalisation transformation
 normalization :: NormRewrite
-normalization = etaTL >-> constantPropgation >-> anf >-> rmDeadcode >-> bindConst >-> letTL >-> evalConst >-> cse >-> recLetRec
+normalization = etaTL >-> constantPropgation >-!-> anf >-!-> rmDeadcode >->
+                bindConst >-> letTL >-> evalConst >-!-> cse >-!-> recLetRec
   where
     etaTL      = apply "etaTL" etaExpansionTL
     anf        = topdownR (apply "nonRepANF" nonRepANF) >-> apply "ANF" makeANF
@@ -23,11 +24,9 @@
 constantPropgation :: NormRewrite
 constantPropgation = propagate >-> repeatR inlineAndPropagate >-> lifting >-> spec
   where
-    inlineAndPropagate = inlining >-> propagate
-    propagateAndInline = propagate >-> inlining
     propagate = innerMost (applyMany transInner)
-    inlining  = topdownR (applyMany transBUP !-> propagateAndInline)
-    lifting   = bottomupR (apply "liftNonRep" liftNonRep)
+    inlineAndPropagate = bottomupR (applyMany transBUP) !-> propagate
+    lifting   = bottomupR (apply "liftNonRep" liftNonRep) -- See: [Note] bottom-up traversal for liftNonRep
     spec      = bottomupR (applyMany specRws)
 
     transInner :: [(String,NormRewrite)]
@@ -42,7 +41,7 @@
     transBUP = [ ("inlineClosed", inlineClosed)
                , ("inlineSmall" , inlineSmall)
                , ("inlineNonRep", inlineNonRep)
-               , ("bindNonRep"  , bindNonRep)
+               , ("bindNonRep"  , bindNonRep) -- See: [Note] bindNonRep before liftNonRep
                ]
 
     specRws :: [(String,NormRewrite)]
@@ -51,12 +50,143 @@
               , ("nonRepSpec"  , nonRepSpec)
               ]
 
+{- [Note] bottom-up traversal for liftNonRep
+We used to say:
+
+"The liftNonRep transformation must be applied in a topDown traversal because
+of what CLaSH considers tail calls in its join-point analysis."
+
+Consider:
+
+> let fail = \x -> ...
+> in  case ... of
+>       A -> let fail1 = \y -> case ... of
+>                                 X -> fail ...
+>                                 Y -> ...
+>            in case ... of
+>                 P -> fail1 ...
+>                 Q -> ...
+>       B -> fail ...
+
+under "normal" tail call rules, the local 'fail' functions is not a join-point
+because it is used in a let-binding. However, we apply "special" tail call rules
+in CLaSH. Because 'fail' is used in a TC position within 'fail1', and 'fail1' is
+only used in a TC position, in CLaSH, we consider 'tail' also only to be used
+in a TC position.
+
+Now image we apply 'liftNonRep' in a bottom up traversal, we will end up with:
+
+> fail1 = \fail y -> case ... of
+>   X -> fail ...
+>   Y -> ...
+
+> let fail = \x -> ...
+> in  case ... of
+>       A -> case ... of
+>                 P -> fail1 fail ...
+>                 Q -> ...
+>       B -> fail ...
+
+Suddenly, 'fail' ends up in an argument position, because it occurred as a
+_locally_ bound variable within 'fail1'. And because of that 'fail' stops being
+a join-point.
+
+However, when we apply 'liftNonRep' in a top down traversal we end up with:
+
+> fail = \x -> ...
+>
+> fail1 = \y -> case ... of
+>   X -> fail ...
+>   Y -> ...
+>
+> let ...
+> in  case ... of
+>       A -> let
+>            in case ... of
+>                 P -> fail1 ...
+>                 Q -> ...
+>       B -> fail ...
+
+and all is well with the world.
+
+UPDATE:
+We can now just perform liftNonRep in a bottom-up traversal again, because
+liftNonRep no longer checks that if the binding that is lifted is a join-point.
+However, for this to work, bindNonRep must always have been exhaustively applied
+before liftNonRep. See also: [Note] bindNonRep before liftNonRep.
+-}
+
+{- [Note] bindNonRep before liftNonRep
+The combination of liftNonRep and nonRepSpec can lead to non-termination in an
+unchecked rewrite system (without termination measures in place) on the
+following:
+
+> main = f not
+> f    = \a x -> (a x) && (f a x)
+
+nonRepSpec will lead to:
+
+> main = f'
+> f    = \a x -> (a x) && (f a x)
+> f'   = (\a x -> (a x) && (f a x)) not
+
+then lamApp leads to:
+
+> main = f'
+> f    = \a x -> (a x) && (f a x)
+> f'   = let a = not in (\x -> (a x) && (f a x))
+
+then liftNonRep leads to:
+
+> main = f'
+> f    = \a x -> (a x) && (f a x)
+> f'   = \x -> (g x) && (f g x)
+> g    = not
+
+and nonRepSepc leads to:
+
+> main = f'
+> f    = \a x -> (a x) && (f a x)
+> f'   = \x -> (g x) && (f'' g x)
+> g    = not
+> f''  = (\a x -> (a x) && (f a x)) g
+
+This cycle continues indefinitely, as liftNonRep creates a new global variable,
+which is never alpha-equivalent to the previous global variable introduced by
+liftNonRep.
+
+That is why bindNonRep must always be applied before liftNonRep. When we end up
+in the situation after lamApp:
+
+> main = f'
+> f    = \a x -> (a x) && (f a x)
+> f'   = let a = not in (\x -> (a x) && (f a x))
+
+bindNonRep will now lead to:
+
+> main = f'
+> f    = \a x -> (a x) && (f a x)
+> f'   = \x -> (not x) && (f not x)
+
+Because f has already been specialised on the alpha-equivalent-to-itself not
+function, liftNonRep leads to:
+
+> main = f'
+> f    = \a x -> (a x) && (f a x)
+> f'   = \x -> (not x) && (f' x)
+
+And there is no non-terminating rewriting cycle.
+
+That is why bindNonRep must always be exhaustively applied before we apply
+liftNonRep.
+-}
+
 -- | Topdown traversal, stops upon first success
-topdownSucR :: (Functor m, Monad m) => Rewrite m -> Rewrite m
+topdownSucR :: Rewrite extra -> Rewrite extra
 topdownSucR r = r >-! (allR True (topdownSucR r))
 
-innerMost :: (Functor m, Monad m) => Rewrite m -> Rewrite m
+innerMost :: Rewrite extra -> Rewrite extra
 innerMost r = bottomupR (r !-> innerMost r)
 
-applyMany :: (Functor m, Monad m) => [(String,Rewrite m)] -> Rewrite m
+applyMany :: [(String,Rewrite extra)] -> Rewrite extra
 applyMany = foldr1 (>->) . map (uncurry apply)
diff --git a/src/CLaSH/Normalize/Transformations.hs b/src/CLaSH/Normalize/Transformations.hs
--- a/src/CLaSH/Normalize/Transformations.hs
+++ b/src/CLaSH/Normalize/Transformations.hs
@@ -1,6 +1,5 @@
-{-# LANGUAGE TemplateHaskell #-}
-{-# LANGUAGE TypeFamilies    #-}
-{-# LANGUAGE ViewPatterns    #-}
+{-# LANGUAGE TemplateHaskell  #-}
+{-# LANGUAGE ViewPatterns     #-}
 
 -- | Transformations of the Normalization process
 module CLaSH.Normalize.Transformations
@@ -65,25 +64,33 @@
 import           CLaSH.Rewrite.Util
 import           CLaSH.Util
 
--- | Inline non-recursive, non-representable let-bindings
+-- | Inline non-recursive, non-representable, non-join-point, let-bindings
 bindNonRep :: NormRewrite
 bindNonRep = inlineBinders nonRepTest
   where
-    nonRepTest (Id idName tyE, exprE)
-      = (&&) <$> (not <$> (representableType <$> Lens.use typeTranslator <*> Lens.use tcCache <*> pure (unembed tyE)))
-             <*> (notElem idName <$> (Lens.toListOf <$> localFreeIds <*> pure (unembed exprE)))
+    nonRepTest :: Term -> (Var Term, Embed Term) -> RewriteMonad extra Bool
+    nonRepTest e (id_@(Id idName tyE), exprE)
+      = (&&) <$> (not <$> (representableType <$> Lens.view typeTranslator <*> Lens.view tcCache <*> pure (unembed tyE)))
+             <*> ((&&) <$> (notElem idName <$> (Lens.toListOf <$> localFreeIds <*> pure (unembed exprE)))
+                       <*> (pure (not $ isJoinPointIn id_ e)))
 
-    nonRepTest _ = return False
+    nonRepTest _ _ = return False
 
 -- | Lift non-representable let-bindings
 liftNonRep :: NormRewrite
 liftNonRep = liftBinders nonRepTest
   where
-    nonRepTest (Id idName tyE, exprE)
-      = (&&) <$> (not <$> (representableType <$> Lens.use typeTranslator <*> Lens.use tcCache <*> pure (unembed tyE)))
-             <*> (elem idName <$> (Lens.toListOf <$> localFreeIds <*> pure (unembed exprE)))
+    nonRepTest :: Term -> (Var Term, Embed Term) -> RewriteMonad extra Bool
+    nonRepTest _ ((Id _ tyE), _)
+      -- We used to also check whether the binder we are lifting is either
+      -- recursive or a join-point. This is no longer needed because we apply
+      -- bindNonRep exhaustively before we apply liftNonRep. See also:
+      -- [Note] bindNonRep before liftNonRep
+      = not <$> (representableType <$> Lens.view typeTranslator
+                                   <*> Lens.view tcCache
+                                   <*> pure (unembed tyE))
 
-    nonRepTest _ = return False
+    nonRepTest _ _ = return False
 
 -- | Specialize functions on their type
 typeSpec :: NormRewrite
@@ -101,29 +108,29 @@
   | (Var _ _, args) <- collectArgs e1
   , (_, [])     <- Either.partitionEithers args
   , null $ Lens.toListOf termFreeTyVars e2
-  = R $ do tcm <- Lens.use tcCache
-           e2Ty <- termType tcm e2
-           localVar <- isLocalVar e2
-           nonRepE2 <- not <$> (representableType <$> Lens.use typeTranslator <*> Lens.use tcCache <*> pure e2Ty)
-           if nonRepE2 && not localVar
-             then runR $ specializeNorm True ctx e
-             else return e
+  = do tcm <- Lens.view tcCache
+       e2Ty <- termType tcm e2
+       localVar <- isLocalVar e2
+       nonRepE2 <- not <$> (representableType <$> Lens.view typeTranslator <*> Lens.view tcCache <*> pure e2Ty)
+       if nonRepE2 && not localVar
+         then specializeNorm True ctx e
+         else return e
 
 nonRepSpec _ e = return e
 
 -- | Lift the let-bindings out of the subject of a Case-decomposition
 caseLet :: NormRewrite
-caseLet _ (Case (Letrec b) ty alts) = R $ do
+caseLet _ (Case (Letrec b) ty alts) = do
   (xes,e) <- unbind b
-  changed . Letrec $ bind xes (Case e ty alts)
+  changed (Letrec (bind xes (Case e ty alts)))
 
 caseLet _ e = return e
 
 -- | Move a Case-decomposition from the subject of a Case-decomposition to the alternatives
 caseCase :: NormRewrite
 caseCase _ e@(Case (Case scrut alts1Ty alts1) alts2Ty alts2)
-  = R $ do
-    ty1Rep  <- representableType <$> Lens.use typeTranslator <*> Lens.use tcCache <*> pure alts1Ty
+  = do
+    ty1Rep  <- representableType <$> Lens.view typeTranslator <*> Lens.view tcCache <*> pure alts1Ty
     if not ty1Rep
       then do newAlts <- mapM ( return
                                   . uncurry bind
@@ -140,15 +147,15 @@
 inlineNonRep :: NormRewrite
 inlineNonRep _ e@(Case scrut altsTy alts)
   | (Var _ f, args) <- collectArgs scrut
-  = R $ do
-    isInlined <- liftR $ alreadyInlined f
-    limit     <- liftR $ Lens.use inlineLimit
-    tcm       <- Lens.use tcCache
+  = do
+    cf        <- Lens.use curFun
+    isInlined <- zoomExtra (alreadyInlined f cf)
+    limit     <- Lens.use (extra.inlineLimit)
+    tcm       <- Lens.view tcCache
     scrutTy   <- termType tcm scrut
     let noException = not (exception tcm scrutTy)
     if noException && (Maybe.fromMaybe 0 isInlined) > limit
       then do
-        cf <- liftR $ Lens.use curFun
         ty <- termType tcm scrut
         traceIf True (concat [$(curLoc) ++ "InlineNonRep: " ++ show f
                              ," already inlined " ++ show limit ++ " times in:"
@@ -163,10 +170,10 @@
                      (return e)
       else do
         bodyMaybe   <- fmap (HashMap.lookup f) $ Lens.use bindings
-        nonRepScrut <- not <$> (representableType <$> Lens.use typeTranslator <*> Lens.use tcCache <*> pure scrutTy)
+        nonRepScrut <- not <$> (representableType <$> Lens.view typeTranslator <*> Lens.view tcCache <*> pure scrutTy)
         case (nonRepScrut, bodyMaybe) of
           (True,Just (_, scrutBody)) -> do
-            Monad.when noException (liftR $ addNewInline f)
+            Monad.when noException (zoomExtra (addNewInline f cf))
             changed $ Case (mkApps scrutBody args) altsTy alts
           _ -> return e
   where
@@ -181,7 +188,7 @@
 caseCon :: NormRewrite
 caseCon _ c@(Case scrut _ alts)
   | (Data dc, args) <- collectArgs scrut
-  = R $ do
+  = do
     alts' <- mapM unbind alts
     let dcAltM = List.find (equalCon dc . fst) alts'
     case dcAltM of
@@ -202,7 +209,7 @@
     equalCon dc (DataPat dc' _) = dcTag dc == dcTag (unembed dc')
     equalCon _  _               = False
 
-caseCon _ c@(Case (Literal l) _ alts) = R $ do
+caseCon _ c@(Case (Literal l) _ alts) = do
   alts' <- mapM unbind alts
   let ltAltsM = List.find (equalLit . fst) alts'
   case ltAltsM of
@@ -216,9 +223,9 @@
 
 caseCon ctx e@(Case subj ty alts)
   | isConstant subj = do
-    tcm <- Lens.use tcCache
+    tcm <- Lens.view tcCache
     lvl <- Lens.view dbgLevel
-    reduceConstant <- Lens.use evaluator
+    reduceConstant <- Lens.view evaluator
     case reduceConstant tcm subj of
       Literal l -> caseCon ctx (Case (Literal l) ty alts)
       subj'@(collectArgs -> (Data _,_)) -> caseCon ctx (Case subj' ty alts)
@@ -226,8 +233,8 @@
 
 caseCon _ e = caseOneAlt e
 
-caseOneAlt :: Monad m => Term -> R m Term
-caseOneAlt e@(Case _ _ [alt]) = R $ do
+caseOneAlt :: Term -> RewriteMonad extra Term
+caseOneAlt e@(Case _ _ [alt]) = do
   (pat,altE) <- unbind alt
   case pat of
     DefaultPat    -> changed altE
@@ -249,13 +256,13 @@
 nonRepANF ctx e@(App appConPrim arg)
   | (conPrim, _) <- collectArgs e
   , isCon conPrim || isPrim conPrim
-  = R $ do
+  = do
     untranslatable <- isUntranslatable arg
     case (untranslatable,arg) of
       (True,Letrec b) -> do (binds,body) <- unbind b
-                            changed . Letrec $ bind binds (App appConPrim body)
-      (True,Case {})  -> runR $ specializeNorm True ctx e
-      (True,Lam _)    -> runR $ specializeNorm True ctx e
+                            changed (Letrec (bind binds (App appConPrim body)))
+      (True,Case {})  -> specializeNorm True ctx e
+      (True,Lam _)    -> specializeNorm True ctx e
       _               -> return e
 
 nonRepANF _ e = return e
@@ -265,23 +272,23 @@
 topLet :: NormRewrite
 topLet ctx e
   | all isLambdaBodyCtx ctx && not (isLet e)
-  = R $ do
+  = do
   untranslatable <- isUntranslatable e
   if untranslatable
     then return e
-    else do tcm <- Lens.use tcCache
+    else do tcm <- Lens.view tcCache
             (argId,argVar) <- mkTmBinderFor tcm "topLet" e
             changed . Letrec $ bind (rec [(argId,embed e)]) argVar
 
 topLet ctx e@(Letrec b)
   | all isLambdaBodyCtx ctx
-  = R $ do
+  = do
     (binds,body)   <- unbind b
     localVar       <- isLocalVar body
     untranslatable <- isUntranslatable body
     if localVar || untranslatable
       then return e
-      else do tcm <- Lens.use tcCache
+      else do tcm <- Lens.view tcCache
               (argId,argVar) <- mkTmBinderFor tcm "topLet" body
               changed . Letrec $ bind (rec $ unrec binds ++ [(argId,embed body)]) argVar
 
@@ -291,7 +298,7 @@
 
 -- | Remove unused let-bindings
 deadCode :: NormRewrite
-deadCode _ e@(Letrec binds) = R $ do
+deadCode _ e@(Letrec binds) = do
     (xes, body) <- fmap (first unrec) $ unbind binds
     let bodyFVs = Lens.toListOf termFreeIds body
         (xesUsed,xesOther) = List.partition
@@ -304,6 +311,8 @@
       then changed . Letrec $ bind (rec xesUsed') body
       else return e
   where
+    findUsedBndrs :: [(Var Term, Embed Term)] -> [(Var Term, Embed Term)]
+                  -> [(Var Term, Embed Term)] -> [(Var Term, Embed Term)]
     findUsedBndrs used []      _     = used
     findUsedBndrs used explore other =
       let fvsUsed = concatMap (Lens.toListOf termFreeIds . unembed . snd) explore
@@ -321,13 +330,13 @@
 bindConstantVar :: NormRewrite
 bindConstantVar = inlineBinders test
   where
-    test (_,Embed e) = (||) <$> isLocalVar e <*> pure (isConstant e)
+    test _ (_,Embed e) = (||) <$> isLocalVar e <*> pure (isConstant e)
 
 -- | Inline nullary/closed functions
 inlineClosed :: NormRewrite
 inlineClosed _ e@(collectArgs -> (Var _ f,args))
   | all (either isConstant (const True)) args
-  = R $ do
+  = do
     untranslatable <- isUntranslatable e
     if untranslatable
       then return e
@@ -341,8 +350,8 @@
                               else return e
           _ -> return e
 
-inlineClosed _ e@(Var _ f) = R $ do
-  tcm <- Lens.use tcCache
+inlineClosed _ e@(Var _ f) = do
+  tcm <- Lens.view tcCache
   closed <- isClosed tcm e
   untranslatable <- isUntranslatable e
   if closed && not untranslatable
@@ -361,13 +370,13 @@
 
 -- | Inline small functions
 inlineSmall :: NormRewrite
-inlineSmall _ e@(collectArgs -> (Var _ f,args)) = R $ do
+inlineSmall _ e@(collectArgs -> (Var _ f,args)) = do
   untranslatable <- isUntranslatable e
   if untranslatable
     then return e
     else do
       bndrs <- Lens.use bindings
-      sizeLimit <- liftR $ Lens.use inlineBelow
+      sizeLimit <- Lens.use (extra.inlineBelow)
       case HashMap.lookup f bndrs of
         -- Don't inline recursive expressions
         Just (_,body) -> let cg = callGraph [] bndrs f
@@ -396,18 +405,18 @@
 -- | Propagate arguments of application inwards; except for 'Lam' where the
 -- argument becomes let-bound.
 appProp :: NormRewrite
-appProp _ (App (Lam b) arg) = R $ do
+appProp _ (App (Lam b) arg) = do
   (v,e) <- unbind b
   if isConstant arg || isVar arg
     then changed $ substTm (varName v) arg e
     else changed . Letrec $ bind (rec [(v,embed arg)]) e
 
-appProp _ (App (Letrec b) arg) = R $ do
+appProp _ (App (Letrec b) arg) = do
   (v,e) <- unbind b
   changed . Letrec $ bind v (App e arg)
 
-appProp _ (App (Case scrut ty alts) arg) = R $ do
-  tcm <- Lens.use tcCache
+appProp _ (App (Case scrut ty alts) arg) = do
+  tcm <- Lens.view tcCache
   argTy <- termType tcm arg
   let ty' = applyFunTy tcm ty argTy
   if isConstant arg || isVar arg
@@ -427,31 +436,27 @@
                     ) alts
       changed . Letrec $ bind (rec [(boundArg,embed arg)]) (Case scrut ty' alts')
 
-appProp _ (TyApp (TyLam b) t) = R $ do
+appProp _ (TyApp (TyLam b) t) = do
   (tv,e) <- unbind b
   changed $ substTyInTm (varName tv) t e
 
-appProp _ (TyApp (Letrec b) t) = R $ do
+appProp _ (TyApp (Letrec b) t) = do
   (v,e) <- unbind b
   changed . Letrec $ bind v (TyApp e t)
 
-appProp _ (TyApp (Case scrut altsTy alts) ty) = R $ do
+appProp _ (TyApp (Case scrut altsTy alts) ty) = do
   alts' <- mapM ( return
                 . uncurry bind
                 . second (`TyApp` ty)
                 <=< unbind
                 ) alts
-  tcm <- Lens.use tcCache
+  tcm <- Lens.view tcCache
   ty' <- applyTy tcm altsTy ty
   changed $ Case scrut ty' alts'
 
 appProp _ e = return e
 
-type NormRewriteW = Transform (WriterT [LetBinding] (R NormalizeMonad))
-
-liftNormR :: RewriteMonad NormalizeMonad a
-          -> WriterT [LetBinding] (R NormalizeMonad) a
-liftNormR = lift . R
+type NormRewriteW = Transform (WriterT [LetBinding] (RewriteMonad NormalizeState))
 
 -- NOTE [unsafeUnbind]: Use unsafeUnbind (which doesn't freshen pattern
 -- variables). Reason: previously collected expression still reference
@@ -469,8 +474,8 @@
 makeANF _ (TyLam b) = return (TyLam b)
 
 makeANF ctx e
-  = R $ do
-    (e',bndrs) <- runR $ runWriterT $ bottomupR collectANF ctx e
+  = do
+    (e',bndrs) <- runWriterT $ bottomupR collectANF ctx e
     case bndrs of
       [] -> return e
       _  -> changed . Letrec $ bind (rec bndrs) e'
@@ -480,11 +485,11 @@
   | (conVarPrim, _) <- collectArgs e
   , isCon conVarPrim || isPrim conVarPrim || isVar conVarPrim
   = do
-    untranslatable <- liftNormR $ isUntranslatable arg
-    localVar       <- liftNormR $ isLocalVar arg
+    untranslatable <- lift (isUntranslatable arg)
+    localVar       <- lift (isLocalVar arg)
     case (untranslatable,localVar || isConstant arg,arg) of
-      (False,False,_) -> do tcm <- Lens.use tcCache
-                            (argId,argVar) <- liftNormR $ mkTmBinderFor tcm "repANF" arg
+      (False,False,_) -> do tcm <- Lens.view tcCache
+                            (argId,argVar) <- lift (mkTmBinderFor tcm "repANF" arg)
                             tell [(argId,embed arg)]
                             return (App appf argVar)
       (True,False,Letrec b) -> do (binds,body) <- unbind b
@@ -496,13 +501,13 @@
   -- See NOTE [unsafeUnbind]
   let (binds,body) = unsafeUnbind b
   tell (unrec binds)
-  untranslatable <- liftNormR $ isUntranslatable body
-  localVar       <- liftNormR $ isLocalVar body
+  untranslatable <- lift (isUntranslatable body)
+  localVar       <- lift (isLocalVar body)
   if localVar || untranslatable
     then return body
     else do
-      tcm <- Lens.use tcCache
-      (argId,argVar) <- liftNormR $ mkTmBinderFor tcm "bodyVar" body
+      tcm <- Lens.view tcCache
+      (argId,argVar) <- lift (mkTmBinderFor tcm "bodyVar" body)
       tell [(argId,embed body)]
       return argVar
 
@@ -526,23 +531,23 @@
   | name2String (dcName $ unembed dc) == "CLaSH.Signal.Internal.:-" = return e
 
 collectANF ctx (Case subj ty alts) = do
-    localVar     <- liftNormR $ isLocalVar subj
+    localVar     <- lift (isLocalVar subj)
     (bndr,subj') <- if localVar || isConstant subj
       then return ([],subj)
-      else do tcm <- Lens.use tcCache
-              (argId,argVar) <- liftNormR $ mkTmBinderFor tcm "subjLet" subj
+      else do tcm <- Lens.view tcCache
+              (argId,argVar) <- lift (mkTmBinderFor tcm "subjLet" subj)
               return ([(argId,embed subj)],argVar)
 
-    (binds,alts') <- fmap (first concat . unzip) $ liftNormR $ mapM (doAlt subj') alts
+    (binds,alts') <- fmap (first concat . unzip) $ mapM (lift . doAlt subj') alts
 
     tell (bndr ++ binds)
     return (Case subj' ty alts')
   where
-    doAlt :: Term -> Bind Pat Term -> RewriteMonad NormalizeMonad ([LetBinding],Bind Pat Term)
+    doAlt :: Term -> Bind Pat Term -> RewriteMonad NormalizeState ([LetBinding],Bind Pat Term)
     -- See NOTE [unsafeUnbind]
     doAlt subj' = fmap (second (uncurry bind)) . doAlt' subj' . unsafeUnbind
 
-    doAlt' :: Term -> (Pat,Term) -> RewriteMonad NormalizeMonad ([LetBinding],(Pat,Term))
+    doAlt' :: Term -> (Pat,Term) -> RewriteMonad NormalizeState ([LetBinding],(Pat,Term))
     doAlt' subj' alt@(DataPat dc pxs@(unrebind -> ([],xs)),altExpr) = do
       lv      <- isLocalVar altExpr
       patSels <- Monad.zipWithM (doPatBndr subj' (unembed dc)) xs [0..]
@@ -550,7 +555,7 @@
           usesXs _         = False
       if (lv && not (usesXs altExpr)) || isConstant altExpr
         then return (patSels,alt)
-        else do tcm <- Lens.use tcCache
+        else do tcm <- Lens.view tcCache
                 (altId,altVar) <- mkTmBinderFor tcm "altLet" altExpr
                 return ((altId,embed altExpr):patSels,(DataPat dc pxs,altVar))
     doAlt' _ alt@(DataPat _ _, _) = return ([],alt)
@@ -558,13 +563,13 @@
       lv <- isLocalVar altExpr
       if lv || isConstant altExpr
         then return ([],alt)
-        else do tcm <- Lens.use tcCache
+        else do tcm <- Lens.view tcCache
                 (altId,altVar) <- mkTmBinderFor tcm "altLet" altExpr
                 return ([(altId,embed altExpr)],(pat,altVar))
 
-    doPatBndr :: Term -> DataCon -> Id -> Int -> RewriteMonad NormalizeMonad LetBinding
+    doPatBndr :: Term -> DataCon -> Id -> Int -> RewriteMonad NormalizeState LetBinding
     doPatBndr subj' dc pId i
-      = do tcm <- Lens.use tcCache
+      = do tcm <- Lens.view tcCache
            patExpr <- mkSelectorCase ($(curLoc) ++ "doPatBndr") tcm ctx subj' (dcTag dc) i
            return (pId,embed patExpr)
 
@@ -578,8 +583,8 @@
   return $ Lam (bind bndr e')
 
 etaExpansionTL ctx e
-  = R $ do
-    tcm <- Lens.use tcCache
+  = do
+    tcm <- Lens.view tcCache
     isF <- isFun tcm e
     if isF
       then do
@@ -590,7 +595,7 @@
                  <=< termType tcm
                  ) e
         (newIdB,newIdV) <- mkInternalVar "eta" argTy
-        e' <- runR $ etaExpansionTL (LamBody newIdB:ctx) (App e newIdV)
+        e' <- etaExpansionTL (LamBody newIdB:ctx) (App e newIdV)
         changed . Lam $ bind newIdB e'
       else return e
 
@@ -599,10 +604,10 @@
 -- means that all recursive calls are replaced by the same variable reference as
 -- found in the body of the top-level let-expression.
 recToLetRec :: NormRewrite
-recToLetRec [] e = R $ do
-  fn          <- liftR $ Lens.use curFun
+recToLetRec [] e = do
+  fn          <- Lens.use curFun
   bodyM       <- fmap (HashMap.lookup fn) $ Lens.use bindings
-  tcm         <- Lens.use tcCache
+  tcm         <- Lens.view tcCache
   normalizedE <- splitNormalized tcm e
   case (normalizedE,bodyM) of
     (Right (args,bndrs,res), Just (bodyTy,_)) -> do
@@ -623,23 +628,23 @@
 inlineHO :: NormRewrite
 inlineHO _ e@(App _ _)
   | (Var _ f, args) <- collectArgs e
-  = R $ do
-    tcm <- Lens.use tcCache
+  = do
+    tcm <- Lens.view tcCache
     hasPolyFunArgs <- or <$> mapM (either (isPolyFun tcm) (const (return False))) args
     if hasPolyFunArgs
-      then do isInlined <- liftR $ alreadyInlined f
-              limit     <- liftR $ Lens.use inlineLimit
+      then do cf        <- Lens.use curFun
+              isInlined <- zoomExtra (alreadyInlined f cf)
+              limit     <- Lens.use (extra.inlineLimit)
               if (Maybe.fromMaybe 0 isInlined) > limit
                 then do
-                  cf  <- liftR $ Lens.use curFun
                   lvl <- Lens.view dbgLevel
                   traceIf (lvl > DebugNone) ($(curLoc) ++ "InlineHO: " ++ show f ++ " already inlined " ++ show limit ++ " times in:" ++ show cf) (return e)
                 else do
                   bodyMaybe <- fmap (HashMap.lookup f) $ Lens.use bindings
                   case bodyMaybe of
                     Just (_, body) -> do
-                      liftR $ addNewInline f
-                      changed $ mkApps body args
+                      zoomExtra (addNewInline f cf)
+                      changed (mkApps body args)
                     _ -> return e
       else return e
 
@@ -647,7 +652,7 @@
 
 -- | Simplified CSE, only works on let-bindings, works from top to bottom
 simpleCSE :: NormRewrite
-simpleCSE _ e@(Letrec b) = R $ do
+simpleCSE _ e@(Letrec b) = do
   (binders,body) <- first unrec <$> unbind b
   let (reducedBindings,body') = reduceBindersFix binders body
   if length binders /= length reducedBindings
@@ -685,9 +690,9 @@
   | isConstant e
   , (conPrim, _) <- collectArgs e
   , isPrim conPrim
-  = R $ do
-    tcm <- Lens.use tcCache
-    reduceConstant <- Lens.use evaluator
+  = do
+    tcm <- Lens.view tcCache
+    reduceConstant <- Lens.view evaluator
     case reduceConstant tcm e of
       e'@(Data _)    -> changed e'
       e'@(Literal _) -> changed e'
diff --git a/src/CLaSH/Normalize/Types.hs b/src/CLaSH/Normalize/Types.hs
--- a/src/CLaSH/Normalize/Types.hs
+++ b/src/CLaSH/Normalize/Types.hs
@@ -2,13 +2,13 @@
 -- | Types used in Normalize modules
 module CLaSH.Normalize.Types where
 
-import Control.Monad.State (State)
+import Control.Monad.State.Strict (State)
 import Data.HashMap.Strict (HashMap)
 import Data.Map            (Map)
 
 import CLaSH.Core.Term     (Term, TmName)
 import CLaSH.Core.Type     (Type)
-import CLaSH.Rewrite.Types (Rewrite, RewriteSession)
+import CLaSH.Rewrite.Types (Rewrite, RewriteMonad)
 import CLaSH.Util
 
 -- | State of the 'NormalizeMonad'
@@ -24,7 +24,7 @@
   -- * Elem: (name of specialised function,type of specialised function)
   , _specialisationHistory :: HashMap TmName Int
   -- ^ Cache of how many times a function was specialized
-  , _specialisationLimit :: Int
+  , _specialisationLimit :: !Int
   -- ^ Number of time a function 'f' can be specialized
   , _inlineHistory   :: HashMap TmName (HashMap TmName Int)
   -- ^ Cache of function where inlining took place:
@@ -32,13 +32,11 @@
   -- * Key: function where inlining took place
   --
   -- * Elem: (functions which were inlined, number of times inlined)
-  , _inlineLimit     :: Int
+  , _inlineLimit     :: !Int
   -- ^ Number of times a function 'f' can be inlined in a function 'g'
-  , _inlineBelow     :: Int
+  , _inlineBelow     :: !Int
   -- ^ Size of a function below which it is always inlined if it is not
   -- recursive
-  , _curFun          :: TmName
-  -- ^ Function which is currently normalized
   }
 
 makeLenses ''NormalizeState
@@ -47,7 +45,7 @@
 type NormalizeMonad = State NormalizeState
 
 -- | RewriteSession with extra Normalisation information
-type NormalizeSession = RewriteSession NormalizeMonad
+type NormalizeSession = RewriteMonad NormalizeState
 
 -- | A 'Transform' action in the context of the 'RewriteMonad' and 'NormalizeMonad'
-type NormRewrite = Rewrite NormalizeMonad
+type NormRewrite = Rewrite NormalizeState
diff --git a/src/CLaSH/Normalize/Util.hs b/src/CLaSH/Normalize/Util.hs
--- a/src/CLaSH/Normalize/Util.hs
+++ b/src/CLaSH/Normalize/Util.hs
@@ -28,19 +28,19 @@
 import           CLaSH.Util              (curLoc)
 
 -- | Determine if a function is already inlined in the context of the 'NetlistMonad'
-alreadyInlined :: TmName
+alreadyInlined :: TmName -- ^ Function we want to inline
+               -> TmName -- ^ Function in which we want to perform the inlining
                -> NormalizeMonad (Maybe Int)
-alreadyInlined f = do
-  cf <- Lens.use curFun
+alreadyInlined f cf = do
   inlinedHM <- Lens.use inlineHistory
   case HashMap.lookup cf inlinedHM of
     Nothing       -> return Nothing
     Just inlined' -> return (HashMap.lookup f inlined')
 
-addNewInline :: TmName
+addNewInline :: TmName -- ^ Function we want to inline
+             -> TmName -- ^ Function in which we want to perform the inlining
              -> NormalizeMonad ()
-addNewInline f = do
-  cf <- Lens.use curFun
+addNewInline f cf =
   inlineHistory %= HashMap.insertWith
                      (\_ hm -> HashMap.insertWith (+) f 1 hm)
                      cf
diff --git a/src/CLaSH/Primitives/Types.hs b/src/CLaSH/Primitives/Types.hs
--- a/src/CLaSH/Primitives/Types.hs
+++ b/src/CLaSH/Primitives/Types.hs
@@ -18,13 +18,13 @@
 data Primitive
   -- | A primitive that has a template that can be filled out by the backend render
   = BlackBox
-  { name     :: S.Text -- ^ Name of the primitive
-  , template :: Either Text Text -- ^ Either a /declaration/ or an /expression/ template.
+  { name     :: !S.Text -- ^ Name of the primitive
+  , template :: !(Either Text Text) -- ^ Either a /declaration/ or an /expression/ template.
   }
   -- | A primitive that carries additional information
   | Primitive
-  { name     :: S.Text -- ^ Name of the primitive
-  , primType :: Text -- ^ Additional information
+  { name     :: !S.Text -- ^ Name of the primitive
+  , primType :: !Text -- ^ Additional information
   }
   deriving Show
 
diff --git a/src/CLaSH/Rewrite/Combinators.hs b/src/CLaSH/Rewrite/Combinators.hs
--- a/src/CLaSH/Rewrite/Combinators.hs
+++ b/src/CLaSH/Rewrite/Combinators.hs
@@ -3,11 +3,12 @@
 -- | Rewriting combinators and traversals
 module CLaSH.Rewrite.Combinators where
 
+import           Control.DeepSeq             (deepseq)
 import           Control.Monad               ((<=<), (>=>))
 import qualified Control.Monad.Writer        as Writer
 import qualified Data.Monoid                 as Monoid
-import           Unbound.Generics.LocallyNameless     (Embed, Fresh, bind, embed, rec,
-                                              unbind, unembed, unrec)
+import           Unbound.Generics.LocallyNameless (Embed, Fresh, bind, embed,
+                                                   rec, unbind, unembed, unrec)
 import           Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind)
 
 import           CLaSH.Core.Term             (Pat, Term (..))
@@ -73,6 +74,13 @@
 (>->) :: (Monad m) => Transform m -> Transform m -> Transform m
 (>->) r1 r2 c = r1 c >=> r2 c
 
+infixr 6 >-!->
+-- | Apply two transformations in succession, and perform a deepseq in between.
+(>-!->) :: (Monad m) => Transform m -> Transform m -> Transform m
+(>-!->) r1 r2 c e = do
+  e' <- r1 c e
+  deepseq e' (r2 c e')
+
 -- | Apply a transformation in a topdown traversal
 topdownR :: (Fresh m, Functor m, Monad m) => Transform m -> Transform m
 topdownR r = r >-> allR True (topdownR r)
@@ -93,24 +101,24 @@
 
 infixr 5 !->
 -- | Only apply the second transformation if the first one succeeds.
-(!->) :: Monad m => Rewrite m -> Rewrite m -> Rewrite m
-(!->) r1 r2 c expr = R $ do
-  (expr',changed) <- runR $ Writer.listen $ r1 c expr
+(!->) :: Rewrite m -> Rewrite m -> Rewrite m
+(!->) r1 r2 c expr = do
+  (expr',changed) <- Writer.listen $ r1 c expr
   if Monoid.getAny changed
-    then runR $ r2 c expr'
+    then r2 c expr'
     else return expr'
 
 infixr 5 >-!
 -- | Only apply the second transformation if the first one fails.
-(>-!) :: Monad m => Rewrite m -> Rewrite m -> Rewrite m
-(>-!) r1 r2 c expr = R $ do
-  (expr',changed) <- runR $ Writer.listen $ r1 c expr
+(>-!) :: Rewrite m -> Rewrite m -> Rewrite m
+(>-!) r1 r2 c expr = do
+  (expr',changed) <- Writer.listen $ r1 c expr
   if Monoid.getAny changed
     then return expr'
-    else runR $ r2 c expr'
+    else r2 c expr'
 
 -- | Keep applying a transformation until it fails.
-repeatR :: Monad m => Rewrite m -> Rewrite m
+repeatR :: Rewrite m -> Rewrite m
 repeatR r = r !-> repeatR r
 
 whenR :: Monad m
diff --git a/src/CLaSH/Rewrite/Types.hs b/src/CLaSH/Rewrite/Types.hs
--- a/src/CLaSH/Rewrite/Types.hs
+++ b/src/CLaSH/Rewrite/Types.hs
@@ -1,18 +1,21 @@
 {-# LANGUAGE FlexibleInstances          #-}
+{-# LANGUAGE MultiParamTypeClasses      #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE TemplateHaskell            #-}
 
 -- | Type and instance definitions for Rewrite modules
 module CLaSH.Rewrite.Types where
 
-import Control.Concurrent.Supply (Supply, freshId)
-import Control.Lens              (use, (.=))
-import Control.Monad.Reader      (MonadReader, ReaderT, lift)
-import Control.Monad.State       (MonadState, StateT)
-import Control.Monad.Writer      (MonadWriter, WriterT)
-import Data.HashMap.Strict       (HashMap)
-import Data.Monoid               (Any)
-import Unbound.Generics.LocallyNameless   (Fresh, FreshMT)
+import Control.Concurrent.Supply             (Supply, freshId)
+import Control.Lens                          (use, (.=), (<<%=))
+import Control.Monad.Reader                  (MonadReader (..))
+import Control.Monad
+import Control.Monad.State                   (MonadState (..))
+import Control.Monad.Writer                  (MonadWriter (..))
+import Data.HashMap.Strict                   (HashMap)
+import Data.Monoid                           (Any)
+import Unbound.Generics.LocallyNameless      (Fresh (..))
+import Unbound.Generics.LocallyNameless.Name (Name (..))
 
 import CLaSH.Core.Term           (Term, TmName)
 import CLaSH.Core.Type           (Type)
@@ -22,73 +25,116 @@
 import CLaSH.Util
 
 -- | Context in which a term appears
-data CoreContext = AppFun -- ^ Function position of an application
-                 | AppArg -- ^ Argument position of an application
-                 | TyAppC -- ^ Function position of a type application
-                 | LetBinding [Id] -- ^ RHS of a Let-binder with the sibling LHS'
-                 | LetBody    [Id] -- ^ Body of a Let-binding with the bound LHS'
-                 | LamBody    Id   -- ^ Body of a lambda-term with the abstracted variable
-                 | TyLamBody  TyVar -- ^ Body of a TyLambda-term with the abstracted type-variable
-                 | CaseAlt    [Id] -- ^ RHS of a case-alternative with the variables bound by the pattern on the LHS
-                 | CaseScrut -- ^ Subject of a case-decomposition
-                 deriving (Eq,Show)
+data CoreContext
+  = AppFun           -- ^ Function position of an application
+  | AppArg           -- ^ Argument position of an application
+  | TyAppC           -- ^ Function position of a type application
+  | LetBinding [Id]  -- ^ RHS of a Let-binder with the sibling LHS'
+  | LetBody    [Id]  -- ^ Body of a Let-binding with the bound LHS'
+  | LamBody    Id    -- ^ Body of a lambda-term with the abstracted variable
+  | TyLamBody  TyVar -- ^ Body of a TyLambda-term with the abstracted
+                     -- type-variable
+  | CaseAlt    [Id]  -- ^ RHS of a case-alternative with the variables bound by
+                     -- the pattern on the LHS
+  | CaseScrut        -- ^ Subject of a case-decomposition
+  deriving (Eq,Show)
 
 -- | State of a rewriting session
-data RewriteState
+data RewriteState extra
   = RewriteState
-  { _transformCounter :: Int -- ^ Number of applied transformations
-  , _bindings         :: HashMap TmName (Type,Term) -- ^ Global binders
-  , _uniqSupply       :: Supply -- ^ Supply of unique numbers
-  , _typeTranslator   :: HashMap TyConName TyCon -> Type -> Maybe (Either String HWType) -- ^ Hardcode Type -> HWType translator
-  , _tcCache          :: HashMap TyConName TyCon -- ^ TyCon cache
-  , _evaluator        :: HashMap TyConName TyCon -> Term -> Term -- ^ Hardcoded evaluator (delta-reduction)
+  { _transformCounter :: {-# UNPACK #-} !Int
+  -- ^ Number of applied transformations
+  , _bindings         :: !(HashMap TmName (Type,Term))
+  -- ^ Global binders
+  , _uniqSupply       :: !Supply
+  -- ^ Supply of unique numbers
+  , _curFun           :: TmName -- Initially set to undefined: no strictness annotation
+  -- ^ Function which is currently normalized
+  , _nameCounter      :: {-# UNPACK #-} !Int
+  -- ^ Used for 'Fresh'
+  , _extra            :: !extra
+  -- ^ Additional state
   }
 
 makeLenses ''RewriteState
 
 -- | Debug Message Verbosity
 data DebugLevel
-  = DebugNone -- ^ Don't show debug messages
-  | DebugFinal -- ^ Show completely normalized expressions
-  | DebugName -- ^ Names of applied transformations
+  = DebugNone    -- ^ Don't show debug messages
+  | DebugFinal   -- ^ Show completely normalized expressions
+  | DebugName    -- ^ Names of applied transformations
   | DebugApplied -- ^ Show sub-expressions after a successful rewrite
-  | DebugAll -- ^ Show all sub-expressions on which a rewrite is attempted
+  | DebugAll     -- ^ Show all sub-expressions on which a rewrite is attempted
   deriving (Eq,Ord,Read)
 
 -- | Read-only environment of a rewriting session
-newtype RewriteEnv = RE { _dbgLevel :: DebugLevel }
+data RewriteEnv
+  = RewriteEnv
+  { _dbgLevel       :: DebugLevel
+  -- ^ Lvl at which we print debugging messages
+  , _typeTranslator :: HashMap TyConName TyCon -> Type
+                    -> Maybe (Either String HWType)
+  -- ^ Hardcode Type -> HWType translator
+  , _tcCache        :: HashMap TyConName TyCon
+  -- ^ TyCon cache
+  , _evaluator      :: HashMap TyConName TyCon -> Term -> Term
+  -- ^ Hardcoded evaluator (delta-reduction)}
+  }
 
 makeLenses ''RewriteEnv
 
 -- | Monad that keeps track how many transformations have been applied and can
--- generate fresh variables and unique identifiers
-type RewriteSession m = ReaderT RewriteEnv (StateT RewriteState (FreshMT m))
-
--- | Monad that can do the same as 'RewriteSession' and in addition keeps track
+-- generate fresh variables and unique identifiers. In addition, it keeps track
 -- if a transformation/rewrite has been successfully applied.
-type RewriteMonad m = WriterT Any (RewriteSession m)
+newtype RewriteMonad extra a = R
+  { runR :: RewriteEnv -> RewriteState extra -> (a,RewriteState extra,Any) }
 
-instance Monad m => MonadUnique (RewriteMonad m) where
+instance Functor (RewriteMonad extra) where
+  fmap f m = R (\r s -> case runR m r s of (a,s',w) -> (f a,s',w))
+
+instance Applicative (RewriteMonad extra) where
+  pure  = return
+  (<*>) = ap
+
+instance Monad (RewriteMonad extra) where
+  return a = R (\_ s -> (a, s, mempty))
+  m >>= k  = R (\r s -> case runR m r s of
+                          (a,s',w) -> case runR (k a) r s' of
+                                        (b,s'',w') -> let w'' = mappend w w'
+                                                      in seq w'' (b,s'',w''))
+
+instance MonadState (RewriteState extra) (RewriteMonad extra) where
+  get     = R (\_ s -> (s,s,mempty))
+  put s   = R (\_ _ -> ((),s,mempty))
+  state f = R (\_ s -> case f s of (a,s') -> (a,s',mempty))
+
+instance Fresh (RewriteMonad extra) where
+  fresh (Fn s _) = do
+    n <- nameCounter <<%= (+1)
+    let n' = toInteger n
+    n' `seq` return (Fn s n')
+  fresh nm@(Bn {}) = return nm
+
+instance MonadUnique (RewriteMonad extra) where
   getUniqueM = do
-    sup <- lift . lift $ use uniqSupply
+    sup <- use uniqSupply
     let (a,sup') = freshId sup
-    lift . lift $ uniqSupply .= sup'
-    return a
+    uniqSupply .= sup'
+    a `seq` return a
 
--- | MTL convenience wrapper around 'RewriteMonad'
-newtype R m a = R { runR :: RewriteMonad m a }
-  deriving ( Functor
-           , Applicative
-           , Monad
-           , MonadReader RewriteEnv
-           , MonadState  RewriteState
-           , MonadWriter Any
-           , MonadUnique
-           , Fresh
-           )
+instance MonadWriter Any (RewriteMonad extra) where
+  writer (a,w) = R (\_ s -> (a,s,w))
+  tell   w     = R (\_ s -> ((),s,w))
+  listen m     = R (\r s -> case runR m r s of (a,s',w) -> ((a,w),s',w))
+  pass   m     = R (\r s -> case runR m r s of ((a,f),s',w) -> (a, s', f w))
 
+instance MonadReader RewriteEnv (RewriteMonad extra) where
+   ask       = R (\r s -> (r,s,mempty))
+   local f m = R (\r s -> runR m (f r) s)
+   reader f  = R (\r s -> (f r,s,mempty))
+
 -- | Monadic action that transforms a term given a certain context
 type Transform m = [CoreContext] -> Term -> m Term
 
 -- | A 'Transform' action in the context of the 'RewriteMonad'
-type Rewrite m   = Transform (R m)
+type Rewrite extra = Transform (RewriteMonad extra)
diff --git a/src/CLaSH/Rewrite/Util.hs b/src/CLaSH/Rewrite/Util.hs
--- a/src/CLaSH/Rewrite/Util.hs
+++ b/src/CLaSH/Rewrite/Util.hs
@@ -8,15 +8,14 @@
 import           Control.Lens                (Lens', (%=), (+=), (^.))
 import qualified Control.Lens                as Lens
 import qualified Control.Monad               as Monad
-import qualified Control.Monad.Reader        as Reader
-import qualified Control.Monad.State         as State
-import           Control.Monad.Trans.Class   (lift)
+import qualified Control.Monad.State.Strict  as State
 import qualified Control.Monad.Writer        as Writer
 import           Data.HashMap.Strict         (HashMap)
 import qualified Data.HashMap.Lazy           as HML
 import qualified Data.HashMap.Strict         as HMS
 import qualified Data.List                   as List
 import qualified Data.Map                    as Map
+import           Data.Maybe                  (catMaybes,isJust,mapMaybe)
 import qualified Data.Monoid                 as Monoid
 import qualified Data.Set                    as Set
 import qualified Data.Set.Lens               as Lens
@@ -24,10 +23,11 @@
                                               embed, makeName, name2String,
                                               rebind, rec, string2Name, unbind,
                                               unembed, unrec)
-import qualified Unbound.Generics.LocallyNameless     as Unbound
+import           Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind)
 
 import           CLaSH.Core.DataCon          (dataConInstArgTys)
-import           CLaSH.Core.FreeVars         (termFreeIds, termFreeTyVars, typeFreeVars)
+import           CLaSH.Core.FreeVars         (termFreeIds, termFreeTyVars,
+                                              typeFreeVars)
 import           CLaSH.Core.Pretty           (showDoc)
 import           CLaSH.Core.Subst            (substTm)
 import           CLaSH.Core.Term             (LetBinding, Pat (..), Term (..),
@@ -45,30 +45,27 @@
 import           CLaSH.Rewrite.Types
 import           CLaSH.Util
 
--- | Lift an action working in the inner monad to the 'RewriteMonad'
-liftR :: Monad m => m a -> RewriteMonad m a
-liftR m = lift . lift . lift . lift $ m
-
--- | Lift an action working in the inner monad to the 'RewriteSession'
-liftRS :: Monad m => m a -> RewriteSession m a
-liftRS m = lift . lift . lift $ m
+-- | Lift an action working in the '_extra' state to the 'RewriteMonad'
+zoomExtra :: State.State extra a
+          -> RewriteMonad extra a
+zoomExtra m = R (\_ s -> case State.runState m (s ^. extra) of
+                           (a,s') -> (a,s {_extra = s'},mempty))
 
 -- | Record if a transformation is succesfully applied
-apply :: (Monad m, Functor m)
-      => String -- ^ Name of the transformation
-      -> Rewrite m -- ^ Transformation to be applied
-      -> Rewrite m
-apply name rewrite ctx expr = R $ do
+apply :: String -- ^ Name of the transformation
+      -> Rewrite extra -- ^ Transformation to be applied
+      -> Rewrite extra
+apply name rewrite ctx expr = do
   lvl <- Lens.view dbgLevel
   let before = showDoc expr
-  (expr', anyChanged) <- traceIf (lvl >= DebugAll) ("Trying: " ++ name ++ " on:\n" ++ before) $ Writer.listen $ runR $ rewrite ctx expr
+  (expr', anyChanged) <- traceIf (lvl >= DebugAll) ("Trying: " ++ name ++ " on:\n" ++ before) $ Writer.listen $ rewrite ctx expr
   let hasChanged = Monoid.getAny anyChanged
   Monad.when hasChanged $ transformCounter += 1
   let after  = showDoc expr'
   let expr'' = if hasChanged then expr' else expr
 
   Monad.when (lvl > DebugNone && hasChanged) $ do
-    tcm                  <- Lens.use tcCache
+    tcm                  <- Lens.view tcCache
     beforeTy             <- fmap transparentTy $ termType tcm expr
     let beforeFTV        = Lens.setOf termFreeTyVars expr
     beforeFV             <- Lens.setOf <$> localFreeIds <*> pure expr
@@ -105,34 +102,31 @@
         return expr''
 
 -- | Perform a transformation on a Term
-runRewrite :: (Monad m, Functor m)
-           => String -- ^ Name of the transformation
-           -> Rewrite m -- ^ Transformation to perform
+runRewrite :: String -- ^ Name of the transformation
+           -> Rewrite extra -- ^ Transformation to perform
            -> Term  -- ^ Term to transform
-           -> RewriteSession m Term
-runRewrite name rewrite expr = do
-  (expr',_) <- Writer.runWriterT . runR $ apply name rewrite [] expr
-  return expr'
+           -> RewriteMonad extra Term
+runRewrite name rewrite expr = apply name rewrite [] expr
 
 -- | Evaluate a RewriteSession to its inner monad
-runRewriteSession :: (Functor m, Monad m)
-                  => DebugLevel
-                  -> RewriteState
-                  -> RewriteSession m a
-                  -> m a
-runRewriteSession lvl st
-  = Unbound.runFreshMT
-  . fmap (\(a,s) -> traceIf True ("Applied " ++ show (s ^. transformCounter) ++ " transformations") a)
-  . (`State.runStateT` st)
-  . (`Reader.runReaderT` RE lvl)
+runRewriteSession :: RewriteEnv
+                  -> RewriteState extra
+                  -> RewriteMonad extra a
+                  -> a
+runRewriteSession r s m = traceIf True ("Applied " ++
+                                        show (s' ^. transformCounter) ++
+                                        " transformations")
+                                  a
+  where
+    (a,s',_) = runR m r s
 
 -- | Notify that a transformation has changed the expression
-setChanged :: Monad m => RewriteMonad m ()
+setChanged :: RewriteMonad extra ()
 setChanged = Writer.tell (Monoid.Any True)
 
 -- | Identity function that additionally notifies that a transformation has
 -- changed the expression
-changed :: Monad m => a -> RewriteMonad m a
+changed :: a -> RewriteMonad extra a
 changed val = do
   Writer.tell (Monoid.Any True)
   return val
@@ -173,9 +167,8 @@
 
 -- | Create a complete type and kind context out of the global binders and the
 -- transformation context
-mkEnv :: (Functor m, Monad m)
-      => [CoreContext]
-      -> RewriteMonad m (Gamma, Delta)
+mkEnv :: [CoreContext]
+      -> RewriteMonad extra (Gamma, Delta)
 mkEnv ctx = do
   let (gamma,delta) = contextEnv ctx
   tsMap             <- fmap (HML.map fst) $ Lens.use bindings
@@ -216,12 +209,12 @@
   return (Id name' (embed ty),Var ty name')
 
 -- | Inline the binders in a let-binding that have a certain property
-inlineBinders :: Monad m
-              => (LetBinding -> RewriteMonad m Bool) -- ^ Property test
-              -> Rewrite m
-inlineBinders condition _ expr@(Letrec b) = R $ do
+inlineBinders :: (Term -> LetBinding -> RewriteMonad extra Bool) -- ^ Property test
+              -> Rewrite extra
+inlineBinders condition _ expr@(Letrec b) = do
   (xes,res)        <- unbind b
-  (replace,others) <- partitionM condition (unrec xes)
+  let expr' = Letrec (bind xes res)
+  (replace,others) <- partitionM (condition expr') (unrec xes)
   case replace of
     [] -> return expr
     _  -> do
@@ -229,10 +222,61 @@
           newExpr = case others' of
                           [] -> res'
                           _  -> Letrec (bind (rec others') res')
+
       changed newExpr
 
 inlineBinders _ _ e = return e
 
+-- | Determine whether a binder is a join-point created for a complex case
+-- expression.
+--
+-- A join-point is when a local function only occurs in tail-call positions,
+-- and when it does, more than once.
+isJoinPointIn :: Id   -- ^ 'Id' of the local binder
+              -> Term -- ^ Expression in which the binder is bound
+              -> Bool
+isJoinPointIn id_ e = case tailCalls id_ e of
+                      Just n | n > 1 -> True
+                      _              -> False
+
+-- | Count the number of (only) tail calls of a function in an expression.
+-- 'Nothing' indicates that the function was used in a non-tail call position.
+tailCalls :: Id   -- ^ Function to check
+          -> Term -- ^ Expression to check it in
+          -> Maybe Int
+tailCalls id_ expr = case expr of
+  Var _ nm | varName id_ == nm -> Just 1
+           | otherwise       -> Just 0
+  Lam b -> let (_,expr') = unsafeUnbind b
+           in  tailCalls id_ expr'
+  TyLam b -> let (_,expr') = unsafeUnbind b
+             in  tailCalls id_ expr'
+  App l r  -> case tailCalls id_ r of
+                Just 0 -> tailCalls id_ l
+                _      -> Nothing
+  TyApp l _ -> tailCalls id_ l
+  Letrec b ->
+    let (bsR,expr')     = unsafeUnbind b
+        (bsIds,bsExprs) = unzip (unrec bsR)
+        bsTls           = map (tailCalls id_ . unembed) bsExprs
+        bsIdsUsed       = mapMaybe (\(l,r) -> pure l <* r) (zip bsIds bsTls)
+        bsIdsTls        = map (`tailCalls` expr') bsIdsUsed
+        bsCount         = pure . sum $ catMaybes bsTls
+    in  case (all isJust bsTls) of
+          False -> Nothing
+          True  -> case (all (==0) $ catMaybes bsTls) of
+            False  -> case all isJust bsIdsTls of
+              False -> Nothing
+              True  -> (+) <$> bsCount <*> tailCalls id_ expr'
+            True -> tailCalls id_ expr'
+  Case scrut _ alts ->
+    let scrutTl = tailCalls id_ scrut
+        altsTl  = map (tailCalls id_ . snd . unsafeUnbind) alts
+    in  case scrutTl of
+          Just 0 | all (/= Nothing) altsTl -> Just (sum (catMaybes altsTl))
+          _ -> Nothing
+  _ -> Just 0
+
 -- | Substitute the RHS of the first set of Let-binders for references to the
 -- first set of Let-binders in: the second set of Let-binders and the additional
 -- term
@@ -261,20 +305,20 @@
 
 -- | Calculate the /local/ free variable of an expression: the free variables
 -- that are not bound in the global environment.
-localFreeIds :: (Applicative f, Lens.Contravariant f, Monad m)
-             => RewriteMonad m ((TmName -> f TmName) -> Term -> f Term)
+localFreeIds :: (Applicative f, Lens.Contravariant f)
+             => RewriteMonad extra ((TmName -> f TmName) -> Term -> f Term)
 localFreeIds = do
   globalBndrs <- Lens.use bindings
   return ((termFreeIds . Lens.filtered (not . (`HML.member` globalBndrs))))
 
 -- | Lift the binders in a let-binding to a global function that have a certain
 -- property
-liftBinders :: (Functor m, Monad m)
-            => (LetBinding -> RewriteMonad m Bool) -- ^ Property test
-            -> Rewrite m
-liftBinders condition ctx expr@(Letrec b) = R $ do
+liftBinders :: (Term -> LetBinding -> RewriteMonad extra Bool) -- ^ Property test
+            -> Rewrite extra
+liftBinders condition ctx expr@(Letrec b) = do
   (xes,res)        <- unbind b
-  (replace,others) <- partitionM condition (unrec xes)
+  let expr' = Letrec (bind xes res)
+  (replace,others) <- partitionM (condition expr') (unrec xes)
   case replace of
     [] -> return expr
     _  -> do
@@ -291,11 +335,10 @@
 -- | Create a global function for a Let-binding and return a Let-binding where
 -- the RHS is a reference to the new global function applied to the free
 -- variables of the original RHS
-liftBinding :: (Functor m, Monad m)
-            => Gamma
+liftBinding :: Gamma
             -> Delta
             -> LetBinding
-            -> RewriteMonad m LetBinding
+            -> RewriteMonad extra LetBinding
 liftBinding gamma delta (Id idName tyE,eE) = do
   let ty = unembed tyE
       e  = unembed eE
@@ -309,9 +352,10 @@
       boundFTVs = zipWith mkTyVar localFTVkinds localFTVs
       boundFVs  = zipWith mkId localFVtys' localFVs'
   -- Make a new global ID
-  tcm       <- Lens.use tcCache
+  tcm       <- Lens.view tcCache
   newBodyTy <- termType tcm $ mkTyLams (mkLams e boundFVs) boundFTVs
-  newBodyId <- fmap (makeName (name2String idName) . toInteger) getUniqueM
+  cf        <- Lens.use curFun
+  newBodyId <- fmap (makeName (name2String cf ++ "_" ++ name2String idName) . toInteger) getUniqueM
   -- Make a new expression, consisting of the the lifted function applied to
   -- its free variables
   let newExpr = mkTmApps
@@ -330,48 +374,43 @@
 liftBinding _ _ _ = error $ $(curLoc) ++ "liftBinding: invalid core, expr bound to tyvar"
 
 -- | Make a global function for a name-term tuple
-mkFunction :: (Functor m, Monad m)
-           => TmName -- ^ Name of the function
+mkFunction :: TmName -- ^ Name of the function
            -> Term -- ^ Term bound to the function
-           -> RewriteMonad m (TmName,Type) -- ^ Name with a proper unique and the type of the function
+           -> RewriteMonad extra (TmName,Type) -- ^ Name with a proper unique and the type of the function
 mkFunction bndr body = do
-  tcm    <- Lens.use tcCache
+  tcm    <- Lens.view tcCache
   bodyTy <- termType tcm body
   bodyId <- cloneVar bndr
   addGlobalBind bodyId bodyTy body
   return (bodyId,bodyTy)
 
 -- | Add a function to the set of global binders
-addGlobalBind :: (Functor m, Monad m)
-              => TmName
+addGlobalBind :: TmName
               -> Type
               -> Term
-              -> RewriteMonad m ()
+              -> RewriteMonad extra ()
 addGlobalBind vId ty body = (ty,body) `deepseq` bindings %= HMS.insert vId (ty,body)
 
 -- | Create a new name out of the given name, but with another unique
-cloneVar :: (Functor m, Monad m)
-         => TmName
-         -> RewriteMonad m TmName
+cloneVar :: TmName
+         -> RewriteMonad extra TmName
 cloneVar name = fmap (makeName (name2String name) . toInteger) getUniqueM
 
 
 -- | Test whether a term is a variable reference to a local binder
-isLocalVar :: (Functor m, Monad m)
-           => Term
-           -> RewriteMonad m Bool
+isLocalVar :: Term
+           -> RewriteMonad extra Bool
 isLocalVar (Var _ name)
   = fmap (not . HML.member name)
   $ Lens.use bindings
 isLocalVar _ = return False
 
 -- | Determine if a term cannot be represented in hardware
-isUntranslatable :: (Functor m, Monad m)
-                 => Term
-                 -> RewriteMonad m Bool
+isUntranslatable :: Term
+                 -> RewriteMonad extra Bool
 isUntranslatable tm = do
-  tcm <- Lens.use tcCache
-  not <$> (representableType <$> Lens.use typeTranslator <*> pure tcm <*> termType tcm tm)
+  tcm <- Lens.view tcCache
+  not <$> (representableType <$> Lens.view typeTranslator <*> pure tcm <*> termType tcm tm)
 
 -- | Is the Context a Lambda/Term-abstraction context?
 isLambdaBodyCtx :: CoreContext
@@ -418,37 +457,34 @@
     _ -> cantCreate $(curLoc) ("Type of subject is not a datatype: " ++ showDoc scrutTy)
 
 -- | Specialise an application on its argument
-specialise :: (Functor m, State.MonadState s m)
-           => Lens' s (Map.Map (TmName, Int, Either Term Type) (TmName,Type)) -- ^ Lens into previous specialisations
-           -> Lens' s (HashMap TmName Int) -- ^ Lens into the specialisation history
-           -> Lens' s Int -- ^ Lens into the specialisation limit
+specialise :: Lens' extra (Map.Map (TmName, Int, Either Term Type) (TmName,Type)) -- ^ Lens into previous specialisations
+           -> Lens' extra (HashMap TmName Int) -- ^ Lens into the specialisation history
+           -> Lens' extra Int -- ^ Lens into the specialisation limit
            -> Bool
-           -> Rewrite m
+           -> Rewrite extra
 specialise specMapLbl specHistLbl specLimitLbl doCheck ctx e = case e of
   (TyApp e1 ty) -> specialise' specMapLbl specHistLbl specLimitLbl False ctx e (collectArgs e1) (Right ty)
   (App e1 e2)   -> specialise' specMapLbl specHistLbl specLimitLbl doCheck ctx e (collectArgs e1) (Left  e2)
   _             -> return e
 
 -- | Specialise an application on its argument
-specialise' :: (Functor m, State.MonadState s m)
-            => Lens' s (Map.Map (TmName, Int, Either Term Type) (TmName,Type)) -- ^ Lens into previous specialisations
-            -> Lens' s (HashMap TmName Int) -- ^ Lens into specialisation history
-            -> Lens' s Int -- ^ Lens into the specialisation limit
+specialise' :: Lens' extra (Map.Map (TmName, Int, Either Term Type) (TmName,Type)) -- ^ Lens into previous specialisations
+            -> Lens' extra (HashMap TmName Int) -- ^ Lens into specialisation history
+            -> Lens' extra Int -- ^ Lens into the specialisation limit
             -> Bool -- ^ Perform specialisation limit check
             -> [CoreContext] -- Transformation context
             -> Term -- ^ Original term
             -> (Term, [Either Term Type]) -- ^ Function part of the term, split into root and applied arguments
             -> Either Term Type -- ^ Argument to specialize on
-            -> R m Term
-specialise' specMapLbl specHistLbl specLimitLbl doCheck ctx e (Var _ f, args) specArg = R $ do
+            -> RewriteMonad extra Term
+specialise' specMapLbl specHistLbl specLimitLbl doCheck ctx e (Var _ f, args) specArg = do
   lvl <- Lens.view dbgLevel
   -- Create binders and variable references for free variables in 'specArg'
   (specBndrs,specVars) <- specArgBndrsAndVars ctx specArg
   let argLen  = length args
       specAbs = either (Left . (`mkAbstraction` specBndrs)) (Right . id) specArg
   -- Determine if 'f' has already been specialized on 'specArg'
-  specM <- liftR $ fmap (Map.lookup (f,argLen,specAbs))
-                 $ Lens.use specMapLbl
+  specM <- Map.lookup (f,argLen,specAbs) <$> Lens.use (extra.specMapLbl)
   case specM of
     -- Use previously specialized function
     Just (fname,fty) ->
@@ -461,8 +497,8 @@
       case bodyMaybe of
         Just (_,bodyTm) -> do
           -- Determine if we see a sequence of specialisations on a growing argument
-          specHistM <- liftR $ fmap (HML.lookup f) (Lens.use specHistLbl)
-          specLim   <- liftR $ Lens.use specLimitLbl
+          specHistM <- HML.lookup f <$> Lens.use (extra.specHistLbl)
+          specLim   <- Lens.use (extra . specLimitLbl)
           if doCheck && maybe False (> specLim) specHistM
             then fail $ unlines [ "Hit specialisation limit " ++ show specLim ++ " on function `" ++ showDoc f ++ "'.\n"
                                 , "The function `" ++ showDoc f ++ "' is most likely recursive, and looks like it is being indefinitely specialized on a growing argument.\n"
@@ -472,21 +508,21 @@
                                 ]
             else do
               -- Make new binders for existing arguments
-              tcm                 <- Lens.use tcCache
+              tcm                 <- Lens.view tcCache
               (boundArgs,argVars) <- fmap (unzip . map (either (Left *** Left) (Right *** Right))) $
                                      mapM (mkBinderFor tcm "pTS") args
               -- Create specialized functions
               let newBody = mkAbstraction (mkApps bodyTm (argVars ++ [specArg])) (boundArgs ++ specBndrs)
               newf <- mkFunction f newBody
               -- Remember specialization
-              liftR $ specHistLbl %= HML.insertWith (+) f 1
-              liftR $ specMapLbl %= Map.insert (f,argLen,specAbs) newf
+              (extra.specHistLbl) %= HML.insertWith (+) f 1
+              (extra.specMapLbl)  %= Map.insert (f,argLen,specAbs) newf
               -- use specialized function
               let newExpr = mkApps ((uncurry . flip) Var newf) (args ++ specVars)
               newf `deepseq` changed newExpr
         Nothing -> return e
 
-specialise' _ _ _ _ ctx _ (appE,args) (Left specArg) = R $ do
+specialise' _ _ _ _ ctx _ (appE,args) (Left specArg) = do
   -- Create binders and variable references for free variables in 'specArg'
   (specBndrs,specVars) <- specArgBndrsAndVars ctx (Left specArg)
   -- Create specialized function
@@ -501,10 +537,9 @@
 specialise' _ _ _ _ _ e _ _ = return e
 
 -- | Create binders and variable references for free variables in 'specArg'
-specArgBndrsAndVars :: (Functor m, Monad m)
-                    => [CoreContext]
+specArgBndrsAndVars :: [CoreContext]
                     -> Either Term Type
-                    -> RewriteMonad m ([Either Id TyVar],[Either Term Type])
+                    -> RewriteMonad extra ([Either Id TyVar],[Either Term Type])
 specArgBndrsAndVars ctx specArg = do
   let specFTVs = List.nub $ either (Lens.toListOf termFreeTyVars) (Lens.toListOf typeFreeVars) specArg
   specFVs <- List.nub <$> either ((Lens.toListOf <$> localFreeIds <*>) . pure) (const (pure [])) specArg
diff --git a/src/Unbound/Generics/LocallyNameless/Extra.hs b/src/Unbound/Generics/LocallyNameless/Extra.hs
--- a/src/Unbound/Generics/LocallyNameless/Extra.hs
+++ b/src/Unbound/Generics/LocallyNameless/Extra.hs
@@ -6,6 +6,10 @@
 
 module Unbound.Generics.LocallyNameless.Extra where
 
+#ifndef CABAL
+#define MIN_VERSION_unbound_generics(x,y,z)(1)
+#endif
+
 #if MIN_VERSION_unbound_generics(0,2,0)
 #else
 import Control.DeepSeq