Check scoping rules and naming conventions for identifiers.

Here, we ensure that all identifiers that appear in the AST only appear after they are previously declared or defined.

Identifiers can be segregated into two categories: data identifiers, which produce expressions, and type identifiers, which produce types (more accurately, type expressions). These inhabit separate namespaces and are distinguished by the different contexts in which they are used.

Of each category, there are two kinds of identifiers: constructors and variables. Constructors must begin with an upper case letter or a colon (:); all other identifiers are variables (see isCons and isVar). For instance, data constructors name the variants of an algebraic data type, while data variables name values bound by a let-binding, a pattern-match, or a lambda. Meanwhile, type constructors are points in the type system defined by the user, while type variables are universally quantified in each type expression.

Consider the following example:

@@ type Bool = True False

type Either t u = Left t Right u

liftEither b x y: Bool -> a -> b -> Either a b = match b True = Left x False = Right y @@

Data variables are switch, b, x, and y; data constructors are True, False, Left, and Right. Type variables are t, u, a, and b; type constructors are Bool and Either.

The grammar as it appears in the parser does not actually distinguish between any of these kinds of identifiers, so it is the responsibility of this module to check that, a data constructor does not appear where a data variable is expected, e.g., let F x = e, or vice versa, e.g., let f (x Y) = e.