A solver type is an abstraction, implemented using a combination of a private representation type and a constraint store.
The constraint store is an (impure) piece of state used to keep track of the extant constraints on variables of the solver type. This will typically be implemented using foreign code.
It is important that changes to the constraint store are properly trailed (see Trailing) so that changes can be undone on backtracking.
The solver type implementation should provide functions and predicates
anysolver type variables to
groundif possible (this is obviously an impure operation — see Impurity),