Commit ebd773a0 authored by Ryan Scott's avatar Ryan Scott Committed by Ben Gamari

Fix #15450 by refactoring checkEmptyCase'

`checkEmptyCase'` (the code path for coverage-checking
`EmptyCase` expressions) had a fair bit of code duplication from the
code path for coverage-checking non-`EmptyCase` expressions, and to
make things worse, it behaved subtly different in some respects (for
instance, emitting different warnings under unsatisfiable
constraints, as shown in #15450). This patch attempts to clean up
both this discrepancy and the code duplication by doing the
following:

* Factor out a `pmInitialTmTyCs` function, which returns the initial
  set of term and type constraints to use when beginning coverage
  checking. If either set of constraints is unsatisfiable, we use an
  empty set in its place so that we can continue to emit as many
  warnings as possible. (The code path for non-`EmptyCase`
  expressions was doing this already, but not the code path for
  `EmptyCase` expressions, which is the root cause of #15450.)

  Along the way, I added a `Note` to explain why we do this.
* Factor out a `pmIsSatisfiable` constraint which checks if a set of
  term and type constraints are satisfiable. This does not change any
  existing behavior; this is just for the sake of deduplicating code.

Test Plan: make test TEST=T15450

Reviewers: simonpj, bgamari

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #15450

Differential Revision: https://phabricator.haskell.org/D5017

(cherry picked from commit 7f3cb50d)
parent a97ead78
......@@ -426,32 +426,28 @@ checkMatches' vars matches
-- for details.
checkEmptyCase' :: Id -> PmM PmResult
checkEmptyCase' var = do
tm_css <- map toComplex . bagToList <$> liftD getTmCsDs
case tmOracle initialTmState tm_css of
Just tm_state -> do
ty_css <- liftD getDictsDs
fam_insts <- liftD dsGetFamInstEnvs
mb_candidates <- inhabitationCandidates fam_insts (idType var)
case mb_candidates of
-- Inhabitation checking failed / the type is trivially inhabited
Left ty -> return (uncoveredWithTy ty)
-- A list of inhabitant candidates is available: Check for each
-- one for the satisfiability of the constraints it gives rise to.
Right candidates -> do
missing_m <- flip concatMapM candidates $ \(va,tm_ct,ty_cs) -> do
let all_ty_cs = unionBags ty_cs ty_css
sat_ty <- tyOracle all_ty_cs
return $ case (sat_ty, tmOracle tm_state (tm_ct:tm_css)) of
(True, Just tm_state') -> [(va, all_ty_cs, tm_state')]
_non_sat -> []
let mkValVec (va,all_ty_cs,tm_state')
= ValVec [va] (MkDelta all_ty_cs tm_state')
uncovered = UncoveredPatterns (map mkValVec missing_m)
return $ if null missing_m
then emptyPmResult
else PmResult FromBuiltin [] uncovered []
Nothing -> return emptyPmResult
(tm_css, ty_css) <- pmInitialTmTyCs
fam_insts <- liftD dsGetFamInstEnvs
mb_candidates <- inhabitationCandidates fam_insts (idType var)
case mb_candidates of
-- Inhabitation checking failed / the type is trivially inhabited
Left ty -> return (uncoveredWithTy ty)
-- A list of inhabitant candidates is available: Check for each
-- one for the satisfiability of the constraints it gives rise to.
Right candidates -> do
missing_m <- flip concatMapM candidates $ \(va,tm_ct,ty_cs) -> do
mb_sat <- pmIsSatisfiable tm_ct tm_css ty_cs ty_css
pure $ case mb_sat of
Just (tm_state', all_ty_cs)
-> [(va, all_ty_cs, tm_state')]
Nothing -> []
let mkValVec (va,all_ty_cs,tm_state')
= ValVec [va] (MkDelta all_ty_cs tm_state')
uncovered = UncoveredPatterns (map mkValVec missing_m)
return $ if null missing_m
then emptyPmResult
else PmResult FromBuiltin [] uncovered []
-- | Returns 'True' if the argument 'Type' is a fully saturated application of
-- a closed type constructor.
......@@ -543,6 +539,73 @@ pmTopNormaliseType_maybe env typ
Just (_co, rhs) -> NS_Step rec_nts rhs ((rhs:), id)
_ -> NS_Done
-- | Determine suitable constraints to use at the beginning of pattern-match
-- coverage checking by consulting the sets of term and type constraints
-- currently in scope. If one of these sets of constraints is unsatisfiable,
-- use an empty set in its place. (See
-- @Note [Recovering from unsatisfiable pattern-matching constraints]@
-- for why this is done.)
pmInitialTmTyCs :: PmM (TmState, Bag EvVar)
pmInitialTmTyCs = do
ty_cs <- liftD getDictsDs
tm_cs <- map toComplex . bagToList <$> liftD getTmCsDs
sat_ty <- tyOracle ty_cs
let initTyCs = if sat_ty then ty_cs else emptyBag
initTmState = fromMaybe initialTmState (tmOracle initialTmState tm_cs)
pure (initTmState, initTyCs)
{-
Note [Recovering from unsatisfiable pattern-matching constraints]
~~~~~~~~~~~~~~~~
Consider the following code (see #12957 and #15450):
f :: Int ~ Bool => ()
f = case True of { False -> () }
We want to warn that the pattern-matching in `f` is non-exhaustive. But GHC
used not to do this; in fact, it would warn that the match was /redundant/!
This is because the constraint (Int ~ Bool) in `f` is unsatisfiable, and the
coverage checker deems any matches with unsatifiable constraint sets to be
unreachable.
We decide to better than this. When beginning coverage checking, we first
check if the constraints in scope are unsatisfiable, and if so, we start
afresh with an empty set of constraints. This way, we'll get the warnings
that we expect.
-}
-- | Given some term and type constraints, check if they are satisfiable.
-- (In other words, this is the ⊢_Sat oracle judgment from the GADTs Meet
-- Their Match paper.)
--
-- For the purposes of efficiency, this takes as separate arguments the
-- ambient term and type constraints (which are known beforehand to be
-- satisfiable), as well as the new term and type constraints (which may not
-- be satisfiable). This lets us implement two mini-optimizations:
--
-- * If there are no new type constraints, then don't bother initializing
-- the type oracle, since it's redundant to do so.
-- * Since the new term constraint is a separate argument, we only need to
-- execute one iteration of the term oracle (instead of traversing the
-- entire set of term constraints).
pmIsSatisfiable
:: ComplexEq -- ^ The new term constraint.
-> TmState -- ^ The ambient term constraints (known to be satisfiable).
-> Bag EvVar -- ^ The new type constraints.
-> Bag EvVar -- ^ The ambient type constraints (known to be satisfiable).
-> PmM (Maybe (TmState, Bag EvVar))
-- ^ @'Just' (term_cs, ty_cs)@ if the constraints are
-- satisfiable, where @term_cs@ and @ty_cs@ are the new sets of
-- term and type constraints, respectively. 'Nothing' otherwise.
pmIsSatisfiable new_term_c amb_term_cs new_ty_cs amb_ty_cs = do
let ty_cs = new_ty_cs `unionBags` amb_ty_cs
sat_ty <- if isEmptyBag new_ty_cs
then pure True
else tyOracle ty_cs
pure $ case (sat_ty, solveOneEq amb_term_cs new_term_c) of
(True, Just term_cs) -> Just (term_cs, ty_cs)
_unsat -> Nothing
{- Note [Type normalisation for EmptyCase]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
EmptyCase is an exception for pattern matching, since it is strict. This means
......@@ -1544,14 +1607,8 @@ runMany pm (m:ms) = mappend <$> pm m <*> runMany pm ms
-- delta with all term and type constraints in scope.
mkInitialUncovered :: [Id] -> PmM Uncovered
mkInitialUncovered vars = do
ty_cs <- liftD getDictsDs
tm_cs <- map toComplex . bagToList <$> liftD getTmCsDs
sat_ty <- tyOracle ty_cs
let initTyCs = if sat_ty then ty_cs else emptyBag
initTmState = fromMaybe initialTmState (tmOracle initialTmState tm_cs)
patterns = map PmVar vars
-- If any of the term/type constraints are non
-- satisfiable then return with the initialTmState. See #12957
(initTmState, initTyCs) <- pmInitialTmTyCs
let patterns = map PmVar vars
return [ValVec patterns (MkDelta initTyCs initTmState)]
-- | Increase the counter for elapsed algorithm iterations, check that the
......@@ -1680,12 +1737,12 @@ pmcheckHd (p@(PmCon { pm_con_con = con, pm_con_arg_tys = tys }))
cons_cs <- mapM (liftD . mkOneConFull x) complete_match
inst_vsa <- flip concatMapM cons_cs $ \(va, tm_ct, ty_cs) -> do
let ty_state = ty_cs `unionBags` delta_ty_cs delta -- not actually a state
sat_ty <- if isEmptyBag ty_cs then return True
else tyOracle ty_state
return $ case (sat_ty, solveOneEq (delta_tm_cs delta) tm_ct) of
(True, Just tm_state) -> [ValVec (va:vva) (MkDelta ty_state tm_state)]
_ty_or_tm_failed -> []
mb_sat <- pmIsSatisfiable tm_ct (delta_tm_cs delta)
ty_cs (delta_ty_cs delta)
pure $ case mb_sat of
Just (tm_state, ty_state)
-> [ValVec (va:vva) (MkDelta ty_state tm_state)]
Nothing -> []
set_provenance prov .
force_if (canDiverge (idName x) (delta_tm_cs delta)) <$>
......
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE GADTs #-}
module T15450 where
f :: (Int ~ Bool) => Bool -> a
f x = case x of {}
g :: (Int ~ Bool) => Bool -> a
g x = case x of True -> undefined
T15450.hs:6:7: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In a case alternative:
Patterns not matched:
False
True
T15450.hs:9:7: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In a case alternative: Patterns not matched: False
......@@ -47,6 +47,8 @@ test('T14086', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T14098', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T15450', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
# Other tests
test('pmc001', [], compile,
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment