{-# 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 #-}

{-| 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(..)
  , 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(..)
  , ToSing(..)
  , SingKind(..)
    -- * Functions
    -- ** Show
  , showsForall
  , showsForeach
  , showForall
  , showListForall
  , showListForeach
  , showsForall2
  , showForall2
    -- ** Defaulting
  , defaultEqForallPoly
  , defaultCompareForallPoly
    -- ** Weakening
  , weakenEquality
  , weakenOrdering
  , strengthenEquality
  , strengthenOrdering
  , strengthenUnequalOrdering
    -- ** Other
  , 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

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

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

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

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

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

-- 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
"[]" 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

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

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

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

-- | 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 -> 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 -- this case should not happen                                          
  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