# Opaque definitions¶

Opaque definitions are a mechanism for controlling unfolding of Agda definitions, to help with both goal readability and performance. Like abstract definitions, opaque definitions will not unfold in general, but unlike `abstract` definitions, opacity can be selectively controlled at use-sites.

Our implementation of unfolding control is based on the theory introduced by Gratzer et. al. in Controlling unfolding in type theory, but handled entirely at the elaborator level, without a dependency on our (cubical) extension types.

## Overview¶

• Functions (and primitive functions) can be marked `opaque`. Outside of `opaque` blocks, these behave like postulates.

• Opaque blocks, even in unrelated modules, can have `unfolding` clauses, which allow the user to list their choice of names that should be locally treated as transparent.

• Opaque definitions do not reduce in type signatures, even inside opaque blocks where they would otherwise be unfolded.

## Unfolding opaque definitions¶

Consider an implementation of the integers as an abstract setoid: The underlying representation is given by pairs of natural numbers, representing a difference, but day-to-day, we would like to treat `ℤ` as its own type.

Our core module might define these operations:

```module Integer where
opaque
ℤ : Set
ℤ = Nat × Nat

_≡ℤ_ : (x y : ℤ) → Set
(p , n) ≡ℤ (p' , n') = (p + n') ≡ (p' + n)

infix 10 _≡ℤ_

0ℤ : ℤ
0ℤ = 0 , 0

1ℤ : ℤ
1ℤ = 1 , 0

_+ℤ_ : (x y : ℤ) → ℤ
(p , n) +ℤ (p' , n') = (p + p') , (n + n')

_*ℤ_ : (x y : ℤ) → ℤ
(a , b) *ℤ (c , d) = ((a * c) + (b * d)) , ((a * d) + (b * c))

infixl 20 _+ℤ_
infixl 30 _*ℤ_

-ℤ_ : ℤ → ℤ
-ℤ (p , n) = (n , p)
```

We’d now like to prove that the integers form a ring, under the `_≡ℤ_` notion of equality. Some of the equations on natural numbers involved are pretty nasty, though, so this would be very hard to do without a solver for semiring equations. However, such a solver would also depend on reflection machinery, bloating the dependency tree of the `Integer` module for people who do not care about it provably forming a ring.

Fortunately, since `ℤ` is opaque rather than abstract, a different module, say `Integer-ring`, can provide its own proofs, in an `opaque` block that unfolds the definition of `ℤ`:

```module Integer-ring where
open Integer

opaque
unfolding ℤ

distlℤ : ∀ x y z → x *ℤ (y +ℤ z) ≡ℤ x *ℤ y +ℤ x *ℤ z
distlℤ (a , b) (c , d) (e , f) = use-nat-solver where postulate
use-nat-solver
: a * (c + e) + b * (d + f) + (a * d + b * c + (a * f + b * e))
≡ a * c + b * d + (a * e + b * f) + (a * (d + f) + b * (c + e))
```

Since the definition of `distlℤ` is in an `opaque` block with an `unfolding ℤ` clause, it sees through the opacity of `ℤ`, and of all names unfolded by `ℤ`’s opaque block (see below).

## What actually unfolds?¶

When an `opaque` block is checked, Agda will compute ahead-of-time the set of names it is allowed to unfold. This set is per-block, not per-definition. An `unfolding` clause, if it mentions opaque names, will cause the unfolding sets associated with those names to be added to the current block.

The following illustrates the behaviour of these rules:

• Unfolding any name in an opaque block will cause any of the other names in that block to be unfolded as well. Example:

```module _ where private
opaque
x : Nat
y : Nat

x = 3
y = 4

opaque
unfolding x

_ : y ≡ 4
_ = refl
```

Here, even though only `x` was asked for, `y` is also available for unfolding.

• Since the unfolding sets brought in by clauses are associated with the block, unfolding is transitive:

```module _ where private
opaque
x : Nat
x = 3

opaque
unfolding x
y : Nat
y = 4 + x

opaque
unfolding y
_ : y ≡ 7
_ = refl
```
• Opaque blocks which are lexically nested can also unfold the names of their parent blocks, even if the name is not in scope when the child block is defined:

```module _ where private
opaque
x : Nat
x = 3

opaque
y : Nat
y = 4

_ : x ≡ 3
_ = refl

z : Nat
z = 5

opaque
unfolding y
_ : z ≡ 5
_ = refl
```

This is because the `x` and `z` are direct children of the same `opaque` block: the `opaque` block that defines `y` does not “split” its parent block.

Multiple unfolding clauses are supported, as well as unfolding more than one name per clause. The syntax for the latter is simply a space-separated list of names, which must refer to unambiguous functions:

```module _ where private
opaque
x : Nat
x = 3

opaque
y : Nat
y = 4

opaque
z : Nat
z = 5

opaque
unfolding x y
unfolding z

_ : x + y + z ≡ 12
_ = refl
```

Finally, `unfolding` clauses do not introduce new layout context, so that the following is legal: note that `y` appears to the left of `x`, but is still attached to the same `unfolding` clause. This allows the user their preference for how to lay out their unfolding sets:

```opaque
unfolding x
y
unfolding z

_ : x + y + z ≡ 12
_ = refl
```

Having an `unfolding` clause appear after other definitions, or outside of `opaque` blocks, is a syntax error.

Note that unlike `abstract` blocks, which are treated on a per-module basis, `opaque` blocks will only unfold names according to the rules above:

```module _ where private
opaque
x : Nat
x = 3

-- opaque
-- _ : x ≡ 3
-- _ = refl
-- Fails with: x != 3 of type Nat
```

## Unfolding in types¶

Note that unfolding clauses do not apply to the type signatures inside an `opaque` block. Much like for `abstract` blocks, this prevents leakage of implementation details, but it is also necessary to ensure that the types of names defined by the opaque block remain valid outside the opaque block. Consider:

```opaque
S : Set₁
S = Set

foo′ : S
foo′ = Nat

opaque
unfolding foo′

-- bar′ : foo′
-- bar′ = 123
-- Error: S should be a sort, but it isn't
```

If the definition of `bar′` were allowed, we would have ```bar′ : foo′``` in the context. Outside of the relevant opaque blocks, `foo′` is not a type, for `foo′ : S`, and `S` is not a sort. In cases like this, using an auxiliary definition whose type is a sort is required:

```-- Lift foo′ to a definition:
ty′ : Set
ty′ = foo′

bar′ : ty′
bar′ = 123
```

Since `ty′ : Set` is manifestly a well-formed type, even outside of this opaque block, there is no problem in adding `bar′ : ty′` to the context.

## Bibliography¶

Daniel Gratzer, Jonathan Sterling, Carlo Angiuli, Thierry Coquand, and Lars Birkedal; “Controlling unfolding in type theory”.