Remove flattening variables

This patch redesigns the flattener to simplify type family applications
directly instead of using flattening meta-variables and skolems. The key new
innovation is the CanEqLHS type and the new CEqCan constraint (Ct). A CanEqLHS
is either a type variable or exactly-saturated type family application; either
can now be rewritten using a CEqCan constraint in the inert set.

Because the flattener no longer reduces all type family applications to
variables, there was some performance degradation if a lengthy type family
application is now flattened over and over (not making progress). To
compensate, this patch contains some extra optimizations in the flattener,
leading to a number of performance improvements.

Close #18875.
Close #18910.

There are many extra parts of the compiler that had to be affected in writing
this patch:

* The family-application cache (formerly the flat-cache) sometimes stores
  coercions built from Given inerts. When these inerts get kicked out, we must
  kick out from the cache as well. (This was, I believe, true previously, but
  somehow never caused trouble.) Kicking out from the cache requires adding a
  filterTM function to TrieMap.

* This patch obviates the need to distinguish "blocking" coercion holes from
  non-blocking ones (which, previously, arose from CFunEqCans). There is thus
  some simplification around coercion holes.

* Extra commentary throughout parts of the code I read through, to preserve
  the knowledge I gained while working.

* A change in the pure unifier around unifying skolems with other types.
  Unifying a skolem now leads to SurelyApart, not MaybeApart, as documented
  in Note [Binding when looking up instances] in GHC.Core.InstEnv.

* Some more use of MCoercion where appropriate.

* Previously, class-instance lookup automatically noticed that e.g. C Int was
  a "unifier" to a target [W] C (F Bool), because the F Bool was flattened to
  a variable. Now, a little more care must be taken around checking for
  unifying instances.

* Previously, tcSplitTyConApp_maybe would split (Eq a => a). This is silly,
  because (=>) is not a tycon in Haskell. Fixed now, but there are some
  knock-on changes in e.g. TrieMap code and in the canonicaliser.

* New function anyFreeVarsOf{Type,Co} to check whether a free variable
  satisfies a certain predicate.

* Type synonyms now remember whether or not they are "forgetful"; a forgetful
  synonym drops at least one argument. This is useful when flattening; see
  flattenView.

* The pattern-match completeness checker invokes the solver. This invocation
  might need to look through newtypes when checking representational equality.
  Thus, the desugarer needs to keep track of the in-scope variables to know
  what newtype constructors are in scope. I bet this bug was around before but
  never noticed.

* Extra-constraints wildcards are no longer simplified before printing.
  See Note [Do not simplify ConstraintHoles] in GHC.Tc.Solver.

* Whether or not there are Given equalities has become slightly subtler.
  See the new HasGivenEqs datatype.

* Note [Type variable cycles in Givens] in GHC.Tc.Solver.Canonical
  explains a significant new wrinkle in the new approach.

* See Note [What might match later?] in GHC.Tc.Solver.Interact, which
  explains the fix to #18910.

* The inert_count field of InertCans wasn't actually used, so I removed
  it.

Though I (Richard) did the implementation, Simon PJ was very involved
in design and review.

This updates the Haddock submodule to avoid #18932 by adding
a type signature.

-------------------------
Metric Decrease:
    T12227
    T5030
    T9872a
    T9872b
    T9872c
Metric Increase:
    T9872d
-------------------------

1 files changed, 11 insertions, 6 deletions

diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 6e42b9e21e..0246426222 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -1189,6 +1189,11 @@ tc_hs_type _ rn_ty@(HsTyLit _ (HsStrTy _ s)) exp_kind
   = do { checkWiredInTyCon typeSymbolKindCon
        ; checkExpectedKind rn_ty (mkStrLitTy s) typeSymbolKind exp_kind }
 
+--------- Wildcards
+
+tc_hs_type mode ty@(HsWildCardTy _)        ek
+  = tcAnonWildCardOcc NoExtraConstraint mode ty ek
+
 --------- Potentially kind-polymorphic types: call the "up" checker
 -- See Note [Future-proofing the type checker]
 tc_hs_type mode ty@(HsTyVar {})            ek = tc_infer_hs_type_ek mode ty ek
@@ -1197,7 +1202,6 @@ tc_hs_type mode ty@(HsAppKindTy{})         ek = tc_infer_hs_type_ek mode ty ek
 tc_hs_type mode ty@(HsOpTy {})             ek = tc_infer_hs_type_ek mode ty ek
 tc_hs_type mode ty@(HsKindSig {})          ek = tc_infer_hs_type_ek mode ty ek
 tc_hs_type mode ty@(XHsType (NHsCoreTy{})) ek = tc_infer_hs_type_ek mode ty ek
-tc_hs_type mode ty@(HsWildCardTy _)        ek = tcAnonWildCardOcc mode ty ek
 
 {-
 Note [Variable Specificity and Forall Visibility]
@@ -2071,8 +2075,9 @@ newNamedWildTyVar _name   -- Currently ignoring the "_x" wildcard name used in t
        ; return tyvar }
 
 ---------------------------
-tcAnonWildCardOcc :: TcTyMode -> HsType GhcRn -> Kind -> TcM TcType
-tcAnonWildCardOcc (TcTyMode { mode_holes = Just (hole_lvl, hole_mode) })
+tcAnonWildCardOcc :: IsExtraConstraint
+                  -> TcTyMode -> HsType GhcRn -> Kind -> TcM TcType
+tcAnonWildCardOcc is_extra (TcTyMode { mode_holes = Just (hole_lvl, hole_mode) })
                   ty exp_kind
     -- hole_lvl: see Note [Checking partial type signatures]
     --           esp the bullet on nested forall types
@@ -2086,7 +2091,7 @@ tcAnonWildCardOcc (TcTyMode { mode_holes = Just (hole_lvl, hole_mode) })
 
        ; traceTc "tcAnonWildCardOcc" (ppr hole_lvl <+> ppr emit_holes)
        ; when emit_holes $
-         emitAnonTypeHole wc_tv
+         emitAnonTypeHole is_extra wc_tv
          -- Why the 'when' guard?
          -- See Note [Wildcards in visible kind application]
 
@@ -2107,7 +2112,7 @@ tcAnonWildCardOcc (TcTyMode { mode_holes = Just (hole_lvl, hole_mode) })
                      HM_FamPat  -> False
                      HM_VTA     -> False
 
-tcAnonWildCardOcc mode ty _
+tcAnonWildCardOcc _ mode ty _
 -- mode_holes is Nothing.  Should not happen, because renamer
 -- should already have rejected holes in unexpected places
   = pprPanic "tcWildCardOcc" (ppr mode $$ ppr ty)
@@ -3805,7 +3810,7 @@ tcPartialContext mode hs_theta
   | Just (hs_theta1, hs_ctxt_last) <- snocView hs_theta
   , L wc_loc ty@(HsWildCardTy _) <- ignoreParens hs_ctxt_last
   = do { wc_tv_ty <- setSrcSpan wc_loc $
-                     tcAnonWildCardOcc mode ty constraintKind
+                     tcAnonWildCardOcc YesExtraConstraint mode ty constraintKind
        ; theta <- mapM (tc_lhs_pred mode) hs_theta1
        ; return (theta, Just wc_tv_ty) }
   | otherwise