diff --git a/DDC/Core/Tetra.hs b/DDC/Core/Tetra.hs
--- a/DDC/Core/Tetra.hs
+++ b/DDC/Core/Tetra.hs
@@ -22,6 +22,7 @@
         , OpError       (..)
         , PrimTyCon     (..),   pprPrimTyConStem
         , PrimArith     (..)
+        , PrimCast      (..)
 
           -- * Name Parsing
         , readName
@@ -32,6 +33,7 @@
         , readOpErrorFlag
         , readPrimTyCon,        readPrimTyConStem
         , readPrimArithFlag
+        , readPrimCastFlag
 
         -- * Name Generation
         , freshT
diff --git a/DDC/Core/Tetra/Check.hs b/DDC/Core/Tetra/Check.hs
--- a/DDC/Core/Tetra/Check.hs
+++ b/DDC/Core/Tetra/Check.hs
@@ -6,7 +6,6 @@
 import DDC.Core.Tetra.Error
 import DDC.Core.Tetra.Prim
 import DDC.Core.Module
-import DDC.Type.Exp
 
 
 -- | Perform Core Tetra specific checks on a module.
diff --git a/DDC/Core/Tetra/Compounds.hs b/DDC/Core/Tetra/Compounds.hs
--- a/DDC/Core/Tetra/Compounds.hs
+++ b/DDC/Core/Tetra/Compounds.hs
@@ -1,9 +1,9 @@
 
 module DDC.Core.Tetra.Compounds
-        ( module DDC.Core.Exp.Annot.Compounds
+        ( module DDC.Core.Exp.Annot
 
           -- * Primitive
-        , tBool, tNat, tInt, tSize, tWord, tFloat
+        , tVoid, tBool, tNat, tInt, tSize, tWord, tFloat
         , tPtr
 
           -- * Tetra types.
@@ -21,8 +21,7 @@
 import DDC.Core.Tetra.Prim.OpCast
 import DDC.Core.Tetra.Prim.OpFun
 import DDC.Core.Tetra.Prim.Base
-import DDC.Core.Exp.Annot.Compounds
-import DDC.Core.Exp.Annot.Exp
+import DDC.Core.Exp.Annot
 
 
 -- | Reify a super or foreign function into a closure.
@@ -90,8 +89,8 @@
 xCastConvert :: a -> Type Name -> Type Name -> Exp a Name -> Exp a Name 
 xCastConvert a tTo tFrom x
  = xApps a
-        (XVar a (UPrim (NamePrimCast PrimCastConvert) 
-                       (typePrimCast PrimCastConvert)))
+        (XVar a (UPrim (NamePrimCast PrimCastConvert False) 
+                       (typePrimCastFlag PrimCastConvert False)))
         [ XType a tTo
         , XType a tFrom
         , x ]
diff --git a/DDC/Core/Tetra/Convert.hs b/DDC/Core/Tetra/Convert.hs
--- a/DDC/Core/Tetra/Convert.hs
+++ b/DDC/Core/Tetra/Convert.hs
@@ -27,9 +27,9 @@
 import DDC.Type.Env                                     (KindEnv, TypeEnv)
 import qualified DDC.Type.Env                           as Env
 
-import DDC.Control.Monad.Check                          (throw, evalCheck)
+import DDC.Control.Check                                (throw, evalCheck)
 import Data.Map                                         (Map)
-import qualified Data.Map                               as Map
+import qualified Data.Map.Strict                        as Map
 import qualified Data.Set                               as Set
 
 
@@ -86,11 +86,16 @@
                    $ fromListDataDefs 
                    $ moduleImportDataDefs mm ++ moduleDataDefsLocal mm
 
+        let eqns'  = Map.unions
+                   [ Map.fromList $ [(n, t) | (n, (_, t)) <- moduleImportTypeDefs mm]
+                   , Map.fromList $ [(n, t) | (n, (_, t)) <- moduleTypeDefsLocal  mm] ]
+
         let nsForeignBoxedTypes
                    = [n | (n, ImportTypeBoxed _) <- moduleImportTypes mm ]
 
         let tctx'  = T.Context
                    { T.contextDataDefs  = defs'
+                   , T.contextTypeEqns  = eqns'
                    , T.contextForeignBoxedTypeCtors     
                         = Set.fromList nsForeignBoxedTypes
                    , T.contextKindEnv   = Env.empty }
@@ -109,16 +114,18 @@
 
         -- Starting context for the conversion.
         let ctx = Context
-                { contextPlatform    = pp
-                , contextDataDefs    = defs'
-                , contextForeignBoxedTypeCtors = Set.fromList $ nsForeignBoxedTypes
-                , contextCallable    = callables
-                , contextKindEnv     = kenv
-                , contextTypeEnv     = tenv' 
-                , contextSuperBinds  = Map.empty
-                , contextConvertExp  = convertExp 
-                , contextConvertLets = convertLets 
-                , contextConvertAlt  = convertAlt }
+                { contextPlatform       = pp
+                , contextDataDefs       = defs'
+                , contextTypeEqns       = eqns'
+                , contextForeignBoxedTypeCtors 
+                                        = Set.fromList $ nsForeignBoxedTypes
+                , contextCallable       = callables
+                , contextKindEnv        = kenv
+                , contextTypeEnv        = tenv' 
+                , contextSuperBinds     = Map.empty
+                , contextConvertExp     = convertExp 
+                , contextConvertLets    = convertLets 
+                , contextConvertAlt     = convertAlt }
 
         -- Convert the body of the module itself.
         x1      <- convertExp ExpTop ctx 
@@ -164,11 +171,13 @@
                 , moduleImportCaps      = []
                 , moduleImportValues    = (Map.toList A.runtimeImportTypes) ++ ntsImports'
                 , moduleImportDataDefs  = []
+                , moduleImportTypeDefs  = []
 
                   -- Data constructors and pattern matches should have been
                   -- flattened into primops, so we don't need the data type
                   -- definitions.
                 , moduleDataDefsLocal   = []
+                , moduleTypeDefsLocal   = []
 
                 , moduleBody            = x2 }
 
@@ -187,8 +196,9 @@
 convertExportM
         :: T.Context                     -- ^ Context of the conversion.
         -> Map A.Name (Type A.Name)      -- ^ Salt types of top-level values.
-        -> (E.Name, ExportSource E.Name) -- ^ Name and export def to convert.
-        -> ConvertM a (A.Name, ExportSource A.Name)
+        -> (E.Name, ExportSource E.Name (Type E.Name)) 
+                                        -- ^ Name and export def to convert.
+        -> ConvertM a (A.Name, ExportSource A.Name (Type A.Name))
 
 convertExportM tctx tsSalt (n, esrc)
  = do   n'      <- convertBindNameM n
@@ -204,10 +214,10 @@
 --  of each export from the list of previously known Salt types.
 --
 convertExportSourceM 
-        :: T.Context                    -- ^ Context of the conversion.
-        -> Map A.Name (Type A.Name)     -- ^ Salt types of top-level values.
-        -> ExportSource E.Name          -- ^ Export source to convert.
-        -> ConvertM a (ExportSource A.Name)
+        :: T.Context                            -- ^ Context of the conversion.
+        -> Map A.Name (Type A.Name)             -- ^ Salt types of top-level values.
+        -> ExportSource E.Name (Type E.Name)    -- ^ Export source to convert.
+        -> ConvertM a (ExportSource A.Name (Type A.Name))
 
 convertExportSourceM tctx tsSalt esrc
  = case esrc of
@@ -233,8 +243,8 @@
 ---------------------------------------------------------------------------------------------------
 -- | Convert an import spec.
 convertNameImportValueM
-        :: T.Context -> (E.Name, ImportValue E.Name)
-        -> ConvertM a (A.Name, ImportValue A.Name)
+        :: T.Context -> (E.Name, ImportValue E.Name (Type E.Name))
+        -> ConvertM a (A.Name, ImportValue A.Name (Type A.Name))
 
 convertNameImportValueM tctx (n, isrc)
  = do   n'      <- convertImportNameM n
@@ -255,8 +265,8 @@
 
 -- | Convert an import source to Salt.
 convertImportValueM 
-        :: T.Context -> ImportValue E.Name
-        -> ConvertM a (ImportValue A.Name)
+        :: T.Context -> ImportValue E.Name (Type E.Name)
+        -> ConvertM a (ImportValue A.Name (Type A.Name))
 
 convertImportValueM tctx isrc
  = case isrc of
diff --git a/DDC/Core/Tetra/Convert/Boxing.hs b/DDC/Core/Tetra/Convert/Boxing.hs
--- a/DDC/Core/Tetra/Convert/Boxing.hs
+++ b/DDC/Core/Tetra/Convert/Boxing.hs
@@ -26,7 +26,6 @@
 import DDC.Core.Tetra.Prim
 import DDC.Core.Tetra.Compounds
 import DDC.Type.DataDef
-import DDC.Type.Exp
 
 
 -- Predicates -----------------------------------------------------------------
diff --git a/DDC/Core/Tetra/Convert/Data.hs b/DDC/Core/Tetra/Convert/Data.hs
--- a/DDC/Core/Tetra/Convert/Data.hs
+++ b/DDC/Core/Tetra/Convert/Data.hs
@@ -9,8 +9,7 @@
 import DDC.Core.Transform.BoundX
 import DDC.Core.Exp
 import DDC.Type.Env
-import DDC.Type.Compounds
-import DDC.Type.Predicates
+import DDC.Type.Exp.Simple
 import DDC.Type.DataDef
 import qualified DDC.Core.Tetra.Prim            as E
 import qualified DDC.Core.Salt.Runtime          as A
diff --git a/DDC/Core/Tetra/Convert/Error.hs b/DDC/Core/Tetra/Convert/Error.hs
--- a/DDC/Core/Tetra/Convert/Error.hs
+++ b/DDC/Core/Tetra/Convert/Error.hs
@@ -4,11 +4,11 @@
         ,  Error (..))
 where
 import DDC.Core.Exp
-import DDC.Base.Pretty
+import DDC.Data.Pretty
 import DDC.Core.Check                                   (AnTEC(..))
 import DDC.Core.Tetra.Prim                              as E
 import qualified DDC.Core.Tetra.Transform.Curry.Error   as Curry
-import qualified DDC.Control.Monad.Check                as G
+import qualified DDC.Control.Check                      as G
 
 -- | Conversion Monad
 type ConvertM a x = G.CheckM () (Error a) x
@@ -54,7 +54,7 @@
 
         -- | An invalid data constructor name.
         | ErrorInvalidDaCon
-        { errorDaCon    :: DaCon E.Name }
+        { errorDaCon    :: DaCon E.Name (Type E.Name)}
 
         -- | An invalid name used for the constructor of an alternative.
         | ErrorInvalidAlt
diff --git a/DDC/Core/Tetra/Convert/Exp.hs b/DDC/Core/Tetra/Convert/Exp.hs
--- a/DDC/Core/Tetra/Convert/Exp.hs
+++ b/DDC/Core/Tetra/Convert/Exp.hs
@@ -23,18 +23,17 @@
 import qualified DDC.Core.Salt.Name             as A
 
 import DDC.Type.DataDef
-import DDC.Base.Pretty
-import Text.Show.Pretty
+import DDC.Data.Pretty
 import Control.Monad
 import Data.Maybe
-import DDC.Control.Monad.Check                  (throw)
+import DDC.Control.Check                        (throw)
 import qualified Data.Map                       as Map
 
 
 ---------------------------------------------------------------------------------------------------
 -- | Convert the body of a supercombinator to Salt.
 convertExp 
-        :: Show a 
+        :: Show a
         => ExpContext                   -- ^ The surrounding expression context.
         -> Context a                    -- ^ Types and values in the environment.
         -> Exp (AnTEC a E.Name) E.Name  -- ^ Expression to convert.
@@ -71,11 +70,11 @@
 
 
         ---------------------------------------------------
-        -- Type abstractions can only appear at the top-level of a function.
-        XLAM{}
-         -> throw $ ErrorUnsupported xx
-          $ vcat [ text "Cannot convert type abstraction in this context."
-                 , text "The program must be lambda-lifted before conversion." ]
+        -- Type abstractions can appear in the body of expressions when
+        -- the Curry transform has eta-expanded a higher-ranked type.
+        XLAM _ b x
+         -> let ctx'    = extendsKindEnv [b] ctx
+            in  convertExp ectx ctx' x
 
 
         ---------------------------------------------------
@@ -90,13 +89,15 @@
         -- Conversions for primitive operators are defined separately.
         _ 
          |  Just n <- takeNamePrimX xx
-         ,  Just r <- case n of
-                         E.NamePrimArith{} -> convertPrimArith  ectx ctx xx
-                         E.NamePrimCast{}  -> convertPrimBoxing ectx ctx xx
-                         E.NameOpError{}   -> convertPrimError  ectx ctx xx
-                         E.NameOpVector{}  -> convertPrimVector ectx ctx xx 
-                         E.NameOpFun{}     -> convertPrimCall   ectx ctx xx
-                         _                 -> Nothing
+         ,  Just r 
+             <- case n of
+                  E.NamePrimArith{}       -> convertPrimArith  ectx ctx xx
+                  E.NamePrimCast _ True   -> convertPrimArith  ectx ctx xx
+                  E.NamePrimCast _ False  -> convertPrimBoxing ectx ctx xx
+                  E.NameOpError{}         -> convertPrimError  ectx ctx xx
+                  E.NameOpVector{}        -> convertPrimVector ectx ctx xx 
+                  E.NameOpFun{}           -> convertPrimCall   ectx ctx xx
+                  _                       -> Nothing
          -> r
 
         ---------------------------------------------------
@@ -295,8 +296,7 @@
 
 ---------------------------------------------------------------------------------------------------
 convertExpSuperCall
-        :: Show a 
-        => Exp (AnTEC a E.Name) E.Name
+        :: Exp (AnTEC a E.Name) E.Name
         -> ExpContext                    -- ^ The surrounding expression context.
         -> Context a                     -- ^ Types and values in the environment.
         -> Bool                          -- ^ Whether this is call is directly inside a 'run'
@@ -317,7 +317,10 @@
  | Just (arityVal, boxings)
     <- case Map.lookup nFun (contextCallable ctx) of
         Just (Callable _src _ty cs)
-           |  Just (_, csVal, csBox)      <- Call.splitStdCallCons cs
+           |  Just (_, csVal, csBox)      
+                <- Call.splitStdCallCons 
+                $  filter (not . Call.isConsType) cs
+
            -> Just (length csVal, length csBox)
 
         _  -> Nothing
@@ -350,7 +353,6 @@
         , text "xx:        " <> ppr xx
         , text "fun:       " <> ppr nFun
         , text "args:      " <> ppr xsArgs
-        , text "callables: " <> text (ppShow $ contextCallable  ctx)
         ]
 
 
diff --git a/DDC/Core/Tetra/Convert/Exp/Alt.hs b/DDC/Core/Tetra/Convert/Exp/Alt.hs
--- a/DDC/Core/Tetra/Convert/Exp/Alt.hs
+++ b/DDC/Core/Tetra/Convert/Exp/Alt.hs
@@ -9,7 +9,7 @@
 import DDC.Core.Exp.Annot
 import DDC.Type.DataDef
 import DDC.Core.Check                    (AnTEC(..))
-import DDC.Control.Monad.Check           (throw)
+import DDC.Control.Check                (throw)
 import qualified DDC.Core.Tetra.Prim     as E
 import qualified DDC.Core.Salt.Name      as A
 import qualified DDC.Core.Salt.Compounds as A
@@ -18,8 +18,7 @@
 
 -- | Convert a Tetra alternative to Salt.
 convertAlt 
-        :: Show a
-        => a                            -- ^ Annotation from case expression.
+        :: a                            -- ^ Annotation from case expression.
         -> Bound E.Name                 -- ^ Bound of scrutinee.
         -> Type  E.Name                 -- ^ Type  of scrutinee
         -> ExpContext                   -- ^ Context of enclosing case-expression.
diff --git a/DDC/Core/Tetra/Convert/Exp/Arg.hs b/DDC/Core/Tetra/Convert/Exp/Arg.hs
--- a/DDC/Core/Tetra/Convert/Exp/Arg.hs
+++ b/DDC/Core/Tetra/Convert/Exp/Arg.hs
@@ -17,8 +17,7 @@
 --   it to the corresponding argument to use in the Salt program, or 
 --   return Nothing which indicates it should be discarded.
 convertOrDiscardSuperArgX
-        :: Show a                       
-        => Context a                    -- ^ Type context of the conversion.
+        :: Context a                    -- ^ Type context of the conversion.
         -> Exp (AnTEC a E.Name) E.Name  -- ^ Expression to convert.
         -> ConvertM a (Maybe (Exp a A.Name))
 
diff --git a/DDC/Core/Tetra/Convert/Exp/Base.hs b/DDC/Core/Tetra/Convert/Exp/Base.hs
--- a/DDC/Core/Tetra/Convert/Exp/Base.hs
+++ b/DDC/Core/Tetra/Convert/Exp/Base.hs
@@ -38,10 +38,13 @@
           contextPlatform       :: Platform
 
           -- | Data type definitions.
-          --   These are all the visible data type definitions, from both
-          --   the current module and imported ones.
+          --   All the visible type equations, from the current and imported modules.
         , contextDataDefs       :: DataDefs E.Name
 
+          -- | Type equations.
+          --   All the visible type equations, from the current and imported modules.
+        , contextTypeEqns       :: Map E.Name (Type E.Name)
+
           -- | Names of foreign boxed data type contructors.
           --   These are names like 'Ref' and 'Array' that are defined in the
           --   runtime system rather than as an algebraic data type with a 
@@ -98,6 +101,7 @@
 typeContext ctx
         = T.Context
         { T.contextDataDefs     = contextDataDefs ctx
+        , T.contextTypeEqns     = contextTypeEqns ctx
         , T.contextForeignBoxedTypeCtors 
                                 = contextForeignBoxedTypeCtors ctx
         , T.contextKindEnv      = contextKindEnv  ctx }
diff --git a/DDC/Core/Tetra/Convert/Exp/Ctor.hs b/DDC/Core/Tetra/Convert/Exp/Ctor.hs
--- a/DDC/Core/Tetra/Convert/Exp/Ctor.hs
+++ b/DDC/Core/Tetra/Convert/Exp/Ctor.hs
@@ -17,7 +17,7 @@
 
 import DDC.Type.DataDef
 
-import DDC.Control.Monad.Check           (throw)
+import DDC.Control.Check                (throw)
 import qualified Data.Map                as Map
 
 
@@ -26,7 +26,7 @@
         :: Show a
         => Context a
         -> AnTEC a  E.Name                -- ^ Annot from deconstructed app node.
-        -> DaCon    E.Name                -- ^ Data constructor being applied.
+        -> DaCon    E.Name (Type E.Name)  -- ^ Data constructor being applied.
         -> [Exp (AnTEC a E.Name) E.Name]  -- ^ Data constructor arguments.
         -> ConvertM a (Exp a A.Name)
 
diff --git a/DDC/Core/Tetra/Convert/Exp/Lets.hs b/DDC/Core/Tetra/Convert/Exp/Lets.hs
--- a/DDC/Core/Tetra/Convert/Exp/Lets.hs
+++ b/DDC/Core/Tetra/Convert/Exp/Lets.hs
@@ -15,8 +15,7 @@
 
 -- | Convert some let-bindings to Salt.
 convertLets
-        :: Show a  
-        => Context a
+        :: Context a
         -> Lets (AnTEC a E.Name) E.Name -- ^ Expression to convert.
         -> ConvertM a (Maybe (Lets a A.Name), Context a)
 
@@ -59,8 +58,7 @@
 
 -- | Convert a possibly recursive let binding.
 convertBinding
-        :: Show a
-        => Context a
+        :: Context a
         -> Bind  E.Name
         -> Exp (AnTEC a E.Name) E.Name 
         -> ConvertM a (Bind A.Name, Exp a A.Name)
@@ -138,11 +136,13 @@
          -- lambda in Salt which binds the region the object is in.
          | isDataKind $ typeOfBind bParamX
 
-         , BName (E.NameVar strX) _ <- bParamX
+         , BName nX _   <- bParamX
+         , Just strX    <- takeNameStr nX
          , strX'        <-  strX ++ "$r"
          , bParamX'     <-  BName (A.NameVar strX') kRegion
 
-         , BName (E.NameVar strT) _ <- bParamT
+         , BName nT _   <- bParamT
+         , Just strT    <- takeNameStr nT
          , strT'        <-  strT ++ "$r"
          , bParamT'     <-  BName (A.NameVar strT') kRegion
 
@@ -196,6 +196,13 @@
                 tBody'  <- convertDataT ctxT tt
                 return  ( xBody', tBody' )
 
+
+takeNameStr (E.NameVar str)
+                = Just $ str
+
+takeNameStr (E.NameExt (E.NameVar str1) str2)
+                = Just $ str1 ++ "$" ++ str2
+takeNameStr _   = Nothing
 
 -- Note: Binding top-level supers.
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/DDC/Core/Tetra/Convert/Exp/Lit.hs b/DDC/Core/Tetra/Convert/Exp/Lit.hs
--- a/DDC/Core/Tetra/Convert/Exp/Lit.hs
+++ b/DDC/Core/Tetra/Convert/Exp/Lit.hs
@@ -7,14 +7,14 @@
 import qualified DDC.Core.Tetra.Prim     as E
 import qualified DDC.Core.Salt.Name      as A
 import qualified DDC.Core.Salt.Compounds as A
-import DDC.Control.Monad.Check           (throw)
+import DDC.Control.Check                (throw)
 
 
 -- | Convert a literal constructor to Salt.
 --   These are values that have boxable index types like Bool# and Nat#.
 convertLitCtor
         :: a                            -- ^ Annot from deconstructed XCon node.
-        -> DaCon E.Name                 -- ^ Data constructor of literal.
+        -> DaCon E.Name (Type E.Name)   -- ^ Data constructor of literal.
         -> ConvertM a (Exp a A.Name)
 
 convertLitCtor a dc
@@ -26,6 +26,7 @@
         E.NameLitSize    i      -> return $ A.xSize    a i
         E.NameLitWord    i bits -> return $ A.xWord    a i bits
         E.NameLitFloat   f bits -> return $ A.xFloat   a f bits
+        E.NameLitChar    c      -> return $ A.xChar    a c
         E.NameLitTextLit bs     -> return $ A.xTextLit a bs
         _                       -> throw $ ErrorMalformed "Invalid literal."
 
diff --git a/DDC/Core/Tetra/Convert/Exp/PrimArith.hs b/DDC/Core/Tetra/Convert/Exp/PrimArith.hs
--- a/DDC/Core/Tetra/Convert/Exp/PrimArith.hs
+++ b/DDC/Core/Tetra/Convert/Exp/PrimArith.hs
@@ -8,16 +8,15 @@
 import DDC.Core.Tetra.Convert.Error
 import DDC.Core.Pretty
 import DDC.Core.Exp.Annot
-import DDC.Core.Check                    (AnTEC(..))
-import DDC.Control.Monad.Check           (throw)
-import qualified DDC.Core.Tetra.Prim     as E
-import qualified DDC.Core.Salt.Name      as A
+import DDC.Core.Check                   (AnTEC(..))
+import DDC.Control.Check                (throw)
+import qualified DDC.Core.Tetra.Prim    as E
+import qualified DDC.Core.Salt.Name     as A
 
 
 -- | Convert a Tetra arithmetic or logic primop to Salt.
 convertPrimArith
-        :: Show a 
-        => ExpContext                   -- ^ The surrounding expression context.
+        :: ExpContext                   -- ^ The surrounding expression context.
         -> Context a                    -- ^ Types and values in the environment.
         -> Exp (AnTEC a E.Name) E.Name  -- ^ Expression to convert.
         -> Maybe (ConvertM a (Exp a A.Name))
@@ -70,8 +69,7 @@
 --   we need to convert the ones applied directly to primops, 
 --   as the primops are specified polytypically.
 convertPrimArgX 
-        :: Show a 
-        => Context a
+        :: Context a
         -> ExpContext                   -- ^ What context we're converting in.
         -> Exp (AnTEC a E.Name) E.Name  -- ^ Expression to convert.
         -> ConvertM a (Exp a A.Name)
diff --git a/DDC/Core/Tetra/Convert/Exp/PrimBoxing.hs b/DDC/Core/Tetra/Convert/Exp/PrimBoxing.hs
--- a/DDC/Core/Tetra/Convert/Exp/PrimBoxing.hs
+++ b/DDC/Core/Tetra/Convert/Exp/PrimBoxing.hs
@@ -39,7 +39,7 @@
         --   We fake-up a data-type declaration so we can use the same data layout
         --   code as for user-defined types.
         XApp a _ _
-         | Just ( E.NamePrimCast E.PrimCastConvert
+         | Just ( E.NamePrimCast E.PrimCastConvert False
                 , [XType _ tUx, XType _ tBx, xArg])     <- takeXPrimApps xx
          , isUnboxedRepType tUx
          , isNumericType    tBx
@@ -59,7 +59,7 @@
         --   We fake-up a data-type declaration so we can use the same data layout
         --   code as for used-defined types.
         XApp a _ _
-         | Just ( E.NamePrimCast E.PrimCastConvert
+         | Just ( E.NamePrimCast E.PrimCastConvert False
                 , [XType _ tBx, XType _ tUx, xArg])     <- takeXPrimApps xx
          , isUnboxedRepType tUx
          , isNumericType    tBx
diff --git a/DDC/Core/Tetra/Convert/Exp/PrimCall.hs b/DDC/Core/Tetra/Convert/Exp/PrimCall.hs
--- a/DDC/Core/Tetra/Convert/Exp/PrimCall.hs
+++ b/DDC/Core/Tetra/Convert/Exp/PrimCall.hs
@@ -21,8 +21,7 @@
 
 -- | Convert a Tetra function call primitive to Salt.
 convertPrimCall
-        :: Show a 
-        => ExpContext                   -- ^ The surrounding expression context.
+        :: ExpContext                   -- ^ The surrounding expression context.
         -> Context a                    -- ^ Types and values in the environment.
         -> Exp (AnTEC a E.Name) E.Name  -- ^ Expression to convert.
         -> Maybe (ConvertM a (Exp a A.Name))
diff --git a/DDC/Core/Tetra/Convert/Exp/PrimError.hs b/DDC/Core/Tetra/Convert/Exp/PrimError.hs
--- a/DDC/Core/Tetra/Convert/Exp/PrimError.hs
+++ b/DDC/Core/Tetra/Convert/Exp/PrimError.hs
@@ -15,8 +15,7 @@
 
 -- | Covnert a Tetra error primop to Salt.
 convertPrimError
-        :: Show a
-        => ExpContext                   -- ^ The surrounding expression context.
+        :: ExpContext                   -- ^ The surrounding expression context.
         -> Context a                    -- ^ Types and values in the environment.
         -> Exp (AnTEC a E.Name) E.Name  -- ^ Expression to convert.
         -> Maybe (ConvertM a (Exp a A.Name))
diff --git a/DDC/Core/Tetra/Convert/Exp/PrimVector.hs b/DDC/Core/Tetra/Convert/Exp/PrimVector.hs
--- a/DDC/Core/Tetra/Convert/Exp/PrimVector.hs
+++ b/DDC/Core/Tetra/Convert/Exp/PrimVector.hs
@@ -15,8 +15,7 @@
 
 
 convertPrimVector
-        :: Show a
-        => ExpContext                   -- ^ The surrounding expression context.
+        :: ExpContext                   -- ^ The surrounding expression context.
         -> Context a                    -- ^ Types and values in the environment.
         -> Exp (AnTEC a E.Name) E.Name  -- ^ Expression to convert.
         -> Maybe (ConvertM a (Exp a A.Name))
diff --git a/DDC/Core/Tetra/Convert/Layout.hs b/DDC/Core/Tetra/Convert/Layout.hs
--- a/DDC/Core/Tetra/Convert/Layout.hs
+++ b/DDC/Core/Tetra/Convert/Layout.hs
@@ -12,9 +12,8 @@
 import DDC.Core.Tetra.Convert.Boxing
 import DDC.Core.Tetra.Prim
 import DDC.Core.Salt.Platform
-import DDC.Type.Compounds
+import DDC.Type.Exp.Simple
 import DDC.Type.DataDef
-import DDC.Type.Exp
 import Control.Monad
 import Data.Maybe
 import qualified DDC.Core.Salt.Name     as A
@@ -97,20 +96,25 @@
 fieldSizeOfType    :: Platform -> Type Name -> Maybe Integer
 fieldSizeOfType platform tt
  = case tt of
+        -- Polymorphic objects are represented boxed.
         TVar{}          -> Just $ platformAddrBytes platform
 
+        -- Type constructor might be a primitive or boxed value type.
         TCon tc
          -> case tc of
                 TyConBound (UPrim n _) _ -> fieldSizeOfPrim platform n
                 TyConBound _ _           -> Just $ platformAddrBytes platform
                 _                        -> Nothing
 
-        -- We're not supporting polymorphic fields yet.
-        TForall{}       -> Nothing
+        --- Higher kinded types are not value types.
+        TAbs{}          -> Nothing
 
         -- Assume anything that isn't a primitive constructor is
         -- represented by a pointer.
         TApp{}          -> Just $ platformAddrBytes platform
+
+        -- We're not supporting polymorphic fields yet.
+        TForall{}       -> Nothing
 
         -- We shouldn't find any TSums, because field types always have
         -- kind data.
diff --git a/DDC/Core/Tetra/Convert/Type/Base.hs b/DDC/Core/Tetra/Convert/Type/Base.hs
--- a/DDC/Core/Tetra/Convert/Type/Base.hs
+++ b/DDC/Core/Tetra/Convert/Type/Base.hs
@@ -8,9 +8,10 @@
 import DDC.Core.Tetra.Convert.Error
 import DDC.Type.Exp
 import DDC.Type.DataDef
-import DDC.Control.Monad.Check                  (throw)
+import DDC.Control.Check                        (throw)
 import DDC.Type.Env                             (KindEnv)
 import Data.Set                                 (Set)
+import Data.Map.Strict                          (Map)
 import qualified DDC.Type.Env                   as Env
 import qualified DDC.Core.Tetra.Prim            as E
 import qualified DDC.Core.Salt.Name             as A
@@ -23,6 +24,9 @@
           --   These are all the visible data type definitions, from both
           --   the current module and imported ones.
           contextDataDefs       :: DataDefs E.Name       
+
+          -- | Type equations.
+        , contextTypeEqns       :: Map E.Name (Type E.Name)
 
           -- | Names of foreign boxed data type contructors.
           --   These are names like 'Ref' and 'Array' that are defined in the
diff --git a/DDC/Core/Tetra/Convert/Type/DaCon.hs b/DDC/Core/Tetra/Convert/Type/DaCon.hs
--- a/DDC/Core/Tetra/Convert/Type/DaCon.hs
+++ b/DDC/Core/Tetra/Convert/Type/DaCon.hs
@@ -7,10 +7,8 @@
 import DDC.Core.Tetra.Convert.Type.Data
 import DDC.Core.Tetra.Convert.Type.Base
 import DDC.Core.Tetra.Convert.Error
-import DDC.Core.Exp.Annot.Exp
-import DDC.Type.Compounds
-import DDC.Type.Predicates
-import DDC.Control.Monad.Check                  (throw)
+import DDC.Core.Exp.Annot
+import DDC.Control.Check                        (throw)
 import qualified DDC.Core.Tetra.Prim            as E
 import qualified DDC.Core.Salt.Name             as A
 
@@ -82,7 +80,11 @@
 
 -- DaCon ------------------------------------------------------------------------------------------
 -- | Convert a data constructor definition.
-convertDaCon :: Context -> DaCon E.Name -> ConvertM a (DaCon A.Name)
+convertDaCon 
+        :: Context 
+        -> DaCon E.Name (Type E.Name)
+        -> ConvertM a (DaCon A.Name (Type A.Name))
+
 convertDaCon ctx dc
  = case dc of
         DaConUnit       
@@ -102,7 +104,11 @@
 
 
 -- | Convert the name of a data constructor.
-convertDaConNameM :: DaCon E.Name -> E.Name -> ConvertM a A.Name
+convertDaConNameM 
+        :: DaCon E.Name (Type E.Name)
+        -> E.Name 
+        -> ConvertM a A.Name
+
 convertDaConNameM dc nn
  = case nn of
         E.NameLitUnboxed (E.NameLitBool val)       
diff --git a/DDC/Core/Tetra/Convert/Type/Data.hs b/DDC/Core/Tetra/Convert/Type/Data.hs
--- a/DDC/Core/Tetra/Convert/Type/Data.hs
+++ b/DDC/Core/Tetra/Convert/Type/Data.hs
@@ -9,11 +9,9 @@
 import DDC.Core.Tetra.Convert.Type.Base
 import DDC.Core.Tetra.Convert.Boxing
 import DDC.Core.Tetra.Convert.Error
-import DDC.Core.Exp.Annot.Exp
+import DDC.Core.Exp.Annot
 import DDC.Type.DataDef
-import DDC.Type.Compounds
-import DDC.Type.Predicates
-import DDC.Control.Monad.Check                  (throw)
+import DDC.Control.Check                        (throw)
 import qualified DDC.Core.Tetra.Prim            as E
 import qualified DDC.Core.Salt.Compounds        as A
 import qualified DDC.Core.Salt.Runtime          as A
@@ -23,7 +21,7 @@
 import qualified Data.Map                       as Map
 import qualified Data.Set                       as Set
 import Control.Monad
-import DDC.Base.Pretty
+import DDC.Data.Pretty
 
 
 -- | Convert a value binder with a representable type.
@@ -60,7 +58,7 @@
                   $  Just $ UPrim (A.NamePrimOp (A.PrimArith op)) 
                                   (A.typeOfPrimArith op)
 
-                E.NamePrimCast op
+                E.NamePrimCast op True
                   -> return 
                   $  Just $ UPrim (A.NamePrimOp (A.PrimCast  op)) 
                                   (A.typeOfPrimCast  op)
@@ -94,16 +92,21 @@
              Nothing 
               -> throw $ ErrorUnbound u
 
-        -- We should not find any polymorphic values.
-        TForall{} -> throw $ ErrorMalformed
-                           $ "Invalid polymorphic value type."
-
         -- Convert unapplied type constructors.
         TCon{}    -> convertDataAppT ctx tt
 
+        -- We should not find any type abstractions.
+        TAbs{}    -> throw $ ErrorMalformed $ "Invalid type abstraction."
+
         -- Convert type constructor applications.
         TApp{}    -> convertDataAppT ctx tt
 
+        -- Polymorphic value.
+        TForall bParam tBody
+         -> let kenv'   = Env.extend bParam (contextKindEnv ctx)
+                ctx'    = ctx { contextKindEnv = kenv' }
+            in  convertDataT ctx' tBody
+
         -- Resentable types always have kind Data, but type sums cannot.
         TSum{}    -> throw $ ErrorUnexpectedSum
 
@@ -223,14 +226,24 @@
 
         -- A user-defined data type without a primary region.
         --   These are converted to generic boxed objects in the top-level region.
-        | Just (TyConBound (UName n) _, _)          <- takeTyConApps tt
+        | Just (TyConBound (UName n) _, _) <- takeTyConApps tt
         , Map.member n (dataDefsTypes $ contextDataDefs ctx)
         = do   return  $ A.tPtr A.rTop A.tObj
 
+        -- ISSUE #377: Look through type equations during Tetra to Salt transform.
+        | Just (TyConBound (UName n) _, []) <- takeTyConApps tt
+        , Just t' <- Map.lookup n (contextTypeEqns ctx)
+        = convertDataAppT ctx t'
+
+        -- Application of an abstract type constructor like (m a)
+        -- From the type we can't know what region the object it allocated into.
+        | TVar _ : _    <- takeTApps tt
+        = do    return  $ A.tPtr A.rTop A.tObj
+
         | otherwise
-        =      throw   $ ErrorMalformed 
-                       $  "Invalid type constructor application "
-                       ++ (renderIndent $ ppr tt)
+        = throw   $ ErrorMalformed 
+                  $  "Invalid type constructor application "
+                  ++ (renderIndent $ ppr tt)
 
 
 -- | Convert a primitive type directly to its Salt form.
@@ -247,10 +260,12 @@
 
                 E.PrimTyConTextLit      -> return $ A.tTextLit
 
-                _ -> throw $ ErrorMalformed 
-                           $ "Invalid primitive type " ++ (renderIndent $ ppr tt)
+                _ -> throw $  ErrorMalformed 
+                           $  "Invalid primitive type "
+                           ++ (renderIndent $ ppr tt)
 
         | otherwise
-        = throw $ ErrorMalformed 
-                $ "Invalid primitive type " ++ (renderIndent $ ppr tt)
+        = throw $  ErrorMalformed 
+                $  "Invalid primitive type "
+                ++ (renderIndent $ ppr tt)
 
diff --git a/DDC/Core/Tetra/Convert/Type/Kind.hs b/DDC/Core/Tetra/Convert/Type/Kind.hs
--- a/DDC/Core/Tetra/Convert/Type/Kind.hs
+++ b/DDC/Core/Tetra/Convert/Type/Kind.hs
@@ -7,8 +7,8 @@
 import DDC.Core.Tetra.Convert.Type.Base
 import DDC.Core.Tetra.Convert.Error
 import DDC.Type.Exp
-import DDC.Base.Pretty
-import DDC.Control.Monad.Check                  (throw)
+import DDC.Data.Pretty
+import DDC.Control.Check                        (throw)
 import Control.Monad
 import qualified DDC.Core.Tetra.Prim            as E
 import qualified DDC.Core.Salt.Name             as A
diff --git a/DDC/Core/Tetra/Convert/Type/Region.hs b/DDC/Core/Tetra/Convert/Type/Region.hs
--- a/DDC/Core/Tetra/Convert/Type/Region.hs
+++ b/DDC/Core/Tetra/Convert/Type/Region.hs
@@ -5,16 +5,14 @@
 where
 import DDC.Core.Tetra.Convert.Type.Base
 import DDC.Core.Tetra.Convert.Error
-import DDC.Core.Exp.Annot.Exp
+import DDC.Core.Exp.Annot
 import DDC.Type.Env
-import DDC.Type.Compounds
-import DDC.Type.Predicates
-import DDC.Control.Monad.Check                  (throw)
+import DDC.Control.Check                        (throw)
 import qualified DDC.Core.Tetra.Prim            as E
 import qualified DDC.Core.Salt.Runtime          as A
 import qualified DDC.Core.Salt.Name             as A
 import qualified DDC.Type.Env                   as Env
-import DDC.Base.Pretty
+import DDC.Data.Pretty
        
 
 -- Region Types -----------------------------------------------------------------------------------
@@ -35,36 +33,14 @@
 -- | Given the type of some data value, determine what prime region to use 
 --   for the object in the Salt language. The supplied type must have kind
 --   Data, else you'll get a bogus result.
---
---   Boxed data types whose first parameter is a region, by convention that
---   region is the prime one.
---     List r1 a  =>  r1 
---
---   Boxed data types that do not have a region as the first parameter,
---   these are allocated into the top-level region.
---     Unit       => rTop
---     B# Nat#    => rTop
---     
---   Functions are also allocated into the top-level region.
---     a -> b     => rTop
---     forall ... => rTop
---
---   For completely parametric data types we use a region named after the
---   associated type variable.
---     a          => a$r
---
---   For types with an abstract constructor, we currently reject them outright.
---   There's no way to tell what region an object of such a type should be 
---   allocated into. In future we should add a supertype of regions, and treat
---   such objects as belong to the Any region.
---   See [Note: Salt conversion for higher kinded type arguments]
---     c a b      => ** NOTHING **
+-- 
+--   NOTE: This used to do something more useful, but was changed so that
+--   all values go into rTop. The problem is that given a type like (m Nat)
+--   we can't know what region the value will be allocated into as the
+--   type is too polymorphic. We need to implement a region subtyping system
+--   so that the Top region can be treated as an Any/DontKnow specifier
+--   rather than a specific region that is distinct from all others.
 --   
---   Unboxed and index types don't refer to boxed objects, so they don't have
---   associated prime regions.
---     Nat#       => ** NOTHING **
---     U# Nat#    => ** NOTHING **
---
 saltPrimeRegionOfDataType
         :: KindEnv E.Name 
         -> Type E.Name 
@@ -75,24 +51,29 @@
         | TCon _ : TVar u : _   <- takeTApps tt
         , Just k                <- Env.lookup u kenv
         , isRegionKind k
-        = do    -- u'      <- convertTypeU u
-                return  A.rTop
-
-        -- Boxed data types without an attached primary region variable.
-        -- This also covers the function case.
-        | TCon _ : _           <- takeTApps tt
         = do    return  A.rTop
 
-        -- Quantified types.
-        | TForall{}     <- tt
-        = do    return  A.rTop
-
         -- Completely parametric data types.
         | TVar u        <- tt
         , Just k        <- Env.lookup u kenv
         , isDataKind k
         = do    return  A.rTop
 
+        -- Boxed data types without an attached primary region variable.
+        --   For applications of abstract type constructors like in 
+        --   (m Nat), we can't know what constructor 'm' will be instantiated
+        --   with, nor what region the resulting value will be allocated into.
+        | TCon{}  <- tt
+        = do    return  A.rTop
+
+        | TApp{}   <- tt
+        = do    return  A.rTop
+
+        -- Quantified types.
+        | TForall{}     <- tt
+        = do    return  A.rTop
+
+        -- Type variable which is not in the environment.
         | otherwise
         = throw $ ErrorMalformed       
                 $ "Cannot take prime region from " ++ (renderIndent $ ppr tt)
diff --git a/DDC/Core/Tetra/Convert/Type/Super.hs b/DDC/Core/Tetra/Convert/Type/Super.hs
--- a/DDC/Core/Tetra/Convert/Type/Super.hs
+++ b/DDC/Core/Tetra/Convert/Type/Super.hs
@@ -7,9 +7,7 @@
 import DDC.Core.Tetra.Convert.Type.Base
 import DDC.Core.Tetra.Convert.Error
 import DDC.Core.Call
-import DDC.Core.Exp.Annot.Exp
-import DDC.Type.Compounds
-import DDC.Type.Predicates
+import DDC.Core.Exp.Annot
 import qualified DDC.Core.Tetra.Prim            as E
 import qualified DDC.Core.Salt.Name             as A
 
diff --git a/DDC/Core/Tetra/Convert/Type/Witness.hs b/DDC/Core/Tetra/Convert/Type/Witness.hs
--- a/DDC/Core/Tetra/Convert/Type/Witness.hs
+++ b/DDC/Core/Tetra/Convert/Type/Witness.hs
@@ -6,13 +6,12 @@
 import DDC.Core.Tetra.Convert.Type.Region
 import DDC.Core.Tetra.Convert.Type.Base
 import DDC.Core.Tetra.Convert.Error
-import DDC.Core.Exp.Annot.Exp
-import DDC.Type.Compounds
-import DDC.Control.Monad.Check                  (throw)
+import DDC.Core.Exp.Annot
+import DDC.Control.Check                        (throw)
 import qualified DDC.Core.Tetra.Prim            as E
 import qualified DDC.Core.Salt.Name             as A
 import Control.Monad
-import DDC.Base.Pretty
+import DDC.Data.Pretty
 
 
 -- | Convert a witness binder.
diff --git a/DDC/Core/Tetra/Env.hs b/DDC/Core/Tetra/Env.hs
--- a/DDC/Core/Tetra/Env.hs
+++ b/DDC/Core/Tetra/Env.hs
@@ -10,7 +10,6 @@
 import DDC.Core.Tetra.Prim
 import DDC.Core.Tetra.Compounds
 import DDC.Type.DataDef
-import DDC.Type.Exp
 import DDC.Type.Env             (Env)
 import qualified DDC.Type.Env   as Env
 
@@ -125,26 +124,27 @@
 typeOfPrimName :: Name -> Maybe (Type Name)
 typeOfPrimName dc
  = case dc of
-        NameDaConTetra p                        -> Just $ typeDaConTetra    p
-        NameOpFun      p                        -> Just $ typeOpFun         p
-        NameOpVector   p f                      -> Just $ typeOpVectorFlag  p f
-        NameOpError    p f                      -> Just $ typeOpErrorFlag   p f
-        NamePrimArith  p f                      -> Just $ typePrimArithFlag p f
-        NamePrimCast   p                        -> Just $ typePrimCast      p
+        NameDaConTetra  p                    -> Just $ typeDaConTetra    p
+        NameOpFun       p                    -> Just $ typeOpFun         p
+        NameOpVector    p f                  -> Just $ typeOpVectorFlag  p f
+        NameOpError     p f                  -> Just $ typeOpErrorFlag   p f
+        NamePrimArith   p f                  -> Just $ typePrimArithFlag p f
+        NamePrimCast    p f                  -> Just $ typePrimCastFlag  p f
 
-        NameLitBool _                           -> Just $ tBool
-        NameLitNat  _                           -> Just $ tNat
-        NameLitInt  _                           -> Just $ tInt
-        NameLitWord _ bits                      -> Just $ tWord bits
-        NameLitFloat _ bits                     -> Just $ tFloat bits
-        NameLitTextLit _                        -> Just $ tTextLit
+        NameLitBool     _                    -> Just $ tBool
+        NameLitNat      _                    -> Just $ tNat
+        NameLitInt      _                    -> Just $ tInt
+        NameLitWord     _ bits               -> Just $ tWord bits
+        NameLitFloat    _ bits               -> Just $ tFloat bits
+        NameLitChar     _                    -> Just $ tWord 32
+        NameLitTextLit  _                    -> Just $ tTextLit
 
-        NameLitUnboxed NameLitBool{}            -> Just $ tUnboxed tBool
-        NameLitUnboxed NameLitNat{}             -> Just $ tUnboxed tNat
-        NameLitUnboxed NameLitInt{}             -> Just $ tUnboxed tInt
-        NameLitUnboxed (NameLitWord  _ bits)    -> Just $ tUnboxed (tWord bits)
-        NameLitUnboxed (NameLitFloat _ bits)    -> Just $ tUnboxed (tFloat bits)
-        NameLitUnboxed NameLitTextLit{}         -> Just $ tUnboxed tTextLit
+        NameLitUnboxed NameLitBool{}         -> Just $ tUnboxed tBool
+        NameLitUnboxed NameLitNat{}          -> Just $ tUnboxed tNat
+        NameLitUnboxed NameLitInt{}          -> Just $ tUnboxed tInt
+        NameLitUnboxed (NameLitWord  _ bits) -> Just $ tUnboxed (tWord bits)
+        NameLitUnboxed (NameLitFloat _ bits) -> Just $ tUnboxed (tFloat bits)
+        NameLitUnboxed NameLitTextLit{}      -> Just $ tUnboxed tTextLit
 
-        _                                       -> Nothing
+        _                                    -> Nothing
 
diff --git a/DDC/Core/Tetra/Prim.hs b/DDC/Core/Tetra/Prim.hs
--- a/DDC/Core/Tetra/Prim.hs
+++ b/DDC/Core/Tetra/Prim.hs
@@ -19,9 +19,6 @@
         , DaConTetra     (..)
         , readDaConTetra
         , typeDaConTetra
-        , xTuple2
-        , dcTuple2
-        , dcTupleN 
 
           -- * Baked-in function operators.
         , OpFun         (..)
@@ -51,8 +48,8 @@
 
           -- * Primitive numeric casts.
         , PrimCast      (..)
-        , readPrimCast
-        , typePrimCast)
+        , readPrimCastFlag
+        , typePrimCastFlag)
 where
 import DDC.Core.Tetra.Prim.Base
 import DDC.Core.Tetra.Prim.TyConTetra
@@ -63,15 +60,15 @@
 import DDC.Core.Tetra.Prim.OpCast
 import DDC.Core.Tetra.Prim.OpFun
 import DDC.Core.Tetra.Prim.OpVector
-import DDC.Data.ListUtils
 import DDC.Type.Exp
-import DDC.Base.Pretty
-import DDC.Base.Name
+import DDC.Data.ListUtils
+import DDC.Data.Pretty
+import DDC.Data.Name
 import Control.DeepSeq
 import Data.Char        
 import qualified Data.Text              as T
 
-import DDC.Core.Lexer.Names             (isVarStart)
+import DDC.Core.Lexer.Tokens            (isVarStart)
 import DDC.Core.Salt.Name 
         ( readLitNat
         , readLitInt
@@ -93,7 +90,7 @@
 
         NamePrimTyCon  op       -> rnf op
         NamePrimArith  op !_    -> rnf op
-        NamePrimCast   op       -> rnf op
+        NamePrimCast   op !_    -> rnf op
 
         NameLitBool    b        -> rnf b
         NameLitNat     n        -> rnf n
@@ -101,6 +98,7 @@
         NameLitSize    s        -> rnf s
         NameLitWord    i bits   -> rnf i `seq` rnf bits
         NameLitFloat   d bits   -> rnf d `seq` rnf bits
+        NameLitChar    c        -> rnf c
         NameLitTextLit bs       -> rnf bs       
 
         NameLitUnboxed n        -> rnf n
@@ -121,7 +119,6 @@
         NameOpError    op False -> ppr op
         NameOpError    op True  -> ppr op <> text "#"
 
-
         NameOpFun      op       -> ppr op
 
         NameOpVector   op False -> ppr op
@@ -132,16 +129,18 @@
         NamePrimArith  op False -> ppr op
         NamePrimArith  op True  -> ppr op <> text "#"
 
-        NamePrimCast   op       -> ppr op
+        NamePrimCast   op False -> ppr op
+        NamePrimCast   op True  -> ppr op <> text "#"
 
-        NameLitBool True        -> text "True#"
-        NameLitBool False       -> text "False#"
-        NameLitNat  i           -> integer i
-        NameLitInt  i           -> integer i <> text "i"
-        NameLitSize    s        -> integer s <> text "s"
-        NameLitWord    i bits   -> integer i <> text "w" <> int bits
-        NameLitFloat   f bits   -> double  f <> text "f" <> int bits
-        NameLitTextLit tx       -> text (show $ T.unpack tx)
+        NameLitBool    True     -> text "True#"
+        NameLitBool    False    -> text "False#"
+        NameLitNat     i        -> integer i                            <> text "#"
+        NameLitInt     i        -> integer i <> text "i"                <> text "#"
+        NameLitSize    s        -> integer s <> text "s"                <> text "#"
+        NameLitWord    i bits   -> integer i <> text "w" <> int bits    <> text "#"
+        NameLitFloat   f bits   -> double  f <> text "f" <> int bits    <> text "#"
+        NameLitChar    c        -> text (show c)                        <> text "#"
+        NameLitTextLit tx       -> text (show $ T.unpack tx)            <> text "#"
 
         NameLitUnboxed n        -> ppr n <> text "#"
 
@@ -152,6 +151,9 @@
  extendName n str       
   = NameExt n str
  
+ newVarName str
+  = NameVar str
+
  splitName nn
   = case nn of
         NameExt n str   -> Just (n, str)
@@ -178,14 +180,14 @@
         = Just $ NameOpVector p f
 
         -- Primitive names.
-        | Just p <- readPrimTyCon str  
+        | Just p      <- readPrimTyCon     str  
         = Just $ NamePrimTyCon p
 
         | Just (p, f) <- readPrimArithFlag str  
         = Just $ NamePrimArith p f
 
-        | Just p <- readPrimCast  str
-        = Just $ NamePrimCast  p
+        | Just (p, f) <- readPrimCastFlag  str
+        = Just $ NamePrimCast  p f
 
         -- Literal Bools
         | str == "True"  = Just $ NameLitBool True
@@ -253,6 +255,6 @@
         NameOpFun       op      -> Just (typeOpFun         op)
         NameOpVector    op f    -> Just (typeOpVectorFlag  op f)
         NamePrimArith   op f    -> Just (typePrimArithFlag op f)
-        NamePrimCast    op      -> Just (typePrimCast      op)
+        NamePrimCast    op f    -> Just (typePrimCastFlag  op f)
         _                       -> Nothing
 
diff --git a/DDC/Core/Tetra/Prim/Base.hs b/DDC/Core/Tetra/Prim/Base.hs
--- a/DDC/Core/Tetra/Prim/Base.hs
+++ b/DDC/Core/Tetra/Prim/Base.hs
@@ -58,12 +58,14 @@
 
         -- | Primitive arithmetic, logic, comparison and
         --   bit-wise operators.
-        --   The flag indicates whether this is the boxed
-        --   (False) or unboxed (True) version.
+        --   The flag indicates whether this is the
+        --   boxed (False) or unboxed (True) version.
         | NamePrimArith         !PrimArith      !Bool
 
         -- | Primitive numeric casting operators.
-        | NamePrimCast          !PrimCast
+        --   The flat indicates whether this is the 
+        --   boxed (False) or unboxed (True) version.
+        | NamePrimCast          !PrimCast       !Bool
 
         -- Literals -----------------------------
         -- | A boolean literal.
@@ -89,6 +91,11 @@
         --   with the given number of bits precision.
         | NameLitFloat          !Double  !Int
 
+        -- | A character literal,
+        --   These are special syntax for a Word32 expressing a
+        --   Unicode codepoint.
+        | NameLitChar           !Char
+
         -- | A text literal (UTF-8 encoded)
         --   Note that 'Text' and 'TextLit#' are different types. 
         --   The later is the primitive literal.
@@ -122,6 +129,7 @@
         NameLitSize{}    -> True
         NameLitWord{}    -> True
         NameLitFloat{}   -> True
+        NameLitChar{}    -> True
         NameLitTextLit{} -> True
         NameLitUnboxed n -> isNameLit n
         _                -> False
diff --git a/DDC/Core/Tetra/Prim/DaConTetra.hs b/DDC/Core/Tetra/Prim/DaConTetra.hs
--- a/DDC/Core/Tetra/Prim/DaConTetra.hs
+++ b/DDC/Core/Tetra/Prim/DaConTetra.hs
@@ -1,16 +1,12 @@
 
 module DDC.Core.Tetra.Prim.DaConTetra
         ( typeDaConTetra
-        , readDaConTetra
-        , xTuple2
-        , dcTuple2
-        , dcTupleN )
+        , readDaConTetra)
 where
 import DDC.Core.Tetra.Prim.Base
 import DDC.Core.Tetra.Prim.TyConTetra
-import DDC.Core.Exp.Simple.Compounds
-import DDC.Core.Exp.Simple.Exp
-import DDC.Base.Pretty
+import DDC.Type.Exp.Simple
+import DDC.Data.Pretty
 import Control.DeepSeq
 import Data.Char
 import Data.List
@@ -44,28 +40,4 @@
 typeDaConTetra (DaConTetraTuple n)
         = tForalls (replicate n kData)
         $ \args -> foldr tFun (tTupleN args) args
-
-
--- | Construct a @Tuple2#@
-xTuple2 :: Type Name  -> Type Name 
-        -> Exp a Name -> Exp a Name 
-        -> Exp a Name
-
-xTuple2 t1 t2 x1 x2
-        = xApps (XCon dcTuple2) 
-                [XType t1, XType t2, x1, x2]
-
-
--- | Data constructor for @Tuple2#@
-dcTuple2 :: DaCon Name
-dcTuple2  = DaConPrim   (NameDaConTetra (DaConTetraTuple 2))
-                        (typeDaConTetra (DaConTetraTuple 2))
-
-
--- | Data constructor for n-tuples
-dcTupleN :: Int -> DaCon Name
-dcTupleN n
-          = DaConPrim   (NameDaConTetra (DaConTetraTuple n))
-                        (typeDaConTetra (DaConTetraTuple n))
-
 
diff --git a/DDC/Core/Tetra/Prim/OpArith.hs b/DDC/Core/Tetra/Prim/OpArith.hs
--- a/DDC/Core/Tetra/Prim/OpArith.hs
+++ b/DDC/Core/Tetra/Prim/OpArith.hs
@@ -6,8 +6,7 @@
 import DDC.Core.Tetra.Prim.TyConTetra
 import DDC.Core.Tetra.Prim.TyConPrim
 import DDC.Core.Tetra.Prim.Base
-import DDC.Type.Compounds
-import DDC.Type.Exp
+import DDC.Type.Exp.Simple
 import Data.List
 
 
diff --git a/DDC/Core/Tetra/Prim/OpCast.hs b/DDC/Core/Tetra/Prim/OpCast.hs
--- a/DDC/Core/Tetra/Prim/OpCast.hs
+++ b/DDC/Core/Tetra/Prim/OpCast.hs
@@ -1,24 +1,49 @@
 
 module DDC.Core.Tetra.Prim.OpCast
-        ( readPrimCast
-        , typePrimCast)
+        ( readPrimCastFlag
+        , typePrimCastFlag)
 where
+import DDC.Core.Tetra.Prim.TyConTetra
 import DDC.Core.Tetra.Prim.Base
-import DDC.Type.Compounds
-import DDC.Type.Exp
-import DDC.Core.Salt.Name       (readPrimCast)
+import DDC.Type.Exp.Simple
+import Data.List
 
 
 -- | Take the type of a primitive numeric cast operator.
-typePrimCast :: PrimCast -> Type Name
-typePrimCast op
- = case op of
+typePrimCastFlag :: PrimCast -> Bool -> Type Name
+typePrimCastFlag op bUnboxed
+ = let  fb | bUnboxed   = tUnboxed
+           | otherwise  = id
+
+   in case op of
         PrimCastConvert  
-         -> tForalls [kData, kData] $ \[t1, t2] -> t1 `tFun` t2
+         -> tForalls [kData, kData] $ \[t1, t2] -> fb t1 `tFun` fb t2
 
         PrimCastPromote  
-         -> tForalls [kData, kData] $ \[t1, t2] -> t1 `tFun` t2
+         -> tForalls [kData, kData] $ \[t1, t2] -> fb t2 `tFun` fb t1
 
         PrimCastTruncate 
-         -> tForalls [kData, kData] $ \[t1, t2] -> t1 `tFun` t2
+         -> tForalls [kData, kData] $ \[t1, t2] -> fb t2 `tFun` fb t1
+
+
+-- | Read a primitive cast operator.
+readPrimCastFlag :: String -> Maybe (PrimCast, Bool)
+readPrimCastFlag str
+  =  case find (\(_, n) -> str == n) primCastNames of
+        Just (p, _)     -> Just p
+        _               -> Nothing
+
+
+-- | Names of primitve operators.
+primCastNames :: [((PrimCast, Bool), String)]
+primCastNames
+ = concat 
+        $ [ [ ((p, False),  str)
+            , ((p, True),   str ++ "#")]  
+          | (p, str) <- table]
+ where
+  table 
+   =    [ (PrimCastPromote,     "promote#")
+        , (PrimCastTruncate,    "truncate#")
+        , (PrimCastConvert,     "convert#") ]
 
diff --git a/DDC/Core/Tetra/Prim/OpError.hs b/DDC/Core/Tetra/Prim/OpError.hs
--- a/DDC/Core/Tetra/Prim/OpError.hs
+++ b/DDC/Core/Tetra/Prim/OpError.hs
@@ -7,9 +7,8 @@
 import DDC.Core.Tetra.Prim.TyConTetra
 import DDC.Core.Tetra.Prim.TyConPrim
 import DDC.Core.Tetra.Prim.Base
-import DDC.Type.Compounds
-import DDC.Type.Exp
-import DDC.Base.Pretty
+import DDC.Type.Exp.Simple
+import DDC.Data.Pretty
 import Control.DeepSeq
 
 
diff --git a/DDC/Core/Tetra/Prim/OpFun.hs b/DDC/Core/Tetra/Prim/OpFun.hs
--- a/DDC/Core/Tetra/Prim/OpFun.hs
+++ b/DDC/Core/Tetra/Prim/OpFun.hs
@@ -6,9 +6,8 @@
 where
 import DDC.Core.Tetra.Prim.TyConTetra
 import DDC.Core.Tetra.Prim.Base
-import DDC.Type.Compounds
-import DDC.Type.Exp
-import DDC.Base.Pretty
+import DDC.Type.Exp.Simple
+import DDC.Data.Pretty
 import Control.DeepSeq
 import Data.Char
 import Data.List
diff --git a/DDC/Core/Tetra/Prim/OpVector.hs b/DDC/Core/Tetra/Prim/OpVector.hs
--- a/DDC/Core/Tetra/Prim/OpVector.hs
+++ b/DDC/Core/Tetra/Prim/OpVector.hs
@@ -6,9 +6,8 @@
 import DDC.Core.Tetra.Prim.TyConTetra
 import DDC.Core.Tetra.Prim.TyConPrim
 import DDC.Core.Tetra.Prim.Base
-import DDC.Type.Compounds
-import DDC.Type.Exp
-import DDC.Base.Pretty
+import DDC.Type.Exp.Simple
+import DDC.Data.Pretty
 import Control.DeepSeq
 
 
diff --git a/DDC/Core/Tetra/Prim/TyConPrim.hs b/DDC/Core/Tetra/Prim/TyConPrim.hs
--- a/DDC/Core/Tetra/Prim/TyConPrim.hs
+++ b/DDC/Core/Tetra/Prim/TyConPrim.hs
@@ -11,8 +11,7 @@
         , tTextLit)
 where
 import DDC.Core.Tetra.Prim.Base
-import DDC.Core.Exp.Annot.Compounds
-import DDC.Core.Exp.Simple.Exp
+import DDC.Core.Exp.Annot
 import DDC.Core.Salt.Name
         ( pprPrimTyConStem
         , readPrimTyCon, readPrimTyConStem)
diff --git a/DDC/Core/Tetra/Prim/TyConTetra.hs b/DDC/Core/Tetra/Prim/TyConTetra.hs
--- a/DDC/Core/Tetra/Prim/TyConTetra.hs
+++ b/DDC/Core/Tetra/Prim/TyConTetra.hs
@@ -9,9 +9,8 @@
         , tCloValue)
 where
 import DDC.Core.Tetra.Prim.Base
-import DDC.Core.Exp.Simple.Exp
-import DDC.Type.Compounds
-import DDC.Base.Pretty
+import DDC.Type.Exp.Simple
+import DDC.Data.Pretty
 import Control.DeepSeq
 import Data.List
 import Data.Char
diff --git a/DDC/Core/Tetra/Profile.hs b/DDC/Core/Tetra/Profile.hs
--- a/DDC/Core/Tetra/Profile.hs
+++ b/DDC/Core/Tetra/Profile.hs
@@ -12,11 +12,12 @@
 import DDC.Core.Fragment
 import DDC.Core.Lexer
 import DDC.Type.Exp
-import DDC.Data.Token
 import Control.Monad.State.Strict
 import DDC.Type.Env             (Env)
+import DDC.Data.SourcePos       
 import qualified DDC.Type.Env   as Env
 
+
 -- | Language profile for Disciple Core Tetra.
 profile :: Profile Name 
 profile
@@ -28,9 +29,25 @@
         , profilePrimTypes              = primTypeEnv
         , profileTypeIsUnboxed          = const False 
         , profileNameIsHole             = Just isNameHole 
-        , profileMakeStringName         = Just (\_ t -> NameLitTextLit t) }
+        , profileMakeLiteralName        = Just makeLiteralName }
 
 
+-- | Convert a literal to a Tetra name.
+makeLiteralName :: SourcePos -> Literal -> Bool -> Maybe Name
+makeLiteralName _ lit True
+ = case lit of
+        LNat    n       -> Just $ NameLitNat     n
+        LInt    i       -> Just $ NameLitInt     i
+        LSize   s       -> Just $ NameLitSize    s
+        LWord   i b     -> Just $ NameLitWord    i b
+        LFloat  f b     -> Just $ NameLitFloat   f b
+        LChar   c       -> Just $ NameLitChar    c
+        LString tx      -> Just $ NameLitTextLit tx
+
+makeLiteralName _ _ _
+ = Nothing
+
+
 features :: Features
 features 
         = Features
@@ -62,25 +79,27 @@
 -- | Lex a string to tokens, using primitive names.
 --
 --   The first argument gives the starting source line number.
-lexModuleString :: String -> Int -> String -> [Token (Tok Name)]
+lexModuleString :: String -> Int -> String -> [Located (Token Name)]
 lexModuleString sourceName lineStart str
  = map rn $ lexModuleWithOffside sourceName lineStart str
- where rn (Token strTok sp) 
-        = case renameTok readName strTok of
-                Just t' -> Token t' sp
-                Nothing -> Token (KErrorJunk "lexical error") sp
+ where
+        rn (Located sp strTok) 
+         = case renameToken readName strTok of
+                Just t' -> Located sp t'
+                Nothing -> Located sp (KErrorJunk "lexical error")
 
 
 -- | Lex a string to tokens, using primitive names.
 --
 --   The first argument gives the starting source line number.
-lexExpString :: String -> Int -> String -> [Token (Tok Name)]
+lexExpString :: String -> Int -> String -> [Located (Token Name)]
 lexExpString sourceName lineStart str
  = map rn $ lexExp sourceName lineStart str
- where rn (Token strTok sp) 
-        = case renameTok readName strTok of
-                Just t' -> Token t' sp
-                Nothing -> Token (KErrorJunk "lexical error") sp
+ where 
+        rn (Located sp strTok) 
+         = case renameToken readName strTok of
+                Just t' -> Located sp t'
+                Nothing -> Located sp (KErrorJunk "lexical error")
 
 
 -- | Create a new type variable name that is not in the given environment.
diff --git a/DDC/Core/Tetra/Transform/Boxing.hs b/DDC/Core/Tetra/Transform/Boxing.hs
--- a/DDC/Core/Tetra/Transform/Boxing.hs
+++ b/DDC/Core/Tetra/Transform/Boxing.hs
@@ -5,13 +5,12 @@
 import DDC.Core.Tetra.Compounds
 import DDC.Core.Tetra.Prim
 import DDC.Core.Module
-import DDC.Core.Exp
 import DDC.Core.Transform.Boxing           (Rep(..), Config(..))
 import qualified DDC.Core.Transform.Boxing as Boxing
 
 
 -- | Manage boxing of numeric values in a module.
-boxingModule :: Show a => Module a Name -> Module a Name
+boxingModule :: Module a Name -> Module a Name
 boxingModule mm 
  = let
         tsForeignSea    
@@ -118,19 +117,11 @@
 unboxPrimOpName :: Name -> Maybe Name
 unboxPrimOpName n
  = case n of
-        -- The types of arithmetic operators are already polytypic,
-        -- and can be instantiated at either value types or unboxed types.
-        NamePrimArith op False 
-          -> Just $ NamePrimArith op True
-
-        -- The types of vector operators have different value type and unboxed versions.
-        NameOpVector  op False
-          -> Just $ NameOpVector  op True
-
-        NameOpError   op False
-          -> Just $ NameOpError   op True
-
-        _ -> Nothing
+        NamePrimArith op False  -> Just $ NamePrimArith op True
+        NamePrimCast  op False  -> Just $ NamePrimCast  op True
+        NameOpVector  op False  -> Just $ NameOpVector  op True
+        NameOpError   op False  -> Just $ NameOpError   op True
+        _                       -> Nothing
 
 
 -- | If this is the name of an literal, then produce the unboxed version.
diff --git a/DDC/Core/Tetra/Transform/Curry.hs b/DDC/Core/Tetra/Transform/Curry.hs
--- a/DDC/Core/Tetra/Transform/Curry.hs
+++ b/DDC/Core/Tetra/Transform/Curry.hs
@@ -8,10 +8,13 @@
 import DDC.Core.Tetra.Prim
 import DDC.Core.Transform.Reannotate
 import DDC.Core.Exp.Annot.AnTEC
+import DDC.Core.Tetra.Profile
 import DDC.Core.Module
 import DDC.Core.Exp.Annot
 import Data.Maybe
 import Data.Map                                 (Map)
+import DDC.Core.Env.EnvT                        (EnvT)
+import qualified DDC.Core.Fragment              as C
 import qualified DDC.Core.Call                  as Call
 import qualified Data.Map.Strict                as Map
 import qualified Data.List                      as List
@@ -23,11 +26,16 @@
 --   over applied, and build and evaluate closures as necessary.
 --
 curryModule 
-        :: Module (AnTEC a Name) Name 
+        :: Show a
+        => Module (AnTEC a Name) Name   -- ^ Module to transform.
         -> Either Error (Module () Name)
 
 curryModule mm
  = do
+        -- Extract the top-level environment for types from the module.
+        let kenv  = C.profilePrimKinds profile
+        let envt  = moduleEnvT kenv mm
+
         -- Add all the foreign functions to the function map.
         -- We can do a saturated call for these directly.
         callables <- fmap (Map.fromList . catMaybes)
@@ -35,7 +43,7 @@
                   $  moduleImportValues mm
 
         -- Apply curry transform in the body of the module.
-        xBody'    <- curryBody callables
+        xBody'    <- curryBody envt callables
                   $  moduleBody mm
 
         return  $ mm { moduleBody = xBody' }
@@ -43,11 +51,13 @@
 
 -- | Manage higher-order functions in a module body.
 curryBody 
-        :: Map Name Callable
-        -> Exp (AnTEC a Name) Name 
+        :: Show a
+        => EnvT Name                    -- ^ Current type environment.
+        -> Map Name Callable            -- ^ Map of directly callable supers
+        -> Exp (AnTEC a Name) Name      -- ^ Expression to transform.
         -> Either Error (Exp () Name)
 
-curryBody callables xx
+curryBody envt callables xx
  = case xx of
         XLet _ (LRec bxs) xBody
          -> do  let (bs, xs) = unzip bxs
@@ -60,24 +70,26 @@
                         = Map.union csSuper callables
 
                 -- Rewrite bindings in the body of the let-expression.
-                xs'      <- mapM (curryX callables') xs
+                xs'      <- mapM (curryX envt callables') xs
                 let bxs' =  zip bs xs'
-                xBody'   <- curryBody callables' xBody
+                xBody'   <- curryBody envt callables' xBody
                 return   $  XLet () (LRec bxs') xBody'
 
         _ ->    return   $ reannotate (const ()) xx
 
 
 -- | Manage function application in an expression.
-curryX  :: Map Name Callable
-        -> Exp (AnTEC a Name) Name 
+curryX  :: Show a
+        => EnvT Name                    -- ^ Current type environment.
+        -> Map Name Callable            -- ^ Map of directly callable supers.
+        -> Exp (AnTEC a Name) Name      -- ^ Expression to transform.
         -> Either Error (Exp () Name)
 
-curryX callables xx
- = let down x = curryX callables x
+curryX envt callables xx
+ = let down x = curryX envt callables x
    in case xx of
         XVar  a (UName nF)
-         -> do  result  <- makeCall callables nF (annotType a) []
+         -> do  result    <- makeCall envt callables nF (annotType a) []
                 case result of 
                  Just xx' -> return xx'
                  Nothing  -> return $ XVar () (UName nF)
@@ -86,13 +98,13 @@
          ->     return $ XVar () u
 
         XApp  _ x1 x2
-         -> do  result  <- curryX_call callables xx
+         -> do  result  <- curryX_call envt callables xx
                 case result of
-                 Just xx' -> return xx'
-                 Nothing  -> XApp () <$> down x1 <*> down x2
+                    Just xx' -> return xx'
+                    Nothing  -> XApp () <$> down x1 <*> down x2
 
         XCast _ CastRun x1
-         -> do  result  <- curryX_call callables xx
+         -> do  result  <- curryX_call envt callables xx
                 case result of
                  Just xx' -> return xx'
                  Nothing  -> XCast () CastRun    <$> down x1
@@ -103,33 +115,33 @@
 
         XLam     _ b xBody   
          -> let callables' = shadowCallables [b] callables
-            in  XLam () b <$> curryX   callables' xBody
+            in  XLam () b <$> curryX   envt callables' xBody
 
         XLAM     _ b xBody
-         ->     XLAM () b <$> curryX   callables  xBody
+         ->     XLAM () b <$> curryX   envt callables  xBody
 
         XLet     _ lts@(LLet b _) xBody
          -> let callables' = shadowCallables [b] callables
-            in  XLet  ()  <$> curryLts callables' lts 
-                          <*> curryX   callables' xBody
+            in  XLet  ()  <$> curryLts envt callables' lts 
+                          <*> curryX   envt callables' xBody
 
         XLet     _ lts@(LRec bxs) xBody
          -> let bs         = map fst bxs
                 callables' = shadowCallables bs callables
-            in  XLet  ()  <$> curryLts callables' lts
-                          <*> curryX   callables' xBody
+            in  XLet  ()  <$> curryLts envt callables' lts
+                          <*> curryX   envt callables' xBody
 
         XLet     _ lts@(LPrivate{}) xBody
-         ->     XLet  ()  <$> curryLts callables  lts
-                          <*> curryX   callables  xBody
+         ->     XLet  ()  <$> curryLts envt callables  lts
+                          <*> curryX   envt callables  xBody
 
         XCase    _ x as
          ->     XCase ()  <$> down x
-                          <*> mapM (curryAlt callables) as
+                          <*> mapM (curryAlt envt callables) as
 
         XCast    _ c xBody
          ->     XCast ()  <$> return (reannotate (const ()) c)
-                          <*> curryX callables xBody
+                          <*> curryX envt callables xBody
 
         XType    _ t
          -> return $ XType    () t
@@ -150,19 +162,20 @@
 
 -- | Build a function call for the given application expression.
 curryX_call 
-        :: Map Name Callable
+        :: Show a
+        => EnvT Name
+        -> Map Name Callable
         -> Exp (AnTEC a Name) Name 
         -> Either Error (Maybe (Exp () Name))
 
-curryX_call callables xx
-
+curryX_call envt callables xx
  -- If this is a call of a named function then split it into the
  --  functional part and arguments, then work out how to call it.
  | (xF, esArgs)         <- Call.takeCallElim xx
  , XVar aF (UName nF)   <- xF
  , length esArgs  > 0
  = do   esArgs'   <- mapM downElim esArgs
-        makeCall callables nF (annotType aF) esArgs'
+        makeCall envt callables nF (annotType aF) esArgs'
 
  | otherwise
  = return $ Nothing
@@ -174,25 +187,27 @@
 
                 Call.ElimValue _ x   
                  ->  Call.ElimValue () 
-                 <$> curryX callables x
+                 <$> curryX envt callables x
 
                 Call.ElimRun   _
                  -> return $ Call.ElimRun   ()
 
 
 -- | Manage function application in a let binding.
-curryLts :: Map Name Callable 
+curryLts :: Show a
+         => EnvT Name 
+         -> Map Name Callable 
          -> Lets (AnTEC a Name) Name 
          -> Either Error (Lets () Name)
 
-curryLts callables lts
+curryLts envt callables lts
  = case lts of
         LLet b x
-         -> LLet b <$> curryX callables x
+         -> LLet b <$> curryX envt callables x
 
         LRec bxs          
          -> do  let (bs, xs) =  unzip bxs
-                xs'          <- mapM (curryX callables) xs
+                xs'          <- mapM (curryX envt callables) xs
                 return  $ LRec  $ zip bs xs'
 
         LPrivate bs mt ws 
@@ -200,14 +215,16 @@
 
 
 -- | Manage function application in a case alternative.
-curryAlt :: Map Name Callable 
+curryAlt :: Show a
+         => EnvT Name
+         -> Map Name Callable 
          -> Alt (AnTEC a Name) Name 
          -> Either Error (Alt () Name)
 
-curryAlt callables alt
+curryAlt envt callables alt
  = case alt of
         AAlt w xBody
          -> let bs         = bindsOfPat w
                 callables' = shadowCallables bs callables
-            in  AAlt w  <$> curryX callables' xBody
+            in  AAlt w  <$> curryX envt callables' xBody
 
diff --git a/DDC/Core/Tetra/Transform/Curry/Call.hs b/DDC/Core/Tetra/Transform/Curry/Call.hs
--- a/DDC/Core/Tetra/Transform/Curry/Call.hs
+++ b/DDC/Core/Tetra/Transform/Curry/Call.hs
@@ -8,9 +8,10 @@
 import DDC.Core.Tetra.Transform.Curry.Error
 import DDC.Core.Tetra.Prim
 import DDC.Core.Exp
-import DDC.Type.Equiv
+import DDC.Type.Exp.Simple.Equiv
 import Control.Monad
 import Data.Map                                 (Map)
+import DDC.Core.Env.EnvT                        (EnvT)
 import qualified DDC.Core.Call                  as Call
 import qualified Data.Map                       as Map
 
@@ -18,14 +19,14 @@
 -- | Call a thing, depending on what it is.
 --   Decide how to call the functional thing, depending on 
 --   whether its a super, foreign imports, or thunk.
-makeCall 
-        :: Map Name Callable    -- ^ Types and arities of functions in the environment.
-        -> Name                 -- ^ Name of function to call. 
-        -> Type Name            -- ^ Type of function to call.
-        -> [Call.Elim () Name]  -- ^ Eliminators for function call.
-        -> Either Error (Maybe (Exp () Name))
+makeCall :: EnvT Name
+         -> Map  Name Callable   -- ^ Types and arities of functions in the environment.
+         -> Name                 -- ^ Name of function to call. 
+         -> Type Name            -- ^ Type of function to call.
+         -> [Call.Elim () Name]  -- ^ Eliminators for function call.
+         -> Either Error (Maybe (Exp () Name))
 
-makeCall callables nFun tFun esArgs
+makeCall envt callables nFun tFun esArgs
 
  -- Call of a local or imported super.
  | Just (tFunTable, csF)
@@ -36,7 +37,7 @@
         -- Internal sanity check: the type annotation on the function
         -- to call should match the type we have for it in the callables
         -- table. If not then we're bugged.
-        when (not $ equivT tFun tFunTable)
+        when (not $ equivT envt tFun tFunTable)
          $ Left $ ErrorSuperTypeMismatch nFun tFun tFunTable
 
         case Call.dischargeConsWithElims csF esArgs of
diff --git a/DDC/Core/Tetra/Transform/Curry/CallSuper.hs b/DDC/Core/Tetra/Transform/Curry/CallSuper.hs
--- a/DDC/Core/Tetra/Transform/Curry/CallSuper.hs
+++ b/DDC/Core/Tetra/Transform/Curry/CallSuper.hs
@@ -60,14 +60,9 @@
         -> [Call.Elim () Name]  -- ^ Eliminators at call site.
         -> Either Error (Maybe (Exp () Name))
 
-makeCallSuperUnder nF tF cs es
- -- We have no eliminators at all, 
- -- so this is just a reference to a top-level super that is not 
- -- being applied.
- --  | []   <- es
- -- = return $ Just $ XVar () (UName nF)
 
-
+-- Under application where we have a type argument for each of the type parameters.
+makeCallSuperUnder nF tF cs es
  -- We have more constructors than eliminators.
  | length es <  length cs
 
@@ -115,17 +110,66 @@
          -- We should have at least one argument to apply. 
          -- If not then the arity information is wrong or the super we were
          -- told to call doesn't have any parameters. Either case is a bug.
-         [] -> error $ "ddc-core-tetra.makeCallSuperUnder: no arguments to apply."
+         [] -> error $ "ddc-core-tetra.makeCallSuperUnder: no parameters for super."
 
          tParamFirst : tsParamRest
           -> let tSuperResult    = C.tFunOfParamResult tsParamRest tResult'
              in return
                  $ Just
                  $ makeRuns () (length esRuns)
-                 $ C.xApps  () (C.xFunCurry () tsParamSat tResultClo 
+                 $ C.xApps  () (C.xFunCurry  () tsParamSat  tResultClo 
                                (C.xFunCReify () tParamFirst tSuperResult xFunAPP))
                                xsArgValue
 
- | otherwise
- = return $ Nothing
 
+-- Under application where we don't have any type arguments.
+-- This happens when we have a reference to a polymorphic function:
+-- 
+-- > let f = /\a. \x. x  
+-- > in  g f
+--
+-- We handle the call to f by eta-expanding it,
+-- so that we can apply the reify function.
+--
+-- > let f = /\a. \x. x
+-- > in  g (/\a. curry0# (creify# [a] [a] (f [a])))
+--
+makeCallSuperUnder nF tF cs es
+ -- We don't have any eliminators.
+ | null es
+
+ -- The super must be in standard form.
+ , Just (csType, _csValue, _cBox) <- Call.splitStdCallCons cs
+ 
+ -- There is at least one type parameter.
+ , not $ null csType
+
+ -- All the type parameters must be named.
+ , bsParam      <- [b | Call.ConsType b <- csType]
+ , Just nsParam <- sequence
+                $  map (\b -> case b of
+                                BName n _ -> Just n
+                                _         -> Nothing) bsParam
+
+ , tsArgs        <- [TVar (UName n) | n <- nsParam]
+ , Just tF_inst  <- T.instantiateTs tF tsArgs
+
+ = let  (tsParamLam, tResult) 
+         = C.takeTFunArgResult tF_inst
+
+   in   case tsParamLam of
+         [] -> error $ "ddc-core-tetra.makeCallSuperUnder: no parameters for super"
+
+         tParamFirst : tsParamRest
+          -> let tSuperResult = C.tFunOfParamResult tsParamRest tResult
+             in  return
+                   $ Just
+                   $ C.xLAMs () bsParam 
+                   $ C.xFunCurry () [] tF_inst
+                   $ C.xFunCReify () tParamFirst tSuperResult 
+                        ( xApps () (XVar () (UName nF)) 
+                                $ map (XType ()) tsArgs)
+
+
+makeCallSuperUnder _nF _tF _cs _es
+ = return $ Nothing
diff --git a/DDC/Core/Tetra/Transform/Curry/CallThunk.hs b/DDC/Core/Tetra/Transform/Curry/CallThunk.hs
--- a/DDC/Core/Tetra/Transform/Curry/CallThunk.hs
+++ b/DDC/Core/Tetra/Transform/Curry/CallThunk.hs
@@ -7,7 +7,7 @@
 import DDC.Core.Exp.Annot
 import qualified DDC.Core.Call                          as Call
 import qualified DDC.Core.Tetra.Compounds               as C
-
+import qualified DDC.Type.Transform.Instantiate         as T
 
 -- | Apply a thunk to some more arguments.
 --
@@ -23,27 +23,31 @@
 makeCallThunk xF tF esArgs
 
  -- Split the eliminators according to the standard call pattern.
- | Just ([], esValues, esRuns)  <- Call.splitStdCallElims esArgs
+ | Just (esType, esValue, esRun)  
+                <- Call.splitStdCallElims esArgs
+ , Just tF_inst <- T.instantiateTs tF [t | Call.ElimType _ _ t <- esType]
  = let  
-        (tsParam, tResult)       = C.takeTFunArgResult tF
+        (tsParam, tResult)       = C.takeTFunArgResult tF_inst
 
         -- Split the value parameters into ones applied to the thunk,
         -- and the ones that form part of its resulting type. 
-        (tsParamArg, tsParamClo) = splitAt (length esValues) tsParam
+        (tsParamArg, tsParamClo) = splitAt (length esValue) tsParam
 
         -- Build the type of the returned closure.
         --   Splitting the type like this assumes that the thunk 
         --   we're applying has a monomorphic type, which is true
         --   for thunked supers with standard calling convention as
-        -- t  he types of these are all prenex.
+        --   the types of these are all prenex.
         tResultClo      = C.tFunOfParamResult tsParamClo tResult
 
-        xsArgs  = [ x | Call.ElimValue _ x <- esValues] 
+        xsArgs          = [ x | Call.ElimValue _ x <- esValue] 
 
    in  return 
          $ Just 
-         $ makeRuns    () (length esRuns)
-         $ C.xFunApply () tsParamArg tResultClo xF xsArgs
+         $ makeRuns    () (length esRun)
+         $ C.xFunApply () tsParamArg tResultClo 
+                (xApps () xF [XType () t | Call.ElimType _ _ t <- esType])
+                xsArgs
 
  | otherwise
  = return $ Nothing
diff --git a/DDC/Core/Tetra/Transform/Curry/Callable.hs b/DDC/Core/Tetra/Transform/Curry/Callable.hs
--- a/DDC/Core/Tetra/Transform/Curry/Callable.hs
+++ b/DDC/Core/Tetra/Transform/Curry/Callable.hs
@@ -80,8 +80,8 @@
 
 -- | Take a `Callable` from an `ImportValue`, or Nothing if there isn't one.
 takeCallableFromImport
-        :: E.Name               -- ^ Name of the imported thing.
-        -> ImportValue E.Name   -- ^ Import definition.
+        :: E.Name                               -- ^ Name of the imported thing.
+        -> ImportValue E.Name (Type E.Name)     -- ^ Import definition.
         -> Either Error (Maybe (E.Name, Callable))
 
 takeCallableFromImport n im
diff --git a/DDC/Core/Tetra/Transform/Curry/Error.hs b/DDC/Core/Tetra/Transform/Curry/Error.hs
--- a/DDC/Core/Tetra/Transform/Curry/Error.hs
+++ b/DDC/Core/Tetra/Transform/Curry/Error.hs
@@ -4,7 +4,7 @@
 where
 import DDC.Core.Tetra.Prim
 import DDC.Type.Exp
-import DDC.Base.Pretty
+import DDC.Data.Pretty
 import qualified DDC.Core.Call          as Call
 
 
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,7 +1,7 @@
 --------------------------------------------------------------------------------
 The Disciplined Disciple Compiler License (MIT style)
 
-Copyrite (K) 2007-2014 The Disciplined Disciple Compiler Strike Force
+Copyrite (K) 2007-2016 The Disciplined Disciple Compiler Strike Force
 All rights reversed.
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
diff --git a/ddc-core-tetra.cabal b/ddc-core-tetra.cabal
--- a/ddc-core-tetra.cabal
+++ b/ddc-core-tetra.cabal
@@ -1,5 +1,5 @@
 Name:           ddc-core-tetra
-Version:        0.4.2.1
+Version:        0.4.3.1
 License:        MIT
 License-file:   LICENSE
 Author:         The Disciplined Disciple Compiler Strike Force
@@ -15,18 +15,17 @@
 
 Library
   Build-Depends: 
-        base            >= 4.6    && < 4.9,
+        base            >= 4.6    && < 4.10,
         array           >= 0.4    && < 0.6,
         deepseq         >= 1.3    && < 1.5,
-        containers      == 0.5.*,
         text            >= 1.0    && < 1.3,
         pretty-show     >= 1.6.8  && < 1.7,
-        transformers    == 0.4.*,
+        containers      == 0.5.*,
+        transformers    == 0.5.*,
         mtl             == 2.2.1.*,
-        ddc-base        == 0.4.2.*,
-        ddc-core        == 0.4.2.*,
-        ddc-core-salt   == 0.4.2.*,
-        ddc-core-simpl  == 0.4.2.*
+        ddc-core        == 0.4.3.*,
+        ddc-core-salt   == 0.4.3.*,
+        ddc-core-simpl  == 0.4.3.*
 
   Exposed-modules:
         DDC.Core.Tetra.Transform.Boxing