Obviously overlapping blanket impls are accepted

[CheaterCodes]

In the hope of progressing rust-lang/rust#20400, I stumbled across rust-lang/rfcs#1672.
Given this comment, I decided to properly investigate a-mir-formality.

As it turns out, the current overlap checks are very generous. I don't know whether this is intentional and I just misunderstood the purpose of this tool, or if it's an oversight, or simply incompleteness. In any case, the following test is currently accepted by a-mir-formality, and I personally think it should (obviously) not be:

[
    crate core {
        trait Foo { }

        trait Bar { }

        impl<ty T> Foo for T { }
        
        impl<ty T> Foo for T where T: Bar { }
    }
]

I also pushed this test blanket_overlap with the expected error output to a branch on my fork:
https://github.com/CheaterCodes/a-mir-formality/tree/overlap_test

It appears that currently, a-mir-formality is not considering that a downstream type may implement both of the above traits, instead it just determines that may_be_remote is provable false (which it isn't, if I understand this code correctly).

If my understanding so far is correct, I'll happily look into this more closely, but it seems like fairly major effort would be required.

[compiler-errors]

For the record, : is outlives syntax. See #147.

I think the trait bound is expressed Bar(T), though reference other tests to make sure.

[lqd]

Coherence is also currently being worked on according to https://hackmd.io/gw4UQcN8Rm-MGqFFF0M6jA#Tracking-issue-for-a-mir-formality

[CheaterCodes]

For the record, : is outlives syntax. See #147.

I think the trait bound is expressed Bar(T), though reference other tests to make sure.

I'm not sure if this is true. Other tests use the same syntax, and the grammar also suggests that this is correct:

a-mir-formality/tests/ui/coherence_overlap/u32_T_where_T_Is_impls.🔬

Line 7 in 3468054

impl<ty T> Foo for T where T: Is {}