Import list

```
module Term_Inference where

open import Data.Empty    using (⊥)
open import Data.Unit     using (⊤; tt)
open import Data.Sum      using (_⊎_; inj₁; inj₂)
open import Data.Nat      using (ℕ; zero; suc)```

Term inference

The Agda compiler tries to infer terms marked with underscore. If the choice of term is ambiguous, the term inference will fail.

Examples:

```
data Fin′ : ℕ → Set where
zero : (n : _) → Fin′ (suc n)            -- ℕ is inferred
suc  : (n : _) → Fin′ n → Fin′ (suc n)   -- ℕ is inferred again

x : Fin′ 3
x = suc _ (zero _)   -- 2 and 1 are inferred```

Term inference failure is marked with yellow colour.

Implicit arguments

Underscores can be hidden by making arguments of constructors implicit with curly brackets.

```
data Fin : ℕ → Set where
zero : {n : _} → Fin (suc n)
suc  : {n : _} → Fin n → Fin (suc n)```

After that, we obtain the following:

```
x′ : Fin 3
x′ = suc {_} (zero {_})```

And the `{_}`s can be now deleted:

```
x″ : Fin 3
x″ = suc zero```

Although `zero : Fin 1` and `zero : Fin 2`, `zero` does not have multiple different types; the implicit arguments make the types unique.

Named and multiple implicit arguments

There can be more implicit arguments, as the following definition demonstrates:

```
data T : ℕ → ℕ → ℕ → Set where
c : {n m k : _} → T (suc n) (suc m) (suc k)

xt : T 1 2 3
xt = c```

In addition to that, in case of multiple implicit arguments, some of their actual values may be set by naming them. For example:

```
xt' : T 1 2 3
xt' = c {m = 1}```

Syntactic abbreviations

Consider the following definitions again from above:

``````data Fin′ : ℕ → Set where
zero : (n : _) → Fin′ (suc n)
suc  : (n : _) → Fin′ n → Fin′ (suc n)

data Fin : ℕ → Set where
zero : {n : _} → Fin (suc n)
suc  : {n : _} → Fin n → Fin (suc n)``````

There variables with inferred types can be introduced by the `∀` (universal quantification) symbol, no matter if they are explicit or implicit:

``````data Fin′ : ℕ → Set where
zero : ∀ n → Fin′ (suc n)
suc  : ∀ n → Fin′ n → Fin′ (suc n)

data Fin : ℕ → Set where
zero : ∀ {n} → Fin (suc n)
suc  : ∀ {n} → Fin n → Fin (suc n)``````