module Data.Type.Witness.Specific.Some where

import Data.Type.Witness.General.AllConstraint
import Data.Type.Witness.General.Order
import Data.Type.Witness.General.WitnessConstraint
import Import

-- | Any value with a witness to a parameter of its type.
type SomeFor :: forall k. (k -> Type) -> (k -> Type) -> Type
type role SomeFor representational representational
data SomeFor f w =
    forall a. MkSomeFor (w a)
                        (f a)

mapSome ::
       forall k (g :: k -> Type) (w1 :: k -> Type) (w2 :: k -> Type).
       (forall t. w1 t -> w2 t)
    -> SomeFor g w1
    -> SomeFor g w2
mapSome :: forall k (g :: k -> Type) (w1 :: k -> Type) (w2 :: k -> Type).
(forall (t :: k). w1 t -> w2 t) -> SomeFor g w1 -> SomeFor g w2
mapSome forall (t :: k). w1 t -> w2 t
f (MkSomeFor w1 a
wt g a
gt) = w2 a -> g a -> SomeFor g w2
forall k (f :: k -> Type) (w :: k -> Type) (a :: k).
w a -> f a -> SomeFor f w
MkSomeFor (w1 a -> w2 a
forall (t :: k). w1 t -> w2 t
f w1 a
wt) g a
gt

matchSomeFor :: TestEquality w => w a -> SomeFor f w -> Maybe (f a)
matchSomeFor :: forall {k} (w :: k -> Type) (a :: k) (f :: k -> Type).
TestEquality w =>
w a -> SomeFor f w -> Maybe (f a)
matchSomeFor w a
wit (MkSomeFor w a
cwit f a
cfa) = do
    a :~: a
Refl <- w a -> w a -> Maybe (a :~: a)
forall (a :: k) (b :: k). w a -> w b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality w a
cwit w a
wit
    f a -> Maybe (f a)
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return f a
f a
cfa

type SomeOf :: (Type -> Type) -> Type
type SomeOf = SomeFor Identity

pattern MkSomeOf :: w a -> a -> SomeOf w

pattern $mMkSomeOf :: forall {r} {w :: Type -> Type}.
SomeOf w -> (forall {a}. w a -> a -> r) -> ((# #) -> r) -> r
$bMkSomeOf :: forall (w :: Type -> Type) a. w a -> a -> SomeOf w
MkSomeOf wa a = MkSomeFor wa (Identity a)

{-# COMPLETE MkSomeOf #-}

instance (TestEquality w, WitnessConstraint Eq w) => Eq (SomeOf w) where
    MkSomeOf w a
wa a
a == :: SomeOf w -> SomeOf w -> Bool
== MkSomeOf w a
wb a
b =
        case w a -> w a -> Maybe (a :~: a)
forall a b. w a -> w b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality w a
wa w a
wb of
            Maybe (a :~: a)
Nothing -> Bool
False
            Just a :~: a
Refl ->
                case forall k (c :: k -> Constraint) (w :: k -> Type) (t :: k).
WitnessConstraint c w =>
w t -> Dict (c t)
witnessConstraint @_ @Eq w a
wa of
                    Dict (Eq a)
Dict -> a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a
b

matchSomeOf ::
       forall (w :: Type -> Type) (a :: Type). TestEquality w
    => w a
    -> SomeOf w
    -> Maybe a
matchSomeOf :: forall (w :: Type -> Type) a.
TestEquality w =>
w a -> SomeOf w -> Maybe a
matchSomeOf w a
wit SomeOf w
av = do
    Identity a
a <- w a -> SomeOf w -> Maybe (Identity a)
forall {k} (w :: k -> Type) (a :: k) (f :: k -> Type).
TestEquality w =>
w a -> SomeFor f w -> Maybe (f a)
matchSomeFor w a
wit SomeOf w
av
    a -> Maybe a
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return a
a

type Some :: forall k. (k -> Type) -> Type
type Some @k = SomeFor @k (Const ())

pattern MkSome :: w a -> Some w

pattern $mMkSome :: forall {r} {k} {w :: k -> Type}.
Some w -> (forall {a :: k}. w a -> r) -> ((# #) -> r) -> r
$bMkSome :: forall {k} (w :: k -> Type) (a :: k). w a -> Some w
MkSome wa = MkSomeFor wa (Const ())

{-# COMPLETE MkSome #-}

matchSome ::
       forall k (w :: k -> Type) (a :: k). TestEquality w
    => w a
    -> Some w
    -> Bool
matchSome :: forall k (w :: k -> Type) (a :: k).
TestEquality w =>
w a -> Some w -> Bool
matchSome w a
wit Some w
aw = Maybe (Const () a) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Const () a) -> Bool) -> Maybe (Const () a) -> Bool
forall a b. (a -> b) -> a -> b
$ w a -> Some w -> Maybe (Const () a)
forall {k} (w :: k -> Type) (a :: k) (f :: k -> Type).
TestEquality w =>
w a -> SomeFor f w -> Maybe (f a)
matchSomeFor w a
wit Some w
aw

instance forall k (w :: k -> Type). TestEquality w => Eq (Some w) where
    == :: Some w -> Some w -> Bool
(==) (MkSome w a
wa) = w a -> Some w -> Bool
forall k (w :: k -> Type) (a :: k).
TestEquality w =>
w a -> Some w -> Bool
matchSome w a
wa

instance forall k (w :: k -> Type). TestOrder w => Ord (Some w) where
    compare :: Some w -> Some w -> Ordering
compare (MkSome w a
wa) (MkSome w a
wb) = WOrdering a a -> Ordering
forall {k} (a :: k) (b :: k). WOrdering a b -> Ordering
wOrderingToOrdering (WOrdering a a -> Ordering) -> WOrdering a a -> Ordering
forall a b. (a -> b) -> a -> b
$ w a -> w a -> WOrdering a a
forall (a :: k) (b :: k). w a -> w b -> WOrdering a b
forall k (w :: k -> Type) (a :: k) (b :: k).
TestOrder w =>
w a -> w b -> WOrdering a b
testCompare w a
wa w a
wb

withSomeAllConstraint ::
       forall k (c :: Type -> Constraint) (w :: k -> Type) (r :: Type). AllConstraint c w
    => Some w
    -> (forall a. c (w a) => w a -> r)
    -> r
withSomeAllConstraint :: forall k (c :: Type -> Constraint) (w :: k -> Type) r.
AllConstraint c w =>
Some w -> (forall (a :: k). c (w a) => w a -> r) -> r
withSomeAllConstraint (MkSome w a
wa) forall (a :: k). c (w a) => w a -> r
call = forall k (c :: Type -> Constraint) (w :: k -> Type) (a :: k) r.
AllConstraint c w =>
w a -> (c (w a) => r) -> r
withAllConstraint @k @c w a
wa ((c (w a) => r) -> r) -> (c (w a) => r) -> r
forall a b. (a -> b) -> a -> b
$ w a -> r
forall (a :: k). c (w a) => w a -> r
call w a
wa

instance forall k (w :: k -> Type). AllConstraint Show w => Show (Some w) where
    show :: Some w -> String
show Some w
swa = forall k (c :: Type -> Constraint) (w :: k -> Type) r.
AllConstraint c w =>
Some w -> (forall (a :: k). c (w a) => w a -> r) -> r
withSomeAllConstraint @k @Show Some w
swa w a -> String
forall (a :: k). Show (w a) => w a -> String
forall a. Show a => a -> String
show

someForToSome :: SomeFor f w -> Some w
someForToSome :: forall {k} (f :: k -> Type) (w :: k -> Type). SomeFor f w -> Some w
someForToSome (MkSomeFor w a
wa f a
_) = w a -> Some w
forall {k} (w :: k -> Type) (a :: k). w a -> Some w
MkSome w a
wa