Should have more kind signatures, particularly (a :: *)

[mgsloan]

I noticed that the definition of Capture is data Capture (sym :: Symbol) a. The problem with this is that it allows me to write nonsense like Capture "foo" Maybe :> Post '[JSON] (), and only get a type error later when matching up the implementations with the type specs. The error would be much nicer if the definition of Capture was instead data Capture (sym :: Symbol) (a :: *). Similar should be done for some other types, definitely CaptureAll, ReqBody, QueryParam, QueryParams. BasicAuth already has it. This is not by any means an exhaustive list. I'm new to servant and I just opened up a few modules to see how widespread this was.

I think this will make some errors a bit kinder.

Also, I was quite confused that I was able to write Capture "foo" :> Post '[JSON] (). Note the missing type argument on Capture. I suppose the reason this isn't done is that it's desired to have an open world of types for APIs, and we don't have anything like "kind constraints"? I guess I'm spoiled by typechecking and expect similar at the kind level.

[alpmestan]

Hello @mgsloan,

You are making some good points. When we know that we are going to get something of kind * and that anything else just doesn't make sense (that's the case for all the combinators that you point out, namely Capture, CaptureAll, etc.), there's just no good reason not to. I think we consistently do this for type level lists or strings so there's no reason not to do it for the most common of all kinds, *. I don't know how nicer the errors get with those changes either, but I'm convinced this would be a strict improvement.

Regarding the last case that you mention, namely the fact that you can define an API type without supplying all the parameters of Capture, this is indeed something we cannot do much about. While the RHS of :> is always of kind *, its LHS in practice either has kind Symbol or * (because we want to make type level strings special, we don't want to be forced say type API = Static "foo" :> Capture "fooid" FooId :> Get '[JSON] Foo, writing the strings directly is just so handy and nicer to read), so we to need to allow other kinds than * in the LHS of :>. The definition we have therefore is: data (path :: k) :> a.

Would you be interested in giving a shot at a PR to add the missing kind signatures?

[mgsloan]

Sure!

[mgsloan]

While the RHS of :> is always of kind *, its LHS in practice either has kind Symbol or * (because we want to make type level strings special, we don't want to be forced say type API = Static "foo" :> Capture "fooid" FooId :> Get '[JSON] Foo, writing the strings directly is just so handy and nicer to read)

IMHO this is a design mistake. If concision is the concern you could have data S (s :: Symbol). This turns things that should be kind errors into huge confusing type errors. But, uh, it's not up to me and I realize it'd be a huge breaking change.

I guess we can hope that the kinds of type errors this generates will motivate some ghc error reporting enhancements.

[jkarni]

IMHO this is a design mistake. If concision is the concern you could have data S (s :: Symbol). This turns things that should be kind errors into huge confusing type errors. But, uh, it's not up to me and I realize it'd be a huge breaking change.

@mgsloan In theory we could have a type family and have our cake and eat it too:

import GHC.TypeLits

data Path k = Path
  deriving (Show)

-- Our old :> 
data Sub (a :: *) (b :: *)

type family (:>) (i :: n) (j :: *) :: * where
  (s :: Symbol) :> b = Path s `Sub`  b
  (k :: *) :> b = k `Sub` b
  -- For appropriate GHC versions
  (k :: other) :> b = TypeError ('Text "Expected something of kind Symbol or *, got: "
                            ':<>: 'ShowType k
                            ':<>: 'Text " on the LHS of ':>'")

main :: IO ()
main = print (undefined :: Sub :> Int)

giving:

.../TF.hs:24:8: error:
    • Expected something of kind Symbol or *, got: Sub on the LHS of ':>'
    • In the expression: print (undefined :: Sub :> Int)
      In an equation for ‘main’: main = print (undefined :: Sub :> Int)

And at least for the common use cases this would be backwards compatible. But, all the instances mentioning :> would have to be changed, which would be pretty horrible.

The simpler option, which we've discussed before but never implemented, is to just have an overlapping instances for HasServer (x :> b) for polykinded x that is not Symbol or * that throws a custom type error (or for earlier GHC versions has an informatively-named but unsatisfiable constraint). The point here is that we can make our own typechecker, and don't have to limit ourselves to the kindchecker.

[mgsloan]

And at least for the common use cases this would be backwards compatible. But, all the instances mentioning :> would have to be changed, which would be pretty horrible.

Do users ever write instances for it? If not, seems ok. I'm not sure - pretty new to using servant.

The simpler option, which we've discussed before but never implemented, is to just have an overlapping instances for HasServer (x :> b) for polykinded x that is not Symbol or * that throws a custom type error (or for earlier GHC versions has an informatively-named but unsatisfiable constraint). The point here is that we can make our own typechecker, and don't have to limit ourselves to the kindchecker.

That is a cool solution, thanks for describing it!

[fizruk]

Do users ever write instances for it?

@mgsloan yes, it is very common to define instances for custom combinators like this:

instance HasServer api => HasServer (CustomCombinator :> api) where
  ...

Since there are a lot of interpretations (type classes) and a lot of combinators, that's indeed a lot of code to update, including user code.

[mgsloan]

I see, good to know!

[alpmestan]

In fact, any instance that's not for a "terminating symbol" of our DSL (Get, Post etc, so more generally anything defined in terms of Verb) is defined with the very shape that you're discussing: instance (HasXXX api, OtherStuffs) => HasXXX (MyCombinator :> api) where ....

[mgsloan]

Merged, so closing

[phadej]

*Servant> serve (Proxy :: Proxy (Capture "foo" :> Get '[JSON] Int)) undefined

<interactive>:6:1: error:
    • What are you doing
    • In the expression:
        serve (Proxy :: Proxy (Capture "foo" :> Get '[JSON] Int)) undefined

with (tested only with GHC-8.2.2):

diff --git a/servant-server/src/Servant/Server/Internal.hs b/servant-server/src/Servant/Server/Internal.hs
index cf454fe..b6acdf8 100644
--- a/servant-server/src/Servant/Server/Internal.hs
+++ b/servant-server/src/Servant/Server/Internal.hs
@@ -41,8 +41,9 @@ import           Data.String.Conversions    (cs, (<>))
 import           Data.Tagged                (Tagged(..), retag, untag)
 import qualified Data.Text                  as T
 import           Data.Typeable
+import           Data.Void
 import           GHC.TypeLits               (KnownNat, KnownSymbol, natVal,
-                                             symbolVal)
+                                             symbolVal, TypeError, ErrorMessage (..))
 import           Network.HTTP.Types         hiding (Header, ResponseHeaders)
 import qualified Network.HTTP.Media         as NHM
 import           Network.Socket             (SockAddr)
@@ -504,6 +505,11 @@ instance (KnownSymbol sym, HasServer api context)
           examine v | v == "true" || v == "1" || v == "" = True
                     | otherwise = False
 
+instance TypeError ('Text "What are you doing") => HasServer ((arr :: k -> l) :> api) context where
+    type ServerT (arr :> api) m = Void
+    route Proxy _context _d = error "sooner or later you'd call absurd"
+    hoistServerWithContext _ _ _ = id
+

---

Does anyone else see why forbidding (k -> l) kind as LHS of :> would be bad? It would catch non complete applications...

Maybe having that instance for non TypeError GHCs too, asking for Void (or better named type for that purpose), would make type-errors better, will it?

Does someone want to give a shot?