Safe Haskell	Safe-Inferred
Language	Haskell2010

Unison.KindInference.Solve

Description

Handles solving kind constraints generated by Unison.KindInference.Generate.

Synopsis

step :: (Var v, Ord loc, Show loc) => Env -> SolveState v loc -> [GeneratedConstraint v loc] -> Either (NonEmpty (KindError v loc)) (SolveState v loc)
verify :: Var v => SolveState v loc -> Either (NonEmpty (KindError v loc)) (SolveState v loc)
initialState :: forall v loc. (BuiltinAnnotation loc, Show loc, Ord loc, Var v) => Env -> SolveState v loc
defaultUnconstrainedVars :: Var v => SolveState v loc -> SolveState v loc
data KindError v loc
- = CycleDetected loc (UVar v loc) (ConstraintMap v loc)
- | UnexpectedArgument loc (UVar v loc) (UVar v loc) (ConstraintMap v loc)
- | ArgumentMismatch (UVar v loc) (UVar v loc) (UVar v loc) (ConstraintMap v loc)
- | ArgumentMismatchArrow (loc, Type v loc, Type v loc) (ConstraintConflict v loc) (ConstraintMap v loc)
- | EffectListMismatch (ConstraintConflict v loc) (ConstraintMap v loc)
- | ConstraintConflict (GeneratedConstraint v loc) (ConstraintConflict v loc) (ConstraintMap v loc)
data ConstraintConflict v loc = ConstraintConflict' {
- conflictedVar :: UVar v loc
- impliedConstraint :: Constraint (UVar v loc) v loc
- conflictedConstraint :: Constraint (UVar v loc) v loc
}

Documentation

step :: (Var v, Ord loc, Show loc) => Env -> SolveState v loc -> [GeneratedConstraint v loc] -> Either (NonEmpty (KindError v loc)) (SolveState v loc) Source #

This is the primary function in the exposed API. step applies some generated constraints to a solve state, returning a kind error if detected or a new solve state.

verify :: Var v => SolveState v loc -> Either (NonEmpty (KindError v loc)) (SolveState v loc) Source #

Do an occurence check and return an error or the resulting solve state

initialState :: forall v loc. (BuiltinAnnotation loc, Show loc, Ord loc, Var v) => Env -> SolveState v loc Source #

defaultUnconstrainedVars :: Var v => SolveState v loc -> SolveState v loc Source #

Default any unconstrained vars to Type

data KindError v loc Source #

Errors that may arise during kind inference

Constructors

CycleDetected loc (UVar v loc) (ConstraintMap v loc)	A variable is constrained to have an infinite kind
UnexpectedArgument	Something of kind * or Effect is applied to an argument
Fields loc src span of abs (UVar v loc) abs var (UVar v loc) arg var (ConstraintMap v loc) context \| An arrow kind is applied to a type, but its kind doesn't match the expected argument kind
ArgumentMismatch
Fields (UVar v loc) abs var (UVar v loc) expected var (UVar v loc) given var (ConstraintMap v loc) context \| Same as `ArgumentMismatch`, but for applications to the builtin `Arrow` type.
ArgumentMismatchArrow
Fields (loc, Type v loc, Type v loc) (The applied arrow range, lhs, rhs) (ConstraintConflict v loc) (ConstraintMap v loc)
EffectListMismatch (ConstraintConflict v loc) (ConstraintMap v loc)	Something appeared in an effect list that isn't of kind Effect
ConstraintConflict	Generic constraint conflict
Fields (GeneratedConstraint v loc) Failed to add this constraint (ConstraintConflict v loc) Due to this conflict (ConstraintMap v loc) in this context

Instances

Instances details

Show (KindError v loc) Source #
Instance details Defined in Unison.KindInference.Error Methods showsPrec :: Int -> KindError v loc -> ShowS # show :: KindError v loc -> String # showList :: [KindError v loc] -> ShowS #

data ConstraintConflict v loc Source #

Two incompatible constraints on a UVar.

Constructors

ConstraintConflict'
Fields conflictedVar :: UVar v loc impliedConstraint :: Constraint (UVar v loc) v loc conflictedConstraint :: Constraint (UVar v loc) v loc