{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
{-# LANGUAGE DataKinds, DefaultSignatures, DeriveAnyClass, EmptyCase #-}
{-# LANGUAGE ExplicitNamespaces, FlexibleContexts, FlexibleInstances #-}
{-# LANGUAGE GADTs, KindSignatures, LambdaCase, PolyKinds #-}
{-# LANGUAGE StandaloneDeriving, TupleSections, TypeOperators #-}
module Proof.Propositional.Empty (Empty(..), withEmpty, withEmpty') where
import Data.Void (Void, absurd)
import GHC.Generics
import Unsafe.Coerce (unsafeCoerce)
class Empty a where
eliminate :: a -> x
default eliminate :: (Generic a, GEmpty (Rep a)) => a -> x
eliminate = forall {k} (f :: k -> *) (a :: k) x. GEmpty f => f a -> x
geliminate forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) = 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) = forall {k} (f :: k -> *) (a :: k) x. GEmpty f => f a -> x
geliminate f a
a
geliminate (R1 g a
b) = 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) = 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)
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 = forall a b. a -> b
unsafeCoerce (forall e a. (Empty e => a) -> MagicEmpty e a
MagicEmpty Empty a => b
k :: MagicEmpty a b) (forall x. Void -> x
absurd forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Void
neg)
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 = forall a b. a -> b
unsafeCoerce (forall e a. (Empty e => a) -> MagicEmpty e a
MagicEmpty Empty a => b
k :: MagicEmpty a b) forall c. a -> c
neg