Safe Haskell | Safe-Inferred |
---|---|
Language | GHC2021 |
Language.Giml.Types.Infer.Solve
Contents
Description
Solve type inference constraints
In this phase we go over the constraints one by one and try to unify them.
For example, if we see Equality (TypeVar "t1") (TypeCon Int)
, we create
a mapping from t1
to Int
(called a substitution) and
we go over the rest of the constraints and replace t1
with Int
(apply the substitution).
We also keep all the substitutions we created from the constraints (and merge them to one substitution but applying new substitution to the accumulated substitution).
If we see Equality (TypeCon Int) (TypeCon String)
, we throw a type error,
because the two types do not match.
We keep going until there are no more constraints or until we encountered an error.
The result of the algorithm is the accumulated substitution.
Synopsis
- solve :: MonadBase b b => LogAction b LogMsg -> Int -> Constraints -> ExceptT TypeErrorA b (Substitution, Int)
- type Solve b m = (MonadBase b m, MonadError TypeErrorA m, MonadState ElabState m, MonadReader (ElabEnv b) m)
- runSolve :: MonadBase b b => LogAction b LogMsg -> Int -> Constraints -> ExceptT TypeErrorA b (Substitution, Int)
- solveConstraints :: Solve b m => Substitution -> [ConstraintA] -> m Substitution
- solveConstraint :: Solve b m => ConstraintA -> m ([ConstraintA], Substitution)
Solve constraints
solve :: MonadBase b b => LogAction b LogMsg -> Int -> Constraints -> ExceptT TypeErrorA b (Substitution, Int) Source #
Run constraint solving algorithm
Types
type Solve b m = (MonadBase b m, MonadError TypeErrorA m, MonadState ElabState m, MonadReader (ElabEnv b) m) Source #
Monadic capabilities for the Solve algorithm
Algorithm
runSolve :: MonadBase b b => LogAction b LogMsg -> Int -> Constraints -> ExceptT TypeErrorA b (Substitution, Int) Source #
solveConstraints :: Solve b m => Substitution -> [ConstraintA] -> m Substitution Source #
Recursively the constraints in order, passing the accumulated substitution.
solveConstraint :: Solve b m => ConstraintA -> m ([ConstraintA], Substitution) Source #
Solve a constraint. Returns new constraints that may arise from this constraint and a substitution