Add reify and unreify to Table class

Previously these were implemented with `unsafeCoerce`, which was mostly correct, but was incorrect for certain instances of `HList`. With this change, `deriving Rel8able` will now fail to type check in those instances.
2024-08-17 20:00:23 +03:00 · 2021-04-27 14:40:10 +01:00 · 2021-04-27 14:40:10 +01:00 · 1c73ec6814
commit 1c73ec6814
parent 1276bebbb0
20 changed files with 576 additions and 139 deletions
--- a/rel8.cabal
+++ b/rel8.cabal
@ -63,6 +63,7 @@ library

    Rel8.FCF

+    Rel8.Kind.Context
    Rel8.Kind.Labels
    Rel8.Kind.Necessity

@ -115,6 +116,7 @@ library
    Rel8.Schema.Kind
    Rel8.Schema.Name
    Rel8.Schema.Null
+    Rel8.Schema.Reify
    Rel8.Schema.Result
    Rel8.Schema.Spec
    Rel8.Schema.Spec.ConstrainDBType
@ -148,6 +150,7 @@ library
    Rel8.Table.Tag
    Rel8.Table.These
    Rel8.Table.Undefined
+    Rel8.Table.Unreify

    Rel8.Type
    Rel8.Type.Array
--- a/src/Rel8/Aggregate.hs
+++ b/src/Rel8/Aggregate.hs
@ -37,9 +37,13 @@ import Rel8.Schema.Context.Label ( Labelable(..) )
 import Rel8.Schema.HTable ( hfield, htabulate, htabulateA, hspecs )
 import Rel8.Schema.Name ( Name )
 import Rel8.Schema.Null ( Sql )
+import Rel8.Schema.Reify ( notReify )
 import Rel8.Schema.Result ( Result )
 import Rel8.Schema.Spec ( Spec( Spec ), SSpec(..) )
-import Rel8.Table ( Table, Columns, Context, fromColumns, toColumns )
+import Rel8.Table
+  ( Table, Columns, Context, fromColumns, toColumns
+  , reify, unreify
+  )
 import Rel8.Table.Recontextualize ( Recontextualize )
 import Rel8.Type ( DBType )

@ -82,6 +86,9 @@ instance Table Expr a => Table Aggregate (Aggregate a) where
    case hfield as field of
      Aggregation a -> DB <$> a

+  reify = notReify
+  unreify = notReify
+

 instance Sql DBType a =>
  Recontextualize Aggregate Aggregate (Aggregate (Expr a)) (Aggregate (Expr a))
--- a/src/Rel8/Expr.hs
+++ b/src/Rel8/Expr.hs
@ -41,9 +41,12 @@ import Rel8.Schema.Context ( Interpretation, Col )
 import Rel8.Schema.Context.Label ( Labelable, labeler, unlabeler )
 import Rel8.Schema.HTable.Type ( HType( HType ) )
 import Rel8.Schema.Null ( Nullity( Null, NotNull ), Sql, nullable )
+import Rel8.Schema.Reify ( notReify )
 import Rel8.Schema.Result ( Result )
 import Rel8.Schema.Spec ( Spec( Spec ) )
-import Rel8.Table ( Table, Columns, Context, fromColumns, toColumns )
+import Rel8.Table
+  ( Table, Columns, Context, fromColumns, toColumns, reify, unreify
+  )
 import Rel8.Table.Recontextualize ( Recontextualize )
 import Rel8.Type ( DBType )
 import Rel8.Type.Monoid ( DBMonoid, memptyExpr )
@ -112,6 +115,8 @@ instance Sql DBType a => Table Expr (Expr a) where

  toColumns a = HType (DB a)
  fromColumns (HType (DB a)) = a
+  reify = notReify
+  unreify = notReify


 instance Sql DBType a => Recontextualize Expr Expr (Expr a) (Expr a)
--- a/src/Rel8/Generic/Table.hs
+++ b/src/Rel8/Generic/Table.hs
@ -12,7 +12,8 @@
 {-# language UndecidableInstances #-}

 module Rel8.Generic.Table
-  ( GTable, GColumns, GContext, fromGColumns, toGColumns, gtable
+  ( GTable, GColumns, GContext, GUnreify
+  , fromGColumns, toGColumns, gtable, greify, gunreify
  )
 where

@ -53,6 +54,14 @@ type family GContext _Context rep where
  GContext _Context (K1 _ a) = Eval (_Context a)


+type GUnreify :: (Type -> Exp a) -> (Type -> Type) -> Type -> Type
+type family GUnreify _Unreify rep where
+  GUnreify _Unreify (M1 i c rep) = M1 i c (GUnreify _Unreify rep)
+  GUnreify _Unreify (rep1 :*: rep2) =
+    GUnreify _Unreify rep1 :*: GUnreify _Unreify rep2
+  GUnreify _Unreify (K1 i a) = K1 i (Eval (_Unreify a))
+
+
 type GTable
  :: (Type -> Exp Constraint)
  -> (Type -> Exp K.HTable)
@ -73,6 +82,18 @@ class GTable _Table _Columns context rep
    => (forall a. Eval (_Table a) => Proxy a -> Eval (_Columns a) context)
    -> GColumns _Columns rep context

+  greify :: ()
+    => Proxy _Unreify
+    -> (forall a. Eval (_Table a) => Eval (_Unreify a) -> a)
+    -> GUnreify _Unreify rep x
+    -> rep x
+
+  gunreify :: ()
+    => Proxy _Unreify
+    -> (forall a. Eval (_Table a) => a -> Eval (_Unreify a))
+    -> rep x
+    -> GUnreify _Unreify rep x
+

 instance GTable _Table _Columns context rep =>
  GTable _Table _Columns context (M1 D c rep)
@ -82,6 +103,10 @@ instance GTable _Table _Columns context rep =>
  toGColumns toColumns (M1 a) =
    toGColumns @_Table @_Columns @context @rep toColumns a
  gtable = gtable @_Table @_Columns @context @rep
+  greify proxy reify (M1 a) =
+    M1 (greify @_Table @_Columns @context @rep proxy reify a)
+  gunreify proxy unreify (M1 a) =
+    M1 (gunreify @_Table @_Columns @context @rep proxy unreify a)


 instance GTable _Table _Columns context rep =>
@ -92,6 +117,10 @@ instance GTable _Table _Columns context rep =>
  toGColumns toColumns (M1 a) =
    toGColumns @_Table @_Columns @context @rep toColumns a
  gtable = gtable @_Table @_Columns @context @rep
+  greify proxy reify (M1 a) =
+    M1 (greify @_Table @_Columns @context @rep proxy reify a)
+  gunreify proxy unreify (M1 a) =
+    M1 (gunreify @_Table @_Columns @context @rep proxy unreify a)


 instance
@ -109,6 +138,12 @@ instance
  gtable table = HProduct
    (gtable @_Table @_Columns @context @rep1 table)
    (gtable @_Table @_Columns @context @rep2 table)
+  greify proxy reify (a :*: b) =
+    greify @_Table @_Columns @context @rep1 proxy reify a :*:
+    greify @_Table @_Columns @context @rep2 proxy reify b
+  gunreify proxy unreify (a :*: b) =
+    gunreify @_Table @_Columns @context @rep1 proxy unreify a :*:
+    gunreify @_Table @_Columns @context @rep2 proxy unreify b


 instance
@ -116,7 +151,6 @@ instance
  , Eval (_Table a)
  , HLabelable context
  , KnownSymbol label
-  , GColumns _Columns (M1 S meta k1) ~ HLabel label (Eval (_Columns a))
  , meta ~ 'MetaSel ('Just label) _su _ss _ds
  , k1 ~ K1 i a
  )
@ -125,3 +159,5 @@ instance
  fromGColumns fromColumns = M1 . K1 . fromColumns . hunlabel hunlabeler
  toGColumns toColumns (M1 (K1 a)) = hlabel hlabeler (toColumns a)
  gtable table = hlabel hlabeler (table (Proxy @a))
+  greify _ reify (M1 (K1 a)) = M1 (K1 (reify a))
+  gunreify _ unreify (M1 (K1 a)) = M1 (K1 (unreify a))
--- a/src/Rel8/Kind/Context.hs
+++ b/src/Rel8/Kind/Context.hs
@ -0,0 +1,89 @@
+{-# language DataKinds #-}
+{-# language GADTs #-}
+{-# language LambdaCase #-}
+{-# language StandaloneKindSignatures #-}
+
+module Rel8.Kind.Context
+  ( Reifiable( contextSing )
+  , SContext(..)
+  , sReifiable
+  , sLabelable
+  )
+where
+
+-- base
+import Data.Kind ( Constraint, Type )
+import Prelude ()
+
+-- rel8
+import Rel8.Aggregate ( Aggregate )
+import Rel8.Expr ( Expr )
+import Rel8.Schema.Dict ( Dict( Dict ) )
+import Rel8.Schema.Context ( Interpretation )
+import Rel8.Schema.Context.Label ( Labelable )
+import Rel8.Schema.Insert ( Insert )
+import Rel8.Schema.Kind ( Context )
+import Rel8.Schema.Name ( Name )
+import Rel8.Schema.Reify ( Reify )
+import Rel8.Schema.Result ( Result )
+
+
+type SContext :: Context -> Type
+data SContext context where
+  SAggregate :: SContext Aggregate
+  SExpr :: SContext Expr
+  SInsert :: SContext Insert
+  SName :: SContext Name
+  SResult :: SContext Result
+  SReify :: SContext context -> SContext (Reify context)
+
+
+type Reifiable :: Context -> Constraint
+class Interpretation context => Reifiable context where
+  contextSing :: SContext context
+
+
+instance Reifiable Aggregate where
+  contextSing = SAggregate
+
+
+instance Reifiable Expr where
+  contextSing = SExpr
+
+
+instance Reifiable Result where
+  contextSing = SResult
+
+
+instance Reifiable Insert where
+  contextSing = SInsert
+
+
+instance Reifiable Name where
+  contextSing = SName
+
+
+instance Reifiable context => Reifiable (Reify context) where
+  contextSing = SReify contextSing
+
+
+sReifiable :: SContext context -> Dict Reifiable context
+sReifiable = \case
+  SAggregate -> Dict
+  SExpr -> Dict
+  SInsert -> Dict
+  SName -> Dict
+  SResult -> Dict
+  SReify context -> case sReifiable context of
+    Dict -> Dict
+
+
+sLabelable :: SContext context -> Dict Labelable context
+sLabelable = \case
+  SAggregate -> Dict
+  SExpr -> Dict
+  SInsert -> Dict
+  SName -> Dict
+  SResult -> Dict
+  SReify context -> case sLabelable context of
+    Dict -> Dict
--- a/src/Rel8/Schema/Field.hs
+++ b/src/Rel8/Schema/Field.hs
@ -10,31 +10,28 @@
 module Rel8.Schema.Field
  ( Field
  , HEither, HList, HMaybe, HNonEmpty, HThese
-  , Reify, hreify, hunreify
-  , Reifiable(..)
  , AField(..)
  , AHEither(..), AHList(..), AHMaybe(..), AHNonEmpty(..), AHThese(..)
-  , SContext(..)
  )
 where

 -- base
+import Control.Applicative ( liftA2 )
 import Data.Bifunctor ( Bifunctor, bimap )
-import Data.Kind ( Constraint, Type )
+import Data.Kind ( Type )
 import Data.List.NonEmpty ( NonEmpty )
 import Prelude

 -- rel8
 import Rel8.Aggregate ( Aggregate, Col(..) )
 import Rel8.Expr ( Expr, Col(..) )
+import Rel8.Kind.Context ( SContext(..), Reifiable( contextSing ) )
 import Rel8.Kind.Necessity
  ( Necessity( Required, Optional )
  , SNecessity( SRequired, SOptional )
  , KnownNecessity, necessitySing
  )
-import Rel8.Schema.Context ( Interpretation, Col(..) )
-import Rel8.Schema.Context.Label ( Labelable, labeler, unlabeler )
-import Rel8.Schema.HTable ( HTable, hfield, htabulate )
+import Rel8.Schema.Context ( Col(..) )
 import Rel8.Schema.HTable.Either ( HEitherTable )
 import Rel8.Schema.HTable.List ( HListTable )
 import Rel8.Schema.HTable.Maybe ( HMaybeTable )
@ -45,11 +42,12 @@ import Rel8.Schema.Insert ( Insert, Col(..) )
 import qualified Rel8.Schema.Kind as K
 import Rel8.Schema.Name ( Name(..), Col(..) )
 import Rel8.Schema.Null ( Sql )
+import Rel8.Schema.Reify ( Reify, Col(..), hreify, hunreify )
 import Rel8.Schema.Result ( Result )
 import Rel8.Schema.Spec ( Spec( Spec ) )
 import Rel8.Table
-  ( Table, Columns, Context, fromColumns, toColumns
-  , Congruent
+  ( Table, Columns, Congruent, Context, fromColumns, toColumns
+  , Unreify, reify, unreify
  )
 import Rel8.Table.Either ( EitherTable )
 import Rel8.Table.List ( ListTable( ListTable ) )
@ -57,6 +55,7 @@ import Rel8.Table.Maybe ( MaybeTable )
 import Rel8.Table.NonEmpty ( NonEmptyTable( NonEmptyTable ) )
 import Rel8.Table.Recontextualize ( Recontextualize )
 import Rel8.Table.These ( TheseTable )
+import Rel8.Table.Unreify ( Unreifiable )
 import Rel8.Type ( DBType )

 -- these
@ -133,9 +132,12 @@ instance (Reifiable context, KnownNecessity necessity, Sql DBType a) =>
 where
  type Context (AField context necessity a) = Reify context
  type Columns (AField context necessity a) = HIdentity ('Spec '[""] necessity a)
+  type Unreify (AField context necessity a) = Field context necessity a

  fromColumns (HIdentity (Reify a)) = sfromColumn contextSing a
  toColumns = HIdentity . Reify . stoColumn contextSing necessitySing
+  reify _ = AField
+  unreify _ (AField a) = a


 instance
@ -166,9 +168,12 @@ instance (Reifiable context, Table (Reify context) a, Table (Reify context) b)
 where
  type Context (AHEither context a b) = Reify context
  type Columns (AHEither context a b) = HEitherTable (Columns a) (Columns b)
+  type Unreify (AHEither context a b) = HEither context (Unreify a) (Unreify b)

  fromColumns = sfromColumnsEither contextSing
  toColumns = stoColumnsEither contextSing
+  reify proof = liftA2 bimap reify reify proof . AHEither
+  unreify proof = (\(AHEither a) -> a) . liftA2 bimap unreify unreify proof


 instance
@ -187,18 +192,30 @@ type AHList :: K.Context -> Type -> Type
 newtype AHList context a = AHList (HList context a)


-instance (Reifiable context, Table (Reify context) a) =>
-  Table (Reify context) (AHList context a)
+instance
+  ( Reifiable context
+  , Table (Reify context) a
+  , Unreifiable (Reify context) a
+  )
+  => Table (Reify context) (AHList context a)
 where
  type Context (AHList context a) = Reify context
  type Columns (AHList context a) = HListTable (Columns a)
+  type Unreify (AHList context a) = HList context (Unreify a)

  fromColumns = sfromColumnsList contextSing
  toColumns = stoColumnsList contextSing
+  reify proof =
+    smapList contextSing (reify proof) hreify .
+    AHList
+  unreify proof =
+    (\(AHList a) -> a) .
+    smapList contextSing (unreify proof) hunreify


 instance
  ( Reifiable context, Reifiable context'
+  , Unreifiable (Reify context) a, Unreifiable (Reify context') a'
  , Recontextualize (Reify context) (Reify context') a a'
  ) =>
  Recontextualize
@ -221,9 +238,12 @@ instance (Reifiable context, Table (Reify context) a) =>
 where
  type Context (AHMaybe context a) = Reify context
  type Columns (AHMaybe context a) = HMaybeTable (Columns a)
+  type Unreify (AHMaybe context a) = HMaybe context (Unreify a)

  fromColumns = sfromColumnsMaybe contextSing
  toColumns = stoColumnsMaybe contextSing
+  reify proof = fmap fmap reify proof . AHMaybe
+  unreify proof = (\(AHMaybe a) -> a) . fmap fmap unreify proof


 instance
@ -241,18 +261,30 @@ type AHNonEmpty :: K.Context -> Type -> Type
 newtype AHNonEmpty context a = AHNonEmpty (HNonEmpty context a)


-instance (Reifiable context, Table (Reify context) a) =>
-  Table (Reify context) (AHNonEmpty context a)
+instance
+  ( Reifiable context
+  , Table (Reify context) a
+  , Unreifiable (Reify context) a
+  )
+  => Table (Reify context) (AHNonEmpty context a)
 where
  type Context (AHNonEmpty context a) = Reify context
  type Columns (AHNonEmpty context a) = HNonEmptyTable (Columns a)
+  type Unreify (AHNonEmpty context a) = HNonEmpty context (Unreify a)

  fromColumns = sfromColumnsNonEmpty contextSing
  toColumns = stoColumnsNonEmpty contextSing
+  reify proof =
+    smapNonEmpty contextSing (reify proof) hreify .
+    AHNonEmpty
+  unreify proof =
+    (\(AHNonEmpty a) -> a) .
+    smapNonEmpty contextSing (unreify proof) hunreify


 instance
  ( Reifiable context, Reifiable context'
+  , Unreifiable (Reify context) a, Unreifiable (Reify context') a'
  , Recontextualize (Reify context) (Reify context') a a'
  ) =>
  Recontextualize
@ -279,9 +311,12 @@ instance (Reifiable context, Table (Reify context) a, Table (Reify context) b)
 where
  type Context (AHThese context a b) = Reify context
  type Columns (AHThese context a b) = HTheseTable (Columns a) (Columns b)
+  type Unreify (AHThese context a b) = HThese context (Unreify a) (Unreify b)

  fromColumns = sfromColumnsThese contextSing
  toColumns = stoColumnsThese contextSing
+  reify proof = liftA2 bimap reify reify proof . AHThese
+  unreify proof = (\(AHThese a) -> a) . liftA2 bimap unreify unreify proof


 instance
@ -296,58 +331,6 @@ instance
    (AHThese context' a' b')


-type SContext :: K.Context -> Type
-data SContext context where
-  SAggregate :: SContext Aggregate
-  SExpr :: SContext Expr
-  SInsert :: SContext Insert
-  SName :: SContext Name
-  SResult :: SContext Result
-  SReify :: SContext context -> SContext (Reify context)
-
-
-type Reifiable :: K.Context -> Constraint
-class Interpretation context => Reifiable context where
-  contextSing :: SContext context
-
-
-instance Reifiable Aggregate where
-  contextSing = SAggregate
-
-
-instance Reifiable Expr where
-  contextSing = SExpr
-
-
-instance Reifiable Result where
-  contextSing = SResult
-
-
-instance Reifiable Insert where
-  contextSing = SInsert
-
-
-instance Reifiable Name where
-  contextSing = SName
-
-
-type Reify :: K.Context -> K.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 (Reify a) = Reify (labeler a)
-  unlabeler (Reify a) = Reify (unlabeler a)
-
-
-instance Reifiable context => Reifiable (Reify context) where
-  contextSing = SReify contextSing
-
-
 sfromColumn :: ()
  => SContext context
  -> Col context ('Spec labels necessity a)
@ -710,12 +693,3 @@ stoColumnsThese = \case
    stoColumnsThese context .
    sbimapThese context (hunreify . toColumns) (hunreify . toColumns) .
    (\(AHThese a) -> a)
-
-
-hreify :: HTable t => t (Col context) -> t (Col (Reify context))
-hreify a = htabulate $ \field -> Reify (hfield a field)
-
-
-hunreify :: HTable t => t (Col (Reify context)) -> t (Col context)
-hunreify a = htabulate $ \field -> case hfield a field of
-  Reify x -> x
--- a/src/Rel8/Schema/Generic.hs
+++ b/src/Rel8/Schema/Generic.hs
@ -19,38 +19,56 @@ where

 -- base
 import Data.Kind ( Constraint, Type )
+import Data.Proxy ( Proxy( Proxy ) )
+import Data.Type.Equality ( (:~:)( Refl ) )
 import GHC.Generics ( Generic, Rep, from, to )
 import Prelude
-import Unsafe.Coerce ( unsafeCoerce )

 -- rel8
+import Rel8.Kind.Context
+  ( SContext( SReify )
+  , Reifiable, contextSing
+  , sLabelable, sReifiable
+  )
 import Rel8.Generic.Record ( Record(..) )
 import Rel8.Generic.Table
  ( GTable, GColumns, fromGColumns, toGColumns
+  , GUnreify
  )
+import qualified Rel8.Generic.Table as G
 import Rel8.Schema.Context ( Col )
 import Rel8.Schema.Context.Label ( Labelable )
-import Rel8.Schema.Field ( Reify, Reifiable, hreify, hunreify )
+import Rel8.Schema.Dict ( Dict( Dict ) )
 import Rel8.Schema.HTable ( HTable )
 import qualified Rel8.Schema.Kind as K
 import Rel8.Schema.Name ( Name )
+import Rel8.Schema.Reify ( Reify, UnwrapReify, hreify, hunreify )
 import Rel8.Table
  ( Table, Columns, Context, fromColumns, toColumns
-  , TTable, TColumns
+  , Unreify, reify, unreify
+  , TTable, TColumns, TUnreify
  )


-instance
-  ( Rel8able t
-  , Labelable context
-  , Reifiable context
-  ) => Table context (t context)
+instance (Rel8able t, Labelable context, Reifiable context) =>
+  Table context (t context)
 where
  type Columns (t context) = GRep t
  type Context (t context) = context
+  type Unreify (t context) = t (UnwrapReify context)

-  fromColumns = unreify . gfromColumns . hreify
-  toColumns = hunreify . gtoColumns . reify
+  fromColumns = gunreify . gfromColumns . hreify
+  toColumns = hunreify . gtoColumns . greify
+
+  reify Refl = case contextSing @context of
+    SReify context -> case sLabelable context of
+      Dict -> case sReifiable context of
+        Dict -> greify
+
+  unreify Refl = case contextSing @context of
+    SReify context -> case sLabelable context of
+      Dict -> case sReifiable context of
+        Dict -> gunreify


 type KRel8able :: Type
@ -109,6 +127,12 @@ class HTable (GRep t) => Rel8able t where
  gtoColumns :: (Labelable context, Reifiable context)
    => t (Reify context) -> GRep t (Col (Reify context))

+  greify :: (Labelable context, Reifiable context)
+    => t context -> t (Reify context)
+
+  gunreify :: (Labelable context, Reifiable context)
+    => t (Reify context) -> t context
+
  type GRep t = GColumns TColumns (Rep (Record (t (Reify Name))))

  default gfromColumns :: forall context.
@ -133,18 +157,32 @@ class HTable (GRep t) => Rel8able t where
    from .
    Record

+  default greify :: forall context.
+    ( Generic (Record (t context))
+    , Generic (Record (t (Reify context)))
+    , GTable (TTable (Reify context)) TColumns (Col (Reify context)) (Rep (Record (t (Reify context))))
+    , Rep (Record (t context)) ~ GUnreify TUnreify (Rep (Record (t (Reify context))))
+    )
+    => t context -> t (Reify context)
+  greify =
+    unrecord .
+    to .
+    G.greify @(TTable (Reify context)) @TColumns @(Col (Reify context)) (Proxy @TUnreify)
+      (reify Refl) .
+    from .
+    Record

-reify ::
-  (-- Rel8able t
-  --, forall necessity a. Coercible (Field context necessity a) (AField context necessity a) => Coercible (t context) (t (Reify context))
-  )
-  => t context -> t (Reify context)
-reify = unsafeCoerce
-
-
-unreify ::
-  (-- Rel8able t
-  --, forall necessity a. Coercible (AField context necessity a) (Field context necessity a) => Coercible (t (Reify context)) (t context)
-  )
-  => t (Reify context) -> t context
-unreify = unsafeCoerce
+  default gunreify :: forall context.
+    ( Generic (Record (t context))
+    , Generic (Record (t (Reify context)))
+    , GTable (TTable (Reify context)) TColumns (Col (Reify context)) (Rep (Record (t (Reify context))))
+    , Rep (Record (t context)) ~ GUnreify TUnreify (Rep (Record (t (Reify context))))
+    )
+    => t (Reify context) -> t context
+  gunreify =
+    unrecord .
+    to .
+    G.gunreify @(TTable (Reify context)) @TColumns @(Col (Reify context)) (Proxy @TUnreify)
+      (unreify Refl) .
+    from .
+    Record
--- a/src/Rel8/Schema/Generic/Test.hs
+++ b/src/Rel8/Schema/Generic/Test.hs
@ -8,6 +8,8 @@
 {-# language StandaloneDeriving #-}
 {-# language TypeFamilies #-}

+{-# options_ghc -O0 #-}
+
 module Rel8.Schema.Generic.Test
  ( module Rel8.Schema.Generic.Test
  )
@ -77,7 +79,7 @@ data TableList f = TableList

 data TableNonEmpty f = TableNonEmpty
  { foo :: Column f Bool
-  , bars :: HNonEmpty f (TableList f, Default f Char)
+  , bars :: HNonEmpty f (TableList f, TableMaybe f)
  }
  deriving stock Generic
  deriving anyclass Rel8able
@ -86,14 +88,15 @@ data TableNonEmpty f = TableNonEmpty
 data S3Object = S3Object
  { bucketName :: Text
  , objectKey :: Text
-  } deriving stock Generic
+  }
+  deriving stock Generic


 deriving via HKDT S3Object
  instance x ~ HKD S3Object Expr => ToExprs x S3Object


-data HKDTest f = HKDTest
+newtype HKDTest f = HKDTest
  { s3Object :: Lift f S3Object
  } 
  deriving stock Generic
--- a/src/Rel8/Schema/HKD.hs
+++ b/src/Rel8/Schema/HKD.hs
@ -37,17 +37,17 @@ import GHC.TypeLits ( KnownSymbol )
 import Prelude

 -- higgledy
-import Data.Generic.HKD ( Construct, HKD( HKD, runHKD ), GHKD_, construct, deconstruct )
+import Data.Generic.HKD ( Construct, HKD(..), GHKD_, construct, deconstruct )

 -- rel8
 import Rel8.Aggregate ( Col(..), Aggregate )
 import Rel8.Expr ( Expr )
+import Rel8.Kind.Context ( Reifiable(..), SContext(..) )
 import Rel8.Schema.Context.Label
  ( Labelable
  , HLabelable, hlabeler, hunlabeler
  )
 import Rel8.Schema.Dict ( Dict( Dict ) )
-import Rel8.Schema.Field ( Reify, Reifiable(..), SContext(..), hunreify, hreify )
 import Rel8.Schema.HTable ( HTable )
 import Rel8.Schema.HTable.Label ( HLabel, hlabel, hunlabel )
 import Rel8.Schema.HTable.Product ( HProduct( HProduct ) )
@ -56,8 +56,12 @@ import Rel8.Schema.Insert ( Insert, Col(..) )
 import qualified Rel8.Schema.Kind as K
 import Rel8.Schema.Name ( Name(..) )
 import Rel8.Schema.Null ( Sql )
+import Rel8.Schema.Reify ( Reify, hreify, hunreify, NotReify, notReify )
 import Rel8.Schema.Result ( Result )
-import Rel8.Table ( Table, Columns, Context, fromColumns, toColumns )
+import Rel8.Table
+  ( Table, Columns, Context, fromColumns, toColumns
+  , Unreify, reify, unreify
+  )
 import Rel8.Table.Recontextualize ( Recontextualize )
 import Rel8.Table.Serialize ( FromExprs, ToExprs, fromResult, toResult )
 import Rel8.Type ( DBType )
@ -178,19 +182,27 @@ type family GColumns rep where
  GColumns (f :*: g) = HProduct (GColumns f) (GColumns g)


-instance (GTable (Rep a), Column1 context f, Labelable context) =>
-  Table context (HKD a f)
+instance
+  ( GTable (Rep a)
+  , Column1 context f
+  , Labelable context
+  , NotReify context
+  )
+  => Table context (HKD a f)
 where
  type Columns (HKD a f) = GRep a
  type Context (HKD a f) = Context1 f

  toColumns = toGColumns toColumn1 . runHKD
  fromColumns = HKD . fromGColumns fromColumn1
+  reify = notReify
+  unreify = notReify


 instance
  ( a ~ a'
  , GTable (Rep a)
+  , NotReify context, NotReify context'
  , Recontextualize1 context context' f f'
  , Column1 context f, Labelable context
  , Column1 context' f', Labelable context'
@ -227,9 +239,12 @@ instance
 where
  type Context (ALift context a) = Reify context
  type Columns (ALift context a) = GRep a
+  type Unreify (ALift context a) = Lift context a

  fromColumns = sfromColumnsLift contextSing
  toColumns = stoColumnsLift contextSing
+  reify _ = ALift
+  unreify _ (ALift a) = a


 instance
--- a/src/Rel8/Schema/HTable/Nullify.hs
+++ b/src/Rel8/Schema/HTable/Nullify.hs
@ -1,13 +1,13 @@
-{-# LANGUAGE DeriveAnyClass #-}
-{-# LANGUAGE DerivingStrategies #-}
-{-# LANGUAGE DeriveGeneric #-}
-{-# LANGUAGE NamedFieldPuns #-}
-{-# LANGUAGE LambdaCase #-}
 {-# language ConstraintKinds #-}
 {-# language DataKinds #-}
+{-# language DeriveAnyClass #-}
+{-# language DerivingStrategies #-}
+{-# language DeriveGeneric #-}
 {-# language FlexibleInstances #-}
 {-# language GADTs #-}
+{-# language LambdaCase #-}
 {-# language MultiParamTypeClasses #-}
+{-# language NamedFieldPuns #-}
 {-# language QuantifiedConstraints #-}
 {-# language RankNTypes #-}
 {-# language ScopedTypeVariables #-}
--- a/src/Rel8/Schema/Insert.hs
+++ b/src/Rel8/Schema/Insert.hs
@ -39,11 +39,15 @@ import Rel8.Schema.Context.Nullify
 import Rel8.Schema.HTable.Type ( HType( HType ) )
 import Rel8.Schema.Name ( Name, Selects )
 import Rel8.Schema.Null ( Sql )
+import Rel8.Schema.Reify ( notReify )
 import Rel8.Schema.Result ( Result )
 import Rel8.Schema.Spec ( SSpec(SSpec, nullity), Spec(Spec) )
 import Rel8.Schema.Table ( TableSchema )
 import Rel8.Statement.Returning ( Returning )
-import Rel8.Table ( Table(..) )
+import Rel8.Table
+  ( Table, Context, Columns, fromColumns, toColumns
+  , reify, unreify
+  )
 import Rel8.Table.Recontextualize ( Recontextualize )
 import Rel8.Table.Tag ( Tag(..), fromExpr )
 import Rel8.Type ( DBType )
@ -89,6 +93,8 @@ instance Sql DBType a => Table Insert (Insertion a) where

  toColumns (Insertion a) = HType (RequiredInsert a)
  fromColumns (HType (RequiredInsert a)) = Insertion a
+  reify = notReify
+  unreify = notReify


 instance Sql DBType a =>
--- a/src/Rel8/Schema/Name.hs
+++ b/src/Rel8/Schema/Name.hs
@ -31,8 +31,11 @@ import Rel8.Schema.Context ( Interpretation, Col )
 import Rel8.Schema.Context.Label ( Labelable, labeler, unlabeler )
 import Rel8.Schema.HTable.Type ( HType( HType ) )
 import Rel8.Schema.Null ( Sql )
+import Rel8.Schema.Reify ( notReify )
 import Rel8.Schema.Result ( Result )
-import Rel8.Table ( Table, Columns, Context, fromColumns, toColumns )
+import Rel8.Table
+  ( Table, Columns, Context, fromColumns, toColumns, reify, unreify
+  )
 import Rel8.Table.Recontextualize ( Recontextualize )
 import Rel8.Type ( DBType )

@ -59,6 +62,8 @@ instance Sql DBType a => Table Name (Name a) where

  toColumns (Name a) = HType (NameCol a)
  fromColumns (HType (NameCol a)) = Name a
+  reify = notReify
+  unreify = notReify


 instance Sql DBType a => Recontextualize Expr Name (Expr a) (Name a)
--- a/src/Rel8/Schema/Reify.hs
+++ b/src/Rel8/Schema/Reify.hs
@ -0,0 +1,75 @@
+{-# 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, hfield, htabulate )
+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 (Reify a) = Reify (labeler a)
+  unlabeler (Reify a) = Reify (unlabeler a)
+
+
+hreify :: HTable t => t (Col context) -> t (Col (Reify context))
+hreify a = htabulate $ \field -> Reify (hfield a field)
+
+
+hunreify :: HTable t => t (Col (Reify context)) -> t (Col context)
+hunreify a = htabulate $ \field -> case hfield a field of
+  Reify x -> x
+
+
+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 refl = case lemma @context of
+  Refl -> case refl of
+
+
+lemma :: NotReify context => IsReify context :~: 'False
+lemma = Refl
--- a/src/Rel8/Table.hs
+++ b/src/Rel8/Table.hs
@ -1,3 +1,4 @@
+{-# language AllowAmbiguousTypes #-}
 {-# language DataKinds #-}
 {-# language DefaultSignatures #-}
 {-# language DisambiguateRecordFields #-}
@ -14,9 +15,9 @@
 {-# language UndecidableInstances #-}

 module Rel8.Table
-  ( Table (Columns, Context, toColumns, fromColumns)
+  ( Table (Columns, Context, Unreify, toColumns, fromColumns, reify, unreify)
  , Congruent
-  , TTable, TColumns, TContext
+  , TTable, TColumns, TContext, TUnreify
  )
 where

@ -25,13 +26,16 @@ import Data.Functor ( ($>) )
 import Data.Functor.Identity ( Identity( Identity ) )
 import Data.Kind ( Constraint, Type )
 import Data.List.NonEmpty ( NonEmpty )
+import Data.Proxy ( Proxy( Proxy ) )
+import Data.Type.Equality ( (:~:)( Refl ) )
 import GHC.Generics ( Generic, Rep, from, to )
 import Prelude hiding ( null )

 -- rel8
 import Rel8.FCF ( Eval, Exp )
 import Rel8.Generic.Table
-  ( GTable, GColumns, GContext, fromGColumns, toGColumns
+  ( GTable, GColumns, GContext, GUnreify
+  , fromGColumns, toGColumns, greify, gunreify
  )
 import Rel8.Generic.Record ( Record(..) )
 import Rel8.Schema.Context ( Col(..) )
@ -49,6 +53,11 @@ import Rel8.Schema.HTable.Type ( HType( HType ) )
 import Rel8.Schema.HTable.Vectorize ( hvectorize, hunvectorize )
 import qualified Rel8.Schema.Kind as K
 import Rel8.Schema.Null ( Nullify, Nullity( Null, NotNull ), Sql )
+import Rel8.Schema.Reify
+  ( Reify, Col( Reify ), hreify, hunreify
+  , UnwrapReify
+  , notReify
+  )
 import Rel8.Schema.Result ( Result )
 import Rel8.Schema.Spec ( Spec( Spec ), SSpec(..), KnownSpec )
 import Rel8.Type ( DBType )
@ -78,18 +87,24 @@ class (HTable (Columns a), context ~ Context a) => Table context a | a -> contex
  -- | The common context that all columns use as an interpretation.
  type Context a :: K.Context

-  toColumns :: a -> Columns a (Col (Context a))
-  fromColumns :: Columns a (Col (Context a)) -> a
+  type Unreify a :: Type
+
+  toColumns :: a -> Columns a (Col context)
+  fromColumns :: Columns a (Col context) -> a
+
+  reify :: context :~: Reify ctx -> Unreify a -> a
+  unreify :: context :~: Reify ctx -> a -> Unreify a

  type Columns a = GColumns TColumns (Rep (Record a))
  type Context a = GContext TContext (Rep (Record a))
+  type Unreify a = DefaultUnreify a

  default toColumns ::
    ( Generic (Record a)
-    , GTable (TTable context) TColumns (Col (Context a)) (Rep (Record a))
+    , GTable (TTable context) TColumns (Col context) (Rep (Record a))
    , Columns a ~ GColumns TColumns (Rep (Record a))
    )
-    => a -> Columns a (Col (Context a))
+    => a -> Columns a (Col context)
  toColumns =
    toGColumns @(TTable context) @TColumns toColumns .
    from .
@ -97,15 +112,45 @@ class (HTable (Columns a), context ~ Context a) => Table context a | a -> contex

  default fromColumns ::
    ( Generic (Record a)
-    , GTable (TTable context) TColumns (Col (Context a)) (Rep (Record a))
+    , GTable (TTable context) TColumns (Col context) (Rep (Record a))
    , Columns a ~ GColumns TColumns (Rep (Record a))
    )
-    => Columns a (Col (Context a)) -> a
+    => Columns a (Col context) -> a
  fromColumns =
    unrecord .
    to .
    fromGColumns @(TTable context) @TColumns fromColumns

+  default reify ::
+    ( Generic (Record a)
+    , Generic (Record (Unreify a))
+    , GTable (TTable context) TColumns (Col context) (Rep (Record a))
+    , Rep (Record (Unreify a)) ~ GUnreify TUnreify (Rep (Record a))
+    )
+    => context :~: Reify ctx -> Unreify a -> a
+  reify Refl =
+    unrecord .
+    to .
+    greify @(TTable context) @TColumns @(Col context) (Proxy @TUnreify)
+      (reify Refl) .
+    from .
+    Record
+
+  default unreify ::
+    ( Generic (Record a)
+    , Generic (Record (Unreify a))
+    , GTable (TTable context) TColumns (Col context) (Rep (Record a))
+    , Rep (Record (Unreify a)) ~ GUnreify TUnreify (Rep (Record a))
+    )
+    => context :~: Reify ctx -> a -> Unreify a
+  unreify Refl =
+    unrecord .
+    to .
+    gunreify @(TTable context) @TColumns @(Col context) (Proxy @TUnreify)
+      (unreify Refl) .
+    from .
+    Record
+

 data TTable :: K.Context -> Type -> Exp Constraint
 type instance Eval (TTable context a) = Table context a
@ -119,23 +164,50 @@ data TContext :: Type -> Exp K.Context
 type instance Eval (TContext a) = Context a


+data TUnreify :: Type -> Exp Type
+type instance Eval (TUnreify a) = Unreify a
+
+
+type DefaultUnreify :: Type -> Type
+type family DefaultUnreify a where
+  DefaultUnreify (t a b c d e f g) =
+    t (Unreify a) (Unreify b) (Unreify c) (Unreify d) (Unreify e) (Unreify f) (Unreify g)
+  DefaultUnreify (t a b c d e f) =
+    t (Unreify a) (Unreify b) (Unreify c) (Unreify d) (Unreify e) (Unreify f)
+  DefaultUnreify (t a b c d e) =
+    t (Unreify a) (Unreify b) (Unreify c) (Unreify d) (Unreify e)
+  DefaultUnreify (t a b c d) =
+    t (Unreify a) (Unreify b) (Unreify c) (Unreify d)
+  DefaultUnreify (t a b c) = t (Unreify a) (Unreify b) (Unreify c)
+  DefaultUnreify (t a b) = t (Unreify a) (Unreify b)
+  DefaultUnreify (t a) = t (Unreify a)
+
+
 -- | Any 'HTable' is also a 'Table'.
 instance HTable t => Table context (t (Col context)) where
  type Columns (t (Col context)) = t
  type Context (t (Col context)) = context
+  type Unreify (t (Col context)) = t (Col (UnwrapReify context))

  toColumns = id
  fromColumns = id

+  reify Refl = hreify
+  unreify Refl = hunreify
+

 -- | Any context is trivially a table.
 instance KnownSpec spec => Table context (Col context spec) where
  type Columns (Col context spec) = HIdentity spec
  type Context (Col context spec) = context
+  type Unreify (Col context spec) = Col (UnwrapReify context) spec

  toColumns = HIdentity
  fromColumns = unHIdentity

+  reify Refl = Reify
+  unreify Refl (Reify a) = a
+

 instance Sql DBType a => Table Result (Identity a) where
  type Columns (Identity a) = HType a
@ -144,6 +216,9 @@ instance Sql DBType a => Table Result (Identity a) where
  toColumns (Identity a) = HType (Result a)
  fromColumns (HType (Result a)) = Identity a

+  reify = notReify
+  unreify = notReify
+

 instance (Table Result a, Table Result b) => Table Result (Either a b) where
  type Columns (Either a b) = HEitherTable (Columns a) (Columns b)
@ -168,6 +243,9 @@ instance (Table Result a, Table Result b) => Table Result (Either a b) where
    where
      err = error "Either.fromColumns: mismatch between tag and data"

+  reify = notReify
+  unreify = notReify
+

 instance Table Result a => Table Result [a] where
  type Columns [a] = HListTable (Columns a)
@ -176,6 +254,9 @@ instance Table Result a => Table Result [a] where
  toColumns = hvectorize vectorizer . fmap toColumns
  fromColumns = fmap fromColumns . hunvectorize unvectorizer

+  reify = notReify
+  unreify = notReify
+

 instance Table Result a => Table Result (Maybe a) where
  type Columns (Maybe a) = HMaybeTable (Columns a)
@ -197,6 +278,9 @@ instance Table Result a => Table Result (Maybe a) where
        Nothing -> error "Maybe.fromColumns: mismatch between tag and data"
        Just just -> fromColumns just

+  reify = notReify
+  unreify = notReify
+

 instance Table Result a => Table Result (NonEmpty a) where
  type Columns (NonEmpty a) = HNonEmptyTable (Columns a)
@ -205,6 +289,9 @@ instance Table Result a => Table Result (NonEmpty a) where
  toColumns = hvectorize vectorizer . fmap toColumns
  fromColumns = fmap fromColumns . hunvectorize unvectorizer

+  reify = notReify
+  unreify = notReify
+

 instance (Table Result a, Table Result b) => Table Result (These a b) where
  type Columns (These a b) = HTheseTable (Columns a) (Columns b)
@ -242,6 +329,9 @@ instance (Table Result a, Table Result b) => Table Result (These a b) where
        , hjust = hlabel labeler (hunlabel unlabeler hthere)
        }

+  reify = notReify
+  unreify = notReify
+

 instance (Table context a, Table context b, Labelable context)
  => Table context (a, b)
--- a/src/Rel8/Table/Either.hs
+++ b/src/Rel8/Table/Either.hs
@ -20,6 +20,7 @@ module Rel8.Table.Either
 where

 -- base
+import Control.Applicative ( liftA2 )
 import Data.Bifunctor ( Bifunctor, bimap )
 import Data.Functor.Identity ( runIdentity )
 import Data.Kind ( Type )
@ -46,7 +47,10 @@ import Rel8.Schema.HTable.Identity ( HIdentity(..) )
 import Rel8.Schema.HTable.Label ( hlabel, hunlabel )
 import Rel8.Schema.HTable.Nullify ( hnullify, hunnullify )
 import Rel8.Schema.Name ( Name )
-import Rel8.Table ( Table, Columns, Context, fromColumns, toColumns )
+import Rel8.Table
+  ( Table, Columns, Context, fromColumns, toColumns
+  , reify, unreify
+  )
 import Rel8.Table.Bool ( bool )
 import Rel8.Table.Eq ( EqTable, eqTable )
 import Rel8.Table.Ord ( OrdTable, ordTable )
@ -108,6 +112,8 @@ instance

  toColumns = toColumns2 toColumns toColumns
  fromColumns = fromColumns2 fromColumns fromColumns
+  reify = liftA2 bimap reify reify
+  unreify = liftA2 bimap unreify unreify


 instance
--- a/src/Rel8/Table/List.hs
+++ b/src/Rel8/Table/List.hs
@ -17,6 +17,7 @@ where
 -- base
 import Data.Functor.Identity ( Identity( Identity ) )
 import Data.Kind ( Type )
+import Data.Type.Equality ( (:~:)( Refl ) )
 import Prelude

 -- rel8
@ -28,7 +29,11 @@ import Rel8.Schema.HTable.Vectorize ( happend, hempty, hvectorize )
 import Rel8.Schema.Null ( Nullity( Null, NotNull ) )
 import Rel8.Schema.Spec ( SSpec(..) )
 import Rel8.Schema.Spec.ConstrainDBType ( dbTypeDict, dbTypeNullity )
-import Rel8.Table ( Table, Context, Columns, fromColumns, toColumns )
+import Rel8.Schema.Reify ( hreify, hunreify )
+import Rel8.Table
+  ( Table, Context, Columns, fromColumns, toColumns
+  , reify, unreify
+  )
 import Rel8.Table.Alternative
  ( AltTable, (<|>:)
  , AlternativeTable, emptyTable
@ -36,6 +41,7 @@ import Rel8.Table.Alternative
 import Rel8.Table.Eq ( EqTable, eqTable )
 import Rel8.Table.Ord ( OrdTable, ordTable )
 import Rel8.Table.Recontextualize ( Recontextualize )
+import Rel8.Table.Unreify ( Unreifiable )


 -- | A @ListTable@ value contains zero or more instances of @a@. You construct
@ -44,16 +50,24 @@ type ListTable :: Type -> Type
 newtype ListTable a = ListTable (HListTable (Columns a) (Col (Context a)))


-instance Table context a => Table context (ListTable a) where
+instance (Table context a, Unreifiable context a) =>
+  Table context (ListTable a)
+ where
  type Columns (ListTable a) = HListTable (Columns a)
  type Context (ListTable a) = Context a

  fromColumns = ListTable
  toColumns (ListTable a) = a

+  reify Refl (ListTable a) = ListTable (hreify a)
+  unreify Refl (ListTable a) = ListTable (hunreify a)

-instance Recontextualize from to a b =>
-  Recontextualize from to (ListTable a) (ListTable b)
+
+instance
+  ( Unreifiable from a, Unreifiable to b
+  , Recontextualize from to a b
+  )
+  => Recontextualize from to (ListTable a) (ListTable b)


 instance EqTable a => EqTable (ListTable a) where
--- a/src/Rel8/Table/Maybe.hs
+++ b/src/Rel8/Table/Maybe.hs
@ -48,7 +48,10 @@ import Rel8.Schema.HTable.Maybe ( HMaybeTable(..) )
 import Rel8.Schema.HTable.Nullify ( hnullify, hunnullify )
 import Rel8.Schema.Name ( Name )
 import Rel8.Schema.Null ( Nullify, Nullity( Null, NotNull ), Sql, nullable )
-import Rel8.Table ( Table, Columns, Context, fromColumns, toColumns )
+import Rel8.Table
+  ( Table, Columns, Context, fromColumns, toColumns
+  , reify, unreify
+  )
 import Rel8.Table.Alternative
  ( AltTable, (<|>:)
  , AlternativeTable, emptyTable
@ -139,13 +142,16 @@ instance

  toColumns = toColumns1 toColumns
  fromColumns = fromColumns1 fromColumns
+  reify = fmap fmap reify
+  unreify = fmap fmap unreify


 instance
  ( Labelable from, Nullifiable from, ConstrainTag from MaybeTag
  , Labelable to, Nullifiable to, ConstrainTag to MaybeTag
  , Recontextualize from to a b
-  ) => Recontextualize from to (MaybeTable a) (MaybeTable b)
+  )
+  => Recontextualize from to (MaybeTable a) (MaybeTable b)


 instance EqTable a => EqTable (MaybeTable a) where
--- a/src/Rel8/Table/NonEmpty.hs
+++ b/src/Rel8/Table/NonEmpty.hs
@ -1,7 +1,9 @@
+{-# language DataKinds #-}
 {-# language FlexibleContexts #-}
 {-# language FlexibleInstances #-}
 {-# language MultiParamTypeClasses #-}
 {-# language NamedFieldPuns #-}
+{-# language QuantifiedConstraints #-}
 {-# language ScopedTypeVariables #-}
 {-# language StandaloneKindSignatures #-}
 {-# language TypeApplications #-}
@ -19,6 +21,7 @@ where
 import Data.Functor.Identity ( Identity( Identity ) )
 import Data.Kind ( Type )
 import Data.List.NonEmpty ( NonEmpty )
+import Data.Type.Equality ( (:~:)( Refl ) )
 import Prelude

 -- rel8
@ -28,13 +31,18 @@ import Rel8.Schema.Dict ( Dict( Dict ) )
 import Rel8.Schema.HTable.NonEmpty ( HNonEmptyTable )
 import Rel8.Schema.HTable.Vectorize ( happend, hvectorize )
 import Rel8.Schema.Null ( Nullity( Null, NotNull ) )
+import Rel8.Schema.Reify ( hreify, hunreify )
 import Rel8.Schema.Spec ( SSpec(..) )
 import Rel8.Schema.Spec.ConstrainDBType ( dbTypeDict, dbTypeNullity )
-import Rel8.Table ( Table, Context, Columns, fromColumns, toColumns )
+import Rel8.Table
+  ( Table, Context, Columns, fromColumns, toColumns
+  , reify, unreify
+  )
 import Rel8.Table.Alternative ( AltTable, (<|>:) )
 import Rel8.Table.Eq ( EqTable, eqTable )
 import Rel8.Table.Ord ( OrdTable, ordTable )
 import Rel8.Table.Recontextualize ( Recontextualize )
+import Rel8.Table.Unreify ( Unreifiable )


 -- | A @NonEmptyTable@ value contains one or more instances of @a@. You
@ -44,16 +52,24 @@ newtype NonEmptyTable a =
  NonEmptyTable (HNonEmptyTable (Columns a) (Col (Context a)))


-instance Table context a => Table context (NonEmptyTable a) where
+instance (Table context a, Unreifiable context a) =>
+  Table context (NonEmptyTable a)
+ where
  type Columns (NonEmptyTable a) = HNonEmptyTable (Columns a)
  type Context (NonEmptyTable a) = Context a

  fromColumns = NonEmptyTable
  toColumns (NonEmptyTable a) = a

+  reify Refl (NonEmptyTable a) = NonEmptyTable (hreify a)
+  unreify Refl (NonEmptyTable a) = NonEmptyTable (hunreify a)

-instance Recontextualize from to a b =>
-  Recontextualize from to (NonEmptyTable a) (NonEmptyTable b)
+
+instance
+  ( Unreifiable from a, Unreifiable to b
+  , Recontextualize from to a b
+  )
+  => Recontextualize from to (NonEmptyTable a) (NonEmptyTable b)


 instance EqTable a => EqTable (NonEmptyTable a) where
--- a/src/Rel8/Table/These.hs
+++ b/src/Rel8/Table/These.hs
@ -24,6 +24,7 @@ module Rel8.Table.These
 where

 -- base
+import Control.Applicative ( liftA2 )
 import Data.Bifunctor ( Bifunctor, bimap )
 import Data.Functor.Identity ( runIdentity )
 import Data.Kind ( Type )
@ -49,8 +50,11 @@ import Rel8.Schema.HTable.Label ( hlabel, hunlabel )
 import Rel8.Schema.HTable.Identity ( HIdentity(..) )
 import Rel8.Schema.HTable.Nullify ( hnullify, hunnullify )
 import Rel8.Schema.HTable.These ( HTheseTable(..) )
-import Rel8.Schema.Name ( Name  )
-import Rel8.Table ( Table, Columns, Context, fromColumns, toColumns )
+import Rel8.Schema.Name ( Name )
+import Rel8.Table
+  ( Table, Columns, Context, fromColumns, toColumns
+  , reify, unreify
+  )
 import Rel8.Table.Eq ( EqTable, eqTable )
 import Rel8.Table.Maybe
  ( MaybeTable(..)
@ -128,6 +132,8 @@ instance

  toColumns = toColumns2 toColumns toColumns
  fromColumns = fromColumns2 fromColumns fromColumns
+  reify = liftA2 bimap reify reify
+  unreify = liftA2 bimap unreify unreify


 instance
--- a/src/Rel8/Table/Unreify.hs
+++ b/src/Rel8/Table/Unreify.hs
@ -0,0 +1,43 @@
+{-# language DataKinds #-}
+{-# language StandaloneKindSignatures #-}
+{-# language TypeFamilies #-}
+{-# language UndecidableInstances #-}
+
+-- | This module implements some machinery for implementing methods of the
+-- 'Table' class for a particular special (but important) class of polymorphic
+-- @Table@ types.
+--
+-- This special case is characterised by a @newtype@ wrapper around a bare
+-- 'HTable' which is constructed by applying a type family to the polymorphic
+-- type variable.
+--
+-- Examples of this class of @Table@ include @ListTable@ and @NonEmptyTable@.
+--
+-- The tricky part about implementing @Table@ for these types is 'reify' and
+-- 'unreify'. There is no guarantee in general that @'Unreify' a@ is itself
+-- a @Table@, let alone a @Table@ with the same 'Columns' as @a@
+-- (e.g., @Unreify (AColumn Result Bool) = Bool@, and @Bool@ is not a
+-- @Table@)
+
+module Rel8.Table.Unreify
+  ( Unreifiable
+  )
+where
+
+-- base
+import Data.Kind ( Constraint, Type )
+import Prelude ()
+
+-- rel8
+import qualified Rel8.Schema.Kind as K
+import Rel8.Schema.Reify ( Reify )
+import Rel8.Table ( Table, Columns, Unreify )
+
+
+type Unreifiable :: K.Context -> Type -> Constraint
+type family Unreifiable context a where
+  Unreifiable (Reify context) a =
+    ( Table context (Unreify a)
+    , Columns a ~ Columns (Unreify a)
+    )
+  Unreifiable _ _ = ()