Data.Proxy in servant's public API (why Proxy with ScopedTypeVariables doesn't work)

Question

I'm excited about servant, and I'm ok with its internal typelevel magic as long as it doesn't gets in the way, and the only thing that confuses me is its use of a type-proxy in public API. Here's the code:

serve :: HasServer layout => Proxy layout -> Server layout -> Application
serve p server = toApplication (runRouter (route p (return (RR (Right server)))))

As I understand, type-proxies are fairly simple thing and are needed to carry a type when you don't have a value with that type. So why to pass a proxy carrying layout type when there is already layout type in Server's type parameter? I've tried cloning servant's repo and changing code to this:

{-# LANGUAGE ScopedTypeVariables #-}

serve :: forall layout . HasServer layout => Server layout -> Application
serve server = toApplication (runRouter (route p (return (RR (Right server)))))
  where
    p :: Proxy layout
    p  = Proxy

And surprisingly to me this fails to compile (telling something about layout type mismatch). But why, shouldn't my local p have the same layout type as server (with ScopedTypeVariables turned on)?

Answer 1

Type families are not injective, and behind Server there's one. So if you pass a Server MyAPI to this function, GHC won't be able to conclude layout = MyAPI. We unfortunately really need a Proxy in there. Even if we had injective type families, that wouldn't help:

type API1 = Get '[JSON] User
type API2 = Post '[JSON] User

These two APIs are such that Server API1 = Server API2 but API1 /= API2, which actually shows us that Server must not be injective. The easiest way to disambiguate the API type we want to target is the Proxy. On the other hand, that's quite often the only thing our APIs ask for in the various servant packages.

Answer 2

Server isn't a type constructor, it's a type synonym for the ServerT associated type in the HasServer class. Therefore layout occurring in Server layout doesn't disambiguate the HasServer constraint. We can only resolve the Server layout type if we already have a HasServer layout instance.