Type encoding issue with equality between different types

[jad-hamza]

This example uses an equality between different types, and type encoding introduces a type error:

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

object TypeEncodingEquality {
  case class P[A](p: List[BigInt] => Option[(A, List[BigInt])]) {
    def flatMap[B](f: A => P[B]): P[B] = P(ts => p(ts).flatMap {
      case (x, rs) => f(x).p(rs)
    })
  }

  def test[A, B](m: P[A], f: A => P[B], ts: List[BigInt]): Unit = {
    assert(m.p(ts) == m.flatMap(f))
  }
}

Some debug output:

[ Debug  ] Symbols before TypeEncoding
[ Debug  ] 
[ Debug  ] -------------Functions-------------
[ Debug  ] def test[A, B](m: P[A], f: (A) => P[B], ts: List[BigInt]): Unit = {
[ Debug  ]   assert(m.p(ts) == flatMap[A, B](m, f))
[ Debug  ]   ()
[ Debug  ] }
[ Debug  ] 
[ Debug  ] 
[ Debug  ] 
[ Debug  ] 
[ Debug  ] Symbols after TypeEncoding
[ Debug  ] 
[ Debug  ] -------------Functions-------------
[ Debug  ] def test[A, B](m: P[A], f: (A) => P[B], ts: List[BigInt]): Unit = {
[ Debug  ]   assert(Option(asOption[(A, List[BigInt]), Object](m.p(ts), (x: (A, List[BigInt])) => Tuple2((x._1, List(asList[BigInt, Object](x._2, (x: BigInt) => Integer(x), (x: Object) => @unchecked x.value)))), (x: Object) => (@unchecked x.value._1, asList[Object, BigInt]({
[ Debug  ]     val x: Object = @unchecked x.value._2
[ Debug  ]     @unchecked x.value
[ Debug  ]   }, (x: Object) => @unchecked x.value, (x: BigInt) => Integer(x))))) == P(asP[B, Object](flatMap[A, B](m, f), (x: B) => x, (x: Object) => x)))
[ Debug  ]   ()
[ Debug  ] }
[ Debug  ] 
[ Debug  ] 
[ Debug  ] 
[ Debug  ] 
[ Debug  ] 
[ Debug  ] Ensuring well-formedness after phase TypeEncoding...
[ Error  ] Tokenizer.scala:12:5: Type error: assert(Option(asOption[(A, List[BigInt]), Object](m.p(ts), (x: (A, List[BigInt])) => Tuple2((x._1, List(asList[BigInt, Object](x._2, (x: BigInt) => Integer(x), (x: Object) => @unchecked x.value)))), (x: Object) => (@unchecked x.value._1, asList[Object, BigInt]({
[ Error  ]   val x: Object = @unchecked x.value._2
[ Error  ]   @unchecked x.value
[ Error  ] }, (x: Object) => @unchecked x.value, (x: BigInt) => Integer(x))))) == P(asP[B, Object](flatMap[A, B](m, f), (x: B) => x, (x: Object) => x)))
[ Error  ] (), expected Unit, 
[ Error  ] found <untyped>
[ Error  ] 
[ Error  ] Typing explanation:
[ Error  ] assert(Option(asOption[(A, List[BigInt]), Object](m.p(ts), (x: (A, List[BigInt])) => Tuple2((x._1, List(asList[BigInt, Object](x._2, (x: BigInt) => Integer(x), (x: Object) => @unchecked x.value)))), (x: Object) => (@unchecked x.value._1, asList[Object, BigInt]({
[ Error  ]   val x: Object = @unchecked x.value._2
[ Error  ]   @unchecked x.value
[ Error  ] }, (x: Object) => @unchecked x.value, (x: BigInt) => Integer(x))))) == P(asP[B, Object](flatMap[A, B](m, f), (x: B) => x, (x: Object) => x)))
[ Error  ] () is of type <untyped>
[ Error  ]   Option(asOption[(A, List[BigInt]), Object](m.p(ts), (x: (A, List[BigInt])) => Tuple2((x._1, List(asList[BigInt, Object](x._2, (x: BigInt) => Integer(x), (x: Object) => @unchecked x.value)))), (x: Object) => (@unchecked x.value._1, asList[Object, BigInt]({
[ Error  ]     val x: Object = @unchecked x.value._2
[ Error  ]     @unchecked x.value
[ Error  ]   }, (x: Object) => @unchecked x.value, (x: BigInt) => Integer(x))))) == P(asP[B, Object](flatMap[A, B](m, f), (x: B) => x, (x: Object) => x)) is of type <untyped>
[ Error  ]     Option(asOption[(A, List[BigInt]), Object](m.p(ts), (x: (A, List[BigInt])) => Tuple2((x._1, List(asList[BigInt, Object](x._2, (x: BigInt) => Integer(x), (x: Object) => @unchecked x.value)))), (x: Object) => (@unchecked x.value._1, asList[Object, BigInt]({
[ Error  ]       val x: Object = @unchecked x.value._2
[ Error  ]       @unchecked x.value
[ Error  ]     }, (x: Object) => @unchecked x.value, (x: BigInt) => Integer(x))))) is of type <untyped>
[ Error  ]       asOption[(A, List[BigInt]), Object](m.p(ts), (x: (A, List[BigInt])) => Tuple2((x._1, List(asList[BigInt, Object](x._2, (x: BigInt) => Integer(x), (x: Object) => @unchecked x.value)))), (x: Object) => (@unchecked x.value._1, asList[Object, BigInt]({
[ Error  ]         val x: Object = @unchecked x.value._2
[ Error  ]         @unchecked x.value
[ Error  ]       }, (x: Object) => @unchecked x.value, (x: BigInt) => Integer(x)))) is of type <untyped>
[ Error  ]         m.p(ts) is of type Option[(A, List[BigInt])]
[ Error  ]           m.p is of type (List[BigInt]) => Option[(A, List[BigInt])]
[ Error  ]             m is of type P[A]
[ Error  ]           ts is of type List[BigInt]
[ Error  ]         (x: (A, List[BigInt])) => Tuple2((x._1, List(asList[BigInt, Object](x._2, (x: BigInt) => Integer(x), (x: Object) => @unchecked x.value)))) is of type <untyped>
[ Error  ]           Tuple2((x._1, List(asList[BigInt, Object](x._2, (x: BigInt) => Integer(x), (x: Object) => @unchecked x.value)))) is of type <untyped>
[ Error  ]             (x._1, List(asList[BigInt, Object](x._2, (x: BigInt) => Integer(x), (x: Object) => @unchecked x.value))) is of type (A, Object)
[ Error  ]               x._1 is of type A
[ Error  ]                 x is of type (A, List[BigInt])
[ Error  ]               List(asList[BigInt, Object](x._2, (x: BigInt) => Integer(x), (x: Object) => @unchecked x.value)) is of type Object
[ Error  ]                 asList[BigInt, Object](x._2, (x: BigInt) => Integer(x), (x: Object) => @unchecked x.value) is of type List[Object]
[ Error  ]                   x._2 is of type List[BigInt]
[ Error  ]                     x is of type (A, List[BigInt])
[ Error  ]                   (x: BigInt) => Integer(x) is of type (BigInt) => Object
[ Error  ]                     Integer(x) is of type Object
[ Error  ]                       x is of type BigInt because Integer was instantiated with  with fields (BigInt)
[ Error  ]                   (x: Object) => @unchecked x.value is of type (Object) => BigInt
[ Error  ]                     @unchecked x.value is of type BigInt
[ Error  ]                       x.value is of type BigInt
[ Error  ]                         x is of type Object because asList was instantiated with T:=BigInt,T:=Object with type (List[T],(T) => T,(T) => T) => List[T] because List was instantiated with  with fields (List[Object]) because Tuple2 was instantiated with  with fields ((Object, Object))
[ Error  ]         (x: Object) => (@unchecked x.value._1, asList[Object, BigInt]({
[ Error  ]           val x: Object = @unchecked x.value._2
[ Error  ]           @unchecked x.value
[ Error  ]         }, (x: Object) => @unchecked x.value, (x: BigInt) => Integer(x))) is of type (Object) => (Object, List[BigInt])
[ Error  ]           (@unchecked x.value._1, asList[Object, BigInt]({
[ Error  ]             val x: Object = @unchecked x.value._2
[ Error  ]             @unchecked x.value
[ Error  ]           }, (x: Object) => @unchecked x.value, (x: BigInt) => Integer(x))) is of type (Object, List[BigInt])
[ Error  ]             @unchecked x.value._1 is of type Object
[ Error  ]               @unchecked x.value is of type (Object, Object)
[ Error  ]                 x.value is of type (Object, Object)
[ Error  ]                   x is of type Object
[ Error  ]             asList[Object, BigInt]({
[ Error  ]               val x: Object = @unchecked x.value._2
[ Error  ]               @unchecked x.value
[ Error  ]             }, (x: Object) => @unchecked x.value, (x: BigInt) => Integer(x)) is of type List[BigInt]
[ Error  ]               val x: Object = @unchecked x.value._2
[ Error  ]               @unchecked x.value is of type List[Object]
[ Error  ]                 @unchecked x.value._2 is of type Object
[ Error  ]                   @unchecked x.value is of type (Object, Object)
[ Error  ]                     x.value is of type (Object, Object)
[ Error  ]                       x is of type Object
[ Error  ]                 @unchecked x.value is of type List[Object]
[ Error  ]                   x.value is of type List[Object]
[ Error  ]                     x is of type Object
[ Error  ]               (x: Object) => @unchecked x.value is of type (Object) => BigInt
[ Error  ]                 @unchecked x.value is of type BigInt
[ Error  ]                   x.value is of type BigInt
[ Error  ]                     x is of type Object
[ Error  ]               (x: BigInt) => Integer(x) is of type (BigInt) => Object
[ Error  ]                 Integer(x) is of type Object
[ Error  ]                   x is of type BigInt because Integer was instantiated with  with fields (BigInt) because asList was instantiated with T:=Object,T:=BigInt with type (List[T],(T) => T,(T) => T) => List[T] because asOption was instantiated with T:=(A, List[BigInt]),T:=Object with type (Option[T],(T) => T,(T) => T) => Option[T] but couldn't find constructor Option
[ Error  ]     P(asP[B, Object](flatMap[A, B](m, f), (x: B) => x, (x: Object) => x)) is of type <untyped>
[ Error  ]       asP[B, Object](flatMap[A, B](m, f), (x: B) => x, (x: Object) => x) is of type <untyped>
[ Error  ]         flatMap[A, B](m, f) is of type P[B]
[ Error  ]           m is of type P[A]
[ Error  ]           f is of type (A) => P[B] because flatMap was instantiated with A:=A,B:=B with type (P[A],(A) => P[B]) => P[B]
[ Error  ]         (x: B) => x is of type (B) => B
[ Error  ]           x is of type B
[ Error  ]         (x: Object) => x is of type (Object) => Object
[ Error  ]           x is of type Object because asP was instantiated with A:=B,A:=Object with type (P[A],(A) => A,(A) => A) => P[A] but couldn't find constructor P
[ Error  ]   () is of type Unit
               assert(m.p(ts) == m.flatMap(f))
               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[ Fatal  ] Well-formedness check failed after phase TypeEncoding

[jad-hamza]

Probably related to: https://github.com/epfl-lara/stainless/issues/847