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
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) = forall k (f :: k -> Type) (w :: k -> Type) (a :: k).
w a -> f a -> SomeFor f w
MkSomeFor (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 <- 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
    forall (m :: Type -> Type) a. Monad m => a -> m a
return f a
cfa

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

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

pattern $bMkSomeOf :: forall (w :: Type -> Type) a. w a -> a -> SomeOf w
$mMkSomeOf :: forall {r} {w :: Type -> Type}.
SomeOf w -> (forall {a}. w a -> a -> r) -> ((# #) -> r) -> r
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 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 forall a. Eq a => a -> a -> Bool
== 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 <- 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
    forall (m :: Type -> Type) a. Monad m => a -> m a
return a
a

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

pattern MkSome :: w a -> Some w

pattern $bMkSome :: forall {k} (w :: k -> Type) (a :: k). w a -> Some w
$mMkSome :: forall {r} {k} {w :: k -> Type}.
Some w -> (forall {a :: k}. w a -> r) -> ((# #) -> r) -> r
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 = forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ 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) = 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) = forall {k} (a :: k) (b :: k). WOrdering a b -> Ordering
wOrderingToOrdering forall a b. (a -> b) -> 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 forall a b. (a -> b) -> a -> b
$ 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 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
_) = forall {k} (w :: k -> Type) (a :: k). w a -> Some w
MkSome w a
wa