inspect changes

we currently leak uncanonicalized data from the current InferCtxt in the proof trees.

my proposal how to not leak

IDEA: canonicalize everything which currently contains infer vars.

EXAMPLE: instead of GoalEvaluationStep::instantiated_goal being QueryInput<'tcx, Predicate<'tcx>>^[1] it will be Canonical<'tcx, QueryInput<'tcx, Predicate<'tcx>>>

ISSUE: it's completely unclear where the bound vars come from.

IDEA: similar to the canonical query response returned by the solver, also put the "source" of the bound vars into the Canonical

so we'd use Canonical<'tcx, ProofTreeData<'tcx, QueryInput<'tcx, Predicate<'tcx>>>

struct ProofTreeData<'tcx, T> {
    var_values: CanonicalVarValues<'tcx>,
    data: T,
}

The var_values are the same as in CanonicalResponse.

Now the input isn't the only place which can introduce inference vars. Other sources are: instantiatiating binders in the query, instantiating impl params, the normalizes-to hack.

We could change the ProofTreeData to the following

struct ProofTreeData<'tcx, T> {
    var_values: CanonicalVarValues<'tcx>,
    normalizes_to_hack_term: Ty<'tcx>,
    data: T,
}

SUS

nested goals and inference progress

goals exist multiple times which is sus, they ignore inference progress.

idea: instantiate all goals, and dedup them fully resolving all of them. then fetch the nested proof tree for these goals by recomputing it.

issue: equating var_values can result in nested goals which may not hold

alternative

track add_goal.

instantiate the added goals and run it in a fulfillment context.

TODO

• differentiate between Root and nested goals because I have to track orig_values as either canonicalized or not
• canonicalize
  • change AddGoal to store State<T>
  • store orig_values for root and nested goals
• add the analyse visitor and impl it
  • how to handle cycles and overflow?
    • cycles: do not recurse into them
      Image Not Showing Possible Reasons

      • The image file may be corrupted
      • The server hosting the image is unavailable
      • The image path is incorrect
      • The image format is not supported

      Learn More →
    • overflow: completely fail to recurse? sucks idk