Refinement type not properly freshened

Originally discovered by @agilot

The following cause a crash in TypeChecker:

import stainless.covcollection._

object Bug {
  case class Set[T]() {
    def funTrue: T => Boolean = t => true
  }

  def foo[T](l: List[T]): Set[T] = Set[T]()

  def bug[T](l: List[T], n: T): Unit = {
    require(foo[T](l).funTrue(n))
  }
}

with the following message:

inox.package$FatalError: Typing context already contains variable x$205
        at inox.package$FatalError$.apply(package.scala:24)
        at inox.Reporter.onFatal(Reporter.scala:47)
        at inox.Reporter.internalError(Reporter.scala:63)
        at inox.Reporter.internalError(Reporter.scala:115)
        at stainless.verification.TypeCheckerContext$TypingContext.checkFreshTermVariable(TypeCheckerContext.scala:33)
...

The problem stems from a refinement type not being properly freshened. The first time it happens (without causing a crash) is in https://github.com/epfl-lara/stainless/blob/9fbc579493e74048377c29e620b945bb5da8961e/core/src/main/scala/stainless/verification/TypeChecker.scala#L743 This returns the following typed definition:

typed def funTrue$0[{ x$161: Object$0 | (T$120(x$161)): @dropConjunct  }]: ({ x$161: Object$0 | (T$120(x$161)): @dropConjunct  }) => Boolean

We can see that x$161 is declared twice (which gets replaced by x$205 later on and ultimately causing the error). It seems that the TypeInstantiator should freshen the instantiated type.

epfl-lara / stainless

Refinement type not properly freshened #1430