Type error after type encoding with Nil()

[jad-hamza]

A type error happens after the type encoding phase on this example. (Workaround: write Nil[T]() instead of Nil()).

import stainless.collection._
import stainless.annotation._

object TypeEncodingNil {
  @extern
  def f[T](l: List[T], p: T => Boolean) : Unit = {
  }.ensuring(_ => l.dropWhile(p) == Nil())
}

Here's part of the debug output:

[ Debug  ] Symbols before TypeEncoding
[ Debug  ] 
[ Debug  ] -------------Functions-------------
[ Debug  ] @extern
[ Debug  ] def f[T](l: List[T], p: (T) => Boolean): Unit = {
[ Debug  ]   <empty tree>[Unit]
[ Debug  ] } ensuring {
[ Debug  ]   (x$1: Unit) => dropWhile[T](l, p) == Nil[Nothing]()
[ Debug  ] }
[ Debug  ] 
[ Debug  ] 
[ Debug  ] 
[ Debug  ] 
[ Debug  ] Symbols after TypeEncoding
[ Debug  ] 
[ Debug  ] -------------Functions-------------
[ Debug  ] @extern
[ Debug  ] def f[T](l: List[T], p: (T) => Boolean): Unit = {
[ Debug  ]   <empty tree>[Unit]
[ Debug  ] } ensuring {
[ Debug  ]   (x$1: Unit) => List(asList[T, Object](dropWhile[T](l, p), (x: T) => x, (x: Object) => x)) == List(asList[{ x: Object | @unchecked false }, Object](Nil[{ x: Object | @unchecked false }](), (x: { x: Object | @unchecked false }) => x, (x: Object) => x))
[ Debug  ] }
[ Debug  ] 
[ Debug  ] 
[ Debug  ] 
[ Debug  ] 
[ Debug  ] 
[ Debug  ] Ensuring well-formedness after phase TypeEncoding...
[ Error  ] lab2.scala:6:50: Type error: {
[ Error  ]   <empty tree>[Unit]
[ Error  ] } ensuring {
[ Error  ]   (x$1: Unit) => List(asList[T, Object](dropWhile[T](l, p), (x: T) => x, (x: Object) => x)) == List(asList[{ x: Object | @unchecked false }, Object](Nil[{ x: Object | @unchecked false }](), (x: { x: Object | @unchecked false }) => x, (x: Object) => x))
[ Error  ] }, expected Unit, 
[ Error  ] found <untyped>
[ Error  ] 
[ Error  ] Typing explanation:
[ Error  ] {
[ Error  ]   <empty tree>[Unit]
[ Error  ] } ensuring {
[ Error  ]   (x$1: Unit) => List(asList[T, Object](dropWhile[T](l, p), (x: T) => x, (x: Object) => x)) == List(asList[{ x: Object | @unchecked false }, Object](Nil[{ x: Object | @unchecked false }](), (x: { x: Object | @unchecked false }) => x, (x: Object) => x))
[ Error  ] } is of type <untyped>
[ Error  ]   <empty tree>[Unit] is of type Unit
[ Error  ]   (x$1: Unit) => List(asList[T, Object](dropWhile[T](l, p), (x: T) => x, (x: Object) => x)) == List(asList[{ x: Object | @unchecked false }, Object](Nil[{ x: Object | @unchecked false }](), (x: { x: Object | @unchecked false }) => x, (x: Object) => x)) is of type <untyped>
[ Error  ]     List(asList[T, Object](dropWhile[T](l, p), (x: T) => x, (x: Object) => x)) == List(asList[{ x: Object | @unchecked false }, Object](Nil[{ x: Object | @unchecked false }](), (x: { x: Object | @unchecked false }) => x, (x: Object) => x)) is of type <untyped>
[ Error  ]       List(asList[T, Object](dropWhile[T](l, p), (x: T) => x, (x: Object) => x)) is of type <untyped>
[ Error  ]         asList[T, Object](dropWhile[T](l, p), (x: T) => x, (x: Object) => x) is of type <untyped>
[ Error  ]           dropWhile[T](l, p) is of type List[T]
[ Error  ]             l is of type List[T]
[ Error  ]             p is of type (T) => Boolean because dropWhile was instantiated with T:=T with type (List[T],(T) => Boolean) => List[T]
[ Error  ]           (x: T) => x is of type (T) => T
[ Error  ]             x is of type T
[ Error  ]           (x: Object) => x is of type (Object) => Object
[ Error  ]             x is of type Object because asList was instantiated with T:=T,T:=Object with type (List[T],(T) => T,(T) => T) => List[T] because List was instantiated with  with fields (List[Object])
[ Error  ]       List(asList[{ x: Object | @unchecked false }, Object](Nil[{ x: Object | @unchecked false }](), (x: { x: Object | @unchecked false }) => x, (x: Object) => x)) is of type Object
[ Error  ]         asList[{ x: Object | @unchecked false }, Object](Nil[{ x: Object | @unchecked false }](), (x: { x: Object | @unchecked false }) => x, (x: Object) => x) is of type List[Object]
[ Error  ]           Nil[{ x: Object | @unchecked false }]() is of type List[Object] because Nil was instantiated with T:={ x: Object | @unchecked false } with fields ()
[ Error  ]           (x: { x: Object | @unchecked false }) => x is of type (Object) => Object
[ Error  ]             x is of type Object
[ Error  ]           (x: Object) => x is of type (Object) => Object
[ Error  ]             x is of type Object because asList was instantiated with T:={ x: Object | @unchecked false },T:=Object with type (List[T],(T) => T,(T) => T) => List[T] because List was instantiated with  with fields (List[Object])
             def f[T](l: List[T], p: T => Boolean) : Unit = {
                                                            ^...
[ Fatal  ] Well-formedness check failed after phase TypeEncoding

[samarion]

I believe the type encoding should be erasing the type parameter T in f here.

The most likely culprit is missing cases in the check which determines whether a type parameter will need to be erased or not. Maybe try adding an extra case like

case e if tpe == s.AnyType() =>
  simple --= s.typeOps.typeParamsOf(e.getType)
  super.transform(e, tpe)

[jad-hamza]

Thanks for the suggestion! Unfortunately, that didn't seem to help (same error)

[ Debug  ] Symbols after TypeEncoding
[ Debug  ] 
[ Debug  ] -------------Functions-------------
[ Debug  ] @extern
[ Debug  ] def f[T](l: List[T], p: (T) => Boolean): Unit = {
[ Debug  ]   <empty tree>[Unit]
[ Debug  ] } ensuring {
[ Debug  ]   (x$1: Unit) => List(asList[T, Object](dropWhile[T](l, p), (x: T) => x, (x: Object) => x)) == List(asList[{ x: Object | @unchecked false }, Object](Nil[{ x: Object | @unchecked false }](), (x: { x: Object | @unchecked false }) => x, (x: Object) => x))
[ Debug  ] }

[vkuncak]

I can no longer reproduce this. It is accepted by stainless-scalac and (more correctly) rejected by stainless-dotty.