Declarations with standalone kind signatures are rendered without kinds

[RyanGlScott]

If I run this code through Haddock 2.24.0:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
module Foo where

type Comp :: (b -> c) -> (a -> b) -> (a -> c)
type Comp f g x = f (g x)

This is how it is rendered:

This is a bit of a shame, as Haddock completely loses the kind information associated with the standalone kind signature. For a more elaborate example of where this happens, see the Hackage documentation for singletons-2.7 (example).

I can see two possible solutions:

1. Render standalone kind signatures in Haddock. This would be a rather large undertaking, and there are several design considerations that I'm not sure about.

2. When processing a declaration with a standalone kind signature, then render it as if it had been written using inline kind annotations. In other words, render Comp above like this instead:

   

   This is arguably somewhat hackier, but it accomplishes the goal of displaying the kind information without having to support rendering standalone kind signatures in full.

[RyanGlScott]

Solution (2) would have to be implemented carefully. Here is a tricky corner case:

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
module Foo where

import Data.Kind

type D :: (j -> Type) -> (j -> Type) -> Type
data D (f :: k -> Type) g = forall (a :: k). MkD (f a) (g a)

How should data D be rendered? It has both a standalone kind signature and inline kind information. Here are two incorrect ways to render it:

• Overwrite D's inline kind information with the standalone kind signature's kinds. In other words, render D like this:

  data D (f :: j -> Type) (g :: j -> Type) = forall (a :: k). MkD (f a) (g a)

  This is wrong, however, since k is now out of scope.

• Use the standalone kind signature's kinds, but keep the inline kind information whenever it is available. This would cause D to be rendered like so:

  data D (f :: k -> Type) (g :: j -> Type) = forall (a :: k). MkD (f a) (g a)

  This is also wrong, since it conveys the idea that f and g have different kinds.

The only sensible ways to render D would be one of the following:

• data D (f :: j -> Type) (g :: j -> Type) = forall (a :: j). MkD (f a) (g a)

• data D (f :: k -> Type) (g :: k -> Type) = forall (a :: k). MkD (f a) (g a)

Either option would require at least one kind substitution. It's not clear to me if one option would be easier to implement than the other.

[RyanGlScott]

See goldfirere/singletons#466 for an example of where this limitation occurs "in practice". In particular, goldfirere/singletons#466 (comment) contains a laundry list of obstacles that I ran into when trying to implement option (1) from #1178 (comment).

[vdukhovni]

Reading over the previous comments, it seems to me that (1) is the only plausible path forward, along the lines of goldfirere/singletons#466 with boring kind signatures elided. If the kind and the type are always presented together there'd be no need for a separate namespace to refer to the kind signature. As for documentation, of both the SAKS and the type declaration have haddock comments, present both, with wherever the type definition appears in the docs. I don't think there's a way to export just a kind signature without a definition, so the definition controls the placement of the text.

This just came up in MR 6969 where Compare a b was missing the kind signature that gave it proper context...