size of array literals

Stream: lean4

[Jun Yoshida]

I have some questions about array literals.
The following causes "(deterministic) timeout at 'whnf' ..." error:

example : #[0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15].size = 16 :=
  rfl
/-
(deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
-/

1. Why does this happen? I think the array literal #[...] is identical to [...].toArray which the kernel understands as a sequence of List.concat, right? So it may be slow, but timeout on 16 elements is surprising.

2. What is the reason not just setting #[...] to be defeq to Array.mk [...]? If it is the runtime performance, then we can use implemented_by.

3. In contrast to the above, the version below type checks within a second:

example : #[0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15].size = 16 := by
  rfl   -- `rfl` tactic is OK

Strangely, the generated term, which show_term tactic shows, looks almost identical to the above version.
I have no idea what is going on. Do you have any ideas?

[Mauricio Collares]

This is likely related to the issue being investigated in https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/What.20is.20the.20elaborator.20doing.20in.20this.20example

[Mauricio Collares]

Indeed, I can confirm that the fix there fixes this issue as well

[Mauricio Collares]

Can you add your testcase to lean4#2627?

[Jun Yoshida]

@Mauricio Collares I did it.