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.
This works:
The same using Stainless'
List
doesn't:which outputs:
I also tried:
which outputs:
I think the problem is that
List
doesn't take the size of its type parameter into account. This is clear when tracingfullSize
:where the
fullSize
of theTypeParameter
T
is0
, that's the default case offullSize
:https://github.com/epfl-lara/stainless/blob/e5099c5fef3a53bd42cb4fcf103e1d4b0b48329f/core/src/main/scala/stainless/termination/SizeFunctions.scala#L207-L208
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.