cryptol-2.7.0: Cryptol: The Language of Cryptography

Copyright	(c) 2013-2016 Galois Inc.
License	BSD3
Maintainer	cryptol@galois.com
Stability	provisional
Portability	portable
Safe Haskell	Safe
Language	Haskell2010

Cryptol.TypeCheck.Unify

Description

Synopsis

type MGU = (Subst, [Prop])
type Result a = Writer [UnificationError] a
runResult :: Result a -> (a, [UnificationError])
data UnificationError
- = 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
freeParams :: FVS t => t -> Set TParam

Documentation

type MGU = (Subst, [Prop]) Source #

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

type Result a = Writer [UnificationError] a Source #

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

data UnificationError Source #

Constructors

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

uniError :: UnificationError -> Result MGU Source #

emptyMGU :: MGU Source #

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

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

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

freeParams :: FVS t => t -> Set TParam Source #