examples/fail.quox

@@ -2,9 +2,9 @@
 def missing-b : {a, b} → {a} =
   λ x ⇒ case x return {a} of { 'a ⇒ 'a }
 
--- @[fail "duplicate tags"]
--- def repeat-enum-case : {a} → {a} =
---   λ x ⇒ case x return {a} of { 'a ⇒ 'a; 'a ⇒ 'a }
+@[fail "duplicate arms"]
+def repeat-enum-case : {a} → {a} =
+  λ x ⇒ case x return {a} of { 'a ⇒ 'a; 'a ⇒ 'a }
 
 @[fail "duplicate tags"]
 def repeat-enum-type : {a, a} = 'a

lib/Quox/Parser/FromParser.idr

@@ -181,7 +181,7 @@ mutual
       map E $ CaseEnum (fromPQty pi)
         <$> fromPTermElim ds ns tag
         <*> fromPTermTScope ds ns [< r] ret
-        <*> assert_total fromPTermEnumArms ds ns arms
+        <*> assert_total fromPTermEnumArms loc ds ns arms
         <*> pure loc
 
     Nat loc => pure $ Nat loc
@@ -196,12 +196,11 @@ mutual
         <*> fromPTermTScope ds ns [< s, ih] suc
         <*> pure loc
 
-    Enum strs loc =>
-      let set = SortedSet.fromList strs in
-      if length strs == length (SortedSet.toList set) then
+    Enum strs loc => do
+      let set = SortedSet.fromList strs
+      unless (length strs == length (SortedSet.toList set)) $
+        throw $ DuplicatesInEnumType loc strs
       pure $ Enum set loc
-      else
-        throw $ DuplicatesInEnum loc strs
 
     Tag str loc => pure $ Tag str loc
 
@@ -259,12 +258,15 @@ mutual
         <*> pure loc
 
   private
-  fromPTermEnumArms : Context' PatVar d -> Context' PatVar n ->
+  fromPTermEnumArms : Loc -> Context' PatVar d -> Context' PatVar n ->
                       List (PTagVal, PTerm) ->
                       Eff FromParserPure (CaseEnumArms d n)
-  fromPTermEnumArms ds ns =
-    map SortedMap.fromList .
-    traverse (bitraverse (pure . fromPTagVal) (fromPTermWith ds ns))
+  fromPTermEnumArms loc ds ns arms = do
+    res <- SortedMap.fromList <$>
+           traverse (bitraverse (pure . fromPTagVal) (fromPTermWith ds ns)) arms
+    unless (length (keys res) == length arms) $
+      throw $ DuplicatesInEnumCase loc (map (fromPTagVal . fst) arms)
+    pure res
 
   private
   fromPTermElim : Context' PatVar d -> Context' PatVar n ->

lib/Quox/Parser/FromParser/Error.idr

@@ -22,7 +22,8 @@ ParseError = Parser.Error
 public export
 data Error =
     AnnotationNeeded Loc (NameContexts d n) (Term d n)
-  | DuplicatesInEnum Loc (List TagVal)
+  | DuplicatesInEnumType Loc (List TagVal)
+  | DuplicatesInEnumCase Loc (List TagVal)
   | TermNotInScope Loc Name
   | DimNotInScope Loc PBaseName
   | QtyNotGlobal Loc Qty
@@ -64,19 +65,23 @@ prettyParseError file (ParseError errs) =
     traverse (map ("-" <++>) . prettyParseError1 file) (toList errs)
 
 
-parameters (showContext : Bool)
+parameters {opts : LayoutOpts} (showContext : Bool)
   export
-  prettyError : {opts : _} -> Error -> Eff Pretty (Doc opts)
+  prettyError : Error -> Eff Pretty (Doc opts)
   prettyError (AnnotationNeeded loc ctx tm) =
     [|vappend (prettyLoc loc)
         (hangD "type annotation needed on"
                !(prettyTerm ctx.dnames ctx.tnames tm))|]
     -- [todo] print the original PTerm instead
 
-  prettyError (DuplicatesInEnum loc tags) =
+  prettyError (DuplicatesInEnumType loc tags) =
     [|vappend (prettyLoc loc)
         (hangD "duplicate tags in enum type" !(prettyEnum tags))|]
 
+  prettyError (DuplicatesInEnumCase loc tags) =
+    [|vappend (prettyLoc loc)
+        (hangD "duplicate arms in enum case" !(prettyEnum tags))|]
+
   prettyError (DimNotInScope loc i) =
     [|vappend (prettyLoc loc)
         (pure $ hsep ["dimension", !(hl DVar $ text i), "not in scope"])|]