{-# LANGUAGE UndecidableInstances #-}

-- | Existential types and helpers to work with existentials 'HList's and 'HTree's
module Data.HTree.Existential
  ( -- * existential data types
    Some (..)
  , Some2 (..)

    -- * existential type synonyms
  , ETree
  , EList

    -- * working with existential HTrees/HLists functions
  , with
  , with2
  , withSomeHTree
  , withSomeHList
  , hcFoldEHList
  , hcFoldMapEHTree

    -- * useful functors to work with existential type-level structures
  , Has (..)
  , HasTypeable
  , HasIs

    -- ** working with 'Has'
  , 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))

-- | a Some type that takes an arity one type constructor, this is for completeness
type Some :: forall l. (l -> Type) -> Type
data Some g where
  MkSome :: g k -> Some g

-- | take some existentai arity one type constructor and a function that takes the
--   non-existential one and returns some `r` and return an `r`
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

-- | a Some type that take an arity two type constructor, this is necessary
--   so that we avoid using composition on the type level or having visible
--   parameters to the type synonyms
type Some2 :: forall k l. (k -> l -> Type) -> k -> Type
data Some2 g f where
  MkSome2 :: g f k -> Some2 g f

-- | take some existential arity two type constructor and a function that takes the
--   non-existential one and returns some `r` and return an `r`
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

-- | HTree but the type level tree is existential
type ETree :: forall k. (k -> Type) -> Type
type ETree = Some2 HTree

-- | HList but the type level list is existential
type EList :: forall k. (k -> Type) -> Type
type EList = Some2 HList

-- | 'with2' specialized to 'HTree's
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

-- | 'with2' specialized to 'HList's
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

-- | fold over existential hlists
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

-- | fold over existential htrees
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))

-- | destruct 'Some', destruct 'Has'
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)

-- | condens the 'Has' constraints in an existential
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)

-- | flip the constraints in an existential
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)