The trait solver can optionally emit a "proof tree", a tree representation of what happened while trying to prove a goal.
The used datastructures for which are currently stored in
rustc_middle::traits::solve::inspect.
There are 3 intended uses for proof trees. These uses are not yet implemented as the representation of proof trees itself is currently still unstable.
They should be used by type system diagnostics to get information about why a goal failed or remained ambiguous. They should be used by rustdoc to get the auto-trait implementations for user-defined types, and they should be usable to vastly improve the debugging experience of the trait solver.
For debugging you can use -Zdump-solver-proof-tree which dumps the proof tree
for all goals proven by the trait solver in the current session.
The trait solver uses Canonicalization and uses completely separate InferCtxt for
each nested goal. Both diagnostics and auto-traits in rustdoc need to correctly
handle "looking into nested goals". Given a goal like Vec<Vec<?x>>: Debug, we
canonicalize to exists<T0> Vec<Vec<T0>>: Debug, instantiate that goal as
Vec<Vec<?0>>: Debug, get a nested goal Vec<?0>: Debug, canonicalize this to get
exists<T0> Vec<T0>: Debug, instantiate this as Vec<?0>: Debug which then results
in a nested ?0: Debug goal which is ambiguous.
We need to be able to figure out that ?x corresponds to ?0 in the nested queries.
The debug output should also accurately represent the state at each point in the solver.
This means that even though a goal like fn(?0): FnOnce(i32) infers ?0 to i32, the
proof tree should still store fn(<some infer var>): FnOnce(i32) instead of
fn(i32): FnOnce(i32) until we actually infer ?0 to i32.
Proof trees will be quite involved as they should accurately represent everything the trait solver does, which includes fixpoint iterations and performance optimizations.
We intend to provide a lossy user interface for all usecases.
TODO: implement this user interface and explain how it can be used here.