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, 7 insertions, 13 deletions

diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index e0dc5bcfa8..d64a911550 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -1990,13 +1990,10 @@ zonkWCRec (WC { wc_simple = simple, wc_impl = implic })
        ; return (WC { wc_simple = simple', wc_impl = implic' }) }
 
 zonkSimples :: Cts -> TcM Cts
-zonkSimples cts = do { cts' <- mapBagM zonkCt' cts
+zonkSimples cts = do { cts' <- mapBagM zonkCt cts
                      ; traceTc "zonkSimples done:" (ppr cts')
                      ; return cts' }
 
-zonkCt' :: Ct -> TcM Ct
-zonkCt' ct = zonkCt ct
-
 {- Note [zonkCt behaviour]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 zonkCt tries to maintain the canonical form of a Ct.  For example,
@@ -2035,15 +2032,12 @@ zonkCt ct@(CDictCan { cc_ev = ev, cc_tyargs = args })
        ; args' <- mapM zonkTcType args
        ; return $ ct { cc_ev = ev', cc_tyargs = args' } }
 
-zonkCt ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = rhs })
-  = do { ev'    <- zonkCtEvidence ev
-       ; tv_ty' <- zonkTcTyVar tv
-       ; case getTyVar_maybe tv_ty' of
-           Just tv' -> do { rhs' <- zonkTcType rhs
-                          ; return ct { cc_ev    = ev'
-                                      , cc_tyvar = tv'
-                                      , cc_rhs   = rhs' } }
-           Nothing  -> return (mkNonCanonical ev') }
+zonkCt (CTyEqCan { cc_ev = ev })
+  = mkNonCanonical <$> zonkCtEvidence ev
+  -- CTyEqCan has some delicate invariants that may be violated by
+  -- zonking (documented with the Ct type) , so we don't want to create
+  -- a CTyEqCan here. Besides, this will be canonicalized again anyway,
+  -- so there is very little benefit in keeping the CTyEqCan constructor.
 
 zonkCt ct@(CIrredCan { cc_ev = ev }) -- Preserve the cc_insol flag
   = do { ev' <- zonkCtEvidence ev