[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 (Type    |              Version:  8.2.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #7873             |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Old description:

> (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 it's strange becuase the `k` is existential, so
> the definition is probably unusable.
>
> 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?

New description:

 (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 it's strange becuase the `k` is existential, so
 the definition is probably unusable.

 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:

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

   {{{#!hs
   MkFoo :: (forall {k} (a :: k). Proxy k a) -> Foo
   }}}
 4. 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?

--

Comment (by goldfire):

 Nice description of the problem.

 I'll respond to your proposed solutions.

 1. Yes.

 2. No. H98 syntax should not be in the business of guessing existential
 variables. Existentials are a bit strange and should be strictly opt-in
 (at least for H98 syntax).

 3. No. We stopped inferring kind quantification anywhere nested within a
 type with GHC 8.

 4. We could do this, but I doubt it's what the user wants. Indeed, I think
 it would be an improvement to reject that type synonym, which is probably
 not what the user wants at all.

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