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

mentioned in issue #13985 (closed)

changed weight to 5

added Tbug Trac import TypeInType typechecker labels

mentioned in issue #14131 (closed)

I ended up needing to fix this as a part of an unrelated patch, D3872. (Note that I borrowed the solution for this particular issue from Richard, so the credit should go to him.)

Trac metadata

Trac field	Value
Differential revisions	- → D3872

1. ..but D3872 is in limbo for the time being, so I'll set the resolution back to "new" again.

Trac metadata

Trac field	Value
Differential revisions	D3872 → -

1. ..and now D3872 is back! Re-setting the Differential revision.

Trac metadata

Trac field	Value
Differential revisions	- → D3872

I decided to split this off into its own Diff, since it's a somewhat hefty patch by itself.

Trac metadata

Trac field	Value
Differential revisions	D3872 → D3902
Blocking	- → #14131 (closed)

mentioned in commit b9ac9e05

Can this be considered resolved?

Trac metadata

Trac field	Value
Test case	- → ghci/scripts/T13988

closed

changed milestone to %8.4.1

Replying to [ticket:13988#comment:141912 bgamari]:

Can this be considered resolved?

Indeed it can.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

added incorrect runtime result label

added Pnormal label