@@ -1,4 +1,11 @@
11{-# language DataKinds #-}
2+{-# language FlexibleContexts #-}
3+{-# language FlexibleInstances #-}
4+{-# language GADTs #-}
5+{-# language LambdaCase #-}
6+{-# language MultiParamTypeClasses #-}
7+{-# language QuantifiedConstraints #-}
8+{-# language RankNTypes #-}
29{-# language StandaloneKindSignatures #-}
310{-# language TypeFamilies #-}
411{-# language UndecidableInstances #-}
@@ -20,7 +27,8 @@
2027-- @Table@)
2128
2229module Rel8.Table.Unreify
23− ( Unreifiable
30+ ( Unreifiable, Unreifiability( Unreifiability ), unreifiability
31+ , Unreifies
2432 )
2533where
2634
@@ -29,15 +37,73 @@ import Data.Kind ( Constraint, Type )
2937import Prelude ()
3038
3139-- rel8
40+import Rel8.Aggregate ( Aggregate )
41+import Rel8.Expr ( Expr )
42+import Rel8.Kind.Context ( SContext(..), Reifiable, sReifiable )
43+import Rel8.Schema.Dict ( Dict( Dict ) )
44+import Rel8.Schema.Insert ( Insert )
3245import qualified Rel8.Schema.Kind as K
46+import Rel8.Schema.Name ( Name )
3347import Rel8.Schema.Reify ( Reify )
34−import Rel8.Table ( Table, Columns, Unreify )
48+import Rel8.Schema.Result ( Result )
49+import Rel8.Table ( Table, Context, Congruent, Unreify )
3550
3651
37−type Unreifiable :: K.Context -> Type -> Constraint
38−type family Unreifiable context a where
39− Unreifiable (Reify context) a =
40− ( Table context (Unreify a)
41− , Columns a ~ Columns (Unreify a)
42− )
43− Unreifiable _ _ = ()
52+type Unreifies :: K.Context -> Type -> Constraint
53+type family Unreifies context a where
54+ Unreifies (Reify context) a = Unreifier context a
55+ Unreifies _ _ = ()
56+
57+
58+type Unreifiable :: Type -> Constraint
59+class
60+ ( Context a ~ Reify Aggregate => Unreifier Aggregate a
61+ , Context a ~ Reify Expr => Unreifier Expr a
62+ , Context a ~ Reify Insert => Unreifier Insert a
63+ , Context a ~ Reify Name => Unreifier Name a
64+ , Context a ~ Reify Result => Unreifier Result a
65+ , (forall ctx. (Context a ~ Reify (Reify ctx), Reifiable ctx) => Unreifier (Reify ctx) a)
66+ )
67+ => Unreifiable a
68+instance
69+ ( Context a ~ Reify Aggregate => Unreifier Aggregate a
70+ , Context a ~ Reify Expr => Unreifier Expr a
71+ , Context a ~ Reify Insert => Unreifier Insert a
72+ , Context a ~ Reify Name => Unreifier Name a
73+ , Context a ~ Reify Result => Unreifier Result a
74+ , (forall ctx. (Context a ~ Reify (Reify ctx), Reifiable ctx) => Unreifier (Reify ctx) a)
75+ )
76+ => Unreifiable a
77+
78+
79+type Unreifier :: K.Context -> Type -> Constraint
80+class
81+ ( Table (Reify context) a
82+ , Table context (Unreify a)
83+ , Congruent a (Unreify a)
84+ )
85+ => Unreifier context a
86+instance
87+ ( Table (Reify context) a
88+ , Table context (Unreify a)
89+ , Congruent a (Unreify a)
90+ )
91+ => Unreifier context a
92+
93+
94+type Unreifiability :: K.Context -> Type -> Type
95+data Unreifiability context a where
96+ Unreifiability :: Unreifier context a
97+ => SContext context -> Unreifiability context a
98+
99+
100+unreifiability :: (Context a ~ Reify context, Unreifiable a)
101+ => SContext context -> Unreifiability context a
102+unreifiability = \case
103+ SAggregate -> Unreifiability SAggregate
104+ SExpr -> Unreifiability SExpr
105+ SInsert -> Unreifiability SInsert
106+ SName -> Unreifiability SName
107+ SResult -> Unreifiability SResult
108+ SReify context -> case sReifiable context of
109+ Dict -> Unreifiability (SReify context)