Opened 13 months ago

Last modified 7 weeks ago

#14198 new bug

Inconsistent treatment of implicitly bound kind variables as free-floating

Reported by: RyanGlScott Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.2.1
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: #14268 Blocking:
Related Tickets: #7873, #15474 Differential Rev(s):
Wiki Page:

Description (last modified by goldfire)

(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, 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:

  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:
MkFoo :: (forall {k} (a :: k). Proxy k a) -> Foo
  1. 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 to Any:

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

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

Change History (9)

comment:1 Changed 13 months ago by simonpj

Description: modified (diff)

comment:2 Changed 13 months ago by goldfire

Description: modified (diff)

Nice description of the problem.

I'll respond to your proposed solutions.

  1. Yes.
  1. 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).
  1. No. We stopped inferring kind quantification anywhere nested within a type with GHC 8.
  1. 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.

comment:3 Changed 13 months ago by RyanGlScott

Going with option 1 (have both be an error) sounds fine to me. But I'm not quite sure what the error message should be when we encounter an inferred, free-floating kind variable, as in data Foo = MkFoo (forall a. Proxy a), where the k in (a :: k) is inferred. We could go with the usual Kind variable ‘k’ is implicitly bound in data type fare, but users might find that befuddling.

comment:4 Changed 13 months ago by goldfire

I think we actually have the opportunity for a good error message here. I think we'll know that the k is not user-written, because it will be Inferred, not Specified. So we can say that the variable was inferred instead of just calling it an inscrutable k0.

comment:5 in reply to:  4 Changed 13 months ago by RyanGlScott

Replying to goldfire:

I think we'll know that the k is not user-written, because it will be Inferred, not Specified.

So you wish to perform free-floating checks on TyConBinders instead of TyVars? That might work... but wait. How would this work for data family instances? IIUC, they don't have anything like TyConBinders, so I'm not sure how we'd perform this check there.

comment:6 Changed 13 months ago by goldfire

OK. Perhaps I'm just wrong. I didn't look at the code to compose comment:4.

comment:7 Changed 6 months ago by RyanGlScott

Blocked By: 14268 added

Note that data family instances will gain TyVarBndrs once #14268 is implemented, so let's wait until that is done before coming back to this issue.

comment:8 Changed 7 weeks ago by RyanGlScott

See #15474 for another ticket about type Foo3 in the original comment.

comment:9 Changed 7 weeks ago by simonpj

Keywords: TypeInType added
Note: See TracTickets for help on using tickets.