    {-# LANGUAGE ApplicativeDo       #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE ViewPatterns        #-}
    {-# LANGUAGE MultiWayIf          #-}

    -- | Domain types used in "GHC.HsToCore.Pmc.Solver".
    -- The ultimate goal is to define 'Nabla', which models normalised refinement
    -- types from the paper
    -- [Lower Your Guards: A Compositional Pattern-Match Coverage Checker"](https://dl.acm.org/doi/abs/10.1145/3408989).
    module GHC.HsToCore.Pmc.Solver.Types (

            -- * Normalised refinement types
            BotInfo(..), PmAltConApp(..), VarInfo(..), TmState(..), TyState(..),
            Nabla(..), Nablas(..), initNablas,
            lookupRefuts, lookupSolution,

            -- ** Looking up 'VarInfo'
            lookupVarInfo, lookupVarInfoNT, trvVarInfo,

            -- ** Caching residual COMPLETE sets
            CompleteMatch, ResidualCompleteMatches(..), getRcm, isRcmInitialised,

            -- ** Representations for Literals and AltCons
            PmLit(..), PmLitValue(..), PmAltCon(..), pmLitType, pmAltConType,
            isPmAltConMatchStrict, pmAltConImplBangs,

            -- *** PmAltConSet
            PmAltConSet, emptyPmAltConSet, isEmptyPmAltConSet, elemPmAltConSet,
            extendPmAltConSet, pmAltConSetElems,

            -- *** Equality on 'PmAltCon's
            PmEquality(..), eqPmAltCon,

            -- *** Operations on 'PmLit'
            literalToPmLit, negatePmLit, overloadPmLit,
            pmLitAsStringLit, coreExprAsPmLit

        ) where

    import GHC.Prelude

    import GHC.Data.Bag
    import GHC.Data.FastString
    import GHC.Types.Id
    import GHC.Types.Var.Set
    import GHC.Types.Unique.DSet
    import GHC.Types.Unique.SDFM
    import GHC.Types.Name
    import GHC.Core.DataCon
    import GHC.Core.ConLike
    import GHC.Utils.Outputable
    import GHC.Utils.Panic.Plain
    import GHC.Utils.Misc (lastMaybe)
    import GHC.Data.List.SetOps (unionLists)
    import GHC.Data.Maybe
    import GHC.Core.Type
    import GHC.Core.TyCon
    import GHC.Types.Literal
    import GHC.Core
    import GHC.Core.TyCo.Compare( eqType )
    import GHC.Core.Map.Expr
    import GHC.Core.Utils (exprType)
    import GHC.Builtin.Names
    import GHC.Builtin.Types
    import GHC.Builtin.Types.Prim
    import GHC.Tc.Solver.InertSet (InertSet, emptyInert)
    import GHC.Tc.Utils.TcType (isStringTy)
    import GHC.Types.CompleteMatch
    import GHC.Types.SourceText (SourceText(..), mkFractionalLit, FractionalLit
                                , fractionalLitFromRational
                                , FractionalExponentBase(..))
    import Numeric (fromRat)
    import Data.Foldable (find)
    import Data.Ratio
    import GHC.Real (Ratio(..))
    import qualified Data.Semigroup as Semi

    -- import GHC.Driver.Ppr

    --
    -- * Normalised refinement types
    --

    -- | A normalised refinement type ∇ (\"nabla\"), comprised of an inert set of
    -- canonical (i.e. mutually compatible) term and type constraints that form the
    -- refinement type's predicate.
    data Nabla
      = MkNabla
      { Nabla -> TyState
    nabla_ty_st :: !TyState
      -- ^ Type oracle; things like a~Int
      , Nabla -> TmState
    nabla_tm_st :: !TmState
      -- ^ Term oracle; things like x~Nothing
      }

    -- | An initial nabla that is always satisfiable
    initNabla :: Nabla
    initNabla :: Nabla
    initNabla = TyState -> TmState -> Nabla
    MkNabla TyState
    initTyState TmState
    initTmState

    instance Outputable Nabla where
      ppr :: Nabla -> SDoc
    ppr Nabla
    nabla = SDoc -> Int -> SDoc -> SDoc
    hang (String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "Nabla") Int
    2 (SDoc -> SDoc) -> SDoc -> SDoc
    forall a b. (a -> b) -> a -> b
    $ [SDoc] -> SDoc
    forall doc. IsDoc doc => [doc] -> doc
    vcat [
          -- intentionally formatted this way enable the dev to comment in only
          -- the info they need
          TmState -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (Nabla -> TmState
    nabla_tm_st Nabla
    nabla),
          TyState -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (Nabla -> TyState
    nabla_ty_st Nabla
    nabla)
        ]

    -- | A disjunctive bag of 'Nabla's, representing a refinement type.
    newtype Nablas = MkNablas (Bag Nabla)

    initNablas :: Nablas
    initNablas :: Nablas
    initNablas = Bag Nabla -> Nablas
    MkNablas (Nabla -> Bag Nabla
    forall a. a -> Bag a
    unitBag Nabla
    initNabla)

    instance Outputable Nablas where
      ppr :: Nablas -> SDoc
    ppr (MkNablas Bag Nabla
    nablas) = Bag Nabla -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Bag Nabla
    nablas

    instance Semigroup Nablas where
      MkNablas Bag Nabla
    l <> :: Nablas -> Nablas -> Nablas
    <> MkNablas Bag Nabla
    r = Bag Nabla -> Nablas
    MkNablas (Bag Nabla
    l Bag Nabla -> Bag Nabla -> Bag Nabla
    forall a. Bag a -> Bag a -> Bag a
    `unionBags` Bag Nabla
    r)

    instance Monoid Nablas where
      mempty :: Nablas
    mempty = Bag Nabla -> Nablas
    MkNablas Bag Nabla
    forall a. Bag a
    emptyBag

    -- | The type oracle state. An 'GHC.Tc.Solver.Monad.InertSet' that we
    -- incrementally add local type constraints to, together with a sequence
    -- number that counts the number of times we extended it with new facts.
    data TyState = TySt { TyState -> Int
    ty_st_n :: !Int, TyState -> InertSet
    ty_st_inert :: !InertSet }

    -- | Not user-facing.
    instance Outputable TyState where
      ppr :: TyState -> SDoc
    ppr (TySt Int
    n InertSet
    inert) = Int -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Int
    n SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> InertSet -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr InertSet
    inert

    initTyState :: TyState
    initTyState :: TyState
    initTyState = Int -> InertSet -> TyState
    TySt Int
    0 InertSet
    emptyInert

    -- | The term oracle state. Stores 'VarInfo' for encountered 'Id's. These
    -- entries are possibly shared when we figure out that two variables must be
    -- equal, thus represent the same set of values.
    --
    -- See Note [TmState invariants] in "GHC.HsToCore.Pmc.Solver".
    data TmState
      = TmSt
      { TmState -> UniqSDFM Id VarInfo
    ts_facts :: !(UniqSDFM Id VarInfo)
      -- ^ Facts about term variables. Deterministic env, so that we generate
      -- deterministic error messages.
      , TmState -> CoreMap Id
    ts_reps  :: !(CoreMap Id)
      -- ^ An environment for looking up whether we already encountered semantically
      -- equivalent expressions that we want to represent by the same 'Id'
      -- representative.
      , TmState -> DIdSet
    ts_dirty :: !DIdSet
      -- ^ Which 'VarInfo' needs to be checked for inhabitants because of new
      -- negative constraints (e.g. @x ≁ ⊥@ or @x ≁ K@).
      }

    -- | Information about an 'Id'. Stores positive ('vi_pos') facts, like @x ~ Just 42@,
    -- and negative ('vi_neg') facts, like "x is not (:)".
    -- Also caches the type ('vi_ty'), the 'ResidualCompleteMatches' of a COMPLETE set
    -- ('vi_rcm').
    --
    -- Subject to Note [The Pos/Neg invariant] in "GHC.HsToCore.Pmc.Solver".
    data VarInfo
      = VI
      { VarInfo -> Id
    vi_id  :: !Id
      -- ^ The 'Id' in question. Important for adding new constraints relative to
      -- this 'VarInfo' when we don't easily have the 'Id' available.

      , VarInfo -> [PmAltConApp]
    vi_pos :: ![PmAltConApp]
      -- ^ Positive info: 'PmAltCon' apps it is (i.e. @x ~ [Just y, PatSyn z]@), all
      -- at the same time (i.e. conjunctive).  We need a list because of nested
      -- pattern matches involving pattern synonym
      --    case x of { Just y -> case x of PatSyn z -> ... }
      -- However, no more than one RealDataCon in the list, otherwise contradiction
      -- because of generativity.

      , VarInfo -> PmAltConSet
    vi_neg :: !PmAltConSet
      -- ^ Negative info: A list of 'PmAltCon's that it cannot match.
      -- Example, assuming
      --
      -- @
      --     data T = Leaf Int | Branch T T | Node Int T
      -- @
      --
      -- then @x ≁ [Leaf, Node]@ means that @x@ cannot match a @Leaf@ or @Node@,
      -- and hence can only match @Branch@. Is orthogonal to anything from 'vi_pos',
      -- in the sense that 'eqPmAltCon' returns @PossiblyOverlap@ for any pairing
      -- between 'vi_pos' and 'vi_neg'.

      -- See Note [Why record both positive and negative info?]
      -- It's worth having an actual set rather than a simple association list,
      -- because files like Cabal's `LicenseId` define relatively huge enums
      -- that lead to quadratic or worse behavior.

      , VarInfo -> BotInfo
    vi_bot :: BotInfo
      -- ^ Can this variable be ⊥? Models (mutually contradicting) @x ~ ⊥@ and
      --   @x ≁ ⊥@ constraints. E.g.
      --    * 'MaybeBot': Don't know; Neither @x ~ ⊥@ nor @x ≁ ⊥@.
      --    * 'IsBot': @x ~ ⊥@
      --    * 'IsNotBot': @x ≁ ⊥@

      , VarInfo -> ResidualCompleteMatches
    vi_rcm :: !ResidualCompleteMatches
      -- ^ A cache of the associated COMPLETE sets. At any time a superset of
      -- possible constructors of each COMPLETE set. So, if it's not in here, we
      -- can't possibly match on it. Complementary to 'vi_neg'. We still need it
      -- to recognise completion of a COMPLETE set efficiently for large enums.
      }

    data PmAltConApp
      = PACA
      { PmAltConApp -> PmAltCon
    paca_con :: !PmAltCon
      , PmAltConApp -> [Id]
    paca_tvs :: ![TyVar]
      , PmAltConApp -> [Id]
    paca_ids :: ![Id]
      }

    -- | See 'vi_bot'.
    data BotInfo
      = IsBot
      | IsNotBot
      | MaybeBot
      deriving BotInfo -> BotInfo -> Bool
    (BotInfo -> BotInfo -> Bool)
    -> (BotInfo -> BotInfo -> Bool) -> Eq BotInfo
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: BotInfo -> BotInfo -> Bool
    == :: BotInfo -> BotInfo -> Bool
    $c/= :: BotInfo -> BotInfo -> Bool
    /= :: BotInfo -> BotInfo -> Bool
    Eq

    instance Outputable PmAltConApp where
      ppr :: PmAltConApp -> SDoc
    ppr PACA{paca_con :: PmAltConApp -> PmAltCon
    paca_con = PmAltCon
    con, paca_tvs :: PmAltConApp -> [Id]
    paca_tvs = [Id]
    tvs, paca_ids :: PmAltConApp -> [Id]
    paca_ids = [Id]
    ids} =
        [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]
    : (Id -> SDoc) -> [Id] -> [SDoc]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Char -> SDoc
    forall doc. IsLine doc => Char -> doc
    char Char
    '@' SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <>) (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 [SDoc] -> [SDoc] -> [SDoc]
    forall a. [a] -> [a] -> [a]
    ++ (Id -> SDoc) -> [Id] -> [SDoc]
    forall a b. (a -> b) -> [a] -> [b]
    map Id -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr [Id]
    ids)

    instance Outputable BotInfo where
      ppr :: BotInfo -> SDoc
    ppr BotInfo
    MaybeBot = SDoc
    forall doc. IsLine doc => doc
    underscore
      ppr BotInfo
    IsBot    = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "~⊥"
      ppr BotInfo
    IsNotBot = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "≁⊥"

    -- | Not user-facing.
    instance Outputable TmState where
      ppr :: TmState -> SDoc
    ppr (TmSt UniqSDFM Id VarInfo
    state CoreMap Id
    reps DIdSet
    dirty) = UniqSDFM Id VarInfo -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr UniqSDFM Id VarInfo
    state SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$ CoreMap Id -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr CoreMap Id
    reps SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$ DIdSet -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr DIdSet
    dirty

    -- | Not user-facing.
    instance Outputable VarInfo where
      ppr :: VarInfo -> SDoc
    ppr (VI Id
    x [PmAltConApp]
    pos PmAltConSet
    neg BotInfo
    bot ResidualCompleteMatches
    cache)
        = SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc
    braces ([SDoc] -> SDoc
    forall doc. IsLine doc => [doc] -> doc
    hcat (SDoc -> [SDoc] -> [SDoc]
    forall doc. IsLine doc => doc -> [doc] -> [doc]
    punctuate SDoc
    forall doc. IsLine doc => doc
    comma [SDoc
    pp_x, SDoc
    pp_pos, SDoc
    pp_neg, BotInfo -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr BotInfo
    bot, SDoc
    pp_cache]))
        where
          pp_x :: SDoc
    pp_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
    <> Kind -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (Id -> Kind
    idType Id
    x)
          pp_pos :: SDoc
    pp_pos
            | [] <- [PmAltConApp]
    pos  = SDoc
    forall doc. IsLine doc => doc
    underscore
            | [PmAltConApp
    p] <- [PmAltConApp]
    pos = Char -> SDoc
    forall doc. IsLine doc => Char -> doc
    char Char
    '~' SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <> PmAltConApp -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr PmAltConApp
    p -- suppress outer [_] if singleton
            | Bool
    otherwise  = Char -> SDoc
    forall doc. IsLine doc => Char -> doc
    char Char
    '~' SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <> [PmAltConApp] -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr [PmAltConApp]
    pos
          pp_neg :: SDoc
    pp_neg
            | PmAltConSet -> Bool
    isEmptyPmAltConSet PmAltConSet
    neg = SDoc
    forall doc. IsLine doc => doc
    underscore
            | Bool
    otherwise              = Char -> SDoc
    forall doc. IsLine doc => Char -> doc
    char Char
    '≁' SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <> PmAltConSet -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr PmAltConSet
    neg
          pp_cache :: SDoc
    pp_cache
            | RCM Maybe DsCompleteMatch
    Nothing Maybe DsCompleteMatches
    Nothing <- ResidualCompleteMatches
    cache = SDoc
    forall doc. IsLine doc => doc
    underscore
            | Bool
    otherwise                    = ResidualCompleteMatches -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ResidualCompleteMatches
    cache

    -- | Initial state of the term oracle.
    initTmState :: TmState
    initTmState :: TmState
    initTmState = UniqSDFM Id VarInfo -> CoreMap Id -> DIdSet -> TmState
    TmSt UniqSDFM Id VarInfo
    forall key ele. UniqSDFM key ele
    emptyUSDFM CoreMap Id
    forall a. CoreMap a
    emptyCoreMap DIdSet
    emptyDVarSet

    -- | A data type that caches for the 'VarInfo' of @x@ the results of querying
    -- 'dsGetCompleteMatches' and then striking out all occurrences of @K@ for
    -- which we already know @x ≁ K@ from these sets.
    --
    -- For motivation, see Section 5.3 in Lower Your Guards.
    -- See also Note [Implementation of COMPLETE pragmas]
    data ResidualCompleteMatches
      = RCM
      { ResidualCompleteMatches -> Maybe DsCompleteMatch
    rcm_vanilla :: !(Maybe DsCompleteMatch)
      -- ^ The residual set for the vanilla COMPLETE set from the data defn.
      -- Tracked separately from 'rcm_pragmas', because it might only be
      -- known much later (when we have enough type information to see the 'TyCon'
      -- of the match), or not at all even. Until that happens, it is 'Nothing'.
      , ResidualCompleteMatches -> Maybe DsCompleteMatches
    rcm_pragmas :: !(Maybe DsCompleteMatches)
      -- ^ The residual sets for /all/ COMPLETE sets from pragmas that are
      -- visible when compiling this module. Querying that set with
      -- 'dsGetCompleteMatches' requires 'DsM', so we initialise it with 'Nothing'
      -- until first needed in a 'DsM' context.
      }

    getRcm :: ResidualCompleteMatches -> DsCompleteMatches
    getRcm :: ResidualCompleteMatches -> DsCompleteMatches
    getRcm (RCM Maybe DsCompleteMatch
    vanilla Maybe DsCompleteMatches
    pragmas) = Maybe DsCompleteMatch -> DsCompleteMatches
    forall a. Maybe a -> [a]
    maybeToList Maybe DsCompleteMatch
    vanilla DsCompleteMatches -> DsCompleteMatches -> DsCompleteMatches
    forall a. [a] -> [a] -> [a]
    ++ DsCompleteMatches -> Maybe DsCompleteMatches -> DsCompleteMatches
    forall a. a -> Maybe a -> a
    fromMaybe [] Maybe DsCompleteMatches
    pragmas

    isRcmInitialised :: ResidualCompleteMatches -> Bool
    isRcmInitialised :: ResidualCompleteMatches -> Bool
    isRcmInitialised (RCM Maybe DsCompleteMatch
    vanilla Maybe DsCompleteMatches
    pragmas) = Maybe DsCompleteMatch -> Bool
    forall a. Maybe a -> Bool
    isJust Maybe DsCompleteMatch
    vanilla Bool -> Bool -> Bool
    && Maybe DsCompleteMatches -> Bool
    forall a. Maybe a -> Bool
    isJust Maybe DsCompleteMatches
    pragmas

    instance Outputable ResidualCompleteMatches where
      -- formats as "[{Nothing,Just},{P,Q}]"
      ppr :: ResidualCompleteMatches -> SDoc
    ppr ResidualCompleteMatches
    rcm = DsCompleteMatches -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (ResidualCompleteMatches -> DsCompleteMatches
    getRcm ResidualCompleteMatches
    rcm)

    -----------------------
    -- * Looking up VarInfo

    emptyRCM :: ResidualCompleteMatches
    emptyRCM :: ResidualCompleteMatches
    emptyRCM = Maybe DsCompleteMatch
    -> Maybe DsCompleteMatches -> ResidualCompleteMatches
    RCM Maybe DsCompleteMatch
    forall a. Maybe a
    Nothing Maybe DsCompleteMatches
    forall a. Maybe a
    Nothing

    emptyVarInfo :: Id -> VarInfo
    emptyVarInfo :: Id -> VarInfo
    emptyVarInfo Id
    x
      = VI
      { vi_id :: Id
    vi_id = Id
    x
      , vi_pos :: [PmAltConApp]
    vi_pos = []
      , vi_neg :: PmAltConSet
    vi_neg = PmAltConSet
    emptyPmAltConSet
      -- Why not set IsNotBot for unlifted type here?
      -- Because we'd have to trigger an inhabitation test, which we can't.
      -- See case (4) in Note [Strict fields and variables of unlifted type]
      -- in GHC.HsToCore.Pmc.Solver
      , vi_bot :: BotInfo
    vi_bot = BotInfo
    MaybeBot
      , vi_rcm :: ResidualCompleteMatches
    vi_rcm = ResidualCompleteMatches
    emptyRCM
      }

    lookupVarInfo :: TmState -> Id -> VarInfo
    -- (lookupVarInfo tms x) tells what we know about 'x'
    lookupVarInfo :: TmState -> Id -> VarInfo
    lookupVarInfo (TmSt UniqSDFM Id VarInfo
    env CoreMap Id
    _ DIdSet
    _) Id
    x = VarInfo -> Maybe VarInfo -> VarInfo
    forall a. a -> Maybe a -> a
    fromMaybe (Id -> VarInfo
    emptyVarInfo Id
    x) (UniqSDFM Id VarInfo -> Id -> Maybe VarInfo
    forall key ele.
    Uniquable key =>
    UniqSDFM key ele -> key -> Maybe ele
    lookupUSDFM UniqSDFM Id VarInfo
    env Id
    x)

    -- | Like @lookupVarInfo ts x@, but @lookupVarInfo ts x = (y, vi)@ also looks
    -- through newtype constructors. We have @x ~ N1 (... (Nk y))@ such that the
    -- returned @y@ doesn't have a positive newtype constructor constraint
    -- associated with it (yet). The 'VarInfo' returned is that of @y@'s
    -- representative.
    --
    -- Careful, this means that @idType x@ might be different to @idType y@, even
    -- modulo type normalisation!
    --
    -- See also Note [Coverage checking Newtype matches] in GHC.HsToCore.Pmc.Solver.
    lookupVarInfoNT :: TmState -> Id -> (Id, VarInfo)
    lookupVarInfoNT :: TmState -> Id -> (Id, VarInfo)
    lookupVarInfoNT TmState
    ts Id
    x = case TmState -> Id -> VarInfo
    lookupVarInfo TmState
    ts Id
    x of
      VI{ vi_pos :: VarInfo -> [PmAltConApp]
    vi_pos = [PmAltConApp] -> Maybe Id
    as_newtype -> Just Id
    y } -> TmState -> Id -> (Id, VarInfo)
    lookupVarInfoNT TmState
    ts Id
    y
      VarInfo
    res                                 -> (Id
    x, VarInfo
    res)
      where
        as_newtype :: [PmAltConApp] -> Maybe Id
    as_newtype = [Id] -> Maybe Id
    forall a. [a] -> Maybe a
    listToMaybe ([Id] -> Maybe Id)
    -> ([PmAltConApp] -> [Id]) -> [PmAltConApp] -> Maybe Id
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (PmAltConApp -> Maybe Id) -> [PmAltConApp] -> [Id]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe PmAltConApp -> Maybe Id
    go
        go :: PmAltConApp -> Maybe Id
    go PACA{paca_con :: PmAltConApp -> PmAltCon
    paca_con = PmAltConLike (RealDataCon DataCon
    dc), paca_ids :: PmAltConApp -> [Id]
    paca_ids = [Id
    y]}
          | DataCon -> Bool
    isNewDataCon DataCon
    dc = Id -> Maybe Id
    forall a. a -> Maybe a
    Just Id
    y
        go PmAltConApp
    _                = Maybe Id
    forall a. Maybe a
    Nothing

    trvVarInfo :: Functor f => (VarInfo -> f (a, VarInfo)) -> Nabla -> Id -> f (a, Nabla)
    {-# INLINE trvVarInfo #-}
    -- This function is called a lot and we want to specilise it, not only
    -- for the type class, but also for its 'f' function argument.
    -- Before the INLINE pragma it sometimes inlined and sometimes didn't,
    -- depending delicately on GHC's optimisations.  Better to use a pragma.
    trvVarInfo :: forall (f :: * -> *) a.
    Functor f =>
    (VarInfo -> f (a, VarInfo)) -> Nabla -> Id -> f (a, Nabla)
    trvVarInfo VarInfo -> f (a, VarInfo)
    f 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
      = (a, VarInfo) -> (a, Nabla)
    set_vi ((a, VarInfo) -> (a, Nabla)) -> f (a, VarInfo) -> f (a, Nabla)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> VarInfo -> f (a, VarInfo)
    f (TmState -> Id -> VarInfo
    lookupVarInfo TmState
    ts Id
    x)
      where
        set_vi :: (a, VarInfo) -> (a, Nabla)
    set_vi (a
    a, VarInfo
    vi') =
          (a
    a, Nabla
    nabla{ nabla_tm_st = ts{ ts_facts = addToUSDFM env (vi_id vi') vi' } })

    ------------------------------------------------
    -- * Exported utility functions querying 'Nabla'

    lookupRefuts :: Nabla -> Id -> [PmAltCon]
    -- Unfortunately we need the extra bit of polymorphism and the unfortunate
    -- duplication of lookupVarInfo here.
    lookupRefuts :: Nabla -> Id -> [PmAltCon]
    lookupRefuts MkNabla{ nabla_tm_st :: Nabla -> TmState
    nabla_tm_st = TmState
    ts } Id
    x =
      PmAltConSet -> [PmAltCon]
    pmAltConSetElems (PmAltConSet -> [PmAltCon]) -> PmAltConSet -> [PmAltCon]
    forall a b. (a -> b) -> a -> b
    $ VarInfo -> PmAltConSet
    vi_neg (VarInfo -> PmAltConSet) -> VarInfo -> PmAltConSet
    forall a b. (a -> b) -> a -> b
    $ TmState -> Id -> VarInfo
    lookupVarInfo TmState
    ts Id
    x

    isDataConSolution :: PmAltConApp -> Bool
    isDataConSolution :: PmAltConApp -> Bool
    isDataConSolution PACA{paca_con :: PmAltConApp -> PmAltCon
    paca_con = PmAltConLike (RealDataCon DataCon
    _)} = Bool
    True
    isDataConSolution PmAltConApp
    _                                             = Bool
    False

    -- @lookupSolution nabla x@ picks a single solution ('vi_pos') of @x@ from
    -- possibly many, preferring 'RealDataCon' solutions whenever possible.
    lookupSolution :: Nabla -> Id -> Maybe PmAltConApp
    lookupSolution :: Nabla -> Id -> Maybe PmAltConApp
    lookupSolution Nabla
    nabla Id
    x = case VarInfo -> [PmAltConApp]
    vi_pos (TmState -> Id -> VarInfo
    lookupVarInfo (Nabla -> TmState
    nabla_tm_st Nabla
    nabla) Id
    x) of
      []                                         -> Maybe PmAltConApp
    forall a. Maybe a
    Nothing
      pos :: [PmAltConApp]
    pos@(PmAltConApp
    x:[PmAltConApp]
    _)
        | Just PmAltConApp
    sol <- (PmAltConApp -> Bool) -> [PmAltConApp] -> Maybe PmAltConApp
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    find PmAltConApp -> Bool
    isDataConSolution [PmAltConApp]
    pos -> PmAltConApp -> Maybe PmAltConApp
    forall a. a -> Maybe a
    Just PmAltConApp
    sol
        | Bool
    otherwise                              -> PmAltConApp -> Maybe PmAltConApp
    forall a. a -> Maybe a
    Just PmAltConApp
    x

    --------------------------------------------------------------------------------
    -- The rest is just providing an IR for (overloaded!) literals and AltCons that
    -- sits between Hs and Core. We need a reliable way to detect and determine
    -- equality between them, which is impossible with Hs (too expressive) and with
    -- Core (no notion of overloaded literals, and even plain 'Int' literals are
    -- actually constructor apps). Also String literals are troublesome.

    -- | Literals (simple and overloaded ones) for pattern match checking.
    --
    -- See Note [Undecidable Equality for PmAltCons]
    data PmLit = PmLit
               { PmLit -> Kind
    pm_lit_ty  :: Type
               , PmLit -> PmLitValue
    pm_lit_val :: PmLitValue }

    data PmLitValue
      = PmLitInt Integer
      | PmLitRat Rational
      | PmLitChar Char
      -- We won't actually see PmLitString in the oracle since we desugar strings to
      -- lists
      | PmLitString FastString
      | PmLitOverInt Int {- How often Negated? -} Integer
      | PmLitOverRat Int {- How often Negated? -} FractionalLit
      | PmLitOverString FastString

    -- | Undecidable semantic equality result.
    -- See Note [Undecidable Equality for PmAltCons]
    data PmEquality
      = Equal
      | Disjoint
      | PossiblyOverlap
      deriving (PmEquality -> PmEquality -> Bool
    (PmEquality -> PmEquality -> Bool)
    -> (PmEquality -> PmEquality -> Bool) -> Eq PmEquality
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: PmEquality -> PmEquality -> Bool
    == :: PmEquality -> PmEquality -> Bool
    $c/= :: PmEquality -> PmEquality -> Bool
    /= :: PmEquality -> PmEquality -> Bool
    Eq, Int -> PmEquality -> ShowS
    [PmEquality] -> ShowS
    PmEquality -> String
    (Int -> PmEquality -> ShowS)
    -> (PmEquality -> String)
    -> ([PmEquality] -> ShowS)
    -> Show PmEquality
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> PmEquality -> ShowS
    showsPrec :: Int -> PmEquality -> ShowS
    $cshow :: PmEquality -> String
    show :: PmEquality -> String
    $cshowList :: [PmEquality] -> ShowS
    showList :: [PmEquality] -> ShowS
    Show)

    -- | When 'PmEquality' can be decided. @True <=> Equal@, @False <=> Disjoint@.
    decEquality :: Bool -> PmEquality
    decEquality :: Bool -> PmEquality
    decEquality Bool
    True  = PmEquality
    Equal
    decEquality Bool
    False = PmEquality
    Disjoint

    -- | Undecidable equality for values represented by 'PmLit's.
    -- See Note [Undecidable Equality for PmAltCons]
    --
    -- * @Just True@ ==> Surely equal
    -- * @Just False@ ==> Surely different (non-overlapping, even!)
    -- * @Nothing@ ==> Equality relation undecidable
    eqPmLit :: PmLit -> PmLit -> PmEquality
    eqPmLit :: PmLit -> PmLit -> PmEquality
    eqPmLit (PmLit Kind
    t1 PmLitValue
    v1) (PmLit Kind
    t2 PmLitValue
    v2)
      -- no haddock | pprTrace "eqPmLit" (ppr t1 <+> ppr v1 $$ ppr t2 <+> ppr v2) False = undefined
      | Bool -> Bool
    not (Kind
    t1 HasCallStack => Kind -> Kind -> Bool
    Kind -> Kind -> Bool
    `eqType` Kind
    t2) = PmEquality
    Disjoint
      | Bool
    otherwise            = PmLitValue -> PmLitValue -> PmEquality
    go PmLitValue
    v1 PmLitValue
    v2
      where
        go :: PmLitValue -> PmLitValue -> PmEquality
    go (PmLitInt Integer
    i1)        (PmLitInt Integer
    i2)        = Bool -> PmEquality
    decEquality (Integer
    i1 Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    i2)
        go (PmLitRat Rational
    r1)        (PmLitRat Rational
    r2)        = Bool -> PmEquality
    decEquality (Rational
    r1 Rational -> Rational -> Bool
    forall a. Eq a => a -> a -> Bool
    == Rational
    r2)
        go (PmLitChar Char
    c1)       (PmLitChar Char
    c2)       = Bool -> PmEquality
    decEquality (Char
    c1 Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    c2)
        go (PmLitString FastString
    s1)     (PmLitString FastString
    s2)     = Bool -> PmEquality
    decEquality (FastString
    s1 FastString -> FastString -> Bool
    forall a. Eq a => a -> a -> Bool
    == FastString
    s2)
        go (PmLitOverInt Int
    n1 Integer
    i1) (PmLitOverInt Int
    n2 Integer
    i2)
          | Int
    n1 Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    n2 Bool -> Bool -> Bool
    && Integer
    i1 Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    i2                     = PmEquality
    Equal
        go (PmLitOverRat Int
    n1 FractionalLit
    r1) (PmLitOverRat Int
    n2 FractionalLit
    r2)
          | Int
    n1 Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    n2 Bool -> Bool -> Bool
    && FractionalLit
    r1 FractionalLit -> FractionalLit -> Bool
    forall a. Eq a => a -> a -> Bool
    == FractionalLit
    r2                     = PmEquality
    Equal
        go (PmLitOverString FastString
    s1) (PmLitOverString FastString
    s2)
          | FastString
    s1 FastString -> FastString -> Bool
    forall a. Eq a => a -> a -> Bool
    == FastString
    s2                                 = PmEquality
    Equal
        go PmLitValue
    _                    PmLitValue
    _                    = PmEquality
    PossiblyOverlap

    -- | Syntactic equality.
    instance Eq PmLit where
      PmLit
    a == :: PmLit -> PmLit -> Bool
    == PmLit
    b = PmLit -> PmLit -> PmEquality
    eqPmLit PmLit
    a PmLit
    b PmEquality -> PmEquality -> Bool
    forall a. Eq a => a -> a -> Bool
    == PmEquality
    Equal

    -- | Type of a 'PmLit'
    pmLitType :: PmLit -> Type
    pmLitType :: PmLit -> Kind
    pmLitType (PmLit Kind
    ty PmLitValue
    _) = Kind
    ty

    -- | Undecidable equality for values represented by 'ConLike's.
    -- See Note [Undecidable Equality for PmAltCons].
    -- 'PatSynCon's aren't enforced to be generative, so two syntactically different
    -- 'PatSynCon's might match the exact same values. Without looking into and
    -- reasoning about the pattern synonym's definition, we can't decide if their
    -- sets of matched values is different.
    --
    -- * @Just True@ ==> Surely equal
    -- * @Just False@ ==> Surely different (non-overlapping, even!)
    -- * @Nothing@ ==> Equality relation undecidable
    eqConLike :: ConLike -> ConLike -> PmEquality
    eqConLike :: ConLike -> ConLike -> PmEquality
    eqConLike (RealDataCon DataCon
    dc1) (RealDataCon DataCon
    dc2) = Bool -> PmEquality
    decEquality (DataCon
    dc1 DataCon -> DataCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == DataCon
    dc2)
    eqConLike (PatSynCon PatSyn
    psc1)  (PatSynCon PatSyn
    psc2)
      | PatSyn
    psc1 PatSyn -> PatSyn -> Bool
    forall a. Eq a => a -> a -> Bool
    == PatSyn
    psc2
      = PmEquality
    Equal
    eqConLike ConLike
    _                 ConLike
    _                 = PmEquality
    PossiblyOverlap

    -- | Represents the head of a match against a 'ConLike' or literal.
    -- Really similar to 'GHC.Core.AltCon'.
    data PmAltCon = PmAltConLike ConLike
                  | PmAltLit     PmLit

    data PmAltConSet = PACS !(UniqDSet ConLike) ![PmLit]

    emptyPmAltConSet :: PmAltConSet
    emptyPmAltConSet :: PmAltConSet
    emptyPmAltConSet = UniqDSet ConLike -> [PmLit] -> PmAltConSet
    PACS UniqDSet ConLike
    forall a. UniqDSet a
    emptyUniqDSet []

    isEmptyPmAltConSet :: PmAltConSet -> Bool
    isEmptyPmAltConSet :: PmAltConSet -> Bool
    isEmptyPmAltConSet (PACS UniqDSet ConLike
    cls [PmLit]
    lits) = UniqDSet ConLike -> Bool
    forall a. UniqDSet a -> Bool
    isEmptyUniqDSet UniqDSet ConLike
    cls Bool -> Bool -> Bool
    && [PmLit] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [PmLit]
    lits

    -- | Whether there is a 'PmAltCon' in the 'PmAltConSet' that compares 'Equal' to
    -- the given 'PmAltCon' according to 'eqPmAltCon'.
    elemPmAltConSet :: PmAltCon -> PmAltConSet -> Bool
    elemPmAltConSet :: PmAltCon -> PmAltConSet -> Bool
    elemPmAltConSet (PmAltConLike ConLike
    cl) (PACS UniqDSet ConLike
    cls [PmLit]
    _   ) = ConLike -> UniqDSet ConLike -> Bool
    forall a. Uniquable a => a -> UniqDSet a -> Bool
    elementOfUniqDSet ConLike
    cl UniqDSet ConLike
    cls
    elemPmAltConSet (PmAltLit PmLit
    lit)    (PACS UniqDSet ConLike
    _   [PmLit]
    lits) = PmLit -> [PmLit] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    elem PmLit
    lit [PmLit]
    lits

    extendPmAltConSet :: PmAltConSet -> PmAltCon -> PmAltConSet
    extendPmAltConSet :: PmAltConSet -> PmAltCon -> PmAltConSet
    extendPmAltConSet (PACS UniqDSet ConLike
    cls [PmLit]
    lits) (PmAltConLike ConLike
    cl)
      = UniqDSet ConLike -> [PmLit] -> PmAltConSet
    PACS (UniqDSet ConLike -> ConLike -> UniqDSet ConLike
    forall a. Uniquable a => UniqDSet a -> a -> UniqDSet a
    addOneToUniqDSet UniqDSet ConLike
    cls ConLike
    cl) [PmLit]
    lits
    extendPmAltConSet (PACS UniqDSet ConLike
    cls [PmLit]
    lits) (PmAltLit PmLit
    lit)
      = UniqDSet ConLike -> [PmLit] -> PmAltConSet
    PACS UniqDSet ConLike
    cls ([PmLit] -> [PmLit] -> [PmLit]
    forall a.
    (HasDebugCallStack, Outputable a, Eq a) =>
    [a] -> [a] -> [a]
    unionLists [PmLit]
    lits [PmLit
    lit])

    pmAltConSetElems :: PmAltConSet -> [PmAltCon]
    pmAltConSetElems :: PmAltConSet -> [PmAltCon]
    pmAltConSetElems (PACS UniqDSet ConLike
    cls [PmLit]
    lits)
      = (ConLike -> PmAltCon) -> [ConLike] -> [PmAltCon]
    forall a b. (a -> b) -> [a] -> [b]
    map ConLike -> PmAltCon
    PmAltConLike (UniqDSet ConLike -> [ConLike]
    forall a. UniqDSet a -> [a]
    uniqDSetToList UniqDSet ConLike
    cls) [PmAltCon] -> [PmAltCon] -> [PmAltCon]
    forall a. [a] -> [a] -> [a]
    ++ (PmLit -> PmAltCon) -> [PmLit] -> [PmAltCon]
    forall a b. (a -> b) -> [a] -> [b]
    map PmLit -> PmAltCon
    PmAltLit [PmLit]
    lits

    instance Outputable PmAltConSet where
      ppr :: PmAltConSet -> SDoc
    ppr = [PmAltCon] -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ([PmAltCon] -> SDoc)
    -> (PmAltConSet -> [PmAltCon]) -> PmAltConSet -> SDoc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PmAltConSet -> [PmAltCon]
    pmAltConSetElems

    -- | We can't in general decide whether two 'PmAltCon's match the same set of
    -- values. In addition to the reasons in 'eqPmLit' and 'eqConLike', a
    -- 'PmAltConLike' might or might not represent the same value as a 'PmAltLit'.
    -- See Note [Undecidable Equality for PmAltCons].
    --
    -- * @Just True@ ==> Surely equal
    -- * @Just False@ ==> Surely different (non-overlapping, even!)
    -- * @Nothing@ ==> Equality relation undecidable
    --
    -- Examples (omitting some constructor wrapping):
    --
    -- * @eqPmAltCon (LitInt 42) (LitInt 1) == Just False@: Lit equality is
    --   decidable
    -- * @eqPmAltCon (DataCon A) (DataCon B) == Just False@: DataCon equality is
    --   decidable
    -- * @eqPmAltCon (LitOverInt 42) (LitOverInt 1) == Nothing@: OverLit equality
    --   is undecidable
    -- * @eqPmAltCon (PatSyn PA) (PatSyn PB) == Nothing@: PatSyn equality is
    --   undecidable
    -- * @eqPmAltCon (DataCon I#) (LitInt 1) == Nothing@: DataCon to Lit
    --   comparisons are undecidable without reasoning about the wrapped @Int#@
    -- * @eqPmAltCon (LitOverInt 1) (LitOverInt 1) == Just True@: We assume
    --   reflexivity for overloaded literals
    -- * @eqPmAltCon (PatSyn PA) (PatSyn PA) == Just True@: We assume reflexivity
    --   for Pattern Synonyms
    eqPmAltCon :: PmAltCon -> PmAltCon -> PmEquality
    eqPmAltCon :: PmAltCon -> PmAltCon -> PmEquality
    eqPmAltCon (PmAltConLike ConLike
    cl1) (PmAltConLike ConLike
    cl2) = ConLike -> ConLike -> PmEquality
    eqConLike ConLike
    cl1 ConLike
    cl2
    eqPmAltCon (PmAltLit     PmLit
    l1)  (PmAltLit     PmLit
    l2)  = PmLit -> PmLit -> PmEquality
    eqPmLit PmLit
    l1 PmLit
    l2
    eqPmAltCon PmAltCon
    _                  PmAltCon
    _                  = PmEquality
    PossiblyOverlap

    -- | Syntactic equality.
    instance Eq PmAltCon where
      PmAltCon
    a == :: PmAltCon -> PmAltCon -> Bool
    == PmAltCon
    b = PmAltCon -> PmAltCon -> PmEquality
    eqPmAltCon PmAltCon
    a PmAltCon
    b PmEquality -> PmEquality -> Bool
    forall a. Eq a => a -> a -> Bool
    == PmEquality
    Equal

    -- | Type of a 'PmAltCon'
    pmAltConType :: PmAltCon -> [Type] -> Type
    pmAltConType :: PmAltCon -> [Kind] -> Kind
    pmAltConType (PmAltLit PmLit
    lit)     [Kind]
    _arg_tys = Bool -> Kind -> Kind
    forall a. HasCallStack => Bool -> a -> a
    assert ([Kind] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Kind]
    _arg_tys ) (Kind -> Kind) -> Kind -> Kind
    forall a b. (a -> b) -> a -> b
    $ PmLit -> Kind
    pmLitType PmLit
    lit
    pmAltConType (PmAltConLike ConLike
    con) [Kind]
    arg_tys  = ConLike -> [Kind] -> Kind
    conLikeResTy ConLike
    con [Kind]
    arg_tys

    -- | Is a match on this constructor forcing the match variable?
    -- True of data constructors, literals and pattern synonyms (#17357), but not of
    -- newtypes.
    -- See Note [Coverage checking Newtype matches] in GHC.HsToCore.Pmc.Solver.
    isPmAltConMatchStrict :: PmAltCon -> Bool
    isPmAltConMatchStrict :: PmAltCon -> Bool
    isPmAltConMatchStrict PmAltLit{}                      = Bool
    True
    isPmAltConMatchStrict (PmAltConLike PatSynCon{})      = Bool
    True -- #17357
    isPmAltConMatchStrict (PmAltConLike (RealDataCon DataCon
    dc)) = Bool -> Bool
    not (DataCon -> Bool
    isNewDataCon DataCon
    dc)

    pmAltConImplBangs :: PmAltCon -> [HsImplBang]
    pmAltConImplBangs :: PmAltCon -> [HsImplBang]
    pmAltConImplBangs PmAltLit{}         = []
    pmAltConImplBangs (PmAltConLike ConLike
    con) = ConLike -> [HsImplBang]
    conLikeImplBangs ConLike
    con

    {- Note [Undecidable Equality for PmAltCons]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Equality on overloaded literals is undecidable in the general case. Consider
    the following example:

      instance Num Bool where
        ...
        fromInteger 0 = False -- C-like representation of booleans
        fromInteger _ = True

        f :: Bool -> ()
        f 1 = ()        -- Clause A
        f 2 = ()        -- Clause B

    Clause B is redundant but to detect this, we must decide the constraint:
    @fromInteger 2 ~ fromInteger 1@ which means that we
    have to look through function @fromInteger@, whose implementation could
    be anything. This poses difficulties for:

    1. The expressive power of the check.
       We cannot expect a reasonable implementation of pattern matching to detect
       that @fromInteger 2 ~ fromInteger 1@ is True, unless we unfold function
       fromInteger. This puts termination at risk and is undecidable in the
       general case.

    2. Error messages/Warnings.
       What should our message for @f@ above be? A reasonable approach would be
       to issue:

         Pattern matches are (potentially) redundant:
           f 2 = ...    under the assumption that 1 == 2

       but seems to complex and confusing for the user.

    We choose to equate only obviously equal overloaded literals, in all other cases
    we signal undecidability by returning Nothing from 'eqPmAltCons'. We do
    better for non-overloaded literals, because we know their fromInteger/fromString
    implementation is actually injective, allowing us to simplify the constraint
    @fromInteger 1 ~ fromInteger 2@ to @1 ~ 2@, which is trivially unsatisfiable.

    The impact of this treatment of overloaded literals is the following:

      * Redundancy checking is rather conservative, since it cannot see that clause
        B above is redundant.

      * We have instant equality check for overloaded literals (we do not rely on
        the term oracle which is rather expensive, both in terms of performance and
        memory). This significantly improves the performance of functions `covered`
        `uncovered` and `divergent` in "GHC.HsToCore.Pmc" and effectively addresses
        #11161.

      * The warnings issued are simpler.

    Similar reasoning applies to pattern synonyms: In contrast to data constructors,
    which are generative, constraints like F a ~ G b for two different pattern
    synonyms F and G aren't immediately unsatisfiable. We assume F a ~ F a, though.
    -}

    literalToPmLit :: Type -> Literal -> Maybe PmLit
    literalToPmLit :: Kind -> Literal -> Maybe PmLit
    literalToPmLit Kind
    ty Literal
    l = Kind -> PmLitValue -> PmLit
    PmLit Kind
    ty (PmLitValue -> PmLit) -> Maybe PmLitValue -> Maybe PmLit
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Literal -> Maybe PmLitValue
    go Literal
    l
      where
        go :: Literal -> Maybe PmLitValue
    go (LitChar Char
    c)       = PmLitValue -> Maybe PmLitValue
    forall a. a -> Maybe a
    Just (Char -> PmLitValue
    PmLitChar Char
    c)
        go (LitFloat Rational
    r)      = PmLitValue -> Maybe PmLitValue
    forall a. a -> Maybe a
    Just (Rational -> PmLitValue
    PmLitRat Rational
    r)
        go (LitDouble Rational
    r)     = PmLitValue -> Maybe PmLitValue
    forall a. a -> Maybe a
    Just (Rational -> PmLitValue
    PmLitRat Rational
    r)
        go (LitString ByteString
    s)     = PmLitValue -> Maybe PmLitValue
    forall a. a -> Maybe a
    Just (FastString -> PmLitValue
    PmLitString (ByteString -> FastString
    mkFastStringByteString ByteString
    s))
        go (LitNumber LitNumType
    _ Integer
    i)   = PmLitValue -> Maybe PmLitValue
    forall a. a -> Maybe a
    Just (Integer -> PmLitValue
    PmLitInt Integer
    i)
        go Literal
    _                 = Maybe PmLitValue
    forall a. Maybe a
    Nothing

    negatePmLit :: PmLit -> Maybe PmLit
    negatePmLit :: PmLit -> Maybe PmLit
    negatePmLit (PmLit Kind
    ty PmLitValue
    v) = Kind -> PmLitValue -> PmLit
    PmLit Kind
    ty (PmLitValue -> PmLit) -> Maybe PmLitValue -> Maybe PmLit
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PmLitValue -> Maybe PmLitValue
    go PmLitValue
    v
      where
        go :: PmLitValue -> Maybe PmLitValue
    go (PmLitInt Integer
    i)       = PmLitValue -> Maybe PmLitValue
    forall a. a -> Maybe a
    Just (Integer -> PmLitValue
    PmLitInt (-Integer
    i))
        go (PmLitRat Rational
    r)       = PmLitValue -> Maybe PmLitValue
    forall a. a -> Maybe a
    Just (Rational -> PmLitValue
    PmLitRat (-Rational
    r))
        go (PmLitOverInt Int
    n Integer
    i) = PmLitValue -> Maybe PmLitValue
    forall a. a -> Maybe a
    Just (Int -> Integer -> PmLitValue
    PmLitOverInt (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) Integer
    i)
        go (PmLitOverRat Int
    n FractionalLit
    r) = PmLitValue -> Maybe PmLitValue
    forall a. a -> Maybe a
    Just (Int -> FractionalLit -> PmLitValue
    PmLitOverRat (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) FractionalLit
    r)
        go PmLitValue
    _                  = Maybe PmLitValue
    forall a. Maybe a
    Nothing

    overloadPmLit :: Type -> PmLit -> Maybe PmLit
    overloadPmLit :: Kind -> PmLit -> Maybe PmLit
    overloadPmLit Kind
    ty (PmLit Kind
    _ PmLitValue
    v) = Kind -> PmLitValue -> PmLit
    PmLit Kind
    ty (PmLitValue -> PmLit) -> Maybe PmLitValue -> Maybe PmLit
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PmLitValue -> Maybe PmLitValue
    go PmLitValue
    v
      where
        go :: PmLitValue -> Maybe PmLitValue
    go (PmLitInt Integer
    i)          = PmLitValue -> Maybe PmLitValue
    forall a. a -> Maybe a
    Just (Int -> Integer -> PmLitValue
    PmLitOverInt Int
    0 Integer
    i)
        go (PmLitRat Rational
    r)          = PmLitValue -> Maybe PmLitValue
    forall a. a -> Maybe a
    Just (PmLitValue -> Maybe PmLitValue) -> PmLitValue -> Maybe PmLitValue
    forall a b. (a -> b) -> a -> b
    $! Int -> FractionalLit -> PmLitValue
    PmLitOverRat Int
    0 (FractionalLit -> PmLitValue) -> FractionalLit -> PmLitValue
    forall a b. (a -> b) -> a -> b
    $! Rational -> FractionalLit
    fractionalLitFromRational Rational
    r
        go (PmLitString FastString
    s)
          | Kind
    ty HasCallStack => Kind -> Kind -> Bool
    Kind -> Kind -> Bool
    `eqType` Kind
    stringTy = PmLitValue -> Maybe PmLitValue
    forall a. a -> Maybe a
    Just PmLitValue
    v
          | Bool
    otherwise            = PmLitValue -> Maybe PmLitValue
    forall a. a -> Maybe a
    Just (FastString -> PmLitValue
    PmLitOverString FastString
    s)
        go ovRat :: PmLitValue
    ovRat@PmLitOverRat{}  = PmLitValue -> Maybe PmLitValue
    forall a. a -> Maybe a
    Just PmLitValue
    ovRat
        go PmLitValue
    _               = Maybe PmLitValue
    forall a. Maybe a
    Nothing

    pmLitAsStringLit :: PmLit -> Maybe FastString
    pmLitAsStringLit :: PmLit -> Maybe FastString
    pmLitAsStringLit (PmLit Kind
    _ (PmLitString FastString
    s)) = FastString -> Maybe FastString
    forall a. a -> Maybe a
    Just FastString
    s
    pmLitAsStringLit PmLit
    _                         = Maybe FastString
    forall a. Maybe a
    Nothing

    coreExprAsPmLit :: CoreExpr -> Maybe PmLit
    -- coreExprAsPmLit e | pprTrace "coreExprAsPmLit" (ppr e) False = undefined
    coreExprAsPmLit :: CoreExpr -> Maybe PmLit
    coreExprAsPmLit (Tick CoreTickish
    _t CoreExpr
    e) = CoreExpr -> Maybe PmLit
    coreExprAsPmLit CoreExpr
    e
    coreExprAsPmLit (Lit Literal
    l) = Kind -> Literal -> Maybe PmLit
    literalToPmLit (Literal -> Kind
    literalType Literal
    l) Literal
    l
    coreExprAsPmLit CoreExpr
    e = case CoreExpr -> (CoreExpr, [CoreExpr])
    forall b. Expr b -> (Expr b, [Expr b])
    collectArgs CoreExpr
    e of
      (Var Id
    x, [Lit Literal
    l])
        | Just DataCon
    dc <- Id -> Maybe DataCon
    isDataConWorkId_maybe Id
    x
        , DataCon
    dc DataCon -> [DataCon] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [DataCon
    intDataCon, DataCon
    wordDataCon, DataCon
    charDataCon, DataCon
    floatDataCon, DataCon
    doubleDataCon]
        -> Kind -> Literal -> Maybe PmLit
    literalToPmLit (HasDebugCallStack => CoreExpr -> Kind
    CoreExpr -> Kind
    exprType CoreExpr
    e) Literal
    l
      (Var Id
    x, [Lit (LitNumber LitNumType
    _ Integer
    l)])
        | Just (Kind
    ty,Integer
    l) <- Id -> Integer -> Maybe (Kind, Integer)
    forall {b}. Num b => Id -> b -> Maybe (Kind, b)
    bignum_lit_maybe Id
    x Integer
    l
        -> PmLit -> Maybe PmLit
    forall a. a -> Maybe a
    Just (Kind -> PmLitValue -> PmLit
    PmLit Kind
    ty (Integer -> PmLitValue
    PmLitInt Integer
    l))
      (Var Id
    x, [CoreExpr
    _ty, CoreExpr
    n_arg, CoreExpr
    d_arg])
        | Just DataCon
    dc <- Id -> Maybe DataCon
    isDataConWorkId_maybe Id
    x
        , DataCon -> Name
    dataConName DataCon
    dc Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name
    ratioDataConName
        , Just (PmLit Kind
    _ (PmLitInt Integer
    n)) <- CoreExpr -> Maybe PmLit
    coreExprAsPmLit CoreExpr
    n_arg
        , Just (PmLit Kind
    _ (PmLitInt Integer
    d)) <- CoreExpr -> Maybe PmLit
    coreExprAsPmLit CoreExpr
    d_arg
        -- HACK: just assume we have a literal double. This case only occurs for
        --       overloaded lits anyway, so we immediately override type information
        -> Kind -> Literal -> Maybe PmLit
    literalToPmLit (HasDebugCallStack => CoreExpr -> Kind
    CoreExpr -> Kind
    exprType CoreExpr
    e) (Rational -> Literal
    mkLitDouble (Integer
    n Integer -> Integer -> Rational
    forall a. Integral a => a -> a -> Ratio a
    % Integer
    d))

      (Var Id
    x, [CoreExpr]
    args)
        -- See Note [Detecting overloaded literals with -XRebindableSyntax]
        | Id -> Name -> Bool
    is_rebound_name Id
    x Name
    fromIntegerName
        , Just CoreExpr
    arg <- [CoreExpr] -> Maybe CoreExpr
    forall a. [a] -> Maybe a
    lastMaybe [CoreExpr]
    args
        , Just (Kind
    _ty,Integer
    l) <- CoreExpr -> Maybe (Kind, Integer)
    forall {b}. Expr b -> Maybe (Kind, Integer)
    bignum_conapp_maybe CoreExpr
    arg
        -> PmLit -> Maybe PmLit
    forall a. a -> Maybe a
    Just (Kind -> PmLitValue -> PmLit
    PmLit Kind
    integerTy (Integer -> PmLitValue
    PmLitInt Integer
    l)) Maybe PmLit -> (PmLit -> Maybe PmLit) -> Maybe PmLit
    forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Kind -> PmLit -> Maybe PmLit
    overloadPmLit (HasDebugCallStack => CoreExpr -> Kind
    CoreExpr -> Kind
    exprType CoreExpr
    e)
      (Var Id
    x, [CoreExpr]
    args)
        -- See Note [Detecting overloaded literals with -XRebindableSyntax]
        -- fromRational <expr>
        | Id -> Name -> Bool
    is_rebound_name Id
    x Name
    fromRationalName
        , [CoreExpr
    r] <- (CoreExpr -> Bool) -> [CoreExpr] -> [CoreExpr]
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile (Bool -> Bool
    not (Bool -> Bool) -> (CoreExpr -> Bool) -> CoreExpr -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CoreExpr -> Bool
    is_ratio) [CoreExpr]
    args
        -> CoreExpr -> Maybe PmLit
    coreExprAsPmLit CoreExpr
    r Maybe PmLit -> (PmLit -> Maybe PmLit) -> Maybe PmLit
    forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Kind -> PmLit -> Maybe PmLit
    overloadPmLit (HasDebugCallStack => CoreExpr -> Kind
    CoreExpr -> Kind
    exprType CoreExpr
    e)

      --Rationals with large exponents
      (Var Id
    x, [CoreExpr]
    args)
        -- See Note [Detecting overloaded literals with -XRebindableSyntax]
        -- See Note [Dealing with rationals with large exponents]
        -- mkRationalBase* <rational> <exponent>
        | Just FractionalExponentBase
    exp_base <- Id -> Maybe FractionalExponentBase
    is_larg_exp_ratio Id
    x
        , [CoreExpr
    r, CoreExpr
    exp] <- (CoreExpr -> Bool) -> [CoreExpr] -> [CoreExpr]
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile (Bool -> Bool
    not (Bool -> Bool) -> (CoreExpr -> Bool) -> CoreExpr -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CoreExpr -> Bool
    is_ratio) [CoreExpr]
    args
        , (Var Id
    x, [CoreExpr
    _ty, CoreExpr
    n_arg, CoreExpr
    d_arg]) <- CoreExpr -> (CoreExpr, [CoreExpr])
    forall b. Expr b -> (Expr b, [Expr b])
    collectArgs CoreExpr
    r
        , Just DataCon
    dc <- Id -> Maybe DataCon
    isDataConWorkId_maybe Id
    x
        , DataCon -> Name
    dataConName DataCon
    dc Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name
    ratioDataConName
        , Just (PmLit Kind
    _ (PmLitInt Integer
    n)) <- CoreExpr -> Maybe PmLit
    coreExprAsPmLit CoreExpr
    n_arg
        , Just (PmLit Kind
    _ (PmLitInt Integer
    d)) <- CoreExpr -> Maybe PmLit
    coreExprAsPmLit CoreExpr
    d_arg
        , Just (Kind
    _exp_ty,Integer
    exp') <- CoreExpr -> Maybe (Kind, Integer)
    forall {b}. Expr b -> Maybe (Kind, Integer)
    bignum_conapp_maybe CoreExpr
    exp
        -> do
          let rational :: Rational
    rational = (Integer -> Integer
    forall a. Num a => a -> a
    abs Integer
    n) Integer -> Integer -> Rational
    forall a. a -> a -> Ratio a
    :% Integer
    d
          let neg :: Int
    neg = if Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    0 then Int
    1 else Int
    0
          let frac :: FractionalLit
    frac = SourceText
    -> Bool
    -> Rational
    -> Integer
    -> FractionalExponentBase
    -> FractionalLit
    mkFractionalLit SourceText
    NoSourceText Bool
    False Rational
    rational Integer
    exp' FractionalExponentBase
    exp_base
          PmLit -> Maybe PmLit
    forall a. a -> Maybe a
    Just (PmLit -> Maybe PmLit) -> PmLit -> Maybe PmLit
    forall a b. (a -> b) -> a -> b
    $ Kind -> PmLitValue -> PmLit
    PmLit (HasDebugCallStack => CoreExpr -> Kind
    CoreExpr -> Kind
    exprType CoreExpr
    e) (Int -> FractionalLit -> PmLitValue
    PmLitOverRat Int
    neg FractionalLit
    frac)

      (Var Id
    x, [CoreExpr]
    args)
        | Id -> Name -> Bool
    is_rebound_name Id
    x Name
    fromStringName
        -- See Note [Detecting overloaded literals with -XRebindableSyntax]
        , CoreExpr
    s:[CoreExpr]
    _ <- (CoreExpr -> Bool) -> [CoreExpr] -> [CoreExpr]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Kind -> Bool
    isStringTy (Kind -> Bool) -> (CoreExpr -> Kind) -> CoreExpr -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . HasDebugCallStack => CoreExpr -> Kind
    CoreExpr -> Kind
    exprType) ([CoreExpr] -> [CoreExpr]) -> [CoreExpr] -> [CoreExpr]
    forall a b. (a -> b) -> a -> b
    $ (CoreExpr -> Bool) -> [CoreExpr] -> [CoreExpr]
    forall a. (a -> Bool) -> [a] -> [a]
    filter CoreExpr -> Bool
    forall b. Expr b -> Bool
    isValArg [CoreExpr]
    args
        -- NB: Calls coreExprAsPmLit and then overloadPmLit, so that we return PmLitOverStrings
        -> CoreExpr -> Maybe PmLit
    coreExprAsPmLit CoreExpr
    s Maybe PmLit -> (PmLit -> Maybe PmLit) -> Maybe PmLit
    forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Kind -> PmLit -> Maybe PmLit
    overloadPmLit (HasDebugCallStack => CoreExpr -> Kind
    CoreExpr -> Kind
    exprType CoreExpr
    e)
      -- These last two cases handle proper String literals
      (Var Id
    x, [Type Kind
    ty])
        | Just DataCon
    dc <- Id -> Maybe DataCon
    isDataConWorkId_maybe Id
    x
        , DataCon
    dc DataCon -> DataCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == DataCon
    nilDataCon
        , Kind
    ty HasCallStack => Kind -> Kind -> Bool
    Kind -> Kind -> Bool
    `eqType` Kind
    charTy
        -> Kind -> Literal -> Maybe PmLit
    literalToPmLit Kind
    stringTy (String -> Literal
    mkLitString String
    "")
      (Var Id
    x, [Lit Literal
    l])
        | Id -> Name
    idName Id
    x Name -> [Name] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Name
    unpackCStringName, Name
    unpackCStringUtf8Name]
        -> Kind -> Literal -> Maybe PmLit
    literalToPmLit Kind
    stringTy Literal
    l

      (CoreExpr, [CoreExpr])
    _ -> Maybe PmLit
    forall a. Maybe a
    Nothing
      where
        bignum_conapp_maybe :: Expr b -> Maybe (Kind, Integer)
    bignum_conapp_maybe (App (Var Id
    x) (Lit (LitNumber LitNumType
    _ Integer
    l)))
          = Id -> Integer -> Maybe (Kind, Integer)
    forall {b}. Num b => Id -> b -> Maybe (Kind, b)
    bignum_lit_maybe Id
    x Integer
    l
        bignum_conapp_maybe Expr b
    _ = Maybe (Kind, Integer)
    forall a. Maybe a
    Nothing

        bignum_lit_maybe :: Id -> b -> Maybe (Kind, b)
    bignum_lit_maybe Id
    x b
    l
          | Just DataCon
    dc <- Id -> Maybe DataCon
    isDataConWorkId_maybe Id
    x
          = if | DataCon
    dc DataCon -> DataCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == DataCon
    integerISDataCon -> (Kind, b) -> Maybe (Kind, b)
    forall a. a -> Maybe a
    Just (Kind
    integerTy,b
    l)
               | DataCon
    dc DataCon -> DataCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == DataCon
    integerIPDataCon -> (Kind, b) -> Maybe (Kind, b)
    forall a. a -> Maybe a
    Just (Kind
    integerTy,b
    l)
               | DataCon
    dc DataCon -> DataCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == DataCon
    integerINDataCon -> (Kind, b) -> Maybe (Kind, b)
    forall a. a -> Maybe a
    Just (Kind
    integerTy,b -> b
    forall a. Num a => a -> a
    negate b
    l)
               | DataCon
    dc DataCon -> DataCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == DataCon
    naturalNSDataCon -> (Kind, b) -> Maybe (Kind, b)
    forall a. a -> Maybe a
    Just (Kind
    naturalTy,b
    l)
               | DataCon
    dc DataCon -> DataCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == DataCon
    naturalNBDataCon -> (Kind, b) -> Maybe (Kind, b)
    forall a. a -> Maybe a
    Just (Kind
    naturalTy,b
    l)
               | Bool
    otherwise              -> Maybe (Kind, b)
    forall a. Maybe a
    Nothing
        bignum_lit_maybe Id
    _ b
    _ = Maybe (Kind, b)
    forall a. Maybe a
    Nothing

        is_ratio :: CoreExpr -> Bool
    is_ratio (Type Kind
    _) = Bool
    False
        is_ratio CoreExpr
    r
          | Just (TyCon
    tc, [Kind]
    _) <- HasDebugCallStack => Kind -> Maybe (TyCon, [Kind])
    Kind -> Maybe (TyCon, [Kind])
    splitTyConApp_maybe (HasDebugCallStack => CoreExpr -> Kind
    CoreExpr -> Kind
    exprType CoreExpr
    r)
          = TyCon -> Name
    tyConName TyCon
    tc Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name
    ratioTyConName
          | Bool
    otherwise
          = Bool
    False
        is_larg_exp_ratio :: Id -> Maybe FractionalExponentBase
    is_larg_exp_ratio Id
    x
          | Id -> Name -> Bool
    is_rebound_name Id
    x Name
    mkRationalBase10Name
          = FractionalExponentBase -> Maybe FractionalExponentBase
    forall a. a -> Maybe a
    Just FractionalExponentBase
    Base10
          | Id -> Name -> Bool
    is_rebound_name Id
    x Name
    mkRationalBase2Name
          = FractionalExponentBase -> Maybe FractionalExponentBase
    forall a. a -> Maybe a
    Just FractionalExponentBase
    Base2
          | Bool
    otherwise
          = Maybe FractionalExponentBase
    forall a. Maybe a
    Nothing

        -- See Note [Detecting overloaded literals with -XRebindableSyntax]
        is_rebound_name :: Id -> Name -> Bool
        is_rebound_name :: Id -> Name -> Bool
    is_rebound_name Id
    x Name
    n = Name -> FastString
    forall a. NamedThing a => a -> FastString
    getOccFS (Id -> Name
    idName Id
    x) FastString -> FastString -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name -> FastString
    forall a. NamedThing a => a -> FastString
    getOccFS Name
    n

    {- Note [Detecting overloaded literals with -XRebindableSyntax]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Normally, we'd find e.g. overloaded string literals by comparing the
    application head of an expression to `fromStringName`. But that doesn't work
    with -XRebindableSyntax: The `Name` of a user-provided `fromString` function is
    different to `fromStringName`, which lives in a certain module, etc.

    There really is no other way than to compare `OccName`s and guess which
    argument is the actual literal string (we assume it's the first argument of
    type `String`).

    The same applies to other overloaded literals, such as overloaded rationals
    (`fromRational`)and overloaded integer literals (`fromInteger`).

    Note [Dealing with rationals with large exponents]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Rationals with large exponents are *not* desugared to
    a simple rational. As that would require us to compute
    their value which can be expensive. Rather they desugar
    to an expression. For example 1e1000 will desugar to an
    expression of the form: `mkRationalWithExponentBase10 (1 :% 1) 1000`

    Only overloaded literals desugar to this form however, so we
    we can just return a overloaded rational literal.

    The most complex case is if we have RebindableSyntax enabled.
    By example if we have a pattern like this: `f 3.3 = True`

    It will desugar to:
      fromRational
        [TYPE: Rational, mkRationalBase10 (:% @Integer 10 1) (-1)]

    The fromRational is properly detected as an overloaded Rational by
    coreExprAsPmLit and it's general code for detecting overloaded rationals.
    See Note [Detecting overloaded literals with -XRebindableSyntax].

    This case then recurses into coreExprAsPmLit passing only the expression
    `mkRationalBase10 (:% @Integer 10 1) (-1)`. Which is caught by rationals
    with large exponents case. This will return a `PmLitOverRat` literal.

    Which is then passed to overloadPmLit which simply returns it as-is since
    it's already overloaded.

    -}

    instance Outputable PmLitValue where
      ppr :: PmLitValue -> SDoc
    ppr (PmLitInt Integer
    i)        = Integer -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Integer
    i
      ppr (PmLitRat Rational
    r)        = Double -> SDoc
    forall doc. IsLine doc => Double -> doc
    double (Rational -> Double
    forall a. RealFloat a => Rational -> a
    fromRat Rational
    r) -- good enough
      ppr (PmLitChar Char
    c)       = Char -> SDoc
    pprHsChar Char
    c
      ppr (PmLitString FastString
    s)     = FastString -> SDoc
    pprHsString FastString
    s
      ppr (PmLitOverInt Int
    n Integer
    i)  = Int -> SDoc -> SDoc
    minuses Int
    n (Integer -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Integer
    i)
      ppr (PmLitOverRat Int
    n FractionalLit
    r)  = Int -> SDoc -> SDoc
    minuses Int
    n (FractionalLit -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr FractionalLit
    r)
      ppr (PmLitOverString FastString
    s) = FastString -> SDoc
    pprHsString FastString
    s

    -- Take care of negated literals
    minuses :: Int -> SDoc -> SDoc
    minuses :: Int -> SDoc -> SDoc
    minuses Int
    n SDoc
    sdoc = (SDoc -> SDoc) -> SDoc -> [SDoc]
    forall a. (a -> a) -> a -> [a]
    iterate (\SDoc
    sdoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc
    parens (Char -> SDoc
    forall doc. IsLine doc => Char -> doc
    char Char
    '-' SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <> SDoc
    sdoc)) SDoc
    sdoc [SDoc] -> Int -> SDoc
    forall a. HasCallStack => [a] -> Int -> a
    !! Int
    n

    instance Outputable PmLit where
      ppr :: PmLit -> SDoc
    ppr (PmLit Kind
    ty PmLitValue
    v) = PmLitValue -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr PmLitValue
    v SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <> SDoc
    suffix
        where
          -- Some ad-hoc hackery for displaying proper lit suffixes based on type
          tbl :: [(Kind, SDoc)]
    tbl = [ (Kind
    intPrimTy, SDoc
    primIntSuffix)
                , (Kind
    int64PrimTy, SDoc
    primInt64Suffix)
                , (Kind
    wordPrimTy, SDoc
    primWordSuffix)
                , (Kind
    word64PrimTy, SDoc
    primWord64Suffix)
                , (Kind
    charPrimTy, SDoc
    primCharSuffix)
                , (Kind
    floatPrimTy, SDoc
    primFloatSuffix)
                , (Kind
    doublePrimTy, SDoc
    primDoubleSuffix) ]
          suffix :: SDoc
    suffix = SDoc -> Maybe SDoc -> SDoc
    forall a. a -> Maybe a -> a
    fromMaybe SDoc
    forall doc. IsOutput doc => doc
    empty ((Kind, SDoc) -> SDoc
    forall a b. (a, b) -> b
    snd ((Kind, SDoc) -> SDoc) -> Maybe (Kind, SDoc) -> Maybe SDoc
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((Kind, SDoc) -> Bool) -> [(Kind, SDoc)] -> Maybe (Kind, SDoc)
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    find (HasCallStack => Kind -> Kind -> Bool
    Kind -> Kind -> Bool
    eqType Kind
    ty (Kind -> Bool) -> ((Kind, SDoc) -> Kind) -> (Kind, SDoc) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Kind, SDoc) -> Kind
    forall a b. (a, b) -> a
    fst) [(Kind, SDoc)]
    tbl)

    instance Outputable PmAltCon where
      ppr :: PmAltCon -> SDoc
    ppr (PmAltConLike ConLike
    cl) = ConLike -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ConLike
    cl
      ppr (PmAltLit PmLit
    l)      = PmLit -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr PmLit
    l

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