Safe Haskell  SafeInferred 

Capture avoiding substitution of types in types.
 class SubstituteT c where
 substituteT :: (SubstituteT c, Ord n) => Bind n > Type n > c n > c n
 substituteTs :: (SubstituteT c, Ord n) => [(Bind n, Type n)] > c n > c n
 substituteBoundT :: (SubstituteT c, Ord n) => Bound n > Type n > c n > c n
 data BindStack n = BindStack {
 stackBinds :: [Bind n]
 stackAll :: [Bind n]
 stackAnons :: Int
 stackNamed :: Int
 pushBind :: Ord n => Set n > BindStack n > Bind n > (BindStack n, Bind n)
 pushBinds :: Ord n => Set n > BindStack n > [Bind n] > (BindStack n, [Bind n])
 substBound :: Ord n => BindStack n > Bound n > Bound n > Either (Bound n) Int
Documentation
class SubstituteT c whereSource
:: forall n . Ord n  
=> Bound n  Bound variable that we're subsituting into. 
> Type n  Type to substitute. 
> Set n  Names of free varaibles in the type to substitute. 
> BindStack n  Bind stack. 
> c n  
> c n 
Substitute a type into some thing. In the target, if we find a named binder that would capture a free variable in the type to substitute, then we rewrite that binder to anonymous form, avoiding the capture.
substituteT :: (SubstituteT c, Ord n) => Bind n > Type n > c n > c nSource
substituteTs :: (SubstituteT c, Ord n) => [(Bind n, Type n)] > c n > c nSource
Wrapper for substituteT
to substitute multiple things.
substituteBoundT :: (SubstituteT c, Ord n) => Bound n > Type n > c n > c nSource
Stack of anonymous binders that we've entered under during substitution.
BindStack  

:: Ord n  
=> Set n  Names that need to be rewritten. 
> BindStack n  Current bind stack. 
> Bind n  Bind to push. 
> (BindStack n, Bind n)  New stack and possibly anonymised bind. 
Push a bind onto a bind stack, anonymizing it if need be to avoid variable capture.