cryptol-2.2.6: Cryptol: The Language of Cryptography

Copyright | (c) 2013-2015 Galois, Inc.
License | BSD3
Maintainer | cryptol@galois.com
Stability | provisional
Portability | portable
Safe Haskell | Safe
Language | Haskell98

Cryptol.TypeCheck.Unify

Description

Synopsis

- type MGU = (Subst, [Prop])
- data Result a
  - = OK a
  - | Error UnificationError
- data UnificationError
  - = 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

# 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

Monad Result Source |
Functor Result Source |
Applicative Result Source |

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