git.iko.soy/rel8
on 07daf4f help sign in
rel8/src/Rel8/Schema/Reify.hs
68 lines 1.6 kB history raw
1{-# language AllowAmbiguousTypes #-}
2{-# language EmptyCase #-}
3{-# language DataKinds #-}
4{-# language FlexibleInstances #-}
5{-# language ScopedTypeVariables #-}
6{-# language StandaloneKindSignatures #-}
7{-# language TypeApplications #-}
8{-# language TypeFamilies #-}
9{-# language TypeOperators #-}
10{-# language UndecidableInstances #-}
12module Rel8.Schema.Reify
13 ( Reify, Col( Reify ), hreify, hunreify
14 , UnwrapReify
15 , NotReify, notReify
16 )
17where
19-- base
20import Data.Kind ( Constraint )
21import Data.Type.Equality ( (:~:)( Refl ) )
22import Prelude
24-- rel8
25import Rel8.Schema.Context ( Interpretation, Col )
26import Rel8.Schema.HTable ( HTable, hmap )
27import Rel8.Schema.Kind ( Context )
30type Reify :: Context -> Context
31data Reify context a
34instance Interpretation (Reify context) where
35 newtype Col (Reify context) spec = Reify (Col context spec)
38hreify :: HTable t => t (Col context) -> t (Col (Reify context))
39hreify = hmap Reify
42hunreify :: HTable t => t (Col (Reify context)) -> t (Col context)
43hunreify = hmap (\(Reify a) -> a)
46type UnwrapReify :: Context -> Context
47type family UnwrapReify context where
48 UnwrapReify (Reify context) = context
51type IsReify :: Context -> Bool
52type family IsReify context where
53 IsReify (Reify _) = 'True
54 IsReify _ = 'False
57type NotReify :: Context -> Constraint
58class IsReify context ~ 'False => NotReify context
59instance IsReify context ~ 'False => NotReify context
62notReify :: forall context ctx a. NotReify context => context :~: Reify ctx -> a
63notReify refl = case lemma @context of
64 Refl -> case refl of
67lemma :: NotReify context => IsReify context :~: 'False
68lemma = Refl