data-diverse 1.2.0.1 → 1.2.0.2

raw patch · 7 files changed

+162/−178 lines, 7 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• README.md +4/−0
• data-diverse.cabal +1/−1
• src/Data/Diverse/Many.hs +1/−2
• src/Data/Diverse/Many/Internal.hs +93/−109
• src/Data/Diverse/TypeLevel.hs +1/−4
• src/Data/Diverse/Which/Internal.hs +62/−60
• test/Data/Diverse/ManySpec.hs +0/−2

@@ -14,6 +14,10 @@  # Changelog +* 1.2.0.2+  - Added 'insert'/'remove' for GHC < 8.2+  - Removed type functions 'UniqueMemberAt', 'MaybeUniqueMemberAt'+ * 1.2.0.1   - 'insert'/'remove' is not available in GHC 8.2 onwards. 

@@ -1,5 +1,5 @@ name:                data-diverse-version:             1.2.0.1+version:             1.2.0.2 synopsis:            Extensible records and polymorphic variants. description:         "Data.Diverse.Many" is an extensible record for any size encoded efficiently as (Seq Any).                      "Data.Diverse.Which" is a polymorphic variant of possibilities encoded as (Int, Any).

@@ -92,7 +92,6 @@     , insetAfterL     , insetAfterN -#if __GLASGOW_HASKELL__ >= 802     -- * insert single item     , insertBefore     , insertBeforeL@@ -105,7 +104,7 @@     , remove     , removeL     , removeN-#endif+     ) where  import Data.Diverse.Many.Internal

@@ -108,7 +108,6 @@     , insetAfterL     , insetAfterN -#if __GLASGOW_HASKELL__ >= 802     -- * insert single item     , insertBefore     , insertBeforeL@@ -121,7 +120,6 @@     , remove     , removeL     , removeN-#endif      ) where @@ -355,12 +353,12 @@  -- | Add an element to the right of a Many iff the field doesn't already exist. postfix'-    :: forall y xs n.-       MaybeUniqueMemberAt n y xs+    :: forall y xs.+       MaybeUniqueMember y xs     => Many xs -> y -> Many (SnocUnique xs y) postfix'(Many ls) y = if i /= 0 then Many ls else Many (ls S.|> unsafeCoerce y)   where-    i = fromInteger (natVal @n Proxy) :: Int+    i = fromInteger (natVal @(PositionOf y xs) Proxy) :: Int infixl 5 `postfix'`  -- | Infix version of 'postfix'.@@ -389,7 +387,7 @@ instance CanAppendUnique xs '[] where    append' ls _ = ls -instance ( MaybeUniqueMemberAt n y xs+instance ( MaybeUniqueMember y xs          , CanAppendUnique (SnocUnique xs y) ys          , AppendUnique (SnocUnique xs y) ys ~ AppendUnique xs (y : ys)) => CanAppendUnique xs (y ': ys) where    append' ls rs = append' (postfix' ls r) rs'@@ -443,20 +441,14 @@ --------------------------------------------------  -- | Split a Many into two, where the last type in the first Many is unique @x@-splitAfter_-    :: forall x xs n proxy.-       (KnownNat n, n ~ IndexOf x xs)-    => proxy x -> Many xs -> (Many (To x xs), Many (After x xs))-splitAfter_ _ (Many xs) = let (as, bs) = S.splitAt (i + 1) xs in (Many as, Many bs)+splitAfter_ :: forall n proxy. KnownNat n => proxy n -> S.Seq Any -> (S.Seq Any, S.Seq Any)+splitAfter_ _ xs = let (as, bs) = S.splitAt (i + 1) xs in (as, bs)   where     i = fromInteger (natVal @n Proxy) :: Int  -- | Split a Many into two, where the first type in the second Many is unique @x@-splitBefore_-    :: forall x xs n proxy.-       (KnownNat n, n ~ IndexOf x xs)-    => proxy x -> Many xs -> (Many (Before x xs), Many (From x xs))-splitBefore_ _ (Many xs) = let (as, bs) = S.splitAt i xs in (Many as, Many bs)+splitBefore_ :: forall n proxy. KnownNat n => proxy n -> S.Seq Any -> (S.Seq Any, S.Seq Any)+splitBefore_ _ xs = let (as, bs) = S.splitAt i xs in (as, bs)   where     i = fromInteger (natVal @n Proxy) :: Int @@ -465,64 +457,54 @@     :: forall x xs proxy.        (UniqueMember x xs)     => proxy x -> Many xs -> (Many (To x xs), Many (After x xs))-splitAfter _ = splitAfter_ (Proxy @x)+splitAfter _ (Many xs) = let (as, bs) = splitAfter_ (Proxy @(IndexOf x xs)) xs in (Many as, Many bs)  -- | Split a Many into two, where the first type in the second Many is unique @x@ splitBefore     :: forall x xs proxy.        (UniqueMember x xs)     => proxy x -> Many xs -> (Many (Before x xs), Many (From x xs))-splitBefore _ = splitBefore_ (Proxy @x)+splitBefore _ (Many xs) = let (as, bs) = splitBefore_ (Proxy @(IndexOf x xs)) xs in (Many as, Many bs)  -- | Split a Many into two, where the last type in the first Many is unique label @l@ splitAfterL     :: forall l xs proxy x.        (UniqueLabelMember l xs, x ~ KindAtLabel l xs)     => proxy l -> Many xs -> (Many (To x xs), Many (After x xs))-splitAfterL _ = splitAfter_ (Proxy @x)+splitAfterL _ (Many xs) = let (as, bs) = splitAfter_ (Proxy @(IndexOf x xs)) xs in (Many as, Many bs)  -- | Split a Many into two, where the first type in the second Many is unique label @l@ splitBeforeL     :: forall l xs proxy x.        (UniqueLabelMember l xs, x ~ KindAtLabel l xs)     => proxy l -> Many xs -> (Many (Before x xs), Many (From x xs))-splitBeforeL _ = splitBefore_ (Proxy @x)+splitBeforeL _ (Many xs) = let (as, bs) = splitBefore_ (Proxy @(IndexOf x xs)) xs in (Many as, Many bs)  -- | Split a Many into two, where the second Many starts at index @(n + 1)@ splitAfterN     :: forall n xs proxy.        (KnownNat n, n + 1 <= Length xs)     => proxy n -> Many xs -> (Many (ToIndex n xs), Many (AfterIndex n xs))-splitAfterN _ (Many xs) = let (as, bs) = S.splitAt (i + 1) xs in (Many as, Many bs)-  where-    i = fromInteger (natVal @n Proxy) :: Int+splitAfterN p (Many xs) = let (as, bs) = splitAfter_ p xs in (Many as, Many bs)  -- | Split a Many into two, where the second Many starts at index @n@ splitBeforeN     :: forall n xs proxy.        (KnownNat n, n + 1 <= Length xs)     => proxy n -> Many xs -> (Many (BeforeIndex n xs), Many (FromIndex n xs))-splitBeforeN _ (Many xs) = let (as, bs) = S.splitAt i xs in (Many as, Many bs)-  where-    i = fromInteger (natVal @n Proxy) :: Int+splitBeforeN p (Many xs) = let (as, bs) = splitBefore_ p xs in (Many as, Many bs)  --------------------------------------------------  -- | Insert a Many into another Many, inserting after a unique @x@-insetAfter_-    :: forall x ys xs n proxy.-       (KnownNat n, n ~ IndexOf x xs)-    => proxy x -> Many ys -> Many xs -> Many (Append (To x xs) (Append ys (After x xs)))-insetAfter_ _ (Many ys) (Many xs) = let (as, bs) = S.splitAt (i + 1) xs in Many (as S.>< ys S.>< bs)+insetAfter_ :: forall n proxy. KnownNat n => proxy n -> S.Seq Any -> S.Seq Any -> S.Seq Any+insetAfter_ _ ys xs = let (as, bs) = S.splitAt (i + 1) xs in as S.>< ys S.>< bs   where     i = fromInteger (natVal @n Proxy) :: Int  -- | Insert a Many into another Many, inserting before a unique @x@-insetBefore_-    :: forall x ys xs n proxy.-       (KnownNat n, n ~ IndexOf x xs)-    => proxy x -> Many ys -> Many xs -> Many (Append (Before x xs) (Append ys (From x xs)))-insetBefore_ _ (Many ys) (Many xs) = let (as, bs) = S.splitAt i xs in Many (as S.>< ys S.>< bs)+insetBefore_ :: forall n proxy. KnownNat n => proxy n -> S.Seq Any -> S.Seq Any -> S.Seq Any+insetBefore_ _ ys xs = let (as, bs) = S.splitAt i xs in as S.>< ys S.>< bs   where     i = fromInteger (natVal @n Proxy) :: Int @@ -531,151 +513,161 @@     :: forall x ys xs proxy.        (UniqueMember x xs)     => proxy x -> Many ys -> Many xs -> Many (Append (To x xs) (Append ys (After x xs)))-insetAfter _ = insetAfter_ (Proxy @x)+insetAfter _ (Many ys) (Many xs) = Many $ insetAfter_ (Proxy @(IndexOf x xs)) ys xs  -- | Insert a Many into another Many, inserting before a unique @x@ insetBefore     :: forall x ys xs proxy.        (UniqueMember x xs)     => proxy x -> Many ys -> Many xs -> Many (Append (Before x xs) (Append ys (From x xs)))-insetBefore _ = insetBefore_ (Proxy @x)+insetBefore _ (Many ys) (Many xs) = Many $ insetBefore_ (Proxy @(IndexOf x xs)) ys xs  -- | Insert a Many into another Many, inserting after a unique label @l@ insetAfterL     :: forall l ys xs proxy x.        (UniqueLabelMember l xs, x ~ KindAtLabel l xs)     => proxy l -> Many ys -> Many xs -> Many (Append (To x xs) (Append ys (After x xs)))-insetAfterL _ = insetAfter_ (Proxy @x)+insetAfterL _ (Many ys) (Many xs) = Many $ insetAfter_ (Proxy @(IndexOf x xs)) ys xs  -- | Insert a Many into another Many, inserting before a unique label @l@ insetBeforeL     :: forall l ys xs proxy x.        (UniqueLabelMember l xs, x ~ KindAtLabel l xs)     => proxy l -> Many ys -> Many xs -> Many (Append (Before x xs) (Append ys (From x xs)))-insetBeforeL _ = insetBefore_ (Proxy @x)+insetBeforeL _ (Many ys) (Many xs) = Many $ insetBefore_ (Proxy @(IndexOf x xs)) ys xs  -- | Insert a Many into another Many, starting at index @(n + 1)@ insetAfterN     :: forall n ys xs proxy.        (KnownNat n, n + 1 <= Length xs)     => proxy n -> Many ys -> Many xs -> Many (Append (ToIndex n xs) (Append ys (AfterIndex n xs)))-insetAfterN _ (Many ys) (Many xs) = let (as, bs) = S.splitAt (i + 1) xs in Many (as S.>< ys S.>< bs)-  where-    i = fromInteger (natVal @n Proxy) :: Int+insetAfterN p (Many ys) (Many xs) = Many $ insetAfter_ p ys xs  -- | Insert a Many into another Many, starting at index @n@ insetBeforeN     :: forall n ys xs proxy.        (KnownNat n, n + 1 <= Length xs)     => proxy n -> Many ys -> Many xs -> Many (Append (BeforeIndex n xs) (Append ys (FromIndex n xs)))-insetBeforeN _ (Many ys) (Many xs) = let (as, bs) = S.splitAt i xs in Many (as S.>< ys S.>< bs)+insetBeforeN p (Many ys) (Many xs) = Many $ insetBefore_ p ys xs++--------------------------------------------------+#if __GLASGOW_HASKELL__ >= 802+-- The following uses containers > 0.5.7.1 for insertAt and deleteAt only available after GHC 8.2++-- | Insert an item into a Many, inserting after unique type @x@+-- | Insert an item into a Many, inserting after unique type @x@+insertAfter_ :: forall n proxy. KnownNat n => proxy n -> Any -> S.Seq Any -> S.Seq Any+insertAfter_ _ y xs = S.insertAt (i + 1) y xs   where     i = fromInteger (natVal @n Proxy) :: Int +-- | Insert an item into a Many, inserting before unique type @x@+insertBefore_ :: forall n proxy. KnownNat n => proxy n -> Any -> S.Seq Any -> S.Seq Any+insertBefore_ _ y xs = S.insertAt i y xs+  where+    i = fromInteger (natVal @n Proxy) :: Int+ ---------------------------------------------------#if __GLASGOW_HASKELL__ >= 802 +-- | Remove the unique @x@ from a Many.+-- Not named 'delete' to avoid conflicts with 'Data.List.delete'+remove_ :: forall n proxy. KnownNat n => proxy n -> S.Seq Any -> S.Seq Any+remove_ _ xs = S.deleteAt i xs+  where+    i = fromInteger (natVal @n Proxy) :: Int++#else++-- Emulate insertAt and deleteAt for GHC < 8.2 && containers <= 0.5.7.1+ -- | Insert an item into a Many, inserting after unique type @x@-insertAfter_-    :: forall x y xs n proxy.-       (KnownNat n, n ~ IndexOf x xs)-    => proxy x -> y -> Many xs -> Many (Append (To x xs) (y ': After x xs))-insertAfter_ _ y (Many xs) = Many (S.insertAt (i + 1) (unsafeCoerce y) xs)+insertAfter_ :: forall n proxy. KnownNat n => proxy n -> Any -> S.Seq Any -> S.Seq Any+insertAfter_ _ y xs = let (as, bs) = S.splitAt (i + 1) xs in (as S.>< (y S.<| bs))   where     i = fromInteger (natVal @n Proxy) :: Int  -- | Insert an item into a Many, inserting before unique type @x@-insertBefore_-    :: forall x y xs n proxy.-       (KnownNat n, n ~ IndexOf x xs)-    => proxy x -> y -> Many xs -> Many (Append (Before x xs) (y ': From x xs))-insertBefore_ _ y (Many xs) = Many (S.insertAt i (unsafeCoerce y) xs)+insertBefore_ :: forall n proxy. KnownNat n => proxy n -> Any -> S.Seq Any -> S.Seq Any+insertBefore_ _ y xs = let (as, bs) = S.splitAt i xs in as S.>< (y S.<| bs)   where     i = fromInteger (natVal @n Proxy) :: Int +--------------------------------------------------++-- | Remove the unique @x@ from a Many.+-- Not named 'delete' to avoid conflicts with 'Data.List.delete'+remove_ :: forall n proxy. KnownNat n => proxy n -> S.Seq Any -> S.Seq Any+remove_ _ xs = let (as, bs) = S.splitAt i xs in as S.>< S.drop 1 bs+  where+    i = fromInteger (natVal @n Proxy) :: Int++#endif+ -- | Insert an item into a Many, inserting after unique type @x@ insertAfter     :: forall x y xs proxy.        (UniqueMember x xs)     => proxy x -> y -> Many xs -> Many (Append (To x xs) (y ': After x xs))-insertAfter _ = insertAfter_ (Proxy @x)+insertAfter _ y (Many xs) = Many (insertAfter_ (Proxy @(IndexOf x xs)) (unsafeCoerce y) xs)  -- | Insert an item into a Many, inserting before unique type @x@ insertBefore     :: forall x y xs proxy.        (UniqueMember x xs)     => proxy x -> y -> Many xs -> Many (Append (Before x xs) (y ': From x xs))-insertBefore _ = insertBefore_ (Proxy @x)+insertBefore _ y (Many xs) = Many $ insertBefore_ (Proxy @(IndexOf x xs)) (unsafeCoerce y) xs  -- | Insert an item into a Many, inserting after unique label @l@ insertAfterL     :: forall l y xs proxy x.        (UniqueLabelMember l xs, x ~ KindAtLabel l xs)     => proxy l -> y -> Many xs -> Many (Append (To x xs) (y ': After x xs))-insertAfterL _ = insertAfter_ (Proxy @x)+insertAfterL _ y (Many xs) = Many $ insertAfter_ (Proxy @(IndexOf x xs)) (unsafeCoerce y) xs  -- | Insert an item into a Many, inserting before unique label @l@ insertBeforeL     :: forall l y xs proxy x.        (UniqueLabelMember l xs, x ~ KindAtLabel l xs)     => proxy l -> y -> Many xs -> Many (Append (Before x xs) (y ': From x xs))-insertBeforeL _ = insertBefore_ (Proxy @x)+insertBeforeL _ y (Many xs) = Many $ insertBefore_ (Proxy @(IndexOf x xs)) (unsafeCoerce y) xs  -- | Insert an item into a Many, inserting after index @n@ insertAfterN     :: forall n y xs proxy.        (KnownNat n, n + 1 <= Length xs)     => proxy n -> y -> Many xs -> Many (Append (ToIndex n xs) (y ': AfterIndex n xs))-insertAfterN _ y (Many xs) = Many (S.insertAt (i + 1) (unsafeCoerce y) xs)-  where-    i = fromInteger (natVal @n Proxy) :: Int+insertAfterN p y (Many xs) = Many $ insertAfter_ p (unsafeCoerce y) xs  -- | Insert an item into a Many, inserting before index @n@ insertBeforeN     :: forall n y xs proxy.        (KnownNat n, n + 1 <= Length xs)     => proxy n -> y -> Many xs -> Many (Append (BeforeIndex n xs) (y ': FromIndex n xs))-insertBeforeN _ y (Many xs) = Many (S.insertAt i (unsafeCoerce y) xs)-  where-    i = fromInteger (natVal @n Proxy) :: Int+insertBeforeN p y (Many xs) = Many $ insertBefore_ p (unsafeCoerce y) xs  --------------------------------------------------  -- | Remove the unique @x@ from a Many. -- Not named 'delete' to avoid conflicts with 'Data.List.delete'-remove_-    :: forall x xs n proxy.-       (KnownNat n, n ~ IndexOf x xs)-    => proxy x -> Many xs -> Many (Remove x xs)-remove_ _ (Many xs) = Many (S.deleteAt i xs)-  where-    i = fromInteger (natVal @n Proxy) :: Int---- | Remove the unique @x@ from a Many.--- Not named 'delete' to avoid conflicts with 'Data.List.delete' remove     :: forall x xs proxy.        (UniqueMember x xs)     => proxy x -> Many xs -> Many (Remove x xs)-remove _ = remove_ (Proxy @x)+remove _ (Many xs) = Many $ remove_ (Proxy @(IndexOf x xs)) xs  -- | Remove the unique label @l@ from a Many. removeL     :: forall l xs proxy x.        (UniqueLabelMember l xs, x ~ KindAtLabel l xs)     => proxy l -> Many xs -> Many (Remove x xs)-removeL _ = remove_ (Proxy @x)+removeL _ (Many xs) = Many $ remove_ (Proxy @(IndexOf x xs)) xs  -- | Remove the @n@-th item from a Many. removeN     :: forall n xs proxy.        (KnownNat n, n + 1 <= Length xs)     => proxy n -> Many xs -> Many (RemoveIndex n xs)-removeN _ (Many xs) = Many (S.deleteAt i xs)-  where-    i = fromInteger (natVal @n Proxy) :: Int--#endif+removeN p (Many xs) = Many $ remove_ p xs  -------------------------------------------------- @@ -686,11 +678,10 @@ -- 'fetch' \@Int x \`shouldBe` 5 -- @ fetch :: forall x xs. UniqueMember x xs => Many xs -> x-fetch = fetch_+fetch (Many xs) = unsafeCoerce $ fetch_ (Proxy @(IndexOf x xs)) xs --- | Using S.lookup to ensure Seq is not stored in a thunk-fetch_ :: forall x xs n. (KnownNat n, n ~ IndexOf x xs) => Many xs -> x-fetch_ (Many xs) = let !x = S.index xs i in (unsafeCoerce x) -- forcing x to avoid storing Seq in thunk+fetch_ :: forall n proxy. KnownNat n => proxy n -> S.Seq Any -> Any+fetch_ _ xs = let !x = S.index xs i in x -- forcing x to avoid storing Seq in thunk   where i = fromInteger (natVal @n Proxy)  --------------------------------------------------@@ -704,7 +695,7 @@ -- 'fetchL' \@"Hi" Proxy y \`shouldBe` Tagged \@"Hi" True -- @ fetchL :: forall l xs proxy x. (UniqueLabelMember l xs, x ~ KindAtLabel l xs) => proxy l -> Many xs -> x-fetchL _ = fetch_ @x+fetchL _ (Many xs) = unsafeCoerce $ fetch_ (Proxy @(IndexOf x xs)) xs  -------------------------------------------------- @@ -715,8 +706,7 @@ -- 'fetchN' @1 Proxy x \`shouldBe` False -- @ fetchN :: forall n xs proxy x. MemberAt n x xs => proxy n -> Many xs -> x-fetchN p (Many xs) = let !x = S.index xs i in (unsafeCoerce x) -- forcing x to avoid storing Seq in thunk-  where i = fromInteger (natVal p)+fetchN p (Many xs) = unsafeCoerce $ fetch_ p xs  -------------------------------------------------- @@ -727,10 +717,10 @@ -- 'replace' \@Int x 6 \`shouldBe` (6 :: Int) './' False './' \'X' './' Just \'O' './' 'nil' -- @ replace :: forall x xs. UniqueMember x xs => Many xs -> x -> Many xs-replace = replace_+replace (Many xs) x = Many $ replace_ (Proxy @(IndexOf x xs)) xs (unsafeCoerce x) -replace_ :: forall x xs n. (KnownNat n, n ~ IndexOf x xs) => Many xs -> x -> Many xs-replace_ (Many xs) v = Many (S.update i (unsafeCoerce v) xs)+replace_ :: forall n proxy. KnownNat n => proxy n -> S.Seq Any -> Any -> S.Seq Any+replace_ _ xs x = S.update i x xs   where i = fromInteger (natVal @n Proxy)  -- | Polymorphic setter by unique type. Set the field with type @x@, and replace with type @y@@@ -740,11 +730,7 @@ -- 'replace'' \@Int Proxy x (Just True) \`shouldBe` Just True './' False './' \'X' './' Just \'O' './' 'nil' -- @ replace' :: forall x y xs proxy. UniqueMember x xs => proxy x -> Many xs -> y -> Many (Replace x y xs)-replace' = replace'_--replace'_ :: forall x y xs proxy n. (KnownNat n, n ~ IndexOf x xs) => proxy x -> Many xs -> y -> Many (Replace x y xs)-replace'_ _ (Many xs) v = Many (S.update i (unsafeCoerce v) xs)-  where i = fromInteger (natVal @n Proxy)+replace' _ (Many xs) x = Many $ replace_ (Proxy @(IndexOf x xs)) xs (unsafeCoerce x)  -------------------------------------------------- @@ -758,7 +744,7 @@ --     (5 :: Int) './' False './' Tagged \@Foo \'X' './' Tagged \@\"Hello" (7 :: Int) './' 'nil' -- @ replaceL :: forall l xs proxy x. (UniqueLabelMember l xs, x ~ KindAtLabel l xs) => proxy l -> Many xs -> x -> Many xs-replaceL _ = replace_ @x+replaceL _ (Many xs) x = Many $ replace_ (Proxy @(IndexOf x xs)) xs (unsafeCoerce x)  -- | Polymorphic setter by unique type. Set the field with type @x@, and replace with type @y@ --@@ -770,7 +756,7 @@ --     (5 :: Int) './' False './' Tagged \@Foo \'X' './' Tagged \@\"Hello" False './' 'nil' -- @ replaceL' :: forall l y xs proxy x. (UniqueLabelMember l xs, x ~ KindAtLabel l xs) => proxy l -> Many xs -> y -> Many (Replace x y xs)-replaceL' _ = replace'_ @x Proxy+replaceL' _ (Many xs) x = Many $ replace_ (Proxy @(IndexOf x xs)) xs (unsafeCoerce x)  -------------------------------------------------- @@ -781,13 +767,11 @@ -- 'replaceN' \@0 Proxy x 7 `shouldBe` -- @ replaceN :: forall n xs proxy x. MemberAt n x xs => proxy n -> Many xs -> x -> Many xs-replaceN p (Many xs) v = Many (S.update i (unsafeCoerce v) xs)-  where i = fromInteger (natVal p)+replaceN p (Many xs) x = Many $ replace_ p xs (unsafeCoerce x)  -- | Polymorphic version of 'replaceN' replaceN' :: forall n y xs proxy x. MemberAt n x xs => proxy n -> Many xs -> y -> Many (ReplaceIndex n y xs)-replaceN' p (Many xs) v = Many (S.update i (unsafeCoerce v) xs)-  where i = fromInteger (natVal p)+replaceN' p (Many xs) x = Many $ replace_ p xs (unsafeCoerce x)  ----------------------------------------------------------------------- @@ -1018,14 +1002,14 @@     reiterate = coerce  -- | For each type x in larger, find the index in ys, and create a (key, value)-instance forall smaller larger x xs n. (UniqueIfExists smaller x larger, MaybeUniqueMemberAt n x smaller) =>+instance forall smaller larger x xs. (UniqueIfExists smaller x larger, MaybeUniqueMember x smaller) =>     CaseAny (CaseSelect smaller larger (Maybe (Int, WrappedAny))) (x ': xs) where     caseAny _ v =         case i of             0 -> Nothing             i' -> Just (i' - 1, WrappedAny v)       where-        i = fromInteger (natVal @n Proxy)+        i = fromInteger (natVal @(PositionOf x smaller) Proxy)  ----------------------------------------------------------------------- @@ -1117,11 +1101,11 @@     reiterate = coerce  -- | for each x in @smaller@, convert it to a (k, v) to insert into the x in @Many larger@-instance UniqueMemberAt n x larger =>+instance UniqueMember x larger =>          CaseAny (CaseAmend larger (Int, WrappedAny)) (x ': xs) where     caseAny _ v = (i, WrappedAny v)       where-        i = fromInteger (natVal @n Proxy)+        i = fromInteger (natVal @(IndexOf x larger) Proxy)  ----------------------------------------------------------------------- @@ -1167,11 +1151,11 @@     reiterate = coerce  -- | for each y in @smaller@, convert it to a (k, v) to insert into the x in @Many larger@-instance (UniqueMemberAt n x larger) =>+instance (UniqueMember x larger) =>          CaseAny (CaseAmend' larger (Int, WrappedAny)) ((x, y) ': zs) where     caseAny _ v = (i, WrappedAny v)       where-        i = fromInteger (natVal @n Proxy)+        i = fromInteger (natVal @(IndexOf x larger) Proxy)  ----------------------------------------------------------------------- 

@@ -22,13 +22,10 @@     UniqueMembers (x ': xs) ys = (UniqueMember x ys, UniqueMembers xs ys)  -- | Ensures that @x@ is a unique member of @xs@, and that 'natVal' can be used.-type UniqueMemberAt n x xs = (Unique x xs, KnownNat n, n ~ IndexOf x xs)---- | Ensures that @x@ is a unique member of @xs@, and that 'natVal' can be used. type UniqueLabelMember l xs = (UniqueLabel l xs, KnownNat (IndexOf (KindAtLabel l xs) xs))  -- | Ensures that @x@ is a unique member of @xs@ if it exists, and that 'natVal' can be used.-type MaybeUniqueMemberAt n x xs = (Unique x xs, KnownNat n, n ~ PositionOf x xs)+type MaybeUniqueMember x xs = (Unique x xs, KnownNat (PositionOf x xs))  -- | Ensures that @x@ is a member of @xs@ at @n@, and that 'natVal' can be used. type MemberAt n x xs = (KnownNat n, x ~ KindAtIndex n xs)

@@ -225,19 +225,6 @@ obvious :: Which '[a] -> a obvious (Which _ v) = unsafeCoerce v --- | 'trial' a type in a 'Which' and 'Either' get the 'Right' value or the 'Left'-over possibilities.------ @--- let x = 'pick' \'A' \@'[Int, Bool, Char, Maybe String] :: 'Which' '[Int, Bool, Char, Maybe String]--- 'trial' \@Char x \`shouldBe` Right \'A'--- 'trial' \@Int x \`shouldBe` Left ('pick' \'A') :: 'Which' '[Bool, Char, Maybe String]--- @-trial-    :: forall x xs.-       (UniqueMember x xs)-    => Which xs -> Either (Which (Remove x xs)) x-trial = trial_- trial_     :: forall n x xs.        (KnownNat n, n ~ IndexOf x xs)@@ -249,21 +236,36 @@                           then Left (Which (n - 1) v)                           else Left (Which n v) --- | Variation of 'trial' which returns a Maybe-trial'+-- | 'trialN' the n-th type of a 'Which', and get 'Either' the 'Right' value or the 'Left'-over possibilities.+--+-- @+-- let x = 'pick' \'A' \@_ \@'[Int, Bool, Char, Maybe String] :: 'Which' '[Int, Bool, Char, Maybe String]+-- 'trialN' \@_ \@1 Proxy x \`shouldBe` Left ('pick' \'A') :: 'Which' '[Int, Char, Maybe String]+-- @+trialN+    :: forall n xs proxy x.+       (MemberAt n x xs)+    => proxy n -> Which xs -> Either (Which (RemoveIndex n xs)) x+trialN _ (Which n v) = let i = fromInteger (natVal @n Proxy)+                  in if n == i+                     then Right (unsafeCoerce v)+                     else if n > i+                          then Left (Which (n - 1) v)+                          else Left (Which n v)+++-- | 'trial' a type in a 'Which' and 'Either' get the 'Right' value or the 'Left'-over possibilities.+--+-- @+-- let x = 'pick' \'A' \@'[Int, Bool, Char, Maybe String] :: 'Which' '[Int, Bool, Char, Maybe String]+-- 'trial' \@Char x \`shouldBe` Right \'A'+-- 'trial' \@Int x \`shouldBe` Left ('pick' \'A') :: 'Which' '[Bool, Char, Maybe String]+-- @+trial     :: forall x xs.        (UniqueMember x xs)-    => Which xs -> Maybe x-trial' = trial_'--trial_'-    :: forall n x xs.-       (KnownNat n, n ~ IndexOf x xs)-    => Which xs -> Maybe x-trial_' (Which n v) = let i = fromInteger (natVal @n Proxy)-                  in if n == i-                     then Just (unsafeCoerce v)-                     else Nothing+    => Which xs -> Either (Which (Remove x xs)) x+trial = trial_  -- | A variation of 'trial' where x is specified via a label --@@ -278,6 +280,34 @@     => proxy l -> Which xs -> Either (Which (Remove x xs)) x trialL _ = trial_ @_ @x ++trial_'+    :: forall n x xs.+       (KnownNat n, n ~ IndexOf x xs)+    => Which xs -> Maybe x+trial_' (Which n v) = let i = fromInteger (natVal @n Proxy)+                  in if n == i+                     then Just (unsafeCoerce v)+                     else Nothing+++-- | Variation of 'trialN' which returns a Maybe+trialN'+    :: forall n xs proxy x.+       (MemberAt n x xs)+    => proxy n -> Which xs -> Maybe x+trialN' _ (Which n v) = let i = fromInteger (natVal @n Proxy)+                  in if n == i+                     then Just (unsafeCoerce v)+                     else Nothing++-- | Variation of 'trial' which returns a Maybe+trial'+    :: forall x xs.+       (UniqueMember x xs)+    => Which xs -> Maybe x+trial' = trial_'+ -- | Variation of 'trialL' which returns a Maybe trialL'     :: forall l xs proxy x.@@ -302,33 +332,6 @@            then Just (unsafeCoerce v)            else Nothing --- | 'trialN' the n-th type of a 'Which', and get 'Either' the 'Right' value or the 'Left'-over possibilities.------ @--- let x = 'pick' \'A' \@_ \@'[Int, Bool, Char, Maybe String] :: 'Which' '[Int, Bool, Char, Maybe String]--- 'trialN' \@_ \@1 Proxy x \`shouldBe` Left ('pick' \'A') :: 'Which' '[Int, Char, Maybe String]--- @-trialN-    :: forall n xs proxy x.-       (MemberAt n x xs)-    => proxy n -> Which xs -> Either (Which (RemoveIndex n xs)) x-trialN _ (Which n v) = let i = fromInteger (natVal @n Proxy)-                  in if n == i-                     then Right (unsafeCoerce v)-                     else if n > i-                          then Left (Which (n - 1) v)-                          else Left (Which n v)---- | Variation of 'trialN' which returns a Maybe-trialN'-    :: forall n xs proxy x.-       (MemberAt n x xs)-    => proxy n -> Which xs -> Maybe x-trialN' _ (Which n v) = let i = fromInteger (natVal @n Proxy)-                  in if n == i-                     then Just (unsafeCoerce v)-                     else Nothing- -----------------------------------------------------------------  -- | A friendlier constraint synonym for 'diversify'.@@ -456,15 +459,15 @@ instance Reiterate (CaseReinterpret branch tree r) tree' where     reiterate CaseReinterpret = CaseReinterpret -instance ( MaybeUniqueMemberAt n x branch+instance ( MaybeUniqueMember x branch          , comp ~ Complement tree branch-         , MaybeUniqueMemberAt n' x comp+         , MaybeUniqueMember x comp          , Unique x tree -- Compile error to ensure reinterpret only works with unique fields          ) =>          Case (CaseReinterpret branch tree (Either (Which comp) (Which branch))) (x ': tree') where     case' CaseReinterpret a =-        case fromInteger (natVal @n Proxy) of-            0 -> let j = fromInteger (natVal @n' Proxy)+        case fromInteger (natVal @(PositionOf x branch) Proxy) of+            0 -> let j = fromInteger (natVal @(PositionOf x comp) Proxy)                  -- safe use of partial! j will never be zero due to check above                  in Left $ Which (j - 1) (unsafeCoerce a)             i -> Right $ Which (i - 1) (unsafeCoerce a)@@ -485,14 +488,13 @@ instance Reiterate (CaseReinterpret' branch tree r) tree' where     reiterate CaseReinterpret' = CaseReinterpret' -instance ( MaybeUniqueMemberAt n x branch+instance ( MaybeUniqueMember x branch          , comp ~ Complement tree branch-         -- , MaybeUniqueMemberAt n' x comp          , Unique x tree -- Compile error to ensure reinterpret only works with unique fields          ) =>          Case (CaseReinterpret' branch tree (Maybe (Which branch))) (x ': tree') where     case' CaseReinterpret' a =-        case fromInteger (natVal @n Proxy) of+        case fromInteger (natVal @(PositionOf x branch) Proxy) of             0 -> Nothing             i -> Just $ Which (i - 1) (unsafeCoerce a) 

@@ -391,7 +391,6 @@             insetAfterL (Proxy @Dee) z y `shouldBe` y2a /./ z /./ y2b             insetAfterN (Proxy @2) z x `shouldBe` x2a /./ z /./ x2b -#if __GLASGOW_HASKELL__ >= 802         it "can be 'insert'ted with an item at a specific place" $ do             let x = (5 :: Int) ./ False ./ 'X' ./ Just True ./ Just 'A' ./ nil                 y = (Tagged 5 :: Tagged Foo Int) ./ False ./ Tagged @Dee 'X' ./ Just True ./ Tagged @Bar (Just 'A') ./ nil@@ -444,4 +443,3 @@             remove (Proxy @(Char)) x `shouldBe` x'             removeL (Proxy @Dee) y `shouldBe` y'             removeN (Proxy @2) x `shouldBe` x'-#endif