make empty operational typeclass TC opaque

Like iris!914 (merged), but only for the Empty typeclass which (being just a constant) is particularly prone to Coq TC instance "hallucination".

It would be great to have a test case.

I don't think I know how to reproduce this "hallucination" in a small example, unfortunately.

Anyway we have a whole bunch of failures in reverse deps:

• https://gitlab.mpi-sws.org/iris/gpfsl/-/jobs/231434
• https://gitlab.mpi-sws.org/iris/iron/-/jobs/231435
• https://gitlab.mpi-sws.org/iris/lambda-rust/-/jobs/231431
• https://gitlab.mpi-sws.org/iris/lambda-rust/-/jobs/231432
• https://gitlab.mpi-sws.org/iris/reloc/-/jobs/231436
• https://gitlab.mpi-sws.org/iris/actris/-/jobs/231439

I haven't looked deeper into them, but this seems pretty clear:

File "./gpfsl-examples/queue/proof_ms_abs_graph.v", line 1737, characters 6-26:
Error: Tactic failure: iFrame: cannot frame
(@{Vh} SeenEnqueuedLink_val ∅ ∅ [(ηs, s)] ηs s)%I.

It seems this experiment failed, should we close? Or maybe have an issue to discuss other options?

Yeah, let's close for now and I'll try to create a testcase next time I run into this.

closed