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
-------------------------

3 files changed, 49 insertions, 1 deletions

diff --git a/docs/users_guide/9.2.1-notes.rst b/docs/users_guide/9.2.1-notes.rst
index da0461f982..30a58175f4 100644
--- a/docs/users_guide/9.2.1-notes.rst
+++ b/docs/users_guide/9.2.1-notes.rst
@@ -44,6 +44,10 @@ Compiler
   that the compiler automatically insert cost-centres on all call-sites of
   the named function.
 
+- There is a significant refactoring in the solver; any type-checker plugins
+  will have to be updated, as GHC no longer uses flattening skolems or
+  flattening metavariables.
+  
 ``ghc-prim`` library
 ~~~~~~~~~~~~~~~~~~~~
 
diff --git a/docs/users_guide/expected-undocumented-flags.txt b/docs/users_guide/expected-undocumented-flags.txt
index 23b5a4abe7..75a433189c 100644
--- a/docs/users_guide/expected-undocumented-flags.txt
+++ b/docs/users_guide/expected-undocumented-flags.txt
@@ -57,7 +57,6 @@
 -fextended-default-rules
 -fffi
 -ffi
--fflat-cache
 -ffloat-all-lams
 -ffloat-lam-args
 -ffrontend-opt
diff --git a/docs/users_guide/exts/type_families.rst b/docs/users_guide/exts/type_families.rst
index 3c09e63a14..4843e35a80 100644
--- a/docs/users_guide/exts/type_families.rst
+++ b/docs/users_guide/exts/type_families.rst
@@ -581,6 +581,51 @@ If the option :extension:`UndecidableInstances` is passed to the compiler, the
 above restrictions are not enforced and it is on the programmer to ensure
 termination of the normalisation of type families during type inference.
 
+Reducing type family applications
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. ghc-flag:: -ffamily-application-cache
+    :shortdesc: Use a cache when reducing type family applications
+    :type: dynamic
+    :reverse: -fno-family-application-cache
+    :category:
+
+    The flag :ghc-flag:`-ffamily-application-cache` (on by default) instructs
+    GHC to use a cache when reducing type family applications. In most cases,
+    this will speed up compilation. The use of this flag will not affect
+    runtime behaviour.
+
+When GHC encounters a type family application (like ``F Int a``) in a program,
+it must often reduce it in order to complete type checking. Here is a simple
+example::
+
+  type family F a where
+    F Int            = Bool
+    F (Maybe Double) = Char
+
+  g :: F Int -> Bool
+  g = not
+
+Despite the fact that ``g``\'s type mentions ``F Int``, GHC must recognize that
+``g``\'s argument really has type ``Bool``. This is done by *reducing* ``F Int``
+to become ``Bool``. Sometimes, there is not enough information to reduce a type
+family application; we say such an application is *stuck*. Continuing this example,
+an occurrence of ``F (Maybe a)`` (for some type variable ``a``) would be stuck, as
+no equation applies.
+
+During type checking, GHC uses heuristics to determine which type family application
+to reduce next; there is no predictable ordering among different type family applications.
+The non-determinism rarely matters in practice. In most programs, type family reduction
+terminates, and so these choices are immaterial. However, if a type family application
+does not terminate, it is possible that type-checking may unpredictably diverge. (GHC
+will always take the same path for a given source program, but small changes in that
+source program may induce GHC to take a different path. Compiling a given, unchanged
+source program is still deterministic.)
+
+In order to speed up type family reduction, GHC normally uses a cache, remembering what
+type family applications it has previously reduced. This feature can be disabled with
+:ghc-flag:`-fno-family-application-cache`.
+
 .. _type-wildcards-lhs:
 
 Wildcards on the LHS of data and type family instances