Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Refinement type not properly freshened #1430

Open
mario-bucev opened this issue Jun 27, 2023 · 0 comments
Open

Refinement type not properly freshened #1430

mario-bucev opened this issue Jun 27, 2023 · 0 comments
Labels

Comments

@mario-bucev
Copy link
Collaborator

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

1 participant