@@ -39,13 +39,8 @@ import GHC.TypeLits (TypeError, ErrorMessage(..))
39
39
40
40
-- | Flatten API into a list of endpoints.
41
41
--
42
- -- >>> :t showType @(Endpoints SampleAPI)
43
- -- ...
44
- -- ... :: Proxy
45
- -- ... '["hello" :> Verb 'GET 200 '[JSON] Int,
46
- -- ... "bye"
47
- -- ... :> (Capture "name" String
48
- -- ... :> Verb 'POST 200 '[JSON, PlainText] Bool)]
42
+ -- >>> Refl :: Endpoints SampleAPI :~: '["hello" :> Verb 'GET 200 '[JSON] Int, "bye" :> (Capture "name" String :> Verb 'POST 200 '[JSON, PlainText] Bool)]
43
+ -- Refl
49
44
type family Endpoints api where
50
45
Endpoints (a :<|> b ) = AppendList (Endpoints a ) (Endpoints b )
51
46
Endpoints (e :> a ) = MapSub e (Endpoints a )
@@ -70,21 +65,21 @@ type family IsElem' a s :: Constraint
70
65
-- | Closed type family, check if @endpoint@ is within @api@.
71
66
-- Uses @'IsElem''@ if it exhausts all other options.
72
67
--
73
- -- >>> ok @( IsElem ("hello" :> Get '[JSON] Int) SampleAPI)
68
+ -- >>> ok (Proxy :: Proxy ( IsElem ("hello" :> Get '[JSON] Int) SampleAPI) )
74
69
-- OK
75
70
--
76
- -- >>> ok @( IsElem ("bye" :> Get '[JSON] Int) SampleAPI)
71
+ -- >>> ok (Proxy :: Proxy ( IsElem ("bye" :> Get '[JSON] Int) SampleAPI) )
77
72
-- ...
78
- -- ... Could not deduce: ...
73
+ -- ... Could not deduce...
79
74
-- ...
80
75
--
81
76
-- An endpoint is considered within an api even if it is missing combinators
82
77
-- that don't affect the URL:
83
78
--
84
- -- >>> ok @( IsElem (Get '[JSON] Int) (Header "h" Bool :> Get '[JSON] Int))
79
+ -- >>> ok (Proxy :: Proxy ( IsElem (Get '[JSON] Int) (Header "h" Bool :> Get '[JSON] Int) ))
85
80
-- OK
86
81
--
87
- -- >>> ok @( IsElem (Get '[JSON] Int) (ReqBody '[JSON] Bool :> Get '[JSON] Int))
82
+ -- >>> ok (Proxy :: Proxy ( IsElem (Get '[JSON] Int) (ReqBody '[JSON] Bool :> Get '[JSON] Int) ))
88
83
-- OK
89
84
--
90
85
-- *N.B.:* @IsElem a b@ can be seen as capturing the notion of whether the URL
@@ -110,12 +105,12 @@ type family IsElem endpoint api :: Constraint where
110
105
111
106
-- | Check whether @sub@ is a sub-API of @api@.
112
107
--
113
- -- >>> ok @( IsSubAPI SampleAPI (SampleAPI :<|> Get '[JSON] Int))
108
+ -- >>> ok (Proxy :: Proxy ( IsSubAPI SampleAPI (SampleAPI :<|> Get '[JSON] Int) ))
114
109
-- OK
115
110
--
116
- -- >>> ok @( IsSubAPI (SampleAPI :<|> Get '[JSON] Int) SampleAPI)
111
+ -- >>> ok (Proxy :: Proxy ( IsSubAPI (SampleAPI :<|> Get '[JSON] Int) SampleAPI) )
117
112
-- ...
118
- -- ... Could not deduce: ...
113
+ -- ... Could not deduce...
119
114
-- ...
120
115
--
121
116
-- This uses @IsElem@ for checking; thus the note there applies here.
@@ -131,14 +126,14 @@ type family AllIsElem xs api :: Constraint where
131
126
132
127
-- | Closed type family, check if @endpoint@ is exactly within @api@.
133
128
--
134
- -- >>> ok @( IsIn ("hello" :> Get '[JSON] Int) SampleAPI)
129
+ -- >>> ok (Proxy :: Proxy ( IsIn ("hello" :> Get '[JSON] Int) SampleAPI) )
135
130
-- OK
136
131
--
137
132
-- Unlike 'IsElem', this requires an *exact* match.
138
133
--
139
- -- >>> ok @( IsIn (Get '[JSON] Int) (Header "h" Bool :> Get '[JSON] Int))
134
+ -- >>> ok (Proxy :: Proxy ( IsIn (Get '[JSON] Int) (Header "h" Bool :> Get '[JSON] Int) ))
140
135
-- ...
141
- -- ... Could not deduce: ...
136
+ -- ... Could not deduce...
142
137
-- ...
143
138
type family IsIn (endpoint :: * ) (api :: * ) :: Constraint where
144
139
IsIn e (sa :<|> sb ) = Or (IsIn e sa ) (IsIn e sb )
@@ -153,7 +148,7 @@ type family IsStrictSubAPI sub api :: Constraint where
153
148
154
149
-- | Check that every element of @xs@ is an endpoint of @api@ (using @'IsIn'@).
155
150
--
156
- -- OK @( AllIsIn (Endpoints SampleAPI) SampleAPI)
151
+ -- ok (Proxy :: Proxy ( AllIsIn (Endpoints SampleAPI) SampleAPI) )
157
152
-- OK
158
153
type family AllIsIn xs api :: Constraint where
159
154
AllIsIn '[] api = ()
@@ -179,12 +174,12 @@ type family IsSubList a b :: Constraint where
179
174
180
175
-- | Check that a value is an element of a list:
181
176
--
182
- -- >>> ok @( Elem Bool '[Int, Bool])
177
+ -- >>> ok (Proxy :: Proxy ( Elem Bool '[Int, Bool]) )
183
178
-- OK
184
179
--
185
- -- >>> ok @( Elem String '[Int, Bool])
180
+ -- >>> ok (Proxy :: Proxy ( Elem String '[Int, Bool]) )
186
181
-- ...
187
- -- ... [Char] expected in list '[Int, Bool]
182
+ -- ... [Char]... '[Int, Bool...
188
183
-- ...
189
184
type Elem e es = ElemGo e es es
190
185
@@ -228,12 +223,13 @@ families are not evaluated (see https://ghc.haskell.org/trac/ghc/ticket/12048).
228
223
229
224
230
225
-- $setup
231
- -- >>> :set -XTypeApplications
232
226
-- >>> :set -XPolyKinds
227
+ -- >>> :set -XGADTs
233
228
-- >>> import Data.Proxy
229
+ -- >>> import Data.Type.Equality
234
230
-- >>> import Servant.API
235
- -- >>> data OK ctx = OK deriving (Show)
236
- -- >>> let ok :: ctx => OK ctx; ok = OK
237
- -- >>> let showType :: Proxy a ; showType = Proxy
231
+ -- >>> data OK ctx where OK :: ctx => OK ctx
232
+ -- >>> instance Show (OK ctx) where show _ = "OK"
233
+ -- >>> let ok :: ctx => Proxy ctx -> OK ctx; ok _ = OK
238
234
-- >>> type SampleAPI = "hello" :> Get '[JSON] Int :<|> "bye" :> Capture "name" String :> Post '[JSON, PlainText] Bool
239
235
-- >>> let sampleAPI = Proxy :: Proxy SampleAPI
0 commit comments