An annotated type.

Type constructor or literal.

Type variable.

Type abstracton.

Type application.

The void constructor.

The unit constructor.

The function constructor.

Take the least upper bound at the given kind.

The least element of the given kind.

The universal quantifier with a parameter of the given kind.

The existential quantifier with a parameter of the given kind.

Primitive constructor.

Bound constructor.

Value variable or primitive operation.

Primitive values.

Data constructor or literal.

Type abstraction (level-1).

Value and Witness abstraction (level-0).

Application.

A non-recursive let-binding.

Case branching.

Type cast.

Type can appear as the argument of an application.

Witness can appear as the argument of an application.

Some expressions and infix operators that need to be resolved into proper function applications.

Use of a naked infix operator, like in 1 + 2. INVARIANT: only appears in the list of an XDefix node.

Use of an infix operator as a plain variable, like in (+) 1 2. INVARIANT: only appears in the list of an XDefix node.

Match expression with default. Similar to a case expression, except that if an alternative fails then we try the next one instead of failing. If none of the alternatives succeeds then the overall value is the value of the default expression.

Where expression defines a group of recursive clauses, and is desugared to a letrec.

Lambda abstraction which matches its argument against a single pattern.

Lambda abstraction that matches its argument against the given alternatives.

Non-recursive expression binding.

Recursive binding of lambda abstractions.

Bind a local region variable, and witnesses to its properties.

A possibly recursive group of binding clauses.

Multiple clauses in the group may be part of the same function.

The default pattern always succeeds.

Give a name to the value matched by a pattern.

The variable pattern always succeeds and binds the value to the new variable.

Match a data constructor and bind its arguments.

A separate type signature.

A function binding using pattern matching and guards.

Type parameter with optional kind.

Witness parameter with optional type.

Value paatter with optional type.

Weaken the effect of an expression. The given effect is added to the effect of the body.

Purify the effect (action) of an expression.

Box a computation, capturing its effects in the S computation type.

Run a computation, releasing its effects into the environment.

Witness annotation

Witness variable.

Witness constructor.

Witness application.

Type can appear as an argument of a witness application.

Witness constructors defined in the environment. In the interpreter we use this to hold runtime capabilities. The attached type must be closed.

Baked in unit data constructor.

Primitive data constructor used for literals and baked-in constructors.

The type of the constructor needs to be attached to handle the case where there are too many constructors in the data type to list, like for Int literals. In this case we determine what data type it belongs to from the attached type of the data constructor.

Data constructor that has a data type declaration.