## Unexpected order of variable quantification with GADT constructor

Here's some code:

```
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Foo where
data N = Z | S N
data Vec (n :: N) a where
VNil :: forall a. Vec Z a
VCons :: forall n a. a -> Vec n a -> Vec (S n) a
```

I want to use `TypeApplications`

on `VCons`

. I tried doing so in GHCi:

```
GHCi, version 8.2.0.20170523: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo ( Foo.hs, interpreted )
Ok, modules loaded: Foo.
λ> :set -XTypeApplications -XDataKinds
λ> :t VCons @Z @Int 1 VNil
<interactive>:1:8: error:
• Expected a type, but ‘'Z’ has kind ‘N’
• In the type ‘Z’
In the expression: VCons @Z @Int 1 VNil
<interactive>:1:11: error:
• Expected kind ‘N’, but ‘Int’ has kind ‘*’
• In the type ‘Int’
In the expression: VCons @Z @Int 1 VNil
<interactive>:1:17: error:
• Couldn't match type ‘'Z’ with ‘Int’
Expected type: Vec Int 'Z
Actual type: Vec 'Z 'Z
• In the fourth argument of ‘VCons’, namely ‘VNil’
In the expression: VCons @Z @Int 1 VNil
```

Huh? That's strange, I would have expected the first type application to be of kind `N`

, and the second to be of kind `*`

. But GHC disagrees!

```
λ> :set -fprint-explicit-foralls
λ> :type +v VCons
VCons :: forall a (n :: N). a -> Vec n a -> Vec ('S n) a
```

That's downright unintuitive to me, since I explicitly specified the order in which the quantified variables should appear in the type signature for `VCons`

.

Similarly, if you leave out the `forall`

s:

```
data Vec (n :: N) a where
VNil :: Vec Z a
VCons :: a -> Vec n a -> Vec (S n) a
```

Then `:type +v`

will also report the same quantified variable order for `VCons`

. This is perhaps less surprising, since the `n`

and `a`

in `data Vec (n :: N) a`

don't scope over the constructors, so GHC must infer the topological order in which the variables appear in each constructor. But I would certainly not expect GHC to do this if I manually specify the order with `forall`

.

## Trac metadata

Trac field | Value |
---|---|

Version | 8.0.1 |

Type | Bug |

TypeOfFailure | OtherFailure |

Priority | normal |

Resolution | Unresolved |

Component | Compiler (Type checker) |

Test case | |

Differential revisions | |

BlockedBy | |

Related | |

Blocking | |

CC | |

Operating system | |

Architecture |