Cryptol.TypeCheck.Unify

Documentation

type MGU = (Subst, [Prop])

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

data Result a

Constructors

OK a

Error UnificationError

Instances

Monad Result

Methods

(>>=) :: Result a -> (a -> Result b) -> Result b

(>>) :: Result a -> Result b -> Result b

return :: a -> Result a

fail :: String -> Result a

Functor Result

Methods

fmap :: (a -> b) -> Result a -> Result b

(<$) :: a -> Result b -> Result a

Applicative Result

Methods

pure :: a -> Result a

(<*>) :: Result (a -> b) -> Result a -> Result b

(*>) :: Result a -> Result b -> Result b

(<*) :: Result a -> Result b -> Result a

data UnificationError

Constructors

UniTypeMismatch Type Type

UniKindMismatch Kind Kind

UniTypeLenMismatch Int Int

UniRecursive TVar Type

UniNonPolyDepends TVar [TVar]

UniNonPoly TVar Type

uniError :: UnificationError -> Result a

emptyMGU :: MGU

mgu :: Type -> Type -> Result MGU

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

bindVar :: TVar -> Type -> Result MGU