Exhaustiveness check for EmptyCase (Trac #10746)
authorGeorge Karachalias <george.karachalias@gmail.com>
Thu, 2 Feb 2017 18:51:33 +0000 (13:51 -0500)
committerBen Gamari <ben@smart-cactus.org>
Thu, 2 Feb 2017 19:20:45 +0000 (14:20 -0500)
Empty case expressions have strict semantics so the problem boils down
to inhabitation checking for the type of the scrutinee. 3 main functions
added:

- pmTopNormaliseType_maybe for the normalisation of the scrutinee type

- inhabitationCandidates for generating the possible patterns of the
  appropriate type

- checkEmptyCase' to filter out the candidates that give rise to
  unsatisfiable constraints.

See Note [Checking EmptyCase Expressions] in Check
and Note [Type normalisation for EmptyCase] in FamInstEnv

Test Plan: validate

Reviewers: simonpj, goldfire, dfeuer, austin, bgamari

Reviewed By: bgamari

Subscribers: mpickering, thomie

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

GHC Trac Issues: #10746

26 files changed:
compiler/deSugar/Check.hs
compiler/types/FamInstEnv.hs
compiler/types/Type.hs
testsuite/tests/pmcheck/should_compile/EmptyCase001.hs [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/EmptyCase001.stderr [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/EmptyCase002.hs [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/EmptyCase002.stderr [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/EmptyCase003.hs [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/EmptyCase003.stderr [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/EmptyCase004.hs [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/EmptyCase004.stderr [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/EmptyCase005.hs [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/EmptyCase005.stderr [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/EmptyCase006.hs [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/EmptyCase006.stderr [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/EmptyCase007.hs [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/EmptyCase007.stderr [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/EmptyCase008.hs [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/EmptyCase008.stderr [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/EmptyCase009.hs [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/EmptyCase009.stderr [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/EmptyCase010.hs [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/EmptyCase010.stderr [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/T10746.hs [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/T10746.stderr [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/all.T

index 80f7fa5..5fd1adf 100644 (file)
@@ -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 ()
index 40d2582..d23afad 100644 (file)
@@ -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
index 86d6eae..e13a1b9 100644 (file)
@@ -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 (file)
index 0000000..99e414d
--- /dev/null
@@ -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 (file)
index 0000000..ba9e61f
--- /dev/null
@@ -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 (file)
index 0000000..8af96be
--- /dev/null
@@ -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 (file)
index 0000000..8979fda
--- /dev/null
@@ -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 (file)
index 0000000..14f5c60
--- /dev/null
@@ -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 (file)
index 0000000..8db12ac
--- /dev/null
@@ -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 (file)
index 0000000..31ba020
--- /dev/null
@@ -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 (file)
index 0000000..1e002e1
--- /dev/null
@@ -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 (file)
index 0000000..b05dd9d
--- /dev/null
@@ -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 (file)
index 0000000..53be507
--- /dev/null
@@ -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 (file)
index 0000000..bf902b7
--- /dev/null
@@ -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 (file)
index 0000000..a1d372b
--- /dev/null
@@ -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 (file)
index 0000000..71a3d26
--- /dev/null
@@ -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 (file)
index 0000000..822baee
--- /dev/null
@@ -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 (file)
index 0000000..b1f6a0a
--- /dev/null
@@ -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 (file)
index 0000000..a13e61a
--- /dev/null
@@ -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 (file)
index 0000000..f6741b8
--- /dev/null
@@ -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 (file)
index 0000000..ab3fb0a
--- /dev/null
@@ -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 (file)
index 0000000..48b1a24
--- /dev/null
@@ -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 (file)
index 0000000..d4ccce3
--- /dev/null
@@ -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 (file)
index 0000000..8b06abc
--- /dev/null
@@ -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 (file)
index 0000000..9c0a196
--- /dev/null
@@ -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
index 3f4e0c8..f19e1de 100644 (file)
@@ -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'])