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