From d11605ab1e8b636d9e3e013587c1c5407818f62c Mon Sep 17 00:00:00 2001
From: Jonathan Cubides <jonathan.cubides@uib.no>
Date: Fri, 15 Jul 2022 10:58:49 +0200
Subject: [PATCH] Check all the type parameter names are different when
 declaring an inductive type (#1377)

* Fix #1334

* Rename error type
---
 src/Juvix/Syntax/Concrete/Scoped/Error.hs     |  2 ++
 .../Syntax/Concrete/Scoped/Error/Types.hs     | 24 ++++++++++++++
 src/Juvix/Syntax/Concrete/Scoped/Scoper.hs    | 33 +++++++++++--------
 test/Scope/Negative.hs                        |  7 ++++
 .../DuplicateInductiveParameterName.juvix     |  5 +++
 5 files changed, 58 insertions(+), 13 deletions(-)
 create mode 100644 tests/negative/DuplicateInductiveParameterName.juvix

diff --git a/src/Juvix/Syntax/Concrete/Scoped/Error.hs b/src/Juvix/Syntax/Concrete/Scoped/Error.hs
index 5da8ab007..80db0b085 100644
--- a/src/Juvix/Syntax/Concrete/Scoped/Error.hs
+++ b/src/Juvix/Syntax/Concrete/Scoped/Error.hs
@@ -32,6 +32,7 @@ data ScoperError
   | ErrMultipleCompileBlockSameName MultipleCompileBlockSameName
   | ErrMultipleCompileRuleSameBackend MultipleCompileRuleSameBackend
   | ErrWrongKindExpressionCompileBlock WrongKindExpressionCompileBlock
+  | ErrDuplicateInductiveParameterName DuplicateInductiveParameterName
   deriving stock (Show)
 
 instance ToGenericError ScoperError where
@@ -58,3 +59,4 @@ instance ToGenericError ScoperError where
     ErrMultipleCompileBlockSameName e -> genericError e
     ErrMultipleCompileRuleSameBackend e -> genericError e
     ErrWrongKindExpressionCompileBlock e -> genericError e
+    ErrDuplicateInductiveParameterName e -> genericError e
diff --git a/src/Juvix/Syntax/Concrete/Scoped/Error/Types.hs b/src/Juvix/Syntax/Concrete/Scoped/Error/Types.hs
index 5ca9392a7..0a3439ec8 100644
--- a/src/Juvix/Syntax/Concrete/Scoped/Error/Types.hs
+++ b/src/Juvix/Syntax/Concrete/Scoped/Error/Types.hs
@@ -522,3 +522,27 @@ ambiguousMessage n es =
       <> "It could be any of:"
       <> line
       <> indent' (vsep (map ppCode es))
+
+newtype DuplicateInductiveParameterName = DuplicateInductiveParameterName
+  { _duplicateInductiveParameterName :: Symbol
+  }
+  deriving stock (Show)
+
+makeLenses ''DuplicateInductiveParameterName
+
+instance ToGenericError DuplicateInductiveParameterName where
+  genericError e =
+    GenericError
+      { _genericErrorLoc = i,
+        _genericErrorMessage = prettyError msg,
+        _genericErrorIntervals = [i]
+      }
+    where
+      param = e ^. duplicateInductiveParameterName
+      i = getLoc param
+      msg =
+        "Invalid name"
+          <+> ppCode param
+            <> "."
+            <> line
+            <> "Inductive parameter names can not be repeated."
diff --git a/src/Juvix/Syntax/Concrete/Scoped/Scoper.hs b/src/Juvix/Syntax/Concrete/Scoped/Scoper.hs
index d0f3d2705..8268cde27 100644
--- a/src/Juvix/Syntax/Concrete/Scoped/Scoper.hs
+++ b/src/Juvix/Syntax/Concrete/Scoped/Scoper.hs
@@ -429,24 +429,31 @@ withParams ::
   [InductiveParameter 'Parsed] ->
   ([InductiveParameter 'Scoped] -> Sem r a) ->
   Sem r a
-withParams xs a = go [] xs
+withParams xs a = go [] [] xs
   where
-    go :: [InductiveParameter 'Scoped] -> [InductiveParameter 'Parsed] -> Sem r a
-    go inductiveParameters' params =
+    go :: [InductiveParameter 'Scoped] -> [Symbol] -> [InductiveParameter 'Parsed] -> Sem r a
+    go inductiveParameters' usedNames params =
       case params of
+        -- All params have been checked
+        [] -> a inductiveParameters'
         -- More params to check
         (InductiveParameter {..} : ps) -> do
           inductiveParameterType' <- checkParseExpressionAtoms _inductiveParameterType
-          inductiveParameterName' <- freshVariable _inductiveParameterName
-          let param' =
-                InductiveParameter
-                  { _inductiveParameterType = inductiveParameterType',
-                    _inductiveParameterName = inductiveParameterName'
-                  }
-          withBindLocalVariable (LocalVariable inductiveParameterName') $
-            go (inductiveParameters' ++ [param']) ps
-        -- All params have been checked
-        [] -> a inductiveParameters'
+          if
+              | _inductiveParameterName `elem` usedNames ->
+                  throw
+                    ( ErrDuplicateInductiveParameterName
+                        (DuplicateInductiveParameterName _inductiveParameterName)
+                    )
+              | otherwise -> do
+                  inductiveParameterName' <- freshVariable _inductiveParameterName
+                  let param' =
+                        InductiveParameter
+                          { _inductiveParameterType = inductiveParameterType',
+                            _inductiveParameterName = inductiveParameterName'
+                          }
+                  withBindLocalVariable (LocalVariable inductiveParameterName') $
+                    go (inductiveParameters' ++ [param']) (_inductiveParameterName : usedNames) ps
 
 checkInductiveDef ::
   forall r.
diff --git a/test/Scope/Negative.hs b/test/Scope/Negative.hs
index e108293d9..405fbec15 100644
--- a/test/Scope/Negative.hs
+++ b/test/Scope/Negative.hs
@@ -211,6 +211,13 @@ scoperErrorTests =
       "WrongKindExpressionCompileBlock.juvix"
       $ \case
         ErrWrongKindExpressionCompileBlock {} -> Nothing
+        _ -> wrongError,
+    NegTest
+      "A type parameter name occurs twice when declaring an inductive type"
+      "."
+      "DuplicateInductiveParameterName.juvix"
+      $ \case
+        ErrDuplicateInductiveParameterName {} -> Nothing
         _ -> wrongError
   ]
 
diff --git a/tests/negative/DuplicateInductiveParameterName.juvix b/tests/negative/DuplicateInductiveParameterName.juvix
new file mode 100644
index 000000000..a84c418c4
--- /dev/null
+++ b/tests/negative/DuplicateInductiveParameterName.juvix
@@ -0,0 +1,5 @@
+module DuplicateInductiveParameterName;
+
+inductive T (A : Type) (B : Type) (A : Type) {};
+
+end;
\ No newline at end of file