purescript-0.11.2: PureScript Programming Language Compiler

Language.PureScript.TypeChecker.Skolems

Description

Functions relating to skolemization used during typechecking

Synopsis

# Documentation

Generate a new skolem constant

Introduce skolem scope at every occurence of a ForAll

Generate a new skolem scope

Skolemize a type variable by replacing its instances with fresh skolem constants

This function skolemizes type variables appearing in any type signatures or DeferredDictionary placeholders. These type variables are the only places where scoped type variables can appear in expressions.

skolemEscapeCheck :: MonadError MultipleErrors m => Expr -> m () Source #

Ensure skolem variables do not escape their scope

Every skolem variable is created when a ForAll type is skolemized. This determines the scope of that skolem variable, which is copied from the SkolemScope field of the ForAll constructor.

This function traverses the tree top-down, and collects any SkolemScopes introduced by ForAlls. If a Skolem is encountered whose SkolemScope is not in the current list, then we have found an escaped skolem variable.