diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,15 @@
 Changelog
 =========
 
+Version 0.1.4.1
+---------------
+
+*February 27, 2023*
+
+<https://github.com/mstksg/list-witnesses/releases/tag/v0.1.4.1>
+
+*   Remove upper bounds, fix deprecated pragmas
+
 Version 0.1.4.0
 ---------------
 
diff --git a/list-witnesses.cabal b/list-witnesses.cabal
--- a/list-witnesses.cabal
+++ b/list-witnesses.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           list-witnesses
-version:        0.1.4.0
+version:        0.1.4.1
 synopsis:       Witnesses for working with type-level lists
 description:    Collection of assorted inductive witnesses and functions for working with
                 type-level lists.
@@ -44,11 +44,11 @@
   ghc-options: -Wall -Wcompat -Wredundant-constraints -Werror=incomplete-patterns
   build-depends:
       base >=4.7 && <5
-    , decidable >=0.3.1 && <0.4
-    , functor-products >=0.1.2 && <0.2
-    , microlens <0.5
-    , profunctors <5.7
-    , singletons-base >=3.0 && <3.1
-    , singletons >=3.0 && <3.2
-    , vinyl >=0.14.3 &&  <0.15
+    , decidable >=0.3.1.1
+    , functor-products >=0.1.2
+    , microlens
+    , profunctors
+    , singletons-base >=3.0
+    , singletons >=3.0
+    , vinyl >=0.14.3
   default-language: Haskell2010
diff --git a/src/Data/Type/List/Edit.hs b/src/Data/Type/List/Edit.hs
--- a/src/Data/Type/List/Edit.hs
+++ b/src/Data/Type/List/Edit.hs
@@ -1,19 +1,18 @@
-{-# LANGUAGE EmptyCase             #-}
-{-# LANGUAGE FlexibleContexts      #-}
-{-# LANGUAGE FlexibleInstances     #-}
-{-# LANGUAGE GADTs                 #-}
-{-# LANGUAGE KindSignatures        #-}
-{-# LANGUAGE LambdaCase            #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE RankNTypes            #-}
-{-# LANGUAGE ScopedTypeVariables   #-}
-{-# LANGUAGE StandaloneDeriving    #-}
-{-# LANGUAGE TypeApplications      #-}
-{-# LANGUAGE TypeFamilies          #-}
-{-# LANGUAGE TypeInType            #-}
-{-# LANGUAGE TypeOperators         #-}
-{-# LANGUAGE TypeSynonymInstances  #-}
-{-# LANGUAGE UndecidableInstances  #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 -- |
 -- Module      : Data.Type.List.Edit
@@ -27,59 +26,88 @@
 -- Witnesses regarding single-item edits of lists.
 module Data.Type.List.Edit (
   -- * Simple edits
-    Insert(..), autoInsert
-  , Delete(..), autoDelete
-  , insToDel
-  , delToIns
-  , Substitute(..), autoSubstitute
-  , flipSub
-  , subToDelIns
+  Insert (..),
+  autoInsert,
+  Delete (..),
+  autoDelete,
+  insToDel,
+  delToIns,
+  Substitute (..),
+  autoSubstitute,
+  flipSub,
+  subToDelIns,
+
   -- ** Predicates
-  , IsInsert, InsertedInto
-  , IsDelete, DeletedFrom
-  , IsSubstitute
+  IsInsert,
+  InsertedInto,
+  IsDelete,
+  DeletedFrom,
+  IsSubstitute,
+
   -- ** Singletons
-  , SInsert(..)
-  , SDelete(..)
-  , SSubstitute(..)
+  SInsert (..),
+  SDelete (..),
+  SSubstitute (..),
+
   -- * Compound edits
-  , Edit(..)
-  , compEdit
-  , flipEdit
+  Edit (..),
+  compEdit,
+  flipEdit,
+
   -- * Rec
-  , insertRec, deleteRec, deleteGetRec
-  , recLens, substituteRec
+  insertRec,
+  deleteRec,
+  deleteGetRec,
+  recLens,
+  substituteRec,
+
   -- * Index
+
   -- ** Manipulating indices
-  , insertIndex
-  , DeletedIx(..), deleteIndex, deleteIndex_
-  , SubstitutedIx(..), substituteIndex, substituteIndex_
+  insertIndex,
+  DeletedIx (..),
+  deleteIndex,
+  deleteIndex_,
+  SubstitutedIx (..),
+  substituteIndex,
+  substituteIndex_,
+
   -- ** Converting from indices
-  , withDelete, withInsert, withInsertAfter
+  withDelete,
+  withInsert,
+  withInsertAfter,
+
   -- * Type-Level
-  , InsertIndex, sInsertIndex
-  , SDeletedIx(..)
-  , DeleteIndex, sDeleteIndex
-  , SSubstitutedIx(..)
-  , SubstituteIndex, sSubstituteIndex
+  InsertIndex,
+  sInsertIndex,
+  SDeletedIx (..),
+  DeleteIndex,
+  sDeleteIndex,
+  SSubstitutedIx (..),
+  SubstituteIndex,
+  sSubstituteIndex,
+
   -- ** Defunctionalization Symbols
-  , InsertIndexSym0, InsertIndexSym
-  , DeleteIndexSym0, DeleteIndexSym
-  , SubstituteIndexSym0, SubstituteIndexSym
-  ) where
+  InsertIndexSym0,
+  InsertIndexSym,
+  DeleteIndexSym0,
+  DeleteIndexSym,
+  SubstituteIndexSym0,
+  SubstituteIndexSym,
+) where
 
-import           Data.Function.Singletons (IdSym0)
-import           Data.Kind
-import           Data.List.Singletons (SList(..))
-import           Data.Singletons
-import           Data.Singletons.Decide
-import           Data.Singletons.Sigma
-import           Data.Type.Functor.Product
-import           Data.Type.Predicate
-import           Data.Type.Predicate.Auto
-import           Data.Type.Predicate.Param
-import           Lens.Micro hiding         ((%~))
-import qualified Control.Category          as C
+import qualified Control.Category as C
+import Data.Function.Singletons (IdSym0)
+import Data.Kind
+import Data.List.Singletons (SList (..))
+import Data.Singletons
+import Data.Singletons.Decide
+import Data.Singletons.Sigma
+import Data.Type.Functor.Product
+import Data.Type.Predicate
+import Data.Type.Predicate.Auto
+import Data.Type.Predicate.Param
+import Lens.Micro hiding ((%~))
 
 -- | An @'Insert' as bs x@ is a witness that you can insert @x@ into some
 -- position in list @as@ to produce list @bs@.  It is essentially 'Delete'
@@ -96,8 +124,8 @@
 --
 -- @bs@ will always be exactly one item longer than @as@.
 data Insert :: [k] -> [k] -> k -> Type where
-    InsZ :: Insert as (x ': as) x
-    InsS :: Insert as bs x -> Insert (a ': as) (a ': bs) x
+  InsZ :: Insert as (x ': as) x
+  InsS :: Insert as bs x -> Insert (a ': as) (a ': bs) x
 
 deriving instance Show (Insert as bs x)
 
@@ -109,29 +137,17 @@
 
 -- | Prefers the "earlier" insert if there is ambiguity
 instance Auto (IsInsert as (x ': as)) x where
-    auto = InsZ
+  auto = InsZ
 
 instance {-# INCOHERENT #-} Auto (IsInsert as bs) x => Auto (IsInsert (a ': as) (a ': bs)) x where
-    auto = InsS (auto @_ @(IsInsert as bs) @x)
+  auto = InsS (auto @_ @(IsInsert as bs) @x)
 
 instance (SDecide k, SingI (as :: [k]), SingI bs) => Decidable (IsInsert as bs) where
-    decide z = case sing @bs of
-      SNil -> Disproved $ \case {}
-      y `SCons` (ys@Sing :: Sing bs') -> case y %~ z of
-        Proved Refl -> case sing @as %~ ys of
-          Proved Refl -> Proved InsZ
-          Disproved v -> case sing @as of
-            SNil -> Disproved $ \case
-              InsZ -> v Refl
-            x `SCons` (Sing :: Sing as') -> case x %~ y of
-              Proved Refl -> case decide @(IsInsert as' bs') z of
-                Proved i -> Proved $ InsS i
-                Disproved u -> Disproved $ \case
-                  InsZ -> u InsZ
-                  InsS i -> u i
-              Disproved u -> Disproved $ \case
-                InsZ   -> v Refl
-                InsS _ -> u Refl
+  decide z = case sing @bs of
+    SNil -> Disproved $ \case {}
+    y `SCons` (ys@Sing :: Sing bs') -> case y %~ z of
+      Proved Refl -> case sing @as %~ ys of
+        Proved Refl -> Proved InsZ
         Disproved v -> case sing @as of
           SNil -> Disproved $ \case
             InsZ -> v Refl
@@ -142,8 +158,20 @@
                 InsZ -> u InsZ
                 InsS i -> u i
             Disproved u -> Disproved $ \case
-              InsZ   -> v Refl
+              InsZ -> v Refl
               InsS _ -> u Refl
+      Disproved v -> case sing @as of
+        SNil -> Disproved $ \case
+          InsZ -> v Refl
+        x `SCons` (Sing :: Sing as') -> case x %~ y of
+          Proved Refl -> case decide @(IsInsert as' bs') z of
+            Proved i -> Proved $ InsS i
+            Disproved u -> Disproved $ \case
+              InsZ -> u InsZ
+              InsS i -> u i
+          Disproved u -> Disproved $ \case
+            InsZ -> v Refl
+            InsS _ -> u Refl
 
 -- | If @bs@ satisfies @'InsertedInto' as@, it means that there exists some
 -- element @x@ such that @'IsInsert' as bs \@\@ x@: you can get @bs@ by
@@ -166,22 +194,22 @@
 type InsertedInto (as :: [k]) = (TyPP (Insert as) :: ParamPred [k] k)
 
 instance (SDecide k, SingI (as :: [k])) => Decidable (Found (InsertedInto as)) where
-    decide = \case
-      SNil -> Disproved $ \(_ :&: i) -> case i of {}
-      y `SCons` ys -> case sing @as %~ ys of
-        Proved Refl -> Proved $ y :&: InsZ
-        Disproved v -> case sing @as of
-          SNil -> Disproved $ \(_ :&: i) -> case i of
+  decide = \case
+    SNil -> Disproved $ \(_ :&: i) -> case i of {}
+    y `SCons` ys -> case sing @as %~ ys of
+      Proved Refl -> Proved $ y :&: InsZ
+      Disproved v -> case sing @as of
+        SNil -> Disproved $ \(_ :&: i) -> case i of
+          InsZ -> v Refl
+        x `SCons` (Sing :: Sing as') -> case x %~ y of
+          Proved Refl -> case decide @(Found (InsertedInto as')) ys of
+            Proved (z :&: i) -> Proved $ z :&: InsS i
+            Disproved u -> Disproved $ \(z :&: i) -> case i of
+              InsZ -> u $ z :&: InsZ
+              InsS i' -> u $ z :&: i'
+          Disproved u -> Disproved $ \(_ :&: i) -> case i of
             InsZ -> v Refl
-          x `SCons` (Sing :: Sing as') -> case x %~ y of
-            Proved Refl -> case decide @(Found (InsertedInto as')) ys of
-              Proved (z :&: i) -> Proved $ z :&: InsS i
-              Disproved u      -> Disproved $ \(z :&: i) -> case i of
-                InsZ    -> u $ z :&: InsZ
-                InsS i' -> u $ z :&: i'
-            Disproved u -> Disproved $ \(_ :&: i) -> case i of
-              InsZ   -> v Refl
-              InsS _ -> u Refl
+            InsS _ -> u Refl
 
 -- | Automatically generate an 'Insert' if @as@, @bs@ and @x@ are known
 -- statically.
@@ -200,16 +228,16 @@
 
 -- | Kind-indexed singleton for 'Insert'.
 data SInsert (as :: [k]) (bs :: [k]) (x :: k) :: Insert as bs x -> Type where
-    SInsZ :: SInsert as (x ': as) x 'InsZ
-    SInsS :: SInsert as bs x ins -> SInsert (a ': as) (a ': bs) x ('InsS ins)
+  SInsZ :: SInsert as (x ': as) x 'InsZ
+  SInsS :: SInsert as bs x ins -> SInsert (a ': as) (a ': bs) x ('InsS ins)
 
 deriving instance Show (SInsert as bs x del)
 
 -- | Flip an insertion.
 insToDel :: Insert as bs x -> Delete bs as x
 insToDel = \case
-    InsZ   -> DelZ
-    InsS i -> DelS (insToDel i)
+  InsZ -> DelZ
+  InsS i -> DelS (insToDel i)
 
 -- | A @'Delete' as bs x@ is a witness that you can delete item @x@ from
 -- @as@ to produce the list @bs@.  It is essentially 'Insert' flipped.
@@ -224,8 +252,8 @@
 --
 -- @bs@ will always be exactly one item shorter than @as@.
 data Delete :: [k] -> [k] -> k -> Type where
-    DelZ :: Delete (x ': as) as x
-    DelS :: Delete as bs x -> Delete (a ': as) (a ': bs) x
+  DelZ :: Delete (x ': as) as x
+  DelS :: Delete as bs x -> Delete (a ': as) (a ': bs) x
 
 deriving instance Show (Delete as bs x)
 
@@ -237,13 +265,13 @@
 
 -- | Prefers the "earlier" delete if there is ambiguity
 instance Auto (IsDelete (x ': as) as) x where
-    auto = DelZ
+  auto = DelZ
 
 instance {-# INCOHERENT #-} Auto (IsDelete as bs) x => Auto (IsDelete (a ': as) (a ': bs)) x where
-    auto = DelS (auto @_ @(IsDelete as bs) @x)
+  auto = DelS (auto @_ @(IsDelete as bs) @x)
 
 instance (SDecide k, SingI (as :: [k]), SingI bs) => Decidable (IsDelete as bs) where
-    decide = mapDecision insToDel delToIns . decide @(IsInsert bs as)
+  decide = mapDecision insToDel delToIns . decide @(IsInsert bs as)
 
 -- | If @bs@ satisfies @'DeletedFrom' as@, it means that there exists some
 -- element @x@ such that @'IsDelete' as bs \@\@ x@: you can get @bs@ by
@@ -266,9 +294,10 @@
 type DeletedFrom (as :: [k]) = (TyPP (Delete as) :: ParamPred [k] k)
 
 instance (SDecide k, SingI (as :: [k])) => Decidable (Found (DeletedFrom as)) where
-    decide (Sing :: Sing bs) =
-        mapDecision (mapSigma (sing @IdSym0) insToDel)
-                    (mapSigma (sing @IdSym0) delToIns)
+  decide (Sing :: Sing bs) =
+    mapDecision
+      (mapSigma (sing @IdSym0) insToDel)
+      (mapSigma (sing @IdSym0) delToIns)
       $ decide @(Found (InsertedInto bs)) (sing @as)
 
 -- | Automatically generate an 'Delete' if @as@, @bs@ and @x@ are known
@@ -288,16 +317,16 @@
 
 -- | Kind-indexed singleton for 'Delete'.
 data SDelete (as :: [k]) (bs :: [k]) (x :: k) :: Delete as bs x -> Type where
-    SDelZ :: SDelete (x ': as) as x 'DelZ
-    SDelS :: SDelete as bs x del -> SDelete (a ': as) (a ': bs) x ('DelS del)
+  SDelZ :: SDelete (x ': as) as x 'DelZ
+  SDelS :: SDelete as bs x del -> SDelete (a ': as) (a ': bs) x ('DelS del)
 
 deriving instance Show (SDelete as bs x del)
 
 -- | Flip a deletion.
 delToIns :: Delete as bs x -> Insert bs as x
 delToIns = \case
-    DelZ   -> InsZ
-    DelS d -> InsS (delToIns d)
+  DelZ -> InsZ
+  DelS d -> InsS (delToIns d)
 
 -- | A @'Substitute' as bs x y@ is a witness that you can replace item @x@ in
 -- @as@ with item @y@ to produce @bs@.
@@ -309,10 +338,9 @@
 -- SubS SubZ        :: Substitute '[1,2,3] '[1,4,3] 2 4
 -- SubS (SubS SubZ) :: Substitute '[1,2,3] '[1,2,4] 3 4
 -- @
---
 data Substitute :: [k] -> [k] -> k -> k -> Type where
-    SubZ :: Substitute (x ': as) (y ': as) x y
-    SubS :: Substitute as bs x y -> Substitute (c ': as) (c ': bs) x y
+  SubZ :: Substitute (x ': as) (y ': as) x y
+  SubS :: Substitute as bs x y -> Substitute (c ': as) (c ': bs) x y
 
 deriving instance Show (Substitute as bs x y)
 
@@ -323,14 +351,14 @@
 type IsSubstitute as bs x = TyPred (Substitute as bs x)
 
 instance Auto (IsSubstitute (x ': as) (y ': as) x) y where
-    auto = SubZ
+  auto = SubZ
 
 -- | Prefers the earlier subsitution if there is ambiguity.
 instance Auto (IsSubstitute as bs x) y => Auto (IsSubstitute (c ': as) (c ': bs) x) y where
-    auto = SubS (auto @_ @(IsSubstitute as bs x) @y)
+  auto = SubS (auto @_ @(IsSubstitute as bs x) @y)
 
 instance {-# INCOHERENT #-} Auto (IsSubstitute (x ': as) (x ': as) x) x where
-    auto = SubZ
+  auto = SubZ
 
 -- | Automatically generate an 'Substitute' if @as@, @bs@, @x@, and @y@ are
 -- known statically.
@@ -349,24 +377,25 @@
 
 -- | Kind-indexed singleton for 'Substitute'.
 data SSubstitute (as :: [k]) (bs :: [k]) (x :: k) (y :: k) :: Substitute as bs x y -> Type where
-    SSubZ :: SSubstitute (x ': as) (y ': as) x y 'SubZ
-    SSubS :: SSubstitute as bs x y sub
-          -> SSubstitute (c ': as) (c ': bs) x y ('SubS sub)
+  SSubZ :: SSubstitute (x ': as) (y ': as) x y 'SubZ
+  SSubS ::
+    SSubstitute as bs x y sub ->
+    SSubstitute (c ': as) (c ': bs) x y ('SubS sub)
 
 -- | Flip a substitution
 flipSub :: Substitute as bs x y -> Substitute bs as y x
 flipSub = \case
-    SubZ   -> SubZ
-    SubS s -> SubS (flipSub s)
+  SubZ -> SubZ
+  SubS s -> SubS (flipSub s)
 
 -- | Decompose a 'Substitute' into a 'Delete' followed by an 'Insert'.
-subToDelIns
-    :: Substitute as bs x y
-    -> (forall cs. Delete as cs x -> Insert cs bs y -> r)
-    -> r
+subToDelIns ::
+  Substitute as bs x y ->
+  (forall cs. Delete as cs x -> Insert cs bs y -> r) ->
+  r
 subToDelIns = \case
-    SubZ   -> \f -> f DelZ InsZ
-    SubS s -> \f -> subToDelIns s $ \d i -> f (DelS d) (InsS i)
+  SubZ -> \f -> f DelZ InsZ
+  SubS s -> \f -> subToDelIns s $ \d i -> f (DelS d) (InsS i)
 
 -- | An @'Edit' as bs@ is a reversible edit script transforming @as@ into
 -- @bs@ through successive insertions, deletions, and substitutions.
@@ -374,25 +403,25 @@
 -- TODO: implement Wagner-Fischer or something similar to minimize find
 -- a minimal edit distance
 data Edit :: [k] -> [k] -> Type where
-    ENil :: Edit as as
-    EIns :: Insert bs cs x -> Edit as bs -> Edit as cs
-    EDel :: Delete bs cs x -> Edit as bs -> Edit as cs
-    ESub :: Substitute bs cs x y -> Edit as bs -> Edit as cs
+  ENil :: Edit as as
+  EIns :: Insert bs cs x -> Edit as bs -> Edit as cs
+  EDel :: Delete bs cs x -> Edit as bs -> Edit as cs
+  ESub :: Substitute bs cs x y -> Edit as bs -> Edit as cs
 
 deriving instance Show (Edit as bs)
 
 -- | Compose two 'Edit's
 compEdit :: Edit as bs -> Edit bs cs -> Edit as cs
 compEdit xs = \case
-    ENil -> xs
-    EIns i ys -> EIns i (compEdit xs ys)
-    EDel d ys -> EDel d (compEdit xs ys)
-    ESub s ys -> ESub s (compEdit xs ys)
+  ENil -> xs
+  EIns i ys -> EIns i (compEdit xs ys)
+  EDel d ys -> EDel d (compEdit xs ys)
+  ESub s ys -> ESub s (compEdit xs ys)
 
 -- | 'Edit' composition
 instance C.Category Edit where
-    id = ENil
-    xs . ys = compEdit ys xs
+  id = ENil
+  xs . ys = compEdit ys xs
 
 -- | Reverse an 'Edit' script.  O(n^2).  Please do not use ever in any
 -- circumstance.
@@ -400,34 +429,35 @@
 -- TODO: Make O(n) using diff lists.
 flipEdit :: Edit as bs -> Edit bs as
 flipEdit = \case
-    ENil      -> ENil
-    EIns i ys -> EDel (insToDel i) ENil `compEdit` flipEdit ys
-    EDel d ys -> EIns (delToIns d) ENil `compEdit` flipEdit ys
-    ESub s ys -> ESub (flipSub  s) ENil `compEdit` flipEdit ys
+  ENil -> ENil
+  EIns i ys -> EDel (insToDel i) ENil `compEdit` flipEdit ys
+  EDel d ys -> EIns (delToIns d) ENil `compEdit` flipEdit ys
+  ESub s ys -> ESub (flipSub s) ENil `compEdit` flipEdit ys
 
 -- | Insert a value into a 'Rec', at a position indicated by the 'Insert'.
 insertRec :: Insert as bs x -> f x -> Rec f as -> Rec f bs
 insertRec = \case
-    InsZ   -> (:&)
-    InsS i -> \x -> \case
-      y :& ys -> y :& insertRec i x ys
+  InsZ -> (:&)
+  InsS i -> \x -> \case
+    y :& ys -> y :& insertRec i x ys
 
 -- | Retrieve and delete a value in a 'Rec', at a position indicated by the 'Delete'.
 deleteGetRec :: Delete as bs x -> Rec f as -> (f x, Rec f bs)
 deleteGetRec = \case
-    DelZ -> \case
-      x :& xs -> (x, xs)
-    DelS d -> \case
-      x :& xs -> let (y, ys) = deleteGetRec d xs
-                 in  (y, x :& ys)
+  DelZ -> \case
+    x :& xs -> (x, xs)
+  DelS d -> \case
+    x :& xs ->
+      let (y, ys) = deleteGetRec d xs
+       in (y, x :& ys)
 
 -- | Delete a value in a 'Rec', at a position indicated by the 'Delete'.
 deleteRec :: Delete as bs x -> Rec f as -> Rec f bs
 deleteRec = \case
-    DelZ -> \case
-      _ :& xs -> xs
-    DelS d -> \case
-      x :& xs -> x :& deleteRec d xs
+  DelZ -> \case
+    _ :& xs -> xs
+  DelS d -> \case
+    x :& xs -> x :& deleteRec d xs
 
 -- | A type-changing lens into a value in a 'Rec', given a 'Substitute'
 -- indicating which value.
@@ -445,15 +475,17 @@
 --
 -- This is similar to 'Data.Vinyl.Lens.rlensC' from /vinyl/, but is built
 -- explicitly and inductively, instead of using typeclass magic.
-recLens
-    :: forall as bs x y f. ()
-    => Substitute as bs x y
-    -> Lens (Rec f as) (Rec f bs) (f x) (f y)
+recLens ::
+  forall as bs x y f.
+  () =>
+  Substitute as bs x y ->
+  Lens (Rec f as) (Rec f bs) (f x) (f y)
 recLens s0 (f :: f x -> g (f y)) = go s0
   where
-    go  :: Substitute cs ds x y
-        -> Rec f cs
-        -> g (Rec f ds)
+    go ::
+      Substitute cs ds x y ->
+      Rec f cs ->
+      g (Rec f ds)
     go = \case
       SubZ -> \case
         x :& xs -> (:& xs) <$> f x
@@ -462,11 +494,11 @@
 
 -- | Substitute a value in a 'Rec' at a given position, indicated by the
 -- 'Substitute'.  This is essentially a specialized version of 'recLens'.
-substituteRec
-    :: Substitute as bs x y
-    -> (f x -> f y)
-    -> Rec f as
-    -> Rec f bs
+substituteRec ::
+  Substitute as bs x y ->
+  (f x -> f y) ->
+  Rec f as ->
+  Rec f bs
 substituteRec s = over (recLens s)
 
 -- | If you add an item to @as@ to create @bs@, you also need to shift an
@@ -475,17 +507,17 @@
 -- same original value.
 insertIndex :: Insert as bs x -> Index as y -> Index bs y
 insertIndex = \case
-    InsZ   -> IS
-    InsS ins -> \case
-      IZ   -> IZ
-      IS i -> IS (insertIndex ins i)
+  InsZ -> IS
+  InsS ins -> \case
+    IZ -> IZ
+    IS i -> IS (insertIndex ins i)
 
 -- | Used as the return type of 'deleteIndex'.  An @'DeletedIx' bs x y@ is
 -- like a @'Maybe' ('Index' bs y)@, except the 'Nothing' case witnesses
 -- that @x ~ y@.
 data DeletedIx :: [k] -> k -> k -> Type where
-    GotDeleted :: DeletedIx bs x x
-    NotDeleted :: Index bs y -> DeletedIx bs x y
+  GotDeleted :: DeletedIx bs x x
+  NotDeleted :: Index bs y -> DeletedIx bs x y
 
 deriving instance Show (DeletedIx bs x y)
 
@@ -500,29 +532,29 @@
 -- returns 'NotDeleted' with the unshifted index.
 deleteIndex :: Delete as bs x -> Index as y -> DeletedIx bs x y
 deleteIndex = \case
-    DelZ -> \case
-      IZ   -> GotDeleted
-      IS i -> NotDeleted i
-    DelS del -> \case
-      IZ   -> NotDeleted IZ
-      IS i -> case deleteIndex del i of
-        GotDeleted   -> GotDeleted
-        NotDeleted j -> NotDeleted (IS j)
+  DelZ -> \case
+    IZ -> GotDeleted
+    IS i -> NotDeleted i
+  DelS del -> \case
+    IZ -> NotDeleted IZ
+    IS i -> case deleteIndex del i of
+      GotDeleted -> GotDeleted
+      NotDeleted j -> NotDeleted (IS j)
 
 -- | A version of 'deleteIndex' returning a simple 'Maybe'.  This can be
 -- used if you don't care about witnessing that @x ~ y@ in the case that
 -- the index is the item that is deleted.
 deleteIndex_ :: Delete as bs x -> Index as y -> Maybe (Index bs y)
 deleteIndex_ del i = case deleteIndex del i of
-    GotDeleted   -> Nothing
-    NotDeleted j -> Just j
+  GotDeleted -> Nothing
+  NotDeleted j -> Just j
 
 -- | Used as the return type of 'substituteIndex'.  An @'SubstitutedIx' bs x y z@ is
 -- like an @'Either' ('Index' bs y) ('Index' bs z)@, except the 'Left' case
 -- witnesses that @x ~ z@.
 data SubstitutedIx :: [k] -> k -> k -> k -> Type where
-    GotSubbed :: Index bs y -> SubstitutedIx bs z y z
-    NotSubbed :: Index bs z -> SubstitutedIx bs x y z
+  GotSubbed :: Index bs y -> SubstitutedIx bs z y z
+  NotSubbed :: Index bs z -> SubstitutedIx bs x y z
 
 -- | If you substitute an item in @as@ to create @bs@, you also need to
 -- reshift @'Index' as z@ into @'Index' bs z@.  This reshifts the 'Index'
@@ -533,72 +565,75 @@
 -- that the index was originally pointing to.  If this is the case, this
 -- function returns 'GotSubbed', a witness that @x ~ z@.  Otherwise, it
 -- returns 'NotSubbed'.  Both contain the updated index.
-substituteIndex
-    :: Substitute as bs x y
-    -> Index as z
-    -> SubstitutedIx bs x y z
+substituteIndex ::
+  Substitute as bs x y ->
+  Index as z ->
+  SubstitutedIx bs x y z
 substituteIndex = \case
-    SubZ -> \case
-      IZ   -> GotSubbed IZ
-      IS i -> NotSubbed (IS i)
-    SubS s -> \case
-      IZ   -> NotSubbed IZ
-      IS i -> case substituteIndex s i of
-        GotSubbed j -> GotSubbed (IS j)
-        NotSubbed j -> NotSubbed (IS j)
+  SubZ -> \case
+    IZ -> GotSubbed IZ
+    IS i -> NotSubbed (IS i)
+  SubS s -> \case
+    IZ -> NotSubbed IZ
+    IS i -> case substituteIndex s i of
+      GotSubbed j -> GotSubbed (IS j)
+      NotSubbed j -> NotSubbed (IS j)
 
 -- | A version of 'substituteIndex' returning a simple 'Either'.  This can be
 -- the case if you don't care about witnessing @x ~ z@ in the case that the
 -- index is the item that was substituted.
-substituteIndex_
-    :: Substitute as bs x y
-    -> Index as z
-    -> Either (Index bs y) (Index bs z)
+substituteIndex_ ::
+  Substitute as bs x y ->
+  Index as z ->
+  Either (Index bs y) (Index bs z)
 substituteIndex_ sub i = case substituteIndex sub i of
-    GotSubbed j -> Left  j
-    NotSubbed j -> Right j
+  GotSubbed j -> Left j
+  NotSubbed j -> Right j
 
 -- | Given an 'Index' pointing to an element, create a 'Delete'
 -- corresponding to the given item.  The type of the resulting list is
 -- existentially quantified, is guaranteed to be just exactly the original
 -- list minus the specified element.
-withDelete
-    :: Index as x
-    -> (forall bs. Delete as bs x -> r)
-    -> r
+withDelete ::
+  Index as x ->
+  (forall bs. Delete as bs x -> r) ->
+  r
 withDelete = \case
-    IZ   -> \f -> f DelZ
-    IS i -> \f -> withDelete i (f . DelS)
+  IZ -> \f -> f DelZ
+  IS i -> \f -> withDelete i (f . DelS)
 
 -- | Given an 'Index' pointing to an element, create an 'Insert' placing an
 -- item /directly before/ the given element.  The type is existentailly
 -- quantified.
-withInsert
-    :: Index as x
-    -> (forall bs. Insert as bs y -> r)
-    -> r
+withInsert ::
+  Index as x ->
+  (forall bs. Insert as bs y -> r) ->
+  r
 withInsert = \case
-    IZ   -> \f -> f InsZ
-    IS i -> \f -> withInsert i (f . InsS)
+  IZ -> \f -> f InsZ
+  IS i -> \f -> withInsert i (f . InsS)
 
 -- | Given an 'Index' pointing to an element, create an 'Insert' placing an
 -- item /directly after/ the given element.  The type is existentailly
 -- quantified.
-withInsertAfter
-    :: Index as x
-    -> (forall bs. Insert as bs y -> r)
-    -> r
+withInsertAfter ::
+  Index as x ->
+  (forall bs. Insert as bs y -> r) ->
+  r
 withInsertAfter = \case
-    IZ   -> \f -> f (InsS InsZ)
-    IS i -> \f -> withInsertAfter i (f . InsS)
+  IZ -> \f -> f (InsS InsZ)
+  IS i -> \f -> withInsertAfter i (f . InsS)
 
 -- | Type-level version of 'insertIndex'.  Because of how GADTs and type
 -- families interact, the type-level lists and kinds of the insertion and
 -- index must be provided.
-type family InsertIndex (as :: [k]) (bs :: [k]) (x :: k) (y :: k) (ins :: Insert as bs x) (i :: Index as y) :: Index bs y where
-    InsertIndex as        (x ': as) x y 'InsZ       i       = 'IS i
-    InsertIndex (y ': as) (y ': bs) x y ('InsS ins) 'IZ     = 'IZ
-    InsertIndex (a ': as) (a ': bs) x y ('InsS ins) ('IS i) = 'IS (InsertIndex as bs x y ins i)
+type family
+  InsertIndex (as :: [k]) (bs :: [k]) (x :: k) (y :: k) (ins :: Insert as bs x) (i :: Index as y) ::
+    Index bs y
+  where
+  InsertIndex as (x ': as) x y 'InsZ i = 'IS i
+  InsertIndex (y ': as) (y ': bs) x y ('InsS ins) 'IZ = 'IZ
+  InsertIndex (a ': as) (a ': bs) x y ('InsS ins) ('IS i) = 'IS (InsertIndex as bs x y ins i)
 
 -- | Defunctionalization symbol for 'InsertIndex', expecting only the kind
 -- variables.
@@ -612,30 +647,37 @@
 type instance Apply (InsertIndexSym as bs x y ins) i = InsertIndex as bs x y ins i
 
 -- | Singleton witness for 'InsertIndex'.
-sInsertIndex
-    :: SInsert as bs x ins
-    -> SIndex  as    y i
-    -> SIndex  bs    y (InsertIndex as bs x y ins i)
+sInsertIndex ::
+  SInsert as bs x ins ->
+  SIndex as y i ->
+  SIndex bs y (InsertIndex as bs x y ins i)
 sInsertIndex = \case
-    SInsZ     -> SIS
-    SInsS ins -> \case
-      SIZ   -> SIZ
-      SIS i -> SIS (sInsertIndex ins i)
+  SInsZ -> SIS
+  SInsS ins -> \case
+    SIZ -> SIZ
+    SIS i -> SIS (sInsertIndex ins i)
 
 -- | Helper type family for the implementation of 'DeleteIndex', to get
 -- around the lack of case statements at the type level.
-type family SuccDeletedIx (b :: k) (bs :: [k]) (x :: k) (y :: k) (del :: DeletedIx bs x y) :: DeletedIx (b ': bs) x y where
-    SuccDeletedIx b bs x x 'GotDeleted = 'GotDeleted
-    SuccDeletedIx b bs x y ('NotDeleted i) = 'NotDeleted ('IS i)
+type family
+  SuccDeletedIx (b :: k) (bs :: [k]) (x :: k) (y :: k) (del :: DeletedIx bs x y) ::
+    DeletedIx (b ': bs) x y
+  where
+  SuccDeletedIx b bs x x 'GotDeleted = 'GotDeleted
+  SuccDeletedIx b bs x y ('NotDeleted i) = 'NotDeleted ('IS i)
 
 -- | Type-level version of 'deleteIndex'.  Because of how GADTs and type
 -- families interact, the type-level lists and kinds of the insertion and
 -- index must be provided.
-type family DeleteIndex (as :: [k]) (bs :: [k]) (x :: k) (y :: k) (del :: Delete as bs x) (i :: Index as y) :: DeletedIx bs x y where
-    DeleteIndex (x ': bs) bs         x x 'DelZ       'IZ     = 'GotDeleted
-    DeleteIndex (x ': bs) bs         x y 'DelZ       ('IS i) = 'NotDeleted i
-    DeleteIndex (y ': as) (y ': bs)  x y ('DelS del) 'IZ     = 'NotDeleted 'IZ
-    DeleteIndex (b ': as) (b ': bs)  x y ('DelS del) ('IS i) = SuccDeletedIx b bs x y (DeleteIndex as bs x y del i)
+type family
+  DeleteIndex (as :: [k]) (bs :: [k]) (x :: k) (y :: k) (del :: Delete as bs x) (i :: Index as y) ::
+    DeletedIx bs x y
+  where
+  DeleteIndex (x ': bs) bs x x 'DelZ 'IZ = 'GotDeleted
+  DeleteIndex (x ': bs) bs x y 'DelZ ('IS i) = 'NotDeleted i
+  DeleteIndex (y ': as) (y ': bs) x y ('DelS del) 'IZ = 'NotDeleted 'IZ
+  DeleteIndex (b ': as) (b ': bs) x y ('DelS del) ('IS i) =
+    SuccDeletedIx b bs x y (DeleteIndex as bs x y del i)
 
 -- | Defunctionalization symbol for 'DeleteIndex', expecting only the kind
 -- variables.
@@ -650,38 +692,52 @@
 
 -- | Kind-indexed singleton for 'DeletedIx'.
 data SDeletedIx (bs :: [k]) (x :: k) (y :: k) :: DeletedIx bs x y -> Type where
-    SGotDeleted :: SDeletedIx bs x x 'GotDeleted
-    SNotDeleted :: SIndex bs y i -> SDeletedIx bs x y ('NotDeleted i)
+  SGotDeleted :: SDeletedIx bs x x 'GotDeleted
+  SNotDeleted :: SIndex bs y i -> SDeletedIx bs x y ('NotDeleted i)
 
 -- | Singleton witness for 'DeleteIndex'.
-sDeleteIndex
-    :: SDelete as bs x del
-    -> SIndex  as    y i
-    -> SDeletedIx bs x y (DeleteIndex as bs x y del i)
+sDeleteIndex ::
+  SDelete as bs x del ->
+  SIndex as y i ->
+  SDeletedIx bs x y (DeleteIndex as bs x y del i)
 sDeleteIndex = \case
-    SDelZ -> \case
-      SIZ   -> SGotDeleted
-      SIS i -> SNotDeleted i
-    SDelS del -> \case
-      SIZ   -> SNotDeleted SIZ
-      SIS i -> case sDeleteIndex del i of
-        SGotDeleted   -> SGotDeleted
-        SNotDeleted j -> SNotDeleted (SIS j)
+  SDelZ -> \case
+    SIZ -> SGotDeleted
+    SIS i -> SNotDeleted i
+  SDelS del -> \case
+    SIZ -> SNotDeleted SIZ
+    SIS i -> case sDeleteIndex del i of
+      SGotDeleted -> SGotDeleted
+      SNotDeleted j -> SNotDeleted (SIS j)
 
 -- | Helper type family for the implementation of 'SubstituteIndex', to get
 -- around the lack of case statements at the type level.
-type family SuccSubstitutedIx (b :: k) (bs :: [k]) (x :: k) (y :: k) (z :: k) (s :: SubstitutedIx bs x y z) :: SubstitutedIx (b ': bs) x y z where
-    SuccSubstitutedIx b bs x y x ('GotSubbed i) = 'GotSubbed ('IS i)
-    SuccSubstitutedIx b bs x y z ('NotSubbed i) = 'NotSubbed ('IS i)
+type family
+  SuccSubstitutedIx (b :: k) (bs :: [k]) (x :: k) (y :: k) (z :: k) (s :: SubstitutedIx bs x y z) ::
+    SubstitutedIx (b ': bs) x y z
+  where
+  SuccSubstitutedIx b bs x y x ('GotSubbed i) = 'GotSubbed ('IS i)
+  SuccSubstitutedIx b bs x y z ('NotSubbed i) = 'NotSubbed ('IS i)
 
 -- | Type-level version of 'substituteIndex'.  Because of how GADTs and
 -- type families interact, the type-level lists and kinds of the insertion
 -- and index must be provided.
-type family SubstituteIndex (as :: [k]) (bs :: [k]) (x :: k) (y :: k) (z :: k) (s :: Substitute as bs x y) (i :: Index as z) :: SubstitutedIx bs x y z where
-    SubstituteIndex (z ': as) (y ': as) z y z 'SubZ     'IZ     = 'GotSubbed 'IZ
-    SubstituteIndex (x ': as) (y ': as) x y z 'SubZ     ('IS i) = 'NotSubbed ('IS i)
-    SubstituteIndex (z ': as) (z ': bs) x y z ('SubS s) 'IZ     = 'NotSubbed 'IZ
-    SubstituteIndex (b ': as) (b ': bs) x y z ('SubS s) ('IS i) = SuccSubstitutedIx b bs x y z (SubstituteIndex as bs x y z s i)
+type family
+  SubstituteIndex
+    (as :: [k])
+    (bs :: [k])
+    (x :: k)
+    (y :: k)
+    (z :: k)
+    (s :: Substitute as bs x y)
+    (i :: Index as z) ::
+    SubstitutedIx bs x y z
+  where
+  SubstituteIndex (z ': as) (y ': as) z y z 'SubZ 'IZ = 'GotSubbed 'IZ
+  SubstituteIndex (x ': as) (y ': as) x y z 'SubZ ('IS i) = 'NotSubbed ('IS i)
+  SubstituteIndex (z ': as) (z ': bs) x y z ('SubS s) 'IZ = 'NotSubbed 'IZ
+  SubstituteIndex (b ': as) (b ': bs) x y z ('SubS s) ('IS i) =
+    SuccSubstitutedIx b bs x y z (SubstituteIndex as bs x y z s i)
 
 -- | Defunctionalization symbol for 'SubstituteIndex', expecting only the kind
 -- variables.
@@ -696,20 +752,20 @@
 
 -- | Kind-indexed singleton for 'SubstitutedIx'.
 data SSubstitutedIx (bs :: [k]) (x :: k) (y :: k) (z :: k) :: SubstitutedIx bs x y z -> Type where
-    SGotSubbed :: SIndex bs y i -> SSubstitutedIx bs z y z ('GotSubbed i)
-    SNotSubbed :: SIndex bs z i -> SSubstitutedIx bs x y z ('NotSubbed i)
+  SGotSubbed :: SIndex bs y i -> SSubstitutedIx bs z y z ('GotSubbed i)
+  SNotSubbed :: SIndex bs z i -> SSubstitutedIx bs x y z ('NotSubbed i)
 
 -- | Singleton witness for 'SubstituteIndex'.
-sSubstituteIndex
-    :: SSubstitute as bs x y s
-    -> SIndex as z i
-    -> SSubstitutedIx bs x y z (SubstituteIndex as bs x y z s i)
+sSubstituteIndex ::
+  SSubstitute as bs x y s ->
+  SIndex as z i ->
+  SSubstitutedIx bs x y z (SubstituteIndex as bs x y z s i)
 sSubstituteIndex = \case
-    SSubZ -> \case
-      SIZ   -> SGotSubbed SIZ
-      SIS i -> SNotSubbed (SIS i)
-    SSubS s -> \case
-      SIZ   -> SNotSubbed SIZ
-      SIS i -> case sSubstituteIndex s i of
-        SGotSubbed j -> SGotSubbed (SIS j)
-        SNotSubbed j -> SNotSubbed (SIS j)
+  SSubZ -> \case
+    SIZ -> SGotSubbed SIZ
+    SIS i -> SNotSubbed (SIS i)
+  SSubS s -> \case
+    SIZ -> SNotSubbed SIZ
+    SIS i -> case sSubstituteIndex s i of
+      SGotSubbed j -> SGotSubbed (SIS j)
+      SNotSubbed j -> SNotSubbed (SIS j)
diff --git a/src/Data/Type/List/Sublist.hs b/src/Data/Type/List/Sublist.hs
--- a/src/Data/Type/List/Sublist.hs
+++ b/src/Data/Type/List/Sublist.hs
@@ -1,19 +1,19 @@
-{-# LANGUAGE EmptyCase             #-}
-{-# LANGUAGE FlexibleContexts      #-}
-{-# LANGUAGE FlexibleInstances     #-}
-{-# LANGUAGE GADTs                 #-}
-{-# LANGUAGE KindSignatures        #-}
-{-# LANGUAGE LambdaCase            #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE PatternSynonyms       #-}
-{-# LANGUAGE RankNTypes            #-}
-{-# LANGUAGE ScopedTypeVariables   #-}
-{-# LANGUAGE StandaloneDeriving    #-}
-{-# LANGUAGE TupleSections         #-}
-{-# LANGUAGE TypeApplications      #-}
-{-# LANGUAGE TypeInType            #-}
-{-# LANGUAGE TypeOperators         #-}
-{-# LANGUAGE ViewPatterns          #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ViewPatterns #-}
 
 -- |
 -- Module      : Data.Type.List.Sublist
@@ -27,67 +27,112 @@
 -- Witnesses regarding sublists of lists.
 module Data.Type.List.Sublist (
   -- * Prefix and Suffix
+
   -- ** Prefix
-    Prefix(..), IsPrefix, autoPrefix
-  , takeRec, prefixLens, takeIndex, weakenIndex
-  , prefixShape
+  Prefix (..),
+  IsPrefix,
+  autoPrefix,
+  takeRec,
+  prefixLens,
+  takeIndex,
+  weakenIndex,
+  prefixShape,
+
   -- ** Suffix
-  , Suffix(..), IsSuffix, autoSuffix
-  , dropRec, suffixLens, dropIndex, shiftIndex
+  Suffix (..),
+  IsSuffix,
+  autoSuffix,
+  dropRec,
+  suffixLens,
+  dropIndex,
+  shiftIndex,
+
   -- * Append
-  , Append(..), IsAppend, autoAppend, withAppend
-  , prefixToAppend, suffixToAppend
-  , appendToPrefix, appendToSuffix, splitAppend
-  , appendShape
+  Append (..),
+  IsAppend,
+  autoAppend,
+  withAppend,
+  prefixToAppend,
+  suffixToAppend,
+  appendToPrefix,
+  appendToSuffix,
+  splitAppend,
+  appendShape,
+
   -- ** Application
-  , splitRec, appendRec, splitRecIso
-  , splitIndex
+  splitRec,
+  appendRec,
+  splitRecIso,
+  splitIndex,
+
   -- ** Witnesses
+
   -- *** Singletons
-  , pattern AppendWit
-  , appendWit, implyAppend, unAppendWit
+  pattern AppendWit,
+  appendWit,
+  implyAppend,
+  unAppendWit,
+
   -- *** Vinyl
-  , pattern AppendWitV
-  , appendWitV, implyAppendV, unAppendWitV
+  pattern AppendWitV,
+  appendWitV,
+  implyAppendV,
+  unAppendWitV,
+
   -- *** Both
-  , pattern AppendWit'
-  , convertAppends
-  , AppendedTo
+  pattern AppendWit',
+  convertAppends,
+  AppendedTo,
+
   -- * Interleave
-  , Interleave(..), IsInterleave, autoInterleave
-  , interleaveRec, unweaveRec, interleaveRecIso
-  , injectIndexL, injectIndexR, unweaveIndex
-  , interleavedIxes, swapInterleave
-  , interleaveShapes
+  Interleave (..),
+  IsInterleave,
+  autoInterleave,
+  interleaveRec,
+  unweaveRec,
+  interleaveRecIso,
+  injectIndexL,
+  injectIndexR,
+  unweaveIndex,
+  interleavedIxes,
+  swapInterleave,
+  interleaveShapes,
+
   -- * Subset
-  , Subset(..), IsSubset, autoSubset
-  , subsetComplement
-  , interleaveRToSubset, interleaveLToSubset
-  , subsetToInterleaveL, subsetToInterleaveR
-  , subsetRec, getSubset
-  , subsetShapes
-  , subsetIxes
-  , weakenSubsetIndex, strengthenSubsetIndex
-  ) where
+  Subset (..),
+  IsSubset,
+  autoSubset,
+  subsetComplement,
+  interleaveRToSubset,
+  interleaveLToSubset,
+  subsetToInterleaveL,
+  subsetToInterleaveR,
+  subsetRec,
+  getSubset,
+  subsetShapes,
+  subsetIxes,
+  weakenSubsetIndex,
+  strengthenSubsetIndex,
+) where
 
-import           Data.Bifunctor
-import           Data.Functor.Compose
-import           Data.Kind
-import           Data.List.Singletons (SList(..), type (++))
-import           Data.Profunctor
-import           Data.Singletons
-import           Data.Singletons.Decide
-import           Data.Singletons.Sigma
-import           Data.Type.Functor.Product
-import           Data.Type.Predicate
-import           Data.Type.Predicate.Auto
-import           Data.Type.Predicate.Param
-import           Data.Vinyl hiding            ((:~:))
-import           GHC.Generics                 ((:+:)(..))
-import           Lens.Micro hiding            ((%~))
-import           Lens.Micro.Extras
-import qualified Data.Vinyl.Recursive         as VR
-import qualified Data.Vinyl.TypeLevel         as V
+import Data.Bifunctor
+import Data.Functor.Compose
+import Data.Kind
+import Data.List.Singletons (SList (..), type (++))
+import Data.Profunctor
+import Data.Singletons
+import Data.Singletons.Decide
+import Data.Singletons.Sigma
+import Data.Type.Functor.Product
+import Data.Type.Predicate
+import Data.Type.Predicate.Auto
+import Data.Type.Predicate.Param
+import Data.Vinyl hiding ((:~:))
+import qualified Data.Vinyl.Recursive as VR
+import qualified Data.Vinyl.TypeLevel as V
+import GHC.Generics ((:+:) (..))
+import Lens.Micro hiding ((%~))
+import Lens.Micro.Extras
 
 -- | A @'Prefix' as bs@ witnesses that @as@ is a prefix of @bs@.
 --
@@ -106,8 +151,8 @@
 -- This is essentially the first half of an 'Append', but is conceptually
 -- easier to work with.
 data Prefix :: [k] -> [k] -> Type where
-    PreZ :: Prefix '[] as
-    PreS :: Prefix  as bs -> Prefix  (a ': as) (a ': bs)
+  PreZ :: Prefix '[] as
+  PreS :: Prefix as bs -> Prefix (a ': as) (a ': bs)
 
 deriving instance Show (Prefix as bs)
 
@@ -125,23 +170,23 @@
 type IsPrefix as = TyPred (Prefix as)
 
 instance Auto (IsPrefix '[]) bs where
-    auto = PreZ
+  auto = PreZ
 
 instance Auto (IsPrefix as) bs => Auto (IsPrefix (a ': as)) (a ': bs) where
-    auto = PreS (auto @_ @(IsPrefix as) @bs)
+  auto = PreS (auto @_ @(IsPrefix as) @bs)
 
 instance (SDecide k, SingI (as :: [k])) => Decidable (IsPrefix as) where
-    decide = case sing @as of
-      SNil         -> \_ -> Proved PreZ
-      x `SCons` (Sing :: Sing as') -> \case
-        SNil -> Disproved $ \case {}
-        y `SCons` (ys :: Sing bs') -> case x %~ y of
-          Proved Refl -> case decide @(IsPrefix as') ys of
-            Proved p -> Proved (PreS p)
-            Disproved v -> Disproved $ \case
-              PreS p -> v p
+  decide = case sing @as of
+    SNil -> \_ -> Proved PreZ
+    x `SCons` (Sing :: Sing as') -> \case
+      SNil -> Disproved $ \case {}
+      y `SCons` (ys :: Sing bs') -> case x %~ y of
+        Proved Refl -> case decide @(IsPrefix as') ys of
+          Proved p -> Proved (PreS p)
           Disproved v -> Disproved $ \case
-            PreS _ -> v Refl
+            PreS p -> v p
+        Disproved v -> Disproved $ \case
+          PreS _ -> v Refl
 
 -- | Automatically generate a 'Prefix' if @as@ and @bs@ are known
 -- statically.
@@ -153,12 +198,12 @@
 -- | Get the 'Shape' associated with a 'Prefix'.
 --
 -- @since 0.1.3.0
-prefixShape
-    :: Prefix as bs
-    -> Shape [] as
+prefixShape ::
+  Prefix as bs ->
+  Shape [] as
 prefixShape = \case
-    PreZ   -> RNil
-    PreS p -> Proxy :& prefixShape p
+  PreZ -> RNil
+  PreS p -> Proxy :& prefixShape p
 
 -- | A @'Suffix' as bs@ witnesses that @as@ is a suffix of @bs@.
 --
@@ -177,8 +222,8 @@
 -- This is essentially the second half of an 'Append', but is conceptually
 -- easier to work with.
 data Suffix :: [k] -> [k] -> Type where
-    SufZ :: Suffix as as
-    SufS :: Suffix as bs -> Suffix as (b ': bs)
+  SufZ :: Suffix as as
+  SufS :: Suffix as bs -> Suffix as (b ': bs)
 
 deriving instance Show (Suffix as bs)
 
@@ -188,24 +233,24 @@
 type IsSuffix as = TyPred (Suffix as)
 
 instance Auto (IsSuffix '[]) '[] where
-    auto = SufZ
+  auto = SufZ
 
 instance {-# OVERLAPPABLE #-} Auto (IsSuffix (a ': as)) (a ': as) where
-    auto = SufZ
+  auto = SufZ
 
 instance {-# OVERLAPPABLE #-} Auto (IsSuffix as) bs => Auto (IsSuffix as) (b ': bs) where
-    auto = SufS (auto @_ @(IsSuffix as) @bs)
+  auto = SufS (auto @_ @(IsSuffix as) @bs)
 
 instance (SDecide k, SingI (as :: [k])) => Decidable (IsSuffix as) where
-    decide = \case
-      SNil -> case sing @as of
-        SNil -> Proved SufZ
-        _ `SCons` _ -> Disproved $ \case {}
-      _ `SCons` ys -> case decide @(IsSuffix as) ys of
-        Proved s    -> Proved $ SufS s
-        Disproved v -> Disproved $ \case
-          SufZ   -> error "help me"
-          SufS s -> v s
+  decide = \case
+    SNil -> case sing @as of
+      SNil -> Proved SufZ
+      _ `SCons` _ -> Disproved $ \case {}
+    _ `SCons` ys -> case decide @(IsSuffix as) ys of
+      Proved s -> Proved $ SufS s
+      Disproved v -> Disproved $ \case
+        SufZ -> error "help me"
+        SufS s -> v s
 
 -- | Automatically generate a 'Suffix' if @as@ and @bs@ are known
 -- statically.
@@ -238,8 +283,8 @@
 --
 -- This basically combines 'Prefix' and 'Suffix'.
 data Append :: [k] -> [k] -> [k] -> Type where
-    AppZ :: Append '[] as as
-    AppS :: Append as bs cs -> Append (a ': as) bs (a ': cs)
+  AppZ :: Append '[] as as
+  AppS :: Append as bs cs -> Append (a ': as) bs (a ': cs)
 
 deriving instance Show (Append as bs cs)
 
@@ -265,30 +310,30 @@
 type AppendedTo as = TyPP (Append as)
 
 instance Auto (IsAppend '[] as) as where
-    auto = AppZ
+  auto = AppZ
 
 instance Auto (IsAppend as bs) cs => Auto (IsAppend (a ': as) bs) (a ': cs) where
-    auto = AppS (auto @_ @(IsAppend as bs) @cs)
+  auto = AppS (auto @_ @(IsAppend as bs) @cs)
 
 instance (SDecide k, SingI (as :: [k]), SingI bs) => Decidable (IsAppend as bs) where
-    decide = case sing @as of
-      SNil         -> \cs -> case sing @bs %~ cs of
-        Proved Refl -> Proved AppZ
-        Disproved v -> Disproved $ \case
-          AppZ -> v Refl
-      x `SCons` (Sing :: Sing as') -> \case
-        SNil -> Disproved $ \case {}
-        y `SCons` (ys :: Sing bs') -> case x %~ y of
-          Proved Refl -> case decide @(IsAppend as' bs) ys of
-            Proved p -> Proved (AppS p)
-            Disproved v -> Disproved $ \case
-              AppS p -> v p
+  decide = case sing @as of
+    SNil -> \cs -> case sing @bs %~ cs of
+      Proved Refl -> Proved AppZ
+      Disproved v -> Disproved $ \case
+        AppZ -> v Refl
+    x `SCons` (Sing :: Sing as') -> \case
+      SNil -> Disproved $ \case {}
+      y `SCons` (ys :: Sing bs') -> case x %~ y of
+        Proved Refl -> case decide @(IsAppend as' bs) ys of
+          Proved p -> Proved (AppS p)
           Disproved v -> Disproved $ \case
-            AppS _ -> v Refl
+            AppS p -> v p
+        Disproved v -> Disproved $ \case
+          AppS _ -> v Refl
 
 instance SingI as => Decidable (Found (AppendedTo as))
 instance SingI as => Provable (Found (AppendedTo as)) where
-    prove ys = withAppend (singProd (sing @as)) (singProd ys) $ \s x -> prodSing s :&: x
+  prove ys = withAppend (singProd (sing @as)) (singProd ys) $ \s x -> prodSing s :&: x
 
 -- | Automatically generate an 'Append' if @as@, @bs@ and @cs@ are known
 -- statically.
@@ -303,23 +348,23 @@
 -- @since 0.1.2.0
 appendWit :: Append as bs cs -> (as ++ bs) :~: cs
 appendWit = \case
-    AppZ   -> Refl
-    AppS a -> case appendWit a of
-      Refl -> Refl
+  AppZ -> Refl
+  AppS a -> case appendWit a of
+    Refl -> Refl
 
 -- | The inverse of 'appendWit': if we know @(as ++ bs) ~ cs@ (using @++@
 -- from "Data.Singletons.Prelude.List"), we can create an @'Append' as bs
 -- cs@ given structure witnesses 'Sing'.
 --
 -- @since 0.1.2.0
-unAppendWit
-    :: (as ++ bs) ~ cs
-    => Rec f as
-    -> Rec f bs
-    -> Append as bs cs
+unAppendWit ::
+  (as ++ bs) ~ cs =>
+  Rec f as ->
+  Rec f bs ->
+  Append as bs cs
 unAppendWit = \case
-    RNil    -> \_   -> AppZ
-    _ :& xs -> AppS . unAppendWit xs
+  RNil -> \_ -> AppZ
+  _ :& xs -> AppS . unAppendWit xs
 
 -- | A useful pattern synonym for using 'Append' with @++@ from
 -- "Data.Singletons.Prelude.List".
@@ -331,10 +376,12 @@
 -- you have @(as ++ bs) ~ cs@ in the context.
 --
 -- @since 0.1.2.0
-pattern AppendWit :: forall as bs cs. (RecApplicative as, RecApplicative bs) => (as ++ bs) ~ cs => Append as bs cs
+pattern AppendWit ::
+  forall as bs cs. (RecApplicative as, RecApplicative bs) => (as ++ bs) ~ cs => Append as bs cs
 pattern AppendWit <- (appendWit @as @bs @cs -> Refl)
   where
     AppendWit = unAppendWit @as @bs @cs pureShape pureShape
+
 {-# COMPLETE AppendWit #-}
 
 -- | 'appendWit' stated as a 'Predicate' implication.
@@ -349,23 +396,23 @@
 -- @since 0.1.2.0
 appendWitV :: Append as bs cs -> (as V.++ bs) :~: cs
 appendWitV = \case
-    AppZ -> Refl
-    AppS a -> case appendWitV a of
-      Refl -> Refl
+  AppZ -> Refl
+  AppS a -> case appendWitV a of
+    Refl -> Refl
 
 -- | The inverse of 'appendWitV': if we know @(as ++ bs) ~ cs@ (using @++@
 -- from "Data.Vinyl.TypeLevel"), we can create an @'Append' as bs cs@ given
 -- structure witnesses 'Sing'.
 --
 -- @since 0.1.2.0
-unAppendWitV
-    :: (as V.++ bs) ~ cs
-    => Rec f as
-    -> Rec f bs
-    -> Append as bs cs
+unAppendWitV ::
+  (as V.++ bs) ~ cs =>
+  Rec f as ->
+  Rec f bs ->
+  Append as bs cs
 unAppendWitV = \case
-    RNil     -> \_   -> AppZ
-    _ :& xs -> AppS . unAppendWitV xs
+  RNil -> \_ -> AppZ
+  _ :& xs -> AppS . unAppendWitV xs
 
 -- | A useful pattern synonym for using 'Append' with @++@ from
 -- "Data.Vinyl.TypeLevel".
@@ -377,10 +424,12 @@
 -- you have @(as ++ bs) ~ cs@ in the context.
 --
 -- @since 0.1.2.0
-pattern AppendWitV :: forall as bs cs. (RecApplicative as, RecApplicative bs) => (as V.++ bs) ~ cs => Append as bs cs
+pattern AppendWitV ::
+  forall as bs cs. (RecApplicative as, RecApplicative bs) => (as V.++ bs) ~ cs => Append as bs cs
 pattern AppendWitV <- (appendWitV @as @bs @cs -> Refl)
   where
     AppendWitV = unAppendWitV @as @bs @cs pureShape pureShape
+
 {-# COMPLETE AppendWitV #-}
 
 -- | Combine the powers of 'AppendWit' and 'AppendWitV' by matching on an
@@ -390,10 +439,15 @@
 -- by transitive property.
 --
 -- @since 0.1.2.0
-pattern AppendWit' :: forall as bs cs. (RecApplicative as, RecApplicative bs) => ((as ++ bs) ~ cs, (as V.++ bs) ~ cs) => Append as bs cs
-pattern AppendWit' <- ((\a -> (a,a)) -> (AppendWit, AppendWitV))
+pattern AppendWit' ::
+  forall as bs cs.
+  (RecApplicative as, RecApplicative bs) =>
+  ((as ++ bs) ~ cs, (as V.++ bs) ~ cs) =>
+  Append as bs cs
+pattern AppendWit' <- ((\a -> (a, a)) -> (AppendWit, AppendWitV))
   where
     AppendWit' = AppendWit
+
 {-# COMPLETE AppendWitV #-}
 
 -- | 'appendWitV' stated as a 'Predicate' implication.
@@ -407,26 +461,26 @@
 -- "Data.Vinyl.TypeLevel".
 convertAppends :: Append as bs cs -> (as ++ bs) :~: (as V.++ bs)
 convertAppends a = case appendWit a of
-    Refl -> case appendWitV a of
-      Refl -> Refl
+  Refl -> case appendWitV a of
+    Refl -> Refl
 
 -- | Given @as@ and @bs@, create an @'Append' as bs cs@ with, with @cs@
 -- existentially quantified
 withAppend :: Rec f as -> Rec f bs -> (forall cs. Rec f cs -> Append as bs cs -> r) -> r
 withAppend = \case
-    RNil -> \ys f -> f ys AppZ
-    x :& xs -> \ys f -> withAppend xs ys $ \zs a ->
-      f (x :& zs) (AppS a)
+  RNil -> \ys f -> f ys AppZ
+  x :& xs -> \ys f -> withAppend xs ys $ \zs a ->
+    f (x :& zs) (AppS a)
 
 -- | Get the 'Shape' associated with an 'Append''s prefix.
 --
 -- @since 0.1.3.0
-appendShape
-    :: Append as bs cs
-    -> Shape [] as
+appendShape ::
+  Append as bs cs ->
+  Shape [] as
 appendShape = \case
-    AppZ   -> RNil
-    AppS a -> Proxy :& appendShape a
+  AppZ -> RNil
+  AppS a -> Proxy :& appendShape a
 
 -- | Witness an isomorphism between 'Rec' and two parts that compose it.
 --
@@ -441,137 +495,141 @@
 -- This can be used with the combinators from the lens library.
 --
 -- The 'Append' tells the point to split the 'Rec' at.
-splitRecIso
-    :: (Profunctor p, Functor f)
-    => Append as bs cs
-    -> p (Rec g as, Rec g bs) (f (Rec g as, Rec g bs))
-    -> p (Rec g cs)           (f (Rec g cs))
+splitRecIso ::
+  (Profunctor p, Functor f) =>
+  Append as bs cs ->
+  p (Rec g as, Rec g bs) (f (Rec g as, Rec g bs)) ->
+  p (Rec g cs) (f (Rec g cs))
 splitRecIso a = dimap (splitRec a) ((fmap . uncurry) (appendRec a))
 
 -- | Split a 'Rec' into a prefix and suffix.  Basically 'takeRec'
 -- and 'dropRec' combined.
-splitRec
-    :: Append as bs cs
-    -> Rec f cs
-    -> (Rec f as, Rec f bs)
+splitRec ::
+  Append as bs cs ->
+  Rec f cs ->
+  (Rec f as, Rec f bs)
 splitRec = \case
-    AppZ   -> (RNil,)
-    AppS a -> \case
-      x :& xs -> first (x :&) . splitRec a $ xs
+  AppZ -> (RNil,)
+  AppS a -> \case
+    x :& xs -> first (x :&) . splitRec a $ xs
 
 -- | Append two 'Rec's together according to an 'Append'.
-appendRec
-    :: Append as bs cs
-    -> Rec f as
-    -> Rec f bs
-    -> Rec f cs
+appendRec ::
+  Append as bs cs ->
+  Rec f as ->
+  Rec f bs ->
+  Rec f cs
 appendRec = \case
-    AppZ   -> \_ -> id
-    AppS a -> \case
-      x :& xs -> (x :&) . appendRec a xs
+  AppZ -> \_ -> id
+  AppS a -> \case
+    x :& xs -> (x :&) . appendRec a xs
 
 -- | Convert a 'Prefix' to an 'Append', with an existential @bs@.
-prefixToAppend
-    :: Prefix as cs
-    -> (forall bs. Append as bs cs -> r)
-    -> r
+prefixToAppend ::
+  Prefix as cs ->
+  (forall bs. Append as bs cs -> r) ->
+  r
 prefixToAppend = \case
-    PreZ   -> ($ AppZ)
-    PreS p -> \f -> prefixToAppend p (f . AppS)
+  PreZ -> ($ AppZ)
+  PreS p -> \f -> prefixToAppend p (f . AppS)
 
 -- | Convert a 'Suffix' to an 'Append', with an existential @as@.
-suffixToAppend
-    :: Suffix bs cs
-    -> (forall as. Append as bs cs -> r)
-    -> r
+suffixToAppend ::
+  Suffix bs cs ->
+  (forall as. Append as bs cs -> r) ->
+  r
 suffixToAppend = \case
-    SufZ   -> ($ AppZ)
-    SufS s -> \f -> suffixToAppend s (f . AppS)
+  SufZ -> ($ AppZ)
+  SufS s -> \f -> suffixToAppend s (f . AppS)
 
 -- | Split an 'Append' into a 'Prefix' and 'Suffix'.  Basically
 -- 'appendToPrefix' and 'appendToSuffix' at the same time.
-splitAppend
-    :: Append as bs cs
-    -> (Prefix as cs, Suffix bs cs)
+splitAppend ::
+  Append as bs cs ->
+  (Prefix as cs, Suffix bs cs)
 splitAppend = \case
-    AppZ   -> (PreZ, SufZ)
-    AppS a -> bimap PreS SufS . splitAppend $ a
+  AppZ -> (PreZ, SufZ)
+  AppS a -> bimap PreS SufS . splitAppend $ a
 
 -- | Convert an 'Append' to a 'Prefix', forgetting the suffix.
 appendToPrefix :: Append as bs cs -> Prefix as cs
 appendToPrefix = \case
-    AppZ   -> PreZ
-    AppS a -> PreS . appendToPrefix $ a
+  AppZ -> PreZ
+  AppS a -> PreS . appendToPrefix $ a
 
 -- | Convert an 'Append' to a 'Suffix', forgetting the prefix
 appendToSuffix :: Append as bs cs -> Suffix bs cs
 appendToSuffix = \case
-    AppZ   -> SufZ
-    AppS a -> SufS . appendToSuffix $ a
+  AppZ -> SufZ
+  AppS a -> SufS . appendToSuffix $ a
 
 -- | Split an 'Index' by an 'Append'.  If the 'Index' was in the first part
 -- of the list, it'll return 'Left'.  If it was in the second part, it'll
 -- return 'Right'.
 --
 -- This is essentially 'takeIndex' and 'dropIndex' at the same time.
-splitIndex
-    :: Append as bs cs
-    -> Index cs x
-    -> Either (Index as x) (Index bs x)
+splitIndex ::
+  Append as bs cs ->
+  Index cs x ->
+  Either (Index as x) (Index bs x)
 splitIndex = \case
-    AppZ   -> Right
-    AppS a -> \case
-      IZ   -> Left IZ
-      IS i -> first IS . splitIndex a $ i
+  AppZ -> Right
+  AppS a -> \case
+    IZ -> Left IZ
+    IS i -> first IS . splitIndex a $ i
 
 -- | Shave off the final inhabitants of an 'Index', keeping only indices
 -- a part of a given prefix.  If the index is out of range, 'Nothing' will
 -- be returned.
 --
 -- This is essentially 'splitIndex', but taking only 'Left' results.
-takeIndex
-    :: Prefix as bs
-    -> Index bs x
-    -> Maybe (Index as x)
-takeIndex p i = prefixToAppend p $ either Just (const Nothing)
-                                 . (`splitIndex` i)
+takeIndex ::
+  Prefix as bs ->
+  Index bs x ->
+  Maybe (Index as x)
+takeIndex p i =
+  prefixToAppend p $
+    either Just (const Nothing)
+      . (`splitIndex` i)
 
 -- | Shave off the initial inhabitants of an 'Index', keeping only indices
 -- a part of a given suffix  If the index is out of range, 'Nothing' will
 -- be returned.
 --
 -- This is essentially 'splitIndex', but taking only 'Right' results.
-dropIndex
-    :: Suffix as bs
-    -> Index bs x
-    -> Maybe (Index as x)
-dropIndex s i = suffixToAppend s $ either (const Nothing) Just
-                                 . (`splitIndex` i)
+dropIndex ::
+  Suffix as bs ->
+  Index bs x ->
+  Maybe (Index as x)
+dropIndex s i =
+  suffixToAppend s $
+    either (const Nothing) Just
+      . (`splitIndex` i)
 
 -- | An index pointing to a given item in a prefix is also an index
 -- pointing to the same item in the full list.  This "weakens" the bounds
 -- of an index, widening the list at the end but preserving the original
 -- index.  This is the inverse of 'takeIndex'.
-weakenIndex
-    :: Prefix as bs
-    -> Index as x
-    -> Index bs x
+weakenIndex ::
+  Prefix as bs ->
+  Index as x ->
+  Index bs x
 weakenIndex = \case
-    PreZ   -> \case {}
-    PreS p -> \case
-      IZ   -> IZ
-      IS i -> IS (weakenIndex p i)
+  PreZ -> \case {}
+  PreS p -> \case
+    IZ -> IZ
+    IS i -> IS (weakenIndex p i)
 
 -- | An index pointing to a given item in a suffix can be transformed into
 -- an index pointing to the same item in the full list.  This is the
 -- inverse of 'dropIndex'.
-shiftIndex
-    :: Suffix as bs
-    -> Index as x
-    -> Index bs x
+shiftIndex ::
+  Suffix as bs ->
+  Index as x ->
+  Index bs x
 shiftIndex = \case
-    SufZ   -> id
-    SufS s -> IS . shiftIndex s
+  SufZ -> id
+  SufS s -> IS . shiftIndex s
 
 -- | A @'Interleave' as bs cs@ witnesses that @cs@ is @as@ interleaved with
 -- @bs@. It is constructed by selectively zipping items from @as@ and @bs@
@@ -591,9 +649,9 @@
 --
 -- @since 0.1.1.0
 data Interleave :: [k] -> [k] -> [k] -> Type where
-    IntZ :: Interleave '[] '[] '[]
-    IntL :: Interleave as bs cs -> Interleave (a ': as) bs        (a ': cs)
-    IntR :: Interleave as bs cs -> Interleave as        (b ': bs) (b ': cs)
+  IntZ :: Interleave '[] '[] '[]
+  IntL :: Interleave as bs cs -> Interleave (a ': as) bs (a ': cs)
+  IntR :: Interleave as bs cs -> Interleave as (b ': bs) (b ': cs)
 
 deriving instance Show (Interleave as bs cs)
 
@@ -604,63 +662,63 @@
 type IsInterleave as bs = TyPred (Interleave as bs)
 
 instance Auto (IsInterleave '[] '[]) '[] where
-    auto = IntZ
+  auto = IntZ
 
 -- | Prefers 'IntL' if there is an ambiguity.
 instance Auto (IsInterleave as bs) cs => Auto (IsInterleave (a ': as) bs) (a ': cs) where
-    auto = IntL (auto @_ @(IsInterleave as bs) @cs)
+  auto = IntL (auto @_ @(IsInterleave as bs) @cs)
 
 instance {-# INCOHERENT #-} Auto (IsInterleave as bs) cs => Auto (IsInterleave as (b ': bs)) (b ': cs) where
-    auto = IntR (auto @_ @(IsInterleave as bs) @cs)
+  auto = IntR (auto @_ @(IsInterleave as bs) @cs)
 
 instance (SDecide k, SingI (as :: [k]), SingI bs) => Decidable (IsInterleave as bs) where
-    decide = case sing @as of
-      SNil -> case sing @bs of
-        SNil -> \case
-          SNil -> Proved IntZ
-          _ `SCons` _ -> Disproved $ \case {}
-        y `SCons` (Sing :: Sing bs') -> \case
-          z `SCons` (zs :: Sing cs') -> case y %~ z of
-            Proved Refl -> case decide @(IsInterleave '[] bs') zs of
-              Proved i -> Proved $ IntR i
-              Disproved v -> Disproved $ \case
-                IntR i -> v i
+  decide = case sing @as of
+    SNil -> case sing @bs of
+      SNil -> \case
+        SNil -> Proved IntZ
+        _ `SCons` _ -> Disproved $ \case {}
+      y `SCons` (Sing :: Sing bs') -> \case
+        z `SCons` (zs :: Sing cs') -> case y %~ z of
+          Proved Refl -> case decide @(IsInterleave '[] bs') zs of
+            Proved i -> Proved $ IntR i
             Disproved v -> Disproved $ \case
-              IntR _ -> v Refl
-          SNil -> Disproved $ \case {}
-      x `SCons` (Sing :: Sing as') -> case sing @bs of
-        SNil -> \case
-          z `SCons` (zs :: Sing cs') -> case x %~ z of
-            Proved Refl -> case decide @(IsInterleave as' '[]) zs of
-              Proved i -> Proved $ IntL i
-              Disproved v -> Disproved $ \case
-                IntL i -> v i
+              IntR i -> v i
+          Disproved v -> Disproved $ \case
+            IntR _ -> v Refl
+        SNil -> Disproved $ \case {}
+    x `SCons` (Sing :: Sing as') -> case sing @bs of
+      SNil -> \case
+        z `SCons` (zs :: Sing cs') -> case x %~ z of
+          Proved Refl -> case decide @(IsInterleave as' '[]) zs of
+            Proved i -> Proved $ IntL i
             Disproved v -> Disproved $ \case
-              IntL _ -> v Refl
-          SNil -> Disproved $ \case {}
-        y `SCons` (Sing :: Sing bs') -> \case
-          SNil -> Disproved $ \case {}
-          z `SCons` (zs :: Sing cs') -> case x %~ z of
-            Proved Refl -> case decide @(IsInterleave as' bs) zs of
-              Proved i    -> Proved $ IntL i
-              Disproved v -> case y %~ z of
-                Proved Refl -> case decide @(IsInterleave as bs') zs of
-                  Proved i -> Proved $ IntR i
-                  Disproved u -> Disproved $ \case
-                    IntL i -> v i
-                    IntR i -> u i
-                Disproved u -> Disproved $ \case
-                  IntL i -> v i
-                  IntR _ -> u Refl
+              IntL i -> v i
+          Disproved v -> Disproved $ \case
+            IntL _ -> v Refl
+        SNil -> Disproved $ \case {}
+      y `SCons` (Sing :: Sing bs') -> \case
+        SNil -> Disproved $ \case {}
+        z `SCons` (zs :: Sing cs') -> case x %~ z of
+          Proved Refl -> case decide @(IsInterleave as' bs) zs of
+            Proved i -> Proved $ IntL i
             Disproved v -> case y %~ z of
               Proved Refl -> case decide @(IsInterleave as bs') zs of
                 Proved i -> Proved $ IntR i
                 Disproved u -> Disproved $ \case
-                  IntL _ -> v Refl
+                  IntL i -> v i
                   IntR i -> u i
               Disproved u -> Disproved $ \case
-                IntL _ -> v Refl
+                IntL i -> v i
                 IntR _ -> u Refl
+          Disproved v -> case y %~ z of
+            Proved Refl -> case decide @(IsInterleave as bs') zs of
+              Proved i -> Proved $ IntR i
+              Disproved u -> Disproved $ \case
+                IntL _ -> v Refl
+                IntR i -> u i
+            Disproved u -> Disproved $ \case
+              IntL _ -> v Refl
+              IntR _ -> u Refl
 
 -- | Automatically generate an 'Interleave' if @as@, @bs@, and @cs@ are
 -- known statically.
@@ -683,13 +741,13 @@
 -- @since 0.1.1.0
 interleaveRec :: Interleave as bs cs -> Rec f as -> Rec f bs -> Rec f cs
 interleaveRec = \case
-    IntZ -> \case
-      RNil -> \case
-        RNil -> RNil
-    IntL m -> \case
-      x :& xs -> \ys -> x :& interleaveRec m xs ys
-    IntR m -> \xs -> \case
-      y :& ys -> y :& interleaveRec m xs ys
+  IntZ -> \case
+    RNil -> \case
+      RNil -> RNil
+  IntL m -> \case
+    x :& xs -> \ys -> x :& interleaveRec m xs ys
+  IntR m -> \xs -> \case
+    y :& ys -> y :& interleaveRec m xs ys
 
 -- | Given a 'Rec', disinterleave it into two 'Rec's corresponding to an
 -- 'Interleave'.
@@ -697,12 +755,12 @@
 -- @since 0.1.1.0
 unweaveRec :: Interleave as bs cs -> Rec f cs -> (Rec f as, Rec f bs)
 unweaveRec = \case
-    IntZ -> \case
-      RNil -> (RNil, RNil)
-    IntL m -> \case
-      x :& xs -> first  (x :&) . unweaveRec m $ xs
-    IntR m -> \case
-      x :& xs -> second (x :&) . unweaveRec m $ xs
+  IntZ -> \case
+    RNil -> (RNil, RNil)
+  IntL m -> \case
+    x :& xs -> first (x :&) . unweaveRec m $ xs
+  IntR m -> \case
+    x :& xs -> second (x :&) . unweaveRec m $ xs
 
 -- | Turn an 'Interleave' into a 'Rec' of indices from either sublist.
 --
@@ -711,11 +769,17 @@
 -- @since 0.1.2.0
 interleavedIxes :: Interleave as bs cs -> Rec (Index as :+: Index bs) cs
 interleavedIxes = \case
-    IntZ   -> RNil
-    IntL i -> L1 IZ :& VR.rmap (\case L1 i' -> L1 (IS i'); R1 j -> R1 j)
-                               (interleavedIxes i)
-    IntR j -> R1 IZ :& VR.rmap (\case L1 i -> L1 i; R1 j' -> R1 (IS j'))
-                               (interleavedIxes j)
+  IntZ -> RNil
+  IntL i ->
+    L1 IZ
+      :& VR.rmap
+        (\case L1 i' -> L1 (IS i'); R1 j -> R1 j)
+        (interleavedIxes i)
+  IntR j ->
+    R1 IZ
+      :& VR.rmap
+        (\case L1 i -> L1 i; R1 j' -> R1 (IS j'))
+        (interleavedIxes j)
 
 -- | Interleave an 'Index' on @as@ into a full index on @cs@, which is @as@
 -- interleaved with @bs@.
@@ -723,11 +787,11 @@
 -- @since 0.1.1.0
 injectIndexL :: Interleave as bs cs -> Index as a -> Index cs a
 injectIndexL = \case
-    IntZ -> \case {}
-    IntL m -> \case
-      IZ -> IZ
-      IS i -> IS (injectIndexL m i)
-    IntR m -> IS . injectIndexL m
+  IntZ -> \case {}
+  IntL m -> \case
+    IZ -> IZ
+    IS i -> IS (injectIndexL m i)
+  IntR m -> IS . injectIndexL m
 
 -- | Interleave an 'Index' on @bs@ into a full index on @cs@, which is @as@
 -- interleaved with @bs@.
@@ -735,11 +799,11 @@
 -- @since 0.1.1.0
 injectIndexR :: Interleave as bs cs -> Index bs b -> Index cs b
 injectIndexR = \case
-    IntZ -> \case {}
-    IntL m -> IS . injectIndexR m
-    IntR m -> \case
-      IZ -> IZ
-      IS i -> IS (injectIndexR m i)
+  IntZ -> \case {}
+  IntL m -> IS . injectIndexR m
+  IntR m -> \case
+    IZ -> IZ
+    IS i -> IS (injectIndexR m i)
 
 -- | Given an index on @cs@, disinterleave it into either an index on @as@
 -- or on @bs@.
@@ -747,13 +811,13 @@
 -- @since 0.1.1.0
 unweaveIndex :: Interleave as bs cs -> Index cs c -> Either (Index as c) (Index bs c)
 unweaveIndex = \case
-    IntZ -> \case {}
-    IntL m -> \case
-      IZ   -> Left IZ
-      IS i -> first IS $ unweaveIndex m i
-    IntR m -> \case
-      IZ   -> Right IZ
-      IS i -> second IS $ unweaveIndex m i
+  IntZ -> \case {}
+  IntL m -> \case
+    IZ -> Left IZ
+    IS i -> first IS $ unweaveIndex m i
+  IntR m -> \case
+    IZ -> Right IZ
+    IS i -> second IS $ unweaveIndex m i
 
 -- | Witness an isomorphism between 'Rec' and two parts that interleave it.
 --
@@ -770,38 +834,38 @@
 -- The 'Interleave' tells how to unweave the 'Rec'.
 --
 -- @since 0.1.1.0
-interleaveRecIso
-    :: (Profunctor p, Functor f)
-    => Interleave as bs cs
-    -> p (Rec g as, Rec g bs) (f (Rec g as, Rec g bs))
-    -> p (Rec g cs)           (f (Rec g cs))
+interleaveRecIso ::
+  (Profunctor p, Functor f) =>
+  Interleave as bs cs ->
+  p (Rec g as, Rec g bs) (f (Rec g as, Rec g bs)) ->
+  p (Rec g cs) (f (Rec g cs))
 interleaveRecIso m = dimap (unweaveRec m) ((fmap . uncurry) (interleaveRec m))
 
 -- | Swap the two halves of an 'Interleave'.
 --
 -- @since 0.1.3.0
-swapInterleave
-    :: Interleave as bs cs
-    -> Interleave bs as cs
+swapInterleave ::
+  Interleave as bs cs ->
+  Interleave bs as cs
 swapInterleave = \case
-    IntZ   -> IntZ
-    IntL i -> IntR $ swapInterleave i
-    IntR i -> IntL $ swapInterleave i
+  IntZ -> IntZ
+  IntL i -> IntR $ swapInterleave i
+  IntR i -> IntL $ swapInterleave i
 
 -- | Get the 'Shape's associated with an 'Interleave'.
 --
 -- @since 0.1.3.0
-interleaveShapes
-    :: Interleave as bs cs
-    -> (Shape [] as, Shape [] bs, Shape [] cs)
+interleaveShapes ::
+  Interleave as bs cs ->
+  (Shape [] as, Shape [] bs, Shape [] cs)
 interleaveShapes = \case
-    IntZ   -> (RNil, RNil, RNil)
-    IntL i ->
-      let (as         , bs         , cs         ) = interleaveShapes i
-      in  (Proxy :& as, bs         , Proxy :& cs)
-    IntR i ->
-      let (as         , bs         , cs         ) = interleaveShapes i
-      in  (as         , Proxy :& bs, Proxy :& cs)
+  IntZ -> (RNil, RNil, RNil)
+  IntL i ->
+    let (as, bs, cs) = interleaveShapes i
+     in (Proxy :& as, bs, Proxy :& cs)
+  IntR i ->
+    let (as, bs, cs) = interleaveShapes i
+     in (as, Proxy :& bs, Proxy :& cs)
 
 -- | A @'Subset' as bs@ witnesses that @as@ is some subset of @bs@, with
 -- items in the same order.  It is constructed by specifying
@@ -823,60 +887,59 @@
 --
 -- @since 0.1.3.0
 data Subset :: [k] -> [k] -> Type where
-    SubsetNil :: Subset '[] '[]
-    SubsetNo  :: Subset as bs -> Subset as        (b ': bs)
-    SubsetYes :: Subset as bs -> Subset (a ': as) (a ': bs)
+  SubsetNil :: Subset '[] '[]
+  SubsetNo :: Subset as bs -> Subset as (b ': bs)
+  SubsetYes :: Subset as bs -> Subset (a ': as) (a ': bs)
 
 -- | Drop the right side of an 'Interleave', leaving only the left side.
 interleaveLToSubset :: Interleave as bs cs -> Subset as cs
 interleaveLToSubset = \case
-    IntZ   -> SubsetNil
-    IntL i -> SubsetYes . interleaveLToSubset $ i
-    IntR i -> SubsetNo  . interleaveLToSubset $ i
+  IntZ -> SubsetNil
+  IntL i -> SubsetYes . interleaveLToSubset $ i
+  IntR i -> SubsetNo . interleaveLToSubset $ i
 
 -- | Drop the left side of an 'Interleave', leaving only the right side.
 interleaveRToSubset :: Interleave as bs cs -> Subset bs cs
 interleaveRToSubset = \case
-    IntZ   -> SubsetNil
-    IntL i -> SubsetNo  . interleaveRToSubset $ i
-    IntR i -> SubsetYes . interleaveRToSubset $ i
+  IntZ -> SubsetNil
+  IntL i -> SubsetNo . interleaveRToSubset $ i
+  IntR i -> SubsetYes . interleaveRToSubset $ i
 
 -- | Convert a 'Subset' into an left 'Interleave', recovering the dropped
 -- items.
-subsetToInterleaveL
-    :: Subset as cs
-    -> (forall bs. Interleave as bs cs -> r)
-    -> r
+subsetToInterleaveL ::
+  Subset as cs ->
+  (forall bs. Interleave as bs cs -> r) ->
+  r
 subsetToInterleaveL = \case
-    SubsetNil   -> \f -> f IntZ
-    SubsetNo  s -> \f -> subsetToInterleaveL s (f . IntR)
-    SubsetYes s -> \f -> subsetToInterleaveL s (f . IntL)
+  SubsetNil -> \f -> f IntZ
+  SubsetNo s -> \f -> subsetToInterleaveL s (f . IntR)
+  SubsetYes s -> \f -> subsetToInterleaveL s (f . IntL)
 
 -- | Convert a 'Subset' into an right 'Interleave', recovering the dropped
 -- items.
-subsetToInterleaveR
-    :: Subset bs cs
-    -> (forall as. Interleave as bs cs -> r)
-    -> r
+subsetToInterleaveR ::
+  Subset bs cs ->
+  (forall as. Interleave as bs cs -> r) ->
+  r
 subsetToInterleaveR = \case
-    SubsetNil   -> \f -> f IntZ
-    SubsetNo  s -> \f -> subsetToInterleaveR s (f . IntL)
-    SubsetYes s -> \f -> subsetToInterleaveR s (f . IntR)
+  SubsetNil -> \f -> f IntZ
+  SubsetNo s -> \f -> subsetToInterleaveR s (f . IntL)
+  SubsetYes s -> \f -> subsetToInterleaveR s (f . IntR)
 
 -- | @as@ is a subset of @cs@; this function recovers @bs@, the subset of
 -- @cs@ that is not @as@.
-subsetComplement
-    :: Subset as cs
-    -> (forall bs. Subset bs cs -> r)
-    -> r
+subsetComplement ::
+  Subset as cs ->
+  (forall bs. Subset bs cs -> r) ->
+  r
 subsetComplement = \case
-    SubsetNil   -> \f -> f SubsetNil
-    SubsetNo  s -> \f -> subsetComplement s (f . SubsetYes)
-    SubsetYes s -> \f -> subsetComplement s (f . SubsetNo)
+  SubsetNil -> \f -> f SubsetNil
+  SubsetNo s -> \f -> subsetComplement s (f . SubsetYes)
+  SubsetYes s -> \f -> subsetComplement s (f . SubsetNo)
 
 deriving instance Show (Subset as bs)
 
-
 -- | A type-level predicate that a given list is a "superset" of @as@, in
 -- correct order
 --
@@ -884,37 +947,37 @@
 type IsSubset as = TyPred (Subset as)
 
 instance Auto (IsSubset '[]) '[] where
-    auto = SubsetNil
+  auto = SubsetNil
 
 instance {-# OVERLAPPING #-} Auto (IsSubset as) bs => Auto (IsSubset as) (b ': bs) where
-    auto = SubsetNo (auto @_ @(IsSubset as) @bs)
+  auto = SubsetNo (auto @_ @(IsSubset as) @bs)
 
 instance {-# OVERLAPPING #-} Auto (IsSubset as) bs => Auto (IsSubset (a ': as)) (a ': bs) where
-    auto = SubsetYes (auto @_ @(IsSubset as) @bs)
+  auto = SubsetYes (auto @_ @(IsSubset as) @bs)
 
 instance (SDecide k, SingI (as :: [k])) => Decidable (IsSubset as) where
-    decide = case sing @as of
-      SNil -> \case
-        SNil -> Proved SubsetNil
-        _ `SCons` ys -> case decide @(IsSubset '[]) ys of
-          Proved s    -> Proved $ SubsetNo s
-          Disproved v -> Disproved $ \case
-            SubsetNo s -> v s
-      x `SCons` (Sing :: Sing as') -> \case
-        SNil -> Disproved $ \case {}
-        y `SCons` ys -> case x %~ y of
-          Proved Refl -> case decide @(IsSubset as') ys of
-            Proved s    -> Proved $ SubsetYes s
-            Disproved v -> case decide @(IsSubset as) ys of
-              Proved s    -> Proved $ SubsetNo s
-              Disproved u -> Disproved $ \case
-                SubsetNo s  -> u s
-                SubsetYes s -> v s
+  decide = case sing @as of
+    SNil -> \case
+      SNil -> Proved SubsetNil
+      _ `SCons` ys -> case decide @(IsSubset '[]) ys of
+        Proved s -> Proved $ SubsetNo s
+        Disproved v -> Disproved $ \case
+          SubsetNo s -> v s
+    x `SCons` (Sing :: Sing as') -> \case
+      SNil -> Disproved $ \case {}
+      y `SCons` ys -> case x %~ y of
+        Proved Refl -> case decide @(IsSubset as') ys of
+          Proved s -> Proved $ SubsetYes s
           Disproved v -> case decide @(IsSubset as) ys of
-            Proved s    -> Proved $ SubsetNo s
+            Proved s -> Proved $ SubsetNo s
             Disproved u -> Disproved $ \case
-              SubsetNo s  -> u s
-              SubsetYes _ -> v Refl
+              SubsetNo s -> u s
+              SubsetYes s -> v s
+        Disproved v -> case decide @(IsSubset as) ys of
+          Proved s -> Proved $ SubsetNo s
+          Disproved u -> Disproved $ \case
+            SubsetNo s -> u s
+            SubsetYes _ -> v Refl
 
 -- | Automatically generate an 'Subset' if @as@ and @bs@ are known
 -- statically.
@@ -924,54 +987,55 @@
 -- | A lens into a subset of a record, indicated by a 'Subset'.
 subsetRec :: Subset as bs -> Lens' (Rec f bs) (Rec f as)
 subsetRec = \case
-    SubsetNil   -> id
-    SubsetNo  s -> \f -> \case
-      x :& xs -> (x :&) <$> subsetRec s f xs
-    SubsetYes s -> \f -> \case
-      x :& xs -> fmap (uncurry (:&))
-               . getCompose
-               . subsetRec s (Compose . fmap (\(y :& ys) -> (y,ys)) . f . (x :&))
-               $ xs
+  SubsetNil -> id
+  SubsetNo s -> \f -> \case
+    x :& xs -> (x :&) <$> subsetRec s f xs
+  SubsetYes s -> \f -> \case
+    x :& xs ->
+      fmap (uncurry (:&))
+        . getCompose
+        . subsetRec s (Compose . fmap (\(y :& ys) -> (y, ys)) . f . (x :&))
+        $ xs
 
 -- | Take a subset out of a 'Rec'.  An alias for @'view' ('subsetRec' s)@.
-getSubset
-    :: Subset as bs
-    -> Rec f bs
-    -> Rec f as
+getSubset ::
+  Subset as bs ->
+  Rec f bs ->
+  Rec f as
 getSubset = view . subsetRec
 
 -- | Get all of the indices of all the items in a 'Subset'.
-subsetIxes
-    :: Subset as bs
-    -> Rec (Index bs) as
+subsetIxes ::
+  Subset as bs ->
+  Rec (Index bs) as
 subsetIxes s = getSubset s . imapProd const $ sp
   where
     (_, sp) = subsetShapes s
 
 -- | Get the 'Shape's associated with a 'Subset'.
-subsetShapes
-    :: Subset as bs
-    -> (Shape [] as, Shape [] bs)
+subsetShapes ::
+  Subset as bs ->
+  (Shape [] as, Shape [] bs)
 subsetShapes = \case
-    SubsetNil    -> (RNil, RNil)
-    SubsetNo   s -> second (Proxy :&) $ subsetShapes s
-    SubsetYes  s -> bimap (Proxy :&) (Proxy :&) $ subsetShapes s
+  SubsetNil -> (RNil, RNil)
+  SubsetNo s -> second (Proxy :&) $ subsetShapes s
+  SubsetYes s -> bimap (Proxy :&) (Proxy :&) $ subsetShapes s
 
 -- | Because @as@ is a subset of @bs@, an index into @as@ should also be an
 -- index into @bs@.  This performs that transformation.
 --
 -- This is like a version of 'injectIndexL' or 'injectIndexR', for
 -- 'Subset'.
-weakenSubsetIndex
-    :: Subset as bs
-    -> Index as a
-    -> Index bs a
+weakenSubsetIndex ::
+  Subset as bs ->
+  Index as a ->
+  Index bs a
 weakenSubsetIndex = \case
-    SubsetNil   -> \case {}
-    SubsetNo  s -> IS . weakenSubsetIndex s
-    SubsetYes s -> \case
-      IZ   -> IZ
-      IS i -> IS $ weakenSubsetIndex s i
+  SubsetNil -> \case {}
+  SubsetNo s -> IS . weakenSubsetIndex s
+  SubsetYes s -> \case
+    IZ -> IZ
+    IS i -> IS $ weakenSubsetIndex s i
 
 -- | Because @as@ is a subset of @bs@, we can /sometimes/ transform an
 -- index into @bs@ into an index into @as@.  This performs that
@@ -985,15 +1049,15 @@
 -- the exact same item (positionlly) in the list, if it is possible.
 --
 -- This is like a version of 'unweaveIndex', but for 'Subset'.
-strengthenSubsetIndex
-    :: Subset as bs
-    -> Index bs a
-    -> Maybe (Index as a)
+strengthenSubsetIndex ::
+  Subset as bs ->
+  Index bs a ->
+  Maybe (Index as a)
 strengthenSubsetIndex = \case
-    SubsetNil   -> \case {}
-    SubsetNo  s -> \case
-      IZ   -> Nothing
-      IS i -> strengthenSubsetIndex s i
-    SubsetYes s -> \case
-      IZ   -> Just IZ
-      IS i -> IS <$> strengthenSubsetIndex s i
+  SubsetNil -> \case {}
+  SubsetNo s -> \case
+    IZ -> Nothing
+    IS i -> strengthenSubsetIndex s i
+  SubsetYes s -> \case
+    IZ -> Just IZ
+    IS i -> IS <$> strengthenSubsetIndex s i