Well-formedness checking of declarations

[nikomatsakis]

We don't currently do any WF checking. Specifically, it'd be nice to lower each struct/trait/impl into a predicate that, if provable, defines whether the declaration is well-formed. In most cases this is relatively straightforward, though depending how far we go we might need to extend the IR.

For example, structs don't currently list their fields, but the WF rules for structs require that the type of each field is WF. So if we had a struct:

struct Foo<T> {
    b: Bar<T>
}

struct Bar<T> where T: Eq { t: T }

Then the WF predicate for Foo might look like:

StructFooWF :-
    forall<T> {
        WF(Bar<T>)
    }.

This relies on us having the rules for when types are well-formed (which...I think we do? if not, should open a bug on that), which would look like:

WF(Bar<T>) :- T: Eq.

In this case, that would be unprovable, and hence the struct Foo is not considered well-formed (not without a T: Eq where-clause, at least). If we added the T: Eq where clause:

struct Foo<T> where T: Eq { b: Bar<T> }

then we would have:

StructFooWF :-
    forall<T> {
        if (T: Eq) {
            WF(Bar<T>)
        }
    }.

and everything is provable again.

[nikomatsakis]

Probably the first step to tackling this bug is breaking it into steps and opening issues on those =)

[mrhota]

@nikomatsakis can you provide some guidance on what those steps might be?