Slow elaboration of `List Nat` literals

[kmill]

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 :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.