diff --git a/Changelog.md b/Changelog.md
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,3 +1,16 @@
+# NEXT
+
+# 0.3.2
+
+* Bump `deepseq >= 1.4.0.0` remove benchmark dependency on `deepseq-generics`
+* Tested with GHC 8.4.1
+* Tested with GHC 8.2.2
+* Compile with `-Wcompat`
+* Add `Semigroup` instances for all types that were previously `Monoid` instances
+* Added more examples to the [examples/ directory](https://github.com/lambdageek/unbound-generics/tree/master/examples)
+* Added "exceptions" dependency and `MonadThrow`, `MonadCatch`, `MonadMask` instances for `FreshMT` and `LFreshMT`.
+  Thanks Alex McKenna.
+
 # 0.3.1
 
 * Tested with GHC 8.0.1
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -14,8 +14,11 @@
 
 This is a reimplementation of (parts of) [unbound](http://hackage.haskell.org/package/unbound) but using [GHC generics](http://www.haskell.org/ghc/docs/latest/html/libraries/base-4.7.0.1/GHC-Generics.html) instead of [RepLib](https://hackage.haskell.org/package/RepLib).
 
-## Example
+## Examples
 
+Some examples are in the `examples/` directory in the source.  And also at [unbound-generics on GitHub Pages](https://lambdageek.github.io/unbound-generics)
+
+### Example: Untyped lambda calculus interpreter
 Here is how you would implement call by value evaluation for the untyped lambda calculus:
 
 ```haskell
diff --git a/benchmarks/BenchLam.hs b/benchmarks/BenchLam.hs
--- a/benchmarks/BenchLam.hs
+++ b/benchmarks/BenchLam.hs
@@ -1,5 +1,5 @@
 -- | Untyped lambda calc for benchmarking
-{-# LANGUAGE DeriveGeneric, DeriveDataTypeable #-}
+{-# LANGUAGE DeriveGeneric, DeriveDataTypeable, CPP #-}
 module BenchLam where
 
 import Control.Applicative
@@ -10,7 +10,10 @@
 import Data.Typeable (Typeable)
 
 import Control.DeepSeq (NFData(..), deepseq)
+#if MIN_VERSION_deepseq (1,4,0)
+#else
 import Control.DeepSeq.Generics (genericRnf)
+#endif
 import Criterion (Benchmark, env, bench, nf)
 
 import Unbound.Generics.LocallyNameless
@@ -24,7 +27,11 @@
     deriving (Show, Generic, Typeable)
 
 instance Alpha Term
+#if MIN_VERSION_deepseq (1,4,0)
+instance NFData Term
+#else
 instance NFData Term where rnf = genericRnf
+#endif
 
 
 -- | lambda abstract over all the given vars
diff --git a/examples/CanonicalLF.lhs b/examples/CanonicalLF.lhs
new file mode 100644
--- /dev/null
+++ b/examples/CanonicalLF.lhs
@@ -0,0 +1,535 @@
+% Canonical LF using unbound-generics
+% Aleksey Kliger
+% June 2016
+
+Canonical LF
+============
+
+This is a representation of [LF](http://www.twelf.org/) in which all terms are
+automatically in *canonical form*.  The key idea is to segregate the type families
+and the terms into *atomic* and *normal* forms where the term variables only stand
+for atomic terms, and not arbitrary ones.  Then, a substitution procedure is defined
+that takes terms in normal form and performs a substitution for a variable while
+simultaneously normalizing any redices that occur.
+
+> {-# LANGUAGE DeriveGeneric, StandaloneDeriving, DeriveDataTypeable,
+>     ViewPatterns, RankNTypes, FlexibleContexts, FlexibleInstances,
+>     FunctionalDependencies, TypeFamilies
+>   #-}
+> module CanonicalLF where
+> import Unbound.Generics.LocallyNameless
+> import GHC.Generics (Generic)
+> import Data.Typeable (Typeable)
+> import qualified Data.Map as M
+> import Control.Monad.Reader
+> import Control.Monad.Except
+> import Data.Functor.Identity
+> import Control.Applicative (Const(..))
+
+Syntax
+------
+
+An LF signature introduces type family atoms and constant terms.
+
+> data Signature = NilS
+>   | SnocAtom (Rebind Signature (Atm, Embed Kind))
+>   | SnocConst (Rebind Signature (Cnst, Embed Type))
+>   deriving (Show, Generic, Typeable)
+
+The type families are classified by kinds and may either be plain
+types, or pi-kinds for families of types indexed by a term
+variable.
+
+> data Kind = TypeK | PiK (Bind (Var, Embed Type) Kind)
+>   deriving (Show, Generic, Typeable)
+
+The atomic type families are either type familiy atoms applied to zero
+or more terms in normal form.
+
+> type Atm = Name P
+> data P = AtmP Atm | AppP P Term
+>   deriving (Show, Generic, Typeable)
+
+Type families in normal form are either atomic type families or dependent product
+types indexed by a term variable of normal type.
+
+> data Type = PT P | PiT (Bind (Var, Embed Type) Type)
+>   deriving (Show, Generic, Typeable)
+
+The atomic terms are either variables or constants applied to zero or
+more terms in normal form.
+
+> type Cnst = Name R
+> type Var = Name R
+> data R = VarR Var | ConstR Cnst | AppR R Term
+>   deriving (Show, Generic, Typeable)
+
+A term in normal form is either an atomic term or a lambda abstraction
+that binds a term variable.
+
+> data Term = RM R | LamM (Bind Var Term)
+>   deriving (Show, Generic, Typeable)
+
+When typechecking kinds, types or terms, new term variables may come
+into scope. They are collected in contexts.
+
+> data Context = NilC
+>              | Snoc (Rebind Context (Var, Embed Type))
+>              deriving (Show, Generic, Typeable)
+
+All the syntactic objects are equivalent upto renaming of bound variables.
+
+> instance Alpha Signature
+> instance Alpha Kind
+> instance Alpha P
+> instance Alpha Type
+> instance Alpha R
+> instance Alpha Term
+> instance Alpha Context
+
+The metatheory of Canonical LF uses simple types to prove the
+termination of hereditary substitution (defined below).  But they
+aren't needed in the implementation.  (Although it would be
+interesting to lift them to Haskell kinds and index the terms by the
+simple types to disallow some malformed terms.)
+
+> data SimpleType = AtmS Atm | ArrS SimpleType SimpleType
+>   deriving (Show, Generic, Typeable)
+>
+> instance Alpha SimpleType
+
+Hereditary Substitution
+-----------------------
+
+Variables in Canonical LF stand for atomic terms, but we will need to
+subtitute terms for them.  If we used ordinary capture-avoiding
+substitution, such substitution would produce redices, which we are
+precisely what we don't want.  However redices will potentially only
+occur when the variable for which we're substituting occurs at the
+head of an atomic term.
+
+> isHeadVarR :: Var -> R -> Bool
+> isHeadVarR x (VarR y) = x == y
+> isHeadVarR _ (ConstR _) = False
+> isHeadVarR x (AppR r _) = isHeadVarR x r
+
+Just using a boolean to decide if the variable is at the head of an
+atomic term is fine, but we can actually partition an atomic term into
+its head variable or constant together with a spine of applications.
+
+> data Spine a = NilSp a | AppSp (Spine a) Term
+> data Head = VarH Var | ConstH Cnst
+
+If the variable for which we'll be substituting is at the head we only
+really care about the spine.  Otherwise we have some other variable,
+or perhaps a constant at the head.
+
+> headSpine :: Var -> R -> Either (Spine Head) (Spine ())
+> headSpine x (VarR y) | x == y    = Right (NilSp ())
+>                      | otherwise = Left (NilSp (VarH y))
+> headSpine _ (ConstR c)           = Left (NilSp (ConstH c))
+> headSpine x (AppR r m)           = case headSpine x r of
+>   Left s -> Left (AppSp s m)
+>   Right s -> Right (AppSp s m)
+
+Substitution in a kind just carries out substitution in the types.
+Likewise substutition in normal type families.
+
+> substKind :: Fresh m => Term -> Var -> Kind -> m Kind
+> substKind _ _ TypeK = return TypeK
+> substKind m x (PiK bnd) = do
+>   ((y, unembed -> a), k) <- unbind bnd
+>   a' <- substType m x a
+>   k' <- substKind m x k
+>   return $ PiK $ bind (y, embed a') k'
+>
+> substType :: Fresh m => Term -> Var -> Type -> m Type
+> substType m x (PT p) = do
+>   p' <- substP m x p
+>   return (PT p')
+> substType m x (PiT bnd) = do
+>   ((y, unembed -> a), b) <- unbind bnd
+>   a' <- substType m x a
+>   b' <- substType m x b
+>   return $ PiT $ bind (y, embed a') b'
+
+Atomic type family application substitutes a term for a variable in the (normal) index terms.
+
+> substP :: Fresh m => Term -> Var -> P -> m P
+> substP _ _ (AtmP a) = return (AtmP a)
+> substP m x (AppP p n) = do
+>   p' <- substP m x p
+>   n' <- substTerm m x n
+>   return (AppP p' n')
+
+Normal term substitution goes under a lambda (freshness is ensured by
+the library) and into the atomic term.
+
+> substTerm :: Fresh m => Term -> Var -> Term -> m Term
+> substTerm m x (RM r) = substR m x r
+> substTerm m x (LamM bnd) = do
+>   (y, n) <- unbind bnd
+>   n' <- substTerm m x n
+>   return $ LamM $ bind y n'
+
+To substitute in an atomic term we separate the head and the spine and
+proceed according to whether the variable at the head is the one we
+are substituting for.
+
+> substR :: Fresh m => Term -> Var -> R -> m Term
+> substR m x r =
+>   case headSpine x r of
+>     Left rsp -> RM <$> substRRsp m x rsp
+>     Right msp -> substMsp m x msp
+
+If there is another variable or a constant at the head, we will get
+some kind of atomic term out since the head is unchanged and we only
+substitute into the index terms.
+
+> substRRsp :: Fresh m => Term -> Var -> Spine Head -> m R
+> substRRsp _ _ (NilSp h) = return (headR h)
+> substRRsp m x (AppSp sp n) = do
+>   n' <- substTerm m x n
+>   r <- substRRsp m x sp
+>   return $ AppR r n'
+>
+> headR :: Head -> R
+> headR (VarH y) = VarR y
+> headR (ConstH c) = ConstR c
+
+When the variable we care about is at the head, we apply the
+substitution to the rest of the spine to get a normal term (which, by
+the metatheory will turn out to be some kind of a lambda), apply the
+substitution to the index, and then carry out a new substitution of
+the new index for the variable bound by the lambda to the body of the
+lambda.  This last step is the heredetary part of heredetary
+substitution.  The metatheory guarantees that this process will
+terminate.  (Because the simple type of the body of the lambda is
+smaller than the simple type of the original term).
+
+> substMsp :: Fresh m => Term -> Var -> Spine () -> m Term
+> substMsp m _ (NilSp ()) = return m
+> substMsp m x (AppSp s n) = do
+>   o_ <- substMsp m x s
+>   n' <- substTerm m x n
+>   case o_ of
+>     LamM bnd -> do
+>       (y, o) <- unbind bnd
+>       substTerm n' y o
+>     _ -> error "can't happen"
+
+Typechecking
+============
+
+We typecheck in an environment that maps type family atoms, term
+costants and variables to their respective kinds and types.
+
+> data Env = Env { _envAtm :: M.Map Atm Kind,
+>                  _envConst :: M.Map Cnst Type,
+>                  _envCtx :: M.Map Var Type }
+
+> emptyEnv :: Env
+> emptyEnv = Env M.empty M.empty M.empty
+
+Some lenses to work with the environment
+
+> envAtm :: Lens' Env (M.Map Atm Kind)
+> envAtm afb s = fmap (\atms -> s { _envAtm = atms }) $ afb (_envAtm s)
+>
+> envCtx :: Lens' Env (M.Map Var Type)
+> envCtx afb s = fmap (\ctx -> s { _envCtx = ctx } ) $ afb (_envCtx s)
+>
+> envConst :: Lens' Env (M.Map Cnst Type)
+> envConst afb s = fmap (\sig -> s { _envConst = sig} ) $ afb (_envConst s)
+
+And some combinators to perform lookups.
+
+> lookupOver :: (MonadReader e m, MonadError String m) => Getting p e p -> String -> (p -> Maybe c) -> m c
+> lookupOver l s f = do
+>   mk <- views l f
+>   case mk of
+>     Nothing -> throwError $ "unbound " ++ s
+>     Just c -> return c
+>
+> lookupAtom :: (MonadReader Env m, MonadError String m) => Atm -> m Kind
+> lookupAtom = lookupOver envAtm "atom" . M.lookup 
+>
+> lookupVar :: (MonadReader Env m, MonadError String m) => Var -> m Type
+> lookupVar = lookupOver envCtx "variable" . M.lookup
+>
+> lookupConst :: (MonadReader Env m, MonadError String m) => Cnst -> m Type
+> lookupConst = lookupOver envConst "constant" . M.lookup
+
+To check a signature we check the kind or type classifying the atom or
+constant and then continue in an environment extended with the new
+binding.
+
+> withSigOk :: (Fresh m, MonadReader Env m, MonadError String m) => Signature -> m r -> m r
+> withSigOk NilS kont = kont
+> withSigOk (SnocAtom (unrebind -> (s, (a, unembed -> k)))) kont =
+>   withSigOk s $ do
+>   local (set envCtx M.empty) $ wfk k
+>   local (over envAtm (M.insert a k)) kont
+> withSigOk (SnocConst (unrebind -> (s, (c, unembed -> a)))) kont =
+>   withSigOk s $ do
+>   local (set envCtx M.empty) $ wfType a
+>   local (over envConst (M.insert c a)) kont
+
+Kind and normal type formation is unsurprising.  Note that PT is only
+well-formed when the atomic type family is fully applied and is of
+base kind.
+
+> wfk :: (Fresh m, MonadReader Env m, MonadError String m) => Kind -> m ()
+> wfk TypeK = return ()
+> wfk (PiK bnd) = do
+>   ((x, unembed -> t), k) <- unbind bnd
+>   wfType t
+>   local (over envCtx (M.insert x t)) $ wfk k
+>
+> wfType :: (Fresh m, MonadReader Env m, MonadError String m) => Type -> m ()
+> wfType (PT p) = do
+>   k <- inferP p
+>   case k of
+>     TypeK -> return ()
+>     _ -> throwError "expected a type"
+> wfType (PiT bnd) = do
+>   ((x, unembed -> a), b) <- unbind bnd
+>   wfType a
+>   local (over envCtx (M.insert x a)) $ wfType b
+
+For atomic type families we infer their kinds.  For atoms we read the
+kind off from the environment.  For applications we infer the kind of
+the type family (which had better be a pi kind), and then check that
+the term argument has the expected type and then return the resulting
+kind where we (heredeterily) substitute the term for the index
+variable.
+
+> inferP :: (Fresh m, MonadReader Env m, MonadError String m) => P -> m Kind
+> inferP (AtmP atm) = lookupAtom atm
+> inferP (AppP p m) = do
+>   k <- inferP p
+>   case k of
+>     TypeK -> throwError "expected a pi kind"
+>     PiK bnd -> do
+>       ((x, unembed -> a), k') <- unbind bnd
+>       checkTerm m a
+>       substKind m x k'
+
+To check that a term in normal form has the expected normal type, we
+check that its either a lambda of pi type, or an atomic term of atomic
+type.  The latter ensures that terms are in eta long form by requiring
+all variables and constants to be fully applied.
+
+We infer the type of an atomic term (which had better be atomic) and
+then check that it is alpha-equivalent to the given atomic type.
+Because the calculus is constructed to only allow terms in normal
+form, alpha equivalence suffices and we don't have to do any
+normalization.  (We paid that price in heredetary substitution.)
+
+> checkTerm :: (Fresh m, MonadReader Env m, MonadError String m) => Term -> Type -> m ()
+> checkTerm (LamM bnd) (PiT bnd') = do
+>   mmatch <- unbind2 bnd bnd'
+>   case mmatch of
+>     Just (x, m, (_, unembed -> a), b) -> do
+>       wfType a
+>       local (over envCtx (M.insert x a)) $ checkTerm m b
+>     Nothing -> throwError "did not match"
+> checkTerm (RM r) (PT p) = do
+>   t <- inferTerm r
+>   case t of
+>     (PT p') | p `aeq` p' -> return ()
+>     _ -> throwError "atomic term doesn't have the expected atomic type."
+> checkTerm (LamM {}) _ = throwError "lambda with no-PI type"
+> checkTerm (RM {}) _ = throwError "atomic term with non-atomic type"
+
+To infer the type of a term, we lookup variables and constants in the
+environment.  For applications we ensure that the head has some kind
+of pi type and then check the index against the argument type, and
+then return the result type with the argument substituted for the
+index variable.
+
+> inferTerm :: (Fresh m, MonadReader Env m, MonadError String m) => R -> m Type
+> inferTerm (VarR x) = lookupVar x
+> inferTerm (ConstR c) = lookupConst c
+> inferTerm (AppR r m) = do
+>   p_ <- inferTerm r
+>   case p_ of
+>     PiT bnd -> do
+>       ((x, unembed -> a), b) <- unbind bnd
+>       checkTerm m a
+>       substType m x b
+>     PT {} -> throwError "expected a function in application position"
+
+Smart Constructors
+==================
+
+This section defines a little DSL for writing Canonical LF terms in
+Haskell.  It's a higher-order encoding that uses haskell variable
+binding to represent LF binding constructs.
+
+We use a higher-kinded repr parameter to allow for different sorts of
+interpretations for this DSL.  Although in this example we only build
+one using the Syn newtype to wrap a fresh-name monad computation that
+just builds a term in our original AST, above.
+
+> class TermSyntax repr r n | r -> n, n -> r where
+>   lam :: String -> ((repr r) -> (repr n)) -> (repr n)
+>   app :: repr r -> repr n -> repr r
+>   rm :: repr r -> repr n
+>
+> newtype Syn m a = Syn { unSyn :: m a } 
+>
+> instance Fresh m => TermSyntax (Syn m) R Term where
+>   lam hint f = Syn $ do
+>     x <- fresh (s2n hint)
+>     m <- unSyn $ f (Syn $ return $ VarR x)
+>     return $ LamM (bind x m)
+>   app r n = Syn (AppR <$> unSyn r <*> unSyn n)
+>   rm r = Syn (RM <$> unSyn r)
+
+> class  TypeSyntax repr p a | a -> p, p -> a where
+>   type TermInType repr a :: *
+>   type RInType repr a :: *
+>   piT :: String -> repr a -> (repr (RInType repr a) -> repr a) -> repr a
+>   arrT :: repr a -> repr a -> repr a
+>   arrT a b = piT "_" a (const b)
+>   appP :: repr p -> repr (TermInType repr a) -> repr p
+>   pt :: repr p -> repr a
+
+> instance Fresh m => TypeSyntax (Syn m) P Type where
+>   type TermInType (Syn m) Type = Term
+>   type RInType (Syn m) Type = R
+>   piT hint sa f = Syn $ do
+>     x <- fresh (s2n hint)
+>     b <- unSyn $ f (Syn $ return $ VarR x)
+>     a <- unSyn sa
+>     return $ PiT $ bind (x, embed a) b
+>   appP p m = Syn (AppP <$> unSyn p <*> unSyn m)
+>   pt p = Syn (PT <$> unSyn p)
+
+> class KindSyntax repr k where
+>   type TypeInKind repr k :: *
+>   type RInKind repr k :: *
+>   typeK :: repr k
+>   piK :: String -> repr (TypeInKind repr k) -> (repr (RInKind repr k) -> repr k) -> repr k
+>   arrK :: repr (TypeInKind repr k) -> repr k -> repr k
+>   arrK a k = piK "_" a (const k)
+
+> instance Fresh m => KindSyntax (Syn m) Kind where
+>   type TypeInKind (Syn m) Kind = Type
+>   type RInKind (Syn m) Kind = R
+>   typeK = Syn $ return TypeK
+>   piK hint sa sk = Syn $ do
+>     x <- fresh (s2n hint)
+>     a <- unSyn sa
+>     k <- unSyn $ sk (Syn $ return $ VarR x)
+>     return $ PiK $ bind (x, embed a) k
+
+> class SignatureSyntax repr sig p r | sig -> p r where
+>   type KindInSig repr sig :: *
+>   type TypeInSig repr sig :: *
+>   letAtom :: String -> repr (KindInSig repr sig) -> (repr p -> repr sig) -> repr sig
+>   letConstant :: String -> repr (TypeInSig repr sig) -> (repr r -> repr sig) -> repr sig
+>   endSig :: repr sig
+>
+> instance Fresh m => SignatureSyntax (Syn m) (Signature -> Signature) P R where
+>   type KindInSig (Syn m) (Signature -> Signature) = Kind
+>   type TypeInSig (Syn m) (Signature -> Signature) = Type
+>
+>   letAtom hint sk kont = Syn $ do
+>     a <- fresh (s2n hint)
+>     k <- unSyn sk
+>     f <- unSyn $ kont $ Syn $ return $ AtmP a
+>     return $ \sig -> f (SnocAtom $ rebind sig (a, embed k))
+>
+>   letConstant hinst st kont = Syn $ do
+>     c <- fresh (s2n hinst)
+>     t <- unSyn st
+>     f <- unSyn $ kont $ Syn $ return $ ConstR c
+>     return $ \sig -> f (SnocConst $ rebind sig (c, embed t))
+>
+>   endSig = Syn $ return id
+
+> infixr 6 `arrT`, `arrK`
+> infixl 6 `appP`, `app`
+
+Example
+-------
+
+An LF signature fragment for first-order logic.
+
+> example1 :: Fresh m => Syn m (Signature -> Signature)
+> example1 =
+>   letAtom "o" typeK $ \o ->
+>   letConstant "tt" (pt o) $ \tt ->
+>   letConstant "ff" (pt o) $ \ff ->
+>   letConstant "not" (pt o `arrT` pt o) $ \not ->
+>   letConstant "and" (pt o `arrT` pt o `arrT` pt o) $ \and ->
+>   letAtom "nd" (pt o `arrK` typeK) $ \nd ->
+>   letConstant "tti" (pt (nd `appP` rm tt)) $ \tti ->
+>   letConstant "ffe" (piT "a" (pt o) $ \a ->
+>                        pt (nd `appP` rm ff)
+>                        `arrT`
+>                        pt (nd `appP` rm a)) $ \ffe ->
+>   letConstant "noti" (piT "a" (pt o) $ \a ->
+>                          (piT "p" (pt o) $ \p ->
+>                              pt (nd `appP` rm a)
+>                              `arrT`
+>                              pt (nd `appP` rm p))
+>                          `arrT`
+>                          pt (nd `appP` rm (not `app` rm a))) $ \noti ->
+>   letConstant "note" (piT "a" (pt o) $ \a -> piT "c" (pt o) $ \c ->
+>                          pt (nd `appP` rm (not `app` rm a))
+>                          `arrT`
+>                          pt (nd `appP` rm a)
+>                          `arrT`
+>                          pt (nd `appP` rm c)) $ \note ->
+>   letConstant "andi" (piT "a" (pt o) $ \a -> piT "b" (pt o) $ \b ->
+>                          pt (nd `appP` rm a)
+>                          `arrT`
+>                          pt (nd `appP` rm b)
+>                          `arrT`
+>                          pt (nd `appP` rm (and `app` rm a `app` rm b))) $ \andi ->
+>   letConstant "ande1" (piT "a" (pt o) $ \a -> piT "b" (pt o) $ \b ->
+>                           pt (nd `appP` rm (and `app` rm a `app` rm b))
+>                           `arrT`
+>                           pt (nd `appP` rm a)) $ \ande1 ->
+>   letConstant "ande2" (piT "a" (pt o) $ \a -> piT "b" (pt o) $ \b ->
+>                           pt (nd `appP` rm (and `app` rm a `app` rm b))
+>                           `arrT`
+>                           pt (nd `appP` rm b)) $ \ande2 ->
+>   endSig
+
+> checkSynSig :: (Fresh m, MonadReader Env m, MonadError String m) => Syn m (Signature -> Signature) -> m ()
+> checkSynSig sig = do
+>   sigf <- unSyn sig
+>   withSigOk (sigf NilS) $ return ()
+
+Example:
+```haskell
+  >>> runExceptT $ runFreshMT $ runReaderT (checkSynSig example1) emptyEnv
+  Right ()
+```
+
+Appendix: Lens utilities
+==============
+
+Some machinery to work with records.
+
+> type Lens s t a b = forall f . Functor f => (a -> f b) -> s -> f t
+> type Lens' s a = Lens s s a a
+
+> type Setting s t a b = (a -> Identity b) -> s -> Identity t
+> type Setting' s a = Setting s s a a
+
+> over :: Setting s t a b -> (a -> b) -> s -> t
+> over l f = runIdentity . l (Identity . f)
+
+> set :: Setting s t a b -> b -> s -> t
+> set l = over l . const
+
+> type Getting r s a = (a -> Const r a) -> s -> Const r s
+
+> views :: MonadReader s m => Getting a s a -> (a -> r) -> m r
+> views l f = asks (\s -> f (getConst (l Const s)))
+
diff --git a/examples/Nanevski.lhs b/examples/Nanevski.lhs
new file mode 100644
--- /dev/null
+++ b/examples/Nanevski.lhs
@@ -0,0 +1,1149 @@
+% "Meta-programming with names and necessity" using unbound-generics
+% Aleksey Kliger
+% August 2016
+
+
+Introduction
+============
+
+This example is based on Nanevski's “Meta-programming with Names and
+Necessity”[1](http://reports-archive.adm.cs.cmu.edu/anon/2002/CMU-CS-02-123R.pdf).
+In particular, it demonstrates how to represent a language with
+multiple sorts of names (value variables, code variables, nominals and
+support variables) some with non-standard notions of substitution.
+
+As a tutorial example, we show how to represent the language and
+demonstrate its operational semantics.  Additionally, this document
+includes a typecheker and pretty printer.
+
+This file is Literate Haskell, so we start with some boilerplate.
+
+Every `unbound-generics` syntax representation needs `deriving (Show, Generic, Typeable)` declarations for all the datatypes.
+
+> {-# language DeriveDataTypeable, DeriveGeneric #-}
+
+> {-# language MultiParamTypeClasses,
+>     FlexibleContexts, FlexibleInstances, DefaultSignatures, ViewPatterns, RankNTypes,
+>     GeneralizedNewtypeDeriving #-}
+> module Nanevski where
+> import GHC.Generics (Generic)
+> import Data.Typeable (Typeable)
+> import Unbound.Generics.LocallyNameless
+> import Unbound.Generics.LocallyNameless.Internal.Fold (Fold, foldMapOf)
+> import qualified Unbound.Generics.PermM as PermM
+>
+> import Control.Monad.Except
+> import Control.Monad.State
+> import Control.Monad.Writer
+> import Control.Monad.Reader
+> import Data.List (partition, nub, sort, (\\), isSubsequenceOf)
+> import Data.Monoid (Any (..))
+> import Data.Either (partitionEithers)
+> import qualified System.IO as IO
+> import qualified Text.PrettyPrint.ANSI.Leijen as PP
+> import Text.PrettyPrint.ANSI.Leijen ()
+
+Introduction to meta-programming
+--------------------------------
+
+Meta-programming is the process of writing programs that create,
+manipulate or reason about other programs.  The meta-program is
+written in the *meta-language* and it manipulates *object-language*
+programs.
+
+In the system in this document, the object language and the
+meta-language coincide.  In general they could be different (for
+example the meta-language could be compiled down to machine code,
+while the object-language remains as some sort of abstract syntax
+trees).
+
+The type discipline of the system in this document applies both to the
+meta- and object-languages: a well-typed meta-program can only
+construct well-typed object-language programs.
+
+One important concept is the *support* of an object-language
+expression: it is the set of meta-language names that appear within
+the object-language program fragment.  The meta-language program may
+compose larger object-language fragments by substituting
+object-language expressions for the names.
+
+Example
+-------
+
+Suppose we wanted to construct the object-language cube function `“λx:int. 1 * x * x * x”`
+
+The following program constructs such a function:
+
+> -- >>> ppretty (pexp @@ number 3)
+> -- (λn:int.
+> --  choose
+> --  (νX∼int.
+> --   let □w = (Λp.
+> --             λe:□_{p} int.
+> --             rec
+> --               go (m:int) : □_{p} int
+> --               is if (□_{p} int;
+> --                      m ≤ 0;
+> --                      λ_:(). “1”;
+> --                      λ_:(). let □u = go (m + -1) in let □w = e in “⟨⟩u * ⟨⟩w”)
+> --                  ()) {X}
+> --            “X”
+> --            n in “λx:int. ⟨X ↦ x⟩w”))
+> -- 3
+
+
+Syntax
+======
+
+Types
+-----
+
+
+> data BaseType = UnitT | BoolT | IntT
+>   deriving (Typeable, Generic, Show)
+
+> data Support = Support { supportNominals :: ![Nominal],
+>                          supportVars :: ![SupportVar] }
+>   deriving (Typeable, Generic, Show)
+> type SupportVar = Name Support
+
+> data Type =
+>   BaseT BaseType          -- some base types
+>   | ArrT Type Type        -- τ₁→τ₂ functions
+>   | BoxT Type Support   -- □_C τ is the type of code of type τ with support C
+>   | NomArrT Type Type      -- τ₁ ↛ τ₂ is the type of νN:τ₁.e brings a
+>                           -- new name N associated with type τ₁ into
+>                           -- scope in a body of type τ₂.  The new
+>                           -- name cannot appear in the type τ₂ or in
+>                           -- the support of e.  It is thus
+>                           -- guaranteed to either be substituted
+>                           -- away or only appear in code in e, not
+>                           -- in subexpresisons that may be evaluated
+>                           -- in teh course of evaluating e.
+>   | ForallSupT (Bind SupportVar Type) -- support-polymorphic functions
+>   deriving (Typeable, Generic, Show)
+
+Meta-language expressions
+-------------------------
+
+> data Expr =
+>   V Var
+>   | U NominalSubst CodeVar
+>   | N Nominal
+>   | C BaseConst
+>   | P PrimOp [Value] [Expr] -- partially evaluated primop p v₁...vₙ e₁...eₘ
+>   | Lambda (Bind (Var, Embed Type) Expr)
+>   | RecFun (Bind (Var, Var, Embed Type, Embed Type) Expr) -- fun f (x : τ₁) : τ₂ = e
+>   | App Expr Expr
+>   | Let Expr (Bind Var Expr)
+>   | Box Code  -- A box expression represents some syntactic code as a data structure.
+>   | LetBox Expr (Bind CodeVar Expr)
+>   | New (Bind (Nominal, Embed Type) Expr)   -- the New operation brings names into scope; it is the job of the type system to ensure that the new name does not appear in the type of the body, nor its support.
+>   | Choose Expr
+>   | PLamSupport (Bind SupportVar Expr)
+>   | PAppSupport Expr Support
+>   deriving (Typeable, Generic, Show)
+>
+> data BaseConst = UnitC | BoolC !Bool | IntC !Int
+>   deriving (Typeable, Generic, Show)
+> data PrimOp = IfPrim Type | AddPrim | MulPrim | LeqPrim
+>   deriving (Typeable, Generic, Show)
+
+>
+> type Var = Name Expr
+
+Ordinary variables just stand for expressions.
+
+> type Value = Expr
+
+
+> isValue :: Expr -> Bool
+> isValue (C _) = True
+> isValue (Lambda _) = True
+> isValue (Box _) = True
+> isValue (New _) = True
+> isValue (PLamSupport _) = True
+> isValue _ = False
+
+Object-level Code
+-----------------
+
+Think of Code as some data structure that the expressions can build
+up.  Code is a first-class value in this language.  You can build it
+up, pass it to functions, return it as a result etc.  Code that is
+open has non-empty support is guaranteed by the type system not to be
+evaluated.  Code that is closed and has empty support , on the other
+hand may appear in expressions in positions where it may potentially
+be run.
+
+> newtype Code = Code { codeExpr :: Expr }
+>   deriving (Typeable, Generic, Show)
+> type CodeVar = Name Code
+
+Code variables stand for code, but they only occur in expressions
+together with an explicit subtitution that substitutes away some Nominals.
+
+> newtype NominalSubst = NominalSubst { nominalSubst :: [(Nominal, Nom)] }
+>   deriving (Typeable, Generic, Show)
+
+Nominals
+--------
+
+A Nominal can appear in code (but not in an expression that may be
+evaluated).  It stands for an expression just like Var, but in
+unbound-generics since we want to treat Nominal and Var distinctly, we
+add a newtype wrapper around Expr and call it a Nom.
+
+> newtype Nom = Nom {nomExpr :: Expr }
+>   deriving (Typeable, Generic, Show)
+> type Nominal = Name Nom
+
+Alpha renaming, free names, alpha-equivalence boilerplate
+---------------------------------------------------------
+
+All the types we defined will participate in various Alpha operations:
+we can collect the free Variabes, Nominals or CodeVars of all the
+syntactic categories.  They are also subject to alpha equivalence upto
+renaming of bound occurrances, etc.
+
+> instance Alpha Nom
+> instance Alpha Code
+> instance Alpha Support
+> instance Alpha NominalSubst
+> instance Alpha Type
+> instance Alpha Expr
+> instance Alpha BaseType
+> instance Alpha BaseConst
+> instance Alpha PrimOp
+
+Substitution
+============
+
+We also have notions of substitution for variables, nominals and code variables.
+
+For base types, constants and primitive operations, we give some
+catch-all substitution operations since they cannot contain any sort
+of name.
+
+> instance Subst a BaseType where
+>   subst _ _ = id
+>   substs _ = id
+>
+> instance Subst a BaseConst where
+>   subst _ _ = id
+>   substs _ = id
+>
+> instance Subst Expr PrimOp where
+>   subst _ _ = id
+>   substs _ = id
+> instance Subst Code PrimOp where
+>   subst _ _ = id
+>   substs _ = id
+> instance Subst Nom PrimOp
+> instance Subst Support PrimOp
+
+Expression substitution
+-----------------------
+
+Ordinary variables can occur in expressions as well as code, noms and
+nominal substitutions.  They don't occur in types, so we can
+short-circuit substitution there and return the type unchanged.
+
+> instance Subst Expr Type where
+>   subst _ _ = id
+>   substs _ = id
+> instance Subst Expr Expr where
+>   isvar (V v) = Just (SubstName v)
+>   isvar _ = Nothing
+> instance Subst Expr NominalSubst
+> instance Subst Expr Nom
+> instance Subst Expr Support where
+>   subst _ _ = id
+>   substs _ = id
+
+Nominal substitution
+--------------------
+
+> instance Subst Nom Nom
+> instance Subst Nom Support
+
+To substitute for a nominal N in an expression e, we use need to use
+\texttt{isCoerceVar} to pull out the expression from the Nom being
+substituted.
+
+> instance Subst Nom Expr where
+>   isCoerceVar (N n) = Just $ SubstCoerce n (Just . nomExpr)
+>   isCoerceVar _ = Nothing
+
+An important property (justified by the type system) of this language
+is that when substituting for a name N or ordinary variable v in an
+expression Box (Code e) we can just return Box (Code e) unchanged
+since the type system prevents Code from depending on the ordinary
+variable context or by using names that do not contribute to the
+support of a term.
+
+> instance Subst Nom Code where
+>   subst _ _ = id
+>   substs _ = id
+> instance Subst Expr Code where
+>   subst _ _ = id
+>   substs _ = id
+
+> instance Subst Nom Type
+> instance Subst Nom NominalSubst
+
+Code substitution
+-----------------
+
+> instance Subst Code Code
+
+We can substitute for code variables u in expressions, but since
+u's appear only together with an explicit substitution for its
+Nominals, we use \texttt{isCoerceVar} to have unbound-generics perform
+the nominal substitution.
+
+> instance Subst Code Expr where
+>   isCoerceVar (U noms u) = Just $ SubstCoerce u (Just . substituteSupported noms)
+>   isCoerceVar _ = Nothing
+>
+
+Note that in this case we peek inside a \texttt{(Code e)} using
+codeExpr. (Just using \texttt{substs (nominalSubst noms) c} would give
+us back the same unchanged syntactic object!)
+
+> substituteSupported :: NominalSubst -> Code -> Expr
+> substituteSupported noms c = substs (nominalSubst noms) (codeExpr c)
+
+> instance Subst Code NominalSubst
+> instance Subst Code Nom
+
+> instance Subst Code Type where
+>   subst _ _ = id
+>   substs _ = id
+
+> instance Subst Code Support where
+>   subst _ _ = id
+>   substs _ = id
+
+Support polymorphism substitution
+---------------------------------
+
+Support variables stand for support sets.  We have to do a bit of
+juggling to normalize the result of the substitution.
+
+> instance Subst Support Support where
+>   subst v sup sup0@(Support noms vs) =
+>     case Data.List.partition (== v) vs of
+>       ((_:_), vs') -> let
+>         noms' = sort (supportNominals sup ++ noms)
+>         vs'' = sort (supportVars sup ++ vs')
+>         in Support noms' vs''
+>       _ -> sup0
+>   substs ss (Support noms vs) =
+>     let f v = case lookup v ss of
+>           Just sup -> Left sup
+>           Nothing -> Right v
+>         (sups, vs') = partitionEithers (map f vs)
+>         noms' = sort (concatMap supportNominals sups ++ noms)
+>         vs'' = sort (concatMap supportVars sups ++ vs')
+>         in Support noms' vs''
+
+> instance Subst Support Type
+
+> instance Subst Support Expr
+> instance Subst Support Nom
+> instance Subst Support NominalSubst
+
+As with Nominals, since SupportVars stand for the support of an
+expression, and boxed code is meant to have empty support until it is
+unboxed and evaluated, the support variable substitution on code is
+the identity.
+
+> instance Subst Support Code where
+>   subst _ _ = id
+>   substs _ = id
+
+Operational Semantics
+=====================
+
+The operational semantics take configurations consisting of a context
+of Nominals together with their associated types and an expression
+with empty support to another such configuration.
+
+> data NomCtx = NilNC | SnocNC (Rebind NomCtx (Nominal, Embed Type))
+>             | SnocSupNC (NomCtx, SupportVar)
+>   deriving (Typeable, Generic, Show)
+> instance Alpha NomCtx
+
+A configuration just pairs together a nominal ctx and an expression in some manner.
+We will use a state monad. But we could also bind the names of the context in the expression.
+
+> type ClosedConfig = Bind NomCtx Expr
+
+We will need to work in a monad that also gives us fresh names and a way to signal errors
+
+> step :: (MonadError String m, MonadState NomCtx m, Fresh m) => Expr -> m Expr
+> step e0 = case e0 of
+>   V v -> evalError ("unbound variable: "  ++ show v)
+>   U _ u -> evalError ("unbound code variable: " ++ show u)
+>   N n -> evalError ("unbound name: " ++ show n)
+>   C c -> evalError ("already a value: " ++ show c)
+>   P p vs [] -> applyPrim p vs
+>   P p vs (e:es) | isValue e -> pure (P p (vs ++ [e]) es) 
+>                 | otherwise -> P p vs <$> ((:) <$> step e <*> pure es)
+>   Lambda _ -> evalError ("already a value: " ++ show e0)
+>   efun@(RecFun bnd) -> do
+>     ((f, x, t1, _), e) <- unbind bnd
+>     return $ Lambda $ bind (x, t1) (subst f efun e)
+>   Let e1 bnd | isValue e1 -> do
+>                  (x, e2) <- unbind bnd
+>                  return $ subst x e1 e2
+>   Let e1 bnd -> Let <$> step e1 <*> pure bnd
+>   Box _ -> evalError ("already a value: " ++ show e0)
+>   App e1@(Lambda bnd) e2 | isValue e2 -> do
+>                              ((x, _), ebody) <- unbind bnd
+>                              return $ subst x e2 ebody
+>                          | otherwise -> do
+>                              App e1 <$> step e2
+>   App e1 e2 -> App <$> step e1 <*> pure e2
+>   LetBox (Box c) bnd -> do
+>     (u, ebody) <- unbind bnd
+>     return $ subst u c ebody
+>   LetBox e1 bnd -> LetBox <$> step e1 <*> pure bnd
+>   New _ -> evalError ("already a value: " ++ show e0)
+>   Choose (New bnd) -> do
+>     -- In the paper there's a side-condition here that the chosen
+>     -- name has to be fresh (with respect to the nominal ctx.
+>     -- Fortunately unbound-generics will always give us a fresh
+>     -- name.
+>     (nt, ebody) <- unbind bnd
+>     modify (\ctx -> SnocNC $ rebind ctx nt)
+>     return ebody
+>   Choose e -> Choose <$> step e
+>   PLamSupport _ -> evalError ("already a value: " ++ show e0)
+>   PAppSupport (PLamSupport bnd) sup -> do
+>     (sv, ebody) <- unbind bnd
+>     return $ subst sv sup ebody
+>   PAppSupport e1 sup -> PAppSupport <$> step e1 <*> pure sup
+
+> evalError :: MonadError String m => String -> m a
+> evalError = throwError
+
+> applyPrim :: MonadError String m => PrimOp -> [Value] -> m Value
+> applyPrim (IfPrim _t) [C (BoolC b), v1, v2] = return $ if b then v1 else v2
+> applyPrim AddPrim [C (IntC x), C (IntC y)] = return $ C $ IntC $ x + y
+> applyPrim MulPrim [C (IntC x), C (IntC y)] = return $ C $ IntC $ x * y
+> applyPrim LeqPrim [C (IntC x), C (IntC y)] = return $ C $ BoolC $ x <= y
+> applyPrim p vs = evalError (show p ++ show vs ++ " does not step")
+
+> eval :: (Fresh m, MonadState NomCtx m, MonadError String m) => Expr -> m Expr
+> eval e = if isValue e then return e else step e >>= eval
+  
+Evaluation Example
+==================
+
+A little DSL for term construction
+----------------------------------
+
+> lam :: String -> Type -> (Expr -> Expr) -> Expr
+> lam s t f =
+>   let x = s2n s
+>   in Lambda $ bind (x, embed t) (f $ V x)
+
+> recFun :: String -> String -> Type -> Type -> (Expr -> Expr -> Expr) -> Expr
+> recFun sfn sx t1 t2 f =
+>   let fn = s2n sfn
+>       x = s2n sx
+>   in RecFun $ bind (fn, x, embed t1, embed t2) (f (V fn) (V x))
+
+> plam :: String -> (SupportVar -> Expr) -> Expr
+> plam s f =
+>   let sv = s2n s
+>   in PLamSupport (bind sv (f sv))
+
+> intT, unitT, boolT :: Type
+> intT = BaseT IntT
+> unitT = BaseT UnitT
+> boolT = BaseT BoolT
+> boxT :: Type -> [Nominal] -> [SupportVar] -> Type
+> boxT t noms svs = BoxT t (Support noms svs)
+> boxT_ :: Type -> [Nominal] -> Type
+> boxT_ t noms = boxT t noms []
+> arrT :: Type -> Type -> Type
+> arrT = ArrT
+> infixr 5 `arrT`
+> forallSupT :: String -> (SupportVar -> Type) -> Type
+> forallSupT s f =
+>   let sv = s2n s
+>   in ForallSupT (bind sv (f sv))
+
+> (@@) :: Expr -> Expr -> Expr
+> (@@) = App
+> infixl 5 @@
+
+> papp :: Expr -> [Nominal] -> [SupportVar] -> Expr
+> papp e noms svs = PAppSupport e (Support noms svs)
+
+> chooseNew :: String -> Type -> (Nominal -> Expr) -> Expr
+> chooseNew s t f =
+>   let n = s2n s
+>   in Choose $ New $ bind (n, embed t) (f n)
+
+> letExp :: String -> Expr -> (Expr -> Expr) -> Expr
+> letExp s e1 f =
+>   let x = s2n s
+>   in Let e1 (bind x (f $ V x))
+
+> letBox :: String -> Expr -> (CodeVar -> Expr) -> Expr
+> letBox s e1 f =
+>   let u = s2n s
+>   in LetBox e1 (bind u (f u))
+
+> box :: Expr -> Expr
+> box = Box . Code
+
+> code :: [(Nominal, Expr)] -> CodeVar -> Expr
+> code nome = U (NominalSubst $ map (fmap Nom) nome)
+
+> runCode :: CodeVar -> Expr
+> runCode = U (NominalSubst []) 
+
+> name :: Nominal -> Expr
+> name = N
+
+> number :: Int -> Expr
+> number = C . IntC 
+
+> ifLeqZ :: Type -> Expr -> Expr -> Expr -> Expr
+> ifLeqZ tres ex etrue efalse =
+>   App (P (IfPrim tres) [] [etest, thunk etrue, thunk efalse]) (C UnitC)
+>   where
+>     etest = P LeqPrim [] [ex, number 0]
+>     thunk e = lam "_" unitT (\_ -> e)
+
+> sub1 :: Expr -> Expr
+> sub1 e = P AddPrim [] [e, number (-1)]
+
+> add, mul :: Expr -> Expr -> Expr
+> add e1 e2 = P AddPrim [] [e1, e2]
+> mul e1 e2 = P MulPrim [] [e1, e2]
+
+> infixl 6 `add`
+> infixl 7 `mul`
+
+> (~~) :: a -> b -> (a, b)
+> (~~) = (,)
+> infix 5 ~~
+
+Example: Staged exponential function
+------------------------------------
+
+(Note that within the calculus itself there's not a way to abstract over a nominal like this - the example below chooses a new X which appears in the definition of this helper function.)
+
+First a little recursive helper function that expands out to the m-fold multiplication code \texttt{X * X * X * ... * 1}
+
+> exp' :: Nominal -> Expr
+> exp' nX = recFun "exp'" "m" intT (boxT_ intT [nX]) $ \exp' m ->
+>   ifLeqZ (boxT_ intT [nX]) m (box $ number 1) (letBox "u" (exp' @@ (sub1 m)) $ \u ->
+>                                      box $ mul (name nX) (runCode u))
+>   
+
+And the example exponential function takes an integer n and then constructs a piece of code consiting of a lambda abstraction whose argument x is multiplied with itself n times.
+
+> expon :: Expr
+> expon = lam "n" intT $ \n ->
+>   chooseNew "X" intT $ \nX ->
+>   letExp "exp'" (exp' nX) $ \exp' ->
+>   letBox "v"  (exp' @@ n) $ \v ->
+>   box (lam "x" intT $ \x -> code [nX ~~ x] v)
+
+Let's set up an environment for running evaluations.
+
+> run :: StateT NomCtx (ExceptT String FreshM) a -> Either String (a, NomCtx)
+> run comp = runFreshM (runExceptT (runStateT comp NilNC))
+
+Running the example \texttt{expon 3} we get the expected final
+configuration of \texttt{box (λx : int . x * x * x * 1)} and the used
+name X1 (which doesn't appear in the code, and therefore we could run
+the code).
+
+> -- >>> run (eval (expon @@ number 3))
+> -- Right (Box (Code {codeExpr = Lambda (<(x,{BaseT IntT})> P MulPrim [] [V 0@0,P MulPrim [] [V 0@0,P MulPrim [] [V 0@0,C (IntC 1)]]])}),SnocNC (<<NilNC>> (X1,{BaseT IntT})))
+
+> -- >>> run (eval (letBox "exp3" (expon @@ number 3) $ \exp3 -> (runCode exp3) @@ number 2))
+> -- Right (C (IntC 8),SnocNC (<<NilNC>> (X1,{BaseT IntT})))
+
+
+Example: Staged support-polymorphic exponential kernel
+------------------------------------------------------
+
+> pexpKernel :: Expr
+> pexpKernel = plam "p" $ \sp ->
+>   let tResult = boxT intT [] [sp]
+>   in lam "e" tResult $ \e ->
+>     recFun "go" "m" intT tResult $ \go m ->
+>     ifLeqZ tResult m (box $ number 1) (letBox "u" (go @@ (sub1 m)) $ \u ->
+>                                           letBox "w" e $ \w ->
+>                                           box $ mul (runCode u) (runCode w))
+
+> -- >>> run $ eval (papp pexpKernel [] [] @@ box (number 42) @@ number 3)
+> -- Right (Box (Code {codeExpr = P MulPrim [] [P MulPrim [] [P MulPrim [] [C (IntC 1),C (IntC 42)],C (IntC 42)],C (IntC 42)]}),NilNC)
+
+> pexp :: Expr
+> pexp = lam "n" intT $ \n ->
+>   chooseNew "X" intT $ \nX ->
+>   letBox "w" (papp pexpKernel [nX] [] @@ box (name nX) @@ n) $ \w ->
+>   box (lam "x" intT $ \x -> code [nX ~~ x] w)
+
+> -- >>> run $ eval (pexp @@ number 5)
+> -- Right (Box (Code {codeExpr = Lambda (<(x,{BaseT IntT})> P MulPrim [] [P MulPrim [] [P MulPrim [] [P MulPrim [] [P MulPrim [] [C (IntC 1),V 0@0],V 0@0],V 0@0],V 0@0],V 0@0])}),SnocNC (<<NilNC>> (X1,{BaseT IntT})))
+
+> -- >>> run $ eval (letBox "c" (pexp @@ number 5) $ \c -> runCode c @@ number 2)
+> -- Right (C (IntC 32),SnocNC (<<NilNC>> (X1,{BaseT IntT})))
+
+
+Appendix: Type checking and support inference
+=============================================
+
+> class Fresh m => TC m where
+>  lookupSupportVar :: SupportVar -> m () -- just check it exists
+>  lookupVar :: Var -> m Type
+>  lookupCodeVar :: CodeVar -> m (Type, Support)
+>  lookupNom :: Nominal -> m Type
+>  extendVar :: Var -> Type -> m a -> m a
+>  extendCodeVar :: CodeVar -> Type -> Support -> m a -> m a
+>  extendNom :: Nominal -> Type -> m a -> m a
+>  extendSupportVar :: SupportVar -> m a -> m a
+>
+>  tcError :: String -> m a
+>  default tcError :: (MonadError String m) => String -> m a
+>  tcError = throwError
+>
+>  inSupport :: Nominal -> m ()
+>  inSupport n = includeSupport (Support [n] [])
+>  includeSupport :: Support -> m ()
+>  default includeSupport :: (MonadWriter Support m) => Support -> m ()
+>  includeSupport = tell
+>
+>  -- run the subcomputation, grab its support and then completely censor it
+>  withEmptySupport :: m a -> m (a, Support)
+>  default withEmptySupport :: (MonadWriter Support m) => m a -> m (a, Support)
+>  withEmptySupport comp =
+>    let censorEverything = const mempty
+>    in pass ((\asup -> (asup, censorEverything)) <$> listen comp)
+>    
+
+> wellFormed :: TC m => Type -> m ()
+> wellFormed t0 =
+>   case t0 of
+>     BaseT {} -> return ()
+>     (ArrT t1 t2) -> wellFormed t1 >> wellFormed t2
+>     (NomArrT t1 t2) -> wellFormed t1 >> wellFormed t2
+>     (BoxT t sup) -> wellFormed t >> wellFormedSupport sup
+>     (ForallSupT bnd) -> do
+>       (sv, t) <- unbind bnd
+>       extendSupportVar sv $ wellFormed t
+>     _ -> tcError ("Unimplemented! " ++ show t0)
+
+> wellFormedSupport :: TC m => Support -> m ()
+> wellFormedSupport (Support _noms svs) = mapM_ lookupSupportVar svs
+
+> newtype Expected a = Expecting { unExpecting :: a }
+
+> inferExpr :: TC m => Expr -> m Type
+> inferExpr e = inferExpr_ e (Expecting Nothing)
+
+> expecting :: TC m => Expected (Maybe Type) -> Type -> m Type
+> expecting (Expecting Nothing) t = return t
+> expecting (Expecting (Just texp)) t = do
+>   unless (t `aeq` texp) $ tcError $ "expected type " ++ show texp ++ " but got " ++ show t
+>   return texp
+
+> expectingSup :: TC m => Expected (Maybe Support) -> Support -> m Support
+> expectingSup (Expecting Nothing) sup = return sup
+> expectingSup (Expecting (Just supexp)) sup = do
+>   unless (sup `subsup` supexp) $ tcError $ "expected support " ++ show supexp ++ " but got " ++ show sup
+>   return supexp
+
+> subsup :: Support -> Support -> Bool
+> subsup (Support noms svs) (Support noms' svs') =
+>   let nomsLeq = noms `isSubsequenceOf` noms'
+>       svsLeq = svs `isSubsequenceOf` svs'
+>   in nomsLeq && svsLeq
+
+> checkExpr :: TC m => Expr -> Type -> m ()
+> checkExpr e t = inferExpr_ e (Expecting (Just t)) >> return ()
+> 
+
+> inferExpr_ :: (TC m) => Expr -> Expected (Maybe Type) -> m Type
+> inferExpr_ e0 xpt =
+>   case e0 of
+>     V x -> lookupVar x >>= expecting xpt
+>     U noms u -> do
+>       (t, supIn) <- lookupCodeVar u
+>       checkSubst noms supIn
+>       expecting xpt t
+>     N nX -> do
+>       t <- lookupNom nX
+>       inSupport nX
+>       expecting xpt t
+>     C bc -> expecting xpt $ BaseT $ inferConst bc
+>     P primOp vs es -> do
+>       checkPrimitive primOp (vs ++ es) >>= expecting xpt
+>     Lambda bnd -> do
+>       ((x, unembed -> tDom), e) <- unbind bnd
+>       wellFormed tDom
+>       xptCod <- unExpectArrType xpt tDom
+>       tCod <- extendVar x tDom $ inferExpr_ e xptCod
+>       return (tDom `ArrT` tCod)
+>     App e1 e2 -> do
+>       tf <- inferExpr e1
+>       (tDom, tCod) <- matchArrType tf
+>       checkExpr e2 tDom
+>       expecting xpt tCod
+>     RecFun bnd -> do
+>       ((f, x, unembed -> tDom, unembed -> tCod), e) <- unbind bnd
+>       let funT = tDom `ArrT` tCod
+>       extendVar f funT $ extendVar x tDom $ checkExpr e tCod
+>       expecting xpt funT
+>     Let e1 bnd -> do
+>       t <- inferExpr e1
+>       (x, e2) <- unbind bnd
+>       extendVar x t $ inferExpr_ e2 xpt
+>     Box c -> do
+>       (xpt, xpsup) <- unExpectBoxType xpt
+>       inferCode c xpt xpsup
+>     LetBox e1 bnd -> do
+>       tbox <- inferExpr e1
+>       (t, sup) <- matchBoxType tbox
+>       (u, e2) <- unbind bnd
+>       extendCodeVar u t sup $ inferExpr_ e2 xpt
+>     New bnd -> do
+>       ((nX, unembed -> tDom), e) <- unbind bnd
+>       wellFormed tDom
+>       xptCod <- unExpectNomArrType xpt tDom
+>       (tCod, supOut) <- withEmptySupport $ extendNom nX tDom $ inferExpr_ e xptCod
+>       let inType = anyOf fv (== nX) tCod
+>           inSup = anyOf fv (== nX) (supportNominals supOut)
+>       when inType $ tcError ("Name " ++ show nX ++ " appears in the result type of a ν-expression " ++ show tCod)
+>       when inSup $ tcError ("Name " ++ show nX ++ " appears in the support of ν-expression " ++ show supOut)
+>       includeSupport supOut
+>       return (tDom `NomArrT` tCod)
+>     Choose e -> do
+>       tarr <- inferExpr e
+>       (_, tCod) <- matchNomArrType tarr
+>       expecting xpt tCod
+>     PLamSupport bnd -> do
+>       (sv, e) <- unbind bnd
+>       xptout <- unExpectForallSupType xpt sv 
+>       (t, supOut) <- withEmptySupport $ extendSupportVar sv $ inferExpr_ e xptout
+>       let inSup = anyOf fv (== sv) (supportVars supOut)
+>       when inSup $ tcError ("support variable " ++ show sv ++ " appears in the support of the body of the support-polymorphic function")
+>       includeSupport supOut
+>       expecting xpt $ ForallSupT (bind sv t)
+>     PAppSupport e sup -> do
+>       tall <- inferExpr e
+>       wellFormedSupport sup
+>       (sv, t) <- matchForallSup tall
+>       expecting xpt $ subst sv sup t
+
+> inferCode :: TC m => Code -> Expected (Maybe Type) -> Expected (Maybe Support) -> m Type
+> inferCode (Code e) xpt xpsup = do
+>   (t, supOut) <- withEmptySupport (inferExpr_ e xpt)
+>   BoxT t <$> expectingSup xpsup supOut
+
+> matchArrType :: TC m => Type -> m (Type, Type)
+> matchArrType (ArrT tdom tcod) = return (tdom, tcod)
+> matchArrType t0 = tcError ("Expected an expression of function type, got " ++ show t0)
+
+> matchNomArrType :: TC m => Type -> m (Type, Type)
+> matchNomArrType (NomArrT tdom tcod) = return (tdom, tcod)
+> matchNomArrType t0 = tcError ("Expected an expression of nominal-function type, got " ++ show t0)
+
+> matchForallSup :: TC m => Type -> m (SupportVar, Type)
+> matchForallSup (ForallSupT bnd) = unbind bnd
+> matchForallSup t0 = tcError ("Expected a support-polymorphic type, got " ++ show t0)
+
+> matchBoxType :: TC m => Type -> m (Type, Support)
+> matchBoxType (BoxT t sup) = return (t, sup)
+> matchBoxType t0 = tcError ("Expected an expression of code type, got " ++ show t0)
+
+> unExpectArrType :: TC m => Expected (Maybe Type) -> Type -> m (Expected (Maybe Type))
+> unExpectArrType (Expecting Nothing) _ = return (Expecting Nothing)
+> unExpectArrType (Expecting (Just texp)) t' = do
+>   (tdom, tcod) <- matchArrType texp
+>   expecting (Expecting (Just tdom)) t'
+>   return (Expecting (Just tcod))
+
+> unExpectNomArrType :: TC m => Expected (Maybe Type) -> Type -> m (Expected (Maybe Type))
+> unExpectNomArrType (Expecting Nothing) _ = return (Expecting Nothing)
+> unExpectNomArrType (Expecting (Just texp)) t' = do
+>   (tdom, tcod) <- matchNomArrType texp
+>   expecting (Expecting (Just tdom)) t'
+>   return (Expecting (Just tcod))
+
+> unExpectForallSupType :: TC m => Expected (Maybe Type) -> SupportVar -> m (Expected (Maybe Type))
+> unExpectForallSupType (Expecting Nothing) _ = return (Expecting Nothing)
+> unExpectForallSupType (Expecting (Just texp)) sv = do
+>   (sv', t) <- matchForallSup texp
+>   return (Expecting (Just (swaps (PermM.single (AnyName sv) (AnyName sv')) t)))
+
+> unExpectBoxType :: TC m => Expected (Maybe Type) -> m (Expected (Maybe Type), Expected (Maybe Support))
+> unExpectBoxType (Expecting Nothing) = return (Expecting Nothing, Expecting Nothing)
+> unExpectBoxType (Expecting (Just t)) = do
+>   (t', sup) <- matchBoxType t
+>   return (Expecting (Just t'), Expecting (Just sup))
+
+> inferConst :: BaseConst -> BaseType
+> inferConst UnitC = UnitT
+> inferConst (BoolC _) = BoolT
+> inferConst (IntC _) = IntT
+
+> checkPrimitive :: TC m => PrimOp -> [Expr] -> m Type
+> checkPrimitive (IfPrim t) [e, thunk1, thunk2] = do
+>   wellFormed t
+>   let thunkT = unitT `ArrT` t
+>   checkExpr e boolT
+>   checkExpr thunk1 thunkT
+>   checkExpr thunk2 thunkT
+>   return thunkT
+> checkPrimitive (IfPrim _) es = tcError $ "if expression expected 2 branches, got " ++ show (length es)
+> checkPrimitive AddPrim [e1,e2] = checkExpr e1 intT >> checkExpr e2 intT >> return intT
+> checkPrimitive AddPrim es = binOpPrimitiveError AddPrim es
+> checkPrimitive MulPrim [e1,e2] = checkExpr e1 intT >> checkExpr e2 intT >> return intT
+> checkPrimitive MulPrim es = binOpPrimitiveError MulPrim es
+> checkPrimitive LeqPrim [e1,e2] = checkExpr e1 intT >> checkExpr e2 intT >> return boolT
+> checkPrimitive LeqPrim es = binOpPrimitiveError LeqPrim es
+>
+> binOpPrimitiveError :: TC m => PrimOp -> [Expr] -> m a
+> binOpPrimitiveError p es = tcError $ "expected 2 arguments to " ++ show p ++ ", got " ++ show (length es)
+
+
+> checkSubst :: (TC m) => NominalSubst -> Support -> m ()
+> checkSubst = go . nominalSubst
+>   where
+>     go :: (TC m) => [(Nominal, Nom)] -> Support -> m ()
+>     go [] = includeSupport
+>     go ((nX, ne):noms) = \supIn -> do
+>       t <- lookupNom nX
+>       checkExpr (nomExpr ne) t
+>       go noms (supIn `excludingNominal` nX)
+
+> excludingNominal :: Support -> Nominal -> Support
+> excludingNominal (Support noms svs) nX = Support (noms \\ [nX]) svs
+
+> instance Monoid Support where
+>   mempty = Support [] []
+>   (Support noms svs) `mappend` (Support noms' svs') = Support noms'' svs''
+>     where
+>       noms'' = nub $ sort (noms ++ noms')
+>       svs'' = nub $ sort (svs ++ svs')
+
+> anyOf :: Fold s a -> (a -> Bool) -> s -> Bool
+> anyOf l f =  getAny . foldMapOf l (Any . f)
+
+> data Env = Env { envSigma :: NomCtx, envDelta :: [(CodeVar, Embed (Type, Support))], envGamma :: [(Var, Embed Type)] }
+
+> newtype TypeCheck a = TypeCheck { unTypeCheck :: ReaderT Env (WriterT Support (ExceptT String FreshM)) a }
+>                     deriving (Functor, Applicative, Monad, Fresh)
+
+> hasSupportNomCtx :: SupportVar -> NomCtx -> Bool
+> hasSupportNomCtx  _ NilNC = False
+> hasSupportNomCtx sv (SnocNC (unrebind -> (ctx, _))) = hasSupportNomCtx sv ctx
+> hasSupportNomCtx sv (SnocSupNC (ctx, sv')) | sv == sv' = True
+>                                            | otherwise = hasSupportNomCtx sv ctx
+>   
+
+> lookupNominalNomCtx :: Nominal -> NomCtx -> Maybe (Embed Type)
+> lookupNominalNomCtx _ NilNC = Nothing
+> lookupNominalNomCtx nX (SnocNC (unrebind -> (ctx, (nY, t)))) | nX == nY = Just t
+>                                                              | otherwise = lookupNominalNomCtx nX ctx
+> lookupNominalNomCtx nX (SnocSupNC (ctx, _)) = lookupNominalNomCtx nX ctx
+
+> instance TC TypeCheck where
+>   lookupSupportVar sv = do
+>     b <- TypeCheck $ asks (hasSupportNomCtx sv . envSigma)
+>     unless b $ tcError ("Support variable " ++ show sv ++ " not in scope")
+>   lookupVar x = do
+>     m <- TypeCheck $ asks (lookup x . envGamma)
+>     case m of
+>       Just t -> return (unembed t)
+>       Nothing -> tcError ("Variable " ++ show x ++ " not in scope")
+>   lookupCodeVar u = do
+>     m <- TypeCheck $ asks (lookup u . envDelta)
+>     case m of
+>       Just ts -> return (unembed ts)
+>       Nothing -> tcError ("Code variable " ++ show u ++ " not in scope")
+>   lookupNom nX = do
+>     m <- TypeCheck $ asks (lookupNominalNomCtx nX . envSigma)
+>     case m of
+>       Just t -> return (unembed t)
+>       Nothing -> tcError ("Nominal " ++ show nX ++ " not in scope")
+>   extendVar x t = TypeCheck . local (\env -> env { envGamma = (x, embed t) : envGamma env  }) . unTypeCheck
+>   extendCodeVar u t sup = TypeCheck . local (\env -> env { envDelta = (u, embed (t, sup)) : envDelta env } ) . unTypeCheck
+>   extendNom nX t = TypeCheck . local (\env -> env { envSigma = SnocNC (rebind (envSigma env) (nX, embed t)) } ) . unTypeCheck
+>   extendSupportVar sv = TypeCheck . local (\env -> env { envSigma = SnocSupNC (envSigma env, sv) } ) . unTypeCheck
+> 
+>   tcError = TypeCheck . throwError
+>
+>   includeSupport = TypeCheck . tell
+>
+>   withEmptySupport comp =
+>     let censorEverything = const mempty
+>     in TypeCheck (pass ((\asup -> (asup, censorEverything)) <$> listen (unTypeCheck comp)))
+
+> inferClosedConfig :: TC m => ClosedConfig -> m Type
+> inferClosedConfig bnd = do
+>   (ctx, expr) <- unbind bnd
+>   inferConfiguration ctx expr
+
+> inferConfiguration :: TC m => NomCtx -> Expr -> m Type
+> inferConfiguration ctx = inWellFormedNomCtx ctx . inferExpr
+
+> inWellFormedNomCtx :: TC m => NomCtx -> m a -> m a
+> inWellFormedNomCtx NilNC = id
+> inWellFormedNomCtx (SnocNC (unrebind -> (ctx, (nX, unembed -> t)))) = \k ->
+>   inWellFormedNomCtx ctx $ do
+>   wellFormed t
+>   extendNom nX t k
+> inWellFormedNomCtx (SnocSupNC (ctx,sv)) = inWellFormedNomCtx ctx . extendSupportVar sv 
+
+> runTypeCheck :: TypeCheck a -> Either String (a, Support)
+> runTypeCheck comp = runFreshM (runExceptT (runWriterT (runReaderT (unTypeCheck comp) emptyEnv)))
+>   where emptyEnv = Env emptySigma emptyDelta emptyGamma
+>         emptySigma = NilNC
+>         emptyDelta = []
+>         emptyGamma = []
+
+Appendix: Pretty Printing
+==========================
+
+We need our own pretty printer class because we want locally fresh
+names when we descened under binders.
+
+> type Precedence = Int
+
+> class Pretty a where
+>   pp :: LFresh m => a -> Precedence -> m PP.Doc
+
+> paren :: Functor m => Bool -> m PP.Doc -> m PP.Doc
+> paren b = if b then fmap PP.parens else id
+
+> lowest, quantBodyPrec, arrPrec, arrPrecLeft, boxPrec, quantPrec :: Precedence
+> lowest = -1
+> quantBodyPrec = 2
+> arrPrec = 5
+> arrPrecLeft = 6
+> boxPrec = 9
+> quantPrec = 2
+
+> lamBodyPrec, appPrec :: Precedence
+> semiPrec = 1
+> letBodyPrec = 1
+> lamBodyPrec = 2
+> leqPrec = 3
+> addPrec = 4
+> addPrecRight = 5
+> mulPrec = 5
+> mulPrecRight = 6
+> lambdaPrec = 7
+> letPrec = 7
+> bindingPrec = 8
+> appPrec = 10
+
+> instance Pretty BaseType where
+>   pp b _p = pure $ PP.text $ case b of
+>     UnitT -> "()"
+>     BoolT -> "bool"
+>     IntT  -> "int"
+
+> instance Pretty Type where
+>   pp t0 p = case t0 of
+>     BaseT b -> pp b lowest
+>     ArrT t1 t2 -> paren (p > arrPrec) (infixBinary <$> pp t1 arrPrecLeft <*> pure (PP.text "→") <*> pp t2 arrPrec)
+>     NomArrT t1 t2 -> paren (p > arrPrec) (infixBinary <$> pp t1 arrPrecLeft <*> pure (PP.text "↛") <*> pp t2 arrPrec)
+>     BoxT t sup -> paren (p > boxPrec) (ppboxType <$> pp t boxPrec <*> pp sup lowest)
+>     ForallSupT bnd -> paren (p > quantPrec) (quantifier "∀" <$> lunbind bnd (\(sv, t) -> (,) <$> pp sv lowest <*> pp t quantBodyPrec))
+
+> instance Pretty Support where
+>   pp (Support noms svs) _dk = ppsupport <$> traverse (fmap decorNominal . flip pp lowest) noms <*> traverse (fmap decorSupportVar . flip pp lowest) svs
+
+> decorSupportVar :: PP.Doc -> PP.Doc
+> decorSupportVar = PP.dullblue
+
+> decorCodeVar :: PP.Doc -> PP.Doc
+> decorCodeVar = PP.dullmagenta
+
+> decorNominal :: PP.Doc -> PP.Doc
+> decorNominal = PP.bold
+
+> instance Pretty (Name a) where
+>   pp a _dk = pure $ PP.text $ show a
+
+> ppboxType :: PP.Doc -> PP.Doc -> PP.Doc
+> ppboxType t sup = PP.hang 2 (PP.text "□_" PP.<> sup PP.</> PP.group t)
+
+> ppsupport :: [PP.Doc] -> [PP.Doc] -> PP.Doc
+> ppsupport noms svs = PP.group $ PP.hang 2 $ PP.braces $ PP.fillSep $ PP.punctuate PP.comma (noms ++ svs)
+
+
+> infixBinary :: PP.Doc -> PP.Doc -> PP.Doc -> PP.Doc
+> infixBinary p1 s p2 = PP.group $ PP.fillSep [p1, s, p2]
+
+> quantifier :: String -> (PP.Doc, PP.Doc) -> PP.Doc
+> quantifier q (obj, body) = PP.text q PP.<//> obj PP.<//> PP.dot PP.<//> body
+
+> instance Pretty Expr where
+>   pp e0 p = case e0 of
+>     V x -> pp x lowest
+>     U subs u -> (PP.<>) <$> pp subs lowest <*> (fmap decorCodeVar . flip pp lowest) u
+>     N nom -> decorNominal <$> pp nom lowest
+>     C c -> pp c lowest
+>     P prim vs es -> paren (p > primPrecedence prim) (ppPrimitive prim (vs ++ es))
+>     Lambda bnd -> paren (p > lambdaPrec) (pplambda "λ" <$> lunbind bnd (\((x, unembed -> t), e) -> (,) <$> (colonclass <$> pp x lowest <*> pp t lowest) <*> pp e lamBodyPrec))
+>     RecFun bnd -> paren (p > lambdaPrec) (pprecfun <$> lunbind bnd (\((f, x, unembed -> targ, unembed -> tres), e) -> (,,,,) <$> pp f lowest <*> pp x lowest <*> pp targ lowest <*> pp tres lowest <*> pp e lamBodyPrec ))
+>     App e1 e2 -> paren (p > appPrec) (ppapp <$> pp e1 appPrec <*> pp e2 (appPrec + 1))
+>     Let e1 bnd -> paren (p > letPrec) (pplet PP.empty <$> pp e1 bindingPrec <*> lunbind bnd (\(x, e2) -> (,) <$> pp x lowest <*> pp e2 letBodyPrec))
+>     LetBox e1 bnd -> paren (p > letPrec) (pplet (PP.text "□") <$> pp e1 bindingPrec <*> lunbind bnd (\(u, e2) -> (,) <$> (fmap decorCodeVar . flip pp lowest) u <*> pp e2 letBodyPrec))
+>     Box code -> pp code lowest
+>     New bnd -> paren (p > lambdaPrec) (pplambda "ν" <$> lunbind bnd (\((nX, unembed -> t), e) -> (,) <$> ppnombind nX t <*> pp e lamBodyPrec))
+>     Choose e -> paren (p > appPrec) (ppapp (PP.text "choose") <$> pp e appPrec)
+>     PLamSupport bnd -> paren (p > lambdaPrec) (pplambda "Λ" <$> lunbind bnd (\(sv, e) -> (,) <$> (fmap decorSupportVar . flip pp lowest) sv <*> pp e lamBodyPrec))
+>     PAppSupport e sup -> paren (p > appPrec) (PP.nest 2 <$> ((PP.</>) <$> (fmap PP.group . flip pp appPrec) e <*> pp sup lowest))
+
+> ppnombind nX t = assocclass <$> fmap decorNominal (pp nX lowest) <*> pp t lowest
+
+> instance Pretty Code where
+>   pp (Code e) _dk = ppcode <$> pp e lowest
+>     where
+>       ppcode c = PP.enclose (PP.text "“") (PP.text "”") (PP.underline c)
+
+> instance Pretty BaseConst where
+>   pp bc _dk = pure $ case bc of
+>     UnitC -> PP.text "()"
+>     BoolC b -> PP.text $ show b
+>     IntC i -> PP.int i
+
+> primPrecedence :: PrimOp -> Precedence
+> primPrecedence (IfPrim _) = appPrec
+> primPrecedence AddPrim = addPrec
+> primPrecedence MulPrim = mulPrec
+> primPrecedence LeqPrim = leqPrec
+>
+> ppPrimitive :: LFresh m => Pretty a => PrimOp -> [a] -> m PP.Doc
+> ppPrimitive (IfPrim t) es = do
+>   let prettyExpr = fmap PP.group . flip pp semiPrec
+>   pes <- traverse prettyExpr es
+>   pt <- pp t lowest
+>   return $ PP.group (PP.text "if" PP.</> (PP.parens $ PP.group $ PP.align $ PP.vsep $ PP.punctuate PP.semi (pt:pes)))
+> ppPrimitive AddPrim [e1,e2] = infixBinary <$> pp e1 addPrec <*> pure (PP.text "+") <*> pp e2 addPrecRight
+> ppPrimitive MulPrim [e1,e2] = infixBinary <$> pp e1 mulPrec <*> pure (PP.text "*") <*> pp e2 mulPrecRight
+> ppPrimitive LeqPrim [e1,e2] = infixBinary <$> pp e1 leqPrec <*> pure (PP.text "≤") <*> pp e2 leqPrec
+> ppPrimitive _ _ = error "cant' happen (in well-typed code)"
+
+> colonclass :: PP.Doc -> PP.Doc -> PP.Doc
+> colonclass v clas = v PP.<//> PP.colon PP.<//> clas
+
+> assocclass :: PP.Doc -> PP.Doc -> PP.Doc
+> assocclass v clas = v PP.<//> PP.text "∼" PP.<//> clas
+
+> pplambda :: String -> (PP.Doc, PP.Doc) -> PP.Doc
+> pplambda lam (vclas, body) = PP.group $ PP.align $ PP.vsep [PP.group (PP.vcat [PP.text lam, vclas, PP.dot]), PP.group body]
+
+> ppapp :: PP.Doc -> PP.Doc -> PP.Doc
+> ppapp e1 e2 = PP.group $ PP.align $ PP.vsep [PP.group e1, PP.nest 2 (PP.group e2)]
+
+> pprecfun :: (PP.Doc, PP.Doc, PP.Doc, PP.Doc, PP.Doc) -> PP.Doc
+> pprecfun (f, x, targ, tres, e) = PP.group $ PP.hang 2 $ PP.vsep [PP.text "rec", PP.group (PP.sep [f, binding, PP.colon, tres]), PP.group (PP.text "is" PP.</> PP.nest 2 (PP.group e))]
+>   where
+>     binding = PP.parens (colonclass x targ)
+
+> pplet :: PP.Doc -> PP.Doc -> (PP.Doc, PP.Doc) -> PP.Doc
+> pplet unclas e1 (x,e2) = PP.fillSep [PP.text "let", PP.hang 2 binding] PP.</> PP.group (PP.hang 2 (PP.text "in" PP.</> PP.nest 2 e2))
+>   where
+>     binding = PP.group (PP.fillSep [unclas PP.<//> x, PP.text "="] PP.</> PP.hang 2 e1)
+
+> instance Pretty NominalSubst where
+>   pp (NominalSubst subs) _dk =
+>     ppsubstitution <$> traverse ppsub subs
+>     where
+>       ppsubstitution = PP.enclose (PP.text "⟨") (PP.text "⟩") . PP.fillSep . PP.punctuate PP.comma
+>       ppsub (nX, nom) = mapto <$> (fmap decorNominal . flip pp lowest) nX <*> pp nom lowest
+>       mapto nX nom = PP.group (nX PP.</> PP.text "↦") PP.</> nom
+
+> instance Pretty Nom where
+>   pp = pp . nomExpr
+
+> pretty :: Pretty a => a -> String
+> pretty a = flip PP.displayS "" $ PP.renderSmart 0.8 80 $ runLFreshM $ pp a lowest
+
+> ppretty :: Pretty a => a -> IO ()
+> ppretty a = do
+>   PP.displayIO IO.stdout $ PP.renderSmart 0.8 80 $ runLFreshM $ pp a lowest
+>   putStrLn ""
+
+Example
+-------
+
+> -- >>> ppretty (pexp @@ number 3)
+> -- (λn:int.
+> -- choose
+> --  (νX∼int.
+> --   let □w = (Λp.
+> --             λe:□_{p} int.
+> --             rec
+> --               go (m:int) : □_{p} int
+> --               is if (□_{p} int;
+> --                      m ≤ 0;
+> --                      λ_:(). “1”;
+> --                      λ_:(). let □u = go (m + -1) in let □w = e in “⟨⟩u * ⟨⟩w”)
+> --                  ()) {X}
+> --            “X”
+> --            n in “λx:int. ⟨X ↦ x⟩w”))
+> -- 3
+
+Appendix: Tracing evaluator
+===========================
+
+> instance Pretty NomCtx where
+>   pp NilNC _ = pure PP.empty
+>   pp (SnocNC (unrebind -> (NilNC, (nX, unembed -> t)))) _ = ppnombind nX t
+>   pp (SnocNC (unrebind -> (ctx, (nX, unembed -> t)))) _ = (PP.</>) <$> fmap (\pctx -> pctx PP.</> PP.comma) (pp ctx lowest) <*> ppnombind nX t
+>   pp (SnocSupNC (NilNC, sv)) _ = decorSupportVar <$> pp sv lowest
+>   pp (SnocSupNC (ctx, sv)) _ = (PP.</>) <$> fmap (\pctx -> pctx PP.</> PP.comma) (pp ctx lowest) <*> (decorSupportVar <$> pp sv lowest)
+
+> data WellTypedProgram = WellTypedProgram NomCtx Expr Type Support
+>
+> instance Pretty WellTypedProgram where
+>   pp (WellTypedProgram ctx e t sup) _ = do
+>     pctx <- pp ctx lowest
+>     pe <- pp e lowest
+>     pt <- pp t lowest
+>     psup <- pp sup lowest
+>     return $ PP.group $ PP.vcat [pctx, PP.text "⊢", pe, PP.nest 2 PP.colon, PP.nest 4 pt, PP.nest 4 psup]
+
+> traceProgram :: Expr -> IO ()
+> traceProgram initialExpr = do
+>   let tc ctx e = case runTypeCheck (inferConfiguration ctx e) of
+>         Right (t, sup) -> ppretty (WellTypedProgram ctx e t sup)
+>         Left err -> putStrLn err >> fail "(Not running)"
+>   let
+>     trace :: (Fresh m, MonadState NomCtx m, MonadError String m, MonadIO m) => Expr -> m ()
+>     trace e =
+>         if isValue e
+>         then return ()
+>         else
+>         do
+>           e' <- step e
+>           ctx <- get
+>           liftIO $ do
+>             tc ctx e'
+>             putStrLn "————"
+>           trace e'
+>   tc NilNC initialExpr
+>   putStrLn "————"
+>   _ <- runFreshMT (runExceptT (runStateT (trace initialExpr) NilNC))
+>   return ()
+> _ = ()
+
+
diff --git a/examples/Prof.hs b/examples/Prof.hs
new file mode 100644
--- /dev/null
+++ b/examples/Prof.hs
@@ -0,0 +1,42 @@
+{-# language GADTs, RankNTypes #-}
+module Prof where
+
+import Data.Profunctor
+
+data Shop a b s t where
+  Shop :: (s -> a) -> (s -> b -> t) -> Shop a b s t
+
+type Optic p s t a b  = p a b -> p s t
+type Lens s t a b = forall p . (Strong p) => Optic p s t a b
+
+lens :: (s -> a) -> (s -> b -> t) -> Lens s t a b
+lens get set pab = dimap (\s -> (s, get s)) (uncurry set) (second' pab)
+
+instance Profunctor (Shop a b) where
+  dimap f g (Shop get set) = Shop (get . f) (\s -> g . set (f s))
+
+instance Strong (Shop a b) where
+   first' (Shop get set) = Shop (get . fst) (\(s,c) b -> (set s b, c))
+
+withLens :: Lens s t a b -> ((s -> a) -> (s -> b -> t) -> r) -> r
+withLens l k = case l (Shop id (const id)) of
+                 Shop getter setter -> k getter setter
+
+
+type Prism s t a b = forall p . (Choice p) => Optic p s t a b
+
+prism :: (s -> Either t a) -> (b -> t) -> Prism s t a b
+prism view review pab = dimap view (either id review) (right' pab)
+
+data Market a b s t where
+  Market :: (s -> Either t a) -> (b -> t) -> Market a b s t
+
+instance Profunctor (Market a b) where
+  dimap f g (Market view review) = Market (either (Left . g) Right . (view . f)) (g . review)
+
+instance Choice (Market a b) where
+  left' (Market view review) = Market (either (either (Left . Left) Right . view) (Left . Right)) (Left . review)
+
+withPrism :: Prism s t a b -> ((s -> Either t a) -> (b -> t) -> r) -> r
+withPrism l k = case l (Market Right id) of
+                  Market view review -> k view review
diff --git a/src/Unbound/Generics/LocallyNameless/Alpha.hs b/src/Unbound/Generics/LocallyNameless/Alpha.hs
--- a/src/Unbound/Generics/LocallyNameless/Alpha.hs
+++ b/src/Unbound/Generics/LocallyNameless/Alpha.hs
@@ -58,8 +58,9 @@
 import Data.Functor.Contravariant (Contravariant(..))
 import Data.Foldable (Foldable(..))
 import Data.List (intersect)
-import Data.Monoid (Monoid(..), (<>), All(..))
+import Data.Monoid (Monoid(..), All(..))
 import Data.Ratio (Ratio)
+import Data.Semigroup as Sem
 import Data.Typeable (Typeable, gcast, typeOf)
 import GHC.Generics
 
@@ -117,13 +118,17 @@
 -- @
 newtype DisjointSet a = DisjointSet (Maybe [a])
 
-instance Eq a => Monoid (DisjointSet a) where
-  mempty = DisjointSet (Just [])
-  mappend s1 s2 =
+-- | @since 0.3.2
+instance Eq a => Sem.Semigroup (DisjointSet a) where
+  (<>) = \s1 s2 ->
     case (s1, s2) of
       (DisjointSet (Just xs), DisjointSet (Just ys)) | disjointLists xs ys -> DisjointSet (Just (xs <> ys))
       _ -> inconsistentDisjointSet
 
+instance Eq a => Monoid (DisjointSet a) where
+  mempty = DisjointSet (Just [])
+  mappend = (<>)
+
 instance Foldable DisjointSet where
   foldMap summarize (DisjointSet ms) = foldMap (foldMap summarize) ms
 
@@ -262,12 +267,13 @@
   {-# INLINE fmap #-}
 
 instance Applicative (FFM f) where
-  pure = return
+  pure x = FFM (\r _j -> r x)
+  {-# INLINE pure #-}
   (FFM h) <*> (FFM k) = FFM (\r j -> h (\f -> k (r . f) j) j)
   {-# INLINE (<*>) #-}
 
 instance Monad (FFM f) where
-  return x = FFM (\r _j -> r x)
+  return = pure
   {-# INLINE return #-}
   (FFM h) >>= f = FFM (\r j -> h (\x -> runFFM (f x) r j) j)
   {-# INLINE (>>=) #-}
@@ -291,13 +297,17 @@
 -- is the @i@th name in @a@
 newtype NthPatFind = NthPatFind { runNthPatFind :: Integer -> Either Integer AnyName }
 
-instance Monoid NthPatFind where
-  mempty = NthPatFind Left
-  mappend (NthPatFind f) (NthPatFind g) =
+-- | @since 0.3.2
+instance Sem.Semigroup NthPatFind where
+  (<>) = \(NthPatFind f) (NthPatFind g) ->
     NthPatFind $ \i -> case f i of
     Left i' -> g i'
     found@Right {} -> found
 
+instance Monoid NthPatFind where
+  mempty = NthPatFind Left
+  mappend = (<>)
+
 -- | The result of @'namePatFind' a x@ is either @Left i@ if @a@ is a pattern that
 -- contains @i@ free names none of which are @x@, or @Right j@ if @x@ is the @j@th name
 -- in @a@
@@ -306,14 +316,18 @@
                                                       -- Right - index of the name we found
                                                       -> Either Integer Integer }
 
-instance Monoid NamePatFind where
-  mempty = NamePatFind (\_ -> Left 0)
-  mappend (NamePatFind f) (NamePatFind g) =
+-- | @since 0.3.2
+instance Sem.Semigroup NamePatFind where
+  (<>) = \(NamePatFind f) (NamePatFind g) ->
     NamePatFind $ \nm -> case f nm of
     ans@Right {} -> ans
     Left n -> case g nm of
       Left m -> Left $! n + m
       Right i -> Right $! n + i
+
+instance Monoid NamePatFind where
+  mempty = NamePatFind (\_ -> Left 0)
+  mappend = (<>)
 
 -- | The "Generic" representation version of 'Alpha'
 class GAlpha f where
diff --git a/src/Unbound/Generics/LocallyNameless/Fresh.hs b/src/Unbound/Generics/LocallyNameless/Fresh.hs
--- a/src/Unbound/Generics/LocallyNameless/Fresh.hs
+++ b/src/Unbound/Generics/LocallyNameless/Fresh.hs
@@ -19,6 +19,7 @@
 
 import Control.Monad.Identity
 
+import Control.Monad.Catch (MonadThrow, MonadCatch, MonadMask)
 import Control.Monad.Trans
 import Control.Monad.Trans.Except
 import Control.Monad.Trans.Error
@@ -53,7 +54,18 @@
 --   still globally unused, and increments the index every time it is
 --   asked for a fresh name.
 newtype FreshMT m a = FreshMT { unFreshMT :: St.StateT Integer m a }
-  deriving (Functor, Applicative, Alternative, Monad, MonadPlus, MonadIO, MonadFix)
+  deriving
+    ( Functor
+    , Applicative
+    , Alternative
+    , Monad
+    , MonadIO
+    , MonadPlus
+    , MonadFix
+    , MonadThrow
+    , MonadCatch
+    , MonadMask
+    )
 
 -- | Run a 'FreshMT' computation (with the global index starting at zero).
 runFreshMT :: Monad m => FreshMT m a -> m a
diff --git a/src/Unbound/Generics/LocallyNameless/LFresh.hs b/src/Unbound/Generics/LocallyNameless/LFresh.hs
--- a/src/Unbound/Generics/LocallyNameless/LFresh.hs
+++ b/src/Unbound/Generics/LocallyNameless/LFresh.hs
@@ -63,6 +63,7 @@
 import Data.Monoid
 import Data.Typeable (Typeable)
 
+import Control.Monad.Catch (MonadThrow, MonadCatch, MonadMask)
 import Control.Monad.Reader
 import Control.Monad.Identity
 import Control.Applicative (Applicative, Alternative)
@@ -102,7 +103,18 @@
 -- avoid, and when asked for a fresh one will choose the first numeric
 -- prefix of the given name which is currently unused.
 newtype LFreshMT m a = LFreshMT { unLFreshMT :: ReaderT (Set AnyName) m a }
-  deriving (Functor, Applicative, Alternative, Monad, MonadIO, MonadPlus, MonadFix)
+  deriving
+    ( Functor
+    , Applicative
+    , Alternative
+    , Monad
+    , MonadIO
+    , MonadPlus
+    , MonadFix
+    , MonadThrow
+    , MonadCatch
+    , MonadMask
+    )
 
 -- | Run an 'LFreshMT' computation in an empty context.
 runLFreshMT :: LFreshMT m a -> m a
diff --git a/src/Unbound/Generics/PermM.hs b/src/Unbound/Generics/PermM.hs
--- a/src/Unbound/Generics/PermM.hs
+++ b/src/Unbound/Generics/PermM.hs
@@ -47,9 +47,10 @@
   ) where
 
 import Prelude (Eq(..), Show(..), (.), ($), Monad(return), Ord(..), Maybe(..), otherwise, (&&), Bool(..), id, uncurry, Functor(..))
-import Data.Monoid
+import Data.Monoid hiding ((<>))
 import Data.List
 import Data.Map (Map)
+import Data.Semigroup as Sem
 import qualified Data.Map as M
 import qualified Data.Set as S
 import Control.Arrow ((&&&))
@@ -97,10 +98,15 @@
   Perm (M.fromList ([ (x,M.findWithDefault y y b) | (x,y) <- M.toList a]
          ++ [ (x, M.findWithDefault x x b) | x <- M.keys b, M.notMember x a]))
 
--- | Permutations form a monoid under composition.
+-- | Permutations form a semigroup under 'compose'.
+-- @since 0.3.2
+instance Ord a => Sem.Semigroup (Perm a) where
+  (<>) = compose
+
+-- | Permutations form a monoid with identity 'empty'.
 instance Ord a => Monoid (Perm a) where
   mempty  = empty
-  mappend = compose
+  mappend = (<>)
 
 -- | Is this the identity permutation?
 isid :: Ord a => Perm a -> Bool
diff --git a/unbound-generics.cabal b/unbound-generics.cabal
--- a/unbound-generics.cabal
+++ b/unbound-generics.cabal
@@ -2,7 +2,7 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                unbound-generics
-version:             0.3.1
+version:             0.3.2
 synopsis:            Support for programming with names and binders using GHC Generics
 description:         Specify the binding structure of your data type with an
                      expressive set of type combinators, and unbound-generics
@@ -12,7 +12,7 @@
                      @Unbound.Generics.LocallyNameless@ to get started.
                      .
                      This is an independent re-implementation of <http://hackage.haskell.org/package/unbound Unbound>
-                     but using <http://www.haskell.org/ghc/docs/latest/html/libraries/base-4.9.0.0/GHC-Generics.html GHC.Generics>
+                     but using <https://hackage.haskell.org/package/base/docs/GHC-Generics.html GHC.Generics>
                      instead of <http://hackage.haskell.org/package/RepLib RepLib>.
                      See the accompanying README for some porting notes.
                      
@@ -22,14 +22,14 @@
 license-file:        LICENSE
 author:              Aleksey Kliger
 maintainer:          aleksey@lambdageek.org
-copyright:           (c) 2014-2016, Aleksey Kliger
+copyright:           (c) 2014-2018, Aleksey Kliger
 category:            Language
 build-type:          Simple
-extra-source-files:  examples/*.hs,
+extra-source-files:  examples/*.hs, examples/*.lhs,
                      README.md,
                      Changelog.md
 cabal-version:       >=1.10
-tested-with: GHC == 7.6.3, GHC == 7.8.4, GHC == 7.10.3, GHC == 8.0.1
+tested-with: GHC == 7.6.3, GHC == 7.8.4, GHC == 7.10.3, GHC == 8.0.1, GHC == 8.2.2, GHC == 8.4.1
              
 library
   exposed-modules:     Unbound.Generics.LocallyNameless
@@ -54,16 +54,22 @@
   -- other-extensions:    
   build-depends:       base >=4.6 && <5,
                        template-haskell >= 2.8.0.0,
-                       deepseq >= 1.3,
+                       deepseq >= 1.3.0.0,
                        mtl >= 2.1,
                        transformers >= 0.3,
                        transformers-compat >= 0.3,
                        containers == 0.5.*,
                        contravariant >= 0.5,
-                       profunctors >= 4.0
+                       profunctors >= 4.0,
+                       ansi-wl-pprint >= 0.6.7.2 && < 0.7,
+                       exceptions >= 0.8 && < 0.9
   hs-source-dirs:      src
   default-language:    Haskell2010
   ghc-options:         -Wall
+  if impl (ghc >= 8.0.0)
+    ghc-options:     -Wcompat
+  if !impl(ghc >= 8.0)
+    build-depends: semigroups == 0.18.*
 
 Test-Suite test-unbound-generics
   type:                exitcode-stdio-1.0
@@ -88,6 +94,8 @@
   hs-source-dirs:      test
   default-language:    Haskell2010
   ghc-options:         -Wall
+  if impl (ghc >= 8.0.0)
+    ghc-options:     -Wcompat
 
 Benchmark benchmark-unbound-generics
   type:                exitcode-stdio-1.0
@@ -95,12 +103,19 @@
   hs-source-dirs:      benchmarks
   main-is:             benchmark-main.hs
   build-depends:       base
-                     , criterion
+                     , criterion >= 1.0.0.1
                      , deepseq >= 1.3.0.0
-                     , deepseq-generics >= 0.1.1.2
                      , unbound-generics
+  if impl (ghc == 7.6.*)
+    build-depends:     unix <= 2.6.0.1
+  if impl (ghc == 7.6.*) || impl (ghc == 7.8.*)
+    build-depends:     deepseq-generics
+  else
+    build-depends:     deepseq >= 1.4.0.0
   other-modules:       BenchLam
   ghc-options:       -Wall
+  if impl (ghc >= 8.0.0)
+    ghc-options:     -Wcompat
 
 source-repository head
   type:                git