Size of type parameters

[mbovel]

This works:

import stainless.collection.{List, Nil, Cons}
import stainless.lang.*

enum Term:
  case Atom(i: BigInt)
  case App(fun: Term, args: TermList)

enum TermList:
  case TermNil()
  case TermCons(x: Term, xs: TermList)

import Term.*
import TermList.*

def termSize(t: Term): BigInt = {
  t match
    case Atom(_)        => BigInt(1)
    case App(fun, args) => 1 + termSize(fun) + termListSize(args)
}.ensuring(_ >= 1)

def termListSize(l: TermList): BigInt = {
  l match
    case TermNil()       => BigInt(0)
    case TermCons(x, xs) => termSize(x) + termListSize(xs)
}.ensuring(_ >= 0)

The same using Stainless'List doesn't:

import stainless.collection.{List, Nil, Cons}
import stainless.lang.*

enum Term2:
  case Atom(i: BigInt)
  case App(fun: Term2, args: List[Term2])
import Term2.*

def term2Size(t: Term2): BigInt = {
  decreases(t)
  t match
    case Atom(_)        => BigInt(1)
    case App(fun, args) => 1 + term2Size(fun) + term2ListSize(args)
}.ensuring(_ >= 1)

def term2ListSize(l: List[Term2]): BigInt = {
  decreases(l)
  l match
    case Nil()       => BigInt(0)
    case Cons(x, xs) => term2Size(x) + term2ListSize(xs)
}.ensuring(_ >= 0)

which outputs:

[Warning ]  - Result for 'measure decreases' VC for term2ListSize @25:25:
[Warning ] l.isInstanceOf[Nil] || Term2PrimitiveSize(l.h) < ListPrimitiveSize[Term2](l)
[Warning ] stcc2.scala:25:25:  => INVALID
               case Cons(x, xs) => term2Size(x) + term2ListSize(xs)
                                   ^^^^^^^^^^^^
[Warning ] Found counter-example:
[Warning ]   l: List[Term2] -> Cons[Term2](Atom(BigInt("-1")), Nil[Term2]())

I also tried:

import stainless.collection.{List, Nil, Cons}
import stainless.lang.*

enum Term3:
  case Atom(i: BigInt)
  case App(fun: Term3, args: List[Term3])
import Term3.*

def term3Size(t: Term3): BigInt = {
  decreases(t)
  t match
    case Atom(_)        => BigInt(1)
    case App(fun, args) =>
      args match
        case Nil()       => BigInt(1)
        case Cons(x, xs) =>
          BigInt(1) + term3Size(x) + term3Size(App(fun, xs))
}.ensuring(_ >= 1)

which outputs:

[Warning ]  - Result for 'measure decreases' VC for term3Size @22:23:
[Warning ] t.isInstanceOf[Atom] || t.args.isInstanceOf[Nil] || Term3PrimitiveSize(t.args.h) < Term3PrimitiveSize(t)
[Warning ] stcc3.scala:22:23:  => INVALID
                     BigInt(1) + term3Size(x) + term3Size(App(fun, xs))
                                 ^^^^^^^^^^^^
[Warning ] Found counter-example:
[Warning ]   t: Term3 -> App(Atom(BigInt("0")), Cons[Term3](App(Atom(BigInt("-1")), Nil[Term3]()), Nil[Term3]()))

I think the problem is that List doesn't take the size of its type parameter into account. This is clear when tracing fullSize:

fullSize:      args
fullSize type: List[Term3]

fullSize:      h
fullSize type: T

where the fullSize of the TypeParameter T is 0, that's the default case of fullSize:

stainless/core/src/main/scala/stainless/termination/SizeFunctions.scala

Lines 207 to 208 in e5099c5

	case _ =>
	IntegerLiteral(0)

This makes sense as there is currently a single size function per sort.

But this means that the size of a list is just its length, which prevents recursing on its elements.

Could the size of type parameters somehow be taken into account when computing the size of parametric types? That would probably require generating a different size function for each instantiation of a parametric type.

Or are there known workarounds? Defining my own monomorphic list type is one, but it's far from ideal as I have to re-implement and re-prove any method or property I want to use on lists.