Option type with Generics: cannot return a value of the generic type

[Ramla-I]

I copied the Option code that was given in the user guide, and tried to convert it to use generics:

pub enum TrustedOption<T: Copy + Clone> {
    Some(T),
    None,
}

impl<T: Copy + Clone> TrustedOption<T> {

    #[pure]
    pub fn is_none(&self) -> bool {
        match self {
            TrustedOption::Some(_) => false,
            TrustedOption::None => true,
        }
    }

    #[pure]
    pub fn is_some(&self) -> bool {
        !self.is_none()
    }

    #[pure]
    #[requires(self.is_some())]
    pub fn peek(&self) -> T {
        match self {
            TrustedOption::Some(val) => *val,
            TrustedOption::None => unreachable!(),
        }
    }
}

I get the error [Prusti: unsupported feature] T type is not supported

Is this expected, or am I missing something in how generics are used in Prusti?

[vakaras]

This looks like a bug. Since T is Copy, this should work.

[JonasAlaif]

See my comment here: https://github.com/viperproject/prusti-dev/issues/1117#issuecomment-1229510304 (it looks like you are using an "outdated" - we should do a stable release soon - version of Prusti)