Perform `fast_done` first in `naive_solver`.
naive_solver tearing whole goals apart, even if the goal appears exactly as a hypothesis.
In Iris/C I ran into this problem after the recent
set_solver changes (4ff965b2). Since
set_unfold unfolds more stuff than it used to do,
naive_solver essentially had to solve
P → P. However, since it was tearing the entire goal apart, and trying to reestablish it while there were other assumptions in the context that influenced instantiation of existentials, it was not able to solve
P again. By performing
fast_done eagerly, it will not simply solve
P → P immediately without tearing the entire goal apart.
It appears that the impact on e.g. LambdaRust is in the noise range: https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=lambda-rust&var-branch1=master&var-commit1=4ad3f8b08c1ff4481d0fab41f878b215257a6462&var-config1=coq-8.9.0&var-branch2=ci%2Frobbert%2Fnaive_solver&var-commit2=11c5f900bf7b1f9fdaf4ba8cfc36d601bb5abdbf&var-config2=coq-8.9.0&var-group=().*&var-metric=instructions