in-other-words-plugin-0.1.0.0: Disambiguate obvious uses of effects when using in-other-words.
Safe HaskellNone
LanguageHaskell2010

Control.Effect.Plugin.Fundep.Unification

Synopsis

Documentation

data SolveContext Source #

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.

mustUnify :: 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 Eff (State Int) m => ..., if we see get :: Eff (State s) m => m s, we should unify s ~ Int.

canUnifyRecursive Source #

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 Eff (State s) m => ..., 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 $ get @Int

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 Source #

A non-recursive version of canUnifyRecursive.

data Unification Source #

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

Constructors

Unification 

newtype 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 

Fields

Instances

Instances details
Eq OrdType Source # 
Instance details

Defined in Control.Effect.Plugin.Fundep.Unification

Methods

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

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

Ord OrdType Source # 
Instance details

Defined in Control.Effect.Plugin.Fundep.Unification

unzipNewWanteds :: 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.