packages feed

quantification 0.4 → 0.5.0

raw patch · 6 files changed

+631/−163 lines, 6 filesdep +binarydep ~containers

Dependencies added: binary

Dependency ranges changed: containers

Files

quantification.cabal view
@@ -1,5 +1,6 @@+cabal-version: 2.0 name: quantification-version: 0.4+version: 0.5.0 synopsis: Rage against the quantification description: Data types and typeclasses to deal with universally and existentially quantified types homepage: https://github.com/andrewthad/quantification#readme@@ -7,20 +8,21 @@ license-file: LICENSE author: Andrew Martin maintainer: andrew.thaddeus@gmail.com-copyright: 2016 Andrew Martin+copyright: 2018 Andrew Martin category: Web build-type: Simple-cabal-version: >=1.10  library   hs-source-dirs: src   exposed-modules:+    Data.Binary.Lifted     Data.Exists     Data.Monoid.Lifted     Topaz.Rec     Topaz.Types   build-depends:        base >= 4.9 && < 5+    , binary >= 0.8 && < 0.10     , ghc-prim >= 0.5 && < 0.6     , hashable >= 1.2 && < 1.3     , aeson >= 1.0 && < 1.5@@ -30,6 +32,7 @@     , containers >= 0.5 && < 0.6     , unordered-containers >= 0.2 && < 0.3   default-language: Haskell2010+  ghc-options: -O2 -Wall  source-repository head   type:     git
+ src/Data/Binary/Lifted.hs view
@@ -0,0 +1,59 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}++module Data.Binary.Lifted+  ( Binary1(..)+  , put1+  , get1+  ) where++import Data.Binary (Get,Put,Binary,get,put)+import Data.Functor.Compose (Compose(..))+import Data.Word (Word8)+import Data.Semigroup ((<>))++class Binary1 f where+  liftPut :: (a -> Put) -> f a -> Put+  liftGet :: Get a -> Get (f a)++instance Binary1 [] where+  liftPut = liftPutList+  liftGet = liftGetList++instance Binary1 Maybe where+  liftPut _ Nothing  = put (0 :: Word8)+  liftPut f (Just x) = put (1 :: Word8) <> f x+  liftGet f = do+    (w :: Word8) <- get+    case w of+      0 -> return Nothing+      _ -> fmap Just f++instance (Binary1 f, Binary1 g) => Binary1 (Compose f g) where+  liftPut f (Compose x) = liftPut (liftPut f) x+  liftGet f = fmap Compose (liftGet (liftGet f))++liftPutList :: (a -> Put) -> [a] -> Put+liftPutList f xs = put (length xs) <> mapM_ f xs                                ++liftGetList :: Get a -> Get [a]                                                    +liftGetList g = do+  n <- get :: Get Int                                                           +  internalGetMany g n                                                              ++internalGetMany :: Get a -> Int -> Get [a]                                         +internalGetMany g n = go [] n                                                      +  where +  go xs !0 = return $! reverse xs                                                  +  go xs !i = do                                                                    +    !x <- g+    go (x:xs) (i-1)                                                                ++get1 :: (Binary1 f, Binary a) => Get (f a)+get1 = liftGet get++put1 :: (Binary1 f, Binary a) => f a -> Put+put1 = liftPut put++
src/Data/Exists.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE BangPatterns #-}+{-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE ExistentialQuantification #-}@@ -13,14 +14,16 @@ {-# LANGUAGE TypeFamilyDependencies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UnboxedTuples #-}  {-# OPTIONS_GHC -Wall #-}  {-| Data types and type classes for working with existentially quantified-    values. In the event that Quantified Class Constraints ever land in GHC,-    this package will be considered obsolete. The benefit that most of the-    typeclasses in this module provide is that they help populate the instances-    of 'Exists'.+    values. When Quantified Class Constraints land in GHC 8.6,+    the @BarForall@ classes will be considered obsolete. When Dependent+    Haskell lands, the @BarForeach@ classes will also be obsolete.+    The benefit that most of the typeclasses in this module provide is+    that they help populate the instances of 'Exists' and @Rec@. -}  module Data.Exists@@ -32,6 +35,9 @@   , DependentPair(..)   , WitnessedEquality(..)   , WitnessedOrdering(..)+  , ApplyForall(..)+  , ApplyForeach(..)+  , ApplyLifted(..)     -- * Type Classes   , EqForall(..)   , EqForallPoly(..)@@ -41,26 +47,38 @@   , OrdForeach(..)   , ShowForall(..)   , ShowForeach(..)-  , ReadForall(..)+  , ReadExists(..)   , EnumForall(..)-  , BoundedForall(..)+  , EnumExists(..)+  , BoundedExists(..)   , SemigroupForall(..)+  , SemigroupForeach(..)   , MonoidForall(..)+  , MonoidForeach(..)   , HashableForall(..)-  , PathPieceForall(..)-  , FromJSONForall(..)+  , HashableForeach(..)+  , PathPieceExists(..)+  , FromJSONForeach(..)   , FromJSONExists(..)   , ToJSONForall(..)+  , ToJSONForeach(..)   , ToJSONKeyFunctionForall(..)-  , FromJSONKeyFunctionForall(..)+  , FromJSONKeyFunctionForeach(..)   , ToJSONKeyForall(..)+  , ToJSONKeyForeach(..)   , FromJSONKeyExists(..)-  , FromJSONKeyForall(..)+  , FromJSONKeyForeach(..)+  , StorableForeach(..)   , StorableForall(..)+  , PrimForall(..)+  , BinaryExists(..)+  , BinaryForeach(..)     -- * Higher Rank Classes   , EqForall2(..)   , EqForallPoly2(..)   , ShowForall2(..)+  , ShowForeach2(..)+  , BinaryExists2(..)     -- * More Type Classes   , Sing   , SingList(..)@@ -69,55 +87,72 @@   , Unreify(..)     -- * Sing Type Classes   , EqSing(..)+  , OrdSing(..)+  , ShowSing(..)   , ToJSONSing(..)   , FromJSONSing(..)   , ToSing(..)+  , SingKind(..)     -- * Functions     -- ** Show   , showsForall+  , showsForeach   , showForall+  , showListForall+  , showListForeach   , showsForall2   , showForall2     -- ** Defaulting   , defaultEqForallPoly   , defaultCompareForallPoly-  , parseJSONMapForallKey+  , parseJSONMapForeachKey+  , toJSONMapForeachKey     -- ** Weakening   , weakenEquality   , weakenOrdering+  , strengthenEquality+  , strengthenOrdering+  , strengthenUnequalOrdering     -- ** Other   , unreifyList   ) where -import Data.Proxy (Proxy(..))-import Data.Type.Equality ((:~:)(Refl),TestEquality(..)) import Control.Applicative (Const(..)) import Data.Aeson (ToJSON(..),FromJSON(..))-import Data.Hashable (Hashable(..))-import Data.Text (Text)-import Data.Functor.Classes (Eq1(..),Show1(..))-import Data.Functor.Sum (Sum(..))-import Data.Functor.Product (Product(..))+import Data.Aeson (ToJSONKey(..),FromJSONKey(..))+import Data.Aeson (ToJSONKeyFunction(..),FromJSONKeyFunction(..))+import Data.Aeson.Internal ((<?>),JSONPathElement(Key,Index))+import Data.Binary (Get,Put,Binary)+import Data.Binary.Lifted (Binary1(..))+import Data.Coerce (coerce)+import Data.Functor.Classes (Eq1(..),Show1(..),Ord1(..),eq1,compare1) import Data.Functor.Compose (Compose(..))-import GHC.Int (Int(..))-import GHC.Prim (dataToTag#)-import Foreign.Ptr (Ptr)+import Data.Functor.Product (Product(..))+import Data.Functor.Sum (Sum(..))+import Data.Hashable (Hashable(..)) import Data.Kind (Type) import Data.Map.Strict (Map)-import Data.Coerce (coerce)-import qualified Data.Traversable as TRV-import qualified Data.Map.Strict as M+import Data.Monoid.Lifted (Semigroup1(..),Monoid1(..),append1,empty1)+import Data.Proxy (Proxy(..))+import Data.Semigroup (Semigroup)+import Data.Text (Text)+import Data.Type.Equality ((:~:)(Refl),TestEquality(..))+import Foreign.Ptr (Ptr)+import GHC.Exts (dataToTag#,State#,Int#,Proxy#,Addr#,ByteArray#,MutableByteArray#)+import GHC.Int (Int(..))++import qualified Data.Aeson.Encoding as Aeson+import qualified Data.Aeson.Encoding.Internal as AEI+import qualified Data.Aeson.Types as Aeson+import qualified Data.Binary as BN import qualified Data.HashMap.Strict as HM+import qualified Data.Map.Strict as M+import qualified Data.Semigroup as SG+import qualified Data.Traversable as TRV import qualified Data.Vector as V-import qualified Data.Aeson.Types as Aeson import qualified Text.Read as R import qualified Web.PathPieces as PP -import qualified Data.Aeson.Encoding as Aeson-import Data.Aeson (ToJSONKey(..),FromJSONKey(..),-  ToJSONKeyFunction(..),FromJSONKeyFunction(..))-import Data.Aeson.Internal ((<?>),JSONPathElement(Key,Index))- -- | Hide a type parameter. data Exists (f :: k -> Type) = forall a. Exists !(f a) @@ -127,9 +162,16 @@ -- | Hide three type parameters. data Exists3 (f :: k -> j -> l -> Type) = forall a b c. Exists3 !(f a b c) +-- | A pair in which the type of the second element can only+--   be discovered by looking at the first element. The type+--   instance does not enforce this, but all of its typeclass+--   instances make this assumption. data DependentPair (f :: k -> Type) (g :: k -> Type) =   forall a. DependentPair (f a) (g a) +-- | A dependent pair in which the first element is a singleton.+data Some (f :: k -> Type) = forall a. Some !(Sing a) !(f a)+ data WitnessedEquality (a :: k) (b :: k) where   WitnessedEqualityEqual :: WitnessedEquality a a   WitnessedEqualityUnequal :: WitnessedEquality a b@@ -142,10 +184,147 @@ data ToJSONKeyFunctionForall f   = ToJSONKeyTextForall !(forall a. f a -> Text) !(forall a. f a -> Aeson.Encoding' Text)   | ToJSONKeyValueForall !(forall a. f a -> Aeson.Value) !(forall a. f a -> Aeson.Encoding)-data FromJSONKeyFunctionForall f-  = FromJSONKeyTextParserForall !(forall a. Sing a -> Text -> Aeson.Parser (f a))-  | FromJSONKeyValueForall !(forall a. Sing a -> Aeson.Value -> Aeson.Parser (f a))+data FromJSONKeyFunctionForeach f+  = FromJSONKeyTextParserForeach !(forall a. Sing a -> Text -> Aeson.Parser (f a))+  | FromJSONKeyValueForeach !(forall a. Sing a -> Aeson.Value -> Aeson.Parser (f a)) +newtype ApplyForall f a = ApplyForall { getApplyForall :: f a }++instance ShowForall f => Show (ApplyForall f a) where+  showsPrec p (ApplyForall x) = showParen (p > 10)+    $ showString "ApplyForall "+    . showsPrecForall 11 x++instance SemigroupForall f => Semigroup (ApplyForall f a) where+  (<>) = appendForall++instance MonoidForall f => Monoid (ApplyForall f a) where+  mempty = emptyForall+  mappend = (SG.<>)++instance SemigroupForall f => SemigroupForall (ApplyForall f) where+  appendForall (ApplyForall a) (ApplyForall b) = ApplyForall (appendForall a b)++instance MonoidForall f => MonoidForall (ApplyForall f) where+  emptyForall = ApplyForall emptyForall++newtype ApplyLifted f a = ApplyLifted { getApplyLifted :: f a }                         ++instance (Semigroup1 f, Semigroup a) => Semigroup (ApplyLifted f a) where  +  (<>) = append1++instance (Monoid1 f, Monoid a) => Monoid (ApplyLifted f a) where+  mempty = empty1 +  mappend = liftAppend mappend++instance (Eq1 f, Eq a) => Eq (ApplyLifted f a) where+  (==) = eq1 ++instance (Ord1 f, Ord a) => Ord (ApplyLifted f a) where+  compare = compare1 ++instance Semigroup1 f => Semigroup1 (ApplyLifted f) where  +  liftAppend g (ApplyLifted a) (ApplyLifted b) = ApplyLifted (liftAppend g a b)                        ++instance Monoid1 f => Monoid1 (ApplyLifted f) where        +  liftEmpty f = ApplyLifted (liftEmpty f)                                        ++instance Eq1 f => Eq1 (ApplyLifted f) where+  liftEq f (ApplyLifted a) (ApplyLifted b) = liftEq f a b++instance Ord1 f => Ord1 (ApplyLifted f) where+  liftCompare f (ApplyLifted a) (ApplyLifted b) = liftCompare f a b++-- | This is useful for recovering an instance of a typeclass when+-- we have the pi-quantified variant and a singleton in scope.+newtype ApplyForeach f a = ApplyForeach { getApplyForeach :: f a }++instance (EqForeach f, Reify a) => Eq (ApplyForeach f a) where+  ApplyForeach a == ApplyForeach b = eqForeach reify a b++instance (OrdForeach f, Reify a) => Ord (ApplyForeach f a) where+  compare (ApplyForeach a) (ApplyForeach b) = compareForeach reify a b++instance (ShowForeach f, Reify a) => Show (ApplyForeach f a) where+  showsPrec p (ApplyForeach a) = showParen (p > 10)+    $ showString "ApplyForeach "+    . showsPrecForeach reify 11 a++instance (SemigroupForeach f, Reify a) => Semigroup (ApplyForeach f a) where+  (<>) = appendForeach reify++instance (MonoidForeach f, Reify a) => Monoid (ApplyForeach f a) where+  mempty = emptyForeach reify+  mappend = (SG.<>)++instance (ToJSONForeach f, Reify a) => ToJSON (ApplyForeach f a) where+  toJSON = toJSONForeach reify++instance (FromJSONForeach f, Reify a) => FromJSON (ApplyForeach f a) where+  parseJSON = parseJSONForeach reify++instance EqForeach f => EqForeach (ApplyForeach f) where+  eqForeach s (ApplyForeach a) (ApplyForeach b) = eqForeach s a b++instance OrdForeach f => OrdForeach (ApplyForeach f) where+  compareForeach s (ApplyForeach a) (ApplyForeach b) = compareForeach s a b++instance SemigroupForeach f => SemigroupForeach (ApplyForeach f) where+  appendForeach s (ApplyForeach a) (ApplyForeach b) = ApplyForeach (appendForeach s a b)++instance MonoidForeach f => MonoidForeach (ApplyForeach f) where+  emptyForeach s = ApplyForeach (emptyForeach s)++instance ToJSONForeach f => ToJSONForeach (ApplyForeach f) where+  toJSONForeach s (ApplyForeach x) = toJSONForeach s x++instance FromJSONForeach f => FromJSONForeach (ApplyForeach f) where+  parseJSONForeach s = fmap ApplyForeach . parseJSONForeach s++instance ToJSONKeyForeach f => ToJSONKeyForeach (ApplyForeach f) where+  toJSONKeyForeach = case toJSONKeyForeach of+    ToJSONKeyTextForall f g -> ToJSONKeyTextForall+      (\(Pair s (ApplyForeach x)) -> f (Pair s x))+      (\(Pair s (ApplyForeach x)) -> g (Pair s x))+    ToJSONKeyValueForall f g -> ToJSONKeyValueForall+      (\(Pair s (ApplyForeach x)) -> f (Pair s x))+      (\(Pair s (ApplyForeach x)) -> g (Pair s x))++instance FromJSONKeyForeach f => FromJSONKeyForeach (ApplyForeach f) where+  fromJSONKeyForeach = case fromJSONKeyForeach of+    FromJSONKeyTextParserForeach f -> FromJSONKeyTextParserForeach (\s t -> fmap ApplyForeach (f s t))+    FromJSONKeyValueForeach f -> FromJSONKeyValueForeach (\s t -> fmap ApplyForeach (f s t))++instance (ToJSONKeyForeach f, Reify a) => ToJSONKey (ApplyForeach f a) where+  toJSONKey = case toJSONKeyForeach of+    ToJSONKeyTextForall toText toEnc -> ToJSONKeyText+      (\(ApplyForeach x) -> toText (Pair reify x))+      (\(ApplyForeach x) -> toEnc (Pair reify x))+    ToJSONKeyValueForall toValue toEnc -> ToJSONKeyValue+      (\(ApplyForeach x) -> toValue (Pair reify x))+      (\(ApplyForeach x) -> toEnc (Pair reify x))+  toJSONKeyList = case toJSONKeyForeach of+    ToJSONKeyTextForall toText toEnc -> ToJSONKeyValue+      (\xs -> toJSON $ map (\(ApplyForeach x) -> toText (Pair reify x)) xs)+      (\xs -> Aeson.list (textEncodingToValueEncoding . toEnc . Pair reify) (map getApplyForeach xs))+    ToJSONKeyValueForall toValue toEnc -> ToJSONKeyValue+      (\xs -> toJSON $ map (\(ApplyForeach x) -> toValue (Pair reify x)) xs)+      (\xs -> Aeson.list (toEnc . Pair reify) (map getApplyForeach xs))++-- this is always safe+textEncodingToValueEncoding :: Aeson.Encoding' Text -> Aeson.Encoding' Aeson.Value+textEncodingToValueEncoding = AEI.retagEncoding++instance (FromJSONKeyForeach f, Reify a) => FromJSONKey (ApplyForeach f a) where+  fromJSONKey = case fromJSONKeyForeach of+    FromJSONKeyTextParserForeach f -> FromJSONKeyTextParser (fmap ApplyForeach . f reify)+    FromJSONKeyValueForeach f -> FromJSONKeyValue (fmap ApplyForeach . f reify)+  fromJSONKeyList = case fromJSONKeyForeach of+    FromJSONKeyTextParserForeach f -> FromJSONKeyValue $ Aeson.withArray "ApplyForeach" $ \xs -> do+      fmap V.toList (mapM (fmap ApplyForeach . Aeson.withText "ApplyForeach" (f reify)) xs)+    FromJSONKeyValueForeach f -> FromJSONKeyValue $ Aeson.withArray "ApplyForeach" $ \xs -> do+      fmap V.toList (mapM (fmap ApplyForeach . f reify) xs)+ class EqForall f where   eqForall :: f a -> f a -> Bool @@ -179,9 +358,15 @@ class ShowForall2 f where   showsPrecForall2 :: Int -> f a b -> ShowS +class ShowForeach2 f where+  showsPrecForeach2 :: Sing a -> Sing b -> Int -> f a b -> ShowS+ showsForall :: ShowForall f => f a -> ShowS showsForall = showsPrecForall 0 +showsForeach :: ShowForeach f => Sing a -> f a -> ShowS+showsForeach s = showsPrecForeach s 0+ showForall :: ShowForall f => f a -> String showForall x = showsForall x "" @@ -191,57 +376,106 @@ showForall2 :: ShowForall2 f => f a b -> String showForall2 x = showsForall2 x "" -class ReadForall f where-  readPrecForall :: R.ReadPrec (Exists f)+class ReadExists f where+  readPrecExists :: R.ReadPrec (Exists f)  class EqForall2 f where   eqForall2 :: f a b -> f a b -> Bool -class EqForallPoly2 f where-  eqForallPoly2 :: f a b -> f c d -> Bool+class EqForallPoly2 (f :: k -> j -> Type) where +  eqForallPoly2 :: forall (a :: k) (b :: j) (c :: k) (d :: j). f a b -> f c d -> WitnessedEquality '(a,b) '(c,d)  class HashableForall f where   hashWithSaltForall :: Int -> f a -> Int +class HashableForeach f where+  hashWithSaltForeach :: Sing a -> Int -> f a -> Int+ class ToJSONKeyForall f where   toJSONKeyForall :: ToJSONKeyFunctionForall f +class ToJSONKeyForeach f where+  toJSONKeyForeach :: ToJSONKeyFunctionForall (Product Sing f)+ class FromJSONKeyExists f where   fromJSONKeyExists :: FromJSONKeyFunction (Exists f) -class FromJSONKeyForall f where-  fromJSONKeyForall :: FromJSONKeyFunctionForall f+class FromJSONKeyForeach f where+  fromJSONKeyForeach :: FromJSONKeyFunctionForeach f  class ToJSONForall f where   toJSONForall :: f a -> Aeson.Value -class FromJSONForall f where-  parseJSONForall :: Sing a -> Aeson.Value -> Aeson.Parser (f a)+class ToJSONForeach f where+  toJSONForeach :: Sing a -> f a -> Aeson.Value +class FromJSONForeach f where+  parseJSONForeach :: Sing a -> Aeson.Value -> Aeson.Parser (f a)+ class FromJSONExists f where   parseJSONExists :: Aeson.Value -> Aeson.Parser (Exists f)  class EnumForall f where-  toEnumForall :: Int -> Exists f+  toEnumForall :: Int -> f a   fromEnumForall :: f a -> Int -class BoundedForall f where-  minBoundForall :: Exists f-  maxBoundForall :: Exists f+class EnumExists f where+  toEnumExists :: Int -> Exists f+  fromEnumExists :: Exists f -> Int -class PathPieceForall f where+class BoundedExists f where+  minBoundExists :: Exists f+  maxBoundExists :: Exists f++class PathPieceExists f where   fromPathPieceForall :: Text -> Maybe (Exists f)-  toPathPieceForall :: f a -> Text+  toPathPieceForall :: Exists f -> Text +class SemigroupForeach f where+  appendForeach :: Sing a -> f a -> f a -> f a+ class SemigroupForall f where-  sappendForall :: f a -> f a -> f a+  appendForall :: f a -> f a -> f a +class StorableForeach (f :: k -> Type) where+  peekForeach :: Sing a -> Ptr (f a) -> IO (f a)+  pokeForeach :: Sing a -> Ptr (f a) -> f a -> IO ()+  sizeOfForeach :: forall (a :: k). Proxy f -> Sing a -> Int++-- | This is like 'StorableForall' except that the type constructor+-- must ignore its argument (for purposes of representation). class StorableForall (f :: k -> Type) where-  peekForall :: Sing a -> Ptr (f a) -> IO (f a)+  peekForall :: Ptr (f a) -> IO (f a)   pokeForall :: Ptr (f a) -> f a -> IO ()-  sizeOfFunctorForall :: f a -> Int-  sizeOfForall :: forall (a :: k). Proxy f -> Sing a -> Int+  sizeOfForall :: Proxy f -> Int +-- | Be careful with this typeclass. It is more unsafe than 'Prim'.+-- With 'writeByteArray#' and 'readByteArray#', one can implement+-- @unsafeCoerce@.+class PrimForall (f :: k -> Type) where+  sizeOfForall# :: Proxy# f -> Int#+  alignmentForall# :: Proxy# f -> Int#+  indexByteArrayForall# :: ByteArray# -> Int# -> f a+  readByteArrayForall# :: MutableByteArray# s -> Int# -> State# s -> (# State# s, f a #)+  writeByteArrayForall# :: MutableByteArray# s -> Int# -> f a -> State# s -> State# s+  setByteArrayForall# :: MutableByteArray# s -> Int# -> Int# -> f a -> State# s -> State# s+  indexOffAddrForall# :: Addr# -> Int# -> f a+  readOffAddrForall# :: Addr# -> Int# -> State# s -> (# State# s, f a #)+  writeOffAddrForall# :: Addr# -> Int# -> f a -> State# s -> State# s+  setOffAddrForall# :: Addr# -> Int# -> Int# -> f a -> State# s -> State# s++class BinaryForeach (f :: k -> Type) where+  putForeach :: Sing a -> f a -> Put+  getForeach :: Sing a -> Get (f a)++class BinaryExists (f :: k -> Type) where+  putExists :: Exists f -> Put+  getExists :: Get (Exists f)++class BinaryExists2 (f :: k -> j -> Type) where+  putExists2 :: Exists2 f -> Put+  getExists2 :: Get (Exists2 f)+ -------------------- -- Instances Below --------------------@@ -255,11 +489,11 @@ instance ShowForall Proxy where   showsPrecForall = showsPrec -instance ReadForall Proxy where-  readPrecForall = fmap Exists R.readPrec +instance ReadExists Proxy where+  readPrecExists = fmap Exists R.readPrec   instance SemigroupForall Proxy where-  sappendForall _ _ = Proxy +  appendForall _ _ = Proxy   instance EqForall ((:~:) a) where   eqForall Refl Refl = True@@ -267,7 +501,10 @@ instance EqForall2 (:~:) where   eqForall2 Refl Refl = True -+instance Show a => ShowForall (Const a) where+  showsPrecForall p (Const a) = showParen (p > 10)+    $ showString "Const "+    . showsPrec p a  instance Eq a => EqForall (Const a) where   eqForall (Const x) (Const y) = x == y@@ -278,8 +515,11 @@ instance Hashable a => HashableForall (Const a) where   hashWithSaltForall s (Const a) = hashWithSalt s a +instance FromJSON a => FromJSONForeach (Const a) where+  parseJSONForeach _ = fmap Const . parseJSON --- I need to get rid of the ToJSONForall and FromJSONForall constraints++-- I need to get rid of the ToJSONForall and FromJSONForeach constraints -- on these two instances. instance (ToJSONKeyForall f, ToJSONForall f) => ToJSONKey (Exists f) where   toJSONKey = case toJSONKeyForall of@@ -293,7 +533,7 @@   Exists a == Exists b = weakenEquality (eqForallPoly a b)  instance EqForallPoly2 f => Eq (Exists2 f) where-  Exists2 a == Exists2 b = eqForallPoly2 a b+  Exists2 a == Exists2 b = weakenEquality (eqForallPoly2 a b)  instance OrdForallPoly f => Ord (Exists f) where   compare (Exists a) (Exists b) = weakenOrdering (compareForallPoly a b)@@ -317,21 +557,29 @@     (p >= 11)      (showString "Exists " . showsPrecForall2 11 a) -instance ReadForall f => Read (Exists f) where+instance ReadExists f => Read (Exists f) where   readPrec = R.parens $ R.prec 10 $ do     R.Ident "Exists" <- R.lexP-    R.step readPrecForall+    R.step readPrecExists     -instance EnumForall f => Enum (Exists f) where-  fromEnum (Exists x) = fromEnumForall x-  toEnum = toEnumForall+instance EnumExists f => Enum (Exists f) where+  fromEnum = fromEnumExists+  toEnum = toEnumExists -instance BoundedForall f => Bounded (Exists f) where-  minBound = minBoundForall-  maxBound = maxBoundForall+instance BoundedExists f => Bounded (Exists f) where+  minBound = minBoundExists+  maxBound = maxBoundExists -instance PathPieceForall f => PP.PathPiece (Exists f) where-  toPathPiece (Exists f) = toPathPieceForall f+instance BinaryExists f => Binary (Exists f) where+  get = getExists+  put = putExists++instance BinaryExists2 f => Binary (Exists2 f) where+  get = getExists2+  put = putExists2++instance PathPieceExists f => PP.PathPiece (Exists f) where+  toPathPiece = toPathPieceForall   fromPathPiece = fromPathPieceForall  instance (EqForall f, EqForall g) => EqForall (Product f g) where@@ -356,23 +604,45 @@     (p >= 11)      (showString "Pair " . showsPrecForall 11 f . showChar ' ' . showsPrecForall 11 g) +instance (Semigroup1 f, SemigroupForall g) => SemigroupForall (Compose f g) where+  appendForall (Compose x) (Compose y) = Compose (liftAppend appendForall x y)+ instance (Aeson.ToJSON1 f, ToJSONForall g) => ToJSONForall (Compose f g) where   toJSONForall (Compose x) = Aeson.liftToJSON toJSONForall (Aeson.toJSON . map toJSONForall) x -instance (Aeson.FromJSON1 f, FromJSONForall g) => FromJSONForall (Compose f g) where-  parseJSONForall s = fmap Compose . Aeson.liftParseJSON-    (parseJSONForall s)-    (Aeson.withArray "Compose" (fmap V.toList . V.mapM (parseJSONForall s)))+instance (Aeson.ToJSON1 f, ToJSONForeach g) => ToJSONForeach (Compose f g) where+  toJSONForeach s (Compose x) = Aeson.liftToJSON (toJSONForeach s) (Aeson.toJSON . map (toJSONForeach s)) x +instance (Aeson.FromJSON1 f, FromJSONForeach g) => FromJSONForeach (Compose f g) where+  parseJSONForeach s = fmap Compose . Aeson.liftParseJSON+    (parseJSONForeach s)+    (Aeson.withArray "Compose" (fmap V.toList . V.mapM (parseJSONForeach s)))+ instance (Eq1 f, EqForall g) => EqForall (Compose f g) where   eqForall (Compose x) (Compose y) = liftEq eqForall x y +instance (Eq1 f, EqForeach g) => EqForeach (Compose f g) where+  eqForeach s (Compose x) (Compose y) = liftEq (eqForeach s) x y+ instance (Show1 f, ShowForall g) => ShowForall (Compose f g) where-  showsPrecForall _ (Compose x) = showString "Compose " . liftShowsPrec showsPrecForall showListForall 11 x+  showsPrecForall p (Compose x) = showParen (p > 10) $ showString "Compose " . liftShowsPrec showsPrecForall showListForall 11 x +instance (Show1 f, ShowForeach g) => ShowForeach (Compose f g) where+  showsPrecForeach s p (Compose x) = showParen (p > 10) $ showString "Compose " . liftShowsPrec (showsPrecForeach s) (showListForeach s) 11 x++instance (Semigroup1 f, SemigroupForeach g) => SemigroupForeach (Compose f g) where+  appendForeach s (Compose x) (Compose y) = Compose (liftAppend (appendForeach s) x y)++instance (Binary1 f, BinaryForeach g) => BinaryForeach (Compose f g) where+  putForeach s (Compose x) = liftPut (putForeach s) x+  getForeach s = fmap Compose (liftGet (getForeach s))+ showListForall :: ShowForall f => [f a] -> ShowS showListForall = showList__ showsForall +showListForeach :: ShowForeach f => Sing a -> [f a] -> ShowS+showListForeach s = showList__ (showsForeach s)+ -- Copied from GHC.Show. I do not like to import internal modules -- if I can instead copy a small amount of code. showList__ :: (a -> ShowS) ->  [a] -> ShowS@@ -410,6 +680,19 @@  type family Sing = (r :: k -> Type) | r -> k +-- | The two functions must form an isomorphism.+class SingKind k where+  demoteSing :: Sing (a :: k) -> k+  promoteSing :: k -> Exists (Sing :: k -> Type)++instance SingKind k => SingKind [k] where+  demoteSing SingListNil = []+  demoteSing (SingListCons s ss) = demoteSing s : demoteSing ss+  promoteSing [] = Exists SingListNil+  promoteSing (x : xs) = case promoteSing x of+    Exists s -> case promoteSing xs of+      Exists ss -> Exists (SingListCons s ss)+ type instance Sing = SingList type instance Sing = SingMaybe @@ -437,6 +720,12 @@ class EqSing k where   eqSing :: forall (a :: k) (b :: k). Sing a -> Sing b -> Maybe (a :~: b) +class EqSing k => OrdSing k where+  compareSing :: forall (a :: k) (b :: k). Sing a -> Sing b -> WitnessedOrdering a b++class ShowSing k where+  showsPrecSing :: forall (a :: k). Int -> Sing a -> ShowS+ instance EqSing a => EqSing [a] where   eqSing = eqSingList @@ -450,13 +739,46 @@     Nothing -> Nothing   Nothing -> Nothing +class SemigroupForeach f => MonoidForeach f where+  emptyForeach :: Sing a -> f a+ class SemigroupForall f => MonoidForall f where-  memptyForall :: Sing a -> f a+  emptyForall :: f a -data SingList :: [k] -> Type where+data SingList :: forall (k :: Type). [k] -> Type where   SingListNil :: SingList '[]   SingListCons :: Sing r -> SingList rs -> SingList (r ': rs) +-- singletons can only have one inhabitant per type, so if the+-- types are equal, the values must be equal+instance EqForall SingList where+  eqForall _ _ = True++instance EqSing k => EqForallPoly (SingList :: [k] -> Type) where+  eqForallPoly SingListNil SingListNil = WitnessedEqualityEqual+  eqForallPoly SingListNil (SingListCons _ _) = WitnessedEqualityUnequal+  eqForallPoly (SingListCons _ _) SingListNil = WitnessedEqualityUnequal+  eqForallPoly (SingListCons r rs) (SingListCons s ss) = case eqSing r s of+    Nothing -> WitnessedEqualityUnequal+    Just Refl -> case eqForallPoly rs ss of+      WitnessedEqualityUnequal -> WitnessedEqualityUnequal+      WitnessedEqualityEqual -> WitnessedEqualityEqual++instance (SingKind k, Binary k) => BinaryExists (SingList :: [k] -> Type) where+  putExists (Exists xs) = BN.put (demoteSing xs)+  getExists = fmap promoteSing BN.get++instance (ShowSing k) => Show (SingList (xs :: [k])) where+  showsPrec _ SingListNil = showString "SingListNil"+  showsPrec p (SingListCons s ss) = showParen (p > 10)+    $ showString "SingListCons "+    . showsPrecSing 11 s+    . showChar ' '+    . showsPrec 11 ss++instance ShowSing k => ShowSing [k] where+  showsPrecSing = showsPrec+ data SingMaybe :: Maybe k -> Type where   SingMaybeJust :: Sing a -> SingMaybe ('Just a)   SingMaybeNothing :: SingMaybe 'Nothing@@ -468,63 +790,79 @@ unreifyList SingListNil b = b unreifyList (SingListCons s ss) b = unreify s (unreifyList ss b) -data Some (f :: k -> Type) = forall a. Some !(Sing a) !(f a)--instance (EqForall f, EqSing k) => Eq (Some (f :: k -> Type)) where +instance (EqForeach f, EqSing k) => Eq (Some (f :: k -> Type)) where    Some s1 v1 == Some s2 v2 = case eqSing s1 s2 of-    Just Refl -> eqForall v1 v2+    Just Refl -> eqForeach s1 v1 v2     Nothing -> False +instance (OrdForeach f, OrdSing k) => Ord (Some (f :: k -> Type)) where +  compare (Some s1 v1) (Some s2 v2) = case compareSing s1 s2 of+    WitnessedOrderingEQ -> compareForeach s1 v1 v2+    WitnessedOrderingLT -> LT+    WitnessedOrderingGT -> GT++instance (ShowForeach f, ShowSing k) => Show (Some (f :: k -> Type)) where+  showsPrec p (Some s a) = showParen (p >= 11)+    $ showString "Sing "+    . showsPrecSing 11 s+    . showChar ' '+    . showsPrecForeach s 11 a+ class ToSing (f :: k -> Type) where   toSing :: f a -> Sing a  class ToJSONSing k where   toJSONSing :: forall (a :: k). Sing a -> Aeson.Value -instance (ToJSONForall f, ToJSONSing k) => ToJSON (Some (f :: k -> Type)) where-  toJSON (Some s v) = toJSON [toJSONSing s, toJSONForall v]+instance (ToJSONForeach f, ToJSONSing k) => ToJSON (Some (f :: k -> Type)) where+  toJSON (Some s v) = toJSON [toJSONSing s, toJSONForeach s v]  class FromJSONSing k where   parseJSONSing :: Aeson.Value -> Aeson.Parser (Exists (Sing :: k -> Type)) -instance (FromJSONForall f, FromJSONSing k) => FromJSON (Some (f :: k -> Type)) where+instance (FromJSONForeach f, FromJSONSing k) => FromJSON (Some (f :: k -> Type)) where   parseJSON = Aeson.withArray "Some" $ \v -> if V.length v == 2     then do       let x = V.unsafeIndex v 0           y = V.unsafeIndex v 1       Exists s <- parseJSONSing x :: Aeson.Parser (Exists (Sing :: k -> Type))-      val <- parseJSONForall s y+      val <- parseJSONForeach s y       return (Some s val)     else fail "array of length 2 expected" --- only used internally for its instances-newtype Apply f a = Apply { getApply :: f a }--instance EqForall f => Eq (Apply f a) where-  Apply a == Apply b = eqForall a b--instance OrdForall f => Ord (Apply f a) where-  compare (Apply a) (Apply b) = compareForall a b+-- This name is not great. I need to figure out a better naming+-- scheme that allows this area to grow.+toJSONMapForeachKey :: (ToJSONKeyForeach f, ToJSONForeach v)+  => Sing a+  -> Map (f a) (v a)+  -> Aeson.Value+toJSONMapForeachKey s m = case toJSONKeyForeach of+  ToJSONKeyTextForall keyToText _ -> toJSON $ M.foldlWithKey'+    ( \hm key val -> HM.insert (keyToText (Pair s key)) (toJSONForeach s val) hm+    ) HM.empty m+  ToJSONKeyValueForall keyToValue _ -> toJSON $ M.foldrWithKey' +    ( \key val xs -> (keyToValue (Pair s key), toJSONForeach s val) : xs+    ) [] m  -- | Parse a 'Map' whose key type is higher-kinded. This only creates a valid 'Map'---   if the 'OrdForall' instance agrees with the 'Ord' instance.-parseJSONMapForallKey :: forall f a v. (FromJSONKeyForall f, OrdForall f)+--   if the 'OrdForeach' instance agrees with the 'Ord' instance.+parseJSONMapForeachKey :: forall k (f :: k -> Type) (a :: k) v. (FromJSONKeyForeach f, OrdForeach f, Unreify k)   => (Aeson.Value -> Aeson.Parser v)    -> Sing a   -> Aeson.Value   -> Aeson.Parser (Map (f a) v)-parseJSONMapForallKey valueParser s obj = case fromJSONKeyForall of-  FromJSONKeyTextParserForall f -> Aeson.withObject "Map k v"-    ( fmap (M.mapKeysMonotonic getApply) . HM.foldrWithKey+parseJSONMapForeachKey valueParser s obj = unreify s $ case fromJSONKeyForeach of+  FromJSONKeyTextParserForeach f -> Aeson.withObject "Map k v"+    ( fmap (M.mapKeysMonotonic getApplyForeach) . HM.foldrWithKey       (\k v m -> M.insert-        <$> (coerce (f s k :: Aeson.Parser (f a)) :: Aeson.Parser (Apply f a)) <?> Key k+        <$> (coerce (f s k :: Aeson.Parser (f a)) :: Aeson.Parser (ApplyForeach f a)) <?> Key k         <*> valueParser v <?> Key k         <*> m       ) (pure M.empty)     ) obj-  FromJSONKeyValueForall f -> Aeson.withArray "Map k v"-    ( fmap (M.mapKeysMonotonic getApply . M.fromList)-    . (coerce :: Aeson.Parser [(f a, v)] -> Aeson.Parser [(Apply f a, v)])+  FromJSONKeyValueForeach f -> Aeson.withArray "Map k v"+    ( fmap (M.mapKeysMonotonic getApplyForeach . M.fromList)+    . (coerce :: Aeson.Parser [(f a, v)] -> Aeson.Parser [(ApplyForeach f a, v)])     . TRV.sequence     . zipWith (parseIndexedJSONPair (f s) valueParser) [0..]     . V.toList@@ -558,6 +896,26 @@   WitnessedOrderingEQ -> EQ   WitnessedOrderingLT -> LT +strengthenEquality :: Bool -> WitnessedEquality a a+strengthenEquality = \case+  True -> WitnessedEqualityEqual+  False -> WitnessedEqualityUnequal++-- | Given that we already know two types are equal, promote an 'Ordering'.+strengthenOrdering :: Ordering -> WitnessedOrdering a a                                +strengthenOrdering = \case+  LT -> WitnessedOrderingLT                                                    +  EQ -> WitnessedOrderingEQ                                                              +  GT -> WitnessedOrderingGT                                                                ++-- | Given that we already know two types to be unequal, promote an 'Ordering'.+-- The argument should not be @EQ@.+strengthenUnequalOrdering :: Ordering -> WitnessedOrdering a b                   +strengthenUnequalOrdering = \case                                                  +  LT -> WitnessedOrderingLT +  EQ -> WitnessedOrderingLT -- this case should not happen                                          +  GT -> WitnessedOrderingGT               + instance (EqForallPoly f, ToSing f, EqForeach g) => Eq (DependentPair f g) where   DependentPair a1 b1 == DependentPair a2 b2 = case eqForallPoly a1 a2 of     WitnessedEqualityUnequal -> False@@ -575,4 +933,13 @@     (showString "DependentPair " . showsPrecForall 11 a . showChar ' ' . showsPrecForeach (toSing a) 11 b)     s +instance Semigroup a => SemigroupForall (Const a) where+  appendForall (Const x) (Const y) = Const (x SG.<> y)++#if MIN_VERSION_base(4,11,0)+instance Monoid a => MonoidForall (Const a) where+#else+instance (Semigroup a, Monoid a) => MonoidForall (Const a) where+#endif+  emptyForall = Const mempty 
src/Data/Monoid/Lifted.hs view
@@ -5,19 +5,20 @@   , empty1   ) where -import Data.Functor.Identity+import Control.Applicative import Data.Functor.Compose-import qualified Data.Functor.Product as FP-import Data.Map.Strict (Map)+import Data.Functor.Identity import Data.HashMap.Strict (HashMap)-import Control.Applicative-import Data.Semigroup (Semigroup) import Data.Hashable (Hashable)+import Data.Map.Strict (Map) import Data.Monoid import Data.Proxy (Proxy(..))-import qualified Data.Semigroup as SG-import qualified Data.Map.Strict as M+import Data.Semigroup (Semigroup)+import Data.Functor.Const (Const(..))+import qualified Data.Functor.Product as FP import qualified Data.HashMap.Strict as HM+import qualified Data.Map.Strict as M+import qualified Data.Semigroup as SG  -- | Laws for this typeclass: --@@ -59,6 +60,9 @@ instance Ord k => Semigroup1 (Map k) where   liftAppend = M.unionWith +instance Ord k => Monoid1 (Map k) where+  liftEmpty _ = M.empty+ -- | Disagrees with 'Semigroup' instance for 'HashMap' instance (Hashable k, Eq k) => Semigroup1 (HashMap k) where   liftAppend = HM.unionWith@@ -107,4 +111,7 @@  instance Monoid1 ((->) a) where   liftEmpty b _ = b++instance Semigroup a => Semigroup1 (Const a) where+  liftAppend _ (Const x) (Const y) = Const (x SG.<> y) 
src/Topaz/Rec.hs view
@@ -30,16 +30,14 @@   , puts     -- * Conversion   , fromSingList+  , toSingList   ) where  import Prelude hiding (map,zipWith,foldMap,traverse) import Topaz.Types (Elem(..),type (++),Rec(..))-import Topaz.Types (Elem(..),Rec(..)) import Data.Exists-import Data.Proxy (Proxy(..)) import Data.Semigroup (Semigroup) import qualified Data.Semigroup as SG-import qualified Data.Vector as V  map :: (forall x. f x -> g x) -> Rec f as -> Rec g as map _ RecNil = RecNil@@ -117,4 +115,8 @@ fromSingList :: SingList as -> Rec Sing as fromSingList SingListNil = RecNil fromSingList (SingListCons r rs) = RecCons r (fromSingList rs)++toSingList :: Rec Sing as -> SingList as+toSingList RecNil = SingListNil+toSingList (RecCons r rs) = SingListCons r (toSingList rs) 
src/Topaz/Types.hs view
@@ -27,20 +27,22 @@   , type (++)   ) where +import Control.Applicative (liftA2) import Data.Exists-import Data.Hashable (Hashable(..))-import Foreign.Storable (Storable(..))-import Data.Type.Equality-import Data.Type.Coercion-import Data.Semigroup (Semigroup)-import Data.Proxy (Proxy(..))-import Foreign.Ptr (castPtr,plusPtr) import Data.Foldable (foldrM)+import Data.Hashable (Hashable(..)) import Data.Kind (Type) import Data.Monoid.Lifted (Semigroup1(..), Monoid1(..), append1)-import qualified Data.Semigroup as SG+import Data.Proxy (Proxy(..))+import Data.Semigroup (Semigroup)+import Data.Type.Coercion+import Data.Type.Equality+import Foreign.Ptr (castPtr,plusPtr)+import Foreign.Storable (Storable(..))+ import qualified Data.Aeson as AE import qualified Data.Aeson.Types as AET+import qualified Data.Semigroup as SG import qualified Data.Vector as V  data Nat = Succ Nat | Zero@@ -121,9 +123,6 @@     Just Coercion   testCoercion _ _ = Nothing -instance EqForall f => Eq (Rec f as) where-  (==) = eqForall- instance HashableForall f => HashableForall (Rec f) where   hashWithSaltForall s0 = go s0 where     go :: Int -> Rec f rs -> Int@@ -146,11 +145,37 @@ instance ShowForall f => Show (Rec f as) where   showsPrec = showsPrecForall +instance ShowForeach f => ShowForeach (Rec f) where+  showsPrecForeach SingListNil _ RecNil = showString "RecNil"+  showsPrecForeach (SingListCons s ss) p (RecCons v vs) = showParen (p > 10)+    $ showString "RecCons "+    . showsPrecForeach s 11 v+    . showString " "+    . showsPrecForeach ss 11 vs++instance EqForall f => Eq (Rec f as) where+  (==) = eqForall+ instance EqForall f => EqForall (Rec f) where   eqForall RecNil RecNil = True   eqForall (RecCons a as) (RecCons b bs) =     eqForall a b && eqForall as bs +instance EqForeach f => EqForeach (Rec f) where+  eqForeach SingListNil RecNil RecNil = True+  eqForeach (SingListCons s ss) (RecCons a as) (RecCons b bs) =+    eqForeach s a b && eqForeach ss as bs++instance EqForallPoly f => EqForallPoly (Rec f) where+  eqForallPoly RecNil RecNil = WitnessedEqualityEqual+  eqForallPoly RecNil (RecCons _ _) = WitnessedEqualityUnequal+  eqForallPoly (RecCons _ _) RecNil = WitnessedEqualityUnequal+  eqForallPoly (RecCons x xs) (RecCons y ys) = case eqForallPoly x y of+    WitnessedEqualityUnequal -> WitnessedEqualityUnequal+    WitnessedEqualityEqual -> case eqForallPoly xs ys of+      WitnessedEqualityUnequal -> WitnessedEqualityUnequal+      WitnessedEqualityEqual -> WitnessedEqualityEqual+ instance OrdForall f => Ord (Rec f as) where   compare = compareForall @@ -159,19 +184,26 @@   compareForall (RecCons a as) (RecCons b bs) =     mappend (compareForall a b) (compareForall as bs) +instance OrdForeach f => OrdForeach (Rec f) where+  compareForeach SingListNil RecNil RecNil = EQ+  compareForeach (SingListCons s ss) (RecCons a as) (RecCons b bs) =+    mappend (compareForeach s a b) (compareForeach ss as bs)++ instance SemigroupForall f => Semigroup (Rec f as) where-  (<>) = recZipWith sappendForall+  (<>) = recZipWith appendForall -instance (MonoidForall f, Reify as) => Monoid (Rec f as) where-  mempty = recMap memptyForall (singListToRec reify)-  mappend = recZipWith sappendForall+instance SemigroupForeach f => SemigroupForeach (Rec f) where+  appendForeach SingListNil RecNil RecNil = RecNil+  appendForeach (SingListCons s ss) (RecCons x xs) (RecCons y ys) =+    RecCons (appendForeach s x y) (appendForeach ss xs ys) -instance MonoidForall f => MonoidForall (Rec f) where-  memptyForall SingListNil = RecNil-  memptyForall (SingListCons s ss) = RecCons (memptyForall s) (memptyForall ss)+instance MonoidForeach f => MonoidForeach (Rec f) where+  emptyForeach SingListNil = RecNil+  emptyForeach (SingListCons s ss) = RecCons (emptyForeach s) (emptyForeach ss)  instance SemigroupForall f => SemigroupForall (Rec f) where-  sappendForall = recZipWith sappendForall+  appendForall = recZipWith appendForall  instance ToJSONForall f => AE.ToJSON (Rec f as) where   toJSON = toJSONForall@@ -183,46 +215,52 @@     go RecNil = []     go (RecCons x xs) = toJSONForall x : go xs -instance (FromJSONForall f, Reify as) => AE.FromJSON (Rec f as) where-  parseJSON = parseJSONForall reify+instance (FromJSONForeach f, Reify as) => AE.FromJSON (Rec f as) where+  parseJSON = parseJSONForeach reify -instance FromJSONForall f => FromJSONForall (Rec f) where-  parseJSONForall s0 = AE.withArray "Rec" $ \vs -> do+instance FromJSONForeach f => FromJSONForeach (Rec f) where+  parseJSONForeach s0 = AE.withArray "Rec" $ \vs -> do     let go :: SingList as -> Int -> AET.Parser (Rec f as)         go SingListNil !ix = if V.length vs == ix           then return RecNil           else fail "too many elements in array"         go (SingListCons s ss) !ix = if ix < V.length vs           then do-            r <- parseJSONForall s (vs V.! ix)+            r <- parseJSONForeach s (vs V.! ix)             rs <- go ss (ix + 1)             return (RecCons r rs)           else fail "not enough elements in array"     go s0 0 -instance StorableForall f => StorableForall (Rec f) where-  sizeOfFunctorForall RecNil = 0-  sizeOfFunctorForall (RecCons r rs) =-    sizeOfFunctorForall r + sizeOfFunctorForall rs-  sizeOfForall _ SingListNil = 0-  sizeOfForall _ (SingListCons s ss) =-    sizeOfForall (Proxy :: Proxy f) s + sizeOfForall (Proxy :: Proxy (Rec f)) ss-  peekForall SingListNil _ = return RecNil-  peekForall (SingListCons s ss) ptr = do-    r <- peekForall s (castPtr ptr)-    rs <- peekForall ss (plusPtr ptr (sizeOfForall (Proxy :: Proxy f) s))+instance StorableForeach f => StorableForeach (Rec f) where+  sizeOfForeach _ SingListNil = 0+  sizeOfForeach _ (SingListCons s ss) =+    sizeOfForeach (Proxy :: Proxy f) s + sizeOfForeach (Proxy :: Proxy (Rec f)) ss+  peekForeach SingListNil _ = return RecNil+  peekForeach (SingListCons s ss) ptr = do+    r <- peekForeach s (castPtr ptr)+    rs <- peekForeach ss (plusPtr ptr (sizeOfForeach (Proxy :: Proxy f) s))     return (RecCons r rs)-  pokeForall _ RecNil = return ()-  pokeForall ptr (RecCons r rs) = do-    pokeForall (castPtr ptr) r-    pokeForall (plusPtr ptr (sizeOfFunctorForall r)) rs+  pokeForeach _ _ RecNil = return ()+  pokeForeach (SingListCons s ss) ptr (RecCons r rs) = do+    pokeForeach s (castPtr ptr) r+    pokeForeach ss (plusPtr ptr (sizeOfForeach (Proxy :: Proxy f) s)) rs -instance (StorableForall f, Reify as) => Storable (Rec f as) where-  sizeOf _ = sizeOfForall (Proxy :: Proxy (Rec f)) (reify :: SingList as)+instance (StorableForeach f, Reify as) => Storable (Rec f as) where+  sizeOf _ = sizeOfForeach (Proxy :: Proxy (Rec f)) (reify :: SingList as)   alignment _ = sizeOf (undefined :: Rec f as)-  poke = pokeForall-  peek = peekForall (reify :: SingList as)+  poke = pokeForeach (reify :: SingList as)+  peek = peekForeach (reify :: SingList as) +instance BinaryForeach f => BinaryForeach (Rec f) where+  putForeach SingListNil RecNil = return ()+  putForeach (SingListCons s ss) (RecCons r rs) = do+    putForeach s r+    putForeach ss rs+  getForeach SingListNil = return RecNil+  getForeach (SingListCons s ss) =+    liftA2 RecCons (getForeach s) (getForeach ss)+ instance FromJSONExists f => FromJSONExists (Rec f) where   parseJSONExists = AE.withArray "Rec" $ \vs ->      foldrM go (Exists RecNil) vs@@ -232,16 +270,8 @@       Exists r <- parseJSONExists v :: AET.Parser (Exists g)       return (Exists (RecCons r rs)) -singListToRec :: SingList as -> Rec Sing as-singListToRec SingListNil = RecNil-singListToRec (SingListCons r rs) = RecCons r (singListToRec rs)- recZipWith :: (forall x. f x -> g x -> h x) -> Rec f rs -> Rec g rs -> Rec h rs recZipWith _ RecNil RecNil = RecNil recZipWith f (RecCons a as) (RecCons b bs) =   RecCons (f a b) (recZipWith f as bs)--recMap :: (forall x. f x -> g x) -> Rec f as -> Rec g as-recMap _ RecNil = RecNil-recMap f (RecCons x xs) = RecCons (f x) (recMap f xs)