[GHC] #13848: Unexpected order of variable quantification with GADT constructor

[GHC]

#13848: Unexpected order of variable quantification with GADT constructor
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
  TypeApplications                   |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Here's some code:

 {{{#!hs
 {-# 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:

 {{{#!hs
 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`.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13848>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler