{-# LANGUAGE DataKinds, DefaultSignatures, DeriveAnyClass, EmptyCase  #-}
{-# LANGUAGE ExplicitNamespaces, FlexibleContexts, FlexibleInstances  #-}
{-# LANGUAGE GADTs, KindSignatures, LambdaCase, PolyKinds, RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TupleSections   #-}
{-# LANGUAGE TypeOperators                                            #-}
module Proof.Propositional.Inhabited (Inhabited(..), withInhabited) where
import GHC.Generics
import Unsafe.Coerce (unsafeCoerce)

-- | Types with at least one inhabitant, dual to @'Proof.Propositional.Empty'@.
--   Currently, GHC doesn't provide a selective-instance,
--   hence we can't generically derive @'Inhabited'@ instances
--   for sum types (i.e. by @DeriveAnyClass@).
--
--   To derive an instance for each concrete types,
--   use @'Proof.Propositional.prove'@.
--
--   Since 0.4.0.0.
class Inhabited a where
  -- | A /generic/ inhabitant of type @'a'@, which means that
  --   one cannot assume anything about the value of @'trivial'@
  --   except that it
  --
  --   * is of type @a@, and
  --   * doesn't contain any partial values.
  trivial :: a

  default trivial :: (Generic a, GInhabited (Rep a)) => a
  trivial = forall a x. Generic a => Rep a x -> a
to forall {k} (f :: k -> *) (a :: k). GInhabited f => f a
gtrivial

class GInhabited f where
  gtrivial :: f a

instance GInhabited f => GInhabited (M1 i t f) where
  gtrivial :: forall (a :: k). M1 i t f a
gtrivial = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall {k} (f :: k -> *) (a :: k). GInhabited f => f a
gtrivial

instance (GInhabited f, GInhabited g) => GInhabited (f :*: g) where
  gtrivial :: forall (a :: k). (:*:) f g a
gtrivial = forall {k} (f :: k -> *) (a :: k). GInhabited f => f a
gtrivial forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall {k} (f :: k -> *) (a :: k). GInhabited f => f a
gtrivial

instance Inhabited c => GInhabited (K1 i c) where
  gtrivial :: forall (a :: k). K1 i c a
gtrivial = forall k i c (p :: k). c -> K1 i c p
K1 forall a. Inhabited a => a
trivial

instance GInhabited U1 where
  gtrivial :: forall (a :: k). U1 a
gtrivial = forall k (a :: k). U1 a
U1

deriving instance Inhabited ()
deriving instance (Inhabited a, Inhabited b) => Inhabited (a, b)
deriving instance (Inhabited a, Inhabited b, Inhabited c) => Inhabited (a, b, c)
deriving instance (Inhabited a, Inhabited b, Inhabited c, Inhabited d) => Inhabited (a, b, c, d)

instance Inhabited b => Inhabited (a -> b) where
  trivial :: a -> b
trivial = forall a b. a -> b -> a
const forall a. Inhabited a => a
trivial

newtype MagicInhabited a b = MagicInhabited (Inhabited a => b)

withInhabited :: forall a b. a -> (Inhabited a => b) -> b
withInhabited :: forall a b. a -> (Inhabited a => b) -> b
withInhabited a
wit Inhabited a => b
k = forall a b. a -> b
unsafeCoerce (forall a b. (Inhabited a => b) -> MagicInhabited a b
MagicInhabited Inhabited a => b
k :: MagicInhabited a b) a
wit