Documentation

The constraints that are required for kind checking.

The general constraints that are required for type checking a Plutus AST.

Mapping from Builtins to their Normalized Kinds.

Configuration of the kind checker.

Configuration of the type checker.

Decides what to do upon encountering a variable whose name doesn't match the name of the variable with the same unique that is currently in the scope. Consider for example this type:

(a_0 :: *) (b_0 :: *) -> a_0

here b_0 shadows a_0 and so any variable having the 0th unique within the body of the lambda references b_0, but we have a_0 there and so there's a name mismatch. Technically, it's not a type error to have a name mismatch, because uniques are the single source of truth, however a name mismatch is deeply suspicious and is likely to be caused by a bug somewhere.

We perform the same check for term-level variables too.

We want HasKindCheckConfig to be a superclass of HasTypeCheckConfig for being able to seamlessly call the kind checker from the type checker, hence we're rolling out our own makeClassy here just to add the constraint.

The environment that the type checker runs in.

The type checking monad that the type checker runs in. In contains a TypeCheckEnv and allows to throw TypeErrors.

The constraints that are required for type checking Plutus Core.

Extend the context of a TypeCheckM computation with a typed variable.

Normalize a Kind.

Substitute a type for a variable in a type and normalize the result.

Check a Term against a NormalizedType.

Run a TypeCheckM computation by supplying a TypeCheckConfig to it.

Used for both type and kind checking, because we need to do kind checking during type checking and so it makes sense to keep a single monad. However type checking requires a TypeCheckConfig, while kind checking doesn't, hence we keep the kind checker fully polymorphic over the type of config, so that the kinder checker can be run with an empty config (such as ()) and access to a TypeCheckConfig is not needed.

Extend the context of a TypeCheckM computation with a kinded variable.

Look up the type of a built-in function.

Look up a type variable in the current context.

Look up a term variable in the current context.

Infer the kind of a type.

Check a Kind against a Kind.

unfoldIFixOf pat arg k = NORM (vPat ((a :: k) -> ifix vPat a) arg)

Synthesize the type of a term, returning a normalized type.

The constraints that type normalization requires.