diff --git a/.ghci b/.ghci
deleted file mode 100644
--- a/.ghci
+++ /dev/null
@@ -1,1 +0,0 @@
-:set -isrc -idist/build/autogen -optP-include -optPdist/build/autogen/cabal_macros.h
diff --git a/.gitignore b/.gitignore
--- a/.gitignore
+++ b/.gitignore
@@ -1,4 +1,5 @@
 dist
+dist-newstyle
 docs
 wiki
 TAGS
@@ -11,3 +12,21 @@
 *.hi
 *~
 *#
+.stack-work/
+cabal-dev
+*.chi
+*.chs.h
+*.dyn_o
+*.dyn_hi
+.hpc
+.hsenv
+.cabal-sandbox/
+cabal.sandbox.config
+*.prof
+*.aux
+*.hp
+*.eventlog
+cabal.project.local
+cabal.project.local~
+.HTF/
+.ghc.environment.*
diff --git a/.travis.yml b/.travis.yml
deleted file mode 100644
--- a/.travis.yml
+++ /dev/null
@@ -1,50 +0,0 @@
-language: c
-sudo: false
-
-matrix:
-  include:
-    - env: CABALVER=1.16 GHCVER=7.4.2
-      addons: {apt: {packages: [cabal-install-1.16,ghc-7.4.2], sources: [hvr-ghc]}}
-    - env: CABALVER=1.16 GHCVER=7.6.3
-      addons: {apt: {packages: [cabal-install-1.16,ghc-7.6.3], sources: [hvr-ghc]}}
-    - env: CABALVER=1.18 GHCVER=7.8.4
-      addons: {apt: {packages: [cabal-install-1.18,ghc-7.8.4], sources: [hvr-ghc]}}
-    - env: CABALVER=1.22 GHCVER=7.10.1
-      addons: {apt: {packages: [cabal-install-1.22,ghc-7.10.1],sources: [hvr-ghc]}}
-    - env: CABALVER=head GHCVER=head
-      addons: {apt: {packages: [cabal-install-head,ghc-head],  sources: [hvr-ghc]}}
-
-  allow_failures:
-   - env: CABALVER=head GHCVER=head
-
-before_install:
- - export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$PATH
- - export CABAL=cabal-$CABALVER
- - $CABAL --version
-
-install:
- - travis_retry $CABAL update
- - $CABAL install "Cabal == $CABALVER.*"
- - $CABAL install --enable-tests --only-dependencies
-
-script:
- - $CABAL configure -v2 --enable-tests
- - $CABAL build
- - $CABAL test
- - $CABAL sdist
- - export SRC_TGZ=$($CABAL info . | awk '{print $2 ".tar.gz";exit}') ;
-   cd dist/;
-   if [ -f "$SRC_TGZ" ]; then
-      $CABAL install "$SRC_TGZ";
-   else
-      echo "expected '$SRC_TGZ' not found";
-      exit 1;
-   fi
-
-notifications:
-  irc:
-    channels:
-      - "irc.freenode.org#haskell-lens"
-    skip_join: true
-    template:
-      - "\x0313bound\x0f/\x0306%{branch}\x0f \x0314%{commit}\x0f %{message} \x0302\x1f%{build_url}\x0f"
diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown
--- a/CHANGELOG.markdown
+++ b/CHANGELOG.markdown
@@ -1,3 +1,50 @@
+2.0.7 [2023.08.06]
+------------------
+* Support building with `template-haskell-2.21.*` (GHC 9.8).
+
+2.0.6 [2023.01.18]
+------------------
+* Allow the examples to build with `base-4.18.*` (GHC 9.6).
+
+2.0.5 [2022.05.07]
+------------------
+* Allow building with `transformers-0.6.*`.
+
+2.0.4 [2021.11.07]
+------------------
+* Allow building with `template-haskell-2.18` (GHC 9.2).
+* The `Bound.TH` module no longer requires the `TemplateHaskell` extension
+  (only `TemplateHaskellQuotes`) when building with GHC 9.0 or later.
+* Drop support for pre-8.0 versions of GHC.
+
+2.0.3 [2021.02.05]
+------------------
+* Allow the examples to build with `vector-0.12.2` or later.
+* The build-type has been changed from `Custom` to `Simple`.
+  To achieve this, the `doctests` test suite has been removed in favor of using [`cabal-docspec`](https://github.com/phadej/cabal-extras/tree/master/cabal-docspec) to run the doctests.
+
+2.0.2 [2020.10.01]
+------------------
+* Allow building with GHC 9.0.
+
+2.0.1
+-----
+* Add `abstractEither` and `instantiateEither` to `Bound.Scope`, and
+  add `abstractEitherName` and `instantiateEitherName` to `Bound.Scope.Name`
+* Add `Generic(1)` instances for `Name` and `Scope`
+* Support `doctest-0.12`
+
+2
+-
+* GHC 8.0 and 8.2 support
+* Converted from `prelude-extras` to `transformers` + `transformers-compat` for the `Eq1`, `Ord1`, `Show1`, and `Read1` functionality.
+* `makeBound` supports `Functor` components
+* Add `MFunctor` instance for `Scope`
+* Add `NFData` instances for `Name`, `Scope`, and `Var`
+* Revamp `Setup.hs` to use `cabal-doctest`. This makes it build
+  with `Cabal-1.25`, and makes the `doctest`s work with `cabal new-build` and
+  sandboxes.
+
 1.0.7
 ------
 * Added an `-f-template-haskell` option to allow disabling `template-haskell` support. This is an unsupported configuration but may be useful for expert users in sandbox configurations.
diff --git a/README.markdown b/README.markdown
--- a/README.markdown
+++ b/README.markdown
@@ -1,7 +1,7 @@
 Bound
 =====
 
-[![Hackage](https://img.shields.io/hackage/v/bound.svg)](https://hackage.haskell.org/package/bound) [![Build Status](https://secure.travis-ci.org/ekmett/bound.png?branch=master)](http://travis-ci.org/ekmett/bound)
+[![Hackage](https://img.shields.io/hackage/v/bound.svg)](https://hackage.haskell.org/package/bound) [![Build Status](https://github.com/ekmett/bound/workflows/Haskell-CI/badge.svg)](https://github.com/ekmett/bound/actions?query=workflow%3AHaskell-CI)
 
 Goals
 -----
@@ -16,21 +16,21 @@
 {-# LANGUAGE DeriveFunctor #-}
 {-# LANGUAGE DeriveFoldable #-}
 {-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE TemplateHaskell #-}
+
 import Bound
-import Prelude.Extras
 import Control.Applicative
 import Control.Monad
+import Data.Functor.Classes
 import Data.Foldable
 import Data.Traversable
+import Data.Eq.Deriving (deriveEq1)      -- these two are from the
+import Text.Show.Deriving (deriveShow1)  -- deriving-compat package
 
 infixl 9 :@
 data Exp a = V a | Exp a :@ Exp a | Lam (Scope () Exp a)
-  deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable)
+  deriving (Eq,Show,Functor,Foldable,Traversable)
 
-instance Eq1 Exp
-instance Ord1 Exp
-instance Show1 Exp
-instance Read1 Exp
 instance Applicative Exp where pure = V; (<*>) = ap
 
 instance Monad Exp where
@@ -47,6 +47,15 @@
   Lam b -> whnf (instantiate1 a b)
   f'    -> f' :@ a
 whnf e = e
+
+deriveEq1 ''Exp
+deriveShow1 ''Exp
+
+main :: IO ()
+main = do
+  let term = lam 'x' (V 'x') :@ V 'y'
+  print term         -- Lam (Scope (V (B ()))) :@ V 'y'
+  print $ whnf term  -- V 'y'
 ```
 
    There are longer examples in the [examples/ folder](https://github.com/ekmett/bound/tree/master/examples).
diff --git a/Setup.lhs b/Setup.lhs
--- a/Setup.lhs
+++ b/Setup.lhs
@@ -1,44 +1,7 @@
 #!/usr/bin/runhaskell
-\begin{code}
-{-# OPTIONS_GHC -Wall #-}
-module Main (main) where
-
-import Data.List ( nub )
-import Data.Version ( showVersion )
-import Distribution.Package ( PackageName(PackageName), PackageId, InstalledPackageId, packageVersion, packageName )
-import Distribution.PackageDescription ( PackageDescription(), TestSuite(..) )
-import Distribution.Simple ( defaultMainWithHooks, UserHooks(..), simpleUserHooks )
-import Distribution.Simple.Utils ( rewriteFile, createDirectoryIfMissingVerbose )
-import Distribution.Simple.BuildPaths ( autogenModulesDir )
-import Distribution.Simple.Setup ( BuildFlags(buildVerbosity), fromFlag )
-import Distribution.Simple.LocalBuildInfo ( withLibLBI, withTestLBI, LocalBuildInfo(), ComponentLocalBuildInfo(componentPackageDeps) )
-import Distribution.Verbosity ( Verbosity )
-import System.FilePath ( (</>) )
-
-main :: IO ()
-main = defaultMainWithHooks simpleUserHooks
-  { buildHook = \pkg lbi hooks flags -> do
-     generateBuildModule (fromFlag (buildVerbosity flags)) pkg lbi
-     buildHook simpleUserHooks pkg lbi hooks flags
-  }
-
-generateBuildModule :: Verbosity -> PackageDescription -> LocalBuildInfo -> IO ()
-generateBuildModule verbosity pkg lbi = do
-  let dir = autogenModulesDir lbi
-  createDirectoryIfMissingVerbose verbosity True dir
-  withLibLBI pkg lbi $ \_ libcfg -> do
-    withTestLBI pkg lbi $ \suite suitecfg -> do
-      rewriteFile (dir </> "Build_" ++ testName suite ++ ".hs") $ unlines
-        [ "module Build_" ++ testName suite ++ " where"
-        , "deps :: [String]"
-        , "deps = " ++ (show $ formatdeps (testDeps libcfg suitecfg))
-        ]
-  where
-    formatdeps = map (formatone . snd)
-    formatone p = case packageName p of
-      PackageName n -> n ++ "-" ++ showVersion (packageVersion p)
+> module Main (main) where
 
-testDeps :: ComponentLocalBuildInfo -> ComponentLocalBuildInfo -> [(InstalledPackageId, PackageId)]
-testDeps xs ys = nub $ componentPackageDeps xs ++ componentPackageDeps ys
+> import Distribution.Simple
 
-\end{code}
+> main :: IO ()
+> main = defaultMain
diff --git a/bound.cabal b/bound.cabal
--- a/bound.cabal
+++ b/bound.cabal
@@ -1,8 +1,8 @@
 name:          bound
 category:      Language, Compilers/Interpreters
-version:       1.0.7
+version:       2.0.7
 license:       BSD3
-cabal-version: >= 1.9.2
+cabal-version: >= 1.10
 license-file:  LICENSE
 author:        Edward A. Kmett
 maintainer:    Edward A. Kmett <ekmett@gmail.com>
@@ -11,7 +11,7 @@
 bug-reports:   http://github.com/ekmett/bound/issues
 copyright:     Copyright (C) 2012-2013 Edward A. Kmett
 synopsis:      Making de Bruijn Succ Less
-build-type:    Custom
+build-type:    Simple
 description:
    We represent the target language itself as an ideal monad supplied by the
    user, and provide a 'Scope' monad transformer for introducing bound variables
@@ -19,7 +19,7 @@
    and we traverse to find free variables, and use the Monad to perform
    substitution that avoids bound variables.
    .
-   Slides describing and motivating this approach to name binding are available 
+   Slides describing and motivating this approach to name binding are available
    online at:
    .
    <http://www.slideshare.net/ekmett/bound-making-de-bruijn-succ-less>
@@ -30,24 +30,31 @@
    With generalized de Bruijn term you can 'lift' whole trees instead of just
    applying 'succ' to individual variables, weakening the all variables bound
    by a scope and greatly speeding up instantiation. By giving binders more
-   structure we permit easy simultaneous substitution and further speed up 
+   structure we permit easy simultaneous substitution and further speed up
    instantiation.
 
 extra-source-files:
-  .travis.yml
-  .ghci
   .gitignore
   .vim.custom
-  examples/Simple.hs
-  examples/Deriving.hs
-  examples/Overkill.hs
-  tests/doctests.hs
-  travis/cabal-apt-install
-  travis/config
+  doc/*.hs
+  doc/bound-laws.cabal
+  doc/LICENSE
   README.markdown
   CHANGELOG.markdown
   AUTHORS.markdown
 
+tested-with:
+  GHC==8.0.2,
+  GHC==8.2.2,
+  GHC==8.4.4,
+  GHC==8.6.5,
+  GHC==8.8.4,
+  GHC==8.10.7,
+  GHC==9.0.2,
+  GHC==9.2.8,
+  GHC==9.4.5,
+  GHC==9.6.2
+
 flag template-haskell
   description:
     You can disable the use of the `template-haskell` package using `-f-template-haskell`.
@@ -74,46 +81,78 @@
     Bound.Var
 
   build-depends:
-    base             >= 4       && < 5,
-    bifunctors       >= 3       && < 6,
-    binary           >= 0.5     && < 0.8,
-    bytes            >= 0.4     && < 1,
-    cereal           >= 0.3.5.2 && < 0.6,
-    comonad          >= 3       && < 5,
-    hashable         >= 1.1     && < 1.3,
-    hashable-extras  >= 0.1     && < 1,
-    prelude-extras   >= 0.3     && < 1,
+    base             >= 4.9     && < 5,
+    bifunctors       >= 5       && < 6,
+    binary           >= 0.8.3   && < 0.9,
+    bytes            >= 0.15.2  && < 1,
+    cereal           >= 0.4.1   && < 0.6,
+    comonad          >= 5       && < 6,
+    hashable         >= 1.2.5.0 && < 1.5,
+    mmorph           >= 1.0     && < 1.3,
+    deepseq          >= 1.4.2   && < 1.6,
     profunctors      >= 3.3     && < 6,
-    template-haskell >= 2.7     && < 3,
-    transformers     >= 0.2     && < 0.5
+    th-abstraction   >= 0.4     && < 0.7,
+    transformers     >= 0.5     && < 0.7,
+    transformers-compat >= 0.5  && < 1
 
   ghc-options: -Wall -O2 -fspec-constr -fdicts-cheap -funbox-strict-fields
 
-  if impl(ghc >=7.4 && < 7.6)
-    build-depends: ghc-prim
+  default-language: Haskell2010
 
   if flag(template-haskell) && impl(ghc)
-    build-depends: template-haskell >= 2.7 && < 3.0
+    build-depends: template-haskell >= 2.11.1 && < 3.0
 
 test-suite Simple
   type: exitcode-stdio-1.0
   main-is: Simple.hs
   hs-source-dirs: examples
+  buildable: True
+
   ghc-options: -Wall -threaded
+  default-language: Haskell2010
   build-depends:
-    base,
+    base            >= 4.5   && < 5,
     bound,
-    prelude-extras,
-    transformers
+    deriving-compat >= 0.3.4 && < 0.7,
+    transformers,
+    transformers-compat
 
-test-suite doctests
-  type:    exitcode-stdio-1.0
-  main-is: doctests.hs
-  hs-source-dirs: tests
+test-suite Overkill
+  type: exitcode-stdio-1.0
+  main-is: Overkill.hs
+  hs-source-dirs: examples
   ghc-options: -Wall -threaded
+  default-language: Haskell2010
   build-depends:
-    base,
-    directory >= 1.0 && < 1.3,
-    doctest   >= 0.9 && < 0.10,
-    filepath,
-    vector    >= 0.9 && < 0.11
+    base >= 4.5 && < 5,
+    bound,
+    transformers,
+    transformers-compat,
+    vector >= 0.12
+  if !impl(ghc >= 7.8)
+    buildable: False
+
+test-suite Deriving
+  type: exitcode-stdio-1.0
+  main-is: Deriving.hs
+  hs-source-dirs: examples
+  ghc-options: -Wall -threaded
+  default-language: Haskell2010
+  build-depends:
+    base >= 4.5 && < 5,
+    bound,
+    transformers,
+    transformers-compat
+
+test-suite Imperative
+  type: exitcode-stdio-1.0
+  main-is: Imperative.hs
+  hs-source-dirs: examples
+  ghc-options: -Wall -threaded
+  default-language: Haskell2010
+  build-depends:
+    base >= 4.5 && < 5,
+    bound,
+    transformers,
+    transformers-compat,
+    void
diff --git a/doc/BoundLaws.hs b/doc/BoundLaws.hs
new file mode 100644
--- /dev/null
+++ b/doc/BoundLaws.hs
@@ -0,0 +1,102 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE KindSignatures #-}
+module BoundLaws where
+
+import Bound.Class
+import Control.Monad
+import Data.Kind
+
+{-
+
+What laws should Bound have?
+
+We need at least enough to make sure the typical Monad Exp instances are valid.
+
+Let's start by writing some generic Bound instances.
+
+-}
+
+newtype Const x (m :: Type -> Type) a = Const x
+
+instance Bound (Const x) where
+  Const x >>>= _ = Const x
+
+
+newtype Identity (m :: Type -> Type) a = Id (m a)
+
+instance Bound Identity where
+   Id ma >>>= f = Id (ma >>= f)
+
+
+data Product f g (m :: Type -> Type) a = f m a :*: g m a
+
+instance (Bound f, Bound g) => Bound (Product f g) where
+    (fma :*: gma) >>>= f = (fma >>>= f) :*: (gma >>>= f)
+
+
+data Sum f g (m :: Type -> Type) a = Inl (f m a) | Inr (g m a)
+
+instance (Bound f, Bound g) => Bound (Sum f g) where
+    Inl fma >>>= f = Inl (fma >>>= f)
+    Inr gma >>>= f = Inr (gma >>>= f)
+
+
+{-
+
+Now we can actually write the typical Monad Exp instance generically
+(for theory, not practice), since sums and products and all of the
+above is plenty enough to specify an AST.
+
+-}
+
+data Exp (f :: (Type -> Type) -> Type -> Type) a = Var a | Branch (f (Exp f) a)
+
+instance Bound f => Functor (Exp f) where
+  fmap = liftM
+
+instance Bound f => Applicative (Exp f) where
+  pure = Var
+  (<*>) = ap
+
+instance Bound f => Monad (Exp f) where
+#if !(MIN_VERSION_base(4,11,0))
+  return = Var
+#endif
+  Var a     >>= f = f a
+  Branch fE >>= f = Branch (fE >>>= f)
+
+{-
+
+Is this valid? Let's go to Agda and try to prove the Monad laws.
+
+
+  left-return : ∀ {A B} (x : A)(f : A -> Exp F B) -> (return x >>= f) ≡ f x
+  left-return x f = refl
+
+  right-return : ∀ {A}(m : Exp F A) -> (m >>= return) ≡ m
+  right-return (Var x)    = refl
+  right-return (Branch m) = cong Branch {!!}0
+
+  assoc : ∀ {A B C} (m : Exp F A) (k : A -> Exp F B) (h : B -> Exp F C) -> (m >>= (\ x -> k x >>= h)) ≡ ((m >>= k) >>= h)
+  assoc (Var x)    k h = refl
+  assoc (Branch m) k h = cong Branch {!!}1
+
+
+So the first one is fine, but we have two holes:
+
+  ?0 : m >>>= return ≡ m
+  ?1 : m >>>= (λ x → k x >>= h) ≡ (m >>>= k) >>>= h
+
+But all of the instances above respect these laws, and they are implied by
+the current law for monad transformers, we could just make them the
+Bound class laws.
+
+Btw these laws correspond to requiring (f m) to be an m-left module for every m [1],
+so we'd also get a law-abiding fmap for (f m).
+
+
+Bonus: composing pointwise (\m a -> f m (g m a)) would also create a valid Bound
+
+
+[1] Modules over Monads and Initial Semantics - http://web.math.unifi.it/users/maggesi/syn.pdf
+-}
diff --git a/doc/LICENSE b/doc/LICENSE
new file mode 100644
--- /dev/null
+++ b/doc/LICENSE
@@ -0,0 +1,30 @@
+Copyright 2012 Edward Kmett
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright
+   notice, this list of conditions and the following disclaimer in the
+   documentation and/or other materials provided with the distribution.
+
+3. Neither the name of the author nor the names of his contributors
+   may be used to endorse or promote products derived from this software
+   without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS OR
+IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED.  IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR
+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,
+STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
+ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+POSSIBILITY OF SUCH DAMAGE.
diff --git a/doc/bound-laws.cabal b/doc/bound-laws.cabal
new file mode 100644
--- /dev/null
+++ b/doc/bound-laws.cabal
@@ -0,0 +1,40 @@
+name:          bound-laws
+category:      Language, Compilers/Interpreters
+version:       0.1
+license:       BSD3
+cabal-version: >= 1.10
+license-file:  LICENSE
+author:        Edward A. Kmett
+maintainer:    Edward A. Kmett <ekmett@gmail.com>
+stability:     experimental
+homepage:      http://github.com/ekmett/bound/
+bug-reports:   http://github.com/ekmett/bound/issues
+copyright:     Copyright (C) 2012-2013 Edward A. Kmett
+synopsis:      Making de Bruijn Succ Less
+build-type:    Simple
+description:   Some laws for the @Bound@ class
+
+tested-with:
+  GHC==8.0.2,
+  GHC==8.2.2,
+  GHC==8.4.4,
+  GHC==8.6.5,
+  GHC==8.8.4,
+  GHC==8.10.7,
+  GHC==9.0.2,
+  GHC==9.2.8,
+  GHC==9.4.5,
+  GHC==9.6.2
+
+source-repository head
+  type: git
+  location: git://github.com/ekmett/bound.git
+
+library
+  exposed-modules: BoundLaws
+  hs-source-dirs: .
+  ghc-options: -Wall
+  default-language: Haskell2010
+  build-depends:
+    base >= 4.9 && < 5,
+    bound
diff --git a/examples/Deriving.hs b/examples/Deriving.hs
--- a/examples/Deriving.hs
+++ b/examples/Deriving.hs
@@ -1,12 +1,9 @@
-{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
-module Deriving where
+{-# LANGUAGE CPP, DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
+module Main where
 
-import Data.List
-import Data.Foldable
-import Data.Traversable
+import qualified Data.List as L
 import Control.Monad
-import Control.Applicative
-import Prelude.Extras
+import Data.Functor.Classes
 import Bound
 
 infixl 9 :@
@@ -17,24 +14,30 @@
   | Lam {-# UNPACK #-} !Int (Pat Exp a) (Scope Int Exp a)
   | Let {-# UNPACK #-} !Int [Scope Int Exp a] (Scope Int Exp a)
   | Case (Exp a) [Alt Exp a]
-  deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable)
+  deriving (Eq,Functor,Foldable,Traversable)
 
 instance Applicative Exp where
   pure = V
   (<*>) = ap
 
 instance Monad Exp where
+#if !(MIN_VERSION_base(4,11,0))
   return = V
+#endif
   V a        >>= f = f a
   (x :@ y)   >>= f = (x >>= f) :@ (y >>= f)
   Lam n p e  >>= f = Lam n (p >>>= f) (e >>>= f)
   Let n bs e >>= f = Let n (map (>>>= f) bs) (e >>>= f)
   Case e as  >>= f = Case (e >>= f) (map (>>>= f) as)
 
-instance Eq1   Exp
-instance Ord1  Exp
-instance Show1 Exp
-instance Read1 Exp
+instance Eq1   Exp where
+  liftEq eq (V a)        (V b)           = eq a b
+  liftEq eq (a :@ a')    (b :@ b')       = liftEq eq a b && liftEq eq a' b'
+  liftEq eq (Lam n p e)  (Lam n' p' e')  = n == n' && liftEq eq p p' && liftEq eq e e'
+  liftEq eq (Let n bs e) (Let n' bs' e') = n == n' && liftEq (liftEq eq) bs bs' && liftEq eq e e'
+  liftEq eq (Case e as)  (Case e' as')   = liftEq eq e e' && liftEq (liftEq eq) as as'
+  liftEq _  _            _               = False
+-- And "similarly" for Ord1, Show1 and Read1
 
 data Pat f a
   = VarP
@@ -44,6 +47,14 @@
   | ViewP (Scope Int f a) (Pat f a)
   deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable)
 
+instance (Eq1 f, Monad f) => Eq1 (Pat f) where
+  liftEq _  VarP        VarP          = True
+  liftEq _  WildP       WildP         = True
+  liftEq eq (AsP p)     (AsP p')      = liftEq eq p p'
+  liftEq eq (ConP g ps) (ConP g' ps') = g == g' && liftEq (liftEq eq) ps ps'
+  liftEq eq (ViewP e p) (ViewP e' p') = liftEq eq e e' && liftEq eq p p'
+  liftEq _ _ _ = False
+
 instance Bound Pat where
   VarP      >>>= _ = VarP
   WildP     >>>= _ = WildP
@@ -52,8 +63,12 @@
   ViewP e p >>>= f = ViewP (e >>>= f) (p >>>= f)
 
 data Alt f a = Alt {-# UNPACK #-} !Int (Pat f a) (Scope Int f a)
-  deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable)
+  deriving (Eq,Functor,Foldable,Traversable)
 
+instance (Eq1 f, Monad f) => Eq1 (Alt f) where
+  liftEq eq (Alt n p b) (Alt n' p' b') =
+    n == n' && liftEq eq p p' && liftEq eq b b'
+
 instance Bound Alt where
   Alt n p b >>>= f = Alt n (p >>>= f) (b >>>= f)
 
@@ -79,12 +94,12 @@
 conp :: String -> [P a] -> P a
 conp g ps = P (ConP g . go ps) (ps >>= bindings)
   where
-    go (P p as:ps) bs = p bs : go ps (bs ++ as)
+    go (P p as:ps') bs = p bs : go ps' (bs ++ as)
     go [] _ = []
 
 -- | view patterns can view variables that are bound earlier than them in the pattern
 viewp :: Eq a => Exp a -> P a -> P a
-viewp t (P p as) = P (\bs -> ViewP (abstract (`elemIndex` bs) t) (p bs)) as
+viewp t (P p as) = P (\bs -> ViewP (abstract (`L.elemIndex` bs) t) (p bs)) as
 
 -- | smart lam constructor
 --
@@ -97,20 +112,20 @@
 -- >>> lam (conp "F" [varp "x", viewp (V "y") $ varp "y"]) (V "y")
 -- Lam 2 (ConP "F" [VarP,ViewP (Scope (V (F (V "y")))) VarP]) (Scope (V (B 1)))
 lam :: Eq a => P a -> Exp a -> Exp a
-lam (P p as) t = Lam (length as) (p []) (abstract (`elemIndex` as) t)
+lam (P p as) t = Lam (length as) (p []) (abstract (`L.elemIndex` as) t)
 
 -- | smart let constructor
 let_ :: Eq a => [(a, Exp a)] -> Exp a -> Exp a
 let_ bs b = Let (length bs) (map (abstr . snd) bs) (abstr b)
   where vs  = map fst bs
-        abstr = abstract (`elemIndex` vs)
+        abstr = abstract (`L.elemIndex` vs)
 
 -- | smart alt constructor
 --
 -- >>> lam (varp "x") $ Case (V "x") [alt (conp "Hello" [varp "z",wildp]) (V "x"), alt (varp "y") (V "y")]
 -- Lam 1 VarP (Scope (Case (V (B 0)) [Alt 1 (ConP "Hello" [VarP,WildP]) (Scope (V (F (V (B 0))))),Alt 1 VarP (Scope (V (B 0)))]))
 alt :: Eq a => P a -> Exp a -> Alt Exp a
-alt (P p as) t = Alt (length as) (p []) (abstract (`elemIndex` as) t)
+alt (P p as) t = Alt (length as) (p []) (abstract (`L.elemIndex` as) t)
 
 main :: IO ()
 main = return ()
diff --git a/examples/Imperative.hs b/examples/Imperative.hs
new file mode 100644
--- /dev/null
+++ b/examples/Imperative.hs
@@ -0,0 +1,286 @@
+{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable, RankNTypes, ScopedTypeVariables #-}
+module Main where
+
+-- It's possible to use bound "sideways" in order to support terms which do not
+-- have a Monad instance. A typical situation in which this would happen is when
+-- modelling an imperative language: variables are bound by statements, but they
+-- are used in positions where it would make no sense to replace them by another
+-- statement.
+
+import Bound.Scope -- .Simple
+import Bound.Var
+import Control.Monad (ap)
+import Data.Functor.Identity
+import Data.IORef
+import Data.Void (Void, absurd)
+
+-- PART 1: We want to model a tiny assembly language.
+--
+--   %0 = add 1 2
+--   %1 = add %0 %0
+--   ret %1
+--
+-- Add binds a fresh variable, and its operands can either be literals or
+-- previously-bound variables. Ret must be the last instruction.
+--
+-- Operand is monadic, traversable, and satisfies all the other requirements in
+-- order to be used with bound. But this is not sufficient, since Operand is
+-- not the whole language: we also need to define Prog, the sequence of
+-- instructions.
+data Operand a
+  = Lit Int
+  | Var a
+  deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable)
+
+instance Applicative Operand where
+  pure = Var
+  (<*>) = ap
+
+instance Monad Operand where
+  return = pure
+  Lit i >>= _ = Lit i
+  Var x >>= f = f x
+
+-- The following definition correctly models the instructions and their free
+-- variables. But since the Var in Operand cannot be replaced with a Prog, this
+-- definition is not monadic, and so we cannot manipulate the (Scope () Prog a)
+-- using bound's functions. This defeats the point of using Scope at all!
+--
+--   data Prog a
+--     = Ret (Operand a)
+--     | Add (Operand a) (Operand a)
+--           (Scope () Prog a) -- one more bound variable, available
+--                             -- in the rest of the program
+--
+-- The sideways trick is to replace the Operand constructor with a (* -> *) type
+-- parameter. Instantiating this with the real Operand will allow Operand to
+-- access the same free variables as Prog. But if we instantiate this with
+-- (Scope () Operand) instead, then the operands will have access to one extra
+-- bound variable! This way, we can bind fresh variables which can only be used
+-- inside the operands, and not in Prog.
+data Prog operand a
+  = Ret (operand a)
+  | Add (operand a) (operand a)
+        (Prog (Scope () operand) a)
+  deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable)
+
+-- The fact that the variables are not available in Prog after they are bound
+-- might seem strange, and we'll fix this in part 2, but it is actually a good
+-- thing. We want to be able to replace those variables with operand values, and
+-- that would not be possible if variables were allowed to appear inside Prog
+-- but outside of an operand.
+pInstantiate1 :: forall operand b a. (Applicative operand, Monad operand)
+              => operand a
+              -> Prog (Scope b operand) a
+              -> Prog operand a
+pInstantiate1 = go instantiate1
+  where
+    -- A value of type (Prog (Scope b operand) a) contains operands of type
+    -- (Scope b operand a), on which we can call instantiate1:
+    --
+    --   instantiate1 :: operand a -> Scope b operand a -> operand a
+    --
+    -- In the function below, (Scope b operand) and operand become o and o',
+    -- and instantiate1 is called f:
+    --
+    --   f :: operand v -> o v -> o' v
+    go :: forall o o' u. (Monad o, Monad o')
+       => (forall v. operand v -> o v -> o' v)
+       -> operand u -> Prog o u -> Prog o' u
+    go f x (Ret o)        = Ret (f x o)
+    go f x (Add o1 o2 cc) = Add (f x o1) (f x o2)
+                          $ go f' x cc
+      where
+        -- The rest of the program has access to one extra variable:
+        --
+        --   cc :: Prog (Scope () (Scope b operand)) a
+        --
+        -- In there, the operands have type (Scope () (Scope b operand) a), and
+        -- this time we cannot call instantiate1 because it would instantiate ()
+        -- instead of instantiating b. Instead, we create a function f' which
+        -- preserves the outer (Scope ()):
+        --
+        --   f' :: operand a -> Scope () (Scope b operand) a -> Scope () operand a
+        --   f' :: operand a -> Scope () o                 a -> Scope () o'      a
+        --
+        -- In the recursive call to go, (Scope () (Scope b operand)) and
+        -- (Scope () operand) become o and o', and f' is called f.
+        f' :: operand v -> Scope () o v -> Scope () o' v
+        f' v = toScope . f (fmap F v) . fromScope
+
+pAbstract1 :: forall operand a. (Applicative operand, Monad operand, Eq a)
+           => a
+           -> Prog operand a
+           -> Prog (Scope () operand) a
+pAbstract1 = go abstract1
+  where
+    go :: forall o o' u. (Eq u, Monad o, Monad o')
+       => (forall v. Eq v => v -> o v -> o' v)
+       -> u -> Prog o u -> Prog o' u
+    go f x (Ret o)        = Ret (f x o)
+    go f x (Add o1 o2 cc) = Add (f x o1) (f x o2)
+                          $ go f' x cc
+      where
+        f' :: forall v. Eq v => v -> Scope () o v -> Scope () o' v
+        f' v = toScope . f (F v) . fromScope
+
+evalOperand :: Operand Void -> Int
+evalOperand (Lit i)    = i
+evalOperand (Var void) = absurd void
+
+-- |
+-- >>> :{
+-- let Just prog = closed
+--               $ Add (Lit 1) (Lit 2)       $ pAbstract1 "%0"
+--               $ Add (Var "%0") (Var "%0") $ pAbstract1 "%1"
+--               $ Ret (Var "%1")
+-- :}
+--
+-- >>> evalProg prog
+-- 6
+evalProg :: Prog Operand Void -> Int
+evalProg (Ret o)        = evalOperand o
+evalProg (Add o1 o2 cc) = evalProg cc'
+  where
+    result :: Int
+    result = evalOperand o1 + evalOperand o2
+
+    cc' :: Prog Operand Void
+    cc' = pInstantiate1 (Lit result) cc
+
+
+-- PART 2: Here's a slightly more complicated language.
+--
+--   %0 = add 1 2
+--   %1 = add %0 %0
+--   swp %0 %1
+--   ret %1
+--
+-- The new swp command swaps the contents of two variables, so the two arguments
+-- must be previously-bound variables, they cannot be literals. This time the
+-- naïve definition looks like this:
+--
+--   data Prog' a
+--     = Ret' (Operand a)
+--     | Swp' a a
+--            (Prog' a)
+--     | Add' (Operand a) (Operand a)
+--            (Scope () Prog' a)
+--
+-- If we apply the sideways trick to this definition, the newly-bound variables
+-- will only be available in the operands, and so it won't be possible to call
+-- swp on them. The first step towards a solution is to add seemingly-useless
+-- Identity wrappers:
+--
+--   data Prog' a
+--     = Ret' (Operand a)
+--     | Swp' (Identity a) (Identity a)
+--            (Prog' a)
+--     | Add' (Operand a) (Operand a)
+--            (Scope () Prog' a)
+--
+-- We can now apply the sideways trick twice: once for Operand, and once for
+-- Identity. This gives us a lot of control: we can bind fresh variables which
+-- can only be used inside the operands, we can bind fresh variables which can
+-- be used inside Prog but not inside the operands, and as required for this
+-- example, we can bind fresh variables which can be used in both.
+data Prog' operand identity a
+  = Ret' (operand a)
+  | Swp' (identity a) (identity a)
+         (Prog' operand identity a)
+  | Add' (operand a) (operand a)
+         (Prog' (Scope () operand) (Scope () identity) a)
+  deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable)
+
+-- Bound variables can now occur in both operand and identity, so we can no
+-- longer instantiate them with operands. Instead, we'll have to instantiate
+-- them with a value which both (Operand a) and (Identity a) can contain:
+-- a free variable.
+pInstantiate1' :: ( Applicative operand, Monad operand
+                  , Applicative identity, Monad identity
+                  )
+               => a
+               -> Prog' (Scope () operand) (Scope () identity) a
+               -> Prog' operand identity a
+pInstantiate1' = go (instantiate1 . pure) (instantiate1 . pure)
+  where
+    go :: forall o o' i i' u. (Monad i, Monad i', Monad o, Monad o')
+       => (forall v. v -> o v -> o' v)
+       -> (forall v. v -> i v -> i' v)
+       -> u -> Prog' o i u -> Prog' o' i' u
+    go fo fi x = go'
+      where
+        go' (Ret' o)        = Ret' (fo x o)
+        go' (Swp' i1 i2 cc) = Swp' (fi x i1)
+                                   (fi x i2)
+                                   (go' cc)
+        go' (Add' o1 o2 cc) = Add' (fo x o1)
+                                   (fo x o2)
+                                   (go fo' fi' x cc)
+
+        fo' :: v -> Scope () o v -> Scope () o' v
+        fo' v = toScope . fo (F v) . fromScope
+
+        fi' :: v -> Scope () i v -> Scope () i' v
+        fi' v = toScope . fi (F v) . fromScope
+
+pAbstract1' :: ( Applicative operand, Monad operand
+               , Applicative identity, Monad identity
+               , Eq a
+               )
+            => a
+            -> Prog' operand identity a
+            -> Prog' (Scope () operand) (Scope () identity) a
+pAbstract1' = go abstract1 abstract1
+  where
+    go :: forall o o' i i' u. (Eq u, Monad i, Monad i', Monad o, Monad o')
+       => (forall v. Eq v => v -> o v -> o' v)
+       -> (forall v. Eq v => v -> i v -> i' v)
+       -> u -> Prog' o i u -> Prog' o' i' u
+    go fo fi x = go'
+      where
+        go' (Ret' o)        = Ret' (fo x o)
+        go' (Swp' i1 i2 cc) = Swp' (fi x i1)
+                                   (fi x i2)
+                                   (go' cc)
+        go' (Add' o1 o2 cc) = Add' (fo x o1)
+                                   (fo x o2)
+                                   (go fo' fi' x cc)
+
+        fo' :: Eq v => v -> Scope () o v -> Scope () o' v
+        fo' v = toScope . fo (F v) . fromScope
+
+        fi' :: Eq v => v -> Scope () i v -> Scope () i' v
+        fi' v = toScope . fi (F v) . fromScope
+
+evalOperand' :: Operand (IORef Int) -> IO Int
+evalOperand' (Lit i)   = return i
+evalOperand' (Var ref) = readIORef ref
+
+-- |
+-- >>> :{
+-- let Just prog' = closed
+--                $ Add' (Lit 1) (Lit 2)       $ pAbstract1' "%0"
+--                $ Add' (Var "%0") (Var "%0") $ pAbstract1' "%1"
+--                $ Swp' (Identity "%0") (Identity "%1")
+--                $ Ret' (Var "%1")
+-- :}
+--
+-- >>> evalProg' prog'
+-- 3
+evalProg' :: Prog' Operand Identity (IORef Int) -> IO Int
+evalProg' (Ret' o)        = evalOperand' o
+evalProg' (Swp' (Identity ref1) (Identity ref2) cc) = do
+    x <- readIORef ref1
+    y <- readIORef ref2
+    writeIORef ref1 y
+    writeIORef ref2 x
+    evalProg' cc
+evalProg' (Add' o1 o2 cc) = do
+    result <- (+) <$> evalOperand' o1 <*> evalOperand' o2
+    ref <- newIORef result
+    evalProg' (pInstantiate1' ref cc)
+
+
+main :: IO ()
+main = return ()
diff --git a/examples/Overkill.hs b/examples/Overkill.hs
--- a/examples/Overkill.hs
+++ b/examples/Overkill.hs
@@ -1,32 +1,30 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE TypeOperators #-}
 
-{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+{-# OPTIONS_GHC -Wincomplete-patterns -Wno-orphans #-}
 
-module Overkill where
+module Main where
 
-import Data.Vector as Vector hiding ((++), map)
-import Data.List as List
+import Data.Kind
+import qualified Data.Vector as Vector
+import Data.Vector (Vector)
+import qualified Data.List as List
 import Data.Foldable
 import Data.Traversable
-import Data.Monoid (Monoid(..))
 import Control.Monad
 import Control.Applicative
 import Prelude hiding (foldr)
-import Prelude.Extras
+import Data.Functor.Classes
 import Data.Type.Equality
 import Bound
 
 infixl 9 :@
 infixr 5 :>
 
--- little orphan instances
-instance Show1 Vector where showsPrec1 = showsPrec
-instance Eq1 Vector where (==#) = (==)
-
 data Exp a
   = Var a
   | Exp a :@ Exp a
@@ -35,24 +33,24 @@
 
 data Index = VarI | WildI | AsI Index | ConI [Index]
 
-data Pat :: Index -> (* -> *) -> * -> * where
+data Pat :: Index -> (Type -> Type) -> Type -> Type where
   VarP  ::                             Pat 'VarI f a
   WildP ::                             Pat 'WildI f a
   AsP   :: Pat i f a                -> Pat ('AsI i) f a
   ConP  :: String    -> Pats bs f a -> Pat ('ConI bs) f a
   ViewP :: f a       -> Pat b f a   -> Pat b f a -- TODO: allow references to earlier variables
 
-data Pats :: [Index] -> (* -> *) -> * -> * where
+data Pats :: [Index] -> (Type -> Type) -> Type -> Type where
   NilP  :: Pats '[] f a
   (:>) :: Pat b f a -> Pats bs f a -> Pats (b ': bs) f a
 
-data Path :: Index -> * where
+data Path :: Index -> Type where
   V :: Path 'VarI
   L :: Path ('AsI a)
   R :: Path a -> Path ('AsI a)
   C :: MPath as -> Path ('ConI as)
 
-data MPath :: [Index] -> * where
+data MPath :: [Index] -> Type where
   H :: Path a   -> MPath (a ':as)
   T :: MPath as -> MPath (a ':as)
 
@@ -73,30 +71,32 @@
   traverse f (Let bs e) = Let <$> traverse (traverse f) bs <*> traverse f e
 
 instance Monad Exp where
+#if !(MIN_VERSION_base(4,11,0))
   return         = Var
+#endif
   Var a    >>= f = f a
   (x :@ y) >>= f = (x >>= f) :@ (y >>= f)
   Lam p e  >>= f = Lam (p >>>= f) (e >>>= f)
   Let bs e >>= f = Let (fmap (>>>= f) bs) (e >>>= f)
 
-instance Eq a => Eq (Exp a) where (==) = (==#)
+instance Eq a => Eq (Exp a) where (==) = eq1
 instance Eq1 Exp where
-  Var a     ==# Var b     = a == b
-  (a :@ b)  ==# (c :@ d)  = a ==# c && b ==# d
-  Lam ps a  ==# Lam qs b  =
-    case eqPat' ps qs of
+  liftEq eq (Var a)    (Var b)     = eq a b
+  liftEq eq (a :@ a')  (b :@ b')   = liftEq eq a b && liftEq eq a' b'
+  liftEq eq (Lam ps a) (Lam qs b)  =
+    case eqPat' eq ps qs of
       Nothing -> False
-      Just Refl -> a ==# b
+      Just Refl -> liftEq eq a b
 
-  Let as a  ==# Let bs b  = as == bs && a ==# b
-  _         ==# _         = False
+  liftEq eq (Let as a) (Let bs b)  = liftEq (liftEq eq) as bs && liftEq eq a b
+  liftEq _  _          _           = False
 
 instance Show a => Show (Exp a) where showsPrec = showsPrec1
 instance Show1 Exp where
-  showsPrec1 d (Var a)    = showParen (d > 10) $ showString "Var " . showsPrec 11 a
-  showsPrec1 d (a :@ b)   = showParen (d > 9) $ showsPrec1 9 a . showString " :@ " . showsPrec1 10 b
-  showsPrec1 d (Lam ps b) = showParen (d > 10) $ showString "Lam " . showsPrec1 11 ps . showChar ' ' . showsPrec1 11 b
-  showsPrec1 d (Let bs b) = showParen (d > 10) $ showString "Let " . showsPrec1 11 bs . showChar ' ' . showsPrec1 11 b
+  liftShowsPrec s _ d (Var a)     = showParen (d > 10) $ showString "Var " . s 11 a
+  liftShowsPrec s sl d (a :@ b)   = showParen (d > 9)  $ liftShowsPrec s sl 9 a . showString " :@ " . liftShowsPrec s sl 10 b
+  liftShowsPrec s sl d (Lam ps b) = showParen (d > 10) $ showString "Lam " . liftShowsPrec s sl 11 ps . showChar ' ' . liftShowsPrec s sl 11 b
+  liftShowsPrec s sl d (Let bs b) = showParen (d > 10) $ showString "Let " . liftShowsPrec (liftShowsPrec s sl) (liftShowList s sl) 11 bs . showChar ' ' . liftShowsPrec s sl 11 b
 
 -- * smart lam
 
@@ -142,40 +142,41 @@
 
 -- ** A Kind of Shape
 
-eqPat :: (Eq1 f, Eq a) => Pat b f a -> Pat b' f a -> Bool
-eqPat VarP        VarP        = True
-eqPat WildP       WildP       = True
-eqPat (AsP p)     (AsP q)     = eqPat p q
-eqPat (ConP g ps) (ConP h qs) = g == h  && eqPats ps qs
-eqPat (ViewP e p) (ViewP f q) = e ==# f && eqPat p q
-eqPat _ _ = False
+eqPat :: (Eq1 f) => (a -> b -> Bool) -> Pat i f a -> Pat i' f b -> Bool
+eqPat _  VarP        VarP        = True
+eqPat _  WildP       WildP       = True
+eqPat eq (AsP p)     (AsP q)     = eqPat eq p q
+eqPat eq (ConP g ps) (ConP h qs) = g == h  && eqPats eq ps qs
+eqPat eq (ViewP e p) (ViewP f q) = liftEq eq e f && eqPat eq p q
+eqPat _ _ _ = False
 
 -- The same as eqPat, but if the patterns are equal, it returns a
 -- proof that their type arguments are the same.
-eqPat' :: (Eq1 f, Eq a) => Pat b f a -> Pat b' f a -> Maybe (b :~: b')
-eqPat' VarP VarP = Just Refl
-eqPat' WildP WildP = Just Refl
-eqPat' (AsP p) (AsP q) = do
-  Refl <- eqPat' p q
+eqPat' :: (Eq1 f) => (a -> a' -> Bool) -> Pat b f a -> Pat b' f a' -> Maybe (b :~: b')
+eqPat' _  VarP VarP = Just Refl
+eqPat' _  WildP WildP = Just Refl
+eqPat' eq (AsP p) (AsP q) = do
+  Refl <- eqPat' eq p q
   Just Refl
-eqPat' (ConP g ps) (ConP h qs) = do
+eqPat' eq (ConP g ps) (ConP h qs) = do
   guard (g == h)
-  Refl <- eqPats' ps qs
+  Refl <- eqPats' eq ps qs
   Just Refl
-eqPat' (ViewP e p) (ViewP f q) = guard (e ==# f) >> eqPat' p q
-eqPat' _ _ = Nothing
+eqPat' eq (ViewP e p) (ViewP f q) = guard (liftEq eq e f) >> eqPat' eq p q
+eqPat' _ _ _ = Nothing
 
-instance Eq1 f   => Eq1 (Pat b f)        where (==#) = eqPat
-instance (Eq1 f, Eq a) => Eq (Pat b f a) where (==) = eqPat
+instance Eq1 f   => Eq1 (Pat b f)        where liftEq = eqPat
+instance (Eq1 f, Eq a) => Eq (Pat b f a) where (==) = eq1
 
-instance Show1 f => Show1 (Pat b f) where showsPrec1 = showsPrec
-instance (Show1 f, Show a) => Show (Pat b f a) where
-  showsPrec _ VarP        = showString "VarP"
-  showsPrec _ WildP       = showString "WildP"
-  showsPrec d (AsP p)     = showParen (d > 10) $ showString "AsP " . showsPrec 11 p
-  showsPrec d (ConP g ps) = showParen (d > 10) $ showString "ConP " . showsPrec 11 g . showChar ' ' . showsPrec 11 ps
-  showsPrec d (ViewP e p) = showParen (d > 10) $ showString "ViewP " . showsPrec1 11 e . showChar ' ' . showsPrec 11 p
+instance (Show1 f, Show a) => Show (Pat b f a) where showsPrec = showsPrec1
 
+instance Show1 f => Show1 (Pat b f) where
+  liftShowsPrec _ _  _ VarP        = showString "VarP"
+  liftShowsPrec _ _  _ WildP       = showString "WildP"
+  liftShowsPrec s sl d (AsP p)     = showParen (d > 10) $ showString "AsP " . liftShowsPrec s sl 11 p
+  liftShowsPrec s sl d (ConP g ps) = showParen (d > 10) $ showString "ConP " . showsPrec 11 g . showChar ' ' . liftShowsPrec s sl 11 ps
+  liftShowsPrec s sl d (ViewP e p) = showParen (d > 10) $ showString "ViewP " . liftShowsPrec s sl 11 e . showChar ' ' . liftShowsPrec s sl 11 p
+
 instance Functor f => Functor (Pat b f) where
   fmap _ VarP = VarP
   fmap _ WildP = WildP
@@ -204,29 +205,29 @@
   ViewP e p >>>= f = ViewP (e >>= f) (p >>>= f)
 
 -- ** Pats
-eqPats :: (Eq1 f, Eq a) => Pats bs f a -> Pats bs' f a -> Bool
-eqPats NilP      NilP      = True
-eqPats (p :> ps) (q :> qs) = eqPat p q && eqPats ps qs
-eqPats _         _         = False
+eqPats :: (Eq1 f) => (a -> b -> Bool) -> Pats bs f a -> Pats bs' f b -> Bool
+eqPats _  NilP      NilP      = True
+eqPats eq (p :> ps) (q :> qs) = eqPat eq p q && eqPats eq ps qs
+eqPats _  _         _         = False
 
 -- Like eqPats, but if the patses are equal, it returns a proof that their
 -- type arguments are the same.
-eqPats' :: (Eq1 f, Eq a) => Pats bs f a -> Pats bs' f a -> Maybe (bs :~: bs')
-eqPats' NilP NilP = Just Refl
-eqPats' (p :> ps) (q :> qs) = do
-  Refl <- eqPat' p q
-  Refl <- eqPats' ps qs
+eqPats' :: (Eq1 f) => (a -> a' -> Bool) -> Pats bs f a -> Pats bs' f a' -> Maybe (bs :~: bs')
+eqPats' _  NilP NilP = Just Refl
+eqPats' eq (p :> ps) (q :> qs) = do
+  Refl <- eqPat' eq p q
+  Refl <- eqPats' eq ps qs
   Just Refl
-eqPats' _ _ = Nothing
+eqPats' _ _ _ = Nothing
 
-instance Eq1 f         => Eq1 (Pats bs f)   where (==#) = eqPats
-instance (Eq1 f, Eq a) => Eq  (Pats bs f a) where (==)  = eqPats
+instance Eq1 f         => Eq1 (Pats bs f)   where liftEq = eqPats
+instance (Eq1 f, Eq a) => Eq  (Pats bs f a) where (==)  = eq1
 
 instance (Show1 f, Show a) => Show (Pats bs f a) where showsPrec = showsPrec1
 instance Show1 f => Show1 (Pats bs f) where
-  showsPrec1 _ NilP      = showString "NilP"
-  showsPrec1 d (p :> ps) = showParen (d > 5) $
-    showsPrec1 6 p . showString " :> " . showsPrec1 5 ps
+  liftShowsPrec _ _  _ NilP      = showString "NilP"
+  liftShowsPrec s sl d (p :> ps) = showParen (d > 5) $
+    liftShowsPrec s sl 6 p . showString " :> " . liftShowsPrec s sl 5 ps
 
 instance Functor f => Functor (Pats bs f) where
   fmap _ NilP = NilP
diff --git a/examples/Simple.hs b/examples/Simple.hs
--- a/examples/Simple.hs
+++ b/examples/Simple.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP, TemplateHaskell #-}
 module Main where
 
 -- this is a simple example where lambdas only bind a single variable at a time
@@ -8,13 +9,14 @@
 import Data.Maybe (fromJust)
 import Data.Traversable
 import Control.Monad
-import Control.Monad.Trans.Class
 import Control.Applicative
 import Prelude hiding (foldr,abs)
-import Prelude.Extras
+import Data.Deriving (deriveEq1, deriveOrd1, deriveRead1, deriveShow1)
+import Data.Functor.Classes
 import Bound
 import System.Exit
 
+
 infixl 9 :@
 
 data Exp a
@@ -22,7 +24,6 @@
   | Exp a :@ Exp a
   | Lam (Scope () Exp a)
   | Let [Scope Int Exp a] (Scope Int Exp a)
-  deriving (Eq,Ord,Show,Read)
 
 -- | A smart constructor for Lam
 --
@@ -52,17 +53,25 @@
   traverse f (Let bs b) = Let <$> traverse (traverse f) bs <*> traverse f b
 
 instance Monad Exp where
+#if !(MIN_VERSION_base(4,11,0))
   return = V
+#endif
   V a      >>= f = f a
   (x :@ y) >>= f = (x >>= f) :@ (y >>= f)
   Lam e    >>= f = Lam (e >>>= f)
   Let bs b >>= f = Let (map (>>>= f) bs) (b >>>= f)
 
--- these 4 classes are needed to help Eq, Ord, Show and Read pass through Scope
-instance Eq1 Exp      where (==#)      = (==)
-instance Ord1 Exp     where compare1   = compare
-instance Show1 Exp    where showsPrec1 = showsPrec
-instance Read1 Exp    where readsPrec1 = readsPrec
+fmap concat $ sequence
+  [ deriveEq1   ''Exp
+  , deriveOrd1  ''Exp
+  , deriveRead1 ''Exp
+  , deriveShow1 ''Exp
+  , [d| instance Eq a => Eq (Exp a) where (==) = eq1
+        instance Ord a => Ord (Exp a) where compare = compare1
+        instance Show a => Show (Exp a) where showsPrec = showsPrec1
+        instance Read a => Read (Exp a) where readsPrec = readsPrec1
+      |]
+  ]
 
 -- | Compute the normal form of an expression
 nf :: Exp a -> Exp a
@@ -139,28 +148,30 @@
 -- TODO: use a real pretty printer
 
 prettyPrec :: [String] -> Bool -> Int -> Exp String -> ShowS
-prettyPrec _      d n (V a)      = showString a
-prettyPrec vs     d n (x :@ y)   = showParen d $ 
+prettyPrec _      _ _ (V a)      = showString a
+prettyPrec vs     d n (x :@ y)   = showParen d $
   prettyPrec vs False n x . showChar ' ' . prettyPrec vs True n y
-prettyPrec (v:vs) d n (Lam b)    = showParen d $ 
+prettyPrec (v:vs) d n (Lam b)    = showParen d $
   showString v . showString ". " . prettyPrec vs False n (instantiate1 (V v) b)
-prettyPrec vs     d n (Let bs b) = showParen d $ 
+prettyPrec []     _ _ (Lam _)    = error "Ran out of variable names"
+prettyPrec vs     d n (Let bs b) = showParen d $
   showString "let" .  foldr (.) id (zipWith showBinding xs bs) .
   showString " in " . indent . prettyPrec ys False n (inst b)
   where (xs,ys) = splitAt (length bs) vs
-        inst = instantiate (\n -> V (xs !! n))
+        inst = instantiate (\n' -> V (xs !! n'))
         indent = showString ('\n' : replicate (n + 4) ' ')
-        showBinding x b = indent . showString x . showString " = " . prettyPrec ys False (n + 4) (inst b)
+        showBinding x b' = indent . showString x . showString " = " . prettyPrec ys False (n + 4) (inst b')
 
 prettyWith :: [String] -> Exp String -> String
 prettyWith vs t = prettyPrec (filter (`notElem` toList t) vs) False 0 t ""
 
 pretty :: Exp String -> String
-pretty = prettyWith $ [ [i] | i <- ['a'..'z']] ++ [i : show j | j <- [1..], i <- ['a'..'z'] ]
+pretty = prettyWith $ [ [i] | i <- ['a'..'z']] ++ [i : show j | j <- [1 :: Int ..], i <- ['a'..'z'] ]
 
 pp :: Exp String -> IO ()
 pp = putStrLn . pretty
 
+main :: IO ()
 main = do
   pp cooked
   let result = nf cooked
diff --git a/src/Bound.hs b/src/Bound.hs
--- a/src/Bound.hs
+++ b/src/Bound.hs
@@ -18,38 +18,48 @@
 -- An untyped lambda calculus:
 --
 -- @
--- {-\# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable \#-}
+-- {-\# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable, TemplateHaskell \#-}
 -- import Bound
 -- import Control.Applicative
 -- import Control.Monad ('Control.Monad.ap')
--- import Prelude.Extras
+-- import Data.Functor.Classes
 -- import Data.Foldable
 -- import Data.Traversable
+-- -- This is from deriving-compat package
+-- import Data.Deriving (deriveEq1, deriveOrd1, deriveRead1, deriveShow1)
 -- @
 --
 -- @
 -- infixl 9 :\@
 -- data Exp a = V a | Exp a :\@ Exp a | Lam ('Scope' () Exp a)
---   deriving ('Eq','Ord','Show','Read','Functor','Data.Foldable.Foldable','Data.Foldable.Traversable')
+--   deriving ('Functor','Data.Foldable.Foldable','Data.Foldable.Traversable')
 -- @
 --
 -- @
--- instance 'Prelude.Extras.Eq1' Exp
--- instance 'Prelude.Extras.Ord1' Exp
--- instance 'Prelude.Extras.Show1' Exp
--- instance 'Prelude.Extras.Read1' Exp
 -- instance 'Control.Applicative.Applicative' Exp where 'Control.Applicative.pure' = V; ('<*>') = 'Control.Monad.ap'
--- @
---
--- @
 -- instance 'Monad' Exp where
 --   'return' = V
 --   V a      '>>=' f = f a
---   (x :\@ y) '>>=' f = (x '>>=' f) :\@ (y >>= f)
+--   (x :\@ y) '>>=' f = (x '>>=' f) :\@ (y '>>=' f)
 --   Lam e    '>>=' f = Lam (e '>>>=' f)
 -- @
 --
 -- @
+-- concat <$> sequence
+--   [ deriveEq1   ''Exp
+--   , deriveOrd1  ''Exp
+--   , deriveRead1 ''Exp
+--   , deriveShow1 ''Exp
+--
+--   , [d| instance 'Eq' a   => 'Eq'   (Exp a) where (==) = eq1
+--         instance 'Ord' a  => 'Ord'  (Exp a) where compare = compare1
+--         instance 'Show' a => 'Show' (Exp a) where showsPrec = showsPrec1
+--         instance 'Read' a => 'Read' (Exp a) where readsPrec = readsPrec1
+--       |]
+--   ]
+-- @
+--
+-- @
 -- lam :: 'Eq' a => a -> 'Exp' a -> 'Exp' a
 -- lam v b = Lam ('abstract1' v b)
 -- @
@@ -80,7 +90,7 @@
 -- recursion pattern in their generalized de Bruijn representation. It is named
 -- 'Scope' to match up with the terminology and usage pattern from Conor McBride
 -- and James McKinna's \"I am not a number: I am a free variable\", available
--- from <http://www.cs.st-andrews.ac.uk/~james/RESEARCH/notanum.pdf>, but since
+-- from <http://www.cs.ru.nl/~james/RESEARCH/haskell2004.pdf>, but since
 -- the set of variables is visible in the type, we can provide stronger type
 -- safety guarantees.
 --
@@ -121,8 +131,10 @@
   , Var(..)
   , fromScope
   , toScope
-  -- * Deriving instances 
+#ifdef MIN_VERSION_template_haskell
+  -- * Deriving instances
   , makeBound
+#endif
   ) where
 
 import Bound.Var
diff --git a/src/Bound/Class.hs b/src/Bound/Class.hs
--- a/src/Bound/Class.hs
+++ b/src/Bound/Class.hs
@@ -1,8 +1,8 @@
 {-# LANGUAGE CPP #-}
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 704
+#if defined(__GLASGOW_HASKELL__)
 {-# LANGUAGE DefaultSignatures #-}
 #endif
-{-# OPTIONS -fno-warn-deprecations #-}
+{-# OPTIONS -Wno-deprecations #-}
 -----------------------------------------------------------------------------
 -- |
 -- Copyright   :  (C) 2012-2015 Edward Kmett
@@ -20,21 +20,18 @@
   , (=<<<)
   ) where
 
-#if __GLASGOW_HASKELL__ >= 704
 import Control.Monad.Trans.Class
-#endif
-#if __GLASGOW_HASKELL__ < 710
-import Data.Monoid
-#endif
 import Control.Monad.Trans.Cont
-import Control.Monad.Trans.Error
 import Control.Monad.Trans.Identity
-import Control.Monad.Trans.List
 import Control.Monad.Trans.Maybe
 import Control.Monad.Trans.RWS
 import Control.Monad.Trans.Reader
 import Control.Monad.Trans.State
 import Control.Monad.Trans.Writer
+#if !(MIN_VERSION_transformers(0,6,0))
+import Control.Monad.Trans.Error
+import Control.Monad.Trans.List
+#endif
 
 infixl 1 >>>=
 
@@ -56,6 +53,9 @@
 -- This is useful for types like expression lists, case alternatives,
 -- schemas, etc. that may not be expressions in their own right, but often
 -- contain expressions.
+--
+-- /Note:/ 'Control.Monad.Free.Free' isn't "really" a monad transformer, even if
+-- the kind matches. Therefore there isn't @'Bound' 'Control.Monad.Free.Free'@ instance.
 class Bound t where
   -- | Perform substitution
   --
@@ -64,7 +64,7 @@
   --
   -- @m '>>>=' f = m '>>=' 'lift' '.' f@
   (>>>=) :: Monad f => t f a -> (a -> f c) -> t f c
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 704
+#if defined(__GLASGOW_HASKELL__)
   default (>>>=) :: (MonadTrans t, Monad f, Monad (t f)) =>
                     t f a -> (a -> f c) -> t f c
   m >>>= f = m >>= lift . f
@@ -75,18 +75,10 @@
   m >>>= f = m >>= lift . f
   {-# INLINE (>>>=) #-}
 
-instance Error e => Bound (ErrorT e) where
- m >>>= f = m >>= lift . f
- {-# INLINE (>>>=) #-}
-
 instance Bound IdentityT where
  m >>>= f = m >>= lift . f
  {-# INLINE (>>>=) #-}
 
-instance Bound ListT where
- m >>>= f = m >>= lift . f
- {-# INLINE (>>>=) #-}
-
 instance Bound MaybeT where
  m >>>= f = m >>= lift . f
  {-# INLINE (>>>=) #-}
@@ -106,6 +98,16 @@
 instance Monoid w => Bound (WriterT w) where
  m >>>= f = m >>= lift . f
  {-# INLINE (>>>=) #-}
+
+#if !(MIN_VERSION_transformers(0,6,0))
+instance Error e => Bound (ErrorT e) where
+ m >>>= f = m >>= lift . f
+ {-# INLINE (>>>=) #-}
+
+instance Bound ListT where
+ m >>>= f = m >>= lift . f
+ {-# INLINE (>>>=) #-}
+#endif
 
 infixr 1 =<<<
 -- | A flipped version of ('>>>=').
diff --git a/src/Bound/Name.hs b/src/Bound/Name.hs
--- a/src/Bound/Name.hs
+++ b/src/Bound/Name.hs
@@ -1,16 +1,10 @@
 {-# LANGUAGE CPP #-}
 #ifdef __GLASGOW_HASKELL__
 {-# LANGUAGE DeriveDataTypeable #-}
-
-# if __GLASGOW_HASKELL__ >= 704
 {-# LANGUAGE DeriveGeneric #-}
-# endif
-
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
 {-# LANGUAGE Trustworthy #-}
 #endif
 
-#endif
 -----------------------------------------------------------------------------
 -- |
 -- Copyright   :  (C) 2012 Edward Kmett
@@ -37,40 +31,33 @@
   , name
   , abstractName
   , abstract1Name
+  , abstractEitherName
   , instantiateName
   , instantiate1Name
+  , instantiateEitherName
   ) where
 
 import Bound.Scope
 import Bound.Var
-#if __GLASGOW_HASKELL__ < 710
-import Control.Applicative
-#endif
 import Control.Comonad
+import Control.DeepSeq
 import Control.Monad (liftM, liftM2)
-#if __GLASGOW_HASKELL__ < 710
-import Data.Foldable
-import Data.Monoid
-import Data.Traversable
-#endif
 import Data.Bifunctor
 import Data.Bifoldable
 import qualified Data.Binary as Binary
 import Data.Binary (Binary)
 import Data.Bitraversable
 import Data.Bytes.Serial
+import Data.Functor.Classes
 #ifdef __GLASGOW_HASKELL__
 import Data.Data
-# if __GLASGOW_HASKELL__ >= 704
 import GHC.Generics
-# endif
 #endif
-import Data.Hashable
-import Data.Hashable.Extras
+import Data.Hashable (Hashable(..))
+import Data.Hashable.Lifted (Hashable1(..), Hashable2(..))
 import Data.Profunctor
 import qualified Data.Serialize as Serialize
 import Data.Serialize (Serialize)
-import Prelude.Extras
 
 -------------------------------------------------------------------------------
 -- Names
@@ -85,11 +72,9 @@
   ( Show
   , Read
 #ifdef __GLASGOW_HASKELL__
-  , Typeable
   , Data
-# if __GLASGOW_HASKELL__ >= 704
   , Generic
-# endif
+  , Generic1
 #endif
   )
 
@@ -118,12 +103,12 @@
   {-# INLINE (==) #-}
 
 instance Hashable2 Name where
-  hashWithSalt2 m (Name _ a) = hashWithSalt m a
-  {-# INLINE hashWithSalt2 #-}
+  liftHashWithSalt2 _ h s (Name _ a) = h s a
+  {-# INLINE liftHashWithSalt2 #-}
 
 instance Hashable1 (Name n) where
-  hashWithSalt1 m (Name _ a) = hashWithSalt m a
-  {-# INLINE hashWithSalt1 #-}
+  liftHashWithSalt h s (Name _ a) = h s a
+  {-# INLINE liftHashWithSalt #-}
 
 instance Hashable a => Hashable (Name n a) where
   hashWithSalt m (Name _ a) = hashWithSalt m a
@@ -163,25 +148,30 @@
   extend f w@(Name n _) = Name n (f w)
   {-# INLINE extend #-}
 
-instance Eq1   (Name b) where
-  (==#)      = (==)
-  {-# INLINE (==#) #-}
-instance Ord1  (Name b) where
-  compare1   = compare
-  {-# INLINE compare1 #-}
-instance Show b => Show1 (Name b) where showsPrec1 = showsPrec
-instance Read b => Read1 (Name b) where readsPrec1 = readsPrec
+instance Eq2 Name where
+  liftEq2 _ g (Name _ b) (Name _ d) = g b d
 
--- these are slightly too restrictive, but still safe
-instance Eq2 Name   where
-  (==##)     = (==)
-  {-# INLINE (==##) #-}
-instance Ord2 Name  where
-  compare2   = compare
-  {-# INLINE compare2 #-}
-instance Show2 Name where showsPrec2 = showsPrec
-instance Read2 Name where readsPrec2  = readsPrec
+instance Ord2 Name where
+  liftCompare2 _ g (Name _ b) (Name _ d) = g b d
 
+instance Show2 Name where
+  liftShowsPrec2 f _ h _ d (Name a b) = showsBinaryWith f h "Name" d a b
+
+instance Read2 Name where
+  liftReadsPrec2 f _ h _ = readsData $ readsBinaryWith f h "Name" Name
+
+instance Eq1 (Name b) where
+  liftEq f (Name _ b) (Name _ d) = f b d
+
+instance Ord1 (Name b) where
+  liftCompare f (Name _ b) (Name _ d) = f b d
+
+instance Show b => Show1 (Name b) where
+  liftShowsPrec f _ d (Name a b) = showsBinaryWith showsPrec f "Name" d a b
+
+instance Read b => Read1 (Name b) where
+  liftReadsPrec f _ = readsData $ readsBinaryWith readsPrec f "Name" Name
+
 instance Serial2 Name where
   serializeWith2 pb pf (Name b a) = pb b >> pf a
   {-# INLINE serializeWith2 #-}
@@ -209,6 +199,9 @@
   put = serializeWith2 Serialize.put Serialize.put
   get = deserializeWith2 Serialize.get Serialize.get
 
+instance (NFData b, NFData a) => NFData (Name b a) where
+  rnf (Name a b) = rnf a `seq` rnf b
+
 -------------------------------------------------------------------------------
 -- Abstraction
 -------------------------------------------------------------------------------
@@ -226,6 +219,15 @@
 abstract1Name a = abstractName (\b -> if a == b then Just () else Nothing)
 {-# INLINE abstract1Name #-}
 
+-- | Capture some free variables in an expression to yield
+-- a 'Scope' with named bound variables. Optionally change the
+-- types of the remaining free variables.
+abstractEitherName :: Monad f => (a -> Either b c) -> f a -> Scope (Name a b) f c
+abstractEitherName f e = Scope (liftM k e) where
+  k y = case f y of
+    Left z -> B (Name y z)
+    Right y' -> F (return y')
+
 -------------------------------------------------------------------------------
 -- Instantiation
 -------------------------------------------------------------------------------
@@ -244,3 +246,9 @@
 instantiate1Name :: Monad f => f a -> Scope n f a -> f a
 instantiate1Name = instantiate1
 {-# INLINE instantiate1Name #-}
+
+instantiateEitherName :: (Monad f, Comonad n) => (Either b a -> f c) -> Scope (n b) f a -> f c
+instantiateEitherName k e = unscope e >>= \v -> case v of
+  B b -> k (Left (extract b))
+  F a -> a >>= k . Right
+{-# INLINE instantiateEitherName #-}
diff --git a/src/Bound/Scope.hs b/src/Bound/Scope.hs
--- a/src/Bound/Scope.hs
+++ b/src/Bound/Scope.hs
@@ -6,15 +6,8 @@
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE UndecidableInstances #-}
-
-#if __GLASGOW_HASKELL__ >= 702
 {-# LANGUAGE Trustworthy #-}
-#endif
-
-#endif
-
-#ifndef MIN_VERSION_base
-#define MIN_VERSION_base(x,y,z) 1
+{-# LANGUAGE DeriveGeneric #-}
 #endif
 
 -----------------------------------------------------------------------------
@@ -34,9 +27,9 @@
 module Bound.Scope
   ( Scope(..)
   -- * Abstraction
-  , abstract, abstract1
+  , abstract, abstract1, abstractEither
   -- * Instantiation
-  , instantiate, instantiate1
+  , instantiate, instantiate1, instantiateEither
   -- * Traditional de Bruijn
   , fromScope
   , toScope
@@ -69,8 +62,9 @@
 import Bound.Class
 import Bound.Var
 import Control.Applicative
+import Control.DeepSeq
 import Control.Monad hiding (mapM, mapM_)
-import Control.Monad.Trans.Class
+import Control.Monad.Morph
 import Data.Bifunctor
 import Data.Bifoldable
 import qualified Data.Binary as Binary
@@ -80,16 +74,22 @@
 import Data.Bytes.Put
 import Data.Bytes.Serial
 import Data.Foldable
-import Data.Hashable
-import Data.Hashable.Extras
+import Data.Functor.Classes
+import Data.Hashable (Hashable (..))
+import Data.Hashable.Lifted (Hashable1(..), hashWithSalt1)
 import Data.Monoid
 import qualified Data.Serialize as Serialize
 import Data.Serialize (Serialize)
 import Data.Traversable
-import Prelude.Extras
 import Prelude hiding (foldr, mapM, mapM_)
 import Data.Data
+#if defined(__GLASGOW_HASKELL__)
+import GHC.Generics ( Generic, Generic1 )
+#endif
 
+-- $setup
+-- >>> import Bound.Var
+
 -------------------------------------------------------------------------------
 -- Scopes
 -------------------------------------------------------------------------------
@@ -114,10 +114,10 @@
 -- @f (Var b a)@, but the extra @f a@ inside permits us a cheaper 'lift'.
 --
 newtype Scope b f a = Scope { unscope :: f (Var b (f a)) }
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
-  deriving Typeable
+#if defined(__GLASGOW_HASKELL__)
+  deriving (Generic)
 #endif
-
+deriving instance Functor f => Generic1 (Scope b f)
 
 -------------------------------------------------------------------------------
 -- Instances
@@ -145,10 +145,6 @@
 -- | The monad permits substitution on free variables, while preserving
 -- bound variables
 instance Monad f => Monad (Scope b f) where
-#if __GLASGOW_HASKELL__ < 710
-  return a = Scope (return (F (return a)))
-  {-# INLINE return #-}
-#endif
   Scope e >>= f = Scope $ e >>= \v -> case v of
     B b -> return (B b)
     F ea -> ea >>= unscope . f
@@ -158,46 +154,53 @@
   lift m = Scope (return (F m))
   {-# INLINE lift #-}
 
-instance (Monad f, Eq b, Eq1 f, Eq a) => Eq  (Scope b f a) where
-  (==) = (==#)
-  {-# INLINE (==) #-}
-instance (Monad f, Eq b, Eq1 f)       => Eq1 (Scope b f)   where
-  a ==# b = fromScope a ==# fromScope b
-  {-# INLINE (==#) #-}
+instance MFunctor (Scope b) where
+  hoist = hoistScope
+  {-# INLINE hoist #-}
 
-instance (Monad f, Ord b, Ord1 f, Ord a) => Ord  (Scope b f a) where
-  compare = compare1
-  {-# INLINE compare #-}
-instance (Monad f, Ord b, Ord1 f)        => Ord1 (Scope b f) where
-  compare1 a b = fromScope a `compare1` fromScope b
-  {-# INLINE compare1 #-}
+instance (Monad f, Eq b, Eq1 f, Eq a) => Eq  (Scope b f a) where (==) = eq1
+instance (Monad f, Ord b, Ord1 f, Ord a) => Ord  (Scope b f a) where compare = compare1
 
-instance (Functor f, Show b, Show1 f, Show a) => Show (Scope b f a) where
-  showsPrec = showsPrec1
-instance (Functor f, Show b, Show1 f) => Show1 (Scope b f) where
-  showsPrec1 d a = showParen (d > 10) $
-    showString "Scope " . showsPrec1 11 (fmap (fmap Lift1) (unscope a))
+--------------------------------------------------------------------------------
+-- * transformers 0.5 Data.Functor.Classes
+--------------------------------------------------------------------------------
 
-instance (Functor f, Read b, Read1 f, Read a) => Read  (Scope b f a) where
-  readsPrec = readsPrec1
-instance (Functor f, Read b, Read1 f)         => Read1 (Scope b f) where
-  readsPrec1 d = readParen (d > 10) $ \r -> do
-    ("Scope", r') <- lex r
-    (s, r'') <- readsPrec1 11 r'
-    return (Scope (fmap (fmap lower1) s), r'')
+instance (Read b, Read1 f, Read a) => Read  (Scope b f a) where readsPrec = readsPrec1
+instance (Show b, Show1 f, Show a) => Show (Scope b f a) where showsPrec = showsPrec1
 
+instance (Monad f, Eq b, Eq1 f) => Eq1 (Scope b f) where
+  liftEq f m n = liftEq (liftEq f) (fromScope m) (fromScope n)
+
+instance (Monad f, Ord b, Ord1 f) => Ord1 (Scope b f) where
+  liftCompare f m n = liftCompare (liftCompare f) (fromScope m) (fromScope n)
+
+instance (Show b, Show1 f) => Show1 (Scope b f) where
+  liftShowsPrec f g d m = showsUnaryWith (liftShowsPrec (liftShowsPrec f' g') (liftShowList f' g')) "Scope" d (unscope m) where
+    f' = liftShowsPrec f g
+    g' = liftShowList f g
+
+instance (Read b, Read1 f) => Read1 (Scope b f) where
+  liftReadsPrec f g = readsData $ readsUnaryWith (liftReadsPrec (liftReadsPrec f' g') (liftReadList f' g')) "Scope" Scope where
+    f' = liftReadsPrec f g
+    g' = liftReadList f g
+
 instance Bound (Scope b) where
   Scope m >>>= f = Scope (liftM (fmap (>>= f)) m)
   {-# INLINE (>>>=) #-}
 
+--  {-# INLINE hashWithSalt1 #-}
+
 instance (Hashable b, Monad f, Hashable1 f) => Hashable1 (Scope b f) where
-  hashWithSalt1 n m = hashWithSalt1 n (fromScope m)
-  {-# INLINE hashWithSalt1 #-}
+  liftHashWithSalt h s m = liftHashWithSalt (liftHashWithSalt h) s (fromScope m)
+  {-# INLINE liftHashWithSalt #-}
 
 instance (Hashable b, Monad f, Hashable1 f, Hashable a) => Hashable (Scope b f a) where
   hashWithSalt n m = hashWithSalt1 n (fromScope m)
   {-# INLINE hashWithSalt #-}
 
+instance NFData (f (Var b (f a))) => NFData (Scope b f a) where
+  rnf scope = rnf (unscope scope)
+
 -------------------------------------------------------------------------------
 -- Abstraction
 -------------------------------------------------------------------------------
@@ -223,6 +226,15 @@
 abstract1 a = abstract (\b -> if a == b then Just () else Nothing)
 {-# INLINE abstract1 #-}
 
+-- | Capture some free variables in an expression to yield
+-- a 'Scope' with bound variables in @b@. Optionally change the
+-- types of the remaining free variables.
+abstractEither :: Monad f => (a -> Either b c) -> f a -> Scope b f c
+abstractEither f e = Scope (liftM k e) where
+  k y = case f y of
+    Left z -> B z
+    Right y' -> F (return y')
+
 -------------------------------------------------------------------------------
 -- Instantiation
 -------------------------------------------------------------------------------
@@ -246,6 +258,13 @@
 instantiate1 e = instantiate (const e)
 {-# INLINE instantiate1 #-}
 
+-- | Enter a scope, and instantiate all bound and free variables in one go.
+instantiateEither :: Monad f => (Either b a -> f c) -> Scope b f a -> f c
+instantiateEither f s = unscope s >>= \v -> case v of
+  B b -> f (Left b)
+  F ea -> ea >>= f . Right
+{-# INLINE instantiateEither #-}
+
 -------------------------------------------------------------------------------
 -- Traditional de Bruijn
 -------------------------------------------------------------------------------
@@ -362,7 +381,7 @@
 mapMScope_ f g (Scope s) = mapM_ (bimapM_ f (mapM_ g)) s
 {-# INLINE mapMScope_ #-}
 
--- | Traverse both bound and free variables
+-- | 'traverse' the bound variables in a 'Scope'.
 traverseBound :: (Applicative g, Traversable f) =>
                  (b -> g c) -> Scope b f a -> g (Scope c f a)
 traverseBound f (Scope s) = Scope <$> traverse f' s where
@@ -442,22 +461,5 @@
   get = deserializeScope Serialize.get Serialize.get
 
 #ifdef __GLASGOW_HASKELL__
-
-#if __GLASGOW_HASKELL__ < 707
-instance (Typeable b, Typeable1 f) => Typeable1 (Scope b f) where
-  typeOf1 _ = mkTyConApp scopeTyCon [typeOf (undefined :: b), typeOf1 (undefined :: f ())]
-
-scopeTyCon :: TyCon
-#if MIN_VERSION_base(4,4,0)
-scopeTyCon = mkTyCon3 "bound" "Bound.Scope" "Scope"
-#else
-scopeTyCon = mkTyCon "Bound.Scope.Scope"
-#endif
-
-#else
-#define Typeable1 Typeable
-#endif
-
-deriving instance (Typeable b, Typeable1 f, Data a, Data (f (Var b (f a)))) => Data (Scope b f a)
-
+deriving instance (Typeable b, Typeable f, Data a, Data (f (Var b (f a)))) => Data (Scope b f a)
 #endif
diff --git a/src/Bound/Scope/Simple.hs b/src/Bound/Scope/Simple.hs
--- a/src/Bound/Scope/Simple.hs
+++ b/src/Bound/Scope/Simple.hs
@@ -4,18 +4,12 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE UndecidableInstances #-}
-
-#if __GLASGOW_HASKELL__ >= 702
 {-# LANGUAGE Trustworthy #-}
 #endif
 
-#endif
-
-#ifndef MIN_VERSION_base
-#define MIN_VERSION_base(x,y,z) 1
-#endif
 -----------------------------------------------------------------------------
 -- |
 -- Copyright   :  (C) 2013 Edward Kmett
@@ -67,8 +61,9 @@
 import Bound.Class
 import Bound.Var
 import Control.Applicative
+import Control.DeepSeq
 import Control.Monad hiding (mapM, mapM_)
-import Control.Monad.Trans.Class
+import Control.Monad.Morph
 import Data.Bifunctor
 import Data.Bifoldable
 import qualified Data.Binary as Binary
@@ -79,15 +74,21 @@
 import Data.Bytes.Serial
 import Data.Data
 import Data.Foldable
-import Data.Hashable
-import Data.Hashable.Extras
+import Data.Functor.Classes
+import Data.Hashable (Hashable(..))
+import Data.Hashable.Lifted (Hashable1(..), hashWithSalt1)
 import Data.Monoid
 import qualified Data.Serialize as Serialize
 import Data.Serialize (Serialize)
 import Data.Traversable
-import Prelude.Extras
 import Prelude hiding (foldr, mapM, mapM_)
+#if defined(__GLASGOW_HASKELL__)
+import GHC.Generics (Generic, Generic1)
+#endif
 
+-- $setup
+-- >>> import Bound.Var
+
 -------------------------------------------------------------------------------
 -- Scopes
 -------------------------------------------------------------------------------
@@ -107,14 +108,18 @@
 -- Another use case is for syntaxes not stable under substitution,
 -- therefore with only a 'Functor' instance and no 'Monad' instance.
 newtype Scope b f a = Scope { unscope :: f (Var b a) }
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ > 707
-  deriving Typeable
+#if defined(__GLASGOW_HASKELL__)
+  deriving Generic
 #endif
+deriving instance Functor f => Generic1 (Scope b f)
 
 -------------------------------------------------------------------------------
 -- Instances
 -------------------------------------------------------------------------------
 
+instance NFData (f (Var b a)) => NFData (Scope b f a) where
+  rnf (Scope x) = rnf x
+
 instance Functor f => Functor (Scope b f) where
   fmap f (Scope a) = Scope (fmap (fmap f) a)
   {-# INLINE fmap #-}
@@ -128,7 +133,7 @@
   traverse f (Scope a) = Scope <$> traverse (traverse f) a
   {-# INLINE traverse #-}
 
-instance (Functor f, Monad f) => Applicative (Scope b f) where
+instance Monad f => Applicative (Scope b f) where
   pure a = Scope (return (F a))
   {-# INLINE pure #-}
   (<*>) = ap
@@ -137,10 +142,6 @@
 -- | The monad permits substitution on free variables, while preserving
 -- bound variables
 instance Monad f => Monad (Scope b f) where
-#if __GLASGOW_HASKELL__ < 710
-  return a = Scope (return (F a))
-  {-# INLINE return #-}
-#endif
   Scope e >>= f = Scope $ e >>= \v -> case v of
     B b -> return (B b)
     F a -> unscope (f a)
@@ -150,33 +151,37 @@
   lift ma = Scope (liftM F ma)
   {-# INLINE lift #-}
 
-instance (Functor f, Eq b, Eq1 f, Eq a) => Eq  (Scope b f a) where
-  (==) = (==#)
-  {-# INLINE (==) #-}
-instance (Functor f, Eq b, Eq1 f)       => Eq1 (Scope b f)   where
-  a ==# b = unscope a ==# unscope b
-  {-# INLINE (==#) #-}
+instance MFunctor (Scope b) where
+  hoist f = hoistScope f
+  {-# INLINE hoist #-}
 
-instance (Functor f, Ord b, Ord1 f, Ord a) => Ord  (Scope b f a) where
+instance (Eq b, Eq1 f) => Eq1 (Scope b f)  where
+  liftEq f m n = liftEq (liftEq f) (unscope m) (unscope n)
+
+instance (Ord b, Ord1 f) => Ord1 (Scope b f) where
+  liftCompare f m n = liftCompare (liftCompare f) (unscope m) (unscope n)
+
+instance (Show b, Show1 f) => Show1 (Scope b f) where
+  liftShowsPrec f g d m = showParen (d > 10) $
+    showString "Scope " . liftShowsPrec (liftShowsPrec f g) (liftShowList f g) 11 (unscope m)
+
+instance (Read b, Read1 f) => Read1 (Scope b f) where
+  liftReadsPrec f g d = readParen (d > 10) $ \r -> do
+    ("Scope", r') <- lex r
+    (s, r'') <- liftReadsPrec (liftReadsPrec f g) (liftReadList f g) 11 r'
+    return (Scope s, r'')
+
+instance (Eq b, Eq1 f, Eq a) => Eq (Scope b f a) where
+  (==) = eq1
+
+instance (Ord b, Ord1 f, Ord a) => Ord (Scope b f a) where
   compare = compare1
-  {-# INLINE compare #-}
-instance (Functor f, Ord b, Ord1 f)        => Ord1 (Scope b f) where
-  compare1 a b = unscope a `compare1` unscope b
-  {-# INLINE compare1 #-}
 
-instance (Functor f, Show b, Show1 f, Show a) => Show (Scope b f a) where
+instance (Show b, Show1 f, Show a) => Show (Scope b f a) where
   showsPrec = showsPrec1
-instance (Functor f, Show b, Show1 f) => Show1 (Scope b f) where
-  showsPrec1 d a = showParen (d > 10) $
-    showString "Scope " . showsPrec1 11 (unscope a)
 
-instance (Functor f, Read b, Read1 f, Read a) => Read  (Scope b f a) where
+instance (Read b, Read1 f, Read a) => Read (Scope b f a) where
   readsPrec = readsPrec1
-instance (Functor f, Read b, Read1 f)         => Read1 (Scope b f) where
-  readsPrec1 d = readParen (d > 10) $ \r -> do
-    ("Scope", r') <- lex r
-    (s, r'') <- readsPrec1 11 r'
-    return (Scope (fmap lower1 s), r'')
 
 instance Bound (Scope b) where
   Scope m >>>= f = Scope $ m >>= \v -> case v of
@@ -184,11 +189,11 @@
     F a -> liftM F (f a)
   {-# INLINE (>>>=) #-}
 
-instance (Hashable b, Monad f, Hashable1 f) => Hashable1 (Scope b f) where
-  hashWithSalt1 n m = hashWithSalt1 n (unscope m)
-  {-# INLINE hashWithSalt1 #-}
+instance (Hashable b, Hashable1 f) => Hashable1 (Scope b f) where
+  liftHashWithSalt h n m = liftHashWithSalt (liftHashWithSalt h) n (unscope m)
+  {-# INLINE liftHashWithSalt #-}
 
-instance (Hashable b, Monad f, Hashable1 f, Hashable a) => Hashable (Scope b f a) where
+instance (Hashable b, Hashable1 f, Hashable a) => Hashable (Scope b f a) where
   hashWithSalt n m = hashWithSalt1 n (unscope m)
   {-# INLINE hashWithSalt #-}
 
@@ -425,25 +430,5 @@
   get = deserializeScope Serialize.get Serialize.get
 
 #ifdef __GLASGOW_HASKELL__
-
-#if __GLASGOW_HASKELL__ < 707
-instance (Typeable b, Typeable1 f) => Typeable1 (Scope b f) where
-  typeOf1 _ = mkTyConApp scopeTyCon [typeOf (undefined :: b), typeOf1 (undefined :: f ())]
-
-scopeTyCon :: TyCon
-#if MIN_VERSION_base(4,4,0)
-scopeTyCon = mkTyCon3 "bound" "Bound.Scope" "Scope"
-#else
-scopeTyCon = mkTyCon "Bound.Scope.Scope"
-#endif
-
-#else
-
--- only needed for ghc7.8.1rc1 compatibility
-#define Typeable1 Typeable
-
-#endif
-
-deriving instance (Typeable b, Typeable1 f, Data a, Data (f (Var b a))) => Data (Scope b f a)
-
+deriving instance (Typeable b, Typeable f, Data a, Data (f (Var b a))) => Data (Scope b f a)
 #endif
diff --git a/src/Bound/TH.hs b/src/Bound/TH.hs
--- a/src/Bound/TH.hs
+++ b/src/Bound/TH.hs
@@ -1,6 +1,11 @@
-{-# LANGUAGE CPP             #-}
+{-# LANGUAGE CPP           #-}
+{-# LANGUAGE PatternGuards #-}
+
+#if __GLASGOW_HASKELL__ >= 900
+{-# LANGUAGE TemplateHaskellQuotes #-}
+#else
 {-# LANGUAGE TemplateHaskell #-}
-{-# LANGUAGE PatternGuards   #-}
+#endif
 
 -----------------------------------------------------------------------------
 -- |
@@ -15,7 +20,7 @@
 -- 'Monad' instances for data types.
 ----------------------------------------------------------------------------
 
-module Bound.TH 
+module Bound.TH
   (
 #ifdef MIN_VERSION_template_haskell
     makeBound
@@ -25,178 +30,121 @@
 #ifdef MIN_VERSION_template_haskell
 import Data.List        (intercalate)
 import Data.Traversable (for)
-import Control.Monad    (foldM)
+import Control.Monad    (foldM, mzero, guard)
 import Bound.Class      (Bound((>>>=)))
 import Language.Haskell.TH
-#if __GLASGOW_HASKELL__ < 710
-import Control.Applicative (Applicative, pure, (<*>))
-#endif
+import Language.Haskell.TH.Datatype.TyVarBndr
 
--- | 
+import Control.Monad.Trans.Class (lift)
+import Control.Monad.Trans.Maybe (MaybeT (..))
+
+-- |
 -- Use to automatically derive 'Applicative' and 'Monad' instances for
 -- your datatype.
--- 
--- In GHC 7.10 or later the @DeriveAnyClass@ extension may be used to derive the 'Show1' and 'Read1' instances
--- 
+--
+-- Also works for components that are lists or instances of 'Functor',
+-- but still does not work for a great deal of other things.
+--
+-- The @deriving-compat@ package may be used to derive the 'Show1' and 'Read1'
+-- instances. Note that due to Template Haskell staging restrictions, we must
+-- define these instances within the same TH splice as the 'Show' and 'Read'
+-- instances. (This is needed for GHC 9.6 and later, where 'Show' and 'Read'
+-- are quantified superclasses of 'Show1' and 'Read1', respectively.)
+--
 -- @
--- {-# LANGUAGE DeriveAnyClass  #-}
--- {-# LANGUAGE DeriveFunctor   #-}
--- {-# LANGUAGE TemplateHaskell #-}
--- 
--- import Bound          (Scope, makeBound)
--- import Prelude.Extras (Read1, Show1)
+-- {-\# LANGUAGE DeriveFunctor      #-}
+-- {-\# LANGUAGE TemplateHaskell    #-}
 --
--- data Exp a 
---   = V a 
---   | App (Exp a) (Exp a) 
---   | Lam (Scope () Exp a) 
---   | I Int 
---   deriving (Functor, Read, Read1, Show, Show1)
--- 
+-- import Bound                (Scope, makeBound)
+-- import Data.Functor.Classes (Show1, Read1, showsPrec1, readsPrec1)
+-- import Data.Deriving        (deriveShow1, deriveRead1)
+--
+-- data Exp a
+--   = V a
+--   | App (Exp a) (Exp a)
+--   | Lam (Scope () Exp a)
+--   | ND [Exp a]
+--   | I Int
+--   deriving (Functor)
+--
 -- makeBound ''Exp
+--
+-- concat <$> sequence
+--   [ deriveShow1 ''Exp
+--   , deriveRead1 ''Exp
+--   , [d| instance Read a => Read (Exp a) where readsPrec = readsPrec1
+--         instance Show a => Show (Exp a) where showsPrec = showsPrec1
+--       |]
+--   ]
 -- @
--- 
+--
 -- and in GHCi
--- 
--- @
--- ghci> :set -XDeriveAnyClass
--- ghci> :set -XDeriveFunctor 
--- ghci> :set -XTemplateHaskell 
--- ghci> import Bound          (Scope, makeBound)
--- ghci> import Prelude.Extras (Read1, Show1)
--- ghci> data Exp a = V a | App (Exp a) (Exp a) | Lam (Scope () Exp a) | I Int deriving (Functor, Read, Read1, Show, Show1); makeBound ''Exp
--- @
 --
--- or
--- 
--- @ 
--- ghci> :{
--- ghci| data Exp a = V a | App (Exp a) (Exp a) | Lam (Scope () Exp a) | I Int deriving (Functor, Read, Read1, Show, Show1)
--- ghci| makeBound ''Exp
--- ghci| :}
--- 
--- If @DeriveAnyClass@ is not used the instances must be declared explicitly:
--- 
 -- @
--- data Exp a 
---   = V a 
---   | App (Exp a) (Exp a) 
---   | Lam (Scope () Exp a) 
---   | I Int 
---   deriving (Functor, Read, Show)
--- instance Read1 Exp
--- instance Show1 Exp
--- 
--- makeBound ''Exp
--- @ 
--- 
--- or in GHCi:
--- 
--- @
+-- ghci> :set -XDeriveFunctor
+-- ghci> :set -XTemplateHaskell
+-- ghci> import Bound                (Scope, makeBound)
+-- ghci> import Data.Functor.Classes (Show1, Read1, showsPrec1, readsPrec1)
+-- ghci> import Data.Deriving        (deriveShow1, deriveRead1)
 -- ghci> :{
--- ghci| data Exp a = V a | App (Exp a) (Exp a) | Lam (Scope () Exp a) | I Int deriving (Functor, Read, Show)
--- ghci| instance Read1 Exp
--- ghci| instance Show1 Exp
+-- ghci| data Exp a = V a | App (Exp a) (Exp a) | Lam (Scope () Exp a) | ND [Exp a] | I Int deriving (Functor)
 -- ghci| makeBound ''Exp
+-- ghci| fmap concat $ sequence [deriveShow1 ''Exp, deriveRead1 ''Exp, [d| instance Read a => Read (Exp a) where { readsPrec = readsPrec1 }; instance Show a => Show (Exp a) where { showsPrec = showsPrec1 } |]]
 -- ghci| :}
 -- @
--- 
--- 'Eq' and 'Ord' instances need to be derived differently if the data
--- type's immediate components include 'Scope' (or other instances of
--- 'Bound')
--- 
--- In a file with @{-# LANGUAGE StandaloneDeriving #-}@ at the top:
--- 
+--
+-- The 'Eq' and 'Ord' instances can be derived similarly:
+--
 -- @
--- instance Eq1 Exp
--- deriving instance Eq a => Eq (Exp a)
--- 
--- instance Ord1 Exp
--- deriving instance Ord a => Ord (Exp a)
+-- import Data.Functor.Classes (Eq1, Ord1, eq1, compare1)
+-- import Data.Deriving        (deriveEq1, deriveOrd1)
+--
+-- fmap concat $ sequence
+--   [ deriveEq1 ''Exp
+--   , deriveOrd1 ''Exp
+--   , [d| instance Eq a => Eq (Exp a) where (==) = eq1
+--         instance Ord a => Ord (Exp a) where compare = compare1
+--       |]
+--   ]
 -- @
--- 
+--
 -- or in GHCi:
 --
 -- @
--- ghci> :set -XStandaloneDeriving 
--- ghci> deriving instance Eq a => Eq (Exp a); instance Eq1 Exp
--- ghci> deriving instance Ord a => Ord (Exp a); instance Ord1 Exp
+-- ghci> import Data.Functor.Classes (Eq1, Ord1, eq1, compare1)
+-- ghci> import Data.Deriving        (deriveEq1, deriveOrd1)
+-- ghci> :{
+-- ghci| fmap concat $ sequence [deriveEq1 ''Exp, deriveOrd1 ''Exp, [d| instance Eq a => Eq (Exp a) where { (==) = eq1 }; instance Ord a => Ord (Exp a) where { compare = compare1 } |]]
+-- ghci| :}
 -- @
--- 
--- because their 'Eq' and 'Ord' instances require @Exp@ to be a 'Monad':
--- 
+--
+-- We cannot automatically derive 'Eq' and 'Ord' using the standard GHC mechanism,
+-- because instances require @Exp@ to be a 'Monad':
+--
 -- @
---   instance (Monad f, Eq b, Eq1 f, Eq a)    => Eq (Scope b f a)
---   instance (Monad f, Ord b, Ord1 f, Ord a) => Ord (Scope b f a)
+-- instance (Monad f, Eq b, Eq1 f, Eq a)    => Eq (Scope b f a)
+-- instance (Monad f, Ord b, Ord1 f, Ord a) => Ord (Scope b f a)
 -- @
--- 
--- Does not work yet for components that are lists or instances of
--- 'Functor' or with a great deal other things.
 
 makeBound :: Name -> DecsQ
 makeBound name = do
-  let var  :: ExpQ
-      var  = ConE `fmap` getPure name
-
-      bind :: ExpQ
-      bind = constructBind name
-
-#if __GLASGOW_HASKELL__ < 708
-      def :: Name -> DecQ -> [DecQ]
-#if __GLASGOW_HASKELL__ < 706
-      def _theName dec = [dec]
-#else 
-      def theName  dec = [pragInlD theName Inline FunLike AllPhases, dec]
-#endif
-
-      pureBody :: Name -> [DecQ]
-      pureBody pure'or'return = 
-        def pure'or'return 
-          (valD (varP pure'or'return) (normalB var) [])
-
-      bindBody :: [DecQ]
-      bindBody = 
-        def '(>>=)
-          (valD (varP '(>>=)) (normalB bind) [])
-
-  apBody <- do 
-    ff <- newName "ff"  
-    fy <- newName "fy"
-    f  <- newName "f"  
-    y  <- newName "y"
-
-    -- \ff fy -> do
-    --   f <- ff
-    --   y <- fy
-    --   pure (f x)
-    let ap :: ExpQ
-        ap = lamE [varP ff, varP fy] (doE 
-              [bindS   (varP f) (varE ff),
-               bindS   (varP y) (varE fy),
-               noBindS (varE 'pure `appE` (varE f `appE` varE y))])
+  TyConI dec <- reify name
+  case dec of
+    DataD _ _name vars _ cons _ -> makeBound' name vars cons
+    _ -> fail $ show name ++ " Must be a data type."
 
-    pure (def '(<*>) (valD (varP '(<*>)) (normalB ap) []))
+makeBound' :: Name -> [TyVarBndrVis] -> [Con] -> DecsQ
+makeBound' name vars cons = do
+  let instanceHead :: Type
+      instanceHead = name `conAppsT` map VarT (typeVars (init vars))
 
-  -- instance Applicative $name where
-  --   pure   = $var
-  --   (<*>)  = \ff fy -> do
-  --     f <- ff
-  --     y <- fy
-  --     pure (f y)
-  applicative <- 
-    instanceD (cxt []) (appT (conT ''Applicative) (conT name))
-      (pureBody 'pure ++ apBody)
+      var  :: ExpQ
+      var  = ConE `fmap` getPure name vars cons
 
-  -- instance Monad $name where
-  --   return = $var
-  --   (>>=)  = $bind
-  monad <- 
-    instanceD (cxt []) (appT (conT ''Monad) (conT name))
-      (pureBody 'return ++ bindBody)
+      bind :: ExpQ
+      bind = constructBind name vars cons
 
-  pure [applicative, monad]
-#else
-  [d| instance Applicative $(conT name) where
+  [d| instance Applicative $(pure instanceHead) where
         pure = $var
         {-# INLINE pure #-}
 
@@ -206,42 +154,35 @@
           pure (f y)
         {-# INLINE (<*>) #-}
 
-      instance Monad $(conT name) where
-# if __GLASGOW_HASKELL__ < 710
-        return = $var
-        {-# INLINE return #-}
-# endif
-
+      instance Monad $(pure instanceHead) where
         (>>=)  = $bind
         {-# INLINE (>>=) #-}
     |]
-#endif
 
 -- Internals
-data Prop 
-  = Bound 
-  | Konst 
-  | Exp 
+data Prop
+  = Bound
+  | Konst
+  | Funktor Int -- ^ number tells how many layers are there
+  | Exp
   deriving Show
 
-data Components 
+data Components
   = Component Name [(Name, Prop)]
   | Variable Name
   deriving Show
 
-constructBind :: Name -> ExpQ
-constructBind name = do
-  TyConI dec <- reify name
-
-  interpret =<< construct dec
+constructBind :: Name -> [TyVarBndrVis] -> [Con] -> ExpQ
+constructBind name vars cons = do
+  interpret =<< construct name vars cons
 
-construct :: Dec -> Q [Components]
-construct (DataD _ name tyvar constructors _) = do
-  var <- getPure name
+construct :: Name -> [TyVarBndrVis] -> [Con] -> Q [Components]
+construct name vars constructors = do
+  var <- getPure name vars constructors
   for constructors $ \con -> do
     case con of
-      NormalC conName [(_, _)] 
-        | conName == var 
+      NormalC conName [(_, _)]
+        | conName == var
         -> pure (Variable conName)
       NormalC conName types
         -> Component conName `fmap` mapM typeToBnd [ ty | (_, ty) <- types ]
@@ -252,25 +193,26 @@
         bndA <- typeToBnd a
         bndB <- typeToBnd b
         pure (Component conName [bndA, bndB])
-      ForallC{} -> error "Not implemented."
+      _ -> error "Not implemented."
 
   where
   expa :: Type
-  expa = ConT name `AppT` VarT (getName (last tyvar))
+  expa = name `conAppsT` map VarT (typeVars vars)
 
   typeToBnd :: Type -> Q (Name, Prop)
   typeToBnd ty = do
     boundInstance <- isBound ty
+    functorApp <- isFunctorApp ty
     var <- newName "var"
-    pure $ 
-      case () of () 
-                   | ty == expa    -> (var, Exp)
-                   | boundInstance -> (var, Bound)
-                   | ConT{} <- ty  -> (var, Konst)
-                   | otherwise     -> error $ "This is bad: " 
-                                           ++ show ty
-                                           ++ " "
-                                           ++ show boundInstance
+    pure $ case () of
+      _ | ty == expa           -> (var, Exp)
+        | boundInstance        -> (var, Bound)
+        | isKonst ty           -> (var, Konst)
+        | Just n <- functorApp -> (var, Funktor n)
+        | otherwise            -> error $ "This is bad: "
+                                        ++ show ty
+                                        ++ " "
+                                        ++ show boundInstance
 
   -- Checks whether a type is an instance of Bound by stripping its last
   -- two type arguments:
@@ -278,11 +220,28 @@
   --  -> isInstance ''Bound [Scope ()]
   --  -> True
   isBound :: Type -> Q Bool
-  isBound ty 
-    | Just a <- stripLast2 ty = isInstance ''Bound [a]
+  isBound ty
+    -- We might fail with kind error, but we don't care
+    | Just a <- stripLast2 ty = pure False `recover` isInstance ''Bound [a]
     | otherwise               = return False
-construct _ = error "Must be a data type."
 
+  isKonst :: Type -> Bool
+  isKonst ConT {} = True
+  isKonst (VarT n) = n /= tvName (last vars)
+  isKonst (AppT a b) = isKonst a && isKonst b
+  isKonst _ = False
+
+  isFunctorApp :: Type -> Q (Maybe Int)
+  isFunctorApp = runMaybeT . go
+    where
+      go x | x == expa  = pure 0
+      go (f `AppT` x)   = do
+          isFunctor <- lift $ isInstance ''Functor [f]
+          guard isFunctor
+          n <- go x
+          pure $ n + 1
+      go _              = mzero
+
 interpret :: [Components] -> ExpQ
 interpret bnds = do
   x       <- newName "x"
@@ -299,43 +258,46 @@
 
     bind (Component name bounds) = do
      exprs <- foldM bindOne (ConE name) bounds
-     pure $ 
+     pure $
        Match
-       (ConP name [ VarP arg | (arg, _) <- bounds ])
-       (NormalB 
+       (ConP name
+#if MIN_VERSION_template_haskell(2,18,0)
+             []
+#endif
+             [ VarP arg | (arg, _) <- bounds ])
+       (NormalB
          exprs)
         []
 
     bindOne :: Exp -> (Name, Prop) -> Q Exp
     bindOne expr (name, bnd) = case bnd of
-      Bound -> 
+      Bound ->
         pure expr `appE` (varE '(>>>=) `appE` varE name `appE` varE f)
-      Konst -> 
+      Konst ->
         pure expr `appE` varE name
-      Exp   -> 
+      Exp   ->
         pure expr `appE` (varE '(>>=) `appE` varE name `appE` varE f)
+      Funktor n ->
+        pure expr `appE` (pure (fmapN n) `appE` (varE '(>>=) `sectionR` varE f) `appE` varE name)
 
+    fmapN :: Int -> Exp
+    fmapN n = foldr1 (\a b -> VarE '(.) `AppE` a `AppE` b) $ replicate n (VarE 'fmap)
+
   matches <- for bnds bind
   pure $ LamE [VarP x, VarP f] (CaseE (VarE x) matches)
 
 stripLast2 :: Type -> Maybe Type
-stripLast2 (a `AppT` b `AppT` _ `AppT` d) 
+stripLast2 (a `AppT` b `AppT` _ `AppT` d)
   | AppT{} <- d = Nothing
   | otherwise   = Just (a `AppT` b)
-stripLast2 _ = Nothing 
-
-getName :: TyVarBndr -> Name
-getName (PlainTV name)    = name
-getName (KindedTV name _) = name
-
--- Returns candidate 
-getPure :: Name -> Q Name
-getPure name = do
-  TyConI (DataD _ _ tyvr cons _) <- reify name
+stripLast2 _ = Nothing
 
-  let 
+-- Returns candidate
+getPure :: Name -> [TyVarBndrVis] -> [Con] -> Q Name
+getPure _name tyvr cons= do
+  let
     findReturn :: Type -> [(Name, [Type])] -> Name
-    findReturn ty constrs = 
+    findReturn ty constrs =
       case [ constr | (constr, [ty']) <- constrs, ty' == ty ] of
         []  -> error "Too few candidates for a variable constructor."
         [x] -> x
@@ -345,22 +307,39 @@
         xs  -> error ("Too many candidates: " ++ intercalate ", " (map pprint xs))
 
     -- Gets the last type variable, given 'data Exp a b c = ...'
-    -- 
+    --
     --   lastTyVar = c
     lastTyVar :: Type
-    lastTyVar = VarT (last (map getName tyvr))
+    lastTyVar = VarT (last (typeVars tyvr))
 
     allTypeArgs :: Con -> (Name, [Type])
     allTypeArgs con = case con of
-      NormalC conName tys -> 
+      NormalC conName tys ->
         (conName, [ ty |    (_, ty) <- tys ])
-      RecC conName tys -> 
+      RecC conName tys ->
         (conName, [ ty | (_, _, ty) <- tys ])
-      InfixC (_, t1) conName (_, t2) -> 
+      InfixC (_, t1) conName (_, t2) ->
         (conName, [ t1, t2 ])
       ForallC _ _ conName ->
          allTypeArgs conName
+      _ -> error "Not implemented"
 
-  return (findReturn lastTyVar (allTypeArgs `fmap` cons)) 
+  return (findReturn lastTyVar (allTypeArgs `fmap` cons))
+
+-------------------------------------------------------------------------------
+-- Type mangling
+-------------------------------------------------------------------------------
+
+-- | Extract type variables
+typeVars :: [TyVarBndr_ flag] -> [Name]
+typeVars = map tvName
+
+-- | Apply arguments to a type constructor.
+conAppsT :: Name -> [Type] -> Type
+conAppsT conName = foldl AppT (ConT conName)
+
+# if !MIN_VERSION_template_haskell(2,21,0) && !MIN_VERSION_th_abstraction(0,6,0)
+type TyVarBndrVis = TyVarBndrUnit
+# endif
 #else
 #endif
diff --git a/src/Bound/Var.hs b/src/Bound/Var.hs
--- a/src/Bound/Var.hs
+++ b/src/Bound/Var.hs
@@ -2,16 +2,9 @@
 
 #ifdef __GLASGOW_HASKELL__
 {-# LANGUAGE DeriveDataTypeable #-}
-
-#if __GLASGOW_HASKELL__ >= 704
 {-# LANGUAGE DeriveGeneric #-}
-#endif
-
-#if __GLASGOW_HASKELL__ >= 702
 {-# LANGUAGE Trustworthy #-}
 #endif
-
-#endif
 -----------------------------------------------------------------------------
 -- |
 -- Copyright   :  (C) 2012 Edward Kmett
@@ -29,17 +22,10 @@
   , _F
   ) where
 
-#if __GLASGOW_HASKELL__ < 710
-import Control.Applicative
-#endif
+import Control.DeepSeq
 import Control.Monad (liftM, ap)
-#if __GLASGOW_HASKELL__ < 710
-import Data.Foldable
-import Data.Traversable
-import Data.Monoid (mempty)
-#endif
-import Data.Hashable
-import Data.Hashable.Extras
+import Data.Hashable (Hashable(..))
+import Data.Hashable.Lifted (Hashable1(..), Hashable2(..))
 import Data.Bifunctor
 import Data.Bifoldable
 import qualified Data.Binary as Binary
@@ -48,19 +34,14 @@
 import Data.Bytes.Get
 import Data.Bytes.Put
 import Data.Bytes.Serial
-#ifdef __GLASGOW_HASKELL__
-import Data.Data
-# if __GLASGOW_HASKELL__ >= 704
-import GHC.Generics
-# endif
-#endif
+import Data.Functor.Classes
 import Data.Profunctor
 import qualified Data.Serialize as Serialize
 import Data.Serialize (Serialize)
-#if __GLASGOW_HASKELL__ < 710
-import Data.Word
+#ifdef __GLASGOW_HASKELL__
+import Data.Data
+import GHC.Generics
 #endif
-import Prelude.Extras
 
 ----------------------------------------------------------------------------
 -- Bound and Free Variables
@@ -82,18 +63,21 @@
   , Read
 #ifdef __GLASGOW_HASKELL__
   , Data
-  , Typeable
-# if __GLASGOW_HASKELL__ >= 704
   , Generic
-# endif
+  , Generic1
 #endif
   )
 
 distinguisher :: Int
 distinguisher = fromIntegral $ (maxBound :: Word) `quot` 3
 
-instance Hashable2 Var
-instance Hashable b => Hashable1 (Var b)
+instance Hashable2 Var where
+  liftHashWithSalt2 h _ s (B b) = h s b
+  liftHashWithSalt2 _ h s (F a) = h s a `hashWithSalt` distinguisher
+  {-# INLINE liftHashWithSalt2 #-}
+instance Hashable b => Hashable1 (Var b) where
+  liftHashWithSalt = liftHashWithSalt2 hashWithSalt
+  {-# INLINE liftHashWithSalt #-}
 instance (Hashable b, Hashable a) => Hashable (Var b a) where
   hashWithSalt s (B b) = hashWithSalt s b
   hashWithSalt s (F a) = hashWithSalt s a `hashWithSalt` distinguisher
@@ -202,20 +186,36 @@
   bitraverse _ g (F a) = F <$> g a
   {-# INLINE bitraverse #-}
 
-instance Eq2 Var   where
-  (==##)     = (==)
-  {-# INLINE (==##) #-}
-instance Ord2 Var  where
-  compare2   = compare
-  {-# INLINE compare2 #-}
-instance Show2 Var where showsPrec2 = showsPrec
-instance Read2 Var where readsPrec2  = readsPrec
+instance Eq2 Var where
+  liftEq2 f _ (B a) (B c) = f a c
+  liftEq2 _ g (F b) (F d) = g b d
+  liftEq2 _ _ _ _ = False
 
-instance Eq b   => Eq1   (Var b) where
-  (==#)      = (==)
-  {-# INLINE (==#) #-}
-instance Ord b  => Ord1  (Var b) where
-  compare1   = compare
-  {-# INLINE compare1 #-}
-instance Show b => Show1 (Var b) where showsPrec1 = showsPrec
-instance Read b => Read1 (Var b) where readsPrec1  = readsPrec
+instance Ord2 Var where
+  liftCompare2 f _ (B a) (B c) = f a c
+  liftCompare2 _ _ B{} F{} = LT
+  liftCompare2 _ _ F{} B{} = GT
+  liftCompare2 _ g (F b) (F d) = g b d
+
+instance Show2 Var where
+  liftShowsPrec2 f _ _ _ d (B a) = showsUnaryWith f "B" d a
+  liftShowsPrec2 _ _ h _ d (F a) = showsUnaryWith h "F" d a
+
+instance Read2 Var where
+  liftReadsPrec2 f _ h _ = readsData $ readsUnaryWith f "B" B `mappend` readsUnaryWith h "F" F
+
+instance Eq b => Eq1 (Var b) where
+  liftEq = liftEq2 (==)
+
+instance Ord b => Ord1 (Var b) where
+  liftCompare = liftCompare2 compare
+
+instance Show b => Show1 (Var b) where
+  liftShowsPrec = liftShowsPrec2 showsPrec showList
+
+instance Read b => Read1 (Var b) where
+  liftReadsPrec = liftReadsPrec2 readsPrec readList
+
+instance (NFData a, NFData b) => NFData (Var b a) where
+  rnf (B b) = rnf b
+  rnf (F f) = rnf f
diff --git a/tests/doctests.hs b/tests/doctests.hs
deleted file mode 100644
--- a/tests/doctests.hs
+++ /dev/null
@@ -1,30 +0,0 @@
-module Main where
-
-import Build_doctests (deps)
-import Control.Applicative
-import Control.Monad
-import Data.List
-import System.Directory
-import System.FilePath
-import Test.DocTest
-
-main :: IO ()
-main = getSources >>= \sources -> doctest $
-    "-isrc"
-  : "-idist/build/autogen"
-  : "-optP-include"
-  : "-optPdist/build/autogen/cabal_macros.h"
-  : "-hide-all-packages"
-  : map ("-package="++) deps ++ sources
-
-getSources :: IO [FilePath]
-getSources = filter (isSuffixOf ".hs") <$> go "src"
-  where
-    go dir = do
-      (dirs, files) <- getFilesAndDirectories dir
-      (files ++) . concat <$> mapM go dirs
-
-getFilesAndDirectories :: FilePath -> IO ([FilePath], [FilePath])
-getFilesAndDirectories dir = do
-  c <- map (dir </>) . filter (`notElem` ["..", "."]) <$> getDirectoryContents dir
-  (,) <$> filterM doesDirectoryExist c <*> filterM doesFileExist c
diff --git a/travis/cabal-apt-install b/travis/cabal-apt-install
deleted file mode 100644
--- a/travis/cabal-apt-install
+++ /dev/null
@@ -1,27 +0,0 @@
-#! /bin/bash
-set -eu
-
-APT="sudo apt-get -q -y"
-CABAL_INSTALL_DEPS="cabal install --only-dependencies --force-reinstall"
-
-$APT update
-$APT install dctrl-tools
-
-# Find potential system packages to satisfy cabal dependencies
-deps()
-{
-	local M='^\([^ ]\+\)-[0-9.]\+ (.*$'
-	local G=' -o ( -FPackage -X libghc-\L\1\E-dev )'
-	local E="$($CABAL_INSTALL_DEPS "$@" --dry-run -v 2> /dev/null \
-		| sed -ne "s/$M/$G/p" | sort -u)"
-	grep-aptavail -n -sPackage \( -FNone -X None \) $E | sort -u
-}
-
-$APT install $(deps "$@") libghc-quickcheck2-dev # QuickCheck is special
-$CABAL_INSTALL_DEPS "$@" # Install the rest via Hackage
-
-if ! $APT install hlint ; then
-	$APT install $(deps hlint)
-	cabal install hlint
-fi
-
diff --git a/travis/config b/travis/config
deleted file mode 100644
--- a/travis/config
+++ /dev/null
@@ -1,16 +0,0 @@
--- This provides a custom ~/.cabal/config file for use when hackage is down that should work on unix
---
--- This is particularly useful for travis-ci to get it to stop complaining
--- about a broken build when everything is still correct on our end.
---
--- This uses Luite Stegeman's mirror of hackage provided by his 'hdiff' site instead
---
--- To enable this, uncomment the before_script in .travis.yml
-
-remote-repo: hdiff.luite.com:http://hdiff.luite.com/packages/archive
-remote-repo-cache: ~/.cabal/packages
-world-file: ~/.cabal/world
-build-summary: ~/.cabal/logs/build.log
-remote-build-reporting: anonymous
-install-dirs user
-install-dirs global