Implement the "Explicit specificity in type variable binders" proposal

changed weight to 5

@rae I'd like to start implementing this. Since I'm not very familiar with the typechecking internals, perhaps I could lay out my plan of attack and you could tell me what I'm missing:

modify HsTyVarBndr to have an extra field indicating whether the user-written type variable is specified or inferred
track those changes through the parser, renamer, desugarer (non of this should be tricky - just plumbing around the new extra field)
modify TH.TyVarBndr to also have an extra field (same purpose as HsTyVarBndr) and follow changes for converting to and from that type
modify something related to bindExplicitTKBndrsX? (this is really what's unclear - where in TcHsType is the logic for choosing ArgFlag's located?)

I've already got something working with the above plan, I'm just not sure it is working for the right reasons

ghci> :set -XPolyKinds -XExplicitForAll -XTypeApplications
ghci> import Data.Proxy
ghci> foo :: forall {k} (a :: k) b. Proxy a -> b; foo = undefined
ghci> :t foo @Int @Bool
foo @Int @Bool :: Proxy Int -> Bool

modify HsTyVarBndr to have an extra field indicating whether the user-written type variable is specified or inferred

Actually I'm not sure that's right. I think you want to modify Var.ForallVisFlag to add ForallInferred. That flag is already in HsForAllTy

data HsType pass
  = HsForAllTy   -- See Note [HsType binders]
      { hst_xforall :: XForAllTy pass
      , hst_fvf     :: ForallVisFlag -- Is this `forall a -> {...}` or
                                     --         `forall a. {...}`?
      , hst_bndrs   :: [LHsTyVarBndr pass]
                                       -- Explicit, user-supplied 'forall a b c'
      , hst_body    :: LHsType pass      -- body type
      }

Then you need to expand these lines in TcHsType.tc_hs_type (the HsForAllTy case)

       ; let argf        = case fvf of
                             ForallVis   -> Required
                             ForallInvis -> Specified

Just add a case for ForallInferred.

Then you need to modify the pretty-printer too, which you don't mention.

In fact I'm suddenly unsure why we have ForallVisFlag at all. Why don't we use ArgFlag?

data ArgFlag = Inferred | Specified | Required

These are precisely ForallInferred, ForAllInvis, and ForallVis respectively. I see no reason to have two. And in fact ForallVisFlag is a better name than ArgFlag.

Richard?

In an unexpected move, I'm going to agree with @harpocrates and disagree with @simonpj. The ForallVisFlag is a flag on the entire forall, indicating whether it ends with a . or an ->. In contrast, explicit specificity requires putting information on each individual binder; that information says whether or not the binder has braces. This is a bit uncomfortable, because now both our concrete and abstract syntaxes will allow nonsense like forall {k} a -> .... What is the visibility of k? Is it Inferred or Required? (I surely hope we don't split the difference and call it Specified!) I think it should just be rejected. But it's awkward that visibility has 3 settings, and yet we discern between two of the 3 per-binder and a different two of the 3 per-forall. I've thought about this some and can't come up with anything better than, say, using forall {k} a <b>. to mean Inferred, Specified, and Required, respectively.

Moving past syntactic choices that have already been approved by the committee:

Yes, I agree with @harpocrates's plan. I recommend putting another flag in the menagerie defined in Var.hs, perhaps HsTyVarBndrFlag. Sadly, reusing types in TH is a pain, so you'll have to define something identical, but distinct, there.

The bindExplicitTKBndrs function is indeed the place to edit, but the actual HsTyVarBndrs are handled in a passed-in helper. So you'll need to edit tcHsTyVarBndr and tcHsQTyVarBndr to return both the fresh TcTyVar and the HsTyVarBndrFlag. This means bindExplicitTKBndrs (in all variants) will have to return a [(TcTyVar, HsTyVarBndrFlag)]. Call sites of bindExplicitTKBndrs generally route the returned tyvars to a mkSpecForAllTys. You will want to write a mkFlagForAllTys :: [(TcTyVar, HsTyVarBndrFlag)] -> Type -> Type function that chooses between Specified and Inferred based on the HsTyVarBndrFlag. In the HsForAllTy case, you will need to look for the possibility of an HsInferred with ForallVis: this is an error. (This might crop up elsewhere, but you should find it in your audit of uses of bindExplicitTKBndrs.)

Do note that you won't have to touch the desugarer: types are already gone by then.

I think that should do it. Thanks much for stepping up to do this! :)

OK now I really am deeply confused.

In the end every type variable in a forall is Inferred, Specified, or Required. The question is what concrete syntax we use to convey that information.

Are you suggesting that to signal Required we use an arrow, and apply that to lots of type variables, but for Inferred we use curly braces and apply that to individual variables. That bizarre. And what would it mean to have curly braces and an arrow? They contradict each other. Surely we can do better?

Maybe we should support

forall a b c -> blah
forall a b c. blah
forall {a b c}. blah

I suppose that would force us into forall {k}. forall (a::k). blah which I guess no one will like.

I don't think the committee ever had this debate. I suppose that we can regard it as purely an issue of convenient concrete syntax, and lay out carefully how the choices work out. That is, no curly braces if you have an arrow.

We have to be careful before slapping flags int HsTyVarBndr. It's used in data type and class declarations

data LHsQTyVars pass   -- See Note [HsType binders]
  = HsQTvs { hsq_ext :: XHsQTvs pass

           , hsq_explicit :: [LHsTyVarBndr pass]
                -- Explicit variables, written by the user
                -- See Note [HsForAllTy tyvar binders]
    }

The proposal doesn't allow curly braces in data type decls.

In fact I think it allow curly braces precisely in the HsForAllTy constructor of HsType. If so, we should stick the flag only in the HsForAllTy constructor, not in HsTyVarBndr. Then you won't have to mess with bindExplicitTKBndrs etc, which is all to do with data type decls.

I don't think this particular point was ever raised in committee, no, but it has been mentioned in various conversations. That's not quite a proper debate, I admit.

Yes, it's a frustrating design. I think requiring more foralls (as you've suggested) will make people less happy, not more (as you admit). I do think my forall <required_var :: blah>. ... syntax has some merit (as a replacement for the freshly implemented VDQ design), but it's not very obvious at all to a reader what the <> signify. Bottom line: I don't have better to suggest. But do feel free to take a stab (any reader of this post).

As to slapping flags in HsTyVarBndr. You might be right that we can just put this in HsForAllTy. Perhaps @harpocrates can check the abstract syntax against the forms mentioned in the proposal to see where it's necessary.

Alec, how's it going? Do you have a patch to look at?

I suppose that would force us into forall {k}. forall (a::k). blah which I guess no one will like.

I would like this! Visibility control is already per-quantifier with forall a. vs forall a ->, and relevance control will be per-quantifier with forall vs foreach. Why make a weird exception and make specificity control per-variable?

If we are willing to go down the route of per-variable specificity control, let's make everything per-variable. Richard suggests forall <a>. vs forall a. (which I don't really like to be honest, this would be the first precedent of using < > as brackets in Haskell), but then what about relevance? How do we choose forall vs foreach per-variable?

Controlling specificity via forall has unfortunate interactions with -XScopedTypeVariables. Consider typeRep :: forall {k}. forall (a :: k). .... Is a in scope in the body of typeRep? I suppose it wouldn't completely kill us if the answer were "no" because of https://github.com/ghc-proposals/ghc-proposals/pull/155, but it's still unfortunate.

That said, I think Vlad has a point about this being an exception to the general trend of marking these decisions higher up in the syntax tree. I don't yet see a good way forward, but my discomfort with this syntax is only growing.

I thought we were going to say

tyepRep :: forall {k} (a::k). blah

Simon, we can still say typeRep :: forall {k}. forall (a::k). blah, can't we?

Richard, this seems to me as an infelicity of ScopedTypeVariables more than anything else. I've been bitten by this before, when I tried something along the lines of f :: forall a. F a -> forall b. F b -> blah and couldn't access b in the body. Why don't we gather type variables from all rank-1 foralls for ScopedTypeVariables?

Alec, how's it going? Do you have a patch to look at?

I expect to have a patch up by the end of the week.

We have to be careful before slapping flags int HsTyVarBndr. It's used in data type and class declarations

As to slapping flags in HsTyVarBndr. You might be right that we can just put this in HsForAllTy. Perhaps @harpocrates can check the abstract syntax against the forms mentioned in the proposal to see where it's necessary.

Yep, that's the large remaining TODO. Perhaps we could parametrize HsTyVarBndr (and it's uses) with some extension argument that gets filled in with NoExt in the cases where inferred type variables don't make sense and HsTyVarBndrFlag where they do? I should check what VDQ does (I imagine forall -> is also not accepted in all places where forall can go).

I agree the concrete syntax leaves something to be desired, especially when you pitch it against the VDQ stuff. Although forall a ->, forall a., forall {a}. will all make sense forall {a} -> is going to be complete bogus. Is it too late to bikeshed this? Not that I have better ideas, I just don't like how ad-hoc the user-facing AST is getting... Perhaps this is an opportunity to redesign the entire forall binder syntax with more of an eye towards the future (ScopedTypeVariables, unifying productions for types and expressions, etc.).

I'd welcome an update to this whole part of the syntax, but I really don't have any good ideas. If you can brainstorm up something good, by all means bring it up. It's not too late.

Perhaps we could parametrize HsTyVarBndr (and it's uses) with some extension argument that gets filled in with NoExt in the cases where inferred type variables don't make sense and HsTyVarBndrFlag where they do?

It would be much simpler and more direct to add the flag in the cases where it's needed. Thus {{{ data HsType pass = HsForAllTy -- See Note [HsType binders] { hst_xforall :: XForAllTy pass , hst_fvf :: ForallVisFlag -- Is this forall a -> {...} or -- forall a. {...}? , hst_bndrs :: [(LHsTyVarBndr pass, InferredFlag)] -- Explicit, user-supplied 'forall a b c' , hst_body :: LHsType pass -- body type } }}} Bingo. We reflect, straightforwardly and directly in the abstract syntax:

The curly braces per binder InferredFlag
The arrow vs dot hs_fvf :: ForallVisFlag.

Of course this abstract syntax can represent a bogus type like forall {a} -> blah, but that's fine; we parse and reject it (say in the renamer) with a persipicuous message.

Easy!

@simonpj Having hst_bndrs :: [(LHsTyVarBndr pass, InferredFlag)] seems fine to me - I'll implement as such. Thanks for the suggestion.

Alec, how's it going? Can we help?

added Pnormal label

Currently, (with -XExplicitForAll and -XPartialTypeSignatures) a definition like

const' :: forall a . a -> _ -> a
const' x _ = x

and then typing :t +v const' in GHCi with :set -fprint-explicit-foralls results in const' :: forall a {_}. a -> _ -> a. Is this syntax supposed to be allowed once this ticket is implemented? Or would this be a remaining discrepancy between the output of :t and what types the user is allowed to type?

That output not only uses {...} for an inferred variable, it also names a variable _. There are no plans to allow type variables to be named _. Sadly, fixing this output is much harder than you might think, because GHC has no good fixed notion of what _ means. Problems like this inspired https://github.com/ghc-proposals/ghc-proposals/pull/194, which will allow us to clean up the mess.

I'd like to start implementing this

@harpocrates, any progress on this? In particular, is there an on-going MR? Thanks!

Once this is done, add a kind sigature for Typeable: #17569

As this issue has been quiet for a while, I have started implementing this.

mentioned in merge request !2465 (closed)

mentioned in issue #18023 (closed)

mentioned in commit b430e095

mentioned in commit 365c1f1f

mentioned in commit dc800bb4

mentioned in commit a9311cd5

The proposal is implemented and has been merged in master Closing this ticket.

closed

changed milestone to %9.0.1

Trac field	Value
Version
Type	Task
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	goldfire
Operating system
Architecture

Implement the "Explicit specificity in type variable binders" proposal

Child items 0

Activity