Documentation

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

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.

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!

A non-recursive version of canUnifyRecursive.

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

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.

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.