Proving length of large array by rfl hangs

[vihdzp]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The following snippet summarizes the issue:

import Init.Prelude

structure MyVector (α : Type u) (n : Nat) where
  toArray : Array α
  size_eq : toArray.size = n

-- works almost instantly
example : MyVector Nat 32 :=
  ⟨#[1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1], rfl⟩

-- (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached
example : MyVector Nat 33 :=
  ⟨#[1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1], rfl⟩

Context

This is affecting batteries, as the v# notation doesn't work with vectors of length 33 or above. See Zulip.

Steps to Reproduce

1. Declare a Batteries vector with length 33 or above.

Expected behavior: The code typechecks with no issues

Actual behavior: The code hangs indefinitely

Versions

4.12.0-rc1

Additional Information

by simp works just fine in these proofs.

There's a seemingly related issue I've found relating to this code snippet:

import Init.Prelude

example : List Nat :=
  let l := [1]
  -- 32 copies
  [l[0], l[0], l[0], l[0], l[0], l[0], l[0], l[0], l[0], l[0], l[0], l[0], l[0], l[0], l[0], l[0], l[0], l[0], l[0], l[0], l[0], l[0], l[0], l[0], l[0], l[0], l[0], l[0], l[0], l[0], l[0], l[0]]

Adding one more instance of l[0] makes this typecheck noticeably slower. In my production code where l was some more complicated list, adding this extra entry made Lean eat all of my remaining 5GB of RAM (whereas it was running on only 1GB beforehand)

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[kmill]

Using by rfl instead of rfl somehow works around the issue:

example : MyVector Nat 33 :=
  ⟨#[1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1, 1], by rfl⟩

[kmill]

Some more context for by rfl working: I was wondering whether by rfl was fast because it used the kernel defeq, but the difference between the meta defeq working or not is just whether pending metavariables have been synthesized.

open Lean Meta Elab Command Term
elab tk:"check_defeq " ker?:(&"kernel ")? synth?:(&"synth ")? a:term " =?= " b:term : command => liftTermElabM do
  let mut x ← elabTerm a none
  let mut y ← elabTerm b none
  if synth?.isSome then
    synthesizeSyntheticMVarsUsingDefault
    x ← instantiateMVars x
    y ← instantiateMVars y
  let success ←
    if ker?.isSome then
      ofExceptKernelException (Kernel.isDefEq (← getEnv) {} x y)
    else
      isDefEq x y
  if success then
    logInfoAt tk "defeq"
  else
    logErrorAt tk "not defeq"

check_defeq kernel synth #[1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1].size =?= (33 : Nat)
-- defeq
check_defeq synth #[1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1].size =?= (33 : Nat)
-- defeq
check_defeq #[1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1].size =?= (33 : Nat)
-- error: timeout

Interestingly, the following succeeds

-- works
notation "z" => Nat.zero
check_defeq #[z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z].size =?= (33 : Nat)

This works for the MyVector case as well

-- works
notation "z" => Nat.zero
example : MyVector Nat 33 :=
  ⟨#[z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z,z], rfl⟩

But, strangely, using a local variable instead of this notation causes a timeout, so it's not just a matter of somehow avoiding OfNat instance problems.

-- times out
example (n : Nat) : MyVector Nat 33 :=
  ⟨#[n,n,n,n,n,n,n,n,n,n,n,n,n,n,n,n,n,n,n,n,n,n,n,n,n,n,n,n,n,n,n,n,n], rfl⟩