| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Language.PureScript.TypeChecker.Skolems
Description
Functions relating to skolemization used during typechecking
- newSkolemConstant :: MonadState CheckState m => m Int
- introduceSkolemScope :: MonadState CheckState m => Type -> m Type
- newSkolemScope :: MonadState CheckState m => m SkolemScope
- skolemize :: Text -> Int -> SkolemScope -> Maybe SourceSpan -> Type -> Type
- skolemizeTypesInValue :: Text -> Int -> SkolemScope -> Maybe SourceSpan -> Expr -> Expr
- skolemEscapeCheck :: MonadError MultipleErrors m => Expr -> m ()
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.