    {-# LANGUAGE LambdaCase          #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE ViewPatterns        #-}

    {-
    Authors: George Karachalias <george.karachalias@cs.kuleuven.be>
             Sebastian Graf <sgraf1337@gmail.com>
             Ryan Scott <ryan.gl.scott@gmail.com>
    -}

    -- | Model refinements type as per the
    -- [Lower Your Guards paper](https://dl.acm.org/doi/abs/10.1145/3408989).
    -- The main export of the module are the functions 'addPhiCtsNablas' for adding
    -- facts to the oracle, 'isInhabited' to check if a refinement type is inhabited
    -- and 'generateInhabitingPatterns' to turn a 'Nabla' into a concrete pattern
    -- for an equation.
    --
    -- In terms of the LYG paper, this module is concerned with Sections 3.4, 3.6
    -- and 3.7. E.g., it represents refinement types directly as a bunch of
    -- normalised refinement types 'Nabla'.

    module GHC.HsToCore.Pmc.Solver (

            Nabla, Nablas(..), initNablas,

            PhiCt(..), PhiCts,
            addPhiCtNablas,
            addPhiCtsNablas,

            isInhabited,
            generateInhabitingPatterns, GenerateInhabitingPatternsMode(..)

        ) where

    import GHC.Prelude

    import GHC.HsToCore.Pmc.Types
    import GHC.HsToCore.Pmc.Utils (tracePm, traceWhenFailPm, mkPmId)

    import GHC.Driver.DynFlags
    import GHC.Driver.Config
    import GHC.Utils.Outputable
    import GHC.Utils.Misc
    import GHC.Utils.Monad (allM)
    import GHC.Utils.Panic
    import GHC.Data.Bag

    import GHC.Types.CompleteMatch
    import GHC.Types.Unique.Set
    import GHC.Types.Unique.DSet
    import GHC.Types.Unique.SDFM
    import GHC.Types.Id
    import GHC.Types.Name
    import GHC.Types.Var      (EvVar)
    import GHC.Types.Var.Env
    import GHC.Types.Var.Set
    import GHC.Types.Unique.Supply

    import GHC.Core
    import GHC.Core.FVs         (exprFreeVars)
    import GHC.Core.TyCo.Compare( eqType )
    import GHC.Core.Map.Expr
    import GHC.Core.Predicate (typeDeterminesValue)
    import GHC.Core.SimpleOpt (simpleOptExpr, exprIsConApp_maybe)
    import GHC.Core.Utils     (exprType)
    import GHC.Core.Make      (mkListExpr, mkCharExpr, mkImpossibleExpr)

    import GHC.Data.FastString
    import GHC.Types.SrcLoc
    import GHC.Data.Maybe
    import GHC.Core.ConLike
    import GHC.Core.DataCon
    import GHC.Core.PatSyn
    import GHC.Core.TyCon
    import GHC.Core.TyCon.RecWalk
    import GHC.Builtin.Names
    import GHC.Builtin.Types
    import GHC.Core.TyCo.Rep
    import GHC.Core.TyCo.Subst (elemSubst)
    import GHC.Core.Type
    import GHC.Tc.Solver   (tcNormalise, tcCheckGivens, tcCheckWanteds)
    import GHC.Core.Unify    (tcMatchTy)
    import GHC.Core.Coercion
    import GHC.Core.Reduction
    import GHC.HsToCore.Monad hiding (foldlM)
    import GHC.Tc.Instance.Family
    import GHC.Core.FamInstEnv

    import Control.Applicative ((<|>))
    import Control.Monad (foldM, forM, guard, mzero, when, filterM)
    import Control.Monad.Trans.Class (lift)
    import Control.Monad.Trans.State.Strict
    import Data.Coerce
    import Data.Foldable (foldlM, minimumBy, toList)
    import Data.Monoid   (Any(..))
    import Data.List     (sortBy, find)
    import qualified Data.List.NonEmpty as NE
    import Data.Ord      (comparing)

    --
    -- * Main exports
    --

    -- | Add a bunch of 'PhiCt's to all the 'Nabla's.
    -- Lifts 'addPhiCts' over many 'Nablas'.
    addPhiCtsNablas :: Nablas -> PhiCts -> DsM Nablas
    addPhiCtsNablas :: Nablas -> PhiCts -> DsM Nablas
    addPhiCtsNablas Nablas
    nablas PhiCts
    cts = (Nabla -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla))
    -> Nablas -> DsM Nablas
    forall (m :: * -> *).
    Monad m =>
    (Nabla -> m (Maybe Nabla)) -> Nablas -> m Nablas
    liftNablasM (\Nabla
    d -> Nabla -> PhiCts -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
    addPhiCts Nabla
    d PhiCts
    cts) Nablas
    nablas

    -- | 'addPmCtsNablas' for a single 'PmCt'.
    addPhiCtNablas :: Nablas -> PhiCt -> DsM Nablas
    addPhiCtNablas :: Nablas -> PhiCt -> DsM Nablas
    addPhiCtNablas Nablas
    nablas PhiCt
    ct = Nablas -> PhiCts -> DsM Nablas
    addPhiCtsNablas Nablas
    nablas (PhiCt -> PhiCts
    forall a. a -> Bag a
    unitBag PhiCt
    ct)

    liftNablasM :: Monad m => (Nabla -> m (Maybe Nabla)) -> Nablas -> m Nablas
    liftNablasM :: forall (m :: * -> *).
    Monad m =>
    (Nabla -> m (Maybe Nabla)) -> Nablas -> m Nablas
    liftNablasM Nabla -> m (Maybe Nabla)
    f (MkNablas Bag Nabla
    ds) = Bag Nabla -> Nablas
    MkNablas (Bag Nabla -> Nablas)
    -> (Bag (Maybe Nabla) -> Bag Nabla) -> Bag (Maybe Nabla) -> Nablas
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bag (Maybe Nabla) -> Bag Nabla
    forall a. Bag (Maybe a) -> Bag a
    catBagMaybes (Bag (Maybe Nabla) -> Nablas) -> m (Bag (Maybe Nabla)) -> m Nablas
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((Nabla -> m (Maybe Nabla)) -> Bag Nabla -> m (Bag (Maybe Nabla))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Bag a -> f (Bag b)
    traverse Nabla -> m (Maybe Nabla)
    f Bag Nabla
    ds)

    -- | Test if any of the 'Nabla's is inhabited. Currently this is pure, because
    -- we preserve the invariant that there are no uninhabited 'Nabla's. But that
    -- could change in the future, for example by implementing this function in
    -- terms of @notNull <$> generateInhabitingPatterns 1 ds@.
    isInhabited :: Nablas -> DsM Bool
    isInhabited :: Nablas -> DsM Bool
    isInhabited (MkNablas Bag Nabla
    ds) = Bool -> DsM Bool
    forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> Bool
    not (Bag Nabla -> Bool
    forall a. Bag a -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Bag Nabla
    ds))

    -----------------------------------------------
    -- * Caching residual COMPLETE sets

    -- See Note [Implementation of COMPLETE pragmas]

    -- | Update the COMPLETE sets of 'ResidualCompleteMatches', or 'Nothing'
    -- if there was no change as per the update function.
    updRcm :: (CompleteMatch          -> (Bool, CompleteMatch))
           -> ResidualCompleteMatches -> (Maybe ResidualCompleteMatches)
    updRcm :: (CompleteMatch -> (Bool, CompleteMatch))
    -> ResidualCompleteMatches -> Maybe ResidualCompleteMatches
    updRcm CompleteMatch -> (Bool, CompleteMatch)
    f (RCM Maybe CompleteMatch
    vanilla Maybe [CompleteMatch]
    pragmas)
      | Bool -> Bool
    not Bool
    any_change = Maybe ResidualCompleteMatches
    forall a. Maybe a
    Nothing
      | Bool
    otherwise      = ResidualCompleteMatches -> Maybe ResidualCompleteMatches
    forall a. a -> Maybe a
    Just (Maybe CompleteMatch
    -> Maybe [CompleteMatch] -> ResidualCompleteMatches
    RCM Maybe CompleteMatch
    vanilla' Maybe [CompleteMatch]
    pragmas')
      where
        f' ::  CompleteMatch          -> (Any,  CompleteMatch)
        f' :: CompleteMatch -> (Any, CompleteMatch)
    f' = (CompleteMatch -> (Bool, CompleteMatch))
    -> CompleteMatch -> (Any, CompleteMatch)
    forall a b. Coercible a b => a -> b
    coerce CompleteMatch -> (Bool, CompleteMatch)
    f
        (Any
    chgd, Maybe CompleteMatch
    vanilla')  = (CompleteMatch -> (Any, CompleteMatch))
    -> Maybe CompleteMatch -> (Any, Maybe CompleteMatch)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Maybe a -> f (Maybe b)
    traverse CompleteMatch -> (Any, CompleteMatch)
    f' Maybe CompleteMatch
    vanilla
        (Any
    chgds, Maybe [CompleteMatch]
    pragmas') = ([CompleteMatch] -> (Any, [CompleteMatch]))
    -> Maybe [CompleteMatch] -> (Any, Maybe [CompleteMatch])
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Maybe a -> f (Maybe b)
    traverse ((CompleteMatch -> (Any, CompleteMatch))
    -> [CompleteMatch] -> (Any, [CompleteMatch])
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse CompleteMatch -> (Any, CompleteMatch)
    f') Maybe [CompleteMatch]
    pragmas
        any_change :: Bool
    any_change        = Any -> Bool
    getAny (Any -> Bool) -> Any -> Bool
    forall a b. (a -> b) -> a -> b
    $ Any
    chgd Any -> Any -> Any
    forall a. Monoid a => a -> a -> a
    `mappend` Any
    chgds

    -- | A pseudo-'CompleteMatch' for the vanilla complete set of the given data
    -- 'TyCon'.
    -- Ex.: @vanillaCompleteMatchTC 'Maybe' ==> Just ("Maybe", {'Just','Nothing'})@
    vanillaCompleteMatchTC :: TyCon -> Maybe CompleteMatch
    vanillaCompleteMatchTC :: TyCon -> Maybe CompleteMatch
    vanillaCompleteMatchTC TyCon
    tc =
      let mb_dcs :: Maybe [DataCon]
    mb_dcs | -- TYPE acts like an empty data type on the term level (#14086),
                   -- but it is a PrimTyCon, so tyConDataCons_maybe returns Nothing.
                   -- Hence a special case.
                   TyCon
    tc TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    tYPETyCon    = [DataCon] -> Maybe [DataCon]
    forall a. a -> Maybe a
    Just []
                 | -- Similarly, treat `type data` declarations as empty data types on
                   -- the term level, as `type data` data constructors only exist at
                   -- the type level (#22964).  See wrinkle (W2a) in
                   -- Note [Type data declarations] in GHC.Rename.Module.
                   TyCon -> Bool
    isTypeDataTyCon TyCon
    tc = [DataCon] -> Maybe [DataCon]
    forall a. a -> Maybe a
    Just []
                 | Bool
    otherwise          = TyCon -> Maybe [DataCon]
    tyConDataCons_maybe TyCon
    tc
      in UniqDSet ConLike -> CompleteMatch
    vanillaCompleteMatch (UniqDSet ConLike -> CompleteMatch)
    -> ([DataCon] -> UniqDSet ConLike) -> [DataCon] -> CompleteMatch
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [ConLike] -> UniqDSet ConLike
    forall a. Uniquable a => [a] -> UniqDSet a
    mkUniqDSet ([ConLike] -> UniqDSet ConLike)
    -> ([DataCon] -> [ConLike]) -> [DataCon] -> UniqDSet ConLike
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (DataCon -> ConLike) -> [DataCon] -> [ConLike]
    forall a b. (a -> b) -> [a] -> [b]
    map DataCon -> ConLike
    RealDataCon ([DataCon] -> CompleteMatch)
    -> Maybe [DataCon] -> Maybe CompleteMatch
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe [DataCon]
    mb_dcs

    -- | Initialise from 'dsGetCompleteMatches' (containing all COMPLETE pragmas)
    -- if the given 'ResidualCompleteMatches' were empty.
    addCompleteMatches :: ResidualCompleteMatches -> DsM ResidualCompleteMatches
    addCompleteMatches :: ResidualCompleteMatches -> DsM ResidualCompleteMatches
    addCompleteMatches (RCM Maybe CompleteMatch
    v Maybe [CompleteMatch]
    Nothing) = Maybe CompleteMatch
    -> Maybe [CompleteMatch] -> ResidualCompleteMatches
    RCM Maybe CompleteMatch
    v (Maybe [CompleteMatch] -> ResidualCompleteMatches)
    -> ([CompleteMatch] -> Maybe [CompleteMatch])
    -> [CompleteMatch]
    -> ResidualCompleteMatches
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [CompleteMatch] -> Maybe [CompleteMatch]
    forall a. a -> Maybe a
    Just ([CompleteMatch] -> ResidualCompleteMatches)
    -> IOEnv (Env DsGblEnv DsLclEnv) [CompleteMatch]
    -> DsM ResidualCompleteMatches
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IOEnv (Env DsGblEnv DsLclEnv) [CompleteMatch]
    dsGetCompleteMatches
    addCompleteMatches ResidualCompleteMatches
    rcm             = ResidualCompleteMatches -> DsM ResidualCompleteMatches
    forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ResidualCompleteMatches
    rcm

    -- | Adds the declared 'CompleteMatches' from COMPLETE pragmas, as well as the
    -- vanilla data defn if it is a 'DataCon'.
    addConLikeMatches :: ConLike -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
    addConLikeMatches :: ConLike -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
    addConLikeMatches (RealDataCon DataCon
    dc) ResidualCompleteMatches
    rcm = TyCon -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
    addTyConMatches (DataCon -> TyCon
    dataConTyCon DataCon
    dc) ResidualCompleteMatches
    rcm
    addConLikeMatches (PatSynCon PatSyn
    _)    ResidualCompleteMatches
    rcm = ResidualCompleteMatches -> DsM ResidualCompleteMatches
    addCompleteMatches ResidualCompleteMatches
    rcm

    -- | Adds
    --    * the 'CompleteMatches' from COMPLETE pragmas
    --    * and the /vanilla/ 'CompleteMatch' from the data 'TyCon'
    -- to the 'ResidualCompleteMatches', if not already present.
    addTyConMatches :: TyCon -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
    addTyConMatches :: TyCon -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
    addTyConMatches TyCon
    tc ResidualCompleteMatches
    rcm = ResidualCompleteMatches -> ResidualCompleteMatches
    add_tc_match (ResidualCompleteMatches -> ResidualCompleteMatches)
    -> DsM ResidualCompleteMatches -> DsM ResidualCompleteMatches
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ResidualCompleteMatches -> DsM ResidualCompleteMatches
    addCompleteMatches ResidualCompleteMatches
    rcm
      where
        -- Add the vanilla COMPLETE set from the data defn, if any. But only if
        -- it's not already present.
        add_tc_match :: ResidualCompleteMatches -> ResidualCompleteMatches
    add_tc_match ResidualCompleteMatches
    rcm
          = ResidualCompleteMatches
    rcm{rcm_vanilla = rcm_vanilla rcm <|> vanillaCompleteMatchTC tc}

    markMatched :: PmAltCon -> ResidualCompleteMatches -> DsM (Maybe ResidualCompleteMatches)
    -- Nothing means the PmAltCon didn't occur in any COMPLETE set.
    -- See Note [Shortcutting the inhabitation test] for how this is useful for
    -- performance on T17836.
    markMatched :: PmAltCon
    -> ResidualCompleteMatches -> DsM (Maybe ResidualCompleteMatches)
    markMatched (PmAltLit PmLit
    _)      ResidualCompleteMatches
    _   = Maybe ResidualCompleteMatches
    -> DsM (Maybe ResidualCompleteMatches)
    forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Maybe ResidualCompleteMatches
    forall a. Maybe a
    Nothing -- lits are never part of a COMPLETE set
    markMatched (PmAltConLike ConLike
    cl) ResidualCompleteMatches
    rcm = do
      rcm' <- ConLike -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
    addConLikeMatches ConLike
    cl ResidualCompleteMatches
    rcm
      let go CompleteMatch
    cm = case UniqDSet ConLike -> ConLike -> Maybe ConLike
    forall a. Uniquable a => UniqDSet a -> a -> Maybe a
    lookupUniqDSet (CompleteMatch -> UniqDSet ConLike
    cmConLikes CompleteMatch
    cm) ConLike
    cl of
            Maybe ConLike
    Nothing -> (Bool
    False, CompleteMatch
    cm)
            Just ConLike
    _  -> (Bool
    True,  CompleteMatch
    cm { cmConLikes = delOneFromUniqDSet (cmConLikes cm) cl })
      pure $ updRcm go rcm'

    {-
    Note [Implementation of COMPLETE pragmas]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    A COMPLETE set represents a set of conlikes (i.e., constructors or
    pattern synonyms) such that if they are all pattern-matched against in a
    function, it gives rise to a total function. An example is:

      newtype Boolean = Boolean Int
      pattern F, T :: Boolean
      pattern F = Boolean 0
      pattern T = Boolean 1
      {-# COMPLETE F, T #-}

      -- This is a total function
      booleanToInt :: Boolean -> Int
      booleanToInt F = 0
      booleanToInt T = 1

    COMPLETE sets are represented internally in GHC as a set of 'ConLike's. For
    example, the pragma {-# COMPLETE F, T #-} would be represented as:

      CompleteMatch {F, T} Nothing

    What is the Maybe for? Answer: COMPLETE pragmas may optionally specify a
    result *type constructor* (cf. T14422):

      class C f where
        foo :: f a -> ()
      pattern P :: C f => f a
      pattern P <- (foo -> ())

      instance C State where
        foo _ = ()
      {-# COMPLETE P :: State #-}

      f :: State a -> ()
      f P = ()
      g :: C f => f a -> ()
      g P = ()

    The @:: State@ here means that the types at which the COMPLETE pragma *applies*
    is restricted to scrutinee types that are applications of the 'State' TyCon. So
    it applies to the match in @f@ but not in @g@ above, resulting in a warning for
    the latter but not for the former. The pragma is represented as

      CompleteMatch {P} (Just State)

    GHC collects all COMPLETE pragmas from the current module and from imports
    into a field in the DsM environment, which can be accessed with
    dsGetCompleteMatches from "GHC.HsToCore.Monad".
    Currently, COMPLETE pragmas can't be orphans (e.g. at least one ConLike must
    also be defined in the module of the pragma) and do not impact recompilation
    checking (#18675).

    The pattern-match checker will then initialise each variable's 'VarInfo' with
    *all* imported COMPLETE sets (in 'GHC.HsToCore.Pmc.Solver.addCompleteMatches'),
    well-typed or not, into a 'ResidualCompleteMatches'. The trick is that a
    COMPLETE set that is ill-typed for that match variable could never be written by
    the user! And we make sure not to report any ill-typed COMPLETE sets when
    formatting 'Nabla's for warnings in 'generateInhabitingPatterns'.

    A 'ResidualCompleteMatches' is a list of all COMPLETE sets, minus the ConLikes
    we know a particular variable can't be (through negative constructor constraints
    @x /~ K@ or a failed attempt at instantiating that ConLike during inhabitation
    testing). If *any* of the COMPLETE sets become empty, we know that the match
    was exhaustive.

    We assume that a COMPLETE set does not apply if for one of its
    ConLikes we fail to 'matchConLikeResTy' or the
    type of the match variable isn't an application of the optional
    result type constructor from the pragma. Why don't we simply
    prune inapplicable COMPLETE sets from 'ResidualCompleteMatches'?
    The answer is that additional type constraints might make more
    COMPLETE sets applicable! Example:

      h :: a -> a :~: Boolean -> ()
      h x Refl | T <- x = ()
               | F <- x = ()

    If we eagerly prune {F,T} from the residual matches of @x@, then we don't see
    that the match in the guards of @h@ is exhaustive, where the COMPLETE set
    applies due to refined type information.
    -}

    -----------------------
    -- * Type normalisation

    -- | The return value of 'pmTopNormaliseType'
    data TopNormaliseTypeResult
      = NormalisedByConstraints Type
      -- ^ 'tcNormalise' was able to simplify the type with some local constraint
      -- from the type oracle, but 'topNormaliseTypeX' couldn't identify a type
      -- redex.
      | HadRedexes Type [(Type, DataCon, Type)] Type
      -- ^ 'tcNormalise' may or may not been able to simplify the type, but
      -- 'topNormaliseTypeX' made progress either way and got rid of at least one
      -- outermost type or data family redex or newtype.
      -- The first field is the last type that was reduced solely through type
      -- family applications (possibly just the 'tcNormalise'd type). This is the
      -- one that is equal (in source Haskell) to the initial type.
      -- The third field is the type that we get when also looking through data
      -- family applications and newtypes. This would be the representation type in
      -- Core (modulo casts).
      -- The second field is the list of Newtype 'DataCon's that we looked through
      -- in the chain of reduction steps between the Source type and the Core type.
      -- We also keep the type of the DataCon application and its field, so that we
      -- don't have to reconstruct it in 'inhabitationCandidates' and
      -- 'generateInhabitingPatterns'.
      -- For an example, see Note [Type normalisation].

    -- | Return the fields of 'HadRedexes'. Returns appropriate defaults in the
    -- other cases.
    tntrGuts :: TopNormaliseTypeResult -> (Type, [(Type, DataCon, Type)], Type)
    tntrGuts :: TopNormaliseTypeResult -> (Type, [(Type, DataCon, Type)], Type)
    tntrGuts (NormalisedByConstraints Type
    ty)   = (Type
    ty,     [],      Type
    ty)
    tntrGuts (HadRedexes Type
    src_ty [(Type, DataCon, Type)]
    ds Type
    core_ty) = (Type
    src_ty, [(Type, DataCon, Type)]
    ds, Type
    core_ty)

    instance Outputable TopNormaliseTypeResult where
      ppr :: TopNormaliseTypeResult -> SDoc
    ppr (NormalisedByConstraints Type
    ty)   = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "NormalisedByConstraints" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Type -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Type
    ty
      ppr (HadRedexes Type
    src_ty [(Type, DataCon, Type)]
    ds Type
    core_ty) = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "HadRedexes" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc
    braces SDoc
    fields
        where
          fields :: SDoc
    fields = [SDoc] -> SDoc
    forall doc. IsLine doc => [doc] -> doc
    fsep (SDoc -> [SDoc] -> [SDoc]
    forall doc. IsLine doc => doc -> [doc] -> [doc]
    punctuate SDoc
    forall doc. IsLine doc => doc
    comma [ String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "src_ty =" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Type -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Type
    src_ty
                                         , String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "newtype_dcs =" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> [(Type, DataCon, Type)] -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr [(Type, DataCon, Type)]
    ds
                                         , String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "core_ty =" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Type -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Type
    core_ty ])

    pmTopNormaliseType :: TyState -> Type -> DsM TopNormaliseTypeResult
    -- ^ Get rid of *outermost* (or toplevel)
    --      * type function redex
    --      * data family redex
    --      * newtypes
    --
    -- Behaves like `topNormaliseType_maybe`, but instead of returning a
    -- coercion, it returns useful information for issuing pattern matching
    -- warnings. See Note [Type normalisation] for details.
    -- It also initially 'tcNormalise's the type with the bag of local constraints.
    --
    -- See 'TopNormaliseTypeResult' for the meaning of the return value.
    --
    -- NB: Normalisation can potentially change kinds, if the head of the type
    -- is a type family with a variable result kind. I (Richard E) can't think
    -- of a way to cause trouble here, though.
    pmTopNormaliseType :: TyState -> Type -> DsM TopNormaliseTypeResult
    pmTopNormaliseType (TySt Int
    _ InertSet
    inert) Type
    typ = {-# SCC "pmTopNormaliseType" #-} do
      env <- DsM FamInstEnvs
    dsGetFamInstEnvs
      tracePm "normalise" (ppr typ)
      -- Before proceeding, we chuck typ into the constraint solver, in case
      -- solving for given equalities may reduce typ some. See
      -- "Wrinkle: local equalities" in Note [Type normalisation].
      typ' <- initTcDsForSolver $ tcNormalise inert typ
      -- Now we look with topNormaliseTypeX through type and data family
      -- applications and newtypes, which tcNormalise does not do.
      -- See also 'TopNormaliseTypeResult'.
      pure $ case topNormaliseTypeX (stepper env) comb typ' of
        Maybe
      ((ThetaType -> ThetaType,
        [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]),
       Type)
    Nothing                -> Type -> TopNormaliseTypeResult
    NormalisedByConstraints Type
    typ'
        Just ((ThetaType -> ThetaType
    ty_f,[(Type, DataCon, Type)] -> [(Type, DataCon, Type)]
    tm_f), Type
    ty) -> Type -> [(Type, DataCon, Type)] -> Type -> TopNormaliseTypeResult
    HadRedexes Type
    src_ty [(Type, DataCon, Type)]
    newtype_dcs Type
    core_ty
          where
            src_ty :: Type
    src_ty = Type -> ThetaType -> Type
    eq_src_ty Type
    ty (Type
    typ' Type -> ThetaType -> ThetaType
    forall a. a -> [a] -> [a]
    : ThetaType -> ThetaType
    ty_f [Type
    ty])
            newtype_dcs :: [(Type, DataCon, Type)]
    newtype_dcs = [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]
    tm_f []
            core_ty :: Type
    core_ty = Type
    ty
      where
        -- Find the first type in the sequence of rewrites that is a data type,
        -- newtype, or a data family application (not the representation tycon!).
        -- This is the one that is equal (in source Haskell) to the initial type.
        -- If none is found in the list, then all of them are type family
        -- applications, so we simply return the last one, which is the *simplest*.
        eq_src_ty :: Type -> [Type] -> Type
        eq_src_ty :: Type -> ThetaType -> Type
    eq_src_ty Type
    ty ThetaType
    tys = Type -> (Type -> Type) -> Maybe Type -> Type
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Type
    ty Type -> Type
    forall a. a -> a
    id ((Type -> Bool) -> ThetaType -> Maybe Type
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    find Type -> Bool
    is_closed_or_data_family ThetaType
    tys)

        is_closed_or_data_family :: Type -> Bool
        is_closed_or_data_family :: Type -> Bool
    is_closed_or_data_family Type
    ty = Type -> Bool
    pmIsClosedType Type
    ty Bool -> Bool -> Bool
    || Type -> Bool
    isDataFamilyAppType Type
    ty

        -- For efficiency, represent both lists as difference lists.
        -- comb performs the concatenation, for both lists.
        comb :: (b -> c, b -> c) -> (a -> b, a -> b) -> (a -> c, a -> c)
    comb (b -> c
    tyf1, b -> c
    tmf1) (a -> b
    tyf2, a -> b
    tmf2) = (b -> c
    tyf1 (b -> c) -> (a -> b) -> a -> c
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> b
    tyf2, b -> c
    tmf1 (b -> c) -> (a -> b) -> a -> c
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> b
    tmf2)

        stepper :: FamInstEnvs
    -> NormaliseStepper
         (ThetaType -> ThetaType,
          [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
    stepper FamInstEnvs
    env = NormaliseStepper
      (ThetaType -> ThetaType,
       [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
    newTypeStepper NormaliseStepper
      (ThetaType -> ThetaType,
       [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
    -> NormaliseStepper
         (ThetaType -> ThetaType,
          [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
    -> NormaliseStepper
         (ThetaType -> ThetaType,
          [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
    forall ev.
    NormaliseStepper ev -> NormaliseStepper ev -> NormaliseStepper ev
    `composeSteppers` FamInstEnvs
    -> NormaliseStepper
         (ThetaType -> ThetaType,
          [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
    forall a.
    FamInstEnvs -> NormaliseStepper (ThetaType -> ThetaType, a -> a)
    tyFamStepper FamInstEnvs
    env

        -- A 'NormaliseStepper' that unwraps newtypes, careful not to fall into
        -- a loop. If it would fall into a loop, it produces 'NS_Abort'.
        newTypeStepper :: NormaliseStepper ([Type] -> [Type],[(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
        newTypeStepper :: NormaliseStepper
      (ThetaType -> ThetaType,
       [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
    newTypeStepper RecTcChecker
    rec_nts TyCon
    tc ThetaType
    tys
          | Just (Type
    ty', Coercion
    _co) <- TyCon -> ThetaType -> Maybe (Type, Coercion)
    instNewTyCon_maybe TyCon
    tc ThetaType
    tys
          , let orig_ty :: Type
    orig_ty = TyCon -> ThetaType -> Type
    TyConApp TyCon
    tc ThetaType
    tys
          = case RecTcChecker -> TyCon -> Maybe RecTcChecker
    checkRecTc RecTcChecker
    rec_nts TyCon
    tc of
              Just RecTcChecker
    rec_nts' -> let tyf :: ThetaType -> ThetaType
    tyf = (Type
    orig_tyType -> ThetaType -> ThetaType
    forall a. a -> [a] -> [a]
    :)
                                   tmf :: [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]
    tmf = ((Type
    orig_ty, TyCon -> DataCon
    tyConSingleDataCon TyCon
    tc, Type
    ty')(Type, DataCon, Type)
    -> [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]
    forall a. a -> [a] -> [a]
    :)
                               in  RecTcChecker
    -> Type
    -> (ThetaType -> ThetaType,
        [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
    -> NormaliseStepResult
         (ThetaType -> ThetaType,
          [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
    forall ev. RecTcChecker -> Type -> ev -> NormaliseStepResult ev
    NS_Step RecTcChecker
    rec_nts' Type
    ty' (ThetaType -> ThetaType
    tyf, [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]
    tmf)
              Maybe RecTcChecker
    Nothing       -> NormaliseStepResult
      (ThetaType -> ThetaType,
       [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
    forall ev. NormaliseStepResult ev
    NS_Abort
          | Bool
    otherwise
          = NormaliseStepResult
      (ThetaType -> ThetaType,
       [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
    forall ev. NormaliseStepResult ev
    NS_Done

        tyFamStepper :: FamInstEnvs -> NormaliseStepper ([Type] -> [Type], a -> a)
        tyFamStepper :: forall a.
    FamInstEnvs -> NormaliseStepper (ThetaType -> ThetaType, a -> a)
    tyFamStepper FamInstEnvs
    env RecTcChecker
    rec_nts TyCon
    tc ThetaType
    tys  -- Try to step a type/data family
          = case FamInstEnvs -> TyCon -> ThetaType -> Maybe HetReduction
    topReduceTyFamApp_maybe FamInstEnvs
    env TyCon
    tc ThetaType
    tys of
              Just (HetReduction (Reduction Coercion
    _ Type
    rhs) MCoercionN
    _)
                -> RecTcChecker
    -> Type
    -> (ThetaType -> ThetaType, a -> a)
    -> NormaliseStepResult (ThetaType -> ThetaType, a -> a)
    forall ev. RecTcChecker -> Type -> ev -> NormaliseStepResult ev
    NS_Step RecTcChecker
    rec_nts Type
    rhs ((Type
    rhsType -> ThetaType -> ThetaType
    forall a. a -> [a] -> [a]
    :), a -> a
    forall a. a -> a
    id)
              Maybe HetReduction
    _ -> NormaliseStepResult (ThetaType -> ThetaType, a -> a)
    forall ev. NormaliseStepResult ev
    NS_Done

    -- | Returns 'True' if the argument 'Type' is a fully saturated application of
    -- a closed type constructor.
    --
    -- Closed type constructors are those with a fixed right hand side, as
    -- opposed to e.g. associated types. These are of particular interest for
    -- pattern-match coverage checking, because GHC can exhaustively consider all
    -- possible forms that values of a closed type can take on.
    --
    -- Note that this function is intended to be used to check types of value-level
    -- patterns, so as a consequence, the 'Type' supplied as an argument to this
    -- function should be of kind @Type@.
    pmIsClosedType :: Type -> Bool
    pmIsClosedType :: Type -> Bool
    pmIsClosedType Type
    ty
      = case HasDebugCallStack => Type -> Maybe (TyCon, ThetaType)
    Type -> Maybe (TyCon, ThetaType)
    splitTyConApp_maybe Type
    ty of
          Just (TyCon
    tc, ThetaType
    ty_args)
                 | TyCon -> Bool
    is_algebraic_like TyCon
    tc Bool -> Bool -> Bool
    && Bool -> Bool
    not (TyCon -> Bool
    isFamilyTyCon TyCon
    tc)
                 -> Bool -> SDoc -> Bool -> Bool
    forall a. HasCallStack => Bool -> SDoc -> a -> a
    assertPpr (ThetaType
    ty_args ThetaType -> Int -> Bool
    forall a. [a] -> Int -> Bool
    `lengthIs` TyCon -> Int
    tyConArity TyCon
    tc) (Type -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Type
    ty) Bool
    True
          Maybe (TyCon, ThetaType)
    _other -> Bool
    False
      where
        -- This returns True for TyCons which /act like/ algebraic types.
        -- (See "Type#type_classification" for what an algebraic type is.)
        --
        -- This is qualified with \"like\" because of a particular special
        -- case: TYPE (the underlying kind behind Type, among others). TYPE
        -- is conceptually a datatype (and thus algebraic), but in practice it is
        -- a primitive builtin type, so we must check for it specially.
        --
        -- NB: it makes sense to think of TYPE as a closed type in a value-level,
        -- pattern-matching context. However, at the kind level, TYPE is certainly
        -- not closed! Since this function is specifically tailored towards pattern
        -- matching, however, it's OK to label TYPE as closed.
        is_algebraic_like :: TyCon -> Bool
        is_algebraic_like :: TyCon -> Bool
    is_algebraic_like TyCon
    tc = TyCon -> Bool
    isAlgTyCon TyCon
    tc Bool -> Bool -> Bool
    || TyCon
    tc TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    tYPETyCon

    -- | Normalise the given source type to WHNF. If it isn't already in WHNF
    -- ('isSourceTypeInWHNF') , it will normalise the type and then try to step
    -- through type family applications, but not data family applications or
    -- newtypes.
    --
    -- This is a pretty common case of calling 'pmTopNormaliseType' and it should be
    -- efficient.
    normaliseSourceTypeWHNF :: TyState -> Type -> DsM Type
    normaliseSourceTypeWHNF :: TyState -> Type -> DsM Type
    normaliseSourceTypeWHNF TyState
    _     Type
    ty | Type -> Bool
    isSourceTypeInWHNF Type
    ty = Type -> DsM Type
    forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Type
    ty
    normaliseSourceTypeWHNF TyState
    ty_st Type
    ty =
      TyState -> Type -> DsM TopNormaliseTypeResult
    pmTopNormaliseType TyState
    ty_st Type
    ty DsM TopNormaliseTypeResult
    -> (TopNormaliseTypeResult -> DsM Type) -> DsM Type
    forall a b.
    IOEnv (Env DsGblEnv DsLclEnv) a
    -> (a -> IOEnv (Env DsGblEnv DsLclEnv) b)
    -> IOEnv (Env DsGblEnv DsLclEnv) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        NormalisedByConstraints Type
    ty -> Type -> DsM Type
    forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Type
    ty
        HadRedexes Type
    ty [(Type, DataCon, Type)]
    _ Type
    _          -> Type -> DsM Type
    forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Type
    ty

    -- | Is the source type in WHNF wrt. 'pmTopNormaliseType'?
    --
    -- Returns False if the given type is not a TyCon application, or if the TyCon
    -- app head is a type family TyCon. (But not for data family TyCons!)
    isSourceTypeInWHNF :: Type -> Bool
    isSourceTypeInWHNF :: Type -> Bool
    isSourceTypeInWHNF Type
    ty
      | Just (TyCon
    tc, ThetaType
    _) <- HasDebugCallStack => Type -> Maybe (TyCon, ThetaType)
    Type -> Maybe (TyCon, ThetaType)
    splitTyConApp_maybe Type
    ty = Bool -> Bool
    not (TyCon -> Bool
    isTypeFamilyTyCon TyCon
    tc)
      | Bool
    otherwise                              = Bool
    False

    {- Note [Type normalisation]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Constructs like -XEmptyCase or a previous unsuccessful pattern match on a data
    constructor place a non-void constraint on the matched thing. This means that it
    boils down to checking whether the type of the scrutinee is inhabited. Function
    pmTopNormaliseType gets rid of the outermost type function/data family redex and
    newtypes, in search of an algebraic type constructor, which is easier to check
    for inhabitation.

    It returns 3 results instead of one, because there are 2 subtle points:
    1. Newtypes are isomorphic to the underlying type in core but not in the source
       language,
    2. The representational data family tycon is used internally but should not be
       shown to the user

    Hence, if pmTopNormaliseType env ty_cs ty = Just (src_ty, dcs, core_ty),
    then
      (a) src_ty is the rewritten type which we can show to the user. That is, the
          type we get if we rewrite type families but not data families or
          newtypes.
      (b) dcs is the list of newtype constructors "skipped", every time we normalise
          a newtype to its core representation, we keep track of the source data
          constructor. For convenience, we also track the type we unwrap and the
          type of its field. Example: @Down 42@ => @[(Down @Int, Down, Int)]
      (c) core_ty is the rewritten type. That is,
            pmTopNormaliseType env ty_cs ty = Just (src_ty, dcs, core_ty)
          implies
            topNormaliseType_maybe env ty = Just (co, core_ty)
          for some coercion co.

    To see how all cases come into play, consider the following example:

      data family T a :: *
      data instance T Int = T1 | T2 Bool
      -- Which gives rise to FC:
      --   data T a
      --   data R:TInt = T1 | T2 Bool
      --   axiom ax_ti : T Int ~R R:TInt

      newtype G1 = MkG1 (T Int)
      newtype G2 = MkG2 G1

      type instance F Int  = F Char
      type instance F Char = G2

    In this case pmTopNormaliseType env ty_cs (F Int) results in

      Just (G2, [(G2,MkG2,G1),(G1,MkG1,T Int)], R:TInt)

    Which means that in source Haskell:
      - G2 is equivalent to F Int (in contrast, G1 isn't).
      - if (x : R:TInt) then (MkG2 (MkG1 x) : F Int).

    -----
    -- Wrinkle: Local equalities
    -----

    Given the following type family:

      type family F a
      type instance F Int = Void

    Should the following program (from #14813) be considered exhaustive?

      f :: (i ~ Int) => F i -> a
      f x = case x of {}

    You might think "of course, since `x` is obviously of type Void". But the
    idType of `x` is technically F i, not Void, so if we pass F i to
    inhabitationCandidates, we'll mistakenly conclude that `f` is non-exhaustive.
    In order to avoid this pitfall, we need to normalise the type passed to
    pmTopNormaliseType, using the constraint solver to solve for any local
    equalities (such as i ~ Int) that may be in scope.

    Note [Coverage checking Newtype matches]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Newtypes have quite peculiar match semantics compared to ordinary DataCons. In a
    pattern-match, they behave like a irrefutable (lazy) match, but for inhabitation
    testing purposes (e.g. at construction sites), they behave rather like a DataCon
    with a *strict* field, because they don't contribute their own bottom and are
    inhabited iff the wrapped type is inhabited.

    This distinction becomes apparent in #17248:

      newtype T2 a = T2 a
      g _      True = ()
      g (T2 _) True = ()
      g !_     True = ()

    If we treat Newtypes like we treat regular DataCons, we would mark the third
    clause as redundant, which clearly is unsound. The solution:
    1. 'isPmAltConMatchStrict' returns False for newtypes, indicating that a
       newtype match is lazy.
    2. When we find @x ~ T2 y@, transfer all constraints on @x@ (which involve @⊥@)
       to @y@, similar to what 'equate' does, and don't add a @x ≁ ⊥@ constraint.
       This way, the third clause will still be marked as inaccessible RHS instead
       of redundant. This is ensured by calling 'lookupVarInfoNT'.
    3. Immediately reject when we find @x ≁ T2@.
    Handling of Newtypes is also described in the Appendix of the Lower Your Guards paper,
    where you can find the solution in a perhaps more digestible format.
    -}

    -------------------------
    -- * Adding φ constraints
    --
    -- Figure 7 in the LYG paper.

    -- | A high-level pattern-match constraint. Corresponds to φ from Figure 3 of
    -- the LYG paper.
    data PhiCt
      = PhiTyCt !PredType
      -- ^ A type constraint "T ~ U".
      | PhiCoreCt    !Id !CoreExpr
      -- ^ @PhiCoreCt x e@ encodes "x ~ e", equating @x@ with the 'CoreExpr' @e@.
      | PhiConCt     !Id !PmAltCon ![TyVar] ![PredType] ![Id]
      -- ^ @PhiConCt x K tvs dicts ys@ encodes @K \@tvs dicts ys <- x@, matching @x@
      -- against the 'PmAltCon' application @K \@tvs dicts ys@, binding @tvs@,
      -- @dicts@ and possibly unlifted fields @ys@ in the process.
      -- See Note [Strict fields and variables of unlifted type].
      | PhiNotConCt  !Id !PmAltCon
      -- ^ @PhiNotConCt x K@ encodes "x ≁ K", asserting that @x@ can't be headed
      -- by @K@.
      | PhiBotCt     !Id
      -- ^ @PhiBotCt x@ encodes "x ~ ⊥", equating @x@ to ⊥.
      -- by @K@.
      | PhiNotBotCt !Id
      -- ^ @PhiNotBotCt x y@ encodes "x ≁ ⊥", asserting that @x@ can't be ⊥.

    instance Outputable PhiCt where
      ppr :: PhiCt -> SDoc
    ppr (PhiTyCt Type
    ty_ct)                 = Type -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Type
    ty_ct
      ppr (PhiCoreCt Id
    x CoreExpr
    e)                 = Id -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Id
    x SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Char -> SDoc
    forall doc. IsLine doc => Char -> doc
    char Char
    '~' SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> CoreExpr -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr CoreExpr
    e
      ppr (PhiConCt Id
    x PmAltCon
    con [Id]
    tvs ThetaType
    dicts [Id]
    args) =
        [SDoc] -> SDoc
    forall doc. IsLine doc => [doc] -> doc
    hsep (PmAltCon -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr PmAltCon
    con SDoc -> [SDoc] -> [SDoc]
    forall a. a -> [a] -> [a]
    : [SDoc]
    pp_tvs [SDoc] -> [SDoc] -> [SDoc]
    forall a. [a] -> [a] -> [a]
    ++ [SDoc]
    pp_dicts [SDoc] -> [SDoc] -> [SDoc]
    forall a. [a] -> [a] -> [a]
    ++ [SDoc]
    pp_args) SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "<-" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Id -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Id
    x
        where
          pp_tvs :: [SDoc]
    pp_tvs   = (Id -> SDoc) -> [Id] -> [SDoc]
    forall a b. (a -> b) -> [a] -> [b]
    map ((SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <> Char -> SDoc
    forall doc. IsLine doc => Char -> doc
    char Char
    '@') (SDoc -> SDoc) -> (Id -> SDoc) -> Id -> SDoc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Id -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr) [Id]
    tvs
          pp_dicts :: [SDoc]
    pp_dicts = (Type -> SDoc) -> ThetaType -> [SDoc]
    forall a b. (a -> b) -> [a] -> [b]
    map Type -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ThetaType
    dicts
          pp_args :: [SDoc]
    pp_args  = (Id -> SDoc) -> [Id] -> [SDoc]
    forall a b. (a -> b) -> [a] -> [b]
    map Id -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr [Id]
    args
      ppr (PhiNotConCt Id
    x PmAltCon
    con)             = Id -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Id
    x SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "≁" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> PmAltCon -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr PmAltCon
    con
      ppr (PhiBotCt Id
    x)                    = Id -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Id
    x SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "~ ⊥"
      ppr (PhiNotBotCt Id
    x)                 = Id -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Id
    x SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "≁ ⊥"

    type PhiCts = Bag PhiCt

    -- | The fuel for the inhabitation test.
    -- See Note [Fuel for the inhabitation test].
    initFuel :: Int
    initFuel :: Int
    initFuel = Int
    4 -- 4 because it's the smallest number that passes f' in T17977b

    -- | Adds new constraints to 'Nabla' and returns 'Nothing' if that leads to a
    -- contradiction.
    --
    -- In terms of the paper, this function models the \(⊕_φ\) function in
    -- Figure 7 on batches of φ constraints.
    addPhiCts :: Nabla -> PhiCts -> DsM (Maybe Nabla)
    -- See Note [TmState invariants].
    addPhiCts :: Nabla -> PhiCts -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
    addPhiCts Nabla
    nabla PhiCts
    cts = MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT (MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
     -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla))
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
    forall a b. (a -> b) -> a -> b
    $ do
      let (ThetaType
    ty_cts, [PhiCt]
    tm_cts) = PhiCts -> (ThetaType, [PhiCt])
    partitionPhiCts PhiCts
    cts
      nabla' <- Nabla -> Bag Type -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    addTyCts Nabla
    nabla (ThetaType -> Bag Type
    forall a. [a] -> Bag a
    listToBag ThetaType
    ty_cts)
      nabla'' <- foldlM addPhiTmCt nabla' (listToBag tm_cts)
      inhabitationTest initFuel (nabla_ty_st nabla) nabla''

    partitionPhiCts :: PhiCts -> ([PredType], [PhiCt])
    partitionPhiCts :: PhiCts -> (ThetaType, [PhiCt])
    partitionPhiCts = (PhiCt -> Either Type PhiCt) -> [PhiCt] -> (ThetaType, [PhiCt])
    forall a b c. (a -> Either b c) -> [a] -> ([b], [c])
    partitionWith PhiCt -> Either Type PhiCt
    to_either ([PhiCt] -> (ThetaType, [PhiCt]))
    -> (PhiCts -> [PhiCt]) -> PhiCts -> (ThetaType, [PhiCt])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PhiCts -> [PhiCt]
    forall a. Bag a -> [a]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    toList
      where
        to_either :: PhiCt -> Either Type PhiCt
    to_either (PhiTyCt Type
    pred_ty) = Type -> Either Type PhiCt
    forall a b. a -> Either a b
    Left Type
    pred_ty
        to_either PhiCt
    ct                = PhiCt -> Either Type PhiCt
    forall a b. b -> Either a b
    Right PhiCt
    ct

    -----------------------------
    -- ** Adding type constraints

    -- | Adds new type-level constraints by calling out to the type-checker via
    -- 'tyOracle'.
    addTyCts :: Nabla -> Bag PredType -> MaybeT DsM Nabla
    addTyCts :: Nabla -> Bag Type -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    addTyCts nabla :: Nabla
    nabla@MkNabla{ nabla_ty_st :: Nabla -> TyState
    nabla_ty_st = TyState
    ty_st } Bag Type
    new_ty_cs = do
      ty_st' <- DsM (Maybe TyState)
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) TyState
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (TyState -> Bag Type -> DsM (Maybe TyState)
    tyOracle TyState
    ty_st Bag Type
    new_ty_cs)
      pure nabla{ nabla_ty_st = ty_st' }

    -- | Add some extra type constraints to the 'TyState'; return 'Nothing' if we
    -- find a contradiction (e.g. @Int ~ Bool@).
    --
    -- See Note [Pattern match warnings with insoluble Givens] in GHC.Tc.Solver.
    tyOracle :: TyState -> Bag PredType -> DsM (Maybe TyState)
    tyOracle :: TyState -> Bag Type -> DsM (Maybe TyState)
    tyOracle ty_st :: TyState
    ty_st@(TySt Int
    n InertSet
    inert) Bag Type
    cts
      | Bag Type -> Bool
    forall a. Bag a -> Bool
    isEmptyBag Bag Type
    cts
      = Maybe TyState -> DsM (Maybe TyState)
    forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (TyState -> Maybe TyState
    forall a. a -> Maybe a
    Just TyState
    ty_st)
      | Bool
    otherwise
      = {-# SCC "tyOracle" #-}
        do { evs <- (Type -> IOEnv (Env DsGblEnv DsLclEnv) Id)
    -> Bag Type -> IOEnv (Env DsGblEnv DsLclEnv) (Bag Id)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Bag a -> f (Bag b)
    traverse Type -> IOEnv (Env DsGblEnv DsLclEnv) Id
    nameTyCt Bag Type
    cts
           ; tracePm "tyOracle" (ppr n $$ ppr cts $$ ppr inert)
           ; mb_new_inert <- initTcDsForSolver $ tcCheckGivens inert evs
             -- return the new inert set and increment the sequence number n
           ; return (TySt (n+1) <$> mb_new_inert) }

    -- | Allocates a fresh 'EvVar' name for 'PredTy's.
    nameTyCt :: PredType -> DsM EvVar
    nameTyCt :: Type -> IOEnv (Env DsGblEnv DsLclEnv) Id
    nameTyCt Type
    pred_ty = do
      unique <- IOEnv (Env DsGblEnv DsLclEnv) Unique
    forall (m :: * -> *). MonadUnique m => m Unique
    getUniqueM
      let occname = FastString -> OccName
    mkVarOccFS (String -> FastString
    fsLit (String
    "pm_"String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++Unique -> String
    forall a. Show a => a -> String
    show Unique
    unique))
      return (mkUserLocalOrCoVar occname unique ManyTy pred_ty noSrcSpan)

    -----------------------------
    -- ** Adding term constraints

    -- | Adds a single higher-level φ constraint by dispatching to the various
    -- oracle functions.
    --
    -- In terms of the paper, this function amounts to the constructor constraint
    -- case of \(⊕_φ\) in Figure 7, which "desugars" higher-level φ constraints
    -- into lower-level δ constraints. We don't have a data type for δ constraints
    -- and call the corresponding oracle function directly instead.
    --
    -- Precondition: The φ is /not/ a type constraint! These should be handled by
    -- 'addTyCts' before, through 'addPhiCts'.
    addPhiTmCt :: Nabla -> PhiCt -> MaybeT DsM Nabla
    addPhiTmCt :: Nabla -> PhiCt -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    addPhiTmCt Nabla
    _     (PhiTyCt Type
    ct)              = String -> SDoc -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    forall a. HasCallStack => String -> SDoc -> a
    pprPanic String
    "addPhiCt:TyCt" (Type -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Type
    ct) -- See the precondition
    addPhiTmCt Nabla
    nabla (PhiCoreCt Id
    x CoreExpr
    e)           = Nabla
    -> Id -> CoreExpr -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    addCoreCt Nabla
    nabla Id
    x CoreExpr
    e
    addPhiTmCt Nabla
    nabla (PhiConCt Id
    x PmAltCon
    con [Id]
    tvs ThetaType
    dicts [Id]
    args) = do
      -- Case (1) of Note [Strict fields and variables of unlifted type]
      -- PhiConCt correspond to the higher-level φ constraints from the paper with
      -- bindings semantics. It disperses into lower-level δ constraints that the
      -- 'add*Ct' functions correspond to.
      nabla' <- Nabla -> Bag Type -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    addTyCts Nabla
    nabla (ThetaType -> Bag Type
    forall a. [a] -> Bag a
    listToBag ThetaType
    dicts)
      nabla'' <- addConCt nabla' x con tvs args
      foldlM addNotBotCt nabla'' (filterUnliftedFields con args)
    addPhiTmCt Nabla
    nabla (PhiNotConCt Id
    x PmAltCon
    con)       = Nabla
    -> Id -> PmAltCon -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    addNotConCt Nabla
    nabla Id
    x PmAltCon
    con
    addPhiTmCt Nabla
    nabla (PhiBotCt Id
    x)              = Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    addBotCt Nabla
    nabla Id
    x
    addPhiTmCt Nabla
    nabla (PhiNotBotCt Id
    x)           = Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    addNotBotCt Nabla
    nabla Id
    x

    filterUnliftedFields :: PmAltCon -> [Id] -> [Id]
    filterUnliftedFields :: PmAltCon -> [Id] -> [Id]
    filterUnliftedFields PmAltCon
    con [Id]
    args =
      [ Id
    arg | (Id
    arg, HsImplBang
    bang) <- String -> [Id] -> [HsImplBang] -> [(Id, HsImplBang)]
    forall a b. HasDebugCallStack => String -> [a] -> [b] -> [(a, b)]
    zipEqual String
    "addPhiCt" [Id]
    args (PmAltCon -> [HsImplBang]
    pmAltConImplBangs PmAltCon
    con)
            , HsImplBang -> Bool
    isBanged HsImplBang
    bang Bool -> Bool -> Bool
    || Type -> Bool
    definitelyUnliftedType (Id -> Type
    idType Id
    arg) ]

    -- | Adds the constraint @x ~ ⊥@, e.g. that evaluation of a particular 'Id' @x@
    -- surely diverges. Quite similar to 'addConCt', only that it only cares about
    -- ⊥.
    addBotCt :: Nabla -> Id -> MaybeT DsM Nabla
    addBotCt :: Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    addBotCt nabla :: Nabla
    nabla@MkNabla{ nabla_tm_st :: Nabla -> TmState
    nabla_tm_st = ts :: TmState
    ts@TmSt{ ts_facts :: TmState -> UniqSDFM Id VarInfo
    ts_facts=UniqSDFM Id VarInfo
    env } } Id
    x = do
      let (Id
    y, vi :: VarInfo
    vi@VI { vi_bot :: VarInfo -> BotInfo
    vi_bot = BotInfo
    bot }) = TmState -> Id -> (Id, VarInfo)
    lookupVarInfoNT (Nabla -> TmState
    nabla_tm_st Nabla
    nabla) Id
    x
      case BotInfo
    bot of
        BotInfo
    IsNotBot -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    forall a. MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero      -- There was x ≁ ⊥. Contradiction!
        BotInfo
    IsBot    -> Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Nabla
    nabla -- There already is x ~ ⊥. Nothing left to do
        BotInfo
    MaybeBot               -- We add x ~ ⊥
          | Type -> Bool
    definitelyUnliftedType (Id -> Type
    idType Id
    x)
          -- Case (3) in Note [Strict fields and variables of unlifted type]
          -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    forall a. MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero -- unlifted vars can never be ⊥
          | Bool
    otherwise
          -> do
              let vi' :: VarInfo
    vi' = VarInfo
    vi{ vi_bot = IsBot }
              Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Nabla
    nabla{ nabla_tm_st = ts{ts_facts = addToUSDFM env y vi' } }

    -- | Adds the constraint @x ~/ ⊥@ to 'Nabla'. Quite similar to 'addNotConCt',
    -- but only cares for the ⊥ "constructor".
    addNotBotCt :: Nabla -> Id -> MaybeT DsM Nabla
    addNotBotCt :: Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    addNotBotCt nabla :: Nabla
    nabla@MkNabla{ nabla_tm_st :: Nabla -> TmState
    nabla_tm_st = ts :: TmState
    ts@TmSt{ts_facts :: TmState -> UniqSDFM Id VarInfo
    ts_facts=UniqSDFM Id VarInfo
    env} } Id
    x = do
      let (Id
    y, vi :: VarInfo
    vi@VI { vi_bot :: VarInfo -> BotInfo
    vi_bot = BotInfo
    bot }) = TmState -> Id -> (Id, VarInfo)
    lookupVarInfoNT (Nabla -> TmState
    nabla_tm_st Nabla
    nabla) Id
    x
      case BotInfo
    bot of
        BotInfo
    IsBot    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    forall a. MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero      -- There was x ~ ⊥. Contradiction!
        BotInfo
    IsNotBot -> Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Nabla
    nabla -- There already is x ≁ ⊥. Nothing left to do
        BotInfo
    MaybeBot -> do         -- We add x ≁ ⊥ and test if x is still inhabited
          -- Mark dirty for a delayed inhabitation test
          let vi' :: VarInfo
    vi' = VarInfo
    vi{ vi_bot = IsNotBot}
          Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla)
    -> Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    forall a b. (a -> b) -> a -> b
    $ Id -> Nabla -> Nabla
    markDirty Id
    y
               (Nabla -> Nabla) -> Nabla -> Nabla
    forall a b. (a -> b) -> a -> b
    $ Nabla
    nabla{ nabla_tm_st = ts{ ts_facts = addToUSDFM env y vi' } }

    -- | Record a @x ~/ K@ constraint, e.g. that a particular 'Id' @x@ can't
    -- take the shape of a 'PmAltCon' @K@ in the 'Nabla' and return @Nothing@ if
    -- that leads to a contradiction.
    -- See Note [TmState invariants].
    addNotConCt :: Nabla -> Id -> PmAltCon -> MaybeT DsM Nabla
    addNotConCt :: Nabla
    -> Id -> PmAltCon -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    addNotConCt Nabla
    _     Id
    _ (PmAltConLike (RealDataCon DataCon
    dc))
      | DataCon -> Bool
    isNewDataCon DataCon
    dc = MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    forall a. MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero -- (3) in Note [Coverage checking Newtype matches]
    addNotConCt Nabla
    nabla Id
    x PmAltCon
    nalt = do
      (mb_mark_dirty, nabla') <- (VarInfo
     -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Maybe Id, VarInfo))
    -> Nabla
    -> Id
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Maybe Id, Nabla)
    forall (f :: * -> *) a.
    Functor f =>
    (VarInfo -> f (a, VarInfo)) -> Nabla -> Id -> f (a, Nabla)
    trvVarInfo VarInfo
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Maybe Id, VarInfo)
    go Nabla
    nabla Id
    x
      pure $ case mb_mark_dirty of
        Just Id
    x  -> Id -> Nabla -> Nabla
    markDirty Id
    x Nabla
    nabla'
        Maybe Id
    Nothing -> Nabla
    nabla'
      where
        -- Update `x`'s 'VarInfo' entry. Fail ('MaybeT') if contradiction,
        -- otherwise return updated entry and `Just x'` if `x` should be marked dirty,
        -- where `x'` is the representative of `x`.
        go :: VarInfo -> MaybeT DsM (Maybe Id, VarInfo)
        go :: VarInfo
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Maybe Id, VarInfo)
    go vi :: VarInfo
    vi@(VI Id
    x' [PmAltConApp]
    pos PmAltConSet
    neg BotInfo
    _ ResidualCompleteMatches
    rcm) = do
          -- 1. Bail out quickly when nalt contradicts a solution
          let contradicts :: PmAltCon -> PmAltConApp -> Bool
    contradicts PmAltCon
    nalt PmAltConApp
    sol = PmAltCon -> PmAltCon -> PmEquality
    eqPmAltCon (PmAltConApp -> PmAltCon
    paca_con PmAltConApp
    sol) PmAltCon
    nalt PmEquality -> PmEquality -> Bool
    forall a. Eq a => a -> a -> Bool
    == PmEquality
    Equal
          Bool -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> Bool
    not ((PmAltConApp -> Bool) -> [PmAltConApp] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (PmAltCon -> PmAltConApp -> Bool
    contradicts PmAltCon
    nalt) [PmAltConApp]
    pos))
          -- 2. Only record the new fact when it's not already implied by one of the
          -- solutions
          let implies :: PmAltCon -> PmAltConApp -> Bool
    implies PmAltCon
    nalt PmAltConApp
    sol = PmAltCon -> PmAltCon -> PmEquality
    eqPmAltCon (PmAltConApp -> PmAltCon
    paca_con PmAltConApp
    sol) PmAltCon
    nalt PmEquality -> PmEquality -> Bool
    forall a. Eq a => a -> a -> Bool
    == PmEquality
    Disjoint
          let neg' :: PmAltConSet
    neg'
                | (PmAltConApp -> Bool) -> [PmAltConApp] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (PmAltCon -> PmAltConApp -> Bool
    implies PmAltCon
    nalt) [PmAltConApp]
    pos = PmAltConSet
    neg
                -- See Note [Completeness checking with required Thetas]
                | PmAltCon -> Bool
    hasRequiredTheta PmAltCon
    nalt  = PmAltConSet
    neg
                | Bool
    otherwise              = PmAltConSet -> PmAltCon -> PmAltConSet
    extendPmAltConSet PmAltConSet
    neg PmAltCon
    nalt
          Bool -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) ()
    forall (m :: * -> *). (HasCallStack, Applicative m) => Bool -> m ()
    massert (PmAltCon -> Bool
    isPmAltConMatchStrict PmAltCon
    nalt)
          let vi' :: VarInfo
    vi' = VarInfo
    vi{ vi_neg = neg', vi_bot = IsNotBot }
          -- 3. Make sure there's at least one other possible constructor
          mb_rcm' <- DsM (Maybe ResidualCompleteMatches)
    -> MaybeT
         (IOEnv (Env DsGblEnv DsLclEnv)) (Maybe ResidualCompleteMatches)
    forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (PmAltCon
    -> ResidualCompleteMatches -> DsM (Maybe ResidualCompleteMatches)
    markMatched PmAltCon
    nalt ResidualCompleteMatches
    rcm)
          pure $ case mb_rcm' of
            -- If nalt could be removed from a COMPLETE set, we'll get back Just and
            -- have to mark x dirty, by returning Just x'.
            Just ResidualCompleteMatches
    rcm' -> (Id -> Maybe Id
    forall a. a -> Maybe a
    Just Id
    x',  VarInfo
    vi'{ vi_rcm = rcm' })
            -- Otherwise, nalt didn't occur in any residual COMPLETE set and we
            -- don't have to mark it dirty. So we return Nothing, which in the case
            -- above would have compromised precision.
            -- See Note [Shortcutting the inhabitation test], grep for T17836.
            Maybe ResidualCompleteMatches
    Nothing   -> (Maybe Id
    forall a. Maybe a
    Nothing, VarInfo
    vi')

    hasRequiredTheta :: PmAltCon -> Bool
    hasRequiredTheta :: PmAltCon -> Bool
    hasRequiredTheta (PmAltConLike ConLike
    cl) = ThetaType -> Bool
    forall (f :: * -> *) a. Foldable f => f a -> Bool
    notNull ThetaType
    req_theta
      where
        ([Id]
    _,[Id]
    _,[EqSpec]
    _,ThetaType
    _,ThetaType
    req_theta,[Scaled Type]
    _,Type
    _) = ConLike
    -> ([Id], [Id], [EqSpec], ThetaType, ThetaType, [Scaled Type],
        Type)
    conLikeFullSig ConLike
    cl
    hasRequiredTheta PmAltCon
    _                 = Bool
    False

    -- | Add a @x ~ K tvs args ts@ constraint.
    -- @addConCt x K tvs args ts@ extends the substitution with a solution
    -- @x :-> (K, tvs, args)@ if compatible with the negative and positive info we
    -- have on @x@, reject (@Nothing@) otherwise.
    --
    -- See Note [TmState invariants].
    addConCt :: Nabla -> Id -> PmAltCon -> [TyVar] -> [Id] -> MaybeT DsM Nabla
    addConCt :: Nabla
    -> Id
    -> PmAltCon
    -> [Id]
    -> [Id]
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    addConCt nabla :: Nabla
    nabla@MkNabla{ nabla_tm_st :: Nabla -> TmState
    nabla_tm_st = ts :: TmState
    ts@TmSt{ ts_facts :: TmState -> UniqSDFM Id VarInfo
    ts_facts=UniqSDFM Id VarInfo
    env } } Id
    x PmAltCon
    alt [Id]
    tvs [Id]
    args = do
      let vi :: VarInfo
    vi@(VI Id
    _ [PmAltConApp]
    pos PmAltConSet
    neg BotInfo
    bot ResidualCompleteMatches
    _) = TmState -> Id -> VarInfo
    lookupVarInfo TmState
    ts Id
    x
      -- First try to refute with a negative fact
      Bool -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> Bool
    not (PmAltCon -> PmAltConSet -> Bool
    elemPmAltConSet PmAltCon
    alt PmAltConSet
    neg))
      -- Then see if any of the other solutions (remember: each of them is an
      -- additional refinement of the possible values x could take) indicate a
      -- contradiction
      Bool -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard ((PmAltConApp -> Bool) -> [PmAltConApp] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all ((PmEquality -> PmEquality -> Bool
    forall a. Eq a => a -> a -> Bool
    /= PmEquality
    Disjoint) (PmEquality -> Bool)
    -> (PmAltConApp -> PmEquality) -> PmAltConApp -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PmAltCon -> PmAltCon -> PmEquality
    eqPmAltCon PmAltCon
    alt (PmAltCon -> PmEquality)
    -> (PmAltConApp -> PmAltCon) -> PmAltConApp -> PmEquality
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PmAltConApp -> PmAltCon
    paca_con) [PmAltConApp]
    pos)
      -- Now we should be good! Add (alt, tvs, args) as a possible solution, or
      -- refine an existing one
      case (PmAltConApp -> Bool) -> [PmAltConApp] -> Maybe PmAltConApp
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    find ((PmEquality -> PmEquality -> Bool
    forall a. Eq a => a -> a -> Bool
    == PmEquality
    Equal) (PmEquality -> Bool)
    -> (PmAltConApp -> PmEquality) -> PmAltConApp -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PmAltCon -> PmAltCon -> PmEquality
    eqPmAltCon PmAltCon
    alt (PmAltCon -> PmEquality)
    -> (PmAltConApp -> PmAltCon) -> PmAltConApp -> PmEquality
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PmAltConApp -> PmAltCon
    paca_con) [PmAltConApp]
    pos of
        Just (PACA PmAltCon
    _con [Id]
    other_tvs [Id]
    other_args) -> do
          -- We must unify existentially bound ty vars and arguments!
          let ty_cts :: [PhiCt]
    ty_cts = ThetaType -> ThetaType -> [PhiCt]
    equateTys ((Id -> Type) -> [Id] -> ThetaType
    forall a b. (a -> b) -> [a] -> [b]
    map Id -> Type
    mkTyVarTy [Id]
    tvs) ((Id -> Type) -> [Id] -> ThetaType
    forall a b. (a -> b) -> [a] -> [b]
    map Id -> Type
    mkTyVarTy [Id]
    other_tvs)
          nabla' <- IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
     -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla)
    -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    forall a b. (a -> b) -> a -> b
    $ Nabla -> PhiCts -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
    addPhiCts Nabla
    nabla ([PhiCt] -> PhiCts
    forall a. [a] -> Bag a
    listToBag [PhiCt]
    ty_cts)
          let add_var_ct Nabla
    nabla (Id
    a, Id
    b) = Nabla -> Id -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    addVarCt Nabla
    nabla Id
    a Id
    b
          foldlM add_var_ct nabla' $ zipEqual "addConCt" args other_args
        Maybe PmAltConApp
    Nothing -> do
          let pos' :: [PmAltConApp]
    pos' = PmAltCon -> [Id] -> [Id] -> PmAltConApp
    PACA PmAltCon
    alt [Id]
    tvs [Id]
    args PmAltConApp -> [PmAltConApp] -> [PmAltConApp]
    forall a. a -> [a] -> [a]
    : [PmAltConApp]
    pos
          let nabla_with :: BotInfo -> Nabla
    nabla_with BotInfo
    bot' =
                Nabla
    nabla{ nabla_tm_st = ts{ts_facts = addToUSDFM env x (vi{vi_pos = pos', vi_bot = bot'})} }
          -- Do (2) in Note [Coverage checking Newtype matches]
          case (PmAltCon
    alt, [Id]
    args) of
            (PmAltConLike (RealDataCon DataCon
    dc), [Id
    y]) | DataCon -> Bool
    isNewDataCon DataCon
    dc ->
              case BotInfo
    bot of
                BotInfo
    MaybeBot -> Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BotInfo -> Nabla
    nabla_with BotInfo
    MaybeBot)
                BotInfo
    IsBot    -> Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    addBotCt (BotInfo -> Nabla
    nabla_with BotInfo
    MaybeBot) Id
    y
                BotInfo
    IsNotBot -> Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    addNotBotCt (BotInfo -> Nabla
    nabla_with BotInfo
    MaybeBot) Id
    y
            (PmAltCon, [Id])
    _ -> Bool
    -> (Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla)
    -> Nabla
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    forall a. HasCallStack => Bool -> a -> a
    assert (PmAltCon -> Bool
    isPmAltConMatchStrict PmAltCon
    alt )
                 Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BotInfo -> Nabla
    nabla_with BotInfo
    IsNotBot) -- strict match ==> not ⊥

    equateTys :: [Type] -> [Type] -> [PhiCt]
    equateTys :: ThetaType -> ThetaType -> [PhiCt]
    equateTys ThetaType
    ts ThetaType
    us =
      [ Type -> PhiCt
    PhiTyCt (Type -> Type -> Type
    mkPrimEqPred Type
    t Type
    u)
      | (Type
    t, Type
    u) <- String -> ThetaType -> ThetaType -> [(Type, Type)]
    forall a b. HasDebugCallStack => String -> [a] -> [b] -> [(a, b)]
    zipEqual String
    "equateTys" ThetaType
    ts ThetaType
    us
      -- The following line filters out trivial Refl constraints, so that we don't
      -- need to initialise the type oracle that often
      , Bool -> Bool
    not (Type -> Type -> Bool
    eqType Type
    t Type
    u)
      ]

    -- | Adds a @x ~ y@ constraint by merging the two 'VarInfo's and record the
    -- gained knowledge in 'Nabla'.
    --
    -- Returns @Nothing@ when there's a contradiction while merging. Returns @Just
    -- nabla@ when the constraint was compatible with prior facts, in which case
    -- @nabla@ has integrated the knowledge from the equality constraint.
    --
    -- See Note [TmState invariants].
    addVarCt :: Nabla -> Id -> Id -> MaybeT DsM Nabla
    addVarCt :: Nabla -> Id -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    addVarCt nabla :: Nabla
    nabla@MkNabla{ nabla_tm_st :: Nabla -> TmState
    nabla_tm_st = ts :: TmState
    ts@TmSt{ ts_facts :: TmState -> UniqSDFM Id VarInfo
    ts_facts = UniqSDFM Id VarInfo
    env } } Id
    x Id
    y =
      case UniqSDFM Id VarInfo
    -> Id -> Id -> (Maybe VarInfo, UniqSDFM Id VarInfo)
    forall key ele.
    Uniquable key =>
    UniqSDFM key ele -> key -> key -> (Maybe ele, UniqSDFM key ele)
    equateUSDFM UniqSDFM Id VarInfo
    env Id
    x Id
    y of
        (Maybe VarInfo
    Nothing,   UniqSDFM Id VarInfo
    env') -> Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Nabla
    nabla{ nabla_tm_st = ts{ ts_facts = env' } })
        -- Add the constraints we had for x to y
        (Just VarInfo
    vi_x, UniqSDFM Id VarInfo
    env') -> do
          let nabla_equated :: Nabla
    nabla_equated = Nabla
    nabla{ nabla_tm_st = ts{ts_facts = env'} }
          -- and then gradually merge every positive fact we have on x into y
          let add_pos :: Nabla
    -> PmAltConApp -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    add_pos Nabla
    nabla (PACA PmAltCon
    cl [Id]
    tvs [Id]
    args) = Nabla
    -> Id
    -> PmAltCon
    -> [Id]
    -> [Id]
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    addConCt Nabla
    nabla Id
    y PmAltCon
    cl [Id]
    tvs [Id]
    args
          nabla_pos <- (Nabla
     -> PmAltConApp -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla)
    -> Nabla
    -> [PmAltConApp]
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldlM Nabla
    -> PmAltConApp -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    add_pos Nabla
    nabla_equated (VarInfo -> [PmAltConApp]
    vi_pos VarInfo
    vi_x)
          -- Do the same for negative info
          let add_neg Nabla
    nabla PmAltCon
    nalt = Nabla
    -> Id -> PmAltCon -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    addNotConCt Nabla
    nabla Id
    y PmAltCon
    nalt
          foldlM add_neg nabla_pos (pmAltConSetElems (vi_neg vi_x))

    -- | Inspects a 'PmCoreCt' @let x = e@ by recording constraints for @x@ based
    -- on the shape of the 'CoreExpr' @e@. Examples:
    --
    --   * For @let x = Just (42, 'z')@ we want to record the
    --     constraints @x ~ Just a, a ~ (b, c), b ~ 42, c ~ 'z'@.
    --     See 'data_con_app'.
    --   * For @let x = unpackCString# "tmp"@ we want to record the literal
    --     constraint @x ~ "tmp"@.
    --   * For @let x = I# 42@ we want the literal constraint @x ~ 42@. Similar
    --     for other literals. See 'coreExprAsPmLit'.
    --   * Finally, if we have @let x = e@ and we already have seen @let y = e@, we
    --     want to record @x ~ y@.
    addCoreCt :: Nabla -> Id -> CoreExpr -> MaybeT DsM Nabla
    addCoreCt :: Nabla
    -> Id -> CoreExpr -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    addCoreCt Nabla
    nabla Id
    x CoreExpr
    e = do
      simpl_opts <- DynFlags -> SimpleOpts
    initSimpleOpts (DynFlags -> SimpleOpts)
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) DynFlags
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) SimpleOpts
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) DynFlags
    forall (m :: * -> *). HasDynFlags m => m DynFlags
    getDynFlags
      let e' = HasDebugCallStack => SimpleOpts -> CoreExpr -> CoreExpr
    SimpleOpts -> CoreExpr -> CoreExpr
    simpleOptExpr SimpleOpts
    simpl_opts CoreExpr
    e
      -- lift $ tracePm "addCoreCt" (ppr x <+> dcolon <+> ppr (idType x) $$ ppr e $$ ppr e')
      execStateT (core_expr x e') nabla
      where
        -- Takes apart a 'CoreExpr' and tries to extract as much information about
        -- literals and constructor applications as possible.
        core_expr :: Id -> CoreExpr -> StateT Nabla (MaybeT DsM) ()
        -- TODO: Handle newtypes properly, by wrapping the expression in a DataCon
        -- This is the right thing for casts involving data family instances and
        -- their representation TyCon, though (which are not visible in source
        -- syntax). See Note [COMPLETE sets on data families]
        -- core_expr x e | pprTrace "core_expr" (ppr x $$ ppr e) False = undefined
        core_expr :: Id
    -> CoreExpr
    -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
    core_expr Id
    x (Cast CoreExpr
    e Coercion
    _co) = Id
    -> CoreExpr
    -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
    core_expr Id
    x CoreExpr
    e
        core_expr Id
    x (Tick CoreTickish
    _t CoreExpr
    e) = Id
    -> CoreExpr
    -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
    core_expr Id
    x CoreExpr
    e
        core_expr Id
    x CoreExpr
    e
          | Just (PmLit -> Maybe FastString
    pmLitAsStringLit -> Just FastString
    s) <- CoreExpr -> Maybe PmLit
    coreExprAsPmLit CoreExpr
    e
          , Type
    expr_ty Type -> Type -> Bool
    `eqType` Type
    stringTy
          -- See Note [Representation of Strings in TmState]
          = case FastString -> String
    unpackFS FastString
    s of
              -- We need this special case to break a loop with coreExprAsPmLit
              -- Otherwise we alternate endlessly between [] and ""
              [] -> Id
    -> InScopeSet
    -> DataCon
    -> [CoreExpr]
    -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
    data_con_app Id
    x InScopeSet
    emptyInScopeSet DataCon
    nilDataCon []
              String
    s' -> Id
    -> CoreExpr
    -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
    core_expr Id
    x (Type -> [CoreExpr] -> CoreExpr
    mkListExpr Type
    charTy ((Char -> CoreExpr) -> String -> [CoreExpr]
    forall a b. (a -> b) -> [a] -> [b]
    map Char -> CoreExpr
    mkCharExpr String
    s'))
          | Just PmLit
    lit <- CoreExpr -> Maybe PmLit
    coreExprAsPmLit CoreExpr
    e
          = Id
    -> PmLit
    -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
    pm_lit Id
    x PmLit
    lit
          | Just (InScopeSet
    in_scope, _empty_floats :: [FloatBind]
    _empty_floats@[], DataCon
    dc, ThetaType
    _arg_tys, [CoreExpr]
    args)
                <- HasDebugCallStack =>
    InScopeEnv
    -> CoreExpr
    -> Maybe (InScopeSet, [FloatBind], DataCon, ThetaType, [CoreExpr])
    InScopeEnv
    -> CoreExpr
    -> Maybe (InScopeSet, [FloatBind], DataCon, ThetaType, [CoreExpr])
    exprIsConApp_maybe InScopeEnv
    in_scope_env CoreExpr
    e
          = Id
    -> InScopeSet
    -> DataCon
    -> [CoreExpr]
    -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
    data_con_app Id
    x InScopeSet
    in_scope DataCon
    dc [CoreExpr]
    args
          -- See Note [Detecting pattern synonym applications in expressions]
          | Var Id
    y <- CoreExpr
    e, Maybe DataCon
    Nothing <- Id -> Maybe DataCon
    isDataConId_maybe Id
    x
          -- We don't consider DataCons flexible variables
          = (Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla)
    -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
    forall (m :: * -> *) s. Monad m => (s -> m s) -> StateT s m ()
    modifyT (\Nabla
    nabla -> Nabla -> Id -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    addVarCt Nabla
    nabla Id
    x Id
    y)
          | Bool
    otherwise
          -- Any other expression. Try to find other uses of a semantically
          -- equivalent expression and represent them by the same variable!
          = Id
    -> CoreExpr
    -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
    equate_with_similar_expr Id
    x CoreExpr
    e
          where
            expr_ty :: Type
    expr_ty       = HasDebugCallStack => CoreExpr -> Type
    CoreExpr -> Type
    exprType CoreExpr
    e
            expr_in_scope :: InScopeSet
    expr_in_scope = VarSet -> InScopeSet
    mkInScopeSet (CoreExpr -> VarSet
    exprFreeVars CoreExpr
    e)
            in_scope_env :: InScopeEnv
    in_scope_env  = InScopeSet -> IdUnfoldingFun -> InScopeEnv
    ISE InScopeSet
    expr_in_scope IdUnfoldingFun
    noUnfoldingFun
            -- It's inconvenient to get hold of a global in-scope set
            -- here, but it'll only be needed if exprIsConApp_maybe ends
            -- up substituting inside a forall or lambda (i.e. seldom)
            -- so using exprFreeVars seems fine.   See MR !1647.

        -- The @e@ in @let x = e@ had no familiar form. But we can still see if
        -- see if we already encountered a constraint @let y = e'@ with @e'@
        -- semantically equivalent to @e@, in which case we may add the constraint
        -- @x ~ y@.
        equate_with_similar_expr :: Id -> CoreExpr -> StateT Nabla (MaybeT DsM) ()
        equate_with_similar_expr :: Id
    -> CoreExpr
    -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
    equate_with_similar_expr Id
    x CoreExpr
    e = do
          rep <- (Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Nabla))
    -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) Id
    forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
    StateT ((Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Nabla))
     -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) Id)
    -> (Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Nabla))
    -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) Id
    forall a b. (a -> b) -> a -> b
    $ \Nabla
    nabla -> DsM (Id, Nabla)
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Nabla)
    forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (Nabla -> CoreExpr -> DsM (Id, Nabla)
    representCoreExpr Nabla
    nabla CoreExpr
    e)
          -- Note that @rep == x@ if we encountered @e@ for the first time.
          modifyT (\Nabla
    nabla -> Nabla -> Id -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    addVarCt Nabla
    nabla Id
    x Id
    rep)

        bind_expr :: CoreExpr -> StateT Nabla (MaybeT DsM) Id
        bind_expr :: CoreExpr
    -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) Id
    bind_expr CoreExpr
    e = do
          x <- MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Id
    -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) Id
    forall (m :: * -> *) a. Monad m => m a -> StateT Nabla m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (IOEnv (Env DsGblEnv DsLclEnv) Id
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Id
    forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (Type -> IOEnv (Env DsGblEnv DsLclEnv) Id
    mkPmId (HasDebugCallStack => CoreExpr -> Type
    CoreExpr -> Type
    exprType CoreExpr
    e)))
          core_expr x e
          pure x

        -- Look at @let x = K taus theta es@ and generate the following
        -- constraints (assuming universals were dropped from @taus@ before):
        --   1. @x ≁ ⊥@ if 'K' is not a Newtype constructor.
        --   2. @a_1 ~ tau_1, ..., a_n ~ tau_n@ for fresh @a_i@
        --   3. @y_1 ~ e_1, ..., y_m ~ e_m@ for fresh @y_i@
        --   4. @x ~ K as ys@
        -- This is quite similar to PmCheck.pmConCts.
        data_con_app :: Id -> InScopeSet -> DataCon -> [CoreExpr] -> StateT Nabla (MaybeT DsM) ()
        data_con_app :: Id
    -> InScopeSet
    -> DataCon
    -> [CoreExpr]
    -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
    data_con_app Id
    x InScopeSet
    in_scope DataCon
    dc [CoreExpr]
    args = do
          let dc_ex_tvs :: [Id]
    dc_ex_tvs              = DataCon -> [Id]
    dataConExTyCoVars DataCon
    dc
              arty :: Int
    arty                   = DataCon -> Int
    dataConSourceArity DataCon
    dc
              ([CoreExpr]
    ex_ty_args, [CoreExpr]
    val_args) = [Id] -> [CoreExpr] -> ([CoreExpr], [CoreExpr])
    forall b a. [b] -> [a] -> ([a], [a])
    splitAtList [Id]
    dc_ex_tvs [CoreExpr]
    args
              ex_tys :: ThetaType
    ex_tys                 = (CoreExpr -> Type) -> [CoreExpr] -> ThetaType
    forall a b. (a -> b) -> [a] -> [b]
    map CoreExpr -> Type
    exprToType [CoreExpr]
    ex_ty_args
              vis_args :: [CoreExpr]
    vis_args               = [CoreExpr] -> [CoreExpr]
    forall a. [a] -> [a]
    reverse ([CoreExpr] -> [CoreExpr]) -> [CoreExpr] -> [CoreExpr]
    forall a b. (a -> b) -> a -> b
    $ Int -> [CoreExpr] -> [CoreExpr]
    forall a. Int -> [a] -> [a]
    take Int
    arty ([CoreExpr] -> [CoreExpr]) -> [CoreExpr] -> [CoreExpr]
    forall a b. (a -> b) -> a -> b
    $ [CoreExpr] -> [CoreExpr]
    forall a. [a] -> [a]
    reverse [CoreExpr]
    val_args
          uniq_supply <- MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) UniqSupply
    -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) UniqSupply
    forall (m :: * -> *) a. Monad m => m a -> StateT Nabla m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) UniqSupply
     -> StateT
          Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) UniqSupply)
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) UniqSupply
    -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) UniqSupply
    forall a b. (a -> b) -> a -> b
    $ DsM UniqSupply -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) UniqSupply
    forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (DsM UniqSupply
     -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) UniqSupply)
    -> DsM UniqSupply
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) UniqSupply
    forall a b. (a -> b) -> a -> b
    $ DsM UniqSupply
    forall (m :: * -> *). MonadUnique m => m UniqSupply
    getUniqueSupplyM
          let (_, ex_tvs) = cloneTyVarBndrs (mkEmptySubst in_scope) dc_ex_tvs uniq_supply
              ty_cts      = ThetaType -> ThetaType -> [PhiCt]
    equateTys ((Id -> Type) -> [Id] -> ThetaType
    forall a b. (a -> b) -> [a] -> [b]
    map Id -> Type
    mkTyVarTy [Id]
    ex_tvs) ThetaType
    ex_tys
          -- 1. @x ≁ ⊥@ if 'K' is not a Newtype constructor (#18341)
          when (not (isNewDataCon dc)) $
            modifyT $ \Nabla
    nabla -> Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    addNotBotCt Nabla
    nabla Id
    x
          -- 2. @a_1 ~ tau_1, ..., a_n ~ tau_n@ for fresh @a_i@. See also #17703
          modifyT $ \Nabla
    nabla -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
     -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla)
    -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    forall a b. (a -> b) -> a -> b
    $ Nabla -> PhiCts -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
    addPhiCts Nabla
    nabla ([PhiCt] -> PhiCts
    forall a. [a] -> Bag a
    listToBag [PhiCt]
    ty_cts)
          -- 3. @y_1 ~ e_1, ..., y_m ~ e_m@ for fresh @y_i@
          arg_ids <- traverse bind_expr vis_args
          -- 4. @x ~ K as ys@
          pm_alt_con_app x (PmAltConLike (RealDataCon dc)) ex_tvs arg_ids

        -- Adds a literal constraint, i.e. @x ~ 42@.
        -- Also we assume that literal expressions won't diverge, so this
        -- will add a @x ~/ ⊥@ constraint.
        pm_lit :: Id -> PmLit -> StateT Nabla (MaybeT DsM) ()
        pm_lit :: Id
    -> PmLit
    -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
    pm_lit Id
    x PmLit
    lit = do
          (Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla)
    -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
    forall (m :: * -> *) s. Monad m => (s -> m s) -> StateT s m ()
    modifyT ((Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla)
     -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ())
    -> (Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla)
    -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
    forall a b. (a -> b) -> a -> b
    $ \Nabla
    nabla -> Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    addNotBotCt Nabla
    nabla Id
    x
          Id
    -> PmAltCon
    -> [Id]
    -> [Id]
    -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
    pm_alt_con_app Id
    x (PmLit -> PmAltCon
    PmAltLit PmLit
    lit) [] []

        -- Adds the given constructor application as a solution for @x@.
        pm_alt_con_app :: Id -> PmAltCon -> [TyVar] -> [Id] -> StateT Nabla (MaybeT DsM) ()
        pm_alt_con_app :: Id
    -> PmAltCon
    -> [Id]
    -> [Id]
    -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
    pm_alt_con_app Id
    x PmAltCon
    con [Id]
    tvs [Id]
    args = (Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla)
    -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
    forall (m :: * -> *) s. Monad m => (s -> m s) -> StateT s m ()
    modifyT ((Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla)
     -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ())
    -> (Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla)
    -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
    forall a b. (a -> b) -> a -> b
    $ \Nabla
    nabla -> Nabla
    -> Id
    -> PmAltCon
    -> [Id]
    -> [Id]
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    addConCt Nabla
    nabla Id
    x PmAltCon
    con [Id]
    tvs [Id]
    args

    -- | Like 'modify', but with an effectful modifier action
    modifyT :: Monad m => (s -> m s) -> StateT s m ()
    modifyT :: forall (m :: * -> *) s. Monad m => (s -> m s) -> StateT s m ()
    modifyT s -> m s
    f = (s -> m ((), s)) -> StateT s m ()
    forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
    StateT ((s -> m ((), s)) -> StateT s m ())
    -> (s -> m ((), s)) -> StateT s m ()
    forall a b. (a -> b) -> a -> b
    $ (s -> ((), s)) -> m s -> m ((), s)
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((,) ()) (m s -> m ((), s)) -> (s -> m s) -> s -> m ((), s)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . s -> m s
    f

    -- | Finds a representant of the semantic equality class of the given @e@.
    -- Which is the @x@ of a @let x = e'@ constraint (with @e@ semantically
    -- equivalent to @e'@) we encountered earlier, or a fresh identifier if
    -- there weren't any such constraints.
    representCoreExpr :: Nabla -> CoreExpr -> DsM (Id, Nabla)
    representCoreExpr :: Nabla -> CoreExpr -> DsM (Id, Nabla)
    representCoreExpr nabla :: Nabla
    nabla@MkNabla{ nabla_tm_st :: Nabla -> TmState
    nabla_tm_st = ts :: TmState
    ts@TmSt{ ts_reps :: TmState -> CoreMap Id
    ts_reps = CoreMap Id
    reps } } CoreExpr
    e
      | Just Id
    rep <- CoreMap Id -> CoreExpr -> Maybe Id
    forall a. CoreMap a -> CoreExpr -> Maybe a
    lookupCoreMap CoreMap Id
    reps CoreExpr
    key = (Id, Nabla) -> DsM (Id, Nabla)
    forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Id
    rep, Nabla
    nabla)
      | Bool
    otherwise = do
          rep <- Type -> IOEnv (Env DsGblEnv DsLclEnv) Id
    mkPmId (HasDebugCallStack => CoreExpr -> Type
    CoreExpr -> Type
    exprType CoreExpr
    e)
          let reps'  = CoreMap Id -> CoreExpr -> Id -> CoreMap Id
    forall a. CoreMap a -> CoreExpr -> a -> CoreMap a
    extendCoreMap CoreMap Id
    reps CoreExpr
    key Id
    rep
          let nabla' = Nabla
    nabla{ nabla_tm_st = ts{ ts_reps = reps' } }
          pure (rep, nabla')
      where
        key :: CoreExpr
    key = CoreExpr -> CoreExpr
    makeDictsCoherent CoreExpr
    e
          -- Use a key in which dictionaries for the same type become equal.
          -- See Note [Unique dictionaries in the TmOracle CoreMap]

    -- | Change out 'Id's which are uniquely determined by their type to a
    -- common value, so that different names for dictionaries of the same type
    -- are considered equal when building a 'CoreMap'.
    --
    -- See Note [Unique dictionaries in the TmOracle CoreMap]
    makeDictsCoherent :: CoreExpr -> CoreExpr
    makeDictsCoherent :: CoreExpr -> CoreExpr
    makeDictsCoherent var :: CoreExpr
    var@(Var Id
    v)
      | let ty :: Type
    ty = Id -> Type
    idType Id
    v
      , Type -> Bool
    typeDeterminesValue Type
    ty
      = Type -> String -> CoreExpr
    mkImpossibleExpr Type
    ty String
    "Solver.makeDictsCoherent"
      | Bool
    otherwise
      = CoreExpr
    var
    makeDictsCoherent lit :: CoreExpr
    lit@(Lit {})
      = CoreExpr
    lit
    makeDictsCoherent (App CoreExpr
    f CoreExpr
    a)
      = CoreExpr -> CoreExpr -> CoreExpr
    forall b. Expr b -> Expr b -> Expr b
    App (CoreExpr -> CoreExpr
    makeDictsCoherent CoreExpr
    f) (CoreExpr -> CoreExpr
    makeDictsCoherent CoreExpr
    a)
    makeDictsCoherent (Lam Id
    f CoreExpr
    body)
      = Id -> CoreExpr -> CoreExpr
    forall b. b -> Expr b -> Expr b
    Lam Id
    f (CoreExpr -> CoreExpr
    makeDictsCoherent CoreExpr
    body)
    makeDictsCoherent (Let Bind Id
    bndr CoreExpr
    body)
      = Bind Id -> CoreExpr -> CoreExpr
    forall b. Bind b -> Expr b -> Expr b
    Let
          (Bind Id -> Bind Id
    go_bndr Bind Id
    bndr)
          (CoreExpr -> CoreExpr
    makeDictsCoherent CoreExpr
    body)
      where
        go_bndr :: Bind Id -> Bind Id
    go_bndr (NonRec Id
    bndr CoreExpr
    expr) = Id -> CoreExpr -> Bind Id
    forall b. b -> Expr b -> Bind b
    NonRec Id
    bndr (CoreExpr -> CoreExpr
    makeDictsCoherent CoreExpr
    expr)
        go_bndr (Rec [(Id, CoreExpr)]
    bndrs) = [(Id, CoreExpr)] -> Bind Id
    forall b. [(b, Expr b)] -> Bind b
    Rec (((Id, CoreExpr) -> (Id, CoreExpr))
    -> [(Id, CoreExpr)] -> [(Id, CoreExpr)]
    forall a b. (a -> b) -> [a] -> [b]
    map ( \(Id
    b, CoreExpr
    expr) -> (Id
    b, CoreExpr -> CoreExpr
    makeDictsCoherent CoreExpr
    expr) ) [(Id, CoreExpr)]
    bndrs)
    makeDictsCoherent (Case CoreExpr
    scrut Id
    bndr Type
    ty [Alt Id]
    alts)
      = CoreExpr -> Id -> Type -> [Alt Id] -> CoreExpr
    forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
    Case CoreExpr
    scrut Id
    bndr Type
    ty
          [ AltCon -> [Id] -> CoreExpr -> Alt Id
    forall b. AltCon -> [b] -> Expr b -> Alt b
    Alt AltCon
    con [Id]
    bndr CoreExpr
    expr'
          | Alt AltCon
    con [Id]
    bndr CoreExpr
    expr <- [Alt Id]
    alts
          , let expr' :: CoreExpr
    expr' = CoreExpr -> CoreExpr
    makeDictsCoherent CoreExpr
    expr ]
    makeDictsCoherent (Cast CoreExpr
    expr Coercion
    co)
      = CoreExpr -> Coercion -> CoreExpr
    forall b. Expr b -> Coercion -> Expr b
    Cast (CoreExpr -> CoreExpr
    makeDictsCoherent CoreExpr
    expr) Coercion
    co
    makeDictsCoherent (Tick CoreTickish
    tick CoreExpr
    expr)
      = CoreTickish -> CoreExpr -> CoreExpr
    forall b. CoreTickish -> Expr b -> Expr b
    Tick CoreTickish
    tick (CoreExpr -> CoreExpr
    makeDictsCoherent CoreExpr
    expr)
    makeDictsCoherent ty :: CoreExpr
    ty@(Type {})
      = CoreExpr
    ty
    makeDictsCoherent co :: CoreExpr
    co@(Coercion {})
      = CoreExpr
    co

    {- Note [Unique dictionaries in the TmOracle CoreMap]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Any two dictionaries for a coherent typeclass should be considered equal
    in the TmOracle CoreMap, as this allows us to report better pattern-match
    warnings.

    Consider for example T21662:

      view_fn :: forall (n :: Nat). KnownNat n => Int -> Bool

      foo :: Int -> Int
      foo (view_fn @12 -> True ) = 0
      foo (view_fn @12 -> False) = 1

    In this example, the pattern match is exhaustive because we have covered
    the range of the view pattern function. However, we may fail to recognise
    the fact that the two cases use the same view function if the KnownNat
    dictionaries aren't syntactically equal:

      eqn 1: [let ds_d1p0 = view_fn @12 $dKnownNat_a1ny ds_d1oR,  True <- ds_d1p0]
      eqn 2: [let ds_d1p6 = view_fn @12 $dKnownNat_a1nC ds_d1oR, False <- ds_d1p6]

    Note that the uniques of the KnownNat 12 dictionary differ. If we fail to utilise
    the coherence of the KnownNat constraint, then we have to pessimistically assume
    that we have two function calls with different arguments:

      foo (fn arg1 -> True ) = ...
      foo (fn arg2 -> False) = ...

    In this case we can't determine whether the pattern matches are complete, so we
    emit a pattern match warning.

    Solution: replace all 'Id's whose type uniquely determines its value with
    a common value, e.g. in the above example we would replace both
    $dKnownNat_a1ny and $dKnownNat_a1nC with error @(KnownNat 12).

    Why did we choose this solution? Here are some alternatives that were considered:

      1. Perform CSE first. This would common up the dictionaries before we compare
         using the CoreMap.
         However, this is architecturally difficult as it would require threading
         a CSEnv through to desugarPat.
      2. Directly modify CoreMap so that any two dictionaries of the same type are
         considered equal.
         The problem is that this affects all users of CoreMap. For example, CSE
         would now assume that any two dictionaries of the same type are equal,
         but this isn't necessarily true in the presence of magicDict, which
         violates coherence by design. It seems more prudent to limit the changes
         to the pattern-match checker only, to avoid undesirable consequences.

    In the end, replacing dictionaries with an error value in the pattern-match
    checker was the most self-contained, although we might want to revisit once
    we implement a more robust approach to computing equality in the pattern-match
    checker (see #19272).
    -}

    {- Note [The Pos/Neg invariant]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Invariant applying to each VarInfo: Whenever we have @C @tvs args@ in 'vi_pos',
    any entry in 'vi_neg' must be incomparable to C (return Nothing) according to
    'eqPmAltCons'. Those entries that are comparable either lead to a refutation
    or are redundant. Examples:
    * @x ~ Just y@, @x ≁ [Just]@. 'eqPmAltCon' returns @Equal@, so refute.
    * @x ~ Nothing@, @x ≁ [Just]@. 'eqPmAltCon' returns @Disjoint@, so negative
      info is redundant and should be discarded.
    * @x ~ I# y@, @x ≁ [4,2]@. 'eqPmAltCon' returns @PossiblyOverlap@, so orthogonal.
      We keep this info in order to be able to refute a redundant match on i.e. 4
      later on.

    This carries over to pattern synonyms and overloaded literals. Say, we have
        pattern Just42 = Just 42
        case Just42 of x
          Nothing -> ()
          Just _  -> ()
    Even though we had a solution for the value abstraction called x here in form
    of a PatSynCon Just42, this solution is incomparable to both Nothing and
    Just. Hence we retain the info in vi_neg, which eventually allows us to detect
    the complete pattern match.

    The Pos/Neg invariant extends to vi_rcm, which essentially stores positive
    information. We make sure that vi_neg and vi_rcm never overlap. This isn't
    strictly necessary since vi_rcm is just a cache, so doesn't need to be
    accurate: Every suggestion of a possible ConLike from vi_rcm might be
    refutable by the type oracle anyway. But it helps to maintain sanity while
    debugging traces.

    Note [Why record both positive and negative info?]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    You might think that knowing positive info (like x ~ Just y) would render
    negative info irrelevant, but not so because of pattern synonyms.  E.g we might
    know that x cannot match (Foo 4), where pattern Foo p = Just p

    Also overloaded literals themselves behave like pattern synonyms. E.g if
    postively we know that (x ~ I# y), we might also negatively want to record that
    x does not match 45 f 45       = e2 f (I# 22#) = e3 f 45       = e4  --
    Overlapped

    Note [TmState invariants]
    ~~~~~~~~~~~~~~~~~~~~~~~~~
    The term oracle state is never obviously (i.e., without consulting the type
    oracle or doing inhabitation testing) contradictory. This implies a few
    invariants:
    * Whenever vi_pos overlaps with vi_neg according to 'eqPmAltCon', we refute.
      This is implied by the Note [The Pos/Neg invariant].
    * Whenever vi_neg subsumes a COMPLETE set, we refute. We consult vi_rcm to
      detect this, but we could just compare whole COMPLETE sets to vi_neg every
      time, if it weren't for performance.

    Maintaining these invariants in 'addVarCt' (the core of the term oracle) and
    'addNotConCt' is subtle.
    * Merging VarInfos. Example: Add the fact @x ~ y@ (see 'equate').
      - (COMPLETE) If we had @x ≁ True@ and @y ≁ False@, then we get
        @x ≁ [True,False]@. This is vacuous by matter of comparing to the built-in
        COMPLETE set, so should refute.
      - (Pos/Neg) If we had @x ≁ True@ and @y ~ True@, we have to refute.
    * Adding positive information. Example: Add the fact @x ~ K ys@ (see 'addConCt')
      - (Neg) If we had @x ≁ K@, refute.
      - (Pos) If we had @x ~ K2@, and that contradicts the new solution according to
        'eqPmAltCon' (ex. K2 is [] and K is (:)), then refute.
      - (Refine) If we had @x ≁ K zs@, unify each y with each z in turn.
    * Adding negative information. Example: Add the fact @x ≁ Nothing@ (see 'addNotConCt')
      - (Refut) If we have @x ~ K ys@, refute.
      - (COMPLETE) If K=Nothing and we had @x ≁ Just@, then we get
        @x ≁ [Just,Nothing]@. This is vacuous by matter of comparing to the built-in
        COMPLETE set, so should refute.

    Note that merging VarInfo in equate can be done by calling out to 'addConCt' and
    'addNotConCt' for each of the facts individually.

    Note [Representation of Strings in TmState]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Instead of treating regular String literals as a PmLits, we treat it as a list
    of characters in the oracle for better overlap reasoning. The following example
    shows why:

      f :: String -> ()
      f ('f':_) = ()
      f "foo"   = ()
      f _       = ()

    The second case is redundant, and we like to warn about it. Therefore either
    the oracle will have to do some smart conversion between the list and literal
    representation or treat is as the list it really is at runtime.

    The "smart conversion" has the advantage of leveraging the more compact literal
    representation wherever possible, but is really nasty to get right with negative
    equalities: Just think of how to encode @x /= "foo"@.
    The "list" option is far simpler, but incurs some overhead in representation and
    warning messages (which can be alleviated by someone with enough dedication).

    Note [Detecting pattern synonym applications in expressions]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    At the moment we fail to detect pattern synonyms in scrutinees and RHS of
    guards. This could be alleviated with considerable effort and complexity, but
    the returns are meager. Consider:

        pattern P
        pattern Q
        case P 15 of
          Q _  -> ...
          P 15 ->

    Compared to the situation where P and Q are DataCons, the lack of generativity
    means we could never flag Q as redundant. (also see Note [Undecidable Equality
    for PmAltCons] in PmTypes.) On the other hand, if we fail to recognise the
    pattern synonym, we flag the pattern match as inexhaustive. That wouldn't happen
    if we had knowledge about the scrutinee, in which case the oracle basically
    knows "If it's a P, then its field is 15".

    This is a pretty narrow use case and I don't think we should to try to fix it
    until a user complains energetically.

    Note [Completeness checking with required Thetas]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Consider the situation in #11224

        import Text.Read (readMaybe)
        pattern PRead :: Read a => () => a -> String
        pattern PRead x <- (readMaybe -> Just x)
        f :: String -> Int
        f (PRead x)  = x
        f (PRead xs) = length xs
        f _          = 0

    Is the first match exhaustive on the PRead synonym? Should the second line thus
    deemed redundant? The answer is, of course, No! The required theta is like a
    hidden parameter which must be supplied at the pattern match site, so PRead
    is much more like a view pattern (where behavior depends on the particular value
    passed in).
    The simple solution here is to forget in 'addNotConCt' that we matched
    on synonyms with a required Theta like @PRead@, so that subsequent matches on
    the same constructor are never flagged as redundant. The consequence is that
    we no longer detect the actually redundant match in

        g :: String -> Int
        g (PRead x) = x
        g (PRead y) = y -- redundant!
        g _         = 0

    But that's a small price to pay, compared to the proper solution here involving
    storing required arguments along with the PmAltConLike in 'vi_neg'.

    Note [Strict fields and variables of unlifted type]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Binders of unlifted type (and strict fields) are unlifted by construction;
    they are conceived with an implicit (but delayed checked) @≁⊥@ constraint to
    begin with. Hence, desugaring in "GHC.HsToCore.Pmc" is entirely unconcerned
    by strict fields, since the forcing happens *before* pattern matching. And
    the φ constructor constraints emitted by 'GHC.HsToCore.Pmc.checkGrd' have
    complex binding semantics (binding type constraints and unlifted fields), so
    unliftedness semantics are entirely confined to the oracle.

    These are the moving parts:

      1.  For each strict (or more generally, unlifted) field @s@ of a 'PhiConCt'
          we have to add a @s ≁ ⊥@ constraint in the corresponding case of
          'addPhiTmCt'. Strict fields are devoid of ⊥ by construction, there's
          nothing that a bang pattern would act on. Example from #18341:

            data T = MkT !Int
            f :: T -> ()
            f (MkT  _) | False = () -- inaccessible
            f (MkT !_) | False = () -- redundant, not only inaccessible!
            f _                = ()

          The second clause desugars to @MkT n <- x, !n@. When coverage checked,
          the 'PmCon' @MkT n <- x@ refines the set of values that reach the bang
          pattern with the φ constraints @MkT n <- x@ (Nothing surprising so far).
          Upon that constraint, it disperses into two lower-level δ constraints
          @x ~ MkT n, n ≁ ⊥@ per Equation (3) in Figure 7 of the paper.

          Checking the 'PmBang' @!n@ will then try to add the
          constraint @n ~ ⊥@ to this set to get the diverging set, which is found
          to be empty. Hence the whole clause is detected as redundant, as
          expected.

      2.  Similarly, when performing the 'inhabitationTest', when instantiating a
          constructor we call 'instCon', which generates a higher-level φ
          constructor constraint.

      3.  The preceding points handle unlifted constructor fields, but there also
          are regular binders of unlifted type. We simply fail in 'addBotCt' for
          any binder of unlifted type.
          It would be enough to check for unliftedness once, when the binder comes
          into scope, but we haven't really a way to track that.

      4.  Why not start an 'emptyVarInfo' of unlifted type with @vi_bot = IsNotBot@?
          Because then we'd need to trigger an inhabitation test, because the var
          might actually be void to begin with. But we can't trigger the test from
          'emptyVarInfo'.
          Historically, that is what we did and not doing the test led to #20631,
          where 'addNotBotCt' trivially succeeded, because the 'VarInfo' already
          said 'IsNotBot', implying that a prior inhabitation test succeeded.
    -}

    -------------------------
    -- * Inhabitation testing
    --
    -- Figure 8 in the LYG paper.

    tyStateRefined :: TyState -> TyState -> Bool
    -- Makes use of the fact that the two TyStates we compare will never have the
    -- same sequence number. It is invalid to call this function when a is not a
    -- refinement of b or vice versa!
    tyStateRefined :: TyState -> TyState -> Bool
    tyStateRefined TyState
    a TyState
    b = TyState -> Int
    ty_st_n TyState
    a Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    /= TyState -> Int
    ty_st_n TyState
    b

    markDirty :: Id -> Nabla -> Nabla
    markDirty :: Id -> Nabla -> Nabla
    markDirty Id
    x nabla :: Nabla
    nabla@MkNabla{nabla_tm_st :: Nabla -> TmState
    nabla_tm_st = ts :: TmState
    ts@TmSt{ts_dirty :: TmState -> DIdSet
    ts_dirty = DIdSet
    dirty} } =
      Nabla
    nabla{ nabla_tm_st = ts{ ts_dirty = extendDVarSet dirty x } }

    traverseDirty :: Monad m => (VarInfo -> m VarInfo) -> TmState -> m TmState
    traverseDirty :: forall (m :: * -> *).
    Monad m =>
    (VarInfo -> m VarInfo) -> TmState -> m TmState
    traverseDirty VarInfo -> m VarInfo
    f ts :: TmState
    ts@TmSt{ts_facts :: TmState -> UniqSDFM Id VarInfo
    ts_facts = UniqSDFM Id VarInfo
    env, ts_dirty :: TmState -> DIdSet
    ts_dirty = DIdSet
    dirty} =
      [Id] -> UniqSDFM Id VarInfo -> m TmState
    go (DIdSet -> [Id]
    forall a. UniqDSet a -> [a]
    uniqDSetToList DIdSet
    dirty) UniqSDFM Id VarInfo
    env
      where
        go :: [Id] -> UniqSDFM Id VarInfo -> m TmState
    go []     UniqSDFM Id VarInfo
    env  = TmState -> m TmState
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TmState
    ts{ts_facts=env}
        go (Id
    x:[Id]
    xs) !UniqSDFM Id VarInfo
    env = do
          vi' <- VarInfo -> m VarInfo
    f (TmState -> Id -> VarInfo
    lookupVarInfo TmState
    ts Id
    x)
          go xs (addToUSDFM env x vi')

    traverseAll :: Monad m => (VarInfo -> m VarInfo) -> TmState -> m TmState
    traverseAll :: forall (m :: * -> *).
    Monad m =>
    (VarInfo -> m VarInfo) -> TmState -> m TmState
    traverseAll VarInfo -> m VarInfo
    f ts :: TmState
    ts@TmSt{ts_facts :: TmState -> UniqSDFM Id VarInfo
    ts_facts = UniqSDFM Id VarInfo
    env} = do
      env' <- (VarInfo -> m VarInfo)
    -> UniqSDFM Id VarInfo -> m (UniqSDFM Id VarInfo)
    forall key a b (f :: * -> *).
    Applicative f =>
    (a -> f b) -> UniqSDFM key a -> f (UniqSDFM key b)
    traverseUSDFM VarInfo -> m VarInfo
    f UniqSDFM Id VarInfo
    env
      pure ts{ts_facts = env'}

    -- | Makes sure the given 'Nabla' is still inhabited, by trying to instantiate
    -- all dirty variables (or all variables when the 'TyState' changed) to concrete
    -- inhabitants. It returns a 'Nabla' with the *same* inhabitants, but with some
    -- amount of work cached (like failed instantiation attempts) from the test.
    --
    -- The \(∇ ⊢ x inh\) judgment form in Figure 8 of the LYG paper.
    inhabitationTest :: Int -> TyState -> Nabla -> MaybeT DsM Nabla
    inhabitationTest :: Int
    -> TyState -> Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    inhabitationTest Int
    0     TyState
    _         Nabla
    nabla             = Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Nabla
    nabla
    inhabitationTest Int
    fuel  TyState
    old_ty_st nabla :: Nabla
    nabla@MkNabla{ nabla_tm_st :: Nabla -> TmState
    nabla_tm_st = TmState
    ts } = {-# SCC "inhabitationTest" #-} do
      -- lift $ tracePm "inhabitation test" $ vcat
      --   [ ppr fuel
      --   , ppr old_ty_st
      --   , ppr nabla
      --   , text "tyStateRefined:" <+> ppr (tyStateRefined old_ty_st (nabla_ty_st nabla))
      --   ]
      -- When type state didn't change, we only need to traverse dirty VarInfos
      ts' <- if TyState -> TyState -> Bool
    tyStateRefined TyState
    old_ty_st (Nabla -> TyState
    nabla_ty_st Nabla
    nabla)
                then (VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo)
    -> TmState -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) TmState
    forall (m :: * -> *).
    Monad m =>
    (VarInfo -> m VarInfo) -> TmState -> m TmState
    traverseAll   VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
    test_one TmState
    ts
                else (VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo)
    -> TmState -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) TmState
    forall (m :: * -> *).
    Monad m =>
    (VarInfo -> m VarInfo) -> TmState -> m TmState
    traverseDirty VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
    test_one TmState
    ts
      pure nabla{ nabla_tm_st = ts'{ts_dirty=emptyDVarSet}}
      where
        nabla_not_dirty :: Nabla
    nabla_not_dirty = Nabla
    nabla{ nabla_tm_st = ts{ts_dirty=emptyDVarSet} }
        test_one :: VarInfo -> MaybeT DsM VarInfo
        test_one :: VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
    test_one VarInfo
    vi =
          DsM Bool -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Bool
    forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TyState -> Nabla -> VarInfo -> DsM Bool
    varNeedsTesting TyState
    old_ty_st Nabla
    nabla VarInfo
    vi) MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Bool
    -> (Bool -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo)
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
    forall a b.
    MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
    -> (a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) b)
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
            Bool
    True -> do
              -- lift $ tracePm "test_one" (ppr vi)
              -- No solution yet and needs testing
              -- We have to test with a Nabla where all dirty bits are cleared
              Int
    -> Nabla
    -> VarInfo
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
    instantiate (Int
    fuelInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) Nabla
    nabla_not_dirty VarInfo
    vi
            Bool
    _ -> VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
    forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure VarInfo
    vi

    -- | Checks whether the given 'VarInfo' needs to be tested for inhabitants.
    -- Returns `False` when we can skip the inhabitation test, presuming it would
    -- say "yes" anyway. See Note [Shortcutting the inhabitation test].
    varNeedsTesting :: TyState -> Nabla -> VarInfo -> DsM Bool
    varNeedsTesting :: TyState -> Nabla -> VarInfo -> DsM Bool
    varNeedsTesting TyState
    _         MkNabla{nabla_tm_st :: Nabla -> TmState
    nabla_tm_st=TmState
    tm_st}     VarInfo
    vi
      | Id -> DIdSet -> Bool
    elemDVarSet (VarInfo -> Id
    vi_id VarInfo
    vi) (TmState -> DIdSet
    ts_dirty TmState
    tm_st) = Bool -> DsM Bool
    forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    True
    varNeedsTesting TyState
    _         Nabla
    _                              VarInfo
    vi
      | [PmAltConApp] -> Bool
    forall (f :: * -> *) a. Foldable f => f a -> Bool
    notNull (VarInfo -> [PmAltConApp]
    vi_pos VarInfo
    vi)                     = Bool -> DsM Bool
    forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    False
    varNeedsTesting TyState
    old_ty_st MkNabla{nabla_ty_st :: Nabla -> TyState
    nabla_ty_st=TyState
    new_ty_st} VarInfo
    _
      -- Same type state => still inhabited
      | Bool -> Bool
    not (TyState -> TyState -> Bool
    tyStateRefined TyState
    old_ty_st TyState
    new_ty_st) = Bool -> DsM Bool
    forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    False
    varNeedsTesting TyState
    old_ty_st MkNabla{nabla_ty_st :: Nabla -> TyState
    nabla_ty_st=TyState
    new_ty_st} VarInfo
    vi = do
      -- These normalisations are relatively expensive, but still better than having
      -- to perform a full inhabitation test
      (_, _, old_norm_ty) <- TopNormaliseTypeResult -> (Type, [(Type, DataCon, Type)], Type)
    tntrGuts (TopNormaliseTypeResult -> (Type, [(Type, DataCon, Type)], Type))
    -> DsM TopNormaliseTypeResult
    -> IOEnv
         (Env DsGblEnv DsLclEnv) (Type, [(Type, DataCon, Type)], Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TyState -> Type -> DsM TopNormaliseTypeResult
    pmTopNormaliseType TyState
    old_ty_st (Id -> Type
    idType (Id -> Type) -> Id -> Type
    forall a b. (a -> b) -> a -> b
    $ VarInfo -> Id
    vi_id VarInfo
    vi)
      (_, _, new_norm_ty) <- tntrGuts <$> pmTopNormaliseType new_ty_st (idType $ vi_id vi)
      if old_norm_ty `eqType` new_norm_ty
        then pure False
        else pure True

    -- | Returns (Just vi) if at least one member of each ConLike in the COMPLETE
    -- set satisfies the oracle
    --
    -- Internally uses and updates the CompleteMatchs in vi_rcm.
    --
    -- NB: Does /not/ filter each CompleteMatch with the oracle; members may
    --     remain that do not satisfy it.  This lazy approach just
    --     avoids doing unnecessary work.
    instantiate :: Int -> Nabla -> VarInfo -> MaybeT DsM VarInfo
    instantiate :: Int
    -> Nabla
    -> VarInfo
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
    instantiate Int
    fuel Nabla
    nabla VarInfo
    vi = {-# SCC "instantiate" #-}
      (Int
    -> Nabla
    -> VarInfo
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
    instBot Int
    fuel Nabla
    nabla VarInfo
    vi MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
    forall a.
    MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> Int
    -> Nabla
    -> VarInfo
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
    instCompleteSets Int
    fuel Nabla
    nabla VarInfo
    vi)

    -- | The \(⊢_{Bot}\) rule from the paper
    instBot :: Int -> Nabla -> VarInfo -> MaybeT DsM VarInfo
    instBot :: Int
    -> Nabla
    -> VarInfo
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
    instBot Int
    _fuel Nabla
    nabla VarInfo
    vi = {-# SCC "instBot" #-} do
      _nabla' <- Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    addBotCt Nabla
    nabla (VarInfo -> Id
    vi_id VarInfo
    vi)
      pure vi

    addNormalisedTypeMatches :: Nabla -> Id -> DsM (ResidualCompleteMatches, Nabla)
    addNormalisedTypeMatches :: Nabla -> Id -> DsM (ResidualCompleteMatches, Nabla)
    addNormalisedTypeMatches nabla :: Nabla
    nabla@MkNabla{ nabla_ty_st :: Nabla -> TyState
    nabla_ty_st = TyState
    ty_st } Id
    x
      = (VarInfo
     -> IOEnv
          (Env DsGblEnv DsLclEnv) (ResidualCompleteMatches, VarInfo))
    -> Nabla -> Id -> DsM (ResidualCompleteMatches, Nabla)
    forall (f :: * -> *) a.
    Functor f =>
    (VarInfo -> f (a, VarInfo)) -> Nabla -> Id -> f (a, Nabla)
    trvVarInfo VarInfo
    -> IOEnv (Env DsGblEnv DsLclEnv) (ResidualCompleteMatches, VarInfo)
    add_matches Nabla
    nabla Id
    x
      where
        add_matches :: VarInfo
    -> IOEnv (Env DsGblEnv DsLclEnv) (ResidualCompleteMatches, VarInfo)
    add_matches vi :: VarInfo
    vi@VI{ vi_rcm :: VarInfo -> ResidualCompleteMatches
    vi_rcm = ResidualCompleteMatches
    rcm }
          -- important common case, shaving down allocations of PmSeriesG by -5%
          | ResidualCompleteMatches -> Bool
    isRcmInitialised ResidualCompleteMatches
    rcm = (ResidualCompleteMatches, VarInfo)
    -> IOEnv (Env DsGblEnv DsLclEnv) (ResidualCompleteMatches, VarInfo)
    forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (ResidualCompleteMatches
    rcm, VarInfo
    vi)
        add_matches vi :: VarInfo
    vi@VI{ vi_rcm :: VarInfo -> ResidualCompleteMatches
    vi_rcm = ResidualCompleteMatches
    rcm } = do
          norm_res_ty <- TyState -> Type -> DsM Type
    normaliseSourceTypeWHNF TyState
    ty_st (Id -> Type
    idType Id
    x)
          env <- dsGetFamInstEnvs
          rcm' <- case splitReprTyConApp_maybe env norm_res_ty of
            Just (TyCon
    rep_tc, ThetaType
    _args, Coercion
    _co)  -> TyCon -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
    addTyConMatches TyCon
    rep_tc ResidualCompleteMatches
    rcm
            Maybe (TyCon, ThetaType, Coercion)
    Nothing                    -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
    addCompleteMatches ResidualCompleteMatches
    rcm
          pure (rcm', vi{ vi_rcm = rcm' })

    -- | Does a 'splitTyConApp_maybe' and then tries to look through a data family
    -- application to find the representation TyCon, to which the data constructors
    -- are attached. Returns the representation TyCon, the TyCon application args
    -- and a representational coercion that will be Refl for non-data family apps.
    splitReprTyConApp_maybe :: FamInstEnvs -> Type -> Maybe (TyCon, [Type], Coercion)
    splitReprTyConApp_maybe :: FamInstEnvs -> Type -> Maybe (TyCon, ThetaType, Coercion)
    splitReprTyConApp_maybe FamInstEnvs
    env Type
    ty =
      (TyCon -> ThetaType -> (TyCon, ThetaType, Coercion))
    -> (TyCon, ThetaType) -> (TyCon, ThetaType, Coercion)
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry (FamInstEnvs -> TyCon -> ThetaType -> (TyCon, ThetaType, Coercion)
    tcLookupDataFamInst FamInstEnvs
    env) ((TyCon, ThetaType) -> (TyCon, ThetaType, Coercion))
    -> Maybe (TyCon, ThetaType) -> Maybe (TyCon, ThetaType, Coercion)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> HasDebugCallStack => Type -> Maybe (TyCon, ThetaType)
    Type -> Maybe (TyCon, ThetaType)
    splitTyConApp_maybe Type
    ty

    -- | This is the |-Inst rule from the paper (section 4.5). Tries to
    -- find an inhabitant in every complete set by instantiating with one their
    -- constructors. If there is any complete set where we can't find an
    -- inhabitant, the whole thing is uninhabited. It returns the updated 'VarInfo'
    -- where all the attempted ConLike instantiations have been purged from the
    -- 'ResidualCompleteMatches', which functions as a cache.
    instCompleteSets :: Int -> Nabla -> VarInfo -> MaybeT DsM VarInfo
    instCompleteSets :: Int
    -> Nabla
    -> VarInfo
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
    instCompleteSets Int
    fuel Nabla
    nabla VarInfo
    vi = {-# SCC "instCompleteSets" #-} do
      let x :: Id
    x = VarInfo -> Id
    vi_id VarInfo
    vi
      (rcm, nabla) <- DsM (ResidualCompleteMatches, Nabla)
    -> MaybeT
         (IOEnv (Env DsGblEnv DsLclEnv)) (ResidualCompleteMatches, Nabla)
    forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (Nabla -> Id -> DsM (ResidualCompleteMatches, Nabla)
    addNormalisedTypeMatches Nabla
    nabla Id
    x)
      nabla <- foldM (\Nabla
    nabla CompleteMatch
    cls -> Int
    -> Nabla
    -> Id
    -> CompleteMatch
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    instCompleteSet Int
    fuel Nabla
    nabla Id
    x CompleteMatch
    cls) nabla (getRcm rcm)
      pure (lookupVarInfo (nabla_tm_st nabla) x)

    anyConLikeSolution :: (ConLike -> Bool) -> [PmAltConApp] -> Bool
    anyConLikeSolution :: (ConLike -> Bool) -> [PmAltConApp] -> Bool
    anyConLikeSolution ConLike -> Bool
    p = (PmAltConApp -> Bool) -> [PmAltConApp] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (PmAltCon -> Bool
    go (PmAltCon -> Bool)
    -> (PmAltConApp -> PmAltCon) -> PmAltConApp -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PmAltConApp -> PmAltCon
    paca_con)
      where
        go :: PmAltCon -> Bool
    go (PmAltConLike ConLike
    cl) = ConLike -> Bool
    p ConLike
    cl
        go PmAltCon
    _                 = Bool
    False

    -- | @instCompleteSet fuel nabla x cls@ iterates over @cls@ until it finds
    -- the first inhabited ConLike (as per 'instCon'). Any failed instantiation
    -- attempts of a ConLike are recorded as negative information in the returned
    -- 'Nabla', so that later calls to this function can skip repeatedly fruitless
    -- instantiation of that same constructor.
    --
    -- Note that the returned Nabla is just a different representation of the
    -- original Nabla, not a proper refinement! No positive information will be
    -- added, only negative information from failed instantiation attempts,
    -- entirely as an optimisation.
    instCompleteSet :: Int -> Nabla -> Id -> CompleteMatch -> MaybeT DsM Nabla
    instCompleteSet :: Int
    -> Nabla
    -> Id
    -> CompleteMatch
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    instCompleteSet Int
    fuel Nabla
    nabla Id
    x CompleteMatch
    cs
      | (ConLike -> Bool) -> [PmAltConApp] -> Bool
    anyConLikeSolution (ConLike -> UniqDSet ConLike -> Bool
    forall a. Uniquable a => a -> UniqDSet a -> Bool
    `elementOfUniqDSet` (CompleteMatch -> UniqDSet ConLike
    cmConLikes CompleteMatch
    cs)) (VarInfo -> [PmAltConApp]
    vi_pos VarInfo
    vi)
      -- No need to instantiate a constructor of this COMPLETE set if we already
      -- have a solution!
      = Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Nabla
    nabla
      | Bool -> Bool
    not (Type -> CompleteMatch -> Bool
    completeMatchAppliesAtType (Id -> Type
    varType Id
    x) CompleteMatch
    cs)
      = Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Nabla
    nabla
      | Bool
    otherwise
      = {-# SCC "instCompleteSet" #-} Nabla -> [ConLike] -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    go Nabla
    nabla (CompleteMatch -> [ConLike]
    sorted_candidates CompleteMatch
    cs)
      where
        vi :: VarInfo
    vi = TmState -> Id -> VarInfo
    lookupVarInfo (Nabla -> TmState
    nabla_tm_st Nabla
    nabla) Id
    x

        sorted_candidates :: CompleteMatch -> [ConLike]
        sorted_candidates :: CompleteMatch -> [ConLike]
    sorted_candidates CompleteMatch
    cm
          -- If there aren't many candidates, we can try to sort them by number of
          -- strict fields, type constraints, etc., so that we are fast in the
          -- common case
          -- (either many simple constructors *or* few "complicated" ones).
          | UniqDSet ConLike -> Int
    forall a. UniqDSet a -> Int
    sizeUniqDSet UniqDSet ConLike
    cs Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    5 = (ConLike -> ConLike -> Ordering) -> [ConLike] -> [ConLike]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy ConLike -> ConLike -> Ordering
    compareConLikeTestability (UniqDSet ConLike -> [ConLike]
    forall a. UniqDSet a -> [a]
    uniqDSetToList UniqDSet ConLike
    cs)
          | Bool
    otherwise            = UniqDSet ConLike -> [ConLike]
    forall a. UniqDSet a -> [a]
    uniqDSetToList UniqDSet ConLike
    cs
          where cs :: UniqDSet ConLike
    cs = CompleteMatch -> UniqDSet ConLike
    cmConLikes CompleteMatch
    cm

        go :: Nabla -> [ConLike] -> MaybeT DsM Nabla
        go :: Nabla -> [ConLike] -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    go Nabla
    _     []         = MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    forall a. MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
        go Nabla
    nabla (RealDataCon DataCon
    dc:[ConLike]
    _)
          -- See Note [DataCons that are definitely inhabitable]
          -- Recall that dc can't be in vi_neg, because then it would be
          -- deleted from the residual COMPLETE set.
          | DataCon -> Bool
    isDataConTriviallyInhabited DataCon
    dc
          = Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Nabla
    nabla
        go Nabla
    nabla (ConLike
    con:[ConLike]
    cons) = do
          let x :: Id
    x = VarInfo -> Id
    vi_id VarInfo
    vi
          let recur_not_con :: MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    recur_not_con = do
                nabla' <- Nabla
    -> Id -> PmAltCon -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    addNotConCt Nabla
    nabla Id
    x (ConLike -> PmAltCon
    PmAltConLike ConLike
    con)
                go nabla' cons
          (Nabla
    nabla Nabla
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    forall a b.
    a
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) b
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Int
    -> Nabla
    -> Id
    -> ConLike
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    instCon Int
    fuel Nabla
    nabla Id
    x ConLike
    con) -- return the original nabla, not the
                                              -- refined one!
                MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    forall a.
    MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    recur_not_con -- Assume that x can't be con. Encode that fact
                                  -- with addNotConCt and recur.

    -- | Is this 'DataCon' trivially inhabited, that is, without needing to perform
    -- any inhabitation testing because of strict/unlifted fields or type
    -- equalities? See Note [DataCons that are definitely inhabitable]
    isDataConTriviallyInhabited :: DataCon -> Bool
    isDataConTriviallyInhabited :: DataCon -> Bool
    isDataConTriviallyInhabited DataCon
    dc
      | TyCon -> Bool
    isTyConTriviallyInhabited (DataCon -> TyCon
    dataConTyCon DataCon
    dc) = Bool
    True
    isDataConTriviallyInhabited DataCon
    dc =
      ThetaType -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null (DataCon -> ThetaType
    dataConTheta DataCon
    dc) Bool -> Bool -> Bool
    &&                -- (1)
      [HsImplBang] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null (DataCon -> [HsImplBang]
    dataConImplBangs DataCon
    dc) Bool -> Bool -> Bool
    &&            -- (2)
      ThetaType -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null (DataCon -> ThetaType
    dataConMightBeUnliftedFieldTys DataCon
    dc) -- (3)

    dataConMightBeUnliftedFieldTys :: DataCon -> [Type]
    dataConMightBeUnliftedFieldTys :: DataCon -> ThetaType
    dataConMightBeUnliftedFieldTys =
      (Type -> Bool) -> ThetaType -> ThetaType
    forall a. (a -> Bool) -> [a] -> [a]
    filter Type -> Bool
    mightBeUnliftedType (ThetaType -> ThetaType)
    -> (DataCon -> ThetaType) -> DataCon -> ThetaType
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Scaled Type -> Type) -> [Scaled Type] -> ThetaType
    forall a b. (a -> b) -> [a] -> [b]
    map Scaled Type -> Type
    forall a. Scaled a -> a
    scaledThing ([Scaled Type] -> ThetaType)
    -> (DataCon -> [Scaled Type]) -> DataCon -> ThetaType
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DataCon -> [Scaled Type]
    dataConOrigArgTys

    isTyConTriviallyInhabited :: TyCon -> Bool
    isTyConTriviallyInhabited :: TyCon -> Bool
    isTyConTriviallyInhabited TyCon
    tc = Unique -> UniqSet Unique -> Bool
    forall a. Uniquable a => a -> UniqSet a -> Bool
    elementOfUniqSet (TyCon -> Unique
    forall a. Uniquable a => a -> Unique
    getUnique TyCon
    tc) UniqSet Unique
    triviallyInhabitedTyConKeys

    -- | All these types are trivially inhabited
    triviallyInhabitedTyConKeys :: UniqSet Unique
    triviallyInhabitedTyConKeys :: UniqSet Unique
    triviallyInhabitedTyConKeys = [Unique] -> UniqSet Unique
    forall a. Uniquable a => [a] -> UniqSet a
    mkUniqSet [
        Unique
    charTyConKey, Unique
    doubleTyConKey, Unique
    floatTyConKey,
        Unique
    intTyConKey, Unique
    int8TyConKey, Unique
    int16TyConKey, Unique
    int32TyConKey, Unique
    int64TyConKey,
        Unique
    intPrimTyConKey, Unique
    int8PrimTyConKey, Unique
    int16PrimTyConKey, Unique
    int32PrimTyConKey, Unique
    int64PrimTyConKey,
        Unique
    wordTyConKey, Unique
    word8TyConKey, Unique
    word16TyConKey, Unique
    word32TyConKey, Unique
    word64TyConKey,
        Unique
    wordPrimTyConKey, Unique
    word8PrimTyConKey, Unique
    word16PrimTyConKey, Unique
    word32PrimTyConKey, Unique
    word64PrimTyConKey,
        Unique
    trTyConTyConKey
      ]

    compareConLikeTestability :: ConLike -> ConLike -> Ordering
    -- We should instantiate DataCons first, because they are likely to occur in
    -- multiple COMPLETE sets at once and we might find that multiple COMPLETE sets
    -- are inhabited by instantiating only a single DataCon.
    compareConLikeTestability :: ConLike -> ConLike -> Ordering
    compareConLikeTestability PatSynCon{}     ConLike
    _               = Ordering
    GT
    compareConLikeTestability ConLike
    _               PatSynCon{}     = Ordering
    GT
    compareConLikeTestability (RealDataCon DataCon
    a) (RealDataCon DataCon
    b) = [DataCon -> DataCon -> Ordering] -> DataCon -> DataCon -> Ordering
    forall a. Monoid a => [a] -> a
    mconcat
      -- Thetas are most expensive to check, as they might incur a whole new round
      -- of inhabitation testing
      [ (DataCon -> Int) -> DataCon -> DataCon -> Ordering
    forall a b. Ord a => (b -> a) -> b -> b -> Ordering
    comparing (ThetaType -> Int
    forall a. [a] -> Int
    fast_length (ThetaType -> Int) -> (DataCon -> ThetaType) -> DataCon -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DataCon -> ThetaType
    dataConTheta)
      -- Unlifted or strict fields only incur an inhabitation test for that
      -- particular field. Still something to avoid.
      , (DataCon -> Int) -> DataCon -> DataCon -> Ordering
    forall a b. Ord a => (b -> a) -> b -> b -> Ordering
    comparing DataCon -> Int
    unlifted_or_strict_fields
      ] DataCon
    a DataCon
    b
      where
        fast_length :: [a] -> Int
        fast_length :: forall a. [a] -> Int
    fast_length [a]
    xs = ([a] -> Int) -> Int -> [a] -> Int -> Int
    forall a b. ([a] -> b) -> b -> [a] -> Int -> b
    atLength [a] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Int
    6 [a]
    xs Int
    5 -- @min 6 (length xs)@, but O(1)

        -- An upper bound on the number of strict or unlifted fields. Approximate in
        -- the unlikely bogus case of an unlifted field that has a bang.
        unlifted_or_strict_fields :: DataCon -> Int
        unlifted_or_strict_fields :: DataCon -> Int
    unlifted_or_strict_fields DataCon
    dc = [HsImplBang] -> Int
    forall a. [a] -> Int
    fast_length (DataCon -> [HsImplBang]
    dataConImplBangs DataCon
    dc)
                                     Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + ThetaType -> Int
    forall a. [a] -> Int
    fast_length (DataCon -> ThetaType
    dataConMightBeUnliftedFieldTys DataCon
    dc)

    -- | @instCon fuel nabla (x::match_ty) K@ tries to instantiate @x@ to @K@ by
    -- adding the proper constructor constraint.
    --
    -- See Note [Instantiating a ConLike].
    instCon :: Int -> Nabla -> Id -> ConLike -> MaybeT DsM Nabla
    instCon :: Int
    -> Nabla
    -> Id
    -> ConLike
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    instCon Int
    fuel nabla :: Nabla
    nabla@MkNabla{nabla_ty_st :: Nabla -> TyState
    nabla_ty_st = TyState
    ty_st} Id
    x ConLike
    con = {-# SCC "instCon" #-} IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
     -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla)
    -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    forall a b. (a -> b) -> a -> b
    $ do
      let hdr :: String -> String
    hdr String
    what = String
    "instCon " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    fuel String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    what
      env <- DsM FamInstEnvs
    dsGetFamInstEnvs
      let match_ty = Id -> Type
    idType Id
    x
      tracePm (hdr "{") $
        ppr con <+> text "... <-" <+> ppr x <+> dcolon <+> ppr match_ty
      norm_match_ty <- normaliseSourceTypeWHNF ty_st match_ty
      mb_sigma_univ <- matchConLikeResTy env ty_st norm_match_ty con
      case mb_sigma_univ of
        Just Subst
    sigma_univ -> do
          let ([Id]
    _univ_tvs, [Id]
    ex_tvs, [EqSpec]
    eq_spec, ThetaType
    thetas, ThetaType
    _req_theta, [Scaled Type]
    field_tys, Type
    _con_res_ty)
                = ConLike
    -> ([Id], [Id], [EqSpec], ThetaType, ThetaType, [Scaled Type],
        Type)
    conLikeFullSig ConLike
    con
          -- Following Note [Instantiating a ConLike]:
          -- (1) _req_theta has been tested in 'matchConLikeResTy'
          -- (2) Instantiate fresh existentials
          (sigma_ex, _) <- Subst -> [Id] -> UniqSupply -> (Subst, [Id])
    cloneTyVarBndrs Subst
    sigma_univ [Id]
    ex_tvs (UniqSupply -> (Subst, [Id]))
    -> DsM UniqSupply -> IOEnv (Env DsGblEnv DsLclEnv) (Subst, [Id])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> DsM UniqSupply
    forall (m :: * -> *). MonadUnique m => m UniqSupply
    getUniqueSupplyM
          -- (3) Substitute provided constraints bound by the constructor.
          --     These are added to the type oracle as new facts (in a moment)
          let gammas = HasDebugCallStack => Subst -> ThetaType -> ThetaType
    Subst -> ThetaType -> ThetaType
    substTheta Subst
    sigma_ex ([EqSpec] -> ThetaType
    eqSpecPreds [EqSpec]
    eq_spec ThetaType -> ThetaType -> ThetaType
    forall a. [a] -> [a] -> [a]
    ++ ThetaType
    thetas)
          -- (4) Instantiate fresh term variables as arguments to the constructor
          let field_tys' = HasDebugCallStack => Subst -> ThetaType -> ThetaType
    Subst -> ThetaType -> ThetaType
    substTys Subst
    sigma_ex (ThetaType -> ThetaType) -> ThetaType -> ThetaType
    forall a b. (a -> b) -> a -> b
    $ (Scaled Type -> Type) -> [Scaled Type] -> ThetaType
    forall a b. (a -> b) -> [a] -> [b]
    map Scaled Type -> Type
    forall a. Scaled a -> a
    scaledThing [Scaled Type]
    field_tys
          arg_ids <- mapM mkPmId field_tys'
          tracePm (hdr "(cts)") $ vcat
            [ ppr x <+> dcolon <+> ppr match_ty
            , text "In WHNF:" <+> ppr (isSourceTypeInWHNF match_ty) <+> ppr norm_match_ty
            , ppr con <+> dcolon <+> text "... ->" <+> ppr _con_res_ty
            , ppr (map (\Id
    tv -> Id -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Id
    tv SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Char -> SDoc
    forall doc. IsLine doc => Char -> doc
    char Char
    '↦' SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Type -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (Subst -> Id -> Type
    substTyVar Subst
    sigma_univ Id
    tv)) _univ_tvs)
            , ppr gammas
            , ppr (map (\Id
    x -> Id -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Id
    x SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> SDoc
    dcolon SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Type -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (Id -> Type
    idType Id
    x)) arg_ids)
            ]
          -- (5) Finally add the new constructor constraint
          runMaybeT $ do
            -- Case (2) of Note [Strict fields and variables of unlifted type]
            let alt = ConLike -> PmAltCon
    PmAltConLike ConLike
    con
            let branching_factor = [Id] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length ([Id] -> Int) -> [Id] -> Int
    forall a b. (a -> b) -> a -> b
    $ PmAltCon -> [Id] -> [Id]
    filterUnliftedFields PmAltCon
    alt [Id]
    arg_ids
            let ct = Id -> PmAltCon -> [Id] -> ThetaType -> [Id] -> PhiCt
    PhiConCt Id
    x PmAltCon
    alt [Id]
    ex_tvs ThetaType
    gammas [Id]
    arg_ids
            nabla1 <- traceWhenFailPm (hdr "(ct unsatisfiable) }") (ppr ct) $
                      addPhiTmCt nabla ct
            -- See Note [Fuel for the inhabitation test]
            let new_fuel
                  | Int
    branching_factor Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    1 = Int
    fuel
                  | Bool
    otherwise             = Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    min Int
    fuel Int
    2
            lift $ tracePm (hdr "(ct satisfiable)") $ vcat
              [ ppr ct
              , ppr x <+> dcolon <+> ppr match_ty
              , text "In WHNF:" <+> ppr (isSourceTypeInWHNF match_ty) <+> ppr norm_match_ty
              , ppr con <+> dcolon <+> text "... ->" <+> ppr _con_res_ty
              , ppr (map (\Id
    tv -> Id -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Id
    tv SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Char -> SDoc
    forall doc. IsLine doc => Char -> doc
    char Char
    '↦' SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Type -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (Subst -> Id -> Type
    substTyVar Subst
    sigma_univ Id
    tv)) _univ_tvs)
              , ppr gammas
              , ppr (map (\Id
    x -> Id -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Id
    x SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> SDoc
    dcolon SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Type -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (Id -> Type
    idType Id
    x)) arg_ids)
              , ppr branching_factor
              , ppr new_fuel
              ]
            nabla2 <- traceWhenFailPm (hdr "(inh test failed) }") (ppr nabla1) $
                      inhabitationTest new_fuel (nabla_ty_st nabla) nabla1
            lift $ tracePm (hdr "(inh test succeeded) }") (ppr nabla2)
            pure nabla2
        Maybe Subst
    Nothing -> do
          String -> SDoc -> DsM ()
    tracePm (String -> String
    hdr String
    "(match_ty not instance of res_ty) }") SDoc
    forall doc. IsOutput doc => doc
    empty
          Maybe Nabla -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
    forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Nabla -> Maybe Nabla
    forall a. a -> Maybe a
    Just Nabla
    nabla) -- Matching against match_ty failed. Inhabited!
                            -- See Note [Instantiating a ConLike].

    -- | @matchConLikeResTy _ _ ty K@ tries to match @ty@ against the result
    -- type of @K@, @res_ty@. It returns a substitution @s@ for @K@'s universal
    -- tyvars such that @s(res_ty)@ equals @ty@ if successful.
    --
    -- Make sure that @ty@ is normalised before.
    --
    -- See Note [Matching against a ConLike result type].
    matchConLikeResTy :: FamInstEnvs -> TyState -> Type -> ConLike -> DsM (Maybe Subst)
    matchConLikeResTy :: FamInstEnvs -> TyState -> Type -> ConLike -> DsM (Maybe Subst)
    matchConLikeResTy FamInstEnvs
    env TyState
    _              Type
    ty (RealDataCon DataCon
    dc) = Maybe Subst -> DsM (Maybe Subst)
    forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Maybe Subst -> DsM (Maybe Subst))
    -> Maybe Subst -> DsM (Maybe Subst)
    forall a b. (a -> b) -> a -> b
    $ do
      (rep_tc, tc_args, _co) <- FamInstEnvs -> Type -> Maybe (TyCon, ThetaType, Coercion)
    splitReprTyConApp_maybe FamInstEnvs
    env Type
    ty
      if rep_tc == dataConTyCon dc
        then Just (zipTCvSubst (dataConUnivTyVars dc) tc_args)
        else Nothing
    matchConLikeResTy FamInstEnvs
    _   (TySt Int
    _ InertSet
    inert) Type
    ty (PatSynCon PatSyn
    ps) = {-# SCC "matchConLikeResTy" #-} MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Subst -> DsM (Maybe Subst)
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT (MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Subst -> DsM (Maybe Subst))
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Subst
    -> DsM (Maybe Subst)
    forall a b. (a -> b) -> a -> b
    $ do
      let ([Id]
    univ_tvs,ThetaType
    req_theta,[Id]
    _,ThetaType
    _,[Scaled Type]
    _,Type
    con_res_ty) = PatSyn -> ([Id], ThetaType, [Id], ThetaType, [Scaled Type], Type)
    patSynSig PatSyn
    ps
      subst <- DsM (Maybe Subst) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Subst
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (DsM (Maybe Subst) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Subst)
    -> DsM (Maybe Subst)
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Subst
    forall a b. (a -> b) -> a -> b
    $ Maybe Subst -> DsM (Maybe Subst)
    forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Maybe Subst -> DsM (Maybe Subst))
    -> Maybe Subst -> DsM (Maybe Subst)
    forall a b. (a -> b) -> a -> b
    $ Type -> Type -> Maybe Subst
    tcMatchTy Type
    con_res_ty Type
    ty
      guard $ all (`elemSubst` subst) univ_tvs -- See the Note about T11336b
      if null req_theta
        then pure subst
        else do
          let req_theta' = HasDebugCallStack => Subst -> ThetaType -> ThetaType
    Subst -> ThetaType -> ThetaType
    substTys Subst
    subst ThetaType
    req_theta
          satisfiable <- lift $ initTcDsForSolver $ tcCheckWanteds inert req_theta'
          if satisfiable
            then pure subst
            else mzero

    {- Note [Soundness and Completeness]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Soundness and completeness of the pattern-match checker depend entirely on the
    soundness and completeness of the inhabitation test.

    Achieving both soundness and completeness at the same time is undecidable.
    See also T17977 and Note [Fuel for the inhabitation test].
    Losing soundness would make the algorithm pointless; hence we give up on
    completeness, but try to get as close as possible (how close is called
    the 'precision' of the algorithm).

    Soundness means that you
      1. Can remove clauses flagged as redundant without changing program semantics
         (no false positives).
      2. Can be sure that your program is free of incomplete pattern matches
         when the checker doesn't flag any inexhaustive definitions
         (no false negatives).

    A complete algorithm would mean that
      1. When a clause can be deleted without changing program semantics, it will
         be flagged as redundant (no false negatives).
      2. A program that is free of incomplete pattern matches will never have a
         definition be flagged as inexhaustive (no false positives).

    Via the LYG algorithm, we reduce both these properties to a property on
    the inhabitation test of refinement types:
      *Soundness*:    If the inhabitation test says "no" for a given refinement type
                      Nabla, then it provably has no inhabitant.
      *Completeness*: If the inhabitation test says "yes" for a given refinement type
                      Nabla, then it provably has an inhabitant.
    Our test is sound, but incomplete, so there are instances where we say
    "yes" but in fact the Nabla is empty. Which entails false positive exhaustivity
    and false negative redundancy warnings, as above.

    In summary, we have the following correspondence:

    Property     | Exhaustiveness warnings | Redundancy warnings | Inhabitation test |
    -------------|-------------------------|---------------------|-------------------|
    Soundness    | No false negatives      | No false positives  | Only says "no"    |
                 |                         |                     | if there is no    |
                 |                         |                     | inhabitant        |
    Completeness | No false positives      | No false negatives  | Only says "yes"   |
                 |                         |                     | if there is an    |
                 |                         |                     | inhabitant        |

    Note [Shortcutting the inhabitation test]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Generally, we have to re-test a refinement type for inhabitants whenever we
    add a new constraint. Often, we can say "no" early, upon trying to add a
    contradicting constraint, see Note [The Pos/Neg invariant]. Still, COMPLETE
    sets and type evidence are best handled in a delayed fashion, because of
    the recursive nature of the test and our fuel-based approach.
    But even then there are some cases in which we can skip the full test,
    because we are sure that the refinement type is still inhabited. These
    conditions are monitored by 'varNeedsTesting'. It returns

    - `True` whenever a full inhabitation test is needed
    - `False` whenever the test can be skipped, amounting to an inhabitation test
      that says "yes".

    According to Note [Soundness and Completeness], this test will never compromise
    soundness: The `True` case just forwards to the actual inhabitation test and the
    `False` case amounts to an inhabitation test that is trivially sound, because it
    never says "no".

    Of course, if the returns says `False`, Completeness (and thus Precision) of the
    algorithm is affected, but we get to skip costly inhabitation tests. We try to
    trade as little Precision as possible against as much Performance as possible.
    Here are the tests, in order:

      1. If a variable is dirty (because of a newly added negative term constraint),
         we have to test.
      2. If a variable has positive information, we don't have to test: The
         positive information acts as constructive proof for inhabitation.
      3. If the type state didn't change, there is no need to test.
      4. If the variable's normalised type didn't change, there is no need to test.
      5. Otherwise, we have to test.

    Why (1) before (2)?
    -------------------
    Consider the reverse for (T18960):
      pattern P x = x
      {-# COMPLETE P :: () #-}
      foo = case () of x@(P _) -> ()
    This should be exhaustive. But if we say "We know `x` has solution `()`, so it's
    inhabited", then we'll get a warning saying that `()` wasn't matched.
    But the match on `P` added the new negative information to the uncovered set,
    in the process of which we marked `x` as dirty. By giving the dirty flag a
    higher priority than positive info, we get to test again and see that `x` is
    uninhabited and the match is exhaustive.

    But suppose that `P` wasn't mentioned in any COMPLETE set. Then we simply
    don't mark `x` as dirty and will emit a warning again (which we would anyway),
    without running a superfluous inhabitation test. That speeds up T17836
    considerably.

    Why (2) before (3) and (4)?
    ---------------------------
    Simply because (2) is more efficient to test than (3) (not by a lot), which
    is more efficient to test than (4), which is still more efficient than running
    the full inhabitation test (5).

    Note [Fuel for the inhabitation test]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Whether or not a type is inhabited is undecidable in general, see also
    Note [Soundness and Completeness]. As a result, we can run into infinite
    loops in `inhabitationTest`. Therefore, we adopt a fuel-based approach to
    prevent that.

    Consider the following example:

      data Abyss = MkAbyss !Abyss
      stareIntoTheAbyss :: Abyss -> a
      stareIntoTheAbyss x = case x of {}

    In principle, stareIntoTheAbyss is exhaustive, since there is no way to
    construct a terminating value using MkAbyss. But this can't be proven by mere
    instantiation and requires an inductive argument, which `inhabitationTest`
    currently isn't equipped to do.

    In order to prevent endless instantiation attempts in @inhabitationTest@, we
    use the fuel as an upper bound on such attempts.

    The same problem occurs with recursive newtypes, like in the following code:

      newtype Chasm = MkChasm Chasm
      gazeIntoTheChasm :: Chasm -> a
      gazeIntoTheChasm x = case x of {} -- Erroneously warned as non-exhaustive

    So this limitation is somewhat understandable.

    Note that even with this recursion detection, there is still a possibility that
    `inhabitationTest` can run in exponential time in the amount of fuel. Consider
    the following data type:

      data T = MkT !T !T !T

    If we try to instantiate each of its fields, that will require us to once again
    check if `MkT` is inhabitable in each of those three fields, which in turn will
    require us to check if `MkT` is inhabitable again... As you can see, the
    branching factor adds up quickly, and if the initial fuel is, say,
    100, then the inhabitation test will effectively take forever.

    To mitigate this, we check the branching factor every time we are about to do
    inhabitation testing in 'instCon'. If the branching factor exceeds 1
    (i.e., if there is potential for exponential runtime), then we limit the
    maximum recursion depth to 1 to mitigate the problem. If the branching factor
    is exactly 1 (i.e., we have a linear chain instead of a tree), then it's okay
    to stick with a larger maximum recursion depth.

    In #17977 we saw that the defaultRecTcMaxBound (100 at the time of writing) was
    too large and had detrimental effect on performance of the coverage checker.
    Given that we only commit to a best effort anyway, we decided to substantially
    decrement the fuel to 4, at the cost of precision in some edge cases
    like

      data Nat = Z | S Nat
      data Down :: Nat -> Type where
        Down :: !(Down n) -> Down (S n)
      f :: Down (S (S (S (S (S Z))))) -> ()
      f x = case x of {}

    Since the coverage won't bother to instantiate Down 4 levels deep to see that it
    is in fact uninhabited, it will emit a inexhaustivity warning for the case.

    Note [DataCons that are definitely inhabitable]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Another microoptimization applies to data types like this one:

      data S a = S ![a] !T

    Even though there is a strict field of type [a], it's quite silly to call
    'instCon' on it, since it's "obvious" that it is inhabitable. To make this
    intuition formal, we say that a DataCon C is definitely inhabitable (DI) if:

      1. C has no equality constraints (since they might be unsatisfiable)
      2. C has no strict arguments (since they might be uninhabitable)
      3. C has no unlifted argument types (since they might be uninhabitable)

    It's relatively cheap to check if a DataCon is DI, so before we call 'instCon'
    on a constructor of a COMPLETE set, we filter out all of the DI ones.

    This fast path shaves down -7% allocations for PmSeriesG, for example.

    Note [Matching against a ConLike result type]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Given a ConLike

    > C :: forall us. R => ... -> res_ty

    is a pattern `C ...` compatible with the type `ty`? Clearly that is the case if
    `res_ty` /subsumes/ `ty` and the required constraints `R` (strictly a feature of
    pattern synonyms) are satisfiable. In that case, 'matchConLikeResTy' returns a
    substitution σ over `us` such that `σ(res_ty) == ty`.

    It's surprisingly tricky to implement correctly, and works quite different for
    DataCons and PatSynCons:

      * For data cons, we look at `ty` and see if it's a TyCon app `T t1 ... tn`.
        If that is the case, we make sure that `C` is a DataCon of `T` and return
        a substitution mapping `C`'s universal tyvars `us` to `t1`...`tn`.

        Wrinkle: Since `T` might be a data family TyCon, we have to look up its
        representation TyCon before we compare to `C`'s TyCon.
        So we use 'splitReprTyConApp_maybe' instead of 'splitTyConApp_maybe'.

      * For pattern synonyms, we directly match `ty` against `res_ty` to get the
        substitution σ. See Note [Pattern synonym result type] in "GHC.Core.PatSyn".

        Fortunately, we don't have to treat data family TyCons specially:
        Pattern synonyms /never/ apply to a data family representation TyCon.
        We do have to consider the required constraints `σ(R)`, though, as we have
        seen in #19475. That is done by solving them as Wanted constraints given the
        inert set of the current type state (which is part of a Nabla's TySt). Since
        spinning up a constraint solver session is costly, we only do so in the rare
        cases that a pattern synonym actually carries any required constraints.

        We can get into the strange situation that not all universal type variables
        `us` occur in `res_ty`. Example from T11336b:

          instance C Proxy where ...                      -- impl uninteresting
          pattern P :: forall f a. C f => f a -> Proxy a  -- impl uninteresting

          fun :: Proxy a -> ()
          fun (P Proxy) = ()
          fun (P Proxy) = () -- ideally detected as redundant

        `f` is a universal type variable and `C f` the required constraint of
        pattern synonym `P`. But `f` doesn't occur in the result type `Proxy a` of
        `P`, so σ will not even have `f` in its in-scope set. It's a bit unclear
        what to do here; we might want to freshen `f` to `f'` and see if we can
        solve `C f'` as a Wanted constraint, which we most likely can't.
        Hence, we simply skip the freshening and declare the match as failed when
        there is a variable like `f`. For the definition of `fun`, that
        means we will not remember that we matched on `P` and thus will
        not detect its second clause as redundant.

        See Note [Pattern synonym result type] in "GHC.Core.PatSyn" for similar
        oddities.

    Note [Instantiating a ConLike]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    `instCon` implements the \(Inst\) function from Figure 8 of the LYG paper.

    Given the following type of ConLike `K`

    > K :: forall us. R => forall es. P => t1 -> ... -> tn -> res_ty

    and a variable `x::match_ty`, it tries to find an instantiation
    `K ex_tvs gammas arg_ids :: match_ty` (for fresh `arg_ids`) and ultimately adds
    a constructor constraint `K ex_tvs gammas arg_ids <- x` to the given Nabla.

    As a first step, it tries (via 'matchConLikeResTy') to match `match_ty` against
    `res_ty` and checks that that the required constraints @R@ are satisfiable.
    See Note [Matching against a ConLike result type].

    If matching /fails/, it trivially (and conservatively) reports "inhabited" by
    returning the unrefined input Nabla. After all, the match might have failed due
    to incomplete type information in Nabla.
    (Later type refinement from unpacking GADT constructors might monomorphise
    `match_ty` so much that `res_ty` ultimately subsumes it.)

    If matching /succeeds/, we get a substitution σ for the (universal)
    tyvars `us`. After applying σ, we get

    > K @σ(us) :: σ(R) => forall σ(es). σ(P) => σ(t1) -> ... -> σ(tn) -> match_ty

    The existentials `es` might still occur in argument types `σ(tn)`, though.
    Now 'instCon' performs the following steps:

     1. It drops the required constraints `σ(R)`, as they have already been
        discharged by 'matchConLikeResTy'.
     2. It instantiates fresh binders `es'` for the other type variables `es`
        bound by `K` and adds the mapping to σ to get σ', so that we have

        > K @σ(us) @es' :: σ'(P) => σ'(t1) -> ... -> σ'(tn) -> match_ty

     3. It adds new type constraints from the substituted
        provided constraints @σ'(P)@.
     4. It substitutes and conjures new binders @arg_ids@ for the argument types
        @σ'(t1) ... σ'(tn)@.
     5. It adds a term constraint @K es' σ'(P) arg_ids <- x@, which handles
        the details regarding type constraints and unlifted fields.

    And finally the extended 'Nabla' is returned if all the constraints were
    compatible.
    -}

    --------------------------------------
    -- * Generating inhabitants of a Nabla
    --
    -- This is important for warnings. Roughly corresponds to G in Figure 6 of the
    -- LYG paper, with a few tweaks for better warning messages.

    -- | See Note [Case split inhabiting patterns]
    data GenerateInhabitingPatternsMode
      = CaseSplitTopLevel
      | MinimalCover
      deriving (GenerateInhabitingPatternsMode
    -> GenerateInhabitingPatternsMode -> Bool
    (GenerateInhabitingPatternsMode
     -> GenerateInhabitingPatternsMode -> Bool)
    -> (GenerateInhabitingPatternsMode
        -> GenerateInhabitingPatternsMode -> Bool)
    -> Eq GenerateInhabitingPatternsMode
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: GenerateInhabitingPatternsMode
    -> GenerateInhabitingPatternsMode -> Bool
    == :: GenerateInhabitingPatternsMode
    -> GenerateInhabitingPatternsMode -> Bool
    $c/= :: GenerateInhabitingPatternsMode
    -> GenerateInhabitingPatternsMode -> Bool
    /= :: GenerateInhabitingPatternsMode
    -> GenerateInhabitingPatternsMode -> Bool
    Eq, Int -> GenerateInhabitingPatternsMode -> String -> String
    [GenerateInhabitingPatternsMode] -> String -> String
    GenerateInhabitingPatternsMode -> String
    (Int -> GenerateInhabitingPatternsMode -> String -> String)
    -> (GenerateInhabitingPatternsMode -> String)
    -> ([GenerateInhabitingPatternsMode] -> String -> String)
    -> Show GenerateInhabitingPatternsMode
    forall a.
    (Int -> a -> String -> String)
    -> (a -> String) -> ([a] -> String -> String) -> Show a
    $cshowsPrec :: Int -> GenerateInhabitingPatternsMode -> String -> String
    showsPrec :: Int -> GenerateInhabitingPatternsMode -> String -> String
    $cshow :: GenerateInhabitingPatternsMode -> String
    show :: GenerateInhabitingPatternsMode -> String
    $cshowList :: [GenerateInhabitingPatternsMode] -> String -> String
    showList :: [GenerateInhabitingPatternsMode] -> String -> String
    Show)

    instance Outputable GenerateInhabitingPatternsMode where
      ppr :: GenerateInhabitingPatternsMode -> SDoc
    ppr = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text (String -> SDoc)
    -> (GenerateInhabitingPatternsMode -> String)
    -> GenerateInhabitingPatternsMode
    -> SDoc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . GenerateInhabitingPatternsMode -> String
    forall a. Show a => a -> String
    show

    -- | @generateInhabitingPatterns vs n nabla@ returns a list of at most @n@ (but
    -- perhaps empty) refinements of @nabla@ that represent inhabited patterns.
    -- Negative information is only retained if literals are involved or for
    -- recursive GADTs.
    generateInhabitingPatterns :: GenerateInhabitingPatternsMode -> [Id] -> Int -> Nabla -> DsM [Nabla]
    -- See Note [Why inhabitationTest doesn't call generateInhabitingPatterns]
    generateInhabitingPatterns :: GenerateInhabitingPatternsMode
    -> [Id] -> Int -> Nabla -> DsM [Nabla]
    generateInhabitingPatterns GenerateInhabitingPatternsMode
    _    [Id]
    _      Int
    0 Nabla
    _     = [Nabla] -> DsM [Nabla]
    forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure []
    generateInhabitingPatterns GenerateInhabitingPatternsMode
    _    []     Int
    _ Nabla
    nabla = [Nabla] -> DsM [Nabla]
    forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [Nabla
    nabla]
    generateInhabitingPatterns GenerateInhabitingPatternsMode
    mode (Id
    x:[Id]
    xs) Int
    n Nabla
    nabla = do
      String -> SDoc -> DsM ()
    tracePm String
    "generateInhabitingPatterns" (GenerateInhabitingPatternsMode -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr GenerateInhabitingPatternsMode
    mode SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Int -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Int
    n SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> [Id] -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (Id
    xId -> [Id] -> [Id]
    forall a. a -> [a] -> [a]
    :[Id]
    xs) SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$ Nabla -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Nabla
    nabla)
      let VI Id
    _ [PmAltConApp]
    pos PmAltConSet
    neg BotInfo
    _ ResidualCompleteMatches
    _ = TmState -> Id -> VarInfo
    lookupVarInfo (Nabla -> TmState
    nabla_tm_st Nabla
    nabla) Id
    x
      case [PmAltConApp]
    pos of
        PmAltConApp
    _:[PmAltConApp]
    _ -> do
          -- Example for multiple solutions (must involve a PatSyn):
          --   f x@(Just _) True | SomePatSyn _ <- x = ...
          -- within the RHS, we know that
          --   * @x ~ Just y@ for some @y@
          --   * @x ~ SomePatSyn z@ for some @z@
          -- and both conditions have to hold /at the same time/. Hence we must
          -- find evidence for @y@ and @z@ that is valid at the same time. These
          -- constitute arg_vas below.
          let arg_vas :: [Id]
    arg_vas = (PmAltConApp -> [Id]) -> [PmAltConApp] -> [Id]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap PmAltConApp -> [Id]
    paca_ids [PmAltConApp]
    pos
          GenerateInhabitingPatternsMode
    -> [Id] -> Int -> Nabla -> DsM [Nabla]
    generateInhabitingPatterns GenerateInhabitingPatternsMode
    mode ([Id]
    arg_vas [Id] -> [Id] -> [Id]
    forall a. [a] -> [a] -> [a]
    ++ [Id]
    xs) Int
    n Nabla
    nabla
        []
          -- When there are literals involved, just print negative info
          -- instead of listing missed constructors
          | [PmLit] -> Bool
    forall (f :: * -> *) a. Foldable f => f a -> Bool
    notNull [ PmLit
    l | PmAltLit PmLit
    l <- PmAltConSet -> [PmAltCon]
    pmAltConSetElems PmAltConSet
    neg ]
          -> GenerateInhabitingPatternsMode
    -> [Id] -> Int -> Nabla -> DsM [Nabla]
    generateInhabitingPatterns GenerateInhabitingPatternsMode
    mode [Id]
    xs Int
    n Nabla
    nabla
          -- When some constructors are impossible or when we don't care for a
          -- minimal cover (Note [Case split inhabiting patterns]), do a case split.
          | Bool -> Bool
    not (PmAltConSet -> Bool
    isEmptyPmAltConSet PmAltConSet
    neg) Bool -> Bool -> Bool
    || GenerateInhabitingPatternsMode
    mode GenerateInhabitingPatternsMode
    -> GenerateInhabitingPatternsMode -> Bool
    forall a. Eq a => a -> a -> Bool
    == GenerateInhabitingPatternsMode
    CaseSplitTopLevel
          -> Id -> [Id] -> Int -> Nabla -> DsM [Nabla]
    try_instantiate Id
    x [Id]
    xs Int
    n Nabla
    nabla
          -- Else don't do a case split on this var, just print a wildcard.
          -- But try splitting for the remaining vars, of course
          | Bool
    otherwise
          -> GenerateInhabitingPatternsMode
    -> [Id] -> Int -> Nabla -> DsM [Nabla]
    generateInhabitingPatterns GenerateInhabitingPatternsMode
    mode [Id]
    xs Int
    n Nabla
    nabla
      where
        -- Tries to instantiate a variable by possibly following the chain of
        -- newtypes and then instantiating to all ConLikes of the wrapped type's
        -- minimal residual COMPLETE set.
        try_instantiate :: Id -> [Id] -> Int -> Nabla -> DsM [Nabla]
        -- Convention: x binds the outer constructor in the chain, y the inner one.
        try_instantiate :: Id -> [Id] -> Int -> Nabla -> DsM [Nabla]
    try_instantiate Id
    x [Id]
    xs Int
    n Nabla
    nabla = do
          (_src_ty, dcs, rep_ty) <- TopNormaliseTypeResult -> (Type, [(Type, DataCon, Type)], Type)
    tntrGuts (TopNormaliseTypeResult -> (Type, [(Type, DataCon, Type)], Type))
    -> DsM TopNormaliseTypeResult
    -> IOEnv
         (Env DsGblEnv DsLclEnv) (Type, [(Type, DataCon, Type)], Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TyState -> Type -> DsM TopNormaliseTypeResult
    pmTopNormaliseType (Nabla -> TyState
    nabla_ty_st Nabla
    nabla) (Id -> Type
    idType Id
    x)
          mb_stuff <- runMaybeT $ instantiate_newtype_chain x nabla dcs
          case mb_stuff of
            Maybe (Id, Nabla)
    Nothing -> [Nabla] -> DsM [Nabla]
    forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure []
            Just (Id
    y, Nabla
    newty_nabla) -> do
              let vi :: VarInfo
    vi = TmState -> Id -> VarInfo
    lookupVarInfo (Nabla -> TmState
    nabla_tm_st Nabla
    newty_nabla) Id
    y
              env <- DsM FamInstEnvs
    dsGetFamInstEnvs
              rcm <- case splitReprTyConApp_maybe env rep_ty of
                Just (TyCon
    tc, ThetaType
    _, Coercion
    _) -> TyCon -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
    addTyConMatches TyCon
    tc (VarInfo -> ResidualCompleteMatches
    vi_rcm VarInfo
    vi)
                Maybe (TyCon, ThetaType, Coercion)
    Nothing         -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
    addCompleteMatches (VarInfo -> ResidualCompleteMatches
    vi_rcm VarInfo
    vi)

              -- Test all COMPLETE sets for inhabitants (n inhs at max). Take care of ⊥.
              clss <- pickApplicableCompleteSets (nabla_ty_st nabla) rep_ty rcm
              case NE.nonEmpty (uniqDSetToList . cmConLikes <$> clss) of
                Maybe (NonEmpty [ConLike])
    Nothing ->
                  -- No COMPLETE sets ==> inhabited
                  GenerateInhabitingPatternsMode
    -> [Id] -> Int -> Nabla -> DsM [Nabla]
    generateInhabitingPatterns GenerateInhabitingPatternsMode
    mode [Id]
    xs Int
    n Nabla
    newty_nabla
                Just NonEmpty [ConLike]
    clss -> do
                  -- Try each COMPLETE set, pick the one with the smallest number of
                  -- inhabitants
                  nablass' <- NonEmpty [ConLike]
    -> ([ConLike] -> DsM [Nabla])
    -> IOEnv (Env DsGblEnv DsLclEnv) (NonEmpty [Nabla])
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM NonEmpty [ConLike]
    clss (Id -> Type -> [Id] -> Int -> Nabla -> [ConLike] -> DsM [Nabla]
    instantiate_cons Id
    y Type
    rep_ty [Id]
    xs Int
    n Nabla
    newty_nabla)
                  let nablas' = ([Nabla] -> [Nabla] -> Ordering) -> NonEmpty [Nabla] -> [Nabla]
    forall (t :: * -> *) a.
    Foldable t =>
    (a -> a -> Ordering) -> t a -> a
    minimumBy (([Nabla] -> Int) -> [Nabla] -> [Nabla] -> Ordering
    forall a b. Ord a => (b -> a) -> b -> b -> Ordering
    comparing [Nabla] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length) NonEmpty [Nabla]
    nablass'
                  if null nablas' && vi_bot vi /= IsNotBot
                    then generateInhabitingPatterns mode xs n newty_nabla -- bot is still possible. Display a wildcard!
                    else pure nablas'

        -- Instantiates a chain of newtypes, beginning at @x@.
        -- Turns @x nabla [T,U,V]@ to @(y, nabla')@, where @nabla'@ we has the fact
        -- @x ~ T (U (V y))@.
        instantiate_newtype_chain :: Id -> Nabla -> [(Type, DataCon, Type)] -> MaybeT DsM (Id, Nabla)
        instantiate_newtype_chain :: Id
    -> Nabla
    -> [(Type, DataCon, Type)]
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Nabla)
    instantiate_newtype_chain Id
    x Nabla
    nabla []                      = (Id, Nabla) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Nabla)
    forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Id
    x, Nabla
    nabla)
        instantiate_newtype_chain Id
    x Nabla
    nabla ((Type
    _ty, DataCon
    dc, Type
    arg_ty):[(Type, DataCon, Type)]
    dcs) = do
          y <- IOEnv (Env DsGblEnv DsLclEnv) Id
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Id
    forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (IOEnv (Env DsGblEnv DsLclEnv) Id
     -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Id)
    -> IOEnv (Env DsGblEnv DsLclEnv) Id
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Id
    forall a b. (a -> b) -> a -> b
    $ Type -> IOEnv (Env DsGblEnv DsLclEnv) Id
    mkPmId Type
    arg_ty
          -- Newtypes don't have existentials (yet?!), so passing an empty
          -- list as ex_tvs.
          nabla' <- addConCt nabla x (PmAltConLike (RealDataCon dc)) [] [y]
          instantiate_newtype_chain y nabla' dcs

        instantiate_cons :: Id -> Type -> [Id] -> Int -> Nabla -> [ConLike] -> DsM [Nabla]
        instantiate_cons :: Id -> Type -> [Id] -> Int -> Nabla -> [ConLike] -> DsM [Nabla]
    instantiate_cons Id
    _ Type
    _  [Id]
    _  Int
    _ Nabla
    _     []       = [Nabla] -> DsM [Nabla]
    forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure []
        instantiate_cons Id
    _ Type
    _  [Id]
    _  Int
    0 Nabla
    _     [ConLike]
    _        = [Nabla] -> DsM [Nabla]
    forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure []
        instantiate_cons Id
    _ Type
    ty [Id]
    xs Int
    n Nabla
    nabla [ConLike]
    _
          -- We don't want to expose users to GHC-specific constructors for Int etc.
          | ((TyCon, ThetaType) -> Bool)
    -> Maybe (TyCon, ThetaType) -> Maybe Bool
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (TyCon -> Bool
    isTyConTriviallyInhabited (TyCon -> Bool)
    -> ((TyCon, ThetaType) -> TyCon) -> (TyCon, ThetaType) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (TyCon, ThetaType) -> TyCon
    forall a b. (a, b) -> a
    fst) (HasDebugCallStack => Type -> Maybe (TyCon, ThetaType)
    Type -> Maybe (TyCon, ThetaType)
    splitTyConApp_maybe Type
    ty) Maybe Bool -> Maybe Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    == Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True
          = GenerateInhabitingPatternsMode
    -> [Id] -> Int -> Nabla -> DsM [Nabla]
    generateInhabitingPatterns GenerateInhabitingPatternsMode
    mode [Id]
    xs Int
    n Nabla
    nabla
        instantiate_cons Id
    x Type
    ty [Id]
    xs Int
    n Nabla
    nabla (ConLike
    cl:[ConLike]
    cls) = do
          -- The following line is where we call out to the inhabitationTest!
          mb_nabla <- MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT (MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
     -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla))
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
    forall a b. (a -> b) -> a -> b
    $ Int
    -> Nabla
    -> Id
    -> ConLike
    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
    instCon Int
    4 Nabla
    nabla Id
    x ConLike
    cl
          tracePm "instantiate_cons" (vcat [ ppr x <+> dcolon <+> ppr (idType x)
                                           , ppr ty
                                           , ppr cl
                                           , ppr nabla
                                           , ppr mb_nabla
                                           , ppr n ])
          con_nablas <- case mb_nabla of
            Maybe Nabla
    Nothing     -> [Nabla] -> DsM [Nabla]
    forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure []
            -- NB: We don't prepend arg_vars as we don't have any evidence on
            -- them and we only want to split once on a data type. They are
            -- inhabited, otherwise the inhabitation test would have refuted.
            Just Nabla
    nabla' -> GenerateInhabitingPatternsMode
    -> [Id] -> Int -> Nabla -> DsM [Nabla]
    generateInhabitingPatterns GenerateInhabitingPatternsMode
    mode [Id]
    xs Int
    n Nabla
    nabla'
          other_cons_nablas <- instantiate_cons x ty xs (n - length con_nablas) nabla cls
          pure (con_nablas ++ other_cons_nablas)

    pickApplicableCompleteSets :: TyState -> Type -> ResidualCompleteMatches -> DsM [CompleteMatch]
    -- See Note [Implementation of COMPLETE pragmas] on what "applicable" means
    pickApplicableCompleteSets :: TyState
    -> Type
    -> ResidualCompleteMatches
    -> IOEnv (Env DsGblEnv DsLclEnv) [CompleteMatch]
    pickApplicableCompleteSets TyState
    ty_st Type
    ty ResidualCompleteMatches
    rcm = do
      let cl_res_ty_ok :: ConLike -> DsM Bool
          cl_res_ty_ok :: ConLike -> DsM Bool
    cl_res_ty_ok ConLike
    cl = do
            env <- DsM FamInstEnvs
    dsGetFamInstEnvs
            isJust <$> matchConLikeResTy env ty_st ty cl
      let cm_applicable :: CompleteMatch -> DsM Bool
          cm_applicable :: CompleteMatch -> DsM Bool
    cm_applicable CompleteMatch
    cm = do
            cls_ok <- (ConLike -> DsM Bool) -> [ConLike] -> DsM Bool
    forall (m :: * -> *) (f :: * -> *) a.
    (Monad m, Foldable f) =>
    (a -> m Bool) -> f a -> m Bool
    allM ConLike -> DsM Bool
    cl_res_ty_ok (UniqDSet ConLike -> [ConLike]
    forall a. UniqDSet a -> [a]
    uniqDSetToList (CompleteMatch -> UniqDSet ConLike
    cmConLikes CompleteMatch
    cm))
            let match_ty_ok = Type -> CompleteMatch -> Bool
    completeMatchAppliesAtType Type
    ty CompleteMatch
    cm
            pure (cls_ok && match_ty_ok)
      applicable_cms <- (CompleteMatch -> DsM Bool)
    -> [CompleteMatch] -> IOEnv (Env DsGblEnv DsLclEnv) [CompleteMatch]
    forall (m :: * -> *) a.
    Applicative m =>
    (a -> m Bool) -> [a] -> m [a]
    filterM CompleteMatch -> DsM Bool
    cm_applicable (ResidualCompleteMatches -> [CompleteMatch]
    getRcm ResidualCompleteMatches
    rcm)
      tracePm "pickApplicableCompleteSets:" $
        vcat
          [ ppr ty
          , ppr rcm
          , ppr applicable_cms
          ]
      return applicable_cms

    {- Note [Why inhabitationTest doesn't call generateInhabitingPatterns]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Why can't we define `inhabitationTest` (IT) in terms of
    `generateInhabitingPatterns` (GIP) as

      inhabitationTest nabla = do
        nablas <- lift $ generateInhabitingPatterns all_variables 1 nabla
        guard (notNull nablas)

    There are a few technical reasons, like the lack of a fuel-tracking approach
    to stay decidable, that could be overcome. But the nail in the coffin is
    performance: In order to provide good warning messages, GIP commits to *one*
    COMPLETE set, and goes through some hoops to find the minimal one. This implies
    it has to look at *all* constructors in the residual COMPLETE matches and see if
    they match, if only to filter out ill-typed COMPLETE sets
    (see Note [Implementation of COMPLETE pragmas]). That is untractable for an
    efficient IT on huge enumerations.

    But we still need GIP to produce the Nablas as proxies for
    uncovered patterns that we display warnings for. It's fine to pay this price
    once at the end, but IT is called far more often than that.

    Note [Case split inhabiting patterns]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    When we have an -XEmptyCase,
    ```hs
    f :: Maybe a -> ()
    f x = case x of {}
    ```
    we want to show the different missing patterns {'Just _', 'Nothing'} to the user
    instead of an uninformative wildcard pattern '_'.

    But when we have a match as part of a function definition, such as
    ```hs
    g :: (Bool, [a]) -> ()
    g (_, []) = ()
    ```
    we established in #20642 that we *do not* want to report P1={'(False, (_:_))',
    '(True, (_:_))'} when we could just give the singleton set P2={'(_, (_:_))'}!
    The latter set M is a "minimal cover" of the space of missing patterns S, in
    that

    1. The union of M is *exactly* S
    2. The size of M is minimal under all such candidates.

    In terms of 'g', P2 satisfies both (1) and (2). While P1 satisfies (1), it does
    not satisfy (2). The set {'_'} satisfies (2), but it does not satisfy (1) as
    it also covers the pattern '(_,[])' which is not part of the space of missing
    patterns of 'g', so it would be a bad (too conservative) suggestion.

    Note that for -XEmptyCase, we don't want to emit a minimal cover. We arrange
    that by passing 'CaseSplitTopLevel' to 'generateInhabitingPatterns'. We detect
    the -XEmptyCase case in 'reportWarnings' by looking for 'ReportEmptyCase'.
    -}