#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... #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