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/.travis.yml b/.travis.yml
--- a/.travis.yml
+++ b/.travis.yml
@@ -1,145 +1,171 @@
 # This Travis job script has been generated by a script via
 #
-#   runghc make_travis_yml_2.hs '-o' '.travis.yml' '--irc-channel=irc.freenode.org#haskell-lens' '--no-no-tests-no-bench' '--no-installed' 'cabal.project'
+#   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"
+      - irc.freenode.org#haskell-lens
     skip_join: true
     template:
       - "\x0313eq\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
-
-  - rm -rfv $HOME/.cabal/packages/head.hackage
-
-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.0.4"
-    # env: TEST=--disable-tests BENCH=--disable-benchmarks
-      addons: {apt: {packages: [*apt_packages,cabal-install-2.0,ghc-7.0.4], sources: [hvr-ghc]}}
-    - compiler: "ghc-7.2.2"
-    # env: TEST=--disable-tests BENCH=--disable-benchmarks
-      addons: {apt: {packages: [*apt_packages,cabal-install-2.0,ghc-7.2.2], sources: [hvr-ghc]}}
-    - compiler: "ghc-7.4.2"
-    # env: TEST=--disable-tests BENCH=--disable-benchmarks
-      addons: {apt: {packages: [*apt_packages,cabal-install-2.0,ghc-7.4.2], sources: [hvr-ghc]}}
-    - compiler: "ghc-7.6.3"
-    # env: TEST=--disable-tests BENCH=--disable-benchmarks
-      addons: {apt: {packages: [*apt_packages,cabal-install-2.0,ghc-7.6.3], sources: [hvr-ghc]}}
-    - compiler: "ghc-7.8.4"
-    # env: TEST=--disable-tests BENCH=--disable-benchmarks
-      addons: {apt: {packages: [*apt_packages,cabal-install-2.0,ghc-7.8.4], sources: [hvr-ghc]}}
-    - compiler: "ghc-7.10.3"
-    # env: TEST=--disable-tests BENCH=--disable-benchmarks
-      addons: {apt: {packages: [*apt_packages,cabal-install-2.0,ghc-7.10.3], sources: [hvr-ghc]}}
-    - compiler: "ghc-8.0.2"
-    # env: TEST=--disable-tests BENCH=--disable-benchmarks
-      addons: {apt: {packages: [*apt_packages,cabal-install-2.0,ghc-8.0.2], sources: [hvr-ghc]}}
-    - compiler: "ghc-8.2.2"
-    # env: TEST=--disable-tests BENCH=--disable-benchmarks
-      addons: {apt: {packages: [*apt_packages,cabal-install-2.0,ghc-8.2.2], sources: [hvr-ghc]}}
-    - compiler: "ghc-8.4.2"
-    # env: TEST=--disable-tests BENCH=--disable-benchmarks
-      addons: {apt: {packages: [*apt_packages,cabal-install-2.2,ghc-8.4.2], sources: [hvr-ghc]}}
-    - compiler: "ghc-head"
-      env: GHCHEAD=true
-      addons: {apt: {packages: [*apt_packages,cabal-install-head,ghc-head], 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
+    - compiler: ghc-7.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-7.2.2","cabal-install-3.2"]}}
+      os: linux
+    - compiler: ghc-7.0.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.0.4","cabal-install-3.2"]}}
+      os: linux
   allow_failures:
-    - compiler: "ghc-7.0.4"
-    - compiler: "ghc-7.2.2"
-    - compiler: "ghc-head"
-
+    - compiler: ghc-7.0.4
+    - compiler: ghc-7.2.2
 before_install:
-  - HC=${CC}
-  - HCPKG=${HC/ghc/ghc-pkg}
+  - HC=$(echo "/opt/$CC/bin/ghc" | sed 's/-/\//')
+  - WITHCOMPILER="-w $HC"
+  - HADDOCK=$(echo "/opt/$CC/bin/haddock" | sed 's/-/\//')
+  - HCPKG="$HC-pkg"
   - unset CC
-  - ROOTDIR=$(pwd)
-  - mkdir -p $HOME/.local/bin
-  - "PATH=/opt/ghc/bin:/opt/ghc-ppa-tools/bin:$HOME/local/bin:$PATH"
-  - HCNUMVER=$(( $(${HC} --numeric-version|sed -E 's/([0-9]+)\.([0-9]+)\.([0-9]+).*/\1 * 10000 + \2 * 100 + \3/') ))
+  - 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
+  - ${CABAL} --version
   - echo "$(${HC} --version) [$(${HC} --print-project-git-commit-id 2> /dev/null || echo '?')]"
-  - BENCH=${BENCH---enable-benchmarks}
-  - TEST=${TEST---enable-tests}
-  - HADDOCK=${HADDOCK-true}
-  - INSTALLED=${INSTALLED-true}
-  - GHCHEAD=${GHCHEAD-false}
-  - travis_retry cabal update -v
-  - "sed -i.bak 's/^jobs:/-- jobs:/' ${HOME}/.cabal/config"
-  - rm -fv cabal.project cabal.project.local
-  # Overlay Hackage Package Index for GHC HEAD: https://github.com/hvr/head.hackage
   - |
-    if $GHCHEAD; then
-      sed -i.bak 's/-- allow-newer:.*/allow-newer: *:base, *:template-haskell, *:ghc, *:Cabal/' ${HOME}/.cabal/config
-
-      echo 'repository head.hackage'                                                        >> ${HOME}/.cabal/config
-      echo '   url: http://head.hackage.haskell.org/'                                       >> ${HOME}/.cabal/config
-      echo '   secure: True'                                                                >> ${HOME}/.cabal/config
-      echo '   root-keys: 07c59cb65787dedfaef5bd5f987ceb5f7e5ebf88b904bbd4c5cbdeb2ff71b740' >> ${HOME}/.cabal/config
-      echo '              2e8555dde16ebd8df076f1a8ef13b8f14c66bad8eafefd7d9e37d0ed711821fb' >> ${HOME}/.cabal/config
-      echo '              8f79fd2389ab2967354407ec852cbe73f2e8635793ac446d09461ffb99527f6e' >> ${HOME}/.cabal/config
-      echo '   key-threshold: 3'                                                            >> ${HOME}/.cabal.config
-
-      cabal new-update head.hackage -v
-    fi
-  - grep -Ev -- '^\s*--' ${HOME}/.cabal/config | grep -Ev '^\s*$'
-  - "printf 'packages: \".\"\\n' > cabal.project"
-  - cat cabal.project
-  - if [ -f "./configure.ac" ]; then
-      (cd "." && autoreconf -i);
-    fi
-  - rm -f cabal.project.freeze
-  - cabal new-build -w ${HC} ${TEST} ${BENCH} --project-file="cabal.project" --dep -j2 all
-  - rm -rf "."/.ghc.environment.* "."/dist
-  - DISTDIR=$(mktemp -d /tmp/dist-test.XXXX)
-
-# 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.
+    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
+  - if [ $HCNUMVER -ge 80200 ] ; then echo 'package eq' >> 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 -- '^(eq)$' || 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
+  - ${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:
-  # test that source-distributions can be generated
-  - (cd "." && cabal sdist)
-  - mv "."/dist/eq-*.tar.gz ${DISTDIR}/
+  - 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 -name '*.tar.gz' -exec tar -xvf '{}' \;
-  - "printf 'packages: eq-*/*.cabal\\n' > cabal.project"
-  - cat cabal.project
-
-
+  - find . -maxdepth 1 -type f -name '*.tar.gz' -exec tar -xvf '{}' \;
+  - find . -maxdepth 1 -type f -name '*.tar.gz' -exec rm       '{}' \;
+  - PKGDIR_eq="$(find . -maxdepth 1 -type d -regex '.*/eq-[0-9.]*')"
+  # Generate cabal.project
+  - rm -rf cabal.project cabal.project.local cabal.project.freeze
+  - touch cabal.project
+  - |
+    echo "packages: ${PKGDIR_eq}" >> cabal.project
+  - if [ $HCNUMVER -ge 80200 ] ; then echo 'package eq' >> 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 -- '^(eq)$' || 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 new-build -w ${HC} ${TEST} ${BENCH} all
-
-  # cabal check
-  - (cd eq-* && cabal check)
-
-  # haddock
-  - rm -rf ./dist-newstyle
-  - if $HADDOCK; then cabal new-haddock -w ${HC} ${TEST} ${BENCH} all; else echo "Skipping haddock generation";fi
+  - ${CABAL} v2-build $WITHCOMPILER ${TEST} ${BENCH} all
+  # cabal check...
+  - (cd ${PKGDIR_eq} && ${CABAL} -vnormal check)
+  # haddock...
+  - ${CABAL} v2-haddock $WITHCOMPILER --with-haddock $HADDOCK ${TEST} ${BENCH} all
 
-# REGENDATA ["-o",".travis.yml","--irc-channel=irc.freenode.org#haskell-lens","--no-no-tests-no-bench","--no-installed","cabal.project"]
+# REGENDATA ("0.10",["--output=.travis.yml","--config=cabal.haskell-ci","cabal.project"])
 # EOF
diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown
--- a/CHANGELOG.markdown
+++ b/CHANGELOG.markdown
@@ -1,3 +1,7 @@
+4.2.1 [2020.10.01]
+------------------
+* Allow building with GHC 9.0.
+
 4.2 [2018.04.24]
 ----------------
 * Make `lower`, `lower2`, and `lower3` in `Data.Eq.Type` poly-kinded.
diff --git a/eq.cabal b/eq.cabal
--- a/eq.cabal
+++ b/eq.cabal
@@ -1,8 +1,8 @@
 name:          eq
 category:      Type System
-version:       4.2
+version:       4.2.1
 license:       BSD3
-cabal-version: >= 1.6
+cabal-version: >= 1.10
 license-file:  LICENSE
 author:        Edward A. Kmett
 maintainer:    Edward A. Kmett <ekmett@gmail.com>
@@ -21,10 +21,12 @@
              , GHC == 7.10.3
              , GHC == 8.0.2
              , GHC == 8.2.2
-             , GHC == 8.4.2
+             , GHC == 8.4.4
+             , GHC == 8.6.5
+             , GHC == 8.8.3
+             , GHC == 8.10.1
 
 extra-source-files:
-  .ghci
   .gitignore
   .vim.custom
   .travis.yml
@@ -49,11 +51,12 @@
     Data.Eq.Type
 
   if impl(ghc >= 7.0)
-    extensions: TypeFamilies
+    default-extensions: TypeFamilies
     cpp-options: -DLANGUAGE_TypeFamilies
 
   if impl(ghc >= 8.2)
     exposed-modules: Data.Eq.Type.Hetero
 
   ghc-options: -Wall
+  default-language: Haskell2010
   hs-source-dirs: src
diff --git a/src/Data/Eq/Type.hs b/src/Data/Eq/Type.hs
--- a/src/Data/Eq/Type.hs
+++ b/src/Data/Eq/Type.hs
@@ -59,7 +59,7 @@
 #endif
   ) where
 
-import Prelude (Maybe(..), flip)
+import Prelude (Maybe(..))
 import Control.Category
 import Data.Semigroupoid
 import Data.Groupoid
@@ -90,17 +90,17 @@
 -- | Equality forms a category
 instance Category (:=) where
   id = Refl id
-  (.) = subst
+  bc . ab = subst bc ab
 
 instance Semigroupoid (:=) where
-  o = subst
+  bc `o` ab = subst bc ab
 
 instance Groupoid (:=) where
   inv = symm
 
 -- | Equality is transitive
 trans :: a := b -> b := c -> a := c
-trans = flip subst
+trans ab bc = subst bc ab
 
 newtype Symm p a b = Symm { unsymm :: p b a }
 -- | Equality is symmetric
diff --git a/src/Data/Eq/Type/Hetero.hs b/src/Data/Eq/Type/Hetero.hs
--- a/src/Data/Eq/Type/Hetero.hs
+++ b/src/Data/Eq/Type/Hetero.hs
@@ -15,7 +15,7 @@
 -- Stability   :  provisional
 -- Portability :  GHC
 --
--- Leibnizian equality à la "Data.Eq.Type", generalized to be heterogenous
+-- Leibnizian equality à la "Data.Eq.Type", generalized to be heterogeneous
 -- using higher-rank kinds.
 --
 -- This module is only exposed on GHC 8.2 and later.
@@ -71,7 +71,7 @@
 -- Leibnizian equality states that two things are equal if you can
 -- substitute one for the other in all contexts.
 newtype (a :: j) :== (b :: k)
-  = HRefl { hsubst :: forall (c :: forall (i :: Type). i -> Type). c a -> c b }
+  = HRefl { hsubst :: forall (c :: forall i. i -> Type). c a -> c b }
 type role (:==) nominal nominal
 
 -- | Equality is reflexive.
@@ -88,10 +88,10 @@
 coerce :: a :== b -> a -> b
 coerce f = uncoerce . hsubst f . Coerce
 
-newtype Push :: (forall (j :: Type) (k :: Type). j -> k -> Type)
-             -> forall (j :: Type). j -> forall (k :: Type). k -> Type where
-  Push :: forall (p :: forall (j :: Type) (k :: Type). j -> k -> Type)
-                 (j :: Type) (k :: Type) (a :: j) (b :: k).
+newtype Push :: (forall j k. j -> k -> Type)
+             -> forall j. j -> forall k. k -> Type where
+  Push :: forall (p :: forall j k. j -> k -> Type)
+                 j k (a :: j) (b :: k).
           { unpush :: p a b } -> Push p a b
 
 -- | Equality is compositional.
@@ -113,36 +113,32 @@
 trans :: a :== b -> b :== c -> a :== c
 trans = flip comp
 
-newtype Symm :: (forall (i1 :: Type). i1 -> forall (i2 :: Type). i2 -> Type)
-             -> forall (j :: Type). j
-             -> forall (k :: Type). k
-             -> Type where
-  Symm :: forall (p :: forall (i1 :: Type). i1 -> forall (i2 :: Type). i2 -> Type)
-                 (j :: Type) (k :: Type)
-                 (a :: j) (b :: k).
+newtype Symm :: (forall j. j -> forall k. k -> Type)
+             ->  forall j. j -> forall k. k -> Type where
+  Symm :: forall (p :: forall j. j -> forall k. k -> Type)
+                 j k (a :: j) (b :: k).
           { unsymm :: p b a } -> Symm p a b
 
 -- | Equality is symmetric.
 symm :: a :== b -> b :== a
 symm ab = unpush $ unsymm $ hsubst ab $ Symm $ Push refl
 
-newtype Lift :: forall (j :: Type) (r :: Type).
+newtype Lift :: forall j r.
                 (j -> r) -> j
-             -> forall (k :: Type). k
+             -> forall k. k
              -> Type where
-  Lift :: forall (j :: Type) (k :: Type) (r :: Type)
-                 (f :: j -> r) (a :: j) (b :: k).
+  Lift :: forall j r k (f :: j -> r) (a :: j) (b :: k).
           { unlift :: f a :== f (MassageKind j b) } -> Lift f a b
 
 -- | You can lift equality into any type constructor...
 lift :: a :== b -> f a :== f b
 lift f = unlift $ hsubst f $ Lift refl
 
-newtype Lift2 :: forall (j1 :: Type) (j2 :: Type) (r :: Type).
+newtype Lift2 :: forall j1 j2 r.
                  (j1 -> j2 -> r) -> j1 -> j2
-              -> forall (k :: Type). k
+              -> forall k. k
               -> Type where
-  Lift2 :: forall (j1 :: Type) (j2 :: Type) (k :: Type) (r :: Type)
+  Lift2 :: forall j1 j2 r k
                   (f :: j1 -> j2 -> r) (a :: j1) (b :: k) (c :: j2).
            { unlift2 :: f a c :== f (MassageKind j1 b) c } -> Lift2 f a c b
 
@@ -153,11 +149,11 @@
 lift2' :: a :== b -> c :== d -> f a c :== f b d
 lift2' ab cd = unpush $ lift2 ab `hsubst` Push (lift cd)
 
-newtype Lift3 :: forall (j1 :: Type) (j2 :: Type) (j3 :: Type) (r :: Type).
+newtype Lift3 :: forall j1 j2 j3 r.
                  (j1 -> j2 -> j3 -> r) -> j1 -> j2 -> j3
-              -> forall (k :: Type). k
+              -> forall k. k
               -> Type where
-  Lift3 :: forall (j1 :: Type) (j2 :: Type) (j3 :: Type) (k :: Type) (r :: Type)
+  Lift3 :: forall j1 j2 j3 r k
                   (f :: j1 -> j2 -> j3 -> r) (a :: j1) (b :: k) (c :: j2) (d :: j3).
            { unlift3 :: f a c d :== f (MassageKind j1 b) c d } -> Lift3 f a c d b
 
@@ -168,9 +164,10 @@
 lift3' ab cd ef = unpush $ unpush (lift3 ab `hsubst` Push (lift2 cd)) `hsubst` Push (lift ef)
 
 newtype Lower :: Type
-              -> forall (j :: Type). j
-              -> forall (k :: Type). k -> Type where
-  Lower :: forall (i :: Type) (j :: Type) (k :: Type) (a :: j) (b :: k).
+              -> forall j. j
+              -> forall k. k
+              -> Type where
+  Lower :: forall i j k (a :: j) (b :: k).
            { unlower :: Inj i a :== Inj i (MassageKind j b) } -> Lower i a b
 
 type family Inj (j :: Type) (a :: k) :: j where
@@ -178,45 +175,45 @@
   Inj _ _            = Any
 
 -- | Type constructors are injective, so you can lower equality through any type constructor.
-lower :: forall (j :: Type) (k :: Type) (f :: j -> k) (a :: j) (b :: j).
+lower :: forall j k (f :: j -> k) (a :: j) (b :: j).
          f a :== f b -> a :== b
 lower f = unlower $ hsubst f (Lower refl :: Lower j (f a) (f a))
 
 newtype Lower2 :: Type
-               -> forall (j :: Type). j
-               -> forall (k :: Type). k -> Type where
-  Lower2 :: forall (i :: Type) (j :: Type) (k :: Type) (a :: j) (b :: k).
+               -> forall j. j
+               -> forall k. k
+               -> Type where
+  Lower2 :: forall i j k (a :: j) (b :: k).
             { unlower2 :: Inj2 i a :== Inj2 i (MassageKind j b) } -> Lower2 i a b
 
 type family Inj2 (j :: Type) (a :: k) :: j where
   Inj2 j (f (a :: j) b) = a
   Inj2 _ _              = Any
 
-lower2 :: forall (i :: Type) (j :: Type) (k :: Type)
-                 (f :: i -> j -> k) (a :: i) (b :: i) (c :: j).
+lower2 :: forall i j k (f :: i -> j -> k) (a :: i) (b :: i) (c :: j).
           f a c :== f b c -> a :== b
 lower2 f = unlower2 $ hsubst f (Lower2 refl :: Lower2 i (f a c) (f a c))
 
 newtype Lower3 :: Type
-               -> forall (j :: Type). j
-               -> forall (k :: Type). k -> Type where
-  Lower3 :: forall (i :: Type) (j :: Type) (k :: Type) (a :: j) (b :: k).
+               -> forall j. j
+               -> forall k. k
+               -> Type where
+  Lower3 :: forall i j k (a :: j) (b :: k).
             { unlower3 :: Inj3 i a :== Inj3 i (MassageKind j b) } -> Lower3 i a b
 
 type family Inj3 (j :: Type) (a :: k) :: j where
   Inj3 j (f (a :: j) b c) = a
   Inj3 _ _                = Any
 
-lower3 :: forall (h :: Type) (i :: Type) (j :: Type) (k :: Type)
-                 (f :: h -> i -> j -> k) (a :: h) (b :: h) (c :: i) (d :: j).
+lower3 :: forall h i j k (f :: h -> i -> j -> k) (a :: h) (b :: h) (c :: i) (d :: j).
           f a c d :== f b c d -> a :== b
 lower3 f = unlower3 $ hsubst f (Lower3 refl :: Lower3 h (f a c d) (f a c d))
 
-newtype Flay :: forall (j :: Type).
+newtype Flay :: forall j.
                 (j -> j -> Type) -> j
-             -> forall (k :: Type). k -> Type where
-  Flay :: forall (j :: Type) (k :: Type)
-                 (p :: j -> j -> Type) (a :: j) (b :: k).
+             -> forall k. k
+             -> Type where
+  Flay :: forall j k (p :: j -> j -> Type) (a :: j) (b :: k).
           { unflay :: p a (MassageKind j b) } -> Flay p a b
 
 -- | Convert an appropriately kinded heterogeneous Leibnizian equality into