singletons-2.7's Haddocks omit the kinds of type families

[RyanGlScott]

While browsing the Haddocks for singletons-2.7 recently, I came across this:

Notice how Flip has no kind information whatsoever! Contrast this with how Flip is rendered here in the Haddocks for singletons-2.6:

I'm using Flip as an example, but this problem applies to basically every TH-generated promoted type family, defunctionalization symbol, and singleton type. Eek.

What changed between singletons-2.6 and singletons-2.7? There's a superficial difference between the way Flip is defined between the two versions, as singletons-2.6 defines Flip like shown above (modulo TH-generated oddities), whereas singletons-2.7 defines Flip with a standalone kind signature:

type Flip :: (a ~> b ~> c) -> b -> a -> c
type family Flip f x y where ...

This raises another question: why doesn't Haddock just render the standalone kind signature for Flip? Unfortunately, this is because of a deficiency of Haddock—see haskell/haddock#1178. Fixing haskell/haddock#1178 would be a pretty tall order, so I don't foresee things changing any time soon on Haddock's end.

In the meantime, I we could make things slightly more tolerable for Haddock users. Since Haddock simply drops standalone kind signatures, we can give it more kind information in the body:

type Flip :: (a ~> b ~> c) -> b -> a -> c
type family Flip (f :: a ~> b ~> c) (x :: b) (y :: a) :: c where ...

Indeed, singletons-th already computes the argument and result kinds in this fashion, but it currently avoids putting them into the body of the type family under the guise that this information is redundant. However, given the existence of haskell/haddock#1178, it might be worth including this redundant information for the benefit of Haddock readers.

[int-index]

I'd just go with solution (1) in haskell/haddock#1178 and render SAKS unconditionally.

[RyanGlScott]

Certainly, fixing haskell/haddock#1178 would be ideal. In fact, I tried implementing solution (1) myself, but it turns out that there are a lot of tricky design decisions one must figure out:

• Where should the Haddocks themselves be placed? Consider this example:

  -- | Some Haddocks.
  type T :: Type -> Type
  data T a

  Haddock comments are always attached to some form of declaration, but surprisingly, the Haddock comment above isn't attached to the SAK, but rather the body. It's as if you had written this:

  type T :: Type -> Type
  -- | Some Haddocks.
  data T a

  Is this an acceptable state of affairs? If not, should we tweak Haddock so that comments can be attached to SAKS as well? If so, what happens in situations like this?

  -- | SAK Haddocks.
  type T :: Type -> Type
  -- | Body Haddocks.
  data T a

• How should hyperlinking to declarations with SAKS work? For example, http://hackage.haskell.org/package/singletons-2.7/docs/Data-Singletons-Prelude.html#t:Flip currently links to the body of Flip. If Flip's SAK were rendered, however, should that hyperlink point to the SAK instead? (This choice is important, since it's conceivable that the SAK and the body might have different Haddocks.) If so, will we need to introduce another hyperlink suffix (besides t:Flip) for pointing to the bodies of declarations?

• What should the policy for rendering the SAKS of declarations loaded from interface files be? This is a strange question to ask, but Haddock has completely different code paths for rendering "in-place" declarations defined within the same package versus rendering declarations that must be loaded from external interface files.

  Rendering "in-place" declarations are much easier, since Haddock simply uses the GHC AST to figure out how they should be rendered. With interface-file declarations, however, Haddock must start with Core and reverse-engineer the original declaration. In particular, Core does not record whether an entity was declared with a SAK or not. Does this mean that we should render SAKS for every declaration that is loaded from an interface file?

  Assuming the answer to the above question is "yes", there are still some additional questions to answer. Suppose this declaration were loaded from an interface file:

  type S :: Type -> Type
  data S (a :: Type) :: Type where ...

  The kind annotation on a, as well as the :: Type kind annotation, are redundant, so Haddock might consider omitting those. But we cannot omit all kind information from the body in general. This example, for instance, will not kind-check without the kind annotation on a:

  type KindOf :: k -> Type
  type KindOf (a :: k) = k

  In light of this, what policy should we adopt when determining how to render "inline" kinds?

• How should SAKS be rendered in the Haddock preview pane? Consider how SMaybe is rendered in the preview pane below, for example:

  

  What should be done with its SAK type SMaybe :: Maybe a -> Type in the preview? Should we render both the SAK and the body? Just the SAK? Just the body? Moreover, should the policy differ for declarations that have SAKS and those that don't?

• The concerns above all apply the the XHTML backend in Haddock. But there are other backends to consider as well, including the LaTeX and Hoogle backends. I haven't given them much thought, but it's possible that there could be other backend-specific design considerations there as well.

In light of all this uncertainty, I abandoned my attempt at implementing solution (1). This is the main reason why I predicted in #466 (comment) that I don't foresee things changing any time soon on Haddock's end.

[int-index]

Is this an acceptable state of affairs?

I don't see why it's a problem. Consider the declaration and its SAKS as a single unit, with a documentation comment that applies to both of them.

Does this mean that we should render SAKS for every declaration that is loaded from an interface file?

Indeed, that's what I meant when I said "unconditionally". Just render SAKS for every type, as :info does.

This example, for instance, will not kind-check without the kind annotation on a:

type KindOf :: k -> Type
type KindOf (a :: k) = k

In light of this, what policy should we adopt when determining how to render "inline" kinds?

I'd say the solution here is ghc-proposals/ghc-proposals#326. Render it as follows:

type KindOf :: k -> Type
type KindOf @k a = k

And the policy is to show those invisible binders on LHS that are used on the RHS. For example,type S1 (a :: k) (b :: j) = k would be rendered as:

type S1 :: k -> j -> Type
type S1 @k a b = k

No @j binder because it's not used on the RHS. And type S2 (a :: k) (b :: j) (c :: h) = (k, h) would be rendered as:

type S2 :: k -> j -> h -> Type
type S2 @k @_ @h a b c = (k, h)

We must skip a binder for j using @_ in order to bind @h.

What should be done with its SAK type SMaybe :: Maybe a -> Type in the preview? Should we render both the SAK and the body?

For the preview, I'd say we need to define "boring" kinds and render only the interesting ones. Personally, I think boring kinds are defined by the following grammar:

k ::= Type | Constraint | Type -> k

So Type, Type -> Type, Type -> Type -> Type, etc, are not worthy of a SAKS in the preview pane. Anything else (higher-kinded types, poly-kinds, data-kinds, etc) gives useful info to the user.

[goldfirere]

I agree wholeheartedly with @int-index above. And the summary of issues is very helpful, @RyanGlScott. Thanks.

[RyanGlScott]

I broadly agree with the design in #466 (comment), but at the same time, I don't see this being implemented any time soon. In light of this, I still think it would be worthwhile to include redundant kind information in TH-generated declarations, which would be trivial to implement. Do you agree?

[goldfirere]

If it's indeed easy to implement, then yes.

[RyanGlScott]

See #467. This PR appears large from a glance, but only because (1) lots of test cases needed to be updated, and (2) I had to update several hand-written declarations to match the new redundant kind policy.

[RyanGlScott]

Fixed in #467.