Slow elaboration of `List Nat` literals

Description

Long lists of natural number literals can take a long time to elaborate.

Context

Reported by @dwrensha on the Lean Zulip.

Steps to Reproduce

Given the following:

set_option trace.profiler true in
def dualEquationIds : List Nat :=
  [  1,   2,   3,   5,   4,   6,   7,  23,  28,  25,  31,  34,  24,  29,  30,  26,  32,  36,  27,  35,
    33,  37,   8,  13,  10,  16,  19,   9,  14,  15,  11,  17,  21,  12,  20,  18,  22,  39,  38,  40,
    41,  45,  43,  44,  42,  46, 255, 270, 260, 280, 290, 257, 273, 276, 263, 283, 298, 266, 294, 286,
   302, 256, 271, 272, 261, 281, 292, 262, 291, 282, 293, 258, 274, 278, 264, 284, 300, 268, 295, 288,
   305, 259, 277, 275, 279, 267, 287, 296, 304, 265, 299, 285, 301, 269, 303, 297, 289, 306, 203, 218,
   208, 228, 238, 205, 221, 224, 211, 231, 246, 214, 242, 234, 250, 204, 219, 220, 209, 229, 240, 210,
   239, 230, 241, 206, 222, 226, 212, 232, 248, 216, 243, 236, 253, 207, 225, 223, 227, 215, 235, 244,
   252, 213, 247, 233, 249, 217, 251, 245, 237, 254, 151, 166, 156, 176, 186, 153, 169, 172, 159, 179,
   194, 162, 190, 182, 198, 152, 167, 168, 157, 177, 188, 158, 187, 178, 189, 154, 170, 174, 160, 180,
   196, 164, 191, 184, 201, 155, 173, 171, 175, 163, 183, 192, 200, 161, 195, 181, 197, 165, 199, 193,
   185, 202,  99, 114, 104, 124, 134, 101, 117, 120, 107, 127, 142, 110, 138, 130, 146, 100, 115, 116,
   105, 125, 136, 106, 135, 126, 137, 102, 118, 122, 108, 128, 144, 112, 139, 132, 149, 103, 121, 119,
   123, 111, 131, 140, 148, 109, 143, 129, 145, 113, 147, 141, 133, 150,  47,  62,  52,  72,  82,  49,
    65,  68,  55,  75,  90,  58,  86,  78,  94,  48,  63,  64,  53,  73,  84,  54,  83,  74,  85,  50,
    66,  70,  56,  76,  92,  60,  87,  80,  97,  51,  69,  67,  71,  59,  79,  88,  96,  57,  91,  77,
    93,  61,  95,  89,  81,  98, 359, 364, 361, 367, 370, 360, 365, 366, 362, 368, 372, 363, 371, 369,
   373, 388, 378, 399, 385, 375, 395, 391, 381, 403, 407, 387, 377, 398, 384, 374, 394, 390, 380, 402,
   406, 389, 379, 400, 401, 386, 376, 396, 397, 392, 382, 404, 409, 393, 383, 408, 405, 410, 307, 312,
   309, 315, 318, 308, 313, 314, 310, 316, 320, 311, 319, 317, 321, 336, 326, 347, 333, 323, 343, 339,
   329, 351, 355, 335, 325, 346, 332, 322, 342, 338, 328, 350, 354, 337, 327, 348, 349, 334, 324, 344,
   345, 340, 330, 352, 357, 341, 331, 356, 353, 358,3050,3102,3065,3139,3176,3055,3112,3122,3075,3149,
  3210,3085,3193,3159,3227,3052,3105,3108,3068,3142,3184,3071,3180,3145,3188,3058,3115,3130,3078,3152,
  3218,3093,3197,3167,3242,3061,3126,3118,3134,3089,3163,3201,3237,3081,3214,3155,3222,3097,3232,3205,
  3171,3247,3051,3103,3104,3066,3140,3178,3067,3177,3141,3179,3056,3113,3124,3076,3150,3212,3087,3194,
  3161,3230,3057,3123,3114,3125,3086,3160,3195,3229,3077,3211,3151,3213,3088,3228,3196,3162,3231,3053,
  3106,3110,3069,3143,3186,3073,3181,3147,3191,3059,3116,3132,3079,3153,3220,3095,3198,3169,3245,3063,
  3127,3120,3137,3090,3164,3203,3239,3083,3215,3157,3225,3100,3233,3208,3174,3251,3054,3109,3107,3111,
  3072,3146,3182,3190,3070,3185,3144,3187,3074,3189,3183,3148,3192,3062,3119,3128,3136,3082,3156,3216,
  3224,3091,3202,3165,3240,3099,3206,3235,3173,3250,3060,3131,3117,3133,3094,3168,3199,3244,3080,3219,
  3154,3221,3096,3243,3200,3170,3246,3064,3135,3129,3121,3138,3098,3172,3234,3207,3249,3092,3238,3166,
  3204,3241,3084,3223,3217,3158,3226,3101,3248,3236,3209,3175,3252,2847,2899,2862,2936,2973,2852,2909,
  2919,2872,2946,3007,2882,2990,2956,3024,2849,2902,2905,2865,2939,2981,2868,2977,2942,2985,2855,2912,
  2927,2875,2949,3015,2890,2994,2964,3039,2858,2923,2915,2931,2886,2960,2998,3034,2878,3011,2952,3019,
  2894,3029,3002,2968,3044,2848,2900,2901,2863,2937,2975,2864,2974,2938,2976,2853,2910,2921,2873,2947,
  3009,2884,2991,2958,3027,2854,2920,2911,2922,2883,2957,2992,3026,2874,3008,2948,3010,2885,3025,2993,
  2959,3028,2850,2903,2907,2866,2940,2983,2870,2978,2944,2988,2856,2913,2929,2876,2950,3017,2892,2995,
  2966,3042,2860,2924,2917,2934,2887,2961,3000,3036,2880,3012,2954,3022,2897,3030,3005,2971,3048,2851,
  2906,2904,2908,2869,2943,2979,2987,2867,2982,2941,2984,2871,2986,2980,2945,2989,2859,2916,2925,2933,
  2879,2953,3013,3021,2888,2999,2962,3037,2896,3003,3032,2970,3047,2857,2928,2914,2930,2891,2965,2996,
  3041,2877,3016,2951,3018,2893,3040,2997,2967,3043,2861,2932,2926,2918,2935,2895,2969,3031,3004,3046,
  2889,3035,2963,3001,3038,2881,3020,3014,2955,3023,2898,3045,3033,3006,2972,3049,2644,2696,2659,2733,
  2770,2649,2706,2716,2669,2743,2804,2679,2787,2753,2821,2646,2699,2702,2662,2736,2778,2665,2774,2739,
  2782,2652,2709,2724,2672,2746,2812,2687,2791,2761,2836,2655,2720,2712,2728,2683,2757,2795,2831,2675,
  2808,2749,2816,2691,2826,2799,2765,2841,2645,2697,2698,2660,2734,2772,2661,2771,2735,2773,2650,2707,
  2718,2670,2744,2806,2681,2788,2755,2824,2651,2717,2708,2719,2680,2754,2789,2823,2671,2805,2745,2807,
  2682,2822,2790,2756,2825,2647,2700,2704,2663,2737,2780,2667,2775,2741,2785,2653,2710,2726,2673,2747,
  2814,2689,2792,2763,2839,2657,2721,2714,2731,2684,2758,2797,2833,2677,2809,2751,2819,2694,2827,2802,
  2768,2845,2648,2703,2701,2705,2666,2740,2776,2784,2664,2779,2738,2781,2668,2783,2777,2742,2786,2656]

Expected behavior: Elaborates quickly

Actual behavior: Takes 1.4s to elaborate

Versions

4.13.0-rc3 macOS m2

Additional Information

Doubling the length of the list takes 4.6s, and quadrupling it takes 19.4s, suggesting there is some superlinear algorithm in elaboration (the amount of time in seconds taken to elaborate a list of length n is roughly modeled by (0.0012 * n) ^ 2).

Related issue: #5502

Impact

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

Start by reproducing the List Nat literal example from the issue with set_option trace.profiler true on Lean 4.13.0-rc3, then compare the reported timings for the original, doubled, and quadrupled lists. Use related issue #5502 as context; done means long List Nat literals elaborate quickly without the reported superlinear scaling.