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

@@ -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

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."

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.

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
   ]
 

tests/negative/DuplicateInductiveParameterName.juvix

@@ -0,0 +1,5 @@
+module DuplicateInductiveParameterName;
+
+inductive T (A : Type) (B : Type) (A : Type) {};
+
+end;