Commit 2026-09-23 16:06 2bc4889b

feat(Translate): better relevant_arg heuristic (#43801) This PR improves the heuristic around relevant_arg that to_dual and to_additive use. Currently, the we eagerly set (relevant_arg := 1) whenever we cannot find any relevant argument. This is problematic in a setting where there really should be no relevant argument, such as for ComplexShape. After this PR, we only default to (relevant_arg := 1) for types (i.e. anything whose type is Sort _). For terms that aren't types, we instead purely rely on the algorithm that determines the relevant argument (which was added in #35318). In order for this algorithm to work in all cases, relevant_arg needs to be set on all relevant types. This includes some types that are dual to themselves, like LE and LinearOrder, and hence do not have a to_dual attribute (and hence also don't have a relevant_arg). To fix this, I added the following trick: when we add a translation for a class projection or class constructor, and if that class has no translation, then we first add a translation from that class to itself. As a result, classes like LE and LinearOrder are now part of the translation dictionary, and are being translated into themselves.