Safe Haskell | Safe-Inferred |
---|---|

Language | GHC2021 |

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