Me and Yuchen Pei have been studying how JSON ARRAY indexing is done in MySQL. The details are posted here: MDEV-40822.

Yuchen has discovered cases where using ARRAY index for reads causes different query results from the same query not using the index. Looks like a bug (or maybe two). Sometimes one has to choose between being compatible with MySQL and producing correct query results.