Stop using infer_conv_ustate in unification

[SkySkimmer]

The type compatibility check throws away the univ constraints, so we use a univ-ignoring comparison instead.

The main call is incorrect when alpha equality infers unsatisfiable constraints and reducing is needed.

Fix #21674

[SkySkimmer]

@coqbot bench

[coqbot-app]

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]      │           CPU instructions            │  max resident mem [KB]  │
│                                     │                         │                                       │                         │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│ coq-neural-net-interp-computed-lite │  237.18   239.65  -1.03 │  2270733579236   2270774583632  -0.00 │  895620   895236   0.04 │
│                 rocq-mathcomp-field │  201.74   202.79  -0.52 │  1545757082978   1545773284397  -0.00 │ 2963148  2965172  -0.07 │
│                        rocq-runtime │   74.39    74.73  -0.45 │   541588328775    541490784041   0.02 │  501984   501936   0.01 │
│                 rocq-mathcomp-order │   81.23    81.59  -0.44 │   600558179035    600554955741   0.00 │ 1983980  1983104   0.04 │
│              rocq-mathcomp-solvable │  106.58   106.93  -0.33 │   745353356006    748838580682  -0.47 │ 1531180  1535612  -0.29 │
│                           rocq-elpi │   15.82    15.86  -0.25 │   111007743354    111012448795  -0.00 │  577336   576852   0.08 │
│                         coq-coqutil │   47.42    47.53  -0.23 │   294266555253    294261632464   0.00 │  568632   568540   0.02 │
│                    coq-math-classes │   83.73    83.89  -0.19 │   508730796004    508797014323  -0.01 │  514372   519100  -0.91 │
│              rocq-metarocq-template │   84.78    84.92  -0.16 │   581536676659    581576772448  -0.01 │ 1059632  1057048   0.24 │
│        coq-fiat-crypto-with-bedrock │ 7301.51  7312.93  -0.16 │ 59970579403234  59978025173601  -0.01 │ 3139308  3132556   0.22 │
│                   coq-iris-examples │  370.10   370.12  -0.01 │  2425468927092   2424457316102   0.04 │ 1117264  1113152   0.37 │
│              rocq-mathcomp-fingroup │   27.41    27.41   0.00 │   180110348589    179717751983   0.22 │  645104   645728  -0.10 │
│                            coq-core │    2.68     2.68   0.00 │    18289204415     18289128772   0.00 │   90076    89548   0.59 │
│               coq-engine-bench-lite │  129.02   129.00   0.02 │   959281177219    961293073549  -0.21 │ 1007916  1007720   0.02 │
│               rocq-mathcomp-algebra │  348.16   348.07   0.03 │  2614841061550   2611850154920   0.11 │ 1625020  1625620  -0.04 │
│                 rocq-metarocq-utils │   24.25    24.23   0.08 │   157603578613    157562573126   0.03 │  592888   593072  -0.03 │
│                            coq-hott │  159.17   159.03   0.09 │  1068849258059   1069008498550  -0.01 │  454560   458256  -0.81 │
│                  rocq-mathcomp-boot │   39.88    39.84   0.10 │   235033403705    234949349457   0.04 │  751580   751664  -0.01 │
│             rocq-mathcomp-character │  108.79   108.68   0.10 │   783728427899    783774294978  -0.01 │ 2219472  2219916  -0.02 │
│                             coq-vst │  854.39   853.45   0.11 │  6455191122283   6454787796779   0.01 │ 2233936  2207480   1.20 │
│                         rocq-stdlib │  435.43   434.68   0.17 │  1567586738113   1546736212723   1.35 │  650344   655076  -0.72 │
│              coq-mathcomp-odd-order │  628.55   627.37   0.19 │  4513598805436   4513034457399   0.01 │ 3750316  3752892  -0.07 │
│         coq-rewriter-perf-SuperFast │  481.47   480.39   0.22 │  3751979650797   3751669005395   0.01 │ 1250568  1231872   1.52 │
│                        rocq-bignums │   25.86    25.80   0.23 │   164035242983    163999347189   0.02 │  463144   460372   0.60 │
│          coq-performance-tests-lite │  906.03   903.83   0.24 │  7248527293713   7247242844049   0.02 │ 1234396  1226892   0.61 │
│                    coq-fiat-parsers │  279.66   278.98   0.24 │  2145628226264   2139525230705   0.29 │ 2317140  2249668   3.00 │
│                        coq-rewriter │  336.10   335.20   0.27 │  2501732566244   2500829601441   0.04 │ 1525848  1526004  -0.01 │
│                           coq-verdi │   44.48    44.35   0.29 │   294137820381    294164637627  -0.01 │  526652   527896  -0.24 │
│               coq-mathcomp-analysis │ 1206.86  1202.96   0.32 │  9102114308064   9101082332478   0.01 │ 2649880  2651480  -0.06 │
│                       coq-fourcolor │ 1371.85  1367.37   0.33 │ 12579485961884  12579095781313   0.00 │ 1458964  1462372  -0.23 │
│                        coq-compcert │  308.62   307.59   0.33 │  2021788695515   2019710612809   0.10 │ 1163868  1163784   0.01 │
│               rocq-metarocq-erasure │  483.42   481.56   0.39 │  3300380596123   3297982268107   0.07 │ 1787452  1789908  -0.14 │
│                      coq-verdi-raft │  501.00   498.95   0.41 │  3452318085480   3450950514864   0.04 │  822176   822260  -0.01 │
│                rocq-metarocq-common │   41.22    41.05   0.41 │   265149687513    264710630003   0.17 │  915552   928272  -1.37 │
│                         coq-unimath │ 1819.95  1812.32   0.42 │ 15082667636144  15079020419055   0.02 │ 1063764  1101872  -3.46 │
│                       coq-fiat-core │   56.90    56.66   0.42 │   345934283478    345891781892   0.01 │  482856   484756  -0.39 │
│                           coq-color │  235.09   234.08   0.43 │  1488910010183   1487921054804   0.07 │ 1174652  1181468  -0.58 │
│                        coq-bedrock2 │  362.73   359.80   0.81 │  3002997625960   3003172156844  -0.01 │  887636   892536  -0.55 │
│                      coq-coquelicot │   40.63    40.30   0.82 │   246108877994    246099714558   0.00 │  839796   839932  -0.02 │
│                        coq-coqprime │   54.21    53.70   0.95 │   368332031211    368259494042   0.02 │  825956   825984  -0.00 │
│                 coq-category-theory │  561.15   555.81   0.96 │  4075890686264   4053442481878   0.55 │  879328   895384  -1.79 │
│                      rocq-equations │    8.77     8.68   1.04 │    59943162341     59951600704  -0.01 │  401928   399872   0.51 │
│                            coq-corn │  670.17   660.46   1.47 │  4506000422892   4458561793673   1.06 │  754632   736932   2.40 │
│          rocq-metarocq-translations │   16.99    16.72   1.61 │   119315747079    119332842843  -0.01 │  778964   777380   0.20 │
│           rocq-metarocq-safechecker │  345.29   336.62   2.58 │  2519318150129   2479480233959   1.61 │ 1867688  1790036   4.34 │
│                 rocq-metarocq-pcuic │  654.83   634.03   3.28 │  4171958970926   4071949426769   2.46 │ 2265700  2315180  -2.14 │
│                           rocq-core │    6.81     6.57   3.65 │    40604121873     40608089840  -0.01 │  445768   443704   0.47 │
│             rocq-mathcomp-ssreflect │    1.17     1.12   4.46 │     7719737703      7720516830  -0.01 │  848996   849164  -0.02 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

🐢 Top 25 slow downs

┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                    TOP 25 SLOW DOWNS                                                     │
│                                                                                                                          │
│   OLD     NEW    DIFF     %DIFF     Ln                  FILE                                                             │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│    62.4   66.1  3.6401      5.83%   608  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                     │
│    1.76   3.00  1.2402     70.38%  1479  rocq-metarocq-pcuic/pcuic/theories/PCUICSubstitution.v.html                     │
│    93.8   95.0  1.2249      1.31%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│    2.06   2.89  0.8297     40.37%   102  coq-fiat-parsers/src/Parsers/ParserImplementation.v.html                        │
│    2.47   3.27  0.8081     32.78%    34  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html          │
│   0.856   1.57  0.7094     82.84%  2601  rocq-metarocq-safechecker/safechecker/theories/PCUICTypeChecker.v.html          │
│   0.933   1.61  0.6750     72.36%  2493  rocq-metarocq-safechecker/safechecker/theories/PCUICTypeChecker.v.html          │
│    21.2   21.8  0.6221      2.93%   651  rocq-stdlib/theories/Zmod/ZmodBase.v.html                                       │
│    1.18   1.80  0.6171     52.11%    78  rocq-metarocq-pcuic/pcuic/theories/PCUICConversion.v.html                       │
│   0.304  0.915  0.6114    201.15%   153  rocq-mathcomp-algebra/algebra/spectral.v.html                                   │
│   0.668   1.26  0.5912     88.47%   298  rocq-metarocq-pcuic/pcuic/theories/Bidirectional/BDUnique.v.html                │
│    9.25   9.83  0.5791      6.26%   434  coq-mathcomp-odd-order/theories/PFsection12.v.html                              │
│   0.792   1.37  0.5732     72.38%   395  rocq-metarocq-pcuic/pcuic/theories/PCUICElimination.v.html                      │
│   0.316  0.876  0.5602    177.53%   245  rocq-metarocq-pcuic/pcuic/theories/PCUICSR.v.html                               │
│    16.9   17.4  0.5558      3.30%   905  coq-unimath/UniMath/ModelCategories/Generated/LNWFSCocomplete.v.html            │
│   0.686   1.23  0.5417     78.98%   278  rocq-metarocq-pcuic/pcuic/theories/Bidirectional/BDUnique.v.html                │
│   0.657   1.19  0.5357     81.48%   266  rocq-metarocq-pcuic/pcuic/theories/Bidirectional/BDUnique.v.html                │
│   0.616   1.12  0.5067     82.31%   770  rocq-metarocq-pcuic/pcuic/theories/PCUICEquality.v.html                         │
│    1.58   2.08  0.4984     31.58%    42  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html        │
│    94.4   94.9  0.4888      0.52%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│   0.196  0.668  0.4715    240.40%   682  rocq-stdlib/theories/Numbers/DecimalFacts.v.html                                │
│    58.3   58.7  0.4710      0.81%   660  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html           │
│ 0.00100  0.437  0.4361  43439.54%   292  coq-mathcomp-odd-order/theories/BGsection11.v.html                              │
│   0.491  0.915  0.4237     86.26%   409  rocq-metarocq-pcuic/pcuic/theories/PCUICConvCumInversion.v.html                 │
│   0.459  0.882  0.4230     92.07%  1815  rocq-metarocq-safechecker/safechecker/theories/PCUICTypeChecker.v.html          │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                           TOP 25 SPEED UPS                                                            │
│                                                                                                                                       │
│  OLD     NEW     DIFF     %DIFF    Ln                    FILE                                                                         │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  67.2     62.4  -4.8098   -7.15%   608  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │
│   203      201  -2.2395   -1.10%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │
│  61.2     59.3  -1.8370   -3.00%    27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                      │
│  5.36     4.34  -1.0172  -18.98%  2862  rocq-metarocq-safechecker/safechecker/theories/PCUICTypeChecker.v.html                        │
│   120      119  -0.9882   -0.83%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                        │
│  94.7     93.9  -0.7761   -0.82%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                   │
│  29.6     28.9  -0.6926   -2.34%    31  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html          │
│  1.17    0.497  -0.6724  -57.49%  1604  rocq-stdlib/theories/micromega/Tauto.v.html                                                   │
│ 0.772    0.233  -0.5391  -69.80%    17  rocq-stdlib/theories/micromega/Env.v.html                                                     │
│  27.4     26.9  -0.5147   -1.88%    34  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html          │
│ 0.426  0.00327  -0.4230  -99.23%    75  rocq-mathcomp-algebra/algebra/spectral.v.html                                                 │
│ 0.423  0.00938  -0.4138  -97.78%   154  rocq-mathcomp-algebra/algebra/spectral.v.html                                                 │
│ 0.446   0.0387  -0.4077  -91.33%   140  rocq-mathcomp-solvable/solvable/extraspecial.v.html                                           │
│  21.9     21.5  -0.4015   -1.83%    49  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                       │
│ 0.683    0.289  -0.3943  -57.73%    19  rocq-stdlib/theories/ZArith/Int.v.html                                                        │
│  30.4     30.0  -0.3820   -1.26%   307  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/Addchain.v.html                            │
│ 0.806    0.425  -0.3815  -47.31%    59  rocq-stdlib/theories/ZArith/Zeuclid.v.html                                                    │
│  27.7     27.4  -0.3689   -1.33%   129  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Projective.v.html                         │
│  24.0     23.7  -0.3641   -1.52%   777  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                          │
│  1.18    0.818  -0.3611  -30.63%   408  rocq-stdlib/theories/MSets/MSetAVL.v.html                                                     │
│  28.7     28.3  -0.3297   -1.15%   795  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                          │
│  22.9     22.6  -0.3282   -1.43%  1073  rocq-metarocq-safechecker/safechecker/theories/PCUICSafeReduce.v.html                         │
│  1.04    0.722  -0.3154  -30.40%   702  rocq-stdlib/theories/Numbers/HexadecimalFacts.v.html                                          │
│  31.5     31.2  -0.3120   -0.99%   259  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord.v.html                                    │
│ 0.754    0.443  -0.3111  -41.25%    11  rocq-stdlib/theories/ZArith/Zpow_alt.v.html                                                   │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

• 🪑 GitLab Bench Job

[ppedrot]

Strangely enough it seems to be slightly slower on some examples.

[SkySkimmer]

If syntactic equality produces invalid constraints we now do full conversion, so it makes sense that some cases are slower IMO

[ppedrot]

It's not a crazy slowdown so it's fine to me. Should we backport this to 9.2.X though?