Modulepolysemy-plugin-0.4.5.3Haskell2010

Polysemy.Plugin.Fundep.Unification

Synopsis

data SolveContext
value mustUnify
value unify
value tryUnifyUnivarsButNotSkolems
data Unification
newtype OrdType
value unzipNewWanteds

Packagepolysemy-plugin-0.4.5.3
Exports7
LanguageHaskell2010
LicenceBSD-3-Clause
SourceUnification.hs

datadata SolveContext

Source#

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.

Instances3Eq, Ord, Outputable

Eq SolveContextDefined in polysemy-plugin-0.4.5.3 · Polysemy.Plugin.Fundep.Unification
Ord SolveContextDefined in polysemy-plugin-0.4.5.3 · Polysemy.Plugin.Fundep.Unification
Outputable SolveContextDefined in polysemy-plugin-0.4.5.3 · Polysemy.Plugin.Fundep.Unification

valuemustUnify :: SolveContext -> Bool

Source#

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.

valueunify

:: SolveContext
-> Type
wanted
-> Type
given
-> Maybe Subst

Source#

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.

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

datadata Unification

Source#

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

Constructors

Unification
- _unifyLHS :: OrdType
- _unifyRHS :: OrdType

Instances2Eq, Ord

Eq UnificationDefined in polysemy-plugin-0.4.5.3 · Polysemy.Plugin.Fundep.Unification
Ord UnificationDefined in polysemy-plugin-0.4.5.3 · Polysemy.Plugin.Fundep.Unification

newtypenewtype OrdType

Source#

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
- getOrdType :: Type

Instances2Eq, Ord

Eq OrdTypeDefined in polysemy-plugin-0.4.5.3 · Polysemy.Plugin.Fundep.Unification
Ord OrdTypeDefined in polysemy-plugin-0.4.5.3 · Polysemy.Plugin.Fundep.Unification

valueunzipNewWanteds

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

Source#

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.