cryptol-2.2.6: Cryptol: The Language of Cryptography

Copyright(c) 2013-2015 Galois, Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe
LanguageHaskell98

Cryptol.TypeCheck.Unify

Description

 

Synopsis

Documentation

type MGU = (Subst, [Prop]) Source

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

data Result a Source

Constructors

OK a 
Error UnificationError 

Instances

data UnificationError Source

Constructors

UniTypeMismatch Type Type 
UniKindMismatch Kind Kind 
UniTypeLenMismatch Int Int 
UniRecursive TVar Type 
UniNonPolyDepends TVar [TVar] 
UniNonPoly TVar Type 

uniError :: UnificationError -> Result a Source

emptyMGU :: MGU Source

mgu :: Type -> Type -> Result MGU Source

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

bindVar :: TVar -> Type -> Result MGU Source