Hole type inference very slow with long sequences of rewrites

[Sventimir]

The following example compiles in an instant (about 0.4s to be exact) :

import Data.Nat

lemma : S (2 * (S (2 * q))) = 4 * q + 3
lemma =
  rewrite plusZeroRightNeutral q in
  rewrite plusZeroRightNeutral (S (q + q)) in
  rewrite sym $ plusSuccRightSucc (S (q + q)) (q + q) in
  rewrite sym $ plusZeroRightNeutral (q + q + (q + q)) in
  rewrite plusSuccRightSucc (q + q + (q + q)) 0 in
  rewrite plusSuccRightSucc (q + q + (q + q)) 1 in
  rewrite plusSuccRightSucc (q + q + (q + q)) 2 in
  rewrite sym $ plusAssociative q q (q + q) in
  rewrite cong (\x => (q + (q + x))) $ sym (plusZeroRightNeutral q) in
  Refl

However, replace the final Refl with a hole and the compilation time increases dramatically. Actually it ran for 15 minutes, completely occupying one of the cores and consumed almost 60G of RAM before I decided to kill it:

$ time idris2 Report.idr -c ':q'
1/1: Building Report (Report.idr)
^C^C^C^C^C^C^C^C^C^C^C^C^C^C^C^C^C^C^C^C^C^C^C^C^C^C^C^C^C^C^C^C^C^C^C^C
real    15m56.294s
user    15m44.735s
sys     0m11.208s

it also took a significant amount of time to die.

The problem can be mittigated somewhat by extracting a part of the rewrite into a separate lemma, e.g.:

import Data.Nat

threeSuccLemma : (q : Nat) -> (S (S (S q))) = q + 3
threeSuccLemma q =
  rewrite sym $ plusZeroRightNeutral q in
  rewrite plusSuccRightSucc q 0 in
  rewrite plusSuccRightSucc q 1 in
  rewrite plusSuccRightSucc q 2 in
  rewrite plusZeroRightNeutral q in
  Refl

lemma : S (2 * (S (2 * q))) = 4 * q + 3
lemma =
  rewrite plusZeroRightNeutral q in
  rewrite plusZeroRightNeutral (S (q + q)) in
  rewrite sym $ plusSuccRightSucc (S (q + q)) (q + q) in
  rewrite threeSuccLemma (q + q + (q + q)) in
  rewrite sym $ plusAssociative q q (q + q) in
  rewrite cong (\x => (q + (q + x))) $ sym (plusZeroRightNeutral q) in
  Refl

In this example replacing the final Refl with a hole also increases compilation time, but only to about 2s.

Of course having a hole instead of a Refl allows us to delete some rewrites and see how it impacts behaviour. In my experience around 7 consecutive rewrites is a boundary beyond which compilation time and memory consumption grow rapidly with each next rewrite.

This is the behaviour I observe. What is the correct one, I don't know. I wish compilation time and memory consumption grew lineary with the number of steps in a proof, but perhaps it's unreasonable to expect that. In any case the sudden and rapid growth of compilation time is suspicious.

[ohad]

As a workaround for this (and similar) issues (which we should fix!), as well as a general programming-style, I recommend using equational reasoning instead of long chains of rewrites.

In this specific example, I would use the (different) proof:

import Syntax.PreorderReasoning
import Data.Nat

lemma : S (2 * (S (2 * q))) = 4 * q + 3
lemma = Calc $
  |~ 1 + (2 * (1 + (2 * q)))
  ~~ 1 + (2 + 2*(2*q)) ...(cong (1+) $ multDistributesOverPlusRight 2 1 _)
  ~~ 3 + 2*(2*q)       ...(Refl)
  ~~ 3 + 4*q           ...(cong (3+) $ multAssociative 2 2 _)
  ~~ 4 * q + 3         ...(plusCommutative _ _)

I discourage using long chains of rewrites because using many rewrites means we implicitly mutate the implicit type-checking goal. This kind of imperative programming makes it hard to read and understand what's going on. It also leads to a style where we do lots and lots of mindless and small rewrites, instead of a clearer high-level argument.

Equational reasoning, instead, exposes the implicit goal as the intermediate terms, and maybe choose clearer arguments. Spelling the implicit goals out can also help you omit arguments to the rewriting justification.

There's still lots more work left to do on equational reasoning, for example, better support for using congruence, and algebraic-simplification libraries.