
Hi everyone, The proposal is about adding stand-alone kind signatures for type declarations: https://github.com/ghc-proposals/ghc-proposals/pull/54 The basic idea is to add support for kind signatures like this: type T :: Type -> Type -> Type data T a b = ... Signatures would be introduced by the keyword 'type' and could be provided for data types, type synonyms, type families and classes. The extension would be enable via -XTopLevelKinds. Additionally, complete user-supplied kind signatures (CUSKs, see https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts...) would be given a separate language extension, -XCUSKs which would be on by default for now but turned off in GHC 8.8 and then deprecated and removed. The proposal depends on #81. Feedback has been positive and this is rather cleaner than the current story so I'm in favour of accepting this. Like Richard, I'm not really happy with the name "TopLevelKinds", especially since signatures for associated types aren't even on the top level. Would something like StandAloneKinds or ExplicitKindSignatures be better? One minor point that isn't clear to me: the proposal says that "Associated types may be given kind signatures within their classes". Are type variables mentioned in the class head visible in the kind signature for the associated type? Thanks, Roman

I’m strongly in favour of #54. The current CUSK stuff is a huge mess. The inability to write a kind signature for a type constructor is terrible.
One minor point that isn't clear to me: the proposal says that "Associated types may be given kind signatures within their classes". Are type variables mentioned in the class head visible in the kind signature for the associated type?
Good point. I was going to say “behave like GADTs” where the variables in the header do not scope over the signatures; but unfortunately in class decls the variables in the header *do* scope over the (term-level) signatures.
Richard, what do you think? Maybe associated types should only be given kind signatures at the top level (alongside the kind signature for the class). That would at least be clear.
Simon
From: ghc-steering-committee

On Aug 17, 2018, at 7:24 AM, Simon Peyton Jones via ghc-steering-committee
wrote: Good point. I was going to say “behave like GADTs” where the variables in the header do not scope over the signatures; but unfortunately in class decls the variables in the header *do* scope over the (term-level) signatures.
It's even worse than this. Not only do they scope over term-level signatures, but they scope over associated type declarations. (Confusingly, they do not scope over associated type family default equations.)
Richard, what do you think? Maybe associated types should only be given kind signatures at the top level (alongside the kind signature for the class). That would at least be clear.
That would be clear and unambiguous, but quite awkward: class C a where type F a b type F :: ... Why does one `type` appear in within the class but the other does not? We have some long-winded arguments here to answer that question, but it's all unsatisfying. I don't have a better idea, though. Separately, we could just tack this new feature into -XKindSignatures instead of inventing a new extension.... but making a change to an extension as stable and as old as -XKindSignatures is unfortunate. Richard

Hi, Am Freitag, den 17.08.2018, 11:24 +0000 schrieb Simon Peyton Jones via ghc-steering-committee:
I’m strongly in favour of #54.
and nobody disagrees, accepted. Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/
participants (4)
-
Joachim Breitner
-
Richard Eisenberg
-
Roman Leshchinskiy
-
Simon Peyton Jones