
#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