Commit 2024-04-29 16:41 0924a3d4

feat: FastSubsingleton and FastIsEmpty to speed up congr!/convert (#12495) This is a PR that's a temporary measure to improve performance of congr!/convert, and the implementation may change in a future PR with a new version of congr!. Introduces two typeclasses that are meant to quickly evaluate in common cases of Subsingleton and IsEmpty. Makes congr! use these typeclasses rather than Subsingleton. Local Subsingleton/IsEmpty instances are included as Fast instances. To get congr!/convert to reason about subsingleton types, you can add such instances to the local context. Or, you can apply Subsingleton.elim yourself. Zulip discussion