{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UnboxedTuples #-}
{-# OPTIONS_GHC -Wall #-}
module Data.Exists
(
Exists(..)
, Exists2(..)
, Exists3(..)
, Some(..)
, DependentPair(..)
, WitnessedEquality(..)
, WitnessedOrdering(..)
, ApplyForall(..)
, ApplyForeach(..)
, ApplyLifted(..)
, EqForall(..)
, EqForallPoly(..)
, EqForeach(..)
, OrdForall(..)
, OrdForallPoly(..)
, OrdForeach(..)
, ShowForall(..)
, ShowForeach(..)
, ReadExists(..)
, EnumForall(..)
, EnumExists(..)
, BoundedExists(..)
, SemigroupForall(..)
, SemigroupForeach(..)
, MonoidForall(..)
, MonoidForeach(..)
, HashableForall(..)
, HashableForeach(..)
, PathPieceExists(..)
, StorableForeach(..)
, StorableForall(..)
, PrimForall(..)
, BinaryExists(..)
, BinaryForeach(..)
, EqForall2(..)
, EqForallPoly2(..)
, ShowForall2(..)
, ShowForeach2(..)
, BinaryExists2(..)
, Sing
, SingList(..)
, SingMaybe(..)
, Reify(..)
, Unreify(..)
, EqSing(..)
, OrdSing(..)
, ShowSing(..)
, ToSing(..)
, SingKind(..)
, showsForall
, showsForeach
, showForall
, showListForall
, showListForeach
, showsForall2
, showForall2
, defaultEqForallPoly
, defaultCompareForallPoly
, weakenEquality
, weakenOrdering
, strengthenEquality
, strengthenOrdering
, strengthenUnequalOrdering
, unreifyList
) where
import Control.Applicative (Const(..))
import Data.Binary (Get,Put,Binary)
import Data.Binary.Lifted (Binary1(..))
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.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.Binary as BN
import qualified Data.Semigroup as SG
import qualified Text.Read as R
import qualified Web.PathPieces as PP
data Exists (f :: k -> Type) = forall a. Exists !(f a)
data Exists2 (f :: k -> j -> Type) = forall a b. Exists2 !(f a b)
data Exists3 (f :: k -> j -> l -> Type) = forall a b c. Exists3 !(f a b c)
data DependentPair (f :: k -> Type) (g :: k -> Type) =
forall a. DependentPair (f a) (g a)
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
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10)
(ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"ApplyForall "
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> f a -> ShowS
forall (a :: k). Int -> f a -> ShowS
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
(<>) = ApplyForall f a -> ApplyForall f a -> ApplyForall f a
forall (a :: k).
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 = ApplyForall f a
forall (a :: k). ApplyForall f a
forall {k} (f :: k -> *) (a :: k). MonoidForall f => f a
emptyForall
mappend :: ApplyForall f a -> ApplyForall f a -> ApplyForall f a
mappend = ApplyForall f a -> ApplyForall f a -> ApplyForall f a
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) = f a -> ApplyForall f a
forall {k} (f :: k -> *) (a :: k). f a -> ApplyForall f a
ApplyForall (f a -> f a -> f a
forall (a :: k). f a -> f a -> f a
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 = f a -> ApplyForall f a
forall {k} (f :: k -> *) (a :: k). f a -> ApplyForall f a
ApplyForall f a
forall (a :: k). f a
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
(<>) = 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 = ApplyLifted f a
forall (f :: * -> *) a. (Monoid1 f, Monoid a) => f a
empty1
mappend :: ApplyLifted f a -> ApplyLifted f a -> ApplyLifted f a
mappend = ApplyLifted f a -> ApplyLifted f a -> ApplyLifted f a
forall a. Semigroup a => a -> a -> a
(<>)
instance (Eq1 f, Eq a) => Eq (ApplyLifted f a) where
== :: ApplyLifted f a -> ApplyLifted f a -> Bool
(==) = 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 = ApplyLifted f a -> ApplyLifted f a -> Ordering
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) = f a -> ApplyLifted f a
forall {k} (f :: k -> *) (a :: k). f a -> ApplyLifted f a
ApplyLifted ((a -> a -> a) -> f a -> f a -> f a
forall a. (a -> a -> a) -> f a -> f a -> f a
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 = f a -> ApplyLifted f a
forall {k} (f :: k -> *) (a :: k). f a -> ApplyLifted f a
ApplyLifted (a -> f a
forall a. a -> f a
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) = (a -> b -> Bool) -> f a -> f b -> Bool
forall a b. (a -> b -> Bool) -> f a -> f b -> Bool
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) = (a -> b -> Ordering) -> f a -> f b -> Ordering
forall a b. (a -> b -> Ordering) -> f a -> f b -> Ordering
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
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 = Sing a -> f a -> f a -> Bool
forall (a :: k). Sing a -> f a -> f a -> Bool
forall {k} (f :: k -> *) (a :: k).
EqForeach f =>
Sing a -> f a -> f a -> Bool
eqForeach Sing a
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) = Sing a -> f a -> f a -> Ordering
forall (a :: k). Sing a -> f a -> f a -> Ordering
forall {k} (f :: k -> *) (a :: k).
OrdForeach f =>
Sing a -> f a -> f a -> Ordering
compareForeach Sing a
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10)
(ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"ApplyForeach "
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing a -> Int -> f a -> ShowS
forall (a :: k). Sing a -> Int -> f a -> ShowS
forall {k} (f :: k -> *) (a :: k).
ShowForeach f =>
Sing a -> Int -> f a -> ShowS
showsPrecForeach Sing a
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
(<>) = Sing a -> ApplyForeach f a -> ApplyForeach f a -> ApplyForeach f a
forall (a :: k).
Sing a -> 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 Sing a
forall {k} (a :: k). Reify a => Sing a
reify
instance (MonoidForeach f, Reify a) => Monoid (ApplyForeach f a) where
mempty :: ApplyForeach f a
mempty = Sing a -> ApplyForeach f a
forall (a :: k). Sing a -> ApplyForeach f a
forall {k} (f :: k -> *) (a :: k). MonoidForeach f => Sing a -> f a
emptyForeach Sing a
forall {k} (a :: k). Reify a => Sing a
reify
mappend :: ApplyForeach f a -> ApplyForeach f a -> ApplyForeach f a
mappend = ApplyForeach f a -> ApplyForeach f a -> ApplyForeach f a
forall a. Semigroup a => a -> a -> a
(SG.<>)
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) = Sing a -> f a -> f a -> Bool
forall (a :: k). Sing a -> f a -> f a -> Bool
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) = Sing a -> f a -> f a -> Ordering
forall (a :: k). Sing a -> f a -> f a -> Ordering
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) = f a -> ApplyForeach f a
forall {k} (f :: k -> *) (a :: k). f a -> ApplyForeach f a
ApplyForeach (Sing a -> f a -> f a -> f a
forall (a :: k). Sing a -> f a -> f a -> f a
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 = f a -> ApplyForeach f a
forall {k} (f :: k -> *) (a :: k). f a -> ApplyForeach f a
ApplyForeach (Sing a -> f a
forall (a :: k). Sing a -> f a
forall {k} (f :: k -> *) (a :: k). MonoidForeach f => Sing a -> f a
emptyForeach Sing a
s)
class EqForall f where
eqForall :: f a -> f a -> Bool
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 = f a -> f b -> WitnessedEquality a b
forall {k} (f :: k -> *) (a :: k) (b :: k).
(TestEquality f, EqForall f) =>
f a -> f b -> WitnessedEquality a b
defaultEqForallPoly
class (OrdForall f, EqForallPoly f) => OrdForallPoly f where
compareForallPoly :: f a -> f b -> WitnessedOrdering a b
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 = Int -> f a -> ShowS
forall (a :: k). Int -> f a -> ShowS
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 = Sing a -> Int -> f a -> ShowS
forall (a :: k). Sing a -> Int -> f a -> ShowS
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 = f a -> ShowS
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 = Int -> f a b -> ShowS
forall (a :: k) (b :: k). Int -> f a b -> ShowS
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 = f a b -> ShowS
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 EnumForall f where
toEnumForall :: Int -> f a
:: f a -> Int
class EnumExists f where
toEnumExists :: Int -> Exists f
:: 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
class StorableForall (f :: k -> Type) where
peekForall :: Ptr (f a) -> IO (f a)
pokeForall :: Ptr (f a) -> f a -> IO ()
sizeOfForall :: Proxy f -> Int
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)
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 = Int -> Proxy a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec
instance ReadExists Proxy where
readPrecExists :: ReadPrec (Exists Proxy)
readPrecExists = (Proxy Any -> Exists Proxy)
-> ReadPrec (Proxy Any) -> ReadPrec (Exists Proxy)
forall a b. (a -> b) -> ReadPrec a -> ReadPrec b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Proxy Any -> Exists Proxy
forall k (f :: k -> *) (a :: k). f a -> Exists f
Exists ReadPrec (Proxy Any)
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
_ = 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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10)
(ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Const "
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> ShowS
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 a -> a -> Bool
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) = a -> a -> Ordering
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) = Int -> a -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s a
a
instance EqForallPoly f => Eq (Exists f) where
Exists f a
a == :: Exists f -> Exists f -> Bool
== Exists f a
b = WitnessedEquality a a -> Bool
forall {k} (a :: k) (b :: k). WitnessedEquality a b -> Bool
weakenEquality (f a -> f a -> WitnessedEquality a a
forall (a :: k) (b :: k). f a -> f b -> WitnessedEquality a b
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 = WitnessedEquality '(a, b) '(a, b) -> Bool
forall {k} (a :: k) (b :: k). WitnessedEquality a b -> Bool
weakenEquality (f a b -> f a b -> WitnessedEquality '(a, b) '(a, b)
forall (a :: k) (b :: j) (c :: k) (d :: j).
f a b -> f c d -> WitnessedEquality '(a, b) '(c, d)
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) = WitnessedOrdering a a -> Ordering
forall {k} (a :: k) (b :: k). WitnessedOrdering a b -> Ordering
weakenOrdering (f a -> f a -> WitnessedOrdering a a
forall (a :: k) (b :: k). f a -> f b -> WitnessedOrdering a b
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) = Int -> f a -> Int
forall (a :: k). Int -> f a -> Int
forall {k} (f :: k -> *) (a :: k).
HashableForall f =>
Int -> f a -> Int
hashWithSaltForall Int
s f a
a
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11)
(String -> ShowS
showString String
"Exists " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> f a -> ShowS
forall (a :: k). Int -> f a -> ShowS
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11)
(String -> ShowS
showString String
"Exists " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> f a b -> ShowS
forall (a :: k) (b :: j). Int -> f a b -> ShowS
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 = ReadPrec (Exists f) -> ReadPrec (Exists f)
forall a. ReadPrec a -> ReadPrec a
R.parens (ReadPrec (Exists f) -> ReadPrec (Exists f))
-> ReadPrec (Exists f) -> ReadPrec (Exists f)
forall a b. (a -> b) -> a -> b
$ Int -> ReadPrec (Exists f) -> ReadPrec (Exists f)
forall a. Int -> ReadPrec a -> ReadPrec a
R.prec Int
10 (ReadPrec (Exists f) -> ReadPrec (Exists f))
-> ReadPrec (Exists f) -> ReadPrec (Exists f)
forall a b. (a -> b) -> a -> b
$ do
R.Ident String
"Exists" <- ReadPrec Lexeme
R.lexP
ReadPrec (Exists f) -> ReadPrec (Exists f)
forall a. ReadPrec a -> ReadPrec a
R.step ReadPrec (Exists f)
forall k (f :: k -> *). ReadExists f => ReadPrec (Exists f)
readPrecExists
instance EnumExists f => Enum (Exists f) where
fromEnum :: Exists f -> Int
fromEnum = Exists f -> Int
forall k (f :: k -> *). EnumExists f => Exists f -> Int
fromEnumExists
toEnum :: Int -> Exists f
toEnum = Int -> Exists f
forall k (f :: k -> *). EnumExists f => Int -> Exists f
toEnumExists
instance BoundedExists f => Bounded (Exists f) where
minBound :: Exists f
minBound = Exists f
forall k (f :: k -> *). BoundedExists f => Exists f
minBoundExists
maxBound :: Exists f
maxBound = Exists f
forall k (f :: k -> *). BoundedExists f => Exists f
maxBoundExists
instance BinaryExists f => Binary (Exists f) where
get :: Get (Exists f)
get = Get (Exists f)
forall k (f :: k -> *). BinaryExists f => Get (Exists f)
getExists
put :: Exists f -> Put
put = Exists f -> Put
forall k (f :: k -> *). BinaryExists f => Exists f -> Put
putExists
instance BinaryExists2 f => Binary (Exists2 f) where
get :: Get (Exists2 f)
get = Get (Exists2 f)
forall k j (f :: k -> j -> *). BinaryExists2 f => Get (Exists2 f)
getExists2
put :: Exists2 f -> Put
put = Exists2 f -> 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 = Exists f -> Text
forall k (f :: k -> *). PathPieceExists f => Exists f -> Text
toPathPieceForall
fromPathPiece :: Text -> Maybe (Exists f)
fromPathPiece = Text -> Maybe (Exists f)
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) = f a -> f a -> Bool
forall (a :: k). f a -> f a -> Bool
forall {k} (f :: k -> *) (a :: k). EqForall f => f a -> f a -> Bool
eqForall f a
f1 f a
f2 Bool -> Bool -> Bool
&& g a -> g a -> Bool
forall (a :: k). g a -> g a -> 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 f a -> f b -> WitnessedEquality a b
forall (a :: k) (b :: k). f a -> f b -> WitnessedEquality a b
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 -> g a -> g b -> WitnessedEquality a b
forall (a :: k) (b :: k). g a -> g b -> WitnessedEquality a b
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 -> WitnessedEquality a b
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) = Ordering -> Ordering -> Ordering
forall a. Monoid a => a -> a -> a
mappend (f a -> f a -> Ordering
forall (a :: k). f a -> f a -> Ordering
forall {k} (f :: k -> *) (a :: k).
OrdForall f =>
f a -> f a -> Ordering
compareForall f a
f1 f a
f2) (g a -> g a -> Ordering
forall (a :: k). g a -> g a -> Ordering
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 f a -> f b -> WitnessedOrdering a b
forall (a :: k) (b :: k). f a -> f b -> WitnessedOrdering a b
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 -> WitnessedOrdering a b
forall {k} (a :: k) (b :: k). WitnessedOrdering a b
WitnessedOrderingLT
WitnessedOrdering a b
WitnessedOrderingGT -> WitnessedOrdering a b
forall {k} (a :: k) (b :: k). WitnessedOrdering a b
WitnessedOrderingGT
WitnessedOrdering a b
WitnessedOrderingEQ -> g a -> g b -> WitnessedOrdering a b
forall (a :: k) (b :: k). g a -> g b -> WitnessedOrdering a b
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11)
(String -> ShowS
showString String
"Pair " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> f a -> ShowS
forall (a :: k). Int -> f a -> ShowS
forall {k} (f :: k -> *) (a :: k).
ShowForall f =>
Int -> f a -> ShowS
showsPrecForall Int
11 f a
f ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' ' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> g a -> ShowS
forall (a :: k). Int -> g a -> ShowS
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) = (g a -> g a -> Ordering) -> f (g a) -> f (g a) -> Ordering
forall a b. (a -> b -> Ordering) -> f a -> f b -> Ordering
forall (f :: * -> *) a b.
Ord1 f =>
(a -> b -> Ordering) -> f a -> f b -> Ordering
liftCompare (Sing a -> g a -> g a -> Ordering
forall (a :: k). Sing a -> g a -> g a -> Ordering
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) = f (g a) -> Compose f g a
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose ((g a -> g a -> g a) -> f (g a) -> f (g a) -> f (g a)
forall a. (a -> a -> a) -> f a -> f a -> f a
forall (f :: * -> *) a.
Semigroup1 f =>
(a -> a -> a) -> f a -> f a -> f a
liftAppend g a -> g a -> g a
forall (a :: k). g a -> g a -> g a
forall {k} (f :: k -> *) (a :: k).
SemigroupForall f =>
f a -> f a -> f a
appendForall f (g a)
x f (g a)
y)
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) = (g a -> g a -> Bool) -> f (g a) -> f (g a) -> Bool
forall a b. (a -> b -> Bool) -> f a -> f b -> Bool
forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq g a -> g a -> Bool
forall (a :: k). g a -> g a -> Bool
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) = (g a -> g a -> Bool) -> f (g a) -> f (g a) -> Bool
forall a b. (a -> b -> Bool) -> f a -> f b -> Bool
forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq (Sing a -> g a -> g a -> Bool
forall (a :: k). Sing a -> g a -> g a -> Bool
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Compose " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> g a -> ShowS)
-> ([g a] -> ShowS) -> Int -> f (g a) -> ShowS
forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS
forall (f :: * -> *) a.
Show1 f =>
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS
liftShowsPrec Int -> g a -> ShowS
forall (a :: k). Int -> g a -> ShowS
forall {k} (f :: k -> *) (a :: k).
ShowForall f =>
Int -> f a -> ShowS
showsPrecForall [g a] -> ShowS
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Compose " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> g a -> ShowS)
-> ([g a] -> ShowS) -> Int -> f (g a) -> ShowS
forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS
forall (f :: * -> *) a.
Show1 f =>
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS
liftShowsPrec (Sing a -> Int -> g a -> ShowS
forall (a :: k). Sing a -> Int -> g a -> ShowS
forall {k} (f :: k -> *) (a :: k).
ShowForeach f =>
Sing a -> Int -> f a -> ShowS
showsPrecForeach Sing a
s) (Sing a -> [g a] -> ShowS
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) = f (g a) -> Compose f g a
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose ((g a -> g a -> g a) -> f (g a) -> f (g a) -> f (g a)
forall a. (a -> a -> a) -> f a -> f a -> f a
forall (f :: * -> *) a.
Semigroup1 f =>
(a -> a -> a) -> f a -> f a -> f a
liftAppend (Sing a -> g a -> g a -> g a
forall (a :: k). Sing a -> g a -> g a -> g a
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) = (g a -> Put) -> f (g a) -> Put
forall a. (a -> Put) -> f a -> Put
forall (f :: * -> *) a. Binary1 f => (a -> Put) -> f a -> Put
liftPut (Sing a -> g a -> Put
forall (a :: k). Sing a -> g a -> Put
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 = (f (g a) -> Compose f g a) -> Get (f (g a)) -> Get (Compose f g a)
forall a b. (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (g a) -> Compose f g a
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Get (g a) -> Get (f (g a))
forall a. Get a -> Get (f a)
forall (f :: * -> *) a. Binary1 f => Get a -> Get (f a)
liftGet (Sing a -> Get (g a)
forall (a :: k). Sing a -> Get (g a)
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 = (f a -> ShowS) -> [f a] -> ShowS
forall a. (a -> ShowS) -> [a] -> ShowS
showList__ f a -> ShowS
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 = (f a -> ShowS) -> [f a] -> ShowS
forall a. (a -> ShowS) -> [a] -> ShowS
showList__ (Sing a -> f a -> ShowS
forall {k} (f :: k -> *) (a :: k).
ShowForeach f =>
Sing a -> f a -> ShowS
showsForeach Sing a
s)
showList__ :: (a -> ShowS) -> [a] -> ShowS
showList__ :: forall a. (a -> ShowS) -> [a] -> ShowS
showList__ a -> ShowS
_ [] String
s = String
"[]" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s
showList__ a -> ShowS
showx (a
x:[a]
xs) String
s = Char
'[' Char -> ShowS
forall a. a -> [a] -> [a]
: a -> ShowS
showx a
x ([a] -> String
showl [a]
xs)
where
showl :: [a] -> String
showl [] = Char
']' Char -> ShowS
forall a. a -> [a] -> [a]
: String
s
showl (a
y:[a]
ys) = Char
',' Char -> ShowS
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) = f a -> f a -> Bool
forall (a :: k). f a -> f a -> Bool
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) = g a -> g a -> Bool
forall (a :: k). g a -> g a -> Bool
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) = f a -> f a -> Ordering
forall (a :: k). f a -> f a -> Ordering
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) = g a -> g a -> Ordering
forall (a :: k). g a -> g a -> Ordering
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 f a -> f b -> Maybe (a :~: b)
forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b)
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 -> Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (f a -> Int
forall a. a -> Int
getTagBox f a
a) (f b -> Int
forall a. a -> Int
getTagBox f b
b)
Just a :~: b
Refl -> f a -> f a -> Ordering
forall (a :: k). f a -> f a -> Ordering
forall {k} (f :: k -> *) (a :: k).
OrdForall f =>
f a -> f a -> Ordering
compareForall f a
a f 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 f a -> f b -> Maybe (a :~: b)
forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b)
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 -> WitnessedEquality a b
forall {k} (a :: k) (b :: k). WitnessedEquality a b
WitnessedEqualityUnequal
Just a :~: b
Refl -> if f a -> f a -> Bool
forall (a :: k). f a -> f a -> Bool
forall {k} (f :: k -> *) (a :: k). EqForall f => f a -> f a -> Bool
eqForall f a
x f a
f b
y then WitnessedEquality a a
WitnessedEquality a b
forall {k} (a :: k). WitnessedEquality a a
WitnessedEqualityEqual else WitnessedEquality a b
forall {k} (a :: k) (b :: k). WitnessedEquality a b
WitnessedEqualityUnequal
getTagBox :: a -> Int
getTagBox :: forall a. a -> Int
getTagBox !a
x = Int# -> Int
I# (a -> Int#
forall a. a -> Int#
dataToTag# a
x)
{-# INLINE getTagBox #-}
type family Sing = (r :: k -> Type) | r -> k
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) = Sing r -> k
forall (a :: k). Sing a -> k
forall k (a :: k). SingKind k => Sing a -> k
demoteSing Sing r
s k -> [k] -> [k]
forall a. a -> [a] -> [a]
: Sing rs -> [k]
forall (a :: [k]). Sing a -> [k]
forall k (a :: k). SingKind k => Sing a -> k
demoteSing SingList rs
Sing rs
ss
promoteSing :: [k] -> Exists Sing
promoteSing [] = SingList '[] -> Exists SingList
forall k (f :: k -> *) (a :: k). f a -> Exists f
Exists SingList '[]
forall {k}. SingList '[]
SingListNil
promoteSing (k
x : [k]
xs) = case k -> Exists Sing
forall k. SingKind k => k -> Exists Sing
promoteSing k
x of
Exists Sing a
s -> case [k] -> Exists Sing
forall k. SingKind k => k -> Exists Sing
promoteSing [k]
xs of
Exists Sing a
ss -> SingList (a : a) -> Exists SingList
forall k (f :: k -> *) (a :: k). f a -> Exists f
Exists (Sing a -> SingList a -> SingList (a : a)
forall {k} (a :: k) (rs :: [k]).
Sing a -> SingList rs -> SingList (a : rs)
SingListCons Sing a
s SingList a
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 = SingList a -> (Reify a => b) -> b
Sing a -> (Reify a => b) -> b
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 = SingList '[]
Sing '[]
forall {k}. SingList '[]
SingListNil
instance (Reify a, Reify as) => Reify (a ': as) where
reify :: Sing (a : as)
reify = Sing a -> SingList as -> SingList (a : as)
forall {k} (a :: k) (rs :: [k]).
Sing a -> SingList rs -> SingList (a : rs)
SingListCons Sing a
forall {k} (a :: k). Reify a => Sing a
reify SingList as
Sing as
forall {k} (a :: k). Reify a => Sing a
reify
instance Reify 'Nothing where
reify :: Sing 'Nothing
reify = SingMaybe 'Nothing
Sing 'Nothing
forall {k}. SingMaybe 'Nothing
SingMaybeNothing
instance Reify a => Reify ('Just a) where
reify :: Sing ('Just a)
reify = Sing a -> SingMaybe ('Just a)
forall {k} (a :: k). Sing a -> SingMaybe ('Just a)
SingMaybeJust Sing a
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 = SingList a -> SingList b -> Maybe (a :~: b)
Sing a -> Sing b -> Maybe (a :~: b)
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 = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
eqSingList SingList a
SingListNil (SingListCons Sing r
_ SingList rs
_) = Maybe (a :~: b)
forall a. Maybe a
Nothing
eqSingList (SingListCons Sing r
_ SingList rs
_) SingList b
SingListNil = Maybe (a :~: b)
forall a. Maybe a
Nothing
eqSingList (SingListCons Sing r
a SingList rs
as) (SingListCons Sing r
b SingList rs
bs) = case Sing r -> Sing r -> Maybe (r :~: r)
forall (a :: k) (b :: k). Sing a -> Sing b -> Maybe (a :~: b)
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 SingList rs -> SingList rs -> Maybe (rs :~: rs)
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 -> (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
Maybe (rs :~: rs)
Nothing -> Maybe (a :~: b)
forall a. Maybe a
Nothing
Maybe (r :~: r)
Nothing -> Maybe (a :~: b)
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)
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 = WitnessedEquality a a
WitnessedEquality a b
forall {k} (a :: k). WitnessedEquality a a
WitnessedEqualityEqual
eqForallPoly SingList a
SingListNil (SingListCons Sing r
_ SingList rs
_) = WitnessedEquality a b
forall {k} (a :: k) (b :: k). WitnessedEquality a b
WitnessedEqualityUnequal
eqForallPoly (SingListCons Sing r
_ SingList rs
_) SingList b
SingListNil = WitnessedEquality a b
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 Sing r -> Sing r -> Maybe (r :~: r)
forall (a :: k) (b :: k). Sing a -> Sing b -> Maybe (a :~: b)
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 -> WitnessedEquality a b
forall {k} (a :: k) (b :: k). WitnessedEquality a b
WitnessedEqualityUnequal
Just r :~: r
Refl -> case SingList rs -> SingList rs -> WitnessedEquality rs rs
forall (a :: [k]) (b :: [k]).
SingList a -> SingList b -> WitnessedEquality a b
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 -> WitnessedEquality a b
forall {k} (a :: k) (b :: k). WitnessedEquality a b
WitnessedEqualityUnequal
WitnessedEquality rs rs
WitnessedEqualityEqual -> WitnessedEquality a a
WitnessedEquality a b
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) = [k] -> Put
forall t. Binary t => t -> Put
BN.put (Sing a -> [k]
forall (a :: [k]). Sing a -> [k]
forall k (a :: k). SingKind k => Sing a -> k
demoteSing SingList a
Sing a
xs)
getExists :: Get (Exists SingList)
getExists = ([k] -> Exists SingList) -> Get [k] -> Get (Exists SingList)
forall a b. (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [k] -> Exists SingList
[k] -> Exists Sing
forall k. SingKind k => k -> Exists Sing
promoteSing Get [k]
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10)
(ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"SingListCons "
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Sing r -> ShowS
forall (a :: k). Int -> Sing a -> ShowS
forall k (a :: k). ShowSing k => Int -> Sing a -> ShowS
showsPrecSing Int
11 Sing r
s
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' '
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> SingList rs -> ShowS
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 = Int -> SingList a -> ShowS
Int -> Sing a -> ShowS
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 = b
Reify as => b
b
unreifyList (SingListCons Sing r
s SingList rs
ss) Reify as => b
b = Sing r -> (Reify r => b) -> b
forall (a :: k) b. Sing a -> (Reify a => b) -> b
forall k (a :: k) b. Unreify k => Sing a -> (Reify a => b) -> b
unreify Sing r
s (SingList rs -> (Reify rs => b) -> b
forall k (as :: [k]) b.
Unreify k =>
SingList as -> (Reify as => b) -> b
unreifyList SingList rs
ss b
Reify as => b
Reify rs => 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 Sing a -> Sing a -> Maybe (a :~: a)
forall (a :: k) (b :: k). Sing a -> Sing b -> Maybe (a :~: b)
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 -> Sing a -> f a -> f a -> Bool
forall (a :: k). Sing a -> f a -> f a -> Bool
forall {k} (f :: k -> *) (a :: k).
EqForeach f =>
Sing a -> f a -> f a -> Bool
eqForeach Sing a
s1 f a
v1 f a
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 Sing a -> Sing a -> WitnessedOrdering a a
forall (a :: k) (b :: k). Sing a -> Sing b -> WitnessedOrdering a b
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 -> Sing a -> f a -> f a -> Ordering
forall (a :: k). Sing a -> f a -> f a -> Ordering
forall {k} (f :: k -> *) (a :: k).
OrdForeach f =>
Sing a -> f a -> f a -> Ordering
compareForeach Sing a
s1 f a
v1 f a
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11)
(ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Sing "
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Sing a -> ShowS
forall (a :: k). Int -> Sing a -> ShowS
forall k (a :: k). ShowSing k => Int -> Sing a -> ShowS
showsPrecSing Int
11 Sing a
s
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' '
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing a -> Int -> f a -> ShowS
forall (a :: k). Sing a -> Int -> f a -> ShowS
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
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 -> WitnessedEquality a a
forall {k} (a :: k). WitnessedEquality a a
WitnessedEqualityEqual
Bool
False -> WitnessedEquality a a
forall {k} (a :: k) (b :: k). WitnessedEquality a b
WitnessedEqualityUnequal
strengthenOrdering :: Ordering -> WitnessedOrdering a a
strengthenOrdering :: forall {k} (a :: k). Ordering -> WitnessedOrdering a a
strengthenOrdering = \case
Ordering
LT -> WitnessedOrdering a a
forall {k} (a :: k) (b :: k). WitnessedOrdering a b
WitnessedOrderingLT
Ordering
EQ -> WitnessedOrdering a a
forall {k} (a :: k). WitnessedOrdering a a
WitnessedOrderingEQ
Ordering
GT -> WitnessedOrdering a a
forall {k} (a :: k) (b :: k). WitnessedOrdering a b
WitnessedOrderingGT
strengthenUnequalOrdering :: Ordering -> WitnessedOrdering a b
strengthenUnequalOrdering :: forall {k} (a :: k) (b :: k). Ordering -> WitnessedOrdering a b
strengthenUnequalOrdering = \case
Ordering
LT -> WitnessedOrdering a b
forall {k} (a :: k) (b :: k). WitnessedOrdering a b
WitnessedOrderingLT
Ordering
EQ -> WitnessedOrdering a b
forall {k} (a :: k) (b :: k). WitnessedOrdering a b
WitnessedOrderingLT
Ordering
GT -> WitnessedOrdering a b
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 f a -> f a -> WitnessedEquality a a
forall (a :: k) (b :: k). f a -> f b -> WitnessedEquality a b
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 -> Sing a -> g a -> g a -> Bool
forall (a :: k). Sing a -> g a -> g a -> Bool
forall {k} (f :: k -> *) (a :: k).
EqForeach f =>
Sing a -> f a -> f a -> Bool
eqForeach (f a -> Sing a
forall (a :: k). f a -> Sing a
forall k (f :: k -> *) (a :: k). ToSing f => f a -> Sing a
toSing f a
a1) g a
b1 g a
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 f a -> f a -> WitnessedOrdering a a
forall (a :: k) (b :: k). f a -> f b -> WitnessedOrdering a b
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 -> Sing a -> g a -> g a -> Ordering
forall (a :: k). Sing a -> g a -> g a -> Ordering
forall {k} (f :: k -> *) (a :: k).
OrdForeach f =>
Sing a -> f a -> f a -> Ordering
compareForeach (f a -> Sing a
forall (a :: k). f a -> Sing a
forall k (f :: k -> *) (a :: k). ToSing f => f a -> Sing a
toSing f a
a1) g a
b1 g a
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11)
(String -> ShowS
showString String
"DependentPair " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> f a -> ShowS
forall (a :: k). Int -> f a -> ShowS
forall {k} (f :: k -> *) (a :: k).
ShowForall f =>
Int -> f a -> ShowS
showsPrecForall Int
11 f a
a ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' ' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing a -> Int -> g a -> ShowS
forall (a :: k). Sing a -> Int -> g a -> ShowS
forall {k} (f :: k -> *) (a :: k).
ShowForeach f =>
Sing a -> Int -> f a -> ShowS
showsPrecForeach (f a -> Sing a
forall (a :: k). f a -> Sing a
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) = a -> Const a a
forall {k} a (b :: k). a -> Const a b
Const (a
x a -> a -> a
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 = a -> Const a a
forall {k} a (b :: k). a -> Const a b
Const a
forall a. Monoid a => a
mempty