error: Lookup failed for adt with symbol Conc$27 in phase FunctionSpecialization

[vkuncak]

This uses equality between wrong types in _ == t1.toList ++ t2.toList, but throws off function specialization:

info Finished compiling                                       
info Preprocessing finished                                   
info Running phase FunctionSpecialization                     
error: Lookup failed for adt with symbol `Conc$27`

Here is the entire code.

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

object SimpleConc:

  sealed abstract class Conc[T]
  case class Empty[T]() extends Conc[T]
  case class Single[T](x: T) extends Conc[T]
  case class CC[T](left: Conc[T], right: Conc[T], csize: BigInt) extends Conc[T] {
    require(csize == left.size + right.size)
  }

  extension[T](t1: Conc[T])
    def <>(t2: Conc[T]) = CC(t1, t2, t1.size + t2.size)
    def toList: List[T] = t1 match
      case Empty() => Nil[T]()
      case Single(x) => x :: Nil[T]()
      case CC(l, r, _) => l.toList ++ r.toList

    def size: BigInt = {
      t1 match
        case Empty() => BigInt(0)
        case Single(_) => BigInt(1)
        case CC(_, _, csize) => csize
    }.ensuring(_ == t1.toList.size)

    def ++(t2: Conc[T]): Conc[T] = {
      t1 match
        case Empty() => t2
        case Single(_) => t1 <> t2
        case CC(l, r, _) =>
          l ++ (r ++ t2)
    }.ensuring(_ == t1.toList ++ t2.toList)

end SimpleConc

[mario-bucev]

Should we add a check that ensures equality is only applied to comparable types?