Cryptol.TypeCheck.Unify

Documentation

type MGU = (Subst, [Prop])

The most general unifier is a substitution and a set of constraints on bound variables.

type Result a = Writer [UnificationError] a

runResult :: Result a -> (a, [UnificationError])

data UnificationError

Constructors

UniTypeMismatch Type Type

UniKindMismatch Kind Kind

UniTypeLenMismatch Int Int

UniRecursive TVar Type

UniNonPolyDepends TVar [TParam]

UniNonPoly TVar Type

uniError :: UnificationError -> Result MGU

emptyMGU :: MGU

mgu :: Type -> Type -> Result MGU

mguMany :: [Type] -> [Type] -> Result MGU

bindVar :: TVar -> Type -> Result MGU