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 |