AST.Unify.Constraints

A class for constraints for unification variables

Documentation

class (PartialOrd c, Semigroup c) => TypeConstraints c where

A class for constraints for unification variables.

Methods

generalizeConstraints :: c -> c

Remove scope constraints.

When generalizing unification variables into universally quantified variables, and then into fresh unification variables upon instantiation, some constraints need to be carried over, and the "scope" constraints need to be erased.

toScopeConstraints :: c -> c

Remove all constraints other than the scope constraints

Useful for comparing constraints to the current scope constraints

Instances

TypeConstraints ScopeLevel

Defined in AST.Infer.ScopeLevel

Methods

generalizeConstraints :: ScopeLevel -> ScopeLevel

toScopeConstraints :: ScopeLevel -> ScopeLevel

class Monad m => MonadScopeConstraints c m where

A class for unification monads with scope levels

Methods

scopeConstraints :: m c

Get the current scope constraint

class TypeConstraints (TypeConstraintsOf ast) => HasTypeConstraints (ast :: Knot -> *) where

A class for terms that have constraints.

A dependency of Unify

Associated Types

type TypeConstraintsOf (ast :: Knot -> Type) :: Type

Methods

verifyConstraints :: TypeConstraintsOf ast -> Tree ast k -> Maybe (Tree ast (WithConstraint k))

Verify constraints on the ast and apply the given child verifier on children

data WithConstraint k ast

A Knot to represent a term alongside a constraint.

Used for verifyConstraints.

Constructors

WithConstraint

Fields

• _wcConstraint :: TypeConstraintsOf (GetKnot ast)
• _wcBody :: k ast

wcConstraint :: forall k ast. Lens' (WithConstraint k ast) (TypeConstraintsOf (GetKnot ast))

wcBody :: forall k ast k. Lens (WithConstraint k ast) (WithConstraint k ast) (k ast) (k ast)