Whenever one or more variables is bound, the type checker records information from that binding to typecheck the uses of that variable in its scope. This information is stored in a typing context, which is just a sequence of variable names and their types. When an expression is in the scope of many bindings, the typechecker will carry a composite context of all of the typing contexts created by all of those bindings.

Declarations, combinators, and function calls all bind variables. Often, only a single variable is bound, so only one binding is generated. However, pattern matching may generate an entire set of variable bindings.

When a variable is typechecked, its type is found by first looking in the most recent context (i.e. from the nearest binding), and if its type is not found there, proceeding further and further out in scope. If the variable is not in the typing context, then it is a free variable, which is a syntactic error.