Description
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:
Then we have to update the chalk-slg HhGoal type in an analogous fashion:
Presumably extending the Context trait with the notion of a clause as well:
Finally, we have to modify the Context::program_clauses implementation:
In particular, this is the code that finds hypotheses from the environment:
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.)