Language.PureScript.TypeChecker.Entailment.Coercible

Interaction solver for Coercible constraints

Documentation

data GivenSolverState

State of the given constraints solver.

Constructors

GivenSolverState

Fields

• inertGivens :: [(SourceType, SourceType, SourceType)]

  A set of irreducible given constraints which do not interact together.

• unsolvedGivens :: [(SourceType, SourceType)]

  Given constraints yet to be solved.

initialGivenSolverState :: [(SourceType, SourceType)] -> GivenSolverState

Initialize the given constraints solver state with the givens to solve.

solveGivens :: MonadError MultipleErrors m => MonadState CheckState m => Environment -> StateT GivenSolverState m ()

The given constraints solver follows these steps:

1. Solving can diverge for recursive newtypes, so we check the solver depth and abort if we crossed an arbitrary limit.

For instance the declarations:

newtype N a = N (a -> N a)

example :: forall a b. N a -> N b
example = coerce

yield the wanted Coercible (N a) (N b) which we can unwrap on both sides to yield Coercible (a -> N a) (b -> N b), which we can then decompose back to Coercible a b and Coercible (N a) (N b).

1. We pick a constraint from the unsolved queue. If the queue is empty we are done, otherwise we unify the constraint arguments kinds and continue.
2. Then we try to canonicalize the constraint.

data WantedSolverState

State of the wanted constraints solver.

Constructors

WantedSolverState

Fields

• inertGivens :: [(SourceType, SourceType, SourceType)]

  A set of irreducible given constraints which do not interact together, but which could interact with the wanteds.

• inertWanteds :: [(SourceType, SourceType, SourceType)]

  A set of irreducible wanted constraints which do not interact together, nor with any given.

• unsolvedWanteds :: [(SourceType, SourceType)]

  Wanted constraints yet to be solved.

initialWantedSolverState :: [(SourceType, SourceType, SourceType)] -> SourceType -> SourceType -> WantedSolverState

Initialize the wanted constraints solver state with an inert set of givens and the two parameters of the wanted to solve.

solveWanteds :: MonadError MultipleErrors m => MonadWriter [ErrorMessageHint] m => MonadState CheckState m => Environment -> StateT WantedSolverState m ()

The wanted constraints solver follows similar steps than the given solver, except for:

1. When canonicalization fails we can swallow the error, but only if the wanted interacts with the givens.

For instance the declarations:

data D a = D a
type role D nominal

example :: forall a b. Coercible (D a) (D b) => D a -> D b
example = coerce

yield an insoluble wanted Coercible (D a) (D b) which is discharged by the given. But we want example :: forall a b. D a -> D b to fail.

1. Irreducible wanted constraints don't interact with the inert wanteds set, because doing so would yield confusing error messages.

For instance the declarations:

data D a = D a

example :: forall a. D a a -> D Boolean Char
example = coerce

yield the wanted Coercible (D a a) (D Boolean Char), which is decomposed to the irreducibles Coercible a Boolean and Coercible a Char. Would we interact the latter with the former, we would report an insoluble Coercible Boolean Char.

insoluble :: SourceType -> SourceType -> SourceType -> MultipleErrors