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 foralls:

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