data-diverse 0.4.0.0 → 0.5.0.0

raw patch · 15 files changed

+392/−382 lines, 15 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• README.md +2/−2
• data-diverse.cabal +6/−6
• src/Data/Diverse.hs +2/−2
• src/Data/Diverse/Case.hs +1/−1
• src/Data/Diverse/CaseTypeable.hs +1/−1
• src/Data/Diverse/Cases.hs +1/−1
• src/Data/Diverse/Many/Internal.hs +1/−1
• src/Data/Diverse/Reduce.hs +3/−6
• src/Data/Diverse/Reiterate.hs +1/−1
• src/Data/Diverse/Type.hs +0/−145
• src/Data/Diverse/Type/Internal.hs +0/−194
• src/Data/Diverse/TypeLevel.hs +145/−0
• src/Data/Diverse/TypeLevel/Internal.hs +194/−0
• src/Data/Diverse/Which/Internal.hs +34/−21
• test/Data/Diverse/TypeSpec.hs +1/−1

@@ -5,7 +5,7 @@  "Data.Diverse.Which" polymorphic variant of possibilities encoded as (Int, Any). -Provides getters, setters, projection, injection, fold, and catamorphisms;-accessed by type or index.+Provides getters, setters, projection, injection, folds, and catamorphisms;+accessed by type or index or label.  Refer to [ManySpec.hs](https://github.com/louispan/data-diverse/blob/master/test/Data/Diverse/ManySpec.hs) and [WhichSpec.hs](https://github.com/louispan/data-diverse/blob/master/test/Data/Diverse/WhichSpec.hs) for example usages.

@@ -1,10 +1,10 @@ name:                data-diverse-version:             0.4.0.0+version:             0.5.0.0 synopsis:            Extensible records and polymorphic variants. description:         "Data.Diverse.Many" is an extensible record for any size encoded efficiently as (Int, Map Int Any).                      "Data.Diverse.Which" is a polymorphic variant of possibilities encoded as (Int, Any).-                     Provides getters, setters, projection, injection, fold, and catamorphisms;-                     accessed by type or index.+                     Provides getters, setters, projection, injection, folds, and catamorphisms;+                     accessed by type, index or label.                      Refer to [ManySpec.hs](https://github.com/louispan/data-diverse/blob/master/test/Data/Diverse/ManySpec.hs) and [WhichSpec.hs](https://github.com/louispan/data-diverse/blob/master/test/Data/Diverse/WhichSpec.hs) for example usages. homepage:            https://github.com/louispan/data-diverse#readme license:             BSD3@@ -16,7 +16,7 @@ build-type:          Simple extra-source-files:  README.md cabal-version:       >=1.10-tested-with:         GHC == 8.0.1+tested-with:         GHC == 8.0.2  library   hs-source-dirs:      src@@ -29,10 +29,10 @@                        Data.Diverse.Many.Internal                        Data.Diverse.Reduce                        Data.Diverse.Reiterate-                       Data.Diverse.Type+                       Data.Diverse.TypeLevel+                       Data.Diverse.TypeLevel.Internal                        Data.Diverse.Which                        Data.Diverse.Which.Internal-  other-modules:       Data.Diverse.Type.Internal   build-depends:       base >= 4.7 && < 5                      , containers >= 0.5 && < 0.6                      , ghc-prim >= 0.5 && < 1

@@ -6,7 +6,7 @@     , module Data.Diverse.Many     , module Data.Diverse.Reduce     , module Data.Diverse.Reiterate-    , module Data.Diverse.Type+    , module Data.Diverse.TypeLevel     , module Data.Diverse.Which     ) where @@ -17,5 +17,5 @@ import Data.Diverse.Many import Data.Diverse.Reduce import Data.Diverse.Reiterate-import Data.Diverse.Type+import Data.Diverse.TypeLevel import Data.Diverse.Which

@@ -6,7 +6,7 @@  module Data.Diverse.Case where -import Data.Diverse.Type+import Data.Diverse.TypeLevel import Data.Kind  -- | This class allows defining handlers that can handle the 'Head' type in the @xs@ typelist.

@@ -9,7 +9,7 @@  import Data.Diverse.Case import Data.Diverse.Reiterate-import Data.Diverse.Type+import Data.Diverse.TypeLevel import Data.Kind import Data.Typeable 

@@ -21,7 +21,7 @@ import Data.Diverse.Case import Data.Diverse.Many import Data.Diverse.Reiterate-import Data.Diverse.Type+import Data.Diverse.TypeLevel import Data.Kind import Data.Proxy import GHC.TypeLits

@@ -103,7 +103,7 @@ import Data.Diverse.AFoldable import Data.Diverse.Case import Data.Diverse.Reiterate-import Data.Diverse.Type+import Data.Diverse.TypeLevel import Data.Kind import qualified Data.Map.Strict as M import Data.Proxy

@@ -1,12 +1,9 @@ {-# LANGUAGE DataKinds #-}-{-# LANGUAGE KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses #-}  module Data.Diverse.Reduce where -import Data.Kind---- | Reduce a polymorphic variant @v xs@ into @r@ using handlers.+-- | Convert something @v@ into @r@ using handlers. -- This class is required in order to step through all the different types in a variant.-class Reduce v handler (xs :: [Type]) r where-    reduce :: handler xs r -> v xs -> r+class Reduce v handler r where+    reduce :: handler r -> v -> r

@@ -6,7 +6,7 @@  module Data.Diverse.Reiterate where -import Data.Diverse.Type+import Data.Diverse.TypeLevel import Data.Kind import GHC.TypeLits 

@@ -1,145 +0,0 @@-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE UndecidableInstances #-}-{-# LANGUAGE TypeInType #-}--module Data.Diverse.Type where--import Data.Diverse.Type.Internal-import Data.Kind-import GHC.TypeLits---- | Ensures that @x@ is a unique member of @xs@, and that 'natVal' can be used.-type UniqueMember x xs = (Unique x xs, KnownNat (IndexOf x xs))---- | 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)---- | 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)---- | Ensures that @x@ is a member of @xs@ at @n@ if it exists, and that 'natVal' can be used.-type MaybeMemberAt n x xs = (KnownNat n, KindAtPositionIs n x xs)---- | Ensures x is a unique member in @xs@ iff it exists in @ys@-type family UniqueIfExists ys x xs :: Constraint where-    UniqueIfExists '[] x xs = ()-    UniqueIfExists (y ': ys) y xs = Unique y xs-    UniqueIfExists (y ': ys) x xs = UniqueIfExists ys x xs---- | Ensures that the type list contain unique types-type IsDistinct (xs :: [k]) = IsDistinctImpl xs xs---- | Return the list of distinct types in a typelist-type family Nub (xs :: [k]) :: [k] where-    Nub '[] = '[]-    Nub (x ': xs) = NubImpl xs x xs---- | Ensures that @x@ only ever appears once in @xs@-type Unique (x :: k) (xs :: [k]) = UniqueImpl xs x xs---- | Ensures that the @label@ in @tagged label v@ only ever appears once in @xs@.-type UniqueLabel (l :: k1) (xs :: [k]) = UniqueLabelImpl xs l xs---- | Ensures that the @label@ list all 'UniqueLabel's-type family UniqueLabels (ls :: [k1]) (xs :: [k]) :: Constraint where-    UniqueLabels '[] xs = ()-    UniqueLabels (l ': ls) xs = (UniqueLabel l xs, UniqueLabels ls xs)---- | Get the first index of a type (Indexed by 0)--- Will result in type error if x doesn't exist in xs.-type IndexOf (x :: k) (xs :: [k]) = IndexOfImpl xs x xs---- | Get the first index of a type (Indexed by 1)--- Will return 0 if x doesn't exists in xs.-type PositionOf (x :: k) (xs :: [k]) = PositionOfImpl 0 x xs---- | Get the type at an index-type KindAtIndex (n :: Nat) (xs :: [k]) = KindAtIndexImpl n xs n xs---- | Get the type at a label-type KindAtLabel (l :: k1) (xs :: [k]) = KindAtLabelImpl l xs xs---- | It's actually ok for the position to be zero, but if it's not zero then the types must match-type family KindAtPositionIs (n :: Nat) (x :: k) (xs :: [k]) :: Constraint where-    KindAtPositionIs 0 x xs = ()-    KindAtPositionIs n x xs = (x ~ KindAtIndexImpl (n - 1) xs (n - 1) xs)---- | Get the types at an list of index-type family KindsAtIndices (ns :: [Nat]) (xs :: [k]) :: [k] where-    KindsAtIndices '[] xs = '[]-    KindsAtIndices (n ': ns) xs = KindAtIndex n xs ': KindsAtIndices ns xs--type family KindsAtLabels (ls :: [k1]) (xs :: [k]) :: [k] where-    KindsAtLabels '[] xs = '[]-    KindsAtLabels (l ': ls) xs = KindAtLabel l xs ': KindsAtLabels ls xs---- | The typelist @xs@ without first @x@. It is okay for @x@ not to exist in @xs@-type family Without (x :: k) (xs :: [k]) :: [k] where-    Without x '[] = '[]-    Without x (x ': xs) = xs-    Without x (y ': xs) = y ': Without x xs---- | The typelist @xs@ with the first @x@ replaced by @y@. It is okay for @x@ not to exist in @xs@-type Replace (x :: k) (y :: k) (xs :: [k]) = ReplaceImpl x y xs---- | The typelist @zs@ with the first @xs@ replaced by @ys@.--- @xs@ must be the same size as @ys@-type Replaces (xs :: [k]) (ys :: [k]) (zs :: [k]) = ReplacesImpl xs ys xs ys zs---- | The typelist @xs@ without the type at Nat @n@. @n@ must be within bounds of @xs@-type WithoutIndex (n :: Nat) (xs :: [k]) = WithoutIndexImpl n xs n xs---- | The typelist @xs@ without the type at Nat @n@ replaced by @y@. @n@ must be within bounds of @xs@-type ReplaceIndex (n :: Nat) (y :: k) (xs :: [k]) = ReplaceIndexImpl n xs n y xs---- | The typelist @xs@ replaced by @ys@ at the indices @ns@. @ns@ and @ys@ must be the same length. @ns@ must be within bounds of @xs@-type ReplacesIndex (ns :: [Nat]) (ys :: [k]) (xs :: [k]) = ReplacesIndexImpl 0 ns ys xs---- | Get the typelist without the 'Head' type-type family Tail (xs :: [k]) :: [k] where-    Tail '[] = TypeError ('Text "Tail error: empty type list")-    Tail (x ': xs) = xs---- | Get the first type in a typelist-type family Head (xs :: [k]) :: k where-    Head '[] = TypeError ('Text "Head error: empty type list")-    Head (x ': xs) = x---- | Get the last type in a typelist-type family Last (xs :: [k]) :: k where-    Last '[] = TypeError ('Text "Last error: empty type list")-    Last (x ': x' ': xs) = Last (x' ': xs)-    Last '[x] = x---- | Ensures two typelists are the same length-type SameLength (xs :: [k1]) (ys :: [k2]) = SameLengthImpl xs ys xs ys---- | Set complement. Returns the set of things in @xs@ that are not in @ys@.-type family Complement (xs :: [k]) (ys :: [k]) :: [k] where-    Complement xs '[] = xs-    Complement xs (y ': ys)  = Complement (Without y xs) ys---- | Returns a @xs@ appended with @ys@-type family Append (xs :: [k]) (ys :: [k]) :: [k] where-    Append '[] ys = ys-    Append (x ': xs) ys = x ': Append xs ys---- | Returns the typelist without the 'Last' type-type family Init (xs :: [k]) :: [k] where-    Init '[]  = TypeError ('Text "Init error: empty type list")-    Init '[x] = '[]-    Init (x ': xs) = x ': Init xs---- | Takes two lists which must be the same length and returns a list of corresponding pairs.-type Zip (xs :: [k]) (ys :: [k]) = ZipImpl xs ys xs ys

@@ -1,194 +0,0 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE UndecidableInstances #-}--module Data.Diverse.Type.Internal where--import Data.Kind-import GHC.TypeLits---- | Get the first position of a type (indexed by 1)--- Will return 0 if @x@ doesn't exists in @xs@.-type family PositionOfImpl (i :: Nat) (x :: k) (xs :: [k]) :: Nat where-   PositionOfImpl i x (x ': xs) = i + 1-   PositionOfImpl i y (x ': xs) = PositionOfImpl (i + 1) y xs-   PositionOfImpl i x '[] = 0---- | Get the first index of a type from a list-type family IndexOfImpl (ctx :: [k]) (x :: k) (xs :: [k]) :: Nat where-   IndexOfImpl ctx x (x ': xs) = 0-   IndexOfImpl ctx y (x ': xs) = 1 + IndexOfImpl ctx y xs-   IndexOfImpl ctx y '[] = TypeError ('Text "IndexOf error: ‘"-                                      ':<>: 'ShowType y-                                      ':<>: 'Text "’"-                                      ':<>: 'Text " is not a member of "-                                      ':<>: 'Text "‘"-                                      ':<>: 'ShowType ctx-                                      ':<>: 'Text "’")---- | Searches for y in ys--- if not found, than use y, and repeat search with next (y ': ys) in ctx--- else if found, then don't use y, then repeat search with next (y ': ys) in ctx-type family NubImpl (ctx :: [k]) (y :: k) (ys :: [k]) :: [k] where-    NubImpl '[] y '[] = y ': '[]-    NubImpl '[] y (y ': xs) = '[]-    NubImpl (x ': xs) y '[] = y ': NubImpl xs x xs-    NubImpl (x ': xs) y (y ': ys) = NubImpl xs x xs-    NubImpl ctx y (x ': xs) = NubImpl ctx y xs---- | Errors if a type exists in a typelist-type family MissingImpl (ctx :: [k]) (y :: k) (xs :: [k]) :: Constraint where-    MissingImpl ctx y '[] = ()-    MissingImpl ctx x (x ': xs) = TypeError ('Text "Not unique error: ‘"-                                             ':<>: 'ShowType x-                                             ':<>: 'Text "’"-                                             ':<>: 'Text " is a duplicate in "-                                             ':<>: 'Text "‘"-                                             ':<>: 'ShowType ctx-                                             ':<>: 'Text "’")-    MissingImpl ctx y (x ': xs) = (MissingImpl ctx y xs)---- | Errors if a label exists in a typelist-type family MissingLabelImpl (ctx :: [k]) (l :: k2) (xs :: [k]) :: Constraint where-    MissingLabelImpl ctx y '[] = ()-    MissingLabelImpl ctx l (tagged l x ': xs) = TypeError ('Text "Not unique label error: ‘"-                                             ':<>: 'ShowType l-                                             ':<>: 'Text "’"-                                             ':<>: 'Text " is a duplicate in "-                                             ':<>: 'Text "‘"-                                             ':<>: 'ShowType ctx-                                             ':<>: 'Text "’")-    MissingLabelImpl ctx l (x ': xs) = (MissingLabelImpl ctx l xs)---- | Ensures that the type list contain unique types.--- Not implemented as @(xs ~ Nub xs)@ for better type error messages.-type family IsDistinctImpl (ctx :: [k]) (xs :: [k]) :: Constraint where-    IsDistinctImpl ctx '[] = ()-    IsDistinctImpl ctx (x ': xs) = (MissingImpl ctx x xs, IsDistinctImpl ctx xs)---- | Ensures that @x@ only ever appears once in @xs@-type family UniqueImpl (ctx :: [k]) (x :: k) (xs :: [k]) :: Constraint where-    UniqueImpl ctx x '[] = ()-    UniqueImpl ctx x (x ': xs) = MissingImpl ctx x xs-    UniqueImpl ctx x (y ': xs) = UniqueImpl ctx x xs---- | Ensures that the @label@ in @tagged label v@ only ever appears once in @xs@.-type family UniqueLabelImpl (ctx :: [k]) (l :: k1) (xs :: [k]) :: Constraint where-    UniqueLabelImpl ctx l '[] = ()-    UniqueLabelImpl ctx l (tagged l x ': xs) = MissingLabelImpl ctx l xs-    UniqueLabelImpl ctx l (y ': xs) = UniqueLabelImpl ctx l xs---- | Indexed access into the list-type family KindAtIndexImpl (orig :: Nat) (ctx :: [k]) (n :: Nat) (xs :: [k]) :: k where-    KindAtIndexImpl i ctx 0 '[] = TypeError ('Text "KindAtIndex error: Index ‘"-                                       ':<>: 'ShowType i-                                       ':<>: 'Text "’"-                                       ':<>: 'Text " is out of bounds of "-                                       ':<>: 'Text "‘"-                                       ':<>: 'ShowType ctx-                                       ':<>: 'Text "’")-    KindAtIndexImpl i ctx 0 (x ': xs) = x-    KindAtIndexImpl i ctx n (x ': xs) = KindAtIndexImpl i ctx (n - 1) xs---- | Labelled access into the list-type family KindAtLabelImpl (l :: k1) (ctx :: [k]) (xs :: [k]) :: k where-    KindAtLabelImpl l ctx '[] = TypeError ('Text "KindAtLabel error: Label ‘"-                                       ':<>: 'ShowType l-                                       ':<>: 'Text "’"-                                       ':<>: 'Text " is not found in "-                                       ':<>: 'Text "‘"-                                       ':<>: 'ShowType ctx-                                       ':<>: 'Text "’")-    KindAtLabelImpl l ctx (tagged l x ': xs) = tagged l x-    KindAtLabelImpl l ctx (x ': xs) = KindAtLabelImpl l ctx xs---- | Ensures two typelists are the same length-type family SameLengthImpl (ctx :: [k1]) (cty :: [k2]) (xs :: [k1]) (yx :: [k2]) :: Constraint where-    SameLengthImpl as bs '[] '[] = ()-    SameLengthImpl as bs (x ': xs) (y ': ys) = SameLengthImpl as bs xs ys-    SameLengthImpl as bs xs ys = TypeError ('Text "SameLength error: ‘"-                                            ':<>: 'ShowType as-                                            ':<>: 'Text "’"-                                            ':<>: 'Text " is not the same length as "-                                            ':<>: 'Text "‘"-                                            ':<>: 'ShowType bs-                                            ':<>: 'Text "’")---- | The typelist @xs@ without the type at Nat @n@. @n@ must be within bounds of @xs@-type family WithoutIndexImpl (i :: Nat) (ctx :: [k]) (n :: Nat) (xs :: [k]) :: [k] where-    WithoutIndexImpl i ctx n '[] = TypeError ('Text "WithoutIndex error: Index ‘"-                                       ':<>: 'ShowType i-                                       ':<>: 'Text "’"-                                       ':<>: 'Text " is out of bounds of "-                                       ':<>: 'Text "‘"-                                       ':<>: 'ShowType ctx-                                       ':<>: 'Text "’")-    WithoutIndexImpl i ctx 0 (x ': xs) = xs-    WithoutIndexImpl i ctx n (x ': xs) = x ': WithoutIndexImpl i ctx (n - 1) xs---- | The typelist @xs@ without the type at Nat @n@ replaced by @y@. @n@ must be within bounds of @xs@-type family ReplaceIndexImpl (i :: Nat) (ctx :: [k]) (n :: Nat) (y :: k) (xs :: [k]) :: [k] where-    ReplaceIndexImpl i ctx n y '[] = TypeError ('Text "ReplaceIndex error: Index ‘"-                                       ':<>: 'ShowType i-                                       ':<>: 'Text "’"-                                       ':<>: 'Text " is out of bounds of "-                                       ':<>: 'Text "‘"-                                       ':<>: 'ShowType ctx-                                       ':<>: 'Text "’")-    ReplaceIndexImpl i ctx 0 y (x ': xs) = y ': xs-    ReplaceIndexImpl i ctx n y (x ': xs) = x ': ReplaceIndexImpl i ctx (n - 1) y xs---- | The typelist @xs@ with the first @x@ replaced by @y@. It is okay for @x@ not to exist in @xs@-type family ReplaceImpl (x :: k) (y :: k) (xs :: [k]) :: [k] where-    ReplaceImpl x y '[] = '[]-    ReplaceImpl x y (x ': xs) = y ': xs-    ReplaceImpl x y (z ': xs) = z ': ReplaceImpl x y xs---- | The typelist @zs@ with the first @xs@ replaced by @ys@.--- @xs@ must be the same size as @ys@-type family ReplacesImpl (xs' :: [k]) (ys' :: [k]) (xs :: [k]) (ys :: [k]) (zs :: [k]) :: [k] where-    ReplacesImpl xs' ys' xs ys '[] = '[]-    ReplacesImpl xs' ys' '[] '[] (z ': zs) = z ': ReplacesImpl xs' ys' xs' ys' zs-    ReplacesImpl xs' ys' (x ': xs) (y ': ys) (x ': zs) = y ': ReplacesImpl xs' ys' xs' ys' zs-    ReplacesImpl xs' ys' (x ': xs) (y ': ys) (z ': zs) = ReplacesImpl xs' ys' xs ys (z ': zs)-    ReplacesImpl xs' ys' xs ys zs = TypeError ('Text "Replaces error: ‘"-                                       ':<>: 'ShowType xs'-                                       ':<>: 'Text "’"-                                       ':<>: 'Text " must be the same size as "-                                       ':<>: 'Text "‘"-                                       ':<>: 'ShowType ys'-                                       ':<>: 'Text "’")---- | The type @x@ replaced by an @y@ if an @n@ matches @i@.-type family ReplaceIfIndex (ns :: [Nat]) (ys :: [k]) (i :: Nat) (x :: k) :: k where-    ReplaceIfIndex '[] ys i x = x-    ReplaceIfIndex ns '[] i x = x-    ReplaceIfIndex (n ': ns) (y ': ys) n x = y-    ReplaceIfIndex (n ': ns) (y ': ys) i x = ReplaceIfIndex ns ys i x---- | The typelist @xs@ replaced by @ys@ at the indices @ns@. @ns@ and @ys@ must be the same length. @ns@ must be within bounds of @xs@-type family ReplacesIndexImpl (i :: Nat) (ns :: [Nat]) (ys :: [k]) (xs :: [k]) :: [k] where-    ReplacesIndexImpl i ns ys '[] = '[]-    ReplacesIndexImpl i '[] '[] xs = xs-    ReplacesIndexImpl i ns ys (x ': xs) = ReplaceIfIndex ns ys i x ': ReplacesIndexImpl (i + 1) ns ys xs-    ReplacesIndexImpl i ns ys xs = TypeError ('Text "ReplacesIndex error: ‘"-                                       ':<>: 'ShowType ns-                                       ':<>: 'Text "’"-                                       ':<>: 'Text " must be the same size as "-                                       ':<>: 'Text "‘"-                                       ':<>: 'ShowType ys-                                       ':<>: 'Text "’")---- | Zips up @xs@ and @ys@, which must be the same length-type family ZipImpl (xs' :: [k]) (ys' :: [k]) (xs :: [k]) (ys :: [k]) :: [k] where-    ZipImpl xs' ys' '[] '[] = '[]-    ZipImpl xs' ys' (x ': xs) (y ': ys) = (x, y) ': ZipImpl xs' ys' xs ys-    ZipImpl xs' ys' xs ys = TypeError ('Text "Zip error: ‘"-                              ':<>: 'ShowType xs'-                              ':<>: 'Text "’"-                              ':<>: 'Text " must be the same size as "-                              ':<>: 'Text "‘"-                              ':<>: 'ShowType ys'-                              ':<>: 'Text "’")

@@ -0,0 +1,145 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE TypeInType #-}++module Data.Diverse.TypeLevel where++import Data.Diverse.TypeLevel.Internal+import Data.Kind+import GHC.TypeLits++-- | Ensures that @x@ is a unique member of @xs@, and that 'natVal' can be used.+type UniqueMember x xs = (Unique x xs, KnownNat (IndexOf x xs))++-- | 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)++-- | 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)++-- | Ensures that @x@ is a member of @xs@ at @n@ if it exists, and that 'natVal' can be used.+type MaybeMemberAt n x xs = (KnownNat n, KindAtPositionIs n x xs)++-- | Ensures x is a unique member in @xs@ iff it exists in @ys@+type family UniqueIfExists ys x xs :: Constraint where+    UniqueIfExists '[] x xs = ()+    UniqueIfExists (y ': ys) y xs = Unique y xs+    UniqueIfExists (y ': ys) x xs = UniqueIfExists ys x xs++-- | Ensures that the type list contain unique types+type IsDistinct (xs :: [k]) = IsDistinctImpl xs xs++-- | Return the list of distinct types in a typelist+type family Nub (xs :: [k]) :: [k] where+    Nub '[] = '[]+    Nub (x ': xs) = NubImpl xs x xs++-- | Ensures that @x@ only ever appears once in @xs@+type Unique (x :: k) (xs :: [k]) = UniqueImpl xs x xs++-- | Ensures that the @label@ in @tagged label v@ only ever appears once in @xs@.+type UniqueLabel (l :: k1) (xs :: [k]) = UniqueLabelImpl xs l xs++-- | Ensures that the @label@ list all 'UniqueLabel's+type family UniqueLabels (ls :: [k1]) (xs :: [k]) :: Constraint where+    UniqueLabels '[] xs = ()+    UniqueLabels (l ': ls) xs = (UniqueLabel l xs, UniqueLabels ls xs)++-- | Get the first index of a type (Indexed by 0)+-- Will result in type error if x doesn't exist in xs.+type IndexOf (x :: k) (xs :: [k]) = IndexOfImpl xs x xs++-- | Get the first index of a type (Indexed by 1)+-- Will return 0 if x doesn't exists in xs.+type PositionOf (x :: k) (xs :: [k]) = PositionOfImpl 0 x xs++-- | Get the type at an index+type KindAtIndex (n :: Nat) (xs :: [k]) = KindAtIndexImpl n xs n xs++-- | Get the type at a label+type KindAtLabel (l :: k1) (xs :: [k]) = KindAtLabelImpl l xs xs++-- | It's actually ok for the position to be zero, but if it's not zero then the types must match+type family KindAtPositionIs (n :: Nat) (x :: k) (xs :: [k]) :: Constraint where+    KindAtPositionIs 0 x xs = ()+    KindAtPositionIs n x xs = (x ~ KindAtIndexImpl (n - 1) xs (n - 1) xs)++-- | Get the types at an list of index+type family KindsAtIndices (ns :: [Nat]) (xs :: [k]) :: [k] where+    KindsAtIndices '[] xs = '[]+    KindsAtIndices (n ': ns) xs = KindAtIndex n xs ': KindsAtIndices ns xs++type family KindsAtLabels (ls :: [k1]) (xs :: [k]) :: [k] where+    KindsAtLabels '[] xs = '[]+    KindsAtLabels (l ': ls) xs = KindAtLabel l xs ': KindsAtLabels ls xs++-- | The typelist @xs@ without first @x@. It is okay for @x@ not to exist in @xs@+type family Without (x :: k) (xs :: [k]) :: [k] where+    Without x '[] = '[]+    Without x (x ': xs) = xs+    Without x (y ': xs) = y ': Without x xs++-- | The typelist @xs@ with the first @x@ replaced by @y@. It is okay for @x@ not to exist in @xs@+type Replace (x :: k) (y :: k) (xs :: [k]) = ReplaceImpl x y xs++-- | The typelist @zs@ with the first @xs@ replaced by @ys@.+-- @xs@ must be the same size as @ys@+type Replaces (xs :: [k]) (ys :: [k]) (zs :: [k]) = ReplacesImpl xs ys xs ys zs++-- | The typelist @xs@ without the type at Nat @n@. @n@ must be within bounds of @xs@+type WithoutIndex (n :: Nat) (xs :: [k]) = WithoutIndexImpl n xs n xs++-- | The typelist @xs@ without the type at Nat @n@ replaced by @y@. @n@ must be within bounds of @xs@+type ReplaceIndex (n :: Nat) (y :: k) (xs :: [k]) = ReplaceIndexImpl n xs n y xs++-- | The typelist @xs@ replaced by @ys@ at the indices @ns@. @ns@ and @ys@ must be the same length. @ns@ must be within bounds of @xs@+type ReplacesIndex (ns :: [Nat]) (ys :: [k]) (xs :: [k]) = ReplacesIndexImpl 0 ns ys xs++-- | Get the typelist without the 'Head' type+type family Tail (xs :: [k]) :: [k] where+    Tail '[] = TypeError ('Text "Tail error: empty type list")+    Tail (x ': xs) = xs++-- | Get the first type in a typelist+type family Head (xs :: [k]) :: k where+    Head '[] = TypeError ('Text "Head error: empty type list")+    Head (x ': xs) = x++-- | Get the last type in a typelist+type family Last (xs :: [k]) :: k where+    Last '[] = TypeError ('Text "Last error: empty type list")+    Last (x ': x' ': xs) = Last (x' ': xs)+    Last '[x] = x++-- | Ensures two typelists are the same length+type SameLength (xs :: [k1]) (ys :: [k2]) = SameLengthImpl xs ys xs ys++-- | Set complement. Returns the set of things in @xs@ that are not in @ys@.+type family Complement (xs :: [k]) (ys :: [k]) :: [k] where+    Complement xs '[] = xs+    Complement xs (y ': ys)  = Complement (Without y xs) ys++-- | Returns a @xs@ appended with @ys@+type family Append (xs :: [k]) (ys :: [k]) :: [k] where+    Append '[] ys = ys+    Append (x ': xs) ys = x ': Append xs ys++-- | Returns the typelist without the 'Last' type+type family Init (xs :: [k]) :: [k] where+    Init '[]  = TypeError ('Text "Init error: empty type list")+    Init '[x] = '[]+    Init (x ': xs) = x ': Init xs++-- | Takes two lists which must be the same length and returns a list of corresponding pairs.+type Zip (xs :: [k]) (ys :: [k]) = ZipImpl xs ys xs ys

@@ -0,0 +1,194 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++module Data.Diverse.TypeLevel.Internal where++import Data.Kind+import GHC.TypeLits++-- | Get the first position of a type (indexed by 1)+-- Will return 0 if @x@ doesn't exists in @xs@.+type family PositionOfImpl (i :: Nat) (x :: k) (xs :: [k]) :: Nat where+   PositionOfImpl i x (x ': xs) = i + 1+   PositionOfImpl i y (x ': xs) = PositionOfImpl (i + 1) y xs+   PositionOfImpl i x '[] = 0++-- | Get the first index of a type from a list+type family IndexOfImpl (ctx :: [k]) (x :: k) (xs :: [k]) :: Nat where+   IndexOfImpl ctx x (x ': xs) = 0+   IndexOfImpl ctx y (x ': xs) = 1 + IndexOfImpl ctx y xs+   IndexOfImpl ctx y '[] = TypeError ('Text "IndexOf error: ‘"+                                      ':<>: 'ShowType y+                                      ':<>: 'Text "’"+                                      ':<>: 'Text " is not a member of "+                                      ':<>: 'Text "‘"+                                      ':<>: 'ShowType ctx+                                      ':<>: 'Text "’")++-- | Searches for y in ys+-- if not found, than use y, and repeat search with next (y ': ys) in ctx+-- else if found, then don't use y, then repeat search with next (y ': ys) in ctx+type family NubImpl (ctx :: [k]) (y :: k) (ys :: [k]) :: [k] where+    NubImpl '[] y '[] = y ': '[]+    NubImpl '[] y (y ': xs) = '[]+    NubImpl (x ': xs) y '[] = y ': NubImpl xs x xs+    NubImpl (x ': xs) y (y ': ys) = NubImpl xs x xs+    NubImpl ctx y (x ': xs) = NubImpl ctx y xs++-- | Errors if a type exists in a typelist+type family MissingImpl (ctx :: [k]) (y :: k) (xs :: [k]) :: Constraint where+    MissingImpl ctx y '[] = ()+    MissingImpl ctx x (x ': xs) = TypeError ('Text "Not unique error: ‘"+                                             ':<>: 'ShowType x+                                             ':<>: 'Text "’"+                                             ':<>: 'Text " is a duplicate in "+                                             ':<>: 'Text "‘"+                                             ':<>: 'ShowType ctx+                                             ':<>: 'Text "’")+    MissingImpl ctx y (x ': xs) = (MissingImpl ctx y xs)++-- | Errors if a label exists in a typelist+type family MissingLabelImpl (ctx :: [k]) (l :: k2) (xs :: [k]) :: Constraint where+    MissingLabelImpl ctx y '[] = ()+    MissingLabelImpl ctx l (tagged l x ': xs) = TypeError ('Text "Not unique label error: ‘"+                                             ':<>: 'ShowType l+                                             ':<>: 'Text "’"+                                             ':<>: 'Text " is a duplicate in "+                                             ':<>: 'Text "‘"+                                             ':<>: 'ShowType ctx+                                             ':<>: 'Text "’")+    MissingLabelImpl ctx l (x ': xs) = (MissingLabelImpl ctx l xs)++-- | Ensures that the type list contain unique types.+-- Not implemented as @(xs ~ Nub xs)@ for better type error messages.+type family IsDistinctImpl (ctx :: [k]) (xs :: [k]) :: Constraint where+    IsDistinctImpl ctx '[] = ()+    IsDistinctImpl ctx (x ': xs) = (MissingImpl ctx x xs, IsDistinctImpl ctx xs)++-- | Ensures that @x@ only ever appears once in @xs@+type family UniqueImpl (ctx :: [k]) (x :: k) (xs :: [k]) :: Constraint where+    UniqueImpl ctx x '[] = ()+    UniqueImpl ctx x (x ': xs) = MissingImpl ctx x xs+    UniqueImpl ctx x (y ': xs) = UniqueImpl ctx x xs++-- | Ensures that the @label@ in @tagged label v@ only ever appears once in @xs@.+type family UniqueLabelImpl (ctx :: [k]) (l :: k1) (xs :: [k]) :: Constraint where+    UniqueLabelImpl ctx l '[] = ()+    UniqueLabelImpl ctx l (tagged l x ': xs) = MissingLabelImpl ctx l xs+    UniqueLabelImpl ctx l (y ': xs) = UniqueLabelImpl ctx l xs++-- | Indexed access into the list+type family KindAtIndexImpl (orig :: Nat) (ctx :: [k]) (n :: Nat) (xs :: [k]) :: k where+    KindAtIndexImpl i ctx 0 '[] = TypeError ('Text "KindAtIndex error: Index ‘"+                                       ':<>: 'ShowType i+                                       ':<>: 'Text "’"+                                       ':<>: 'Text " is out of bounds of "+                                       ':<>: 'Text "‘"+                                       ':<>: 'ShowType ctx+                                       ':<>: 'Text "’")+    KindAtIndexImpl i ctx 0 (x ': xs) = x+    KindAtIndexImpl i ctx n (x ': xs) = KindAtIndexImpl i ctx (n - 1) xs++-- | Labelled access into the list+type family KindAtLabelImpl (l :: k1) (ctx :: [k]) (xs :: [k]) :: k where+    KindAtLabelImpl l ctx '[] = TypeError ('Text "KindAtLabel error: Label ‘"+                                       ':<>: 'ShowType l+                                       ':<>: 'Text "’"+                                       ':<>: 'Text " is not found in "+                                       ':<>: 'Text "‘"+                                       ':<>: 'ShowType ctx+                                       ':<>: 'Text "’")+    KindAtLabelImpl l ctx (tagged l x ': xs) = tagged l x+    KindAtLabelImpl l ctx (x ': xs) = KindAtLabelImpl l ctx xs++-- | Ensures two typelists are the same length+type family SameLengthImpl (ctx :: [k1]) (cty :: [k2]) (xs :: [k1]) (yx :: [k2]) :: Constraint where+    SameLengthImpl as bs '[] '[] = ()+    SameLengthImpl as bs (x ': xs) (y ': ys) = SameLengthImpl as bs xs ys+    SameLengthImpl as bs xs ys = TypeError ('Text "SameLength error: ‘"+                                            ':<>: 'ShowType as+                                            ':<>: 'Text "’"+                                            ':<>: 'Text " is not the same length as "+                                            ':<>: 'Text "‘"+                                            ':<>: 'ShowType bs+                                            ':<>: 'Text "’")++-- | The typelist @xs@ without the type at Nat @n@. @n@ must be within bounds of @xs@+type family WithoutIndexImpl (i :: Nat) (ctx :: [k]) (n :: Nat) (xs :: [k]) :: [k] where+    WithoutIndexImpl i ctx n '[] = TypeError ('Text "WithoutIndex error: Index ‘"+                                       ':<>: 'ShowType i+                                       ':<>: 'Text "’"+                                       ':<>: 'Text " is out of bounds of "+                                       ':<>: 'Text "‘"+                                       ':<>: 'ShowType ctx+                                       ':<>: 'Text "’")+    WithoutIndexImpl i ctx 0 (x ': xs) = xs+    WithoutIndexImpl i ctx n (x ': xs) = x ': WithoutIndexImpl i ctx (n - 1) xs++-- | The typelist @xs@ without the type at Nat @n@ replaced by @y@. @n@ must be within bounds of @xs@+type family ReplaceIndexImpl (i :: Nat) (ctx :: [k]) (n :: Nat) (y :: k) (xs :: [k]) :: [k] where+    ReplaceIndexImpl i ctx n y '[] = TypeError ('Text "ReplaceIndex error: Index ‘"+                                       ':<>: 'ShowType i+                                       ':<>: 'Text "’"+                                       ':<>: 'Text " is out of bounds of "+                                       ':<>: 'Text "‘"+                                       ':<>: 'ShowType ctx+                                       ':<>: 'Text "’")+    ReplaceIndexImpl i ctx 0 y (x ': xs) = y ': xs+    ReplaceIndexImpl i ctx n y (x ': xs) = x ': ReplaceIndexImpl i ctx (n - 1) y xs++-- | The typelist @xs@ with the first @x@ replaced by @y@. It is okay for @x@ not to exist in @xs@+type family ReplaceImpl (x :: k) (y :: k) (xs :: [k]) :: [k] where+    ReplaceImpl x y '[] = '[]+    ReplaceImpl x y (x ': xs) = y ': xs+    ReplaceImpl x y (z ': xs) = z ': ReplaceImpl x y xs++-- | The typelist @zs@ with the first @xs@ replaced by @ys@.+-- @xs@ must be the same size as @ys@+type family ReplacesImpl (xs' :: [k]) (ys' :: [k]) (xs :: [k]) (ys :: [k]) (zs :: [k]) :: [k] where+    ReplacesImpl xs' ys' xs ys '[] = '[]+    ReplacesImpl xs' ys' '[] '[] (z ': zs) = z ': ReplacesImpl xs' ys' xs' ys' zs+    ReplacesImpl xs' ys' (x ': xs) (y ': ys) (x ': zs) = y ': ReplacesImpl xs' ys' xs' ys' zs+    ReplacesImpl xs' ys' (x ': xs) (y ': ys) (z ': zs) = ReplacesImpl xs' ys' xs ys (z ': zs)+    ReplacesImpl xs' ys' xs ys zs = TypeError ('Text "Replaces error: ‘"+                                       ':<>: 'ShowType xs'+                                       ':<>: 'Text "’"+                                       ':<>: 'Text " must be the same size as "+                                       ':<>: 'Text "‘"+                                       ':<>: 'ShowType ys'+                                       ':<>: 'Text "’")++-- | The type @x@ replaced by an @y@ if an @n@ matches @i@.+type family ReplaceIfIndex (ns :: [Nat]) (ys :: [k]) (i :: Nat) (x :: k) :: k where+    ReplaceIfIndex '[] ys i x = x+    ReplaceIfIndex ns '[] i x = x+    ReplaceIfIndex (n ': ns) (y ': ys) n x = y+    ReplaceIfIndex (n ': ns) (y ': ys) i x = ReplaceIfIndex ns ys i x++-- | The typelist @xs@ replaced by @ys@ at the indices @ns@. @ns@ and @ys@ must be the same length. @ns@ must be within bounds of @xs@+type family ReplacesIndexImpl (i :: Nat) (ns :: [Nat]) (ys :: [k]) (xs :: [k]) :: [k] where+    ReplacesIndexImpl i ns ys '[] = '[]+    ReplacesIndexImpl i '[] '[] xs = xs+    ReplacesIndexImpl i ns ys (x ': xs) = ReplaceIfIndex ns ys i x ': ReplacesIndexImpl (i + 1) ns ys xs+    ReplacesIndexImpl i ns ys xs = TypeError ('Text "ReplacesIndex error: ‘"+                                       ':<>: 'ShowType ns+                                       ':<>: 'Text "’"+                                       ':<>: 'Text " must be the same size as "+                                       ':<>: 'Text "‘"+                                       ':<>: 'ShowType ys+                                       ':<>: 'Text "’")++-- | Zips up @xs@ and @ys@, which must be the same length+type family ZipImpl (xs' :: [k]) (ys' :: [k]) (xs :: [k]) (ys :: [k]) :: [k] where+    ZipImpl xs' ys' '[] '[] = '[]+    ZipImpl xs' ys' (x ': xs) (y ': ys) = (x, y) ': ZipImpl xs' ys' xs ys+    ZipImpl xs' ys' xs ys = TypeError ('Text "Zip error: ‘"+                              ':<>: 'ShowType xs'+                              ':<>: 'Text "’"+                              ':<>: 'Text " must be the same size as "+                              ':<>: 'Text "‘"+                              ':<>: 'ShowType ys'+                              ':<>: 'Text "’")

@@ -70,7 +70,7 @@ import Data.Diverse.Case import Data.Diverse.Reduce import Data.Diverse.Reiterate-import Data.Diverse.Type+import Data.Diverse.TypeLevel import Data.Kind import Data.Proxy import qualified GHC.Generics as G@@ -322,7 +322,7 @@ ------------------------------------------------------------------  -- | A friendlier constraint synonym for 'diversify'.-type Diversify (tree :: [Type]) (branch :: [Type]) = Reduce Which (Switch (CaseDiversify tree branch)) branch (Which tree)+type Diversify (tree :: [Type]) (branch :: [Type]) = Reduce (Which branch) (Switch (CaseDiversify tree branch) branch) (Which tree)  -- | Convert a 'Which' to another 'Which' that may include other possibilities. -- That is, @branch@ is equal or is a subset of @tree@.@@ -378,7 +378,9 @@ ------------------------------------------------------------------  -- | A friendlier constraint synonym for 'diversifyN'.-type DiversifyN (indices :: [Nat]) (tree :: [Type]) (branch :: [Type]) = (Reduce Which (SwitchN (CaseDiversifyN indices) 0) (KindsAtIndices indices tree) (Which tree), KindsAtIndices indices tree ~ branch)+type DiversifyN (indices :: [Nat]) (tree :: [Type]) (branch :: [Type]) =+    ( Reduce (Which branch) (SwitchN (CaseDiversifyN indices) 0 branch) (Which tree)+    , KindsAtIndices indices tree ~ branch)  -- | A variation of 'diversify' which uses a Nat list @indices@ to specify how to reorder the fields, where --@@ -410,7 +412,7 @@ ------------------------------------------------------------------  -- | A friendlier constraint synonym for 'reinterpret'.-type Reinterpret branch tree = Reduce Which (Switch (CaseReinterpret branch tree)) tree (Either (Which (Complement tree branch)) (Which branch))+type Reinterpret branch tree = Reduce (Which tree) (Switch (CaseReinterpret branch tree) tree) (Either (Which (Complement tree branch)) (Which branch))  -- | Convert a 'Which' into possibly another 'Which' with a totally different typelist. -- Returns either a 'Which' with the 'Right' value, or a 'Which' with the 'Left'over @compliment@ types.@@ -472,7 +474,9 @@ ------------------------------------------------------------------  -- | A friendlier constraint synonym for 'reinterpretN'.-type ReinterpretN (indices :: [Nat]) (branch :: [Type]) (tree :: [Type]) = (Reduce Which (SwitchN (CaseReinterpretN indices) 0) tree (Maybe (Which (KindsAtIndices indices tree))), KindsAtIndices indices tree ~ branch)+type ReinterpretN (indices :: [Nat]) (branch :: [Type]) (tree :: [Type]) =+    ( Reduce (Which tree) (SwitchN (CaseReinterpretN indices) 0 tree) (Maybe (Which branch))+    , KindsAtIndices indices tree ~ branch)  -- | A limited variation of 'reinterpret' which uses a Nat list @n@ to specify how to reorder the fields, where --@@ -571,24 +575,26 @@  -- | 'trial0' each type in a 'Which', and either handle the 'case'' with value discovered, or __'reiterate'__ -- trying the next type in the type list.-instance (Case c (x ': x' ': xs) r, Reduce Which (Switch c) (x' ': xs) r, Reiterate c (x : x' : xs)) =>-         Reduce Which (Switch c) (x ': x' ': xs) r where+instance (Case c (x ': x' ': xs) r, Reduce (Which (x' ': xs)) (Switch c (x' ': xs)) r, Reiterate c (x : x' : xs)) =>+         Reduce (Which (x ': x' ': xs)) (Switch c (x ': x' ': xs)) r where     reduce (Switch c) v =         case trial0 v of             Right a -> case' c a             Left v' -> reduce (Switch (reiterate c)) v'     -- GHC compilation is SLOW if there is no pragma for recursive typeclass functions for different types-    {-# NOINLINE reduce #-}+    -- Using INLINEABLE instead of NOLINE so that ghc 8.2.1 can optimize to single case statement+    -- See https://ghc.haskell.org/trac/ghc/ticket/12877+    {-# INLINEABLE reduce #-}  -- | Terminating case of the loop, ensuring that a instance of @Case '[]@ -- with an empty typelist is not required. -- You can't reduce 'impossible'-instance (Case c '[x] r) => Reduce Which (Switch c) '[x] r where+instance (Case c '[x] r) => Reduce (Which '[x]) (Switch c '[x]) r where     reduce (Switch c) v = case obvious v of             a -> case' c a  -- | Catamorphism for 'Which'. This is equivalent to @flip 'switch'@.-which :: Reduce Which (Switch case') xs r => case' xs r -> Which xs -> r+which :: Reduce (Which xs) (Switch case' xs) r => case' xs r -> Which xs -> r which = reduce . Switch  -- | A switch/case statement for 'Which'. This is equivalent to @flip 'which'@@@ -611,7 +617,7 @@ -- @ -- -- Or you may use your own custom instance of 'Case'.-switch :: Reduce Which (Switch case') xs r => Which xs -> case' xs r -> r+switch :: Reduce (Which xs) (Switch case' xs) r => Which xs -> case' xs r -> r switch = flip which  ------------------------------------------------------------------@@ -622,24 +628,26 @@  -- | 'trial0' each type in a 'Which', and either handle the 'case'' with value discovered, or __'reiterateN'__ -- trying the next type in the type list.-instance (Case (c n) (x ': x' ': xs) r, Reduce Which (SwitchN c (n + 1)) (x' ': xs) r, ReiterateN c n (x : x' : xs)) =>-         Reduce Which (SwitchN c n) (x ': x' ': xs) r where+instance (Case (c n) (x ': x' ': xs) r, Reduce (Which (x' ': xs)) (SwitchN c (n + 1) (x' ': xs)) r, ReiterateN c n (x : x' : xs)) =>+         Reduce (Which (x ': x' ': xs)) (SwitchN c n (x ': x' ': xs)) r where     reduce (SwitchN c) v =         case trial0 v of             Right a -> case' c a             Left v' -> reduce (SwitchN (reiterateN c)) v'     -- GHC compilation is SLOW if there is no pragma for recursive typeclass functions for different types-    {-# NOINLINE reduce #-}+    -- Using INLINEABLE instead of NOLINE so that ghc 8.2.1 can optimize to single case statement+    -- See https://ghc.haskell.org/trac/ghc/ticket/12877+    {-# INLINEABLE reduce #-}  -- | Terminating case of the loop, ensuring that a instance of @Case '[]@ -- with an empty typelist is not required. -- You can't reduce 'impossible'-instance (Case (c n) '[x] r) => Reduce Which (SwitchN c n) '[x] r where+instance (Case (c n) '[x] r) => Reduce (Which '[x]) (SwitchN c n '[x]) r where     reduce (SwitchN c) v = case obvious v of             a -> case' c a  -- | Catamorphism for 'Which'. This is equivalent to @flip 'switchN'@.-whichN :: Reduce Which (SwitchN case' n) xs r => case' n xs r -> Which xs -> r+whichN :: Reduce (Which xs) (SwitchN case' n xs) r => case' n xs r -> Which xs -> r whichN = reduce . SwitchN  -- | A switch/case statement for 'Which'. This is equivalent to @flip 'whichN'@@@ -658,13 +666,13 @@ -- @ -- -- Or you may use your own custom instance of 'Case'.-switchN :: Reduce Which (SwitchN case' n) xs r => Which xs -> case' n xs r -> r+switchN :: Reduce (Which xs) (SwitchN case' n xs) r => Which xs -> case' n xs r -> r switchN = flip whichN  -----------------------------------------------------------------  -- | Two 'Which'es are only equal iff they both contain the equivalnet value at the same type index.-instance (Reduce Which (Switch CaseEqWhich) (x ': xs) Bool) => Eq (Which (x ': xs)) where+instance (Reduce (Which (x ': xs)) (Switch CaseEqWhich (x ': xs)) Bool) => Eq (Which (x ': xs)) where     l@(Which i _) == (Which j u) =         if i /= j             then False@@ -687,7 +695,10 @@ -----------------------------------------------------------------  -- | A 'Which' with a type at smaller type index is considered smaller.-instance (Reduce Which (Switch CaseEqWhich) (x ': xs) Bool, Reduce Which (Switch CaseOrdWhich) (x ': xs) Ordering) => Ord (Which (x ': xs)) where+instance ( Reduce (Which (x ': xs)) (Switch CaseEqWhich (x ': xs)) Bool+         , Reduce (Which (x ': xs)) (Switch CaseOrdWhich (x ': xs)) Ordering+         ) =>+         Ord (Which (x ': xs)) where     compare l@(Which i _) (Which j u) =         if i /= j             then compare i j@@ -710,7 +721,7 @@ ------------------------------------------------------------------  -- | @show ('pick'' \'A') == "pick \'A'"@-instance (Reduce Which (Switch CaseShowWhich) (x ': xs) ShowS) => Show (Which (x ': xs)) where+instance (Reduce (Which (x ': xs)) (Switch CaseShowWhich (x ': xs)) ShowS) => Show (Which (x ': xs)) where     showsPrec d v = showParen (d > app_prec) (which (CaseShowWhich 0) v)       where app_prec = 10 @@ -750,7 +761,9 @@     whichReadPrec i j = readWhich_ i j                <|> (diversify0' <$> (whichReadPrec i (j + 1) :: ReadPrec (Which_ (x' ': xs))))     -- GHC compilation is SLOW if there is no pragma for recursive typeclass functions for different types-    {-# NOINLINE whichReadPrec #-}+    -- Using INLINEABLE instead of NOLINE so that ghc 8.2.1 can optimize to single case statement+    -- See https://ghc.haskell.org/trac/ghc/ticket/12877+    {-# INLINEABLE whichReadPrec #-}   -- | This 'Read' instance tries to read using the each type in the typelist, using the first successful type read.

@@ -29,7 +29,7 @@             fromIntegral (natVal @(PositionOf Int '[Bool, String, Char]) Proxy) `shouldBe` (0 :: Int)          it "ComplementOf" $ do-            let complementTest :: (Complement xs ys ~ comp) => Proxy xs -> Proxy ys -> Proxy comp -> Proxy comp+            let complementTest :: Proxy xs -> Proxy ys -> Proxy (Complement xs ys) -> Proxy (Complement xs ys)                 complementTest _ _ comp = comp              complementTest (Proxy @[String, Int]) (Proxy @[Bool, Int]) (Proxy @'[String]) `shouldBe` Proxy