Deprecate and remove `Array` literal patterns

[Kha]

We added support for #[...] patterns early on for syntax match and didn't have a plan for supporting reasoning about it; we never used it in syntax match and still don't have a reasoning plan. Because of the complexity of even the current implementation, the most reasonable way to move forward is to deprecate and remove the syntax.

A perhaps naive regex '\| #\[ finds about a dozen uses in core and another dozen in the Mathlib tree:

$ git grep -E '\| #\['
src/Init/Meta.lean:  | #[]  => fn
src/Lean/Elab/Deriving/FromToJson.lean:    | #[], _ => ``(toJson $(quote ctorStr))
src/Lean/Elab/Deriving/FromToJson.lean:    | #[(x, t)], none => ``(mkObj [($(quote ctorStr), $(← mkToJson x t))])
src/Lean/Elab/Quotation.lean:  | #[]  => `(Unit.unit)
src/Lean/Elab/Quotation.lean:  | #[e] => return e
src/Lean/Elab/Quotation.lean:            | #[id] => pure id
src/Lean/Elab/Quotation.lean:      | #[] =>
src/Lean/Elab/Syntax.lean:      | #[]       => Parser.ensureConstantParserAlias aliasName; ``(ParserDescr.const $(quote aliasName))
src/Lean/Elab/Syntax.lean:      | #[p1]     => Parser.ensureUnaryParserAlias aliasName; ``(ParserDescr.unary $(quote aliasName) $p1)
src/Lean/Elab/Syntax.lean:      | #[p1, p2] => Parser.ensureBinaryParserAlias aliasName; ``(ParserDescr.binary $(quote aliasName) $p1 $p2)
src/Lean/Elab/Tactic/Simpa.lean:          let h := match xs with | #[h] | #[] => h | _ => unreachable!
src/Lean/Widget/TaggedText.lean:  | #[] => acc
tests/bench/liasolver.lean:  | #[]           => panic! "Cannot calculate GCD of empty list of coefficients"
tests/bench/liasolver.lean:  | #[(i, x)]     => x
tests/lean/match1.lean:| #[x]    => x
tests/lean/match1.lean:| #[x, y] => x + y
tests/lean/match1.lean:  | #[1, 2]    => 2
tests/lean/match1.lean:  | #[]        => 0
tests/lean/match1.lean:  | #[3, 4, 5] => 3
tests/lean/match1.lean.expected.out:  | #[1, 2] => 2
tests/lean/match1.lean.expected.out:  | #[] => 0
tests/lean/match1.lean.expected.out:  | #[3, 4, 5] => 3
tests/lean/run/matchArrayLit.lean:| #[]           => _
tests/lean/run/matchArrayLit.lean:| #[a₁]         => _
tests/lean/run/matchArrayLit.lean:| #[a₁, a₂, a₃] => _
$ grep -E '\| #\[' ../mathlib4 -r
../mathlib4/Cache/IO.lean:          runCmd (← getLeanTar) <| #[zipPath.toString, trace] ++
../mathlib4/Mathlib/RingTheory/WittVector/IsPoly.lean:    | #[x] => evalTactic (← `(tactic| refine IsPoly.ext (f := $fS) (g := $gS) ?_ ?_ ?_ _ $x))
../mathlib4/Mathlib/RingTheory/WittVector/IsPoly.lean:    | #[x, y] => evalTactic (← `(tactic| refine IsPoly₂.ext (f := $fS) (g := $gS) ?_ ?_ ?_ _ $x $y))
../mathlib4/Mathlib/Tactic/Linter/Lint.lean:      | #[id] =>
../mathlib4/lake-packages/std/Std/Tactic/Lint/Misc.lean:    | #[u] => some u
../mathlib4/lake-packages/std/Std/Tactic/RCases.lean:  | #[_, pat] => RCasesPatt.parse pat
../mathlib4/lake-packages/std/Std/Tactic/RCases.lean:  | #[] => pure $ RCasesPatt.tuple tk []
../mathlib4/lake-packages/std/Std/Tactic/Simpa.lean:        let h := match xs with | #[h] | #[] => h | _ => unreachable!
../mathlib4/lake-packages/aesop/Aesop/BuiltinRules/DestructProducts.lean:    | #[α, β] =>
../mathlib4/lake-packages/Cli/Cli/Basic.lean:              return some <| #[(inputFlagName, ⟨flag, ""⟩)] ++ tail
../mathlib4/lake-packages/proofwidgets/ProofWidgets/Data/Html.lean:  let `(term| #[ $[($as:str, $vs)],* ] ) := attrs | failure
../mathlib4/lake-packages/proofwidgets/ProofWidgets/Data/Html.lean:  let `(term| #[ $cs,* ]) := children | failure
../mathlib4/.lake/packages/batteries/Batteries/Tactic/Lint/Misc.lean:    | #[u] => some u
../mathlib4/.lake/packages/aesop/Aesop/BuiltinRules/DestructProducts.lean:    | #[α, β] =>
../mathlib4/.lake/packages/proofwidgets/ProofWidgets/Data/Html.lean:  -- into ``children ← `(term| #[a, Html.text " text "] ++ cs ++ #[d])``.
../mathlib4/.lake/packages/proofwidgets/ProofWidgets/Data/Html.lean:        csArrs ← csArrs.push <$> `(term| #[$csArr,*])
../mathlib4/.lake/packages/proofwidgets/ProofWidgets/Data/Html.lean:    csArrs ← csArrs.push <$> `(term| #[$csArr,*])
../mathlib4/.lake/packages/proofwidgets/ProofWidgets/Data/Html.lean:      | #[w], #[] => pure w
../mathlib4/.lake/packages/proofwidgets/ProofWidgets/Data/Html.lean:      `(term| #[$vs',*]))
../mathlib4/.lake/packages/importGraph/ImportGraph/Cli.lean:    | #[] => Std.HashSet.empty.insert "dot"
../mathlib4/.lake/packages/importGraph/ImportGraph/Cli.lean:  | #[] => writeFile "import_graph.dot" (outFiles["dot"]!)
../mathlib4/.lake/packages/Cli/Cli/Basic.lean:              return some <| #[(inputFlagName, ⟨flag, ""⟩)] ++ tail

[digama0]

Is it possible to make it expand to the same as ⟨[...]⟩ instead? I would hope that this happens automatically, assuming Array.mk (or is it Array.ofList now?) is implemented efficiently and used in the elaboration of #[...] literals. Alternatively, this could also be implemented by having #[...] elaborate to an Array.mk expression when it detects it is in pattern position. This would also fix the issue that mixing ⟨[...]⟩ and #[...] patterns in the same pattern match doesn't work.

As long as the compiler is able to avoid the performance cost of the naive implementation here, I think this would solve most of the reasoning issues. It's not clear to me if this will happen without any work though, and just removing array literal patterns without compiler support for the elaborated version could result in a performance regression otherwise.

[Kha]

I don't know how feasible that is, but if at all it would have to happen in the new code generator

[digama0]

I think it would still be better to have #[...] in pattern position mean ⟨[...]⟩ even if it just does the completely naive thing codegen-wise, and this ends up on the todo list for the new code generator.

(I am willing to write a PR for the pattern elaboration part of this, if accepted.)