Refinement type not properly freshened
mario-bucev opened this issue · 0 comments
mario-bucev commented
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
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.