[Agda] Proof seemingly takes far too long to check?

[depsterr]

Hi all, I've run into something quite unusual.

I've been trying to construct the reals and prove that their equality is an equivalence relation, however during the proof of symmetry I've ran into an issue. My proof type checks but the addition of one of the lemmas/helpers has forced me to set the agda heap size to 16GB and wait 37 minutes for it to typecheck.

The culprit is the following:

  a-b≡-b-a : ∀ (a b : ℚ) → a - b ≡ - (b - a)
  a-b≡-b-a a b =
    begin
      a - b
    ≡⟨⟩
      a + - b
    ≡˘⟨ ⁻¹-involutive (a + - b) ⟩
      - (- (a + - b))
    ≡⟨ cong -_ (neg-distrib-+ a (- b)) ⟩
      - (- a + - (- b))
    ≡⟨ cong (λ c → - (- a + c) ) (⁻¹-involutive b) ⟩
      - (- a + b)
    ≡⟨ cong -_ (+-comm (- a) b)  ⟩
      - (b + - a)
    ≡⟨⟩
      - (b - a)
    ∎

It seems that it's the usage of ⁻¹-involutive which slows it down, as it took no longer than 30 seconds before it was added (if you replace it with holes, for instance).

I'm not quite sure if this should be considered a bug or if I'm doing something wrong, certainly something this trivial shouldn't take so long?

I'm using agda built from source with `cabal install -foptimise-heavily` from commit `505464961f07f0991263708fd8cbf5f7ad12f53f` on master.

My standard library is version 1.7.1

I am using flags `--sage --without-K`

The full agda file can be found here https://githug.xyz/depsterr/constructive-analysis-in-agda/src/commit/345d7d11c12cc446764f7c1a9fe0afa0920632fb/src/Chapter2.agda

Hope to gain some insight into this, Cheers!