content: {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE DefaultSignatures #-}
  {-# LANGUAGE DeriveAnyClass #-}
  {-# LANGUAGE EmptyCase #-}
  {-# LANGUAGE ExplicitNamespaces #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE KindSignatures #-}
  {-# LANGUAGE LambdaCase #-}
  {-# LANGUAGE PolyKinds #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE StandaloneDeriving #-}
  {-# LANGUAGE TupleSections #-}
  {-# LANGUAGE TypeOperators #-}
  
  module Proof.Propositional.Empty (Empty (..), withEmpty, withEmpty') where
  
  import Data.Void (Void, absurd)
  import GHC.Generics
  import Unsafe.Coerce (unsafeCoerce)
  
  {- | Type-class for types without inhabitants, dual to @'Proof.Propositional.Inhabited'@.
    Current GHC doesn't provide selective-instance,
    hence we don't @'Empty'@ provide instances
    for product types in a generic deriving (DeriveAnyClass).
  
    To derive an instance for each concrete types,
    use @'Proof.Propositional.refute'@.
  
    Since 0.4.0.0.
  -}
  class Empty a where
    eliminate :: a -> x
    default eliminate :: (Generic a, GEmpty (Rep a)) => a -> x
    eliminate = geliminate . from
  
  class GEmpty f where
    geliminate :: f a -> x
  
  instance (GEmpty f) => GEmpty (M1 i t f) where
    geliminate (M1 a) = geliminate a
  
  instance (GEmpty f, GEmpty g) => GEmpty (f :+: g) where
    geliminate (L1 a) = geliminate a
    geliminate (R1 b) = geliminate b
  
  instance (Empty c) => GEmpty (K1 i c) where
    geliminate (K1 a) = eliminate a
  
  instance GEmpty V1 where
    geliminate = \case {}
  
  deriving instance (Empty a, Empty b) => Empty (Either a b)
  
  deriving instance Empty Void
  
  newtype MagicEmpty e a = MagicEmpty ((Empty e) => a)
  
  {- | Giving falsity witness by proving @'Void'@ from @a@.
    See also 'withEmpty''.
  
    Since 0.4.0.0
  -}
  withEmpty :: forall a b. (a -> Void) -> ((Empty a) => b) -> b
  withEmpty neg k = unsafeCoerce (MagicEmpty k :: MagicEmpty a b) (absurd . neg)
  
  {- | Giving falsity witness by showing @a@ entails everything.
    See also 'withEmpty'.
  
    Since 0.4.0.0
  -}
  withEmpty' :: forall a b. (forall c. a -> c) -> ((Empty a) => b) -> b
  withEmpty' neg k = unsafeCoerce (MagicEmpty k :: MagicEmpty a b) neg
  