exinst 0.2 → 0.3

raw patch · 14 files changed

+1552/−418 lines, 14 filesdep +QuickCheckdep +aesondep +bytesdep ~basedep ~constraintsdep ~profunctorsPVP ok

version bump matches the API change (PVP)

Dependencies added: QuickCheck, aeson, bytes, deepseq, exinst, generic-random, hashable, tasty, tasty-hunit, tasty-quickcheck

Dependency ranges changed: base, constraints, profunctors, singletons

API changes (from Hackage documentation)

Files

• CHANGELOG.md +45/−1
• LICENSE.txt +1/−1
• README.md +15/−48
• exinst.cabal +68/−6
• src/lib/Exinst.hs +79/−0
• src/lib/Exinst/Instances/Aeson.hs +159/−0
• src/lib/Exinst/Instances/Base.hs +259/−9
• src/lib/Exinst/Instances/Bytes.hs +118/−0
• src/lib/Exinst/Instances/DeepSeq.hs +60/−0
• src/lib/Exinst/Instances/Hashable.hs +99/−0
• src/lib/Exinst/Instances/QuickCheck.hs +106/−0
• src/lib/Exinst/Internal.hs +361/−0
• src/lib/Exinst/Singletons.hs +0/−353
• tests/Main.hs +182/−0

@@ -1,10 +1,54 @@+# Version 0.3++* BREAKING: Renamed module `Exinst.Singletons` to  `Exinst`.++* BREAKING: The `Exinst.Instances.Base` module is gone. The `base` instances are+  now exported from `Exinst`.++* Add `Dict0`.++* Re-export `Constraint` from `base`.++* Add `Dict{0,2,3,4}` instances for `Bool`.++* Add `GHC.Generics.Generic` support for `Some{1,2,3,4}`. This only works for+  indexes with `PEnum` and `PBounded` instances.++* Added tests.++* Added `Test.QuickCheck.Arbitrary` instances for `Some{1,2,3,4}` in+  `Exinst.Instances.QuickCheck`. These instances and their dependency on+  `QuickCheck` can be toggled with the `quickcheck` Cabal flag.++* Added `Data.Aeson.{FromJSON,ToJSON}` instances for `Some{1,2,3,4}` in+  `Exinst.Instances.Aeson`. These instances and their dependency on+  `aeson` can be toggled with the `aeson` Cabal flag. These instances used to+  exist in now-deprecated the `exinst-aeson` package, and are compatible with+  them.++* Added `Bytes.Serial.Serial` instances for `Some{1,2,3,4}` in+  `Exinst.Instances.Bytes`. These instances and their dependency on `bytes` can+  be toggled with the `bytes` Cabal flag. These instances used to exist in+  now-deprecated the `exinst-bytes` package, and are compatible with them.++* Added `Control.DeepSeq.NFData` instances for `Some{1,2,3,4}` in+  `Exinst.Instances.DeepSeq`. These instances and their dependency on `deepseq`+  can be toggled with the `deepseq` Cabal flag. These instances used to exist in+  now-deprecated the `exinst-deepseq` package, and are compatible with them.++* Added `Data.Hashable.Hashable` instances for `Some{1,2,3,4}` in+  `Exinst.Instances.DeepSeq`. These instances and their dependency on `hashable`+  can be toggled with the `hashable` Cabal flag. These instances used to exist+  in now-deprecated the `exinst-hashable` package, and are compatible with them.++ # Version 0.2  * Depend on `singletons-2.2`, which means `KProxy` is gone.  * Add `_Some{1,2,3,4}` prisms. -* Add `Dict` instance for `Bool`.+* Add `Dict1` instance for `Bool`.  * Add `some{1,2,3,4}SingRep`. 

@@ -1,4 +1,4 @@-Copyright (c) 2015-2016, Renzo Carbonara+Copyright (c) 2015-2017, Renzo Carbonara  All rights reserved. 

@@ -1,5 +1,7 @@ # exinst +[![Build Status](https://travis-ci.org/k0001/exinst.svg?branch=master)](https://travis-ci.org/k0001/exinst)+ > See the [BSD3 LICENSE](https://github.com/k0001/exinst/blob/master/exinst/LICENSE.txt) > file to learn about the legal terms and conditions for this library. @@ -50,7 +52,7 @@ `Receptacle` can describe three types of receptacles (`Vase`, `Glass` and `Barrel`), while at the same time being able to indicate, at the type level, whether the size of the receptacle is `Big` or `Small`. Additionally, we've-provided `Show` instances for `Receptacle`. +provided `Show` instances for `Receptacle`.  Now, if we want to put `Receptacle`s in a container, for example in `[]`, we can do so only as long as the `Receptacle` type is fully applied and monomorphic. That is, we can@@ -182,7 +184,7 @@ Note: this code won't work yet. Keep reading.  ```-> import Exinst.Singletons (some1)+> import Exinst (some1) > import Exinst.Instances.Base () > :t some1 Glass :t some1 Glass :: Some1 Receptacle@@ -218,7 +220,7 @@ type.  ```haskell--- The Exinst.Singletons.Dict1 class+-- The Exinst.Dict1 class class Dict1 (c :: * -> Constraint) (f1 :: k1 -> *) where   dict1 :: Sing (a1 :: k1) -> Dict (c (f1 a1)) ```@@ -282,25 +284,21 @@ with `Some1`, nor with the choice of `f` nor with the choice of `c`; it is only related to the singleton type used as a type-index for `f`. -As of this writing, we can find some ready-made instances for `Some1`, `Some2`,-`Some3` and `Some4` in the following modules, which you need to import so as to-bring to scope the desired instances at their usage site:+The `Exinst` module exports ready-made instances for `Some1`, `Some2`, `Some3`+and `Some4` (they can be enabled with some cabal flags). -* Package `exinst`, module `Exinst.Instances.Base`: Instances for various-  type-classes found in the `base` package: `Eq`, `Ord`, `Show`.+* `Eq`, `Ord`, `Show` from the `base` package. -* Package `exinst-aeson`, module `Exinst.Instances.Aeson`: Instances for-  `FromJSON` and `ToJSON` from the `aeson` package.+* `FromJSON` and `ToJSON` from the `aeson` package. -* Package `exinst-bytes`, module `Exinst.Instances.Bytes`: Instances for-  `Serial` from the `bytes` package.+* `Serial` from the `bytes` package. -* Package `exinst-hashable`, module `Exinst.Instances.Hashable`: Instances for-  `Hashable` from the `hashable` package.+* `Hashable` from the `hashable` package. -* Package `exinst-deepseq`, module `Exinst.Instances.DeepSeq`: Instances for-  `NFData` from the `deepseq` package.+* `NFData` from the `deepseq` package. +* `Arbitrary` from the `QuickCheck` package.+ You are invited to read the instance heads for said instances so as to understand what you need to provide in order to get those instances “for free”. As a rule of thumb, most instances will require this: If you expect to have an instance for@@ -309,10 +307,6 @@ (f :: k -> *)` or more general instance exists, and that the `Y` instance for `Some1 (f :: k -> *)` exists too. -> TODO: Have something similar to `Dict1` and friends for working with-> non-singleton types, possibly integrating with 'Data.Constraint.Forall.ForallT'-> if it made sense to do so.- Here is the full code needed to have, say, the `Eq`, `Show`, `ToJSON` and `FromJSON` instances available for `Some1 Receptacle`: @@ -332,7 +326,7 @@ import qualified Data.Aeson as Ae import           Data.Constraint (Dict(Dict)) import qualified Data.Singletons.TH-import           Exinst.Singletons (Dict1(dict1))+import           Exinst (Dict1(dict1))  ----- @@ -536,30 +530,3 @@ using `Read`.  -# Related work on Generic instances for GADTs--One of the most appealing applications of `exinst` is to reduce the boilerplate-associated with manually writing instances for existentialized GADTs. However,-quite often, writing instances for said GADTs on its own is very cumbersome-due to the lack of generic instance deriving mechanisms for GADTs. There exists,-however, at the time of this writing, at least one library able to derive-generic representations for some GADTs using TH:-[`instant-generics`](https://hackage.haskell.org/package/instant-generics).--Combining [`instant-generics`](https://hackage.haskell.org/package/instant-generics) (and-[`instant-aeson`](https://hackage.haskell.org/package/instant-aeson),-[`instant-hashable`](https://hackage.haskell.org/package/instant-hashable),-[`instant-bytes`](https://hackage.haskell.org/package/instant-bytes) and-[`instant-deepseq`](https://hackage.haskell.org/package/instant-deepseq))-with [`exinst`](https://hackage.haskell.org/package/exinst) (and-[`exinst-aeson`](https://hackage.haskell.org/package/exinst-aeson),-[`exinst-hashable`](https://hackage.haskell.org/package/exinst-hashable),-[`exinst-bytes`](https://hackage.haskell.org/package/exinst-bytes) and-[`exinst-deepseq`](https://hackage.haskell.org/package/exinst-deepseq)),-you can reduce a lot of the boilerplate associated with working with GADTs, in-particular when it comes to the serialization and deserialization of them (i.e.,-`Show` and `Read`, or `ToJSON` and `FromJSON`) or puting GADTs in monomorphic-containers (i.e., `[]` or `HashMap`), which become straightforward things to do-once you are able able to both generically derive the instances for your GADT-and then existentialize away the type-index while keeping the underlying-instances available.

@@ -1,8 +1,8 @@ name:                exinst-version:             0.2+version:             0.3 author:              Renzo Carbonara maintainer:          renzoλcarbonara.com.ar-copyright:           Renzo Carbonara 2015-2016+copyright:           Renzo Carbonara 2015-2017 license:             BSD3 license-file:        LICENSE.txt extra-source-files:  README.md CHANGELOG.md@@ -18,12 +18,74 @@   hs-source-dirs: src/lib   default-language: Haskell2010   exposed-modules:-      Exinst.Singletons+      Exinst+  other-modules:+      Exinst.Internal       Exinst.Instances.Base   build-depends:       base >=4.9 && <5.0-    , constraints >=0.4 && <0.9-    , profunctors >=5.0 && <6.0-    , singletons >=2.2 && <2.3+    , constraints >=0.4+    , profunctors >=5.0+    , singletons >=2.2   ghcjs-options: -Wall -O3   ghc-options: -Wall -O2++  if flag(aeson)+    build-depends: aeson+    other-modules: Exinst.Instances.Aeson+  if flag(bytes)+    build-depends: bytes >=0.15 && <0.16+    other-modules: Exinst.Instances.Bytes+  if flag(deepseq)+    build-depends: deepseq+    other-modules: Exinst.Instances.DeepSeq+  if flag(hashable)+    build-depends: hashable+    other-modules: Exinst.Instances.Hashable+  if flag(quickcheck)+    build-depends: QuickCheck+    other-modules: Exinst.Instances.QuickCheck+++test-suite tests+  default-language: Haskell2010+  type: exitcode-stdio-1.0+  hs-source-dirs: tests+  main-is: Main.hs+  build-depends:+     aeson+   , base+   , bytes+   , constraints+   , deepseq+   , exinst+   , generic-random >=0.4+   , hashable+   , profunctors+   , QuickCheck+   , singletons+   , tasty+   , tasty-hunit+   , tasty-quickcheck+++flag aeson+  description: Provide instances for @aeson@+  default: True+  manual: True+flag bytes+  description: Provide instances for @bytes@+  default: True+  manual: True+flag deepseq+  description: Provide instances for @deepseq@+  default: True+  manual: True+flag hashable+  description: Provide instances for @hashable@+  default: True+  manual: True+flag quickcheck+  description: Provide instances for @QuickCheck@+  default: True+  manual: True

@@ -0,0 +1,79 @@+{-# LANGUAGE CPP #-}++-- | See the README file for documentation: https://hackage.haskell.org/package/exinst#readme+module Exinst+ ( -- * 1 type index+   Some1(Some1)+ , some1+ , fromSome1+ , _Some1+ , withSome1+ , withSome1Sing+ , some1SingRep+ , Dict1(dict1)++   -- * 2 type indexes+ , Some2(Some2)+ , some2+ , fromSome2+ , _Some2+ , withSome2+ , withSome2Sing+ , some2SingRep+ , Dict2(dict2)++   -- * 3 type indexes+ , Some3(Some3)+ , some3+ , fromSome3+ , _Some3+ , withSome3+ , withSome3Sing+ , some3SingRep+ , Dict3(dict3)++   -- * 4 type indexes+ , Some4(Some4)+ , some4+ , fromSome4+ , _Some4+ , withSome4+ , withSome4Sing+ , some4SingRep+ , Dict4(dict4)++   -- * Miscellaneous+ , Dict0(dict0)++   -- * Re-exports+ , Constraint+ , Dict(Dict)+ ) where++import Data.Constraint (Constraint, Dict(Dict))++import Exinst.Internal++#ifdef VERSION_aeson+import Exinst.Instances.Aeson ()+#endif++#ifdef VERSION_bytes+import Exinst.Instances.Bytes ()+#endif++#ifdef VERSION_bytes+import Exinst.Instances.Base ()+#endif++#ifdef VERSION_bytes+import Exinst.Instances.DeepSeq ()+#endif++#ifdef VERSION_bytes+import Exinst.Instances.Hashable ()+#endif++#ifdef VERSION_QuickCheck+import Exinst.Instances.QuickCheck ()+#endif

@@ -0,0 +1,159 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE UndecidableInstances #-}++{-# OPTIONS_GHC -fno-warn-orphans #-}++-- | This module exports 'Ae.FromJSON' and 'Ae.ToJSON' instances for 'Some1',+-- 'Some2', 'Some3' and 'Some4' from "Exinst", provided situable+-- 'Dict1', 'Dict2', 'Dict3' and 'Dict4' instances are available.+--+-- See the README file in the @exinst@ package for more general documentation:+-- https://hackage.haskell.org/package/exinst#readme+module Exinst.Instances.Aeson () where++import qualified Data.Aeson as Ae+import Data.Constraint+import Data.Singletons+import Prelude++import Exinst.Internal++--------------------------------------------------------------------------------++instance forall (f1 :: k1 -> *)+  . ( SingKind k1+    , Ae.ToJSON (DemoteRep k1)+    , Dict1 Ae.ToJSON f1+    ) => Ae.ToJSON (Some1 f1)+  where+    {-# INLINABLE toJSON #-}+    toJSON = \some1x -> withSome1Sing some1x $ \sa1 (x :: f1 a1) ->+       case dict1 sa1 :: Dict (Ae.ToJSON (f1 a1)) of+          Dict -> Ae.toJSON (fromSing sa1, x)++instance forall (f2 :: k2 -> k1 -> *)+  . ( SingKind k2+    , SingKind k1+    , Ae.ToJSON (DemoteRep k2)+    , Ae.ToJSON (DemoteRep k1)+    , Dict2 Ae.ToJSON f2+    ) => Ae.ToJSON (Some2 f2)+  where+    {-# INLINABLE toJSON #-}+    toJSON = \some2x -> withSome2Sing some2x $ \sa2 sa1 (x :: f2 a2 a1) ->+       case dict2 sa2 sa1 :: Dict (Ae.ToJSON (f2 a2 a1)) of+          Dict -> Ae.toJSON ((fromSing sa2, fromSing sa1), x)++instance forall (f3 :: k3 -> k2 -> k1 -> *)+  . ( SingKind k3+    , SingKind k2+    , SingKind k1+    , Ae.ToJSON (DemoteRep k3)+    , Ae.ToJSON (DemoteRep k2)+    , Ae.ToJSON (DemoteRep k1)+    , Dict3 Ae.ToJSON f3+    ) => Ae.ToJSON (Some3 f3)+  where+    {-# INLINABLE toJSON #-}+    toJSON = \some3x -> withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f3 a3 a2 a1) ->+       case dict3 sa3 sa2 sa1 :: Dict (Ae.ToJSON (f3 a3 a2 a1)) of+          Dict -> Ae.toJSON ((fromSing sa3, fromSing sa2, fromSing sa1), x)++instance forall (f4 :: k4 -> k3 -> k2 -> k1 -> *)+  . ( SingKind k4+    , SingKind k3+    , SingKind k2+    , SingKind k1+    , Ae.ToJSON (DemoteRep k4)+    , Ae.ToJSON (DemoteRep k3)+    , Ae.ToJSON (DemoteRep k2)+    , Ae.ToJSON (DemoteRep k1)+    , Dict4 Ae.ToJSON f4+    ) => Ae.ToJSON (Some4 f4)+  where+    {-# INLINABLE toJSON #-}+    toJSON = \some4x -> withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f4 a4 a3 a2 a1) ->+       case dict4 sa4 sa3 sa2 sa1 :: Dict (Ae.ToJSON (f4 a4 a3 a2 a1)) of+          Dict -> Ae.toJSON ((fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1), x)++--------------------------------------------------------------------------------++instance forall (f1 :: k1 -> *)+  . ( SingKind k1+    , Ae.FromJSON (DemoteRep k1)+    , Dict1 Ae.FromJSON f1+    ) => Ae.FromJSON (Some1 f1)+  where+    {-# INLINABLE parseJSON #-}+    parseJSON = \v -> do+      (rsa1, v') <- Ae.parseJSON v+      withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> withSingI sa1 $+         case dict1 sa1 :: Dict (Ae.FromJSON (f1 a1)) of+            Dict -> do+               x :: f1 a1 <- Ae.parseJSON v'+               return (some1 x)++instance forall (f2 :: k2 -> k1 -> *)+  . ( SingKind k2+    , SingKind k1+    , Ae.FromJSON (DemoteRep k2)+    , Ae.FromJSON (DemoteRep k1)+    , Dict2 Ae.FromJSON f2+    ) => Ae.FromJSON (Some2 f2)+  where+    {-# INLINABLE parseJSON #-}+    parseJSON = \v -> do+      ((rsa2, rsa1), v') <- Ae.parseJSON v+      withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> withSingI sa2 $+         withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> withSingI sa1 $+            case dict2 sa2 sa1 :: Dict (Ae.FromJSON (f2 a2 a1)) of+               Dict -> do+                  x :: f2 a2 a1 <- Ae.parseJSON v'+                  return (some2 x)++instance forall (f3 :: k3 -> k2 -> k1 -> *)+  . ( SingKind k3+    , SingKind k2+    , SingKind k1+    , Ae.FromJSON (DemoteRep k3)+    , Ae.FromJSON (DemoteRep k2)+    , Ae.FromJSON (DemoteRep k1)+    , Dict3 Ae.FromJSON f3+    ) => Ae.FromJSON (Some3 f3)+  where+    {-# INLINABLE parseJSON #-}+    parseJSON = \v -> do+      ((rsa3, rsa2, rsa1), v') <- Ae.parseJSON v+      withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> withSingI sa3 $+         withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> withSingI sa2 $+            withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> withSingI sa1 $+               case dict3 sa3 sa2 sa1 :: Dict (Ae.FromJSON (f3 a3 a2 a1)) of+                  Dict -> do+                     x :: f3 a3 a2 a1 <- Ae.parseJSON v'+                     return (some3 x)++instance forall (f4 :: k4 -> k3 -> k2 -> k1 -> *)+  . ( SingKind k4+    , SingKind k3+    , SingKind k2+    , SingKind k1+    , Ae.FromJSON (DemoteRep k4)+    , Ae.FromJSON (DemoteRep k3)+    , Ae.FromJSON (DemoteRep k2)+    , Ae.FromJSON (DemoteRep k1)+    , Dict4 Ae.FromJSON f4+    ) => Ae.FromJSON (Some4 f4)+  where+    {-# INLINABLE parseJSON #-}+    parseJSON = \v -> do+      ((rsa4, rsa3, rsa2, rsa1), v') <- Ae.parseJSON v+      withSomeSing rsa4 $ \(sa4 :: Sing (a4 :: k4)) -> withSingI sa4 $+         withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> withSingI sa3 $+            withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> withSingI sa2 $+               withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> withSingI sa1 $+                  case dict4 sa4 sa3 sa2 sa1 :: Dict (Ae.FromJSON (f4 a4 a3 a2 a1)) of+                     Dict -> do+                        x :: f4 a4 a3 a2 a1 <- Ae.parseJSON v'+                        return (some4 x)

@@ -6,13 +6,14 @@ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE UndecidableInstances #-}  {-# OPTIONS_GHC -fno-warn-orphans #-}  -- | This module exports 'Show', 'Eq' and 'Ord' instances for 'Exinst.Some1',--- 'Exinst.Some2', 'Exinst.Some3' and 'Exinst.Some4' from "Exinst.Singletons", provided situable+-- 'Exinst.Some2', 'Exinst.Some3' and 'Exinst.Some4' from "Exinst", provided situable -- 'Dict1', 'Dict2', 'Dict3' and 'Dict4' instances are available. -- -- See the README file for more general documentation: https://hackage.haskell.org/package/exinst#readme@@ -21,14 +22,19 @@ import Data.Constraint import Data.Kind (Type) import Data.Singletons+import Data.Singletons.Prelude.Enum (PEnum(EnumFromTo), PBounded(MinBound, MaxBound)) import Data.Singletons.Prelude.Bool (Sing(STrue,SFalse))+import qualified Data.Singletons.Prelude.List as List+import Data.Singletons.Prelude.Tuple (Tuple2Sym1) import Data.Singletons.Decide import Data.Type.Equality-import Exinst.Singletons-  hiding (Some1(..), Some2(..), Some3(..), Some4(..))-import qualified Exinst.Singletons as Exinst+import qualified GHC.Generics as G import Prelude +import Exinst.Internal+  hiding (Some1(..), Some2(..), Some3(..), Some4(..))+import qualified Exinst.Internal as Exinst+ --------------------------------------------------------------------------------  -- Internal wrappers used to avoid writing the string manipulation in 'Show'@@ -276,10 +282,254 @@                      Dict -> Just (compare x y)  --------------------------------------------------------------------------------+-- Generic++type Eithers1 (f :: k1 -> Type) =+  Eithers1' (EnumFromTo (MinBound :: k1) (MaxBound :: k1)) f++-- | TODO: Mak1e this logarithmic.+type family Eithers1' (xs :: [k1]) (f :: k1 -> Type) :: Type where+  Eithers1' (x ': '[]) f = f x+  Eithers1' (x ': xs)  f = Either (f x) (Eithers1' xs f)++instance forall k1 (f :: k1 -> Type)+  . ( SingKind k1+    , PEnum ('Proxy :: Proxy k1)+    , PBounded ('Proxy :: Proxy k1)+    , G.Generic (DemoteRep k1)+    , Dict1 G.Generic f+    , Dict1 (Inj (Eithers1 f)) f+    ) => G.Generic (Exinst.Some1 f)+  where+    type Rep (Exinst.Some1 (f :: k1 -> Type)) =+      G.Rep (DemoteRep k1, Eithers1 f)+    {-# INLINABLE from #-}+    from = \s1x -> withSome1Sing s1x $ \sa1 (x :: f a1) ->+      case dict1 sa1 :: Dict (G.Generic (f a1)) of+        Dict -> case dict1 sa1 :: Dict (Inj (Eithers1 f) (f a1)) of+          Dict -> G.from (fromSing sa1, inj x)+    {-# INLINABLE to #-}+    to = \(G.M1 (G.M1 (G.M1 (G.K1 da1) G.:*: G.M1 (G.K1 ex)))) ->+      withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) ->+        case dict1 sa1 :: Dict (Inj (Eithers1 f) (f a1)) of+          Dict -> case prj ex of+            Just x -> Exinst.Some1 sa1 (x :: f a1)+            Nothing -> error "Generic Some1: Malformed Rep"++---+type Eithers2 (f :: k2 -> k1 -> Type) =+  Eithers2' (Cartesian2 (EnumFromTo (MinBound :: k2) (MaxBound :: k2))+                        (EnumFromTo (MinBound :: k1) (MaxBound :: k1))) f++-- | TODO: Mak1e this logarithmic.+type family Eithers2' (xs :: [(k2, k1)]) (f :: k2 -> k1 -> Type) :: Type where+  Eithers2' ( '(x2, x1) ': '[]) f = f x2 x1+  Eithers2' ( '(x2, x1) ': xs)  f = Either (f x2 x1) (Eithers2' xs f)++type family Cartesian2 (xs2 :: [k2]) (xs1 :: [k1]) :: [(k2,k1)] where+  Cartesian2 '[] xs1 = '[]+  Cartesian2 (x2 ': xs2) xs1 =+    List.Concat [List.Map (Tuple2Sym1 x2) xs1, Cartesian2 xs2 xs1]+++instance forall k2 k1 (f :: k2 -> k1 -> Type)+  . ( SingKind k2+    , SingKind k1+    , PEnum ('Proxy :: Proxy k2)+    , PEnum ('Proxy :: Proxy k1)+    , PBounded ('Proxy :: Proxy k2)+    , PBounded ('Proxy :: Proxy k1)+    , G.Generic (DemoteRep k2)+    , G.Generic (DemoteRep k1)+    , Dict2 G.Generic f+    , Dict2 (Inj (Eithers2 f)) f+    ) => G.Generic (Exinst.Some2 f)+  where+    type Rep (Exinst.Some2 (f :: k2 -> k1 -> Type)) =+      G.Rep ((DemoteRep k2, DemoteRep k1), Eithers2 f)+    {-# INLINABLE from #-}+    from = \s2x -> withSome2Sing s2x $ \sa2 sa1 (x :: f a2 a1) ->+      case dict2 sa2 sa1 :: Dict (G.Generic (f a2 a1)) of+        Dict -> case dict2 sa2 sa1 :: Dict (Inj (Eithers2 f) (f a2 a1)) of+          Dict -> G.from ((fromSing sa2, fromSing sa1), inj x)+    {-# INLINABLE to #-}+    to = \(G.M1 (G.M1 (G.M1 (G.K1 (da2, da1)) G.:*: G.M1 (G.K1 ex)))) ->+      withSomeSing da2 $ \(sa2 :: Sing (a2 :: k2)) ->+        withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) ->+          case dict2 sa2 sa1 :: Dict (Inj (Eithers2 f) (f a2 a1)) of+            Dict -> case prj ex of+              Just x -> Exinst.Some2 sa2 sa1 (x :: f a2 a1)+              Nothing -> error "Generic Some2: Malformed Rep"+++---+type Eithers3 (f :: k3 -> k2 -> k1 -> Type) =+  Eithers3' (Cartesian3 (EnumFromTo (MinBound :: k3) (MaxBound :: k3))+                        (EnumFromTo (MinBound :: k2) (MaxBound :: k2))+                        (EnumFromTo (MinBound :: k1) (MaxBound :: k1))) f++-- | TODO: Mak1e this logarithmic.+type family Eithers3' (xs :: [(k3, (k2, k1))]) (f :: k3 -> k2 -> k1 -> Type) :: Type where+  Eithers3' ( '(x3, '(x2, x1)) ': '[]) f = f x3 x2 x1+  Eithers3' ( '(x3, '(x2, x1)) ': xs)  f = Either (f x3 x2 x1) (Eithers3' xs f)++-- | We use nested 2-tuples instead of 3-tuples because it's easier to implement.+type family Cartesian3 (xs3 :: [k3]) (xs2 :: [k2]) (xs1 :: [k1]) :: [(k3,(k2,k1))] where+  Cartesian3 '[] xs2 xs1 = '[]+  Cartesian3 (x3 ': xs3) xs2 xs1 =+    List.Concat [ List.Map (Tuple2Sym1 x3) (Cartesian2 xs2 xs1)+                , Cartesian3 xs3 xs2 xs1 ]+++instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type)+  . ( SingKind k3+    , SingKind k2+    , SingKind k1+    , PEnum ('Proxy :: Proxy k3)+    , PEnum ('Proxy :: Proxy k2)+    , PEnum ('Proxy :: Proxy k1)+    , PBounded ('Proxy :: Proxy k3)+    , PBounded ('Proxy :: Proxy k2)+    , PBounded ('Proxy :: Proxy k1)+    , G.Generic (DemoteRep k3)+    , G.Generic (DemoteRep k2)+    , G.Generic (DemoteRep k1)+    , Dict3 G.Generic f+    , Dict3 (Inj (Eithers3 f)) f+    ) => G.Generic (Exinst.Some3 f)+  where+    type Rep (Exinst.Some3 (f :: k3 -> k2 -> k1 -> Type)) =+      G.Rep ((DemoteRep k3, DemoteRep k2, DemoteRep k1), Eithers3 f)+    {-# INLINABLE from #-}+    from = \s3x -> withSome3Sing s3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) ->+      case dict3 sa3 sa2 sa1 :: Dict (G.Generic (f a3 a2 a1)) of+        Dict -> case dict3 sa3 sa2 sa1 :: Dict (Inj (Eithers3 f) (f a3 a2 a1)) of+          Dict -> G.from ((fromSing sa3, fromSing sa2, fromSing sa1), inj x)+    {-# INLINABLE to #-}+    to = \(G.M1 (G.M1 (G.M1 (G.K1 (da3, da2, da1)) G.:*: G.M1 (G.K1 ex)))) ->+      withSomeSing da3 $ \(sa3 :: Sing (a3 :: k3)) ->+        withSomeSing da2 $ \(sa2 :: Sing (a2 :: k2)) ->+          withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) ->+            case dict3 sa3 sa2 sa1 :: Dict (Inj (Eithers3 f) (f a3 a2 a1)) of+              Dict -> case prj ex of+                Just x -> Exinst.Some3 sa3 sa2 sa1 (x :: f a3 a2 a1)+                Nothing -> error "Generic Some3: Malformed Rep"+++---+type Eithers4 (f :: k4 -> k3 -> k2 -> k1 -> Type) =+  Eithers4' (Cartesian4 (EnumFromTo (MinBound :: k4) (MaxBound :: k4))+                        (EnumFromTo (MinBound :: k3) (MaxBound :: k3))+                        (EnumFromTo (MinBound :: k2) (MaxBound :: k2))+                        (EnumFromTo (MinBound :: k1) (MaxBound :: k1))) f++-- | TODO: Mak1e this logarithmic.+type family Eithers4' (xs :: [(k4, (k3, (k2, k1)))]) (f :: k4 -> k3 -> k2 -> k1 -> Type) :: Type where+  Eithers4' ( '( x4, '(x3, '(x2, x1))) ': '[]) f = f x4 x3 x2 x1+  Eithers4' ( '( x4, '(x3, '(x2, x1))) ': xs)  f = Either (f x4 x3 x2 x1) (Eithers4' xs f)++-- | We use nested 2-tuples instead of 4-tuples because it's easier to implement.+type family Cartesian4 (xs4 :: [k4]) (xs3 :: [k3]) (xs2 :: [k2]) (xs1 :: [k1]) :: [(k4,(k3,(k2,k1)))] where+  Cartesian4 '[] xs3 xs2 xs1 = '[]+  Cartesian4 (x4 ': xs4) xs3 xs2 xs1 =+    List.Concat [ List.Map (Tuple2Sym1 x4) (Cartesian3 xs3 xs2 xs1)+                , Cartesian4 xs4 xs3 xs2 xs1 ]+++instance forall k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type)+  . ( SingKind k4+    , SingKind k3+    , SingKind k2+    , SingKind k1+    , PEnum ('Proxy :: Proxy k4)+    , PEnum ('Proxy :: Proxy k3)+    , PEnum ('Proxy :: Proxy k2)+    , PEnum ('Proxy :: Proxy k1)+    , PBounded ('Proxy :: Proxy k4)+    , PBounded ('Proxy :: Proxy k3)+    , PBounded ('Proxy :: Proxy k2)+    , PBounded ('Proxy :: Proxy k1)+    , G.Generic (DemoteRep k4)+    , G.Generic (DemoteRep k3)+    , G.Generic (DemoteRep k2)+    , G.Generic (DemoteRep k1)+    , Dict4 G.Generic f+    , Dict4 (Inj (Eithers4 f)) f+    ) => G.Generic (Exinst.Some4 f)+  where+    type Rep (Exinst.Some4 (f :: k4 -> k3 -> k2 -> k1 -> Type)) =+      G.Rep ((DemoteRep k4, DemoteRep k3, DemoteRep k2, DemoteRep k1), Eithers4 f)+    {-# INLINABLE from #-}+    from = \s4x -> withSome4Sing s4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) ->+      case dict4 sa4 sa3 sa2 sa1 :: Dict (G.Generic (f a4 a3 a2 a1)) of+        Dict -> case dict4 sa4 sa3 sa2 sa1 :: Dict (Inj (Eithers4 f) (f a4 a3 a2 a1)) of+          Dict -> G.from ((fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1), inj x)+    {-# INLINABLE to #-}+    to = \(G.M1 (G.M1 (G.M1 (G.K1 (da4, da3, da2, da1)) G.:*: G.M1 (G.K1 ex)))) ->+      withSomeSing da4 $ \(sa4 :: Sing (a4 :: k4)) ->+        withSomeSing da3 $ \(sa3 :: Sing (a3 :: k3)) ->+          withSomeSing da2 $ \(sa2 :: Sing (a2 :: k2)) ->+            withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) ->+              case dict4 sa4 sa3 sa2 sa1 :: Dict (Inj (Eithers4 f) (f a4 a3 a2 a1)) of+                Dict -> case prj ex of+                  Just x -> Exinst.Some4 sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1)+                  Nothing -> error "Generic Some4: Malformed Rep"+ ----------------------------------------------------------------------------------- Out of the box 'Dict1' instances for some @base@ types+--------------------------------------------------------------------------------+-- Out of the box 'DictX' instances for some @base@ types -instance (c (f 'True), c (f 'False)) => Dict1 c (f :: Bool -> k0) where-  dict1 = \case-    STrue -> Dict-    SFalse -> Dict+instance+  (c 'False, c 'True+  ) => Dict0 (c :: Bool -> Constraint) where+  {-# INLINABLE dict0 #-}+  dict0 = \case { SFalse -> Dict; STrue -> Dict }++instance+  ( c (f 'False), c (f 'True)+  ) => Dict1 c (f :: Bool -> k0) where+  {-# INLINABLE dict1 #-}+  dict1 = \case { SFalse -> Dict; STrue -> Dict }++instance+  ( Dict1 c (f 'False), Dict1 c (f 'True)+  ) => Dict2 c (f :: Bool -> k1 -> k0) where+  {-# INLINABLE dict2 #-}+  dict2 = \x -> case x of { SFalse -> dict1; STrue -> dict1 }++instance+  ( Dict2 c (f 'False), Dict2 c (f 'True)+  ) => Dict3 c (f :: Bool -> k2 -> k1 -> k0) where+  {-# INLINABLE dict3 #-}+  dict3 = \x -> case x of { SFalse -> dict2; STrue -> dict2 }++instance+  ( Dict3 c (f 'False), Dict3 c (f 'True)+  ) => Dict4 c (f :: Bool -> k3 -> k2 -> k1 -> k0) where+  {-# INLINABLE dict4 #-}+  dict4 = \x -> case x of { SFalse -> dict3; STrue -> dict3 }++--------------------------------------------------------------------------------+--------------------------------------------------------------------------------+-- Misc++class Inj b a where+  inj :: a -> b+  prj :: b -> Maybe a+instance Inj a a where+  {-# INLINE inj #-}+  inj = id+  {-# INLINE prj #-}+  prj = Just+instance Inj (Either a b) a where+  {-# INLINE inj #-}+  inj = Left+  {-# INLINE prj #-}+  prj = either Just (const Nothing)+-- | TODO: Make this logarithmic.+instance {-# OVERLAPPABLE #-} Inj x a => Inj (Either b x) a where+  {-# INLINE inj #-}+  inj = Right . inj+  {-# INLINE prj #-}+  prj = either (const Nothing) prj+

@@ -0,0 +1,118 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE UndecidableInstances #-}++{-# OPTIONS_GHC -fno-warn-orphans #-}++-- | This module exports 'By.Serial' instances for 'Some1', 'Some2', 'Some3'+-- and 'Some4' from "Exinst", provided situable 'Dict1', 'Dict2',+-- 'Dict3' and 'Dict4' instances are available.+--+-- See the README file in the @exinst@ package for more general documentation:+-- https://hackage.haskell.org/package/exinst#readme+module Exinst.Instances.Bytes () where++import qualified Data.Bytes.Serial as By+import Data.Constraint+import Data.Singletons+import Prelude++import Exinst.Internal++--------------------------------------------------------------------------------++instance forall (f1 :: k1 -> *)+  . ( SingKind k1+    , By.Serial (DemoteRep k1)+    , Dict1 By.Serial f1+    ) => By.Serial (Some1 f1)+  where+    {-# INLINABLE serialize #-}+    serialize = \some1x -> withSome1Sing some1x $ \sa1 (x :: f1 a1) ->+       case dict1 sa1 :: Dict (By.Serial (f1 a1)) of+          Dict -> do By.serialize (fromSing sa1)+                     By.serialize x+    {-# INLINABLE deserialize #-}+    deserialize = do+      rsa1 <- By.deserialize+      withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> withSingI sa1 $+         case dict1 sa1 :: Dict (By.Serial (f1 a1)) of+            Dict -> do x :: f1 a1 <- By.deserialize+                       return (some1 x)++instance forall (f2 :: k2 -> k1 -> *)+  . ( SingKind k2+    , SingKind k1+    , By.Serial (DemoteRep k2)+    , By.Serial (DemoteRep k1)+    , Dict2 By.Serial f2+    ) => By.Serial (Some2 f2)+  where+    {-# INLINABLE serialize #-}+    serialize = \some2x -> withSome2Sing some2x $ \sa2 sa1 (x :: f2 a2 a1) ->+       case dict2 sa2 sa1 :: Dict (By.Serial (f2 a2 a1)) of+          Dict -> do By.serialize (fromSing sa2, fromSing sa1)+                     By.serialize x+    {-# INLINABLE deserialize #-}+    deserialize = do+      (rsa2, rsa1) <- By.deserialize+      withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> withSingI sa2 $+         withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> withSingI sa1 $+            case dict2 sa2 sa1 :: Dict (By.Serial (f2 a2 a1)) of+               Dict -> do x :: f2 a2 a1 <- By.deserialize+                          return (some2 x)++instance forall (f3 :: k3 -> k2 -> k1 -> *)+  . ( SingKind k3+    , SingKind k2+    , SingKind k1+    , By.Serial (DemoteRep k3)+    , By.Serial (DemoteRep k2)+    , By.Serial (DemoteRep k1)+    , Dict3 By.Serial f3+    ) => By.Serial (Some3 f3)+  where+    {-# INLINABLE serialize #-}+    serialize = \some3x -> withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f3 a3 a2 a1) ->+       case dict3 sa3 sa2 sa1 :: Dict (By.Serial (f3 a3 a2 a1)) of+          Dict -> do By.serialize (fromSing sa3, fromSing sa2, fromSing sa1)+                     By.serialize x+    {-# INLINABLE deserialize #-}+    deserialize = do+      (rsa3, rsa2, rsa1) <- By.deserialize+      withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> withSingI sa3 $+         withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> withSingI sa2 $+            withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> withSingI sa1 $+               case dict3 sa3 sa2 sa1 :: Dict (By.Serial (f3 a3 a2 a1)) of+                  Dict -> do x :: f3 a3 a2 a1 <- By.deserialize+                             return (some3 x)++instance forall (f4 :: k4 -> k3 -> k2 -> k1 -> *)+  . ( SingKind k4+    , SingKind k3+    , SingKind k2+    , SingKind k1+    , By.Serial (DemoteRep k4)+    , By.Serial (DemoteRep k3)+    , By.Serial (DemoteRep k2)+    , By.Serial (DemoteRep k1)+    , Dict4 By.Serial f4+    ) => By.Serial (Some4 f4)+  where+    {-# INLINABLE serialize #-}+    serialize = \some4x -> withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f4 a4 a3 a2 a1) ->+       case dict4 sa4 sa3 sa2 sa1 :: Dict (By.Serial (f4 a4 a3 a2 a1)) of+          Dict -> do By.serialize (fromSing sa4, fromSing sa3,+                                   fromSing sa2, fromSing sa1)+                     By.serialize x+    {-# INLINABLE deserialize #-}+    deserialize = do+      (rsa4, rsa3, rsa2, rsa1) <- By.deserialize+      withSomeSing rsa4 $ \(sa4 :: Sing (a4 :: k4)) -> withSingI sa4 $+         withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> withSingI sa3 $+            withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> withSingI sa2 $+               withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> withSingI sa1 $+                  case dict4 sa4 sa3 sa2 sa1 :: Dict (By.Serial (f4 a4 a3 a2 a1)) of+                     Dict -> do x :: f4 a4 a3 a2 a1 <- By.deserialize+                                return (some4 x)

@@ -0,0 +1,60 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE UndecidableInstances #-}++{-# OPTIONS_GHC -fno-warn-orphans #-}++-- | This module exports 'NFData' instances for 'Some1', 'Some2', 'Some3' and+-- 'Some4' from "Exinst", provided situable 'Dict1', 'Dict2', 'Dict3'+-- and 'Dict4' instances are available.+--+-- See the README file in the @exinst@ package for more general documentation:+-- https://hackage.haskell.org/package/exinst#readme+module Exinst.Instances.DeepSeq () where++import Control.DeepSeq (NFData(rnf))+import Data.Constraint+import Prelude++import Exinst.Internal++--------------------------------------------------------------------------------++instance forall (f1 :: k1 -> *).+  ( Dict1 NFData f1+  ) => NFData (Some1 f1) where+  {-# INLINABLE rnf #-}+  rnf = \(!some1x) ->+    withSome1Sing some1x $ \ !sa1 !(x :: f1 a1) ->+       case dict1 sa1 :: Dict (NFData (f1 a1)) of+          Dict -> rnf x `seq` ()++instance forall (f2 :: k2 -> k1 -> *).+  ( Dict2 NFData f2+  ) => NFData (Some2 f2) where+  {-# INLINABLE rnf #-}+  rnf = \(!some2x) ->+    withSome2Sing some2x $ \ !sa2 !sa1 !(x :: f2 a2 a1) ->+       case dict2 sa2 sa1 :: Dict (NFData (f2 a2 a1)) of+          Dict -> rnf x `seq` ()++instance forall (f3 :: k3 -> k2 -> k1 -> *).+  ( Dict3 NFData f3+  ) => NFData (Some3 f3) where+  {-# INLINABLE rnf #-}+  rnf = \(!some3x) ->+    withSome3Sing some3x $ \ !sa3 !sa2 !sa1 !(x :: f3 a3 a2 a1) ->+       case dict3 sa3 sa2 sa1 :: Dict (NFData (f3 a3 a2 a1)) of+          Dict -> rnf x `seq` ()++instance forall (f4 :: k4 -> k3 -> k2 -> k1 -> *).+  ( Dict4 NFData f4+  ) => NFData (Some4 f4) where+  {-# INLINABLE rnf #-}+  rnf = \(!some4x) ->+    withSome4Sing some4x $ \ !(sa4) !sa3 !sa2 !sa1 !(x :: f4 a4 a3 a2 a1) ->+       case dict4 sa4 sa3 sa2 sa1 :: Dict (NFData (f4 a4 a3 a2 a1)) of+          Dict -> rnf x `seq` ()+

@@ -0,0 +1,99 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE UndecidableInstances #-}++{-# OPTIONS_GHC -fno-warn-orphans #-}++-- | This module exports 'Hashable' instances for 'Some1', 'Some2', 'Some3' and+-- 'Some4' from "Exinst", provided situable 'Dict1', 'Dict2', 'Dict3'+-- and 'Dict4' instances are available.+--+-- See the README file in the @exinst@ package for more general documentation:+-- https://hackage.haskell.org/package/exinst#readme+module Exinst.Instances.Hashable () where++import Data.Hashable (Hashable(hashWithSalt))+import Data.Constraint+import Data.Singletons+import Prelude++import Exinst.Internal++--------------------------------------------------------------------------------++-- | Some salt we add to hashes calculated in this module.+salt0 :: Int+salt0 = 6700417++--------------------------------------------------------------------------------++instance forall (f1 :: k1 -> *)+  . ( SingKind k1+    , Hashable (DemoteRep k1)+    , Dict1 Hashable f1+    ) => Hashable (Some1 f1)+  where+    {-# INLINABLE hashWithSalt #-}+    hashWithSalt salt some1x = withSome1Sing some1x $ \sa1 (x :: f1 a1) ->+       case dict1 sa1 :: Dict (Hashable (f1 a1)) of+          Dict -> salt `hashWithSalt` salt0+                       `hashWithSalt` fromSing sa1+                       `hashWithSalt` x++instance forall (f2 :: k2 -> k1 -> *)+  . ( SingKind k2+    , SingKind k1+    , Hashable (DemoteRep k2)+    , Hashable (DemoteRep k1)+    , Dict2 Hashable f2+    ) => Hashable (Some2 f2)+  where+    {-# INLINABLE hashWithSalt #-}+    hashWithSalt salt some2x = withSome2Sing some2x $ \sa2 sa1 (x :: f2 a2 a1) ->+       case dict2 sa2 sa1 :: Dict (Hashable (f2 a2 a1)) of+          Dict -> salt `hashWithSalt` salt0+                       `hashWithSalt` fromSing sa2+                       `hashWithSalt` fromSing sa1+                       `hashWithSalt` x++instance forall (f3 :: k3 -> k2 -> k1 -> *)+  . ( SingKind k3+    , SingKind k2+    , SingKind k1+    , Hashable (DemoteRep k3)+    , Hashable (DemoteRep k2)+    , Hashable (DemoteRep k1)+    , Dict3 Hashable f3+    ) => Hashable (Some3 f3)+  where+    {-# INLINABLE hashWithSalt #-}+    hashWithSalt salt some3x = withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f3 a3 a2 a1) ->+       case dict3 sa3 sa2 sa1 :: Dict (Hashable (f3 a3 a2 a1)) of+          Dict -> salt `hashWithSalt` salt0+                       `hashWithSalt` fromSing sa3+                       `hashWithSalt` fromSing sa2+                       `hashWithSalt` fromSing sa1+                       `hashWithSalt` x++instance forall (f4 :: k4 -> k3 -> k2 -> k1 -> *)+  . ( SingKind k4+    , SingKind k3+    , SingKind k2+    , SingKind k1+    , Hashable (DemoteRep k4)+    , Hashable (DemoteRep k3)+    , Hashable (DemoteRep k2)+    , Hashable (DemoteRep k1)+    , Dict4 Hashable f4+    ) => Hashable (Some4 f4)+  where+    {-# INLINABLE hashWithSalt #-}+    hashWithSalt salt some4x = withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f4 a4 a3 a2 a1) ->+       case dict4 sa4 sa3 sa2 sa1 :: Dict (Hashable (f4 a4 a3 a2 a1)) of+          Dict -> salt `hashWithSalt` salt0+                       `hashWithSalt` fromSing sa4+                       `hashWithSalt` fromSing sa3+                       `hashWithSalt` fromSing sa2+                       `hashWithSalt` fromSing sa1+                       `hashWithSalt` x

@@ -0,0 +1,106 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeInType #-}++{-# OPTIONS_GHC -fno-warn-orphans #-}++-- | This module exports 'QC.arbitrary' instances for 'Exinst.Some1', 'Some2',+-- 'Some3' and 'Some4' from "Exinst", provided situable 'Dict1',+-- 'Dict2', 'Dict3' and 'Dict4' instances are available.+--+-- See the README file for more general documentation: https://hackage.haskell.org/package/exinst#readme+module Exinst.Instances.QuickCheck () where++import Data.Constraint+import Data.Kind (Type)+import Data.Singletons (SingKind, Sing, DemoteRep, withSomeSing)+import qualified Test.QuickCheck as QC++import Exinst.Internal++--------------------------------------------------------------------------------++instance+  forall k1 (f :: k1 -> Type).+  ( SingKind k1+  , QC.Arbitrary (DemoteRep k1)+  , Dict1 QC.Arbitrary f+  ) => QC.Arbitrary (Some1 f) where+  arbitrary = do+    da1 <- QC.arbitrary+    withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) ->+      case dict1 sa1 :: Dict (QC.Arbitrary (f a1)) of+        Dict -> Some1 sa1 <$> QC.arbitrary+  shrink = \s1x -> withSome1Sing s1x $ \sa1 (x :: f a1) ->+    case dict1 sa1 :: Dict (QC.Arbitrary (f a1)) of+      Dict -> Some1 sa1 <$> QC.shrink x++instance+  forall k2 k1 (f :: k2 -> k1 -> Type).+  ( SingKind k2+  , SingKind k1+  , QC.Arbitrary (DemoteRep k2)+  , QC.Arbitrary (DemoteRep k1)+  , Dict2 QC.Arbitrary f+  ) => QC.Arbitrary (Some2 f) where+  arbitrary = do+    da2 <- QC.arbitrary+    da1 <- QC.arbitrary+    withSomeSing da2 $ \(sa2 :: Sing (a2 :: k2)) ->+      withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) ->+        case dict2 sa2 sa1 :: Dict (QC.Arbitrary (f a2 a1)) of+          Dict -> Some2 sa2 sa1 <$> QC.arbitrary+  shrink = \s2x -> withSome2Sing s2x $ \sa2 sa1 (x :: f a2 a1) ->+    case dict2 sa2 sa1 :: Dict (QC.Arbitrary (f a2 a1)) of+      Dict -> Some2 sa2 sa1 <$> QC.shrink x++instance+  forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type).+  ( SingKind k3+  , SingKind k2+  , SingKind k1+  , QC.Arbitrary (DemoteRep k3)+  , QC.Arbitrary (DemoteRep k2)+  , QC.Arbitrary (DemoteRep k1)+  , Dict3 QC.Arbitrary f+  ) => QC.Arbitrary (Some3 f) where+  arbitrary = do+    da3 <- QC.arbitrary+    da2 <- QC.arbitrary+    da1 <- QC.arbitrary+    withSomeSing da3 $ \(sa3 :: Sing (a3 :: k3)) ->+      withSomeSing da2 $ \(sa2 :: Sing (a2 :: k2)) ->+        withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) ->+          case dict3 sa3 sa2 sa1 :: Dict (QC.Arbitrary (f a3 a2 a1)) of+            Dict -> Some3 sa3 sa2 sa1 <$> QC.arbitrary+  shrink = \s3x -> withSome3Sing s3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) ->+    case dict3 sa3 sa2 sa1 :: Dict (QC.Arbitrary (f a3 a2 a1)) of+      Dict -> Some3 sa3 sa2 sa1 <$> QC.shrink x++instance+  forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type).+  ( SingKind k4+  , SingKind k3+  , SingKind k2+  , SingKind k1+  , QC.Arbitrary (DemoteRep k4)+  , QC.Arbitrary (DemoteRep k3)+  , QC.Arbitrary (DemoteRep k2)+  , QC.Arbitrary (DemoteRep k1)+  , Dict4 QC.Arbitrary f+  ) => QC.Arbitrary (Some4 f) where+  arbitrary = do+    da4 <- QC.arbitrary+    da3 <- QC.arbitrary+    da2 <- QC.arbitrary+    da1 <- QC.arbitrary+    withSomeSing da4 $ \(sa4 :: Sing (a4 :: k4)) ->+      withSomeSing da3 $ \(sa3 :: Sing (a3 :: k3)) ->+        withSomeSing da2 $ \(sa2 :: Sing (a2 :: k2)) ->+          withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) ->+            case dict4 sa4 sa3 sa2 sa1 :: Dict (QC.Arbitrary (f a4 a3 a2 a1)) of+              Dict -> Some4 sa4 sa3 sa2 sa1 <$> QC.arbitrary+  shrink = \s3x -> withSome4Sing s3x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) ->+    case dict4 sa4 sa3 sa2 sa1 :: Dict (QC.Arbitrary (f a4 a3 a2 a1)) of+      Dict -> Some4 sa4 sa3 sa2 sa1 <$> QC.shrink x+

@@ -0,0 +1,361 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+++module Exinst.Internal+ ( -- * 1 type index+   Some1(Some1)+ , some1+ , fromSome1+ , _Some1+ , withSome1+ , withSome1Sing+ , some1SingRep+ , Dict1(dict1)++   -- * 2 type indexes+ , Some2(Some2)+ , some2+ , fromSome2+ , _Some2+ , withSome2+ , withSome2Sing+ , some2SingRep+ , Dict2(dict2)++   -- * 3 type indexes+ , Some3(Some3)+ , some3+ , fromSome3+ , _Some3+ , withSome3+ , withSome3Sing+ , some3SingRep+ , Dict3(dict3)++   -- * 4 type indexes+ , Some4(Some4)+ , some4+ , fromSome4+ , _Some4+ , withSome4+ , withSome4Sing+ , some4SingRep+ , Dict4(dict4)++   -- * Miscellaneous+ , Dict0(dict0)+ ) where++import Data.Constraint+import Data.Kind (Type)+import Data.Profunctor (dimap, Choice(right'))+import Data.Singletons+import Data.Singletons.Decide+import Data.Type.Equality+import Prelude++--------------------------------------------------------------------------------++data Some1 (f1 :: k1 -> Type) = forall a1.+  Some1 !(Sing a1) !(f1 a1)++data Some2 (f2 :: k2 -> k1 -> Type) = forall a2 a1.+  Some2 !(Sing a2) !(Sing a1) !(f2 a2 a1)++data Some3 (f3 :: k3 -> k2 -> k1 -> Type) = forall a3 a2 a1.+  Some3 !(Sing a3) !(Sing a2) !(Sing a1) !(f3 a3 a2 a1)++data Some4 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) = forall a4 a3 a2 a1.+  Some4 !(Sing a4) !(Sing a3) !(Sing a2) !(Sing a1) !(f4 a4 a3 a2 a1)++--------------------------------------------------------------------------------++some1+  :: forall (f1 :: k1 -> Type) a1+  .  SingI a1+  => f1 a1+  -> Some1 f1 -- ^+some1 = Some1 (sing :: Sing a1)+{-# INLINE some1 #-}++some2+  :: forall (f2 :: k2 -> k1 -> Type) a2 a1+  .  (SingI a2, SingI a1)+  => f2 a2 a1+  -> Some2 f2 -- ^+some2 = Some2 (sing :: Sing a2) (sing :: Sing a1)+{-# INLINE some2 #-}++some3+  :: forall (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1+  .  (SingI a3, SingI a2, SingI a1)+  => f3 a3 a2 a1+  -> Some3 f3 -- ^+some3 = Some3 (sing :: Sing a3) (sing :: Sing a2) (sing :: Sing a1)+{-# INLINE some3 #-}++some4+  :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1+  .  (SingI a4, SingI a3, SingI a2, SingI a1)+  => f4 a4 a3 a2 a1+  -> Some4 f4 -- ^+some4 = Some4 (sing :: Sing a4) (sing :: Sing a3)+              (sing :: Sing a2) (sing :: Sing a1)+{-# INLINE some4 #-}++--------------------------------------------------------------------------------++withSome1+  :: forall (f1 :: k1 -> Type) (r :: Type)+   . Some1 f1+  -> (forall a1. SingI a1 => f1 a1 -> r)+  -> r -- ^+withSome1 s1 g = withSome1Sing s1 (\_ -> g)+{-# INLINABLE withSome1 #-}++withSome2+  :: forall (f2 :: k2 -> k1 -> Type) (r :: Type)+  .  Some2 f2+  -> (forall a2 a1. (SingI a2, SingI a1) => f2 a2 a1 -> r)+  -> r -- ^+withSome2 s2 g = withSome2Sing s2 (\_ _ -> g)+{-# INLINABLE withSome2 #-}++withSome3+  :: forall (f3 :: k3 -> k2 -> k1 -> Type) (r :: Type)+  .  Some3 f3+  -> (forall a3 a2 a1. (SingI a3, SingI a2, SingI a1) => f3 a3 a2 a1 -> r)+  -> r -- ^+withSome3 s3 g = withSome3Sing s3 (\_ _ _ -> g)+{-# INLINABLE withSome3 #-}++withSome4+  :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) (r :: Type)+  .  Some4 f4+  -> (forall a4 a3 a2 a1+        .  (SingI a4, SingI a3, SingI a2, SingI a1)+        => f4 a4 a3 a2 a1 -> r)+  -> r -- ^+withSome4 s4 g = withSome4Sing s4 (\_ _ _ _ -> g)+{-# INLINABLE withSome4 #-}++--------------------------------------------------------------------------------++-- | Like 'withSome1', but takes an explicit 'Sing' besides the 'SingI' instance.+withSome1Sing+  :: forall (f1 :: k1 -> Type) (r :: Type)+   . Some1 f1+  -> (forall a1. (SingI a1) => Sing a1 -> f1 a1 -> r)+  -> r -- ^+withSome1Sing (Some1 sa1 x) g = withSingI sa1 (g sa1 x)+{-# INLINABLE withSome1Sing #-}++-- | Like 'withSome2', but takes explicit 'Sing's besides the 'SingI' instances.+withSome2Sing+  :: forall (f2 :: k2 -> k1 -> Type) (r :: Type)+  .  Some2 f2+  -> (forall a2 a1. (SingI a2, SingI a1) => Sing a2 -> Sing a1 -> f2 a2 a1 -> r)+  -> r -- ^+withSome2Sing (Some2 sa2 sa1 x) g = withSingI sa2 (withSingI sa1 (g sa2 sa1 x))+{-# INLINABLE withSome2Sing #-}++-- | Like 'withSome3', but takes explicit 'Sing's besides the 'SingI' instances.+withSome3Sing+  :: forall (f3 :: k3 -> k2 -> k1 -> Type) (r :: Type)+  .  Some3 f3+  -> (forall a3 a2 a1+         .  (SingI a3, SingI a2, SingI a1)+         => Sing a3 -> Sing a2 -> Sing a1 -> f3 a3 a2 a1 -> r)+  -> r -- ^+withSome3Sing (Some3 sa3 sa2 sa1 x) g =+  withSingI sa3 (withSingI sa2 (withSingI sa1 (g sa3 sa2 sa1 x)))+{-# INLINABLE withSome3Sing #-}++-- | Like 'withSome4', but takes explicit 'Sing's besides the 'SingI' instances.+withSome4Sing+  :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) (r :: Type)+  .  Some4 f4+  -> (forall a4 a3 a2 a1+        .  (SingI a4, SingI a3, SingI a2, SingI a1)+        => Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> f4 a4 a3 a2 a1 -> r)+  -> r -- ^+withSome4Sing (Some4 sa4 sa3 sa2 sa1 x) g =+  withSingI sa4 (withSingI sa3 (withSingI sa2 (withSingI sa1+     (g sa4 sa3 sa2 sa1 x))))+{-# INLINABLE withSome4Sing #-}++--------------------------------------------------------------------------------++fromSome1+   :: forall (f1 :: k1 -> Type) a1+    . (SingI a1, SDecide k1)+   => Some1 f1+   -> Maybe (f1 a1) -- ^+fromSome1 = \(Some1 sa1' x) -> do+   Refl <- testEquality sa1' (sing :: Sing a1)+   return x+{-# INLINABLE fromSome1 #-}++fromSome2+   :: forall (f2 :: k2 -> k1 -> Type) a2 a1+    . ( SingI a2, SDecide k2+      , SingI a1, SDecide k1 )+   => Some2 f2+   -> Maybe (f2 a2 a1) -- ^+fromSome2 = \(Some2 sa2' sa1' x) -> do+   Refl <- testEquality sa2' (sing :: Sing a2)+   Refl <- testEquality sa1' (sing :: Sing a1)+   return x+{-# INLINABLE fromSome2 #-}++fromSome3+   :: forall (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1+    . ( SingI a3, SDecide k3+      , SingI a2, SDecide k2+      , SingI a1, SDecide k1 )+   => Some3 f3+   -> Maybe (f3 a3 a2 a1) -- ^+fromSome3 = \(Some3 sa3' sa2' sa1' x) -> do+   Refl <- testEquality sa3' (sing :: Sing a3)+   Refl <- testEquality sa2' (sing :: Sing a2)+   Refl <- testEquality sa1' (sing :: Sing a1)+   return x+{-# INLINABLE fromSome3 #-}++fromSome4+   :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1+    . ( SingI a4, SDecide k4+      , SingI a3, SDecide k3+      , SingI a2, SDecide k2+      , SingI a1, SDecide k1 )+   => Some4 f4+   -> Maybe (f4 a4 a3 a2 a1) -- ^+fromSome4 = \(Some4 sa4' sa3' sa2' sa1' x) -> do+   Refl <- testEquality sa4' (sing :: Sing a4)+   Refl <- testEquality sa3' (sing :: Sing a3)+   Refl <- testEquality sa2' (sing :: Sing a2)+   Refl <- testEquality sa1' (sing :: Sing a1)+   return x+{-# INLINABLE fromSome4 #-}++--------------------------------------------------------------------------------++-- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some1'.+_Some1+  :: forall (f1 :: k1 -> Type) a1+  .  (SingI a1, SDecide k1)+  => Prism' (Some1 f1) (f1 a1)+_Some1 = prism' some1 fromSome1+{-# INLINE _Some1 #-}++-- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some2'.+_Some2+  :: forall (f2 :: k2 -> k1 -> Type) a2 a1+  .  ( SingI a2, SDecide k2+     , SingI a1, SDecide k1 )+  => Prism' (Some2 f2) (f2 a2 a1)+_Some2 = prism' some2 fromSome2+{-# INLINE _Some2 #-}++-- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some3'.+_Some3+  :: forall (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1+  .  ( SingI a3, SDecide k3+     , SingI a2, SDecide k2+     , SingI a1, SDecide k1 )+  => Prism' (Some3 f3) (f3 a3 a2 a1)+_Some3 = prism' some3 fromSome3+{-# INLINE _Some3 #-}++-- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some4'.+_Some4+  :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1+  .  ( SingI a4, SDecide k4+     , SingI a3, SDecide k3+     , SingI a2, SDecide k2+     , SingI a1, SDecide k1 )+  => Prism' (Some4 f4) (f4 a4 a3 a2 a1)+_Some4 = prism' some4 fromSome4+{-# INLINE _Some4 #-}++--------------------------------------------------------------------------------++some1SingRep+  :: SingKind k1+  => Some1 (f1 :: k1 -> Type)+  -> DemoteRep k1 -- ^+some1SingRep = \(Some1 sa1 _) -> fromSing sa1+{-# INLINE some1SingRep #-}++some2SingRep+  :: (SingKind k2, SingKind k1)+  => Some2 (f2 :: k2 -> k1 -> Type)+  -> (DemoteRep k2, DemoteRep k1) -- ^+some2SingRep = \(Some2 sa2 sa1 _) -> (fromSing sa2, fromSing sa1)+{-# INLINE some2SingRep #-}++some3SingRep+  :: (SingKind k3, SingKind k2, SingKind k1)+  => Some3 (f3 :: k3 -> k2 -> k1 -> Type)+  -> (DemoteRep k3, DemoteRep k2, DemoteRep k1) -- ^+some3SingRep = \(Some3 sa3 sa2 sa1 _) ->+  (fromSing sa3, fromSing sa2, fromSing sa1)+{-# INLINE some3SingRep #-}++some4SingRep+  :: (SingKind k4, SingKind k3, SingKind k2, SingKind k1)+  => Some4 (f4 :: k4 -> k3 -> k2 -> k1 -> Type)+  -> (DemoteRep k4, DemoteRep k3, DemoteRep k2, DemoteRep k1) -- ^+some4SingRep = \(Some4 sa4 sa3 sa2 sa1 _) ->+  (fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1)+{-# INLINE some4SingRep #-}++--------------------------------------------------------------------------------++-- | 'Dict0' is a bit different from 'Dict1', 'Dict2', etc. in that it looks up+-- an instance for the singleton type itself, and not for some other type+-- indexed by said singleton type.+class Dict0 (c :: k0 -> Constraint) where+  -- | Runtime lookup of the @c a0@ instance.+  dict0 :: Sing a0 -> Dict (c a0)++class Dict1 (c :: k0 -> Constraint) (f1 :: k1 -> k0) where+  -- | Runtime lookup of the @c (f1 a1)@ instance.+  dict1 :: Sing a1 -> Dict (c (f1 a1))++class Dict2 (c :: k0 -> Constraint) (f2 :: k2 -> k1 -> k0) where+  -- Runtime lookup of the @c (f2 a2 a1)@ instance.+  dict2 :: Sing a2 -> Sing a1 -> Dict (c (f2 a2 a1))++class Dict3 (c :: k0 -> Constraint) (f3 :: k3 -> k2 -> k1 -> k0) where+  -- Runtime lookup of the @c (f3 a3 a2 a1)@ instance.+  dict3 :: Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f3 a3 a2 a1))++class Dict4 (c :: k0 -> Constraint) (f4 :: k4 -> k3 -> k2 -> k1 -> k0) where+  -- Runtime lookup of the @c (f4 a4 a3 a2 a1)@ instance.+  dict4 :: Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f4 a4 a3 a2 a1))++--------------------------------------------------------------------------------+-- Miscelaneous @lens@-compatible stuff.++type Prism s t a b+  = forall p f. (Choice p, Applicative f) => p a (f b) -> p s (f t)++type Prism' s a = Prism s s a a++prism :: (b -> t) -> (s -> Either t a) -> Prism s t a b+prism bt seta = dimap seta (either pure (fmap bt)) . right'+{-# INLINE prism #-}++prism' :: (b -> s) -> (s -> Maybe a) -> Prism s s a b+prism' bs sma = prism bs (\s -> maybe (Left s) Right (sma s))+{-# INLINE prism' #-}+

@@ -1,353 +0,0 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeInType #-}---- | See the README file for documentation: https://hackage.haskell.org/package/exinst#readme-module Exinst.Singletons- ( -- * 1 type index-   Some1(Some1)- , some1- , fromSome1- , _Some1- , withSome1- , withSome1Sing- , some1SingRep- , Dict1(dict1)--   -- * 2 type indexes- , Some2(Some2)- , some2- , fromSome2- , _Some2- , withSome2- , withSome2Sing- , some2SingRep- , Dict2(dict2)--   -- * 3 type indexes- , Some3(Some3)- , some3- , fromSome3- , _Some3- , withSome3- , withSome3Sing- , some3SingRep- , Dict3(dict3)--   -- * 4 type indexes- , Some4(Some4)- , some4- , fromSome4- , _Some4- , withSome4- , withSome4Sing- , some4SingRep- , Dict4(dict4)--   -- * Re-exports- , Dict(Dict)- ) where--import Data.Constraint-import Data.Kind (Type)-import Data.Profunctor (dimap, Choice(right'))-import Data.Singletons-import Data.Singletons.Decide-import Data.Type.Equality-import Prelude------------------------------------------------------------------------------------data Some1 (f1 :: k1 -> Type) = forall a1.-  Some1 !(Sing a1) !(f1 a1)--data Some2 (f2 :: k2 -> k1 -> Type) = forall a2 a1.-  Some2 !(Sing a2) !(Sing a1) !(f2 a2 a1)--data Some3 (f3 :: k3 -> k2 -> k1 -> Type) = forall a3 a2 a1.-  Some3 !(Sing a3) !(Sing a2) !(Sing a1) !(f3 a3 a2 a1)--data Some4 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) = forall a4 a3 a2 a1.-  Some4 !(Sing a4) !(Sing a3) !(Sing a2) !(Sing a1) !(f4 a4 a3 a2 a1)------------------------------------------------------------------------------------some1-  :: forall (f1 :: k1 -> Type) a1-  .  SingI a1-  => f1 a1-  -> Some1 f1 -- ^-some1 = Some1 (sing :: Sing a1)-{-# INLINE some1 #-}--some2-  :: forall (f2 :: k2 -> k1 -> Type) a2 a1-  .  (SingI a2, SingI a1)-  => f2 a2 a1-  -> Some2 f2 -- ^-some2 = Some2 (sing :: Sing a2) (sing :: Sing a1)-{-# INLINE some2 #-}--some3-  :: forall (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1-  .  (SingI a3, SingI a2, SingI a1)-  => f3 a3 a2 a1-  -> Some3 f3 -- ^-some3 = Some3 (sing :: Sing a3) (sing :: Sing a2) (sing :: Sing a1)-{-# INLINE some3 #-}--some4-  :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1-  .  (SingI a4, SingI a3, SingI a2, SingI a1)-  => f4 a4 a3 a2 a1-  -> Some4 f4 -- ^-some4 = Some4 (sing :: Sing a4) (sing :: Sing a3)-              (sing :: Sing a2) (sing :: Sing a1)-{-# INLINE some4 #-}------------------------------------------------------------------------------------withSome1-  :: forall (f1 :: k1 -> Type) (r :: Type)-   . Some1 f1-  -> (forall a1. SingI a1 => f1 a1 -> r)-  -> r -- ^-withSome1 s1 g = withSome1Sing s1 (\_ -> g)-{-# INLINABLE withSome1 #-}--withSome2-  :: forall (f2 :: k2 -> k1 -> Type) (r :: Type)-  .  Some2 f2-  -> (forall a2 a1. (SingI a2, SingI a1) => f2 a2 a1 -> r)-  -> r -- ^-withSome2 s2 g = withSome2Sing s2 (\_ _ -> g)-{-# INLINABLE withSome2 #-}--withSome3-  :: forall (f3 :: k3 -> k2 -> k1 -> Type) (r :: Type)-  .  Some3 f3-  -> (forall a3 a2 a1. (SingI a3, SingI a2, SingI a1) => f3 a3 a2 a1 -> r)-  -> r -- ^-withSome3 s3 g = withSome3Sing s3 (\_ _ _ -> g)-{-# INLINABLE withSome3 #-}--withSome4-  :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) (r :: Type)-  .  Some4 f4-  -> (forall a4 a3 a2 a1-        .  (SingI a4, SingI a3, SingI a2, SingI a1)-        => f4 a4 a3 a2 a1 -> r)-  -> r -- ^-withSome4 s4 g = withSome4Sing s4 (\_ _ _ _ -> g)-{-# INLINABLE withSome4 #-}-------------------------------------------------------------------------------------- | Like 'withSome1', but takes an explicit 'Sing' besides the 'SingI' instance.-withSome1Sing-  :: forall (f1 :: k1 -> Type) (r :: Type)-   . Some1 f1-  -> (forall a1. (SingI a1) => Sing a1 -> f1 a1 -> r)-  -> r -- ^-withSome1Sing (Some1 sa1 x) g = withSingI sa1 (g sa1 x)-{-# INLINABLE withSome1Sing #-}---- | Like 'withSome2', but takes explicit 'Sing's besides the 'SingI' instances.-withSome2Sing-  :: forall (f2 :: k2 -> k1 -> Type) (r :: Type)-  .  Some2 f2-  -> (forall a2 a1. (SingI a2, SingI a1) => Sing a2 -> Sing a1 -> f2 a2 a1 -> r)-  -> r -- ^-withSome2Sing (Some2 sa2 sa1 x) g = withSingI sa2 (withSingI sa1 (g sa2 sa1 x))-{-# INLINABLE withSome2Sing #-}---- | Like 'withSome3', but takes explicit 'Sing's besides the 'SingI' instances.-withSome3Sing-  :: forall (f3 :: k3 -> k2 -> k1 -> Type) (r :: Type)-  .  Some3 f3-  -> (forall a3 a2 a1-         .  (SingI a3, SingI a2, SingI a1)-         => Sing a3 -> Sing a2 -> Sing a1 -> f3 a3 a2 a1 -> r)-  -> r -- ^-withSome3Sing (Some3 sa3 sa2 sa1 x) g =-  withSingI sa3 (withSingI sa2 (withSingI sa1 (g sa3 sa2 sa1 x)))-{-# INLINABLE withSome3Sing #-}---- | Like 'withSome4', but takes explicit 'Sing's besides the 'SingI' instances.-withSome4Sing-  :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) (r :: Type)-  .  Some4 f4-  -> (forall a4 a3 a2 a1-        .  (SingI a4, SingI a3, SingI a2, SingI a1)-        => Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> f4 a4 a3 a2 a1 -> r)-  -> r -- ^-withSome4Sing (Some4 sa4 sa3 sa2 sa1 x) g =-  withSingI sa4 (withSingI sa3 (withSingI sa2 (withSingI sa1-     (g sa4 sa3 sa2 sa1 x))))-{-# INLINABLE withSome4Sing #-}------------------------------------------------------------------------------------fromSome1-   :: forall (f1 :: k1 -> Type) a1-    . (SingI a1, SDecide k1)-   => Some1 f1-   -> Maybe (f1 a1) -- ^-fromSome1 = \(Some1 sa1' x) -> do-   Refl <- testEquality sa1' (sing :: Sing a1)-   return x-{-# INLINABLE fromSome1 #-}--fromSome2-   :: forall (f2 :: k2 -> k1 -> Type) a2 a1-    . ( SingI a2, SDecide k2-      , SingI a1, SDecide k1 )-   => Some2 f2-   -> Maybe (f2 a2 a1) -- ^-fromSome2 = \(Some2 sa2' sa1' x) -> do-   Refl <- testEquality sa2' (sing :: Sing a2)-   Refl <- testEquality sa1' (sing :: Sing a1)-   return x-{-# INLINABLE fromSome2 #-}--fromSome3-   :: forall (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1-    . ( SingI a3, SDecide k3-      , SingI a2, SDecide k2-      , SingI a1, SDecide k1 )-   => Some3 f3-   -> Maybe (f3 a3 a2 a1) -- ^-fromSome3 = \(Some3 sa3' sa2' sa1' x) -> do-   Refl <- testEquality sa3' (sing :: Sing a3)-   Refl <- testEquality sa2' (sing :: Sing a2)-   Refl <- testEquality sa1' (sing :: Sing a1)-   return x-{-# INLINABLE fromSome3 #-}--fromSome4-   :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1-    . ( SingI a4, SDecide k4-      , SingI a3, SDecide k3-      , SingI a2, SDecide k2-      , SingI a1, SDecide k1 )-   => Some4 f4-   -> Maybe (f4 a4 a3 a2 a1) -- ^-fromSome4 = \(Some4 sa4' sa3' sa2' sa1' x) -> do-   Refl <- testEquality sa4' (sing :: Sing a4)-   Refl <- testEquality sa3' (sing :: Sing a3)-   Refl <- testEquality sa2' (sing :: Sing a2)-   Refl <- testEquality sa1' (sing :: Sing a1)-   return x-{-# INLINABLE fromSome4 #-}-------------------------------------------------------------------------------------- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some1'.-_Some1-  :: forall (f1 :: k1 -> Type) a1-  .  (SingI a1, SDecide k1)-  => Prism' (Some1 f1) (f1 a1)-_Some1 = prism' some1 fromSome1-{-# INLINE _Some1 #-}---- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some2'.-_Some2-  :: forall (f2 :: k2 -> k1 -> Type) a2 a1-  .  ( SingI a2, SDecide k2-     , SingI a1, SDecide k1 )-  => Prism' (Some2 f2) (f2 a2 a1)-_Some2 = prism' some2 fromSome2-{-# INLINE _Some2 #-}---- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some3'.-_Some3-  :: forall (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1-  .  ( SingI a3, SDecide k3-     , SingI a2, SDecide k2-     , SingI a1, SDecide k1 )-  => Prism' (Some3 f3) (f3 a3 a2 a1)-_Some3 = prism' some3 fromSome3-{-# INLINE _Some3 #-}---- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some4'.-_Some4-  :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1-  .  ( SingI a4, SDecide k4-     , SingI a3, SDecide k3-     , SingI a2, SDecide k2-     , SingI a1, SDecide k1 )-  => Prism' (Some4 f4) (f4 a4 a3 a2 a1)-_Some4 = prism' some4 fromSome4-{-# INLINE _Some4 #-}------------------------------------------------------------------------------------some1SingRep-  :: SingKind k1-  => Some1 (f1 :: k1 -> Type)-  -> DemoteRep k1 -- ^-some1SingRep = \(Some1 sa1 _) -> fromSing sa1-{-# INLINE some1SingRep #-}--some2SingRep-  :: (SingKind k2, SingKind k1)-  => Some2 (f2 :: k2 -> k1 -> Type)-  -> (DemoteRep k2, DemoteRep k1) -- ^-some2SingRep = \(Some2 sa2 sa1 _) -> (fromSing sa2, fromSing sa1)-{-# INLINE some2SingRep #-}--some3SingRep-  :: (SingKind k3, SingKind k2, SingKind k1)-  => Some3 (f3 :: k3 -> k2 -> k1 -> Type)-  -> (DemoteRep k3, DemoteRep k2, DemoteRep k1) -- ^-some3SingRep = \(Some3 sa3 sa2 sa1 _) ->-  (fromSing sa3, fromSing sa2, fromSing sa1)-{-# INLINE some3SingRep #-}--some4SingRep-  :: (SingKind k4, SingKind k3, SingKind k2, SingKind k1)-  => Some4 (f4 :: k4 -> k3 -> k2 -> k1 -> Type)-  -> (DemoteRep k4, DemoteRep k3, DemoteRep k2, DemoteRep k1) -- ^-some4SingRep = \(Some4 sa4 sa3 sa2 sa1 _) ->-  (fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1)-{-# INLINE some4SingRep #-}------------------------------------------------------------------------------------class Dict1 (c :: k0 -> Constraint) (f1 :: k1 -> k0) where-  -- | Runtime lookup of the @c (f1 a1)@ instance.-  dict1 :: Sing a1 -> Dict (c (f1 a1))--class Dict2 (c :: k0 -> Constraint) (f2 :: k2 -> k1 -> k0) where-  -- Runtime lookup of the @c (f2 a2 a1)@ instance.-  dict2 :: Sing a2 -> Sing a1 -> Dict (c (f2 a2 a1))--class Dict3 (c :: k0 -> Constraint) (f3 :: k3 -> k2 -> k1 -> k0) where-  -- Runtime lookup of the @c (f3 a3 a2 a1)@ instance.-  dict3 :: Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f3 a3 a2 a1))--class Dict4 (c :: k0 -> Constraint) (f4 :: k4 -> k3 -> k2 -> k1 -> k0) where-  -- Runtime lookup of the @c (f4 a4 a3 a2 a1)@ instance.-  dict4 :: Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f4 a4 a3 a2 a1))------------------------------------------------------------------------------------- Miscelaneous @lens@-compatible stuff.--type Prism s t a b-  = forall p f. (Choice p, Applicative f) => p a (f b) -> p s (f t)--type Prism' s a = Prism s s a a--prism :: (b -> t) -> (s -> Either t a) -> Prism s t a b-prism bt seta = dimap seta (either pure (fmap bt)) . right'-{-# INLINE prism #-}--prism' :: (b -> s) -> (s -> Maybe a) -> Prism s s a b-prism' bs sma = prism bs (\s -> maybe (Left s) Right (sma s))-{-# INLINE prism' #-}

@@ -0,0 +1,182 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}++module Main where++import Control.DeepSeq (NFData(rnf))+import qualified Data.Aeson as Aeson+import qualified Data.Bytes.Get as Bytes+import qualified Data.Bytes.Put as Bytes+import qualified Data.Bytes.Serial as Bytes+import Data.Hashable (Hashable(hash))+import Data.Kind (Type)+import Data.Proxy (Proxy)+import Generic.Random.Generic (genericArbitrary, uniform)+import qualified GHC.Generics as G+import qualified Test.Tasty as Tasty+import qualified Test.Tasty.Runners as Tasty+import Test.Tasty.QuickCheck ((===))+import qualified Test.Tasty.QuickCheck as QC++import Data.Singletons (SingKind, Sing, DemoteRep, withSomeSing)++import Exinst++--------------------------------------------------------------------------------++main :: IO ()+main = Tasty.defaultMainWithIngredients+  [ Tasty.consoleTestReporter+  , Tasty.listingTests+  ] tt++--------------------------------------------------------------------------------++tt :: Tasty.TestTree+tt =+  Tasty.testGroup "main"+  [ tt_id "Identity through GHC's Generic" id_generic+  , tt_id "Identity through Aeson's FromJSON/ToJSON" id_aeson+  , tt_id "Identity through Bytes's Serial" id_bytes+  , tt_nfdata+  ]++tt_id+  :: String+  -> (forall a.+        ( G.Generic a, Aeson.FromJSON a, Aeson.ToJSON a, Bytes.Serial a+        ) => a -> Maybe a+     ) -- ^ It's easier to put all the constraints here.+  -> Tasty.TestTree+tt_id = \title id' -> Tasty.testGroup title+  [ QC.testProperty "Some1" $+      QC.forAll QC.arbitrary $ \(x :: Some1 Foo1) -> Just x === id' x+  , QC.testProperty "Some2" $+      QC.forAll QC.arbitrary $ \(x :: Some2 Foo2) -> Just x === id' x+  , QC.testProperty "Some3" $+      QC.forAll QC.arbitrary $ \(x :: Some3 Foo3) -> Just x === id' x+  , QC.testProperty "Some4" $+      QC.forAll QC.arbitrary $ \(x :: Some4 Foo4) -> Just x === id' x+  ]++tt_nfdata :: Tasty.TestTree+tt_nfdata = Tasty.testGroup "NFData"+  [ QC.testProperty "Some1" $+      QC.forAll QC.arbitrary $ \(x :: Some1 Foo1) -> () === rnf x+  , QC.testProperty "Some2" $+      QC.forAll QC.arbitrary $ \(x :: Some2 Foo2) -> () === rnf x+  , QC.testProperty "Some3" $+      QC.forAll QC.arbitrary $ \(x :: Some3 Foo3) -> () === rnf x+  , QC.testProperty "Some4" $+      QC.forAll QC.arbitrary $ \(x :: Some4 Foo4) -> () === rnf x+  ]++tt_hashable :: Tasty.TestTree+tt_hashable = Tasty.testGroup "Hashable"+  [ QC.testProperty "Some1" $+      QC.forAll QC.arbitrary $ \(x :: Some1 Foo1) -> () === (hash x `seq` ())+  , QC.testProperty "Some2" $+      QC.forAll QC.arbitrary $ \(x :: Some2 Foo2) -> () === (hash x `seq` ())+  , QC.testProperty "Some3" $+      QC.forAll QC.arbitrary $ \(x :: Some3 Foo3) -> () === (hash x `seq` ())+  , QC.testProperty "Some4" $+      QC.forAll QC.arbitrary $ \(x :: Some4 Foo4) -> () === (hash x `seq` ())+  ]++--------------------------------------------------------------------------------++id_generic :: G.Generic a => a -> Maybe a+id_generic = Just . G.to . G.from++id_aeson :: (Aeson.FromJSON a, Aeson.ToJSON a) => a -> Maybe a+id_aeson = Aeson.decode . Aeson.encode++id_bytes :: Bytes.Serial a => a -> Maybe a+id_bytes = \a ->+  let bs = Bytes.runPutS (Bytes.serialize a)+  in case Bytes.runGetS Bytes.deserialize bs of+       Left _ -> Nothing+       Right a' -> Just a'++--------------------------------------------------------------------------------++data family Foo1 :: Bool -> Type+data instance Foo1 'False = F1 | F2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)+data instance Foo1 'True = T1 | T2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)++data family Foo2 :: Bool -> Bool -> Type+data instance Foo2 'False 'False = FF1 | FF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)+data instance Foo2 'False 'True = FT1 | FT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)+data instance Foo2 'True 'False = TF1 | TF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)+data instance Foo2 'True 'True = TT1 | TT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)++data family Foo3 :: Bool -> Bool -> Bool -> Type+data instance Foo3 'False 'False 'False = FFF1 | FFF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)+data instance Foo3 'False 'False 'True = FFT1 | FFT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)+data instance Foo3 'False 'True 'False = FTF1 | FTF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)+data instance Foo3 'False 'True 'True = FTT1 | FTT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)+data instance Foo3 'True 'False 'False = TFF1 | TFF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)+data instance Foo3 'True 'False 'True = TFT1 | TFT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)+data instance Foo3 'True 'True 'False = TTF1 | TTF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)+data instance Foo3 'True 'True 'True = TTT1 | TTT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)++data family Foo4 :: Bool -> Bool -> Bool -> Bool -> Type+data instance Foo4 'False 'False 'False 'False = FFFF1 | FFFF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)+data instance Foo4 'False 'False 'False 'True = FFFT1 | FFFT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)+data instance Foo4 'False 'False 'True 'False = FFTF1 | FFTF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)+data instance Foo4 'False 'False 'True 'True = FFTT1 | FFTT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)+data instance Foo4 'False 'True 'False 'False = FTFF1 | FTFF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)+data instance Foo4 'False 'True 'False 'True = FTFT1 | FTFT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)+data instance Foo4 'False 'True 'True 'False = FTTF1 | FTTF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)+data instance Foo4 'False 'True 'True 'True = FTTT1 | FTTT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)+data instance Foo4 'True 'False 'False 'False = TFFF1 | TFFF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)+data instance Foo4 'True 'False 'False 'True = TFFT1 | TFFT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)+data instance Foo4 'True 'False 'True 'False = TFTF1 | TFTF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)+data instance Foo4 'True 'False 'True 'True = TFTT1 | TFTT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)+data instance Foo4 'True 'True 'False 'False = TTFF1 | TTFF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)+data instance Foo4 'True 'True 'False 'True = TTFT1 | TTFT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)+data instance Foo4 'True 'True 'True 'False = TTTF1 | TTTF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)+data instance Foo4 'True 'True 'True 'True = TTTT1 | TTTT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable)++--------------------------------------------------------------------------------+-- Arbitrary instances++instance QC.Arbitrary (Foo1 'False) where arbitrary = genericArbitrary uniform+instance QC.Arbitrary (Foo1 'True) where arbitrary = genericArbitrary uniform++instance QC.Arbitrary (Foo2 'False 'False) where arbitrary = genericArbitrary uniform+instance QC.Arbitrary (Foo2 'False 'True) where arbitrary = genericArbitrary uniform+instance QC.Arbitrary (Foo2 'True 'False) where arbitrary = genericArbitrary uniform+instance QC.Arbitrary (Foo2 'True 'True) where arbitrary = genericArbitrary uniform++instance QC.Arbitrary (Foo3 'False 'False 'False) where arbitrary = genericArbitrary uniform+instance QC.Arbitrary (Foo3 'False 'False 'True) where arbitrary = genericArbitrary uniform+instance QC.Arbitrary (Foo3 'False 'True 'False) where arbitrary = genericArbitrary uniform+instance QC.Arbitrary (Foo3 'False 'True 'True) where arbitrary = genericArbitrary uniform+instance QC.Arbitrary (Foo3 'True 'False 'False) where arbitrary = genericArbitrary uniform+instance QC.Arbitrary (Foo3 'True 'False 'True) where arbitrary = genericArbitrary uniform+instance QC.Arbitrary (Foo3 'True 'True 'False) where arbitrary = genericArbitrary uniform+instance QC.Arbitrary (Foo3 'True 'True 'True) where arbitrary = genericArbitrary uniform++instance QC.Arbitrary (Foo4 'False 'False 'False 'False) where arbitrary = genericArbitrary uniform+instance QC.Arbitrary (Foo4 'False 'False 'False 'True) where arbitrary = genericArbitrary uniform+instance QC.Arbitrary (Foo4 'False 'False 'True 'False) where arbitrary = genericArbitrary uniform+instance QC.Arbitrary (Foo4 'False 'False 'True 'True) where arbitrary = genericArbitrary uniform+instance QC.Arbitrary (Foo4 'False 'True 'False 'False) where arbitrary = genericArbitrary uniform+instance QC.Arbitrary (Foo4 'False 'True 'False 'True) where arbitrary = genericArbitrary uniform+instance QC.Arbitrary (Foo4 'False 'True 'True 'False) where arbitrary = genericArbitrary uniform+instance QC.Arbitrary (Foo4 'False 'True 'True 'True) where arbitrary = genericArbitrary uniform+instance QC.Arbitrary (Foo4 'True 'False 'False 'False) where arbitrary = genericArbitrary uniform+instance QC.Arbitrary (Foo4 'True 'False 'False 'True) where arbitrary = genericArbitrary uniform+instance QC.Arbitrary (Foo4 'True 'False 'True 'False) where arbitrary = genericArbitrary uniform+instance QC.Arbitrary (Foo4 'True 'False 'True 'True) where arbitrary = genericArbitrary uniform+instance QC.Arbitrary (Foo4 'True 'True 'False 'False) where arbitrary = genericArbitrary uniform+instance QC.Arbitrary (Foo4 'True 'True 'False 'True) where arbitrary = genericArbitrary uniform+instance QC.Arbitrary (Foo4 'True 'True 'True 'False) where arbitrary = genericArbitrary uniform+instance QC.Arbitrary (Foo4 'True 'True 'True 'True) where arbitrary = genericArbitrary uniform+