Application types

TyKind variants that consist of some type-specific info ("type name") and a substitution are usually referred to as application types. These include most of the "normal Rust types", such as Vec and (f32, u32). Such types are only "equal" to themselves (modulo aliases, see below). Scalar types (and some others) also fall into this category, despite having no substitutions: we treat them as having zero-length substitutions. Note that we group together both user-defined structs/enums/unions (like Vec) as well as built-in types like f32, which effectively behave the same.

We used to have application types in chalk as a separate notion in the codebase, but have since moved away from that; nevertheless, the term is still useful in discussions.

Notable application types

Coroutine

A Coroutine represents a Rust coroutine. There are three major components to a coroutine:

  • Upvars - similar to closure upvars, they reference values outside of the coroutine, and are stored across all yield points.
  • Resume/yield/return types - the types produced/consumed by various coroutine methods. These are not stored in the coroutine across yield points - they are only used when the coroutine is running.
  • Coroutine witness - see the Coroutine Witness section below.

Of these types, only upvars and resume/yield/return are stored directly in CoroutineDatum (which is accessed via RustIrDatabase). The coroutine witness is implicitly associated with the coroutine by virtue of sharing the same CoroutineId. It is only used when determining auto trait impls, where it is considered a 'constituent type'.

For example:

// This is not "real" syntax at the moment.
fn gen() -> Bar {
  let a = yield 0usize;
  use(a)
}

fn use(_: usize) -> Bar {}

The type of yield would be usize, the resume type would be the type of a and the return type would be Bar.

Coroutine witness types

The CoroutineWitness variant represents the coroutine witness of the coroutine with id CoroutineId.

The coroutine witness contains multiple witness types, which represent the types that may be part of a coroutine state - that is, the types of all variables that may be live across a yield point.

Unlike other types, witnesses include bound, existential lifetimes, which refer to lifetimes within the suspended stack frame. You can think of it as a type like exists<'a> { (T...) }. As an example, imagine that a type that isn't Send lives across a yield, then the coroutine itself can't be Send.

Witnesses have a binder for the erased lifetime(s), which must be handled specifically in equating and so forth. In many ways, witnesses are also quite similar to Function types, and it is not out of the question that these two could be unified; however, they are quite distinct semantically and so that would be an annoying mismatch in other parts of the system. Witnesses are also similar to a Dyn type, in that they represent an existential type, but in contrast to Dyn, what we know here is not a predicate but rather some upper bound on the set of types contained within.