-
Notifications
You must be signed in to change notification settings - Fork 48
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
Fatal error: Well-formedness check failed after extraction #1416
Comments
@vkuncak @mario-bucev where would be a good place to add the full example? Bolts? Benchmarks? |
It seems to stem from the compiler inferring something else than extension (l: List[Int])
def mapTr(f: Int => Int, acc: List[Int]): List[Int] =
l match
case Nil() => acc
case Cons(x, xs) => xs.mapTr(f, acc ++ (f(x) :: Nil[Int]()))
def MapEqMapTr(l: List[Int], f: Int => Int): Boolean = {
( Nil[Int]().map(f) == Nil[Int]().mapTr(f, Nil[Int]()) ) because {
Nil[Int]().map(f) ==| trivial |
Nil[Int]() ==| trivial |
Nil[Int]().mapTr(f, Nil[Int]())
}.qed
}.holds which we could add in |
@mario-bucev Scala compiler inferring what it does, can Stainless give a better error message? |
That would be neat however I do not see how we could proceed: should we emit a warning when we encounter any |
The following (minimized) example:
results in the following error message:
The text was updated successfully, but these errors were encountered: