@@ -1,8 +1,11 @@
1+{-# LANGUAGE CPP #-}
12{-# LANGUAGE DataKinds #-}
23{-# LANGUAGE KindSignatures #-}
34{-# LANGUAGE PolyKinds #-}
45{-# LANGUAGE TypeFamilies #-}
56{-# LANGUAGE TypeOperators #-}
7+{-# LANGUAGE ConstraintKinds #-}
8+{-# LANGUAGE MultiParamTypeClasses #-}
69{-# LANGUAGE UndecidableInstances #-}
710module Servant.API.TypeLevel where
811
@@ -14,6 +17,9 @@ import Servant.API.Header ( Header )
1417import Servant.API.Verbs ( Verb )
1518import Servant.API.Sub ( type (:>) )
1619import Servant.API.Alternative ( type (:<|>) )
20+#if MIN_VERSION_base(4,9,0)
21+import GHC.TypeLits (TypeError, ErrorMessage(..))
22+#endif
1723
1824-- * API predicates
1925
@@ -104,9 +110,24 @@ type family IsSubList a b :: Constraint where
104110 IsSubList '[] b = ()
105111 IsSubList (x ': xs) y = Elem x y `And` IsSubList xs y
106112
107−type family Elem e es :: Constraint where
108− Elem x (x ': xs) = ()
109− Elem y (x ': xs) = Elem y xs
113+-- | Check that an eleme is an element of a list:
114+--
115+-- >>> ok (Proxy :: Proxy (Elem Bool '[Int, Bool]))
116+-- OK
117+--
118+-- >>> ok (Proxy :: Proxy (Elem String '[Int, Bool]))
119+-- ...
120+-- No instance for (ElemNotFoundIn [Char] '[Int, Bool])
121+-- arising from a use of ‘ok’
122+-- ...
123+type Elem e es = ElemGo e es es
124+
125+-- 'orig' is used to store original list for better error messages
126+type family ElemGo e es orig :: Constraint where
127+ ElemGo x (x ': xs) orig = ()
128+ ElemGo y (x ': xs) orig = ElemGo y xs orig
129+ ElemGo x '[] orig = ElemNotFoundIn x orig
130+
110131
111132-- ** Logic
112133
@@ -121,3 +142,33 @@ type family Or (a :: Constraint) (b :: Constraint) :: Constraint where
121142type family And (a :: Constraint) (b :: Constraint) :: Constraint where
122143 And () () = ()
123144
145+-- * Custom type errors
146+
147+#if MIN_VERSION_base(4,9,0)
148+-- GHC >= 8
149+
150+
151+type ElemNotFoundIn val list = TypeError
152+ (ShowType val :<>: Text " expected in list " :<>: ShowList list)
153+
154+
155+-- Utilities
156+
157+type family ShowListGo ls :: ErrorMessage where
158+ ShowListGo '[] = Text ""
159+ ShowListGo (x ': xs) = ShowType x :<>: Text ", " :<>: ShowListGo xs
160+
161+type ShowList ls = Text "[" :<>: ShowListGo ls :<>: Text "]"
162+
163+
164+#else
165+
166+-- GHC < 8
167+class ElemNotFoundIn val list
168+
169+#endif
170+
171+-- $setup
172+-- >>> import Data.Proxy
173+-- >>> data OK = OK deriving (Show)
174+-- >>> let ok :: ctx => Proxy ctx -> OK; ok _ = OK