Get rid of Rel8.Table.Unreify and all remaining uses of QuantifiedCon…

…straints (#103)

But we need more proofs

rel8.cabal

@@ -81,6 +81,7 @@ library
     Rel8.Kind.Algebra
     Rel8.Kind.Context
 
+    Rel8.Generic.Coherence
     Rel8.Generic.Construction
     Rel8.Generic.Construction.ADT
     Rel8.Generic.Construction.Record
@@ -114,6 +115,7 @@ library
     Rel8.Query.Values
 
     Rel8.Schema.Context
+    Rel8.Schema.Context.Abstract
     Rel8.Schema.Context.Nullify
     Rel8.Schema.Dict
     Rel8.Schema.HTable
@@ -164,7 +166,6 @@ library
     Rel8.Table.Serialize
     Rel8.Table.These
     Rel8.Table.Undefined
-    Rel8.Table.Unreify
 
     Rel8.Type
     Rel8.Type.Array

src/Rel8/Aggregate.hs

@@ -41,7 +41,7 @@ import Rel8.Schema.Result ( Result )
 import Rel8.Schema.Spec ( Spec( Spec ) )
 import Rel8.Table
   ( Table, Columns, Context, fromColumns, toColumns
-  , reify, unreify
+  , reify, unreify, coherence, congruence
   )
 import Rel8.Table.Recontextualize ( Recontextualize )
 import Rel8.Type ( DBType )
@@ -73,6 +73,8 @@ instance Sql DBType a => Table Aggregate (Aggregate a) where
 
   reify = notReify
   unreify = notReify
+  coherence = notReify
+  congruence = notReify
 
 
 instance Sql DBType a =>

src/Rel8/Column.hs

@@ -2,7 +2,9 @@
 {-# language FlexibleContexts #-}
 {-# language LambdaCase #-}
 {-# language MultiParamTypeClasses #-}
+{-# language ScopedTypeVariables #-}
 {-# language StandaloneKindSignatures #-}
+{-# language TypeApplications #-}
 {-# language TypeFamilies #-}
 
 module Rel8.Column
@@ -13,6 +15,7 @@ where
 
 -- base
 import Data.Kind ( Type )
+import Data.Type.Equality ( (:~:)( Refl ) )
 import Prelude
 
 -- rel8
@@ -25,11 +28,11 @@ import qualified Rel8.Schema.Kind as K
 import Rel8.Schema.Name ( Name(..), Col( N ) )
 import Rel8.Schema.Null ( Sql )
 import Rel8.Schema.Reify ( Reify, Col(..) )
-import Rel8.Schema.Result ( Col( R ), Result )
+import Rel8.Schema.Result ( Col( R ), Result, absurd )
 import Rel8.Schema.Spec ( Spec( Spec ) )
 import Rel8.Table
   ( Table, Columns, Context, fromColumns, toColumns
-  , Unreify, reify, unreify
+  , Unreify, reify, unreify, coherence, congruence
   )
 import Rel8.Table.Recontextualize ( Recontextualize )
 import Rel8.Type ( DBType )
@@ -63,11 +66,22 @@ instance (Reifiable context, Sql DBType a) =>
   reify _ = AColumn
   unreify _ (AColumn a) = a
 
+  coherence Refl = case contextSing @context of
+    SAggregate -> const Refl
+    SExpr -> const Refl
+    SName -> const Refl
+    SResult -> absurd
+    SReify _ -> const Refl
 
-instance
-  ( Reifiable context, Reifiable context'
-  , Sql DBType a
-  ) =>
+  congruence Refl = case contextSing @context of
+    SAggregate -> const Refl
+    SExpr -> const Refl
+    SName -> const Refl
+    SResult -> absurd
+    SReify _ -> const Refl
+
+
+instance (Reifiable context, Reifiable context',  Sql DBType a) =>
   Recontextualize
     (Reify context)
     (Reify context')

src/Rel8/Column/ADT.hs

@@ -1,7 +1,9 @@
 {-# language DataKinds #-}
 {-# language LambdaCase #-}
 {-# language MultiParamTypeClasses #-}
+{-# language ScopedTypeVariables #-}
 {-# language StandaloneKindSignatures #-}
+{-# language TypeApplications #-}
 {-# language TypeFamilies #-}
 {-# language UndecidableInstances #-}
 
@@ -12,6 +14,7 @@ where
 
 -- base
 import Data.Kind ( Type )
+import Data.Type.Equality ( (:~:)( Refl ) )
 import Prelude
 
 -- rel8
@@ -20,12 +23,13 @@ import Rel8.Kind.Context ( SContext(..), Reifiable, contextSing )
 import Rel8.Schema.Context ( Col )
 import qualified Rel8.Schema.Kind as K
 import Rel8.Schema.Reify ( Reify, hreify, hunreify )
-import Rel8.Schema.Result ( Result )
+import Rel8.Schema.Result ( Result, absurd )
 import Rel8.Table
   ( Table, Columns, Context, fromColumns, toColumns
-  , Unreify, reify, unreify
+  , Unreify, reify, unreify, coherence, congruence
   )
 import Rel8.Table.ADT ( ADT( ADT ), ADTable, fromADT, toADT )
+import Rel8.Table.Rel8able ()
 import Rel8.Table.Recontextualize ( Recontextualize )
 
 
@@ -52,6 +56,20 @@ instance (ADTable t, Reifiable context) =>
   reify _ = AHADT
   unreify _ (AHADT a) = a
 
+  coherence = case contextSing @context of
+    SAggregate -> \Refl _ -> Refl
+    SExpr -> \Refl _ -> Refl
+    SName -> \Refl _ -> Refl
+    SResult -> \Refl -> absurd
+    SReify _ -> \Refl _ -> Refl
+
+  congruence = case contextSing @context of
+    SAggregate -> \_ _ -> Refl
+    SExpr -> \_ _ -> Refl
+    SName -> \_ _ -> Refl
+    SResult -> \Refl -> absurd
+    SReify _ -> \_ _ -> Refl
+
 
 instance
   ( Reifiable context, Reifiable context'

src/Rel8/Column/Either.hs

@@ -2,7 +2,9 @@
 {-# language FlexibleContexts #-}
 {-# language LambdaCase #-}
 {-# language MultiParamTypeClasses #-}
+{-# language ScopedTypeVariables #-}
 {-# language StandaloneKindSignatures #-}
+{-# language TypeApplications #-}
 {-# language TypeFamilyDependencies #-}
 {-# language UndecidableInstances #-}
 
@@ -13,9 +15,11 @@ where
 
 -- base
 import Control.Applicative ( liftA2 )
+import Control.Category ( id )
 import Data.Bifunctor ( Bifunctor, bimap )
 import Data.Kind ( Type )
-import Prelude
+import Data.Type.Equality ( (:~:)( Refl ), apply )
+import Prelude hiding ( id )
 
 -- rel8
 import Rel8.Aggregate ( Aggregate )
@@ -26,10 +30,10 @@ import Rel8.Schema.HTable.Either ( HEitherTable )
 import qualified Rel8.Schema.Kind as K
 import Rel8.Schema.Name ( Name(..) )
 import Rel8.Schema.Reify ( Reify, hreify, hunreify )
-import Rel8.Schema.Result ( Result )
+import Rel8.Schema.Result ( Result, absurd )
 import Rel8.Table
   ( Table, Columns, Context, fromColumns, toColumns
-  , Unreify, reify, unreify
+  , Unreify, reify, unreify, coherence, congruence
   )
 import Rel8.Table.Either ( EitherTable )
 import Rel8.Table.Recontextualize ( Recontextualize )
@@ -71,6 +75,32 @@ instance (Reifiable context, Table (Reify context) a, Table (Reify context) b)
   reify proof = liftA2 bimap reify reify proof . AHEither
   unreify proof = (\(AHEither a) -> a) . liftA2 bimap unreify unreify proof
 
+  coherence = case contextSing @context of
+    SAggregate -> coherence @(Reify context) @a
+    SExpr -> coherence @(Reify context) @a
+    SName -> coherence @(Reify context) @a
+    SResult -> \Refl -> absurd
+    SReify _ -> \Refl _ -> Refl
+
+  congruence proof@Refl abstract = case contextSing @context of
+    SAggregate ->
+      id `apply`
+      congruence @(Reify context) @a proof abstract `apply`
+      congruence @(Reify context) @b proof abstract
+    SExpr ->
+      id `apply`
+      congruence @(Reify context) @a proof abstract `apply`
+      congruence @(Reify context) @b proof abstract
+    SName ->
+      id `apply`
+      congruence @(Reify context) @a proof abstract `apply`
+      congruence @(Reify context) @b proof abstract
+    SResult -> absurd abstract
+    SReify _ ->
+      id `apply`
+      congruence @(Reify context) @a proof abstract `apply`
+      congruence @(Reify context) @b proof abstract
+
 
 instance
   ( Reifiable context, Reifiable context'

src/Rel8/Column/Lift.hs

@@ -1,7 +1,9 @@
 {-# language DataKinds #-}
 {-# language LambdaCase #-}
 {-# language MultiParamTypeClasses #-}
+{-# language ScopedTypeVariables #-}
 {-# language StandaloneKindSignatures #-}
+{-# language TypeApplications #-}
 {-# language TypeFamilies #-}
 
 module Rel8.Column.Lift
@@ -11,6 +13,7 @@ where
 
 -- base
 import Data.Kind ( Type )
+import Data.Type.Equality ( (:~:)( Refl ) )
 import Prelude
 
 -- rel8
@@ -19,10 +22,10 @@ import Rel8.Kind.Context ( Reifiable(..), SContext(..) )
 import Rel8.Schema.Context ( Col )
 import qualified Rel8.Schema.Kind as K
 import Rel8.Schema.Reify ( Reify, hreify, hunreify )
-import Rel8.Schema.Result ( Result )
+import Rel8.Schema.Result ( Result, absurd )
 import Rel8.Table
   ( Table, Columns, Context, fromColumns, toColumns
-  , Unreify, reify, unreify
+  , Unreify, reify, unreify, coherence, congruence
   )
 import Rel8.Table.Rel8able ()
 import Rel8.Table.HKD ( HKD( HKD ), HKDable, fromHKD, toHKD )
@@ -54,6 +57,20 @@ instance (Reifiable context, HKDable a) =>
   reify _ = ALift
   unreify _ (ALift a) = a
 
+  coherence = case contextSing @context of
+    SAggregate -> \Refl _ -> Refl
+    SExpr -> \Refl _ -> Refl
+    SName -> \Refl _ -> Refl
+    SResult -> \Refl -> absurd
+    SReify _ -> \Refl _ -> Refl
+
+  congruence = case contextSing @context of
+    SAggregate -> \_ _ -> Refl
+    SExpr -> \_ _ -> Refl
+    SName -> \_ _ -> Refl
+    SResult -> \Refl -> absurd
+    SReify _ -> \_ _ -> Refl
+
 
 instance (Reifiable context, Reifiable context', HKDable a) =>
   Recontextualize