From 09c8464a5a5c6ce99f4b5a2f7f80de8fb6927e95 Mon Sep 17 00:00:00 2001
From: Nickolay Kudasov <nickolay.kudasov@gmail.com>
Date: Wed, 20 Jan 2016 17:39:18 +0300
Subject: [PATCH 01/12] Move type-level operations from Utils.Links to
 API.TypeLevel

---
 servant/servant.cabal                   |  1 +
 servant/src/Servant/API/TypeLevel.hs    | 78 +++++++++++++++++++++++++
 servant/src/Servant/Utils/Links.hs      | 62 +-------------------
 servant/test/Servant/Utils/LinksSpec.hs |  1 +
 4 files changed, 83 insertions(+), 59 deletions(-)
 create mode 100644 servant/src/Servant/API/TypeLevel.hs

diff --git a/servant/servant.cabal b/servant/servant.cabal
index 79d08e39..ffb627e0 100644
--- a/servant/servant.cabal
+++ b/servant/servant.cabal
@@ -47,6 +47,7 @@ library
     Servant.API.ReqBody
     Servant.API.ResponseHeaders
     Servant.API.Sub
+    Servant.API.TypeLevel
     Servant.API.Vault
     Servant.API.Verbs
     Servant.API.WithNamedContext
diff --git a/servant/src/Servant/API/TypeLevel.hs b/servant/src/Servant/API/TypeLevel.hs
new file mode 100644
index 00000000..9a78639f
--- /dev/null
+++ b/servant/src/Servant/API/TypeLevel.hs
@@ -0,0 +1,78 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+module Servant.API.TypeLevel where
+
+import GHC.Exts(Constraint)
+import Servant.API.Capture ( Capture )
+import Servant.API.ReqBody ( ReqBody )
+import Servant.API.QueryParam ( QueryParam, QueryParams, QueryFlag )
+import Servant.API.Header ( Header )
+import Servant.API.Verbs ( Verb )
+import Servant.API.Sub ( type (:>) )
+import Servant.API.Alternative ( type (:<|>) )
+
+-- * API predicates
+
+-- | 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''@.
+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
+
+-- * Helpers
+
+-- ** Lists
+
+type family IsSubList a b :: Constraint where
+    IsSubList '[] b          = ()
+    IsSubList (x ': xs) y    = Elem x y `And` IsSubList xs y
+
+type family Elem e es :: Constraint where
+    Elem x (x ': xs) = ()
+    Elem y (x ': xs) = Elem y xs
+
+-- ** 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 () ()     = ()
+
diff --git a/servant/src/Servant/Utils/Links.hs b/servant/src/Servant/Utils/Links.hs
index c4cfea26..618bb2aa 100644
--- a/servant/src/Servant/Utils/Links.hs
+++ b/servant/src/Servant/Utils/Links.hs
@@ -6,7 +6,6 @@
 {-# LANGUAGE ScopedTypeVariables    #-}
 {-# LANGUAGE TypeFamilies           #-}
 {-# LANGUAGE TypeOperators          #-}
-{-# LANGUAGE UndecidableInstances   #-}
 {-# OPTIONS_HADDOCK not-home        #-}
 
 -- | Type safe generation of internal links.
@@ -79,6 +78,8 @@
 --  bad_link under api after trying the open (but empty) type family
 --  `IsElem'` as a last resort.
 module Servant.Utils.Links (
+  module Servant.API.TypeLevel,
+
   -- * Building and using safe links
   --
   -- | Note that 'URI' is Network.URI.URI from the network-uri package.
@@ -88,10 +89,6 @@ module Servant.Utils.Links (
   , HasLink(..)
   , linkURI
   , Link
-  , IsElem'
-  -- * Illustrative exports
-  , IsElem
-  , Or
 ) where
 
 import           Data.List
@@ -99,7 +96,6 @@ import           Data.Monoid.Compat    ( (<>) )
 import           Data.Proxy            ( Proxy(..) )
 import qualified Data.Text             as Text
 import qualified Data.Text.Encoding    as TE
-import           GHC.Exts              (Constraint)
 import           GHC.TypeLits          ( KnownSymbol, symbolVal )
 import           Network.URI           ( URI(..), escapeURIString, isUnreserved )
 import           Prelude               ()
@@ -115,7 +111,7 @@ import Servant.API.RemoteHost ( RemoteHost )
 import Servant.API.Verbs ( Verb )
 import Servant.API.Sub ( type (:>) )
 import Servant.API.Raw ( Raw )
-import Servant.API.Alternative ( type (:<|>) )
+import Servant.API.TypeLevel
 
 -- | A safe link datatype.
 -- The only way of constructing a 'Link' is using 'safeLink', which means any
@@ -131,58 +127,6 @@ instance ToHttpApiData Link where
         let uri = linkURI l
         in Text.pack $ uriPath uri ++ uriQuery uri
 
--- | 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 () ()     = ()
-
--- | 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
-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 (Capture z y :> sa) (Capture x y :> sb)
-                                            = IsElem sa sb
-    IsElem (CaptureAll z y :> sa) (CaptureAll 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
-
-type family IsSubList a b :: Constraint where
-    IsSubList '[] b          = ()
-    IsSubList (x ': xs) y    = Elem x y `And` IsSubList xs y
-
-type family Elem e es :: Constraint where
-    Elem x (x ': xs) = ()
-    Elem y (x ': xs) = Elem y xs
-
 -- Phantom types for Param
 data Query
 
diff --git a/servant/test/Servant/Utils/LinksSpec.hs b/servant/test/Servant/Utils/LinksSpec.hs
index 6a6bb8dc..fbc5ce0b 100644
--- a/servant/test/Servant/Utils/LinksSpec.hs
+++ b/servant/test/Servant/Utils/LinksSpec.hs
@@ -10,6 +10,7 @@ import           Test.Hspec              (Expectation, Spec, describe, it,
 import           Data.String             (fromString)
 
 import           Servant.API
+import           Servant.API.TypeLevel
 
 type TestApi =
   -- Capture and query params

From e9b281f3cc972ea61757fa06b3a9e3d16465a628 Mon Sep 17 00:00:00 2001
From: Nickolay Kudasov <nickolay.kudasov@gmail.com>
Date: Wed, 20 Jan 2016 17:53:32 +0300
Subject: [PATCH 02/12] Add IsIn and IsSubAPI constraints

---
 servant/src/Servant/API/TypeLevel.hs | 55 +++++++++++++++++++++++++---
 1 file changed, 50 insertions(+), 5 deletions(-)

diff --git a/servant/src/Servant/API/TypeLevel.hs b/servant/src/Servant/API/TypeLevel.hs
index 9a78639f..f74f9d4f 100644
--- a/servant/src/Servant/API/TypeLevel.hs
+++ b/servant/src/Servant/API/TypeLevel.hs
@@ -17,23 +17,30 @@ import Servant.API.Alternative ( type (:<|>) )
 
 -- * API predicates
 
+-- | Flatten API into a list of endpoints.
+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
+-- @'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'`
+-- 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.
+-- 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''@.
+-- Uses @'IsElem''@ if it exhausts all other options.
 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
@@ -51,10 +58,48 @@ type family IsElem endpoint api :: Constraint where
     IsElem e e                              = ()
     IsElem e a                              = IsElem' e a
 
+-- | Check whether @sub@ is a sub API of @api@.
+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@.
+-- We aren't sure what affects how an endpoint is built up, so we require an
+-- exact match.
+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@.
+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'@).
+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

From a6de4ba1235943c1991d90105e8cdc28e01489d1 Mon Sep 17 00:00:00 2001
From: Nickolay Kudasov <nickolay.kudasov@gmail.com>
Date: Wed, 20 Jan 2016 17:56:52 +0300
Subject: [PATCH 03/12] Remove IsIn from servant-docs

---
 servant-docs/src/Servant/Docs/Internal.hs | 10 +---------
 1 file changed, 1 insertion(+), 9 deletions(-)

diff --git a/servant-docs/src/Servant/Docs/Internal.hs b/servant-docs/src/Servant/Docs/Internal.hs
index 70530455..076ced71 100644
--- a/servant-docs/src/Servant/Docs/Internal.hs
+++ b/servant-docs/src/Servant/Docs/Internal.hs
@@ -42,6 +42,7 @@ import           GHC.Generics
 import           GHC.TypeLits
 import           Servant.API
 import           Servant.API.ContentTypes
+import           Servant.API.TypeLevel
 import           Servant.Utils.Links
 
 import qualified Data.HashMap.Strict        as HM
@@ -306,15 +307,6 @@ docs p = docsWithOptions p defaultDocOptions
 docsWithOptions :: HasDocs api => Proxy api -> DocOptions -> API
 docsWithOptions p = docsFor p (defEndpoint, defAction)
 
--- | Closed type family, check if endpoint is exactly within API.
-
--- We aren't sure what affects how an Endpoint is built up, so we require an
--- exact match.
-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                           = ()
-
 -- | Create an 'ExtraInfo' that is guaranteed to be within the given API layout.
 --
 -- The safety here is to ensure that you only add custom documentation to an

From b836f13dea71714e57ae566ac3f028cd55ccfe8d Mon Sep 17 00:00:00 2001
From: Nickolay Kudasov <nickolay.kudasov@gmail.com>
Date: Wed, 20 Jan 2016 18:23:10 +0300
Subject: [PATCH 04/12] Remove Elem from servant-foreign

---
 servant-foreign/src/Servant/Foreign/Internal.hs | 10 +---------
 servant/src/Servant/API/TypeLevel.hs            |  2 +-
 2 files changed, 2 insertions(+), 10 deletions(-)

diff --git a/servant-foreign/src/Servant/Foreign/Internal.hs b/servant-foreign/src/Servant/Foreign/Internal.hs
index 3eced051..e05583d3 100644
--- a/servant-foreign/src/Servant/Foreign/Internal.hs
+++ b/servant-foreign/src/Servant/Foreign/Internal.hs
@@ -21,6 +21,7 @@ import           GHC.TypeLits
 import qualified Network.HTTP.Types as HTTP
 import           Prelude hiding (concat)
 import           Servant.API
+import           Servant.API.TypeLevel
 
 
 newtype FunctionName = FunctionName { unFunctionName :: [Text] }
@@ -135,15 +136,6 @@ makeLenses ''Req
 defReq :: Req ftype
 defReq = Req defUrl "GET" [] Nothing Nothing (FunctionName [])
 
--- | To be used exclusively as a "negative" return type/constraint
--- by @'Elem`@ type family.
-class NotFound
-
-type family Elem (a :: *) (ls::[*]) :: Constraint where
-  Elem a '[]         = NotFound
-  Elem a (a ': list) = ()
-  Elem a (b ': list) = Elem a list
-
 -- | 'HasForeignType' maps Haskell types with types in the target
 -- language of your backend. For example, let's say you're
 -- implementing a backend to some language __X__, and you want
diff --git a/servant/src/Servant/API/TypeLevel.hs b/servant/src/Servant/API/TypeLevel.hs
index f74f9d4f..9565ee5d 100644
--- a/servant/src/Servant/API/TypeLevel.hs
+++ b/servant/src/Servant/API/TypeLevel.hs
@@ -7,7 +7,7 @@
 module Servant.API.TypeLevel where
 
 import GHC.Exts(Constraint)
-import Servant.API.Capture ( Capture )
+import Servant.API.Capture ( Capture, CaptureAll )
 import Servant.API.ReqBody ( ReqBody )
 import Servant.API.QueryParam ( QueryParam, QueryParams, QueryFlag )
 import Servant.API.Header ( Header )

From e0cd899e06a984ae2cb09b72b38149e31f15c7eb Mon Sep 17 00:00:00 2001
From: "Julian K. Arni" <jkarni@gmail.com>
Date: Mon, 22 Aug 2016 11:27:33 -0300
Subject: [PATCH 05/12] Updated changelog for Servant.API.TypeLevel changes

---
 servant/CHANGELOG.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/servant/CHANGELOG.md b/servant/CHANGELOG.md
index 81c638d3..0232c4f5 100644
--- a/servant/CHANGELOG.md
+++ b/servant/CHANGELOG.md
@@ -24,6 +24,8 @@
 ----
 
 * Add `CaptureAll` combinator. Captures all of the remaining segments in a URL.
+* Add `Servant.API.TypeLevel` module, with frequently used type-level
+functionaliy.
 
 0.8
 ---

From 92b11968306dc0e34090cebc96170103c7d37e16 Mon Sep 17 00:00:00 2001
From: "Julian K. Arni" <jkarni@gmail.com>
Date: Mon, 22 Aug 2016 12:24:36 -0300
Subject: [PATCH 06/12] Redundant import fixes

---
 servant-docs/src/Servant/Docs/Internal.hs     |  2 -
 .../src/Servant/Foreign/Internal.hs           |  1 -
 servant/src/Servant/API/TypeLevel.hs          | 57 ++++++++++++++++++-
 servant/test/Servant/Utils/LinksSpec.hs       |  1 -
 4 files changed, 54 insertions(+), 7 deletions(-)

diff --git a/servant-docs/src/Servant/Docs/Internal.hs b/servant-docs/src/Servant/Docs/Internal.hs
index 076ced71..502c540f 100644
--- a/servant-docs/src/Servant/Docs/Internal.hs
+++ b/servant-docs/src/Servant/Docs/Internal.hs
@@ -37,13 +37,11 @@ import           Data.Ord                   (comparing)
 import           Data.Proxy                 (Proxy(Proxy))
 import           Data.String.Conversions    (cs)
 import           Data.Text                  (Text, unpack)
-import           GHC.Exts                   (Constraint)
 import           GHC.Generics
 import           GHC.TypeLits
 import           Servant.API
 import           Servant.API.ContentTypes
 import           Servant.API.TypeLevel
-import           Servant.Utils.Links
 
 import qualified Data.HashMap.Strict        as HM
 import qualified Data.Text                  as T
diff --git a/servant-foreign/src/Servant/Foreign/Internal.hs b/servant-foreign/src/Servant/Foreign/Internal.hs
index e05583d3..5165a8e5 100644
--- a/servant-foreign/src/Servant/Foreign/Internal.hs
+++ b/servant-foreign/src/Servant/Foreign/Internal.hs
@@ -16,7 +16,6 @@ import           Data.Proxy
 import           Data.String
 import           Data.Text
 import           Data.Text.Encoding (decodeUtf8)
-import           GHC.Exts (Constraint)
 import           GHC.TypeLits
 import qualified Network.HTTP.Types as HTTP
 import           Prelude hiding (concat)
diff --git a/servant/src/Servant/API/TypeLevel.hs b/servant/src/Servant/API/TypeLevel.hs
index 9565ee5d..759d89c0 100644
--- a/servant/src/Servant/API/TypeLevel.hs
+++ b/servant/src/Servant/API/TypeLevel.hs
@@ -1,8 +1,11 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE UndecidableInstances #-}
 module Servant.API.TypeLevel where
 
@@ -14,6 +17,9 @@ import Servant.API.Header ( Header )
 import Servant.API.Verbs ( Verb )
 import Servant.API.Sub ( type (:>) )
 import Servant.API.Alternative ( type (:<|>) )
+#if MIN_VERSION_base(4,9,0)
+import GHC.TypeLits (TypeError, ErrorMessage(..))
+#endif
 
 -- * API predicates
 
@@ -104,9 +110,24 @@ type family IsSubList a b :: Constraint where
     IsSubList '[] b          = ()
     IsSubList (x ': xs) y    = Elem x y `And` IsSubList xs y
 
-type family Elem e es :: Constraint where
-    Elem x (x ': xs) = ()
-    Elem y (x ': xs) = Elem y xs
+-- | Check that an eleme is an element of a list:
+--
+-- >>> ok (Proxy :: Proxy (Elem Bool '[Int, Bool]))
+-- OK
+--
+-- >>> ok (Proxy  :: Proxy (Elem String '[Int, Bool]))
+-- ...
+--     No instance for (ElemNotFoundIn [Char] '[Int, Bool])
+--       arising from a use of ‘ok’
+-- ...
+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
+    ElemGo x '[] orig       = ElemNotFoundIn x orig
+
 
 -- ** Logic
 
@@ -121,3 +142,33 @@ type family Or (a :: Constraint) (b :: Constraint) :: Constraint where
 type family And (a :: Constraint) (b :: Constraint) :: Constraint where
     And () ()     = ()
 
+-- * Custom type errors
+
+#if MIN_VERSION_base(4,9,0)
+-- GHC >= 8
+
+
+type ElemNotFoundIn val list = TypeError
+  (ShowType val :<>: Text " expected in list " :<>: ShowList list)
+
+
+-- Utilities
+
+type family ShowListGo ls :: ErrorMessage where
+  ShowListGo '[] = Text ""
+  ShowListGo (x ': xs) = ShowType x :<>: Text ", " :<>: ShowListGo xs
+
+type ShowList ls = Text "[" :<>: ShowListGo ls :<>: Text "]"
+
+
+#else
+
+-- GHC < 8
+class ElemNotFoundIn val list
+
+#endif
+
+-- $setup
+-- >>> import Data.Proxy
+-- >>> data OK = OK deriving (Show)
+-- >>> let ok :: ctx => Proxy ctx -> OK; ok _ = OK
diff --git a/servant/test/Servant/Utils/LinksSpec.hs b/servant/test/Servant/Utils/LinksSpec.hs
index fbc5ce0b..6a6bb8dc 100644
--- a/servant/test/Servant/Utils/LinksSpec.hs
+++ b/servant/test/Servant/Utils/LinksSpec.hs
@@ -10,7 +10,6 @@ import           Test.Hspec              (Expectation, Spec, describe, it,
 import           Data.String             (fromString)
 
 import           Servant.API
-import           Servant.API.TypeLevel
 
 type TestApi =
   -- Capture and query params

From 02e4281d513b887f2123ec7ab31b21a9c830f5a4 Mon Sep 17 00:00:00 2001
From: "Julian K. Arni" <jkarni@gmail.com>
Date: Mon, 22 Aug 2016 12:44:39 -0300
Subject: [PATCH 07/12] Custom type errors

---
 servant/src/Servant/API/TypeLevel.hs | 51 +++++++++++++++-------------
 1 file changed, 28 insertions(+), 23 deletions(-)

diff --git a/servant/src/Servant/API/TypeLevel.hs b/servant/src/Servant/API/TypeLevel.hs
index 759d89c0..f61c9b51 100644
--- a/servant/src/Servant/API/TypeLevel.hs
+++ b/servant/src/Servant/API/TypeLevel.hs
@@ -110,7 +110,8 @@ type family IsSubList a b :: Constraint where
     IsSubList '[] b          = ()
     IsSubList (x ': xs) y    = Elem x y `And` IsSubList xs y
 
--- | Check that an eleme is an element of a list:
+#if !MIN_VERSION_base(4,9,0)
+-- | Check that a value is an element of a list:
 --
 -- >>> ok (Proxy :: Proxy (Elem Bool '[Int, Bool]))
 -- OK
@@ -121,13 +122,31 @@ type family IsSubList a b :: Constraint where
 --       arising from a use of ‘ok’
 -- ...
 type Elem e es = ElemGo e es es
+#else
+-- | 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] expected in list '[Int, Bool]
+-- ...
+type Elem e es = ElemGo e es es
+#endif
 
 -- '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
 
@@ -144,30 +163,16 @@ type family And (a :: Constraint) (b :: Constraint) :: Constraint where
 
 -- * Custom type errors
 
-#if MIN_VERSION_base(4,9,0)
--- GHC >= 8
-
-
-type ElemNotFoundIn val list = TypeError
-  (ShowType val :<>: Text " expected in list " :<>: ShowList list)
-
-
--- Utilities
-
-type family ShowListGo ls :: ErrorMessage where
-  ShowListGo '[] = Text ""
-  ShowListGo (x ': xs) = ShowType x :<>: Text ", " :<>: ShowListGo xs
-
-type ShowList ls = Text "[" :<>: ShowListGo ls :<>: Text "]"
-
-
-#else
-
--- GHC < 8
+#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
 -- >>> import Data.Proxy
 -- >>> data OK = OK deriving (Show)

From 931e67f3471640af81946a963bba42ab2afae6ad Mon Sep 17 00:00:00 2001
From: "Julian K. Arni" <jkarni@gmail.com>
Date: Thu, 25 Aug 2016 11:56:04 -0300
Subject: [PATCH 08/12] Loads of documetation and doctests.

---
 servant/src/Servant/API/TypeLevel.hs | 196 +++++++++++++++++----------
 1 file changed, 128 insertions(+), 68 deletions(-)

diff --git a/servant/src/Servant/API/TypeLevel.hs b/servant/src/Servant/API/TypeLevel.hs
index f61c9b51..23e44b70 100644
--- a/servant/src/Servant/API/TypeLevel.hs
+++ b/servant/src/Servant/API/TypeLevel.hs
@@ -1,29 +1,51 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE CPP                   #-}
+{-# LANGUAGE ConstraintKinds       #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE KindSignatures        #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE UndecidableInstances #-}
+{-# 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 where
 
-import GHC.Exts(Constraint)
-import Servant.API.Capture ( Capture, CaptureAll )
-import Servant.API.ReqBody ( ReqBody )
-import Servant.API.QueryParam ( QueryParam, QueryParams, QueryFlag )
-import Servant.API.Header ( Header )
-import Servant.API.Verbs ( Verb )
-import Servant.API.Sub ( type (:>) )
-import Servant.API.Alternative ( type (:<|>) )
+
+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(..))
+import           GHC.TypeLits            (TypeError, ErrorMessage(..))
 #endif
 
+
+
 -- * API predicates
 
 -- | Flatten API into a list of endpoints.
+--
+-- >>> :t showType @(Endpoints SampleAPI)
+-- ...
+-- ... :: Proxy
+-- ...  '["hello" :> Verb 'GET 200 '[JSON] Int,
+-- ...    "bye"
+-- ...    :> (Capture "name" String
+-- ...        :> Verb 'POST 200 '[JSON, PlainText] Bool)]
 type family Endpoints api where
   Endpoints (a :<|> b) = AppendList (Endpoints a) (Endpoints b)
   Endpoints (e :> a)   = MapSub e (Endpoints a)
@@ -47,24 +69,56 @@ type family IsElem' a s :: Constraint
 
 -- | Closed type family, check if @endpoint@ is within @api@.
 -- Uses @'IsElem''@ if it exhausts all other options.
+--
+-- >>> ok @(IsElem ("hello" :> Get '[JSON] Int) SampleAPI)
+-- OK
+--
+-- >>> ok @(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 @(IsElem (Get '[JSON] Int) (Header "h" Bool :> Get '[JSON] Int))
+-- OK
+--
+-- >>> ok @(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
+  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@.
+-- | Check whether @sub@ is a sub-API of @api@.
+--
+-- >>> ok @(IsSubAPI SampleAPI (SampleAPI :<|> Get '[JSON] Int))
+-- OK
+--
+-- >>> ok @(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
 
@@ -76,18 +130,31 @@ type family AllIsElem xs api :: Constraint where
 -- ** Strict inclusion
 
 -- | Closed type family, check if @endpoint@ is exactly within @api@.
--- We aren't sure what affects how an endpoint is built up, so we require an
--- exact match.
+--
+-- >>> ok @(IsIn ("hello" :> Get '[JSON] Int) SampleAPI)
+-- OK
+--
+-- Unlike 'IsElem', this requires an *exact* match.
+--
+-- >>> ok @(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                           = ()
+  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 @(AllIsIn (Endpoints SampleAPI) SampleAPI)
+-- OK
 type family AllIsIn xs api :: Constraint where
   AllIsIn '[] api = ()
   AllIsIn (x ': xs) api = (IsIn x api, AllIsIn xs api)
@@ -107,45 +174,31 @@ type family AppendList xs ys where
   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
+  IsSubList '[] b          = ()
+  IsSubList (x ': xs) y    = Elem x y `And` IsSubList xs y
 
-#if !MIN_VERSION_base(4,9,0)
 -- | Check that a value is an element of a list:
 --
--- >>> ok (Proxy :: Proxy (Elem Bool '[Int, Bool]))
+-- >>> ok @(Elem Bool '[Int, Bool])
 -- OK
 --
--- >>> ok (Proxy  :: Proxy (Elem String '[Int, Bool]))
--- ...
---     No instance for (ElemNotFoundIn [Char] '[Int, Bool])
---       arising from a use of ‘ok’
--- ...
-type Elem e es = ElemGo e es es
-#else
--- | 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]))
+-- >>> ok @(Elem String '[Int, Bool])
 -- ...
 -- ... [Char] expected in list '[Int, Bool]
 -- ...
 type Elem e es = ElemGo e es es
-#endif
 
 -- '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
+  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)
+  -- Note [Custom Errors]
+  ElemGo x '[] orig       = TypeError ('ShowType x
+                                 ':<>: 'Text " expected in list "
+                                 ':<>: 'ShowType orig)
 #else
-    ElemGo x '[] orig       = ElemNotFoundIn x orig
+  ElemGo x '[] orig       = ElemNotFoundIn x orig
 #endif
 
 -- ** Logic
@@ -154,12 +207,12 @@ type family ElemGo e es orig :: Constraint where
 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 ()       = ()
+  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 () ()     = ()
+  And () ()     = ()
 
 -- * Custom type errors
 
@@ -173,7 +226,14 @@ 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
+-- >>> :set -XTypeApplications
+-- >>> :set -XPolyKinds
 -- >>> import Data.Proxy
--- >>> data OK = OK deriving (Show)
--- >>> let ok :: ctx => Proxy ctx -> OK; ok _ = OK
+-- >>> import Servant.API
+-- >>> data OK ctx = OK deriving (Show)
+-- >>> let ok :: ctx => OK ctx; ok = OK
+-- >>> let showType :: Proxy a ; showType = Proxy
+-- >>> type SampleAPI = "hello" :> Get '[JSON] Int :<|> "bye" :> Capture "name" String :> Post '[JSON, PlainText] Bool
+-- >>> let sampleAPI = Proxy :: Proxy SampleAPI

From 6cf3188907141996ac664301022999ee9952ae91 Mon Sep 17 00:00:00 2001
From: Oleg Grenrus <oleg.grenrus@iki.fi>
Date: Mon, 16 Jan 2017 13:43:24 +0200
Subject: [PATCH 09/12] Fix doctests

---
 servant/src/Servant/API/TypeLevel.hs | 48 +++++++++++++---------------
 1 file changed, 22 insertions(+), 26 deletions(-)

diff --git a/servant/src/Servant/API/TypeLevel.hs b/servant/src/Servant/API/TypeLevel.hs
index 23e44b70..13813b17 100644
--- a/servant/src/Servant/API/TypeLevel.hs
+++ b/servant/src/Servant/API/TypeLevel.hs
@@ -39,13 +39,8 @@ import           GHC.TypeLits            (TypeError, ErrorMessage(..))
 
 -- | Flatten API into a list of endpoints.
 --
--- >>> :t showType @(Endpoints SampleAPI)
--- ...
--- ... :: Proxy
--- ...  '["hello" :> Verb 'GET 200 '[JSON] Int,
--- ...    "bye"
--- ...    :> (Capture "name" String
--- ...        :> Verb 'POST 200 '[JSON, PlainText] Bool)]
+-- >>> 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)
@@ -70,21 +65,21 @@ type family IsElem' a s :: Constraint
 -- | Closed type family, check if @endpoint@ is within @api@.
 -- Uses @'IsElem''@ if it exhausts all other options.
 --
--- >>> ok @(IsElem ("hello" :> Get '[JSON] Int) SampleAPI)
+-- >>> ok (Proxy :: Proxy (IsElem ("hello" :> Get '[JSON] Int) SampleAPI))
 -- OK
 --
--- >>> ok @(IsElem ("bye" :> Get '[JSON] Int) SampleAPI)
+-- >>> ok (Proxy :: Proxy (IsElem ("bye" :> Get '[JSON] Int) SampleAPI))
 -- ...
--- ... Could not deduce: ...
+-- ... Could not deduce...
 -- ...
 --
 -- An endpoint is considered within an api even if it is missing combinators
 -- that don't affect the URL:
 --
--- >>> ok @(IsElem (Get '[JSON] Int) (Header "h" Bool :> Get '[JSON] Int))
+-- >>> ok (Proxy :: Proxy (IsElem (Get '[JSON] Int) (Header "h" Bool :> Get '[JSON] Int)))
 -- OK
 --
--- >>> ok @(IsElem (Get '[JSON] Int) (ReqBody '[JSON] Bool :> Get '[JSON] Int))
+-- >>> 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
@@ -110,12 +105,12 @@ type family IsElem endpoint api :: Constraint where
 
 -- | Check whether @sub@ is a sub-API of @api@.
 --
--- >>> ok @(IsSubAPI SampleAPI (SampleAPI :<|> Get '[JSON] Int))
+-- >>> ok (Proxy :: Proxy (IsSubAPI SampleAPI (SampleAPI :<|> Get '[JSON] Int)))
 -- OK
 --
--- >>> ok @(IsSubAPI (SampleAPI :<|> Get '[JSON] Int) SampleAPI)
+-- >>> ok (Proxy :: Proxy (IsSubAPI (SampleAPI :<|> Get '[JSON] Int) SampleAPI))
 -- ...
--- ... Could not deduce: ...
+-- ... Could not deduce...
 -- ...
 --
 -- This uses @IsElem@ for checking; thus the note there applies here.
@@ -131,14 +126,14 @@ type family AllIsElem xs api :: Constraint where
 
 -- | Closed type family, check if @endpoint@ is exactly within @api@.
 --
--- >>> ok @(IsIn ("hello" :> Get '[JSON] Int) SampleAPI)
+-- >>> ok (Proxy :: Proxy (IsIn ("hello" :> Get '[JSON] Int) SampleAPI))
 -- OK
 --
 -- Unlike 'IsElem', this requires an *exact* match.
 --
--- >>> ok @(IsIn (Get '[JSON] Int) (Header "h" Bool :> Get '[JSON] Int))
+-- >>> ok (Proxy :: Proxy (IsIn (Get '[JSON] Int) (Header "h" Bool :> Get '[JSON] Int)))
 -- ...
--- ... Could not deduce: ...
+-- ... Could not deduce...
 -- ...
 type family IsIn (endpoint :: *) (api :: *) :: Constraint where
   IsIn e (sa :<|> sb)                = Or (IsIn e sa) (IsIn e sb)
@@ -153,7 +148,7 @@ type family IsStrictSubAPI sub api :: Constraint where
 
 -- | Check that every element of @xs@ is an endpoint of @api@ (using @'IsIn'@).
 --
--- OK @(AllIsIn (Endpoints SampleAPI) SampleAPI)
+-- ok (Proxy :: Proxy (AllIsIn (Endpoints SampleAPI) SampleAPI))
 -- OK
 type family AllIsIn xs api :: Constraint where
   AllIsIn '[] api = ()
@@ -179,12 +174,12 @@ type family IsSubList a b :: Constraint where
 
 -- | Check that a value is an element of a list:
 --
--- >>> ok @(Elem Bool '[Int, Bool])
+-- >>> ok (Proxy :: Proxy (Elem Bool '[Int, Bool]))
 -- OK
 --
--- >>> ok @(Elem String '[Int, Bool])
+-- >>> ok (Proxy :: Proxy (Elem String '[Int, Bool]))
 -- ...
--- ... [Char] expected in list '[Int, Bool]
+-- ... [Char]...'[Int, Bool...
 -- ...
 type Elem e es = ElemGo e es es
 
@@ -228,12 +223,13 @@ families are not evaluated (see https://ghc.haskell.org/trac/ghc/ticket/12048).
 
 
 -- $setup
--- >>> :set -XTypeApplications
 -- >>> :set -XPolyKinds
+-- >>> :set -XGADTs
 -- >>> import Data.Proxy
+-- >>> import Data.Type.Equality
 -- >>> import Servant.API
--- >>> data OK ctx = OK deriving (Show)
--- >>> let ok :: ctx => OK ctx; ok = OK
--- >>> let showType :: Proxy a ; showType = Proxy
+-- >>> 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

From 3c83f615caf0ca24cec062fc03d75541a2e81647 Mon Sep 17 00:00:00 2001
From: Oleg Grenrus <oleg.grenrus@iki.fi>
Date: Mon, 16 Jan 2017 13:54:00 +0200
Subject: [PATCH 10/12] Write explicit export list in Servant.API.TypeLevel

---
 servant/src/Servant/API/TypeLevel.hs | 30 +++++++++++++++++++++++++++-
 1 file changed, 29 insertions(+), 1 deletion(-)

diff --git a/servant/src/Servant/API/TypeLevel.hs b/servant/src/Servant/API/TypeLevel.hs
index 13813b17..2a7aeb44 100644
--- a/servant/src/Servant/API/TypeLevel.hs
+++ b/servant/src/Servant/API/TypeLevel.hs
@@ -18,7 +18,32 @@ The code samples in this module use the following type synonym:
 >             :<|> "bye" :> Capture "name" String :> Post '[JSON, PlainText] Bool
 
 -}
-module Servant.API.TypeLevel where
+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,
+    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)
@@ -223,6 +248,9 @@ 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

From 55c8f0b4a1361f51dfec460c62935d4e41b2b072 Mon Sep 17 00:00:00 2001
From: Oleg Grenrus <oleg.grenrus@iki.fi>
Date: Mon, 16 Jan 2017 13:59:24 +0200
Subject: [PATCH 11/12] Add changelog entry

---
 servant/CHANGELOG.md | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/servant/CHANGELOG.md b/servant/CHANGELOG.md
index 0232c4f5..f7f7988b 100644
--- a/servant/CHANGELOG.md
+++ b/servant/CHANGELOG.md
@@ -8,6 +8,10 @@
   use its `ToHttpApiData` instance or `linkURI`.
   ([#527](https://github.com/haskell-servant/servant/issues/527))
 
+* Add `Servant.API.TypeLevel` module with type families to work with API types.
+  ([#345](https://github.com/haskell-servant/servant/pull/345))
+  ([#305](https://github.com/haskell-servant/servant/issues/305))
+
 0.9.1
 ------
 

From c7c6c054a5195b1ad992d52c417e3ed2b42e2955 Mon Sep 17 00:00:00 2001
From: Oleg Grenrus <oleg.grenrus@iki.fi>
Date: Mon, 16 Jan 2017 14:36:51 +0200
Subject: [PATCH 12/12] Add Logic subsection to the export list

---
 servant/src/Servant/API/TypeLevel.hs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/servant/src/Servant/API/TypeLevel.hs b/servant/src/Servant/API/TypeLevel.hs
index 2a7aeb44..3cb8076b 100644
--- a/servant/src/Servant/API/TypeLevel.hs
+++ b/servant/src/Servant/API/TypeLevel.hs
@@ -38,6 +38,7 @@ module Servant.API.TypeLevel (
     IsSubList,
     Elem,
     ElemGo,
+    -- ** Logic
     Or,
     And,
     -- * Custom type errors