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