search

dafny-lang / dafny

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

Rust compilation doesn't handle polymorphic static functions #5758

Open erniecohen opened 2 months ago

erniecohen commented 2 months ago

Dafny version

4.8.0 (nightly 9/6)

Code to produce this issue

datatype F<T> = F(t:T) {
    static function ctor(t:T):F<T> { F(t) }
}

Command to run and resulting output

Dafny.dll run -t:rs test.dfy

What happened?

(0,-1): Error: Microsoft.Dafny.UnsupportedInvalidOperationException: Static functions with type arguments

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

Mac

robin-aws commented 2 months ago

Thanks for the report. There are several gaps like this since the Rust backend is not yet complete, but this may be easy to address. @MikaelMayer?