module Data.Empty where

import Data.Searchable
import Data.Void

-- | There are no values.
class Finite n => Empty n where
    never :: n -> a

instance Empty Void where
    never :: forall a. Void -> a
never = Void -> a
forall a. Void -> a
absurd

instance (Empty a, Empty b) => Empty (Either a b) where
    never :: forall a. Either a b -> a
never (Left a
a) = a -> a
forall a. a -> a
forall n a. Empty n => n -> a
never a
a
    never (Right b
a) = b -> a
forall a. b -> a
forall n a. Empty n => n -> a
never b
a

instance (Empty a, Finite b) => Empty (a, b) where
    never :: forall a. (a, b) -> a
never (a
a, b
_) = a -> a
forall a. a -> a
forall n a. Empty n => n -> a
never a
a