never executed always true always false
1
2 {-# LANGUAGE FlexibleInstances #-}
3 {-# LANGUAGE GADTs #-}
4 {-# LANGUAGE LambdaCase #-}
5
6 -- | This module coverage checks pattern matches. It finds
7 --
8 -- * Uncovered patterns, certifying non-exhaustivity
9 -- * Redundant equations
10 -- * Equations with an inaccessible right-hand-side
11 --
12 -- The algorithm is based on the paper
13 -- [Lower Your Guards: A Compositional Pattern-Match Coverage Checker"](https://dl.acm.org/doi/abs/10.1145/3408989)
14 --
15 -- There is an overview Figure 2 in there that's probably helpful.
16 -- Here is an overview of how it's implemented, which follows the structure of
17 -- the entry points such as 'pmcMatches':
18 --
19 -- 1. Desugar source syntax (like 'LMatch') to guard tree variants (like
20 -- 'GrdMatch'), with one of the desugaring functions (like 'desugarMatch').
21 -- See "GHC.HsToCore.Pmc.Desugar".
22 -- Follows Section 3.1 in the paper.
23 -- 2. Coverage check guard trees (with a function like 'checkMatch') to get a
24 -- 'CheckResult'. See "GHC.HsToCore.Pmc.Check".
25 -- The normalised refinement types 'Nabla' are tested for inhabitants by
26 -- "GHC.HsToCore.Pmc.Solver".
27 -- 3. Collect redundancy information into a 'CIRB' with a function such
28 -- as 'cirbsMatch'. Follows the R function from Figure 6 of the paper.
29 -- 4. Format and report uncovered patterns and redundant equations ('CIRB')
30 -- with 'formatReportWarnings'. Basically job of the G function, plus proper
31 -- pretty printing of the warnings (Section 5.4 of the paper).
32 -- 5. Return 'Nablas' reaching syntactic sub-components for
33 -- Note [Long-distance information]. Collected by functions such as
34 -- 'ldiMatch'. See Section 4.1 of the paper.
35 module GHC.HsToCore.Pmc (
36 -- Checking and printing
37 pmcPatBind, pmcMatches, pmcGRHSs,
38 isMatchContextPmChecked,
39
40 -- See Note [Long-distance information]
41 addTyCs, addCoreScrutTmCs, addHsScrutTmCs
42 ) where
43
44 import GHC.Prelude
45
46 import GHC.HsToCore.Errors.Types
47 import GHC.HsToCore.Pmc.Types
48 import GHC.HsToCore.Pmc.Utils
49 import GHC.HsToCore.Pmc.Desugar
50 import GHC.HsToCore.Pmc.Check
51 import GHC.HsToCore.Pmc.Solver
52 import GHC.Types.Basic (Origin(..))
53 import GHC.Core (CoreExpr)
54 import GHC.Driver.Session
55 import GHC.Hs
56 import GHC.Types.Id
57 import GHC.Types.SrcLoc
58 import GHC.Utils.Misc
59 import GHC.Utils.Outputable
60 import GHC.Utils.Panic
61 import GHC.Types.Var (EvVar)
62 import GHC.Tc.Utils.TcType (evVarPred)
63 import GHC.Tc.Utils.Monad (updTopFlags)
64 import {-# SOURCE #-} GHC.HsToCore.Expr (dsLExpr)
65 import GHC.HsToCore.Monad
66 import GHC.Data.Bag
67 import GHC.Data.IOEnv (unsafeInterleaveM)
68 import GHC.Data.OrdList
69 import GHC.Utils.Monad (mapMaybeM)
70
71 import Control.Monad (when, forM_)
72 import qualified Data.Semigroup as Semi
73 import Data.List.NonEmpty ( NonEmpty(..) )
74 import qualified Data.List.NonEmpty as NE
75 import Data.Coerce
76
77 --
78 -- * Exported entry points to the checker
79 --
80
81 -- | A non-empty delta that is initialised from the ambient refinement type
82 -- capturing long-distance information, or the trivially habitable 'Nablas' if
83 -- the former is uninhabited.
84 -- See Note [Recovering from unsatisfiable pattern-matching constraints].
85 getLdiNablas :: DsM Nablas
86 getLdiNablas = do
87 nablas <- getPmNablas
88 isInhabited nablas >>= \case
89 True -> pure nablas
90 False -> pure initNablas
91
92 -- | We need to call the Hs desugarer to get the Core of a let-binding or where
93 -- clause. We don't want to run the coverage checker when doing so! Efficiency
94 -- is one concern, but also a lack of properly set up long-distance information
95 -- might trigger warnings that we normally wouldn't emit.
96 noCheckDs :: DsM a -> DsM a
97 noCheckDs = updTopFlags (\dflags -> foldl' wopt_unset dflags allPmCheckWarnings)
98
99 -- | Check a pattern binding (let, where) for exhaustiveness.
100 pmcPatBind :: DsMatchContext -> Id -> Pat GhcTc -> DsM ()
101 -- See Note [pmcPatBind only checks PatBindRhs]
102 pmcPatBind ctxt@(DsMatchContext PatBindRhs loc) var p = do
103 !missing <- getLdiNablas
104 pat_bind <- noCheckDs $ desugarPatBind loc var p
105 tracePm "pmcPatBind {" (vcat [ppr ctxt, ppr var, ppr p, ppr pat_bind, ppr missing])
106 result <- unCA (checkPatBind pat_bind) missing
107 tracePm "}: " (ppr (cr_uncov result))
108 formatReportWarnings cirbsPatBind ctxt [var] result
109 pmcPatBind _ _ _ = pure ()
110
111 -- | Exhaustive for guard matches, is used for guards in pattern bindings and
112 -- in @MultiIf@ expressions. Returns the 'Nablas' covered by the RHSs.
113 pmcGRHSs
114 :: HsMatchContext GhcRn -- ^ Match context, for warning messages
115 -> GRHSs GhcTc (LHsExpr GhcTc) -- ^ The GRHSs to check
116 -> DsM (NonEmpty Nablas) -- ^ Covered 'Nablas' for each RHS, for long
117 -- distance info
118 pmcGRHSs hs_ctxt guards@(GRHSs _ grhss _) = do
119 let combined_loc = foldl1 combineSrcSpans (map getLocA grhss)
120 ctxt = DsMatchContext hs_ctxt combined_loc
121 !missing <- getLdiNablas
122 matches <- noCheckDs $ desugarGRHSs combined_loc empty guards
123 tracePm "pmcGRHSs" (hang (vcat [ppr ctxt
124 , text "Guards:"])
125 2
126 (pprGRHSs hs_ctxt guards $$ ppr missing))
127 result <- unCA (checkGRHSs matches) missing
128 tracePm "}: " (ppr (cr_uncov result))
129 formatReportWarnings cirbsGRHSs ctxt [] result
130 return (ldiGRHSs (cr_ret result))
131
132 -- | Check a list of syntactic 'Match'es (part of case, functions, etc.), each
133 -- with a 'Pat' and one or more 'GRHSs':
134 --
135 -- @
136 -- f x y | x == y = 1 -- match on x and y with two guarded RHSs
137 -- | otherwise = 2
138 -- f _ _ = 3 -- clause with a single, un-guarded RHS
139 -- @
140 --
141 -- Returns one non-empty 'Nablas' for 1.) each pattern of a 'Match' and 2.)
142 -- each of a 'Match'es 'GRHS' for Note [Long-distance information].
143 --
144 -- Special case: When there are /no matches/, then the functionassumes it
145 -- checks and @-XEmptyCase@ with only a single match variable.
146 -- See Note [Checking EmptyCase].
147 pmcMatches
148 :: DsMatchContext -- ^ Match context, for warnings messages
149 -> [Id] -- ^ Match variables, i.e. x and y above
150 -> [LMatch GhcTc (LHsExpr GhcTc)] -- ^ List of matches
151 -> DsM [(Nablas, NonEmpty Nablas)] -- ^ One covered 'Nablas' per Match and
152 -- GRHS, for long distance info.
153 pmcMatches ctxt vars matches = {-# SCC "pmcMatches" #-} do
154 -- We have to force @missing@ before printing out the trace message,
155 -- otherwise we get interleaved output from the solver. This function
156 -- should be strict in @missing@ anyway!
157 !missing <- getLdiNablas
158 tracePm "pmcMatches {" $
159 hang (vcat [ppr ctxt, ppr vars, text "Matches:"])
160 2
161 (vcat (map ppr matches) $$ ppr missing)
162 case NE.nonEmpty matches of
163 Nothing -> do
164 -- This must be an -XEmptyCase. See Note [Checking EmptyCase]
165 let var = only vars
166 empty_case <- noCheckDs $ desugarEmptyCase var
167 result <- unCA (checkEmptyCase empty_case) missing
168 tracePm "}: " (ppr (cr_uncov result))
169 formatReportWarnings cirbsEmptyCase ctxt vars result
170 return []
171 Just matches -> do
172 matches <- {-# SCC "desugarMatches" #-}
173 noCheckDs $ desugarMatches vars matches
174 result <- {-# SCC "checkMatchGroup" #-}
175 unCA (checkMatchGroup matches) missing
176 tracePm "}: " (ppr (cr_uncov result))
177 {-# SCC "formatReportWarnings" #-} formatReportWarnings cirbsMatchGroup ctxt vars result
178 return (NE.toList (ldiMatchGroup (cr_ret result)))
179
180 {- Note [pmcPatBind only checks PatBindRhs]
181 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
182 @pmcPatBind@'s sole purpose is to check vanilla pattern bindings, like
183 @x :: Int; Just x = e@, which is in a @PatBindRhs@ context.
184 But its caller is also called for individual pattern guards in a @StmtCtxt@.
185 For example, both pattern guards in @f x y | True <- x, False <- y = ...@ will
186 go through this function. It makes no sense to do coverage checking there:
187 * Pattern guards may well fail. Fall-through is not an unrecoverable panic,
188 but rather behavior the programmer expects, so inexhaustivity should not be
189 reported.
190 * Redundancy is already reported for the whole GRHS via one of the other
191 exported coverage checking functions. Also reporting individual redundant
192 guards is... redundant. See #17646.
193 Note that we can't just omit checking of @StmtCtxt@ altogether (by adjusting
194 'isMatchContextPmChecked'), because that affects the other checking functions,
195 too.
196 -}
197
198 --
199 -- * Collecting long-distance information
200 --
201
202 ldiMatchGroup :: PmMatchGroup Post -> NonEmpty (Nablas, NonEmpty Nablas)
203 ldiMatchGroup (PmMatchGroup matches) = ldiMatch <$> matches
204
205 ldiMatch :: PmMatch Post -> (Nablas, NonEmpty Nablas)
206 ldiMatch (PmMatch { pm_pats = red, pm_grhss = grhss }) =
207 (rs_cov red, ldiGRHSs grhss)
208
209 ldiGRHSs :: PmGRHSs Post -> NonEmpty Nablas
210 ldiGRHSs (PmGRHSs { pgs_grhss = grhss }) = ldiGRHS <$> grhss
211
212 ldiGRHS :: PmGRHS Post -> Nablas
213 ldiGRHS (PmGRHS { pg_grds = red }) = rs_cov red
214
215 --
216 -- * Collecting redundancy information
217 --
218
219 -- | The result of redundancy checking:
220 -- * RHSs classified as /C/overed, /I/naccessible and /R/edundant
221 -- * And redundant /B/ang patterns. See Note [Dead bang patterns].
222 data CIRB
223 = CIRB
224 { cirb_cov :: !(OrdList SrcInfo) -- ^ Covered clauses
225 , cirb_inacc :: !(OrdList SrcInfo) -- ^ Inaccessible clauses
226 , cirb_red :: !(OrdList SrcInfo) -- ^ Redundant clauses
227 , cirb_bangs :: !(OrdList SrcInfo) -- ^ Redundant bang patterns
228 }
229
230 instance Semigroup CIRB where
231 CIRB a b c d <> CIRB e f g h = CIRB (a <> e) (b <> f) (c <> g) (d <> h)
232 where (<>) = (Semi.<>)
233
234 instance Monoid CIRB where
235 mempty = CIRB mempty mempty mempty mempty
236
237 -- See Note [Determining inaccessible clauses]
238 ensureOneNotRedundant :: CIRB -> CIRB
239 ensureOneNotRedundant ci = case ci of
240 CIRB { cirb_cov = NilOL, cirb_inacc = NilOL, cirb_red = ConsOL r rs }
241 -> ci { cirb_inacc = unitOL r, cirb_red = rs }
242 _ -> ci
243
244 -- | Only adds the redundant bangs to the @CIRB@ if there is at least one
245 -- non-redundant 'SrcInfo'. There is no point in remembering a redundant bang
246 -- if the whole match is redundant!
247 addRedundantBangs :: OrdList SrcInfo -> CIRB -> CIRB
248 addRedundantBangs _red_bangs cirb@CIRB { cirb_cov = NilOL, cirb_inacc = NilOL } =
249 cirb
250 addRedundantBangs red_bangs cirb =
251 cirb { cirb_bangs = cirb_bangs cirb Semi.<> red_bangs }
252
253 -- | Checks the 'Nablas' in a 'RedSets' for inhabitants and returns
254 -- 1. Whether the Covered set was inhabited
255 -- 2. Whether the Diverging set was inhabited
256 -- 3. All source bangs whose 'Nablas' were empty, which means they are
257 -- redundant.
258 testRedSets :: RedSets -> DsM (Bool, Bool, OrdList SrcInfo)
259 testRedSets RedSets { rs_cov = cov, rs_div = div, rs_bangs = bangs } = do
260 is_covered <- isInhabited cov
261 may_diverge <- isInhabited div
262 red_bangs <- flip mapMaybeM (fromOL bangs) $ \(nablas, bang) ->
263 isInhabited nablas >>= \case
264 True -> pure Nothing
265 False -> pure (Just bang)
266 pure (is_covered, may_diverge, toOL red_bangs)
267
268 cirbsMatchGroup :: PmMatchGroup Post -> DsM CIRB
269 cirbsMatchGroup (PmMatchGroup matches) =
270 Semi.sconcat <$> traverse cirbsMatch matches
271
272 cirbsMatch :: PmMatch Post -> DsM CIRB
273 cirbsMatch PmMatch { pm_pats = red, pm_grhss = grhss } = do
274 (_is_covered, may_diverge, red_bangs) <- testRedSets red
275 -- Don't look at is_covered: If it is True, all children are redundant anyway,
276 -- unless there is a 'considerAccessible', which may break that rule
277 -- intentionally. See Note [considerAccessible] in "GHC.HsToCore.Pmc.Check".
278 cirb <- cirbsGRHSs grhss
279 pure $ addRedundantBangs red_bangs
280 -- See Note [Determining inaccessible clauses]
281 $ applyWhen may_diverge ensureOneNotRedundant
282 $ cirb
283
284 cirbsGRHSs :: PmGRHSs Post -> DsM CIRB
285 cirbsGRHSs (PmGRHSs { pgs_grhss = grhss }) = Semi.sconcat <$> traverse cirbsGRHS grhss
286
287 cirbsGRHS :: PmGRHS Post -> DsM CIRB
288 cirbsGRHS PmGRHS { pg_grds = red, pg_rhs = info } = do
289 (is_covered, may_diverge, red_bangs) <- testRedSets red
290 let cirb | is_covered = mempty { cirb_cov = unitOL info }
291 | may_diverge = mempty { cirb_inacc = unitOL info }
292 | otherwise = mempty { cirb_red = unitOL info }
293 pure (addRedundantBangs red_bangs cirb)
294
295 cirbsEmptyCase :: PmEmptyCase -> DsM CIRB
296 cirbsEmptyCase _ = pure mempty
297
298 cirbsPatBind :: PmPatBind Post -> DsM CIRB
299 cirbsPatBind = coerce cirbsGRHS
300
301 {- Note [Determining inaccessible clauses]
302 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
303 Consider
304 f _ True = ()
305 f () True = ()
306 f _ _ = ()
307 Is f's second clause redundant? The perhaps surprising answer is, no, it isn't!
308 @f (error "boom") False@ will force the error with clause 2, but will return
309 () if it was deleted, so clearly not redundant. Yet for now combination of
310 arguments we can ever reach clause 2's RHS, so we say it has inaccessible RHS
311 (as opposed to being completely redundant).
312
313 We detect an inaccessible RHS simply by pretending it's redundant, until we see
314 -}
315
316 --
317 -- * Formatting and reporting warnings
318 --
319
320 -- | Given a function that collects 'CIRB's, this function will emit warnings
321 -- for a 'CheckResult'.
322 formatReportWarnings :: (ann -> DsM CIRB) -> DsMatchContext -> [Id] -> CheckResult ann -> DsM ()
323 formatReportWarnings collect ctx vars cr@CheckResult { cr_ret = ann } = do
324 cov_info <- collect ann
325 dflags <- getDynFlags
326 reportWarnings dflags ctx vars cr{cr_ret=cov_info}
327
328 -- | Issue all the warnings
329 -- (redundancy, inaccessibility, exhaustiveness, redundant bangs).
330 reportWarnings :: DynFlags -> DsMatchContext -> [Id] -> CheckResult CIRB -> DsM ()
331 reportWarnings dflags (DsMatchContext kind loc) vars
332 CheckResult { cr_ret = CIRB { cirb_inacc = inaccessible_rhss
333 , cirb_red = redundant_rhss
334 , cirb_bangs = redundant_bangs }
335 , cr_uncov = uncovered
336 , cr_approx = precision }
337 = when (flag_i || flag_u || flag_b) $ do
338 unc_examples <- getNFirstUncovered vars (maxPatterns + 1) uncovered
339 let exists_r = flag_i && notNull redundant_rhss
340 exists_i = flag_i && notNull inaccessible_rhss
341 exists_u = flag_u && notNull unc_examples
342 exists_b = flag_b && notNull redundant_bangs
343 approx = precision == Approximate
344
345 when (approx && (exists_u || exists_i)) $
346 putSrcSpanDs loc (diagnosticDs (DsMaxPmCheckModelsReached (maxPmCheckModels dflags)))
347
348 when exists_b $ forM_ redundant_bangs $ \(SrcInfo (L l q)) ->
349 putSrcSpanDs l (diagnosticDs (DsRedundantBangPatterns kind q))
350
351 when exists_r $ forM_ redundant_rhss $ \(SrcInfo (L l q)) ->
352 putSrcSpanDs l (diagnosticDs (DsOverlappingPatterns kind q))
353 when exists_i $ forM_ inaccessible_rhss $ \(SrcInfo (L l q)) ->
354 putSrcSpanDs l (diagnosticDs (DsInaccessibleRhs kind q))
355
356 when exists_u $
357 putSrcSpanDs loc (diagnosticDs (DsNonExhaustivePatterns kind check_type maxPatterns vars unc_examples))
358 where
359 flag_i = overlapping dflags kind
360 flag_u = exhaustive dflags kind
361 flag_b = redundantBang dflags
362 check_type = ExhaustivityCheckType (exhaustiveWarningFlag kind)
363
364 maxPatterns = maxUncoveredPatterns dflags
365
366 getNFirstUncovered :: [Id] -> Int -> Nablas -> DsM [Nabla]
367 getNFirstUncovered vars n (MkNablas nablas) = go n (bagToList nablas)
368 where
369 go 0 _ = pure []
370 go _ [] = pure []
371 go n (nabla:nablas) = do
372 front <- generateInhabitingPatterns vars n nabla
373 back <- go (n - length front) nablas
374 pure (front ++ back)
375
376 --
377 -- * Adding external long-distance information
378 --
379
380 -- | Locally update 'dsl_nablas' with the given action, but defer evaluation
381 -- with 'unsafeInterleaveM' in order not to do unnecessary work.
382 locallyExtendPmNablas :: (Nablas -> DsM Nablas) -> DsM a -> DsM a
383 locallyExtendPmNablas ext k = do
384 nablas <- getLdiNablas
385 nablas' <- unsafeInterleaveM $ ext nablas
386 updPmNablas nablas' k
387
388 -- | Add in-scope type constraints if the coverage checker might run and then
389 -- run the given action.
390 addTyCs :: Origin -> Bag EvVar -> DsM a -> DsM a
391 addTyCs origin ev_vars m = do
392 dflags <- getDynFlags
393 applyWhen (needToRunPmCheck dflags origin)
394 (locallyExtendPmNablas $ \nablas ->
395 addPhiCtsNablas nablas (PhiTyCt . evVarPred <$> ev_vars))
396 m
397
398 -- | Add equalities for the 'CoreExpr' scrutinee to the local 'DsM' environment
399 -- when checking a case expression:
400 -- case e of x { matches }
401 -- When checking matches we record that (x ~ e) where x is the initial
402 -- uncovered. All matches will have to satisfy this equality.
403 addCoreScrutTmCs :: Maybe CoreExpr -> [Id] -> DsM a -> DsM a
404 addCoreScrutTmCs Nothing _ k = k
405 addCoreScrutTmCs (Just scr) [x] k =
406 flip locallyExtendPmNablas k $ \nablas ->
407 addPhiCtsNablas nablas (unitBag (PhiCoreCt x scr))
408 addCoreScrutTmCs _ _ _ = panic "addCoreScrutTmCs: scrutinee, but more than one match id"
409
410 -- | 'addCoreScrutTmCs', but desugars the 'LHsExpr' first.
411 addHsScrutTmCs :: Maybe (LHsExpr GhcTc) -> [Id] -> DsM a -> DsM a
412 addHsScrutTmCs Nothing _ k = k
413 addHsScrutTmCs (Just scr) vars k = do
414 scr_e <- dsLExpr scr
415 addCoreScrutTmCs (Just scr_e) vars k
416
417 {- Note [Long-distance information]
418 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
419 Consider
420
421 data Color = R | G | B
422 f :: Color -> Int
423 f R = …
424 f c = … (case c of
425 G -> True
426 B -> False) …
427
428 Humans can make the "long-distance connection" between the outer pattern match
429 and the nested case pattern match to see that the inner pattern match is
430 exhaustive: @c@ can't be @R@ anymore because it was matched in the first clause
431 of @f@.
432
433 To achieve similar reasoning in the coverage checker, we keep track of the set
434 of values that can reach a particular program point (often loosely referred to
435 as "Covered set") in 'GHC.HsToCore.Monad.dsl_nablas'.
436 We fill that set with Covered Nablas returned by the exported checking
437 functions, which the call sites put into place with
438 'GHC.HsToCore.Monad.updPmNablas'.
439 Call sites also extend this set with facts from type-constraint dictionaries,
440 case scrutinees, etc. with the exported functions 'addTyCs', 'addCoreScrutTmCs'
441 and 'addHsScrutTmCs'.
442
443 Note [Recovering from unsatisfiable pattern-matching constraints]
444 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
445 Consider the following code (see #12957 and #15450):
446
447 f :: Int ~ Bool => ()
448 f = case True of { False -> () }
449
450 We want to warn that the pattern-matching in `f` is non-exhaustive. But GHC
451 used not to do this; in fact, it would warn that the match was /redundant/!
452 This is because the constraint (Int ~ Bool) in `f` is unsatisfiable, and the
453 coverage checker deems any matches with unsatisfiable constraint sets to be
454 unreachable.
455
456 We make sure to always start from an inhabited 'Nablas' by calling
457 'getLdiNablas', which falls back to the trivially inhabited 'Nablas' if the
458 long-distance info returned by 'GHC.HsToCore.Monad.getPmNablas' is empty.
459 -}