diff --git a/src/Cryptol/ModuleSystem.hs b/src/Cryptol/ModuleSystem.hs
index 7a39c2a8..0962245a 100644
--- a/src/Cryptol/ModuleSystem.hs
+++ b/src/Cryptol/ModuleSystem.hs
@@ -6,6 +6,8 @@
 -- Stability   :  provisional
 -- Portability :  portable
 
+{-# LANGUAGE FlexibleContexts #-}
+
 module Cryptol.ModuleSystem (
     -- * Module System
     ModuleEnv(..), initialModuleEnv
@@ -21,6 +23,9 @@ module Cryptol.ModuleSystem (
   , evalDecls
   , noPat
   , focusedEnv
+  , getPrimMap
+  , renameVar
+  , renameType
 
     -- * Interfaces
   , Iface(..), IfaceDecls(..), genIface
@@ -31,8 +36,8 @@ import qualified Cryptol.Eval.Value        as E
 import           Cryptol.ModuleSystem.Env
 import           Cryptol.ModuleSystem.Interface
 import           Cryptol.ModuleSystem.Monad
-import           Cryptol.ModuleSystem.Name (Name)
-import           Cryptol.ModuleSystem.Renamer (Rename,BindsNames)
+import           Cryptol.ModuleSystem.Name (Name,PrimMap)
+import qualified Cryptol.ModuleSystem.Renamer as R
 import qualified Cryptol.ModuleSystem.Base as Base
 import qualified Cryptol.Parser.AST        as P
 import           Cryptol.Parser.Name (PName)
@@ -40,6 +45,7 @@ import           Cryptol.Parser.NoPat (RemovePatterns)
 import           Cryptol.Parser.Position (HasLoc)
 import qualified Cryptol.TypeCheck.AST     as T
 import qualified Cryptol.TypeCheck.Depends as T
+import qualified Cryptol.Utils.Ident as M
 
 
 -- Public Interface ------------------------------------------------------------
@@ -48,6 +54,9 @@ type ModuleCmd a = ModuleEnv -> IO (ModuleRes a)
 
 type ModuleRes a = (Either ModuleError (a,ModuleEnv), [ModuleWarning])
 
+getPrimMap :: ModuleCmd PrimMap
+getPrimMap me = runModuleM me Base.getPrimMap
+
 -- | Find the file associated with a module name in the module search path.
 findModule :: P.ModName -> ModuleCmd FilePath
 findModule n env = runModuleM env (Base.findModule n)
@@ -89,10 +98,12 @@ evalExpr :: T.Expr -> ModuleCmd E.Value
 evalExpr e env = runModuleM env (interactive (Base.evalExpr e))
 
 -- | Typecheck declarations.
-checkDecls :: (HasLoc (d Name), Rename d, T.FromDecl (d Name)
-              ,BindsNames (d PName))
+checkDecls :: (HasLoc (d Name), R.Rename d, T.FromDecl (d Name)
+              ,R.BindsNames (R.InModule (d PName)))
            => [d PName] -> ModuleCmd [T.DeclGroup]
-checkDecls ds env = runModuleM env (interactive (Base.checkDecls ds))
+checkDecls ds env = runModuleM env
+                  $ interactive
+                  $ Base.checkDecls ds
 
 -- | Evaluate declarations and add them to the extended environment.
 evalDecls :: [T.DeclGroup] -> ModuleCmd ()
@@ -100,3 +111,11 @@ evalDecls dgs env = runModuleM env (interactive (Base.evalDecls dgs))
 
 noPat :: RemovePatterns a => a -> ModuleCmd a
 noPat a env = runModuleM env (interactive (Base.noPat a))
+
+renameVar :: R.NamingEnv -> PName -> ModuleCmd Name
+renameVar names n env = runModuleM env $ interactive $
+  Base.rename M.interactiveName names (R.renameVar n)
+
+renameType :: R.NamingEnv -> PName -> ModuleCmd Name
+renameType names n env = runModuleM env $ interactive $
+  Base.rename M.interactiveName names (R.renameType n)
diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs
index 9527f2db..27592c7c 100644
--- a/src/Cryptol/ModuleSystem/Base.hs
+++ b/src/Cryptol/ModuleSystem/Base.hs
@@ -7,6 +7,7 @@
 -- Portability :  portable
 
 {-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE FlexibleContexts #-}
 
 module Cryptol.ModuleSystem.Base where
 
@@ -319,15 +320,16 @@ checkExpr e = do
 -- | Typecheck a group of declarations.
 --
 -- INVARIANT: This assumes that NoPat has already been run on the declarations.
-checkDecls :: (R.BindsNames (d PName), R.Rename d, T.FromDecl (d Name)
+checkDecls :: (R.BindsNames (R.InModule (d PName)), R.Rename d, T.FromDecl (d Name)
               ,HasLoc (d Name))
            => [d PName] -> ModuleM [T.DeclGroup]
 checkDecls ds = do
   (decls,names) <- getLocalEnv
 
   -- introduce names for the declarations before renaming them
-  rds <- rename interactiveName names $ R.shadowNames ds
-                                      $ traverse R.rename ds
+  rds <- rename interactiveName names
+       $ R.shadowNames (map (R.InModule interactiveName) ds)
+       $ traverse R.rename ds
 
   prims <- getPrimMap
   let act  = TCAction { tcAction = T.tcDecls, tcLinter = declsLinter
diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs
index 853ef93d..3d7115a2 100644
--- a/src/Cryptol/ModuleSystem/Renamer.hs
+++ b/src/Cryptol/ModuleSystem/Renamer.hs
@@ -17,12 +17,14 @@
 
 module Cryptol.ModuleSystem.Renamer (
     NamingEnv(), shadowing
-  , BindsNames(..), namingEnv'
+  , BindsNames(..), InModule(..), namingEnv'
   , checkNamingEnv
   , shadowNames
   , Rename(..), runRenamer, RenameM()
   , RenamerError(..)
   , RenamerWarning(..)
+  , renameVar
+  , renameType
   ) where
 
 import Cryptol.ModuleSystem.Name
diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs
index d81e8832..1ffa313b 100644
--- a/src/Cryptol/REPL/Command.hs
+++ b/src/Cryptol/REPL/Command.hs
@@ -48,9 +48,10 @@ import Cryptol.REPL.Monad
 import Cryptol.REPL.Trie
 
 import qualified Cryptol.ModuleSystem as M
-import qualified Cryptol.ModuleSystem.Name as M (preludeName)
+import qualified Cryptol.ModuleSystem.Name as M
 import qualified Cryptol.ModuleSystem.NamingEnv as M
 import qualified Cryptol.ModuleSystem.Renamer as M (RenamerWarning(SymbolShadowed))
+import qualified Cryptol.Utils.Ident as M
 
 import qualified Cryptol.Eval.Value as E
 import qualified Cryptol.Testing.Eval    as Test
@@ -90,6 +91,7 @@ import qualified Data.IntMap as IntMap
 import System.IO(hFlush,stdout)
 import System.Random.TF(newTFGen)
 import Numeric (showFFloat)
+import qualified Data.Text as ST
 import qualified Data.Text.Lazy as T
 
 #if __GLASGOW_HASKELL__ < 710
@@ -405,7 +407,7 @@ cmdProveSat isSat expr = do
         Symbolic.ProverError msg     -> rPutStrLn msg
         Symbolic.ThmResult ts        -> do
           rPutStrLn (if isSat then "Unsatisfiable" else "Q.E.D.")
-          let (t, e) = mkSolverResult cexStr (not isSat) (Left ts)
+          (t, e) <- mkSolverResult cexStr (not isSat) (Left ts)
           bindItVariable t e
         Symbolic.AllSatResult tevss -> do
           let tess = map (map $ \(t,e,_) -> (t,e)) tevss
@@ -417,8 +419,8 @@ cmdProveSat isSat expr = do
                     doc = ppPrec 3 parseExpr
                 rPrint $ hsep (doc : docs) <+>
                   text (if isSat then "= True" else "= False")
-              resultRecs = map (mkSolverResult cexStr isSat . Right) tess
-              collectTes tes = (t, es)
+          resultRecs <- mapM (mkSolverResult cexStr isSat . Right) tess
+          let collectTes tes = (t, es)
                 where
                   (ts, es) = unzip tes
                   t = case nub ts of
@@ -477,27 +479,38 @@ offlineProveSat isSat str mfile = do
         }
   liftModuleCmd $ Symbolic.satProveOffline cmd
 
+rIdent :: M.Ident
+rIdent  = M.packIdent "result"
+
 -- | Make a type/expression pair that is suitable for binding to @it@
 -- after running @:sat@ or @:prove@
 mkSolverResult :: String
                -> Bool
                -> Either [T.Type] [(T.Type, T.Expr)]
-               -> (T.Type, T.Expr)
-mkSolverResult thing result earg = (rty, re)
+               -> REPL (T.Type, T.Expr)
+mkSolverResult thing result earg =
+  do prims <- getPrimMap
+     let eError str = T.ePrim prims (M.packIdent "error")
+         addError t = (t, T.eError prims t ("no " ++ thing ++ " available"))
+
+         argF = case earg of
+                  Left ts   -> mkArgs (map addError ts)
+                  Right tes -> mkArgs tes
+
+         eTrue  = T.ePrim prims (M.packIdent "True")
+         eFalse = T.ePrim prims (M.packIdent "False")
+         resultE = if result then eTrue else eFalse
+
+         rty = T.TRec $ [(rIdent, T.tBit )] ++ map fst argF
+         re  = T.ERec $ [(rIdent, resultE)] ++ map snd argF
+
+     return (rty, re)
   where
-    rName = T.mkName "result"
-    rty = T.TRec $ [(rName, T.tBit )] ++ map fst argF
-    re  = T.ERec $ [(rName, resultE)] ++ map snd argF
-    resultE = if result then T.eTrue else T.eFalse
-    mkArgs tes = reverse (go tes [] (1 :: Int))
-      where
-        go [] fs _ = fs
-        go ((t, e):tes') fs n = go tes' (((argName, t), (argName, e)):fs) (n+1)
-          where argName = T.mkName ("arg" ++ show n)
-    argF = case earg of
-      Left ts -> mkArgs $ (map addError) ts
-        where addError t = (t, T.eError t ("no " ++ thing ++ " available"))
-      Right tes -> mkArgs tes
+  mkArgs tes = zipWith mkArg [1 :: Int ..] tes
+    where
+    mkArg n (t,e) =
+      let argName = M.packIdent ("arg" ++ show n)
+       in ((argName,t),(argName,e))
 
 specializeCmd :: String -> REPL ()
 specializeCmd str = do
@@ -520,7 +533,7 @@ typeOfCmd str = do
   -- XXX need more warnings from the module system
   --io (mapM_ printWarning ws)
   whenDebug (rPutStrLn (dump def))
-  (_,names) <- getFocusedEnv
+  (_,_,names) <- getFocusedEnv
   rPrint $ runDoc names $ pp re <+> text ":" <+> pp sig
 
 reloadCmd :: REPL ()
@@ -588,12 +601,13 @@ quitCmd  = stop
 
 browseCmd :: String -> REPL ()
 browseCmd pfx = do
-  env <- getFocusedEnv
+  (iface,_,disp) <- getFocusedEnv
+  let env = (iface,disp)
   browseTSyns env pfx
   browseNewtypes env pfx
   browseVars env pfx
 
-browseTSyns :: (M.IfaceDecls,NameEnv) -> String -> REPL ()
+browseTSyns :: (M.IfaceDecls,NameDisp) -> String -> REPL ()
 browseTSyns (decls,names) pfx = do
   let tsyns = keepOne "browseTSyns" `fmap` M.ifTySyns decls
       tsyns' = Map.filterWithKey (\k _ -> pfx `isNamePrefix` k) tsyns
@@ -604,7 +618,7 @@ browseTSyns (decls,names) pfx = do
     rPrint (runDoc names (nest 4 (vcat (map ppSyn (Map.toList tsyns')))))
     rPutStrLn ""
 
-browseNewtypes :: (M.IfaceDecls,NameEnv) -> String -> REPL ()
+browseNewtypes :: (M.IfaceDecls,NameDisp) -> String -> REPL ()
 browseNewtypes (decls,names) pfx = do
   let nts  = keepOne "browseNewtypes" `fmap` M.ifNewtypes decls
       nts' = Map.filterWithKey (\k _ -> pfx `isNamePrefix` k) nts
@@ -615,7 +629,7 @@ browseNewtypes (decls,names) pfx = do
     rPrint (runDoc names (nest 4 (vcat (map ppNT (Map.toList nts')))))
     rPutStrLn ""
 
-browseVars :: (M.IfaceDecls,NameEnv) -> String -> REPL ()
+browseVars :: (M.IfaceDecls,NameDisp) -> String -> REPL ()
 browseVars (decls,names) pfx = do
   let vars = keepOne "browseVars" `fmap` M.ifDecls decls
       allNames = vars
@@ -669,14 +683,16 @@ setOptionCmd str
                                    rPutStrLn ("Did you mean: `:set " ++ k1 ++ " =" ++ k2 ++ "`?")
 
 
+-- XXX at the moment, this can only look at declarations.
 helpCmd :: String -> REPL ()
 helpCmd cmd
   | null cmd  = mapM_ rPutStrLn (genHelp commandList)
   | otherwise =
     case parseHelpName cmd of
       Just qname ->
-        do (env,nameEnv) <- getFocusedEnv
-           case Map.lookup qname (M.ifDecls env) of
+        do (env,rnEnv,nameEnv) <- getFocusedEnv
+           name <- liftModuleCmd (M.renameVar rnEnv qname)
+           case Map.lookup name (M.ifDecls env) of
              Just [M.IfaceDecl { .. }] ->
                do rPutStrLn ""
 
@@ -723,10 +739,13 @@ handleCtrlC  = rPutStrLn "Ctrl-C"
 
 -- Utilities -------------------------------------------------------------------
 
-isNamePrefix :: String -> P.QName -> Bool
-isNamePrefix pfx n = case n of
-  P.QName _ (P.Name _) -> pfx `isPrefixOf` pretty n
-  _                    -> False
+isNamePrefix :: String -> M.Name -> Bool
+isNamePrefix pfx =
+  let pfx' = ST.pack pfx
+   in \n -> case M.nameInfo n of
+              M.Declared _ -> pfx' `ST.isPrefixOf` M.identText (M.nameIdent n)
+              M.Parameter  -> False
+
 
 {-
 printWarning :: (Range,Warning) -> IO ()
@@ -742,15 +761,18 @@ replParse parse str = case parse str of
   Right a -> return a
   Left e  -> raise (ParseError e)
 
-replParseInput :: String -> REPL P.ReplInput
+replParseInput :: String -> REPL (P.ReplInput P.PName)
 replParseInput = replParse (parseReplWith interactiveConfig . T.pack)
 
-replParseExpr :: String -> REPL P.Expr
+replParseExpr :: String -> REPL (P.Expr P.PName)
 replParseExpr = replParse (parseExprWith interactiveConfig . T.pack)
 
 interactiveConfig :: Config
 interactiveConfig = defaultConfig { cfgSource = "<interactive>" }
 
+getPrimMap :: REPL M.PrimMap
+getPrimMap  = liftModuleCmd M.getPrimMap
+
 liftModuleCmd :: M.ModuleCmd a -> REPL a
 liftModuleCmd cmd = moduleCmdResult =<< io . cmd =<< getModuleEnv
 
@@ -779,23 +801,22 @@ moduleCmdResult (res,ws0) = do
       filterShadowing w = Just w
 
   let ws = mapMaybe filterDefaults . mapMaybe filterShadowing $ ws0
-  (_,names) <- getFocusedEnv
+  (_,_,names) <- getFocusedEnv
   mapM_ (rPrint . runDoc names . pp) ws
   case res of
     Right (a,me') -> setModuleEnv me' >> return a
     Left err      -> raise (ModuleSystemError names err)
 
-replCheckExpr :: P.Expr -> REPL (P.Expr,T.Expr,T.Schema)
+replCheckExpr :: P.Expr P.PName -> REPL (P.Expr M.Name,T.Expr,T.Schema)
 replCheckExpr e = liftModuleCmd $ M.checkExpr e
 
 -- | Check declarations as though they were defined at the top-level.
-replCheckDecls :: [P.Decl] -> REPL [T.DeclGroup]
+replCheckDecls :: [P.Decl P.PName] -> REPL [T.DeclGroup]
 replCheckDecls ds = do
   npds <- liftModuleCmd $ M.noPat ds
   denv <- getDynEnv
-  let dnames = M.namingEnv npds
-  ne' <- M.travNamingEnv uniqify dnames
-  let denv' = denv { M.deNames = ne' `M.shadowing` M.deNames denv }
+  dnames <- M.liftSupply (M.namingEnv' (map (M.InModule M.interactiveName) npds))
+  let denv' = denv { M.deNames = dnames `M.shadowing` M.deNames denv }
       undo exn = do
         -- if typechecking fails, we want to revert changes to the
         -- dynamic environment and reraise
@@ -803,12 +824,12 @@ replCheckDecls ds = do
         raise exn
   setDynEnv denv'
   let topDecls = [ P.Decl (P.TopLevel P.Public Nothing d) | d <- npds ]
-  catch (liftModuleCmd $ M.checkDecls topDecls) undo
+  catch (liftModuleCmd (M.checkDecls topDecls)) undo
 
 replSpecExpr :: T.Expr -> REPL T.Expr
 replSpecExpr e = liftModuleCmd $ S.specialize e
 
-replEvalExpr :: P.Expr -> REPL (E.Value, T.Type)
+replEvalExpr :: P.Expr P.PName -> REPL (E.Value, T.Type)
 replEvalExpr expr =
   do (_,def,sig) <- replCheckExpr expr
 
@@ -835,14 +856,16 @@ replEvalExpr expr =
   warnDefault ns (x,t) =
         rPrint $ text "Assuming" <+> ppWithNames ns x <+> text "=" <+> pp t
 
+
+itIdent :: M.Ident
+itIdent  = M.packIdent "it"
+
 -- | Creates a fresh binding of "it" to the expression given, and adds
 -- it to the current dynamic environment
 bindItVariable :: T.Type -> T.Expr -> REPL ()
 bindItVariable ty expr = do
-  let it = T.QName Nothing (P.mkName "it")
-  freshIt <- uniqify it
-  let dg = T.NonRecursive decl
-      schema = T.Forall { T.sVars  = []
+  freshIt <- freshName itIdent
+  let schema = T.Forall { T.sVars  = []
                         , T.sProps = []
                         , T.sType  = ty
                         }
@@ -854,10 +877,10 @@ bindItVariable ty expr = do
                     , T.dFixity     = Nothing
                     , T.dDoc        = Nothing
                     }
-  liftModuleCmd (M.evalDecls [dg])
+  liftModuleCmd (M.evalDecls [T.NonRecursive decl])
   denv <- getDynEnv
-  let en = M.EFromBind (P.Located emptyRange freshIt)
-      nenv' = M.singletonE it en `M.shadowing` M.deNames denv
+  let nenv' = M.singletonE (P.UnQual itIdent) freshIt
+                           `M.shadowing` M.deNames denv
   setDynEnv $ denv { M.deNames = nenv' }
 
 -- | Creates a fresh binding of "it" to a finite sequence of
@@ -870,7 +893,7 @@ bindItVariables ty exprs = bindItVariable seqTy seqExpr
     seqTy = T.tSeq (T.tNum len) ty
     seqExpr = T.EList exprs ty
 
-replEvalDecl :: P.Decl -> REPL ()
+replEvalDecl :: P.Decl P.PName -> REPL ()
 replEvalDecl decl = do
   dgs <- replCheckDecls [decl]
   whenDebug (mapM_ (\dg -> (rPutStrLn (dump dg))) dgs)
diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs
index b8d17945..78180846 100644
--- a/src/Cryptol/REPL/Monad.hs
+++ b/src/Cryptol/REPL/Monad.hs
@@ -31,7 +31,7 @@ module Cryptol.REPL.Monad (
   , getFocusedEnv, keepOne
   , getModuleEnv, setModuleEnv
   , getDynEnv, setDynEnv
-  , uniqify
+  , uniqify, freshName
   , getTSyns, getNewtypes, getVars
   , whenDebug
   , getExprNames
@@ -71,12 +71,15 @@ import Cryptol.REPL.Trie
 import Cryptol.Eval (EvalError)
 import qualified Cryptol.ModuleSystem as M
 import qualified Cryptol.ModuleSystem.Env as M
+import qualified Cryptol.ModuleSystem.Name as M
 import qualified Cryptol.ModuleSystem.NamingEnv as M
 import Cryptol.Parser (ParseError,ppError)
 import Cryptol.Parser.NoInclude (IncludeError,ppIncludeError)
 import Cryptol.Parser.NoPat (Error)
+import Cryptol.Parser.Position (emptyRange)
 import qualified Cryptol.TypeCheck.AST as T
 import qualified Cryptol.TypeCheck as T
+import qualified Cryptol.Utils.Ident as I
 import Cryptol.Utils.PP
 import Cryptol.Utils.Panic (panic)
 import qualified Cryptol.Parser.AST as P
@@ -86,7 +89,7 @@ import Control.Monad (ap,unless,when)
 import Control.Monad.IO.Class
 import Data.Char (isSpace)
 import Data.IORef
-    (IORef,newIORef,readIORef,modifyIORef)
+    (IORef,newIORef,readIORef,modifyIORef,atomicModifyIORef)
 import Data.List (intercalate, isPrefixOf, unfoldr)
 import Data.Maybe (catMaybes)
 import Data.Typeable (Typeable)
@@ -115,7 +118,6 @@ data RW = RW
   , eContinue    :: Bool
   , eIsBatch     :: Bool
   , eModuleEnv   :: M.ModuleEnv
-  , eNameSupply  :: Int
   , eUserEnv     :: UserEnv
   , ePutStr      :: String -> IO ()
   , eLetEnabled  :: Bool
@@ -131,7 +133,6 @@ defaultRW isBatch = do
     , eContinue    = True
     , eIsBatch     = isBatch
     , eModuleEnv   = env
-    , eNameSupply  = 0
     , eUserEnv     = mkUserEnv userOptions
     , ePutStr      = putStr
     , eLetEnabled  = True
@@ -177,6 +178,12 @@ instance Monad REPL where
 instance MonadIO REPL where
   liftIO = io
 
+instance M.FreshM REPL where
+  liftSupply f = modifyRW $ \ RW { .. } ->
+    let (a,s') = f (M.meSupply eModuleEnv)
+     in (RW { eModuleEnv = eModuleEnv { M.meSupply = s' }, .. },a)
+
+
 -- Exceptions ------------------------------------------------------------------
 
 -- | REPL exceptions.
@@ -207,7 +214,7 @@ instance PP REPLException where
                                   ]
     NoPatError es        -> vcat (map pp es)
     NoIncludeError es    -> vcat (map ppIncludeError es)
-    ModuleSystemError ns me -> withNameDisp ns (pp me)
+    ModuleSystemError ns me -> fixNameDisp ns (pp me)
     EvalError e          -> pp e
     EvalPolyError s      -> text "Cannot evaluate polymorphic value."
                          $$ text "Type:" <+> pp s
@@ -243,6 +250,9 @@ io m = REPL (\ _ -> m)
 getRW :: REPL RW
 getRW  = REPL readIORef
 
+modifyRW :: (RW -> (RW,a)) -> REPL a
+modifyRW f = REPL (\ ref -> atomicModifyIORef ref f)
+
 modifyRW_ :: (RW -> RW) -> REPL ()
 modifyRW_ f = REPL (\ ref -> modifyIORef ref f)
 
@@ -339,47 +349,51 @@ keepOne src as = case as of
   [a] -> a
   _   -> panic ("REPL: " ++ src) ["name clash in interface file"]
 
-getFocusedEnv :: REPL (M.IfaceDecls,NameDisp)
+getFocusedEnv :: REPL (M.IfaceDecls,M.NamingEnv,NameDisp)
 getFocusedEnv  = do
   me <- getModuleEnv
   -- dyNames is a NameEnv that removes the #Uniq prefix from interactively-bound
   -- variables.
   let (dyDecls,dyNames,dyDisp) = M.dynamicEnv me
-
-  -- the subtle part here is removing the #Uniq prefix from
-  -- interactively-bound variables, and also excluding any that are
-  -- shadowed and thus can no longer be referenced
   let (fDecls,fNames,fDisp) = M.focusedEnv me
-      edecls = M.ifDecls dyDecls
-      -- is this QName something the user might actually type?
-      isShadowed (qn@(P.QName (Just (P.unModName -> ['#':_])) name), _) =
-          case Map.lookup localName neExprs of
-            Nothing -> False
-            Just uniqueNames -> isNamed uniqueNames
-        where localName = P.QName Nothing name
-              isNamed us = any (== qn) (map M.qname us)
-              neExprs = M.neExprs (M.deNames (M.meDynEnv me))
-      isShadowed _ = False
-      unqual ((P.QName _ name), ifds) = (P.QName Nothing name, ifds)
-      edecls' = Map.fromList
-              . map unqual
-              . filter isShadowed
-              $ Map.toList edecls
-  return (decls `mappend` mempty { M.ifDecls = edecls' }, names `mappend` dyNames)
+  return ( dyDecls `mappend` fDecls
+         , dyNames `M.shadowing` fNames
+         , dyDisp `mappend` fDisp)
 
-getVars :: REPL (Map.Map P.QName M.IfaceDecl)
+  -- -- the subtle part here is removing the #Uniq prefix from
+  -- -- interactively-bound variables, and also excluding any that are
+  -- -- shadowed and thus can no longer be referenced
+  -- let (fDecls,fNames,fDisp) = M.focusedEnv me
+  --     edecls = M.ifDecls dyDecls
+  --     -- is this QName something the user might actually type?
+  --     isShadowed (qn@(P.QName (Just (P.unModName -> ['#':_])) name), _) =
+  --         case Map.lookup localName neExprs of
+  --           Nothing -> False
+  --           Just uniqueNames -> isNamed uniqueNames
+  --       where localName = P.QName Nothing name
+  --             isNamed us = any (== qn) (map M.qname us)
+  --             neExprs = M.neExprs (M.deNames (M.meDynEnv me))
+  --     isShadowed _ = False
+  --     unqual ((P.QName _ name), ifds) = (P.QName Nothing name, ifds)
+  --     edecls' = Map.fromList
+  --             . map unqual
+  --             . filter isShadowed
+  --             $ Map.toList edecls
+  -- return (decls `mappend` mempty { M.ifDecls = edecls' }, names `mappend` dyNames)
+
+getVars :: REPL (Map.Map M.Name M.IfaceDecl)
 getVars  = do
-  (decls,_) <- getFocusedEnv
+  (decls,_,_) <- getFocusedEnv
   return (keepOne "getVars" `fmap` M.ifDecls decls)
 
-getTSyns :: REPL (Map.Map P.QName T.TySyn)
+getTSyns :: REPL (Map.Map M.Name T.TySyn)
 getTSyns  = do
-  (decls,_) <- getFocusedEnv
+  (decls,_,_) <- getFocusedEnv
   return (keepOne "getTSyns" `fmap` M.ifTySyns decls)
 
-getNewtypes :: REPL (Map.Map P.QName T.Newtype)
+getNewtypes :: REPL (Map.Map M.Name T.Newtype)
 getNewtypes = do
-  (decls,_) <- getFocusedEnv
+  (decls,_,_) <- getFocusedEnv
   return (keepOne "getNewtypes" `fmap` M.ifNewtypes decls)
 
 -- | Get visible variable names.
@@ -399,7 +413,7 @@ getPropertyNames =
      return [ getName x | (x,d) <- Map.toList xs,
                 T.PragmaProperty `elem` M.ifDeclPragmas d ]
 
-getName :: P.QName -> String
+getName :: M.Name -> String
 getName  = show . pp
 
 getModuleEnv :: REPL M.ModuleEnv
@@ -419,14 +433,32 @@ setDynEnv denv = do
 -- | Given an existing qualified name, prefix it with a
 -- relatively-unique string. We make it unique by prefixing with a
 -- character @#@ that is not lexically valid in a module name.
-uniqify :: P.QName -> REPL P.QName
-uniqify (P.QName Nothing name) = do
-  i <- eNameSupply `fmap` getRW
-  modifyRW_ (\rw -> rw { eNameSupply = i+1 })
-  let modname' = P.mkModName [ '#' : ("Uniq_" ++ show i) ]
-  return (P.QName (Just modname') name)
-uniqify qn =
-  panic "[REPL] uniqify" ["tried to uniqify a qualified name: " ++ pretty qn]
+uniqify :: M.Name -> REPL M.Name
+
+uniqify name =
+  case M.nameInfo name of
+    M.Declared ns ->
+      M.liftSupply (M.mkDeclared ns (M.nameIdent name) (M.nameLoc name))
+
+    M.Parameter ->
+      panic "[REPL] uniqify" ["tried to uniqify a parameter: " ++ pretty name]
+
+
+-- uniqify (P.QName Nothing name) = do
+--   i <- eNameSupply `fmap` getRW
+--   modifyRW_ (\rw -> rw { eNameSupply = i+1 })
+--   let modname' = P.mkModName [ '#' : ("Uniq_" ++ show i) ]
+--   return (P.QName (Just modname') name)
+
+-- uniqify qn =
+--   panic "[REPL] uniqify" ["tried to uniqify a qualified name: " ++ pretty qn]
+
+
+-- | Generate a fresh name using the given index. The name will reside within
+-- the "<interactive>" namespace.
+freshName :: I.Ident -> REPL M.Name
+freshName i = M.liftSupply (M.mkDeclared I.interactiveName i emptyRange)
+
 
 -- User Environment Interaction ------------------------------------------------
 
diff --git a/src/Cryptol/Symbolic.hs b/src/Cryptol/Symbolic.hs
index 6ebf734b..5407530c 100644
--- a/src/Cryptol/Symbolic.hs
+++ b/src/Cryptol/Symbolic.hs
@@ -21,7 +21,7 @@ import qualified Control.Exception as X
 
 import qualified Data.SBV.Dynamic as SBV
 
-import qualified Cryptol.ModuleSystem as M
+import qualified Cryptol.ModuleSystem as M hiding (getPrimMap)
 import qualified Cryptol.ModuleSystem.Env as M
 import qualified Cryptol.ModuleSystem.Base as M
 import qualified Cryptol.ModuleSystem.Monad as M
diff --git a/src/Cryptol/TypeCheck/AST.hs b/src/Cryptol/TypeCheck/AST.hs
index 5f154b08..6beccd72 100644
--- a/src/Cryptol/TypeCheck/AST.hs
+++ b/src/Cryptol/TypeCheck/AST.hs
@@ -31,7 +31,7 @@ import Cryptol.Parser.AST ( Selector(..),Pragma(..), ppSelector
                           , Import(..), ImportSpec(..), ExportType(..)
                           , ExportSpec(..), isExportedBind
                           , isExportedType, Fixity(..) )
-import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName)
+import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName,packIdent)
 import Cryptol.Utils.Panic(panic)
 import Cryptol.TypeCheck.PP
 import Cryptol.TypeCheck.Solver.InfNat
@@ -548,6 +548,20 @@ newtypeConType nt =
 ePrim :: PrimMap -> Ident -> Expr
 ePrim pm n = EVar (lookupPrimDecl n pm)
 
+-- | Make an expression that is `error` pre-applied to a type and a message.
+eError :: PrimMap -> Type -> String -> Expr
+eError prims t str =
+  EApp (ETApp (ETApp (ePrim prims (packIdent "error")) t)
+              (tNum (length str))) (eString prims str)
+
+eString :: PrimMap -> String -> Expr
+eString prims str = EList (map (eChar prims) str) tChar
+
+eChar :: PrimMap -> Char -> Expr
+eChar prims c = ETApp (ETApp (ePrim prims (packIdent "demote")) (tNum v)) (tNum w)
+  where v = fromEnum c
+        w = 8 :: Int
+
 
 --------------------------------------------------------------------------------
 
diff --git a/src/Cryptol/Utils/PP.hs b/src/Cryptol/Utils/PP.hs
index e46e8bf5..de340451 100644
--- a/src/Cryptol/Utils/PP.hs
+++ b/src/Cryptol/Utils/PP.hs
@@ -32,6 +32,9 @@ import qualified Text.PrettyPrint as PJ
 data NameDisp = EmptyNameDisp
               | NameDisp (ModName -> Ident -> Maybe NameFormat)
 
+instance Show NameDisp where
+  show _ = "<NameDisp>"
+
 instance M.Monoid NameDisp where
   mempty = EmptyNameDisp
 
@@ -67,6 +70,10 @@ getNameFormat _ _ EmptyNameDisp = NotInScope
 withNameDisp :: (NameDisp -> Doc) -> Doc
 withNameDisp k = Doc (\disp -> runDoc disp (k disp))
 
+-- | Fix the way that names are displayed inside of a doc.
+fixNameDisp :: NameDisp -> Doc -> Doc
+fixNameDisp disp (Doc f) = Doc (\ _ -> f disp)
+
 
 -- Documents -------------------------------------------------------------------