extend the definition of "clause" that chalk uses

[nikomatsakis]

The first-order hereditary harrop predicates that Chalk uses allow for a fairly flexible definition of program clause:

Clause = DomainGoal | Clause && Clause | Goal => DomainGoal | ForAll { Clause }

The intention then is that implications in Goal can reference these clauses in their full generality:

Goal = ... | Clause => Goal | ...

However, Chalk currently uses a rather simpler definition:

https://github.com/rust-lang-nursery/chalk/blob/master/src/ir/mod.rs#L776

This is equivalent to the following:

Clause = DomainGoal | Clause && Clause

We should generalize this to the full form -- or at least include ForAll binders. This will require a few changes. For one thing, we'll have to change environments to store clauses, rather than just domain goals:

https://github.com/rust-lang-nursery/chalk/blob/2575275d42a94589b9ab4263e6b62d076b66d166/src/ir/mod.rs#L74-L79

Then we have to update the chalk-slg HhGoal type in an analogous fashion:

https://github.com/rust-lang-nursery/chalk/blob/2575275d42a94589b9ab4263e6b62d076b66d166/chalk-slg/src/hh.rs#L10

Presumably extending the Context trait with the notion of a clause as well:

https://github.com/rust-lang-nursery/chalk/blob/2575275d42a94589b9ab4263e6b62d076b66d166/chalk-slg/src/context/mod.rs#L9-L11

Finally, we have to modify the Context::program_clauses implementation:

https://github.com/rust-lang-nursery/chalk/blob/2575275d42a94589b9ab4263e6b62d076b66d166/src/solve/slg/implementation/mod.rs#L69-L73

In particular, this is the code that finds hypotheses from the environment:

https://github.com/rust-lang-nursery/chalk/blob/2575275d42a94589b9ab4263e6b62d076b66d166/src/solve/slg/implementation/mod.rs#L74-L78

Actually, this code is probably fine as is, we just have to (a) implement CouldMatch for Clause and (b) implement into_program_clause for CouldMatch.

(Note: It might be good to do #90 first, just to limit the amount of code affected.)

[nikomatsakis]

cc @rust-lang-nursery/wg-traits -- another good chalk starter issue! I've laid out the steps involved.

[nikomatsakis]

@PramodBisht expressed interest in taking this on

[PramodBisht]

@nikomatsakis seems like it is more tough for me than I expected, after replacing DomainGoal with Clause(enum), I found myself replicating what DomainGoal is doing, for example changing DomainGoal type to Clause at many places. I am getting feeling that I am not wrong track. Even if this is the expected path, I assume we have to do some magic in push_initial_strands to add support of forAll clause. Please check PramodBisht@6fd653f