Fatal error: Well-formedness check failed after extraction

[drganam]

The following (minimized) example:

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

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()))

def MapEqMapTr(l: List[Int], f: Int => Int): Boolean = {
  ( Nil().map(f) == Nil().mapTr(f, Nil()) ) because {
    Nil().map(f)                    ==|  trivial                    |
    Nil()                           ==|  trivial                    |
    Nil().mapTr(f, Nil())
  }.qed
}.holds

results in the following error message:

[ Error  ]   boolean2ProofOps(Nil[Int]().map[Int](f) == mapTr(Nil[Int](), f, Nil[Int]())).because(any2RelReasoning[List[_ >: Int <: Any]](Nil[Int]().map[Int](f)).==|(trivial).|[List[_ >: Int <: Any]](any2RelReasoning[List[_ >: Int <: Any]](Nil[Any]()).==|(trivial)).|(any2RelReasoning[List[_ >: Int <: Any]](mapTr(Nil[Int](), f, Nil[Int]()))).qed)
[ Error  ] } ensuring {
[ Error  ]   (holds: Boolean) => holds
[ Error  ] }, expected Boolean,
[ Error  ] found <untyped>
[ Error  ] 
[ Error  ] Typing explanation:
[ Error  ] {
[ Error  ]   boolean2ProofOps(Nil[Int]().map[Int](f) == mapTr(Nil[Int](), f, Nil[Int]())).because(any2RelReasoning[List[_ >: Int <: Any]](Nil[Int]().map[Int](f)).==|(trivial).|[List[_ >: Int <: Any]](any2RelReasoning[List[_ >: Int <: Any]](Nil[Any]()).==|(trivial)).|(any2RelReasoning[List[_ >: Int <: Any]](mapTr(Nil[Int](), f, Nil[Int]()))).qed)
[ Error  ] } ensuring {
[ Error  ]   (holds: Boolean) => holds
[ Error  ] } is of type <untyped>
[ Error  ]   boolean2ProofOps(Nil[Int]().map[Int](f) == mapTr(Nil[Int](), f, Nil[Int]())).because(any2RelReasoning[List[_ >: Int <: Any]](Nil[Int]().map[Int](f)).==|(trivial).|[List[_ >: Int <: Any]](any2RelReasoning[List[_ >: Int <: Any]](Nil[Any]()).==|(trivial)).|(any2RelReasoning[List[_ >: Int <: Any]](mapTr(Nil[Int](), f, Nil[Int]()))).qed) is of type <untyped>
[ Error  ]     boolean2ProofOps(Nil[Int]().map[Int](f) == mapTr(Nil[Int](), f, Nil[Int]())) is of type ProofOps
[ Error  ]       Nil[Int]().map[Int](f) == mapTr(Nil[Int](), f, Nil[Int]()) is of type Boolean
[ Error  ]         Nil[Int]().map[Int](f) is of type List[Int]
[ Error  ]           Nil[Int]() is of type Nil[Int]
[ Error  ]           f is of type (Int) => Int
[ Error  ]         mapTr(Nil[Int](), f, Nil[Int]()) is of type List[Int]
[ Error  ]           Nil[Int]() is of type Nil[Int]
[ Error  ]           f is of type (Int) => Int
[ Error  ]           Nil[Int]() is of type Nil[Int] because mapTr was instantiated with  with type (List[Int],(Int) => Int,List[Int]) => List[Int] because boolean2ProofOps was instantiated with  with type (Boolean) => ProofOps
[ Error  ]     any2RelReasoning[List[_ >: Int <: Any]](Nil[Int]().map[Int](f)).==|(trivial).|[List[_ >: Int <: Any]](any2RelReasoning[List[_ >: Int <: Any]](Nil[Any]()).==|(trivial)).|(any2RelReasoning[List[_ >: Int <: Any]](mapTr(Nil[Int](), f, Nil[Int]()))).qed is of type <untyped>
[ Error  ]       any2RelReasoning[List[_ >: Int <: Any]](Nil[Int]().map[Int](f)).==|(trivial).|[List[_ >: Int <: Any]](any2RelReasoning[List[_ >: Int <: Any]](Nil[Any]()).==|(trivial)).|(any2RelReasoning[List[_ >: Int <: Any]](mapTr(Nil[Int](), f, Nil[Int]()))) is of type <untyped>
[ Error  ]         any2RelReasoning[List[_ >: Int <: Any]](Nil[Int]().map[Int](f)).==|(trivial).|[List[_ >: Int <: Any]](any2RelReasoning[List[_ >: Int <: Any]](Nil[Any]()).==|(trivial)) is of type <untyped>
[ Error  ]           any2RelReasoning[List[_ >: Int <: Any]](Nil[Int]().map[Int](f)).==|(trivial) is of type <untyped>
[ Error  ]             any2RelReasoning[List[_ >: Int <: Any]](Nil[Int]().map[Int](f)) is of type <untyped>
[ Error  ]               Nil[Int]().map[Int](f) is of type List[Int]
[ Error  ]                 Nil[Int]() is of type Nil[Int]
[ Error  ]                 f is of type (Int) => Int because any2RelReasoning was instantiated with A:=List[_ >: Int <: Any] with type (A) => RelReasoning[A]
[ Error  ]             trivial is of type Boolean because trivial was instantiated with  with type () => Boolean
[ Error  ]           any2RelReasoning[List[_ >: Int <: Any]](Nil[Any]()).==|(trivial) is of type <untyped>
[ Error  ]             any2RelReasoning[List[_ >: Int <: Any]](Nil[Any]()) is of type <untyped>
[ Error  ]               Nil[Any]() is of type Nil[Any] because any2RelReasoning was instantiated with A:=List[_ >: Int <: Any] with type (A) => RelReasoning[A]
[ Error  ]             trivial is of type Boolean because trivial was instantiated with  with type () => Boolean
[ Error  ]         any2RelReasoning[List[_ >: Int <: Any]](mapTr(Nil[Int](), f, Nil[Int]())) is of type <untyped>
[ Error  ]           mapTr(Nil[Int](), f, Nil[Int]()) is of type List[Int]
[ Error  ]             Nil[Int]() is of type Nil[Int]
[ Error  ]             f is of type (Int) => Int
[ Error  ]             Nil[Int]() is of type Nil[Int] because mapTr was instantiated with  with type (List[Int],(Int) => Int,List[Int]) => List[Int] because any2RelReasoning was instantiated with A:=List[_ >: Int <: Any] with type (A) => RelReasoning[A]
[ Error  ]   (holds: Boolean) => holds is of type (Boolean) => Boolean
[ Error  ]     holds is of type Boolean
           def MapEqMapTr(l: List[Int], f: Int => Int): Boolean = {
                                                                  ^...
[ Fatal  ] Well-formedness check failed after extraction

[drganam]

@vkuncak @mario-bucev where would be a good place to add the full example? Bolts? Benchmarks?

[mario-bucev]

It seems to stem from the compiler inferring something else than List[Int] for the expression Nil(). The following adaptation works:

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 verification/valid

[drganam]

https://github.com/epfl-lara/stainless/pull/1421

[vkuncak]

@mario-bucev Scala compiler inferring what it does, can Stainless give a better error message?

[mario-bucev]

That would be neat however I do not see how we could proceed: should we emit a warning when we encounter any Any or bounds inferred type? We could even error in such instances but that may invalidate the few legitimate cases there are. If, however, the Scala compiler has the information on whether a type was inferred or not, I think ruling out such cases would be a fair trade