It is probably worth explicitly pointing out in your overview that a goal of this inference is that the inference results should be oblivious to the code (expression bodies) within the crate, and solely uses the type definitions and function signatures as the basis for building up its constraint sets.

This goal is an explicit pat of the Altidor paper, and I know that its a goal of yours from my conversations with you.   I just think pointing it out explicitly in a comment will help people comprehend the code.