The checks for is-implemented where clauses are too lax

[mattheww]

formality-check isn't rejecting an is-implemented where clause with nonsense in the implementing type or in a parameter to the trait.

For example it doesn't reject a where clause whose implementing type doesn't exist:

trait Trait1 {}
struct S where Nonex: Trait1 {}

or which gives the implementing type the wrong number of parameters:

trait Trait1 {}
struct S1 {}
struct S2<ty T> where S1<T>: Trait1 {
    dummy: T
}

It accepts nonsensical types in trait parameters too:

trait Trait1<ty T> {}
struct S where u8: Trait1<Nonex> {}

I see:

• formality-check's checks amount to proving wc.well_formed() for the single where clause

• wc.well_formed() amounts to proving WellFormedTraitRef for (say) Nonex: Trait1

• the "trait well formed" rule in prove_wc() considers only the where clauses of the TraitRef's underlying trait, ignoring the TraitRef's parameters.