From ea380fa25aa50cd8928445aa9693a4c48ac28e1c Mon Sep 17 00:00:00 2001
From: Jad Hamza <jad.hamza@epfl.ch>
Date: Wed, 24 Feb 2021 15:58:02 +0100
Subject: [PATCH] Avoid occurrences of the same variable with different types

---
 .../scala/stainless/verification/TypeChecker.scala     |  7 +++++--
 .../stainless/verification/TypeCheckerUtils.scala      | 10 +++++-----
 2 files changed, 10 insertions(+), 7 deletions(-)

diff --git a/core/src/main/scala/stainless/verification/TypeChecker.scala b/core/src/main/scala/stainless/verification/TypeChecker.scala
index a50afc8f95..1443930408 100644
--- a/core/src/main/scala/stainless/verification/TypeChecker.scala
+++ b/core/src/main/scala/stainless/verification/TypeChecker.scala
@@ -950,7 +950,7 @@ trait TypeChecker {
         case Truth(t) =>
           implies(t, acc)
         case RefinementType(vd, pred) =>
-          implies(renameVar(pred, vd.id, v.id), acc)
+          implies(substVar(pred, vd.id, v), acc)
         case _ =>
           acc
       }
@@ -1144,7 +1144,10 @@ trait TypeChecker {
         tr ++ isSubtype(tc2, freshener.transform(to1), freshener.transform(to2))
 
       case (RefinementType(vd1, prop1), RefinementType(vd2, prop2)) if (vd1.tpe == vd2.tpe) =>
-        buildVC(tc.bind(vd1).withTruth(prop1).withVCKind(VCKind.RefinementSubtype), renameVar(prop2, vd2.id, vd1.id))
+        buildVC(
+          tc.bind(vd1).withTruth(prop1).withVCKind(VCKind.RefinementSubtype),
+          substVar(prop2, vd2.id, vd1.toVariable)
+        )
 
       case (_, RefinementType(vd, prop)) =>
         isSubtype(tc, tp1, vd.tpe) ++ buildVC(tc.withVCKind(VCKind.RefinementSubtype), prop)
diff --git a/core/src/main/scala/stainless/verification/TypeCheckerUtils.scala b/core/src/main/scala/stainless/verification/TypeCheckerUtils.scala
index 1dccd137e3..7ed547204b 100644
--- a/core/src/main/scala/stainless/verification/TypeCheckerUtils.scala
+++ b/core/src/main/scala/stainless/verification/TypeCheckerUtils.scala
@@ -71,13 +71,13 @@ object TypeCheckerUtils {
     def unapply(v: Variable): Option[(Variable, Expr)] = unapply(v.tpe)
   }
 
-  def renameVar(e: Expr, id1: Identifier, id2: Identifier): Expr = {
+  def substVar(expr: Expr, id: Identifier, replacement: Expr): Expr = {
     new SelfTreeTransformer {
       override def transform(e: Expr) = e match {
-        case Variable(id, tpe, flags) if id == id1 => Variable(id2, transform(tpe), flags.map(transform))
+        case Variable(id2, _, _) if id2 == id => replacement
         case _ => super.transform(e)
       }
-    }.transform(e)
+    }.transform(expr)
   }
 
   // TODO: implement ite for more types (PiType, SigmaType, etc.)
@@ -87,8 +87,8 @@ object TypeCheckerUtils {
     case (RefinementType(vd1, prop1), RefinementType(vd2, prop2)) =>
       val newType = ite(b, vd1.tpe, vd2.tpe)
       val vd = ValDef.fresh(vd1.id.name, newType)
-      val newProp1 = renameVar(prop1, vd1.id, vd.id)
-      val newProp2 = renameVar(prop2, vd2.id, vd.id)
+      val newProp1 = substVar(prop1, vd1.id, vd.toVariable)
+      val newProp2 = substVar(prop2, vd2.id, vd.toVariable)
       RefinementType(vd, IfExpr(b, newProp1, newProp2))
 
     case (RefinementType(vd1, prop1), _) if (vd1.tpe == t2) =>