[Git][ghc/ghc][master] 2 commits: PmCheck: Big refactor of module structure
Marge Bot
gitlab at gitlab.haskell.org
Sat Sep 26 09:37:01 UTC 2020
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
af1e84e7 by Sebastian Graf at 2020-09-26T05:36:46-04:00
PmCheck: Big refactor of module structure
* Move everything from `GHC.HsToCore.PmCheck.*` to
`GHC.HsToCore.Pmc.*` in analogy to `GHC.Tc`, rename exported
`covCheck*` functions to `pmc*`
* Rename `Pmc.Oracle` to `Pmc.Solver`
* Split off the LYG desugaring and checking steps into their own
modules (`Pmc.Desugar` and `Pmc.Check` respectively)
* Split off a `Pmc.Utils` module with stuff shared by
`Pmc.{,Desugar,Check,Solver}`
* Move `Pmc.Types` to `Pmc.Solver.Types`, add a new `Pmc.Types` module
with all the LYG types, which form the interfaces between
`Pmc.{Desugar,Check,Solver,}`.
- - - - -
f08f98e8 by Sebastian Graf at 2020-09-26T05:36:46-04:00
Extract SharedIdEnv into its own module
It's now named `GHC.Types.Unique.SDFM.UniqSDFM`.
The implementation is more clear about its stated goals and supported
operations.
- - - - -
18 changed files:
- compiler/GHC/Hs/Extension.hs
- compiler/GHC/HsToCore/Binds.hs
- compiler/GHC/HsToCore/Expr.hs
- compiler/GHC/HsToCore/GuardedRHSs.hs
- compiler/GHC/HsToCore/Match.hs
- compiler/GHC/HsToCore/Monad.hs
- compiler/GHC/HsToCore/PmCheck.hs → compiler/GHC/HsToCore/Pmc.hs
- + compiler/GHC/HsToCore/Pmc/Check.hs
- + compiler/GHC/HsToCore/Pmc/Desugar.hs
- compiler/GHC/HsToCore/PmCheck/Ppr.hs → compiler/GHC/HsToCore/Pmc/Ppr.hs
- compiler/GHC/HsToCore/PmCheck/Oracle.hs → compiler/GHC/HsToCore/Pmc/Solver.hs
- compiler/GHC/HsToCore/PmCheck/Types.hs → compiler/GHC/HsToCore/Pmc/Solver/Types.hs
- + compiler/GHC/HsToCore/Pmc/Types.hs
- + compiler/GHC/HsToCore/Pmc/Utils.hs
- compiler/GHC/HsToCore/Types.hs
- compiler/GHC/Tc/Solver.hs
- + compiler/GHC/Types/Unique/SDFM.hs
- compiler/ghc.cabal.in
Changes:
=====================================
compiler/GHC/Hs/Extension.hs
=====================================
@@ -247,7 +247,7 @@ NoExtCon. But since (1) the field is strict and (2) NoExtCon is an empty data
type, there is no possible way to reach the right-hand side of the XHsDecl
case. As a result, the coverage checker concludes that the XHsDecl case is
inaccessible, so it can be removed.
-(See Note [Strict argument type constraints] in GHC.HsToCore.PmCheck.Oracle for
+(See Note [Strict argument type constraints] in GHC.HsToCore.Pmc.Solver for
more on how this works.)
Bottom line: if you add a TTG extension constructor that uses NoExtCon, make
=====================================
compiler/GHC/HsToCore/Binds.hs
=====================================
@@ -33,7 +33,7 @@ import {-# SOURCE #-} GHC.HsToCore.Match ( matchWrapper )
import GHC.HsToCore.Monad
import GHC.HsToCore.GuardedRHSs
import GHC.HsToCore.Utils
-import GHC.HsToCore.PmCheck ( addTyCs, covCheckGRHSs )
+import GHC.HsToCore.Pmc ( addTyCs, pmcGRHSs )
import GHC.Hs -- lots of things
import GHC.Core -- lots of things
@@ -159,7 +159,7 @@ dsHsBind dflags b@(FunBind { fun_id = L loc fun
-- oracle.
-- addTyCs: Add type evidence to the refinement type
-- predicate of the coverage checker
- -- See Note [Long-distance information] in "GHC.HsToCore.PmCheck"
+ -- See Note [Long-distance information] in "GHC.HsToCore.Pmc"
matchWrapper
(mkPrefixFunRhs (L loc (idName fun)))
Nothing matches
@@ -185,7 +185,7 @@ dsHsBind dflags b@(FunBind { fun_id = L loc fun
dsHsBind dflags (PatBind { pat_lhs = pat, pat_rhs = grhss
, pat_ext = ty
, pat_ticks = (rhs_tick, var_ticks) })
- = do { rhss_nablas <- covCheckGRHSs PatBindGuards grhss
+ = do { rhss_nablas <- pmcGRHSs PatBindGuards grhss
; body_expr <- dsGuarded grhss ty rhss_nablas
; let body' = mkOptTickBox rhs_tick body_expr
pat' = decideBangHood dflags pat
=====================================
compiler/GHC/HsToCore/Expr.hs
=====================================
@@ -31,7 +31,7 @@ import GHC.HsToCore.ListComp
import GHC.HsToCore.Utils
import GHC.HsToCore.Arrows
import GHC.HsToCore.Monad
-import GHC.HsToCore.PmCheck ( addTyCs, covCheckGRHSs )
+import GHC.HsToCore.Pmc ( addTyCs, pmcGRHSs )
import GHC.Types.Name
import GHC.Types.Name.Env
import GHC.Core.FamInstEnv( topNormaliseType )
@@ -215,7 +215,7 @@ dsUnliftedBind (PatBind {pat_lhs = pat, pat_rhs = grhss
, pat_ext = ty }) body
= -- let C x# y# = rhs in body
-- ==> case rhs of C x# y# -> body
- do { match_nablas <- covCheckGRHSs PatBindGuards grhss
+ do { match_nablas <- pmcGRHSs PatBindGuards grhss
; rhs <- dsGuarded grhss ty match_nablas
; let upat = unLoc pat
eqn = EqnInfo { eqn_pats = [upat],
@@ -490,7 +490,7 @@ dsExpr (HsMultiIf res_ty alts)
| otherwise
= do { let grhss = GRHSs noExtField alts (noLoc emptyLocalBinds)
- ; rhss_nablas <- covCheckGRHSs IfAlt grhss
+ ; rhss_nablas <- pmcGRHSs IfAlt grhss
; match_result <- dsGRHSs IfAlt grhss res_ty rhss_nablas
; error_expr <- mkErrorExpr
; extractMatchResult match_result error_expr }
=====================================
compiler/GHC/HsToCore/GuardedRHSs.hs
=====================================
@@ -25,7 +25,7 @@ import GHC.Core.Utils (bindNonRec)
import GHC.HsToCore.Monad
import GHC.HsToCore.Utils
-import GHC.HsToCore.PmCheck.Types ( Nablas )
+import GHC.HsToCore.Pmc.Types ( Nablas )
import GHC.Core.Type ( Type )
import GHC.Utils.Misc
import GHC.Types.SrcLoc
=====================================
compiler/GHC/HsToCore/Match.hs
=====================================
@@ -34,8 +34,8 @@ import GHC.Hs
import GHC.Tc.Utils.Zonk
import GHC.Tc.Types.Evidence
import GHC.Tc.Utils.Monad
-import GHC.HsToCore.PmCheck
-import GHC.HsToCore.PmCheck.Types ( Nablas, initNablas )
+import GHC.HsToCore.Pmc
+import GHC.HsToCore.Pmc.Types ( Nablas, initNablas )
import GHC.Core
import GHC.Types.Literal
import GHC.Core.Utils
@@ -771,7 +771,7 @@ matchWrapper ctxt mb_scr (MG { mg_alts = L _ matches
; matches_nablas <- if isMatchContextPmChecked dflags origin ctxt
then addHsScrutTmCs mb_scr new_vars $
-- See Note [Long-distance information]
- covCheckMatches (DsMatchContext ctxt locn) new_vars matches
+ pmcMatches (DsMatchContext ctxt locn) new_vars matches
else pure (initNablasMatches matches)
; eqns_info <- zipWithM mk_eqn_info matches matches_nablas
@@ -881,7 +881,7 @@ matchSinglePatVar var mb_scrut ctx pat ty match_result
-- Pattern match check warnings
; when (isMatchContextPmChecked dflags FromSource ctx) $
addCoreScrutTmCs mb_scrut [var] $
- covCheckPatBind (DsMatchContext ctx locn) var (unLoc pat)
+ pmcPatBind (DsMatchContext ctx locn) var (unLoc pat)
; let eqn_info = EqnInfo { eqn_pats = [unLoc (decideBangHood dflags pat)]
, eqn_orig = FromSource
=====================================
compiler/GHC/HsToCore/Monad.hs
=====================================
@@ -75,7 +75,7 @@ import GHC.Core.DataCon
import GHC.Core.ConLike
import GHC.Core.TyCon
import GHC.HsToCore.Types
-import GHC.HsToCore.PmCheck.Types
+import GHC.HsToCore.Pmc.Solver.Types (Nablas, initNablas)
import GHC.Types.Id
import GHC.Unit.Module
import GHC.Utils.Outputable
=====================================
compiler/GHC/HsToCore/PmCheck.hs → compiler/GHC/HsToCore/Pmc.hs
=====================================
@@ -19,18 +19,16 @@
--
-- There is an overview Figure 2 in there that's probably helpful.
-- Here is an overview of how it's implemented, which follows the structure of
--- the entry points such as 'covCheckMatches':
+-- the entry points such as 'pmcMatches':
--
-- 1. Desugar source syntax (like 'LMatch') to guard tree variants (like
-- 'GrdMatch'), with one of the desugaring functions (like 'desugarMatch').
+-- See "GHC.HsToCore.Pmc.Desugar".
-- Follows Section 3.1 in the paper.
-- 2. Coverage check guard trees (with a function like 'checkMatch') to get a
--- 'CheckResult', containing
--- a. The set of uncovered values, 'cr_uncov'
--- b. And an annotated tree variant (like 'AnnMatch') that captures
--- redundancy and inaccessibility information as 'RedSets' annotations
--- Basically the UA function from Section 5.1. The Normalised Refinement
--- Types 'Nablas' are maintained in "GHC.HsToCore.PmCheck.Oracle".
+-- 'CheckResult'. See "GHC.HsToCore.Pmc.Check".
+-- The normalised refinement types 'Nabla' are tested for inhabitants by
+-- "GHC.HsToCore.Pmc.Solver".
-- 3. Collect redundancy information into a 'CIRB' with a function such
-- as 'cirbsMatch'. Follows the R function from Figure 6 of the paper.
-- 4. Format and report uncovered patterns and redundant equations ('CIRB')
@@ -39,9 +37,9 @@
-- 5. Return 'Nablas' reaching syntactic sub-components for
-- Note [Long-distance information]. Collected by functions such as
-- 'ldiMatch'. See Section 4.1 of the paper.
-module GHC.HsToCore.PmCheck (
+module GHC.HsToCore.Pmc (
-- Checking and printing
- covCheckPatBind, covCheckMatches, covCheckGRHSs,
+ pmcPatBind, pmcMatches, pmcGRHSs,
isMatchContextPmChecked,
-- See Note [Long-distance information]
@@ -52,45 +50,31 @@ module GHC.HsToCore.PmCheck (
import GHC.Prelude
-import GHC.HsToCore.PmCheck.Types
-import GHC.HsToCore.PmCheck.Oracle
-import GHC.HsToCore.PmCheck.Ppr
-import GHC.Types.Basic (Origin(..), isGenerated)
-import GHC.Core (CoreExpr, Expr(Var,App))
-import GHC.Data.FastString (unpackFS, lengthFS)
+import GHC.HsToCore.Pmc.Types
+import GHC.HsToCore.Pmc.Utils
+import GHC.HsToCore.Pmc.Desugar
+import GHC.HsToCore.Pmc.Check
+import GHC.HsToCore.Pmc.Solver
+import GHC.HsToCore.Pmc.Ppr
+import GHC.Types.Basic (Origin(..))
+import GHC.Core (CoreExpr)
import GHC.Driver.Session
import GHC.Hs
-import GHC.Tc.Utils.Zonk (shortCutLit)
import GHC.Types.Id
-import GHC.Core.ConLike
-import GHC.Types.Name
-import GHC.Builtin.Types
import GHC.Types.SrcLoc
import GHC.Utils.Misc
import GHC.Utils.Outputable
import GHC.Utils.Panic
-import GHC.Core.DataCon
import GHC.Types.Var (EvVar)
-import GHC.Core.Coercion
-import GHC.Tc.Types.Evidence (HsWrapper(..), isIdHsWrapper)
import GHC.Tc.Utils.TcType (evVarPred)
-import {-# SOURCE #-} GHC.HsToCore.Expr (dsExpr, dsLExpr, dsSyntaxExpr)
-import {-# SOURCE #-} GHC.HsToCore.Binds (dsHsWrapper)
-import GHC.HsToCore.Utils (selectMatchVar)
-import GHC.HsToCore.Match.Literal (dsLit, dsOverLit)
+import {-# SOURCE #-} GHC.HsToCore.Expr (dsLExpr)
import GHC.HsToCore.Monad
import GHC.Data.Bag
import GHC.Data.IOEnv (unsafeInterleaveM)
import GHC.Data.OrdList
-import GHC.Core.TyCo.Rep
-import GHC.Core.Type
-import GHC.HsToCore.Utils (isTrueLHsExpr)
-import GHC.Data.Maybe
-import qualified GHC.LanguageExtensions as LangExt
-import GHC.Utils.Monad (concatMapM, mapMaybeM)
+import GHC.Utils.Monad (mapMaybeM)
-import Control.Monad (when, forM_, zipWithM)
-import Data.List (elemIndex)
+import Control.Monad (when, forM_)
import qualified Data.Semigroup as Semi
import Data.List.NonEmpty ( NonEmpty(..) )
import qualified Data.List.NonEmpty as NE
@@ -112,30 +96,30 @@ getLdiNablas = do
False -> pure initNablas
-- | Check a pattern binding (let, where) for exhaustiveness.
-covCheckPatBind :: DsMatchContext -> Id -> Pat GhcTc -> DsM ()
--- See Note [covCheckPatBind only checks PatBindRhs]
-covCheckPatBind ctxt@(DsMatchContext PatBindRhs loc) var p = do
+pmcPatBind :: DsMatchContext -> Id -> Pat GhcTc -> DsM ()
+-- See Note [pmcPatBind only checks PatBindRhs]
+pmcPatBind ctxt@(DsMatchContext PatBindRhs loc) var p = do
missing <- getLdiNablas
pat_bind <- desugarPatBind loc var p
- tracePm "covCheckPatBind {" (vcat [ppr ctxt, ppr var, ppr p, ppr pat_bind, ppr missing])
+ tracePm "pmcPatBind {" (vcat [ppr ctxt, ppr var, ppr p, ppr pat_bind, ppr missing])
result <- unCA (checkPatBind pat_bind) missing
tracePm "}: " (ppr (cr_uncov result))
formatReportWarnings cirbsPatBind ctxt [var] result
-covCheckPatBind _ _ _ = pure ()
+pmcPatBind _ _ _ = pure ()
-- | Exhaustive for guard matches, is used for guards in pattern bindings and
-- in @MultiIf@ expressions. Returns the 'Nablas' covered by the RHSs.
-covCheckGRHSs
+pmcGRHSs
:: HsMatchContext GhcRn -- ^ Match context, for warning messages
-> GRHSs GhcTc (LHsExpr GhcTc) -- ^ The GRHSs to check
-> DsM (NonEmpty Nablas) -- ^ Covered 'Nablas' for each RHS, for long
-- distance info
-covCheckGRHSs hs_ctxt guards@(GRHSs _ grhss _) = do
+pmcGRHSs hs_ctxt guards@(GRHSs _ grhss _) = do
let combined_loc = foldl1 combineSrcSpans (map getLoc grhss)
ctxt = DsMatchContext hs_ctxt combined_loc
matches <- desugarGRHSs combined_loc empty guards
missing <- getLdiNablas
- tracePm "covCheckGRHSs" (hang (vcat [ppr ctxt
+ tracePm "pmcGRHSs" (hang (vcat [ppr ctxt
, text "Guards:"])
2
(pprGRHSs hs_ctxt guards $$ ppr missing))
@@ -159,18 +143,18 @@ covCheckGRHSs hs_ctxt guards@(GRHSs _ grhss _) = do
-- Special case: When there are /no matches/, then the functionassumes it
-- checks and @-XEmptyCase@ with only a single match variable.
-- See Note [Checking EmptyCase].
-covCheckMatches
+pmcMatches
:: DsMatchContext -- ^ Match context, for warnings messages
-> [Id] -- ^ Match variables, i.e. x and y above
-> [LMatch GhcTc (LHsExpr GhcTc)] -- ^ List of matches
-> DsM [(Nablas, NonEmpty Nablas)] -- ^ One covered 'Nablas' per Match and
-- GRHS, for long distance info.
-covCheckMatches ctxt vars matches = do
+pmcMatches ctxt vars matches = do
-- We have to force @missing@ before printing out the trace message,
-- otherwise we get interleaved output from the solver. This function
-- should be strict in @missing@ anyway!
!missing <- getLdiNablas
- tracePm "covCheckMatches {" $
+ tracePm "pmcMatches {" $
hang (vcat [ppr ctxt, ppr vars, text "Matches:"])
2
(vcat (map ppr matches) $$ ppr missing)
@@ -190,9 +174,9 @@ covCheckMatches ctxt vars matches = do
formatReportWarnings cirbsMatchGroup ctxt vars result
return (NE.toList (ldiMatchGroup (cr_ret result)))
-{- Note [covCheckPatBind only checks PatBindRhs]
+{- Note [pmcPatBind only checks PatBindRhs]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
- at covCheckPatBind@'s sole purpose is to check vanilla pattern bindings, like
+ at pmcPatBind@'s sole purpose is to check vanilla pattern bindings, like
@x :: Int; Just x = e@, which is in a @PatBindRhs@ context.
But its caller is also called for individual pattern guards in a @StmtCtxt at .
For example, both pattern guards in @f x y | True <- x, False <- y = ...@ will
@@ -206,837 +190,6 @@ go through this function. It makes no sense to do coverage checking there:
Note that we can't just omit checking of @StmtCtxt@ altogether (by adjusting
'isMatchContextPmChecked'), because that affects the other checking functions,
too.
-
-Note [Checking EmptyCase]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--XEmptyCase is useful for matching on empty data types like 'Void'. For example,
-the following is a complete match:
-
- f :: Void -> ()
- f x = case x of {}
-
-Really, -XEmptyCase is the only way to write a program that at the same time is
-safe (@f _ = error "boom"@ is not because of ⊥), doesn't trigger a warning
-(@f !_ = error "inaccessible" has inaccessible RHS) and doesn't turn an
-exception into divergence (@f x = f x@).
-
-Semantically, unlike every other case expression, -XEmptyCase is strict in its
-match var x, which rules out ⊥ as an inhabitant. So we add x ≁ ⊥ to the
-initial Nabla and check if there are any values left to match on.
--}
-
---
--- * Guard language
---
-
--- | A very simple language for pattern guards. Let bindings, bang patterns,
--- and matching variables against flat constructor patterns.
-data PmGrd
- = -- | @PmCon x K dicts args@ corresponds to a @K dicts args <- x@ guard.
- -- The @args@ are bound in this construct, the @x@ is just a use.
- -- For the arguments' meaning see 'GHC.Hs.Pat.ConPatOut'.
- PmCon {
- pm_id :: !Id,
- pm_con_con :: !PmAltCon,
- pm_con_tvs :: ![TyVar],
- pm_con_dicts :: ![EvVar],
- pm_con_args :: ![Id]
- }
-
- -- | @PmBang x@ corresponds to a @seq x True@ guard.
- -- If the extra 'SrcInfo' is present, the bang guard came from a source
- -- bang pattern, in which case we might want to report it as redundant.
- -- See Note [Dead bang patterns].
- | PmBang {
- pm_id :: !Id,
- _pm_loc :: !(Maybe SrcInfo)
- }
-
- -- | @PmLet x expr@ corresponds to a @let x = expr@ guard. This actually
- -- /binds/ @x at .
- | PmLet {
- pm_id :: !Id,
- _pm_let_expr :: !CoreExpr
- }
-
--- | Should not be user-facing.
-instance Outputable PmGrd where
- ppr (PmCon x alt _tvs _con_dicts con_args)
- = hsep [ppr alt, hsep (map ppr con_args), text "<-", ppr x]
- ppr (PmBang x _loc) = char '!' <> ppr x
- ppr (PmLet x expr) = hsep [text "let", ppr x, text "=", ppr expr]
-
-type GrdVec = [PmGrd]
-
-data Precision = Approximate | Precise
- deriving (Eq, Show)
-
-instance Outputable Precision where
- ppr = text . show
-
-instance Semi.Semigroup Precision where
- Precise <> Precise = Precise
- _ <> _ = Approximate
-
-instance Monoid Precision where
- mempty = Precise
- mappend = (Semi.<>)
-
---
--- * Guard tree language
---
-
--- | Means by which we identify a source construct for later pretty-printing in
--- a warning message. 'SDoc' for the equation to show, 'Located' for the
--- location.
-type SrcInfo = Located SDoc
-
--- | Redundancy sets, used to determine redundancy of RHSs and bang patterns
--- (later digested into a 'CIRB').
-data RedSets
- = RedSets
- { rs_cov :: !Nablas
- -- ^ The /Covered/ set; the set of values reaching a particular program
- -- point.
- , rs_div :: !Nablas
- -- ^ The /Diverging/ set; empty if no match can lead to divergence.
- -- If it wasn't empty, we have to turn redundancy warnings into
- -- inaccessibility warnings for any subclauses.
- , rs_bangs :: !(OrdList (Nablas, SrcInfo))
- -- ^ If any of the 'Nablas' is empty, the corresponding 'SrcInfo' pin-points
- -- a bang pattern in source that is redundant. See Note [Dead bang patterns].
- }
-
--- The following two type synonyms instantiate our tree structures to guard
--- trees and annotated trees, respectively, by giving the types to attach as
--- payload.
-
--- | Used as tree payload pre-checking. The LYG guards to check.
-type Pre = [PmGrd]
-
--- | Used as tree payload post-checking. The redundancy info we elaborated.
-type Post = RedSets
-
--- | A guard tree denoting 'MatchGroup'.
-newtype PmMatchGroup p = PmMatchGroup (NonEmpty (PmMatch p))
-
--- | A guard tree denoting 'Match': A payload describing the pats and a bunch of
--- GRHS.
-data PmMatch p = PmMatch { pm_pats :: !p, pm_grhss :: !(NonEmpty (PmGRHS p)) }
-
--- | A guard tree denoting 'GRHS': A payload describing the grds and a 'SrcInfo'
--- useful for printing out in warnings messages.
-data PmGRHS p = PmGRHS { pg_grds :: !p, pg_rhs :: !SrcInfo }
-
--- | A guard tree denoting an -XEmptyCase.
-newtype PmEmptyCase = PmEmptyCase { pe_var :: Id }
-
--- | A guard tree denoting a pattern binding.
-newtype PmPatBind p =
- -- just reuse GrdGRHS and pretend its @SrcInfo@ is info on the /pattern/,
- -- rather than on the pattern bindings.
- PmPatBind (PmGRHS p)
-
-emptyRedSets :: RedSets
--- Semigroup instance would be misleading!
-emptyRedSets = RedSets mempty mempty mempty
-
-pprSrcInfo :: SrcInfo -> SDoc
-pprSrcInfo (L (RealSrcSpan rss _) _) = ppr (srcSpanStartLine rss)
-pprSrcInfo (L s _) = ppr s
-
--- | Format LYG guards as @| True <- x, let x = 42, !z@
-pprLygGuards :: [PmGrd] -> SDoc
-pprLygGuards [] = empty
-pprLygGuards (g:gs) = fsep (char '|' <+> ppr g : map ((comma <+>) . ppr) gs)
-
--- | Format a LYG sequence (e.g. 'Match'es of a 'MatchGroup' or 'GRHSs') as
--- @{ <first alt>; ...; <last alt> }@
-pprLygSequence :: Outputable a => NonEmpty a -> SDoc
-pprLygSequence (NE.toList -> as) =
- braces (space <> fsep (punctuate semi (map ppr as)) <> space)
-
-instance Outputable (PmMatchGroup Pre) where
- ppr (PmMatchGroup matches) = pprLygSequence matches
-
-instance Outputable (PmMatch Pre) where
- ppr (PmMatch { pm_pats = grds, pm_grhss = grhss }) =
- pprLygGuards grds <+> ppr grhss
-
-instance Outputable (PmGRHS Pre) where
- ppr (PmGRHS { pg_grds = grds, pg_rhs = rhs }) =
- pprLygGuards grds <+> text "->" <+> pprSrcInfo rhs
-
-instance Outputable (PmPatBind Pre) where
- ppr (PmPatBind PmGRHS { pg_grds = grds, pg_rhs = bind }) =
- ppr bind <+> pprLygGuards grds <+> text "=" <+> text "..."
-
-instance Outputable PmEmptyCase where
- ppr (PmEmptyCase { pe_var = var }) =
- text "<empty case on " <> ppr var <> text ">"
-
-pprRedSets :: RedSets -> SDoc
--- It's useful to change this definition for different verbosity levels in
--- printf-debugging
-pprRedSets RedSets { rs_cov = _cov, rs_div = _div, rs_bangs = _bangs }
- = empty
-
-instance Outputable (PmMatchGroup Post) where
- ppr (PmMatchGroup matches) = pprLygSequence matches
-
-instance Outputable (PmMatch Post) where
- ppr (PmMatch { pm_pats = red, pm_grhss = grhss }) =
- pprRedSets red <+> ppr grhss
-
-instance Outputable (PmGRHS Post) where
- ppr (PmGRHS { pg_grds = red, pg_rhs = rhs }) =
- pprRedSets red <+> text "->" <+> pprSrcInfo rhs
-
-{- Note [Dead bang patterns]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
-
- f :: Bool -> Int
- f True = 1
- f !x = 2
-
-Whenever we fall through to the second equation, we will already have evaluated
-the argument. Thus, the bang pattern serves no purpose and should be warned
-about. We call this kind of bang patterns "dead". Dead bangs are the ones
-that under no circumstances can force a thunk that wasn't already forced.
-Dead bangs are a form of redundant bangs; see below.
-
-We can detect dead bang patterns by checking whether @x ~ ⊥@ is satisfiable
-where the PmBang appears in 'checkGrd'. If not, then clearly the bang is
-dead. Such a dead bang is then indicated in the annotated pattern-match tree by
-a 'RedundantSrcBang' wrapping. In 'redundantAndInaccessibles', we collect
-all dead bangs to warn about.
-
-Note that we don't want to warn for a dead bang that appears on a redundant
-clause. That is because in that case, we recommend to delete the clause wholly,
-including its leading pattern match.
-
-Dead bang patterns are redundant. But there are bang patterns which are
-redundant that aren't dead, for example
-
- f !() = 0
-
-the bang still forces the match variable, before we attempt to match on (). But
-it is redundant with the forcing done by the () match. We currently don't
-detect redundant bangs that aren't dead.
--}
-
---
--- * Desugaring source syntax to guard trees
---
-
--- | Smart constructor that eliminates trivial lets
-mkPmLetVar :: Id -> Id -> GrdVec
-mkPmLetVar x y | x == y = []
-mkPmLetVar x y = [PmLet x (Var y)]
-
--- | ADT constructor pattern => no existentials, no local constraints
-vanillaConGrd :: Id -> DataCon -> [Id] -> PmGrd
-vanillaConGrd scrut con arg_ids =
- PmCon { pm_id = scrut, pm_con_con = PmAltConLike (RealDataCon con)
- , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = arg_ids }
-
--- | Creates a 'GrdVec' refining a match var of list type to a list,
--- where list fields are matched against the incoming tagged 'GrdVec's.
--- For example:
--- @mkListGrds "a" "[(x, True <- x),(y, !y)]"@
--- to
--- @"[(x:b) <- a, True <- x, (y:c) <- b, !y, [] <- c]"@
--- where @b@ and @c@ are freshly allocated in @mkListGrds@ and @a@ is the match
--- variable.
-mkListGrds :: Id -> [(Id, GrdVec)] -> DsM GrdVec
--- See Note [Order of guards matter] for why we need to intertwine guards
--- on list elements.
-mkListGrds a [] = pure [vanillaConGrd a nilDataCon []]
-mkListGrds a ((x, head_grds):xs) = do
- b <- mkPmId (idType a)
- tail_grds <- mkListGrds b xs
- pure $ vanillaConGrd a consDataCon [x, b] : head_grds ++ tail_grds
-
--- | Create a 'GrdVec' refining a match variable to a 'PmLit'.
-mkPmLitGrds :: Id -> PmLit -> DsM GrdVec
-mkPmLitGrds x (PmLit _ (PmLitString s)) = do
- -- We desugar String literals to list literals for better overlap reasoning.
- -- It's a little unfortunate we do this here rather than in
- -- 'GHC.HsToCore.PmCheck.Oracle.trySolve' and
- -- 'GHC.HsToCore.PmCheck.Oracle.addRefutableAltCon', but it's so much simpler
- -- here. See Note [Representation of Strings in TmState] in
- -- GHC.HsToCore.PmCheck.Oracle
- vars <- traverse mkPmId (take (lengthFS s) (repeat charTy))
- let mk_char_lit y c = mkPmLitGrds y (PmLit charTy (PmLitChar c))
- char_grdss <- zipWithM mk_char_lit vars (unpackFS s)
- mkListGrds x (zip vars char_grdss)
-mkPmLitGrds x lit = do
- let grd = PmCon { pm_id = x
- , pm_con_con = PmAltLit lit
- , pm_con_tvs = []
- , pm_con_dicts = []
- , pm_con_args = [] }
- pure [grd]
-
--- | @desugarPat _ x pat@ transforms @pat@ into a 'GrdVec', where
--- the variable representing the match is @x at .
-desugarPat :: Id -> Pat GhcTc -> DsM GrdVec
-desugarPat x pat = case pat of
- WildPat _ty -> pure []
- VarPat _ y -> pure (mkPmLetVar (unLoc y) x)
- ParPat _ p -> desugarLPat x p
- LazyPat _ _ -> pure [] -- like a wildcard
- BangPat _ p@(L l p') ->
- -- Add the bang in front of the list, because it will happen before any
- -- nested stuff.
- (PmBang x pm_loc :) <$> desugarLPat x p
- where pm_loc = Just (L l (ppr p'))
-
- -- (x at pat) ==> Desugar pat with x as match var and handle impedance
- -- mismatch with incoming match var
- AsPat _ (L _ y) p -> (mkPmLetVar y x ++) <$> desugarLPat y p
-
- SigPat _ p _ty -> desugarLPat x p
-
- -- See Note [Desugar CoPats]
- -- Generally the translation is
- -- pat |> co ===> let y = x |> co, pat <- y where y is a match var of pat
- XPat (CoPat wrapper p _ty)
- | isIdHsWrapper wrapper -> desugarPat x p
- | WpCast co <- wrapper, isReflexiveCo co -> desugarPat x p
- | otherwise -> do
- (y, grds) <- desugarPatV p
- wrap_rhs_y <- dsHsWrapper wrapper
- pure (PmLet y (wrap_rhs_y (Var x)) : grds)
-
- -- (n + k) ===> let b = x >= k, True <- b, let n = x-k
- NPlusKPat _pat_ty (L _ n) k1 k2 ge minus -> do
- b <- mkPmId boolTy
- let grd_b = vanillaConGrd b trueDataCon []
- [ke1, ke2] <- traverse dsOverLit [unLoc k1, k2]
- rhs_b <- dsSyntaxExpr ge [Var x, ke1]
- rhs_n <- dsSyntaxExpr minus [Var x, ke2]
- pure [PmLet b rhs_b, grd_b, PmLet n rhs_n]
-
- -- (fun -> pat) ===> let y = fun x, pat <- y where y is a match var of pat
- ViewPat _arg_ty lexpr pat -> do
- (y, grds) <- desugarLPatV pat
- fun <- dsLExpr lexpr
- pure $ PmLet y (App fun (Var x)) : grds
-
- -- list
- ListPat (ListPatTc _elem_ty Nothing) ps ->
- desugarListPat x ps
-
- -- overloaded list
- ListPat (ListPatTc elem_ty (Just (pat_ty, to_list))) pats -> do
- dflags <- getDynFlags
- case splitListTyConApp_maybe pat_ty of
- Just _e_ty
- | not (xopt LangExt.RebindableSyntax dflags)
- -- Just desugar it as a regular ListPat
- -> desugarListPat x pats
- _ -> do
- y <- mkPmId (mkListTy elem_ty)
- grds <- desugarListPat y pats
- rhs_y <- dsSyntaxExpr to_list [Var x]
- pure $ PmLet y rhs_y : grds
-
- -- (a) In the presence of RebindableSyntax, we don't know anything about
- -- `toList`, we should treat `ListPat` as any other view pattern.
- --
- -- (b) In the absence of RebindableSyntax,
- -- - If the pat_ty is `[a]`, then we treat the overloaded list pattern
- -- as ordinary list pattern. Although we can give an instance
- -- `IsList [Int]` (more specific than the default `IsList [a]`), in
- -- practice, we almost never do that. We assume the `to_list` is
- -- the `toList` from `instance IsList [a]`.
- --
- -- - Otherwise, we treat the `ListPat` as ordinary view pattern.
- --
- -- See #14547, especially comment#9 and comment#10.
-
- ConPat { pat_con = L _ con
- , pat_args = ps
- , pat_con_ext = ConPatTc
- { cpt_arg_tys = arg_tys
- , cpt_tvs = ex_tvs
- , cpt_dicts = dicts
- }
- } -> do
- desugarConPatOut x con arg_tys ex_tvs dicts ps
-
- NPat ty (L _ olit) mb_neg _ -> do
- -- See Note [Literal short cut] in "GHC.HsToCore.Match.Literal"
- -- We inline the Literal short cut for @ty@ here, because @ty@ is more
- -- precise than the field of OverLitTc, which is all that dsOverLit (which
- -- normally does the literal short cut) can look at. Also @ty@ matches the
- -- type of the scrutinee, so info on both pattern and scrutinee (for which
- -- short cutting in dsOverLit works properly) is overloaded iff either is.
- dflags <- getDynFlags
- let platform = targetPlatform dflags
- core_expr <- case olit of
- OverLit{ ol_val = val, ol_ext = OverLitTc rebindable _ }
- | not rebindable
- , Just expr <- shortCutLit platform val ty
- -> dsExpr expr
- _ -> dsOverLit olit
- let lit = expectJust "failed to detect OverLit" (coreExprAsPmLit core_expr)
- let lit' = case mb_neg of
- Just _ -> expectJust "failed to negate lit" (negatePmLit lit)
- Nothing -> lit
- mkPmLitGrds x lit'
-
- LitPat _ lit -> do
- core_expr <- dsLit (convertLit lit)
- let lit = expectJust "failed to detect Lit" (coreExprAsPmLit core_expr)
- mkPmLitGrds x lit
-
- TuplePat _tys pats boxity -> do
- (vars, grdss) <- mapAndUnzipM desugarLPatV pats
- let tuple_con = tupleDataCon boxity (length vars)
- pure $ vanillaConGrd x tuple_con vars : concat grdss
-
- SumPat _ty p alt arity -> do
- (y, grds) <- desugarLPatV p
- let sum_con = sumDataCon alt arity
- -- See Note [Unboxed tuple RuntimeRep vars] in GHC.Core.TyCon
- pure $ vanillaConGrd x sum_con [y] : grds
-
- SplicePat {} -> panic "Check.desugarPat: SplicePat"
-
--- | 'desugarPat', but also select and return a new match var.
-desugarPatV :: Pat GhcTc -> DsM (Id, GrdVec)
-desugarPatV pat = do
- x <- selectMatchVar Many pat
- grds <- desugarPat x pat
- pure (x, grds)
-
-desugarLPat :: Id -> LPat GhcTc -> DsM GrdVec
-desugarLPat x = desugarPat x . unLoc
-
--- | 'desugarLPat', but also select and return a new match var.
-desugarLPatV :: LPat GhcTc -> DsM (Id, GrdVec)
-desugarLPatV = desugarPatV . unLoc
-
--- | @desugarListPat _ x [p1, ..., pn]@ is basically
--- @desugarConPatOut _ x $(mkListConPatOuts [p1, ..., pn]>@ without ever
--- constructing the 'ConPatOut's.
-desugarListPat :: Id -> [LPat GhcTc] -> DsM GrdVec
-desugarListPat x pats = do
- vars_and_grdss <- traverse desugarLPatV pats
- mkListGrds x vars_and_grdss
-
--- | Desugar a constructor pattern
-desugarConPatOut :: Id -> ConLike -> [Type] -> [TyVar]
- -> [EvVar] -> HsConPatDetails GhcTc -> DsM GrdVec
-desugarConPatOut x con univ_tys ex_tvs dicts = \case
- PrefixCon ps -> go_field_pats (zip [0..] ps)
- InfixCon p1 p2 -> go_field_pats (zip [0..] [p1,p2])
- RecCon (HsRecFields fs _) -> go_field_pats (rec_field_ps fs)
- where
- -- The actual argument types (instantiated)
- arg_tys = map scaledThing $ conLikeInstOrigArgTys con (univ_tys ++ mkTyVarTys ex_tvs)
-
- -- Extract record field patterns tagged by field index from a list of
- -- LHsRecField
- rec_field_ps fs = map (tagged_pat . unLoc) fs
- where
- tagged_pat f = (lbl_to_index (getName (hsRecFieldId f)), hsRecFieldArg f)
- -- Unfortunately the label info is empty when the DataCon wasn't defined
- -- with record field labels, hence we desugar to field index.
- orig_lbls = map flSelector $ conLikeFieldLabels con
- lbl_to_index lbl = expectJust "lbl_to_index" $ elemIndex lbl orig_lbls
-
- go_field_pats tagged_pats = do
- -- The fields that appear might not be in the correct order. So
- -- 1. Do the PmCon match
- -- 2. Then pattern match on the fields in the order given by the first
- -- field of @tagged_pats at .
- -- See Note [Field match order for RecCon]
-
- -- Desugar the mentioned field patterns. We're doing this first to get
- -- the Ids for pm_con_args and bring them in order afterwards.
- let trans_pat (n, pat) = do
- (var, pvec) <- desugarLPatV pat
- pure ((n, var), pvec)
- (tagged_vars, arg_grdss) <- mapAndUnzipM trans_pat tagged_pats
-
- let get_pat_id n ty = case lookup n tagged_vars of
- Just var -> pure var
- Nothing -> mkPmId ty
-
- -- 1. the constructor pattern match itself
- arg_ids <- zipWithM get_pat_id [0..] arg_tys
- let con_grd = PmCon x (PmAltConLike con) ex_tvs dicts arg_ids
-
- -- 2. guards from field selector patterns
- let arg_grds = concat arg_grdss
-
- -- tracePm "ConPatOut" (ppr x $$ ppr con $$ ppr arg_ids)
- pure (con_grd : arg_grds)
-
-desugarPatBind :: SrcSpan -> Id -> Pat GhcTc -> DsM (PmPatBind Pre)
--- See 'GrdPatBind' for how this simply repurposes GrdGRHS.
-desugarPatBind loc var pat =
- PmPatBind . flip PmGRHS (L loc (ppr pat)) <$> desugarPat var pat
-
-desugarEmptyCase :: Id -> DsM PmEmptyCase
-desugarEmptyCase var = pure PmEmptyCase { pe_var = var }
-
--- | Desugar the non-empty 'Match'es of a 'MatchGroup'.
-desugarMatches :: [Id] -> NonEmpty (LMatch GhcTc (LHsExpr GhcTc))
- -> DsM (PmMatchGroup Pre)
-desugarMatches vars matches =
- PmMatchGroup <$> traverse (desugarMatch vars) matches
-
--- Desugar a single match
-desugarMatch :: [Id] -> LMatch GhcTc (LHsExpr GhcTc) -> DsM (PmMatch Pre)
-desugarMatch vars (L match_loc (Match { m_pats = pats, m_grhss = grhss })) = do
- pats' <- concat <$> zipWithM desugarLPat vars pats
- grhss' <- desugarGRHSs match_loc (sep (map ppr pats)) grhss
- -- tracePm "desugarMatch" (vcat [ppr pats, ppr pats', ppr grhss'])
- return PmMatch { pm_pats = pats', pm_grhss = grhss' }
-
-desugarGRHSs :: SrcSpan -> SDoc -> GRHSs GhcTc (LHsExpr GhcTc) -> DsM (NonEmpty (PmGRHS Pre))
-desugarGRHSs match_loc pp_pats grhss
- = traverse (desugarLGRHS match_loc pp_pats)
- . expectJust "desugarGRHSs"
- . NE.nonEmpty
- $ grhssGRHSs grhss
-
--- | Desugar a guarded right-hand side to a single 'GrdTree'
-desugarLGRHS :: SrcSpan -> SDoc -> LGRHS GhcTc (LHsExpr GhcTc) -> DsM (PmGRHS Pre)
-desugarLGRHS match_loc pp_pats (L _loc (GRHS _ gs _)) = do
- -- _loc points to the match separator (ie =, ->) that comes after the guards.
- -- Hence we have to pass in the match_loc, which we use in case that the RHS
- -- is unguarded.
- -- pp_pats is the space-separated pattern of the current Match this
- -- GRHS belongs to, so the @A B x@ part in @A B x | 0 <- x at .
- let rhs_info = case gs of
- [] -> L match_loc pp_pats
- (L grd_loc _):_ -> L grd_loc (pp_pats <+> vbar <+> interpp'SP gs)
- grds <- concatMapM (desugarGuard . unLoc) gs
- pure PmGRHS { pg_grds = grds, pg_rhs = rhs_info }
-
--- | Desugar a guard statement to a 'GrdVec'
-desugarGuard :: GuardStmt GhcTc -> DsM GrdVec
-desugarGuard guard = case guard of
- BodyStmt _ e _ _ -> desugarBoolGuard e
- LetStmt _ binds -> desugarLet (unLoc binds)
- BindStmt _ p e -> desugarBind p e
- LastStmt {} -> panic "desugarGuard LastStmt"
- ParStmt {} -> panic "desugarGuard ParStmt"
- TransStmt {} -> panic "desugarGuard TransStmt"
- RecStmt {} -> panic "desugarGuard RecStmt"
- ApplicativeStmt {} -> panic "desugarGuard ApplicativeLastStmt"
-
--- | Desugar let-bindings
-desugarLet :: HsLocalBinds GhcTc -> DsM GrdVec
-desugarLet _binds = return []
-
--- | Desugar a pattern guard
--- @pat <- e ==> let x = e; <guards for pat <- x>@
-desugarBind :: LPat GhcTc -> LHsExpr GhcTc -> DsM GrdVec
-desugarBind p e = dsLExpr e >>= \case
- Var y
- | Nothing <- isDataConId_maybe y
- -- RHS is a variable, so that will allow us to omit the let
- -> desugarLPat y p
- rhs -> do
- (x, grds) <- desugarLPatV p
- pure (PmLet x rhs : grds)
-
--- | Desugar a boolean guard
--- @e ==> let x = e; True <- x@
-desugarBoolGuard :: LHsExpr GhcTc -> DsM GrdVec
-desugarBoolGuard e
- | isJust (isTrueLHsExpr e) = return []
- -- The formal thing to do would be to generate (True <- True)
- -- but it is trivial to solve so instead we give back an empty
- -- GrdVec for efficiency
- | otherwise = dsLExpr e >>= \case
- Var y
- | Nothing <- isDataConId_maybe y
- -- Omit the let by matching on y
- -> pure [vanillaConGrd y trueDataCon []]
- rhs -> do
- x <- mkPmId boolTy
- pure [PmLet x rhs, vanillaConGrd x trueDataCon []]
-
-{- Note [Field match order for RecCon]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The order for RecCon field patterns actually determines evaluation order of
-the pattern match. For example:
-
- data T = T { a :: Char, b :: Int }
- f :: T -> ()
- f T{ b = 42, a = 'a' } = ()
-
-Then @f (T (error "a") (error "b"))@ errors out with "b" because it is mentioned
-first in the pattern match.
-
-This means we can't just desugar the pattern match to
-@[T a b <- x, 'a' <- a, 42 <- b]@. Instead we have to force them in the
-right order: @[T a b <- x, 42 <- b, 'a' <- a]@.
-
-Note [Order of guards matters]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Similar to Note [Field match order for RecCon], the order in which the guards
-for a pattern match appear matter. Consider a situation similar to T5117:
-
- f (0:_) = ()
- f (0:[]) = ()
-
-The latter clause is clearly redundant. Yet if we desugar the second clause as
-
- [x:xs' <- xs, [] <- xs', 0 <- x]
-
-We will say that the second clause only has an inaccessible RHS. That's because
-we force the tail of the list before comparing its head! So the correct
-translation would have been
-
- [x:xs' <- xs, 0 <- x, [] <- xs']
-
-And we have to take in the guards on list cells into @mkListGrds at .
-
-Note [Desugar CoPats]
-~~~~~~~~~~~~~~~~~~~~~~~
-The pattern match checker did not know how to handle coerced patterns
-`CoPat` efficiently, which gave rise to #11276. The original approach
-desugared `CoPat`s:
-
- pat |> co ===> x (pat <- (x |> co))
-
-Why did we do this seemingly unnecessary expansion in the first place?
-The reason is that the type of @pat |> co@ (which is the type of the value
-abstraction we match against) might be different than that of @pat at . Data
-instances such as @Sing (a :: Bool)@ are a good example of this: If we would
-just drop the coercion, we'd get a type error when matching @pat@ against its
-value abstraction, with the result being that pmIsSatisfiable decides that every
-possible data constructor fitting @pat@ is rejected as uninhabitated, leading to
-a lot of false warnings.
-
-But we can check whether the coercion is a hole or if it is just refl, in
-which case we can drop it.
--}
-
---
--- * Coverage checking guard trees into annotated trees
---
-
--- | Pattern-match coverage check result
-data CheckResult a
- = CheckResult
- { cr_ret :: !a
- -- ^ A hole for redundancy info and covered sets.
- , cr_uncov :: !Nablas
- -- ^ The set of uncovered values falling out at the bottom.
- -- (for -Wincomplete-patterns, but also important state for the algorithm)
- , cr_approx :: !Precision
- -- ^ A flag saying whether we ran into the 'maxPmCheckModels' limit for the
- -- purpose of suggesting to crank it up in the warning message. Writer state.
- } deriving Functor
-
-instance Outputable a => Outputable (CheckResult a) where
- ppr (CheckResult c unc pc)
- = text "CheckResult" <+> ppr_precision pc <+> braces (fsep
- [ field "ret" c <> comma
- , field "uncov" unc])
- where
- ppr_precision Precise = empty
- ppr_precision Approximate = text "(Approximate)"
- field name value = text name <+> equals <+> ppr value
-
--- | Lift 'addPmCts' over 'Nablas'.
-addPhiCtsNablas :: Nablas -> PhiCts -> DsM Nablas
-addPhiCtsNablas nablas cts = liftNablasM (\d -> addPhiCts d cts) nablas
-
--- | 'addPmCtsNablas' for a single 'PmCt'.
-addPhiCtNablas :: Nablas -> PhiCt -> DsM Nablas
-addPhiCtNablas nablas ct = addPhiCtsNablas nablas (unitBag ct)
-
--- | Test if any of the 'Nabla's is inhabited. Currently this is pure, because
--- we preserve the invariant that there are no uninhabited 'Nabla's. But that
--- could change in the future, for example by implementing this function in
--- terms of @notNull <$> generateInhabitingPatterns 1 ds at .
-isInhabited :: Nablas -> DsM Bool
-isInhabited (MkNablas ds) = pure (not (null ds))
-
--- | Coverage checking action. Can be composed 'leftToRight' or 'topToBottom'.
-newtype CheckAction a = CA { unCA :: Nablas -> DsM (CheckResult a) }
- deriving Functor
-
--- | Composes 'CheckAction's top-to-bottom:
--- If a value falls through the resulting action, then it must fall through the
--- first action and then through the second action.
--- If a value matches the resulting action, then it either matches the
--- first action or matches the second action.
--- Basically the semantics of the LYG branching construct.
-topToBottom :: (top -> bot -> ret)
- -> CheckAction top
- -> CheckAction bot
- -> CheckAction ret
-topToBottom f (CA top) (CA bot) = CA $ \inc -> do
- t <- top inc
- b <- bot (cr_uncov t)
- pure CheckResult { cr_ret = f (cr_ret t) (cr_ret b)
- , cr_uncov = cr_uncov b
- , cr_approx = cr_approx t Semi.<> cr_approx b }
-
-
--- | Composes 'CheckAction's left-to-right:
--- If a value falls through the resulting action, then it either falls through the
--- first action or through the second action.
--- If a value matches the resulting action, then it must match the first action
--- and then match the second action.
--- Basically the semantics of the LYG guard construct.
-leftToRight :: (RedSets -> right -> ret)
- -> CheckAction RedSets
- -> CheckAction right
- -> CheckAction ret
-leftToRight f (CA left) (CA right) = CA $ \inc -> do
- l <- left inc
- r <- right (rs_cov (cr_ret l))
- limit <- maxPmCheckModels <$> getDynFlags
- let uncov = cr_uncov l Semi.<> cr_uncov r
- -- See Note [Countering exponential blowup]
- let (prec', uncov') = throttle limit inc uncov
- pure CheckResult { cr_ret = f (cr_ret l) (cr_ret r)
- , cr_uncov = uncov'
- , cr_approx = prec' Semi.<> cr_approx l Semi.<> cr_approx r }
-
--- | @throttle limit old new@ returns @old@ if the number of 'Nabla's in @new@
--- is exceeding the given @limit@ and the @old@ number of 'Nabla's.
--- See Note [Countering exponential blowup].
-throttle :: Int -> Nablas -> Nablas -> (Precision, Nablas)
-throttle limit old@(MkNablas old_ds) new@(MkNablas new_ds)
- --- | pprTrace "PmCheck:throttle" (ppr (length old_ds) <+> ppr (length new_ds) <+> ppr limit) False = undefined
- | length new_ds > max limit (length old_ds) = (Approximate, old)
- | otherwise = (Precise, new)
-
-checkSequence :: (grdtree -> CheckAction anntree) -> NonEmpty grdtree -> CheckAction (NonEmpty anntree)
--- The implementation is pretty similar to
--- @traverse1 :: Apply f => (a -> f b) -> NonEmpty a -> f (NonEmpty b)@
-checkSequence act (t :| []) = (:| []) <$> act t
-checkSequence act (t1 :| (t2:ts)) =
- topToBottom (NE.<|) (act t1) (checkSequence act (t2:|ts))
-
-checkGrd :: PmGrd -> CheckAction RedSets
-checkGrd grd = CA $ \inc -> case grd of
- -- let x = e: Refine with x ~ e
- PmLet x e -> do
- matched <- addPhiCtNablas inc (PhiCoreCt x e)
- tracePm "check:Let" (ppr x <+> char '=' <+> ppr e)
- pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched }
- , cr_uncov = mempty
- , cr_approx = Precise }
- -- Bang x _: Diverge on x ~ ⊥, refine with x ≁ ⊥
- PmBang x mb_info -> do
- div <- addPhiCtNablas inc (PhiBotCt x)
- matched <- addPhiCtNablas inc (PhiNotBotCt x)
- -- See Note [Dead bang patterns]
- -- mb_info = Just info <==> PmBang originates from bang pattern in source
- let bangs | Just info <- mb_info = unitOL (div, info)
- | otherwise = NilOL
- tracePm "check:Bang" (ppr x <+> ppr div)
- pure CheckResult { cr_ret = RedSets { rs_cov = matched, rs_div = div, rs_bangs = bangs }
- , cr_uncov = mempty
- , cr_approx = Precise }
- -- Con: Fall through on x ≁ K and refine with x ~ K ys and type info
- PmCon x con tvs dicts args -> do
- !div <- if isPmAltConMatchStrict con
- then addPhiCtNablas inc (PhiBotCt x)
- else pure mempty
- !matched <- addPhiCtNablas inc (PhiConCt x con tvs (map evVarPred dicts) args)
- !uncov <- addPhiCtNablas inc (PhiNotConCt x con)
- tracePm "check:Con" $ vcat
- [ ppr grd
- , ppr inc
- , hang (text "div") 2 (ppr div)
- , hang (text "matched") 2 (ppr matched)
- , hang (text "uncov") 2 (ppr uncov)
- ]
- pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched, rs_div = div }
- , cr_uncov = uncov
- , cr_approx = Precise }
-
-checkGrds :: [PmGrd] -> CheckAction RedSets
-checkGrds [] = CA $ \inc ->
- pure CheckResult { cr_ret = emptyRedSets { rs_cov = inc }
- , cr_uncov = mempty
- , cr_approx = Precise }
-checkGrds (g:grds) = leftToRight merge (checkGrd g) (checkGrds grds)
- where
- merge ri_g ri_grds = -- This operation would /not/ form a Semigroup!
- RedSets { rs_cov = rs_cov ri_grds
- , rs_div = rs_div ri_g Semi.<> rs_div ri_grds
- , rs_bangs = rs_bangs ri_g Semi.<> rs_bangs ri_grds }
-
-checkMatchGroup :: PmMatchGroup Pre -> CheckAction (PmMatchGroup Post)
-checkMatchGroup (PmMatchGroup matches) =
- PmMatchGroup <$> checkSequence checkMatch matches
-
-checkMatch :: PmMatch Pre -> CheckAction (PmMatch Post)
-checkMatch (PmMatch { pm_pats = grds, pm_grhss = grhss }) =
- leftToRight PmMatch (checkGrds grds) (checkGRHSs grhss)
-
-checkGRHSs :: NonEmpty (PmGRHS Pre) -> CheckAction (NonEmpty (PmGRHS Post))
-checkGRHSs = checkSequence checkGRHS
-
-checkGRHS :: PmGRHS Pre -> CheckAction (PmGRHS Post)
-checkGRHS (PmGRHS { pg_grds = grds, pg_rhs = rhs_info }) =
- flip PmGRHS rhs_info <$> checkGrds grds
-
-checkEmptyCase :: PmEmptyCase -> CheckAction PmEmptyCase
-checkEmptyCase pe@(PmEmptyCase { pe_var = var }) = CA $ \inc -> do
- unc <- addPhiCtNablas inc (PhiNotBotCt var)
- pure CheckResult { cr_ret = pe, cr_uncov = unc, cr_approx = mempty }
-
-checkPatBind :: (PmPatBind Pre) -> CheckAction (PmPatBind Post)
-checkPatBind = coerce checkGRHS
-
-{- Note [Countering exponential blowup]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Precise pattern match exhaustiveness checking is necessarily exponential in
-the size of some input programs. We implement a counter-measure in the form of
-the -fmax-pmcheck-models flag, limiting the number of Nablas we check against
-each pattern by a constant.
-
-How do we do that? Consider
-
- f True True = ()
- f True True = ()
-
-And imagine we set our limit to 1 for the sake of the example. The first clause
-will be checked against the initial Nabla, {}. Doing so will produce an
-Uncovered set of size 2, containing the models {x≁True} and {x~True,y≁True}.
-Also we find the first clause to cover the model {x~True,y~True}.
-
-But the Uncovered set we get out of the match is too huge! We somehow have to
-ensure not to make things worse as they are already, so we continue checking
-with a singleton Uncovered set of the initial Nabla {}. Why is this
-sound (wrt. the notion in GADTs Meet Their Match)? Well, it basically amounts
-to forgetting that we matched against the first clause. The values represented
-by {} are a superset of those represented by its two refinements {x≁True} and
-{x~True,y≁True}.
-
-This forgetfulness becomes very apparent in the example above: By continuing
-with {} we don't detect the second clause as redundant, as it again covers the
-same non-empty subset of {}. So we don't flag everything as redundant anymore,
-but still will never flag something as redundant that isn't.
-
-For exhaustivity, the converse applies: We will report @f@ as non-exhaustive
-and report @f _ _@ as missing, which is a superset of the actual missing
-matches. But soundness means we will never fail to report a missing match.
-
-This mechanism is implemented in 'throttle'.
-
-Guards are an extreme example in this regard, with #11195 being a particularly
-dreadful example: Since their RHS are often pretty much unique, we split on a
-variable (the one representing the RHS) that doesn't occur anywhere else in the
-program, so we don't actually get useful information out of that split!
-}
--
@@ -1188,14 +341,14 @@ reportWarnings dflags ctx@(DsMatchContext kind loc) vars
when (approx && (exists_u || exists_i)) $
putSrcSpanDs loc (warnDs NoReason approx_msg)
- when exists_b $ forM_ redundant_bangs $ \(L l q) -> do
+ when exists_b $ forM_ redundant_bangs $ \(SrcInfo (L l q)) -> do
putSrcSpanDs l (warnDs (Reason Opt_WarnRedundantBangPatterns)
(pprEqn q "has redundant bang"))
- when exists_r $ forM_ redundant_rhss $ \(L l q) -> do
+ when exists_r $ forM_ redundant_rhss $ \(SrcInfo (L l q)) -> do
putSrcSpanDs l (warnDs (Reason Opt_WarnOverlappingPatterns)
(pprEqn q "is redundant"))
- when exists_i $ forM_ inaccessible_rhss $ \(L l q) -> do
+ when exists_i $ forM_ inaccessible_rhss $ \(SrcInfo (L l q)) -> do
putSrcSpanDs l (warnDs (Reason Opt_WarnOverlappingPatterns)
(pprEqn q "has inaccessible right hand side"))
@@ -1204,7 +357,7 @@ reportWarnings dflags ctx@(DsMatchContext kind loc) vars
where
flag_i = overlapping dflags kind
flag_u = exhaustive dflags kind
- flag_b = redundant_bang dflags
+ flag_b = redundantBang dflags
flag_u_reason = maybe NoReason Reason (exhaustiveWarningFlag kind)
maxPatterns = maxUncoveredPatterns dflags
@@ -1263,105 +416,7 @@ pprContext singular (DsMatchContext kind _loc) msg rest_of_msg_fun
_ -> (pprMatchContext kind, \ pp -> pp)
--
--- * Utilities
---
-
--- | All warning flags that need to run the pattern match checker.
-allPmCheckWarnings :: [WarningFlag]
-allPmCheckWarnings =
- [ Opt_WarnIncompletePatterns
- , Opt_WarnIncompleteUniPatterns
- , Opt_WarnIncompletePatternsRecUpd
- , Opt_WarnOverlappingPatterns
- ]
-
--- | Check whether the redundancy checker should run (redundancy only)
-overlapping :: DynFlags -> HsMatchContext id -> Bool
--- See Note [Inaccessible warnings for record updates]
-overlapping _ RecUpd = False
-overlapping dflags _ = wopt Opt_WarnOverlappingPatterns dflags
-
--- | Check whether the exhaustiveness checker should run (exhaustiveness only)
-exhaustive :: DynFlags -> HsMatchContext id -> Bool
-exhaustive dflags = maybe False (`wopt` dflags) . exhaustiveWarningFlag
-
--- | Check whether unnecessary bangs should be warned about
-redundant_bang :: DynFlags -> Bool
-redundant_bang dflags = wopt Opt_WarnRedundantBangPatterns dflags
-
--- | Denotes whether an exhaustiveness check is supported, and if so,
--- via which 'WarningFlag' it's controlled.
--- Returns 'Nothing' if check is not supported.
-exhaustiveWarningFlag :: HsMatchContext id -> Maybe WarningFlag
-exhaustiveWarningFlag (FunRhs {}) = Just Opt_WarnIncompletePatterns
-exhaustiveWarningFlag CaseAlt = Just Opt_WarnIncompletePatterns
-exhaustiveWarningFlag IfAlt = Just Opt_WarnIncompletePatterns
-exhaustiveWarningFlag LambdaExpr = Just Opt_WarnIncompleteUniPatterns
-exhaustiveWarningFlag PatBindRhs = Just Opt_WarnIncompleteUniPatterns
-exhaustiveWarningFlag PatBindGuards = Just Opt_WarnIncompletePatterns
-exhaustiveWarningFlag ProcExpr = Just Opt_WarnIncompleteUniPatterns
-exhaustiveWarningFlag RecUpd = Just Opt_WarnIncompletePatternsRecUpd
-exhaustiveWarningFlag ThPatSplice = Nothing
-exhaustiveWarningFlag PatSyn = Nothing
-exhaustiveWarningFlag ThPatQuote = Nothing
--- Don't warn about incomplete patterns in list comprehensions, pattern guards
--- etc. They are often *supposed* to be incomplete
-exhaustiveWarningFlag (StmtCtxt {}) = Nothing
-
--- | Check whether any part of pattern match checking is enabled for this
--- 'HsMatchContext' (does not matter whether it is the redundancy check or the
--- exhaustiveness check).
-isMatchContextPmChecked :: DynFlags -> Origin -> HsMatchContext id -> Bool
-isMatchContextPmChecked dflags origin kind
- | isGenerated origin
- = False
- | otherwise
- = overlapping dflags kind || exhaustive dflags kind
-
--- | Return True when any of the pattern match warnings ('allPmCheckWarnings')
--- are enabled, in which case we need to run the pattern match checker.
-needToRunPmCheck :: DynFlags -> Origin -> Bool
-needToRunPmCheck dflags origin
- | isGenerated origin
- = False
- | otherwise
- = notNull (filter (`wopt` dflags) allPmCheckWarnings)
-
-{- Note [Inaccessible warnings for record updates]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider (#12957)
- data T a where
- T1 :: { x :: Int } -> T Bool
- T2 :: { x :: Int } -> T a
- T3 :: T a
-
- f :: T Char -> T a
- f r = r { x = 3 }
-
-The desugarer will conservatively generate a case for T1 even though
-it's impossible:
- f r = case r of
- T1 x -> T1 3 -- Inaccessible branch
- T2 x -> T2 3
- _ -> error "Missing"
-
-We don't want to warn about the inaccessible branch because the programmer
-didn't put it there! So we filter out the warning here.
-
-The same can happen for long distance term constraints instead of type
-constraints (#17783):
-
- data T = A { x :: Int } | B { x :: Int }
- f r at A{} = r { x = 3 }
- f _ = B 0
-
-Here, the long distance info from the FunRhs match (@r ~ A x@) will make the
-clause matching on @B@ of the desugaring to @case@ redundant. It's generated
-code that we don't want to warn about.
--}
-
---
--- * Long-distance information
+-- * Adding external long-distance information
--
-- | Locally update 'dsl_nablas' with the given action, but defer evaluation
=====================================
compiler/GHC/HsToCore/Pmc/Check.hs
=====================================
@@ -0,0 +1,276 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE FlexibleInstances #-}
+
+-- | Coverage checking step of the
+-- [Lower Your Guards paper](https://dl.acm.org/doi/abs/10.1145/3408989).
+--
+-- Coverage check guard trees (like @'PmMatch' 'Pre'@) to get a
+-- 'CheckResult', containing
+--
+-- 1. The set of uncovered values, 'cr_uncov'
+-- 2. And an annotated tree variant (like @'PmMatch' 'Post'@) that captures
+-- redundancy and inaccessibility information as 'RedSets' annotations
+--
+-- Basically the UA function from Section 5.1, which is an optimised
+-- interleaving of U and A from Section 3.2 (Figure 5).
+-- The Normalised Refinement Types 'Nablas' are maintained in
+-- "GHC.HsToCore.Pmc.Solver".
+module GHC.HsToCore.Pmc.Check (
+ CheckAction(..),
+ checkMatchGroup, checkGRHSs, checkPatBind, checkEmptyCase
+ ) where
+
+#include "HsVersions.h"
+
+import GHC.Prelude
+
+import GHC.HsToCore.Monad ( DsM )
+import GHC.HsToCore.Pmc.Types
+import GHC.HsToCore.Pmc.Utils
+import GHC.HsToCore.Pmc.Solver
+import GHC.Driver.Session
+import GHC.Utils.Outputable
+import GHC.Tc.Utils.TcType (evVarPred)
+import GHC.Data.OrdList
+
+import qualified Data.Semigroup as Semi
+import Data.List.NonEmpty ( NonEmpty(..) )
+import qualified Data.List.NonEmpty as NE
+import Data.Coerce
+
+-- | Coverage checking action. Can be composed 'leftToRight' or 'topToBottom'.
+newtype CheckAction a = CA { unCA :: Nablas -> DsM (CheckResult a) }
+ deriving Functor
+
+-- | Composes 'CheckAction's top-to-bottom:
+-- If a value falls through the resulting action, then it must fall through the
+-- first action and then through the second action.
+-- If a value matches the resulting action, then it either matches the
+-- first action or matches the second action.
+-- Basically the semantics of the LYG branching construct.
+topToBottom :: (top -> bot -> ret)
+ -> CheckAction top
+ -> CheckAction bot
+ -> CheckAction ret
+topToBottom f (CA top) (CA bot) = CA $ \inc -> do
+ t <- top inc
+ b <- bot (cr_uncov t)
+ pure CheckResult { cr_ret = f (cr_ret t) (cr_ret b)
+ , cr_uncov = cr_uncov b
+ , cr_approx = cr_approx t Semi.<> cr_approx b }
+
+
+-- | Composes 'CheckAction's left-to-right:
+-- If a value falls through the resulting action, then it either falls through the
+-- first action or through the second action.
+-- If a value matches the resulting action, then it must match the first action
+-- and then match the second action.
+-- Basically the semantics of the LYG guard construct.
+leftToRight :: (RedSets -> right -> ret)
+ -> CheckAction RedSets
+ -> CheckAction right
+ -> CheckAction ret
+leftToRight f (CA left) (CA right) = CA $ \inc -> do
+ l <- left inc
+ r <- right (rs_cov (cr_ret l))
+ limit <- maxPmCheckModels <$> getDynFlags
+ let uncov = cr_uncov l Semi.<> cr_uncov r
+ -- See Note [Countering exponential blowup]
+ let (prec', uncov') = throttle limit inc uncov
+ pure CheckResult { cr_ret = f (cr_ret l) (cr_ret r)
+ , cr_uncov = uncov'
+ , cr_approx = prec' Semi.<> cr_approx l Semi.<> cr_approx r }
+
+-- | @throttle limit old new@ returns @old@ if the number of 'Nabla's in @new@
+-- is exceeding the given @limit@ and the @old@ number of 'Nabla's.
+-- See Note [Countering exponential blowup].
+throttle :: Int -> Nablas -> Nablas -> (Precision, Nablas)
+throttle limit old@(MkNablas old_ds) new@(MkNablas new_ds)
+ --- | pprTrace "PmCheck:throttle" (ppr (length old_ds) <+> ppr (length new_ds) <+> ppr limit) False = undefined
+ | length new_ds > max limit (length old_ds) = (Approximate, old)
+ | otherwise = (Precise, new)
+
+checkSequence :: (grdtree -> CheckAction anntree) -> NonEmpty grdtree -> CheckAction (NonEmpty anntree)
+-- The implementation is pretty similar to
+-- @traverse1 :: Apply f => (a -> f b) -> NonEmpty a -> f (NonEmpty b)@
+checkSequence act (t :| []) = (:| []) <$> act t
+checkSequence act (t1 :| (t2:ts)) =
+ topToBottom (NE.<|) (act t1) (checkSequence act (t2:|ts))
+
+emptyRedSets :: RedSets
+-- Semigroup instance would be misleading!
+emptyRedSets = RedSets mempty mempty mempty
+
+checkGrd :: PmGrd -> CheckAction RedSets
+checkGrd grd = CA $ \inc -> case grd of
+ -- let x = e: Refine with x ~ e
+ PmLet x e -> do
+ matched <- addPhiCtNablas inc (PhiCoreCt x e)
+ tracePm "check:Let" (ppr x <+> char '=' <+> ppr e)
+ pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched }
+ , cr_uncov = mempty
+ , cr_approx = Precise }
+ -- Bang x _: Diverge on x ~ ⊥, refine with x ≁ ⊥
+ PmBang x mb_info -> do
+ div <- addPhiCtNablas inc (PhiBotCt x)
+ matched <- addPhiCtNablas inc (PhiNotBotCt x)
+ -- See Note [Dead bang patterns]
+ -- mb_info = Just info <==> PmBang originates from bang pattern in source
+ let bangs | Just info <- mb_info = unitOL (div, info)
+ | otherwise = NilOL
+ tracePm "check:Bang" (ppr x <+> ppr div)
+ pure CheckResult { cr_ret = RedSets { rs_cov = matched, rs_div = div, rs_bangs = bangs }
+ , cr_uncov = mempty
+ , cr_approx = Precise }
+ -- Con: Fall through on x ≁ K and refine with x ~ K ys and type info
+ PmCon x con tvs dicts args -> do
+ !div <- if isPmAltConMatchStrict con
+ then addPhiCtNablas inc (PhiBotCt x)
+ else pure mempty
+ !matched <- addPhiCtNablas inc (PhiConCt x con tvs (map evVarPred dicts) args)
+ !uncov <- addPhiCtNablas inc (PhiNotConCt x con)
+ tracePm "check:Con" $ vcat
+ [ ppr grd
+ , ppr inc
+ , hang (text "div") 2 (ppr div)
+ , hang (text "matched") 2 (ppr matched)
+ , hang (text "uncov") 2 (ppr uncov)
+ ]
+ pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched, rs_div = div }
+ , cr_uncov = uncov
+ , cr_approx = Precise }
+
+checkGrds :: [PmGrd] -> CheckAction RedSets
+checkGrds [] = CA $ \inc ->
+ pure CheckResult { cr_ret = emptyRedSets { rs_cov = inc }
+ , cr_uncov = mempty
+ , cr_approx = Precise }
+checkGrds (g:grds) = leftToRight merge (checkGrd g) (checkGrds grds)
+ where
+ merge ri_g ri_grds = -- This operation would /not/ form a Semigroup!
+ RedSets { rs_cov = rs_cov ri_grds
+ , rs_div = rs_div ri_g Semi.<> rs_div ri_grds
+ , rs_bangs = rs_bangs ri_g Semi.<> rs_bangs ri_grds }
+
+checkMatchGroup :: PmMatchGroup Pre -> CheckAction (PmMatchGroup Post)
+checkMatchGroup (PmMatchGroup matches) =
+ PmMatchGroup <$> checkSequence checkMatch matches
+
+checkMatch :: PmMatch Pre -> CheckAction (PmMatch Post)
+checkMatch (PmMatch { pm_pats = GrdVec grds, pm_grhss = grhss }) =
+ leftToRight PmMatch (checkGrds grds) (checkGRHSs grhss)
+
+checkGRHSs :: NonEmpty (PmGRHS Pre) -> CheckAction (NonEmpty (PmGRHS Post))
+checkGRHSs = checkSequence checkGRHS
+
+checkGRHS :: PmGRHS Pre -> CheckAction (PmGRHS Post)
+checkGRHS (PmGRHS { pg_grds = GrdVec grds, pg_rhs = rhs_info }) =
+ flip PmGRHS rhs_info <$> checkGrds grds
+
+checkEmptyCase :: PmEmptyCase -> CheckAction PmEmptyCase
+-- See Note [Checking EmptyCase]
+checkEmptyCase pe@(PmEmptyCase { pe_var = var }) = CA $ \inc -> do
+ unc <- addPhiCtNablas inc (PhiNotBotCt var)
+ pure CheckResult { cr_ret = pe, cr_uncov = unc, cr_approx = mempty }
+
+checkPatBind :: (PmPatBind Pre) -> CheckAction (PmPatBind Post)
+checkPatBind = coerce checkGRHS
+
+{- Note [Checking EmptyCase]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-XEmptyCase is useful for matching on empty data types like 'Void'. For example,
+the following is a complete match:
+
+ f :: Void -> ()
+ f x = case x of {}
+
+Really, -XEmptyCase is the only way to write a program that at the same time is
+safe (@f _ = error "boom"@ is not because of ⊥), doesn't trigger a warning
+(@f !_ = error "inaccessible" has inaccessible RHS) and doesn't turn an
+exception into divergence (@f x = f x@).
+
+Semantically, unlike every other case expression, -XEmptyCase is strict in its
+match var x, which rules out ⊥ as an inhabitant. So we add x ≁ ⊥ to the
+initial Nabla and check if there are any values left to match on.
+
+Note [Dead bang patterns]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+
+ f :: Bool -> Int
+ f True = 1
+ f !x = 2
+
+Whenever we fall through to the second equation, we will already have evaluated
+the argument. Thus, the bang pattern serves no purpose and should be warned
+about. We call this kind of bang patterns "dead". Dead bangs are the ones
+that under no circumstances can force a thunk that wasn't already forced.
+Dead bangs are a form of redundant bangs; see below.
+
+We can detect dead bang patterns by checking whether @x ~ ⊥@ is satisfiable
+where the PmBang appears in 'checkGrd'. If not, then clearly the bang is
+dead. So for a source bang, we add the refined Nabla and the source info to
+the 'RedSet's 'rs_bangs'. When collecting stuff to warn, we test that Nabla for
+inhabitants. If it's empty, we'll warn that it's redundant.
+
+Note that we don't want to warn for a dead bang that appears on a redundant
+clause. That is because in that case, we recommend to delete the clause wholly,
+including its leading pattern match.
+
+Dead bang patterns are redundant. But there are bang patterns which are
+redundant that aren't dead, for example
+
+ f !() = 0
+
+the bang still forces the match variable, before we attempt to match on (). But
+it is redundant with the forcing done by the () match. We currently don't
+detect redundant bangs that aren't dead.
+
+Note [Countering exponential blowup]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Precise pattern match exhaustiveness checking is necessarily exponential in
+the size of some input programs. We implement a counter-measure in the form of
+the -fmax-pmcheck-models flag, limiting the number of Nablas we check against
+each pattern by a constant.
+
+How do we do that? Consider
+
+ f True True = ()
+ f True True = ()
+
+And imagine we set our limit to 1 for the sake of the example. The first clause
+will be checked against the initial Nabla, {}. Doing so will produce an
+Uncovered set of size 2, containing the models {x≁True} and {x~True,y≁True}.
+Also we find the first clause to cover the model {x~True,y~True}.
+
+But the Uncovered set we get out of the match is too huge! We somehow have to
+ensure not to make things worse as they are already, so we continue checking
+with a singleton Uncovered set of the initial Nabla {}. Why is this
+sound (wrt. the notion in GADTs Meet Their Match)? Well, it basically amounts
+to forgetting that we matched against the first clause. The values represented
+by {} are a superset of those represented by its two refinements {x≁True} and
+{x~True,y≁True}.
+
+This forgetfulness becomes very apparent in the example above: By continuing
+with {} we don't detect the second clause as redundant, as it again covers the
+same non-empty subset of {}. So we don't flag everything as redundant anymore,
+but still will never flag something as redundant that isn't.
+
+For exhaustivity, the converse applies: We will report @f@ as non-exhaustive
+and report @f _ _@ as missing, which is a superset of the actual missing
+matches. But soundness means we will never fail to report a missing match.
+
+This mechanism is implemented in 'throttle'.
+
+Guards are an extreme example in this regard, with #11195 being a particularly
+dreadful example: Since their RHS are often pretty much unique, we split on a
+variable (the one representing the RHS) that doesn't occur anywhere else in the
+program, so we don't actually get useful information out of that split!
+-}
=====================================
compiler/GHC/HsToCore/Pmc/Desugar.hs
=====================================
@@ -0,0 +1,450 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE FlexibleInstances #-}
+
+-- | Desugaring step of the
+-- [Lower Your Guards paper](https://dl.acm.org/doi/abs/10.1145/3408989).
+--
+-- Desugars Haskell source syntax into guard tree variants Pm*.
+-- In terms of the paper, this module is concerned with Sections 3.1, Figure 4,
+-- in particular.
+module GHC.HsToCore.Pmc.Desugar (
+ desugarPatBind, desugarGRHSs, desugarMatches, desugarEmptyCase
+ ) where
+
+#include "HsVersions.h"
+
+import GHC.Prelude
+
+import GHC.HsToCore.Pmc.Types
+import GHC.HsToCore.Pmc.Utils
+import GHC.Core (Expr(Var,App))
+import GHC.Data.FastString (unpackFS, lengthFS)
+import GHC.Driver.Session
+import GHC.Hs
+import GHC.Tc.Utils.Zonk (shortCutLit)
+import GHC.Types.Id
+import GHC.Core.ConLike
+import GHC.Types.Name
+import GHC.Builtin.Types
+import GHC.Types.SrcLoc
+import GHC.Utils.Outputable
+import GHC.Utils.Panic
+import GHC.Core.DataCon
+import GHC.Types.Var (EvVar)
+import GHC.Core.Coercion
+import GHC.Tc.Types.Evidence (HsWrapper(..), isIdHsWrapper)
+import {-# SOURCE #-} GHC.HsToCore.Expr (dsExpr, dsLExpr, dsSyntaxExpr)
+import {-# SOURCE #-} GHC.HsToCore.Binds (dsHsWrapper)
+import GHC.HsToCore.Utils (selectMatchVar)
+import GHC.HsToCore.Match.Literal (dsLit, dsOverLit)
+import GHC.HsToCore.Monad
+import GHC.Core.TyCo.Rep
+import GHC.Core.Type
+import GHC.HsToCore.Utils (isTrueLHsExpr)
+import GHC.Data.Maybe
+import qualified GHC.LanguageExtensions as LangExt
+import GHC.Utils.Monad (concatMapM)
+
+import Control.Monad (zipWithM)
+import Data.List (elemIndex)
+import Data.List.NonEmpty ( NonEmpty(..) )
+import qualified Data.List.NonEmpty as NE
+
+-- | Smart constructor that eliminates trivial lets
+mkPmLetVar :: Id -> Id -> [PmGrd]
+mkPmLetVar x y | x == y = []
+mkPmLetVar x y = [PmLet x (Var y)]
+
+-- | ADT constructor pattern => no existentials, no local constraints
+vanillaConGrd :: Id -> DataCon -> [Id] -> PmGrd
+vanillaConGrd scrut con arg_ids =
+ PmCon { pm_id = scrut, pm_con_con = PmAltConLike (RealDataCon con)
+ , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = arg_ids }
+
+-- | Creates a '[PmGrd]' refining a match var of list type to a list,
+-- where list fields are matched against the incoming tagged '[PmGrd]'s.
+-- For example:
+-- @mkListGrds "a" "[(x, True <- x),(y, !y)]"@
+-- to
+-- @"[(x:b) <- a, True <- x, (y:c) <- b, !y, [] <- c]"@
+-- where @b@ and @c@ are freshly allocated in @mkListGrds@ and @a@ is the match
+-- variable.
+mkListGrds :: Id -> [(Id, [PmGrd])] -> DsM [PmGrd]
+-- See Note [Order of guards matter] for why we need to intertwine guards
+-- on list elements.
+mkListGrds a [] = pure [vanillaConGrd a nilDataCon []]
+mkListGrds a ((x, head_grds):xs) = do
+ b <- mkPmId (idType a)
+ tail_grds <- mkListGrds b xs
+ pure $ vanillaConGrd a consDataCon [x, b] : head_grds ++ tail_grds
+
+-- | Create a '[PmGrd]' refining a match variable to a 'PmLit'.
+mkPmLitGrds :: Id -> PmLit -> DsM [PmGrd]
+mkPmLitGrds x (PmLit _ (PmLitString s)) = do
+ -- We desugar String literals to list literals for better overlap reasoning.
+ -- It's a little unfortunate we do this here rather than in
+ -- 'GHC.HsToCore.Pmc.Solver.trySolve' and
+ -- 'GHC.HsToCore.Pmc.Solver.addRefutableAltCon', but it's so much simpler
+ -- here. See Note [Representation of Strings in TmState] in
+ -- GHC.HsToCore.Pmc.Solver
+ vars <- traverse mkPmId (take (lengthFS s) (repeat charTy))
+ let mk_char_lit y c = mkPmLitGrds y (PmLit charTy (PmLitChar c))
+ char_grdss <- zipWithM mk_char_lit vars (unpackFS s)
+ mkListGrds x (zip vars char_grdss)
+mkPmLitGrds x lit = do
+ let grd = PmCon { pm_id = x
+ , pm_con_con = PmAltLit lit
+ , pm_con_tvs = []
+ , pm_con_dicts = []
+ , pm_con_args = [] }
+ pure [grd]
+
+-- | @desugarPat _ x pat@ transforms @pat@ into a '[PmGrd]', where
+-- the variable representing the match is @x at .
+desugarPat :: Id -> Pat GhcTc -> DsM [PmGrd]
+desugarPat x pat = case pat of
+ WildPat _ty -> pure []
+ VarPat _ y -> pure (mkPmLetVar (unLoc y) x)
+ ParPat _ p -> desugarLPat x p
+ LazyPat _ _ -> pure [] -- like a wildcard
+ BangPat _ p@(L l p') ->
+ -- Add the bang in front of the list, because it will happen before any
+ -- nested stuff.
+ (PmBang x pm_loc :) <$> desugarLPat x p
+ where pm_loc = Just (SrcInfo (L l (ppr p')))
+
+ -- (x at pat) ==> Desugar pat with x as match var and handle impedance
+ -- mismatch with incoming match var
+ AsPat _ (L _ y) p -> (mkPmLetVar y x ++) <$> desugarLPat y p
+
+ SigPat _ p _ty -> desugarLPat x p
+
+ -- See Note [Desugar CoPats]
+ -- Generally the translation is
+ -- pat |> co ===> let y = x |> co, pat <- y where y is a match var of pat
+ XPat (CoPat wrapper p _ty)
+ | isIdHsWrapper wrapper -> desugarPat x p
+ | WpCast co <- wrapper, isReflexiveCo co -> desugarPat x p
+ | otherwise -> do
+ (y, grds) <- desugarPatV p
+ wrap_rhs_y <- dsHsWrapper wrapper
+ pure (PmLet y (wrap_rhs_y (Var x)) : grds)
+
+ -- (n + k) ===> let b = x >= k, True <- b, let n = x-k
+ NPlusKPat _pat_ty (L _ n) k1 k2 ge minus -> do
+ b <- mkPmId boolTy
+ let grd_b = vanillaConGrd b trueDataCon []
+ [ke1, ke2] <- traverse dsOverLit [unLoc k1, k2]
+ rhs_b <- dsSyntaxExpr ge [Var x, ke1]
+ rhs_n <- dsSyntaxExpr minus [Var x, ke2]
+ pure [PmLet b rhs_b, grd_b, PmLet n rhs_n]
+
+ -- (fun -> pat) ===> let y = fun x, pat <- y where y is a match var of pat
+ ViewPat _arg_ty lexpr pat -> do
+ (y, grds) <- desugarLPatV pat
+ fun <- dsLExpr lexpr
+ pure $ PmLet y (App fun (Var x)) : grds
+
+ -- list
+ ListPat (ListPatTc _elem_ty Nothing) ps ->
+ desugarListPat x ps
+
+ -- overloaded list
+ ListPat (ListPatTc elem_ty (Just (pat_ty, to_list))) pats -> do
+ dflags <- getDynFlags
+ case splitListTyConApp_maybe pat_ty of
+ Just _e_ty
+ | not (xopt LangExt.RebindableSyntax dflags)
+ -- Just desugar it as a regular ListPat
+ -> desugarListPat x pats
+ _ -> do
+ y <- mkPmId (mkListTy elem_ty)
+ grds <- desugarListPat y pats
+ rhs_y <- dsSyntaxExpr to_list [Var x]
+ pure $ PmLet y rhs_y : grds
+
+ -- (a) In the presence of RebindableSyntax, we don't know anything about
+ -- `toList`, we should treat `ListPat` as any other view pattern.
+ --
+ -- (b) In the absence of RebindableSyntax,
+ -- - If the pat_ty is `[a]`, then we treat the overloaded list pattern
+ -- as ordinary list pattern. Although we can give an instance
+ -- `IsList [Int]` (more specific than the default `IsList [a]`), in
+ -- practice, we almost never do that. We assume the `to_list` is
+ -- the `toList` from `instance IsList [a]`.
+ --
+ -- - Otherwise, we treat the `ListPat` as ordinary view pattern.
+ --
+ -- See #14547, especially comment#9 and comment#10.
+
+ ConPat { pat_con = L _ con
+ , pat_args = ps
+ , pat_con_ext = ConPatTc
+ { cpt_arg_tys = arg_tys
+ , cpt_tvs = ex_tvs
+ , cpt_dicts = dicts
+ }
+ } -> do
+ desugarConPatOut x con arg_tys ex_tvs dicts ps
+
+ NPat ty (L _ olit) mb_neg _ -> do
+ -- See Note [Literal short cut] in "GHC.HsToCore.Match.Literal"
+ -- We inline the Literal short cut for @ty@ here, because @ty@ is more
+ -- precise than the field of OverLitTc, which is all that dsOverLit (which
+ -- normally does the literal short cut) can look at. Also @ty@ matches the
+ -- type of the scrutinee, so info on both pattern and scrutinee (for which
+ -- short cutting in dsOverLit works properly) is overloaded iff either is.
+ dflags <- getDynFlags
+ let platform = targetPlatform dflags
+ core_expr <- case olit of
+ OverLit{ ol_val = val, ol_ext = OverLitTc rebindable _ }
+ | not rebindable
+ , Just expr <- shortCutLit platform val ty
+ -> dsExpr expr
+ _ -> dsOverLit olit
+ let lit = expectJust "failed to detect OverLit" (coreExprAsPmLit core_expr)
+ let lit' = case mb_neg of
+ Just _ -> expectJust "failed to negate lit" (negatePmLit lit)
+ Nothing -> lit
+ mkPmLitGrds x lit'
+
+ LitPat _ lit -> do
+ core_expr <- dsLit (convertLit lit)
+ let lit = expectJust "failed to detect Lit" (coreExprAsPmLit core_expr)
+ mkPmLitGrds x lit
+
+ TuplePat _tys pats boxity -> do
+ (vars, grdss) <- mapAndUnzipM desugarLPatV pats
+ let tuple_con = tupleDataCon boxity (length vars)
+ pure $ vanillaConGrd x tuple_con vars : concat grdss
+
+ SumPat _ty p alt arity -> do
+ (y, grds) <- desugarLPatV p
+ let sum_con = sumDataCon alt arity
+ -- See Note [Unboxed tuple RuntimeRep vars] in GHC.Core.TyCon
+ pure $ vanillaConGrd x sum_con [y] : grds
+
+ SplicePat {} -> panic "Check.desugarPat: SplicePat"
+
+-- | 'desugarPat', but also select and return a new match var.
+desugarPatV :: Pat GhcTc -> DsM (Id, [PmGrd])
+desugarPatV pat = do
+ x <- selectMatchVar Many pat
+ grds <- desugarPat x pat
+ pure (x, grds)
+
+desugarLPat :: Id -> LPat GhcTc -> DsM [PmGrd]
+desugarLPat x = desugarPat x . unLoc
+
+-- | 'desugarLPat', but also select and return a new match var.
+desugarLPatV :: LPat GhcTc -> DsM (Id, [PmGrd])
+desugarLPatV = desugarPatV . unLoc
+
+-- | @desugarListPat _ x [p1, ..., pn]@ is basically
+-- @desugarConPatOut _ x $(mkListConPatOuts [p1, ..., pn]>@ without ever
+-- constructing the 'ConPatOut's.
+desugarListPat :: Id -> [LPat GhcTc] -> DsM [PmGrd]
+desugarListPat x pats = do
+ vars_and_grdss <- traverse desugarLPatV pats
+ mkListGrds x vars_and_grdss
+
+-- | Desugar a constructor pattern
+desugarConPatOut :: Id -> ConLike -> [Type] -> [TyVar]
+ -> [EvVar] -> HsConPatDetails GhcTc -> DsM [PmGrd]
+desugarConPatOut x con univ_tys ex_tvs dicts = \case
+ PrefixCon ps -> go_field_pats (zip [0..] ps)
+ InfixCon p1 p2 -> go_field_pats (zip [0..] [p1,p2])
+ RecCon (HsRecFields fs _) -> go_field_pats (rec_field_ps fs)
+ where
+ -- The actual argument types (instantiated)
+ arg_tys = map scaledThing $ conLikeInstOrigArgTys con (univ_tys ++ mkTyVarTys ex_tvs)
+
+ -- Extract record field patterns tagged by field index from a list of
+ -- LHsRecField
+ rec_field_ps fs = map (tagged_pat . unLoc) fs
+ where
+ tagged_pat f = (lbl_to_index (getName (hsRecFieldId f)), hsRecFieldArg f)
+ -- Unfortunately the label info is empty when the DataCon wasn't defined
+ -- with record field labels, hence we desugar to field index.
+ orig_lbls = map flSelector $ conLikeFieldLabels con
+ lbl_to_index lbl = expectJust "lbl_to_index" $ elemIndex lbl orig_lbls
+
+ go_field_pats tagged_pats = do
+ -- The fields that appear might not be in the correct order. So
+ -- 1. Do the PmCon match
+ -- 2. Then pattern match on the fields in the order given by the first
+ -- field of @tagged_pats at .
+ -- See Note [Field match order for RecCon]
+
+ -- Desugar the mentioned field patterns. We're doing this first to get
+ -- the Ids for pm_con_args and bring them in order afterwards.
+ let trans_pat (n, pat) = do
+ (var, pvec) <- desugarLPatV pat
+ pure ((n, var), pvec)
+ (tagged_vars, arg_grdss) <- mapAndUnzipM trans_pat tagged_pats
+
+ let get_pat_id n ty = case lookup n tagged_vars of
+ Just var -> pure var
+ Nothing -> mkPmId ty
+
+ -- 1. the constructor pattern match itself
+ arg_ids <- zipWithM get_pat_id [0..] arg_tys
+ let con_grd = PmCon x (PmAltConLike con) ex_tvs dicts arg_ids
+
+ -- 2. guards from field selector patterns
+ let arg_grds = concat arg_grdss
+
+ -- tracePm "ConPatOut" (ppr x $$ ppr con $$ ppr arg_ids)
+ pure (con_grd : arg_grds)
+
+desugarPatBind :: SrcSpan -> Id -> Pat GhcTc -> DsM (PmPatBind Pre)
+-- See 'GrdPatBind' for how this simply repurposes GrdGRHS.
+desugarPatBind loc var pat =
+ PmPatBind . flip PmGRHS (SrcInfo (L loc (ppr pat))) . GrdVec <$> desugarPat var pat
+
+desugarEmptyCase :: Id -> DsM PmEmptyCase
+desugarEmptyCase var = pure PmEmptyCase { pe_var = var }
+
+-- | Desugar the non-empty 'Match'es of a 'MatchGroup'.
+desugarMatches :: [Id] -> NonEmpty (LMatch GhcTc (LHsExpr GhcTc))
+ -> DsM (PmMatchGroup Pre)
+desugarMatches vars matches =
+ PmMatchGroup <$> traverse (desugarMatch vars) matches
+
+-- Desugar a single match
+desugarMatch :: [Id] -> LMatch GhcTc (LHsExpr GhcTc) -> DsM (PmMatch Pre)
+desugarMatch vars (L match_loc (Match { m_pats = pats, m_grhss = grhss })) = do
+ pats' <- concat <$> zipWithM desugarLPat vars pats
+ grhss' <- desugarGRHSs match_loc (sep (map ppr pats)) grhss
+ -- tracePm "desugarMatch" (vcat [ppr pats, ppr pats', ppr grhss'])
+ return PmMatch { pm_pats = GrdVec pats', pm_grhss = grhss' }
+
+desugarGRHSs :: SrcSpan -> SDoc -> GRHSs GhcTc (LHsExpr GhcTc) -> DsM (NonEmpty (PmGRHS Pre))
+desugarGRHSs match_loc pp_pats grhss
+ = traverse (desugarLGRHS match_loc pp_pats)
+ . expectJust "desugarGRHSs"
+ . NE.nonEmpty
+ $ grhssGRHSs grhss
+
+-- | Desugar a guarded right-hand side to a single 'GrdTree'
+desugarLGRHS :: SrcSpan -> SDoc -> LGRHS GhcTc (LHsExpr GhcTc) -> DsM (PmGRHS Pre)
+desugarLGRHS match_loc pp_pats (L _loc (GRHS _ gs _)) = do
+ -- _loc points to the match separator (ie =, ->) that comes after the guards.
+ -- Hence we have to pass in the match_loc, which we use in case that the RHS
+ -- is unguarded.
+ -- pp_pats is the space-separated pattern of the current Match this
+ -- GRHS belongs to, so the @A B x@ part in @A B x | 0 <- x at .
+ let rhs_info = case gs of
+ [] -> L match_loc pp_pats
+ (L grd_loc _):_ -> L grd_loc (pp_pats <+> vbar <+> interpp'SP gs)
+ grds <- concatMapM (desugarGuard . unLoc) gs
+ pure PmGRHS { pg_grds = GrdVec grds, pg_rhs = SrcInfo rhs_info }
+
+-- | Desugar a guard statement to a '[PmGrd]'
+desugarGuard :: GuardStmt GhcTc -> DsM [PmGrd]
+desugarGuard guard = case guard of
+ BodyStmt _ e _ _ -> desugarBoolGuard e
+ LetStmt _ binds -> desugarLet (unLoc binds)
+ BindStmt _ p e -> desugarBind p e
+ LastStmt {} -> panic "desugarGuard LastStmt"
+ ParStmt {} -> panic "desugarGuard ParStmt"
+ TransStmt {} -> panic "desugarGuard TransStmt"
+ RecStmt {} -> panic "desugarGuard RecStmt"
+ ApplicativeStmt {} -> panic "desugarGuard ApplicativeLastStmt"
+
+-- | Desugar let-bindings
+desugarLet :: HsLocalBinds GhcTc -> DsM [PmGrd]
+desugarLet _binds = return []
+
+-- | Desugar a pattern guard
+-- @pat <- e ==> let x = e; <guards for pat <- x>@
+desugarBind :: LPat GhcTc -> LHsExpr GhcTc -> DsM [PmGrd]
+desugarBind p e = dsLExpr e >>= \case
+ Var y
+ | Nothing <- isDataConId_maybe y
+ -- RHS is a variable, so that will allow us to omit the let
+ -> desugarLPat y p
+ rhs -> do
+ (x, grds) <- desugarLPatV p
+ pure (PmLet x rhs : grds)
+
+-- | Desugar a boolean guard
+-- @e ==> let x = e; True <- x@
+desugarBoolGuard :: LHsExpr GhcTc -> DsM [PmGrd]
+desugarBoolGuard e
+ | isJust (isTrueLHsExpr e) = return []
+ -- The formal thing to do would be to generate (True <- True)
+ -- but it is trivial to solve so instead we give back an empty
+ -- [PmGrd] for efficiency
+ | otherwise = dsLExpr e >>= \case
+ Var y
+ | Nothing <- isDataConId_maybe y
+ -- Omit the let by matching on y
+ -> pure [vanillaConGrd y trueDataCon []]
+ rhs -> do
+ x <- mkPmId boolTy
+ pure [PmLet x rhs, vanillaConGrd x trueDataCon []]
+
+{- Note [Field match order for RecCon]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The order for RecCon field patterns actually determines evaluation order of
+the pattern match. For example:
+
+ data T = T { a :: Char, b :: Int }
+ f :: T -> ()
+ f T{ b = 42, a = 'a' } = ()
+
+Then @f (T (error "a") (error "b"))@ errors out with "b" because it is mentioned
+first in the pattern match.
+
+This means we can't just desugar the pattern match to
+@[T a b <- x, 'a' <- a, 42 <- b]@. Instead we have to force them in the
+right order: @[T a b <- x, 42 <- b, 'a' <- a]@.
+
+Note [Order of guards matters]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Similar to Note [Field match order for RecCon], the order in which the guards
+for a pattern match appear matter. Consider a situation similar to T5117:
+
+ f (0:_) = ()
+ f (0:[]) = ()
+
+The latter clause is clearly redundant. Yet if we desugar the second clause as
+
+ [x:xs' <- xs, [] <- xs', 0 <- x]
+
+We will say that the second clause only has an inaccessible RHS. That's because
+we force the tail of the list before comparing its head! So the correct
+translation would have been
+
+ [x:xs' <- xs, 0 <- x, [] <- xs']
+
+And we have to take in the guards on list cells into @mkListGrds at .
+
+Note [Desugar CoPats]
+~~~~~~~~~~~~~~~~~~~~~~~
+The pattern match checker did not know how to handle coerced patterns
+`CoPat` efficiently, which gave rise to #11276. The original approach
+desugared `CoPat`s:
+
+ pat |> co ===> x (pat <- (x |> co))
+
+Why did we do this seemingly unnecessary expansion in the first place?
+The reason is that the type of @pat |> co@ (which is the type of the value
+abstraction we match against) might be different than that of @pat at . Data
+instances such as @Sing (a :: Bool)@ are a good example of this: If we would
+just drop the coercion, we'd get a type error when matching @pat@ against its
+value abstraction, with the result being that pmIsSatisfiable decides that every
+possible data constructor fitting @pat@ is rejected as uninhabitated, leading to
+a lot of false warnings.
+
+But we can check whether the coercion is a hole or if it is just refl, in
+which case we can drop it.
+-}
=====================================
compiler/GHC/HsToCore/PmCheck/Ppr.hs → compiler/GHC/HsToCore/Pmc/Ppr.hs
=====================================
@@ -4,7 +4,7 @@
-- | Provides factilities for pretty-printing 'Nabla's in a way appropriate for
-- user facing pattern match warnings.
-module GHC.HsToCore.PmCheck.Ppr (
+module GHC.HsToCore.Pmc.Ppr (
pprUncovered
) where
@@ -26,8 +26,8 @@ import GHC.Utils.Misc
import GHC.Data.Maybe
import Data.List.NonEmpty (NonEmpty, nonEmpty, toList)
-import GHC.HsToCore.PmCheck.Types
-import GHC.HsToCore.PmCheck.Oracle
+import GHC.HsToCore.Pmc.Types
+import GHC.HsToCore.Pmc.Solver
-- | Pretty-print the guts of an uncovered value vector abstraction, i.e., its
-- components and refutable shapes associated to any mentioned variables.
@@ -93,25 +93,25 @@ Unhandled constraints that refer to HsExpr are typically ignored by the solver
(it does not even substitute in HsExpr so they are even printed as wildcards).
Additionally, the oracle returns a substitution if it succeeds so we apply this
substitution to the vectors before printing them out (see function `pprOne' in
-"GHC.HsToCore.PmCheck") to be more precise.
+"GHC.HsToCore.Pmc") to be more precise.
-}
-- | Extract and assigns pretty names to constraint variables with refutable
-- shapes.
-prettifyRefuts :: Nabla -> DIdEnv SDoc -> DIdEnv (SDoc, [PmAltCon])
+prettifyRefuts :: Nabla -> DIdEnv (Id, SDoc) -> DIdEnv (SDoc, [PmAltCon])
prettifyRefuts nabla = listToUDFM_Directly . map attach_refuts . udfmToList
where
- attach_refuts (u, sdoc) = (u, (sdoc, lookupRefuts nabla u))
+ attach_refuts (u, (x, sdoc)) = (u, (sdoc, lookupRefuts nabla x))
-type PmPprM a = RWS Nabla () (DIdEnv SDoc, [SDoc]) a
+type PmPprM a = RWS Nabla () (DIdEnv (Id, SDoc), [SDoc]) a
-- Try nice names p,q,r,s,t before using the (ugly) t_i
nameList :: [SDoc]
nameList = map text ["p","q","r","s","t"] ++
[ text ('t':show u) | u <- [(0 :: Int)..] ]
-runPmPpr :: Nabla -> PmPprM a -> (a, DIdEnv SDoc)
+runPmPpr :: Nabla -> PmPprM a -> (a, DIdEnv (Id, SDoc))
runPmPpr nabla m = case runRWS m nabla (emptyDVarEnv, nameList) of
(a, (renamings, _), _) -> (a, renamings)
@@ -122,9 +122,9 @@ getCleanName x = do
(renamings, name_supply) <- get
let (clean_name:name_supply') = name_supply
case lookupDVarEnv renamings x of
- Just nm -> pure nm
+ Just (_, nm) -> pure nm
Nothing -> do
- put (extendDVarEnv renamings x clean_name, name_supply')
+ put (extendDVarEnv renamings x (x, clean_name), name_supply')
pure clean_name
checkRefuts :: Id -> PmPprM (Maybe SDoc) -- the clean name if it has negative info attached
@@ -139,8 +139,8 @@ checkRefuts x = do
-- underscores. Even with a type signature, if it's not too noisy.
pprPmVar :: PprPrec -> Id -> PmPprM SDoc
-- Type signature is "too noisy" by my definition if it needs to parenthesize.
--- I like "not matched: _ :: Proxy (DIdEnv SDoc)",
--- but I don't like "not matched: (_ :: stuff) (_:_) (_ :: Proxy (DIdEnv SDoc))"
+-- I like "not matched: _ :: Proxy (DIdEnv (Id, SDoc))",
+-- but I don't like "not matched: (_ :: stuff) (_:_) (_ :: Proxy (DIdEnv (Id, SDoc)))"
-- The useful information in the latter case is the constructor that we missed,
-- not the types of the wildcards in the places that aren't matched as a result.
pprPmVar prec x = do
=====================================
compiler/GHC/HsToCore/PmCheck/Oracle.hs → compiler/GHC/HsToCore/Pmc/Solver.hs
=====================================
@@ -7,41 +7,47 @@ Authors: George Karachalias <george.karachalias at cs.kuleuven.be>
{-# LANGUAGE CPP, LambdaCase, TupleSections, PatternSynonyms, ViewPatterns,
MultiWayIf, ScopedTypeVariables, MagicHash #-}
--- | The pattern match oracle. The main export of the module are the functions
--- 'addPhiCts' for adding facts to the oracle, and 'generateInhabitingPatterns' to turn a
--- 'Nabla' into a concrete evidence for an equation.
+-- | Model refinements type as per the
+-- [Lower Your Guards paper](https://dl.acm.org/doi/abs/10.1145/3408989).
+-- The main export of the module are the functions 'addPhiCtsNablas' for adding
+-- facts to the oracle, 'isInhabited' to check if a refinement type is inhabited
+-- and 'generateInhabitingPatterns' to turn a 'Nabla' into a concrete pattern
+-- for an equation.
--
--- In terms of the [Lower Your Guards paper](https://dl.acm.org/doi/abs/10.1145/3408989)
--- describing the implementation, this module is concerned with Sections 3.4, 3.6 and 3.7.
--- E.g., it represents refinement types directly as a normalised refinement type 'Nabla'.
-module GHC.HsToCore.PmCheck.Oracle (
+-- In terms of the LYG paper, this module is concerned with Sections 3.4, 3.6
+-- and 3.7. E.g., it represents refinement types directly as a bunch of
+-- normalised refinement types 'Nabla'.
+module GHC.HsToCore.Pmc.Solver (
- DsM, tracePm, mkPmId,
- Nabla, initNablas, lookupRefuts, lookupSolution,
+ Nabla, Nablas(..), initNablas,
+ lookupRefuts, lookupSolution,
PhiCt(..), PhiCts,
+ addPhiCtNablas,
+ addPhiCtsNablas,
- addPhiCts, -- Add a constraint to the oracle.
+ isInhabited,
generateInhabitingPatterns
+
) where
#include "HsVersions.h"
import GHC.Prelude
-import GHC.HsToCore.PmCheck.Types
+import GHC.HsToCore.Pmc.Types
+import GHC.HsToCore.Pmc.Utils ( tracePm, mkPmId )
import GHC.Driver.Session
import GHC.Driver.Config
import GHC.Utils.Outputable
-import GHC.Utils.Error
+import GHC.Utils.Error ( pprErrMsgBagWithLoc )
import GHC.Utils.Misc
import GHC.Utils.Panic
import GHC.Data.Bag
-import GHC.Types.Unique
import GHC.Types.Unique.Set
import GHC.Types.Unique.DSet
-import GHC.Types.Unique.DFM
+import GHC.Types.Unique.SDFM
import GHC.Types.Id
import GHC.Types.Name
import GHC.Types.Var (EvVar)
@@ -68,7 +74,6 @@ import GHC.Core.Type
import GHC.Tc.Solver (tcNormalise, tcCheckSatisfiability)
import GHC.Core.Unify (tcMatchTy)
import GHC.Core.Coercion
-import GHC.Utils.Monad hiding (foldlM)
import GHC.HsToCore.Monad hiding (foldlM)
import GHC.Tc.Instance.Family
import GHC.Core.FamInstEnv
@@ -82,40 +87,32 @@ import Data.Foldable (foldlM, minimumBy, toList)
import Data.List (sortBy, find)
import qualified Data.List.NonEmpty as NE
import Data.Ord (comparing)
-import Data.Tuple (swap)
-
-import GHC.Driver.Ppr (pprTrace)
--- Debugging Infrastructure
-
-tracePm :: String -> SDoc -> DsM ()
-tracePm herald doc = do
- dflags <- getDynFlags
- printer <- mkPrintUnqualifiedDs
- liftIO $ dumpIfSet_dyn_printer printer dflags
- Opt_D_dump_ec_trace "" FormatText (text herald $$ (nest 2 doc))
-{-# INLINE tracePm #-} -- see Note [INLINE conditional tracing utilities]
+--
+-- * Main exports
+--
-debugOn :: () -> Bool
-debugOn _ = False
--- debugOn _ = True
+-- | Add a bunch of 'PhiCt's to all the 'Nabla's.
+-- Lifts 'addPhiCts' over many 'Nablas'.
+addPhiCtsNablas :: Nablas -> PhiCts -> DsM Nablas
+addPhiCtsNablas nablas cts = liftNablasM (\d -> addPhiCts d cts) nablas
-trc :: String -> SDoc -> a -> a
-trc | debugOn () = pprTrace
- | otherwise = \_ _ a -> a
+-- | 'addPmCtsNablas' for a single 'PmCt'.
+addPhiCtNablas :: Nablas -> PhiCt -> DsM Nablas
+addPhiCtNablas nablas ct = addPhiCtsNablas nablas (unitBag ct)
-_trcM :: Monad m => String -> SDoc -> m ()
-_trcM header doc = trc header doc (return ())
+liftNablasM :: Monad m => (Nabla -> m (Maybe Nabla)) -> Nablas -> m Nablas
+liftNablasM f (MkNablas ds) = MkNablas . catBagMaybes <$> (traverse f ds)
--- | Generate a fresh `Id` of a given type
-mkPmId :: Type -> DsM Id
-mkPmId ty = getUniqueM >>= \unique ->
- let occname = mkVarOccFS $ fsLit "pm"
- name = mkInternalName unique occname noSrcSpan
- in return (mkLocalIdOrCoVar name Many ty)
+-- | Test if any of the 'Nabla's is inhabited. Currently this is pure, because
+-- we preserve the invariant that there are no uninhabited 'Nabla's. But that
+-- could change in the future, for example by implementing this function in
+-- terms of @notNull <$> generateInhabitingPatterns 1 ds at .
+isInhabited :: Nablas -> DsM Bool
+isInhabited (MkNablas ds) = pure (not (null ds))
-----------------------------------------------
--- * Caching residual COMPLETE set
+-- * Caching residual COMPLETE sets
-- See Note [Implementation of COMPLETE pragmas]
@@ -195,7 +192,7 @@ also be defined in the module of the pragma) and do not impact recompilation
checking (#18675).
The pattern-match checker will then initialise each variable's 'VarInfo' with
-*all* imported COMPLETE sets (in 'GHC.HsToCore.PmCheck.Oracle.addCompleteMatches'),
+*all* imported COMPLETE sets (in 'GHC.HsToCore.Pmc.Solver.addCompleteMatches'),
well-typed or not, into a 'ResidualCompleteMatches'. The trick is that a
COMPLETE set that is ill-typed for that match variable could never be written by
the user! And we make sure not to report any ill-typed COMPLETE sets when
@@ -496,7 +493,7 @@ emptyVarInfo x
lookupVarInfo :: TmState -> Id -> VarInfo
-- (lookupVarInfo tms x) tells what we know about 'x'
-lookupVarInfo (TmSt env _ _) x = fromMaybe (emptyVarInfo x) (lookupSDIE env x)
+lookupVarInfo (TmSt env _ _) x = fromMaybe (emptyVarInfo x) (lookupUSDFM env 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
@@ -523,10 +520,7 @@ trvVarInfo f nabla at MkNabla{ nabla_tm_st = ts at TmSt{ts_facts = env} } x
= set_vi <$> f (lookupVarInfo ts x)
where
set_vi (a, vi') =
- (a, nabla{ nabla_tm_st = ts{ ts_facts = setEntrySDIE env (vi_id vi') vi' } })
-
-------------------------------------------------
--- * Exported utility functions querying 'Nabla'
+ (a, nabla{ nabla_tm_st = ts{ ts_facts = addToUSDFM env (vi_id vi') vi' } })
{- Note [Coverage checking Newtype matches]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -556,14 +550,14 @@ Handling of Newtypes is also described in the Appendix of the Lower Your Guards
where you can find the solution in a perhaps more digestible format.
-}
-lookupRefuts :: Uniquable k => Nabla -> k -> [PmAltCon]
+------------------------------------------------
+-- * 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 MkNabla{ nabla_tm_st = ts@(TmSt{ts_facts = (SDIE env)}) } k =
- case lookupUDFM_Directly env (getUnique k) of
- Nothing -> []
- Just (Indirect y) -> pmAltConSetElems (vi_neg (lookupVarInfo ts y))
- Just (Entry vi) -> pmAltConSetElems (vi_neg vi)
+lookupRefuts MkNabla{ nabla_tm_st = ts } x =
+ pmAltConSetElems $ vi_neg $ lookupVarInfo ts x
isDataConSolution :: PmAltConApp -> Bool
isDataConSolution PACA{paca_con = PmAltConLike (RealDataCon _)} = True
@@ -720,7 +714,7 @@ addBotCt nabla at MkNabla{ nabla_tm_st = ts at TmSt{ ts_facts=env } } x = do
IsBot -> pure nabla -- There already is x ~ ⊥. Nothing left to do
MaybeBot -> do -- We add x ~ ⊥
let vi' = vi{ vi_bot = IsBot }
- pure nabla{ nabla_tm_st = ts{ts_facts = setEntrySDIE env y vi' } }
+ pure nabla{ nabla_tm_st = ts{ts_facts = addToUSDFM env y vi' } }
-- | Adds the constraint @x ~/ ⊥@ to 'Nabla'. Quite similar to 'addNotConCt',
-- but only cares for the ⊥ "constructor".
@@ -734,7 +728,7 @@ addNotBotCt nabla at MkNabla{ nabla_tm_st = ts at TmSt{ts_facts=env} } x = do
-- Mark dirty for a delayed inhabitation test
let vi' = vi{ vi_bot = IsNotBot}
pure $ markDirty y
- $ nabla{ nabla_tm_st = ts{ ts_facts = setEntrySDIE env y vi' } }
+ $ nabla{ nabla_tm_st = ts{ ts_facts = addToUSDFM env y vi' } }
-- | Record a @x ~/ K@ constraint, e.g. that a particular 'Id' @x@ can't
-- take the shape of a 'PmAltCon' @K@ in the 'Nabla' and return @Nothing@ if
@@ -807,7 +801,7 @@ addConCt nabla at MkNabla{ nabla_tm_st = ts at TmSt{ ts_facts=env } } x alt tvs args =
Nothing -> do
let pos' = PACA alt tvs args : pos
let nabla_with bot' =
- nabla{ nabla_tm_st = ts{ts_facts = setEntrySDIE env x (vi{vi_pos = pos', vi_bot = bot'})} }
+ nabla{ nabla_tm_st = ts{ts_facts = addToUSDFM env x (vi{vi_pos = pos', vi_bot = bot'})} }
-- Do (2) in Note [Coverage checking Newtype matches]
case (alt, args) of
(PmAltConLike (RealDataCon dc), [y]) | isNewDataCon dc ->
@@ -827,55 +821,27 @@ equateTys ts us =
, not (eqType t u)
]
--- | Adds a @x ~ y@ constraint by trying to unify two 'Id's and record the
+-- | Adds a @x ~ y@ constraint by merging the two 'VarInfo's and record the
-- gained knowledge in 'Nabla'.
--
--- Returns @Nothing@ when there's a contradiction. Returns @Just nabla@
--- when the constraint was compatible with prior facts, in which case @nabla@
--- has integrated the knowledge from the equality constraint.
+-- Returns @Nothing@ when there's a contradiction while merging. Returns @Just
+-- nabla@ when the constraint was compatible with prior facts, in which case
+-- @nabla@ has integrated the knowledge from the equality constraint.
--
-- See Note [TmState invariants].
addVarCt :: Nabla -> Id -> Id -> MaybeT DsM Nabla
-addVarCt nabla at MkNabla{ nabla_tm_st = TmSt{ ts_facts = env } } x y
- -- It's important that we never @equate@ two variables of the same equivalence
- -- class, otherwise we might get cyclic substitutions.
- -- Cf. 'extendSubstAndSolve' and
- -- @testsuite/tests/pmcheck/should_compile/CyclicSubst.hs at .
- | sameRepresentativeSDIE env x y = pure nabla
- | otherwise = equate nabla x y
-
--- | @equate ts@(TmSt env) x y@ merges the equivalence classes of @x@ and @y@ by
--- adding an indirection to the environment.
--- Makes sure that the positive and negative facts of @x@ and @y@ are
--- compatible.
--- Preconditions: @not (sameRepresentativeSDIE env x y)@
---
--- See Note [TmState invariants].
-equate :: Nabla -> Id -> Id -> MaybeT DsM Nabla
-equate nabla at MkNabla{ nabla_tm_st = ts at TmSt{ts_facts = env} } x y
- = ASSERT( not (sameRepresentativeSDIE env x y) )
- case (lookupSDIE env x, lookupSDIE env y) of
- (Nothing, _) -> pure (nabla{ nabla_tm_st = ts{ ts_facts = setIndirectSDIE env x y } })
- (_, Nothing) -> pure (nabla{ nabla_tm_st = ts{ ts_facts = setIndirectSDIE env y x } })
- -- Merge the info we have for x into the info for y
- (Just vi_x, Just vi_y) -> do
- -- This assert will probably trigger at some point...
- -- We should decide how to break the tie
- MASSERT2( idType (vi_id vi_x) `eqType` idType (vi_id vi_y), text "Not same type" )
- -- First assume that x and y are in the same equivalence class
- let env_ind = setIndirectSDIE env x y
- -- Then sum up the refinement counters
- let env_refs = setEntrySDIE env_ind y vi_y
- let nabla_refs = nabla{ nabla_tm_st = ts{ts_facts = env_refs} }
- -- and then gradually merge every positive fact we have on x into y
- let add_fact nabla (PACA cl tvs args) = addConCt nabla y cl tvs args
- nabla_pos <- foldlM add_fact nabla_refs (vi_pos vi_x)
- -- Do the same for negative info
- let add_refut nabla nalt = addNotConCt nabla y nalt
- nabla_neg <- foldlM add_refut nabla_pos (pmAltConSetElems (vi_neg vi_x))
- -- vi_rcm will be updated in addNotConCt, so we are good to
- -- go!
- pure nabla_neg
+addVarCt nabla at MkNabla{ nabla_tm_st = ts at TmSt{ ts_facts = env } } x y =
+ case equateUSDFM env x y of
+ (Nothing, env') -> pure (nabla{ nabla_tm_st = ts{ ts_facts = env' } })
+ -- Add the constraints we had for x to y
+ (Just vi_x, env') -> do
+ let nabla_equated = nabla{ nabla_tm_st = ts{ts_facts = env'} }
+ -- and then gradually merge every positive fact we have on x into y
+ let add_pos nabla (PACA cl tvs args) = addConCt nabla y cl tvs args
+ nabla_pos <- foldlM add_pos nabla_equated (vi_pos vi_x)
+ -- Do the same for negative info
+ let add_neg nabla nalt = addNotConCt nabla y nalt
+ foldlM add_neg nabla_pos (pmAltConSetElems (vi_neg vi_x))
-- | Inspects a 'PmCoreCt' @let x = e@ by recording constraints for @x@ based
-- on the shape of the 'CoreExpr' @e at . Examples:
@@ -943,7 +909,7 @@ addCoreCt nabla x e = do
-- @x ~ y at .
equate_with_similar_expr :: Id -> CoreExpr -> StateT Nabla (MaybeT DsM) ()
equate_with_similar_expr x e = do
- rep <- StateT $ \nabla -> swap <$> lift (representCoreExpr nabla e)
+ rep <- StateT $ \nabla -> lift (representCoreExpr nabla e)
-- Note that @rep == x@ if we encountered @e@ for the first time.
modifyT (\nabla -> addVarCt nabla x rep)
@@ -996,14 +962,14 @@ addCoreCt nabla x e = do
-- Which is the @x@ of a @let x = e'@ constraint (with @e@ semantically
-- equivalent to @e'@) we encountered earlier, or a fresh identifier if
-- there weren't any such constraints.
-representCoreExpr :: Nabla -> CoreExpr -> DsM (Nabla, Id)
+representCoreExpr :: Nabla -> CoreExpr -> DsM (Id, Nabla)
representCoreExpr nabla at MkNabla{ nabla_tm_st = ts at TmSt{ ts_reps = reps } } e
- | Just rep <- lookupCoreMap reps e = pure (nabla, rep)
+ | Just rep <- lookupCoreMap reps e = pure (rep, nabla)
| otherwise = do
rep <- mkPmId (exprType e)
let reps' = extendCoreMap reps e rep
let nabla' = nabla{ nabla_tm_st = ts{ ts_reps = reps' } }
- pure (nabla', rep)
+ pure (rep, nabla')
-- | Like 'modify', but with an effectful modifier action
modifyT :: Monad m => (s -> m s) -> StateT s m ()
@@ -1159,9 +1125,9 @@ Note [Strict fields and variables of unlifted type]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Binders of unlifted type (and strict fields) are unlifted by construction;
they are conceived with an implicit @≁⊥@ constraint to begin with. Hence,
-desugaring in "GHC.HsToCore.PmCheck" is entirely unconcerned by strict fields,
+desugaring in "GHC.HsToCore.Pmc" is entirely unconcerned by strict fields,
since the forcing happens *before* pattern matching.
-And the φ constructor constraints emitted by 'GHC.HsToCore.PmCheck.checkGrd'
+And the φ constructor constraints emitted by 'GHC.HsToCore.Pmc.checkGrd'
have complex binding semantics (binding type constraints and unlifted fields),
so unliftedness semantics are entirely confined to the oracle.
@@ -1223,11 +1189,11 @@ traverseDirty f ts at TmSt{ts_facts = env, ts_dirty = dirty} =
go [] env = pure ts{ts_facts=env}
go (x:xs) !env = do
vi' <- f (lookupVarInfo ts x)
- go xs (setEntrySDIE env x vi')
+ go xs (addToUSDFM env x vi')
traverseAll :: Monad m => (VarInfo -> m VarInfo) -> TmState -> m TmState
traverseAll f ts at TmSt{ts_facts = env} = do
- env' <- traverseSDIE f env
+ env' <- traverseUSDFM f env
pure ts{ts_facts = env'}
-- | Makes sure the given 'Nabla' is still inhabited, by trying to instantiate
=====================================
compiler/GHC/HsToCore/PmCheck/Types.hs → compiler/GHC/HsToCore/Pmc/Solver/Types.hs
=====================================
@@ -1,43 +1,37 @@
-{-
-Author: George Karachalias <george.karachalias at cs.kuleuven.be>
- Sebastian Graf <sgraf1337 at gmail.com>
--}
-
{-# LANGUAGE CPP #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ApplicativeDo #-}
--- | Types used through-out pattern match checking. This module is mostly there
--- to be imported from "GHC.Tc.Types". The exposed API is that of
--- "GHC.HsToCore.PmCheck.Oracle" and "GHC.HsToCore.PmCheck".
-module GHC.HsToCore.PmCheck.Types (
- -- * Representations for Literals and AltCons
- PmLit(..), PmLitValue(..), PmAltCon(..), pmLitType, pmAltConType,
- isPmAltConMatchStrict, pmAltConImplBangs,
+-- | 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 (
- -- ** Equality on 'PmAltCon's
- PmEquality(..), eqPmAltCon,
-
- -- ** Operations on 'PmLit'
- literalToPmLit, negatePmLit, overloadPmLit,
- pmLitAsStringLit, coreExprAsPmLit,
+ -- * Normalised refinement types
+ BotInfo(..), PmAltConApp(..), VarInfo(..), TmState(..), TyState(..),
+ Nabla(..), Nablas(..), initNablas,
- -- * Caching residual COMPLETE sets
+ -- ** Caching residual COMPLETE sets
ConLikeSet, ResidualCompleteMatches(..), getRcm, isRcmInitialised,
- -- * PmAltConSet
+ -- ** Representations for Literals and AltCons
+ PmLit(..), PmLitValue(..), PmAltCon(..), pmLitType, pmAltConType,
+ isPmAltConMatchStrict, pmAltConImplBangs,
+
+ -- *** PmAltConSet
PmAltConSet, emptyPmAltConSet, isEmptyPmAltConSet, elemPmAltConSet,
extendPmAltConSet, pmAltConSetElems,
- -- * A 'DIdEnv' where entries may be shared
- Shared(..), SharedDIdEnv(..), emptySDIE, lookupSDIE, sameRepresentativeSDIE,
- setIndirectSDIE, setEntrySDIE, traverseSDIE, entriesSDIE,
+ -- *** Equality on 'PmAltCon's
+ PmEquality(..), eqPmAltCon,
+
+ -- *** Operations on 'PmLit'
+ literalToPmLit, negatePmLit, overloadPmLit,
+ pmLitAsStringLit, coreExprAsPmLit
- -- * The pattern match oracle
- BotInfo(..), PmAltConApp(..), VarInfo(..), TmState(..), TyState(..),
- Nabla(..), Nablas(..), initNablas, liftNablasM
) where
#include "HsVersions.h"
@@ -48,10 +42,9 @@ import GHC.Utils.Misc
import GHC.Data.Bag
import GHC.Data.FastString
import GHC.Types.Id
-import GHC.Types.Var.Env
import GHC.Types.Var.Set
import GHC.Types.Unique.DSet
-import GHC.Types.Unique.DFM
+import GHC.Types.Unique.SDFM
import GHC.Types.Name
import GHC.Core.DataCon
import GHC.Core.ConLike
@@ -76,6 +69,216 @@ import Data.Foldable (find)
import Data.Ratio
import qualified Data.Semigroup as Semi
+--
+-- * 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_ty_st :: !TyState
+ -- ^ Type oracle; things like a~Int
+ , nabla_tm_st :: !TmState
+ -- ^ Term oracle; things like x~Nothing
+ }
+
+-- | An initial nabla that is always satisfiable
+initNabla :: Nabla
+initNabla = MkNabla initTyState initTmState
+
+instance Outputable Nabla where
+ ppr nabla = hang (text "Nabla") 2 $ vcat [
+ -- intentionally formatted this way enable the dev to comment in only
+ -- the info she needs
+ ppr (nabla_tm_st nabla),
+ ppr (nabla_ty_st nabla)
+ ]
+
+-- | A disjunctive bag of 'Nabla's, representing a refinement type.
+newtype Nablas = MkNablas (Bag Nabla)
+
+initNablas :: Nablas
+initNablas = MkNablas (unitBag initNabla)
+
+instance Outputable Nablas where
+ ppr (MkNablas nablas) = ppr nablas
+
+instance Semigroup Nablas where
+ MkNablas l <> MkNablas r = MkNablas (l `unionBags` r)
+
+instance Monoid Nablas where
+ mempty = MkNablas 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 { ty_st_n :: !Int, ty_st_inert :: !InertSet }
+
+-- | Not user-facing.
+instance Outputable TyState where
+ ppr (TySt n inert) = ppr n <+> ppr inert
+
+initTyState :: TyState
+initTyState = TySt 0 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
+ { ts_facts :: !(UniqSDFM Id VarInfo)
+ -- ^ Facts about term variables. Deterministic env, so that we generate
+ -- deterministic error messages.
+ , 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.
+ , 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
+ { 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.
+
+ , 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.
+
+ , 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 at . 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.
+
+ , 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 ≁ ⊥@
+
+ , 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
+ { paca_con :: !PmAltCon
+ , paca_tvs :: ![TyVar]
+ , paca_ids :: ![Id]
+ }
+
+-- | See 'vi_bot'.
+data BotInfo
+ = IsBot
+ | IsNotBot
+ | MaybeBot
+ deriving Eq
+
+instance Outputable PmAltConApp where
+ ppr PACA{paca_con = con, paca_tvs = tvs, paca_ids = ids} =
+ hsep (ppr con : map ((char '@' <>) . ppr) tvs ++ map ppr ids)
+
+instance Outputable BotInfo where
+ ppr MaybeBot = underscore
+ ppr IsBot = text "~⊥"
+ ppr IsNotBot = text "≁⊥"
+
+-- | Not user-facing.
+instance Outputable TmState where
+ ppr (TmSt state reps dirty) = ppr state $$ ppr reps $$ ppr dirty
+
+-- | Not user-facing.
+instance Outputable VarInfo where
+ ppr (VI x pos neg bot cache)
+ = braces (hcat (punctuate comma [pp_x, pp_pos, pp_neg, ppr bot, pp_cache]))
+ where
+ pp_x = ppr x <> dcolon <> ppr (idType x)
+ pp_pos
+ | [] <- pos = underscore
+ | [p] <- pos = char '~' <> ppr p -- suppress outer [_] if singleton
+ | otherwise = char '~' <> ppr pos
+ pp_neg
+ | isEmptyPmAltConSet neg = underscore
+ | otherwise = char '≁' <> ppr neg
+ pp_cache
+ | RCM Nothing Nothing <- cache = underscore
+ | otherwise = ppr cache
+
+-- | Initial state of the term oracle.
+initTmState :: TmState
+initTmState = TmSt emptyUSDFM emptyCoreMap 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
+ { rcm_vanilla :: !(Maybe ConLikeSet)
+ -- ^ 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'.
+ , rcm_pragmas :: !(Maybe [ConLikeSet])
+ -- ^ 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 -> [ConLikeSet]
+getRcm (RCM vanilla pragmas) = maybeToList vanilla ++ fromMaybe [] pragmas
+
+isRcmInitialised :: ResidualCompleteMatches -> Bool
+isRcmInitialised (RCM vanilla pragmas) = isJust vanilla && isJust pragmas
+
+instance Outputable ResidualCompleteMatches where
+ -- formats as "[{Nothing,Just},{P,Q}]"
+ ppr rcm = ppr (getRcm rcm)
+
+--------------------------------------------------------------------------------
+-- 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]
@@ -230,7 +433,7 @@ pmAltConType (PmAltConLike con) arg_tys = conLikeResTy con 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.PmCheck.Oracle".
+-- See Note [Coverage checking Newtype matches] in "GHC.HsToCore.Pmc.Solver".
isPmAltConMatchStrict :: PmAltCon -> Bool
isPmAltConMatchStrict PmAltLit{} = True
isPmAltConMatchStrict (PmAltConLike PatSynCon{}) = True -- #17357
@@ -288,7 +491,7 @@ The impact of this treatment of overloaded literals is the following:
* 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.PmCheck" and effectively addresses
+ `uncovered` and `divergent` in "GHC.HsToCore.Pmc" and effectively addresses
#11161.
* The warnings issued are simpler.
@@ -347,23 +550,22 @@ coreExprAsPmLit e = case collectArgs e of
-- overloaded lits anyway, so we immediately override type information
-> literalToPmLit (exprType e) (mkLitDouble (litValue n % litValue d))
(Var x, args)
- -- Take care of -XRebindableSyntax. The last argument should be the (only)
- -- integer literal, otherwise we can't really do much about it.
- | [Lit l] <- dropWhile (not . is_lit) args
- , is_rebound_name x fromIntegerName
+ -- See Note [Detecting overloaded literals with -XRebindableSyntax]
+ | is_rebound_name x fromIntegerName
+ , [Lit l] <- dropWhile (not . is_lit) args
-> literalToPmLit (literalType l) l >>= overloadPmLit (exprType e)
(Var x, args)
- -- Similar to fromInteger case
- | [r] <- dropWhile (not . is_ratio) args
- , is_rebound_name x fromRationalName
+ -- See Note [Detecting overloaded literals with -XRebindableSyntax]
+ | is_rebound_name x fromRationalName
+ , [r] <- dropWhile (not . is_ratio) args
-> coreExprAsPmLit r >>= overloadPmLit (exprType e)
(Var x, args)
| is_rebound_name x fromStringName
- -- With -XRebindableSyntax or without: The first String argument is what we are after
+ -- See Note [Detecting overloaded literals with -XRebindableSyntax]
, s:_ <- filter (eqType stringTy . exprType) args
-- NB: Calls coreExprAsPmLit and then overloadPmLit, so that we return PmLitOverStrings
-> coreExprAsPmLit s >>= overloadPmLit (exprType e)
- -- These last two cases handle String literals
+ -- These last two cases handle proper String literals
(Var x, [Type ty])
| Just dc <- isDataConWorkId_maybe x
, dc == nilDataCon
@@ -383,11 +585,25 @@ coreExprAsPmLit e = case collectArgs e of
| otherwise
= False
- -- | Compares the given Id to the Name based on OccName, to detect
- -- -XRebindableSyntax.
+ -- See Note [Detecting overloaded literals with -XRebindableSyntax]
is_rebound_name :: Id -> Name -> Bool
is_rebound_name x n = getOccFS (idName x) == getOccFS 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`).
+-}
+
instance Outputable PmLitValue where
ppr (PmLitInt i) = ppr i
ppr (PmLitRat r) = ppr (double (fromRat r)) -- good enough
@@ -420,271 +636,3 @@ instance Outputable PmAltCon where
instance Outputable PmEquality where
ppr = text . show
-
--- | 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
- { rcm_vanilla :: !(Maybe ConLikeSet)
- -- ^ 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'.
- , rcm_pragmas :: !(Maybe [ConLikeSet])
- -- ^ 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 -> [ConLikeSet]
-getRcm (RCM vanilla pragmas) = maybeToList vanilla ++ fromMaybe [] pragmas
-
-isRcmInitialised :: ResidualCompleteMatches -> Bool
-isRcmInitialised (RCM vanilla pragmas) = isJust vanilla && isJust pragmas
-
-instance Outputable ResidualCompleteMatches where
- -- formats as "[{Nothing,Just},{P,Q}]"
- ppr rcm = ppr (getRcm rcm)
-
--- | Either @Indirect x@, meaning the value is represented by that of @x@, or
--- an @Entry@ containing containing the actual value it represents.
-data Shared a
- = Indirect Id
- | Entry a
-
--- | A 'DIdEnv' in which entries can be shared by multiple 'Id's.
--- Merge equivalence classes of two Ids by 'setIndirectSDIE' and set the entry
--- of an Id with 'setEntrySDIE'.
-newtype SharedDIdEnv a
- = SDIE { unSDIE :: DIdEnv (Shared a) }
-
-emptySDIE :: SharedDIdEnv a
-emptySDIE = SDIE emptyDVarEnv
-
-lookupReprAndEntrySDIE :: SharedDIdEnv a -> Id -> (Id, Maybe a)
-lookupReprAndEntrySDIE sdie@(SDIE env) x = case lookupDVarEnv env x of
- Nothing -> (x, Nothing)
- Just (Indirect y) -> lookupReprAndEntrySDIE sdie y
- Just (Entry a) -> (x, Just a)
-
--- | @lookupSDIE env x@ looks up an entry for @x@, looking through all
--- 'Indirect's until it finds a shared 'Entry'.
-lookupSDIE :: SharedDIdEnv a -> Id -> Maybe a
-lookupSDIE sdie x = snd (lookupReprAndEntrySDIE sdie x)
-
--- | Check if two variables are part of the same equivalence class.
-sameRepresentativeSDIE :: SharedDIdEnv a -> Id -> Id -> Bool
-sameRepresentativeSDIE sdie x y =
- fst (lookupReprAndEntrySDIE sdie x) == fst (lookupReprAndEntrySDIE sdie y)
-
--- | @setIndirectSDIE env x y@ sets @x@'s 'Entry' to @Indirect y@, thereby
--- merging @x@'s equivalence class into @y@'s. This will discard all info on
--- @x@!
-setIndirectSDIE :: SharedDIdEnv a -> Id -> Id -> SharedDIdEnv a
-setIndirectSDIE sdie@(SDIE env) x y =
- SDIE $ extendDVarEnv env (fst (lookupReprAndEntrySDIE sdie x)) (Indirect y)
-
--- | @setEntrySDIE env x a@ sets the 'Entry' @x@ is associated with to @a@,
--- thereby modifying its whole equivalence class.
-setEntrySDIE :: SharedDIdEnv a -> Id -> a -> SharedDIdEnv a
-setEntrySDIE sdie@(SDIE env) x a =
- SDIE $ extendDVarEnv env (fst (lookupReprAndEntrySDIE sdie x)) (Entry a)
-
-entriesSDIE :: SharedDIdEnv a -> [a]
-entriesSDIE (SDIE env) = mapMaybe preview_entry (eltsUDFM env)
- where
- preview_entry (Entry e) = Just e
- preview_entry _ = Nothing
-
-traverseSDIE :: forall a b f. Applicative f => (a -> f b) -> SharedDIdEnv a -> f (SharedDIdEnv b)
-traverseSDIE f = fmap (SDIE . listToUDFM_Directly) . traverse g . udfmToList . unSDIE
- where
- g :: (Unique, Shared a) -> f (Unique, Shared b)
- g (u, Indirect y) = pure (u,Indirect y)
- g (u, Entry a) = do
- a' <- f a
- pure (u,Entry a')
-
-instance Outputable a => Outputable (Shared a) where
- ppr (Indirect x) = ppr x
- ppr (Entry a) = ppr a
-
-instance Outputable a => Outputable (SharedDIdEnv a) where
- ppr (SDIE env) = ppr env
-
--- | 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.PmCheck.Oracle".
-data TmState
- = TmSt
- { ts_facts :: !(SharedDIdEnv VarInfo)
- -- ^ Facts about term variables. Deterministic env, so that we generate
- -- deterministic error messages.
- , 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.
- , 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.PmCheck.Oracle".
-data VarInfo
- = VI
- { 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.
-
- , 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.
-
- , 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 at . 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.
-
- , 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 ≁ ⊥@
-
- , 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
- { paca_con :: !PmAltCon
- , paca_tvs :: ![TyVar]
- , paca_ids :: ![Id]
- }
-
--- | See 'vi_bot'.
-data BotInfo
- = IsBot
- | IsNotBot
- | MaybeBot
- deriving Eq
-
-instance Outputable PmAltConApp where
- ppr PACA{paca_con = con, paca_tvs = tvs, paca_ids = ids} =
- hsep (ppr con : map ((char '@' <>) . ppr) tvs ++ map ppr ids)
-
-instance Outputable BotInfo where
- ppr MaybeBot = underscore
- ppr IsBot = text "~⊥"
- ppr IsNotBot = text "≁⊥"
-
--- | Not user-facing.
-instance Outputable TmState where
- ppr (TmSt state reps dirty) = ppr state $$ ppr reps $$ ppr dirty
-
--- | Not user-facing.
-instance Outputable VarInfo where
- ppr (VI x pos neg bot cache)
- = braces (hcat (punctuate comma [pp_x, pp_pos, pp_neg, ppr bot, pp_cache]))
- where
- pp_x = ppr x <> dcolon <> ppr (idType x)
- pp_pos
- | [] <- pos = underscore
- | [p] <- pos = char '~' <> ppr p -- suppress outer [_] if singleton
- | otherwise = char '~' <> ppr pos
- pp_neg
- | isEmptyPmAltConSet neg = underscore
- | otherwise = char '≁' <> ppr neg
- pp_cache
- | RCM Nothing Nothing <- cache = underscore
- | otherwise = ppr cache
-
--- | Initial state of the term oracle.
-initTmState :: TmState
-initTmState = TmSt emptySDIE emptyCoreMap emptyDVarSet
-
--- | The type oracle state. An 'GHC.Tc.Solver.Monad.InsertSet' 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 { ty_st_n :: !Int, ty_st_inert :: !InertSet }
-
--- | Not user-facing.
-instance Outputable TyState where
- ppr (TySt n inert) = ppr n <+> ppr inert
-
-initTyState :: TyState
-initTyState = TySt 0 emptyInert
-
--- | 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_ty_st :: !TyState
- -- ^ Type oracle; things like a~Int
- , nabla_tm_st :: !TmState
- -- ^ Term oracle; things like x~Nothing
- }
-
--- | An initial nabla that is always satisfiable
-initNabla :: Nabla
-initNabla = MkNabla initTyState initTmState
-
-instance Outputable Nabla where
- ppr nabla = hang (text "Nabla") 2 $ vcat [
- -- intentionally formatted this way enable the dev to comment in only
- -- the info she needs
- ppr (nabla_tm_st nabla),
- ppr (nabla_ty_st nabla)
- ]
-
--- | A disjunctive bag of 'Nabla's, representing a refinement type.
-newtype Nablas = MkNablas (Bag Nabla)
-
-initNablas :: Nablas
-initNablas = MkNablas (unitBag initNabla)
-
-instance Outputable Nablas where
- ppr (MkNablas nablas) = ppr nablas
-
-instance Semigroup Nablas where
- MkNablas l <> MkNablas r = MkNablas (l `unionBags` r)
-
-instance Monoid Nablas where
- mempty = MkNablas emptyBag
-
-liftNablasM :: Monad m => (Nabla -> m (Maybe Nabla)) -> Nablas -> m Nablas
-liftNablasM f (MkNablas ds) = MkNablas . catBagMaybes <$> (traverse f ds)
=====================================
compiler/GHC/HsToCore/Pmc/Types.hs
=====================================
@@ -0,0 +1,231 @@
+{-
+Author: George Karachalias <george.karachalias at cs.kuleuven.be>
+ Sebastian Graf <sgraf1337 at gmail.com>
+-}
+
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE DeriveFunctor #-}
+
+-- | Types used through-out pattern match checking. This module is mostly there
+-- to be imported from "GHC.HsToCore.Types". The exposed API is that of
+-- "GHC.HsToCore.Pmc".
+--
+-- These types model the paper
+-- [Lower Your Guards: A Compositional Pattern-Match Coverage Checker"](https://dl.acm.org/doi/abs/10.1145/3408989).
+module GHC.HsToCore.Pmc.Types (
+ -- * LYG syntax
+
+ -- ** Guard language
+ SrcInfo(..), PmGrd(..), GrdVec(..),
+
+ -- ** Guard tree language
+ PmMatchGroup(..), PmMatch(..), PmGRHS(..), PmPatBind(..), PmEmptyCase(..),
+
+ -- * Coverage Checking types
+ RedSets (..), Precision (..), CheckResult (..),
+
+ -- * Pre and post coverage checking synonyms
+ Pre, Post,
+
+ -- * Normalised refinement types
+ module GHC.HsToCore.Pmc.Solver.Types
+
+ ) where
+
+#include "HsVersions.h"
+
+import GHC.Prelude
+
+import GHC.HsToCore.Pmc.Solver.Types
+
+import GHC.Data.OrdList
+import GHC.Types.Id
+import GHC.Types.Var (EvVar)
+import GHC.Types.SrcLoc
+import GHC.Utils.Outputable
+import GHC.Core.Type
+import GHC.Core
+
+import Data.List.NonEmpty ( NonEmpty(..) )
+import qualified Data.List.NonEmpty as NE
+import qualified Data.Semigroup as Semi
+
+--
+-- * Guard language
+--
+
+-- | A very simple language for pattern guards. Let bindings, bang patterns,
+-- and matching variables against flat constructor patterns.
+-- The LYG guard language.
+data PmGrd
+ = -- | @PmCon x K dicts args@ corresponds to a @K dicts args <- x@ guard.
+ -- The @args@ are bound in this construct, the @x@ is just a use.
+ -- For the arguments' meaning see 'GHC.Hs.Pat.ConPatOut'.
+ PmCon {
+ pm_id :: !Id,
+ pm_con_con :: !PmAltCon,
+ pm_con_tvs :: ![TyVar],
+ pm_con_dicts :: ![EvVar],
+ pm_con_args :: ![Id]
+ }
+
+ -- | @PmBang x@ corresponds to a @seq x True@ guard.
+ -- If the extra 'SrcInfo' is present, the bang guard came from a source
+ -- bang pattern, in which case we might want to report it as redundant.
+ -- See Note [Dead bang patterns] in GHC.HsToCore.Pmc.Check.
+ | PmBang {
+ pm_id :: !Id,
+ _pm_loc :: !(Maybe SrcInfo)
+ }
+
+ -- | @PmLet x expr@ corresponds to a @let x = expr@ guard. This actually
+ -- /binds/ @x at .
+ | PmLet {
+ pm_id :: !Id,
+ _pm_let_expr :: !CoreExpr
+ }
+
+-- | Should not be user-facing.
+instance Outputable PmGrd where
+ ppr (PmCon x alt _tvs _con_dicts con_args)
+ = hsep [ppr alt, hsep (map ppr con_args), text "<-", ppr x]
+ ppr (PmBang x _loc) = char '!' <> ppr x
+ ppr (PmLet x expr) = hsep [text "let", ppr x, text "=", ppr expr]
+
+--
+-- * Guard tree language
+--
+
+-- | Means by which we identify a source construct for later pretty-printing in
+-- a warning message. 'SDoc' for the equation to show, 'Located' for the
+-- location.
+newtype SrcInfo = SrcInfo (Located SDoc)
+
+-- | A sequence of 'PmGrd's.
+newtype GrdVec = GrdVec [PmGrd]
+
+-- | A guard tree denoting 'MatchGroup'.
+newtype PmMatchGroup p = PmMatchGroup (NonEmpty (PmMatch p))
+
+-- | A guard tree denoting 'Match': A payload describing the pats and a bunch of
+-- GRHS.
+data PmMatch p = PmMatch { pm_pats :: !p, pm_grhss :: !(NonEmpty (PmGRHS p)) }
+
+-- | A guard tree denoting 'GRHS': A payload describing the grds and a 'SrcInfo'
+-- useful for printing out in warnings messages.
+data PmGRHS p = PmGRHS { pg_grds :: !p, pg_rhs :: !SrcInfo }
+
+-- | A guard tree denoting an -XEmptyCase.
+newtype PmEmptyCase = PmEmptyCase { pe_var :: Id }
+
+-- | A guard tree denoting a pattern binding.
+newtype PmPatBind p =
+ -- just reuse GrdGRHS and pretend its @SrcInfo@ is info on the /pattern/,
+ -- rather than on the pattern bindings.
+ PmPatBind (PmGRHS p)
+
+instance Outputable SrcInfo where
+ ppr (SrcInfo (L (RealSrcSpan rss _) _)) = ppr (srcSpanStartLine rss)
+ ppr (SrcInfo (L s _)) = ppr s
+
+-- | Format LYG guards as @| True <- x, let x = 42, !z@
+instance Outputable GrdVec where
+ ppr (GrdVec []) = empty
+ ppr (GrdVec (g:gs)) = fsep (char '|' <+> ppr g : map ((comma <+>) . ppr) gs)
+
+-- | Format a LYG sequence (e.g. 'Match'es of a 'MatchGroup' or 'GRHSs') as
+-- @{ <first alt>; ...; <last alt> }@
+pprLygSequence :: Outputable a => NonEmpty a -> SDoc
+pprLygSequence (NE.toList -> as) =
+ braces (space <> fsep (punctuate semi (map ppr as)) <> space)
+
+instance Outputable p => Outputable (PmMatchGroup p) where
+ ppr (PmMatchGroup matches) = pprLygSequence matches
+
+instance Outputable p => Outputable (PmMatch p) where
+ ppr (PmMatch { pm_pats = grds, pm_grhss = grhss }) =
+ ppr grds <+> ppr grhss
+
+instance Outputable p => Outputable (PmGRHS p) where
+ ppr (PmGRHS { pg_grds = grds, pg_rhs = rhs }) =
+ ppr grds <+> text "->" <+> ppr rhs
+
+instance Outputable p => Outputable (PmPatBind p) where
+ ppr (PmPatBind PmGRHS { pg_grds = grds, pg_rhs = bind }) =
+ ppr bind <+> ppr grds <+> text "=" <+> text "..."
+
+instance Outputable PmEmptyCase where
+ ppr (PmEmptyCase { pe_var = var }) =
+ text "<empty case on " <> ppr var <> text ">"
+
+data Precision = Approximate | Precise
+ deriving (Eq, Show)
+
+instance Outputable Precision where
+ ppr = text . show
+
+instance Semi.Semigroup Precision where
+ Precise <> Precise = Precise
+ _ <> _ = Approximate
+
+instance Monoid Precision where
+ mempty = Precise
+ mappend = (Semi.<>)
+
+-- | Redundancy sets, used to determine redundancy of RHSs and bang patterns
+-- (later digested into a 'CIRB').
+data RedSets
+ = RedSets
+ { rs_cov :: !Nablas
+ -- ^ The /Covered/ set; the set of values reaching a particular program
+ -- point.
+ , rs_div :: !Nablas
+ -- ^ The /Diverging/ set; empty if no match can lead to divergence.
+ -- If it wasn't empty, we have to turn redundancy warnings into
+ -- inaccessibility warnings for any subclauses.
+ , rs_bangs :: !(OrdList (Nablas, SrcInfo))
+ -- ^ If any of the 'Nablas' is empty, the corresponding 'SrcInfo' pin-points
+ -- a bang pattern in source that is redundant. See Note [Dead bang patterns].
+ }
+
+instance Outputable RedSets where
+ ppr RedSets { rs_cov = _cov, rs_div = _div, rs_bangs = _bangs }
+ -- It's useful to change this definition for different verbosity levels in
+ -- printf-debugging
+ = empty
+
+-- | Pattern-match coverage check result
+data CheckResult a
+ = CheckResult
+ { cr_ret :: !a
+ -- ^ A hole for redundancy info and covered sets.
+ , cr_uncov :: !Nablas
+ -- ^ The set of uncovered values falling out at the bottom.
+ -- (for -Wincomplete-patterns, but also important state for the algorithm)
+ , cr_approx :: !Precision
+ -- ^ A flag saying whether we ran into the 'maxPmCheckModels' limit for the
+ -- purpose of suggesting to crank it up in the warning message. Writer state.
+ } deriving Functor
+
+instance Outputable a => Outputable (CheckResult a) where
+ ppr (CheckResult c unc pc)
+ = text "CheckResult" <+> ppr_precision pc <+> braces (fsep
+ [ field "ret" c <> comma
+ , field "uncov" unc])
+ where
+ ppr_precision Precise = empty
+ ppr_precision Approximate = text "(Approximate)"
+ field name value = text name <+> equals <+> ppr value
+
+--
+-- * Pre and post coverage checking synonyms
+--
+
+-- | Used as tree payload pre-checking. The LYG guards to check.
+type Pre = GrdVec
+
+-- | Used as tree payload post-checking. The redundancy info we elaborated.
+type Post = RedSets
=====================================
compiler/GHC/HsToCore/Pmc/Utils.hs
=====================================
@@ -0,0 +1,140 @@
+{-# LANGUAGE CPP, LambdaCase, TupleSections, PatternSynonyms, ViewPatterns,
+ MultiWayIf, ScopedTypeVariables, MagicHash #-}
+
+-- | Utility module for the pattern-match coverage checker.
+module GHC.HsToCore.Pmc.Utils (
+
+ tracePm, mkPmId,
+ allPmCheckWarnings, overlapping, exhaustive, redundantBang,
+ exhaustiveWarningFlag,
+ isMatchContextPmChecked, needToRunPmCheck
+
+ ) where
+
+#include "HsVersions.h"
+
+import GHC.Prelude
+
+import GHC.Types.Basic (Origin(..), isGenerated)
+import GHC.Driver.Session
+import GHC.Hs
+import GHC.Core.Type
+import GHC.Data.FastString
+import GHC.Data.IOEnv
+import GHC.Types.Id
+import GHC.Types.Name
+import GHC.Types.Unique.Supply
+import GHC.Types.SrcLoc
+import GHC.Utils.Error
+import GHC.Utils.Misc
+import GHC.Utils.Outputable
+import GHC.HsToCore.Monad
+
+tracePm :: String -> SDoc -> DsM ()
+tracePm herald doc = do
+ dflags <- getDynFlags
+ printer <- mkPrintUnqualifiedDs
+ liftIO $ dumpIfSet_dyn_printer printer dflags
+ Opt_D_dump_ec_trace "" FormatText (text herald $$ (nest 2 doc))
+{-# INLINE tracePm #-} -- see Note [INLINE conditional tracing utilities]
+
+-- | Generate a fresh `Id` of a given type
+mkPmId :: Type -> DsM Id
+mkPmId ty = getUniqueM >>= \unique ->
+ let occname = mkVarOccFS $ fsLit "pm"
+ name = mkInternalName unique occname noSrcSpan
+ in return (mkLocalIdOrCoVar name Many ty)
+
+-- | All warning flags that need to run the pattern match checker.
+allPmCheckWarnings :: [WarningFlag]
+allPmCheckWarnings =
+ [ Opt_WarnIncompletePatterns
+ , Opt_WarnIncompleteUniPatterns
+ , Opt_WarnIncompletePatternsRecUpd
+ , Opt_WarnOverlappingPatterns
+ ]
+
+-- | Check whether the redundancy checker should run (redundancy only)
+overlapping :: DynFlags -> HsMatchContext id -> Bool
+-- See Note [Inaccessible warnings for record updates]
+overlapping _ RecUpd = False
+overlapping dflags _ = wopt Opt_WarnOverlappingPatterns dflags
+
+-- | Check whether the exhaustiveness checker should run (exhaustiveness only)
+exhaustive :: DynFlags -> HsMatchContext id -> Bool
+exhaustive dflags = maybe False (`wopt` dflags) . exhaustiveWarningFlag
+
+-- | Check whether unnecessary bangs should be warned about
+redundantBang :: DynFlags -> Bool
+redundantBang dflags = wopt Opt_WarnRedundantBangPatterns dflags
+
+-- | Denotes whether an exhaustiveness check is supported, and if so,
+-- via which 'WarningFlag' it's controlled.
+-- Returns 'Nothing' if check is not supported.
+exhaustiveWarningFlag :: HsMatchContext id -> Maybe WarningFlag
+exhaustiveWarningFlag (FunRhs {}) = Just Opt_WarnIncompletePatterns
+exhaustiveWarningFlag CaseAlt = Just Opt_WarnIncompletePatterns
+exhaustiveWarningFlag IfAlt = Just Opt_WarnIncompletePatterns
+exhaustiveWarningFlag LambdaExpr = Just Opt_WarnIncompleteUniPatterns
+exhaustiveWarningFlag PatBindRhs = Just Opt_WarnIncompleteUniPatterns
+exhaustiveWarningFlag PatBindGuards = Just Opt_WarnIncompletePatterns
+exhaustiveWarningFlag ProcExpr = Just Opt_WarnIncompleteUniPatterns
+exhaustiveWarningFlag RecUpd = Just Opt_WarnIncompletePatternsRecUpd
+exhaustiveWarningFlag ThPatSplice = Nothing
+exhaustiveWarningFlag PatSyn = Nothing
+exhaustiveWarningFlag ThPatQuote = Nothing
+-- Don't warn about incomplete patterns in list comprehensions, pattern guards
+-- etc. They are often *supposed* to be incomplete
+exhaustiveWarningFlag (StmtCtxt {}) = Nothing
+
+-- | Check whether any part of pattern match checking is enabled for this
+-- 'HsMatchContext' (does not matter whether it is the redundancy check or the
+-- exhaustiveness check).
+isMatchContextPmChecked :: DynFlags -> Origin -> HsMatchContext id -> Bool
+isMatchContextPmChecked dflags origin kind
+ | isGenerated origin
+ = False
+ | otherwise
+ = overlapping dflags kind || exhaustive dflags kind
+
+-- | Return True when any of the pattern match warnings ('allPmCheckWarnings')
+-- are enabled, in which case we need to run the pattern match checker.
+needToRunPmCheck :: DynFlags -> Origin -> Bool
+needToRunPmCheck dflags origin
+ | isGenerated origin
+ = False
+ | otherwise
+ = notNull (filter (`wopt` dflags) allPmCheckWarnings)
+
+{- Note [Inaccessible warnings for record updates]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider (#12957)
+ data T a where
+ T1 :: { x :: Int } -> T Bool
+ T2 :: { x :: Int } -> T a
+ T3 :: T a
+
+ f :: T Char -> T a
+ f r = r { x = 3 }
+
+The desugarer will conservatively generate a case for T1 even though
+it's impossible:
+ f r = case r of
+ T1 x -> T1 3 -- Inaccessible branch
+ T2 x -> T2 3
+ _ -> error "Missing"
+
+We don't want to warn about the inaccessible branch because the programmer
+didn't put it there! So we filter out the warning here.
+
+The same can happen for long distance term constraints instead of type
+constraints (#17783):
+
+ data T = A { x :: Int } | B { x :: Int }
+ f r at A{} = r { x = 3 }
+ f _ = B 0
+
+Here, the long distance info from the FunRhs match (@r ~ A x@) will make the
+clause matching on @B@ of the desugaring to @case@ redundant. It's generated
+code that we don't want to warn about.
+-}
=====================================
compiler/GHC/HsToCore/Types.hs
=====================================
@@ -14,7 +14,7 @@ import GHC.Types.SrcLoc
import GHC.Types.Var
import GHC.Hs (LForeignDecl, HsExpr, GhcTc)
import GHC.Tc.Types (TcRnIf, IfGblEnv, IfLclEnv, CompleteMatches)
-import GHC.HsToCore.PmCheck.Types (Nablas)
+import GHC.HsToCore.Pmc.Types (Nablas)
import GHC.Core (CoreExpr)
import GHC.Core.FamInstEnv
import GHC.Utils.Error
@@ -61,7 +61,7 @@ data DsLclEnv
{ dsl_meta :: DsMetaEnv -- ^ Template Haskell bindings
, dsl_loc :: RealSrcSpan -- ^ To put in pattern-matching error msgs
, dsl_nablas :: Nablas
- -- ^ See Note [Note [Long-distance information] in "GHC.HsToCore.PmCheck".
+ -- ^ See Note [Note [Long-distance information] in "GHC.HsToCore.Pmc".
-- The set of reaching values Nablas is augmented as we walk inwards, refined
-- through each pattern match in turn
}
=====================================
compiler/GHC/Tc/Solver.hs
=====================================
@@ -820,7 +820,7 @@ It does *not* reduce type or data family applications or look through newtypes.
Why is this useful? As one example, when coverage-checking an EmptyCase
expression, it's possible that the type of the scrutinee will only reduce
if some local equalities are solved for. See "Wrinkle: Local equalities"
-in Note [Type normalisation] in "GHC.HsToCore.PmCheck".
+in Note [Type normalisation] in "GHC.HsToCore.Pmc".
To accomplish its stated goal, tcNormalise first initialises the solver monad
with the given InertCans, then uses flattenType to simplify the desired type
=====================================
compiler/GHC/Types/Unique/SDFM.hs
=====================================
@@ -0,0 +1,121 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE ApplicativeDo #-}
+{-# OPTIONS_GHC -Wall #-}
+
+-- | Like a 'UniqDFM', but maintains equivalence classes of keys sharing the
+-- same entry. See 'UniqSDFM'.
+module GHC.Types.Unique.SDFM (
+ -- * Unique-keyed, /shared/, deterministic mappings
+ UniqSDFM,
+
+ emptyUSDFM,
+ lookupUSDFM,
+ equateUSDFM, addToUSDFM,
+ traverseUSDFM
+ ) where
+
+import GHC.Prelude
+
+import GHC.Types.Unique
+import GHC.Types.Unique.DFM
+import GHC.Utils.Outputable
+
+-- | Either @Indirect x@, meaning the value is represented by that of @x@, or
+-- an @Entry@ containing containing the actual value it represents.
+data Shared key ele
+ = Indirect !key
+ | Entry !ele
+
+-- | A 'UniqDFM' whose domain is /sets/ of 'Unique's, each of which share a
+-- common value of type @ele at .
+-- Every such set (\"equivalence class\") has a distinct representative
+-- 'Unique'. Supports merging the entries of multiple such sets in a union-find
+-- like fashion.
+--
+-- An accurate model is that of @[(Set key, Maybe ele)]@: A finite mapping from
+-- sets of @key at s to possibly absent entries @ele@, where the sets don't overlap.
+-- Example:
+-- @
+-- m = [({u1,u3}, Just ele1), ({u2}, Just ele2), ({u4,u7}, Nothing)]
+-- @
+-- On this model we support the following main operations:
+--
+-- * @'lookupUSDFM' m u3 == Just ele1@, @'lookupUSDFM' m u4 == Nothing@,
+-- @'lookupUSDFM' m u5 == Nothing at .
+-- * @'equateUSDFM' m u1 u3@ is a no-op, but
+-- @'equateUSDFM' m u1 u2@ merges @{u1,u3}@ and @{u2}@ to point to
+-- @Just ele2@ and returns the old entry of @{u1,u3}@, @Just ele1 at .
+-- * @'addToUSDFM' m u3 ele4@ sets the entry of @{u1,u3}@ to @Just ele4 at .
+--
+-- As well as a few means for traversal/conversion to list.
+newtype UniqSDFM key ele
+ = USDFM { unUSDFM :: UniqDFM key (Shared key ele) }
+
+emptyUSDFM :: UniqSDFM key ele
+emptyUSDFM = USDFM emptyUDFM
+
+lookupReprAndEntryUSDFM :: Uniquable key => UniqSDFM key ele -> key -> (key, Maybe ele)
+lookupReprAndEntryUSDFM (USDFM env) = go
+ where
+ go x = case lookupUDFM env x of
+ Nothing -> (x, Nothing)
+ Just (Indirect y) -> go y
+ Just (Entry ele) -> (x, Just ele)
+
+-- | @lookupSUDFM env x@ looks up an entry for @x@, looking through all
+-- 'Indirect's until it finds a shared 'Entry'.
+--
+-- Examples in terms of the model (see 'UniqSDFM'):
+-- >>> lookupUSDFM [({u1,u3}, Just ele1), ({u2}, Just ele2)] u3 == Just ele1
+-- >>> lookupUSDFM [({u1,u3}, Just ele1), ({u2}, Just ele2)] u4 == Nothing
+-- >>> lookupUSDFM [({u1,u3}, Just ele1), ({u2}, Nothing)] u2 == Nothing
+lookupUSDFM :: Uniquable key => UniqSDFM key ele -> key -> Maybe ele
+lookupUSDFM usdfm x = snd (lookupReprAndEntryUSDFM usdfm x)
+
+-- | @equateUSDFM env x y@ makes @x@ and @y@ point to the same entry,
+-- thereby merging @x@'s class with @y@'s.
+-- If both @x@ and @y@ are in the domain of the map, then @y@'s entry will be
+-- chosen as the new entry and @x@'s old entry will be returned.
+--
+-- Examples in terms of the model (see 'UniqSDFM'):
+-- >>> equateUSDFM [] u1 u2 == (Nothing, [({u1,u2}, Nothing)])
+-- >>> equateUSDFM [({u1,u3}, Just ele1)] u3 u4 == (Nothing, [({u1,u3,u4}, Just ele1)])
+-- >>> equateUSDFM [({u1,u3}, Just ele1)] u4 u3 == (Nothing, [({u1,u3,u4}, Just ele1)])
+-- >>> equateUSDFM [({u1,u3}, Just ele1), ({u2}, Just ele2)] u3 u2 == (Just ele1, [({u2,u1,u3}, Just ele2)])
+equateUSDFM
+ :: Uniquable key => UniqSDFM key ele -> key -> key -> (Maybe ele, UniqSDFM key ele)
+equateUSDFM usdfm@(USDFM env) x y =
+ case (lu x, lu y) of
+ ((x', _) , (y', _))
+ | getUnique x' == getUnique y' -> (Nothing, usdfm) -- nothing to do
+ ((x', _) , (_ , Nothing)) -> (Nothing, set_indirect y x')
+ ((_ , mb_ex), (y', _)) -> (mb_ex, set_indirect x y')
+ where
+ lu = lookupReprAndEntryUSDFM usdfm
+ set_indirect a b = USDFM $ addToUDFM env a (Indirect b)
+
+-- | @addToUSDFM env x a@ sets the entry @x@ is associated with to @a@,
+-- thereby modifying its whole equivalence class.
+--
+-- Examples in terms of the model (see 'UniqSDFM'):
+-- >>> addToUSDFM [] u1 ele1 == [({u1}, Just ele1)]
+-- >>> addToUSDFM [({u1,u3}, Just ele1)] u3 ele2 == [({u1,u3}, Just ele2)]
+addToUSDFM :: Uniquable key => UniqSDFM key ele -> key -> ele -> UniqSDFM key ele
+addToUSDFM usdfm@(USDFM env) x v =
+ USDFM $ addToUDFM env (fst (lookupReprAndEntryUSDFM usdfm x)) (Entry v)
+
+traverseUSDFM :: forall key a b f. Applicative f => (a -> f b) -> UniqSDFM key a -> f (UniqSDFM key b)
+traverseUSDFM f = fmap (USDFM . listToUDFM_Directly) . traverse g . udfmToList . unUSDFM
+ where
+ g :: (Unique, Shared key a) -> f (Unique, Shared key b)
+ g (u, Indirect y) = pure (u,Indirect y)
+ g (u, Entry a) = do
+ a' <- f a
+ pure (u,Entry a')
+
+instance (Outputable key, Outputable ele) => Outputable (Shared key ele) where
+ ppr (Indirect x) = ppr x
+ ppr (Entry a) = ppr a
+
+instance (Outputable key, Outputable ele) => Outputable (UniqSDFM key ele) where
+ ppr (USDFM env) = ppr env
=====================================
compiler/ghc.cabal.in
=====================================
@@ -307,10 +307,14 @@ Library
GHC.Core.Stats
GHC.Core.Make
GHC.Core.Ppr
- GHC.HsToCore.PmCheck.Oracle
- GHC.HsToCore.PmCheck.Ppr
- GHC.HsToCore.PmCheck.Types
- GHC.HsToCore.PmCheck
+ GHC.HsToCore.Pmc
+ GHC.HsToCore.Pmc.Types
+ GHC.HsToCore.Pmc.Utils
+ GHC.HsToCore.Pmc.Desugar
+ GHC.HsToCore.Pmc.Check
+ GHC.HsToCore.Pmc.Solver.Types
+ GHC.HsToCore.Pmc.Solver
+ GHC.HsToCore.Pmc.Ppr
GHC.HsToCore.Coverage
GHC.HsToCore
GHC.HsToCore.Types
@@ -565,6 +569,7 @@ Library
GHC.Data.Stream
GHC.Data.StringBuffer
GHC.Types.Unique.DFM
+ GHC.Types.Unique.SDFM
GHC.Types.Unique.DSet
GHC.Types.Unique.FM
GHC.Types.Unique.Set
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/83407ffc7acc00cc025b9f6ed063add9ab9f9bcc...f08f98e821bc4b755a7b6ad3bad39ce1099c5405
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/83407ffc7acc00cc025b9f6ed063add9ab9f9bcc...f08f98e821bc4b755a7b6ad3bad39ce1099c5405
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20200926/6350d265/attachment-0001.html>
More information about the ghc-commits
mailing list