| Copyright | disco team and contributors |
|---|---|
| License | BSD-3-Clause |
| Maintainer | byorgey@gmail.com |
| Safe Haskell | None |
| Language | Haskell2010 |
Disco.Typecheck.Solve
Description
Constraint solver for the constraints generated during type checking/inference.
Synopsis
- data SolveError where
- NoWeakUnifier :: SolveError
- NoUnify :: SolveError
- UnqualBase :: Qualifier -> BaseTy -> SolveError
- Unqual :: Qualifier -> Type -> SolveError
- QualSkolem :: Qualifier -> Name Type -> SolveError
- runSolve :: Sem (Fresh ': (Error SolveError ': r)) a -> Sem r (Either SolveError a)
- filterErrors :: Member (Error e) r => [Sem r a] -> Sem r [a]
- asum' :: Member (Error e) r => [Sem r a] -> Sem r a
- data SimpleConstraint where
- (:<:) :: Type -> Type -> SimpleConstraint
- (:=:) :: Type -> Type -> SimpleConstraint
- data TyVarInfo = TVI {
- _tyVarIlk :: First Ilk
- _tyVarSort :: Sort
- tyVarSort :: Lens' TyVarInfo Sort
- tyVarIlk :: Lens' TyVarInfo (First Ilk)
- mkTVI :: Ilk -> Sort -> TyVarInfo
- newtype TyVarInfoMap = VM {}
- onVM :: (Map (Name Type) TyVarInfo -> Map (Name Type) TyVarInfo) -> TyVarInfoMap -> TyVarInfoMap
- lookupVM :: Name Type -> TyVarInfoMap -> Maybe TyVarInfo
- deleteVM :: Name Type -> TyVarInfoMap -> TyVarInfoMap
- addSkolems :: [Name Type] -> TyVarInfoMap -> TyVarInfoMap
- getSort :: TyVarInfoMap -> Name Type -> Sort
- getIlk :: TyVarInfoMap -> Name Type -> Maybe Ilk
- extendSort :: Name Type -> Sort -> TyVarInfoMap -> TyVarInfoMap
- data SimplifyState = SS {}
- ssVarMap :: Lens' SimplifyState TyVarInfoMap
- ssSubst :: Lens' SimplifyState S
- ssSeen :: Lens' SimplifyState (Set SimpleConstraint)
- ssConstraints :: Lens' SimplifyState [SimpleConstraint]
- lkup :: (Ord k, Show k, Show (Map k a)) => String -> Map k a -> k -> a
- solveConstraint :: Members '[Fresh, Error SolveError, Output Message, Input TyDefCtx] r => Constraint -> Sem r S
- solveConstraintChoice :: Members '[Fresh, Error SolveError, Output Message, Input TyDefCtx] r => TyVarInfoMap -> [SimpleConstraint] -> Sem r S
- decomposeConstraint :: Members '[Fresh, Error SolveError, Input TyDefCtx] r => Constraint -> Sem r [(TyVarInfoMap, [SimpleConstraint])]
- decomposeQual :: Members '[Fresh, Error SolveError, Input TyDefCtx] r => Type -> Qualifier -> Sem r TyVarInfoMap
- checkQual :: Members '[Fresh, Error SolveError] r => Qualifier -> Atom -> Sem r TyVarInfoMap
- simplify :: Members '[Error SolveError, Output Message, Input TyDefCtx] r => TyVarInfoMap -> [SimpleConstraint] -> Sem r (TyVarInfoMap, [(Atom, Atom)], S)
- mkConstraintGraph :: (Show a, Ord a) => Set a -> [(a, a)] -> Graph a
- checkSkolems :: Members '[Error SolveError, Output Message, Input TyDefCtx] r => TyVarInfoMap -> Graph Atom -> Sem r (Graph UAtom, S)
- elimCycles :: Members '[Error SolveError] r => TyDefCtx -> Graph UAtom -> Sem r (Graph UAtom, S)
- elimCyclesGen :: forall a b r. (Subst a a, Ord a, Members '[Error SolveError] r) => (Substitution a -> Substitution b) -> ([a] -> Maybe (Substitution a)) -> Graph a -> Sem r (Graph a, Substitution b)
- data Rels = Rels {}
- newtype RelMap = RelMap {}
- substRel :: Name Type -> BaseTy -> RelMap -> RelMap
- dirtypesBySort :: TyVarInfoMap -> RelMap -> Dir -> BaseTy -> Sort -> Set (Name Type) -> [BaseTy]
- limBySort :: TyVarInfoMap -> RelMap -> Dir -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy
- lubBySort :: TyVarInfoMap -> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy
- glbBySort :: TyVarInfoMap -> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy
- solveGraph :: Members '[Fresh, Error SolveError, Output Message] r => TyVarInfoMap -> Graph UAtom -> Sem r S
Documentation
data SolveError where Source #
Type of errors which can be generated by the constraint solving process.
Constructors
| NoWeakUnifier :: SolveError | |
| NoUnify :: SolveError | |
| UnqualBase :: Qualifier -> BaseTy -> SolveError | |
| Unqual :: Qualifier -> Type -> SolveError | |
| QualSkolem :: Qualifier -> Name Type -> SolveError |
Instances
| Show SolveError Source # | |
Defined in Disco.Typecheck.Solve Methods showsPrec :: Int -> SolveError -> ShowS # show :: SolveError -> String # showList :: [SolveError] -> ShowS # | |
| Semigroup SolveError Source # | |
Defined in Disco.Typecheck.Solve Methods (<>) :: SolveError -> SolveError -> SolveError # sconcat :: NonEmpty SolveError -> SolveError # stimes :: Integral b => b -> SolveError -> SolveError # | |
runSolve :: Sem (Fresh ': (Error SolveError ': r)) a -> Sem r (Either SolveError a) Source #
filterErrors :: Member (Error e) r => [Sem r a] -> Sem r [a] Source #
Run a list of actions, and return the results from those which do not throw an error. If all of them throw an error, rethrow the first one.
asum' :: Member (Error e) r => [Sem r a] -> Sem r a Source #
A variant of asum which picks the first action that succeeds,
or re-throws the error of the last one if none of them
do. Precondition: the list must not be empty.
data SimpleConstraint where Source #
Constructors
| (:<:) :: Type -> Type -> SimpleConstraint | |
| (:=:) :: Type -> Type -> SimpleConstraint |
Instances
Information about a particular type variable. More information may be added in the future (e.g. polarity).
Constructors
| TVI | |
Fields
| |
newtype TyVarInfoMap Source #
A TyVarInfoMap records what we know about each type variable;
it is a mapping from type variable names to TyVarInfo records.
Instances
| Show TyVarInfoMap Source # | |
Defined in Disco.Typecheck.Solve Methods showsPrec :: Int -> TyVarInfoMap -> ShowS # show :: TyVarInfoMap -> String # showList :: [TyVarInfoMap] -> ShowS # | |
| Semigroup TyVarInfoMap Source # | The |
Defined in Disco.Typecheck.Solve Methods (<>) :: TyVarInfoMap -> TyVarInfoMap -> TyVarInfoMap # sconcat :: NonEmpty TyVarInfoMap -> TyVarInfoMap # stimes :: Integral b => b -> TyVarInfoMap -> TyVarInfoMap # | |
| Monoid TyVarInfoMap Source # | |
Defined in Disco.Typecheck.Solve Methods mempty :: TyVarInfoMap # mappend :: TyVarInfoMap -> TyVarInfoMap -> TyVarInfoMap # mconcat :: [TyVarInfoMap] -> TyVarInfoMap # | |
| Pretty TyVarInfoMap Source # | |
onVM :: (Map (Name Type) TyVarInfo -> Map (Name Type) TyVarInfo) -> TyVarInfoMap -> TyVarInfoMap Source #
Utility function for acting on a TyVarInfoMap by acting on the
underlying Map.
lookupVM :: Name Type -> TyVarInfoMap -> Maybe TyVarInfo Source #
Look up a given variable name in a TyVarInfoMap.
deleteVM :: Name Type -> TyVarInfoMap -> TyVarInfoMap Source #
Remove the mapping for a particular variable name (if it exists)
from a TyVarInfoMap.
addSkolems :: [Name Type] -> TyVarInfoMap -> TyVarInfoMap Source #
Given a list of type variable names, add them all to the
TyVarInfoMap as Skolem variables (with a trivial sort).
getSort :: TyVarInfoMap -> Name Type -> Sort Source #
Get the sort of a particular variable recorded in a
TyVarInfoMap. Returns the trivial (empty) sort for a variable
not in the map.
getIlk :: TyVarInfoMap -> Name Type -> Maybe Ilk Source #
Get the Ilk of a variable recorded in a TyVarInfoMap.
Returns Nothing if the variable is not in the map, or if its
ilk is not known.
extendSort :: Name Type -> Sort -> TyVarInfoMap -> TyVarInfoMap Source #
Extend the sort of a type variable by combining its existing sort with the given one. Has no effect if the variable is not already in the map.
data SimplifyState Source #
Constructors
| SS | |
Fields
| |
solveConstraint :: Members '[Fresh, Error SolveError, Output Message, Input TyDefCtx] r => Constraint -> Sem r S Source #
solveConstraintChoice :: Members '[Fresh, Error SolveError, Output Message, Input TyDefCtx] r => TyVarInfoMap -> [SimpleConstraint] -> Sem r S Source #
decomposeConstraint :: Members '[Fresh, Error SolveError, Input TyDefCtx] r => Constraint -> Sem r [(TyVarInfoMap, [SimpleConstraint])] Source #
decomposeQual :: Members '[Fresh, Error SolveError, Input TyDefCtx] r => Type -> Qualifier -> Sem r TyVarInfoMap Source #
checkQual :: Members '[Fresh, Error SolveError] r => Qualifier -> Atom -> Sem r TyVarInfoMap Source #
simplify :: Members '[Error SolveError, Output Message, Input TyDefCtx] r => TyVarInfoMap -> [SimpleConstraint] -> Sem r (TyVarInfoMap, [(Atom, Atom)], S) Source #
This step does unification of equality constraints, as well as structural decomposition of subtyping constraints. For example, if we have a constraint (x -> y) (z - Int), then we can decompose it into two constraints, (z <: x) and (y <: Int); if we have a constraint v <: (a,b), then we substitute v ↦ (x,y) (where x and y are fresh type variables) and continue; and so on.
After this step, the remaining constraints will all be atomic constraints, that is, only of the form (v1 <: v2), (v <: b), or (b <: v), where v is a type variable and b is a base type.
mkConstraintGraph :: (Show a, Ord a) => Set a -> [(a, a)] -> Graph a Source #
Given a list of atoms and atomic subtype constraints (each pair
(a1,a2) corresponds to the constraint a1 <: a2) build the
corresponding constraint graph.
checkSkolems :: Members '[Error SolveError, Output Message, Input TyDefCtx] r => TyVarInfoMap -> Graph Atom -> Sem r (Graph UAtom, S) Source #
Check for any weakly connected components containing more than one skolem, or a skolem and a base type, or a skolem and any variables with nontrivial sorts; such components are not allowed. If there are any WCCs with a single skolem, no base types, and only unsorted variables, just unify them all with the skolem and remove those components.
elimCycles :: Members '[Error SolveError] r => TyDefCtx -> Graph UAtom -> Sem r (Graph UAtom, S) Source #
Eliminate cycles in the constraint set by collapsing each strongly connected component to a single node, (unifying all the types in the SCC). A strongly connected component is a maximal set of nodes where every node is reachable from every other by a directed path; since we are using directed edges to indicate a subtyping constraint, this means every node must be a subtype of every other, and the only way this can happen is if all are in fact equal.
Of course, this step can fail if the types in a SCC are not unifiable. If it succeeds, it returns the collapsed graph (which is now guaranteed to be acyclic, i.e. a DAG) and a substitution.
elimCyclesGen :: forall a b r. (Subst a a, Ord a, Members '[Error SolveError] r) => (Substitution a -> Substitution b) -> ([a] -> Maybe (Substitution a)) -> Graph a -> Sem r (Graph a, Substitution b) Source #
Rels stores the set of base types and variables related to a given variable in the constraint graph (either predecessors or successors, but not both).
A RelMap associates each variable to its sets of base type and variable predecessors and successors in the constraint graph.
substRel :: Name Type -> BaseTy -> RelMap -> RelMap Source #
Modify a RelMap to record the fact that we have solved for a
type variable. In particular, delete the variable from the
RelMap as a key, and also update the relative sets of every
other variable to remove this variable and add the base type we
chose for it.
dirtypesBySort :: TyVarInfoMap -> RelMap -> Dir -> BaseTy -> Sort -> Set (Name Type) -> [BaseTy] Source #
Essentially dirtypesBySort vm rm dir t s x finds all the dir-types (sub- or super-) of t which have sort s, relative to the variables in x. This is overbar{T}_S^X (resp. underbar...) from Traytel et al.
limBySort :: TyVarInfoMap -> RelMap -> Dir -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy Source #
Sort-aware infimum or supremum.
solveGraph :: Members '[Fresh, Error SolveError, Output Message] r => TyVarInfoMap -> Graph UAtom -> Sem r S Source #
From the constraint graph, build the sets of sub- and super- base types of each type variable, as well as the sets of sub- and supertype variables. For each type variable x in turn, try to find a common supertype of its base subtypes which is consistent with the sort of x and with the sorts of all its sub-variables, as well as symmetrically a common subtype of its supertypes, etc. Assign x one of the two: if it has only successors, assign it their inf; otherwise, assign it the sup of its predecessors. If it has both, we have a choice of whether to assign it the sup of predecessors or inf of successors; both lead to a sound & complete algorithm. We choose to assign it the sup of its predecessors in this case, since it seems nice to default to "simpler" types lower down in the subtyping chain.