spurious proof obligations generated from subset types

[erniecohen]

Dafny version

4.9.1

Code to produce this issue

datatype List<T> = Nil | Cons(hd:T,tl:List<T>) 
predicate c(x:T_,y:T_) decreases x.sz() + y.sz() requires x.i() && y.i()
type T = t:T_ | t.i() witness *       
datatype T_ = N | P(x:T_,y:T_) {
    function sz():nat { if N? then 1 else 1 + x.sz() + y.sz() }
    predicate i() decreases sz() { N? || (x.i() && y.i() && c(x,y))}
}
function lSz(l:List<T>):nat { if l.Nil? then 0 else l.hd.sz() + lSz(l.tl) }
function f(ts:List<T>):List<T> decreases lSz(ts) { // flatten
    if ts.Nil? then Nil else if ts.hd.N? then List<T>.Cons(ts.hd,f(ts.tl)) 
    else Cons(ts.hd.x,Cons(ts.hd.y,ts.tl as List<T_>))
}

Command to run and resulting output

In `f`, removing either the `as List<T_>` or the `List<T>.` prefix of the preceding `Cons` causes verification to fail.

What happened?

Neither of these annotations should be necessary. Note that normally T_ would be hidden from clients, so even the evil as workaround above would not be sufficient.

What type of operating system are you experiencing the problem on?

Mac