summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--compiler/deSugar/Check.hs194
-rw-r--r--compiler/types/FamInstEnv.hs114
-rw-r--r--compiler/types/Type.hs8
-rw-r--r--testsuite/tests/pmcheck/should_compile/EmptyCase001.hs18
-rw-r--r--testsuite/tests/pmcheck/should_compile/EmptyCase001.stderr14
-rw-r--r--testsuite/tests/pmcheck/should_compile/EmptyCase002.hs54
-rw-r--r--testsuite/tests/pmcheck/should_compile/EmptyCase002.stderr22
-rw-r--r--testsuite/tests/pmcheck/should_compile/EmptyCase003.hs95
-rw-r--r--testsuite/tests/pmcheck/should_compile/EmptyCase003.stderr11
-rw-r--r--testsuite/tests/pmcheck/should_compile/EmptyCase004.hs49
-rw-r--r--testsuite/tests/pmcheck/should_compile/EmptyCase004.stderr36
-rw-r--r--testsuite/tests/pmcheck/should_compile/EmptyCase005.hs101
-rw-r--r--testsuite/tests/pmcheck/should_compile/EmptyCase005.stderr32
-rw-r--r--testsuite/tests/pmcheck/should_compile/EmptyCase006.hs28
-rw-r--r--testsuite/tests/pmcheck/should_compile/EmptyCase006.stderr11
-rw-r--r--testsuite/tests/pmcheck/should_compile/EmptyCase007.hs46
-rw-r--r--testsuite/tests/pmcheck/should_compile/EmptyCase007.stderr26
-rw-r--r--testsuite/tests/pmcheck/should_compile/EmptyCase008.hs52
-rw-r--r--testsuite/tests/pmcheck/should_compile/EmptyCase008.stderr18
-rw-r--r--testsuite/tests/pmcheck/should_compile/EmptyCase009.hs40
-rw-r--r--testsuite/tests/pmcheck/should_compile/EmptyCase009.stderr11
-rw-r--r--testsuite/tests/pmcheck/should_compile/EmptyCase010.hs71
-rw-r--r--testsuite/tests/pmcheck/should_compile/EmptyCase010.stderr41
-rw-r--r--testsuite/tests/pmcheck/should_compile/T10746.hs25
-rw-r--r--testsuite/tests/pmcheck/should_compile/T10746.stderr6
-rw-r--r--testsuite/tests/pmcheck/should_compile/all.T24
26 files changed, 1128 insertions, 19 deletions
diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs
index 80f7fa50e3..5fd1adfa1b 100644
--- a/compiler/deSugar/Check.hs
+++ b/compiler/deSugar/Check.hs
@@ -108,10 +108,10 @@ getResult ls = do
-- Careful not to force unecessary results
go :: Maybe PmResult -> PmResult -> Maybe PmResult
go Nothing rs = Just rs
- go old@(Just (PmResult prov rs us is)) new
+ go old@(Just (PmResult prov rs (UncoveredPatterns us) is)) new
| null us && null rs && null is = old
| otherwise =
- let PmResult prov' rs' us' is' = new
+ let PmResult prov' rs' (UncoveredPatterns us') is' = new
lr = length rs
lr' = length rs'
li = length is
@@ -123,6 +123,8 @@ getResult ls = do
GT -> Just new
EQ -> Just new
LT -> old
+ go (Just (PmResult _ _ (TypeOfUncovered _) _)) _new
+ = panic "getResult: No inhabitation candidates"
data PatTy = PAT | VA -- Used only as a kind, to index PmPat
@@ -245,15 +247,43 @@ instance Monoid PartialResult where
-- | Pattern check result
--
-- * Redundant clauses
--- * Not-covered clauses
+-- * Not-covered clauses (or their type, if no pattern is available)
-- * Clauses with inaccessible RHS
+--
+-- More details about the classification of clauses into useful, redundant
+-- and with inaccessible right hand side can be found here:
+--
+-- https://ghc.haskell.org/trac/ghc/wiki/PatternMatchCheck
+--
data PmResult =
PmResult {
pmresultProvenance :: Provenance
, pmresultRedundant :: [Located [LPat Id]]
- , pmresultUncovered :: Uncovered
+ , pmresultUncovered :: UncoveredCandidates
, pmresultInaccessible :: [Located [LPat Id]] }
+-- | Either a list of patterns that are not covered, or their type, in case we
+-- have no patterns at hand. Not having patterns at hand can arise when
+-- handling EmptyCase expressions, in two cases:
+--
+-- * The type of the scrutinee is a trivially inhabited type (like Int or Char)
+-- * The type of the scrutinee cannot be reduced to WHNF.
+--
+-- In both these cases we have no inhabitation candidates for the type at hand,
+-- but we don't want to issue just a wildcard as missing. Instead, we print a
+-- type annotated wildcard, so that the user knows what kind of patterns is
+-- expected (e.g. (_ :: Int), or (_ :: F Int), where F Int does not reduce).
+data UncoveredCandidates = UncoveredPatterns Uncovered
+ | TypeOfUncovered Type
+
+-- | The empty pattern check result
+emptyPmResult :: PmResult
+emptyPmResult = PmResult FromBuiltin [] (UncoveredPatterns []) []
+
+-- | Non-exhaustive empty case with unknown/trivial inhabitants
+uncoveredWithTy :: Type -> PmResult
+uncoveredWithTy ty = PmResult FromBuiltin [] (TypeOfUncovered ty) []
+
{-
%************************************************************************
%* *
@@ -281,10 +311,11 @@ checkSingle' locn var p = do
tracePm "checkSingle: missing" (vcat (map pprValVecDebug missing))
-- no guards
PartialResult prov cs us ds <- runMany (pmcheckI clause []) missing
+ let us' = UncoveredPatterns us
return $ case (cs,ds) of
- (Covered, _ ) -> PmResult prov [] us [] -- useful
- (NotCovered, NotDiverged) -> PmResult prov m us [] -- redundant
- (NotCovered, Diverged ) -> PmResult prov [] us m -- inaccessible rhs
+ (Covered, _ ) -> PmResult prov [] us' [] -- useful
+ (NotCovered, NotDiverged) -> PmResult prov m us' [] -- redundant
+ (NotCovered, Diverged ) -> PmResult prov [] us' m -- inaccessible rhs
where m = [L locn [L locn p]]
-- | Check a matchgroup (case, functions, etc.)
@@ -296,22 +327,30 @@ checkMatches dflags ctxt vars matches = do
, text "Matches:"])
2
(vcat (map ppr matches)))
- mb_pm_res <- tryM (getResult (checkMatches' vars matches))
+ mb_pm_res <- tryM $ getResult $ case matches of
+ -- Check EmptyCase separately
+ -- See Note [Checking EmptyCase Expressions]
+ [] | [var] <- vars -> checkEmptyCase' var
+ _normal_match -> checkMatches' vars matches
case mb_pm_res of
Left _ -> warnPmIters dflags ctxt
Right res -> dsPmWarn dflags ctxt res
--- | Check a matchgroup (case, functions, etc.)
+-- | Check a matchgroup (case, functions, etc.). To be called on a non-empty
+-- list of matches. For empty case expressions, use checkEmptyCase' instead.
checkMatches' :: [Id] -> [LMatch Id (LHsExpr Id)] -> PmM PmResult
checkMatches' vars matches
- | null matches = return $ PmResult FromBuiltin [] [] []
+ | null matches = panic "checkMatches': EmptyCase"
| otherwise = do
liftD resetPmIterDs -- set the iter-no to zero
missing <- mkInitialUncovered vars
tracePm "checkMatches: missing" (vcat (map pprValVecDebug missing))
(prov, rs,us,ds) <- go matches missing
- return
- $ PmResult prov (map hsLMatchToLPats rs) us (map hsLMatchToLPats ds)
+ return $ PmResult {
+ pmresultProvenance = prov
+ , pmresultRedundant = map hsLMatchToLPats rs
+ , pmresultUncovered = UncoveredPatterns us
+ , pmresultInaccessible = map hsLMatchToLPats ds }
where
go :: [LMatch Id (LHsExpr Id)] -> Uncovered
-> PmM (Provenance
@@ -339,7 +378,113 @@ checkMatches' vars matches
hsLMatchToLPats :: LMatch id body -> Located [LPat id]
hsLMatchToLPats (L l (Match _ pats _ _)) = L l pats
-{-
+-- | Check an empty case expression. Since there are no clauses to process, we
+-- only compute the uncovered set. See Note [Checking EmptyCase Expressions]
+-- 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
+
+-- | Generate all inhabitation candidates for a given type. The result is
+-- either (Left ty), if the type cannot be reduced to a closed algebraic type
+-- (or if it's one trivially inhabited, like Int), or (Right candidates), if it
+-- can. In this case, the candidates are the singnature of the tycon, each one
+-- accompanied by the term- and type- constraints it gives rise to.
+-- See also Note [Checking EmptyCase Expressions]
+inhabitationCandidates :: FamInstEnvs -> Type
+ -> PmM (Either Type [(ValAbs, ComplexEq, Bag EvVar)])
+inhabitationCandidates fam_insts ty
+ = case pmTopNormaliseType_maybe fam_insts ty of
+ Just (src_ty, dcs, core_ty) -> alts_to_check src_ty core_ty dcs
+ Nothing -> alts_to_check ty ty []
+ where
+ -- All these types are trivially inhabited
+ trivially_inhabited = [ charTyCon, doubleTyCon, floatTyCon
+ , intTyCon, wordTyCon, word8TyCon ]
+
+ -- Note: At the moment we leave all the typing and constraint fields of
+ -- PmCon empty, since we know that they are not gonna be used. Is the
+ -- right-thing-to-do to actually create them, even if they are never used?
+ build_tm :: ValAbs -> [DataCon] -> ValAbs
+ build_tm = foldr (\dc e -> PmCon (RealDataCon dc) [] [] [] [e])
+
+ -- Inhabitation candidates, using the result of pmTopNormaliseType_maybe
+ alts_to_check :: Type -> Type -> [DataCon]
+ -> PmM (Either Type [(ValAbs, ComplexEq, Bag EvVar)])
+ alts_to_check src_ty core_ty dcs = case splitTyConApp_maybe core_ty of
+ Just (tc, _)
+ | tc `elem` trivially_inhabited -> case dcs of
+ [] -> return (Left src_ty)
+ (_:_) -> do var <- liftD $ mkPmId (toTcType core_ty)
+ let va = build_tm (PmVar var) dcs
+ return $ Right [(va, mkIdEq var, emptyBag)]
+ | isClosedAlgType core_ty -> liftD $ do
+ var <- mkPmId (toTcType core_ty) -- it would be wrong to unify x
+ alts <- mapM (mkOneConFull var . RealDataCon) (tyConDataCons tc)
+ return $ Right [(build_tm va dcs, eq, cs) | (va, eq, cs) <- alts]
+ -- For other types conservatively assume that they are inhabited.
+ _other -> return (Left src_ty)
+
+{- Note [Checking EmptyCase Expressions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Empty case expressions are strict on the scrutinee. That is, `case x of {}`
+will force argument `x`. Hence, `checkMatches` is not sufficient for checking
+empty cases, because it assumes that the match is not strict (which is true
+for all other cases, apart from EmptyCase). This gave rise to #10746. Instead,
+we do the following:
+
+1. We normalise the outermost type family redex, data family redex or newtype,
+ using pmTopNormaliseType_maybe (in types/FamInstEnv.hs). This computes 3
+ things:
+ (a) A normalised type src_ty, which is equal to the type of the scrutinee in
+ source Haskell (does not normalise newtypes or data families)
+ (b) The actual normalised type core_ty, which coincides with the result
+ topNormaliseType_maybe. This type is not necessarily equal to the input
+ type in source Haskell. And this is precicely the reason we compute (a)
+ and (c): the reasoning happens with the underlying types, but both the
+ patterns and types we print should respect newtypes and also show the
+ family type constructors and not the representation constructors.
+
+ (c) A list of all newtype data constructors dcs, each one corresponding to a
+ newtype rewrite performed in (b).
+
+ For an example see also Note [Type normalisation for EmptyCase]
+ in types/FamInstEnv.hs.
+
+2. Function checkEmptyCase' performs the check:
+ - If core_ty is not an algebraic type, then we cannot check for
+ inhabitation, so we emit (_ :: src_ty) as missing, conservatively assuming
+ that the type is inhabited.
+ - If core_ty is an algebraic type, then we unfold the scrutinee to all
+ possible constructor patterns, using inhabitationCandidates, and then
+ check each one for constraint satisfiability, same as we for normal
+ pattern match checking.
+
%************************************************************************
%* *
Transform source syntax to *our* syntax
@@ -868,6 +1013,13 @@ mkPosEq :: Id -> PmLit -> ComplexEq
mkPosEq x l = (PmExprVar (idName x), PmExprLit l)
{-# INLINE mkPosEq #-}
+-- | Create a term equality of the form: `(x ~ x)`
+-- (always discharged by the term oracle)
+mkIdEq :: Id -> ComplexEq
+mkIdEq x = (PmExprVar name, PmExprVar name)
+ where name = idName x
+{-# INLINE mkIdEq #-}
+
-- | Generate a variable pattern of a given type
mkPmVar :: Type -> DsM (PmPat p)
mkPmVar ty = PmVar <$> mkPmId ty
@@ -1457,15 +1609,20 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result
= when (flag_i || flag_u) $ do
let exists_r = flag_i && notNull redundant && onlyBuiltin
exists_i = flag_i && notNull inaccessible && onlyBuiltin
- exists_u = flag_u && notNull uncovered
+ exists_u = flag_u && (case uncovered of
+ TypeOfUncovered _ -> True
+ UncoveredPatterns u -> notNull u)
+
when exists_r $ forM_ redundant $ \(L l q) -> do
putSrcSpanDs l (warnDs (Reason Opt_WarnOverlappingPatterns)
(pprEqn q "is redundant"))
when exists_i $ forM_ inaccessible $ \(L l q) -> do
putSrcSpanDs l (warnDs (Reason Opt_WarnOverlappingPatterns)
(pprEqn q "has inaccessible right hand side"))
- when exists_u $
- putSrcSpanDs loc (warnDs flag_u_reason (pprEqns uncovered))
+ when exists_u $ putSrcSpanDs loc $ warnDs flag_u_reason $
+ case uncovered of
+ TypeOfUncovered ty -> warnEmptyCase ty
+ UncoveredPatterns candidates -> pprEqns candidates
where
PmResult
{ pmresultProvenance = prov
@@ -1494,6 +1651,11 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result
(vcat (take maxPatterns us)
$$ dots maxPatterns us)
+ -- Print a type-annotated wildcard (for non-exhaustive `EmptyCase`s for
+ -- which we only know the type and have no inhabitants at hand)
+ warnEmptyCase ty = pp_context False ctx (text "are non-exhaustive") $ \_ ->
+ hang (text "Patterns not matched:") 4 (underscore <+> dcolon <+> ppr ty)
+
-- | Issue a warning when the predefined number of iterations is exceeded
-- for the pattern match checker
warnPmIters :: DynFlags -> DsMatchContext -> DsM ()
diff --git a/compiler/types/FamInstEnv.hs b/compiler/types/FamInstEnv.hs
index 40d2582b47..d23afad401 100644
--- a/compiler/types/FamInstEnv.hs
+++ b/compiler/types/FamInstEnv.hs
@@ -31,6 +31,7 @@ module FamInstEnv (
topNormaliseType, topNormaliseType_maybe,
normaliseType, normaliseTcApp,
reduceTyFamApp_maybe,
+ pmTopNormaliseType_maybe,
-- Flattening
flattenTys
@@ -42,6 +43,7 @@ import Unify
import Type
import TyCoRep
import TyCon
+import DataCon (DataCon)
import Coercion
import CoAxiom
import VarSet
@@ -61,7 +63,7 @@ import FastString
import MonadUtils
import Control.Monad
import Data.Function ( on )
-import Data.List( mapAccumL )
+import Data.List( mapAccumL, find )
{-
************************************************************************
@@ -1232,7 +1234,7 @@ topNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe (Coercion, Type)
-- * data family redex
-- * newtypes
-- returning an appropriate Representational coercion. Specifically, if
--- topNormaliseType_maybe env ty = Maybe (co, ty')
+-- topNormaliseType_maybe env ty = Just (co, ty')
-- then
-- (a) co :: ty ~R ty'
-- (b) ty' is not a newtype, and is not a type-family or data-family redex
@@ -1258,6 +1260,114 @@ topNormaliseType_maybe env ty
_ -> NS_Done
---------------
+pmTopNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe (Type, [DataCon], Type)
+-- ^ Get rid of *outermost* (or toplevel)
+-- * type function redex
+-- * data family redex
+-- * newtypes
+--
+-- Behaves exactly like `topNormaliseType_maybe`, but instead of returning a
+-- coercion, it returns useful information for issuing pattern matching
+-- warnings. See Note [Type normalisation for EmptyCase] for details.
+pmTopNormaliseType_maybe env typ
+ = do ((ty_f,tm_f), ty) <- topNormaliseTypeX stepper comb typ
+ return (eq_src_ty ty (typ : ty_f [ty]), tm_f [], ty)
+ where
+ -- Find the first type in the sequence of rewrites that is a data type,
+ -- newtype, or a data family application (not the representation tycon!).
+ -- This is the one that is equal (in source Haskell) to the initial type.
+ -- If none is found in the list, then all of them are type family
+ -- applications, so we simply return the last one, which is the *simplest*.
+ eq_src_ty :: Type -> [Type] -> Type
+ eq_src_ty ty tys = maybe ty id (find is_alg_or_data_family tys)
+
+ is_alg_or_data_family :: Type -> Bool
+ is_alg_or_data_family ty = isClosedAlgType ty || isDataFamilyAppType ty
+
+ -- For efficiency, represent both lists as difference lists.
+ -- comb performs the concatenation, for both lists.
+ comb (tyf1, tmf1) (tyf2, tmf2) = (tyf1 . tyf2, tmf1 . tmf2)
+
+ stepper = newTypeStepper `composeSteppers` tyFamStepper
+
+ -- A 'NormaliseStepper' that unwraps newtypes, careful not to fall into
+ -- a loop. If it would fall into a loop, it produces 'NS_Abort'.
+ newTypeStepper :: NormaliseStepper ([Type] -> [Type],[DataCon] -> [DataCon])
+ newTypeStepper rec_nts tc tys
+ | Just (ty', _co) <- instNewTyCon_maybe tc tys
+ = case checkRecTc rec_nts tc of
+ Just rec_nts' -> let tyf = ((TyConApp tc tys):)
+ tmf = ((tyConSingleDataCon tc):)
+ in NS_Step rec_nts' ty' (tyf, tmf)
+ Nothing -> NS_Abort
+ | otherwise
+ = NS_Done
+
+ tyFamStepper :: NormaliseStepper ([Type] -> [Type], [DataCon] -> [DataCon])
+ tyFamStepper rec_nts tc tys -- Try to step a type/data familiy
+ = let (_args_co, ntys) = normaliseTcArgs env Representational tc tys in
+ -- NB: It's OK to use normaliseTcArgs here instead of
+ -- normalise_tc_args (which takes the LiftingContext described
+ -- in Note [Normalising types]) because the reduceTyFamApp below
+ -- works only at top level. We'll never recur in this function
+ -- after reducing the kind of a bound tyvar.
+
+ case reduceTyFamApp_maybe env Representational tc ntys of
+ Just (_co, rhs) -> NS_Step rec_nts rhs ((rhs:), id)
+ _ -> NS_Done
+
+{- Note [Type normalisation for EmptyCase]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+EmptyCase is an exception for pattern matching, since it is strict. This means
+that it boils down to checking whether the type of the scrutinee is inhabited.
+Function pmTopNormaliseType_maybe gets rid of the outermost type function/data
+family redex and newtypes, in search of an algebraic type constructor, which is
+easier to check for inhabitation.
+
+It returns 3 results instead of one, because there are 2 subtle points:
+1. Newtypes are isomorphic to the underlying type in core but not in the source
+ language,
+2. The representational data family tycon is used internally but should not be
+ shown to the user
+
+Hence, if pmTopNormaliseType_maybe env ty = Just (src_ty, dcs, core_ty), then
+ (a) src_ty is the rewritten type which we can show to the user. That is, the
+ type we get if we rewrite type families but not data families or
+ newtypes.
+ (b) dcs is the list of data constructors "skipped", every time we normalise a
+ newtype to it's core representation, we keep track of the source data
+ constructor.
+ (c) core_ty is the rewritten type. That is,
+ pmTopNormaliseType_maybe env ty = Just (src_ty, dcs, core_ty)
+ implies
+ topNormaliseType_maybe env ty = Just (co, core_ty)
+ for some coercion co.
+
+To see how all cases come into play, consider the following example:
+
+ data family T a :: *
+ data instance T Int = T1 | T2 Bool
+ -- Which gives rise to FC:
+ -- data T a
+ -- data R:TInt = T1 | T2 Bool
+ -- axiom ax_ti : T Int ~R R:TInt
+
+ newtype G1 = MkG1 (T Int)
+ newtype G2 = MkG2 G1
+
+ type instance F Int = F Char
+ type instance F Char = G2
+
+In this case pmTopNormaliseType_maybe env (F Int) results in
+
+ Just (G2, [MkG2,MkG1], R:TInt)
+
+Which means that in source Haskell:
+ - G2 is equivalent to F Int (in contrast, G1 isn't).
+ - if (x : R:TInt) then (MkG2 (MkG1 x) : F Int).
+-}
+
+---------------
normaliseTcApp :: FamInstEnvs -> Role -> TyCon -> [Type] -> (Coercion, Type)
-- See comments on normaliseType for the arguments of this function
normaliseTcApp env role tc tys
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 86d6eaecd0..e13a1b9695 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -107,7 +107,7 @@ module Type (
-- (Lifting and boxity)
isLiftedType_maybe, isUnliftedType, isUnboxedTupleType, isUnboxedSumType,
- isAlgType, isClosedAlgType,
+ isAlgType, isClosedAlgType, isDataFamilyAppType,
isPrimitiveType, isStrictType,
isRuntimeRepTy, isRuntimeRepVar, isRuntimeRepKindedTy,
dropRuntimeRepArgs,
@@ -1942,6 +1942,12 @@ isClosedAlgType ty
-> ASSERT2( ty_args `lengthIs` tyConArity tc, ppr ty ) True
_other -> False
+-- | Check whether a type is a data family type
+isDataFamilyAppType :: Type -> Bool
+isDataFamilyAppType ty = case tyConAppTyCon_maybe ty of
+ Just tc -> isDataFamilyTyCon tc
+ _ -> False
+
-- | Computes whether an argument (or let right hand side) should
-- be computed strictly or lazily, based only on its type.
-- Currently, it's just 'isUnliftedType'. Panics on levity-polymorphic types.
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase001.hs b/testsuite/tests/pmcheck/should_compile/EmptyCase001.hs
new file mode 100644
index 0000000000..99e414d357
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase001.hs
@@ -0,0 +1,18 @@
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+{-# LANGUAGE EmptyCase, LambdaCase #-}
+
+-- Check some predefined types
+module EmptyCase001 where
+
+-- Non-exhaustive with *infinite* inhabitants
+f1 :: Int -> a
+f1 = \case
+
+-- Non-exhaustive. Since a string is just a list of characters
+-- (that is, an algebraic type), we have [] and (_:_) as missing.
+f2 :: String -> a
+f2 x = case x of {}
+
+-- Non-exhaustive (do not unfold the alternatives)
+f3 :: Char -> a
+f3 x = case x of {}
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase001.stderr b/testsuite/tests/pmcheck/should_compile/EmptyCase001.stderr
new file mode 100644
index 0000000000..ba9e61fc51
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase001.stderr
@@ -0,0 +1,14 @@
+EmptyCase001.hs:9:6: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: _ :: Int
+
+EmptyCase001.hs:14:8: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative:
+ Patterns not matched:
+ []
+ (_:_)
+
+EmptyCase001.hs:18:8: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: _ :: Char
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase002.hs b/testsuite/tests/pmcheck/should_compile/EmptyCase002.hs
new file mode 100644
index 0000000000..8af96be77c
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase002.hs
@@ -0,0 +1,54 @@
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+{-# LANGUAGE EmptyCase, LambdaCase #-}
+{-# LANGUAGE GADTs, TypeFamilies #-}
+
+-- Check some newtypes, in combination with GADTs and TypeFamilies
+module EmptyCase002 where
+
+newtype T = MkT H
+newtype G = MkG T
+newtype H = MkH G
+
+-- Exhaustive but it cannot be detected.
+f1 :: T -> a
+f1 = \case
+
+data A
+
+data B = B1 | B2
+
+data C :: * -> * where
+ C1 :: C Int
+ C2 :: C Bool
+
+data D :: * -> * -> * where
+ D1 :: D Int Bool
+ D2 :: D Bool Char
+
+type family E (a :: *) :: * where
+ E Int = Bool
+ E Bool = Char
+
+newtype T1 a = MkT1 a
+newtype T2 b = MkT2 b
+
+-- Exhaustive
+f2 :: T1 A -> z
+f2 = \case
+
+-- Non-exhaustive. Missing cases: MkT1 B1, MkT1 B2
+f3 :: T1 B -> z
+f3 = \case
+
+-- Non-exhaustive. Missing cases: MkT1 False, MkT1 True
+f4 :: T1 (E Int) -> z
+f4 = \case
+
+-- Non-exhaustive. Missing cases: MkT1 (MkT2 (MkT1 D2))
+f5 :: T1 (T2 (T1 (D (E Int) (E (E Int))))) -> z
+f5 = \case
+
+-- Exhaustive. Not an EmptyCase but good to have for
+-- comparison with the example above
+f6 :: T1 (T2 (T1 (D (E Int) (E (E Int))))) -> ()
+f6 = \case MkT1 (MkT2 (MkT1 D2)) -> ()
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase002.stderr b/testsuite/tests/pmcheck/should_compile/EmptyCase002.stderr
new file mode 100644
index 0000000000..8979fda155
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase002.stderr
@@ -0,0 +1,22 @@
+EmptyCase002.hs:14:6: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: (MkT _)
+
+EmptyCase002.hs:41:6: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative:
+ Patterns not matched:
+ (MkT1 B1)
+ (MkT1 B2)
+
+EmptyCase002.hs:45:6: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative:
+ Patterns not matched:
+ (MkT1 False)
+ (MkT1 True)
+
+EmptyCase002.hs:49:6: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative:
+ Patterns not matched: (MkT1 (MkT2 (MkT1 D2)))
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase003.hs b/testsuite/tests/pmcheck/should_compile/EmptyCase003.hs
new file mode 100644
index 0000000000..14f5c60747
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase003.hs
@@ -0,0 +1,95 @@
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+{-# LANGUAGE EmptyCase, LambdaCase #-}
+{-# LANGUAGE TypeFamilies, UndecidableInstances #-}
+
+-- Check some type families and type synonyms
+module EmptyCase003 where
+
+type family A (a :: *) :: *
+
+-- Conservatively considered non-exhaustive (A a missing),
+-- since A a does not reduce to anything.
+f1 :: A a -> a -> b
+f1 = \case
+
+data Void
+
+type family B (a :: *) :: *
+type instance B a = Void
+
+-- Exhaustive
+f2 :: B a -> b
+f2 = \case
+
+type family C (a :: *) :: *
+type instance C Int = Char
+type instance C Bool = Void
+
+-- Non-exhaustive (C a missing, no info about `a`)
+f3 :: C a -> a -> b
+f3 = \case
+
+-- Non-exhaustive (_ :: Char missing): C Int rewrites
+-- to Char (which is trivially inhabited)
+f4 :: C Int -> a
+f4 = \case
+
+-- Exhaustive: C Bool rewrites to Void
+f5 :: C Bool -> a
+f5 = \case
+
+-- type family D (a :: *) :: *
+-- type instance D x = D x -- non-terminating
+--
+-- -- Exhaustive but *impossible* to detect that, since rewriting
+-- -- D Int does not terminate (the checker should loop).
+-- f6 :: D Int -> a
+-- f6 = \case
+
+data Zero
+data Succ n
+
+type TenC n = Succ (Succ (Succ (Succ (Succ
+ (Succ (Succ (Succ (Succ (Succ n)))))))))
+
+type Ten = TenC Zero
+
+type Hundred = TenC (TenC (TenC (TenC (TenC
+ (TenC (TenC (TenC (TenC (TenC Zero)))))))))
+
+type family E (n :: *) (a :: *) :: *
+type instance E Zero b = b
+type instance E (Succ n) b = E n b
+
+-- Exhaustive (10 rewrites)
+f7 :: E Ten Void -> b
+f7 = \case
+
+-- Exhaustive (100 rewrites)
+f8 :: E Hundred Void -> b
+f8 = \case
+
+type family Add (a :: *) (b :: *) :: *
+type instance Add Zero m = m
+type instance Add (Succ n) m = Succ (Add n m)
+
+type family Mult (a :: *) (b :: *) :: *
+type instance Mult Zero m = Zero
+type instance Mult (Succ n) m = Add m (Mult n m)
+
+type Five = Succ (Succ (Succ (Succ (Succ Zero))))
+type Four = Succ (Succ (Succ (Succ Zero)))
+
+-- Exhaustive (80 rewrites)
+f9 :: E (Mult Four (Mult Four Five)) Void -> a
+f9 = \case
+
+-- This gets killed on my dell
+--
+-- -- Exhaustive (390625 rewrites)
+-- f10 :: E (Mult (Mult (Mult Five Five)
+-- (Mult Five Five))
+-- (Mult (Mult Five Five)
+-- (Mult Five Five)))
+-- Void -> a
+-- f10 = \case
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase003.stderr b/testsuite/tests/pmcheck/should_compile/EmptyCase003.stderr
new file mode 100644
index 0000000000..8db12ac5b5
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase003.stderr
@@ -0,0 +1,11 @@
+EmptyCase003.hs:13:6: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: _ :: A a
+
+EmptyCase003.hs:30:6: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: _ :: C a
+
+EmptyCase003.hs:35:6: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: _ :: Char
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase004.hs b/testsuite/tests/pmcheck/should_compile/EmptyCase004.hs
new file mode 100644
index 0000000000..31ba020c33
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase004.hs
@@ -0,0 +1,49 @@
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+{-# LANGUAGE GADTs, KindSignatures, EmptyCase, LambdaCase #-}
+
+-- Check some GADTs
+module EmptyCase004 where
+
+data A :: * -> * where
+ A1 :: A Int
+ A2 :: A Bool
+
+-- Non-exhaustive: Missing A2
+f1 :: A Bool -> a
+f1 = \case
+
+-- Non-exhaustive: missing both A1 & A2
+f2 :: A a -> b
+f2 = \case
+
+-- Exhaustive
+f3 :: A [a] -> b
+f3 = \case
+
+data B :: * -> * -> * where
+ B1 :: Int -> B Bool Bool
+ B2 :: B Int Bool
+
+-- Non-exhaustive: missing (B1 _)
+g1 :: B a a -> b
+g1 x = case x of
+
+-- Non-exhaustive: missing both (B1 _) & B2
+g2 :: B a b -> c
+g2 = \case
+
+-- Exhaustive
+g3 :: B Char a -> b
+g3 = \case
+
+-- NOTE: A lambda-case always has ONE scrutinee and a lambda case refers
+-- always to the first of the arguments. Hence, the following warnings are
+-- valid:
+
+-- Non-exhaustive: Missing both A1 & A2
+h1 :: A a -> A a -> b
+h1 = \case
+
+h2 :: A a -> B a b -> ()
+h2 A1 = \case -- Non-exhaustive, missing B2
+h2 A2 = \case -- Non-exhaustive, missing (B1 _)
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase004.stderr b/testsuite/tests/pmcheck/should_compile/EmptyCase004.stderr
new file mode 100644
index 0000000000..1e002e18c5
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase004.stderr
@@ -0,0 +1,36 @@
+EmptyCase004.hs:13:6: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: A2
+
+EmptyCase004.hs:17:6: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative:
+ Patterns not matched:
+ A1
+ A2
+
+EmptyCase004.hs:29:8: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: (B1 _)
+
+EmptyCase004.hs:33:6: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative:
+ Patterns not matched:
+ (B1 _)
+ B2
+
+EmptyCase004.hs:45:6: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative:
+ Patterns not matched:
+ A1
+ A2
+
+EmptyCase004.hs:48:9: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: B2
+
+EmptyCase004.hs:49:9: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: (B1 _)
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase005.hs b/testsuite/tests/pmcheck/should_compile/EmptyCase005.hs
new file mode 100644
index 0000000000..b05dd9d4af
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase005.hs
@@ -0,0 +1,101 @@
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+{-# LANGUAGE TypeFamilies, EmptyCase, LambdaCase #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- Check some DataFamilies, warning appearance and other stuff
+module EmptyCase005 where
+
+data Void
+
+newtype Void2 = Void2 Void
+data Void3 = Void3 Void
+
+-- Exhaustive
+f1 :: Void2 -> Bool
+f1 x = case x of {}
+-- > f1 undefined
+-- *** Exception: Prelude.undefined
+--
+-- > f1 (Void2 undefined)
+-- *** Exception: Prelude.undefined
+
+-- Non-exhaustive: missing (Void3 _)
+f2 :: Void3 -> Bool
+f2 x = case x of {}
+-- > f2 undefined
+-- *** Exception: Prelude.undefined
+--
+-- > f2 (Void3 undefined)
+-- *** Exception: Void.hs:31:7-10: Non-exhaustive patterns in case
+
+newtype V1 = V1 Void
+newtype V2 = V2 V1
+newtype V3 = V3 V2
+newtype V4 = V4 V3
+
+-- Exhaustive
+f3 :: V4 -> Bool
+f3 x = case x of {}
+-- > v undefined
+-- *** Exception: Prelude.undefined
+--
+-- > v (V4 undefined)
+-- *** Exception: Prelude.undefined
+--
+-- > v (V4 (V3 undefined))
+-- *** Exception: Prelude.undefined
+--
+-- > v (V4 (V3 (V2 undefined)))
+-- *** Exception: Prelude.undefined
+--
+-- > v (V4 (V3 (V2 (V1 undefined))))
+-- *** Exception: Prelude.undefined
+
+-- Exhaustive
+type family A a
+type instance A Bool = V4
+
+f4 :: A Bool -> Bool
+f4 x = case x of {}
+
+data family T a
+
+data instance T () = T1 | T2
+
+-- Non-exhaustive: missing both T1 & T2
+f5 :: T () -> Bool
+f5 x = case x of {}
+
+newtype instance T Bool = MkTBool Bool
+
+-- Non-exhaustive: missing both (MkTBool True) & (MkTBool False)
+f6 :: T Bool -> Bool
+f6 x = case x of {}
+
+newtype instance T Int = MkTInt Char
+
+-- Non-exhaustive: missing (MkTInt _)
+f7 :: T Int -> Bool
+f7 x = case x of {}
+
+newtype V = MkV Bool
+
+type family F a
+type instance F Bool = V
+
+type family G a
+type instance G Int = F Bool
+
+-- Non-exhaustive: missing MkV True & MkV False
+f8 :: G Int -> Bool
+f8 x = case x of {}
+
+type family H a
+type instance H Int = H Bool
+type instance H Bool = H Char
+
+-- Non-exhaustive: missing (_ :: H Char)
+-- (H Int), (H Bool) and (H Char) are all the same and stuck, but we want to
+-- show the latest rewrite, that is, (H Char) and not (H Int) or (H Bool).
+f9 :: H Int -> Bool
+f9 x = case x of {}
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase005.stderr b/testsuite/tests/pmcheck/should_compile/EmptyCase005.stderr
new file mode 100644
index 0000000000..53be507400
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase005.stderr
@@ -0,0 +1,32 @@
+EmptyCase005.hs:24:8: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: (Void3 _)
+
+EmptyCase005.hs:67:8: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative:
+ Patterns not matched:
+ T1
+ T2
+
+EmptyCase005.hs:73:8: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative:
+ Patterns not matched:
+ (MkTBool False)
+ (MkTBool True)
+
+EmptyCase005.hs:79:8: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: (MkTInt _)
+
+EmptyCase005.hs:91:8: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative:
+ Patterns not matched:
+ (MkV False)
+ (MkV True)
+
+EmptyCase005.hs:101:8: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: _ :: H Char
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase006.hs b/testsuite/tests/pmcheck/should_compile/EmptyCase006.hs
new file mode 100644
index 0000000000..bf902b766d
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase006.hs
@@ -0,0 +1,28 @@
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+{-# LANGUAGE GADTs, KindSignatures, EmptyCase, LambdaCase #-}
+
+-- Check interaction between Newtypes and GADTs
+module EmptyCase006 where
+
+data GA :: * -> * where
+ MkGA1 :: GA Int
+ MkGA2 :: GA a -> GA [a]
+ MkGA3 :: GA (a,a)
+
+newtype Foo1 a = Foo1 (GA a)
+
+-- Non-exhaustive. Missing: Foo1 MkGA1
+f01 :: Foo1 Int -> ()
+f01 = \case
+
+-- Exhaustive
+f02 :: Foo1 (Int, Bool) -> ()
+f02 = \case
+
+-- Non-exhaustive. Missing: Foo1 MkGA1, Foo1 (MkGA2 _), Foo1 MkGA3
+f03 :: Foo1 a -> ()
+f03 = \case
+
+-- Exhaustive
+f04 :: Foo1 () -> ()
+f04 = \case
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase006.stderr b/testsuite/tests/pmcheck/should_compile/EmptyCase006.stderr
new file mode 100644
index 0000000000..a1d372b14f
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase006.stderr
@@ -0,0 +1,11 @@
+EmptyCase006.hs:16:7: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: (Foo1 MkGA1)
+
+EmptyCase006.hs:24:7: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative:
+ Patterns not matched:
+ (Foo1 MkGA1)
+ (Foo1 (MkGA2 _))
+ (Foo1 MkGA3)
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase007.hs b/testsuite/tests/pmcheck/should_compile/EmptyCase007.hs
new file mode 100644
index 0000000000..71a3d2606c
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase007.hs
@@ -0,0 +1,46 @@
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+{-# LANGUAGE TypeFamilies, EmptyCase, LambdaCase #-}
+
+-- Check interaction between Newtypes and Type Families
+module EmptyCase007 where
+
+type family FA a :: * -- just an open type family
+type instance FA Int = (Char, Bool)
+type instance FA Char = Char
+type instance FA [a] = [FA a]
+type instance FA (a,b,b) = Void1
+
+newtype Foo2 a = Foo2 (FA a)
+
+data Void1
+
+-- Non-exhaustive. Missing: (_ :: Foo2 a) (no info about a)
+f05 :: Foo2 a -> ()
+f05 = \case
+
+-- Non-exhaustive. Missing: (_ :: Foo2 (a, a)) (does not reduce)
+f06 :: Foo2 (a, a) -> ()
+f06 = \case
+
+-- Exhaustive (reduces to Void)
+f07 :: Foo2 (Int, Char, Char) -> ()
+f07 = \case
+
+-- Non-exhaustive. Missing: Foo2 (_, _)
+f08 :: Foo2 Int -> ()
+f08 = \case
+
+-- Non-exhaustive. Missing: Foo2 _
+f09 :: Foo2 Char -> ()
+f09 = \case
+
+-- Non-exhaustive. Missing: (_ :: Char)
+-- This is a more general trick: If the warning gives you a constructor form
+-- and you don't know what the type of the underscore is, just match against
+-- the constructor form, and the warning you'll get will fill the type in.
+f09' :: Foo2 Char -> ()
+f09' (Foo2 x) = case x of {}
+
+-- Non-exhaustive. Missing: Foo2 [], Foo2 (_:_)
+f10 :: Foo2 [Int] -> ()
+f10 = \case
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase007.stderr b/testsuite/tests/pmcheck/should_compile/EmptyCase007.stderr
new file mode 100644
index 0000000000..822baee3bb
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase007.stderr
@@ -0,0 +1,26 @@
+EmptyCase007.hs:19:7: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: _ :: Foo2 a
+
+EmptyCase007.hs:23:7: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: _ :: Foo2 (a, a)
+
+EmptyCase007.hs:31:7: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: (Foo2 (_, _))
+
+EmptyCase007.hs:35:7: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: (Foo2 _)
+
+EmptyCase007.hs:42:17: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: _ :: Char
+
+EmptyCase007.hs:46:7: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative:
+ Patterns not matched:
+ (Foo2 [])
+ (Foo2 (_:_))
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase008.hs b/testsuite/tests/pmcheck/should_compile/EmptyCase008.hs
new file mode 100644
index 0000000000..b1f6a0ae73
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase008.hs
@@ -0,0 +1,52 @@
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+{-# LANGUAGE TypeFamilies, GADTs, EmptyCase, LambdaCase #-}
+
+-- Check interaction between Newtypes and DataFamilies
+module EmptyCase008 where
+
+data family DA a
+
+newtype Foo3 a = Foo3 (DA a)
+
+data instance DA Int = MkDA1 Char | MkDA2
+
+-- Non-exhaustive. Missing: MkDA1 Char, MkDA2
+f11 :: Foo3 Int -> ()
+f11 = \case
+
+-- Non-exhaustive. (no info about a)
+f12 :: Foo3 a -> ()
+f12 = \case
+
+data instance DA () -- Empty data type
+
+-- Exhaustive.
+f13 :: Foo3 () -> ()
+f13 = \case
+
+-- ----------------
+data family DB a :: * -> *
+
+data instance DB Int a where
+ MkDB1 :: DB Int ()
+ MkDB2 :: DB Int Bool
+
+newtype Foo4 a b = Foo4 (DB a b)
+
+-- Non-exhaustive. Missing: Foo4 MkDB1
+f14 :: Foo4 Int () -> ()
+f14 = \case
+
+-- Exhaustive
+f15 :: Foo4 Int [a] -> ()
+f15 = \case
+
+-- Non-exhaustive. Missing: (_ :: Foo4 a b) (no information about a or b)
+f16 :: Foo4 a b -> ()
+f16 = \case
+
+data instance DB Char Bool -- Empty data type
+
+-- Exhaustive (empty data type)
+f17 :: Foo4 Char Bool -> ()
+f17 = \case
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase008.stderr b/testsuite/tests/pmcheck/should_compile/EmptyCase008.stderr
new file mode 100644
index 0000000000..a13e61aa67
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase008.stderr
@@ -0,0 +1,18 @@
+EmptyCase008.hs:15:7: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative:
+ Patterns not matched:
+ (Foo3 (MkDA1 _))
+ (Foo3 MkDA2)
+
+EmptyCase008.hs:19:7: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: _ :: Foo3 a
+
+EmptyCase008.hs:38:7: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: (Foo4 MkDB1)
+
+EmptyCase008.hs:46:7: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: _ :: Foo4 a b
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase009.hs b/testsuite/tests/pmcheck/should_compile/EmptyCase009.hs
new file mode 100644
index 0000000000..f6741b88c8
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase009.hs
@@ -0,0 +1,40 @@
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+{-# LANGUAGE TypeFamilies, GADTs, EmptyCase, LambdaCase #-}
+
+-- Arrow Kind, Newtypes, GADTs, DataFamilies
+module EmptyCase009 where
+
+data family DB a :: * -> *
+
+data instance DB Int a where
+ MkDB1 :: DB Int ()
+ MkDB2 :: DB Int Bool
+
+data instance DB Char Bool -- Empty data type
+
+newtype Bar f = Bar (f Int)
+
+-- Non-exhaustive. Missing: (_ :: Bar f)
+f17 :: Bar f -> ()
+f17 x = case x of {}
+
+-- Exhaustive (Bar (DB Int) ~ DB Int Int, incompatible with both MkDB1 & MkDB2)
+f18 :: Bar (DB Int) -> ()
+f18 x = case x of {}
+
+data instance DB () a where
+ MkDB1_u :: DB () ()
+ MkDB2_u :: DB () Int
+
+-- Non-exhaustive. Missing: Bar MkDB2_u
+f19 :: Bar (DB ()) -> ()
+f19 = \case
+
+data GB :: * -> * where
+ MkGB1 :: Int -> GB ()
+ MkGB2 :: GB (a,a)
+ MkGB3 :: GB b
+
+-- Non-exhaustive. Missing: Bar MkGB3
+f20 :: Bar GB -> ()
+f20 = \case
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase009.stderr b/testsuite/tests/pmcheck/should_compile/EmptyCase009.stderr
new file mode 100644
index 0000000000..ab3fb0a45f
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase009.stderr
@@ -0,0 +1,11 @@
+EmptyCase009.hs:19:9: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: _ :: Bar f
+
+EmptyCase009.hs:31:7: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: (Bar MkDB2_u)
+
+EmptyCase009.hs:40:7: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: (Bar MkGB3)
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase010.hs b/testsuite/tests/pmcheck/should_compile/EmptyCase010.hs
new file mode 100644
index 0000000000..48b1a247b8
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase010.hs
@@ -0,0 +1,71 @@
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+{-# LANGUAGE TypeFamilies, GADTs, PolyKinds, DataKinds
+ , EmptyCase, LambdaCase #-}
+
+-- Newtypes, PolyKinds, DataKinds, GADTs, DataFamilies
+module EmptyCase010 where
+
+newtype Baz (f :: k -> *) (a :: k) = Baz (f a)
+
+data T = T1 | T2 T | T3 T T | T4 () -- only promoted
+
+data GC :: T -> * where
+ MkGC1 :: GC 'T1
+ MkGC2 :: T -> GC (T4 '())
+
+-- Exhaustive: GC ('T2 'T1) is not strictly inhabited
+f21 :: Baz GC ('T2 'T1) -> ()
+f21 = \case
+
+-- Non-exhaustive. Missing: Baz MkGC1, Baz (MkGC2 _)
+f22 :: Baz GC a -> ()
+f22 = \case
+
+-- Non-exhaustive. Missing: Baz MkGC1
+f23 :: Baz GC 'T1 -> ()
+f23 = \case
+
+data GD :: (* -> *) -> * where
+ MkGD1 :: GD Maybe
+ MkGD2 :: GD []
+ MkGD3 :: GD f
+
+-- Non-exhaustive. Missing: Baz MkGD1, Baz MkGD3
+f24 :: Baz GD Maybe -> ()
+f24 = \case
+
+-- Non-exhaustive. Missing: Baz MkGD3
+f25 :: Baz GD (Either Int) -> ()
+f25 x = case x of {}
+
+-- Non-exhaustive. Missing: Baz MkGD1, Baz MkGD2, Baz MkGD3
+f26 :: Baz GD f -> ()
+f26 = \case
+
+data family DC a :: * -> *
+
+data instance DC () Int -- Empty type
+
+-- Exhaustive
+f27 :: Baz (DC ()) Int -> ()
+f27 = \case
+
+-- Non-exhaustive. Missing: _ :: Baz (DC ()) a (a is unknown)
+f28 :: Baz (DC ()) a -> ()
+f28 = \case
+
+data instance DC Bool a where
+ MkDC1 :: DC Bool Int
+ MkDC2 :: DC Bool [a]
+
+-- Exhaustive. (DC Bool Char) is not strictly inhabited
+f29 :: Baz (DC Bool) Char -> ()
+f29 = \case
+
+-- Non-exhaustive. Missing: Baz MkDC2
+f30 :: Baz (DC Bool) [Int] -> ()
+f30 = \case
+
+-- Non-exhaustive. Missing: Baz f a (a and f unknown (and the kind too))
+f31 :: Baz f a -> ()
+f31 x = case x of {}
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase010.stderr b/testsuite/tests/pmcheck/should_compile/EmptyCase010.stderr
new file mode 100644
index 0000000000..d4ccce34bb
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase010.stderr
@@ -0,0 +1,41 @@
+EmptyCase010.hs:22:7: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative:
+ Patterns not matched:
+ (Baz MkGC1)
+ (Baz (MkGC2 _))
+
+EmptyCase010.hs:26:7: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: (Baz MkGC1)
+
+EmptyCase010.hs:35:7: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative:
+ Patterns not matched:
+ (Baz MkGD1)
+ (Baz MkGD3)
+
+EmptyCase010.hs:39:9: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: (Baz MkGD3)
+
+EmptyCase010.hs:43:7: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative:
+ Patterns not matched:
+ (Baz MkGD1)
+ (Baz MkGD2)
+ (Baz MkGD3)
+
+EmptyCase010.hs:55:7: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: _ :: Baz (DC ()) a
+
+EmptyCase010.hs:67:7: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: (Baz MkDC2)
+
+EmptyCase010.hs:71:9: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: _ :: Baz f a
diff --git a/testsuite/tests/pmcheck/should_compile/T10746.hs b/testsuite/tests/pmcheck/should_compile/T10746.hs
new file mode 100644
index 0000000000..8b06abcde8
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T10746.hs
@@ -0,0 +1,25 @@
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE GADTs, DataKinds #-}
+
+module Test where
+
+-- Non-exhaustive (missing True & False)
+test :: Bool -> Int
+test a = case a of
+
+data Void
+
+-- Exhaustive
+absurd :: Void -> a
+absurd a = case a of {}
+
+data Nat = Zero | Succ Nat
+
+data Fin n where
+ FZ :: Fin (Succ n)
+ FS :: Fin n -> Fin (Succ n)
+
+-- Exhaustive
+f :: Fin Zero -> a
+f x = case x of {}
diff --git a/testsuite/tests/pmcheck/should_compile/T10746.stderr b/testsuite/tests/pmcheck/should_compile/T10746.stderr
new file mode 100644
index 0000000000..9c0a196a08
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T10746.stderr
@@ -0,0 +1,6 @@
+T10746.hs:9:10: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative:
+ Patterns not matched:
+ False
+ True
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index 3f4e0c8af8..f19e1deedf 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -59,3 +59,27 @@ test('pmc007', [], compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T11245', [], compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+
+# EmptyCase
+test('T10746', [], compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('EmptyCase001', [], compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('EmptyCase002', [], compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('EmptyCase003', [], compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('EmptyCase004', [], compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('EmptyCase005', [], compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('EmptyCase006', [], compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('EmptyCase007', [], compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('EmptyCase008', [], compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('EmptyCase009', [], compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('EmptyCase010', [], compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])