git.iko.soy/rel8
on 8301eb7 help sign in
rel8/src/Rel8/Schema/Reify.hs
74 lines 1.9 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.Context.Label ( Labelable, labeler, unlabeler )
27import Rel8.Schema.HTable ( HTable, hmap )
28import Rel8.Schema.Kind ( Context )
31type Reify :: Context -> Context
32data Reify context a
35instance Interpretation (Reify context) where
36 newtype Col (Reify context) spec = Reify (Col context spec)
39instance Labelable context => Labelable (Reify context) where
40 labeler (Reify a) = Reify (labeler a)
41 unlabeler (Reify a) = Reify (unlabeler a)
44hreify :: HTable t => t (Col context) -> t (Col (Reify context))
45hreify = hmap Reify
48hunreify :: HTable t => t (Col (Reify context)) -> t (Col context)
49hunreify = hmap (\(Reify a) -> a)
52type UnwrapReify :: Context -> Context
53type family UnwrapReify context where
54 UnwrapReify (Reify context) = context
57type IsReify :: Context -> Bool
58type family IsReify context where
59 IsReify (Reify _) = 'True
60 IsReify _ = 'False
63type NotReify :: Context -> Constraint
64class IsReify context ~ 'False => NotReify context
65instance IsReify context ~ 'False => NotReify context
68notReify :: forall context ctx a. NotReify context => context :~: Reify ctx -> a
69notReify refl = case lemma @context of
70 Refl -> case refl of
73lemma :: NotReify context => IsReify context :~: 'False
74lemma = Refl