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

[nomeata]

Is it list syntax to blame, or does the same happen if you write it with many calls to List.cons?

[kmill]

I think it's some interaction between how long List syntax works and OfNat defaulting. For example, this is very fast:

def longList (n : Nat) : List Nat :=
  [n, n, n, n, n, n, n, n, n, n, ... 1000 n's ... , n]

As is

set_option maxRecDepth 5000
def longList (n : Nat) : List Nat :=
  2 :: 2 :: 2 :: 2 :: ... 930 2's ... :: 2 :: 2 :: []

(Thats the biggest the cons list can be without a true stack overflow.)

[dwrensha]

Elaborating List Float is slow too. Does that also go through OfNat?

set_option trace.profiler true in
def a : List Float := [
  0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5,
  0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5,
  0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5,
  0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5,
  0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5,
  0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5,
  0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5,
  0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5,
  0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5,
  0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5,
  0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5,
  0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5,
  0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5,
  0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5,
  0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5,
  0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5,
  0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5,
  0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5,
  0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5,
  0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5,
  0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5,
  0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5,
  0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5,
  0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5
]