Fix #1349 (#1393)

core/src/main/scala/stainless/extraction/methods/MethodLifting.scala

@@ -71,9 +71,18 @@ class MethodLifting(override val s: Trees, override val t: oo.Trees)
 
     override def transform(e: s.Expr): t.Expr = e match {
       case s.MethodInvocation(rec, id, tps, args) =>
-        val ct = rec.getType(using symbols).asInstanceOf[s.ClassType]
+        given s.Symbols = symbols
+        val ct = rec.getType match {
+          case ct: s.ClassType => ct
+          case ta: s.TypeApply if ta.lookupTypeDef.isDefined && !ta.isAbstract =>
+            ta.resolve match {
+              case ct: s.ClassType => ct
+              case other => context.reporter.fatalError(rec.getPos, s"Unexpected type for method invocation receiver: got $other")
+            }
+          case other => context.reporter.fatalError(rec.getPos, s"Unexpected type for method invocation receiver: got $other")
+        }
         val cid = symbols.getFunction(id).flags.collectFirst { case s.IsMethodOf(cid) => cid }.get
-        val tcd = (ct.tcd(using symbols) +: ct.tcd(using symbols).ancestors).find(_.id == cid).get
+        val tcd = (ct.tcd +: ct.tcd.ancestors).find(_.id == cid).get
         t.FunctionInvocation(id, (tcd.tps ++ tps) map transform, (rec +: args) map transform).copiedFrom(e)
 
       case _ => super.transform(e)

frontends/benchmarks/verification/valid/i1349a.scala

@@ -0,0 +1,27 @@
+import stainless.lang._
+import stainless.collection._
+
+object i1349a {
+  type Index = BigInt
+
+  type LIndex = List[Index]
+
+  case class IndexedKey(index: BigInt, key: LIndex) {
+    require(0 <= index && index < key.length)
+  }
+
+  def mkIndexedKey1(index: BigInt, key: LIndex): IndexedKey = {
+    require(0 <= index && index < key.length)
+    IndexedKey(index, key)
+  }
+
+  def mkIndexedKey2(index: BigInt, key: List[Index]): IndexedKey = {
+    require(0 <= index && index < key.length)
+    IndexedKey(index, key)
+  }
+
+  def mkIndexedKey3(index: Index, key: LIndex): IndexedKey = {
+    require(0 <= index && index < key.length)
+    IndexedKey(index, key)
+  }
+}

frontends/benchmarks/verification/valid/i1349b.scala

@@ -0,0 +1,21 @@
+object i1349b {
+  final case class Wrap[A](a: A) {
+    def get: A = a
+  }
+
+  type WInt = Wrap[Int]
+
+  case class IndexedKey(key: WInt) {
+    require(key.get < 100)
+  }
+
+  def mkIndexedKey1(key: WInt): IndexedKey = {
+    require(key.get < 100)
+    IndexedKey(key)
+  }
+
+  def mkIndexedKey2(key: Wrap[Int]): IndexedKey = {
+    require(key.get < 100)
+    IndexedKey(key)
+  }
+}