Idea: Change trait implied bounds to use a fix-point algorithm to support cycles

compiler traits working group
1 
pub trait Tr1 {
    type Ty: Tr2<Ty = Self>;
    type Ty2: Tr1<Ty2 = Self::Ty2>;
}

pub trait Tr2 {
    type Ty: Tr1<Ty = Self>;
}

pub trait Tr3: Tr1<Ty2: Tr3> {}

I think it would be nice for the trait implied bounds algorithm to use a fixed-point algorithm (which would let the above code compile) instead of what it is now, where it apparently tries to do a depth-first search and errors on any loops.

2

Note that there's no single "fixpoint" here. Declaring all those traits to be well formed or no trait to be well formed are both fixpoints, respectively the greatest and least fixpoint. A depth-first search with error on any loop is a valid least fixpoint algorithm (assuming no "or" clauses). What you want is instead a greatest fixpoint, also known as coinductive cycles. The rustc dev guide has a page on coinduction, along with an explanation of some issues that arise from extending this to more goals (in which associated type bounds are included)

5 Likes