exinst-base (empty) → 0.9

raw patch · 6 files changed

+978/−0 lines, 6 filesdep +QuickCheckdep +basedep +binary

Dependencies added: QuickCheck, base, binary, bytestring, constraints, deepseq, exinst, exinst-base, hashable, singletons, singletons-base, tasty, tasty-quickcheck

Files

CHANGELOG.md +6/−0
LICENSE.txt +30/−0
README.md +6/−0
exinst-base.cabal +47/−0
lib/Exinst/Base.hs +621/−0
tests/Main.hs +268/−0

+ CHANGELOG.md view

@@ -0,0 +1,6 @@+# Version 0.9++* Builds with GHC 9.4.++* This library exports the `Show`, `Read`, `Eq` `Ord` and `Generic`+  instances previously exported from `exinst-0.8`, as well as its tests.

+ LICENSE.txt view

@@ -0,0 +1,30 @@+Copyright (c) 2015-2018, Renzo Carbonara++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Renzo Carbonara nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

+ README.md view

@@ -0,0 +1,6 @@+# exinst-base++See the [BSD3 LICENSE](https://github.com/k0001/exinst/blob/master/exinst/exinst-base/LICENSE.txt)+file to learn about the legal terms and conditions for this library.++

+ exinst-base.cabal view

@@ -0,0 +1,47 @@+name:                exinst-base+version:             0.9+author:              Renzo Carbonara+maintainer:          renλren!zone+copyright:           Renzo Carbonara 2015+license:             BSD3+license-file:        LICENSE.txt+extra-source-files:  README.md CHANGELOG.md+category:            Data+build-type:          Simple+cabal-version:       1.18+synopsis:            @exinst@ support for @base@ package.+homepage:            https://github.com/k0001/exinst+bug-reports:         https://github.com/k0001/exinst/issues+++library+  hs-source-dirs: lib+  default-language: Haskell2010+  exposed-modules: Exinst.Base+  build-depends:+      base >=4.9 && <5.0+    , constraints+    , exinst >= 0.9+    , singletons+    , singletons-base+  ghcjs-options: -Wall -O3+  ghc-options: -Wall -O2++test-suite tests+  default-language: Haskell2010+  type: exitcode-stdio-1.0+  hs-source-dirs: tests+  main-is: Main.hs+  build-depends:+     base+   , binary+   , bytestring+   , deepseq+   , exinst+   , exinst-base+   , hashable+   , QuickCheck+   , tasty+   , tasty-quickcheck+  ghcjs-options: -Wall -O0+  ghc-options: -Wall -O0

+ lib/Exinst/Base.hs view

@@ -0,0 +1,621 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# 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', 'Read', 'Eq', 'Ord' and 'Generic'  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.Base.Enum (PEnum(EnumFromTo), PBounded(MinBound, MaxBound))+import Data.Bool.Singletons (SBool(STrue, SFalse))+import qualified Data.List.Singletons as List+import Data.Tuple.Singletons (Tuple2Sym1)+import Data.Singletons.Decide+import qualified GHC.Generics as G+import Prelude+import qualified Text.Read as Read++import Exinst hiding (Some1(..), Some2(..), Some3(..), Some4(..))+import qualified Exinst 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 k1 (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 k2 k1 (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 k3 k2 k1 (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 k4 k3 k2 k1 (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 k1 (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 k2 k1 (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 k3 k2 k1 (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 k4 k3 k2 k1 (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 k1 (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 <- decideEquality sa1x sa1y+              case dict1 sa1x :: Dict (Eq (f a1x)) of+                 Dict -> Just (x == y)++instance forall k2 k1 (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 <- decideEquality sa2x sa2y+                Refl <- decideEquality sa1x sa1y+                case dict2 sa2x sa1x :: Dict (Eq (f a2x a1x)) of+                   Dict -> Just (x == y)++instance forall k3 k2 k1 (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 <- decideEquality sa3x sa3y+                Refl <- decideEquality sa2x sa2y+                Refl <- decideEquality sa1x sa1y+                case dict3 sa3x sa2x sa1x :: Dict (Eq (f a3x a2x a1x)) of+                   Dict -> Just (x == y)++instance forall k4 k3 k2 k1 (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 <- decideEquality sa4x sa4y+                Refl <- decideEquality sa3x sa3y+                Refl <- decideEquality sa2x sa2y+                Refl <- decideEquality sa1x sa1y+                case dict4 sa4x sa3x sa2x sa1x :: Dict (Eq (f a4x a3x a2x a1x)) of+                   Dict -> Just (x == y)++--------------------------------------------------------------------------------+-- Ord++instance forall k1 (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 <- decideEquality sa1x sa1y+                  case dict1 sa1x :: Dict (Ord (f a1x)) of+                     Dict -> Just (compare x y)++instance forall k2 k1 (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 <- decideEquality sa2x sa2y+                   Refl <- decideEquality sa1x sa1y+                   case dict2 sa2x sa1x :: Dict (Ord (f a2x a1x)) of+                      Dict -> Just (compare x y)++instance forall k3 k2 k1 (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 <- decideEquality sa3x sa3y+                  Refl <- decideEquality sa2x sa2y+                  Refl <- decideEquality sa1x sa1y+                  case dict3 sa3x sa2x sa1x :: Dict (Ord (f a3x a2x a1x)) of+                     Dict -> Just (compare x y)++instance forall k4 k3 k2 k1 (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 <- decideEquality sa4x sa4y+                  Refl <- decideEquality sa3x sa3y+                  Refl <- decideEquality sa2x sa2y+                  Refl <- decideEquality 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 k4 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 forall c.+  (c 'False, c 'True+  ) => Dict0 (c :: Bool -> Constraint) where+  {-# INLINABLE dict0 #-}+  dict0 = \case { SFalse -> Dict; STrue -> Dict }++instance forall k0 c f.+  ( c (f 'False), c (f 'True)+  ) => Dict1 c (f :: Bool -> k0) where+  {-# INLINABLE dict1 #-}+  dict1 = \case { SFalse -> Dict; STrue -> Dict }++instance forall k1 k0 c f.+  ( 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 forall k2 k1 k0 c f.+  ( 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 forall k3 k2 k1 k0 c f.+  ( 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+

+ tests/Main.hs view

@@ -0,0 +1,268 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}++module Main where++import Control.DeepSeq (NFData(rnf))+import qualified Data.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+import qualified Test.Tasty as Tasty+import qualified Test.Tasty.Runners as Tasty+import Test.Tasty.QuickCheck ((===))+import qualified Test.Tasty.QuickCheck as QC+import Text.Read (readMaybe)++import Exinst+import Exinst.Base ()++--------------------------------------------------------------------------------++main :: IO ()+main = Tasty.defaultMainWithIngredients+  [ Tasty.consoleTestReporter+  , Tasty.listingTests+  ] tt++--------------------------------------------------------------------------------++data family X1 :: Bool -> Type+data instance X1 'False = XF1 | XF2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData)+data instance X1 'True = XT1 | XT2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData)++data family X2 :: Bool -> Bool -> Type+data instance X2 'False 'False = XFF1 | XFF2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData)+data instance X2 'False 'True = XFT1 | XFT2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData)+data instance X2 'True 'False = XTF1 | XTF2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData)+data instance X2 'True 'True = XTT1 | XTT2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData)++data family X3 :: Bool -> Bool -> Bool -> Type+data instance X3 'False 'False 'False = XFFF1 | XFFF2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData)+data instance X3 'False 'False 'True = XFFT1 | XFFT2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData)+data instance X3 'False 'True 'False = XFTF1 | XFTF2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData)+data instance X3 'False 'True 'True = XFTT1 | XFTT2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData)+data instance X3 'True 'False 'False = XTFF1 | XTFF2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData)+data instance X3 'True 'False 'True = XTFT1 | XTFT2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData)+data instance X3 'True 'True 'False = XTTF1 | XTTF2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData)+data instance X3 'True 'True 'True = XTTT1 | XTTT2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData)++data family X4 :: Bool -> Bool -> Bool -> Bool -> Type+data instance X4 'False 'False 'False 'False = XFFFF1 | XFFFF2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData)+data instance X4 'False 'False 'False 'True = XFFFT1 | XFFFT2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData)+data instance X4 'False 'False 'True 'False = XFFTF1 | XFFTF2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData)+data instance X4 'False 'False 'True 'True = XFFTT1 | XFFTT2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData)+data instance X4 'False 'True 'False 'False = XFTFF1 | XFTFF2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData)+data instance X4 'False 'True 'False 'True = XFTFT1 | XFTFT2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData)+data instance X4 'False 'True 'True 'False = XFTTF1 | XFTTF2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData)+data instance X4 'False 'True 'True 'True = XFTTT1 | XFTTT2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData)+data instance X4 'True 'False 'False 'False = XTFFF1 | XTFFF2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData)+data instance X4 'True 'False 'False 'True = XTFFT1 | XTFFT2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData)+data instance X4 'True 'False 'True 'False = XTFTF1 | XTFTF2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData)+data instance X4 'True 'False 'True 'True = XTFTT1 | XTFTT2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData)+data instance X4 'True 'True 'False 'False = XTTFF1 | XTTFF2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData)+data instance X4 'True 'True 'False 'True = XTTFT1 | XTTFT2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData)+data instance X4 'True 'True 'True 'False = XTTTF1 | XTTTF2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData)+data instance X4 'True 'True 'True 'True = XTTTT1 | XTTTT2 Int32 deriving (Eq, Show, Read, G.Generic, Bin.Binary, NFData)++#define INSTANCETRON(c) \+  instance c (X1 'False); \+  instance c (X1 'True); \+  instance c (X2 'False 'False); \+  instance c (X2 'False 'True); \+  instance c (X2 'True 'False); \+  instance c (X2 'True 'True); \+  instance c (X3 'False 'False 'False); \+  instance c (X3 'False 'False 'True); \+  instance c (X3 'False 'True 'False); \+  instance c (X3 'False 'True 'True); \+  instance c (X3 'True 'False 'False); \+  instance c (X3 'True 'False 'True); \+  instance c (X3 'True 'True 'False); \+  instance c (X3 'True 'True 'True); \+  instance c (X4 'False 'False 'False 'False); \+  instance c (X4 'False 'False 'False 'True); \+  instance c (X4 'False 'False 'True 'False); \+  instance c (X4 'False 'False 'True 'True); \+  instance c (X4 'False 'True 'False 'False); \+  instance c (X4 'False 'True 'False 'True); \+  instance c (X4 'False 'True 'True 'False); \+  instance c (X4 'False 'True 'True 'True); \+  instance c (X4 'True 'False 'False 'False); \+  instance c (X4 'True 'False 'False 'True); \+  instance c (X4 'True 'False 'True 'False); \+  instance c (X4 'True 'False 'True 'True); \+  instance c (X4 'True 'True 'False 'False); \+  instance c (X4 'True 'True 'False 'True); \+  instance c (X4 'True 'True 'True 'False); \+  instance c (X4 'True 'True 'True 'True)++--------------------------------------------------------------------------------+-- Arbitrary instances++instance QC.Arbitrary (X1 'False) where arbitrary = QC.oneof [ pure XF1, fmap XF2 QC.arbitrary ]+instance QC.Arbitrary (X1 'True) where arbitrary = QC.oneof [ pure XT1, fmap XT2 QC.arbitrary ]++instance QC.Arbitrary (X2 'False 'False) where arbitrary = QC.oneof [ pure XFF1, fmap XFF2 QC.arbitrary ]+instance QC.Arbitrary (X2 'False 'True) where arbitrary = QC.oneof [ pure XFT1, fmap XFT2 QC.arbitrary ]+instance QC.Arbitrary (X2 'True 'False) where arbitrary = QC.oneof [ pure XTF1, fmap XTF2 QC.arbitrary ]+instance QC.Arbitrary (X2 'True 'True) where arbitrary = QC.oneof [ pure XTT1, fmap XTT2 QC.arbitrary ]++instance QC.Arbitrary (X3 'False 'False 'False) where arbitrary = QC.oneof [ pure XFFF1, fmap XFFF2 QC.arbitrary ]+instance QC.Arbitrary (X3 'False 'False 'True) where arbitrary = QC.oneof [ pure XFFT1, fmap XFFT2 QC.arbitrary ]+instance QC.Arbitrary (X3 'False 'True 'False) where arbitrary = QC.oneof [ pure XFTF1, fmap XFTF2 QC.arbitrary ]+instance QC.Arbitrary (X3 'False 'True 'True) where arbitrary = QC.oneof [ pure XFTT1, fmap XFTT2 QC.arbitrary ]+instance QC.Arbitrary (X3 'True 'False 'False) where arbitrary = QC.oneof [ pure XTFF1, fmap XTFF2 QC.arbitrary ]+instance QC.Arbitrary (X3 'True 'False 'True) where arbitrary = QC.oneof [ pure XTFT1, fmap XTFT2 QC.arbitrary ]+instance QC.Arbitrary (X3 'True 'True 'False) where arbitrary = QC.oneof [ pure XTTF1, fmap XTTF2 QC.arbitrary ]+instance QC.Arbitrary (X3 'True 'True 'True) where arbitrary = QC.oneof [ pure XTTT1, fmap XTTT2 QC.arbitrary ]++instance QC.Arbitrary (X4 'False 'False 'False 'False) where arbitrary = QC.oneof [ pure XFFFF1, fmap XFFFF2 QC.arbitrary ]+instance QC.Arbitrary (X4 'False 'False 'False 'True) where arbitrary = QC.oneof [ pure XFFFT1, fmap XFFFT2 QC.arbitrary ]+instance QC.Arbitrary (X4 'False 'False 'True 'False) where arbitrary = QC.oneof [ pure XFFTF1, fmap XFFTF2 QC.arbitrary ]+instance QC.Arbitrary (X4 'False 'False 'True 'True) where arbitrary = QC.oneof [ pure XFFTT1, fmap XFFTT2 QC.arbitrary ]+instance QC.Arbitrary (X4 'False 'True 'False 'False) where arbitrary = QC.oneof [ pure XFTFF1, fmap XFTFF2 QC.arbitrary ]+instance QC.Arbitrary (X4 'False 'True 'False 'True) where arbitrary = QC.oneof [ pure XFTFT1, fmap XFTFT2 QC.arbitrary ]+instance QC.Arbitrary (X4 'False 'True 'True 'False) where arbitrary = QC.oneof [ pure XFTTF1, fmap XFTTF2 QC.arbitrary ]+instance QC.Arbitrary (X4 'False 'True 'True 'True) where arbitrary = QC.oneof [ pure XFTTT1, fmap XFTTT2 QC.arbitrary ]+instance QC.Arbitrary (X4 'True 'False 'False 'False) where arbitrary = QC.oneof [ pure XTFFF1, fmap XTFFF2 QC.arbitrary ]+instance QC.Arbitrary (X4 'True 'False 'False 'True) where arbitrary = QC.oneof [ pure XTFFT1, fmap XTFFT2 QC.arbitrary ]+instance QC.Arbitrary (X4 'True 'False 'True 'False) where arbitrary = QC.oneof [ pure XTFTF1, fmap XTFTF2 QC.arbitrary ]+instance QC.Arbitrary (X4 'True 'False 'True 'True) where arbitrary = QC.oneof [ pure XTFTT1, fmap XTFTT2 QC.arbitrary ]+instance QC.Arbitrary (X4 'True 'True 'False 'False) where arbitrary = QC.oneof [ pure XTTFF1, fmap XTTFF2 QC.arbitrary ]+instance QC.Arbitrary (X4 'True 'True 'False 'True) where arbitrary = QC.oneof [ pure XTTFT1, fmap XTTFT2 QC.arbitrary ]+instance QC.Arbitrary (X4 'True 'True 'True 'False) where arbitrary = QC.oneof [ pure XTTTF1, fmap XTTTF2 QC.arbitrary ]+instance QC.Arbitrary (X4 'True 'True 'True 'True) where arbitrary = QC.oneof [ pure XTTTT1, fmap XTTTT2 QC.arbitrary ]++--------------------------------------------------------------------------------++tt :: Tasty.TestTree+tt =+  Tasty.testGroup "main"+  [ tt_nfdata+  , 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+  ]++type MegaCtx a =+  ( G.Generic a+  , Show a+  , Read a+  , Hashable a+  , Bin.Binary a+  )++tt_id+  :: String+  -> (forall a. MegaCtx a => a -> Maybe a)+  -- ^ It's easier to put all the constraints here in the 'MegaCtx' monster.+  -> Tasty.TestTree+tt_id = \title id' -> Tasty.testGroup title+  [ QC.testProperty "Some1 X1" $+      QC.forAll QC.arbitrary $ \(x :: Some1 X1) -> Just x === id' x+  , QC.testProperty "Some2 X2" $+      QC.forAll QC.arbitrary $ \(x :: Some2 X2) -> Just x === id' x+  , QC.testProperty "Some3 X3" $+      QC.forAll QC.arbitrary $ \(x :: Some3 X3) -> Just x === id' x+  , QC.testProperty "Some4 X4" $+      QC.forAll QC.arbitrary $ \(x :: Some4 X4) -> Just x === id' x+  , QC.testProperty "Some1 (P1 X1 X1)" $+      QC.forAll QC.arbitrary $ \(x :: Some1 (P1 X1 X1)) -> Just x === id' x+  , QC.testProperty "Some2 (P2 X2 X2)" $+      QC.forAll QC.arbitrary $ \(x :: Some2 (P2 X2 X2)) -> Just x === id' x+  , QC.testProperty "Some3 (P3 X3 X3)" $+      QC.forAll QC.arbitrary $ \(x :: Some3 (P3 X3 X3)) -> Just x === id' x+  , QC.testProperty "Some4 (P4 X4 X4)" $+      QC.forAll QC.arbitrary $ \(x :: Some4 (P4 X4 X4)) -> Just x === id' x+  , QC.testProperty "Some1 (S1 X1 X1)" $+      QC.forAll QC.arbitrary $ \(x :: Some1 (S1 X1 X1)) -> Just x === id' x+  , QC.testProperty "Some2 (S2 X2 X2)" $+      QC.forAll QC.arbitrary $ \(x :: Some2 (S2 X2 X2)) -> Just x === id' x+  , QC.testProperty "Some3 (S3 X3 X3)" $+      QC.forAll QC.arbitrary $ \(x :: Some3 (S3 X3 X3)) -> Just x === id' x+  , QC.testProperty "Some4 (S4 X4 X4)" $+      QC.forAll QC.arbitrary $ \(x :: Some4 (S4 X4 X4)) -> Just x === id' x+  ]++tt_nfdata :: Tasty.TestTree+tt_nfdata = Tasty.testGroup "NFData"+  [ QC.testProperty "Some1 X1" $+      QC.forAll QC.arbitrary $ \(x :: Some1 X1) -> () === rnf x+  , QC.testProperty "Some2 X2" $+      QC.forAll QC.arbitrary $ \(x :: Some2 X2) -> () === rnf x+  , QC.testProperty "Some3 X3" $+      QC.forAll QC.arbitrary $ \(x :: Some3 X3) -> () === rnf x+  , QC.testProperty "Some4 X4" $+      QC.forAll QC.arbitrary $ \(x :: Some4 X4) -> () === rnf x+  , QC.testProperty "Some1 (P1 X1 X1)" $+      QC.forAll QC.arbitrary $ \(x :: Some1 (P1 X1 X1)) -> () === rnf x+  , QC.testProperty "Some2 (P2 X2 X2)" $+      QC.forAll QC.arbitrary $ \(x :: Some2 (P2 X2 X2)) -> () === rnf x+  , QC.testProperty "Some3 (P3 X3 X3)" $+      QC.forAll QC.arbitrary $ \(x :: Some3 (P3 X3 X3)) -> () === rnf x+  , QC.testProperty "Some4 (P4 X4 X4)" $+      QC.forAll QC.arbitrary $ \(x :: Some4 (P4 X4 X4)) -> () === rnf x+  , QC.testProperty "Some1 (S1 X1 X1)" $+      QC.forAll QC.arbitrary $ \(x :: Some1 (S1 X1 X1)) -> () === rnf x+  , QC.testProperty "Some2 (S2 X2 X2)" $+      QC.forAll QC.arbitrary $ \(x :: Some2 (S2 X2 X2)) -> () === rnf x+  , QC.testProperty "Some3 (S3 X3 X3)" $+      QC.forAll QC.arbitrary $ \(x :: Some3 (S3 X3 X3)) -> () === rnf x+  , QC.testProperty "Some4 (S4 X4 X4)" $+      QC.forAll QC.arbitrary $ \(x :: Some4 (S4 X4 X4)) -> () === rnf x+  ]++INSTANCETRON(Hashable)++tt_hashable :: Tasty.TestTree+tt_hashable = Tasty.testGroup "Hashable"+  [ QC.testProperty "Some1 X1" $+      QC.forAll QC.arbitrary $ \(x :: Some1 X1) -> () === (hash x `seq` ())+  , QC.testProperty "Some2 X2" $+      QC.forAll QC.arbitrary $ \(x :: Some2 X2) -> () === (hash x `seq` ())+  , QC.testProperty "Some3 X3" $+      QC.forAll QC.arbitrary $ \(x :: Some3 X3) -> () === (hash x `seq` ())+  , QC.testProperty "Some4 X4" $+      QC.forAll QC.arbitrary $ \(x :: Some4 X4) -> () === (hash x `seq` ())+  , QC.testProperty "Some1 (P1 X1 X1)" $+      QC.forAll QC.arbitrary $ \(x :: Some1 (P1 X1 X1)) -> () === (hash x `seq` ())+  , QC.testProperty "Some2 (P2 X2 X2)" $+      QC.forAll QC.arbitrary $ \(x :: Some2 (P2 X2 X2)) -> () === (hash x `seq` ())+  , QC.testProperty "Some3 (P3 X3 X3)" $+      QC.forAll QC.arbitrary $ \(x :: Some3 (P3 X3 X3)) -> () === (hash x `seq` ())+  , QC.testProperty "Some4 (P4 X4 X4)" $+      QC.forAll QC.arbitrary $ \(x :: Some4 (P4 X4 X4)) -> () === (hash x `seq` ())+  , QC.testProperty "Some1 (S1 X1 X1)" $+      QC.forAll QC.arbitrary $ \(x :: Some1 (S1 X1 X1)) -> () === (hash x `seq` ())+  , QC.testProperty "Some2 (S2 X2 X2)" $+      QC.forAll QC.arbitrary $ \(x :: Some2 (S2 X2 X2)) -> () === (hash x `seq` ())+  , QC.testProperty "Some3 (S3 X3 X3)" $+      QC.forAll QC.arbitrary $ \(x :: Some3 (S3 X3 X3)) -> () === (hash x `seq` ())+  , QC.testProperty "Some4 (S4 X4 X4)" $+      QC.forAll QC.arbitrary $ \(x :: Some4 (S4 X4 X4)) -> () === (hash x `seq` ())+  ]++--------------------------------------------------------------------------------++id_show_read :: (Show a, Read a) => a -> Maybe a+id_show_read = readMaybe . show++id_generic :: G.Generic a => a -> Maybe a+id_generic = Just . G.to . G.from++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+