diff --git a/DDC/Core/Check/CheckExp.hs b/DDC/Core/Check/CheckExp.hs
--- a/DDC/Core/Check/CheckExp.hs
+++ b/DDC/Core/Check/CheckExp.hs
@@ -21,6 +21,7 @@
 import DDC.Type.Transform.Trim
 import DDC.Type.Transform.Instantiate
 import DDC.Type.Transform.LiftT
+import DDC.Type.Transform.LowerT
 import DDC.Type.Equiv
 import DDC.Type.Universe
 import DDC.Type.Compounds
@@ -33,6 +34,7 @@
 import qualified DDC.Type.Env           as Env
 import qualified DDC.Type.Check         as T
 import qualified Data.Set               as Set
+import qualified Data.Map               as Map
 import Control.Monad
 import Data.List                        as L
 import Data.Maybe
@@ -165,18 +167,33 @@
 
 
 -- constructors ---------------------------------
-checkExpM' _defs _kenv _tenv (XCon a u)
-      = return  ( XCon a u
-                , typeOfBound u
-                , Sum.empty kEffect
-                , Set.empty)
+checkExpM' defs _kenv _tenv xx@(XCon a u)
+        | UName n _     <- u
+        = case Map.lookup n (dataDefsCtors defs) of
+           Nothing -> throw $ ErrorUndefinedCtor xx
+           Just _  
+            -> return  
+                  ( XCon a u
+                  , typeOfBound u
+                  , Sum.empty kEffect
+                  , Set.empty)
 
+        | UPrim{}       <- u
+        = return  ( XCon a u
+                  , typeOfBound u
+                  , Sum.empty kEffect
+                  , Set.empty)
 
+        -- Constructors can't be locally bound.
+        | otherwise
+        = throw $ ErrorMalformedExp xx
+
+
 -- application ------------------------------------
 -- value-type application.
 checkExpM' defs kenv tenv xx@(XApp a x1 (XType t2))
  = do   (x1', t1, effs1, clos1) <- checkExpM  defs kenv tenv x1
-        k2                      <- checkTypeM kenv t2
+        k2                      <- checkTypeM defs kenv t2
         case t1 of
          TForall b11 t12
           | typeOfBind b11 == k2
@@ -192,7 +209,7 @@
 -- value-witness application.
 checkExpM' defs kenv tenv xx@(XApp a x1 (XWitness w2))
  = do   (x1', t1, effs1, clos1) <- checkExpM     defs kenv tenv x1
-        t2                      <- checkWitnessM      kenv tenv w2
+        t2                      <- checkWitnessM defs kenv tenv w2
         case t1 of
          TApp (TApp (TCon (TyConWitness TwConImpl)) t11) t12
           | t11 `equivT` t2   
@@ -209,6 +226,9 @@
 checkExpM' defs kenv tenv xx@(XApp a x1 x2)
  = do   (x1', t1, effs1, clos1)    <- checkExpM defs kenv tenv x1
         (x2', t2, effs2, clos2)    <- checkExpM defs kenv tenv x2
+
+        -- Note: we don't need to use the closure of the function because
+        --       all of its components will already be part of clos1 above.
         case t1 of
          TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFun)) t11) eff) _clo) t12
           | t11 `equivT` t2   
@@ -225,12 +245,13 @@
 -- spec abstraction -----------------------------
 checkExpM' defs kenv tenv xx@(XLAM a b1 x2)
  = do   let t1          = typeOfBind b1
-        _               <- checkTypeM kenv t1
+        _               <- checkTypeM defs kenv t1
 
         -- Check the body
-        let kenv'         =  Env.extend b1 kenv
-        (x2', t2, e2, c2) <- checkExpM defs kenv' tenv x2
-        k2                <- checkTypeM kenv' t2
+        let kenv'         = Env.extend b1 kenv
+        let tenv'         = Env.lift   1  tenv
+        (x2', t2, e2, c2) <- checkExpM  defs kenv' tenv' x2
+        k2                <- checkTypeM defs kenv' t2
 
         when (Env.memberBind b1 kenv)
          $ throw $ ErrorLamShadow xx b1
@@ -256,13 +277,13 @@
 
 -- function abstractions ------------------------
 checkExpM' defs kenv tenv xx@(XLam a b1 x2)
- = do   let t1          =  typeOfBind b1
-        k1              <- checkTypeM kenv t1
+ = do   let t1               =  typeOfBind b1
+        k1                   <- checkTypeM defs kenv t1
 
         -- Check the body.
         let tenv'            =  Env.extend b1 tenv
         (x2', t2, e2, c2)    <- checkExpM  defs kenv tenv' x2   
-        k2                   <- checkTypeM kenv t2
+        k2                   <- checkTypeM defs kenv t2
 
         -- The form of the function constructor depends on what universe the 
         -- binder is in.
@@ -311,7 +332,7 @@
 
         -- Check binder annotation against the type we inferred for the right.
         (b11', k11')    
-         <- checkLetBindOfTypeM xx kenv tenv t12 b11
+         <- checkLetBindOfTypeM xx defs kenv tenv t12 b11
 
         -- The right of the binding should have data kind.
         when (not $ isDataKind k11')
@@ -322,7 +343,7 @@
         (x2', t2, effs2, c2)    <- checkExpM defs kenv tenv1 x2
 
         -- The body should have data kind.
-        k2 <- checkTypeM kenv t2
+        k2 <- checkTypeM defs kenv t2
         when (not $ isDataKind k2)
          $ throw $ ErrorLetBodyNotData xx t2 k2
 
@@ -351,7 +372,7 @@
           LetLazy Nothing
            -> do case takeDataTyConApps t12 of
                   Just (_tc, t1 : _)
-                   ->  do k1 <- checkTypeM kenv t1
+                   ->  do k1 <- checkTypeM defs kenv t1
                           when (isRegionKind k1)
                            $ throw $ ErrorLetLazyNoWitness xx b11 t12
 
@@ -360,7 +381,7 @@
           -- Type of lazy binding might have a head region,
           -- so we need a Lazy witness for it.
           LetLazy (Just wit)
-           -> do tWit        <- checkWitnessM kenv tenv wit
+           -> do tWit        <- checkWitnessM defs kenv tenv wit
                  let tWitExp =  case takeDataTyConApps t12 of
                                  Just (_tc, tR : _ts) -> tLazy tR
                                  _                    -> tHeadLazy t12
@@ -382,7 +403,8 @@
         let (bs, xs)    = unzip bxs
 
         -- Check all the annotations.
-        ks              <- mapM (checkTypeM kenv) $ map typeOfBind bs
+        ks              <- mapM (checkTypeM defs kenv) 
+                        $  map typeOfBind bs
 
         -- Check all the annots have data kind.
         zipWithM_ (\b k
@@ -414,7 +436,7 @@
                 <- checkExpM defs kenv tenv' xBody
 
         -- The body type must have data kind.
-        kBody   <- checkTypeM kenv tBody
+        kBody   <- checkTypeM defs kenv tBody
         when (not $ isDataKind kBody)
          $ throw $ ErrorLetBodyNotData xx tBody kBody
 
@@ -440,7 +462,7 @@
       -> do
         -- Check the type on the region binder.
         let k   = typeOfBind b
-        checkTypeM kenv k
+        checkTypeM defs kenv k
 
         -- The binder must have region kind.
         when (not $ isRegionKind k)
@@ -452,19 +474,20 @@
          $ throw $ ErrorLetRegionRebound xx b
         
         -- Check the witness types.
-        let kenv'         = Env.extend b kenv
-        mapM_ (checkTypeM kenv') $ map typeOfBind bs
+        let kenv'       = Env.extend b kenv
+        let tenv'       = Env.lift 1 tenv
+        mapM_ (checkTypeM defs kenv') $ map typeOfBind bs
 
         -- Check that the witnesses bound here are for the region,
         -- and they don't conflict with each other.
         checkWitnessBindsM xx u bs
 
         -- Check the body expression.
-        let tenv'       = Env.extends bs tenv
-        (xBody', tBody, effs, clo)  <- checkExpM defs kenv' tenv' x
+        let tenv2       = Env.extends bs tenv'
+        (xBody', tBody, effs, clo)  <- checkExpM defs kenv' tenv2 x
 
         -- The body type must have data kind.
-        kBody           <- checkTypeM kenv' tBody
+        kBody           <- checkTypeM defs kenv' tBody
         when (not $ isDataKind kBody)
          $ throw $ ErrorLetBodyNotData xx tBody kBody
 
@@ -480,20 +503,22 @@
                         $ effs
 
         -- Delete the bound region variable from the closure.
-        let clo_masked  = Set.delete (GBoundRgnVar u) 
-                        $ clo
-        
+        -- Mask closure terms due to locally bound region vars.
+        let c2_cut      = Set.fromList
+                        $ mapMaybe (cutTaggedClosureT b)
+                        $ Set.toList clo
+
         return  ( XLet a (LLetRegion b bs) xBody'
-                , tBody
-                , effs'
-                , clo_masked)
+                , lowerT 1 tBody
+                , lowerT 1 effs'
+                , c2_cut)
 
 
 -- withregion -----------------------------------
 checkExpM' defs kenv tenv xx@(XLet a (LWithRegion u) x)
  = do   -- Check the type on the region handle.
         let k   = typeOfBound u
-        checkTypeM kenv k
+        checkTypeM defs kenv k
 
         -- The handle must have region kind.
         when (not $ isRegionKind k)
@@ -504,7 +529,7 @@
                <- checkExpM defs kenv tenv x
 
         -- The body type must have data kind.
-        kBody  <- checkTypeM kenv tBody
+        kBody  <- checkTypeM defs kenv tBody
         when (not $ isDataKind kBody)
          $ throw $ ErrorLetBodyNotData xx tBody kBody
         
@@ -634,7 +659,7 @@
 checkExpM' defs kenv tenv xx@(XCast a c@(CastWeakenEffect eff) x1)
  = do   
         -- Check the effect term.
-        kEff    <- checkTypeM kenv eff
+        kEff    <- checkTypeM defs kenv eff
         when (not $ isEffectKind kEff)
          $ throw $ ErrorMaxeffNotEff xx eff kEff
 
@@ -651,7 +676,7 @@
 checkExpM' defs kenv tenv xx@(XCast a c@(CastWeakenClosure clo2) x1)
  = do   
         -- Check the closure term.
-        kClo    <- checkTypeM kenv clo2
+        kClo    <- checkTypeM defs kenv clo2
         when (not $ isClosureKind kClo)
          $ throw $ ErrorMaxcloNotClo xx clo2 kClo
 
@@ -673,8 +698,8 @@
 
 -- Purify an effect, given a witness that it is pure.
 checkExpM' defs kenv tenv xx@(XCast a c@(CastPurify w) x1)
- = do   tW                   <- checkWitnessM  kenv tenv w
-        (x1', t1, effs, clo) <- checkExpM defs kenv tenv x1
+ = do   tW                   <- checkWitnessM defs kenv tenv w
+        (x1', t1, effs, clo) <- checkExpM     defs kenv tenv x1
                 
         effs' <- case tW of
                   TApp (TCon (TyConWitness TwConPure)) effMask
@@ -689,8 +714,8 @@
 
 -- Forget a closure, given a witness that it is empty.
 checkExpM' defs kenv tenv xx@(XCast a c@(CastForget w) x1)
- = do   tW                    <- checkWitnessM  kenv tenv w
-        (x1', t1, effs, clos) <- checkExpM defs kenv tenv x1
+ = do   tW                    <- checkWitnessM defs kenv tenv w
+        (x1', t1, effs, clos) <- checkExpM     defs kenv tenv x1
 
         clos' <- case tW of
                   TApp (TCon (TyConWitness TwConEmpty)) cloMask
@@ -877,10 +902,14 @@
 
 -------------------------------------------------------------------------------
 -- | Check a type in the exp checking monad.
-checkTypeM :: (Ord n, Pretty n) => Env n -> Type n -> CheckM a n (Kind n)
+checkTypeM :: (Ord n, Pretty n) 
+           => DataDefs n 
+           -> Env n 
+           -> Type n 
+           -> CheckM a n (Kind n)
 
-checkTypeM kenv tt
- = case T.checkType kenv tt of
+checkTypeM defs kenv tt
+ = case T.checkType defs kenv tt of
         Left err        -> throw $ ErrorType err
         Right k         -> return k
 
@@ -893,16 +922,17 @@
 checkLetBindOfTypeM 
         :: (Eq n, Ord n, Pretty n) 
         => Exp a n 
+        -> DataDefs n           -- Data type definitions.
         -> Env n                -- Kind environment. 
         -> Env n                -- Type environment.
         -> Type n 
         -> Bind n 
         -> CheckM a n (Bind n, Kind n)
 
-checkLetBindOfTypeM xx kenv _tenv tRight b
+checkLetBindOfTypeM xx defs kenv _tenv tRight b
         -- If the annotation is Bot then just replace it.
         | isBot (typeOfBind b)
-        = do    k       <- checkTypeM kenv tRight
+        = do    k       <- checkTypeM defs kenv tRight
                 return  ( replaceTypeOfBind tRight b 
                         , k)
 
@@ -911,6 +941,6 @@
         = throw $ ErrorLetMismatch xx b tRight
 
         | otherwise
-        = do    k       <- checkTypeM kenv (typeOfBind b)
+        = do    k       <- checkTypeM defs kenv (typeOfBind b)
                 return (b, k)
 
diff --git a/DDC/Core/Check/CheckWitness.hs b/DDC/Core/Check/CheckWitness.hs
--- a/DDC/Core/Check/CheckWitness.hs
+++ b/DDC/Core/Check/CheckWitness.hs
@@ -9,6 +9,7 @@
         , CheckM
         , checkWitnessM)
 where
+import DDC.Core.DataDef
 import DDC.Core.Exp
 import DDC.Core.Pretty
 import DDC.Core.Check.Error
@@ -45,13 +46,14 @@
 --
 checkWitness
         :: (Ord n, Pretty n)
-        => Env n                -- ^ Kind Environment.
+        => DataDefs n           -- ^ Data type definitions.
+        -> Env n                -- ^ Kind Environment.
         -> Env n                -- ^ Type Environment.
         -> Witness n            -- ^ Witness to check.
         -> Either (Error a n) (Type n)
 
-checkWitness kenv tenv xx
-        = result $ checkWitnessM kenv tenv xx
+checkWitness defs kenv tenv xx
+        = result $ checkWitnessM defs kenv tenv xx
 
 
 -- | Like `checkWitness`, but check in an empty environment.
@@ -62,23 +64,26 @@
 --
 typeOfWitness 
         :: (Ord n, Pretty n) 
-        => Witness n 
+        => DataDefs n
+        -> Witness n 
         -> Either (Error a n) (Type n)
-typeOfWitness ww 
+
+typeOfWitness defs ww 
         = result 
-        $ checkWitnessM Env.empty Env.empty ww
+        $ checkWitnessM defs Env.empty Env.empty ww
 
 
 ------------------------------------------------------------------------------
 -- | Like `checkWitness` but using the `CheckM` monad to manage errors.
 checkWitnessM 
         :: (Ord n, Pretty n)
-        => Env n                -- ^ Kind environment.
+        => DataDefs n           -- ^ Data type definitions.
+        -> Env n                -- ^ Kind environment.
         -> Env n                -- ^ Type environment.
         -> Witness n            -- ^ Witness to check.
         -> CheckM a n (Type n)
 
-checkWitnessM _kenv tenv (WVar u)
+checkWitnessM _defs _kenv tenv (WVar u)
  = do   let tBound      = typeOfBound u
         let mtEnv       = Env.lookup u tenv
 
@@ -122,14 +127,14 @@
         return tResult
 
 
-checkWitnessM _kenv _tenv (WCon wc)
+checkWitnessM _defs _kenv _tenv (WCon wc)
  = return $ typeOfWiCon wc
 
   
 -- value-type application
-checkWitnessM kenv tenv ww@(WApp w1 (WType t2))
- = do   t1      <- checkWitnessM  kenv tenv w1
-        k2      <- checkTypeM     kenv t2
+checkWitnessM defs kenv tenv ww@(WApp w1 (WType t2))
+ = do   t1      <- checkWitnessM  defs kenv tenv w1
+        k2      <- checkTypeM     defs kenv t2
         case t1 of
          TForall b11 t12
           |  typeOfBind b11 == k2
@@ -139,9 +144,9 @@
          _              -> throw $ ErrorWAppNotCtor  ww t1 t2
 
 -- witness-witness application
-checkWitnessM kenv tenv ww@(WApp w1 w2)
- = do   t1      <- checkWitnessM kenv tenv w1
-        t2      <- checkWitnessM kenv tenv w2
+checkWitnessM defs kenv tenv ww@(WApp w1 w2)
+ = do   t1      <- checkWitnessM defs kenv tenv w1
+        t2      <- checkWitnessM defs kenv tenv w2
         case t1 of
          TApp (TApp (TCon (TyConWitness TwConImpl)) t11) t12
           |  t11 == t2   
@@ -151,9 +156,9 @@
          _              -> throw $ ErrorWAppNotCtor  ww t1 t2
 
 -- witness joining
-checkWitnessM kenv tenv ww@(WJoin w1 w2)
- = do   t1      <- checkWitnessM kenv tenv w1
-        t2      <- checkWitnessM kenv tenv w2
+checkWitnessM defs kenv tenv ww@(WJoin w1 w2)
+ = do   t1      <- checkWitnessM defs kenv tenv w1
+        t2      <- checkWitnessM defs kenv tenv w2
         case (t1, t2) of
          (  TApp (TCon (TyConWitness TwConPure)) eff1
           , TApp (TCon (TyConWitness TwConPure)) eff2)
@@ -168,8 +173,8 @@
          _ -> throw $ ErrorCannotJoin ww w1 t1 w2 t2
 
 -- embedded types
-checkWitnessM kenv _tenv (WType t)
- = checkTypeM kenv t
+checkWitnessM defs kenv _tenv (WType t)
+ = checkTypeM defs kenv t
         
 
 -- | Take the type of a witness constructor.
@@ -193,9 +198,15 @@
 
 -- checkType ------------------------------------------------------------------
 -- | Check a type in the exp checking monad.
-checkTypeM :: (Ord n, Pretty n) => Env n -> Type n -> CheckM a n (Kind n)
-checkTypeM kenv tt
- = case T.checkType kenv tt of
+checkTypeM 
+        :: (Ord n, Pretty n) 
+        => DataDefs n 
+        -> Env n 
+        -> Type n 
+        -> CheckM a n (Kind n)
+
+checkTypeM defs kenv tt
+ = case T.checkType defs kenv tt of
         Left err        -> throw $ ErrorType err
         Right k         -> return k
 
diff --git a/DDC/Core/Check/Error.hs b/DDC/Core/Check/Error.hs
--- a/DDC/Core/Check/Error.hs
+++ b/DDC/Core/Check/Error.hs
@@ -39,6 +39,11 @@
         { errorBound            :: Bound n
         , errorTypeEnv          :: Type n }
 
+        -- Con --------------------------------------------
+        -- | A data constructor that wasn't in the set of data definitions.
+        | ErrorUndefinedCtor
+        { errorChecking         :: Exp a n }
+
         -- Application ------------------------------------
         -- | A function application where the parameter and argument don't match.
         | ErrorAppMismatch
diff --git a/DDC/Core/Check/ErrorMessage.hs b/DDC/Core/Check/ErrorMessage.hs
--- a/DDC/Core/Check/ErrorMessage.hs
+++ b/DDC/Core/Check/ErrorMessage.hs
@@ -40,6 +40,11 @@
                  , text "     from environment." ]
 
 
+        -- Constructor ------------------------------------
+        ErrorUndefinedCtor xx
+         -> vcat [ text "Undefined data constructor: "  <> ppr xx ]
+
+
         -- Application ------------------------------------
         ErrorAppMismatch xx t1 t2
          -> vcat [ text "Type mismatch in application." 
diff --git a/DDC/Core/Compounds.hs b/DDC/Core/Compounds.hs
--- a/DDC/Core/Compounds.hs
+++ b/DDC/Core/Compounds.hs
@@ -122,7 +122,7 @@
  = foldr (\(f, b) x'
            -> if f then XLAM a b x'
                    else XLam a b x')
-                x (reverse fbs)
+                x fbs
 
 
 -- Applications ---------------------------------------------------------------
diff --git a/DDC/Core/DataDef.hs b/DDC/Core/DataDef.hs
--- a/DDC/Core/DataDef.hs
+++ b/DDC/Core/DataDef.hs
@@ -30,7 +30,7 @@
           -- | Kinds of type parameters.
         , dataDefParamKinds     :: [Kind n]
 
-          -- | Constructors of is data type, or Nothing if there are
+          -- | Constructors of the data type, or Nothing if there are
           --   too many to list (like with `Int`).
         , dataDefCtors          :: Maybe [(n, [Type n])] }
 
diff --git a/DDC/Core/Parser.hs b/DDC/Core/Parser.hs
--- a/DDC/Core/Parser.hs
+++ b/DDC/Core/Parser.hs
@@ -68,15 +68,25 @@
         x2              <- pExp
         return  $ XLet () (LLet mode1 b1 x1) x2
 
+
         -- letrec expression
  , do   pTok KLetRec
-        pTok KBraceBra
-        lets    <- P.sepEndBy1 pLetRecBinding (pTok KSemiColon)
-        pTok KBraceKet
-        pTok KIn
-        x       <- pExp
 
-        return  $ XLet () (LRec lets) x
+        P.choice
+         -- Multiple bindings in braces
+         [ do   pTok KBraceBra
+                lets    <- P.sepEndBy1 pLetRecBinding (pTok KSemiColon)
+                pTok KBraceKet
+                pTok KIn
+                x       <- pExp
+                return  $ XLet () (LRec lets) x
+
+         -- A single binding without braces.
+         , do   ll      <- pLetRecBinding
+                pTok KIn
+                x       <- pExp
+                return  $ XLet () (LRec [ll]) x
+         ]      
 
 
         -- Local region binding.
diff --git a/DDC/Type/Check.hs b/DDC/Type/Check.hs
--- a/DDC/Type/Check.hs
+++ b/DDC/Type/Check.hs
@@ -17,6 +17,7 @@
 import DDC.Type.Compounds
 import DDC.Type.Predicates
 import DDC.Type.Transform.LiftT
+import DDC.Core.DataDef
 import DDC.Type.Exp
 import DDC.Base.Pretty
 import Data.List
@@ -27,6 +28,7 @@
 import qualified DDC.Type.Sum           as TS
 import qualified DDC.Type.Env           as Env
 import qualified DDC.Type.Check.Monad   as G
+import qualified Data.Map               as Map
 
 
 -- | The type checker monad.
@@ -35,15 +37,26 @@
 
 -- Wrappers -------------------------------------------------------------------
 -- | Check a type in the given environment, returning an error or its kind.
-checkType  :: (Ord n, Pretty n) => Env n -> Type n -> Either (Error n) (Kind n)
-checkType env tt = result $ checkTypeM env tt
+checkType  :: (Ord n, Pretty n) 
+           => DataDefs n 
+           -> Env n 
+           -> Type n 
+           -> Either (Error n) (Kind n)
 
+checkType defs env tt 
+        = result $ checkTypeM defs env tt
 
+
 -- | Check a type in an empty environment, returning an error or its kind.
-kindOfType :: (Ord n, Pretty n) => Type n -> Either (Error n) (Kind n)
-kindOfType tt = result $ checkTypeM Env.empty tt
+kindOfType :: (Ord n, Pretty n) 
+           => DataDefs n
+           -> Type n 
+           -> Either (Error n) (Kind n)
 
+kindOfType defs tt
+        = result $ checkTypeM defs Env.empty tt
 
+
 -- checkType ------------------------------------------------------------------
 -- | Check a type, returning its kind.
 ---
@@ -51,13 +64,19 @@
 --   (==) instead of equivT. This is because kinds do not contain quantifiers
 --   that need to be compared up to alpha-equivalence, nor do they contain
 --   crushable components terms.
-checkTypeM :: (Ord n, Pretty n) => Env n -> Type n -> CheckM n (Kind n)
-checkTypeM env tt
+checkTypeM 
+        :: (Ord n, Pretty n) 
+        => DataDefs n
+        -> Env n
+        -> Type n 
+        -> CheckM n (Kind n)
+
+checkTypeM defs env tt
         = -- trace (pretty $ text "checkTypeM:" <+> ppr tt) $
-          checkTypeM' env tt
+          checkTypeM' defs env tt
 
 -- Variables ------------------
-checkTypeM' env (TVar u)
+checkTypeM' _defs env (TVar u)
  = do   let tBound      = typeOfBound u
         let mtEnv       = Env.lookup u env
 
@@ -97,7 +116,7 @@
         mkResult
 
 -- Constructors ---------------
-checkTypeM' _env tt@(TCon tc)
+checkTypeM' defs _env tt@(TCon tc)
  = case tc of
         -- Sorts don't have a higher classification.
         TyConSort _      -> throw $ ErrorNakedSort tt
@@ -111,13 +130,25 @@
 
         TyConWitness tcw -> return $ kindOfTwCon tcw
         TyConSpec    tcc -> return $ kindOfTcCon tcc
-        TyConBound    u  -> return $ typeOfBound u
 
+        -- User defined type constructors need to be in the set of data defs.
+        TyConBound    u  
+         -> case u of
+                UName n _
+                 | Just _ <- Map.lookup n (dataDefsTypes defs)
+                 -> return $ typeOfBound u
 
+                 | otherwise
+                 -> throw $ ErrorUndefinedCtor u
+
+                UPrim{} -> return $ typeOfBound u
+                UIx{}   -> error "sorry"
+
+
 -- Quantifiers ----------------
-checkTypeM' env tt@(TForall b1 t2)
- = do   _       <- checkTypeM env (typeOfBind b1)
-        k2      <- checkTypeM (Env.extend b1 env) t2
+checkTypeM' defs env tt@(TForall b1 t2)
+ = do   _       <- checkTypeM defs env (typeOfBind b1)
+        k2      <- checkTypeM defs (Env.extend b1 env) t2
 
         -- The body must have data or witness kind.
         when (  (not $ isDataKind k2)
@@ -129,18 +160,18 @@
 -- Applications ---------------
 -- Applications of the kind function constructor are handled directly
 -- because the constructor doesn't have a sort by itself.
-checkTypeM' env (TApp (TApp (TCon (TyConKind KiConFun)) k1) k2)
- = do   _       <- checkTypeM env k1
-        s2      <- checkTypeM env k2
+checkTypeM' defs env (TApp (TApp (TCon (TyConKind KiConFun)) k1) k2)
+ = do   _       <- checkTypeM defs env k1
+        s2      <- checkTypeM defs env k2
         return  s2
 
 -- The implication constructor is overloaded and can have the
 -- following kinds:
 --   (=>) :: @ ~> @ ~> @,  for witness implication.
 --   (=>) :: @ ~> * ~> *,  for a context.
-checkTypeM' env tt@(TApp (TApp (TCon (TyConWitness TwConImpl)) t1) t2)
- = do   k1      <- checkTypeM env t1
-        k2      <- checkTypeM env t2
+checkTypeM' defs env tt@(TApp (TApp (TCon (TyConWitness TwConImpl)) t1) t2)
+ = do   k1      <- checkTypeM defs env t1
+        k2      <- checkTypeM defs env t2
         if      isWitnessKind k1 && isWitnessKind k2
          then     return kWitness
         else if isWitnessKind k1 && isDataKind k2
@@ -148,9 +179,9 @@
         else    throw $ ErrorWitnessImplInvalid tt t1 k1 t2 k2
 
 -- Type application.
-checkTypeM' env tt@(TApp t1 t2)
- = do   k1      <- checkTypeM env t1
-        k2      <- checkTypeM env t2
+checkTypeM' defs env tt@(TApp t1 t2)
+ = do   k1      <- checkTypeM defs env t1
+        k2      <- checkTypeM defs env t2
         case k1 of
          TApp (TApp (TCon (TyConKind KiConFun)) k11) k12
           | k11 == k2   -> return k12
@@ -159,8 +190,8 @@
          _              -> throw $ ErrorAppNotFun tt t1 k1 t2 k2
 
 -- Sums -----------------------
-checkTypeM' env (TSum ts)
- = do   ks      <- mapM (checkTypeM env) $ TS.toList ts
+checkTypeM' defs env (TSum ts)
+ = do   ks      <- mapM (checkTypeM defs env) $ TS.toList ts
 
         -- Check that all the types in the sum have a single kind, 
         -- and return that kind.
diff --git a/DDC/Type/Check/CheckError.hs b/DDC/Type/Check/CheckError.hs
--- a/DDC/Type/Check/CheckError.hs
+++ b/DDC/Type/Check/CheckError.hs
@@ -16,6 +16,10 @@
         = ErrorUndefined        
         { errorBound            :: Bound n }
 
+        -- | An undefined type constructor.
+        | ErrorUndefinedCtor
+        { errorBound            :: Bound n }
+
         -- | The kind annotation on the variables does not match the one in the environment.
         | ErrorVarAnnotMismatch
         { errorBound            :: Bound n
@@ -72,14 +76,17 @@
 instance (Eq n, Pretty n) => Pretty (Error n) where
  ppr err
   = case err of
+        ErrorUndefined u
+         -> text "Undefined type variable:  " <> ppr u
+
+        ErrorUndefinedCtor u
+         -> text "Undefined type constructor:  " <> ppr u
+
         ErrorUnappliedKindFun 
          -> text "Can't take sort of unapplied kind function constructor."
         
         ErrorNakedSort s
          -> text "Can't check a naked sort: " <> ppr s
-
-        ErrorUndefined u
-         -> text "Undefined type variable:  " <> ppr u
         
         ErrorVarAnnotMismatch u t
          -> vcat [ text "Type mismatch in annotation."
diff --git a/DDC/Type/Env.hs b/DDC/Type/Env.hs
--- a/DDC/Type/Env.hs
+++ b/DDC/Type/Env.hs
@@ -16,9 +16,11 @@
         , member,       memberBind
         , lookup,       lookupName
         , depth
+        , lift
         , wrapTForalls)
 where
 import DDC.Type.Exp
+import DDC.Type.Transform.LiftT
 import Data.Maybe
 import Data.Map                 (Map)
 import Prelude                  hiding (lookup)
@@ -139,6 +141,18 @@
 -- | Yield the total depth of the deBruijn stack.
 depth :: Env n -> Int
 depth env       = envStackLength env
+
+
+-- | Lift all free deBruijn indices in the environment by the given number of steps.
+--   TODO: Delay this, only lift when we extract the final type.
+--         will also need to update the 'member' function.
+lift  :: Ord n => Int -> Env n -> Env n
+lift n env
+        = Env
+        { envMap         = Map.map (liftT n) (envMap env)
+        , envStack       = map (liftT n) (envStack env)
+        , envStackLength = envStackLength env
+        , envPrimFun     = envPrimFun     env }
 
 
 -- | Wrap locally bound (non primitive) variables defined in an environment
diff --git a/DDC/Type/Pretty.hs b/DDC/Type/Pretty.hs
--- a/DDC/Type/Pretty.hs
+++ b/DDC/Type/Pretty.hs
@@ -67,21 +67,20 @@
          -> pprParen (d > 5)
          $  ppr k1 <+> text "~>" <+> ppr k2
 
-        TApp (TApp (TCon (TyConWitness TwConImpl)) k1) k2
+        TApp (TApp (TCon (TyConWitness TwConImpl)) t1) t2
          -> pprParen (d > 5)
-         $  ppr k1 <+> text "=>" </> pprPrec 6 k2
+         $  pprPrec 6 t1 <+> text "=>" </> pprPrec 5 t2
 
         TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFun)) t1) eff) clo) t2
          | isBot eff, isBot clo
          -> pprParen (d > 5)
-         $  (if isTFun t1 then pprPrec 6 t1 else pprPrec 5 t1)
-                   <+> text "->" </> ppr t2
+         $  pprPrec 6 t1 <+> text "->"  </> pprPrec 5 t2
 
          | otherwise
          -> pprParen (d > 5)
-         $  (if isTFun t1 then pprPrec 6 t1 else pprPrec 5 t1)
-                   <+> text "-(" <> ppr eff <> text " | " <> ppr clo <> text ")>" 
-                   </> ppr t2
+         $  pprPrec 6 t1
+                <+> text "-(" <> ppr eff <> text " | " <> ppr clo <> text ")>" 
+                </> pprPrec 5 t2
                    
         -- Standard types.
         TCon tc    -> ppr tc
@@ -90,11 +89,11 @@
         TForall b t
          | Just (bsMore, tBody) <- takeTForalls t
          -> let groups  = partitionBindsByType (b:bsMore)
-            in  pprParen (d > 1) 
+            in  pprParen (d > 5) 
                  $ (cat $ map pprBinderGroup groups) <> ppr tBody
                         
          | otherwise
-         -> pprParen (d > 1)
+         -> pprParen (d > 5)
                 $ brackets (ppr b) <> dot <> ppr t
 
         TApp t1 t2
@@ -107,14 +106,6 @@
          
          | otherwise
          -> pprParen (d > 9) $  ppr ts
-
-
-isTFun :: Type n -> Bool
-isTFun tt
- = case tt of
-         TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFun)) _) _) _) _
-                -> True
-         _      -> False
 
 
 instance (Pretty n, Eq n) => Pretty (TypeSum n) where
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,7 +1,8 @@
 --------------------------------------------------------------------------------
 The Disciplined Disciple Compiler License (MIT style)
 
-Copyright (c) 2008-2011 Benjamin Lippmeier
+Copyrite (K) 2007-2012 The Disciplined Disciple Compiler Strike Force
+All rights reversed.
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
 of this software and associated documentation files (the "Software"), to deal
@@ -12,6 +13,15 @@
 
 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:
diff --git a/ddc-core.cabal b/ddc-core.cabal
--- a/ddc-core.cabal
+++ b/ddc-core.cabal
@@ -1,9 +1,9 @@
 Name:           ddc-core
-Version:        0.2.0.2
+Version:        0.2.1.1
 License:        MIT
 License-file:   LICENSE
-Author:         Ben Lippmeier
-Maintainer:     benl@ouroborus.net
+Author:         The Disciplined Disciple Compiler Strike Force
+Maintainer:     Ben Lippmeier <benl@ouroborus.net>
 Build-Type:     Simple
 Cabal-Version:  >=1.6
 Stability:      experimental
@@ -29,7 +29,7 @@
         array           == 0.4.*,
         transformers    == 0.2.*,
         mtl             == 2.0.*,
-        ddc-base        == 0.2.0.*
+        ddc-base        == 0.2.1.*
 
   Exposed-modules:
         DDC.Core.Check.CheckExp