From 8395bec4cbeb28852e7bdc74ade39a2aa9d65e2e Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Fri, 22 Sep 2023 14:03:00 +0200
Subject: [PATCH] check for duplicate cases in enum matches

---
 examples/fail.quox                   |  6 +++---
 lib/Quox/Parser/FromParser.idr       | 24 +++++++++++++-----------
 lib/Quox/Parser/FromParser/Error.idr | 13 +++++++++----
 3 files changed, 25 insertions(+), 18 deletions(-)

diff --git a/examples/fail.quox b/examples/fail.quox
index 7d3ed8a..d879e61 100644
--- a/examples/fail.quox
+++ b/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
diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr
index 53411c7..57bf939 100644
--- a/lib/Quox/Parser/FromParser.idr
+++ b/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
-        pure $ Enum set loc
-      else
-        throw $ DuplicatesInEnum loc strs
+    Enum strs loc => do
+      let set = SortedSet.fromList strs
+      unless (length strs == length (SortedSet.toList set)) $
+        throw $ DuplicatesInEnumType loc strs
+      pure $ Enum set loc
 
     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 ->
diff --git a/lib/Quox/Parser/FromParser/Error.idr b/lib/Quox/Parser/FromParser/Error.idr
index 0803f1f..d561df7 100644
--- a/lib/Quox/Parser/FromParser/Error.idr
+++ b/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"])|]