WF rules for structs

[nikomatsakis]

In #145, @jackh726 added basic WF rules for ADTs:

a-mir-formality/crates/formality-prove/src/prove/prove_wf.rs

Lines 42 to 46 in c0e0691

	(
	(for_all(&decls, &env, &assumptions, &parameters, &prove_wf) => c)
	--- ("ADT")
	(prove_wf(decls, env, assumptions, RigidTy { name: RigidName::AdtId(_), parameters }) => c)
	)

These rules effectively say that Foo<T0...Tn> is WF if T0..Tn are WF. That's necessary but not sufficient. They should also look up the where-clauses declared on Foo and prove that those hold.

[nikomatsakis]

Mentoring instructions

The Decls struct needs to be extended to include information about each ADT, similar to the existing trait_decls field. I imagine something like adt_decls: Vec<AdtDecl>. Like [TraitDecl], each AdtDecl would have a id: AdtId field and a binder field, the bound data for which stores the where-clauses (and eventually the field names and types). This would be populated based on the structs and enums appearing in the crates.

[shua]

I guess this was completed in #148? I do see a check for where clauses on adts.