module Data.Type.Witness.Specific.Empty where

import Data.Type.Witness.General.Finite
import Data.Type.Witness.General.ListElement
import Data.Type.Witness.General.Order
import Data.Type.Witness.General.Representative
import Data.Type.Witness.General.WitnessConstraint
import Data.Type.Witness.Specific.All
import Import

type EmptyType :: forall k. k -> Type
type role EmptyType phantom
newtype EmptyType t =
    MkEmptyType Void
    deriving newtype (EmptyType t -> EmptyType t -> Bool
(EmptyType t -> EmptyType t -> Bool)
-> (EmptyType t -> EmptyType t -> Bool) -> Eq (EmptyType t)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (t :: k). EmptyType t -> EmptyType t -> Bool
$c== :: forall k (t :: k). EmptyType t -> EmptyType t -> Bool
== :: EmptyType t -> EmptyType t -> Bool
$c/= :: forall k (t :: k). EmptyType t -> EmptyType t -> Bool
/= :: EmptyType t -> EmptyType t -> Bool
Eq, Eq (EmptyType t)
Eq (EmptyType t) =>
(EmptyType t -> Maybe (EmptyType t))
-> (Maybe (EmptyType t) -> Maybe (EmptyType t))
-> Countable (EmptyType t)
Maybe (EmptyType t) -> Maybe (EmptyType t)
EmptyType t -> Maybe (EmptyType t)
forall a.
Eq a =>
(a -> Maybe a) -> (Maybe a -> Maybe a) -> Countable a
forall k (t :: k). Eq (EmptyType t)
forall k (t :: k). Maybe (EmptyType t) -> Maybe (EmptyType t)
forall k (t :: k). EmptyType t -> Maybe (EmptyType t)
$ccountPrevious :: forall k (t :: k). EmptyType t -> Maybe (EmptyType t)
countPrevious :: EmptyType t -> Maybe (EmptyType t)
$ccountMaybeNext :: forall k (t :: k). Maybe (EmptyType t) -> Maybe (EmptyType t)
countMaybeNext :: Maybe (EmptyType t) -> Maybe (EmptyType t)
Countable, (forall b. (EmptyType t -> Maybe b) -> Maybe b)
-> Searchable (EmptyType t)
forall b. (EmptyType t -> Maybe b) -> Maybe b
forall a. (forall b. (a -> Maybe b) -> Maybe b) -> Searchable a
forall k (t :: k) b. (EmptyType t -> Maybe b) -> Maybe b
$csearch :: forall k (t :: k) b. (EmptyType t -> Maybe b) -> Maybe b
search :: forall b. (EmptyType t -> Maybe b) -> Maybe b
Searchable, Finite (EmptyType t)
Finite (EmptyType t) =>
(forall a. EmptyType t -> a) -> Empty (EmptyType t)
forall n. Finite n => (forall a. n -> a) -> Empty n
forall a. EmptyType t -> a
forall k (t :: k). Finite (EmptyType t)
forall k (t :: k) a. EmptyType t -> a
$cnever :: forall k (t :: k) a. EmptyType t -> a
never :: forall a. EmptyType t -> a
Empty)

instance Finite (EmptyType t) where
    allValues :: [EmptyType t]
allValues = []
    assemble :: forall b (f :: Type -> Type).
Applicative f =>
(EmptyType t -> f b) -> f (EmptyType t -> b)
assemble EmptyType t -> f b
_ = (EmptyType t -> b) -> f (EmptyType t -> b)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure EmptyType t -> b
forall n a. Empty n => n -> a
forall a. EmptyType t -> a
never

instance TestEquality EmptyType where
    testEquality :: forall (a :: k) (b :: k).
EmptyType a -> EmptyType b -> Maybe (a :~: b)
testEquality = EmptyType a -> EmptyType b -> Maybe (a :~: b)
forall n a. Empty n => n -> a
forall a. EmptyType a -> a
never

instance TestOrder EmptyType where
    testCompare :: forall (a :: k) (b :: k).
EmptyType a -> EmptyType b -> WOrdering a b
testCompare = EmptyType a -> EmptyType b -> WOrdering a b
forall n a. Empty n => n -> a
forall a. EmptyType a -> a
never

instance Representative EmptyType where
    getRepWitness :: Subrepresentative EmptyType EmptyType
getRepWitness = EmptyType a -> Dict (Is EmptyType a)
forall n a. Empty n => n -> a
forall a. EmptyType a -> a
never

instance FiniteWitness EmptyType where
    assembleAllFor :: forall (m :: Type -> Type) (f :: k -> Type).
Applicative m =>
(forall (t :: k). EmptyType t -> m (f t)) -> m (AllFor f EmptyType)
assembleAllFor forall (t :: k). EmptyType t -> m (f t)
_ = AllFor f EmptyType -> m (AllFor f EmptyType)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure AllFor f EmptyType
forall {k} (f :: k -> Type). AllFor f EmptyType
emptyAllFor

instance WitnessConstraint c EmptyType where
    witnessConstraint :: forall (t :: k). EmptyType t -> Dict (c t)
witnessConstraint = EmptyType t -> Dict (c t)
forall n a. Empty n => n -> a
forall a. EmptyType t -> a
never

instance ListElementWitness EmptyType where
    type WitnessTypeList EmptyType = '[]
    toListElementWitness :: forall (t :: k).
EmptyType t -> ListElementType (WitnessTypeList EmptyType) t
toListElementWitness EmptyType t
wit = EmptyType t -> ListElementType '[] t
forall n a. Empty n => n -> a
forall a. EmptyType t -> a
never EmptyType t
wit
    fromListElementWitness :: forall (t :: k).
ListElementType (WitnessTypeList EmptyType) t -> EmptyType t
fromListElementWitness ListElementType (WitnessTypeList EmptyType) t
lt = ListElementType '[] t -> EmptyType t
forall n a. Empty n => n -> a
forall a. ListElementType '[] t -> a
never ListElementType '[] t
ListElementType (WitnessTypeList EmptyType) t
lt

emptyAllOf :: AllOf EmptyType
emptyAllOf :: AllOf EmptyType
emptyAllOf = (forall t. EmptyType t -> t) -> AllOf EmptyType
forall (w :: Type -> Type). (forall t. w t -> t) -> AllOf w
MkAllOf EmptyType t -> t
forall n a. Empty n => n -> a
forall t. EmptyType t -> t
forall a. EmptyType t -> a
never

emptyAllFor :: AllFor f EmptyType
emptyAllFor :: forall {k} (f :: k -> Type). AllFor f EmptyType
emptyAllFor = (forall (t :: k). EmptyType t -> f t) -> AllFor f EmptyType
forall k (f :: k -> Type) (w :: k -> Type).
(forall (t :: k). w t -> f t) -> AllFor f w
MkAllFor EmptyType t -> f t
forall (t :: k). EmptyType t -> f t
forall n a. Empty n => n -> a
forall a. EmptyType t -> a
never