[GHC] #12569: TypeApplications allows instantiation of implicitly-quantified kind variables

[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:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 I see no bugs here, except possibly bugs in error messages /
 documentation.

 The tick is merely at the level of name resolution. When GHC sees an
 unticked constructor-like name (that is, a capitalized identifier, an
 identifier starting with a colon, or a use of list syntax in a type), it
 looks to see if there is a type constructor of that name. If there is, it
 uses the type name. If there is not, it looks for a data constructor of
 that name. And that's it. There is no type-directed lookup here.

 So, when you say `[0]`, without the tick, GHC uses the type `[]` which has
 the wrong kind. You're right that you "obviously" mean `'[]`, but this
 would require type-directed name resolution, which GHC does not support.
 This all works for `True` because there is no type named `True`. (If there
 were -- try declaring one! -- then your `True` example wouldn't work.)

 As for `TypeApplications` quantification: if you have mentioned the name
 of the type/kind variable in the text of your program, it is available for
 quantification. That's the simple rule, and there are no exceptions
 (barring bugs in implementation, of which there are several). So, for `foo
 :: forall (x :: k). ...`, both `k` and `x` are available for visible type
 application. GHC quantifies the variables in left-to-right order and then
 does a stable topological sort, putting depended-on variables before their
 dependencies. (A topological sort is a sort that puts depended-on things
 before dependencies, and "stable" here means that there is no extra
 violations of the left-to-right ordering of quantification.) In this case,
 we get `k` and then `x`. This is explained in the manual
 [https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html
 #visible-type-application here].

 I'm happy to take concrete suggestions for improvement, either of the
 manual or of error messages here. Or, of course, we can debate whether the
 current behavior is desired -- I'm certainly not wedded to it, but it does
 seem like a good compromise between the availability of visible type
 application and need to write `forall` a lot.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12569#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler