From 394b5a3d23c7afa0878222278f52cc9da5f6567f Mon Sep 17 00:00:00 2001
From: Arne Keller <arne.keller@student.kit.edu>
Date: Fri, 9 Jul 2021 12:26:18 +0200
Subject: [PATCH] Reject duplicate quantified type variables

---
 .../typicalc/model/parser/TypeAssumptionParser.java   |  7 ++++++-
 .../model/parser/TypeAssumptionParserTest.java        | 11 +++++++++++
 2 files changed, 17 insertions(+), 1 deletion(-)

diff --git a/src/main/java/edu/kit/typicalc/model/parser/TypeAssumptionParser.java b/src/main/java/edu/kit/typicalc/model/parser/TypeAssumptionParser.java
index b9ff37d..7e30cf8 100644
--- a/src/main/java/edu/kit/typicalc/model/parser/TypeAssumptionParser.java
+++ b/src/main/java/edu/kit/typicalc/model/parser/TypeAssumptionParser.java
@@ -441,7 +441,12 @@ public class TypeAssumptionParser {
                                 .withToken(t, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
                     }
                     int i = Integer.parseInt(input.substring(1));
-                    variables.add(new TypeVariable(TypeVariableKind.USER_INPUT, i));
+                    TypeVariable variable = new TypeVariable(TypeVariableKind.USER_INPUT, i);
+                    if (variables.contains(variable)) {
+                        return new ParserResult<>(ParseError.UNEXPECTED_TOKEN
+                                .withToken(t, ParseError.ErrorType.TYPE_ASSUMPTION_ERROR));
+                    }
+                    variables.add(variable);
                     expectCommaOrDot = true;
                     return new ParserResult<>(this);
                 case COMMA:
diff --git a/src/test/java/edu/kit/typicalc/model/parser/TypeAssumptionParserTest.java b/src/test/java/edu/kit/typicalc/model/parser/TypeAssumptionParserTest.java
index ac37554..9cc99b5 100644
--- a/src/test/java/edu/kit/typicalc/model/parser/TypeAssumptionParserTest.java
+++ b/src/test/java/edu/kit/typicalc/model/parser/TypeAssumptionParserTest.java
@@ -228,6 +228,17 @@ class TypeAssumptionParserTest {
         assertTrue(expected.contains(Token.TokenType.COMMA));
     }
 
+    @Test
+    void doesntAcceptDuplicateQuantifiedVariables() {
+        TypeAssumptionParser parser = new TypeAssumptionParser();
+        Result<Map<VarTerm, TypeAbstraction>, ParseError> type = parser.parse("id: ∀ t1, t1 : t1 -> t1");
+        assertTrue(type.isError());
+        ParseError error = type.unwrapError();
+        assertEquals(ParseError.UNEXPECTED_TOKEN, error);
+        assertEquals(Token.TokenType.VARIABLE, error.getCause().get().getType());
+        assertEquals(10, error.getCause().get().getPos());
+    }
+
     @Test
     void errors() {
         Map<String, ParseError> tests = new HashMap<>();