Documentation

The type checker runs in this monad.

Run a TypeM computation.

Retrieve the current Env.

The name of the current file/import.

Are we type-checking at the top level, or are we inside a nested module?

We are now going to type-check the body of a module.

Map source-level names to fresh unique internal names, and evaluate a type checker context with the mapping active.

Map single source-level name to fresh unique internal names, and evaluate a type checker context with the mapping active.

Bind these identifiers in the name map and also check whether they have been used.

Try to prepend qualifiers to the type names such that they represent how to access the type in some scope.

Look up a module type.

Look up an import.

Evaluate a TypeM computation within an extended (not replaced) environment.

Information about an error during type checking.

Prettyprint type error.

Prettyprint type error, without location information. This can be used for cases where the location is printed in some other way.

Attach a reference to documentation explaining the error in more detail.

An unexpected functor appeared!

An unknown variable was referenced.

A name prefixed with an underscore was used.

A collection of extra information regarding a type error.

A single note.

Monads that support type checking. The reason we have this internal interface is because we use distinct monads for checking expressions and declarations.

Indicate that this name has been used. This is usually done implicitly by other operations, but sometimes we want to make a "fake" use to avoid things like top level functions being considered unused.

Elaborate the given name in the given namespace at the given location, producing the corresponding unique VName.

Type-check an attribute.

Elaborate the given qualified name in the given namespace at the given location, producing the corresponding unique QualName.

Elaborate the given qualified name in the given namespace at the given location, producing the corresponding unique QualName. Fails if the name is a module.

Turn a Left TypeError into an actual error.

Does a type with this name already exist? This is used for warnings, so it is OK it's a little unprincipled.

Modules produces environment with this representation.

A mapping of abstract types to their liftedness.

A parametric functor consists of a set of abstract types, the environment of its parameter, and the resulting module type.

A mapping from import import names to Envs. This is used to resolve import declarations.

A mapping from names (which always exist in some namespace) to a unique (tagged) name.

Type parameters, list of parameter types (optinally named), and return type. The type parameters are in scope in both parameter types and the return type. Non-functional values have only a return type.

Representation of a module, which is either a plain environment, or a parametric module ("functor" in SML).

A binding from a name to its definition as a type. We allow a return type here to support type abbreviations that hide some inner sizes (these must necessarily be Lifted or SizeLifted).

Representation of a module type.

All signed integer types.

All unsigned integer types.

All integer types.

All floating-point types.

All number types.

All primitive types.

The space inhabited by a name.

The NameMap corresponding to the intrinsics module.

The names that are available in the initial environment.

Construct the name of a new type variable given a base description and a tag number (note that this is distinct from actually constructing a VName; the tag here is intended for human consumption but the machine does not care).