Safe Haskell  SafeInferred 

Type environments.
An environment contains the types named bound variables, named primitives, and a deBruijn stack for anonymous variables.
 data Env n = Env {
 envMap :: !(Map n (Type n))
 envStack :: ![Type n]
 envStackLength :: !Int
 envPrimFun :: !(n > Maybe (Type n))
 type SuperEnv n = Env n
 type KindEnv n = Env n
 type TypeEnv n = Env n
 empty :: Env n
 singleton :: Ord n => Bind n > Env n
 extend :: Ord n => Bind n > Env n > Env n
 extends :: Ord n => [Bind n] > Env n > Env n
 union :: Ord n => Env n > Env n > Env n
 unions :: Ord n => [Env n] > Env n
 fromList :: Ord n => [Bind n] > Env n
 fromTypeMap :: Map n (Type n) > Env n
 depth :: Env n > Int
 member :: Ord n => Bound n > Env n > Bool
 memberBind :: Ord n => Bind n > Env n > Bool
 lookup :: Ord n => Bound n > Env n > Maybe (Type n)
 lookupName :: Ord n => n > Env n > Maybe (Type n)
 setPrimFun :: (n > Maybe (Type n)) > Env n > Env n
 isPrim :: Env n > n > Bool
 wrapTForalls :: Ord n => Env n > Type n > Type n
 lift :: Ord n => Int > Env n > Env n
Documentation
A type environment.
Env  

Construction
extend :: Ord n => Bind n > Env n > Env nSource
Extend an environment with a new binding. Replaces bindings with the same name already in the environment.
extends :: Ord n => [Bind n] > Env n > Env nSource
Extend an environment with a list of new bindings. Replaces bindings with the same name already in the environment.
union :: Ord n => Env n > Env n > Env nSource
Combine two environments. If both environments have a binding with the same name, then the one in the second environment takes preference.
unions :: Ord n => [Env n] > Env nSource
Combine multiple environments, with the latter ones taking preference.
Conversion
fromTypeMap :: Map n (Type n) > Env nSource
Convert a map of names to types to a environment.
Projections
member :: Ord n => Bound n > Env n > BoolSource
Check whether a bound variable is present in an environment.
memberBind :: Ord n => Bind n > Env n > BoolSource
Check whether a binder is already present in the an environment. This can only return True for named binders, not anonymous or primitive ones.
lookup :: Ord n => Bound n > Env n > Maybe (Type n)Source
Lookup a bound variable from an environment.
lookupName :: Ord n => n > Env n > Maybe (Type n)Source
Lookup a bound name from an environment.
Primitives
setPrimFun :: (n > Maybe (Type n)) > Env n > Env nSource
Set the function that knows the types of primitive things.
isPrim :: Env n > n > BoolSource
Check if the type of a name is defined by the envPrimFun
.
Lifting
wrapTForalls :: Ord n => Env n > Type n > Type nSource
Wrap locally bound (non primitive) variables defined in an environment around a type as new foralls.