{-# 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 (MkSome a) f = f 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 (MkSome2 a) f = f 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 = with2

-- | 'with2' specialized to 'HList's
withSomeHList :: EList f -> (forall xs. HList f xs -> r) -> r
withSomeHList = 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 f def el = with2 el \case
  HNil -> def
  HCons (Proves x) xs ->
    let y = hcFoldEHList f def (MkSome2 xs)
     in f x 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 f et = with2 et \case
  HNode (Proves x) HNil -> f x
  HNode x@(Proves _) (y `HCons` ys) ->
    hcFoldMapEHTree f (MkSome2 y)
      <> hcFoldMapEHTree f (MkSome2 (HNode x ys))

-- | destruct 'Some', destruct 'Has'
withProves :: Some (Has c f) -> (forall a. c a => f a -> r) -> r
withProves x k = with x (`proves` 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 x = withProves x \pc2 -> proves pc2 (MkSome . 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 x = withProves (prodHas x) (MkSome . Proves . 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 (MkSome (Proves f)) =
    "(MkSome (Proves @Typeable " <> show (typeOf f) <> "))"

instance
  (forall x. Eq x => Eq (f x), Typeable f)
  => Eq (ETree (Has (Both Typeable Eq) f))
  where
  ex == ey =
    with2 ex \x -> with2 ey \y ->
      case (x, y) of
        (HNode (Proves m) ms, HNode (Proves n) ns) ->
          case eqTypeRep (typeOf m) (typeOf n) of
            Nothing -> False
            Just HRefl ->
              let go
                    :: forall xs ys
                     . HList (HTree (Has (Both Typeable Eq) f)) xs
                    -> HList (HTree (Has (Both Typeable Eq) f)) ys
                    -> Bool
                  go HNil HNil = True
                  go (m' `HCons` ms') (n' `HCons` ns') =
                    MkSome2 m' == MkSome2 n' && go ms' ns'
                  go _ _ = False
               in m == n && go ms ns

instance
  (forall x. Eq x => Eq (f x), Typeable f)
  => Eq (EList (Has (Both Typeable Eq) f))
  where
  ex == ey =
    with2 ex \x -> with2 ey \y ->
      case (x, y) of
        (HNil, HNil) -> True
        (HCons (Proves x') xs', HCons (Proves y') ys') ->
          case eqTypeRep (typeOf x') (typeOf y') of
            Nothing -> False
            Just HRefl -> x' == y' && MkSome2 xs' == MkSome2 ys'
        (_, _) -> False

instance Eq (f k) => Eq (EList (HasIs k f)) where
  ex == ey =
    with2 ex \x -> with2 ey \y ->
      case (x, y) of
        (HNil, HNil) -> True
        (HCons (Proves x') xs', HCons (Proves y') ys') ->
          (x' == y') && MkSome2 xs' == MkSome2 ys'
        (_, _) -> False

instance
  ( forall x. Eq x => Eq (f x)
  , Typeable f
  )
  => Eq (Some (Has Typeable (Has Eq f)))
  where
  MkSome (Proves (Proves x1)) == MkSome (Proves (Proves x2)) =
    case eqTypeRep (typeOf x1) (typeOf x2) of
      Just HRefl -> x1 == x2
      Nothing -> 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 x1)) `compare` MkSome (Proves (Proves x2)) =
    case eqTypeRep (typeOf x1) (typeOf x2) of
      Just HRefl -> x1 `compare` x2
      Nothing -> SomeTypeRep (typeOf x1) `compare` SomeTypeRep (typeOf x2)