{-# LANGUAGE UndecidableInstances #-}
module Data.HTree.Existential
(
Some (..)
, Some2 (..)
, ETree
, EList
, with
, with2
, withSomeHTree
, withSomeHList
, hcFoldEHList
, hcFoldMapEHTree
, Has (..)
, HasTypeable
, HasIs
, withProves
, prodHas
, flipHas
)
where
import Data.HTree.Constraint (Has (Proves), HasIs, HasTypeable, proves)
import Data.HTree.Families (Both)
import Data.HTree.List (HList (HCons, HNil))
import Data.HTree.Tree (HTree (HNode))
import Data.Kind (Type)
import Type.Reflection (SomeTypeRep (SomeTypeRep), Typeable, eqTypeRep, typeOf, (:~~:) (HRefl))
type Some :: forall l. (l -> Type) -> Type
data Some g where
MkSome :: g k -> Some g
with :: forall {l} (g :: l -> Type) r. Some g -> (forall m. g m -> r) -> r
with :: forall {l} (g :: l -> Type) r.
Some @l g -> (forall (m :: l). g m -> r) -> r
with (MkSome g k
a) forall (m :: l). g m -> r
f = g k -> r
forall (m :: l). g m -> r
f g k
a
type Some2 :: forall k l. (k -> l -> Type) -> k -> Type
data Some2 g f where
MkSome2 :: g f k -> Some2 g f
with2
:: forall {k} {l} (g :: k -> l -> Type) (f :: k) r
. Some2 g f
-> (forall m. g f m -> r)
-> r
with2 :: forall {k} {l} (g :: k -> l -> Type) (f :: k) r.
Some2 @k @l g f -> (forall (m :: l). g f m -> r) -> r
with2 (MkSome2 g f k
a) forall (m :: l). g f m -> r
f = g f k -> r
forall (m :: l). g f m -> r
f g f k
a
type ETree :: forall k. (k -> Type) -> Type
type ETree = Some2 HTree
type EList :: forall k. (k -> Type) -> Type
type EList = Some2 HList
withSomeHTree :: ETree f -> (forall t. HTree f t -> r) -> r
withSomeHTree :: forall {k} (f :: k -> Type) r.
ETree @k f
-> (forall (t :: TyTree @Type k). HTree @k f t -> r) -> r
withSomeHTree = Some2 @(k -> Type) @(TyTree @Type k) (HTree @k) f
-> (forall (m :: TyTree @Type k). HTree @k f m -> r) -> r
forall {k} {l} (g :: k -> l -> Type) (f :: k) r.
Some2 @k @l g f -> (forall (m :: l). g f m -> r) -> r
with2
withSomeHList :: EList f -> (forall xs. HList f xs -> r) -> r
withSomeHList :: forall {k} (f :: k -> Type) r.
EList @k f -> (forall (xs :: [k]). HList @k f xs -> r) -> r
withSomeHList = Some2 @(k -> Type) @[k] (HList @k) f
-> (forall (m :: [k]). HList @k f m -> r) -> r
forall {k} {l} (g :: k -> l -> Type) (f :: k) r.
Some2 @k @l g f -> (forall (m :: l). g f m -> r) -> r
with2
hcFoldEHList
:: forall c f y
. (forall x. c x => f x -> y -> y)
-> y
-> EList (Has c f)
-> y
hcFoldEHList :: forall {k} (c :: k -> Constraint) (f :: k -> Type) y.
(forall (x :: k). c x => f x -> y -> y)
-> y -> EList @k (Has @k c f) -> y
hcFoldEHList forall (x :: k). c x => f x -> y -> y
f y
def EList @k (Has @k c f)
el = EList @k (Has @k c f)
-> (forall (m :: [k]). HList @k (Has @k c f) m -> y) -> y
forall {k} {l} (g :: k -> l -> Type) (f :: k) r.
Some2 @k @l g f -> (forall (m :: l). g f m -> r) -> r
with2 EList @k (Has @k c f)
el \case
HList @k (Has @k c f) m
HNil -> y
def
HCons (Proves f x
x) HList @k (Has @k c f) xs
xs ->
let y :: y
y = (forall (x :: k). c x => f x -> y -> y)
-> y -> EList @k (Has @k c f) -> y
forall {k} (c :: k -> Constraint) (f :: k -> Type) y.
(forall (x :: k). c x => f x -> y -> y)
-> y -> EList @k (Has @k c f) -> y
hcFoldEHList f x -> y -> y
forall (x :: k). c x => f x -> y -> y
f y
def (HList @k (Has @k c f) xs -> EList @k (Has @k c f)
forall {k} {l} (g :: k -> l -> Type) (f :: k) (k :: l).
g f k -> Some2 @k @l g f
MkSome2 HList @k (Has @k c f) xs
xs)
in f x -> y -> y
forall (x :: k). c x => f x -> y -> y
f f x
x y
y
hcFoldMapEHTree
:: forall c f y
. Semigroup y
=> (forall a. c a => f a -> y)
-> ETree (Has c f)
-> y
hcFoldMapEHTree :: forall {k} (c :: k -> Constraint) (f :: k -> Type) y.
Semigroup y =>
(forall (a :: k). c a => f a -> y) -> ETree @k (Has @k c f) -> y
hcFoldMapEHTree forall (a :: k). c a => f a -> y
f ETree @k (Has @k c f)
et = ETree @k (Has @k c f)
-> (forall (m :: TyTree @Type k). HTree @k (Has @k c f) m -> y)
-> y
forall {k} {l} (g :: k -> l -> Type) (f :: k) r.
Some2 @k @l g f -> (forall (m :: l). g f m -> r) -> r
with2 ETree @k (Has @k c f)
et \case
HNode (Proves f a
x) HList @(TyTree @Type k) (HTree @k (Has @k c f)) ts
HNil -> f a -> y
forall (a :: k). c a => f a -> y
f f a
x
HNode x :: Has @k c f a
x@(Proves f a
_) (HTree @k (Has @k c f) x
y `HCons` HList @(TyTree @Type k) (HTree @k (Has @k c f)) xs
ys) ->
(forall (a :: k). c a => f a -> y) -> ETree @k (Has @k c f) -> y
forall {k} (c :: k -> Constraint) (f :: k -> Type) y.
Semigroup y =>
(forall (a :: k). c a => f a -> y) -> ETree @k (Has @k c f) -> y
hcFoldMapEHTree f a -> y
forall (a :: k). c a => f a -> y
f (HTree @k (Has @k c f) x -> ETree @k (Has @k c f)
forall {k} {l} (g :: k -> l -> Type) (f :: k) (k :: l).
g f k -> Some2 @k @l g f
MkSome2 HTree @k (Has @k c f) x
y)
y -> y -> y
forall a. Semigroup a => a -> a -> a
<> (forall (a :: k). c a => f a -> y) -> ETree @k (Has @k c f) -> y
forall {k} (c :: k -> Constraint) (f :: k -> Type) y.
Semigroup y =>
(forall (a :: k). c a => f a -> y) -> ETree @k (Has @k c f) -> y
hcFoldMapEHTree f a -> y
forall (a :: k). c a => f a -> y
f (HTree @k (Has @k c f) ('TyNode @k a xs) -> ETree @k (Has @k c f)
forall {k} {l} (g :: k -> l -> Type) (f :: k) (k :: l).
g f k -> Some2 @k @l g f
MkSome2 (Has @k c f a
-> HList @(TyTree @Type k) (HTree @k (Has @k c f)) xs
-> HTree @k (Has @k c f) ('TyNode @k a xs)
forall {k} (f :: k -> Type) (a :: k) (ts :: TyForest @Type k).
f a -> HForest @k f ts -> HTree @k f ('TyNode @k a ts)
HNode Has @k c f a
x HList @(TyTree @Type k) (HTree @k (Has @k c f)) xs
ys))
withProves :: Some (Has c f) -> (forall a. c a => f a -> r) -> r
withProves :: forall {l} (c :: l -> Constraint) (f :: l -> Type) r.
Some @l (Has @l c f) -> (forall (a :: l). c a => f a -> r) -> r
withProves Some @l (Has @l c f)
x forall (a :: l). c a => f a -> r
k = Some @l (Has @l c f) -> (forall (m :: l). Has @l c f m -> r) -> r
forall {l} (g :: l -> Type) r.
Some @l g -> (forall (m :: l). g m -> r) -> r
with Some @l (Has @l c f)
x (Has @l c f m -> (c m => f m -> r) -> r
forall {k} (c :: k -> Constraint) (f :: k -> Type) (a :: k) r.
Has @k c f a -> (c a => f a -> r) -> r
`proves` c m => f m -> r
f m -> r
forall (a :: l). c a => f a -> r
k)
prodHas :: forall c1 c2 f. Some (Has c1 (Has c2 f)) -> Some (Has (Both c1 c2) f)
prodHas :: forall {l} (c1 :: l -> Constraint) (c2 :: l -> Constraint)
(f :: l -> Type).
Some @l (Has @l c1 (Has @l c2 f))
-> Some @l (Has @l (Both @l c1 c2) f)
prodHas Some @l (Has @l c1 (Has @l c2 f))
x = Some @l (Has @l c1 (Has @l c2 f))
-> (forall (a :: l).
c1 a =>
Has @l c2 f a -> Some @l (Has @l (Both @l c1 c2) f))
-> Some @l (Has @l (Both @l c1 c2) f)
forall {l} (c :: l -> Constraint) (f :: l -> Type) r.
Some @l (Has @l c f) -> (forall (a :: l). c a => f a -> r) -> r
withProves Some @l (Has @l c1 (Has @l c2 f))
x \Has @l c2 f a
pc2 -> Has @l c2 f a
-> (c2 a => f a -> Some @l (Has @l (Both @l c1 c2) f))
-> Some @l (Has @l (Both @l c1 c2) f)
forall {k} (c :: k -> Constraint) (f :: k -> Type) (a :: k) r.
Has @k c f a -> (c a => f a -> r) -> r
proves Has @l c2 f a
pc2 (Has @l (Both @l c1 c2) f a -> Some @l (Has @l (Both @l c1 c2) f)
forall {l} (g :: l -> Type) (k :: l). g k -> Some @l g
MkSome (Has @l (Both @l c1 c2) f a -> Some @l (Has @l (Both @l c1 c2) f))
-> (f a -> Has @l (Both @l c1 c2) f a)
-> f a
-> Some @l (Has @l (Both @l c1 c2) f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> Has @l (Both @l c1 c2) f a
forall {k} (c :: k -> Constraint) (k1 :: k) (f :: k -> Type).
c k1 =>
f k1 -> Has @k c f k1
Proves)
flipHas :: forall c1 c2 f. Some (Has c1 (Has c2 f)) -> Some (Has c2 (Has c1 f))
flipHas :: forall {l} (c1 :: l -> Constraint) (c2 :: l -> Constraint)
(f :: l -> Type).
Some @l (Has @l c1 (Has @l c2 f))
-> Some @l (Has @l c2 (Has @l c1 f))
flipHas Some @l (Has @l c1 (Has @l c2 f))
x = Some @l (Has @l (Both @l c1 c2) f)
-> (forall (a :: l).
Both @l c1 c2 a =>
f a -> Some @l (Has @l c2 (Has @l c1 f)))
-> Some @l (Has @l c2 (Has @l c1 f))
forall {l} (c :: l -> Constraint) (f :: l -> Type) r.
Some @l (Has @l c f) -> (forall (a :: l). c a => f a -> r) -> r
withProves (Some @l (Has @l c1 (Has @l c2 f))
-> Some @l (Has @l (Both @l c1 c2) f)
forall {l} (c1 :: l -> Constraint) (c2 :: l -> Constraint)
(f :: l -> Type).
Some @l (Has @l c1 (Has @l c2 f))
-> Some @l (Has @l (Both @l c1 c2) f)
prodHas Some @l (Has @l c1 (Has @l c2 f))
x) (Has @l c2 (Has @l c1 f) a -> Some @l (Has @l c2 (Has @l c1 f))
forall {l} (g :: l -> Type) (k :: l). g k -> Some @l g
MkSome (Has @l c2 (Has @l c1 f) a -> Some @l (Has @l c2 (Has @l c1 f)))
-> (f a -> Has @l c2 (Has @l c1 f) a)
-> f a
-> Some @l (Has @l c2 (Has @l c1 f))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Has @l c1 f a -> Has @l c2 (Has @l c1 f) a
forall {k} (c :: k -> Constraint) (k1 :: k) (f :: k -> Type).
c k1 =>
f k1 -> Has @k c f k1
Proves (Has @l c1 f a -> Has @l c2 (Has @l c1 f) a)
-> (f a -> Has @l c1 f a) -> f a -> Has @l c2 (Has @l c1 f) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> Has @l c1 f a
forall {k} (c :: k -> Constraint) (k1 :: k) (f :: k -> Type).
c k1 =>
f k1 -> Has @k c f k1
Proves)
deriving stock instance (forall k. Show (g f k)) => Show (Some2 g f)
deriving stock instance (forall k. Show (g k)) => Show (Some g)
instance {-# OVERLAPPING #-} Typeable f => Show (Some (Has Typeable f)) where
show :: Some @l (Has @l (Typeable @l) f) -> String
show (MkSome (Proves f k
f)) =
String
"(MkSome (Proves @Typeable " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> TypeRep @Type (f k) -> String
forall a. Show a => a -> String
show (f k -> TypeRep @Type (f k)
forall a. Typeable @Type a => a -> TypeRep @Type a
typeOf f k
f) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"))"
instance
(forall x. Eq x => Eq (f x), Typeable f)
=> Eq (ETree (Has (Both Typeable Eq) f))
where
ETree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f)
ex == :: ETree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f)
-> ETree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f)
-> Bool
== ETree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f)
ey =
ETree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f)
-> (forall (m :: TyTree @Type Type).
HTree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) m
-> Bool)
-> Bool
forall {k} {l} (g :: k -> l -> Type) (f :: k) r.
Some2 @k @l g f -> (forall (m :: l). g f m -> r) -> r
with2 ETree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f)
ex \HTree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) m
x -> ETree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f)
-> (forall (m :: TyTree @Type Type).
HTree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) m
-> Bool)
-> Bool
forall {k} {l} (g :: k -> l -> Type) (f :: k) r.
Some2 @k @l g f -> (forall (m :: l). g f m -> r) -> r
with2 ETree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f)
ey \HTree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) m
y ->
case (HTree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) m
x, HTree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) m
y) of
(HNode (Proves f a
m) HForest @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) ts
ms, HNode (Proves f a
n) HForest @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) ts
ns) ->
case TypeRep @Type (f a)
-> TypeRep @Type (f a) -> Maybe ((:~~:) @Type @Type (f a) (f a))
forall k1 k2 (a :: k1) (b :: k2).
TypeRep @k1 a -> TypeRep @k2 b -> Maybe ((:~~:) @k1 @k2 a b)
eqTypeRep (f a -> TypeRep @Type (f a)
forall a. Typeable @Type a => a -> TypeRep @Type a
typeOf f a
m) (f a -> TypeRep @Type (f a)
forall a. Typeable @Type a => a -> TypeRep @Type a
typeOf f a
n) of
Maybe ((:~~:) @Type @Type (f a) (f a))
Nothing -> Bool
False
Just (:~~:) @Type @Type (f a) (f a)
HRefl ->
let go
:: forall xs ys
. HList (HTree (Has (Both Typeable Eq) f)) xs
-> HList (HTree (Has (Both Typeable Eq) f)) ys
-> Bool
go :: forall (xs :: [TyTree @Type Type]) (ys :: [TyTree @Type Type]).
HList
@(TyTree @Type Type)
(HTree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f))
xs
-> HList
@(TyTree @Type Type)
(HTree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f))
ys
-> Bool
go HList
@(TyTree @Type Type)
(HTree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f))
xs
HNil HList
@(TyTree @Type Type)
(HTree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f))
ys
HNil = Bool
True
go (HTree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) x
m' `HCons` HList
@(TyTree @Type Type)
(HTree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f))
xs
ms') (HTree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) x
n' `HCons` HList
@(TyTree @Type Type)
(HTree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f))
xs
ns') =
HTree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) x
-> ETree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f)
forall {k} {l} (g :: k -> l -> Type) (f :: k) (k :: l).
g f k -> Some2 @k @l g f
MkSome2 HTree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) x
m' ETree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f)
-> ETree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f)
-> Bool
forall a. Eq a => a -> a -> Bool
== HTree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) x
-> ETree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f)
forall {k} {l} (g :: k -> l -> Type) (f :: k) (k :: l).
g f k -> Some2 @k @l g f
MkSome2 HTree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) x
n' Bool -> Bool -> Bool
&& HList
@(TyTree @Type Type)
(HTree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f))
xs
-> HList
@(TyTree @Type Type)
(HTree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f))
xs
-> Bool
forall (xs :: [TyTree @Type Type]) (ys :: [TyTree @Type Type]).
HList
@(TyTree @Type Type)
(HTree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f))
xs
-> HList
@(TyTree @Type Type)
(HTree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f))
ys
-> Bool
go HList
@(TyTree @Type Type)
(HTree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f))
xs
ms' HList
@(TyTree @Type Type)
(HTree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f))
xs
ns'
go HList
@(TyTree @Type Type)
(HTree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f))
xs
_ HList
@(TyTree @Type Type)
(HTree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f))
ys
_ = Bool
False
in f a
m f a -> f a -> Bool
forall a. Eq a => a -> a -> Bool
== f a
f a
n Bool -> Bool -> Bool
&& HForest @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) ts
-> HForest @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) ts
-> Bool
forall (xs :: [TyTree @Type Type]) (ys :: [TyTree @Type Type]).
HList
@(TyTree @Type Type)
(HTree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f))
xs
-> HList
@(TyTree @Type Type)
(HTree @Type (Has @Type (Both @Type (Typeable @Type) Eq) f))
ys
-> Bool
go HForest @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) ts
ms HForest @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) ts
ns
instance
(forall x. Eq x => Eq (f x), Typeable f)
=> Eq (EList (Has (Both Typeable Eq) f))
where
EList @Type (Has @Type (Both @Type (Typeable @Type) Eq) f)
ex == :: EList @Type (Has @Type (Both @Type (Typeable @Type) Eq) f)
-> EList @Type (Has @Type (Both @Type (Typeable @Type) Eq) f)
-> Bool
== EList @Type (Has @Type (Both @Type (Typeable @Type) Eq) f)
ey =
EList @Type (Has @Type (Both @Type (Typeable @Type) Eq) f)
-> (forall (m :: [Type]).
HList @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) m
-> Bool)
-> Bool
forall {k} {l} (g :: k -> l -> Type) (f :: k) r.
Some2 @k @l g f -> (forall (m :: l). g f m -> r) -> r
with2 EList @Type (Has @Type (Both @Type (Typeable @Type) Eq) f)
ex \HList @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) m
x -> EList @Type (Has @Type (Both @Type (Typeable @Type) Eq) f)
-> (forall (m :: [Type]).
HList @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) m
-> Bool)
-> Bool
forall {k} {l} (g :: k -> l -> Type) (f :: k) r.
Some2 @k @l g f -> (forall (m :: l). g f m -> r) -> r
with2 EList @Type (Has @Type (Both @Type (Typeable @Type) Eq) f)
ey \HList @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) m
y ->
case (HList @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) m
x, HList @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) m
y) of
(HList @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) m
HNil, HList @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) m
HNil) -> Bool
True
(HCons (Proves f x
x') HList @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) xs
xs', HCons (Proves f x
y') HList @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) xs
ys') ->
case TypeRep @Type (f x)
-> TypeRep @Type (f x) -> Maybe ((:~~:) @Type @Type (f x) (f x))
forall k1 k2 (a :: k1) (b :: k2).
TypeRep @k1 a -> TypeRep @k2 b -> Maybe ((:~~:) @k1 @k2 a b)
eqTypeRep (f x -> TypeRep @Type (f x)
forall a. Typeable @Type a => a -> TypeRep @Type a
typeOf f x
x') (f x -> TypeRep @Type (f x)
forall a. Typeable @Type a => a -> TypeRep @Type a
typeOf f x
y') of
Maybe ((:~~:) @Type @Type (f x) (f x))
Nothing -> Bool
False
Just (:~~:) @Type @Type (f x) (f x)
HRefl -> f x
x' f x -> f x -> Bool
forall a. Eq a => a -> a -> Bool
== f x
f x
y' Bool -> Bool -> Bool
&& HList @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) xs
-> EList @Type (Has @Type (Both @Type (Typeable @Type) Eq) f)
forall {k} {l} (g :: k -> l -> Type) (f :: k) (k :: l).
g f k -> Some2 @k @l g f
MkSome2 HList @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) xs
xs' EList @Type (Has @Type (Both @Type (Typeable @Type) Eq) f)
-> EList @Type (Has @Type (Both @Type (Typeable @Type) Eq) f)
-> Bool
forall a. Eq a => a -> a -> Bool
== HList @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) xs
-> EList @Type (Has @Type (Both @Type (Typeable @Type) Eq) f)
forall {k} {l} (g :: k -> l -> Type) (f :: k) (k :: l).
g f k -> Some2 @k @l g f
MkSome2 HList @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) xs
ys'
(HList @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) m
_, HList @Type (Has @Type (Both @Type (Typeable @Type) Eq) f) m
_) -> Bool
False
instance Eq (f k) => Eq (EList (HasIs k f)) where
EList @k (HasIs @k k f)
ex == :: EList @k (HasIs @k k f) -> EList @k (HasIs @k k f) -> Bool
== EList @k (HasIs @k k f)
ey =
EList @k (HasIs @k k f)
-> (forall (m :: [k]). HList @k (HasIs @k k f) m -> Bool) -> Bool
forall {k} {l} (g :: k -> l -> Type) (f :: k) r.
Some2 @k @l g f -> (forall (m :: l). g f m -> r) -> r
with2 EList @k (HasIs @k k f)
ex \HList @k (HasIs @k k f) m
x -> EList @k (HasIs @k k f)
-> (forall (m :: [k]). HList @k (HasIs @k k f) m -> Bool) -> Bool
forall {k} {l} (g :: k -> l -> Type) (f :: k) r.
Some2 @k @l g f -> (forall (m :: l). g f m -> r) -> r
with2 EList @k (HasIs @k k f)
ey \HList @k (HasIs @k k f) m
y ->
case (HList @k (HasIs @k k f) m
x, HList @k (HasIs @k k f) m
y) of
(HList @k (HasIs @k k f) m
HNil, HList @k (HasIs @k k f) m
HNil) -> Bool
True
(HCons (Proves f x
x') HList @k (HasIs @k k f) xs
xs', HCons (Proves f x
y') HList @k (HasIs @k k f) xs
ys') ->
(f x
x' f x -> f x -> Bool
forall a. Eq a => a -> a -> Bool
== f x
f x
y') Bool -> Bool -> Bool
&& HList @k (HasIs @k k f) xs -> EList @k (HasIs @k k f)
forall {k} {l} (g :: k -> l -> Type) (f :: k) (k :: l).
g f k -> Some2 @k @l g f
MkSome2 HList @k (HasIs @k k f) xs
xs' EList @k (HasIs @k k f) -> EList @k (HasIs @k k f) -> Bool
forall a. Eq a => a -> a -> Bool
== HList @k (HasIs @k k f) xs -> EList @k (HasIs @k k f)
forall {k} {l} (g :: k -> l -> Type) (f :: k) (k :: l).
g f k -> Some2 @k @l g f
MkSome2 HList @k (HasIs @k k f) xs
ys'
(HList @k (HasIs @k k f) m
_, HList @k (HasIs @k k f) m
_) -> Bool
False
instance
( forall x. Eq x => Eq (f x)
, Typeable f
)
=> Eq (Some (Has Typeable (Has Eq f)))
where
MkSome (Proves (Proves f k
x1)) == :: Some @Type (Has @Type (Typeable @Type) (Has @Type Eq f))
-> Some @Type (Has @Type (Typeable @Type) (Has @Type Eq f)) -> Bool
== MkSome (Proves (Proves f k
x2)) =
case TypeRep @Type (f k)
-> TypeRep @Type (f k) -> Maybe ((:~~:) @Type @Type (f k) (f k))
forall k1 k2 (a :: k1) (b :: k2).
TypeRep @k1 a -> TypeRep @k2 b -> Maybe ((:~~:) @k1 @k2 a b)
eqTypeRep (f k -> TypeRep @Type (f k)
forall a. Typeable @Type a => a -> TypeRep @Type a
typeOf f k
x1) (f k -> TypeRep @Type (f k)
forall a. Typeable @Type a => a -> TypeRep @Type a
typeOf f k
x2) of
Just (:~~:) @Type @Type (f k) (f k)
HRefl -> f k
x1 f k -> f k -> Bool
forall a. Eq a => a -> a -> Bool
== f k
f k
x2
Maybe ((:~~:) @Type @Type (f k) (f k))
Nothing -> Bool
False
instance
( forall x. Ord x => Ord (f x)
, Typeable f
, Eq (Some (Has Typeable (Has Ord f)))
)
=> Ord (Some (Has Typeable (Has Ord f)))
where
MkSome (Proves (Proves f k
x1)) compare :: Some @Type (Has @Type (Typeable @Type) (Has @Type Ord f))
-> Some @Type (Has @Type (Typeable @Type) (Has @Type Ord f))
-> Ordering
`compare` MkSome (Proves (Proves f k
x2)) =
case TypeRep @Type (f k)
-> TypeRep @Type (f k) -> Maybe ((:~~:) @Type @Type (f k) (f k))
forall k1 k2 (a :: k1) (b :: k2).
TypeRep @k1 a -> TypeRep @k2 b -> Maybe ((:~~:) @k1 @k2 a b)
eqTypeRep (f k -> TypeRep @Type (f k)
forall a. Typeable @Type a => a -> TypeRep @Type a
typeOf f k
x1) (f k -> TypeRep @Type (f k)
forall a. Typeable @Type a => a -> TypeRep @Type a
typeOf f k
x2) of
Just (:~~:) @Type @Type (f k) (f k)
HRefl -> f k
x1 f k -> f k -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` f k
f k
x2
Maybe ((:~~:) @Type @Type (f k) (f k))
Nothing -> TypeRep @Type (f k) -> SomeTypeRep
forall k (a :: k). TypeRep @k a -> SomeTypeRep
SomeTypeRep (f k -> TypeRep @Type (f k)
forall a. Typeable @Type a => a -> TypeRep @Type a
typeOf f k
x1) SomeTypeRep -> SomeTypeRep -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` TypeRep @Type (f k) -> SomeTypeRep
forall k (a :: k). TypeRep @k a -> SomeTypeRep
SomeTypeRep (f k -> TypeRep @Type (f k)
forall a. Typeable @Type a => a -> TypeRep @Type a
typeOf f k
x2)