GADT constructor with kind equality constraint quantifies unused existential type variables

Reproducible with GHC 8.0.1., 8.0.2, 8.2.1, or HEAD (but I'll use GHC 8.2.1 to show the results of :type +v):

$ /opt/ghc/8.2.1/bin/ghci
GHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
λ> :set -XTypeInType -XGADTs -fprint-explicit-foralls 
λ> import Data.Kind
λ> data Foo (a :: k) where MkFoo :: (k ~ Type) => Foo (a :: k)
λ> :type +v MkFoo
MkFoo :: forall k1 (a :: k1) k2 (k3 :: k2). k1 ~ * => Foo a

Note that MkFoo quantifies two extra existential type variables, k2 and k3 which are completely unused!

Note that this does not occur if the MkFoo constructor uses an explicit forall:

λ> :set -XScopedTypeVariables 
λ> data Foo (a :: k) where MkFoo :: forall k (a :: k). (k ~ Type) => Foo (a :: k)
λ> :type +v MkFoo
MkFoo :: forall k (a :: k). k ~ * => Foo a

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