purescript-0.11.7: PureScript Programming Language Compiler

Safe HaskellNone
LanguageHaskell2010

Language.PureScript.TypeChecker.Skolems

Description

Functions relating to skolemization used during typechecking

Synopsis

Documentation

newSkolemConstant :: MonadState CheckState m => m Int Source #

Generate a new skolem constant

introduceSkolemScope :: MonadState CheckState m => Type -> m Type Source #

Introduce skolem scope at every occurence of a ForAll

newSkolemScope :: MonadState CheckState m => m SkolemScope Source #

Generate a new skolem scope

skolemize :: Text -> Int -> SkolemScope -> Maybe SourceSpan -> Type -> Type Source #

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

skolemizeTypesInValue :: Text -> Int -> SkolemScope -> Maybe SourceSpan -> Expr -> Expr Source #

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.