list-witnesses 0.1.4.0 → 0.1.4.1

raw patch · 4 files changed

+833/−704 lines, 4 filesdep ~decidabledep ~functor-productsdep ~microlensPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: decidable, functor-products, microlens, profunctors, singletons, singletons-base, vinyl

API changes (from Hackage documentation)

Files

• CHANGELOG.md +9/−0
• list-witnesses.cabal +8/−8
• src/Data/Type/List/Edit.hs +332/−276
• src/Data/Type/List/Sublist.hs +484/−420

@@ -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 --------------- 

@@ -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

@@ -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)

@@ -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