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