giml-language-0.1.0.0: A purely functional programming language with emphasis on structural typing
Safe HaskellSafe-Inferred
LanguageGHC2021

Language.Giml.Types.Infer.Solve

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 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

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