diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,13 @@
+# Version 0.5
+
+* COMPILER ASSISTED BREAKING CHANGE: Fixed `TypeApplications` for `zip1` so
+  that @c@ comes first.
+
+* Documentation improvements.
+
+* Fixed compilation with GHC 9.8.
+
+
 # Version 0.4
 
 * COMPILER ASSISTED BREAKING CHANGE: Fixed `TypeApplications` for `flay1` so
diff --git a/Setup.hs b/Setup.hs
deleted file mode 100644
--- a/Setup.hs
+++ /dev/null
@@ -1,4 +0,0 @@
-#! /usr/bin/env nix-shell
-#! nix-shell ./shell.nix -i runghc
-import Distribution.Simple
-main = defaultMain
diff --git a/flay.cabal b/flay.cabal
--- a/flay.cabal
+++ b/flay.cabal
@@ -1,18 +1,16 @@
+cabal-version: 1.18
 name: flay
-version: 0.4
+version: 0.5
 author: Renzo Carbonara
 maintainer: renλren!zone
-copyright: Renzo Carbonara 2017-2018
+copyright: Renzo Carbonara 2017
 license: BSD3
 license-file: LICENSE.txt
 extra-source-files: README.md CHANGELOG.md
 category: Data, Generics
 build-type: Simple
-cabal-version: >=1.18
-synopsis: Work generically on your datatype without knowing its shape nor its contents.
-description:
-  Work generically on your datatype without knowing its shape nor its contents using
-  a principlied approach.
+synopsis: Generic programming for higher-kinded types.
+description: Generic programming for higher-kinded types.
 homepage: https://github.com/k0001/flay
 bug-reports: https://github.com/k0001/flay/issues
 source-repository head
@@ -36,7 +34,7 @@
   hs-source-dirs: tests
   main-is: Main.hs
   build-depends:
-    base,
+    base >=4.9 && <5.0,
     flay,
     tasty,
     tasty-quickcheck,
diff --git a/src/Flay.hs b/src/Flay.hs
--- a/src/Flay.hs
+++ b/src/Flay.hs
@@ -7,6 +7,7 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
@@ -19,7 +20,7 @@
 -- unqualified, as necessary:
 --
 -- @
--- import Flay (Flay, Flayable(flay), Flayable1(flay1))
+-- import Flay (Flay, Flayable, flay, Flayable1, flay1)
 -- @
 --
 -- The rest of the names, qualified:
@@ -27,6 +28,10 @@
 -- @
 -- import qualified Flay
 -- @
+--
+-- __IMPORTANT__: Always check the
+-- [changelog](https://hackage.haskell.org/package/flay/changelog) to learn
+-- more about changes between different versions.
 module Flay
  ( Flay
  -- * Flayable
@@ -71,10 +76,11 @@
 import Control.Monad.Trans.Class (lift)
 import Control.Monad.Trans.State (StateT(StateT), runStateT)
 import Control.Monad.Trans.Maybe (MaybeT(MaybeT), runMaybeT)
-import Data.Constraint (Constraint, Dict(Dict))
+import Data.Constraint (Dict(Dict))
 import Data.Dynamic (Dynamic, toDyn, fromDynamic)
 import Data.Functor.Product (Product(Pair))
 import Data.Functor.Const (Const(Const, getConst))
+import Data.Kind
 import Data.Typeable (Typeable)
 import qualified GHC.Generics as G
 import Prelude hiding (zip)
@@ -119,6 +125,7 @@
 -- Consider the following types and values:
 --
 -- @
+-- -- | Foo is a higher-kinded type parametrized over some @f :: 'Type' -> 'Type'@.
 -- data Foo f = Foo (f 'Int') (f 'Bool')
 --
 -- deriving instance ('Show' (f 'Int'), 'Show' (f 'Bool')) => 'Show' (Foo f)
@@ -354,9 +361,9 @@
 -- about the targets themselves beyond the fact that they satisfy a particular
 -- constraint.
 --
-type Flay (c :: k -> Constraint) s t (f :: k -> *) (g :: k -> *)
+type Flay (c :: k -> Constraint) s t (f :: k -> Type) (g :: k -> Type)
   = forall m. Applicative m
-       => (forall (a :: k). Dict (c a) -> f a -> m (g a)) -> s -> m t
+       => (forall a. Dict (c a) -> f a -> m (g a)) -> s -> m t
 
 --------------------------------------------------------------------------------
 
@@ -401,14 +408,14 @@
 -- @
 --
 -- Notice that 'flay' can be defined in terms of 'flay1' as well.
-class Flayable (c :: k -> Constraint) s t (f :: k -> *) (g :: k -> *)
+class Flayable (c :: k -> Constraint) s t (f :: k -> Type) (g :: k -> Type)
   | s -> f, t -> g, s g -> t, t f -> s where
   flay :: Flay c s t f g
   default flay :: GFlay c s t f g => Flay c s t f g
   flay = gflay
   {-# INLINE flay #-}
 
--- | All datatypes parametrized over some type constructor @f :: k -> *@ that
+-- | All datatypes parametrized over some type constructor @f :: k -> 'Type'@ that
 -- have a 'G.Generic' instance get a 'Flayable' instance for free. For example:
 --
 -- @
@@ -435,25 +442,25 @@
 --
 -- @
 -- 'Flayable1' c r
---    ==  forall (f :: k -> *) (g :: k -> *).
+--    ==  forall (f :: k -> 'Type') (g :: k -> 'Type').
 --           'Flayable' c (r f) (r g) f g
 -- @
 
 -- Implementors note: Currently, 'Flayable1' is uses some of the skolem trickery
 -- described in detail in "Data.Constraint.Forall", specialized to 'Flayable'.
-type family Flayable1 (c :: k -> Constraint) (r :: (k -> *) -> *) :: Constraint where
+type family Flayable1 (c :: k -> Constraint) (r :: (k -> Type) -> Type) :: Constraint where
   Flayable1 c r = Flayable1_ c r
 
 -- | This inner 'Flayable1_' class prevents the skolem from leaking to the user.
 class Flayable1K c r (Skolem (Flayable1K c r))
-  => Flayable1_ (c :: k -> Constraint) (r :: (k -> *) -> *)
+  => Flayable1_ (c :: k -> Constraint) (r :: (k -> Type) -> Type)
 instance Flayable1K c r (Skolem (Flayable1K c r))
   => Flayable1_ c r
 
 -- | Like @Flayable c (r F) (r G) F G@, but with a superfluous trailing @x@
 -- to match the kind expected by 'Skolem'.
 class Flayable c (r F) (r G) F G
-  => Flayable1K (c :: k -> Constraint) (r :: (k -> *) -> *) (x :: *)
+  => Flayable1K (c :: k -> Constraint) (r :: (k -> Type) -> Type) (x :: Type)
 instance Flayable c (r F) (r G) F G
   => Flayable1K c r x
 
@@ -477,7 +484,7 @@
 -- This can be used as the @c@ parameter to 'Flay' or 'Flayable' in case you are
 -- not interested in observing the values inside @f@.
 class Trivial (a :: k)
-instance Trivial (a :: k)
+instance Trivial a
 
 -- | Given a 'Flay' for any constraint @c@ obtain a 'Flay' for a 'Trivial'
 -- constraint.
@@ -538,14 +545,14 @@
 --------------------------------------------------------------------------------
 
 -- | Convenient 'Constraint' for satisfying the requirements of 'gflay'.
-type GFlay (c :: k -> Constraint) s t (f :: k -> *) (g :: k -> *)
+type GFlay (c :: k -> Constraint) s t (f :: k -> Type) (g :: k -> Type)
   = (GFlay' c (G.Rep s) (G.Rep t) f g, G.Generic s, G.Generic t)
 
-gflay :: GFlay c s t f g => Flay (c :: k -> Constraint) s t (f :: k -> *) (g :: k -> *)
+gflay :: GFlay c s t f g => Flay (c :: k -> Constraint) s t (f :: k -> Type) (g :: k -> Type)
 gflay = \h s -> G.to <$> gflay' h (G.from s)
 {-# INLINE gflay #-}
 
-class GFlay' (c :: k -> Constraint) s t (f :: k -> *) (g :: k -> *) where
+class GFlay' (c :: k -> Constraint) s t (f :: k -> Type) (g :: k -> Type) where
   gflay' :: Flay c (s p) (t p) f g
 
 instance GFlay' c G.V1 G.V1 f g where
@@ -568,11 +575,11 @@
         arising from a use of ‘Flay.$dmflay1’
       Matching instances:
         instance [safe]
-          forall k1 k2 (c :: k2 -> Constraint) (a :: k2) r (f :: k2 -> *) (g :: k2 -> *).
+          forall k1 k2 (c :: k2 -> Constraint) (a :: k2) r (f :: k2 -> 'Type') (g :: k2 -> 'Type').
           c a =>
           Flay.GFlay' c (G.K1 r (f a)) (G.K1 r (g a)) f g
         instance [overlappable] [safe]
-          forall k1 k2 (c :: k2 -> Constraint) r a (f :: k2 -> *) (g :: k2 -> *).
+          forall k1 k2 (c :: k2 -> Constraint) r a (f :: k2 -> 'Type') (g :: k2 -> 'Type').
           Flay.GFlay' c (G.K1 r a) (G.K1 r a) f g
 
 instance {-# OVERLAPPABLE #-} GFlay' c (G.K1 r a) (G.K1 r a) f g where
@@ -657,7 +664,7 @@
   {-# INLINE terminal #-}
 
 ---
-class GTerminal (f :: * -> *) where
+class GTerminal (f :: Type -> Type) where
   gterminal :: f p
 
 instance GTerminal G.U1 where
@@ -689,23 +696,24 @@
 -- > let foo2 = 'Foo' ('Just' 1) 'Nothing'
 -- >   :: 'Foo' 'Maybe'
 --
--- > 'zip1' (\('Dict' :: 'Dict' ('Trivial' x)) a b -> 'Data.Functor.Product.Pair' a b) foo1 foo2
--- >   :: 'Foo' ('Data.Functor.Product.Product' 'Data.Functor.Identity.Identity' 'Maybe')
--- 'Foo' ('Data.Functor.Product.Pair' ('Data.Functor.Identity.Identity' 0) ('Just' 1)) ('Data.Functor.Product.Pair' ('Data.Functor.Identity.Identity' 'False') 'Nothing')
+-- > 'zip1' (\('Dict' :: 'Dict' ('Trivial' x)) a b -> 'pure' ('Data.Functor.Product.Pair' a b)) foo1 foo2
+-- >   :: 'Applicative' m => m ('Maybe' ('Foo' ('Data.Functor.Product.Product' 'Data.Functor.Identity.Identity' 'Maybe')))
+-- 'Just' ('Foo' ('Data.Functor.Product.Pair' ('Data.Functor.Identity.Identity' 0) ('Just' 1)) ('Data.Functor.Product.Pair' ('Data.Functor.Identity.Identity' 'False') 'Nothing'))
 --
 -- > 'zip1' (\('Dict' :: 'Dict' ('Show' x)) ('Data.Functor.Identity.Identity' a) yb -> case yb of
--- >           'Nothing' -> 'Const' ('show' a)
--- >           'Just' b  -> 'Const' ('show' (a, b)) )
+-- >           'Nothing' -> 'pure' ('Const' ('show' a))
+-- >           'Just' b  -> 'pure' ('Const' ('show' (a, b))) )
 -- >      foo1 foo2
--- >   :: Foo ('Const' 'String')
--- Foo ('Const' \"(0,1)\") ('Const' \"False\")
+-- >   :: 'Applicative' m => m ('Maybe' (Foo ('Const' 'String')))
+-- 'Just' (Foo ('Const' \"(0,1)\") ('Const' \"False\"))
 -- @
 --
 -- Returns 'Nothing' in case the indivual target types do not match.
 --
 -- Note: 'zip1' is safer but less general than 'unsafeZip'.
 zip1
-  :: (Monad m, Typeable f, Flayable1 c s, Flayable1 Typeable s)
+  :: forall c s f g h m
+  .  (Monad m, Typeable f, Flayable1 c s, Flayable1 Typeable s)
   => (forall x. Dict (c x) -> f x -> g x -> m (h x))
   -> s f
   -> s g
@@ -721,7 +729,9 @@
 --
 -- Note: 'zip' is safer but less general than 'unsafeZip'.
 zip
-  :: ( Monad m, Typeable f
+  :: forall c s1 s2 t1 t2 t3 f g h m
+  .  ( Monad m
+     , Typeable f
      , Flayable Typeable s1 t1 f (Const ())
      , Flayable Typeable s2 t2 g (Product f g)
      , Flayable c t2 t3 (Product f g) h )
@@ -759,9 +769,10 @@
    f1 :: Dict (Typeable a) -> f a -> [Dynamic]
    f1 = \Dict !fa -> [toDyn fa :: Dynamic]
    f2 :: Dict (Typeable a) -> g a -> StateT [Dynamic] (MaybeT m) (Product f g a)
-   f2 = \Dict !ga -> StateT $ \(x:xs) -> do
-      !(fa :: f a) <- MaybeT (pure (fromDynamic x))
-      pure (Pair fa ga, xs)
+   f2 = \Dict !ga -> StateT $ \case
+            (x:xs) -> do !(fa :: f a) <- MaybeT (pure (fromDynamic x))
+                         pure (Pair fa ga, xs)
+            [] -> error "Flay.unsafeZip"
    f3 :: Dict (c a) -> Product f g a -> m (h a)
    f3 = \Dict (Pair fa ga) -> pair Dict fa ga
 
@@ -771,7 +782,7 @@
 -- | Wrapper allowing a 'G.Generic' non 'Flayable' type to become 'Flayable'.
 --
 -- Most datatypes that can have useful 'Flayable' instances are often
--- parametrized by a type constructor @f :: k -> *@, and have all or some of
+-- parametrized by a type constructor @f :: k -> 'Type'@, and have all or some of
 -- their fields wrapped in said @f@, like so:
 --
 -- @
@@ -895,8 +906,8 @@
 -- 'dump'.
 type GPump s f = (G.Generic s, GPump' (G.Rep s) f)
 
-class GPump' (s :: k -> *) (f :: * -> *) where
-  type GPumped s f :: k -> *
+class GPump' (s :: k -> Type) (f :: Type -> Type) where
+  type GPumped s f :: k -> Type
   gpump :: (forall a. a -> f a) -> s p -> GPumped s f p
   gdump :: Applicative m => (forall a. f a -> m a) -> GPumped s f p -> m (s p)
 
@@ -1001,7 +1012,7 @@
 -- This 'Constraint' ensures that @c@ is satsfieds by all of the 'G.K1' types
 -- appearing in @s@, which is expected to be one of the various 'G.Generic'
 -- representation types.
-type family GFields (c :: kc -> Constraint) (s :: ks -> *) :: Constraint where
+type family GFields (c :: kc -> Constraint) (s :: ks -> Type) :: Constraint where
   GFields _ G.V1 = ()
   GFields _ G.U1 = ()
   GFields c (G.K1 _ a) = (c a)
@@ -1033,16 +1044,16 @@
 -- where the number of types contained in @f@ is larger. That is:
 --
 -- @
--- forall (c :: * -> 'Constraint').
+-- forall (c :: 'Type' -> 'Constraint').
 --    'FieldsF' c 'Foo'  ==  (c 'Int', c 'Bool')
 -- @
 --
--- Notice that 'FieldsF' only works with types of kind @(k -> *) -> *@ such as
+-- Notice that 'FieldsF' only works with types of kind @(k -> 'Type') -> 'Type'@ such as
 -- 'Foo'. That is, types that are parametrized by a type constructor.
 
 -- This type-family vs. class dance is so that 'F' doesn't show up in the public
 -- API (that is, in 'FieldsF').
-type family FieldsF (c :: k -> Constraint) (r :: (k -> *) -> *) :: Constraint where
+type family FieldsF (c :: k -> Constraint) (r :: (k -> Type) -> Type) :: Constraint where
   FieldsF c r = FieldsF_ c r
 class GFieldsF c (G.Rep (r F)) F => FieldsF_ c r
 instance GFieldsF c (G.Rep (r F)) F => FieldsF_ c r
@@ -1053,7 +1064,7 @@
 --
 -- This 'Constraint' ensures that @c@ is satsfieds by all of the 'G.K1' types
 -- appearing in @s@ that are wrapped by @f@.
-type family GFieldsF (c :: k -> Constraint) (s :: ks -> *) (f :: k -> *) :: Constraint where
+type family GFieldsF (c :: k -> Constraint) (s :: ks -> Type) (f :: k -> Type) :: Constraint where
   GFieldsF _ G.V1 _ = ()
   GFieldsF _ G.U1 _ = ()
   GFieldsF c (G.K1 _ (f a)) f = (c a)
@@ -1062,9 +1073,9 @@
   GFieldsF c (sl G.:*: sr) f = (GFieldsF c sl f, GFieldsF c sr f)
   GFieldsF c (sl G.:+: sr) f = (GFieldsF c sl f, GFieldsF c sr f)
 
--- | INTERNAL. DO NOT EXPORT. Used as a placeholder of kind @forall k. k -> *@.
+-- | INTERNAL. DO NOT EXPORT. Used as a placeholder of kind @forall k. k -> 'Type'@.
 data F (a :: k)
 
--- | INTERNAL. DO NOT EXPORT. Used as a placeholder of kind @forall k. k -> *@.
+-- | INTERNAL. DO NOT EXPORT. Used as a placeholder of kind @forall k. k -> 'Type'@.
 data G (a :: k)
 
diff --git a/tests/Main.hs b/tests/Main.hs
--- a/tests/Main.hs
+++ b/tests/Main.hs
@@ -16,6 +16,7 @@
 import Control.Monad.Trans.State.Strict (State, state, evalState)
 import Data.Functor.Const (Const(Const))
 import Data.Functor.Identity (Identity(Identity), runIdentity)
+import Data.Kind
 import GHC.Exts (Constraint)
 import GHC.Generics (Generic)
 import qualified GHC.Generics as G
@@ -32,8 +33,8 @@
 -- | Just making sure TypeApplications works as expected.
 _test_flay_TypeApplications
   :: Flayable Trivial s t f g
-  => Flay Trivial s t (f :: k -> *) (g :: k -> *)
-_test_flay_TypeApplications = flay @Trivial
+  => Flay Trivial s t (f :: k -> Type) (g :: k -> Type)
+_test_flay_TypeApplications = flay @_ @Trivial
 
 -- | Just making sure TypeApplications works as expected.
 --
@@ -41,7 +42,7 @@
 -- I'm not sure how to prevent it.
 _test_flay1_TypeApplications
   :: Flayable1 Trivial r
-  => Flay Trivial (r f) (r g) (f :: k -> *) (g :: k -> *)
+  => Flay Trivial (r f) (r g) (f :: k -> Type) (g :: k -> Type)
 _test_flay1_TypeApplications = flay1 @Trivial
 
 --------------------------------------------------------------------------------
@@ -137,13 +138,13 @@
 tt = Tasty.testGroup "main"
   [ QC.testProperty "Flayable: Foo: identity law" $
       QC.forAll QC.arbitrary $ \(foo :: Foo Maybe) ->
-         Identity foo === flay @Trivial (const pure) foo
+         Identity foo === flay @_ @Trivial (const pure) foo
   , QC.testProperty "Flayable: Bar: identity law" $
       QC.forAll QC.arbitrary $ \(bar :: Bar Maybe) ->
-         Identity bar === flay @Trivial (const pure) bar
+         Identity bar === flay @_ @Trivial (const pure) bar
   , QC.testProperty "Flayable: Qux: identity law" $
       QC.forAll QC.arbitrary $ \(qux :: Qux Maybe) ->
-         Identity qux === flay @Trivial (const pure) qux
+         Identity qux === flay @_ @Trivial (const pure) qux
   , QC.testProperty "collectShow: Foo: flayFoo" $
       QC.forAll QC.arbitrary $ \foo@(Foo (Identity a) (Identity b)) ->
          [show a, show b] === collectShow' flayFoo foo