packages feed

exinst 0.4 → 0.5

raw patch · 29 files changed

+3102/−2820 lines, 29 filesdep +cborgdep +serialisedep ~singletonsPVP ok

version bump matches the API change (PVP)

Dependencies added: cborg, serialise

Dependency ranges changed: singletons

API changes (from Hackage documentation)

+ Exinst: same1 :: SDecide k1 => (forall a1. SingI a1 => f a1 -> g a1 -> x) -> Some1 (f :: k1 -> Type) -> Some1 (g :: k1 -> Type) -> Maybe x
+ Exinst: same2 :: (SDecide k2, SDecide k1) => (forall a2 a1. SingI a1 => f a2 a1 -> g a2 a1 -> x) -> Some2 (f :: k2 -> k1 -> Type) -> Some2 (g :: k2 -> k1 -> Type) -> Maybe x
+ Exinst: same3 :: (SDecide k3, SDecide k2, SDecide k1) => (forall a3 a2 a1. (SingI a3, SingI a2, SingI a1) => f a3 a2 a1 -> g a3 a2 a1 -> x) -> Some3 (f :: k3 -> k2 -> k1 -> Type) -> Some3 (g :: k3 -> k2 -> k1 -> Type) -> Maybe x
+ Exinst: same4 :: (SDecide k4, SDecide k3, SDecide k2, SDecide k1) => (forall a4 a3 a2 a1. (SingI a4, SingI a3, SingI a2, SingI a1) => f a4 a3 a2 a1 -> g a4 a3 a2 a1 -> x) -> Some4 (f :: k4 -> k3 -> k2 -> k1 -> Type) -> Some4 (g :: k4 -> k3 -> k2 -> k1 -> Type) -> Maybe x
- Exinst: data Dict (a :: Constraint) :: Constraint -> *
+ Exinst: data Dict a :: Constraint -> *
- Exinst: some1SingRep :: SingKind k1 => Some1 (f1 :: k1 -> Type) -> DemoteRep k1
+ Exinst: some1SingRep :: SingKind k1 => Some1 (f1 :: k1 -> Type) -> Demote k1
- Exinst: some2SingRep :: (SingKind k2, SingKind k1) => Some2 (f2 :: k2 -> k1 -> Type) -> (DemoteRep k2, DemoteRep k1)
+ Exinst: some2SingRep :: (SingKind k2, SingKind k1) => Some2 (f2 :: k2 -> k1 -> Type) -> (Demote k2, Demote k1)
- Exinst: some3SingRep :: (SingKind k3, SingKind k2, SingKind k1) => Some3 (f3 :: k3 -> k2 -> k1 -> Type) -> (DemoteRep k3, DemoteRep k2, DemoteRep k1)
+ Exinst: some3SingRep :: (SingKind k3, SingKind k2, SingKind k1) => Some3 (f3 :: k3 -> k2 -> k1 -> Type) -> (Demote k3, Demote k2, Demote k1)
- Exinst: some4SingRep :: (SingKind k4, SingKind k3, SingKind k2, SingKind k1) => Some4 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) -> (DemoteRep k4, DemoteRep k3, DemoteRep k2, DemoteRep k1)
+ Exinst: some4SingRep :: (SingKind k4, SingKind k3, SingKind k2, SingKind k1) => Some4 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) -> (Demote k4, Demote k3, Demote k2, Demote k1)

Files

CHANGELOG.md view
@@ -1,3 +1,14 @@+# Version 0.5++* BREAKING: Depend on `singletons == 2.3.*`.++* Add `same{1,2,3,4}`.++* Add dependencies on `cborg` and `serialise`++* Add instances for `serialise` (binary CBOR encoding/decoding)++ # Version 0.4  * BREAKING: Decouple `binary` and `cereal` instances from `bytes`. This
LICENSE.txt view
@@ -1,4 +1,4 @@-Copyright (c) 2015-2017, Renzo Carbonara+Copyright (c) 2015-2018, Renzo Carbonara  All rights reserved.
exinst.cabal view
@@ -1,21 +1,21 @@ name:                exinst-version:             0.4+version:             0.5 author:              Renzo Carbonara maintainer:          renzoλcarbonara.com.ar-copyright:           Renzo Carbonara 2015-2017+copyright:           Renzo Carbonara 2015-2018 license:             BSD3 license-file:        LICENSE.txt extra-source-files:  README.md CHANGELOG.md category:            Data build-type:          Simple cabal-version:       >=1.18-synopsis:            Recover type indexes and instances for your existentialized types.+synopsis:            Dependent pairs and their instances. homepage:            https://github.com/k0001/exinst bug-reports:         https://github.com/k0001/exinst/issues   library-  hs-source-dirs: src/lib+  hs-source-dirs: lib   default-language: Haskell2010   exposed-modules:       Exinst@@ -28,37 +28,47 @@       base >=4.9 && <5.0     , constraints >=0.4     , profunctors >=5.0-    , singletons >=2.2+    , singletons >=2.3.1   ghcjs-options: -Wall -O3   ghc-options: -Wall -O2    if flag(aeson)     build-depends: aeson     other-modules: Exinst.Instances.Aeson+    cpp-options: -DHAS_aeson   if flag(binary) || flag(bytes)     build-depends: binary     other-modules: Exinst.Instances.Binary+    cpp-options: -DHAS_binary   if flag(bytes)     build-depends: bytes >=0.15     other-modules: Exinst.Instances.Bytes+    cpp-options: -DHAS_bytes   if flag(cereal) || flag(bytes)     build-depends: cereal     other-modules: Exinst.Instances.Cereal+    cpp-options: -DHAS_cereal   if flag(deepseq)     build-depends: deepseq     other-modules: Exinst.Instances.DeepSeq+    cpp-options: -DHAS_deepseq   if flag(hashable)     build-depends: hashable     other-modules: Exinst.Instances.Hashable+    cpp-options: -DHAS_hashable   if flag(quickcheck)     build-depends: QuickCheck     other-modules: Exinst.Instances.QuickCheck-+    cpp-options: -DHAS_quickcheck+  if flag(serialise)+    build-depends: cborg, serialise+    other-modules: Exinst.Instances.Serialise+    cpp-options: -DHAS_serialise  test-suite tests   default-language: Haskell2010   type: exitcode-stdio-1.0-  hs-source-dirs: tests src/lib+  hs-source-dirs: tests lib   main-is: Main.hs   build-depends:      aeson@@ -66,17 +76,27 @@    , binary    , bytes    , bytestring+   , cborg    , cereal    , constraints    , deepseq    , hashable    , profunctors    , QuickCheck+   , serialise    , singletons    , tasty    , tasty-hunit    , tasty-quickcheck-+  cpp-options:+    -DHAS_aeson+    -DHAS_binary+    -DHAS_bytes+    -DHAS_cereal+    -DHAS_deepseq+    -DHAS_hashable+    -DHAS_quickcheck+    -DHAS_serialise  flag aeson   description: Provide instances for @aeson@@@ -104,5 +124,9 @@   manual: True flag quickcheck   description: Provide instances for @QuickCheck@+  default: True+  manual: True+flag serialise+  description: Provide instances for @serialise@   default: True   manual: True
+ lib/Exinst.hs view
@@ -0,0 +1,685 @@+{-# LANGUAGE CPP #-}++{- |++Exinst is a library providing you with tools to recover type-indexed types whose+type-indexes have been existentialized, as well as automatically deriving+instances for them, as long as said type indexes are singleton types+(see [singleton](https://hackage.haskell.org/package/singletons)).++In short, what @exinst@ currently gives you is: For any type @t :: k -> *@, if+@k@ is a singleton type and @c (t a) :: 'Constraint'@ is satisfied, then you can+existentialize away the @a@ parameter with @'Some1' t@, recover it later, and+have @c ('Some1' t)@ automatically satisfied. Currently, up to 4 type indexes+can be existentialized using 'Some1', 'Some2', 'Some3' and 'Some4' respectively.++NOTE: This tutorial asumes some familiarity with singleton types as implemented+by the [singleton](https://hackage.haskell.org/package/singletons) library.+A singleton type is, in very rough terms, a type inhabited by a single term,+which allows one to go from its term-level representation to its type-level+representation and back without much trouble. A bit like the term @()@, which+is of type @()@. Whenever you have the type @()@ you know what that its+term-level representation must be @()@, and whenever you have the term @()@+you know that its type must be @()@.++-}++module Exinst+ ( -- * Tutorial+   -- $motivation++   -- *** Usage+   -- $usage++   -- *** Recovering+   -- $recovering++   -- *** Many indexes+   -- $manyIndexes++   -- *** Writing instances+   -- $writingInstances++   -- *** Products and sums+   -- $prodsums++   -- * 1 type index+   Some1(Some1)+ , some1+ , fromSome1+ , _Some1+ , withSome1+ , withSome1Sing+ , some1SingRep+ , same1+ , Dict1(dict1)++   -- * 2 type indexes+ , Some2(Some2)+ , some2+ , fromSome2+ , _Some2+ , withSome2+ , withSome2Sing+ , some2SingRep+ , same2+ , Dict2(dict2)++   -- * 3 type indexes+ , Some3(Some3)+ , some3+ , fromSome3+ , _Some3+ , withSome3+ , withSome3Sing+ , some3SingRep+ , same3+ , Dict3(dict3)++   -- * 4 type indexes+ , Some4(Some4)+ , some4+ , fromSome4+ , _Some4+ , withSome4+ , withSome4Sing+ , some4SingRep+ , same4+ , Dict4(dict4)++   -- * Miscellaneous+ , Dict0(dict0)++   -- * Products+ , P1(P1)+ , P2(P2)+ , P3(P3)+ , P4(P4)++   -- * Sums+ , S1(S1L,S1R)+ , S2(S2L,S2R)+ , S3(S3L,S3R)+ , S4(S4L,S4R)++   -- * Re-exports+ , Constraint+ , Dict(Dict)+ , Sing+ , SingI+ ) where++import Data.Constraint (Constraint, Dict(Dict))++import Data.Singletons (Sing, SingI)++import Exinst.Internal+import Exinst.Internal.Product+import Exinst.Internal.Sum++import Exinst.Instances.Base ()++#ifdef HAS_aeson+import Exinst.Instances.Aeson ()+#endif++#ifdef HAS_binary+import Exinst.Instances.Binary ()+#endif++#ifdef HAS_bytes+import Exinst.Instances.Bytes ()+#endif++#ifdef HAS_cereal+import Exinst.Instances.Cereal ()+#endif++#ifdef HAS_deepseq+import Exinst.Instances.DeepSeq ()+#endif++#ifdef HAS_hashable+import Exinst.Instances.Hashable ()+#endif++#ifdef HAS_quickcheck+import Exinst.Instances.QuickCheck ()+#endif++#ifdef HAS_serialise+import Exinst.Instances.Serialise ()+#endif+++{- $motivation++As a motivation, let's consider the following example:++@+\{\-\# LANGUAGE GADTs \#\-\}+\{\-\# LANGUAGE DataKinds \#\-\}+\{\-\# LANGUAGE KindSignatures \#\-\}+\{\-\# LANGUAGE FlexibleInstances \#\-\}+\{\-\# LANGUAGE StandaloneDeriving \#\-\}++data Size = Big | Small++data Receptacle (a :: Size) :: * where+  Vase :: Receptacle 'Small+  Glass :: Receptacle 'Small+  Barrel :: Receptacle 'Big++deriving instance 'Show' (Receptacle a)+@++@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@.++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 have @[Receptacle 'Small]@ and @[Receptacle 'Big]@, but we+can't have @[Receptacle]@ nor @[forall a. Receptacle a]@. So, if we want to+have @Receptacle@s of different sizes in a container like @[]@, we need a+different solution.++At this point we need to ask ourselves why we need to put @Receptacle@s of+different sizes in a same container. If the answer is something like “because we+want to show all of them, no matter what size they are”, then we should realize+that what we are actually asking for is that no matter what @Size@ our+@Receptable@ has, we need to be able to find a 'Show' instance for that+@Receptacle@. In Haskell, we can express just that using existential types+and constraints hidden behind a data constructor.++@+-- We need to add these language extensions to the ones in the previous example+\{\-\# LANGUAGE ExistentialQuantification \#\-\}+\{\-\# LANGUAGE FlexibleContexts \#\-\}++data ReceptacleOfAnySizeThatCanBeShown+  = forall a. ('Show' (Receptacle a))+      => MkReceptacleOfAnySizeThatCanBeShown (Receptacle a)+@++We can construct values of type @ReceptacleOfAnySizeThatCanBeShown@ only as long+as there exist a 'Show' instance for the @Receptacle a@ we give to the+@MkReceptacleOfAnySizeThatCanBeShown@ constructor. In our case, both @Receptacle+'Small@ and @Receptacle 'Big@ have 'Show' instances, so all of @Vase@, @Glass@ and+@Barrel@ can be used successfully with @MkReceptacleOfAnySizeThatCanBeShown@.++Now, @ReceptacleOfAnySizeThatCanBeShown@ on itself doesn't yet have a 'Show'+instance, and we can't derive one automatically using the @deriving@ mechanism,+but we can give an explicit 'Show' instance that just forwards the work to the+'Show' instance of the underlying @Receptacle a@.++@+instance 'Show' ReceptacleOfAnySizeThatCanBeShown where+  'show' (MkReceptacleOfAnySizeThatCanBeShown a) = 'show' a+@++That works as intended:++@+> 'show' (MkReceptacleOfAnySizeThatCanBeShown Vase)+"Vase"+> 'show' (MkReceptacleOfAnySizeThatCanBeShown Barrel)+"Barrel"+@++And now, as we wanted, we can put @Receptacle@s of different sizes in a @[]@ and+show them (as long as we wrap each of them as+@ReceptacleOfAnySizeThatCanBeShown@, that is).++@+> 'map' 'show' [MkReceptacleOfAnySizeThatCanBeShown Vase, MkReceptacleOfAnySizeThatCanBeShown Barrel]+["Vase", "Barrel"]+@++However, the above solution is unsatisfying for various reasons: For one, the+'Show' instance for @ReceptacleOfAnySizeThatCanBeShown@ works only as long as+the @ReceptacleOfAnySizeThatCanBeShown@ itself carries a witness that the 'Show'+constraint for @Receptacle a@ is satisfied, which means that if we want to write+yet another instance for @ReceptacleOfAnySizeThatCanBeShown@ that simply forwards+its implementation to the underlying @Receptacle a@, say 'Eq', then the+@MkReceptacleOfAnySizeThatCanBeShown@ constructor would need to be modified to witness+the @Eq (Receptacle a)@ instance too:++@+data ReceptacleOfAnySizeThatCanBeShown+  = forall a. ('Show' (Receptacle a), 'Eq' (Receptacle a))+      => MkReceptacleOfAnySizeThatCanBeShown (Receptacle a)+@++With that in place we can provide an 'Eq' instance for+@ReceptacleOfAnySizeThatCanBeShown@ as we did for 'Show' before, but if we pay+close attention, we can see how the implementation of+@ReceptacleOfAnySizeThatCanBeShown@ starts to become a bottleneck: Every+instance we want to provide for @ReceptacleOfAnySizeThatCanBeShown@ that simply+forwards its work to the underlying @Receptacle a@ needs to be witnessed by+@MkReceptacleOfAnySizeThatCanBeShown@ itself, it is not enough that there exists+an instance for @Receptacle a@. Moreover, even the name+@ReceptacleOfAnySizeThatCanBeShown@ that we chose before isn't completely+accurate anymore, and will become less and less accurate as we continue adding+constraints to @MkReceptacleOfAnySizeThatCanBeShown@.++Additionally, everywhere we use the @MkReceptacleOfAnySizeThatCanBeShown@+constructor we need to witness that the existentialized @Receptacle a@ satisfies+all the required constraints, which means that, if the @Receptacle a@ we pass to+@MkReceptacleOfAnySizeThatCanBeShown@ is being received, say, as a parameter to+a function, then the type of that function will also require that its caller+satisfies all of the same constraints, even though it is obvious to us,+statically, that the instances exist. We can now see how all of this becomes+unmanegeable, or at least very *boilerplatey*, as those constraints start to+propagate through our code base.++What we need is a way for instances such as the 'Show' instance for+@ReceptacleOfAnySizeThatCanBeShown@ to find the 'Show' instance for @Receptacle+a@ without it being explicitely witnessed by the+@MkReceptacleOfAnySizeThatCanBeShown@ constructor. That is exactly the problem+that @exinst@ solves: allowing /exi/stentials to find their /inst/ances. Thus,+the name of this library.++-}++{- $usage++Given the code for @Size@, @Receptacle@ and its 'Show' instances above, we can+achieve the same functionality as our initial @ReceptacleOfAnySizeThatCanBeShown@ by+existentializing the type indexes of @Receptacle 'Small@ and @Receptacle 'Big@+as @'Some1' Receptacle@. In order to do that, we must first ensure that @Size@ and its+constructors can be used as singleton types (as supported by the @singletons@ library),+for which we can use some @TemplateHaskell@ provided by @Data.Singletons.TH@:++@+import qualified "Data.Singletons.TH"++Data.Singletons.TH.genSingletons [''Size]+@++And we'll also need a 'Show' instance for @Size@ for reasons that will become+apparent later:++@+deriving instance 'Show' Size+@++Now we can construct a @Show1 Size@ and 'show' achieving the same results as we+did with @ReceptacleOfAnySizeThatCanBeShown@ before.++Note: this code won't work yet. Keep reading.++@+> import "Exinst" ('Some1', 'some1')+> :t 'some1' Glass+:t 'some1' Glass :: 'Some1' Receptacle+> 'show' ('some1' Glass)+"Some1 Small Glass"+@++Well, actually, the default 'Show' instance for 'Some1' shows a bit more of+information, as it permits this string to be 'Read' back into a @'Some1'+Receptacle@ if needed, but displaying just @"Glass"@ would be possible too, if+desired.++The important thing to notice in the example above is that @some1@ does not+require us to satisfy a @'Show' (Receptacle 'Small)@ constraint, it just requires+that the type index for the type-indexed type we give it as argument is a+singleton type:++@+'some1' :: forall (f1 :: k1 -> *) (a1 :: k1). 'SingI' a1 => f1 a1 -> 'Some1' f1+@++It is the application of 'show' to @'some1' Glass@ which will fail to compile if+there isn't a 'Show' instance for @Receptacle 'Small@, complaining that a 'Show'+instance for @'Some1' Receptable@ can't be found. The reason for this is that even+if 'Show' instances for 'Some1' are derived for free, they are only derived for+@'Some1' (t :: k1 -> *)@ where a @'Show' (t a)@ for a specific but statically+unknown @a@ can be found at runtime (mostly, there are other minor requirements too).+The mechanism through which instances are found at runtime relies on 'Dict' from+the [constraints](https://hackage.haskell.org/package/constraints) library, which+@exinst@ wraps in a 'Dict1' typeclass to be instantiated once per singleton+type.++@+-- The "Exinst.Dict1" class+class 'Dict1' (c :: k0 -> 'Constraint') (f1 :: k1 -> k0) where+  'dict1' :: 'Sing' (a1 :: k1) -> 'Dict' (c (f1 a1))+@++What 'Dict1' says is that: for a type-indexed type @f1@, given a term-level+representation of the singleton type that indexes said @f1@, we can obtain a+witness that the constraint @c@ is satisfied by @f1@ applied to the singleton+type.++That class seems to be a bit too abstract, but the instances we as users need to+write for it are quite silly and straightforward.++Here's an example of how to provide 'Show' support for @'Some1' Receptacle@ via+'Dict1':++@+instance ('Show' (Receptacle 'Small), 'Show' (Receptacle 'Big)) => 'Dict1' 'Show' Receptacle where+  'dict1' = \x -> case x of+    SSmall -> 'Dict'+    SBig -> 'Dict'+@++The implementation of @dict1@ looks quite silly, but it has to look like that as+it is only by pattern-matching on each of the @'Sing' Size@ constructors that we+learn about the type level representation of a singleton type, which we then use+to select the proper 'Show' instance among all of those listed in the instance head.++Given this 'Dict1' instance, we can proceed to excecute the REPL example mentioned before+and it will work just fine.++However, that 'Dict1' instance is still a bit insatisfactory: If we wanted,+again, to provide 'Eq' support for our @'Some1' Receptacle@ type, we would need to+write yet another 'Dict1' instance like the one above, but mentioning 'Eq'+instead of 'Show'. We can do better.++The trick, when writing 'Dict1' instances such as the one above, is to leave @c@+and @f1 :: k1 -> k0@ completely polymorphic, and instead only talk concretely+about the singleton type with kind @k1@. This might sound strange at first, as+@c@ and @f1@ are the only two type parameters to 'Dict1'. But as it often happens+when working with singleton types, we are not particularly interested in the+types involved, but in their kinds instead. So, this is the 'Dict1' instance+you often want to write:++@+instance (c (f1 'Small), c (f1 'Big)) => 'Dict1' c (f1 :: Size -> k0) where+  'dict1' = \x -> case x of+    SSmall -> 'Dict'+    SBig -> 'Dict'+@++That instance says that for any choice of @c@ and @f1 :: Size -> k0@, if an+instance for @c (f1 a)@ exists for a specific choice of @a@, then, given a term+level representation for that @a@ and the aid of @dict1@, said instance can be+looked up at runtime.++Notice that 'Some1' itself doesn't have any requirements about 'Dict1', it's the+various instances for 'Some1' who rely on 'Dict1'. 'Dict1' has nothing to do+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@.++The @Exinst@ module exports ready-made instances for 'Some1', 'Some2', 'Some3'+and 'Some4' (they can be enabled or disabled with some cabal flags).++* 'Eq', 'Ord', 'Show' from the @base@ package.++* 'Data.Aeson.FromJSON' and 'Data.Aeson.ToJSON' from the @aeson@ package.++* 'Data.Bytes.Serial' from the @bytes@ package.++* 'Cereal.Serialize.Serialize' from the @cereal@ package.++* 'Data.Binary.Binary' from the @binary@ package.++* 'Data.Hashable.Hashable' from the @hashable@ package.++* 'Control.DeepSeq.NFData' from the @deepseq@ package.++* 'Test.QuickCheck.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+@class Y => Z a@ satisfied for @'Some1' (f :: k1 -> *)@, then make sure an instance+for @Z@ is available for the @DemoteRep k1@, that a @'Dict1' Z (f :: k1 -> k0)@ or+more general instance exists, and that the @Y@ instance for @'Some1' (f :: k1 ->+*)@ exists too.++Here is the full code needed to have, say, the 'Eq' and 'Show' instances+available for @'Some1' Receptacle@:++@+\{\-\# LANGUAGE ConstraintKinds \#\-\}+\{\-\# LANGUAGE DataKinds \#\-\}+\{\-\# LANGUAGE FlexibleInstances \#\-\}+\{\-\# LANGUAGE GADTs \#\-\}+\{\-\# LANGUAGE KindSignatures \#\-\}+\{\-\# LANGUAGE MultiParamTypeClasses \#\-\}+\{\-\# LANGUAGE OverloadedStrings \#\-\}+\{\-\# LANGUAGE StandaloneDeriving \#\-\}+\{\-\# LANGUAGE TemplateHaskell \#\-\}+\{\-\# LANGUAGE TypeFamilies \#\-\}+\{\-\# LANGUAGE UndecidableInstances \#\-\}++import qualified "Data.Singletons.TH"+import           "Exinst" ('Dict'('Dict'), 'Dict1'('dict1'))++data Size = Big | Small+  deriving ('Eq', 'Show')++Data.Singletons.TH.genSingletons [''Size]+Data.Singletons.TH.singDecideInstances [''Size]++instance (c (f 'Big), c (f 'Small)) => 'Dict1' c f where+  'dict1' = \x -> case x of+    SBig -> 'Dict'+    SSmall -> 'Dict'+++data Receptacle (a :: Size) :: * where+  Vase :: Receptacle 'Small+  Glass :: Receptacle 'Small+  Barrel :: Receptacle 'Big++deriving instance 'Eq' (Receptacle a)+deriving instance 'Show' (Receptacle a)+@++Now, @'Some1' Receptacle@ will have 'Eq' and 'Show' instances:++@+> -- Trying 'fromSome1'.+> 'fromSome1' ('some1' Vase) == 'Just' Vase+'True'+> 'fromSome1' ('some1' Vase) == 'Just' Glass+'False'+> 'fromSome1' ('some1' Vase) == 'Just' Barrel+'False'++> -- Trying 'withSome1'+> 'withSome1' ('some1' Vase) 'show'+"Vase"+> 'withSome1' ('some1' Vase) (== Vase)    -- This will fail, use 'fromSome1'+                                      -- if you know you are expecting+                                      -- a @Receptacle 'Small@++> -- Trying the 'Eq' instance.+> 'some1' Vase == 'some1' Vase+'True'+> 'some1' Vase == 'some1' Glass+'False'+> 'some1' Vase == 'some1' Barrel+'False'++> -- Trying the 'Show' instance.+> 'show' ('some1' Vase)+"Some1 Small Vase"+> 'map' 'show' ['some1' Vase, 'some1' Glass, 'some1' Barrel]+["Some1 Small Vase","Some1 Small Glass","Some1 Big Barrel"]+@++-}++{- $manyIndexes++Just like 'Some1' hides the last singleton type index from fully applied+type-indexed type, 'Some2' hides the last two type indexes, 'Some3' hides the+last three, and 'Some3' hides the last four. They can be used in the same way as+'Some1'.++Like as most instances for 'Some1' require 'Dict1' instances to be present for+their singleton type-index, most instances for 'Some2', 'Some3' and 'Some4' will+require that 'Dict2', 'Dict3' or 'Dict4' instances exist, respectively. Writing+these instances is very straightforward. Supposing you have a type @X :: T4 ->+T3 -> T2 -> T1 -> *@ and want to existentialize all of the four type indexes yet+be able to continue using all of its instances, we can write something like+this:++@+instance (c (f1 'T1a), c (f1 'T1b)) => 'Dict1' c (f1 :: T1 -> k0) where+  'dict1' = \x -> case x of { ST1a -> 'Dict'; ST1b -> 'Dict' }+instance ('Dict1' c (f2 'T2a), 'Dict1' c (f2 'T2b)) => 'Dict2' c (f2 :: T2 -> k1 -> k0) where+  'dict2' = \x -> case x of { ST2a -> 'dict1'; ST2b -> 'dict1' }+instance ('Dict2' c (f3 'T3a), 'Dict2' c (f3 'T3b)) => 'Dict3' c (f3 :: T3 -> k2 -> k1 -> k0) where+  'dict3' = \x -> case x of { ST3a -> 'dict2'; ST3b -> 'dict2' }+instance ('Dict3' c (f4 'T4a), 'Dict3' c (f4 'T4b)) => 'Dict4' c (f4 :: T4 -> k3 -> k2 -> k1 -> k0) where+  'dict4' = \x -> case x of { ST4a -> 'dict3'; ST4b -> 'dict3' }+@++That is, assuming the following @T1@, @T2@, @T3@ and @T4@:++@+data T4 = T4a | T4b+data T3 = T3a | T3b+data T2 = T2a | T2b+data T1 = T1a | T1b+@++Effectively, we wrote just one instance per singleton type per type-index+position, each of them promoting a term-level representation of a singleton+type to its type-level representation and forwarding the rest of the work to+a “smaller” dict. That is, 'dict4' reifies the type of the fourth-to-last+type-index of @X@ and then calls 'dict3' to do the same for the third-to-last+type-index of @X@ and so on. Notice, however, how we didn't need to mention @X@+in none of the instances above: As we said before, these instances are+intended to work for any choice of @c@, @f4@, @f3@, @f2@ and @f1@.++-}++{- $recovering++If you have a @'Some1' (f :: k -> *)@ and you know, statically, that you need an+specific @f (a :: k)@, then you can use 'fromSome1' which will give you an+@f (a :: k)@ only if @a@ was the type that was existentialized by 'Some1'.+Using 'fromSome1' requires that the singleton type-index implements+'Data.Singletons.Decide.SDecide', which can be derived mechanically with+`TemplateHaskell` by means of 'Data.Singletons.TH.singInstance'.++If you don't know, statically, the type of @f (a :: k)@, then you can use+'withSome1Sing' or 'withSome1' to work with @f (a :: k)@ as long as @a@ never+leaves their scope (don't worry, the compiler will yell at you if you try to do+that).++-}+++{- $prodsums++Consider the following types and constructors:++@+data X (a :: 'Bool') where+  XT :: X ''True'+  XF :: X ''False'++data Y (a :: 'Bool') where+  YT :: Y ''True'+  YF :: Y ''False'+@++You can use '(,)' to create a product for values of this type, and 'Either' to+create a sum. However, see what happens if we try to existentialize the type+index when using that approach:++@+> :t ('some1' XT, 'some1' YT)+('some1' XT, 'some1' YT) :: ('Some1' X, 'Some1' Y)+> :t ('some1' XT, 'some1' YF)+('some1' XT, 'some1' YF) :: ('Some1' X, 'Some1' Y)+@++It works, but there is no type level guarantee that the type index taken by @X@+and @Y@ is the same. If you do want to enforce that restriction, then you can+use @P1@ instead:++@+> :t 'P1'+'P1' :: l a -> r a -> 'P1' l r (a :: k)+> :t 'P1' XT YT+'P1' XT YT :: 'P1' X Y ''True'+> :t 'P1' XT YT+'P1' XT YT :: 'P1' X Y ''True'+> :t 'some1' ('P1' XT YT)+'some1' ('P1' XT YT) :: 'Some1' ('P1' X Y)+@++Trying to mix @XT@ with @YF@ fails, of course, since they have different type+indexes:++@+> :t 'P1' XT YF+\<interactive\>:1:7: error:+    • Couldn't match type ‘''False'’ with ‘''True'’+      Expected type: Y ''True'+        Actual type: Y ''False'+    • In the second argument of ‘'P1'’, namely ‘YF’+      In the expression: 'P1' XT YF+@++Moreover, 'P1' supports many common instances from @base@, @hashable@,+@deepseq@, @aeson@, @bytes@, @cereal@, @binary@ and @quickcheck@ out of the+box, so you can benefit from them as well.++There's also 'P2', 'P3' and 'P4' for product types taking a different number of+indexes, and also 'S1', 'S2', 'S3' and 'S4' for sum types:++@+> :t 'S1L'+'S1L' :: l a -> 'S1' l r (a :: k)+> :t 'S1R'+'S1R' :: r a -> 'S1' l r (a :: k)+> :t 'S1L' XT+'S1L' XT :: 'S1' X r ''True'+> :t 'S1R' YT+'S1R' YT :: 'S1' l Y ''True'+> :t 'some1' ('S1L' XT)+'some1' ('S1L' XT) :: 'Some1' ('S1' X r)+> :t 'some1' ('S1R' YT)+'some1' ('S1R' YT) :: 'Some1' ('S1' l Y)+@++-}+++{- $writingInstances++Instances for 'Some1' seem to come out of thin air, but the truth is that they+need to be written at least once by library authors so that, provided all its+requirements are satisfied, they are made available.++For example, when we imported "Exinst" before, we also brought to scope, among+other things, the 'Eq' instance for 'Some1', which is defined as this:++@+instance forall (f :: k1 -> *).+  ( 'Data.Singletons.Decide.SDecide' k1+  , 'Dict1' 'Eq' f+  ) => 'Eq' ('Some1' f)+  where+  (==) = \\som1x som1y ->+     'withSome1Sing' som1x $ \\sa1x (x :: f a1x) ->+        'withSome1Sing' som1y $ \\sa1y (y :: f a1y) ->+           'maybe' 'False' 'id' $ do+              'Data.Type.Equality.Refl' <- 'Data.Type.Equality.testEquality' sa1x sa1y+              case 'dict1' sa1x :: 'Dict' ('Eq' (f a1x)) of+                 'Dict' -> 'Just' (x == y)+@++This code should be relatively straightforward if you are familiar with uses of+the @singletons@ and @constraints@ libraries. We are simply reifying singleton+types from their term-level representation to their type-level representation,+and afterwards using the 'Dict1' mechanism to lookup the required instances+during runtime. Additionaly, this instance requires that the term level+representation of the singleton type implements 'Show' too, as, like we saw in a+previous example, the type index itself is shown in this 'Show' implementation,+in the hope that it can be later recovered and reified to the type level when+using 'Read'.++-}
+ lib/Exinst/Instances/Aeson.hs view
@@ -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 (f :: k1 -> *)+  . ( SingKind k1+    , Ae.ToJSON (Demote k1)+    , Dict1 Ae.ToJSON f+    ) => Ae.ToJSON (Some1 f)+  where+    {-# INLINABLE toJSON #-}+    toJSON = \some1x -> withSome1Sing some1x $ \sa1 (x :: f a1) ->+       case dict1 sa1 :: Dict (Ae.ToJSON (f a1)) of+          Dict -> Ae.toJSON (fromSing sa1, x)++instance forall (f :: k2 -> k1 -> *)+  . ( SingKind k2+    , SingKind k1+    , Ae.ToJSON (Demote k2)+    , Ae.ToJSON (Demote k1)+    , Dict2 Ae.ToJSON f+    ) => Ae.ToJSON (Some2 f)+  where+    {-# INLINABLE toJSON #-}+    toJSON = \some2x -> withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) ->+       case dict2 sa2 sa1 :: Dict (Ae.ToJSON (f a2 a1)) of+          Dict -> Ae.toJSON ((fromSing sa2, fromSing sa1), x)++instance forall (f :: k3 -> k2 -> k1 -> *)+  . ( SingKind k3+    , SingKind k2+    , SingKind k1+    , Ae.ToJSON (Demote k3)+    , Ae.ToJSON (Demote k2)+    , Ae.ToJSON (Demote k1)+    , Dict3 Ae.ToJSON f+    ) => Ae.ToJSON (Some3 f)+  where+    {-# INLINABLE toJSON #-}+    toJSON = \some3x -> withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) ->+       case dict3 sa3 sa2 sa1 :: Dict (Ae.ToJSON (f a3 a2 a1)) of+          Dict -> Ae.toJSON ((fromSing sa3, fromSing sa2, fromSing sa1), x)++instance forall (f :: k4 -> k3 -> k2 -> k1 -> *)+  . ( SingKind k4+    , SingKind k3+    , SingKind k2+    , SingKind k1+    , Ae.ToJSON (Demote k4)+    , Ae.ToJSON (Demote k3)+    , Ae.ToJSON (Demote k2)+    , Ae.ToJSON (Demote k1)+    , Dict4 Ae.ToJSON f+    ) => Ae.ToJSON (Some4 f)+  where+    {-# INLINABLE toJSON #-}+    toJSON = \some4x -> withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) ->+       case dict4 sa4 sa3 sa2 sa1 :: Dict (Ae.ToJSON (f a4 a3 a2 a1)) of+          Dict -> Ae.toJSON ((fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1), x)++--------------------------------------------------------------------------------++instance forall (f :: k1 -> *)+  . ( SingKind k1+    , Ae.FromJSON (Demote k1)+    , Dict1 Ae.FromJSON f+    ) => Ae.FromJSON (Some1 f)+  where+    {-# INLINABLE parseJSON #-}+    parseJSON = \v -> do+      (rsa1, v') <- Ae.parseJSON v+      withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->+         case dict1 sa1 :: Dict (Ae.FromJSON (f a1)) of+            Dict -> do+               x :: f a1 <- Ae.parseJSON v'+               pure (Some1 sa1 x)++instance forall (f :: k2 -> k1 -> *)+  . ( SingKind k2+    , SingKind k1+    , Ae.FromJSON (Demote k2)+    , Ae.FromJSON (Demote k1)+    , Dict2 Ae.FromJSON f+    ) => Ae.FromJSON (Some2 f)+  where+    {-# INLINABLE parseJSON #-}+    parseJSON = \v -> do+      ((rsa2, rsa1), v') <- Ae.parseJSON v+      withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->+         withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->+            case dict2 sa2 sa1 :: Dict (Ae.FromJSON (f a2 a1)) of+               Dict -> do+                  x :: f a2 a1 <- Ae.parseJSON v'+                  pure (Some2 sa2 sa1 x)++instance forall (f :: k3 -> k2 -> k1 -> *)+  . ( SingKind k3+    , SingKind k2+    , SingKind k1+    , Ae.FromJSON (Demote k3)+    , Ae.FromJSON (Demote k2)+    , Ae.FromJSON (Demote k1)+    , Dict3 Ae.FromJSON f+    ) => Ae.FromJSON (Some3 f)+  where+    {-# INLINABLE parseJSON #-}+    parseJSON = \v -> do+      ((rsa3, rsa2, rsa1), v') <- Ae.parseJSON v+      withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) ->+         withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->+            withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->+               case dict3 sa3 sa2 sa1 :: Dict (Ae.FromJSON (f a3 a2 a1)) of+                  Dict -> do+                     x :: f a3 a2 a1 <- Ae.parseJSON v'+                     pure (Some3 sa3 sa2 sa1 x)++instance forall (f :: k4 -> k3 -> k2 -> k1 -> *)+  . ( SingKind k4+    , SingKind k3+    , SingKind k2+    , SingKind k1+    , Ae.FromJSON (Demote k4)+    , Ae.FromJSON (Demote k3)+    , Ae.FromJSON (Demote k2)+    , Ae.FromJSON (Demote k1)+    , Dict4 Ae.FromJSON f+    ) => Ae.FromJSON (Some4 f)+  where+    {-# INLINABLE parseJSON #-}+    parseJSON = \v -> do+      ((rsa4, rsa3, rsa2, rsa1), v') <- Ae.parseJSON v+      withSomeSing rsa4 $ \(sa4 :: Sing (a4 :: k4)) ->+         withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) ->+            withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->+               withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->+                  case dict4 sa4 sa3 sa2 sa1 :: Dict (Ae.FromJSON (f a4 a3 a2 a1)) of+                     Dict -> do+                        x :: f a4 a3 a2 a1 <- Ae.parseJSON v'+                        pure (Some4 sa4 sa3 sa2 sa1 x)
+ lib/Exinst/Instances/Base.hs view
@@ -0,0 +1,622 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# 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", 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.Base () where++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 qualified GHC.Generics as G+import Prelude+import qualified Text.Read as Read++import Exinst.Internal+  hiding (Some1(..), Some2(..), Some3(..), Some4(..))+import qualified Exinst.Internal as Exinst++--------------------------------------------------------------------------------+-- Show++-- Internal wrappers used to avoid writing the string manipulation in 'Show'.+data Some1'Show r1 x = Some1 r1 x deriving (Show)+data Some2'Show r2 r1 x = Some2 r2 r1 x deriving (Show)+data Some3'Show r3 r2 r1 x = Some3 r3 r2 r1 x deriving (Show)+data Some4'Show r4 r3 r2 r1 x = Some4 r4 r3 r2 r1 x deriving (Show)++instance forall (f :: k1 -> Type)+  . ( SingKind k1+    , Show (Demote k1)+    , Dict1 Show f+    ) => Show (Exinst.Some1 f)+  where+    {-# INLINABLE showsPrec #-}+    showsPrec n = \some1x -> withSome1Sing some1x $ \sa1 (x :: f a1) ->+       case dict1 sa1 :: Dict (Show (f a1)) of+          Dict -> showsPrec n (Some1 (fromSing sa1) x)++instance forall (f :: k2 -> k1 -> Type)+  . ( SingKind k2+    , SingKind k1+    , Show (Demote k2)+    , Show (Demote k1)+    , Dict2 Show f+    ) => Show (Exinst.Some2 f)+  where+    {-# INLINABLE showsPrec #-}+    showsPrec n = \some2x -> withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) ->+       case dict2 sa2 sa1 :: Dict (Show (f a2 a1)) of+          Dict -> showsPrec n (Some2 (fromSing sa2) (fromSing sa1) x)++instance forall (f :: k3 -> k2 -> k1 -> Type)+  . ( SingKind k3+    , SingKind k2+    , SingKind k1+    , Show (Demote k3)+    , Show (Demote k2)+    , Show (Demote k1)+    , Dict3 Show f+    ) => Show (Exinst.Some3 f)+  where+    {-# INLINABLE showsPrec #-}+    showsPrec n = \some3x -> withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) ->+       case dict3 sa3 sa2 sa1 :: Dict (Show (f a3 a2 a1)) of+          Dict -> showsPrec n (Some3 (fromSing sa3) (fromSing sa2) (fromSing sa1) x)++instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type)+  . ( SingKind k4+    , SingKind k3+    , SingKind k2+    , SingKind k1+    , Show (Demote k4)+    , Show (Demote k3)+    , Show (Demote k2)+    , Show (Demote k1)+    , Dict4 Show f+    ) => Show (Exinst.Some4 f)+  where+    {-# INLINABLE showsPrec #-}+    showsPrec n = \some4x -> withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) ->+       case dict4 sa4 sa3 sa2 sa1 :: Dict (Show (f a4 a3 a2 a1)) of+          Dict -> showsPrec n (Some4 (fromSing sa4) (fromSing sa3)+                                     (fromSing sa2) (fromSing sa1) x)++--------------------------------------------------------------------------------+-- Read++instance forall (f :: k1 -> Type)+  . ( SingKind k1+    , Read (Demote k1)+    , Dict1 Read f+    ) => Read (Exinst.Some1 f)+  where+    {-# INLINABLE readPrec #-}+    readPrec = do+      Read.Ident "Some1" <- Read.lexP+      rsa1 <- Read.readPrec+      withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->+         case dict1 sa1 :: Dict (Read (f a1)) of+            Dict -> do+               x :: f a1 <- Read.readPrec+               pure (Exinst.Some1 sa1 x)++instance forall (f :: k2 -> k1 -> Type)+  . ( SingKind k2+    , SingKind k1+    , Read (Demote k2)+    , Read (Demote k1)+    , Dict2 Read f+    ) => Read (Exinst.Some2 f)+  where+    {-# INLINABLE readPrec #-}+    readPrec = do+      Read.Ident "Some2" <- Read.lexP+      rsa2 <- Read.readPrec+      rsa1 <- Read.readPrec+      withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->+         withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->+            case dict2 sa2 sa1 :: Dict (Read (f a2 a1)) of+               Dict -> do+                  x :: f a2 a1 <- Read.readPrec+                  pure (Exinst.Some2 sa2 sa1 x)++instance forall (f :: k3 -> k2 -> k1 -> Type)+  . ( SingKind k3+    , SingKind k2+    , SingKind k1+    , Read (Demote k3)+    , Read (Demote k2)+    , Read (Demote k1)+    , Dict3 Read f+    ) => Read (Exinst.Some3 f)+  where+    {-# INLINABLE readPrec #-}+    readPrec = do+      Read.Ident "Some3" <- Read.lexP+      rsa3 <- Read.readPrec+      rsa2 <- Read.readPrec+      rsa1 <- Read.readPrec+      withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) ->+         withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->+            withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->+               case dict3 sa3 sa2 sa1 :: Dict (Read (f a3 a2 a1)) of+                  Dict -> do+                     x :: f a3 a2 a1 <- Read.readPrec+                     pure (Exinst.Some3 sa3 sa2 sa1 x)++instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type)+  . ( SingKind k4+    , SingKind k3+    , SingKind k2+    , SingKind k1+    , Read (Demote k4)+    , Read (Demote k3)+    , Read (Demote k2)+    , Read (Demote k1)+    , Dict4 Read f+    ) => Read (Exinst.Some4 f)+  where+    {-# INLINABLE readPrec #-}+    readPrec = do+      Read.Ident "Some4" <- Read.lexP+      rsa4 <- Read.readPrec+      rsa3 <- Read.readPrec+      rsa2 <- Read.readPrec+      rsa1 <- Read.readPrec+      withSomeSing rsa4 $ \(sa4 :: Sing (a4 :: k4)) ->+         withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) ->+            withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->+               withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->+                  case dict4 sa4 sa3 sa2 sa1 :: Dict (Read (f a4 a3 a2 a1)) of+                     Dict -> do+                        x :: f a4 a3 a2 a1 <- Read.readPrec+                        pure (Exinst.Some4 sa4 sa3 sa2 sa1 x)++--------------------------------------------------------------------------------+-- Eq++instance forall (f :: k1 -> Type).+  ( SDecide k1+  , Dict1 Eq f+  ) => Eq (Exinst.Some1 f)+  where+  {-# INLINABLE (==) #-}+  (==) = \som1x som1y ->+     withSome1Sing som1x $ \sa1x (x :: f a1x) ->+        withSome1Sing som1y $ \sa1y (y :: f a1y) ->+           maybe False id $ do+              Refl <- testEquality sa1x sa1y+              case dict1 sa1x :: Dict (Eq (f a1x)) of+                 Dict -> Just (x == y)++instance forall (f :: k2 -> k1 -> Type)+  . ( SDecide k2+    , SDecide k1+    , Dict2 Eq f+    ) => Eq (Exinst.Some2 f)+  where+    {-# INLINABLE (==) #-}+    (==) = \som2x som2y ->+       withSome2Sing som2x $ \sa2x sa1x (x :: f a2x a1x) ->+          withSome2Sing som2y $ \sa2y sa1y (y :: f a2y a1y) ->+             maybe False id $ do+                Refl <- testEquality sa2x sa2y+                Refl <- testEquality sa1x sa1y+                case dict2 sa2x sa1x :: Dict (Eq (f a2x a1x)) of+                   Dict -> Just (x == y)++instance forall (f :: k3 -> k2 -> k1 -> Type)+  . ( SDecide k3+    , SDecide k2+    , SDecide k1+    , Dict3 Eq f+    ) => Eq (Exinst.Some3 f)+  where+    {-# INLINABLE (==) #-}+    (==) = \som3x som3y ->+       withSome3Sing som3x $ \sa3x sa2x sa1x (x :: f a3x a2x a1x) ->+          withSome3Sing som3y $ \sa3y sa2y sa1y (y :: f a3y a2y a1y) ->+             maybe False id $ do+                Refl <- testEquality sa3x sa3y+                Refl <- testEquality sa2x sa2y+                Refl <- testEquality sa1x sa1y+                case dict3 sa3x sa2x sa1x :: Dict (Eq (f a3x a2x a1x)) of+                   Dict -> Just (x == y)++instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type)+  . ( SDecide k4+    , SDecide k3+    , SDecide k2+    , SDecide k1+    , Dict4 Eq f+    ) => Eq (Exinst.Some4 f)+  where+    {-# INLINABLE (==) #-}+    (==) = \som4x som4y ->+       withSome4Sing som4x $ \sa4x sa3x sa2x sa1x (x :: f a4x a3x a2x a1x) ->+          withSome4Sing som4y $ \sa4y sa3y sa2y sa1y (y :: f a4y a3y a2y a1y) ->+             maybe False id $ do+                Refl <- testEquality sa4x sa4y+                Refl <- testEquality sa3x sa3y+                Refl <- testEquality sa2x sa2y+                Refl <- testEquality sa1x sa1y+                case dict4 sa4x sa3x sa2x sa1x :: Dict (Eq (f a4x a3x a2x a1x)) of+                   Dict -> Just (x == y)++--------------------------------------------------------------------------------+-- Ord++instance forall (f :: k1 -> Type)+  . ( SingKind k1+    , SDecide k1+    , Ord (Demote k1)+    , Dict1 Ord f+    , Eq (Exinst.Some1 f)+    ) => Ord (Exinst.Some1 f)+  where+    {-# INLINABLE compare #-}+    compare = \som1x som1y ->+       withSome1Sing som1x $ \sa1x (x :: f a1x) ->+          withSome1Sing som1y $ \sa1y (y :: f a1y) ->+             let termCompare = compare (fromSing sa1x) (fromSing sa1y)+             in maybe termCompare id $ do+                  Refl <- testEquality sa1x sa1y+                  case dict1 sa1x :: Dict (Ord (f a1x)) of+                     Dict -> Just (compare x y)++instance forall (f :: k2 -> k1 -> Type)+  . ( SingKind k2+    , SingKind k1+    , SDecide k2+    , SDecide k1+    , Ord (Demote k2)+    , Ord (Demote k1)+    , Dict2 Ord f+    , Eq (Exinst.Some2 f)+    ) => Ord (Exinst.Some2 f)+  where+    {-# INLINABLE compare #-}+    compare = \som2x som2y ->+       withSome2Sing som2x $ \sa2x sa1x (x :: f a2x a1x) ->+          withSome2Sing som2y $ \sa2y sa1y (y :: f a2y a1y) ->+             let termCompare = compare (fromSing sa2x, fromSing sa1x)+                                       (fromSing sa2y, fromSing sa1y)+             in maybe termCompare id $ do+                   Refl <- testEquality sa2x sa2y+                   Refl <- testEquality sa1x sa1y+                   case dict2 sa2x sa1x :: Dict (Ord (f a2x a1x)) of+                      Dict -> Just (compare x y)++instance forall (f :: k3 -> k2 -> k1 -> Type)+  . ( SingKind k3+    , SingKind k2+    , SingKind k1+    , SDecide k3+    , SDecide k2+    , SDecide k1+    , Ord (Demote k3)+    , Ord (Demote k2)+    , Ord (Demote k1)+    , Dict3 Ord f+    , Eq (Exinst.Some3 f)+    ) => Ord (Exinst.Some3 f)+  where+    {-# INLINABLE compare #-}+    compare = \som3x som3y ->+       withSome3Sing som3x $ \sa3x sa2x sa1x (x :: f a3x a2x a1x) ->+          withSome3Sing som3y $ \sa3y sa2y sa1y (y :: f a3y a2y a1y) ->+             let termCompare = compare+                   (fromSing sa3x, fromSing sa2x, fromSing sa1x)+                   (fromSing sa3y, fromSing sa2y, fromSing sa1y)+             in maybe termCompare id $ do+                  Refl <- testEquality sa3x sa3y+                  Refl <- testEquality sa2x sa2y+                  Refl <- testEquality sa1x sa1y+                  case dict3 sa3x sa2x sa1x :: Dict (Ord (f a3x a2x a1x)) of+                     Dict -> Just (compare x y)++instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type)+  . ( SingKind k4+    , SingKind k3+    , SingKind k2+    , SingKind k1+    , SDecide k4+    , SDecide k3+    , SDecide k2+    , SDecide k1+    , Ord (Demote k4)+    , Ord (Demote k3)+    , Ord (Demote k2)+    , Ord (Demote k1)+    , Dict4 Ord f+    , Eq (Exinst.Some4 f)+    ) => Ord (Exinst.Some4 f)+  where+    {-# INLINABLE compare #-}+    compare = \som4x som4y ->+       withSome4Sing som4x $ \sa4x sa3x sa2x sa1x (x :: f a4x a3x a2x a1x) ->+          withSome4Sing som4y $ \sa4y sa3y sa2y sa1y (y :: f a4y a3y a2y a1y) ->+             let termCompare = compare+                   (fromSing sa4x, fromSing sa3x, fromSing sa2x, fromSing sa1x)+                   (fromSing sa4y, fromSing sa3y, fromSing sa2y, fromSing sa1y)+             in maybe termCompare id $ do+                  Refl <- testEquality sa4x sa4y+                  Refl <- testEquality sa3x sa3y+                  Refl <- testEquality sa2x sa2y+                  Refl <- testEquality sa1x sa1y+                  case dict4 sa4x sa3x sa2x sa1x :: Dict (Ord (f a4x a3x a2x a1x)) of+                     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 (Demote k1)+    , PBounded (Demote k1)+    , G.Generic (Demote 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 (Demote 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 (Demote k2)+    , PEnum (Demote k1)+    , PBounded (Demote k2)+    , PBounded (Demote k1)+    , G.Generic (Demote k2)+    , G.Generic (Demote 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 ((Demote k2, Demote 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 (Demote k3)+    , PEnum (Demote k2)+    , PEnum (Demote k1)+    , PBounded (Demote k3)+    , PBounded (Demote k2)+    , PBounded (Demote k1)+    , G.Generic (Demote k3)+    , G.Generic (Demote k2)+    , G.Generic (Demote 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 ((Demote k3, Demote k2, Demote 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 (Demote k4)+    , PEnum (Demote k3)+    , PEnum (Demote k2)+    , PEnum (Demote k1)+    , PBounded (Demote k4)+    , PBounded (Demote k3)+    , PBounded (Demote k2)+    , PBounded (Demote k1)+    , G.Generic (Demote k4)+    , G.Generic (Demote k3)+    , G.Generic (Demote k2)+    , G.Generic (Demote 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 ((Demote k4, Demote k3, Demote k2, Demote 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 'DictX' instances for some @base@ types++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+
+ lib/Exinst/Instances/Binary.hs view
@@ -0,0 +1,137 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE UndecidableInstances #-}++{-# OPTIONS_GHC -fno-warn-orphans #-}++-- | This module exports 'Bin.Binary' 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.Binary () where++import qualified Data.Binary as Bin+import Data.Constraint+import Data.Singletons+import Prelude++import Exinst.Internal++--------------------------------------------------------------------------------++-- | Compatible with the 'Data.Bytes.Serial.Serial' instance and+-- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the+-- fully applied @f@ instances are compatible as well.+instance forall (f :: k1 -> *).+  ( SingKind k1+  , Bin.Binary (Demote k1)+  , Dict1 Bin.Binary f+  ) => Bin.Binary (Some1 f) where+  {-# INLINABLE put #-}+  put = \some1x ->+    withSome1Sing some1x $ \sa1 (x :: f a1) ->+      case dict1 sa1 :: Dict (Bin.Binary (f a1)) of+        Dict -> do+          Bin.put (fromSing sa1)+          Bin.put x+  {-# INLINABLE get #-}+  get = do+    rsa1 <- Bin.get+    withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->+      case dict1 sa1 :: Dict (Bin.Binary (f a1)) of+        Dict -> do+          x :: f a1 <- Bin.get+          pure (Some1 sa1 x)++-- | Compatible with the 'Data.Bytes.Serial.Serial' instance and+-- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the+-- fully applied @f@ instances are compatible as well.+instance forall (f :: k2 -> k1 -> *).+  ( SingKind k2+  , SingKind k1+  , Bin.Binary (Demote k2)+  , Bin.Binary (Demote k1)+  , Dict2 Bin.Binary f+  ) => Bin.Binary (Some2 f) where+  {-# INLINABLE put #-}+  put = \some2x ->+    withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) ->+      case dict2 sa2 sa1 :: Dict (Bin.Binary (f a2 a1)) of+        Dict -> do+          Bin.put (fromSing sa2, fromSing sa1)+          Bin.put x+  {-# INLINABLE get #-}+  get = do+    (rsa2, rsa1) <- Bin.get+    withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->+      withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->+        case dict2 sa2 sa1 :: Dict (Bin.Binary (f a2 a1)) of+          Dict -> do+            x :: f a2 a1 <- Bin.get+            pure (Some2 sa2 sa1 x)++-- | Compatible with the 'Data.Bytes.Serial.Serial' instance and+-- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the+-- fully applied @f@ instances are compatible as well.+instance forall (f :: k3 -> k2 -> k1 -> *).+  ( SingKind k3+  , SingKind k2+  , SingKind k1+  , Bin.Binary (Demote k3)+  , Bin.Binary (Demote k2)+  , Bin.Binary (Demote k1)+  , Dict3 Bin.Binary f+  ) => Bin.Binary (Some3 f) where+  {-# INLINABLE put #-}+  put = \some3x ->+    withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) ->+      case dict3 sa3 sa2 sa1 :: Dict (Bin.Binary (f a3 a2 a1)) of+        Dict -> do+          Bin.put (fromSing sa3, fromSing sa2, fromSing sa1)+          Bin.put x+  {-# INLINABLE get #-}+  get = do+    (rsa3, rsa2, rsa1) <- Bin.get+    withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) ->+      withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->+        withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->+          case dict3 sa3 sa2 sa1 :: Dict (Bin.Binary (f a3 a2 a1)) of+            Dict -> do+              x :: f a3 a2 a1 <- Bin.get+              pure (Some3 sa3 sa2 sa1 x)++-- | Compatible with the 'Data.Bytes.Serial.Serial' instance and+-- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the+-- fully applied @f@ instances are compatible as well.+instance forall (f :: k4 -> k3 -> k2 -> k1 -> *).+  ( SingKind k4+  , SingKind k3+  , SingKind k2+  , SingKind k1+  , Bin.Binary (Demote k4)+  , Bin.Binary (Demote k3)+  , Bin.Binary (Demote k2)+  , Bin.Binary (Demote k1)+  , Dict4 Bin.Binary f+  ) => Bin.Binary (Some4 f) where+  {-# INLINABLE put #-}+  put = \some4x ->+    withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) ->+      case dict4 sa4 sa3 sa2 sa1 :: Dict (Bin.Binary (f a4 a3 a2 a1)) of+        Dict -> do+          Bin.put (fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1)+          Bin.put x+  {-# INLINABLE get #-}+  get = do+    (rsa4, rsa3, rsa2, rsa1) <- Bin.get+    withSomeSing rsa4 $ \(sa4 :: Sing (a4 :: k4)) ->+      withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) ->+        withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->+          withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->+            case dict4 sa4 sa3 sa2 sa1 :: Dict (Bin.Binary (f a4 a3 a2 a1)) of+              Dict -> do+                x :: f a4 a3 a2 a1 <- Bin.get+                pure (Some4 sa4 sa3 sa2 sa1 x)
+ lib/Exinst/Instances/Bytes.hs view
@@ -0,0 +1,138 @@+{-# 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++--------------------------------------------------------------------------------++-- | Compatible with the 'Data.Binary.Binary' instance and+-- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the+-- fully applied @f@ instances are compatible as well.+instance forall (f :: k1 -> *).+  ( SingKind k1+  , By.Serial (Demote k1)+  , Dict1 By.Serial f+  ) => By.Serial (Some1 f) where+  {-# INLINABLE serialize #-}+  serialize = \some1x ->+    withSome1Sing some1x $ \sa1 (x :: f a1) ->+      case dict1 sa1 :: Dict (By.Serial (f a1)) of+        Dict -> do+          By.serialize (fromSing sa1)+          By.serialize x+  {-# INLINABLE deserialize #-}+  deserialize = do+    rsa1 <- By.deserialize+    withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->+      case dict1 sa1 :: Dict (By.Serial (f a1)) of+        Dict -> do+          x :: f a1 <- By.deserialize+          pure (Some1 sa1 x)++-- | Compatible with the 'Data.Binary.Binary' instance and+-- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the+-- fully applied @f@ instances are compatible as well.+instance forall (f :: k2 -> k1 -> *).+  ( SingKind k2+  , SingKind k1+  , By.Serial (Demote k2)+  , By.Serial (Demote k1)+  , Dict2 By.Serial f+  ) => By.Serial (Some2 f) where+  {-# INLINABLE serialize #-}+  serialize = \some2x ->+    withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) ->+      case dict2 sa2 sa1 :: Dict (By.Serial (f 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)) ->+      withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->+        case dict2 sa2 sa1 :: Dict (By.Serial (f a2 a1)) of+          Dict -> do+            x :: f a2 a1 <- By.deserialize+            pure (Some2 sa2 sa1 x)++-- | Compatible with the 'Data.Binary.Binary' instance and+-- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the+-- fully applied @f@ instances are compatible as well.+instance forall (f :: k3 -> k2 -> k1 -> *).+  ( SingKind k3+  , SingKind k2+  , SingKind k1+  , By.Serial (Demote k3)+  , By.Serial (Demote k2)+  , By.Serial (Demote k1)+  , Dict3 By.Serial f+  ) => By.Serial (Some3 f) where+  {-# INLINABLE serialize #-}+  serialize = \some3x ->+    withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) ->+      case dict3 sa3 sa2 sa1 :: Dict (By.Serial (f 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)) ->+      withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->+        withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->+           case dict3 sa3 sa2 sa1 :: Dict (By.Serial (f a3 a2 a1)) of+             Dict -> do+               x :: f a3 a2 a1 <- By.deserialize+               pure (Some3 sa3 sa2 sa1 x)++-- | Compatible with the 'Data.Binary.Binary' instance and+-- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the+-- fully applied @f@ instances are compatible as well.+instance forall (f :: k4 -> k3 -> k2 -> k1 -> *).+  ( SingKind k4+  , SingKind k3+  , SingKind k2+  , SingKind k1+  , By.Serial (Demote k4)+  , By.Serial (Demote k3)+  , By.Serial (Demote k2)+  , By.Serial (Demote k1)+  , Dict4 By.Serial f+  ) => By.Serial (Some4 f) where+  {-# INLINABLE serialize #-}+  serialize = \some4x ->+    withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) ->+      case dict4 sa4 sa3 sa2 sa1 :: Dict (By.Serial (f 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)) ->+      withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) ->+        withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->+          withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->+            case dict4 sa4 sa3 sa2 sa1 :: Dict (By.Serial (f a4 a3 a2 a1)) of+              Dict -> do+                x :: f a4 a3 a2 a1 <- By.deserialize+                pure (Some4 sa4 sa3 sa2 sa1 x)
+ lib/Exinst/Instances/Cereal.hs view
@@ -0,0 +1,138 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE UndecidableInstances #-}++{-# OPTIONS_GHC -fno-warn-orphans #-}++-- | This module exports 'Cer.Serialize' 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.Cereal () where++import qualified Data.Serialize as Cer+import Data.Constraint+import Data.Singletons+import Prelude++import Exinst.Internal++--------------------------------------------------------------------------------++-- | Compatible with the 'Data.Bytes.Serial.Serial' instance and+-- 'Data.Binary.Binary' instance, provided all of the 'Demote's and the fully+-- applied @f@ instances are compatible as well.+instance forall (f :: k1 -> *).+  ( SingKind k1+  , Cer.Serialize (Demote k1)+  , Dict1 Cer.Serialize f+  ) => Cer.Serialize (Some1 f) where+  {-# INLINABLE put #-}+  put = \some1x ->+    withSome1Sing some1x $ \sa1 (x :: f a1) ->+      case dict1 sa1 :: Dict (Cer.Serialize (f a1)) of+        Dict -> do+          Cer.put (fromSing sa1)+          Cer.put x+  {-# INLINABLE get #-}+  get = do+    rsa1 <- Cer.get+    withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->+      case dict1 sa1 :: Dict (Cer.Serialize (f a1)) of+        Dict -> do+          x :: f a1 <- Cer.get+          pure (Some1 sa1 x)++-- | Compatible with the 'Data.Bytes.Serial.Serial' instance and+-- 'Data.Binary.Binary' instance, provided all of the 'Demote's and the fully+-- applied @f@ instances are compatible as well.+instance forall (f :: k2 -> k1 -> *).+  ( SingKind k2+  , SingKind k1+  , Cer.Serialize (Demote k2)+  , Cer.Serialize (Demote k1)+  , Dict2 Cer.Serialize f+  ) => Cer.Serialize (Some2 f) where+  {-# INLINABLE put #-}+  put = \some2x ->+    withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) ->+      case dict2 sa2 sa1 :: Dict (Cer.Serialize (f a2 a1)) of+        Dict -> do+          Cer.put (fromSing sa2, fromSing sa1)+          Cer.put x+  {-# INLINABLE get #-}+  get = do+    (rsa2, rsa1) <- Cer.get+    withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->+      withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->+        case dict2 sa2 sa1 :: Dict (Cer.Serialize (f a2 a1)) of+          Dict -> do+            x :: f a2 a1 <- Cer.get+            pure (Some2 sa2 sa1 x)++-- | Compatible with the 'Data.Bytes.Serial.Serial' instance and+-- 'Data.Binary.Binary' instance, provided all of the 'Demote's and the fully+-- applied @f@ instances are compatible as well.+instance forall (f :: k3 -> k2 -> k1 -> *).+  ( SingKind k3+  , SingKind k2+  , SingKind k1+  , Cer.Serialize (Demote k3)+  , Cer.Serialize (Demote k2)+  , Cer.Serialize (Demote k1)+  , Dict3 Cer.Serialize f+  ) => Cer.Serialize (Some3 f) where+  {-# INLINABLE put #-}+  put = \some3x ->+    withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) ->+      case dict3 sa3 sa2 sa1 :: Dict (Cer.Serialize (f a3 a2 a1)) of+        Dict -> do+          Cer.put (fromSing sa3, fromSing sa2, fromSing sa1)+          Cer.put x+  {-# INLINABLE get #-}+  get = do+    (rsa3, rsa2, rsa1) <- Cer.get+    withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) ->+      withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->+        withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->+          case dict3 sa3 sa2 sa1 :: Dict (Cer.Serialize (f a3 a2 a1)) of+            Dict -> do+              x :: f a3 a2 a1 <- Cer.get+              pure (Some3 sa3 sa2 sa1 x)++-- | Compatible with the 'Data.Bytes.Serial.Serial' instance and+-- 'Data.Binary.Binary' instance, provided all of the 'Demote's and the fully+-- applied @f@ instances are compatible as well.+instance forall (f :: k4 -> k3 -> k2 -> k1 -> *).+  ( SingKind k4+  , SingKind k3+  , SingKind k2+  , SingKind k1+  , Cer.Serialize (Demote k4)+  , Cer.Serialize (Demote k3)+  , Cer.Serialize (Demote k2)+  , Cer.Serialize (Demote k1)+  , Dict4 Cer.Serialize f+  ) => Cer.Serialize (Some4 f) where+  {-# INLINABLE put #-}+  put = \some4x ->+    withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) ->+      case dict4 sa4 sa3 sa2 sa1 :: Dict (Cer.Serialize (f a4 a3 a2 a1)) of+        Dict -> do+          Cer.put (fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1)+          Cer.put x+  {-# INLINABLE get #-}+  get = do+    (rsa4, rsa3, rsa2, rsa1) <- Cer.get+    withSomeSing rsa4 $ \(sa4 :: Sing (a4 :: k4)) ->+      withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) ->+        withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->+          withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->+            case dict4 sa4 sa3 sa2 sa1 :: Dict (Cer.Serialize (f a4 a3 a2 a1)) of+              Dict -> do+                x :: f a4 a3 a2 a1 <- Cer.get+                pure (Some4 sa4 sa3 sa2 sa1 x)+
+ lib/Exinst/Instances/DeepSeq.hs view
@@ -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 (f :: k1 -> *).+  ( Dict1 NFData f+  ) => NFData (Some1 f) where+  {-# INLINABLE rnf #-}+  rnf = \(!some1x) ->+    withSome1Sing some1x $ \ !sa1 !(x :: f a1) ->+       case dict1 sa1 :: Dict (NFData (f a1)) of+          Dict -> rnf x `seq` ()++instance forall (f :: k2 -> k1 -> *).+  ( Dict2 NFData f+  ) => NFData (Some2 f) where+  {-# INLINABLE rnf #-}+  rnf = \(!some2x) ->+    withSome2Sing some2x $ \ !sa2 !sa1 !(x :: f a2 a1) ->+       case dict2 sa2 sa1 :: Dict (NFData (f a2 a1)) of+          Dict -> rnf x `seq` ()++instance forall (f :: k3 -> k2 -> k1 -> *).+  ( Dict3 NFData f+  ) => NFData (Some3 f) where+  {-# INLINABLE rnf #-}+  rnf = \(!some3x) ->+    withSome3Sing some3x $ \ !sa3 !sa2 !sa1 !(x :: f a3 a2 a1) ->+       case dict3 sa3 sa2 sa1 :: Dict (NFData (f a3 a2 a1)) of+          Dict -> rnf x `seq` ()++instance forall (f :: k4 -> k3 -> k2 -> k1 -> *).+  ( Dict4 NFData f+  ) => NFData (Some4 f) where+  {-# INLINABLE rnf #-}+  rnf = \(!some4x) ->+    withSome4Sing some4x $ \ !(sa4) !sa3 !sa2 !sa1 !(x :: f a4 a3 a2 a1) ->+       case dict4 sa4 sa3 sa2 sa1 :: Dict (NFData (f a4 a3 a2 a1)) of+          Dict -> rnf x `seq` ()+
+ lib/Exinst/Instances/Hashable.hs view
@@ -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 (f :: k1 -> *)+  . ( SingKind k1+    , Hashable (Demote k1)+    , Dict1 Hashable f+    ) => Hashable (Some1 f)+  where+    {-# INLINABLE hashWithSalt #-}+    hashWithSalt salt some1x = withSome1Sing some1x $ \sa1 (x :: f a1) ->+       case dict1 sa1 :: Dict (Hashable (f a1)) of+          Dict -> salt `hashWithSalt` salt0+                       `hashWithSalt` fromSing sa1+                       `hashWithSalt` x++instance forall (f :: k2 -> k1 -> *)+  . ( SingKind k2+    , SingKind k1+    , Hashable (Demote k2)+    , Hashable (Demote k1)+    , Dict2 Hashable f+    ) => Hashable (Some2 f)+  where+    {-# INLINABLE hashWithSalt #-}+    hashWithSalt salt some2x = withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) ->+       case dict2 sa2 sa1 :: Dict (Hashable (f a2 a1)) of+          Dict -> salt `hashWithSalt` salt0+                       `hashWithSalt` fromSing sa2+                       `hashWithSalt` fromSing sa1+                       `hashWithSalt` x++instance forall (f :: k3 -> k2 -> k1 -> *)+  . ( SingKind k3+    , SingKind k2+    , SingKind k1+    , Hashable (Demote k3)+    , Hashable (Demote k2)+    , Hashable (Demote k1)+    , Dict3 Hashable f+    ) => Hashable (Some3 f)+  where+    {-# INLINABLE hashWithSalt #-}+    hashWithSalt salt some3x = withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) ->+       case dict3 sa3 sa2 sa1 :: Dict (Hashable (f a3 a2 a1)) of+          Dict -> salt `hashWithSalt` salt0+                       `hashWithSalt` fromSing sa3+                       `hashWithSalt` fromSing sa2+                       `hashWithSalt` fromSing sa1+                       `hashWithSalt` x++instance forall (f :: k4 -> k3 -> k2 -> k1 -> *)+  . ( SingKind k4+    , SingKind k3+    , SingKind k2+    , SingKind k1+    , Hashable (Demote k4)+    , Hashable (Demote k3)+    , Hashable (Demote k2)+    , Hashable (Demote k1)+    , Dict4 Hashable f+    ) => Hashable (Some4 f)+  where+    {-# INLINABLE hashWithSalt #-}+    hashWithSalt salt some4x = withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) ->+       case dict4 sa4 sa3 sa2 sa1 :: Dict (Hashable (f a4 a3 a2 a1)) of+          Dict -> salt `hashWithSalt` salt0+                       `hashWithSalt` fromSing sa4+                       `hashWithSalt` fromSing sa3+                       `hashWithSalt` fromSing sa2+                       `hashWithSalt` fromSing sa1+                       `hashWithSalt` x
+ lib/Exinst/Instances/QuickCheck.hs view
@@ -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, Demote, withSomeSing)+import qualified Test.QuickCheck as QC++import Exinst.Internal++--------------------------------------------------------------------------------++instance+  forall k1 (f :: k1 -> Type).+  ( SingKind k1+  , QC.Arbitrary (Demote 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 (Demote k2)+  , QC.Arbitrary (Demote 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 (Demote k3)+  , QC.Arbitrary (Demote k2)+  , QC.Arbitrary (Demote 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 (Demote k4)+  , QC.Arbitrary (Demote k3)+  , QC.Arbitrary (Demote k2)+  , QC.Arbitrary (Demote 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+
+ lib/Exinst/Instances/Serialise.hs view
@@ -0,0 +1,125 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE UndecidableInstances #-}++{-# OPTIONS_GHC -fno-warn-orphans #-}++-- | This module exports 'Serialise' instances (which provide+-- binary serialisation via the CBOR format) 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.Serialise () where++import Codec.Serialise+import Codec.Serialise.Decoding (decodeListLenOf)+import Data.Constraint+import Data.Singletons+import Prelude++import Exinst.Internal++--------------------------------------------------------------------------------++instance forall (f :: k1 -> *)+  . ( SingKind k1+    , Serialise (Demote k1)+    , Dict1 Serialise f+    ) => Serialise (Some1 f)+  where+    {-# INLINABLE encode #-}+    encode = \some1x -> withSome1Sing some1x $ \sa1 (x :: f a1) ->+       case dict1 sa1 :: Dict (Serialise (f a1)) of+          Dict -> encode (fromSing sa1, x)+    {-# INLINABLE decode #-}+    decode = do+      decodeListLenOf 2+      rsa1 <- decode+      withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->+         case dict1 sa1 :: Dict (Serialise (f a1)) of+            Dict -> do+               x :: f a1 <- decode+               pure (Some1 sa1 x)++instance forall (f :: k2 -> k1 -> *)+  . ( SingKind k2+    , SingKind k1+    , Serialise (Demote k2)+    , Serialise (Demote k1)+    , Dict2 Serialise f+    ) => Serialise (Some2 f)+  where+    {-# INLINABLE encode #-}+    encode = \some2x -> withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) ->+       case dict2 sa2 sa1 :: Dict (Serialise (f a2 a1)) of+          Dict -> encode (fromSing sa2, fromSing sa1, x)+++    {-# INLINABLE decode #-}+    decode = do+      decodeListLenOf 3+      rsa2 <- decode; rsa1 <- decode+      withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->+         withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->+            case dict2 sa2 sa1 :: Dict (Serialise (f a2 a1)) of+               Dict -> do+                  x :: f a2 a1 <- decode+                  pure (Some2 sa2 sa1 x)++instance forall (f :: k3 -> k2 -> k1 -> *)+  . ( SingKind k3+    , SingKind k2+    , SingKind k1+    , Serialise (Demote k3)+    , Serialise (Demote k2)+    , Serialise (Demote k1)+    , Dict3 Serialise f+    ) => Serialise (Some3 f)+  where+    {-# INLINABLE encode #-}+    encode = \some3x -> withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) ->+       case dict3 sa3 sa2 sa1 :: Dict (Serialise (f a3 a2 a1)) of+          Dict -> encode (fromSing sa3, fromSing sa2, fromSing sa1, x)+    {-# INLINABLE decode #-}+    decode = do+      decodeListLenOf 4+      rsa3 <- decode; rsa2 <- decode; rsa1 <- decode+      withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) ->+         withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->+            withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->+               case dict3 sa3 sa2 sa1 :: Dict (Serialise (f a3 a2 a1)) of+                  Dict -> do+                     x :: f a3 a2 a1 <- decode+                     pure (Some3 sa3 sa2 sa1 x)++instance forall (f :: k4 -> k3 -> k2 -> k1 -> *)+  . ( SingKind k4+    , SingKind k3+    , SingKind k2+    , SingKind k1+    , Serialise (Demote k4)+    , Serialise (Demote k3)+    , Serialise (Demote k2)+    , Serialise (Demote k1)+    , Dict4 Serialise f+    ) => Serialise (Some4 f)+  where+    {-# INLINABLE encode #-}+    encode = \some4x -> withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) ->+       case dict4 sa4 sa3 sa2 sa1 :: Dict (Serialise (f a4 a3 a2 a1)) of+          Dict -> encode (fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1, x)+    {-# INLINABLE decode #-}+    decode = do+      decodeListLenOf 5+      rsa4 <- decode; rsa3 <- decode; rsa2 <- decode; rsa1 <- decode;+      withSomeSing rsa4 $ \(sa4 :: Sing (a4 :: k4)) ->+         withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) ->+            withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->+               withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->+                  case dict4 sa4 sa3 sa2 sa1 :: Dict (Serialise (f a4 a3 a2 a1)) of+                     Dict -> do+                        x :: f a4 a3 a2 a1 <- decode+                        pure (Some4 sa4 sa3 sa2 sa1 x)
+ lib/Exinst/Internal.hs view
@@ -0,0 +1,443 @@+{-# 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+ , same1+ , Dict1(dict1)++   -- * 2 type indexes+ , Some2(Some2)+ , some2+ , fromSome2+ , _Some2+ , withSome2+ , withSome2Sing+ , some2SingRep+ , same2+ , Dict2(dict2)++   -- * 3 type indexes+ , Some3(Some3)+ , some3+ , fromSome3+ , _Some3+ , withSome3+ , withSome3Sing+ , some3SingRep+ , same3+ , Dict3(dict3)++   -- * 4 type indexes+ , Some4(Some4)+ , some4+ , fromSome4+ , _Some4+ , withSome4+ , withSome4Sing+ , some4SingRep+ , same4+ , 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)+  -> Demote k1 -- ^+some1SingRep = \(Some1 sa1 _) -> fromSing sa1+{-# INLINE some1SingRep #-}++some2SingRep+  :: (SingKind k2, SingKind k1)+  => Some2 (f2 :: k2 -> k1 -> Type)+  -> (Demote k2, Demote k1) -- ^+some2SingRep = \(Some2 sa2 sa1 _) -> (fromSing sa2, fromSing sa1)+{-# INLINE some2SingRep #-}++some3SingRep+  :: (SingKind k3, SingKind k2, SingKind k1)+  => Some3 (f3 :: k3 -> k2 -> k1 -> Type)+  -> (Demote k3, Demote k2, Demote 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)+  -> (Demote k4, Demote k3, Demote k2, Demote k1) -- ^+some4SingRep = \(Some4 sa4 sa3 sa2 sa1 _) ->+  (fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1)+{-# INLINE some4SingRep #-}++--------------------------------------------------------------------------------++-- | @'same1' x a b@ applies @x@ to the contents of @a@ and @b@ if their type+-- indexes are equal.+--+-- Hint: @'same1' ('some1' . 'Exinst.P1') :: 'Some1' f -> 'Some1' g -> 'Some1' ('Exinst.P1' f g)@+{-# INLINABLE same1 #-}+same1+  :: SDecide k1+  => (forall a1. SingI a1 => f a1 -> g a1 -> x)+  -> Some1 (f :: k1 -> Type)+  -> Some1 (g :: k1 -> Type)+  -> Maybe x  -- ^+same1 z = \s1f s1g ->+  withSome1Sing s1f $ \sa1 f ->+    withSome1Sing s1g $ \sa1' g -> do+       Refl <- testEquality sa1 sa1'+       pure (z f g)++-- | @'same2' x a b@ applies @x@ to the contents of @a@ and @b@ if their type+-- indexes are equal.+--+-- Hint: @'same2' ('some2' . 'Exinst.P2') :: 'Some2' f -> 'Some2' g -> 'Some2' ('Exinst.P2' f g)@+{-# INLINABLE same2 #-}+same2+  :: (SDecide k2, SDecide k1)+  => (forall a2 a1. SingI a1 => f a2 a1 -> g a2 a1 -> x)+  -> Some2 (f :: k2 -> k1 -> Type)+  -> Some2 (g :: k2 -> k1 -> Type)+  -> Maybe x  -- ^+same2 z = \s2l s2g ->+  withSome2Sing s2l $ \sa2 sa1 f ->+    withSome2Sing s2g $ \sa2' sa1' g -> do+       Refl <- testEquality sa2 sa2'+       Refl <- testEquality sa1 sa1'+       pure (z f g)++-- | @'same3' x a b@ applies @x@ to the contents of @a@ and @b@ if their type+-- indexes are equal.+--+-- Hint: @'same3' ('some3' . 'Exinst.P3') :: 'Some3' f -> 'Some3' g -> 'Some3' ('Exinst.P3' f g)@+{-# INLINABLE same3 #-}+same3+  :: (SDecide k3, SDecide k2, SDecide k1)+  => (forall a3 a2 a1. (SingI a3, SingI a2, SingI a1)+        => f a3 a2 a1 -> g a3 a2 a1 -> x)+  -> Some3 (f :: k3 -> k2 -> k1 -> Type)+  -> Some3 (g :: k3 -> k2 -> k1 -> Type)+  -> Maybe x  -- ^+same3 z = \s3l s3g ->+  withSome3Sing s3l $ \sa3 sa2 sa1 f ->+    withSome3Sing s3g $ \sa3' sa2' sa1' g -> do+       Refl <- testEquality sa3 sa3'+       Refl <- testEquality sa2 sa2'+       Refl <- testEquality sa1 sa1'+       pure (z f g)++-- | @'same4' x a b@ applies @x@ to the contents of @a@ and @b@ if their type+-- indexes are equal.+--+-- Hint: @'same4' ('some4' . 'Exinst.P4') :: 'Some4' f -> 'Some4' g -> 'Some4' ('Exinst.P4' f g)@+{-# INLINABLE same4 #-}+same4+  :: (SDecide k4, SDecide k3, SDecide k2, SDecide k1)+  => (forall a4 a3 a2 a1. (SingI a4, SingI a3, SingI a2, SingI a1)+        => f a4 a3 a2 a1 -> g a4 a3 a2 a1 -> x)+  -> Some4 (f :: k4 -> k3 -> k2 -> k1 -> Type)+  -> Some4 (g :: k4 -> k3 -> k2 -> k1 -> Type)+  -> Maybe x  -- ^+same4 z = \s4l s4g ->+  withSome4Sing s4l $ \sa4 sa3 sa2 sa1 f ->+    withSome4Sing s4g $ \sa4' sa3' sa2' sa1' g -> do+       Refl <- testEquality sa4 sa4'+       Refl <- testEquality sa3 sa3'+       Refl <- testEquality sa2 sa2'+       Refl <- testEquality sa1 sa1'+       pure (z f g)++--------------------------------------------------------------------------------++-- | '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' #-}+
+ lib/Exinst/Internal/Product.hs view
@@ -0,0 +1,151 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE PolyKinds #-}++module Exinst.Internal.Product+ ( P1(P1)+ , P2(P2)+ , P3(P3)+ , P4(P4)+ ) where++import GHC.Generics (Generic)++#ifdef HAS_aeson+import Data.Aeson (FromJSON, ToJSON)+#endif++#ifdef HAS_binary+import qualified Data.Binary as Bin+#endif++#ifdef HAS_bytes+import qualified Data.Bytes.Serial as By+#endif++#ifdef HAS_cereal+import qualified Data.Serialize as Cer+#endif++#ifdef HAS_deepseq+import Control.DeepSeq (NFData)+#endif++#ifdef HAS_hashable+import Data.Hashable (Hashable)+#endif++#ifdef HAS_quickcheck+import qualified Test.QuickCheck as QC+#endif++#ifdef HAS_serialise+import qualified Codec.Serialise as Cborg+#endif++--------------------------------------------------------------------------------+-- Products++-- | Like 'Data.Functor.Product.Product' from "Data.Functor.Product", but+-- only intended to be used with kinds other than 'Type'.+--+-- This type is particularly useful when used in combination with 'Exinst.Some1'+-- as @'Exinst.Some1' ('P1' l r)@, so as to ensure that @l@ and @r@ are indexed+-- by the same type. Moreover, 'P1' already supports many common instances from+-- @base@, @hashable@, @deepseq@, @aeson@, @bytes@, @cereal@, @binary@, and+-- @quickcheck@ out of the box, so you can benefit from them as well.+data P1 l r (a1 :: k1)+  = P1 (l a1) (r a1)+  deriving (Eq, Show, Read, Ord, Generic)++-- | Like 'P1', but for @l@ and @r@ taking two type indexes.+data P2 l r (a2 :: k2) (a1 :: k1)+  = P2 (l a2 a1) (r a2 a1)+  deriving (Eq, Show, Read, Ord, Generic)++-- | Like 'P1', but for @l@ and @r@ taking three type indexes.+data P3 l r (a3 :: k3) (a2 :: k2) (a1 :: k1)+  = P3 (l a3 a2 a1) (r a3 a2 a1)+  deriving (Eq, Show, Read, Ord, Generic)++-- | Like 'P1', but for @l@ and @r@ taking four type indexes.+data P4 l r (a4 :: k4) (a3 :: k3) (a2 :: k2) (a1 :: k1)+  = P4 (l a4 a3 a2 a1) (r a4 a3 a2 a1)+  deriving (Eq, Show, Read, Ord, Generic)++--------------------------------------------------------------------------------+#ifdef HAS_hashable+instance (Hashable (l a1), Hashable (r a1)) => Hashable (P1 l r a1)+instance (Hashable (l a2 a1), Hashable (r a2 a1)) => Hashable (P2 l r a2 a1)+instance (Hashable (l a3 a2 a1), Hashable (r a3 a2 a1)) => Hashable (P3 l r a3 a2 a1)+instance (Hashable (l a4 a3 a2 a1), Hashable (r a4 a3 a2 a1)) => Hashable (P4 l r a4 a3 a2 a1)+#endif++--------------------------------------------------------------------------------+#ifdef HAS_deepseq+instance (NFData (l a1), NFData (r a1)) => NFData (P1 l r a1)+instance (NFData (l a2 a1), NFData (r a2 a1)) => NFData (P2 l r a2 a1)+instance (NFData (l a3 a2 a1), NFData (r a3 a2 a1)) => NFData (P3 l r a3 a2 a1)+instance (NFData (l a4 a3 a2 a1), NFData (r a4 a3 a2 a1)) => NFData (P4 l r a4 a3 a2 a1)+#endif++--------------------------------------------------------------------------------+#ifdef HAS_aeson+instance (FromJSON (l a1), FromJSON (r a1)) => FromJSON (P1 l r a1)+instance (FromJSON (l a2 a1), FromJSON (r a2 a1)) => FromJSON (P2 l r a2 a1)+instance (FromJSON (l a3 a2 a1), FromJSON (r a3 a2 a1)) => FromJSON (P3 l r a3 a2 a1)+instance (FromJSON (l a4 a3 a2 a1), FromJSON (r a4 a3 a2 a1)) => FromJSON (P4 l r a4 a3 a2 a1)++instance (ToJSON (l a1), ToJSON (r a1)) => ToJSON (P1 l r a1)+instance (ToJSON (l a2 a1), ToJSON (r a2 a1)) => ToJSON (P2 l r a2 a1)+instance (ToJSON (l a3 a2 a1), ToJSON (r a3 a2 a1)) => ToJSON (P3 l r a3 a2 a1)+instance (ToJSON (l a4 a3 a2 a1), ToJSON (r a4 a3 a2 a1)) => ToJSON (P4 l r a4 a3 a2 a1)+#endif++--------------------------------------------------------------------------------+#ifdef HAS_bytes+instance (By.Serial (l a1), By.Serial (r a1)) => By.Serial (P1 l r a1)+instance (By.Serial (l a2 a1), By.Serial (r a2 a1)) => By.Serial (P2 l r a2 a1)+instance (By.Serial (l a3 a2 a1), By.Serial (r a3 a2 a1)) => By.Serial (P3 l r a3 a2 a1)+instance (By.Serial (l a4 a3 a2 a1), By.Serial (r a4 a3 a2 a1)) => By.Serial (P4 l r a4 a3 a2 a1)+#endif++--------------------------------------------------------------------------------+#ifdef HAS_cereal+instance (Cer.Serialize (l a1), Cer.Serialize (r a1)) => Cer.Serialize (P1 l r a1)+instance (Cer.Serialize (l a2 a1), Cer.Serialize (r a2 a1)) => Cer.Serialize (P2 l r a2 a1)+instance (Cer.Serialize (l a3 a2 a1), Cer.Serialize (r a3 a2 a1)) => Cer.Serialize (P3 l r a3 a2 a1)+instance (Cer.Serialize (l a4 a3 a2 a1), Cer.Serialize (r a4 a3 a2 a1)) => Cer.Serialize (P4 l r a4 a3 a2 a1)+#endif++--------------------------------------------------------------------------------+#ifdef HAS_binary+instance (Bin.Binary (l a1), Bin.Binary (r a1)) => Bin.Binary (P1 l r a1)+instance (Bin.Binary (l a2 a1), Bin.Binary (r a2 a1)) => Bin.Binary (P2 l r a2 a1)+instance (Bin.Binary (l a3 a2 a1), Bin.Binary (r a3 a2 a1)) => Bin.Binary (P3 l r a3 a2 a1)+instance (Bin.Binary (l a4 a3 a2 a1), Bin.Binary (r a4 a3 a2 a1)) => Bin.Binary (P4 l r a4 a3 a2 a1)+#endif++--------------------------------------------------------------------------------+#ifdef HAS_quickcheck+instance (QC.Arbitrary (l a1), QC.Arbitrary (r a1)) => QC.Arbitrary (P1 l r a1) where+  arbitrary = P1 <$> QC.arbitrary <*> QC.arbitrary+  shrink (P1 x y) = P1 <$> QC.shrink x <*> QC.shrink y+instance (QC.Arbitrary (l a2 a1), QC.Arbitrary (r a2 a1)) => QC.Arbitrary (P2 l r a2 a1) where+  arbitrary = P2 <$> QC.arbitrary <*> QC.arbitrary+  shrink (P2 x y) = P2 <$> QC.shrink x <*> QC.shrink y+instance (QC.Arbitrary (l a3 a2 a1), QC.Arbitrary (r a3 a2 a1)) => QC.Arbitrary (P3 l r a3 a2 a1) where+  arbitrary = P3 <$> QC.arbitrary <*> QC.arbitrary+  shrink (P3 x y) = P3 <$> QC.shrink x <*> QC.shrink y+instance (QC.Arbitrary (l a4 a3 a2 a1), QC.Arbitrary (r a4 a3 a2 a1)) => QC.Arbitrary (P4 l r a4 a3 a2 a1) where+  arbitrary = P4 <$> QC.arbitrary <*> QC.arbitrary+  shrink (P4 x y) = P4 <$> QC.shrink x <*> QC.shrink y+#endif++--------------------------------------------------------------------------------+#ifdef HAS_serialise+instance (Cborg.Serialise (l a1), Cborg.Serialise (r a1)) => Cborg.Serialise (P1 l r a1)+instance (Cborg.Serialise (l a2 a1), Cborg.Serialise (r a2 a1)) => Cborg.Serialise (P2 l r a2 a1)+instance (Cborg.Serialise (l a3 a2 a1), Cborg.Serialise (r a3 a2 a1)) => Cborg.Serialise (P3 l r a3 a2 a1)+instance (Cborg.Serialise (l a4 a3 a2 a1), Cborg.Serialise (r a4 a3 a2 a1)) => Cborg.Serialise (P4 l r a4 a3 a2 a1)+#endif
+ lib/Exinst/Internal/Sum.hs view
@@ -0,0 +1,155 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE PolyKinds #-}++module Exinst.Internal.Sum+ ( S1(S1L,S1R)+ , S2(S2L,S2R)+ , S3(S3L,S3R)+ , S4(S4L,S4R)+ ) where++import GHC.Generics (Generic)++#ifdef HAS_aeson+import Data.Aeson (FromJSON, ToJSON)+#endif++#ifdef HAS_binary+import qualified Data.Binary as Bin+#endif++#ifdef HAS_bytes+import qualified Data.Bytes.Serial as By+#endif++#ifdef HAS_cereal+import qualified Data.Serialize as Cer+#endif++#ifdef HAS_deepseq+import Control.DeepSeq (NFData)+#endif++#ifdef HAS_hashable+import Data.Hashable (Hashable)+#endif++#ifdef HAS_quickcheck+import qualified Test.QuickCheck as QC+#endif++#ifdef HAS_serialise+import qualified Codec.Serialise as Cborg+#endif++--------------------------------------------------------------------------------+-- Sums++-- | Like 'Data.Functor.Sum.Sum' from "Data.Functor.Sum", but+-- only intended to be used with kinds other than 'Type'.+--+-- This type is particularly useful when used in combination with 'Exinst.Some1'+-- as @'Exinst.Some1' ('S1' l r)@, so as to ensure that @l@ and @r@ are indexed+-- by the same type. Moreover, 'S1' already supports many common instances from+-- @base@, @hashable@, @deepseq@, @aeson@, @bytes@, @cereal@, @binary@, and+-- @quickcheck@ out of the box, so you can benefit from them as well.+data S1 l r (a1 :: k1)+  = S1L (l a1) | S1R (r a1)+  deriving (Eq, Show, Read, Ord, Generic)++-- | Like 'S1', but for @l@ and @r@ taking two type indexes.+data S2 l r (a2 :: k2) (a1 :: k1)+  = S2L (l a2 a1) | S2R (r a2 a1)+  deriving (Eq, Show, Read, Ord, Generic)++-- | Like 'S1', but for @l@ and @r@ taking three type indexes.+data S3 l r (a3 :: k3) (a2 :: k2) (a1 :: k1)+  = S3L (l a3 a2 a1) | S3R (r a3 a2 a1)+  deriving (Eq, Show, Read, Ord, Generic)++-- | Like 'S1', but for @l@ and @r@ taking four type indexes.+data S4 l r (a4 :: k4) (a3 :: k3) (a2 :: k2) (a1 :: k1)+  = S4L (l a4 a3 a2 a1) | S4R (r a4 a3 a2 a1)+  deriving (Eq, Show, Read, Ord, Generic)++--------------------------------------------------------------------------------+#ifdef HAS_hashable+instance (Hashable (l a1), Hashable (r a1)) => Hashable (S1 l r a1)+instance (Hashable (l a2 a1), Hashable (r a2 a1)) => Hashable (S2 l r a2 a1)+instance (Hashable (l a3 a2 a1), Hashable (r a3 a2 a1)) => Hashable (S3 l r a3 a2 a1)+instance (Hashable (l a4 a3 a2 a1), Hashable (r a4 a3 a2 a1)) => Hashable (S4 l r a4 a3 a2 a1)+#endif++--------------------------------------------------------------------------------+#ifdef HAS_deepseq+instance (NFData (l a1), NFData (r a1)) => NFData (S1 l r a1)+instance (NFData (l a2 a1), NFData (r a2 a1)) => NFData (S2 l r a2 a1)+instance (NFData (l a3 a2 a1), NFData (r a3 a2 a1)) => NFData (S3 l r a3 a2 a1)+instance (NFData (l a4 a3 a2 a1), NFData (r a4 a3 a2 a1)) => NFData (S4 l r a4 a3 a2 a1)+#endif++--------------------------------------------------------------------------------+#ifdef HAS_aeson+instance (FromJSON (l a1), FromJSON (r a1)) => FromJSON (S1 l r a1)+instance (FromJSON (l a2 a1), FromJSON (r a2 a1)) => FromJSON (S2 l r a2 a1)+instance (FromJSON (l a3 a2 a1), FromJSON (r a3 a2 a1)) => FromJSON (S3 l r a3 a2 a1)+instance (FromJSON (l a4 a3 a2 a1), FromJSON (r a4 a3 a2 a1)) => FromJSON (S4 l r a4 a3 a2 a1)++instance (ToJSON (l a1), ToJSON (r a1)) => ToJSON (S1 l r a1)+instance (ToJSON (l a2 a1), ToJSON (r a2 a1)) => ToJSON (S2 l r a2 a1)+instance (ToJSON (l a3 a2 a1), ToJSON (r a3 a2 a1)) => ToJSON (S3 l r a3 a2 a1)+instance (ToJSON (l a4 a3 a2 a1), ToJSON (r a4 a3 a2 a1)) => ToJSON (S4 l r a4 a3 a2 a1)+#endif++--------------------------------------------------------------------------------+#ifdef HAS_bytes+instance (By.Serial (l a1), By.Serial (r a1)) => By.Serial (S1 l r a1)+instance (By.Serial (l a2 a1), By.Serial (r a2 a1)) => By.Serial (S2 l r a2 a1)+instance (By.Serial (l a3 a2 a1), By.Serial (r a3 a2 a1)) => By.Serial (S3 l r a3 a2 a1)+instance (By.Serial (l a4 a3 a2 a1), By.Serial (r a4 a3 a2 a1)) => By.Serial (S4 l r a4 a3 a2 a1)+#endif++--------------------------------------------------------------------------------+#ifdef HAS_cereal+instance (Cer.Serialize (l a1), Cer.Serialize (r a1)) => Cer.Serialize (S1 l r a1)+instance (Cer.Serialize (l a2 a1), Cer.Serialize (r a2 a1)) => Cer.Serialize (S2 l r a2 a1)+instance (Cer.Serialize (l a3 a2 a1), Cer.Serialize (r a3 a2 a1)) => Cer.Serialize (S3 l r a3 a2 a1)+instance (Cer.Serialize (l a4 a3 a2 a1), Cer.Serialize (r a4 a3 a2 a1)) => Cer.Serialize (S4 l r a4 a3 a2 a1)+#endif++--------------------------------------------------------------------------------+#ifdef HAS_binary+instance (Bin.Binary (l a1), Bin.Binary (r a1)) => Bin.Binary (S1 l r a1)+instance (Bin.Binary (l a2 a1), Bin.Binary (r a2 a1)) => Bin.Binary (S2 l r a2 a1)+instance (Bin.Binary (l a3 a2 a1), Bin.Binary (r a3 a2 a1)) => Bin.Binary (S3 l r a3 a2 a1)+instance (Bin.Binary (l a4 a3 a2 a1), Bin.Binary (r a4 a3 a2 a1)) => Bin.Binary (S4 l r a4 a3 a2 a1)+#endif++--------------------------------------------------------------------------------+#ifdef HAS_quickcheck+instance (QC.Arbitrary (l a1), QC.Arbitrary (r a1)) => QC.Arbitrary (S1 l r a1) where+  arbitrary = QC.oneof [ fmap S1L QC.arbitrary, fmap S1R QC.arbitrary ]+  shrink (S1L l) = S1L <$> QC.shrink l+  shrink (S1R r) = S1R <$> QC.shrink r+instance (QC.Arbitrary (l a2 a1), QC.Arbitrary (r a2 a1)) => QC.Arbitrary (S2 l r a2 a1) where+  arbitrary = QC.oneof [ fmap S2L QC.arbitrary, fmap S2R QC.arbitrary ]+  shrink (S2L l) = S2L <$> QC.shrink l+  shrink (S2R r) = S2R <$> QC.shrink r+instance (QC.Arbitrary (l a3 a2 a1), QC.Arbitrary (r a3 a2 a1)) => QC.Arbitrary (S3 l r a3 a2 a1) where+  arbitrary = QC.oneof [ fmap S3L QC.arbitrary, fmap S3R QC.arbitrary ]+  shrink (S3L l) = S3L <$> QC.shrink l+  shrink (S3R r) = S3R <$> QC.shrink r+instance (QC.Arbitrary (l a4 a3 a2 a1), QC.Arbitrary (r a4 a3 a2 a1)) => QC.Arbitrary (S4 l r a4 a3 a2 a1) where+  arbitrary = QC.oneof [ fmap S4L QC.arbitrary, fmap S4R QC.arbitrary ]+  shrink (S4L l) = S4L <$> QC.shrink l+  shrink (S4R r) = S4R <$> QC.shrink r+#endif++--------------------------------------------------------------------------------+#ifdef HAS_serialise+instance (Cborg.Serialise (l a1), Cborg.Serialise (r a1)) => Cborg.Serialise (S1 l r a1)+instance (Cborg.Serialise (l a2 a1), Cborg.Serialise (r a2 a1)) => Cborg.Serialise (S2 l r a2 a1)+instance (Cborg.Serialise (l a3 a2 a1), Cborg.Serialise (r a3 a2 a1)) => Cborg.Serialise (S3 l r a3 a2 a1)+instance (Cborg.Serialise (l a4 a3 a2 a1), Cborg.Serialise (r a4 a3 a2 a1)) => Cborg.Serialise (S4 l r a4 a3 a2 a1)+#endif
− src/lib/Exinst.hs 
@@ -1,677 +0,0 @@-{-# LANGUAGE CPP #-}--{- |--Exinst is a library providing you with tools to recover type-indexed types whose-type-indexes have been existentialized, as well as automatically deriving-instances for them, as long as said type indexes are singleton types-(see [singleton](https://hackage.haskell.org/package/singletons)).--In short, what @exinst@ currently gives you is: For any type @t :: k -> *@, if-@k@ is a singleton type and @c (t a) :: 'Constraint'@ is satisfied, then you can-existentialize away the @a@ parameter with @'Some1' t@, recover it later, and-have @c ('Some1' t)@ automatically satisfied. Currently, up to 4 type indexes-can be existentialized using 'Some1', 'Some2', 'Some3' and 'Some4' respectively.--NOTE: This tutorial asumes some familiarity with singleton types as implemented-by the [singleton](https://hackage.haskell.org/package/singletons) library.-A singleton type is, in very rough terms, a type inhabited by a single term,-which allows one to go from its term-level representation to its type-level-representation and back without much trouble. A bit like the term @()@, which-is of type @()@. Whenever you have the type @()@ you know what that its-term-level representation must be @()@, and whenever you have the term @()@-you know that its type must be @()@.---}--module Exinst- ( -- * Tutorial-   -- $motivation--   -- *** Usage-   -- $usage--   -- *** Recovering-   -- $recovering--   -- *** Many indexes-   -- $manyIndexes--   -- *** Writing instances-   -- $writingInstances--   -- *** Products and sums-   -- $prodsums--   -- * 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)--   -- * Products- , P1(P1)- , P2(P2)- , P3(P3)- , P4(P4)--   -- * Sums- , S1(S1L,S1R)- , S2(S2L,S2R)- , S3(S3L,S3R)- , S4(S4L,S4R)--   -- * Re-exports- , Constraint- , Dict(Dict)- , Sing- , SingI- ) where--import Data.Constraint (Constraint, Dict(Dict))--import Data.Singletons (Sing, SingI)--import Exinst.Internal-import Exinst.Internal.Product-import Exinst.Internal.Sum--import Exinst.Instances.Base ()--#ifdef VERSION_aeson-import Exinst.Instances.Aeson ()-#endif--#ifdef VERSION_binary-import Exinst.Instances.Binary ()-#endif--#ifdef VERSION_bytes-import Exinst.Instances.Bytes ()-#endif--#ifdef VERSION_cereal-import Exinst.Instances.Cereal ()-#endif--#ifdef VERSION_deepseq-import Exinst.Instances.DeepSeq ()-#endif--#ifdef VERSION_hashable-import Exinst.Instances.Hashable ()-#endif--#ifdef VERSION_QuickCheck-import Exinst.Instances.QuickCheck ()-#endif---{- $motivation--As a motivation, let's consider the following example:--@-\{\-\# LANGUAGE GADTs \#\-\}-\{\-\# LANGUAGE DataKinds \#\-\}-\{\-\# LANGUAGE KindSignatures \#\-\}-\{\-\# LANGUAGE FlexibleInstances \#\-\}-\{\-\# LANGUAGE StandaloneDeriving \#\-\}--data Size = Big | Small--data Receptacle (a :: Size) :: * where-  Vase :: Receptacle 'Small-  Glass :: Receptacle 'Small-  Barrel :: Receptacle 'Big--deriving instance 'Show' (Receptacle a)-@--@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@.--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 have @[Receptacle 'Small]@ and @[Receptacle 'Big]@, but we-can't have @[Receptacle]@ nor @[forall a. Receptacle a]@. So, if we want to-have @Receptacle@s of different sizes in a container like @[]@, we need a-different solution.--At this point we need to ask ourselves why we need to put @Receptacle@s of-different sizes in a same container. If the answer is something like “because we-want to show all of them, no matter what size they are”, then we should realize-that what we are actually asking for is that no matter what @Size@ our-@Receptable@ has, we need to be able to find a 'Show' instance for that-@Receptacle@. In Haskell, we can express just that using existential types-and constraints hidden behind a data constructor.--@--- We need to add these language extensions to the ones in the previous example-\{\-\# LANGUAGE ExistentialQuantification \#\-\}-\{\-\# LANGUAGE FlexibleContexts \#\-\}--data ReceptacleOfAnySizeThatCanBeShown-  = forall a. ('Show' (Receptacle a))-      => MkReceptacleOfAnySizeThatCanBeShown (Receptacle a)-@--We can construct values of type @ReceptacleOfAnySizeThatCanBeShown@ only as long-as there exist a 'Show' instance for the @Receptacle a@ we give to the-@MkReceptacleOfAnySizeThatCanBeShown@ constructor. In our case, both @Receptacle-'Small@ and @Receptacle 'Big@ have 'Show' instances, so all of @Vase@, @Glass@ and-@Barrel@ can be used successfully with @MkReceptacleOfAnySizeThatCanBeShown@.--Now, @ReceptacleOfAnySizeThatCanBeShown@ on itself doesn't yet have a 'Show'-instance, and we can't derive one automatically using the @deriving@ mechanism,-but we can give an explicit 'Show' instance that just forwards the work to the-'Show' instance of the underlying @Receptacle a@.--@-instance 'Show' ReceptacleOfAnySizeThatCanBeShown where-  'show' (MkReceptacleOfAnySizeThatCanBeShown a) = 'show' a-@--That works as intended:--@-> 'show' (MkReceptacleOfAnySizeThatCanBeShown Vase)-"Vase"-> 'show' (MkReceptacleOfAnySizeThatCanBeShown Barrel)-"Barrel"-@--And now, as we wanted, we can put @Receptacle@s of different sizes in a @[]@ and-show them (as long as we wrap each of them as-@ReceptacleOfAnySizeThatCanBeShown@, that is).--@-> 'map' 'show' [MkReceptacleOfAnySizeThatCanBeShown Vase, MkReceptacleOfAnySizeThatCanBeShown Barrel]-["Vase", "Barrel"]-@--However, the above solution is unsatisfying for various reasons: For one, the-'Show' instance for @ReceptacleOfAnySizeThatCanBeShown@ works only as long as-the @ReceptacleOfAnySizeThatCanBeShown@ itself carries a witness that the 'Show'-constraint for @Receptacle a@ is satisfied, which means that if we want to write-yet another instance for @ReceptacleOfAnySizeThatCanBeShown@ that simply forwards-its implementation to the underlying @Receptacle a@, say 'Eq', then the-@MkReceptacleOfAnySizeThatCanBeShown@ constructor would need to be modified to witness-the @Eq (Receptacle a)@ instance too:--@-data ReceptacleOfAnySizeThatCanBeShown-  = forall a. ('Show' (Receptacle a), 'Eq' (Receptacle a))-      => MkReceptacleOfAnySizeThatCanBeShown (Receptacle a)-@--With that in place we can provide an 'Eq' instance for-@ReceptacleOfAnySizeThatCanBeShown@ as we did for 'Show' before, but if we pay-close attention, we can see how the implementation of-@ReceptacleOfAnySizeThatCanBeShown@ starts to become a bottleneck: Every-instance we want to provide for @ReceptacleOfAnySizeThatCanBeShown@ that simply-forwards its work to the underlying @Receptacle a@ needs to be witnessed by-@MkReceptacleOfAnySizeThatCanBeShown@ itself, it is not enough that there exists-an instance for @Receptacle a@. Moreover, even the name-@ReceptacleOfAnySizeThatCanBeShown@ that we chose before isn't completely-accurate anymore, and will become less and less accurate as we continue adding-constraints to @MkReceptacleOfAnySizeThatCanBeShown@.--Additionally, everywhere we use the @MkReceptacleOfAnySizeThatCanBeShown@-constructor we need to witness that the existentialized @Receptacle a@ satisfies-all the required constraints, which means that, if the @Receptacle a@ we pass to-@MkReceptacleOfAnySizeThatCanBeShown@ is being received, say, as a parameter to-a function, then the type of that function will also require that its caller-satisfies all of the same constraints, even though it is obvious to us,-statically, that the instances exist. We can now see how all of this becomes-unmanegeable, or at least very *boilerplatey*, as those constraints start to-propagate through our code base.--What we need is a way for instances such as the 'Show' instance for-@ReceptacleOfAnySizeThatCanBeShown@ to find the 'Show' instance for @Receptacle-a@ without it being explicitely witnessed by the-@MkReceptacleOfAnySizeThatCanBeShown@ constructor. That is exactly the problem-that @exinst@ solves: allowing /exi/stentials to find their /inst/ances. Thus,-the name of this library.---}--{- $usage--Given the code for @Size@, @Receptacle@ and its 'Show' instances above, we can-achieve the same functionality as our initial @ReceptacleOfAnySizeThatCanBeShown@ by-existentializing the type indexes of @Receptacle 'Small@ and @Receptacle 'Big@-as @'Some1' Receptacle@. In order to do that, we must first ensure that @Size@ and its-constructors can be used as singleton types (as supported by the @singletons@ library),-for which we can use some @TemplateHaskell@ provided by @Data.Singletons.TH@:--@-import qualified "Data.Singletons.TH"--Data.Singletons.TH.genSingletons [''Size]-@--And we'll also need a 'Show' instance for @Size@ for reasons that will become-apparent later:--@-deriving instance 'Show' Size-@--Now we can construct a @Show1 Size@ and 'show' achieving the same results as we-did with @ReceptacleOfAnySizeThatCanBeShown@ before.--Note: this code won't work yet. Keep reading.--@-> import "Exinst" ('Some1', 'some1')-> :t 'some1' Glass-:t 'some1' Glass :: 'Some1' Receptacle-> 'show' ('some1' Glass)-"Some1 Small Glass"-@--Well, actually, the default 'Show' instance for 'Some1' shows a bit more of-information, as it permits this string to be 'Read' back into a @'Some1'-Receptacle@ if needed, but displaying just @"Glass"@ would be possible too, if-desired.--The important thing to notice in the example above is that @some1@ does not-require us to satisfy a @'Show' (Receptacle 'Small)@ constraint, it just requires-that the type index for the type-indexed type we give it as argument is a-singleton type:--@-'some1' :: forall (f1 :: k1 -> *) (a1 :: k1). 'SingI' a1 => f1 a1 -> 'Some1' f1-@--It is the application of 'show' to @'some1' Glass@ which will fail to compile if-there isn't a 'Show' instance for @Receptacle 'Small@, complaining that a 'Show'-instance for @'Some1' Receptable@ can't be found. The reason for this is that even-if 'Show' instances for 'Some1' are derived for free, they are only derived for-@'Some1' (t :: k1 -> *)@ where a @'Show' (t a)@ for a specific but statically-unknown @a@ can be found at runtime (mostly, there are other minor requirements too).-The mechanism through which instances are found at runtime relies on 'Dict' from-the [constraints](https://hackage.haskell.org/package/constraints) library, which-@exinst@ wraps in a 'Dict1' typeclass to be instantiated once per singleton-type.--@--- The "Exinst.Dict1" class-class 'Dict1' (c :: k0 -> 'Constraint') (f1 :: k1 -> k0) where-  'dict1' :: 'Sing' (a1 :: k1) -> 'Dict' (c (f1 a1))-@--What 'Dict1' says is that: for a type-indexed type @f1@, given a term-level-representation of the singleton type that indexes said @f1@, we can obtain a-witness that the constraint @c@ is satisfied by @f1@ applied to the singleton-type.--That class seems to be a bit too abstract, but the instances we as users need to-write for it are quite silly and straightforward.--Here's an example of how to provide 'Show' support for @'Some1' Receptacle@ via-'Dict1':--@-instance ('Show' (Receptacle 'Small), 'Show' (Receptacle 'Big)) => 'Dict1' 'Show' Receptacle where-  'dict1' = \x -> case x of-    SSmall -> 'Dict'-    SBig -> 'Dict'-@--The implementation of @dict1@ looks quite silly, but it has to look like that as-it is only by pattern-matching on each of the @'Sing' Size@ constructors that we-learn about the type level representation of a singleton type, which we then use-to select the proper 'Show' instance among all of those listed in the instance head.--Given this 'Dict1' instance, we can proceed to excecute the REPL example mentioned before-and it will work just fine.--However, that 'Dict1' instance is still a bit insatisfactory: If we wanted,-again, to provide 'Eq' support for our @'Some1' Receptacle@ type, we would need to-write yet another 'Dict1' instance like the one above, but mentioning 'Eq'-instead of 'Show'. We can do better.--The trick, when writing 'Dict1' instances such as the one above, is to leave @c@-and @f1 :: k1 -> k0@ completely polymorphic, and instead only talk concretely-about the singleton type with kind @k1@. This might sound strange at first, as-@c@ and @f1@ are the only two type parameters to 'Dict1'. But as it often happens-when working with singleton types, we are not particularly interested in the-types involved, but in their kinds instead. So, this is the 'Dict1' instance-you often want to write:--@-instance (c (f1 'Small), c (f1 'Big)) => 'Dict1' c (f1 :: Size -> k0) where-  'dict1' = \x -> case x of-    SSmall -> 'Dict'-    SBig -> 'Dict'-@--That instance says that for any choice of @c@ and @f1 :: Size -> k0@, if an-instance for @c (f1 a)@ exists for a specific choice of @a@, then, given a term-level representation for that @a@ and the aid of @dict1@, said instance can be-looked up at runtime.--Notice that 'Some1' itself doesn't have any requirements about 'Dict1', it's the-various instances for 'Some1' who rely on 'Dict1'. 'Dict1' has nothing to do-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@.--The @Exinst@ module exports ready-made instances for 'Some1', 'Some2', 'Some3'-and 'Some4' (they can be enabled or disabled with some cabal flags).--* 'Eq', 'Ord', 'Show' from the @base@ package.--* 'Data.Aeson.FromJSON' and 'Data.Aeson.ToJSON' from the @aeson@ package.--* 'Data.Bytes.Serial' from the @bytes@ package.--* 'Cereal.Serialize.Serialize' from the @cereal@ package.--* 'Data.Binary.Binary' from the @binary@ package.--* 'Data.Hashable.Hashable' from the @hashable@ package.--* 'Control.DeepSeq.NFData' from the @deepseq@ package.--* 'Test.QuickCheck.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-@class Y => Z a@ satisfied for @'Some1' (f :: k1 -> *)@, then make sure an instance-for @Z@ is available for the @DemoteRep k1@, that a @'Dict1' Z (f :: k1 -> k0)@ or-more general instance exists, and that the @Y@ instance for @'Some1' (f :: k1 ->-*)@ exists too.--Here is the full code needed to have, say, the 'Eq' and 'Show' instances-available for @'Some1' Receptacle@:--@-\{\-\# LANGUAGE ConstraintKinds \#\-\}-\{\-\# LANGUAGE DataKinds \#\-\}-\{\-\# LANGUAGE FlexibleInstances \#\-\}-\{\-\# LANGUAGE GADTs \#\-\}-\{\-\# LANGUAGE KindSignatures \#\-\}-\{\-\# LANGUAGE MultiParamTypeClasses \#\-\}-\{\-\# LANGUAGE OverloadedStrings \#\-\}-\{\-\# LANGUAGE StandaloneDeriving \#\-\}-\{\-\# LANGUAGE TemplateHaskell \#\-\}-\{\-\# LANGUAGE TypeFamilies \#\-\}-\{\-\# LANGUAGE UndecidableInstances \#\-\}--import qualified "Data.Singletons.TH"-import           "Exinst" ('Dict'('Dict'), 'Dict1'('dict1'))--data Size = Big | Small-  deriving ('Eq', 'Show')--Data.Singletons.TH.genSingletons [''Size]-Data.Singletons.TH.singDecideInstances [''Size]--instance (c (f 'Big), c (f 'Small)) => 'Dict1' c f where-  'dict1' = \x -> case x of-    SBig -> 'Dict'-    SSmall -> 'Dict'---data Receptacle (a :: Size) :: * where-  Vase :: Receptacle 'Small-  Glass :: Receptacle 'Small-  Barrel :: Receptacle 'Big--deriving instance 'Eq' (Receptacle a)-deriving instance 'Show' (Receptacle a)-@--Now, @'Some1' Receptacle@ will have 'Eq' and 'Show' instances:--@-> -- Trying 'fromSome1'.-> 'fromSome1' ('some1' Vase) == 'Just' Vase-'True'-> 'fromSome1' ('some1' Vase) == 'Just' Glass-'False'-> 'fromSome1' ('some1' Vase) == 'Just' Barrel-'False'--> -- Trying 'withSome1'-> 'withSome1' ('some1' Vase) 'show'-"Vase"-> 'withSome1' ('some1' Vase) (== Vase)    -- This will fail, use 'fromSome1'-                                      -- if you know you are expecting-                                      -- a @Receptacle 'Small@--> -- Trying the 'Eq' instance.-> 'some1' Vase == 'some1' Vase-'True'-> 'some1' Vase == 'some1' Glass-'False'-> 'some1' Vase == 'some1' Barrel-'False'--> -- Trying the 'Show' instance.-> 'show' ('some1' Vase)-"Some1 Small Vase"-> 'map' 'show' ['some1' Vase, 'some1' Glass, 'some1' Barrel]-["Some1 Small Vase","Some1 Small Glass","Some1 Big Barrel"]-@---}--{- $manyIndexes--Just like 'Some1' hides the last singleton type index from fully applied-type-indexed type, 'Some2' hides the last two type indexes, 'Some3' hides the-last three, and 'Some3' hides the last four. They can be used in the same way as-'Some1'.--Like as most instances for 'Some1' require 'Dict1' instances to be present for-their singleton type-index, most instances for 'Some2', 'Some3' and 'Some4' will-require that 'Dict2', 'Dict3' or 'Dict4' instances exist, respectively. Writing-these instances is very straightforward. Supposing you have a type @X :: T4 ->-T3 -> T2 -> T1 -> *@ and want to existentialize all of the four type indexes yet-be able to continue using all of its instances, we can write something like-this:--@-instance (c (f1 'T1a), c (f1 'T1b)) => 'Dict1' c (f1 :: T1 -> k0) where-  'dict1' = \x -> case x of { ST1a -> 'Dict'; ST1b -> 'Dict' }-instance ('Dict1' c (f2 'T2a), 'Dict1' c (f2 'T2b)) => 'Dict2' c (f2 :: T2 -> k1 -> k0) where-  'dict2' = \x -> case x of { ST2a -> 'dict1'; ST2b -> 'dict1' }-instance ('Dict2' c (f3 'T3a), 'Dict2' c (f3 'T3b)) => 'Dict3' c (f3 :: T3 -> k2 -> k1 -> k0) where-  'dict3' = \x -> case x of { ST3a -> 'dict2'; ST3b -> 'dict2' }-instance ('Dict3' c (f4 'T4a), 'Dict3' c (f4 'T4b)) => 'Dict4' c (f4 :: T4 -> k3 -> k2 -> k1 -> k0) where-  'dict4' = \x -> case x of { ST4a -> 'dict3'; ST4b -> 'dict3' }-@--That is, assuming the following @T1@, @T2@, @T3@ and @T4@:--@-data T4 = T4a | T4b-data T3 = T3a | T3b-data T2 = T2a | T2b-data T1 = T1a | T1b-@--Effectively, we wrote just one instance per singleton type per type-index-position, each of them promoting a term-level representation of a singleton-type to its type-level representation and forwarding the rest of the work to-a “smaller” dict. That is, 'dict4' reifies the type of the fourth-to-last-type-index of @X@ and then calls 'dict3' to do the same for the third-to-last-type-index of @X@ and so on. Notice, however, how we didn't need to mention @X@-in none of the instances above: As we said before, these instances are-intended to work for any choice of @c@, @f4@, @f3@, @f2@ and @f1@.---}--{- $recovering--If you have a @'Some1' (f :: k -> *)@ and you know, statically, that you need an-specific @f (a :: k)@, then you can use 'fromSome1' which will give you an-@f (a :: k)@ only if @a@ was the type that was existentialized by 'Some1'.-Using 'fromSome1' requires that the singleton type-index implements-'Data.Singletons.Decide.SDecide', which can be derived mechanically with-`TemplateHaskell` by means of 'Data.Singletons.TH.singInstance'.--If you don't know, statically, the type of @f (a :: k)@, then you can use-'withSome1Sing' or 'withSome1' to work with @f (a :: k)@ as long as @a@ never-leaves their scope (don't worry, the compiler will yell at you if you try to do-that).---}---{- $prodsums--Consider the following types and constructors:--@-data X (a :: 'Bool') where-  XT :: X ''True'-  XF :: X ''False'--data Y (a :: 'Bool') where-  YT :: Y ''True'-  YF :: Y ''False'-@--You can use '(,)' to create a product for values of this type, and 'Either' to-create a sum. However, see what happens if we try to existentialize the type-index when using that approach:--@-> :t ('some1' XT, 'some1' YT)-('some1' XT, 'some1' YT) :: ('Some1' X, 'Some1' Y)-> :t ('some1' XT, 'some1' YF)-('some1' XT, 'some1' YF) :: ('Some1' X, 'Some1' Y)-@--It works, but there is no type level guarantee that the type index taken by @X@-and @Y@ is the same. If you do want to enforce that restriction, then you can-use @P1@ instead:--@-> :t 'P1'-'P1' :: l a -> r a -> 'P1' l r (a :: k)-> :t 'P1' XT YT-'P1' XT YT :: 'P1' X Y ''True'-> :t 'P1' XT YT-'P1' XT YT :: 'P1' X Y ''True'-> :t 'some1' ('P1' XT YT)-'some1' ('P1' XT YT) :: 'Some1' ('P1' X Y)-@--Trying to mix @XT@ with @YF@ fails, of course, since they have different type-indexes:--@-> :t 'P1' XT YF-\<interactive\>:1:7: error:-    • Couldn't match type ‘''False'’ with ‘''True'’-      Expected type: Y ''True'-        Actual type: Y ''False'-    • In the second argument of ‘'P1'’, namely ‘YF’-      In the expression: 'P1' XT YF-@--Moreover, 'P1' supports many common instances from @base@, @hashable@,-@deepseq@, @aeson@, @bytes@, @cereal@, @binary@ and @quickcheck@ out of the-box, so you can benefit from them as well.--There's also 'P2', 'P3' and 'P4' for product types taking a different number of-indexes, and also 'S1', 'S2', 'S3' and 'S4' for sum types:--@-> :t 'S1L'-'S1L' :: l a -> 'S1' l r (a :: k)-> :t 'S1R'-'S1R' :: r a -> 'S1' l r (a :: k)-> :t 'S1L' XT-'S1L' XT :: 'S1' X r ''True'-> :t 'S1R' YT-'S1R' YT :: 'S1' l Y ''True'-> :t 'some1' ('S1L' XT)-'some1' ('S1L' XT) :: 'Some1' ('S1' X r)-> :t 'some1' ('S1R' YT)-'some1' ('S1R' YT) :: 'Some1' ('S1' l Y)-@---}---{- $writingInstances--Instances for 'Some1' seem to come out of thin air, but the truth is that they-need to be written at least once by library authors so that, provided all its-requirements are satisfied, they are made available.--For example, when we imported "Exinst" before, we also brought to scope, among-other things, the 'Eq' instance for 'Some1', which is defined as this:--@-instance forall (f :: k1 -> *).-  ( 'Data.Singletons.Decide.SDecide' k1-  , 'Dict1' 'Eq' f-  ) => 'Eq' ('Some1' f)-  where-  (==) = \\som1x som1y ->-     'withSome1Sing' som1x $ \\sa1x (x :: f a1x) ->-        'withSome1Sing' som1y $ \\sa1y (y :: f a1y) ->-           'maybe' 'False' 'id' $ do-              'Data.Type.Equality.Refl' <- 'Data.Type.Equality.testEquality' sa1x sa1y-              case 'dict1' sa1x :: 'Dict' ('Eq' (f a1x)) of-                 'Dict' -> 'Just' (x == y)-@--This code should be relatively straightforward if you are familiar with uses of-the @singletons@ and @constraints@ libraries. We are simply reifying singleton-types from their term-level representation to their type-level representation,-and afterwards using the 'Dict1' mechanism to lookup the required instances-during runtime. Additionaly, this instance requires that the term level-representation of the singleton type implements 'Show' too, as, like we saw in a-previous example, the type index itself is shown in this 'Show' implementation,-in the hope that it can be later recovered and reified to the type level when-using 'Read'.---}
− src/lib/Exinst/Instances/Aeson.hs 
@@ -1,159 +0,0 @@-{-# 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 (f :: k1 -> *)-  . ( SingKind k1-    , Ae.ToJSON (DemoteRep k1)-    , Dict1 Ae.ToJSON f-    ) => Ae.ToJSON (Some1 f)-  where-    {-# INLINABLE toJSON #-}-    toJSON = \some1x -> withSome1Sing some1x $ \sa1 (x :: f a1) ->-       case dict1 sa1 :: Dict (Ae.ToJSON (f a1)) of-          Dict -> Ae.toJSON (fromSing sa1, x)--instance forall (f :: k2 -> k1 -> *)-  . ( SingKind k2-    , SingKind k1-    , Ae.ToJSON (DemoteRep k2)-    , Ae.ToJSON (DemoteRep k1)-    , Dict2 Ae.ToJSON f-    ) => Ae.ToJSON (Some2 f)-  where-    {-# INLINABLE toJSON #-}-    toJSON = \some2x -> withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) ->-       case dict2 sa2 sa1 :: Dict (Ae.ToJSON (f a2 a1)) of-          Dict -> Ae.toJSON ((fromSing sa2, fromSing sa1), x)--instance forall (f :: k3 -> k2 -> k1 -> *)-  . ( SingKind k3-    , SingKind k2-    , SingKind k1-    , Ae.ToJSON (DemoteRep k3)-    , Ae.ToJSON (DemoteRep k2)-    , Ae.ToJSON (DemoteRep k1)-    , Dict3 Ae.ToJSON f-    ) => Ae.ToJSON (Some3 f)-  where-    {-# INLINABLE toJSON #-}-    toJSON = \some3x -> withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) ->-       case dict3 sa3 sa2 sa1 :: Dict (Ae.ToJSON (f a3 a2 a1)) of-          Dict -> Ae.toJSON ((fromSing sa3, fromSing sa2, fromSing sa1), x)--instance forall (f :: 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 f-    ) => Ae.ToJSON (Some4 f)-  where-    {-# INLINABLE toJSON #-}-    toJSON = \some4x -> withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) ->-       case dict4 sa4 sa3 sa2 sa1 :: Dict (Ae.ToJSON (f a4 a3 a2 a1)) of-          Dict -> Ae.toJSON ((fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1), x)------------------------------------------------------------------------------------instance forall (f :: k1 -> *)-  . ( SingKind k1-    , Ae.FromJSON (DemoteRep k1)-    , Dict1 Ae.FromJSON f-    ) => Ae.FromJSON (Some1 f)-  where-    {-# INLINABLE parseJSON #-}-    parseJSON = \v -> do-      (rsa1, v') <- Ae.parseJSON v-      withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->-         case dict1 sa1 :: Dict (Ae.FromJSON (f a1)) of-            Dict -> do-               x :: f a1 <- Ae.parseJSON v'-               pure (Some1 sa1 x)--instance forall (f :: k2 -> k1 -> *)-  . ( SingKind k2-    , SingKind k1-    , Ae.FromJSON (DemoteRep k2)-    , Ae.FromJSON (DemoteRep k1)-    , Dict2 Ae.FromJSON f-    ) => Ae.FromJSON (Some2 f)-  where-    {-# INLINABLE parseJSON #-}-    parseJSON = \v -> do-      ((rsa2, rsa1), v') <- Ae.parseJSON v-      withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->-         withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->-            case dict2 sa2 sa1 :: Dict (Ae.FromJSON (f a2 a1)) of-               Dict -> do-                  x :: f a2 a1 <- Ae.parseJSON v'-                  pure (Some2 sa2 sa1 x)--instance forall (f :: k3 -> k2 -> k1 -> *)-  . ( SingKind k3-    , SingKind k2-    , SingKind k1-    , Ae.FromJSON (DemoteRep k3)-    , Ae.FromJSON (DemoteRep k2)-    , Ae.FromJSON (DemoteRep k1)-    , Dict3 Ae.FromJSON f-    ) => Ae.FromJSON (Some3 f)-  where-    {-# INLINABLE parseJSON #-}-    parseJSON = \v -> do-      ((rsa3, rsa2, rsa1), v') <- Ae.parseJSON v-      withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) ->-         withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->-            withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->-               case dict3 sa3 sa2 sa1 :: Dict (Ae.FromJSON (f a3 a2 a1)) of-                  Dict -> do-                     x :: f a3 a2 a1 <- Ae.parseJSON v'-                     pure (Some3 sa3 sa2 sa1 x)--instance forall (f :: 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 f-    ) => Ae.FromJSON (Some4 f)-  where-    {-# INLINABLE parseJSON #-}-    parseJSON = \v -> do-      ((rsa4, rsa3, rsa2, rsa1), v') <- Ae.parseJSON v-      withSomeSing rsa4 $ \(sa4 :: Sing (a4 :: k4)) ->-         withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) ->-            withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->-               withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->-                  case dict4 sa4 sa3 sa2 sa1 :: Dict (Ae.FromJSON (f a4 a3 a2 a1)) of-                     Dict -> do-                        x :: f a4 a3 a2 a1 <- Ae.parseJSON v'-                        pure (Some4 sa4 sa3 sa2 sa1 x)
− src/lib/Exinst/Instances/Base.hs 
@@ -1,622 +0,0 @@-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# 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", 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.Base () where--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 qualified GHC.Generics as G-import Prelude-import qualified Text.Read as Read--import Exinst.Internal-  hiding (Some1(..), Some2(..), Some3(..), Some4(..))-import qualified Exinst.Internal as Exinst------------------------------------------------------------------------------------- Show---- Internal wrappers used to avoid writing the string manipulation in 'Show'.-data Some1'Show r1 x = Some1 r1 x deriving (Show)-data Some2'Show r2 r1 x = Some2 r2 r1 x deriving (Show)-data Some3'Show r3 r2 r1 x = Some3 r3 r2 r1 x deriving (Show)-data Some4'Show r4 r3 r2 r1 x = Some4 r4 r3 r2 r1 x deriving (Show)--instance forall (f :: k1 -> Type)-  . ( SingKind k1-    , Show (DemoteRep k1)-    , Dict1 Show f-    ) => Show (Exinst.Some1 f)-  where-    {-# INLINABLE showsPrec #-}-    showsPrec n = \some1x -> withSome1Sing some1x $ \sa1 (x :: f a1) ->-       case dict1 sa1 :: Dict (Show (f a1)) of-          Dict -> showsPrec n (Some1 (fromSing sa1) x)--instance forall (f :: k2 -> k1 -> Type)-  . ( SingKind k2-    , SingKind k1-    , Show (DemoteRep k2)-    , Show (DemoteRep k1)-    , Dict2 Show f-    ) => Show (Exinst.Some2 f)-  where-    {-# INLINABLE showsPrec #-}-    showsPrec n = \some2x -> withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) ->-       case dict2 sa2 sa1 :: Dict (Show (f a2 a1)) of-          Dict -> showsPrec n (Some2 (fromSing sa2) (fromSing sa1) x)--instance forall (f :: k3 -> k2 -> k1 -> Type)-  . ( SingKind k3-    , SingKind k2-    , SingKind k1-    , Show (DemoteRep k3)-    , Show (DemoteRep k2)-    , Show (DemoteRep k1)-    , Dict3 Show f-    ) => Show (Exinst.Some3 f)-  where-    {-# INLINABLE showsPrec #-}-    showsPrec n = \some3x -> withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) ->-       case dict3 sa3 sa2 sa1 :: Dict (Show (f a3 a2 a1)) of-          Dict -> showsPrec n (Some3 (fromSing sa3) (fromSing sa2) (fromSing sa1) x)--instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type)-  . ( SingKind k4-    , SingKind k3-    , SingKind k2-    , SingKind k1-    , Show (DemoteRep k4)-    , Show (DemoteRep k3)-    , Show (DemoteRep k2)-    , Show (DemoteRep k1)-    , Dict4 Show f-    ) => Show (Exinst.Some4 f)-  where-    {-# INLINABLE showsPrec #-}-    showsPrec n = \some4x -> withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) ->-       case dict4 sa4 sa3 sa2 sa1 :: Dict (Show (f a4 a3 a2 a1)) of-          Dict -> showsPrec n (Some4 (fromSing sa4) (fromSing sa3)-                                     (fromSing sa2) (fromSing sa1) x)------------------------------------------------------------------------------------- Read--instance forall (f :: k1 -> Type)-  . ( SingKind k1-    , Read (DemoteRep k1)-    , Dict1 Read f-    ) => Read (Exinst.Some1 f)-  where-    {-# INLINABLE readPrec #-}-    readPrec = do-      Read.Ident "Some1" <- Read.lexP-      rsa1 <- Read.readPrec-      withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->-         case dict1 sa1 :: Dict (Read (f a1)) of-            Dict -> do-               x :: f a1 <- Read.readPrec-               pure (Exinst.Some1 sa1 x)--instance forall (f :: k2 -> k1 -> Type)-  . ( SingKind k2-    , SingKind k1-    , Read (DemoteRep k2)-    , Read (DemoteRep k1)-    , Dict2 Read f-    ) => Read (Exinst.Some2 f)-  where-    {-# INLINABLE readPrec #-}-    readPrec = do-      Read.Ident "Some2" <- Read.lexP-      rsa2 <- Read.readPrec-      rsa1 <- Read.readPrec-      withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->-         withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->-            case dict2 sa2 sa1 :: Dict (Read (f a2 a1)) of-               Dict -> do-                  x :: f a2 a1 <- Read.readPrec-                  pure (Exinst.Some2 sa2 sa1 x)--instance forall (f :: k3 -> k2 -> k1 -> Type)-  . ( SingKind k3-    , SingKind k2-    , SingKind k1-    , Read (DemoteRep k3)-    , Read (DemoteRep k2)-    , Read (DemoteRep k1)-    , Dict3 Read f-    ) => Read (Exinst.Some3 f)-  where-    {-# INLINABLE readPrec #-}-    readPrec = do-      Read.Ident "Some3" <- Read.lexP-      rsa3 <- Read.readPrec-      rsa2 <- Read.readPrec-      rsa1 <- Read.readPrec-      withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) ->-         withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->-            withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->-               case dict3 sa3 sa2 sa1 :: Dict (Read (f a3 a2 a1)) of-                  Dict -> do-                     x :: f a3 a2 a1 <- Read.readPrec-                     pure (Exinst.Some3 sa3 sa2 sa1 x)--instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type)-  . ( SingKind k4-    , SingKind k3-    , SingKind k2-    , SingKind k1-    , Read (DemoteRep k4)-    , Read (DemoteRep k3)-    , Read (DemoteRep k2)-    , Read (DemoteRep k1)-    , Dict4 Read f-    ) => Read (Exinst.Some4 f)-  where-    {-# INLINABLE readPrec #-}-    readPrec = do-      Read.Ident "Some4" <- Read.lexP-      rsa4 <- Read.readPrec-      rsa3 <- Read.readPrec-      rsa2 <- Read.readPrec-      rsa1 <- Read.readPrec-      withSomeSing rsa4 $ \(sa4 :: Sing (a4 :: k4)) ->-         withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) ->-            withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->-               withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->-                  case dict4 sa4 sa3 sa2 sa1 :: Dict (Read (f a4 a3 a2 a1)) of-                     Dict -> do-                        x :: f a4 a3 a2 a1 <- Read.readPrec-                        pure (Exinst.Some4 sa4 sa3 sa2 sa1 x)------------------------------------------------------------------------------------- Eq--instance forall (f :: k1 -> Type).-  ( SDecide k1-  , Dict1 Eq f-  ) => Eq (Exinst.Some1 f)-  where-  {-# INLINABLE (==) #-}-  (==) = \som1x som1y ->-     withSome1Sing som1x $ \sa1x (x :: f a1x) ->-        withSome1Sing som1y $ \sa1y (y :: f a1y) ->-           maybe False id $ do-              Refl <- testEquality sa1x sa1y-              case dict1 sa1x :: Dict (Eq (f a1x)) of-                 Dict -> Just (x == y)--instance forall (f :: k2 -> k1 -> Type)-  . ( SDecide k2-    , SDecide k1-    , Dict2 Eq f-    ) => Eq (Exinst.Some2 f)-  where-    {-# INLINABLE (==) #-}-    (==) = \som2x som2y ->-       withSome2Sing som2x $ \sa2x sa1x (x :: f a2x a1x) ->-          withSome2Sing som2y $ \sa2y sa1y (y :: f a2y a1y) ->-             maybe False id $ do-                Refl <- testEquality sa2x sa2y-                Refl <- testEquality sa1x sa1y-                case dict2 sa2x sa1x :: Dict (Eq (f a2x a1x)) of-                   Dict -> Just (x == y)--instance forall (f :: k3 -> k2 -> k1 -> Type)-  . ( SDecide k3-    , SDecide k2-    , SDecide k1-    , Dict3 Eq f-    ) => Eq (Exinst.Some3 f)-  where-    {-# INLINABLE (==) #-}-    (==) = \som3x som3y ->-       withSome3Sing som3x $ \sa3x sa2x sa1x (x :: f a3x a2x a1x) ->-          withSome3Sing som3y $ \sa3y sa2y sa1y (y :: f a3y a2y a1y) ->-             maybe False id $ do-                Refl <- testEquality sa3x sa3y-                Refl <- testEquality sa2x sa2y-                Refl <- testEquality sa1x sa1y-                case dict3 sa3x sa2x sa1x :: Dict (Eq (f a3x a2x a1x)) of-                   Dict -> Just (x == y)--instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type)-  . ( SDecide k4-    , SDecide k3-    , SDecide k2-    , SDecide k1-    , Dict4 Eq f-    ) => Eq (Exinst.Some4 f)-  where-    {-# INLINABLE (==) #-}-    (==) = \som4x som4y ->-       withSome4Sing som4x $ \sa4x sa3x sa2x sa1x (x :: f a4x a3x a2x a1x) ->-          withSome4Sing som4y $ \sa4y sa3y sa2y sa1y (y :: f a4y a3y a2y a1y) ->-             maybe False id $ do-                Refl <- testEquality sa4x sa4y-                Refl <- testEquality sa3x sa3y-                Refl <- testEquality sa2x sa2y-                Refl <- testEquality sa1x sa1y-                case dict4 sa4x sa3x sa2x sa1x :: Dict (Eq (f a4x a3x a2x a1x)) of-                   Dict -> Just (x == y)------------------------------------------------------------------------------------- Ord--instance forall (f :: k1 -> Type)-  . ( SingKind k1-    , SDecide k1-    , Ord (DemoteRep k1)-    , Dict1 Ord f-    , Eq (Exinst.Some1 f)-    ) => Ord (Exinst.Some1 f)-  where-    {-# INLINABLE compare #-}-    compare = \som1x som1y ->-       withSome1Sing som1x $ \sa1x (x :: f a1x) ->-          withSome1Sing som1y $ \sa1y (y :: f a1y) ->-             let termCompare = compare (fromSing sa1x) (fromSing sa1y)-             in maybe termCompare id $ do-                  Refl <- testEquality sa1x sa1y-                  case dict1 sa1x :: Dict (Ord (f a1x)) of-                     Dict -> Just (compare x y)--instance forall (f :: k2 -> k1 -> Type)-  . ( SingKind k2-    , SingKind k1-    , SDecide k2-    , SDecide k1-    , Ord (DemoteRep k2)-    , Ord (DemoteRep k1)-    , Dict2 Ord f-    , Eq (Exinst.Some2 f)-    ) => Ord (Exinst.Some2 f)-  where-    {-# INLINABLE compare #-}-    compare = \som2x som2y ->-       withSome2Sing som2x $ \sa2x sa1x (x :: f a2x a1x) ->-          withSome2Sing som2y $ \sa2y sa1y (y :: f a2y a1y) ->-             let termCompare = compare (fromSing sa2x, fromSing sa1x)-                                       (fromSing sa2y, fromSing sa1y)-             in maybe termCompare id $ do-                   Refl <- testEquality sa2x sa2y-                   Refl <- testEquality sa1x sa1y-                   case dict2 sa2x sa1x :: Dict (Ord (f a2x a1x)) of-                      Dict -> Just (compare x y)--instance forall (f :: k3 -> k2 -> k1 -> Type)-  . ( SingKind k3-    , SingKind k2-    , SingKind k1-    , SDecide k3-    , SDecide k2-    , SDecide k1-    , Ord (DemoteRep k3)-    , Ord (DemoteRep k2)-    , Ord (DemoteRep k1)-    , Dict3 Ord f-    , Eq (Exinst.Some3 f)-    ) => Ord (Exinst.Some3 f)-  where-    {-# INLINABLE compare #-}-    compare = \som3x som3y ->-       withSome3Sing som3x $ \sa3x sa2x sa1x (x :: f a3x a2x a1x) ->-          withSome3Sing som3y $ \sa3y sa2y sa1y (y :: f a3y a2y a1y) ->-             let termCompare = compare-                   (fromSing sa3x, fromSing sa2x, fromSing sa1x)-                   (fromSing sa3y, fromSing sa2y, fromSing sa1y)-             in maybe termCompare id $ do-                  Refl <- testEquality sa3x sa3y-                  Refl <- testEquality sa2x sa2y-                  Refl <- testEquality sa1x sa1y-                  case dict3 sa3x sa2x sa1x :: Dict (Ord (f a3x a2x a1x)) of-                     Dict -> Just (compare x y)--instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type)-  . ( SingKind k4-    , SingKind k3-    , SingKind k2-    , SingKind k1-    , SDecide k4-    , SDecide k3-    , SDecide k2-    , SDecide k1-    , Ord (DemoteRep k4)-    , Ord (DemoteRep k3)-    , Ord (DemoteRep k2)-    , Ord (DemoteRep k1)-    , Dict4 Ord f-    , Eq (Exinst.Some4 f)-    ) => Ord (Exinst.Some4 f)-  where-    {-# INLINABLE compare #-}-    compare = \som4x som4y ->-       withSome4Sing som4x $ \sa4x sa3x sa2x sa1x (x :: f a4x a3x a2x a1x) ->-          withSome4Sing som4y $ \sa4y sa3y sa2y sa1y (y :: f a4y a3y a2y a1y) ->-             let termCompare = compare-                   (fromSing sa4x, fromSing sa3x, fromSing sa2x, fromSing sa1x)-                   (fromSing sa4y, fromSing sa3y, fromSing sa2y, fromSing sa1y)-             in maybe termCompare id $ do-                  Refl <- testEquality sa4x sa4y-                  Refl <- testEquality sa3x sa3y-                  Refl <- testEquality sa2x sa2y-                  Refl <- testEquality sa1x sa1y-                  case dict4 sa4x sa3x sa2x sa1x :: Dict (Ord (f a4x a3x a2x a1x)) of-                     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 'DictX' instances for some @base@ types--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-
− src/lib/Exinst/Instances/Binary.hs 
@@ -1,137 +0,0 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE UndecidableInstances #-}--{-# OPTIONS_GHC -fno-warn-orphans #-}---- | This module exports 'Bin.Binary' 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.Binary () where--import qualified Data.Binary as Bin-import Data.Constraint-import Data.Singletons-import Prelude--import Exinst.Internal-------------------------------------------------------------------------------------- | Compatible with the 'Data.Bytes.Serial.Serial' instance and--- 'Data.Serialize.Serialize' instance, provided all of the 'DemoteRep's and the--- fully applied @f@ instances are compatible as well.-instance forall (f :: k1 -> *).-  ( SingKind k1-  , Bin.Binary (DemoteRep k1)-  , Dict1 Bin.Binary f-  ) => Bin.Binary (Some1 f) where-  {-# INLINABLE put #-}-  put = \some1x ->-    withSome1Sing some1x $ \sa1 (x :: f a1) ->-      case dict1 sa1 :: Dict (Bin.Binary (f a1)) of-        Dict -> do-          Bin.put (fromSing sa1)-          Bin.put x-  {-# INLINABLE get #-}-  get = do-    rsa1 <- Bin.get-    withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->-      case dict1 sa1 :: Dict (Bin.Binary (f a1)) of-        Dict -> do-          x :: f a1 <- Bin.get-          pure (Some1 sa1 x)---- | Compatible with the 'Data.Bytes.Serial.Serial' instance and--- 'Data.Serialize.Serialize' instance, provided all of the 'DemoteRep's and the--- fully applied @f@ instances are compatible as well.-instance forall (f :: k2 -> k1 -> *).-  ( SingKind k2-  , SingKind k1-  , Bin.Binary (DemoteRep k2)-  , Bin.Binary (DemoteRep k1)-  , Dict2 Bin.Binary f-  ) => Bin.Binary (Some2 f) where-  {-# INLINABLE put #-}-  put = \some2x ->-    withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) ->-      case dict2 sa2 sa1 :: Dict (Bin.Binary (f a2 a1)) of-        Dict -> do-          Bin.put (fromSing sa2, fromSing sa1)-          Bin.put x-  {-# INLINABLE get #-}-  get = do-    (rsa2, rsa1) <- Bin.get-    withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->-      withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->-        case dict2 sa2 sa1 :: Dict (Bin.Binary (f a2 a1)) of-          Dict -> do-            x :: f a2 a1 <- Bin.get-            pure (Some2 sa2 sa1 x)---- | Compatible with the 'Data.Bytes.Serial.Serial' instance and--- 'Data.Serialize.Serialize' instance, provided all of the 'DemoteRep's and the--- fully applied @f@ instances are compatible as well.-instance forall (f :: k3 -> k2 -> k1 -> *).-  ( SingKind k3-  , SingKind k2-  , SingKind k1-  , Bin.Binary (DemoteRep k3)-  , Bin.Binary (DemoteRep k2)-  , Bin.Binary (DemoteRep k1)-  , Dict3 Bin.Binary f-  ) => Bin.Binary (Some3 f) where-  {-# INLINABLE put #-}-  put = \some3x ->-    withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) ->-      case dict3 sa3 sa2 sa1 :: Dict (Bin.Binary (f a3 a2 a1)) of-        Dict -> do-          Bin.put (fromSing sa3, fromSing sa2, fromSing sa1)-          Bin.put x-  {-# INLINABLE get #-}-  get = do-    (rsa3, rsa2, rsa1) <- Bin.get-    withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) ->-      withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->-        withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->-          case dict3 sa3 sa2 sa1 :: Dict (Bin.Binary (f a3 a2 a1)) of-            Dict -> do-              x :: f a3 a2 a1 <- Bin.get-              pure (Some3 sa3 sa2 sa1 x)---- | Compatible with the 'Data.Bytes.Serial.Serial' instance and--- 'Data.Serialize.Serialize' instance, provided all of the 'DemoteRep's and the--- fully applied @f@ instances are compatible as well.-instance forall (f :: k4 -> k3 -> k2 -> k1 -> *).-  ( SingKind k4-  , SingKind k3-  , SingKind k2-  , SingKind k1-  , Bin.Binary (DemoteRep k4)-  , Bin.Binary (DemoteRep k3)-  , Bin.Binary (DemoteRep k2)-  , Bin.Binary (DemoteRep k1)-  , Dict4 Bin.Binary f-  ) => Bin.Binary (Some4 f) where-  {-# INLINABLE put #-}-  put = \some4x ->-    withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) ->-      case dict4 sa4 sa3 sa2 sa1 :: Dict (Bin.Binary (f a4 a3 a2 a1)) of-        Dict -> do-          Bin.put (fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1)-          Bin.put x-  {-# INLINABLE get #-}-  get = do-    (rsa4, rsa3, rsa2, rsa1) <- Bin.get-    withSomeSing rsa4 $ \(sa4 :: Sing (a4 :: k4)) ->-      withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) ->-        withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->-          withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->-            case dict4 sa4 sa3 sa2 sa1 :: Dict (Bin.Binary (f a4 a3 a2 a1)) of-              Dict -> do-                x :: f a4 a3 a2 a1 <- Bin.get-                pure (Some4 sa4 sa3 sa2 sa1 x)
− src/lib/Exinst/Instances/Bytes.hs 
@@ -1,138 +0,0 @@-{-# 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-------------------------------------------------------------------------------------- | Compatible with the 'Data.Binary.Binary' instance and--- 'Data.Serialize.Serialize' instance, provided all of the 'DemoteRep's and the--- fully applied @f@ instances are compatible as well.-instance forall (f :: k1 -> *).-  ( SingKind k1-  , By.Serial (DemoteRep k1)-  , Dict1 By.Serial f-  ) => By.Serial (Some1 f) where-  {-# INLINABLE serialize #-}-  serialize = \some1x ->-    withSome1Sing some1x $ \sa1 (x :: f a1) ->-      case dict1 sa1 :: Dict (By.Serial (f a1)) of-        Dict -> do-          By.serialize (fromSing sa1)-          By.serialize x-  {-# INLINABLE deserialize #-}-  deserialize = do-    rsa1 <- By.deserialize-    withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->-      case dict1 sa1 :: Dict (By.Serial (f a1)) of-        Dict -> do-          x :: f a1 <- By.deserialize-          pure (Some1 sa1 x)---- | Compatible with the 'Data.Binary.Binary' instance and--- 'Data.Serialize.Serialize' instance, provided all of the 'DemoteRep's and the--- fully applied @f@ instances are compatible as well.-instance forall (f :: k2 -> k1 -> *).-  ( SingKind k2-  , SingKind k1-  , By.Serial (DemoteRep k2)-  , By.Serial (DemoteRep k1)-  , Dict2 By.Serial f-  ) => By.Serial (Some2 f) where-  {-# INLINABLE serialize #-}-  serialize = \some2x ->-    withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) ->-      case dict2 sa2 sa1 :: Dict (By.Serial (f 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)) ->-      withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->-        case dict2 sa2 sa1 :: Dict (By.Serial (f a2 a1)) of-          Dict -> do-            x :: f a2 a1 <- By.deserialize-            pure (Some2 sa2 sa1 x)---- | Compatible with the 'Data.Binary.Binary' instance and--- 'Data.Serialize.Serialize' instance, provided all of the 'DemoteRep's and the--- fully applied @f@ instances are compatible as well.-instance forall (f :: k3 -> k2 -> k1 -> *).-  ( SingKind k3-  , SingKind k2-  , SingKind k1-  , By.Serial (DemoteRep k3)-  , By.Serial (DemoteRep k2)-  , By.Serial (DemoteRep k1)-  , Dict3 By.Serial f-  ) => By.Serial (Some3 f) where-  {-# INLINABLE serialize #-}-  serialize = \some3x ->-    withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) ->-      case dict3 sa3 sa2 sa1 :: Dict (By.Serial (f 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)) ->-      withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->-        withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->-           case dict3 sa3 sa2 sa1 :: Dict (By.Serial (f a3 a2 a1)) of-             Dict -> do-               x :: f a3 a2 a1 <- By.deserialize-               pure (Some3 sa3 sa2 sa1 x)---- | Compatible with the 'Data.Binary.Binary' instance and--- 'Data.Serialize.Serialize' instance, provided all of the 'DemoteRep's and the--- fully applied @f@ instances are compatible as well.-instance forall (f :: 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 f-  ) => By.Serial (Some4 f) where-  {-# INLINABLE serialize #-}-  serialize = \some4x ->-    withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) ->-      case dict4 sa4 sa3 sa2 sa1 :: Dict (By.Serial (f 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)) ->-      withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) ->-        withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->-          withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->-            case dict4 sa4 sa3 sa2 sa1 :: Dict (By.Serial (f a4 a3 a2 a1)) of-              Dict -> do-                x :: f a4 a3 a2 a1 <- By.deserialize-                pure (Some4 sa4 sa3 sa2 sa1 x)
− src/lib/Exinst/Instances/Cereal.hs 
@@ -1,138 +0,0 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE UndecidableInstances #-}--{-# OPTIONS_GHC -fno-warn-orphans #-}---- | This module exports 'Cer.Serialize' 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.Cereal () where--import qualified Data.Serialize as Cer-import Data.Constraint-import Data.Singletons-import Prelude--import Exinst.Internal-------------------------------------------------------------------------------------- | Compatible with the 'Data.Bytes.Serial.Serial' instance and--- 'Data.Binary.Binary' instance, provided all of the 'DemoteRep's and the fully--- applied @f@ instances are compatible as well.-instance forall (f :: k1 -> *).-  ( SingKind k1-  , Cer.Serialize (DemoteRep k1)-  , Dict1 Cer.Serialize f-  ) => Cer.Serialize (Some1 f) where-  {-# INLINABLE put #-}-  put = \some1x ->-    withSome1Sing some1x $ \sa1 (x :: f a1) ->-      case dict1 sa1 :: Dict (Cer.Serialize (f a1)) of-        Dict -> do-          Cer.put (fromSing sa1)-          Cer.put x-  {-# INLINABLE get #-}-  get = do-    rsa1 <- Cer.get-    withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->-      case dict1 sa1 :: Dict (Cer.Serialize (f a1)) of-        Dict -> do-          x :: f a1 <- Cer.get-          pure (Some1 sa1 x)---- | Compatible with the 'Data.Bytes.Serial.Serial' instance and--- 'Data.Binary.Binary' instance, provided all of the 'DemoteRep's and the fully--- applied @f@ instances are compatible as well.-instance forall (f :: k2 -> k1 -> *).-  ( SingKind k2-  , SingKind k1-  , Cer.Serialize (DemoteRep k2)-  , Cer.Serialize (DemoteRep k1)-  , Dict2 Cer.Serialize f-  ) => Cer.Serialize (Some2 f) where-  {-# INLINABLE put #-}-  put = \some2x ->-    withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) ->-      case dict2 sa2 sa1 :: Dict (Cer.Serialize (f a2 a1)) of-        Dict -> do-          Cer.put (fromSing sa2, fromSing sa1)-          Cer.put x-  {-# INLINABLE get #-}-  get = do-    (rsa2, rsa1) <- Cer.get-    withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->-      withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->-        case dict2 sa2 sa1 :: Dict (Cer.Serialize (f a2 a1)) of-          Dict -> do-            x :: f a2 a1 <- Cer.get-            pure (Some2 sa2 sa1 x)---- | Compatible with the 'Data.Bytes.Serial.Serial' instance and--- 'Data.Binary.Binary' instance, provided all of the 'DemoteRep's and the fully--- applied @f@ instances are compatible as well.-instance forall (f :: k3 -> k2 -> k1 -> *).-  ( SingKind k3-  , SingKind k2-  , SingKind k1-  , Cer.Serialize (DemoteRep k3)-  , Cer.Serialize (DemoteRep k2)-  , Cer.Serialize (DemoteRep k1)-  , Dict3 Cer.Serialize f-  ) => Cer.Serialize (Some3 f) where-  {-# INLINABLE put #-}-  put = \some3x ->-    withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) ->-      case dict3 sa3 sa2 sa1 :: Dict (Cer.Serialize (f a3 a2 a1)) of-        Dict -> do-          Cer.put (fromSing sa3, fromSing sa2, fromSing sa1)-          Cer.put x-  {-# INLINABLE get #-}-  get = do-    (rsa3, rsa2, rsa1) <- Cer.get-    withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) ->-      withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->-        withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->-          case dict3 sa3 sa2 sa1 :: Dict (Cer.Serialize (f a3 a2 a1)) of-            Dict -> do-              x :: f a3 a2 a1 <- Cer.get-              pure (Some3 sa3 sa2 sa1 x)---- | Compatible with the 'Data.Bytes.Serial.Serial' instance and--- 'Data.Binary.Binary' instance, provided all of the 'DemoteRep's and the fully--- applied @f@ instances are compatible as well.-instance forall (f :: k4 -> k3 -> k2 -> k1 -> *).-  ( SingKind k4-  , SingKind k3-  , SingKind k2-  , SingKind k1-  , Cer.Serialize (DemoteRep k4)-  , Cer.Serialize (DemoteRep k3)-  , Cer.Serialize (DemoteRep k2)-  , Cer.Serialize (DemoteRep k1)-  , Dict4 Cer.Serialize f-  ) => Cer.Serialize (Some4 f) where-  {-# INLINABLE put #-}-  put = \some4x ->-    withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) ->-      case dict4 sa4 sa3 sa2 sa1 :: Dict (Cer.Serialize (f a4 a3 a2 a1)) of-        Dict -> do-          Cer.put (fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1)-          Cer.put x-  {-# INLINABLE get #-}-  get = do-    (rsa4, rsa3, rsa2, rsa1) <- Cer.get-    withSomeSing rsa4 $ \(sa4 :: Sing (a4 :: k4)) ->-      withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) ->-        withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) ->-          withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) ->-            case dict4 sa4 sa3 sa2 sa1 :: Dict (Cer.Serialize (f a4 a3 a2 a1)) of-              Dict -> do-                x :: f a4 a3 a2 a1 <- Cer.get-                pure (Some4 sa4 sa3 sa2 sa1 x)-
− src/lib/Exinst/Instances/DeepSeq.hs 
@@ -1,60 +0,0 @@-{-# 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 (f :: k1 -> *).-  ( Dict1 NFData f-  ) => NFData (Some1 f) where-  {-# INLINABLE rnf #-}-  rnf = \(!some1x) ->-    withSome1Sing some1x $ \ !sa1 !(x :: f a1) ->-       case dict1 sa1 :: Dict (NFData (f a1)) of-          Dict -> rnf x `seq` ()--instance forall (f :: k2 -> k1 -> *).-  ( Dict2 NFData f-  ) => NFData (Some2 f) where-  {-# INLINABLE rnf #-}-  rnf = \(!some2x) ->-    withSome2Sing some2x $ \ !sa2 !sa1 !(x :: f a2 a1) ->-       case dict2 sa2 sa1 :: Dict (NFData (f a2 a1)) of-          Dict -> rnf x `seq` ()--instance forall (f :: k3 -> k2 -> k1 -> *).-  ( Dict3 NFData f-  ) => NFData (Some3 f) where-  {-# INLINABLE rnf #-}-  rnf = \(!some3x) ->-    withSome3Sing some3x $ \ !sa3 !sa2 !sa1 !(x :: f a3 a2 a1) ->-       case dict3 sa3 sa2 sa1 :: Dict (NFData (f a3 a2 a1)) of-          Dict -> rnf x `seq` ()--instance forall (f :: k4 -> k3 -> k2 -> k1 -> *).-  ( Dict4 NFData f-  ) => NFData (Some4 f) where-  {-# INLINABLE rnf #-}-  rnf = \(!some4x) ->-    withSome4Sing some4x $ \ !(sa4) !sa3 !sa2 !sa1 !(x :: f a4 a3 a2 a1) ->-       case dict4 sa4 sa3 sa2 sa1 :: Dict (NFData (f a4 a3 a2 a1)) of-          Dict -> rnf x `seq` ()-
− src/lib/Exinst/Instances/Hashable.hs 
@@ -1,99 +0,0 @@-{-# 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 (f :: k1 -> *)-  . ( SingKind k1-    , Hashable (DemoteRep k1)-    , Dict1 Hashable f-    ) => Hashable (Some1 f)-  where-    {-# INLINABLE hashWithSalt #-}-    hashWithSalt salt some1x = withSome1Sing some1x $ \sa1 (x :: f a1) ->-       case dict1 sa1 :: Dict (Hashable (f a1)) of-          Dict -> salt `hashWithSalt` salt0-                       `hashWithSalt` fromSing sa1-                       `hashWithSalt` x--instance forall (f :: k2 -> k1 -> *)-  . ( SingKind k2-    , SingKind k1-    , Hashable (DemoteRep k2)-    , Hashable (DemoteRep k1)-    , Dict2 Hashable f-    ) => Hashable (Some2 f)-  where-    {-# INLINABLE hashWithSalt #-}-    hashWithSalt salt some2x = withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) ->-       case dict2 sa2 sa1 :: Dict (Hashable (f a2 a1)) of-          Dict -> salt `hashWithSalt` salt0-                       `hashWithSalt` fromSing sa2-                       `hashWithSalt` fromSing sa1-                       `hashWithSalt` x--instance forall (f :: k3 -> k2 -> k1 -> *)-  . ( SingKind k3-    , SingKind k2-    , SingKind k1-    , Hashable (DemoteRep k3)-    , Hashable (DemoteRep k2)-    , Hashable (DemoteRep k1)-    , Dict3 Hashable f-    ) => Hashable (Some3 f)-  where-    {-# INLINABLE hashWithSalt #-}-    hashWithSalt salt some3x = withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) ->-       case dict3 sa3 sa2 sa1 :: Dict (Hashable (f a3 a2 a1)) of-          Dict -> salt `hashWithSalt` salt0-                       `hashWithSalt` fromSing sa3-                       `hashWithSalt` fromSing sa2-                       `hashWithSalt` fromSing sa1-                       `hashWithSalt` x--instance forall (f :: 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 f-    ) => Hashable (Some4 f)-  where-    {-# INLINABLE hashWithSalt #-}-    hashWithSalt salt some4x = withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) ->-       case dict4 sa4 sa3 sa2 sa1 :: Dict (Hashable (f a4 a3 a2 a1)) of-          Dict -> salt `hashWithSalt` salt0-                       `hashWithSalt` fromSing sa4-                       `hashWithSalt` fromSing sa3-                       `hashWithSalt` fromSing sa2-                       `hashWithSalt` fromSing sa1-                       `hashWithSalt` x
− src/lib/Exinst/Instances/QuickCheck.hs 
@@ -1,106 +0,0 @@-{-# 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-
− src/lib/Exinst/Internal.hs 
@@ -1,361 +0,0 @@-{-# 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' #-}-
− src/lib/Exinst/Internal/Product.hs 
@@ -1,139 +0,0 @@-{-# LANGUAGE CPP #-}-{-# LANGUAGE DeriveGeneric #-}-{-# LANGUAGE PolyKinds #-}--module Exinst.Internal.Product- ( P1(P1)- , P2(P2)- , P3(P3)- , P4(P4)- ) where--import GHC.Generics (Generic)--#ifdef VERSION_aeson-import Data.Aeson (FromJSON, ToJSON)-#endif--#ifdef VERSION_binary-import qualified Data.Binary as Bin-#endif--#ifdef VERSION_bytes-import qualified Data.Bytes.Serial as By-#endif--#ifdef VERSION_cereal-import qualified Data.Serialize as Cer-#endif--#ifdef VERSION_deepseq-import Control.DeepSeq (NFData)-#endif--#ifdef VERSION_hashable-import Data.Hashable (Hashable)-#endif--#ifdef VERSION_QuickCheck-import qualified Test.QuickCheck as QC-#endif------------------------------------------------------------------------------------- Products---- | Like 'Data.Functor.Product.Product' from "Data.Functor.Product", but--- only intended to be used with kinds other than 'Type'.------ This type is particularly useful when used in combination with 'Exinst.Some1'--- as @'Exinst.Some1' ('P1' l r)@, so as to ensure that @l@ and @r@ are indexed--- by the same type. Moreover, 'P1' already supports many common instances from--- @base@, @hashable@, @deepseq@, @aeson@, @bytes@, @cereal@, @binary@, and--- @quickcheck@ out of the box, so you can benefit from them as well.-data P1 l r (a1 :: k1)-  = P1 (l a1) (r a1)-  deriving (Eq, Show, Read, Ord, Generic)---- | Like 'P1', but for @l@ and @r@ taking two type indexes.-data P2 l r (a2 :: k2) (a1 :: k1)-  = P2 (l a2 a1) (r a2 a1)-  deriving (Eq, Show, Read, Ord, Generic)---- | Like 'P1', but for @l@ and @r@ taking three type indexes.-data P3 l r (a3 :: k3) (a2 :: k2) (a1 :: k1)-  = P3 (l a3 a2 a1) (r a3 a2 a1)-  deriving (Eq, Show, Read, Ord, Generic)---- | Like 'P1', but for @l@ and @r@ taking four type indexes.-data P4 l r (a4 :: k4) (a3 :: k3) (a2 :: k2) (a1 :: k1)-  = P4 (l a4 a3 a2 a1) (r a4 a3 a2 a1)-  deriving (Eq, Show, Read, Ord, Generic)-----------------------------------------------------------------------------------#ifdef VERSION_hashable-instance (Hashable (l a1), Hashable (r a1)) => Hashable (P1 l r a1)-instance (Hashable (l a2 a1), Hashable (r a2 a1)) => Hashable (P2 l r a2 a1)-instance (Hashable (l a3 a2 a1), Hashable (r a3 a2 a1)) => Hashable (P3 l r a3 a2 a1)-instance (Hashable (l a4 a3 a2 a1), Hashable (r a4 a3 a2 a1)) => Hashable (P4 l r a4 a3 a2 a1)-#endif-----------------------------------------------------------------------------------#ifdef VERSION_deepseq-instance (NFData (l a1), NFData (r a1)) => NFData (P1 l r a1)-instance (NFData (l a2 a1), NFData (r a2 a1)) => NFData (P2 l r a2 a1)-instance (NFData (l a3 a2 a1), NFData (r a3 a2 a1)) => NFData (P3 l r a3 a2 a1)-instance (NFData (l a4 a3 a2 a1), NFData (r a4 a3 a2 a1)) => NFData (P4 l r a4 a3 a2 a1)-#endif-----------------------------------------------------------------------------------#ifdef VERSION_aeson-instance (FromJSON (l a1), FromJSON (r a1)) => FromJSON (P1 l r a1)-instance (FromJSON (l a2 a1), FromJSON (r a2 a1)) => FromJSON (P2 l r a2 a1)-instance (FromJSON (l a3 a2 a1), FromJSON (r a3 a2 a1)) => FromJSON (P3 l r a3 a2 a1)-instance (FromJSON (l a4 a3 a2 a1), FromJSON (r a4 a3 a2 a1)) => FromJSON (P4 l r a4 a3 a2 a1)--instance (ToJSON (l a1), ToJSON (r a1)) => ToJSON (P1 l r a1)-instance (ToJSON (l a2 a1), ToJSON (r a2 a1)) => ToJSON (P2 l r a2 a1)-instance (ToJSON (l a3 a2 a1), ToJSON (r a3 a2 a1)) => ToJSON (P3 l r a3 a2 a1)-instance (ToJSON (l a4 a3 a2 a1), ToJSON (r a4 a3 a2 a1)) => ToJSON (P4 l r a4 a3 a2 a1)-#endif-----------------------------------------------------------------------------------#ifdef VERSION_bytes-instance (By.Serial (l a1), By.Serial (r a1)) => By.Serial (P1 l r a1)-instance (By.Serial (l a2 a1), By.Serial (r a2 a1)) => By.Serial (P2 l r a2 a1)-instance (By.Serial (l a3 a2 a1), By.Serial (r a3 a2 a1)) => By.Serial (P3 l r a3 a2 a1)-instance (By.Serial (l a4 a3 a2 a1), By.Serial (r a4 a3 a2 a1)) => By.Serial (P4 l r a4 a3 a2 a1)-#endif-----------------------------------------------------------------------------------#ifdef VERSION_cereal-instance (Cer.Serialize (l a1), Cer.Serialize (r a1)) => Cer.Serialize (P1 l r a1)-instance (Cer.Serialize (l a2 a1), Cer.Serialize (r a2 a1)) => Cer.Serialize (P2 l r a2 a1)-instance (Cer.Serialize (l a3 a2 a1), Cer.Serialize (r a3 a2 a1)) => Cer.Serialize (P3 l r a3 a2 a1)-instance (Cer.Serialize (l a4 a3 a2 a1), Cer.Serialize (r a4 a3 a2 a1)) => Cer.Serialize (P4 l r a4 a3 a2 a1)-#endif-----------------------------------------------------------------------------------#ifdef VERSION_binary-instance (Bin.Binary (l a1), Bin.Binary (r a1)) => Bin.Binary (P1 l r a1)-instance (Bin.Binary (l a2 a1), Bin.Binary (r a2 a1)) => Bin.Binary (P2 l r a2 a1)-instance (Bin.Binary (l a3 a2 a1), Bin.Binary (r a3 a2 a1)) => Bin.Binary (P3 l r a3 a2 a1)-instance (Bin.Binary (l a4 a3 a2 a1), Bin.Binary (r a4 a3 a2 a1)) => Bin.Binary (P4 l r a4 a3 a2 a1)-#endif-----------------------------------------------------------------------------------#ifdef VERSION_QuickCheck-instance (QC.Arbitrary (l a1), QC.Arbitrary (r a1)) => QC.Arbitrary (P1 l r a1) where-  arbitrary = P1 <$> QC.arbitrary <*> QC.arbitrary-  shrink (P1 x y) = P1 <$> QC.shrink x <*> QC.shrink y-instance (QC.Arbitrary (l a2 a1), QC.Arbitrary (r a2 a1)) => QC.Arbitrary (P2 l r a2 a1) where-  arbitrary = P2 <$> QC.arbitrary <*> QC.arbitrary-  shrink (P2 x y) = P2 <$> QC.shrink x <*> QC.shrink y-instance (QC.Arbitrary (l a3 a2 a1), QC.Arbitrary (r a3 a2 a1)) => QC.Arbitrary (P3 l r a3 a2 a1) where-  arbitrary = P3 <$> QC.arbitrary <*> QC.arbitrary-  shrink (P3 x y) = P3 <$> QC.shrink x <*> QC.shrink y-instance (QC.Arbitrary (l a4 a3 a2 a1), QC.Arbitrary (r a4 a3 a2 a1)) => QC.Arbitrary (P4 l r a4 a3 a2 a1) where-  arbitrary = P4 <$> QC.arbitrary <*> QC.arbitrary-  shrink (P4 x y) = P4 <$> QC.shrink x <*> QC.shrink y-#endif
− src/lib/Exinst/Internal/Sum.hs 
@@ -1,143 +0,0 @@-{-# LANGUAGE CPP #-}-{-# LANGUAGE DeriveGeneric #-}-{-# LANGUAGE PolyKinds #-}--module Exinst.Internal.Sum- ( S1(S1L,S1R)- , S2(S2L,S2R)- , S3(S3L,S3R)- , S4(S4L,S4R)- ) where--import GHC.Generics (Generic)--#ifdef VERSION_aeson-import Data.Aeson (FromJSON, ToJSON)-#endif--#ifdef VERSION_binary-import qualified Data.Binary as Bin-#endif--#ifdef VERSION_bytes-import qualified Data.Bytes.Serial as By-#endif--#ifdef VERSION_cereal-import qualified Data.Serialize as Cer-#endif--#ifdef VERSION_deepseq-import Control.DeepSeq (NFData)-#endif--#ifdef VERSION_hashable-import Data.Hashable (Hashable)-#endif--#ifdef VERSION_QuickCheck-import qualified Test.QuickCheck as QC-#endif------------------------------------------------------------------------------------- Sums---- | Like 'Data.Functor.Sum.Sum' from "Data.Functor.Sum", but--- only intended to be used with kinds other than 'Type'.------ This type is particularly useful when used in combination with 'Exinst.Some1'--- as @'Exinst.Some1' ('S1' l r)@, so as to ensure that @l@ and @r@ are indexed--- by the same type. Moreover, 'S1' already supports many common instances from--- @base@, @hashable@, @deepseq@, @aeson@, @bytes@, @cereal@, @binary@, and--- @quickcheck@ out of the box, so you can benefit from them as well.-data S1 l r (a1 :: k1)-  = S1L (l a1) | S1R (r a1)-  deriving (Eq, Show, Read, Ord, Generic)---- | Like 'S1', but for @l@ and @r@ taking two type indexes.-data S2 l r (a2 :: k2) (a1 :: k1)-  = S2L (l a2 a1) | S2R (r a2 a1)-  deriving (Eq, Show, Read, Ord, Generic)---- | Like 'S1', but for @l@ and @r@ taking three type indexes.-data S3 l r (a3 :: k3) (a2 :: k2) (a1 :: k1)-  = S3L (l a3 a2 a1) | S3R (r a3 a2 a1)-  deriving (Eq, Show, Read, Ord, Generic)---- | Like 'S1', but for @l@ and @r@ taking four type indexes.-data S4 l r (a4 :: k4) (a3 :: k3) (a2 :: k2) (a1 :: k1)-  = S4L (l a4 a3 a2 a1) | S4R (r a4 a3 a2 a1)-  deriving (Eq, Show, Read, Ord, Generic)-----------------------------------------------------------------------------------#ifdef VERSION_hashable-instance (Hashable (l a1), Hashable (r a1)) => Hashable (S1 l r a1)-instance (Hashable (l a2 a1), Hashable (r a2 a1)) => Hashable (S2 l r a2 a1)-instance (Hashable (l a3 a2 a1), Hashable (r a3 a2 a1)) => Hashable (S3 l r a3 a2 a1)-instance (Hashable (l a4 a3 a2 a1), Hashable (r a4 a3 a2 a1)) => Hashable (S4 l r a4 a3 a2 a1)-#endif-----------------------------------------------------------------------------------#ifdef VERSION_deepseq-instance (NFData (l a1), NFData (r a1)) => NFData (S1 l r a1)-instance (NFData (l a2 a1), NFData (r a2 a1)) => NFData (S2 l r a2 a1)-instance (NFData (l a3 a2 a1), NFData (r a3 a2 a1)) => NFData (S3 l r a3 a2 a1)-instance (NFData (l a4 a3 a2 a1), NFData (r a4 a3 a2 a1)) => NFData (S4 l r a4 a3 a2 a1)-#endif-----------------------------------------------------------------------------------#ifdef VERSION_aeson-instance (FromJSON (l a1), FromJSON (r a1)) => FromJSON (S1 l r a1)-instance (FromJSON (l a2 a1), FromJSON (r a2 a1)) => FromJSON (S2 l r a2 a1)-instance (FromJSON (l a3 a2 a1), FromJSON (r a3 a2 a1)) => FromJSON (S3 l r a3 a2 a1)-instance (FromJSON (l a4 a3 a2 a1), FromJSON (r a4 a3 a2 a1)) => FromJSON (S4 l r a4 a3 a2 a1)--instance (ToJSON (l a1), ToJSON (r a1)) => ToJSON (S1 l r a1)-instance (ToJSON (l a2 a1), ToJSON (r a2 a1)) => ToJSON (S2 l r a2 a1)-instance (ToJSON (l a3 a2 a1), ToJSON (r a3 a2 a1)) => ToJSON (S3 l r a3 a2 a1)-instance (ToJSON (l a4 a3 a2 a1), ToJSON (r a4 a3 a2 a1)) => ToJSON (S4 l r a4 a3 a2 a1)-#endif-----------------------------------------------------------------------------------#ifdef VERSION_bytes-instance (By.Serial (l a1), By.Serial (r a1)) => By.Serial (S1 l r a1)-instance (By.Serial (l a2 a1), By.Serial (r a2 a1)) => By.Serial (S2 l r a2 a1)-instance (By.Serial (l a3 a2 a1), By.Serial (r a3 a2 a1)) => By.Serial (S3 l r a3 a2 a1)-instance (By.Serial (l a4 a3 a2 a1), By.Serial (r a4 a3 a2 a1)) => By.Serial (S4 l r a4 a3 a2 a1)-#endif-----------------------------------------------------------------------------------#ifdef VERSION_cereal-instance (Cer.Serialize (l a1), Cer.Serialize (r a1)) => Cer.Serialize (S1 l r a1)-instance (Cer.Serialize (l a2 a1), Cer.Serialize (r a2 a1)) => Cer.Serialize (S2 l r a2 a1)-instance (Cer.Serialize (l a3 a2 a1), Cer.Serialize (r a3 a2 a1)) => Cer.Serialize (S3 l r a3 a2 a1)-instance (Cer.Serialize (l a4 a3 a2 a1), Cer.Serialize (r a4 a3 a2 a1)) => Cer.Serialize (S4 l r a4 a3 a2 a1)-#endif-----------------------------------------------------------------------------------#ifdef VERSION_binary-instance (Bin.Binary (l a1), Bin.Binary (r a1)) => Bin.Binary (S1 l r a1)-instance (Bin.Binary (l a2 a1), Bin.Binary (r a2 a1)) => Bin.Binary (S2 l r a2 a1)-instance (Bin.Binary (l a3 a2 a1), Bin.Binary (r a3 a2 a1)) => Bin.Binary (S3 l r a3 a2 a1)-instance (Bin.Binary (l a4 a3 a2 a1), Bin.Binary (r a4 a3 a2 a1)) => Bin.Binary (S4 l r a4 a3 a2 a1)-#endif-----------------------------------------------------------------------------------#ifdef VERSION_QuickCheck-instance (QC.Arbitrary (l a1), QC.Arbitrary (r a1)) => QC.Arbitrary (S1 l r a1) where-  arbitrary = QC.oneof [ fmap S1L QC.arbitrary, fmap S1R QC.arbitrary ]-  shrink (S1L l) = S1L <$> QC.shrink l-  shrink (S1R r) = S1R <$> QC.shrink r-instance (QC.Arbitrary (l a2 a1), QC.Arbitrary (r a2 a1)) => QC.Arbitrary (S2 l r a2 a1) where-  arbitrary = QC.oneof [ fmap S2L QC.arbitrary, fmap S2R QC.arbitrary ]-  shrink (S2L l) = S2L <$> QC.shrink l-  shrink (S2R r) = S2R <$> QC.shrink r-instance (QC.Arbitrary (l a3 a2 a1), QC.Arbitrary (r a3 a2 a1)) => QC.Arbitrary (S3 l r a3 a2 a1) where-  arbitrary = QC.oneof [ fmap S3L QC.arbitrary, fmap S3R QC.arbitrary ]-  shrink (S3L l) = S3L <$> QC.shrink l-  shrink (S3R r) = S3R <$> QC.shrink r-instance (QC.Arbitrary (l a4 a3 a2 a1), QC.Arbitrary (r a4 a3 a2 a1)) => QC.Arbitrary (S4 l r a4 a3 a2 a1) where-  arbitrary = QC.oneof [ fmap S4L QC.arbitrary, fmap S4R QC.arbitrary ]-  shrink (S4L l) = S4L <$> QC.shrink l-  shrink (S4R r) = S4R <$> QC.shrink r-#endif
tests/Main.hs view
@@ -9,6 +9,7 @@ module Main where  import Control.DeepSeq (NFData(rnf))+import qualified Codec.Serialise as Cborg import qualified Data.Aeson as Aeson import qualified Data.Binary as Bin import qualified Data.ByteString.Lazy as BSL@@ -27,7 +28,7 @@ import qualified Test.Tasty.QuickCheck as QC import Text.Read (readMaybe) -import Data.Singletons (SingKind, Sing, DemoteRep, withSomeSing)+import Data.Singletons (SingKind, Sing, Demote, withSomeSing)  import Exinst @@ -50,6 +51,7 @@   , tt_id "Identity through Bytes's Serial" id_bytes   , tt_id "Identity through Cereal's Serialize" id_cereal   , tt_id "Identity through Binary's Binary" id_binary+  , tt_id "Identity through serialise's Serialise" id_serialise   , tt_id "Identity from Cereal's Serialize to Binary's Binary" id_cereal_to_binary   , tt_id "Identity from Cereal's Serialize to Bytes's Serial" id_cereal_to_bytes   , tt_id "Identity from Binary's Binary to Cereal's Serialize" id_binary_to_cereal@@ -64,7 +66,7 @@   -> (forall a.         ( G.Generic a, Aeson.FromJSON a, Aeson.ToJSON a         , Bytes.Serial a, Bin.Binary a, Cer.Serialize a-        , Show a, Read a+        , Cborg.Serialise a, Show a, Read a         ) => a -> Maybe a      ) -- ^ It's easier to put all the constraints here.   -> Tasty.TestTree@@ -180,6 +182,12 @@      Right a' -> Just a'      Left _ -> Nothing +id_serialise :: Cborg.Serialise a => a -> Maybe a+id_serialise = \a ->+  case Cborg.deserialiseOrFail (Cborg.serialise a) of+    Right a' -> Just a'+    Left _   -> Nothing+ id_cereal_to_binary :: (Bin.Binary a, Cer.Serialize a) => a -> Maybe a id_cereal_to_binary = \a ->    case Bin.decodeOrFail (Cer.encodeLazy a) of@@ -219,42 +227,42 @@ --------------------------------------------------------------------------------  data family X1 :: Bool -> Type-data instance X1 'False = XF1 | XF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable)-data instance X1 'True = XT1 | XT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable)+data instance X1 'False = XF1 | XF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable)+data instance X1 'True = XT1 | XT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable)  data family X2 :: Bool -> Bool -> Type-data instance X2 'False 'False = XFF1 | XFF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable)-data instance X2 'False 'True = XFT1 | XFT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable)-data instance X2 'True 'False = XTF1 | XTF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable)-data instance X2 'True 'True = XTT1 | XTT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable)+data instance X2 'False 'False = XFF1 | XFF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable)+data instance X2 'False 'True = XFT1 | XFT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable)+data instance X2 'True 'False = XTF1 | XTF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable)+data instance X2 'True 'True = XTT1 | XTT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable)  data family X3 :: Bool -> Bool -> Bool -> Type-data instance X3 'False 'False 'False = XFFF1 | XFFF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable)-data instance X3 'False 'False 'True = XFFT1 | XFFT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable)-data instance X3 'False 'True 'False = XFTF1 | XFTF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable)-data instance X3 'False 'True 'True = XFTT1 | XFTT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable)-data instance X3 'True 'False 'False = XTFF1 | XTFF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable)-data instance X3 'True 'False 'True = XTFT1 | XTFT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable)-data instance X3 'True 'True 'False = XTTF1 | XTTF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable)-data instance X3 'True 'True 'True = XTTT1 | XTTT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable)+data instance X3 'False 'False 'False = XFFF1 | XFFF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable)+data instance X3 'False 'False 'True = XFFT1 | XFFT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable)+data instance X3 'False 'True 'False = XFTF1 | XFTF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable)+data instance X3 'False 'True 'True = XFTT1 | XFTT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable)+data instance X3 'True 'False 'False = XTFF1 | XTFF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable)+data instance X3 'True 'False 'True = XTFT1 | XTFT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable)+data instance X3 'True 'True 'False = XTTF1 | XTTF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable)+data instance X3 'True 'True 'True = XTTT1 | XTTT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable)  data family X4 :: Bool -> Bool -> Bool -> Bool -> Type-data instance X4 'False 'False 'False 'False = XFFFF1 | XFFFF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable)-data instance X4 'False 'False 'False 'True = XFFFT1 | XFFFT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable)-data instance X4 'False 'False 'True 'False = XFFTF1 | XFFTF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable)-data instance X4 'False 'False 'True 'True = XFFTT1 | XFFTT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable)-data instance X4 'False 'True 'False 'False = XFTFF1 | XFTFF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable)-data instance X4 'False 'True 'False 'True = XFTFT1 | XFTFT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable)-data instance X4 'False 'True 'True 'False = XFTTF1 | XFTTF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable)-data instance X4 'False 'True 'True 'True = XFTTT1 | XFTTT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable)-data instance X4 'True 'False 'False 'False = XTFFF1 | XTFFF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable)-data instance X4 'True 'False 'False 'True = XTFFT1 | XTFFT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable)-data instance X4 'True 'False 'True 'False = XTFTF1 | XTFTF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable)-data instance X4 'True 'False 'True 'True = XTFTT1 | XTFTT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable)-data instance X4 'True 'True 'False 'False = XTTFF1 | XTTFF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable)-data instance X4 'True 'True 'False 'True = XTTFT1 | XTTFT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable)-data instance X4 'True 'True 'True 'False = XTTTF1 | XTTTF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable)-data instance X4 'True 'True 'True 'True = XTTTT1 | XTTTT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable)+data instance X4 'False 'False 'False 'False = XFFFF1 | XFFFF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable)+data instance X4 'False 'False 'False 'True = XFFFT1 | XFFFT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable)+data instance X4 'False 'False 'True 'False = XFFTF1 | XFFTF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable)+data instance X4 'False 'False 'True 'True = XFFTT1 | XFFTT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable)+data instance X4 'False 'True 'False 'False = XFTFF1 | XFTFF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable)+data instance X4 'False 'True 'False 'True = XFTFT1 | XFTFT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable)+data instance X4 'False 'True 'True 'False = XFTTF1 | XFTTF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable)+data instance X4 'False 'True 'True 'True = XFTTT1 | XFTTT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable)+data instance X4 'True 'False 'False 'False = XTFFF1 | XTFFF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable)+data instance X4 'True 'False 'False 'True = XTFFT1 | XTFFT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable)+data instance X4 'True 'False 'True 'False = XTFTF1 | XTFTF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable)+data instance X4 'True 'False 'True 'True = XTFTT1 | XTFTT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable)+data instance X4 'True 'True 'False 'False = XTTFF1 | XTTFF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable)+data instance X4 'True 'True 'False 'True = XTTFT1 | XTTFT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable)+data instance X4 'True 'True 'True 'False = XTTTF1 | XTTTF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable)+data instance X4 'True 'True 'True 'True = XTTTT1 | XTTTT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable)  -------------------------------------------------------------------------------- -- Arbitrary instances