@@ -39,13 +39,8 @@ import GHC.TypeLits (TypeError, ErrorMessage(..))
40-- | Flatten API into a list of endpoints.
40-- | Flatten API into a list of endpoints.
42−-- >>> :t showType @(Endpoints SampleAPI)
45−-- ... '["hello" :> Verb 'GET 200 '[JSON] Int,
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)]
49type family Endpoints api where
44type family Endpoints api where
50 Endpoints (a :<|> b) = AppendList (Endpoints a) (Endpoints b)
45 Endpoints (a :<|> b) = AppendList (Endpoints a) (Endpoints b)
51 Endpoints (e :> a) = MapSub e (Endpoints a)
46 Endpoints (e :> a) = MapSub e (Endpoints a)
@@ -70,21 +65,21 @@ type family IsElem' a s :: Constraint
70-- | Closed type family, check if @endpoint@ is within @api@.
65-- | Closed type family, check if @endpoint@ is within @api@.
71-- Uses @'IsElem''@ if it exhausts all other options.
66-- Uses @'IsElem''@ if it exhausts all other options.
73−-- >>> ok @(IsElem ("hello" :> Get '[JSON] Int) SampleAPI)
68+-- >>> ok (Proxy :: Proxy (IsElem ("hello" :> Get '[JSON] Int) SampleAPI))
76−-- >>> ok @(IsElem ("bye" :> Get '[JSON] Int) SampleAPI)
71+-- >>> ok (Proxy :: Proxy (IsElem ("bye" :> Get '[JSON] Int) SampleAPI))
78−-- ... Could not deduce: ...
73+-- ... Could not deduce...
81-- An endpoint is considered within an api even if it is missing combinators
76-- An endpoint is considered within an api even if it is missing combinators
82-- that don't affect the URL:
77-- that don't affect the URL:
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)))
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)))
90-- *N.B.:* @IsElem a b@ can be seen as capturing the notion of whether the URL
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
111-- | Check whether @sub@ is a sub-API of @api@.
106-- | Check whether @sub@ is a sub-API of @api@.
113−-- >>> ok @(IsSubAPI SampleAPI (SampleAPI :<|> Get '[JSON] Int))
108+-- >>> ok (Proxy :: Proxy (IsSubAPI SampleAPI (SampleAPI :<|> Get '[JSON] Int)))
116−-- >>> ok @(IsSubAPI (SampleAPI :<|> Get '[JSON] Int) SampleAPI)
111+-- >>> ok (Proxy :: Proxy (IsSubAPI (SampleAPI :<|> Get '[JSON] Int) SampleAPI))
118−-- ... Could not deduce: ...
113+-- ... Could not deduce...
121-- This uses @IsElem@ for checking; thus the note there applies here.
116-- This uses @IsElem@ for checking; thus the note there applies here.
@@ -131,14 +126,14 @@ type family AllIsElem xs api :: Constraint where
132-- | Closed type family, check if @endpoint@ is exactly within @api@.
127-- | Closed type family, check if @endpoint@ is exactly within @api@.
134−-- >>> ok @(IsIn ("hello" :> Get '[JSON] Int) SampleAPI)
129+-- >>> ok (Proxy :: Proxy (IsIn ("hello" :> Get '[JSON] Int) SampleAPI))
137-- Unlike 'IsElem', this requires an *exact* match.
132-- Unlike 'IsElem', this requires an *exact* match.
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)))
141−-- ... Could not deduce: ...
136+-- ... Could not deduce...
143type family IsIn (endpoint :: *) (api :: *) :: Constraint where
138type family IsIn (endpoint :: *) (api :: *) :: Constraint where
144 IsIn e (sa :<|> sb) = Or (IsIn e sa) (IsIn e sb)
139 IsIn e (sa :<|> sb) = Or (IsIn e sa) (IsIn e sb)
@@ -153,7 +148,7 @@ type family IsStrictSubAPI sub api :: Constraint where
154-- | Check that every element of @xs@ is an endpoint of @api@ (using @'IsIn'@).
149-- | Check that every element of @xs@ is an endpoint of @api@ (using @'IsIn'@).
156−-- OK @(AllIsIn (Endpoints SampleAPI) SampleAPI)
151+-- ok (Proxy :: Proxy (AllIsIn (Endpoints SampleAPI) SampleAPI))
158type family AllIsIn xs api :: Constraint where
153type family AllIsIn xs api :: Constraint where
159 AllIsIn '[] api = ()
154 AllIsIn '[] api = ()
@@ -179,12 +174,12 @@ type family IsSubList a b :: Constraint where
180-- | Check that a value is an element of a list:
175-- | Check that a value is an element of a list:
182−-- >>> ok @(Elem Bool '[Int, Bool])
177+-- >>> ok (Proxy :: Proxy (Elem Bool '[Int, Bool]))
185−-- >>> ok @(Elem String '[Int, Bool])
180+-- >>> ok (Proxy :: Proxy (Elem String '[Int, Bool]))
187−-- ... [Char] expected in list '[Int, Bool]
182+-- ... [Char]...'[Int, Bool...
189type Elem e es = ElemGo e es es
184type Elem e es = ElemGo e es es
@@ -228,12 +223,13 @@ families are not evaluated (see https://ghc.haskell.org/trac/ghc/ticket/12048).
231−-- >>> :set -XTypeApplications
232-- >>> :set -XPolyKinds
226-- >>> :set -XPolyKinds
233-- >>> import Data.Proxy
228-- >>> import Data.Proxy
229+-- >>> import Data.Type.Equality
234-- >>> import Servant.API
230-- >>> import Servant.API
235−-- >>> data OK ctx = OK deriving (Show)
231+-- >>> data OK ctx where OK :: ctx => OK ctx
232+-- >>> instance Show (OK ctx) where show _ = "OK"
236−-- >>> let ok :: ctx => OK ctx; ok = OK
233+-- >>> let ok :: ctx => Proxy ctx -> OK ctx; ok _ = OK
237−-- >>> let showType :: Proxy a ; showType = Proxy
238-- >>> type SampleAPI = "hello" :> Get '[JSON] Int :<|> "bye" :> Capture "name" String :> Post '[JSON, PlainText] Bool
234-- >>> type SampleAPI = "hello" :> Get '[JSON] Int :<|> "bye" :> Capture "name" String :> Post '[JSON, PlainText] Bool
239-- >>> let sampleAPI = Proxy :: Proxy SampleAPI
235-- >>> let sampleAPI = Proxy :: Proxy SampleAPI