{-# language AllowAmbiguousTypes #-}
{-# language EmptyCase #-}
{-# language DataKinds #-}
{-# language FlexibleInstances #-}
{-# language ScopedTypeVariables #-}
{-# language StandaloneKindSignatures #-}
{-# language TypeApplications #-}
{-# language TypeFamilies #-}
{-# language TypeOperators #-}
{-# language UndecidableInstances #-}

module Rel8.Schema.Reify
  ( Reify, Col( Reify ), hreify, hunreify
  , UnwrapReify
  , NotReify, notReify
  )
where

-- base
import Data.Kind ( Constraint )
import Data.Type.Equality ( (:~:)( Refl ) )
import Prelude

-- rel8
import Rel8.Schema.Context ( Interpretation, Col )
import Rel8.Schema.Context.Label ( Labelable, labeler, unlabeler )
import Rel8.Schema.HTable ( HTable, hmap )
import Rel8.Schema.Kind ( Context )


type Reify :: Context -> Context
data Reify context a


instance Interpretation (Reify context) where
  newtype Col (Reify context) spec = Reify (Col context spec)


instance Labelable context => Labelable (Reify context) where
  labeler :: Col (Reify context) ('Spec labels necessity a)
-> Col (Reify context) ('Spec (label : labels) necessity a)
labeler (Reify a) = Col context ('Spec (label : labels) necessity a)
-> Col (Reify context) ('Spec (label : labels) necessity a)
forall (context :: Context) (spec :: Spec).
Col context spec -> Col (Reify context) spec
Reify (Col context ('Spec labels necessity a)
-> Col context ('Spec (label : labels) necessity a)
forall (context :: Context) (labels :: Labels)
       (necessity :: Necessity) a (label :: Symbol).
Labelable context =>
Col context ('Spec labels necessity a)
-> Col context ('Spec (label : labels) necessity a)
labeler Col context ('Spec labels necessity a)
a)
  unlabeler :: Col (Reify context) ('Spec (label : labels) necessity a)
-> Col (Reify context) ('Spec labels necessity a)
unlabeler (Reify a) = Col context ('Spec labels necessity a)
-> Col (Reify context) ('Spec labels necessity a)
forall (context :: Context) (spec :: Spec).
Col context spec -> Col (Reify context) spec
Reify (Col context ('Spec (label : labels) necessity a)
-> Col context ('Spec labels necessity a)
forall (context :: Context) (label :: Symbol) (labels :: Labels)
       (necessity :: Necessity) a.
Labelable context =>
Col context ('Spec (label : labels) necessity a)
-> Col context ('Spec labels necessity a)
unlabeler Col context ('Spec (label : labels) necessity a)
a)


hreify :: HTable t => t (Col context) -> t (Col (Reify context))
hreify :: t (Col context) -> t (Col (Reify context))
hreify = (forall (spec :: Spec).
 Col context spec -> Col (Reify context) spec)
-> t (Col context) -> t (Col (Reify context))
forall (t :: HTable) (context :: HContext) (context' :: HContext).
HTable t =>
(forall (spec :: Spec). context spec -> context' spec)
-> t context -> t context'
hmap forall (spec :: Spec). Col context spec -> Col (Reify context) spec
forall (context :: Context) (spec :: Spec).
Col context spec -> Col (Reify context) spec
Reify


hunreify :: HTable t => t (Col (Reify context)) -> t (Col context)
hunreify :: t (Col (Reify context)) -> t (Col context)
hunreify = (forall (spec :: Spec).
 Col (Reify context) spec -> Col context spec)
-> t (Col (Reify context)) -> t (Col context)
forall (t :: HTable) (context :: HContext) (context' :: HContext).
HTable t =>
(forall (spec :: Spec). context spec -> context' spec)
-> t context -> t context'
hmap (\(Reify a) -> Col context spec
a)


type UnwrapReify :: Context -> Context
type family UnwrapReify context where
  UnwrapReify (Reify context) = context


type IsReify :: Context -> Bool
type family IsReify context where
  IsReify (Reify _) = 'True
  IsReify _ = 'False


type NotReify :: Context -> Constraint
class IsReify context ~ 'False => NotReify context
instance IsReify context ~ 'False => NotReify context


notReify :: forall context ctx a. NotReify context => context :~: Reify ctx -> a
notReify :: (context :~: Reify ctx) -> a
notReify context :~: Reify ctx
refl = case NotReify context => IsReify context :~: 'False
forall (context :: Context).
NotReify context =>
IsReify context :~: 'False
lemma @context of
  IsReify context :~: 'False
Refl -> case context :~: Reify ctx
refl of


lemma :: NotReify context => IsReify context :~: 'False
lemma :: IsReify context :~: 'False
lemma = IsReify context :~: 'False
forall k (a :: k). a :~: a
Refl