After GATs are implemented and if everything goes well, we won't need WellFormed(WhereClauseAtom::ProjectionEq) abstraction, defeating the initial purpose of the WhereClauseAtom abstraction.

I propose that we instead re-use WhereClauseAtom to include every where clause that can effectively be written by a Rust programmer, e.g. it should include:

• Implemented(T: Foo)
• ProjectionEq(<T as Foo>::Item = U)
• T: 'a (not implemented for the moment)
• 'a: 'b

Then, the various IR constructs which represent real rust code like:
https://github.com/rust-lang-nursery/chalk/blob/eeb21829c1e847921261ad820b5b2ec35b649c76/src/ir/mod.rs#L202-L207
should carry where clauses of the type Binders<WhereClauseAtom> (which could be aliased into QuantifiedWhereClauseAtom) instead of the current type QuantifiedDomainGoal.

This will enable rewriting some match blocks where we used to do things like:

WellFormed(..) | ... | => panic!("unexepected"),

or

WellFormed(..) | ... | => (),

e.g. like in
https://github.com/rust-lang-nursery/chalk/blob/eeb21829c1e847921261ad820b5b2ec35b649c76/src/lower/wf.rs#L131-L147

Bikeshedding: we could also just use the name WhereClause instead of WhereClauseAtom, like in the old days.

Another question left open: should we merge the current WellFormed / FromEnv predicate -- which would then deal only with trait references -- with WellFormedTy / FromEnvTy?

cc @rust-lang-nursery/wg-traits