@@ -39,13 +39,8 @@ import GHC.TypeLits (TypeError, ErrorMessage(..))
3939
4040-- | Flatten API into a list of endpoints.
4141--
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
4944type family Endpoints api where
5045 Endpoints (a :<|> b) = AppendList (Endpoints a) (Endpoints b)
5146 Endpoints (e :> a) = MapSub e (Endpoints a)
@@ -70,21 +65,21 @@ type family IsElem' a s :: Constraint
7065-- | Closed type family, check if @endpoint@ is within @api@.
7166-- Uses @'IsElem''@ if it exhausts all other options.
7267--
73−-- >>> ok @(IsElem ("hello" :> Get '[JSON] Int) SampleAPI)
68+-- >>> ok (Proxy :: Proxy (IsElem ("hello" :> Get '[JSON] Int) SampleAPI))
7469-- OK
7570--
76−-- >>> ok @(IsElem ("bye" :> Get '[JSON] Int) SampleAPI)
71+-- >>> ok (Proxy :: Proxy (IsElem ("bye" :> Get '[JSON] Int) SampleAPI))
7772-- ...
78−-- ... Could not deduce: ...
73+-- ... Could not deduce...
7974-- ...
8075--
8176-- An endpoint is considered within an api even if it is missing combinators
8277-- that don't affect the URL:
8378--
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)))
8580-- OK
8681--
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)))
8883-- OK
8984--
9085-- *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
110105
111106-- | Check whether @sub@ is a sub-API of @api@.
112107--
113−-- >>> ok @(IsSubAPI SampleAPI (SampleAPI :<|> Get '[JSON] Int))
108+-- >>> ok (Proxy :: Proxy (IsSubAPI SampleAPI (SampleAPI :<|> Get '[JSON] Int)))
114109-- OK
115110--
116−-- >>> ok @(IsSubAPI (SampleAPI :<|> Get '[JSON] Int) SampleAPI)
111+-- >>> ok (Proxy :: Proxy (IsSubAPI (SampleAPI :<|> Get '[JSON] Int) SampleAPI))
117112-- ...
118−-- ... Could not deduce: ...
113+-- ... Could not deduce...
119114-- ...
120115--
121116-- This uses @IsElem@ for checking; thus the note there applies here.
@@ -131,14 +126,14 @@ type family AllIsElem xs api :: Constraint where
131126
132127-- | Closed type family, check if @endpoint@ is exactly within @api@.
133128--
134−-- >>> ok @(IsIn ("hello" :> Get '[JSON] Int) SampleAPI)
129+-- >>> ok (Proxy :: Proxy (IsIn ("hello" :> Get '[JSON] Int) SampleAPI))
135130-- OK
136131--
137132-- Unlike 'IsElem', this requires an *exact* match.
138133--
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)))
140135-- ...
141−-- ... Could not deduce: ...
136+-- ... Could not deduce...
142137-- ...
143138type family IsIn (endpoint :: *) (api :: *) :: Constraint where
144139 IsIn e (sa :<|> sb) = Or (IsIn e sa) (IsIn e sb)
@@ -153,7 +148,7 @@ type family IsStrictSubAPI sub api :: Constraint where
153148
154149-- | Check that every element of @xs@ is an endpoint of @api@ (using @'IsIn'@).
155150--
156−-- OK @(AllIsIn (Endpoints SampleAPI) SampleAPI)
151+-- ok (Proxy :: Proxy (AllIsIn (Endpoints SampleAPI) SampleAPI))
157152-- OK
158153type family AllIsIn xs api :: Constraint where
159154 AllIsIn '[] api = ()
@@ -179,12 +174,12 @@ type family IsSubList a b :: Constraint where
179174
180175-- | Check that a value is an element of a list:
181176--
182−-- >>> ok @(Elem Bool '[Int, Bool])
177+-- >>> ok (Proxy :: Proxy (Elem Bool '[Int, Bool]))
183178-- OK
184179--
185−-- >>> ok @(Elem String '[Int, Bool])
180+-- >>> ok (Proxy :: Proxy (Elem String '[Int, Bool]))
186181-- ...
187−-- ... [Char] expected in list '[Int, Bool]
182+-- ... [Char]...'[Int, Bool...
188183-- ...
189184type Elem e es = ElemGo e es es
190185
@@ -228,12 +223,13 @@ families are not evaluated (see https://ghc.haskell.org/trac/ghc/ticket/12048).
228223
229224
230225-- $setup
231−-- >>> :set -XTypeApplications
232226-- >>> :set -XPolyKinds
227+-- >>> :set -XGADTs
233228-- >>> import Data.Proxy
229+-- >>> import Data.Type.Equality
234230-- >>> 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
238234-- >>> type SampleAPI = "hello" :> Get '[JSON] Int :<|> "bye" :> Capture "name" String :> Post '[JSON, PlainText] Bool
239235-- >>> let sampleAPI = Proxy :: Proxy SampleAPI