newtypes not recognized as subtypes for <

[erniecohen]

Failing code

newtype P = nat
newtype Q = P
predicate test(p:P,q:Q) { p < q } // error: arguments to < must have a common supertype

Steps to reproduce the issue

• Dafny version: 4.6.0.0
• Dafny VSCode extension version: 3.3.0

Expected behavior

Actual behavior

[MikaelMayer]

Newtypes really define a new opaque type that is not compatible with other types except through explicit conversions. So you have to write this:

newtype P = nat
newtype Q = P
predicate test(p:P,q:Q) { p < q as P }

[erniecohen]

I don't think that is correct. For example, you can compare a nat (which is a newtype) to an int without complaint. As the error message says, they just have to have a common supertype, which I assume is where the relational operator is evaluated.

[keyboardDrummer]

For example, you can compare a nat (which is a newtype)

According to the documentation, nat is a subset type of int, which is different from a newtype.

[erniecohen]

Okay, I am officially senile.

[MikaelMayer]

Related fact: the current Dafny to Rust compiler I'm revisiting was emitting the "nat" subset type as a new type declaration and wrapper, which was wrong (it caused many issues with casting). I'm fixing it today. So you're not the only one confused with the difference between newtype and subset type.