{-# 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.Inhabited (Inhabited (..), withInhabited) where
import GHC.Generics
import Unsafe.Coerce (unsafeCoerce)
class Inhabited a where
trivial :: a
default trivial :: (Generic a, GInhabited (Rep a)) => a
trivial = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to Rep a Any
forall a. Rep a a
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 = f a -> M1 i t f a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 f a
forall (a :: k). f a
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 = f a
forall (a :: k). f a
forall {k} (f :: k -> *) (a :: k). GInhabited f => f a
gtrivial f a -> g a -> (:*:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
forall (a :: k). g a
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 = c -> K1 i c a
forall k i c (p :: k). c -> K1 i c p
K1 c
forall a. Inhabited a => a
trivial
instance GInhabited U1 where
gtrivial :: forall (a :: k). U1 a
gtrivial = U1 a
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 = b -> a -> b
forall a b. a -> b -> a
const b
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 = MagicInhabited a b -> a -> b
forall a b. a -> b
unsafeCoerce ((Inhabited a => b) -> MagicInhabited a b
forall a b. (Inhabited a => b) -> MagicInhabited a b
MagicInhabited b
Inhabited a => b
k :: MagicInhabited a b) a
wit