search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.93k stars 262 forks source link

Predicate subtype of bounded type parameter verifies but build fails #5881

Open erniecohen opened 3 weeks ago

erniecohen commented 3 weeks ago

Dafny version

4.9.0

Code to produce this issue

type Unique<T(!new)> = t:T | true witness *
trait IntOps<T(!new)> {
    predicate le(x:T,y:T)
}
datatype Int<T(!new),O(!new) extends IntOps<T>> = Int(t:T, o_:Unique<O>) { 
    const o := o_ as IntOps<T>
}

Command to run and resulting output

dafny run --general-traits:datatype --type-system-refresh

What happened?

ailed to compile C# source code using ... error CS0030: Cannot convert type 'O' to '__O'

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

Mac