Commit 2023-07-28 11:36 7bedbaeb

feat: make congr!'s typeEq plausibility heuristic consider binder info (#5900) There are cases where we want convert/congr! to generate equalities between types, even if they don't pass the plausibility test. The examples involve types that are explicit arguments without forward dependencies, which seems like a reasonable rule to try out. We exclude forward dependencies because those lead to heterogenous equalities.