diff --git a/DDC/Core/Analysis/Arity.hs b/DDC/Core/Analysis/Arity.hs
--- a/DDC/Core/Analysis/Arity.hs
+++ b/DDC/Core/Analysis/Arity.hs
@@ -96,7 +96,7 @@
                 Nothing         -> Nothing
                 Just a          -> Just (b, a)
    in case ll of
-        LLet _ b x      -> sequence $ map get [(b, x)]
+        LLet b x        -> sequence $ map get [(b, x)]
         LRec bxs        -> sequence $ map get bxs
         _               -> Just []
 
diff --git a/DDC/Core/Analysis/Usage.hs b/DDC/Core/Analysis/Usage.hs
--- a/DDC/Core/Analysis/Usage.hs
+++ b/DDC/Core/Analysis/Usage.hs
@@ -19,7 +19,7 @@
 -- Used -----------------------------------------------------------------------
 -- | Tracks how a bound variable is used.
 data Used
-        -- | Bound variable is used as the function of an application.
+        -- | Bound variable is used as the function in an application.
         = UsedFunction
 
         -- | Bound variable is destructed by a case-expression.
@@ -71,7 +71,7 @@
         = foldl' plusUsedMap m ms
 
 
--- Usage ----------------------------------------------------------------------
+-- Module ---------------------------------------------------------------------
 -- | Annotate all binding occurrences of variables in an expression
 --   with how they are used.
 usageModule 
@@ -96,6 +96,7 @@
                 , moduleBody            = usageX body }
 
 
+-- Exp ------------------------------------------------------------------------
 -- | Annotate all binding occurrences of variables in an expression
 --   with how they are used.
 usageX  :: Ord n 
@@ -182,7 +183,9 @@
          -> (empty, XType t)
 
         XWitness w     
-         -> (empty, XWitness w)
+         | (used', w')    <- usageWitness w
+         -> ( used'
+            , XWitness w')
 
 
 -- | Annotate binding occurences of named variables with usage information.
@@ -193,9 +196,9 @@
 
 usageLets lts
  = case lts of
-        LLet mode b x
-         |  (used, x')   <- usageX' x
-         -> (used, LLet mode b x')
+        LLet b x
+         |  (used1', x')        <- usageX' x
+         -> (used1', LLet b x')
 
         LRec bxs
          |  (bs, xs)      <- unzip bxs
@@ -228,12 +231,17 @@
          -> (UsedMap usedCasts, CastWeakenClosure xs')
 
         CastPurify w
-         -> (empty, CastPurify w)
+         | (used, w')   <- usageWitness w
+         -> (used, CastPurify w')
 
         CastForget w
-         -> (empty, CastForget w)
+         | (used, w')   <- usageWitness w
+         -> (used, CastForget w')
 
+        CastSuspend     -> (empty, CastSuspend)
+        CastRun         -> (empty, CastRun)
 
+
 -- | Annotate binding occurrences of named level-0 variables with
 --   usage information.
 usageAlt  
@@ -246,3 +254,32 @@
    in   (used, AAlt p x')
 
 
+-- | Annotate binding occurrences of named level-0 variables with
+--   usage information.
+usageWitness
+        :: Ord n
+        => Witness a n
+        -> (UsedMap n, Witness (UsedMap n, a) n)
+
+usageWitness ww
+ = case ww of
+        WVar a u
+         -> (empty, WVar (empty, a) u)
+
+        WCon a c
+         -> (empty, WCon (empty, a) c)
+
+        WApp a w1 w2
+         | (used1, w1') <- usageWitness w1
+         , (used2, w2') <- usageWitness w2
+         , used'        <- plusUsedMap used1 used2
+         -> (empty, WApp (used', a) w1' w2')
+
+        WJoin a w1 w2
+         | (used1, w1') <- usageWitness w1
+         , (used2, w2') <- usageWitness w2
+         , used'        <- plusUsedMap used1 used2
+         -> (empty, WJoin (used', a) w1' w2')
+
+        WType a t
+         -> (empty, WType (empty, a) t)
diff --git a/DDC/Core/Simplifier/Apply.hs b/DDC/Core/Simplifier/Apply.hs
--- a/DDC/Core/Simplifier/Apply.hs
+++ b/DDC/Core/Simplifier/Apply.hs
@@ -12,11 +12,12 @@
 import DDC.Core.Fragment
 import DDC.Core.Simplifier.Base
 import DDC.Core.Transform.AnonymizeX
-import DDC.Core.Transform.Snip
+import DDC.Core.Transform.Snip          as Snip
 import DDC.Core.Transform.Flatten
 import DDC.Core.Transform.Beta
+import DDC.Core.Transform.Eta           as Eta
 import DDC.Core.Transform.Prune
-import DDC.Core.Transform.Forward
+import DDC.Core.Transform.Forward       as Forward
 import DDC.Core.Transform.Bubble
 import DDC.Core.Transform.Inline
 import DDC.Core.Transform.Namify
@@ -79,12 +80,15 @@
  = case spec of
         Id               -> return mm
         Anonymize        -> return $ anonymizeX mm
-        Snip             -> return $ snip False mm
-        SnipOver         -> return $ snip True mm
+        Snip config      -> return $ snip config mm
         Flatten          -> return $ flatten mm
-        Beta             -> return $ result $ betaReduce False mm
-        BetaLets         -> return $ result $ betaReduce True  mm
-        Forward          -> return $ forwardModule profile mm
+        Beta config      -> return $ result $ betaReduce config mm
+        Eta  config      -> return $ result $ Eta.etaModule config profile mm
+
+        Forward          
+         -> let config  = Forward.Config (const FloatAllow) False
+            in  return $ result $ forwardModule profile config mm
+
         Bubble           -> return $ bubbleModule mm
         Namify namK namT -> namifyUnique namK namT mm
         Inline getDef    -> return $ inline getDef Set.empty mm
@@ -225,14 +229,17 @@
    in case spec of
         Id                -> res xx
         Anonymize         -> res    $ anonymizeX xx
-        Snip              -> res    $ snip False xx
-        SnipOver          -> res    $ snip True xx
+        Snip config       -> res    $ snip config xx
         Flatten           -> res    $ flatten xx
         Inline  getDef    -> res    $ inline getDef Set.empty xx
-        Beta              -> return $ betaReduce False xx
-        BetaLets          -> return $ betaReduce True  xx
+        Beta config       -> return $ betaReduce config xx
+        Eta  config       -> return $ Eta.etaX config profile kenv tenv xx
         Prune             -> return $ pruneX   profile kenv tenv xx
-        Forward           -> return $ forwardX profile xx
+
+        Forward          
+         -> let config  = Forward.Config (const FloatAllow) False
+            in  return $ forwardX profile config xx
+
         Bubble            -> res    $ bubbleX kenv tenv xx
         Namify  namK namT -> namifyUnique namK namT xx >>= res
         Rewrite rules     -> return $ rewriteX rules xx
diff --git a/DDC/Core/Simplifier/Base.hs b/DDC/Core/Simplifier/Base.hs
--- a/DDC/Core/Simplifier/Base.hs
+++ b/DDC/Core/Simplifier/Base.hs
@@ -11,17 +11,19 @@
           -- * Transform Results
         , TransformResult(..)
 	, TransformInfo(..)
-	, NoInformation(..)
+	, NoInformation
 	, resultDone)
 where
+import DDC.Core.Simplifier.Result
 import DDC.Core.Transform.Rewrite.Rule
 import DDC.Core.Transform.Namify
 import DDC.Core.Exp
 import DDC.Type.Env
 import DDC.Base.Pretty
-import qualified DDC.Base.Pretty	as P
+import qualified DDC.Core.Transform.Snip        as Snip
+import qualified DDC.Core.Transform.Eta         as Eta
+import qualified DDC.Core.Transform.Beta        as Beta
 import Data.Monoid
-import Data.Typeable (Typeable)
 
 
 -- Simplifier -----------------------------------------------------------------
@@ -67,21 +69,16 @@
         | Anonymize
 
         -- | Introduce let-bindings for nested applications.
-        | Snip
-
-        -- | Introduce let-bindings for nested applications and over-applied
-        --   functions
-        | SnipOver
+        | Snip  Snip.Config
 
         -- | Flatten nested let and case expressions.
         | Flatten
 
         -- | Perform beta reduction when the argument is not a redex.
-        | Beta
+        | Beta  Beta.Config
 
-        -- | Perform beta reduction, introducing new let-bindings for 
-        --   arguments that are redexes.
-        | BetaLets
+        -- | Perform eta expansion and reduction.
+        | Eta    Eta.Config
 
         -- | Remove unused, pure let bindings.
         | Prune
@@ -133,11 +130,10 @@
   = case ss of
         Id              -> text "Id"
         Anonymize       -> text "Anonymize"
-        Snip            -> text "Snip"
-        SnipOver        -> text "Snip"
+        Snip{}          -> text "Snip"
         Flatten         -> text "Flatten"
-        Beta            -> text "Beta"
-        BetaLets        -> text "BetaLets"
+        Beta{}          -> text "Beta"
+        Eta{}           -> text "Eta"
         Prune           -> text "Prune"
         Forward         -> text "Forward"
         Bubble          -> text "Bubble"
@@ -146,62 +142,3 @@
         Rewrite{}       -> text "Rewrite"
         Elaborate       -> text "Elaborate"
 
-
--- TransformResult ------------------------------------------------------------
--- | Package up the result of applying a single transform.
-data TransformResult r
-        = TransformResult
-        { -- | Transform result proper (eg the new module)
-          result         :: r
-
-          -- | Whether this transform made any progess.
-          --   
-          --   If `False` then the result program must be the same as the
-          --   input program, and a simplifer fixpoint won't apply this
-          --   transform again to the result program.
-        , resultProgress :: Bool
-
-          -- | Whether it might help to run the same transform again.
-          -- 
-          --   If `False` then a simplifier fixpoint won't apply this transform
-          --   again to the result program.
-        , resultAgain    :: Bool
-
-          -- | Transform specific log. This might contain a count of what rules
-          --   fired, or information about what parts of the program couldn't
-          --   be processed.
-        , resultInfo     :: TransformInfo }
-
-
--- | Existential package for a typeable thing,
---   used in `TransformResult`.
-data TransformInfo
-	=  forall i
-        .  (Typeable i, Pretty i)
-	=> TransformInfo i
-
-
--- | Place-holder type to use when there is no real `TransformResult`.
-data NoInformation 
-        = NoInformation String
-        deriving Typeable
-
-
-instance Pretty NoInformation where
-    ppr (NoInformation name) = text name P.<> text ": No information"
-
-
-instance Pretty (TransformResult r) where
- ppr (TransformResult _ _ _ (TransformInfo i))
-  = ppr i
-
-
--- | Create a default result with no transform again.
---  
---   We'll say we made progress, but set `resultAgain` to False
---   so to stop any simplifier fixpoints.
-resultDone :: String -> r -> TransformResult r
-resultDone name r 
-        = TransformResult r True False
-        $ TransformInfo 
-        $ NoInformation name
diff --git a/DDC/Core/Simplifier/Parser.hs b/DDC/Core/Simplifier/Parser.hs
--- a/DDC/Core/Simplifier/Parser.hs
+++ b/DDC/Core/Simplifier/Parser.hs
@@ -11,11 +11,14 @@
 import DDC.Core.Simplifier.Lexer
 import DDC.Data.Token
 import DDC.Data.SourcePos
-import DDC.Base.Parser                  (pTok)
-import Data.Set                         (Set)
-import qualified DDC.Base.Parser        as P
-import qualified Data.Map               as Map
-import qualified Data.Set               as Set
+import DDC.Base.Parser                          (pTok)
+import Data.Set                                 (Set)
+import qualified DDC.Core.Transform.Snip        as Snip
+import qualified DDC.Core.Transform.Beta        as Beta
+import qualified DDC.Core.Transform.Eta         as Eta
+import qualified DDC.Base.Parser                as P
+import qualified Data.Map                       as Map
+import qualified Data.Set                       as Set
 
 
 -------------------------------------------------------------------------------
@@ -189,11 +192,17 @@
  = case name of
         "Id"            -> Just Id
         "Anonymize"     -> Just Anonymize
-        "Snip"          -> Just Snip
-        "SnipOver"      -> Just SnipOver
+
+        "Snip"          -> Just (Snip Snip.configZero)
+        "SnipOver"      -> Just (Snip Snip.configZero { Snip.configSnipOverApplied = True })
+
+        "Eta"           -> Just (Eta  Eta.configZero  { Eta.configExpand = True })
+
         "Flatten"       -> Just Flatten
-        "Beta"          -> Just Beta
-        "BetaLets"      -> Just BetaLets
+
+        "Beta"          -> Just (Beta Beta.configZero)
+        "BetaLets"      -> Just (Beta Beta.configZero { Beta.configBindRedexes    = True })
+
         "Prune"         -> Just Prune
         "Forward"       -> Just Forward
         "Bubble"        -> Just Bubble
diff --git a/DDC/Core/Simplifier/Recipe.hs b/DDC/Core/Simplifier/Recipe.hs
--- a/DDC/Core/Simplifier/Recipe.hs
+++ b/DDC/Core/Simplifier/Recipe.hs
@@ -20,6 +20,8 @@
 where
 import DDC.Core.Simplifier.Base
 import DDC.Core.Transform.Namify
+import qualified DDC.Core.Transform.Snip  as Snip
+import qualified DDC.Core.Transform.Beta  as Beta
 import DDC.Type.Env
 import Data.Monoid
 
@@ -39,12 +41,12 @@
 
 -- | Introduce let-bindings for nested applications.
 snip      :: Simplifier s a n
-snip      = Trans Snip
+snip      = Trans (Snip Snip.configZero)
 
 
 -- | Introduce let-bindings for nested applications.
 snipOver  :: Simplifier s a n
-snipOver  = Trans SnipOver
+snipOver  = Trans (Snip Snip.configZero { Snip.configSnipOverApplied = True })
 
 
 -- | Flatten nested let and case expressions.
@@ -54,12 +56,12 @@
 
 -- | Perform beta reduction
 beta    :: Simplifier s a n
-beta    = Trans Beta
+beta    = Trans (Beta Beta.configZero)
 
 
 -- | Perform beta reduction, introducing let-expressions for compound arguments.
 betaLets :: Simplifier s a n
-betaLets = Trans BetaLets
+betaLets = Trans (Beta Beta.configZero { Beta.configBindRedexes = True })
 
 
 -- | Remove unused, pure let bindings.
@@ -93,7 +95,7 @@
         -> Simplifier s a n
 
 anormalize namK namT
-        =  Trans Snip 
+        =  snip
         <> Trans Flatten 
         <> Trans (Namify namK namT)
 
diff --git a/DDC/Core/Simplifier/Result.hs b/DDC/Core/Simplifier/Result.hs
new file mode 100644
--- /dev/null
+++ b/DDC/Core/Simplifier/Result.hs
@@ -0,0 +1,70 @@
+
+module DDC.Core.Simplifier.Result
+        ( TransformResult (..)
+        , TransformInfo   (..)
+        , NoInformation
+        , resultDone)
+where
+import DDC.Base.Pretty
+import Data.Typeable
+import qualified DDC.Base.Pretty                as P
+
+
+-- TransformResult ------------------------------------------------------------
+-- | Package up the result of applying a single transform.
+data TransformResult r
+        = TransformResult
+        { -- | Transform result proper (eg the new module)
+          result         :: r
+
+          -- | Whether this transform made any progess.
+          --   
+          --   If `False` then the result program must be the same as the
+          --   input program, and a simplifer fixpoint won't apply this
+          --   transform again to the result program.
+        , resultProgress :: Bool
+
+          -- | Whether it might help to run the same transform again.
+          -- 
+          --   If `False` then a simplifier fixpoint won't apply this transform
+          --   again to the result program.
+        , resultAgain    :: Bool
+
+          -- | Transform specific log. This might contain a count of what rules
+          --   fired, or information about what parts of the program couldn't
+          --   be processed.
+        , resultInfo     :: TransformInfo }
+
+
+-- | Existential package for a typeable thing,
+--   used in `TransformResult`.
+data TransformInfo
+        =  forall i
+        .  (Typeable i, Pretty i)
+        => TransformInfo i
+
+
+-- | Place-holder type to use when there is no real `TransformResult`.
+data NoInformation 
+        = NoInformation String
+        deriving Typeable
+
+
+instance Pretty NoInformation where
+    ppr (NoInformation name) = text name P.<> text ": No information"
+
+
+instance Pretty (TransformResult r) where
+ ppr (TransformResult _ _ _ (TransformInfo i))
+  = ppr i
+
+
+-- | Create a default result with no transform again.
+--  
+--   We'll say we made progress, but set `resultAgain` to False
+--   so to stop any simplifier fixpoints.
+resultDone :: String -> r -> TransformResult r
+resultDone name r 
+        = TransformResult r True False
+        $ TransformInfo 
+        $ NoInformation name
diff --git a/DDC/Core/Transform/AnonymizeX.hs b/DDC/Core/Transform/AnonymizeX.hs
--- a/DDC/Core/Transform/AnonymizeX.hs
+++ b/DDC/Core/Transform/AnonymizeX.hs
@@ -9,7 +9,6 @@
 import DDC.Core.Exp
 import DDC.Type.Transform.AnonymizeT
 import DDC.Type.Compounds
-import Control.Monad
 import Data.List
 import Data.Set                         (Set)
 import qualified Data.Set               as Set
@@ -89,25 +88,12 @@
  anonymizeWithX keep kstack tstack cc
   = let down = anonymizeWithX keep kstack tstack
     in case cc of
-        CastWeakenEffect eff
-         -> CastWeakenEffect  (anonymizeWithT kstack eff)
-
-        CastWeakenClosure xs
-         -> CastWeakenClosure (map down xs)
-
-        CastPurify w
-         -> CastPurify        (down w)
-
-        CastForget w
-         -> CastForget        (down w)
-
-
-instance AnonymizeX LetMode where
- anonymizeWithX keep kstack tstack lm
-  = let down = anonymizeWithX keep kstack tstack
-    in case lm of
-        LetStrict       -> lm
-        LetLazy mw      -> LetLazy $ liftM down mw
+        CastWeakenEffect eff    -> CastWeakenEffect  (anonymizeWithT kstack eff)
+        CastWeakenClosure xs    -> CastWeakenClosure (map down xs)
+        CastPurify w            -> CastPurify        (down w)
+        CastForget w            -> CastForget        (down w)
+        CastSuspend             -> CastSuspend
+        CastRun                 -> CastRun
 
 
 instance AnonymizeX (Alt a) where
@@ -123,19 +109,19 @@
             in  AAlt (PData uCon bs') x'
 
 
-instance AnonymizeX Witness where
+instance AnonymizeX (Witness a) where
  anonymizeWithX keep kstack tstack ww
   = let down = anonymizeWithX keep kstack tstack 
     in case ww of
-        WVar u@(UName _)
+        WVar a u@(UName _)
          |  Just ix      <- findIndex (boundMatchesBind u) tstack
-         -> WVar (UIx ix)
+         -> WVar a (UIx ix)
 
-        WVar u          -> WVar u
-        WCon  c         -> WCon  c
-        WApp  w1 w2     -> WApp  (down w1) (down w2)
-        WJoin w1 w2     -> WJoin (down w1) (down w2)
-        WType t         -> WType (anonymizeWithT kstack t)
+        WVar  a u       -> WVar  a u
+        WCon  a c       -> WCon  a c
+        WApp  a w1 w2   -> WApp  a (down w1) (down w2)
+        WJoin a w1 w2   -> WJoin a (down w1) (down w2)
+        WType a t       -> WType a (anonymizeWithT kstack t)
 
 
 instance AnonymizeX Bind where
@@ -199,11 +185,10 @@
 
 pushAnonymizeLets keep kstack tstack lts
  = case lts of
-        LLet mode b x
-         -> let mode'           = anonymizeWithX     keep kstack tstack mode
-                x'              = anonymizeWithX     keep kstack tstack x
+        LLet b x
+         -> let x'              = anonymizeWithX     keep kstack tstack x
                 (tstack', b')   = pushAnonymizeBindX keep kstack tstack b
-            in  (kstack, tstack', LLet mode' b' x')
+            in  (kstack, tstack', LLet b' x')
 
         LRec bxs 
          -> let (bs, xs)        = unzip bxs
diff --git a/DDC/Core/Transform/Beta.hs b/DDC/Core/Transform/Beta.hs
--- a/DDC/Core/Transform/Beta.hs
+++ b/DDC/Core/Transform/Beta.hs
@@ -2,18 +2,20 @@
 -- | Beta-reduce applications of a explicit lambda abstractions 
 --   to variables and values.
 module DDC.Core.Transform.Beta
-        ( BetaReduceInfo(..)
+        ( Config        (..)
+        , configZero
+        , Info          (..)
         , betaReduce)
 where
 import DDC.Base.Pretty
 import DDC.Core.Collect
 import DDC.Core.Exp
 import DDC.Core.Predicates
-import DDC.Core.Simplifier.Base
-import DDC.Core.Transform.TransformX
+import DDC.Core.Transform.TransformUpX
 import DDC.Core.Transform.SubstituteTX
 import DDC.Core.Transform.SubstituteWX
 import DDC.Core.Transform.SubstituteXX
+import DDC.Core.Simplifier.Result
 import Control.Monad.Writer	        (Writer, runWriter, tell)
 import Data.Monoid		        (Monoid, mempty, mappend)
 import Data.Typeable		        (Typeable)
@@ -24,9 +26,25 @@
 
 
 -------------------------------------------------------------------------------
+data Config
+        = Config
+        { -- | If we find a lambda abstraction applied to a redex then let-bind
+          --   the redex and substitute the new variable instead.
+          configBindRedexes     :: Bool }
+        deriving Show
+
+
+-- | Empty beta configuration with all flags set to False.
+configZero :: Config
+configZero
+        = Config
+        { configBindRedexes     = False }
+
+
+-------------------------------------------------------------------------------
 -- | A summary of what the beta reduction transform did.
-data BetaReduceInfo
-        = BetaReduceInfo
+data Info
+        = Info
         { -- | Number of type applications reduced.
           infoTypes             :: Int
 
@@ -44,8 +62,8 @@
         deriving Typeable
 
 
-instance Pretty BetaReduceInfo where
- ppr (BetaReduceInfo ty wit val lets skip)
+instance Pretty Info where
+ ppr (Info ty wit val lets skip)
   =  text "Beta reduction:"
   <$> indent 4 (vcat
       [ text "Types:          " <> int ty
@@ -55,13 +73,13 @@
       , text "Values skipped: " <> int skip ])
 
 
-instance Monoid BetaReduceInfo where
- mempty = BetaReduceInfo 0 0 0 0 0
- mappend (BetaReduceInfo ty1 wit1 val1 lets1 skip1)
-         (BetaReduceInfo ty2 wit2 val2 lets2 skip2)
-  = (BetaReduceInfo 
+instance Monoid Info where
+ mempty = Info 0 0 0 0 0
+ mappend (Info ty1 wit1 val1 lets1 skip1)
+         (Info ty2 wit2 val2 lets2 skip2)
+  = Info 
                 (ty1   + ty2)   (wit1  + wit2) (val1 + val2)
-                (lets1 + lets2) (skip1 + skip2))
+                (lets1 + lets2) (skip1 + skip2)
 
 
 -------------------------------------------------------------------------------
@@ -73,19 +91,20 @@
 --   instead.
 betaReduce  
         :: forall (c :: * -> * -> *) a n 
-        .  (Ord n, TransformUpMX (Writer BetaReduceInfo) c)
-        => Bool         -- ^ Let-bind redexes.
+        .  (Ord n, TransformUpMX (Writer Info) c)
+        => Config
         -> c a n 
         -> TransformResult (c a n)
-betaReduce lets x
+
+betaReduce config x
  = {-# SCC betaReduce #-}
    let (x', info) = runWriter
-		  $ transformUpMX (betaReduce1 lets) Env.empty Env.empty x
+		  $ transformUpMX (betaReduce1 config) Env.empty Env.empty x
 
        -- Check if any actual work was performed
        progress 
         = case info of
-                BetaReduceInfo ty wit val lets' _
+                Info ty wit val lets' _
                  -> (ty + wit + val + lets') > 0
 
    in  TransformResult
@@ -105,13 +124,13 @@
 --    
 betaReduce1
         :: Ord n
-        => Bool	        -- ^ Let-bind redexes.
+        => Config
         -> Env n
         -> Env n
         -> Exp a n
-        -> Writer BetaReduceInfo (Exp a n)
+        -> Writer Info (Exp a n)
 
-betaReduce1 lets _kenv tenv xx
+betaReduce1 config _kenv tenv xx
  = let  ret info x = tell info >> return x
    in case xx of
 
@@ -168,9 +187,9 @@
                     else XCast a (CastWeakenClosure [x2])
                        $ substituteXX b11 x2 x12
 
-         | lets
+         | configBindRedexes config
          -> ret mempty { infoValuesLetted  = 1 }
-	      $	XLet a (LLet LetStrict b11 x2) x12
+	      $	XLet a (LLet b11 x2) x12
 
          | otherwise
          -> ret mempty { infoValuesSkipped = 1 }
diff --git a/DDC/Core/Transform/Bubble.hs b/DDC/Core/Transform/Bubble.hs
--- a/DDC/Core/Transform/Bubble.hs
+++ b/DDC/Core/Transform/Bubble.hs
@@ -122,11 +122,11 @@
 
         -- Drop casts that mention the bound variable here, 
         -- but we can float the others further outwards.
-        LLet m b x
+        LLet b x
          -> let (cs, x')        = bubble kenv tenv x
                 Just a          = takeAnnotOfExp x'
                 (cs', xc')      = dropCasts kenv tenv a [] [b] cs x'
-            in  (cs', LLet m b xc')
+            in  (cs', LLet b xc')
 
         -- ISSUE #299: Bubble casts out of recursive lets.
         LRec bxs
diff --git a/DDC/Core/Transform/Elaborate.hs b/DDC/Core/Transform/Elaborate.hs
--- a/DDC/Core/Transform/Elaborate.hs
+++ b/DDC/Core/Transform/Elaborate.hs
@@ -75,7 +75,7 @@
 elaborateLets us lts 
  = let down = elaborate us 
    in case lts of
-        LLet m b x -> (us, LLet m b (down x))
+        LLet b x   -> (us, LLet b (down x))
         LRec bs    -> (us, LRec $ map (second down) bs)
 
         LLetRegions brs bws
diff --git a/DDC/Core/Transform/Eta.hs b/DDC/Core/Transform/Eta.hs
new file mode 100644
--- /dev/null
+++ b/DDC/Core/Transform/Eta.hs
@@ -0,0 +1,301 @@
+
+-- Eta-expand functional values.
+---
+-- NOTE: This is module currently just does eta-expansion, but in future
+--       we should expand the config to also make it do expansion/contraction
+--       based on the real arity of bindings.
+--
+module DDC.Core.Transform.Eta
+        ( Config(..)
+        , configZero
+        , Info  (..)
+        , etaModule
+        , etaX)
+where
+import qualified DDC.Core.Check as Check
+import DDC.Core.Module
+import DDC.Core.Exp
+import DDC.Core.Fragment
+import DDC.Core.Transform.LiftX
+import DDC.Core.Transform.LiftT
+import DDC.Core.Simplifier.Result
+import DDC.Core.Compounds
+import DDC.Core.Pretty
+import DDC.Type.Env             (TypeEnv, KindEnv)
+import Control.Monad.Writer     (Writer, tell, runWriter)
+import Data.Monoid              (Monoid, mempty, mappend)
+import qualified DDC.Type.Env   as Env
+import Data.Typeable
+
+
+-------------------------------------------------------------------------------
+data Config
+        = Config
+        { configExpand  :: Bool }
+        deriving Show
+
+
+-- | Empty eta configuration with all flags set to False.
+configZero :: Config
+configZero
+        = Config
+        { configExpand  = False }
+
+
+-------------------------------------------------------------------------------
+data Info
+        = Info
+        { -- | Number of level-1 lambdas added.
+          infoExpandedXLAMs     :: Int 
+
+          -- | Number of level-0 lambdas added. 
+        , infoExpandedXLams     :: Int }
+        deriving Typeable
+
+
+instance Pretty Info where
+ ppr (Info ex1 ex0)
+  = text "Eta Transform"
+  <$> indent 4 (vcat
+      [ text "level-1 lambdas added:     " <> int ex1 
+      , text "level-0 lambdas added:     " <> int ex0 ])
+
+
+instance Monoid Info where
+ mempty  = Info 0 0
+ mappend (Info ex1  ex0)
+         (Info ex1' ex0')
+  = Info (ex1 + ex1') (ex0 + ex0')
+
+
+-- Module ---------------------------------------------------------------------
+-- | Eta-transform expressions in a module.
+etaModule
+        :: (Ord n, Show n, Pretty n, Show a)
+        => Config
+        -> Profile n
+        -> Module a n
+        -> TransformResult (Module a n)
+
+etaModule config profile mm
+ = let  cconfig = Check.configOfProfile profile
+        kenv'   = Env.union (profilePrimKinds profile) (moduleKindEnv mm)
+        tenv'   = Env.union (profilePrimTypes profile) (moduleTypeEnv mm)
+        
+        -- Run the eta transform.
+        (mm', info) 
+                = runWriter 
+                $ etaM config cconfig kenv' tenv' mm
+                    
+        -- Check if any actual work was performed
+        progress
+         = case info of
+                Info ex1 ex0
+                 -> ex1 + ex0 > 0
+
+   in   TransformResult
+         { result         = mm'
+         , resultAgain    = False
+         , resultProgress = progress
+         , resultInfo     = TransformInfo info }
+
+
+-- | Eta-transform an expression.
+etaX    :: (Ord n, Show n, Show a, Pretty n)
+        => Config               -- ^ Eta-transform config.
+        -> Profile n            -- ^ Language profile.
+        -> KindEnv n            -- ^ Kind environment.
+        -> TypeEnv n            -- ^ Type environment.
+        -> Exp a n              -- ^ Expression to transform.
+        -> TransformResult (Exp a n)
+
+etaX config profile kenv tenv xx
+ = let  cconfig = Check.configOfProfile profile
+        kenv'   = Env.union (profilePrimKinds profile) kenv
+        tenv'   = Env.union (profilePrimTypes profile) tenv
+
+        -- Run the eta transform.
+        (xx', info)     
+                = runWriter
+                $ etaM config cconfig kenv' tenv' xx
+
+        -- Check if any actual work was performed
+        progress
+         = case info of
+                Info ex1 ex0
+                 -> ex1 + ex0 > 0
+
+   in   TransformResult
+         { result         = xx'
+         , resultAgain    = False
+         , resultProgress = progress
+         , resultInfo     = TransformInfo info }
+
+
+-------------------------------------------------------------------------------
+class Eta (c :: * -> * -> *) where
+ etaM   :: (Ord n, Pretty n, Show n)
+        => Config               -- ^ Eta-transform config.
+        -> Check.Config n       -- ^ Type checker config.
+        -> KindEnv n            -- ^ Kind environment.
+        -> TypeEnv n            -- ^ Type environment.
+        -> c a n                -- ^ Do eta-expansion in this thing.
+        -> Writer Info (c a n)
+
+
+instance Eta Module where
+ etaM config cconfig kenv tenv mm
+  = do  let kenv'       = Env.union (moduleKindEnv mm) kenv
+        let tenv'       = Env.union (moduleTypeEnv mm) tenv
+        xx'             <- etaM config cconfig kenv' tenv' (moduleBody mm)
+        return  $ mm { moduleBody = xx' }
+
+
+instance Eta Exp where
+ etaM config cconfig kenv tenv xx
+  = let down = etaM config cconfig kenv tenv
+    in case xx of
+
+        XVar a _
+         | configExpand config
+         , Right tX     <- Check.typeOfExp cconfig kenv tenv xx
+         -> do  etaExpand a tX xx
+
+        XApp a _ _
+         |  configExpand config
+         ,  Right tX    <- Check.typeOfExp cconfig kenv tenv xx
+         -> do  
+                -- Decend into the arguments first.
+                --   We don't need to decend into the function part because
+                --   we're eta-expanding that here.
+                let (x : xs)    =  takeXAppsAsList xx
+                xs_eta          <- mapM down xs
+
+                -- Now eta expand the result.
+                etaExpand a tX $ xApps a x xs_eta
+
+        XLAM a b x
+         -> do  let kenv'       = Env.extend b kenv
+                x'              <- etaM config cconfig kenv' tenv x
+                return $ XLAM a b x'
+
+        XLam a b x
+         -> do  let tenv'       = Env.extend b tenv
+                x'              <- etaM config cconfig kenv tenv' x
+                return $ XLam a b x'
+
+        XLet a lts x2
+         -> do  lts'            <- down lts
+                let (bs1, bs0)  = bindsOfLets lts
+                let kenv'       = Env.extends bs1 kenv
+                let tenv'       = Env.extends bs0 tenv
+                x2'             <- etaM config cconfig kenv' tenv' x2
+                return $ XLet a lts' x2'
+
+        XCase a x alts
+         -> do  x'              <- down x
+                alts'           <- mapM (etaM config cconfig kenv tenv) alts
+                return $ XCase a x' alts'
+
+        XCast a cc x
+         -> do  x'              <- down x
+                return $ XCast a cc x'
+
+        _ -> return xx
+
+
+instance Eta Lets where
+ etaM config cconfig kenv tenv lts
+  = let down    = etaM config cconfig kenv tenv
+    in case lts of
+        LLet b x
+         -> do  x'      <- down x
+                return  $ LLet b x'
+
+        LRec bxs
+         -> do  let bs    = map fst bxs
+                let tenv' = Env.extends bs tenv
+                xs'       <- mapM (etaM config cconfig kenv tenv') 
+                          $  map snd bxs
+                return    $ LRec (zip bs xs')
+
+        LLetRegions{}   -> return lts
+        LWithRegion{}   -> return lts
+
+
+instance Eta Alt where
+ etaM config cconfig kenv tenv alt
+  = case alt of
+        AAlt p x        
+         -> do  let bs    = bindsOfPat p
+                let tenv' = Env.extends bs tenv
+                x'        <- etaM config cconfig kenv tenv' x
+                return  $ AAlt p x'
+
+
+-- Expand ---------------------------------------------------------------------
+-- | Eta expand an expression.
+etaExpand 
+        :: Ord n
+        => a                    -- ^ Annotation to use for new AST nodes.
+        -> Type n               -- ^ Type of the expression.
+        -> Exp a n              -- ^ Inner expression to wrap.
+        -> Writer Info (Exp a n)
+
+etaExpand a tX xx
+ = do   let btsMore     = expandableArgs tX
+        xx'             <- etaExpand' a 0 0 [] btsMore xx
+        return xx'
+
+
+-- | Decide what type arguments need to be eta-expanded.
+expandableArgs :: Type n -> [(Bool, Type n)]
+expandableArgs tt
+        | TForall b t'          <- tt
+        = (True, typeOfBind b)  : expandableArgs t'
+
+        | Just (t1, t2)         <- takeTFun tt
+        = (False, t1)           : expandableArgs t2
+
+        | otherwise
+        = []
+
+
+-- | Eta-expand an expression.
+etaExpand'
+        :: Ord n 
+        => a                -- ^ Annotation to use for the new AST nodes.
+        -> Int              -- ^ Number of level-1 lambdas we've added so far.
+        -> Int              -- ^ Number of level-0 lambdas we've added so far.
+        -> [Exp a n]        -- ^ Accumulate arguments we need to add to the
+                            --      inner expression.
+        -> [(Bool, Type n)] -- ^ Types of bindings we need to add, along with
+                            --   a flag to indicate level-1 or level-0 binder
+        -> Exp a n          -- ^ Inner expression that is being applied.
+        -> Writer Info (Exp a n)
+
+etaExpand' a levels1 levels0 args [] xx
+ = do   let xx' = liftT levels1 $ liftX levels0 xx
+        return  $ xApps a xx' args
+
+etaExpand' a levels1 levels0 args ((True, t) : ts) xx
+ = do   let depth1 = length $ filter ((== True) . fst) ts
+        xx'     <- etaExpand' a (levels1 + 1) levels0 
+                        (args ++ [XType (TVar (UIx depth1))]) 
+                        ts
+                        xx
+
+        tell mempty { infoExpandedXLAMs = 1 }
+        return  $ XLAM a (BAnon t) xx'
+
+etaExpand' a levels1 levels0 args ((False, t) : ts) xx
+ = do   let depth0 = length $ filter ((== False) . fst) ts
+        xx'     <- etaExpand' a 
+                        levels1 (levels0 + 1) 
+                        (args ++ [XVar a (UIx depth0)])
+                        ts
+                        xx
+
+        tell mempty { infoExpandedXLams = 1 }
+        return  $ XLam a (BAnon t) xx'
+
diff --git a/DDC/Core/Transform/Flatten.hs b/DDC/Core/Transform/Flatten.hs
--- a/DDC/Core/Transform/Flatten.hs
+++ b/DDC/Core/Transform/Flatten.hs
@@ -4,7 +4,7 @@
         (flatten)
 where
 import DDC.Core.Transform.LiftT
-import DDC.Core.Transform.TransformX
+import DDC.Core.Transform.TransformUpX
 import DDC.Core.Transform.AnonymizeX
 import DDC.Core.Transform.LiftX
 import DDC.Core.Exp
@@ -43,21 +43,21 @@
 --      x1
 -- @
 -- 
-flatten1 (XLet a1 (LLet LetStrict b1
-            inner@(XLet a2 (LLet LetStrict b2 def2) x2))
+flatten1 (XLet a1 (LLet b1
+            inner@(XLet a2 (LLet b2 def2) x2))
                x1)
 
  | isBName b2
  = flatten1
-        $ XLet a1 (LLet LetStrict b1 
+        $ XLet a1 (LLet b1 
                (anonymizeX inner))
                x1
 
  | otherwise
  = let  x1'       = liftAcrossX [b1] [b2] x1                                 
-   in   XLet a2 (LLet LetStrict b2 def2) 
+   in   XLet a2 (LLet b2 def2) 
       $ flatten1
-      $ XLet a1 (LLet LetStrict b1 x2) 
+      $ XLet a1 (LLet b1 x2) 
              x1'
 
 
@@ -74,12 +74,12 @@
 -- NOTE: For region allocation this increases the lifetime of the region.
 --       Maybe use a follow on transform to reduce the lifetime again.
 --
-flatten1 (XLet a1 (LLet LetStrict b1
+flatten1 (XLet a1 (LLet b1
             inner@(XLet a2 (LLetRegions b2 bs2) x2))
                x1)
  | all isBName b2
  = flatten1
-        $ XLet a1 (LLet LetStrict b1
+        $ XLet a1 (LLet b1
                   (anonymizeX inner))
                x1
 
@@ -88,7 +88,7 @@
                 $ liftAcrossX [b1] bs2 x1
    in   XLet a2 (LLetRegions b2 bs2) 
       $ flatten1
-      $ XLet a1 (LLet LetStrict (zapX b1) x2) 
+      $ XLet a1 (LLet (zapX b1) x2) 
              x1'
 
 
@@ -105,12 +105,12 @@
 --
 -- * binding must be strict because we force evaluation of x1.
 --
-flatten1 (XLet  a1 (LLet LetStrict b1 
+flatten1 (XLet  a1 (LLet b1 
              inner@(XCase a2 x1 [AAlt p x2]))
                    x3)
  | any isBName $ bindsOfPat p
  = flatten1
-        $ XLet  a1 (LLet LetStrict b1
+        $ XLet  a1 (LLet b1
                    (anonymizeX inner))
                    x3
 
@@ -118,7 +118,7 @@
  = let  x3'     = liftAcrossX [b1] (bindsOfPat p) x3
    in   XCase a2 x1 
            [AAlt p ( flatten1 
-                   $ XLet a1 (LLet LetStrict b1 x2)
+                   $ XLet a1 (LLet b1 x2)
                              (anonymizeX x3'))]
 
 
diff --git a/DDC/Core/Transform/Forward.hs b/DDC/Core/Transform/Forward.hs
--- a/DDC/Core/Transform/Forward.hs
+++ b/DDC/Core/Transform/Forward.hs
@@ -2,6 +2,8 @@
 -- | Float let-bindings with a single use forward into their use-sites.
 module DDC.Core.Transform.Forward
         ( ForwardInfo   (..)
+        , FloatControl  (..)
+        , Config(..)
         , forwardModule
         , forwardX)
 where
@@ -10,8 +12,10 @@
 import DDC.Core.Exp
 import DDC.Core.Module
 import DDC.Core.Simplifier.Base
+import DDC.Core.Transform.Reannotate
 import DDC.Core.Fragment
 import DDC.Core.Predicates
+import DDC.Core.Compounds
 import Data.Map                 (Map)
 import Control.Monad
 import Control.Monad.Writer	(Writer, runWriter, tell)
@@ -24,52 +28,86 @@
 -- | Summary of number of bindings floated.
 data ForwardInfo
         = ForwardInfo
-        { -- | Number of trivial @v1 = v2@ bindings inlined.
-          infoSubsts   :: Int
+        { -- | Number of bindings inspected.
+          infoInspected :: !Int
 
+          -- | Number of trivial @v1 = v2@ bindings inlined.
+        , infoSubsts    :: !Int
+
           -- | Number of bindings floated forwards.
-        , infoBindings :: Int }
+        , infoBindings  :: !Int }
         deriving Typeable
 
 
 instance Pretty ForwardInfo where
- ppr (ForwardInfo substs bindings)
+ ppr (ForwardInfo inspected substs bindings)
   =  text "Forward:"
   <$> indent 4 (vcat
-      [ text "Substitutions:  " <> int substs
-      , text "Bindings:       " <> int bindings ])
+      [ text "Total bindings inspected:      " <> int inspected
+      , text "  Trivial substitutions made:  " <> int substs
+      , text "  Bindings moved forward:      " <> int bindings ])
 
 
 instance Monoid ForwardInfo where
- mempty = ForwardInfo 0 0
- mappend (ForwardInfo s1 b1)(ForwardInfo s2 b2)
-        = ForwardInfo (s1 + s2) (b1 + b2)
+ mempty = ForwardInfo 0 0 0
+ mappend (ForwardInfo i1 s1 b1)(ForwardInfo i2 s2 b2)
+        = ForwardInfo (i1 + i2) (s1 + s2) (b1 + b2)
 
 
 -------------------------------------------------------------------------------
+-- | Fine control over what should be floated.
+data FloatControl
+        = FloatAllow    -- ^ Allow binding to be floated, but don't require it.
+        | FloatDeny     -- ^ Prevent a binding being floated, at all times.
+        | FloatForce    -- ^ Force   a binding to be floated, at all times.
+        deriving (Eq, Show)
+
+data Config a n
+        = Config
+        { configFloatControl    :: Lets a n -> FloatControl
+        , configFloatLetBody    :: Bool }
+
+-------------------------------------------------------------------------------
 -- | Float let-bindings in a module with a single use forward into
 --   their use sites.
 forwardModule 
         :: Ord n
-        => Profile n -> Module a n -> Module a n
+        => Profile n    -- ^ Language profile
+        -> Config a n
+        -> Module a n 
+        -> TransformResult (Module a n)
 
-forwardModule profile mm
-        = fst   $ runWriter
-                $ forwardWith profile Map.empty 
+forwardModule profile config mm
+ = let  (mm', info)
+         = runWriter
+                $ forwardWith profile config Map.empty 
                 $ usageModule mm
 
+        progress (ForwardInfo _ s f)
+                = s + f > 0
 
+   in   TransformResult
+         { result         = mm'
+         , resultProgress = progress info
+         , resultAgain    = False
+         , resultInfo     = TransformInfo info }
+
+
 -- | Float let-bindings in an expression with a single use forward into
 --   their use-sites.
 forwardX :: Ord n
-         => Profile n -> Exp a n -> TransformResult (Exp a n)
-forwardX profile xx
+         => Profile n   -- ^ Language profile.
+         -> Config a n 
+         -> Exp a n                      
+         -> TransformResult (Exp a n)
+
+forwardX profile config xx
  = let  (x',info) = runWriter
-		  $ forwardWith profile Map.empty
+		  $ forwardWith profile config Map.empty
 		  $ usageX xx
 
-        progress (ForwardInfo s _) 
-                = s > 0
+        progress (ForwardInfo _ s f) 
+                = s + f > 0
 
    in  TransformResult
         { result	 = x'
@@ -83,13 +121,14 @@
  -- | Carry bindings forward and downward into their use-sites.
  forwardWith 
         :: Ord n
-        => Profile n
-        -> Map n (Exp a n)
+        => Profile n            -- ^ Language profile.
+        -> Config a n
+        -> Map n (Exp a n)      -- ^ Bindings currently being carried forward.
         -> c (UsedMap n, a) n
         -> Writer ForwardInfo (c a n)
 
 instance Forward Module where
- forwardWith profile bindings 
+ forwardWith profile config bindings 
         (ModuleCore
                 { moduleName            = name
                 , moduleExportKinds     = exportKinds
@@ -98,7 +137,7 @@
                 , moduleImportTypes     = importTypes
                 , moduleBody            = body })
 
-  = do	body' <- forwardWith profile bindings body
+  = do	body' <- forwardWith profile config bindings body
 	return ModuleCore
 		{ moduleName            = name
 		, moduleExportKinds     = exportKinds
@@ -109,9 +148,9 @@
 
 
 instance Forward Exp where
- forwardWith profile bindings xx
+ forwardWith profile config bindings xx
   = {-# SCC forwardWith #-}
-    let down    = forwardWith profile bindings 
+    let down    = forwardWith profile config bindings 
     in case xx of
         XVar a u@(UName n)
          -> case Map.lookup n bindings of
@@ -127,33 +166,64 @@
         XLam a b x      -> liftM    (XLam (snd a) b) (down x)
         XApp a x1 x2    -> liftM2   (XApp (snd a))   (down x1) (down x2)
 
-        XLet (UsedMap um, _) (LLet _mode (BName n _) x1) x2
-         | isXLam x1 || isXLAM x1
-         , Just usage     <- Map.lookup n um
-         , [UsedFunction] <- filterUsedInCasts usage
-	 -> do
-                -- Record that we've moved this binding.
-                tell mempty { infoBindings = 1 }
-                x1'           <- down x1
-                forwardWith profile (Map.insert n x1' bindings) x2
+        -- Always float last let-binding into its use.
+        --   let x = exp in x => exp
+        XLet _ (LLet b x1) (XVar _ u)
+         |  boundMatchesBind u b
+         ,  configFloatLetBody config
+         -> down x1
 
-	-- Always float atomic bindings (variables, constructors)
-        XLet _ (LLet _mode b x1) x2
-	 | isAtomX x1
-	 -> do 
+        -- Always float atomic bindings (variables, constructors)
+        XLet _ (LLet b x1) x2
+         | isAtomX x1
+         -> do 
                 -- Record that we've moved this binding.
-                tell mempty { infoBindings = 1 }
+                tell mempty { infoInspected = 1
+                            , infoBindings  = 1 }
 
                 -- Slow, but handles anonymous binders and shadowing
                 down $ S.substituteXX b x1 x2
 
+        XLet (UsedMap um, a') lts@(LLet (BName n _) x1) x2
+         -> do  
+                let control    = configFloatControl config 
+                               $ reannotate snd lts
+
+                let isFun      = isXLam x1 || isXLAM x1
+
+                let isApplied
+                     | Just usage       <- Map.lookup n um
+                     , [UsedFunction]   <- filterUsedInCasts usage
+                                        = True
+                     | otherwise        = False
+
+                let shouldFloat
+                     = case control of
+                        FloatDeny       -> False
+                        FloatForce      -> True
+                        FloatAllow      -> isFun && isApplied
+
+                if shouldFloat 
+                 then do
+                        -- Record that we've moved this binding.
+                        tell mempty { infoInspected = 1
+                                    , infoBindings  = 1 }
+
+                        x1'             <- down x1
+                        let bindings'   = Map.insert n x1' bindings
+                        forwardWith profile config bindings' x2
+
+                 else do        
+                        tell mempty { infoInspected = 1}
+                        liftM2 (XLet a') (down lts) (down x2)
+
         XLet (_, a') lts x     
-         -> liftM2 (XLet a') (down lts) (down x)
+         ->     liftM2 (XLet a') (down lts) (down x)
 
         XCase a x alts  -> liftM2   (XCase (snd a)) (down x) (mapM down alts)
         XCast a c x     -> liftM2   (XCast (snd a)) (down c) (down x)
         XType t         -> return $ XType t
-        XWitness w      -> return $ XWitness w
+        XWitness w      -> return $ XWitness (reannotate snd w)
 
 
 filterUsedInCasts :: [Used] -> [Used]
@@ -163,20 +233,23 @@
 
 
 instance Forward Cast where
- forwardWith profile bindings xx
-  = let down    = forwardWith profile bindings
+ forwardWith profile config bindings xx
+  = let down    = forwardWith profile config bindings
     in case xx of
         CastWeakenEffect eff    -> return $ CastWeakenEffect eff
         CastWeakenClosure xs    -> liftM    CastWeakenClosure (mapM down xs)
-        CastPurify w            -> return $ CastPurify w
-        CastForget w            -> return $ CastForget w
+        CastPurify w            -> return $ CastPurify (reannotate snd w)
+        CastForget w            -> return $ CastForget (reannotate snd w)
+        CastSuspend             -> return $ CastSuspend
+        CastRun                 -> return $ CastRun
 
 
 instance Forward Lets where
- forwardWith profile bindings lts
-  = let down    = forwardWith profile bindings
+ forwardWith profile config bindings lts
+  = let down    = forwardWith profile config bindings
     in case lts of
-        LLet mode b x   -> liftM (LLet mode b) (down x)
+        LLet b x   
+         -> liftM (LLet b) (down x)
 
         LRec bxs        
          -> liftM LRec
@@ -190,6 +263,6 @@
 
 
 instance Forward Alt where
- forwardWith profile bindings (AAlt p x)
-  = liftM (AAlt p) (forwardWith profile bindings x)
+ forwardWith profile config bindings (AAlt p x)
+  = liftM (AAlt p) (forwardWith profile config bindings x)
 
diff --git a/DDC/Core/Transform/Inline.hs b/DDC/Core/Transform/Inline.hs
--- a/DDC/Core/Transform/Inline.hs
+++ b/DDC/Core/Transform/Inline.hs
@@ -62,7 +62,7 @@
                 _               -> inline get inside x
 
     in case lts of
-        LLet mode b x   -> LLet mode b (enter b x)
+        LLet b x        -> LLet b (enter b x)
         LRec bxs        -> LRec [(b, enter b x) | (b, x) <- bxs]
         LLetRegions{}   -> lts
         LWithRegion{}   -> lts
diff --git a/DDC/Core/Transform/Namify.hs b/DDC/Core/Transform/Namify.hs
--- a/DDC/Core/Transform/Namify.hs
+++ b/DDC/Core/Transform/Namify.hs
@@ -98,23 +98,15 @@
         return  $ mm { moduleBody = body' }
 
 
-instance Namify LetMode where
- namify tnam xnam mm
-  = case mm of
-        LetStrict               -> return mm
-        LetLazy Nothing         -> return mm
-        LetLazy (Just w)        -> liftM (LetLazy . Just) $ namify tnam xnam w
-
-
-instance Namify Witness where
+instance Namify (Witness a) where
  namify tnam xnam ww
   = let down = namify tnam xnam
     in case ww of
-        WVar u          -> liftM  WVar  (rewriteX tnam xnam u)
+        WVar  a u       -> liftM  (WVar  a) (rewriteX tnam xnam u)
         WCon{}          -> return ww
-        WApp  w1 w2     -> liftM2 WApp  (down w1) (down w2)
-        WJoin w1 w2     -> liftM2 WJoin (down w1) (down w2)
-        WType t         -> liftM  WType (down t)
+        WApp  a w1 w2   -> liftM2 (WApp  a) (down w1) (down w2)
+        WJoin a w1 w2   -> liftM2 (WJoin a) (down w1) (down w2)
+        WType a t       -> liftM  (WType a) (down t)
 
 
 instance Namify (Exp a) where
@@ -138,12 +130,11 @@
         XApp  a x1 x2   
          ->     liftM3 XApp     (return a) (down x1)  (down x2)
 
-        XLet  a (LLet mode b x1) x2
-         -> do  mode'           <- down mode
-                x1'             <- namify tnam xnam x1
+        XLet  a (LLet b x1) x2
+         -> do  x1'             <- namify tnam xnam x1
                 (xnam', b')     <- pushX  tnam xnam b
                 x2'             <- namify tnam xnam' x2
-                return $ XLet a (LLet mode' b' x1') x2'
+                return $ XLet a (LLet b' x1') x2'
 
         XLet a (LRec bxs) x2
          -> do  let (bs, xs)    = unzip bxs
@@ -183,18 +174,16 @@
  namify tnam xnam cc
   = let down = namify tnam xnam
     in case cc of
-        CastWeakenEffect  eff
-         -> liftM CastWeakenEffect  (down eff)
+        CastWeakenEffect  eff   -> liftM CastWeakenEffect  (down eff)
 
         CastWeakenClosure xs    
          -> do  xs' <- mapM down xs
                 return $ CastWeakenClosure xs'
 
-        CastPurify w
-         -> liftM CastPurify (down w)
-
-        CastForget w
-         -> liftM CastForget (down w)
+        CastPurify w            -> liftM CastPurify (down w)
+        CastForget w            -> liftM CastForget (down w)
+        CastSuspend             -> return CastSuspend
+        CastRun                 -> return CastRun
 
 
 -- | Rewrite level-1 anonymous binders.
diff --git a/DDC/Core/Transform/Prune.hs b/DDC/Core/Transform/Prune.hs
--- a/DDC/Core/Transform/Prune.hs
+++ b/DDC/Core/Transform/Prune.hs
@@ -13,7 +13,7 @@
 import DDC.Core.Analysis.Usage
 import DDC.Core.Simplifier.Base
 import DDC.Core.Transform.Reannotate
-import DDC.Core.Transform.TransformX
+import DDC.Core.Transform.TransformUpX
 import DDC.Core.Fragment
 import DDC.Core.Check
 import DDC.Core.Module
@@ -69,8 +69,8 @@
          -- If the language fragment has untracked effects then we can't do
          -- the prune transform because we risk dropping statements with global
          -- effects.
-         | featuresUntrackedEffects 
-                $ profileFeatures profile
+         | not $ featuresTrackedEffects
+               $ profileFeatures profile
          = mm
 
          | otherwise
@@ -144,7 +144,7 @@
 
 pruneTrans _ _ xx
  = case xx of
-        XLet a@(usedMap, antec) (LLet _mode b x1) x2
+        XLet a@(usedMap, antec) (LLet b x1) x2
          | isUnusedBind b usedMap
          , isContainedEffect $ annotEffect antec
          -> do      
diff --git a/DDC/Core/Transform/Rewrite.hs b/DDC/Core/Transform/Rewrite.hs
--- a/DDC/Core/Transform/Rewrite.hs
+++ b/DDC/Core/Transform/Rewrite.hs
@@ -171,9 +171,9 @@
          =      rewrites env x args
 
 
-        goLets (LLet lm b e) ws 
+        goLets (LLet b e) ws 
          = do   e' <- down ws e 
-                return $ LLet lm b e'
+                return $ LLet b e'
 
         goLets (LRec bs) ws 
          = do   bs'     <- mapM (down ws) $ map snd bs
@@ -202,7 +202,7 @@
 --       x = box ^0
 --   in ...
 --
-goDefHoles rules a l@(LLet LetStrict let_bind def) e env down
+goDefHoles rules a l@(LLet let_bind def) e env down
  | (((sub, []), name, RewriteRule { ruleBinds = bs, ruleLeft = hole }):_)
         <- checkHoles rules def env
 
@@ -233,13 +233,13 @@
 
         -- replace 'def' with LHS-HOLE[sub => ^n]
         anons   = zipWith (\(b,_) i -> (b, XVar a (UIx i))) bas' [0..]
-        lets    = map (\(b,v) -> LLet LetStrict b v) values
+        lets    = map (\(b,v) -> LLet b v) values
 
         def'    = S.substituteXArgs basK
                 $ S.substituteXArgs anons hole
 
         let_bind'  = S.substituteTs basK' let_bind
-        lets'      = lets ++ [LLet LetStrict let_bind' def']
+        lets'      = lets ++ [LLet let_bind' def']
 
         -- lift e by (length bas)
         depth   = case let_bind of
@@ -402,7 +402,7 @@
         anons   = zipWith (\(b,_) i -> (b, XVar a (UIx i))) as' [0..]
         values  = map     (\(b,v) ->   (BAnon (substT bs' $ T.typeOfBind b), v)) 
                           (reverse as')
-        lets    = map (\(b,v) -> LLet LetStrict b v) values
+        lets    = map (\(b,v) -> LLet b v) values
 
    in   (bs' ++ anons, lets)
 
diff --git a/DDC/Core/Transform/Rewrite/Env.hs b/DDC/Core/Transform/Rewrite/Env.hs
--- a/DDC/Core/Transform/Rewrite/Env.hs
+++ b/DDC/Core/Transform/Rewrite/Env.hs
@@ -93,7 +93,7 @@
         extend' b (r:rs') = (b:r) : rs'
         extend' b []	   = [[b]]
 
-extendLets (LLet _ b def) env
+extendLets (LLet b def) env
  = insertDef b (Just def') (liftValue b env)
  where  def' = case b of
 	         BAnon{} -> L.liftX 1 def
diff --git a/DDC/Core/Transform/Rewrite/Match.hs b/DDC/Core/Transform/Rewrite/Match.hs
--- a/DDC/Core/Transform/Rewrite/Match.hs
+++ b/DDC/Core/Transform/Rewrite/Match.hs
@@ -80,7 +80,8 @@
 	match m' bs x12 x22
 
 match m bs (XCast _ c1 x1) (XCast _ c2 x2)
- | eqCast c1 c2	= match m bs x1 x2
+ | eqCast c1 c2	
+ = match m bs x1 x2
 
 match (xs, tys) bs (XType t1) (XType t2)
  = do	tys' <- matchT t1 t2 bs tys
@@ -93,20 +94,25 @@
  = Nothing
 
 
+eqCast :: Ord n => Cast a n -> Cast a n -> Bool
 eqCast lc rc 
  = clean lc == clean rc
  where  clean c 
-         = case c of
-                CastWeakenEffect  eff -> CastWeakenEffect  $ T.anonymizeT eff
-                CastWeakenClosure clo -> CastWeakenClosure $ map cleanX clo
-                CastPurify        wit -> CastPurify wit
-                CastForget        wit -> CastForget wit
+         = T.reannotate (const ())
+         $ case c of
+                CastWeakenEffect  eff   -> CastWeakenEffect  $ T.anonymizeT eff
+                CastWeakenClosure clo   -> CastWeakenClosure $ map T.anonymizeX clo
+                CastPurify        wit   -> CastPurify        wit
+                CastForget        wit   -> CastForget wit
+                CastSuspend             -> CastSuspend
+                CastRun                 -> CastRun
 
-        cleanX 
-         = T.anonymizeX . T.reannotate (const ())
 
+eqWit  :: Ord n => Witness a n -> Witness a n -> Bool
 eqWit lw rw 
-        = lw == rw
+        =  T.reannotate (const ()) lw 
+        == T.reannotate (const ()) rw
+
 
 -- Types ----------------------------------------------------------------------
 type VarSet n = Set.Set n
diff --git a/DDC/Core/Transform/Rewrite/Parser.hs b/DDC/Core/Transform/Rewrite/Parser.hs
--- a/DDC/Core/Transform/Rewrite/Parser.hs
+++ b/DDC/Core/Transform/Rewrite/Parser.hs
@@ -19,13 +19,14 @@
 	x
 -}
 -- | Parse a rewrite rule.
-pRule	:: Ord n => Parser n (R.RewriteRule () n)
-pRule
- = do	bs	 <- pRuleBinders
-	(cs,lhs) <- pRuleCsLhs
-	hole	 <- pRuleHole
+pRule	:: Ord n 
+        => Context -> Parser n (R.RewriteRule P.SourcePos n)
+pRule c
+ = do	bs	 <- pRuleBinders c
+	(cs,lhs) <- pRuleCsLhs c
+	hole	 <- pRuleHole c
 	pTok KEquals
-	rhs	 <- pExp
+	rhs	 <- pExp c
 
 	return $ R.mkRewriteRule bs cs lhs hole rhs
 
@@ -41,44 +42,53 @@
         ;
 -}
 -- | Parse many rewrite rules.
-pRuleMany	:: Ord n => Parser n [(n,R.RewriteRule () n)]
-pRuleMany
+pRuleMany	
+        :: Ord n 
+        => Context -> Parser n [(n,R.RewriteRule P.SourcePos n)]
+pRuleMany c
  = P.many (do
         n <- pName
-        r <- pRule
+        r <- pRule c
         pTok KSemiColon
         return (n,r))
 
 
-pRuleBinders :: Ord n => Parser n [(R.BindMode,Bind n)]
-pRuleBinders
+pRuleBinders 
+        :: Ord n 
+        => Context -> Parser n [(R.BindMode,Bind n)]
+
+pRuleBinders c
  = P.choice
- [ do	bs <- P.many1 pBinders
+ [ do	bs <- P.many1 (pBinders c)
 	pTok KDot
 	return $ concat bs
  , return []
  ]
 
 
-pRuleCsLhs :: Ord n => Parser n ([Type n], Exp () n)
-pRuleCsLhs
+pRuleCsLhs 
+        :: Ord n 
+        => Context -> Parser n ([Type n], Exp P.SourcePos n)
+pRuleCsLhs c
  = P.choice
  [ do	cs <- P.many1 $ P.try (do
-		c <- pTypeApp
+		cc <- pTypeApp c
 		pTok KArrowEquals
-		return c)
-	lhs <- pExp
+		return cc)
+	lhs <- pExp c
 	return (cs,lhs)
- , do	lhs <- pExp
+ , do	lhs <- pExp c
 	return ([],lhs)
  ]
 
 
-pRuleHole :: Ord n => Parser n (Maybe (Exp () n))
-pRuleHole
+pRuleHole 
+        :: Ord n 
+        => Context -> Parser n (Maybe (Exp P.SourcePos n))
+pRuleHole c
  = P.optionMaybe
  $ do	pTok KBraceBra
-	e <- pExp
+	e <- pExp c
 	pTok KBraceKet
 	return e
 
@@ -89,26 +99,29 @@
 --       [BIND1 BIND2 .. BINDN : TYPE]
 --   or  (BIND : TYPE)
 --
-pBinders :: Ord n => Parser n [(R.BindMode, Bind n)]
-pBinders
+pBinders 
+        :: Ord n 
+        => Context -> Parser n [(R.BindMode, Bind n)]
+pBinders c
  = P.choice
- [ pBindersBetween R.BMSpec      (pTok KSquareBra) (pTok KSquareKet)
- , pBindersBetween (R.BMValue 0) (pTok KRoundBra)  (pTok KRoundKet)
+ [ pBindersBetween c R.BMSpec      (pTok KSquareBra) (pTok KSquareKet)
+ , pBindersBetween c (R.BMValue 0) (pTok KRoundBra)  (pTok KRoundKet)
  ]
 
 
 pBindersBetween 
         :: Ord n 
-        => R.BindMode 
+        => Context
+        -> R.BindMode 
         -> Parser n () 
         -> Parser n () 
         -> Parser n [(R.BindMode,Bind n)]
 
-pBindersBetween bm bra ket
+pBindersBetween c bm bra ket
  = do	bra
         bs      <- P.many1 pBinder
         pTok KColon
-        t       <- pType
+        t       <- pType c
         ket
         return $ map (mk t) bs
  where mk t b = (bm,T.makeBindFromBinder b t)
diff --git a/DDC/Core/Transform/Rewrite/Rule.hs b/DDC/Core/Transform/Rewrite/Rule.hs
--- a/DDC/Core/Transform/Rewrite/Rule.hs
+++ b/DDC/Core/Transform/Rewrite/Rule.hs
@@ -16,7 +16,7 @@
 where
 import DDC.Core.Transform.Rewrite.Error
 import DDC.Core.Transform.Reannotate
-import DDC.Core.Transform.TransformX
+import DDC.Core.Transform.TransformUpX
 import DDC.Core.Exp
 import DDC.Core.Pretty                          ()
 import DDC.Core.Collect
@@ -305,8 +305,8 @@
         -> Type n       -- ^ The constraint type to check.
         -> Either (Error a n) (Kind n)
 
-checkConstraint defs kenv tt
- = case T.checkType (C.configPrimDataDefs defs) kenv tt of
+checkConstraint config kenv tt
+ = case T.checkType config kenv tt of
         Left _err               -> Left $ ErrorBadConstraint tt
         Right k
          | T.isWitnessType tt   -> return k
@@ -392,7 +392,7 @@
          $  [XVar a u 
                 | u <- Set.toList $ daLeft `Set.difference` daRight ]
 
-         ++ [XWitness (WVar u)
+         ++ [XWitness (WVar a u)
                 | u <- Set.toList $ wiLeft `Set.difference` wiRight ]
 
          ++ [XType (TVar u)
@@ -414,8 +414,7 @@
   remove kenv _tenv x
 
    | XType et   <- x
-   , Right k    <- T.checkType (C.configPrimDataDefs config)
-                               kenv et
+   , Right k    <- T.checkType config kenv et
    , T.isEffectKind k
    = XType $ T.tBot T.kEffect
 
diff --git a/DDC/Core/Transform/Snip.hs b/DDC/Core/Transform/Snip.hs
--- a/DDC/Core/Transform/Snip.hs
+++ b/DDC/Core/Transform/Snip.hs
@@ -1,16 +1,41 @@
 
 -- | Snip out nested applications.
 module DDC.Core.Transform.Snip
-        (Snip(..))
+        ( Snip   (..)
+        , Config (..)
+        , configZero)
 where
 import DDC.Core.Analysis.Arity
 import DDC.Core.Module
 import DDC.Core.Exp
 import DDC.Core.Compounds
+import DDC.Core.Predicates
 import qualified DDC.Core.Transform.LiftX       as L
 import qualified DDC.Type.Compounds             as T
 
 
+-------------------------------------------------------------------------------
+-- | Snipper configuration.
+data Config 
+        = Config
+        { -- | Introduce new bindings for over-applied functions.
+          configSnipOverApplied :: Bool
+        
+          -- | Ensure the body of a let-expression is a variable.
+        , configSnipLetBody     :: Bool
+        }
+
+
+-- | Snipper configuration with all flags set to False.
+configZero :: Config
+configZero
+        = Config
+        { configSnipOverApplied = False
+        , configSnipLetBody     = False }
+
+
+-------------------------------------------------------------------------------
+-- | Class of things that can have things snipped out of them.
 class Snip (c :: * -> *) where
 
  -- | Snip out nested applications as anonymous bindings.
@@ -19,54 +44,50 @@
  --      f (g x) (h y)
  --  ==> let ^ = g x in ^ = h y in f ^1 ^0
  -- @
- snip   :: Ord n 
-        => Bool         -- ^ Introduce extra bindings for over-applied functions.
-        -> c n 
-        -> c n
+ snip   :: Ord n => Config -> c n -> c n
 
 
 instance Snip (Module a) where
- snip bOver mm
-  = {-# SCC "snip[Module]" #-}
-    let arities = aritiesOfModule mm
-        body'   = snipX bOver arities (moduleBody mm) []
+ snip config mm
+  = let arities = aritiesOfModule mm
+        body'   = snipX config arities (moduleBody mm) []
     in  mm { moduleBody = body'  }
 
 
 instance Snip (Exp a) where
- snip bOver x 
-  = {-# SCC "snip[Exp]" #-}
-    snipX bOver emptyArities x []
+ snip config x 
+  = snipX config emptyArities x []
 
 
 -- | Convert an expression into A-normal form.
-snipX 
-        :: Ord n
-        => Bool           -- ^ Introduce extra bindings for over-applied functions.
+snipX   :: Ord n
+        => Config
         -> Arities n      -- ^ Arities of functions in environment.
         -> Exp a n        -- ^ Expression to transform.
         -> [(Exp a n, a)] -- ^ Arguments being applied to current expression.
         -> Exp a n
 
-snipX bOver arities x args
+snipX config arities x args
         -- For applications, remember the argument that the function is being 
         --   applied to, and decend into the function part.
         --   This unzips application nodes as we decend into the tree.
         | XApp a fun arg        <- x
-        = snipX bOver arities fun $ (snipX bOver arities arg [], a) : args
+        = snipX  config arities fun 
+                $ (snipX config arities arg [], a) : args
 
         -- Some non-application node with no arguments.
         | null args
-        = enterX bOver arities x
+        = enterX config arities x
 
         -- Some non-application node being applied to arguments.
         | otherwise
-        = buildNormalisedApp bOver arities (enterX bOver arities x) args
+        = let   x'      = enterX config arities x
+          in    buildNormalisedApp config arities x' args
 
 -- Enter into a non-application.
-enterX bOver arities xx
+enterX config arities xx
  = let  down ars e 
-         = snipX bOver (extendsArities arities ars) e []
+         = snipX config (extendsArities arities ars) e []
 
    in case xx of
         -- The snipX function shouldn't have called us with an XApp.
@@ -87,10 +108,11 @@
          -> XLam a b (down [(b,0)] e)
 
         -- non-recursive let
-        XLet a (LLet m b x1) x2
-         -> let x1' = down [] x1
-                x2' = down [(b, arityOfExp' x1')] x2
-            in  XLet a (LLet m b x1') x2'
+        XLet a (LLet b x1) x2
+         -> let x1'     = down [] x1
+                x2'     = snipLetBody config a
+                        $ down [(b, arityOfExp' x1')] x2
+            in  XLet a (LLet b x1') x2'
 
         -- recursive let
         XLet a (LRec lets) x2
@@ -98,17 +120,19 @@
                 xs      = map snd lets 
                 ars     = zip bs (map arityOfExp' xs) 
                 xs'     = map (down ars) xs
-                x2'     = down ars x2
+                x2'     = snipLetBody config a $ down ars x2
             in  XLet a (LRec $ zip bs xs') x2' 
 
         -- letregion, just make sure we record bindings with dummy val.
         XLet a (LLetRegions b bs) x2
-         -> let ars = zip bs (repeat 0) 
-            in  XLet a (LLetRegions b bs) (down ars x2)
+         -> let ars     = zip bs (repeat 0)
+                x2'     = snipLetBody config a $ down ars x2
+            in  XLet a (LLetRegions b bs) x2'
 
         -- withregion
-        XLet a (LWithRegion b) z2
-         -> XLet a (LWithRegion b) (down [] z2)
+        XLet a (LWithRegion b) x2
+         -> let x2'     = snipLetBody config a $ down [] x2
+            in  XLet a (LWithRegion b) x2'
 
         -- case
         -- Split out non-atomic discriminants into their own bindings.
@@ -121,11 +145,14 @@
 
          | otherwise
          -> let e'      = down [] e
-                alts'   = [AAlt pat (down (aritiesOfPat pat) ae) | AAlt pat ae <- alts]
+                alts'   = [AAlt pat (down (aritiesOfPat pat) ae) 
+                                | AAlt pat ae <- alts]
+                xBody'  = snipLetBody config a
+                        $ XCase a (XVar a $ UIx 0)
+                                  (map (L.liftX 1) alts')
 
-            in   XLet a (LLet LetStrict (BAnon (T.tBot T.kData)) e')
-                        (XCase a (XVar a $ UIx 0) 
-                                 (map (L.liftX 1) alts'))
+            in  XLet a (LLet (BAnon (T.tBot T.kData)) e')
+                       xBody'
 
         -- cast
         XCast a c e
@@ -134,18 +161,18 @@
 
 -- | Build an A-normalised application of some functional expression to 
 --   its arguments. Atomic arguments are applied directly, while 
---   on-atomic arguments are bound via let-expressions, then the
+--   non-atomic arguments are bound via let-expressions, then the
 --   associated let-bound variable is passed to the function.
 buildNormalisedApp 
         :: Ord n
-        => Bool            -- ^ Introduce extra bindings for over-applied functions.
+        => Config          -- ^ Snipper config.
         -> Arities n	   -- ^ environment, arities of bound variables
         -> Exp a n	   -- ^ function
         -> [(Exp a n,a)]   -- ^ arguments being applied to current expression
         -> Exp a n
 
-buildNormalisedApp _bOver _  f0 [] = f0
-buildNormalisedApp bOver arities f0 args@( (_, annot) : _)
+buildNormalisedApp _ _  f0 [] = f0
+buildNormalisedApp config arities f0 args@( (_, annot) : _)
  = make annot f0 args
  where
         tBot' = T.tBot T.kData
@@ -164,13 +191,14 @@
 
          -- The function part is already atomic.
          | isAtom xFun
-         = buildNormalisedFunApp bOver a f0Arity xFun xsArgs
+         = buildNormalisedFunApp config a f0Arity xFun xsArgs
 
          -- The function part is not atomic, 
          --  so we need to add an outer-most let-binding for it.
          | otherwise
-         = XLet a (LLet LetStrict (BAnon tBot') xFun)
-                  (buildNormalisedFunApp bOver a f0Arity 
+         = XLet a (LLet (BAnon tBot') xFun)
+                  (snipLetBody config a
+                    $ buildNormalisedFunApp config a f0Arity 
                                (XVar a (UIx 0)) 
                                [ (L.liftX 1 x, a') | (x, a') <- xsArgs])
 
@@ -184,14 +212,14 @@
 --   wants the function part to be normalised as well.
 buildNormalisedFunApp
         :: Ord n
-        => Bool           -- ^ Introduce extra bindings for over-applied functions.
+        => Config         -- ^ Snipper configuration.
         -> a              -- ^ Annotation to use.
         -> Int            -- ^ Arity of the function part.
         -> Exp a n        -- ^ Function part.
         -> [(Exp a n, a)] -- ^ Arguments to apply
         -> Exp a n
 
-buildNormalisedFunApp bOver an funArity xFun xsArgs
+buildNormalisedFunApp config an funArity xFun xsArgs
  = let  tBot' = T.tBot T.kData
 
         -- Split arguments into the already atomic ones,
@@ -228,12 +256,13 @@
          -- If the function is over-applied then create an intermediate
          -- binding that saturates it, then apply the extra arguments
          -- separately.
-         | bOver
+         | configSnipOverApplied config
          , length xsArgs' > funArity
          , (xsSat, xsOver)      <- splitAt funArity xsArgs'
-         = XLet an (LLet LetStrict (BAnon tBot') 
+         = XLet an (LLet (BAnon tBot') 
                         (makeXAppsWithAnnots xFun' xsSat))
-                   (makeXAppsWithAnnots 
+                   (snipLetBody config an
+                    $ makeXAppsWithAnnots 
                         (XVar an (UIx 0)) 
                         [ (L.liftX 1 x, a) | (x, a) <- xsOver ])
 
@@ -246,10 +275,12 @@
 
         -- Wrap the function application in the let-bindings
         -- for its arguments.
-   in   foldr (\(x, a) x' -> XLet a x x')
-                xFunApps
-                [ (LLet LetStrict (BAnon tBot') x, a) 
-                        | (x, a) <- xsLets' ]
+   in   case xsLets' of
+         []     -> xFunApps
+         _      -> foldr (\(x, a) x' -> XLet a x x')
+                        (snipLetBody config an xFunApps)
+                        [ (LLet (BAnon tBot') x, a) 
+                                | (x, a) <- xsLets' ]
 
 
 -- | Sort function arguments into either the atomic ones, 
@@ -274,9 +305,24 @@
          = (XVar a (UIx n), a, False, Just xArg)  : go (n + 1) xsArgs
 
 
+-- | If `snipLetResults` is set and this is not an atomic expression then
+--   introduce a new binding for it.
+snipLetBody :: Config -> a -> Exp a n -> Exp a n
+snipLetBody config a xx
+        | configSnipLetBody config
+        , not (isAtom xx)
+        , not (isXLet xx)
+        = let  tBot'   = T.tBot T.kData
+          in   XLet a  (LLet (BAnon tBot') xx)
+                       (XVar a (UIx 0))
+        
+        | otherwise
+        = xx
+
+
 -- | Check if an expression needs a binding, or if it's simple enough to be
 --   applied as-is.
-isAtom :: Ord n => Exp a n -> Bool
+isAtom :: Exp a n -> Bool
 isAtom xx
  = case xx of
         XVar{}          -> True
diff --git a/DDC/Core/Transform/Thread.hs b/DDC/Core/Transform/Thread.hs
new file mode 100644
--- /dev/null
+++ b/DDC/Core/Transform/Thread.hs
@@ -0,0 +1,412 @@
+
+-- | Thread a state token through calls to given functions.
+--
+--   ASSUMPTIONS:
+--   * Program is a-normalized and fully named.
+--
+module DDC.Core.Transform.Thread
+        ( Thread (..)
+        , Config (..)
+        , injectStateType)
+where
+import DDC.Core.Compounds
+import DDC.Core.Module
+import DDC.Core.Exp
+import DDC.Base.Pretty
+import DDC.Core.Transform.Reannotate
+import DDC.Core.Check           (AnTEC (..))
+import DDC.Type.Env             (KindEnv, TypeEnv)
+import qualified DDC.Type.Env   as Env
+import qualified DDC.Core.Check as Check
+
+
+-------------------------------------------------------------------------------
+-- | Configuration for the Thread transform.
+data Config a n
+        = Config
+        { -- | Config for the type checker.
+          --   We need to reconstruct the type of the result of stateful
+          --   functions when bundling them into the tuple that holds the 
+          --   state token.
+          configCheckConfig     :: Check.Config n
+
+          -- | Function to decide which top-level bindings are stateful and
+          --   need the state token threaded through them. If the binding with
+          --   the given name is stateful then the function should return the
+          --   new type for the binding that accepts and returns the state token.
+        , configThreadMe        :: n -> Type n -> Maybe (Type n) 
+
+          -- | Type of the state token to use.
+        , configTokenType       :: Type n
+
+          -- | Type that represents a missing value.
+          --   If a stateful function returns a void then our thread transform
+          --   rewrites it to return the state token, instead of a tuple
+          --   that contains the token as well as a void value.
+        , configVoidType        :: Type n
+
+          -- | Wrap a type with the world token.
+          --   eg change Int to (World#, Int)
+        , configWrapResultType  :: Type n -> Type n
+
+          -- | Wrap a result expression with the state token.
+          --   The function is given the types of the world token and result,
+          --   then the expressions for the same.
+        , configWrapResultExp   :: Exp (AnTEC a n) n  -> Exp (AnTEC a n) n 
+                                -> Exp a n
+
+          -- | Make a pattern which binds the world argument
+          --   from a threaded primop.
+        , configThreadPat       :: n -> Maybe (Bind n -> [Bind n] -> Pat n)
+        }
+
+
+-- | Class of things that can have a state token threaded through them.
+class Thread (c :: * -> * -> *) where
+ thread :: (Ord n, Show n, Pretty n)
+        => Config a n 
+        -> KindEnv n -> TypeEnv n 
+        -> c (AnTEC a n) n     
+        -> c a n
+
+
+instance Thread Module where
+ thread config kenv tenv mm
+  = let body'   = threadModuleBody config kenv tenv (moduleBody mm) 
+    in  mm { moduleBody = body' }
+
+
+-- | Keeps track of which recursive functions we're inside.
+data Context n
+        -- | We're in the body of an effectful recursive function.
+        = ContextRec n
+
+        -- | This effectful function in the context had a world token threaded
+        --   through it, but we're not in its body.
+        | ContextFun n
+        deriving Eq
+
+
+-- Module ---------------------------------------------------------------------
+-- | Thread state token though a module body.
+--   We assume every top-level binding is a stateful function
+--   that needs to accept and return the state token.
+threadModuleBody 
+        :: (Ord n, Show n, Pretty n)
+        => Config a n 
+        -> KindEnv n -> TypeEnv n
+        -> Exp (AnTEC a n) n   
+        -> Exp a n
+
+threadModuleBody config kenv tenv xx
+ = case xx of
+        XLet a lts x
+         -> let lts'       = threadTopLets    config kenv tenv lts
+                (bks, bts) = bindsOfLets lts
+                kenv'      = Env.extends bks kenv
+                tenv'      = Env.extends bts tenv
+                x'         = threadModuleBody config kenv' tenv' x
+            in  XLet (annotTail a) lts' x'
+
+        _ -> reannotate annotTail xx
+
+
+-- | Thread state token through some top-level bindings in a module.
+threadTopLets    
+        :: (Ord n, Show n, Pretty n)
+        => Config a n 
+        -> KindEnv n -> TypeEnv n
+        -> Lets (AnTEC a n) n  
+        -> Lets a n
+
+threadTopLets config kenv tenv lts
+ = case lts of
+        LLet b x
+         -> let (b', x')  = threadTopBind config [] kenv tenv b x
+            in  LLet b' x'
+
+        LRec bxs
+         -> let tenv'     =   Env.extends (map fst bxs) tenv
+                bxs'      = [ threadTopBind config [ContextRec n] kenv tenv' b x 
+                                | (b, x) <- bxs
+                                , let BName n _ = b ]
+            in  LRec bxs'
+
+        _ -> reannotate annotTail lts
+
+
+-- TopBind ------------------------------------------------------------------
+-- | Thread state token into a top-level binding.
+--   We assume every top-level binding is stateful function that needs to
+--   accept and return the state token.
+--
+--   We inject the world type into the type of the function and then call
+--   threadBind which will add the actual lambda for the new argument.
+--
+threadTopBind
+        :: (Ord n, Show n, Pretty n)
+        => Config a n
+        -> [Context n]
+        -> KindEnv n -> TypeEnv n
+        ->  Bind n   -> Exp (AnTEC a n) n
+        -> (Bind n,     Exp a n)
+
+threadTopBind config context kenv tenv b xBody
+ = let  tBind   = typeOfBind b
+        tBind'  = injectStateType config tBind
+        b'      = replaceTypeOfBind tBind' b
+        tenv'   = Env.extend b' tenv
+        tsArgs  = fst $ takeTFunAllArgResult tBind'
+   in   ( b'
+        , threadProc config context kenv tenv' xBody tsArgs)
+
+
+-- Arg ------------------------------------------------------------------------
+-- | Thread state token into an argument expression.
+--   If it is a syntactic function then we assume the function is stateful
+--   and needs the state token added, otherwise return it unharmed.
+threadArg 
+        :: (Ord n, Show n, Pretty n)
+        => Config a n
+        -> [Context n]
+        -> KindEnv n -> TypeEnv n
+        -> Type n    -> Exp (AnTEC a n) n
+        -> Exp a n
+
+threadArg config context kenv tenv t xx
+ = case xx of
+        XLam{}  -> threadProcArg config context kenv tenv t xx
+        XLAM{}  -> threadProcArg config context kenv tenv t xx
+        _       -> reannotate annotTail xx
+
+threadProcArg config context kenv tenv t xx
+ = let  tsArgs  = fst $ takeTFunAllArgResult t
+   in   threadProc config context kenv tenv xx tsArgs
+
+
+-- Proc -----------------------------------------------------------------------
+-- | Thread world token into the body of a stateful function (procedure).
+threadProc
+        :: (Ord n, Show n, Pretty n)
+        => Config a n
+        -> [Context n]
+        -> KindEnv n -> TypeEnv n
+        -> Exp (AnTEC a n) n    -- Whole expression, including lambdas.
+        -> [Type n]             -- Types of function parameters.
+        -> Exp a n
+
+-- We're out of parameters. 
+--  Now thread into the statements in the function body.
+threadProc config context kenv tenv xx []
+ = threadProcBody config context kenv tenv xx
+
+-- We're still decending past all the lambdas.
+--  When we get to the inner-most one then add the state parameter.
+threadProc config context kenv tenv xx (t : tsArgs)
+ = case xx of
+        XLAM a b x
+          -> let kenv'  = Env.extend b kenv
+                 x'     = threadProc config context kenv' tenv x tsArgs
+             in  XLAM (annotTail a) b x'
+
+        XLam a b x      
+          -> let tenv'  = Env.extend b tenv
+                 x'     = threadProc config context kenv tenv' x tsArgs
+             in  XLam (annotTail a) b x'
+
+        -- Inject a new lambda to bind the state parameter.
+        _ |  Just a     <- takeAnnotOfExp xx
+          ,  t == configTokenType config 
+          -> let b'     = BAnon (configTokenType config)
+                 tenv'  = Env.extend b' tenv
+                 x'     = threadProc config context kenv tenv' xx tsArgs
+             in  XLam (annotTail a) b' x'
+
+        -- We've decended past all the lambdas,
+        -- so now thread into the procedure body.
+        _ -> threadProcBody config context kenv tenv xx
+
+
+-- | Thread world token into the body of a procedure,
+--   after we've decended past all the lambdas.
+threadProcBody 
+        :: (Ord n, Show n, Pretty n)
+        => Config a n 
+        -> [Context n]
+        -> KindEnv n -> TypeEnv n
+        -> Exp (AnTEC a n) n   
+        -> Exp a n
+
+threadProcBody config context kenv tenv xx
+ = case xx of
+ 
+        -- Recursive let bindings in a procedure body.
+        -- These will be local loops.
+        XLet a (LRec bxs) x2
+         -> let bxs'    = [threadTopBind config 
+                                (context ++ [ContextRec n]) 
+                                kenv tenv b x
+                                | (b, x)        <- bxs 
+                                , let BName n _ = b ]
+
+                tenv'   = Env.extends (map fst bxs) tenv
+
+
+                x2'     = threadProcBody config 
+                                (context ++ [ContextFun n 
+                                                | (b, _x)  <- bxs
+                                                , let BName n _ = b ])
+                                kenv tenv' x2
+            in  XLet (annotTail a) (LRec bxs') x2'
+
+        -- A statement in the procedure body.
+        XLet _ (LLet b x) x2
+         |  Just (XVar a u, xsArgs) <- takeXApps x
+         ,  Just n       <- takeNameOfBound u
+         ,  Just tOld    <- Env.lookup u tenv
+         ,  Just tNew    <- configThreadMe  config n tOld
+         ,  Just mkPat   <- configThreadPat config n
+         -> let 
+                tWorld  = configTokenType config
+
+                -- Add world token as final argument 
+                xsArgs' = xsArgs ++ [XVar a (UIx 0)]
+
+                -- Thread into possibly higher order arguments.
+                tsArgs   = fst $ takeTFunAllArgResult tNew
+                xsArgs'' = zipWith (threadArg config context kenv tenv) tsArgs xsArgs'
+
+                -- Build the final expression.
+                u'      = replaceTypeOfBound tNew u
+                x'      = xApps (annotTail a) (XVar (annotTail a) u') xsArgs''
+
+                -- Thread into let-expression body.
+                tenv'   = Env.extend b tenv
+                x2'     = threadProcBody config context kenv tenv' x2
+                pat'    = mkPat (BAnon tWorld) [b]
+            in  XCase (annotTail a) x' [AAlt pat' x2']
+
+
+        -- Let bound effectful function.
+        -- Needs to be converted to a 'case'.
+        XLet a (LLet b x1) x2
+         | Just (XVar _ (UName n), _xsArgs) <- takeXApps x1
+         , elem (ContextFun n) context
+         , Just mkPat   <- configThreadPat config n
+         -> let 
+                tWorld  = configTokenType config
+                a'      = annotTail a
+                x1'     = XApp a' (reannotate annotTail x1) (XVar a' (UIx 0))
+                x2'     = threadProcBody config context kenv tenv x2
+                pat'    = mkPat (BAnon tWorld) [b]
+
+            in  XCase (annotTail a) x1' [AAlt pat' x2']
+
+
+        -- A pure binding that doesn't need the token.
+        XLet a lts x
+         -> let (bks, bts) = bindsOfLets lts
+                kenv'   = Env.extends bks kenv
+                tenv'   = Env.extends bts tenv
+                lts'    = reannotate annotTail lts
+                x'      = threadProcBody config context kenv' tenv' x
+            in  XLet (annotTail a) lts' x'
+
+
+        -- Case of an effectful function.
+        XCase a xScrut [AAlt (PData _dc bs) xBody]
+         | Just ((XVar _ (UName n), _xsArgs)) <- takeXApps xScrut
+         , elem (ContextFun n) context
+         , Just mkPat   <- configThreadPat config n
+         -> let 
+                a'      = annotTail a
+                tWorld  = configTokenType config
+                xScrut' = XApp a' (reannotate annotTail xScrut) (XVar a' (UIx 0))
+                pat'    = mkPat (BAnon tWorld) bs
+                alt'    = threadAlt config context kenv tenv 
+                                (AAlt pat' xBody)
+
+            in  XCase (annotTail a) xScrut' [alt']
+
+
+        -- Pure case. 
+        XCase a x alts
+         -> let alts' = map (threadAlt config context kenv tenv) alts
+                x'    = reannotate annotTail x
+            in  XCase (annotTail a) x' alts'
+
+        -- We shouldn't see these things in a proc body.
+        XLAM{}          -> error "ddc-core-simpl.Thread: unexpected XLAM"
+        XLam{}          -> error "ddc-core-simpl.Thread: unexpected XLam"
+        XCast{}         -> error "ddc-core-simpl.Thread: unexpected cast."
+        XType t         -> XType t
+        
+        XWitness w      
+         -> XWitness (reannotate annotTail w)
+
+        -- Tailcalls
+        XApp a _ _
+         | Just ((XVar _ (UName n), _xsArgs)) <- takeXApps xx
+         , elem (ContextRec n) context
+         -> let a'      = annotTail a
+            in  XApp a' (reannotate annotTail xx)
+                        (XVar a' (UIx 0))
+
+
+        -- For XVar, XCon, XApp as result value of function.
+        _
+         -- Otherwise wrap the returned value with a tuple holding
+         -- the world.
+         | otherwise
+         -> let Just a  = takeAnnotOfExp xx
+                a'      = AnTEC (configTokenType config) 
+                                (tBot kEffect) 
+                                (tBot kClosure)
+                                (annotTail a)
+
+                xWorld  = XVar a' (UIx 0)
+                wrap    = configWrapResultExp config
+            in  wrap xWorld xx
+
+
+
+-- | Thread world token into a case alternative
+threadAlt 
+        :: (Ord n, Show n, Pretty n)
+        => Config a n 
+        -> [Context n]
+        -> KindEnv n -> TypeEnv n
+        -> Alt (AnTEC a n) n   
+        -> Alt a n
+
+threadAlt config context kenv tenv (AAlt pat xx)
+ = case pat of
+        PDefault
+         ->     AAlt pat (threadProcBody config context kenv tenv xx)
+
+        PData _ bs
+         -> let tenv' = Env.extends bs tenv
+            in  AAlt pat (threadProcBody config context kenv tenv' xx)
+ 
+
+-------------------------------------------------------------------------------
+-- | Inject the state token into the type of an effectful function.
+--   Eg, change  ([a b : Data]. a -> b -> Int) 
+--          to   ([a b : Data]. a -> b -> World -> (World, Int)
+injectStateType :: Eq n => Config a n -> Type n -> Type n
+injectStateType config tt
+ = let down = injectStateType config
+   in case tt of
+        TForall b x     
+         -> TForall b (down x)
+
+        TApp{}
+         | (tsArg@(_ : _), tResult)     <- takeTFunArgResult tt
+         -> let  tsArg'   = tsArg ++ [configTokenType config]
+                 tResult' = injectStateType config tResult
+            in   foldr tFunPE tResult' tsArg'
+
+        _ | tt == configTokenType config -> tt
+          | tt == configVoidType  config -> configTokenType config
+          | otherwise                    -> configWrapResultType config tt
+
diff --git a/DDC/Core/Transform/TransformDownX.hs b/DDC/Core/Transform/TransformDownX.hs
new file mode 100644
--- /dev/null
+++ b/DDC/Core/Transform/TransformDownX.hs
@@ -0,0 +1,139 @@
+
+-- | General purpose tree walking boilerplate.
+module DDC.Core.Transform.TransformDownX
+        ( TransformDownMX(..)
+        , transformDownX
+        , transformDownX')
+where
+import DDC.Core.Module
+import DDC.Core.Exp
+import DDC.Core.Compounds
+import DDC.Type.Env             (KindEnv, TypeEnv)
+import Data.Functor.Identity
+import Control.Monad
+import qualified DDC.Type.Env   as Env
+
+
+-- | Top-down rewrite of all core expressions in a thing.
+transformDownX
+        :: forall (c :: * -> * -> *) a n
+        .  (Ord n, TransformDownMX Identity c)
+        => (KindEnv n -> TypeEnv n -> Exp a n -> Exp a n)       
+                        -- ^ The worker function is given the current kind and type environments.
+        -> KindEnv n    -- ^ Initial kind environment.
+        -> TypeEnv n    -- ^ Initial type environment.
+        -> c a n        -- ^ Transform this thing.
+        -> c a n
+
+transformDownX f kenv tenv xx
+        = runIdentity 
+        $ transformDownMX 
+                (\kenv' tenv' x -> return (f kenv' tenv' x)) 
+                kenv tenv xx
+
+
+-- | Like transformDownX, but without using environments.
+transformDownX'
+        :: forall (c :: * -> * -> *) a n
+        .  (Ord n, TransformDownMX Identity c)
+        => (Exp a n -> Exp a n)       
+                        -- ^ The worker function is given the current
+                        --      kind and type environments.
+        -> c a n        -- ^ Transform this thing.
+        -> c a n
+
+transformDownX' f xx
+        = transformDownX (\_ _ -> f) Env.empty Env.empty xx
+
+
+-------------------------------------------------------------------------------
+class TransformDownMX m (c :: * -> * -> *) where
+ -- | Top-down monadic rewrite of all core expressions in a thing.
+ transformDownMX
+        :: Ord n
+        => (KindEnv n -> TypeEnv n -> Exp a n -> m (Exp a n))
+                        -- ^ The worker function is given the current
+                        --      kind and type environments.
+        -> KindEnv n    -- ^ Initial kind environment.
+        -> TypeEnv n    -- ^ Initial type environment.
+        -> c a n        -- ^ Transform this thing.
+        -> m (c a n)
+
+
+instance Monad m => TransformDownMX m Module where
+ transformDownMX f kenv tenv !mm
+  = do  x'    <- transformDownMX f kenv tenv $ moduleBody mm
+        return  $ mm { moduleBody = x' }
+
+
+instance Monad m => TransformDownMX m Exp where
+ transformDownMX f kenv tenv !xx
+  = {-# SCC transformDownMX #-} 
+    f kenv tenv xx >>= \xx' -> 
+     case xx' of
+        XVar{}          -> return xx'
+        XCon{}          -> return xx'
+
+        XLAM a b x1
+         -> liftM3 XLAM (return a) (return b)
+                        (transformDownMX f (Env.extend b kenv) tenv x1)
+
+        XLam a b  x1    
+         -> liftM3 XLam (return a) (return b) 
+                        (transformDownMX f kenv (Env.extend b tenv) x1)
+
+        XApp a x1 x2    
+         -> liftM3 XApp (return a) 
+                        (transformDownMX f kenv tenv x1) 
+                        (transformDownMX f kenv tenv x2)
+
+        XLet a lts x
+         -> do  lts'      <- transformDownMX f kenv tenv lts
+                let kenv' = Env.extends (specBindsOfLets lts')   kenv
+                let tenv' = Env.extends (valwitBindsOfLets lts') tenv
+                x'        <- transformDownMX f kenv' tenv' x
+                return  $ XLet a lts' x'
+                
+        XCase a x alts
+         -> liftM3 XCase (return a)
+                         (transformDownMX f kenv tenv x)
+                         (mapM (transformDownMX f kenv tenv) alts)
+
+        XCast a c x       
+         -> liftM3 XCast
+                        (return a) (return c)
+                        (transformDownMX f kenv tenv x)
+
+        XType _         -> return xx'
+        XWitness _      -> return xx'
+
+
+instance Monad m => TransformDownMX m Lets where
+ transformDownMX f kenv tenv xx
+  = case xx of
+        LLet b x
+         -> liftM2 LLet (return b)
+                        (transformDownMX f kenv tenv x)
+        
+        LRec bxs
+         -> do  let (bs, xs) = unzip bxs
+                let tenv'    = Env.extends bs tenv
+                xs'          <- mapM (transformDownMX f kenv tenv') xs
+                return       $ LRec $ zip bs xs'
+
+        LLetRegions{}    -> return xx
+        LWithRegion{}    -> return xx
+
+
+instance Monad m => TransformDownMX m Alt where
+ transformDownMX f kenv tenv alt
+  = case alt of
+        AAlt p@(PData _ bsArg) x
+         -> let tenv'   = Env.extends bsArg tenv
+            in  liftM2  AAlt (return p) 
+                        (transformDownMX f kenv tenv' x)
+
+        AAlt PDefault x
+         ->     liftM2  AAlt (return PDefault)
+                        (transformDownMX f kenv tenv x) 
+
diff --git a/DDC/Core/Transform/TransformUpX.hs b/DDC/Core/Transform/TransformUpX.hs
new file mode 100644
--- /dev/null
+++ b/DDC/Core/Transform/TransformUpX.hs
@@ -0,0 +1,215 @@
+
+-- | General purpose tree walking boilerplate.
+module DDC.Core.Transform.TransformUpX
+        ( TransformUpMX(..)
+        , transformUpX
+        , transformUpX'
+
+          -- * Via the Simple AST
+        , transformSimpleUpMX
+        , transformSimpleUpX
+        , transformSimpleUpX')
+where
+import DDC.Core.Module
+import DDC.Core.Exp
+import DDC.Core.Compounds
+import DDC.Core.Transform.Annotate
+import DDC.Core.Transform.Deannotate
+import DDC.Type.Env             (KindEnv, TypeEnv)
+import Data.Functor.Identity
+import Control.Monad
+import qualified DDC.Type.Env           as Env
+import qualified DDC.Core.Exp.Simple    as S
+
+
+-- | Bottom up rewrite of all core expressions in a thing.
+transformUpX
+        :: forall (c :: * -> * -> *) a n
+        .  (Ord n, TransformUpMX Identity c)
+        => (KindEnv n -> TypeEnv n -> Exp a n -> Exp a n)       
+                        -- ^ The worker function is given the current kind and type environments.
+        -> KindEnv n    -- ^ Initial kind environment.
+        -> TypeEnv n    -- ^ Initial type environment.
+        -> c a n        -- ^ Transform this thing.
+        -> c a n
+
+transformUpX f kenv tenv xx
+        = runIdentity 
+        $ transformUpMX 
+                (\kenv' tenv' x -> return (f kenv' tenv' x)) 
+                kenv tenv xx
+
+
+-- | Like transformUpX, but without using environments.
+transformUpX'
+        :: forall (c :: * -> * -> *) a n
+        .  (Ord n, TransformUpMX Identity c)
+        => (Exp a n -> Exp a n)       
+                        -- ^ The worker function is given the current
+                        --      kind and type environments.
+        -> c a n        -- ^ Transform this thing.
+        -> c a n
+
+transformUpX' f xx
+        = transformUpX (\_ _ -> f) Env.empty Env.empty xx
+
+
+-------------------------------------------------------------------------------
+class TransformUpMX m (c :: * -> * -> *) where
+ -- | Bottom-up monadic rewrite of all core expressions in a thing.
+ transformUpMX
+        :: Ord n
+        => (KindEnv n -> TypeEnv n -> Exp a n -> m (Exp a n))
+                        -- ^ The worker function is given the current
+                        --      kind and type environments.
+        -> KindEnv n    -- ^ Initial kind environment.
+        -> TypeEnv n    -- ^ Initial type environment.
+        -> c a n        -- ^ Transform this thing.
+        -> m (c a n)
+
+
+instance Monad m => TransformUpMX m Module where
+ transformUpMX f kenv tenv !mm
+  = do  x'    <- transformUpMX f kenv tenv $ moduleBody mm
+        return  $ mm { moduleBody = x' }
+
+
+instance Monad m => TransformUpMX m Exp where
+ transformUpMX f kenv tenv !xx
+  = (f kenv tenv =<<)
+  $ case xx of
+        XVar{}          -> return xx
+        XCon{}          -> return xx
+
+        XLAM a b x1
+         -> liftM3 XLAM (return a) (return b)
+                        (transformUpMX f (Env.extend b kenv) tenv x1)
+
+        XLam a b  x1    
+         -> liftM3 XLam (return a) (return b) 
+                        (transformUpMX f kenv (Env.extend b tenv) x1)
+
+        XApp a x1 x2    
+         -> liftM3 XApp (return a) 
+                        (transformUpMX f kenv tenv x1) 
+                        (transformUpMX f kenv tenv x2)
+
+        XLet a lts x
+         -> do  lts'      <- transformUpMX f kenv tenv lts
+                let kenv' = Env.extends (specBindsOfLets lts')   kenv
+                let tenv' = Env.extends (valwitBindsOfLets lts') tenv
+                x'        <- transformUpMX f kenv' tenv' x
+                return  $ XLet a lts' x'
+                
+        XCase a x alts
+         -> liftM3 XCase (return a)
+                         (transformUpMX f kenv tenv x)
+                         (mapM (transformUpMX f kenv tenv) alts)
+
+        XCast a c x       
+         -> liftM3 XCast
+                        (return a) (return c)
+                        (transformUpMX f kenv tenv x)
+
+        XType _         -> return xx
+        XWitness _      -> return xx
+
+
+instance Monad m => TransformUpMX m Lets where
+ transformUpMX f kenv tenv xx
+  = case xx of
+        LLet b x
+         -> liftM2 LLet (return b)
+                        (transformUpMX f kenv tenv x)
+        
+        LRec bxs
+         -> do  let (bs, xs) = unzip bxs
+                let tenv'    = Env.extends bs tenv
+                xs'          <- mapM (transformUpMX f kenv tenv') xs
+                return       $ LRec $ zip bs xs'
+
+        LLetRegions{}    -> return xx
+        LWithRegion{}    -> return xx
+
+
+instance Monad m => TransformUpMX m Alt where
+ transformUpMX f kenv tenv alt
+  = case alt of
+        AAlt p@(PData _ bsArg) x
+         -> let tenv'   = Env.extends bsArg tenv
+            in  liftM2  AAlt (return p) 
+                        (transformUpMX f kenv tenv' x)
+
+        AAlt PDefault x
+         ->     liftM2  AAlt (return PDefault)
+                        (transformUpMX f kenv tenv x) 
+
+
+-- Simple ---------------------------------------------------------------------
+-- | Like `transformUpMX`, but the worker takes the Simple version of the AST.
+--
+--   * To avoid repeated conversions between the different versions of the AST,
+--     the worker should return `Nothing` if the provided expression is unchanged.
+transformSimpleUpMX 
+        :: (Ord n, TransformUpMX m c, Monad m)
+        => (KindEnv n -> TypeEnv n -> S.Exp a n -> m (Maybe (S.Exp a n)))
+                        -- ^ The worker function is given the current
+                        --     kind and type environments.
+        -> KindEnv n    -- ^ Initial kind environment.
+        -> TypeEnv n    -- ^ Initial type environment.
+        -> c a n        -- ^ Transform thing thing.
+        -> m (c a n)
+
+transformSimpleUpMX f kenv0 tenv0 xx0
+ = let  
+        f' kenv tenv xx
+         = case takeAnnotOfExp xx of
+            Nothing -> return xx
+            Just a  
+             -> do let sxx  = deannotate (const Nothing) xx
+                   msxx'    <- f kenv tenv sxx
+                   case msxx' of
+                        Nothing   -> return $ xx
+                        Just sxx' -> return $ annotate a sxx'
+
+   in   transformUpMX f' kenv0 tenv0 xx0
+
+
+-- | Like `transformUpX`, but the worker takes the Simple version of the AST.
+--
+--   * To avoid repeated conversions between the different versions of the AST,
+--     the worker should return `Nothing` if the provided expression is unchanged.
+transformSimpleUpX
+        :: forall (c :: * -> * -> *) a n
+        .  (Ord n, TransformUpMX Identity c)
+        => (KindEnv n -> TypeEnv n -> S.Exp a n -> Maybe (S.Exp a n))
+                      -- ^ The worker function is given the current
+                      --     kind and type environments.
+        -> KindEnv n  -- ^ Initial kind environment.
+        -> TypeEnv n  -- ^ Initial type environment.
+        -> c a n      -- ^ Transform this thing.
+        -> c a n
+
+transformSimpleUpX f kenv tenv xx
+        = runIdentity 
+        $ transformSimpleUpMX 
+                (\kenv' tenv' x -> return (f kenv' tenv' x)) 
+                kenv tenv xx
+
+
+-- | Like `transformUpX'`, but the worker takes the Simple version of the AST.
+--
+--   * To avoid repeated conversions between the different versions of the AST,
+--     the worker should return `Nothing` if the provided expression is unchanged.
+transformSimpleUpX'
+        :: forall (c :: * -> * -> *) a n
+        .  (Ord n, TransformUpMX Identity c)
+        => (S.Exp a n -> Maybe (S.Exp a n))
+                        -- ^ The worker function is given the current
+                        --      kind and type environments.
+        -> c a n        -- ^ Transform this thing.
+        -> c a n
+
+transformSimpleUpX' f xx
+        = transformSimpleUpX (\_ _ -> f) Env.empty Env.empty xx
+
diff --git a/DDC/Core/Transform/TransformX.hs b/DDC/Core/Transform/TransformX.hs
deleted file mode 100644
--- a/DDC/Core/Transform/TransformX.hs
+++ /dev/null
@@ -1,139 +0,0 @@
-
--- | General purpose tree walking boilerplate.
-module DDC.Core.Transform.TransformX
-        ( TransformUpMX(..)
-        , transformUpX
-        , transformUpX')
-where
-import DDC.Core.Module
-import DDC.Core.Exp
-import DDC.Core.Compounds
-import DDC.Type.Env             (KindEnv, TypeEnv)
-import Data.Functor.Identity
-import Control.Monad
-import qualified DDC.Type.Env   as Env
-
-
--- | Bottom up rewrite of all core expressions in a thing.
-transformUpX
-        :: forall (c :: * -> * -> *) a n
-        .  (Ord n, TransformUpMX Identity c)
-        => (KindEnv n -> TypeEnv n -> Exp a n -> Exp a n)       
-                        -- ^ The worker function is given the current kind and type environments.
-        -> KindEnv n    -- ^ Initial kind environment.
-        -> TypeEnv n    -- ^ Initial type environment.
-        -> c a n        -- ^ Transform this thing.
-        -> c a n
-
-transformUpX f kenv tenv xx
-        = runIdentity 
-        $ transformUpMX 
-                (\kenv' tenv' x -> return (f kenv' tenv' x)) 
-                kenv tenv xx
-
-
--- | Like transformUpX, but without using environments.
-transformUpX'
-        :: forall (c :: * -> * -> *) a n
-        .  (Ord n, TransformUpMX Identity c)
-        => (Exp a n -> Exp a n)       
-                        -- ^ The worker function is given the current
-                        --      kind and type environments.
-        -> c a n        -- ^ Transform this thing.
-        -> c a n
-
-transformUpX' f xx
-        = transformUpX (\_ _ -> f) Env.empty Env.empty xx
-
-
--------------------------------------------------------------------------------
-class TransformUpMX m (c :: * -> * -> *) where
- -- | Bottom-up monadic rewrite of all core expressions in a thing.
- transformUpMX
-        :: Ord n
-        => (KindEnv n -> TypeEnv n -> Exp a n -> m (Exp a n))
-                        -- ^ The worker function is given the current
-                        --      kind and type environments.
-        -> KindEnv n    -- ^ Initial kind environment.
-        -> TypeEnv n    -- ^ Initial type environment.
-        -> c a n        -- ^ Transform this thing.
-        -> m (c a n)
-
-
-instance Monad m => TransformUpMX m Module where
- transformUpMX f kenv tenv !mm
-  = do  x'    <- transformUpMX f kenv tenv $ moduleBody mm
-        return  $ mm { moduleBody = x' }
-
-
-instance Monad m => TransformUpMX m Exp where
- transformUpMX f kenv tenv !xx
-  = {-# SCC transformUpMX #-} 
-    (f kenv tenv =<<)
-  $ case xx of
-        XVar{}          -> return xx
-        XCon{}          -> return xx
-
-        XLAM a b x1
-         -> liftM3 XLAM (return a) (return b)
-                        (transformUpMX f (Env.extend b kenv) tenv x1)
-
-        XLam a b  x1    
-         -> liftM3 XLam (return a) (return b) 
-                        (transformUpMX f kenv (Env.extend b tenv) x1)
-
-        XApp a x1 x2    
-         -> liftM3 XApp (return a) 
-                        (transformUpMX f kenv tenv x1) 
-                        (transformUpMX f kenv tenv x2)
-
-        XLet a lts x
-         -> do  lts'      <- transformUpMX f kenv tenv lts
-                let kenv' = Env.extends (specBindsOfLets lts')   kenv
-                let tenv' = Env.extends (valwitBindsOfLets lts') tenv
-                x'        <- transformUpMX f kenv' tenv' x
-                return  $ XLet a lts' x'
-                
-        XCase a x alts
-         -> liftM3 XCase (return a)
-                         (transformUpMX f kenv tenv x)
-                         (mapM (transformUpMX f kenv tenv) alts)
-
-        XCast a c x       
-         -> liftM3 XCast
-                        (return a) (return c)
-                        (transformUpMX f kenv tenv x)
-
-        XType _         -> return xx
-        XWitness _      -> return xx
-
-
-instance Monad m => TransformUpMX m Lets where
- transformUpMX f kenv tenv xx
-  = case xx of
-        LLet m b x
-         -> liftM3 LLet (return m) (return b)
-                        (transformUpMX f kenv tenv x)
-        
-        LRec bxs
-         -> do  let (bs, xs) = unzip bxs
-                let tenv'    = Env.extends bs tenv
-                xs'          <- mapM (transformUpMX f kenv tenv') xs
-                return       $ LRec $ zip bs xs'
-
-        LLetRegions{}    -> return xx
-        LWithRegion{}    -> return xx
-
-
-instance Monad m => TransformUpMX m Alt where
- transformUpMX f kenv tenv alt
-  = case alt of
-        AAlt p@(PData _ bsArg) x
-         -> let tenv'   = Env.extends bsArg tenv
-            in  liftM2  AAlt (return p) 
-                        (transformUpMX f kenv tenv' x)
-
-        AAlt PDefault x
-         ->     liftM2  AAlt (return PDefault)
-                        (transformUpMX f kenv tenv x) 
-
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,7 +1,7 @@
 --------------------------------------------------------------------------------
 The Disciplined Disciple Compiler License (MIT style)
 
-Copyrite (K) 2007-2012 The Disciplined Disciple Compiler Strike Force
+Copyrite (K) 2007-2013 The Disciplined Disciple Compiler Strike Force
 All rights reversed.
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
diff --git a/ddc-core-simpl.cabal b/ddc-core-simpl.cabal
--- a/ddc-core-simpl.cabal
+++ b/ddc-core-simpl.cabal
@@ -1,5 +1,5 @@
 Name:           ddc-core-simpl
-Version:        0.3.1.1
+Version:        0.3.2.1
 License:        MIT
 License-file:   LICENSE
 Author:         The Disciplined Disciple Compiler Strike Force
@@ -9,7 +9,6 @@
 Stability:      experimental
 Category:       Compilers/Interpreters
 Homepage:       http://disciple.ouroborus.net
-Bug-reports:    disciple@ouroborus.net
 Synopsis:       Disciplined Disciple Compiler code transformations.
 Description:    Disciplined Disciple Compiler code transformations.
 
@@ -21,14 +20,15 @@
         array           == 0.4.*,
         transformers    == 0.3.*,
         mtl             == 2.1.*,
-        ddc-base        == 0.3.1.*,
-        ddc-core        == 0.3.1.*
+        ddc-base        == 0.3.2.*,
+        ddc-core        == 0.3.2.*
 
   Exposed-modules:
         DDC.Core.Analysis.Arity
         DDC.Core.Analysis.Usage
         DDC.Core.Simplifier.Recipe
         DDC.Core.Simplifier.Parser
+        DDC.Core.Simplifier.Result
         DDC.Core.Transform.Rewrite.Disjoint
         DDC.Core.Transform.Rewrite.Env
         DDC.Core.Transform.Rewrite.Match
@@ -39,13 +39,16 @@
         DDC.Core.Transform.Bubble
         DDC.Core.Transform.Prune
         DDC.Core.Transform.Elaborate
+        DDC.Core.Transform.Eta
         DDC.Core.Transform.Flatten
         DDC.Core.Transform.Forward
         DDC.Core.Transform.Inline
         DDC.Core.Transform.Namify
         DDC.Core.Transform.Rewrite
         DDC.Core.Transform.Snip
-        DDC.Core.Transform.TransformX
+        DDC.Core.Transform.Thread
+        DDC.Core.Transform.TransformUpX
+        DDC.Core.Transform.TransformDownX
         DDC.Core.Simplifier
 
         DDC.Type.Transform.Alpha