Make it possible to limit how many times the syntactic equality shortcut is allowed to fail

[nad]

Agda's syntactic equality shortcut is employed recursively (unless --no-syntactic-equality is used). In the implementation of smalltt @AndrasKovacs takes a different approach:

In short, smalltt unification backtracks at most once on any path leading to a subterm ("sub-value" actually, since we recurse on values).

One can make Agda very slow by unifying two big terms that are almost syntactically identical, in the following way:

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Builtin.Nat
open import Agda.Builtin.Reflection
open import Agda.Builtin.Unit

data D : Set where
  c : D

data Delay-D : Set where
  now   : D → Delay-D
  later : Delay-D → Delay-D

f : Nat → D → Delay-D
f zero    x = now x
f (suc n) x = later (f n x)

n = 10_000

macro

  norm : {A : Set} → A → Term → TC ⊤
  norm t goal =
    withNormalisation true
      (bindTC (quoteTC t) λ t →
       unify goal t)

mutual

  α : D
  α = _

  x y : Delay-D
  x = norm (f n α)
  y = norm (f n c)

  _ : x ≡ y
  _ = refl

The time required to type-check the final definition seems to be at least quadratic in n, but roughly linear if --no-syntactic-equality is used (according to --profile=definitions).

I tried to implement something that resembles the approach taken by smalltt: in my implementation checkSyntacticEquality had two continuations, one for success and one for failure, and syntactic equality checking was turned off in the failure continuation. This worked fine for the code above, but led to a substantial slowdown for the standard library. Thus I'm leaning towards making the number of allowed failures configurable, following a suggestion by @AndrasKovacs.

[nad]

I added the option --syntactic-equality. From the changelog:

• The new option --syntactic-equality[=FUEL] can be used to limit how many times the syntactic equality shortcut is allowed to fail (see #5801).

  If FUEL is omitted, then the syntactic equality shortcut is enabled without any restrictions.

  If FUEL is given, then the syntactic equality shortcut is given FUEL units of fuel. The exact meaning of this is implementation-dependent, but successful uses of the shortcut do not affect the amount of fuel. Currently the fuel is decreased in the failure continuations of the implementation of the syntactic equality shortcut.

I experimented a little with this option for the standard library. Giving Agda 24 units of fuel seems to be comparable to not imposing any limit.

[JacquesCarette]

And 23 isn't enough? It would be fascinating to see which file fails at 23, and then figure out what causes Agda to consume so much fuel for that one example.

[nad]

The file Relation.Binary.HeterogeneousEquality.Quotients.Examples took more than 900 seconds to type-check (in one test) when I used the depth 2 (I think), and about 2 seconds when the depth was 24 for all files. I tried different depths, and settled for 24, but the numbers were similar for 23.

For Function.Related.TypeIsomorphisms.Solver there is a major difference between 1 and 2.