{-# 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.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