diff --git a/.gitignore b/.gitignore
--- a/.gitignore
+++ b/.gitignore
@@ -1,4 +1,5 @@
 dist
+dist-newstyle
 docs
 wiki
 TAGS
diff --git a/.travis.yml b/.travis.yml
--- a/.travis.yml
+++ b/.travis.yml
@@ -60,9 +60,9 @@
     - 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.1"
-      env: GHCHEAD=true
-      addons: {apt: {packages: [*apt_packages,cabal-install-head,ghc-8.4.1], 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]}}
@@ -70,7 +70,6 @@
   allow_failures:
     - compiler: "ghc-7.0.4"
     - compiler: "ghc-7.2.2"
-    - compiler: "ghc-8.4.1"
     - compiler: "ghc-head"
 
 before_install:
diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown
--- a/CHANGELOG.markdown
+++ b/CHANGELOG.markdown
@@ -1,3 +1,10 @@
+4.2 [2018.04.24]
+----------------
+* Make `lower`, `lower2`, and `lower3` in `Data.Eq.Type` poly-kinded.
+* Introduce the `Data.Eq.Type.Hetero` module, which exposes `(:==)`, a
+  heterogeneously kinded version of `(:=)`. This module is only available
+  on GHC 8.2 and later.
+
 4.1
 ---
 * Add `TestEquality` and `TestCoercion` instances for `(:=)`.
diff --git a/eq.cabal b/eq.cabal
--- a/eq.cabal
+++ b/eq.cabal
@@ -1,6 +1,6 @@
 name:          eq
 category:      Type System
-version:       4.1
+version:       4.2
 license:       BSD3
 cabal-version: >= 1.6
 license-file:  LICENSE
@@ -21,7 +21,7 @@
              , GHC == 7.10.3
              , GHC == 8.0.2
              , GHC == 8.2.2
-             , GHC == 8.4.1
+             , GHC == 8.4.2
 
 extra-source-files:
   .ghci
@@ -51,6 +51,9 @@
   if impl(ghc >= 7.0)
     extensions: TypeFamilies
     cpp-options: -DLANGUAGE_TypeFamilies
+
+  if impl(ghc >= 8.2)
+    exposed-modules: Data.Eq.Type.Hetero
 
   ghc-options: -Wall
   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
@@ -1,5 +1,6 @@
 {-# LANGUAGE CPP, Rank2Types, TypeOperators #-}
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 706
+#define LANGUAGE_PolyKinds
 {-# LANGUAGE PolyKinds #-}
 #endif
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
@@ -127,29 +128,36 @@
 lift3' ab cd ef = lift3 ab `subst` lift2 cd `subst` lift ef
 
 #ifdef LANGUAGE_TypeFamilies
-type family Inj (f :: *) :: *
-type instance Inj (f a) = a
-newtype Lower a b = Lower { unlower :: Inj a := Inj b }
--- | Type constructors are injective, so you can lower equality through any type constructor
-lower :: forall (a :: *) (b :: *) (f :: * -> *). f a := f b -> a := b
-lower eq = unlower (subst eq (Lower refl :: Lower (f a) (f a)))
+# ifdef LANGUAGE_PolyKinds
+type family Inj  (f :: j -> k)           (a :: k) :: j
+type family Inj2 (f :: i -> j -> k)      (a :: k) :: i
+type family Inj3 (f :: h -> i -> j -> k) (a :: k) :: h
+# else
+type family Inj  (f :: * -> *)           (a :: *) :: *
+type family Inj2 (f :: * -> * -> *)      (a :: *) :: *
+type family Inj3 (f :: * -> * -> * -> *) (a :: *) :: *
+# endif
 
-type family Inj2 (f :: *) :: *
-type instance Inj2 (f a (b :: *)) = a
-newtype Lower2 a b = Lower2 { unlower2 :: Inj2 a := Inj2 b }
--- | ... in any position
-lower2 :: forall (a :: *) (b :: *) (c :: *) (f :: * -> * -> *).
-    f a c := f b c -> a := b
-lower2 eq = unlower2 (subst eq (Lower2 refl :: Lower2 (f a c) (f a c)))
+type instance Inj  f (f a)     = a
+type instance Inj2 f (f a b)   = a
+type instance Inj3 f (f a b c) = a
 
-type family Inj3 (f :: *) :: *
-type instance Inj3 (f a (b :: *) (c :: *)) = a
-newtype Lower3 a b = Lower3 { unlower3 :: Inj3 a := Inj3 b }
--- | But unfortunately these definitions aren't polykinded. Everything is just a star.
-lower3 :: forall (a :: *) (b :: *) (c :: *) (d :: *) (f :: * -> * -> * -> *).
-    f a c d := f b c d -> a := b
-lower3 eq = unlower3 (subst eq (Lower3 refl :: Lower3 (f a c d) (f a c d)))
+newtype Lower  f a b = Lower  { unlower  :: Inj  f a := Inj  f b }
+newtype Lower2 f a b = Lower2 { unlower2 :: Inj2 f a := Inj2 f b }
+newtype Lower3 f a b = Lower3 { unlower3 :: Inj3 f a := Inj3 f b }
 
+-- | Type constructors are injective, so you can lower equality through any
+-- type constructor ...
+lower :: forall a b f. f a := f b -> a := b
+lower eq = unlower (subst eq (Lower refl :: Lower f (f a) (f a)))
+
+-- | ... in any position ...
+lower2 :: forall a b c f. f a c := f b c -> a := b
+lower2 eq = unlower2 (subst eq (Lower2 refl :: Lower2 f (f a c) (f a c)))
+
+-- | ... these definitions are poly-kinded on GHC 7.6 and up.
+lower3 :: forall a b c d f. f a c d := f b c d -> a := b
+lower3 eq = unlower3 (subst eq (Lower3 refl :: Lower3 f (f a c d) (f a c d)))
 #endif
 
 #ifdef HAS_DATA_TYPE_EQUALITY
diff --git a/src/Data/Eq/Type/Hetero.hs b/src/Data/Eq/Type/Hetero.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Eq/Type/Hetero.hs
@@ -0,0 +1,251 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE RoleAnnotations #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Eq.Type.Hetero
+-- Copyright   :  (C) 2011-2014 Edward Kmett, 2018 Ryan Scott
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  provisional
+-- Portability :  GHC
+--
+-- Leibnizian equality à la "Data.Eq.Type", generalized to be heterogenous
+-- using higher-rank kinds.
+--
+-- This module is only exposed on GHC 8.2 and later.
+----------------------------------------------------------------------------
+module Data.Eq.Type.Hetero
+  (
+  -- * Heterogeneous Leibnizian equality
+    (:==)(..)
+  -- * Equality as an equivalence relation
+  , refl
+  , trans
+  , symm
+  , coerce
+  -- * Lifting equality
+  , lift
+  , lift2, lift2'
+  , lift3, lift3'
+  -- * Lowering equality
+  , lower
+  , lower2
+  , lower3
+  -- * 'ET.:=' equivalence
+  -- | 'ET.:=' is equivalent in power
+  , toHomogeneous
+  , fromHomogeneous
+  -- * 'Eq.:~:' equivalence
+  -- | 'Eq.:~:' is equivalent in power
+  , fromLeibniz
+  , toLeibniz
+  -- * 'Eq.:~~:' equivalence
+  -- | 'Eq.:~~:' is equivalent in power
+  , heteroFromLeibniz
+  , heteroToLeibniz
+  -- * 'Co.Coercion' conversion
+  -- | Leibnizian equality can be converted to representational equality
+  , reprLeibniz
+  ) where
+
+import           Control.Category
+import           Data.Groupoid
+import           Data.Semigroupoid
+import qualified Data.Type.Coercion as Co
+import qualified Data.Type.Equality as Eq
+import           Data.Kind
+import qualified Data.Eq.Type as ET
+import           GHC.Exts (Any)
+import           Prelude hiding (id, (.))
+
+infixl 4 :==
+
+-- | Heterogeneous Leibnizian equality.
+--
+-- 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 }
+type role (:==) nominal nominal
+
+-- | Equality is reflexive.
+refl :: a :== a
+refl = HRefl id
+
+newtype Coerce (a :: k) = Coerce { uncoerce :: MassageKind Type a }
+
+type family MassageKind (j :: Type) (a :: k) :: j where
+  MassageKind j (a :: j) = a
+  MassageKind _ _        = Any
+
+-- | If two things are equal, you can convert one to the other.
+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).
+          { unpush :: p a b } -> Push p a b
+
+-- | Equality is compositional.
+comp :: b :== c -> a :== b -> a :== c
+comp f = unpush . hsubst f . Push
+
+-- | Equality forms a category.
+instance Category (:==) where
+  id  = refl
+  (.) = comp
+
+instance Semigroupoid (:==) where
+  o = comp
+
+instance Groupoid (:==) where
+  inv = symm
+
+-- | Equality is transitive.
+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).
+          { 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).
+                (j -> r) -> j
+             -> forall (k :: Type). k
+             -> Type where
+  Lift :: forall (j :: Type) (k :: Type) (r :: Type)
+                 (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).
+                 (j1 -> j2 -> r) -> j1 -> j2
+              -> forall (k :: Type). k
+              -> Type where
+  Lift2 :: forall (j1 :: Type) (j2 :: Type) (k :: Type) (r :: Type)
+                  (f :: j1 -> j2 -> r) (a :: j1) (b :: k) (c :: j2).
+           { unlift2 :: f a c :== f (MassageKind j1 b) c } -> Lift2 f a c b
+
+-- | ... in any position.
+lift2 :: a :== b -> f a c :== f b c
+lift2 f = unlift2 $ hsubst f $ Lift2 refl
+
+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).
+                 (j1 -> j2 -> j3 -> r) -> j1 -> j2 -> j3
+              -> forall (k :: Type). k
+              -> Type where
+  Lift3 :: forall (j1 :: Type) (j2 :: Type) (j3 :: Type) (k :: Type) (r :: Type)
+                  (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
+
+lift3 :: a :== b -> f a c d :== f b c d
+lift3 f = unlift3 $ hsubst f $ Lift3 refl
+
+lift3' :: a :== b -> c :== d -> e :== f -> g a c e :== g b d f
+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).
+           { unlower :: Inj i a :== Inj i (MassageKind j b) } -> Lower i a b
+
+type family Inj (j :: Type) (a :: k) :: j where
+  Inj j (f (a :: j)) = a
+  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).
+         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).
+            { 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).
+          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).
+            { 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).
+          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).
+                (j -> j -> Type) -> j
+             -> forall (k :: Type). k -> Type where
+  Flay :: forall (j :: Type) (k :: Type)
+                 (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
+-- a homogeneous Leibnizian equality '(ET.:=)'.
+toHomogeneous :: a :== b -> a ET.:= b
+toHomogeneous f = unflay $ hsubst f $ Flay ET.refl
+
+-- | Convert a homogeneous Leibnizian equality '(ET.:=)' to an appropriately kinded
+-- heterogeneous Leibizian equality.
+fromHomogeneous :: a ET.:= b -> a :== b
+fromHomogeneous f = ET.subst f refl
+
+fromLeibniz :: forall a b. a :== b -> a Eq.:~: b
+fromLeibniz f = unflay $ hsubst f $ Flay Eq.Refl
+
+toLeibniz :: a Eq.:~: b -> a :== b
+toLeibniz Eq.Refl = refl
+
+heteroFromLeibniz :: a :== b -> a Eq.:~~: b
+heteroFromLeibniz f = unpush $ hsubst f $ Push $ Eq.HRefl
+
+heteroToLeibniz :: a Eq.:~~: b -> a :== b
+heteroToLeibniz Eq.HRefl = refl
+
+instance Eq.TestEquality ((:==) a) where
+  testEquality fa fb = Just (fromLeibniz (trans (symm fa) fb))
+
+reprLeibniz :: a :== b -> Co.Coercion a b
+reprLeibniz f = unflay $ hsubst f $ Flay Co.Coercion
+
+instance Co.TestCoercion ((:==) a) where
+  testCoercion fa fb = Just (reprLeibniz (trans (symm fa) fb))