Unrolled some type families

squeal-postgresql/src/Squeal/PostgreSQL/List.hs

@@ -84,7 +84,12 @@ infixl 9 *:
 -- | @Elem@ is a promoted `Data.List.elem`.
 type family Elem x xs where
   Elem x '[] = 'False
-  Elem x (x ': xs) = 'True
+  Elem x (x ': _) = 'True
+  Elem x (_ ': x ': _) = 'True
+  Elem x (_ ': _ ': x ': _) = 'True
+  Elem x (_ ': _ ': _ ': x ': _) = 'True
+  Elem x (_ ': _ ': _ ': _ ': x ': _) = 'True
+  Elem x (_ ': _ ': _ ': _ ': _ ': x ': _) = 'True
   Elem x (_ ': xs) = Elem x xs
 
 -- | @In x xs@ is a constraint that proves that @x@ is in @xs@.
@@ -99,5 +104,9 @@ Length '[Char,String,Bool,Double] :: Nat
 = 4
 -}
 type family Length (xs :: [k]) :: Nat where
-  Length (x : xs) = 1 + Length xs
+  Length (_ ': _ ': _ ': _ ': _ : xs) = 5 + Length xs
+  Length (_ ': _ ': _ ': _ : xs) = 4 + Length xs
+  Length (_ ': _ ': _ : xs) = 3 + Length xs
+  Length (_ ': _ : xs) = 2 + Length xs
+  Length (_ : xs) = 1 + Length xs
   Length '[] = 0

squeal-postgresql/src/Squeal/PostgreSQL/PG.hs

@@ -178,8 +178,16 @@ type family RowPG (hask :: Type) :: RowType where
 
 -- | `RowOf` applies `NullPG` to the fields of a list.
 type family RowOf (record :: [(Symbol, Type)]) :: RowType where
-  RowOf '[] = '[]
+  RowOf (col ::: ty ': col1 ::: ty1 ': col2 ::: ty2 ': col3 ::: ty3 ': col4 ::: ty4 ': record) =
+    col ::: NullPG ty ': col1 ::: NullPG ty1 ': col2 ::: NullPG ty2 ': col3 ::: NullPG ty3 ': col4 ::: NullPG ty4 ': RowOf record
+  RowOf (col ::: ty ': col1 ::: ty1 ': col2 ::: ty2 ': col3 ::: ty3 ': record) =
+    col ::: NullPG ty ': col1 ::: NullPG ty1 ': col2 ::: NullPG ty2 ': col3 ::: NullPG ty3 ': RowOf record
+  RowOf (col ::: ty ': col1 ::: ty1 ': col2 ::: ty2 ': record) =
+    col ::: NullPG ty ': col1 ::: NullPG ty1 ': col2 ::: NullPG ty2 ': RowOf record
+  RowOf (col ::: ty ': col1 ::: ty1 ': record) =
+    col ::: NullPG ty ': col1::: NullPG ty1 ': RowOf record
   RowOf (col ::: ty ': record) = col ::: NullPG ty ': RowOf record
+  RowOf '[] = '[]
 
 {- | `NullPG` turns a Haskell type into a `NullityType`.
 
@@ -206,8 +214,17 @@ type family TuplePG (hask :: Type) :: [NullityType] where
 
 -- | `TupleOf` turns a list of Haskell `Type`s into a list of `NullityType`s.
 type family TupleOf (tuple :: [Type]) :: [NullityType] where
-  TupleOf '[] = '[]
+  TupleOf (hask ': hask1 ': hask2 ': hask3 ': hask4 ': hask5 ': tuple) =
+    NullPG hask ': NullPG hask1 ': NullPG hask2 ': NullPG hask3 ': NullPG hask4 ': NullPG hask5 ': TupleOf tuple
+  TupleOf (hask ': hask1 ': hask2 ': hask3 ': hask4 ': tuple) =
+    NullPG hask ': NullPG hask1 ': NullPG hask2 ': NullPG hask3 ': NullPG hask4 ': TupleOf tuple
+  TupleOf (hask ': hask1 ': hask2 ': hask3 ': tuple) =
+    NullPG hask ': NullPG hask1 ': NullPG hask2 ': NullPG hask3 ': TupleOf tuple
+  TupleOf (hask ': hask1 ': hask2 ': tuple) =
+    NullPG hask ': NullPG hask1 ': NullPG hask2 ': TupleOf tuple
+  TupleOf (hask ': hask1 ': tuple) = NullPG hask ': NullPG hask1 ': TupleOf tuple
   TupleOf (hask ': tuple) = NullPG hask ': TupleOf tuple
+  TupleOf '[] = '[]
 
 -- | `TupleCodeOf` takes the `SOP.Code` of a haskell `Type`
 -- and if it's a simple product returns it, otherwise giving a `TypeError`.

squeal-postgresql/src/Squeal/PostgreSQL/Schema.hs

@@ -260,9 +260,19 @@ type FromType = [(Symbol,RowType)]
 
 -- | `ColumnsToRow` removes column constraints.
 type family ColumnsToRow (columns :: ColumnsType) :: RowType where
-  ColumnsToRow '[] = '[]
-  ColumnsToRow (column ::: constraint :=> ty ': columns) =
+  ColumnsToRow (column ::: _ :=> ty ': column1 ::: _ :=> ty1 ': column2 ::: _ :=> ty2 ': column3 ::: _ :=> ty3 ': column4 ::: _ :=> ty4 ': column5 ::: _ :=> ty5 ': columns) =
+    column ::: ty ': column1 ::: ty1 ': column2 ::: ty2 ': column3 ::: ty3 ': column4 ::: ty4 ': column5 ::: ty5 ': ColumnsToRow columns
+  ColumnsToRow (column ::: _ :=> ty ': column1 ::: _ :=> ty1 ': column2 ::: _ :=> ty2 ': column3 ::: _ :=> ty3 ': column4 ::: _ :=> ty4 ': columns) =
+    column ::: ty ': column1 ::: ty1 ': column2 ::: ty2 ': column3 ::: ty3 ': column4 ::: ty4 ': ColumnsToRow columns
+  ColumnsToRow (column ::: _ :=> ty ': column1 ::: _ :=> ty1 ': column2 ::: _ :=> ty2 ': column3 ::: _ :=> ty3 ': columns) =
+    column ::: ty ': column1 ::: ty1 ': column2 ::: ty2 ': column3 ::: ty3 ': ColumnsToRow columns
+  ColumnsToRow (column ::: _ :=> ty ': column1 ::: _ :=> ty1 ': column2 ::: _ :=> ty2 ': columns) =
+    column ::: ty ': column1 ::: ty1 ': column2 ::: ty2 ': ColumnsToRow columns
+  ColumnsToRow (column ::: _ :=> ty ': column1 ::: _ :=> ty1 ': columns) =
+    column ::: ty ': column1 ::: ty1 ': ColumnsToRow columns
+  ColumnsToRow (column ::: _ :=> ty ': columns) =
     column ::: ty ': ColumnsToRow columns
+  ColumnsToRow '[] = '[]
 
 -- | `TableToColumns` removes table constraints.
 type family TableToColumns (table :: TableType) :: ColumnsType where
@@ -295,14 +305,24 @@ instance ty0 ~ ty1 => SamePGType
 
 -- | `AllNotNull` is a constraint that proves a `ColumnsType` has no @NULL@s.
 type family AllNotNull (columns :: ColumnsType) :: Constraint where
+  AllNotNull (_ ::: _ :=> 'NotNull _ ': _ ::: _ :=> 'NotNull _ ': _ ::: _ :=> 'NotNull _ ': _ ::: _ :=> 'NotNull _ ': _ ::: _ :=> 'NotNull _ ': _ ::: _ :=> 'NotNull _ ': columns) = AllNotNull columns
+  AllNotNull (_ ::: _ :=> 'NotNull _ ': _ ::: _ :=> 'NotNull _ ': _ ::: _ :=> 'NotNull _ ': _ ::: _ :=> 'NotNull _ ': _ ::: _ :=> 'NotNull _ ': columns) = AllNotNull columns
+  AllNotNull (_ ::: _ :=> 'NotNull _ ': _ ::: _ :=> 'NotNull _ ': _ ::: _ :=> 'NotNull _ ': _ ::: _ :=> 'NotNull _ ': columns) = AllNotNull columns
+  AllNotNull (_ ::: _ :=> 'NotNull _ ': _ ::: _ :=> 'NotNull _ ': _ ::: _ :=> 'NotNull _ ': columns) = AllNotNull columns
+  AllNotNull (_ ::: _ :=> 'NotNull _ ': _ ::: _ :=> 'NotNull _ ': columns) = AllNotNull columns
+  AllNotNull (_ ::: _ :=> 'NotNull _ ': columns) = AllNotNull columns
   AllNotNull '[] = ()
-  AllNotNull (column ::: def :=> 'NotNull ty ': columns) = AllNotNull columns
 
 -- | `NotAllNull` is a constraint that proves a `ColumnsType` has some
 -- @NOT NULL@.
 type family NotAllNull (columns :: ColumnsType) :: Constraint where
-  NotAllNull (column ::: def :=> 'NotNull ty ': columns) = ()
-  NotAllNull (column ::: def :=> 'Null ty ': columns) = NotAllNull columns
+  NotAllNull (_ ::: _ :=> _ _ ': _ ::: _ :=> _ _ ': _ ::: _ :=> _ _ ': _ ::: _ :=> _ _ ': _ ::: _ :=> _ _ ': _ ::: _ :=> 'NotNull _ ': _) = ()
+  NotAllNull (_ ::: _ :=> _ _ ': _ ::: _ :=> _ _ ': _ ::: _ :=> _ _ ': _ ::: _ :=> _ _ ': _ ::: _ :=> 'NotNull _ ': _) = ()
+  NotAllNull (_ ::: _ :=> _ _ ': _ ::: _ :=> _ _ ': _ ::: _ :=> _ _ ': _ ::: _ :=> 'NotNull _ ': _) = ()
+  NotAllNull (_ ::: _ :=> _ _ ': _ ::: _ :=> _ _ ': _ ::: _ :=> 'NotNull _ ': _) = ()
+  NotAllNull (_ ::: _ :=> _ _ ': _ ::: _ :=> 'NotNull _ ': _) = ()
+  NotAllNull (_ ::: _ :=> 'NotNull _ ': _) = ()
+  NotAllNull (_ ::: _ :=> 'Null _ ': columns) = NotAllNull columns
 
 -- | `NullifyType` is an idempotent that nullifies a `NullityType`.
 type family NullifyType (ty :: NullityType) :: NullityType where
@@ -311,17 +331,37 @@ type family NullifyType (ty :: NullityType) :: NullityType where
 
 -- | `NullifyRow` is an idempotent that nullifies a `RowType`.
 type family NullifyRow (columns :: RowType) :: RowType where
-  NullifyRow '[] = '[]
+  NullifyRow (column ::: ty ': column1 ::: ty1 ': column2 ::: ty2 ': column3 ::: ty3 ': column4 ::: ty4 ': column5 ::: ty5 ': columns) =
+    column ::: NullifyType ty ': column1 ::: NullifyType ty1 ': column2 ::: NullifyType ty2 ': column3 ::: NullifyType ty3 ': column4 ::: NullifyType ty4 ': column5 ::: NullifyType ty5 ': NullifyRow columns
+  NullifyRow (column ::: ty ': column1 ::: ty1 ': column2 ::: ty2 ': column3 ::: ty3 ': column4 ::: ty4 ': columns) =
+    column ::: NullifyType ty ': column1 ::: NullifyType ty1 ': column2 ::: NullifyType ty2 ': column3 ::: NullifyType ty3 ': column4 ::: NullifyType ty4 ': NullifyRow columns
+  NullifyRow (column ::: ty ': column1 ::: ty1 ': column2 ::: ty2 ': column3 ::: ty3 ': columns) =
+    column ::: NullifyType ty ': column1 ::: NullifyType ty1 ': column2 ::: NullifyType ty2 ': column3 ::: NullifyType ty3 ': NullifyRow columns
+  NullifyRow (column ::: ty ': column1 ::: ty1 ': column2 ::: ty2 ': columns) =
+    column ::: NullifyType ty ': column1 ::: NullifyType ty1 ': column2 ::: NullifyType ty2 ': NullifyRow columns
+  NullifyRow (column ::: ty ': column1 ::: ty1 ': columns) =
+    column ::: NullifyType ty ': column1 ::: NullifyType ty1 ': NullifyRow columns
   NullifyRow (column ::: ty ': columns) =
     column ::: NullifyType ty ': NullifyRow columns
+  NullifyRow '[] = '[]
 
 -- | `NullifyFrom` is an idempotent that nullifies a `FromType`
 -- used to nullify the left or right hand side of an outer join
 -- in a `Squeal.PostgreSQL.Query.FromClause`.
 type family NullifyFrom (tables :: FromType) :: FromType where
-  NullifyFrom '[] = '[]
+  NullifyFrom (table ::: columns ': table1 ::: columns1 ': table2 ::: columns2 ': table3 ::: columns3 ': table4 ::: columns4 ': table5 ::: columns5 ': tables) =
+    table ::: NullifyRow columns ': table1 ::: NullifyRow columns1 ': table2 ::: NullifyRow columns2 ': table3 ::: NullifyRow columns3 ': table4 ::: NullifyRow columns5 ': table5 ::: NullifyRow columns4 ': NullifyFrom tables
+  NullifyFrom (table ::: columns ': table1 ::: columns1 ': table2 ::: columns2 ': table3 ::: columns3 ': table4 ::: columns4 ': tables) =
+    table ::: NullifyRow columns ': table1 ::: NullifyRow columns1 ': table2 ::: NullifyRow columns2 ': table3 ::: NullifyRow columns3 ': table4 ::: NullifyRow columns4 ': NullifyFrom tables
+  NullifyFrom (table ::: columns ': table1 ::: columns1 ': table2 ::: columns2 ': table3 ::: columns3 ': tables) =
+    table ::: NullifyRow columns ': table1 ::: NullifyRow columns1 ': table2 ::: NullifyRow columns2 ': table3 ::: NullifyRow columns3 ': NullifyFrom tables
+  NullifyFrom (table ::: columns ': table1 ::: columns1 ': table2 ::: columns2 ': tables) =
+    table ::: NullifyRow columns ': table1 ::: NullifyRow columns1 ': table2 ::: NullifyRow columns2 ': NullifyFrom tables
+  NullifyFrom (table ::: columns ': table1 ::: columns1 ': tables) =
+    table ::: NullifyRow columns ': table1 ::: NullifyRow columns1 ': NullifyFrom tables
   NullifyFrom (table ::: columns ': tables) =
     table ::: NullifyRow columns ': NullifyFrom tables
+  NullifyFrom '[] = '[]
 
 -- | @Create alias x xs@ adds @alias ::: x@ to the end of @xs@ and is used in
 -- `Squeal.PostgreSQL.Definition.createTable` statements and in @ALTER TABLE@