@@ -0,0 +1,264 @@
2+{-# LANGUAGE ConstraintKinds #-}
3+{-# LANGUAGE DataKinds #-}
4+{-# LANGUAGE KindSignatures #-}
5+{-# LANGUAGE MultiParamTypeClasses #-}
6+{-# LANGUAGE PolyKinds #-}
7+{-# LANGUAGE TypeFamilies #-}
8+{-# LANGUAGE TypeOperators #-}
9+{-# LANGUAGE UndecidableInstances #-}
12+This module collects utilities for manipulating @servant@ API types. The
13+functionality in this module is for advanced usage.
15+The code samples in this module use the following type synonym:
17+> type SampleAPI = "hello" :> Get '[JSON] Int
18+> :<|> "bye" :> Capture "name" String :> Post '[JSON, PlainText] Bool
21+module Servant.API.TypeLevel (
30+ -- ** Strict inclusion
44+ -- * Custom type errors
45+ -- | Before @base-4.9.0.0@ we use non-exported 'ElemNotFoundIn' class,
46+ -- which cannot be instantiated.
50+import GHC.Exts (Constraint)
51+import Servant.API.Alternative (type (:<|>))
52+import Servant.API.Capture (Capture, CaptureAll)
53+import Servant.API.Header (Header)
54+import Servant.API.QueryParam (QueryFlag, QueryParam, QueryParams)
55+import Servant.API.ReqBody (ReqBody)
56+import Servant.API.Sub (type (:>))
57+import Servant.API.Verbs (Verb)
58+#if MIN_VERSION_base(4,9,0)
59+import GHC.TypeLits (TypeError, ErrorMessage(..))
66+-- | Flatten API into a list of endpoints.
68+-- >>> Refl :: Endpoints SampleAPI :~: '["hello" :> Verb 'GET 200 '[JSON] Int, "bye" :> (Capture "name" String :> Verb 'POST 200 '[JSON, PlainText] Bool)]
70+type family Endpoints api where
71+ Endpoints (a :<|> b) = AppendList (Endpoints a) (Endpoints b)
72+ Endpoints (e :> a) = MapSub e (Endpoints a)
77+-- | You may use this type family to tell the type checker that your custom
78+-- type may be skipped as part of a link. This is useful for things like
79+-- @'QueryParam'@ that are optional in a URI and do not affect them if they are
82+-- >>> data CustomThing
83+-- >>> type instance IsElem' e (CustomThing :> s) = IsElem e s
85+-- Note that @'IsElem'@ is called, which will mutually recurse back to @'IsElem''@
86+-- if it exhausts all other options again.
88+-- Once you have written a @HasLink@ instance for @CustomThing@ you are ready to go.
89+type family IsElem' a s :: Constraint
91+-- | Closed type family, check if @endpoint@ is within @api@.
92+-- Uses @'IsElem''@ if it exhausts all other options.
94+-- >>> ok (Proxy :: Proxy (IsElem ("hello" :> Get '[JSON] Int) SampleAPI))
97+-- >>> ok (Proxy :: Proxy (IsElem ("bye" :> Get '[JSON] Int) SampleAPI))
99+-- ... Could not deduce...
102+-- An endpoint is considered within an api even if it is missing combinators
103+-- that don't affect the URL:
105+-- >>> ok (Proxy :: Proxy (IsElem (Get '[JSON] Int) (Header "h" Bool :> Get '[JSON] Int)))
108+-- >>> ok (Proxy :: Proxy (IsElem (Get '[JSON] Int) (ReqBody '[JSON] Bool :> Get '[JSON] Int)))
111+-- *N.B.:* @IsElem a b@ can be seen as capturing the notion of whether the URL
112+-- represented by @a@ would match the URL represented by @b@, *not* whether a
113+-- request represented by @a@ matches the endpoints serving @b@ (for the
114+-- latter, use 'IsIn').
115+type family IsElem endpoint api :: Constraint where
116+ IsElem e (sa :<|> sb) = Or (IsElem e sa) (IsElem e sb)
117+ IsElem (e :> sa) (e :> sb) = IsElem sa sb
118+ IsElem sa (Header sym x :> sb) = IsElem sa sb
119+ IsElem sa (ReqBody y x :> sb) = IsElem sa sb
120+ IsElem (CaptureAll z y :> sa) (CaptureAll x y :> sb)
122+ IsElem (Capture z y :> sa) (Capture x y :> sb)
124+ IsElem sa (QueryParam x y :> sb) = IsElem sa sb
125+ IsElem sa (QueryParams x y :> sb) = IsElem sa sb
126+ IsElem sa (QueryFlag x :> sb) = IsElem sa sb
127+ IsElem (Verb m s ct typ) (Verb m s ct' typ)
130+ IsElem e a = IsElem' e a
132+-- | Check whether @sub@ is a sub-API of @api@.
134+-- >>> ok (Proxy :: Proxy (IsSubAPI SampleAPI (SampleAPI :<|> Get '[JSON] Int)))
137+-- >>> ok (Proxy :: Proxy (IsSubAPI (SampleAPI :<|> Get '[JSON] Int) SampleAPI))
139+-- ... Could not deduce...
142+-- This uses @IsElem@ for checking; thus the note there applies here.
143+type family IsSubAPI sub api :: Constraint where
144+ IsSubAPI sub api = AllIsElem (Endpoints sub) api
146+-- | Check that every element of @xs@ is an endpoint of @api@ (using @'IsElem'@).
147+type family AllIsElem xs api :: Constraint where
148+ AllIsElem '[] api = ()
149+ AllIsElem (x ': xs) api = (IsElem x api, AllIsElem xs api)
151+-- ** Strict inclusion
153+-- | Closed type family, check if @endpoint@ is exactly within @api@.
155+-- >>> ok (Proxy :: Proxy (IsIn ("hello" :> Get '[JSON] Int) SampleAPI))
158+-- Unlike 'IsElem', this requires an *exact* match.
160+-- >>> ok (Proxy :: Proxy (IsIn (Get '[JSON] Int) (Header "h" Bool :> Get '[JSON] Int)))
162+-- ... Could not deduce...
164+type family IsIn (endpoint :: *) (api :: *) :: Constraint where
165+ IsIn e (sa :<|> sb) = Or (IsIn e sa) (IsIn e sb)
166+ IsIn (e :> sa) (e :> sb) = IsIn sa sb
169+-- | Check whether @sub@ is a sub API of @api@.
171+-- Like 'IsSubAPI', but uses 'IsIn' rather than 'IsElem'.
172+type family IsStrictSubAPI sub api :: Constraint where
173+ IsStrictSubAPI sub api = AllIsIn (Endpoints sub) api
175+-- | Check that every element of @xs@ is an endpoint of @api@ (using @'IsIn'@).
177+-- ok (Proxy :: Proxy (AllIsIn (Endpoints SampleAPI) SampleAPI))
179+type family AllIsIn xs api :: Constraint where
180+ AllIsIn '[] api = ()
181+ AllIsIn (x ': xs) api = (IsIn x api, AllIsIn xs api)
187+-- | Apply @(e :>)@ to every API in @xs@.
188+type family MapSub e xs where
190+ MapSub e (x ': xs) = (e :> x) ': MapSub e xs
192+-- | Append two type-level lists.
193+type family AppendList xs ys where
194+ AppendList '[] ys = ys
195+ AppendList (x ': xs) ys = x ': AppendList xs ys
197+type family IsSubList a b :: Constraint where
198+ IsSubList '[] b = ()
199+ IsSubList (x ': xs) y = Elem x y `And` IsSubList xs y
201+-- | Check that a value is an element of a list:
203+-- >>> ok (Proxy :: Proxy (Elem Bool '[Int, Bool]))
206+-- >>> ok (Proxy :: Proxy (Elem String '[Int, Bool]))
208+-- ... [Char]...'[Int, Bool...
210+type Elem e es = ElemGo e es es
212+-- 'orig' is used to store original list for better error messages
213+type family ElemGo e es orig :: Constraint where
214+ ElemGo x (x ': xs) orig = ()
215+ ElemGo y (x ': xs) orig = ElemGo y xs orig
216+#if MIN_VERSION_base(4,9,0)
217+ -- Note [Custom Errors]
218+ ElemGo x '[] orig = TypeError ('ShowType x
219+ ':<>: 'Text " expected in list "
220+ ':<>: 'ShowType orig)
222+ ElemGo x '[] orig = ElemNotFoundIn x orig
227+-- | If either a or b produce an empty constraint, produce an empty constraint.
228+type family Or (a :: Constraint) (b :: Constraint) :: Constraint where
229+ -- This works because of:
230+ -- https://ghc.haskell.org/trac/ghc/wiki/NewAxioms/CoincidentOverlap
234+-- | If both a or b produce an empty constraint, produce an empty constraint.
235+type family And (a :: Constraint) (b :: Constraint) :: Constraint where
238+-- * Custom type errors
240+#if !MIN_VERSION_base(4,9,0)
241+class ElemNotFoundIn val list
244+{- Note [Custom Errors]
245+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
246+We might try to factor these our more cleanly, but the type synonyms and type
247+families are not evaluated (see https://ghc.haskell.org/trac/ghc/ticket/12048).
253+-- The doctests in this module are run with following preamble:
255+-- >>> :set -XPolyKinds
257+-- >>> import Data.Proxy
258+-- >>> import Data.Type.Equality
259+-- >>> import Servant.API
260+-- >>> data OK ctx where OK :: ctx => OK ctx
261+-- >>> instance Show (OK ctx) where show _ = "OK"
262+-- >>> let ok :: ctx => Proxy ctx -> OK ctx; ok _ = OK
263+-- >>> type SampleAPI = "hello" :> Get '[JSON] Int :<|> "bye" :> Capture "name" String :> Post '[JSON, PlainText] Bool
264+-- >>> let sampleAPI = Proxy :: Proxy SampleAPI