Ticket #10527: Bug.hs

File Bug.hs, 5.2 KB (added by sopvop, 4 years ago)

testcase

Line 
1{-# LANGUAGE ConstraintKinds       #-}
2{-# LANGUAGE DataKinds             #-}
3{-# LANGUAGE FlexibleContexts      #-}
4{-# LANGUAGE FlexibleInstances     #-}
5{-# LANGUAGE GADTs                 #-}
6{-# LANGUAGE MultiParamTypeClasses #-}
7{-# LANGUAGE PolyKinds             #-}
8{-# LANGUAGE ScopedTypeVariables   #-}
9{-# LANGUAGE TypeFamilies          #-}
10{-# LANGUAGE TypeOperators         #-}
11
12module Bug where
13
14import Data.Functor.Identity
15import Data.Proxy
16import Control.Applicative (Const(..))
17
18
19data Expr a = Expr !Int String
20
21-- Stubs
22data UTCTime = UTCTime
23data NoteType = NoteType
24data EventType = EventType
25data MetaData = MetaData
26
27newtype UserId = UserId Int
28newtype EventId = EventId Int
29
30newtype (:->) s a = Col { getCol :: a }
31
32data Nat = Z | S !Nat
33
34type family RIndex (r :: k) (rs :: [k]) :: Nat where
35  RIndex r (r ': rs) = 'Z
36  RIndex r (s ': rs) = 'S (RIndex r rs)
37
38type family RImage (rs :: [k]) (ss :: [k]) :: [Nat] where
39  RImage '[] ss = '[]
40  RImage (r ': rs) ss = RIndex r ss ': RImage rs ss
41
42type family (as :: [k]) ++ (bs :: [k]) :: [k] where
43  '[] ++ bs = bs
44  (a ': as) ++ bs = a ': (as ++ bs)
45
46
47data Rec :: [*] -> * where
48  RNil :: Rec '[]
49  (:&) :: !r -> !(Rec rs) -> Rec (r ': rs)
50
51class i ~ RIndex r rs => RElem (r :: *) (rs :: [*]) (i :: Nat) where
52  rlens :: Functor g
53        => sing r
54        -> (r -> g r)
55        -> Rec rs
56        -> g (Rec rs)
57
58  rget :: sing r -> Rec rs -> r
59  rget k = getConst . rlens k Const
60  rput :: r
61       -> Rec rs
62       -> Rec rs
63  rput y = runIdentity . rlens Proxy (\_ -> Identity y)
64
65instance RElem r (r ': rs) 'Z where
66  rlens _ f (x :& xs) = fmap (:& xs) (f x)
67  {-# INLINE rlens #-}
68
69instance (RIndex r (s ': rs) ~ 'S i, RElem r rs i) => RElem r (s ': rs) ('S i) where
70  rlens p f (x :& xs) = fmap (x :&) (rlens p f xs)
71  {-# INLINE rlens #-}
72
73lens :: Functor f
74     => (t -> s)
75     -> (t -> a -> b)
76     -> (s -> f a)
77     -> t
78     -> f b
79lens sa sbt afb s = fmap (sbt s) $ afb (sa s)
80{-# INLINE lens #-}
81
82
83type IElem r rs = RElem r rs (RIndex r rs)
84
85class is ~ RImage rs ss => RSubset (rs :: [*]) (ss :: [*]) is where
86
87  -- | This is a lens into a slice of the larger record. Morally, we have:
88  --
89  -- > rsubset :: Lens' (Rec f ss) (Rec f rs)
90  rsubset
91    :: Functor g
92    => (Rec rs -> g (Rec rs))
93    -> Rec ss
94    -> g (Rec ss)
95
96  -- | The getter of the 'rsubset' lens is 'rcast', which takes a larger record
97  -- to a smaller one by forgetting fields.
98  rcast
99    :: Rec ss
100    -> Rec rs
101  rcast = getConst . rsubset Const
102  {-# INLINE rcast #-}
103
104  -- | The setter of the 'rsubset' lens is 'rreplace', which allows a slice of
105  -- a record to be replaced with different values.
106  rreplace
107    :: Rec rs
108    -> Rec ss
109    -> Rec ss
110  rreplace rs = runIdentity . rsubset (\_ -> Identity rs)
111  {-# INLINE rreplace #-}
112
113instance RSubset '[] ss '[] where
114  rsubset = lens (const RNil) const
115
116instance (RElem r ss i , RSubset rs ss is) => RSubset (r ': rs) ss (i ': is) where
117  rsubset = lens (\ss -> rget Proxy ss :& rcast ss) set
118    where
119      set :: Rec ss -> Rec (r ': rs) -> Rec ss
120      set ss (r :& rs) = rput r $ rreplace rs ss
121
122type ISubset rs ss = RSubset rs ss (RImage rs ss)
123
124
125type JournalEventColumns = '[ "id"             :-> Expr EventId
126                            , "event_type"     :-> Expr EventType
127                            , "target_id"      :-> Expr Int
128                            , "target_type"    :-> Expr String
129                            , "created_at"     :-> Expr UTCTime
130                            , "created_by"     :-> Expr UserId
131                            ]
132
133type JournalNoteColumns = '[ "id"             :-> Expr EventId
134                           , "event_type"     :-> Expr EventType
135                           , "note_type"      :-> Expr NoteType
136                           , "parent_id"      :-> Expr (Maybe EventId)
137                           , "plain_text"     :-> Expr String
138                           , "logged_time"    :-> Expr (Maybe Int)
139                           , "approved_time"  :-> Expr (Maybe Int)
140                           , "planned_time"   :-> Expr (Maybe Int)
141                           , "modified_at"    :-> Expr UTCTime
142                           , "modified_by"    :-> Expr UserId
143                           ]
144
145type JournalExpandedColumns = '[ "id"             :-> Expr EventId
146                               , "target_id"      :-> Expr Int
147                               , "target_type"    :-> Expr String
148                               , "event_type"     :-> Expr EventType
149                               , "note_type"      :-> Expr NoteType
150                               , "parent_id"      :-> Expr (Maybe EventId)
151                               , "plain_text"     :-> Expr String
152                               , "logged_time"    :-> Expr (Maybe Int)
153                               , "approved_time"  :-> Expr (Maybe Int)
154                               , "planned_time"   :-> Expr (Maybe Int)
155                               , "created_at"     :-> Expr UTCTime
156                               , "created_by"     :-> Expr UserId
157                               , "modified_at"    :-> Expr UTCTime
158                               , "modified_by"    :-> Expr UserId
159                               ]
160
161join_note :: Rec (JournalEventColumns ++ JournalNoteColumns)
162             -> Rec JournalExpandedColumns
163join_note = rcast