Polysemy.Plugin.Fundep.Unification

Documentation

data SolveContext

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

Constructors

FunctionDef

In the context of a function definition.

InterpreterUse Bool

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

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

Show SolveContext

Defined in Polysemy.Plugin.Fundep.Unification

Methods

showsPrec :: Int -> SolveContext -> ShowS

show :: SolveContext -> String

showList :: [SolveContext] -> ShowS

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.

canUnifyRecursive

Arguments

:: SolveContext

-> Type

wanted

-> Type

given

-> Bool

Determine whether or not two effects are unifiable. This is nuanced.

There are several cases:

1. [W] ∀ e1. e1 [G] ∀ e2. e2 Always fails, because we never want to unify two effects if effect names are polymorphic.
2. [W] State s [G] State Int Always succeeds. It's safe to take our given as a fundep annotation.
3. [W] State Int [G] State s (when the [G] is a given that comes from a type signature)

This should fail, because it means we wrote the type signature Member (State s) r => ..., but are trying to use s as an Int. Clearly bogus!

1. [W] State Int [G] State s (when the [G] was generated by running an interpreter)

Sometimes OK, but only if the [G] is the only thing we're trying to solve right now. Consider the case:

runState 5 $ pure @(Sem (State Int ': r)) ()

Here we have [G] forall a. Num a => State a and [W] State Int. Clearly the typechecking should flow "backwards" here, out of the row and into the type of runState.

What happens if there are multiple [G]s in scope for the same r? Then we'd emit multiple unification constraints for the same effect but with different polymorphic variables, which would unify a bunch of effects that shouldn't be!

canUnify :: Bool -> Type -> Type -> Bool

A non-recursive version of canUnifyRecursive.

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.