CREATE TABLE t1 (
  j JSON DEFAULT (CAST('[9,8,0,1]' AS JSON)),
  KEY mv_idx ((CAST(j->'$[*]' AS UNSIGNED ARRAY))));
INSERT INTO t1 VALUES();
DROP TABLE t1;