Экзистенциальные цели слишком быстро заполняются

Похоже, что simple notypeclasses refine {| obj := _ |} выполняет трюк.

• {| obj := _|} - это синтаксис записи, который работает как сокращенное обозначение Build_Category _ _ _ _ _.
• simple notypeclasses refine - все одной тактикой. Это вариант notypeclasses refine, который не откладывает цели и не выполняет никаких действий.
• К сожалению, в отличие от unshelve нет универсального комбинатора notypeclasses. Есть только notypeclasses refine и simple notypeclasses refine.

Для отладки вы можете использовать (недокументированные) Set Typeclasses Debug. Это показывает, что eapply Build_Category разрешает некоторые типы классов, а refine {| obj := _|} еще хуже.

В стороне, я не думаю, что имеет смысл иметь Class Category без каких-либо параметров уровня уровня - почему бы вам когда-либо хотеть, чтобы любая категория автоматически определялась?