cryptol-2.8.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 #