Panic when decreases clause is on a set with generic

[matthias-brun]

I wasn't sure if using a set directly in the decreases clause (rather than using s.len()) is valid. It seems to work for fixed types but Verus panics when the set elements are a generic type:

use vstd::prelude::*; verus! {

spec fn foo<A>(s: Set<A>) -> int
    decreases s when s.finite()
{
    if s.is_empty() {
        0
    } else {
        foo(s.remove(s.choose()))
    }
}

} // verus!

thread '<unnamed>' panicked at vir/src/sst_to_air.rs:168:29:
abstract datatype should be boxed Datatype(Path(Path(Some("vstd"), ["set" :: "Set"])), [TypParam("A")], [])
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
thread '<unnamed>' panicked at rust_verify/src/verifier.rs:2123:29:
worker thread panicked

[tjhance]

The panic, of course, is a bug.

However, it doesn't look like we have the relevant axiom that would make this useful (b.finite() && a.subset(b) && a != b ==> decreases_to!(b => a)). I do think such an axiom would be sound, though.