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

Enums

Traits