Safe Haskell  SafeInferred 

 class Rename c where
 renameWith :: Ord n => Sub n > c n > c n
 data Sub n = Sub {
 subBound :: !(Bound n)
 subShadow0 :: !Bool
 subConflict1 :: !(Set n)
 subConflict0 :: !(Set n)
 subStack1 :: !(BindStack n)
 subStack0 :: !(BindStack 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
 bind1 :: Ord n => Sub n > Bind n > (Sub n, Bind n)
 bind1s :: Ord n => Sub n > [Bind n] > (Sub n, [Bind n])
 bind0 :: Ord n => Sub n > Bind n > (Sub n, Bind n)
 bind0s :: Ord n => Sub n > [Bind n] > (Sub n, [Bind n])
 use1 :: Ord n => Sub n > Bound n > Bound n
 use0 :: Ord n => Sub n > Bound n > Bound n
Documentation
renameWith :: Ord n => Sub n > c n > c nSource
Rewrite names in some thing to anonymous form if they conflict with
any names in the Sub
state. We use this to avoid variable capture
during substitution.
Substitution states
Substitution state. Keeps track of the binders in the environment that have been rewrittten to avoid variable capture or spec binder shadowing.
Sub  

Binding stacks
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.
pushBinds :: Ord n => Set n > BindStack n > [Bind n] > (BindStack n, [Bind n])Source
Push several binds onto the bind stack, anonymyzing them if need be to avoid variable capture.
:: Ord n  
=> BindStack n  Current Bind stack during substitution. 
> Bound n  Bound we're substituting for. 
> Bound n  Bound we're looking at now. 
> Either (Bound n) Int 
Compare a Bound
against the one we're substituting for.
Rewriting binding occurences
bind1 :: Ord n => Sub n > Bind n > (Sub n, Bind n)Source
Push a level1 binder on the rewrite stack.
bind1s :: Ord n => Sub n > [Bind n] > (Sub n, [Bind n])Source
Push some level1 binders on the rewrite stack.
bind0 :: Ord n => Sub n > Bind n > (Sub n, Bind n)Source
Push a level0 binder on the rewrite stack.
bind0s :: Ord n => Sub n > [Bind n] > (Sub n, [Bind n])Source
Push some level0 binders on the rewrite stack.