Expand description

This code is kind of an alternate way of doing subtyping, supertyping, and type equating, distinct from the combine.rs code but very similar in its effect and design. Eventually the two ought to be merged. This code is intended for use in NLL and chalk.

Here are the key differences:

  • This code may choose to bypass some checks (e.g., the occurs check) in the case where we know that there are no unbound type inference variables. This is the case for NLL, because at NLL time types are fully inferred up-to regions.
  • This code uses “universes” to handle higher-ranked regions and not the leak-check. This is “more correct” than what rustc does and we are generally migrating in this direction, but NLL had to get there first.

Also, this code assumes that there are no bound types at all, not even free ones. This is ok because:

  • we are not relating anything quantified over some type variable
  • we will have instantiated all the bound type vars already (the one thing we relate in chalk are basically domain goals and their constituents)

Structs

When we encounter a binder like for<..> fn(..), we actually have to walk the fn value to find all the values bound by the for (these are not explicitly present in the ty representation right now). This visitor handles that: it descends the type, tracking binder depth, and finds late-bound regions targeting the for<..>. For each of those, it creates an entry in bound_region_scope.
The “type generalizer” is used when handling inference variables.

Enums

Traits

When we instantiate an inference variable with a value in relate_ty_var, we always have the pair of a TyVid and a Ty, but the ordering may vary (depending on whether the inference variable was found on the a or b sides). Therefore, this trait allows us to factor out common code, while preserving the order when needed.