search

epfl-lara / stainless

Verification framework and tool for higher-order Scala programs
https://epfl-lara.github.io/stainless/
Apache License 2.0
357 stars 52 forks source link

Type error in presence of type aliases in `Map` keys #1390

Closed mario-bucev closed 1 year ago

mario-bucev commented 1 year ago

Originally discovered by @agilot. The following snippet:

import stainless.lang._
import stainless.collection._

object Types {
  type I = Int
}

import Types._

case class Foo(bar: Map[I, String])

causes a "type error"

[ Error  ] Type error: this.bar, expected Map[Int, Option[String]],
[ Error  ] found Map[I, Option[String]]
[ Error  ] 
[ Error  ] Typing explanation:
[ Error  ] this.bar is of type Map[I, Option[String]]
[ Error  ]   this is of type Foo
[ Fatal  ] Well-formedness check failed after extraction
[ Error  ] Stainless terminated with an error.
[ Error  ] Debug output is available in the file `stainless-stack-trace.txt`. If the crash is caused by Stainless, you may report your issue on https://github.com/epfl-lara/stainless/issues
[ Error  ] You may use --debug=stack to have the stack trace displayed in the output.