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

diff --git a/compiler/GHC/Data/Bag.hs b/compiler/GHC/Data/Bag.hs
index 75e7927a6b..e314309efc 100644
--- a/compiler/GHC/Data/Bag.hs
+++ b/compiler/GHC/Data/Bag.hs
@@ -17,7 +17,7 @@ module GHC.Data.Bag (
         filterBag, partitionBag, partitionBagWith,
         concatBag, catBagMaybes, foldBag,
         isEmptyBag, isSingletonBag, consBag, snocBag, anyBag, allBag,
-        listToBag, bagToList, mapAccumBagL,
+        listToBag, nonEmptyToBag, bagToList, mapAccumBagL,
         concatMapBag, concatMapBagPair, mapMaybeBag,
         mapBagM, mapBagM_,
         flatMapBagM, flatMapBagPairM,
@@ -35,6 +35,7 @@ import Control.Monad
 import Data.Data
 import Data.Maybe( mapMaybe )
 import Data.List ( partition, mapAccumL )
+import Data.List.NonEmpty ( NonEmpty(..) )
 import qualified Data.Foldable as Foldable
 
 infixr 3 `consBag`
@@ -299,6 +300,10 @@ listToBag [] = EmptyBag
 listToBag [x] = UnitBag x
 listToBag vs = ListBag vs
 
+nonEmptyToBag :: NonEmpty a -> Bag a
+nonEmptyToBag (x :| []) = UnitBag x
+nonEmptyToBag (x :| xs) = ListBag (x : xs)
+
 bagToList :: Bag a -> [a]
 bagToList b = foldr (:) [] b
 
diff --git a/compiler/GHC/Data/Maybe.hs b/compiler/GHC/Data/Maybe.hs
index 230468a20e..ac9c687b62 100644
--- a/compiler/GHC/Data/Maybe.hs
+++ b/compiler/GHC/Data/Maybe.hs
@@ -16,7 +16,7 @@ module GHC.Data.Maybe (
         failME, isSuccess,
 
         orElse,
-        firstJust, firstJusts,
+        firstJust, firstJusts, firstJustsM,
         whenIsJust,
         expectJust,
         rightToMaybe,
@@ -31,6 +31,7 @@ import Control.Monad
 import Control.Monad.Trans.Maybe
 import Control.Exception (catch, SomeException(..))
 import Data.Maybe
+import Data.Foldable ( foldlM )
 import GHC.Utils.Misc (HasCallStack)
 
 infixr 4 `orElse`
@@ -51,6 +52,15 @@ firstJust a b = firstJusts [a, b]
 firstJusts :: [Maybe a] -> Maybe a
 firstJusts = msum
 
+-- | Takes computations returnings @Maybes@; tries each one in order.
+-- The first one to return a @Just@ wins. Returns @Nothing@ if all computations
+-- return @Nothing@.
+firstJustsM :: (Monad m, Foldable f) => f (m (Maybe a)) -> m (Maybe a)
+firstJustsM = foldlM go Nothing where
+  go :: Monad m => Maybe a -> m (Maybe a) -> m (Maybe a)
+  go Nothing         action  = action
+  go result@(Just _) _action = return result
+
 expectJust :: HasCallStack => String -> Maybe a -> a
 {-# INLINE expectJust #-}
 expectJust _   (Just x) = x
diff --git a/compiler/GHC/Data/TrieMap.hs b/compiler/GHC/Data/TrieMap.hs
index 52a5b4ac78..54128d28f8 100644
--- a/compiler/GHC/Data/TrieMap.hs
+++ b/compiler/GHC/Data/TrieMap.hs
@@ -16,11 +16,11 @@ module GHC.Data.TrieMap(
    -- * Maps over 'Literal's
    LiteralMap,
    -- * 'TrieMap' class
-   TrieMap(..), insertTM, deleteTM,
+   TrieMap(..), insertTM, deleteTM, foldMapTM, isEmptyTM,
 
    -- * Things helpful for adding additional Instances.
    (>.>), (|>), (|>>), XT,
-   foldMaybe,
+   foldMaybe, filterMaybe,
    -- * Map for leaf compression
    GenMap,
    lkG, xtG, mapG, fdG,
@@ -40,6 +40,8 @@ import GHC.Utils.Outputable
 import Control.Monad( (>=>) )
 import Data.Kind( Type )
 
+import qualified Data.Semigroup as S
+
 {-
 This module implements TrieMaps, which are finite mappings
 whose key is a structured value like a CoreExpr or Type.
@@ -70,6 +72,7 @@ class TrieMap m where
    lookupTM :: forall b. Key m -> m b -> Maybe b
    alterTM  :: forall b. Key m -> XT b -> m b -> m b
    mapTM    :: (a->b) -> m a -> m b
+   filterTM :: (a -> Bool) -> m a -> m a
 
    foldTM   :: (a -> b -> b) -> m a -> b -> b
       -- The unusual argument order here makes
@@ -82,6 +85,13 @@ insertTM k v m = alterTM k (\_ -> Just v) m
 deleteTM :: TrieMap m => Key m -> m a -> m a
 deleteTM k m = alterTM k (\_ -> Nothing) m
 
+foldMapTM :: (TrieMap m, Monoid r) => (a -> r) -> m a -> r
+foldMapTM f m = foldTM (\ x r -> f x S.<> r) m mempty
+
+-- This looks inefficient.
+isEmptyTM :: TrieMap m => m a -> Bool
+isEmptyTM m = foldTM (\ _ _ -> False) m True
+
 ----------------------
 -- Recall that
 --   Control.Monad.(>=>) :: (a -> Maybe b) -> (b -> Maybe c) -> a -> Maybe c
@@ -121,6 +131,7 @@ instance TrieMap IntMap.IntMap where
   alterTM = xtInt
   foldTM k m z = IntMap.foldr k z m
   mapTM f m = IntMap.map f m
+  filterTM f m = IntMap.filter f m
 
 xtInt :: Int -> XT a -> IntMap.IntMap a -> IntMap.IntMap a
 xtInt k f m = IntMap.alter f k m
@@ -132,6 +143,7 @@ instance Ord k => TrieMap (Map.Map k) where
   alterTM k f m = Map.alter f k m
   foldTM k m z = Map.foldr k z m
   mapTM f m = Map.map f m
+  filterTM f m = Map.filter f m
 
 
 {-
@@ -208,6 +220,7 @@ instance forall key. Uniquable key => TrieMap (UniqDFM key) where
   alterTM k f m = alterUDFM f m k
   foldTM k m z = foldUDFM k z m
   mapTM f m = mapUDFM f m
+  filterTM f m = filterUDFM f m
 
 {-
 ************************************************************************
@@ -229,6 +242,10 @@ instance TrieMap m => TrieMap (MaybeMap m) where
    alterTM  = xtMaybe alterTM
    foldTM   = fdMaybe
    mapTM    = mapMb
+   filterTM = ftMaybe
+
+instance TrieMap m => Foldable (MaybeMap m) where
+  foldMap = foldMapTM
 
 mapMb :: TrieMap m => (a->b) -> MaybeMap m a -> MaybeMap m b
 mapMb f (MM { mm_nothing = mn, mm_just = mj })
@@ -248,6 +265,19 @@ fdMaybe :: TrieMap m => (a -> b -> b) -> MaybeMap m a -> b -> b
 fdMaybe k m = foldMaybe k (mm_nothing m)
             . foldTM k (mm_just m)
 
+ftMaybe :: TrieMap m => (a -> Bool) -> MaybeMap m a -> MaybeMap m a
+ftMaybe f (MM { mm_nothing = mn, mm_just = mj })
+  = MM { mm_nothing = filterMaybe f mn, mm_just = filterTM f mj }
+
+foldMaybe :: (a -> b -> b) -> Maybe a -> b -> b
+foldMaybe _ Nothing  b = b
+foldMaybe k (Just a) b = k a b
+
+filterMaybe :: (a -> Bool) -> Maybe a -> Maybe a
+filterMaybe _ Nothing = Nothing
+filterMaybe f input@(Just x) | f x       = input
+                             | otherwise = Nothing
+
 {-
 ************************************************************************
 *                                                                      *
@@ -267,6 +297,10 @@ instance TrieMap m => TrieMap (ListMap m) where
    alterTM  = xtList alterTM
    foldTM   = fdList
    mapTM    = mapList
+   filterTM = ftList
+
+instance TrieMap m => Foldable (ListMap m) where
+  foldMap = foldMapTM
 
 instance (TrieMap m, Outputable a) => Outputable (ListMap m a) where
   ppr m = text "List elts" <+> ppr (foldTM (:) m [])
@@ -290,9 +324,9 @@ fdList :: forall m a b. TrieMap m
 fdList k m = foldMaybe k          (lm_nil m)
            . foldTM    (fdList k) (lm_cons m)
 
-foldMaybe :: (a -> b -> b) -> Maybe a -> b -> b
-foldMaybe _ Nothing  b = b
-foldMaybe k (Just a) b = k a b
+ftList :: TrieMap m => (a -> Bool) -> ListMap m a -> ListMap m a
+ftList f (LM { lm_nil = mnil, lm_cons = mcons })
+  = LM { lm_nil = filterMaybe f mnil, lm_cons = mapTM (filterTM f) mcons }
 
 {-
 ************************************************************************
@@ -354,6 +388,10 @@ instance (Eq (Key m), TrieMap m) => TrieMap (GenMap m) where
    alterTM  = xtG
    foldTM   = fdG
    mapTM    = mapG
+   filterTM = ftG
+
+instance (Eq (Key m), TrieMap m) => Foldable (GenMap m) where
+  foldMap = foldMapTM
 
 --We want to be able to specialize these functions when defining eg
 --tries over (GenMap CoreExpr) which requires INLINEABLE
@@ -403,3 +441,13 @@ fdG :: TrieMap m => (a -> b -> b) -> GenMap m a -> b -> b
 fdG _ EmptyMap = \z -> z
 fdG k (SingletonMap _ v) = \z -> k v z
 fdG k (MultiMap m) = foldTM k m
+
+{-# INLINEABLE ftG #-}
+ftG :: TrieMap m => (a -> Bool) -> GenMap m a -> GenMap m a
+ftG _ EmptyMap = EmptyMap
+ftG f input@(SingletonMap _ v)
+  | f v       = input
+  | otherwise = EmptyMap
+ftG f (MultiMap m) = MultiMap (filterTM f m)
+  -- we don't have enough information to reconstruct the key to make
+  -- a SingletonMap