rustyfi-lang 0.1.4

Abstract syntax tree, elaboration, evaluator, and primitives for SATySFi
Documentation
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
1325
1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
1385
1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
1400
1401
1402
1403
1404
1405
1406
1407
1408
1409
1410
1411
1412
1413
1414
1415
1416
1417
1418
1419
1420
1421
1422
1423
1424
1425
1426
1427
1428
1429
1430
1431
1432
1433
1434
1435
1436
1437
1438
1439
1440
1441
1442
1443
1444
1445
1446
1447
1448
1449
1450
1451
1452
1453
1454
1455
1456
1457
1458
1459
1460
1461
1462
1463
1464
1465
1466
1467
1468
1469
1470
1471
1472
1473
1474
1475
1476
1477
1478
1479
1480
1481
1482
1483
1484
1485
1486
1487
1488
1489
1490
1491
1492
1493
1494
1495
1496
1497
1498
1499
1500
1501
1502
1503
1504
1505
1506
1507
1508
1509
1510
1511
1512
1513
1514
1515
1516
1517
1518
1519
1520
1521
1522
1523
1524
1525
1526
1527
1528
1529
1530
1531
1532
1533
1534
1535
1536
1537
1538
1539
1540
1541
1542
1543
1544
1545
1546
1547
1548
1549
1550
1551
1552
1553
1554
1555
1556
1557
1558
1559
1560
1561
1562
1563
1564
1565
1566
1567
1568
1569
1570
1571
1572
1573
1574
1575
1576
1577
1578
1579
1580
1581
1582
1583
1584
1585
1586
1587
1588
1589
1590
1591
1592
1593
1594
1595
1596
1597
1598
1599
1600
1601
1602
1603
1604
1605
1606
1607
1608
1609
1610
1611
1612
1613
1614
1615
1616
1617
1618
1619
1620
1621
1622
1623
1624
1625
1626
1627
1628
1629
1630
1631
1632
1633
1634
1635
1636
1637
1638
1639
1640
1641
1642
1643
1644
1645
1646
1647
1648
1649
1650
1651
1652
1653
1654
1655
1656
1657
1658
1659
1660
1661
1662
1663
1664
1665
1666
1667
1668
1669
1670
1671
1672
1673
1674
1675
1676
1677
1678
1679
1680
1681
1682
1683
1684
1685
1686
1687
1688
1689
1690
1691
1692
1693
1694
1695
1696
1697
1698
1699
1700
1701
1702
1703
1704
1705
1706
1707
1708
1709
1710
1711
1712
1713
1714
1715
1716
1717
1718
1719
1720
1721
1722
1723
1724
1725
1726
1727
1728
1729
1730
1731
1732
1733
1734
1735
1736
1737
1738
1739
1740
1741
1742
1743
1744
1745
1746
1747
1748
1749
1750
1751
1752
1753
1754
1755
1756
1757
1758
1759
1760
1761
1762
1763
1764
1765
1766
1767
1768
1769
1770
1771
1772
1773
1774
1775
1776
1777
1778
1779
1780
1781
1782
1783
1784
1785
1786
1787
1788
1789
1790
1791
1792
1793
1794
1795
1796
1797
1798
1799
1800
1801
1802
1803
1804
1805
1806
1807
1808
1809
1810
1811
1812
1813
1814
1815
1816
1817
1818
1819
1820
1821
1822
1823
1824
1825
1826
1827
1828
1829
1830
1831
1832
1833
1834
1835
1836
1837
1838
1839
1840
1841
1842
1843
1844
1845
1846
1847
1848
1849
1850
1851
1852
1853
1854
1855
1856
1857
1858
1859
1860
1861
1862
1863
1864
1865
1866
1867
1868
1869
1870
1871
1872
1873
1874
1875
1876
1877
1878
1879
1880
1881
1882
1883
1884
1885
1886
1887
1888
1889
1890
1891
1892
1893
1894
1895
1896
1897
1898
1899
1900
1901
1902
1903
1904
1905
1906
1907
1908
1909
1910
1911
1912
1913
1914
1915
1916
1917
1918
1919
1920
1921
1922
1923
1924
1925
1926
1927
1928
1929
1930
1931
1932
1933
1934
1935
1936
1937
1938
1939
1940
1941
1942
1943
1944
1945
1946
1947
1948
1949
1950
1951
1952
1953
1954
1955
1956
1957
1958
1959
1960
1961
1962
1963
1964
1965
1966
1967
1968
1969
1970
1971
1972
1973
1974
1975
1976
1977
1978
1979
1980
1981
1982
1983
1984
1985
1986
1987
1988
1989
1990
1991
1992
1993
1994
1995
1996
1997
1998
1999
2000
2001
2002
2003
2004
2005
2006
2007
2008
2009
2010
2011
2012
2013
2014
2015
2016
2017
2018
2019
2020
2021
2022
2023
2024
2025
2026
2027
2028
2029
2030
2031
2032
2033
2034
2035
2036
2037
2038
2039
2040
2041
2042
2043
2044
2045
2046
2047
2048
2049
2050
2051
2052
2053
2054
2055
2056
2057
2058
2059
2060
2061
2062
2063
2064
2065
2066
2067
2068
2069
2070
2071
2072
2073
2074
2075
2076
2077
2078
2079
2080
2081
2082
2083
2084
2085
2086
2087
2088
2089
2090
2091
2092
2093
2094
2095
2096
2097
2098
2099
2100
2101
2102
2103
2104
2105
2106
2107
2108
2109
2110
2111
2112
2113
2114
2115
2116
2117
2118
2119
2120
2121
2122
2123
2124
2125
2126
2127
2128
2129
2130
2131
2132
2133
2134
2135
2136
2137
2138
2139
2140
2141
2142
2143
2144
2145
2146
2147
2148
2149
2150
2151
2152
2153
2154
2155
2156
2157
2158
2159
2160
2161
2162
2163
2164
2165
2166
2167
2168
2169
2170
2171
2172
2173
2174
2175
2176
2177
2178
2179
2180
2181
2182
2183
2184
2185
2186
2187
2188
2189
2190
2191
2192
2193
2194
2195
2196
2197
2198
2199
2200
2201
2202
2203
2204
2205
2206
2207
2208
2209
2210
2211
2212
2213
2214
2215
2216
2217
2218
2219
2220
2221
2222
2223
2224
2225
2226
2227
2228
2229
2230
2231
2232
2233
2234
2235
2236
2237
2238
2239
2240
2241
2242
2243
2244
2245
2246
2247
2248
2249
2250
2251
2252
2253
2254
2255
2256
2257
2258
2259
2260
2261
2262
2263
2264
2265
2266
2267
2268
2269
2270
2271
2272
2273
2274
2275
2276
2277
2278
2279
2280
2281
2282
2283
2284
2285
2286
2287
2288
2289
2290
2291
2292
2293
2294
2295
2296
2297
2298
2299
2300
2301
2302
2303
2304
2305
2306
2307
2308
2309
2310
2311
2312
2313
2314
2315
2316
2317
2318
2319
2320
2321
2322
2323
2324
2325
2326
2327
2328
2329
2330
2331
2332
2333
2334
2335
2336
2337
2338
2339
2340
2341
2342
2343
2344
2345
2346
2347
2348
2349
2350
2351
2352
2353
2354
2355
2356
2357
2358
2359
2360
2361
2362
2363
2364
2365
2366
2367
2368
2369
2370
2371
2372
2373
2374
2375
2376
2377
2378
2379
2380
2381
2382
2383
2384
2385
2386
2387
2388
2389
2390
2391
2392
2393
2394
2395
2396
2397
2398
2399
2400
2401
2402
2403
2404
2405
2406
2407
2408
2409
2410
2411
2412
2413
2414
2415
2416
2417
2418
2419
2420
2421
2422
2423
2424
2425
2426
2427
2428
2429
2430
2431
2432
2433
2434
2435
2436
2437
2438
2439
2440
2441
2442
2443
2444
2445
2446
2447
2448
2449
2450
2451
2452
2453
2454
2455
2456
2457
2458
2459
2460
2461
2462
2463
2464
2465
2466
2467
2468
2469
2470
2471
2472
2473
2474
2475
2476
2477
2478
2479
2480
2481
2482
2483
2484
2485
2486
2487
2488
2489
2490
2491
2492
2493
2494
2495
2496
2497
2498
2499
2500
2501
2502
2503
2504
2505
2506
2507
2508
2509
2510
2511
2512
2513
2514
2515
2516
2517
2518
2519
2520
2521
2522
2523
2524
2525
2526
2527
2528
2529
2530
2531
2532
2533
2534
2535
2536
2537
2538
2539
2540
2541
2542
2543
2544
2545
2546
2547
2548
2549
2550
2551
2552
2553
2554
2555
2556
2557
2558
2559
2560
2561
2562
2563
2564
2565
2566
2567
2568
2569
2570
2571
2572
2573
2574
2575
2576
2577
2578
2579
2580
2581
2582
2583
2584
2585
2586
2587
2588
2589
2590
2591
2592
2593
2594
2595
2596
2597
2598
2599
2600
2601
2602
2603
2604
2605
2606
2607
2608
2609
2610
2611
2612
2613
2614
2615
2616
2617
2618
2619
2620
2621
2622
2623
2624
2625
2626
2627
2628
2629
2630
2631
2632
2633
2634
2635
2636
2637
2638
2639
2640
2641
2642
2643
2644
2645
2646
2647
2648
2649
2650
2651
2652
2653
2654
2655
2656
2657
2658
2659
2660
2661
2662
2663
2664
2665
2666
2667
2668
2669
2670
2671
2672
2673
2674
2675
2676
2677
2678
2679
2680
2681
2682
2683
2684
2685
2686
2687
2688
2689
2690
2691
2692
2693
2694
2695
2696
2697
2698
2699
2700
2701
2702
2703
2704
2705
2706
2707
2708
2709
2710
2711
2712
2713
2714
2715
2716
2717
2718
2719
2720
2721
2722
2723
2724
2725
2726
2727
2728
2729
2730
2731
2732
2733
2734
2735
2736
2737
2738
2739
2740
2741
2742
2743
2744
2745
2746
2747
2748
2749
2750
2751
2752
2753
2754
2755
2756
2757
2758
2759
2760
2761
2762
2763
2764
2765
2766
2767
2768
2769
2770
2771
2772
2773
2774
2775
2776
2777
2778
2779
2780
2781
2782
2783
2784
2785
2786
2787
2788
2789
2790
2791
2792
2793
2794
2795
2796
2797
2798
2799
2800
2801
2802
2803
2804
2805
2806
2807
2808
2809
2810
2811
2812
2813
2814
2815
2816
2817
2818
2819
2820
2821
2822
2823
2824
2825
2826
2827
2828
2829
2830
2831
2832
2833
2834
2835
2836
2837
2838
2839
2840
2841
2842
2843
2844
2845
2846
2847
2848
2849
2850
2851
2852
2853
2854
2855
2856
2857
2858
2859
2860
2861
2862
2863
2864
2865
2866
2867
2868
2869
2870
2871
2872
2873
2874
2875
2876
2877
2878
2879
2880
2881
2882
2883
2884
2885
2886
2887
2888
2889
2890
2891
2892
2893
2894
2895
2896
2897
2898
2899
2900
2901
2902
2903
2904
2905
2906
2907
2908
2909
2910
2911
2912
2913
2914
2915
2916
2917
2918
2919
2920
2921
2922
2923
2924
2925
2926
2927
2928
2929
2930
2931
2932
2933
2934
2935
2936
2937
2938
2939
2940
2941
2942
2943
2944
2945
2946
2947
2948
2949
2950
2951
2952
2953
2954
2955
2956
2957
2958
2959
2960
2961
2962
2963
2964
2965
2966
2967
2968
2969
2970
2971
2972
2973
2974
2975
2976
2977
2978
2979
2980
2981
2982
2983
2984
2985
2986
2987
2988
2989
2990
2991
2992
2993
2994
2995
2996
2997
2998
2999
3000
3001
3002
3003
3004
3005
3006
3007
3008
3009
3010
3011
3012
3013
3014
3015
3016
3017
3018
3019
3020
3021
3022
3023
3024
3025
3026
3027
3028
3029
3030
3031
3032
3033
3034
3035
3036
3037
3038
3039
3040
3041
3042
3043
3044
3045
3046
3047
3048
3049
3050
3051
3052
3053
3054
3055
3056
3057
3058
3059
3060
3061
3062
3063
3064
3065
3066
3067
3068
3069
3070
3071
3072
3073
3074
3075
3076
3077
3078
3079
3080
3081
3082
3083
3084
3085
3086
3087
3088
3089
3090
3091
3092
3093
3094
3095
3096
3097
3098
3099
3100
3101
3102
3103
3104
3105
3106
3107
3108
3109
3110
3111
3112
3113
3114
3115
3116
3117
3118
3119
3120
3121
3122
3123
3124
3125
3126
3127
3128
3129
3130
3131
3132
3133
3134
3135
3136
3137
3138
3139
3140
3141
3142
3143
3144
3145
3146
3147
3148
3149
3150
3151
3152
3153
3154
3155
3156
3157
3158
3159
3160
3161
3162
3163
3164
3165
3166
3167
3168
3169
3170
3171
3172
3173
3174
3175
3176
3177
3178
3179
3180
3181
3182
3183
3184
3185
3186
3187
3188
3189
3190
3191
3192
3193
3194
3195
3196
3197
3198
3199
3200
3201
3202
3203
3204
3205
3206
3207
3208
3209
3210
3211
3212
3213
3214
3215
3216
3217
3218
3219
3220
3221
3222
3223
3224
3225
3226
3227
3228
3229
3230
3231
3232
3233
3234
3235
3236
3237
3238
3239
3240
3241
3242
3243
3244
3245
3246
3247
3248
3249
3250
3251
3252
3253
3254
3255
3256
3257
3258
3259
3260
3261
3262
3263
3264
3265
3266
3267
3268
3269
3270
3271
3272
3273
3274
3275
3276
3277
3278
3279
3280
3281
3282
3283
3284
3285
3286
3287
3288
3289
3290
3291
3292
3293
3294
3295
3296
3297
3298
3299
3300
3301
3302
3303
3304
3305
3306
3307
3308
3309
3310
3311
3312
3313
3314
3315
3316
3317
3318
3319
3320
3321
3322
3323
3324
3325
3326
3327
3328
3329
3330
3331
3332
3333
3334
3335
3336
3337
3338
3339
3340
3341
3342
3343
3344
3345
3346
3347
3348
3349
3350
3351
3352
3353
3354
3355
3356
3357
3358
3359
3360
3361
3362
3363
3364
3365
3366
3367
3368
3369
3370
3371
3372
3373
3374
3375
3376
3377
3378
3379
3380
3381
3382
3383
3384
3385
3386
3387
3388
3389
3390
3391
3392
3393
3394
3395
3396
3397
3398
3399
3400
3401
3402
3403
3404
3405
3406
3407
3408
3409
3410
3411
3412
3413
3414
3415
3416
3417
3418
3419
3420
3421
3422
3423
3424
3425
3426
3427
3428
3429
3430
3431
3432
3433
3434
3435
3436
3437
3438
3439
3440
3441
3442
3443
3444
3445
3446
3447
3448
3449
3450
3451
3452
3453
3454
3455
3456
3457
3458
3459
3460
3461
3462
3463
3464
3465
3466
3467
3468
3469
3470
3471
3472
3473
3474
3475
3476
3477
3478
3479
3480
3481
3482
3483
3484
3485
3486
3487
3488
3489
3490
3491
3492
3493
3494
3495
3496
3497
3498
3499
3500
3501
3502
3503
3504
3505
3506
3507
3508
3509
3510
3511
3512
3513
3514
3515
3516
3517
3518
3519
3520
3521
3522
3523
3524
3525
3526
3527
3528
3529
3530
3531
3532
3533
3534
3535
3536
3537
3538
3539
3540
3541
3542
3543
3544
3545
3546
3547
3548
3549
3550
3551
3552
3553
3554
3555
3556
3557
3558
3559
3560
3561
3562
3563
3564
3565
3566
3567
3568
3569
3570
3571
3572
3573
3574
3575
3576
3577
3578
3579
3580
3581
3582
3583
3584
3585
3586
3587
3588
3589
3590
3591
3592
3593
3594
3595
3596
3597
3598
3599
3600
3601
3602
3603
3604
3605
3606
3607
3608
3609
3610
3611
3612
3613
3614
3615
3616
3617
3618
3619
3620
3621
3622
3623
3624
3625
3626
3627
3628
3629
3630
3631
3632
3633
3634
3635
3636
3637
3638
3639
3640
3641
3642
3643
3644
3645
3646
3647
3648
3649
3650
3651
3652
3653
3654
3655
3656
3657
3658
3659
3660
3661
3662
3663
3664
3665
3666
3667
3668
3669
3670
3671
3672
3673
3674
3675
3676
3677
3678
3679
3680
3681
3682
3683
3684
3685
3686
3687
3688
3689
3690
3691
3692
3693
3694
3695
3696
3697
3698
3699
3700
3701
3702
3703
3704
3705
3706
3707
3708
3709
3710
3711
3712
3713
3714
3715
3716
3717
3718
3719
3720
3721
3722
3723
3724
3725
3726
3727
3728
3729
3730
3731
3732
3733
3734
3735
3736
3737
3738
3739
3740
3741
3742
3743
3744
3745
3746
3747
3748
3749
3750
3751
3752
3753
3754
3755
3756
3757
3758
3759
3760
3761
3762
3763
3764
3765
3766
3767
3768
3769
3770
3771
3772
3773
3774
3775
3776
3777
3778
3779
3780
3781
3782
3783
3784
3785
3786
3787
3788
3789
3790
3791
3792
3793
3794
3795
3796
3797
3798
3799
3800
3801
3802
3803
3804
3805
3806
3807
3808
3809
3810
3811
3812
3813
3814
3815
3816
3817
3818
3819
3820
3821
3822
3823
3824
3825
3826
3827
3828
3829
3830
3831
3832
3833
3834
3835
3836
3837
3838
3839
3840
3841
3842
3843
3844
3845
3846
3847
3848
3849
3850
3851
3852
3853
3854
3855
3856
3857
3858
3859
3860
3861
3862
3863
3864
3865
3866
3867
3868
3869
3870
3871
3872
3873
3874
3875
3876
3877
3878
3879
3880
3881
3882
3883
3884
3885
3886
3887
3888
3889
3890
3891
3892
3893
3894
3895
3896
3897
3898
3899
3900
3901
3902
3903
3904
3905
3906
3907
3908
3909
3910
3911
3912
3913
3914
3915
3916
3917
3918
3919
3920
3921
3922
3923
3924
3925
3926
3927
3928
3929
3930
3931
3932
3933
3934
3935
3936
3937
3938
3939
3940
3941
3942
3943
3944
3945
3946
3947
3948
3949
3950
3951
3952
3953
3954
3955
3956
3957
3958
3959
3960
3961
3962
3963
3964
3965
3966
3967
3968
3969
3970
3971
3972
3973
3974
3975
3976
3977
3978
3979
3980
3981
3982
3983
3984
3985
3986
3987
3988
3989
3990
3991
3992
3993
3994
3995
3996
3997
3998
3999
4000
4001
4002
4003
4004
4005
4006
4007
4008
4009
4010
4011
4012
4013
4014
4015
4016
4017
4018
4019
4020
4021
4022
4023
4024
4025
4026
4027
4028
4029
4030
4031
4032
4033
4034
4035
4036
4037
4038
4039
4040
4041
4042
4043
4044
4045
4046
4047
4048
4049
4050
4051
4052
4053
4054
4055
4056
4057
4058
4059
4060
4061
4062
4063
4064
4065
4066
4067
4068
4069
4070
4071
4072
4073
4074
4075
4076
4077
4078
4079
4080
4081
4082
4083
4084
4085
4086
4087
4088
4089
4090
4091
4092
4093
4094
4095
4096
4097
4098
4099
4100
4101
4102
4103
4104
4105
4106
4107
4108
4109
4110
4111
4112
4113
4114
4115
4116
4117
4118
4119
4120
4121
4122
4123
4124
4125
4126
4127
4128
4129
4130
4131
4132
4133
4134
4135
4136
4137
4138
4139
4140
4141
4142
4143
4144
4145
4146
4147
4148
4149
4150
4151
4152
4153
4154
4155
4156
4157
4158
4159
4160
4161
4162
4163
4164
4165
4166
//! The boundary TYPE adapter for a `V0_0` dependency spliced into
//! a `V0_1` program.
//!
//! The compile-time version-scope splice handles the *value* half of the forked-name guard (a spliced
//! binding's RHS runs inside `Ast::VersionScope(V0_0, _)`, so a
//! version-forked *primitive* resolves against its own version). The *type*
//! half stays conservative: `lib.rs`'s `compile_document_v1_with_trials`
//! hard-rejects a dependency that textually names ANY version-forked type
//! (`typecheck::forked_type_names`) anywhere in its `prelude`. This module turns
//! exactly ONE of those rejections into an acceptance: `math` (0.0.6's
//! math-text type) is representationally IDENTICAL to 0.1's `math-text` —
//! both lower to `BaseType::MathText` (`typecheck.rs`'s `name_to_mono`) and
//! share the same runtime `Value::MathText`/`Value::Math` representation
//! (`value.rs:39-56`, not forked at all) — so a `math` reference RELABELS to
//! `math-text` with **zero runtime value coercion**. Every other forked type
//! name stays rejected, plus `page`: its bare NAME lowers to the same
//! `Variant("page",[])` under both versions (invisible to
//! `forked_type_names()`'s automatic diff), but its VALUE representation
//! still forks — 0.0.6 a 9-ctor ADT (`Value::Ctor`), 0.1 a `length*length`
//! tuple (`Value::Product`) — so it is added to the reject set here
//! explicitly. No code path may ever hand a `Value` of one shape to a site
//! expecting another.
//!
//! **Where the type text that actually matters lives.** This port's 0.0.6
//! CST has no type-ascription syntax on an ordinary
//! `let`/`let-inline`/`let-block`/`let-math` binding — a binding's type is
//! 100% HM-inferred. Two surface forms DO carry a `cst::ast::TypeExpr` —
//! `cst::ast::RecBinding::ascription` and `cst::SigAnnot`'s `SigItem::Val*`/
//! `DirectHorzCmd`/`DirectVertCmd` items — but both are parsed and then
//! entirely IGNORED by `elaborate.rs` (`TopBinding::Module`/`RecBinding`
//! handling): neither reaches `typecheck.rs`, so relabeling them has zero
//! effect on typechecking.
//!
//! The one load-bearing form is `cst::TopBinding::Type`: `elaborate.rs`'s
//! `lower_type_decl` clones its ctor payload / synonym body verbatim into
//! `Program::type_decls`/`synonym_decls`, and `typecheck.rs`'s
//! `Checker::declare_variant`/`declare_synonym` — called ONCE per merged
//! program under the single whole-program `Checker.version` (`V0_1`, fixed
//! by `v1::module_check::check_program`'s session setup, NOT swapped by
//! `Ast::VersionScope`, which wraps only a binding's RHS *body*, never a
//! `type` declaration) — lower them via `name_to_mono(_, V0_1)`. A `type foo
//! = A of math` spliced unchanged would register `A`'s payload as the
//! nominal `Variant("math",[])` rather than `Base(MathText)`, so a real math
//! value handed to `A` would fail to unify. So the splice arm (`lib.rs`)
//! relabels exactly the `TopBinding::Type` bodies, recursing through
//! `TopBinding::Module`'s nested `decls` (the only other place a `type`
//! declaration can appear) — see `relabel_type_decls` below. Leaving the
//! decorative `RecAscription`/`SigAnnot` sites un-rewritten has no
//! behavioral effect.
//!
//! The ACCEPT/REJECT decision itself stays where the forked-name guard already computes it
//! (`lib.rs`'s `collect_free_globals` free-type scan) — this module only changes what
//! happens once that scan says the dependency's ENTIRE forked-type touch is
//! exactly `{"math"}`.

use rustyfi_syntax::cst;
use rustyfi_syntax::cst::ast::{TypeApp, TypeAtom, TypeExpr, TypeProd};
use rustyfi_syntax::cst_v1;
use rustyfi_syntax::RustyfiVersion;

use crate::types::{CmdArgType, MonoType, PolyType, Row};
use crate::v1::surface::{self, SurfaceEnv};

/// The verdict for one crossing binding's boundary type.
#[derive(Debug, Clone, PartialEq)]
pub enum BoundaryError {
    /// A forked type name appears in the export signature and is not
    /// representationally shared across the boundary.
    ForkedTypeExport {
        /// The crossing binding/type this offending leaf was found under,
        /// e.g. `"Mod.bar"` or a bare type-declaration name — best-effort,
        /// may be empty when no such context is available (the standalone
        /// [`adapt_export_type`]/[`adapt_export_annotation`] helpers below
        /// don't take one; their callers can wrap/annotate further).
        binding: String,
        /// The offending leaf, e.g. `"page"` / `"deco"` / `"math-boxes"`.
        ty_name: String,
        /// The producer version (the dependency's own).
        from: RustyfiVersion,
        /// The consumer version (the splicing program's).
        to: RustyfiVersion,
        /// A human hint (why this particular name can't be relabeled).
        note: &'static str,
    },
}

impl std::fmt::Display for BoundaryError {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            BoundaryError::ForkedTypeExport {
                binding,
                ty_name,
                from,
                to,
                note,
            } => {
                write!(
                    f,
                    "cross-version import (X3): {}exports a value whose type \
                     names `{ty_name}`, version-forked between {from:?} and \
                     {to:?} with no proven-identical runtime representation — \
                     {note}",
                    if binding.is_empty() {
                        String::new()
                    } else {
                        format!("`{binding}` ")
                    }
                )
            }
        }
    }
}

impl std::error::Error for BoundaryError {}

/// The set of type names refused when crossing the `V0_0` -> `V0_1`
/// boundary unadapted: every name [`crate::typecheck::forked_type_names`]
/// flags, plus `page` (see this module's doc comment for why
/// `page` needs adding explicitly rather than falling out of the automatic
/// diff). `math` is deliberately NOT a member: it is the sole
/// allow-and-relabel case, checked separately by every caller below.
pub fn reject_type_names() -> std::collections::BTreeSet<String> {
    let mut set = crate::typecheck::forked_type_names();
    set.insert("page".to_string());
    set
}

/// [`reject_type_names`] for a producer whose text was written as **0.0.6**,
/// i.e. the forward arm's spliced `V0_0` dependency: the shared set plus
/// `code`.
///
/// `code` forks one level ABOVE `name_to_mono`, invisible to the automatic
/// [`crate::typecheck::forked_type_names`] diff (`page`'s fork is invisible
/// for a different reason — see [`reject_type_names`]): it is the
/// constructor of a one-argument type APPLICATION, gated in
/// `typecheck::lower_type_app`'s `"code" if single.is_some() &&
/// version.has_code_type_syntax()` arm. Under `V0_1` `int code` is the real
/// [`MonoType::Code`](crate::types::MonoType::Code); under `V0_0` it stays
/// the opaque nominal `Variant("code", [int])`, because 0.0.6's manual-type
/// decoder knows only `list` and `ref` (upstream `v0.0.6
/// src/frontend/typeenv.ml:527-530`, vs `dev-0-1-0
/// src/frontend/manualTypeDecoder.ml:31-36` which adds `code`).
///
/// A merged cross-version program has ONE `Checker.version`, hard-coded to
/// `V0_1` (`v1::module_check::check_program_inner`), and a `TopBinding::Type`
/// declaration is registered under it — never inside an `Ast::VersionScope`
/// (this module's doc comment). So a 0.0.6 dependency that WRITES `code` in
/// a type declaration has that text re-read with 0.1's vocabulary and means
/// something different than it does standalone, in both directions of harm.
/// Refusing loudly (`CompileError::CrossVersionUnsupportedName`) is the
/// posture every other unbridgeable name here gets; no bundled 0.0.6 package
/// writes `code` in type position today.
///
/// **Deliberately not in [`reject_type_names`] itself**, which both arms
/// share: this fork is a property of the PRODUCER's generation, not of the
/// crossing. A foreign **0.1** dependency's `code` is already written in the
/// merged program's own (hard-coded `V0_1`) vocabulary, and rejecting it
/// would be a pure regression — pinned by `xver_staging.rs`'s
/// `a_zero_one_dependency_may_still_write_the_code_type`.
///
/// An INFERRED `code` export — the only kind a 0.0.6 package can otherwise
/// have, since `code τ` has no 0.0.6 spelling — writes no such text and
/// crosses fine: `Value::Code { body, env }` has no version field, and a
/// quoted body's primitives freeze to the generation it was written in at
/// compile time (`compile.rs`'s `Ast::Next` arm). See `xver_staging.rs` for
/// both halves.
pub fn reject_type_names_from_v006() -> std::collections::BTreeSet<String> {
    let mut set = reject_type_names();
    set.insert("code".to_string());
    set
}

/// A human hint for why `name` (a member of [`reject_type_names`]) can't be
/// relabeled across the boundary — the classification table below.
///
/// `pub(crate)` so `CompileError::CrossVersionUnsupportedName`'s `Display`
/// can append it (`lib.rs`): without a per-name note every refusal reads as
/// "not implemented yet", even the ones refused because the two generations
/// genuinely disagree about what the value IS.
pub(crate) fn forked_note(name: &str) -> &'static str {
    match name {
        "page" => {
            "0.0.6's page is a 9-ctor ADT (Value::Ctor); 0.1's is a length*length \
             tuple (Value::Product) — no shared runtime representation"
        }
        "math-boxes" => {
            "math-boxes is 0.1-only (the evaluated math tree); math must relabel to \
             math-text, never math-boxes (X3.8/S2) — no 0.0.6 value is ever a \
             math-boxes to begin with"
        }
        "math-text" => {
            "0.0.6 has no math-text primitive; a 0.0.6 package's OWN type named \
             math-text is an unrelated opaque user nominal, not a math value"
        }
        "deco" | "deco-set" => {
            "0.0.6 deco returns `graphics list`; 0.1 deco returns a single `graphics` \
             — the return shape differs, so crossing needs a value-level adapter. \
             X3b/X4b (classify_deco_exports/deco_coercion_prelude, and their reverse \
             twins) generate a POSITIONAL eta-expanding wrapper, which covers a \
             `deco`/`deco-set` TAIL after any number of MANDATORY arguments, at top \
             level or (nested) module scope; this particular occurrence is outside \
             that support — either an OPTIONAL-argument arrow (which has no positional \
             spelling to forward) or a `deco` leaf buried inside a compound type"
        }
        "paren" => {
            "0.0.6's paren is `length -> length -> length -> length -> color -> \
             (inline-boxes * (length -> length))` — (height, signed depth, axis, \
             fontsize, colour); 0.1's is `length -> length -> context -> \
             (inline-boxes * (length -> length))`, pulling the last three out of the \
             context instead. FORWARD that is a PROJECTION and X3b generates it: \
             `size = get-font-size ctx`, `axis = size *' \
             get-math-axis-height-ratio ctx`, `colour = get-text-color ctx`. \
             REVERSE there is no inverse to generate. The 0.0.6 call site \
             (`primitives::make_paren_run`) has only those five scalars and no \
             context at all, so a wrapper would have to invent one — and even \
             granting `set-font-size`/`set-text-color`, the caller's explicit AXIS \
             has no channel: 0.1 recovers the axis from the math font's MATH-table \
             height ratio, which no primitive in EITHER generation can set. A \
             reverse wrapper would therefore silently draw against the invented \
             context's axis rather than the caller's. This occurrence is either \
             that direction or outside the forward wrapper's support (an \
             OPEN optional row, or a `paren` leaf buried inside a compound type)"
        }
        "font" => {
            "a REPRESENTATION FORK, not a missing feature. 0.1's `font` is an OPAQUE \
             HANDLE on one already-loaded face — upstream saphe-split registers \
             (\"font\", FontType) in types.cppo.ml's base_type_hash_table, spells it \
             tFONTKEY, and its only values are BCFontKey of FontKey.t, minted by a \
             font ENVELOPE from a font FILE path (envelopeChecker.ml's \
             check_font_envelope). 0.0.6 has NO `font` type at all: no such row in \
             its own base_type_hash_table and no `type font` in its bundled \
             packages, so the same word in 0.0.6 text is an unrelated opaque user \
             nominal. What 0.0.6 calls a font is the bare product `string * float * \
             float` (tFONT) whose head is an ABBREV naming a row of \
             dist/hash/fonts.satysfi-hash — a different naming universe, and it \
             names no forked type, so it already crosses as the string triple it is. \
             Neither direction has a total map: forward there is no 0.0.6 value that \
             is a face handle, and an untagged `string * float * float` cannot be \
             recognized as a font to coerce; reverse a handle is a store index with \
             no abbrev to recover from it"
        }
        "code" => {
            "0.0.6 has no `code` type spelling at all (its manual-type decoder knows \
             only `list` and `ref`), so `τ code` there is an opaque user nominal — \
             but a merged program reads every type declaration under one hard-coded \
             V0_1 Checker, where the same text means the real staged type. An \
             INFERRED `code` export (a `@stage: 0` binding's `&e`) is unaffected and \
             crosses fine; only WRITTEN `code` type text does not"
        }
        // Unreachable through `reject_type_names()` today — upstream
        // registers the same base type in BOTH generations, so the automatic
        // `forked_type_names()` diff does not report these. Kept because
        // `forked_note` is also reachable from the standalone
        // `adapt_export_type` walk, which takes any name.
        "pre-path" | "path" | "graphics" | "image" => {
            "0.0.6 has no such primitive; this name is an opaque user-nominal \
             stand-in there, with no shared representation against 0.1's real \
             primitive type"
        }
        _ => {
            "no proven-identical Value representation across the version boundary \
              (X3a's whitelist is `math` only)"
        }
    }
}

fn reject_if_forked(
    name: &str,
    from: RustyfiVersion,
    to: RustyfiVersion,
) -> Result<(), BoundaryError> {
    if name == "math" {
        return Ok(());
    }
    if reject_type_names().contains(name) {
        return Err(BoundaryError::ForkedTypeExport {
            binding: String::new(),
            ty_name: name.to_string(),
            from,
            to,
            note: forked_note(name),
        });
    }
    Ok(())
}

// ============================================================================
// `adapt_export_type` — the spec function, operating on an already-
// inferred `PolyType` (a structural MonoType walk). This is the pure,
// directly-unit-testable statement of the classification rule above. It is NOT
// what the splice arm calls (there is no standalone per-export
// `PolyType` object at the splice site — a 0.0.6 export's type only exists
// after whole-program inference); the splice arm instead calls
// `adapt_export_annotation`/`relabel_type_decls` below, on the SURFACE
// syntax, justified by the same rule this function states formally.
//
// UNWIRED, and worth knowing before relying on the doc comments below. These
// five functions are a `MonoType`-level cross-version boundary check; the live
// path does NOT use them — it is name-based, through `reject_type_names` /
// `relabel_or_reject_name`, driven by `typecheck::forked_type_names()`. So
// `adapt_export_type`'s claim to be "the soundness backbone" describes a design
// that is written but not in force. Kept because the structural check is
// strictly more precise than the name-based one (it can see a forked leaf
// nested inside a compound rather than matching a spelling) and is the obvious
// thing to wire when the boundary needs to tighten. Delete them if that is not
// the plan — dead code cannot make anything sound.
// ============================================================================

/// Adapt a producer-version export type into an equivalent consumer-version
/// type whose runtime `Value` representation is provably identical, or
/// reject.
///
/// `ty` is the export's type as it would be read under `from` (its `V0_0`
/// meaning). On `Ok`, the returned `PolyType` is what a `to`-version
/// consumer scope should bind for this export. On `Err`, the caller should
/// raise a compile error and abort.
///
/// Invariant: `adapt_export_type` only ever returns a type reachable
/// from `ty` by a **pure relabel with no value coercion** — any leaf that
/// would require a runtime value adapter is an `Err`. This is the soundness
/// backbone. Because the sole accepted case (`math`) is already
/// `MathText` <-> `MathText` at the `MonoType` level (`types.rs` draws no
/// `math`/`math-text` distinction at all — see `BaseType::MathText`'s doc
/// comment), the `Ok` branch is simply `ty.clone()`: the "relabel" only ever
/// shows up at the surface-annotation level (`adapt_export_annotation`).
#[allow(dead_code)]
pub fn adapt_export_type(
    ty: &PolyType,
    from: RustyfiVersion,
    to: RustyfiVersion,
) -> Result<PolyType, BoundaryError> {
    check_mono_type(ty.body(), from, to)?;
    Ok(ty.clone())
}

#[allow(dead_code)]
fn check_mono_type(
    ty: &MonoType,
    from: RustyfiVersion,
    to: RustyfiVersion,
) -> Result<(), BoundaryError> {
    match ty {
        MonoType::Var(_) | MonoType::Base(_) => Ok(()),
        MonoType::Func(row, dom, cod) => {
            check_row(row, from, to)?;
            check_mono_type(dom, from, to)?;
            check_mono_type(cod, from, to)
        }
        MonoType::Product(items) => {
            for t in items {
                check_mono_type(t, from, to)?;
            }
            Ok(())
        }
        MonoType::List(t) | MonoType::Ref(t) | MonoType::Code(t) => check_mono_type(t, from, to),
        MonoType::Record(row) => check_row(row, from, to),
        MonoType::Variant(name, args) => {
            reject_if_forked(name, from, to)?;
            for t in args {
                check_mono_type(t, from, to)?;
            }
            Ok(())
        }
        MonoType::InlineCmd(items) | MonoType::BlockCmd(items) | MonoType::MathCmd(items) => {
            for c in items {
                check_cmd_arg(c, from, to)?;
            }
            Ok(())
        }
    }
}

#[allow(dead_code)]
fn check_row(row: &Row, from: RustyfiVersion, to: RustyfiVersion) -> Result<(), BoundaryError> {
    match row {
        Row::Empty | Row::Var(_) => Ok(()),
        Row::Cons(_, ty, rest) => {
            check_mono_type(ty, from, to)?;
            check_row(rest, from, to)
        }
    }
}

#[allow(dead_code)]
fn check_cmd_arg(
    c: &CmdArgType,
    from: RustyfiVersion,
    to: RustyfiVersion,
) -> Result<(), BoundaryError> {
    for (_, ty) in &c.opt_labels {
        check_mono_type(ty, from, to)?;
    }
    check_mono_type(&c.ty, from, to)
}

// ============================================================================
// `adapt_export_annotation` — the CST-level helper the splice arm actually
// exercises: walks a SURFACE `cst::ast::TypeExpr`, rewriting every
// free `math` leaf to `math-text` and rejecting any other forked leaf
// (structural walk of `Fun`/`Atom`/`OptRowFun`/`TypeProd`/`TypeApp`/
// `TypeAtom`, mirroring `lib.rs`'s read-only `walk_type_expr` family used by
// `collect_free_globals`, but mutating instead of collecting).
// ============================================================================

/// Adapt one surface type annotation: clone `ann`, rewrite every `math` leaf
/// to `math-text`, and reject if any OTHER forked leaf (`reject_type_names`)
/// appears anywhere in the structure (a forked leaf nested in a
/// compound rejects the WHOLE annotation, no partial acceptance).
#[allow(dead_code)]
pub fn adapt_export_annotation(
    ann: &TypeExpr,
    from: RustyfiVersion,
    to: RustyfiVersion,
) -> Result<TypeExpr, BoundaryError> {
    let mut out = ann.clone();
    relabel_type_expr(&mut out, from, to)?;
    Ok(out)
}

fn relabel_type_expr(
    te: &mut TypeExpr,
    from: RustyfiVersion,
    to: RustyfiVersion,
) -> Result<(), BoundaryError> {
    match te {
        TypeExpr::Fun { opts, dom, cod, .. } => {
            for o in opts.iter_mut() {
                relabel_type_prod(&mut o.ty, from, to)?;
            }
            relabel_type_prod(dom, from, to)?;
            relabel_type_expr(cod, from, to)
        }
        TypeExpr::Atom(prod) => relabel_type_prod(prod, from, to),
        TypeExpr::OptRowFun {
            opt_dom, dom, cod, ..
        } => {
            for e in opt_dom.entries.iter_mut() {
                relabel_type_expr(&mut e.ty.0, from, to)?;
            }
            relabel_type_prod(dom, from, to)?;
            relabel_type_expr(cod, from, to)
        }
    }
}

fn relabel_type_prod(
    tp: &mut TypeProd,
    from: RustyfiVersion,
    to: RustyfiVersion,
) -> Result<(), BoundaryError> {
    relabel_type_app(&mut tp.first, from, to)?;
    for st in tp.rest.iter_mut() {
        relabel_type_app(&mut st.ty, from, to)?;
    }
    Ok(())
}

fn relabel_type_app(
    ta: &mut TypeApp,
    from: RustyfiVersion,
    to: RustyfiVersion,
) -> Result<(), BoundaryError> {
    // Every atom of the application (arguments and the final constructor) is
    // a `TypeAtom`; `relabel_type_atom` relabels a bare `Name` via
    // `relabel_or_reject_name` and passes a qualified `Mod.t` through, so
    // relabeling the whole run covers both the arguments and the ctor.
    relabel_type_atom(&mut ta.head, from, to)?;
    for a in &mut ta.rest {
        relabel_type_atom(a, from, to)?;
    }
    Ok(())
}

fn relabel_type_atom(
    atom: &mut TypeAtom,
    from: RustyfiVersion,
    to: RustyfiVersion,
) -> Result<(), BoundaryError> {
    match atom {
        TypeAtom::Cmd { args, .. } => {
            for a in args.iter_mut() {
                for l in a.opt_labels.iter_mut() {
                    relabel_type_expr(&mut l.ty.0, from, to)?;
                }
                relabel_type_expr(&mut a.ty.0, from, to)?;
            }
            Ok(())
        }
        TypeAtom::Paren { inner, .. } => relabel_type_expr(&mut inner.0, from, to),
        TypeAtom::Record { fields, .. } => {
            for f in fields.iter_mut() {
                relabel_type_expr(&mut f.ty.0, from, to)?;
            }
            Ok(())
        }
        // A bound type variable — never a forked-name candidate.
        TypeAtom::Var(_) => Ok(()),
        TypeAtom::Name(n) => relabel_or_reject_name(&mut n.name, from, to),
        // `Mod.t` — already qualified, never one of the unqualified fork
        // names this policy governs.
        TypeAtom::NameMod(_) => Ok(()),
        TypeAtom::RecordOpen { inner, .. } => {
            for f in inner.fields.iter_mut() {
                relabel_type_expr(&mut f.ty.0, from, to)?;
            }
            Ok(())
        }
    }
}

/// The one leaf-level policy decision, generalized by DIRECTION for
/// the reverse (0.1 -> 0.0.6) import guard.
///
/// **Where each direction is actually WIRED (load-bearing asymmetry).** The
/// FORWARD `(V0_0, V0_1)` arm below IS reached from `lib.rs`'s splice arm,
/// via `relabel_type_decls` — necessary there because
/// `v1::module_check::check_program_inner` hard-codes `Checker.version =
/// V0_1` for EVERY type declaration in the merged program (`module_check.rs`
/// :238-239,271), so a spliced 0.0.6 dependency's own "math" spelling MUST
/// be rewritten into ambient vocabulary before it reaches
/// `program.type_decls`. The REVERSE `(V0_1, V0_0)` arm below is NOT wired
/// into `lib.rs`'s reverse splice arm (`compile_document_v006_xver_with_
/// trials`): a foreign 0.1 dependency's own "math-text"/"math-boxes"
/// spelling is ALREADY that same hard-coded ambient (`V0_1`) vocabulary, so
/// relabeling it to 0.0.6's "math" would corrupt, not fix, it — that splice
/// arm instead uses this module's `reject_type_names()` as a pure WHITELIST
/// GUARD (accept-if-`{"math-text","math-boxes"}`-only, else reject; splice
/// VERBATIM either way). The reverse arm stays correct and unit-tested (this
/// module's `adapt_export_annotation_reverse_*` group) as a
/// direction-complete pure utility, ready for a future caller not bound by
/// `check_program`'s hard-coded-`V0_1` constraint.
///
/// - **`V0_0` -> `V0_1`**: `"math"` relabels in place to `"math-text"`
///   — 0.0.6's undifferentiated math type maps to 0.1's UNEVALUATED half, the
///   correct direction since a crossing 0.0.6 `math` value is exactly a
///   `Value::MathText`/`Value::Math` (never a `Value::MathBoxes`, which no
///   0.0.6 primitive ever produces — the soundness backbone).
/// - **`V0_1` -> `V0_0`**: `"math-text"` OR `"math-boxes"` relabels in
///   place to `"math"` — 0.1's split math types both COARSEN safely into
///   0.0.6's one undifferentiated type. The "must never alias" mirror
///   does not apply: 0.0.6-authored code has no syntax that could ever
///   observe the lost distinction, and both `Value::MathText` and
///   `Value::Math` are ALREADY valid `math`-typed runtime values under 0.0.6
///   (`value.rs:39-56`'s shared representation; 0.0.6 code
///   pattern-matches/embeds a `math` value structurally, never on which of
///   the two variants produced it). So this is a pure, zero-coercion relabel
///   exactly like the forward case.
/// - Every other member of [`reject_type_names`], in EITHER direction, is a
///   hard `Err` (this guard is deliberately conservative — see this
///   module's doc comment for `page`/`graphics`/`deco`/
///   `deco-set`/`pre-path`/`path`/`image`/`font`/`paren`).
/// - Everything else (an ordinary user type name, or a shared builtin like
///   `int`/`string`) passes through untouched, in either direction.
fn relabel_or_reject_name(
    name: &mut String,
    from: RustyfiVersion,
    to: RustyfiVersion,
) -> Result<(), BoundaryError> {
    match (from, to) {
        (RustyfiVersion::V0_0, RustyfiVersion::V0_1) if name == "math" => {
            *name = "math-text".to_string();
            Ok(())
        }
        (RustyfiVersion::V0_1, RustyfiVersion::V0_0)
            if name == "math-text" || name == "math-boxes" =>
        {
            *name = "math".to_string();
            Ok(())
        }
        _ => reject_if_forked(name, from, to),
    }
}

// ============================================================================
// `relabel_type_decls` — the actual splice-arm entry point (`lib.rs`'s
// `compile_document_v1_with_trials`): rewrite every LOAD-BEARING type-text
// site in a spliced `V0_0` dependency's `prelude` (see this module's doc
// comment for why `TopBinding::Type`, recursed through `TopBinding::
// Module`'s nested `decls`, is the complete set of such sites in this
// port's 0.0.6 grammar).
// ============================================================================

/// Clone `prelude` and relabel every `math` leaf inside a `TopBinding::Type`
/// declaration's body (a variant's ctor payloads, or a synonym's body),
/// recursing into `TopBinding::Module`'s nested `decls` — the only other
/// place a `type` declaration can appear. Every other `TopBinding` variant
/// carries no type text this port's typechecker ever consults (see the
/// module doc comment), so it is returned unchanged.
///
/// Precondition (enforced by the caller, `lib.rs`): the dependency's ENTIRE
/// free-type touch (`collect_free_globals`, checked against
/// [`reject_type_names`]) is exactly `{"math"}` — so this walk can never
/// actually observe another forked name and return `Err` in practice; the
/// `Result` is kept for defense in depth / symmetry with
/// `adapt_export_annotation`, not because failure is expected here.
pub(crate) fn relabel_type_decls(
    prelude: &[cst::TopBinding],
    from: RustyfiVersion,
    to: RustyfiVersion,
) -> Result<Vec<cst::TopBinding>, BoundaryError> {
    prelude
        .iter()
        .cloned()
        .map(|tb| relabel_top_binding_types(tb, from, to))
        .collect()
}

fn relabel_top_binding_types(
    mut tb: cst::TopBinding,
    from: RustyfiVersion,
    to: RustyfiVersion,
) -> Result<cst::TopBinding, BoundaryError> {
    match &mut tb {
        cst::TopBinding::Type(td) => {
            relabel_type_decl_body(&mut td.body, from, to)?;
            for a in td.ands.iter_mut() {
                relabel_type_decl_body(&mut a.body, from, to)?;
            }
        }
        cst::TopBinding::Module { decls, .. } => {
            for d in decls.iter_mut() {
                let inner = (*d.0).clone();
                *d.0 = relabel_top_binding_types(inner, from, to)?;
            }
        }
        // `LetRec`/`Let`/`LetInline`/`LetBlock`/`LetMath`/`LetMutable`/
        // `Open` carry no `type`-declaration text (this module's doc
        // comment) — nothing to relabel.
        _ => {}
    }
    Ok(tb)
}

fn relabel_type_decl_body(
    body: &mut cst::TypeDeclBody,
    from: RustyfiVersion,
    to: RustyfiVersion,
) -> Result<(), BoundaryError> {
    match body {
        cst::TypeDeclBody::Variant { first, rest, .. } => {
            relabel_variant_def(first, from, to)?;
            for bv in rest.iter_mut() {
                relabel_variant_def(&mut bv.def, from, to)?;
            }
            Ok(())
        }
        cst::TypeDeclBody::Synonym(ty) => relabel_type_expr(ty, from, to),
    }
}

fn relabel_variant_def(
    vd: &mut cst::VariantDef,
    from: RustyfiVersion,
    to: RustyfiVersion,
) -> Result<(), BoundaryError> {
    if let Some(of_ty) = &mut vd.of_ty {
        relabel_type_expr(&mut of_ty.ty, from, to)?;
    }
    Ok(())
}

// ============================================================================
// The forward deco/paren value-coercion wrapper: a real value-level coercion for the `deco`/`deco-set` case — "0.0.6
// deco returns `graphics list`; 0.1 deco returns a single `graphics`".
//
// Unlike `math`, `deco`'s bare NAME needs no textual relabel at all: once
// accepted, `typecheck::name_to_mono("deco", V0_1)` resolves it to
// `t_deco(V0_1)` unconditionally (gated on `version == V0_1` with no
// analogous `V0_0` arm, so the SAME bare word means the SAME 0.1 arrow-type
// once the splice stops rejecting it). So a `deco`/`deco-set` mention with no
// VALUE attached (a bare `type foo = deco` synonym) is *already* safe with
// zero further work — `relabel_type_decls` above is not even called for it.
//
// What genuinely needs adapting is the VALUE: a `V0_0`-authored `deco`
// closure's body, once fully applied, evaluates to `Value::List` of
// `Value::Graphics` (`prim_types::t_graphics_output`'s
// `!graphics_is_collection` arm; `primitives::coerce_graphics_result`'s
// `else` branch), and the compile-time `Ast::VersionScope` mechanism
// does NOT retroactively change that — a closure's *body* just runs whatever
// it literally constructs. Meanwhile every real `V0_1` call site that
// *applies* a `deco` (`primitives::apply_deco`, fired by `lib.rs`'s
// `fire_inline_frame`/`fire_hooks` at render time) runs
// `coerce_graphics_result` under the AMBIENT `interp.version` — `V0_1` for
// any call reached from consumer code outside a `VersionScope` — which
// expects a SINGLE `graphics`, and `as_graphics` on a `Value::List` fails.
// So a crossing `deco` value must be COERCED, not merely relabeled.
//
// **Scope.** Every shape whose wrapper can be written as a POSITIONAL
// eta-expansion crosses:
//
//   - bare-leaf `: deco`/`: deco-set` on a prelude-ROOT `TopBinding::LetRec`;
//   - arrow-PREFIXED (`length -> color -> color -> deco`) — the wrapper
//     forwards `lead_arity` extra parameters before `deco`'s own four;
//   - MODULE-scoped (a `module .. : sig .. end`'s `val` item, or a member's
//     own ascription inside the struct body) — a top-level `let
//     Deco.simple-frame` is not syntax, so the wrapper is appended INSIDE
//     the module's own `decls` (`inject_module_deco_wrappers`) where
//     ordinary sequential shadowing applies;
//   - NESTED-module scoped (a `module .. = struct module .. = struct ..`
//     chain), same mechanism one or more levels deeper — `DecoExport::
//     module_path` carries the whole chain and the injector matches on it.
//
// The one shape that has NO sound wrap here, and REJECTS: an
// OPTIONAL-argument arrow anywhere in the export's type (`?(l = ty) -> ..`
// / a `TypeExpr::Fun` with a non-empty `opts`). The generated wrapper
// forwards its parameters POSITIONALLY and an optional argument has no
// positional spelling at all, so eta-expanding one would silently drop it —
// [`deco_tail_of`] returns `None` for that case on purpose. Same for a `deco`
// leaf buried in a compound (a product/record/list member): the coercion is
// defined on the RESULT of a curried application, not on an arbitrary
// occurrence. `classify_deco_exports` REJECTS (rather than silently drops)
// every such occurrence, so the splice arm (`lib.rs`) fails loudly.
//
// One more narrowing specific to `deco-set`: its RecBinding's own
// `rb.params` must be EXACTLY one `PatBot::Unit` (`()`). `deco-set` is a
// plain 4-TUPLE, not a function (unlike `deco`) — but `elaborate.rs`
// REQUIRES a `let-rec` binding's RHS to be a function ("must be a function,
// got tuple"), so a bare `deco-set` export can ONLY ever be legally WRITTEN
// as `let-rec name : deco-set | () = (d0, d1, d2, d3)`, the `| ()` idiom this
// test suite's other "plain value" fixtures also use (e.g. `xver_import.rs`'s
// `xver-get-page : page | () = A4Paper`). `deco_coercion_prelude`'s wrap
// therefore applies the mandatory unit thunk (`{name} ()`) before
// destructuring the tuple. `deco` itself needs no such params check: its wrap
// APPLIES 4 fresh arguments through ordinary function application, and HM
// unification is structural, so a `rb.params` mismatch can only produce an
// ordinary `TypeError`. `deco-set`'s `{name} ()`-then-`match` has no such
// automatic backstop — a wrong params shape is *also* an ordinary
// `TypeError`, but a needlessly confusing one, so checking `rb.params` up
// front turns it into this module's clear `BoundaryError` instead.
// ============================================================================

/// Which `deco`-family shape a [`DecoExport`] is.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub(crate) enum DecoKind {
    /// `deco = point -> length -> length -> length -> {list graphics /
    /// graphics}` — a 4-ary curried closure once fully applied.
    Deco,
    /// `deco-set = deco * deco * deco * deco` — a 4-tuple of `deco`s.
    DecoSet,
    /// A `paren` export (`math.satyh`'s `paren-left`/`brace-left`/… — 17 of
    /// them, all module-scoped, two arrow-tailed). 0.0.6 spells it `h -> d ->
    /// axis -> size -> color -> (inline-boxes, length -> length)`; 0.1 spells
    /// it `h -> d -> context -> ..` and has the closure pull fontsize, axis
    /// ratio and colour out of the context itself (`t_paren`,
    /// `primitives::make_paren_run`). The wrapper presents 0.1's interface and
    /// re-derives 0.0.6's three extra arguments from the context.
    Paren,
    /// Not a deco PRODUCER but a deco CONSUMER: an export that TAKES a
    /// `deco`/`deco-set` as an argument, e.g. `code.satyh`'s `val scheme :
    /// deco-set -> color -> context -> string -> block-boxes`. The coercion
    /// runs the other way — contravariantly. A 0.1 caller supplies a 0.1
    /// deco (returning one `graphics`), and the 0.0.6 callee will invoke it
    /// expecting a `graphics list`, so each such argument is DOWNGRADED by
    /// wrapping its result in a singleton list — the literal inverse of the
    /// `unite-graphics` upgrade. Which positions to downgrade is carried in
    /// [`DecoExport::arg_downgrades`].
    Consumer,
}

/// How one LEAD argument position of a [`DecoExport`] spells its optional
/// arguments, if any. The two generations model optionals so differently that
/// the generated wrapper has to reproduce each one in its own terms — see
/// [`deco_wrapper_src`] (0.0.6 → 0.1) and [`deco_downgrade_prelude`]
/// (0.1 → 0.0.6).
#[derive(Debug, Clone, PartialEq, Eq)]
pub(crate) enum LeadOpt {
    /// One plain mandatory argument, no optionals.
    Mandatory,
    /// **0.0.6**, `ty ?->`: this position IS the optional slot. 0.0.6's
    /// optional arguments are POSITIONAL in this port — `lower_type_expr`
    /// turns each `ty ?->` domain into a mandatory `option ty ->` domain, and
    /// `elaborate.rs`'s `app_arg_to_ast` desugars a call site's `?:e`/`?*` to
    /// the plain `Some e`/`None` constructors — so a positional
    /// eta-expansion forwards one by VALUE with nothing lost.
    ///
    /// The one thing the wrapper must still reproduce is the `?:` MARKER on
    /// its own parameter: `elaborate.rs`'s `param_optional_shape` records it
    /// into [`Scope::optional_shape`], which is what lets a marker-less call
    /// site (`frame p w h d`, no `?*`) auto-omit the slot. A wrapper with
    /// plain parameters would shadow the export with one that has no recorded
    /// shape, silently breaking every marker-less call.
    V006Optional,
    /// **0.1**, `?(l : τ, …) dom ->`: this position takes one mandatory
    /// argument PLUS a LABELLED optional row (`MonoType::Func`'s [`Row`]),
    /// named here in declared order. Labelled optionals are not positional
    /// and cannot be forwarded by value: `Ast::LambdaOpt` binds the callee's
    /// binder at `τ option` while `Ast::ApplyOpt`'s `?(l = e)` takes the
    /// RAW `τ` and wraps it in `Some` itself, so there is no spelling that
    /// hands an already-`option` value to a labelled slot. The wrapper
    /// therefore CASE-SPLITS on each label's `option` and re-supplies exactly
    /// the labels that were present — see [`deco_downgrade_prelude`].
    V01Labels(Vec<String>),
}

/// The most optional LABELS (summed over every lead position) a 0.1 export
/// may declare and still cross. The reverse wrapper's case split is
/// exponential in this count (each label is independently present or absent
/// at the call that reaches it), so it is bounded rather than unbounded; four
/// labels is sixteen generated application sites, already far past anything
/// the bundled corpora declare on a single `deco`.
const V01_MAX_OPT_LABELS: usize = 4;

/// One binding a cross-version splice can soundly value-coerce: some number
/// of leading arguments (mandatory, or optional in whichever of the two
/// generations' spellings — see [`LeadOpt`]) followed by a
/// `deco`/`deco-set`/`paren` tail — see this section's doc comment for the
/// exact scope.
///
/// **Shared by both directions.** The forward wrapper classifies a `V0_0` dependency's
/// exports for a `V0_1` consumer (`classify_deco_exports`, off the 0.0.6
/// surface: a `RecBinding.ascription` or a `module .. : sig .. end` item);
/// the reverse wrapper classifies a `V0_1` dependency's exports for a `V0_0` consumer
/// (`classify_deco_exports_v01_sig`, off the 0.1 `:>` sig — the ONE site
/// 0.1's grammar can name such a type at all). The `DecoExport` shape is the
/// same either way; only the generated wrapper differs — `unite-graphics`
/// (list -> single) forward, a singleton list (single -> list) in reverse.
#[derive(Debug, Clone)]
pub(crate) struct DecoExport {
    pub name: String,
    pub kind: DecoKind,
    /// How many arguments the export takes BEFORE its `deco` tail — the
    /// `3` in `simple-frame : length -> color -> color -> deco`. The
    /// generated wrapper eta-expands over exactly this many extra
    /// parameters, then over `deco`'s own four. `0` is the bare `: deco`
    /// case.
    pub lead_arity: usize,
    /// One [`LeadOpt`] per lead position (so `lead_opts.len() == lead_arity`
    /// whenever it is non-empty). EMPTY is the shorthand for "every position
    /// is [`LeadOpt::Mandatory`]" — read it through [`DecoExport::lead_opt`],
    /// never by direct indexing.
    pub lead_opts: Vec<LeadOpt>,
    /// The enclosing `module .. = struct .. end` chain, outermost first;
    /// empty for a top-level binding. A module-scoped export CANNOT be
    /// wrapped by a top-level shadowing binding — `let Deco.simple-frame`
    /// is not syntax — so its wrapper is appended INSIDE the module's own
    /// `decls` instead (`inject_module_deco_wrappers`), where ordinary
    /// sequential shadowing applies (`elaborate.rs`'s `walk_bindings`
    /// folds decls through a `running` scope, so a later decl shadows an
    /// earlier one of the same name).
    pub module_path: Vec<String>,
    /// For [`DecoKind::Consumer`]: one slot per leading argument, `Some(kind)`
    /// where that argument is a bare `deco`/`deco-set` needing the
    /// contravariant downgrade, `None` where it passes straight through.
    /// Empty for every producer.
    pub arg_downgrades: Vec<Option<DecoKind>>,
    /// [`DecoKind::DecoSet`] only: whether the ORIGINAL binding must be
    /// applied to a mandatory `()` thunk before its 4-tuple can be
    /// destructured. `true` for a `let-rec name : deco-set | () = (d0, ..)`
    /// export (`elaborate.rs` refuses a non-function `let-rec` RHS, so that
    /// spelling is the ONLY legal one for a bare, argument-less `deco-set`
    /// `let-rec`); `false` for a sig-declared member bound by an ordinary
    /// `let` to the bare tuple, and for every arrow-tailed `deco-set` (whose
    /// leading arguments are applied instead). Meaningless — and always
    /// `false` — for the other three kinds.
    pub unit_thunk: bool,
}

impl DecoExport {
    /// Lead position `i`'s optional spelling, defaulting to
    /// [`LeadOpt::Mandatory`] for an export whose `lead_opts` is the empty
    /// shorthand (see that field's doc comment).
    fn lead_opt(&self, i: usize) -> &LeadOpt {
        const MANDATORY: LeadOpt = LeadOpt::Mandatory;
        self.lead_opts.get(i).unwrap_or(&MANDATORY)
    }

    /// Whether ANY lead position carries optional arguments — i.e. whether
    /// the generated wrapper needs the optional-aware shape at all. `false`
    /// keeps every generator below on the plain positional path.
    fn has_optionals(&self) -> bool {
        self.lead_opts
            .iter()
            .any(|o| !matches!(o, LeadOpt::Mandatory))
    }

    /// The private name a wrapper binds the export's UNSHADOWED original
    /// under, when it cannot simply name the export itself.
    ///
    /// The forward wrapper normally re-applies the export by its own name and
    /// relies on ordinary shadowing. That stops working the moment the export
    /// has 0.0.6-style optionals: the ORIGINAL binding may carry a
    /// [`Scope::optional_shape`] entry (a `let frame ?:t p w h d = ..`
    /// implementing a sig's `length ?-> deco`), and `elaborate.rs`'s
    /// `app_chain_generic` then reads that shape at the wrapper's OWN call to
    /// it and synthesizes a `None` for the slot instead of consuming the
    /// wrapper's forwarded parameter — shifting every later argument by one.
    /// Binding the original to a fresh name first dodges that, but only if
    /// the alias does not INHERIT the shape, which `alias_optional_shape`
    /// makes it do for a bare `let x = y`; hence the parenthesised RHS in
    /// [`deco_wrapper_src`] (`head_optional_shape` reads a shape only off a
    /// bare `Var`/`VarWithMod` head).
    fn opt_src_alias(&self) -> String {
        format!("xver-opt-src-{}", self.dash_key())
    }

    /// The export's own fully-qualified key — `"M.frame"` for a module
    /// member, the bare `"frame"` for a top-level one. This is the name a
    /// consumer of EITHER generation writes, and the one the view-scheduling mechanism
    /// rebinds to whichever view that consumer should see.
    ///
    /// Deliberately NOT [`deco_export_qualified_name`], which is the reverse wrapper's and
    /// assumes a non-empty `module_path` (it would spell a top-level export
    /// `".frame"`); the forward direction classifies top-level exports too.
    fn qualified_key(&self) -> String {
        if self.module_path.is_empty() {
            self.name.clone()
        } else {
            format!("{}.{}", self.module_path.join("."), self.name)
        }
    }

    /// `qualified_key` with `.` swapped for `-`, so it can be embedded in a
    /// surface identifier (a `.` cannot appear in one, a `-` can).
    fn dash_key(&self) -> String {
        let mut key: Vec<&str> = self.module_path.iter().map(String::as_str).collect();
        key.push(&self.name);
        key.join("-")
    }

    /// The name the view-scheduling mechanism binds the export's UNWRAPPED (0.0.6-shaped) original
    /// under, in the SAME scope the export itself lives in — a sibling
    /// `StructDecl` for a module member, a sibling top-level binding for a
    /// top-level export. Emitted BEFORE the wrapper, while the original is
    /// still the innermost binding of its own name.
    ///
    /// It has to live in that scope rather than at top level because a module
    /// member's original is not reachable from outside once the wrapper has
    /// shadowed it — and a 0.0.6 `sig .. end` seals nothing (`elaborate.rs`'s
    /// `TopBinding::Module` arm accepts `val` items and ignores them; only
    /// `direct` items bind anything), so an extra member is visible to every
    /// later consumer as `M.xver-fwd-orig-frame` with its own inferred type.
    fn orig_capture_name(&self) -> String {
        format!("xver-fwd-orig-{}", self.name)
    }

    /// [`orig_capture_name`](Self::orig_capture_name) qualified the same way
    /// the export itself is — the expression a `Restore` step rebinds the
    /// export's key to.
    fn orig_capture_key(&self) -> String {
        if self.module_path.is_empty() {
            self.orig_capture_name()
        } else {
            format!("{}.{}", self.module_path.join("."), self.orig_capture_name())
        }
    }

    /// The private TOP-LEVEL name the view-scheduling mechanism's `Capture` step binds the WRAPPED
    /// (0.1-shaped) view under, so a later `Install` can put it back without
    /// regenerating the wrapper. A pure function of the export's own key, so
    /// the separate `Capture`/`Install` calls agree on it.
    fn view_capture_name(&self) -> String {
        format!("xver-fwd-view-{}", self.dash_key())
    }
}

/// Scan a spliced `V0_0` dependency's `prelude` for every `deco`/
/// `deco-set` occurrence reachable from a `V0_1` consumer (the SAME
/// boundary sites `lib.rs`'s `collect_free_globals` already treats as
/// export text: a top-level `TopBinding::LetRec`'s own ascription, a
/// `TopBinding::Module`'s `sig` items, and — recursively — a module's own
/// `decls`), and classify each:
///
/// - a bare-leaf (or arrow-tailed) ascription on a `TopBinding::LetRec`,
///   whether top-level or nested inside a `module .. = struct .. end` →
///   sound to wrap, pushed onto the returned `Vec<DecoExport>`;
/// - a `TopBinding::Type` body (a synonym/ctor payload merely NAMING
///   `deco`/`deco-set`, no value attached) → SAFE, no coercion needed at
///   all (see this section's doc comment) — silently skipped (not even
///   visited: `classify_top_binding_deco`'s `_` arm);
/// - anything else that could carry a REAL `deco`/`deco-set`-typed VALUE
///   across the boundary (a `deco` leaf buried in a compound type, or an
///   OPTIONAL-argument arrow — see [`deco_tail_of`] for why the generated
///   positional wrapper cannot express one) → `Err` — the forward wrapper has no sound
///   wrap for these; the caller (`lib.rs`) rejects the WHOLE dependency,
///   exactly as the plain type-relabel path did before any `DecoExport` existed.
pub(crate) fn classify_deco_exports(
    prelude: &[cst::TopBinding],
    from: RustyfiVersion,
    to: RustyfiVersion,
) -> Result<Vec<DecoExport>, BoundaryError> {
    let mut out = Vec::new();
    let skip = std::collections::HashSet::new();
    for tb in prelude {
        classify_top_binding_deco(tb, &mut out, &[], &skip, from, to)?;
    }
    Ok(out)
}

/// `skip` names an ENCLOSING module's already-scheduled sig-item wrappers:
/// the `decls` walk must not schedule a SECOND wrapper for a member whose
/// `sig` item already produced one (that would wrap the wrap — two
/// `unite-graphics` layers). It is per-module-level: each nested
/// `TopBinding::Module` arm below computes its OWN set and passes that down,
/// never the parent's.
fn classify_top_binding_deco(
    tb: &cst::TopBinding,
    out: &mut Vec<DecoExport>,
    module_path: &[String],
    skip: &std::collections::HashSet<String>,
    from: RustyfiVersion,
    to: RustyfiVersion,
) -> Result<(), BoundaryError> {
    match tb {
        cst::TopBinding::LetRec { first, ands, .. } => {
            classify_rec_binding_deco(first, out, module_path, skip, from, to)?;
            for a in ands {
                classify_rec_binding_deco(&a.binding, out, module_path, skip, from, to)?;
            }
            Ok(())
        }
        cst::TopBinding::Module {
            name, sig, decls, ..
        } => {
            let mut inner = module_path.to_vec();
            inner.push(name.name.clone());
            // A module's SIG is the export surface: a `val x : .. -> deco`
            // item names a real value crossing the boundary, and (unlike the
            // top-level case) its `decls` counterpart may be an ordinary
            // `let`, so the sig is the only place the type is written. Wrap
            // what has a deco TAIL; reject anything that merely mentions
            // `deco` somewhere else in the type, which the positional
            // wrapper could not express.
            let mut wrapped: std::collections::HashSet<String> = std::collections::HashSet::new();
            if let Some(sig) = sig {
                for item in &sig.items {
                    if let Some(ty) = sig_item_value_ty(item) {
                        match (
                            sig_item_value_name(item),
                            deco_tail_of(ty),
                            deco_consumer_plan(ty),
                        ) {
                            (Some(n), Some((kind, lead_arity, lead_opts)), _) => {
                                wrapped.insert(n.to_string());
                                out.push(DecoExport {
                                    name: n.to_string(),
                                    kind,
                                    lead_arity,
                                    lead_opts,
                                    module_path: inner.clone(),
                                    arg_downgrades: Vec::new(),
                                    unit_thunk: false,
                                });
                            }
                            (Some(n), None, Some((plan, lead_opts))) => {
                                wrapped.insert(n.to_string());
                                out.push(DecoExport {
                                    name: n.to_string(),
                                    kind: DecoKind::Consumer,
                                    lead_arity: plan.len(),
                                    lead_opts,
                                    module_path: inner.clone(),
                                    arg_downgrades: plan,
                                    unit_thunk: false,
                                });
                            }
                            _ => reject_if_mentions_deco(ty, from, to)?,
                        }
                    }
                }
            }
            // RECURSE into the struct body (the reverse wrapper's sibling nested-module
            // handling). A member's own `: ty` ascription and a NESTED
            // `module .. = struct .. end`'s own `sig`/`decls` are classified
            // exactly as this level's are, just under a longer `module_path` —
            // which is all `inject_module_deco_wrappers` needs, since it
            // already walks nested modules and matches on the full path.
            // `wrapped` is passed as the skip set so a member already
            // scheduled from THIS module's `sig` is not wrapped a second time
            // from its own ascription (its ascription, if any, names the same
            // type the sig does).
            for d in decls {
                classify_top_binding_deco(&d.0, out, &inner, &wrapped, from, to)?;
            }
            Ok(())
        }
        // `Let`/`LetInline`/`LetBlock`/`LetMath`/`LetMutable`/`Open` carry no
        // `: ty` ascription this port's grammar could name `deco`/
        // `deco-set` in at all; `Type`'s body is the SAFE, no-value case
        // (this section's doc comment) — nothing to classify or reject.
        _ => Ok(()),
    }
}

fn classify_rec_binding_deco(
    rb: &cst::ast::RecBinding,
    out: &mut Vec<DecoExport>,
    module_path: &[String],
    skip: &std::collections::HashSet<String>,
    from: RustyfiVersion,
    to: RustyfiVersion,
) -> Result<(), BoundaryError> {
    let Some(asc) = &rb.ascription else {
        return Ok(());
    };
    if skip.contains(&rb.name.name) {
        // Already scheduled from the enclosing module's own `sig` item —
        // see `classify_top_binding_deco`'s `skip` doc comment.
        return Ok(());
    }
    // An arrow-PREFIXED deco (`length -> color -> color -> deco`, the shape
    // every real module export uses) is wrappable the same way a bare one
    // is — the wrapper just eta-expands over the leading arguments first.
    if let Some((kind, lead_arity, lead_opts)) = deco_tail_of(&asc.ty) {
        if lead_arity > 0 {
            out.push(DecoExport {
                name: rb.name.name.clone(),
                kind,
                lead_arity,
                lead_opts,
                module_path: module_path.to_vec(),
                arg_downgrades: Vec::new(),
                unit_thunk: false,
            });
            return Ok(());
        }
    }
    match type_expr_bare_name(&asc.ty) {
        Some("deco") => {
            out.push(DecoExport {
                name: rb.name.name.clone(),
                kind: DecoKind::Deco,
                lead_arity: 0,
                lead_opts: Vec::new(),
                module_path: module_path.to_vec(),
                arg_downgrades: Vec::new(),
                unit_thunk: false,
            });
            Ok(())
        }
        // `rb.params` must be EXACTLY one `PatBot::Unit`: the `| ()` idiom is
        // the only legal spelling of a bare `deco-set` `let-rec`, and the
        // wrapper applies that unit thunk before matching the tuple (see this
        // section's banner). Any other params shape (empty, or a real
        // destructuring pattern) is outside the forward wrapper's scoped support.
        Some("deco-set") if matches!(rb.params.as_slice(), [cst::ast::PatBot::Unit { .. }]) => {
            out.push(DecoExport {
                name: rb.name.name.clone(),
                kind: DecoKind::DecoSet,
                lead_arity: 0,
                lead_opts: Vec::new(),
                module_path: module_path.to_vec(),
                arg_downgrades: Vec::new(),
                unit_thunk: true,
            });
            Ok(())
        }
        _ => reject_if_mentions_deco(&asc.ty, from, to),
    }
}

fn sig_item_value_ty(item: &cst::SigItem) -> Option<&TypeExpr> {
    use cst::SigItem;
    match item {
        SigItem::ValHorzCmd { ty, .. }
        | SigItem::ValVertCmd { ty, .. }
        | SigItem::Val { ty, .. }
        | SigItem::DirectHorzCmd { ty, .. }
        | SigItem::DirectVertCmd { ty, .. } => Some(ty),
        SigItem::Type { .. } => None,
    }
}

/// The value name a sig item declares, for the `Val` forms whose type can
/// carry a `deco` tail. Command items (`val \\cmd`/`val +cmd`, `direct`) are
/// deliberately excluded: a command's binder is not an ordinary identifier a
/// generated `let` could shadow.
fn sig_item_value_name(item: &cst::SigItem) -> Option<&str> {
    use cst::SigItem;
    match item {
        SigItem::Val { name, .. } => Some(name.name.as_str()),
        _ => None,
    }
}

/// If `te` is a (possibly arrow-prefixed) `deco`/`deco-set`, return its kind,
/// how many arguments precede the tail, and each of those positions'
/// optional-argument spelling. `length -> color -> color -> deco` is `(Deco,
/// 3, [Mandatory; 3])`; a bare `deco` is `(Deco, 0, [])`.
///
/// An OPTIONAL-argument arrow (`ty ?-> ..`) is NOT a rejection here: 0.0.6's
/// optionals are positional in this port (`lower_type_expr` gives each `ty
/// ?->` domain the mandatory type `option ty ->`), so `config ?-> length ->
/// deco` contributes TWO lead positions — `[V006Optional, Mandatory]` — and
/// the wrapper forwards both by value. See [`LeadOpt::V006Optional`] for the
/// one thing that still has to be reproduced (the `?:` marker).
///
/// 0.1's LABELLED-optional arrow (`?(l : τ) dom -> ..`,
/// `TypeExpr::OptRowFun`) DOES return `None`. It cannot appear in genuine
/// 0.0.6 source at all — `typecheck::check_type_expr_v0_1_only` rejects the
/// node under `V0_0` with a version error — so a dependency this classifier
/// sees carrying one is 0.1-shaped text in a 0.0.6 file, not something this
/// direction's positional wrapper should be guessing at.
fn deco_tail_of(te: &TypeExpr) -> Option<(DecoKind, usize, Vec<LeadOpt>)> {
    let mut lead_opts: Vec<LeadOpt> = Vec::new();
    let mut cur = te;
    loop {
        match cur {
            TypeExpr::Fun { opts, cod, .. } => {
                for _ in opts {
                    lead_opts.push(LeadOpt::V006Optional);
                }
                lead_opts.push(LeadOpt::Mandatory);
                cur = cod;
            }
            TypeExpr::OptRowFun { .. } => return None,
            _ => {
                let kind = match type_expr_bare_name(cur)? {
                    "deco" => DecoKind::Deco,
                    "deco-set" => DecoKind::DecoSet,
                    "paren" => DecoKind::Paren,
                    _ => return None,
                };
                return Some((kind, lead_opts.len(), lead_opts));
            }
        }
    }
}

/// If `te` TAKES one or more bare `deco`/`deco-set` arguments and its result
/// mentions neither, return the per-argument downgrade plan plus each
/// position's optional-argument spelling. Anything subtler — a deco nested
/// inside a product/application, one in BOTH argument and result position, or
/// one behind a `ty ?->` (whose domain is `option deco`, a compound the
/// singleton-list downgrade is not defined on) — returns `None` and falls
/// through to rejection.
fn deco_consumer_plan(te: &TypeExpr) -> Option<(Vec<Option<DecoKind>>, Vec<LeadOpt>)> {
    let mut plan: Vec<Option<DecoKind>> = Vec::new();
    let mut lead_opts: Vec<LeadOpt> = Vec::new();
    let mut cur = te;
    loop {
        match cur {
            TypeExpr::Fun { opts, dom, cod, .. } => {
                for o in opts {
                    // `ty ?->` is its own positional `option ty` slot, and it
                    // passes straight through — but only if it is not itself
                    // deco-shaped, which no `option`-wrapped downgrade covers.
                    if type_prod_mentions_deco(&o.ty).is_some() {
                        return None;
                    }
                    plan.push(None);
                    lead_opts.push(LeadOpt::V006Optional);
                }
                let dom_te = TypeExpr::Atom(dom.clone());
                plan.push(match type_expr_bare_name(&dom_te) {
                    Some("deco") => Some(DecoKind::Deco),
                    Some("deco-set") => Some(DecoKind::DecoSet),
                    _ => {
                        if type_expr_mentions_deco(&dom_te).is_some() {
                            return None;
                        }
                        None
                    }
                });
                lead_opts.push(LeadOpt::Mandatory);
                cur = cod;
            }
            TypeExpr::OptRowFun { .. } => return None,
            _ => {
                if type_expr_mentions_deco(cur).is_some() {
                    return None;
                }
                return if plan.iter().any(Option::is_some) {
                    Some((plan, lead_opts))
                } else {
                    None
                };
            }
        }
    }
}

fn type_expr_bare_name(te: &TypeExpr) -> Option<&str> {
    match te {
        TypeExpr::Atom(TypeProd {
            first:
                TypeApp {
                    head: TypeAtom::Name(n),
                    rest: app_rest,
                },
            rest,
        }) if rest.is_empty() && app_rest.is_empty() => Some(n.name.as_str()),
        _ => None,
    }
}

fn reject_if_mentions_deco(
    te: &TypeExpr,
    from: RustyfiVersion,
    to: RustyfiVersion,
) -> Result<(), BoundaryError> {
    if let Some(name) = type_expr_mentions_deco(te) {
        return Err(BoundaryError::ForkedTypeExport {
            binding: String::new(),
            ty_name: name.clone(),
            from,
            to,
            note: forked_note(&name),
        });
    }
    Ok(())
}

/// Structural (read-only) walk mirroring `relabel_type_expr`'s traversal —
/// `Some(name)` for the first `"deco"`/`"deco-set"` leaf found anywhere in
/// `te`, `None` if there is none.
fn type_expr_mentions_deco(te: &TypeExpr) -> Option<String> {
    match te {
        TypeExpr::Fun { opts, dom, cod, .. } => opts
            .iter()
            .find_map(|o| type_prod_mentions_deco(&o.ty))
            .or_else(|| type_prod_mentions_deco(dom))
            .or_else(|| type_expr_mentions_deco(cod)),
        TypeExpr::Atom(prod) => type_prod_mentions_deco(prod),
        TypeExpr::OptRowFun {
            opt_dom, dom, cod, ..
        } => opt_dom
            .entries
            .iter()
            .find_map(|e| type_expr_mentions_deco(&e.ty.0))
            .or_else(|| type_prod_mentions_deco(dom))
            .or_else(|| type_expr_mentions_deco(cod)),
    }
}

fn type_prod_mentions_deco(tp: &TypeProd) -> Option<String> {
    type_app_mentions_deco(&tp.first)
        .or_else(|| tp.rest.iter().find_map(|st| type_app_mentions_deco(&st.ty)))
}

fn type_app_mentions_deco(ta: &TypeApp) -> Option<String> {
    // `type_atom_mentions_deco` checks a bare `Name` against `deco_leaf_name`
    // and ignores a qualified `Mod.t`, so scanning every atom covers both the
    // arguments and the final constructor.
    std::iter::once(&ta.head)
        .chain(ta.rest.iter())
        .find_map(type_atom_mentions_deco)
}

fn type_atom_mentions_deco(atom: &TypeAtom) -> Option<String> {
    match atom {
        TypeAtom::Cmd { args, .. } => args.iter().find_map(|a| {
            a.opt_labels
                .iter()
                .find_map(|l| type_expr_mentions_deco(&l.ty.0))
                .or_else(|| type_expr_mentions_deco(&a.ty.0))
        }),
        TypeAtom::Paren { inner, .. } => type_expr_mentions_deco(&inner.0),
        TypeAtom::Record { fields, .. } => {
            fields.iter().find_map(|f| type_expr_mentions_deco(&f.ty.0))
        }
        TypeAtom::Var(_) => None,
        TypeAtom::Name(n) => deco_leaf_name(&n.name),
        // `Mod.t` — a qualified name; never itself a bare builtin fork name.
        TypeAtom::NameMod(_) => None,
        TypeAtom::RecordOpen { inner, .. } => inner
            .fields
            .iter()
            .find_map(|f| type_expr_mentions_deco(&f.ty.0)),
    }
}

fn deco_leaf_name(name: &str) -> Option<String> {
    if name == "deco" || name == "deco-set" || name == "paren" {
        Some(name.to_string())
    } else {
        None
    }
}

pub(crate) const XVER_UNITE_HELPER: &str = "xver-unite-graphics";
pub(crate) const XVER_AXIS_RATIO_HELPER: &str = "xver-math-axis-height-ratio";
pub(crate) const XVER_DOWN_DECO: &str = "xver-downgrade-deco";
pub(crate) const XVER_DOWN_DECOSET: &str = "xver-downgrade-decoset";

/// A `V0_1`-authored binding of [`XVER_UNITE_HELPER`], to be spliced BEFORE a
/// dependency whose module-scoped deco exports need wrapping.
///
/// An in-module wrapper cannot call `unite-graphics` itself. The whole module
/// is a spliced `V0_0` binding, so `elaborate.rs` wraps its members in
/// `Ast::VersionScope(V0_0, _)` — and under that scope `unite-graphics`, a
/// `V0_1`-only primitive, is an unbound variable at run time (observed, not
/// theorised). Top-level wrappers dodge this by being appended OUTSIDE the
/// dependency's index range; an in-module one has nowhere else to go.
///
/// So the `V0_1` primitive is captured once, outside any version scope, into
/// an ordinary user binding. Version scoping governs which `PrimDef` a
/// primitive NAME folds to; it does not change how a plain variable resolves,
/// so the scoped wrapper can call this helper and still get 0.1's
/// `unite-graphics`. Eta-expanded rather than bound bare so it goes through
/// the ordinary application path.
pub(crate) fn unite_helper_prelude() -> Vec<cst::TopBinding> {
    let src = format!(
        "let {XVER_UNITE_HELPER} xver-gs = unite-graphics xver-gs\n\
         let {XVER_AXIS_RATIO_HELPER} xver-c = get-math-axis-height-ratio xver-c\n\
         let {XVER_DOWN_DECO} xver-f xver-p xver-w xver-h xver-d =\n\
         \x20 [xver-f xver-p xver-w xver-h xver-d]\n\
         let {XVER_DOWN_DECOSET} xver-s =\n\
         \x20 match xver-s with\n\
         \x20 | (xver-s0, xver-s1, xver-s2, xver-s3) ->\n\
         \x20   ({XVER_DOWN_DECO} xver-s0, {XVER_DOWN_DECO} xver-s1,\n\
         \x20    {XVER_DOWN_DECO} xver-s2, {XVER_DOWN_DECO} xver-s3)\n"
    );
    rustyfi_syntax::parse_file(&src)
        .unwrap_or_else(|e| panic!("xver_adapt::unite_helper_prelude failed to parse: {e}"))
        .prelude
}

/// Whether any of `exports` needs [`unite_helper_prelude`] spliced — i.e. is
/// module-scoped, and so wrapped from INSIDE the dependency's version scope
/// where a `V0_1`-only primitive cannot be named directly.
pub(crate) fn needs_unite_helper(exports: &[DecoExport]) -> bool {
    exports
        .iter()
        .any(|e| !e.module_path.is_empty() || e.kind == DecoKind::Consumer)
}

/// The wrapper source for one export, as a struct/top-level `let` that COERCES
/// the already-spliced (`V0_0`-semantics, list-returning) value into the
/// single-`graphics` shape a `V0_1` consumer's call sites expect.
///
/// For [`DecoKind::Deco`], `lead_arity` extra parameters are forwarded
/// positionally before `deco`'s own four (point, length, length, length —
/// `prim_types::t_deco`'s arity) and the `graphics list` result is united via
/// the real `V0_1` `unite-graphics : list graphics -> graphics` primitive
/// (`primitives.rs`'s `prim_unite_graphics`), so `simple-frame : length ->
/// color -> color -> deco` becomes `let simple-frame xver-a0 xver-a1 xver-a2
/// xver-p xver-w xver-h xver-d = unite-graphics (simple-frame xver-a0 ..
/// xver-d)`. For [`DecoKind::DecoSet`], the original 4-tuple is destructured
/// and each component rewrapped the same way. Every generated identifier is
/// `xver-`-prefixed so it cannot capture one of the export's own
/// (unknown-to-us) parameter names.
///
/// [`DecoExport::unit_thunk`] distinguishes the two argument-less `deco-set`
/// spellings — see that field's own doc comment.
fn deco_wrapper_src(exp: &DecoExport) -> String {
    // A top-level wrapper is spliced outside the dependency's version-scoped
    // range and can name the primitive directly; an in-module one is inside
    // it and must go through the pre-bound helper (see above).
    let unite = if exp.module_path.is_empty() {
        "unite-graphics"
    } else {
        XVER_UNITE_HELPER
    };
    let lead: Vec<String> = (0..exp.lead_arity).map(|i| format!("xver-a{i}")).collect();
    // The ARGUMENT spelling is always positional — a 0.0.6 optional argument
    // IS an `option`-typed positional slot in this port, so forwarding one by
    // value is exact (`LeadOpt::V006Optional`). Only the PARAMETER spelling
    // differs: a `?:` marker is reproduced so the wrapper records the same
    // `Scope::optional_shape` the export declared, keeping marker-less call
    // sites working.
    let lead_args = if lead.is_empty() {
        String::new()
    } else {
        format!("{} ", lead.join(" "))
    };
    let lead_params = if lead.is_empty() {
        String::new()
    } else {
        let marked: Vec<String> = (0..exp.lead_arity)
            .map(|i| match exp.lead_opt(i) {
                LeadOpt::V006Optional => format!("?:xver-a{i}"),
                _ => format!("xver-a{i}"),
            })
            .collect();
        format!("{} ", marked.join(" "))
    };
    // With no optionals the wrapper re-applies the export by its own name
    // and relies on ordinary shadowing. With optionals it must go through a
    // private, shape-less alias instead — see `DecoExport::opt_src_alias` for
    // the marker-less-defaulting trap that forces it, and note the
    // PARENTHESISED right-hand side, which is what stops `elaborate.rs`'s
    // `alias_optional_shape` from copying the original's shape straight back
    // onto the alias.
    let alias = exp.opt_src_alias();
    let (orig, alias_binding) = if exp.has_optionals() {
        (
            alias.as_str(),
            format!("let {alias} = ({})\n", exp.name),
        )
    } else {
        (exp.name.as_str(), String::new())
    };
    // `get-font-size`/`get-text-color` exist under BOTH versions, so a scoped
    // wrapper may name them directly; the axis RATIO is V0_1-only and needs
    // the same pre-bound-helper treatment as `unite-graphics`.
    let axis_ratio = if exp.module_path.is_empty() {
        "get-math-axis-height-ratio"
    } else {
        XVER_AXIS_RATIO_HELPER
    };
    match exp.kind {
        // Contravariant: forward every argument, downgrading the deco-typed
        // ones. `xver-downgrade-deco` wraps a 0.1 deco's single `graphics`
        // result in a singleton list, which is exactly what the 0.0.6 callee's
        // `as_list` expects — the inverse of the `unite-graphics` upgrade.
        DecoKind::Consumer => {
            let args: Vec<String> = exp
                .arg_downgrades
                .iter()
                .enumerate()
                .map(|(i, down)| match down {
                    Some(DecoKind::DecoSet) => format!("({XVER_DOWN_DECOSET} xver-a{i})"),
                    Some(_) => format!("({XVER_DOWN_DECO} xver-a{i})"),
                    None => format!("xver-a{i}"),
                })
                .collect();
            let params: Vec<String> = (0..exp.arg_downgrades.len())
                .map(|i| match exp.lead_opt(i) {
                    LeadOpt::V006Optional => format!("?:xver-a{i}"),
                    _ => format!("xver-a{i}"),
                })
                .collect();
            format!(
                "{alias_binding}let {name} {} =\n\x20 {orig} {}\n",
                params.join(" "),
                args.join(" "),
                name = exp.name
            )
        }
        // 0.1 hands the closure `(h, signed d, ctx)`; 0.0.6 wants
        // `(h, signed d, axis, size, color)`. Both versions pass the SAME
        // signed depth (`make_paren_run` negates before either call), so h and
        // d forward untouched. The three extra arguments come out of the
        // context: `axis = size *' ratio` reproduces `MathC::axis(size)`
        // exactly (`primitives.rs`: `axis(s) = s * axis_height`), and `size` is
        // the LOCAL script-scaled one because `make_paren_run` sets
        // `c2.font_size = size` before applying — the detail whose absence
        // would silently oversize every script-level delimiter.
        DecoKind::Paren => format!(
            "{alias_binding}let {name} {lead_params}xver-h xver-d xver-ctx =\n\
             \x20 {orig} {lead_args}xver-h xver-d\n\
             \x20   ((get-font-size xver-ctx) *' ({axis_ratio} xver-ctx))\n\
             \x20   (get-font-size xver-ctx)\n\
             \x20   (get-text-color xver-ctx)\n",
            name = exp.name
        ),
        DecoKind::Deco => format!(
            "{alias_binding}let {name} {lead_params}xver-p xver-w xver-h xver-d =\n\
             \x20 {unite} ({orig} {lead_args}xver-p xver-w xver-h xver-d)\n",
            name = exp.name
        ),
        DecoKind::DecoSet => {
            // The original binding, applied to whatever it needs before its
            // 4-tuple is reachable: the mandatory `()` thunk of a bare
            // `let-rec name : deco-set | () = ..` (`unit_thunk`), or — for an
            // arrow-tailed `deco-set` — the same leading arguments the
            // wrapper itself just took.
            let scrutinee = if exp.unit_thunk {
                format!("{orig} ()")
            } else if lead.is_empty() {
                orig.to_string()
            } else {
                format!("{orig} {}", lead.join(" "))
            };
            let mut out = format!(
                "{alias_binding}let {name} {lead_params}=\n\
                 \x20 match {scrutinee} with\n\
                 \x20 | (xver-d0, xver-d1, xver-d2, xver-d3) ->\n",
                name = exp.name
            );
            let wrap = |i: usize| {
                format!(
                    "(fun xver-p xver-w xver-h xver-d -> \
                     {unite} (xver-d{i} xver-p xver-w xver-h xver-d))"
                )
            };
            out.push_str(&format!(
                "   ({}, {}, {}, {})\n",
                wrap(0),
                wrap(1),
                wrap(2),
                wrap(3)
            ));
            out
        }
    }
}

/// Append each module-scoped [`DecoExport`]'s wrapper INSIDE its own module,
/// as one more `StructDecl` after the export's original binding.
///
/// This is the half `deco_coercion_prelude` cannot do. A module member is
/// reached as `Deco.simple-frame`, and there is no syntax for a top-level
/// `let Deco.simple-frame = ..`, so the shadow has to live one scope deeper.
/// `elaborate.rs`'s `walk_bindings` folds a module's `decls` sequentially
/// through a `running` scope, so a later decl of the same name shadows the
/// earlier one and the module's export surface picks up the wrapper —
/// exactly the mechanism the top-level case already relies on.
///
/// The decls are built by parsing a synthetic `module .. = struct .. end`
/// and lifting its `decls`, so the wrapper text goes through the real parser
/// rather than being hand-constructed as CST.
pub(crate) fn inject_module_deco_wrappers(prelude: &mut [cst::TopBinding], exports: &[DecoExport]) {
    for tb in prelude.iter_mut() {
        inject_into_top_binding(tb, &[], exports);
    }
}

fn inject_into_top_binding(tb: &mut cst::TopBinding, path: &[String], exports: &[DecoExport]) {
    let cst::TopBinding::Module { name, decls, .. } = tb else {
        return;
    };
    let mut here = path.to_vec();
    here.push(name.name.clone());
    let mine: Vec<&DecoExport> = exports.iter().filter(|e| e.module_path == here).collect();
    if !mine.is_empty() {
        let mut src = String::from("module XverWrap = struct\n");
        for exp in &mine {
            // Keep the UNWRAPPED original reachable under a private
            // sibling name before the wrapper shadows it — see
            // `DecoExport::orig_capture_name` for why it must live in this
            // scope, and `deco_upgrade_prelude`'s **Placement** section for
            // what reads it.
            src.push_str(&format!(
                "let {} = {}\n",
                exp.orig_capture_name(),
                exp.name
            ));
            src.push_str(&deco_wrapper_src(exp));
        }
        src.push_str("end\n");
        let file = rustyfi_syntax::parse_file(&src).unwrap_or_else(|e| {
            panic!(
                "xver_adapt::inject_module_deco_wrappers: internally-generated X3b \
                 wrapper source failed to parse (a bug in xver_adapt.rs, not user \
                 input): {e}\n--- generated source ---\n{src}"
            )
        });
        if let Some(cst::TopBinding::Module { decls: gen, .. }) = file.prelude.into_iter().next() {
            decls.extend(gen);
        }
    }
    for d in decls.iter_mut() {
        inject_into_top_binding(&mut d.0, &here, exports);
    }
}

/// The TOP-LEVEL half of the forward wrapper's wrapping: one shadowing `let` per top-level
/// [`DecoExport`] ([`deco_wrapper_src`]), parsed via
/// [`rustyfi_syntax::parse_file`]. `panic!`s on a parse failure, since that
/// would mean this function itself generated malformed syntax (an internal
/// bug), never a symptom of the user's own dependency source.
pub(crate) fn deco_coercion_prelude(exports: &[DecoExport]) -> Vec<cst::TopBinding> {
    if exports.is_empty() {
        return Vec::new();
    }
    let mut src = String::new();
    for exp in exports {
        // Module-scoped exports are wrapped in place by
        // `inject_module_deco_wrappers`; a top-level shadow cannot name them.
        if !exp.module_path.is_empty() {
            continue;
        }
        // The unwrapped original, kept reachable under a private name
        // before the wrapper shadows it (see `inject_module_deco_wrappers`
        // for the module-scoped twin, and `deco_upgrade_prelude` for what
        // reads it).
        src.push_str(&format!(
            "let {} = {}\n",
            exp.orig_capture_name(),
            exp.name
        ));
        src.push_str(&deco_wrapper_src(exp));
    }
    if src.is_empty() {
        return Vec::new();
    }
    // Deliberately NO trailing dummy body: `File.body` is legitimately
    // `Option`-al (`cst.rs`'s doc comment — "Absent for a library file
    // (`nxtopsubseq`'s bare `EOI` case)"), and a bare literal like `0` is a
    // valid ATOM that a preceding `let`'s value expression's application
    // chain would happily keep consuming as one more argument (nothing
    // about a top-level decl boundary is whitespace-sensitive here — only a
    // following reserved keyword like `let`/`type`/`module` stops an
    // application chain). Parsing as a bare `prelude* EOI` library file
    // sidesteps that trap entirely; only `.prelude` is ever read below.
    let file = rustyfi_syntax::parse_file(&src).unwrap_or_else(|e| {
        panic!(
            "xver_adapt::deco_coercion_prelude: internally-generated X3b wrapper \
             source failed to parse (a bug in xver_adapt.rs, not user input): {e}\n\
             --- generated source ---\n{src}"
        )
    });
    file.prelude
}

// ============================================================================
// WHICH consumers see the forward wrapper's adapted view.
//
// The forward wrapper installs the 0.1-shaped view of a crossed `deco`/`deco-set`/`paren`
// export by SHADOWING the export's own name: a later `StructDecl` inside the
// exporting module (`inject_module_deco_wrappers`), or a later top-level
// binding (`deco_coercion_prelude`). Both are permanent — the merged prelude
// is one flat `Ast::LetIn` chain and `Ast::VersionScope(V0_0, _)` wraps a
// binding's RHS, never the continuation after it, so a shadow is visible to
// EVERYTHING that follows regardless of which generation authored it.
//
// That is right for the 0.1 entry and wrong for a later 0.0.6-AUTHORED
// dependency, which is elaborated in `Ast::VersionScope(V0_0, _)` and means
// 0.0.6's shape by every name it writes. Multi-package 0.0.6 corpora hit it
// constantly, because a package that exports a `deco`/`paren` is exactly the
// kind of package other packages build on:
//
//   - `math.satyh` declares `val paren-right : paren` and `latexcmds` applies
//     it with 0.0.6's five arguments — `type mismatch: expected `length`,
//     found `context``, unlocated, from a document that named neither file;
//   - the same for `deco`: an exporter's `graphics list` result is united into
//     one `graphics`, and the next 0.0.6 package's `inline-frame-outer` (typed
//     `t_deco(V0_0)` inside its own version scope) refuses it with `expected
//     `graphics list`, found `graphics``.
//
// So the adapted view is POSITION-INDEXED rather than permanent — the exact
// mirror of the reverse wrapper's placement schedule in the other direction. What makes a
// position-indexed view sufficient is unchanged from the reverse wrapper: each block
// `lib.rs`'s forward loop splices is homogeneous (a `V0_0` dependency's whole
// `prelude` goes into `v006_indices`, a `V0_1` dependency's whole `lowered`
// stays out of it), the entry is 0.1-authored and last, and the loader orders
// dependencies topologically so a consumer always follows what it
// `@require:`s.
//
// The three steps are [`UpgradeStep`]; both transitions are lazy, so a program
// whose 0.0.6 dependencies never consume each other's crossed exports (the
// single-dependency case) emits NOTHING.
// ============================================================================

/// Which of the view-scheduling mechanism's three placement bindings [`deco_upgrade_prelude`] should
/// generate. The forward twin of [`DowngradeStep`], and deliberately its
/// mirror image: there the 0.1 view is the resting state and the 0.0.6 one is
/// installed at a transition, here the 0.1 view is what the forward wrapper has already
/// installed and the 0.0.6 one is what a transition has to put BACK.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub(crate) enum UpgradeStep {
    /// `let xver-fwd-view-M-frame = M.frame` — capture the forward wrapper's WRAPPED view
    /// under a private name, so a later [`Install`](UpgradeStep::Install) can
    /// put it back without regenerating the wrapper. Binds a private name
    /// only, so it is invisible to consumers of either generation. Emitted
    /// once per export, at the first transition into 0.0.6-authored code —
    /// which is the last position at which naming the export's own key still
    /// yields the wrapped view.
    Capture,
    /// `let M.frame = M.xver-fwd-orig-frame` — put the UNWRAPPED, 0.0.6-shaped
    /// original back. Emitted on entering a 0.0.6-authored block. The
    /// right-hand side is the in-place capture the forward wrapper's two injectors emit next
    /// to the original itself (`DecoExport::orig_capture_name`).
    Restore,
    /// `let M.frame = xver-fwd-view-M-frame` — re-install the 0.1-shaped view
    /// from [`Capture`](UpgradeStep::Capture). Emitted on entering a
    /// 0.1-authored block (a foreign 0.1 dependency, or the entry) once the
    /// 0.0.6 view has been restored.
    Install,
}

/// Build the `V0_1`-authored placement bindings for `exports` — see
/// [`UpgradeStep`] for which of the three this call emits, and this section's
/// banner for why the view has to move at all.
///
/// [`Restore`](UpgradeStep::Restore) and [`Install`](UpgradeStep::Install)
/// both REBIND the export's own key, which for a module member is the dotted
/// `M.frame`. No surface syntax spells a top-level `let M.frame = ..`, but
/// `elaborate.rs`'s `push_named_binding` takes the binder name as an opaque
/// `String`, so — exactly as [`deco_downgrade_prelude`] does in the other
/// direction — the binding is parsed for its SHAPE under a private name whose
/// `BindName` is then replaced by the qualified key.
///
/// **Why `Restore`'s right-hand side is a MEMBER and `Install`'s is not.**
/// `Install` puts back a value that exists at top level the moment the forward
/// wrapper has run, so a top-level capture reaches it. `Restore` puts back the
/// value the wrapper SHADOWED, which at top level no longer has a name at all
/// — hence the in-place `xver-fwd-orig-` sibling the forward wrapper's injectors now emit next
/// to the original. That sibling is reachable from outside because a 0.0.6
/// `module M : sig .. end = struct .. end` SEALS NOTHING in this port:
/// `elaborate.rs`'s `TopBinding::Module` arm accepts `val` items and ignores
/// them (only `direct` items bind anything), and `v1::module_check`'s
/// `static_env.seals` is built from the 0.1 `cst_v1` dependencies alone. So
/// the extra member neither changes the module's declared surface nor trips a
/// conformance check.
///
/// **Optional shapes.** A 0.0.6 export may carry `?:`-marked leading
/// parameters, and `elaborate.rs`'s `Scope::optional_shape` follows a bare
/// `let x = y` alias (`alias_optional_shape`). That is what these three want:
/// every binding here is a bare `Var`/`VarWithMod` alias, so the restored
/// original keeps the 0.0.6 shape its marker-less call sites need and the
/// re-installed wrapper keeps the shape it declared. (The wrapper's OWN
/// shape-less source alias is a separate, parenthesised binding —
/// [`DecoExport::opt_src_alias`].)
pub(crate) fn deco_upgrade_prelude(
    exports: &[DecoExport],
    step: UpgradeStep,
) -> Vec<cst::TopBinding> {
    if exports.is_empty() {
        return Vec::new();
    }
    let mut src = String::new();
    let mut shadow_names: Vec<(String, String)> = Vec::new();
    for exp in exports {
        let qualified = exp.qualified_key();
        let view = exp.view_capture_name();
        match step {
            UpgradeStep::Capture => {
                src.push_str(&format!("let {view} = {qualified}\n"));
            }
            UpgradeStep::Restore => {
                let shadow = format!("xver-fwd-shadow-{}", exp.dash_key());
                src.push_str(&format!("let {shadow} = {}\n", exp.orig_capture_key()));
                shadow_names.push((shadow, qualified));
            }
            UpgradeStep::Install => {
                let shadow = format!("xver-fwd-shadow-{}", exp.dash_key());
                src.push_str(&format!("let {shadow} = {view}\n"));
                shadow_names.push((shadow, qualified));
            }
        }
    }
    // Parsed as a bare `prelude* EOI` library file, for the same reason
    // `deco_coercion_prelude` is — see its comment about a trailing dummy body
    // being swallowed by the preceding application chain.
    let file = rustyfi_syntax::parse_file(&src).unwrap_or_else(|e| {
        panic!(
            "xver_adapt::deco_upgrade_prelude: internally-generated X3c placement \
             source failed to parse (a bug in xver_adapt.rs, not user input): {e}\n\
             --- generated source ---\n{src}"
        )
    });
    let mut prelude = file.prelude;
    rebind_shadows_to_qualified(&mut prelude, &shadow_names, "deco_upgrade_prelude");
    prelude
}

/// Replace each generated `let {shadow} = ..`'s binder with the dotted
/// qualified key it stands for. Shared by [`deco_upgrade_prelude`] and
/// [`deco_downgrade_prelude`]: both need a top-level binding of a name
/// no surface syntax can spell, and both get it the same way — parse under a
/// private name, then swap the `BindName`, which `elaborate.rs`'s
/// `push_named_binding` treats as an opaque `String`.
fn rebind_shadows_to_qualified(
    prelude: &mut [cst::TopBinding],
    shadow_names: &[(String, String)],
    who: &str,
) {
    for (shadow, qualified) in shadow_names {
        let mut found = false;
        for tb in prelude.iter_mut() {
            if let cst::TopBinding::Let(tl) = tb {
                if tl.name.name == *shadow {
                    tl.name = cst::BindName::from(rustyfi_syntax::leaf::VarTok {
                        name: qualified.clone(),
                        span: tl.name.span,
                    });
                    found = true;
                    break;
                }
            }
        }
        assert!(
            found,
            "xver_adapt::{who}: generated shadow `{shadow}` vanished from its own \
             parse (a bug in xver_adapt.rs)"
        );
    }
}

// ============================================================================
// The reverse deco/paren coercion (the reverse mirror of the forward wrapper, above): a foreign `V0_1` dependency's
// `deco`/`deco-set` export returns a single `graphics` (0.1 semantics); every
// REAL `V0_0`-authored consumer call site
// (`primitives::apply_deco`/`coerce_graphics_result`, fired at render time
// under `interp.version == V0_0` — `lib.rs`'s
// `compile_document_v006_xver_with_trials` always calls
// `eval_document_trials(.., RustyfiVersion::V0_0)`) expects a `graphics list`
// back (`coerce_graphics_result`'s `!graphics_is_collection()` branch,
// `as_list`). The coercion is the literal INVERSE of the forward wrapper's `unite-graphics`
// wrap: a SINGLETON LIST, `let name p w h d = [name p w h d]`. It is a
// type-level requirement too, not merely a runtime one — a 0.0.6-authored
// consumer is elaborated inside `Ast::VersionScope(V0_0, _)`, where
// `inline-frame-outer`/`inline-frame-breakable` carry
// `t_deco(V0_0)`/`t_decoset(V0_0)`, so an unwrapped 0.1 deco fails to unify
// long before eval.
//
// **Where the export's type is NAMED, and what that costs.** 0.1's grammar
// has NO bare top-level type-ascription syntax at all (`cst_v1::Bind::
// Value`/`ValueRec`'s own doc comments — no `: ty` on a plain `val`/`val
// rec`), so the ONLY textual site a 0.1 export's `deco`/`deco-set` type can
// ever be NAMED is a `module M :> sig val name : deco .. end = struct ..
// end` SIG item — which is exactly what `classify_deco_exports_v01_sig`
// (below) reads, off the PRE-lowering `cst_v1::FileV1` (lowering DROPS
// `sig_annot`). An UNANNOTATED 0.1 deco export is therefore invisible to
// this scan and does NOT cross; it fails with an ordinary `TypeError` at the
// consumer's call site, exactly as it did before this coercion existed. That is a
// false-NEGATIVE (a refusal), never a false-accept.
//
// **The one obstacle, and how it is resolved.** Every 0.1 module signature
// annotation is the `:>` (COERCE) form (`SigAnnotV1.coerce: CoerceTok`,
// unconditionally), and `v1::module_check`'s phase-D spine walk
// conformance-checks EVERY such annotation for EVERY `Ast::LetIn` node whose
// name matches a `static_env.seals` entry. That check is PURELY NAME-KEYED,
// not "first occurrence only", so the coercion shadow (a second binding of the
// same qualified name, whose whole POINT is to have a DIFFERENT shape from the
// module's declared `deco`) trips it no matter where it is spliced — verified
// empirically for both candidate positions (inside the module's own `decls`,
// and as a later top-level binding under the same dotted key).
//
// The resolution is an EXPLICIT, caller-supplied exemption rather than a
// trick: `lib.rs`'s reverse arm passes the set of qualified names it is about
// to shadow to `v1::module_check::check_program_with_xver_shadows`, and that
// walk exempts only the SECOND-and-later `Ast::LetIn` of such a name — the
// FIRST, the module's own export alias, is still fully conformance-checked
// against the declared `deco`. Nothing is left unchecked by that exemption:
// the shadow's own body is `[orig a.. p w h d]` where `orig` is bound to the
// module's SEALED scheme, so ordinary HM inference proves its type is exactly
// `t_deco(V0_0)`, with the same leading prefix.
//
// **Placement — which consumers see the adapted view.** The adapted view is
// SCHEDULED, not permanent: captured once under a private name while the 0.1
// view is in force, INSTALLED lazily on entering a 0.0.6-authored block,
// RESTORED on entering a 0.1-authored one. See
// [`DowngradeStep`]/[`deco_downgrade_prelude`]'s **Placement** section for the
// full derivation.
//
// A bare `type foo = deco` synonym (no value attached — safe with zero
// coercion, the same reasoning as the forward direction's `type
// xver-deco-alias = deco`) is unaffected: it is not a sig `val` item at all,
// so this scan never sees it, and the ordinary POST-lowering
// `collect_free_globals` scan (`lib.rs`) already lets it splice verbatim.
// ============================================================================

/// Classify every `deco`/`deco-set` VALUE export in a foreign `V0_1`
/// dependency's OWN top-level module signature, so `lib.rs`'s reverse splice
/// arm can generate a downgrade wrapper per export
/// ([`deco_downgrade_prelude`]); reject any `deco`-family mention this
/// positional wrapper cannot express. Operates on the dependency's file's
/// ORIGINAL, PRE-lowering `cst_v1::FileV1` — `v1::lower::
/// lower_file_v1_with_surfaces` DROPS a 0.1 module's `sig_annot` entirely
/// (`v1/lower.rs`'s own "sig_annot is then simply DROPPED" doc comment),
/// so this is the only stage at which the sig's text still exists; the
/// ordinary POST-lowering `collect_free_globals` scan (`lib.rs`) can never
/// see it.
///
/// Each returned [`DecoExport`] carries the exporting module chain as its
/// `module_path` — the top-level module's own name, plus one segment per
/// nested `Decl::Module` the scan descended through — so the generated shadow
/// can name the member the way a consumer does (`M.name`, `M.Inner.name`).
///
/// `Ok(vec![])` for a `FileV1::Document` (never a dependency), a `Library`
/// with no `sig_annot` at all, or one whose signature this scan cannot resolve
/// to a concrete decl list at all (see the "what still does not resolve" list
/// below) — a forked type hiding behind one of those is NOT a soundness gap:
/// HM still infers the crossing value's REAL shape at every use
/// site regardless of what this textual scan saw, so the worst case is an
/// ordinary `TypeError` far from its cause, never silent corruption.
///
/// A `deco` reached through a NESTED `module M : ..` decl DOES cross. The
/// generated shadow must name the member under exactly the qualified key
/// `v1::module_check` seals it by, `lower::qualify_type_key(mod_path,
/// member)` — the SAME `mod_path` `walk_nested_seals_a` composes by pushing
/// each nested `Bind::Module`'s own name onto its parent's
/// (`module_check.rs`'s `child_path`), and the one
/// `elaborate::push_named_binding` binds the member's export alias under. So
/// the recursion below pushes each nested `Decl::Module`'s name onto
/// `module_path`, and [`deco_export_qualified_name`] spells
/// `Outer.Inner.frame` — the `env.seals` key, the `Ast::LetIn` binder name,
/// and the string a 0.0.6 consumer's reference resolves through, all at once.
///
/// **NON-literal nested signatures resolve too**, not just a literal `sig ..
/// end`: [`v01_resolve_sig_decls`] dereferences a named reference (`module M :
/// S`, `module M : A.B.S`) and a `with type` refinement through the very table
/// `v1::module_check`'s own `resolve_sig` consults — `surface::find_sig_keyed`,
/// keyed and searched OUTWARD from the same `site_path`. `include` resolves
/// too, and splices at the ENCLOSING path rather than a lengthened one,
/// mirroring `module_check::splice_decls`. `signature S = ..` is SKIPPED
/// rather than rejected: a signature member declares no value at any path, so
/// nothing a 0.0.6 consumer can name hides behind one — but the definition it
/// registers is what a sibling `module M : S` resolves through.
///
/// **What still does not resolve, and why it is genuine.** Two shapes stay
/// unresolvable AT THIS POINT IN THE PIPELINE, and each keeps its precise
/// textual rejection ([`v1_reject_if_mentions_deco`], so a `deco` reachable
/// from one rejects rather than silently splicing):
///
/// - a FUNCTOR signature member (`module Make : (X : S1) -> S2`). A functor is
///   not a module: there is no member path `Outer.Make.frame` for a shadow to
///   rebind, and 0.0.6 has no syntax that could apply one. Its members become
///   reachable only through an APPLICATION (`module Inst = Outer.Make Arg`),
///   which `v1::functor` re-lowers at the APPLICATION's own path — in a
///   different file, possibly one this loop has not read yet. The path the
///   shadow would have to name is therefore not a function of this file's
///   signature at all;
/// - a named reference that does not resolve (unknown signature name, or an
///   `include`/`module` cycle through names). Both are hard, precise errors
///   from `module_check::resolve_sig` a moment later; this scan simply
///   declines to guess.
pub(crate) fn classify_deco_exports_v01_sig<'a>(
    file: &'a cst_v1::FileV1,
    surfaces: &SurfaceEnv<'a>,
) -> Result<Vec<DecoExport>, BoundaryError> {
    let cst_v1::FileV1::Library {
        name,
        sig_annot: Some(sig_annot),
        ..
    } = file
    else {
        return Ok(Vec::new());
    };
    let module_path = vec![name.name.clone()];
    let mut out = Vec::new();
    let mut visited: Vec<String> = Vec::new();
    classify_v01_sig_expr(
        &sig_annot.sig_.0,
        &module_path,
        surfaces,
        &mut visited,
        &V01Syns::default(),
        &[],
        &mut out,
    )?;
    Ok(out)
}

/// One signature EXPRESSION's value exports at `module_path` — resolve it to a
/// decl list first ([`v01_resolve_sig_decls`]), then classify that list.
///
/// `visited` is the named-signature cycle guard, keyed (like `module_check::
/// resolve_named_sig`'s own) by the RESOLVED table key rather than the written
/// suffix, so two differently-pathed same-suffix signatures do not
/// false-positive. A re-entry yields NO exports rather than an error: an
/// `include`/`module` cycle through names is `module_check::resolve_sig`'s own
/// precise diagnostic a moment later, and this scan never invents user-facing
/// text for it.
/// `inherited_refines` are an ENCLOSING layer's `with ⟨chain⟩ type`
/// refinements addressed to this signature (already stripped of the segments
/// that named the way here) — the same routing `module_check::
/// prescan_seal_types` performs, so what makes a member's type transparent
/// there makes it visible here.
fn classify_v01_sig_expr<'a>(
    se: &'a cst_v1::ast::SigExpr,
    module_path: &[String],
    surfaces: &SurfaceEnv<'a>,
    visited: &mut Vec<String>,
    syns: &V01Syns<'a>,
    inherited_refines: &[surface::Refine<'a>],
    out: &mut Vec<DecoExport>,
) -> Result<(), BoundaryError> {
    let Some(mut resolved) = v01_resolve_sig_decls(se, module_path, surfaces) else {
        // Genuinely unresolvable here (see [`classify_deco_exports_v01_sig`]'s
        // doc comment for the per-shape derivation) — guard textually, so a
        // `deco` reachable from one rejects rather than silently splicing.
        return v1_reject_if_mentions_deco(se, syns);
    };
    resolved.refines.extend(inherited_refines.iter().cloned());
    // This layer's OWN transparent type declarations (and any `with type`
    // refinement that made an opaque one transparent) extend the enclosing
    // signature's synonyms before a single `val` is classified — see
    // [`V01Syns`].
    let inner = syns.extended(resolved.decls, &resolved.refines, module_path, surfaces);
    let Some(k) = resolved.key else {
        // A LITERAL `sig .. end`: nesting is finite, no guard needed (the same
        // argument `module_check`'s own cycle guard rests on).
        return classify_v01_sig_decls(
            resolved.decls,
            module_path,
            surfaces,
            visited,
            &inner,
            &resolved.refines,
            out,
        );
    };
    if visited.contains(&k) {
        return Ok(());
    }
    visited.push(k);
    let r = classify_v01_sig_decls(
        resolved.decls,
        module_path,
        surfaces,
        visited,
        &inner,
        &resolved.refines,
        out,
    );
    visited.pop();
    r
}

/// One `sig .. end` body's decls, at the module path `module_path` — recursive
/// through `Decl::Module` (see [`classify_deco_exports_v01_sig`]'s doc comment
/// for why the composed path is exactly the seal key) and through
/// `Decl::Include` (at the SAME path, mirroring `module_check::splice_decls`).
fn classify_v01_sig_decls<'a>(
    decls: &'a [cst_v1::StructDeclV1],
    module_path: &[String],
    surfaces: &SurfaceEnv<'a>,
    visited: &mut Vec<String>,
    syns: &V01Syns<'a>,
    refines: &[surface::Refine<'a>],
    out: &mut Vec<DecoExport>,
) -> Result<(), BoundaryError> {
    for d in decls {
        match &*d.0 {
            cst_v1::ast::Decl::Val { name, ty, .. } => match v1_deco_tail_of(ty, syns) {
                Some((kind, lead_arity, lead_opts)) if kind != DecoKind::Paren => {
                    out.push(DecoExport {
                        name: name.name.clone(),
                        kind,
                        lead_arity,
                        lead_opts,
                        module_path: module_path.to_vec(),
                        arg_downgrades: Vec::new(),
                        unit_thunk: false,
                    })
                }
                // A `paren` export, or a `deco` this wrapper cannot express (a
                // leaf buried in a compound, or an optional-argument row this
                // direction's bounded case split will not enumerate — a row
                // VARIABLE tail, or more than `V01_MAX_OPT_LABELS` labels):
                // reject, loudly and specifically.
                _ => v1_reject_if_mentions_deco_ty(ty, syns)?,
            },
            cst_v1::ast::Decl::Module { name, sig_, .. } => {
                let mut inner = module_path.to_vec();
                inner.push(name.name.clone());
                // A `with N ⟨…⟩ type t = τ` refinement addressed to THIS
                // member descends into it with one segment consumed —
                // `prescan_seal_types`' own routing, reproduced.
                let child_refines: Vec<surface::Refine<'a>> = refines
                    .iter()
                    .filter(|r| r.path.first() == Some(&name.name))
                    .map(|r| {
                        let mut r = r.clone();
                        r.path.remove(0);
                        r
                    })
                    .collect();
                classify_v01_sig_expr(
                    sig_,
                    &inner,
                    surfaces,
                    visited,
                    syns,
                    &child_refines,
                    out,
                )?;
            }
            // `include S` splices S's OWN decls into the enclosing signature
            // in place, at the enclosing path — `module_check::splice_decls`,
            // so this layer's refinements apply to what it splices in.
            cst_v1::ast::Decl::Include { sig_, .. } => {
                classify_v01_sig_expr(sig_, module_path, surfaces, visited, syns, refines, out)?;
            }
            // `signature S = ..` declares a SIGNATURE, not a value: no member
            // of it is reachable at any path (`handle_signature_decl` only
            // identity-checks it against the struct's own `signature` bind, and
            // 0.0.6 has no signature syntax at all), so there is nothing here
            // to cross and nothing to refuse. `surface::build_file_surface`
            // has already registered the definition itself, which is what a
            // sibling `module M : S` resolves through.
            cst_v1::ast::Decl::Signature { .. } => {}
            other => {
                if let Some(n) = v1_decl_mentions_deco(other, syns) {
                    return Err(v1_boundary_error(&n));
                }
            }
        }
    }
    Ok(())
}

/// Resolve one signature expression to the decl list it denotes, plus the
/// `surfaces.sigs` table key it came from (`None` for a literal `sig .. end`,
/// which needs no cycle guard). `None` for the two genuinely unresolvable
/// shapes enumerated in [`classify_deco_exports_v01_sig`]'s doc comment.
///
/// Deliberately the SAME lookup `v1::module_check`'s `resolve_sig_bot`
/// performs — `surface::find_sig_keyed`, searched outward from `site_path` —
/// so a member found here sits at exactly the path `module_check` seals it
/// under, and the SAME `with type` refinement composition (an inline node's
/// own `binds`, plus a named signature's stored [`surface::SigDef::refines`])
/// — a refinement never changes a `val` decl's SPELLED type, but it DOES turn
/// an opaque `type t :: o` into the transparent synonym a `val` decl's
/// spelling may then name ([`V01Syns`]). What it deliberately does NOT
/// reproduce is `resolve_sig`'s eager `Decl::Include` flattening (this scan
/// recurses through `Decl::Include` in place instead, which is the same
/// traversal).
struct V01ResolvedSig<'a> {
    decls: &'a [cst_v1::StructDeclV1],
    /// The `surfaces.sigs` table key this came from — `None` for a literal
    /// `sig .. end`, which needs no cycle guard.
    key: Option<String>,
    refines: Vec<surface::Refine<'a>>,
}

fn v01_resolve_sig_decls<'a>(
    se: &'a cst_v1::ast::SigExpr,
    site_path: &[String],
    surfaces: &SurfaceEnv<'a>,
) -> Option<V01ResolvedSig<'a>> {
    use cst_v1::ast::SigExpr;
    match se {
        SigExpr::Bot(bot) => v01_resolve_sig_bot(bot, site_path, surfaces),
        SigExpr::WithType {
            base, path, binds, ..
        } => {
            let mut resolved = v01_resolve_sig_bot(base, site_path, surfaces)?;
            resolved
                .refines
                .extend(surface::collect_refines(binds, mod_chain_segments(path)));
            Some(resolved)
        }
        // A functor SIGNATURE — not a module signature; see the doc comment.
        SigExpr::Functor { .. } => None,
    }
}

fn v01_resolve_sig_bot<'a>(
    bot: &'a cst_v1::ast::SigBotV1,
    site_path: &[String],
    surfaces: &SurfaceEnv<'a>,
) -> Option<V01ResolvedSig<'a>> {
    use cst_v1::ast::SigBotV1;
    match bot {
        SigBotV1::Sig { decls, .. } => Some(V01ResolvedSig {
            decls: decls.as_slice(),
            key: None,
            refines: Vec::new(),
        }),
        SigBotV1::Var(t) => {
            surface::find_sig_keyed(surfaces, site_path, &t.name).map(|(key, def)| V01ResolvedSig {
                decls: def.decls,
                key: Some(key),
                refines: def.refines.clone(),
            })
        }
        SigBotV1::Path(t) => {
            let suffix = surface::sig_path_suffix(&t.mods, &t.name);
            surface::find_sig_keyed(surfaces, site_path, &suffix).map(|(key, def)| V01ResolvedSig {
                decls: def.decls,
                key: Some(key),
                refines: def.refines.clone(),
            })
        }
    }
}

/// The transparent type SYNONYMS a signature layer's `val` decls may name —
/// the whole of what makes
///
/// ```text
/// module M :> sig  type t = deco  val frame : length -> t  end = struct .. end
/// ```
///
/// cross. The scan reads a `val`'s SPELLED type, so without this the tail
/// reads as the bare name `t`, matches no forked builtin, and the export
/// silently declines to cross (surfacing much later as an ordinary
/// `TypeError` at a 0.0.6 consumer's call site rather than as this module's
/// own boundary diagnostic).
///
/// One entry per type name DECLARED by the signature layer being scanned, or
/// by any enclosing one (a nested `sig` sees its parent's type declarations,
/// and an `include`d signature's declarations splice into the includer's own
/// scope — so the map is threaded down, extended, never reset):
///
/// - `Some(body)` — a TRANSPARENT `type t = τ` with NO parameters, whose body
///   is kept whole and expanded IN PLACE at the tail
///   ([`v1_deco_tail_of`])/at a leaf ([`V01Syns::mentions_deco`]). Keeping the
///   body (rather than a pre-resolved verdict) is what makes an arrow-bodied
///   synonym — `type frame = length -> deco` — contribute its own lead
///   positions to the generated wrapper, exactly as if it had been spelled
///   out;
/// - `None` — a name this layer declares but that names no expandable
///   synonym: an OPAQUE `type t :: o`, a PARAMETERISED `type t 'a = ..` (a
///   bare `t` reference to which is ill-typed anyway), or a variant body.
///   Recorded rather than omitted so that it SHADOWS an enclosing layer's
///   entry — and so that a locally-declared name never falls through to the
///   builtin lookup below it.
///
/// A `with type t = τ` refinement (inline, or inherited from a named
/// signature's own stored refinements) is absorbed AFTER the decls, since its
/// whole job is to overwrite the `None` an opaque `type t :: o` just wrote.
///
/// Lookup is MAP-FIRST, builtin-second: a signature that declares its own
/// `type deco` shadows the builtin of that name for the layers below it, and
/// this scan must not then generate a coercion wrapper for a value that is
/// not a `deco` at all.
#[derive(Default, Clone)]
struct V01Syns<'a> {
    map: std::collections::HashMap<String, Option<&'a cst_v1::ast::TypeExpr>>,
}

/// What a bare type NAME denotes, as far as this scan can tell.
enum V01SynLookup<'a> {
    /// A transparent, zero-parameter synonym — expand its body in place.
    Body(&'a cst_v1::ast::TypeExpr),
    /// Declared by some enclosing signature layer, but not expandable (see
    /// [`V01Syns`]'s `None` case). Whatever it is, it is NOT the builtin of
    /// the same name.
    Opaque,
    /// Named by no signature layer in scope — a builtin (or an outright
    /// unknown, which is downstream's error, not this scan's).
    Undeclared,
}

impl<'a> V01Syns<'a> {
    fn lookup(&self, name: &str) -> V01SynLookup<'a> {
        match self.map.get(name) {
            Some(Some(body)) => V01SynLookup::Body(body),
            Some(None) => V01SynLookup::Opaque,
            None => V01SynLookup::Undeclared,
        }
    }

    /// This env extended with one signature layer's own type declarations
    /// (recursing through `include`, whose decls splice into the enclosing
    /// scope) and then its `with type` refinements.
    fn extended(
        &self,
        decls: &'a [cst_v1::StructDeclV1],
        refines: &[surface::Refine<'a>],
        site_path: &[String],
        surfaces: &SurfaceEnv<'a>,
    ) -> V01Syns<'a> {
        let mut out = self.clone();
        let mut visited: Vec<String> = Vec::new();
        out.absorb_decls(decls, site_path, surfaces, &mut visited);
        out.absorb_refines(refines);
        out
    }

    fn absorb_decls(
        &mut self,
        decls: &'a [cst_v1::StructDeclV1],
        site_path: &[String],
        surfaces: &SurfaceEnv<'a>,
        visited: &mut Vec<String>,
    ) {
        for d in decls {
            match &*d.0 {
                cst_v1::ast::Decl::Type { binds, .. } => {
                    for single in v01_flatten_type_binds(binds) {
                        self.map
                            .insert(single.name.name.clone(), v01_synonym_body(single));
                    }
                }
                cst_v1::ast::Decl::TypeOpaque { name, .. } => {
                    self.map.insert(name.name.clone(), None);
                }
                cst_v1::ast::Decl::Include { sig_, .. } => {
                    let Some(resolved) = v01_resolve_sig_decls(sig_, site_path, surfaces) else {
                        continue;
                    };
                    if let Some(k) = &resolved.key {
                        if visited.contains(k) {
                            continue;
                        }
                        visited.push(k.clone());
                        self.absorb_decls(resolved.decls, site_path, surfaces, visited);
                        self.absorb_refines(&resolved.refines);
                        visited.pop();
                    } else {
                        self.absorb_decls(resolved.decls, site_path, surfaces, visited);
                        self.absorb_refines(&resolved.refines);
                    }
                }
                _ => {}
            }
        }
    }

    /// A refinement that made an opaque declaration transparent overwrites
    /// the `None` that declaration just wrote. Only a refinement whose own
    /// `path` is EMPTY applies at this layer — `S with M type t = τ` refines
    /// the nested member `M`'s `t`, and reaches it as an empty-path
    /// refinement one layer down (`classify_v01_sig_decls`'s `Decl::Module`
    /// arm re-resolves `M`'s own signature, refinements and all).
    fn absorb_refines(&mut self, refines: &[surface::Refine<'a>]) {
        for r in refines {
            if !r.path.is_empty() {
                continue;
            }
            let body = match (r.tyvars.is_empty(), r.body) {
                (true, cst_v1::TypeBodyV1::Synonym(ty)) => Some(ty),
                _ => None,
            };
            self.map.insert(r.name.clone(), body);
        }
    }
}

/// A `type t = τ` bind's expandable body: `Some` only for a zero-parameter
/// SYNONYM (see [`V01Syns`]'s `None` case for why the rest are not).
fn v01_synonym_body(single: &cst_v1::TypeBindSingleV1) -> Option<&cst_v1::ast::TypeExpr> {
    match (single.tyvars.is_empty(), &single.body) {
        (true, cst_v1::TypeBodyV1::Synonym(ty)) => Some(ty),
        _ => None,
    }
}

/// `module_check::flatten_type_binds`' local twin (that one is private to its
/// own module, and this scan runs a whole phase earlier).
fn v01_flatten_type_binds(binds: &cst_v1::TypeBindsErasedV1) -> Vec<&cst_v1::TypeBindSingleV1> {
    let mut out = vec![&binds.0.first];
    for a in &binds.0.ands {
        out.push(&a.bind);
    }
    out
}

/// A `with M.N type ..` refinement's module chain, as path segments (empty
/// for the plain `with type ..` form).
fn mod_chain_segments(path: &Option<cst_v1::ast::ModChainV1>) -> Vec<String> {
    match path {
        None => Vec::new(),
        Some(cst_v1::ast::ModChainV1::Single(t)) => vec![t.name.clone()],
        Some(cst_v1::ast::ModChainV1::Long(t)) => {
            let mut segs = t.mods.clone();
            segs.push(t.name.clone());
            segs
        }
    }
}

fn v1_boundary_error(name: &str) -> BoundaryError {
    BoundaryError::ForkedTypeExport {
        binding: String::new(),
        ty_name: name.to_string(),
        from: RustyfiVersion::V0_1,
        to: RustyfiVersion::V0_0,
        note: forked_note(name),
    }
}

fn v1_reject_if_mentions_deco(
    se: &cst_v1::ast::SigExpr,
    syns: &V01Syns<'_>,
) -> Result<(), BoundaryError> {
    match v1_sigexpr_mentions_deco(se, syns) {
        Some(n) => Err(v1_boundary_error(&n)),
        None => Ok(()),
    }
}

fn v1_reject_if_mentions_deco_ty(
    ty: &cst_v1::ast::TypeExpr,
    syns: &V01Syns<'_>,
) -> Result<(), BoundaryError> {
    match v1_type_expr_mentions_deco(ty, syns) {
        Some(n) => Err(v1_boundary_error(&n)),
        None => Ok(()),
    }
}

/// The 0.1-grammar twin of [`deco_tail_of`]: if `te` is a (possibly
/// arrow-prefixed) `deco`/`deco-set`/`paren`, return its kind, how many
/// arguments precede the tail, and each of those positions' optional-argument
/// spelling.
///
/// A [`cst_v1::ast::TypeExpr::OptRowFun`] (0.1's `?(l : τ, …) dom -> ..`
/// LABELLED-optional arrow) contributes ONE lead position carrying
/// [`LeadOpt::V01Labels`] — the shadow case-splits on each label's `option`
/// rather than forwarding it (see [`deco_downgrade_prelude`]). Two shapes
/// still return `None`, and so still reject:
///
/// - a ROW-VARIABLE tail (`?(l : τ | ?'r) ->`): the label set is open, so
///   there is no finite case split to generate. (`v1/lower.rs` rejects the
///   tail with its own `LowerError` slightly later anyway — signature-level
///   row quantification is not implemented — but this scan runs PRE-lowering
///   and must not fall through to a wrapper it cannot write.)
/// - more than [`V01_MAX_OPT_LABELS`] labels in total: the case split is
///   exponential in the label count, and is bounded rather than unbounded.
///
/// A tail (or a whole type) spelled as a signature-declared type SYNONYM is
/// EXPANDED in place through `syns` ([`V01Syns`]) before any of the above is
/// decided, so `type t = deco  val f : length -> t` reads exactly as `val f :
/// length -> deco` does — including an arrow-bodied synonym, whose own lead
/// positions append to the ones already collected. A synonym cycle (`type t =
/// u  type u = t`, which a later phase rejects on its own terms) terminates
/// at the first repeat and declines, rather than looping.
fn v1_deco_tail_of<'a>(
    te: &'a cst_v1::ast::TypeExpr,
    syns: &V01Syns<'a>,
) -> Option<(DecoKind, usize, Vec<LeadOpt>)> {
    use cst_v1::ast::TypeExpr;
    let mut lead_opts: Vec<LeadOpt> = Vec::new();
    let mut labels = 0usize;
    let mut expanded: Vec<&str> = Vec::new();
    let mut cur = te;
    loop {
        match cur {
            TypeExpr::OptRowFun { opt_dom, cod, .. } => {
                if opt_dom.inner.row_tail.is_some() {
                    return None;
                }
                let here: Vec<String> = opt_dom
                    .inner
                    .entries
                    .iter()
                    .map(|e| e.label.name.clone())
                    .collect();
                labels += here.len();
                if labels > V01_MAX_OPT_LABELS {
                    return None;
                }
                lead_opts.push(LeadOpt::V01Labels(here));
                cur = cod;
            }
            TypeExpr::Fun { cod, .. } => {
                lead_opts.push(LeadOpt::Mandatory);
                cur = cod;
            }
            _ => {
                let name = v1_type_expr_bare_name(cur)?;
                match syns.lookup(name) {
                    V01SynLookup::Body(body) => {
                        if expanded.contains(&name) {
                            return None;
                        }
                        expanded.push(name);
                        cur = body;
                        continue;
                    }
                    // Declared, but naming no expandable synonym — whatever
                    // it is, it is NOT the builtin of the same name.
                    V01SynLookup::Opaque => return None,
                    V01SynLookup::Undeclared => {}
                }
                let kind = match name {
                    "deco" => DecoKind::Deco,
                    "deco-set" => DecoKind::DecoSet,
                    "paren" => DecoKind::Paren,
                    _ => return None,
                };
                return Some((kind, lead_opts.len(), lead_opts));
            }
        }
    }
}

/// The 0.1-grammar twin of [`type_expr_bare_name`]: `Some(name)` iff `te` is
/// *exactly* one bare `TypeAtom::Name` with no arrow wrapper, no product
/// continuation, and no type application.
fn v1_type_expr_bare_name(te: &cst_v1::ast::TypeExpr) -> Option<&str> {
    use cst_v1::ast::{TypeApp, TypeAtom, TypeExpr};
    let TypeExpr::Atom(prod) = te else {
        return None;
    };
    if !prod.rest.is_empty() {
        return None;
    }
    match &prod.first {
        TypeApp::Atom(TypeAtom::Name(n)) => Some(n.name.as_str()),
        _ => None,
    }
}

/// Which of the reverse deco/paren coercion's three placement bindings [`deco_downgrade_prelude`] should
/// generate for a set of exports. The merged prelude is a single flat
/// `Ast::LetIn` chain, so "which view of `M.frame` is in force" is a function
/// of POSITION in that chain; these three steps are how `lib.rs`'s reverse arm
/// drives that position-indexed view (see [`deco_downgrade_prelude`]'s
/// **Placement** section for the schedule and its derivation).
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub(crate) enum DowngradeStep {
    /// `let xver-rev-orig-M-frame = M.frame` — capture the 0.1 original under
    /// a private name. Emitted ONCE per export, immediately after the
    /// dependency that defines it, while the 0.1 view is still the installed
    /// one. Binds a private name only: it never rebinds `M.frame`, so it is
    /// invisible to every consumer of either generation.
    Capture,
    /// `let M.frame = fun .. -> [xver-rev-orig-M-frame ..]` — install the
    /// 0.0.6-shaped view. Emitted at each transition INTO a 0.0.6-authored
    /// block (a native `V0_0` dependency, or the entry).
    Install,
    /// `let M.frame = xver-rev-orig-M-frame` — put the 0.1 view back. Emitted
    /// at each transition back into a 0.1-authored block, so a LATER 0.1
    /// dependency consuming the same export reads it at the shape its own
    /// `deco` means.
    Restore,
}

/// Build the `V0_1`-authored downgrade bindings for `exports` — see
/// [`DowngradeStep`] for which of the three this call emits. The load-bearing
/// one is [`DowngradeStep::Install`]: it REBINDS the export's own
/// fully-qualified name (`M.frame`) to a coerced view whose result is the
/// `graphics list` a `V0_0`-authored consumer expects.
///
/// Unlike the forward direction, the shadow CANNOT be appended inside the
/// exporting module's own `decls`: `elaborate.rs` emits one `Ast::LetIn`
/// export alias PER struct decl, so shadowing in place produces a FIRST
/// alias with the declared shape and a SECOND with the coerced one — and
/// `v1::module_check` conformance-checks BOTH, so the coerced one fails.
/// The shadow is therefore a TOP-LEVEL binding whose binder name is the
/// dotted qualified key directly. That is expressible even though no surface
/// syntax spells it: `elaborate.rs`'s `push_named_binding` takes the binder
/// name as an opaque `String`, so the generated `let xver-rev-shadow-N .. =
/// ..` is parsed for its SHAPE and its `BindName` then replaced with the
/// qualified key.
///
/// `Ast::Var` resolution follows suit for free: a consumer's `M.frame`
/// elaborates to a lookup of the string `"M.frame"` (`atomic`'s
/// `VarWithMod` arm via `qualify_key`), and `open M in ..`/`M.(..)` re-binds
/// the bare name to `Scope::resolve("M.frame")` — both land on whichever
/// binding of that key is innermost at that point, i.e. the shadow.
///
/// **Optional arguments ([`LeadOpt::V01Labels`]).** A 0.1 export may declare
/// LABELLED optionals (`?(thickness : length) length -> deco`), and the
/// shadow must present the same labelled interface or the export's optionals
/// vanish. It cannot do that by FORWARDING them, because 0.1's two halves
/// disagree about who owns the `option`: `Ast::LambdaOpt`
/// (`typecheck.rs`'s `infer_lambda_opt`) binds the receiving binder at `τ
/// option`, while `Ast::ApplyOpt` (`infer_apply_opt`) takes the RAW `τ` at
/// `?(l = e)` and `eval.rs`'s `push_opt_slots` wraps it in `Some` itself. So
/// `?(l = x)` where `x : τ option` is a type error, and no surface form hands
/// an already-`option` value to a labelled slot.
///
/// What the shadow CAN do is decide, per label, which spelling to use: `Some
/// v` re-supplies it as `?(l = v)`, `None` omits the label entirely and lets
/// `push_opt_slots` restore the `None`. That is a `match` per label, hence a
/// case split with one application site per subset of labels — bounded by
/// [`V01_MAX_OPT_LABELS`]. The omitting branch relies on plain `Ast::Apply`
/// carrying an OPEN row var under `V0_1` (`typecheck.rs`'s `Ast::Apply`
/// arm), which absorbs the callee's whole declared optional row; that is also
/// what lets a 0.0.6-authored consumer call the shadow with no optional
/// syntax of its own.
///
/// **Placement — which consumers see the coerced view.** The merged prelude is
/// one flat `Ast::LetIn` chain, and `Ast::VersionScope(V0_0, _)` is NOT a
/// lexical scope for names (it wraps ONE binding's RHS, never the continuation
/// after it — `ast.rs`'s own doc comment), so a rebinding of `M.frame` is
/// visible to *everything* that follows it, whichever generation authored it.
/// Do NOT splice the shadow unconditionally right after its dependency: that
/// hands the 0.0.6-shaped view to a LATER 0.1 dependency too, which then fails
/// its own `:>` conformance check.
///
/// What makes a position-indexed view sufficient is that each splice unit is
/// homogeneous and correctly ordered: `lib.rs`'s reverse loop contributes one
/// CONTIGUOUS block per dependency, wholly 0.0.6-authored (every index of it
/// in `v006_indices`) or wholly 0.1-authored (no index of it in
/// `v006_indices`), with the entry — always 0.0.6-authored — last; and the
/// loader orders dependencies topologically, so a consumer's block always
/// follows what it `@require:`s. "Which generation is reading `M.frame` right
/// now" is therefore constant within a block and known at splice time:
///
/// - [`Capture`](DowngradeStep::Capture) once, right after the defining
///   dependency (the 0.1 view is in force there — see the `Restore` below);
/// - [`Install`](DowngradeStep::Install) for EVERY export crossed so far, on
///   entering a 0.0.6-authored block, if the 0.0.6 view is not already
///   installed;
/// - [`Restore`](DowngradeStep::Restore) for every export crossed so far, on
///   entering a 0.1-authored block, if it is.
///
/// Both transitions are lazy, so a program with no interleaving (every 0.1
/// dependency, then the 0.0.6 entry — the common case, and every bundled
/// package) emits exactly one `Install` and no `Restore` at all.
///
/// `Install`/`Restore` both rebind a name `v1::module_check` has a `seals`
/// entry for, which is what `check_program_with_xver_shadows`'s exemption
/// covers — it exempts the SECOND-and-later `Ast::LetIn` of a listed name, so
/// a re-`Install` after a `Restore` is exempted for the same reason the first
/// one was, and the exporting module's OWN alias (the first) stays fully
/// conformance-checked.
pub(crate) fn deco_downgrade_prelude(
    exports: &[DecoExport],
    step: DowngradeStep,
) -> Vec<cst::TopBinding> {
    if exports.is_empty() {
        return Vec::new();
    }
    let mut src = String::new();
    let mut shadow_names: Vec<(String, String)> = Vec::new();
    for exp in exports.iter() {
        // `classify_deco_exports_v01_sig` never emits these two in this
        // direction (`paren` rejects; `Consumer` is a forward-only
        // contravariant case), so there is nothing to generate.
        if matches!(exp.kind, DecoKind::Paren | DecoKind::Consumer) {
            continue;
        }
        let qualified = deco_export_qualified_name(exp);
        // Mangled from the qualified key (a `.` cannot appear in a surface
        // identifier, a `-` can): the private names are a pure function of the
        // export's own qualified key, so [`DowngradeStep::Capture`]'s binding
        // and every later `Install`/`Restore` that reads it agree on the name
        // across the SEPARATE calls the placement schedule makes.
        let mangled = qualified.replace('.', "-");
        let orig = format!("xver-rev-orig-{mangled}");
        let shadow = format!("xver-rev-shadow-{mangled}");
        // The still-unshadowed original, captured under a private name. The
        // shadow's own body must NOT name `M.frame` — that is the key it is
        // about to rebind, and this indirection is what makes the rebinding
        // a plain (non-recursive) coercion rather than a self-reference. It is
        // ALSO what lets the 0.1 view be put back later: `Restore` simply
        // rebinds the key to this capture.
        if step == DowngradeStep::Capture {
            src.push_str(&format!("let {orig} = {qualified}\n"));
            continue;
        }
        if step == DowngradeStep::Restore {
            src.push_str(&format!("let {shadow} = {orig}\n"));
            shadow_names.push((shadow, qualified));
            continue;
        }
        let lead: Vec<String> = (0..exp.lead_arity).map(|k| format!("xver-a{k}")).collect();
        let lead_params = if lead.is_empty() {
            String::new()
        } else {
            format!("{} ", lead.join(" "))
        };
        // With labelled optionals the shadow needs `fun ?(l = x) p -> ..`
        // lambdas and a per-label case split (see this function's doc
        // comment); without them it keeps the plain parameter-list shape.
        let lambdas = v01_shadow_lambdas(exp);
        let case_split = |tail: &str| {
            let slots = v01_opt_slots(exp);
            let mut chosen = vec![false; slots.len()];
            v01_opt_case_split(&slots, 0, &mut chosen, &|chosen| {
                format!("{orig} {}{tail}", v01_shadow_args(exp, &slots, chosen))
            })
        };
        match exp.kind {
            DecoKind::Deco if exp.has_optionals() => src.push_str(&format!(
                "let {shadow} = {lambdas}fun xver-p xver-w xver-h xver-d ->\n\
                 \x20 [{}]\n",
                case_split("xver-p xver-w xver-h xver-d")
            )),
            DecoKind::Deco => src.push_str(&format!(
                "let {shadow} {lead_params}xver-p xver-w xver-h xver-d =\n\
                 \x20 [{orig} {lead_params}xver-p xver-w xver-h xver-d]\n",
            )),
            DecoKind::DecoSet => {
                let scrutinee = if exp.has_optionals() {
                    case_split("")
                } else if lead.is_empty() {
                    orig.clone()
                } else {
                    format!("{orig} {}", lead.join(" "))
                };
                // `let {shadow} p0 p1 =` when every position is mandatory;
                // `let {shadow} = fun ?(l = o) p0 -> ..` once a labelled
                // optional row has to be re-declared.
                let binder = if exp.has_optionals() {
                    format!("let {shadow} = {lambdas}")
                } else {
                    format!("let {shadow} {lead_params}= ")
                };
                let wrap = |k: usize| {
                    format!(
                        "(fun xver-p xver-w xver-h xver-d -> \
                         [xver-d{k} xver-p xver-w xver-h xver-d])"
                    )
                };
                src.push_str(&format!(
                    "{}\n\
                     \x20 match {scrutinee} with\n\
                     \x20 | (xver-d0, xver-d1, xver-d2, xver-d3) ->\n\
                     \x20   ({}, {}, {}, {})\n",
                    binder.trim_end(),
                    wrap(0),
                    wrap(1),
                    wrap(2),
                    wrap(3)
                ));
            }
            DecoKind::Paren | DecoKind::Consumer => unreachable!("skipped above"),
        }
        shadow_names.push((shadow, qualified));
    }
    if src.is_empty() {
        return Vec::new();
    }
    // Parsed as a bare `prelude* EOI` library file, for the same reason
    // `deco_coercion_prelude` is — see its comment about a trailing dummy
    // body being swallowed by the preceding application chain.
    let file = rustyfi_syntax::parse_file(&src).unwrap_or_else(|e| {
        panic!(
            "xver_adapt::deco_downgrade_prelude: internally-generated X4b wrapper \
             source failed to parse (a bug in xver_adapt.rs, not user input): {e}\n\
             --- generated source ---\n{src}"
        )
    });
    let mut prelude = file.prelude;
    rebind_shadows_to_qualified(&mut prelude, &shadow_names, "deco_downgrade_prelude");
    prelude
}

/// Every optional LABEL a 0.1 export declares, flattened to `(position,
/// index-within-position, label)`. The generated shadow binds each one's
/// `option` as `xver-o{position}-{index}` and, in the branch that re-supplies
/// it, its unwrapped payload as `xver-v{position}-{index}`.
fn v01_opt_slots(exp: &DecoExport) -> Vec<(usize, usize, String)> {
    let mut out = Vec::new();
    for i in 0..exp.lead_arity {
        if let LeadOpt::V01Labels(labels) = exp.lead_opt(i) {
            for (k, l) in labels.iter().enumerate() {
                out.push((i, k, l.clone()));
            }
        }
    }
    out
}

/// The shadow's parameter lambdas, one `fun .. ->` per lead position:
/// `fun ?(l = xver-o0-0) xver-a0 -> ` for a position with a labelled optional
/// row (`Expr::FunRows`, which elaborates to `Ast::LambdaOpt` and so puts the
/// same `Row::Cons(l, τ, …)` back on the shadow's own arrow), `fun xver-a0 ->
/// ` for a mandatory one. Empty when the export takes no leading arguments.
fn v01_shadow_lambdas(exp: &DecoExport) -> String {
    let mut out = String::new();
    for i in 0..exp.lead_arity {
        match exp.lead_opt(i) {
            LeadOpt::V01Labels(labels) => {
                let binders: Vec<String> = labels
                    .iter()
                    .enumerate()
                    .map(|(k, l)| format!("{l} = xver-o{i}-{k}"))
                    .collect();
                out.push_str(&format!("fun ?({}) xver-a{i} -> ", binders.join(", ")));
            }
            _ => out.push_str(&format!("fun xver-a{i} -> ")),
        }
    }
    out
}

/// The argument list of ONE leaf of the shadow's case split: every lead
/// position in order, each preceded by a `?(l = xver-v..)` bundle naming
/// exactly the labels `chosen` marks present at that position. A position
/// whose labels are all absent is spelled bare, so `Ast::Apply`'s open row
/// absorbs the callee's declared row and `push_opt_slots` restores the `None`s.
fn v01_shadow_args(exp: &DecoExport, slots: &[(usize, usize, String)], chosen: &[bool]) -> String {
    let mut out = String::new();
    for i in 0..exp.lead_arity {
        let here: Vec<String> = slots
            .iter()
            .zip(chosen)
            .filter(|((p, _, _), take)| *p == i && **take)
            .map(|((p, k, l), _)| format!("{l} = xver-v{p}-{k}"))
            .collect();
        if !here.is_empty() {
            out.push_str(&format!("?({}) ", here.join(", ")));
        }
        out.push_str(&format!("xver-a{i} "));
    }
    out
}

/// Expand `slots[idx..]` into nested `match .. with | None -> .. | Some(..) ->
/// ..` arms, calling `apply` at each of the `2^slots.len()` leaves with the
/// present/absent decision for every slot. Every generated `match` is
/// parenthesised, so nesting one inside an arm (and inside the list literal or
/// `match` scrutinee the caller wraps the whole thing in) is unambiguous.
fn v01_opt_case_split(
    slots: &[(usize, usize, String)],
    idx: usize,
    chosen: &mut Vec<bool>,
    apply: &dyn Fn(&[bool]) -> String,
) -> String {
    if idx == slots.len() {
        return apply(chosen);
    }
    let (p, k, _) = &slots[idx];
    chosen[idx] = false;
    let absent = v01_opt_case_split(slots, idx + 1, chosen, apply);
    chosen[idx] = true;
    let present = v01_opt_case_split(slots, idx + 1, chosen, apply);
    chosen[idx] = false;
    format!(
        "(match xver-o{p}-{k} with | None -> {absent} | Some(xver-v{p}-{k}) -> {present})"
    )
}

/// The qualified key [`deco_downgrade_prelude`] rebinds for `exp` — the same
/// string `v1::module_check` keys its `static_env.seals` entry by, and the
/// one `lib.rs` hands to `check_program_with_xver_shadows` as an exemption.
pub(crate) fn deco_export_qualified_name(exp: &DecoExport) -> String {
    format!("{}.{}", exp.module_path.join("."), exp.name)
}

/// Structural (read-only) walk of a 0.1 signature expression, looking for
/// any `deco`/`deco-set` mention anywhere reachable from it: a direct
/// inline `sig .. end` body's `val`/`val \cmd`/`val +cmd` items (recursing
/// into any nested `module`/`signature`/`include` declaration too), or a
/// `with type` refinement's base. A named-signature reference
/// (`SigBotV1::Path`/`Var`) is NOT chased further HERE — this is the
/// LAST-RESORT guard [`classify_v01_sig_expr`] falls back to once
/// [`v01_resolve_sig_decls`] has already declined to resolve the expression
/// at all (a functor signature, or a name with no entry in `surfaces.sigs`);
/// in the first case the nested names it does reach are exactly the ones
/// worth guarding, and in the second there is nothing to chase. See
/// [`classify_deco_exports_v01_sig`]'s own doc comment for why a false
/// negative here is still sound (an ordinary `TypeError`, never unsoundness).
fn v1_sigexpr_mentions_deco(se: &cst_v1::ast::SigExpr, syns: &V01Syns<'_>) -> Option<String> {
    use cst_v1::ast::SigExpr;
    match se {
        SigExpr::Functor { dom, cod, .. } => v1_sigexpr_mentions_deco(dom, syns)
            .or_else(|| v1_sigexpr_mentions_deco(cod, syns)),
        SigExpr::WithType { base, .. } => v1_sigbot_mentions_deco(base, syns),
        SigExpr::Bot(bot) => v1_sigbot_mentions_deco(bot, syns),
    }
}

fn v1_sigbot_mentions_deco(bot: &cst_v1::ast::SigBotV1, syns: &V01Syns<'_>) -> Option<String> {
    use cst_v1::ast::SigBotV1;
    match bot {
        // An unresolved named-signature reference — not chased (this
        // section's doc comment).
        SigBotV1::Path(_) | SigBotV1::Var(_) => None,
        SigBotV1::Sig { decls, .. } => decls
            .iter()
            .find_map(|d| v1_decl_mentions_deco(&d.0, syns)),
    }
}

fn v1_decl_mentions_deco(decl: &cst_v1::ast::Decl, syns: &V01Syns<'_>) -> Option<String> {
    use cst_v1::ast::Decl;
    match decl {
        Decl::Val { ty, .. } | Decl::ValHorzCmd { ty, .. } | Decl::ValVertCmd { ty, .. } => {
            v1_type_expr_mentions_deco(ty, syns)
        }
        // A `type`/opaque-`type` sig item merely NAMES `deco`/`deco-set`
        // with no attached VALUE — safe, no coercion needed at all (this
        // section's doc comment's "bare `type foo = deco` synonym" case).
        Decl::TypeOpaque { .. } | Decl::Type { .. } => None,
        Decl::Module { sig_, .. } | Decl::Signature { sig_, .. } | Decl::Include { sig_, .. } => {
            v1_sigexpr_mentions_deco(sig_, syns)
        }
    }
}

/// Structural (read-only) walk of the WIDENED 0.1 type-expression grammar
/// (`cst_v1::ast::TypeExpr`) — the 0.1-grammar twin of this module's own
/// `type_expr_mentions_deco`, additionally covering 0.1-only shapes
/// (`OptRowFun`, prefix `TypeApp::Applied`/`AppliedLong`, the `inline
/// [..]`/`block [..]`/`math [..]` command-type forms). `Some(name)` for
/// the first `"deco"`/`"deco-set"` leaf found anywhere in `te`, `None` if
/// there is none.
fn v1_type_expr_mentions_deco(te: &cst_v1::ast::TypeExpr, syns: &V01Syns<'_>) -> Option<String> {
    use cst_v1::ast::TypeExpr;
    match te {
        TypeExpr::OptRowFun {
            opt_dom, dom, cod, ..
        } => opt_dom
            .inner
            .entries
            .iter()
            .find_map(|e| v1_type_expr_mentions_deco(&e.ty.0, syns))
            .or_else(|| v1_type_prod_mentions_deco(dom, syns))
            .or_else(|| v1_type_expr_mentions_deco(cod, syns)),
        TypeExpr::Fun { dom, cod, .. } => v1_type_prod_mentions_deco(dom, syns)
            .or_else(|| v1_type_expr_mentions_deco(cod, syns)),
        TypeExpr::Atom(prod) => v1_type_prod_mentions_deco(prod, syns),
    }
}

fn v1_type_prod_mentions_deco(tp: &cst_v1::ast::TypeProd, syns: &V01Syns<'_>) -> Option<String> {
    v1_type_app_mentions_deco(&tp.first, syns).or_else(|| {
        tp.rest
            .iter()
            .find_map(|st| v1_type_app_mentions_deco(&st.ty, syns))
    })
}

fn v1_type_app_mentions_deco(ta: &cst_v1::ast::TypeApp, syns: &V01Syns<'_>) -> Option<String> {
    use cst_v1::ast::TypeApp;
    match ta {
        // Prefix application (`list int`, 0.1-only shape): the CTOR itself
        // is the bare-name position here (unlike the universal postfix
        // grammar) — check it, plus every argument atom.
        TypeApp::Applied { ctor, first, rest } => v1_leaf_name_through_syns(&ctor.name, syns)
            .or_else(|| v1_type_atom_mentions_deco(first, syns))
            .or_else(|| {
                rest.iter()
                    .find_map(|a| v1_type_atom_mentions_deco(a, syns))
            }),
        // `M.t τ…` — a QUALIFIED ctor name; never itself a bare
        // `"deco"`/`"deco-set"` (those are unqualified builtins), only its
        // arguments can mention one.
        TypeApp::AppliedLong { first, rest, .. } => v1_type_atom_mentions_deco(first, syns)
            .or_else(|| {
                rest.iter()
                    .find_map(|a| v1_type_atom_mentions_deco(a, syns))
            }),
        TypeApp::InlineCmdTy { args, .. }
        | TypeApp::BlockCmdTy { args, .. }
        | TypeApp::MathCmdTy { args, .. } => args
            .iter()
            .find_map(|a| v1_type_cmd_arg_mentions_deco(a, syns)),
        TypeApp::Atom(atom) => v1_type_atom_mentions_deco(atom, syns),
    }
}

fn v1_type_cmd_arg_mentions_deco(
    item: &cst_v1::ast::TypeCmdArgItemV1,
    syns: &V01Syns<'_>,
) -> Option<String> {
    item.opts
        .as_ref()
        .and_then(|o| {
            o.entries
                .iter()
                .find_map(|e| v1_type_expr_mentions_deco(&e.ty.0, syns))
        })
        .or_else(|| v1_type_expr_mentions_deco(&item.ty.0, syns))
}

fn v1_type_atom_mentions_deco(atom: &cst_v1::ast::TypeAtom, syns: &V01Syns<'_>) -> Option<String> {
    use cst_v1::ast::TypeAtom;
    match atom {
        TypeAtom::Paren { inner, .. } => v1_type_expr_mentions_deco(&inner.0, syns),
        TypeAtom::Record { inner, .. } => inner
            .fields
            .iter()
            .find_map(|f| v1_type_expr_mentions_deco(&f.ty.0, syns)),
        // A bound type variable — never a forked-name candidate.
        TypeAtom::Var(_) => None,
        // `M.t` — a qualified name; never itself a bare builtin fork name.
        TypeAtom::LongName(_) => None,
        TypeAtom::Name(n) => v1_leaf_name_through_syns(&n.name, syns),
    }
}

/// [`deco_leaf_name`] THROUGH the signature's own type synonyms: a name a
/// signature layer in scope declares transparently is expanded (recursively,
/// cycle-guarded) and the expansion searched instead, so a `deco` reachable
/// only via a synonym — `type t = deco  val g : t list` — is refused as
/// loudly as a directly-spelled one, rather than quietly declining to cross.
/// A name declared NON-transparently (opaque, parameterised) is not a forked
/// builtin at all; a name declared nowhere falls through to the builtin test.
fn v1_leaf_name_through_syns(name: &str, syns: &V01Syns<'_>) -> Option<String> {
    v1_leaf_name_through_syns_guarded(name, syns, &mut Vec::new())
}

fn v1_leaf_name_through_syns_guarded(
    name: &str,
    syns: &V01Syns<'_>,
    expanded: &mut Vec<String>,
) -> Option<String> {
    match syns.lookup(name) {
        V01SynLookup::Body(body) => {
            if expanded.iter().any(|e| e == name) {
                return None;
            }
            expanded.push(name.to_string());
            // The body is searched with the SAME guard list, so a cycle
            // through any number of intermediate synonyms terminates.
            let out = v1_type_expr_mentions_deco_guarded(body, syns, expanded);
            expanded.pop();
            out
        }
        V01SynLookup::Opaque => None,
        V01SynLookup::Undeclared => deco_leaf_name(name),
    }
}

/// [`v1_type_expr_mentions_deco`] with an explicit synonym-expansion guard —
/// only reachable from [`v1_leaf_name_through_syns_guarded`], which is the
/// only place a cycle can arise. A synonym body is a plain type expression,
/// so this reuses the ordinary walk by temporarily hiding the names already
/// being expanded.
fn v1_type_expr_mentions_deco_guarded(
    te: &cst_v1::ast::TypeExpr,
    syns: &V01Syns<'_>,
    expanded: &mut Vec<String>,
) -> Option<String> {
    let mut hidden = syns.clone();
    for name in expanded.iter() {
        hidden.map.insert(name.clone(), None);
    }
    v1_type_expr_mentions_deco(te, &hidden)
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::types::BaseType;

    fn v006() -> RustyfiVersion {
        RustyfiVersion::V0_0
    }
    fn v01() -> RustyfiVersion {
        RustyfiVersion::V0_1
    }

    // ------------------------------------------------------------------
    // adapt_export_type (PolyType-level spec function)
    // ------------------------------------------------------------------

    #[test]
    fn adapt_export_type_accepts_bare_math_text_base() {
        // `math`'s 0.0.6 meaning IS `Base(MathText)` (name_to_mono already
        // performed the math->MathText fold before this function ever sees
        // it) — the identity/no-op accept path.
        let ty = PolyType::mono(MonoType::Base(BaseType::MathText));
        let out = adapt_export_type(&ty, v006(), v01()).expect("math (MathText) must be accepted");
        assert!(matches!(out.body(), MonoType::Base(BaseType::MathText)));
    }

    #[test]
    fn adapt_export_type_accepts_math_nested_in_function_and_list() {
        let ty = PolyType::mono(MonoType::Func(
            Box::new(Row::Empty),
            Box::new(MonoType::List(Box::new(MonoType::Base(BaseType::MathText)))),
            Box::new(MonoType::Base(BaseType::MathText)),
        ));
        assert!(adapt_export_type(&ty, v006(), v01()).is_ok());
    }

    #[test]
    fn adapt_export_type_rejects_page_nominal() {
        let ty = PolyType::mono(MonoType::Variant("page".to_string(), vec![]));
        let err = adapt_export_type(&ty, v006(), v01()).expect_err("page must reject");
        match err {
            BoundaryError::ForkedTypeExport { ty_name, .. } => assert_eq!(ty_name, "page"),
        }
    }

    #[test]
    fn adapt_export_type_rejects_opaque_nominals() {
        // `pre-path`/`path`/`graphics`/`image` are deliberately NOT here: they
        // are not forked. Upstream 0.0.6's `base_type_hash_table`
        // (`types.cppo.ml:295-298`) maps all four to the same base types 0.1
        // uses, and this port's `t_prepath`/`t_path`/`t_graphics`/`t_image` and
        // their `Value` reps take no version either — see the test below.
        for name in ["math-text", "math-boxes", "font"] {
            let ty = PolyType::mono(MonoType::Variant(name.to_string(), vec![]));
            let err = adapt_export_type(&ty, v006(), v01()).unwrap_err();
            match err {
                BoundaryError::ForkedTypeExport { ty_name, .. } => assert_eq!(ty_name, name),
            }
        }
    }

    #[test]
    fn graphics_tier_base_types_are_not_forked_and_cross_in_both_directions() {
        // The four graphics-tier base types resolve identically under both
        // versions, so they must not appear in the fork set at all...
        let forked = crate::typecheck::forked_type_names();
        for name in ["pre-path", "path", "graphics", "image"] {
            assert!(
                !forked.contains(name),
                "`{name}` must not be reported as version-forked: upstream 0.0.6 \
                 registers it as a base type exactly as 0.1 does"
            );
            assert!(
                !reject_type_names().contains(name),
                "`{name}` must not be rejected"
            );
        }
        // ...and an export mentioning one must cross unchanged, either way.
        for (from, to) in [(v006(), v01()), (v01(), v006())] {
            for name in ["pre-path", "path", "graphics", "image"] {
                let ann = parse_ty(name);
                adapt_export_annotation(&ann, from, to)
                    .unwrap_or_else(|e| panic!("`{name}` must cross {from:?}->{to:?}: {e:?}"));
            }
        }
    }

    #[test]
    fn adapt_export_type_rejects_forked_leaf_nested_in_a_compound() {
        // A forked leaf anywhere in the structure rejects the whole
        // export, even alongside an otherwise-fine math leaf.
        let ty = PolyType::mono(MonoType::Product(vec![
            MonoType::Base(BaseType::MathText),
            MonoType::Variant("page".to_string(), vec![]),
        ]));
        assert!(adapt_export_type(&ty, v006(), v01()).is_err());
    }

    #[test]
    fn adapt_export_type_accepts_ordinary_user_nominal() {
        // A ordinary, non-forked user type name must pass through untouched
        // (the flip side: only the specific reject set is conservative,
        // not every nominal).
        let ty = PolyType::mono(MonoType::Variant(
            "option".to_string(),
            vec![MonoType::Base(BaseType::Int)],
        ));
        assert!(adapt_export_type(&ty, v006(), v01()).is_ok());
    }

    // ------------------------------------------------------------------
    // adapt_export_annotation (CST-level helper)
    // ------------------------------------------------------------------

    fn parse_ty(src: &str) -> TypeExpr {
        // Reuse a `type` declaration's RHS to get a real parsed TypeExpr —
        // simplest way to build one without hand-rolling the CST.
        let file =
            rustyfi_syntax::parse_file(&format!("type xver-probe = {src}\n0\n")).expect("parse");
        for tb in &file.prelude {
            if let cst::TopBinding::Type(td) = tb {
                if let cst::TypeDeclBody::Synonym(ty) = &td.body {
                    return ty.clone();
                }
            }
        }
        panic!("expected a type synonym declaration");
    }

    #[test]
    fn adapt_export_annotation_relabels_bare_math() {
        let ann = parse_ty("math");
        let out = adapt_export_annotation(&ann, v006(), v01()).expect("math must be accepted");
        match out {
            TypeExpr::Atom(TypeProd {
                first:
                    TypeApp {
                        head: TypeAtom::Name(n),
                        ..
                    },
                ..
            }) => assert_eq!(n.name, "math-text"),
            other => panic!("expected a bare relabeled Name, got {other:?}"),
        }
    }

    #[test]
    fn adapt_export_annotation_relabels_math_nested_in_function_type() {
        let ann = parse_ty("math -> math");
        let out =
            adapt_export_annotation(&ann, v006(), v01()).expect("math -> math must be accepted");
        // Round-trip through Display/Debug is overkill; just confirm no
        // `Err` and that unparsing still contains `math-text` twice, not
        // bare `math`.
        let unparsed = format!("{out:?}");
        assert!(
            !unparsed.contains("\"math\""),
            "no bare `math` should survive: {unparsed}"
        );
    }

    #[test]
    fn adapt_export_annotation_rejects_page() {
        let ann = parse_ty("page -> document");
        let err = adapt_export_annotation(&ann, v006(), v01()).expect_err("page must reject");
        match err {
            BoundaryError::ForkedTypeExport { ty_name, .. } => assert_eq!(ty_name, "page"),
        }
    }

    #[test]
    fn adapt_export_annotation_rejects_deco() {
        let ann = parse_ty("deco");
        let err = adapt_export_annotation(&ann, v006(), v01()).expect_err("deco must reject");
        match err {
            BoundaryError::ForkedTypeExport { ty_name, .. } => assert_eq!(ty_name, "deco"),
        }
    }

    // ------------------------------------------------------------------
    // The REVERSE (V0_1 -> V0_0) direction of the leaf policy
    // (`relabel_or_reject_name`). NOTE: these pin the PURE function's
    // contract only — `lib.rs`'s reverse arm deliberately does NOT call
    // `adapt_export_annotation`/`relabel_type_decls` in this direction, since
    // a foreign 0.1 dependency's own "math-text"/"math-boxes" spelling is
    // ALREADY the hard-coded-`V0_1` vocabulary that matters. See
    // `relabel_or_reject_name`'s own doc comment.
    // ------------------------------------------------------------------

    #[test]
    fn adapt_export_annotation_reverse_relabels_math_text_to_math() {
        let ann = parse_ty("math-text");
        let out = adapt_export_annotation(&ann, v01(), v006()).expect("math-text must be accepted");
        match out {
            TypeExpr::Atom(TypeProd {
                first:
                    TypeApp {
                        head: TypeAtom::Name(n),
                        ..
                    },
                ..
            }) => assert_eq!(n.name, "math"),
            other => panic!("expected a bare relabeled Name, got {other:?}"),
        }
    }

    #[test]
    fn adapt_export_annotation_reverse_relabels_math_boxes_to_math() {
        let ann = parse_ty("math-boxes");
        let out =
            adapt_export_annotation(&ann, v01(), v006()).expect("math-boxes must be accepted");
        match out {
            TypeExpr::Atom(TypeProd {
                first:
                    TypeApp {
                        head: TypeAtom::Name(n),
                        ..
                    },
                ..
            }) => assert_eq!(n.name, "math"),
            other => panic!("expected a bare relabeled Name, got {other:?}"),
        }
    }

    #[test]
    fn adapt_export_annotation_reverse_rejects_page() {
        let ann = parse_ty("page -> document");
        let err = adapt_export_annotation(&ann, v01(), v006()).expect_err("page must reject");
        match err {
            BoundaryError::ForkedTypeExport { ty_name, .. } => assert_eq!(ty_name, "page"),
        }
    }

    #[test]
    fn adapt_export_annotation_reverse_rejects_a_genuinely_forked_name() {
        // `font` IS forked: 0.0.6 has no `font` type at all (the word there
        // is an unrelated opaque user nominal), 0.1's is a real opaque
        // handle — no shared runtime rep, so it must not cross. Contrast
        // `graphics`, which is not forked (see
        // `graphics_tier_base_types_are_not_forked_and_cross_in_both_directions`).
        let ann = parse_ty("font");
        let err = adapt_export_annotation(&ann, v01(), v006()).expect_err("font must reject");
        match err {
            BoundaryError::ForkedTypeExport { ty_name, .. } => assert_eq!(ty_name, "font"),
        }
    }

    #[test]
    fn adapt_export_annotation_forward_math_relabel_is_unaffected_by_the_reverse_arm() {
        // Non-regression: the (V0_1, V0_0) arm must not perturb the
        // (V0_0, V0_1) "math"->"math-text" relabel.
        let ann = parse_ty("math");
        let out =
            adapt_export_annotation(&ann, v006(), v01()).expect("math must still be accepted");
        match out {
            TypeExpr::Atom(TypeProd {
                first:
                    TypeApp {
                        head: TypeAtom::Name(n),
                        ..
                    },
                ..
            }) => assert_eq!(n.name, "math-text"),
            other => panic!("expected a bare relabeled Name, got {other:?}"),
        }
    }

    // ------------------------------------------------------------------
    // relabel_type_decls (prelude-level splice-arm entry point)
    // ------------------------------------------------------------------

    fn prelude_of(src: &str) -> Vec<cst::TopBinding> {
        let file = rustyfi_syntax::parse_file(src).expect("parse");
        file.prelude
    }

    #[test]
    fn relabel_type_decls_rewrites_variant_ctor_payload() {
        let prelude = prelude_of("type xver-wrap = XverWrap of math\n0\n");
        let out =
            relabel_type_decls(&prelude, v006(), v01()).expect("math-only prelude must relabel");
        match &out[0] {
            cst::TopBinding::Type(td) => match &td.body {
                cst::TypeDeclBody::Variant { first, .. } => {
                    let ty = &first.of_ty.as_ref().unwrap().ty;
                    match ty {
                        TypeExpr::Atom(TypeProd {
                            first:
                                TypeApp {
                                    head: TypeAtom::Name(n),
                                    ..
                                },
                            ..
                        }) => assert_eq!(n.name, "math-text"),
                        other => panic!("expected relabeled Name, got {other:?}"),
                    }
                }
                other => panic!("expected a Variant body, got {other:?}"),
            },
            other => panic!("expected a Type binding, got {other:?}"),
        }
    }

    #[test]
    fn relabel_type_decls_recurses_into_nested_module() {
        let prelude =
            prelude_of("module M = struct\n  type inner-wrap = InnerWrap of math\nend\n0\n");
        let out = relabel_type_decls(&prelude, v006(), v01())
            .expect("nested math-only prelude must relabel");
        match &out[0] {
            cst::TopBinding::Module { decls, .. } => match decls[0].0.as_ref() {
                cst::TopBinding::Type(td) => match &td.body {
                    cst::TypeDeclBody::Variant { first, .. } => {
                        let ty = &first.of_ty.as_ref().unwrap().ty;
                        match ty {
                            TypeExpr::Atom(TypeProd {
                                first:
                                    TypeApp {
                                        head: TypeAtom::Name(n),
                                        ..
                                    },
                                ..
                            }) => assert_eq!(n.name, "math-text"),
                            other => panic!("expected relabeled Name, got {other:?}"),
                        }
                    }
                    other => panic!("expected a Variant body, got {other:?}"),
                },
                other => panic!("expected a nested Type binding, got {other:?}"),
            },
            other => panic!("expected a Module binding, got {other:?}"),
        }
    }

    #[test]
    fn relabel_type_decls_leaves_non_math_untouched() {
        // Sanity: a prelude with no forked type text at all is unaffected
        // (this exercises the same walk the touched=={} fast path in
        // lib.rs never even calls, but confirms the walk itself is a no-op
        // absent any `math`).
        let prelude = prelude_of("type ordinary = Foo of int\n0\n");
        let out = relabel_type_decls(&prelude, v006(), v01()).expect("no forked names present");
        assert_eq!(format!("{prelude:?}"), format!("{out:?}"));
    }

    // ------------------------------------------------------------------
    // The forward wrapper: classify_deco_exports / deco_coercion_prelude
    // ------------------------------------------------------------------

    #[test]
    fn classify_deco_exports_accepts_bare_top_level_letrec() {
        let prelude = prelude_of("let-rec xver-my-deco : deco | (x, y) w h d = []\n0\n");
        let exports =
            classify_deco_exports(&prelude, v006(), v01()).expect("bare `: deco` must be accepted");
        assert_eq!(exports.len(), 1);
        assert_eq!(exports[0].name, "xver-my-deco");
        assert_eq!(exports[0].kind, DecoKind::Deco);
    }

    #[test]
    fn classify_deco_exports_accepts_bare_decoset() {
        // `| ()` is the ONLY legal idiom for a plain `deco-set` VALUE export
        // — `elaborate.rs` requires a `let-rec`'s RHS to be a function, so
        // `let-rec name : deco-set | = (tuple)` (zero params, no `()`) does
        // not even elaborate; see `classify_rec_binding_deco`'s doc comment.
        let prelude = prelude_of("let-rec xver-my-decoset : deco-set | () = (0, 0, 0, 0)\n0\n");
        let exports = classify_deco_exports(&prelude, v006(), v01())
            .expect("`| ()` deco-set must be accepted");
        assert_eq!(exports.len(), 1);
        assert_eq!(exports[0].name, "xver-my-decoset");
        assert_eq!(exports[0].kind, DecoKind::DecoSet);
    }

    #[test]
    fn classify_deco_exports_rejects_decoset_with_wrong_params() {
        // A `deco-set` export with a REAL (non-unit) param — outside the forward wrapper's
        // scoped support (only the bare `| ()` idiom is handled).
        let prelude = prelude_of("let-rec xver-my-decoset : deco-set | t = (0, 0, 0, 0)\n0\n");
        let err = classify_deco_exports(&prelude, v006(), v01())
            .expect_err("a deco-set export with a non-unit param must still be rejected");
        match err {
            BoundaryError::ForkedTypeExport { ty_name, .. } => assert_eq!(ty_name, "deco-set"),
        }
    }

    #[test]
    fn classify_deco_exports_ignores_type_synonym() {
        // A bare `type .. = deco` synonym has no attached value — safe with
        // zero coercion, so it must not be classified as a `DecoExport` at
        // all (nothing to wrap).
        let prelude = prelude_of("type xver-deco-alias = deco\n0\n");
        let exports = classify_deco_exports(&prelude, v006(), v01())
            .expect("a type synonym must be accepted");
        assert!(exports.is_empty());
    }

    #[test]
    fn classify_deco_exports_accepts_curried_prefix() {
        // `length -> deco` — the arrow-PREFIXED shape: the wrapper
        // eta-expands over the leading arguments, so it is classified with
        // its lead arity.
        let prelude =
            prelude_of("let-rec xver-my-deco : length -> deco | t (x, y) w h d = []\n0\n");
        let got = classify_deco_exports(&prelude, v006(), v01())
            .expect("a curried-prefix deco export is now wrappable");
        assert_eq!(got.len(), 1);
        assert_eq!(got[0].name, "xver-my-deco");
        assert_eq!(got[0].lead_arity, 1);
        assert!(got[0].module_path.is_empty());
    }

    #[test]
    fn classify_deco_exports_accepts_module_sig_item() {
        // The shape the whole 0.0.6 corpus actually uses: exports inside a
        // `module .. : sig .. end`. Recorded with the enclosing module path,
        // which is what routes it to `inject_module_deco_wrappers`.
        let prelude = prelude_of(
            "module M : sig\n  val simple : length -> deco\n  val plain : deco\nend = struct\n  \
             let simple t (x, y) w h d = []\n  let plain (x, y) w h d = []\nend\n0\n",
        );
        let got = classify_deco_exports(&prelude, v006(), v01())
            .expect("a module-scoped deco export is now wrappable");
        assert_eq!(got.len(), 2);
        assert_eq!(got[0].name, "simple");
        assert_eq!(got[0].lead_arity, 1);
        assert_eq!(got[0].module_path, vec!["M".to_string()]);
        assert_eq!(got[1].name, "plain");
        assert_eq!(got[1].lead_arity, 0);
    }

    #[test]
    fn module_deco_wrapper_is_injected_inside_the_module() {
        let mut prelude = prelude_of(
            "module M : sig\n  val simple : length -> deco\nend = struct\n  \
             let simple t (x, y) w h d = []\nend\n0\n",
        );
        let exports = classify_deco_exports(&prelude, v006(), v01()).unwrap();
        let before = match &prelude[0] {
            cst::TopBinding::Module { decls, .. } => decls.len(),
            other => panic!("expected a module, got {other:?}"),
        };
        inject_module_deco_wrappers(&mut prelude, &exports);
        match &prelude[0] {
            cst::TopBinding::Module { decls, .. } => {
                assert_eq!(
                    decls.len(),
                    before + 2,
                    "the X3c capture AND the wrapper must be appended INSIDE the module"
                );
                // The capture of the UNWRAPPED original comes FIRST, while the
                // original is still the innermost binding of its own name
                // (see `DecoExport::orig_capture_name`).
                match &*decls[decls.len() - 2].0 {
                    cst::TopBinding::Let(tl) => {
                        assert_eq!(tl.name.name, "xver-fwd-orig-simple")
                    }
                    other => panic!("expected the X3c original capture, got {other:?}"),
                }
                // ...and the wrapper must shadow, i.e. bind the SAME name, LAST.
                match &*decls[decls.len() - 1].0 {
                    cst::TopBinding::Let(tl) => assert_eq!(tl.name.name, "simple"),
                    other => panic!("expected a shadowing `let simple`, got {other:?}"),
                }
            }
            other => panic!("expected a module, got {other:?}"),
        }
        // A module-scoped export must NOT also get a top-level shadow: there
        // is no `let M.simple` to write.
        assert!(deco_coercion_prelude(&exports).is_empty());
    }

    #[test]
    fn deco_coercion_prelude_generates_parseable_wrap() {
        let exports = vec![
            DecoExport {
                name: "xver-my-deco".to_string(),
                kind: DecoKind::Deco,
                lead_arity: 0,
                lead_opts: Vec::new(),
                module_path: Vec::new(),
                arg_downgrades: Vec::new(),
                unit_thunk: false,
            },
            DecoExport {
                name: "xver-my-decoset".to_string(),
                kind: DecoKind::DecoSet,
                lead_arity: 0,
                lead_opts: Vec::new(),
                module_path: Vec::new(),
                arg_downgrades: Vec::new(),
                unit_thunk: true,
            },
        ];
        let out = deco_coercion_prelude(&exports);
        // TWO synthetic `TopBinding::Let`s per export, in order: the capture
        // of the unwrapped original, then the shadowing wrapper.
        assert_eq!(out.len(), 4);
        let names: Vec<&str> = out
            .iter()
            .map(|tb| match tb {
                cst::TopBinding::Let(tl) => tl.name.name.as_str(),
                other => panic!("expected a Let binding, got {other:?}"),
            })
            .collect();
        assert_eq!(
            names,
            vec![
                "xver-fwd-orig-xver-my-deco",
                "xver-my-deco",
                "xver-fwd-orig-xver-my-decoset",
                "xver-my-decoset",
            ]
        );
    }

    #[test]
    fn deco_coercion_prelude_empty_is_empty() {
        assert!(deco_coercion_prelude(&[]).is_empty());
    }

    // ------------------------------------------------------------------
    // The reverse deco/paren coercion: classify_deco_exports_v01_sig / deco_downgrade_prelude (the
    // reverse direction — a 0.1 dependency's `deco` export consumed by a
    // 0.0.6 document, coerced by wrapping its single `graphics` in a
    // singleton list)
    // ------------------------------------------------------------------

    fn v1_file(src: &str) -> cst_v1::FileV1 {
        cst_v1::parse_file_v1(src).expect("parse v1 fixture")
    }

    /// [`classify_deco_exports_v01_sig`] against `file`'s OWN surface — the
    /// same `build_file_surface`-then-classify order `lib.rs`'s reverse splice
    /// arm uses, so a `signature S = ..` bind in the fixture is already
    /// registered by the time a `module M : S` decl has to resolve it.
    fn classify_v1(file: &cst_v1::FileV1) -> Result<Vec<DecoExport>, BoundaryError> {
        let mut surfaces = SurfaceEnv::default();
        surface::build_file_surface(file, &mut surfaces);
        classify_deco_exports_v01_sig(file, &surfaces)
    }

    #[test]
    fn classify_v01_sig_accepts_bare_sig_val_deco() {
        // The ONE shape 0.1's grammar can express a bare `deco` ascription
        // at all: a top-level module's own `sig val name : deco` item
        // (`cst_v1::Bind::Value` has no ascription syntax of its own).
        let file = v1_file(
            "module M :> sig\n  val my-deco : deco\nend = struct\n  val my-deco = 0\nend\n",
        );
        let exports = classify_v1(&file).expect("a bare `: deco` sig item");
        assert_eq!(exports.len(), 1);
        assert_eq!(exports[0].name, "my-deco");
        assert_eq!(exports[0].kind, DecoKind::Deco);
        assert_eq!(exports[0].lead_arity, 0);
        assert_eq!(exports[0].module_path, vec!["M".to_string()]);
        assert_eq!(deco_export_qualified_name(&exports[0]), "M.my-deco");
    }

    #[test]
    fn classify_v01_sig_accepts_bare_sig_val_decoset() {
        let file = v1_file("module M :> sig\n  val my-decoset : deco-set\nend = struct\n  val my-decoset = 0\nend\n");
        let exports = classify_v1(&file).expect("a bare `: deco-set` sig item");
        assert_eq!(exports.len(), 1);
        assert_eq!(exports[0].kind, DecoKind::DecoSet);
        assert!(
            !exports[0].unit_thunk,
            "a 0.1 sig-declared `deco-set` is bound to the bare 4-tuple — no `()` thunk"
        );
    }

    #[test]
    fn classify_v01_sig_accepts_curried_sig_val() {
        let file =
            v1_file("module M :> sig\n  val my-deco : length -> color -> deco\nend = struct\n  val my-deco t c p w h d = 0\nend\n");
        let exports = classify_v1(&file).expect("an arrow-tailed `deco` export");
        assert_eq!(exports.len(), 1);
        assert_eq!(exports[0].kind, DecoKind::Deco);
        assert_eq!(exports[0].lead_arity, 2);
    }

    #[test]
    fn classify_v01_sig_accepts_an_optional_argument_arrow() {
        // The wrapper carries labelled optionals across (rather than
        // forwarding them positionally, which has no spelling), so a `?(l :
        // ty) .. -> deco` export classifies.
        let file = v1_file(
            "module M :> sig\n  val my-deco : ?(thickness : length) length -> deco\nend \
             = struct\n  val my-deco = 0\nend\n",
        );
        let exports = classify_v1(&file).expect("a labelled-optional arrow is forwardable now");
        assert_eq!(exports.len(), 1);
        assert_eq!(exports[0].name, "my-deco");
    }

    #[test]
    fn classify_v01_sig_rejects_paren() {
        let file = v1_file(
            "module M :> sig\n  val my-paren : paren\nend = struct\n  val my-paren = 0\nend\n",
        );
        // NOT because 0.1's `paren` is a stand-in — `prim_types::t_paren`
        // matches saphe-split's `tPAREN` exactly, as the V0_0 arm matches
        // `v0.0.6 primitives.cppo.ml:86`. It rejects because the forward
        // wrapper is a PROJECTION of the 0.1 context onto 0.0.6's three
        // explicit scalars, and that has no inverse: the reverse call site has
        // no context to hand and the caller's explicit AXIS reaches 0.1 only
        // through the math font's MATH-table ratio, which nothing can set. See
        // `forked_note`'s `"paren"` arm.
        let err = classify_v1(&file)
            .expect_err("a 0.1 `paren` export must still reject in the reverse direction");
        match err {
            BoundaryError::ForkedTypeExport { ty_name, .. } => assert_eq!(ty_name, "paren"),
        }
    }

    #[test]
    fn classify_v01_sig_crosses_nested_module_under_composed_key() {
        // A nested member's seal key goes through `walk_nested_seals_a`'s path
        // composition — "push the child module's name onto the parent's" — so
        // the classifier reproduces exactly that, and the shadow's qualified
        // name is the composed `Outer.Inner.my-deco`.
        let file = v1_file(
            "module Outer :> sig\n  module Inner : sig val my-deco : deco end\nend = struct\n  \
             module Inner :> sig val my-deco : deco end = struct val my-deco = 0 end\nend\n",
        );
        let exports =
            classify_v1(&file).expect("a NESTED module's sig `val : deco` item must cross");
        assert_eq!(exports.len(), 1);
        assert_eq!(exports[0].kind, DecoKind::Deco);
        assert_eq!(
            deco_export_qualified_name(&exports[0]),
            "Outer.Inner.my-deco"
        );
    }

    #[test]
    fn classify_v01_sig_ignores_a_signature_member_that_binds_no_value() {
        // A `signature S = ..` MEMBER declares a signature, not a value:
        // `handle_signature_decl` only identity-checks it against the struct's
        // own `signature` bind, so no member of it is reachable at any path a
        // 0.0.6 consumer could name (0.0.6 has no signature syntax at all).
        // Nothing to cross — and therefore nothing to refuse either.
        let file = v1_file(
            "module Outer :> sig\n  signature S = sig val my-deco : deco end\nend = struct\n  \
             signature S = sig val my-deco : deco end\nend\n",
        );
        assert!(classify_v1(&file)
            .expect("a signature member binds no value — nothing to coerce")
            .is_empty());
    }

    #[test]
    fn classify_v01_sig_crosses_a_nested_module_typed_by_a_named_signature() {
        // The nested decl's signature is a NAME, not a literal `sig .. end`.
        // `surface::find_sig_keyed` dereferences it —
        // outward from the same `site_path` `module_check::resolve_sig` uses —
        // so the member lands under the composed key `Outer.Inner.my-deco`,
        // exactly as the literal spelling does.
        let file = v1_file(
            "module Outer :> sig\n  signature S = sig val my-deco : deco end\n  \
             module Inner : S\nend = struct\n  \
             signature S = sig val my-deco : deco end\n  \
             module Inner :> S = struct val my-deco = 0 end\nend\n",
        );
        let exports =
            classify_v1(&file).expect("a nested module typed by a NAMED signature must now cross");
        assert_eq!(exports.len(), 1);
        assert_eq!(exports[0].kind, DecoKind::Deco);
        assert_eq!(
            deco_export_qualified_name(&exports[0]),
            "Outer.Inner.my-deco"
        );
    }

    #[test]
    fn classify_v01_sig_crosses_through_an_include_at_the_enclosing_path() {
        // `include S` splices S's decls into the ENCLOSING signature in place
        // (`module_check::splice_decls`), so the member's path is the
        // includer's own — `Outer.my-deco`, NOT `Outer.S.my-deco`.
        let file = v1_file(
            "module Outer :> sig\n  signature S = sig val my-deco : deco end\n  include S\nend \
             = struct\n  signature S = sig val my-deco : deco end\n  val my-deco = 0\nend\n",
        );
        let exports = classify_v1(&file).expect("an `include`d `deco` export must cross");
        assert_eq!(exports.len(), 1);
        assert_eq!(deco_export_qualified_name(&exports[0]), "Outer.my-deco");
    }

    #[test]
    fn classify_v01_sig_crosses_through_a_with_type_refinement() {
        // A `with type` refinement narrows a TYPE member; every `val` decl's
        // SPELLED type is the base's, unchanged, so the scan reads through to
        // the base's decl list.
        let file = v1_file(
            "module Outer :> sig\n  \
             signature S = sig type t :: o  val my-deco : deco end\n  \
             module Inner : S with type t = int\nend = struct\n  \
             signature S = sig type t :: o  val my-deco : deco end\n  \
             module Inner :> S with type t = int = struct\n    \
             type t = int\n    val my-deco = 0\n  end\nend\n",
        );
        let exports = classify_v1(&file)
            .expect("a `with type`-refined nested signature must resolve to its base");
        assert_eq!(exports.len(), 1);
        assert_eq!(
            deco_export_qualified_name(&exports[0]),
            "Outer.Inner.my-deco"
        );
    }

    #[test]
    fn classify_v01_sig_rejects_a_deco_behind_a_functor_signature_member() {
        // The narrowing that genuinely survives: a functor is not a module, so
        // there is no `Outer.Make.my-deco` for a shadow to rebind; its members
        // exist only at an APPLICATION's path, in a file this scan cannot see.
        let file = v1_file(
            "module Outer :> sig\n  \
             module Make : (X : sig val n : int end) -> sig val my-deco : deco end\nend \
             = struct\n  \
             module Make = fun (X : sig val n : int end) -> struct val my-deco = 0 end\nend\n",
        );
        let err = classify_v1(&file)
            .expect_err("a `deco` behind a functor signature member must still reject");
        match err {
            BoundaryError::ForkedTypeExport { ty_name, .. } => assert_eq!(ty_name, "deco"),
        }
    }

    #[test]
    fn classify_v01_sig_unknown_signature_name_neither_crosses_nor_panics() {
        // An unresolvable NAME: `module_check::resolve_sig` turns this into a
        // precise "unknown signature name" error a moment later, so this scan
        // declines to guess rather than inventing text of its own — and, with
        // nothing textually reachable, has no `deco` to refuse either.
        let file = v1_file(
            "module Outer :> sig\n  module Inner : Nope\nend = struct\n  \
             module Inner = struct val my-deco = 0 end\nend\n",
        );
        assert!(classify_v1(&file)
            .expect("an unresolved name is downstream's error, not this scan's")
            .is_empty());
    }

    #[test]
    fn classify_v01_sig_self_including_signature_terminates() {
        // The cycle guard: `signature S = sig include S end` would otherwise
        // recur forever. Keyed by the RESOLVED table key, like
        // `module_check::resolve_named_sig`'s own guard.
        let file = v1_file(
            "module Outer :> sig\n  signature S = sig include S end\n  module Inner : S\nend \
             = struct\n  signature S = sig include S end\n  \
             module Inner = struct val my-deco = 0 end\nend\n",
        );
        assert!(classify_v1(&file)
            .expect("an include cycle is downstream's precise error, not a hang")
            .is_empty());
    }

    #[test]
    fn classify_v01_sig_ignores_type_only_mention() {
        // A transparent `type .. = deco` sig item merely NAMING
        // `deco`/`deco-set` (no value attached) is safe with zero coercion
        // — nothing to classify, and nothing to reject.
        let file = v1_file(
            "module M :> sig\n  type xver-deco-alias = deco\nend = struct\n  type xver-deco-alias = deco\nend\n",
        );
        assert!(classify_v1(&file)
            .expect("a type-only mention is safe")
            .is_empty());
    }

    #[test]
    fn classify_v01_sig_crosses_a_member_declared_at_a_type_synonym() {
        // The scan reads a `val`'s SPELLED type, and `t` is not a builtin —
        // so without expanding the signature's OWN `type t = deco` this
        // export would silently decline to cross, surfacing much later as an
        // ordinary `TypeError` at a 0.0.6 consumer's call site.
        let file = v1_file(
            "module M :> sig\n  type t = deco\n  val frame : length -> t\nend = struct\n  \
             type t = deco\n  val frame w p x y z = 0\nend\n",
        );
        let exports = classify_v1(&file).expect("a synonym OF `deco` is a deco export");
        assert_eq!(exports.len(), 1);
        assert_eq!(exports[0].name, "frame");
        assert_eq!(exports[0].kind, DecoKind::Deco);
        assert_eq!(exports[0].lead_arity, 1);
        assert_eq!(deco_export_qualified_name(&exports[0]), "M.frame");
    }

    #[test]
    fn classify_v01_sig_expands_a_synonym_chain_and_an_arrow_bodied_one() {
        // A chain (`u` -> `t` -> `deco`) resolves, and an ARROW-BODIED
        // synonym contributes its own lead positions — the wrapper has to
        // eta-expand over exactly as many arguments as the spelled-out form
        // would give it.
        let file = v1_file(
            "module M :> sig\n  type t = deco\n  type u = t\n  type framer = length -> u\n  \
             val frame : color -> framer\nend = struct\n  val frame c w p x y z = 0\nend\n",
        );
        let exports = classify_v1(&file).expect("a synonym CHAIN is still a deco export");
        assert_eq!(exports.len(), 1);
        assert_eq!(exports[0].kind, DecoKind::Deco);
        assert_eq!(
            exports[0].lead_arity, 2,
            "one lead position from the `val`'s own arrow, one from the synonym's body"
        );
    }

    #[test]
    fn classify_v01_sig_crosses_a_synonym_declared_in_an_included_signature() {
        // `include S` splices S's decls into the enclosing signature in
        // place, so a synonym S declares is in scope for the includer's own
        // `val` decls — the same scope `module_check::splice_decls` gives it.
        let file = v1_file(
            "module Outer :> sig\n  signature S = sig type t = deco end\n  include S\n  \
             val frame : t\nend = struct\n  signature S = sig type t = deco end\n  \
             type t = deco\n  val frame = 0\nend\n",
        );
        let exports = classify_v1(&file).expect("an `include`d synonym is in scope");
        assert_eq!(exports.len(), 1);
        assert_eq!(deco_export_qualified_name(&exports[0]), "Outer.frame");
    }

    #[test]
    fn classify_v01_sig_crosses_a_nested_members_use_of_an_enclosing_synonym() {
        // A nested `sig` sees its parent's type declarations, so the map is
        // threaded down rather than reset at each layer.
        let file = v1_file(
            "module Outer :> sig\n  type t = deco\n  module Inner : sig val frame : t end\nend \
             = struct\n  type t = deco\n  module Inner :> sig val frame : t end \
             = struct val frame = 0 end\nend\n",
        );
        let exports = classify_v1(&file).expect("an enclosing layer's synonym is in scope");
        assert_eq!(exports.len(), 1);
        assert_eq!(deco_export_qualified_name(&exports[0]), "Outer.Inner.frame");
    }

    #[test]
    fn classify_v01_sig_opaque_type_is_not_a_deco_and_does_not_cross() {
        // The distinction that matters: an OPAQUE `type t :: o` names no
        // forked type at all, so it must NOT start being coerced — nor
        // rejected. (And it is not the builtin of the same name either: a
        // signature-declared `type deco :: o` shadows it.)
        let file = v1_file(
            "module M :> sig\n  type t :: o\n  val frame : length -> t\nend = struct\n  \
             type t = int\n  val frame w = 0\nend\n",
        );
        assert!(classify_v1(&file)
            .expect("an opaque type is not a deco")
            .is_empty());

        let shadowed = v1_file(
            "module M :> sig\n  type deco :: o\n  val frame : deco\nend = struct\n  \
             type deco = int\n  val frame = 0\nend\n",
        );
        assert!(
            classify_v1(&shadowed)
                .expect("a locally-declared `deco` is not the builtin one")
                .is_empty(),
            "map-first lookup: a signature's own `type deco` shadows the builtin, so no \
             coercion wrapper may be generated for a value that is not a `deco` at all"
        );
    }

    #[test]
    fn classify_v01_sig_rejects_a_synonym_of_deco_buried_in_a_compound() {
        // The deliberate rejection survives synonym expansion: a `deco` the
        // positional wrapper cannot express is refused just as loudly when
        // it is spelled through a synonym.
        let file = v1_file(
            "module M :> sig\n  type t = deco\n  val frames : t list\nend = struct\n  \
             val frames = 0\nend\n",
        );
        let err = classify_v1(&file).expect_err("a buried deco must reject, synonym or not");
        match err {
            BoundaryError::ForkedTypeExport { ty_name, .. } => assert_eq!(ty_name, "deco"),
        }
    }

    #[test]
    fn classify_v01_sig_synonym_cycle_terminates() {
        // `type t = u  type u = t` is a later phase's error; this scan must
        // decline rather than loop.
        let file = v1_file(
            "module M :> sig\n  type t = u\n  type u = t\n  val frame : t\nend = struct\n  \
             val frame = 0\nend\n",
        );
        assert!(classify_v1(&file)
            .expect("a synonym cycle is downstream's error, not a hang")
            .is_empty());
    }

    #[test]
    fn classify_v01_sig_crosses_a_with_type_refined_deco() {
        // The other spelling of the same false negative: the base declares
        // `type t :: o` opaquely and the USE SITE refines it to `deco`, so
        // the member really is a `deco` at this signature.
        let file = v1_file(
            "module Outer :> sig\n  \
             signature S = sig type t :: o  val frame : t end\n  \
             module Inner : S with type t = deco\nend = struct\n  \
             signature S = sig type t :: o  val frame : t end\n  \
             module Inner :> S with type t = deco = struct\n    \
             type t = deco\n    val frame = 0\n  end\nend\n",
        );
        let exports = classify_v1(&file).expect("a `with type`-refined `deco` member crosses");
        assert_eq!(exports.len(), 1);
        assert_eq!(deco_export_qualified_name(&exports[0]), "Outer.Inner.frame");
    }

    #[test]
    fn classify_v01_sig_crosses_a_with_submodule_type_refined_deco() {
        // `S with M type t = deco`: the refinement descends into the named
        // member, where it makes that member's own `t` transparent — and the
        // export crosses.
        let file = v1_file(
            "module Outer :> sig\n  \
             module Inner : sig type t :: o  val frame : t end\n\
             end with Inner type t = deco = struct\n  \
             module Inner :> sig type t :: o  val frame : t end \
             = struct type t = deco  val frame = 0 end\nend\n",
        );
        let exports =
            classify_v1(&file).expect("a `with M type`-refined `deco` member must cross");
        assert_eq!(exports.len(), 1);
        assert_eq!(deco_export_qualified_name(&exports[0]), "Outer.Inner.frame");
    }

    #[test]
    fn classify_v01_sig_empty_for_no_sig() {
        let file = v1_file("module M = struct\n  val my-deco p w h d = 0\nend\n");
        assert!(
            classify_v1(&file)
                .expect("no sig, nothing to see")
                .is_empty(),
            "an UNSEALED module (no sig_annot at all) has no textual site for this scan to read"
        );
    }

    #[test]
    fn classify_v01_sig_empty_for_document() {
        let file = v1_file("0\n");
        assert!(classify_v1(&file)
            .expect("a document is never a dependency")
            .is_empty());
    }

    fn one_deco_export() -> Vec<DecoExport> {
        let file = v1_file(
            "module M :> sig\n  val my-deco : length -> deco\nend = struct\n  val my-deco t p w h d = 0\nend\n",
        );
        classify_v1(&file).expect("classify")
    }

    fn binding_name(tb: &cst::TopBinding) -> &str {
        match tb {
            cst::TopBinding::Let(tl) => tl.name.name.as_str(),
            other => panic!("expected a Let binding, got {other:?}"),
        }
    }

    #[test]
    fn deco_downgrade_capture_binds_only_a_private_name() {
        // The capture must NOT rebind `M.my-deco`: it is spliced while the 0.1
        // view is still the installed one, and rebinding there would hand the
        // coerced shape to the very 0.1 code the schedule protects.
        let out = deco_downgrade_prelude(&one_deco_export(), DowngradeStep::Capture);
        assert_eq!(out.len(), 1);
        assert_eq!(binding_name(&out[0]), "xver-rev-orig-M-my-deco");
    }

    #[test]
    fn deco_downgrade_install_rebinds_the_qualified_key() {
        // The shadow is bound under the export's own DOTTED qualified key —
        // no surface syntax spells that; see `deco_downgrade_prelude`.
        let out = deco_downgrade_prelude(&one_deco_export(), DowngradeStep::Install);
        assert_eq!(out.len(), 1);
        assert_eq!(binding_name(&out[0]), "M.my-deco");
    }

    #[test]
    fn deco_downgrade_restore_rebinds_the_qualified_key_to_the_capture() {
        // The restore rebinds the same dotted key straight back to the private
        // capture, so a 0.1 dependency after a 0.0.6 one reads the export at
        // exactly the scheme the exporting module sealed.
        let out = deco_downgrade_prelude(&one_deco_export(), DowngradeStep::Restore);
        assert_eq!(out.len(), 1);
        assert_eq!(binding_name(&out[0]), "M.my-deco");
        let src = format!("{:?}", out[0]);
        assert!(
            src.contains("xver-rev-orig-M-my-deco"),
            "the restore's body must name the private capture, got: {src}"
        );
    }

    #[test]
    fn deco_downgrade_private_name_is_a_function_of_the_qualified_key_alone() {
        // Load-bearing for the placement schedule: `Capture` and every later
        // `Install`/`Restore` are SEPARATE calls, so they can only agree on the
        // private name if it depends on nothing call-local.
        let exports = one_deco_export();
        let capture = deco_downgrade_prelude(&exports, DowngradeStep::Capture);
        let restore = deco_downgrade_prelude(&exports, DowngradeStep::Restore);
        assert!(format!("{:?}", restore[0]).contains(binding_name(&capture[0])));
    }

    #[test]
    fn deco_downgrade_prelude_empty_is_empty() {
        assert!(deco_downgrade_prelude(&[], DowngradeStep::Capture).is_empty());
        assert!(deco_downgrade_prelude(&[], DowngradeStep::Install).is_empty());
        assert!(deco_downgrade_prelude(&[], DowngradeStep::Restore).is_empty());
    }

    #[test]
    fn classify_v01_sig_does_not_perturb_forward_toplevel_letrec() {
        // Non-regression: the reverse scan must not change the FORWARD
        // direction's existing top-level `let-rec` acceptance path at all
        // (a wholly separate function operating on a wholly separate CST
        // type — `cst_v1::FileV1`, not `cst::TopBinding`).
        let prelude = prelude_of("let-rec xver-my-deco : deco | (x, y) w h d = []\n0\n");
        let exports = classify_deco_exports(&prelude, v006(), v01())
            .expect("bare `: deco` must still be accepted forward");
        assert_eq!(exports.len(), 1);
    }

    // ------------------------------------------------------------------
    // Nested-module deco exports (the forward direction's own recursion):
    // a `deco` export inside a `module .. = struct .. end` — or inside a
    // module inside a module — is classified and wrapped.
    // ------------------------------------------------------------------

    #[test]
    fn classify_deco_in_sigless_module_letrec_ascription() {
        let prelude = prelude_of(
            "module XverMod = struct\n  \
             let-rec frame : length -> deco | t (x, y) w h d = []\nend\n0\n",
        );
        let exports = classify_deco_exports(&prelude, v006(), v01()).expect(
            "a `let-rec .. : deco` inside a sig-less module must be classified, not rejected",
        );
        assert_eq!(exports.len(), 1);
        assert_eq!(exports[0].name, "frame");
        assert_eq!(exports[0].kind, DecoKind::Deco);
        assert_eq!(exports[0].lead_arity, 1);
        assert_eq!(exports[0].module_path, vec!["XverMod".to_string()]);
    }

    #[test]
    fn classify_deco_in_doubly_nested_module_sig() {
        let prelude = prelude_of(
            "module Outer = struct\n  \
             module Inner : sig\n    val frame : length -> deco\n  end = struct\n    \
             let frame t (x, y) w h d = []\n  end\nend\n0\n",
        );
        let exports = classify_deco_exports(&prelude, v006(), v01())
            .expect("a doubly-nested module's sig `deco` export must be classified");
        assert_eq!(exports.len(), 1);
        assert_eq!(
            exports[0].module_path,
            vec!["Outer".to_string(), "Inner".to_string()]
        );
    }

    #[test]
    fn classify_deco_in_module_sig_is_not_double_wrapped_by_its_own_ascription() {
        // The `skip` set: a member declared in the module's `sig` AND
        // carrying its own `: deco` ascription must yield exactly ONE
        // wrapper, never two (two would unite an already-united graphics).
        let prelude = prelude_of(
            "module XverMod : sig\n  val frame : length -> deco\nend = struct\n  \
             let-rec frame : length -> deco | t (x, y) w h d = []\nend\n0\n",
        );
        let exports = classify_deco_exports(&prelude, v006(), v01()).expect("classify");
        assert_eq!(
            exports.len(),
            1,
            "one wrapper per export, even when sig and ascription both name the type"
        );
    }

    #[test]
    fn classify_deco_in_nested_module_accepts_an_optional_argument_arrow() {
        // The recursion into a module must classify the export AND record
        // WHICH leading parameters are optional, since forwarding a 0.0.6
        // optional depends on knowing that.
        let prelude = prelude_of(
            "module XverMod = struct\n  \
             let-rec frame : length ?-> length -> deco | t (x, y) w h d = []\nend\n0\n",
        );
        let exports = classify_deco_exports(&prelude, v006(), v01())
            .expect("an optional-argument arrow is forwardable now");
        assert_eq!(exports.len(), 1);
        assert_eq!(exports[0].module_path, vec!["XverMod".to_string()]);
        assert!(
            exports[0].lead_opts.contains(&LeadOpt::V006Optional),
            "the optional slot must be recorded, not flattened into a positional one: {:?}",
            exports[0].lead_opts
        );
    }
}