diff --git a/.gitignore b/.gitignore
--- a/.gitignore
+++ b/.gitignore
@@ -12,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
--- a/.travis.yml
+++ b/.travis.yml
@@ -1,99 +1,173 @@
 # This Travis job script has been generated by a script via
 #
-#   make_travis_yml_2.hs 'bound.cabal'
+#   haskell-ci '--output=.travis.yml' '--config=cabal.haskell-ci' 'cabal.project'
 #
-# For more information, see https://github.com/hvr/multi-ghc-travis
+# To regenerate the script (for example after adjusting tested-with) run
 #
+#   haskell-ci regenerate
+#
+# For more information, see https://github.com/haskell-CI/haskell-ci
+#
+# version: 0.10
+#
+version: ~> 1.0
 language: c
-sudo: false
-
+os: linux
+dist: xenial
 git:
-  submodules: false  # whether to recursively clone submodules
-
+  # whether to recursively clone submodules
+  submodules: false
+notifications:
+  irc:
+    channels:
+      - irc.freenode.org#haskell-lens
+    skip_join: true
+    template:
+      - "\x0313bound\x03/\x0306%{branch}\x03 \x0314%{commit}\x03 %{build_url} %{message}"
 cache:
   directories:
     - $HOME/.cabal/packages
     - $HOME/.cabal/store
-
+    - $HOME/.hlint
 before_cache:
-  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/build-reports.log
+  - rm -fv $CABALHOME/packages/hackage.haskell.org/build-reports.log
   # remove files that are regenerated by 'cabal update'
-  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/00-index.*
-  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/*.json
-  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/01-index.cache
-  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/01-index.tar
-  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/01-index.tar.idx
-
-matrix:
+  - rm -fv $CABALHOME/packages/hackage.haskell.org/00-index.*
+  - rm -fv $CABALHOME/packages/hackage.haskell.org/*.json
+  - rm -fv $CABALHOME/packages/hackage.haskell.org/01-index.cache
+  - rm -fv $CABALHOME/packages/hackage.haskell.org/01-index.tar
+  - rm -fv $CABALHOME/packages/hackage.haskell.org/01-index.tar.idx
+  - rm -rfv $CABALHOME/packages/head.hackage
+jobs:
   include:
-    - compiler: "ghc-7.4.2"
-    # env: TEST=--disable-tests BENCH=--disable-benchmarks
-      addons: {apt: {packages: [ghc-ppa-tools,cabal-install-head,ghc-7.4.2], sources: [hvr-ghc]}}
-    - compiler: "ghc-7.6.3"
-    # env: TEST=--disable-tests BENCH=--disable-benchmarks
-      addons: {apt: {packages: [ghc-ppa-tools,cabal-install-head,ghc-7.6.3], sources: [hvr-ghc]}}
-    - compiler: "ghc-7.8.4"
-    # env: TEST=--disable-tests BENCH=--disable-benchmarks
-      addons: {apt: {packages: [ghc-ppa-tools,cabal-install-head,ghc-7.8.4], sources: [hvr-ghc]}}
-    - compiler: "ghc-7.10.3"
-    # env: TEST=--disable-tests BENCH=--disable-benchmarks
-      addons: {apt: {packages: [ghc-ppa-tools,cabal-install-head,ghc-7.10.3], sources: [hvr-ghc]}}
-    - compiler: "ghc-8.0.2"
-    # env: TEST=--disable-tests BENCH=--disable-benchmarks
-      addons: {apt: {packages: [ghc-ppa-tools,cabal-install-head,ghc-8.0.2], sources: [hvr-ghc]}}
-    - compiler: "ghc-8.2.1"
-    # env: TEST=--disable-tests BENCH=--disable-benchmarks
-      addons: {apt: {packages: [ghc-ppa-tools,cabal-install-head,ghc-8.2.1], sources: [hvr-ghc]}}
-
+    - compiler: ghc-8.10.1
+      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-8.10.1","cabal-install-3.2"]}}
+      os: linux
+    - compiler: ghc-8.8.3
+      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-8.8.3","cabal-install-3.2"]}}
+      os: linux
+    - compiler: ghc-8.6.5
+      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-8.6.5","cabal-install-3.2"]}}
+      os: linux
+    - compiler: ghc-8.4.4
+      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-8.4.4","cabal-install-3.2"]}}
+      os: linux
+    - compiler: ghc-8.2.2
+      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-8.2.2","cabal-install-3.2"]}}
+      os: linux
+    - compiler: ghc-8.0.2
+      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-8.0.2","cabal-install-3.2"]}}
+      os: linux
+    - compiler: ghc-7.10.3
+      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-7.10.3","cabal-install-3.2"]}}
+      os: linux
+    - compiler: ghc-7.8.4
+      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-7.8.4","cabal-install-3.2"]}}
+      os: linux
+    - compiler: ghc-7.6.3
+      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-7.6.3","cabal-install-3.2"]}}
+      os: linux
+    - compiler: ghc-7.4.2
+      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-7.4.2","cabal-install-3.2"]}}
+      os: linux
 before_install:
- - HC=${CC}
- - unset CC
- - PATH=/opt/ghc/bin:/opt/ghc-ppa-tools/bin:$PATH
- - PKGNAME='bound'
-
+  - HC=$(echo "/opt/$CC/bin/ghc" | sed 's/-/\//')
+  - WITHCOMPILER="-w $HC"
+  - HADDOCK=$(echo "/opt/$CC/bin/haddock" | sed 's/-/\//')
+  - HCPKG="$HC-pkg"
+  - unset CC
+  - CABAL=/opt/ghc/bin/cabal
+  - CABALHOME=$HOME/.cabal
+  - export PATH="$CABALHOME/bin:$PATH"
+  - TOP=$(pwd)
+  - "HCNUMVER=$(${HC} --numeric-version|perl -ne '/^(\\d+)\\.(\\d+)\\.(\\d+)(\\.(\\d+))?$/; print(10000 * $1 + 100 * $2 + ($3 == 0 ? $5 != 1 : $3))')"
+  - echo $HCNUMVER
+  - CABAL="$CABAL -vnormal+nowrap"
+  - set -o pipefail
+  - TEST=--enable-tests
+  - BENCH=--enable-benchmarks
+  - HEADHACKAGE=false
+  - rm -f $CABALHOME/config
+  - |
+    echo "verbose: normal +nowrap +markoutput"          >> $CABALHOME/config
+    echo "remote-build-reporting: anonymous"            >> $CABALHOME/config
+    echo "write-ghc-environment-files: always"          >> $CABALHOME/config
+    echo "remote-repo-cache: $CABALHOME/packages"       >> $CABALHOME/config
+    echo "logs-dir:          $CABALHOME/logs"           >> $CABALHOME/config
+    echo "world-file:        $CABALHOME/world"          >> $CABALHOME/config
+    echo "extra-prog-path:   $CABALHOME/bin"            >> $CABALHOME/config
+    echo "symlink-bindir:    $CABALHOME/bin"            >> $CABALHOME/config
+    echo "installdir:        $CABALHOME/bin"            >> $CABALHOME/config
+    echo "build-summary:     $CABALHOME/logs/build.log" >> $CABALHOME/config
+    echo "store-dir:         $CABALHOME/store"          >> $CABALHOME/config
+    echo "install-dirs user"                            >> $CABALHOME/config
+    echo "  prefix: $CABALHOME"                         >> $CABALHOME/config
+    echo "repository hackage.haskell.org"               >> $CABALHOME/config
+    echo "  url: http://hackage.haskell.org/"           >> $CABALHOME/config
 install:
- - cabal --version
- - echo "$(${HC} --version) [$(${HC} --print-project-git-commit-id 2> /dev/null || echo '?')]"
- - BENCH=${BENCH---enable-benchmarks}
- - TEST=${TEST---enable-tests}
- - travis_retry cabal update -v
- - sed -i 's/^jobs:/-- jobs:/' ${HOME}/.cabal/config
- - rm -fv cabal.project.local
- - "echo 'packages: .' > cabal.project"
- - rm -f cabal.project.freeze
- - cabal new-build -w ${HC} ${TEST} ${BENCH} --dep -j2 all
- - cabal new-build -w ${HC} --disable-tests --disable-benchmarks --dep -j2 all
-
-# Here starts the actual work to be performed for the package under test;
-# any command which exits with a non-zero exit code causes the build to fail.
+  - ${CABAL} --version
+  - echo "$(${HC} --version) [$(${HC} --print-project-git-commit-id 2> /dev/null || echo '?')]"
+  - |
+    echo "program-default-options"                >> $CABALHOME/config
+    echo "  ghc-options: $GHCJOBS +RTS -M6G -RTS" >> $CABALHOME/config
+  - cat $CABALHOME/config
+  - rm -fv cabal.project cabal.project.local cabal.project.freeze
+  - travis_retry ${CABAL} v2-update -v
+  # Generate cabal.project
+  - rm -rf cabal.project cabal.project.local cabal.project.freeze
+  - touch cabal.project
+  - |
+    echo "packages: ." >> cabal.project
+    echo "packages: ./doc" >> cabal.project
+  - if [ $HCNUMVER -ge 80200 ] ; then echo 'package bound' >> cabal.project ; fi
+  - "if [ $HCNUMVER -ge 80200 ] ; then echo '  ghc-options: -Werror=missing-methods' >> cabal.project ; fi"
+  - if [ $HCNUMVER -ge 80200 ] ; then echo 'package bound-laws' >> cabal.project ; fi
+  - "if [ $HCNUMVER -ge 80200 ] ; then echo '  ghc-options: -Werror=missing-methods' >> cabal.project ; fi"
+  - |
+  - "for pkg in $($HCPKG list --simple-output); do echo $pkg | sed 's/-[^-]*$//' | (grep -vE -- '^(bound|bound-laws)$' || true) | sed 's/^/constraints: /' | sed 's/$/ installed/' >> cabal.project.local; done"
+  - cat cabal.project || true
+  - cat cabal.project.local || true
+  - if [ -f "./configure.ac" ]; then (cd "." && autoreconf -i); fi
+  - if [ -f "./doc/configure.ac" ]; then (cd "./doc" && autoreconf -i); fi
+  - ${CABAL} v2-freeze $WITHCOMPILER ${TEST} ${BENCH}
+  - "cat cabal.project.freeze | sed -E 's/^(constraints: *| *)//' | sed 's/any.//'"
+  - rm  cabal.project.freeze
+  - travis_wait 40 ${CABAL} v2-build $WITHCOMPILER ${TEST} ${BENCH} --dep -j2 all
 script:
- - if [ -f configure.ac ]; then autoreconf -i; fi
- - rm -rf dist/ .ghc.environment.*
- - cabal sdist # test that a source-distribution can be generated
- - cd dist/
- - SRCTAR=(${PKGNAME}-*.tar.gz)
- - SRC_BASENAME="${SRCTAR/%.tar.gz}"
- - tar -xvf "./$SRC_BASENAME.tar.gz"
- - cd "$SRC_BASENAME/"
-## from here on, CWD is inside the extracted source-tarball
- - rm -fv cabal.project.local
- - "echo 'packages: .' > cabal.project"
- # this builds all libraries and executables (without tests/benchmarks)
- - rm -f cabal.project.freeze
- - cabal new-build -w ${HC} --disable-tests --disable-benchmarks all
- # this builds all libraries and executables (including tests/benchmarks)
- # - rm -rf ./dist-newstyle
-
- # build & run tests
- - cabal new-build -w ${HC} ${TEST} ${BENCH} all
- - if [ "x$TEST" = "x--enable-tests" ]; then cabal new-test -w ${HC} ${TEST} all; fi
+  - DISTDIR=$(mktemp -d /tmp/dist-test.XXXX)
+  # Packaging...
+  - ${CABAL} v2-sdist all
+  # Unpacking...
+  - mv dist-newstyle/sdist/*.tar.gz ${DISTDIR}/
+  - cd ${DISTDIR} || false
+  - find . -maxdepth 1 -type f -name '*.tar.gz' -exec tar -xvf '{}' \;
+  - find . -maxdepth 1 -type f -name '*.tar.gz' -exec rm       '{}' \;
+  - PKGDIR_bound="$(find . -maxdepth 1 -type d -regex '.*/bound-[0-9.]*')"
+  - PKGDIR_bound_laws="$(find . -maxdepth 1 -type d -regex '.*/bound-laws-[0-9.]*')"
+  # Generate cabal.project
+  - rm -rf cabal.project cabal.project.local cabal.project.freeze
+  - touch cabal.project
+  - |
+    echo "packages: ${PKGDIR_bound}" >> cabal.project
+    echo "packages: ${PKGDIR_bound_laws}" >> cabal.project
+  - if [ $HCNUMVER -ge 80200 ] ; then echo 'package bound' >> cabal.project ; fi
+  - "if [ $HCNUMVER -ge 80200 ] ; then echo '  ghc-options: -Werror=missing-methods' >> cabal.project ; fi"
+  - if [ $HCNUMVER -ge 80200 ] ; then echo 'package bound-laws' >> cabal.project ; fi
+  - "if [ $HCNUMVER -ge 80200 ] ; then echo '  ghc-options: -Werror=missing-methods' >> cabal.project ; fi"
+  - |
+  - "for pkg in $($HCPKG list --simple-output); do echo $pkg | sed 's/-[^-]*$//' | (grep -vE -- '^(bound|bound-laws)$' || true) | sed 's/^/constraints: /' | sed 's/$/ installed/' >> cabal.project.local; done"
+  - cat cabal.project || true
+  - cat cabal.project.local || true
+  # Building with tests and benchmarks...
+  # build & run tests, build benchmarks
+  - ${CABAL} v2-build $WITHCOMPILER ${TEST} ${BENCH} all
+  # Testing...
+  - ${CABAL} v2-test $WITHCOMPILER ${TEST} ${BENCH} all
+  # cabal check...
+  - (cd ${PKGDIR_bound} && ${CABAL} -vnormal check)
+  - (cd ${PKGDIR_bound_laws} && ${CABAL} -vnormal check)
+  # haddock...
+  - ${CABAL} v2-haddock $WITHCOMPILER --with-haddock $HADDOCK ${TEST} ${BENCH} all
 
+# REGENDATA ("0.10",["--output=.travis.yml","--config=cabal.haskell-ci","cabal.project"])
 # EOF
-
-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,7 @@
+2.0.2 [2020.10.01]
+------------------
+* Allow building with GHC 9.0.
+
 2.0.1
 -----
 * Add `abstractEither` and `instantiateEither` to `Bound.Scope`, and
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:       2.0.1
+version:       2.0.2
 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>
@@ -38,10 +38,9 @@
   .ghci
   .gitignore
   .vim.custom
-  examples/Simple.hs
-  examples/Deriving.hs
-  examples/Overkill.hs
-  tests/doctests.hs
+  doc/*.hs
+  doc/bound-laws.cabal
+  doc/LICENSE
   travis/cabal-apt-install
   travis/config
   README.markdown
@@ -54,7 +53,11 @@
   GHC==7.8.4,
   GHC==7.10.3,
   GHC==8.0.2,
-  GHC==8.2.1
+  GHC==8.2.2,
+  GHC==8.4.4,
+  GHC==8.6.5,
+  GHC==8.8.3,
+  GHC==8.10.1
 
 flag template-haskell
   description:
@@ -66,9 +69,9 @@
 
 custom-setup
   setup-depends:
-    base >= 4 && <5,
+    base          >= 4.5   && < 5,
     Cabal,
-    cabal-doctest >= 1.0.1 && <1.1
+    cabal-doctest >= 1.0.1 && < 1.1
 
 source-repository head
   type: git
@@ -88,22 +91,25 @@
     Bound.Var
 
   build-depends:
-    base             >= 4       && < 5,
+    base             >= 4.5     && < 5,
     bifunctors       >= 3       && < 6,
     binary           >= 0.5     && < 0.9,
     bytes            >= 0.4     && < 1,
     cereal           >= 0.3.5.2 && < 0.6,
     comonad          >= 3       && < 6,
-    hashable         >= 1.2.5.0 && < 1.3,
+    hashable         >= 1.2.5.0 && < 1.4,
     mmorph           >= 1.0     && < 1.2,
     deepseq          >= 1.1     && < 1.5,
     profunctors      >= 3.3     && < 6,
     template-haskell >= 2.7     && < 3,
+    th-abstraction   >= 0.4     && < 0.5,
     transformers     >= 0.2     && < 0.6,
     transformers-compat >= 0.5  && < 1
 
   ghc-options: -Wall -O2 -fspec-constr -fdicts-cheap -funbox-strict-fields
 
+  default-language: Haskell2010
+
   if impl(ghc >=7.4 && < 7.6)
     build-depends: ghc-prim
 
@@ -117,10 +123,11 @@
   buildable: True
 
   ghc-options: -Wall -threaded
+  default-language: Haskell2010
   build-depends:
-    base,
+    base            >= 4.5   && < 5,
     bound,
-    deriving-compat >=0.3.4 && <0.4,
+    deriving-compat >= 0.3.4 && < 0.6,
     transformers,
     transformers-compat
 
@@ -128,9 +135,12 @@
   type: exitcode-stdio-1.0
   main-is: Overkill.hs
   hs-source-dirs: examples
-  ghc-options: -Wall -threaded -main-is Overkill
+  ghc-options: -Wall -threaded
+  if impl(ghc >= 8.6)
+    ghc-options: -Wno-star-is-type
+  default-language: Haskell2010
   build-depends:
-    base,
+    base >= 4.5 && < 5,
     bound,
     transformers,
     transformers-compat,
@@ -143,9 +153,10 @@
   type: exitcode-stdio-1.0
   main-is: Deriving.hs
   hs-source-dirs: examples
-  ghc-options: -Wall -threaded -main-is Deriving
+  ghc-options: -Wall -threaded
+  default-language: Haskell2010
   build-depends:
-    base,
+    base >= 4.5 && < 5,
     bound,
     transformers,
     transformers-compat
@@ -154,9 +165,10 @@
   type: exitcode-stdio-1.0
   main-is: Imperative.hs
   hs-source-dirs: examples
-  ghc-options: -Wall -threaded -main-is Imperative
+  ghc-options: -Wall -threaded
+  default-language: Haskell2010
   build-depends:
-    base,
+    base >= 4.5 && < 5,
     bound,
     transformers,
     transformers-compat,
@@ -167,9 +179,10 @@
   main-is: doctests.hs
   hs-source-dirs: tests
   ghc-options: -Wall -threaded
+  default-language: Haskell2010
   build-depends:
-    base,
+    base      >= 4.5    && < 5,
     bound,
-    doctest   >= 0.11.2 && < 0.13,
-    vector    >= 0.9 && < 0.13,
+    doctest   >= 0.11.2 && < 0.18,
+    vector    >= 0.9    && < 0.13,
     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
+#if !(MIN_VERSION_base(4,8,0))
+import Control.Applicative hiding (Const(..))
+#endif
+import Control.Monad
+
+{-
+
+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 :: * -> *) a = Const x
+
+instance Bound (Const x) where
+  Const x >>>= _ = Const x
+
+
+newtype Identity (m :: * -> *) a = Id (m a)
+
+instance Bound Identity where
+   Id ma >>>= f = Id (ma >>= f)
+
+
+data Product f g (m :: * -> *) 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 :: * -> *) 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 :: (* -> *) -> * -> *) 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
+  return = Var
+  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,42 @@
+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==7.4.2,
+  GHC==7.6.3,
+  GHC==7.8.4,
+  GHC==7.10.3,
+  GHC==8.0.2,
+  GHC==8.2.2,
+  GHC==8.4.4,
+  GHC==8.6.5,
+  GHC==8.8.3,
+  GHC==8.10.1
+
+source-repository head
+  type: git
+  location: git://github.com/ekmett/bound.git
+
+library
+  exposed-modules: BoundLaws
+  hs-source-dirs: .
+  ghc-options: -Wall
+  if impl(ghc >= 8.6)
+    ghc-options: -Wno-star-is-type
+  default-language: Haskell2010
+  build-depends:
+    base >= 4.5 && < 5,
+    bound
diff --git a/examples/Deriving.hs b/examples/Deriving.hs
--- a/examples/Deriving.hs
+++ b/examples/Deriving.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE CPP, DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
-module Deriving where
+module Main where
 
 import Data.List
 import Data.Foldable
diff --git a/examples/Imperative.hs b/examples/Imperative.hs
--- a/examples/Imperative.hs
+++ b/examples/Imperative.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable, RankNTypes, ScopedTypeVariables #-}
-module Imperative where
+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
@@ -8,7 +8,7 @@
 -- statement.
 
 import Bound.Class
-import Bound.Scope.Simple
+import Bound.Scope -- .Simple
 import Bound.Term
 import Bound.Var
 import Control.Applicative
@@ -22,14 +22,14 @@
 
 
 -- 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
@@ -52,13 +52,13 @@
 -- 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
@@ -84,36 +84,36 @@
   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
-        . (forall v. 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 = Scope . f (fmap F v) . unscope
+        f' v = toScope . f (fmap F v) . fromScope
 
 pAbstract1 :: forall operand a. (Applicative operand, Monad operand, Eq a)
            => a
@@ -121,7 +121,7 @@
            -> Prog (Scope () operand) a
 pAbstract1 = go abstract1
   where
-    go :: forall o o' u. Eq u
+    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)
@@ -129,7 +129,7 @@
                           $ go f' x cc
       where
         f' :: forall v. Eq v => v -> Scope () o v -> Scope () o' v
-        f' v = Scope . f (F v) . unscope
+        f' v = toScope . f (F v) . fromScope
 
 evalOperand :: Operand Void -> Int
 evalOperand (Lit i)    = i
@@ -142,7 +142,7 @@
 --               $ Add (Var "%0") (Var "%0") $ pAbstract1 "%1"
 --               $ Ret (Var "%1")
 -- :}
--- 
+--
 -- >>> evalProg prog
 -- 6
 evalProg :: Prog Operand Void -> Int
@@ -151,41 +151,41 @@
   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
@@ -211,8 +211,8 @@
                -> Prog' operand identity a
 pInstantiate1' = go (instantiate1 . pure) (instantiate1 . pure)
   where
-    go :: forall o o' i i' u
-        . (forall v. v -> o v -> o' v)
+    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'
@@ -224,12 +224,12 @@
         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 = Scope . fo (F v) . unscope
-        
+        fo' v = toScope . fo (F v) . fromScope
+
         fi' :: v -> Scope () i v -> Scope () i' v
-        fi' v = Scope . fi (F v) . unscope
+        fi' v = toScope . fi (F v) . fromScope
 
 pAbstract1' :: ( Applicative operand, Monad operand
                , Applicative identity, Monad identity
@@ -240,7 +240,7 @@
             -> Prog' (Scope () operand) (Scope () identity) a
 pAbstract1' = go abstract1 abstract1
   where
-    go :: forall o o' i i' u. Eq u
+    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
@@ -253,12 +253,12 @@
         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 = Scope . fo (F v) . unscope
-        
+        fo' v = toScope . fo (F v) . fromScope
+
         fi' :: Eq v => v -> Scope () i v -> Scope () i' v
-        fi' v = Scope . fi (F v) . unscope
+        fi' v = toScope . fi (F v) . fromScope
 
 evalOperand' :: Operand (IORef Int) -> IO Int
 evalOperand' (Lit i)   = return i
@@ -272,7 +272,7 @@
 --                $ Swp' (Identity "%0") (Identity "%1")
 --                $ Ret' (Var "%1")
 -- :}
--- 
+--
 -- >>> evalProg' prog'
 -- 3
 evalProg' :: Prog' Operand Identity (IORef Int) -> IO Int
diff --git a/examples/Overkill.hs b/examples/Overkill.hs
--- a/examples/Overkill.hs
+++ b/examples/Overkill.hs
@@ -7,7 +7,7 @@
 
 {-# OPTIONS_GHC -fwarn-incomplete-patterns -fno-warn-orphans #-}
 
-module Overkill where
+module Main where
 
 -- Dara.Functor.Classes in transformers 0.4.0 are totally different
 #if MIN_VERSION_transformers(0,5,0) || !MIN_VERSION_transformers(0,4,0)
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
@@ -170,11 +170,7 @@
   {-# INLINE lift #-}
 
 instance MFunctor (Scope b) where
-#if !MIN_VERSION_base(4,8,0)
   hoist f = hoistScope f
-#else
-  hoist = hoistScope
-#endif
   {-# INLINE hoist #-}
 
 #if (MIN_VERSION_transformers(0,5,0)) || !(MIN_VERSION_transformers(0,4,0))
diff --git a/src/Bound/TH.hs b/src/Bound/TH.hs
--- a/src/Bound/TH.hs
+++ b/src/Bound/TH.hs
@@ -28,6 +28,7 @@
 import Control.Monad    (foldM, mzero, guard)
 import Bound.Class      (Bound((>>>=)))
 import Language.Haskell.TH
+import Language.Haskell.TH.Datatype.TyVarBndr
 #if __GLASGOW_HASKELL__ < 710
 import Control.Applicative (Applicative, pure, (<*>))
 #endif
@@ -49,7 +50,7 @@
 -- {-\# LANGUAGE TemplateHaskell    #-}
 --
 -- import Bound                (Scope, makeBound)
--- import Data.Functor.Classes (Show1, Read1, shosPrec1, readsPrec1)
+-- import Data.Functor.Classes (Show1, Read1, showsPrec1, readsPrec1)
 -- import Data.Deriving        (deriveShow1, deriveRead1)
 --
 -- data Exp a
@@ -129,7 +130,7 @@
 #endif
     _ -> fail $ show name ++ " Must be a data type."
 
-makeBound' :: Name -> [TyVarBndr] -> [Con] -> DecsQ
+makeBound' :: Name -> [TyVarBndrUnit] -> [Con] -> DecsQ
 makeBound' name vars cons = do
   let instanceHead :: Type
       instanceHead = name `conAppsT` map VarT (typeVars (init vars))
@@ -229,11 +230,11 @@
   | Variable Name
   deriving Show
 
-constructBind :: Name -> [TyVarBndr] -> [Con] -> ExpQ
+constructBind :: Name -> [TyVarBndrUnit] -> [Con] -> ExpQ
 constructBind name vars cons = do
   interpret =<< construct name vars cons
 
-construct :: Name -> [TyVarBndr] -> [Con] -> Q [Components]
+construct :: Name -> [TyVarBndrUnit] -> [Con] -> Q [Components]
 construct name vars constructors = do
   var <- getPure name vars constructors
   for constructors $ \con -> do
@@ -284,7 +285,7 @@
 
   isKonst :: Type -> Bool
   isKonst ConT {} = True
-  isKonst (VarT n) = n /= getName (last vars)
+  isKonst (VarT n) = n /= tvName (last vars)
   isKonst (AppT a b) = isKonst a && isKonst b
   isKonst _ = False
 
@@ -345,12 +346,8 @@
   | otherwise   = Just (a `AppT` b)
 stripLast2 _ = Nothing
 
-getName :: TyVarBndr -> Name
-getName (PlainTV name)    = name
-getName (KindedTV name _) = name
-
 -- Returns candidate
-getPure :: Name -> [TyVarBndr] -> [Con] -> Q Name
+getPure :: Name -> [TyVarBndrUnit] -> [Con] -> Q Name
 getPure _name tyvr cons= do
   let
     findReturn :: Type -> [(Name, [Type])] -> Name
@@ -367,7 +364,7 @@
     --
     --   lastTyVar = c
     lastTyVar :: Type
-    lastTyVar = VarT (last (map getName tyvr))
+    lastTyVar = VarT (last (typeVars tyvr))
 
     allTypeArgs :: Con -> (Name, [Type])
     allTypeArgs con = case con of
@@ -391,13 +388,9 @@
 -- Type mangling
 -------------------------------------------------------------------------------
 
--- | Extraty type variables
-typeVars :: [TyVarBndr] -> [Name]
-typeVars = map varBindName
-
-varBindName :: TyVarBndr -> Name
-varBindName (PlainTV n)    = n
-varBindName (KindedTV n _) = n
+-- | Extract type variables
+typeVars :: [TyVarBndr_ flag] -> [Name]
+typeVars = map tvName
 
 -- | Apply arguments to a type constructor.
 conAppsT :: Name -> [Type] -> Type