packages feed

exinst 0.6 → 0.7

raw patch · 22 files changed

+1208/−2043 lines, 22 filesdep +exinstdep −aesondep −bytesdep −cborgsetup-changedPVP ok

version bump matches the API change (PVP)

Dependencies added: exinst

Dependencies removed: aeson, bytes, cborg, cereal, serialise

API changes (from Hackage documentation)

- Exinst: class SingI k (a :: k)
+ Exinst: class SingI (a :: k)
- Exinst: data Constraint :: *
+ Exinst: data Constraint
- Exinst: data Dict a :: Constraint -> *
+ Exinst: data Dict a

Files

CHANGELOG.md view
@@ -1,3 +1,14 @@+# Version 0.7++* BACKWARDS COMPATIBLE COMPILER ASSISTED CHANGE: All of the cabal flags+  for turning on and off instances were removed.  The `hashable` are now+  always exported from the `exinst`, and the `aeson`, `bytes`,+  `cereal` and `serialise` instances  are now exported from new+  packages `exinst-aeson`, `exinst-bytes`, `exinst-cereal` and+  `exinst-serialise`. The instances exported from those packages are+  the same as the ones exported with `exinst-0.6`.++ # Version 0.6  * The `binary` and `deepseq` Cabal flags were removed since these two packages
README.md view
@@ -1,11 +1,9 @@ # exinst -[![Build Status](https://travis-ci.org/k0001/exinst.svg?branch=master)](https://travis-ci.org/k0001/exinst)--See the [BSD3 LICENSE](https://github.com/k0001/exinst/blob/master/exinst/LICENSE.txt)+See the [BSD3 LICENSE](https://github.com/k0001/exinst/blob/master/exinst/exinst/LICENSE.txt) file to learn about the legal terms and conditions for this library.  Find documentation for this library in the top-level-[`Exinst`](https://github.com/k0001/exinst/blob/master/exinst/src/lib/Exinst.hs)+[`Exinst`](https://github.com/k0001/exinst/blob/master/exinst/lib/Exinst.hs) module. 
Setup.hs view
@@ -1,4 +1,2 @@-#! /usr/bin/env nix-shell-#! nix-shell ./shell.nix -i runghc import Distribution.Simple main = defaultMain
exinst.cabal view
@@ -1,5 +1,5 @@ name:                exinst-version:             0.6+version:             0.7 author:              Renzo Carbonara maintainer:          renzoλcarbonara.com.ar copyright:           Renzo Carbonara 2015-2018@@ -23,48 +23,40 @@       Exinst.Internal       Exinst.Internal.Product       Exinst.Internal.Sum-      Exinst.Instances.Base-      Exinst.Instances.Binary-      Exinst.Instances.DeepSeq+      Exinst.Base+      Exinst.Binary+      Exinst.DeepSeq+      Exinst.Hashable+      Exinst.QuickCheck   build-depends:       base >=4.9 && <5.0     , binary     , constraints >=0.4     , deepseq+    , hashable     , profunctors >=5.0     , singletons >=2.3.1+    , QuickCheck   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(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(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+--  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(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 lib+  hs-source-dirs: tests   main-is: Main.hs   build-depends:      base@@ -72,6 +64,8 @@    , bytestring    , constraints    , deepseq+   , exinst+   , hashable    , profunctors    , QuickCheck    , singletons@@ -80,45 +74,38 @@    , tasty-quickcheck   ghcjs-options: -Wall -O0   ghc-options: -Wall -O0-  cpp-options:-    -DHAS_quickcheck-  if flag(aeson)-    build-depends: aeson-    cpp-options: -DHAS_aeson-  if flag(bytes)-    build-depends: bytes-    cpp-options: -DHAS_bytes-  if flag(cereal) || flag(bytes)-    build-depends: cereal-    cpp-options: -DHAS_cereal-  if flag(hashable)-    build-depends: hashable-    cpp-options: -DHAS_hashable-  if flag(serialise)-    build-depends: cborg, serialise-    cpp-options: -DHAS_serialise--flag aeson-  description: Provide instances for @aeson@-  default: True-  manual: True-flag bytes-  description: Provide instances for @bytes@ (implies @ceral@ and @binary@).-  default: True-  manual: True-flag cereal-  description: Provide instances for @cereal@.-  default: True-  manual: True-flag hashable-  description: Provide instances for @hashable@-  default: True-  manual: True-flag quickcheck-  description: Provide instances for @QuickCheck@-  default: True-  manual: True-flag serialise-  description: Provide instances for @serialise@-  default: True-  manual: True+--   cpp-options:+--     -DHAS_quickcheck+--   if flag(bytes)+--     build-depends: bytes+--     cpp-options: -DHAS_bytes+--   if flag(cereal) || flag(bytes)+--     build-depends: cereal+--     cpp-options: -DHAS_cereal+--   if flag(hashable)+--     build-depends: hashable+--     cpp-options: -DHAS_hashable+--   if flag(serialise)+--     build-depends: cborg, serialise+--     cpp-options: -DHAS_serialise+--+-- flag bytes+--   description: Provide instances for @bytes@ (implies @ceral@ and @binary@).+--   default: True+--   manual: True+-- flag cereal+--   description: Provide instances for @cereal@.+--   default: True+--   manual: True+-- flag hashable+--   description: Provide instances for @hashable@+--   default: True+--   manual: True+-- flag quickcheck+--   description: Provide instances for @QuickCheck@+--   default: True+--   manual: True+-- flag serialise+--   description: Provide instances for @serialise@+--   default: True+--   manual: True
lib/Exinst.hs view
@@ -117,34 +117,11 @@ import Exinst.Internal.Product import Exinst.Internal.Sum -import Exinst.Instances.Base ()-import Exinst.Instances.Binary ()-import Exinst.Instances.DeepSeq ()--#ifdef HAS_aeson-import Exinst.Instances.Aeson ()-#endif--#ifdef HAS_bytes-import Exinst.Instances.Bytes ()-#endif--#ifdef HAS_cereal-import Exinst.Instances.Cereal ()-#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-+import Exinst.Base ()+import Exinst.Binary ()+import Exinst.DeepSeq ()+import Exinst.Hashable ()+import Exinst.QuickCheck ()  {- $motivation @@ -404,12 +381,6 @@  * '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.@@ -417,6 +388,23 @@ * 'Control.DeepSeq.NFData' from the @deepseq@ package.  * 'Test.QuickCheck.Arbitrary' from the @QuickCheck@ package.++Furthermore, other libraries export other orphan instances for the datatypes+exported by 'exinst':++* [exinst-aeson](https://hackage.haskell.org/package/exinst-aeson) exports+instances for 'Data.Aeson.FromJSON' and 'Data.Aeson.ToJSON' from the @aeson@+package.++* [exinst-bytes](https://hackage.haskell.org/package/exinst-bytes) exports+instances for 'Data.Bytes.Serial' from the @bytes@ package.++* [exinst-cereal](https://hackage.haskell.org/package/exinst-cereal) exports+instances for 'Cereal.Serialize.Serialize' from the @cereal@ package.++* [exinst-serialise](https://hackage.haskell.org/package/exinst-serialise)+exports instances for 'Codec.Serialise.Serialise' from the @serialise@ 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
+ lib/Exinst/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.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/Binary.hs view
@@ -0,0 +1,155 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeInType #-}+{-# 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.Binary () where++import qualified Data.Binary as Bin+import Data.Constraint+import Data.Kind (Type)+import Data.Singletons+import Prelude++import Exinst.Internal+import Exinst.Internal.Sum+import Exinst.Internal.Product++--------------------------------------------------------------------------------++-- | 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 -> Type).+  ( 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 -> Type).+  ( 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 -> Type).+  ( 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 -> Type).+  ( 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)++--------------------------------------------------------------------------------++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)++--------------------------------------------------------------------------------++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)
+ lib/Exinst/DeepSeq.hs view
@@ -0,0 +1,76 @@+{-# 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.DeepSeq () where++import Control.DeepSeq (NFData(rnf))+import Data.Constraint+import Prelude++import Exinst.Internal+import Exinst.Internal.Sum+import Exinst.Internal.Product++--------------------------------------------------------------------------------++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` ()++--------------------------------------------------------------------------------++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)++--------------------------------------------------------------------------------++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)+
+ lib/Exinst/Hashable.hs view
@@ -0,0 +1,118 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeInType #-}+{-# 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.Hashable () where++import Data.Hashable (Hashable(hashWithSalt))+import Data.Constraint+import Data.Kind (Type)+import Data.Singletons+import Prelude++import Exinst.Internal+import Exinst.Internal.Sum+import Exinst.Internal.Product++--------------------------------------------------------------------------------++-- | Some salt we add to hashes calculated in this module.+salt0 :: Int+salt0 = 6700417++--------------------------------------------------------------------------------++instance forall (f :: k1 -> Type)+  . ( 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 -> Type)+  . ( 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 -> Type)+  . ( 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 -> Type)+  . ( 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++--------------------------------------------------------------------------------++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)++--------------------------------------------------------------------------------++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)+
− lib/Exinst/Instances/Aeson.hs
@@ -1,161 +0,0 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeInType #-}-{-# 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.Kind (Type)-import Data.Singletons-import Prelude--import Exinst.Internal------------------------------------------------------------------------------------instance forall (f :: k1 -> Type)-  . ( 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 -> Type)-  . ( 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 -> Type)-  . ( 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 -> Type)-  . ( 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 -> Type)-  . ( 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 -> Type)-  . ( 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 -> Type)-  . ( 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 -> Type)-  . ( 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
@@ -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 (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
@@ -1,139 +0,0 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeInType #-}-{-# 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.Kind (Type)-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 -> Type).-  ( 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 -> Type).-  ( 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 -> Type).-  ( 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 -> Type).-  ( 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
@@ -1,140 +0,0 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeInType #-}-{-# 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.Kind (Type)-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 -> Type).-  ( 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 -> Type).-  ( 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 -> Type).-  ( 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 -> Type).-  ( 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
@@ -1,140 +0,0 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeInType #-}-{-# 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.Kind (Type)-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 -> Type).-  ( 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 -> Type).-  ( 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 -> Type).-  ( 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 -> Type).-  ( 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
@@ -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` ()-
− lib/Exinst/Instances/Hashable.hs
@@ -1,101 +0,0 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeInType #-}-{-# 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.Kind (Type)-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 -> Type)-  . ( 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 -> Type)-  . ( 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 -> Type)-  . ( 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 -> Type)-  . ( 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
@@ -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, 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
@@ -1,127 +0,0 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeInType #-}-{-# 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.Kind (Type)-import Data.Singletons-import Prelude--import Exinst.Internal------------------------------------------------------------------------------------instance forall (f :: k1 -> Type)-  . ( 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 -> Type)-  . ( 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 -> Type)-  . ( 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 -> Type)-  . ( 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/Product.hs view
@@ -1,4 +1,3 @@-{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE PolyKinds #-} @@ -9,35 +8,8 @@  , P4(P4)  ) where -import Control.DeepSeq (NFData)-import qualified Data.Binary as Bin import GHC.Generics (Generic) -#ifdef HAS_aeson-import Data.Aeson (FromJSON, ToJSON)-#endif--#ifdef HAS_bytes-import qualified Data.Bytes.Serial as By-#endif--#ifdef HAS_cereal-import qualified Data.Serialize as Cer-#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 @@ -67,76 +39,3 @@ 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-----------------------------------------------------------------------------------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)-----------------------------------------------------------------------------------#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-----------------------------------------------------------------------------------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)-----------------------------------------------------------------------------------#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
@@ -1,4 +1,3 @@-{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE PolyKinds #-} @@ -9,34 +8,8 @@  , S4(S4L,S4R)  ) where -import Control.DeepSeq (NFData)-import qualified Data.Binary as Bin import GHC.Generics (Generic) -#ifdef HAS_aeson-import Data.Aeson (FromJSON, ToJSON)-#endif--#ifdef HAS_bytes-import qualified Data.Bytes.Serial as By-#endif--#ifdef HAS_cereal-import qualified Data.Serialize as Cer-#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 @@ -67,79 +40,3 @@   = 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-----------------------------------------------------------------------------------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)-----------------------------------------------------------------------------------#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-----------------------------------------------------------------------------------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)-----------------------------------------------------------------------------------#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
+ lib/Exinst/QuickCheck.hs view
@@ -0,0 +1,142 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE UndecidableInstances #-}++{-# 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.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+import Exinst.Internal.Sum+import Exinst.Internal.Product++--------------------------------------------------------------------------------++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++--------------------------------------------------------------------------------++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++--------------------------------------------------------------------------------++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
tests/Main.hs view
@@ -13,6 +13,7 @@ import Control.DeepSeq (NFData(rnf)) import qualified Data.Binary as Bin import qualified Data.ByteString.Lazy as BSL+import Data.Hashable (Hashable(hash)) import Data.Int (Int32) import Data.Kind (Type) import qualified GHC.Generics as G@@ -22,28 +23,6 @@ import qualified Test.Tasty.QuickCheck as QC import Text.Read (readMaybe) -#ifdef HAS_aeson-import qualified Data.Aeson as Aeson-#endif--#ifdef HAS_bytes-import qualified Data.Bytes.Get as Bytes-import qualified Data.Bytes.Put as Bytes-import qualified Data.Bytes.Serial as Bytes-#endif--#ifdef HAS_cereal-import qualified Data.Serialize as Cer-#endif--#ifdef HAS_hashable-import Data.Hashable (Hashable(hash))-#endif--#ifdef HAS_serialise-import qualified Codec.Serialise as Cborg-#endif- import Exinst  --------------------------------------------------------------------------------@@ -172,50 +151,14 @@   , tt_id "Identity through Show/Read" id_show_read   , tt_id "Identity through GHC's Generic" id_generic   , tt_id "Identity through Binary's Binary" id_binary--#ifdef HAS_aeson-  , tt_id "Identity through Aeson's ToJSON/FromJSON" id_aeson-#endif--#ifdef HAS_bytes-  , tt_id "Identity through Bytes's Serial" id_bytes-  , tt_id "Identity from Binary's Binary to Bytes's Serial" id_binary_to_bytes-  , tt_id "Identity from Bytes's Serial to Binary's Binary" id_bytes_to_binary-#ifdef HAS_cereal-  , tt_id "Identity from Cereal's Serialize to Bytes's Serial" id_cereal_to_bytes-  , tt_id "Identity from Bytes's Serial to Cereal's Serialize" id_bytes_to_cereal-#endif-#endif--#ifdef HAS_cereal-  , tt_id "Identity through Cereal's Serialize" id_cereal-  , tt_id "Identity from Binary's Binary to Cereal's Serialize" id_binary_to_cereal-  , tt_id "Identity from Cereal's Serialize to Binary's Binary" id_cereal_to_binary-#endif--#ifdef HAS_serialise-  , tt_id "Identity through serialise's Serialise" id_serialise-#endif   ]  type MegaCtx a =   ( G.Generic a   , Show a   , Read a+  , Hashable a   , Bin.Binary a-#ifdef HAS_aeson-  , Aeson.FromJSON a-  , Aeson.ToJSON a-#endif-#ifdef HAS_bytes-  , Bytes.Serial a-#endif-#ifdef HAS_cereal-  , Cer.Serialize a-#endif-#ifdef HAS_serialise-  , Cborg.Serialise a-#endif   )  tt_id@@ -278,7 +221,6 @@       QC.forAll QC.arbitrary $ \(x :: Some4 (S4 X4 X4)) -> () === rnf x   ] -#ifdef HAS_hashable INSTANCETRON(Hashable)  tt_hashable :: Tasty.TestTree@@ -308,7 +250,6 @@   , QC.testProperty "Some4 (S4 X4 X4)" $       QC.forAll QC.arbitrary $ \(x :: Some4 (S4 X4 X4)) -> () === (hash x `seq` ())   ]-#endif  -------------------------------------------------------------------------------- @@ -318,80 +259,9 @@ id_generic :: G.Generic a => a -> Maybe a id_generic = Just . G.to . G.from -#ifdef HAS_aeson-INSTANCETRON(Aeson.ToJSON)-INSTANCETRON(Aeson.FromJSON)-id_aeson :: (Aeson.FromJSON a, Aeson.ToJSON a) => a -> Maybe a-id_aeson = Aeson.decode . Aeson.encode-#endif--#ifdef HAS_bytes-INSTANCETRON(Bytes.Serial)-id_bytes :: Bytes.Serial a => a -> Maybe a-id_bytes = \a ->-  case Bytes.runGetS Bytes.deserialize (Bytes.runPutS (Bytes.serialize a)) of-     Left _ -> Nothing-     Right a' -> Just a'--id_binary_to_bytes :: (Bin.Binary a, Bytes.Serial a) => a -> Maybe a-id_binary_to_bytes = \a ->-   case Bytes.runGetS Bytes.deserialize (BSL.toStrict (Bin.encode a)) of-     Left _ -> Nothing-     Right a' -> Just a'--id_bytes_to_binary :: (Bytes.Serial a, Bin.Binary a) => a -> Maybe a-id_bytes_to_binary = \a ->-   case Bin.decodeOrFail (Bytes.runPutL (Bytes.serialize a)) of-      Right (z,_,a') | BSL.null z -> Just a'-      _ -> Nothing-#endif- id_binary :: Bin.Binary a => a -> Maybe a id_binary = \a ->   case Bin.decodeOrFail (Bin.encode a) of       Right (z,_,a') | BSL.null z -> Just a'       _ -> Nothing -#ifdef HAS_cereal-INSTANCETRON(Cer.Serialize)-id_cereal :: Cer.Serialize a => a -> Maybe a-id_cereal = \a ->-  case Cer.decodeLazy (Cer.encodeLazy a) of-     Right a' -> Just a'-     Left _ -> Nothing--id_binary_to_cereal :: (Bin.Binary a, Cer.Serialize a) => a -> Maybe a-id_binary_to_cereal = \a ->-  case Cer.decodeLazy (Bin.encode 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-      Right (z,_,a') | BSL.null z -> Just a'-      _ -> Nothing--#ifdef HAS_bytes-id_cereal_to_bytes :: (Cer.Serialize a, Bytes.Serial a) => a -> Maybe a-id_cereal_to_bytes = \a ->-   case Bytes.runGetS Bytes.deserialize (Cer.encode a) of-     Left _ -> Nothing-     Right a' -> Just a'--id_bytes_to_cereal :: (Bytes.Serial a, Cer.Serialize a) => a -> Maybe a-id_bytes_to_cereal = \a ->-  case Cer.decodeLazy (Bytes.runPutL (Bytes.serialize a)) of-     Right a' -> Just a'-     Left _ -> Nothing-#endif-#endif--#ifdef HAS_serialise-INSTANCETRON(Cborg.Serialise)-id_serialise :: Cborg.Serialise a => a -> Maybe a-id_serialise = \a ->-  case Cborg.deserialiseOrFail (Cborg.serialise a) of-    Right a' -> Just a'-    Left _   -> Nothing-#endif