Skip to content

decrease priority for rtc_reflexive instance

Ralf Jung requested to merge ralf/rtc into master

We give this instance a lower-than-usual priority because when it is applied to Reflexive ?, it leads to a new evar being created for R. Unfortunately, we cannot set Hint Mode for Reflexive in a way that just rules out Reflexive ? [1], but we can at least stop TC search from using this instance. This helps performance because it gives TC search less freedom in the remainder of the search. It doesn't seem like backtracking is happening here.

Also see the discussion below https://gitlab.mpi-sws.org/FP/iris-coq/commit/8e8c722870b36c23032d9bc10019e40e6eb6be62. I think this is useful even if we decide to roll back the IntoVal change as there may be other places where rtc_reflexive inadvertently gets chosen.

[1] That would break https://gitlab.mpi-sws.org/FP/iris-coq/blob/38ba379fae88865ed3a06ba44bf22938b6524610/theories/algebra/list.v#L213

Edited by Ralf Jung

Merge request reports