1 Modern Scoped Type Variables ¶

This proposal updates the treatment of scoped type variables in GHC, tying together many existing proposals:

#126: Accepted, implemented proposal on accepting type arguments to constructor patterns, allowing constructions like f (Just @Int x) = x + 5 and g (Dynamic @a x) = show (typeOf (x :: a)).
#155: Accepted, not implemented proposal on accepting type arguments to lambdas, allowing constructions like \ @a (x :: a) -> x.
#238: Not yet accepted proposal that updates and extends #155 to include a reshuffling of extensions around scoped type variables, as well as describing clearer rules mediating between the old -XScopedTypeVariables behavior and the new proposed behavior.
#285: Accepted, not implemented proposal introducing -XNoImplicitForAll and -XNoPatternSignatureBinds, restricting where type variables may implicitly be brought into scope.
#291: Not yet accepted proposal that is an amendment to #126 to change the way type variables are brought into scope to be more like term variables, and less like pattern signatures.
#420: Not yet accepted proposal that is an amendment to #285, with a very tiny, technical tweak to a definition.

This proposal supersedes all of the proposals above, including the accepted ones. The goal of writing this is to provide a unified framework, so that we can design our language with cohesive treatment of scoped type variables, instead of simply an agglomeration of features.

1.1 Motivation ¶

With GHC’s powerful type-level programming features, we need powerful abilities to bring type variables into scope. The proposal defers to the individual proposals linked above for motivation for why we generally want these type-level features. Individual aspects of this unifying proposal are motivated near where they are introduced.

1.2 How to read this proposal ¶

This is a large proposal, with a number of moving parts. The essential reason all these moving parts are glued together in just one proposal is so that they can be unified by their desire to uphold the principles added to our principles document. Individual components of this proposal can be designed, debated, and implemented separately, yet are presented in one document as they are meant to dovetail together nicely.

As currently written, this proposal is not self-contained, in that motivation for some individual pieces was not copied from their source proposals. In all cases, when this proposal refers to others as inspiration, seeking more information there will likely be helpful.

If this proposal is accepted, it may be a good idea to incorporate that motivation, etc., right in this proposal here, to make it self-contained. I am happy to do this at the direction of the committee.

1.3 Extension shuffling ¶

Right now, -XScopedTypeVariables does a lot of heavy lifting. This proposal breaks up -XScopedTypeVariables into its components. This enables finer-grained control, and the ability for e.g. the a in f :: forall a. a -> a not to scope over the definition of f.

The new meaning of -XScopedTypeVariables is the same as the old one. The only backward-incompatible part of this is that, today, -XPatternSignatures is a deprecated synonym of -XScopedTypeVariables. Under this change, that would no longer be true.

This component of this proposal is taken from the accepted proposal #285, and not-yet-accepted proposals #238 and #420. The difference from #238 is that -XScopedForAlls has become in this proposal -XExtendedForAllScope. The difference from #285 is that -XPatternSignatureBinds is disabled, not enabled by default, which was proposed in both #238 and #420. (John Ericson is the author of #285 and #420, and views the latter as correcting an oversight in the former.) -XNoImplicitForAll is included from #285 unchanged.

1.3.1 Motivation for any extension shuffling ¶

The main goal of this extension shuffling is to introduce -XExtendedForAllScope as an extension separate from -XScopedTypeVariables. This separation is motivated by two reasons:

Some people [citation needed] dislike the behavior captured in -XExtendedForAllScope (where the a in f :: forall a. a -> a is in scope in f‘s definition). Separating out the extension allows us to avoid this behavior.
The behavior of -XExtendedForAllScope is at odds with the behavior of -XTypeAbstractions for binding type variables in lambda patterns; see this specification point. It thus seems necessary to separate out the problematic -XExtendedForAllScope from the other components of -XScopedTypeVariables.

Having separated out -XExtendedForAllScope, it seemed strange to have a -XRumpEndOfOldScopedTypeVariables extension, and so I’ve introduced separate -XMethodTypeVariables and -XPatternSignatures. The latter is further broken down to separate out -XPatternSignatureBinds, as a part of accepted proposal #285.

1.3.2 Motivation for `-XPatternSignatures`¶

This is taken from #119. “I” and “me” here is Joachim Breitner, aka @nomeata.

Originally, PatternSignatures was a an extension on its own, but at some point it started to imply ScopedTypeVariables and eventually was deprecated in favor of the latter. This has always bothered me and I often find myself in situations where I need to use a pattern signature without having any need for scoped type variables. This need has increased with more polymorphic functions in base (e.g. post FTP).

I too often thoughts “I should have raised this point when it was time, but it is too late now”. But maybe it is not too late… hence this proposal.

The concrete motivation is to be able to write something like this:

{-# LANGUAGE OverloadedStrings #-}
foo :: Monad m => m Int
foo = do
  list <- return ""
  return $ length list

Currently, this fails with (much shortened):

Test.hs:4:18: error:
    • Could not deduce (Data.String.IsString (t0 a0))
        arising from the literal '""'
Test.hs:5:12: error:
    • Could not deduce (Foldable t0) arising from a use of 'length'

Ah, the FTP strikes again. So to fix this, I have to specify list‘s type. In Haskell98 I can add a type signature to the use of list, but that is ugly: Types should be declared where stuff is brought into scope! So I want to write:

{-# LANGUAGE OverloadedStrings #-}
foo :: Monad m => m Int
foo = do
  list :: String <- return ""
  return $ length list

but I get:

Test.hs:4:3: error:
    Illegal type signature: 'String'
      Type signatures are only allowed in patterns with ScopedTypeVariables

Ok, that works, but why am I bothered with ScopedTypeVariables? Furthermore, ScopedTypeVariables is not conservative; it may actually break my program somewhere!

What I really want in this case is a pattern signature, and it would be nice if I could just state that PatternSignatures.

1.3.2.1 Motivation for not doing binding ¶

-XPatternSignatures as proposed here is more narrow than its prior incarnation circa GHC 6. This is because it just allows signatures using already-bound variables, and doesn’t include any implicit binding mechanism for variables in the signature that aren’t yet bound. (That instead is left as part of -XScopedTypeVariables.)

We here discuss the motivation for this decision.

1.3.2.1.1 Principles ¶

This is necessary in order to uphold the Lexical Scoping Principle, part (a).

1.3.2.1.2 Avoiding Redundancy ¶

A comment SPJ left in now-closed proposal #523 states the argument well:

Currently pattern signatures are funny: you can only tell whether (\(x::a) -> blah) brings a into scope if you know whether or not a is already in scope. Not a beautiful thing.

[…]

An alternative would be to abolish pattern signatures — or at least abolish the rule that allows a pattern signature to bring a variable into scope. _That rule was only present to allow us to give a name to existential type variables._ E.g.
data T = forall a. MkT [a] (a -> Int)

f :: T -> [Int]
f (MkT (xs :: [a]) f) = let mf :: [a] -> [Int]
                            mf = map f
                        in mf xs
Here the pattern signature on xs brings a into scope, so that it can be mentioned in the type signature for mf. In the past there was no other way to do this. But now we can say
f :: T -> [Int]
f (MkT @a xs f) = let mf :: [a] -> [Int]
                      mf = map f
                  in mf xs
So we could, if we chose, deprecate and ultimately abolish the ability for pattern signatures to bring a new type variable into scope. Instead of adding complexity to the language, let’s remove it.

It would be hard to change -XScopedTypeVariables, so we don’t propose that. But right now, and only right now, it is easy to adjust -XPatternSignatures before it is reintroduced. This is our best shot to steer people away from pattern signature binds and towards @ instead!

1.3.2.2 Unified Namespace ¶

#281 introduces -XRequiredTypeArguments which is almost backwards compatible, except for conflicting with implicit binding. -XRequiredTypeArguments effectively simulates a single namespace by having variable usages check the “other” namespace when an identifier is unbound in its “proper” namespace (e.g. in the type namespace when the identifier occurs within a type). For example,

x = Int
y = 1 :: x -- OK renaming, x is found in the term namespace.

type X = Int
y :: Type = X -- OK renaming, X is found in the type namespace

(There are errors after renaming in the above examples, but lets ignore them for now. The goal is to make those errors go away long term, so we should not rely on them giving us “syntax to steal”. More complicated examples will work completely with #281 without further generalizations that rely on the same cross-namespace variable lookup in both directions.)

This is an extension of the same method of namespace used for -XDataKinds, and is backwards-compatible for the same reason.

The issues arise with implicit binding (pattern signature bindings and implicit forall bindings alike). Consider this program:

t = Int
foo (x :: t) = 0

With -XScopedTypeVariables today, t is considered unbound, and so t is implicitly bound. But this breaks the single-namespace illusion — t would have been found in the other namespace, if it weren’t for the implicit binding. -XRequiredTypeArguments is thus forced to choose between being a conservative extension (allowing more programs, changing the meaning of no existing program) or faithfully simulating a unified single namespace; it chooses the latter at the expense of the former. It does so by changing the implicit binding rules to consult both namespaces first: t above is a use not a bind.

The goal of this proposal, `#448`_ is to move away away from -XScopedTypeVariables, and adopt designs that are compatible with -XRequiredTypeArguments without requiring it. -XPatternSignatures without implicit bindings is just that:

Adding implicit pattern bindings is a conservative extension
Adding just cross-namespace variable resolution is a conservative extension

It therefore serves as a “least common ancestor” of these other extensions. It is useful to materialize these points in the design space with language extensions: both to isolate the points of agreement from the points of controversy in the design space, and allow people to write less restricted code that they are nonetheless confident they can copy between between different modules with different versions of the language without issue.

1.3.2.2.1 Consistency ¶

This more narrow formulation of -XPatternSignatures matches -XKindSignatures. KindSignatures doesn’t allow implicit binds for a rather roundabout reason: implicit binds would imply implicit kind-level foralls, which would require -XPolyKinds:

ghci> :set -XKindSignatures
ghci> :set -XNoPolyKinds
ghci> data Foo (a :: b)

<interactive>:3:16: error:
    Unexpected kind variable ‘b’
    Perhaps you intended to use PolyKinds
    In the data type declaration for ‘Foo’

We can reinterpret this as a simple syntactic rule: -XKindSignatures alone doesn’t do implicit binding:

ghci> :set -XKindSignatures
ghci> data Foo (a :: b)

<interactive>:3:16: error: Not in scope: type variable ‘b’

The error message is completely different, but the effect with respect to merely whether the program was rejected is the same. (Choosing a way to disable the implicit binding part of -XPolyKinds is left as future work — possibly a future amendment to this proposal.)

Now, both extensions (-XPatternSignatures and -XKindSignatures) just allow, respectively, term-level and type-level signatures, with no other functionality like implicit binding mechanisms also thrown in.

1.3.2.2.2 Conservativism for standardization ¶

With both of these extensions being very minimal, I think they would be easy uncontroversial candidates for a new language report. Conversely, all implicit binding constructs are very fraught with a complicated mix of upsides and downsides, and we should only standardize them with great care.

1.3.3 Motivation for `-XNoImplicitForAll`¶

This is taken directly from #285, updated to refer to warnings instead of language extensions. The “I” here is John Ericson.

There are two independent motivations: education and consistency with a unified namespace.

1.3.3.1 Education ¶

Some people think that implicit binding is bad for people learning Haskell. All other variables are explicitly bound, and the inconsistency means more to learn. Also, implicit syntax in general allows the beginner to not realize what they are doing. What are tedious tasks for the expert may be helpful learning steps to them.

Further, the most beginnning students may be taught with both -XNoImplicitForAll and -XNoExplicitForAll. This means it’s impossible to write forall types by any means. Combine with -Wmissing-signatures and -Wmissing-local-signatures, so inferred polymorphic types of bindings are also prohibited, and a monomorphic custom prelude, and forall types are all but expunged entirely.

I don’t wish to argue whether these choices do or don’t actually help learning, but just state that some people have opinions that they do and there is no technical reason GHC cannot accommodate them.

1.3.3.2 Unified Namespace ¶

See the discussion above for -XPatternSignatures. The same exact principles apply. In this case, problemantic programs with implicit binding look something like this:

t = Int
x :: t -- sugar for 'forall t. t', not 't ~ Int'
x = 0

-XRequiredTypeArguments again chooses to break with -XScopedTypeVariables (and in particular -XImplicitForAll) to make t above refer to Int and not a freshly-quantified type variable.

1.3.4 Motivation for `-XPatternSignatureBinds`¶

Given that -XPatternSignatures does not include pattern signature binds (as argued above), we have a choice:

Have -XScopedTypeVariables directly allow pattern signature binds in addition to implying other proposals
Introduce -XPatternSignatureBinds so that -XScopedTypeVariables is just an alias for other extensions, and does nothing on its own separate from those other extensions.

In discussion, it seems the latter is preferred.

1.3.5 Proposed Change Specification ¶

Points below up to and including the new (backward-compatible) definition of -XScopedTypeVariables come from not-yet-accepted proposal #238. The point about -XImplicitForAll and -XPatternSignatureBinds is a restatement of (part of) accepted proposal #285, except for the fact that -XPatternSignatureBinds is off by default (as proposed in not-yet-accepted proposals #238 and #420, the latter of which modified #285).

Re-purpose deprecated extension -XPatternSignatures. With -XPatternSignatures, we allow type signatures in patterns. These signatures can mention in-scope type variables as variable occurrences, but can not bind type variables without the (separate) -XPatternSignatureBinds extension.

The current -XPatternSignatures is just a synonym for -XScopedTypeVariables. This change is thus not backward-compatible, but given that the existing extension is deprecated, I think this change is acceptable.
Introduce -XPatternSignatureBinds. With -XPatternSignatureBinds, any out-of-scope type variables written in a pattern signature would be bound there and would remain in scope over the same region of code that term-level variables introduced in a pattern scope over. This extension is off by default. (This extension is a part of accepted, unimplemented proposal #285.)
Introduce -XMethodTypeVariables. With -XMethodTypeVariables, type variables introduced in an instance head would scope over the bodies of method implementations. Additionally, type variables introduced in a class head would scope over the bodies of method defaults.
Introduce -XExtendedForAllScope. With -XExtendedForAllScope, any type variables mentioned in an explicit forall scopes over an expression. This applies to the following constructs:
- Function bindings
- Pattern synonym bindings (including in any where clause)
- Expression type signatures
Separating out -XExtendedForAllScope gets us closer to the Contiguous Scoping Principle.
The extension -XScopedTypeVariables would imply all of the above extensions: -XPatternSignatures, -XPatternSignatureBinds, -XMethodTypeVariables, and -XExtendedForAllScope; this way, -XScopedTypeVariables does not change from its current meaning.
Introduce -XImplicitForAll, on by default. With -XImplicitForAll, an out-of-scope type variable mentioned in various constructs (listed below) is implicitly brought into scope over the construct. With -XNoImplicitForAll, this implicit scoping does not happen, and the use of the variable is an error.

Constructs affected:
1. Type signatures for variable declarations, methods, and foreign imports & exports. Example: let f :: a -> a; f = ... in ... becomes let f :: forall a. a -> a; f = ... in ....
2. Kind signatures. Example: type T :: k -> Type becomes type T :: forall k. k -> Type.
3. GADT constructor declarations. Example: MkG :: a -> Maybe b -> G (Either Int b) becomes MkG :: forall a b. a -> Maybe b -> G (Either Int b).
4. Pattern synonym signatures. Example: pattern P :: a -> Maybe a becomes pattern P :: forall a. a -> Maybe a. Implicit quantification in pattern synonyms always produces universal variables, never existential ones.
5. Type annotations in expressions and SPECIALISE pragmas. Example: Right True :: Either a Bool becomes Right True :: forall a. Either a Bool.
6. Types in a deriving clause. Example: data T deriving (C a) becomes data T deriving (forall a. C a).
7. Instance heads, including standalone-deriving instances. Example: instance Show a => Show (Maybe a) becomes instance forall a. Show a => Show (Maybe a).
8. Type and data family instances, as well as closed type family equations. Example: type instance F (Maybe a) = Int becomes type instance forall a. F (Maybe a) = Int.
9. RULES pragmas. Example: {-# RULES "name" forall (x :: Maybe a). foo x = 5 #-} becomes {-# RULES "name" forall a. forall (x :: Maybe a). foo x = 5 #-}. (The double-forall syntax separates type variables like a from term variables like x.)
This extension is part of accepted, unimplemented proposal #285; the only change is including RULES pragmas, which @Ericson2314 simply forgot to include in #285 (his own admission).

Being able to turn off this extension is necessary to uphold the Explicit Binding Principle.

1.3.6 Effects ¶

We could now advocate for avoiding -XExtendedForAllScope, in favor of -XTypeAbstractions (introduced below). The other parts of the old -XScopedTypeVariables (namely, -XPatternSignatures and -XMethodTypeVariables) could be considered for inclusion in a future language standard.

1.3.7 Alternatives ¶

Previous versions of this proposal had a warning -Wpattern-signature-binds, indended to be used with -Werror=… as an alternative to -XNoPatternSignatureBinds. The argument was that we don’t need a proliferation of -XNo… extensions for people to disable parts of the language they don’t like when warnings, or even an external-to-GHC linter will not do. I think this argument makes sense when there is a single “all extensions on” language we can agree on such everyone’s preference is just a sublanguage of it.

The problem is that we do not have such an “all extensions on” consensus here. As discussed earlier in the motivation section, we have multiple notions of implicit binding based on whether the user wants to program with a single unified namespace or multiple overlapping namespaces. That is a fundamental unavoidable conflict between implicit binding and the choice of namespaces, and there is no way around it. Given this “fork” in the design space, a separate language extension makes a lot more sense: we’re not “just” disabling functionality some people don’t like, we are formalizing the “last point of agreement” before design preferences split in multiple irreconcilable directions.

1.4 Type arguments in constructor patterns ¶

This is an update to accepted, implemented proposal #126, incorporating the logic of not-yet-accepted amendment #291.

The original proposal #126 is indeed implemented and released, but the implementation is not faithful to the specification around type variables that are already in scope. The original proposal says that, if a is already in scope, then f (Just @a x) = ... is an occurrence of the in-scope a. By contrast, the implementation errors in this case.

Not-yet-accepted amendment #291 says that type variables scope just like term variables: they can be shadowed. Accordingly, f (Just @a x) = ... would always, unconditionally bind a new type variable a, possibly shadowing any in-scope type variable a. This design supports the Visibility Orthogonality Principle, which states that the presence of an @ should affect only whether a thing is visible or not, not other characteristics (like its shadowing and scoping behavior). Additionally, this choice edges us closer to the `Local Lexical Scoping Principle`_, because we no longer have to check whether a is in scope before identifying the a in f (Just @a x) = ... is a binding site or an occurrence.

The other change in this restatement is the use of new extension -XTypeAbstractions instead of the current status of piggy-backing on the combination of -XTypeApplications and -XScopedTypeVariables (both need to be enabled today). This proposal suggests that initially -XScopedTypeVariables and -XScopedTypeVariables should jointly enable type applications in constructor patterns; but that this combination doing so should be deprecated, and at some later point removed. We have conflicting principles at play:

New experimental functionality should not be gated under older established extensions
Breaking changes under established extensions — even if it only affects experimental functionality that should have not been there in the first place — should be avoided.

Given these too things, a small deprecation cycle / migration path to -XTypeAbstractions seems the best we can do.

1.4.1 Motivation ¶

This is taken directly from #126.

TypeApplications are a convenient and natural way to specifying types of polymorphic functions. Consider:

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

With TypeApplications, I can replace the somewhat clumsy MkFoo (x :: ty) with MkFoo @ty x. Seen this way, explicit type applications are merely an alternative syntax for type signatures.

At the moment, this only works in terms, but not in patterns: We can use type signatures in patterns (if PatternSignatures or ScopedTypeVariables are enabled), but not type applications. Given the strong relation between these syntactic forms, this is odd – why can I write:

foo (MkFoo (x :: ty)) = …

but not:

foo (MkFoo @ty x) = …

This proposal fills this gap: It allows type applications in patterns, and specifies them to behave “just like type signatures”.

The intention of the following specification is that the following holds: For a constructor with type like C :: forall a. a -> … the meaning of C @ty x should coincide with the existing form C (x :: ty).

1.4.2 Proposed Change Specification ¶

Introduce a new extension -XTypeAbstractions (This extension is further extended in the next part of this proposal.)

When -XTypeAbstractions is enabled, allow type application syntax in constructor patterns.

Concretely, the grammar goes from

pat → gcon apat1 … apatk
    …

pat → gcon tyapp_or_pat1 … tyapp_or_patk
    …

tyapp_or_pat → '@' atype    -- '@' is in prefix position
             → apat

For backward compatiblity, also accept type application syntax in constructor patterns if both -XScopedTypeVariables and -XTypeApplications are enabled, but -XTypeAbstractions is not. In that case, emit a warning, stating that type applications in constructor patterns should be enabled with -XTypeAbstractions, and that the temporary expedient of enabling it by the combination of -XScopedTypeVariables and -XTypeApplications will be removed.

After 2 releases remove clause (b); -XTypeAbstractions will be the only way to enable this feature.
Type applications in constructor patterns do not affect whether the pattern-match is successful.
Type applications in constructor patterns must correspond to forall … . quantifications in the declared constructor or pattern synonym type. (Right now, pattern synonyms require all such quantifications to occur before any term arguments, but accepted proposal #402 allows these quantifications to occur in any order in data constructors.)
In accordance with the Visibility Orthogonality Principle, the rules that determine whether a variable occurrence is a binding site or a use site are not affected by the presence of a @. At the time of writing, the rules for patterns and pattern signatures are as follows:
- Outside pattern signatures, variable occurrences are considered binding sites, shadowing any other in-scope variables. It is an error to bring the same type variable into scope in two (or more) places within the same match group.
- Inside pattern signatures (i.e. on the right-hand side of pat :: sig), occurrences of in-scope type variables are usages, whereas occurrences of out-of-scope type variables create implicit bindings. It is allowed to mention the same out-of-scope variable more than once.
Generalize these rules to apply not only to pattern signatures but also to kind signatures in type applications in constructor patterns (and to kind signatures in type variable patterns defined in the “Type arguments in lambda patterns” section).
Typing follows the rules in Type Variables in Patterns. In particular, see Figure 7, which we modify here in two ways:
1. Ignore the isInternalTypeVar premise, which was done away with by accepted proposal #128.
2. Change the cs = ftv(τ's) \ dom(Γ) premise to be cs = ftv(τ's) and cs # dom(Γ). That is, instead of making the new type variables cs be only those that are not already in scope, require all the type variables to be fresh (shadowing is possible, but left implicit here).
A wildcard _ as a type argument says simply to skip that argument; it does not trigger any behavior associated with partial type signatures. In particular, -XPartialTypeSignatures is not necessary, and no diagnostic is produced.

1.4.3 Examples ¶

There are examples of pattern signatures using type variables which are already in scope:

foo :: forall b. Maybe b -> ()
foo @a (_ :: Maybe a) = ()

bar :: forall b. Maybe b -> ()
bar (Just @a (_ :: a)) = ()

baz :: forall b. b ~ () -> ()
baz @b () = ()
  where
    () :: b = ()

These examples are all accepted with -XPatternSignatures.

This is an example of a pattern signture binding a type variable:

id (x :: a) = x :: a

This example is allowed with -XScopedTypeVariables as today, but disallowed with just -XPatternSignatures.

Here is an example (taken from #15050):

type family F a where
  F Bool = Int
data T a where
  MkT :: forall b a. b ~ F a => b -> T a

foo :: T Bool -> ()
foo (MkT @Int _) = ()

This should type-check, because the following code does:

foo :: T Bool -> ()
foo (MkT (_ :: Int)) = ()

Note that the data constructor expects up-to two type arguments (forall b a.…), but we are passing only one type argument, which then corresponds to the first type argument of of the data constructor.

A more complex example is this (also inspired by #15050):

data T a where
  MkT1 :: forall a.              T a
  MkT2 :: forall a.              T (a,a)
  MkT3 :: forall a b.            T a
  MkT4 :: forall a b. b ~ Int => T a
  MkT5 :: forall a b c. b ~ c => T a

foo :: T (Int, Int) -> ()
foo (MkT1 @(Int,Int))  = ()
foo (MkT2 @x)          = (() :: x ~ Int => ())
foo (MkT3 @_ @x)       = (() :: x ~ x => ())
foo (MkT4 @_ @x)       = (() :: x ~ Int => ())
foo (MkT4 @_ @Int)     = ()
foo (MkT5 @_ @x @x)    = (() :: x ~ x => ())    -- not accepted

All (save the last) of these equations type-check (just like they would if added value arguments of type a, b,… to the constructors and turned the type applications into type signatures). The last is rejected because it tries to bind x twice in the same pattern, in just the same way as a pattern binding the same term variable twice is rejected.

Note that the @_ are not treated like partial type signatures: they do not create any diagnostics; they are merely placeholders for type variables not bound.

Note that it is usually a type error to supply a non-tyvar type, or an in-scope tyvar, in an existential position (e.g. MkT3 @_ @Int is wrong), unless the data constructor has constraints that equate the existential type variable to some type (as in the equations involving MkT4 and MkT5 above).

{-# LANGUAGE ExtendedForAllScope #-}
data Ex = forall a. MkEx a
f2 :: forall b. b -> Ex -> Int
f2 y (MkEx @b z) = ...

This is rejected under #126, as it appears to insist that the existential type packed in MkEx is the same as the type argument passed to f2. On the other hand, this is accepted by the current proposal, allowing the existential b to shadow the b brought into scope by the forall.

This shadowing behavior mimics what happens with term variables in patterns.

f :: Maybe Int -> Int
f (Nothing @a) = (4 :: a)
f (Just @a _)  = (5 :: a)

This is accepted. The type variable a is bound to Int, by pattern-matching.

Here is an example of pattern signatures within a type abstraction in a pattern:

{-# LANGUAGE ScopedTypeVariables #-} -- for pattern signature bindings
data Proxy a = P
g2 :: Proxy (Nothing @(a, a)) -> ()
g2 (P @(Nothing :: Maybe (t, t))) = ()

Note multiple occurrences of t in the pattern. Normally, we would disallow multiple bindings of a single variable:

f1 (P x) (P x) = x               -- Rejected (multiple bindings of ‘x’)
f2 (P @a x) (P @a y) = x         -- Rejected (multiple bindings of ‘a’)

Pattern and kind signatures, however, are not subject to this restriction, since variable occurrences in pattern signatures are considered usages (not bindings):

{-# LANGUAGE ScopedTypeVariables #-} -- for pattern signature bindings

g1 (P x :: Proxy (a,a)) = x               -- Accepted (multiple occurrences of ‘a’ notwithstanding)

g2 :: Proxy (Nothing @(a, a)) -> ()
g2 (P @(Nothing :: Maybe (t, t))) = ()    -- Accepted (multiple occurrences of ‘t’ notwithstanding)

1.4.4 Effects ¶

The ability to bind existential variables via a construct such as this is necessary to support the Explicit Variable Principle.
The previous proposal #126 followed the paper more closely, bringing into scope only those variables that are not already in scope. However, given that this behavior is triggered only by a @, doing this is in violation of the Visibility Orthogonality Principle. This newer version instead labels all variables as binding sites.
Having type variables have the same behavior as term variables with respect to shadowing (and repeated binding) upholds the Visibility Orthogonality Principle. In addition, the fact that type variables are unconditionally brought into scope upholds the Lexical Scoping Principle, part (a).
It may be useful to write a variable occurrence to instantiate a universal argument. This proposal prevents this possibility. We expect a future proposal to remedy this problem, with either a modifier or some symbol. For example, perhaps we would say e.g. f (Just @(*a) x) = ... to denote an occurrence of already-in-scope type variable a.
Backward-compatibility with the current implementation, which merely requires both -XScopedTypeVariables and -XTypeApplications to be in effect and not any extension dedicated to this feature, is preserved. But whenever the old way of enabling this feature is used, a deprecation warning will be issued.
After 2 releases of deprecation with the warning, the above implication is removed. That cleans up new experimental functionality from leaking under established extensions. This is a breaking change, but with the advanced notice given via the warning, the costs are reduced to the point that the benefits are deemed to outweigh them.

1.5 Type arguments in lambda patterns ¶

This is a restatement of accepted, unimplemented proposal #155, as amended by not-yet-accepted #238. It introduces the ability to bind type variables by a lambda, controlled by the -XTypeAbstractions extension.

1.5.1 Motivation ¶

This is adapted from #238.

There are several motivating factors for this addition:

There are cases where a Proxy is necessary in order for a higher-rank function argument to access a type variable, such as:
```
type family F a

higherRankF :: (forall a. F a -> F a) -> ...

usage = higherRankF (\ (x :: F a) -> ...)
```
The (x :: F a) pattern signature does not work, because F is not injective. There is no way to be sure that the a in usage is meant to match the a in higherRankF. Currently, there is simply no way for usage to get access to the type variable written in the signature for higherRankF. This code would have to be rewritten to use Proxy. Under this proposal, however, usage could be simply
```
usage = higherRankF (\ @a x -> ...)
```
Ah. That’s better.
With #126, we can bind type variables in constructor patterns, allowing us to easily capture existentials. The only other place a type variable can enter scope is in a function definition, and so it’s only logical to extend #126 to do so. Furthermore, doing so is necessary to uphold the Explicit Variable Principle.
-XExtendedForAllScope's mechanism for binding type variables using a forall in a signature has never sat well with some. (I’m in the some, but I’m not the only one.) A type signature can appear arbitrarily far away from a function definition, and (to me) the use of forall to induce scoping over the function definition is far from intuitive. Using this new syntax, all the action happens in the function definition. This allows for the possibility of usefully disabling -XExtendedForAllScope while still binding type variables, helping to support the Contiguous Scoping Principle.
See crowd-sourced example here.

1.5.2 Proposed Change Specification ¶

With -XTypeAbstractions, introduce a new form of pattern (cf. The Haskell 2010 Report):
```
apat → … | '@' tyvar | '@' '(' tyvar '::' kind ')' | '@' '_'   -- '@' is a prefix occurrence
```
Conveniently, apats are used both in function left-hand sides and in lambda-expressions, so this change covers both use-cases.

(Note that this does not subsume the new grammar for constructor patterns, which allow types, not just variables.)
In accordance with the Visibility Orthogonality Principle, the rules that determine whether a variable occurrence is a binding site or a use site are not affected by the presence of a @. That is, name resolution in kind signatures in type variable patterns follows the rules for pattern signatures. (The rules for pattern signatures are given in the “Type arguments in constructor patterns” section).
A type variable pattern is not allowed in the following contexts:
1. To the right of an as-pattern
2. As the top node in a lazy (~) pattern
3. As the top node in a lpat (that is, to the left of an infix constructor, directly inside a parenthesis, as a component of a tuple, as a component of a list, or directly after an = in a record pattern)
Typing rules for the new construct are as in a recent paper: see ETm-InfTyAbs, ETm-CheckTyAbs, Pat-InfTyVar, and Pat-CheckTyVar, all in Figure 7. While the typeset versions remain the official typing rules, I will summarise the different rules below.

Background. GHC implements bidirectional type-checking, where we sometimes know what type to expect an expression to have. When we know such a type (for example, because we have a type signature, or an expression is an argument to a function with a known type), we say we are in checking mode. When we do not know such a type (for example, when we are inferring the type of a let-binding or the type of a function applied to arguments), we say we are in synthesis mode. The Practical Type Inference paper gives a nice, Haskell-oriented introduction.
1. In synthesis mode, when examining \ @a -> expr, we simply put a in scope as a fresh skolem variable (that is, not equal to any other type) and then check expr. (Presumably, expr uses a in a type signature.) When we infer that expr has type ty, the expression \ @a -> expr has type forall a. ty. Example: \ @a (x :: a) -> x infers the type forall a. a -> a. (For this example, we note that \ @a (x :: a) -> x is a short-hand for \ @a -> \ (x :: a) -> x.)
2. In checking mode, when examining \ @a -> expr against type ty, we require that ty has the shape forall a. ty', where a is a specified variable (possibly after skolemising any inferred variables in ty), renaming the bound variable as necessary to match the name used in the expression. We then check expr against type ty'.
3. In synthesis mode, when examining a function argument @a to a function f, we bring a into scope as a fresh skolem variable and check the remainder of the arguments and the right-hand side. In the type of f, we include a forall a. in the spot corresponding to the type variable argument.
  
  If there are multiple equations, each equation is required to bind type variables in the same locations. (If this is burdensome, write a type signature.) (We could probably do better, by inferring the maximum count of bound type variables between each required argument and then treating each set of bound type variables as a prefix against this maximum, but there is little incentive. Just write a type signature!)
4. In checking mode, when examining a function argument @a to a function f with type signature ty, we require the corresponding spot in the type signature to have a forall a (possibly renaming the bound variable). The type variable a is then brought into scope and we continue checking arguments and the right-hand side.
  
  Multiple equations can bind type variables in different places, as we have a type signature to guide us. Exception: The number of type variables bound after all term patterns must be the same for all equations; discussion below.
Typing rules for pattern synonym bindings are complicated, as usual.
1. A visible type abstraction in a pattern synonym binding that lacks a type signature is rejected. (While we could, at some cost, work out what should happen here, please just use a type signature.)
2. (Background information; no new specification here.) Pattern synonym type signatures have a restricted form that looks like this:
```
pattern P :: forall universal_tvs.   required_context =>
             forall existential_tvs. provided_context =>
             arg1 -> arg2 -> ... ->
             result
```
  The GHC manual has the details for how parts of this signature can be left out; I will not repeat these rules here. The key observation is that all quantified type variables occur before any required term-level arguments.
  
  Furthermore, pattern synonym bindings may be specified in two parts, for explicit bidirectional pattern synonyms:
```
pattern P <- pat
  where P = expr
```
  Call the top line the pattern synonym pattern binding, while the second line is the pattern synonym expression binding.
  
  In an implicitly bidirection pattern synonym binding, the pattern synonym pattern binding and pattern synonym expression binding are written with one bit of syntax. For the purposes of this proposal, though, we consider type-checking this bit of syntax twice, once as a pattern synonym pattern binding, and once as a pattern synonym expression binding.
3. With -XTypeAbstractions, a pattern synonym pattern binding may include any number of type abstractions (such as @a or @_) directly after the pattern synonym name. (Such a binding must be written in prefix notation, not infix.) These bindings correspond to a prefix of the specified universal type variables in the pattern synonym’s type. It is an error to write more type abstractions than there are specified universal variables.
  
  Each type abstraction binds a local name to the corresponding universal type variable. These names are available in the right-hand side (after the <- or =).
  
  (Existentials are excluded here because an existential type variable is bound by the pattern in the right-hand side. There appears to be no motivation for being able to name these on the left.)
  
  The rules for the usage of such variables on the right-hand side are unchanged from the way scoped type variables work in pattern synonyms today.
4. With -XTypeAbstractions, a pattern synonym expression binding may include any number of type abstractions (such as @a or @_) directly after the pattern synonym name. (Such a binding must be written in prefix notation, not infix.) These correspond to a prefix of the concatentation of the specified universal and specified existential type variables written in the pattern synonym type signature. It is an error to write more type abstractions than there are specified universal and specified existential type variables.
  
  Each type abstraction binds a local name to the corresponding universal or existential type variable. These names are available in the right-hand side (after the =).
  
  (Existentials are included here because a pattern synonym used as an expression takes existentials as arguments from call sites, and it is sensible to bind these on the left.)
  
  The rules for the usage of such variables on the right-hand side are just as they exist for ordinary function bindings.
-XTypeAbstractions and -XExtendedForAllScope have a fraught relationship, as both are trying to accomplish the same goal via different means. Here are the rules keeping this sibling rivalry at bay:
1. -XExtendedForAllScope does not apply in expression type signatures. Instead, if users want a type variable brought into scope, they are encouraged to use -XTypeAbstractions. (It would not be hard to introduce a helpful error message instructing users to do this.)
2. If -XExtendedForAllScope is enabled, in an equation for a function definition for a function f (and similar for pattern synonym pattern bindings and pattern synonym expression bindings):
  - If f is written with no arguments or its first argument is not a type argument (that is, the next token after f is not a prefix @), then -XExtendedForAllScope is in effect and brings type variables into scope.
  - Otherwise, if f's first argument is a type argument, then -XExtendedForAllScope has no effect. No additional type variables are brought into scope.

1.5.3 Examples of new behavior of scoped type variables ¶

f :: forall a. a -> a
f @b x = (x :: a)   -- rejected, because -XExtendedForAllScope is disabled here

g :: forall a. a -> a
g @a x = (x :: a)   -- accepted with -XTypeAbstractions

h = ((\x -> (x :: a)) :: forall a. a -> a)
  -- accepted with previous -XScopedTypeVariables, but rejected
  -- now

i = ((\ @a x -> (x :: a)) :: forall a. a -> a)
  -- accepted with -XTypeAbstractions

Note that turning off -XExtendedForAllScope with -XTypeAbstractions is necessary if we think about where type variables are brought into scope. Are they brought into scope by the forall? Or by the @a? It can’t be both, as there is no sensible desugaring into System F. Specifically, if we have expr :: forall a. ty, that gets desugared into /\ a -> expr. If we have (\ @a -> expr) :: forall b. ty, what does it get desugared into? It would have to be /\ b -> /\ a -> expr, but then b and a are different.

Here might be another way of thinking about it. Suppose we’re checking expr against the pushed-down (known) type forall a. ty. If we bring a into scope, what type do we check expr against? Is it forall a. ty again? That’s very awkward if a is already in scope. If we check expr against ty and expr looks like \ @b -> expr', then we check \ @b -> expr' against ty – not against forall a. ty.

1.5.4 Further examples ¶

Here are two real-world examples of how this will help, courtesy of @int-index:

It would be useful to eliminate Proxy in this style of proof:

class WithSpine xs where
  onSpine ::
    forall r.
    Proxy xs ->
    ((xs ~ '[]) => r) ->
    (forall y ys.
      (xs ~ (y : ys)) =>
      WithSpine ys =>
      Proxy y ->
      Proxy ys ->
      r) ->
    r

Code taken from here.

Compare:

@-style: withSpine @xs (onNil ...) (\ @y @ys -> onCons ...)
Proxy-style: withSpine (Proxy :: Proxy xs) (onNil ...) (\(Proxy :: Proxy y) (Proxy :: Proxy ys) -> onCons ...)

From reflection:

reify :: forall a r. a -> (forall (s :: *). Reifies s a => Proxy s -> r) -> r

Compare:

@-style: reify (\ @s -> ...)
Proxy-style: reify (\(Proxy :: Proxy s) -> ...)

1.5.5 Examples of varying type variables among equations ¶

f1 @a (x :: a) = x    -- accepted

f2 @a True  x (y :: a) = x
f2 @_ False x y        = y   -- accepted

f3 @a True  x (y :: a) = x
f3    False x y        = y   -- rejected: too confusing to have different type variable bindings

f4 :: Bool -> a -> a -> a
f4 @a True  x (y :: a) = x
f4    False x y        = y   -- accepted: the type signature allows us to do this

f5 :: Bool -> forall a. a -> a -> a
f5 True @a x (y :: a) = x
f5 False   x y        = y    -- accepted

f6 :: Bool -> forall a. a -> a -> a
f6 True  @a = const @a @a
f6 False @_ = flip const     -- accepted: the type variables after term variables line up

f7 :: Bool -> forall a. a -> a -> a
f7 True  @a = const @a @a
f7 False    = flip const     -- rejected: variable tail of type variables

1.5.6 Effects ¶

An astute reader will note that I put spaces after all my lambdas. That is because \@ is a valid name for a user-defined operator. This proposal does not change that. If you want to bind a type variable in a lambda, you must separate the \ from the @.
This proposal makes abstracting over type variables the dual of applying types with visible type application.
Accepted proposal #99 introduces the possibility of user-written specificity annotations (forall {k} ...). An inferred variable, including one written by the programmer using this new notation, is not available for use with any form of visible type application, including the one proposed here. If you have a function f :: forall {k} (a :: k). ..., you will have to rely on the behavior of -XExtendedForAllScope to bring k into scope in f's definition, or you will have to use a pattern signature. This is regrettable but seems an inevitable consequence of the {k} notation.
This delivers the Explicit Variable Principle, meaning we can rid of Proxy.
The last set of examples above show how we deal with functions with multiple equations with varying type variable bindings.

No variation is allowed when there is no type signature, as doing so seems challenging (though possible), and we can just encourage a type signature.

With a type signature, variation is allowed (example f4, with one exception: the tail of arguments must be consistent. The reason for this restriction can be understood in thinking about f7: in the right-hand side of the second equation, is the expected type forall a. a -> a -> a or a -> a -> a, with a already bound? This choice matters: perhaps the right-hand side is \ @a -> flip (const @a @a). Or, if we have a type like Bool -> forall a b. ..., are both a and b bound to the left of the =? We could, for example, look at all equations and bind a number of variables equal to the maximum number of type variables across all equations. But re-consider f7 again: if we just wrote the second equation without the first, that would have a different meaning than writing the equation along with the first. That is, we might imagine this being accepted:
```
f7' :: Bool -> forall a. a -> a -> a
f7' False = \ @a -> flip (const @a @a)
```
but this being rejected as ill-typed:
```
f7'' :: Bool -> forall a. a -> a -> a
f7'' False   = \ @a -> flip (const @a @a)
f7'' True @a = const @a @a
```
This is strange, where the addition of a new equation violates the typing of a previous one (that was otherwise fine). To avoid this strangeness, we simply forbid varying the number of bound variables in the tail.

Note that we do not want to forbid binding variables in the tail generally, because someone might want
```
myId :: forall a. a -> a
myId @a = id @a
```
which binds a variable in the tail. Happily, definitions like this will have only one equation.
(technical) The Visible Type Applications (VTA) paper defines the behavior about what to do when checking against a polytype: it says to deeply skolemize. However, eager deep skolemization will spell trouble for this extension, as we need the lambdas to see the foralls. The end of the Section 6.1 in the extended VTA paper discusses why we do eager deep skolemization: essentially, the alternative would be to do type generalization at inflection points between checking and inference mode, right before doing the subsumption check. Type generalization is hard in GHC, though, and so the paper avoided it. In order to implement this proposal, we’ll have to work out how to do this.

1.5.7 Costs and Drawbacks ¶

This part of the proposal is not backward-compatible with today’s -XScopedTypeVariables, because it rejects expressions like
```
((\x -> (x :: a)) :: forall a. a -> a)
```
which are accepted today. No migration period is proposed, because it is very hard to imagine how -XTypeAbstractions and -XExtendedForAllScope should co-exist peacefully here. Instead, we can issue a specific error message telling users how to migrate their code in this case.

My hope is that constructs such as this one are rare and would not impact many users.

If necessary, we could imagine taking the expression expr :: forall ... . ty and looking proactively to see whether expr ever uses a type variable pattern from this proposal. If not, -XExtendedForAllScope could trigger (and we issue a warning with -Wcompat). But, if a type argument appears anywhere in expr, then -XExtendedForAllScope is disabled. This would be backward-compatible, but unfortunately non-local and annoying. I prefer just to skip this migration step.

1.5.8 Alternatives ¶

We could add the following specification item if we like:

Specification

If -XTypeAbstractions is in effect, then a function binding may use @(..) on its left-hand side. Here is the BNF (cf. the Haskell 2010 Report, Section 4.4.3), recalling that braces mean “0 or more”:
```
funlhs  →  var apat { apat }
        |  pat varop pat
        |  '(' funlhs ')' apat { apat }
        |  funlhs '@' '(' '..' ')'
```
The last line is new, and we assume the @ is in prefix form. This construct is available only when the function being defined has a type signature. The new construct brings into scope all type variables brought into scope at that point in the signature. Note that implicitly quantified type variables are brought into scope at the top of a signature, and so
```
f :: a -> b -> a
f @(..) = -- RHS
```
would have a and b in scope in the RHS.

The @(..) construct works for both specified and inferred variables, and is additionally available in pattern synonym pattern bindings (where it brings into scope only universals) and pattern synonym expression bindings (where it brings into scope both universals and existentials). (In an implicitly bidirectional pattern synonym, the @(..) brings into scope only universals.)

Discussion

This new notation seems like a convenient middle ground, allowing for an easy transition from the old-style -XScopedTypeVariables to the newer -XTypeAbstractions. It brings the inferred variables (from #99) into scope, quite conveniently. This new notation also allows type variables to be brought into scope without the forall keyword in the type, in case the user does not want to trigger forall-or-nothing behavior.

Note that this notation is forward compatible with visible dependent quantification in terms (#281):
```
f :: foreach (count :: Int) (label :: String) (is_paid_for :: Bool) -> Invoice
f (..) = -- here, count, label, and is_pair_for are all in scope
```
This style allows for more perspicuous types while avoiding redundancy. The particular example here uses foreach to denote arguments that are available at runtime, but nothing about foreach is required to make this all work (as far as scoping is concerned).

Accepting the @(..) syntax does not entail accepting this new, separate (..) syntax, though it is good to know that the idea is forward compatible.

A @(..) argument counts as a type argument when asking whether -XExtendedForAllScope affects a function equation.

The new @(..) notation does not work with expression type signatures, lambda-expressions, or anywhere other than a function binding with a type signature. This is because doing so would require propagating type information into scoping, which is problematic.

Some have argued on GitHub that it may be best to hold off the @(..) until we gain more experience here: adding new features is easier than removing them. While I agree that this could be done, the @(..) construct makes for a very easy migration from today’s -XScopedTypeVariables and is thus tempting to be around from the start. I don’t feel strongly but would personally vote for inclusion.
We could simply make -XExtendedForAllScope and -XTypeAbstractions incompatible. If the user specifies both, reject the program.

I find this approach less convenient, as it prevents an easy migration from the status quo (with -XScopedTypeVariables enabled often, including in -XGHC2021) to a future relying more on -XTypeAbstractions. The approach described in this proposal means that enabling -XTypeAbstractions affects nothing about -XExtendedForAllScope, until a user tries to actually use a type abstraction. That’s a nice property.

1.6 Effects and Interactions ¶

The effects of this proposal are written out in the individual sections. Here, I summarize the effects on the principles.

We get closer to the Lexical Scoping Principle: with ``-XNoPatternSignatureBinds`, type variables cannot be bound in pattern signatures, closing one of the places where the Lexical Scoping Principle is currently violated.

This would not be the case with the treatment of in-scope variables as originally written in #126, where the choice between a binding site and an occurrence depends on whether a type variable is in scope.
The Explicit Variable Principle is made to hold, by allowing explicit binders for type variables for existentials and the variables bound by an inner forall in a higher-rank type.
The Explicit Binding Principle is made to hold, by introducing -XNoImplicitForAll and -XNoPatternSignatureBinds. However, it is impossible to use pattern signatures in this mode; there is no alternative way to bind pattern-signature variables.
The Visibility Orthogonality Principle is made to hold, by ensuring that types and terms are treated identically in patterns. This was not the case with the old version of #126 for constructor patterns, which treated variables after @ different to those without a @.

1.7 Costs and Drawbacks ¶

The poor interplay between -XExtendedForAllScope and -XTypeAbstractions is regrettable, but I see no way to improve this.
The extension shuffling introduces some complexity. Is the gain worth the complexity?

ghc-proposals documentation