Language.PureScript.TypeChecker.Monad

Monads for type checking and type inference and associated data types

Documentation

newtype UnkLevel

Constructors

UnkLevel (NonEmpty Unknown)

Instances

Show UnkLevel

Defined in Language.PureScript.TypeChecker.Monad

Methods

showsPrec :: Int -> UnkLevel -> ShowS

show :: UnkLevel -> String

showList :: [UnkLevel] -> ShowS

Eq UnkLevel

Defined in Language.PureScript.TypeChecker.Monad

Methods

(==) :: UnkLevel -> UnkLevel -> Bool

(/=) :: UnkLevel -> UnkLevel -> Bool

Ord UnkLevel

Defined in Language.PureScript.TypeChecker.Monad

Methods

compare :: UnkLevel -> UnkLevel -> Ordering

(<) :: UnkLevel -> UnkLevel -> Bool

(<=) :: UnkLevel -> UnkLevel -> Bool

(>) :: UnkLevel -> UnkLevel -> Bool

(>=) :: UnkLevel -> UnkLevel -> Bool

max :: UnkLevel -> UnkLevel -> UnkLevel

min :: UnkLevel -> UnkLevel -> UnkLevel

data Substitution

A substitution of unification variables for types.

Constructors

Substitution

Fields

• substType :: Map Int SourceType

  Type substitution

• substUnsolved :: Map Int (UnkLevel, SourceType)

  Unsolved unification variables with their level (scope ordering) and kind

• substNames :: Map Int Text

  The original names of unknowns

insertUnkName :: MonadState CheckState m => Unknown -> Text -> m ()

lookupUnkName :: MonadState CheckState m => Unknown -> m (Maybe Text)

emptySubstitution :: Substitution

An empty substitution

data CheckState

State required for type checking

Constructors

CheckState

Fields

• checkEnv :: Environment

  The current Environment

• checkNextType :: Int

  The next type unification variable

• checkNextSkolem :: Int

  The next skolem variable

• checkNextSkolemScope :: Int

  The next skolem scope constant

• checkCurrentModule :: Maybe ModuleName

  The current module

• checkCurrentModuleImports :: [(SourceAnn, ModuleName, ImportDeclarationType, Maybe ModuleName, Map (ProperName 'TypeName) ([ProperName 'ConstructorName], ExportSource))]

  The current module imports and their exported types. Newtype constructors have to be in scope for some Coercible constraints to be solvable, so we need to know which constructors are imported and whether they are actually defined in or re-exported from the imported modules.

• checkSubstitution :: Substitution

  The current substitution

• checkHints :: [ErrorMessageHint]

  The current error message hint stack. This goes into state, rather than using rethrow, since this way, we can provide good error messages during instance resolution.

• checkConstructorImportsForCoercible :: Set (ModuleName, Qualified (ProperName 'ConstructorName))

  Newtype constructors imports required to solve Coercible constraints. We have to keep track of them so that we don't emit unused import warnings.

emptyCheckState :: Environment -> CheckState

Create an empty CheckState

type Unknown = Int

Unification variables

bindNames :: MonadState CheckState m => Map (Qualified Ident) (SourceType, NameKind, NameVisibility) -> m a -> m a

Temporarily bind a collection of names to values

bindTypes :: MonadState CheckState m => Map (Qualified (ProperName 'TypeName)) (SourceType, TypeKind) -> m a -> m a

Temporarily bind a collection of names to types

withScopedTypeVars :: (MonadState CheckState m, MonadWriter MultipleErrors m) => ModuleName -> [(Text, SourceType)] -> m a -> m a

Temporarily bind a collection of names to types

withErrorMessageHint :: (MonadState CheckState m, MonadError MultipleErrors m) => ErrorMessageHint -> m a -> m a

getHints :: MonadState CheckState m => m [ErrorMessageHint]

These hints are added at the front, so the most nested hint occurs at the front, but the simplifier assumes the reverse order.

rethrowWithPositionTC :: (MonadState CheckState m, MonadError MultipleErrors m) => SourceSpan -> m a -> m a

warnAndRethrowWithPositionTC :: (MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) => SourceSpan -> m a -> m a

withTypeClassDictionaries :: MonadState CheckState m => [NamedDict] -> m a -> m a

Temporarily make a collection of type class dictionaries available

getTypeClassDictionaries :: MonadState CheckState m => m (Map QualifiedBy (Map (Qualified (ProperName 'ClassName)) (Map (Qualified Ident) (NonEmpty NamedDict))))

Get the currently available map of type class dictionaries

lookupTypeClassDictionaries :: MonadState CheckState m => QualifiedBy -> m (Map (Qualified (ProperName 'ClassName)) (Map (Qualified Ident) (NonEmpty NamedDict)))

Lookup type class dictionaries in a module.

lookupTypeClassDictionariesForClass :: MonadState CheckState m => QualifiedBy -> Qualified (ProperName 'ClassName) -> m (Map (Qualified Ident) (NonEmpty NamedDict))

Lookup type class dictionaries in a module.

bindLocalVariables :: MonadState CheckState m => [(SourceSpan, Ident, SourceType, NameVisibility)] -> m a -> m a

Temporarily bind a collection of names to local variables

bindLocalTypeVariables :: MonadState CheckState m => ModuleName -> [(ProperName 'TypeName, SourceType)] -> m a -> m a

Temporarily bind a collection of names to local type variables

makeBindingGroupVisible :: MonadState CheckState m => m ()

Update the visibility of all names to Defined

withBindingGroupVisible :: MonadState CheckState m => m a -> m a

Update the visibility of all names to Defined in the scope of the provided action

preservingNames :: MonadState CheckState m => m a -> m a

Perform an action while preserving the names from the Environment.

lookupVariable :: (e ~ MultipleErrors, MonadState CheckState m, MonadError e m) => Qualified Ident -> m SourceType

Lookup the type of a value by name in the Environment

getVisibility :: (e ~ MultipleErrors, MonadState CheckState m, MonadError e m) => Qualified Ident -> m NameVisibility

Lookup the visibility of a value by name in the Environment

checkVisibility :: (e ~ MultipleErrors, MonadState CheckState m, MonadError e m) => Qualified Ident -> m ()

Assert that a name is visible

lookupTypeVariable :: (e ~ MultipleErrors, MonadState CheckState m, MonadError e m) => ModuleName -> Qualified (ProperName 'TypeName) -> m SourceType

Lookup the kind of a type by name in the Environment

getEnv :: MonadState CheckState m => m Environment

Get the current Environment

getLocalContext :: MonadState CheckState m => m Context

Get locally-bound names in context, to create an error message.

putEnv :: MonadState CheckState m => Environment -> m ()

Update the Environment

modifyEnv :: MonadState CheckState m => (Environment -> Environment) -> m ()

Modify the Environment

runCheck :: Functor m => CheckState -> StateT CheckState m a -> m (a, Environment)

Run a computation in the typechecking monad, failing with an error, or succeeding with a return value and the final Environment.

guardWith :: MonadError e m => e -> Bool -> m ()

Make an assertion, failing with an error message

capturingSubstitution :: MonadState CheckState m => (a -> Substitution -> b) -> m a -> m b

withFreshSubstitution :: MonadState CheckState m => m a -> m a

withoutWarnings :: MonadWriter w m => m a -> m (a, w)

unsafeCheckCurrentModule :: forall m. (MonadError MultipleErrors m, MonadState CheckState m) => m ModuleName

debugEnv :: Environment -> [String]

debugType :: Type a -> String

debugConstraint :: Constraint a -> String

debugTypes :: Environment -> [String]

debugNames :: Environment -> [String]

debugDataConstructors :: Environment -> [String]

debugTypeSynonyms :: Environment -> [String]

debugTypeClassDictionaries :: Environment -> [String]

debugTypeClasses :: Environment -> [String]

debugValue :: Expr -> String

debugSubstitution :: Substitution -> [String]