Why chalk is not used directly by rust? And is this chalk test correct?

code review
1

Recently I had to dig in rust type system, mainly by trial and error to figure out how its logic is implemented. I have finally find out a bug that is pervasive, for example it affects the typenum crate. This bug happen in complex situations but can be reduced, I believe, to that:

trait Tr {
                type Output;
            }
 trait X <T, U> 
 where T: Tr<Output = <U as Tr>::Output>,
            U: Tr<Output = <T as Tr>::Output>
                  {}

I have started to dive inside rust source code and apparently, rust type system logic is meant to be implemented by a crate called chalk. I wrote a test and chalk does accept this code:

#[test]
fn recursively_bounded_projection() {
    lowering_success! {
        program {
            trait Tr {
                type Output;
            }
            trait X <T, U> 
            where T: Tr<Output = <U as Tr>::Output>,
                  U: Tr<Output = <T as Tr>::Output>
                  {}
        }
    }
}

Does this mean that chalk support those kind of recursive constraints ?

An other unrelated question, why rust does not use chalk directly for the type system logic?

2

It’s a work in progress, which can be turned on with the -Zchalk option to the nightly compiler. Last time I checked (a few months ago), it failed on most Rust code.

1 Like
3

This topic was automatically closed 90 days after the last reply. We invite you to open a new topic if you have further questions or comments.