module Data.Type.Witness.General.WitnessValue where

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

type WitnessValue :: forall k. (k -> Type) -> Constraint
class WitnessValue w where
    type WitnessValueType w :: Type
    witnessToValue :: forall t. w t -> WitnessValueType w
    valueToWitness :: forall r. WitnessValueType w -> (forall t. w t -> r) -> r

someToValue ::
       forall k (w :: k -> Type). WitnessValue w
    => Some w
    -> WitnessValueType w
someToValue :: forall k (w :: k -> Type).
WitnessValue w =>
Some w -> WitnessValueType w
someToValue (MkSome w a
wt) = forall k (w :: k -> Type) (t :: k).
WitnessValue w =>
w t -> WitnessValueType w
witnessToValue w a
wt

valueToSome ::
       forall k (w :: k -> Type). WitnessValue w
    => WitnessValueType w
    -> Some w
valueToSome :: forall k (w :: k -> Type).
WitnessValue w =>
WitnessValueType w -> Some w
valueToSome WitnessValueType w
v = forall k (w :: k -> Type) r.
WitnessValue w =>
WitnessValueType w -> (forall (t :: k). w t -> r) -> r
valueToWitness WitnessValueType w
v forall {k} (w :: k -> Type) (a :: k). w a -> Some w
MkSome