module Data.Type.Witness.Specific.Symbol ( module Data.Type.Witness.Specific.Symbol , Symbol , KnownSymbol ) where import Data.Type.Witness.General.AllConstraint import Data.Type.Witness.General.Order import Data.Type.Witness.General.Representative import Data.Type.Witness.General.WitnessValue import GHC.TypeLits import Import type SymbolType :: Symbol -> Type data SymbolType symbol where MkSymbolType :: KnownSymbol symbol => SymbolType symbol instance WitnessValue SymbolType where type WitnessValueType SymbolType = String witnessToValue :: forall t. SymbolType t -> String witnessToValue :: forall (t :: Symbol). SymbolType t -> String witnessToValue SymbolType t MkSymbolType = forall (n :: Symbol) (proxy :: Symbol -> Type). KnownSymbol n => proxy n -> String symbolVal (forall {k} (t :: k). Proxy t Proxy :: Proxy t) valueToWitness :: forall r. WitnessValueType SymbolType -> (forall (t :: Symbol). SymbolType t -> r) -> r valueToWitness WitnessValueType SymbolType s forall (t :: Symbol). SymbolType t -> r cont = case String -> SomeSymbol someSymbolVal WitnessValueType SymbolType s of SomeSymbol Proxy n p -> let psw :: forall (t :: Symbol). KnownSymbol t => Proxy t -> SymbolType t psw :: forall (t :: Symbol). KnownSymbol t => Proxy t -> SymbolType t psw Proxy t _ = forall (symbol :: Symbol). KnownSymbol symbol => SymbolType symbol MkSymbolType in forall (t :: Symbol). SymbolType t -> r cont forall a b. (a -> b) -> a -> b $ forall (t :: Symbol). KnownSymbol t => Proxy t -> SymbolType t psw Proxy n p instance TestEquality SymbolType where testEquality :: forall (a :: Symbol) (b :: Symbol). SymbolType a -> SymbolType b -> Maybe (a :~: b) testEquality (SymbolType a MkSymbolType :: SymbolType a) (SymbolType b MkSymbolType :: SymbolType b) = forall (a :: Symbol) (b :: Symbol) (proxy1 :: Symbol -> Type) (proxy2 :: Symbol -> Type). (KnownSymbol a, KnownSymbol b) => proxy1 a -> proxy2 b -> Maybe (a :~: b) sameSymbol (forall {k} (t :: k). Proxy t Proxy @a) (forall {k} (t :: k). Proxy t Proxy @b) instance TestOrder SymbolType where testCompare :: forall (a :: Symbol) (b :: Symbol). SymbolType a -> SymbolType b -> WOrdering a b testCompare SymbolType a a SymbolType b b = case forall {k} (f :: k -> Type) (a :: k) (b :: k). TestEquality f => f a -> f b -> Maybe (a :~: b) testEquality SymbolType a a SymbolType b b of Just a :~: b Refl -> forall k (a :: k). WOrdering a a WEQ Maybe (a :~: b) Nothing -> if forall k (w :: k -> Type) (t :: k). WitnessValue w => w t -> WitnessValueType w witnessToValue SymbolType a a forall a. Ord a => a -> a -> Bool > forall k (w :: k -> Type) (t :: k). WitnessValue w => w t -> WitnessValueType w witnessToValue SymbolType b b then forall k (a :: k) (b :: k). WOrdering a b WGT else forall k (a :: k) (b :: k). WOrdering a b WLT instance Representative SymbolType where getRepWitness :: Subrepresentative SymbolType SymbolType getRepWitness SymbolType a MkSymbolType = forall (a :: Constraint). a => Dict a Dict instance KnownSymbol symbol => Is SymbolType symbol where representative :: SymbolType symbol representative = forall (symbol :: Symbol). KnownSymbol symbol => SymbolType symbol MkSymbolType instance Show (SymbolType symbol) where show :: SymbolType symbol -> String show = forall k (w :: k -> Type) (t :: k). WitnessValue w => w t -> WitnessValueType w witnessToValue instance AllConstraint Show SymbolType where allConstraint :: forall (t :: Symbol). Dict (Show (SymbolType t)) allConstraint = forall (a :: Constraint). a => Dict a Dict