# Generalization of Declared Variables¶

## Overview¶

Since version 2.6.0, Agda supports implicit generalization over variables in types.
Variables to be generalized over must be declared with their types in a `variable`

block. For example:

```
variable
ℓ : Level
n m : Nat
data Vec (A : Set ℓ) : Nat → Set ℓ where
[] : Vec A 0
_∷_ : A → Vec A n → Vec A (suc n)
```

Here the parameter `ℓ`

and the `n`

in the type of `_∷_`

are not bound explicitly,
but since they are declared as generalizable variables, bindings for them are inserted
automatically. The level `ℓ`

is added as a parameter to the datatype and `n`

is added
as an argument to `_∷_`

. The resulting declaration is

```
data Vec {ℓ : Set} (A : Set ℓ) : Nat → Set ℓ where
[] : Vec A 0
_∷_ : {n : Nat} → A → Vec A n → Vec A (suc n)
```

See Placement of generalized bindings below for more details on where bindings are inserted.

Variables are generalized in top-level type signatures, module telescopes, and record and datatype parameter telescopes.

Issues related to this feature are marked with generalize in the issue tracker.

## Nested generalization¶

When generalizing a variable, any generalizable variables in its type are also generalized
over. For instance, you can declare `A`

to be a type at some level `ℓ`

as

```
variable
A : Set ℓ
```

Now if `A`

is mentioned in a type, the level `ℓ`

will also be generalized over:

```
-- id : {A.ℓ : Level} {A : Set ℓ} → A → A
id : A → A
id x = x
```

The nesting can be arbitrarily deep, so

```
variable
x : A
refl′ : x ≡ x
refl′ = refl
```

expands to

```
refl′ : {x.A.ℓ : Level} {x.A : Set x.A.ℓ} {x : x.A} → x ≡ x
```

See Naming of nested variables below for how the names are chosen.

Nested variables are not necessarily generalized over. In this example, if the universe
level of `A`

is fixed there is nothing to generalize:

```
postulate
-- pure : {A : Set} {F : Set → Set} → A → F A
pure : {F : Set → Set} → A → F A
```

See Generalization over unsolved metavariables for more details.

Note

Nested generalized variables are local to each variable, so if you declare

```
variable
B : Set ℓ
```

then `A`

and `B`

can still be generalized at different levels. For instance,

```
-- _$_ : {A.ℓ : Level} {A : Set A.ℓ} {B.ℓ : Level} {B : Set B.ℓ} → (A → B) → A → B
_$_ : (A → B) → A → B
f $ x = f x
```

### Generalization over unsolved metavariables¶

Generalization over nested variables is implemented by creating a metavariable for each
nested variable and generalize over any such meta that is still unsolved after type
checking. This is what makes the `pure`

example from the previous section work: the
metavariable created for `ℓ`

is solved to level 0 and is thus not generalized over.

A typical case where this happens is when you have dependencies between different nested variables. For instance:

```
postulate
Con : Set
variable
Γ Δ Θ : Con
postulate
Sub : Con → Con → Set
idS : Sub Γ Γ
_∘_ : Sub Γ Δ → Sub Δ Θ → Sub Γ Θ
variable
δ σ γ : Sub Γ Δ
postulate
assoc : δ ∘ (σ ∘ γ) ≡ (δ ∘ σ) ∘ γ
```

In the type of `assoc`

each substitution gets two nested variable metas for their contexts,
but the type of `_∘_`

requires the contexts of its arguments to match up, so some of
these metavariables are solved. The resulting type is

```
assoc : {δ.Γ δ.Δ : Con} {δ : Sub δ.Γ δ.Δ} {σ.Δ : Con} {σ : Sub δ.Δ σ.Δ}
{γ.Δ : Con} {γ : Sub σ.Δ γ.Δ} → (δ ∘ (σ ∘ γ)) ≡ ((δ ∘ σ) ∘ γ)
```

where we can see from the names that `σ.Γ`

was unified with `δ.Δ`

and `γ.Γ`

with
`σ.Δ`

. In general, when unifying two metavariables the “youngest” one is eliminated which
is why `δ.Δ`

and `σ.Δ`

are the ones that remain in the type.

If a metavariable for a nested generalizable variable is partially solved, the left-over metas are generalized over. For instance,

```
variable
xs : Vec A n
head : Vec A (suc n) → A
head (x ∷ _) = x
-- lemma : {n : Nat} {xs : Vec Nat (suc n)} → head xs ≡ 1 → (0 < sum xs) ≡ true
lemma : head xs ≡ 1 → (0 < sum xs) ≡ true
```

In the type of `lemma`

a metavariable is created for the length of `xs`

, which
the application `head xs`

refines to `suc n`

, for some new metavariable `n`

.
Since there are no further constraints on `n`

, it’s generalized over, creating the
type given in the comment.

Note

Only metavariables originating from nested variables are generalized over. An exception
to this is in `variable`

blocks where all unsolved metas are turned into nested variables.
This means writing

```
variable
A : Set _
```

is equivalent to `A : Set ℓ`

up to naming of the nested variable (see below).

### Naming of nested variables¶

The general naming scheme for nested generalized variables is
`parentVar.nestedVar`

. So, in the case of the identity function
`id : A → A`

expanding to

```
id : {A.ℓ : Level} {A : Set ℓ} → A → A
```

the name of the level variable is `A.ℓ`

since the name of the nested variable is
`ℓ`

and its parent is the named variable `A`

. For multiple levels of nesting the
parent can be another nested variable as in the `refl′`

case above

```
refl′ : {x.A.ℓ : Level} {x.A : Set x.A.ℓ} {x : x.A} → x ≡ x
```

If a variable comes from a free unsolved metavariable in a `variable`

block
(see this note), its name is chosen as follows:

- If it is a labelled argument to a function, the label is used as the name,
- otherwise the name is its left-to-right index (starting at 1) in the list of unnamed variables in the type.

It is then given a hierarchical name based on the named variable whose type it occurs in. For example,

```
postulate
V : (A : Set) → Nat → Set
P : V A n → Set
variable
v : V _ _
postulate
thm : P v
```

Here there are two unnamed variables in the type of `v`

, namely the two arguments to `V`

.
The first argument has the label `A`

in the definition of `V`

, so this variable gets the name
`v.A`

. The second argument has no label and thus gets the name `v.2`

since it is the second
unnamed variable in the type of `v`

.

If the variable comes from a partially instantiated nested variable the name of the metavariable is used unqualified.

Note

Currently it is not allowed to use hierarchical names when giving parameters to functions, see Issue #3208.

## Placement of generalized bindings¶

The following rules are used to place generalized variables:

- Generalized variables are placed at the front of the type signature or telescope.
- Variables mentioned eariler are placed before variables mentioned later, where nested variables count as being mentioned together with their parent.

Note

This means that an implicitly quantified variable cannot depend on an explicitly quantified one. See Issue #3352 for the feature request to lift this restriction.

### Indexed datatypes¶

When generalizing datatype parameters and indicies a variable is turned into an index if it is only mentioned in indices and into a parameter otherwise. For instance,

```
data All (P : A → Set) : Vec A n → Set where
[] : All P []
_∷_ : P x → All P xs → All P (x ∷ xs)
```

Here `A`

is generalized as a parameter and `n`

as an index. That is, the
resulting signature is

```
data All {A : Set} (P : A → Set) : {n : Nat} → Vec A n → Set where
```

## Instance and irrelevant variables¶

Generalized variables are introduced as implicit arguments by default, but this can be changed to instance arguments or irrelevant arguments by annotating the declaration of the variable:

```
record Eq (A : Set) : Set where
field eq : A → A → Bool
variable
{{EqA}} : Eq A -- generalized as an instance argument
.ignore : A -- generalized as an irrelevant (implicit) argument
```

Variables are never generalized as explicit arguments.

## Importing and exporting variables¶

Generalizable variables are treated in the same way as other declared symbols
(functions, datatypes, etc) and use the same mechanisms for importing and exporting
between modules. This means that unless marked `private`

they are exported from a
module.

## Interaction¶

When developing types interactively, generalizable variables can be used in holes if they have already been generalized, but it is not possible to introduce new generalizations interactively. For instance,

```
works : (A → B) → Vec A n → Vec B {!n!}
fails : (A → B) → Vec A {!n!} → Vec B {!n!}
```

In `works`

you can give `n`

in the hole, since a binding for `n`

has been introduced
by its occurrence in the argument vector. In `fails`

on the other hand, there is no reference
to `n`

so neither hole can be filled interactively.