Serokell’s Work on GHC: Dependent Types, Part 2

Links
1
26 Likes
2

Thanks very much for the clear explanation, as well as, of course, the work on GHC itself.

3 Likes
3

Am I reading correctly that forall is now a term-level keyword (i.e. can’t be used as an identifier) even without the new RequiredTypeArguments extension specified? Why? Was it too difficult to adjust the lexer to make forall keyword only in the presence of the language extension?

1 Like
4

Am I reading correctly that forall is now a term-level keyword (i.e. can’t be used as an identifier) even without the new RequiredTypeArguments extension specified?

That is correct.

Was it too difficult to adjust the lexer to make forall keyword only in the presence of the language extension?

This precedent had been set earlier, when forall was made an unconditional keyword in types (GHC Proposal #193). You can’t name a type variable forall even if ExplicitForAll is disabled.

That is, f :: a -> a is valid but f :: forall -> forall is not. The reason is that it improves error messages if you forget to enable ExplicitForAll.

Previously, this was only affecting type variables (but not term variables). RequiredTypeArguments is a step towards unifying type and term syntax. If forall is a keyword, it’s got to be a keyword everywhere. So we have two viable options

  1. Make forall a keyword everywhere (types and terms) regardless of enabled extensions
  2. Make forall a keyword everywhere (types and terms) iff ExplicitForAll is enabled

The committee has made the judgement call to go with option (1).

6 Likes