[GHC] #12569: TypeApplications allows instantiation of implicitly-quantified kind variables (was: TypeApplications doesn't allow unticked list constructors.)

[GHC]

#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