module Data.OpenUnion.Extra
  ( (@@>),
    TryLiftUnion (..),
    pattern SingletonUnion,
  )
where

import Control.Applicative
import Data.Dynamic
import Data.OpenUnion.Internal
import Data.Typeable
import TypeFun.Data.List hiding (Union)

class TryLiftUnion xs where
  tryLiftUnion :: (Alternative m, Typeable x) => x -> m (Union xs)

instance TryLiftUnion '[] where
  tryLiftUnion :: x -> m (Union '[])
tryLiftUnion x
_ = m (Union '[])
forall (f :: * -> *) a. Alternative f => f a
empty

instance
  (Typeable y, SubList ys (y : ys), TryLiftUnion ys) =>
  TryLiftUnion (y ': ys)
  where
  tryLiftUnion :: x -> m (Union (y : ys))
tryLiftUnion (x
x :: x) = case (Typeable x, Typeable y) => Maybe (x :~: y)
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @x @y of
    Maybe (x :~: y)
Nothing -> Union ys -> Union (y : ys)
forall (s :: [*]) (s' :: [*]). SubList s s' => Union s -> Union s'
reUnion (Union ys -> Union (y : ys)) -> m (Union ys) -> m (Union (y : ys))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> x -> m (Union ys)
forall (xs :: [*]) (m :: * -> *) x.
(TryLiftUnion xs, Alternative m, Typeable x) =>
x -> m (Union xs)
tryLiftUnion @ys x
x
    Just x :~: y
Refl -> Union (y : ys) -> m (Union (y : ys))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Union (y : ys) -> m (Union (y : ys)))
-> Union (y : ys) -> m (Union (y : ys))
forall a b. (a -> b) -> a -> b
$ x -> Union (y : ys)
forall a (s :: [*]). (Typeable a, Elem a s) => a -> Union s
liftUnion x
x

-- | Like '@>', but enforces a specific type list order.
-- (Useful for deconstruction-directed type inference.)
(@@>) :: Typeable a => (a -> b) -> (Union xs -> b) -> Union (a ': xs) -> b
a -> b
r @@> :: (a -> b) -> (Union xs -> b) -> Union (a : xs) -> b
@@> Union xs -> b
l = (Union xs -> b) -> (a -> b) -> Either (Union xs) a -> b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Union xs -> b
l a -> b
r (Either (Union xs) a -> b)
-> (Union (a : xs) -> Either (Union xs) a) -> Union (a : xs) -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Union (a : xs) -> Either (Union xs) a
forall a (aa :: [*]).
Typeable a =>
Union (a : aa) -> Either (Union aa) a
restrict'
  where
    restrict' :: Typeable a => Union (a ': aa) -> Either (Union aa) a
    restrict' :: Union (a : aa) -> Either (Union aa) a
restrict' (Union Dynamic
d) = Either (Union aa) a
-> (a -> Either (Union aa) a) -> Maybe a -> Either (Union aa) a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Union aa -> Either (Union aa) a
forall a b. a -> Either a b
Left (Union aa -> Either (Union aa) a)
-> Union aa -> Either (Union aa) a
forall a b. (a -> b) -> a -> b
$ Dynamic -> Union aa
forall (s :: [*]). Dynamic -> Union s
Union Dynamic
d) a -> Either (Union aa) a
forall a b. b -> Either a b
Right (Maybe a -> Either (Union aa) a) -> Maybe a -> Either (Union aa) a
forall a b. (a -> b) -> a -> b
$ Dynamic -> Maybe a
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
d
{-# INLINE (@@>) #-}

infixr 2 @@>

pattern SingletonUnion :: (Typeable a, Elem a s) => a -> Union s
pattern $bSingletonUnion :: a -> Union s
$mSingletonUnion :: forall r a (s :: [*]).
(Typeable a, Elem a s) =>
Union s -> (a -> r) -> (Void# -> r) -> r
SingletonUnion x <-
  ((\(Union y) -> fromDynamic y) -> Just x)
  where
    SingletonUnion a
x = a -> Union s
forall a (s :: [*]). (Typeable a, Elem a s) => a -> Union s
liftUnion a
x