Time out while matching on a Tuple ADT

[yannbolliger]

The combination of

• using a type class,
• having a recursive data type and
• matching on a Tuple2 ADT

makes Stainless time out on the following benchmark:

import stainless.annotation._

object Mutable {
  case class Tuple2[@mutable T0, @mutable T1](_0: T0, _1: T1)

  @mutable
  sealed abstract class List[@mutable T] {}
  case class Nil[@mutable T]() extends List[T]
  case class Cons[@mutable T](var _0: T, var _1: List[T]) extends List[T]

  abstract class Equals[@mutable T] {
    @pure
    def equals(param0: T, param1: T): Boolean
  }

  case class ListTasEquals[@mutable T](ev0: Equals[T]) extends Equals[List[T]] {
    @pure
    def equals(self: List[T], other: List[T]): Boolean =
      Tuple2(self, other) match {
        case Tuple2(Nil(), Nil()) => true
        case Tuple2(Cons(x, xs), Cons(y, ys)) => this.ev0.equals(x, y)
        case _ => false
      }
  }
}

The issue seems to arise in AntiAliasing where some strange casts are introduced.

tree ouput

Symbols before AntiAliasing:
 @pure
 def equals[T @mutable](thiss: ListTasEquals[T @mutable], self: List[T @mutable], other: List[T @mutable]): Boolean = Tuple2[List[T @mutable], 
List[T @mutable]](self, other) match {
   case Tuple2(Nil(), Nil()) =>
     true
   case Tuple2(Cons(x, xs), Cons(y, ys)) =>
     equals[T @mutable](thiss.ev0, x, y)
   case _ =>
     false
 }

Symbols after AntiAliasing:
 @pure
 def equals[T @mutable](thiss: ListTasEquals[T @mutable], self: List[T @mutable], other: List[T @mutable]): Boolean = Tuple2[List[T @mutable], List[T @mutable]](self, other) match {
   case Tuple2(Nil(), Nil()) =>
     true
   case Tuple2(Cons(x, xs), Cons(y, ys)) =>
     var res: (Boolean, T @mutable, T @mutable) = equals[T @mutable](thiss.ev0, Tuple2[List[T @mutable], List[T @mutable]](self, other).asInstanceOf[Tuple2[List[T @mutable], List[T @mutable]]]._0.asInstanceOf[Cons[T @mutable]]._0, Tuple2[List[T @mutable], List[T @mutable]](self, other).asInstanceOf[Tuple2[List[T @mutable], List[T @mutable]]]._1.asInstanceOf[Cons[T @mutable]]._0)
     res._1
   case _ =>
     false
 }

The issue goes away, if one

• doesn't match on the Tuple2,
• uses a normal, native tuple,
• puts true instead of calling the method this.ev0.equals(x, y),
• uses a non-recursive data type like

  sealed abstract class Option[@mutable T] {}
  case class None[@mutable T]() extends Option[T]
  case class Some[@mutable T](var _0: T) extends Option[T]