Equality, Subtyping, and Snapshots in Rust Type Inference

value as a result. The region variables work somewhat differently, and are described below in a separate section. ## Enforcing equality / subtyping The most basic operations you can perform in the type inferencer is **equality**, which forces two types `T` and `U` to be the same. The recommended way to add an equality constraint is to use the `at` method, roughly like so: ```rust,ignore infcx.at(...).eq(t, u); ``` The first `at()` call provides a bit of context, i.e. why you are doing this unification, and in what environment, and the `eq` method performs the actual equality constraint. When you equate things, you force them to be precisely equal. Equating returns an `InferResult` – if it returns `Err(err)`, then equating failed, and the enclosing `TypeError` will tell you what went wrong. The success case is perhaps more interesting. The "primary" return type of `eq` is `()` – that is, when it succeeds, it doesn't return a value of any particular interest. Rather, it is executed for its side-effects of constraining type variables and so forth. However, the actual return type is not `()`, but rather `InferOk<()>`. The `InferOk` type is used to carry extra trait obligations – your job is to ensure that these are fulfilled (typically by enrolling them in a fulfillment context). See the [trait chapter] for more background on that. You can similarly enforce subtyping through `infcx.at(..).sub(..)`. The same basic concepts as above apply. ## "Trying" equality Sometimes you would like to know if it is *possible* to equate two types without error. You can test that with `infcx.can_eq` (or `infcx.can_sub` for subtyping). If this returns `Ok`, then equality is possible – but in all cases, any side-effects are reversed. Be aware, though, that the success or failure of these methods is always **modulo regions**. That is, two types `&'a u32` and `&'b u32` will return `Ok` for `can_eq`, even if `'a != 'b`. This falls out from the "two-phase" nature of how we solve region constraints. ## Snapshots As described in the previous section on `can_eq`, often it is useful to be able to do a series of operations and then roll back their side-effects. This is done for various reasons: one of them is to be able to backtrack, trying out multiple possibilities before settling on which path to take. Another is in order to ensure that a series of smaller changes take place atomically or not at all. To allow for this, the inference context supports a `snapshot` method. When you call it, it will start recording changes that occur from the operations you perform. When you are done, you can either invoke `rollback_to`, which will undo those changes, or else `confirm`, which will make them permanent. Snapshots can be nested as long as you follow a stack-like discipline. Rather than use snapshots directly, it is often helpful to use the methods like `commit_if_ok` or `probe` that encapsulate higher-level patterns. ## Subtyping obligations One thing worth discussing is subtyping obligations. When you force two types to be a subtype, like `?T <: i32`, we can often convert those into equality constraints. This follows from Rust's rather limited notion of subtyping: so, in the above case, `?T <: i32` is equivalent to `?T = i32`. However, in some cases we have to be more careful. For example, when

This section discusses the enforcement of equality and subtyping in Rust's type inference using methods like `infcx.at(...).eq(t, u)` and `infcx.at(..).sub(..)`. It explains how these methods work, their return types (`InferOk`), and the importance of fulfilling trait obligations. Additionally, it covers how to test the possibility of equating two types without errors using `infcx.can_eq` and `infcx.can_sub`, noting that these methods are modulo regions. The section also details the use of snapshots for rolling back side-effects of operations, enabling backtracking and ensuring atomic changes, with methods like `rollback_to` and `confirm` for managing these changes. It finally touches upon subtyping obligations, explaining how they can often be converted into equality constraints.