{-# 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 = Rep a Any -> x
forall a x. Rep a a -> x
forall {k} (f :: k -> *) (a :: k) x. GEmpty f => f a -> x
geliminate (Rep a Any -> x) -> (a -> Rep a Any) -> a -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from

class GEmpty f where
  geliminate :: f a -> x

instance (GEmpty f) => GEmpty (M1 i t f) where
  geliminate :: forall (a :: k) x. M1 i t f a -> x
geliminate (M1 f a
a) = f a -> x
forall (a :: k) x. f a -> x
forall {k} (f :: k -> *) (a :: k) x. GEmpty f => f a -> x
geliminate f a
a

instance (GEmpty f, GEmpty g) => GEmpty (f :+: g) where
  geliminate :: forall (a :: k) x. (:+:) f g a -> x
geliminate (L1 f a
a) = f a -> x
forall (a :: k) x. f a -> x
forall {k} (f :: k -> *) (a :: k) x. GEmpty f => f a -> x
geliminate f a
a
  geliminate (R1 g a
b) = g a -> x
forall (a :: k) x. g a -> x
forall {k} (f :: k -> *) (a :: k) x. GEmpty f => f a -> x
geliminate g a
b

instance (Empty c) => GEmpty (K1 i c) where
  geliminate :: forall (a :: k) x. K1 i c a -> x
geliminate (K1 c
a) = c -> x
forall x. c -> x
forall a x. Empty a => a -> x
eliminate c
a

instance GEmpty V1 where
  geliminate :: forall (a :: k) x. V1 a -> x
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 :: forall a b. (a -> Void) -> (Empty a => b) -> b
withEmpty a -> Void
neg Empty a => b
k = MagicEmpty a b -> (a -> Any) -> b
forall a b. a -> b
unsafeCoerce ((Empty a => b) -> MagicEmpty a b
forall e a. (Empty e => a) -> MagicEmpty e a
MagicEmpty b
Empty a => b
k :: MagicEmpty a b) (Void -> Any
forall x. Void -> x
absurd (Void -> Any) -> (a -> Void) -> a -> Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Void
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' :: forall a b. (forall c. a -> c) -> (Empty a => b) -> b
withEmpty' forall c. a -> c
neg Empty a => b
k = MagicEmpty a b -> (a -> Any) -> b
forall a b. a -> b
unsafeCoerce ((Empty a => b) -> MagicEmpty a b
forall e a. (Empty e => a) -> MagicEmpty e a
MagicEmpty b
Empty a => b
k :: MagicEmpty a b) a -> Any
forall c. a -> c
neg