diff --git a/examples/fail.quox b/examples/fail.quox
index a3edac8..daf5c05 100644
--- a/examples/fail.quox
+++ b/examples/fail.quox
@@ -8,3 +8,9 @@ def repeat-enum-case : {a} → {a} =
 
 #[fail "duplicate tags"]
 def repeat-enum-type : {a, a} = 'a
+
+#[fail "double-def.X has already been defined"]
+namespace double-def {
+  def0 X : ★ = {a}
+  def0 X : ★ = {a}
+}
diff --git a/exe/Main.idr b/exe/Main.idr
index e522169..dbb7897 100644
--- a/exe/Main.idr
+++ b/exe/Main.idr
@@ -1,46 +1,201 @@
 module Main
 
-import Quox.Syntax
+import Quox.Syntax as Q
 import Quox.Parser
-import Quox.Definition
+import Quox.Definition as Q
 import Quox.Pretty
+import Quox.Untyped.Syntax as U
+import Quox.Untyped.Erase
+import Options
 
-import System
 import Data.IORef
 import Data.SortedSet
+import Text.Show.PrettyVal
+import Text.Show.Pretty
+import System
+import System.File
 import Control.Eff
 
-private
-Opts : LayoutOpts
-Opts = Opts 80
+%hide Doc.(>>=)
+%hide Core.(>>=)
+
+
+parameters {auto _ : HasIO io} (width : Nat)
+  private
+  putDoc : Doc (Opts width) -> io ()
+  putDoc = putStr . render _
+
+  private
+  fPutDoc : File -> Doc (Opts width) -> io (Either FileError ())
+  fPutDoc h = fPutStr h . render _
+
+  private
+  putDocErr : Doc (Opts width) -> io ()
+  putDocErr = ignore . fPutDoc stderr
+
+  private
+  die : Doc (Opts width) -> io a
+  die err = do putDocErr err; exitFailure
 
 private
-putDoc : Doc Opts -> IO ()
-putDoc = putStr . render Opts
+runPretty : Options -> Eff Pretty a -> a
+runPretty opts act =
+  let doColor = opts.color && opts.outFile == Stdout
+      hl      = if doColor then highlightSGR else noHighlight
+  in
+  runPrettyWith Outer opts.flavor hl 2 act
 
 private
-die : Doc Opts -> IO a
-die err = do putDoc err; exitFailure
+putErrLn : HasIO io => String -> io ()
+putErrLn = ignore . fPutStrLn stderr
 
 private
-prettySig : Name -> Definition -> Eff Pretty (Doc Opts)
-prettySig name def = do
-  qty  <- prettyQty def.qty.qty
-  name <- prettyFree name
-  type <- prettyTerm [<] [<] def.type
-  hangDSingle (hsep [hcat [qty, !dotD, name], !colonD]) type
+record State where
+  constructor MkState
+  seen : IORef SeenSet
+  defs : IORef Q.Definitions
+  ns   : IORef Mods
+  suf  : IORef NameSuf
+%name Main.State state
+
+private
+newState : HasIO io => io State
+newState = pure $ MkState {
+  seen = !(newIORef empty),
+  defs = !(newIORef empty),
+  ns   = !(newIORef [<]),
+  suf  = !(newIORef 0)
+}
+
+private
+data Error
+  = ParseError String Parser.Error
+  | FromParserError FromParser.Error
+  | EraseError Erase.Error
+  | WriteError FilePath FileError
+%hide FromParser.Error
+%hide Erase.Error
+%hide Lexer.Error
+%hide Parser.Error
+
+private
+loadError : Loc -> FilePath -> FileError -> Error
+loadError loc file err = FromParserError $ LoadError loc file err
+
+private
+data CompileTag = OPTS | STATE
+
+private
+Compile : List (Type -> Type)
+Compile =
+  [Except Error,
+   ReaderL STATE State, ReaderL OPTS Options,
+   LoadFile, IO]
+
+private
+runCompile : Options -> State -> Eff Compile a -> IO (Either Error a)
+runCompile opts state act =
+  fromIOErr $ runEff act $ with Union.(::)
+    [handleExcept (\e => ioLeft e),
+     handleReaderConst state,
+     handleReaderConst opts,
+     handleLoadFileIOE loadError ParseError state.seen opts.include,
+     liftIO]
+
+
+private
+data StopTag = STOP
+
+private
+CompileStop : List (Type -> Type)
+CompileStop = FailL STOP :: Compile
+
+private
+withEarlyStop : Has (FailL STOP) fs => Eff fs () -> Eff (fs - FailL STOP) ()
+withEarlyStop = ignore . runFailAt STOP
+
+private
+stopHere : Has (FailL STOP) fs => Eff fs ()
+stopHere = failAt STOP
+
+
+private
+FlexDoc : Type
+FlexDoc = {opts : LayoutOpts} -> Doc opts
+
+
+private
+outputDoc : FlexDoc -> Eff Compile ()
+outputDoc doc =
+  case !(asksAt OPTS outFile) of
+    None   => pure ()
+    Stdout => putDoc !(asksAt OPTS width) doc
+    File f => do
+      res <- withFile f WriteTruncate pure $ \h =>
+        fPutDoc !(asksAt OPTS width) h doc
+      rethrow $ mapFst (WriteError f) res
+
+private
+outputDocStopIf : Phase -> FlexDoc -> Eff CompileStop ()
+outputDocStopIf p doc =
+  when (!(asksAt OPTS until) == Just p) $ do
+    lift (outputDoc doc)
+    stopHere
+
+private
+liftFromParser : Eff FromParserIO a -> Eff CompileStop a
+liftFromParser act =
+  runEff act $ with Union.(::)
+    [\g => send g,
+     handleExcept (\err => throw $ FromParserError err),
+     handleStateIORef !(asksAt STATE defs),
+     handleStateIORef !(asksAt STATE ns),
+     handleStateIORef !(asksAt STATE suf)]
+
+private
+liftErase : Q.Definitions -> Eff Erase a -> Eff CompileStop a
+liftErase defs act =
+  runEff act
+    [\case Err e => throw $ EraseError e,
+     \case Ask   => pure defs,
+     handleStateIORef !(asksAt STATE suf)]
+
+
+private
+processFile : String -> Eff Compile ()
+processFile file = withEarlyStop $ do
+  Just ast <- loadFile noLoc file
+    | Nothing => pure ()
+  putErrLn "checking \{file}"
+  outputDocStopIf Parse $ dumpDoc ast
+  defList <- liftFromParser $ concat <$> traverse fromPTopLevel ast
+  outputDocStopIf Check $ runPretty !(askAt OPTS) $
+    vsep <$> traverse (uncurry Q.prettyDef) defList
+  let defs = SortedMap.fromList defList
+  erased <- liftErase defs $
+    traverse (\(x, d) => (x,) <$> eraseDef x d) defList
+  outputDocStopIf Erase $ runPretty !(askAt OPTS) $
+    vsep . catMaybes <$> traverse (uncurry U.prettyDef) erased
+  die "that's all folks"
+
+private
+dieError : HasIO io => Options -> Error -> io a
+dieError opts e = do
+  die opts.width $ runPretty opts $ case e of
+    ParseError file e => prettyParseError file e
+    FromParserError e => FromParser.prettyError True e
+    EraseError      e => Erase.prettyError True e
+    WriteError file e => pure $
+      hangSingle 2 (text "couldn't write file \{file}:") (pshow e)
 
 export
 main : IO ()
 main = do
-  seen <- newIORef SortedSet.empty
-  defs <- newIORef SortedMap.empty
-  suf  <- newIORef 0
-  for_ (drop 1 !getArgs) $ \file => do
-    putStrLn "checking \{file}"
-    Right res <- fromParserIO ["."] seen suf defs $ loadProcessFile noLoc file
-      | Left err => die $ runPrettyColor $ prettyError True err
-    for_ res $ \(name, def) => putDoc $ runPrettyColor $ prettySig name def
+  (_, opts, files) <- options
+  case !(runCompile opts !newState $ traverse_ processFile files) of
+    Right () => pure ()
+    Left  e  => dieError opts e
+
 
 -----------------------------------
 {-
diff --git a/exe/Options.idr b/exe/Options.idr
new file mode 100644
index 0000000..58b545b
--- /dev/null
+++ b/exe/Options.idr
@@ -0,0 +1,158 @@
+module Options
+
+import Quox.Pretty
+import System
+import System.Console.GetOpt
+import System.File
+import System.Term
+import Derive.Prelude
+
+%language ElabReflection
+
+public export
+data OutFile = File String | Stdout | None
+%name OutFile f
+%runElab derive "OutFile" [Eq, Ord, Show]
+
+public export
+data Phase = Parse | Check | Erase
+%name Phase p
+%runElab derive "Phase" [Eq, Ord, Show]
+
+||| a list of all `Phase`s
+public export %inline
+allPhases : List Phase
+allPhases = %runElab do
+  -- as a script so it stays up to date
+  cs <- getCons $ fst !(lookupName "Phase")
+  traverse (check . var) cs
+
+public export
+record Options where
+  constructor MkOpts
+  color   : Bool
+  outFile : OutFile
+  until   : Maybe Phase
+  flavor  : Pretty.Flavor
+  width   : Nat
+  include : List String
+%name Options opts
+%runElab derive "Options" [Show]
+
+export
+defaultOpts : IO Options
+defaultOpts = pure $ MkOpts {
+  color   = True,
+  outFile = Stdout,
+  until   = Nothing,
+  flavor  = Unicode,
+  width   = cast !getTermCols,
+  include = ["."]
+}
+
+private
+data HelpType = Common | All
+
+private
+data OptAction = ShowHelp HelpType | Err String | Ok (Options -> Options)
+%name OptAction act
+
+private
+toOutFile : String -> OptAction
+toOutFile ""  = Ok {outFile := None}
+toOutFile "-" = Ok {outFile := Stdout}
+toOutFile f   = Ok {outFile := File f}
+
+private
+phaseName : Phase -> String
+phaseName Parse = "parse"
+phaseName Check = "check"
+phaseName Erase = "erase"
+
+private
+toPhase : String -> OptAction
+toPhase str = case toLower str of
+  "parse" => Ok {until := Just Parse}
+  "check" => Ok {until := Just Check}
+  "erase" => Ok {until := Just Erase}
+  _       => Err "unknown phase name \{show str}\nphases: \{phaseNames}"
+where phaseNames = joinBy ", " $ map phaseName allPhases
+
+private
+toWidth : String -> OptAction
+toWidth s = case parsePositive s of
+  Just n  => Ok {width := n}
+  Nothing => Err "invalid width: \{show s}"
+
+private
+commonOptDescrs' : List (OptDescr OptAction)
+commonOptDescrs' = [
+  MkOpt ['i'] ["include"] (ReqArg (\i => Ok {include $= (i ::)}) "<dir>")
+    "add a directory to look for source files",
+  MkOpt ['o'] ["output"] (ReqArg toOutFile "<file>")
+    "output file (\"-\" for stdout, \"\" for no output)",
+  MkOpt ['P'] ["phase"] (ReqArg toPhase "<phase>")
+    "phase to stop at (by default go as far as exists)"
+]
+
+private
+extraOptDescrs : List (OptDescr OptAction)
+extraOptDescrs = [
+  MkOpt [] ["unicode"] (NoArg $ Ok {flavor := Unicode})
+    "use unicode syntax when printing (default)",
+  MkOpt [] ["ascii"] (NoArg $ Ok {flavor := Ascii})
+    "use ascii syntax when printing",
+  MkOpt [] ["width"] (ReqArg toWidth "<width>")
+    "max output width (defaults to terminal width)",
+  MkOpt [] ["color", "colour"] (NoArg $ Ok {color := True})
+    "use colour output (default)",
+  MkOpt [] ["no-color", "no-colour"] (NoArg $ Ok {color := False})
+    "don't use colour output"
+]
+
+private
+helpOptDescrs : List (OptDescr OptAction)
+helpOptDescrs = [
+  MkOpt ['h'] ["help"]     (NoArg $ ShowHelp Common) "show common options",
+  MkOpt []    ["help-all"] (NoArg $ ShowHelp All)    "show all options"
+]
+
+commonOptDescrs = commonOptDescrs' ++ helpOptDescrs
+allOptDescrs    = commonOptDescrs' ++ extraOptDescrs ++ helpOptDescrs
+
+export
+usageHeader : String
+usageHeader = joinBy "\n" [
+  "quox [options] [file.quox ...]",
+  "rawr"
+]
+
+export
+usage : List (OptDescr _) -> IO a
+usage ds = do
+  ignore $ fPutStr stderr $ usageInfo usageHeader ds
+  exitSuccess
+
+private
+applyAction : Options -> OptAction -> IO Options
+applyAction opts (ShowHelp Common) = usage commonOptDescrs
+applyAction opts (ShowHelp All)    = usage allOptDescrs
+applyAction opts (Err err)         = die err
+applyAction opts (Ok f)            = pure $ f opts
+
+private
+finalise : Options -> Options
+finalise = {include $= reverse}
+
+export
+options : IO (String, Options, List String)
+options = do
+  app :: args <- getArgs
+    | [] => die "couldn't get command line arguments"
+  let res = getOpt Permute allOptDescrs args
+  unless (null res.errors) $
+    die $ trim $ concat res.errors
+  unless (null res.unrecognized) $
+    die "unrecognised options: \{joinBy ", " res.unrecognized}"
+  opts <- foldlM applyAction !defaultOpts res.options
+  pure (app, finalise opts, res.nonOptions)
diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr
index e537962..f34a3d7 100644
--- a/lib/Quox/Parser/FromParser.idr
+++ b/lib/Quox/Parser/FromParser.idr
@@ -335,6 +335,8 @@ export covering
 fromPDef : PDefinition -> Eff FromParserPure NDefinition
 fromPDef (MkPDef qty pname ptype pterm defLoc) = do
   name <- fromPBaseNameNS pname
+  when !(getsAt DEFS $ isJust . lookup name) $ do
+    throw $ AlreadyExists defLoc name
   gqty <- globalPQty qty.val qty.loc
   let sqty = globalToSubj gqty
   type <- traverse fromPTerm ptype
diff --git a/lib/Quox/Parser/FromParser/Error.idr b/lib/Quox/Parser/FromParser/Error.idr
index 44cd0db..eee70b5 100644
--- a/lib/Quox/Parser/FromParser/Error.idr
+++ b/lib/Quox/Parser/FromParser/Error.idr
@@ -32,6 +32,7 @@ data Error =
   | DimNameInTerm Loc PBaseName
   | DisplacedBoundVar Loc PName
   | WrapTypeError TypeError
+  | AlreadyExists Loc Name
   | LoadError Loc FilePath FileError
   | ExpectedFail Loc
   | WrongFail String Error Loc
@@ -112,6 +113,10 @@ parameters {opts : LayoutOpts} (showContext : Bool)
   prettyError (WrapTypeError err) =
     Typing.prettyError showContext $ trimContext 2 err
 
+  prettyError (AlreadyExists loc name) = pure $
+    vsep [!(prettyLoc loc),
+          sep [!(prettyFree name), "has already been defined"]]
+
   prettyError (LoadError loc file err) = pure $
     vsep [!(prettyLoc loc),
           "couldn't load file" <++> text file,
diff --git a/lib/Quox/Pretty.idr b/lib/Quox/Pretty.idr
index 4aaf792..4753d76 100644
--- a/lib/Quox/Pretty.idr
+++ b/lib/Quox/Pretty.idr
@@ -115,11 +115,14 @@ export %inline
 hangD : {opts : LayoutOpts} -> Doc opts -> Doc opts -> Eff Pretty (Doc opts)
 hangD d1 d2 = pure $ hangSep !(askAt INDENT) d1 d2
 
+export %inline
+hangSingle : {opts : LayoutOpts} -> Nat -> Doc opts -> Doc opts -> Doc opts
+hangSingle n d1 d2 = ifMultiline (d1 <++> d2) (vappend d1 (indent n d2))
+
 export %inline
 hangDSingle : {opts : LayoutOpts} -> Doc opts -> Doc opts ->
               Eff Pretty (Doc opts)
-hangDSingle d1 d2 =
-  pure $ ifMultiline (d1 <++> d2) (vappend d1 !(indentD d2))
+hangDSingle d1 d2 = pure $ hangSingle !(askAt INDENT) d1 d2
 
 
 export
@@ -193,6 +196,11 @@ parameters {opts : LayoutOpts} {auto _ : Foldable t}
   fillSeparateTight d = fillSep . exceptLast (<+> d) . toList
 
 
+export %inline
+pshow : {opts : LayoutOpts} -> Show a => a -> Doc opts
+pshow = text . show
+
+
 export %inline
 ifUnicode : (uni, asc : Lazy a) -> Eff Pretty a
 ifUnicode uni asc =
diff --git a/lib/Quox/Syntax/DimEq.idr b/lib/Quox/Syntax/DimEq.idr
index 4f9ba19..574414f 100644
--- a/lib/Quox/Syntax/DimEq.idr
+++ b/lib/Quox/Syntax/DimEq.idr
@@ -237,9 +237,20 @@ setSelf (B i _)    (C eqs) with (compareP i i) | (compare i.nat i.nat)
   _ | IsGT gt | GT = absurd gt
 
 
+private %inline
+dimEqPrec : BContext d -> Maybe (DimEq' d) -> PPrec
+dimEqPrec vars eqs =
+  if length vars <= 1 && maybe True null eqs then Arg else Outer
+
 private
-prettyDVars : {opts : _} -> BContext d -> Eff Pretty (SnocList (Doc opts))
-prettyDVars = traverse prettyDBind . toSnocList'
+prettyDVars' : {opts : _} -> BContext d -> Eff Pretty (SnocList (Doc opts))
+prettyDVars' = traverse prettyDBind . toSnocList'
+
+export
+prettyDVars : {opts : _} -> BContext d -> Eff Pretty (Doc opts)
+prettyDVars vars =
+  parensIfM (dimEqPrec vars Nothing) $
+  fillSeparateTight !commaD $ !(prettyDVars' vars)
 
 private
 prettyCst : {opts : _} -> BContext d -> Dim d -> Dim d -> Eff Pretty (Doc opts)
@@ -256,16 +267,16 @@ prettyCsts dnames (eqs :< Just q)  =
 
 export
 prettyDimEq' : {opts : _} -> BContext d -> DimEq' d -> Eff Pretty (Doc opts)
-prettyDimEq' dnames eqs = do
-  vars <- prettyDVars dnames
-  eqs  <- prettyCsts dnames eqs
-  let prec = if length vars <= 1 && null eqs then Arg else Outer
-  parensIfM prec $ fillSeparateTight !commaD $ toList vars ++ toList eqs
+prettyDimEq' vars eqs = do
+  vars' <- prettyDVars' vars
+  eqs'  <- prettyCsts vars eqs
+  parensIfM (dimEqPrec vars (Just eqs)) $
+    fillSeparateTight !commaD $ vars' ++ eqs'
 
 export
 prettyDimEq : {opts : _} -> BContext d -> DimEq d -> Eff Pretty (Doc opts)
 prettyDimEq dnames ZeroIsOne = do
-  vars <- prettyDVars dnames
+  vars <- prettyDVars' dnames
   cst  <- prettyCst [<] (K Zero noLoc) (K One noLoc)
   pure $ separateTight !commaD $ vars :< cst
 prettyDimEq dnames (C eqs) = prettyDimEq' dnames eqs
diff --git a/lib/Quox/Untyped/Syntax.idr b/lib/Quox/Untyped/Syntax.idr
index 62dbbc3..daea0a7 100644
--- a/lib/Quox/Untyped/Syntax.idr
+++ b/lib/Quox/Untyped/Syntax.idr
@@ -144,6 +144,15 @@ parameters {opts : LayoutOpts}
   prettyTerm _ (Erased _) =
     hl Syntax =<< ifUnicode "⌷" "[]"
 
+  export
+  prettyDef : Name -> Definition -> Eff Pretty (Maybe (Doc opts))
+  prettyDef _    ErasedDef     = [|Nothing|]
+  prettyDef name (KeptDef rhs) = map Just $ do
+    name <- prettyFree name
+    eq   <- cstD
+    rhs  <- prettyTerm [<] rhs
+    hangDSingle (name <++> eq) rhs
+
 
 public export
 USubst : Nat -> Nat -> Type