module Data.Type.Witness.General.Representative where

import Data.Type.Witness.General.WitnessValue
import Data.Type.Witness.Specific.Some
import Import

isWitnessRepresentative :: Dict (Is rep a) -> rep a
isWitnessRepresentative :: forall {k} (rep :: k -> Type) (a :: k). Dict (Is rep a) -> rep a
isWitnessRepresentative Dict (Is rep a)
Dict = forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative

type Subrepresentative (p :: k -> Type) (q :: k -> Type) = forall (a :: k). p a -> Dict (Is q a)

withSubrepresentative :: Subrepresentative p q -> p a -> (Is q a => r) -> r
withSubrepresentative :: forall {k} (p :: k -> Type) (q :: k -> Type) (a :: k) r.
Subrepresentative p q -> p a -> (Is q a => r) -> r
withSubrepresentative Subrepresentative p q
subrep p a
pa Is q a => r
f =
    case Subrepresentative p q
subrep p a
pa of
        Dict (Is q a)
Dict -> Is q a => r
f

type Representative :: forall k. (k -> Type) -> Constraint
class Representative rep where
    -- | Every value is an instance of 'Is'.
    getRepWitness :: Subrepresentative rep rep

instance Representative Proxy where
    getRepWitness :: Subrepresentative Proxy Proxy
getRepWitness Proxy a
Proxy = forall (a :: Constraint). a => Dict a
Dict

withRepresentative :: Representative rep => rep a -> (Is rep a => r) -> r
withRepresentative :: forall {k} (rep :: k -> Type) (a :: k) r.
Representative rep =>
rep a -> (Is rep a => r) -> r
withRepresentative = forall {k} (p :: k -> Type) (q :: k -> Type) (a :: k) r.
Subrepresentative p q -> p a -> (Is q a => r) -> r
withSubrepresentative forall k (rep :: k -> Type).
Representative rep =>
Subrepresentative rep rep
getRepWitness

-- | If two representatives have the same type, then they have the same value.
type Is :: forall k. (k -> Type) -> k -> Constraint
class Representative rep => Is rep a where
    -- | The representative value for type @a@.
    representative :: rep a

instance Is Proxy a where
    representative :: Proxy a
representative = forall k (a :: k). Proxy a
Proxy

getRepresentative :: Is rep a => a -> rep a
getRepresentative :: forall (rep :: Type -> Type) a. Is rep a => a -> rep a
getRepresentative a
_ = forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative

rerepresentative :: Is rep a => p a -> rep a
rerepresentative :: forall {k} (rep :: k -> Type) (a :: k) (p :: k -> Type).
Is rep a =>
p a -> rep a
rerepresentative p a
_ = forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative

fromRepWitness :: Dict (Is rep a) -> rep a
fromRepWitness :: forall {k} (rep :: k -> Type) (a :: k). Dict (Is rep a) -> rep a
fromRepWitness Dict (Is rep a)
Dict = forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative

mkSomeOf :: Is rep a => a -> SomeOf rep
mkSomeOf :: forall (rep :: Type -> Type) a. Is rep a => a -> SomeOf rep
mkSomeOf a
a = forall (w :: Type -> Type) a. w a -> a -> SomeOf w
MkSomeOf forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative a
a

mkSomeFor :: Is rep a => f a -> SomeFor f rep
mkSomeFor :: forall {k} (rep :: k -> Type) (a :: k) (f :: k -> Type).
Is rep a =>
f a -> SomeFor f rep
mkSomeFor f a
fa = forall k (f :: k -> Type) (w :: k -> Type) (a :: k).
w a -> f a -> SomeFor f w
MkSomeFor forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative f a
fa

instance Representative ((:~:) (t :: k)) where
    getRepWitness :: Subrepresentative ((:~:) t) ((:~:) t)
getRepWitness t :~: a
Refl = forall (a :: Constraint). a => Dict a
Dict

instance Is ((:~:) (t :: k)) (t :: k) where
    representative :: t :~: t
representative = forall k (t :: k). t :~: t
Refl

instance Representative (Compose Dict c) where
    getRepWitness :: Subrepresentative (Compose Dict c) (Compose Dict c)
getRepWitness (Compose Dict (c a)
Dict) = forall (a :: Constraint). a => Dict a
Dict

instance c t => Is (Compose Dict c) t where
    representative :: Compose Dict c t
representative = forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall (a :: Constraint). a => Dict a
Dict

typeValue ::
       forall k (rep :: k -> Type) (a :: k). (Is rep a, WitnessValue rep)
    => WitnessValueType rep
typeValue :: forall k (rep :: k -> Type) (a :: k).
(Is rep a, WitnessValue rep) =>
WitnessValueType rep
typeValue = forall k (w :: k -> Type) (t :: k).
WitnessValue w =>
w t -> WitnessValueType w
witnessToValue @k @rep (forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative @k @rep @a)

-- | See whether two represented and witnessed types are the same.
matchIs ::
       forall w a b. (TestEquality w, Is w a, Is w b)
    => Maybe (a :~: b)
matchIs :: forall {k} (w :: k -> Type) (a :: k) (b :: k).
(TestEquality w, Is w a, Is w b) =>
Maybe (a :~: b)
matchIs = let
    r :: forall t. Is w t
      => w t
    r :: forall (t :: k). Is w t => w t
r = forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative
    in forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall (t :: k). Is w t => w t
r @a) (forall (t :: k). Is w t => w t
r @b)