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  Setwhere
  []  : 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  Setwhere
  []  : 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.