Safe Haskell	Safe-Inferred
Language	Haskell2010

Unison.KindInference.Solve.Monad

Synopsis

newtype Solve v loc a = Solve {
- unSolve :: ReaderT Env (StateT (SolveState v loc) (Except (SolveError loc))) a
}
data Env = Env {
- prettyPrintEnv :: PrettyPrintEnv
}
data SolveState v loc = SolveState {
- unifVars :: !(Set Symbol)
- newUnifVars :: [UVar v loc]
- constraints :: !(UFMap (UVar v loc) (Descriptor v loc))
- typeMap :: !(Map (Type v loc) (NonEmpty (UVar v loc)))
}
data SolveError loc = MissingBuiltin loc Reference
data Descriptor v loc = Descriptor {
- descriptorConstraint :: Maybe (Constraint (UVar v loc) v loc)
}
type ConstraintMap v loc = UFMap (UVar v loc) (Descriptor v loc)
liftGen :: Gen v loc a -> Solve v loc a
runSolve :: Env -> SolveState v loc -> Solve v loc a -> Either (SolveError loc) (a, SolveState v loc)
emptyState :: SolveState v loc
find :: Var v => UVar v loc -> Solve v loc (Maybe (Constraint (UVar v loc) v loc))
runGen :: Var v => Gen v loc a -> Solve v loc a
addUnconstrainedVar :: Var v => UVar v loc -> Solve v loc ()

Documentation

newtype Solve v loc a Source #

Constructors

Solve
Fields unSolve :: ReaderT Env (StateT (SolveState v loc) (Except (SolveError loc))) a

Instances

Instances details

MonadReader Env (Solve v loc) Source #
Instance details Defined in Unison.KindInference.Solve.Monad Methods ask :: Solve v loc Env # local :: (Env -> Env) -> Solve v loc a -> Solve v loc a # reader :: (Env -> a) -> Solve v loc a #
MonadFix (Solve v loc) Source #
Instance details Defined in Unison.KindInference.Solve.Monad Methods mfix :: (a -> Solve v loc a) -> Solve v loc a #
Applicative (Solve v loc) Source #
Instance details Defined in Unison.KindInference.Solve.Monad Methods pure :: a -> Solve v loc a # (<>) :: Solve v loc (a -> b) -> Solve v loc a -> Solve v loc b # liftA2 :: (a -> b -> c) -> Solve v loc a -> Solve v loc b -> Solve v loc c # (>) :: Solve v loc a -> Solve v loc b -> Solve v loc b # (<*) :: Solve v loc a -> Solve v loc b -> Solve v loc a #
Functor (Solve v loc) Source #
Instance details Defined in Unison.KindInference.Solve.Monad Methods fmap :: (a -> b) -> Solve v loc a -> Solve v loc b # (<$) :: a -> Solve v loc b -> Solve v loc a #
Monad (Solve v loc) Source #
Instance details Defined in Unison.KindInference.Solve.Monad Methods (>>=) :: Solve v loc a -> (a -> Solve v loc b) -> Solve v loc b # (>>) :: Solve v loc a -> Solve v loc b -> Solve v loc b # return :: a -> Solve v loc a #
MonadState (SolveState v loc) (Solve v loc) Source #
Instance details Defined in Unison.KindInference.Solve.Monad Methods get :: Solve v loc (SolveState v loc) # put :: SolveState v loc -> Solve v loc () # state :: (SolveState v loc -> (a, SolveState v loc)) -> Solve v loc a #

data Env Source #

Constructors

Env
Fields prettyPrintEnv :: PrettyPrintEnv

Instances

Instances details

MonadReader Env (Solve v loc) Source #
Instance details Defined in Unison.KindInference.Solve.Monad Methods ask :: Solve v loc Env # local :: (Env -> Env) -> Solve v loc a -> Solve v loc a # reader :: (Env -> a) -> Solve v loc a #

data SolveState v loc Source #

The SolveState holds all kind constraints gathered for each type. For example, after processing data and effect decls the typeMap will hold entries for every decl, and looking up the corresponding UVar in constraints will return its kind.

The other fields, unifVars and newUnifVars, are relevant when interleaving constraint generation with solving. Constraint generation needs to create fresh unification variables, so it needs the set of bound unification variables from unifVars. newUnifVars holds the uvars that are candidates for kind defaulting (see defaultUnconstrainedVars).

Constructors

SolveState
Fields unifVars :: !(Set Symbol) newUnifVars :: [UVar v loc] constraints :: !(UFMap (UVar v loc) (Descriptor v loc)) typeMap :: !(Map (Type v loc) (NonEmpty (UVar v loc)))

Instances

Instances details

MonadState (SolveState v loc) (Solve v loc) Source #
Instance details Defined in Unison.KindInference.Solve.Monad Methods get :: Solve v loc (SolveState v loc) # put :: SolveState v loc -> Solve v loc () # state :: (SolveState v loc -> (a, SolveState v loc)) -> Solve v loc a #

data SolveError loc Source #

Constructors

MissingBuiltin loc Reference

Instances

Instances details

Show loc => Show (SolveError loc) Source #
Instance details Defined in Unison.KindInference.Solve.Monad Methods showsPrec :: Int -> SolveError loc -> ShowS # show :: SolveError loc -> String # showList :: [SolveError loc] -> ShowS #
Eq loc => Eq (SolveError loc) Source #
Instance details Defined in Unison.KindInference.Solve.Monad Methods (==) :: SolveError loc -> SolveError loc -> Bool # (/=) :: SolveError loc -> SolveError loc -> Bool #

data Descriptor v loc Source #

Constraints associated with a unification variable

Constructors

Descriptor
Fields descriptorConstraint :: Maybe (Constraint (UVar v loc) v loc)

type ConstraintMap v loc = UFMap (UVar v loc) (Descriptor v loc) Source #

liftGen :: Gen v loc a -> Solve v loc a Source #

runSolve :: Env -> SolveState v loc -> Solve v loc a -> Either (SolveError loc) (a, SolveState v loc) Source #

Runner for the Solve monad

emptyState :: SolveState v loc Source #

Initial solve state

find :: Var v => UVar v loc -> Solve v loc (Maybe (Constraint (UVar v loc) v loc)) Source #

Lookup the constraints associated with a unification variable

runGen :: Var v => Gen v loc a -> Solve v loc a Source #

Interleave constraint generation into constraint solving

addUnconstrainedVar :: Var v => UVar v loc -> Solve v loc () Source #

Add a unification variable to the constarint mapping with no constraints. This is done on uvars created during constraint generation to initialize the new uvars (see runGen).