Implement a coverage checker for injectivity

This fixes #16512.

There are lots of parts of this patch:

* The main payload is in FamInst. See
Note [Coverage condition for injective type families] there
for the overview. But it doesn't fix the bug.

* We now bump the reduction depth every time we discharge
a CFunEqCan. See Note [Flatten when discharging CFunEqCan]
in TcInteract.

* Exploration of this revealed a new, easy to maintain invariant
for CTyEqCans. See Note [Almost function-free] in TcRnTypes.

* We also realized that type inference for injectivity was a
bit incomplete. This means we exchanged lookupFlattenTyVar for
rewriteTyVar. See Note [rewriteTyVar] in TcFlatten. The new
function is monadic while the previous one was pure, necessitating
some faff in TcInteract. Nothing too bad.

* zonkCt did not maintain invariants on CTyEqCan. It's not worth
the bother doing so, so we just transmute CTyEqCans to
CNonCanonicals.

* The pure unifier was finding the fixpoint of the returned
substitution, even when doing one-way matching (in tcUnifyTysWithTFs).
Fixed now.

Test cases: typecheck/should_fail/T16512{a,b}

1 files changed, 1 insertions, 1 deletions

diff --git a/compiler/utils/Util.hs b/compiler/utils/Util.hs
index d6cea5ca8d..c484ba90ea 100644
--- a/compiler/utils/Util.hs
+++ b/compiler/utils/Util.hs
@@ -387,7 +387,7 @@ filterByLists _          _      _      = []
 -- to 'True' go to the left; elements corresponding to 'False' go to the right.
 -- For example, @partitionByList [True, False, True] [1,2,3] == ([1,3], [2])@
 -- This function does not check whether the lists have equal
--- length.
+-- length; when one list runs out, the function stops.
 partitionByList :: [Bool] -> [a] -> ([a], [a])
 partitionByList = go [] []
   where