{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UnboxedTuples #-}

{-# OPTIONS_GHC -Wall #-}

{-| Data types and type classes for working with existentially quantified
    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
  ( -- * Data Types
    Exists(..)
  , Exists2(..)
  , Exists3(..)
  , Some(..)
  , DependentPair(..)
  , WitnessedEquality(..)
  , WitnessedOrdering(..)
  , ApplyForall(..)
  , ApplyForeach(..)
  , ApplyLifted(..)
    -- * Type Classes
  , EqForall(..)
  , EqForallPoly(..)
  , EqForeach(..)
  , OrdForall(..)
  , OrdForallPoly(..)
  , OrdForeach(..)
  , ShowForall(..)
  , ShowForeach(..)
  , ReadExists(..)
  , EnumForall(..)
  , EnumExists(..)
  , BoundedExists(..)
  , SemigroupForall(..)
  , SemigroupForeach(..)
  , MonoidForall(..)
  , MonoidForeach(..)
  , HashableForall(..)
  , HashableForeach(..)
  , PathPieceExists(..)
  , FromJSONForall(..) 
  , FromJSONForeach(..)
  , FromJSONExists(..)
  , ToJSONForall(..)
  , ToJSONForeach(..)
  , ToJSONKeyFunctionForall(..)
  , FromJSONKeyFunctionForeach(..)
  , ToJSONKeyForall(..)
  , ToJSONKeyForeach(..)
  , FromJSONKeyExists(..)
  , FromJSONKeyForeach(..)
  , StorableForeach(..)
  , StorableForall(..)
  , PrimForall(..)
  , BinaryExists(..)
  , BinaryForeach(..)
    -- * Higher Rank Classes
  , EqForall2(..)
  , EqForallPoly2(..)
  , ShowForall2(..)
  , ShowForeach2(..)
  , BinaryExists2(..)
    -- * More Type Classes
  , Sing
  , SingList(..)
  , SingMaybe(..)
  , Reify(..)
  , Unreify(..)
    -- * Sing Type Classes
  , EqSing(..)
  , OrdSing(..)
  , ShowSing(..)
  , ToJSONSing(..)
  , FromJSONSing(..)
  , ToSing(..)
  , SingKind(..)
    -- * Functions
    -- ** Show
  , showsForall
  , showsForeach
  , showForall
  , showListForall
  , showListForeach
  , showsForall2
  , showForall2
    -- ** Defaulting
  , defaultEqForallPoly
  , defaultCompareForallPoly
  , parseJSONMapForeachKey
  , toJSONMapForeachKey
    -- ** Weakening
  , weakenEquality
  , weakenOrdering
  , strengthenEquality
  , strengthenOrdering
  , strengthenUnequalOrdering
    -- ** Other
  , unreifyList
  ) where

import Control.Applicative (Const(..))
import Data.Aeson (ToJSON(..),FromJSON(..))
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 Data.Functor.Product (Product(..))
import Data.Functor.Sum (Sum(..))
import Data.Hashable (Hashable(..))
import Data.Kind (Type)
import Data.Map.Strict (Map)
import Data.Monoid.Lifted (Semigroup1(..),Monoid1(..),append1,empty1)
import Data.Proxy (Proxy(..))
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.Key as Key
import qualified Data.Aeson.KeyMap as KM
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 Text.Read as R
import qualified Web.PathPieces as PP

-- | Hide a type parameter.
data Exists (f :: k -> Type) = forall a. Exists !(f a)

-- | Hide two type parameters.
data Exists2 (f :: k -> j -> Type) = forall a b. Exists2 !(f a b)

-- | 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

data WitnessedOrdering (a :: k) (b :: k) where
  WitnessedOrderingLT :: WitnessedOrdering a b
  WitnessedOrderingEQ :: WitnessedOrdering a a
  WitnessedOrderingGT :: WitnessedOrdering a b

data ToJSONKeyFunctionForall f
  = ToJSONKeyTextForall !(forall a. f a -> Aeson.Key) !(forall a. f a -> Aeson.Encoding' Aeson.Key)
  | ToJSONKeyValueForall !(forall a. f a -> Aeson.Value) !(forall a. f a -> Aeson.Encoding)
data FromJSONKeyFunctionForeach f
  = FromJSONKeyTextParserForeach !(forall a. Sing a -> Aeson.Key -> Aeson.Parser (f a))
  | FromJSONKeyValueForeach !(forall a. Sing a -> Aeson.Value -> Aeson.Parser (f a))

newtype ApplyForall f a = ApplyForall { forall {k} (f :: k -> *) (a :: k). ApplyForall f a -> f a
getApplyForall :: f a }

instance ShowForall f => Show (ApplyForall f a) where
  showsPrec :: Int -> ApplyForall f a -> ShowS
showsPrec Int
p (ApplyForall f a
x) = Bool -> ShowS -> ShowS
showParen (Int
p forall a. Ord a => a -> a -> Bool
> Int
10)
    forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"ApplyForall "
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k).
ShowForall f =>
Int -> f a -> ShowS
showsPrecForall Int
11 f a
x

instance SemigroupForall f => Semigroup (ApplyForall f a) where
  <> :: ApplyForall f a -> ApplyForall f a -> ApplyForall f a
(<>) = forall {k} (f :: k -> *) (a :: k).
SemigroupForall f =>
f a -> f a -> f a
appendForall

instance MonoidForall f => Monoid (ApplyForall f a) where
  mempty :: ApplyForall f a
mempty = forall {k} (f :: k -> *) (a :: k). MonoidForall f => f a
emptyForall
  mappend :: ApplyForall f a -> ApplyForall f a -> ApplyForall f a
mappend = forall a. Semigroup a => a -> a -> a
(SG.<>)

instance SemigroupForall f => SemigroupForall (ApplyForall f) where
  appendForall :: forall (a :: k).
ApplyForall f a -> ApplyForall f a -> ApplyForall f a
appendForall (ApplyForall f a
a) (ApplyForall f a
b) = forall {k} (f :: k -> *) (a :: k). f a -> ApplyForall f a
ApplyForall (forall {k} (f :: k -> *) (a :: k).
SemigroupForall f =>
f a -> f a -> f a
appendForall f a
a f a
b)

instance MonoidForall f => MonoidForall (ApplyForall f) where
  emptyForall :: forall (a :: k). ApplyForall f a
emptyForall = forall {k} (f :: k -> *) (a :: k). f a -> ApplyForall f a
ApplyForall forall {k} (f :: k -> *) (a :: k). MonoidForall f => f a
emptyForall

newtype ApplyLifted f a = ApplyLifted { forall {k} (f :: k -> *) (a :: k). ApplyLifted f a -> f a
getApplyLifted :: f a }                         

instance (Semigroup1 f, Semigroup a) => Semigroup (ApplyLifted f a) where  
  <> :: ApplyLifted f a -> ApplyLifted f a -> ApplyLifted f a
(<>) = forall (f :: * -> *) a.
(Semigroup1 f, Semigroup a) =>
f a -> f a -> f a
append1

instance (Monoid1 f, Monoid a) => Monoid (ApplyLifted f a) where
  mempty :: ApplyLifted f a
mempty = forall (f :: * -> *) a. (Monoid1 f, Monoid a) => f a
empty1 
  mappend :: ApplyLifted f a -> ApplyLifted f a -> ApplyLifted f a
mappend = forall a. Semigroup a => a -> a -> a
(<>)

instance (Eq1 f, Eq a) => Eq (ApplyLifted f a) where
  == :: ApplyLifted f a -> ApplyLifted f a -> Bool
(==) = forall (f :: * -> *) a. (Eq1 f, Eq a) => f a -> f a -> Bool
eq1 

instance (Ord1 f, Ord a) => Ord (ApplyLifted f a) where
  compare :: ApplyLifted f a -> ApplyLifted f a -> Ordering
compare = forall (f :: * -> *) a. (Ord1 f, Ord a) => f a -> f a -> Ordering
compare1 

instance Semigroup1 f => Semigroup1 (ApplyLifted f) where  
  liftAppend :: forall a.
(a -> a -> a)
-> ApplyLifted f a -> ApplyLifted f a -> ApplyLifted f a
liftAppend a -> a -> a
g (ApplyLifted f a
a) (ApplyLifted f a
b) = forall {k} (f :: k -> *) (a :: k). f a -> ApplyLifted f a
ApplyLifted (forall (f :: * -> *) a.
Semigroup1 f =>
(a -> a -> a) -> f a -> f a -> f a
liftAppend a -> a -> a
g f a
a f a
b)                        

instance Monoid1 f => Monoid1 (ApplyLifted f) where        
  liftEmpty :: forall a. a -> ApplyLifted f a
liftEmpty a
f = forall {k} (f :: k -> *) (a :: k). f a -> ApplyLifted f a
ApplyLifted (forall (f :: * -> *) a. Monoid1 f => a -> f a
liftEmpty a
f)                                        

instance Eq1 f => Eq1 (ApplyLifted f) where
  liftEq :: forall a b.
(a -> b -> Bool) -> ApplyLifted f a -> ApplyLifted f b -> Bool
liftEq a -> b -> Bool
f (ApplyLifted f a
a) (ApplyLifted f b
b) = forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq a -> b -> Bool
f f a
a f b
b

instance Ord1 f => Ord1 (ApplyLifted f) where
  liftCompare :: forall a b.
(a -> b -> Ordering)
-> ApplyLifted f a -> ApplyLifted f b -> Ordering
liftCompare a -> b -> Ordering
f (ApplyLifted f a
a) (ApplyLifted f b
b) = forall (f :: * -> *) a b.
Ord1 f =>
(a -> b -> Ordering) -> f a -> f b -> Ordering
liftCompare a -> b -> Ordering
f f a
a f b
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 { forall {k} (f :: k -> *) (a :: k). ApplyForeach f a -> f a
getApplyForeach :: f a }

instance (EqForeach f, Reify a) => Eq (ApplyForeach f a) where
  ApplyForeach f a
a == :: ApplyForeach f a -> ApplyForeach f a -> Bool
== ApplyForeach f a
b = forall {k} (f :: k -> *) (a :: k).
EqForeach f =>
Sing a -> f a -> f a -> Bool
eqForeach forall {k} (a :: k). Reify a => Sing a
reify f a
a f a
b

instance (OrdForeach f, Reify a) => Ord (ApplyForeach f a) where
  compare :: ApplyForeach f a -> ApplyForeach f a -> Ordering
compare (ApplyForeach f a
a) (ApplyForeach f a
b) = forall {k} (f :: k -> *) (a :: k).
OrdForeach f =>
Sing a -> f a -> f a -> Ordering
compareForeach forall {k} (a :: k). Reify a => Sing a
reify f a
a f a
b

instance (ShowForeach f, Reify a) => Show (ApplyForeach f a) where
  showsPrec :: Int -> ApplyForeach f a -> ShowS
showsPrec Int
p (ApplyForeach f a
a) = Bool -> ShowS -> ShowS
showParen (Int
p forall a. Ord a => a -> a -> Bool
> Int
10)
    forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"ApplyForeach "
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k).
ShowForeach f =>
Sing a -> Int -> f a -> ShowS
showsPrecForeach forall {k} (a :: k). Reify a => Sing a
reify Int
11 f a
a

instance (SemigroupForeach f, Reify a) => Semigroup (ApplyForeach f a) where
  <> :: ApplyForeach f a -> ApplyForeach f a -> ApplyForeach f a
(<>) = forall {k} (f :: k -> *) (a :: k).
SemigroupForeach f =>
Sing a -> f a -> f a -> f a
appendForeach forall {k} (a :: k). Reify a => Sing a
reify

instance (MonoidForeach f, Reify a) => Monoid (ApplyForeach f a) where
  mempty :: ApplyForeach f a
mempty = forall {k} (f :: k -> *) (a :: k). MonoidForeach f => Sing a -> f a
emptyForeach forall {k} (a :: k). Reify a => Sing a
reify
  mappend :: ApplyForeach f a -> ApplyForeach f a -> ApplyForeach f a
mappend = forall a. Semigroup a => a -> a -> a
(SG.<>)

instance (ToJSONForeach f, Reify a) => ToJSON (ApplyForeach f a) where
  toJSON :: ApplyForeach f a -> Value
toJSON = forall {k} (f :: k -> *) (a :: k).
ToJSONForeach f =>
Sing a -> f a -> Value
toJSONForeach forall {k} (a :: k). Reify a => Sing a
reify

instance (FromJSONForeach f, Reify a) => FromJSON (ApplyForeach f a) where
  parseJSON :: Value -> Parser (ApplyForeach f a)
parseJSON = forall {k} (f :: k -> *) (a :: k).
FromJSONForeach f =>
Sing a -> Value -> Parser (f a)
parseJSONForeach forall {k} (a :: k). Reify a => Sing a
reify

instance EqForeach f => EqForeach (ApplyForeach f) where
  eqForeach :: forall (a :: k).
Sing a -> ApplyForeach f a -> ApplyForeach f a -> Bool
eqForeach Sing a
s (ApplyForeach f a
a) (ApplyForeach f a
b) = forall {k} (f :: k -> *) (a :: k).
EqForeach f =>
Sing a -> f a -> f a -> Bool
eqForeach Sing a
s f a
a f a
b

instance OrdForeach f => OrdForeach (ApplyForeach f) where
  compareForeach :: forall (a :: k).
Sing a -> ApplyForeach f a -> ApplyForeach f a -> Ordering
compareForeach Sing a
s (ApplyForeach f a
a) (ApplyForeach f a
b) = forall {k} (f :: k -> *) (a :: k).
OrdForeach f =>
Sing a -> f a -> f a -> Ordering
compareForeach Sing a
s f a
a f a
b

instance SemigroupForeach f => SemigroupForeach (ApplyForeach f) where
  appendForeach :: forall (a :: k).
Sing a -> ApplyForeach f a -> ApplyForeach f a -> ApplyForeach f a
appendForeach Sing a
s (ApplyForeach f a
a) (ApplyForeach f a
b) = forall {k} (f :: k -> *) (a :: k). f a -> ApplyForeach f a
ApplyForeach (forall {k} (f :: k -> *) (a :: k).
SemigroupForeach f =>
Sing a -> f a -> f a -> f a
appendForeach Sing a
s f a
a f a
b)

instance MonoidForeach f => MonoidForeach (ApplyForeach f) where
  emptyForeach :: forall (a :: k). Sing a -> ApplyForeach f a
emptyForeach Sing a
s = forall {k} (f :: k -> *) (a :: k). f a -> ApplyForeach f a
ApplyForeach (forall {k} (f :: k -> *) (a :: k). MonoidForeach f => Sing a -> f a
emptyForeach Sing a
s)

instance ToJSONForeach f => ToJSONForeach (ApplyForeach f) where
  toJSONForeach :: forall (a :: k). Sing a -> ApplyForeach f a -> Value
toJSONForeach Sing a
s (ApplyForeach f a
x) = forall {k} (f :: k -> *) (a :: k).
ToJSONForeach f =>
Sing a -> f a -> Value
toJSONForeach Sing a
s f a
x

instance FromJSONForeach f => FromJSONForeach (ApplyForeach f) where
  parseJSONForeach :: forall (a :: k). Sing a -> Value -> Parser (ApplyForeach f a)
parseJSONForeach Sing a
s = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {k} (f :: k -> *) (a :: k). f a -> ApplyForeach f a
ApplyForeach forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k).
FromJSONForeach f =>
Sing a -> Value -> Parser (f a)
parseJSONForeach Sing a
s

instance ToJSONKeyForeach f => ToJSONKeyForeach (ApplyForeach f) where
  toJSONKeyForeach :: ToJSONKeyFunctionForall (Product Sing (ApplyForeach f))
toJSONKeyForeach = case forall {k} (f :: k -> *).
ToJSONKeyForeach f =>
ToJSONKeyFunctionForall (Product Sing f)
toJSONKeyForeach of
    ToJSONKeyTextForall forall (a :: k). Product Sing f a -> Key
f forall (a :: k). Product Sing f a -> Encoding' Key
g -> forall {k} (f :: k -> *).
(forall (a :: k). f a -> Key)
-> (forall (a :: k). f a -> Encoding' Key)
-> ToJSONKeyFunctionForall f
ToJSONKeyTextForall
      (\(Pair Sing a
s (ApplyForeach f a
x)) -> forall (a :: k). Product Sing f a -> Key
f (forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair Sing a
s f a
x))
      (\(Pair Sing a
s (ApplyForeach f a
x)) -> forall (a :: k). Product Sing f a -> Encoding' Key
g (forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair Sing a
s f a
x))
    ToJSONKeyValueForall forall (a :: k). Product Sing f a -> Value
f forall (a :: k). Product Sing f a -> Encoding
g -> forall {k} (f :: k -> *).
(forall (a :: k). f a -> Value)
-> (forall (a :: k). f a -> Encoding) -> ToJSONKeyFunctionForall f
ToJSONKeyValueForall
      (\(Pair Sing a
s (ApplyForeach f a
x)) -> forall (a :: k). Product Sing f a -> Value
f (forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair Sing a
s f a
x))
      (\(Pair Sing a
s (ApplyForeach f a
x)) -> forall (a :: k). Product Sing f a -> Encoding
g (forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair Sing a
s f a
x))

instance FromJSONKeyForeach f => FromJSONKeyForeach (ApplyForeach f) where
  fromJSONKeyForeach :: FromJSONKeyFunctionForeach (ApplyForeach f)
fromJSONKeyForeach = case forall {k} (f :: k -> *).
FromJSONKeyForeach f =>
FromJSONKeyFunctionForeach f
fromJSONKeyForeach of
    FromJSONKeyTextParserForeach forall (a :: k). Sing a -> Key -> Parser (f a)
f -> forall {k} (f :: k -> *).
(forall (a :: k). Sing a -> Key -> Parser (f a))
-> FromJSONKeyFunctionForeach f
FromJSONKeyTextParserForeach (\Sing a
s Key
t -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {k} (f :: k -> *) (a :: k). f a -> ApplyForeach f a
ApplyForeach (forall (a :: k). Sing a -> Key -> Parser (f a)
f Sing a
s Key
t))
    FromJSONKeyValueForeach forall (a :: k). Sing a -> Value -> Parser (f a)
f -> forall {k} (f :: k -> *).
(forall (a :: k). Sing a -> Value -> Parser (f a))
-> FromJSONKeyFunctionForeach f
FromJSONKeyValueForeach (\Sing a
s Value
t -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {k} (f :: k -> *) (a :: k). f a -> ApplyForeach f a
ApplyForeach (forall (a :: k). Sing a -> Value -> Parser (f a)
f Sing a
s Value
t))

instance (ToJSONKeyForeach f, Reify a) => ToJSONKey (ApplyForeach f a) where
  toJSONKey :: ToJSONKeyFunction (ApplyForeach f a)
toJSONKey = case forall {k} (f :: k -> *).
ToJSONKeyForeach f =>
ToJSONKeyFunctionForall (Product Sing f)
toJSONKeyForeach of
    ToJSONKeyTextForall forall (a :: k). Product Sing f a -> Key
toText forall (a :: k). Product Sing f a -> Encoding' Key
toEnc -> forall a. (a -> Key) -> (a -> Encoding' Key) -> ToJSONKeyFunction a
ToJSONKeyText
      (\(ApplyForeach f a
x) -> forall (a :: k). Product Sing f a -> Key
toText (forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair forall {k} (a :: k). Reify a => Sing a
reify f a
x))
      (\(ApplyForeach f a
x) -> forall (a :: k). Product Sing f a -> Encoding' Key
toEnc (forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair forall {k} (a :: k). Reify a => Sing a
reify f a
x))
    ToJSONKeyValueForall forall (a :: k). Product Sing f a -> Value
toValue forall (a :: k). Product Sing f a -> Encoding
toEnc -> forall a. (a -> Value) -> (a -> Encoding) -> ToJSONKeyFunction a
ToJSONKeyValue
      (\(ApplyForeach f a
x) -> forall (a :: k). Product Sing f a -> Value
toValue (forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair forall {k} (a :: k). Reify a => Sing a
reify f a
x))
      (\(ApplyForeach f a
x) -> forall (a :: k). Product Sing f a -> Encoding
toEnc (forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair forall {k} (a :: k). Reify a => Sing a
reify f a
x))
  toJSONKeyList :: ToJSONKeyFunction [ApplyForeach f a]
toJSONKeyList = case forall {k} (f :: k -> *).
ToJSONKeyForeach f =>
ToJSONKeyFunctionForall (Product Sing f)
toJSONKeyForeach of
    ToJSONKeyTextForall forall (a :: k). Product Sing f a -> Key
toText forall (a :: k). Product Sing f a -> Encoding' Key
toEnc -> forall a. (a -> Value) -> (a -> Encoding) -> ToJSONKeyFunction a
ToJSONKeyValue
      (\[ApplyForeach f a]
xs -> forall a. ToJSON a => a -> Value
toJSON forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\(ApplyForeach f a
x) -> forall (a :: k). Product Sing f a -> Key
toText (forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair forall {k} (a :: k). Reify a => Sing a
reify f a
x)) [ApplyForeach f a]
xs)
      (\[ApplyForeach f a]
xs -> forall a. (a -> Encoding) -> [a] -> Encoding
Aeson.list (Encoding' Key -> Encoding
textEncodingToValueEncoding forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: k). Product Sing f a -> Encoding' Key
toEnc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair forall {k} (a :: k). Reify a => Sing a
reify) (forall a b. (a -> b) -> [a] -> [b]
map forall {k} (f :: k -> *) (a :: k). ApplyForeach f a -> f a
getApplyForeach [ApplyForeach f a]
xs))
    ToJSONKeyValueForall forall (a :: k). Product Sing f a -> Value
toValue forall (a :: k). Product Sing f a -> Encoding
toEnc -> forall a. (a -> Value) -> (a -> Encoding) -> ToJSONKeyFunction a
ToJSONKeyValue
      (\[ApplyForeach f a]
xs -> forall a. ToJSON a => a -> Value
toJSON forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\(ApplyForeach f a
x) -> forall (a :: k). Product Sing f a -> Value
toValue (forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair forall {k} (a :: k). Reify a => Sing a
reify f a
x)) [ApplyForeach f a]
xs)
      (\[ApplyForeach f a]
xs -> forall a. (a -> Encoding) -> [a] -> Encoding
Aeson.list (forall (a :: k). Product Sing f a -> Encoding
toEnc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair forall {k} (a :: k). Reify a => Sing a
reify) (forall a b. (a -> b) -> [a] -> [b]
map forall {k} (f :: k -> *) (a :: k). ApplyForeach f a -> f a
getApplyForeach [ApplyForeach f a]
xs))

-- this is always safe
textEncodingToValueEncoding :: Aeson.Encoding' Aeson.Key -> Aeson.Encoding' Aeson.Value
textEncodingToValueEncoding :: Encoding' Key -> Encoding
textEncodingToValueEncoding = forall a b. Encoding' a -> Encoding' b
AEI.retagEncoding

instance (FromJSONKeyForeach f, Reify a) => FromJSONKey (ApplyForeach f a) where
  fromJSONKey :: FromJSONKeyFunction (ApplyForeach f a)
fromJSONKey = case forall {k} (f :: k -> *).
FromJSONKeyForeach f =>
FromJSONKeyFunctionForeach f
fromJSONKeyForeach of
    FromJSONKeyTextParserForeach forall (a :: k). Sing a -> Key -> Parser (f a)
f -> forall a. (Text -> Parser a) -> FromJSONKeyFunction a
FromJSONKeyTextParser (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {k} (f :: k -> *) (a :: k). f a -> ApplyForeach f a
ApplyForeach forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: k). Sing a -> Key -> Parser (f a)
f forall {k} (a :: k). Reify a => Sing a
reify forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Key
Key.fromText)
    FromJSONKeyValueForeach forall (a :: k). Sing a -> Value -> Parser (f a)
f -> forall a. (Value -> Parser a) -> FromJSONKeyFunction a
FromJSONKeyValue (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {k} (f :: k -> *) (a :: k). f a -> ApplyForeach f a
ApplyForeach forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: k). Sing a -> Value -> Parser (f a)
f forall {k} (a :: k). Reify a => Sing a
reify)
  fromJSONKeyList :: FromJSONKeyFunction [ApplyForeach f a]
fromJSONKeyList = case forall {k} (f :: k -> *).
FromJSONKeyForeach f =>
FromJSONKeyFunctionForeach f
fromJSONKeyForeach of
    FromJSONKeyTextParserForeach forall (a :: k). Sing a -> Key -> Parser (f a)
f -> forall a. (Value -> Parser a) -> FromJSONKeyFunction a
FromJSONKeyValue forall a b. (a -> b) -> a -> b
$ forall a. String -> (Array -> Parser a) -> Value -> Parser a
Aeson.withArray String
"ApplyForeach" forall a b. (a -> b) -> a -> b
$ \Array
xs -> do
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Vector a -> [a]
V.toList (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {k} (f :: k -> *) (a :: k). f a -> ApplyForeach f a
ApplyForeach forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. String -> (Text -> Parser a) -> Value -> Parser a
Aeson.withText String
"ApplyForeach" (forall (a :: k). Sing a -> Key -> Parser (f a)
f forall {k} (a :: k). Reify a => Sing a
reify forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Key
Key.fromText)) Array
xs)
    FromJSONKeyValueForeach forall (a :: k). Sing a -> Value -> Parser (f a)
f -> forall a. (Value -> Parser a) -> FromJSONKeyFunction a
FromJSONKeyValue forall a b. (a -> b) -> a -> b
$ forall a. String -> (Array -> Parser a) -> Value -> Parser a
Aeson.withArray String
"ApplyForeach" forall a b. (a -> b) -> a -> b
$ \Array
xs -> do
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Vector a -> [a]
V.toList (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {k} (f :: k -> *) (a :: k). f a -> ApplyForeach f a
ApplyForeach forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: k). Sing a -> Value -> Parser (f a)
f forall {k} (a :: k). Reify a => Sing a
reify) Array
xs)

class EqForall f where
  eqForall :: f a -> f a -> Bool

-- | Variant of 'EqForall' that requires a pi-quantified type.
class EqForeach f where
  eqForeach :: Sing a -> f a -> f a -> Bool

class EqForall f => OrdForall f where
  compareForall :: f a -> f a -> Ordering

class EqForall f => EqForallPoly f where
  eqForallPoly :: f a -> f b -> WitnessedEquality a b
  default eqForallPoly :: TestEquality f => f a -> f b -> WitnessedEquality a b
  eqForallPoly = forall {k} (f :: k -> *) (a :: k) (b :: k).
(TestEquality f, EqForall f) =>
f a -> f b -> WitnessedEquality a b
defaultEqForallPoly

-- the default method does not work if your data type is a newtype wrapper
-- over a function, but that should not really ever happen.
class (OrdForall f, EqForallPoly f) => OrdForallPoly f where
  compareForallPoly :: f a -> f b -> WitnessedOrdering a b

-- | Variant of 'OrdForall' that requires a pi-quantified type.
class EqForeach f => OrdForeach f where
  compareForeach :: Sing a -> f a -> f a -> Ordering

class ShowForall f where
  showsPrecForall :: Int -> f a -> ShowS

class ShowForeach f where
  showsPrecForeach :: Sing a -> Int -> f a -> ShowS

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 :: forall {k} (f :: k -> *) (a :: k). ShowForall f => f a -> ShowS
showsForall = forall {k} (f :: k -> *) (a :: k).
ShowForall f =>
Int -> f a -> ShowS
showsPrecForall Int
0

showsForeach :: ShowForeach f => Sing a -> f a -> ShowS
showsForeach :: forall {k} (f :: k -> *) (a :: k).
ShowForeach f =>
Sing a -> f a -> ShowS
showsForeach Sing a
s = forall {k} (f :: k -> *) (a :: k).
ShowForeach f =>
Sing a -> Int -> f a -> ShowS
showsPrecForeach Sing a
s Int
0

showForall :: ShowForall f => f a -> String
showForall :: forall {k} (f :: k -> *) (a :: k). ShowForall f => f a -> String
showForall f a
x = forall {k} (f :: k -> *) (a :: k). ShowForall f => f a -> ShowS
showsForall f a
x String
""

showsForall2 :: ShowForall2 f => f a b -> ShowS
showsForall2 :: forall {k} {k} (f :: k -> k -> *) (a :: k) (b :: k).
ShowForall2 f =>
f a b -> ShowS
showsForall2 = forall {k} {k} (f :: k -> k -> *) (a :: k) (b :: k).
ShowForall2 f =>
Int -> f a b -> ShowS
showsPrecForall2 Int
0

showForall2 :: ShowForall2 f => f a b -> String
showForall2 :: forall {k} {k} (f :: k -> k -> *) (a :: k) (b :: k).
ShowForall2 f =>
f a b -> String
showForall2 f a b
x = forall {k} {k} (f :: k -> k -> *) (a :: k) (b :: k).
ShowForall2 f =>
f a b -> ShowS
showsForall2 f a b
x String
""

class ReadExists f where
  readPrecExists :: R.ReadPrec (Exists f)

class EqForall2 f where
  eqForall2 :: f a b -> f a b -> 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 FromJSONKeyForeach f where
  fromJSONKeyForeach :: FromJSONKeyFunctionForeach f

class ToJSONForall f where
  toJSONForall :: f a -> Aeson.Value

class ToJSONForeach f where
  toJSONForeach :: Sing a -> f a -> Aeson.Value

class FromJSONForall f where
  parseJSONForall :: Sing a -> Aeson.Value -> Aeson.Parser (f a)

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 -> f a
  fromEnumForall :: f a -> Int

class EnumExists f where
  toEnumExists :: Int -> Exists f
  fromEnumExists :: Exists f -> Int

class BoundedExists f where
  minBoundExists :: Exists f
  maxBoundExists :: Exists f

class PathPieceExists f where
  fromPathPieceForall :: Text -> Maybe (Exists f)
  toPathPieceForall :: Exists f -> Text

class SemigroupForeach f where
  appendForeach :: Sing a -> f a -> f a -> f a

class SemigroupForall f where
  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 :: Ptr (f a) -> IO (f a)
  pokeForall :: Ptr (f a) -> f a -> IO ()
  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
--------------------

instance EqForall Proxy where
  eqForall :: forall (a :: k). Proxy a -> Proxy a -> Bool
eqForall Proxy a
_ Proxy a
_ = Bool
True

instance OrdForall Proxy where
  compareForall :: forall (a :: k). Proxy a -> Proxy a -> Ordering
compareForall Proxy a
_ Proxy a
_ = Ordering
EQ

instance ShowForall Proxy where
  showsPrecForall :: forall (a :: k). Int -> Proxy a -> ShowS
showsPrecForall = forall a. Show a => Int -> a -> ShowS
showsPrec

instance ReadExists Proxy where
  readPrecExists :: ReadPrec (Exists Proxy)
readPrecExists = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k (f :: k -> *) (a :: k). f a -> Exists f
Exists forall a. Read a => ReadPrec a
R.readPrec 

instance SemigroupForall Proxy where
  appendForall :: forall (a :: k). Proxy a -> Proxy a -> Proxy a
appendForall Proxy a
_ Proxy a
_ = forall {k} (t :: k). Proxy t
Proxy 

instance EqForall ((:~:) a) where
  eqForall :: forall (a :: k). (a :~: a) -> (a :~: a) -> Bool
eqForall a :~: a
Refl a :~: a
Refl = Bool
True

instance EqForall2 (:~:) where
  eqForall2 :: forall (a :: k) (b :: k). (a :~: b) -> (a :~: b) -> Bool
eqForall2 a :~: b
Refl a :~: b
Refl = Bool
True

instance Show a => ShowForall (Const a) where
  showsPrecForall :: forall (a :: k). Int -> Const a a -> ShowS
showsPrecForall Int
p (Const a
a) = Bool -> ShowS -> ShowS
showParen (Int
p forall a. Ord a => a -> a -> Bool
> Int
10)
    forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Const "
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
p a
a

instance Eq a => EqForall (Const a) where
  eqForall :: forall (a :: k). Const a a -> Const a a -> Bool
eqForall (Const a
x) (Const a
y) = a
x forall a. Eq a => a -> a -> Bool
== a
y

instance Ord a => OrdForall (Const a) where
  compareForall :: forall (a :: k). Const a a -> Const a a -> Ordering
compareForall (Const a
x) (Const a
y) = forall a. Ord a => a -> a -> Ordering
compare a
x a
y

instance Hashable a => HashableForall (Const a) where
  hashWithSaltForall :: forall (a :: k). Int -> Const a a -> Int
hashWithSaltForall Int
s (Const a
a) = forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s a
a

instance FromJSON a => FromJSONForeach (Const a) where
  parseJSONForeach :: forall (a :: k). Sing a -> Value -> Parser (Const a a)
parseJSONForeach Sing a
_ = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {k} a (b :: k). a -> Const a b
Const forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. FromJSON a => Value -> Parser a
parseJSON

instance ToJSON a => ToJSONForeach (Const a) where
  toJSONForeach :: forall (a :: k). Sing a -> Const a a -> Value
toJSONForeach Sing a
_ = coerce :: forall a b. Coercible a b => a -> b
coerce (forall a. ToJSON a => a -> Value
toJSON @a)

-- 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 :: ToJSONKeyFunction (Exists f)
toJSONKey = case forall {k} (f :: k -> *).
ToJSONKeyForall f =>
ToJSONKeyFunctionForall f
toJSONKeyForall of
    ToJSONKeyTextForall forall (a :: k). f a -> Key
t forall (a :: k). f a -> Encoding' Key
e -> forall a. (a -> Key) -> (a -> Encoding' Key) -> ToJSONKeyFunction a
ToJSONKeyText (\(Exists f a
a) -> forall (a :: k). f a -> Key
t f a
a) (\(Exists f a
a) -> forall (a :: k). f a -> Encoding' Key
e f a
a)
    ToJSONKeyValueForall forall (a :: k). f a -> Value
v forall (a :: k). f a -> Encoding
e -> forall a. (a -> Value) -> (a -> Encoding) -> ToJSONKeyFunction a
ToJSONKeyValue (\Exists f
x -> case Exists f
x of Exists f a
a -> forall (a :: k). f a -> Value
v f a
a) (\(Exists f a
a) -> forall (a :: k). f a -> Encoding
e f a
a)

instance (FromJSONKeyExists f, FromJSONExists f) => FromJSONKey (Exists f) where
  fromJSONKey :: FromJSONKeyFunction (Exists f)
fromJSONKey = forall {k} (f :: k -> *).
FromJSONKeyExists f =>
FromJSONKeyFunction (Exists f)
fromJSONKeyExists

instance EqForallPoly f => Eq (Exists f) where
  Exists f a
a == :: Exists f -> Exists f -> Bool
== Exists f a
b = forall {k} (a :: k) (b :: k). WitnessedEquality a b -> Bool
weakenEquality (forall {k} (f :: k -> *) (a :: k) (b :: k).
EqForallPoly f =>
f a -> f b -> WitnessedEquality a b
eqForallPoly f a
a f a
b)

instance EqForallPoly2 f => Eq (Exists2 f) where
  Exists2 f a b
a == :: Exists2 f -> Exists2 f -> Bool
== Exists2 f a b
b = forall {k} (a :: k) (b :: k). WitnessedEquality a b -> Bool
weakenEquality (forall k j (f :: k -> j -> *) (a :: k) (b :: j) (c :: k) (d :: j).
EqForallPoly2 f =>
f a b -> f c d -> WitnessedEquality '(a, b) '(c, d)
eqForallPoly2 f a b
a f a b
b)

instance OrdForallPoly f => Ord (Exists f) where
  compare :: Exists f -> Exists f -> Ordering
compare (Exists f a
a) (Exists f a
b) = forall {k} (a :: k) (b :: k). WitnessedOrdering a b -> Ordering
weakenOrdering (forall {k} (f :: k -> *) (a :: k) (b :: k).
OrdForallPoly f =>
f a -> f b -> WitnessedOrdering a b
compareForallPoly f a
a f a
b)

instance (EqForallPoly f, HashableForall f) => Hashable (Exists f) where
  hashWithSalt :: Int -> Exists f -> Int
hashWithSalt Int
s (Exists f a
a) = forall {k} (f :: k -> *) (a :: k).
HashableForall f =>
Int -> f a -> Int
hashWithSaltForall Int
s f a
a

instance ToJSONForall f => ToJSON (Exists f) where
  toJSON :: Exists f -> Value
toJSON (Exists f a
a) = forall {k} (f :: k -> *) (a :: k). ToJSONForall f => f a -> Value
toJSONForall f a
a

instance FromJSONExists f => FromJSON (Exists f) where
  parseJSON :: Value -> Parser (Exists f)
parseJSON Value
v = forall k (f :: k -> *).
FromJSONExists f =>
Value -> Parser (Exists f)
parseJSONExists Value
v

instance ShowForall f => Show (Exists f) where
  showsPrec :: Int -> Exists f -> ShowS
showsPrec Int
p (Exists f a
a) = Bool -> ShowS -> ShowS
showParen 
    (Int
p forall a. Ord a => a -> a -> Bool
>= Int
11) 
    (String -> ShowS
showString String
"Exists " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k).
ShowForall f =>
Int -> f a -> ShowS
showsPrecForall Int
11 f a
a)

instance ShowForall2 f => Show (Exists2 f) where
  showsPrec :: Int -> Exists2 f -> ShowS
showsPrec Int
p (Exists2 f a b
a) = Bool -> ShowS -> ShowS
showParen 
    (Int
p forall a. Ord a => a -> a -> Bool
>= Int
11) 
    (String -> ShowS
showString String
"Exists " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} {k} (f :: k -> k -> *) (a :: k) (b :: k).
ShowForall2 f =>
Int -> f a b -> ShowS
showsPrecForall2 Int
11 f a b
a)

instance ReadExists f => Read (Exists f) where
  readPrec :: ReadPrec (Exists f)
readPrec = forall a. ReadPrec a -> ReadPrec a
R.parens forall a b. (a -> b) -> a -> b
$ forall a. Int -> ReadPrec a -> ReadPrec a
R.prec Int
10 forall a b. (a -> b) -> a -> b
$ do
    R.Ident String
"Exists" <- ReadPrec Lexeme
R.lexP
    forall a. ReadPrec a -> ReadPrec a
R.step forall k (f :: k -> *). ReadExists f => ReadPrec (Exists f)
readPrecExists
    
instance EnumExists f => Enum (Exists f) where
  fromEnum :: Exists f -> Int
fromEnum = forall k (f :: k -> *). EnumExists f => Exists f -> Int
fromEnumExists
  toEnum :: Int -> Exists f
toEnum = forall k (f :: k -> *). EnumExists f => Int -> Exists f
toEnumExists

instance BoundedExists f => Bounded (Exists f) where
  minBound :: Exists f
minBound = forall k (f :: k -> *). BoundedExists f => Exists f
minBoundExists
  maxBound :: Exists f
maxBound = forall k (f :: k -> *). BoundedExists f => Exists f
maxBoundExists

instance BinaryExists f => Binary (Exists f) where
  get :: Get (Exists f)
get = forall k (f :: k -> *). BinaryExists f => Get (Exists f)
getExists
  put :: Exists f -> Put
put = forall k (f :: k -> *). BinaryExists f => Exists f -> Put
putExists

instance BinaryExists2 f => Binary (Exists2 f) where
  get :: Get (Exists2 f)
get = forall k j (f :: k -> j -> *). BinaryExists2 f => Get (Exists2 f)
getExists2
  put :: Exists2 f -> Put
put = forall k j (f :: k -> j -> *). BinaryExists2 f => Exists2 f -> Put
putExists2

instance PathPieceExists f => PP.PathPiece (Exists f) where
  toPathPiece :: Exists f -> Text
toPathPiece = forall k (f :: k -> *). PathPieceExists f => Exists f -> Text
toPathPieceForall
  fromPathPiece :: Text -> Maybe (Exists f)
fromPathPiece = forall k (f :: k -> *).
PathPieceExists f =>
Text -> Maybe (Exists f)
fromPathPieceForall

instance (EqForall f, EqForall g) => EqForall (Product f g) where
  eqForall :: forall (a :: k). Product f g a -> Product f g a -> Bool
eqForall (Pair f a
f1 g a
g1) (Pair f a
f2 g a
g2) = forall {k} (f :: k -> *) (a :: k). EqForall f => f a -> f a -> Bool
eqForall f a
f1 f a
f2 Bool -> Bool -> Bool
&& forall {k} (f :: k -> *) (a :: k). EqForall f => f a -> f a -> Bool
eqForall g a
g1 g a
g2

instance (EqForallPoly f, EqForallPoly g) => EqForallPoly (Product f g) where
  eqForallPoly :: forall (a :: k) (b :: k).
Product f g a -> Product f g b -> WitnessedEquality a b
eqForallPoly (Pair f a
f1 g a
g1) (Pair f b
f2 g b
g2) = case forall {k} (f :: k -> *) (a :: k) (b :: k).
EqForallPoly f =>
f a -> f b -> WitnessedEquality a b
eqForallPoly f a
f1 f b
f2 of
    WitnessedEquality a b
WitnessedEqualityEqual -> forall {k} (f :: k -> *) (a :: k) (b :: k).
EqForallPoly f =>
f a -> f b -> WitnessedEquality a b
eqForallPoly g a
g1 g b
g2
    WitnessedEquality a b
WitnessedEqualityUnequal -> forall {k} (a :: k) (b :: k). WitnessedEquality a b
WitnessedEqualityUnequal

instance (OrdForall f, OrdForall g) => OrdForall (Product f g) where
  compareForall :: forall (a :: k). Product f g a -> Product f g a -> Ordering
compareForall (Pair f a
f1 g a
g1) (Pair f a
f2 g a
g2) = forall a. Monoid a => a -> a -> a
mappend (forall {k} (f :: k -> *) (a :: k).
OrdForall f =>
f a -> f a -> Ordering
compareForall f a
f1 f a
f2) (forall {k} (f :: k -> *) (a :: k).
OrdForall f =>
f a -> f a -> Ordering
compareForall g a
g1 g a
g2)

instance (OrdForallPoly f, OrdForallPoly g) => OrdForallPoly (Product f g) where
  compareForallPoly :: forall (a :: k) (b :: k).
Product f g a -> Product f g b -> WitnessedOrdering a b
compareForallPoly (Pair f a
f1 g a
g1) (Pair f b
f2 g b
g2) = case forall {k} (f :: k -> *) (a :: k) (b :: k).
OrdForallPoly f =>
f a -> f b -> WitnessedOrdering a b
compareForallPoly f a
f1 f b
f2 of
    WitnessedOrdering a b
WitnessedOrderingLT -> forall {k} (a :: k) (b :: k). WitnessedOrdering a b
WitnessedOrderingLT
    WitnessedOrdering a b
WitnessedOrderingGT -> forall {k} (a :: k) (b :: k). WitnessedOrdering a b
WitnessedOrderingGT
    WitnessedOrdering a b
WitnessedOrderingEQ -> forall {k} (f :: k -> *) (a :: k) (b :: k).
OrdForallPoly f =>
f a -> f b -> WitnessedOrdering a b
compareForallPoly g a
g1 g b
g2

instance (ShowForall f, ShowForall g) => ShowForall (Product f g) where
  showsPrecForall :: forall (a :: k). Int -> Product f g a -> ShowS
showsPrecForall Int
p (Pair f a
f g a
g) = Bool -> ShowS -> ShowS
showParen 
    (Int
p forall a. Ord a => a -> a -> Bool
>= Int
11) 
    (String -> ShowS
showString String
"Pair " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k).
ShowForall f =>
Int -> f a -> ShowS
showsPrecForall Int
11 f a
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' ' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k).
ShowForall f =>
Int -> f a -> ShowS
showsPrecForall Int
11 g a
g)

instance (Ord1 f, OrdForeach g) => OrdForeach (Compose f g) where
  compareForeach :: forall (a :: k).
Sing a -> Compose f g a -> Compose f g a -> Ordering
compareForeach Sing a
s (Compose f (g a)
x) (Compose f (g a)
y) = forall (f :: * -> *) a b.
Ord1 f =>
(a -> b -> Ordering) -> f a -> f b -> Ordering
liftCompare (forall {k} (f :: k -> *) (a :: k).
OrdForeach f =>
Sing a -> f a -> f a -> Ordering
compareForeach Sing a
s) f (g a)
x f (g a)
y

instance (Semigroup1 f, SemigroupForall g) => SemigroupForall (Compose f g) where
  appendForall :: forall (a :: k). Compose f g a -> Compose f g a -> Compose f g a
appendForall (Compose f (g a)
x) (Compose f (g a)
y) = forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (forall (f :: * -> *) a.
Semigroup1 f =>
(a -> a -> a) -> f a -> f a -> f a
liftAppend forall {k} (f :: k -> *) (a :: k).
SemigroupForall f =>
f a -> f a -> f a
appendForall f (g a)
x f (g a)
y)

instance (Aeson.ToJSON1 f, ToJSONForall g) => ToJSONForall (Compose f g) where
  toJSONForall :: forall (a :: k). Compose f g a -> Value
toJSONForall (Compose f (g a)
x) = forall (f :: * -> *) a.
ToJSON1 f =>
(a -> Value) -> ([a] -> Value) -> f a -> Value
Aeson.liftToJSON forall {k} (f :: k -> *) (a :: k). ToJSONForall f => f a -> Value
toJSONForall (forall a. ToJSON a => a -> Value
Aeson.toJSON forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall {k} (f :: k -> *) (a :: k). ToJSONForall f => f a -> Value
toJSONForall) f (g a)
x

instance (Aeson.ToJSON1 f, ToJSONForeach g) => ToJSONForeach (Compose f g) where
  toJSONForeach :: forall (a :: k). Sing a -> Compose f g a -> Value
toJSONForeach Sing a
s (Compose f (g a)
x) = forall (f :: * -> *) a.
ToJSON1 f =>
(a -> Value) -> ([a] -> Value) -> f a -> Value
Aeson.liftToJSON (forall {k} (f :: k -> *) (a :: k).
ToJSONForeach f =>
Sing a -> f a -> Value
toJSONForeach Sing a
s) (forall a. ToJSON a => a -> Value
Aeson.toJSON forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall {k} (f :: k -> *) (a :: k).
ToJSONForeach f =>
Sing a -> f a -> Value
toJSONForeach Sing a
s)) f (g a)
x

instance (Aeson.FromJSON1 f, FromJSONForeach g) => FromJSONForeach (Compose f g) where
  parseJSONForeach :: forall (a :: k). Sing a -> Value -> Parser (Compose f g a)
parseJSONForeach Sing a
s = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a.
FromJSON1 f =>
(Value -> Parser a)
-> (Value -> Parser [a]) -> Value -> Parser (f a)
Aeson.liftParseJSON
    (forall {k} (f :: k -> *) (a :: k).
FromJSONForeach f =>
Sing a -> Value -> Parser (f a)
parseJSONForeach Sing a
s)
    (forall a. String -> (Array -> Parser a) -> Value -> Parser a
Aeson.withArray String
"Compose" (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Vector a -> [a]
V.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Vector a -> m (Vector b)
V.mapM (forall {k} (f :: k -> *) (a :: k).
FromJSONForeach f =>
Sing a -> Value -> Parser (f a)
parseJSONForeach Sing a
s)))

instance (Eq1 f, EqForall g) => EqForall (Compose f g) where
  eqForall :: forall (a :: k). Compose f g a -> Compose f g a -> Bool
eqForall (Compose f (g a)
x) (Compose f (g a)
y) = forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq forall {k} (f :: k -> *) (a :: k). EqForall f => f a -> f a -> Bool
eqForall f (g a)
x f (g a)
y

instance (Eq1 f, EqForeach g) => EqForeach (Compose f g) where
  eqForeach :: forall (a :: k). Sing a -> Compose f g a -> Compose f g a -> Bool
eqForeach Sing a
s (Compose f (g a)
x) (Compose f (g a)
y) = forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq (forall {k} (f :: k -> *) (a :: k).
EqForeach f =>
Sing a -> f a -> f a -> Bool
eqForeach Sing a
s) f (g a)
x f (g a)
y

instance (Show1 f, ShowForall g) => ShowForall (Compose f g) where
  showsPrecForall :: forall (a :: k). Int -> Compose f g a -> ShowS
showsPrecForall Int
p (Compose f (g a)
x) = Bool -> ShowS -> ShowS
showParen (Int
p forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Compose " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a.
Show1 f =>
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS
liftShowsPrec forall {k} (f :: k -> *) (a :: k).
ShowForall f =>
Int -> f a -> ShowS
showsPrecForall forall {k} (f :: k -> *) (a :: k). ShowForall f => [f a] -> ShowS
showListForall Int
11 f (g a)
x

instance (Show1 f, ShowForeach g) => ShowForeach (Compose f g) where
  showsPrecForeach :: forall (a :: k). Sing a -> Int -> Compose f g a -> ShowS
showsPrecForeach Sing a
s Int
p (Compose f (g a)
x) = Bool -> ShowS -> ShowS
showParen (Int
p forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Compose " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a.
Show1 f =>
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS
liftShowsPrec (forall {k} (f :: k -> *) (a :: k).
ShowForeach f =>
Sing a -> Int -> f a -> ShowS
showsPrecForeach Sing a
s) (forall {k} (f :: k -> *) (a :: k).
ShowForeach f =>
Sing a -> [f a] -> ShowS
showListForeach Sing a
s) Int
11 f (g a)
x

instance (Semigroup1 f, SemigroupForeach g) => SemigroupForeach (Compose f g) where
  appendForeach :: forall (a :: k).
Sing a -> Compose f g a -> Compose f g a -> Compose f g a
appendForeach Sing a
s (Compose f (g a)
x) (Compose f (g a)
y) = forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (forall (f :: * -> *) a.
Semigroup1 f =>
(a -> a -> a) -> f a -> f a -> f a
liftAppend (forall {k} (f :: k -> *) (a :: k).
SemigroupForeach f =>
Sing a -> f a -> f a -> f a
appendForeach Sing a
s) f (g a)
x f (g a)
y)

instance (Binary1 f, BinaryForeach g) => BinaryForeach (Compose f g) where
  putForeach :: forall (a :: k). Sing a -> Compose f g a -> Put
putForeach Sing a
s (Compose f (g a)
x) = forall (f :: * -> *) a. Binary1 f => (a -> Put) -> f a -> Put
liftPut (forall k (f :: k -> *) (a :: k).
BinaryForeach f =>
Sing a -> f a -> Put
putForeach Sing a
s) f (g a)
x
  getForeach :: forall (a :: k). Sing a -> Get (Compose f g a)
getForeach Sing a
s = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (forall (f :: * -> *) a. Binary1 f => Get a -> Get (f a)
liftGet (forall k (f :: k -> *) (a :: k).
BinaryForeach f =>
Sing a -> Get (f a)
getForeach Sing a
s))

showListForall :: ShowForall f => [f a] -> ShowS
showListForall :: forall {k} (f :: k -> *) (a :: k). ShowForall f => [f a] -> ShowS
showListForall = forall a. (a -> ShowS) -> [a] -> ShowS
showList__ forall {k} (f :: k -> *) (a :: k). ShowForall f => f a -> ShowS
showsForall

showListForeach :: ShowForeach f => Sing a -> [f a] -> ShowS
showListForeach :: forall {k} (f :: k -> *) (a :: k).
ShowForeach f =>
Sing a -> [f a] -> ShowS
showListForeach Sing a
s = forall a. (a -> ShowS) -> [a] -> ShowS
showList__ (forall {k} (f :: k -> *) (a :: k).
ShowForeach f =>
Sing a -> f a -> ShowS
showsForeach Sing a
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
showList__ :: forall a. (a -> ShowS) -> [a] -> ShowS
showList__ a -> ShowS
_     []     String
s = String
"[]" forall a. [a] -> [a] -> [a]
++ String
s
showList__ a -> ShowS
showx (a
x:[a]
xs) String
s = Char
'[' forall a. a -> [a] -> [a]
: a -> ShowS
showx a
x ([a] -> String
showl [a]
xs)
  where
    showl :: [a] -> String
showl []     = Char
']' forall a. a -> [a] -> [a]
: String
s
    showl (a
y:[a]
ys) = Char
',' forall a. a -> [a] -> [a]
: a -> ShowS
showx a
y ([a] -> String
showl [a]
ys)

instance (EqForall f, EqForall g) => EqForall (Sum f g) where
  eqForall :: forall (a :: k). Sum f g a -> Sum f g a -> Bool
eqForall (InL f a
f1) (InL f a
f2) = forall {k} (f :: k -> *) (a :: k). EqForall f => f a -> f a -> Bool
eqForall f a
f1 f a
f2
  eqForall (InR g a
f1) (InR g a
f2) = forall {k} (f :: k -> *) (a :: k). EqForall f => f a -> f a -> Bool
eqForall g a
f1 g a
f2
  eqForall (InR g a
_) (InL f a
_) = Bool
False
  eqForall (InL f a
_) (InR g a
_) = Bool
False

instance (OrdForall f, OrdForall g) => OrdForall (Sum f g) where
  compareForall :: forall (a :: k). Sum f g a -> Sum f g a -> Ordering
compareForall (InL f a
f1) (InL f a
f2) = forall {k} (f :: k -> *) (a :: k).
OrdForall f =>
f a -> f a -> Ordering
compareForall f a
f1 f a
f2
  compareForall (InR g a
f1) (InR g a
f2) = forall {k} (f :: k -> *) (a :: k).
OrdForall f =>
f a -> f a -> Ordering
compareForall g a
f1 g a
f2
  compareForall (InR g a
_) (InL f a
_) = Ordering
GT
  compareForall (InL f a
_) (InR g a
_) = Ordering
LT

defaultCompareForallPoly :: (TestEquality f, OrdForall f) => f a -> f b -> Ordering
defaultCompareForallPoly :: forall {k} (f :: k -> *) (a :: k) (b :: k).
(TestEquality f, OrdForall f) =>
f a -> f b -> Ordering
defaultCompareForallPoly f a
a f b
b = case forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality f a
a f b
b of
  Maybe (a :~: b)
Nothing -> forall a. Ord a => a -> a -> Ordering
compare (forall a. a -> Int
getTagBox f a
a) (forall a. a -> Int
getTagBox f b
b)
  Just a :~: b
Refl -> forall {k} (f :: k -> *) (a :: k).
OrdForall f =>
f a -> f a -> Ordering
compareForall f a
a f b
b

defaultEqForallPoly :: (TestEquality f, EqForall f) => f a -> f b -> WitnessedEquality a b
defaultEqForallPoly :: forall {k} (f :: k -> *) (a :: k) (b :: k).
(TestEquality f, EqForall f) =>
f a -> f b -> WitnessedEquality a b
defaultEqForallPoly f a
x f b
y = case forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality f a
x f b
y of
  Maybe (a :~: b)
Nothing -> forall {k} (a :: k) (b :: k). WitnessedEquality a b
WitnessedEqualityUnequal
  Just a :~: b
Refl -> if forall {k} (f :: k -> *) (a :: k). EqForall f => f a -> f a -> Bool
eqForall f a
x f b
y then forall {k} (a :: k). WitnessedEquality a a
WitnessedEqualityEqual else forall {k} (a :: k) (b :: k). WitnessedEquality a b
WitnessedEqualityUnequal

getTagBox :: a -> Int
getTagBox :: forall a. a -> Int
getTagBox !a
x = Int# -> Int
I# (forall a. a -> Int#
dataToTag# a
x)
{-# INLINE getTagBox #-}

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 :: forall (a :: [k]). Sing a -> [k]
demoteSing SingList a
Sing a
SingListNil = []
  demoteSing (SingListCons Sing r
s SingList rs
ss) = forall k (a :: k). SingKind k => Sing a -> k
demoteSing Sing r
s forall a. a -> [a] -> [a]
: forall k (a :: k). SingKind k => Sing a -> k
demoteSing SingList rs
ss
  promoteSing :: [k] -> Exists Sing
promoteSing [] = forall k (f :: k -> *) (a :: k). f a -> Exists f
Exists forall {k}. SingList '[]
SingListNil
  promoteSing (k
x : [k]
xs) = case forall k. SingKind k => k -> Exists Sing
promoteSing k
x of
    Exists Sing a
s -> case forall k. SingKind k => k -> Exists Sing
promoteSing [k]
xs of
      Exists Sing a
ss -> forall k (f :: k -> *) (a :: k). f a -> Exists f
Exists (forall {k} (a :: k) (rs :: [k]).
Sing a -> SingList rs -> SingList (a : rs)
SingListCons Sing a
s Sing a
ss)

type instance Sing = SingList
type instance Sing = SingMaybe

class Unreify k where
  unreify :: forall (a :: k) b. Sing a -> (Reify a => b) -> b

instance Unreify k => Unreify [k] where
  unreify :: forall (a :: [k]) b. Sing a -> (Reify a => b) -> b
unreify = forall k (as :: [k]) b.
Unreify k =>
SingList as -> (Reify as => b) -> b
unreifyList

class Reify a where
  reify :: Sing a

instance Reify '[] where
  reify :: Sing '[]
reify = forall {k}. SingList '[]
SingListNil

instance (Reify a, Reify as) => Reify (a ': as) where
  reify :: Sing (a : as)
reify = forall {k} (a :: k) (rs :: [k]).
Sing a -> SingList rs -> SingList (a : rs)
SingListCons forall {k} (a :: k). Reify a => Sing a
reify forall {k} (a :: k). Reify a => Sing a
reify

instance Reify 'Nothing where
  reify :: Sing 'Nothing
reify = forall {k}. SingMaybe 'Nothing
SingMaybeNothing

instance Reify a => Reify ('Just a) where
  reify :: Sing ('Just a)
reify = forall {k} (a :: k). Sing a -> SingMaybe ('Just a)
SingMaybeJust forall {k} (a :: k). Reify a => Sing a
reify

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 :: forall (a :: [a]) (b :: [a]). Sing a -> Sing b -> Maybe (a :~: b)
eqSing = forall k (a :: [k]) (b :: [k]).
EqSing k =>
SingList a -> SingList b -> Maybe (a :~: b)
eqSingList

eqSingList :: forall (k :: Type) (a :: [k]) (b :: [k]). EqSing k => SingList a -> SingList b -> Maybe (a :~: b)
eqSingList :: forall k (a :: [k]) (b :: [k]).
EqSing k =>
SingList a -> SingList b -> Maybe (a :~: b)
eqSingList SingList a
SingListNil SingList b
SingListNil = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
eqSingList SingList a
SingListNil (SingListCons Sing r
_ SingList rs
_) = forall a. Maybe a
Nothing
eqSingList (SingListCons Sing r
_ SingList rs
_) SingList b
SingListNil = forall a. Maybe a
Nothing
eqSingList (SingListCons Sing r
a SingList rs
as) (SingListCons Sing r
b SingList rs
bs) = case forall k (a :: k) (b :: k).
EqSing k =>
Sing a -> Sing b -> Maybe (a :~: b)
eqSing Sing r
a Sing r
b of
  Just r :~: r
Refl -> case forall k (a :: [k]) (b :: [k]).
EqSing k =>
SingList a -> SingList b -> Maybe (a :~: b)
eqSingList SingList rs
as SingList rs
bs of
    Just rs :~: rs
Refl -> forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    Maybe (rs :~: rs)
Nothing -> forall a. Maybe a
Nothing
  Maybe (r :~: r)
Nothing -> forall a. Maybe a
Nothing

class SemigroupForeach f => MonoidForeach f where
  emptyForeach :: Sing a -> f a

class SemigroupForall f => MonoidForall f where
  emptyForall :: f a

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 :: forall (a :: [k]). SingList a -> SingList a -> Bool
eqForall SingList a
_ SingList a
_ = Bool
True

instance EqSing k => EqForallPoly (SingList :: [k] -> Type) where
  eqForallPoly :: forall (a :: [k]) (b :: [k]).
SingList a -> SingList b -> WitnessedEquality a b
eqForallPoly SingList a
SingListNil SingList b
SingListNil = forall {k} (a :: k). WitnessedEquality a a
WitnessedEqualityEqual
  eqForallPoly SingList a
SingListNil (SingListCons Sing r
_ SingList rs
_) = forall {k} (a :: k) (b :: k). WitnessedEquality a b
WitnessedEqualityUnequal
  eqForallPoly (SingListCons Sing r
_ SingList rs
_) SingList b
SingListNil = forall {k} (a :: k) (b :: k). WitnessedEquality a b
WitnessedEqualityUnequal
  eqForallPoly (SingListCons Sing r
r SingList rs
rs) (SingListCons Sing r
s SingList rs
ss) = case forall k (a :: k) (b :: k).
EqSing k =>
Sing a -> Sing b -> Maybe (a :~: b)
eqSing Sing r
r Sing r
s of
    Maybe (r :~: r)
Nothing -> forall {k} (a :: k) (b :: k). WitnessedEquality a b
WitnessedEqualityUnequal
    Just r :~: r
Refl -> case forall {k} (f :: k -> *) (a :: k) (b :: k).
EqForallPoly f =>
f a -> f b -> WitnessedEquality a b
eqForallPoly SingList rs
rs SingList rs
ss of
      WitnessedEquality rs rs
WitnessedEqualityUnequal -> forall {k} (a :: k) (b :: k). WitnessedEquality a b
WitnessedEqualityUnequal
      WitnessedEquality rs rs
WitnessedEqualityEqual -> forall {k} (a :: k). WitnessedEquality a a
WitnessedEqualityEqual

instance (SingKind k, Binary k) => BinaryExists (SingList :: [k] -> Type) where
  putExists :: Exists SingList -> Put
putExists (Exists SingList a
xs) = forall t. Binary t => t -> Put
BN.put (forall k (a :: k). SingKind k => Sing a -> k
demoteSing SingList a
xs)
  getExists :: Get (Exists SingList)
getExists = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k. SingKind k => k -> Exists Sing
promoteSing forall t. Binary t => Get t
BN.get

instance (ShowSing k) => Show (SingList (xs :: [k])) where
  showsPrec :: Int -> SingList xs -> ShowS
showsPrec Int
_ SingList xs
SingListNil = String -> ShowS
showString String
"SingListNil"
  showsPrec Int
p (SingListCons Sing r
s SingList rs
ss) = Bool -> ShowS -> ShowS
showParen (Int
p forall a. Ord a => a -> a -> Bool
> Int
10)
    forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"SingListCons "
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (a :: k). ShowSing k => Int -> Sing a -> ShowS
showsPrecSing Int
11 Sing r
s
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' '
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 SingList rs
ss

instance ShowSing k => ShowSing [k] where
  showsPrecSing :: forall (a :: [k]). Int -> Sing a -> ShowS
showsPrecSing = forall a. Show a => Int -> a -> ShowS
showsPrec

data SingMaybe :: Maybe k -> Type where
  SingMaybeJust :: Sing a -> SingMaybe ('Just a)
  SingMaybeNothing :: SingMaybe 'Nothing

unreifyList :: forall (k :: Type) (as :: [k]) (b :: Type) . Unreify k
  => SingList as
  -> (Reify as => b)
  -> b
unreifyList :: forall k (as :: [k]) b.
Unreify k =>
SingList as -> (Reify as => b) -> b
unreifyList SingList as
SingListNil Reify as => b
b = Reify as => b
b
unreifyList (SingListCons Sing r
s SingList rs
ss) Reify as => b
b = forall k (a :: k) b. Unreify k => Sing a -> (Reify a => b) -> b
unreify Sing r
s (forall k (as :: [k]) b.
Unreify k =>
SingList as -> (Reify as => b) -> b
unreifyList SingList rs
ss Reify as => b
b)

instance (EqForeach f, EqSing k) => Eq (Some (f :: k -> Type)) where 
  Some Sing a
s1 f a
v1 == :: Some f -> Some f -> Bool
== Some Sing a
s2 f a
v2 = case forall k (a :: k) (b :: k).
EqSing k =>
Sing a -> Sing b -> Maybe (a :~: b)
eqSing Sing a
s1 Sing a
s2 of
    Just a :~: a
Refl -> forall {k} (f :: k -> *) (a :: k).
EqForeach f =>
Sing a -> f a -> f a -> Bool
eqForeach Sing a
s1 f a
v1 f a
v2
    Maybe (a :~: a)
Nothing -> Bool
False

instance (OrdForeach f, OrdSing k) => Ord (Some (f :: k -> Type)) where 
  compare :: Some f -> Some f -> Ordering
compare (Some Sing a
s1 f a
v1) (Some Sing a
s2 f a
v2) = case forall k (a :: k) (b :: k).
OrdSing k =>
Sing a -> Sing b -> WitnessedOrdering a b
compareSing Sing a
s1 Sing a
s2 of
    WitnessedOrdering a a
WitnessedOrderingEQ -> forall {k} (f :: k -> *) (a :: k).
OrdForeach f =>
Sing a -> f a -> f a -> Ordering
compareForeach Sing a
s1 f a
v1 f a
v2
    WitnessedOrdering a a
WitnessedOrderingLT -> Ordering
LT
    WitnessedOrdering a a
WitnessedOrderingGT -> Ordering
GT

instance (ShowForeach f, ShowSing k) => Show (Some (f :: k -> Type)) where
  showsPrec :: Int -> Some f -> ShowS
showsPrec Int
p (Some Sing a
s f a
a) = Bool -> ShowS -> ShowS
showParen (Int
p forall a. Ord a => a -> a -> Bool
>= Int
11)
    forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Sing "
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (a :: k). ShowSing k => Int -> Sing a -> ShowS
showsPrecSing Int
11 Sing a
s
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' '
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k).
ShowForeach f =>
Sing a -> Int -> f a -> ShowS
showsPrecForeach Sing a
s Int
11 f a
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 (ToJSONForeach f, ToJSONSing k) => ToJSON (Some (f :: k -> Type)) where
  toJSON :: Some f -> Value
toJSON (Some Sing a
s f a
v) = forall a. ToJSON a => a -> Value
toJSON [forall k (a :: k). ToJSONSing k => Sing a -> Value
toJSONSing Sing a
s, forall {k} (f :: k -> *) (a :: k).
ToJSONForeach f =>
Sing a -> f a -> Value
toJSONForeach Sing a
s f a
v]

class FromJSONSing k where
  parseJSONSing :: Aeson.Value -> Aeson.Parser (Exists (Sing :: k -> Type))

instance (Aeson.FromJSON1 f, FromJSONForall g) => FromJSONForall (Compose f g) where
  parseJSONForall :: forall (a :: k). Sing a -> Value -> Parser (Compose f g a)
parseJSONForall Sing a
s = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a.
FromJSON1 f =>
(Value -> Parser a)
-> (Value -> Parser [a]) -> Value -> Parser (f a)
Aeson.liftParseJSON
      (forall {k} (f :: k -> *) (a :: k).
FromJSONForall f =>
Sing a -> Value -> Parser (f a)
parseJSONForall Sing a
s)
          (forall a. String -> (Array -> Parser a) -> Value -> Parser a
Aeson.withArray String
"Compose" (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Vector a -> [a]
V.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Vector a -> m (Vector b)
V.mapM (forall {k} (f :: k -> *) (a :: k).
FromJSONForall f =>
Sing a -> Value -> Parser (f a)
parseJSONForall Sing a
s)))

instance (FromJSONForeach f, FromJSONSing k) => FromJSON (Some (f :: k -> Type)) where
  parseJSON :: Value -> Parser (Some f)
parseJSON = forall a. String -> (Array -> Parser a) -> Value -> Parser a
Aeson.withArray String
"Some" forall a b. (a -> b) -> a -> b
$ \Array
v -> if forall a. Vector a -> Int
V.length Array
v forall a. Eq a => a -> a -> Bool
== Int
2
    then do
      let x :: Value
x = forall a. Vector a -> Int -> a
V.unsafeIndex Array
v Int
0
          y :: Value
y = forall a. Vector a -> Int -> a
V.unsafeIndex Array
v Int
1
      Exists Sing a
s <- forall k. FromJSONSing k => Value -> Parser (Exists Sing)
parseJSONSing Value
x :: Aeson.Parser (Exists (Sing :: k -> Type))
      f a
val <- forall {k} (f :: k -> *) (a :: k).
FromJSONForeach f =>
Sing a -> Value -> Parser (f a)
parseJSONForeach Sing a
s Value
y
      forall (m :: * -> *) a. Monad m => a -> m a
return (forall k (f :: k -> *) (a :: k). Sing a -> f a -> Some f
Some Sing a
s f a
val)
    else forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"array of length 2 expected"

-- 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 :: forall {k} (f :: k -> *) (v :: k -> *) (a :: k).
(ToJSONKeyForeach f, ToJSONForeach v) =>
Sing a -> Map (f a) (v a) -> Value
toJSONMapForeachKey Sing a
s Map (f a) (v a)
m = case forall {k} (f :: k -> *).
ToJSONKeyForeach f =>
ToJSONKeyFunctionForall (Product Sing f)
toJSONKeyForeach of
  ToJSONKeyTextForall forall (a :: k). Product Sing f a -> Key
keyToText forall (a :: k). Product Sing f a -> Encoding' Key
_ -> forall a. ToJSON a => a -> Value
toJSON forall a b. (a -> b) -> a -> b
$ forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
M.foldlWithKey'
    ( \HashMap Key Value
hm f a
key v a
val -> forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HM.insert (forall (a :: k). Product Sing f a -> Key
keyToText (forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair Sing a
s f a
key)) (forall {k} (f :: k -> *) (a :: k).
ToJSONForeach f =>
Sing a -> f a -> Value
toJSONForeach Sing a
s v a
val) HashMap Key Value
hm
    ) forall k v. HashMap k v
HM.empty Map (f a) (v a)
m
  ToJSONKeyValueForall forall (a :: k). Product Sing f a -> Value
keyToValue forall (a :: k). Product Sing f a -> Encoding
_ -> forall a. ToJSON a => a -> Value
toJSON forall a b. (a -> b) -> a -> b
$ forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
M.foldrWithKey' 
    ( \f a
key v a
val [(Value, Value)]
xs -> (forall (a :: k). Product Sing f a -> Value
keyToValue (forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair Sing a
s f a
key), forall {k} (f :: k -> *) (a :: k).
ToJSONForeach f =>
Sing a -> f a -> Value
toJSONForeach Sing a
s v a
val) forall a. a -> [a] -> [a]
: [(Value, Value)]
xs
    ) [] Map (f a) (v a)
m

-- | Parse a 'Map' whose key type is higher-kinded. This only creates a valid 'Map'
--   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)
parseJSONMapForeachKey :: forall k (f :: k -> *) (a :: k) v.
(FromJSONKeyForeach f, OrdForeach f, Unreify k) =>
(Value -> Parser v) -> Sing a -> Value -> Parser (Map (f a) v)
parseJSONMapForeachKey Value -> Parser v
valueParser Sing a
s Value
obj = forall k (a :: k) b. Unreify k => Sing a -> (Reify a => b) -> b
unreify Sing a
s forall a b. (a -> b) -> a -> b
$ case forall {k} (f :: k -> *).
FromJSONKeyForeach f =>
FromJSONKeyFunctionForeach f
fromJSONKeyForeach of
  FromJSONKeyTextParserForeach forall (a :: k). Sing a -> Key -> Parser (f a)
f -> forall a. String -> (Object -> Parser a) -> Value -> Parser a
Aeson.withObject String
"Map k v"
    ( forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall k1 k2 a. (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeysMonotonic forall {k} (f :: k -> *) (a :: k). ApplyForeach f a -> f a
getApplyForeach) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall v a. (Key -> v -> a -> a) -> a -> KeyMap v -> a
KM.foldrWithKey
      (\Key
k Value
v Parser (Map (ApplyForeach f a) v)
m -> forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (coerce :: forall a b. Coercible a b => a -> b
coerce (forall (a :: k). Sing a -> Key -> Parser (f a)
f Sing a
s Key
k :: Aeson.Parser (f a)) :: Aeson.Parser (ApplyForeach f a)) forall a. Parser a -> JSONPathElement -> Parser a
<?> Key -> JSONPathElement
Key Key
k
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Value -> Parser v
valueParser Value
v forall a. Parser a -> JSONPathElement -> Parser a
<?> Key -> JSONPathElement
Key Key
k
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (Map (ApplyForeach f a) v)
m
      ) (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall k a. Map k a
M.empty)
    ) Value
obj
  FromJSONKeyValueForeach forall (a :: k). Sing a -> Value -> Parser (f a)
f -> forall a. String -> (Array -> Parser a) -> Value -> Parser a
Aeson.withArray String
"Map k v"
    ( forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall k1 k2 a. (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeysMonotonic forall {k} (f :: k -> *) (a :: k). ApplyForeach f a -> f a
getApplyForeach forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => [(k, a)] -> Map k a
M.fromList)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. (coerce :: forall a b. Coercible a b => a -> b
coerce :: Aeson.Parser [(f a, v)] -> Aeson.Parser [(ApplyForeach f a, v)])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
TRV.sequence
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (forall a b.
(Value -> Parser a)
-> (Value -> Parser b) -> Int -> Value -> Parser (a, b)
parseIndexedJSONPair (forall (a :: k). Sing a -> Value -> Parser (f a)
f Sing a
s) Value -> Parser v
valueParser) [Int
0..]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Vector a -> [a]
V.toList
    ) Value
obj

-- copied from aeson
parseIndexedJSONPair :: (Aeson.Value -> Aeson.Parser a) -> (Aeson.Value -> Aeson.Parser b) -> Int -> Aeson.Value -> Aeson.Parser (a, b)
parseIndexedJSONPair :: forall a b.
(Value -> Parser a)
-> (Value -> Parser b) -> Int -> Value -> Parser (a, b)
parseIndexedJSONPair Value -> Parser a
keyParser Value -> Parser b
valParser Int
idx Value
value = Value -> Parser (a, b)
p Value
value forall a. Parser a -> JSONPathElement -> Parser a
<?> Int -> JSONPathElement
Index Int
idx
  where
    p :: Value -> Parser (a, b)
p = forall a. String -> (Array -> Parser a) -> Value -> Parser a
Aeson.withArray String
"(k,v)" forall a b. (a -> b) -> a -> b
$ \Array
ab ->
        let n :: Int
n = forall a. Vector a -> Int
V.length Array
ab
        in if Int
n forall a. Eq a => a -> a -> Bool
== Int
2
             then (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (Value -> Parser a) -> Int -> Array -> Parser a
parseJSONElemAtIndex Value -> Parser a
keyParser Int
0 Array
ab
                      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. (Value -> Parser a) -> Int -> Array -> Parser a
parseJSONElemAtIndex Value -> Parser b
valParser Int
1 Array
ab
             else forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"cannot unpack array of length " forall a. [a] -> [a] -> [a]
++
                         forall a. Show a => a -> String
show Int
n forall a. [a] -> [a] -> [a]
++ String
" into a pair"
{-# INLINE parseIndexedJSONPair #-}

-- copied from aeson
parseJSONElemAtIndex :: (Aeson.Value -> Aeson.Parser a) -> Int -> V.Vector Aeson.Value -> Aeson.Parser a
parseJSONElemAtIndex :: forall a. (Value -> Parser a) -> Int -> Array -> Parser a
parseJSONElemAtIndex Value -> Parser a
p Int
idx Array
ary = Value -> Parser a
p (forall a. Vector a -> Int -> a
V.unsafeIndex Array
ary Int
idx) forall a. Parser a -> JSONPathElement -> Parser a
<?> Int -> JSONPathElement
Index Int
idx

weakenEquality :: WitnessedEquality a b -> Bool
weakenEquality :: forall {k} (a :: k) (b :: k). WitnessedEquality a b -> Bool
weakenEquality = \case
  WitnessedEquality a b
WitnessedEqualityEqual -> Bool
True
  WitnessedEquality a b
WitnessedEqualityUnequal -> Bool
False

weakenOrdering :: WitnessedOrdering a b -> Ordering
weakenOrdering :: forall {k} (a :: k) (b :: k). WitnessedOrdering a b -> Ordering
weakenOrdering = \case
  WitnessedOrdering a b
WitnessedOrderingGT -> Ordering
GT
  WitnessedOrdering a b
WitnessedOrderingEQ -> Ordering
EQ
  WitnessedOrdering a b
WitnessedOrderingLT -> Ordering
LT

strengthenEquality :: Bool -> WitnessedEquality a a
strengthenEquality :: forall {k} (a :: k). Bool -> WitnessedEquality a a
strengthenEquality = \case
  Bool
True -> forall {k} (a :: k). WitnessedEquality a a
WitnessedEqualityEqual
  Bool
False -> forall {k} (a :: k) (b :: k). WitnessedEquality a b
WitnessedEqualityUnequal

-- | Given that we already know two types are equal, promote an 'Ordering'.
strengthenOrdering :: Ordering -> WitnessedOrdering a a                                
strengthenOrdering :: forall {k} (a :: k). Ordering -> WitnessedOrdering a a
strengthenOrdering = \case
  Ordering
LT -> forall {k} (a :: k) (b :: k). WitnessedOrdering a b
WitnessedOrderingLT                                                    
  Ordering
EQ -> forall {k} (a :: k). WitnessedOrdering a a
WitnessedOrderingEQ                                                              
  Ordering
GT -> forall {k} (a :: k) (b :: k). WitnessedOrdering a b
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 :: forall {k} (a :: k) (b :: k). Ordering -> WitnessedOrdering a b
strengthenUnequalOrdering = \case                                                  
  Ordering
LT -> forall {k} (a :: k) (b :: k). WitnessedOrdering a b
WitnessedOrderingLT 
  Ordering
EQ -> forall {k} (a :: k) (b :: k). WitnessedOrdering a b
WitnessedOrderingLT -- this case should not happen                                          
  Ordering
GT -> forall {k} (a :: k) (b :: k). WitnessedOrdering a b
WitnessedOrderingGT               

instance (EqForallPoly f, ToSing f, EqForeach g) => Eq (DependentPair f g) where
  DependentPair f a
a1 g a
b1 == :: DependentPair f g -> DependentPair f g -> Bool
== DependentPair f a
a2 g a
b2 = case forall {k} (f :: k -> *) (a :: k) (b :: k).
EqForallPoly f =>
f a -> f b -> WitnessedEquality a b
eqForallPoly f a
a1 f a
a2 of
    WitnessedEquality a a
WitnessedEqualityUnequal -> Bool
False
    WitnessedEquality a a
WitnessedEqualityEqual -> forall {k} (f :: k -> *) (a :: k).
EqForeach f =>
Sing a -> f a -> f a -> Bool
eqForeach (forall k (f :: k -> *) (a :: k). ToSing f => f a -> Sing a
toSing f a
a1) g a
b1 g a
b2

instance (OrdForallPoly f, ToSing f, OrdForeach g) => Ord (DependentPair f g) where
  compare :: DependentPair f g -> DependentPair f g -> Ordering
compare (DependentPair f a
a1 g a
b1) (DependentPair f a
a2 g a
b2) = case forall {k} (f :: k -> *) (a :: k) (b :: k).
OrdForallPoly f =>
f a -> f b -> WitnessedOrdering a b
compareForallPoly f a
a1 f a
a2 of
    WitnessedOrdering a a
WitnessedOrderingLT -> Ordering
LT
    WitnessedOrdering a a
WitnessedOrderingGT -> Ordering
GT
    WitnessedOrdering a a
WitnessedOrderingEQ -> forall {k} (f :: k -> *) (a :: k).
OrdForeach f =>
Sing a -> f a -> f a -> Ordering
compareForeach (forall k (f :: k -> *) (a :: k). ToSing f => f a -> Sing a
toSing f a
a1) g a
b1 g a
b2

instance (ShowForall f, ToSing f, ShowForeach g) => Show (DependentPair f g) where
  showsPrec :: Int -> DependentPair f g -> ShowS
showsPrec Int
p (DependentPair f a
a g a
b) String
s = Bool -> ShowS -> ShowS
showParen 
    (Int
p forall a. Ord a => a -> a -> Bool
>= Int
11) 
    (String -> ShowS
showString String
"DependentPair " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k).
ShowForall f =>
Int -> f a -> ShowS
showsPrecForall Int
11 f a
a forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' ' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k).
ShowForeach f =>
Sing a -> Int -> f a -> ShowS
showsPrecForeach (forall k (f :: k -> *) (a :: k). ToSing f => f a -> Sing a
toSing f a
a) Int
11 g a
b)
    String
s

instance Semigroup a => SemigroupForall (Const a) where
  appendForall :: forall (a :: k). Const a a -> Const a a -> Const a a
appendForall (Const a
x) (Const a
y) = forall {k} a (b :: k). a -> Const a b
Const (a
x forall a. Semigroup a => a -> a -> a
SG.<> a
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 :: forall (a :: k). Const a a
emptyForall = forall {k} a (b :: k). a -> Const a b
Const forall a. Monoid a => a
mempty