purescript- PureScript Programming Language Compiler

Safe HaskellNone



Functions relating to skolemization used during typechecking



newSkolemConstant :: MonadState CheckState m => m Int Source

Generate a new skolem constant

introduceSkolemScope :: (Functor m, Applicative m, 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 :: String -> Int -> SkolemScope -> Maybe SourceSpan -> Type -> Type Source

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

skolemizeTypesInValue :: String -> Int -> SkolemScope -> Maybe SourceSpan -> Expr -> Expr Source

This function has one purpose - to skolemize type variables appearing in a SuperClassDictionary placeholder. These type variables are somewhat unique since they are the only example of scoped type variables.

skolemEscapeCheck :: (MonadError MultipleErrors m, MonadState CheckState m) => Expr -> m () Source

Ensure skolem variables do not escape their scope