From 064001d67bd3bcf0059b892dbc91a1043a653773 Mon Sep 17 00:00:00 2001
From: Oliver Charles <ollie@ocharles.org.uk>
Date: Fri, 24 Jan 2020 10:28:07 +0000
Subject: [PATCH] New 'Recontextualise' approach

---
 src/Rel8.hs                   |   1 +
 src/Rel8/Aggregate.hs         |  43 +++--
 src/Rel8/Column.hs            |  33 +++-
 src/Rel8/EqTable.hs           |   4 +-
 src/Rel8/Expr.hs              |  24 ++-
 src/Rel8/FromRow.hs           |  15 +-
 src/Rel8/HigherKindedTable.hs | 288 ++++++++++++++++++++++++++++++++++
 src/Rel8/MonadQuery.hs        |   2 +
 8 files changed, 376 insertions(+), 34 deletions(-)
 create mode 100644 src/Rel8/HigherKindedTable.hs

diff --git a/src/Rel8.hs b/src/Rel8.hs
index 0d979f9..fae0158 100644
--- a/src/Rel8.hs
+++ b/src/Rel8.hs
@@ -109,6 +109,7 @@ import Rel8.DBEq
 import Rel8.EqTable
 import Rel8.Expr
 import Rel8.FromRow
+import Rel8.HigherKindedTable
 import Rel8.MaybeTable
 import Rel8.MonadQuery
 import Rel8.Query
diff --git a/src/Rel8/Aggregate.hs b/src/Rel8/Aggregate.hs
index aecd8fa..012a9f0 100644
--- a/src/Rel8/Aggregate.hs
+++ b/src/Rel8/Aggregate.hs
@@ -9,6 +9,7 @@
 {-# language TypeApplications #-}
 {-# language TypeFamilies #-}
 {-# language UndecidableInstances #-}
+{-# language UndecidableSuperClasses #-}
 
 module Rel8.Aggregate
   ( aggregateExpr
@@ -30,10 +31,12 @@ import qualified Opaleye.Internal.PackMap as Opaleye
 import Rel8.Column
 import Rel8.EqTable
 import Rel8.Expr
+import Rel8.HigherKindedTable
 import Rel8.MonadQuery
 import Rel8.Nest
 import Rel8.SimpleConstraints
 import Rel8.Table
+import Rel8.Unconstrained
 
 
 {-| @groupAndAggregate@ is the fundamental aggregation operator in Rel8. Like
@@ -85,6 +88,11 @@ groupAndAggregate
      , EqTable k
      , Promote m k' k
      , Promote m v' v
+     , MapContext Demote k ~ k'
+     , MapContext Demote v ~ v'
+     , Recontextualise k Demote
+     , Recontextualise v Demote
+     , Recontextualise k Id
      )
   => ( a -> GroupBy k v ) -> Nest m a -> m ( k', v' )
 groupAndAggregate = groupAndAggregate_forAll
@@ -94,13 +102,17 @@ groupAndAggregate_forAll
   :: forall a k k' v v' m
    . ( MonadQuery m
      , MonoidTable v
+     , Recontextualise k Demote
+     , Recontextualise v Demote
      , EqTable k
      , Context k ~ Expr ( Nest m )
+     , MapContext Demote k ~ k'
+     , MapContext Demote v ~ v'
      , Context k' ~ Context v'
      , Context v ~ Expr ( Nest m )
      , Context v' ~ Expr m
-     , CompatibleTables k' k
-     , CompatibleTables v' v
+     , Table k
+     , Recontextualise k Id
      )
   => ( a -> GroupBy k v ) -> Nest m a -> m ( k', v' )
 groupAndAggregate_forAll f query =
@@ -122,10 +134,12 @@ groupAndAggregate_forAll f query =
 -- where there is only one group.
 aggregate
   :: ( MonadQuery m
+     , MapContext Demote b ~ b'
      , MonoidTable b
+     , Table b
+     , Recontextualise b Demote
+     , Context b ~ Expr ( Nest m )
      , Context b' ~ Expr m
-     , Context b ~ Expr ( Nest m)
-     , CompatibleTables b' b
      )
   => ( a -> b ) -> Nest m a -> m b'
 aggregate = aggregate_forAll
@@ -134,10 +148,11 @@ aggregate = aggregate_forAll
 aggregate_forAll
   :: forall a b b' m
    . ( MonadQuery m
+     , MapContext Demote b ~ b'
      , MonoidTable b
+     , Recontextualise b Demote
      , Context b' ~ Expr m
      , Context b ~ Expr ( Nest m )
-     , CompatibleTables b' b
      )
   => ( a -> b ) -> Nest m a -> m b'
 aggregate_forAll f =
@@ -147,22 +162,23 @@ aggregate_forAll f =
 
     to :: b -> b'
     to =
-      mapTable ( mapC demote )
+      mapTable @Demote ( mapC demote )
 
 
 -- | The class of tables that can be aggregated. This is like Haskell's 'Monoid'
 -- type.
-class MonoidTable a where
+class Table a => MonoidTable a where
   -- | How to aggregate an entire table.
   aggregator :: Opaleye.Aggregator a a
 
 
 -- | Higher-kinded records can be used a monoidal aggregations if all fields
 -- are instances of 'DBMonoid'.
-instance ConstrainedTable ( t ( Expr m ) ) DBMonoid => MonoidTable ( t ( Expr m ) ) where
+instance ( HConstrainTable t ( Expr m ) Unconstrained, HigherKindedTable t, ConstrainTable ( t ( Expr m ) ) DBMonoid ) => MonoidTable ( t ( Expr m ) ) where
   aggregator =
     Opaleye.Aggregator $ Opaleye.PackMap \f ->
       traverseTableC
+        @Id
         @DBMonoid
         ( traverseCC @DBMonoid ( Opaleye.runAggregator aggregateExpr f ) )
 
@@ -229,13 +245,12 @@ instance ( Table k, Table v, Context k ~ Context v ) => Table ( GroupBy k v ) wh
       <*> tabulateMCP proxy ( f . ValueFields )
 
 
-instance ( Compatible k f k' g, Compatible v f v' g, Context k ~ Context v, Context k' ~ Context v' ) => Compatible ( GroupBy k v ) f ( GroupBy k' v' ) g where
-  transferField = \case
-    KeyFields i -> KeyFields ( transferField i )
-    ValueFields i -> ValueFields ( transferField i )
+instance ( Context v ~ Expr m, Context k ~ Context v, Context ( MapContext f k ) ~ Context ( MapContext f v ), Recontextualise k f, Recontextualise v f ) => Recontextualise ( GroupBy k v ) f where
+  type MapContext f ( GroupBy k v ) =
+    GroupBy ( MapContext f k ) ( MapContext f v )
 
 
-instance ( ConstrainedTable k Unconstrained, Context k ~ Expr m, MonoidTable v ) => MonoidTable ( GroupBy k v ) where
+instance ( Recontextualise k Id, Context v ~ Expr m, Table k, Context k ~ Expr m, MonoidTable v ) => MonoidTable ( GroupBy k v ) where
   aggregator =
     GroupBy
       <$> lmap key group
@@ -246,4 +261,4 @@ instance ( ConstrainedTable k Unconstrained, Context k ~ Expr m, MonoidTable v )
       group :: Opaleye.Aggregator k k
       group =
         Opaleye.Aggregator $ Opaleye.PackMap \f ->
-          traverseTable ( traverseC \x -> fromPrimExpr <$> f ( Nothing, toPrimExpr x ) )
+          traverseTable @Id ( traverseC \x -> fromPrimExpr <$> f ( Nothing, toPrimExpr x ) )
diff --git a/src/Rel8/Column.hs b/src/Rel8/Column.hs
index 788c153..04f146b 100644
--- a/src/Rel8/Column.hs
+++ b/src/Rel8/Column.hs
@@ -16,6 +16,12 @@ module Rel8.Column
   , zipCWithM
   , zipCWithMC
   , Null
+  , Id
+  , Select
+  , From
+  , Demote
+  , Structure
+  , Lit
   ) where
 
 import Data.Functor.Identity
@@ -25,6 +31,24 @@ import Data.Kind
 data Null ( f :: * -> * ) a
 
 
+data Id ( f :: * -> * ) a
+
+
+data From ( m :: * -> * ) ( f :: * -> * ) a
+
+
+data Select ( f :: * -> * ) a
+
+
+data Demote ( f :: * -> * ) a
+
+
+data Structure ( f :: * -> * ) a
+
+
+data Lit ( f :: * -> * ) a
+
+
 {-| The @Column@ type family should be used to indicate which fields of your
 data types are single columns in queries. This type family has special
 support when a query is executed, allowing you to use a single data type for
@@ -57,12 +81,17 @@ In @rel8@ we try hard to always know roughly what @f@ is, which means typed
 holes should mention precise types, rather than the @Column@ type family. You
 should only need to be aware of the type family when defining your table types.
 -}
-type family Column ( f :: Type -> Type ) ( a :: Type ) :: Type where
-  Column ( Null f ) a = Column f ( Maybe a )
+type family Column ( context :: Type -> Type ) ( a :: Type ) :: Type where
+  Column ( Null f ) a = Column f ( Maybe ( DropMaybe a ) )
   Column Identity a = a
   Column f a = f a
 
 
+type family DropMaybe ( a :: Type ) :: Type where
+  DropMaybe ( Maybe a ) = DropMaybe a
+  DropMaybe a = a
+
+
 -- | The @C@ newtype simply wraps 'Column', but this allows us to work
 -- injectivity problems of functions that return type family applications
 -- (for example, 'Rel8.HigherKinded.zipRecord').
diff --git a/src/Rel8/EqTable.hs b/src/Rel8/EqTable.hs
index 3339128..3f51882 100644
--- a/src/Rel8/EqTable.hs
+++ b/src/Rel8/EqTable.hs
@@ -11,7 +11,9 @@ import Control.Applicative
 import Rel8.Column
 import Rel8.DBEq
 import Rel8.Expr
+import Rel8.HigherKindedTable
 import Rel8.Table
+import Rel8.Unconstrained
 
 
 -- | The class of database tables (containing one or more columns) that can be
@@ -44,7 +46,7 @@ instance DBEq a => EqTable ( Expr m a ) where
 
 -- | Higher-kinded records can be compared for equality. Two records are equal
 -- if all of their fields are equal.
-instance ConstrainedTable ( t ( Expr m ) ) DBEq => EqTable ( t ( Expr m ) ) where
+instance ( HigherKindedTable t, HConstrainTable t ( Expr m ) Unconstrained, ConstrainTable ( t ( Expr m ) ) DBEq ) => EqTable ( t ( Expr m ) ) where
   l ==. r =
     and_
       ( getConst
diff --git a/src/Rel8/Expr.hs b/src/Rel8/Expr.hs
index aef7b03..7df4f2b 100644
--- a/src/Rel8/Expr.hs
+++ b/src/Rel8/Expr.hs
@@ -53,6 +53,11 @@ import Rel8.Nest
 import Rel8.Table
 
 
+instance ContextMap Null ( Expr m ) where
+  recontextualiseColumn ( MkC ( Expr x ) ) =
+    MkC ( Expr x )
+
+
 -- | Typed SQL expressions
 newtype Expr ( m :: Type -> Type ) ( a :: Type ) =
   Expr { toPrimExpr :: Opaleye.PrimExpr }
@@ -109,12 +114,14 @@ class DBType ( a :: Type ) where
 
 
 litTable
-  :: ( Compatible b ( Expr m ) a Identity
-     , ConstrainedTable a DBType
-     , ConstrainedTable b DBType
-     ) => a -> b
+  :: ( ConstrainTable ( MapContext Lit a ) DBType
+     , Recontextualise a Lit
+     , Context ( MapContext Lit a ) ~ Expr m
+     , Context a ~ Identity
+     )
+  => a -> MapContext Lit a
 litTable =
-  mapTableC @DBType ( mapCC @DBType lit )
+  mapTableC @DBType @Lit ( mapCC @DBType lit )
 
 
 -- | Corresponds to the @bool@ PostgreSQL type.
@@ -286,9 +293,10 @@ instance Table ( Expr m a ) where
     toColumn <$> f ExprField
 
 
-instance ( a ~ b, Expr m ~ m', Expr n ~ n' ) => Compatible ( Expr m a ) m' ( Expr n b ) n' where
-  transferField ExprField =
-    ExprField
+instance Recontextualise ( Expr m a ) Id where
+  type MapContext Id ( Expr m a ) = Expr m a
+  fieldMapping ExprField = ExprField
+  reverseFieldMapping ExprField = ExprField
 
 
 binExpr :: Opaleye.BinOp -> Expr m a -> Expr m a -> Expr m b
diff --git a/src/Rel8/FromRow.hs b/src/Rel8/FromRow.hs
index 3caecb5..8cc42b2 100644
--- a/src/Rel8/FromRow.hs
+++ b/src/Rel8/FromRow.hs
@@ -9,14 +9,16 @@
 
 module Rel8.FromRow where
 
-import Data.Int
 import Data.Functor.Identity
+import Data.Int
 import Database.PostgreSQL.Simple.FromField ( FromField )
 import Database.PostgreSQL.Simple.FromRow ( RowParser, field )
 import Rel8.Column
 import Rel8.Expr
+import Rel8.HigherKindedTable
 import Rel8.Query
-import Rel8.Table ( Context, Table, ConstrainedTable, traverseTableC )
+import Rel8.Table hiding ( field )
+import Rel8.Unconstrained
 
 
 -- | @FromRow@ witnesses the one-to-one correspondence between the type @sql@,
@@ -26,16 +28,11 @@ class ( Context sql ~ Expr Query, Table sql ) => FromRow sql haskell | sql -> ha
   rowParser :: sql -> RowParser haskell
 
 
-instance ( Context ( sqlA, sqlB ) ~ Expr Query, FromRow sqlA haskellA, FromRow sqlB haskellB ) => FromRow ( sqlA, sqlB ) ( haskellA, haskellB ) where
-  rowParser ( a, b ) =
-    (,) <$> rowParser a <*> rowParser b
-
-
 -- | Any higher-kinded records can be @SELECT@ed, as long as we know how to
 -- decode all of the records constituent part's.
-instance ( ConstrainedTable ( t identity ) FromField, Table ( t expr ), expr ~ Expr Query, identity ~ Identity ) => FromRow ( t expr ) ( t identity ) where
+instance ( HConstrainTable t Identity FromField, HConstrainTable t Identity Unconstrained, HigherKindedTable t, Table ( t expr ), expr ~ Expr Query, identity ~ Identity ) => FromRow ( t expr ) ( t identity ) where
   rowParser =
-    traverseTableC @FromField ( traverseCC @FromField \_ -> field )
+    traverseTableC @Select @FromField ( traverseCC @FromField \_ -> field )
 
 
 instance m ~ Query => FromRow ( Expr m Int32 ) Int32 where
diff --git a/src/Rel8/HigherKindedTable.hs b/src/Rel8/HigherKindedTable.hs
new file mode 100644
index 0000000..21556d0
--- /dev/null
+++ b/src/Rel8/HigherKindedTable.hs
@@ -0,0 +1,288 @@
+{-# language AllowAmbiguousTypes #-}
+{-# language BlockArguments #-}
+{-# language ConstraintKinds #-}
+{-# language DataKinds #-}
+{-# language DefaultSignatures #-}
+{-# language FlexibleContexts #-}
+{-# language FlexibleInstances #-}
+{-# language GADTs #-}
+{-# language KindSignatures #-}
+{-# language LambdaCase #-}
+{-# language MultiParamTypeClasses #-}
+{-# language RankNTypes #-}
+{-# language ScopedTypeVariables #-}
+{-# language TypeApplications #-}
+{-# language TypeFamilyDependencies #-}
+{-# language TypeOperators #-}
+{-# language UndecidableInstances #-}
+
+{-# options -fno-warn-orphans #-}
+
+module Rel8.HigherKindedTable where
+
+import Data.Functor.Identity
+import Data.Kind
+import GHC.Generics hiding ( C )
+import Rel8.Column
+import Rel8.ColumnSchema
+import Rel8.Expr
+import Rel8.Nest
+import Rel8.Query
+import Rel8.Table
+import Rel8.Unconstrained
+
+
+{-| Higher-kinded data types.
+
+Higher-kinded data types are data types of the pattern:
+
+@
+data MyType f =
+  MyType { field1 :: Column f T1 OR HK1 f
+         , field2 :: Column f T2 OR HK2 f
+         , ...
+         , fieldN :: Column f Tn OR HKn f
+         }
+@
+
+where @Tn@ is any Haskell type, and @HKn@ is any higher-kinded type.
+
+That is, higher-kinded data are records where all fields in the record
+are all either of the type @Column f T@ (for any @T@), or are themselves
+higher-kinded data:
+
+[Nested]
+
+@
+data Nested f =
+  Nested { nested1 :: MyType f
+         , nested2 :: MyType f
+         }
+@
+
+The @HigherKindedTable@ type class is used to give us a special mapping
+operation that lets us change the type parameter @f@.
+
+[Supplying @HigherKindedTable@ instances]
+
+This type class should be derived generically for all table types in your
+project. To do this, enable the @DeriveAnyType@ and @DeriveGeneric@ language
+extensions:
+
+@
+\{\-\# LANGUAGE DeriveAnyClass, DeriveGeneric #-\}
+import qualified GHC.Generics
+
+data MyType f = MyType { fieldA :: Column f T }
+  deriving ( GHC.Generics.Generic, HigherKindedTable )
+@
+
+-}
+class HigherKindedTable ( t :: ( Type -> Type ) -> Type ) where
+  -- | Like 'Field', but for higher-kinded tables.
+  type HField t = ( field :: Type -> Type ) | field -> t
+  type HField t =
+    GenericField t
+
+  -- | Like 'Constraintable', but for higher-kinded tables.
+  type HConstrainTable t ( f :: Type -> Type ) ( c :: Type -> Constraint ) :: Constraint
+  type HConstrainTable t f c =
+    GHConstrainTable ( Rep ( t f ) ) ( Rep ( t Spine ) ) c
+
+  -- | Like 'field', but for higher-kinded tables.
+  hfield :: t f -> HField t x -> C f x
+  default hfield
+    :: forall f x
+     . ( Generic ( t f )
+       , HField t ~ GenericField t
+       , GHigherKindedTable ( Rep ( t f ) ) t f ( Rep ( t Spine ) )
+       )
+    => t f -> HField t x -> C f x
+  hfield x ( GenericField i ) =
+    ghfield @( Rep ( t f ) ) @t @f @( Rep ( t Spine ) ) ( from x ) i
+
+  -- | Like 'tabulateMCP', but for higher-kinded tables.
+  htabulate
+    :: ( Applicative m, HConstrainTable t f c )
+    => proxy c -> ( forall x. c x => HField t x -> m ( C f x ) ) -> m ( t f )
+
+  default htabulate
+    :: forall f m c proxy
+     . ( Applicative m, GHConstrainTable ( Rep ( t f ) ) ( Rep ( t Spine ) ) c, Generic ( t f )
+       , GHigherKindedTable ( Rep ( t f ) ) t f ( Rep ( t Spine ) )
+       , HField t ~ GenericField t
+       )
+    => proxy c -> ( forall x. c x => HField t x -> m ( C f x ) ) -> m ( t f )
+  htabulate proxy f =
+    fmap to ( ghtabulate @( Rep ( t f ) ) @t @f @( Rep ( t Spine ) ) proxy ( f . GenericField ) )
+
+
+
+data TableHField t ( f :: Type -> Type ) x where
+  F :: HField t x -> TableHField t f x
+
+
+-- | Any 'HigherKindedTable' is also a 'Table'.
+instance ( ConstrainTable ( t f ) Unconstrained, HigherKindedTable t ) => Table ( t f ) where
+  type Field ( t f ) =
+    TableHField t f
+
+  type Context ( t f ) =
+    f
+
+  type ConstrainTable ( t f ) c =
+    HConstrainTable t f c
+
+  tabulateMCP proxy f =
+    htabulate proxy \x -> f ( F x )
+
+  field x ( F i ) =
+    hfield x i
+
+
+instance ( HigherKindedTable t, HConstrainTable t f Unconstrained ) => Recontextualise ( t f ) Id where
+  type MapContext Id ( t f ) = t f
+  fieldMapping ( F i ) = F i
+  reverseFieldMapping ( F i ) = F i
+
+
+instance ( HConstrainTable t ColumnSchema Unconstrained, HigherKindedTable t, HConstrainTable t ( Expr m ) Unconstrained ) => Recontextualise ( t ColumnSchema ) ( From m ) where
+  type MapContext ( From m ) ( t ColumnSchema ) = t ( Expr m )
+  fieldMapping ( F i ) = F i
+  reverseFieldMapping ( F i ) = F i
+
+
+instance ( HConstrainTable t ( Null ( Expr m ) ) Unconstrained, HigherKindedTable t, HConstrainTable t ( Expr m ) Unconstrained ) => Recontextualise ( t ( Expr m ) ) Null where
+  type MapContext Null ( t ( Expr m ) ) = t ( Null ( Expr m ) )
+  fieldMapping ( F i ) = F i
+  reverseFieldMapping ( F i ) = F i
+
+
+instance ( HConstrainTable t ( Expr ( Nest m ) ) Unconstrained, HigherKindedTable t, HConstrainTable t ( Expr m ) Unconstrained ) => Recontextualise ( t ( Expr ( Nest m ) ) ) Demote where
+  type MapContext Demote ( t ( Expr ( Nest m ) ) ) = t ( Expr m )
+  fieldMapping ( F i ) = F i
+  reverseFieldMapping ( F i ) = F i
+
+
+instance ( HigherKindedTable t, HConstrainTable t f Unconstrained, HConstrainTable t Spine Unconstrained ) => Recontextualise ( t f ) Structure where
+  type MapContext Structure ( t f ) = t Spine
+  fieldMapping ( F i ) = F i
+  reverseFieldMapping ( F i ) = F i
+
+
+instance ( HConstrainTable t Identity Unconstrained, HigherKindedTable t, HConstrainTable t ( Expr Query ) Unconstrained, HConstrainTable t ( Expr Query ) Unconstrained ) => Recontextualise ( t ( Expr Query) ) Select where
+  type MapContext Select ( t ( Expr Query ) ) = t Identity
+  fieldMapping ( F i ) = F i
+  reverseFieldMapping ( F i ) = F i
+
+
+data GenericField t a where
+  GenericField :: GHField t ( Rep ( t Spine ) ) a -> GenericField t a
+
+
+class GHigherKindedTable ( rep :: Type -> Type ) ( t :: ( Type -> Type ) -> Type ) ( f :: Type -> Type ) ( repIdentity :: Type -> Type ) where
+  data GHField t repIdentity :: Type -> Type
+
+  type GHConstrainTable rep repIdentity ( c :: Type -> Constraint ) :: Constraint
+
+  ghfield :: rep a -> GHField t repIdentity x -> C f x
+
+  ghtabulate
+    :: ( Applicative m, GHConstrainTable rep repIdentity c )
+    => proxy c
+    -> ( forall x. c x => GHField t repIdentity x -> m ( C f x ) )
+    -> m ( rep a )
+
+
+instance GHigherKindedTable x t f x' => GHigherKindedTable ( M1 i c x ) t f ( M1 i' c' x' ) where
+  data GHField t ( M1 i' c' x' ) a where
+    M1Field :: GHField t x' a -> GHField t ( M1 i' c' x' ) a
+
+  type GHConstrainTable ( M1 i c x ) ( M1 i' c' x' ) constraint =
+    GHConstrainTable x x' constraint
+
+  ghfield ( M1 a ) ( M1Field i ) =
+    ghfield a i
+
+  ghtabulate proxy f =
+    M1 <$> ghtabulate @x @t @f @x' proxy ( f . M1Field )
+
+
+instance ( GHigherKindedTable x t f x', GHigherKindedTable y t f y' ) => GHigherKindedTable ( x :*: y ) t f ( x' :*: y' ) where
+  data GHField t ( x' :*: y' ) a where
+    FieldL :: GHField t x' a -> GHField t ( x' :*: y' ) a
+    FieldR :: GHField t y' a -> GHField t ( x' :*: y' ) a
+
+  type GHConstrainTable ( x :*: y ) ( x' :*: y' ) constraint =
+    ( GHConstrainTable x x' constraint, GHConstrainTable y y' constraint )
+
+  ghfield ( x :*: y ) = \case
+    FieldL i -> ghfield x i
+    FieldR i -> ghfield y i
+
+  ghtabulate proxy f =
+    (:*:) <$> ghtabulate @x @t @f @x' proxy ( f . FieldL )
+          <*> ghtabulate @y @t @f @y' proxy ( f . FieldR )
+
+
+type family IsColumnApplication ( a :: Type ) :: Bool where
+  IsColumnApplication ( Spine a ) = 'True
+  IsColumnApplication _ = 'False
+
+
+
+instance DispatchK1 ( IsColumnApplication c' ) f c c' => GHigherKindedTable ( K1 i c ) t f ( K1 i' c' ) where
+  data GHField t ( K1 i' c' ) a where
+    K1Field :: K1Field ( IsColumnApplication c' ) c' x -> GHField t ( K1 i' c' ) x
+
+  type GHConstrainTable ( K1 i c ) ( K1 i' c' ) constraint =
+    ConstrainK1 ( IsColumnApplication c' ) c c' constraint
+
+  ghfield ( K1 a ) ( K1Field i ) =
+    k1field @( IsColumnApplication c' ) @f @c @c' a i
+
+  ghtabulate proxy f =
+    K1 <$> k1tabulate @( IsColumnApplication c' ) @f @c @c' proxy ( f . K1Field )
+
+
+class DispatchK1 ( isSpine :: Bool ) f a a' where
+  data K1Field isSpine a' :: Type -> Type
+
+  type ConstrainK1 isSpine a a' ( c :: Type -> Constraint ) :: Constraint
+
+  k1field :: a -> K1Field isSpine a' x -> C f x
+
+  k1tabulate
+    :: ( ConstrainK1 isSpine a a' c, Applicative m )
+    => proxy c -> ( forall x. c x => K1Field isSpine a' x -> m ( C f x ) ) -> m a
+
+
+instance a ~ Column f b => DispatchK1 'True f a ( Spine b ) where
+  data K1Field 'True ( Spine b ) x where
+    K1True :: K1Field 'True ( Spine b ) b
+
+  type ConstrainK1 'True a ( Spine b ) c =
+    c b
+
+  k1field a K1True =
+    MkC a
+
+  k1tabulate _ f =
+    toColumn <$> f @b K1True
+
+
+instance ( Context a ~ f, Table a, Field a' ~ Field ( MapContext Structure a ), Recontextualise a Structure ) => DispatchK1 'False f a a' where
+  data K1Field 'False a' x where
+    K1False :: Field a' x -> K1Field 'False a' x
+
+  type ConstrainK1 'False a a' c =
+    ConstrainTable a c
+
+  k1field a ( K1False i ) =
+    field a ( fieldMapping @_ @Structure i )
+
+  k1tabulate proxy f =
+    tabulateMCP proxy ( f . K1False . reverseFieldMapping @_ @Structure )
+
+
+data Spine a
diff --git a/src/Rel8/MonadQuery.hs b/src/Rel8/MonadQuery.hs
index 77b811d..ef8126b 100644
--- a/src/Rel8/MonadQuery.hs
+++ b/src/Rel8/MonadQuery.hs
@@ -17,6 +17,7 @@
 module Rel8.MonadQuery where
 
 import Control.Applicative ( Const(..), liftA2 )
+import Data.Functor.Identity
 import Numeric.Natural
 import Rel8.Column
 import Rel8.ColumnSchema
@@ -26,6 +27,7 @@ import Rel8.Nest
 import Rel8.SimpleConstraints
 import Rel8.Table
 import Rel8.TableSchema
+import Rel8.Unconstrained
 
 import qualified Opaleye.Binary as Opaleye
 import qualified Opaleye.Distinct as Opaleye