#13761: Can't create poly-kinded GADT with TypeInType enabled, but can without -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Another workaround is to explicitly quantify the kind like so: {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeInType #-} module Works2 where import Data.Kind data T :: forall (k :: Type). k -> Type where MkT :: T Int }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13761#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13761: Can't create poly-kinded GADT with TypeInType enabled, but can without -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:2 goldfire]:

This behavior is all expected... or, in one case, not unexpected.

The very first example in the OP is regrettable, but it is "not unexpected", as `-XNoTypeInType` rejects such programs on a best-effort basis. That one is hard.

The other examples are all consequences of [https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts... #complete-user-supplied-kind-signatures-and-polymorphic-recursion the CUSK rules].

Proposed solution: allow top-level kind signatures of type-level declarations (just like we have top-level type signatures of term-level declarations) and deprecate CUSKs. One Of These Days, I will write a ghc-

Thanks for the link. I'm a bit embarrassed to say I didn't think to look in the users' guide to see if CUSKs were documented, but I'm glad they are! proposal for this. If I may ask, what do you mean by "top-level kind signature" here? I thought that {{{#!hs data T :: forall k. k -> Type }}} //was// a top-level kind signature, but perhaps you meant something different? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13761#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13761: Can't create poly-kinded GADT with TypeInType enabled, but can without -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: invalid | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => invalid Comment: Thanks! That proposal sounds like an interesting solution. Since the original bug is expected behavior (and documented, no less), I'm going to close this ticket. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13761#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13761: Can't create poly-kinded GADT with TypeInType enabled, but can without -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: invalid | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): A separate kind signature will be understood independent of the type definition -- much like how type signatures on functions are understood (and kind-generalized) independently of the body. For example, consider {{{ data Proxy (a :: k) = P data S :: Proxy k -> Type where MkS :: S (P :: Proxy Maybe) }}} What's the type of `k`? Taking the definition into account, we can see that `k :: Type -> Type`. But if we must take the definition into account, then we don't have a CUSK, by definition. Currently, the declaration above causes GHC to complain that `Type -> Type` does not match `k`, as we're using `S` at a different instantiation in its body than in its head (i.e. using polymorphic recursion). Change to {{{ data S :: forall k. Proxy k -> Type where ... }}} and now we get {{{ You have written a *complete user-suppled kind signature*, but the following variable is undetermined: k0 :: * Perhaps add a kind signature. }}} This is quite correct. The declaration looks like it has a CUSK, but really it doesn't. Instead, we can write {{{ data S :: forall (k :: Type -> Type). Proxy k -> Type where ... }}} or {{{ data S :: forall (kk :: Type) (k :: kk). Proxy k -> Type where ... }}} both of which are accepted. Note that these define ''different'' types: the second defines a kind-indexed GADT. The point of all this is that it's incredibly confusing. Much better would be (*) A definition can use polymorphic recursion if it has a standalone type/kind signature. Simple! It works for types and terms. And it's exactly what happens for terms today. Under (*), all the declarations for `S` would be rejected, as none of them have a standalone kind signature. (The proposal will also describe `-XCUSKs`, on by default, that retains the current behavior. This extension will be off by default and deprecated in due course.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13761#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13761: Can't create poly-kinded GADT with TypeInType enabled, but can without -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: invalid | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:8 simonpj]:

The thing you say is "incredibly confusing" is that the switch from inferred to specified is based on some fairly subtle syntactic rules, and you'd like to have a clearer syntactic distinction. It's a software engineering issue, not a technical one.

Yes, precisely. There's no real technical challenge here. I just want an easy way for the user to say what they mean: inference or specification. The problem with the CUSK rules as they are is that sometimes you've written a CUSK when you don't mean to. For example {{{ data T (a :: Proxy k) where ... }}} According to the rules, this declaration has a CUSK. But suppose I want `k`'s kind to be inferred. The only way to do so is to write {{{ data T :: Proxy k -> Type where ... }}} This form is a CUSK with `-XNoTypeInType` but is ''not'' a CUSK with `-XTypeInType`. The reason for the extra rule with `-XTypeInType` is to support this case, where the user wants inference. (Note that with `-XNoTypeInType`, `k`'s kind will always by `Type`, and so the issue of inference doesn't arise.) This particular problem is worse for closed type families and for classes, where there is no alternate syntax available if the user does not want a CUSK. The intent of my proposal is to make all of this simpler: the user simply says whether they want inference (no kind sig) or specification (kind sig). No fiddly rules. No exceptions. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13761#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler