Add IsIn and IsSubAPI constraints

Author: fizruk

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