# Generalization of Declared Variables¶

Variables to be generalized can declared with the keyword `variable`. For example:

```postulate
Con : Set

variable
Γ Δ Θ : Con
```

Declared variables are automatically generalized in type signatures, module telescopes and data and record type parameters and indices. For example,

```postulate
Sub : Con → Con → Set

id  : Sub Γ Γ
--  -- equivalent to
--  id  : {Γ : Con} → Sub Γ Γ

_∘_ : Sub Θ Δ → Sub Γ Θ → Sub Γ Δ
--  -- equivalent to
--  _∘_ : {Γ Δ Θ : Con} → Sub Θ Δ → Sub Γ Θ → Sub Γ Δ
```

Note that each type signature has a separate copy of its declared variables, so `id` and `_∘_` refer to two different `Γ` named variables.

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

```variable
n  : Nat

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

variable
A  : Set
x  : A
xs : Vec A n

-- Here `A` will be a parameter and `n` an index. That is,
-- data All {A : Set} (P : A → Set) : {n : Nat} → Vec A n → Set
data All (P : A → Set) : Vec A n → Set where
[]  : All P []
_∷_ : P x → All P xs → All P (x ∷ xs)
```

The following rules are used to place the generalized variables:

• Generalized variables are placed in the front of the type signatures.
• Variables defined sooner are placed before variables defined later. (The dependencies between the variables are obeyed. The current implementation uses “smallest-numbered available vertex first” topological sorting to determine the exact order.)

`variable` allows metavariables in the type of declared variables. For example:

```postulate
Ty  : Con → Set
_▹_ : (Γ : Con) → Ty Γ → Con

variable
A : Ty _       -- note the underscore here

postulate
π₁ : Sub Γ (Δ ▹ A) → Sub Γ Δ
--  -- equivalent to
--  π₁ : {Γ Δ : Con}{A : Ty Δ} → Sub Γ (Δ ▹ A) → Sub Γ Δ
--  -- note that the metavariable was solved with Δ
```

Note that each type signature has a separate copy of such metavariables, so the underscore in `Ty _` can be solved differently for each type signature which mentions `A`.

Unsolved metavariables originated from `variable` are generalized. For example:

```variable
σ δ ν : Sub _ _   -- metavariables: σ.1, σ.2, δ.1, δ.2, ν.1, ν.2

postulate
ass : (σ ∘ δ) ∘ ν ≡ σ ∘ (δ ∘ ν)
--  -- equivalent to
--  ass : {σ.1 σ.2 δ.1 ν.1 : Con}
--        {σ : Sub σ.1 σ.2}{δ : Sub δ.1 σ.1}{ν : Sub ν.1 δ.1}
--      → (σ ∘ δ) ∘ ν ≡ σ ∘ (δ ∘ ν)
```

Note that `δ.2` was solved with `σ.1` and `ν.2` was solved with `δ.1`. If two generalizable metavariables can be solved with each-other then the metavariable defined later will be eliminated.

Hierarchical names like `δ.2` are used so one can track the origin of the metavariables. Currently it is not allowed to use hierarchical names when giving parameters to functions, see Issue #3280 <https://github.com/agda/agda/issues/3280>.

Name hints of parameters are used for naming generalizable metavariables too:

```postulate
Sub' : (Γ Δ : Con) → Set   -- name hints for parameters of Sub'

variable
θ : Sub' _ _   -- metavariables: θ.Γ, θ.Δ
```

If a generalizable metavariable M is solved with term T then M is not generalized, but metavariables in T became candidates for generalization.

It is allowed to nest declared variables. For example:

```variable
ℓ : Level     -- let ℓ denote a level
S : Set ℓ     -- let A denote a set at a level ℓ

postulate
f : S → Set ℓ
--  -- equivalent to
--  f : {ℓ ℓ' : Level}{S : Set ℓ'} → S → Set ℓ
```

Issues related to this feature are marked with generalize in the issue tracker: https://github.com/agda/agda/labels/generalize