Unsupported constant type Ref(...)

[Patrick-6]

Logical Equality currently does not work for enums:

use prusti_contracts::*;

pub enum TestEnum {
    Nil,
}

#[ensures(TestEnum::Nil === TestEnum::Nil)]
fn test() {}

Error on === TestEnum::Nil:

[Prusti: unsupported feature]
unsupported constant type Ref(ReErased, bug::unsupported_enum_equality::TestEnum, Not)

[Aurel300]

The issue arises when you use &Foo where Foo is a constant, such as an enum variant with no arguments. a === b desugars to snapshot_equality(&a, &b), hence the error here.

[jscissr]

There is a workaround for this problem: You can write a pure function which returns the constant. This only works if the type is Copy.

#[pure]
// Work around Prusti limitation. ("unsupported constant type")
fn none<T: Copy>() -> Option<T> {
  None
}

#[requires(x === none())]
fn demo(x: Option<bool>) {}