Discarding evaluatable bounds and soundness

[lcnr]

What is this

This is a design document for const generics. Any discussions about its content should be on zulip. The conclusions of these discussions should then be edited back into this issue. Please do not post any comments directly in this issue.

Content

Assuming that we add const evaluatability bounds, there might be a lot of cases where explicit bounds are obviously correct but cannot be discarded automatically be the compiler.

fn small<const N: usize>()
where
    evaluatable { N - 2 },
{}

fn big<const N: usize>()
where
    evaluatable { N / 4 - 2 }

fn uses_both<const N: usize>()
where
    ...
{
    small();
    big();
}

To satisfy the bounds of small and big we would have to add both bounds to uses_both, even though the bound of big also guarantees that the bound of small holds. This is impossible to verify for the compiler in the general case.

It would therefore be nice to somehow discard the bound of small as the author of uses_both without being able to prove that it must hold.

How to do that is still unclear however.