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
@@ -78,10 +78,10 @@
 
         aritiesImports  
          = catMaybes
-         $ [ case arityFromType t of
-                Just a  -> Just (BName n t, a)
+         $ [ case arityFromType (typeOfImportSource isrc) of
+                Just a  -> Just (BName n (typeOfImportSource isrc), a)
                 Nothing -> Nothing
-           | (n, (_, t)) <- Map.toList $ moduleImportTypes mm ]
+           | (n, isrc) <- moduleImportTypes mm ]
 
     in  emptyArities
         `extendsArities` aritiesImports
@@ -119,7 +119,8 @@
         XLAM _ _ e      -> liftM (+ 1) $ arityOfExp e
 
         -- Determine a data constructor's arity from its type.
-        XCon _ dc       -> arityFromType (typeOfDaCon dc)
+        XCon _ (DaConPrim _ t)
+                -> arityFromType t
 
         -- Anything else we'll need to apply one at a time
         _               -> Just 0
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
@@ -25,8 +25,8 @@
         -- | Bound variable is destructed by a case-expression.
         | UsedDestruct
 
-	-- | Bound variable is used inside a @weakclo@ cast.
-	| UsedInCast
+        -- | Bound variable is used inside a @weakclo@ cast.
+        | UsedInCast
 
         -- | Bound variable has an occurrence that is not one of the above.
         | UsedOcc
@@ -78,21 +78,23 @@
         :: Ord n
         => Module a n
         -> Module (UsedMap n, a) n
-usageModule 
+usageModule
         (ModuleCore
                 { moduleName            = name
-                , moduleExportKinds     = exportKinds
                 , moduleExportTypes     = exportTypes
-                , moduleImportKinds     = importKinds
+                , moduleExportValues    = exportValues
                 , moduleImportTypes     = importTypes
+                , moduleImportValues    = importValues
+                , moduleDataDefsLocal   = dataDefsLocal
                 , moduleBody            = body })
 
  =       ModuleCore
                 { moduleName            = name
-                , moduleExportKinds     = exportKinds
                 , moduleExportTypes     = exportTypes
-                , moduleImportKinds     = importKinds
+                , moduleExportValues    = exportValues
                 , moduleImportTypes     = importTypes
+                , moduleImportValues    = importValues
+                , moduleDataDefsLocal   = dataDefsLocal
                 , moduleBody            = usageX body }
 
 
@@ -179,13 +181,14 @@
          -> ( used'
             , XCast (used', a) c' x1')
 
-        XType t        
-         -> (empty, XType t)
+        XType a t        
+         -> ( empty
+            , XType (empty, a) t)
 
-        XWitness w     
+        XWitness a w     
          | (used', w')    <- usageWitness w
          -> ( used'
-            , XWitness w')
+            , XWitness (used', a) w')
 
 
 -- | Annotate binding occurences of named variables with usage information.
@@ -206,8 +209,8 @@
          ,  used'         <- sumUsedMap useds'
          -> (used', LRec $ zip bs xs')
 
-        LLetRegions b bs 
-         -> (empty, LLetRegions b bs)
+        LPrivate b mt bs 
+         -> (empty, LPrivate b mt bs)
 
         LWithRegion b
          -> (empty, LWithRegion b)
@@ -227,7 +230,7 @@
         CastWeakenClosure xs
          | (useds, xs')         <- unzip $ map usageX' xs
          , UsedMap used'        <- sumUsedMap useds
-	 , usedCasts		<- Map.map (map $ const UsedInCast) used'
+         , usedCasts            <- Map.map (map $ const UsedInCast) used'
          -> (UsedMap usedCasts, CastWeakenClosure xs')
 
         CastPurify w
@@ -238,7 +241,7 @@
          | (used, w')   <- usageWitness w
          -> (used, CastForget w')
 
-        CastSuspend     -> (empty, CastSuspend)
+        CastBox         -> (empty, CastBox)
         CastRun         -> (empty, CastRun)
 
 
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
@@ -26,8 +26,7 @@
 import DDC.Type.Env                     (KindEnv, TypeEnv)
 import Data.Typeable                    (Typeable)
 import Control.Monad.State.Strict
-import Control.DeepSeq
-import qualified DDC.Base.Pretty	as P
+import qualified DDC.Base.Pretty        as P
 import qualified Data.Set               as Set
 
 
@@ -35,66 +34,126 @@
 -- | Apply a simplifier to a module.
 --
 --   The state monad can be used by `Namifier` functions to generate fresh names.
----
---   ISSUE #277: Make 'applySimplifier' return a TransformResult
---      Applying a simplifier to an expression yields a TransformResult
---      with the transform log, and we should get one for a module as well.
 --
 applySimplifier 
-        :: (Show a, Ord n, Show n, Pretty n, NFData a, NFData n) 
-	=> Profile n		-- ^ Profile of language we're working in
-	-> KindEnv n		-- ^ Kind environment
-	-> TypeEnv n		-- ^ Type environment
+        :: (Show a, Ord n, Show n, Pretty n) 
+        => Profile n            -- ^ Profile of language we're working in
+        -> KindEnv n            -- ^ Kind environment
+        -> TypeEnv n            -- ^ Type environment
         -> Simplifier s a n     -- ^ Simplifier to apply
         -> Module a n           -- ^ Module to simplify
-        -> State s (Module a n)
+        -> State s (TransformResult (Module a n))
 
 applySimplifier !profile !kenv !tenv !spec !mm
- = case spec of
+ = let down = applySimplifier profile kenv tenv
+   in  case spec of
         Seq t1 t2
-         -> do  !mm'     <- applySimplifier profile kenv tenv t1 mm
-                applySimplifier profile kenv tenv t2 mm'
+         -> do  tm  <- down t1 mm
+                tm' <- down t2 (result tm)
 
+                let info =
+                        case (resultInfo tm, resultInfo tm') of
+                        (TransformInfo i1, TransformInfo i2) -> SeqInfo i1 i2
+                
+                let again    = resultAgain    tm || resultAgain    tm'
+                let progress = resultProgress tm || resultProgress tm'
+
+                return TransformResult
+                        { result         = result tm'
+                        , resultAgain    = again
+                        , resultProgress = progress
+                        , resultInfo     = TransformInfo info }
+
+        Fix i s
+         -> do  tm      <- applyFixpoint profile kenv tenv i s mm
+                let info =
+                        case resultInfo tm of
+                        TransformInfo info1 -> FixInfo i info1
+                
+                return TransformResult
+                        { result         = result tm
+                        , resultAgain    = resultAgain    tm
+                        , resultProgress = resultProgress tm
+                        , resultInfo     = TransformInfo info }
+
         Trans t1
          -> applyTransform profile kenv tenv t1 mm
-	
-	Fix 0 _
-	 -> return mm
 
-	Fix !n !s
-	 -> do	!mm' <- applySimplifier profile kenv tenv s mm
-                applySimplifier profile kenv tenv (Fix (n - 1) s) mm'
 
+-- | Apply a transform until it stops progressing, or a maximum number of times
+applyFixpoint
+        :: (Show a, Ord n, Show n, Pretty n)
+        => Profile n            -- ^ Profile of language we're working in
+        -> KindEnv n            -- ^ Kind environment
+        -> TypeEnv n            -- ^ Type environment
+        -> Int                  -- ^ Maximum number of times to apply
+        -> Simplifier s a n      -- ^ Transform to apply.
+        -> Module a n           -- ^ Module to simplify.
+        -> State s (TransformResult (Module a n))
 
+applyFixpoint !profile !kenv !tenv !i' !spec !mm'
+ = go i' mm' False
+ where
+  simp = applySimplifier profile kenv tenv spec
+
+  go 0 mm progress 
+   = do tm  <- simp mm
+        return tm { resultProgress = progress }
+
+  go i mm progress 
+   = do tm  <- simp mm
+        case resultAgain tm of
+         False 
+          ->    return tm { resultProgress = progress }
+
+         True  
+          -> do tm' <- go (i-1) (result tm) True
+
+                let info 
+                     = case (resultInfo tm, resultInfo tm') of
+                        (TransformInfo i1, TransformInfo i2)
+                          -> SeqInfo i1 i2
+
+                return TransformResult
+                        { result         = result tm'
+                        , resultAgain    = resultProgress tm'
+                        , resultProgress = resultProgress tm'
+                        , resultInfo     = TransformInfo info }
+
 -- | Apply a transform to a module.
 applyTransform
         :: (Show a, Ord n, Show n, Pretty n)
-	=> Profile n		-- ^ Profile of language we're working in
-	-> KindEnv n		-- ^ Kind environment
-	-> TypeEnv n		-- ^ Type environment
+        => Profile n            -- ^ Profile of language we're working in
+        -> KindEnv n            -- ^ Kind environment
+        -> TypeEnv n            -- ^ Type environment
         -> Transform s a n      -- ^ Transform to apply.
         -> Module a n           -- ^ Module to simplify.
-        -> State s (Module a n)
+        -> State s (TransformResult (Module a n))
 
 applyTransform !profile !_kenv !_tenv !spec !mm
- = case spec of
-        Id               -> return mm
-        Anonymize        -> return $ anonymizeX mm
-        Snip config      -> return $ snip config mm
-        Flatten          -> return $ flatten mm
-        Beta config      -> return $ result $ betaReduce config mm
-        Eta  config      -> return $ result $ Eta.etaModule config profile mm
+ = let  res x = return $ resultDone (show $ ppr spec) x
+   in case spec of
+        Id               -> res mm
+        Anonymize        -> res $ anonymizeX mm
+        Snip config      -> res $ snip config mm
+        Flatten          -> res $ flatten mm
 
+        Beta config      
+         -> return $ betaReduce    profile config mm
+
+        Eta  config      
+         -> return $ Eta.etaModule profile config mm
+
         Forward          
          -> let config  = Forward.Config (const FloatAllow) False
-            in  return $ result $ forwardModule profile config mm
+            in  return $ forwardModule profile config mm
 
-        Bubble           -> return $ bubbleModule mm
-        Namify namK namT -> namifyUnique namK namT mm
-        Inline getDef    -> return $ inline getDef Set.empty mm
-        Rewrite rules    -> return $ rewriteModule rules mm
-        Prune            -> return $ pruneModule profile mm
-        Elaborate        -> return $ elaborateModule mm
+        Bubble           -> res $ bubbleModule mm
+        Namify namK namT -> namifyUnique namK namT mm >>= res
+        Inline getDef    -> res $ inline getDef Set.empty mm
+        Rewrite rules    -> res $ rewriteModule rules mm
+        Prune            -> res $ pruneModule profile mm
+        Elaborate        -> res $ elaborateModule mm
 
 
 -- Expressions ----------------------------------------------------------------
@@ -104,9 +163,9 @@
 --
 applySimplifierX 
         :: (Show a, Show n, Ord n, Pretty n)
-	=> Profile n		-- ^ Profile of language we're working in
-	-> KindEnv n		-- ^ Kind environment
-	-> TypeEnv n		-- ^ Type environment
+        => Profile n            -- ^ Profile of language we're working in
+        -> KindEnv n            -- ^ Kind environment
+        -> TypeEnv n            -- ^ Type environment
         -> Simplifier s a n     -- ^ Simplifier to apply
         -> Exp a n              -- ^ Expression to simplify
         -> State s (TransformResult (Exp a n))
@@ -118,31 +177,31 @@
          -> do  tx  <- down t1 xx
                 tx' <- down t2 (result tx)
 
-		let info =
-			case (resultInfo tx, resultInfo tx') of
-			(TransformInfo i1, TransformInfo i2) -> SeqInfo i1 i2
-		
+                let info =
+                        case (resultInfo tx, resultInfo tx') of
+                        (TransformInfo i1, TransformInfo i2) -> SeqInfo i1 i2
+                
                 let again    = resultAgain    tx || resultAgain    tx'
                 let progress = resultProgress tx || resultProgress tx'
 
-		return TransformResult
+                return TransformResult
                         { result         = result tx'
                         , resultAgain    = again
                         , resultProgress = progress
                         , resultInfo     = TransformInfo info }
 
-	Fix i s
-	 -> do	tx      <- applyFixpointX profile kenv tenv i s xx
-		let info =
-			case resultInfo tx of
-			TransformInfo info1 -> FixInfo i info1
-		
-		return TransformResult
+        Fix i s
+         -> do  tx      <- applyFixpointX profile kenv tenv i s xx
+                let info =
+                        case resultInfo tx of
+                        TransformInfo info1 -> FixInfo i info1
+                
+                return TransformResult
                         { result         = result tx
                         , resultAgain    = resultAgain    tx
                         , resultProgress = resultProgress tx
                         , resultInfo     = TransformInfo info }
-		
+                
         Trans t1
          -> applyTransformX profile kenv tenv t1 xx
 
@@ -150,11 +209,11 @@
 -- | Apply a simplifier until it stops progressing, or a maximum number of times
 applyFixpointX
         :: (Show a, Show n, Ord n, Pretty n)
-	=> Profile n		-- ^ Profile of language we're working in
-	-> KindEnv n		-- ^ Kind environment
-	-> TypeEnv n		-- ^ Type environment
-        -> Int			-- ^ Maximum number of times to apply
-	-> Simplifier s a n     -- ^ Simplifier to apply.
+        => Profile n            -- ^ Profile of language we're working in
+        -> KindEnv n            -- ^ Kind environment
+        -> TypeEnv n            -- ^ Type environment
+        -> Int                  -- ^ Maximum number of times to apply
+        -> Simplifier s a n     -- ^ Simplifier to apply.
         -> Exp a n              -- ^ Exp to simplify.
         -> State s (TransformResult (Exp a n))
 
@@ -170,19 +229,19 @@
   go i xx progress 
    = do tx      <- simp xx
         case resultAgain tx of
-	 False 
+         False 
           ->    return tx { resultProgress = progress }
 
-	 True  
+         True  
           -> do tx'        <- go (i-1) (result tx) True
 
-	        let info 
+                let info 
                      = case (resultInfo tx, resultInfo tx') of
-	                (TransformInfo i1, TransformInfo i2) 
+                        (TransformInfo i1, TransformInfo i2) 
                           -> SeqInfo i1 i2
 
-	        return TransformResult
-                        { result   	 = result tx'
+                return TransformResult
+                        { result         = result tx'
                         , resultAgain    = resultProgress tx'
                         , resultProgress = resultProgress tx'
                         , resultInfo     = TransformInfo info }
@@ -217,9 +276,9 @@
 -- | Apply a single transform to an expression.
 applyTransformX 
         :: (Show a, Show n, Ord n, Pretty n)
-	=> Profile n		-- ^ Profile of language we're working in
-	-> KindEnv n		-- ^ Kind environment
-	-> TypeEnv n		-- ^ Type environment
+        => Profile n            -- ^ Profile of language we're working in
+        -> KindEnv n            -- ^ Kind environment
+        -> TypeEnv n            -- ^ Type environment
         -> Transform s a n      -- ^ Transform to apply.
         -> Exp a n              -- ^ Exp  to transform.
         -> State s (TransformResult (Exp a n))
@@ -232,9 +291,15 @@
         Snip config       -> res    $ snip config xx
         Flatten           -> res    $ flatten xx
         Inline  getDef    -> res    $ inline getDef Set.empty xx
-        Beta config       -> return $ betaReduce config xx
-        Eta  config       -> return $ Eta.etaX config profile kenv tenv xx
-        Prune             -> return $ pruneX   profile kenv tenv xx
+
+        Beta config       
+         -> return $ betaReduce profile config xx
+
+        Eta  config       
+         -> return $ Eta.etaX   profile config kenv tenv xx
+
+        Prune             
+         -> return $ pruneX     profile kenv tenv xx
 
         Forward          
          -> let config  = Forward.Config (const FloatAllow) False
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
@@ -10,9 +10,9 @@
 
           -- * Transform Results
         , TransformResult(..)
-	, TransformInfo(..)
-	, NoInformation
-	, resultDone)
+        , TransformInfo(..)
+        , NoInformation
+        , resultDone)
 where
 import DDC.Core.Simplifier.Result
 import DDC.Core.Transform.Rewrite.Rule
@@ -38,7 +38,7 @@
         -- | Keep applying a transform until it reports that further
         --   applications won't be helpful, bailing out after a maximum number
         --   of applications.
-	| Fix	Int		   (Simplifier s a n)
+        | Fix   Int                (Simplifier s a n)
 
 
 instance Monoid (Simplifier s a n) where
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
@@ -16,7 +16,7 @@
 
           -- * Compound recipies
         , anormalize
-	, rewriteSimp)
+        , rewriteSimp)
 where
 import DDC.Core.Simplifier.Base
 import DDC.Core.Transform.Namify
@@ -104,7 +104,7 @@
 rewriteSimp
         :: Int                          -- ^ Maximum number of iterations.
         -> NamedRewriteRules a n        -- ^ Rewrite rules to apply.
-	-> Simplifier s a n
+        -> Simplifier s a n
 
 rewriteSimp maxIters rules
  = let  rewrite = Trans $ Rewrite rules
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
@@ -12,8 +12,8 @@
 import Data.List
 import Data.Set                         (Set)
 import qualified Data.Set               as Set
-import qualified Data.Map               as Map
 
+
 -- | Rewrite all binders in a thing to anonymous form.
 anonymizeX :: (Ord n, AnonymizeX c) => c n -> c n
 anonymizeX xx
@@ -27,8 +27,8 @@
  --   The stacks contains existing anonymous binders that we have entered into,
  --   and named binders that we have rewritten. All bound occurrences of variables
  --   will be replaced by references into these stacks.
- anonymizeWithX 
-        :: forall n. Ord n 
+ anonymizeWithX
+        :: forall n. Ord n
         => Set n        -- ^ Don't anonymize level-0 binders with these names.
         -> [Bind n]     -- ^ Stack for Spec binders (level-1).
         -> [Bind n]     -- ^ Stack for Data and Witness binders (level-0).
@@ -36,12 +36,12 @@
 
 instance AnonymizeX (Module a) where
  anonymizeWithX keep kstack tstack mm@ModuleCore{}
-  = let 
-        -- We need to keep exported names, 
+  = let
+        -- We need to keep exported names,
         -- because the export list can't deal with anonymous binders.
-        keep'   = Set.union keep 
-                        $ Set.fromList 
-                        $ Map.keys $ moduleExportTypes mm
+        keep'   = Set.union keep
+                        $ Set.fromList
+                        $ map fst $ moduleExportTypes mm
 
         x'      = anonymizeWithX keep' kstack tstack (moduleBody mm)
 
@@ -54,9 +54,9 @@
     let down = anonymizeWithX keep kstack tstack
     in case xx of
         XVar _ UPrim{}  -> xx
-        XCon{}          -> xx      
+        XCon{}          -> xx
 
-        XVar a u@(UName{})       
+        XVar a u@(UName{})
          |  Just ix      <- findIndex (boundMatchesBind u) tstack
          -> XVar a (UIx ix)
 
@@ -74,14 +74,14 @@
             in  XLam a b'   (anonymizeWithX keep kstack tstack' x)
 
         XLet a lts x
-         -> let (kstack', tstack', lts')  
+         -> let (kstack', tstack', lts')
                  = pushAnonymizeLets keep kstack tstack lts
             in  XLet a lts' (anonymizeWithX keep kstack' tstack' x)
 
-        XCase a x alts  -> XCase a  (down x) (map down alts)
-        XCast a c x     -> XCast a  (down c) (down x)
-        XType t         -> XType    (anonymizeWithT kstack t)
-        XWitness w      -> XWitness (down w)
+        XCase a x alts  -> XCase a    (down x) (map down alts)
+        XCast a c x     -> XCast a    (down c) (down x)
+        XType a t       -> XType a    (anonymizeWithT kstack t)
+        XWitness a w    -> XWitness a (down w)
 
 
 instance AnonymizeX (Cast a) where
@@ -92,7 +92,7 @@
         CastWeakenClosure xs    -> CastWeakenClosure (map down xs)
         CastPurify w            -> CastPurify        (down w)
         CastForget w            -> CastForget        (down w)
-        CastSuspend             -> CastSuspend
+        CastBox                 -> CastBox
         CastRun                 -> CastRun
 
 
@@ -111,7 +111,7 @@
 
 instance AnonymizeX (Witness a) where
  anonymizeWithX keep kstack tstack ww
-  = let down = anonymizeWithX keep kstack tstack 
+  = let down = anonymizeWithX keep kstack tstack
     in case ww of
         WVar a u@(UName _)
          |  Just ix      <- findIndex (boundMatchesBind u) tstack
@@ -127,24 +127,24 @@
 instance AnonymizeX Bind where
  anonymizeWithX _keep kstack _tstack bb
   = let t'      = anonymizeWithT kstack $ typeOfBind bb
-    in  replaceTypeOfBind t' bb 
+    in  replaceTypeOfBind t' bb
 
 
 -- Push ----------------------------------------------------------------------
--- | Push a binding occurrence of a level-0 on the stack, 
+-- | Push a binding occurrence of a level-0 on the stack,
 --   returning the anonyized binding occurrence and the new stack.
-pushAnonymizeBindX 
-        :: Ord n 
+pushAnonymizeBindX
+        :: Ord n
         => Set n        -- ^ Don't anonymize binders with these names.
         -> [Bind n]     -- ^ Stack for Spec binders (level-1)
         -> [Bind n]     -- ^ Stack for Value and Witness binders (level-0)
-        -> Bind n 
+        -> Bind n
         -> ([Bind n], Bind n)
 
 pushAnonymizeBindX keep kstack tstack b@(BName n _)
  | Set.member n keep
  = let  b'      = anonymizeWithX keep kstack tstack b
-   in  (tstack, b')
+   in   (tstack, b')
 
 pushAnonymizeBindX keep kstack tstack b@BNone{}
  = let  b'      = anonymizeWithX keep kstack tstack b
@@ -158,15 +158,15 @@
    in   (tstack', BAnon t')
 
 
--- | Push a binding occurrence on the stack, 
+-- | Push a binding occurrence on the stack,
 --   returning the anonyized binding occurrence and the new stack.
 --  Used in the definition of `anonymize`.
-pushAnonymizeBindXs 
-        :: Ord n 
+pushAnonymizeBindXs
+        :: Ord n
         => Set n        -- ^ Don't anonymize binders with these names.
         -> [Bind n]     -- ^ Stack for Spec binders (level-1)
         -> [Bind n]     -- ^ Stack for Value and Witness binders (level-0)
-        -> [Bind n] 
+        -> [Bind n]
         -> ([Bind n], [Bind n])
 
 pushAnonymizeBindXs keep kstack tstack bs
@@ -175,12 +175,12 @@
         tstack bs
 
 
-pushAnonymizeLets 
-        :: Ord n 
+pushAnonymizeLets
+        :: Ord n
         => Set n
-        -> [Bind n] 
-        -> [Bind n] 
-        -> Lets a n 
+        -> [Bind n]
+        -> [Bind n]
+        -> Lets a n
         -> ([Bind n], [Bind n], Lets a n)
 
 pushAnonymizeLets keep kstack tstack lts
@@ -190,17 +190,17 @@
                 (tstack', b')   = pushAnonymizeBindX keep kstack tstack b
             in  (kstack, tstack', LLet b' x')
 
-        LRec bxs 
+        LRec bxs
          -> let (bs, xs)        = unzip bxs
                 (tstack', bs')  = pushAnonymizeBindXs keep kstack tstack   bs
                 xs'             = map (anonymizeWithX keep kstack tstack') xs
                 bxs'            = zip bs' xs'
             in  (kstack, tstack', LRec bxs')
 
-        LLetRegions b bs
+        LPrivate b mt bs
          -> let (kstack', b')   = mapAccumL pushAnonymizeBindT kstack b
                 (tstack', bs')  = pushAnonymizeBindXs keep kstack' tstack bs
-            in  (kstack', tstack', LLetRegions b' bs')
+            in  (kstack', tstack', LPrivate b' mt bs')
 
         LWithRegion{}
          -> (kstack, tstack, lts)
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
@@ -10,16 +10,17 @@
 import DDC.Base.Pretty
 import DDC.Core.Collect
 import DDC.Core.Exp
+import DDC.Core.Fragment
 import DDC.Core.Predicates
 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)
-import DDC.Type.Env                     (Env)
+import Control.Monad.Writer             (Writer, runWriter, tell)
+import Data.Monoid                      (Monoid, mempty, mappend)
+import Data.Typeable                    (Typeable)
+import DDC.Type.Env                     (KindEnv, TypeEnv)
 import DDC.Type.Compounds
 import qualified DDC.Type.Env           as Env
 import qualified Data.Set               as Set
@@ -92,14 +93,15 @@
 betaReduce  
         :: forall (c :: * -> * -> *) a n 
         .  (Ord n, TransformUpMX (Writer Info) c)
-        => Config
-        -> c a n 
+        => Profile n    -- ^ Language profile.
+        -> Config       -- ^ Beta transform config.
+        -> c a n        -- ^ Thing to transform.
         -> TransformResult (c a n)
 
-betaReduce config x
+betaReduce profile config x
  = {-# SCC betaReduce #-}
    let (x', info) = runWriter
-		  $ transformUpMX (betaReduce1 config) Env.empty Env.empty x
+                  $ transformUpMX (betaReduce1 profile config) Env.empty Env.empty x
 
        -- Check if any actual work was performed
        progress 
@@ -108,10 +110,10 @@
                  -> (ty + wit + val + lets') > 0
 
    in  TransformResult
-	{ result   	 = x'
+        { result         = x'
         , resultAgain    = progress
-	, resultProgress = progress
-	, resultInfo	 = TransformInfo info }
+        , resultProgress = progress
+        , resultInfo     = TransformInfo info }
 
 
 -- | Do a single beta reduction for this application.
@@ -124,21 +126,34 @@
 --    
 betaReduce1
         :: Ord n
-        => Config
-        -> Env n
-        -> Env n
-        -> Exp a n
+        => Profile n    -- ^ Language profile.
+        -> Config       -- ^ Beta tranform config.
+        -> KindEnv n    -- ^ Current kind environment.
+        -> TypeEnv n    -- ^ Current type environment.
+        -> Exp a n      -- ^ Expression to transform.
         -> Writer Info (Exp a n)
 
-betaReduce1 config _kenv tenv xx
+betaReduce1 profile config _kenv tenv xx
  = let  ret info x = tell info >> return x
+
+        -- If we're using closure types then when we perform a beta-reduction:
+        --  (\v. X1) X2 => X1[X2/v] then we need to weaken the closure if the 
+        -- body expression X1 does not reference 'v'.
+        weakenClosure a usesBind fvs2 xWeak x
+         | featuresTrackedClosures $ profileFeatures profile 
+         , not (usesBind || Set.null fvs2)
+         = XCast a (CastWeakenClosure [xWeak]) x
+
+         | otherwise
+         = x
+
    in case xx of
 
         -- Substitute type arguments into type abstractions.
         --  If the type argument of the redex does not appear as an 
         --  argument of the result then we need to add a closure weakening
         --  for the case where t2 was a region variable or handle.
-        XApp a (XLAM _ b11 x12) (XType t2)
+        XApp a (XLAM _ b11 x12) (XType a2 t2)
          | isRegionKind $ typeOfBind b11
          -> let sup             = support Env.empty Env.empty x12
 
@@ -152,28 +167,23 @@
                 fvs2            = freeT Env.empty t2
 
             in  ret mempty { infoTypes = 1}
-                 $ if usesBind || Set.null fvs2
-                    then substituteTX b11 t2 x12
-                    else XCast a (CastWeakenClosure [XType t2])
-                        $ substituteTX b11 t2 x12
+                 $ weakenClosure a usesBind fvs2 (XType a2 t2)
+                 $ substituteTX b11 t2 x12
 
         -- Substitute type arguments into type abstractions,
         --  Where the argument is not a region type.
-        XApp _ (XLAM _ b11 x12) (XType t2)
+        XApp _ (XLAM _ b11 x12) (XType _ t2)
          -> ret mempty { infoTypes = 1 }
                  $ substituteTX b11 t2 x12
 
         -- Substitute witness arguments into witness abstractions.
-        XApp a (XLam _ b11 x12) (XWitness w2)
+        XApp a (XLam _ b11 x12) (XWitness a2 w2)
          -> let usesBind        = any (flip boundMatchesBind b11)
                                 $ Set.toList $ freeX tenv x12
                 fvs2            = freeX Env.empty w2
             in  ret mempty { infoWits = 1 }
-                 $ if usesBind || Set.null fvs2
-                    then substituteWX b11 w2 x12
-                    else XCast a (CastWeakenClosure [XWitness w2])
-                       $ substituteWX b11 w2 x12
-
+                 $ weakenClosure a usesBind fvs2 (XWitness a2 w2)
+                 $ substituteWX b11 w2 x12
 
         -- Substitute value arguments into value abstractions.
         XApp a (XLam _ b11 x12) x2
@@ -182,14 +192,12 @@
                                 $ Set.toList $ freeX tenv x12
                 fvs2            = freeX Env.empty x2
             in  ret mempty { infoValues = 1 }
-                 $ if usesBind || Set.null fvs2
-                    then substituteXX b11 x2 x12
-                    else XCast a (CastWeakenClosure [x2])
-                       $ substituteXX b11 x2 x12
+                 $ weakenClosure a usesBind fvs2 x2
+                 $ substituteXX b11 x2 x12
 
          | configBindRedexes config
          -> ret mempty { infoValuesLetted  = 1 }
-	      $	XLet a (LLet b11 x2) x12
+              $ XLet a (LLet b11 x2) x12
 
          | otherwise
          -> ret mempty { infoValuesSkipped = 1 }
@@ -213,10 +221,10 @@
         XLam{}  -> True
         XLAM{}  -> True
 
-        XApp _ x1 (XType _)
+        XApp _ x1 XType{}
          -> canBetaSubstX x1
 
-        XApp _ x1 (XWitness _)
+        XApp _ x1 XWitness{}
          -> canBetaSubstX x1 
 
         _       -> False
diff --git a/DDC/Core/Transform/Boxing.hs b/DDC/Core/Transform/Boxing.hs
new file mode 100644
--- /dev/null
+++ b/DDC/Core/Transform/Boxing.hs
@@ -0,0 +1,459 @@
+-- | Manage representation of numeric values in a module.
+--
+--   We use three seprate versions of each numeric type.
+--      Nat#            Numeric index type.
+--      B# Nat#         Boxed representation type.
+--      U# Nat#         Unboxed representation type.
+--
+--   A numeric index type is the type of pure values like 23#, where "pure value"
+--   means the mathematical value, free from any considerations about how that 
+--   might be represented at runtime in the physical machine.
+--
+--   The Boxed and Unboxed representation types commit to a specific runtime
+--   representation, and have implications for runtime performance and space 
+--   usage of the compiled program.
+--
+--   The boxing transform takes an input program using just pure values and
+--   numeric index types, and refines it to a program that commits to particular
+--   representations of those values. In particular, we commit to a particular
+--   representation for function arguments and results, which makes the program
+--   adhere to a function calling convention that follow-on transformations
+--   to lower level languages (like Core Salt) can deal with.
+--
+--   This Boxing transform should do  just enough to make the code well-formed
+--   with respect to runtime representation. Demand-driven optimisations like
+--   local unboxing should be done in follow-on transformations.
+--
+--   We make the following representation commitments, so that the default
+--   representation is boxed.
+--
+--   Literal values are wrapped into their boxed representation:
+--        23# 
+--     => convert# [B# Nat#] [Nat#] 23#
+--
+--   Use unboxed versions of primitive operators:
+--        add# [Nat#] x y 
+--     => convert# [B# Nat#] [U# Nat#] 
+--                 (add# [U# Nat#] (convert# [U# Nat#] [B# Nat#] x)
+--                                 (convert# [U# Nat#] [B# Nat#] y))
+--
+--   Case scrutinees are unwrapped when matching against literal patterns:
+--        case x of { 0# -> ... }
+--     => case convert [B# Nat#] [Nat#] x of { 0# -> ... }
+--
+--   After performing this transformation the program is said
+--   to "use representational types", or be in "representational form".
+--
+--  [Note: Boxing and Partial Application]
+--  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+--  Unlike in Haskell, we do not allow explictly unboxed types in the source
+--  program because we don't want to deal with partial applications of
+--  functions to unboxed values. With our current setup we always have a version
+--  of each function that accepts boxed values, so we never need to do generic
+--  application involving unboxed values. Fast-path function specialisations
+--  that take unboxed parameters should be created separately, and not replace
+--  the existing slow-path, fully boxed version. Taking this approach is possible
+--  in a strict language because the boxed and unboxed values have the same 
+--  semantic meaning. Boxing of values does not imply "lifting" of the associated
+--  semantic domain.
+--
+module DDC.Core.Transform.Boxing
+        ( Rep           (..)
+        , Config        (..)
+        , Boxing        (..))
+where
+import DDC.Core.Compounds
+import DDC.Core.Module
+import DDC.Core.Exp
+import DDC.Type.Transform.Instantiate
+import DDC.Type.DataDef
+import Control.Monad
+
+
+---------------------------------------------------------------------------------------------------
+-- | Representation of the values of some type.
+data Rep
+        -- | Values of this type cannot be directly represented in the target
+        --   language. We need to use a boxed or unboxed representation instead.
+        = RepNone
+
+        -- | Type is represented in boxed form,
+        --   and thus can instantiate polymorphic types.
+        | RepBoxed     
+
+        -- | Type is represented in unboxed form,
+        --   and thus cannot instantiate polymorphic types.
+        | RepUnboxed
+        deriving (Eq, Ord, Show)
+
+
+data Config a n
+        = Config
+        { -- | Values of this type needs boxing to make the program
+          --   representational. This will only be passed types of kind Data.
+          configIsValueIndexType        :: Type n -> Bool
+
+          -- | Check if this is a boxed representation type.
+        , configIsBoxedType             :: Type n -> Bool
+
+          -- | Check if this is an unboxed representation type.
+        , configIsUnboxedType           :: Type n -> Bool
+
+          -- | Get the boxed version of some data type, if any.
+          --   This will only be passed types where typeNeedsBoxing returns True.
+        , configBoxedOfIndexType        :: Type n -> Maybe (Type n) 
+
+          -- | Get the unboxed version of some data type, if any.
+          --   This will only be passed types where typeNeedsBoxing returns True.
+        , configUnboxedOfIndexType      :: Type n -> Maybe (Type n) 
+
+          -- | Take the index type from a boxed type, if it is one.
+        , configIndexTypeOfBoxed        :: Type n -> Maybe (Type n)
+
+          -- | Take the index type from an unboxed type, if it is one.
+        , configIndexTypeOfUnboxed      :: Type n -> Maybe (Type n)
+
+          -- | Take the type of a literal name, if there is one.
+        , configValueTypeOfLitName      :: n -> Maybe (Type n)
+
+          -- | Take the type of a primitive operator name, if it is one.
+          --   The primops can be polytypic, but must have prenex rank-1 types.
+        , configValueTypeOfPrimOpName   :: n -> Maybe (Type n) 
+
+          -- | Take the type of a foreign function name, if it is one.
+          --   The function can be polymorphic, but must have a prenex rank-1 type.
+        , configValueTypeOfForeignName  :: n -> Maybe (Type n)
+
+          -- | Check if the primop with this name works on unboxed values
+          --   directly. Operators where this function returns False are assumed
+          --   to take boxed values for every argument.
+        , configNameIsUnboxedOp         :: n -> Bool 
+
+          -- | Wrap a value of the given index type.
+          --   This will only be passed types where typeNeedsBoxing returns True.
+        , configBoxedOfValue    :: a -> Exp a n -> Type n -> Maybe (Exp a n) 
+
+          -- | Unwrap a boxed value of the given index type.
+          --   This will only be passed types where typeNeedsBoxing returns True.
+        , configValueOfBoxed    :: a -> Exp a n -> Type n -> Maybe (Exp a n)
+
+          -- | Box an unboxed value of the given index type.
+          --   This will only be passed types where typeNeedsBoxing returns True.
+        , configBoxedOfUnboxed  :: a -> Exp a n -> Type n -> Maybe (Exp a n)
+
+          -- | Unbox a boxed value of the given index type.
+          --   This will only be passed types where typeNeedsBoxing returns True.
+        , configUnboxedOfBoxed  :: a -> Exp a n -> Type n -> Maybe (Exp a n) }
+
+
+---------------------------------------------------------------------------------------------------
+class Boxing (c :: * -> * -> *) where
+ -- | Rewrite a module to use explitit boxed and unboxed types.
+ boxing :: (Show n, Show a, Ord n)
+        => Config a n
+        -> c a n
+        -> c a n
+
+
+-- Module -----------------------------------------------------------------------------------------
+instance Boxing Module where
+ boxing config mm
+  = let 
+        -- Handle boxing in the types of exported values.
+        exportValues'
+         = map (boxingExportValue config) $ moduleExportValues mm
+         
+        -- Handle boxing in the types of imported values.
+        importValues'
+         = map (boxingImportValue config) $ moduleImportValues mm
+
+        -- Add locally imported foreign functions to the foreign function detector.
+        --  We want the original type here, before it has been passed through
+        --  the boxing transform.
+        typeOfForeignName n
+         -- The provided config already says this is foreign.
+         | Just t       <- configValueTypeOfForeignName config n  
+         = Just t
+
+         -- This is a locally imported C function.
+         | Just (ImportSourceSea _ t)
+                        <- lookup n (moduleImportValues mm)  
+         = Just t
+
+         | otherwise
+         = Nothing
+
+        -- Use our new foreign function detector in the config.
+        config'
+         = config
+         { configValueTypeOfForeignName  = typeOfForeignName }
+
+        -- Do the boxing transform.
+    in  mm  { moduleBody            = boxing config' (moduleBody mm) 
+            , moduleExportValues    = exportValues'
+            , moduleImportValues    = importValues'
+            , moduleDataDefsLocal   = map (boxingDataDef config') (moduleDataDefsLocal mm) }
+
+
+-- | Manage boxing in the type of an exported value.
+boxingExportValue
+        :: Config a n
+        -> (n, ExportSource n)
+        -> (n, ExportSource n)
+
+boxingExportValue config (n, esrc)
+ = case esrc of
+        ExportSourceLocal n' t
+         -> (n, ExportSourceLocal n' (boxingT config t))
+
+        ExportSourceLocalNoType{}
+         -> (n, esrc)
+
+
+-- | Manage boxing in the type of an imported value.
+boxingImportValue 
+        :: Config a n
+        => (n, ImportSource n)
+        -> (n, ImportSource n)
+
+boxingImportValue config (n, isrc)
+ = case isrc of
+        -- This shouldn't happen for values, but just pass it through.
+        ImportSourceAbstract _
+         -> (n, isrc)
+
+        -- Function imported from a DDC compiled module.
+        ImportSourceModule mn n' t
+         -> (n, ImportSourceModule mn n' (boxingT config t))
+
+        -- Value imported using the standard C calling convention.
+        ImportSourceSea str t
+         -> (n, ImportSourceSea str (boxingSeaT config t))
+
+
+-- Exp --------------------------------------------------------------------------------------------
+instance Boxing Exp where
+ boxing config xx
+  = let down = boxing config
+    in case xx of
+
+        -- Convert literals to their boxed representations.
+        XCon a dc
+         |  Just dcn    <- takeNameOfDaCon dc
+         ,  Just tLit   <- configValueTypeOfLitName config dcn
+         ,  configIsValueIndexType config tLit
+         ,  Just xx'    <- configBoxedOfValue  config a xx tLit
+         -> xx'
+
+        -- When applying a primop that works on unboxed values, 
+        -- unbox its arguments and then rebox the result.
+        XApp a x1 x2
+         -- Split the application of a primop into its name and arguments.
+         -- The arguments here include type arguments as well.
+         | Just (xFn, tPrim, xsArgsAll) 
+                <- splitUnboxedOpApp config xx
+         -> let 
+                -- Split off the type arguments.
+                (asArgs, tsArgs) = unzip $ [(a', t) | XType a' t <- xsArgsAll]
+                
+                -- For each type argument, if we know how to create the unboxed version
+                -- then do so. If this is wrong then the type checker will catch it later.
+                getTypeUnboxed t
+                 | Just t'      <- configUnboxedOfIndexType config t  
+                                = t'                
+                 | otherwise    = t 
+
+                tsArgsUnboxed   = map getTypeUnboxed tsArgs
+                
+                -- Instantiate the type to work out which arguments need to be unboxed,
+                -- and which we can leave as-is. 
+                Just tPrimInstUnboxed   = instantiateTs tPrim tsArgsUnboxed
+                (tsArgsInstUnboxed, tResultInstUnboxed)
+                                        = takeTFunArgResult tPrimInstUnboxed
+
+                -- Unboxing arguments to the function.
+                xsArgs  = drop (length tsArgs) xsArgsAll
+
+            in if -- We must end up with a type of each argument.
+                  -- If not then the primop is partially applied or something else is wrong.
+                  -- The Tetra to Salt conversion will give a proper error message
+                  -- if the primop is indeed partially applied.
+                  not (length xsArgs == length tsArgsInstUnboxed)
+                   then XApp a (down x1) (down x2)
+
+                   -- We got a type for each argument, so the primop is fully applied
+                   -- and we can do the boxing/unboxing transform.
+                   else let xsArgs' 
+                             = [ unboxExp config a tArgInst (down xArg)
+                                  | xArg      <- xsArgs
+                                  | tArgInst  <- tsArgsInstUnboxed ]
+                        in  boxExp config a tResultInstUnboxed
+                                $ xApps a xFn  (  [XType a' t  | t  <- tsArgsUnboxed
+                                                        | a' <- asArgs]
+                                                ++ xsArgs')
+
+        -- Unrap scrutinees when matching against literal patterns.
+        XCase a xScrut alts
+         | p : _        <- [ p  | AAlt (PData p@DaConPrim{} []) _ <- alts]
+         , Just tLit    <- configValueTypeOfLitName config (daConName p)
+         , configIsValueIndexType config tLit
+         , Just xScrut' <- configValueOfBoxed  config a (down xScrut) tLit
+         -> XCase a xScrut' (map down alts)
+
+        -- Boilerplate
+        XVar{}          -> xx
+        XCon{}          -> xx
+        XLAM a b x      -> XLAM  a b (down x)
+        XLam a b x      -> XLam  a (boxingB config b) (down x)
+        XApp a x1 x2    -> XApp  a (down x1)  (down x2)
+        XLet a lts x    -> XLet  a (down lts) (down x)
+        XCase a x alts  -> XCase a (down x)   (map down alts)
+        XCast a c x     -> XCast a c (down x)
+        XType a t       -> XType a (boxingT config t)
+        XWitness{}      -> xx
+
+
+-- | Box an expression that produces a value.
+boxExp :: Config a n -> a -> Type n -> Exp a n -> Exp a n
+boxExp config a t xx
+        | configIsValueIndexType config t
+        , Just x'      <- configBoxedOfUnboxed config a xx t
+        = x'
+
+        | configIsUnboxedType config t
+        , Just tIdx    <- configIndexTypeOfUnboxed config t
+        , Just x'      <- configBoxedOfUnboxed config a xx tIdx
+        = x'
+
+        | otherwise
+        = xx
+
+
+-- | Unbox an expression that produces a boxed value.
+unboxExp :: Config a n -> a -> Type n -> Exp a n -> Exp a n
+unboxExp config a t xx
+        | configIsValueIndexType config t
+        , Just x'      <- configUnboxedOfBoxed     config a xx t
+        = x'
+
+        | configIsUnboxedType config t
+        , Just tIdx    <- configIndexTypeOfUnboxed config t
+        , Just x'      <- configUnboxedOfBoxed     config a xx tIdx
+        = x'
+
+        | otherwise
+        = xx
+
+
+-- | If this is an application of some primitive operator or foreign function that 
+--   works on unboxed values then split it into the function and arguments.
+--
+--   The arguments returned include type arguments as well.
+splitUnboxedOpApp
+        :: Config a n
+        -> Exp a n 
+        -> Maybe (Exp a n, Type n, [Exp a n])
+
+splitUnboxedOpApp config xx
+ = case xx of
+        XApp{}
+         | Just (n, xsArgsAll)  <- takeXPrimApps xx
+         , Just (xFn, _)        <- takeXApps     xx
+         , configNameIsUnboxedOp config n
+         , Just tPrim           <- configValueTypeOfPrimOpName config n
+         -> Just (xFn, tPrim, xsArgsAll)
+
+        XApp{}
+         | Just (xFn@(XVar _ (UName n)), xsArgsAll)
+                                <- takeXApps xx
+         , Just tForeign        <- configValueTypeOfForeignName config n
+         -> Just (xFn, tForeign, xsArgsAll)
+
+        _ -> Nothing
+
+
+-- Lets -------------------------------------------------------------------------------------------
+instance Boxing Lets where
+ boxing config lts
+  = let down    = boxing config
+    in case lts of
+        LLet b x
+         -> let b'      = boxingB config b
+                x'      = down x
+            in  LLet b' x'
+
+        LRec bxs
+         -> let bxs'    = [(boxingB config b, down x) 
+                                | (b, x) <- bxs]
+            in  LRec bxs'
+
+        LPrivate{}      -> lts
+        LWithRegion{}   -> lts
+
+
+-- Alt --------------------------------------------------------------------------------------------
+instance Boxing Alt where
+ boxing config alt
+  = case alt of
+        AAlt PDefault x 
+         -> AAlt PDefault (boxing config x)
+
+        AAlt (PData dc bs) x
+         -> AAlt (PData dc (map (boxingB config) bs)) (boxing config x)
+
+
+---------------------------------------------------------------------------------------------------
+-- | Manage boxing in a Bind.
+boxingB :: Config a n -> Bind n -> Bind n
+boxingB config bb
+ = case bb of
+        BAnon t         -> BAnon   (boxingT config t)
+        BName n t       -> BName n (boxingT config t)
+        BNone t         -> BNone   (boxingT config t)
+
+
+-- | Manage boxing in a Type.
+boxingT :: Config a n -> Type n -> Type n
+boxingT config tt
+  | configIsValueIndexType config tt
+  , Just tResult        <- configBoxedOfIndexType config tt
+  = tResult
+
+  | otherwise
+  = let down = boxingT config
+    in case tt of
+        TVar{}          -> tt
+        TCon{}          -> tt
+        TForall b t     -> TForall b (down t)
+        TApp t1 t2      -> TApp (down t1) (down t2)
+        TSum{}          -> tt
+
+
+-- | Manage boxing in the type of a C value.
+boxingSeaT :: Config a n -> Type n -> Type n
+boxingSeaT config tt
+  | configIsValueIndexType config tt
+  , Just tResult        <- configUnboxedOfIndexType config tt
+  = tResult
+
+  | otherwise
+  = let down = boxingSeaT config
+    in case tt of
+        TVar{}          -> tt
+        TCon{}          -> tt
+        TForall b t     -> TForall b (down t)
+        TApp t1 t2      -> TApp (down t1) (down t2)
+        TSum{}          -> tt
+
+-- | Manage boxing in a data type definition.
+boxingDataDef :: Config a n -> DataDef n -> DataDef n
+boxingDataDef config def@DataDef{}
+        = def { dataDefCtors = liftM (map (boxingDataCtor config)) (dataDefCtors def) }
+
+
+-- | Manage boxing in a data constructor definition.
+boxingDataCtor :: Config a n -> DataCtor n -> DataCtor n    
+boxingDataCtor config ctor@DataCtor{}
+        = ctor 
+        { dataCtorFieldTypes   = map (boxingT config) (dataCtorFieldTypes ctor)
+        , dataCtorResultType   = boxingT config (dataCtorResultType ctor) }
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
@@ -40,8 +40,8 @@
  = let  
         -- Bubble the expression, yielding any casts that floated out
         -- to top-level.
-        (cs, x')        = bubble kenv tenv x
-        Just a          = takeAnnotOfExp x'
+        (cs, x') = bubble kenv tenv x
+        a        = annotOfExp x'
 
         -- Reattach top-level casts.
    in   dropAllCasts kenv tenv a cs x'
@@ -124,7 +124,7 @@
         -- but we can float the others further outwards.
         LLet b x
          -> let (cs, x')        = bubble kenv tenv x
-                Just a          = takeAnnotOfExp x'
+                a               = annotOfExp x'
                 (cs', xc')      = dropCasts kenv tenv a [] [b] cs x'
             in  (cs', LLet b xc')
 
@@ -135,14 +135,14 @@
 
                 bubbleRec (b, x)
                  = let  (cs, x') = bubble kenv tenv' x
-                        Just a   = takeAnnotOfExp x'
+                        a        = annotOfExp x'
                    in   (b, dropAllCasts kenv tenv' a cs x')
 
                 bxs'            = map bubbleRec bxs
 
             in  ([], LRec bxs')
 
-        LLetRegions{}           -> ([], lts)
+        LPrivate{}              -> ([], lts)
         LWithRegion{}           -> ([], lts)
 
 
@@ -158,7 +158,7 @@
  -- variables bound by the pattern.
  bubble kenv tenv (AAlt p x)
   = let bs              = bindsOfPat p
-        Just a          = takeAnnotOfExp x'
+        a               = annotOfExp x'
         tenv'           = Env.extends bs tenv
         (cs, x')        = bubble kenv tenv' x
         (csUp, xcHere)  = dropCasts kenv tenv' a [] bs cs x'
@@ -252,8 +252,8 @@
 
         (vsSp, vsDa)      = eat Set.empty Set.empty xx
 
-   in   [XType (TVar u) | u <- Set.toList vsSp]
-     ++ [XVar a u       | u <- Set.toList vsDa, keepBound kenv tenv u]
+   in   [XType a (TVar u) | u <- Set.toList vsSp]
+     ++ [XVar a u         | u <- Set.toList vsDa, keepBound kenv tenv u]
 
 
 -- | When packing vars given to a closure weakening, we only need to keep
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
@@ -78,7 +78,7 @@
         LLet b x   -> (us, LLet b (down x))
         LRec bs    -> (us, LRec $ map (second down) bs)
 
-        LLetRegions brs bws
+        LPrivate brs mt bws
          |  urs@(_:_) <- takeSubstBoundsOfBinds brs
          -> let 
                 -- Mutable regions bound here.
@@ -97,7 +97,7 @@
                                 ++ zip        urs  ursTail
 
             in  ( us ++ urs
-                , LLetRegions brs $ bws ++ distinctWits ++ constWits )
+                , LPrivate brs mt $ bws ++ distinctWits ++ constWits )
 
         _          -> (us, lts)
 
diff --git a/DDC/Core/Transform/Eta.hs b/DDC/Core/Transform/Eta.hs
--- a/DDC/Core/Transform/Eta.hs
+++ b/DDC/Core/Transform/Eta.hs
@@ -72,12 +72,12 @@
 -- | Eta-transform expressions in a module.
 etaModule
         :: (Ord n, Show n, Pretty n, Show a)
-        => Config
-        -> Profile n
+        => Profile n
+        -> Config
         -> Module a n
         -> TransformResult (Module a n)
 
-etaModule config profile mm
+etaModule profile config  mm
  = let  cconfig = Check.configOfProfile profile
         kenv'   = Env.union (profilePrimKinds profile) (moduleKindEnv mm)
         tenv'   = Env.union (profilePrimTypes profile) (moduleTypeEnv mm)
@@ -102,14 +102,14 @@
 
 -- | Eta-transform an expression.
 etaX    :: (Ord n, Show n, Show a, Pretty n)
-        => Config               -- ^ Eta-transform config.
-        -> Profile n            -- ^ Language profile.
+        => Profile n            -- ^ Language profile.
+        -> Config               -- ^ Eta-transform config.
         -> KindEnv n            -- ^ Kind environment.
         -> TypeEnv n            -- ^ Type environment.
         -> Exp a n              -- ^ Expression to transform.
         -> TransformResult (Exp a n)
 
-etaX config profile kenv tenv xx
+etaX profile config kenv tenv xx
  = let  cconfig = Check.configOfProfile profile
         kenv'   = Env.union (profilePrimKinds profile) kenv
         tenv'   = Env.union (profilePrimTypes profile) tenv
@@ -219,7 +219,7 @@
                           $  map snd bxs
                 return    $ LRec (zip bs xs')
 
-        LLetRegions{}   -> return lts
+        LPrivate{}      -> return lts
         LWithRegion{}   -> return lts
 
 
@@ -281,7 +281,7 @@
 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))]) 
+                        (args ++ [XType a (TVar (UIx depth1))]) 
                         ts
                         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
@@ -75,7 +75,7 @@
 --       Maybe use a follow on transform to reduce the lifetime again.
 --
 flatten1 (XLet a1 (LLet b1
-            inner@(XLet a2 (LLetRegions b2 bs2) x2))
+            inner@(XLet a2 (LPrivate b2 mt bs2) x2))
                x1)
  | all isBName b2
  = flatten1
@@ -86,7 +86,7 @@
  | otherwise
  = let  x1'     = liftAcrossT []   b2
                 $ liftAcrossX [b1] bs2 x1
-   in   XLet a2 (LLetRegions b2 bs2) 
+   in   XLet a2 (LPrivate b2 mt bs2) 
       $ flatten1
       $ XLet a1 (LLet (zapX b1) x2) 
              x1'
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
@@ -18,11 +18,11 @@
 import DDC.Core.Compounds
 import Data.Map                 (Map)
 import Control.Monad
-import Control.Monad.Writer	(Writer, runWriter, tell)
-import Data.Monoid		(Monoid, mempty, mappend)
+import Control.Monad.Writer     (Writer, runWriter, tell)
+import Data.Monoid              (Monoid, mempty, mappend)
 import Data.Typeable
 import qualified Data.Map                               as Map
-import qualified DDC.Core.Transform.SubstituteXX	as S
+import qualified DDC.Core.Transform.SubstituteXX        as S
 
 -------------------------------------------------------------------------------
 -- | Summary of number of bindings floated.
@@ -103,17 +103,17 @@
 
 forwardX profile config xx
  = let  (x',info) = runWriter
-		  $ forwardWith profile config Map.empty
-		  $ usageX xx
+                  $ forwardWith profile config Map.empty
+                  $ usageX xx
 
         progress (ForwardInfo _ s f) 
                 = s + f > 0
 
    in  TransformResult
-        { result	 = x'
+        { result         = x'
         , resultProgress = progress info
         , resultAgain    = False
-        , resultInfo	 = TransformInfo info }
+        , resultInfo     = TransformInfo info }
 
 
 -------------------------------------------------------------------------------
@@ -131,20 +131,22 @@
  forwardWith profile config bindings 
         (ModuleCore
                 { moduleName            = name
-                , moduleExportKinds     = exportKinds
                 , moduleExportTypes     = exportTypes
-                , moduleImportKinds     = importKinds
+                , moduleExportValues    = exportValues
                 , moduleImportTypes     = importTypes
+                , moduleImportValues    = importValues
+                , moduleDataDefsLocal   = dataDefsLocal
                 , moduleBody            = body })
 
-  = do	body' <- forwardWith profile config bindings body
-	return ModuleCore
-		{ moduleName            = name
-		, moduleExportKinds     = exportKinds
-		, moduleExportTypes     = exportTypes
-		, moduleImportKinds     = importKinds
-		, moduleImportTypes     = importTypes
-		, moduleBody            = body' }
+  = do  body' <- forwardWith profile config bindings body
+        return ModuleCore
+                { moduleName            = name
+                , moduleExportTypes     = exportTypes
+                , moduleExportValues    = exportValues
+                , moduleImportTypes     = importTypes
+                , moduleImportValues    = importValues
+                , moduleDataDefsLocal   = dataDefsLocal
+                , moduleBody            = body' }
 
 
 instance Forward Exp where
@@ -155,10 +157,10 @@
         XVar a u@(UName n)
          -> case Map.lookup n bindings of
                 Just xx'        -> do
-		    tell mempty { infoSubsts = 1 }
-		    return xx'
+                    tell mempty { infoSubsts = 1 }
+                    return xx'
                 Nothing         ->
-		    return $ XVar (snd a) u
+                    return $ XVar (snd a) u
 
         XVar a u        -> return $ XVar (snd a) u
         XCon a u        -> return $ XCon (snd a) u
@@ -220,10 +222,10 @@
         XLet (_, a') lts 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 (reannotate snd w)
+        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 a t       -> return (XType    (snd a) t)
+        XWitness a w    -> return (XWitness (snd a) (reannotate snd w))
 
 
 filterUsedInCasts :: [Used] -> [Used]
@@ -240,7 +242,7 @@
         CastWeakenClosure xs    -> liftM    CastWeakenClosure (mapM down xs)
         CastPurify w            -> return $ CastPurify (reannotate snd w)
         CastForget w            -> return $ CastForget (reannotate snd w)
-        CastSuspend             -> return $ CastSuspend
+        CastBox                 -> return $ CastBox
         CastRun                 -> return $ CastRun
 
 
@@ -255,10 +257,10 @@
          -> liftM LRec
          $  mapM (\(b,x) 
                     -> do x' <- down x
-			  return (b, x')) 
+                          return (b, x')) 
             bxs
 
-        LLetRegions b bs -> return $ LLetRegions b bs
+        LPrivate b mt bs -> return $ LPrivate b mt bs
         LWithRegion b    -> return $ LWithRegion b
 
 
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
@@ -64,7 +64,7 @@
     in case lts of
         LLet b x        -> LLet b (enter b x)
         LRec bxs        -> LRec [(b, enter b x) | (b, x) <- bxs]
-        LLetRegions{}   -> lts
+        LPrivate{}      -> 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
@@ -143,21 +143,21 @@
                 x2'             <- namify tnam xnam' x2
                 return $ XLet a (LRec (zip bs' xs')) x2'
 
-        XLet a (LLetRegions b bs) x2
+        XLet a (LPrivate b mt bs) x2
          -> do  (tnam', b')     <- pushTs tnam b
                 (xnam', bs')    <- pushXs tnam' xnam bs
                 x2'             <- namify tnam' xnam' x2
-                return $ XLet a (LLetRegions b' bs') x2'
+                return $ XLet a (LPrivate b' mt bs') x2'
 
         XLet a (LWithRegion u) x2
          -> do  u'              <- rewriteX tnam xnam u
                 x2'             <- down x2
                 return  $ XLet a (LWithRegion u') x2'
 
-        XCase a x1 alts -> liftM3 XCase    (return a) (down x1)  (mapM down alts)
-        XCast a c  x    -> liftM3 XCast    (return a) (down c)   (down x)
-        XType t         -> liftM  XType    (down t)
-        XWitness w      -> liftM  XWitness (down w)
+        XCase a x1 alts -> liftM2 (XCase    a) (down x1)  (mapM down alts)
+        XCast a c  x    -> liftM2 (XCast    a) (down c)   (down x)
+        XType a t       -> liftM  (XType    a) (down t)
+        XWitness a w    -> liftM  (XWitness a) (down w)
 
 
 instance Namify (Alt a) where
@@ -182,7 +182,7 @@
 
         CastPurify w            -> liftM CastPurify (down w)
         CastForget w            -> liftM CastForget (down w)
-        CastSuspend             -> return CastSuspend
+        CastBox                 -> return CastBox
         CastRun                 -> return CastRun
 
 
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
@@ -27,11 +27,11 @@
 import qualified Data.Set                               as Set
 import qualified DDC.Type.Env                           as Env
 import qualified DDC.Core.Collect                       as C
-import qualified DDC.Core.Transform.SubstituteXX	as S
-import qualified DDC.Core.Transform.Trim               	as Trim
-import qualified DDC.Type.Compounds			as T
-import qualified DDC.Type.Sum				as TS
-import qualified DDC.Type.Transform.Crush		as T
+import qualified DDC.Core.Transform.SubstituteXX        as S
+import qualified DDC.Core.Transform.Trim                as Trim
+import qualified DDC.Type.Compounds                     as T
+import qualified DDC.Type.Sum                           as TS
+import qualified DDC.Type.Transform.Crush               as T
 
 
 -------------------------------------------------------------------------------
@@ -60,10 +60,10 @@
 -------------------------------------------------------------------------------
 -- | Erase pure let-bindings in a module that have no uses.
 pruneModule
-	:: (Show a, Show n, Ord n, Pretty n)
-	=> Profile n           -- ^ Profile of the language we're in
-	-> Module a n
-	-> Module a n
+        :: (Show a, Show n, Ord n, Pretty n)
+        => Profile n           -- ^ Profile of the language we're in
+        -> Module a n
+        -> Module a n
 
 pruneModule profile mm
          -- If the language fragment has untracked effects then we can't do
@@ -82,26 +82,26 @@
 
 -- | Erase pure let-bindings in an expression that have no uses.
 pruneX
-	:: (Show a, Show n, Ord n, Pretty n)
-	=> Profile n           -- ^ Profile of the language we're in
-	-> KindEnv n           -- ^ Kind environment
-	-> TypeEnv n           -- ^ Type environment
-	-> Exp a n
-	-> TransformResult (Exp a n)
+        :: (Show a, Show n, Ord n, Pretty n)
+        => Profile n           -- ^ Profile of the language we're in
+        -> KindEnv n           -- ^ Kind environment
+        -> TypeEnv n           -- ^ Type environment
+        -> Exp a n
+        -> TransformResult (Exp a n)
 
 pruneX profile kenv tenv xx
  = {-# SCC pruneX #-}
    let  
         (xx', info)
                 = transformTypeUsage profile kenv tenv
-	               (transformUpMX pruneTrans kenv tenv)
+                       (transformUpMX pruneTrans kenv tenv)
                        xx
 
         progress (PruneInfo r) 
                 = r > 0
 
    in TransformResult
-        { result	 = xx'
+        { result         = xx'
         , resultAgain    = progress info
         , resultProgress = progress info
         , resultInfo     = TransformInfo info }
@@ -114,17 +114,16 @@
 -- deadCodeTrans to actually erase dead bindings.
 --
 transformTypeUsage profile kenv tenv trans xx
- = case checkExp (configOfProfile profile) kenv tenv xx of
+ = case fst $ checkExp (configOfProfile profile) kenv tenv xx Recon of
         Right (xx1, _, _,_) 
          -> let xx2        = usageX xx1
                 (x', info) = runWriter (trans xx2)
                 x''        = reannotate (\(_, AnTEC { annotTail = a }) -> a) x'
             in  (x'', info)
 
-        Left err 
+        Left _
          -> error $  renderIndent
-         $  vcat [ text "DDC.Core.Transform.Prune: core type error"
-                 , ppr err ]
+         $  vcat [ text "ddc-coe-simpl.Prune: core type error" ]
 
 
 -------------------------------------------------------------------------------
@@ -135,11 +134,11 @@
 
 -- | Apply the dead-code transform to an annotated expression.
 pruneTrans
-	:: (Show a, Show n, Ord n, Pretty n)
-	=> KindEnv n
-	-> TypeEnv n
-	-> Exp (Annot a n) n
-	-> Writer PruneInfo 
+        :: (Show a, Show n, Ord n, Pretty n)
+        => KindEnv n
+        -> TypeEnv n
+        -> Exp (Annot a n) n
+        -> Writer PruneInfo 
                  (Exp (Annot a n) n)
 
 pruneTrans _ _ xx
@@ -170,7 +169,7 @@
         weakClo a x1 
          = CastWeakenClosure
          $ Trim.trimClosures a
-                (  (map (XType . TVar)
+                (  (map ((XType a) . TVar)
                         $ Set.toList
                         $ C.freeT Env.empty x1)
                 ++ (map (XVar a)
@@ -187,7 +186,7 @@
         BName n _
          -> case Map.lookup n um of
                 Just useds -> filterUsedInCasts useds == []
-        	Nothing	   -> True
+                Nothing    -> True
 
         BNone _ -> True
         _       -> False
@@ -211,12 +210,12 @@
  where
         contained (c : _args)
          = case c of
-                TCon (TyConSpec TcConAlloc)	-> True
-        	TCon (TyConSpec TcConDeepAlloc) -> True
-        	TCon (TyConSpec TcConRead)      -> True
+                TCon (TyConSpec TcConAlloc)     -> True
+                TCon (TyConSpec TcConDeepAlloc) -> True
+                TCon (TyConSpec TcConRead)      -> True
                 TCon (TyConSpec TcConHeadRead)  -> True
                 TCon (TyConSpec TcConDeepRead)  -> True
-        	_				-> False
+                _                               -> False
 
         contained [] = False
 
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
@@ -208,7 +208,7 @@
 
  = let  -- only get value-level bindings
         bs'     = filter (isBMValue . fst) bs
-        bas'    = lookupFromSubst bs' sub
+        bas'    = lookupFromSubst a bs' sub
 
         -- check if it looks like something has already been unfolded
         isUIx x = case x of 
@@ -221,7 +221,7 @@
 
         -- find kind-values and sub those in as well
         bsK'    = filter ((== BMSpec) . fst) bs
-        basK    = lookupFromSubst bsK' sub
+        basK    = lookupFromSubst a bsK' sub
 
         basK'   = concatMap (\(b,x) -> case X.takeXType x of
                                              Just t -> [(b,t)]
@@ -323,9 +323,9 @@
         (m, rest)       <- matchWithRule rule env f args RM.emptySubstInfo
 
         -- Check constraints, perform substitution and add weakens if necessary.
-        let Just a      = X.takeAnnotOfExp f
+        let a           = X.annotOfExp f
 
-        let bas2        = lookupFromSubst binds m
+        let bas2        = lookupFromSubst a binds m
         let rhs2        = A.anonymizeX rhs
         let (bas3,lets) = wrapLets a binds bas2
         let rhs3        = L.liftX (length lets) rhs2
@@ -410,7 +410,7 @@
 -- | Substitute type bindings into a type.
 substT :: Ord n => [(Bind n, Exp a n)] -> Type n -> Type n
 substT bas x 
- = let  sub     = [(b, t) | (b, XType t) <- bas ] 
+ = let  sub     = [(b, t) | (b, XType _ t) <- bas ] 
    in   S.substituteTs sub x
 
 
@@ -506,7 +506,7 @@
 
         -- Try to match against entire rule with no inlining.
         -- Eg (unbox (box 5))
-        | Just a        <- X.takeAnnotOfExp f
+        | a             <- X.annotOfExp f
         , lhs_full      <- XApp a (ruleLeft rule) hole 
         , rule_full     <- rule { ruleLeft = lhs_full, ruleLeftHole = Nothing}
         , Just subst    <- matchWithRule rule_full env f args sub
@@ -541,12 +541,14 @@
 --
 --    Eg: RULE [x : %] (x : Int x). ...
 -- 
-lookupFromSubst :: Ord n
-        => [(BindMode,Bind n)]
+lookupFromSubst 
+        :: Ord n
+        => a
+        -> [(BindMode,Bind n)]
         -> (Map n (Exp a n), Map n (Type n))
         -> [(Bind n, Exp a n)]
 
-lookupFromSubst bs m
+lookupFromSubst a1 bs m
  = let  bas  = catMaybes $ map (lookupX m) bs
    in   map (\(b, a) -> (A.anonymizeX b, A.anonymizeX a)) bas
    
@@ -556,7 +558,7 @@
 
         lookupX (_,tys) (BMSpec, b@(BName n _))
          | Just t <- Map.lookup n tys
-         = Just (b, XType t)
+         = Just (b, XType a1 t)
 
         lookupX _ _ = Nothing
 
diff --git a/DDC/Core/Transform/Rewrite/Disjoint.hs b/DDC/Core/Transform/Rewrite/Disjoint.hs
--- a/DDC/Core/Transform/Rewrite/Disjoint.hs
+++ b/DDC/Core/Transform/Rewrite/Disjoint.hs
@@ -6,9 +6,9 @@
 import DDC.Core.Exp
 import DDC.Type.Predicates
 import DDC.Type.Compounds
-import qualified DDC.Core.Transform.Rewrite.Env	as RE
-import qualified DDC.Type.Sum			as Sum
-import qualified DDC.Type.Transform.Crush	as TC
+import qualified DDC.Core.Transform.Rewrite.Env as RE
+import qualified DDC.Type.Sum                   as Sum
+import qualified DDC.Type.Transform.Crush       as TC
 
 
 -- | Check whether a disjointness property is true in the given
@@ -53,15 +53,15 @@
 --   Example:
 --   
 -- >  checkDisjoint
--- >	(Disjoint (Read r1 + Read r2) (Write r3))
--- >	[Distinct r1 r3, Distinct r2 r3]
+-- >    (Disjoint (Read r1 + Read r2) (Write r3))
+-- >    [Distinct r1 r3, Distinct r2 r3]
 -- >  = True
 --
 checkDisjoint
         :: (Ord n, Show n)
         => Type n               -- ^ Type of property we want
                                 --   eg @Disjoint e1 e2@
-        -> RE.RewriteEnv a n	-- ^ Environment we're rewriting in.
+        -> RE.RewriteEnv a n    -- ^ Environment we're rewriting in.
         -> Bool
 
 checkDisjoint c env
@@ -117,15 +117,15 @@
 --
 checkDistinct
     :: Ord n
-    => Type n			-- ^ Type of the property we want,
+    => Type n                   -- ^ Type of the property we want,
                                 --   eg @Distinct r1 r2@
-    -> RE.RewriteEnv a n	-- ^ Environment we're rewriting in.
+    -> RE.RewriteEnv a n        -- ^ Environment we're rewriting in.
     -> Bool
 
 checkDistinct c env
         -- It's of the form "Distinct r q"
         | (TCon (TyConWitness (TwConDistinct _)) : args)
-        	<- takeTApps c
+                <- takeTApps c
         = all (uncurry $ areDistinct env) (combinations args)
 
         | otherwise
@@ -186,7 +186,7 @@
                 concrete r
                  = case r of
                         UPrim _ _ -> True
-                        _	  -> RE.containsRegion r env
+                        _         -> RE.containsRegion r env
 
                 check w
                  | (TCon (TyConWitness (TwConDistinct _)) : args)
@@ -199,5 +199,5 @@
                 rgn b
                  = case b of
                     UPrim _ t   -> TCon (TyConBound b t)
-                    _	        -> TVar b
+                    _           -> TVar b
 
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
@@ -13,11 +13,11 @@
         , liftValue)
 where
 import DDC.Core.Exp
-import qualified DDC.Type.Exp			as T
-import qualified DDC.Type.Compounds		as T
-import qualified DDC.Type.Predicates		as T
-import qualified DDC.Type.Transform.LiftT	as L
-import qualified DDC.Core.Transform.LiftX	as L
+import qualified DDC.Type.Exp                   as T
+import qualified DDC.Type.Compounds             as T
+import qualified DDC.Type.Predicates            as T
+import qualified DDC.Type.Transform.LiftT       as L
+import qualified DDC.Core.Transform.LiftX       as L
 import Data.Maybe (fromMaybe, listToMaybe, isJust)
 
 
@@ -43,7 +43,7 @@
           -- | Assoc of known values
           --   If going to inline them, they must only reference de bruijn binds
           --   these are value-level bindings, so be careful lifting.
-        , defs	         :: [[RewriteDef a n]] }
+        , defs           :: [[RewriteDef a n]] }
         deriving (Show,Eq)
 
 
@@ -75,7 +75,7 @@
 --   If it's a letregion, remember the region's name and any witnesses.
 --
 extendLets :: Ord n => Lets a n -> RewriteEnv a n -> RewriteEnv a n
-extendLets (LLetRegions bs cs) renv
+extendLets (LPrivate bs _mt cs) renv
  = foldl (flip extend) (foldl extendB renv bs) cs
  where  
         extendB (env@RewriteEnv{witnesses = ws, letregions = rs}) b
@@ -91,13 +91,13 @@
                  -> env
 
         extend' b (r:rs') = (b:r) : rs'
-        extend' b []	   = [[b]]
+        extend' b []      = [[b]]
 
 extendLets (LLet b def) env
  = insertDef b (Just def') (liftValue b env)
  where  def' = case b of
-	         BAnon{} -> L.liftX 1 def
-        	 _	 -> def
+                 BAnon{} -> L.liftX 1 def
+                 _       -> def
 
 extendLets (LRec bs) env
  = foldl lift' env (map fst bs)
@@ -160,7 +160,7 @@
  = env { defs = extend' $ defs env }
  where  
         extend' (r:rs') = ((b,def):r) : rs'
-        extend' []	= [[(b,def)]]
+        extend' []      = [[(b,def)]]
 
 
 hasDef  :: (Ord n, L.MapBoundX (Exp a) n)
@@ -192,9 +192,9 @@
 
         match b' i ds
                 = fmap (fmap $ L.liftX i)
-		$ listToMaybe
-		$ map snd
-		$ filter (T.boundMatchesBind b' . fst) ds
+                $ listToMaybe
+                $ map snd
+                $ filter (T.boundMatchesBind b' . fst) ds
 
         orM (Just x) _  = Just x
         orM Nothing  y  = y
diff --git a/DDC/Core/Transform/Rewrite/Error.hs b/DDC/Core/Transform/Rewrite/Error.hs
--- a/DDC/Core/Transform/Rewrite/Error.hs
+++ b/DDC/Core/Transform/Rewrite/Error.hs
@@ -4,7 +4,7 @@
 where
 import DDC.Core.Exp
 import DDC.Core.Check                   ()
-import DDC.Type.Pretty
+import DDC.Core.Pretty
 import qualified DDC.Core.Check         as C
 
 
@@ -49,7 +49,8 @@
  ppr Rhs = text "rhs"
 
 
-instance (Show a, Pretty n, Show n, Eq n) => Pretty (Error a n) where
+instance (Pretty a, Show a, Pretty n, Show n, Eq n) 
+        => Pretty (Error a n) where
  ppr err
   = case err of
         ErrorTypeCheck s x e
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
@@ -12,12 +12,12 @@
 import Data.Set                                 (Set)
 import Data.Map                                 (Map)
 import qualified DDC.Type.Sum                   as Sum
-import qualified DDC.Type.Transform.AnonymizeT	as T
-import qualified DDC.Core.Transform.AnonymizeX	as T
-import qualified DDC.Core.Transform.Reannotate	as T
-import qualified DDC.Type.Equiv			as TE
-import qualified Data.Map			as Map
-import qualified Data.Set			as Set
+import qualified DDC.Type.Transform.AnonymizeT  as T
+import qualified DDC.Core.Transform.AnonymizeX  as T
+import qualified DDC.Core.Transform.Reannotate  as T
+import qualified DDC.Type.Equiv                 as TE
+import qualified Data.Map                       as Map
+import qualified Data.Set                       as Set
 
 
 -------------------------------------------------------------------------------
@@ -62,12 +62,12 @@
    Nothing -> return $ insertx n r m
    Just x  
     ->  -- Check if they're equal. Anonymize so names don't matter.
-	-- Reannotate so annotations are ignored.
-	let  x' = T.anonymizeX $ T.reannotate (const ()) x
-	     r' = T.anonymizeX $ T.reannotate (const ()) r
-	in if   x' == r'
-	   then Just m
-	   else Nothing
+        -- Reannotate so annotations are ignored.
+        let  x' = T.anonymizeX $ T.reannotate (const ()) x
+             r' = T.anonymizeX $ T.reannotate (const ()) r
+        in if   x' == r'
+           then Just m
+           else Nothing
 
 match m _ (XVar _ v1) (XVar _ v2)
  | v1 == v2      = Just m
@@ -76,19 +76,19 @@
  | c1 == c2      = Just m
 
 match m bs (XApp _ x11 x12) (XApp _ x21 x22)
- = do	m' <- match m bs x11 x21
-	match m' bs x12 x22
+ = do   m' <- match m bs x11 x21
+        match m' bs x12 x22
 
 match m bs (XCast _ c1 x1) (XCast _ c2 x2)
- | eqCast c1 c2	
+ | eqCast c1 c2 
  = match m bs x1 x2
 
-match (xs, tys) bs (XType t1) (XType t2)
- = do	tys' <- matchT t1 t2 bs tys
-	return (xs, tys')
+match (xs, tys) bs (XType _ t1) (XType _ t2)
+ = do   tys' <- matchT t1 t2 bs tys
+        return (xs, tys')
 
-match m _ (XWitness w1) (XWitness w2)
- | eqWit w1 w2	= return m
+match m _ (XWitness _ w1) (XWitness _ w2)
+ | eqWit w1 w2  = return m
 
 match _ _ _ _ 
  = Nothing
@@ -104,7 +104,7 @@
                 CastWeakenClosure clo   -> CastWeakenClosure $ map T.anonymizeX clo
                 CastPurify        wit   -> CastPurify        wit
                 CastForget        wit   -> CastForget wit
-                CastSuspend             -> CastSuspend
+                CastBox                 -> CastBox
                 CastRun                 -> CastRun
 
 
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
@@ -14,35 +14,35 @@
 -- Rewrite Rules ----------------------------------------------------------------
 {-
     [r1 r2 : %] (x : Int r1).
-	Const r1 =>
-	addInt [:r1 r2 r1:] x (0 [r2] ()) =
-	x
+        Const r1 =>
+        addInt [:r1 r2 r1:] x (0 [r2] ()) =
+        x
 -}
 -- | Parse a rewrite rule.
-pRule	:: Ord n 
+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 c
+ = do   bs       <- pRuleBinders c
+        (cs,lhs) <- pRuleCsLhs c
+        hole     <- pRuleHole c
+        pTok (KOp "=")
+        rhs      <- pExp c
 
-	return $ R.mkRewriteRule bs cs lhs hole rhs
+        return $ R.mkRewriteRule bs cs lhs hole rhs
 
 
 {-
 add_zero_r
     [r1 r2 : %] (x : Int r1).
-	Const r1 =>
-	addInt [:r1 r2 r1:] x (0 [r2] ()) =
-	x;
+        Const r1 =>
+        addInt [:r1 r2 r1:] x (0 [r2] ()) =
+        x;
 add_zero_l
     [r1 r2 : %] ...
         ;
 -}
 -- | Parse many rewrite rules.
-pRuleMany	
+pRuleMany       
         :: Ord n 
         => Context -> Parser n [(n,R.RewriteRule P.SourcePos n)]
 pRuleMany c
@@ -59,9 +59,9 @@
 
 pRuleBinders c
  = P.choice
- [ do	bs <- P.many1 (pBinders c)
-	pTok KDot
-	return $ concat bs
+ [ do   bs <- P.many1 (pBinders c)
+        pTok KDot
+        return $ concat bs
  , return []
  ]
 
@@ -71,14 +71,14 @@
         => Context -> Parser n ([Type n], Exp P.SourcePos n)
 pRuleCsLhs c
  = P.choice
- [ do	cs <- P.many1 $ P.try (do
-		cc <- pTypeApp c
-		pTok KArrowEquals
-		return cc)
-	lhs <- pExp c
-	return (cs,lhs)
- , do	lhs <- pExp c
-	return ([],lhs)
+ [ do   cs <- P.many1 $ P.try (do
+                cc <- pTypeApp c
+                pTok KArrowEquals
+                return cc)
+        lhs <- pExp c
+        return (cs,lhs)
+ , do   lhs <- pExp c
+        return ([],lhs)
  ]
 
 
@@ -87,10 +87,12 @@
         => Context -> Parser n (Maybe (Exp P.SourcePos n))
 pRuleHole c
  = P.optionMaybe
- $ do	pTok KBraceBra
-	e <- pExp c
-	pTok KBraceKet
-	return e
+ $ do   pTok KUnderscore
+        pTok KBraceBra
+        e <- pExp c
+        pTok KBraceKet
+        pTok KUnderscore
+        return e
 
 
 -- | Parse rewrite binders
@@ -118,9 +120,9 @@
         -> Parser n [(R.BindMode,Bind n)]
 
 pBindersBetween c bm bra ket
- = do	bra
+ = do   bra
         bs      <- P.many1 pBinder
-        pTok KColon
+        pTok (KOp ":")
         t       <- pType c
         ket
         return $ map (mk t) bs
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
@@ -21,10 +21,9 @@
 import DDC.Core.Pretty                          ()
 import DDC.Core.Collect
 import DDC.Core.Compounds
-import DDC.Type.Pretty                          ()
+import DDC.Core.Pretty                          ()
 import DDC.Type.Env                             (KindEnv, TypeEnv)
 import DDC.Base.Pretty
-import Control.Monad
 import qualified DDC.Core.Analysis.Usage        as U
 import qualified DDC.Core.Check                 as C
 import qualified DDC.Core.Collect               as C
@@ -197,7 +196,7 @@
 
         -- Build application from lhs and the hole so we can check its
         -- type against rhs
-        let Just a      = takeAnnotOfExp lhs
+        let a           = annotOfExp lhs
         let lhs_full    = maybe lhs (XApp a lhs) hole
 
         -- Check the full left hand side.
@@ -292,7 +291,7 @@
 
 checkExp defs kenv tenv side xx
  = let xx' = S.spreadX kenv tenv xx 
-   in  case C.checkExp defs kenv tenv xx' of
+   in  case fst $ C.checkExp defs kenv tenv xx' C.Recon of
         Left err  -> Left $ ErrorTypeCheck side xx' err
         Right rhs -> return rhs
 
@@ -306,9 +305,9 @@
         -> Either (Error a n) (Kind n)
 
 checkConstraint config kenv tt
- = case T.checkType config kenv tt of
+ = case T.checkSpec config kenv tt of
         Left _err               -> Left $ ErrorBadConstraint tt
-        Right k
+        Right (_, k)
          | T.isWitnessType tt   -> return k
          | otherwise            -> Left $ ErrorBadConstraint tt
 
@@ -386,16 +385,16 @@
         wiRight = supportWiVar supportRight
         spRight = supportSpVar supportRight
 
-        Just a  = takeAnnotOfExp lhs
+        a       = annotOfExp lhs
 
    in   Right 
          $  [XVar a u 
                 | u <- Set.toList $ daLeft `Set.difference` daRight ]
 
-         ++ [XWitness (WVar a u)
+         ++ [XWitness a (WVar a u)
                 | u <- Set.toList $ wiLeft `Set.difference` wiRight ]
 
-         ++ [XType (TVar u)
+         ++ [XType a (TVar u)
                 | u <- Set.toList $ spLeft `Set.difference` spRight ]
 
 
@@ -413,10 +412,10 @@
  where
   remove kenv _tenv x
 
-   | XType et   <- x
-   , Right k    <- T.checkType config kenv et
+   | XType a et     <- x
+   , Right (_, k) <- T.checkSpec config kenv et
    , T.isEffectKind k
-   = XType $ T.tBot T.kEffect
+   = XType a $ T.tBot T.kEffect
 
    | otherwise
    = x
@@ -469,14 +468,14 @@
         go x@(XLet _ _ _)       = Left $ ErrorNotFirstOrder x
         go x@(XCase _ _ _)      = Left $ ErrorNotFirstOrder x
         go (XCast _ _ x)        = go x
-        go (XType t)            = go_t t
-        go (XWitness _)         = return ()
+        go (XType a t)          = go_t a t
+        go (XWitness _ _)       = return ()
 
-        go_t (TVar _)           = return ()
-        go_t (TCon _)           = return ()
-        go_t t@(TForall _ _)    = Left $ ErrorNotFirstOrder (XType t)
-        go_t (TApp l r)         = go_t l >> go_t r
-        go_t (TSum _)           = return ()
+        go_t _ (TVar _)         = return ()
+        go_t _ (TCon _)         = return ()
+        go_t a t@(TForall _ _)  = Left $ ErrorNotFirstOrder (XType a t)
+        go_t a (TApp l r)       = go_t a l >> go_t a r
+        go_t _ (TSum _)         = return ()
 
 
 -- | Count how many times each binder is used in right-hand side.
@@ -487,8 +486,8 @@
         -> Either (Error a n) [(BindMode, Bind n)]
 
 countBinderUsage bs x
- = let  Just (U.UsedMap um)
-                = liftM fst $ takeAnnotOfExp $ U.usageX x
+ = let  U.UsedMap um
+                = fst $ annotOfExp $ U.usageX x
 
         get (BMValue _, BName n t)
          = (BMValue
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
@@ -23,6 +23,10 @@
         
           -- | Ensure the body of a let-expression is a variable.
         , configSnipLetBody     :: Bool
+
+          -- | Treat lambda abstractions as atomic, 
+          --   and don't snip them.
+        , configPreserveLambdas :: Bool 
         }
 
 
@@ -31,7 +35,8 @@
 configZero
         = Config
         { configSnipOverApplied = False
-        , configSnipLetBody     = False }
+        , configSnipLetBody     = False 
+        , configPreserveLambdas = False }
 
 
 -------------------------------------------------------------------------------
@@ -92,7 +97,7 @@
    in case xx of
         -- The snipX function shouldn't have called us with an XApp.
         XApp{}           
-         -> error "DDC.Core.Transform.Snip: snipX shouldn't give us an XApp"
+         -> error "ddc-core-simpl.Snip: snipX shouldn't give us an XApp"
 
         -- leafy constructors
         XVar{}           -> xx
@@ -123,11 +128,11 @@
                 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
+        -- private, just make sure we record bindings with dummy val.
+        XLet a (LPrivate b mt bs) x2
          -> let ars     = zip bs (repeat 0)
                 x2'     = snipLetBody config a $ down ars x2
-            in  XLet a (LLetRegions b bs) x2'
+            in  XLet a (LPrivate b mt bs) x2'
 
         -- withregion
         XLet a (LWithRegion b) x2
@@ -224,7 +229,7 @@
 
         -- Split arguments into the already atomic ones,
         --  and the ones we need to introduce let-expressions for.
-        argss    = splitArgs xsArgs
+        argss    = splitArgs config xsArgs
 
         -- Collect up the new let-bindings.
         xsLets   = [ (x, a)  
@@ -287,18 +292,23 @@
 --   or compound ones.
 splitArgs 
         :: Ord n
-        => [(Exp a n, a)] 
+        => Config               
+        -> [(Exp a n, a)] 
         -> [( Exp a n            -- Expression to use as the new argument.
             , a                  -- Annoation for the argument application.
             , Bool               -- Whether this argument was already atomic.
             , Maybe (Exp a n))]  -- New expression to let-bind.
 
-splitArgs args
+splitArgs config args
  = reverse $ go 0 $ reverse args
  where  
         go _n [] = []
         go n ((xArg, a) : xsArgs)
          | isAtom xArg
+         = (xArg,           a, True,  Nothing)    : go n       xsArgs
+
+         | configPreserveLambdas config
+         , isXLam xArg || isXLAM xArg
          = (xArg,           a, True,  Nothing)    : go n       xsArgs
 
          | otherwise
diff --git a/DDC/Core/Transform/Thread.hs b/DDC/Core/Transform/Thread.hs
--- a/DDC/Core/Transform/Thread.hs
+++ b/DDC/Core/Transform/Thread.hs
@@ -215,7 +215,7 @@
              in  XLam (annotTail a) b x'
 
         -- Inject a new lambda to bind the state parameter.
-        _ |  Just a     <- takeAnnotOfExp xx
+        _ |  a          <- annotOfExp xx
           ,  t == configTokenType config 
           -> let b'     = BAnon (configTokenType config)
                  tenv'  = Env.extend b' tenv
@@ -339,10 +339,12 @@
         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
+
+        XType a t       
+         -> XType    (annotTail a) t
         
-        XWitness w      
-         -> XWitness (reannotate annotTail w)
+        XWitness a w      
+         -> XWitness (annotTail a) (reannotate annotTail w)
 
         -- Tailcalls
         XApp a _ _
@@ -358,7 +360,7 @@
          -- Otherwise wrap the returned value with a tuple holding
          -- the world.
          | otherwise
-         -> let Just a  = takeAnnotOfExp xx
+         -> let a       = annotOfExp xx
                 a'      = AnTEC (configTokenType config) 
                                 (tBot kEffect) 
                                 (tBot kClosure)
diff --git a/DDC/Core/Transform/TransformDownX.hs b/DDC/Core/Transform/TransformDownX.hs
--- a/DDC/Core/Transform/TransformDownX.hs
+++ b/DDC/Core/Transform/TransformDownX.hs
@@ -104,8 +104,8 @@
                         (return a) (return c)
                         (transformDownMX f kenv tenv x)
 
-        XType _         -> return xx'
-        XWitness _      -> return xx'
+        XType{}         -> return xx'
+        XWitness{}      -> return xx'
 
 
 instance Monad m => TransformDownMX m Lets where
@@ -121,8 +121,8 @@
                 xs'          <- mapM (transformDownMX f kenv tenv') xs
                 return       $ LRec $ zip bs xs'
 
-        LLetRegions{}    -> return xx
-        LWithRegion{}    -> return xx
+        LPrivate{}      -> return xx
+        LWithRegion{}   -> return xx
 
 
 instance Monad m => TransformDownMX m Alt where
diff --git a/DDC/Core/Transform/TransformUpX.hs b/DDC/Core/Transform/TransformUpX.hs
--- a/DDC/Core/Transform/TransformUpX.hs
+++ b/DDC/Core/Transform/TransformUpX.hs
@@ -111,8 +111,8 @@
                         (return a) (return c)
                         (transformUpMX f kenv tenv x)
 
-        XType _         -> return xx
-        XWitness _      -> return xx
+        XType{}         -> return xx
+        XWitness{}      -> return xx
 
 
 instance Monad m => TransformUpMX m Lets where
@@ -128,8 +128,8 @@
                 xs'          <- mapM (transformUpMX f kenv tenv') xs
                 return       $ LRec $ zip bs xs'
 
-        LLetRegions{}    -> return xx
-        LWithRegion{}    -> return xx
+        LPrivate{}      -> return xx
+        LWithRegion{}   -> return xx
 
 
 instance Monad m => TransformUpMX m Alt where
@@ -163,14 +163,12 @@
 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'
+         = do   let a    = annotOfExp xx
+                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
 
diff --git a/DDC/Type/Transform/Alpha.hs b/DDC/Type/Transform/Alpha.hs
--- a/DDC/Type/Transform/Alpha.hs
+++ b/DDC/Type/Transform/Alpha.hs
@@ -49,5 +49,6 @@
         TyConKind kc    -> TyConKind    kc
         TyConWitness tc -> TyConWitness tc
         TyConSpec tc    -> TyConSpec    tc
-        TyConBound u t  -> TyConBound (alpha f u) (alpha f t)
+        TyConBound  u k -> TyConBound   (alpha f u) (alpha f k)
+        TyConExists i k -> TyConExists  i           (alpha f k)
 
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,7 +1,7 @@
 --------------------------------------------------------------------------------
 The Disciplined Disciple Compiler License (MIT style)
 
-Copyrite (K) 2007-2013 The Disciplined Disciple Compiler Strike Force
+Copyrite (K) 2007-2014 The Disciplined Disciple Compiler Strike Force
 All rights reversed.
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
@@ -13,18 +13,4 @@
 
 The above copyright notice and this permission notice shall be included in
 all copies or substantial portions of the Software.
-
--------------------------------------------------------------------------------
-Under Australian law copyright is free and automatic.
-By contributing to DDC authors grant all rights they have regarding their
-contributions to the other members of the Disciplined Disciple Compiler Strike
-Force, past, present and future, as well as placing their contributions under
-the above license.
-
-Use "darcs show authors" to get a list of Strike Force members.
-
 --------------------------------------------------------------------------------
-Redistributions of libraries in ./external are governed by their own licenses:
-
-  - TinyPTC   GNU Lesser General Public License
-  
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.2.1
+Version:        0.4.1.1
 License:        MIT
 License-file:   LICENSE
 Author:         The Disciplined Disciple Compiler Strike Force
@@ -14,21 +14,23 @@
 
 Library
   Build-Depends: 
-        base            == 4.6.*,
+        base            >= 4.6 && < 4.8,
+        array           >= 0.4 && < 0.6,
         deepseq         == 1.3.*,
         containers      == 0.5.*,
-        array           == 0.4.*,
         transformers    == 0.3.*,
         mtl             == 2.1.*,
-        ddc-base        == 0.3.2.*,
-        ddc-core        == 0.3.2.*
+        ddc-base        == 0.4.1.*,
+        ddc-core        == 0.4.1.*
 
   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
@@ -36,6 +38,7 @@
         DDC.Core.Transform.Rewrite.Rule
         DDC.Core.Transform.AnonymizeX
         DDC.Core.Transform.Beta
+        DDC.Core.Transform.Boxing
         DDC.Core.Transform.Bubble
         DDC.Core.Transform.Prune
         DDC.Core.Transform.Elaborate
@@ -49,6 +52,7 @@
         DDC.Core.Transform.Thread
         DDC.Core.Transform.TransformUpX
         DDC.Core.Transform.TransformDownX
+
         DDC.Core.Simplifier
 
         DDC.Type.Transform.Alpha
@@ -67,6 +71,7 @@
         -Wall
         -fno-warn-orphans
         -fno-warn-missing-signatures
+        -fno-warn-missing-methods
         -fno-warn-unused-do-bind
 
   Extensions: