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
- 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 |
freeParams :: FVS t => t -> Set TParam Source #