@@ -27,41 +27,46 @@ import Prelude.Compat
2727
2828import Servant.API
2929
30+-- | Helper type family to state the 'Enter' symmetry.
3031type family Entered m n api where
31− Entered m n (m a) = n a
3232 Entered m n (a -> api) = a -> Entered m n api
33+ Entered m n (m a) = n a
3334 Entered m n (api1 :<|> api2) = Entered m n api1 :<|> Entered m n api2
3435
35−class ( Entered m n typ ~ ret
36− , Entered n m ret ~ typ
37− )
38− => Enter typ m n ret
36+class
37+ ( Entered m n typ ~ ret
38+ , Entered n m ret ~ typ
39+ ) => Enter typ m n ret | typ m n -> ret, ret m n -> typ, ret typ m -> n, ret typ n -> m
3940 where
41+ -- | Map the leafs of an API type.
4042 enter :: (m :~> n) -> typ -> ret
4143
42−-- ** Servant combinators
44+-- ** Servant combinators
4345
4446instance
45− ( Entered m1 n1 (typ1 :<|> typ2) ~ (ret1 :<|> ret2)
46− , Entered n1 m1 (ret1 :<|> ret2) ~ (typ1 :<|> typ2)
47− , Enter typ1 m1 n1 ret1, Enter typ2 m2 n2 ret2
47+ ( Enter typ1 m1 n1 ret1, Enter typ2 m2 n2 ret2
4848 , m1 ~ m2, n1 ~ n2
49+ , Entered m1 n1 (typ1 :<|> typ2) ~ (ret1 :<|> ret2)
50+ , Entered n1 m1 (ret1 :<|> ret2) ~ (typ1 :<|> typ2)
4951 ) => Enter (typ1 :<|> typ2) m1 n1 (ret1 :<|> ret2)
5052 where
5153 enter e (a :<|> b) = enter e a :<|> enter e b
5254
5355instance
54− ( Entered m n (a -> typ) ~ (a -> ret)
56+ ( Enter typ m n ret
57+ , Entered m n (a -> typ) ~ (a -> ret)
5558 , Entered n m (a -> ret) ~ (a -> typ)
56− , Enter typ m n ret
57− )
58− => Enter (a -> typ) m n (a -> ret)
59+ ) => Enter (a -> typ) m n (a -> ret)
5960 where
6061 enter arg f a = enter arg (f a)
6162
62−-- ** Useful instances
63+-- ** Leaf instances
6364
64−instance Enter (m a) m n (n a) where
65+instance
66+ ( Entered m n (m a) ~ n a
67+ , Entered n m (n a) ~ m a
68+ ) => Enter (m a) m n (n a)
69+ where
6570 enter (NT f) = f
6671
6772-- | Like `lift`.