Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Interaction solver for Coercible constraints
Synopsis
- data GivenSolverState = GivenSolverState {
- inertGivens :: [(SourceType, SourceType, SourceType)]
- unsolvedGivens :: [(SourceType, SourceType)]
- initialGivenSolverState :: [(SourceType, SourceType)] -> GivenSolverState
- solveGivens :: MonadError MultipleErrors m => MonadState CheckState m => Environment -> StateT GivenSolverState m ()
- data WantedSolverState = WantedSolverState {
- inertGivens :: [(SourceType, SourceType, SourceType)]
- inertWanteds :: [(SourceType, SourceType, SourceType)]
- unsolvedWanteds :: [(SourceType, SourceType)]
- initialWantedSolverState :: [(SourceType, SourceType, SourceType)] -> SourceType -> SourceType -> WantedSolverState
- solveWanteds :: MonadError MultipleErrors m => MonadWriter [ErrorMessageHint] m => MonadState CheckState m => Environment -> StateT WantedSolverState m ()
- insoluble :: SourceType -> SourceType -> SourceType -> MultipleErrors
Documentation
data GivenSolverState Source #
State of the given constraints solver.
GivenSolverState | |
|
initialGivenSolverState :: [(SourceType, SourceType)] -> GivenSolverState Source #
Initialize the given constraints solver state with the givens to solve.
solveGivens :: MonadError MultipleErrors m => MonadState CheckState m => Environment -> StateT GivenSolverState m () Source #
The given constraints solver follows these steps:
- 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)
.
- 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.
- Then we try to canonicalize the constraint.
data WantedSolverState Source #
State of the wanted constraints solver.
WantedSolverState | |
|
initialWantedSolverState :: [(SourceType, SourceType, SourceType)] -> SourceType -> SourceType -> WantedSolverState Source #
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 () Source #
The wanted constraints solver follows similar steps than the given solver, except for:
- 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.
- 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 Source #