diff --git a/Makefile b/Makefile
--- a/Makefile
+++ b/Makefile
@@ -50,7 +50,7 @@
 	$(RM) html
 
 
-VERSION = 0.4.11
+VERSION = 0.4.12
 DISTDIR = alms-$(VERSION)
 TARBALL = $(DISTDIR).tar.gz
 
diff --git a/alms.cabal b/alms.cabal
--- a/alms.cabal
+++ b/alms.cabal
@@ -1,5 +1,5 @@
 Name:           alms
-Version:        0.4.11
+Version:        0.4.12
 Copyright:      2010, Jesse A. Tov
 Cabal-Version:  >= 1.8
 License:        BSD3
@@ -91,6 +91,7 @@
                         PprClass,
                         Prec,
                         PrettyPrint,
+                        Printing,
                         Rename,
                         Sigma,
                         Statics,
diff --git a/src/Coercion.hs b/src/Coercion.hs
--- a/src/Coercion.hs
+++ b/src/Coercion.hs
@@ -78,9 +78,9 @@
         return $ if null tvs
           then body
           else absContract $
-               exAbsVar' (lid "f") (typeToStx tfrom) $
+               exAbsVar' (lid "f") (typeToStx' tfrom) $
                foldr (\tv0 acc -> exTAbs tv0 . acc) id tvs $
-               exAbsVar' (lid "x") (typeToStx t1') $
+               exAbsVar' (lid "x") (typeToStx' t1') $
                instContract body `exApp`
                foldl (\acc tv0 -> exTApp acc (Syntax.tyVar tv0))
                      (exBVar (lid "f")) tvs `exApp`
@@ -89,19 +89,23 @@
   let recs' = M.insert (tv, tv') Nothing (shadow [tv] [tv'] recs)
   body <- build b recs' t t' >>! instContract
   let tv''  = freshTyVar tv (ftv (tv, tv'))
+      tstx  = typeToStx' t
+      tstx' = typeToStx' t'
   return $
     absContract $
-      [$ex|+ fun (Pack('$tv'', e) : ex '$tv. $stx:t) ->
-               Pack[ex '$tv'. $stx:t']('$tv'', $body e) |]
+      [$ex|+ fun (Pack('$tv'', e) : ex '$tv. $tstx) ->
+               Pack[ex '$tv'. $tstx']('$tv'', $body e) |]
 build b recs (view -> TyMu tv t) (view -> TyMu tv' t') = do
   l    <- freshLid
   let recs' = M.insert (tv, tv') (Just l) (shadow [tv] [tv'] recs)
   body <- build b recs' t t'
+  let tstx  = typeToStx' t
+      tstx' = typeToStx' t'
   return $
     [$ex|+
       let rec $lid:l
               (parties : string * string)
-                       : (mu '$tv. $stx:t) -> mu '$tv'. $stx:t'
+                       : (mu '$tv. $tstx) -> mu '$tv'. $tstx'
           = $body parties
        in $lid:l
     |]
@@ -112,7 +116,8 @@
     = return [$ex|+ INTERNALS.Contract.any ['$tv'] |]
 build _ _    t t' =
   if t <: t'
-    then return [$ex|+ INTERNALS.Contract.any [$stx:t'] |]
+    then let tstx' = typeToStx' t' in
+         return [$ex|+ INTERNALS.Contract.any [$tstx'] |]
     else CMS.lift . throwAlms $ AlmsException StaticsPhase bogus [$msg|
         <dl>
           <dt>from type: <dd>$t
diff --git a/src/Main.hs b/src/Main.hs
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -6,11 +6,13 @@
 ) where
 
 import Util
-import Ppr (Ppr(..), (<+>), (<>), text, char, hang, ($$), nest, printDoc)
+import Ppr (Doc, Ppr(..), (<+>), (<>), text, char, hang,
+            ($$), nest, printDoc, hPrintDoc)
 import qualified Ppr
 import Parser (parseFile, REPLCommand(..), parseCommand)
 import Prec (precOp)
 import Paths (findAlmsLib, findAlmsLibRel, versionString, shortenPath)
+import Printing (addTyNameContext)
 import Rename (RenameState, runRenamingM, renameDecls, renameProg,
                getRenamingInfo, RenamingInfo(..))
 import Statics (tcProg, tcDecls, S, runTC, runTCNew, Module(..),
@@ -66,7 +68,7 @@
   st2 <- foldM (\st n -> findAlmsLibRel n "." >>= tryLoadFile st n)
                st1 (reverse [ name | LoadFile name <- opts ])
   maybe interactive (batch filename) mmsrc (`elem` opts) st2
-    `handleExns` exitFailure
+    `handleExns` (st2, exitFailure)
 
 tryLoadFile :: ReplState -> String -> Maybe String -> IO ReplState
 tryLoadFile st name mfile = case mfile of
@@ -164,8 +166,8 @@
   prog <- getProgName
   hPutStrLn stderr (prog ++ ": " ++ msg)
 
-handleExns :: IO a -> IO a -> IO a
-handleExns body handler =
+handleExns :: IO a -> (ReplState, IO a) -> IO a
+handleExns body (st, handler) =
   body
     `Exn.catches`
     [ Exn.Handler $ \e@(VExn { }) -> do
@@ -186,7 +188,7 @@
           Msg.Flow [Msg.Words (show err)] ]
   where
     continue err = do
-      hPutStrLn stderr (show (err :: EM.AlmsException))
+      hPrintDoc stderr (withRS st (ppr (err :: EM.AlmsException)))
       handler
 
 interactive :: (Option -> Bool) -> ReplState -> IO ()
@@ -200,7 +202,7 @@
         Nothing  -> return ()
         Just (row', ast) -> do
           st' <- doLine st ast
-                   `handleExns` return st
+                   `handleExns` (st, return st)
           repl row' st'
     doLine st ast = let
       rename  :: (ReplState, [Decl Raw]) -> IO ReplState
@@ -233,7 +235,7 @@
                                 display newDefs newVals st3
 
       display newDefs newVals st3
-                          = do printResult newDefs newVals
+                          = do printResult st3 newDefs newVals
                                return st3
 
       in rename (st, ast)
@@ -271,8 +273,8 @@
                   return (Just (row + count, ast))
                 ParseError derr -> 
                   loop (count + 1) ((line, derr) : acc)
-    printResult :: Module -> NewValues -> IO ()
-    printResult md00 values = say (loop True md00) where
+    printResult :: ReplState -> Module -> NewValues -> IO ()
+    printResult st md00 values = say (withRS st (loop True md00)) where
       loop tl md0 = case md0 of
         MdNil               -> Ppr.empty
         MdApp md1 md2       -> loop tl md1 $$ loop tl md2
@@ -282,8 +284,9 @@
           Just Nothing   -> text "exception"<+>ppr u
           Just (Just t') -> text "exception"<+>ppr u<+>text "of"<+>ppr t'
         MdTycon _ tc        ->
-          text "type" <+> ppr (tyConToDec tc :: TyDec Renamed)
-        MdModule u md1      ->
+          text "type" <+>
+          Ppr.askTyNames (\tn -> ppr (tyConToDec tn tc :: TyDec Renamed))
+        MdModule u md1      -> Ppr.enterTyNames u $
           text "module" <+> ppr u <+> char ':' <+> text "sig"
           $$ nest 2 (loop False md1)
           $$ text "end"
@@ -333,12 +336,18 @@
     s = rsStatics st
     --
     mention what who rhs loc = do
-      printDoc $ text what <+> ppr who
-                   >?> rhs Ppr.>?>
-                     if isBogus loc
-                       then text "  -- built-in"
-                       else text "  -- defined at" <+> text (show loc)
+      printDoc $
+        withRS st $
+          text what <+> ppr who
+            >?> rhs Ppr.>?>
+              if isBogus loc
+                then text "  -- built-in"
+                else text "  -- defined at" <+> text (show loc)
       where a >?> b = Ppr.ifEmpty who (a <+> b) (a Ppr.>?> b)
+
+-- Add the ReplState to the pretty-printing context.
+withRS :: ReplState -> Doc -> Doc
+withRS rs = addTyNameContext (rsRenaming rs) (rsStatics rs)
 
 printPrec :: String -> IO ()
 printPrec oper = printDoc $
diff --git a/src/Ppr.hs b/src/Ppr.hs
--- a/src/Ppr.hs
+++ b/src/Ppr.hs
@@ -41,7 +41,16 @@
 pprInfix inspect x0
   | Just (x1, op, Nothing) <- inspect x0
   , precOp op == Right precBang
-    = Just (prec precBang (text op <+> ppr x1))
+    = let rloop x'
+            | Just (x1', op', Nothing) <- inspect x'
+            , precOp op == Right precBang
+            = first (op':) (rloop x1')
+            | otherwise
+            = ([], x')
+          (ops, x) = first (op:) (rloop x1)
+       in Just $
+            fsep (mapTail (nest 2) $ map text ops)
+            <> pprPrec precBang x
   | Just (_, op, Just _) <- inspect x0
   , isOperator (lid op :: Lid Raw)
   , p <- precOp op
@@ -105,8 +114,9 @@
     _ | Just doc <- pprInfix unfoldTyPat tp0
                        -> doc
     N _ (TpVar tv var) -> pprParamV var tv
+    [$tpQ| $qlid:ql |] -> ppr ql
     [$tpQ| ($list:tps) $qlid:ql |]
-                       -> ppr tps <+> ppr ql
+                       -> prec precApp $ sep [ppr tps, ppr ql]
     [$tpQ| $antiP:a |] -> ppr a
 
 unfoldTyPat :: TyPat i -> Maybe (TyPat i, String, Maybe (TyPat i))
diff --git a/src/PprClass.hs b/src/PprClass.hs
--- a/src/PprClass.hs
+++ b/src/PprClass.hs
@@ -9,14 +9,17 @@
   -- ** Helpers
   ppr0, ppr1, pprDepth,
   -- ** Context operations
-  prec, prec1, descend, atPrec, atDepth,
+  prec, mapPrec, prec1, descend, atPrec, atDepth,
   askPrec, askDepth,
   trimList, trimCat,
+  -- *** For type name shortening
+  TyNames(..), tyNames0,
+  setTyNames, askTyNames, enterTyNames, lookupTyNames,
   -- * Pretty-printing combinators
   (>+>), (>?>), ifEmpty,
   vcat, sep, cat, fsep, fcat,
   -- * Renderers
-  render, renderS, printDoc, printPpr,
+  render, renderS, printDoc, printPpr, hPrintDoc, hPrintPpr,
   -- ** Instance helpers
   showFromPpr, pprFromShow,
   -- * Re-exports
@@ -26,20 +29,38 @@
 import PrettyPrint hiding (Doc(..), render, vcat, sep, cat, fsep, fcat)
 import qualified PrettyPrint as P
 
+import Syntax.Ident (QLid, Uid, Renamed)
+
+import System.IO (Handle, stdout, hPutChar, hPutStr)
+
 -- | Context for pretty-printing.
 data PprContext
   = PprContext {
-      pcPrec  :: !Int,
-      pcDepth :: !Int
+      pcPrec   :: !Int,
+      pcDepth  :: !Int,
+      pcTyName :: !TyNames
   }
 
+data TyNames =
+  TyNames {
+    tnLookup   :: Int -> QLid Renamed -> QLid Renamed,
+    tnEnter    :: Uid Renamed -> TyNames
+  }
+
 -- | Default context
 pprContext0 :: PprContext
 pprContext0  = PprContext {
-  pcPrec  = 0,
-  pcDepth = -1
+  pcPrec   = 0,
+  pcDepth  = -1,
+  pcTyName = tyNames0
 }
 
+tyNames0 :: TyNames
+tyNames0  = TyNames {
+  tnLookup = const id,
+  tnEnter  = const tyNames0
+}
+
 type Doc = P.Doc PprContext
 
 data ListStyle 
@@ -115,6 +136,10 @@
     then descend $ parens (atPrec (min p 0) doc)
     else atPrec p doc
 
+-- | Adjust the precedence with the given function.
+mapPrec :: (Int -> Int) -> Doc -> Doc
+mapPrec f doc = askPrec (\p -> prec (f p) doc)
+
 -- | Go to the next (tigher) precedence level.
 prec1 :: Doc -> Doc
 prec1  = mapD (\e -> e { pcPrec = pcPrec e + 1 })
@@ -143,6 +168,24 @@
 askDepth :: (Int -> Doc) -> Doc
 askDepth  = asksD pcDepth
 
+-- | Change the type name lookup function
+setTyNames   :: TyNames -> Doc -> Doc
+setTyNames f  = mapD (\e -> e { pcTyName = f })
+
+-- | Retrieve the type name lookup function
+askTyNames   :: (TyNames -> Doc) -> Doc
+askTyNames    = asksD pcTyName
+
+-- | Render a document with a module opened
+enterTyNames :: Uid Renamed -> Doc -> Doc
+enterTyNames u doc = askTyNames $ \tn ->
+  setTyNames (tnEnter tn u) doc
+
+-- | Look up a type name in the rendering context
+lookupTyNames :: Int -> QLid Renamed -> (QLid Renamed -> Doc) -> Doc
+lookupTyNames tag ql kont = askTyNames $ \tn ->
+  kont (tnLookup tn tag ql)
+
 -- | Trim a list to (about) the given number of elements, with
 --   "..." in the middle.
 trimList :: Int -> [Doc] -> [Doc]
@@ -210,14 +253,21 @@
 
 -- Render and display a document in the preferred style
 printDoc :: Doc -> IO ()
-printDoc = fullRenderIn pprContext0 PageMode 80 1.1 each (putChar '\n')
-  where each (Chr c) io  = putChar c >> io
-        each (Str s) io  = putStr s >> io
-        each (PStr s) io = putStr s >> io
+printDoc  = hPrintDoc stdout
 
 -- Pretty-print, render and display in the preferred style
 printPpr :: Ppr a => a -> IO ()
-printPpr = printDoc . ppr
+printPpr  = hPrintPpr stdout
+
+-- Render and display a document in the preferred style
+hPrintDoc :: Handle -> Doc -> IO ()
+hPrintDoc h = fullRenderIn pprContext0 PageMode 80 1.1 each (putChar '\n')
+  where each (Chr c) io  = hPutChar h c >> io
+        each (Str s) io  = hPutStr h s >> io
+        each (PStr s) io = hPutStr h s >> io
+
+hPrintPpr :: Ppr a => Handle -> a -> IO ()
+hPrintPpr h = hPrintDoc h . ppr
 
 showFromPpr :: Ppr a => Int -> a -> ShowS
 showFromPpr p t = renderS (pprPrec p t)
diff --git a/src/Printing.hs b/src/Printing.hs
new file mode 100644
--- /dev/null
+++ b/src/Printing.hs
@@ -0,0 +1,78 @@
+{-# LANGUAGE
+      PatternGuards #-}
+-- Miscellaneous high-level printing routines.  These can't go in, say,
+-- Ppr, because they depend on Rename and Statics.
+module Printing (
+  addTyNameContext
+) where
+
+import Data.List (tails)
+import PprClass
+import Rename (RenameState, RenamingInfo(..),
+               getRenamingInfo, renamingEnterScope)
+import Statics (S, getTypeInfo, staticsEnterScope)
+import Syntax.Ident
+import Type
+import Util
+
+-- | The status of a type name in an environment
+data NameStatus
+ -- | Bound to the expected type
+ = Match
+ -- | Not bound
+ | NoMatch
+ -- | Shadowed
+ | Interfere
+ deriving Eq
+
+-- | In the given environment, what is the status of the given
+--   type name?
+getNameStatus :: RenameState -> S -> Int -> QLid i -> NameStatus
+getNameStatus r s tag ql =
+  case [ ql' | TyconAt _ ql' <- getRenamingInfo ident r ] of
+    ql':_ ->
+      case getTypeInfo ql' s of
+        Just tc | tcId tc == tag  -> Match
+                | otherwise       -> Interfere
+        _                         -> NoMatch
+    _     -> NoMatch
+  where ident = J (map (uid . unUid) (jpath ql))
+                  (Var (lid (unLid (jname ql))))
+
+-- | Find the best name to refer to a type constructor.
+--   The goal here is to get the shortest unambiguous name.
+--    1. If the first parameter is True, we want an accurate name, so
+--       skip to step 3.
+--    2. If the unqualified name is bound to either the same type
+--       or to nothing, then use the unqualified name.
+--    3. Try qualifiying the name, starting with the last segment
+--       and adding one at a time, and if any of these match, then
+--       use that.
+--    4. Otherwise, uglify the name, because it's probably gone
+--       out of scope.
+getBestName :: RenameState -> S ->
+               Int -> QLid Renamed -> QLid Renamed
+getBestName r s tag ql =
+  case tryQuals (jpath ql) (jname ql) of
+    Just ql' -> ql'
+    _ | isTrivial (lidUnique (jname ql)),
+        NoMatch <- getNameStatus r s tag ql
+             -> ql
+    _        -> uglify
+  where
+    tryQuals us l = msum
+      [ case getNameStatus r s tag (J us' l) of
+          Match     -> Just (J us' l)
+          _         -> Nothing
+      | us' <- reverse (tails us) ]
+    uglify = ql { jpath = uid ('?':show tag) : jpath ql }
+
+makeTyNames :: RenameState -> S -> TyNames
+makeTyNames r s = TyNames {
+  tnLookup = getBestName r s,
+  tnEnter  = \u -> makeTyNames (renamingEnterScope u r)
+                               (staticsEnterScope u s)
+}
+
+addTyNameContext :: RenameState -> S -> Doc -> Doc
+addTyNameContext  = setTyNames <$$> makeTyNames
diff --git a/src/Rename.hs b/src/Rename.hs
--- a/src/Rename.hs
+++ b/src/Rename.hs
@@ -20,6 +20,7 @@
   renameProg, renameDecls, renameDecl, renameType,
   -- * REPL query
   getRenamingInfo, RenamingInfo(..),
+  renamingEnterScope,
 ) where
 
 import ErrorMessage
@@ -957,4 +958,13 @@
     look prj qx build = case envLookup prj qx e of
       Left _                    -> Nothing
       Right (J ps (x', loc, _)) -> Just (build loc (J ps x'))
+
+-- Open the given module, if it exists.
+renamingEnterScope    :: Uid i -> RenameState -> RenameState
+renamingEnterScope u r =
+  let e  = savedEnv r in
+  case M.lookup (uid (unUid u)) (modules e) of
+    Nothing -> r
+    Just (_, _, (_, e'))
+            -> r { savedEnv = e `mappend` e' }
 
diff --git a/src/Statics.hs b/src/Statics.hs
--- a/src/Statics.hs
+++ b/src/Statics.hs
@@ -27,6 +27,7 @@
   -- * Type checking results for the REPL
   runTCNew, Module(..), getExnParam, tyConToDec,
   getVarInfo, getTypeInfo, getConInfo,
+  staticsEnterScope,
 ) where
 
 import Meta.Quasi
@@ -41,7 +42,7 @@
                       TyPat, TyPat'(..))
 import Loc
 import Env as Env
-import Ppr (Ppr)
+import Ppr (Ppr, TyNames)
 import Type
 import TypeRel
 import Coercion (coerceExpression)
@@ -52,18 +53,16 @@
 import Control.Monad.Error  as Error
 import Data.Data (Typeable, Data)
 import Data.Generics (everywhere, mkT)
-import Data.List (transpose)
+import Data.List (transpose, tails)
 import Data.Monoid
 import qualified Data.Map as M
 import qualified Data.Set as S
 
-{-
 import System.IO.Unsafe (unsafePerformIO)
 pP :: Show a => a -> b -> b
 pP a b = unsafePerformIO (print a) `seq` b
 pM :: (Show a, Monad m) => a -> m ()
 pM a = if pP a True then return () else fail "wibble"
--}
 
 -- The kind of names we're using.
 type R = Renamed
@@ -234,7 +233,7 @@
 
 -- | Indicate a type checker bug.
 typeBug :: AlmsMonad m => String -> String -> m a
-typeBug culprit msg0 = throwAlms (almsBug RenamerPhase bogus culprit msg0)
+typeBug culprit msg0 = throwAlms (almsBug StaticsPhase bogus culprit msg0)
 
 -- | Like 'ask', but monadic
 asksM :: MonadReader r m => (r -> m a) -> m a
@@ -268,6 +267,11 @@
 enterModule u = local $ \cxt ->
   cxt { modulePath = u : modulePath cxt }
 
+-- | Forget the module path (for type checking signatures)
+forgetModulePath :: Monad m => TC m a -> TC m a
+forgetModulePath  = local $ \cxt -> cxt { modulePath = [] }
+
+-- | Find out the current module path
 currentModulePath :: Monad m => TC m [Uid R]
 currentModulePath  = asks (reverse . modulePath)
 
@@ -491,7 +495,8 @@
       (t2, e2') <- inModule md $ tc e2
       let b's =
             zipWith3
-              (\b tf e' -> newBinding b { bntype = typeToStx tf, bnexpr = e' })
+              (\b tf e' -> newBinding b { bntype = typeToStx' tf,
+                                          bnexpr = e' })
               bs tfs e's
       return (t2, [$ex|+ let rec $list:b's in $e2' |])
     [$ex| let $decl:d in $e2 |] -> do
@@ -508,7 +513,8 @@
       checkSharing "function body" e md
       (te, e') <- inModule md $ tc e
       q <- getWorthiness e0
-      return (TyFun q t' te, [$ex|+ fun ($x' : $stx:t') -> $e' |])
+      let stxt' = typeToStx' t'
+      return (TyFun q t' te, [$ex|+ fun ($x' : $stxt') -> $e' |])
     [$ex| $_ $_ |] -> do
       tcExApp tc e0
     [$ex| fun '$tv -> $e |] -> do
@@ -520,7 +526,8 @@
       (t1, e1') <- tc e1
       t2'       <- tcType t2
       t1'       <- tapply t1 t2'
-      return (t1', [$ex|+ $e1' [$stx:t2'] |])
+      let stxt2' = typeToStx' t2'
+      return (t1', [$ex|+ $e1' [$stxt2'] |])
     [$ex| Pack[$opt:mt1]($t2, $e) |] -> do
       t2'      <- tcType t2
       (te, e') <- tc e
@@ -537,7 +544,9 @@
                      <dt>hiding:        <dd>$t2
                      <dt>to get:        <dd>$t1'
                    </dl> |]
-          return (t1', [$ex| Pack[$stx:t1']($stx:t2', $e') |])
+          let stxt1' = typeToStx' t1'
+              stxt2' = typeToStx' t2'
+          return (t1', [$ex| Pack[$stxt1']($stxt2', $e') |])
         _ -> terrgot "Pack[-]" t1' "existential type"
     [$ex| ( $e1 : $t2 ) |] -> do
       (t1, e1') <- tc e1
@@ -1016,11 +1025,11 @@
 
 -- END type decl checking
 
--- | Type check a module body
+-- | Type check a signature
 tcSigExp :: (?loc :: Loc, Monad m) =>
             SigExp R -> TC m (SigExp R)
 tcSigExp [$seQ| sig $list:ds end |] = do
-  ds' <- tcMapM tcSigItem ds
+  ds' <- forgetModulePath $ tcMapM tcSigItem ds
   return [$seQ| sig $list:ds' end |]
 tcSigExp [$seQ| $quid:n $list:qls |] = do
   (md, _) <- find (fmap SIGVAR n)
@@ -1129,7 +1138,7 @@
                </dl> |] (qRepresent (qualifier te))
       return te
   x' <- tcPatt t' x
-  return (x', Just (typeToStx t'), e')
+  return (x', Just (typeToStx' t'), e')
 
 -- | Run a computation in the context of a module open declaration
 tcOpen :: (?loc :: Loc, Monad m) =>
@@ -1153,7 +1162,7 @@
 tcException n mt = do
   mt' <- gmapM tcType mt
   bindCon n (maybe tyExn (`tyArr` tyExn) mt')
-  return (fmap typeToStx mt')
+  return (fmap typeToStx' mt')
 
 -- | Type check and bind a module
 tcMod :: (?loc :: Loc, Monad m) =>
@@ -1171,79 +1180,6 @@
   bindSig u md
   return se'
 
-{-
--- | Determine types that are no longer reachable by name
---   in a given scope, and give them an ugly printing name
-hideInvisible :: Monad m =>
-                 Scope -> TC m Scope
-hideInvisible (PEnv modenv level) = do
-  level' <- withAny level $ everywhereM (mkM repair) level
-  withAny level' $ do
-    ((), modenv') <- mapAccumM
-                   (\scope acc -> do
-                      scope' <- hideInvisible scope
-                      return (acc, scope'))
-                   () modenv
-    return (PEnv modenv' level')
-  where
-    repair :: Monad m => Type -> TC m Type
-    repair t@(TyApp tc ts cache) = do
-      mtc <- tryGetAny (tcName tc)
-      return $ if mtc == Just tc
-        then t
-        else TyApp (hide tc) ts cache
-    repair t = return t
-    --
-    hide :: TyCon -> TyCon
-    hide tc@TyCon { tcName = J (Uid _ "?" : _) _ } = tc
-    hide tc@TyCon { tcName = J qs (Lid _ k), tcId = i } =
-      tc { tcName = J (Uid "?":qs) (Lid _ (k ++ ':' : show i)) }
-
--- | Replace the printing name of each type with the shortest
---   path to access that type.  (So unnecessary!)
-requalifyTypes :: [Uid R] -> E -> E
-requalifyTypes _uids env = map (fmap repairLevel) env where
-  repairLevel :: Level -> Level
-  repairLevel level = everywhere (mkT repair) level
-  --
-  repair :: TypeT -> TypeT
-  repair t@(TyCon { }) = case tyConsInThisEnv -.- ttId (tyinfo t) of
-    Nothing   -> t
-    Just name -> t `setTycon` name
-  repair t = t
-  --
-  tyConsInThisEnv :: Env Integer (QLid R)
-  tyConsInThisEnv  = uids <...> foldr addToScopeMap empty env
-  --
-  addToScopeMap :: Scope -> Env Integer (QLid R) -> Env Integer (QLid R)
-  addToScopeMap (PEnv ms level) acc = 
-    foldr (Env.unionWith chooseQLid) acc
-      (makeLevelMap level :
-       [ uid <..> addToScopeMap menv empty
-       | (uid, menv) <- toList ms ])
-  --
-  makeLevelMap (Level _ ts) =
-    fromList [ (ttId tag, J [] lid)
-             | (lid, info) <- toList ts,
-               tag <- tagOfTyInfo info ]
-  --
-  tagOfTyInfo (TiAbs tag)     = [tag]
-  tagOfTyInfo (TiSyn _ _)     = []
-  tagOfTyInfo (TiDat tag _ _) = [tag]
-  tagOfTyInfo TiExn           = [tdExn]
-  --
-  chooseQLid :: QLid R -> QLid R -> QLid R
-  chooseQLid q1@(J p1 _) q2@(J p2 _)
-    | length p1 < length p2 = q1
-    | otherwise             = q2
-  --
-  (<..>) :: Functor f => p -> f (Path p k) -> f (Path p k)
-  (<..>)  = fmap . (<.>)
-  --
-  (<...>) :: Functor f => [p] -> f (Path p k) -> f (Path p k)
-  (<...>) = flip $ foldr (<..>)
--}
-
 -- | Type check a module body
 tcModExp :: (?loc :: Loc, Monad m) =>
             ModExp R -> TC m (ModExp R)
@@ -1391,7 +1327,8 @@
 ascribeSignature :: (?loc :: Loc, Monad m) =>
                     Module -> Module -> TC m ()
 ascribeSignature md1 md2 = do
-  let md2'   = renameSig (makeNameMap md1) md2
+  us <- currentModulePath
+  let md2'   = renameSig (makeNameMap md1) us md2
   onlyInModule md1 $ do
     subst <- matchSigTycons md2'
     subsumeSig (applyTyConSubstInSig subst md2')
@@ -1403,16 +1340,17 @@
 
 -- | Make the names in a signature match the names from the module it's
 --   being applied to.
-renameSig :: NameMap -> Module -> Module
-renameSig nm0 = loop where
+renameSig :: NameMap -> [Uid Renamed] -> Module -> Module
+renameSig nm0 us = loop where
   loop md0 = case md0 of
     MdNil          -> MdNil
     MdApp md1 md2  -> MdApp (loop md1) (loop md2)
     MdValue x t    -> MdValue (fromJust (nm0 =..= x)) t
-    MdTycon x tc   -> MdTycon (fromJust (nm0 =..= x)) tc
+    MdTycon x tc   -> MdTycon (fromJust (nm0 =..= x)) tc'
+      where tc' = tc { tcName = J us (jname (tcName tc)) }
     MdModule x md1 ->
       let Just (x', nm1) = nm0 =..= x
-       in MdModule x' (renameSig nm1 md1)
+       in MdModule x' (renameSig nm1 (us++[x']) md1)
     MdSig x md1    -> MdSig (fromJust (nm0 =..= SIGVAR x)) md1
 
 -- | Given a signature, find the tycon substitutions necessary to
@@ -1457,8 +1395,7 @@
   loop (MdSig _ _)      = id
 
 -- | Check whether the given signature subsumes the signature
---   implicit in the environment; takes a 'NameMap' mapping un-renamed
---   signature names to renamed environment names.
+--   implicit in the environment.
 subsumeSig :: (?loc :: Loc, Monad m) =>
               Module -> TC m ()
 subsumeSig = loop where
@@ -1613,7 +1550,7 @@
         </dl>
       |]
 
--- | Check that two type patterns match, and return the pairs of
+-- | To check that two type patterns match, and return the pairs of
 --   type variables that line up and thus need renaming.
 matchTypats :: (?loc :: Loc, Monad m) =>
                TyPat -> TyPat -> TC m ([TyVar R], [TyVar R])
@@ -1683,16 +1620,16 @@
 getExnParam _               = Nothing
 
 -- | Reconstruct the declaration from a tycon binding, for printing
-tyConToDec :: TyCon -> TyDec R
-tyConToDec tc = case tc of
+tyConToDec :: TyNames -> TyCon -> TyDec R
+tyConToDec tn tc = case tc of
   _ | tc == tcExn
     -> tdAbs (lid "exn") [] [] maxBound
   TyCon { tcName = n, tcNext = Just clauses }
-    -> tdSyn (jname n) [ (map tyPatToStx ps, typeToStx rhs)
+    -> tdSyn (jname n) [ (map (tyPatToStx tn) ps, typeToStx tn rhs)
                        | (ps, rhs) <- clauses ]
   TyCon { tcName = n, tcCons = (ps, alts) }
     | not (isEmpty alts)
-    -> tdDat (jname n) ps [ (u, fmap typeToStx mt)
+    -> tdDat (jname n) ps [ (u, fmap (typeToStx tn) mt)
                           | (u, mt) <- toList alts ]
   TyCon { tcName = n }
     ->
@@ -1711,7 +1648,7 @@
 getTypeInfo :: QLid R -> S -> Maybe TyCon
 getTypeInfo ql (S e _) = e =..= ql
 
--- Find out about a type constructor.  If it's an exception constructor,
+-- Find out about a data constructor.  If it's an exception constructor,
 -- return 'Left' with its paramter, otherwise return the type construtor
 -- of the result type
 getConInfo :: QUid R -> S -> Maybe (Either (Maybe Type) TyCon)
@@ -1725,3 +1662,12 @@
           loop (TyApp tc _ _) = Just (Right tc)
           loop _              = Nothing
        in loop t
+
+-- Open the given module, if it exists.
+staticsEnterScope    :: Uid R -> S -> S
+staticsEnterScope u s =
+  let e = sEnv s in
+  case e =..= u of
+    Just (_, e') -> s { sEnv = e =+= e' }
+    Nothing      -> s
+
diff --git a/src/Syntax/SyntaxTable.hs b/src/Syntax/SyntaxTable.hs
--- a/src/Syntax/SyntaxTable.hs
+++ b/src/Syntax/SyntaxTable.hs
@@ -46,7 +46,6 @@
   & "antiC"  =:< 'CaAnti
 typeAntis
   = "type"   =:! Nothing
-  & "stx"    =:  appFun (TH.mkName "typeToStx'")
   & "anti"   =:< 'TyAnti
 tyPatAntis
   = "typat"  =:! Nothing
diff --git a/src/Type.hs b/src/Type.hs
--- a/src/Type.hs
+++ b/src/Type.hs
@@ -129,9 +129,12 @@
 instance Ord TyCon where
   compare tc tc'  = compare (tcName tc) (tcName tc')
 
-instance Ppr Type   where ppr = ppr . typeToStx
+instance Ppr Type   where
+  ppr t = askTyNames (\tn -> ppr (typeToStx tn t))
+instance Ppr TyPat where
+  ppr t = askTyNames (\tn -> ppr (tyPatToStx tn t))
+
 instance Show Type  where showsPrec = showFromPpr
-instance Ppr TyPat  where ppr = ppr . tyPatToStx
 instance Show TyPat where showsPrec = showFromPpr
 
 -- | The different varieties of type definitions
@@ -685,18 +688,18 @@
 ---
 
 -- | Represent a type value as a pre-syntactic type, for printing
-typeToStx' :: Type -> Stx.Type' Renamed
-typeToStx'  = view . typeToStx
+typeToStx' :: Type -> Stx.Type Renamed
+typeToStx'  = typeToStx tyNames0
 
 -- | Represent a type value as a syntactic type, for printing; renames
 --   so that scope is apparent, since internal renaming may result int
 --   different identifiers that print the same
-typeToStx :: Type -> Stx.Type Renamed
-typeToStx = loop (S.empty, M.empty) where
+typeToStx :: TyNames -> Type -> Stx.Type Renamed
+typeToStx f = loop (S.empty, M.empty) where
   loop ren t0 = case t0 of
     TyVar tv      -> Stx.tyVar (maybe tv id (M.lookup tv (snd ren)))
     TyFun q t1 t2 -> Stx.tyFun (qRepresent q) (loop ren t1) (loop ren t2)
-    TyApp tc ts _ -> Stx.tyApp (tcName tc) {jpath = []} (map (loop ren) ts)
+    TyApp tc ts _ -> Stx.tyApp (bestName f tc) (map (loop ren) ts)
     {-
         (fmap (\ql -> lid ("[" ++ show (tcId tc) ++ "]" ++ unLid ql))
               (tcName tc)) 
@@ -715,15 +718,20 @@
      in (tv', (S.insert (unLid (tvname tv')) seen,
                M.insert tv tv' remap))
 
-tyPatToStx' :: TyPat -> Stx.TyPat' Renamed
-tyPatToStx'  = view . tyPatToStx
+tyPatToStx' :: TyPat -> Stx.TyPat Renamed
+tyPatToStx'  = tyPatToStx tyNames0
 
 -- | Represent a type pattern as a syntactic type pattern, for printing
-tyPatToStx :: TyPat -> Stx.TyPat Renamed
-tyPatToStx tp0 = case tp0 of
+tyPatToStx :: TyNames -> TyPat -> Stx.TyPat Renamed
+tyPatToStx f tp0 = case tp0 of
   TpVar tv      -> Stx.tpVar tv Invariant
-  TpApp tc tps  -> Stx.tpApp (tcName tc) (map tyPatToStx tps)
+  TpApp tc tps  -> Stx.tpApp (bestName f tc) (map (tyPatToStx f) tps)
+  where
 
+-- | Look up the best printing name for a type.
+bestName :: TyNames -> TyCon -> QLid Renamed
+bestName tn = tnLookup tn <$> tcId <*> tcName
+
 -- | Convert a type pattern to a type; useful for quqlifier and variance
 --   analysis
 tyPatToType :: TyPat -> Type
@@ -900,7 +908,6 @@
 
 instance Ppr TyCon where
   ppr tc = atPrec 0 $
-    -- brackets (text (show (tcId tc))) <>
     case tcNext tc of
       Just [(tps,t)] -> pprTyApp (tcName tc) (ps (map snd tvs))
                           >?> qe (map fst tvs)
@@ -910,9 +917,10 @@
                      TpVar tv -> (tv, ppr tv)
                      _        -> let tv  = TV (lid (show i)) qlit
                                      tv' = case qlit of
-                                       Qa -> ppr tv <> char '='
-                                       Qu -> empty
-                                  in (tv, tv' <> pprPrec precEq tp)
+                                       Qa -> ppr tv <> char '=' <>
+                                             mapPrec (max precEq) (ppr tp)
+                                       Qu -> ppr tp
+                                  in (tv, tv')
                  | tp   <- tps
                  | qlit <- tcBounds tc
                  | i <- [ 1 :: Integer .. ] ]
@@ -924,7 +932,8 @@
           tvs  = [ TV (lid (show i)) qlit
                  | qlit <- tcBounds tc
                  | i <- [ 1 .. ] :: [Int] ]
-          alt (tps,t) = char '|' <+> pprPrec precApp tps <+> ppr (tcName tc)
+          alt (tps,t) = char '|' <+> pprPrec precApp tps
+                          <+> ppr (jname (tcName tc))
                           >?> char '=' <+> ppr t
       --
       Nothing -> pprTyApp (tcName tc) (ps tvs)
@@ -948,7 +957,7 @@
                             ppr (qRepresent
                                  (denumberQDen
                                   (map qDenOfTyVar tvs) (tcQual tc)))
-      ps tvs = [ ppr var <> pprPrec precApp tv
+      ps tvs = [ ppr var <> pprPrec (precApp + 1) tv
                | tv <- tvs
                | var <- tcArity tc ]
 
diff --git a/src/TypeRel.hs b/src/TypeRel.hs
--- a/src/TypeRel.hs
+++ b/src/TypeRel.hs
@@ -21,6 +21,7 @@
 
 import Env
 import ErrorST
+import Ppr ()
 import Type
 import Util
 import Viewable