{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE NoOverloadedLists #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Spec.HTree.Orphans where

import Data.HTree (HTree (HNode))
import Data.HTree.Existential (EList, ETree, Has (Proves), Some (MkSome), Some2 (MkSome2))
import Data.HTree.Families (Both)
import Data.HTree.List (HList (HCons, HNil))
import Data.Maybe (catMaybes)
import Data.Proxy (Proxy (Proxy))
import Data.Tree (Tree (Node))
import Spec.HTree.Helpers (liftedWith)
import Spec.HTree.TH (discoverInstancesTypeable)
import Test.QuickCheck.Arbitrary (Arbitrary (arbitrary))
import Test.QuickCheck.Gen (Gen, oneof)
import Test.QuickCheck.Instances ()
import Type.Reflection (Typeable, eqTypeRep, typeRep, (:~~:) (HRefl))

embedType :: [Some (Has Typeable Gen)]
embedType = liftedWith $$(discoverInstancesTypeable @Arbitrary) \(Proves (Proxy :: Proxy a)) ->
  MkSome $ Proves $ arbitrary @a

embedArbOrd :: [Some (Has (Both Typeable Ord) Gen)]
embedArbOrd =
  catMaybes $ concat $ liftedWith $$(discoverInstancesTypeable @Ord) \(Proves (Proxy :: Proxy a)) ->
    liftedWith $$(discoverInstancesTypeable @Arbitrary) \(Proves (Proxy :: Proxy b)) ->
      case eqTypeRep (typeRep @a) (typeRep @b) of
        Nothing -> Nothing
        Just HRefl -> Just (MkSome (Proves $ arbitrary @a))

toEList :: [Some x] -> EList x
toEList [] = MkSome2 HNil
toEList (MkSome x : xs) =
  case toEList xs of
    MkSome2 t -> MkSome2 (HCons x t)

toETree :: Tree (Some f) -> ETree f
toETree (Node (MkSome t) []) = MkSome2 (HNode t HNil)
toETree (Node t' (t : ts)) =
  case (toETree t, toETree (Node t' ts)) of
    (MkSome2 ht, MkSome2 (HNode ht' hts)) -> MkSome2 (HNode ht' (HCons ht hts))

instance Applicative f => Arbitrary (EList (Has Typeable f)) where
  arbitrary = toEList <$> arbitrary

instance Applicative f => Arbitrary (ETree (Has Typeable f)) where
  arbitrary = toETree <$> arbitrary

instance Applicative f => Arbitrary (Some (Has Typeable f)) where
  arbitrary = oneof $ liftedWith embedType \(Proves gen :: Has Typeable Gen b) ->
    MkSome . Proves . pure <$> gen

instance {-# OVERLAPPING #-} Applicative f => Arbitrary (Some (Has Typeable (Has Ord f))) where
  arbitrary = oneof $ liftedWith embedArbOrd \(Proves gen :: Has (Both Typeable Ord) Gen b) ->
    MkSome . Proves . Proves . pure <$> gen

instance (forall x. Eq x => Eq (f x), Typeable f) => Eq (Some (Has Typeable (Has Ord f))) where
  MkSome (Proves (Proves x)) == MkSome (Proves (Proves y)) =
    MkSome (Proves @Typeable (Proves @Eq x)) == MkSome (Proves @Typeable (Proves @Eq y))