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/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,