Commit 2026-02-12 13:23 e3e3ff8b

perf(to_dual): first try translating without inserting casts (#35131) This PR addresses the performance regression introduced by #32438. The problem is that deciding where casts need to be inserted is an expensive operation (similarly expensive to kernel type checking). I expect that in category theory this will be particularly significant. Most uses of to_dual don't need any casts to be inserted at all. So, it is more efficient to simply first try translating without inserting casts. And if that fails, we insert casts and then try again. So after this PR, in the failure case, to_dual will check the term 4 times:

• first try the translation without casts
• then determine where casts should go
• then try the translation of this
• then use Meta.check to get a nicer error message. This is OK, since the failure case is not the performance critical case.