Cyclic dependency between trait definitions doesn't work well with F*

[maximebuyse]

#[derive(PartialEq, Eq)]
struct W(u16);

impl Ord for W {
    fn cmp(&self, other: &Self) -> core::cmp::Ordering {
        self.0.cmp(&other.0)
    }
}

impl PartialOrd for W {
    fn partial_cmp(&self, other: &Self) -> Option<core::cmp::Ordering> {
        Some(self.cmp(other))
    }
}

Open this code snippet in the playground

In this example partial_cmp is defined using cmp. But PartialOrd is a trait bound of Ord so we would need to define mutually recursive type class implementations in F* which is not possible.

Maybe this is not something we want to fix, the workaround for the example would be to not define partial_cmp using cmp and repeat the definition:

impl PartialOrd for W {
    fn partial_cmp(&self, other: &Self) -> Option<core::cmp::Ordering> {
        Some(self.0.cmp(&other.0))
    }
}

And to avoid code duplication this can be reused in the definition of Ord:

impl Ord for W {
    fn cmp(&self, other: &Self) -> core::cmp::Ordering {
        self.partial_cmp(other).unwrap()
    }
}

I mark this as bug because we shouldn't produce invalid F* code, we can decide to leave this as unsupported but then we should report an error.

[karthikbhargavan]

Keeping alive for now.

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[clementblaudeau]

Still relevant