diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,6 +1,6 @@
 MIT License
 
-Copyright (c) 2018-2020 Andrey Mokhov
+Copyright (c) 2018-2021 Andrey Mokhov
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
 of this software and associated documentation files (the "Software"), to deal
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,6 +1,6 @@
 # Selective applicative functors
 
-[![Hackage version](https://img.shields.io/hackage/v/selective.svg?label=Hackage)](https://hackage.haskell.org/package/selective) [![Linux & OS X status](https://img.shields.io/travis/snowleopard/selective/master.svg?label=Linux%20%26%20OS%20X)](https://travis-ci.org/snowleopard/selective) [![Windows status](https://img.shields.io/appveyor/ci/snowleopard/selective/master.svg?label=Windows)](https://ci.appveyor.com/project/snowleopard/selective)
+[![Hackage version](https://img.shields.io/hackage/v/selective.svg?label=Hackage)](https://hackage.haskell.org/package/selective) [![Build status](https://img.shields.io/github/workflow/status/snowleopard/selective/ci.svg)](https://github.com/snowleopard/selective/actions)
 
 This is a library for *selective applicative functors*, or just *selective functors*
 for short, an abstraction between applicative functors and monads, introduced in
diff --git a/examples/Build.hs b/examples/Build.hs
--- a/examples/Build.hs
+++ b/examples/Build.hs
@@ -14,11 +14,11 @@
 -- | Selective build scripts.
 type Script k v = k -> Maybe (Task k v)
 
--- | Build dependencies with over-appriximation.
+-- | Build dependencies with over-approximation.
 dependenciesOver :: Task k v -> [k]
 dependenciesOver task = getOver $ run task (\k -> Over [k])
 
--- | Build dependencies with under-appriximation.
+-- | Build dependencies with under-approximation.
 dependenciesUnder :: Task k v -> [k]
 dependenciesUnder task = getUnder $ run task (\k -> Under [k])
 
@@ -93,7 +93,7 @@
 data Fetch k v a = Fetch k (v -> a) deriving Functor
 
 instance Eq k => Eq (Fetch k v ()) where
-    Fetch x _ == Fetch y _ = (x == y)
+    Fetch x _ == Fetch y _ = x == y
 
 instance Show k => Show (Fetch k v a) where
     show (Fetch k _) = "Fetch " ++ show k
diff --git a/examples/Parser.hs b/examples/Parser.hs
--- a/examples/Parser.hs
+++ b/examples/Parser.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE ConstraintKinds, DeriveFunctor, GADTs, RankNTypes #-}
+{-# LANGUAGE ConstraintKinds, GADTs, LambdaCase, RankNTypes #-}
 module Parser where
 
 import Control.Applicative
@@ -18,7 +18,7 @@
     (<*>)  = ap
 
 instance Alternative Parser where
-    empty   = Parser $ \_ -> []
+    empty   = Parser (const [])
     p <|> q = Parser $ \s -> parse p s ++ parse q s
 
 instance Selective Parser where
@@ -32,10 +32,10 @@
     zero :: f a
 
 instance MonadZero Parser where
-    zero = Parser (\_ -> [])
+    zero = Parser (const [])
 
 item :: Parser Char
-item = Parser $ \s -> case s of
+item = Parser $ \case
     ""    -> []
     (c:cs) -> [(c,cs)]
 
diff --git a/examples/Processor.hs b/examples/Processor.hs
--- a/examples/Processor.hs
+++ b/examples/Processor.hs
@@ -100,11 +100,10 @@
 toState :: MonadState State m => RW a -> m a
 toState = \case
     (Read k t) -> do
-        v <- case k of
-                   Reg  r    -> (Map.! r   ) <$> S.gets registers
-                   Cell addr -> (Map.! addr) <$> S.gets memory
-                   Flag f    -> (Map.! f   ) <$> S.gets flags
-                   PC        -> pc <$> S.get
+        v <- case k of Reg  r    -> S.gets ((Map.! r) . registers)
+                       Cell addr -> S.gets ((Map.! addr) . memory)
+                       Flag f    -> S.gets ((Map.! f) . flags)
+                       PC        -> S.gets pc
         logEntry (ReadEntry k v)
         pure (t v)
     (Write k p t) -> do
@@ -229,9 +228,9 @@
 willOverflow :: Program Value -> Program Value -> Program Bool
 willOverflow arg1 arg2 =
     let o1 = (>) <$> arg2 <*> pure 0
-        o2 = (>) <$> arg1 <*> ((-) <$> pure maxBound <*> arg2)
+        o2 = (>) <$> arg1 <*> ((-) maxBound <$> arg2)
         o3 = (<) <$> arg2 <*> pure 0
-        o4 = (<) <$> arg1 <*> ((-) <$> pure minBound <*> arg2)
+        o4 = (<) <$> arg1 <*> ((-) minBound <$> arg2)
     in  (||) <$> ((&&) <$> o1 <*> o2)
              <*> ((&&) <$> o3 <*> o4)
 
diff --git a/examples/Query.hs b/examples/Query.hs
--- a/examples/Query.hs
+++ b/examples/Query.hs
@@ -2,7 +2,7 @@
 module Query where
 
 import Control.Selective
-import Data.List
+import Data.List (isInfixOf, stripPrefix)
 
 type Prompt = String
 
@@ -24,7 +24,7 @@
     select = Select
 
 pureQuery :: Query String
-pureQuery = (++) <$> pure "Hello " <*> pure "World!"
+pureQuery = (++) <$> Pure "Hello " <*> Pure "World!"
 
 replace :: String -> String -> String -> String
 replace [] _ xs = xs
diff --git a/examples/Teletype.hs b/examples/Teletype.hs
--- a/examples/Teletype.hs
+++ b/examples/Teletype.hs
@@ -14,7 +14,7 @@
 
 instance Eq (TeletypeF ()) where
     Read  _    == Read  _    = True
-    Write x () == Write y () = (x == y)
+    Write x () == Write y () = x == y
     _ == _ = False
 
 instance Show (TeletypeF a) where
@@ -74,7 +74,7 @@
 -- | Applicative ping-pong, which always executes both effect, but can be
 -- statically analysed.
 pingPongA :: IO ()
-pingPongA = fmap (\_ -> id) IO.getLine <*> IO.putStrLn "pong"
+pingPongA = IO.getLine *> IO.putStrLn "pong"
 
 -- | A monadic greeting. Cannot be implemented using selective functors.
 greeting :: IO ()
diff --git a/examples/Teletype/Rigid.hs b/examples/Teletype/Rigid.hs
--- a/examples/Teletype/Rigid.hs
+++ b/examples/Teletype/Rigid.hs
@@ -14,7 +14,7 @@
 
 instance Eq (TeletypeF ()) where
     Read  _    == Read  _    = True
-    Write x () == Write y () = (x == y)
+    Write x () == Write y () = x == y
     _ == _ = False
 
 instance Show (TeletypeF a) where
@@ -67,7 +67,7 @@
 -- | Applicative ping-pong, which always executes both effect, but can be
 -- statically analysed.
 pingPongA :: IO ()
-pingPongA = fmap (\_ -> id) IO.getLine <*> IO.putStrLn "pong"
+pingPongA = IO.getLine *> IO.putStrLn "pong"
 
 -- | A monadic greeting. Cannot be implemented using selective functors.
 greeting :: IO ()
diff --git a/examples/Validation.hs b/examples/Validation.hs
--- a/examples/Validation.hs
+++ b/examples/Validation.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE ConstraintKinds, DeriveFunctor, GADTs, RankNTypes #-}
+{-# LANGUAGE ConstraintKinds, GADTs, RankNTypes #-}
 module Validation where
 
 import Control.Selective
diff --git a/selective.cabal b/selective.cabal
--- a/selective.cabal
+++ b/selective.cabal
@@ -1,21 +1,17 @@
 name:          selective
-version:       0.4.1.1
+version:       0.4.2
 synopsis:      Selective applicative functors
 license:       MIT
 license-file:  LICENSE
 author:        Andrey Mokhov <andrey.mokhov@gmail.com>, github: @snowleopard
 maintainer:    Andrey Mokhov <andrey.mokhov@gmail.com>, github: @snowleopard
-copyright:     Andrey Mokhov, 2018-2020
+copyright:     Andrey Mokhov, 2018-2021
 homepage:      https://github.com/snowleopard/selective
+bug-reports:   https://github.com/snowleopard/selective/issues
 category:      Control
 build-type:    Simple
 cabal-version: 1.18
-tested-with:   GHC == 8.0.2,
-               GHC == 8.2.2,
-               GHC == 8.4.3,
-               GHC == 8.6.5,
-               GHC == 8.8.1
-stability:     experimental
+tested-with:   GHC==9.0, GHC==8.10, GHC==8.8, GHC==8.6, GHC==8.4, GHC==8.2, GHC==8.0
 description:   Selective applicative functors: declare your effects statically,
                select which to execute dynamically.
                .
@@ -50,7 +46,7 @@
                         RankNTypes,
                         StandaloneDeriving,
                         TupleSections
-    GHC-options:        -Wall
+    ghc-options:        -Wall
                         -fno-warn-name-shadowing
                         -Wcompat
                         -Wincomplete-record-updates
@@ -80,7 +76,7 @@
                         tasty-quickcheck       >= 0.8.4,
                         transformers           >= 0.4.2.0 && < 0.6
     default-language:   Haskell2010
-    GHC-options:        -Wall
+    ghc-options:        -Wall
                         -fno-warn-name-shadowing
                         -Wcompat
                         -Wincomplete-record-updates
diff --git a/src/Control/Selective.hs b/src/Control/Selective.hs
--- a/src/Control/Selective.hs
+++ b/src/Control/Selective.hs
@@ -1,4 +1,6 @@
-{-# LANGUAGE CPP, TupleSections, DeriveFunctor, GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE CPP, LambdaCase, TupleSections, DeriveFunctor #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# OPTIONS_GHC -fno-warn-unused-imports #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module     : Control.Selective
@@ -139,6 +141,31 @@
 class Applicative f => Selective f where
     select :: f (Either a b) -> f (a -> b) -> f b
 
+{- Why do we have skew associativity, where we can reassociate effects to the
+   left but not to the right?
+
+   The following two tables, which list all possible combinations of effect
+   execution and skipping, might give you some intuition on why this happens.
+
+     ---------------
+     (x <*? y) <*? z
+     ---------------
+      1     0      0
+      1     1      0
+      1     0      1
+      1     1      1
+
+     ---------------
+     x <*? (y <*? z)
+     ---------------
+     1      0     0
+     1      1     0
+     1      1     1
+
+   A key observation is that when effects are associated to the right, we can't
+   skip the effect y and execute the effect z: combination 101 is impossible.
+-}
+
 -- | An operator alias for 'select', which is sometimes convenient. It tries to
 -- follow the notational convention for 'Applicative' operators. The angle
 -- bracket pointing to the left means we always use the corresponding value.
@@ -196,8 +223,8 @@
 -- | One can easily implement a monadic 'selectM' that satisfies the laws,
 -- hence any 'Monad' is 'Selective'.
 selectM :: Monad f => f (Either a b) -> f (a -> b) -> f b
-selectM x y = x >>= \e -> case e of Left  a -> ($a) <$> y -- execute y
-                                    Right b -> pure b     -- skip y
+selectM x y = x >>= \case Left  a -> ($a) <$> y -- execute y
+                          Right b -> pure b     -- skip y
 
 -- Many useful 'Monad' combinators can be implemented with 'Selective'
 
@@ -240,7 +267,7 @@
 matchM :: Monad m => Cases a -> m a -> (a -> m b) -> m (Either a b)
 matchM (Cases _ p) mx f = do
     x <- mx
-    if p x then Right <$> (f x) else return (Left x)
+    if p x then Right <$> f x else return (Left x)
 
 -- TODO: Add a type-safe version based on @KnownNat@.
 -- | A restricted version of monadic bind. Fails with an error if the 'Bounded'
@@ -473,7 +500,7 @@
     select (ArrowMonad x) y = ArrowMonad $ x >>> (toArrow y ||| returnA)
 
 toArrow :: Arrow a => ArrowMonad a (i -> o) -> a i o
-toArrow (ArrowMonad f) = arr (\x -> ((), x)) >>> first f >>> arr (uncurry ($))
+toArrow (ArrowMonad f) = arr ((),) >>> first f >>> arr (uncurry ($))
 
 ---------------------------------- Alternative ---------------------------------
 -- | Composition of a functor @f@ with the 'Either' monad.
diff --git a/src/Control/Selective/Free.hs b/src/Control/Selective/Free.hs
--- a/src/Control/Selective/Free.hs
+++ b/src/Control/Selective/Free.hs
@@ -31,6 +31,8 @@
 -- | Free selective functors.
 newtype Select f a = Select (forall g. Selective g => (forall x. f x -> g x) -> g a)
 
+-- Ignoring the hint, since GHC can't type check the suggested code.
+{-# ANN module "HLint: ignore Use fmap" #-}
 instance Functor (Select f) where
     fmap f (Select x) = Select $ \k -> f <$> x k
 
@@ -43,7 +45,7 @@
 
 -- | Lift a functor into a free selective computation.
 liftSelect :: f a -> Select f a
-liftSelect x = Select ($x)
+liftSelect x = Select (\f -> f x)
 
 -- | Given a natural transformation from @f@ to @g@, this gives a canonical
 -- natural transformation from @Select f@ to @g@. Note that here we rely on the
diff --git a/src/Control/Selective/Multi.hs b/src/Control/Selective/Multi.hs
--- a/src/Control/Selective/Multi.hs
+++ b/src/Control/Selective/Multi.hs
@@ -251,7 +251,7 @@
 -- a tag, get the payload of the first product and then pass it as input to the
 -- second. This feels too trivial to be useful but is still somewhat cute.
 compose :: (u ~> v) -> (t ~> u) -> (t ~> v)
-compose = (.)
+compose f g = f . g
 
 -- | Update a generalised sum given a generalised product that takes care of all
 -- possible cases.
diff --git a/src/Control/Selective/Rigid/Free.hs b/src/Control/Selective/Rigid/Free.hs
--- a/src/Control/Selective/Rigid/Free.hs
+++ b/src/Control/Selective/Rigid/Free.hs
@@ -15,6 +15,12 @@
 -- This module defines /free rigid selective functors/. Rigid selective functors
 -- are those that satisfy the property @\<*\> = apS@.
 --
+-- Intuitively, a selective functor @f@ is "rigid" if any expression @f a@ is
+-- equivalent to a list of effects chained with @select@ operators (the normal
+-- form given by the free construction). In contrast, "non-rigid" selective
+-- functors can have non-linear, tree-like shapes, because @<*>@ nodes can't be
+-- straightened using the @\<*\> = apS@ equation.
+--
 -----------------------------------------------------------------------------
 module Control.Selective.Rigid.Free (
     -- * Free rigid selective functors
diff --git a/src/Control/Selective/Rigid/Freer.hs b/src/Control/Selective/Rigid/Freer.hs
--- a/src/Control/Selective/Rigid/Freer.hs
+++ b/src/Control/Selective/Rigid/Freer.hs
@@ -70,7 +70,7 @@
 
 -- | Lift a functor into a free selective computation.
 liftSelect :: f a -> Select f a
-liftSelect f = Select (Pure (Left id)) f
+liftSelect = Select (Pure (Left id))
 
 -- | Given a natural transformation from @f@ to @g@, this gives a canonical
 -- natural transformation from @Select f@ to @g@.
diff --git a/test/Laws.hs b/test/Laws.hs
--- a/test/Laws.hs
+++ b/test/Laws.hs
@@ -9,7 +9,6 @@
 import Control.Selective
 import Data.Function
 import Data.Functor.Identity
-import Control.Monad.State
 import Text.Show.Functions()
 
 -- | TODO:
@@ -55,17 +54,17 @@
 -- | Apply a pure function to the result:
 theorem1 :: (Selective f, Eq (f c)) =>
             (a -> c) -> f (Either b a) -> f (b -> a) -> Bool
-theorem1 f x y = (f <$> select x y) == (select (second f <$> x) ((f .) <$> y))
+theorem1 f x y = (f <$> select x y) == select (second f <$> x) ((f .) <$> y)
 
 -- | Apply a pure function to the Left case of the first argument:
 theorem2 :: (Selective f, Eq (f c)) =>
             (a -> b) -> f (Either a c) -> f (b -> c) -> Bool
-theorem2 f x y = (select (first f <$> x) y) == (select x ((. f) <$> y))
+theorem2 f x y = select (first f <$> x) y == select x ((. f) <$> y)
 
 -- | Apply a pure function to the second argument:
 theorem3 :: (Selective f, Eq (f c)) =>
             (a -> b -> c) -> f (Either b c) -> f a -> Bool
-theorem3 f x y = (select x (f <$> y)) == (select (first (flip f) <$> x) ((&) <$> y))
+theorem3 f x y = select x (f <$> y) == select (first (flip f) <$> x) ((&) <$> y)
 
 -- | Generalised identity:
 theorem4 :: (Selective f, Eq (f b)) => f (Either a b) -> (a -> b) -> Bool
@@ -123,7 +122,7 @@
 deriving instance (Eq e, Eq a) => Eq (Validation e a)
 
 instance (Arbitrary e, Arbitrary a) => Arbitrary (Validation e a) where
-  arbitrary = oneof [liftM Failure arbitrary, liftM Success arbitrary]
+  arbitrary = oneof [Failure <$> arbitrary, Success <$> arbitrary]
   shrink (Failure x) = [ Failure x' | x' <- shrink x ]
   shrink (Success y) = [ Success y' | y' <- shrink y ]
 
diff --git a/test/Sketch.hs b/test/Sketch.hs
--- a/test/Sketch.hs
+++ b/test/Sketch.hs
@@ -1,6 +1,6 @@
-{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE DeriveFunctor, EmptyCase, FlexibleInstances, GADTs, RankNTypes #-}
 {-# LANGUAGE MultiParamTypeClasses, ScopedTypeVariables, TupleSections #-}
+{-# OPTIONS_GHC -fno-warn-unused-imports #-}
 module Sketch where
 
 import Control.Arrow hiding (first, second)
@@ -10,9 +10,6 @@
 import Data.Bifunctor
 import Data.Bool
 import Data.Function
-import Data.Functor
-import Data.Functor.Identity
-import Data.Functor.Const
 import Data.Semigroup (Semigroup (..))
 import Data.Void
 
@@ -20,8 +17,11 @@
 import qualified Control.Category as C
 
 -- This file contains various examples and proof sketches and we keep it here to
--- make sure it still compiles.
+-- make sure it still compiles. We ignore HLINT suggestions because they often
+-- get in the way of readable "proofs" that use equational reasoning.
 
+{-# ANN module "HLint: ignore" #-}
+
 ------------------------------- Various examples -------------------------------
 
 bindBool :: Selective f => f Bool -> (Bool -> f a) -> f a
@@ -592,124 +592,3 @@
         rx <- iox
         case rx of Done       x -> runHaxl (f x) -- dynamic dependency on runtime value 'x'
                    Blocked bx x -> return (Blocked bx (x >>= f))
-
--- right' :: Choice p => p a b -> p (Either c a) (Either c b)
--- right' :: ... => (a -> f b) -> Either x a -> f (Either x b)
-
-data P s t a b = P { match' :: s -> Either a t, build' :: b -> t }
-
-fromP :: P s t a b -> Prism s t a b
-fromP (P match build) f s = case match s of
-    Left  a -> build <$> f a
-    Right t -> pure t
-
-
--- Choice p, Applicative f) => p a (f b) -> p s (f t)
-
--- (a -> f b) -> (Either a x -> f (Either b x))
-
-type Lens      s t a b = forall f. Functor f     => (a -> f b) -> s -> f t
-type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t
-type Prism     s t a b = forall f. Selective f   => (a -> f b) -> s -> f t
-
-_fst :: Lens (a, x) (b, x) a b
-_fst f (a, x) = f a <&> (,x)
-
-_snd :: Lens (x, a) (x, b) a b
-_snd f (x, a) = (x,) <$> f a
-
-_Left :: Prism (Either a x) (Either b x) a b
-_Left f = \case Left  a -> Left <$> f a
-                Right x -> pure (Right x)
-
-view :: Lens s t a b -> s -> a
-view lens s = getConst $ lens (\a -> Const a) s
-
-update :: Lens s t a b -> b -> s -> t
-update lens b s = runIdentity $ lens (\_a -> Identity b) s
-
-match :: Prism s t a b -> s -> Either a t
-match prism s = prism Left s
-
--- (a -> f s b) -> s -> f s t
-build :: Prism s t a b -> b -> t
-build prism b = either absurd id $ prism (\_a -> Right b) undefined
-
-
--- x <*? (y <*? z)
-
--- 1      0     0
--- 1      1     0
--- 1      1     1
-
--- (x <*? y) <*? z
-
--- 1      0      0
--- 1      1      0
--- 1      0      1
--- 1      1      1
-
-
--- data Evaluation e a = Unknown e | Known a | Wrapped (Evaluation e a)
---     deriving (Functor, Show)
-
--- type E e a = Identity
-
--- instance Semigroup e => Applicative (Evaluation e) where
---     pure = Known
---     Unknown e1 <*> Unknown e2 = Unknown (e1 <> e2)
---     Unknown e1 <*> Known _    = Unknown e1
---     Known _    <*> Unknown e2 = Unknown e2
---     Known f    <*> Known a    = Known (f a)
-
--- instance Semigroup e => Selective (Evaluation e) where
---     select (Known (Right b)) _            = Known b
---     select (Known (Left  a)) f            = ($a) <$> f
---     select (Unknown e1     ) (Known   _ ) = Unknown e1
---     select (Unknown e1     ) (Unknown e2) = Unknown (e1 <> e2)
-
-
-data C f g a where
-    C :: f x -> g y -> (x -> Either (y -> a) a) -> C f g a
-
-instance Functor (C f g) where
-    fmap f (C p q k) = C p q (fmap (bimap (f.) f) k)
-
-instance (Applicative f, Applicative g) => Applicative (C f g) where
-    pure a = C (pure ()) (pure ()) (const (Left (const a)))
-    C p1 q1 k1 <*> C p2 q2 k2 = C ((,) <$> p1 <*> p2) ((,) <$> q1 <*> q2) $
-        \(x1, x2) -> Left (\(y1, y2) ->
-            (either ($y1) id (k1 x1)) (either ($y2) id (k2 x2)))
-
--- class Applicative f => SelectiveQ f where
---     select :: Enumerable t => f (g a) -> (t ~> f :*: u) -> f (Sigma u)
-
--- instance (Selective f, Selective g) => Selective (f :*: g) where
-
--- instance Selective (Maybe :*: Maybe) where
-
--- instance Selective Maybe where
---     match sigma pi = sigma >>= \s -> pureSelect s pi
-
-
-
--- data Value a b = Likely a | Unlikely b
--- Some kind of "Sigma arrows"
--- Sigma t -> (Match t (Sigma s)) -> Sigma s
--- Sigma t -> (t ~> Sigma s) -> Sigma s
-
--- branchU :: forall f a b c. SelectiveU f => f (Either a b) -> f (a -> c) -> f (b -> c) -> f c
--- branchU x f g = selectU (toAB <$> x) h
---   where
---     -- toAB :: Either a b -> (AB a b x, x)
---     toAB (Left  a) = (A, a)
---     toAB (Right b) = (B, b)
---     -- h :: AB a b x -> f (x -> c)
---     h A = f
---     h B = g
-
--- applyS :: forall f a b. SelectiveS f => f a -> f (a -> b) -> f b
--- applyS x f = sigmaSelect (Sigma Refl <$> x) h
---   where
---     h :: forall x. Refl a x -> f (x -> b)
---     h Refl = f