# 1 Visible forall in types of terms, and types in terms¶

Contents

- 1 Visible forall in types of terms, and types in terms
- 1.1 Background
- 1.2 Motivation
- 1.3 Proposal Structure
- 1.4 Part I: Proposed Change Specification
- 1.5 Part I: Examples and Explanation
- 1.6 Part II: Definitions
- 1.7 Part II: Proposed Change Specification
- 1.8 Part II: Examples
- 1.9 Effect and Interactions
- 1.10 Costs and Drawbacks
- 1.11 Alternatives
- 1.12 Unresolved Questions
- 1.13 Implementation Plan

We propose to allow visible erased dependent quantification, written as
`forall x ->`

, in types of terms.

## 1.1 Background¶

This proposal closely follows the design sketch laid out in the accepted proposal #378 Design for Dependent Types. It may help to read that design sketch first.

In particular, we use the following terminology:

- Type syntax
Parts of the program that are parsed with the

`type`

family of non-terminals (i.e.`type`

,`btype`

,`atype`

, etc) or the`kind`

non-terminal are considered to be written in**type syntax**.This includes (but is not limited to) types in type or class declarations, types after the

`::`

in a type or kind signature, types after the`@`

sign in visible type applications, the LHS and the RHS of type family instances, and so on.- Term syntax
Parts of the program that are parsed with the

`exp`

family of non-terminals (i.e.`exp`

,`infixexp`

,`fexp`

,`aexp`

, etc) or the`pat`

family of non-terminals (i.e.`pat`

,`apat`

, etc) are considered to be written in**term syntax**.This includes (but is not limited to) the LHS and the RHS of function bindings

`f x y = e`

, the LHS and the RHS of pattern bindings`p = e`

, the LHS and the RHS of`p <- e`

bindings in`do`

-notation, the top-level Template Haskell splices (e.g.`makeLenses ''T`

), and so on.- Namespace
Any identifier (including variables, type variables, data constructors, and type constructors) is said to belong to one of the two namespaces: the

**term namespace**and the**type namespace**. The namespace of an identifier is determined at its binding site.Identifiers bound in type syntax populate the type namespace; identifiers bound in term syntax populate the term namespace.

- Punning
Punning occurs when identifiers of the same spelling are introduced in both namespaces, for example:

data T = T

Now any use of

`T`

must use certain rules to disambiguate which`T`

is referred to.- Quantifier
Parts of a type that introduce a function parameter are called quantifiers:

`forall a. ty`

`forall a -> ty`

`foreach a. ty`

`foreach a -> ty`

`Eq a => ty`

`t1 -> t2`

(To see how

`=>`

is a quantifier, one must desugar it with dictionary-passing style).We classify quantifiers along several axes:

- Dependent or non-dependent
- Erased or retained
- Visible or invisible

- Dependence
We call a quantifier dependent when the parameter can be used in the type of the function result.

`forall a.`

, which introduces`a :: Type`

, is a dependent quantifier:id :: forall a. a -> a ^^^^^^^^^^^^^^^^ 'a' is used here

On the other hand,

`a ->`

, which introduces`x :: a`

, is a non-dependent quantifier:id :: forall a. a -> a ^^^^^^^^^^^^^^^^^^^^^^^ 'x' cannot be used here

- Erasure
We call a quantifier retained when the parameter can be pattern-matched on or returned as part of the result, and, as a consequence, must be passed during evaluation. For example,

`a ->`

is a retained quantifier:id :: forall a. a -> a id = \x -> x ^^^ 'x' is returned as the result not :: Bool -> Bool not b = case b of { ... } ^^^ 'b' is used in pattern-matching

On the other hand, in types of terms,

`forall a.`

is an erased quantifier:bad :: forall a. a -> a bad x = case a of { ... } ^^^ 'a' can not be pattern-matched on!

However, in types of types,

`forall a.`

is currently a retained quantifier, as it permits pattern-matching:type IsMaybe :: forall k. k -> Bool type family IsMaybe a where IsMaybe @(Type -> Type) Maybe = True -- matching 'k' with (Type -> Type) IsMaybe @Type (Maybe _) = True -- matching 'k' with Type IsMaybe _ = False

This is considered an oversight in the design of kind polymorphism, and we generally speak of

`forall x.`

as an erased quantifier. (Making it truly so is left as future work, out of scope of this proposal).- Visibility
We call a quantifier visible when the parameter must be specified at use sites, and invisible when the compiler tries to infer it at use sites.

Consider an expression such as

`id True`

. In this call, we have:`x=True`

, as specified`a=Bool`

, as inferred from`(x :: a) = (True :: Bool)`

The reason we don’t write

`id Bool True`

is that`forall a.`

is an invisible quantifier, while`a ->`

is a visible quantifier.With the

`TypeApplications`

extension, we can use a visibility override`@`

to specify an invisible parameter as if it was visible:id @Bool True

## 1.2 Motivation¶

In types of types (in kinds), we have the choice between invisible and visible dependent quantification:

```
type PInv :: forall k. k -> Type -- invisible quantification of 'k'
data PInv a = MkPInv
type PVis :: forall k -> k -> Type -- visible quantification of 'k'
data PVis k a = MkPVis
```

Invisible parameters, introduced with `forall x.`

, are inferred by the
compiler at use sites. Visible parameters, introduced with `forall x ->`

,
must be specified by the user:

```
type TInv = PInv 15 -- infer (k~Nat) from (a::k)~(15::Nat)
type TVis = PVis Nat 15 -- no inference
```

This means our quantifier grid is complete with regards to dependence and visibility:

```
Quantifiers in
types of types Dependent Non-dependent
┌──────────────┬───────────────┐
Visible │ forall a -> │ a -> │
├──────────────┼───────────────┤
Invisible │ forall a. │ c => │
└──────────────┴───────────────┘
```

On the other hand, in types of terms, our grid is incomplete:

```
Quantifiers in
types of terms Dependent Non-dependent
┌──────────────┬───────────────┐
Visible │ │ a -> │
├──────────────┼───────────────┤
Invisible │ forall a. │ c => │
└──────────────┴───────────────┘
```

Other than making terms and types more symmetrical, filling this empty cell would let us design better APIs without the use of proxy types or ambiguous types, and with better error messages.

For example, consider a function that gives the memory residence for a type:

```
sizeOf :: forall a. Sized a => Proxy a -> Int
```

To find out the size of a boolean value, the user of this API would write
`sizeOf (Proxy :: Proxy Bool)`

or `sizeOf (Proxy @Bool)`

. This has two disadvantages:

- Constructing a
`Proxy`

value is unnecessarily verbose, making`sizeOf`

clunky to use. - The
`Proxy`

value is passed at runtime. Even if the optimizer can eliminate it sometimes, there are cases when it cannot.

There is a workaround which involves `AllowAmbiguousTypes`

and
`TypeApplications`

. Here’s an alternative API design:

```
sizeOf :: forall a. Sized a => Int
```

The user is supposed to use a visibility override, `sizeOf @Bool`

. While it
does address the concerns about verbosity and the runtime cost, the error
messages degrade significantly. The invisible parameter `a`

is now ambiguous,
so if the user forgets to specify it, the compiler tries to infer `a`

and
inevitably fails:

```
print_int :: Int -> IO ()
-- Valid code:
main = print_int (sizeOf @Bool)
-- The parameter is not specified, extremely bad error message:
--
-- • Ambiguous type variable ‘a0’ arising from a use of ‘sizeOf’
-- prevents the constraint ‘(Sized a0)’ from being solved.
-- Probable fix: use a type annotation to specify what ‘a0’ should be.
-- These potential instance exist:
-- instance [safe] Sized Bool -- Defined at <interactive>:15:10
-- • In the first argument of ‘print_int’, namely ‘sizeOf’
-- In the expression: print_int sizeOf
-- In an equation for ‘main’: main = print_int sizeOf
--
main = print_int sizeOf
```

It also means that eta-reduction is not possible:

```
-- Valid code:
mySizeOf :: forall a. Sized a => Int
mySizeOf @a = sizeOf @a
-- Eta-reduction attempt fails:
--
-- • Could not deduce (Sized a0) arising from a use of ‘sizeOf’
-- from the context: Sized a
-- bound by the type signature for:
-- mySizeOf :: forall a. Sized a => Int
-- The type variable ‘a0’ is ambiguous
--
mySizeOf :: forall a. Sized a => Int
mySizeOf = sizeOf
```

If we had visible `forall`

, for which there is already precedent in types of
types, we could design an API for `sizeOf`

that has none of the issues listed
above:

```
sizeOf :: forall a -> Sized a => Int
```

This type captures the intent behind this function, and, if we allow it, its use would have the least noise and good error messages:

```
print_int :: Int -> IO ()
-- Valid code:
main = print_int (sizeOf Bool) -- NB: no visibility override '@'
-- The parameter is not specified, good error message:
--
-- • Couldn't match expected type ‘Int’
-- with actual type ‘forall a -> Sized a => Int’
-- • Probable cause: ‘sizeOf’ is applied to too few arguments
-- In the first argument of ‘print_int’, namely ‘sizeOf’
-- In the expression: print_int sizeOf
-- In an equation for ‘main’: main = print_int sizeOf
--
main = print_int sizeOf
```

Eta-reduction is now possible:

```
-- Valid code:
mySizeOf :: forall a -> Sized a => Int
mySizeOf a = sizeOf a
-- Eta-reduction attempt succeeds:
mySizeOf :: forall a -> Sized a => Int
mySizeOf = sizeOf
```

The proposed visible `forall`

would be an erased quantifier. However, if
we were to make it retained, we would get full-blown dependent functions
(pi-types). Therefore, implementing this feature would pave the road for future
work on Dependent Haskell.

To summarize, there are three reasons to make this change:

- Language consistency (symmetry between terms and types)
- Ability to design better APIs (good error messages, no proxy types, no ambiguous types)
- Prepare the compiler internals for further work on dependent types

## 1.3 Proposal Structure¶

We shall present this proposal in two parts:

- In Part I we introduce the
`forall a ->`

quantifier in types of terms but also require a syntactic marker at use sites. This is not as convenient to use (i.e. users would have to write`sizeOf (type Bool)`

instead of`sizeOf Bool`

), but is much easier to specify and understand. - In Part II we specify when it is permissible to omit the
`type`

herald. This greatly increases the convenience of using the proposed feature, but also makes the specification more intricate.

## 1.4 Part I: Proposed Change Specification¶

Add a new language extension,

`RequiredTypeArguments`

. When`RequiredTypeArguments`

is in effect, lift the restriction that the`forall a ->`

quantifier cannot be used in types of terms.**Syntax**. When`ExplicitNamespaces`

is in effect, extend the grammar (as in the Haskell 2010 Report) as follows:exp ::= | 'type' ktype | ... pat ::= | 'type' ktype | ...

Though it is not included in the Report,

`ktype`

above refers to a non-terminal in GHC’s grammar. This non-terminal includes kind annotations and`forall`

-types.The

`type`

keyword at the top-level is interpreted as it always has been; it does not start an expression (as would be used in a Template Haskell declaration splice) or pattern (as would be used in a pattern binding).**Name resolution**. A type embedded into a term with the`type`

marker follows type-level name resolution rules (i.e. uses of punned identifiers resolve to the type namespace), both at binding sites and at use sites.The

`ScopedTypeVariables`

extension has no effect on variables introduced by`forall a ->`

.**Type checking**. In type checking, we alternate between two distinct modes:*checking*and*inference*. This idea, called bidirectional type checking, is presented in more detail in “A quick look at impredicativity”.In inference mode, we never infer

`forall x -> t`

as the type of a lambda expression. Accordingly, writing`\ (type a) -> ...`

in inference mode is always an error.In checking mode, in a function application chain

`f e1 e2 e3`

, we follow the rules shown in Figure 4 of “A quick look at impredicativity”, extended as follows:G |- sigma[a := rho]; pis ~> Theta; phis; rho_r ------------------------------------------------------------------ ITVDQ G |- (forall a -> sigma); (type rho), pis ~> Theta; phis; rho_r

In checking mode, in a function binding

`f (type x) = ...`

or a lambda`\(type x) -> ...`

, the`x`

is a fresh skolem.

**Validity**. Expressions and patterns of form`type t`

but not covered by the type checking rules above are illegal.Specifically, any expression of form

`type t`

must be used as an argument to a function, or else it is rejected with a type error:x = f (type Int) -- OK x = type Int -- invalid use of a type in a term

This is checked during type checking, so Template Haskell is unaffected, and

`[e| type Int |]`

is allowed (but different from`[t| Int |]`

).Furthermore, any pattern of form

`type t`

must be either a variable or a wildcard:f (type x) = ... -- OK f (type _) = ... -- OK f (type Int) = ... -- invalid use of a type in a term

This is also checked during type checking, so Template Haskell must be able to represent patterns such as

`[p| type Int |]`

.**Erasure**. In types of terms,`forall a ->`

is an erased quantifier. Making`forall a ->`

erased in types of types is out of scope of this proposal.

## 1.5 Part I: Examples and Explanation¶

A variant of

`id`

that uses visible`forall`

:-- Definition: idv :: forall a -> a -> a idv (type a) x = x :: a -- Usage: n = idv (type Double) 42

This is equivalent to

`n = (42 :: Double)`

.A wrapper around

`typeRep`

that uses visible`forall`

:-- Definition: typeRepVis :: forall a -> Typeable a => TypeRep a typeRepVis (type a) = typeRep @a -- Usage: t = typeRepVis (type (Maybe String))

A wrapper around

`sizeOf`

that uses visible`forall`

instead of`Proxy`

:-- Definition: sizeOfVis :: forall a -> Storable a => Int sizeOfVis (type a) = sizeOf (Proxy :: Proxy a) -- Usage: n = sizeOfVis (type Int)

A wrapper around

`symbolVal`

that uses visible`forall`

instead of`Proxy`

:-- Definition: symbolValVis :: forall s -> KnownSymbol s => String symbolValVis (type s) = symbolVal (Proxy :: Proxy s) -- Usage str = symbolValVis (type "Hello, World")

Note that as long as we limit ourselves to part I of this proposal, we need the
`type`

marker in all of the above examples, even when the argument is a
syntactically valid term. If the programer were to write ```
symbolValVis "Hello,
World"
```

, they would get an error message stating that a term argument was
received where a type argument was expected. That’s because our typing rule
`ITVDQ`

explicitly requires the argument to be of form `type rho`

.

Could we extend our system to permit arguments without the `type`

prefix?
That is precisely the subject of part II.

## 1.6 Part II: Definitions¶

### 1.6.1 The Resolved Syntax Tree¶

Define **resolved syntax tree** as a representation of a Haskell program
that encodes its syntactic and binding structure, but does not yet include type
information. In particular, in the **resolved syntax tree**, the following
information has been fully determined:

Variable and type variable occurrences have been linked to their bindings, in accordance with shadowing and punning rules.

Shadowing. Consider the following program:

a = 42 f a = \a -> a

In the resolved syntax tree, the occurrence of

`a`

has been linked to its binding as follows:a₀ = 42 f a₁ = \a₂ -> a₂

Thus, we know it stands for

`a₂`

rather than`a₁`

or`a₀`

.Punning. Consider the following program:

{-# LANGUAGE ScopedTypeVariables #-} id :: forall a. a -> a id a = (a :: a)

In the resolved syntax tree, the occurrences of

`a`

have been linked to their bindings as follows:id :: forall aₜ. aₜ -> aₜ id aₑ = (aₑ :: aₜ)

Data constructor and type constructor occurrences have been linked to their bindings, in accordance with the punning rules. Consider the following program:

data Pair a b = Pair !a !b dup :: a -> Pair a a dup x = Pair x x

In the resolved syntax tree, the occurrences of

`Pair`

have been linked to their bindings as follows:data Pairₜ a b = Pairₑ !a !b dup :: a -> Pairₜ a a dup x = Pairₑ x x

The fixity and associativity of infix operators have been determined. Consider the following program:

import Prelude ((+), (*)) f x = x + x * x * x

In the resolved syntax tree, the structure of the infix expression is established as follows:

f x = x + ((x * x) * x)

The meaning of built-in tuple syntax has been determined. Let us denote a pair as

`(a, b)ₑ`

and the type of a pair as`(a, b)ₜ`

. Now consider the following program:p :: (Integer, String) p = (42, "Hello")

In the resolved syntax tree, the meaning of the built-in tuple syntax has been determined as follows:

p :: (Integer, String)ₜ p = (42, "Hello")ₑ

Likewise, for all tuple arities (including the unit type

`()`

as a 0-arity tuple).The meaning of built-in list syntax has been determined. Let us denote a singleton list as

`[a]ₑ`

and the list type as`[a]ₜ`

. Now consider the following program:f :: a -> [a] f x = [x]

In the resolved syntax tree, the meaning of the built-in list syntax is determined as follows:

f :: a -> [a]ₜ f x = [x]ₑ

This also applies to the empty square brackets

`[]`

, which can either stand for an empty list`[]ₑ`

or the list type constructor`[]ₜ`

.With

`DataKinds`

, the`'[a]`

syntax in a type-level context is resolved as`[a]ₑ`

; in a term-level context, this syntax is not available.The meaning of

`*`

has been determined. It can stand for one of the following:`Type`

from the`Data.Kind`

module (under`-XStarIsType`

)- An occurrence of a term-level
`(*)`

infix operator - An occurrence of a type-level
`(*)`

infix operator (under`-XTypeOperators`

)

The meaning of

`'`

has been determined. It can stand for one of the following:- Namespace selection syntax (under
`-XDataKinds`

) - Name quotation syntax (under
`-XTemplateHaskell`

)

- Namespace selection syntax (under

## 1.7 Part II: Proposed Change Specification¶

### 1.7.1 Syntax¶

Extend the term syntax with several constructs that previously could only occur at the type level:

- Function arrows:
`a -> b`

- Multiplicity-polymorphic function arrows:
`a %m -> b`

(under`-XLinearTypes`

) - Constraint arrows:
`a => b`

- Universal quantification:
`forall a. b`

- Visible universal quantification:
`forall a -> b`

.

We will call them

**types-in-terms**.Grammatically, their constituents are terms, not types:

proposed grammar: as opposed to: ┌────────────────────────────────────┬───────────────────────────────────────┐ │ │ │ │ exp ::= │ exp ::= │ │ | exp₀ '->' exp₁ │ | type₀ '->' type₁ │ │ | exp₀ '=>' exp₁ │ | type₀ '=>' type₁ │ │ | 'forall' tv_bndrs '.' exp │ | 'forall' tv_bndrs '.' type │ │ | 'forall' tv_bndrs '->' exp │ | 'forall' tv_bndrs '->' type │ │ │ │ └────────────────────────────────────┴───────────────────────────────────────┘

This is a necessity to avoid parsing conflicts, with the following consequences:

- The
`'`

symbol signifies Template Haskell name quotation rather than`DataKinds`

promotion. - The
`*`

symbol is treated as an infix operator regardless of`-XStarIsType`

. - Built-in syntax for tuples and lists is interpreted as in terms.
That is,
`[a]`

is a singleton list rather than the type of a list, and`(a, b)`

is a pair rather than the type of a pair.

- Function arrows:
The syntactic descriptions here applying to expressions apply equally to patterns, though we will continue to discuss only expressions.

Make

`forall`

a keyword at the term level. Not guarded by any extension (same motivation as #193). This implies`forall`

is no longer a valid identifier.For three releases before this change takes place, include a new warning

`-Wforall-identifier`

in`-Wdefault`

. This warning will be triggered at definition sites (but not use sites) of`forall`

as an identifier.This change applies to

`∀`

(the`UnicodeSyntax`

rendition of`forall`

) as well.When

`ViewPatterns`

are enabled, interpret`f (a -> b) = ...`

as a view pattern, otherwise as`f ((->) a b) = ...`

.`case ... of x -> y -> z`

is an error. We require parentheses to disambiguate:`case ... of (x -> y) -> z`

`case ... of x -> (y -> z)`

### 1.7.2 Name resolution¶

During name resolution,

Identifiers bound in term syntax populate the term namespace; identifiers bound in type syntax populate the type namespace.

This is already the case, but now we generalize this rule to cover types-in-terms, which are considered term syntax.

When looking up an identifier

`v`

or`V`

in type syntax, look it up in the type namespace first; if it is not found there, look it up in the term namespace.This is already the case for uppercase identifiers if

`DataKinds`

is enabled, but now we extend this rule to lowercase identifiers if`RequiredTypeArguments`

is enabled.When looking up an identifier

`v`

or`V`

in term syntax, look it up in the term namespace first; if it is not found there, look it up in the type namespace.This is a new rule, but notice how it mirrors the one for type syntax.

### 1.7.3 Implicit quantification¶

Implicit quantification is an existing feature that allows the programmer to omit a

`forall`

:g :: a -> a -- implicit g :: forall a. a -> a -- explicit

This sort of quantification only happens if the variable is not already in scope:

{-# LANGUAGE ScopedTypeVariables #-} f :: forall a. a -> a f = ... where g :: a -> a -- No implicit quantification!

In other words, we quantify only over

*free*variables.With the proposed changes to name resolution, variables that were previously free are not free anymore:

a = 42 f :: a -> a -- No implicit quantification!

This is a breaking change, and that is why the fallback to the term namespace in type syntax is guarded behind

`RequiredTypeArguments`

.Without

`RequiredTypeArguments`

, implicit quantification is not affected.In order to facilitate writing code that is forward-compatible with

`RequiredTypeArguments`

, introduce a new warning to`-Wcompat`

:`-Wterm-variable-capture`

. This warning will notify users when implicit quantification occurs that would stop working under`RequiredTypeArguments`

.

### 1.7.4 Type checking¶

Generalize the

`ITVDQ`

rule introduced earlier by using`t2t`

:rho = t2t(e) G |- sigma[a := rho]; pis ~> Theta; phis; rho_r ---------------------------------------------------------- ITVDQ-T2T G |- (forall a -> sigma); e, pis ~> Theta; phis; rho_r

`t2t`

transforms term arguments into type arguments, see “T2T-Mapping” below for an informal definition.In other words, given

`f :: forall a -> t`

, the`x`

in`f x`

is parsed and renamed as a term, but then mapped to a type.Any uses of terms in types are ill-typed:

a = 42; f :: Proxy a -> Proxy b -- invalid occurrence of "a" in a type-level position

Any uses of types in terms that do not undergo the T2T transformation are also ill-typed::

f _ = Int -- invalid occurrence of "Int" in a term-level position

When in the checking mode of bidirectional type checking (e.g. in a function binding with an explicit type signature), allow a pattern to bind type variables in the term namespace, such as

`x`

here:f :: forall a -> ... f x = ...

The

`x`

identifier is bound in the term namespace, but stands for an erased,`forall`

-bound type variable.Just as with patterns that use the

`type`

herald explicitly, we permit only variables and wildcards in such positions:f :: forall a -> ... f x = ... -- OK f _ = ... -- OK f Int = ... -- illegal to match on a type

We could, but we do not relax this requirement even when the type is statically known:

data T a where Typed :: forall a -> a -> T a g :: T Int -> ... g (Typed Int x) = ... -- Reasonable, but no.

This is a conservative decision that can be revised in a later proposal.

### 1.7.5 Namespaces vs Semantics¶

With the proposed changes, the namespace of an identifier is no longer tied to whether it stands for a type variable or a term variable.

Before this proposal, all term variables (retained, values, runtime) used names from the term namespace, and all type variables (erased, types, compile-time) used names from the type namespace. This is no longer the case.

### 1.7.6 T2T-Mapping¶

T2T (term-to-type) is a mapping from expressions to types that operates on a
resolved syntax tree and is invoked by the `T2T`

typing rule.

The T2T mapping is partial: it succeeds on expressions that are within the Static Subset (introduced in #378 Design for Dependent Types), and fails on expressions outside of this subset.

- Embedded types
`type t`

are mapped to`t`

directly, without modification. - Variables and constructors (regardless of their namespace) are mapped
directly, without modification.
- In the type checking environment, the variable must stand for a type variable.
- #378 Design for Dependent Types allows term variables in types. However, while the referenced section presents how this can be useful with
`foreach`

, it also explains that it seems much less useful without it. Hence, we save this part of the design of DH for a future proposal that includes a retained quantifier like`foreach`

.

- #378 Design for Dependent Types allows term variables in types. However, while the referenced section presents how this can be useful with
- In the type checking environment, the constructor must stand for a type
constructor, or else require
`DataKinds`

. - In the type checking environment, there should be no variable of the same name but from a different namespace, or else raise an ambiguity error (does not apply to constructors).

- In the type checking environment, the variable must stand for a type variable.
- The types-in-terms (such as
`a -> b`

,`a => b`

,`forall a. b`

) are mapped to types directly, without modification aside from recursively processing subterms. - Function application
`e₀ e₁`

is mapped to type-level function application`t₀ t₁`

, where`t₀ = t2t(e₀)`

,`t₁ = t2t(e₁)`

. - With
`DataKinds`

, a numeric literal`42`

is mapped to a promoted numeric literal. - With
`DataKinds`

, a string literal`"Hello"`

is mapped to a promoted string literal`"Hello"`

. - With
`DataKinds`

, a character literal`'x'`

is mapped to a promoted character literal`'x'`

. - A fractional numeric literal
`3.14`

cannot be mapped at the moment, as we do not have promoted fractional numeric literals. - An unboxed numeric literal
`1337#`

cannot be mapped at the moment, as we do not have promoted unboxed types. - With
`DataKinds`

, a tuple`(e₀, e₁, ...)ₑ`

is mapped to a promoted tuple`(t₀, t₁, ...)ₑ`

, where`t₀ = t2t(e₀)`

,`t₁ = t2t(e₁)`

. - An unboxed tuple
`(# a, b #)`

cannot be mapped at the moment, as we do not have promoted unboxed types. - With
`DataKinds`

, a list literal`[e₀, e₁, ...]`

is mapped to a promoted list`[t₀, t₁, ...]`

, where`t₀ = t2t(e₀)`

,`t₁ = t2t(e₁)`

. - With
`TypeApplications`

, type application`e₀ @t₁`

is mapped to type-level type application`t₀ @t₁`

, where`t₀ = t2t(e₀)`

. - With
`TypeOperators`

, infix application`e₀ op e₁`

is mapped to type-level infix application`e₀ tyop e₁`

, where`t₀ = t2t(e₀)`

,`t₁ = t2t(e₁)`

,`tyop = t2t(op)`

. - With
`KindSignatures`

, a type signature`e₀ :: t₁`

is mapped to a kind signature`t₀ :: t₁`

, where`t₀ = t2t(e₀)`

. - Lambda functions
`\x -> b`

are not mapped and their use is an error, as we do not have type-level lambdas at the moment. - Case-expressions
`case x of ...`

are not mapped and their use is an error, as we do not have type-level case-expressions. - If-expressions
`if c then a else b`

are not mapped and their use is an error, as we do not have type-level if-expressions. - In the same spirit, other syntactic constructs are mapped when there’s a direct type-level equivalent, and their use is an error otherwise.

In accordance with the **Lexical Scoping Principle** of #378 Design for Dependent Types,
T2T preserves the binding structure and the meaning of the syntactic constructs
in the resolved syntax tree.

For example, in `f T`

, the T2T transformation will never change whether the
`T`

refers to a type constructor or a data constructor. Likewise, it will not
change `[a]`

from a singleton list to the list type, or vice versa. The
mapping is as direct as possible and could be removed if we had a single
syntactic category for terms and types.

## 1.8 Part II: Examples¶

A variant of

`id`

that uses visible`forall`

:-- Definition: idv :: forall a -> a -> a idv a x = x :: a -- Usage: n = idv Double 42

This is equivalent to

`n = (42 :: Double)`

.A wrapper around

`typeRep`

that uses visible`forall`

:-- Definition: typeRepVis :: forall a -> Typeable a => TypeRep a typeRepVis a = typeRep @a -- Usage: t = typeRepVis (Maybe String)

A wrapper around

`sizeOf`

that uses visible`forall`

instead of`Proxy`

:-- Definition: sizeOfVis :: forall a -> Storable a => Int sizeOfVis a = sizeOf (Proxy :: Proxy a) -- Usage: n = sizeOfVis Int

A wrapper around

`symbolVal`

that uses visible`forall`

instead of`Proxy`

:-- Definition: symbolValVis :: forall s -> KnownSymbol s => String symbolValVis s = symbolVal (Proxy :: Proxy s) -- Usage str = symbolValVis "Hello, World"

### 1.8.1 Compile-time color literals¶

Definition site:

```
type family ParseRGB (s :: Symbol) :: (Nat, Nat, Nat) where
...
type KnownRGB :: (Nat, Nat, Nat) -> Constraint
class KnownRGB c where
_rgbVal :: (Word8, Word8, Word8)
rgb :: forall s -> KnownRGB (ParseRGB s) => (Word8, Word8, Word8)
rgb s = _rgbVal @(ParseRGB s)
```

Use site:

```
ghci> rgb "red"
(255, 0, 0)
ghci> rgb "#112233"
(17, 34, 51)
ghci> rgb "asdfasdf"
-- custom type error from ParseRGB
```

### 1.8.2 Corner Cases¶

Scoped type variables:

f :: forall a. [a] -> [a] f x = g a x

Here the

`a`

in the first argument to`g`

is not rejected; rather it is an occurrence of the lexically scoped type variable`a`

bound by the`forall`

in`f`

’s type signature. If`g`

turns out to have a visible dependent type, the argument will be converted to a type; if not, it will be rejected.Punning and a local variable:

f :: forall a. [a] -> [a] f a = g a a

Here both

`a`

arguments to`g`

are bound to the inner term-level`a`

binder (`f`

’s argument), regardless of the type of`g`

.Punning and a top-level variable:

a :: Int a = 3 f :: forall a. [a] -> [a] f x = g a a

Both

`a`

arguments to`g`

are bound to term-level binding for`a`

. In terms, a term-level binding “wins”. If`g`

turns out to have a visible dependent type, the program will be rejected because`g`

’s first argument is a type, not a term.Punning and types-in-terms:

f :: forall a. [a]->[a] f a = g (a -> (forall b. b -> a)) a

Again, all those

`a`

’s in`g`

’s arguments are bound to the term-level`a`

. The clues that we are in a type, from the`(->)`

and`forall`

, are not used to change the namespace.Punning and shadowing:

h a = g (forall a. a->a) a

The

`forall`

binds`a`

and that binding is seen by the occurrences in`a->a`

. That is, in a term the forall-bound variables are in the term namespace.Built-in syntax:

x1 = g (Int,Bool) x2 = g [Int]

Here, the built-in syntax occurs in a term-level context, so

`(Int,Bool)`

is a promoted pair, and`[Int]`

is a promoted singleton list.One way to change this is to use synonyms from

`GHC.Tuple`

:x1 = g (TupleN Int Bool) x2 = g (List Int)

Another way is to use the

`type`

herald:x1 = g (type (Int,Bool)) x2 = g (type [Int])

This is purely a matter of style.

The

`@`

changes the meaning of built-in syntax:a = f @(Int,Bool) b = g (Int,Bool)

In

`a`

, the argument is the pair type, in`b`

it is a promoted pair.One way to resolve this is to use synonyms from

`GHC.Tuple`

:a = f @(TupleN Int Bool) b = g (TupleN Int Bool)

Another way is to use the

`type`

herald:a = f @(Int,Bool) b = g (type (Int,Bool))

The

`@`

changes the namespace:data StrictPair a b = StrictPair !a !b x = f (StrictPair Int Bool) y = g @(StrictPair Int Bool)

Resolved with the

`type`

herald or by renaming one of the`StrictPair`

constructors.Type variables as function parameters:

f :: forall a -> a -> a f x y = g True where g :: b -> x g _ = y

Here,

`x`

is a name in the term namespace, but it is in fact a type variable, later used used in the type signature of`g`

.The

`b`

is bound implicitly in this example, assuming there’s no top-level definition of`b`

. To make it clean, one can use an explicit`forall`

:... where g :: forall b. b -> x g _ = y

This is similar to the situation with

`ScopedTypeVariables`

, where we also cannot assume that all lowercase variables in a signature are free.

## 1.9 Effect and Interactions¶

Visible

`forall`

becomes available in types of terms, making them more similar to types of types. There remains a discrepancy that`forall`

in types of types is actually a retained quantifier, while the proposed`forall x ->`

in types of terms is erased. This is to be resolved in the future by making both of them erased.Even though types-in-terms may look like types they are considered term syntax, and a variable bound by a forall-in-terms populates the term namespace. This means that in

`\x -> f (forall x. x)`

, the occurrence of`x`

refers to the forall-bound type variable rather than the lambda-bound variable.The renaming of a visible dependent argument is different than that of a dependent argument with a visibility override. Consider this code:

f :: forall a. Tagged a () g :: forall a -> Tagged a () data T = T a = f @T b = g T

In

`f @T`

, we refer to the type constructor, but in`g T`

we refer to the data constructor.The implementation may offer warning flags to help the user identify such ambiguous occurrences.

When punned names come from external libraries, there are several workarounds to resolve the ambiguity:

Using

`-XExplicitNamespaces`

:import Data.Proxy import qualified Data.Proxy (type Proxy) as T x = f Proxy -- refers to the data constructor y = f T.Proxy -- refers to the type constructor

Using a type synonym:

import Data.Proxy type TProxy = Proxy x = f Proxy -- refers to the data constructor y = f TProxy -- refers to the type constructor

Using the

`type`

herald:import Data.Proxy x = f Proxy y = f (type Proxy)

Identifiers bound to terms are not promoted. Consider this well-typed program:

f :: forall a. Tagged a () g :: forall a -> Tagged a () a = f @(Just True) -- ok b = g (Just True) -- ok

If we factor out

`Just True`

into a type synonym, it continues to work:type X :: Maybe Bool type X = Just True a = f @X -- still OK b = g X -- still OK

However, if we bind it to a term-level variable, the example becomes ill-typed:

x :: Maybe Bool x = Just True a = f @x -- not currently valid b = g x -- not valid under the proposal

This is because we retain the distinction between terms and types. This proposal is a step towards dependent types, but it does not go all the way. Accepting the program above is left as future work.

## 1.10 Costs and Drawbacks¶

This is one more feature to implement and maintain.

## 1.11 Alternatives¶

- Include the proposed functionality in
`ExplicitForAll`

instead of introducing a new extension. - The extension name could use a different name, such as
`-XVDQ`

or`-XVisibleForAll`

. - We could guard type-level uses of visible
`forall`

behind the`VisibleForAll`

extension flag. This would break existing code.

Instead of the

`type`

herald, we could repurpose`@`

as a syntactic marker that indicates types occurring within terms. That is, while`forall x ->`

is a compulsory parameter and`forall x.`

is not, the use sites would be`f @Int`

in both cases.There are several issues with this alternative:

- it creates more syntactic noise in the unambiguous cases (e.g.
`f Int`

, assuming no data constructor named`Int`

) - it is inconsistent with what we have in types where
`@`

is used as a visibility override - it does not move us towards a single syntax for types and terms, which would be an advantage when we have dependent types
- The dual purpose of
`@`

as both a visibility override and a namespace specifier would lead to unwanted interference between`forall x.`

and`forall x ->`

. For example, given`f :: forall k. forall (a::k) -> blah`

, it wouldn’t be possible to specify`a=Int`

as`f @Int`

; one would have to write`f @_ @Int`

or change the type of`f`

to`f :: forall {k}. forall (a::k) -> blah`

.

Richard Eisenberg characterizes this alternative as follows:

It moves us away from uniformity. Let’s even pretend for a moment that I’m not trying to actually merge the term-level and type-level.

Right now, we can say this:

type VDQ :: forall k1. forall k2 -> k1 -> k2 -> Type data VDQ k2 a b type VDQIntTrue = VDQ @Type Bool Int True type VDQCharFalse = VDQ Bool Char False

If we were to require the

`@`

in terms, the term-level equivalent would be:vid :: forall a. forall b -> a -> b -> () vid _ _ _ = () ex1 = vid @Int @Bool 3 True ex2 = vid @_ @Bool 'x' False

These look different! Why different syntaxes for the same idea?

Worse, imagine a data constructor:

data Silly a b where Mk :: forall a. forall b -> a -> b -> Silly a b

Now we have this oddity:

type Different1 = Mk @Nat Bool 3 True type Different2 = Mk Bool "hi" False different3 = Mk @Int @Bool 3 True different4 = Mk @_ @Bool "hi" False

Here, the right-hand sides should be

*the same*, but they have to be different.Today, we have non-uniformity by omission: we have no visible

`forall`

in types of terms. But with your proposed`@`

on required dependent arguments, we would have active non-uniformity, which seems worse as it paints us into a corner that’s difficult to escape from. At least non-uniformity by omission can, in theory, be fixed uniformly, later.- it creates more syntactic noise in the unambiguous cases (e.g.
A previous iteration of this proposal dictated to switch to a type-level name resolution context when processing types-in-terms; we could also parse the right-hand side of

`forall a. t`

as a type; and we could map the`forall`

in terms bind variables in the type namespace.The parsing and name resolution rules of these alternatives were deemed too subtle, so we opted for a design where types-in-terms are parsed and renamed as ordinary terms.

We could error on ambiguous variable occurrences earlier in the pipeline, in the renamer, but then enabling

`RequiredTypeArguments`

would result in rejecting currently valid code:id :: forall a. a -> a id a = (a :: a)

Instead, we opted to raise the ambiguity error during T2T.

## 1.12 Unresolved Questions¶

None at the moment.

## 1.13 Implementation Plan¶

I (Vladislav Zavialov) or a close collaborator will implement this change. There’s currently a prototype by Daniel Rogozin in the works.