    {-# LANGUAGE DerivingStrategies #-}
    {-# LANGUAGE GADTs #-}

    -- | Utility types used within the constraint solver
    module GHC.Tc.Solver.Types (
        -- Inert CDictCans
        DictMap, emptyDictMap,
        findDictsByTyConKey, findDictsByClass,
        foldDicts, findDict,
        dictsToBag,

        FunEqMap, emptyFunEqs, findFunEq, insertFunEq,
        findFunEqsByTyCon,

        TcAppMap, emptyTcAppMap, isEmptyTcAppMap,
        insertTcApp, alterTcApp, filterTcAppMap,
        tcAppMapToBag, foldTcAppMap, delTcApp,

        EqualCtList, filterEqualCtList, addToEqualCtList

      ) where

    import GHC.Prelude

    import GHC.Tc.Types.Constraint
    import GHC.Tc.Types.Origin
    import GHC.Tc.Types.CtLoc( CtLoc, ctLocOrigin )
    import GHC.Tc.Utils.TcType

    import GHC.Types.Unique
    import GHC.Types.Unique.DFM

    import GHC.Core.Class
    import GHC.Core.Map.Type
    import GHC.Core.Predicate
    import GHC.Core.TyCon
    import GHC.Core.TyCon.Env

    import GHC.Data.Bag
    import GHC.Data.Maybe
    import GHC.Data.TrieMap
    import GHC.Utils.Constants
    import GHC.Utils.Outputable
    import GHC.Utils.Panic

    {- *********************************************************************
    *                                                                      *
                       TcAppMap
    *                                                                      *
    ************************************************************************

    Note [Use loose types in inert set]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Whenever we are looking up an inert dictionary (CDictCan) or function
    equality (CEqCan), we use a TcAppMap, which uses the Unique of the
    class/type family tycon and then a trie which maps the arguments. This
    trie does *not* need to match the kinds of the arguments; this Note
    explains why.

    Consider the types ty0 = (T ty1 ty2 ty3 ty4) and ty0' = (T ty1' ty2' ty3' ty4'),
    where ty4 and ty4' have different kinds. Let's further assume that both types
    ty0 and ty0' are well-typed. Because the kind of T is closed, it must be that
    one of the ty1..ty3 does not match ty1'..ty3' (and that the kind of the fourth
    argument to T is dependent on whichever one changed). Since we are matching
    all arguments, during the inert-set lookup, we know that ty1..ty3 do indeed
    match ty1'..ty3'. Therefore, the kind of ty4 and ty4' must match, too --
    without ever looking at it.

    Accordingly, we use LooseTypeMap, which skips the kind check when looking
    up a type. I (Richard E) believe this is just an optimization, and that
    looking at kinds would be harmless.

    -}

    type TcAppMap a = DTyConEnv (ListMap LooseTypeMap a)
        -- Indexed by tycon then the arg types, using "loose" matching, where
        -- we don't require kind equality. This allows, for example, (a |> co)
        -- to match (a).
        -- See Note [Use loose types in inert set]
        -- Used for types and classes; hence UniqDFM
        -- See Note [foldTM determinism] in GHC.Data.TrieMap for why we use DTyConEnv here

    isEmptyTcAppMap :: TcAppMap a -> Bool
    isEmptyTcAppMap :: forall a. TcAppMap a -> Bool
    isEmptyTcAppMap TcAppMap a
    m = TcAppMap a -> Bool
    forall a. DTyConEnv a -> Bool
    isEmptyDTyConEnv TcAppMap a
    m

    emptyTcAppMap :: TcAppMap a
    emptyTcAppMap :: forall a. TcAppMap a
    emptyTcAppMap = DTyConEnv (ListMap LooseTypeMap a)
    forall a. DTyConEnv a
    emptyDTyConEnv

    findTcApp :: TcAppMap a -> TyCon -> [Type] -> Maybe a
    findTcApp :: forall a. TcAppMap a -> TyCon -> [Type] -> Maybe a
    findTcApp TcAppMap a
    m TyCon
    tc [Type]
    tys = do { tys_map <- TcAppMap a -> TyCon -> Maybe (ListMap LooseTypeMap a)
    forall a. DTyConEnv a -> TyCon -> Maybe a
    lookupDTyConEnv TcAppMap a
    m TyCon
    tc
                            ; lookupTM tys tys_map }

    delTcApp :: TcAppMap a -> TyCon -> [Type] -> TcAppMap a
    delTcApp :: forall a. TcAppMap a -> TyCon -> [Type] -> TcAppMap a
    delTcApp TcAppMap a
    m TyCon
    tc [Type]
    tys = (ListMap LooseTypeMap a -> ListMap LooseTypeMap a)
    -> TcAppMap a -> TyCon -> TcAppMap a
    forall a. (a -> a) -> DTyConEnv a -> TyCon -> DTyConEnv a
    adjustDTyConEnv (Key (ListMap LooseTypeMap)
    -> ListMap LooseTypeMap a -> ListMap LooseTypeMap a
    forall (m :: * -> *) a. TrieMap m => Key m -> m a -> m a
    deleteTM [Type]
    Key (ListMap LooseTypeMap)
    tys) TcAppMap a
    m TyCon
    tc

    insertTcApp :: TcAppMap a -> TyCon -> [Type] -> a -> TcAppMap a
    insertTcApp :: forall a. TcAppMap a -> TyCon -> [Type] -> a -> TcAppMap a
    insertTcApp TcAppMap a
    m TyCon
    tc [Type]
    tys a
    ct = (Maybe (ListMap LooseTypeMap a) -> Maybe (ListMap LooseTypeMap a))
    -> TcAppMap a -> TyCon -> TcAppMap a
    forall a.
    (Maybe a -> Maybe a) -> DTyConEnv a -> TyCon -> DTyConEnv a
    alterDTyConEnv Maybe (ListMap LooseTypeMap a) -> Maybe (ListMap LooseTypeMap a)
    alter_tm TcAppMap a
    m TyCon
    tc
      where
        alter_tm :: Maybe (ListMap LooseTypeMap a) -> Maybe (ListMap LooseTypeMap a)
    alter_tm Maybe (ListMap LooseTypeMap a)
    mb_tm = ListMap LooseTypeMap a -> Maybe (ListMap LooseTypeMap a)
    forall a. a -> Maybe a
    Just (Key (ListMap LooseTypeMap)
    -> a -> ListMap LooseTypeMap a -> ListMap LooseTypeMap a
    forall (m :: * -> *) a. TrieMap m => Key m -> a -> m a -> m a
    insertTM [Type]
    Key (ListMap LooseTypeMap)
    tys a
    ct (Maybe (ListMap LooseTypeMap a)
    mb_tm Maybe (ListMap LooseTypeMap a)
    -> ListMap LooseTypeMap a -> ListMap LooseTypeMap a
    forall a. Maybe a -> a -> a
    `orElse` ListMap LooseTypeMap a
    forall a. ListMap LooseTypeMap a
    forall (m :: * -> *) a. TrieMap m => m a
    emptyTM))

    alterTcApp :: forall a. TcAppMap a -> TyCon -> [Type] -> XT a -> TcAppMap a
    alterTcApp :: forall a. TcAppMap a -> TyCon -> [Type] -> XT a -> TcAppMap a
    alterTcApp TcAppMap a
    m TyCon
    tc [Type]
    tys XT a
    upd = (Maybe (ListMap LooseTypeMap a) -> Maybe (ListMap LooseTypeMap a))
    -> TcAppMap a -> TyCon -> TcAppMap a
    forall a.
    (Maybe a -> Maybe a) -> DTyConEnv a -> TyCon -> DTyConEnv a
    alterDTyConEnv Maybe (ListMap LooseTypeMap a) -> Maybe (ListMap LooseTypeMap a)
    alter_tm TcAppMap a
    m TyCon
    tc
      where
        alter_tm :: Maybe (ListMap LooseTypeMap a) -> Maybe (ListMap LooseTypeMap a)
        alter_tm :: Maybe (ListMap LooseTypeMap a) -> Maybe (ListMap LooseTypeMap a)
    alter_tm Maybe (ListMap LooseTypeMap a)
    m_elt = ListMap LooseTypeMap a -> Maybe (ListMap LooseTypeMap a)
    forall a. a -> Maybe a
    Just (Key (ListMap LooseTypeMap)
    -> XT a -> ListMap LooseTypeMap a -> ListMap LooseTypeMap a
    forall b.
    Key (ListMap LooseTypeMap)
    -> XT b -> ListMap LooseTypeMap b -> ListMap LooseTypeMap b
    forall (m :: * -> *) b. TrieMap m => Key m -> XT b -> m b -> m b
    alterTM [Type]
    Key (ListMap LooseTypeMap)
    tys XT a
    upd (Maybe (ListMap LooseTypeMap a)
    m_elt Maybe (ListMap LooseTypeMap a)
    -> ListMap LooseTypeMap a -> ListMap LooseTypeMap a
    forall a. Maybe a -> a -> a
    `orElse` ListMap LooseTypeMap a
    forall a. ListMap LooseTypeMap a
    forall (m :: * -> *) a. TrieMap m => m a
    emptyTM))

    filterTcAppMap :: forall a. (a -> Bool) -> TcAppMap a -> TcAppMap a
    filterTcAppMap :: forall a. (a -> Bool) -> TcAppMap a -> TcAppMap a
    filterTcAppMap a -> Bool
    f TcAppMap a
    m = (ListMap LooseTypeMap a -> Maybe (ListMap LooseTypeMap a))
    -> TcAppMap a -> TcAppMap a
    forall a b. (a -> Maybe b) -> DTyConEnv a -> DTyConEnv b
    mapMaybeDTyConEnv ListMap LooseTypeMap a -> Maybe (ListMap LooseTypeMap a)
    one_tycon TcAppMap a
    m
      where
        one_tycon :: ListMap LooseTypeMap a -> Maybe (ListMap LooseTypeMap a)
        one_tycon :: ListMap LooseTypeMap a -> Maybe (ListMap LooseTypeMap a)
    one_tycon ListMap LooseTypeMap a
    tm
          | ListMap LooseTypeMap a -> Bool
    forall (m :: * -> *) a. TrieMap m => m a -> Bool
    isEmptyTM ListMap LooseTypeMap a
    filtered_tm = Maybe (ListMap LooseTypeMap a)
    forall a. Maybe a
    Nothing
          | Bool
    otherwise             = ListMap LooseTypeMap a -> Maybe (ListMap LooseTypeMap a)
    forall a. a -> Maybe a
    Just ListMap LooseTypeMap a
    filtered_tm
          where
            filtered_tm :: ListMap LooseTypeMap a
    filtered_tm = (a -> Bool) -> ListMap LooseTypeMap a -> ListMap LooseTypeMap a
    forall a.
    (a -> Bool) -> ListMap LooseTypeMap a -> ListMap LooseTypeMap a
    forall (m :: * -> *) a. TrieMap m => (a -> Bool) -> m a -> m a
    filterTM a -> Bool
    f ListMap LooseTypeMap a
    tm

    tcAppMapToBag :: TcAppMap a -> Bag a
    tcAppMapToBag :: forall a. TcAppMap a -> Bag a
    tcAppMapToBag TcAppMap a
    m = (a -> Bag a -> Bag a) -> TcAppMap a -> Bag a -> Bag a
    forall a b. (a -> b -> b) -> TcAppMap a -> b -> b
    foldTcAppMap a -> Bag a -> Bag a
    forall a. a -> Bag a -> Bag a
    consBag TcAppMap a
    m Bag a
    forall a. Bag a
    emptyBag

    foldTcAppMap :: (a -> b -> b) -> TcAppMap a -> b -> b
    foldTcAppMap :: forall a b. (a -> b -> b) -> TcAppMap a -> b -> b
    foldTcAppMap a -> b -> b
    k TcAppMap a
    m b
    z = (ListMap LooseTypeMap a -> b -> b) -> b -> TcAppMap a -> b
    forall elt a. (elt -> a -> a) -> a -> DTyConEnv elt -> a
    foldDTyConEnv ((a -> b -> b) -> ListMap LooseTypeMap a -> b -> b
    forall a b. (a -> b -> b) -> ListMap LooseTypeMap a -> b -> b
    forall (m :: * -> *) a b.
    TrieMap m =>
    (a -> b -> b) -> m a -> b -> b
    foldTM a -> b -> b
    k) b
    z TcAppMap a
    m

    {- *********************************************************************
    *                                                                      *
                       DictMap
    *                                                                      *
    ********************************************************************* -}

    type DictMap a = TcAppMap a

    emptyDictMap :: DictMap a
    emptyDictMap :: forall a. TcAppMap a
    emptyDictMap = TcAppMap a
    forall a. TcAppMap a
    emptyTcAppMap

    findDict :: DictMap a -> CtLoc -> Class -> [Type] -> Maybe a
    findDict :: forall a. DictMap a -> CtLoc -> Class -> [Type] -> Maybe a
    findDict DictMap a
    m CtLoc
    loc Class
    cls [Type]
    tys
      | Just {} <- Class -> [Type] -> Maybe FastString
    isCallStackPred Class
    cls [Type]
    tys
      , CtOrigin -> Bool
    isPushCallStackOrigin (CtLoc -> CtOrigin
    ctLocOrigin CtLoc
    loc)
      = Maybe a
    forall a. Maybe a
    Nothing             -- See Note [Solving CallStack constraints]

      | Bool
    otherwise
      = DictMap a -> TyCon -> [Type] -> Maybe a
    forall a. TcAppMap a -> TyCon -> [Type] -> Maybe a
    findTcApp DictMap a
    m (Class -> TyCon
    classTyCon Class
    cls) [Type]
    tys

    findDictsByClass :: DictMap a -> Class -> Bag a
    findDictsByClass :: forall a. DictMap a -> Class -> Bag a
    findDictsByClass DictMap a
    m Class
    cls = DictMap a -> Unique -> Bag a
    forall a. DictMap a -> Unique -> Bag a
    findDictsByTyConKey DictMap a
    m (TyCon -> Unique
    forall a. Uniquable a => a -> Unique
    getUnique (TyCon -> Unique) -> TyCon -> Unique
    forall a b. (a -> b) -> a -> b
    $ Class -> TyCon
    classTyCon Class
    cls)

    findDictsByTyConKey :: DictMap a -> Unique -> Bag a
    findDictsByTyConKey :: forall a. DictMap a -> Unique -> Bag a
    findDictsByTyConKey DictMap a
    m Unique
    tc
      | Just ListMap LooseTypeMap a
    tm <- DictMap a -> Unique -> Maybe (ListMap LooseTypeMap a)
    forall {k} (key :: k) elt. UniqDFM key elt -> Unique -> Maybe elt
    lookupUDFM_Directly DictMap a
    m Unique
    tc = (a -> Bag a -> Bag a) -> ListMap LooseTypeMap a -> Bag a -> Bag a
    forall a b. (a -> b -> b) -> ListMap LooseTypeMap a -> b -> b
    forall (m :: * -> *) a b.
    TrieMap m =>
    (a -> b -> b) -> m a -> b -> b
    foldTM a -> Bag a -> Bag a
    forall a. a -> Bag a -> Bag a
    consBag ListMap LooseTypeMap a
    tm Bag a
    forall a. Bag a
    emptyBag
      | Bool
    otherwise                           = Bag a
    forall a. Bag a
    emptyBag

    dictsToBag :: DictMap a -> Bag a
    dictsToBag :: forall a. TcAppMap a -> Bag a
    dictsToBag = TcAppMap a -> Bag a
    forall a. TcAppMap a -> Bag a
    tcAppMapToBag

    foldDicts :: (a -> b -> b) -> DictMap a -> b -> b
    foldDicts :: forall a b. (a -> b -> b) -> TcAppMap a -> b -> b
    foldDicts = (a -> b -> b) -> TcAppMap a -> b -> b
    forall a b. (a -> b -> b) -> TcAppMap a -> b -> b
    foldTcAppMap

    {- Note [Solving CallStack constraints]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    See also Note [Overview of implicit CallStacks] in GHc.Tc.Types.Evidence.

    Suppose f :: HasCallStack => blah.  Then

    * Each call to 'f' gives rise to
        [W] s1 :: IP "callStack" CallStack    -- CtOrigin = OccurrenceOf f
      with a CtOrigin that says "OccurrenceOf f".
      Remember that HasCallStack is just shorthand for
        IP "callStack" CallStack
      See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence

    * We cannonicalise such constraints, in GHC.Tc.Solver.Dict.canDictNC, by
      pushing the call-site info on the stack, and changing the CtOrigin
      to record that has been done.
       Bind:  s1 = pushCallStack <site-info> s2
       [W] s2 :: IP "callStack" CallStack   -- CtOrigin = IPOccOrigin

    * Then, and only then, we can solve the constraint from an enclosing
      Given.

    So we must be careful /not/ to solve 's1' from the Givens.  Again,
    we ensure this by arranging that findDict always misses when looking
    up such constraints.
    -}

    {- *********************************************************************
    *                                                                      *
                       FunEqMap
    *                                                                      *
    ********************************************************************* -}

    type FunEqMap a = TcAppMap a  -- A map whose key is a (TyCon, [Type]) pair

    emptyFunEqs :: TcAppMap a
    emptyFunEqs :: forall a. TcAppMap a
    emptyFunEqs = TcAppMap a
    forall a. TcAppMap a
    emptyTcAppMap

    findFunEq :: FunEqMap a -> TyCon -> [Type] -> Maybe a
    findFunEq :: forall a. TcAppMap a -> TyCon -> [Type] -> Maybe a
    findFunEq FunEqMap a
    m TyCon
    tc [Type]
    tys = FunEqMap a -> TyCon -> [Type] -> Maybe a
    forall a. TcAppMap a -> TyCon -> [Type] -> Maybe a
    findTcApp FunEqMap a
    m TyCon
    tc [Type]
    tys

    findFunEqsByTyCon :: FunEqMap a -> TyCon -> [a]
    -- Get inert function equation constraints that have the given tycon
    -- in their head.  Not that the constraints remain in the inert set.
    -- We use this to check for wanted interactions with built-in type-function
    -- constructors.
    findFunEqsByTyCon :: forall a. FunEqMap a -> TyCon -> [a]
    findFunEqsByTyCon FunEqMap a
    m TyCon
    tc
      | Just ListMap LooseTypeMap a
    tm <- FunEqMap a -> TyCon -> Maybe (ListMap LooseTypeMap a)
    forall a. DTyConEnv a -> TyCon -> Maybe a
    lookupDTyConEnv FunEqMap a
    m TyCon
    tc = (a -> [a] -> [a]) -> ListMap LooseTypeMap a -> [a] -> [a]
    forall a b. (a -> b -> b) -> ListMap LooseTypeMap a -> b -> b
    forall (m :: * -> *) a b.
    TrieMap m =>
    (a -> b -> b) -> m a -> b -> b
    foldTM (:) ListMap LooseTypeMap a
    tm []
      | Bool
    otherwise                       = []

    insertFunEq :: FunEqMap a -> TyCon -> [Type] -> a -> FunEqMap a
    insertFunEq :: forall a. TcAppMap a -> TyCon -> [Type] -> a -> TcAppMap a
    insertFunEq FunEqMap a
    m TyCon
    tc [Type]
    tys a
    val = FunEqMap a -> TyCon -> [Type] -> a -> FunEqMap a
    forall a. TcAppMap a -> TyCon -> [Type] -> a -> TcAppMap a
    insertTcApp FunEqMap a
    m TyCon
    tc [Type]
    tys a
    val

    {- *********************************************************************
    *                                                                      *
                       EqualCtList
    *                                                                      *
    ********************************************************************* -}

    {-
    Note [EqualCtList invariants]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
        * All are equalities
        * All these equalities have the same LHS
        * No element of the list can rewrite any other

    Accordingly, this list is either empty, contains one element, or
    contains a Given representational equality and a Wanted nominal one.
    -}

    type EqualCtList = [EqCt]
      -- See Note [EqualCtList invariants]

    addToEqualCtList :: EqCt -> EqualCtList -> EqualCtList
    -- See Note [EqualCtList invariants]
    addToEqualCtList :: EqCt -> [EqCt] -> [EqCt]
    addToEqualCtList EqCt
    ct [EqCt]
    old_eqs
      | Bool
    debugIsOn
      = case EqCt
    ct of
          EqCt { eq_lhs :: EqCt -> CanEqLHS
    eq_lhs = TyVarLHS TcTyVar
    tv } ->
            Bool -> [EqCt] -> [EqCt]
    forall a. HasCallStack => Bool -> a -> a
    assert ((EqCt -> Bool) -> [EqCt] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (TcTyVar -> EqCt -> Bool
    shares_lhs TcTyVar
    tv) [EqCt]
    old_eqs) ([EqCt] -> [EqCt]) -> [EqCt] -> [EqCt]
    forall a b. (a -> b) -> a -> b
    $
            Bool -> SDoc -> [EqCt] -> [EqCt]
    forall a. HasCallStack => Bool -> SDoc -> a -> a
    assertPpr ([(EqCt, EqCt)] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(EqCt, EqCt)]
    bad_prs)
                      ([SDoc] -> SDoc
    forall doc. IsDoc doc => [doc] -> doc
    vcat [ String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "bad_prs" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> [(EqCt, EqCt)] -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr [(EqCt, EqCt)]
    bad_prs
                            , String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "ct:old_eqs" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> [EqCt] -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (EqCt
    ct EqCt -> [EqCt] -> [EqCt]
    forall a. a -> [a] -> [a]
    : [EqCt]
    old_eqs) ]) ([EqCt] -> [EqCt]) -> [EqCt] -> [EqCt]
    forall a b. (a -> b) -> a -> b
    $
            (EqCt
    ct EqCt -> [EqCt] -> [EqCt]
    forall a. a -> [a] -> [a]
    : [EqCt]
    old_eqs)

          EqCt
    _ -> String -> SDoc -> [EqCt]
    forall a. HasCallStack => String -> SDoc -> a
    pprPanic String
    "addToEqualCtList not CEqCan" (EqCt -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr EqCt
    ct)

      | Bool
    otherwise
      = EqCt
    ct EqCt -> [EqCt] -> [EqCt]
    forall a. a -> [a] -> [a]
    : [EqCt]
    old_eqs
      where
        shares_lhs :: TcTyVar -> EqCt -> Bool
    shares_lhs TcTyVar
    tv (EqCt { eq_lhs :: EqCt -> CanEqLHS
    eq_lhs = TyVarLHS TcTyVar
    old_tv }) = TcTyVar
    tv TcTyVar -> TcTyVar -> Bool
    forall a. Eq a => a -> a -> Bool
    == TcTyVar
    old_tv
        shares_lhs TcTyVar
    _ EqCt
    _ = Bool
    False
        bad_prs :: [(EqCt, EqCt)]
    bad_prs = ((EqCt, EqCt) -> Bool) -> [(EqCt, EqCt)] -> [(EqCt, EqCt)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (EqCt, EqCt) -> Bool
    is_bad_pair ([EqCt] -> [(EqCt, EqCt)]
    forall a. [a] -> [(a, a)]
    distinctPairs (EqCt
    ct EqCt -> [EqCt] -> [EqCt]
    forall a. a -> [a] -> [a]
    : [EqCt]
    old_eqs))
        is_bad_pair :: (EqCt, EqCt) -> Bool
        is_bad_pair :: (EqCt, EqCt) -> Bool
    is_bad_pair (EqCt
    ct1,EqCt
    ct2) = EqCt -> CtFlavourRole
    eqCtFlavourRole EqCt
    ct1 CtFlavourRole -> CtFlavourRole -> Bool
    `eqCanRewriteFR` EqCt -> CtFlavourRole
    eqCtFlavourRole EqCt
    ct2

    distinctPairs :: [a] -> [(a,a)]
    -- distinctPairs [x1,...xn] is the list of all pairs [ ...(xi, xj)...]
    --                             where i /= j
    -- NB: does not return pairs (xi,xi), which would be stupid in the
    --     context of addToEqualCtList (#22645)
    distinctPairs :: forall a. [a] -> [(a, a)]
    distinctPairs []     = []
    distinctPairs (a
    x:[a]
    xs) = (a -> [(a, a)]) -> [a] -> [(a, a)]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (\a
    y -> [(a
    x,a
    y),(a
    y,a
    x)]) [a]
    xs [(a, a)] -> [(a, a)] -> [(a, a)]
    forall a. [a] -> [a] -> [a]
    ++ [a] -> [(a, a)]
    forall a. [a] -> [(a, a)]
    distinctPairs [a]
    xs

    -- returns Nothing when the new list is empty, to keep the environments smaller
    filterEqualCtList :: (EqCt -> Bool) -> EqualCtList -> Maybe EqualCtList
    filterEqualCtList :: (EqCt -> Bool) -> [EqCt] -> Maybe [EqCt]
    filterEqualCtList EqCt -> Bool
    pred [EqCt]
    cts
      | [EqCt] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [EqCt]
    new_list
      = Maybe [EqCt]
    forall a. Maybe a
    Nothing
      | Bool
    otherwise
      = [EqCt] -> Maybe [EqCt]
    forall a. a -> Maybe a
    Just [EqCt]
    new_list
      where
        new_list :: [EqCt]
    new_list = (EqCt -> Bool) -> [EqCt] -> [EqCt]
    forall a. (a -> Bool) -> [a] -> [a]
    filter EqCt -> Bool
    pred [EqCt]
    cts