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
newtype EmptyType t =
    MkEmptyType Void
    deriving (EmptyType t -> EmptyType t -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
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
$c== :: forall k (t :: k). EmptyType t -> EmptyType t -> Bool
Eq, 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)
countMaybeNext :: Maybe (EmptyType t) -> Maybe (EmptyType t)
$ccountMaybeNext :: forall k (t :: k). Maybe (EmptyType t) -> Maybe (EmptyType t)
countPrevious :: EmptyType t -> Maybe (EmptyType t)
$ccountPrevious :: forall k (t :: k). EmptyType t -> Maybe (EmptyType t)
Countable, 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
search :: forall b. (EmptyType t -> Maybe b) -> Maybe b
$csearch :: forall k (t :: k) b. (EmptyType t -> Maybe b) -> Maybe b
Searchable, 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
never :: forall a. EmptyType t -> a
$cnever :: forall k (t :: k) 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
_ = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall n a. Empty n => n -> a
never

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

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

instance Representative EmptyType where
    getRepWitness :: Subrepresentative EmptyType EmptyType
getRepWitness = forall n a. Empty n => n -> 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)
_ = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall {k} (f :: k -> Type). AllFor f EmptyType
emptyAllFor

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

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

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

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