#12569: TypeApplications allows instantiation of implicitly-quantified kind variables -------------------------------------+------------------------------------- Reporter: vagarenko | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by adamgundry): * cc: adamgundry, goldfire (added) * keywords: => TypeApplications * component: Compiler => Compiler (Type checker) Comment: I believe the ticked/unticked constructor mechanism is working as designed, but you may be on to something with your "weird" example. == To tick or not to tick == Without a tick, `[0]` as a type is in fact ill-kinded. `[0]` is syntactic sugar for `[] 0` where `[] :: * -> *` is the list type constructor. Moreover, `0` does not have kind `*`. This is why you get two errors from `foo @[0]`. With a tick, `'[0]` is syntactic sugar for `0 ': '[]` (i.e. a promoted list of one element) and has kind `[Nat]` as expected. A tick is necessary when a data constructor and type constructor have the same name, and you want to refer to the data constructor in the type namespace. In the case of `True` and `'True`, in the absence of a type constructor `True`, this is genuinely unambiguous and the tick is optional. == The actual bug == (Whether the constructor is ticked or not is irrelevant here.) When you write `let foo :: forall (x :: k). (); foo = ()`, GHC implicitly quantifies over the kind variable `k` to give `foo :: forall k (x :: k) . ()`. I would expect that `k` would not be available for instantiation via a type application, but apparently it is, because `foo @True` is rejected but `foo @Bool @True` is accepted. I think we should have `foo :: forall {k} (x :: k) . ()` instead. @goldfire, would you agree that this should be changed? In any case, we should document this case in the manual. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12569#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler