never executed always true always false
    1 {-# LANGUAGE ApplicativeDo       #-}
    2 {-# LANGUAGE ScopedTypeVariables #-}
    3 {-# LANGUAGE ViewPatterns        #-}
    4 {-# LANGUAGE MultiWayIf          #-}
    5 
    6 -- | Domain types used in "GHC.HsToCore.Pmc.Solver".
    7 -- The ultimate goal is to define 'Nabla', which models normalised refinement
    8 -- types from the paper
    9 -- [Lower Your Guards: A Compositional Pattern-Match Coverage Checker"](https://dl.acm.org/doi/abs/10.1145/3408989).
   10 module GHC.HsToCore.Pmc.Solver.Types (
   11 
   12         -- * Normalised refinement types
   13         BotInfo(..), PmAltConApp(..), VarInfo(..), TmState(..), TyState(..),
   14         Nabla(..), Nablas(..), initNablas,
   15         lookupRefuts, lookupSolution,
   16 
   17         -- ** Looking up 'VarInfo'
   18         lookupVarInfo, lookupVarInfoNT, trvVarInfo,
   19 
   20         -- ** Caching residual COMPLETE sets
   21         CompleteMatch, ResidualCompleteMatches(..), getRcm, isRcmInitialised,
   22 
   23         -- ** Representations for Literals and AltCons
   24         PmLit(..), PmLitValue(..), PmAltCon(..), pmLitType, pmAltConType,
   25         isPmAltConMatchStrict, pmAltConImplBangs,
   26 
   27         -- *** PmAltConSet
   28         PmAltConSet, emptyPmAltConSet, isEmptyPmAltConSet, elemPmAltConSet,
   29         extendPmAltConSet, pmAltConSetElems,
   30 
   31         -- *** Equality on 'PmAltCon's
   32         PmEquality(..), eqPmAltCon,
   33 
   34         -- *** Operations on 'PmLit'
   35         literalToPmLit, negatePmLit, overloadPmLit,
   36         pmLitAsStringLit, coreExprAsPmLit
   37 
   38     ) where
   39 
   40 import GHC.Prelude
   41 
   42 import GHC.Data.Bag
   43 import GHC.Data.FastString
   44 import GHC.Types.Id
   45 import GHC.Types.Var.Set
   46 import GHC.Types.Unique.DSet
   47 import GHC.Types.Unique.SDFM
   48 import GHC.Types.Name
   49 import GHC.Core.DataCon
   50 import GHC.Core.ConLike
   51 import GHC.Utils.Outputable
   52 import GHC.Utils.Panic.Plain
   53 import GHC.Utils.Misc (lastMaybe)
   54 import GHC.Data.List.SetOps (unionLists)
   55 import GHC.Data.Maybe
   56 import GHC.Core.Type
   57 import GHC.Core.TyCon
   58 import GHC.Types.Literal
   59 import GHC.Core
   60 import GHC.Core.Map.Expr
   61 import GHC.Core.Utils (exprType)
   62 import GHC.Builtin.Names
   63 import GHC.Builtin.Types
   64 import GHC.Builtin.Types.Prim
   65 import GHC.Tc.Solver.InertSet (InertSet, emptyInert)
   66 import GHC.Tc.Utils.TcType (isStringTy)
   67 import GHC.Types.CompleteMatch (CompleteMatch(..))
   68 import GHC.Types.SourceText (SourceText(..), mkFractionalLit, FractionalLit
   69                             , fractionalLitFromRational
   70                             , FractionalExponentBase(..))
   71 import Numeric (fromRat)
   72 import Data.Foldable (find)
   73 import Data.Ratio
   74 import GHC.Real (Ratio(..))
   75 import qualified Data.Semigroup as Semi
   76 
   77 -- import GHC.Driver.Ppr
   78 
   79 --
   80 -- * Normalised refinement types
   81 --
   82 
   83 -- | A normalised refinement type ∇ (\"nabla\"), comprised of an inert set of
   84 -- canonical (i.e. mutually compatible) term and type constraints that form the
   85 -- refinement type's predicate.
   86 data Nabla
   87   = MkNabla
   88   { nabla_ty_st :: !TyState
   89   -- ^ Type oracle; things like a~Int
   90   , nabla_tm_st :: !TmState
   91   -- ^ Term oracle; things like x~Nothing
   92   }
   93 
   94 -- | An initial nabla that is always satisfiable
   95 initNabla :: Nabla
   96 initNabla = MkNabla initTyState initTmState
   97 
   98 instance Outputable Nabla where
   99   ppr nabla = hang (text "Nabla") 2 $ vcat [
  100       -- intentionally formatted this way enable the dev to comment in only
  101       -- the info they need
  102       ppr (nabla_tm_st nabla),
  103       ppr (nabla_ty_st nabla)
  104     ]
  105 
  106 -- | A disjunctive bag of 'Nabla's, representing a refinement type.
  107 newtype Nablas = MkNablas (Bag Nabla)
  108 
  109 initNablas :: Nablas
  110 initNablas = MkNablas (unitBag initNabla)
  111 
  112 instance Outputable Nablas where
  113   ppr (MkNablas nablas) = ppr nablas
  114 
  115 instance Semigroup Nablas where
  116   MkNablas l <> MkNablas r = MkNablas (l `unionBags` r)
  117 
  118 instance Monoid Nablas where
  119   mempty = MkNablas emptyBag
  120 
  121 -- | The type oracle state. An 'GHC.Tc.Solver.Monad.InertSet' that we
  122 -- incrementally add local type constraints to, together with a sequence
  123 -- number that counts the number of times we extended it with new facts.
  124 data TyState = TySt { ty_st_n :: !Int, ty_st_inert :: !InertSet }
  125 
  126 -- | Not user-facing.
  127 instance Outputable TyState where
  128   ppr (TySt n inert) = ppr n <+> ppr inert
  129 
  130 initTyState :: TyState
  131 initTyState = TySt 0 emptyInert
  132 
  133 -- | The term oracle state. Stores 'VarInfo' for encountered 'Id's. These
  134 -- entries are possibly shared when we figure out that two variables must be
  135 -- equal, thus represent the same set of values.
  136 --
  137 -- See Note [TmState invariants] in "GHC.HsToCore.Pmc.Solver".
  138 data TmState
  139   = TmSt
  140   { ts_facts :: !(UniqSDFM Id VarInfo)
  141   -- ^ Facts about term variables. Deterministic env, so that we generate
  142   -- deterministic error messages.
  143   , ts_reps  :: !(CoreMap Id)
  144   -- ^ An environment for looking up whether we already encountered semantically
  145   -- equivalent expressions that we want to represent by the same 'Id'
  146   -- representative.
  147   , ts_dirty :: !DIdSet
  148   -- ^ Which 'VarInfo' needs to be checked for inhabitants because of new
  149   -- negative constraints (e.g. @x ≁ ⊥@ or @x ≁ K@).
  150   }
  151 
  152 -- | Information about an 'Id'. Stores positive ('vi_pos') facts, like @x ~ Just 42@,
  153 -- and negative ('vi_neg') facts, like "x is not (:)".
  154 -- Also caches the type ('vi_ty'), the 'ResidualCompleteMatches' of a COMPLETE set
  155 -- ('vi_rcm').
  156 --
  157 -- Subject to Note [The Pos/Neg invariant] in "GHC.HsToCore.Pmc.Solver".
  158 data VarInfo
  159   = VI
  160   { vi_id  :: !Id
  161   -- ^ The 'Id' in question. Important for adding new constraints relative to
  162   -- this 'VarInfo' when we don't easily have the 'Id' available.
  163 
  164   , vi_pos :: ![PmAltConApp]
  165   -- ^ Positive info: 'PmAltCon' apps it is (i.e. @x ~ [Just y, PatSyn z]@), all
  166   -- at the same time (i.e. conjunctive).  We need a list because of nested
  167   -- pattern matches involving pattern synonym
  168   --    case x of { Just y -> case x of PatSyn z -> ... }
  169   -- However, no more than one RealDataCon in the list, otherwise contradiction
  170   -- because of generativity.
  171 
  172   , vi_neg :: !PmAltConSet
  173   -- ^ Negative info: A list of 'PmAltCon's that it cannot match.
  174   -- Example, assuming
  175   --
  176   -- @
  177   --     data T = Leaf Int | Branch T T | Node Int T
  178   -- @
  179   --
  180   -- then @x ≁ [Leaf, Node]@ means that @x@ cannot match a @Leaf@ or @Node@,
  181   -- and hence can only match @Branch@. Is orthogonal to anything from 'vi_pos',
  182   -- in the sense that 'eqPmAltCon' returns @PossiblyOverlap@ for any pairing
  183   -- between 'vi_pos' and 'vi_neg'.
  184 
  185   -- See Note [Why record both positive and negative info?]
  186   -- It's worth having an actual set rather than a simple association list,
  187   -- because files like Cabal's `LicenseId` define relatively huge enums
  188   -- that lead to quadratic or worse behavior.
  189 
  190   , vi_bot :: BotInfo
  191   -- ^ Can this variable be ⊥? Models (mutually contradicting) @x ~ ⊥@ and
  192   --   @x ≁ ⊥@ constraints. E.g.
  193   --    * 'MaybeBot': Don't know; Neither @x ~ ⊥@ nor @x ≁ ⊥@.
  194   --    * 'IsBot': @x ~ ⊥@
  195   --    * 'IsNotBot': @x ≁ ⊥@
  196 
  197   , vi_rcm :: !ResidualCompleteMatches
  198   -- ^ A cache of the associated COMPLETE sets. At any time a superset of
  199   -- possible constructors of each COMPLETE set. So, if it's not in here, we
  200   -- can't possibly match on it. Complementary to 'vi_neg'. We still need it
  201   -- to recognise completion of a COMPLETE set efficiently for large enums.
  202   }
  203 
  204 data PmAltConApp
  205   = PACA
  206   { paca_con :: !PmAltCon
  207   , paca_tvs :: ![TyVar]
  208   , paca_ids :: ![Id]
  209   }
  210 
  211 -- | See 'vi_bot'.
  212 data BotInfo
  213   = IsBot
  214   | IsNotBot
  215   | MaybeBot
  216   deriving Eq
  217 
  218 instance Outputable PmAltConApp where
  219   ppr PACA{paca_con = con, paca_tvs = tvs, paca_ids = ids} =
  220     hsep (ppr con : map ((char '@' <>) . ppr) tvs ++ map ppr ids)
  221 
  222 instance Outputable BotInfo where
  223   ppr MaybeBot = underscore
  224   ppr IsBot    = text "~⊥"
  225   ppr IsNotBot = text "≁⊥"
  226 
  227 -- | Not user-facing.
  228 instance Outputable TmState where
  229   ppr (TmSt state reps dirty) = ppr state $$ ppr reps $$ ppr dirty
  230 
  231 -- | Not user-facing.
  232 instance Outputable VarInfo where
  233   ppr (VI x pos neg bot cache)
  234     = braces (hcat (punctuate comma [pp_x, pp_pos, pp_neg, ppr bot, pp_cache]))
  235     where
  236       pp_x = ppr x <> dcolon <> ppr (idType x)
  237       pp_pos
  238         | [] <- pos  = underscore
  239         | [p] <- pos = char '~' <> ppr p -- suppress outer [_] if singleton
  240         | otherwise  = char '~' <> ppr pos
  241       pp_neg
  242         | isEmptyPmAltConSet neg = underscore
  243         | otherwise              = char '≁' <> ppr neg
  244       pp_cache
  245         | RCM Nothing Nothing <- cache = underscore
  246         | otherwise                    = ppr cache
  247 
  248 -- | Initial state of the term oracle.
  249 initTmState :: TmState
  250 initTmState = TmSt emptyUSDFM emptyCoreMap emptyDVarSet
  251 
  252 -- | A data type that caches for the 'VarInfo' of @x@ the results of querying
  253 -- 'dsGetCompleteMatches' and then striking out all occurrences of @K@ for
  254 -- which we already know @x ≁ K@ from these sets.
  255 --
  256 -- For motivation, see Section 5.3 in Lower Your Guards.
  257 -- See also Note [Implementation of COMPLETE pragmas]
  258 data ResidualCompleteMatches
  259   = RCM
  260   { rcm_vanilla :: !(Maybe CompleteMatch)
  261   -- ^ The residual set for the vanilla COMPLETE set from the data defn.
  262   -- Tracked separately from 'rcm_pragmas', because it might only be
  263   -- known much later (when we have enough type information to see the 'TyCon'
  264   -- of the match), or not at all even. Until that happens, it is 'Nothing'.
  265   , rcm_pragmas :: !(Maybe [CompleteMatch])
  266   -- ^ The residual sets for /all/ COMPLETE sets from pragmas that are
  267   -- visible when compiling this module. Querying that set with
  268   -- 'dsGetCompleteMatches' requires 'DsM', so we initialise it with 'Nothing'
  269   -- until first needed in a 'DsM' context.
  270   }
  271 
  272 getRcm :: ResidualCompleteMatches -> [CompleteMatch]
  273 getRcm (RCM vanilla pragmas) = maybeToList vanilla ++ fromMaybe [] pragmas
  274 
  275 isRcmInitialised :: ResidualCompleteMatches -> Bool
  276 isRcmInitialised (RCM vanilla pragmas) = isJust vanilla && isJust pragmas
  277 
  278 instance Outputable ResidualCompleteMatches where
  279   -- formats as "[{Nothing,Just},{P,Q}]"
  280   ppr rcm = ppr (getRcm rcm)
  281 
  282 -----------------------
  283 -- * Looking up VarInfo
  284 
  285 emptyRCM :: ResidualCompleteMatches
  286 emptyRCM = RCM Nothing Nothing
  287 
  288 emptyVarInfo :: Id -> VarInfo
  289 emptyVarInfo x
  290   = VI
  291   { vi_id = x
  292   , vi_pos = []
  293   , vi_neg = emptyPmAltConSet
  294   -- Case (3) in Note [Strict fields and fields of unlifted type]
  295   -- in GHC.HsToCore.Pmc.Solver
  296   , vi_bot = if isUnliftedType (idType x) then IsNotBot else MaybeBot
  297   , vi_rcm = emptyRCM
  298   }
  299 
  300 lookupVarInfo :: TmState -> Id -> VarInfo
  301 -- (lookupVarInfo tms x) tells what we know about 'x'
  302 lookupVarInfo (TmSt env _ _) x = fromMaybe (emptyVarInfo x) (lookupUSDFM env x)
  303 
  304 -- | Like @lookupVarInfo ts x@, but @lookupVarInfo ts x = (y, vi)@ also looks
  305 -- through newtype constructors. We have @x ~ N1 (... (Nk y))@ such that the
  306 -- returned @y@ doesn't have a positive newtype constructor constraint
  307 -- associated with it (yet). The 'VarInfo' returned is that of @y@'s
  308 -- representative.
  309 --
  310 -- Careful, this means that @idType x@ might be different to @idType y@, even
  311 -- modulo type normalisation!
  312 --
  313 -- See also Note [Coverage checking Newtype matches] in GHC.HsToCore.Pmc.Solver.
  314 lookupVarInfoNT :: TmState -> Id -> (Id, VarInfo)
  315 lookupVarInfoNT ts x = case lookupVarInfo ts x of
  316   VI{ vi_pos = as_newtype -> Just y } -> lookupVarInfoNT ts y
  317   res                                 -> (x, res)
  318   where
  319     as_newtype = listToMaybe . mapMaybe go
  320     go PACA{paca_con = PmAltConLike (RealDataCon dc), paca_ids = [y]}
  321       | isNewDataCon dc = Just y
  322     go _                = Nothing
  323 
  324 trvVarInfo :: Functor f => (VarInfo -> f (a, VarInfo)) -> Nabla -> Id -> f (a, Nabla)
  325 trvVarInfo f nabla@MkNabla{ nabla_tm_st = ts@TmSt{ts_facts = env} } x
  326   = set_vi <$> f (lookupVarInfo ts x)
  327   where
  328     set_vi (a, vi') =
  329       (a, nabla{ nabla_tm_st = ts{ ts_facts = addToUSDFM env (vi_id vi') vi' } })
  330 
  331 ------------------------------------------------
  332 -- * Exported utility functions querying 'Nabla'
  333 
  334 lookupRefuts :: Nabla -> Id -> [PmAltCon]
  335 -- Unfortunately we need the extra bit of polymorphism and the unfortunate
  336 -- duplication of lookupVarInfo here.
  337 lookupRefuts MkNabla{ nabla_tm_st = ts } x =
  338   pmAltConSetElems $ vi_neg $ lookupVarInfo ts x
  339 
  340 isDataConSolution :: PmAltConApp -> Bool
  341 isDataConSolution PACA{paca_con = PmAltConLike (RealDataCon _)} = True
  342 isDataConSolution _                                             = False
  343 
  344 -- @lookupSolution nabla x@ picks a single solution ('vi_pos') of @x@ from
  345 -- possibly many, preferring 'RealDataCon' solutions whenever possible.
  346 lookupSolution :: Nabla -> Id -> Maybe PmAltConApp
  347 lookupSolution nabla x = case vi_pos (lookupVarInfo (nabla_tm_st nabla) x) of
  348   []                                         -> Nothing
  349   pos
  350     | Just sol <- find isDataConSolution pos -> Just sol
  351     | otherwise                              -> Just (head pos)
  352 
  353 --------------------------------------------------------------------------------
  354 -- The rest is just providing an IR for (overloaded!) literals and AltCons that
  355 -- sits between Hs and Core. We need a reliable way to detect and determine
  356 -- equality between them, which is impossible with Hs (too expressive) and with
  357 -- Core (no notion of overloaded literals, and even plain 'Int' literals are
  358 -- actually constructor apps). Also String literals are troublesome.
  359 
  360 -- | Literals (simple and overloaded ones) for pattern match checking.
  361 --
  362 -- See Note [Undecidable Equality for PmAltCons]
  363 data PmLit = PmLit
  364            { pm_lit_ty  :: Type
  365            , pm_lit_val :: PmLitValue }
  366 
  367 data PmLitValue
  368   = PmLitInt Integer
  369   | PmLitRat Rational
  370   | PmLitChar Char
  371   -- We won't actually see PmLitString in the oracle since we desugar strings to
  372   -- lists
  373   | PmLitString FastString
  374   | PmLitOverInt Int {- How often Negated? -} Integer
  375   | PmLitOverRat Int {- How often Negated? -} FractionalLit
  376   | PmLitOverString FastString
  377 
  378 -- | Undecidable semantic equality result.
  379 -- See Note [Undecidable Equality for PmAltCons]
  380 data PmEquality
  381   = Equal
  382   | Disjoint
  383   | PossiblyOverlap
  384   deriving (Eq, Show)
  385 
  386 -- | When 'PmEquality' can be decided. @True <=> Equal@, @False <=> Disjoint@.
  387 decEquality :: Bool -> PmEquality
  388 decEquality True  = Equal
  389 decEquality False = Disjoint
  390 
  391 -- | Undecidable equality for values represented by 'PmLit's.
  392 -- See Note [Undecidable Equality for PmAltCons]
  393 --
  394 -- * @Just True@ ==> Surely equal
  395 -- * @Just False@ ==> Surely different (non-overlapping, even!)
  396 -- * @Nothing@ ==> Equality relation undecidable
  397 eqPmLit :: PmLit -> PmLit -> PmEquality
  398 eqPmLit (PmLit t1 v1) (PmLit t2 v2)
  399   -- no haddock | pprTrace "eqPmLit" (ppr t1 <+> ppr v1 $$ ppr t2 <+> ppr v2) False = undefined
  400   | not (t1 `eqType` t2) = Disjoint
  401   | otherwise            = go v1 v2
  402   where
  403     go (PmLitInt i1)        (PmLitInt i2)        = decEquality (i1 == i2)
  404     go (PmLitRat r1)        (PmLitRat r2)        = decEquality (r1 == r2)
  405     go (PmLitChar c1)       (PmLitChar c2)       = decEquality (c1 == c2)
  406     go (PmLitString s1)     (PmLitString s2)     = decEquality (s1 == s2)
  407     go (PmLitOverInt n1 i1) (PmLitOverInt n2 i2)
  408       | n1 == n2 && i1 == i2                     = Equal
  409     go (PmLitOverRat n1 r1) (PmLitOverRat n2 r2)
  410       | n1 == n2 && r1 == r2                     = Equal
  411     go (PmLitOverString s1) (PmLitOverString s2)
  412       | s1 == s2                                 = Equal
  413     go _                    _                    = PossiblyOverlap
  414 
  415 -- | Syntactic equality.
  416 instance Eq PmLit where
  417   a == b = eqPmLit a b == Equal
  418 
  419 -- | Type of a 'PmLit'
  420 pmLitType :: PmLit -> Type
  421 pmLitType (PmLit ty _) = ty
  422 
  423 -- | Undecidable equality for values represented by 'ConLike's.
  424 -- See Note [Undecidable Equality for PmAltCons].
  425 -- 'PatSynCon's aren't enforced to be generative, so two syntactically different
  426 -- 'PatSynCon's might match the exact same values. Without looking into and
  427 -- reasoning about the pattern synonym's definition, we can't decide if their
  428 -- sets of matched values is different.
  429 --
  430 -- * @Just True@ ==> Surely equal
  431 -- * @Just False@ ==> Surely different (non-overlapping, even!)
  432 -- * @Nothing@ ==> Equality relation undecidable
  433 eqConLike :: ConLike -> ConLike -> PmEquality
  434 eqConLike (RealDataCon dc1) (RealDataCon dc2) = decEquality (dc1 == dc2)
  435 eqConLike (PatSynCon psc1)  (PatSynCon psc2)
  436   | psc1 == psc2
  437   = Equal
  438 eqConLike _                 _                 = PossiblyOverlap
  439 
  440 -- | Represents the head of a match against a 'ConLike' or literal.
  441 -- Really similar to 'GHC.Core.AltCon'.
  442 data PmAltCon = PmAltConLike ConLike
  443               | PmAltLit     PmLit
  444 
  445 data PmAltConSet = PACS !(UniqDSet ConLike) ![PmLit]
  446 
  447 emptyPmAltConSet :: PmAltConSet
  448 emptyPmAltConSet = PACS emptyUniqDSet []
  449 
  450 isEmptyPmAltConSet :: PmAltConSet -> Bool
  451 isEmptyPmAltConSet (PACS cls lits) = isEmptyUniqDSet cls && null lits
  452 
  453 -- | Whether there is a 'PmAltCon' in the 'PmAltConSet' that compares 'Equal' to
  454 -- the given 'PmAltCon' according to 'eqPmAltCon'.
  455 elemPmAltConSet :: PmAltCon -> PmAltConSet -> Bool
  456 elemPmAltConSet (PmAltConLike cl) (PACS cls _   ) = elementOfUniqDSet cl cls
  457 elemPmAltConSet (PmAltLit lit)    (PACS _   lits) = elem lit lits
  458 
  459 extendPmAltConSet :: PmAltConSet -> PmAltCon -> PmAltConSet
  460 extendPmAltConSet (PACS cls lits) (PmAltConLike cl)
  461   = PACS (addOneToUniqDSet cls cl) lits
  462 extendPmAltConSet (PACS cls lits) (PmAltLit lit)
  463   = PACS cls (unionLists lits [lit])
  464 
  465 pmAltConSetElems :: PmAltConSet -> [PmAltCon]
  466 pmAltConSetElems (PACS cls lits)
  467   = map PmAltConLike (uniqDSetToList cls) ++ map PmAltLit lits
  468 
  469 instance Outputable PmAltConSet where
  470   ppr = ppr . pmAltConSetElems
  471 
  472 -- | We can't in general decide whether two 'PmAltCon's match the same set of
  473 -- values. In addition to the reasons in 'eqPmLit' and 'eqConLike', a
  474 -- 'PmAltConLike' might or might not represent the same value as a 'PmAltLit'.
  475 -- See Note [Undecidable Equality for PmAltCons].
  476 --
  477 -- * @Just True@ ==> Surely equal
  478 -- * @Just False@ ==> Surely different (non-overlapping, even!)
  479 -- * @Nothing@ ==> Equality relation undecidable
  480 --
  481 -- Examples (omitting some constructor wrapping):
  482 --
  483 -- * @eqPmAltCon (LitInt 42) (LitInt 1) == Just False@: Lit equality is
  484 --   decidable
  485 -- * @eqPmAltCon (DataCon A) (DataCon B) == Just False@: DataCon equality is
  486 --   decidable
  487 -- * @eqPmAltCon (LitOverInt 42) (LitOverInt 1) == Nothing@: OverLit equality
  488 --   is undecidable
  489 -- * @eqPmAltCon (PatSyn PA) (PatSyn PB) == Nothing@: PatSyn equality is
  490 --   undecidable
  491 -- * @eqPmAltCon (DataCon I#) (LitInt 1) == Nothing@: DataCon to Lit
  492 --   comparisons are undecidable without reasoning about the wrapped @Int#@
  493 -- * @eqPmAltCon (LitOverInt 1) (LitOverInt 1) == Just True@: We assume
  494 --   reflexivity for overloaded literals
  495 -- * @eqPmAltCon (PatSyn PA) (PatSyn PA) == Just True@: We assume reflexivity
  496 --   for Pattern Synonyms
  497 eqPmAltCon :: PmAltCon -> PmAltCon -> PmEquality
  498 eqPmAltCon (PmAltConLike cl1) (PmAltConLike cl2) = eqConLike cl1 cl2
  499 eqPmAltCon (PmAltLit     l1)  (PmAltLit     l2)  = eqPmLit l1 l2
  500 eqPmAltCon _                  _                  = PossiblyOverlap
  501 
  502 -- | Syntactic equality.
  503 instance Eq PmAltCon where
  504   a == b = eqPmAltCon a b == Equal
  505 
  506 -- | Type of a 'PmAltCon'
  507 pmAltConType :: PmAltCon -> [Type] -> Type
  508 pmAltConType (PmAltLit lit)     _arg_tys = assert (null _arg_tys ) $ pmLitType lit
  509 pmAltConType (PmAltConLike con) arg_tys  = conLikeResTy con arg_tys
  510 
  511 -- | Is a match on this constructor forcing the match variable?
  512 -- True of data constructors, literals and pattern synonyms (#17357), but not of
  513 -- newtypes.
  514 -- See Note [Coverage checking Newtype matches] in GHC.HsToCore.Pmc.Solver.
  515 isPmAltConMatchStrict :: PmAltCon -> Bool
  516 isPmAltConMatchStrict PmAltLit{}                      = True
  517 isPmAltConMatchStrict (PmAltConLike PatSynCon{})      = True -- #17357
  518 isPmAltConMatchStrict (PmAltConLike (RealDataCon dc)) = not (isNewDataCon dc)
  519 
  520 pmAltConImplBangs :: PmAltCon -> [HsImplBang]
  521 pmAltConImplBangs PmAltLit{}         = []
  522 pmAltConImplBangs (PmAltConLike con) = conLikeImplBangs con
  523 
  524 {- Note [Undecidable Equality for PmAltCons]
  525 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  526 Equality on overloaded literals is undecidable in the general case. Consider
  527 the following example:
  528 
  529   instance Num Bool where
  530     ...
  531     fromInteger 0 = False -- C-like representation of booleans
  532     fromInteger _ = True
  533 
  534     f :: Bool -> ()
  535     f 1 = ()        -- Clause A
  536     f 2 = ()        -- Clause B
  537 
  538 Clause B is redundant but to detect this, we must decide the constraint:
  539 @fromInteger 2 ~ fromInteger 1@ which means that we
  540 have to look through function @fromInteger@, whose implementation could
  541 be anything. This poses difficulties for:
  542 
  543 1. The expressive power of the check.
  544    We cannot expect a reasonable implementation of pattern matching to detect
  545    that @fromInteger 2 ~ fromInteger 1@ is True, unless we unfold function
  546    fromInteger. This puts termination at risk and is undecidable in the
  547    general case.
  548 
  549 2. Error messages/Warnings.
  550    What should our message for @f@ above be? A reasonable approach would be
  551    to issue:
  552 
  553      Pattern matches are (potentially) redundant:
  554        f 2 = ...    under the assumption that 1 == 2
  555 
  556    but seems to complex and confusing for the user.
  557 
  558 We choose to equate only obviously equal overloaded literals, in all other cases
  559 we signal undecidability by returning Nothing from 'eqPmAltCons'. We do
  560 better for non-overloaded literals, because we know their fromInteger/fromString
  561 implementation is actually injective, allowing us to simplify the constraint
  562 @fromInteger 1 ~ fromInteger 2@ to @1 ~ 2@, which is trivially unsatisfiable.
  563 
  564 The impact of this treatment of overloaded literals is the following:
  565 
  566   * Redundancy checking is rather conservative, since it cannot see that clause
  567     B above is redundant.
  568 
  569   * We have instant equality check for overloaded literals (we do not rely on
  570     the term oracle which is rather expensive, both in terms of performance and
  571     memory). This significantly improves the performance of functions `covered`
  572     `uncovered` and `divergent` in "GHC.HsToCore.Pmc" and effectively addresses
  573     #11161.
  574 
  575   * The warnings issued are simpler.
  576 
  577 Similar reasoning applies to pattern synonyms: In contrast to data constructors,
  578 which are generative, constraints like F a ~ G b for two different pattern
  579 synonyms F and G aren't immediately unsatisfiable. We assume F a ~ F a, though.
  580 -}
  581 
  582 literalToPmLit :: Type -> Literal -> Maybe PmLit
  583 literalToPmLit ty l = PmLit ty <$> go l
  584   where
  585     go (LitChar c)       = Just (PmLitChar c)
  586     go (LitFloat r)      = Just (PmLitRat r)
  587     go (LitDouble r)     = Just (PmLitRat r)
  588     go (LitString s)     = Just (PmLitString (mkFastStringByteString s))
  589     go (LitNumber _ i)   = Just (PmLitInt i)
  590     go _                 = Nothing
  591 
  592 negatePmLit :: PmLit -> Maybe PmLit
  593 negatePmLit (PmLit ty v) = PmLit ty <$> go v
  594   where
  595     go (PmLitInt i)       = Just (PmLitInt (-i))
  596     go (PmLitRat r)       = Just (PmLitRat (-r))
  597     go (PmLitOverInt n i) = Just (PmLitOverInt (n+1) i)
  598     go (PmLitOverRat n r) = Just (PmLitOverRat (n+1) r)
  599     go _                  = Nothing
  600 
  601 overloadPmLit :: Type -> PmLit -> Maybe PmLit
  602 overloadPmLit ty (PmLit _ v) = PmLit ty <$> go v
  603   where
  604     go (PmLitInt i)          = Just (PmLitOverInt 0 i)
  605     go (PmLitRat r)          = Just $! PmLitOverRat 0 $! fractionalLitFromRational r
  606     go (PmLitString s)
  607       | ty `eqType` stringTy = Just v
  608       | otherwise            = Just (PmLitOverString s)
  609     go ovRat@PmLitOverRat{}  = Just ovRat
  610     go _               = Nothing
  611 
  612 pmLitAsStringLit :: PmLit -> Maybe FastString
  613 pmLitAsStringLit (PmLit _ (PmLitString s)) = Just s
  614 pmLitAsStringLit _                         = Nothing
  615 
  616 coreExprAsPmLit :: CoreExpr -> Maybe PmLit
  617 -- coreExprAsPmLit e | pprTrace "coreExprAsPmLit" (ppr e) False = undefined
  618 coreExprAsPmLit (Tick _t e) = coreExprAsPmLit e
  619 coreExprAsPmLit (Lit l) = literalToPmLit (literalType l) l
  620 coreExprAsPmLit e = case collectArgs e of
  621   (Var x, [Lit l])
  622     | Just dc <- isDataConWorkId_maybe x
  623     , dc `elem` [intDataCon, wordDataCon, charDataCon, floatDataCon, doubleDataCon]
  624     -> literalToPmLit (exprType e) l
  625   (Var x, [Lit (LitNumber _ l)])
  626     | Just (ty,l) <- bignum_lit_maybe x l
  627     -> Just (PmLit ty (PmLitInt l))
  628   (Var x, [_ty, n_arg, d_arg])
  629     | Just dc <- isDataConWorkId_maybe x
  630     , dataConName dc == ratioDataConName
  631     , Just (PmLit _ (PmLitInt n)) <- coreExprAsPmLit n_arg
  632     , Just (PmLit _ (PmLitInt d)) <- coreExprAsPmLit d_arg
  633     -- HACK: just assume we have a literal double. This case only occurs for
  634     --       overloaded lits anyway, so we immediately override type information
  635     -> literalToPmLit (exprType e) (mkLitDouble (n % d))
  636 
  637   (Var x, args)
  638     -- See Note [Detecting overloaded literals with -XRebindableSyntax]
  639     | is_rebound_name x fromIntegerName
  640     , Just arg <- lastMaybe args
  641     , Just (_ty,l) <- bignum_conapp_maybe arg
  642     -> Just (PmLit integerTy (PmLitInt l)) >>= overloadPmLit (exprType e)
  643   (Var x, args)
  644     -- See Note [Detecting overloaded literals with -XRebindableSyntax]
  645     -- fromRational <expr>
  646     | is_rebound_name x fromRationalName
  647     , [r] <- dropWhile (not . is_ratio) args
  648     -> coreExprAsPmLit r >>= overloadPmLit (exprType e)
  649 
  650   --Rationals with large exponents
  651   (Var x, args)
  652     -- See Note [Detecting overloaded literals with -XRebindableSyntax]
  653     -- See Note [Dealing with rationals with large exponents]
  654     -- mkRationalBase* <rational> <exponent>
  655     | Just exp_base <- is_larg_exp_ratio x
  656     , [r, exp] <- dropWhile (not . is_ratio) args
  657     , (Var x, [_ty, n_arg, d_arg]) <- collectArgs r
  658     , Just dc <- isDataConWorkId_maybe x
  659     , dataConName dc == ratioDataConName
  660     , Just (PmLit _ (PmLitInt n)) <- coreExprAsPmLit n_arg
  661     , Just (PmLit _ (PmLitInt d)) <- coreExprAsPmLit d_arg
  662     , Just (_exp_ty,exp') <- bignum_conapp_maybe exp
  663     -> do
  664       let rational = (abs n) :% d
  665       let neg = if n < 0 then 1 else 0
  666       let frac = mkFractionalLit NoSourceText False rational exp' exp_base
  667       Just $ PmLit (exprType e) (PmLitOverRat neg frac)
  668 
  669   (Var x, args)
  670     | is_rebound_name x fromStringName
  671     -- See Note [Detecting overloaded literals with -XRebindableSyntax]
  672     , s:_ <- filter (isStringTy . exprType) $ filter isValArg args
  673     -- NB: Calls coreExprAsPmLit and then overloadPmLit, so that we return PmLitOverStrings
  674     -> coreExprAsPmLit s >>= overloadPmLit (exprType e)
  675   -- These last two cases handle proper String literals
  676   (Var x, [Type ty])
  677     | Just dc <- isDataConWorkId_maybe x
  678     , dc == nilDataCon
  679     , ty `eqType` charTy
  680     -> literalToPmLit stringTy (mkLitString "")
  681   (Var x, [Lit l])
  682     | idName x `elem` [unpackCStringName, unpackCStringUtf8Name]
  683     -> literalToPmLit stringTy l
  684 
  685   _ -> Nothing
  686   where
  687     bignum_conapp_maybe (App (Var x) (Lit (LitNumber _ l)))
  688       = bignum_lit_maybe x l
  689     bignum_conapp_maybe _ = Nothing
  690 
  691     bignum_lit_maybe x l
  692       | Just dc <- isDataConWorkId_maybe x
  693       = if | dc == integerISDataCon -> Just (integerTy,l)
  694            | dc == integerIPDataCon -> Just (integerTy,l)
  695            | dc == integerINDataCon -> Just (integerTy,negate l)
  696            | dc == naturalNSDataCon -> Just (naturalTy,l)
  697            | dc == naturalNBDataCon -> Just (naturalTy,l)
  698            | otherwise              -> Nothing
  699     bignum_lit_maybe _ _ = Nothing
  700 
  701     is_ratio (Type _) = False
  702     is_ratio r
  703       | Just (tc, _) <- splitTyConApp_maybe (exprType r)
  704       = tyConName tc == ratioTyConName
  705       | otherwise
  706       = False
  707     is_larg_exp_ratio x
  708       | is_rebound_name x mkRationalBase10Name
  709       = Just Base10
  710       | is_rebound_name x mkRationalBase2Name
  711       = Just Base2
  712       | otherwise
  713       = Nothing
  714 
  715 
  716     -- See Note [Detecting overloaded literals with -XRebindableSyntax]
  717     is_rebound_name :: Id -> Name -> Bool
  718     is_rebound_name x n = getOccFS (idName x) == getOccFS n
  719 
  720 {- Note [Detecting overloaded literals with -XRebindableSyntax]
  721 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  722 Normally, we'd find e.g. overloaded string literals by comparing the
  723 application head of an expression to `fromStringName`. But that doesn't work
  724 with -XRebindableSyntax: The `Name` of a user-provided `fromString` function is
  725 different to `fromStringName`, which lives in a certain module, etc.
  726 
  727 There really is no other way than to compare `OccName`s and guess which
  728 argument is the actual literal string (we assume it's the first argument of
  729 type `String`).
  730 
  731 The same applies to other overloaded literals, such as overloaded rationals
  732 (`fromRational`)and overloaded integer literals (`fromInteger`).
  733 
  734 Note [Dealing with rationals with large exponents]
  735 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  736 Rationals with large exponents are *not* desugared to
  737 a simple rational. As that would require us to compute
  738 their value which can be expensive. Rather they desugar
  739 to an expression. For example 1e1000 will desugar to an
  740 expression of the form: `mkRationalWithExponentBase10 (1 :% 1) 1000`
  741 
  742 Only overloaded literals desugar to this form however, so we
  743 we can just return a overloaded rational literal.
  744 
  745 The most complex case is if we have RebindableSyntax enabled.
  746 By example if we have a pattern like this: `f 3.3 = True`
  747 
  748 It will desugar to:
  749   fromRational
  750     [TYPE: Rational, mkRationalBase10 (:% @Integer 10 1) (-1)]
  751 
  752 The fromRational is properly detected as an overloaded Rational by
  753 coreExprAsPmLit and it's general code for detecting overloaded rationals.
  754 See Note [Detecting overloaded literals with -XRebindableSyntax].
  755 
  756 This case then recurses into coreExprAsPmLit passing only the expression
  757 `mkRationalBase10 (:% @Integer 10 1) (-1)`. Which is caught by rationals
  758 with large exponents case. This will return a `PmLitOverRat` literal.
  759 
  760 Which is then passed to overloadPmLit which simply returns it as-is since
  761 it's already overloaded.
  762 
  763 -}
  764 
  765 instance Outputable PmLitValue where
  766   ppr (PmLitInt i)        = ppr i
  767   ppr (PmLitRat r)        = ppr (double (fromRat r)) -- good enough
  768   ppr (PmLitChar c)       = pprHsChar c
  769   ppr (PmLitString s)     = pprHsString s
  770   ppr (PmLitOverInt n i)  = minuses n (ppr i)
  771   ppr (PmLitOverRat n r)  = minuses n (ppr r)
  772   ppr (PmLitOverString s) = pprHsString s
  773 
  774 -- Take care of negated literals
  775 minuses :: Int -> SDoc -> SDoc
  776 minuses n sdoc = iterate (\sdoc -> parens (char '-' <> sdoc)) sdoc !! n
  777 
  778 instance Outputable PmLit where
  779   ppr (PmLit ty v) = ppr v <> suffix
  780     where
  781       -- Some ad-hoc hackery for displaying proper lit suffixes based on type
  782       tbl = [ (intPrimTy, primIntSuffix)
  783             , (int64PrimTy, primInt64Suffix)
  784             , (wordPrimTy, primWordSuffix)
  785             , (word64PrimTy, primWord64Suffix)
  786             , (charPrimTy, primCharSuffix)
  787             , (floatPrimTy, primFloatSuffix)
  788             , (doublePrimTy, primDoubleSuffix) ]
  789       suffix = fromMaybe empty (snd <$> find (eqType ty . fst) tbl)
  790 
  791 instance Outputable PmAltCon where
  792   ppr (PmAltConLike cl) = ppr cl
  793   ppr (PmAltLit l)      = ppr l
  794 
  795 instance Outputable PmEquality where
  796   ppr = text . show