Overhaul the Overhauled Pattern Match Checker
authorGeorge Karachalias <george.karachalias@gmail.com>
Wed, 3 Feb 2016 18:06:45 +0000 (19:06 +0100)
committerBen Gamari <ben@smart-cactus.org>
Thu, 4 Feb 2016 09:27:36 +0000 (10:27 +0100)
Overhaul the Overhauled Pattern Match Checker

* Changed the representation of Value Set Abstractions. Instead of
using a prefix tree, we now use a list of Value Vector Abstractions.
The set of constraints Delta for every Value Vector Abstraction is the
oracle state so that we solve everything only once.

* Instead of doing everything lazily, we prune at once (and in general
everything is much stricter). Hence, an example written with pattern
guards is checked in almost the same time as the equivalent with
pattern matching.

* Do not store the covered and the divergent sets at all. Since what we
only need is a yes/no (does this clause cover anything? Does it force
any thunk?) We just keep a boolean for each.

* Removed flags `-Wtoo-many-guards` and `-ffull-guard-reasoning`.
Replaced with `fmax-pmcheck-iterations=n`. Still debatable what should
the default `n` be.

* When a guard is for sure not going to contribute anything, we treat
it as such: The oracle is not called and cases `CGuard`, `UGuard` and
`DGuard` from the paper are not happening at all (the generation of a
fresh variable, the unfolding of the pattern list etc.). his combined
with the above seems to be enough to drop the memory increase for test
T783 down to 18.7%.

* Do not export function `dsPmWarn` (it is now called directly from
within `checkSingle` and `checkMatches`).

* Make `PmExprVar` hold a `Name` instead of an `Id`. The term oracle
does not handle type information so using `Id` was a waste of
time/space.

* Added testcases T11195, T11303b (data families) and T11374

The patch addresses at least the following:
Trac #11195, #11276, #11303, #11374, #11162

Test Plan: validate

Reviewers: goldfire, bgamari, hvr, austin

Subscribers: simonpj, thomie

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

24 files changed:
compiler/deSugar/Check.hs
compiler/deSugar/DsMonad.hs
compiler/deSugar/Match.hs
compiler/deSugar/PmExpr.hs
compiler/deSugar/TmOracle.hs
compiler/ghci/RtClosureInspect.hs
compiler/main/DynFlags.hs
compiler/nativeGen/Dwarf/Constants.hs
compiler/typecheck/TcRnTypes.hs
compiler/types/OptCoercion.hs
docs/users_guide/8.0.1-notes.rst
docs/users_guide/bugs.rst
docs/users_guide/using-warnings.rst
libraries/base/Foreign/C/Error.hs
testsuite/tests/perf/compiler/all.T
testsuite/tests/pmcheck/should_compile/T11195.hs [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/T11303b.hs [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/T11374.hs [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/T2204.stderr
testsuite/tests/pmcheck/should_compile/T9951b.stderr
testsuite/tests/pmcheck/should_compile/all.T
testsuite/tests/pmcheck/should_compile/pmc001.stderr
testsuite/tests/pmcheck/should_compile/pmc007.stderr
utils/mkUserGuidePart/Options/Warnings.hs

index 043b4f2..a28e39e 100644 (file)
@@ -7,14 +7,8 @@ Pattern Matching Coverage Checking.
 {-# LANGUAGE CPP, GADTs, DataKinds, KindSignatures #-}
 
 module Check (
-        -- Actual check and pretty printing
-        checkSingle, checkMatches, dsPmWarn,
-
-        -- Check for exponential explosion due to guards
-        computeNoGuards,
-        isAnyPmCheckEnabled,
-        warnManyGuards,
-        maximum_failing_guards,
+        -- Checking and printing
+        checkSingle, checkMatches, isAnyPmCheckEnabled,
 
         -- See Note [Type and Term Equality Propagation]
         genCaseTmCs1, genCaseTmCs2
@@ -55,6 +49,7 @@ import Data.Maybe    -- isNothing, isJust, fromJust
 import Control.Monad -- liftM3, forM
 import Coercion
 import TcEvidence
+import IOEnv
 
 {-
 This module checks pattern matches for:
@@ -64,7 +59,7 @@ This module checks pattern matches for:
   \item Exhaustiveness
 \end{enumerate}
 
-The algorithm used is described in the paper:
+The algorithm is based on the paper:
 
   "GADTs Meet Their Match:
      Pattern-matching Warnings That Account for GADTs, Guards, and Laziness"
@@ -80,11 +75,6 @@ The algorithm used is described in the paper:
 
 type PmM a = DsM a
 
-data PmConstraint = TmConstraint PmExpr PmExpr -- ^ Term equalities: e ~ e
-                    -- See Note [Representation of Term Equalities]
-                  | TyConstraint [EvVar]   -- ^ Type equalities
-                  | BtConstraint Id        -- ^ Strictness constraints: x ~ _|_
-
 data PatTy = PAT | VA -- Used only as a kind, to index PmPat
 
 -- The *arity* of a PatVec [p1,..,pn] is
@@ -99,10 +89,10 @@ data PmPat :: PatTy -> * where
             -- For PmCon arguments' meaning see @ConPatOut@ in hsSyn/HsPat.hs
   PmVar  :: { pm_var_id   :: Id    } -> PmPat t
   PmLit  :: { pm_lit_lit  :: PmLit } -> PmPat t -- See Note [Literals in PmPat]
-  PmNLit :: { pm_lit_id :: Id
-            , pm_lit_not :: [PmLit] } -> PmPat 'VA
+  PmNLit :: { pm_lit_id   :: Id
+            , pm_lit_not  :: [PmLit] } -> PmPat 'VA
   PmGrd  :: { pm_grd_pv   :: PatVec
-            , pm_grd_expr :: PmExpr } -> PmPat 'PAT
+            , pm_grd_expr :: PmExpr  } -> PmPat 'PAT
 
 -- data T a where
 --     MkT :: forall p q. (Eq p, Ord q) => p -> q -> T [p]
@@ -111,31 +101,36 @@ data PmPat :: PatTy -> * where
 type Pattern = PmPat 'PAT -- ^ Patterns
 type ValAbs  = PmPat 'VA  -- ^ Value Abstractions
 
-type PatVec    = [Pattern] -- Pattern Vectors
-type ValVecAbs = [ValAbs]  -- Value Vector Abstractions
-
-data ValSetAbs   -- Reprsents a set of value vector abstractions
-                 -- Notionally each value vector abstraction is a triple:
-                 --   (Gamma |- us |> Delta)
-                 -- where 'us'    is a ValueVec
-                 --       'Delta' is a constraint
-  -- INVARIANT VsaInvariant: an empty ValSetAbs is always represented by Empty
-  -- INVARIANT VsaArity: the number of Cons's in any path to a leaf is the same
-  -- The *arity* of a ValSetAbs is the number of Cons's in any path to a leaf
-  = Empty                               -- ^ {}
-  | Union ValSetAbs ValSetAbs           -- ^ S1 u S2
-  | Singleton                           -- ^ { |- empty |> empty }
-  | Constraint [PmConstraint] ValSetAbs -- ^ Extend Delta
-  | Cons ValAbs ValSetAbs               -- ^ map (ucon u) vs
+type PatVec = [Pattern]             -- ^ Pattern Vectors
+data ValVec = ValVec [ValAbs] Delta -- ^ Value Vector Abstractions
+
+-- | Term and type constraints to accompany each value vector abstraction.
+-- For efficiency, we store the term oracle state instead of the term
+-- constraints. TODO: Do the same for the type constraints?
+data Delta = MkDelta { delta_ty_cs :: Bag EvVar
+                     , delta_tm_cs :: TmState }
+
+type ValSetAbs = [ValVec]  -- ^ Value Set Abstractions
+type Uncovered = ValSetAbs
+
+-- Instead of keeping the whole sets in memory, we keep a boolean for both the
+-- covered and the divergent set (we store the uncovered set though, since we
+-- want to print it). For both the covered and the divergent we have:
+--
+--   True <=> The set is non-empty
+--
+-- hence:
+--  C = True             ==> Useful clause (no warning)
+--  C = False, D = True  ==> Clause with inaccessible RHS
+--  C = False, D = False ==> Redundant clause
+type Triple = (Bool, Uncovered, Bool)
 
 -- | Pattern check result
 --
--- * redundant clauses
--- * clauses with inaccessible RHS
--- * missing
-type PmResult = ( [[LPat Id]]
-                , [[LPat Id]]
-                , [([PmExpr], [ComplexEq])] )
+-- * Redundant clauses
+-- * Not-covered clauses
+-- * Clauses with inaccessible RHS
+type PmResult = ([[LPat Id]], Uncovered, [[LPat Id]])
 
 {-
 %************************************************************************
@@ -146,78 +141,56 @@ type PmResult = ( [[LPat Id]]
 -}
 
 -- | Check a single pattern binding (let)
-checkSingle :: Id -> Pat Id -> DsM PmResult
-checkSingle var p = do
-  let lp = [noLoc p]
+checkSingle :: DynFlags -> DsMatchContext -> Id -> Pat Id -> DsM ()
+checkSingle dflags ctxt var p = do
+  mb_pm_res <- tryM (checkSingle' var p)
+  case mb_pm_res of
+    Left  _   -> warnPmIters dflags ctxt
+    Right res -> dsPmWarn dflags ctxt res
+
+-- | Check a single pattern binding (let)
+checkSingle' :: Id -> Pat Id -> DsM PmResult
+checkSingle' var p = do
+  resetPmIterDs -- set the iter-no to zero
   fam_insts <- dsGetFamInstEnvs
-  vec <- liftUs (translatePat fam_insts p)
-  vsa <- initial_uncovered [var]
-  (c,d,us') <- patVectProc False (vec,[]) vsa -- no guards
-  us <- pruneVSA us'
-  return $ case (c,d) of
-    (True,  _)     -> ([],   [],   us)
-    (False, True)  -> ([],   [lp], us)
-    (False, False) -> ([lp], [],   us)
+  clause    <- translatePat fam_insts p
+  missing   <- mkInitialUncovered [var]
+  (cs,us,ds) <- runMany (pmcheckI clause []) missing -- no guards
+  return $ case (cs,ds) of
+    (True,  _    ) -> ([], us, []) -- useful
+    (False, False) -> ( m, us, []) -- redundant
+    (False, True ) -> ([], us,  m) -- inaccessible rhs
+  where m = [[noLoc p]]
 
 -- | Check a matchgroup (case, functions, etc.)
-checkMatches :: Bool -> [Id] -> [LMatch Id (LHsExpr Id)] -> DsM PmResult
-checkMatches oversimplify vars matches
-  | null matches = return ([],[],[])
-  | otherwise    = do
-      missing    <- initial_uncovered vars
-      (rs,is,us) <- go matches missing
-      return (map hsLMatchPats rs, map hsLMatchPats is, us)
-  where
-    go [] missing = do
-      missing' <- pruneVSA missing
-      return ([], [], missing')
-
-    go (m:ms) missing = do
-      fam_insts     <- dsGetFamInstEnvs
-      clause        <- liftUs (translateMatch fam_insts m)
-      (c,  d,  us ) <- patVectProc oversimplify clause missing
-      (rs, is, us') <- go ms us
-      return $ case (c,d) of
-        (True,  _)     -> (  rs,   is, us')
-        (False, True)  -> (  rs, m:is, us')
-        (False, False) -> (m:rs,   is, us')
-
--- | Generate the initial uncovered set. It initializes the
--- delta with all term and type constraints in scope.
-initial_uncovered :: [Id] -> DsM ValSetAbs
-initial_uncovered vars = do
-  cs <- getCsPmM
-  let vsa = foldr Cons Singleton (map PmVar vars)
-  return $ if null cs then vsa
-                      else mkConstraint cs vsa
-
--- | Collect all term and type constraints from the local environment
-getCsPmM :: DsM [PmConstraint]
-getCsPmM = do
-  ty_cs <- bagToList <$> getDictsDs
-  tm_cs <- map simpleToTmCs . bagToList <$> getTmCsDs
-  return $ if null ty_cs
-    then tm_cs
-    else TyConstraint ty_cs : tm_cs
-  where
-    simpleToTmCs :: (Id, PmExpr) -> PmConstraint
-    simpleToTmCs (x,e) = TmConstraint (PmExprVar x) e
+checkMatches :: DynFlags -> DsMatchContext
+             -> [Id] -> [LMatch Id (LHsExpr Id)] -> DsM ()
+checkMatches dflags ctxt vars matches = do
+  mb_pm_res <- tryM (checkMatches' vars matches)
+  case mb_pm_res of
+    Left  _   -> warnPmIters dflags ctxt
+    Right res -> dsPmWarn dflags ctxt res
 
--- | Total number of guards in a translated match that could fail.
-noFailingGuards :: [(PatVec,[PatVec])] -> Int
-noFailingGuards clauses = sum [ countPatVecs gvs | (_, gvs) <- clauses ]
+-- | Check a matchgroup (case, functions, etc.)
+checkMatches' :: [Id] -> [LMatch Id (LHsExpr Id)] -> DsM PmResult
+checkMatches' vars matches
+  | null matches = return ([], [], [])
+  | otherwise = do
+      resetPmIterDs -- set the iter-no to zero
+      missing    <- mkInitialUncovered vars
+      (rs,us,ds) <- go matches missing
+      return (map hsLMatchPats rs, us, map hsLMatchPats ds)
   where
-    countPatVec  gv  = length [ () | p <- gv, not (cantFailPattern p) ]
-    countPatVecs gvs = sum [ countPatVec gv | gv <- gvs ]
-
-computeNoGuards :: [LMatch Id (LHsExpr Id)] -> PmM Int
-computeNoGuards matches = do
-  fam_insts <- dsGetFamInstEnvs
-  matches' <- mapM (liftUs . translateMatch fam_insts) matches
-  return (noFailingGuards matches')
-
-maximum_failing_guards :: Int
-maximum_failing_guards = 20 -- Find a better number
+    go []     missing = return ([], missing, [])
+    go (m:ms) missing = do
+      fam_insts          <- dsGetFamInstEnvs
+      (clause, guards)   <- translateMatch fam_insts m
+      (cs, missing', ds) <- runMany (pmcheckI clause guards) missing
+      (rs, final_u, is)  <- go ms missing'
+      return $ case (cs, ds) of
+        (True,  _    ) -> (  rs, final_u,   is) -- useful
+        (False, False) -> (m:rs, final_u,   is) -- redundant
+        (False, True ) -> (  rs, final_u, m:is) -- inaccessible
 
 {-
 %************************************************************************
@@ -235,45 +208,67 @@ nullaryConPattern :: DataCon -> Pattern
 nullaryConPattern con =
   PmCon { pm_con_con = con, pm_con_arg_tys = []
         , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = [] }
+{-# INLINE nullaryConPattern #-}
 
 truePattern :: Pattern
 truePattern = nullaryConPattern trueDataCon
+{-# INLINE truePattern #-}
 
 -- | A fake guard pattern (True <- _) used to represent cases we cannot handle
 fake_pat :: Pattern
 fake_pat = PmGrd { pm_grd_pv   = [truePattern]
                  , pm_grd_expr = PmExprOther EWildPat }
+{-# INLINE fake_pat #-}
+
+-- | Check whether a guard pattern is generated by the checker (unhandled)
+isFakeGuard :: [Pattern] -> PmExpr -> Bool
+isFakeGuard [PmCon { pm_con_con = c }] (PmExprOther EWildPat)
+  | c == trueDataCon = True
+  | otherwise        = False
+isFakeGuard _pats _e = False
+
+-- | Generate a `canFail` pattern vector of a specific type
+mkCanFailPmPat :: Type -> PmM PatVec
+mkCanFailPmPat ty = do
+  var <- mkPmVar ty
+  return [var, fake_pat]
 
 vanillaConPattern :: DataCon -> [Type] -> PatVec -> Pattern
 -- ADT constructor pattern => no existentials, no local constraints
 vanillaConPattern con arg_tys args =
   PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys
         , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = args }
+{-# INLINE vanillaConPattern #-}
 
+-- | Create an empty list pattern of a given type
 nilPattern :: Type -> Pattern
 nilPattern ty =
   PmCon { pm_con_con = nilDataCon, pm_con_arg_tys = [ty]
         , pm_con_tvs = [], pm_con_dicts = []
         , pm_con_args = [] }
+{-# INLINE nilPattern #-}
 
 mkListPatVec :: Type -> PatVec -> PatVec -> PatVec
 mkListPatVec ty xs ys = [PmCon { pm_con_con = consDataCon
                                , pm_con_arg_tys = [ty]
                                , pm_con_tvs = [], pm_con_dicts = []
                                , pm_con_args = xs++ys }]
+{-# INLINE mkListPatVec #-}
 
+-- | Create a (non-overloaded) literal pattern
 mkLitPattern :: HsLit -> Pattern
 mkLitPattern lit = PmLit { pm_lit_lit = PmSLit lit }
+{-# INLINE mkLitPattern #-}
 
 -- -----------------------------------------------------------------------
 -- * Transform (Pat Id) into of (PmPat Id)
 
-translatePat :: FamInstEnvs -> Pat Id -> UniqSM PatVec
+translatePat :: FamInstEnvs -> Pat Id -> PmM PatVec
 translatePat fam_insts pat = case pat of
-  WildPat ty  -> mkPmVarsSM [ty]
+  WildPat ty  -> mkPmVars [ty]
   VarPat  id  -> return [PmVar (unLoc id)]
   ParPat p    -> translatePat fam_insts (unLoc p)
-  LazyPat _   -> mkPmVarsSM [hsPatType pat] -- like a variable
+  LazyPat _   -> mkPmVars [hsPatType pat] -- like a variable
 
   -- ignore strictness annotations for now
   BangPat p   -> translatePat fam_insts (unLoc p)
@@ -281,7 +276,7 @@ translatePat fam_insts pat = case pat of
   AsPat lid p -> do
      -- Note [Translating As Patterns]
     ps <- translatePat fam_insts (unLoc p)
-    let [e] = map valAbsToPmExpr (coercePatVec ps)
+    let [e] = map vaToPmExpr (coercePatVec ps)
         g   = PmGrd [PmVar (unLoc lid)] e
     return (ps ++ [g])
 
@@ -293,18 +288,12 @@ translatePat fam_insts pat = case pat of
     | WpCast co <-  wrapper, isReflexiveCo co -> translatePat fam_insts p
     | otherwise -> do
         ps      <- translatePat fam_insts p
-        (xp,xe) <- mkPmId2FormsSM ty
+        (xp,xe) <- mkPmId2Forms ty
         let g = mkGuard ps (HsWrap wrapper (unLoc xe))
         return [xp,g]
 
   -- (n + k)  ===>   x (True <- x >= k) (n <- x-k)
-  NPlusKPat (L _ n) k1 k2 ge minus ty -> do
-    (xp, xe) <- mkPmId2FormsSM ty
-    let ke1 = L (getLoc k1) (HsOverLit (unLoc k1))
-        ke2 = L (getLoc k1) (HsOverLit k2)
-        g1 = mkGuard [truePattern] (unLoc $ nlHsSyntaxApps ge    [xe, ke1])
-        g2 = mkGuard [PmVar n]     (unLoc $ nlHsSyntaxApps minus [xe, ke2])
-    return [xp, g1, g2]
+  NPlusKPat (L _ _n) _k1 _k2 _ge _minus ty -> mkCanFailPmPat ty
 
   -- (fun -> pat)   ===>   x (pat <- fun x)
   ViewPat lexpr lpat arg_ty -> do
@@ -312,41 +301,38 @@ translatePat fam_insts pat = case pat of
     -- See Note [Guards and Approximation]
     case all cantFailPattern ps of
       True  -> do
-        (xp,xe) <- mkPmId2FormsSM arg_ty
+        (xp,xe) <- mkPmId2Forms arg_ty
         let g = mkGuard ps (HsApp lexpr xe)
         return [xp,g]
-      False -> do
-        var <- mkPmVarSM arg_ty
-        return [var, fake_pat]
+      False -> mkCanFailPmPat arg_ty
 
   -- list
   ListPat ps ty Nothing -> do
-    foldr (mkListPatVec ty) [nilPattern ty] <$> translatePatVec fam_insts (map unLoc ps)
+    foldr (mkListPatVec ty) [nilPattern ty]
+      <$> translatePatVec fam_insts (map unLoc ps)
 
   -- overloaded list
   ListPat lpats elem_ty (Just (pat_ty, _to_list))
     | Just e_ty <- splitListTyConApp_maybe pat_ty
     , (_, norm_elem_ty) <- normaliseType fam_insts Nominal elem_ty
-         -- elem_ty is frequently something like `Item [Int]`, but we prefer `Int`
+         -- elem_ty is frequently something like
+         -- `Item [Int]`, but we prefer `Int`
     , norm_elem_ty `eqType` e_ty ->
         -- We have to ensure that the element types are exactly the same.
         -- Otherwise, one may give an instance IsList [Int] (more specific than
         -- the default IsList [a]) with a different implementation for `toList'
         translatePat fam_insts (ListPat lpats e_ty Nothing)
-    | otherwise -> do
-        -- See Note [Guards and Approximation]
-        var <- mkPmVarSM pat_ty
-        return [var, fake_pat]
+      -- See Note [Guards and Approximation]
+    | otherwise -> mkCanFailPmPat pat_ty
 
-  ConPatOut { pat_con = L _ (PatSynCon _) } -> do
+  ConPatOut { pat_con = L _ (PatSynCon _) } ->
     -- Pattern synonyms have a "matcher"
     -- (see Note [Pattern synonym representation] in PatSyn.hs
     -- We should be able to transform (P x y)
     -- to   v (Just (x, y) <- matchP v (\x y -> Just (x,y)) Nothing
     -- That is, a combination of a variable pattern and a guard
     -- But there are complications with GADTs etc, and this isn't done yet
-    var <- mkPmVarSM (hsPatType pat)
-    return [var,fake_pat]
+    mkCanFailPmPat (hsPatType pat)
 
   ConPatOut { pat_con     = L _ (RealDataCon con)
             , pat_arg_tys = arg_tys
@@ -387,7 +373,7 @@ translatePat fam_insts pat = case pat of
 
 -- | Translate an overloaded literal (see `tidyNPat' in deSugar/MatchLit.hs)
 translateNPat :: FamInstEnvs
-              -> HsOverLit Id -> Maybe (SyntaxExpr Id) -> Type -> UniqSM PatVec
+              -> HsOverLit Id -> Maybe (SyntaxExpr Id) -> Type -> PmM PatVec
 translateNPat fam_insts (OverLit val False _ ty) mb_neg outer_ty
   | not type_change, isStringTy ty, HsIsString src s <- val, Nothing <- mb_neg
   = translatePat fam_insts (LitPat (HsString src s))
@@ -405,22 +391,23 @@ translateNPat _ ol mb_neg _
 
 -- | Translate a list of patterns (Note: each pattern is translated
 -- to a pattern vector but we do not concatenate the results).
-translatePatVec :: FamInstEnvs -> [Pat Id] -> UniqSM [PatVec]
+translatePatVec :: FamInstEnvs -> [Pat Id] -> PmM [PatVec]
 translatePatVec fam_insts pats = mapM (translatePat fam_insts) pats
 
+-- | Translate a constructor pattern
 translateConPatVec :: FamInstEnvs -> [Type] -> [TyVar]
-                   -> DataCon -> HsConPatDetails Id -> UniqSM PatVec
+                   -> DataCon -> HsConPatDetails Id -> PmM PatVec
 translateConPatVec fam_insts _univ_tys _ex_tvs _ (PrefixCon ps)
   = concat <$> translatePatVec fam_insts (map unLoc ps)
 translateConPatVec fam_insts _univ_tys _ex_tvs _ (InfixCon p1 p2)
   = concat <$> translatePatVec fam_insts (map unLoc [p1,p2])
 translateConPatVec fam_insts  univ_tys  ex_tvs c (RecCon (HsRecFields fs _))
     -- Nothing matched. Make up some fresh term variables
-  | null fs        = mkPmVarsSM arg_tys
+  | null fs        = mkPmVars arg_tys
     -- The data constructor was not defined using record syntax. For the
     -- pattern to be in record syntax it should be empty (e.g. Just {}).
     -- So just like the previous case.
-  | null orig_lbls = ASSERT(null matched_lbls) mkPmVarsSM arg_tys
+  | null orig_lbls = ASSERT(null matched_lbls) mkPmVars arg_tys
     -- Some of the fields appear, in the original order (there may be holes).
     -- Generate a simple constructor pattern and make up fresh variables for
     -- the rest of the fields
@@ -428,20 +415,20 @@ translateConPatVec fam_insts  univ_tys  ex_tvs c (RecCon (HsRecFields fs _))
   = ASSERT(length orig_lbls == length arg_tys)
       let translateOne (lbl, ty) = case lookup lbl matched_pats of
             Just p  -> translatePat fam_insts p
-            Nothing -> mkPmVarsSM [ty]
+            Nothing -> mkPmVars [ty]
       in  concatMapM translateOne (zip orig_lbls arg_tys)
     -- The fields that appear are not in the correct order. Make up fresh
     -- variables for all fields and add guards after matching, to force the
     -- evaluation in the correct order.
   | otherwise = do
-      arg_var_pats    <- mkPmVarsSM arg_tys
+      arg_var_pats    <- mkPmVars arg_tys
       translated_pats <- forM matched_pats $ \(x,pat) -> do
         pvec <- translatePat fam_insts pat
         return (x, pvec)
 
       let zipped = zip orig_lbls [ x | PmVar x <- arg_var_pats ]
           guards = map (\(name,pvec) -> case lookup name zipped of
-                            Just x  -> PmGrd pvec (PmExprVar x)
+                            Just x  -> PmGrd pvec (PmExprVar (idName x))
                             Nothing -> panic "translateConPatVec: lookup")
                        translated_pats
 
@@ -463,7 +450,8 @@ translateConPatVec fam_insts  univ_tys  ex_tvs c (RecCon (HsRecFields fs _))
       | x == y    = subsetOf    xs  ys
       | otherwise = subsetOf (x:xs) ys
 
-translateMatch :: FamInstEnvs -> LMatch Id (LHsExpr Id) -> UniqSM (PatVec,[PatVec])
+-- Translate a single match
+translateMatch :: FamInstEnvs -> LMatch Id (LHsExpr Id) -> PmM (PatVec,[PatVec])
 translateMatch fam_insts (L _ (Match _ lpats _ grhss)) = do
   pats'   <- concat <$> translatePatVec fam_insts pats
   guards' <- mapM (translateGuards fam_insts) guards
@@ -479,11 +467,11 @@ translateMatch fam_insts (L _ (Match _ lpats _ grhss)) = do
 -- * Transform source guards (GuardStmt Id) to PmPats (Pattern)
 
 -- | Translate a list of guard statements to a pattern vector
-translateGuards :: FamInstEnvs -> [GuardStmt Id] -> UniqSM PatVec
+translateGuards :: FamInstEnvs -> [GuardStmt Id] -> PmM PatVec
 translateGuards fam_insts guards = do
   all_guards <- concat <$> mapM (translateGuard fam_insts) guards
   return (replace_unhandled all_guards)
-  -- It should have been (return all_guards) but it is too expressive.
+  -- It should have been (return all_guards) but it is too expressive.
   -- Since the term oracle does not handle all constraints we generate,
   -- we (hackily) replace all constraints the oracle cannot handle with a
   -- single one (we need to know if there is a possibility of falure).
@@ -519,28 +507,29 @@ cantFailPattern (PmGrd pv _e)
 cantFailPattern _ = False
 
 -- | Translate a guard statement to Pattern
-translateGuard :: FamInstEnvs -> GuardStmt Id -> UniqSM PatVec
-translateGuard _         (BodyStmt   e _ _ _) = translateBoolGuard e
-translateGuard _         (LetStmt      binds) = translateLet (unLoc binds)
-translateGuard fam_insts (BindStmt p e _ _ _) = translateBind fam_insts p e
-translateGuard _         (LastStmt        {}) = panic "translateGuard LastStmt"
-translateGuard _         (ParStmt         {}) = panic "translateGuard ParStmt"
-translateGuard _         (TransStmt       {}) = panic "translateGuard TransStmt"
-translateGuard _         (RecStmt         {}) = panic "translateGuard RecStmt"
-translateGuard _         (ApplicativeStmt {}) = panic "translateGuard ApplicativeLastStmt"
+translateGuard :: FamInstEnvs -> GuardStmt Id -> PmM PatVec
+translateGuard fam_insts guard = case guard of
+  BodyStmt   e _ _ _ -> translateBoolGuard e
+  LetStmt      binds -> translateLet (unLoc binds)
+  BindStmt p e _ _ _ -> translateBind fam_insts p e
+  LastStmt        {} -> panic "translateGuard LastStmt"
+  ParStmt         {} -> panic "translateGuard ParStmt"
+  TransStmt       {} -> panic "translateGuard TransStmt"
+  RecStmt         {} -> panic "translateGuard RecStmt"
+  ApplicativeStmt {} -> panic "translateGuard ApplicativeLastStmt"
 
 -- | Translate let-bindings
-translateLet :: HsLocalBinds Id -> UniqSM PatVec
+translateLet :: HsLocalBinds Id -> PmM PatVec
 translateLet _binds = return []
 
 -- | Translate a pattern guard
-translateBind :: FamInstEnvs -> LPat Id -> LHsExpr Id -> UniqSM PatVec
+translateBind :: FamInstEnvs -> LPat Id -> LHsExpr Id -> PmM PatVec
 translateBind fam_insts (L _ p) e = do
   ps <- translatePat fam_insts p
   return [mkGuard ps (unLoc e)]
 
 -- | Translate a boolean guard
-translateBoolGuard :: LHsExpr Id -> UniqSM PatVec
+translateBoolGuard :: LHsExpr Id -> PmM PatVec
 translateBoolGuard e
   | isJust (isTrueLHsExpr e) = return []
     -- The formal thing to do would be to generate (True <- True)
@@ -599,7 +588,7 @@ below is the *right thing to do*:
 
    ListPat lpats elem_ty (Just (pat_ty, to_list))
      otherwise -> do
-       (xp, xe) <- mkPmId2FormsSM pat_ty
+       (xp, xe) <- mkPmId2Forms pat_ty
        ps       <- translatePatVec (map unLoc lpats)
        let pats = foldr (mkListPatVec elem_ty) [nilPattern elem_ty] ps
            g    = mkGuard pats (HsApp (noLoc to_list) xe)
@@ -648,39 +637,12 @@ families is not really efficient.
 
 %************************************************************************
 %*                                                                      *
-                    Main Pattern Matching Check
+                 Utilities for Pattern Match Checking
 %*                                                                      *
 %************************************************************************
 -}
 
 -- ----------------------------------------------------------------------------
--- * Process a vector
-
--- Covered, Uncovered, Divergent
-process_guards :: UniqSupply -> Bool -> [PatVec]
-               -> (ValSetAbs, ValSetAbs, ValSetAbs)
-process_guards _us _oversimplify [] = (Singleton, Empty, Empty) -- No guard
-process_guards  us  oversimplify gs
-  -- If we have a list of guards but one of them is empty (True by default)
-  -- then we know that it is exhaustive (just a shortcut)
-  | any null gs  = (Singleton, Empty, Singleton)
-  -- If the user wants the same behaviour (almost no expressivity about guards)
-  | oversimplify = go us Singleton [[fake_pat]] -- to signal failure
-  -- If the user want the full reasoning (may be non-performant)
-  | otherwise    = go us Singleton gs
-  where
-    go _usupply missing []       = (Empty, missing, Empty)
-    go  usupply missing (gv:gvs) = (mkUnion cs css, uss, mkUnion ds dss)
-      where
-        (us1, us2, us3, us4) = splitUniqSupply4 usupply
-
-        cs = covered   us1 Singleton gv missing
-        us = uncovered us2 Empty     gv missing
-        ds = divergent us3 Empty     gv missing
-
-        (css, uss, dss) = go us4 us gvs
-
--- ----------------------------------------------------------------------------
 -- * Basic utilities
 
 -- | Get the type out of a PmPat. For guard patterns (ps <- e) we use the type
@@ -695,7 +657,9 @@ pmPatType (PmGrd  { pm_grd_pv  = pv })
   = ASSERT(patVecArity pv == 1) (pmPatType p)
   where Just p = find ((==1) . patternArity) pv
 
-mkOneConFull :: Id -> UniqSupply -> DataCon -> (ValAbs, [PmConstraint])
+-- | Generate a value abstraction for a given constructor (generate
+-- fresh variables of the appropriate type for arguments)
+mkOneConFull :: Id -> DataCon -> PmM (ValAbs, ComplexEq, Bag EvVar)
 --  *  x :: T tys, where T is an algebraic data type
 --     NB: in the case of a data familiy, T is the *representation* TyCon
 --     e.g.   data instance T (a,b) = T1 a b
@@ -709,142 +673,98 @@ mkOneConFull :: Id -> UniqSupply -> DataCon -> (ValAbs, [PmConstraint])
 --          K tys :: forall bs. Q => s1 .. sn -> T tys
 --
 -- Results: ValAbs:          K (y1::s1) .. (yn::sn)
---          [PmConstraint]:  Q, x ~ K y1..yn
-
-mkOneConFull x usupply con = (con_abs, constraints)
-  where
-
-    (usupply1, usupply2, usupply3) = splitUniqSupply3 usupply
-
-    res_ty = idType x -- res_ty == TyConApp (dataConTyCon cabs_con) cabs_arg_tys
-    (univ_tvs, ex_tvs, eq_spec, thetas, arg_tys, _) = dataConFullSig con
-    data_tc = dataConTyCon con   -- The representation TyCon
-    tc_args = case splitTyConApp_maybe res_ty of
-                 Just (tc, tys) -> ASSERT( tc == data_tc ) tys
-                 Nothing -> pprPanic "mkOneConFull: Not TyConApp:" (ppr res_ty)
-
-    subst1  = zipTvSubst univ_tvs tc_args
-
-    (subst, ex_tvs') = cloneTyVarBndrs subst1 ex_tvs usupply1
-
-    -- Fresh term variables (VAs) as arguments to the constructor
-    arguments  = mkConVars usupply2 (substTys subst arg_tys)
-    -- All constraints bound by the constructor (alpha-renamed)
-    theta_cs   = substTheta subst (eqSpecPreds eq_spec ++ thetas)
-    evvars     = zipWith (nameType "pm") (listSplitUniqSupply usupply3) theta_cs
-    con_abs    = PmCon { pm_con_con     = con
+--          ComplexEq:       x ~ K y1..yn
+--          [EvVar]:         Q
+mkOneConFull x con = do
+  let -- res_ty == TyConApp (dataConTyCon cabs_con) cabs_arg_tys
+      res_ty  = idType x
+      (univ_tvs, ex_tvs, eq_spec, thetas, arg_tys, _) = dataConFullSig con
+      data_tc = dataConTyCon con   -- The representation TyCon
+      tc_args = case splitTyConApp_maybe res_ty of
+                  Just (tc, tys) -> ASSERT( tc == data_tc ) tys
+                  Nothing -> pprPanic "mkOneConFull: Not TyConApp:" (ppr res_ty)
+      subst1  = zipTvSubst univ_tvs tc_args
+
+  (subst, ex_tvs') <- cloneTyVarBndrs subst1 ex_tvs <$> getUniqueSupplyM
+
+  -- Fresh term variables (VAs) as arguments to the constructor
+  arguments <-  mapM mkPmVar (substTys subst arg_tys)
+  -- All constraints bound by the constructor (alpha-renamed)
+  let theta_cs = substTheta subst (eqSpecPreds eq_spec ++ thetas)
+  evvars <- mapM (nameType "pm") theta_cs
+  let con_abs  = PmCon { pm_con_con     = con
                        , pm_con_arg_tys = tc_args
                        , pm_con_tvs     = ex_tvs'
                        , pm_con_dicts   = evvars
                        , pm_con_args    = arguments }
-
-    constraints -- term and type constraints
-      | null evvars = [ TmConstraint (PmExprVar x) (valAbsToPmExpr con_abs) ]
-      | otherwise   = [ TmConstraint (PmExprVar x) (valAbsToPmExpr con_abs)
-                      , TyConstraint evvars ]
-
-mkConVars :: UniqSupply -> [Type] -> [ValAbs] -- ys, fresh with the given type
-mkConVars us tys = zipWith mkPmVar (listSplitUniqSupply us) tys
-
-tailVSA :: ValSetAbs -> ValSetAbs
-tailVSA Empty               = Empty
-tailVSA Singleton           = panic "tailVSA: Singleton"
-tailVSA (Union vsa1 vsa2)   = tailVSA vsa1 `mkUnion` tailVSA vsa2
-tailVSA (Constraint cs vsa) = cs `mkConstraint` tailVSA vsa
-tailVSA (Cons _ vsa)        = vsa -- actual work
-
-wrapK :: DataCon -> [Type] -> [TyVar] -> [EvVar] -> ValSetAbs -> ValSetAbs
-wrapK con arg_tys ex_tvs dicts = go (dataConSourceArity con) emptylist
-  where
-    go :: Int -> DList ValAbs -> ValSetAbs -> ValSetAbs
-    go _ _    Empty = Empty
-    go 0 args vsa   = PmCon { pm_con_con  = con, pm_con_arg_tys = arg_tys
-                            , pm_con_tvs  = ex_tvs, pm_con_dicts = dicts
-                            , pm_con_args = toList args } `mkCons` vsa
-    go _ _    Singleton           = panic "wrapK: Singleton"
-    go n args (Cons vs vsa)       = go (n-1) (args `snoc` vs) vsa
-    go n args (Constraint cs vsa) = cs `mkConstraint` go n args vsa
-    go n args (Union vsa1 vsa2)   = go n args vsa1 `mkUnion` go n args vsa2
-
-newtype DList a = DL { unDL :: [a] -> [a] }
-
-toList :: DList a -> [a]
-toList = ($[]) . unDL
-{-# INLINE toList #-}
-
-emptylist :: DList a
-emptylist = DL id
-{-# INLINE emptylist #-}
-
-infixl `snoc`
-snoc :: DList a -> a -> DList a
-snoc xs x = DL (unDL xs . (x:))
-{-# INLINE snoc #-}
-
--- ----------------------------------------------------------------------------
--- * Smart Value Set Abstraction Constructors
--- (NB: An empty value set can only be represented as `Empty')
-
--- | The smart constructor for Constraint (maintains VsaInvariant)
-mkConstraint :: [PmConstraint] -> ValSetAbs -> ValSetAbs
-mkConstraint _cs Empty                = Empty
-mkConstraint cs1 (Constraint cs2 vsa) = Constraint (cs1++cs2) vsa
-mkConstraint cs  other_vsa            = Constraint cs other_vsa
-
--- | The smart constructor for Union (maintains VsaInvariant)
-mkUnion :: ValSetAbs -> ValSetAbs -> ValSetAbs
-mkUnion Empty vsa = vsa
-mkUnion vsa Empty = vsa
-mkUnion vsa1 vsa2 = Union vsa1 vsa2
-
--- | The smart constructor for Cons (maintains VsaInvariant)
-mkCons :: ValAbs -> ValSetAbs -> ValSetAbs
-mkCons _ Empty = Empty
-mkCons va vsa  = Cons va vsa
+  return (con_abs, (PmExprVar (idName x), vaToPmExpr con_abs), listToBag evvars)
 
 -- ----------------------------------------------------------------------------
 -- * More smart constructors and fresh variable generation
 
+-- | Create a guard pattern
 mkGuard :: PatVec -> HsExpr Id -> Pattern
-mkGuard pv e = PmGrd pv (hsExprToPmExpr e)
-
-mkPmVar :: UniqSupply -> Type -> PmPat p
-mkPmVar usupply ty = PmVar (mkPmId usupply ty)
-
-mkPmVarSM :: Type -> UniqSM Pattern
-mkPmVarSM ty = flip mkPmVar ty <$> getUniqueSupplyM
-
-mkPmVarsSM :: [Type] -> UniqSM PatVec
-mkPmVarsSM tys = mapM mkPmVarSM tys
-
-mkPmId :: UniqSupply -> Type -> Id
-mkPmId usupply ty = mkLocalId name ty
+mkGuard pv e
+  | all cantFailPattern pv = PmGrd pv expr
+  | PmExprOther {} <- expr = fake_pat
+  | otherwise              = PmGrd pv expr
   where
-    unique  = uniqFromSupply usupply
-    occname = mkVarOccFS (fsLit (show unique))
-    name    = mkInternalName unique occname noSrcSpan
-
-mkPmId2FormsSM :: Type -> UniqSM (Pattern, LHsExpr Id)
-mkPmId2FormsSM ty = do
-  us <- getUniqueSupplyM
-  let x = mkPmId us ty
+    expr = hsExprToPmExpr e
+
+-- | Create a term equality of the form: `(False ~ (x ~ lit))`
+mkNegEq :: Id -> PmLit -> ComplexEq
+mkNegEq x l = (falsePmExpr, PmExprVar (idName x) `PmExprEq` PmExprLit l)
+{-# INLINE mkNegEq #-}
+
+-- | Create a term equality of the form: `(x ~ lit)`
+mkPosEq :: Id -> PmLit -> ComplexEq
+mkPosEq x l = (PmExprVar (idName x), PmExprLit l)
+{-# INLINE mkPosEq #-}
+
+-- | Generate a variable pattern of a given type
+mkPmVar :: Type -> PmM (PmPat p)
+mkPmVar ty = PmVar <$> mkPmId ty
+{-# INLINE mkPmVar #-}
+
+-- | Generate many variable patterns, given a list of types
+mkPmVars :: [Type] -> PmM PatVec
+mkPmVars tys = mapM mkPmVar tys
+{-# INLINE mkPmVars #-}
+
+-- | Generate a fresh `Id` of a given type
+mkPmId :: Type -> PmM Id
+mkPmId ty = getUniqueM >>= \unique ->
+  let occname = mkVarOccFS (fsLit (show unique))
+      name    = mkInternalName unique occname noSrcSpan
+  in  return (mkLocalId name ty)
+
+-- | Generate a fresh term variable of a given and return it in two forms:
+-- * A variable pattern
+-- * A variable expression
+mkPmId2Forms :: Type -> PmM (Pattern, LHsExpr Id)
+mkPmId2Forms ty = do
+  x <- mkPmId ty
   return (PmVar x, noLoc (HsVar (noLoc x)))
 
 -- ----------------------------------------------------------------------------
 -- * Converting between Value Abstractions, Patterns and PmExpr
 
-valAbsToPmExpr :: ValAbs -> PmExpr
-valAbsToPmExpr (PmCon  { pm_con_con = c, pm_con_args = ps })
-  = PmExprCon c (map valAbsToPmExpr ps)
-valAbsToPmExpr (PmVar  { pm_var_id  = x }) = PmExprVar x
-valAbsToPmExpr (PmLit  { pm_lit_lit = l }) = PmExprLit l
-valAbsToPmExpr (PmNLit { pm_lit_id  = x }) = PmExprVar x
-
--- Convert a pattern vector to a value list abstraction by dropping the guards
--- recursively (See Note [Translating As Patterns])
-coercePatVec :: PatVec -> ValVecAbs
+-- | Convert a value abstraction an expression
+vaToPmExpr :: ValAbs -> PmExpr
+vaToPmExpr (PmCon  { pm_con_con = c, pm_con_args = ps })
+  = PmExprCon c (map vaToPmExpr ps)
+vaToPmExpr (PmVar  { pm_var_id  = x }) = PmExprVar (idName x)
+vaToPmExpr (PmLit  { pm_lit_lit = l }) = PmExprLit l
+vaToPmExpr (PmNLit { pm_lit_id  = x }) = PmExprVar (idName x)
+
+-- | Convert a pattern vector to a list of value abstractions by dropping the
+-- guards (See Note [Translating As Patterns])
+coercePatVec :: PatVec -> [ValAbs]
 coercePatVec pv = concatMap coercePmPat pv
 
+-- | Convert a pattern to a list of value abstractions (will be either an empty
+-- list if the pattern is a guard pattern, or a singleton list in all other
+-- cases) by dropping the guards (See Note [Translating As Patterns])
 coercePmPat :: Pattern -> [ValAbs]
 coercePmPat (PmVar { pm_var_id  = x }) = [PmVar { pm_var_id  = x }]
 coercePmPat (PmLit { pm_lit_lit = l }) = [PmLit { pm_lit_lit = l }]
@@ -856,7 +776,7 @@ coercePmPat (PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys
            , pm_con_args = coercePatVec args }]
 coercePmPat (PmGrd {}) = [] -- drop the guards
 
--- Get all constructors in the family (including given)
+-- Get all constructors in the family (including given)
 allConstructors :: DataCon -> [DataCon]
 allConstructors = tyConDataCons . dataConTyCon
 
@@ -866,108 +786,21 @@ allConstructors = tyConDataCons . dataConTyCon
 newEvVar :: Name -> Type -> EvVar
 newEvVar name ty = mkLocalId name (toTcType ty)
 
-nameType :: String -> UniqSupply -> Type -> EvVar
-nameType name usupply ty = newEvVar idname ty
-  where
-    unique  = uniqFromSupply usupply
-    occname = mkVarOccFS (fsLit (name++"_"++show unique))
-    idname  = mkInternalName unique occname noSrcSpan
-
--- | Partition the constraints to type cs, term cs and forced variables
-splitConstraints :: [PmConstraint] -> ([EvVar], [(PmExpr, PmExpr)], Maybe Id)
-splitConstraints [] = ([],[],Nothing)
-splitConstraints (c : rest)
-  = case c of
-      TyConstraint cs    -> (cs ++ ty_cs, tm_cs, bot_cs)
-      TmConstraint e1 e2 -> (ty_cs, (e1,e2):tm_cs, bot_cs)
-      BtConstraint cs    -> ASSERT(isNothing bot_cs) -- NB: Only one x ~ _|_
-                                  (ty_cs, tm_cs, Just cs)
-  where
-    (ty_cs, tm_cs, bot_cs) = splitConstraints rest
+nameType :: String -> Type -> PmM EvVar
+nameType name ty = do
+  unique <- getUniqueM
+  let occname = mkVarOccFS (fsLit (name++"_"++show unique))
+      idname  = mkInternalName unique occname noSrcSpan
+  return (newEvVar idname ty)
 
 {-
 %************************************************************************
 %*                                                                      *
-                              The oracles
+                              The type oracle
 %*                                                                      *
 %************************************************************************
 -}
 
--- | Check whether at least a path in a value set
--- abstraction has satisfiable constraints.
-anySatVSA :: ValSetAbs -> PmM Bool
-anySatVSA vsa = notNull <$> pruneVSABound 1 vsa
-
-pruneVSA :: ValSetAbs -> PmM [([PmExpr], [ComplexEq])]
--- Prune a Value Set abstraction, keeping only as many as we are going to print
--- plus one more. We need the additional one to be able to print "..." when the
--- uncovered are too many.
-pruneVSA vsa = pruneVSABound (maximum_output+1) vsa
-
--- | Apply a term substitution to a value vector abstraction. All VAs are
--- transformed to PmExpr (used only before pretty printing).
-substInValVecAbs :: PmVarEnv -> ValVecAbs -> [PmExpr]
-substInValVecAbs subst = map (exprDeepLookup subst . valAbsToPmExpr)
-
-mergeBotCs :: Maybe Id -> Maybe Id -> Maybe Id
-mergeBotCs (Just x) Nothing  = Just x
-mergeBotCs Nothing  (Just y) = Just y
-mergeBotCs Nothing  Nothing  = Nothing
-mergeBotCs (Just _) (Just _) = panic "mergeBotCs: two (x ~ _|_) constraints"
-
--- | Wrap up the term oracle's state once solving is complete. Drop any
--- information about unhandled constraints (involving HsExprs) and flatten
--- (height 1) the substitution.
-wrapUpTmState :: TmState -> ([ComplexEq], PmVarEnv)
-wrapUpTmState (residual, (_, subst)) = (residual, flattenPmVarEnv subst)
-
--- | Prune all paths in a value set abstraction with inconsistent constraints.
--- Returns only `n' value vector abstractions, when `n' is given as an argument.
-pruneVSABound :: Int -> ValSetAbs -> PmM [([PmExpr], [ComplexEq])]
-pruneVSABound n v = go n init_cs emptylist v
-  where
-    init_cs :: ([EvVar], TmState, Maybe Id)
-    init_cs = ([], initialTmState, Nothing)
-
-    go :: Int -> ([EvVar], TmState, Maybe Id) -> DList ValAbs
-       -> ValSetAbs -> PmM [([PmExpr], [ComplexEq])]
-    go n all_cs@(ty_cs, tm_env, bot_ct) vec in_vsa
-      | n <= 0    = return [] -- no need to keep going
-      | otherwise = case in_vsa of
-          Empty -> return []
-          Union vsa1 vsa2 -> do
-            vecs1 <- go n                  all_cs vec vsa1
-            vecs2 <- go (n - length vecs1) all_cs vec vsa2
-            return (vecs1 ++ vecs2)
-          Singleton -> do
-            -- TODO: Provide an incremental interface for the type oracle
-            sat <- tyOracle (listToBag ty_cs)
-            return $ case sat of
-              True  -> let (residual_eqs, subst) = wrapUpTmState tm_env
-                           vector = substInValVecAbs subst (toList vec)
-                       in  [(vector, residual_eqs)]
-              False -> []
-
-          Constraint cs vsa -> case splitConstraints cs of
-            (new_ty_cs, new_tm_cs, new_bot_ct) ->
-              case tmOracle tm_env new_tm_cs of
-                Just new_tm_env ->
-                  let bot = mergeBotCs new_bot_ct bot_ct
-                      ans = case bot of
-                              Nothing -> True                    -- covered
-                              Just b  -> canDiverge b new_tm_env -- divergent
-                  in  case ans of
-                        True  -> go n (new_ty_cs++ty_cs,new_tm_env,bot) vec vsa
-                        False -> return []
-                Nothing -> return []
-          Cons va vsa -> go n all_cs (vec `snoc` va) vsa
-
--- | This variable shows the maximum number of lines of output generated for
--- warnings. It will limit the number of patterns/equations displayed to
--- maximum_output. (TODO: add command-line option?)
-maximum_output :: Int
-maximum_output = 4
-
 -- | Check whether a set of type constraints is satisfiable.
 tyOracle :: Bag EvVar -> PmM Bool
 tyOracle evs
@@ -984,11 +817,15 @@ tyOracle evs
 %************************************************************************
 -}
 
+-- | The arity of a pattern/pattern vector is the
+-- number of top-level patterns that are not guards
 type PmArity = Int
 
+-- | Compute the arity of a pattern vector
 patVecArity :: PatVec -> PmArity
 patVecArity = sum . map patternArity
 
+-- | Compute the arity of a pattern
 patternArity :: Pattern -> PmArity
 patternArity (PmGrd {}) = 0
 patternArity _other_pat = 1
@@ -996,305 +833,270 @@ patternArity _other_pat = 1
 {-
 %************************************************************************
 %*                                                                      *
-            Heart of the algorithm: Function patVectProc
+            Heart of the algorithm: Function pmcheck
 %*                                                                      *
 %************************************************************************
--}
 
--- | Process a single vector
-patVectProc :: Bool -> (PatVec, [PatVec]) -> ValSetAbs
-            -> PmM (Bool, Bool, ValSetAbs)
-patVectProc oversimplify (vec,gvs) vsa = do
-  us <- getUniqueSupplyM
-  let (c_def, u_def, d_def) = process_guards us oversimplify gvs
-  (usC, usU, usD) <- getUniqueSupplyM3
-  mb_c <- anySatVSA (covered   usC c_def vec vsa)
-  mb_d <- anySatVSA (divergent usD d_def vec vsa)
-  let vsa' = uncovered usU u_def vec vsa
-  return (mb_c, mb_d, vsa')
-
--- | Covered, Uncovered, Divergent
-covered, uncovered, divergent :: UniqSupply -> ValSetAbs
-                              -> PatVec -> ValSetAbs -> ValSetAbs
-covered   us gvsa vec vsa = pmTraverse us gvsa cMatcher vec vsa
-uncovered us gvsa vec vsa = pmTraverse us gvsa uMatcher vec vsa
-divergent us gvsa vec vsa = pmTraverse us gvsa dMatcher vec vsa
+Main functions are:
 
--- ----------------------------------------------------------------------------
--- * Generic traversal function
---
--- | Because we represent Value Set Abstractions as a different datatype, more
--- cases than the ones described in the paper appear. Since they are the same
--- for all three functions (covered, uncovered, divergent), function
--- `pmTraverse' handles these cases (`pmTraverse' also takes care of the
--- Guard-Case since it is common for all). The actual work is done by functions
--- `cMatcher', `uMatcher' and `dMatcher' below.
-
-pmTraverse :: UniqSupply
-           -> ValSetAbs -- gvsa
-           -> PmMatcher -- what to do
-           -> PatVec
-           -> ValSetAbs
-           -> ValSetAbs
-pmTraverse _us _gvsa _rec _vec Empty      = Empty
-pmTraverse _us  gvsa _rec []   Singleton  = gvsa
-pmTraverse _us _gvsa _rec []   (Cons _ _) = panic "pmTraverse: cons"
-pmTraverse  us  gvsa  rec vec  (Union vsa1 vsa2)
-  = mkUnion (pmTraverse us1 gvsa rec vec vsa1)
-            (pmTraverse us2 gvsa rec vec vsa2)
-  where (us1, us2) = splitUniqSupply us
-pmTraverse us gvsa rec vec (Constraint cs vsa)
-  = mkConstraint cs (pmTraverse us gvsa rec vec vsa)
-pmTraverse us gvsa rec (p:ps) vsa
-  | PmGrd pv e <- p
-  = -- Guard Case
-    let (us1, us2) = splitUniqSupply us
-        y  = mkPmId us1 (pmPatType p)
-        cs = [TmConstraint (PmExprVar y) e]
-    in  mkConstraint cs $ tailVSA $
-          pmTraverse us2 gvsa rec (pv++ps) (PmVar y `mkCons` vsa)
-
-  -- Constructor/Variable/Literal Case
-  | Cons va vsa <- vsa = rec us gvsa p ps va vsa
-  -- Impossible: length mismatch for ValSetAbs and PatVec
-  | otherwise = panic "pmTraverse: singleton" -- can't be anything else
-
-type PmMatcher =  UniqSupply
-               -> ValSetAbs
-               -> Pattern -> PatVec    -- Vector head and tail
-               -> ValAbs  -> ValSetAbs -- VSA    head and tail
-               -> ValSetAbs
-
-cMatcher, uMatcher, dMatcher :: PmMatcher
-
--- cMatcher
--- ----------------------------------------------------------------------------
+* mkInitialUncovered :: [Id] -> PmM Uncovered
 
--- CVar
-cMatcher us gvsa (PmVar x) ps va vsa
-  = va `mkCons` (cs `mkConstraint` covered us gvsa ps vsa)
-  where cs = [TmConstraint (PmExprVar x) (valAbsToPmExpr va)]
+  Generates the initial uncovered set. Term and type constraints in scope
+  are checked, if they are inconsistent, the set is empty, otherwise, the
+  set contains only a vector of variables with the constraints in scope.
 
--- CLitCon
-cMatcher us gvsa (PmLit l) ps (va@(PmCon {})) vsa
-  = va `mkCons` (cs `mkConstraint` covered us gvsa ps vsa)
-  where cs = [ TmConstraint (PmExprLit l) (valAbsToPmExpr va) ]
+* pmcheck :: PatVec -> [PatVec] -> ValVec -> PmM Triple
 
--- CConLit
-cMatcher us gvsa (p@(PmCon {})) ps (PmLit l) vsa
-  = cMatcher us3 gvsa p ps con_abs (mkConstraint cs vsa)
-  where
-    (us1, us2, us3)   = splitUniqSupply3 us
-    y                 = mkPmId us1 (pmPatType p)
-    (con_abs, all_cs) = mkOneConFull y us2 (pm_con_con p)
-    cs = TmConstraint (PmExprVar y) (PmExprLit l) : all_cs
-
--- CConNLit
-cMatcher us gvsa (p@(PmCon { pm_con_con = con })) ps
-                 (PmNLit { pm_lit_id = x }) vsa
-  = cMatcher us2 gvsa p ps con_abs (mkConstraint all_cs vsa)
-  where
-    (us1, us2)        = splitUniqSupply us
-    (con_abs, all_cs) = mkOneConFull x us1 con
-
--- CConCon
-cMatcher us gvsa (p@(PmCon { pm_con_con = c1, pm_con_args = args1 })) ps
-                    (PmCon { pm_con_con = c2, pm_con_args = args2 }) vsa
-  | c1 /= c2  = Empty
-  | otherwise = wrapK c1 (pm_con_arg_tys p)
-                         (pm_con_tvs     p)
-                         (pm_con_dicts   p)
-                         (covered us gvsa (args1 ++ ps)
-                                          (foldr mkCons vsa args2))
-
--- CLitLit
-cMatcher us gvsa (PmLit l1) ps (va@(PmLit l2)) vsa = case eqPmLit l1 l2 of
-  -- See Note [Undecidable Equality for Overloaded Literals] in PmExpr
-  True  -> va `mkCons` covered us gvsa ps vsa -- match
-  False -> Empty                              -- mismatch
-
--- CConVar
-cMatcher us gvsa (p@(PmCon { pm_con_con = con })) ps (PmVar x) vsa
-  = cMatcher us2 gvsa p ps con_abs (mkConstraint all_cs vsa)
-  where
-    (us1, us2)        = splitUniqSupply us
-    (con_abs, all_cs) = mkOneConFull x us1 con
+  Checks redundancy, coverage and inaccessibility, using auxilary functions
+  `pmcheckGuards` and `pmcheckHd`. Mainly handles the guard case which is
+  common in all three checks (see paper) and calls `pmcheckGuards` when the
+  whole clause is checked, or `pmcheckHd` when the pattern vector does not
+  start with a guard.
 
--- CLitVar
-cMatcher us gvsa (p@(PmLit l)) ps (PmVar x) vsa
-  = cMatcher us gvsa p ps lit_abs (mkConstraint cs vsa)
-  where
-    lit_abs = PmLit l
-    cs      = [TmConstraint (PmExprVar x) (PmExprLit l)]
+* pmcheckGuards :: [PatVec] -> ValVec -> PmM Triple
 
--- CLitNLit
-cMatcher us gvsa (p@(PmLit l)) ps
-                 (PmNLit { pm_lit_id = x, pm_lit_not = lits }) vsa
-  | all (not . eqPmLit l) lits
-  = cMatcher us gvsa p ps lit_abs (mkConstraint cs vsa)
-  | otherwise = Empty
-  where
-    lit_abs = PmLit l
-    cs      = [TmConstraint (PmExprVar x) (PmExprLit l)]
+  Processes the guards.
 
--- Impossible: handled by pmTraverse
-cMatcher _ _ (PmGrd {}) _ _ _ = panic "Check.cMatcher: Guard"
+* pmcheckHd :: Pattern -> PatVec -> [PatVec]
+          -> ValAbs -> ValVec -> PmM Triple
 
--- uMatcher
--- ----------------------------------------------------------------------------
-
--- UVar
-uMatcher us gvsa (PmVar x) ps va vsa
-  = va `mkCons` (cs `mkConstraint` uncovered us gvsa ps vsa)
-  where cs = [TmConstraint (PmExprVar x) (valAbsToPmExpr va)]
+  Worker: This function implements functions `covered`, `uncovered` and
+  `divergent` from the paper at once. Slightly different from the paper because
+  it does not even produce the covered and uncovered sets. Since we only care
+  about whether a clause covers SOMETHING or if it may forces ANY argument, we
+  only store a boolean in both cases, for efficiency.
+-}
 
--- ULitCon
-uMatcher us gvsa (PmLit l) ps (va@(PmCon {})) vsa
-  = uMatcher us2 gvsa (PmVar y) ps va (mkConstraint cs vsa)
-  where
-    (us1, us2) = splitUniqSupply us
-    y  = mkPmId us1 (pmPatType va)
-    cs = [TmConstraint (PmExprVar y) (PmExprLit l)]
+-- | Lift a pattern matching action from a single value vector abstration to a
+-- value set abstraction, but calling it on every vector and the combining the
+-- results.
+runMany :: (ValVec -> PmM Triple) -> (Uncovered -> PmM Triple)
+runMany pm us = mapAndUnzip3M pm us >>= \(css, uss, dss) ->
+                  return (or css, concat uss, or dss)
+{-# INLINE runMany #-}
 
--- UConLit
-uMatcher us gvsa (p@(PmCon {})) ps (PmLit l) vsa
-  = uMatcher us2 gvsa p ps (PmVar y) (mkConstraint cs vsa)
-  where
-    (us1, us2) = splitUniqSupply us
-    y  = mkPmId us1 (pmPatType p)
-    cs = [TmConstraint (PmExprVar y) (PmExprLit l)]
-
--- UConNLit
-uMatcher us gvsa (p@(PmCon {})) ps (PmNLit { pm_lit_id = x }) vsa
-  = uMatcher us gvsa p ps (PmVar x) vsa
-
--- UConCon
-uMatcher us gvsa ( p@(PmCon { pm_con_con = c1, pm_con_args = args1 })) ps
-                 (va@(PmCon { pm_con_con = c2, pm_con_args = args2 })) vsa
-  | c1 /= c2  = va `mkCons` vsa
-  | otherwise = wrapK c1 (pm_con_arg_tys p)
-                         (pm_con_tvs     p)
-                         (pm_con_dicts   p)
-                         (uncovered us gvsa (args1 ++ ps)
-                                            (foldr mkCons vsa args2))
-
--- ULitLit
-uMatcher us gvsa (PmLit l1) ps (va@(PmLit l2)) vsa = case eqPmLit l1 l2 of
-  -- See Note [Undecidable Equality for Overloaded Literals] in PmExpr
-  True  -> va `mkCons` uncovered us gvsa ps vsa -- match
-  False -> va `mkCons` vsa                      -- mismatch
-
--- UConVar
-uMatcher us gvsa (p@(PmCon { pm_con_con = con })) ps (PmVar x) vsa
-  = uncovered us2 gvsa (p : ps) inst_vsa
-  where
-    (us1, us2) = splitUniqSupply us
-
-    -- Unfold the variable to all possible constructor patterns
-    cons_cs  = zipWith (mkOneConFull x) (listSplitUniqSupply us1)
-                                        (allConstructors con)
-    add_one (va,cs) valset = mkUnion valset (va `mkCons` mkConstraint cs vsa)
-    inst_vsa = foldr add_one Empty cons_cs -- instantiated vsa [x mapsto K_j ys]
-
--- ULitVar
-uMatcher us gvsa (p@(PmLit l)) ps (PmVar x) vsa
-  = mkUnion (uMatcher us gvsa p ps (PmLit l) (mkConstraint match_cs vsa))
-            (non_match_cs `mkConstraint` (PmNLit x [l] `mkCons` vsa))
+-- | Generate the initial uncovered set. It initializes the
+-- delta with all term and type constraints in scope.
+mkInitialUncovered :: [Id] -> PmM Uncovered
+mkInitialUncovered vars = do
+  ty_cs  <- getDictsDs
+  tm_cs  <- map toComplex . bagToList <$> getTmCsDs
+  sat_ty <- tyOracle ty_cs
+  return $ case (sat_ty, tmOracle initialTmState tm_cs) of
+    (True, Just tm_state) -> [ValVec patterns (MkDelta ty_cs tm_state)]
+    -- If any of the term/type constraints are non
+    -- satisfiable, the initial uncovered set is empty
+    _non_satisfiable      -> []
   where
-    match_cs     = [ TmConstraint (PmExprVar x) (PmExprLit l)]
-   -- See Note [Representation of Term Equalities]
-    non_match_cs = [ TmConstraint falsePmExpr
-                                  (PmExprEq (PmExprVar x) (PmExprLit l)) ]
-
--- ULitNLit
-uMatcher us gvsa (p@(PmLit l)) ps
-                 (va@(PmNLit { pm_lit_id = x, pm_lit_not = lits })) vsa
-  | all (not . eqPmLit l) lits
-  = mkUnion (uMatcher us gvsa p ps (PmLit l) (mkConstraint match_cs vsa))
-            (non_match_cs `mkConstraint` (PmNLit x (l:lits) `mkCons` vsa))
-  | otherwise = va `mkCons` vsa
+    patterns  = map PmVar vars
+
+-- | Increase the counter for elapsed algorithm iterations, check that the
+-- limit is not exceeded and call `pmcheck`
+pmcheckI :: PatVec -> [PatVec] -> ValVec -> PmM Triple
+pmcheckI ps guards vva = incrCheckPmIterDs >> pmcheck ps guards vva
+{-# INLINE pmcheckI #-}
+
+-- | Increase the counter for elapsed algorithm iterations, check that the
+-- limit is not exceeded and call `pmcheckGuards`
+pmcheckGuardsI :: [PatVec] -> ValVec -> PmM Triple
+pmcheckGuardsI gvs vva = incrCheckPmIterDs >> pmcheckGuards gvs vva
+{-# INLINE pmcheckGuardsI #-}
+
+-- | Increase the counter for elapsed algorithm iterations, check that the
+-- limit is not exceeded and call `pmcheckHd`
+pmcheckHdI :: Pattern -> PatVec -> [PatVec] -> ValAbs -> ValVec -> PmM Triple
+pmcheckHdI p ps guards va vva = incrCheckPmIterDs >>
+                                  pmcheckHd p ps guards va vva
+{-# INLINE pmcheckHdI #-}
+
+-- | Matching function: Check simultaneously a clause (takes separately the
+-- patterns and the list of guards) for exhaustiveness, redundancy and
+-- inaccessibility.
+pmcheck :: PatVec -> [PatVec] -> ValVec -> PmM Triple
+pmcheck [] guards vva@(ValVec [] _)
+  | null guards = return (True, [], False)
+  | otherwise   = pmcheckGuardsI guards vva
+
+-- Guard
+pmcheck (p@(PmGrd pv e) : ps) guards vva@(ValVec vas delta)
+    -- short-circuit if the guard pattern is useless.
+    -- we just have two possible outcomes: fail here or match and recurse
+    -- none of the two contains any useful information about the failure
+    -- though. So just have these two cases but do not do all the boilerplate
+  | isFakeGuard pv e = forces . mkCons vva <$> pmcheckI ps guards vva
+  | otherwise = do
+      y <- mkPmId (pmPatType p)
+      let tm_state = extendSubst y e (delta_tm_cs delta)
+          delta'   = delta { delta_tm_cs = tm_state }
+      utail <$> pmcheckI (pv ++ ps) guards (ValVec (PmVar y : vas) delta')
+
+pmcheck [] _ (ValVec (_:_) _) = panic "pmcheck: nil-cons"
+pmcheck (_:_) _ (ValVec [] _) = panic "pmcheck: cons-nil"
+
+pmcheck (p:ps) guards (ValVec (va:vva) delta)
+  = pmcheckHdI p ps guards va (ValVec vva delta)
+
+-- | Check the list of guards
+pmcheckGuards :: [PatVec] -> ValVec -> PmM Triple
+pmcheckGuards []       vva = return (False, [vva], False)
+pmcheckGuards (gv:gvs) vva = do
+  (cs,  vsa,  ds ) <- pmcheckI gv [] vva
+  (css, vsas, dss) <- runMany (pmcheckGuardsI gvs) vsa
+  return (cs || css, vsas, ds || dss)
+
+-- | Worker function: Implements all cases described in the paper for all three
+-- functions (`covered`, `uncovered` and `divergent`) apart from the `Guard`
+-- cases which are handled by `pmcheck`
+pmcheckHd :: Pattern -> PatVec -> [PatVec] -> ValAbs -> ValVec -> PmM Triple
+
+-- Var
+pmcheckHd (PmVar x) ps guards va (ValVec vva delta)
+  | Just tm_state <- solveOneEq (delta_tm_cs delta)
+                                (PmExprVar (idName x), vaToPmExpr va)
+  = ucon va <$> pmcheckI ps guards (ValVec vva (delta {delta_tm_cs = tm_state}))
+  | otherwise = return (False, [], False)
+
+-- ConCon
+pmcheckHd ( p@(PmCon {pm_con_con = c1, pm_con_args = args1})) ps guards
+          (va@(PmCon {pm_con_con = c2, pm_con_args = args2})) (ValVec vva delta)
+  | c1 /= c2  = return (False, [ValVec (va:vva) delta], False)
+  | otherwise = kcon c1 (pm_con_arg_tys p) (pm_con_tvs p) (pm_con_dicts p)
+                <$> pmcheckI (args1 ++ ps) guards (ValVec (args2 ++ vva) delta)
+
+-- LitLit
+pmcheckHd (PmLit l1) ps guards (va@(PmLit l2)) vva = case eqPmLit l1 l2 of
+  True  -> ucon va <$> pmcheckI ps guards vva
+  False -> return $ ucon va (False, [vva], False)
+
+-- ConVar
+pmcheckHd (p@(PmCon { pm_con_con = con })) ps guards
+          (PmVar x) (ValVec vva delta) = do
+  cons_cs  <- mapM (mkOneConFull x) (allConstructors con)
+  inst_vsa <- flip concatMapM cons_cs $ \(va, tm_ct, ty_cs) -> do
+    let ty_state = ty_cs `unionBags` delta_ty_cs delta -- not actually a state
+    sat_ty <- if isEmptyBag ty_cs then return True
+                                  else tyOracle ty_state
+    return $ case (sat_ty, solveOneEq (delta_tm_cs delta) tm_ct) of
+      (True, Just tm_state) -> [ValVec (va:vva) (MkDelta ty_state tm_state)]
+      _ty_or_tm_failed      -> []
+
+  force_if (canDiverge (idName x) (delta_tm_cs delta)) <$>
+    runMany (pmcheckI (p:ps) guards) inst_vsa
+
+-- LitVar
+pmcheckHd (p@(PmLit l)) ps guards (PmVar x) (ValVec vva delta)
+  = force_if (canDiverge (idName x) (delta_tm_cs delta)) <$>
+      mkUnion non_matched <$>
+        case solveOneEq (delta_tm_cs delta) (mkPosEq x l) of
+          Just tm_state -> pmcheckHdI p ps guards (PmLit l) $
+                             ValVec vva (delta {delta_tm_cs = tm_state})
+          Nothing       -> return (False, [], False)
   where
-    match_cs     = [ TmConstraint (PmExprVar x) (PmExprLit l)]
-   -- See Note [Representation of Term Equalities]
-    non_match_cs = [ TmConstraint falsePmExpr
-                                  (PmExprEq (PmExprVar x) (PmExprLit l)) ]
-
--- Impossible: handled by pmTraverse
-uMatcher _ _ (PmGrd {}) _ _ _ = panic "Check.uMatcher: Guard"
-
--- dMatcher
--- ----------------------------------------------------------------------------
+    us | Just tm_state <- solveOneEq (delta_tm_cs delta) (mkNegEq x l)
+       = [ValVec (PmNLit x [l] : vva) (delta { delta_tm_cs = tm_state })]
+       | otherwise = []
 
--- DVar
-dMatcher us gvsa (PmVar x) ps va vsa
-  = va `mkCons` (cs `mkConstraint` divergent us gvsa ps vsa)
-  where cs = [TmConstraint (PmExprVar x) (valAbsToPmExpr va)]
+    non_matched = (False, us, False)
 
--- DLitCon
-dMatcher us gvsa (PmLit l) ps (va@(PmCon {})) vsa
-  = va `mkCons` (cs `mkConstraint` divergent us gvsa ps vsa)
-  where cs = [ TmConstraint (PmExprLit l) (valAbsToPmExpr va) ]
-
--- DConLit
-dMatcher us gvsa (p@(PmCon { pm_con_con = con })) ps (PmLit l) vsa
-  = dMatcher us3 gvsa p ps con_abs (mkConstraint cs vsa)
-  where
-    (us1, us2, us3)   = splitUniqSupply3 us
-    y                 = mkPmId us1 (pmPatType p)
-    (con_abs, all_cs) = mkOneConFull y us2 con
-    cs = TmConstraint (PmExprVar y) (PmExprLit l) : all_cs
-
--- DConNLit
-dMatcher us gvsa (p@(PmCon { pm_con_con = con })) ps
-                 (PmNLit { pm_lit_id = x }) vsa
-  = dMatcher us2 gvsa p ps con_abs (mkConstraint all_cs vsa)
-  where
-    (us1, us2)        = splitUniqSupply us
-    (con_abs, all_cs) = mkOneConFull x us1 con
-
--- DConCon
-dMatcher us gvsa (p@(PmCon { pm_con_con = c1, pm_con_args = args1 })) ps
-                    (PmCon { pm_con_con = c2, pm_con_args = args2 }) vsa
-  | c1 /= c2  = Empty
-  | otherwise = wrapK c1 (pm_con_arg_tys p)
-                         (pm_con_tvs     p)
-                         (pm_con_dicts   p)
-                         (divergent us gvsa (args1 ++ ps)
-                                            (foldr mkCons vsa args2))
-
--- DLitLit
-dMatcher us gvsa (PmLit l1) ps (va@(PmLit l2)) vsa = case eqPmLit l1 l2 of
-  -- See Note [Undecidable Equality for Overloaded Literals] in PmExpr
-  True  -> va `mkCons` divergent us gvsa ps vsa -- match
-  False -> Empty                                -- mismatch
-
--- DConVar
-dMatcher us gvsa (p@(PmCon { pm_con_con = con })) ps (PmVar x) vsa
-  = mkUnion (PmVar x `mkCons` mkConstraint [BtConstraint x] vsa)
-            (dMatcher us2 gvsa p ps con_abs (mkConstraint all_cs vsa))
+-- LitNLit
+pmcheckHd (p@(PmLit l)) ps guards
+          (PmNLit { pm_lit_id = x, pm_lit_not = lits }) (ValVec vva delta)
+  | all (not . eqPmLit l) lits
+  , Just tm_state <- solveOneEq (delta_tm_cs delta) (mkPosEq x l)
+    -- Both guards check the same so it would be sufficient to have only
+    -- the second one. Nevertheless, it is much cheaper to check whether
+    -- the literal is in the list so we check it first, to avoid calling
+    -- the term oracle (`solveOneEq`) if possible
+  = mkUnion non_matched <$>
+      pmcheckHdI p ps guards (PmLit l)
+                (ValVec vva (delta { delta_tm_cs = tm_state }))
+  | otherwise = return non_matched
   where
-    (us1, us2)        = splitUniqSupply us
-    (con_abs, all_cs) = mkOneConFull x us1 con
+    us | Just tm_state <- solveOneEq (delta_tm_cs delta) (mkNegEq x l)
+       = [ValVec (PmNLit x (l:lits) : vva) (delta { delta_tm_cs = tm_state })]
+       | otherwise = []
 
--- DLitVar
-dMatcher us gvsa (PmLit l) ps (PmVar x) vsa
-  = mkUnion (PmVar x `mkCons` mkConstraint [BtConstraint x] vsa)
-            (dMatcher us gvsa (PmLit l) ps (PmLit l) (mkConstraint cs vsa))
-  where
-    cs = [TmConstraint (PmExprVar x) (PmExprLit l)]
+    non_matched = (False, us, False)
 
--- DLitNLit
-dMatcher us gvsa (p@(PmLit l)) ps
-                 (PmNLit { pm_lit_id = x, pm_lit_not = lits }) vsa
-  | all (not . eqPmLit l) lits
-  = dMatcher us gvsa p ps lit_abs (mkConstraint cs vsa)
-  | otherwise = Empty
-  where
-    lit_abs = PmLit l
-    cs      = [TmConstraint (PmExprVar x) (PmExprLit l)]
+-- ----------------------------------------------------------------------------
+-- The following three can happen only in cases like #322 where constructors
+-- and overloaded literals appear in the same match. The general strategy is
+-- to replace the literal (positive/negative) by a variable and recurse. The
+-- fact that the variable is equal to the literal is recorded in `delta` so
+-- no information is lost
+
+-- LitCon
+pmcheckHd (PmLit l) ps guards (va@(PmCon {})) (ValVec vva delta)
+  = do y <- mkPmId (pmPatType va)
+       let tm_state = extendSubst y (PmExprLit l) (delta_tm_cs delta)
+           delta'   = delta { delta_tm_cs = tm_state }
+       pmcheckHdI (PmVar y) ps guards va (ValVec vva delta')
+
+-- ConLit
+pmcheckHd (p@(PmCon {})) ps guards (PmLit l) (ValVec vva delta)
+  = do y <- mkPmId (pmPatType p)
+       let tm_state = extendSubst y (PmExprLit l) (delta_tm_cs delta)
+           delta'   = delta { delta_tm_cs = tm_state }
+       pmcheckHdI p ps guards (PmVar y) (ValVec vva delta')
+
+-- ConNLit
+pmcheckHd (p@(PmCon {})) ps guards (PmNLit { pm_lit_id = x }) vva
+  = pmcheckHdI p ps guards (PmVar x) vva
+
+-- Impossible: handled by pmcheck
+pmcheckHd (PmGrd {}) _ _ _ _ = panic "pmcheckHd: Guard"
 
--- Impossible: handled by pmTraverse
-dMatcher _ _ (PmGrd {}) _ _ _ = panic "Check.dMatcher: Guard"
+-- ----------------------------------------------------------------------------
+-- * Utilities for main checking
+
+-- | Take the tail of all value vector abstractions in the uncovered set
+utail :: Triple -> Triple
+utail (cs, vsa, ds) = (cs, vsa', ds)
+  where vsa' = [ ValVec vva delta | ValVec (_:vva) delta <- vsa ]
+
+-- | Prepend a value abstraction to all value vector abstractions in the
+-- uncovered set
+ucon :: ValAbs -> Triple -> Triple
+ucon va (cs, vsa, ds) = (cs, vsa', ds)
+  where vsa' = [ ValVec (va:vva) delta | ValVec vva delta <- vsa ]
+
+-- | Given a data constructor of arity `a` and an uncovered set containing
+-- value vector abstractions of length `(a+n)`, pass the first `n` value
+-- abstractions to the constructor (Hence, the resulting value vector
+-- abstractions will have length `n+1`)
+kcon :: DataCon -> [Type] -> [TyVar] -> [EvVar] -> Triple -> Triple
+kcon con arg_tys ex_tvs dicts (cs, vsa, ds)
+  = (cs, [ ValVec (va:vva) delta
+         | ValVec vva' delta <- vsa
+         , let (args, vva) = splitAt n vva'
+         , let va = PmCon { pm_con_con     = con
+                          , pm_con_arg_tys = arg_tys
+                          , pm_con_tvs     = ex_tvs
+                          , pm_con_dicts   = dicts
+                          , pm_con_args    = args } ]
+       , ds)
+  where n = dataConSourceArity con
+
+-- | Get the union of two covered, uncovered and divergent value set
+-- abstractions. Since the covered and divergent sets are represented by a
+-- boolean, union means computing the logical or (at least one of the two is
+-- non-empty).
+mkUnion :: Triple -> Triple -> Triple
+mkUnion (cs1, vsa1, ds1) (cs2, vsa2, ds2)
+  = (cs1 || cs2, vsa1 ++ vsa2, ds1 || ds2)
+
+-- | Add a value vector abstraction to a value set abstraction (uncovered).
+mkCons :: ValVec -> Triple -> Triple
+mkCons vva (cs, vsa, ds) = (cs, vva:vsa, ds)
+
+-- | Set the divergent set to not empty
+forces :: Triple -> Triple
+forces (cs, us, _) = (cs, us, True)
+
+-- | Set the divergent set to non-empty if the flag is `True`
+force_if :: Bool -> Triple -> Triple
+force_if True  (cs,us,_) = (cs,us,True)
+force_if False triple    = triple
 
 -- ----------------------------------------------------------------------------
 -- * Propagation of term constraints inwards when checking nested matches
@@ -1341,10 +1143,9 @@ genCaseTmCs2 :: Maybe (LHsExpr Id) -- Scrutinee
 genCaseTmCs2 Nothing _ _ = return emptyBag
 genCaseTmCs2 (Just scr) [p] [var] = do
   fam_insts <- dsGetFamInstEnvs
-  liftUs $ do
-    [e] <- map valAbsToPmExpr . coercePatVec <$> translatePat fam_insts p
-    let scr_e = lhsExprToPmExpr scr
-    return $ listToBag [(var, e), (var, scr_e)]
+  [e] <- map vaToPmExpr . coercePatVec <$> translatePat fam_insts p
+  let scr_e = lhsExprToPmExpr scr
+  return $ listToBag [(var, e), (var, scr_e)]
 genCaseTmCs2 _ _ _ = panic "genCaseTmCs2: HsCase"
 
 -- | Generate a simple equality when checking a case expression:
@@ -1395,12 +1196,11 @@ Gives the following with the first translation:
 If we use the second translation we get an empty set, independently of the
 oracle. Since the pattern `p' may contain guard patterns though, it cannot be
 used as an expression. That's why we call `coercePatVec' to drop the guard and
-`valAbsToPmExpr' to transform the value abstraction to an expression in the
+`vaToPmExpr' to transform the value abstraction to an expression in the
 guard pattern (value abstractions are a subset of expressions). We keep the
 guards in the first pattern `p' though.
--}
 
-{-
+
 %************************************************************************
 %*                                                                      *
       Pretty printing of exhaustiveness/redundancy check warnings
@@ -1414,24 +1214,27 @@ isAnyPmCheckEnabled :: DynFlags -> DsMatchContext -> Bool
 isAnyPmCheckEnabled dflags (DsMatchContext kind _loc)
   = wopt Opt_WarnOverlappingPatterns dflags || exhaustive dflags kind
 
--- | Issue a warning if the guards are too many and the checker gives up
-warnManyGuards :: DsMatchContext -> DsM ()
-warnManyGuards (DsMatchContext kind loc)
-  = putSrcSpanDs loc $ warnDs $ vcat
-      [ sep [ text "Too many guards in" <+> pprMatchContext kind
-            , text "Guard checking has been over-simplified" ]
-      , parens (text "Use:" <+> (opt_1 $$ opt_2)) ]
-  where
-    opt_1 = hang (text "-Wno-too-many-guards") 2 $
-      text "to suppress this warning"
-    opt_2 = hang (text "-ffull-guard-reasoning") 2 $ vcat
-      [ text "to run the full checker (may increase"
-      , text "compilation time and memory consumption)" ]
-
-dsPmWarn :: DynFlags -> DsMatchContext -> DsM PmResult -> DsM ()
-dsPmWarn dflags ctx@(DsMatchContext kind loc) mPmResult
+instance Outputable ValVec where
+  ppr (ValVec vva delta)
+    = let (residual_eqs, subst) = wrapUpTmState (delta_tm_cs delta)
+          vector                = substInValAbs subst vva
+      in  ppr_uncovered (vector, residual_eqs)
+
+-- | Apply a term substitution to a value vector abstraction. All VAs are
+-- transformed to PmExpr (used only before pretty printing).
+substInValAbs :: PmVarEnv -> [ValAbs] -> [PmExpr]
+substInValAbs subst = map (exprDeepLookup subst . vaToPmExpr)
+
+-- | Wrap up the term oracle's state once solving is complete. Drop any
+-- information about unhandled constraints (involving HsExprs) and flatten
+-- (height 1) the substitution.
+wrapUpTmState :: TmState -> ([ComplexEq], PmVarEnv)
+wrapUpTmState (residual, (_, subst)) = (residual, flattenPmVarEnv subst)
+
+-- | Issue all the warnings (coverage, exhaustiveness, inaccessibility)
+dsPmWarn :: DynFlags -> DsMatchContext -> PmResult -> DsM ()
+dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result
   = when (flag_i || flag_u) $ do
-      (redundant, inaccessible, uncovered) <- mPmResult
       let exists_r = flag_i && notNull redundant
           exists_i = flag_i && notNull inaccessible
           exists_u = flag_u && notNull uncovered
@@ -1439,26 +1242,47 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) mPmResult
       when exists_i $ putSrcSpanDs loc (warnDs (pprEqns  inaccessible imsg))
       when exists_u $ putSrcSpanDs loc (warnDs (pprEqnsU uncovered))
   where
+    (redundant, uncovered, inaccessible) = pm_result
+
     flag_i = wopt Opt_WarnOverlappingPatterns dflags
     flag_u = exhaustive dflags kind
 
     rmsg = "are redundant"
     imsg = "have inaccessible right hand side"
 
-    pprEqns qs text = pp_context ctx (ptext (sLit text)) $ \f ->
+    pprEqns qs txt = pp_context ctx (text txt) $ \f ->
       vcat (map (ppr_eqn f kind) (take maximum_output qs)) $$ dots qs
 
     pprEqnsU qs = pp_context ctx (text "are non-exhaustive") $ \_ ->
       case qs of -- See #11245
-           [([],_)] -> text "Guards do not cover entire pattern space"
-           _missing -> let us = map ppr_uncovered qs
+           [ValVec [] _]
+                    -> text "Guards do not cover entire pattern space"
+           _missing -> let us = map ppr qs
                        in  hang (text "Patterns not matched:") 4
                                 (vcat (take maximum_output us) $$ dots us)
 
+-- | Issue a warning when the predefined number of iterations is exceeded
+-- for the pattern match checker
+warnPmIters :: DynFlags -> DsMatchContext -> PmM ()
+warnPmIters dflags (DsMatchContext kind loc)
+  = when (flag_i || flag_u) $ do
+      iters <- maxPmCheckIterations <$> getDynFlags
+      putSrcSpanDs loc (warnDs (msg iters))
+  where
+    ctxt   = pprMatchContext kind
+    msg is = fsep [ text "Pattern match checker exceeded"
+                  , parens (ppr is), text "iterations in", ctxt <> dot
+                  , text "(Use fmax-pmcheck-iterations=n"
+                  , text "to set the maximun number of iterations to n)" ]
+
+    flag_i = wopt Opt_WarnOverlappingPatterns dflags
+    flag_u = exhaustive dflags kind
+
 dots :: [a] -> SDoc
 dots qs | qs `lengthExceeds` maximum_output = text "..."
         | otherwise                         = empty
 
+-- | Check whether the exhaustiveness checker should run (exhaustiveness only)
 exhaustive :: DynFlags -> HsMatchContext id -> Bool
 exhaustive  dflags (FunRhs {})   = wopt Opt_WarnIncompletePatterns dflags
 exhaustive  dflags CaseAlt       = wopt Opt_WarnIncompletePatterns dflags
@@ -1506,6 +1330,12 @@ ppr_uncovered (expr_vec, complex)
     sdoc_vec = mapM pprPmExprWithParens expr_vec
     (vec,cs) = runPmPprM sdoc_vec (filterComplex complex)
 
+-- | This variable shows the maximum number of lines of output generated for
+-- warnings. It will limit the number of patterns/equations displayed to
+-- maximum_output. (TODO: add command-line option?)
+maximum_output :: Int
+maximum_output = 4
+
 {- Note [Representation of Term Equalities]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 In the paper, term constraints always take the form (x ~ e). Of course, a more
index 92bfde0..3d922f6 100644 (file)
@@ -34,6 +34,9 @@ module DsMonad (
         -- Getting and setting EvVars and term constraints in local environment
         getDictsDs, addDictsDs, getTmCsDs, addTmCsDs,
 
+        -- Iterations for pm checking
+        incrCheckPmIterDs, resetPmIterDs,
+
         -- Warnings
         DsWarning, warnDs, failWithDs, discardWarningsDs,
 
@@ -146,10 +149,12 @@ initDs :: HscEnv
 initDs hsc_env mod rdr_env type_env fam_inst_env thing_inside
   = do  { msg_var <- newIORef (emptyBag, emptyBag)
         ; static_binds_var <- newIORef []
+        ; pm_iter_var      <- newIORef 0
         ; let dflags                   = hsc_dflags hsc_env
               (ds_gbl_env, ds_lcl_env) = mkDsEnvs dflags mod rdr_env type_env
                                                   fam_inst_env msg_var
                                                   static_binds_var
+                                                  pm_iter_var
 
         ; either_res <- initTcRnIf 'd' hsc_env ds_gbl_env ds_lcl_env $
                           loadDAP $
@@ -225,11 +230,12 @@ initDsTc thing_inside
         ; msg_var  <- getErrsVar
         ; dflags   <- getDynFlags
         ; static_binds_var <- liftIO $ newIORef []
+        ; pm_iter_var      <- liftIO $ newIORef 0
         ; let type_env = tcg_type_env tcg_env
               rdr_env  = tcg_rdr_env tcg_env
               fam_inst_env = tcg_fam_inst_env tcg_env
               ds_envs  = mkDsEnvs dflags this_mod rdr_env type_env fam_inst_env
-                                  msg_var static_binds_var
+                                  msg_var static_binds_var pm_iter_var
         ; setEnvs ds_envs thing_inside
         }
 
@@ -258,8 +264,8 @@ initTcDsForSolver thing_inside
 
 mkDsEnvs :: DynFlags -> Module -> GlobalRdrEnv -> TypeEnv -> FamInstEnv
          -> IORef Messages -> IORef [(Fingerprint, (Id, CoreExpr))]
-         -> (DsGblEnv, DsLclEnv)
-mkDsEnvs dflags mod rdr_env type_env fam_inst_env msg_var static_binds_var
+         -> IORef Int -> (DsGblEnv, DsLclEnv)
+mkDsEnvs dflags mod rdr_env type_env fam_inst_env msg_var static_binds_var pmvar
   = let if_genv = IfGblEnv { if_rec_types = Just (mod, return type_env) }
         if_lenv = mkIfLclEnv mod (text "GHC error in desugarer lookup in" <+> ppr mod)
         real_span = realSrcLocSpan (mkRealSrcLoc (moduleNameFS (moduleName mod)) 1 1)
@@ -272,10 +278,11 @@ mkDsEnvs dflags mod rdr_env type_env fam_inst_env msg_var static_binds_var
                            , ds_parr_bi = panic "DsMonad: uninitialised ds_parr_bi"
                            , ds_static_binds = static_binds_var
                            }
-        lcl_env = DsLclEnv { dsl_meta  = emptyNameEnv
-                           , dsl_loc   = real_span
-                           , dsl_dicts = emptyBag
-                           , dsl_tm_cs = emptyBag
+        lcl_env = DsLclEnv { dsl_meta    = emptyNameEnv
+                           , dsl_loc     = real_span
+                           , dsl_dicts   = emptyBag
+                           , dsl_tm_cs   = emptyBag
+                           , dsl_pm_iter = pmvar
                            }
     in (gbl_env, lcl_env)
 
@@ -355,6 +362,24 @@ addTmCsDs :: Bag SimpleEq -> DsM a -> DsM a
 addTmCsDs tm_cs
   = updLclEnv (\env -> env { dsl_tm_cs = unionBags tm_cs (dsl_tm_cs env) })
 
+-- | Check that we have not done more iterations
+-- than we are supposed to and inrease the counter
+
+-- | Increase the counter for elapsed pattern match check iterations.
+-- If the current counter is already over the limit, fail
+incrCheckPmIterDs :: DsM ()
+incrCheckPmIterDs = do
+  env <- getLclEnv
+  cnt <- readTcRef (dsl_pm_iter env)
+  max_iters <- maxPmCheckIterations <$> getDynFlags
+  if cnt >= max_iters
+    then failM
+    else updTcRef (dsl_pm_iter env) (+1)
+
+-- | Reset the counter for pattern match check iterations to zero
+resetPmIterDs :: DsM ()
+resetPmIterDs = do { env <- getLclEnv; writeTcRef (dsl_pm_iter env) 0 }
+
 getSrcSpanDs :: DsM SrcSpan
 getSrcSpanDs = do { env <- getLclEnv
                   ; return (RealSrcSpan (dsl_loc env)) }
index 0128488..be089e6 100644 (file)
@@ -694,21 +694,9 @@ matchWrapper ctxt mb_scr (MG { mg_alts = L _ matches
 
             when (isAnyPmCheckEnabled dflags (DsMatchContext ctxt locn)) $ do
 
-              -- Count the number of guards that can fail
-              guards <- computeNoGuards matches
-
-              let simplify = not (gopt Opt_FullGuardReasoning dflags)
-                              && (guards > maximum_failing_guards)
-
               -- See Note [Type and Term Equality Propagation]
               addTmCsDs (genCaseTmCs1 mb_scr new_vars) $
-                dsPmWarn dflags (DsMatchContext ctxt locn) $
-                  checkMatches simplify new_vars matches
-
-              when (not (gopt Opt_FullGuardReasoning dflags)
-                      && wopt Opt_WarnTooManyGuards dflags
-                      && guards > maximum_failing_guards)
-                   (warnManyGuards (DsMatchContext ctxt locn))
+                checkMatches dflags (DsMatchContext ctxt locn) new_vars matches
 
         ; result_expr <- handleWarnings $
                          matchEquations ctxt new_vars eqns_info rhs_ty
@@ -777,7 +765,7 @@ matchSinglePat (Var var) ctx pat ty match_result
        ; locn   <- getSrcSpanDs
        ; let pat' = getMaybeStrictPat dflags pat
        -- pattern match check warnings
-       ; dsPmWarn dflags (DsMatchContext ctx locn) (checkSingle var pat')
+       ; checkSingle dflags (DsMatchContext ctx locn) var pat'
 
        ; match [var] ty
                [EqnInfo { eqn_pats = [pat'], eqn_rhs  = match_result }] }
index f1f59c1..48044f9 100644 (file)
@@ -7,7 +7,7 @@ Haskell expressions (as used by the pattern matching checker) and utilities.
 {-# LANGUAGE CPP #-}
 
 module PmExpr (
-        PmExpr(..), PmLit(..), SimpleEq, ComplexEq, eqPmLit,
+        PmExpr(..), PmLit(..), SimpleEq, ComplexEq, toComplex, eqPmLit,
         truePmExpr, falsePmExpr, isTruePmExpr, isFalsePmExpr, isNotPmExprOther,
         lhsExprToPmExpr, hsExprToPmExpr, substComplexEq, filterComplex,
         pprPmExprWithParens, runPmPprM
@@ -17,12 +17,13 @@ module PmExpr (
 
 import HsSyn
 import Id
+import Name
+import NameSet
 import DataCon
 import TysWiredIn
 import Outputable
 import Util
 import SrcLoc
-import VarSet
 
 import Data.Maybe (mapMaybe)
 import Data.List (groupBy, sortBy, nubBy)
@@ -50,7 +51,7 @@ refer to variables that are otherwise substituted away.
 -- ** Types
 
 -- | Lifted expressions for pattern match checking.
-data PmExpr = PmExprVar   Id
+data PmExpr = PmExprVar   Name
             | PmExprCon   DataCon [PmExpr]
             | PmExprLit   PmLit
             | PmExprEq    PmExpr PmExpr  -- Syntactic equality
@@ -140,6 +141,10 @@ nubPmLit = nubBy eqPmLit
 type SimpleEq  = (Id, PmExpr) -- We always use this orientation
 type ComplexEq = (PmExpr, PmExpr)
 
+-- | Lift a `SimpleEq` to a `ComplexEq`
+toComplex :: SimpleEq -> ComplexEq
+toComplex (x,e) = (PmExprVar (idName x), e)
+
 -- | Expression `True'
 truePmExpr :: PmExpr
 truePmExpr = PmExprCon trueDataCon []
@@ -193,7 +198,7 @@ isConsDataCon con = consDataCon == con
 
 -- | We return a boolean along with the expression. Hence, if substitution was
 -- a no-op, we know that the expression still cannot progress.
-substPmExpr :: Id -> PmExpr -> PmExpr -> (PmExpr, Bool)
+substPmExpr :: Name -> PmExpr -> PmExpr -> (PmExpr, Bool)
 substPmExpr x e1 e =
   case e of
     PmExprVar z | x == z    -> (e1, True)
@@ -208,7 +213,7 @@ substPmExpr x e1 e =
 
 -- | Substitute in a complex equality. We return (Left eq) if the substitution
 -- affected the equality or (Right eq) if nothing happened.
-substComplexEq :: Id -> PmExpr -> ComplexEq -> Either ComplexEq ComplexEq
+substComplexEq :: Name -> PmExpr -> ComplexEq -> Either ComplexEq ComplexEq
 substComplexEq x e (ex, ey)
   | bx || by  = Left  (ex', ey')
   | otherwise = Right (ex', ey')
@@ -224,7 +229,7 @@ lhsExprToPmExpr (L _ e) = hsExprToPmExpr e
 
 hsExprToPmExpr :: HsExpr Id -> PmExpr
 
-hsExprToPmExpr (HsVar         x) = PmExprVar (unLoc x)
+hsExprToPmExpr (HsVar         x) = PmExprVar (idName (unLoc x))
 hsExprToPmExpr (HsOverLit  olit) = PmExprLit (PmOLit False olit)
 hsExprToPmExpr (HsLit       lit) = PmExprLit (PmSLit lit)
 
@@ -312,7 +317,7 @@ Check.hs) to be more precice.
 -- -----------------------------------------------------------------------------
 -- ** Transform residual constraints in appropriate form for pretty printing
 
-type PmNegLitCt = (Id, (SDoc, [PmLit]))
+type PmNegLitCt = (Name, (SDoc, [PmLit]))
 
 filterComplex :: [ComplexEq] -> [PmNegLitCt]
 filterComplex = zipWith rename nameList . map mkGroup
@@ -342,19 +347,19 @@ filterComplex = zipWith rename nameList . map mkGroup
 runPmPprM :: PmPprM a -> [PmNegLitCt] -> (a, [(SDoc,[PmLit])])
 runPmPprM m lit_env = (result, mapMaybe is_used lit_env)
   where
-    (result, (_lit_env, used)) = runState m (lit_env, emptyVarSet)
+    (result, (_lit_env, used)) = runState m (lit_env, emptyNameSet)
 
     is_used (x,(name, lits))
-      | elemVarSet x used = Just (name, lits)
+      | elemNameSet x used = Just (name, lits)
       | otherwise         = Nothing
 
-type PmPprM a = State ([PmNegLitCt], IdSet) a
+type PmPprM a = State ([PmNegLitCt], NameSet) a
 -- (the first part of the state is read only. make it a reader?)
 
-addUsed :: Id -> PmPprM ()
-addUsed x = modify (\(negated, used) -> (negated, extendVarSet used x))
+addUsed :: Name -> PmPprM ()
+addUsed x = modify (\(negated, used) -> (negated, extendNameSet used x))
 
-checkNegation :: Id -> PmPprM (Maybe SDoc) -- the clean name if it is negated
+checkNegation :: Name -> PmPprM (Maybe SDoc) -- the clean name if it is negated
 checkNegation x = do
   negated <- gets fst
   return $ case lookup x negated of
index 5d7a61a..05966cd 100644 (file)
@@ -10,14 +10,14 @@ module TmOracle (
 
         -- re-exported from PmExpr
         PmExpr(..), PmLit(..), SimpleEq, ComplexEq, PmVarEnv, falsePmExpr,
-        canDiverge, eqPmLit, filterComplex, isNotPmExprOther, runPmPprM,
-        pprPmExprWithParens, lhsExprToPmExpr, hsExprToPmExpr,
+        eqPmLit, filterComplex, isNotPmExprOther, runPmPprM, lhsExprToPmExpr,
+        hsExprToPmExpr, pprPmExprWithParens,
 
         -- the term oracle
-        tmOracle, TmState, initialTmState,
+        tmOracle, TmState, initialTmState, solveOneEq, extendSubst, canDiverge,
 
         -- misc.
-        exprDeepLookup, pmLitType, flattenPmVarEnv
+        toComplex, exprDeepLookup, pmLitType, flattenPmVarEnv
     ) where
 
 #include "HsVersions.h"
@@ -25,6 +25,7 @@ module TmOracle (
 import PmExpr
 
 import Id
+import Name
 import TysWiredIn
 import Type
 import HsLit
@@ -43,7 +44,7 @@ import qualified Data.Map as Map
 -}
 
 -- | The type of substitutions.
-type PmVarEnv = Map.Map Id PmExpr
+type PmVarEnv = Map.Map Name PmExpr
 
 -- | The environment of the oracle contains
 --     1. A Bool (are there any constraints we cannot handle? (PmExprOther)).
@@ -52,7 +53,7 @@ type TmOracleEnv = (Bool, PmVarEnv)
 
 -- | Check whether a constraint (x ~ BOT) can succeed,
 -- given the resulting state of the term oracle.
-canDiverge :: Id -> TmState -> Bool
+canDiverge :: Name -> TmState -> Bool
 canDiverge x (standby, (_unhandled, env))
   -- If the variable seems not evaluated, there is a possibility for
   -- constraint x ~ BOT to be satisfiable.
@@ -66,11 +67,11 @@ canDiverge x (standby, (_unhandled, env))
   | otherwise = False
 
   where
-    isForcedByEq :: Id -> ComplexEq -> Bool
+    isForcedByEq :: Name -> ComplexEq -> Bool
     isForcedByEq y (e1, e2) = varIn y e1 || varIn y e2
 
 -- | Check whether a variable is in the free variables of an expression
-varIn :: Id -> PmExpr -> Bool
+varIn :: Name -> PmExpr -> Bool
 varIn x e = case e of
   PmExprVar y    -> x == y
   PmExprCon _ es -> any (x `varIn`) es
@@ -131,7 +132,7 @@ solveComplexEq solver_state@(standby, (unhandled, env)) eq@(e1, e2) = case eq of
   _ -> Just (standby, (True, env)) -- I HATE CATCH-ALLS
 
 -- | Extend the substitution and solve the (possibly updated) constraints.
-extendSubstAndSolve :: Id -> PmExpr -> TmState -> Maybe TmState
+extendSubstAndSolve :: Name -> PmExpr -> TmState -> Maybe TmState
 extendSubstAndSolve x e (standby, (unhandled, env))
   = foldlM solveComplexEq new_incr_state (map simplifyComplexEq changed)
   where
@@ -142,6 +143,19 @@ extendSubstAndSolve x e (standby, (unhandled, env))
     (changed, unchanged) = partitionWith (substComplexEq x e) standby
     new_incr_state       = (unchanged, (unhandled, Map.insert x e env))
 
+-- | When we know that a variable is fresh, we do not actually have to
+-- check whether anything changes, we know that nothing does. Hence,
+-- `extendSubst` simply extends the substitution, unlike what
+-- `extendSubstAndSolve` does.
+extendSubst :: Id -> PmExpr -> TmState -> TmState
+extendSubst y e (standby, (unhandled, env))
+  | isNotPmExprOther simpl_e
+  = (standby, (unhandled, Map.insert x simpl_e env))
+  | otherwise = (standby, (True, env))
+  where
+    x = idName y
+    simpl_e = fst $ simplifyPmExpr $ exprDeepLookup env e
+
 -- | Simplify a complex equality.
 simplifyComplexEq :: ComplexEq -> ComplexEq
 simplifyComplexEq (e1, e2) = (fst $ simplifyPmExpr e1, fst $ simplifyPmExpr e2)
@@ -204,7 +218,7 @@ applySubstComplexEq :: PmVarEnv -> ComplexEq -> ComplexEq
 applySubstComplexEq env (e1,e2) = (exprDeepLookup env e1, exprDeepLookup env e2)
 
 -- | Apply an (un-flattened) substitution to a variable.
-varDeepLookup :: PmVarEnv -> Id -> PmExpr
+varDeepLookup :: PmVarEnv -> Name -> PmExpr
 varDeepLookup env x
   | Just e <- Map.lookup x env = exprDeepLookup env e -- go deeper
   | otherwise                  = PmExprVar x          -- terminal
index d7922c5..1832ea4 100644 (file)
@@ -1,7 +1,4 @@
 {-# LANGUAGE CPP, ScopedTypeVariables, MagicHash, UnboxedTuples #-}
-#if __GLASGOW_HASKELL__ > 710
-{-# OPTIONS_GHC -ffull-guard-reasoning #-}
-#endif
 
 -----------------------------------------------------------------------------
 --
index 13f3bd7..992f47d 100644 (file)
@@ -531,9 +531,6 @@ data GeneralFlag
    -- safe haskell flags
    | Opt_DistrustAllPackages
    | Opt_PackageTrust
-
-   -- pm checking with guards
-   | Opt_FullGuardReasoning
    deriving (Eq, Show, Enum)
 
 data WarningFlag =
@@ -555,7 +552,6 @@ data WarningFlag =
    | Opt_WarnMissingLocalSigs
    | Opt_WarnNameShadowing
    | Opt_WarnOverlappingPatterns
-   | Opt_WarnTooManyGuards
    | Opt_WarnTypeDefaults
    | Opt_WarnMonomorphism
    | Opt_WarnUnusedTopBinds
@@ -645,6 +641,7 @@ data DynFlags = DynFlags {
   debugLevel            :: Int,         -- ^ How much debug information to produce
   simplPhases           :: Int,         -- ^ Number of simplifier phases
   maxSimplIterations    :: Int,         -- ^ Max simplifier iterations
+  maxPmCheckIterations  :: Int,         -- ^ Max no iterations for pm checking
   ruleCheck             :: Maybe String,
   strictnessBefore      :: [Int],       -- ^ Additional demand analysis
 
@@ -1438,6 +1435,7 @@ defaultDynFlags mySettings =
         debugLevel              = 0,
         simplPhases             = 2,
         maxSimplIterations      = 4,
+        maxPmCheckIterations    = 10000000,
         ruleCheck               = Nothing,
         maxRelevantBinds        = Just 6,
         simplTickFactor         = 100,
@@ -2632,6 +2630,8 @@ dynamic_flags = [
       (intSuffix (\n d -> d{ simplPhases = n }))
   , defFlag "fmax-simplifier-iterations"
       (intSuffix (\n d -> d{ maxSimplIterations = n }))
+  , defFlag "fmax-pmcheck-iterations"
+      (intSuffix (\n d -> d{ maxPmCheckIterations = n }))
   , defFlag "fsimpl-tick-factor"
       (intSuffix (\n d -> d{ simplTickFactor = n }))
   , defFlag "fspec-constr-threshold"
@@ -2980,7 +2980,6 @@ wWarningFlags = [
   flagSpec "orphans"                     Opt_WarnOrphans,
   flagSpec "overflowed-literals"         Opt_WarnOverflowedLiterals,
   flagSpec "overlapping-patterns"        Opt_WarnOverlappingPatterns,
-  flagSpec "too-many-guards"             Opt_WarnTooManyGuards,
   flagSpec "missed-specialisations"      Opt_WarnMissedSpecs,
   flagSpec "all-missed-specialisations"  Opt_WarnAllMissedSpecs,
   flagSpec' "safe"                       Opt_WarnSafe setWarnSafe,
@@ -3117,8 +3116,7 @@ fFlags = [
   flagSpec "unbox-strict-fields"              Opt_UnboxStrictFields,
   flagSpec "vectorisation-avoidance"          Opt_VectorisationAvoidance,
   flagSpec "vectorise"                        Opt_Vectorise,
-  flagSpec "worker-wrapper"                   Opt_WorkerWrapper,
-  flagSpec "full-guard-reasoning"             Opt_FullGuardReasoning
+  flagSpec "worker-wrapper"                   Opt_WorkerWrapper
   ]
 
 -- | These @-f\<blah\>@ flags can all be reversed with @-fno-\<blah\>@
index 6ba1f8a..40e4e7d 100644 (file)
@@ -1,9 +1,5 @@
 -- | Constants describing the DWARF format. Most of this simply
 -- mirrors /usr/include/dwarf.h.
-{-# LANGUAGE CPP #-}
-#if __GLASGOW_HASKELL__ > 710
-{-# OPTIONS_GHC -ffull-guard-reasoning #-}
-#endif
 
 module Dwarf.Constants where
 
index 9ede73d..151e370 100644 (file)
@@ -338,7 +338,8 @@ data DsLclEnv = DsLclEnv {
         dsl_meta    :: DsMetaEnv,        -- Template Haskell bindings
         dsl_loc     :: RealSrcSpan,      -- To put in pattern-matching error msgs
         dsl_dicts   :: Bag EvVar,        -- Constraints from GADT pattern-matching
-        dsl_tm_cs   :: Bag SimpleEq
+        dsl_tm_cs   :: Bag SimpleEq,
+        dsl_pm_iter :: IORef Int         -- no iterations for pmcheck
      }
 
 -- Inside [| |] brackets, the desugarer looks
index 2af66f6..fc6da62 100644 (file)
@@ -2,9 +2,7 @@
 
 {-# LANGUAGE CPP #-}
  -- This module used to take 10GB of memory to compile with the new
- -- (Nov '15) pattern-match check. In order to be able to compile it,
- -- do not enable -ffull-guard-reasoning. Instead, simplify the guards
- -- (default behaviour when guards are too many).
+ -- (Nov '15) pattern-match checker.
 
 module OptCoercion ( optCoercion, checkAxInstCo ) where
 
index 9159026..10eab70 100644 (file)
@@ -287,15 +287,6 @@ Compiler
    warns in the case of unused term-level patterns. Both flags are implied by
    :ghc-flag:`-W`.
 
--  Added the :ghc-flag:`-Wtoo-many-guards` flag. When enabled, this will issue a
-   warning if a pattern match contains too many guards (over 20 at the
-   moment). Makes a difference only if pattern match checking is also enabled.
-
--  Added the :ghc-flag:`-ffull-guard-reasoning` flag. When enabled, pattern match
-   checking tries its best to reason about guards. Since the additional
-   expressivity may come with a high price in terms of compilation time and
-   memory consumption, it is turned off by default.
-
 -  :ghc-flag:`-this-package-key` has been renamed again (hopefully for the last time!)
    to :ghc-flag:`-this-unit-id`.  The renaming was motivated by the fact that
    the identifier you pass to GHC here doesn't have much to do with packages:
index 8304e25..f0c522c 100644 (file)
@@ -358,16 +358,6 @@ Bugs in GHC
    This flag ensures that yield points are inserted at every function entrypoint
    (at the expense of a bit of performance).
 
--  GHC's updated exhaustiveness and coverage checker (see
-   :ref:`options-sanity`) is quite expressive but with a rather high
-   performance cost (in terms of both time and memory consumption), mainly
-   due to guards. Two flags have been introduced to give more control to
-   the user over guard reasoning: :ghc-flag:`-Wtoo-many-guards`
-   and :ghc-flag:`-ffull-guard-reasoning` (see :ref:`options-sanity`).
-   When :ghc-flag:`-ffull-guard-reasoning` is on, pattern match checking for guards
-   runs in full power, which may run out of memory/substantially increase
-   compilation time.
-
 -  GHC does not allow you to have a data type with a context that
    mentions type variables that are not data type parameters. For
    example:
index afcee5b..7fd2019 100644 (file)
@@ -527,40 +527,6 @@ of ``-W(no-)*``.
     This option isn't enabled by default because it can be very noisy,
     and it often doesn't indicate a bug in the program.
 
-.. ghc-flag:: -Wtoo-many-guards
-              -Wno-too-many-guards
-
-    .. index::
-       single: too many guards, warning
-
-    The option :ghc-flag:`-Wtoo-many-guards` warns about places where a
-    pattern match contains too many guards (over 20 at the moment).
-    It has an effect only if any form of exhaustivness/overlapping
-    checking is enabled (one of
-    :ghc-flag:`-Wincomplete-patterns`,
-    :ghc-flag:`-Wincomplete-uni-patterns`,
-    :ghc-flag:`-Wincomplete-record-updates`,
-    :ghc-flag:`-Woverlapping-patterns`). When enabled, the warning can be
-    suppressed by enabling either :ghc-flag:`-Wno-too-many-guards`, which just
-    hides the warning, or :ghc-flag:`-ffull-guard-reasoning` which runs the
-    full check, independently of the number of guards.
-
-.. ghc-flag:: -ffull-guard-reasoning
-
-    :implies: :ghc-flag:`-Wno-too-many-guards`
-
-    .. index::
-       single: guard reasoning, warning
-
-    The option :ghc-flag:`-ffull-guard-reasoning` forces pattern match checking
-    to run in full. This gives more precise warnings concerning pattern
-    guards but in most cases increases memory consumption and
-    compilation time. Hence, it is off by default. Enabling
-    :ghc-flag:`-ffull-guard-reasoning` also implies :ghc-flag:`-Wno-too-many-guards`.
-    Note that (like :ghc-flag:`-Wtoo-many-guards`) :ghc-flag:`-ffull-guard-reasoning`
-    makes a difference only if pattern match checking is already
-    enabled.
-
 .. ghc-flag:: -Wmissing-fields
 
     .. index::
index 4607c37..7614351 100644 (file)
@@ -1,6 +1,5 @@
 {-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE CPP, NoImplicitPrelude #-}
-{-# OPTIONS_GHC -ffull-guard-reasoning #-}
 
 -----------------------------------------------------------------------------
 -- |
index 13ac9b8..7699aff 100644 (file)
@@ -430,7 +430,7 @@ test('T783',
             # 2014-09-03: 223377364 (Windows) better specialisation, raft of core-to-core optimisations
             # 2014-12-22: 235002220 (Windows) not sure why
 
-           (wordsize(64), 1134085384, 10)]),
+           (wordsize(64), 488592288, 10)]),
             # prev:       349263216 (amd64/Linux)
             # 07/08/2012: 384479856 (amd64/Linux)
             # 29/08/2012: 436927840 (amd64/Linux)
@@ -457,6 +457,8 @@ test('T783',
             #    (D757: Emit Typeable instances at site of type definition)
             # 2015-12-04: 1134085384 (amd64/Linux)
             #    (D1535: Major overhaul of pattern match checker, #11162)
+            # 2016-02-03: 488592288 (amd64/Linux)
+            #    (D1795: Another overhaul of pattern match checker, #11374)
       extra_hc_opts('-static')
       ],
       compile,[''])
diff --git a/testsuite/tests/pmcheck/should_compile/T11195.hs b/testsuite/tests/pmcheck/should_compile/T11195.hs
new file mode 100644 (file)
index 0000000..593223f
--- /dev/null
@@ -0,0 +1,189 @@
+{-# OPTIONS_GHC -Woverlapping-patterns -Wincomplete-patterns #-}
+
+module T11195 where
+
+import TyCoRep
+import Coercion
+import Type hiding( substTyVarBndr, substTy, extendTCvSubst )
+import TcType       ( exactTyCoVarsOfType )
+import CoAxiom
+import VarSet
+import VarEnv
+import Pair
+import InstEnv
+
+type NormalCo    = Coercion
+type NormalNonIdCo = NormalCo  -- Extra invariant: not the identity
+type SymFlag = Bool
+type ReprFlag = Bool
+
+chooseRole :: ReprFlag -> Role -> Role
+chooseRole = undefined
+
+wrapRole :: ReprFlag -> Role -> Coercion -> Coercion
+wrapRole = undefined
+
+wrapSym :: SymFlag -> Coercion -> Coercion
+wrapSym = undefined
+
+optForAllCoBndr :: LiftingContext -> Bool
+                -> TyVar -> Coercion -> (LiftingContext, TyVar, Coercion)
+optForAllCoBndr = undefined
+
+opt_trans :: InScopeSet -> NormalCo -> NormalCo -> NormalCo
+opt_trans = undefined
+
+opt_univ :: LiftingContext -> SymFlag -> UnivCoProvenance -> Role
+         -> Type -> Type -> Coercion
+opt_univ = undefined
+
+opt_co3 :: LiftingContext -> SymFlag -> Maybe Role
+        -> Role -> Coercion -> NormalCo
+opt_co3 = undefined
+
+opt_co2 :: LiftingContext -> SymFlag -> Role -> Coercion -> NormalCo
+opt_co2 = undefined
+
+compatible_co :: Coercion -> Coercion -> Bool
+compatible_co = undefined
+
+etaTyConAppCo_maybe = undefined
+etaAppCo_maybe = undefined
+etaForAllCo_maybe = undefined
+
+matchAxiom = undefined
+checkAxInstCo = undefined
+isAxiom_maybe = undefined
+isCohLeft_maybe = undefined
+isCohRight_maybe = undefined
+
+opt_transList :: InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
+opt_transList is = zipWith (opt_trans is)
+
+opt_trans_rule :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
+opt_trans_rule is in_co1@(NthCo d1 co1) in_co2@(NthCo d2 co2)
+  | d1 == d2
+  , co1 `compatible_co` co2 = undefined
+
+opt_trans_rule is in_co1@(LRCo d1 co1) in_co2@(LRCo d2 co2)
+  | d1 == d2
+  , co1 `compatible_co` co2 = undefined
+
+-- Push transitivity inside instantiation
+opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
+  | ty1 `eqCoercion` ty2
+  , co1 `compatible_co` co2 = undefined
+
+opt_trans_rule is in_co1@(UnivCo p1 r1 tyl1 _tyr1)
+                  in_co2@(UnivCo p2 r2 _tyl2 tyr2)
+  | Just prov' <- opt_trans_prov p1 p2 = undefined
+  where
+    -- if the provenances are different, opt'ing will be very confusing
+    opt_trans_prov UnsafeCoerceProv UnsafeCoerceProv
+      = Just UnsafeCoerceProv
+    opt_trans_prov (PhantomProv kco1) (PhantomProv kco2)
+      = Just $ PhantomProv $ opt_trans is kco1 kco2
+    opt_trans_prov (ProofIrrelProv kco1) (ProofIrrelProv kco2)
+      = Just $ ProofIrrelProv $ opt_trans is kco1 kco2
+    opt_trans_prov (PluginProv str1) (PluginProv str2)
+      | str1 == str2 = Just p1
+    opt_trans_prov _ _ = Nothing
+
+-- Push transitivity down through matching top-level constructors.
+opt_trans_rule is in_co1@(TyConAppCo r1 tc1 cos1)
+                  in_co2@(TyConAppCo r2 tc2 cos2)
+  | tc1 == tc2 = undefined
+
+opt_trans_rule is in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)
+  = undefined
+
+-- Eta rules
+opt_trans_rule is co1@(TyConAppCo r tc cos1) co2
+  | Just cos2 <- etaTyConAppCo_maybe tc co2 = undefined
+
+opt_trans_rule is co1 co2@(TyConAppCo r tc cos2)
+  | Just cos1 <- etaTyConAppCo_maybe tc co1 = undefined
+
+opt_trans_rule is co1@(AppCo co1a co1b) co2
+  | Just (co2a,co2b) <- etaAppCo_maybe co2 = undefined
+
+opt_trans_rule is co1 co2@(AppCo co2a co2b)
+  | Just (co1a,co1b) <- etaAppCo_maybe co1 = undefined
+
+-- Push transitivity inside forall
+opt_trans_rule is co1 co2
+  | ForAllCo tv1 eta1 r1 <- co1
+  , Just (tv2,eta2,r2) <- etaForAllCo_maybe co2 = undefined
+
+  | ForAllCo tv2 eta2 r2 <- co2
+  , Just (tv1,eta1,r1) <- etaForAllCo_maybe co1 = undefined
+
+  where
+  push_trans tv1 eta1 r1 tv2 eta2 r2 = undefined
+
+-- Push transitivity inside axioms
+opt_trans_rule is co1 co2
+  | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
+  , True <- sym
+  , Just cos2 <- matchAxiom sym con ind co2
+  , let newAxInst = AxiomInstCo con ind
+                      (opt_transList is (map mkSymCo cos2) cos1)
+  , Nothing <- checkAxInstCo newAxInst
+  = undefined
+
+  -- TrPushAxR
+  | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
+  , False <- sym
+  , Just cos2 <- matchAxiom sym con ind co2
+  , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
+  , Nothing <- checkAxInstCo newAxInst
+  = undefined
+
+  -- TrPushSymAxL
+  | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
+  , True <- sym
+  , Just cos1 <- matchAxiom (not sym) con ind co1
+  , let newAxInst = AxiomInstCo con ind
+                      (opt_transList is cos2 (map mkSymCo cos1))
+  , Nothing <- checkAxInstCo newAxInst
+  = undefined
+
+  -- TrPushAxL
+  | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
+  , False <- sym
+  , Just cos1 <- matchAxiom (not sym) con ind co1
+  , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
+  , Nothing <- checkAxInstCo newAxInst
+  = undefined
+
+  -- TrPushAxSym/TrPushSymAx
+  | Just (sym1, con1, ind1, cos1) <- co1_is_axiom_maybe
+  , Just (sym2, con2, ind2, cos2) <- co2_is_axiom_maybe
+  , con1 == con2
+  , ind1 == ind2
+  , sym1 == not sym2
+  , let branch = coAxiomNthBranch con1 ind1
+        qtvs = coAxBranchTyVars branch ++ coAxBranchCoVars branch
+        lhs  = coAxNthLHS con1 ind1
+        rhs  = coAxBranchRHS branch
+        pivot_tvs = exactTyCoVarsOfType (if sym2 then rhs else lhs)
+  , all (`elemVarSet` pivot_tvs) qtvs
+  = undefined
+  where
+    co1_is_axiom_maybe = isAxiom_maybe co1
+    co2_is_axiom_maybe = isAxiom_maybe co2
+    role = coercionRole co1 -- should be the same as coercionRole co2!
+
+opt_trans_rule is co1 co2
+  | Just (lco, lh) <- isCohRight_maybe co1
+  , Just (rco, rh) <- isCohLeft_maybe co2
+  , (coercionType lh) `eqType` (coercionType rh)
+  = undefined
+
+opt_trans_rule _ co1 co2        -- Identity rule
+  | (Pair ty1 _, r) <- coercionKindRole co1
+  , Pair _ ty2 <- coercionKind co2
+  , ty1 `eqType` ty2
+  = undefined
+
+opt_trans_rule _ _ _ = Nothing
diff --git a/testsuite/tests/pmcheck/should_compile/T11303b.hs b/testsuite/tests/pmcheck/should_compile/T11303b.hs
new file mode 100644 (file)
index 0000000..f8c4917
--- /dev/null
@@ -0,0 +1,25 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# OPTIONS_GHC -Wincomplete-patterns -Woverlapping-patterns #-}
+
+module T11303b where
+
+data family Letter a
+
+data instance Letter a = A | B | C | D | E | F | G | H | I | J
+
+f :: [Letter a] -> Int
+f = foldl go 0
+  where
+    go n letter = n + n'
+      where
+        n' = case letter of
+                  A -> 0
+                  B -> 1
+                  C -> 2
+                  D -> 3
+                  E -> 4
+                  F -> 5
+                  G -> 6
+                  H -> 7
+                  I -> 8
+                  J -> 9
diff --git a/testsuite/tests/pmcheck/should_compile/T11374.hs b/testsuite/tests/pmcheck/should_compile/T11374.hs
new file mode 100644 (file)
index 0000000..e68fbc8
--- /dev/null
@@ -0,0 +1,59 @@
+{-# LANGUAGE Haskell2010 #-}
+{-# OPTIONS_GHC -Woverlapping-patterns -Wincomplete-patterns #-}
+
+module T11374 where
+
+data Type   = TCon TCon [Type]
+            | TUser String [Type] Type
+            | TRec [(String,Type)]
+            deriving (Show,Eq,Ord)
+
+data TCon   = TC TC
+            | TF TFun
+            deriving (Show,Eq,Ord)
+
+data TC     = TCNum Integer
+            | TCInf
+            | TCBit
+            | TCSeq
+            | TCFun
+            | TCTuple Int
+            deriving (Show,Eq,Ord)
+
+data TFun   = TCAdd
+            | TCSub
+            | TCMul
+            | TCDiv
+            | TCMod
+            | TCLg2
+            | TCExp
+            | TCWidth
+            | TCMin
+            | TCMax
+            | TCLenFromThen
+            | TCLenFromThenTo
+            deriving (Show, Eq, Ord, Bounded, Enum)
+
+simpFinTy :: Type -> Maybe [Type]
+simpFinTy ty = case ty of
+    TCon (TC (TCNum _)) _ -> Just []
+
+    TCon (TF tf) [t1]
+      | TCLg2    <- tf -> Just [t1]
+      | TCWidth  <- tf -> Just [t1]
+
+    TCon (TF tf) [t1,t2]
+      | TCAdd <- tf -> Just [t1, t2]
+      | TCSub <- tf -> Just [t1]
+      | TCMul <- tf -> Just [t1, t2]
+      | TCDiv <- tf -> Just [t1]
+      | TCMod <- tf -> Just []
+      | TCExp <- tf -> Just [t1, t2]
+      | TCMin <- tf -> Nothing
+      | TCMax <- tf -> Just [t1, t2]
+
+    TCon (TF tf) [_,_,_]
+      | TCLenFromThen   <- tf -> Just []
+      | TCLenFromThenTo <- tf -> Just []
+
+    _ -> Nothing
index e6ad7cf..d2e6e0a 100644 (file)
@@ -2,10 +2,10 @@ T2204.hs:6:1: warning:
     Pattern match(es) are non-exhaustive
     In an equation for ‘f’:
         Patterns not matched:
-            ('0':'1':_:_)
-            ('0':p:_) where p is not one of {'1'}
-            ['0']
+            []
             (p:_) where p is not one of {'0'}
+            ['0']
+            ('0':p:_) where p is not one of {'1'}
             ...
 
 T2204.hs:9:1: warning:
index 6a9d0ce..b998ce2 100644 (file)
@@ -2,8 +2,8 @@ T9951b.hs:7:1: warning:
     Pattern match(es) are non-exhaustive
     In an equation for ‘f’:
         Patterns not matched:
-            ('a':'b':_:_)
-            ('a':p:_) where p is not one of {'b'}
-            ['a']
+            []
             (p:_) where p is not one of {'a'}
+            ['a']
+            ('a':p:_) where p is not one of {'b'}
             ...
index 521c221..84c2d61 100644 (file)
@@ -24,6 +24,9 @@ test('T9951b',only_compiler_types(['ghc']), compile, ['-fwarn-incomplete-pattern
 test('T9951', only_compiler_types(['ghc']), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T11303', normal, compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns +RTS -M1G -RTS'])
 test('T11276', compile_timeout_multiplier(0.01), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns +RTS -M1G -RTS'])
+test('T11303b', compile_timeout_multiplier(0.01), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns +RTS -M1G -RTS'])
+test('T11374', compile_timeout_multiplier(0.01), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns +RTS -M1G -RTS'])
+test('T11195', compile_timeout_multiplier(0.40), compile, ['-package ghc -fwarn-incomplete-patterns -fwarn-overlapping-patterns +RTS -M1G -RTS'])
 
 # Other tests
 test('pmc001', only_compiler_types(['ghc']), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
index c614543..eb0bd4b 100644 (file)
@@ -2,16 +2,16 @@ pmc001.hs:14:1: warning:
     Pattern match(es) are non-exhaustive
     In an equation for ‘f’:
         Patterns not matched:
-            MkT3 (MkT2 _)
-            MkT3 MkT1
-            (MkT2 _) MkT3
             MkT1 MkT3
+            (MkT2 _) MkT3
+            MkT3 MkT1
+            MkT3 (MkT2 _)
 
 pmc001.hs:19:1: warning:
     Pattern match(es) are non-exhaustive
     In an equation for ‘g’:
         Patterns not matched:
-            MkT3 (MkT2 _)
-            MkT3 MkT1
-            (MkT2 _) MkT3
             MkT1 MkT3
+            (MkT2 _) MkT3
+            MkT3 MkT1
+            MkT3 (MkT2 _)
index bb011be..291fbdc 100644 (file)
@@ -7,18 +7,18 @@ pmc007.hs:12:1: warning:
     Pattern match(es) are non-exhaustive
     In an equation for ‘g’:
         Patterns not matched:
-            ('a':'b':_:_)
-            ('a':'c':_:_)
-            ('a':p:_) where p is not one of {'c', 'b'}
+            []
+            (p:_) where p is not one of {'a'}
             ['a']
+            ('a':p:_) where p is not one of {'c', 'b'}
             ...
 
 pmc007.hs:18:11: warning:
     Pattern match(es) are non-exhaustive
     In a case alternative:
         Patterns not matched:
-            ('a':'b':_:_)
-            ('a':'c':_:_)
-            ('a':p:_) where p is not one of {'c', 'b'}
+            []
+            (p:_) where p is not one of {'a'}
             ['a']
+            ('a':p:_) where p is not one of {'c', 'b'}
             ...
index 3fa9bf0..de5e159 100644 (file)
@@ -237,11 +237,6 @@ warningsOptions =
          , flagType = DynamicFlag
          , flagReverse = "-Wno-tabs"
          }
-  , flag { flagName = "-Wtoo-many-guards"
-         , flagDescription = "warn when a match has too many guards"
-         , flagType = DynamicFlag
-         , flagReverse = "-Wno-too-many-guards"
-         }
   , flag { flagName = "-Wtype-defaults"
          , flagDescription = "warn when defaulting happens"
          , flagType = DynamicFlag
@@ -397,12 +392,4 @@ warningsOptions =
          , flagType = DynamicFlag
          , flagReverse = "-Wno-deriving-typeable"
          }
-  , flag { flagName = "-ffull-guard-reasoning"
-         , flagDescription =
-           "enable the full reasoning of the pattern match checker "++
-           "concerning guards, for more precise exhaustiveness/coverage "++
-           "warnings"
-         , flagType = DynamicFlag
-         , flagReverse = "-fno-full-guard-reasoning"
-         }
   ]