{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module Universe.Core
( Esc
, Some (..)
, SomeTypeIn (..)
, Kinded (..)
, ValueOf (..)
, Contains (..)
, Includes
, knownUniOf
, someType
, someValueOf
, someValue
, someValueType
, DecodeUniM (..)
, Closed (..)
, decodeKindedUni
, peelUniTag
, Permits
, EverywhereAll
, type (<:)
, HasUniApply (..)
, checkStar
, withApplicable
, tryUniApply
, GShow (..)
, gshow
, GEq (..)
, defaultEq
, (:~:)(..)
, DSum (..)
) where
import Control.Applicative
import Control.DeepSeq
import Control.Monad
import Control.Monad.Trans.State.Strict
import Data.Dependent.Sum
import Data.GADT.Compare
import Data.GADT.DeepSeq
import Data.GADT.Show
import Data.Hashable
import Data.Kind
import Data.Proxy
import Data.Some.Newtype
import Data.Type.Equality
import Text.Show.Deriving
import Type.Reflection
type Esc :: forall k. k -> Type
data Esc a
type SomeTypeIn :: (Type -> Type) -> Type
data SomeTypeIn uni = forall k (a :: k). SomeTypeIn !(uni (Esc a))
data Kinded uni ta where
Kinded :: Typeable k => !(uni (Esc a)) -> Kinded uni (Esc (a :: k))
type ValueOf :: (Type -> Type) -> Type -> Type
data ValueOf uni a = ValueOf !(uni (Esc a)) !a
type Contains :: forall k. (Type -> Type) -> k -> Constraint
class uni `Contains` a where
knownUni :: uni (Esc a)
instance (Typeable k, uni `Contains` a) => Kinded uni `Contains` (a :: k) where
knownUni :: Kinded uni (Esc a)
knownUni = uni (Esc a) -> Kinded uni (Esc a)
forall k (uni :: * -> *) (a :: k).
Typeable k =>
uni (Esc a) -> Kinded uni (Esc a)
Kinded uni (Esc a)
forall k (uni :: * -> *) (a :: k). Contains uni a => uni (Esc a)
knownUni
type Includes :: forall k. (Type -> Type) -> k -> Constraint
type Includes uni = Permits (Contains uni)
knownUniOf :: uni `Contains` a => proxy a -> uni (Esc a)
knownUniOf :: forall {k} (uni :: * -> *) (a :: k) (proxy :: k -> *).
Contains uni a =>
proxy a -> uni (Esc a)
knownUniOf proxy a
_ = uni (Esc a)
forall k (uni :: * -> *) (a :: k). Contains uni a => uni (Esc a)
knownUni
someType :: forall k (a :: k) uni. uni `Contains` a => SomeTypeIn uni
someType :: forall k (a :: k) (uni :: * -> *). Contains uni a => SomeTypeIn uni
someType = uni (Esc a) -> SomeTypeIn uni
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn (uni (Esc a) -> SomeTypeIn uni) -> uni (Esc a) -> SomeTypeIn uni
forall a b. (a -> b) -> a -> b
$ forall k (uni :: * -> *) (a :: k). Contains uni a => uni (Esc a)
knownUni @k @uni @a
someValueOf :: forall a uni. uni (Esc a) -> a -> Some (ValueOf uni)
someValueOf :: forall a (uni :: * -> *). uni (Esc a) -> a -> Some (ValueOf uni)
someValueOf uni (Esc a)
uni = ValueOf uni a -> Some (ValueOf uni)
forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
Some (ValueOf uni a -> Some (ValueOf uni))
-> (a -> ValueOf uni a) -> a -> Some (ValueOf uni)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. uni (Esc a) -> a -> ValueOf uni a
forall (uni :: * -> *) a. uni (Esc a) -> a -> ValueOf uni a
ValueOf uni (Esc a)
uni
someValue :: forall a uni. uni `Contains` a => a -> Some (ValueOf uni)
someValue :: forall a (uni :: * -> *). Contains uni a => a -> Some (ValueOf uni)
someValue = uni (Esc a) -> a -> Some (ValueOf uni)
forall a (uni :: * -> *). uni (Esc a) -> a -> Some (ValueOf uni)
someValueOf uni (Esc a)
forall k (uni :: * -> *) (a :: k). Contains uni a => uni (Esc a)
knownUni
someValueType :: Some (ValueOf uni) -> SomeTypeIn uni
someValueType :: forall (uni :: * -> *). Some (ValueOf uni) -> SomeTypeIn uni
someValueType (Some (ValueOf uni (Esc a)
tag a
_)) = uni (Esc a) -> SomeTypeIn uni
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn uni (Esc a)
tag
newtype DecodeUniM a = DecodeUniM
{ forall a. DecodeUniM a -> StateT [Int] Maybe a
unDecodeUniM :: StateT [Int] Maybe a
} deriving newtype ((forall a b. (a -> b) -> DecodeUniM a -> DecodeUniM b)
-> (forall a b. a -> DecodeUniM b -> DecodeUniM a)
-> Functor DecodeUniM
forall a b. a -> DecodeUniM b -> DecodeUniM a
forall a b. (a -> b) -> DecodeUniM a -> DecodeUniM b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> DecodeUniM a -> DecodeUniM b
fmap :: forall a b. (a -> b) -> DecodeUniM a -> DecodeUniM b
$c<$ :: forall a b. a -> DecodeUniM b -> DecodeUniM a
<$ :: forall a b. a -> DecodeUniM b -> DecodeUniM a
Functor, Functor DecodeUniM
Functor DecodeUniM =>
(forall a. a -> DecodeUniM a)
-> (forall a b.
DecodeUniM (a -> b) -> DecodeUniM a -> DecodeUniM b)
-> (forall a b c.
(a -> b -> c) -> DecodeUniM a -> DecodeUniM b -> DecodeUniM c)
-> (forall a b. DecodeUniM a -> DecodeUniM b -> DecodeUniM b)
-> (forall a b. DecodeUniM a -> DecodeUniM b -> DecodeUniM a)
-> Applicative DecodeUniM
forall a. a -> DecodeUniM a
forall a b. DecodeUniM a -> DecodeUniM b -> DecodeUniM a
forall a b. DecodeUniM a -> DecodeUniM b -> DecodeUniM b
forall a b. DecodeUniM (a -> b) -> DecodeUniM a -> DecodeUniM b
forall a b c.
(a -> b -> c) -> DecodeUniM a -> DecodeUniM b -> DecodeUniM c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall a. a -> DecodeUniM a
pure :: forall a. a -> DecodeUniM a
$c<*> :: forall a b. DecodeUniM (a -> b) -> DecodeUniM a -> DecodeUniM b
<*> :: forall a b. DecodeUniM (a -> b) -> DecodeUniM a -> DecodeUniM b
$cliftA2 :: forall a b c.
(a -> b -> c) -> DecodeUniM a -> DecodeUniM b -> DecodeUniM c
liftA2 :: forall a b c.
(a -> b -> c) -> DecodeUniM a -> DecodeUniM b -> DecodeUniM c
$c*> :: forall a b. DecodeUniM a -> DecodeUniM b -> DecodeUniM b
*> :: forall a b. DecodeUniM a -> DecodeUniM b -> DecodeUniM b
$c<* :: forall a b. DecodeUniM a -> DecodeUniM b -> DecodeUniM a
<* :: forall a b. DecodeUniM a -> DecodeUniM b -> DecodeUniM a
Applicative, Applicative DecodeUniM
Applicative DecodeUniM =>
(forall a. DecodeUniM a)
-> (forall a. DecodeUniM a -> DecodeUniM a -> DecodeUniM a)
-> (forall a. DecodeUniM a -> DecodeUniM [a])
-> (forall a. DecodeUniM a -> DecodeUniM [a])
-> Alternative DecodeUniM
forall a. DecodeUniM a
forall a. DecodeUniM a -> DecodeUniM [a]
forall a. DecodeUniM a -> DecodeUniM a -> DecodeUniM a
forall (f :: * -> *).
Applicative f =>
(forall a. f a)
-> (forall a. f a -> f a -> f a)
-> (forall a. f a -> f [a])
-> (forall a. f a -> f [a])
-> Alternative f
$cempty :: forall a. DecodeUniM a
empty :: forall a. DecodeUniM a
$c<|> :: forall a. DecodeUniM a -> DecodeUniM a -> DecodeUniM a
<|> :: forall a. DecodeUniM a -> DecodeUniM a -> DecodeUniM a
$csome :: forall a. DecodeUniM a -> DecodeUniM [a]
some :: forall a. DecodeUniM a -> DecodeUniM [a]
$cmany :: forall a. DecodeUniM a -> DecodeUniM [a]
many :: forall a. DecodeUniM a -> DecodeUniM [a]
Alternative, Applicative DecodeUniM
Applicative DecodeUniM =>
(forall a b. DecodeUniM a -> (a -> DecodeUniM b) -> DecodeUniM b)
-> (forall a b. DecodeUniM a -> DecodeUniM b -> DecodeUniM b)
-> (forall a. a -> DecodeUniM a)
-> Monad DecodeUniM
forall a. a -> DecodeUniM a
forall a b. DecodeUniM a -> DecodeUniM b -> DecodeUniM b
forall a b. DecodeUniM a -> (a -> DecodeUniM b) -> DecodeUniM b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall a b. DecodeUniM a -> (a -> DecodeUniM b) -> DecodeUniM b
>>= :: forall a b. DecodeUniM a -> (a -> DecodeUniM b) -> DecodeUniM b
$c>> :: forall a b. DecodeUniM a -> DecodeUniM b -> DecodeUniM b
>> :: forall a b. DecodeUniM a -> DecodeUniM b -> DecodeUniM b
$creturn :: forall a. a -> DecodeUniM a
return :: forall a. a -> DecodeUniM a
Monad, Monad DecodeUniM
Alternative DecodeUniM
(Alternative DecodeUniM, Monad DecodeUniM) =>
(forall a. DecodeUniM a)
-> (forall a. DecodeUniM a -> DecodeUniM a -> DecodeUniM a)
-> MonadPlus DecodeUniM
forall a. DecodeUniM a
forall a. DecodeUniM a -> DecodeUniM a -> DecodeUniM a
forall (m :: * -> *).
(Alternative m, Monad m) =>
(forall a. m a) -> (forall a. m a -> m a -> m a) -> MonadPlus m
$cmzero :: forall a. DecodeUniM a
mzero :: forall a. DecodeUniM a
$cmplus :: forall a. DecodeUniM a -> DecodeUniM a -> DecodeUniM a
mplus :: forall a. DecodeUniM a -> DecodeUniM a -> DecodeUniM a
MonadPlus, Monad DecodeUniM
Monad DecodeUniM =>
(forall a. String -> DecodeUniM a) -> MonadFail DecodeUniM
forall a. String -> DecodeUniM a
forall (m :: * -> *).
Monad m =>
(forall a. String -> m a) -> MonadFail m
$cfail :: forall a. String -> DecodeUniM a
fail :: forall a. String -> DecodeUniM a
MonadFail)
runDecodeUniM :: [Int] -> DecodeUniM a -> Maybe (a, [Int])
runDecodeUniM :: forall a. [Int] -> DecodeUniM a -> Maybe (a, [Int])
runDecodeUniM [Int]
is (DecodeUniM StateT [Int] Maybe a
a) = StateT [Int] Maybe a -> [Int] -> Maybe (a, [Int])
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT [Int] Maybe a
a [Int]
is
class Closed uni where
type Everywhere uni (constr :: Type -> Constraint) :: Constraint
encodeUni :: uni a -> [Int]
withDecodedUni :: (forall k (a :: k). Typeable k => uni (Esc a) -> DecodeUniM r) -> DecodeUniM r
bring :: uni `Everywhere` constr => proxy constr -> uni (Esc a) -> (constr a => r) -> r
decodeKindedUni :: Closed uni => [Int] -> Maybe (SomeTypeIn (Kinded uni))
decodeKindedUni :: forall (uni :: * -> *).
Closed uni =>
[Int] -> Maybe (SomeTypeIn (Kinded uni))
decodeKindedUni [Int]
is = do
(SomeTypeIn (Kinded uni)
x, []) <- [Int]
-> DecodeUniM (SomeTypeIn (Kinded uni))
-> Maybe (SomeTypeIn (Kinded uni), [Int])
forall a. [Int] -> DecodeUniM a -> Maybe (a, [Int])
runDecodeUniM [Int]
is (DecodeUniM (SomeTypeIn (Kinded uni))
-> Maybe (SomeTypeIn (Kinded uni), [Int]))
-> DecodeUniM (SomeTypeIn (Kinded uni))
-> Maybe (SomeTypeIn (Kinded uni), [Int])
forall a b. (a -> b) -> a -> b
$ (forall k (a :: k).
Typeable k =>
uni (Esc a) -> DecodeUniM (SomeTypeIn (Kinded uni)))
-> DecodeUniM (SomeTypeIn (Kinded uni))
forall r.
(forall k (a :: k). Typeable k => uni (Esc a) -> DecodeUniM r)
-> DecodeUniM r
forall (uni :: * -> *) r.
Closed uni =>
(forall k (a :: k). Typeable k => uni (Esc a) -> DecodeUniM r)
-> DecodeUniM r
withDecodedUni ((forall k (a :: k).
Typeable k =>
uni (Esc a) -> DecodeUniM (SomeTypeIn (Kinded uni)))
-> DecodeUniM (SomeTypeIn (Kinded uni)))
-> (forall k (a :: k).
Typeable k =>
uni (Esc a) -> DecodeUniM (SomeTypeIn (Kinded uni)))
-> DecodeUniM (SomeTypeIn (Kinded uni))
forall a b. (a -> b) -> a -> b
$ SomeTypeIn (Kinded uni) -> DecodeUniM (SomeTypeIn (Kinded uni))
forall a. a -> DecodeUniM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeTypeIn (Kinded uni) -> DecodeUniM (SomeTypeIn (Kinded uni)))
-> (uni (Esc a) -> SomeTypeIn (Kinded uni))
-> uni (Esc a)
-> DecodeUniM (SomeTypeIn (Kinded uni))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kinded uni (Esc a) -> SomeTypeIn (Kinded uni)
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn (Kinded uni (Esc a) -> SomeTypeIn (Kinded uni))
-> (uni (Esc a) -> Kinded uni (Esc a))
-> uni (Esc a)
-> SomeTypeIn (Kinded uni)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. uni (Esc a) -> Kinded uni (Esc a)
forall k (uni :: * -> *) (a :: k).
Typeable k =>
uni (Esc a) -> Kinded uni (Esc a)
Kinded
SomeTypeIn (Kinded uni) -> Maybe (SomeTypeIn (Kinded uni))
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SomeTypeIn (Kinded uni)
x
peelUniTag :: DecodeUniM Int
peelUniTag :: DecodeUniM Int
peelUniTag = StateT [Int] Maybe Int -> DecodeUniM Int
forall a. StateT [Int] Maybe a -> DecodeUniM a
DecodeUniM (StateT [Int] Maybe Int -> DecodeUniM Int)
-> StateT [Int] Maybe Int -> DecodeUniM Int
forall a b. (a -> b) -> a -> b
$ do
Int
i:[Int]
is <- StateT [Int] Maybe [Int]
forall (m :: * -> *) s. Monad m => StateT s m s
get
Int
i Int -> StateT [Int] Maybe () -> StateT [Int] Maybe Int
forall a b. a -> StateT [Int] Maybe b -> StateT [Int] Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Int] -> StateT [Int] Maybe ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put [Int]
is
type Permits0 :: (Type -> Constraint) -> Type -> Constraint
class constr x => constr `Permits0` x
instance constr x => constr `Permits0` x
type Permits1 :: (Type -> Constraint) -> (Type -> Type) -> Constraint
class (forall a. constr a => constr (f a)) => constr `Permits1` f
instance (forall a. constr a => constr (f a)) => constr `Permits1` f
type Permits2 :: (Type -> Constraint) -> (Type -> Type -> Type) -> Constraint
class (forall a b. (constr a, constr b) => constr (f a b)) => constr `Permits2` f
instance (forall a b. (constr a, constr b) => constr (f a b)) => constr `Permits2` f
type Permits3 :: (Type -> Constraint) -> (Type -> Type -> Type -> Type) -> Constraint
class (forall a b c. (constr a, constr b, constr c) => constr (f a b c)) => constr `Permits3` f
instance (forall a b c. (constr a, constr b, constr c) => constr (f a b c)) => constr `Permits3` f
type Permits :: forall k. (Type -> Constraint) -> k -> Constraint
type family Permits constr
type instance Permits @Type constr = Permits0 constr
type instance Permits @(Type -> Type) constr = Permits1 constr
type instance Permits @(Type -> Type -> Type) constr = Permits2 constr
type instance Permits @(Type -> Type -> Type -> Type) constr = Permits3 constr
type EverywhereAll :: (Type -> Type) -> [Type -> Constraint] -> Constraint
type family uni `EverywhereAll` constrs where
uni `EverywhereAll` '[] = ()
uni `EverywhereAll` (constr ': constrs) = (uni `Everywhere` constr, uni `EverywhereAll` constrs)
type uni1 <: uni2 = uni1 `Everywhere` Includes uni2
class HasUniApply (uni :: Type -> Type) where
uniApply :: forall k l (f :: k -> l) a. uni (Esc f) -> uni (Esc a) -> uni (Esc (f a))
matchUniApply
:: uni tb
-> r
-> (forall k l (f :: k -> l) a. tb ~ Esc (f a) => uni (Esc f) -> uni (Esc a) -> r)
-> r
checkStar :: forall uni a (x :: a). Typeable a => uni (Esc x) -> Maybe (a :~: Type)
checkStar :: forall (uni :: * -> *) a (x :: a).
Typeable a =>
uni (Esc x) -> Maybe (a :~: *)
checkStar uni (Esc x)
_ = forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a TypeRep a -> TypeRep (*) -> Maybe (a :~: *)
forall a b. TypeRep a -> TypeRep b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
`testEquality` forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @Type
fromJustM :: MonadPlus f => Maybe a -> f a
fromJustM :: forall (f :: * -> *) a. MonadPlus f => Maybe a -> f a
fromJustM = f a -> (a -> f a) -> Maybe a -> f a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe f a
forall a. f a
forall (m :: * -> *) a. MonadPlus m => m a
mzero a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
withApplicable
:: forall (a :: Type) (ab :: Type) f x uni m r. (Typeable ab, Typeable a, MonadPlus m)
=> uni (Esc (f :: ab))
-> uni (Esc (x :: a))
-> (forall (b :: Type). (Typeable b, ab ~ (a -> b)) => m r)
-> m r
withApplicable :: forall a ab (f :: ab) (x :: a) (uni :: * -> *) (m :: * -> *) r.
(Typeable ab, Typeable a, MonadPlus m) =>
uni (Esc f)
-> uni (Esc x)
-> (forall b. (Typeable b, ab ~ (a -> b)) => m r)
-> m r
withApplicable uni (Esc f)
_ uni (Esc x)
_ forall b. (Typeable b, ab ~ (a -> b)) => m r
k =
case forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @ab of
Fun TypeRep arg
repA TypeRep res
repB -> do
a :~~: arg
HRefl <- Maybe (a :~~: arg) -> m (a :~~: arg)
forall (f :: * -> *) a. MonadPlus f => Maybe a -> f a
fromJustM (Maybe (a :~~: arg) -> m (a :~~: arg))
-> Maybe (a :~~: arg) -> m (a :~~: arg)
forall a b. (a -> b) -> a -> b
$ forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a TypeRep a -> TypeRep arg -> Maybe (a :~~: arg)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
`eqTypeRep` TypeRep arg
repA
TYPE r2 :~: *
Refl <- Maybe (TYPE r2 :~: *) -> m (TYPE r2 :~: *)
forall (f :: * -> *) a. MonadPlus f => Maybe a -> f a
fromJustM (Maybe (TYPE r2 :~: *) -> m (TYPE r2 :~: *))
-> Maybe (TYPE r2 :~: *) -> m (TYPE r2 :~: *)
forall a b. (a -> b) -> a -> b
$ TypeRep res -> TypeRep (TYPE r2)
forall k (a :: k). TypeRep a -> TypeRep k
typeRepKind TypeRep res
repB TypeRep (TYPE r2) -> TypeRep (*) -> Maybe (TYPE r2 :~: *)
forall a b. TypeRep a -> TypeRep b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
`testEquality` forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @Type
TypeRep res -> (Typeable res => m r) -> m r
forall k (a :: k) r. TypeRep a -> (Typeable a => r) -> r
withTypeable TypeRep res
repB m r
Typeable res => m r
forall b. (Typeable b, ab ~ (a -> b)) => m r
k
TypeRep ab
_ -> m r
forall a. m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
tryUniApply
:: (MonadPlus m, HasUniApply uni)
=> SomeTypeIn (Kinded uni) -> SomeTypeIn (Kinded uni) -> m (SomeTypeIn (Kinded uni))
tryUniApply :: forall (m :: * -> *) (uni :: * -> *).
(MonadPlus m, HasUniApply uni) =>
SomeTypeIn (Kinded uni)
-> SomeTypeIn (Kinded uni) -> m (SomeTypeIn (Kinded uni))
tryUniApply (SomeTypeIn (Kinded uni (Esc a)
uniF)) (SomeTypeIn (Kinded uni (Esc a)
uniA)) =
uni (Esc a)
-> uni (Esc a)
-> (forall {b}.
(Typeable b, k ~ (k -> b)) =>
m (SomeTypeIn (Kinded uni)))
-> m (SomeTypeIn (Kinded uni))
forall a ab (f :: ab) (x :: a) (uni :: * -> *) (m :: * -> *) r.
(Typeable ab, Typeable a, MonadPlus m) =>
uni (Esc f)
-> uni (Esc x)
-> (forall b. (Typeable b, ab ~ (a -> b)) => m r)
-> m r
withApplicable uni (Esc a)
uniF uni (Esc a)
uniA ((forall {b}.
(Typeable b, k ~ (k -> b)) =>
m (SomeTypeIn (Kinded uni)))
-> m (SomeTypeIn (Kinded uni)))
-> (forall {b}.
(Typeable b, k ~ (k -> b)) =>
m (SomeTypeIn (Kinded uni)))
-> m (SomeTypeIn (Kinded uni))
forall a b. (a -> b) -> a -> b
$
SomeTypeIn (Kinded uni) -> m (SomeTypeIn (Kinded uni))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeTypeIn (Kinded uni) -> m (SomeTypeIn (Kinded uni)))
-> (uni (Esc (a a)) -> SomeTypeIn (Kinded uni))
-> uni (Esc (a a))
-> m (SomeTypeIn (Kinded uni))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kinded uni (Esc (a a)) -> SomeTypeIn (Kinded uni)
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn (Kinded uni (Esc (a a)) -> SomeTypeIn (Kinded uni))
-> (uni (Esc (a a)) -> Kinded uni (Esc (a a)))
-> uni (Esc (a a))
-> SomeTypeIn (Kinded uni)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. uni (Esc (a a)) -> Kinded uni (Esc (a a))
forall k (uni :: * -> *) (a :: k).
Typeable k =>
uni (Esc a) -> Kinded uni (Esc a)
Kinded (uni (Esc (a a)) -> m (SomeTypeIn (Kinded uni)))
-> uni (Esc (a a)) -> m (SomeTypeIn (Kinded uni))
forall a b. (a -> b) -> a -> b
$ uni (Esc a)
uni (Esc a)
uniF uni (Esc a) -> uni (Esc a) -> uni (Esc (a a))
forall k l (f :: k -> l) (a :: k).
uni (Esc f) -> uni (Esc a) -> uni (Esc (f a))
forall (uni :: * -> *) k l (f :: k -> l) (a :: k).
HasUniApply uni =>
uni (Esc f) -> uni (Esc a) -> uni (Esc (f a))
`uniApply` uni (Esc a)
uniA
newtype AG f a = AG (f a)
$(return [])
instance GShow f => Show (AG f a) where
showsPrec :: Int -> AG f a -> ShowS
showsPrec Int
pr (AG f a
a) = Int -> f a -> ShowS
forall (a :: k). Int -> f a -> ShowS
forall k (t :: k -> *) (a :: k). GShow t => Int -> t a -> ShowS
gshowsPrec Int
pr f a
a
instance GShow uni => Show (SomeTypeIn uni) where
showsPrec :: Int -> SomeTypeIn uni -> ShowS
showsPrec Int
pr (SomeTypeIn uni (Esc a)
uni) = ($(makeShowsPrec ''SomeTypeIn)) Int
pr (AG uni (Esc a) -> SomeTypeIn (AG uni)
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn (uni (Esc a) -> AG uni (Esc a)
forall {k} (f :: k -> *) (a :: k). f a -> AG f a
AG uni (Esc a)
uni))
instance GShow uni => Show (Kinded uni ta) where
showsPrec :: Int -> Kinded uni ta -> ShowS
showsPrec Int
pr (Kinded uni (Esc a)
uni) = ($(makeShowsPrec ''Kinded)) Int
pr (AG uni (Esc a) -> Kinded (AG uni) (Esc a)
forall k (uni :: * -> *) (a :: k).
Typeable k =>
uni (Esc a) -> Kinded uni (Esc a)
Kinded (uni (Esc a) -> AG uni (Esc a)
forall {k} (f :: k -> *) (a :: k). f a -> AG f a
AG uni (Esc a)
uni))
instance GShow uni => GShow (Kinded uni) where gshowsPrec :: forall a. Int -> Kinded uni a -> ShowS
gshowsPrec = Int -> Kinded uni a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec
instance (GShow uni, Closed uni, uni `Everywhere` Show) => GShow (ValueOf uni) where
gshowsPrec :: forall a. Int -> ValueOf uni a -> ShowS
gshowsPrec = Int -> ValueOf uni a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec
instance (GShow uni, Closed uni, uni `Everywhere` Show) => Show (ValueOf uni a) where
showsPrec :: Int -> ValueOf uni a -> ShowS
showsPrec Int
pr (ValueOf uni (Esc a)
uni a
x) =
Proxy Show -> uni (Esc a) -> (Show a => ShowS) -> ShowS
forall (uni :: * -> *) (constr :: * -> Constraint)
(proxy :: (* -> Constraint) -> *) a r.
(Closed uni, Everywhere uni constr) =>
proxy constr -> uni (Esc a) -> (constr a => r) -> r
forall (constr :: * -> Constraint)
(proxy :: (* -> Constraint) -> *) a r.
Everywhere uni constr =>
proxy constr -> uni (Esc a) -> (constr a => r) -> r
bring (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Show) uni (Esc a)
uni ((Show a => ShowS) -> ShowS) -> (Show a => ShowS) -> ShowS
forall a b. (a -> b) -> a -> b
$ ($(makeShowsPrec ''ValueOf)) Int
pr (AG uni (Esc a) -> a -> ValueOf (AG uni) a
forall (uni :: * -> *) a. uni (Esc a) -> a -> ValueOf uni a
ValueOf (uni (Esc a) -> AG uni (Esc a)
forall {k} (f :: k -> *) (a :: k). f a -> AG f a
AG uni (Esc a)
uni) a
x)
instance (GEq uni, Closed uni, uni `Everywhere` Eq) => GEq (ValueOf uni) where
ValueOf uni (Esc a)
uni1 a
x1 geq :: forall a b. ValueOf uni a -> ValueOf uni b -> Maybe (a :~: b)
`geq` ValueOf uni (Esc b)
uni2 b
x2 = do
Esc a :~: Esc b
Refl <- uni (Esc a)
uni1 uni (Esc a) -> uni (Esc b) -> Maybe (Esc a :~: Esc b)
forall a b. uni a -> uni b -> Maybe (a :~: b)
forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
`geq` uni (Esc b)
uni2
Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Proxy Eq -> uni (Esc a) -> (Eq a => Bool) -> Bool
forall (uni :: * -> *) (constr :: * -> Constraint)
(proxy :: (* -> Constraint) -> *) a r.
(Closed uni, Everywhere uni constr) =>
proxy constr -> uni (Esc a) -> (constr a => r) -> r
forall (constr :: * -> Constraint)
(proxy :: (* -> Constraint) -> *) a r.
Everywhere uni constr =>
proxy constr -> uni (Esc a) -> (constr a => r) -> r
bring (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Eq) uni (Esc a)
uni1 (a
x1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b
x2)
(a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
instance GEq uni => Eq (SomeTypeIn uni) where
SomeTypeIn uni (Esc a)
a1 == :: SomeTypeIn uni -> SomeTypeIn uni -> Bool
== SomeTypeIn uni (Esc a)
a2 = uni (Esc a)
a1 uni (Esc a) -> uni (Esc a) -> Bool
forall {k} (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Bool
`defaultEq` uni (Esc a)
a2
instance (GEq uni, Closed uni, uni `Everywhere` Eq) => Eq (ValueOf uni a) where
== :: ValueOf uni a -> ValueOf uni a -> Bool
(==) = ValueOf uni a -> ValueOf uni a -> Bool
forall {k} (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Bool
defaultEq
instance (GCompare uni, Closed uni, uni `Everywhere` Ord, uni `Everywhere` Eq) =>
GCompare (ValueOf uni) where
ValueOf uni (Esc a)
uni1 a
x1 gcompare :: forall a b. ValueOf uni a -> ValueOf uni b -> GOrdering a b
`gcompare` ValueOf uni (Esc b)
uni2 b
x2 =
case uni (Esc a)
uni1 uni (Esc a) -> uni (Esc b) -> GOrdering (Esc a) (Esc b)
forall a b. uni a -> uni b -> GOrdering a b
forall k (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
`gcompare` uni (Esc b)
uni2 of
GOrdering (Esc a) (Esc b)
GLT -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
GOrdering (Esc a) (Esc b)
GGT -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT
GOrdering (Esc a) (Esc b)
GEQ ->
Proxy Ord
-> uni (Esc a) -> (Ord a => GOrdering a b) -> GOrdering a b
forall (uni :: * -> *) (constr :: * -> Constraint)
(proxy :: (* -> Constraint) -> *) a r.
(Closed uni, Everywhere uni constr) =>
proxy constr -> uni (Esc a) -> (constr a => r) -> r
forall (constr :: * -> Constraint)
(proxy :: (* -> Constraint) -> *) a r.
Everywhere uni constr =>
proxy constr -> uni (Esc a) -> (constr a => r) -> r
bring (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Ord) uni (Esc a)
uni1 ((Ord a => GOrdering a b) -> GOrdering a b)
-> (Ord a => GOrdering a b) -> GOrdering a b
forall a b. (a -> b) -> a -> b
$ case a
x1 a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` a
b
x2 of
Ordering
EQ -> GOrdering a a
GOrdering a b
forall {k} (a :: k). GOrdering a a
GEQ
Ordering
LT -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
Ordering
GT -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT
instance GCompare uni => Ord (SomeTypeIn uni) where
SomeTypeIn uni (Esc a)
a1 compare :: SomeTypeIn uni -> SomeTypeIn uni -> Ordering
`compare` SomeTypeIn uni (Esc a)
a2 = uni (Esc a)
a1 uni (Esc a) -> uni (Esc a) -> Ordering
forall {k} (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> Ordering
`defaultCompare` uni (Esc a)
a2
instance (GCompare uni, Closed uni, uni `Everywhere` Ord, uni `Everywhere` Eq) =>
Ord (ValueOf uni a) where
compare :: ValueOf uni a -> ValueOf uni a -> Ordering
compare = ValueOf uni a -> ValueOf uni a -> Ordering
forall {k} (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> Ordering
defaultCompare
instance (Closed uni, uni `Everywhere` NFData) => GNFData (ValueOf uni) where
grnf :: forall a. ValueOf uni a -> ()
grnf (ValueOf uni (Esc a)
uni a
x) = Proxy NFData -> uni (Esc a) -> (NFData a => ()) -> ()
forall (uni :: * -> *) (constr :: * -> Constraint)
(proxy :: (* -> Constraint) -> *) a r.
(Closed uni, Everywhere uni constr) =>
proxy constr -> uni (Esc a) -> (constr a => r) -> r
forall (constr :: * -> Constraint)
(proxy :: (* -> Constraint) -> *) a r.
Everywhere uni constr =>
proxy constr -> uni (Esc a) -> (constr a => r) -> r
bring (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @NFData) uni (Esc a)
uni ((NFData a => ()) -> ()) -> (NFData a => ()) -> ()
forall a b. (a -> b) -> a -> b
$ a -> ()
forall a. NFData a => a -> ()
rnf a
x
instance Closed uni => NFData (SomeTypeIn uni) where
rnf :: SomeTypeIn uni -> ()
rnf (SomeTypeIn uni (Esc a)
uni) = [Int] -> ()
forall a. NFData a => a -> ()
rnf ([Int] -> ()) -> [Int] -> ()
forall a b. (a -> b) -> a -> b
$ uni (Esc a) -> [Int]
forall a. uni a -> [Int]
forall (uni :: * -> *) a. Closed uni => uni a -> [Int]
encodeUni uni (Esc a)
uni
instance (Closed uni, uni `Everywhere` NFData) => NFData (ValueOf uni a) where
rnf :: ValueOf uni a -> ()
rnf = ValueOf uni a -> ()
forall a. ValueOf uni a -> ()
forall k (f :: k -> *) (a :: k). GNFData f => f a -> ()
grnf
instance (Closed uni, GEq uni) => Hashable (SomeTypeIn uni) where
hashWithSalt :: Int -> SomeTypeIn uni -> Int
hashWithSalt Int
salt (SomeTypeIn uni (Esc a)
uni) = Int -> [Int] -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
salt ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ uni (Esc a) -> [Int]
forall a. uni a -> [Int]
forall (uni :: * -> *) a. Closed uni => uni a -> [Int]
encodeUni uni (Esc a)
uni
instance (Closed uni, GEq uni, uni `Everywhere` Eq, uni `Everywhere` Hashable) =>
Hashable (ValueOf uni a) where
hashWithSalt :: Int -> ValueOf uni a -> Int
hashWithSalt Int
salt (ValueOf uni (Esc a)
uni a
x) =
Proxy Hashable -> uni (Esc a) -> (Hashable a => Int) -> Int
forall (uni :: * -> *) (constr :: * -> Constraint)
(proxy :: (* -> Constraint) -> *) a r.
(Closed uni, Everywhere uni constr) =>
proxy constr -> uni (Esc a) -> (constr a => r) -> r
forall (constr :: * -> Constraint)
(proxy :: (* -> Constraint) -> *) a r.
Everywhere uni constr =>
proxy constr -> uni (Esc a) -> (constr a => r) -> r
bring (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Hashable) uni (Esc a)
uni ((Hashable a => Int) -> Int) -> (Hashable a => Int) -> Int
forall a b. (a -> b) -> a -> b
$ Int -> (SomeTypeIn uni, a) -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
salt (uni (Esc a) -> SomeTypeIn uni
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn uni (Esc a)
uni, a
x)
instance (Closed uni, GEq uni, uni `Everywhere` Eq, uni `Everywhere` Hashable) =>
Hashable (Some (ValueOf uni)) where
hashWithSalt :: Int -> Some (ValueOf uni) -> Int
hashWithSalt Int
salt (Some ValueOf uni a
s) = Int -> ValueOf uni a -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
salt ValueOf uni a
s