Documentation

Information needed for type inference.

The results of type inference.

This is used for generating various names.

Read-write component of the monad.

Read-only component of the monad.

Do we allow wild cards in the given context.

This is what's returned when we lookup variables during kind checking.

The monadic computation is about the given range of source code. This is useful for error reporting.

Generate a new free type variable.

Perform the given computation in a new scope (i.e., the subcomputation may use existential type variables). This is a different kind of scope from the nested modules one.

Retrieve the mapping between identifiers and declarations in the prelude.

Get information about the things defined in the module. Note that, in general, the interface may contain *more* than just the definitions in the module, however the ifNames should indicate which ones are part of the module.

The initial seeds, used when checking a fresh program. XXX: why does this start at 10?

Lookup the type of a variable.

Record that the two types should be syntactically equal.

Record some constraints that need to be solved. The string explains where the constraints came from.

Generate an unknown type. The doc is a note about what is this type about.

Apply the accumulated substitution to something with free type variables.

Specify the solution (Expr -> Expr) for the given constraint (Int).

Generate a fresh variable name to be used in a local binding.

This is the current range that we are working on.

Report an error.

This introduces a new "selector scope" which is currently a module. I think that it might be possible to have selectors scopes be groups of recursive declarations instead, as we are not going to learn anything additional once we are done with the recursive group that generated the selectors constraints. We do it at the module level because this allows us to report more errors at once.

A selector scope does the following: * Keep track of the Has constraints generated in this scope * Keep track of the solutions for discharged selector constraints: - this uses a laziness trick where we build up a map containing the solutions for the Has constraints in the state - the *final* value for this map (i.e., at the value the end of the scope) is passed in as thunk in the reader component of the moment - as we type check expressions when we need the solution for a Has constraint we look it up from the reader environment; note that since the map is not yet built up we just get back a thunk, so we have to be carefule to not force it until *after* we've solved the goals - all of this happens in the `rec` block below * At the end of a selector scope we make sure that all Has constraints were discharged. If not, we *abort* further type checking. The reason for aborting rather than just recording an error is that the expression which produce contains thunks that will lead to non-termination if forced, and some type-checking operations (e.g., instantiation a functor) require us to traverse the expressions.

If there are any recoded errors than abort firther type-checking.

Report an error.

Add a bunch of goals that need solving.

The constraints are removed, and returned to the caller. The substitution IS applied to them.

Collect the goals emitted by the given sub-computation. Does not emit any new goals.

Record a constraint that when we select from the first type, we should get a value of the second type. The returned function should be used to wrap the expression from which we are selecting (i.e., the record or tuple). Plese note that the resulting expression should not be forced before the constraint is solved.

Generate a new name for a goal.

Add a previously generated Has constraint

Get the Has constraints. Each of this should either be solved, or added back using addHasGoal.

Generate a new free type variable that depends on these additional type parameters.

Return the keys of the bound variables that are in scope.

Check that the given "flavor" of parameter is allowed to have the given type, and raise an error if not

Generate a new free type variable.

Generate a new version of a type parameter. We use this when instantiating module parameters (the "backtick" imports)

Add to the accumulated substitution, checking that the datatype invariant for Subst is maintained.

Get the substitution that we have accumulated so far.

Variables that are either mentioned in the environment or in a selector constraint.

Lookup a type variable. Return Nothing if there is no such variable in scope, in which case we must be dealing with a type constant.

Lookup the definition of a type synonym.

Returns the type synonyms that are currently in scope.

Lookup the definition of a nominal type

Returns the nominal type declarations that are in scope.

Lookup the kind of a parameter type

Returns the abstract function declarations

Lookup an external (i.e., previously loaded) top module.

Get an environment combining all nested scopes.

Check if we already have a name for this existential type variable and, if so, return the definition. If not, try to create a new definition, if this is allowed. If not, returns nothing.

Constraints on the module's parameters.

Get the set of bound type variables that are in scope.

Retrieve the value of the `mono-binds` option.

We disallow shadowing between type synonyms and type variables because it is confusing. As a bonus, in the implementation we don't need to worry about where we lookup things (i.e., in the variable or type synonym environment.

The sub-computation is performed with the given type parameter in scope.

Execute the given computation in a new top scope. The sub-computation would typically be validating a module.

Update the current scope (first in the list). Assumes there is one.

Start a new submodule scope. The imports and exports are just used to initialize an empty module. As we type check declarations they are added to this module's scope.

The sub-computation is performed with the given type-synonym in scope.

The sub-computation is performed with the given abstract function in scope.

Add some assumptions for an entire module

The sub-computation is performed with the given variable in scope.

The sub-computation is performed with the given variables in scope.

The sub-computation is performed with the given variables in scope.

The arguments to this function are as follows:

(type param. name, kind signature (opt.), type parameter)

The type parameter is just a thunk that we should not force. The reason is that the parameter depends on the kind that we are in the process of computing.

As a result we return the value of the sub-computation and the computed kinds of the type parameters.

Check if a name refers to a type variable.

Are type wild-cards OK in this context?

Reports an error.

Generate a fresh unification variable of the given kind. NOTE: We do not simplify these, because we end up with bottom. See hs XXX: Perhaps we can avoid the recursion?

Lookup the definition of a type synonym.

Lookup the definition of a nominal type.

Replace the given bound variables with concrete types.

Record the kind for a local type variable. This assumes that we already checked that there was no other valid kind for the variable (if there was one, it gets over-written).

The sub-computation is about the given range of the source code.