New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Treat kind and type vars identically with `forall` #103

Merged
merged 5 commits into from May 22, 2018

Conversation

Projects
None yet
6 participants
@goldfirere
Contributor

goldfirere commented Jan 6, 2018

GHC brings kind variables into scope implicitly, even when it would refuse the same service for type variables. This legacy behavior is no longer necessary.

Rendered

@RyanGlScott

This comment has been minimized.

Contributor

RyanGlScott commented Jan 7, 2018

I'll admit that I'm left hanging after reading this proposal, because this doesn't appear to address the most common way to implicitly quantify kind variables (at least in my experience), which is:

j2 :: forall (a :: k). Proxy a -> ()

I'm putting this in a separate category from your j example because one could argue that it satisfies the "forall-or-nothing" rule, since k is specified (despite being quantified implicitly). Does this proposal favor making j2 an error as well?

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Jan 7, 2018

Does this proposal favor making j2 an error as well?

Yes. Perhaps I'm in the minority here (as @simonpj has said something similar to you, @RyanGlScott), but I don't see a substantive difference between my j and your j2. Both mention k only in occurrences, not binding sites. Whether or not the occurrence happens in a kind signature of a binder or somewhere else seems unimportant, to me.

All that said, if a chorus of voices suggest that we treat occurrences in the kind signatures of binders differently than other occurrences, we could consider it. But before going in that direction, how would you feel about

z :: forall (a :: ...blah blah blah lots of constructors... k ...blah blah blah...). Proxy a -> ()

Would you still want k implicitly brought into scope?

@RyanGlScott

This comment has been minimized.

Contributor

RyanGlScott commented Jan 7, 2018

I could lean either way on this particular issue, but it is worth noting that making j2 an error is a positively enormous breaking change, and one that isn't particularly easy to support alongside multiple versions of GHC without unsightly uses of CPP. Perhaps that shouldn't be the primary motivator for how to design this, but it is worth considering carefully. After all, implicitly quantifying kind variables has been around for much longer than explicitly quantifying kind variables (for only two GHC major releases).

Another thing that's worth pointing out is that GHC is not particularly diligent about following the "forall-or-nothing" rule (at least, according to how you've described it in the proposal). For instance, GHC happily accepts the following:

{-# LANGUAGE RankNTypes #-}
f :: a -> forall b. b -> Either c b
f _ = Right

Despite the fact that the explicit forall does not specify a or c.

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Jan 7, 2018

I agree that this would be a major breaking change. This is why this proposal specifies that the new behavior would take effect only 2 releases after #83 is implemented, so that the migration is straightforward.

As for your example, that type signature does not begin with forall, and so does not invoke the forall-or-nothing rule.

@RyanGlScott

This comment has been minimized.

Contributor

RyanGlScott commented Jan 7, 2018

As for your example, that type signature does not begin with forall, and so does not invoke the forall-or-nothing rule.

That's good to know, but the proposal as currently written does not state this requirement. Currently, it simply reads:

if you write an explicit forall in a type signature, you must specify all the type variables brought into scope.

This does not mention anything about beginning the type signature with an explicit forall, merely that it contains one.

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Jan 7, 2018

Fair enough. Fixed.

@simonpj

This comment has been minimized.

Contributor

simonpj commented Jan 8, 2018

I'm strongly in favour. As thing stand, given

data T p q r s = ...
data S k (a::k) = ....
f :: forall a. ....(T (blah :: k) b (blah :: b) c)...S w a....
f = e
  • the variable c is not brought into scope (in e) because it only occurs in a "type position"
  • the variable k is brought into scope because it only occurs in a "kind position"
  • the variable b is in a funny zone: it occurs in both a "type position" and a "kind position" so its status isn't clear
  • the variable w is a required, explicit kind argument to S (it's not optional at S's usage sites). But it's clearly a kind variable. Is it brought into scope in e?

Given that that, with TypeInType there is literally no difference between type and kind variables, these questions are extremely uncomfortable. It's absurd that something as fundamental as lexical scoping is dependent on the vagaries of the occurrences of a variable, deep within a type.

A whole mess of code exists solely to make these distinctions. I don't even know what decision it takes about the latter two cases. Sometimes it takes a lot of code to implement simple uniform things; but often it's a sign that something is wrong. And that's the case here.

We have to fix this!

@andrewthad

This comment has been minimized.

Contributor

andrewthad commented Jan 23, 2018

I'm strongly in favor of this proposal. The breakage that @RyanGlScott describes is unfortunate (it will be very difficult to write polykinded code that works with GHC 8.10 and GHC 7.10), but my experience has been that libraries that use a lot of GHC's type level features tend to only support the newest two or three releases of GHC anyway.

@RyanGlScott

This comment has been minimized.

Contributor

RyanGlScott commented Jan 24, 2018

Out of curiosity, how strict will GHC be in enforcing the structure of telescopes? I ask because I realized today that GHC currently accepts this definition (originally spotted here):

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Foo where

import Data.Proxy

f :: forall k a. Proxy (a :: k)
f = Proxy

I believe this technically satisfies the forall-or-nothing rule, since k is explicitly bound. This program is also of interest because GHC will accept it with just PolyKinds (and doesn't require TypeInType), whereas this equivalent program:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Bar where

import Data.Proxy

f :: forall k (a :: k). Proxy a
f = Proxy

Will be rejected for not using TypeInType, providing an interest twist on the backwards-compat-breakage side of things.

@RyanGlScott

This comment has been minimized.

Contributor

RyanGlScott commented Jan 24, 2018

Granted, you might argue the fact that Foo typechecks without TypeInType is a bug. (See Trac #14170.) If so, then this point is a bit moot.

@RyanGlScott

This comment has been minimized.

Contributor

RyanGlScott commented Jan 26, 2018

Sorry, this point is already moot, as I didn't notice that this proposal says that:

this proposal assumes that proposal #83 has been accepted, meaning that explicit quantification over kind variables is possible with only -XPolyKinds, not needing -XTypeInType.

So we need not gnash our teeth about whether TypeInType is required—it won't be, as it'll be deprecated.

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Jan 26, 2018

It looks like you've answered your own question, Ryan. But the fact that the code is accepted without TypeInType is indeed a bug, as you suggest.

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Jan 26, 2018

Conversation seems to have died out here. I will submit this to the committee soonish, so speak up if you'd like any revisions!

@RyanGlScott

This comment has been minimized.

Contributor

RyanGlScott commented Jan 26, 2018

One more question: does this proposal have any effect on type signatures where an explicit forall is not required to make type variables scope over the body? For instance, this currently typechecks by bringing k into scope over the body of def, even though k is implicitly quantified:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Foo where

import Data.Proxy

class Default a where
  def :: a

instance Default (Proxy (a :: k)) where
  def = Proxy @(a :: k)

Will that change with this proposal? If not, would it affect it if you had written it this way, using an explicit forall plus implicit quantification?

instance forall (a :: k). Default (Proxy a) where
  def = Proxy @(a :: k)
@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Jan 26, 2018

The forall-or-nothing rule applies to instances. So, under this proposal, the last snippet in your comment would be rejected as in violation of the rule. The treatment of the first snippet is unchanged.

I'll clarify the proposal.

RyanGlScott added a commit to goldfirere/singletons that referenced this pull request Jan 30, 2018

Explicitly quantify some kind variables in foralls
This in preparation in a world where implicitly quantifying kind
variables is outlawed in type signatures headed by a `forall`, as
per this proposal:
ghc-proposals/ghc-proposals#103

This is not the end of the story, as TH-generated code often contains
implicitly bound kind variables that defy this new
`forall`-or-nothing rule. See
#297.

@RyanGlScott RyanGlScott referenced this pull request Feb 9, 2018

Merged

Embrace (Type :: Type) #83

goldfirere added a commit to goldfirere/ghc-proposals that referenced this pull request Feb 9, 2018

@RyanGlScott

This comment has been minimized.

Contributor

RyanGlScott commented Feb 9, 2018

I have another question about the definition you're giving for the forall-or-nothing rule. Currently, it says:

if you begin a type signature with an explicit forall, you must specify all the type variables brought into scope.

Does this apply equally to kind signatures? For instance, you can write this in today's GHC:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}

import Data.Kind

data Foo :: forall a. a -> b -> Type where
  MkFoo :: a -> Foo a b

Despite the fact that Foo's kind signature is headed by a forall, and b isn't explicitly quantified.

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Feb 10, 2018

That's a good point about kind signatures. I think that's a bug (inconsistent design) and should be fixed, regardless of this proposal.

@RyanGlScott

This comment has been minimized.

Contributor

RyanGlScott commented Feb 12, 2018

Very well. I've opened GHC Trac #14795 for this.

@simonpj

This comment has been minimized.

Contributor

simonpj commented Feb 22, 2018

I remain strongly in favour. Let's submit this to the committee.

I wonder whether we need wait quite as long as proposed before introducing this!

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Feb 22, 2018

Indeed. Let's send this to the committee @nomeata. I've updated the proposal to list the one substantive new alternative that arose from this conversation. Thanks!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment