Inconsistent treatment of implicitly bound kind variables as freefloating
(Spun off from the discussion starting at https://phabricator.haskell.org/D3872#109927.)
This program is accepted:
{# 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 (closed), 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:
{# 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 theforall
itself. That is:MkFoo :: (forall {k} (a :: k). Proxy k a) > Foo

Something else. When you try a similar trick with type synonyms:
{# 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 toAny
:λ> :i Foo3 type Foo3 = forall (a :: GHC.Types.Any). Proxy a
Would that be an appropriate trick for data types as well?