Trait resolution: given a trait reference, we track which local clause caused it to be true.
This module is independent from the rest of hax, in particular it doesn’t use its
state-tracking machinery.
An ImplExpr describes the full data of a trait implementation. Because of generics, this may
need to combine several concrete trait implementation items. For example, ((1u8, 2u8), "hello").clone() combines the generic implementation of Clone for (A, B) with the
concrete implementations for u8 and &str, represented as a tree.
The source of a particular trait implementation. Most often this is either Concrete for a
concrete impl Trait for Type {} item, or LocalBound for a context-bound where T: Trait.
Solve the trait obligations for a specific item use (for example, a method call, an ADT, etc.)
in the current context. Just like generic args include generics of parent items, this includes
impl exprs for parent items.
Given a clause clause declared on item_did’s counterpart in the trait that impl_did
implements, substitutes the impl’s arguments into it and (1) derives a Clause and (2)
resolves an ImplExpr. item_did is impl_did itself for a clause of the trait, or one of
the impl’s associated items for a clause of that item; the latter appends a generic associated
type’s own parameters, which is the arity the declared clause expects.