[GHC] #14198: Inconsistent treatment of implicitly bound kind variables as free-floating

[GHC]

#14198: Inconsistent treatment of implicitly bound kind variables as free-floating
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:  #7873
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 (Spun off from the discussion starting at
 https://phabricator.haskell.org/D3872#109927.)

 This program is accepted:

 {{{#!hs
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}

 import Data.Proxy

 data Foo = MkFoo (forall a. Proxy a)
 }}}

 There's something interesting going on here, however. Because `PolyKinds`
 is enabled, the kind of `a` is generalized to `k`. But where does `k` get
 quantified? It turns out that it's implicitly quantified as an existential
 type variable to `MkFoo`:

 {{{
 λ> :i Foo
 data Foo = forall k. MkFoo (forall (a :: k). Proxy a)
 }}}

 This was brought up some time ago in #7873, where the conclusion was to
 keep this behavior.

 But to make things stranger, it you write out the kind of `a` explicitly:

 {{{#!hs
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}

 import Data.Proxy

 data Foo2 = MkFoo2 (forall (a :: k). Proxy a)
 }}}

 Then GHC will reject it:

 {{{
 Bug.hs:7:1: error:
     Kind variable ‘k’ is implicitly bound in data type
     ‘Foo2’, but does not appear as the kind of any
     of its type variables. Perhaps you meant
     to bind it (with TypeInType) explicitly somewhere?
   |
 7 | data Foo2 = MkFoo2 (forall (a :: k). Proxy a)
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 }}}

 So GHC's treatment is inconsistent. What should GHC do? We could:

 * Have both be an error.
 * Have both be accepted, and implicitly quantify `k` as an existential
 type variable
 * Have both be accepted, and implicitly quantify `k` in the `forall`
 itself. That is:

   {{{#!hs
   MkFoo :: (forall {k} (a :: k). Proxy k a) -> Foo
   }}}
 * Something else. When you try a similar trick with type synonyms:

   {{{#!hs
   {-# LANGUAGE ExistentialQuantification #-}
   {-# LANGUAGE PolyKinds #-}
   {-# LANGUAGE RankNTypes #-}

   import Data.Proxy

   type Foo3 = forall a. Proxy a
   }}}

   Instead of generalizing the kind of `a`, its kind will default to `Any`:

   {{{
   λ> :i Foo3
   type Foo3 = forall (a :: GHC.Types.Any). Proxy a
   }}}

   Would that be an appropriate trick for data types as well?

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