# Optimizing Canonical Structures

Quentin Vermande

► To cite this version:

Quentin Vermande. Optimizing Canonical Structures. UNIF 2025 - 39th International Workshop on Unification, Jul 2025, Birmingham, United Kingdom. hal-05148851

HAL Id: hal-05148851

https://inria.hal.science/hal-05148851v1

Submitted on 7 Jul 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Optimizing Canonical Structures

Quentin Vermande¹²

¹ Université Côte d'Azur, Inria, STAMP

² Université Claude Bernard Lyon 1, ENS de Lyon, LIP, CNRS, CASH

**Abstract**

While expanding Mathematical Components, a library of formalized mathematics for Rocq, we observed scalability issues in the latter’s unification algorithm. We found that the performance issue comes from the handling of Canonical Structures and proposed a patch, which has been integrated into Rocq 9.0.

# 1 Introduction

When formalizing mathematics in type theory, we need to express the fact that objects come equipped with characteristics in order to resolve symbol overloading and share theories. For example, notations and properties of rings can be shared between $\mathbb{Z}$, $\mathbb{Q}$, $\mathbb{C}[X]$, etc. More specifically, we can define an addition operator as a projection out of a record endowing the carrier type with the necessary structure (here a binary operator). When elaborating an expression such as $x + y$, there are several ways to infer the relevant record. The most common solution is through the use of typeclasses [3]. Rocq (recently renamed from Coq) offers another solution, where the record is inferred at unification time [4] using a mechanism known as Canonical Structures [2]. Let us consider, as a working example,

```haskell
Module AddType.
Structure type := Pack {
    carrier : Type;
    add : carrier -> carrier -> carrier
}.
End AddType.
```

In a nutshell, when encountering a unification problem of the form `AddType.carrier s ≡ nat`, the Canonical Structures mechanism would trigger and look for an instance of `AddType.type` on `nat`. This mechanism relies on a table that associates pairs of projections and names with structures. In our case, the algorithm would look for an entry on the pair (`AddType.carrier`, `nat`) in the table. If the search fails, then the algorithm fails. If the search succeeds and finds a structure `s'`, then the unification algorithm tries to unify `s` and `s`'.

This algorithm is very syntactical in nature. It takes the name that appears first in the term for which we need an instance of some structure, which we call the key, and uses it as an input in the Canonical Structures table. This enables the user to annotate terms to drive the resolution. This is required when there are two instances of the same structure on the same term. For instance, `nat` is ordered both by the usual order and by divisibility. The user can introduce an alias, say `nat_dvd` for `nat` and endow it with the divisibility order.

Mathematical Components, a large library of formalized mathematics, chose Canonical Structures as their representation of structures. This makes for an excellent stress test for them. Indeed, this is how we found that they had scalability issues. More precisely, three pull requests (namely #1169 (preorders), #1125 (semi-modules) and #1256 (monoids)) significantly increased the total compilation time of the library:
<table><thead><tr><th>preorders</th><th>semi-modules</th><th>monoids</th></tr></thead><tbody><tr><td>+21%</td><td>+100%</td><td>+17%</td></tr></tbody></table>

The problem is challenging because we are dealing with unification in presence of definitions and it is difficult to make correct decisions regarding which definition should be expanded. We propose an optimization of the unification algorithm in presence of Canonical Structures and integrate it into Rocq. Although unification is used everywhere, we managed to break almost no user code. In total, we had to change around 200 lines of user code out of the 4 million lines tested in Rocq’s CI. The work presented here was the subject of two pull requests on Rocq (accessible here and here), which were integrated as part of Rocq 9.0. We describe the performance issue in Section 2 and show how we solve it in Section 3.

## 2 Scalability Issues

The issue stems from the inheritance relations between structures. In a nutshell, facing a Canonical Structures problem of the form $S.carrier s ≡ t$ where s is obtained using some number n of coercions from the inheritance graph, the Canonical Structures algorithm goes through n unification of structures. Our claim is that at least n − 1 of these unifications are useless.

Let us consider semigroups (or SG for short). The defining property of semigroups is the associativity of their law, which we define first. Then we define the structure.

Definition associative {$T : Type$} ($op : T \rightarrow T \rightarrow T$) : Prop ::= 
forall x y z : T, $op$ x ($op$ y z) = $op$ ($op$ x y) z.

Module SG.

Structure type := Pack {
  carrier : Type;
  add : carrier -> carrier -> carrier;
  addA : associative add
}.
End SG.

There is an inheritance relation between `AddType.type` and `SG.type`. Indeed, any element of `SG.type` can be turned into an element of `AddType.type`, since we just need to forget the `addA` field. We say that `SG.type` inherits from `AddType.type`, and this relation is represented by a coercion:

`SG_to_AddType : SG.type -> AddType.type`

In practice, we would use a notation $x + y$ standing for `AddType.add x y` and we never want to use `SG.add`. A well-designed hierarchy would do this automatically, but for the sake of the example, let us restate the associativity property of semigroups so as to use `AddType.add x y`.

`addA : ∀(T : SG.type), 
        associative (AddType.add (SG_to_AddType T))`

Now, let us try to apply the associativity property on a sum of natural numbers. When unifying an expression of the form $n + m + k$ with the left-hand side of `addA`, the unification algorithm
would go through the following steps

$$
\begin{align*}
\texttt{AddType.carrier (SG\_to\_AddType ?x)} &\equiv \texttt{nat} \\
\texttt{SG\_to\_AddType ?x} &\equiv \texttt{AddType.Pack nat Nat.add} \\
\texttt{AddType.Pack (SG\_carrier ?x) (SG.add ?x)} &\equiv \texttt{AddType.Pack nat Nat.add} \\
\texttt{SG.carrier ?x} &\equiv \texttt{nat} \\
?x &\equiv \texttt{SG.Pack nat Nat.add} \\
&\qquad \texttt{Nat.add\_assoc} \\
\texttt{SG.add (SG.Pack nat Nat.add Nat.add\_assoc))} &\equiv \texttt{Nat.add} \\
\texttt{Nat.add} &\equiv \texttt{Nat.add}
\end{align*}
$$

The first unification problem is a Canonical Structures problem. The algorithm looks for the pair (`AddType.carrier`, `nat`) in its table, finds an instance `AddType.Pack nat Nat.add` and unifies it with `SG_to_AddType ?x`. The latter term reduces to the `AddType.Pack` constructor, so we start unifying the arguments. The problem `SG.carrier ?x ≡ nat` is another Canonical Structures problem, so we look for the pair (`SG.carrier`, `nat`) in the table which returns the instance `SG.Pack nat Nat.add Nat.addnell. We unify this with the unification variable ?x, which instantiates it. This completes the unification of the first arguments of `AddType.Pack`, so we start unifying the second arguments. The left-hand side reduces to `Nat.add` and the algorithm immediately succeeds.

However, checking that SG_to_AddType ?x and AddType.Pack nat Nat.add coincide on the AddType.add field has nothing to do with the initial unification problem which was about the AddType.carrier field. Reducing the term AddType.carrier (SG_to_AddType ?x) to Semigroup.carrier ?x without looking for Canonical Structures would be strictly better since the current algorithm reaches the unification problem Semigroup.carrier ?x ≡ nat anyway. This is an important inefficiency because structures tend to be large, and hence unifying instances takes a long time.

3 Optimization

With a lot of simplifications and oversights, we describe the initial unification algorithm in Algorithm 1 as a sequence of steps where the algorithm returns the first successful step. We present now three successive refinements Algorithm 2, Algorithm 3 and Algorithm 4 of Algorithm 1, leading to Algorithm 4 being our final proposal. In the rest of this section, we use the word "behavior" to describe the relation between the inputs and outputs of an algorithm. So two algorithms have the same behavior when they produce the same output when given the same input, without any considerations about their internal computations.

In the previous section, the initial unification problem

$$
\texttt{AddType.carrier (SG\_to\_AddType ?x)} \equiv \texttt{nat}
$$

leads to the problem SG.carrier ?x ≡ nat. We would like to reach the latter problem without producing other unnecessary unification problems. In other words, we would like to not launch Canonical Structures resolution when there is nothing to infer. We consider two situations where we skip Canonical Structures. If there is no unification variable in the argument of the projection, then there is obviously nothing to infer. Unifying the argument with a structure from the Canonical Structures table would not instantiate any unification variable and would either fail (e.g. in the case where the argument is a variable) or lead to the same unification problem anyway. The other case is the one we saw in the example: there is a unification
**Input:** s, t two terms

**Output:** A substitution of unification variables that makes s and t equal modulo $\alpha\beta\delta\iota\zeta$-equivalence.

1 if s or t is a unification variable **then**

2 | instantiate it with the other term

3 end

4 if s and t are applications of the same function to the same number of arguments **then**

5 | unify pairwise the arguments

6 end

7 if s or t is a projection applied to an instance of the corresponding structure **then**

8 | call the Canonical Structures algorithm

9 end

10 if t is reducible **then**

11 | reduce t and make a recursive call

12 else

13 | if s is reducible **then**

14 | reduce s and make a recursive call

15 end

16 end

**Algorithm 1:** Initial unification algorithm

**Input:** s, t two terms

**Output:** A substitution of unification variables that makes s and t equal modulo $\alpha\beta\delta\iota\zeta$-equivalence.

1 if s or t is a unification variable **then**

2 | instantiate it with the other term

3 end

4 if s and t are applications of the same function to the same number of arguments **then**

5 | unify pairwise the arguments

6 end

7 if s or t is a projection applied to an instance c of the corresponding structure, where c is not ground and does not reduce to a constructor **then**

8 | call the Canonical Structures algorithm

9 end

10 if t is reducible **then**

11 | reduce t and make a recursive call

12 else

13 | if s is reducible **then**

14 | reduce s and make a recursive call

15 end

16 end

**Algorithm 2:** First refinement

variable, but there is nothing to infer yet because the argument reduces to a constructor. We describe in Algorithm 2 this modified version of Algorithm 1.

Now, the unification algorithm is a very sensitive algorithm which is used pervasively, so any change in its behavior risks breaking the user codebase. The above proposed change is
no exception, and for good reasons. Algorithm 1 never backtracks on a reduction it does, and changing the order of reductions breaks everything. Hence, as a first approximation, we have to keep the reduction strategy from Algorithm 1 in Algorithm 2. In a nutshell, the strategy is to reduce the right-hand side if possible, and the left-hand side otherwise. But what if we have a unification problem which is a succeeding Canonical Structures problem with a projection on the left-hand side and reducing the right-hand-side leads to failing Canonical Structures problems? This may happen because after reduction, the head of the term is not a key in the Canonical Structures table anymore. For instance, if for some reason we had an alias nat' of nat on which there is the structure of SG.type, then Algorithm 2 would have the following trace

$$ 
\begin{align*}
AddType.carrier (SG\_to\_AddType ?x) &\equiv nat' \\
AddType.carrier (SG\_to\_AddType ?x) &\equiv nat \\
SG\_carrier ?x &\equiv nat
\end{align*}
$$

and fail because the pair (SG.carrier, nat) is not in the Canonical Structures Table. The solution we propose is to remember all the terms we encounter while reducing. Whenever we encounter a Canonical Structures problem, we first try solving the Canonical Structures problem with every term we registered while reducing the subject. We describe in Algorithm 3 this modification of Algorithm 2. Then, on the same problem as before, the trace of Algorithm 3 would be

$$ 
\begin{align*}
AddType.carrier (SG\_to\_AddType ?x) &\equiv nat' \\
AddType.carrier (SG\_to\_AddType ?x) &\equiv nat \\
SG\_carrier ?x &\equiv nat \\
?x &\equiv SG.Pack nat' Nat.add
\end{align*}
$$

because we first look for the pair (SG.carrier, nat') in the Canonical Structures table. Now, Algorithm 3 has a behavior that is close enough to that of Algorithm 1 to break very little the user codebase. But Algorithm 3 is too slow because it is inefficient to keep reducing the right-hand side until it is in weak head normal form and then reduce the left-hand side, reach the proper Canonical Structures problem and observe that the first key matches. There is a very specific case where we want to reduce the left-hand side first. This is the case of a Canonical Structures problem we wish to skip but that would have succeeded and with the projection on the left-hand side. In this situation, the way we expect the unification algorithm to succeed is that it reaches a proper Canonical Structures problem after reducing the left-hand side and this Canonical Structures problem has a solution. This works often enough that it is faster to reduce the left-hand side right away. However, if it does not, we need to backtrack and reduce the right-hand side.

Another easy optimization we can do is that when reducing a term, say the right-hand side, there is no point in checking all the corresponding keys again, since if there is a projection on the other side, the keys were checked at the iteration of the algorithm preceding the reduction. So we add a flag to remember which side was last reduced and use it to skip checking keys when possible. We describe in Algorithm 4 the modification of Algorithm 3 with these optimizations. Algorithm 4 and Algorithm 3 have the same behavior, so we did not introduce any difference with respect to the user code, and is fast enough to be integrated into Rocq.

As a nice side effect, Algorithm 3 (and hence Algorithm 4) is more predictable than Algorithm 1 and Algorithm 2. Indeed, by remembering information on what was reduced, we ensure that Canonical Structures get solved using what the user gave us, instead of potentially reducing terms and then discovering a projection on the other side of the equation.
**Input:** s, t two terms, $lu \in \{None, LHS, RHS\}$, ks and kt queues of names

**Output:** A substitution of unification variables that makes s and t equal modulo $\alpha\beta\delta\iota\zeta$-equivalence.

1 if $lu \neq RHS$ then

2 | add the key of s to ks

3 end

4 if $lu \neq LHS$ then

5 | add the key of t to kt

6 end

7 if s or t is a unification variable then

8 | instantiate it with the other term

9 end

10 if s and t are applications of the same function to the same number of arguments then

11 | unify pairwise the arguments

12 end

13 if s is a projection applied to an instance c of the corresponding structure, where c is not ground and does not reduce to a constructor then

14 | call the Canonical Structures algorithm, going through all the keys in kt

15 end

16 if t is a projection applied to an instance c of the corresponding structure, where c is not ground and does not reduce to a constructor then

17 | call the Canonical Structures algorithm, going through all the keys in ks

18 end

19 if t is reducible then

20 | $lu \leftarrow RHS$

21 | reduce t and make a recursive call

22 else

23 | if s is reducible then

24 | $lu \leftarrow LHS$

25 | reduce s and make a recursive call

26 end

27 end

**Algorithm 3:** Second refinement

## 4 Conclusion

Changing Rocq's unification algorithm from Algorithm 1 to Algorithm 4 leads to very few breakages, as we had to update 200 lines of code out of 4 million. Regarding performance, Mathematical Components, which relies heavily on Canonical Structures, received a huge performance boost, with the compilation time of the `rocq-mathcomp-ssreflect` package being reduced by almost 14% (starting from 106s). Some packages got slower, but still within the range considered as noise by the Rocq developers. For instance, the `rocq-equations` package's compilation time was increased by a little less than 3% (starting from 8s). This was to be expected since we do some extra work by registering keys which are not used outside of the Canonical Structures algorithm. Regarding the three very slow pull requests mentioned in the introduction, we obtain the following results (comparing with the `master` branch of `MathComp`):
<table><thead><tr><th></th><th>preorders</th><th>semi-modules</th><th>monoids</th></tr></thead><tbody><tr><td>without optimization</td><td>+21%</td><td>+100%</td><td>+17%</td></tr><tr><td>with optimization</td><td>+6%</td><td>+6%</td><td>+19%</td></tr></tbody></table>

It is pretty surprising that we did not save time on the monoids pull request. Profiling Rocq code is somewhat difficult, but the increase in compilation time seems mostly due to Hierarchy Builder [1] which must declare more Rocq objects due to the changes introduced by the pull request.

From a memory consumption point of view, we did not observe any significant increase.

There are still performance issues related to structures (c.f. #1365), but they are not due to Canonical Structures, so we leave them for future work.

## References

[1] Cyril Cohen, Kazuhiko Sakaguchi, and Enrico Tassi. Hierarchy Builder: Algebraic hierarchies Made Easy in Coq with Elpi. In Zena M. Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), volume 167 of Leibniz International Proceedings in Informatics (LIPIcs), pages 34:1–34:21, Dagstuhl, Germany, 2020. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.

[2] Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, and Derek Dreyer. How to make ad hoc proof automation less ad hoc. SIGPLAN Not., 46(9):163–175, September 2011.

[3] Matthieu Sozeau and Nicolas Oury. First-class type classes. In Otmane Ait Mohamed, César Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, pages 278–293, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg.

[4] Beta Ziliani and Matthieu Sozeau. A comprehensible guide to a new unifier for cic including universe polymorphism and overloading. Journal of Functional Programming, 27:e10, 2017.
**Input:** s, t two terms, $lu \in \{None, LHS, RHS\}$, ks and kt queues of names

**Output:** A substitution of unification variables that makes s and t equal modulo $\alpha\beta\delta\iota\zeta$-equivalence.

1 if $lu \neq RHS$ then

2 | add the key of s to ks

3 end

4 if $lu \neq LHS$ then

5 | add the key of t to kt

6 end

7 $csLHS \leftarrow false$ if s or t is a unification variable then

8 | instantiate it with the other term

9 end

10 if s and t are applications of the same function to the same number of arguments then

11 | unify pairwise the arguments

12 end

13 if s is a projection applied to an instance c of the corresponding structure then

14 | if $lu = RHS$ then

15 | call the Canonical Structures algorithm with s and t

16 else

17 | call the Canonical Structures algorithm, going through all the keys in kt

18 end

19 if the previous call succeeds and c is either ground or reduces to a constructor then

20 | $csLHS \leftarrow true$

21 else

22 | return the previous success

23 end

24 end

25 if t is a projection applied to an instance c of the corresponding structure, where c is not ground and does not reduce to a constructor then

26 | if $lu = LHS$ then

27 | call the Canonical Structures algorithm with s and t

28 else

29 | call the Canonical Structures algorithm, going through all the keys in ks

30 end

31 end

32 if $csLHS = true$ and s is reducible then

33 | $lu \leftarrow LHS$

34 | reduce s and make a recursive call

35 end

36 if t is reducible then

37 | $lu \leftarrow RHS$

38 | reduce t and make a recursive call

39 else

40 | if $csLHS = false$ and s is reducible then

41 | $lu \leftarrow LHS$

42 | reduce s and make a recursive call

43 end

44 end

**Algorithm 4:** Third refinement