Imposes a constraint on keys. They can be obtained by using the associated functions of [TcKey]. Returns a [TcErr] if the constraint immediately reve

Declares that `self` is at least as concrete as `bound`.

Generates a new key representing a term.

Finalizes the type check procedure. Calling this function indicates that all relevant information was passed on to the type checker. It will attempt t

Connects two keys asymmetrically. Refining `bound` refines `self` whereas refining `self` leaves `bound` unaffected.

Equates two keys, i.e., they refer to the same type and are thus symmetrically connected. Refining one will refine the other as well.

Declares a symmetric relation between two keys.

Manages keys for variables. It checks if `var` already has an associated key. If so, it returns the key. Otherwise, it generates a new one.

Declares that `self` is the meet of `left` and `right`. This binds `self` to both `left` and `right` asymmetrically.

Finalizes the type check procedure without constructing a full type table. Refer to [TypeChecker::type_check] if [Variant] implements [Constructable]

This function traverses the expression tree. It creates keys on the fly. This is not possible for many kinds of type systems, in which case the funct

Creates and registers a new vertex.

Grants mutable access to the underlying full vertex. # Panics Panics if `self` is not a full vertex.

Starts a fix point computation successively checking and resolving constraints captured in the graph. Returns the type table mapping each registered k

Transforms `sub` into a forward to `repr`.

Imposes an explicit bound on a key. An Err return indicates a contradiction, an Ok does not indicate the absence of a contradiction.

Grants immutable access to the underlying full vertex. # Panics Panics if `self` is not a full vertex.

Returns the reference of the vertex representing this one. Returns None if this vertex represents itself.

Declares that `self` is the meet of all elements contained in `elems`. This binds `self` to all of these keys asymmetrically.

Declares that `self` is the symmetric meet of all elements contained in `elems`. This binds `self` to all of these keys symmetrically.

Lifts a collection of keys as subset of children into a certain recursive variant.

Registers that a key has at least `n` children. If this fact was already known and thus a key is already associated with the child, the key is return

Returns an Iterator over all full vertices in `self`. This does not resolve forwards, thus every representative only occurs once.

Meets all the types of upper bounds with the type of the vertex itself.

This function traverses the expression tree. It creates keys on the fly. This is not possible for many kinds of type systems, in which case the funct

Transform `self` into an option, i.e., it will yield a `Some` with its arity if defined and `None` otherwise.

Finalizes the type check procedure without constructing a full type table. See [`TypeChecker::type_check_preliminary`] for details.

Finalizes the type check procedure, and returns ownership of the context to the caller. See [`TypeChecker::type_check_with_context`] for details.

Create an iterator over all keys currently registered in the graph.

Returns an iterator over all keys currently present in the type checking procedure.

Returns an immutable reference to the context.

Returns a mutable reference to the context.

Adds `entry` to `v` until it has length `size`.

Provides a key to the `nth` child of the type behind `parent`. This imposes the restriction that `parent` resolves to a type that has at least an arit

Declares that `self` is the symmetric meet of `left` and `right`. This binds `self` to both `left` and `right` symmetrically.

Lifts a collection of keys as children into a certain recursive variant.

Creates an empty constraint graph.

Creates a new, empty type checker.

Creates a full vertex without information regarding its children.