From 19ec6cbc1ab58ca3352f23d505fad00d2ce10ee2 Mon Sep 17 00:00:00 2001
From: Arne Keller <arne.keller@student.kit.edu>
Date: Mon, 26 Jul 2021 10:06:19 +0200
Subject: [PATCH] Increase ID of let inferred type variables

fixes #17
---
 src/main/java/edu/kit/typicalc/model/Tree.java | 10 ++++++++--
 .../java/edu/kit/typicalc/model/TreeTest.java  | 18 ++++++++++++++++--
 2 files changed, 24 insertions(+), 4 deletions(-)

diff --git a/src/main/java/edu/kit/typicalc/model/Tree.java b/src/main/java/edu/kit/typicalc/model/Tree.java
index 3e543eb..0156291 100644
--- a/src/main/java/edu/kit/typicalc/model/Tree.java
+++ b/src/main/java/edu/kit/typicalc/model/Tree.java
@@ -181,8 +181,14 @@ public class Tree implements TermVisitorTree {
                 return new TypeAbstraction(newType, value.getQuantifiedVariables());
             });
 
-            TypeAbstraction newTypeAbstraction = new TypeAbstraction(
-                    typeInfererLet.getType().orElseThrow(IllegalStateException::new), extendedTypeAssumptions);
+            Type letType = typeInfererLet.getType().orElseThrow(IllegalStateException::new);
+            // increase ID of type variables to highlight them separately
+            for (TypeVariable t : letType.getFreeTypeVariables()) {
+                TypeVariable t2 = new TypeVariable(t.getKind(), t.getIndex());
+                t2.setUniqueIndex(t.getUniqueIndex() + 1);
+                letType = letType.substitute(t, t2);
+            }
+            TypeAbstraction newTypeAbstraction = new TypeAbstraction(letType, extendedTypeAssumptions);
             extendedTypeAssumptions.remove(letTerm.getVariable());
             extendedTypeAssumptions.put(letTerm.getVariable(), newTypeAbstraction);
 
diff --git a/src/test/java/edu/kit/typicalc/model/TreeTest.java b/src/test/java/edu/kit/typicalc/model/TreeTest.java
index 8464fda..1b6cad0 100644
--- a/src/test/java/edu/kit/typicalc/model/TreeTest.java
+++ b/src/test/java/edu/kit/typicalc/model/TreeTest.java
@@ -1,5 +1,6 @@
 package edu.kit.typicalc.model;
 
+import edu.kit.typicalc.model.parser.LambdaParser;
 import edu.kit.typicalc.model.step.*;
 import edu.kit.typicalc.model.term.*;
 import edu.kit.typicalc.model.type.*;
@@ -10,8 +11,7 @@ import org.junit.jupiter.api.Test;
 
 import java.util.*;
 
-import static org.junit.jupiter.api.Assertions.assertEquals;
-import static org.junit.jupiter.api.Assertions.assertThrows;
+import static org.junit.jupiter.api.Assertions.*;
 
 class TreeTest {
 
@@ -171,6 +171,20 @@ class TreeTest {
         assertEquals(constraints, tree.getConstraints());
     }
 
+    @Test
+    void derivedLetTypeHasNewUniqueIndex() {
+        var term = "let id = λx.x in id 5";
+        var tree = new Tree(new HashMap<>(), new LambdaParser(term).parse().unwrap());
+        var ls = (LetStep) tree.getFirstInferenceStep();
+        var as = (AbsStepWithLet) ls.getTypeInferer().getFirstInferenceStep();
+        var vs = (VarStep) as.getPremise();
+        var tv = (TypeVariable) vs.getInstantiatedTypeAbs();
+        var as2 = (AppStep) ls.getPremise();
+        var types = as2.getConclusion().getTypeAssumptions().get(new VarTerm("id")).getQuantifiedVariables().toArray(new TypeVariable[0]);
+        assertEquals(1, types.length);
+        assertNotEquals(tv.getUniqueIndex(), types[0].getUniqueIndex());
+    }
+
     @Test
     void equalsTest() {
         EqualsVerifier.forClass(Tree.class).usingGetClass()