[GHC] #13988: GADT constructor with kind equality constraint quantifies unused existential type variables

[GHC]

#13988: GADT constructor with kind equality constraint quantifies unused
existential type variables
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
  (Type checker)                     |
           Keywords:  TypeInType     |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  Incorrect result
  Unknown/Multiple                   |  at runtime
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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
 }}}

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