Polysemy.Plugin.Fundep.Unification

Documentation

data SolveContext

The context in which we're attempting to solve a constraint.

Constructors

FunctionDef (Set TyVar)

In the context of a function definition. The Set TyVar is all of the skolems that exist in the [G] constraints for this function.

InterpreterUse Bool (Set TyVar)

In the context of running an interpreter. The Bool corresponds to whether we are only trying to solve a single Member constraint right now. If so, we *must* produce a unification wanted.

Instances

Outputable SolveContext

Defined in Polysemy.Plugin.Fundep.Unification

Methods

ppr :: SolveContext -> SDoc

Eq SolveContext

Defined in Polysemy.Plugin.Fundep.Unification

Methods

(==) :: SolveContext -> SolveContext -> Bool

(/=) :: SolveContext -> SolveContext -> Bool

Ord SolveContext

Defined in Polysemy.Plugin.Fundep.Unification

Methods

compare :: SolveContext -> SolveContext -> Ordering

(<) :: SolveContext -> SolveContext -> Bool

(<=) :: SolveContext -> SolveContext -> Bool

(>) :: SolveContext -> SolveContext -> Bool

(>=) :: SolveContext -> SolveContext -> Bool

max :: SolveContext -> SolveContext -> SolveContext

min :: SolveContext -> SolveContext -> SolveContext

mustUnify :: SolveContext -> Bool

Depending on the context in which we're solving a constraint, we may or may not want to force a unification of effects. For example, when defining user code whose type is Member (State Int) r => ..., if we see get :: Sem r s, we should unify s ~ Int.

unify

Arguments

:: SolveContext

-> Type

wanted

-> Type

given

-> Maybe Subst

Determine whether or not two effects are unifiable.

All free variables in [W] constraints are considered skolems, and thus are not allowed to unify with anything but themselves. This properly handles all cases in which we are unifying ambiguous [W] constraints (which are true type variables) against [G] constraints.

tryUnifyUnivarsButNotSkolems :: Set TyVar -> Type -> Type -> Maybe Subst

data Unification

A wrapper for two types that we want to say have been unified.

Constructors

Unification

Fields

• _unifyLHS :: OrdType
• _unifyRHS :: OrdType

Instances

Eq Unification

Defined in Polysemy.Plugin.Fundep.Unification

Methods

(==) :: Unification -> Unification -> Bool

(/=) :: Unification -> Unification -> Bool

Ord Unification

Defined in Polysemy.Plugin.Fundep.Unification

Methods

compare :: Unification -> Unification -> Ordering

(<) :: Unification -> Unification -> Bool

(<=) :: Unification -> Unification -> Bool

(>) :: Unification -> Unification -> Bool

(>=) :: Unification -> Unification -> Bool

max :: Unification -> Unification -> Unification

min :: Unification -> Unification -> Unification

newtype OrdType

Types don't have Eq or Ord instances by default, even though there are functions in GHC that implement these operations. This newtype gives us those instances.

Constructors

OrdType

Fields

• getOrdType :: Type

Instances

Eq OrdType

Defined in Polysemy.Plugin.Fundep.Unification

Methods

(==) :: OrdType -> OrdType -> Bool

(/=) :: OrdType -> OrdType -> Bool

Ord OrdType

Defined in Polysemy.Plugin.Fundep.Unification

Methods

compare :: OrdType -> OrdType -> Ordering

(<) :: OrdType -> OrdType -> Bool

(<=) :: OrdType -> OrdType -> Bool

(>) :: OrdType -> OrdType -> Bool

(>=) :: OrdType -> OrdType -> Bool

max :: OrdType -> OrdType -> OrdType

min :: OrdType -> OrdType -> OrdType

unzipNewWanteds :: Set Unification -> [(Unification, Ct)] -> ([Unification], [Ct])

Filter out the unifications we've already emitted, and then give back the things we should put into the S.Set Unification, and the new constraints we should emit.