TypeApplications allows instantiation of implicitly-quantified kind variables

TypeApplications doesn't allow unticked list constructor even when it is unambiguous:

GHCi, version 8.0.1: http://www.haskell.org/ghc/  :? for help
> :set -XDataKinds
> :set -XTypeApplications
> :set -XScopedTypeVariables
> :set -XKindSignatures
> let foo :: forall (xs :: [Nat]). (); foo = ()
> foo @'[0]
()
> foo @[0]

<interactive>:17:6: error:
    * Expected kind `[Nat]', but `[0]' has kind `*'
    * In the type `[0]'
      In the expression: foo @[0]
      In an equation for `it': it = foo @[0]

<interactive>:17:7: error:
    * Expected a type, but `0' has kind `Nat'
    * In the type `[0]'
      In the expression: foo @[0]
      In an equation for `it': it = foo @[0]

why [0] has kind * here?

However this is legal:

> let foo :: forall (x :: Bool). (); foo = ()
> foo @True
()
> foo @'True
()

and this is wierd:

> :set -XPolyKinds
> let foo :: forall (x :: k). (); foo = ()
> foo @'True

<interactive>:12:6: error:
    * Expected a type, but 'True has kind `Bool'
    * In the type `True'
      In the expression: foo @True
      In an equation for `it': it = foo @True
> foo @True

<interactive>:13:6: error:
    * Expected a type, but 'True has kind `Bool'
    * In the type `True'
      In the expression: foo @True
      In an equation for `it': it = foo @True

Trac metadata

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tbug Trac import labels

changed title from TypeApplications doesn't allow unticked list constructors. to TypeApplications allows instantiation of implicitly-quantified kind variables

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.

Trac metadata

Trac field	Value
Component	Compiler → Compiler (Type checker)

added TypeApplications typechecker labels

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

Ah, I imagined that the left-to-right collection and topological sorting of variables applied only when there wasn't an explicit forall. My expectation was that if the user gives an explicit forall, only the binding occurrences would be available for visible type application. Thus forall (x :: k) would make x available alone, whereas forall k (x :: k) would make both k and x available.

I think this alternative would be better, because otherwise there is no way to get at forall {k} (x :: k), is there? Unless we permit visibility annotations in concrete syntax, I suppose...

In any case, this deserves explicit mention in the manual, including the forall (x :: k) example, whichever treatment it ends up getting.

added Pnormal label