{-# LANGUAGE CPP #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-| This module collects utilities for manipulating @servant@ API types. The functionality in this module is for advanced usage. The code samples in this module use the following type synonym: > type SampleAPI = "hello" :> Get '[JSON] Int > :<|> "bye" :> Capture "name" String :> Post '[JSON, PlainText] Bool -} module Servant.API.TypeLevel ( -- $setup -- * API predicates Endpoints, -- ** Lax inclusion IsElem', IsElem, IsSubAPI, AllIsElem, -- ** Strict inclusion IsIn, IsStrictSubAPI, AllIsIn, -- * Helpers -- ** Lists MapSub, AppendList, IsSubList, Elem, ElemGo, -- ** Logic Or, And, -- * Custom type errors -- | Before @base-4.9.0.0@ we use non-exported 'ElemNotFoundIn' class, -- which cannot be instantiated. ) where import GHC.Exts (Constraint) import Servant.API.Alternative (type (:<|>)) import Servant.API.Capture (Capture, CaptureAll) import Servant.API.Header (Header) import Servant.API.QueryParam (QueryFlag, QueryParam, QueryParams) import Servant.API.ReqBody (ReqBody) import Servant.API.Sub (type (:>)) import Servant.API.Verbs (Verb) #if MIN_VERSION_base(4,9,0) import GHC.TypeLits (TypeError, ErrorMessage(..)) #endif -- * API predicates -- | Flatten API into a list of endpoints. -- -- >>> Refl :: Endpoints SampleAPI :~: '["hello" :> Verb 'GET 200 '[JSON] Int, "bye" :> (Capture "name" String :> Verb 'POST 200 '[JSON, PlainText] Bool)] -- Refl type family Endpoints api where Endpoints (a :<|> b) = AppendList (Endpoints a) (Endpoints b) Endpoints (e :> a) = MapSub e (Endpoints a) Endpoints a = '[a] -- ** Lax inclusion -- | You may use this type family to tell the type checker that your custom -- type may be skipped as part of a link. This is useful for things like -- @'QueryParam'@ that are optional in a URI and do not affect them if they are -- omitted. -- -- >>> data CustomThing -- >>> type instance IsElem' e (CustomThing :> s) = IsElem e s -- -- Note that @'IsElem'@ is called, which will mutually recurse back to @'IsElem''@ -- if it exhausts all other options again. -- -- Once you have written a @HasLink@ instance for @CustomThing@ you are ready to go. type family IsElem' a s :: Constraint -- | Closed type family, check if @endpoint@ is within @api@. -- Uses @'IsElem''@ if it exhausts all other options. -- -- >>> ok (Proxy :: Proxy (IsElem ("hello" :> Get '[JSON] Int) SampleAPI)) -- OK -- -- >>> ok (Proxy :: Proxy (IsElem ("bye" :> Get '[JSON] Int) SampleAPI)) -- ... -- ... Could not deduce... -- ... -- -- An endpoint is considered within an api even if it is missing combinators -- that don't affect the URL: -- -- >>> ok (Proxy :: Proxy (IsElem (Get '[JSON] Int) (Header "h" Bool :> Get '[JSON] Int))) -- OK -- -- >>> ok (Proxy :: Proxy (IsElem (Get '[JSON] Int) (ReqBody '[JSON] Bool :> Get '[JSON] Int))) -- OK -- -- *N.B.:* @IsElem a b@ can be seen as capturing the notion of whether the URL -- represented by @a@ would match the URL represented by @b@, *not* whether a -- request represented by @a@ matches the endpoints serving @b@ (for the -- latter, use 'IsIn'). type family IsElem endpoint api :: Constraint where IsElem e (sa :<|> sb) = Or (IsElem e sa) (IsElem e sb) IsElem (e :> sa) (e :> sb) = IsElem sa sb IsElem sa (Header sym x :> sb) = IsElem sa sb IsElem sa (ReqBody y x :> sb) = IsElem sa sb IsElem (CaptureAll z y :> sa) (CaptureAll x y :> sb) = IsElem sa sb IsElem (Capture z y :> sa) (Capture x y :> sb) = IsElem sa sb IsElem sa (QueryParam x y :> sb) = IsElem sa sb IsElem sa (QueryParams x y :> sb) = IsElem sa sb IsElem sa (QueryFlag x :> sb) = IsElem sa sb IsElem (Verb m s ct typ) (Verb m s ct' typ) = IsSubList ct ct' IsElem e e = () IsElem e a = IsElem' e a -- | Check whether @sub@ is a sub-API of @api@. -- -- >>> ok (Proxy :: Proxy (IsSubAPI SampleAPI (SampleAPI :<|> Get '[JSON] Int))) -- OK -- -- >>> ok (Proxy :: Proxy (IsSubAPI (SampleAPI :<|> Get '[JSON] Int) SampleAPI)) -- ... -- ... Could not deduce... -- ... -- -- This uses @IsElem@ for checking; thus the note there applies here. type family IsSubAPI sub api :: Constraint where IsSubAPI sub api = AllIsElem (Endpoints sub) api -- | Check that every element of @xs@ is an endpoint of @api@ (using @'IsElem'@). type family AllIsElem xs api :: Constraint where AllIsElem '[] api = () AllIsElem (x ': xs) api = (IsElem x api, AllIsElem xs api) -- ** Strict inclusion -- | Closed type family, check if @endpoint@ is exactly within @api@. -- -- >>> ok (Proxy :: Proxy (IsIn ("hello" :> Get '[JSON] Int) SampleAPI)) -- OK -- -- Unlike 'IsElem', this requires an *exact* match. -- -- >>> ok (Proxy :: Proxy (IsIn (Get '[JSON] Int) (Header "h" Bool :> Get '[JSON] Int))) -- ... -- ... Could not deduce... -- ... type family IsIn (endpoint :: *) (api :: *) :: Constraint where IsIn e (sa :<|> sb) = Or (IsIn e sa) (IsIn e sb) IsIn (e :> sa) (e :> sb) = IsIn sa sb IsIn e e = () -- | Check whether @sub@ is a sub API of @api@. -- -- Like 'IsSubAPI', but uses 'IsIn' rather than 'IsElem'. type family IsStrictSubAPI sub api :: Constraint where IsStrictSubAPI sub api = AllIsIn (Endpoints sub) api -- | Check that every element of @xs@ is an endpoint of @api@ (using @'IsIn'@). -- -- ok (Proxy :: Proxy (AllIsIn (Endpoints SampleAPI) SampleAPI)) -- OK type family AllIsIn xs api :: Constraint where AllIsIn '[] api = () AllIsIn (x ': xs) api = (IsIn x api, AllIsIn xs api) -- * Helpers -- ** Lists -- | Apply @(e :>)@ to every API in @xs@. type family MapSub e xs where MapSub e '[] = '[] MapSub e (x ': xs) = (e :> x) ': MapSub e xs -- | Append two type-level lists. type family AppendList xs ys where AppendList '[] ys = ys AppendList (x ': xs) ys = x ': AppendList xs ys type family IsSubList a b :: Constraint where IsSubList '[] b = () IsSubList (x ': xs) y = Elem x y `And` IsSubList xs y -- | Check that a value is an element of a list: -- -- >>> ok (Proxy :: Proxy (Elem Bool '[Int, Bool])) -- OK -- -- >>> ok (Proxy :: Proxy (Elem String '[Int, Bool])) -- ... -- ... [Char]...'[Int, Bool... -- ... type Elem e es = ElemGo e es es -- 'orig' is used to store original list for better error messages type family ElemGo e es orig :: Constraint where ElemGo x (x ': xs) orig = () ElemGo y (x ': xs) orig = ElemGo y xs orig #if MIN_VERSION_base(4,9,0) -- Note [Custom Errors] ElemGo x '[] orig = TypeError ('ShowType x ':<>: 'Text " expected in list " ':<>: 'ShowType orig) #else ElemGo x '[] orig = ElemNotFoundIn x orig #endif -- ** Logic -- | If either a or b produce an empty constraint, produce an empty constraint. type family Or (a :: Constraint) (b :: Constraint) :: Constraint where -- This works because of: -- https://ghc.haskell.org/trac/ghc/wiki/NewAxioms/CoincidentOverlap Or () b = () Or a () = () -- | If both a or b produce an empty constraint, produce an empty constraint. type family And (a :: Constraint) (b :: Constraint) :: Constraint where And () () = () -- * Custom type errors #if !MIN_VERSION_base(4,9,0) class ElemNotFoundIn val list #endif {- Note [Custom Errors] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We might try to factor these our more cleanly, but the type synonyms and type families are not evaluated (see https://ghc.haskell.org/trac/ghc/ticket/12048). -} -- $setup -- -- The doctests in this module are run with following preamble: -- -- >>> :set -XPolyKinds -- >>> :set -XGADTs -- >>> import Data.Proxy -- >>> import Data.Type.Equality -- >>> import Servant.API -- >>> data OK ctx where OK :: ctx => OK ctx -- >>> instance Show (OK ctx) where show _ = "OK" -- >>> let ok :: ctx => Proxy ctx -> OK ctx; ok _ = OK -- >>> type SampleAPI = "hello" :> Get '[JSON] Int :<|> "bye" :> Capture "name" String :> Post '[JSON, PlainText] Bool -- >>> let sampleAPI = Proxy :: Proxy SampleAPI