Skip to content
This repository was archived by the owner on Aug 3, 2024. It is now read-only.

Comments

Add kind signatures to tyvars with kind not 'Type'#915

Merged
sjakobi merged 2 commits intohaskell:wip/hi-haddockfrom
harpocrates:kind-sigs
Aug 23, 2018
Merged

Add kind signatures to tyvars with kind not 'Type'#915
sjakobi merged 2 commits intohaskell:wip/hi-haddockfrom
harpocrates:kind-sigs

Conversation

@harpocrates
Copy link
Collaborator

This means that the kinds do not get completely swallowed up in
signatures where they matter, for instance in

 foo :: forall proxy (a :: ()). proxy a

It also means that all higher-kinded type variables now have
explicit kinds.

/cc @sjakobi


I don't think this is what we ultimately want, but we definitely want at least some of these kind annotations. I'm open to implementing any ideas people may have for constraining the number of annotations we show.

The FunArgs test is what initially motivated me to make these changes:

  • On ghc-head:
    screen shot 2018-08-22 at 12 14 56 am

  • On wip/hi-haddock:
    screen shot 2018-08-22 at 12 16 45 am

  • On this branch:
    screen shot 2018-08-22 at 12 15 09 am

This means that the kinds do not get completely swallowed up in
signatures where they matter, like

     foo :: forall proxy (a :: ()). proxy a

It also means that _all_ higher-kinded type variables now have
explicit kinds.
The idea is to hide kind signatures for type variables where the kind can be
inferred from at least one use of the type variable in the given type. This
seems to strike a nice balance between maintaining existing behaviour and
showing something that isn't incorrect.
@harpocrates
Copy link
Collaborator Author

I've come up with what I think is a decent heuristic for hiding some kind signatures and foralls. In particular, we drop kind signatures for type variables when

  • the type variable has at least one use site in the type where it is fully applied
  • the fully applied use site has kind Type
  • at the fully applied use site, the the (kind) arguments of the kind of the type variable match exactly the kind of the arguments to the type variable

For example, consider the type variable m in mapM :: (Traversable t, Monad m) => (a -> m b) -> t a -> m (t b). Here is the logic around not needing a kind annotation for m:

  • take the m b use site
  • m b :: Type
  • m :: Type -> _ and b :: Type

Finally, if all of the type variables in a type end up not needing kind signatures (and the order in which the type variables are mentioned matches the order of the explicit foralls), we drop the whole forall ....

Working on wip/hi-haddock, it turns out that these heuristics cause almost all kind signatures on functions to disappear. (Those on data declarations and classes remain - but I like that!)

Screenshots

For the FunArgs test case, we get:

screen shot 2018-08-23 at 1 20 05 pm

Copy link
Member

@sjakobi sjakobi left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Great stuff! :)

@sjakobi sjakobi merged commit b128737 into haskell:wip/hi-haddock Aug 23, 2018
@harpocrates harpocrates deleted the kind-sigs branch October 16, 2018 20:00
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants