packages feed

pg-schema-0.8.0.1: src/PgSchema/Ann.hs

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TemplateHaskell #-}
module PgSchema.Ann where

import Data.Aeson
import Data.Aeson.Types (Pair, Parser)
import qualified Data.Aeson.KeyMap as KM
import qualified Data.Aeson.Key as Key
import Data.Coerce
import Data.Singletons.TH (genDefunSymbols)
import Data.Type.Bool
import Data.Type.Equality
import Data.Typeable
import Data.Text qualified as T
import Data.Kind
import Database.PostgreSQL.Simple.ToField(ToField(..), Action, toJSONField)
import Database.PostgreSQL.Simple.FromField(FromField(..), fromJSONField)
import Database.PostgreSQL.Simple.ToRow(ToRow(..))
import Database.PostgreSQL.Simple.FromRow(FromRow(..), RowParser, field)
import GHC.Generics
import GHC.Int
import GHC.TypeLits
import PgSchema.Schema
import PgSchema.Types
import PgSchema.Utils.Internal
import Data.Singletons as SP
import PgSchema.Utils.TF as SP



-- $setup
-- >>> import PgSchema.Schema.Catalog
-- >>> import Database.PostgreSQL.Simple
-- >>> conn <- connectPostgreSQL ""

-- | Type-level annotation: enforce constraints at compile time
-- and drive demoted types used to generate correct SQL.
-- 'annRen' and 'annSch' are fixed for the whole DML-operation.
-- 'annDepth' and 'annTab' are changed while traversing the structure of the ADT.
--
data Ann = Ann
  { annRen  :: Renamer -- ^ Renamer to convert Haskell names to database names.
  , annSch  :: Type    -- ^ Schema with tables, relations and types.
  , annDepth :: Nat
  -- ^ Depth of the nested relations. It is mostly used to prevent cycles in types.
  , annTab  :: NameNSK -- ^ Name of the root table.
  }

type family AnnSch (ann :: Ann) where
  AnnSch ('Ann ren sch depth tab) = sch
type family AnnRen (ann :: Ann) where
  AnnRen ('Ann ren sch depth tab) = ren
type family AnnTab (ann :: Ann) where
  AnnTab ('Ann ren sch depth tab) = tab

data ColInfo (p :: Type) = ColInfo
  { ciField   :: SymNat
  , ciType    :: Type
  , ciDbField :: Symbol
  , ciInfo    :: RecField' Symbol p
  }

-- | Renamer is a type-level function from 'Symbol' to 'Symbol'.
type Renamer = Symbol ~> Symbol

-- | Apply renamer to symbol.
--
--  Like 'Data.Singletons.Apply' but specialized for 'Symbol'.
--
-- To make your own Renamer, typically you make
--
-- * data MyRenamer :: Renamer
-- * closed type family: `type family MyRenamerImpl (s :: Symbol) :: Symbol where ... `
-- * type instance ApplyRenamer MyRenamer s = MyRenamerImpl s
--
type family ApplyRenamer (renamer :: Renamer) (s :: Symbol) :: Symbol

-- | Renamer that does not change the symbol.
data RenamerId :: Renamer

type instance ApplyRenamer RenamerId s = s

type family ApplyRenamerNS (ren :: Renamer) (nns :: NameNSK) :: NameNSK where
  ApplyRenamerNS ren ('NameNS ns n) = 'NameNS ns (ApplyRenamer ren n)

type family MapRen (f :: Renamer) (xs :: [Symbol]) :: [Symbol] where
  MapRen f '[] = '[]
  MapRen f (x ': xs) = ApplyRenamer f x ': MapRen f xs

-- | End table after walking @path@ from @t@.
type TabOnDPathRen ren sch t path = TabAtPath sch t path

-- | 'ToStar' for demotion and forced 'TabOnDPath2' walk (invalid edges error here).
type PathCtx ren sch t path =
  ( ToStar path
  , TabAtPath sch t path ~ TabAtPath sch t path
  )

--------------------------------------------------------------------------------
-- Case dispatch
--------------------------------------------------------------------------------

data ColsCase = NonGenericCase | GenericCase

type family ColsCaseOf (r :: Type) :: ColsCase where
  ColsCaseOf (Maybe r)             = ColsCaseOf r
  ColsCaseOf (a :. b)              = 'NonGenericCase
  ColsCaseOf ((_ :: Symbol) := _) = 'NonGenericCase
  ColsCaseOf r = 'GenericCase

--------------------------------------------------------------------------------
-- CCols / CColsCase
--------------------------------------------------------------------------------

class CColsCase ann r (ColsCaseOf r) => CCols ann r where
  type Cols ann r :: [ColInfo NameNSK]

instance CColsCase ann r (ColsCaseOf r) => CCols ann r where
  type Cols ann r = ColsWithCase ann r (ColsCaseOf r)

class CColsCase (ann :: Ann) (r :: Type) (c :: ColsCase) where
  type ColsWithCase ann r c :: [ColInfo NameNSK]

instance CColsCase ann r 'NonGenericCase where
  type ColsWithCase ann r 'NonGenericCase = ColsNonGeneric ann r

instance Generic r => CColsCase ann r 'GenericCase where
  type ColsWithCase ann r 'GenericCase = GCols ann (Rep r)

--------------------------------------------------------------------------------
-- ColsNonGeneric (closed TF: (:.) and (:=))
--------------------------------------------------------------------------------

type family ColsNonGeneric (ann :: Ann) r :: [ColInfo NameNSK] where
  ColsNonGeneric ann (Maybe r) = ColsNonGeneric ann r
  ColsNonGeneric ann (a :. b) = Normalize (Cols ann a SP.++ Cols ann b)
  ColsNonGeneric ann (fld := t) = Col ann fld t

--------------------------------------------------------------------------------
-- Col / ColFI (per-field, reused by GCols)
--------------------------------------------------------------------------------

type family Col (ann :: Ann) (fld :: Symbol) t :: [ColInfo NameNSK] where
  Col ann fld () = '[]
  Col ('Ann ren _s _d _t) fld (Aggr ACount Int64) =
    '[ 'ColInfo '(fld, 0) (Aggr ACount Int64) (ApplyRenamer ren fld)
      ('RFAggr ('FldDef ("pg_catalog" ->> "int8") False False) 'ACount 'True) ]
  Col ('Ann ren _s _d _t) fld (Aggr' ACount Int64) =
    '[ 'ColInfo '(fld, 0) (Aggr' ACount Int64) (ApplyRenamer ren fld)
      ('RFAggr ('FldDef ("pg_catalog" ->> "int8") False False) 'ACount 'True) ]
  Col ('Ann ren sch _d tab) fld (UnsafeCol flds expr t) =
    '[ 'ColInfo '(fld, 0) (PgTag '(sch, tab) (UnsafeCol (MapRen ren flds) expr t)) (ApplyRenamer ren fld)
      ('RFUnsafe (MapRen ren flds) expr) ]
  Col ('Ann ren sch d tab) fld t =
    ColFI ('Ann ren sch d tab) fld (TDBFieldInfo sch tab (ApplyRenamer ren fld)) t

type family ColFI (ann :: Ann) (fld :: Symbol) (fi :: RecFieldK NameNSK) t
  :: [ColInfo NameNSK] where
    ColFI ('Ann ren sch _ _) fld ('RFPlain ('FldDef tn False def)) (PgArr t) =
      '[ 'ColInfo '(fld, 0) (PgTag (TypElem (TTypDef sch tn)) (PgArr t))
        (ApplyRenamer ren fld) (RFPlain ('FldDef tn False def))]
    ColFI ('Ann ren sch _ _) fld ('RFPlain ('FldDef tn True def)) (Maybe (PgArr t)) =
      '[ 'ColInfo '(fld, 0) (Maybe (PgTag (TypElem (TTypDef sch tn)) (PgArr t)))
        (ApplyRenamer ren fld) (RFPlain ('FldDef tn True def))]
    -- RFFromHere: Maybe r
    ColFI ('Ann ren sch d _) fld ('RFFromHere (toTab :: NameNSK) refs) (Maybe r) =
      '[ 'ColInfo '(fld, 0) (Maybe (PgTag (AnnRefTabDepth ('Ann ren sch d toTab) toTab) r))
        (ApplyRenamer ren fld) ('RFFromHere toTab refs) ]
    -- RFFromHere: r (non-Maybe)
    ColFI ('Ann ren sch d _) fld ('RFFromHere (toTab :: NameNSK) refs) r =
      '[ 'ColInfo '(fld, 0) (PgTag (AnnRefTabDepth ('Ann ren sch d toTab) toTab) r)
        (ApplyRenamer ren fld) ('RFFromHere toTab refs) ]
    ColFI ('Ann ren sch d _) fld ('RFToHere (fromTab :: NameNSK) refs) [t] =
      '[ 'ColInfo '(fld, 0) [PgTag (AnnRefTabDepth ('Ann ren sch d fromTab) fromTab) t]
        (ApplyRenamer ren fld) ('RFToHere fromTab refs) ]
    ColFI ann fld ('RFSelfRef tab refs) [t] = ColFI ann fld ('RFToHere tab refs) [t]
    ColFI ann fld ('RFSelfRef tab refs) t = ColFI ann fld ('RFFromHere tab refs) t
    ColFI ('Ann ren sch d tab) fld ('RFPlain fd) (Aggr af t) =
      '[ 'ColInfo '(fld, 0) (Aggr af t) (ApplyRenamer ren fld) ('RFAggr fd af 'True) ]
    ColFI ('Ann ren sch d tab) fld ('RFPlain fd) (Aggr' af t) =
      '[ 'ColInfo '(fld, 0) (Aggr' af t) (ApplyRenamer ren fld) ('RFAggr fd af 'False) ]
    ColFI ('Ann ren sch d _) fld fd t = '[ 'ColInfo '(fld, 0) t (ApplyRenamer ren fld) fd ]
--------------------------------------------------------------------------------
-- GCols (closed TF: Generic Rep)
--------------------------------------------------------------------------------

type family GCols ann (rep :: Type -> Type) :: [ColInfo NameNSK] where
    GCols ann (D1 d (C1 c flds)) = Normalize (GCols ann flds)
    GCols ann (a :*: b) = GCols ann a SP.++ GCols ann b
    GCols ann (S1 (MetaSel ('Just fld) u v w) (Rec0 t)) = Col ann fld t
    GCols ann rep = TypeError
      ( Text "Only Product types with fields are supported in pg-schema."
      :$$: Text "(sum types, empty, or missing field selector are not supported)"
      :$$: Text ""
      :$$: Text "But I've got " :<>: ShowType rep )

--------------------------------------------------------------------------------
-- Normalize (SymNat numbering)
--------------------------------------------------------------------------------

type family AddNum (xs :: [ColInfo p]) (cnts :: [SymNat])
  (accCnts :: [SymNat]) :: [ColInfo p]
  where
    AddNum '[] _ _ = '[]
    AddNum ('ColInfo '(s,_) t f fi : xs) '[] accCnts =
      'ColInfo '(s,0) t f fi ': AddNum xs ('(s,0) ': accCnts) '[]
    AddNum ('ColInfo '(s,_) t f fi : xs) ('(s,n) ': rest) accCnts =
      'ColInfo '(s, n+1) t f fi ': AddNum xs (('(s,n+1) ': accCnts) SP.++ rest) '[]
    AddNum ('ColInfo '(s,x) t f fi : xs) ('(s',n) ': rest) accCnts =
      AddNum ('ColInfo '(s,x) t f fi : xs) rest ('(s',n) ': accCnts)

type Normalize xs = AddNum xs '[] '[]

--------------------------------------------------------------------------------
-- ToJSON for PgTag Ann r
--------------------------------------------------------------------------------

instance
  (cols ~ Cols ann r, colsCase ~ ColsCaseOf r, ToJSONCols ann colsCase cols r)
  => ToJSON (PgTag ann r) where
    toJSON (PgTag r) = Object (KM.fromList (toPairs @ann @colsCase @cols r))
    toEncoding (PgTag r) = pairs (foldMap (uncurry (.=)) $ toPairs @ann @colsCase @cols r)

type family RowNotMaybe (r :: Type) :: Constraint where
  RowNotMaybe (Maybe _) = TypeError
    ( Text "Use FromJSON (PgTag ann (Maybe r)) for optional top-level rows." )
  RowNotMaybe _ = ()

instance
  ( cols ~ Cols ann r, colsCase ~ ColsCaseOf r, FromJSONCols ann colsCase cols r
  , RowNotMaybe r )
  => FromJSON (PgTag ann r) where
   parseJSON v = PgTag <$> parseJSONCols @ann @colsCase @cols v

instance {-# OVERLAPPING #-}
  ( cols ~ Cols ann r, colsCase ~ ColsCaseOf r
  , FromJSONCols ann colsCase cols r )
  => FromJSON (PgTag ann (Maybe r)) where
   parseJSON Null = pure $ PgTag Nothing
   parseJSON v = PgTag . Just <$> parseJSONCols @ann @colsCase @cols v

-- >>> type AnnRel = 'Ann RenamerId PgCatalog (PGC "pg_constraint")
-- >>> rel = PgRelation{ constraint__namespace = PgTag "a", conname = "b", constraint__class = PgClassShort (PgTag "c") "d", constraint__fclass = PgClassShort (PgTag "e") "f", conkey = pgArr' [1,2], confkey = pgArr' [] }
-- >>> rec = "conname" =: ("x" :: T.Text) :. "conname" =: ("z" :: T.Text) :. rel :. "conname" =: ("y" :: T.Text)
-- >>> toJSON $ PgTag @AnnRel rec
-- >>> fromJSON (toJSON $ PgTag @AnnRel rec) == Success (PgTag @AnnRel rec)
-- Object (fromList [("confkey",Array []),("conkey",Array [Number 1.0,Number 2.0]),("conname",String "x"),("conname___1",String "z"),("conname___2",String "b"),("conname___3",String "y"),("constraint__class",Object (fromList [("class__namespace",Object (fromList [("nspname",String "c")])),("relname",String "d")])),("constraint__fclass",Object (fromList [("class__namespace",Object (fromList [("nspname",String "e")])),("relname",String "f")])),("constraint__namespace",Object (fromList [("nspname",String "a")]))])
-- True


class ToJSONCols (ann :: Ann) (colsCase :: ColsCase) (cols :: [ColInfo NameNSK]) r where
  toPairs :: r -> [Pair]

class FromJSONCols (ann :: Ann) (colsCase :: ColsCase) (cols :: [ColInfo NameNSK]) r where
  parseJSONCols :: Value -> Parser r

-- (:=)
--------------------------------------------------------------------------------
-- NonGeneric: (:=) и (:.)
--------------------------------------------------------------------------------
instance ToJSONCols ann 'NonGenericCase '[] (fld := ()) where
  toPairs _ = []

instance FromJSONCols ann 'NonGenericCase '[] (fld := ()) where
  parseJSONCols = pure $ pure (PgTag ())

instance (KnownSymNat sn, ToJSON t, Coercible v t)
  => ToJSONCols ann 'NonGenericCase '[ 'ColInfo sn t db fi ] (fld := v) where
    toPairs (PgTag v) = [Key.fromText (demote @(NameSymNat sn)) .= coerce @_ @t v]

instance
  (KnownSymNat sn, FromJSON tEff, Coercible t tEff)
  => FromJSONCols ann 'NonGenericCase '[ 'ColInfo sn tEff db fi ] (fld := t) where
    parseJSONCols = withObject "record" $ \obj -> do
      case KM.lookup (Key.fromText keyTxt) obj of
        Nothing -> fail ("missing key " ++ T.unpack keyTxt)
        Just v  -> coerce <$> parseJSON @tEff v        -- eff :: tEff
      where
        keyTxt = demote @(NameSymNat sn)

instance
  ( cols ~ Cols ann r, colsCase ~ ColsCaseOf r
  , FromJSONCols ann colsCase cols r )
  => FromJSONCols ann colsCase cols (Maybe r) where
    parseJSONCols Null = pure Nothing
    parseJSONCols v = Just <$> parseJSONCols @ann @colsCase @cols v

instance
  ( cols ~ Cols ann r, colsCase ~ ColsCaseOf r
  , ToJSONCols ann colsCase cols r )
  => ToJSONCols ann colsCase cols (Maybe r) where
    toPairs Nothing = []
    toPairs (Just r) = toPairs @ann @colsCase @cols r

-- Note: we use "split ~" instead of " '(colsA, colsB) ~ " to avoid ambiguity.
instance
  ( ca ~ ColsCaseOf a, cb ~ ColsCaseOf b
  , split ~ SplitAt (Length (Cols ann a)) cols
  , colsA ~ Fst split, colsB ~ Snd split
  , ToJSONCols ann ca colsA a, ToJSONCols ann cb colsB b )
  => ToJSONCols ann 'NonGenericCase cols (a :. b) where
    toPairs (a :. b) = toPairs @ann @ca @colsA a <> toPairs @ann @cb @colsB b

instance
  ( ca ~ ColsCaseOf a, cb ~ ColsCaseOf b
  , split ~ SplitAt (Length (Cols ann a)) cols
  , colsA ~ Fst split, colsB ~ Snd split
  , FromJSONCols ann ca colsA a, FromJSONCols ann cb colsB b)
  => FromJSONCols ann 'NonGenericCase cols (a :. b) where
    parseJSONCols v =
      (:.) <$> parseJSONCols @ann @ca @colsA v <*> parseJSONCols @ann @cb @colsB v

--------------------------------------------------------------------------------
-- Generic
-----------------------------------------------------------------------------
class GToJSONCols (ann :: Ann) (cols :: [ColInfo NameNSK]) (rep :: Type -> Type) where
  gToPairs :: rep x -> [Pair]

class GFromJSONCols (ann :: Ann) (cols :: [ColInfo NameNSK]) (rep :: Type -> Type) where
  gParseJSONCols :: Value -> Parser (rep x)

instance
  (Generic r, GToJSONCols ann cols (Rep r))
  => ToJSONCols ann 'GenericCase cols r where
    toPairs r = gToPairs @ann @cols (from r)

instance
  (Generic r, GFromJSONCols ann cols (Rep r))
  => FromJSONCols ann 'GenericCase cols r where
    parseJSONCols = fmap to . gParseJSONCols @ann @cols

-- D1/C1
instance GToJSONCols ann cols flds
  => GToJSONCols ann cols (D1 d (C1 c flds)) where
    gToPairs (M1 (M1 x)) = gToPairs @ann @cols x

instance GFromJSONCols ann cols flds
  => GFromJSONCols ann cols (D1 d (C1 c flds)) where
    gParseJSONCols = fmap (M1 . M1) . gParseJSONCols @ann @cols

-- (:*:)
instance
  ( split ~ SplitAt (Length (GCols ann a)) cols
  , colsA ~ Fst split, colsB ~ Snd split
  , GToJSONCols ann colsA a, GToJSONCols ann colsB b )
  => GToJSONCols ann cols (a :*: b) where
    gToPairs (a :*: b) = gToPairs @ann @colsA a <> gToPairs @ann @colsB b

instance
  ( split ~ SplitAt (Length (GCols ann a)) cols
  , colsA ~ Fst split, colsB ~ Snd split
  , GFromJSONCols ann colsA a, GFromJSONCols ann colsB b )
  => GFromJSONCols ann cols (a :*: b) where
    gParseJSONCols v =
      (:*:) <$> gParseJSONCols @ann @colsA v <*> gParseJSONCols @ann @colsB v

-- Rec0
instance (ToJSONCols ann 'NonGenericCase cols (fld := t))
  => GToJSONCols ann cols (S1 (MetaSel ('Just fld) u v w) (Rec0 t))
  where
    gToPairs (M1 (K1 v)) = toPairs @ann @'NonGenericCase @cols (fld =: v)

instance (FromJSONCols ann 'NonGenericCase cols (fld := t))
  => GFromJSONCols ann cols (S1 (MetaSel ('Just fld) u v w) (Rec0 t)) where
    gParseJSONCols = fmap (M1 . K1 . unPgTag)
      . parseJSONCols @ann @'NonGenericCase @cols @(fld := t)

--------------------------------------------------------------------------------
-- ToRow / FromRow for PgTag ann r
--------------------------------------------------------------------------------
instance ToJSON (PgTag ann r) => ToField (PgTag (ann :: Ann) r) where
  toField = toJSONField

-- instance ToJSON (PgTag ann r) => ToField (Maybe (PgTag (ann :: Ann) r)) where
--   toField = toJSONField

instance ToJSON (PgTag ann r) => ToField [PgTag (ann :: Ann) r] where
  toField = toJSONField

instance (FromJSON (PgTag ann r), Typeable ann, Typeable r)
  => FromField (PgTag (ann :: Ann) r) where
    fromField = fromJSONField

instance (FromJSON (PgTag ann r), Typeable ann, Typeable r)
  => FromField [PgTag (ann :: Ann) r] where
    fromField = fromJSONField

--------------------------------------------------------------------------------
-- ToRow / FromRow for PgTag ann r
--------------------------------------------------------------------------------
instance
  (cols ~ Cols ann r, colsCase ~ ColsCaseOf r, ToRowCols ann colsCase cols r)
  => ToRow (PgTag ann r) where
    toRow (PgTag r) = toRowCols @ann @colsCase @cols r

instance
  ( cols ~ Cols ann r, colsCase ~ ColsCaseOf r, FromRowCols ann colsCase cols r
  , RowNotMaybe r )
  => FromRow (PgTag ann r) where
    fromRow = PgTag <$> fromRowCols @ann @colsCase @cols

instance {-# OVERLAPPING #-}
  ( cols ~ Cols ann r, colsCase ~ ColsCaseOf r, FromRowCols ann colsCase cols r)
  => FromRow (PgTag ann (Maybe r)) where
    fromRow = PgTag . Just <$> fromRowCols @ann @colsCase @cols

-- >>> type AnnRel = 'Ann RenamerId PgCatalog 1 (PGC "pg_constraint")
-- >>> (r1 :: [PgTag AnnRel ( ("conkey" := Int16))]) <- query_ conn "select 1::int2"
-- >>> r1
-- [PgTag {unPgTag = "conkey" =: 1}]

class ToRowCols (ann :: Ann) (colsCase :: ColsCase) (cols :: [ColInfo NameNSK]) r
  where
    toRowCols :: r -> [Action]

class FromRowCols (ann :: Ann) (colsCase :: ColsCase) (cols :: [ColInfo NameNSK]) r
  where
    fromRowCols :: RowParser r

--------------------------------------------------------------------------------
-- NonGeneric: (:=) and (:.)
--------------------------------------------------------------------------------
instance ToRowCols ann 'NonGenericCase '[] (fld := ()) where
  toRowCols _ = []

instance FromRowCols ann 'NonGenericCase '[] (fld := ()) where
  fromRowCols = pure (PgTag ())

instance (KnownSymNat sn, ToField t, Coercible v t)
  => ToRowCols ann 'NonGenericCase '[ 'ColInfo sn t db fi ] (fld := v) where
    toRowCols (PgTag v) = [toField (coerce @_ @t v)]

instance (FromField tEff, Coercible t tEff)
  => FromRowCols ann 'NonGenericCase '[ 'ColInfo sn tEff db fi ] (fld := t) where
    fromRowCols = coerce <$> field @tEff

instance
  ( ca ~ ColsCaseOf a, cb ~ ColsCaseOf b
  , split ~ SplitAt (Length (Cols ann a)) cols
  , colsA ~ Fst split, colsB ~ Snd split
  , ToRowCols ann ca colsA a, ToRowCols ann cb colsB b )
  => ToRowCols ann 'NonGenericCase cols (a :. b) where
  toRowCols (a :. b) = toRowCols @ann @ca @colsA a <> toRowCols @ann @cb @colsB b

instance
  ( ca ~ ColsCaseOf a, cb ~ ColsCaseOf b
  , split ~ SplitAt (Length (Cols ann a)) cols
  , colsA ~ Fst split, colsB ~ Snd split
  , FromRowCols ann ca colsA a, FromRowCols ann cb colsB b )
  => FromRowCols ann 'NonGenericCase cols (a :. b) where
  fromRowCols = (:.)
    <$> fromRowCols @ann @ca @(Fst split)
    <*> fromRowCols @ann @cb @(Snd split)

--------------------------------------------------------------------------------
-- Generic: through Rep r
--------------------------------------------------------------------------------

class GToRowCols (ann :: Ann) (cols :: [ColInfo NameNSK]) (rep :: Type -> Type) where
  gToRowCols :: rep x -> [Action]

class GFromRowCols (ann :: Ann) (cols :: [ColInfo NameNSK]) (rep :: Type -> Type) where
  gFromRowCols :: RowParser (rep x)

instance (Generic r, GToRowCols ann cols (Rep r))
  => ToRowCols (ann :: Ann) 'GenericCase cols r where
    toRowCols r = gToRowCols @ann @cols (from r)

instance (Generic r, GFromRowCols ann cols (Rep r))
  => FromRowCols ann 'GenericCase cols r where
    fromRowCols = to <$> gFromRowCols @ann @cols

instance GToRowCols ann cols flds
  => GToRowCols ann cols (D1 d (C1 c flds)) where
    gToRowCols (M1 (M1 x)) = gToRowCols @ann @cols x

instance GFromRowCols ann cols flds
  => GFromRowCols ann cols (D1 d (C1 c flds)) where
    gFromRowCols = fmap (M1 . M1) (gFromRowCols @ann @cols)

instance
  ( split ~ SplitAt (Length (GCols ann a)) cols
  , colsA ~ Fst split, colsB ~ Snd split
  , GToRowCols ann colsA a, GToRowCols ann colsB b )
  => GToRowCols ann cols (a :*: b) where
    gToRowCols (a :*: b) = gToRowCols @ann @colsA a <> gToRowCols @ann @colsB b

instance
  ( split ~ SplitAt (Length (GCols ann a)) cols
  , colsA ~ Fst split, colsB ~ Snd split
  , GFromRowCols ann colsA a, GFromRowCols ann colsB b )
  => GFromRowCols ann cols (a :*: b) where
    gFromRowCols = (:*:) <$> gFromRowCols @ann @colsA <*> gFromRowCols @ann @colsB

instance ToRowCols ann 'NonGenericCase cols (fld := t)
  => GToRowCols ann cols (S1 (MetaSel ('Just fld) u v w) (Rec0 t)) where
    gToRowCols (M1 (K1 v)) = toRowCols @ann @'NonGenericCase @cols (fld =: v)

instance
  FromRowCols ann 'NonGenericCase cols (fld := t)
  => GFromRowCols ann cols (S1 (MetaSel ('Just fld) u v w) (Rec0 t)) where
    gFromRowCols = M1 . K1 . unPgTag
      <$> fromRowCols @ann @'NonGenericCase @cols @(fld := t)

--------------------------------------------------------------------------------
-- CRecInfo
--------------------------------------------------------------------------------

data FieldInfo s = FieldInfo
  { fieldName   :: s
  , fieldDbName :: s
  , fieldKind   :: RecField' s (RecordInfo s) }
  deriving Show

data RecordInfo s   = RecordInfo
  { tabName :: NameNS' s
  , fields  :: [FieldInfo s] }
  deriving Show

class CRecInfo (ann :: Ann) (r :: Type) where
  getRecordInfo :: RecordInfo T.Text

class CRecInfoCols (ann :: Ann) (cols :: [ColInfo NameNSK]) where
  getFields :: [FieldInfo T.Text]

class CFldInfo (ann :: Ann) (fldDbName :: Symbol) (fld :: RecField' Symbol NameNSK) t where
  getFldInfo :: RecField (RecordInfo T.Text)

instance
  (SingI (AnnTab ann), cols ~ Cols ann r, CRecInfoCols ann cols)
  => CRecInfo ann r where
  getRecordInfo = RecordInfo (demote @(AnnTab ann)) (getFields @ann @cols)

instance CRecInfoCols ann '[] where getFields = []

instance
  (KnownSymNat sn, KnownSymbol db, CFldInfo ann db fi t, CRecInfoCols ann cols)
  => CRecInfoCols ann ('ColInfo sn t db fi ': cols) where
  getFields = FieldInfo
    { fieldName   = demote @(NameSymNat sn)
    , fieldDbName = demote @db
    , fieldKind   = getFldInfo @ann @db @fi @t } : getFields @ann @cols

instance (ToStar fd, CanConvert (AnnSch ann) (AnnTab ann) fldDbName fd t) => CFldInfo ann fldDbName ('RFPlain fd) t where
  getFldInfo = RFPlain (demote @fd)

instance (ToStar fd, ToStar af, ToStar b) =>
  CFldInfo ann _fldDbName ('RFAggr fd af b) t where
  getFldInfo = RFAggr (demote @fd) (demote @af) (demote @b)

instance (ToStar flds, ToStar expr) =>
  CFldInfo ann _fldDbName ('RFUnsafe flds expr) t where
  getFldInfo = RFUnsafe (demote @flds) (demote @expr)

type family AnnRefTabDepth (ann :: Ann) refTab :: Ann where
  AnnRefTabDepth ('Ann ren sch d tab) refTab =
    'Ann ren sch (DecDepth ('Ann ren sch d tab)) refTab

instance (CRecInfo ann' r, ToStar refs, ann' ~ AnnRefTabDepth ann fromTab)
  => CFldInfo ann _fldDbName ('RFToHere fromTab refs) [PgTag ann' r] where
  getFldInfo = RFToHere (getRecordInfo @ann' @r) (demote @refs)

instance (CRecInfo ann' r, ToStar refs, ann' ~ AnnRefTabDepth ann toTab, CheckRef ann _fldDbName(HasNullableRefs refs) 'True)
  => CFldInfo ann _fldDbName ('RFFromHere toTab refs) (Maybe (PgTag ann' r)) where
  getFldInfo = RFFromHere (getRecordInfo @ann' @r) (demote @refs)

instance (CRecInfo ann' r, ToStar refs, ann' ~ AnnRefTabDepth ann toTab, CheckRef ann _fldDbName(HasNullableRefs refs) 'False)
  => CFldInfo ann _fldDbName ('RFFromHere toTab refs) (PgTag ann' r) where
  getFldInfo = RFFromHere (getRecordInfo @ann' @r) (demote @refs)

--------------------------------------------------------------------------------
-- Helpers over Cols ann r
--------------------------------------------------------------------------------

type family ColDbName (c :: ColInfo p) :: Symbol where
  ColDbName ('ColInfo '(fld, idx) t db fi) = db

type family ColsDbNames (cols :: [ColInfo p]) :: [Symbol] where
  ColsDbNames '[]       = '[]
  ColsDbNames (c ': cs) = ColDbName c ': ColsDbNames cs

--------------------------------------------------------------------------------
-- Plain fields (without relation fields)
--------------------------------------------------------------------------------

type family IsPlainRecField (fi :: RecField' Symbol NameNSK) :: Bool where
  IsPlainRecField ('RFToHere tab rs)   = 'False
  IsPlainRecField ('RFFromHere tab rs) = 'False
  IsPlainRecField ('RFSelfRef tab rs)  = 'False
  IsPlainRecField fi        = 'True

type family NotPlainCols (cols :: [ColInfo NameNSK]) (rs :: [Symbol]) :: [Symbol] where
  NotPlainCols '[] rs = rs
  NotPlainCols ('ColInfo sn t db fi ': cs) rs =
    NotPlainCols cs (AppNotPlain rs db (IsPlainRecField fi))

type family AppNotPlain (rs :: [Symbol]) (db :: Symbol) (b :: Bool) :: [Symbol] where
  AppNotPlain rs db 'True = rs
  AppNotPlain rs db 'False = db ': rs

-- | All fields are plain (no RFToHere/RFFromHere)
type AllPlain (ann :: Ann) (r :: Type) = AllPlainRS ann (NotPlainCols (Cols ann r) '[]) r

type family AllPlainRS (ann :: Ann) (rs :: [Symbol]) (r :: Type) :: Constraint where
  AllPlainRS ann '[] r = ()
  AllPlainRS ann rs r = TypeError
    (  Text "Not all fields in record are 'plain' (no relations allowed)."
    :$$: Text ""
    :$$: Text "Not plain cols: " :<>: ShowType rs
    :$$: Text ""
    :$$: Text "Ann:   " :<>: ShowType ann
    :$$: Text "Cols:  " :<>: ShowType (Cols ann r)
    :$$: Text "" )

--------------------------------------------------------------------------------
-- Type-level RecordInfo for Ann
--------------------------------------------------------------------------------
-- | Decrease relation-walk depth kept in 'Ann'.
-- When depth is exhausted, fail with a detailed type error instead of
-- potentially diverging in recursive type families/instances.
type family DecDepth (ann :: Ann) :: Nat where
  DecDepth ('Ann ren sch 0 tab) = TypeError
    (  Text "pg-schema: relation walk depth limit reached."
    :$$: Text ""
    :$$: Text "Ann:   " :<>: ShowType ('Ann ren sch 0 tab)
    :$$: Text "Table: " :<>: ShowType tab
    :$$: Text ""
    :$$: Text "Likely reason:"
    :$$: Text "  Recursive/self-referential tree (SelfRef or cycle) is deeper"
    :$$: Text "  than annDepth in your Ann."
    :$$: Text ""
    :$$: Text "How to fix:"
    :$$: Text "  1) Increase annDepth in Ann;"
    :$$: Text "  2) Reduce recursion depth in selected/inserted shape;"
    :$$: Text "  3) For true graph cycles, use manual SQL." )
  DecDepth ('Ann _ _ d _) = d - 1

-- Type-level analogue of CFldInfo: take DB-level RecFieldK and Haskell type of field t
-- and build RecField' Symbol (RecordInfo Symbol) with TRecordInfo for children.
type family TFldInfo (ann :: Ann) (fi :: RecField' Symbol NameNSK) t
  :: RecField' Symbol (RecordInfo Symbol) where
  TFldInfo ann ('RFPlain fd) t = 'RFPlain fd
  TFldInfo ann ('RFAggr fd af b) t = 'RFAggr fd af b
  TFldInfo ann ('RFEmpty s) t = 'RFEmpty s
  TFldInfo ('Ann ren sch d tab) ('RFToHere (toTab :: NameNSK) refs)
    [PgTag ('Ann ren sch d' toTab) rChild] =
    'RFToHere ('RecordInfo toTab (TRecordInfo ('Ann ren sch d' toTab) rChild)) refs
  TFldInfo ('Ann ren sch d tab) ('RFFromHere (toTab :: NameNSK) refs)
    (Maybe (PgTag ('Ann ren sch d' toTab) rChild)) =
    'RFFromHere ('RecordInfo toTab (TRecordInfo ('Ann ren sch d' toTab) rChild)) refs
  TFldInfo ('Ann ren sch d tab) ('RFFromHere (toTab :: NameNSK) refs)
    (PgTag ('Ann ren sch d' toTab) rChild) =
    'RFFromHere ('RecordInfo toTab (TRecordInfo ('Ann ren sch d' toTab) rChild)) refs
  TFldInfo ann fi t = TypeError
    (  Text "TFldInfo: unsupported RecField for Ann."
    :$$: Text "  Ann: " :<>: ShowType ann
    :$$: Text "  RecField: " :<>: ShowType fi
    :$$: Text "  Haskell type: " :<>: ShowType t
    :$$: Text ""
    :$$: Text "Most likely TDBFieldInfo / ColFI produced a constructor"
    :$$: Text "that TFldInfo does not know how to map into RecordInfo." )

type family TRecordInfoCols (ann  :: Ann) (cols :: [ColInfo NameNSK]) :: [FieldInfo Symbol] where
  TRecordInfoCols ann '[] = '[]
  TRecordInfoCols ann ('ColInfo sn t db fi ': cs) =
    'FieldInfo (NameSymNat sn) db (TFldInfo ann fi t) ': TRecordInfoCols ann cs

type family TRecordInfo (ann :: Ann) (r :: Type) :: [FieldInfo Symbol] where
  TRecordInfo ann r = TRecordInfoCols ann (Cols ann r)

--------------------------------------------------------------------------------
-- CheckRef
--------------------------------------------------------------------------------
type family CheckRef (ann :: Ann) (fldDbName :: Symbol)
  (hasNullable :: Bool) (expectMaybe :: Bool) :: Constraint where
  CheckRef ('Ann ren sch d tab) fldDbName 'True 'False =
    TypeError
      (  Text "relation result must be Maybe because"
      :$$: Text "foreign key in this relation is nullable."
      :$$: Text ""
      :$$: Text "Table:      " :<>: ShowType tab
      :$$: Text "Relation:   " :<>: ShowType fldDbName
      :$$: Text "" )
  CheckRef ('Ann ren sch d tab) fldDbName 'False 'True =
    TypeError
      (  Text "relation result must NOT be Maybe because"
      :$$: Text "foreign key in this relation is NOT NULL."
      :$$: Text ""
      :$$: Text "Table:      " :<>: ShowType tab
      :$$: Text "Relation:   " :<>: ShowType fldDbName
      :$$: Text "" )
  CheckRef ann fldDbName b b = ()
--------------------------------------------------------------------------------
-- Node-level checks for Mandatory / upsert keys (CheckNodeAll* analogue)
--------------------------------------------------------------------------------

-- | One-table check that all mandatory fields are present
-- rs: list of columns that are already "covered" (including those that come from Reference)
type family CheckAllMandatory (ann :: Ann) (rs :: [Symbol]) :: Constraint where
  CheckAllMandatory ('Ann ren sch d tab) rs =
    CheckAllMandatory' (RestMandatory sch tab rs) ('Ann ren sch d tab) rs

type family CheckAllMandatory' (rest :: [Symbol]) (ann :: Ann) (rs :: [Symbol]) :: Constraint where
  CheckAllMandatory' '[] ann rs = ()
  CheckAllMandatory' rest ('Ann ren sch d tab) rs = TypeError
    (  Text "We can't insert data because not all mandatory fields are present."
    :$$: Text "Table: " :<>: ShowType tab
    :$$: Text "Missing mandatory fields: " :<>: ShowType rest )

-- | All mandatory fields in @rs@, or a full primary key, or a full eligible
-- unique key (see 'IdentityCandidates').
type family CheckAllMandatoryOrHasKey (ann :: Ann) (rs :: [Symbol]) :: Constraint where
  CheckAllMandatoryOrHasKey ('Ann ren sch d tab) rs = CheckAllMandatoryOrHasKey'
    (RestMandatory sch tab rs) (IdentityCandidates sch tab)
    ('Ann ren sch d tab) rs

type family CheckAllMandatoryOrHasKey' (restMandatory :: [Symbol]) (cands :: [[Symbol]]) (ann :: Ann) (rs :: [Symbol]) :: Constraint where
  CheckAllMandatoryOrHasKey' '[] _ ann rs = ()
  CheckAllMandatoryOrHasKey' rm cands ann rs = HasAnyFullIdentity rs cands ann

type family HasAnyFullIdentity (rs :: [Symbol]) (cands :: [[Symbol]]) ann :: Constraint where
  HasAnyFullIdentity rs '[] ('Ann _ sch _ tab) =
    TypeError
      (  Text "We can't upsert data because for table " :<>: ShowType tab
      :$$: Text "not all mandatory fields are present and no full primary or"
      :$$: Text "unique key is covered by record fields."
      :$$: Text "Missing mandatory fields: " :<>: ShowType (RestMandatory sch tab rs)
      :$$: Text "Possible keys: " :<>: ShowType (IdentityCandidates sch tab) )
  HasAnyFullIdentity rs (k ': ks) ann =
    HasAnyFullIdentity' (RestKey rs k) rs ks ann

type family HasAnyFullIdentity' (restKey :: [Symbol]) (rs :: [Symbol]) (ks :: [[Symbol]]) ann :: Constraint where
  HasAnyFullIdentity' '[] rs ks ann = ()
  HasAnyFullIdentity' (_ ': _) rs ks ann = HasAnyFullIdentity rs ks ann

-- | Every node must include a full primary or eligible unique key.
type family CheckHasKey (ann :: Ann) (rs :: [Symbol]) :: Constraint where
  CheckHasKey ('Ann ren sch d tab) rs =
    HasAnyFullIdentity rs (IdentityCandidates sch tab) ('Ann ren sch d tab)

-- | All mandatory fields and a full primary or eligible unique key (flat upsert).
type CheckAllMandatoryAndHasKey ann rs =
  (CheckAllMandatory ann rs, CheckHasKey ann rs)

genDefunSymbols
  [ ''CheckAllMandatory, ''CheckAllMandatoryOrHasKey, ''CheckHasKey ]

--------------------------------------------------------------------------------
-- Recursive AllMandatory / PK for tree (JSON insert / upsert)
--------------------------------------------------------------------------------
type family WalkLevelAnn
  (check :: Ann ~> [Symbol] ~> Constraint)
  (ann :: Ann) (fis :: [FieldInfo Symbol]) (rs :: [Symbol]) :: Constraint where
  WalkLevelAnn check ann '[] rs = SP.Apply (SP.Apply check ann) rs
  WalkLevelAnn check ann ('FieldInfo name db ('RFPlain fd) ': xs) rs =
    WalkLevelAnn check ann xs (db ': rs)
  WalkLevelAnn check ('Ann ren sch d tab)
    ('FieldInfo _ _ ('RFToHere ('RecordInfo childTab childFIs) refs) ': xs) rs =
      ( WalkLevelAnn check ('Ann ren sch d childTab) childFIs (SP.Map1 FromNameSym0 refs)
      , WalkLevelAnn check ('Ann ren sch d tab) xs rs )
  WalkLevelAnn check ann (_ ': xs) rs = WalkLevelAnn check ann xs rs

type family AllMandatoryTree (ann :: Ann) (r :: Type) (rFlds :: [Symbol])
  :: Constraint where
  AllMandatoryTree ann [r] rFlds = AllMandatoryTree ann r rFlds
  AllMandatoryTree ann r rFlds =
    WalkLevelAnn CheckAllMandatorySym0 ann (TRecordInfo ann r) rFlds

type family AllMandatoryOrHasKeyTree (ann :: Ann) (r :: Type) (rFlds :: [Symbol])
  :: Constraint where
  AllMandatoryOrHasKeyTree ann [r] rFlds = AllMandatoryOrHasKeyTree ann r rFlds
  AllMandatoryOrHasKeyTree ann r rFlds =
    WalkLevelAnn CheckAllMandatoryOrHasKeySym0 ann (TRecordInfo ann r) rFlds

type family AllHasKeyTree (ann :: Ann) (r :: Type) (rFlds :: [Symbol])
  :: Constraint where
  AllHasKeyTree ann [r] rFlds = AllHasKeyTree ann r rFlds
  AllHasKeyTree ann r rFlds =
    WalkLevelAnn CheckHasKeySym0 ann (TRecordInfo ann r) rFlds

--------------------------------------------------------------------------------
-- Returning tree must be subtree of input tree (with path)
--------------------------------------------------------------------------------

type family Snoc (p :: [k]) (x :: k) :: [k] where
  Snoc '[] x = '[x]
  Snoc (a ': as) x = a ': Snoc as x

type family FindChildAt (path :: [Symbol]) (db :: Symbol)
  (fisIn :: [FieldInfo Symbol]) :: [FieldInfo Symbol] where
  FindChildAt path db '[] = TypeError
    (  Text "Returning tree is not a subtree of input tree."
    :$$: Text "At path: " :<>: ShowType path
    :$$: Text "Missing branch (db name): " :<>: ShowType db )
  FindChildAt _ db ('FieldInfo _ db ('RFToHere ('RecordInfo _ fis) _) ': xs) = fis
  FindChildAt _ db ('FieldInfo _ db ('RFFromHere ('RecordInfo _ fis) _) ': xs) = fis
  FindChildAt path db (_ ': xs) = FindChildAt path db xs

type family CheckSubtreeAt (path :: [Symbol]) (fisIn :: [FieldInfo Symbol])
  (fisOut :: [FieldInfo Symbol]) :: Constraint where
  CheckSubtreeAt path fisIn '[] = ()
  CheckSubtreeAt path fisIn
    ('FieldInfo _ db ('RFToHere ('RecordInfo _ childFIsOut) _) ': xs) =
      ( CheckSubtreeAt (Snoc path db) (FindChildAt path db fisIn) childFIsOut
      , CheckSubtreeAt path fisIn xs )
  CheckSubtreeAt path fisIn
    ('FieldInfo _ db ('RFFromHere ('RecordInfo _ childFIsOut) _) ': xs) =
      ( CheckSubtreeAt (Snoc path db) (FindChildAt path db fisIn) childFIsOut
      , CheckSubtreeAt path fisIn xs )
  CheckSubtreeAt path fisIn (_ ': xs) = CheckSubtreeAt path fisIn xs

-- | Returning shape must be reachable from the input tree: each relation branch
-- in @rOut@ must exist in @rIn@. Plain columns in @rOut@ are not compared to @rIn@
-- (see 'CheckSubtreeAt'). Used by tree @*JSON@ returning rules, not flat DML.
type family ReturningIsSubtree (ann :: Ann) (rIn :: Type) (rOut :: Type) :: Constraint where
  ReturningIsSubtree ann rIn rOut =
    CheckSubtreeAt '[] (TRecordInfo ann rIn) (TRecordInfo ann rOut)

--------------------------------------------------------------------------------
-- Returning row optionality (Maybe) vs input mandatory coverage
--------------------------------------------------------------------------------

type family AnnChild (ann :: Ann) (childTab :: NameNSK) :: Ann where
  AnnChild ('Ann ren sch _ _) childTab = 'Ann ren sch 0 childTab

type family InnerRow (r :: Type) :: Type where
  InnerRow (Maybe r) = r
  InnerRow r = TypeError
    ( Text "Update returning row must be wrapped in Maybe."
    :$$: Text "Got: " :<>: ShowType r )

type family RequireMaybeRow (r :: Type) :: Constraint where
  RequireMaybeRow (Maybe _) = ()
  RequireMaybeRow r = TypeError
    ( Text "Update returning row must be Maybe ..."
    :$$: Text "Got: " :<>: ShowType r )

-- | Flat @RETURNING@ row must not be wrapped in @Maybe@ (use @IO [Maybe r']@ on
-- 'updateByKey' for per-row absence). Nullable columns may still be @Maybe@ fields.
type family RequireBareRow (r :: Type) :: Constraint where
  RequireBareRow r = RequireBareRow' r

type family RequireBareRow' (r :: Type) :: Constraint where
  RequireBareRow' (Maybe x) = TypeError
    ( Text "Flat returning row must not be wrapped in Maybe."
    :$$: Text "Use IO [Maybe r'] on updateByKey when a row may be absent."
    :$$: Text "Got: " :<>: ShowType (Maybe x) )
  RequireBareRow' _ = ()

type family ListElem (t :: Type) :: Type where
  ListElem [e] = e
  ListElem t = TypeError
    ( Text "Expected a Haskell list type for a child branch."
    :$$: Text "Got: " :<>: ShowType t )

type family SymNatName (sn :: SymNat) :: Symbol where
  SymNatName '(s, _) = s

type family ColTypeByJsonName (name :: Symbol) (cols :: [ColInfo NameNSK]) :: Type where
  ColTypeByJsonName name '[] = TypeError
    ( Text "Returning field not found in output type: " :<>: ShowType name )
  ColTypeByJsonName name ('ColInfo sn t _ _ ': xs) =
    If (SymNatName sn == name) t (ColTypeByJsonName name xs)

type family CoveredRs (ann :: Ann) (fis :: [FieldInfo Symbol]) :: [Symbol] where
  CoveredRs ann '[] = '[]
  CoveredRs ann ('FieldInfo _ db ('RFPlain _) ': xs) = db ': CoveredRs ann xs
  CoveredRs ('Ann ren sch d tab)
    ('FieldInfo _ _ ('RFToHere ('RecordInfo _ _) _) ': xs) =
    CoveredRs ('Ann ren sch d tab) xs
  CoveredRs ann (_ ': xs) = CoveredRs ann xs

type family AssertNoMaybe (path :: [Symbol]) (tab :: NameNSK) (fld :: Symbol) (t :: Type)
  :: Constraint where
  AssertNoMaybe path tab fld (Maybe _) = TypeError
    ( Text "Returning must not use Maybe here (insert or upsert insert-capable node)."
    :$$: Text "At path: " :<>: ShowType path
    :$$: Text "Table: " :<>: ShowType tab
    :$$: Text "Field: " :<>: ShowType fld )
  AssertNoMaybe path tab fld _ = ()

type family AssertMustBeMaybe (path :: [Symbol]) (tab :: NameNSK) (fld :: Symbol)
  (t :: Type) :: Constraint where
  AssertMustBeMaybe path tab fld (Maybe _) = ()
  AssertMustBeMaybe path tab fld t = TypeError
    ( Text "Returning must use Maybe here (update or key-only upsert)."
    :$$: Text "At path: " :<>: ShowType path
    :$$: Text "Table: " :<>: ShowType tab
    :$$: Text "Field: " :<>: ShowType fld
    :$$: Text "Got: " :<>: ShowType t )

type family CheckUpsertListElem (path :: [Symbol]) (tab :: NameNSK) (fld :: Symbol)
  (restMandatory :: [Symbol]) (elemTy :: Type) :: Constraint where
  CheckUpsertListElem path tab fld '[] elemTy =
    AssertNoMaybe path tab fld (ListElem elemTy)
  CheckUpsertListElem path tab fld (_ ': _) elemTy =
    AssertMustBeMaybe path tab fld (ListElem elemTy)

type family SkipOutField (db :: Symbol) (fis :: [FieldInfo Symbol])
  :: [FieldInfo Symbol] where
  SkipOutField db '[] = '[]
  SkipOutField db ('FieldInfo _ db _ ': xs) = xs
  SkipOutField db (_ ': xs) = SkipOutField db xs

type family CheckReturningUpsertAt (path :: [Symbol]) (ann :: Ann) (rIn :: Type)
  (rOut :: Type) (fisIn :: [FieldInfo Symbol]) (fisOut :: [FieldInfo Symbol])
  :: Constraint where
  CheckReturningUpsertAt path ann rIn rOut '[] '[] = ()
  CheckReturningUpsertAt path ('Ann ren sch d tab) rIn rOut fisIn
    ('FieldInfo jsonName db ('RFToHere ('RecordInfo childTab childFIsOut) _) ': outs) =
    ( CheckUpsertListElem path tab jsonName
        (RestMandatory sch tab (CoveredRs ('Ann ren sch d tab) fisIn))
        (ColTypeByJsonName jsonName (Cols ('Ann ren sch d tab) rOut))
    , CheckReturningUpsertAt (Snoc path db) (AnnChild ('Ann ren sch d tab) childTab) rIn rOut
        (FindChildAt path db fisIn) childFIsOut
    , CheckReturningUpsertAt path ('Ann ren sch d tab) rIn rOut fisIn (SkipOutField db outs) )
  CheckReturningUpsertAt path ann rIn rOut
    (_ ': ins) ('FieldInfo _ db _ ': outs) =
    CheckReturningUpsertAt path ann rIn rOut ins (SkipOutField db outs)
  CheckReturningUpsertAt path ann rIn rOut fisIn fisOut =
    CheckSubtreeAt path fisIn fisOut

type family CheckReturningUpdateAt (path :: [Symbol]) (ann :: Ann) (rIn :: Type)
  (rOut :: Type) (fisIn :: [FieldInfo Symbol]) (fisOut :: [FieldInfo Symbol])
  :: Constraint where
  CheckReturningUpdateAt path ann rIn rOut '[] '[] = ()
  CheckReturningUpdateAt path ('Ann ren sch d tab) rIn rOut fisIn
    ('FieldInfo jsonName db ('RFToHere ('RecordInfo childTab childFIsOut) _) ': outs) =
    ( AssertMustBeMaybe path tab jsonName
        (ListElem (ColTypeByJsonName jsonName (Cols ('Ann ren sch d tab) rOut)))
    , CheckReturningUpdateAt (Snoc path db) (AnnChild ('Ann ren sch d tab) childTab) rIn rOut
        (FindChildAt path db fisIn) childFIsOut
    , CheckReturningUpdateAt path ('Ann ren sch d tab) rIn rOut fisIn (SkipOutField db outs) )
  CheckReturningUpdateAt path ann rIn rOut
    (_ ': ins) ('FieldInfo _ db _ ': outs) =
    CheckReturningUpdateAt path ann rIn rOut ins (SkipOutField db outs)
  CheckReturningUpdateAt path ann rIn rOut fisIn fisOut =
    CheckSubtreeAt path fisIn fisOut

type family CheckReturningInsertAt (path :: [Symbol]) (ann :: Ann) (rIn :: Type)
  (rOut :: Type) (fisIn :: [FieldInfo Symbol]) (fisOut :: [FieldInfo Symbol])
  :: Constraint where
  CheckReturningInsertAt path ann rIn rOut '[] '[] = ()
  CheckReturningInsertAt path ('Ann ren sch d tab) rIn rOut fisIn
    ('FieldInfo jsonName db ('RFToHere ('RecordInfo childTab childFIsOut) _) ': outs) =
    ( AssertNoMaybe path tab jsonName
        (ColTypeByJsonName jsonName (Cols ('Ann ren sch d tab) rOut))
    , CheckReturningInsertAt (Snoc path db) (AnnChild ('Ann ren sch d tab) childTab) rIn rOut
        (FindChildAt path db fisIn) childFIsOut
    , CheckReturningInsertAt path ('Ann ren sch d tab) rIn rOut fisIn (SkipOutField db outs) )
  CheckReturningInsertAt path ann rIn rOut
    (_ ': ins) ('FieldInfo _ db _ ': outs) =
    CheckReturningInsertAt path ann rIn rOut ins (SkipOutField db outs)
  CheckReturningInsertAt path ann rIn rOut fisIn fisOut =
    CheckSubtreeAt path fisIn fisOut

-- | Checks that tree @RETURNING@ type @rOut@ matches input @rIn@ after insert:
--
-- * Each relation branch in @rOut@ exists in @rIn@ at the same path; plain columns
--   in @rOut@ need not appear in @rIn@ ('CheckSubtreeAt').
-- * For every child list in @rOut@: the list element type must not be @Maybe@
--   ('AssertNoMaybe').
type family ReturningMatchesInsert (ann :: Ann) (rIn :: Type) (rOut :: Type)
  :: Constraint where
  ReturningMatchesInsert ann rIn rOut =
    ( ReturningIsSubtree ann rIn rOut
    , CheckReturningInsertAt '[] ann rIn rOut
        (TRecordInfo ann rIn) (TRecordInfo ann rOut) )

-- | Checks that tree @RETURNING@ type @rOut@ matches input @rIn@ after upsert:
--
-- * Same relation-subtree rules as 'ReturningMatchesInsert'.
-- * For each child list in @rOut@: if @rIn@ still lacks mandatory plain columns at
--   that node, the element type must be @Maybe@; otherwise it must be bare
--   ('CheckUpsertListElem').
type family ReturningMatchesUpsert (ann :: Ann) (rIn :: Type) (rOut :: Type)
  :: Constraint where
  ReturningMatchesUpsert ann rIn rOut =
    ( ReturningIsSubtree ann rIn rOut
    , CheckReturningUpsertAt '[] ann rIn rOut
        (TRecordInfo ann rIn) (TRecordInfo ann rOut) )

-- | Checks that tree @RETURNING@ type @rOut@ matches input @rIn@ after update:
--
-- * @rOut@ must be @Maybe row@ ('RequireMaybeRow'); checks apply to 'InnerRow rOut'.
-- * Each relation branch in that row exists in @rIn@ at the same path; plain columns
--   in the returning row need not appear in @rIn@.
-- * For every child list there: the element type must be @Maybe@
--   ('AssertMustBeMaybe').
type family ReturningMatchesUpdate (ann :: Ann) (rIn :: Type) (rOut :: Type)
  :: Constraint where
  ReturningMatchesUpdate ann rIn rOut =
    ( RequireMaybeRow rOut
    , ReturningIsSubtree ann rIn (InnerRow rOut)
    , CheckReturningUpdateAt '[] ann rIn (InnerRow rOut)
        (TRecordInfo ann rIn) (TRecordInfo ann (InnerRow rOut)) )