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 ? , 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.