Major Overhaul of Pattern Match Checking (Fixes #595)

This patch adresses several problems concerned with exhaustiveness and
redundancy checking of pattern matching. The list of improvements includes:

* Making the check type-aware (handles GADTs, Type Families, DataKinds, etc.).
  This fixes #4139, #3927, #8970 and other related tickets.

* Making the check laziness-aware. Cases that are overlapped but affect
  evaluation are issued now with "Patterns have inaccessible right hand side".
  Additionally, "Patterns are overlapped" is now replaced by "Patterns are
  redundant".

* Improved messages for literals. This addresses tickets #5724, #2204, etc.

* Improved reasoning concerning cases where simple and overloaded
  patterns are matched (See #322).

* Substantially improved reasoning for pattern guards. Addresses #3078.

* OverloadedLists extension does not break exhaustiveness checking anymore
  (addresses #9951). Note that in general this cannot be handled but if we know
  that an argument has type '[a]', we treat it as a list since, the instance of
  'IsList' gives the identity for both 'fromList' and 'toList'. If the type is
  not clear or is not the list type, then the check cannot do much still. I am
  a bit concerned about OverlappingInstances though, since one may override the
  '[a]' instance with e.g. an '[Int]' instance that is not the identity.

* Improved reasoning for nested pattern matching (partial solution). Now we
  propagate type and (some) term constraints deeper when checking, so we can
  detect more inconsistencies. For example, this is needed for #4139.

I am still not satisfied with several things but I would like to address at
least the following before the next release:
    Term constraints are too many and not printed for non-exhaustive matches
(with the exception of literals). This sometimes results in two identical (in
appearance) uncovered warnings. Unless we actually show their difference, I
would like to have a single warning.

23 files changed, 2483 insertions, 860 deletions

diff --git a/compiler/basicTypes/UniqSupply.hs b/compiler/basicTypes/UniqSupply.hs
index afc4d3c171..16734bc78f 100644
--- a/compiler/basicTypes/UniqSupply.hs
+++ b/compiler/basicTypes/UniqSupply.hs
@@ -15,13 +15,15 @@ module UniqSupply (
 
         mkSplitUniqSupply,
         splitUniqSupply, listSplitUniqSupply,
+        splitUniqSupply3, splitUniqSupply4,
 
         -- * Unique supply monad and its abstraction
-        UniqSM, MonadUnique(..),
+        UniqSM, MonadUnique(..), liftUs,
 
         -- ** Operations on the monad
         initUs, initUs_,
         lazyThenUs, lazyMapUs,
+        getUniqueSupplyM3,
 
         -- * Set supply strategy
         initUniqSupply
@@ -97,6 +99,22 @@ uniqFromSupply  (MkSplitUniqSupply n _ _)  = mkUniqueGrimily n
 uniqsFromSupply (MkSplitUniqSupply n _ s2) = mkUniqueGrimily n : uniqsFromSupply s2
 takeUniqFromSupply (MkSplitUniqSupply n s1 _) = (mkUniqueGrimily n, s1)
 
+-- | Build three 'UniqSupply' from a single one,
+-- each of which can supply its own unique
+splitUniqSupply3 :: UniqSupply -> (UniqSupply, UniqSupply, UniqSupply)
+splitUniqSupply3 us = (us1, us2, us3)
+  where
+    (us1, us') = splitUniqSupply us
+    (us2, us3) = splitUniqSupply us'
+
+-- | Build four 'UniqSupply' from a single one,
+-- each of which can supply its own unique
+splitUniqSupply4 :: UniqSupply -> (UniqSupply, UniqSupply, UniqSupply, UniqSupply)
+splitUniqSupply4 us = (us1, us2, us3, us4)
+  where
+    (us1, us2, us') = splitUniqSupply3 us
+    (us3, us4)      = splitUniqSupply us'
+
 {-
 ************************************************************************
 *                                                                      *
@@ -185,6 +203,12 @@ instance MonadUnique UniqSM where
     getUniqueM  = getUniqueUs
     getUniquesM = getUniquesUs
 
+getUniqueSupplyM3 :: MonadUnique m => m (UniqSupply, UniqSupply, UniqSupply)
+getUniqueSupplyM3 = liftM3 (,,) getUniqueSupplyM getUniqueSupplyM getUniqueSupplyM
+
+liftUs :: MonadUnique m => UniqSM a -> m a
+liftUs m = getUniqueSupplyM >>= return . flip initUs_ m
+
 getUniqueUs :: UniqSM Unique
 getUniqueUs = USM (\us -> case takeUniqFromSupply us of
                           (u,us') -> (# u, us' #))
diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs
index 54a934d3e6..8ca0b54162 100644
--- a/compiler/deSugar/Check.hs
+++ b/compiler/deSugar/Check.hs
@@ -1,770 +1,1399 @@
 {-
-(c) The University of Glasgow 2006
-(c) The GRASP/AQUA Project, Glasgow University, 1997-1998
+Author: George Karachalias <george.karachalias@cs.kuleuven.be>
 
-Author: Juan J. Quintela    <quintela@krilin.dc.fi.udc.es>
+Pattern Matching Coverage Checking.
 -}
 
 {-# LANGUAGE CPP #-}
 
-module Check ( check , ExhaustivePat ) where
+module Check (
+        -- Actual check and pretty printing
+        checkSingle, checkMatches, dsPmWarn,
+
+        -- See Note [Type and Term Equality Propagation]
+        genCaseTmCs1, genCaseTmCs2
+    ) where
 
 #include "HsVersions.h"
 
+import TmOracle
+
+import DynFlags
 import HsSyn
 import TcHsSyn
-import DsUtils
-import MatchLit
 import Id
 import ConLike
 import DataCon
-import PatSyn
 import Name
 import TysWiredIn
-import PrelNames
 import TyCon
 import SrcLoc
-import UniqSet
 import Util
-import BasicTypes
 import Outputable
 import FastString
 
-{-
-This module performs checks about if one list of equations are:
-\begin{itemize}
-\item Overlapped
-\item Non exhaustive
-\end{itemize}
-To discover this we go through the list of equations in a tree-like fashion.
-
-If you like theory, a similar algorithm is described in:
-\begin{quotation}
-        {\em Two Techniques for Compiling Lazy Pattern Matching},
-        Luc Maranguet,
-        INRIA Rocquencourt (RR-2385, 1994)
-\end{quotation}
-The algorithm is based on the first technique, but there are some differences:
-\begin{itemize}
-\item We don't generate code
-\item We have constructors and literals (not only literals as in the
-          article)
-\item We don't use directions, we must select the columns from
-          left-to-right
-\end{itemize}
-(By the way the second technique is really similar to the one used in
- @Match.hs@ to generate code)
-
-The @check@ function takes the equations of a pattern and returns:
-\begin{itemize}
-\item The patterns that are not recognized
-\item The equations that are shadowed or overlapped
-\end{itemize}
-It simplify the patterns and then call @check'@ (the same semantics), and it
-needs to reconstruct the patterns again ....
-
-The problem appear with things like:
-\begin{verbatim}
-  f [x,y]   = ....
-  f (x:xs)  = .....
-\end{verbatim}
-We want to put the two patterns with the same syntax, (prefix form) and
-then all the constructors are equal:
-\begin{verbatim}
-  f (: x (: y []))   = ....
-  f (: x xs)         = .....
-\end{verbatim}
-(more about this in @tidy_eqns@)
-
-We would prefer to have a @WarningPat@ of type @String@, but Strings and the
-Pretty Printer are not friends.
-
-We use @InPat@ in @WarningPat@ instead of @OutPat@
-because we need to print the
-warning messages in the same way they are introduced, i.e. if the user
-wrote:
-\begin{verbatim}
-        f [x,y] = ..
-\end{verbatim}
-He don't want a warning message written:
-\begin{verbatim}
-        f (: x (: y [])) ........
-\end{verbatim}
-Then we need to use InPats.
-\begin{quotation}
-     Juan Quintela 5 JUL 1998\\
-          User-friendliness and compiler writers are no friends.
-\end{quotation}
--}
-
-type WarningPat = InPat Name
-type ExhaustivePat = ([WarningPat], [(Name, [HsLit])])
-type EqnNo  = Int
-type EqnSet = UniqSet EqnNo
+import DsMonad    -- DsM, initTcDsForSolver, getDictsDs
+import TcSimplify -- tcCheckSatisfiability
+import TcType     -- toTcType, toTcTypeBag
+import Bag
+import ErrUtils
+import MonadUtils -- MonadIO
+import Var        -- EvVar
+import Type
+import UniqSupply
+import DsGRHSs    -- isTrueLHsExpr
+
+import Data.List     -- find
+import Data.Maybe    -- isNothing, isJust, fromJust
+import Control.Monad -- liftM3, forM
 
+{-
+This module checks pattern matches for:
+\begin{enumerate}
+  \item Equations that are redundant
+  \item Equations with inaccessible right-hand-side
+  \item Exhaustiveness
+\end{enumerate}
 
-check :: [EquationInfo] -> ([ExhaustivePat], [EquationInfo])
-  -- Second result is the shadowed equations
-  -- if there are view patterns, just give up - don't know what the function is
-check qs = (untidy_warns, shadowed_eqns)
-      where
-        tidy_qs = map tidy_eqn qs
-        (warns, used_nos) = check' ([1..] `zip` tidy_qs)
-        untidy_warns = map untidy_exhaustive warns
-        shadowed_eqns = [eqn | (eqn,i) <- qs `zip` [1..],
-                                not (i `elementOfUniqSet` used_nos)]
-
-untidy_exhaustive :: ExhaustivePat -> ExhaustivePat
-untidy_exhaustive ([pat], messages) =
-                  ([untidy_no_pars pat], map untidy_message messages)
-untidy_exhaustive (pats, messages) =
-                  (map untidy_pars pats, map untidy_message messages)
+The algorithm used is described in the paper:
 
-untidy_message :: (Name, [HsLit]) -> (Name, [HsLit])
-untidy_message (string, lits) = (string, map untidy_lit lits)
+  "GADTs Meet Their Match:
+     Pattern-matching Warnings That Account for GADTs, Guards, and Laziness"
 
--- The function @untidy@ does the reverse work of the @tidy_pat@ function.
+    http://people.cs.kuleuven.be/~george.karachalias/papers/p424-karachalias.pdf
 
-type NeedPars = Bool
+%************************************************************************
+%*                                                                      *
+                     Pattern Match Check Types
+%*                                                                      *
+%************************************************************************
+-}
 
-untidy_no_pars :: WarningPat -> WarningPat
-untidy_no_pars p = untidy False p
+type PmM a = DsM a
+
+data PmConstraint = TmConstraint Id PmExpr -- ^ Term equalities: x ~ e
+                  | TyConstraint [EvVar]   -- ^ Type equalities
+                  | BtConstraint Id        -- ^ Strictness constraints: x ~ _|_
+
+-- The *arity* of a PatVec [p1,..,pn] is
+-- the number of p1..pn that are not Guards
+
+data PmPat p = PmCon { pm_con_con     :: DataCon
+                     , pm_con_arg_tys :: [Type]
+                     , pm_con_tvs     :: [TyVar]
+                     , pm_con_dicts   :: [EvVar]
+                     , pm_con_args    :: [p] }
+               -- For PmCon arguments' meaning see @ConPatOut@ in hsSyn/HsPat.hs
+             | PmVar { pm_var_id      :: Id }
+             | PmLit { pm_lit_lit     :: PmLit } -- See Note [Literals in PmPat]
+
+-- data T a where
+--     MkT :: forall p q. (Eq p, Ord q) => p -> q -> T [p]
+-- or  MkT :: forall p q r. (Eq p, Ord q, [p] ~ r) => p -> q -> T r
+
+data Pattern = PmGuard PatVec PmExpr      -- ^ Guard Patterns
+             | NonGuard (PmPat Pattern)   -- ^ Other Patterns
+
+newtype ValAbs = VA (PmPat ValAbs) -- Value Abstractions
+
+-- Not sure if this is needed
+instance Outputable ValAbs where
+  ppr = ppr . valAbsToPmExpr
+
+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 PmResult = ( [[LPat Id]] -- ^ redundant clauses
+                , [[LPat Id]] -- ^ clauses with inaccessible rhs
+                , [([PmExpr], [ComplexEq])] ) -- ^ missing
 
-untidy_pars :: WarningPat -> WarningPat
-untidy_pars p = untidy True p
+{-
+%************************************************************************
+%*                                                                      *
+       Entry points to the checker: checkSingle and checkMatches
+%*                                                                      *
+%************************************************************************
+-}
 
-untidy :: NeedPars -> WarningPat -> WarningPat
-untidy b (L loc p) = L loc (untidy' b p)
+-- | Check a single pattern binding (let)
+checkSingle :: Id -> Pat Id -> DsM PmResult
+checkSingle var p = do
+  let lp = [noLoc p]
+  vec <- liftUs (translatePat p)
+  vsa <- initial_uncovered [var]
+  (c,d,us') <- patVectProc (vec,[]) vsa -- no guards
+  us <- pruneVSA us'
+  return $ case (c,d) of
+    (True,  _)     -> ([],   [],   us)
+    (False, True)  -> ([],   [lp], us)
+    (False, False) -> ([lp], [],   us)
+
+-- | Check a matchgroup (case, functions, etc.)
+checkMatches :: [Id] -> [LMatch Id (LHsExpr Id)] -> DsM PmResult
+checkMatches 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
-    untidy' _ p@(WildPat _)          = p
-    untidy' _ p@(VarPat _)           = p
-    untidy' _ (LitPat lit)           = LitPat (untidy_lit lit)
-    untidy' _ p@(ConPatIn _ (PrefixCon [])) = p
-    untidy' b (ConPatIn name ps)     = pars b (L loc (ConPatIn name (untidy_con ps)))
-    untidy' _ (ListPat pats ty Nothing)     = ListPat (map untidy_no_pars pats) ty Nothing
-    untidy' _ (TuplePat pats box tys) = TuplePat (map untidy_no_pars pats) box tys
-    untidy' _ (ListPat _ _ (Just _)) = panic "Check.untidy: Overloaded ListPat"
-    untidy' _ (PArrPat _ _)          = panic "Check.untidy: Shouldn't get a parallel array here!"
-    untidy' _ (SigPatIn _ _)         = panic "Check.untidy: SigPat"
-    untidy' _ (LazyPat {})           = panic "Check.untidy: LazyPat"
-    untidy' _ (AsPat {})             = panic "Check.untidy: AsPat"
-    untidy' _ (ParPat {})            = panic "Check.untidy: ParPat"
-    untidy' _ (BangPat {})           = panic "Check.untidy: BangPat"
-    untidy' _ (ConPatOut {})         = panic "Check.untidy: ConPatOut"
-    untidy' _ (ViewPat {})           = panic "Check.untidy: ViewPat"
-    untidy' _ (SplicePat {})         = panic "Check.untidy: SplicePat"
-    untidy' _ (NPat {})              = panic "Check.untidy: NPat"
-    untidy' _ (NPlusKPat {})         = panic "Check.untidy: NPlusKPat"
-    untidy' _ (SigPatOut {})         = panic "Check.untidy: SigPatOut"
-    untidy' _ (CoPat {})             = panic "Check.untidy: CoPat"
-
-untidy_con :: HsConPatDetails Name -> HsConPatDetails Name
-untidy_con (PrefixCon pats) = PrefixCon (map untidy_pars pats)
-untidy_con (InfixCon p1 p2) = InfixCon  (untidy_pars p1) (untidy_pars p2)
-untidy_con (RecCon (HsRecFields flds dd))
-  = RecCon (HsRecFields [ L l (fld { hsRecFieldArg
-                                            = untidy_pars (hsRecFieldArg fld) })
-                        | L l fld <- flds ] dd)
-
-pars :: NeedPars -> WarningPat -> Pat Name
-pars True p = ParPat p
-pars _    p = unLoc p
-
-untidy_lit :: HsLit -> HsLit
-untidy_lit (HsCharPrim src c) = HsChar src c
-untidy_lit lit                = lit
+    go [] missing = do
+      missing' <- pruneVSA missing
+      return ([], [], missing')
+
+    go (m:ms) missing = do
+      clause        <- liftUs (translateMatch m)
+      (c,  d,  us ) <- patVectProc 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
+  ty_cs <- TyConstraint . bagToList <$> getDictsDs
+  tm_cs <- map (uncurry TmConstraint) . bagToList <$> getTmCsDs
+  let vsa = map (VA . PmVar) vars
+  return $ mkConstraint (ty_cs:tm_cs) (foldr Cons Singleton vsa)
 
 {-
-@check@ is the external interface, boring work (tidy, untidy) is done
-in this as it needs to be done only once.
-@check'@ is called recursively, this is the reason to have two functions.
-
-These are the several cases handled in @check'@:
-
-\begin{itemize}
-\item There are no equations: Everything is OK.
-
-\item If all the patterns are variables and the match can't fail
-      then this equation is used and it doesn't generate non-exhaustive cases.
-
-\item There is only one equation that can fail, and all the patterns are
-      variables. Then that equation is used and the same equation is
-      non-exhaustive.
-
-\item All the patterns are variables, and the match can fail, there are
-      more equations then the results is the result of the rest of equations
-      and this equation is used also.
-
-\item In the general case, there can exist literals ,constructors or only
-      vars in the first column, we actuate in consequence.
-
-\end{itemize}
+%************************************************************************
+%*                                                                      *
+              Transform source syntax to *our* syntax
+%*                                                                      *
+%************************************************************************
 -}
 
-check' :: [(EqnNo, EquationInfo)]
-        -> ([ExhaustivePat],    -- Pattern scheme that might not be matched at all
-            EqnSet)             -- Eqns that are used (others are overlapped)
-
-check' [] = ([],emptyUniqSet)
-  -- Was    ([([],[])], emptyUniqSet)
-  -- But that (a) seems weird, and (b) triggered Trac #7669
-  -- So now I'm just doing the simple obvious thing
+-- -----------------------------------------------------------------------
+-- * Utilities
+
+nullaryConPattern :: DataCon -> Pattern
+-- Nullary data constructor and nullary type constructor
+nullaryConPattern con = NonGuard $
+  PmCon { pm_con_con = con, pm_con_arg_tys = []
+        , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = [] }
+
+truePattern :: Pattern
+truePattern = nullaryConPattern trueDataCon
+
+-- | A fake guard pattern (True <- _) used to represent cases we cannot handle
+fake_pat :: Pattern
+fake_pat = PmGuard [truePattern] (PmExprOther EWildPat)
+
+vanillaConPattern :: DataCon -> [Type] -> PatVec -> Pattern
+-- ADT constructor pattern => no existentials, no local constraints
+vanillaConPattern con arg_tys args = NonGuard $
+  PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys
+        , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = args }
+
+nilPattern :: Type -> Pattern
+nilPattern ty = NonGuard $
+  PmCon { pm_con_con = nilDataCon, pm_con_arg_tys = [ty]
+        , pm_con_tvs = [], pm_con_dicts = []
+        , pm_con_args = [] }
+
+mkListPatVec :: Type -> PatVec -> PatVec -> PatVec
+mkListPatVec ty xs ys = [NonGuard $ PmCon { pm_con_con = consDataCon
+                                          , pm_con_arg_tys = [ty]
+                                          , pm_con_tvs = [], pm_con_dicts = []
+                                          , pm_con_args = xs++ys }]
+
+mkLitPattern :: HsLit -> Pattern
+mkLitPattern lit = NonGuard $ PmLit { pm_lit_lit = PmSLit lit }
+
+-- -----------------------------------------------------------------------
+-- * Transform (Pat Id) into of (PmPat Id)
+
+translatePat :: Pat Id -> UniqSM PatVec
+translatePat pat = case pat of
+  WildPat ty         -> mkPatternVarsSM [ty]
+  VarPat  id         -> return [idPatternVar (unLoc id)]
+  ParPat p           -> translatePat (unLoc p)
+  LazyPat _          -> mkPatternVarsSM [hsPatType pat] -- like a variable
+
+  -- ignore strictness annotations for now
+  BangPat p          -> translatePat (unLoc p)
+
+  AsPat lid p -> do
+     -- Note [Translating As Patterns]
+    ps <- translatePat (unLoc p)
+    let [e] = map valAbsToPmExpr (coercePatVec ps)
+        g   = PmGuard [idPatternVar (unLoc lid)] e
+    return (ps ++ [g])
+
+  SigPatOut p _ty -> translatePat (unLoc p)
+
+  CoPat wrapper p ty -> do
+    ps      <- translatePat p
+    (xp,xe) <- mkPmId2FormsSM ty
+    let g = mkGuard ps (HsWrap wrapper (unLoc xe))
+    return [xp,g]
+
+  -- (n + k)  ===>   x (True <- x >= k) (n <- x-k)
+  NPlusKPat (L _ n) k ge minus -> do
+    (xp, xe) <- mkPmId2FormsSM (idType n)
+    let ke = L (getLoc k) (HsOverLit (unLoc k))
+        g1 = mkGuard [truePattern]    (OpApp xe (noLoc ge)    no_fixity ke)
+        g2 = mkGuard [idPatternVar n] (OpApp xe (noLoc minus) no_fixity ke)
+    return [xp, g1, g2]
+
+  -- (fun -> pat)   ===>   x (pat <- fun x)
+  ViewPat lexpr lpat arg_ty -> do
+    ps <- translatePat (unLoc lpat)
+    -- See Note [Guards and Approximation]
+    case all cantFailPattern ps of
+      True  -> do
+        (xp,xe) <- mkPmId2FormsSM arg_ty
+        let g = mkGuard ps (HsApp lexpr xe)
+        return [xp,g]
+      False -> do
+        var <- mkPatternVarSM arg_ty
+        return [var, fake_pat]
+
+  -- list
+  ListPat ps ty Nothing -> do
+    foldr (mkListPatVec ty) [nilPattern ty] <$> translatePatVec (map unLoc ps)
+
+  -- overloaded list
+  ListPat lpats elem_ty (Just (pat_ty, _to_list))
+    | Just e_ty <- splitListTyConApp_maybe pat_ty, 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 (ListPat lpats e_ty Nothing)
+    | otherwise -> do
+        -- See Note [Guards and Approximation]
+        var <- mkPatternVarSM pat_ty
+        return [var, fake_pat]
+
+  ConPatOut { pat_con = L _ (PatSynCon _) } -> do
+    -- 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 <- mkPatternVarSM (hsPatType pat)
+    return [var,fake_pat]
+
+  ConPatOut { pat_con     = L _ (RealDataCon con)
+            , pat_arg_tys = arg_tys
+            , pat_tvs     = ex_tvs
+            , pat_dicts   = dicts
+            , pat_args    = ps } -> do
+    args <- translateConPatVec arg_tys ex_tvs con ps
+    return [ NonGuard $ PmCon { pm_con_con     = con
+                              , pm_con_arg_tys = arg_tys
+                              , pm_con_tvs     = ex_tvs
+                              , pm_con_dicts   = dicts
+                              , pm_con_args    = args }]
+
+  NPat (L _ ol) mb_neg _eq -> translateNPat ol mb_neg
+
+  LitPat lit
+      -- If it is a string then convert it to a list of characters
+    | HsString src s <- lit ->
+        foldr (mkListPatVec charTy) [nilPattern charTy] <$>
+          translatePatVec (map (LitPat . HsChar src) (unpackFS s))
+    | otherwise -> return [mkLitPattern lit]
+
+  PArrPat ps ty -> do
+    tidy_ps <- translatePatVec (map unLoc ps)
+    let fake_con = parrFakeCon (length ps)
+    return [vanillaConPattern fake_con [ty] (concat tidy_ps)]
+
+  TuplePat ps boxity tys -> do
+    tidy_ps   <- translatePatVec (map unLoc ps)
+    let tuple_con = tupleDataCon boxity (length ps)
+    return [vanillaConPattern tuple_con tys (concat tidy_ps)]
+
+  -- --------------------------------------------------------------------------
+  -- Not supposed to happen
+  ConPatIn  {} -> panic "Check.translatePat: ConPatIn"
+  SplicePat {} -> panic "Check.translatePat: SplicePat"
+  SigPatIn  {} -> panic "Check.translatePat: SigPatIn"
+
+-- | Translate an overloaded literal (see `tidyNPat' in deSugar/MatchLit.hs)
+translateNPat :: HsOverLit Id -> Maybe (SyntaxExpr Id) -> UniqSM PatVec
+translateNPat (OverLit val False _ ty) mb_neg
+  | isStringTy ty, HsIsString src s <- val, Nothing <- mb_neg
+  = translatePat (LitPat (HsString src s))
+  | isIntTy    ty, HsIntegral src i <- val
+  = translatePat (mk_num_lit HsInt src i)
+  | isWordTy   ty, HsIntegral src i <- val
+  = translatePat (mk_num_lit HsWordPrim src i)
+  where
+    mk_num_lit c src i = LitPat $ case mb_neg of
+      Nothing -> c src i
+      Just _  -> c src (-i)
+translateNPat ol mb_neg
+  = return [NonGuard $ PmLit { pm_lit_lit = PmOLit (isJust mb_neg) ol }]
+
+-- | Translate a list of patterns (Note: each pattern is translated
+-- to a pattern vector but we do not concatenate the results).
+translatePatVec :: [Pat Id] -> UniqSM [PatVec]
+translatePatVec pats = mapM translatePat pats
+
+translateConPatVec :: [Type] -> [TyVar]
+                   -> DataCon -> HsConPatDetails Id -> UniqSM PatVec
+translateConPatVec _univ_tys _ex_tvs _ (PrefixCon ps)
+  = concat <$> translatePatVec (map unLoc ps)
+translateConPatVec _univ_tys _ex_tvs _ (InfixCon p1 p2)
+  = concat <$> translatePatVec (map unLoc [p1,p2])
+translateConPatVec  univ_tys  ex_tvs c (RecCon (HsRecFields fs _))
+    -- Nothing matched. Make up some fresh term variables
+  | null fs        = mkPatternVarsSM 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) mkPatternVarsSM 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
+  | matched_lbls `subsetOf` orig_lbls
+  = ASSERT (length orig_lbls == length arg_tys)
+      let translateOne (lbl, ty) = case lookup lbl matched_pats of
+            Just p  -> translatePat p
+            Nothing -> mkPatternVarsSM [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    <- mkPatternVarsSM arg_tys
+      translated_pats <- forM matched_pats $ \(x,pat) -> do
+        pvec <- translatePat pat
+        return (x, pvec)
+
+      let zipped = zip orig_lbls [ x | NonGuard (PmVar x) <- arg_var_pats ]
+          guards = map (\(name,pvec) -> case lookup name zipped of
+                            Just x  -> PmGuard pvec (PmExprVar x)
+                            Nothing -> panic "translateConPatVec: lookup")
+                       translated_pats
+
+      return (arg_var_pats ++ guards)
+  where
+    -- The actual argument types (instantiated)
+    arg_tys = dataConInstOrigArgTys c (univ_tys ++ mkTyVarTys ex_tvs)
+
+    -- Some label information
+    orig_lbls    = map flSelector $ dataConFieldLabels c
+    matched_pats = [ (getName (unLoc (hsRecFieldId x)), unLoc (hsRecFieldArg x))
+                   | L _ x <- fs]
+    matched_lbls = [ name | (name, _pat) <- matched_pats ]
+
+    subsetOf :: Eq a => [a] -> [a] -> Bool
+    subsetOf []     _  = True
+    subsetOf (_:_)  [] = False
+    subsetOf (x:xs) (y:ys)
+      | x == y    = subsetOf    xs  ys
+      | otherwise = subsetOf (x:xs) ys
+
+translateMatch :: LMatch Id (LHsExpr Id) -> UniqSM (PatVec,[PatVec])
+translateMatch (L _ (Match _ lpats _ grhss)) = do
+  pats'   <- concat <$> translatePatVec pats
+  guards' <- mapM translateGuards guards
+  return (pats', guards')
+  where
+    extractGuards :: LGRHS Id (LHsExpr Id) -> [GuardStmt Id]
+    extractGuards (L _ (GRHS gs _)) = map unLoc gs
+
+    pats   = map unLoc lpats
+    guards = map extractGuards (grhssGRHSs grhss)
+
+-- -----------------------------------------------------------------------
+-- * Transform source guards (GuardStmt Id) to PmPats (Pattern)
+
+-- | Translate a list of guard statements to a pattern vector
+translateGuards :: [GuardStmt Id] -> UniqSM PatVec
+translateGuards guards = do
+  all_guards <- concat <$> mapM translateGuard guards
+  return (replace_unhandled all_guards)
+  -- 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).
+  -- See Note [Guards and Approximation] for all guard-related approximations
+  -- we implement.
+  where
+    replace_unhandled :: PatVec -> PatVec
+    replace_unhandled gv
+      | any_unhandled gv = fake_pat : [ p | p <- gv, shouldKeep p ]
+      | otherwise        = gv
+
+    any_unhandled :: PatVec -> Bool
+    any_unhandled gv = any (not . shouldKeep) gv
+
+    shouldKeep :: Pattern -> Bool
+    shouldKeep (NonGuard p)
+      | PmVar {} <- p      = True
+      | PmCon {} <- p      = length (allConstructors (pm_con_con p)) == 1
+                             && all shouldKeep (pm_con_args p)
+    shouldKeep (PmGuard pv e)
+      | all shouldKeep pv  = True
+      | isNotPmExprOther e = True  -- expensive but we want it
+    shouldKeep _other_pat  = False -- let the rest..
+
+-- | Check whether a pattern can fail to match
+cantFailPattern :: Pattern -> Bool
+cantFailPattern (NonGuard p)
+  | PmVar {} <- p = True
+  | PmCon {} <- p = length (allConstructors (pm_con_con p)) == 1
+                    && all cantFailPattern (pm_con_args p)
+cantFailPattern (PmGuard pv _e)
+                  = all cantFailPattern pv
+cantFailPattern _ = False
+
+-- | Translate a guard statement to Pattern
+translateGuard :: GuardStmt Id -> UniqSM PatVec
+translateGuard (BodyStmt   e _ _ _) = translateBoolGuard e
+translateGuard (LetStmt      binds) = translateLet (unLoc binds)
+translateGuard (BindStmt   p e _ _) = translateBind 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"
+
+-- | Translate let-bindings
+translateLet :: HsLocalBinds Id -> UniqSM PatVec
+translateLet _binds = return []
+
+-- | Translate a pattern guard
+translateBind :: LPat Id -> LHsExpr Id -> UniqSM PatVec
+translateBind (L _ p) e = do
+  ps <- translatePat p
+  return [mkGuard ps (unLoc e)]
+
+-- | Translate a boolean guard
+translateBoolGuard :: LHsExpr Id -> UniqSM PatVec
+translateBoolGuard e
+  | isJust (isTrueLHsExpr e) = return []
+    -- The formal thing to do would be to generate (True <- True)
+    -- but it is trivial to solve so instead we give back an empty
+    -- PatVec for efficiency
+  | otherwise = return [mkGuard [truePattern] (unLoc e)]
+
+{- Note [Guards and Approximation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Even if the algorithm is really expressive, the term oracle we use is not.
+Hence, several features are not translated *properly* but we approximate.
+The list includes:
+
+1. View Patterns
+----------------
+A view pattern @(f -> p)@ should be translated to @x (p <- f x)@. The term
+oracle does not handle function applications so we know that the generated
+constraints will not be handled at the end. Hence, we distinguish between two
+cases:
+  a) Pattern @p@ cannot fail. Then this is just a binding and we do the *right
+     thing*.
+  b) Pattern @p@ can fail. This means that when checking the guard, we will
+     generate several cases, with no useful information. E.g.:
+
+       h (f -> [a,b]) = ...
+       h x ([a,b] <- f x) = ...
+
+       uncovered set = { [x |> { False ~ (f x ~ [])            }]
+                       , [x |> { False ~ (f x ~ (t1:[]))       }]
+                       , [x |> { False ~ (f x ~ (t1:t2:t3:t4)) }] }
+
+     So we have two problems:
+       1) Since we do not print the constraints in the general case (they may
+          be too many), the warning will look like this:
+
+            Pattern match(es) are non-exhaustive
+            In an equation for `h':
+                Patterns not matched:
+                    _
+                    _
+                    _
+          Which is not short and not more useful than a single underscore.
+       2) The size of the uncovered set increases a lot, without gaining more
+          expressivity in our warnings.
+
+     Hence, in this case, we replace the guard @([a,b] <- f x)@ with a *dummy*
+     @fake_pat@: @True <- _@. That is, we record that there is a possibility
+     of failure but we minimize it to a True/False. This generates a single
+     warning and much smaller uncovered sets.
+
+2. Overloaded Lists
+-------------------
+An overloaded list @[...]@ should be translated to @x ([...] <- toList x)@. The
+problem is exactly like above, as its solution. For future reference, the code
+below is the *right thing to do*:
+
+   ListPat lpats elem_ty (Just (pat_ty, to_list))
+     otherwise -> do
+       (xp, xe) <- mkPmId2FormsSM 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)
+       return [xp,g]
+
+3. Overloaded Literals
+----------------------
+The case with literals is a bit different. a literal @l@ should be translated
+to @x (True <- x == from l)@. Since we want to have better warnings for
+overloaded literals as it is a very common feature, we treat them differently.
+They are mainly covered in Note [Undecidable Equality on Overloaded Literals].
+
+4. N+K Patterns & Pattern Synonyms
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+An n+k pattern (n+k) should be translated to @x (True <- x >= k) (n <- x-k)@.
+Since the only pattern of the three that causes failure is guard @(n <- x-k)@,
+and has two possible outcomes. Hence, there is no benefit in using a dummy and
+we implement the proper thing. Pattern synonyms are simply not implemented yet.
+Hence, to be conservative, we generate a dummy pattern, assuming that the
+pattern can fail.
+
+5. Actual Guards
+----------------
+During translation, boolean guards and pattern guards are translated properly.
+Let bindings though are omitted by function @translateLet@. Since they are lazy
+bindings, we do not actually want to generate a (strict) equality (like we do
+in the pattern bind case). Hence, we safely drop them.
+
+Additionally, top-level guard translation (performed by @translateGuards@)
+replaces guards that cannot be reasoned about (like the ones we described in
+1-4) with a single @fake_pat@ to record the possibility of failure to match.
+
+%************************************************************************
+%*                                                                      *
+                    Main Pattern Matching Check
+%*                                                                      *
+%************************************************************************
+-}
 
-check' ((n, EqnInfo { eqn_pats = ps, eqn_rhs = MatchResult can_fail _ }) : rs)
-   | first_eqn_all_vars && case can_fail of { CantFail -> True; CanFail -> False }
-   = ([], unitUniqSet n)        -- One eqn, which can't fail
+-- ----------------------------------------------------------------------------
+-- * Process a vector
+
+-- Covered, Uncovered, Divergent
+process_guards :: UniqSupply -> [PatVec] -> (ValSetAbs, ValSetAbs, ValSetAbs)
+process_guards _us [] = (Singleton, Empty, Empty) -- No guard == True guard
+process_guards us  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)
+  | 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
+
+patternType :: Pattern -> Type
+patternType (PmGuard pv _) = ASSERT (patVecArity pv == 1) (patternType p)
+  where Just p = find ((==1) . patternArity) pv
+patternType (NonGuard pat) = pmPatType pat
+
+-- | Get the type out of a PmPat. For guard patterns (ps <- e) we use the type
+-- of the first (or the single -WHEREVER IT IS- valid to use?) pattern
+pmPatType :: PmPat p -> Type
+pmPatType (PmCon { pm_con_con = con, pm_con_arg_tys = tys })
+                                     = mkTyConApp (dataConTyCon con) tys
+pmPatType (PmVar { pm_var_id  = x }) = idType x
+pmPatType (PmLit { pm_lit_lit = l }) = pmLitType l
+
+mkOneConFull :: Id -> UniqSupply -> DataCon -> (PmPat ValAbs, [PmConstraint])
+--  *  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
+--       leads to
+--            data TPair a b = T1 a b  -- The "representation" type
+--       It is TPair, not T, that is given to mkOneConFull
+--
+--  * 'con' K is a constructor of data type T
+--
+-- After instantiating the universal tyvars of K we get
+--          K tys :: forall bs. Q => s1 .. sn -> T tys
+--
+-- Results: ValAbs:          K (y1::s1) .. (yn::sn)
+--          [PmConstraint]:  Q, x ~ K y1..yn
 
-   | first_eqn_all_vars && null rs      -- One eqn, but it can fail
-   = ([(takeList ps (repeat nlWildPatName),[])], unitUniqSet n)
+mkOneConFull x usupply con = (con_abs, constraints)
+  where
 
-   | first_eqn_all_vars         -- Several eqns, first can fail
-   = (pats, addOneToUniqSet indexs n)
+    (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  = zipTopTvSubst 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
+                       , 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 x (pmPatToPmExpr con_abs) ]
+      | otherwise   = [ TmConstraint x (pmPatToPmExpr con_abs)
+                      , TyConstraint evvars ]
+
+mkConVars :: UniqSupply -> [Type] -> [ValAbs] -- ys, fresh with the given type
+mkConVars us tys = zipWith mkValAbsVar (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
-    first_eqn_all_vars = all_vars ps
-    (pats,indexs) = check' rs
-
-check' qs
-   | some_literals     = split_by_literals qs
-   | some_constructors = split_by_constructor qs
-   | only_vars         = first_column_only_vars qs
-   | otherwise = pprPanic "Check.check': Not implemented :-(" (ppr first_pats)
-                 -- Shouldn't happen
+    go :: Int -> DList ValAbs -> ValSetAbs -> ValSetAbs
+    go _ _    Empty = Empty
+    go 0 args vsa   = VA (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
+
+-- ----------------------------------------------------------------------------
+-- * More smart constructors and fresh variable generation
+
+mkGuard :: PatVec -> HsExpr Id -> Pattern
+mkGuard pv e = PmGuard pv (hsExprToPmExpr e)
+
+mkPmVar :: UniqSupply -> Type -> PmPat p
+mkPmVar usupply ty = PmVar (mkPmId usupply ty)
+
+idPatternVar :: Id -> Pattern
+idPatternVar x = NonGuard (PmVar x)
+
+mkPatternVar :: UniqSupply -> Type -> Pattern
+mkPatternVar us ty = NonGuard (mkPmVar us ty)
+
+mkValAbsVar :: UniqSupply -> Type -> ValAbs
+mkValAbsVar us ty = VA (mkPmVar us ty)
+
+mkPatternVarSM :: Type -> UniqSM Pattern
+mkPatternVarSM ty = flip mkPatternVar ty <$> getUniqueSupplyM
+
+mkPatternVarsSM :: [Type] -> UniqSM PatVec
+mkPatternVarsSM tys = mapM mkPatternVarSM tys
+
+mkPmId :: UniqSupply -> Type -> Id
+mkPmId usupply ty = mkLocalId name ty
   where
-     -- Note: RecPats will have been simplified to ConPats
-     --       at this stage.
-    first_pats        = ASSERT2( okGroup qs, pprGroup qs ) map firstPatN qs
-    some_constructors = any is_con first_pats
-    some_literals     = any is_lit first_pats
-    only_vars         = all is_var first_pats
+    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
+  return (idPatternVar x, noLoc (HsVar (noLoc x)))
+
+-- ----------------------------------------------------------------------------
+-- * Converting between Value Abstractions, Patterns and PmExpr
+
+valAbsToPmExpr :: ValAbs -> PmExpr
+valAbsToPmExpr (VA va) = pmPatToPmExpr va
+
+pmPatToPmExpr :: PmPat ValAbs -> PmExpr
+pmPatToPmExpr (PmCon { pm_con_con  = c
+                     , pm_con_args = ps }) = PmExprCon c (map valAbsToPmExpr ps)
+pmPatToPmExpr (PmVar { pm_var_id   = x  }) = PmExprVar x
+pmPatToPmExpr (PmLit { pm_lit_lit  = l  }) = PmExprLit l
+
+-- Convert a pattern vector to a value list abstraction by dropping the guards
+-- recursively (See Note [Translating As Patterns])
+coercePatVec :: PatVec -> [ValAbs]
+coercePatVec pv = [ VA (coercePmPat p) | NonGuard p <- pv]
+
+coercePmPat :: PmPat Pattern -> PmPat ValAbs
+coercePmPat (PmVar { pm_var_id  = x }) = PmVar { pm_var_id  = x }
+coercePmPat (PmLit { pm_lit_lit = l }) = PmLit { pm_lit_lit = l }
+coercePmPat (PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys
+                   , pm_con_tvs = tvs, pm_con_dicts = dicts
+                   , pm_con_args = args })
+  = PmCon { pm_con_con  = con, pm_con_arg_tys = arg_tys
+          , pm_con_tvs  = tvs, pm_con_dicts = dicts
+          , pm_con_args = coercePatVec args }
+
+no_fixity :: a -- TODO: Can we retrieve the fixity from the operator name?
+no_fixity = panic "Check: no fixity"
+
+-- Get all constructors in the family (including given)
+allConstructors :: DataCon -> [DataCon]
+allConstructors = tyConDataCons . dataConTyCon
+
+-- -----------------------------------------------------------------------
+-- * Types and constraints
+
+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], [(Id, PmExpr)], Maybe Id)
+splitConstraints [] = ([],[],Nothing)
+splitConstraints (c : rest)
+  = case c of
+      TyConstraint cs  -> (cs ++ ty_cs, tm_cs, bot_cs)
+      TmConstraint x e -> (ty_cs, (x,e):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
 
 {-
-Here begins the code to deal with literals, we need to split the matrix
-in different matrix beginning by each literal and a last matrix with the
-rest of values.
+%************************************************************************
+%*                                                                      *
+                              The oracles
+%*                                                                      *
+%************************************************************************
 -}
 
-split_by_literals :: [(EqnNo, EquationInfo)] -> ([ExhaustivePat], EqnSet)
-split_by_literals qs = process_literals used_lits qs
-           where
-             used_lits = get_used_lits qs
+-- | 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 ->
+            -- Have another go at the term oracle state, for strange
+            -- equalities between overloaded literals. See
+            -- Note [Undecidable Equality on Overloaded Literals] in TmOracle
+            if containsEqLits tm_env
+              then return [] -- not on the safe side
+              else 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
+  = do { ((_warns, errs), res) <- initTcDsForSolver $ tcCheckSatisfiability evs
+       ; case res of
+            Just sat -> return sat
+            Nothing  -> pprPanic "tyOracle" (vcat $ pprErrMsgBagWithLoc errs) }
 
 {-
-@process_explicit_literals@ is a function that process each literal that appears
-in the column of the matrix.
+%************************************************************************
+%*                                                                      *
+                             Sanity Checks
+%*                                                                      *
+%************************************************************************
 -}
 
-process_explicit_literals :: [HsLit] -> [(EqnNo, EquationInfo)] -> ([ExhaustivePat],EqnSet)
-process_explicit_literals lits qs = (concat pats, unionManyUniqSets indexs)
-    where
-      pats_indexs   = map (\x -> construct_literal_matrix x qs) lits
-      (pats,indexs) = unzip pats_indexs
+type PmArity = Int
 
-{-
-@process_literals@ calls @process_explicit_literals@ to deal with the literals
-that appears in the matrix and deal also with the rest of the cases. It
-must be one Variable to be complete.
--}
+patVecArity :: PatVec -> PmArity
+patVecArity = sum . map patternArity
 
-process_literals :: [HsLit] -> [(EqnNo, EquationInfo)] -> ([ExhaustivePat],EqnSet)
-process_literals used_lits qs
-  | null default_eqns  = ASSERT( not (null qs) ) ([make_row_vars used_lits (head qs)] ++ pats,indexs)
-  | otherwise          = (pats_default,indexs_default)
-     where
-       (pats,indexs)   = process_explicit_literals used_lits qs
-       default_eqns    = ASSERT2( okGroup qs, pprGroup qs )
-                         [remove_var q | q <- qs, is_var (firstPatN q)]
-       (pats',indexs') = check' default_eqns
-       pats_default    = [(nlWildPatName:ps,constraints) |
-                                        (ps,constraints) <- (pats')] ++ pats
-       indexs_default  = unionUniqSets indexs' indexs
+patternArity :: Pattern -> PmArity
+patternArity (PmGuard  {}) = 0
+patternArity (NonGuard {}) = 1
 
 {-
-Here we have selected the literal and we will select all the equations that
-begins for that literal and create a new matrix.
+%************************************************************************
+%*                                                                      *
+            Heart of the algorithm: Function patVectProc
+%*                                                                      *
+%************************************************************************
 -}
 
-construct_literal_matrix :: HsLit -> [(EqnNo, EquationInfo)] -> ([ExhaustivePat],EqnSet)
-construct_literal_matrix lit qs =
-    (map (\ (xs,ys) -> (new_lit:xs,ys)) pats,indexs)
+-- | Process a single vector
+patVectProc :: (PatVec, [PatVec]) -> ValSetAbs -> PmM (Bool, Bool, ValSetAbs)
+patVectProc (vec,gvs) vsa = do
+  us <- getUniqueSupplyM
+  let (c_def, u_def, d_def) = process_guards us gvs -- default (continuation)
+  (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
+
+-- ----------------------------------------------------------------------------
+-- * 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 =
+  case p of
+    -- Guard Case
+    PmGuard pv e ->
+      let (us1, us2) = splitUniqSupply us
+          y  = mkPmId us1 (patternType p)
+          cs = [TmConstraint y e]
+      in  mkConstraint cs $ tailVSA $
+            pmTraverse us2 gvsa rec (pv++ps) (VA (PmVar y) `mkCons` vsa)
+
+    -- Constructor/Variable/Literal Case
+    NonGuard pat
+      | Cons (VA va) vsa <- vsa -> rec us gvsa pat ps va vsa
+      | otherwise -> panic "pmTraverse: singleton" -- can't be anything else
+
+type PmMatcher =  UniqSupply
+               -> ValSetAbs
+               -> PmPat Pattern -> PatVec    -- Vector head and tail
+               -> PmPat ValAbs  -> ValSetAbs -- VSA    head and tail
+               -> ValSetAbs
+
+cMatcher, uMatcher, dMatcher :: PmMatcher
+
+-- cMatcher
+-- ----------------------------------------------------------------------------
+
+-- CVar
+cMatcher us gvsa (PmVar x) ps va vsa
+  = VA va `mkCons` (cs `mkConstraint` covered us gvsa ps vsa)
+  where cs = [TmConstraint x (pmPatToPmExpr va)]
+
+-- CLitCon
+cMatcher us gvsa (PmLit l) ps (va@(PmCon {})) vsa
+  = VA va `mkCons` (cs `mkConstraint` covered us2 gvsa ps vsa)
+  where
+    (us1, us2) = splitUniqSupply us
+    y  = mkPmId us1 (pmPatType va)
+    cs = [ TmConstraint y (PmExprLit l)
+         , TmConstraint y (pmPatToPmExpr va) ]
+
+-- CConLit
+cMatcher us gvsa (p@(PmCon {})) ps (PmLit l) vsa
+  = cMatcher us3 gvsa p ps con_abs (mkConstraint cs vsa)
   where
-    (pats,indexs) = (check' (remove_first_column_lit lit qs))
-    new_lit = nlLitPat lit
-
-remove_first_column_lit :: HsLit
-                        -> [(EqnNo, EquationInfo)]
-                        -> [(EqnNo, EquationInfo)]
-remove_first_column_lit lit qs
-  = ASSERT2( okGroup qs, pprGroup qs )
-    [(n, shift_pat eqn) | q@(n,eqn) <- qs, is_var_lit lit (firstPatN q)]
+    (us1, us2, us3)   = splitUniqSupply3 us
+    y                 = mkPmId us1 (pmPatType p)
+    (con_abs, all_cs) = mkOneConFull y us2 (pm_con_con p)
+    cs = TmConstraint y (PmExprLit l) : all_cs
+
+-- 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
+  Just True  -> VA va `mkCons` covered us gvsa ps vsa -- match
+  Just False -> Empty                                 -- mismatch
+  Nothing    -> VA va `mkCons` (cs `mkConstraint` covered us2 gvsa ps vsa)
+  -- See Note [Undecidable Equality on Overloaded Literals] in TmOracle
   where
-     shift_pat eqn@(EqnInfo { eqn_pats = _:ps}) = eqn { eqn_pats = ps }
-     shift_pat _                                = panic "Check.shift_var: no patterns"
+    (us1, us2) = splitUniqSupply us
+    y          = mkPmId us1 (pmPatType va)
+    cs         = [ TmConstraint y (PmExprLit l1)
+                 , TmConstraint y (PmExprLit l2) ]
+
+-- 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
 
-{-
-This function splits the equations @qs@ in groups that deal with the
-same constructor.
--}
+-- 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 x (PmExprLit l)]
 
-split_by_constructor :: [(EqnNo, EquationInfo)] -> ([ExhaustivePat], EqnSet)
-split_by_constructor qs
-  | null used_cons      = ([], mkUniqSet $ map fst qs)
-  | notNull unused_cons = need_default_case used_cons unused_cons qs
-  | otherwise           = no_need_default_case used_cons qs
-                       where
-                          used_cons   = get_used_cons qs
-                          unused_cons = get_unused_cons used_cons
+-- uMatcher
+-- ----------------------------------------------------------------------------
 
-{-
-The first column of the patterns matrix only have vars, then there is
-nothing to do.
--}
+-- UVar
+uMatcher us gvsa (PmVar x) ps va vsa
+  = VA va `mkCons` (cs `mkConstraint` uncovered us gvsa ps vsa)
+  where cs = [TmConstraint x (pmPatToPmExpr va)]
 
-first_column_only_vars :: [(EqnNo, EquationInfo)] -> ([ExhaustivePat],EqnSet)
-first_column_only_vars qs
-  = (map (\ (xs,ys) -> (nlWildPatName:xs,ys)) pats,indexs)
+-- ULitCon
+uMatcher us gvsa (PmLit l) ps (va@(PmCon {})) vsa
+  = uMatcher us2 gvsa (PmVar y) ps va (mkConstraint cs vsa)
   where
-    (pats, indexs) = check' (map remove_var qs)
+    (us1, us2) = splitUniqSupply us
+    y  = mkPmId us1 (pmPatType va)
+    cs = [TmConstraint y (PmExprLit l)]
 
-{-
-This equation takes a matrix of patterns and split the equations by
-constructor, using all the constructors that appears in the first column
-of the pattern matching.
-
-Whether we need a default clause or not depends if we used all the
-constructors or not explicitly. The reasoning is similar to @process_literals@,
-the difference is that here the default case is not always needed.
--}
+-- 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 y (PmExprLit l)]
+
+-- 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 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
+  Just True  -> VA va `mkCons` uncovered us gvsa ps vsa -- match
+  Just False -> VA va `mkCons` vsa                      -- mismatch
+  Nothing    -> mkUnion (VA va `mkCons`
+                            (match_cs `mkConstraint` uncovered us3 gvsa ps vsa))
+                        (non_match_cs `mkConstraint` (VA va `mkCons` vsa))
+  -- See Note [Undecidable Equality on Overloaded Literals] in TmOracle
+  where
+    (us1, us2, us3) = splitUniqSupply3 us
+    y               = mkPmId us1 (pmPatType va)
+    z               = mkPmId us2 boolTy
+    match_cs        = [ TmConstraint y (PmExprLit l1)
+                      , TmConstraint y (PmExprLit l2) ]
+    non_match_cs    = [ TmConstraint z falsePmExpr
+                      , TmConstraint z (PmExprEq (PmExprLit l1) (PmExprLit l2))]
+
+-- UConVar
+uMatcher us gvsa (p@(PmCon { pm_con_con = con })) ps (PmVar x) vsa
+  = uncovered us2 gvsa (NonGuard 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
+                                     (mkCons (VA va) (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 us2 gvsa p ps (PmLit l) (mkConstraint match_cs vsa))
+            (non_match_cs `mkConstraint` (VA (PmVar x) `mkCons` vsa))
+  where
+    (us1, us2) = splitUniqSupply us
+    y  = mkPmId us1 (pmPatType p)
+    match_cs     = [ TmConstraint x (PmExprLit l)]
+    non_match_cs = [ TmConstraint y falsePmExpr
+                   , TmConstraint y (PmExprEq (PmExprVar x) (PmExprLit l)) ]
+
+-- dMatcher
+-- ----------------------------------------------------------------------------
+
+-- DVar
+dMatcher us gvsa (PmVar x) ps va vsa
+  = VA va `mkCons` (cs `mkConstraint` divergent us gvsa ps vsa)
+  where cs = [TmConstraint x (pmPatToPmExpr va)]
+
+-- DLitCon
+dMatcher us gvsa (PmLit l) ps (va@(PmCon {})) vsa
+  = VA va  `mkCons` (cs `mkConstraint` divergent us2 gvsa ps vsa)
+  where
+    (us1, us2) = splitUniqSupply us
+    y  = mkPmId us1 (pmPatType va)
+    cs = [ TmConstraint y (PmExprLit l)
+         , TmConstraint y (pmPatToPmExpr 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 y (PmExprLit l) : all_cs
+
+-- 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
+  Just True  -> VA va `mkCons` divergent us gvsa ps vsa -- we know: match
+  Just False -> Empty                                   -- we know: no match
+  Nothing    -> VA va `mkCons` (cs `mkConstraint` divergent us2 gvsa ps vsa)
+  -- See Note [Undecidable Equality on Overloaded Literals] in TmOracle
+  where
+    (us1, us2) = splitUniqSupply us
+    y          = mkPmId us1 (pmPatType va)
+    cs         = [ TmConstraint y (PmExprLit l1)
+                 , TmConstraint y (PmExprLit l2) ]
+
+-- DConVar
+dMatcher us gvsa (p@(PmCon { pm_con_con = con })) ps (PmVar x) vsa
+  = mkUnion (VA (PmVar x) `mkCons` mkConstraint [BtConstraint 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
 
-no_need_default_case :: [Pat Id] -> [(EqnNo, EquationInfo)] -> ([ExhaustivePat],EqnSet)
-no_need_default_case cons qs = (concat pats, unionManyUniqSets indexs)
-    where
-      pats_indexs   = map (\x -> construct_matrix x qs) cons
-      (pats,indexs) = unzip pats_indexs
-
-need_default_case :: [Pat Id] -> [DataCon] -> [(EqnNo, EquationInfo)] -> ([ExhaustivePat],EqnSet)
-need_default_case used_cons unused_cons qs
-  | null default_eqns  = (pats_default_no_eqns,indexs)
-  | otherwise          = (pats_default,indexs_default)
-     where
-       (pats,indexs)   = no_need_default_case used_cons qs
-       default_eqns    = ASSERT2( okGroup qs, pprGroup qs )
-                         [remove_var q | q <- qs, is_var (firstPatN q)]
-       (pats',indexs') = check' default_eqns
-       pats_default    = [(make_whole_con c:ps,constraints) |
-                          c <- unused_cons, (ps,constraints) <- pats'] ++ pats
-       new_wilds       = ASSERT( not (null qs) ) make_row_vars_for_constructor (head qs)
-       pats_default_no_eqns =  [(make_whole_con c:new_wilds,[]) | c <- unused_cons] ++ pats
-       indexs_default  = unionUniqSets indexs' indexs
-
-construct_matrix :: Pat Id -> [(EqnNo, EquationInfo)] -> ([ExhaustivePat],EqnSet)
-construct_matrix con qs =
-    (map (make_con con) pats,indexs)
+-- DLitVar
+dMatcher us gvsa (PmLit l) ps (PmVar x) vsa
+  = mkUnion (VA (PmVar x) `mkCons` mkConstraint [BtConstraint x] vsa)
+            (dMatcher us gvsa (PmLit l) ps (PmLit l) (mkConstraint cs vsa))
   where
-    (pats,indexs) = (check' (remove_first_column con qs))
+    cs = [TmConstraint x (PmExprLit l)]
 
-{-
-Here removing the first column is more difficult (than literals) due to the fact
-that constructors can have arguments.
-
-For instance, the matrix
-\begin{verbatim}
- (: x xs) y
- z        y
-\end{verbatim}
-is transformed in:
-\begin{verbatim}
- x xs y
- _ _  y
-\end{verbatim}
--}
+-- ----------------------------------------------------------------------------
+-- * Propagation of term constraints inwards when checking nested matches
 
-remove_first_column :: Pat Id                -- Constructor
-                    -> [(EqnNo, EquationInfo)]
-                    -> [(EqnNo, EquationInfo)]
-remove_first_column (ConPatOut{ pat_con = L _ con, pat_args = PrefixCon con_pats }) qs
-  = ASSERT2( okGroup qs, pprGroup qs )
-    [(n, shift_var eqn) | q@(n, eqn) <- qs, is_var_con con (firstPatN q)]
-  where
-     new_wilds = [WildPat (hsLPatType arg_pat) | arg_pat <- con_pats]
-     shift_var eqn@(EqnInfo { eqn_pats = ConPatOut{ pat_args = PrefixCon ps' } : ps})
-        = eqn { eqn_pats = map unLoc ps' ++ ps }
-     shift_var eqn@(EqnInfo { eqn_pats = WildPat _ : ps })
-        = eqn { eqn_pats = new_wilds ++ ps }
-     shift_var _ = panic "Check.Shift_var:No done"
-remove_first_column _ _ = panic "Check.remove_first_column: Not ConPatOut"
-
-make_row_vars :: [HsLit] -> (EqnNo, EquationInfo) -> ExhaustivePat
-make_row_vars used_lits (_, EqnInfo { eqn_pats = pats})
-   = (nlVarPat new_var:takeList (tail pats) (repeat nlWildPatName)
-     ,[(new_var,used_lits)])
-  where
-     new_var = hash_x
-
-hash_x :: Name
-hash_x = mkInternalName unboundKey {- doesn't matter much -}
-                     (mkVarOccFS (fsLit "#x"))
-                     noSrcSpan
-
-make_row_vars_for_constructor :: (EqnNo, EquationInfo) -> [WarningPat]
-make_row_vars_for_constructor (_, EqnInfo { eqn_pats = pats})
-  = takeList (tail pats) (repeat nlWildPatName)
-
-compare_cons :: Pat Id -> Pat Id -> Bool
-compare_cons (ConPatOut{ pat_con = L _ con1 }) (ConPatOut{ pat_con = L _ con2 })
-  = case (con1, con2) of
-    (RealDataCon id1, RealDataCon id2) -> id1 == id2
-    _ -> False
-compare_cons _ _ = panic "Check.compare_cons: Not ConPatOut with RealDataCon"
-
-remove_dups :: [Pat Id] -> [Pat Id]
-remove_dups []     = []
-remove_dups (x:xs) | any (\y -> compare_cons x y) xs = remove_dups  xs
-                   | otherwise                       = x : remove_dups xs
-
-get_used_cons :: [(EqnNo, EquationInfo)] -> [Pat Id]
-get_used_cons qs = remove_dups [pat | q <- qs, let pat = firstPatN q,
-                                      isConPatOut pat]
-
-isConPatOut :: Pat Id -> Bool
-isConPatOut ConPatOut{ pat_con = L _ RealDataCon{} } = True
-isConPatOut _                                        = False
-
-remove_dups' :: [HsLit] -> [HsLit]
-remove_dups' []                   = []
-remove_dups' (x:xs) | x `elem` xs = remove_dups' xs
-                    | otherwise   = x : remove_dups' xs
-
-
-get_used_lits :: [(EqnNo, EquationInfo)] -> [HsLit]
-get_used_lits qs = remove_dups' all_literals
-                 where
-                   all_literals = get_used_lits' qs
-
-get_used_lits' :: [(EqnNo, EquationInfo)] -> [HsLit]
-get_used_lits' [] = []
-get_used_lits' (q:qs)
-  | Just lit <- get_lit (firstPatN q) = lit : get_used_lits' qs
-  | otherwise                         = get_used_lits qs
-
-get_lit :: Pat id -> Maybe HsLit
--- Get a representative HsLit to stand for the OverLit
--- It doesn't matter which one, because they will only be compared
--- with other HsLits gotten in the same way
-get_lit (LitPat lit)                                      = Just lit
-get_lit (NPat (L _ (OverLit { ol_val = HsIntegral src i}))    mb _)
-                        = Just (HsIntPrim src (mb_neg negate              mb i))
-get_lit (NPat (L _ (OverLit { ol_val = HsFractional f })) mb _)
-                        = Just (HsFloatPrim (mb_neg negateFractionalLit mb f))
-get_lit (NPat (L _ (OverLit { ol_val = HsIsString src s }))   _  _)
-                        = Just (HsStringPrim src (fastStringToByteString s))
-get_lit _                                                 = Nothing
-
-mb_neg :: (a -> a) -> Maybe b -> a -> a
-mb_neg _      Nothing  v = v
-mb_neg negate (Just _) v = negate v
-
-get_unused_cons :: [Pat Id] -> [DataCon]
-get_unused_cons used_cons = ASSERT( not (null used_cons) ) unused_cons
-     where
-       used_set :: UniqSet DataCon
-       used_set = mkUniqSet [d | ConPatOut{ pat_con = L _ (RealDataCon d) } <- used_cons]
-       (ConPatOut { pat_con = L _ (RealDataCon con1), pat_arg_tys = inst_tys }) = head used_cons
-       ty_con      = dataConTyCon con1
-       unused_cons = filterOut is_used (tyConDataCons ty_con)
-       is_used con = con `elementOfUniqSet` used_set
-                     || dataConCannotMatch inst_tys con
-
-all_vars :: [Pat Id] -> Bool
-all_vars []             = True
-all_vars (WildPat _:ps) = all_vars ps
-all_vars _              = False
-
-remove_var :: (EqnNo, EquationInfo) -> (EqnNo, EquationInfo)
-remove_var (n, eqn@(EqnInfo { eqn_pats = WildPat _ : ps})) = (n, eqn { eqn_pats = ps })
-remove_var _  = panic "Check.remove_var: equation does not begin with a variable"
-
------------------------
-eqnPats :: (EqnNo, EquationInfo) -> [Pat Id]
-eqnPats (_, eqn) = eqn_pats eqn
-
-okGroup :: [(EqnNo, EquationInfo)] -> Bool
--- True if all equations have at least one pattern, and
--- all have the same number of patterns
-okGroup [] = True
-okGroup (e:es) = n_pats > 0 && and [length (eqnPats e) == n_pats | e <- es]
-               where
-                 n_pats = length (eqnPats e)
-
--- Half-baked print
-pprGroup :: [(EqnNo, EquationInfo)] -> SDoc
-pprEqnInfo :: (EqnNo, EquationInfo) -> SDoc
-pprGroup es = vcat (map pprEqnInfo es)
-pprEqnInfo e = ppr (eqnPats e)
-
-
-firstPatN :: (EqnNo, EquationInfo) -> Pat Id
-firstPatN (_, eqn) = firstPat eqn
-
-is_con :: Pat Id -> Bool
-is_con (ConPatOut {}) = True
-is_con _              = False
-
-is_lit :: Pat Id -> Bool
-is_lit (LitPat _)      = True
-is_lit (NPat _ _ _)  = True
-is_lit _               = False
-
-is_var :: Pat Id -> Bool
-is_var (WildPat _) = True
-is_var _           = False
-
-is_var_con :: ConLike -> Pat Id -> Bool
-is_var_con _   (WildPat _)                     = True
-is_var_con con (ConPatOut{ pat_con = L _ id }) = id == con
-is_var_con _   _                               = False
-
-is_var_lit :: HsLit -> Pat Id -> Bool
-is_var_lit _   (WildPat _)   = True
-is_var_lit lit pat
-  | Just lit' <- get_lit pat = lit == lit'
-  | otherwise                = False
+{- Note [Type and Term Equality Propagation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When checking a match it would be great to have all type and term information
+available so we can get more precise results. For this reason we have functions
+`addDictsDs' and `addTmCsDs' in DsMonad that store in the environment type and
+term constraints (respectively) as we go deeper.
 
-{-
-The difference beteewn @make_con@ and @make_whole_con@ is that
-@make_whole_con@ creates a new constructor with all their arguments, and
-@make_con@ takes a list of arguments, creates the constructor getting their
-arguments from the list. See where \fbox{\ ???\ } are used for details.
-
-We need to reconstruct the patterns (make the constructors infix and
-similar) at the same time that we create the constructors.
-
-You can tell tuple constructors using
-\begin{verbatim}
-        Id.isTupleDataCon
-\end{verbatim}
-You can see if one constructor is infix with this clearer code :-))))))))))
-\begin{verbatim}
-        Lex.isLexConSym (Name.occNameString (Name.getOccName con))
-\end{verbatim}
-
-       Rather clumsy but it works. (Simon Peyton Jones)
-
-
-We don't mind the @nilDataCon@ because it doesn't change the way to
-print the message, we are searching only for things like: @[1,2,3]@,
-not @x:xs@ ....
-
-In @reconstruct_pat@ we want to ``undo'' the work
-that we have done in @tidy_pat@.
-In particular:
-\begin{tabular}{lll}
-        @((,) x y)@   & returns to be & @(x, y)@
-\\      @((:) x xs)@  & returns to be & @(x:xs)@
-\\      @(x:(...:[])@ & returns to be & @[x,...]@
-\end{tabular}
-
-The difficult case is the third one because we need to follow all the
-contructors until the @[]@ to know that we need to use the second case,
-not the second. \fbox{\ ???\ }
+The type constraints we propagate inwards are collected by `collectEvVarsPats'
+in HsPat.hs. This handles bug #4139 ( see example
+  https://ghc.haskell.org/trac/ghc/attachment/ticket/4139/GADTbug.hs )
+where this is needed.
+
+For term equalities we do less, we just generate equalities for HsCase. For
+example we accurately give 2 redundancy warnings for the marked cases:
+
+f :: [a] -> Bool
+f x = case x of
+
+  []    -> case x of        -- brings (x ~ []) in scope
+             []    -> True
+             (_:_) -> False -- can't happen
+
+  (_:_) -> case x of        -- brings (x ~ (_:_)) in scope
+             (_:_) -> True
+             []    -> False -- can't happen
+
+Functions `genCaseTmCs1' and `genCaseTmCs2' are responsible for generating
+these constraints.
 -}
 
-isInfixCon :: DataCon -> Bool
-isInfixCon con = isDataSymOcc (getOccName con)
-
-is_nil :: Pat Name -> Bool
-is_nil (ConPatIn con (PrefixCon [])) = unLoc con == getName nilDataCon
-is_nil _                             = False
-
-is_list :: Pat Name -> Bool
-is_list (ListPat _ _ Nothing) = True
-is_list _             = False
-
-return_list :: DataCon -> Pat Name -> Bool
-return_list id q = id == consDataCon && (is_nil q || is_list q)
-
-make_list :: LPat Name -> Pat Name -> Pat Name
-make_list p q | is_nil q    = ListPat [p] placeHolderType Nothing
-make_list p (ListPat ps ty Nothing) = ListPat (p:ps) ty Nothing
-make_list _ _               = panic "Check.make_list: Invalid argument"
-
-make_con :: Pat Id -> ExhaustivePat -> ExhaustivePat
-make_con (ConPatOut{ pat_con = L _ (RealDataCon id) }) (lp:lq:ps, constraints)
-     | return_list id q = (noLoc (make_list lp q) : ps, constraints)
-     | isInfixCon id    = (nlInfixConPat (getName id) lp lq : ps, constraints)
-   where q  = unLoc lq
-
-make_con (ConPatOut{ pat_con = L _ (RealDataCon id), pat_args = PrefixCon pats})
-         (ps, constraints)
-      | Just sort <- tyConTuple_maybe tc
-                         = (noLoc (TuplePat pats_con (tupleSortBoxity sort) [])
-                                : rest_pats, constraints)
-      | isPArrFakeCon id = (noLoc (PArrPat pats_con placeHolderType)
-                                : rest_pats, constraints)
-      | otherwise        = (nlConPatName name pats_con
-                                : rest_pats, constraints)
-    where
-        name                  = getName id
-        (pats_con, rest_pats) = splitAtList pats ps
-        tc                    = dataConTyCon id
-
-make_con _ _ = panic "Check.make_con: Not ConPatOut"
-
--- reconstruct parallel array pattern
---
---  * don't check for the type only; we need to make sure that we are really
---   dealing with one of the fake constructors and not with the real
---   representation
-
-make_whole_con :: DataCon -> WarningPat
-make_whole_con con | isInfixCon con = nlInfixConPat name
-                                           nlWildPatName nlWildPatName
-                   | otherwise      = nlConPatName name pats
-                where
-                  name   = getName con
-                  pats   = [nlWildPatName | _ <- dataConOrigArgTys con]
+-- | Generate equalities when checking a case expression:
+--     case x of { p1 -> e1; ... pn -> en }
+-- When we go deeper to check e.g. e1 we record two equalities:
+-- (x ~ y), where y is the initial uncovered when checking (p1; .. ; pn)
+-- and (x ~ p1).
+genCaseTmCs2 :: Maybe (LHsExpr Id) -- Scrutinee
+             -> [Pat Id]           -- LHS       (should have length 1)
+             -> [Id]               -- MatchVars (should have length 1)
+             -> DsM (Bag SimpleEq)
+genCaseTmCs2 Nothing _ _ = return emptyBag
+genCaseTmCs2 (Just scr) [p] [var] = liftUs $ do
+  [e] <- map valAbsToPmExpr . coercePatVec <$> translatePat 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:
+--     case x of { matches }
+-- When checking matches we record that (x ~ y) where y is the initial
+-- uncovered. All matches will have to satisfy this equality.
+genCaseTmCs1 :: Maybe (LHsExpr Id) -> [Id] -> Bag SimpleEq
+genCaseTmCs1 Nothing     _    = emptyBag
+genCaseTmCs1 (Just scr) [var] = unitBag (var, lhsExprToPmExpr scr)
+genCaseTmCs1 _ _              = panic "genCaseTmCs1: HsCase"
+
+{- Note [Literals in PmPat]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Instead of translating a literal to a variable accompanied with a guard, we
+treat them like constructor patterns. The following example from
+"./libraries/base/GHC/IO/Encoding.hs" shows why:
+
+mkTextEncoding' :: CodingFailureMode -> String -> IO TextEncoding
+mkTextEncoding' cfm enc = case [toUpper c | c <- enc, c /= '-'] of
+    "UTF8"    -> return $ UTF8.mkUTF8 cfm
+    "UTF16"   -> return $ UTF16.mkUTF16 cfm
+    "UTF16LE" -> return $ UTF16.mkUTF16le cfm
+    ...
+
+Each clause gets translated to a list of variables with an equal number of
+guards. For every guard we generate two cases (equals True/equals False) which
+means that we generate 2^n cases to feed the oracle with, where n is the sum of
+the length of all strings that appear in the patterns. For this particular
+example this means over 2^40 cases. Instead, by representing them like with
+constructor we get the following:
+  1. We exploit the common prefix with our representation of VSAs
+  2. We prune immediately non-reachable cases
+     (e.g. False == (x == "U"), True == (x == "U"))
+
+Note [Translating As Patterns]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Instead of translating x@p as:  x (p <- x)
+we instead translate it as:     p (x <- coercePattern p)
+for performance reasons. For example:
+
+  f x@True  = 1
+  f y@False = 2
+
+Gives the following with the first translation:
+
+  x |> {x == False, x == y, y == True}
+
+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
+guard pattern (value abstractions are a subset of expressions). We keep the
+guards in the first pattern `p' though.
+-}
 
 {-
-------------------------------------------------------------------------
-                   Tidying equations
-------------------------------------------------------------------------
-
-tidy_eqn does more or less the same thing as @tidy@ in @Match.hs@;
-that is, it removes syntactic sugar, reducing the number of cases that
-must be handled by the main checking algorithm.  One difference is
-that here we can do *all* the tidying at once (recursively), rather
-than doing it incrementally.
+%************************************************************************
+%*                                                                      *
+      Pretty printing of exhaustiveness/redundancy check warnings
+%*                                                                      *
+%************************************************************************
 -}
 
-tidy_eqn :: EquationInfo -> EquationInfo
-tidy_eqn eqn = eqn { eqn_pats = map tidy_pat (eqn_pats eqn),
-                     eqn_rhs  = tidy_rhs (eqn_rhs eqn) }
+dsPmWarn :: DynFlags -> DsMatchContext -> DsM PmResult -> DsM ()
+dsPmWarn dflags ctx@(DsMatchContext kind loc) mPmResult
+  = 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
+      when exists_r $ putSrcSpanDs loc (warnDs (pprEqns  redundant    rmsg))
+      when exists_i $ putSrcSpanDs loc (warnDs (pprEqns  inaccessible imsg))
+      when exists_u $ putSrcSpanDs loc (warnDs (pprEqnsU uncovered))
   where
-        -- Horrible hack.  The tidy_pat stuff converts "might-fail" patterns to
-        -- WildPats which of course loses the info that they can fail to match.
-        -- So we stick in a CanFail as if it were a guard.
-    tidy_rhs (MatchResult can_fail body)
-        | any might_fail_pat (eqn_pats eqn) = MatchResult CanFail body
-        | otherwise                         = MatchResult can_fail body
-
---------------
-might_fail_pat :: Pat Id -> Bool
--- Returns True for patterns that might fail
--- (that are not covered by the checking algorithm)  Specifically:
---         NPlusKPat
---         ViewPat (if refutable)
---         ConPatOut of a PatSynCon
-
--- First the two special cases
-might_fail_pat (NPlusKPat {})                = True
-might_fail_pat (ViewPat _ p _)               = not (isIrrefutableHsPat p)
-
--- Now the recursive stuff
-might_fail_pat (ParPat p)                    = might_fail_lpat p
-might_fail_pat (AsPat _ p)                   = might_fail_lpat p
-might_fail_pat (SigPatOut p _ )              = might_fail_lpat p
-might_fail_pat (ListPat ps _ Nothing)        = any might_fail_lpat ps
-might_fail_pat (ListPat _ _ (Just _))      = True
-might_fail_pat (TuplePat ps _ _)             = any might_fail_lpat ps
-might_fail_pat (PArrPat ps _)                = any might_fail_lpat ps
-might_fail_pat (BangPat p)                   = might_fail_lpat p
-might_fail_pat (ConPatOut { pat_con = con, pat_args = ps })
-  = case unLoc con of
-    RealDataCon _dcon -> any might_fail_lpat (hsConPatArgs ps)
-    PatSynCon _psyn -> True -- This is considered 'might fail', as pattern synonym
-                            -- is not supported by checking algorithm
-
--- Finally the ones that are sure to succeed, or which are covered by the checking algorithm
-might_fail_pat (LazyPat _)                   = False -- Always succeeds
-might_fail_pat _                             = False -- VarPat, WildPat, LitPat, NPat
-
---------------
-might_fail_lpat :: LPat Id -> Bool
-might_fail_lpat (L _ p) = might_fail_pat p
-
---------------
-tidy_lpat :: LPat Id -> LPat Id
-tidy_lpat p = fmap tidy_pat p
-
---------------
-tidy_pat :: Pat Id -> Pat Id
-tidy_pat pat@(WildPat _)  = pat
-tidy_pat (VarPat id)      = WildPat (idType (unLoc id))
-tidy_pat (ParPat p)       = tidy_pat (unLoc p)
-tidy_pat (LazyPat p)      = WildPat (hsLPatType p)      -- For overlap and exhaustiveness checking
-                                                        -- purposes, a ~pat is like a wildcard
-tidy_pat (BangPat p)      = tidy_pat (unLoc p)
-tidy_pat (AsPat _ p)      = tidy_pat (unLoc p)
-tidy_pat (SigPatOut p _)  = tidy_pat (unLoc p)
-tidy_pat (CoPat _ pat _)  = tidy_pat pat
-
--- These are might_fail patterns, so we map them to
--- WildPats.  The might_fail_pat stuff arranges that the
--- guard says "this equation might fall through".
-tidy_pat (NPlusKPat id _ _ _) = WildPat (idType (unLoc id))
-tidy_pat (ViewPat _ _ ty)     = WildPat ty
-tidy_pat (ListPat _ _ (Just (ty,_))) = WildPat ty
-tidy_pat (ConPatOut { pat_con = L _ (PatSynCon syn), pat_arg_tys = tys })
-  = WildPat (patSynInstResTy syn tys)
-
-tidy_pat pat@(ConPatOut { pat_con = L _ con, pat_args = ps })
-  = pat { pat_args = tidy_con con ps }
-
-tidy_pat (ListPat ps ty Nothing)
-  = unLoc $ foldr (\ x y -> mkPrefixConPat consDataCon [x,y] [ty])
-                                  (mkNilPat ty)
-                                  (map tidy_lpat ps)
-
--- introduce fake parallel array constructors to be able to handle parallel
--- arrays with the existing machinery for constructor pattern
---
-tidy_pat (PArrPat ps ty)
-  = unLoc $ mkPrefixConPat (parrFakeCon (length ps))
-                           (map tidy_lpat ps)
-                           [ty]
-
-tidy_pat (TuplePat ps boxity tys)
-  = unLoc $ mkPrefixConPat (tupleDataCon boxity arity)
-                           (map tidy_lpat ps) tys
+    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 ->
+      vcat (map (ppr_eqn f kind) (take maximum_output qs)) $$ dots qs
+
+    pprEqnsU qs = pp_context ctx (ptext (sLit "are non-exhaustive")) $ \_ ->
+      let us = map ppr_uncovered qs
+      in  hang (ptext (sLit "Patterns not matched:")) 4
+               (vcat (take maximum_output us) $$ dots us)
+
+dots :: [a] -> SDoc
+dots qs | qs `lengthExceeds` maximum_output = ptext (sLit "...")
+        | otherwise                         = empty
+
+exhaustive :: DynFlags -> HsMatchContext id -> Bool
+exhaustive  dflags (FunRhs {})   = wopt Opt_WarnIncompletePatterns dflags
+exhaustive  dflags CaseAlt       = wopt Opt_WarnIncompletePatterns dflags
+exhaustive _dflags IfAlt         = False
+exhaustive  dflags LambdaExpr    = wopt Opt_WarnIncompleteUniPatterns dflags
+exhaustive  dflags PatBindRhs    = wopt Opt_WarnIncompleteUniPatterns dflags
+exhaustive  dflags ProcExpr      = wopt Opt_WarnIncompleteUniPatterns dflags
+exhaustive  dflags RecUpd        = wopt Opt_WarnIncompletePatternsRecUpd dflags
+exhaustive _dflags ThPatSplice   = False
+exhaustive _dflags PatSyn        = False
+exhaustive _dflags ThPatQuote    = False
+exhaustive _dflags (StmtCtxt {}) = False -- Don't warn about incomplete patterns
+                                       -- in list comprehensions, pattern guards
+                                       -- etc. They are often *supposed* to be
+                                       -- incomplete
+
+pp_context :: DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
+pp_context (DsMatchContext kind _loc) msg rest_of_msg_fun
+  = vcat [ptext (sLit "Pattern match(es)") <+> msg,
+          sep [ ptext (sLit "In") <+> ppr_match <> char ':'
+              , nest 4 (rest_of_msg_fun pref)]]
   where
-    arity = length ps
-
-tidy_pat (NPat (L _ lit) mb_neg eq) = tidyNPat tidy_lit_pat lit mb_neg eq
-tidy_pat (LitPat lit)         = tidy_lit_pat lit
-
-tidy_pat (ConPatIn {})        = panic "Check.tidy_pat: ConPatIn"
-tidy_pat (SplicePat {})       = panic "Check.tidy_pat: SplicePat"
-tidy_pat (SigPatIn {})        = panic "Check.tidy_pat: SigPatIn"
-
-tidy_lit_pat :: HsLit -> Pat Id
--- Unpack string patterns fully, so we can see when they
--- overlap with each other, or even explicit lists of Chars.
-tidy_lit_pat lit
-  | HsString src s <- lit
-  = unLoc $ foldr (\c pat -> mkPrefixConPat consDataCon
-                                             [mkCharLitPat src c, pat] [charTy])
-                  (mkPrefixConPat nilDataCon [] [charTy]) (unpackFS s)
-  | otherwise
-  = tidyLitPat lit
-
------------------
-tidy_con :: ConLike -> HsConPatDetails Id -> HsConPatDetails Id
-tidy_con _   (PrefixCon ps)   = PrefixCon (map tidy_lpat ps)
-tidy_con _   (InfixCon p1 p2) = PrefixCon [tidy_lpat p1, tidy_lpat p2]
-tidy_con con (RecCon (HsRecFields fs _))
-  | null fs   = PrefixCon (replicate arity nlWildPatId)
-                -- Special case for null patterns; maybe not a record at all
-  | otherwise = PrefixCon (map (tidy_lpat.snd) all_pats)
+    (ppr_match, pref)
+        = case kind of
+             FunRhs fun -> (pprMatchContext kind, \ pp -> ppr fun <+> pp)
+             _          -> (pprMatchContext kind, \ pp -> pp)
+
+ppr_pats :: HsMatchContext Name -> [Pat Id] -> SDoc
+ppr_pats kind pats
+  = sep [sep (map ppr pats), matchSeparator kind, ptext (sLit "...")]
+
+ppr_eqn :: (SDoc -> SDoc) -> HsMatchContext Name -> [LPat Id] -> SDoc
+ppr_eqn prefixF kind eqn = prefixF (ppr_pats kind (map unLoc eqn))
+
+ppr_constraint :: (SDoc,[PmLit]) -> SDoc
+ppr_constraint (var, lits) = var <+> ptext (sLit "is not one of")
+                                 <+> braces (pprWithCommas ppr lits)
+
+ppr_uncovered :: ([PmExpr], [ComplexEq]) -> SDoc
+ppr_uncovered (expr_vec, complex)
+  | null cs   = fsep vec -- there are no literal constraints
+  | otherwise = hang (fsep vec) 4 $
+                  ptext (sLit "where") <+> vcat (map ppr_constraint cs)
   where
-    arity = conLikeArity con
-
-     -- pad out all the missing fields with WildPats.
-    field_pats = case con of
-        RealDataCon dc -> map (\ f -> (flSelector f, nlWildPatId)) (dataConFieldLabels dc)
-        PatSynCon{}    -> panic "Check.tidy_con: pattern synonym with record syntax"
-    all_pats = foldr (\ (L _ x) acc -> insertNm (getName (unLoc (hsRecFieldId x))) (hsRecFieldArg x) acc)
-                     field_pats fs
-
-    insertNm nm p [] = [(nm,p)]
-    insertNm nm p (x@(n,_):xs)
-      | nm == n    = (nm,p):xs
-      | otherwise  = x : insertNm nm p xs
+    sdoc_vec = mapM pprPmExprWithParens expr_vec
+    (vec,cs) = runPmPprM sdoc_vec (filterComplex complex)
diff --git a/compiler/deSugar/DsBinds.hs b/compiler/deSugar/DsBinds.hs
index 64d5521927..0da90f0003 100644
--- a/compiler/deSugar/DsBinds.hs
+++ b/compiler/deSugar/DsBinds.hs
@@ -130,7 +130,7 @@ dsHsBind dflags
 dsHsBind dflags
          (FunBind { fun_id = L _ fun, fun_matches = matches
                   , fun_co_fn = co_fn, fun_tick = tick })
- = do   { (args, body) <- matchWrapper (FunRhs (idName fun)) matches
+ = do   { (args, body) <- matchWrapper (FunRhs (idName fun)) Nothing matches
         ; let body' = mkOptTickBox tick body
         ; rhs <- dsHsWrapper co_fn (mkLams args body')
         ; let core_binds@(id,_) = makeCorePair dflags fun False 0 rhs
@@ -169,7 +169,9 @@ dsHsBind dflags
         , abe_mono = local, abe_prags = prags } <- export
   , not (xopt Opt_Strict dflags)                 -- handle strict binds
   , not (anyBag (isBangedPatBind . unLoc) binds) -- in the next case
-  = do  { (_, bind_prs) <- ds_lhs_binds binds
+  = -- push type constraints deeper for pattern match check
+    addDictsDs (toTcTypeBag (listToBag dicts)) $
+     do { (_, bind_prs) <- ds_lhs_binds binds
         ; let core_bind = Rec bind_prs
         ; ds_binds <- dsTcEvBinds_s ev_binds
         ; rhs <- dsHsWrapper wrap $  -- Usually the identity
@@ -191,7 +193,9 @@ dsHsBind dflags
                    , abs_exports = exports, abs_ev_binds = ev_binds
                    , abs_binds = binds })
          -- See Note [Desugaring AbsBinds]
-  = do  { (local_force_vars, bind_prs) <- ds_lhs_binds binds
+  = -- push type constraints deeper for pattern match check
+    addDictsDs (toTcTypeBag (listToBag dicts)) $
+     do { (local_force_vars, bind_prs) <- ds_lhs_binds binds
         ; let core_bind = Rec [ makeCorePair dflags (add_inline lcl_id) False 0 rhs
                               | (lcl_id, rhs) <- bind_prs ]
                 -- Monomorphic recursion possible, hence Rec
diff --git a/compiler/deSugar/DsExpr.hs b/compiler/deSugar/DsExpr.hs
index cd6b96c290..e4c6ff8cfa 100644
--- a/compiler/deSugar/DsExpr.hs
+++ b/compiler/deSugar/DsExpr.hs
@@ -150,7 +150,7 @@ dsUnliftedBind (FunBind { fun_id = L _ fun
                         , fun_tick = tick }) body
                -- Can't be a bang pattern (that looks like a PatBind)
                -- so must be simply unboxed
-  = do { (args, rhs) <- matchWrapper (FunRhs (idName fun)) matches
+  = do { (args, rhs) <- matchWrapper (FunRhs (idName fun)) Nothing matches
        ; MASSERT( null args ) -- Functions aren't lifted
        ; MASSERT( isIdHsWrapper co_fn )
        ; let rhs' = mkOptTickBox tick rhs
@@ -215,11 +215,11 @@ dsExpr (NegApp expr neg_expr)
   = App <$> dsExpr neg_expr <*> dsLExpr expr
 
 dsExpr (HsLam a_Match)
-  = uncurry mkLams <$> matchWrapper LambdaExpr a_Match
+  = uncurry mkLams <$> matchWrapper LambdaExpr Nothing a_Match
 
 dsExpr (HsLamCase arg matches)
   = do { arg_var <- newSysLocalDs arg
-       ; ([discrim_var], matching_code) <- matchWrapper CaseAlt matches
+       ; ([discrim_var], matching_code) <- matchWrapper CaseAlt Nothing matches
        ; return $ Lam arg_var $ bindNonRec discrim_var (Var arg_var) matching_code }
 
 dsExpr e@(HsApp fun arg)
@@ -319,7 +319,7 @@ dsExpr (HsCoreAnn _ _ expr)
 
 dsExpr (HsCase discrim matches)
   = do { core_discrim <- dsLExpr discrim
-       ; ([discrim_var], matching_code) <- matchWrapper CaseAlt matches
+       ; ([discrim_var], matching_code) <- matchWrapper CaseAlt (Just discrim) matches
        ; return (bindNonRec discrim_var core_discrim matching_code) }
 
 -- Pepe: The binds are in scope in the body but NOT in the binding group
@@ -576,11 +576,11 @@ dsExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = fields
         -- constructor aguments.
         ; alts <- mapM (mk_alt upd_fld_env) cons_to_upd
         ; ([discrim_var], matching_code)
-                <- matchWrapper RecUpd (MG { mg_alts = noLoc alts
-                                           , mg_arg_tys = [in_ty]
-                                           , mg_res_ty = out_ty, mg_origin = FromSource })
-                                           -- FromSource is not strictly right, but we
-                                           -- want incomplete pattern-match warnings
+                <- matchWrapper RecUpd Nothing (MG { mg_alts = noLoc alts
+                                                   , mg_arg_tys = [in_ty]
+                                                   , mg_res_ty = out_ty, mg_origin = FromSource })
+                                                   -- FromSource is not strictly right, but we
+                                                   -- want incomplete pattern-match warnings
 
         ; return (add_field_binds field_binds' $
                   bindNonRec discrim_var record_expr' matching_code) }
diff --git a/compiler/deSugar/DsGRHSs.hs b/compiler/deSugar/DsGRHSs.hs
index c5217f1113..352534bb17 100644
--- a/compiler/deSugar/DsGRHSs.hs
+++ b/compiler/deSugar/DsGRHSs.hs
@@ -8,7 +8,7 @@ Matching guarded right-hand-sides (GRHSs)
 
 {-# LANGUAGE CPP #-}
 
-module DsGRHSs ( dsGuarded, dsGRHSs, dsGRHS ) where
+module DsGRHSs ( dsGuarded, dsGRHSs, dsGRHS, isTrueLHsExpr ) where
 
 #include "HsVersions.h"
 
diff --git a/compiler/deSugar/DsMonad.hs b/compiler/deSugar/DsMonad.hs
index 6220a95b77..e33af7ce2c 100644
--- a/compiler/deSugar/DsMonad.hs
+++ b/compiler/deSugar/DsMonad.hs
@@ -11,7 +11,7 @@
 
 module DsMonad (
         DsM, mapM, mapAndUnzipM,
-        initDs, initDsTc, fixDs,
+        initDs, initDsTc, initTcDsForSolver, fixDs,
         foldlM, foldrM, whenGOptM, unsetGOptM, unsetWOptM,
         Applicative(..),(<$>),
 
@@ -31,6 +31,9 @@ module DsMonad (
 
         DsMetaEnv, DsMetaVal(..), dsGetMetaEnv, dsLookupMetaEnv, dsExtendMetaEnv,
 
+        -- Getting and setting EvVars and term constraints in local environment
+        getDictsDs, addDictsDs, getTmCsDs, addTmCsDs,
+
         -- Warnings
         DsWarning, warnDs, failWithDs, discardWarningsDs,
 
@@ -54,6 +57,7 @@ import HscTypes
 import Bag
 import DataCon
 import TyCon
+import PmExpr
 import Id
 import Module
 import Outputable
@@ -66,6 +70,7 @@ import DynFlags
 import ErrUtils
 import FastString
 import Maybes
+import Var (EvVar)
 import GHC.Fingerprint
 
 import Data.IORef
@@ -227,12 +232,36 @@ initDsTc thing_inside
         ; setEnvs ds_envs thing_inside
         }
 
+initTcDsForSolver :: TcM a -> DsM (Messages, Maybe a)
+-- Spin up a TcM context so that we can run the constraint solver
+-- Returns any error messages generated by the constraint solver
+-- and (Just res) if no error happened; Nothing if an errror happened
+--
+-- Simon says: I'm not very happy about this.  We spin up a complete TcM monad
+--             only to immediately refine it to a TcS monad.
+-- Better perhaps to make TcS into its own monad, rather than building on TcS
+-- But that may in turn interact with plugins
+
+initTcDsForSolver thing_inside
+  = do { (gbl, lcl) <- getEnvs
+       ; hsc_env    <- getTopEnv
+
+       ; let DsGblEnv { ds_mod = mod
+                      , ds_fam_inst_env = fam_inst_env } = gbl
+
+             DsLclEnv { dsl_loc = loc }                  = lcl
+
+       ; liftIO $ initTc hsc_env HsSrcFile False mod loc $
+         updGblEnv (\tc_gbl -> tc_gbl { tcg_fam_inst_env = fam_inst_env }) $
+         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
   = let if_genv = IfGblEnv { if_rec_types = Just (mod, return type_env) }
         if_lenv = mkIfLclEnv mod (ptext (sLit "GHC error in desugarer lookup in") <+> ppr mod)
+        real_span = realSrcLocSpan (mkRealSrcLoc (moduleNameFS (moduleName mod)) 1 1)
         gbl_env = DsGblEnv { ds_mod     = mod
                            , ds_fam_inst_env = fam_inst_env
                            , ds_if_env  = (if_genv, if_lenv)
@@ -242,8 +271,10 @@ 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  = noSrcSpan
+        lcl_env = DsLclEnv { dsl_meta  = emptyNameEnv
+                           , dsl_loc   = real_span
+                           , dsl_dicts = emptyBag
+                           , dsl_tm_cs = emptyBag
                            }
     in (gbl_env, lcl_env)
 
@@ -305,11 +336,34 @@ the @SrcSpan@ being carried around.
 getGhcModeDs :: DsM GhcMode
 getGhcModeDs =  getDynFlags >>= return . ghcMode
 
+-- | Get in-scope type constraints (pm check)
+getDictsDs :: DsM (Bag EvVar)
+getDictsDs = do { env <- getLclEnv; return (dsl_dicts env) }
+
+-- | Add in-scope type constraints (pm check)
+addDictsDs :: Bag EvVar -> DsM a -> DsM a
+addDictsDs ev_vars
+  = updLclEnv (\env -> env { dsl_dicts = unionBags ev_vars (dsl_dicts env) })
+
+-- | Get in-scope term constraints (pm check)
+getTmCsDs :: DsM (Bag SimpleEq)
+getTmCsDs = do { env <- getLclEnv; return (dsl_tm_cs env) }
+
+-- | Add in-scope term constraints (pm check)
+addTmCsDs :: Bag SimpleEq -> DsM a -> DsM a
+addTmCsDs tm_cs
+  = updLclEnv (\env -> env { dsl_tm_cs = unionBags tm_cs (dsl_tm_cs env) })
+
 getSrcSpanDs :: DsM SrcSpan
-getSrcSpanDs = do { env <- getLclEnv; return (dsl_loc env) }
+getSrcSpanDs = do { env <- getLclEnv
+                  ; return (RealSrcSpan (dsl_loc env)) }
 
 putSrcSpanDs :: SrcSpan -> DsM a -> DsM a
-putSrcSpanDs new_loc thing_inside = updLclEnv (\ env -> env {dsl_loc = new_loc}) thing_inside
+putSrcSpanDs (UnhelpfulSpan {}) thing_inside
+  = thing_inside
+putSrcSpanDs (RealSrcSpan real_span) thing_inside
+  = updLclEnv (\ env -> env {dsl_loc = real_span}) thing_inside
+
 warnDs :: SDoc -> DsM ()
 warnDs warn = do { env <- getGblEnv
                  ; loc <- getSrcSpanDs
diff --git a/compiler/deSugar/Match.hs b/compiler/deSugar/Match.hs
index 28b30c4d5b..3910250bc7 100644
--- a/compiler/deSugar/Match.hs
+++ b/compiler/deSugar/Match.hs
@@ -35,6 +35,7 @@ import PatSyn
 import MatchCon
 import MatchLit
 import Type
+import TcType ( toTcTypeBag )
 import TyCon( isNewTyCon )
 import TysWiredIn
 import ListSetOps
@@ -44,133 +45,11 @@ import Util
 import Name
 import Outputable
 import BasicTypes ( isGenerated )
-import FastString
 
-import Control.Monad( when )
+import Control.Monad( unless )
 import qualified Data.Map as Map
 
 {-
-This function is a wrapper of @match@, it must be called from all the parts where
-it was called match, but only substitutes the first call, ....
-if the associated flags are declared, warnings will be issued.
-It can not be called matchWrapper because this name already exists :-(
-
-JJCQ 30-Nov-1997
--}
-
-matchCheck ::  DsMatchContext
-            -> [Id]             -- Vars rep'ing the exprs we're matching with
-            -> Type             -- Type of the case expression
-            -> [EquationInfo]   -- Info about patterns, etc. (type synonym below)
-            -> DsM MatchResult  -- Desugared result!
-
-matchCheck ctx vars ty qs
-  = do { dflags <- getDynFlags
-       ; matchCheck_really dflags ctx vars ty qs }
-
-matchCheck_really :: DynFlags
-                  -> DsMatchContext
-                  -> [Id]
-                  -> Type
-                  -> [EquationInfo]
-                  -> DsM MatchResult
-matchCheck_really dflags ctx@(DsMatchContext hs_ctx _) vars ty qs
-  = do { when shadow (dsShadowWarn ctx eqns_shadow)
-       ; when incomplete (dsIncompleteWarn ctx pats)
-       ; match vars ty qs }
-  where
-    (pats, eqns_shadow) = check qs
-    incomplete = incomplete_flag hs_ctx && notNull pats
-    shadow     = wopt Opt_WarnOverlappingPatterns dflags
-              && notNull eqns_shadow
-
-    incomplete_flag :: HsMatchContext id -> Bool
-    incomplete_flag (FunRhs {})   = wopt Opt_WarnIncompletePatterns dflags
-    incomplete_flag CaseAlt       = wopt Opt_WarnIncompletePatterns dflags
-    incomplete_flag IfAlt         = False
-
-    incomplete_flag LambdaExpr    = wopt Opt_WarnIncompleteUniPatterns dflags
-    incomplete_flag PatBindRhs    = wopt Opt_WarnIncompleteUniPatterns dflags
-    incomplete_flag ProcExpr      = wopt Opt_WarnIncompleteUniPatterns dflags
-
-    incomplete_flag RecUpd        = wopt Opt_WarnIncompletePatternsRecUpd dflags
-
-    incomplete_flag ThPatSplice   = False
-    incomplete_flag PatSyn        = False
-    incomplete_flag ThPatQuote    = False
-    incomplete_flag (StmtCtxt {}) = False  -- Don't warn about incomplete patterns
-                                           -- in list comprehensions, pattern guards
-                                           -- etc.  They are often *supposed* to be
-                                           -- incomplete
-
-{-
-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
-
--- The next two functions create the warning message.
-
-dsShadowWarn :: DsMatchContext -> [EquationInfo] -> DsM ()
-dsShadowWarn ctx@(DsMatchContext kind loc) qs
-  = putSrcSpanDs loc (warnDs warn)
-  where
-    warn | qs `lengthExceeds` maximum_output
-         = pp_context ctx (ptext (sLit "are overlapped"))
-                      (\ f -> vcat (map (ppr_eqn f kind) (take maximum_output qs)) $$
-                      ptext (sLit "..."))
-         | otherwise
-         = pp_context ctx (ptext (sLit "are overlapped"))
-                      (\ f -> vcat $ map (ppr_eqn f kind) qs)
-
-
-dsIncompleteWarn :: DsMatchContext -> [ExhaustivePat] -> DsM ()
-dsIncompleteWarn ctx@(DsMatchContext kind loc) pats
-  = putSrcSpanDs loc (warnDs warn)
-        where
-          warn = pp_context ctx (ptext (sLit "are non-exhaustive"))
-                            (\_ -> hang (ptext (sLit "Patterns not matched:"))
-                                   4 ((vcat $ map (ppr_incomplete_pats kind)
-                                                  (take maximum_output pats))
-                                      $$ dots))
-
-          dots | pats `lengthExceeds` maximum_output = ptext (sLit "...")
-               | otherwise                           = empty
-
-pp_context :: DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
-pp_context (DsMatchContext kind _loc) msg rest_of_msg_fun
-  = vcat [ptext (sLit "Pattern match(es)") <+> msg,
-          sep [ptext (sLit "In") <+> ppr_match <> char ':', nest 4 (rest_of_msg_fun pref)]]
-  where
-    (ppr_match, pref)
-        = case kind of
-             FunRhs fun -> (pprMatchContext kind, \ pp -> ppr fun <+> pp)
-             _          -> (pprMatchContext kind, \ pp -> pp)
-
-ppr_pats :: Outputable a => [a] -> SDoc
-ppr_pats pats = sep (map ppr pats)
-
-ppr_shadow_pats :: HsMatchContext Name -> [Pat Id] -> SDoc
-ppr_shadow_pats kind pats
-  = sep [ppr_pats pats, matchSeparator kind, ptext (sLit "...")]
-
-ppr_incomplete_pats :: HsMatchContext Name -> ExhaustivePat -> SDoc
-ppr_incomplete_pats _ (pats,[]) = ppr_pats pats
-ppr_incomplete_pats _ (pats,constraints) =
-                         sep [ppr_pats pats, ptext (sLit "with"),
-                              sep (map ppr_constraint constraints)]
-
-ppr_constraint :: (Name,[HsLit]) -> SDoc
-ppr_constraint (var,pats) = sep [ppr var, ptext (sLit "`notElem`"), ppr pats]
-
-ppr_eqn :: (SDoc -> SDoc) -> HsMatchContext Name -> EquationInfo -> SDoc
-ppr_eqn prefixF kind eqn = prefixF (ppr_shadow_pats kind (eqn_pats eqn))
-
-{-
 ************************************************************************
 *                                                                      *
                 The main matching function
@@ -764,6 +643,7 @@ Call @match@ with all of this information!
 -}
 
 matchWrapper :: HsMatchContext Name         -- For shadowing warning messages
+             -> Maybe (LHsExpr Id)          -- The scrutinee, if we check a case expr
              -> MatchGroup Id (LHsExpr Id)  -- Matches being desugared
              -> DsM ([Id], CoreExpr)        -- Results
 
@@ -791,22 +671,38 @@ one pattern, and match simply only accepts one pattern.
 JJQC 30-Nov-1997
 -}
 
-matchWrapper ctxt (MG { mg_alts = L _ matches
-                      , mg_arg_tys = arg_tys
-                      , mg_res_ty = rhs_ty
-                      , mg_origin = origin })
-  = do  { eqns_info   <- mapM mk_eqn_info matches
+matchWrapper ctxt mb_scr (MG { mg_alts = L _ matches
+                             , mg_arg_tys = arg_tys
+                             , mg_res_ty = rhs_ty
+                             , mg_origin = origin })
+  = do  { dflags <- getDynFlags
+        ; locn   <- getSrcSpanDs
+
         ; new_vars    <- case matches of
                            []    -> mapM newSysLocalDs arg_tys
                            (m:_) -> selectMatchVars (map unLoc (hsLMatchPats m))
+
+        ; eqns_info   <- mapM (mk_eqn_info new_vars) matches
+
+        -- pattern match check warnings
+        ; unless (isGenerated origin) $
+            -- See Note [Type and Term Equality Propagation]
+            addTmCsDs (genCaseTmCs1 mb_scr new_vars) $
+              dsPmWarn dflags (DsMatchContext ctxt locn) $
+                checkMatches new_vars matches
+
         ; result_expr <- handleWarnings $
                          matchEquations ctxt new_vars eqns_info rhs_ty
         ; return (new_vars, result_expr) }
   where
-    mk_eqn_info (L _ (Match _ pats _ grhss))
+    mk_eqn_info vars (L _ (Match _ pats _ grhss))
       = do { dflags <- getDynFlags
            ; let upats = map (strictify dflags) pats
-           ; match_result <- dsGRHSs ctxt upats grhss rhs_ty
+                 dicts = toTcTypeBag (collectEvVarsPats upats) -- Only TcTyVars
+           ; tm_cs <- genCaseTmCs2 mb_scr upats vars
+           ; match_result <- addDictsDs dicts $  -- See Note [Type and Term Equality Propagation]
+                               addTmCsDs tm_cs $ -- See Note [Type and Term Equality Propagation]
+                                 dsGRHSs ctxt upats grhss rhs_ty
            ; return (EqnInfo { eqn_pats = upats, eqn_rhs  = match_result}) }
 
     strictify dflags pat =
@@ -822,11 +718,9 @@ matchEquations  :: HsMatchContext Name
                 -> [Id] -> [EquationInfo] -> Type
                 -> DsM CoreExpr
 matchEquations ctxt vars eqns_info rhs_ty
-  = do  { locn <- getSrcSpanDs
-        ; let   ds_ctxt   = DsMatchContext ctxt locn
-                error_doc = matchContextErrString ctxt
+  = do  { let error_doc = matchContextErrString ctxt
 
-        ; match_result <- matchCheck ds_ctxt vars rhs_ty eqns_info
+        ; match_result <- match vars rhs_ty eqns_info
 
         ; fail_expr <- mkErrorAppDs pAT_ERROR_ID rhs_ty error_doc
         ; extractMatchResult match_result fail_expr }
@@ -864,10 +758,14 @@ matchSinglePat :: CoreExpr -> HsMatchContext Name -> LPat Id
 -- Used for things like [ e | pat <- stuff ], where
 -- incomplete patterns are just fine
 matchSinglePat (Var var) ctx (L _ pat) ty match_result
-  = do { locn <- getSrcSpanDs
-       ; matchCheck (DsMatchContext ctx locn)
-                    [var] ty
-                    [EqnInfo { eqn_pats = [pat], eqn_rhs  = match_result }] }
+  = do { dflags <- getDynFlags
+       ; locn   <- getSrcSpanDs
+
+       -- pattern match check warnings
+       ; dsPmWarn dflags (DsMatchContext ctx locn) (checkSingle var pat)
+
+       ; match [var] ty
+               [EqnInfo { eqn_pats = [pat], eqn_rhs  = match_result }] }
 
 matchSinglePat scrut hs_ctx pat ty match_result
   = do { var <- selectSimpleMatchVarL pat
diff --git a/compiler/deSugar/Match.hs-boot b/compiler/deSugar/Match.hs-boot
index 826f635e32..31bd351caa 100644
--- a/compiler/deSugar/Match.hs-boot
+++ b/compiler/deSugar/Match.hs-boot
@@ -13,6 +13,7 @@ match   :: [Id]
 
 matchWrapper
         :: HsMatchContext Name
+        -> Maybe (LHsExpr Id)
         -> MatchGroup Id (LHsExpr Id)
         -> DsM ([Id], CoreExpr)
 
diff --git a/compiler/deSugar/PmExpr.hs b/compiler/deSugar/PmExpr.hs
new file mode 100644
index 0000000000..c28e95d90d
--- /dev/null
+++ b/compiler/deSugar/PmExpr.hs
@@ -0,0 +1,377 @@
+{-
+Author: George Karachalias <george.karachalias@cs.kuleuven.be>
+
+Haskell expressions (as used by the pattern matching checker) and utilities.
+-}
+
+{-# LANGUAGE CPP #-}
+
+module PmExpr (
+        PmExpr(..), PmLit(..), SimpleEq, ComplexEq, eqPmLit,
+        truePmExpr, falsePmExpr, isTruePmExpr, isFalsePmExpr, isNotPmExprOther,
+        lhsExprToPmExpr, hsExprToPmExpr, substComplexEq, filterComplex,
+        pprPmExprWithParens, runPmPprM
+    ) where
+
+#include "HsVersions.h"
+
+import HsSyn
+import Id
+import DataCon
+import TysWiredIn
+import Outputable
+import Util
+import SrcLoc
+import FastString -- sLit
+import VarSet
+
+import Data.Functor ((<$>))
+import Data.Maybe (mapMaybe)
+import Data.List (groupBy, sortBy)
+import Control.Monad.Trans.State.Lazy
+
+{-
+%************************************************************************
+%*                                                                      *
+                         Lifted Expressions
+%*                                                                      *
+%************************************************************************
+-}
+
+{- Note [PmExprOther in PmExpr]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Since there is no plan to extend the (currently pretty naive) term oracle in
+the near future, instead of playing with the verbose (HsExpr Id), we lift it to
+PmExpr. All expressions the term oracle does not handle are wrapped by the
+constructor PmExprOther. Note that we do not perform substitution in
+PmExprOther. Because of this, we do not even print PmExprOther, since they may
+refer to variables that are otherwise substituted away.
+-}
+
+-- ----------------------------------------------------------------------------
+-- ** Types
+
+-- | Lifted expressions for pattern match checking.
+data PmExpr = PmExprVar   Id
+            | PmExprCon   DataCon [PmExpr]
+            | PmExprLit   PmLit
+            | PmExprEq    PmExpr PmExpr  -- Syntactic equality
+            | PmExprOther (HsExpr Id)    -- Note [PmExprOther in PmExpr]
+
+-- | Literals (simple and overloaded ones) for pattern match checking.
+data PmLit = PmSLit HsLit                                    -- simple
+           | PmOLit Bool {- is it negated? -} (HsOverLit Id) -- overloaded
+
+-- | PmLit equality. If both literals are overloaded, the equality check may be
+-- inconclusive. Since an overloaded PmLit represents a function application
+-- (e.g.  fromInteger 5), if two literals look the same they are the same but
+-- if they don't, whether they are depends on the implementation of the
+-- from-function.
+eqPmLit :: PmLit -> PmLit -> Maybe Bool
+eqPmLit (PmSLit    l1) (PmSLit l2   ) = Just (l1 == l2)
+eqPmLit (PmOLit b1 l1) (PmOLit b2 l2) = if res then Just True else Nothing
+  where res = b1 == b2 && l1 == l2
+eqPmLit _ _ = Just False -- this should not even happen I think
+
+nubPmLit :: [PmLit] -> [PmLit]
+nubPmLit []     = []
+nubPmLit [x]    = [x]
+nubPmLit (x:xs) = x : nubPmLit (filter (neqPmLit x) xs)
+  where neqPmLit l1 l2 = case eqPmLit l1 l2 of
+          Just True  -> False
+          Just False -> True
+          Nothing    -> True
+
+-- | Term equalities
+type SimpleEq  = (Id, PmExpr) -- We always use this orientation
+type ComplexEq = (PmExpr, PmExpr)
+
+-- | Expression `True'
+truePmExpr :: PmExpr
+truePmExpr = PmExprCon trueDataCon []
+
+-- | Expression `False'
+falsePmExpr :: PmExpr
+falsePmExpr = PmExprCon falseDataCon []
+
+-- ----------------------------------------------------------------------------
+-- ** Predicates on PmExpr
+
+-- | Check if an expression is lifted or not
+isNotPmExprOther :: PmExpr -> Bool
+isNotPmExprOther (PmExprOther _) = False
+isNotPmExprOther _expr           = True
+
+-- | Check whether a literal is negated
+isNegatedPmLit :: PmLit -> Bool
+isNegatedPmLit (PmOLit b _) = b
+isNegatedPmLit _other_lit   = False
+
+-- | Check whether a PmExpr is syntactically equal to term `True'.
+isTruePmExpr :: PmExpr -> Bool
+isTruePmExpr (PmExprCon c []) = c == trueDataCon
+isTruePmExpr _other_expr      = False
+
+-- | Check whether a PmExpr is syntactically equal to term `False'.
+isFalsePmExpr :: PmExpr -> Bool
+isFalsePmExpr (PmExprCon c []) = c == falseDataCon
+isFalsePmExpr _other_expr      = False
+
+-- | Check whether a PmExpr is syntactically e
+isNilPmExpr :: PmExpr -> Bool
+isNilPmExpr (PmExprCon c _) = c == nilDataCon
+isNilPmExpr _other_expr     = False
+
+-- | Check whether a PmExpr is syntactically equal to (x == y).
+-- Since (==) is overloaded and can have an arbitrary implementation, we use
+-- the PmExprEq constructor to represent only equalities with non-overloaded
+-- literals where it coincides with a syntactic equality check.
+isPmExprEq :: PmExpr -> Maybe (PmExpr, PmExpr)
+isPmExprEq (PmExprEq e1 e2) = Just (e1,e2)
+isPmExprEq _other_expr      = Nothing
+
+-- | Check if a DataCon is (:).
+isConsDataCon :: DataCon -> Bool
+isConsDataCon con = consDataCon == con
+
+-- ----------------------------------------------------------------------------
+-- ** Substitution in PmExpr
+
+-- | 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 x e1 e =
+  case e of
+    PmExprVar z | x == z    -> (e1, True)
+                | otherwise -> (e, False)
+    PmExprCon c ps -> let (ps', bs) = mapAndUnzip (substPmExpr x e1) ps
+                      in  (PmExprCon c ps', or bs)
+    PmExprEq ex ey -> let (ex', bx) = substPmExpr x e1 ex
+                          (ey', by) = substPmExpr x e1 ey
+                      in  (PmExprEq ex' ey', bx || by)
+    _other_expr    -> (e, False) -- The rest are terminals (We silently ignore
+                                 -- Other). See Note [PmExprOther in PmExpr]
+
+-- | 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 x e (ex, ey)
+  | bx || by  = Left  (ex', ey')
+  | otherwise = Right (ex', ey')
+  where
+    (ex', bx) = substPmExpr x e ex
+    (ey', by) = substPmExpr x e ey
+
+-- -----------------------------------------------------------------------
+-- ** Lift source expressions (HsExpr Id) to PmExpr
+
+lhsExprToPmExpr :: LHsExpr Id -> PmExpr
+lhsExprToPmExpr (L _ e) = hsExprToPmExpr e
+
+hsExprToPmExpr :: HsExpr Id -> PmExpr
+
+hsExprToPmExpr (HsVar         x) = PmExprVar (unLoc x)
+hsExprToPmExpr (HsOverLit  olit) = PmExprLit (PmOLit False olit)
+hsExprToPmExpr (HsLit       lit) = PmExprLit (PmSLit lit)
+
+hsExprToPmExpr e@(NegApp _ neg_e)
+  | PmExprLit (PmOLit False ol) <- hsExprToPmExpr neg_e
+  = PmExprLit (PmOLit True ol)
+  | otherwise = PmExprOther e
+hsExprToPmExpr (HsPar (L _ e)) = hsExprToPmExpr e
+
+hsExprToPmExpr e@(ExplicitTuple ps boxity)
+  | all tupArgPresent ps = PmExprCon tuple_con tuple_args
+  | otherwise            = PmExprOther e
+  where
+    tuple_con  = tupleDataCon boxity (length ps)
+    tuple_args = [ lhsExprToPmExpr e | L _ (Present e) <- ps ]
+
+hsExprToPmExpr e@(ExplicitList _elem_ty mb_ol elems)
+  | Nothing <- mb_ol = foldr cons nil (map lhsExprToPmExpr elems)
+  | otherwise        = PmExprOther e {- overloaded list: No PmExprApp -}
+  where
+    cons x xs = PmExprCon consDataCon [x,xs]
+    nil       = PmExprCon nilDataCon  []
+
+hsExprToPmExpr (ExplicitPArr _elem_ty elems)
+  = PmExprCon (parrFakeCon (length elems)) (map lhsExprToPmExpr elems)
+
+-- we want this but we would have to make evrything monadic :/
+-- ./compiler/deSugar/DsMonad.hs:397:dsLookupDataCon :: Name -> DsM DataCon
+--
+-- hsExprToPmExpr (RecordCon   c _ binds) = do
+--   con  <- dsLookupDataCon (unLoc c)
+--   args <- mapM lhsExprToPmExpr (hsRecFieldsArgs binds)
+--   return (PmExprCon con args)
+hsExprToPmExpr e@(RecordCon   _ _ _ _) = PmExprOther e
+
+hsExprToPmExpr (HsTick            _ e) = lhsExprToPmExpr e
+hsExprToPmExpr (HsBinTick       _ _ e) = lhsExprToPmExpr e
+hsExprToPmExpr (HsTickPragma    _ _ e) = lhsExprToPmExpr e
+hsExprToPmExpr (HsSCC           _ _ e) = lhsExprToPmExpr e
+hsExprToPmExpr (HsCoreAnn       _ _ e) = lhsExprToPmExpr e
+hsExprToPmExpr (ExprWithTySig     e _) = lhsExprToPmExpr e
+hsExprToPmExpr (ExprWithTySigOut  e _) = lhsExprToPmExpr e
+hsExprToPmExpr (HsWrap            _ e) =  hsExprToPmExpr e
+hsExprToPmExpr e = PmExprOther e -- the rest are not handled by the oracle
+
+{-
+%************************************************************************
+%*                                                                      *
+                            Pretty printing
+%*                                                                      *
+%************************************************************************
+-}
+
+{- 1. Literals
+~~~~~~~~~~~~~~
+Starting with a function definition like:
+
+    f :: Int -> Bool
+    f 5 = True
+    f 6 = True
+
+The uncovered set looks like:
+    { var |> False == (var == 5), False == (var == 6) }
+
+Yet, we would like to print this nicely as follows:
+   x , where x not one of {5,6}
+
+Function `filterComplex' takes the set of residual constraints and packs
+together the negative constraints that refer to the same variable so we can do
+just this. Since these variables will be shown to the programmer, we also give
+them better names (t1, t2, ..), hence the SDoc in PmNegLitCt.
+
+2. Residual Constraints
+~~~~~~~~~~~~~~~~~~~~~~~
+Unhandled constraints that refer to HsExpr are typically ignored by the solver
+(it does not even substitute in HsExpr so they are even printed as wildcards).
+Additionally, the oracle returns a substitution if it succeeds so we apply this
+substitution to the vectors before printing them out (see function `pprOne' in
+Check.hs) to be more precice.
+-}
+
+-- -----------------------------------------------------------------------------
+-- ** Transform residual constraints in appropriate form for pretty printing
+
+type PmNegLitCt = (Id, (SDoc, [PmLit]))
+
+filterComplex :: [ComplexEq] -> [PmNegLitCt]
+filterComplex = zipWith rename nameList . map mkGroup
+              . groupBy name . sortBy order . mapMaybe isNegLitCs
+  where
+    order x y = compare (fst x) (fst y)
+    name  x y = fst x == fst y
+    mkGroup l = (fst (head l), nubPmLit $ map snd l)
+    rename new (old, lits) = (old, (new, lits))
+
+    isNegLitCs (e1,e2)
+      | isFalsePmExpr e1, Just (x,y) <- isPmExprEq e2 = isNegLitCs' x y
+      | isFalsePmExpr e2, Just (x,y) <- isPmExprEq e1 = isNegLitCs' x y
+      | otherwise = Nothing
+
+    isNegLitCs' (PmExprVar x) (PmExprLit l) = Just (x, l)
+    isNegLitCs' (PmExprLit l) (PmExprVar x) = Just (x, l)
+    isNegLitCs' _ _             = Nothing
+
+    -- Try nice names p,q,r,s,t before using the (ugly) t_i
+    nameList :: [SDoc]
+    nameList = map (ptext . sLit) ["p","q","r","s","t"] ++
+                 [ ptext (sLit ('t':show u)) | u <- [(0 :: Int)..] ]
+
+-- ----------------------------------------------------------------------------
+
+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)
+
+    is_used (x,(name, lits))
+      | elemVarSet x used = Just (name, lits)
+      | otherwise         = Nothing
+
+type PmPprM a = State ([PmNegLitCt], IdSet) 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))
+
+checkNegation :: Id -> PmPprM (Maybe SDoc) -- the clean name if it is negated
+checkNegation x = do
+  negated <- gets fst
+  return $ case lookup x negated of
+    Just (new, _) -> Just new
+    Nothing       -> Nothing
+
+-- | Pretty print a pmexpr, but remember to prettify the names of the variables
+-- that refer to neg-literals. The ones that cannot be shown are printed as
+-- underscores.
+pprPmExpr :: PmExpr -> PmPprM SDoc
+pprPmExpr (PmExprVar x) = do
+  mb_name <- checkNegation x
+  case mb_name of
+    Just name -> addUsed x >> return name
+    Nothing   -> return underscore
+
+pprPmExpr (PmExprCon con args) = pprPmExprCon con args
+pprPmExpr (PmExprLit l)        = return (ppr l)
+pprPmExpr (PmExprEq _ _)       = return underscore -- don't show
+pprPmExpr (PmExprOther _)      = return underscore -- don't show
+
+needsParens :: PmExpr -> Bool
+needsParens (PmExprVar   {}) = False
+needsParens (PmExprLit    l) = isNegatedPmLit l
+needsParens (PmExprEq    {}) = False -- will become a wildcard
+needsParens (PmExprOther {}) = False -- will become a wildcard
+needsParens (PmExprCon c es)
+  | isTupleDataCon c || isPArrFakeCon c
+  || isConsDataCon c || null es = False
+  | otherwise                   = True
+
+pprPmExprWithParens :: PmExpr -> PmPprM SDoc
+pprPmExprWithParens expr
+  | needsParens expr = parens <$> pprPmExpr expr
+  | otherwise        =            pprPmExpr expr
+
+pprPmExprCon :: DataCon -> [PmExpr] -> PmPprM SDoc
+pprPmExprCon con args
+  | isTupleDataCon con = mkTuple <$> mapM pprPmExpr args
+  |  isPArrFakeCon con = mkPArr  <$> mapM pprPmExpr args
+  |  isConsDataCon con = pretty_list
+  | dataConIsInfix con = case args of
+      [x, y] -> do x' <- pprPmExprWithParens x
+                   y' <- pprPmExprWithParens y
+                   return (x' <+> ppr con <+> y')
+      -- can it be infix but have more than two arguments?
+      list   -> pprPanic "pprPmExprCon:" (ppr list)
+  | null args = return (ppr con)
+  | otherwise = do args' <- mapM pprPmExprWithParens args
+                   return (fsep (ppr con : args'))
+  where
+    mkTuple, mkPArr :: [SDoc] -> SDoc
+    mkTuple = parens     . fsep . punctuate comma
+    mkPArr  = paBrackets . fsep . punctuate comma
+
+    -- lazily, to be used in the list case only
+    pretty_list :: PmPprM SDoc
+    pretty_list = case isNilPmExpr (last list) of
+      True  -> brackets . fsep . punctuate comma <$> mapM pprPmExpr (init list)
+      False -> parens   . hcat . punctuate colon <$> mapM pprPmExpr list
+
+    list = list_elements args
+
+    list_elements [x,y]
+      | PmExprCon c es <- y,  nilDataCon == c = ASSERT (null es) [x,y]
+      | PmExprCon c es <- y, consDataCon == c = x : list_elements es
+      | otherwise = [x,y]
+    list_elements list  = pprPanic "list_elements:" (ppr list)
+
+instance Outputable PmLit where
+  ppr (PmSLit     l) = pmPprHsLit l
+  ppr (PmOLit neg l) = (if neg then char '-' else empty) <> ppr l
+
+-- not really useful for pmexprs per se
+instance Outputable PmExpr where
+  ppr e = fst $ runPmPprM (pprPmExpr e) []
+
diff --git a/compiler/deSugar/TmOracle.hs b/compiler/deSugar/TmOracle.hs
new file mode 100644
index 0000000000..8babc2ebdc
--- /dev/null
+++ b/compiler/deSugar/TmOracle.hs
@@ -0,0 +1,455 @@
+{-
+Author: George Karachalias <george.karachalias@cs.kuleuven.be>
+
+The term equality oracle. The main export of the module is function `tmOracle'.
+-}
+
+{-# LANGUAGE CPP, MultiWayIf #-}
+
+module TmOracle (
+
+        -- re-exported from PmExpr
+        PmExpr(..), PmLit(..), SimpleEq, ComplexEq, PmVarEnv, falsePmExpr,
+        canDiverge, eqPmLit, filterComplex, isNotPmExprOther, runPmPprM,
+        pprPmExprWithParens, lhsExprToPmExpr, hsExprToPmExpr,
+
+        -- the term oracle
+        tmOracle, TmState, initialTmState, containsEqLits,
+
+        -- misc.
+        exprDeepLookup, pmLitType, flattenPmVarEnv
+    ) where
+
+#include "HsVersions.h"
+
+import PmExpr
+
+import Id
+import TysWiredIn
+import Type
+import HsLit
+import TcHsSyn
+import MonadUtils
+import Util
+
+import Data.Maybe (isJust)
+import qualified Data.Map as Map
+
+{-
+%************************************************************************
+%*                                                                      *
+                      The term equality oracle
+%*                                                                      *
+%************************************************************************
+-}
+
+-- | The type of substitutions.
+type PmVarEnv = Map.Map Id PmExpr
+
+-- | The environment of the oracle contains
+--     1. A Bool (are there any constraints we cannot handle? (PmExprOther)).
+--     2. A substitution we extend with every step and return as a result.
+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 x (standby, (_unhandled, env))
+  -- If the variable seems not evaluated, there is a possibility for
+  -- constraint x ~ BOT to be satisfiable.
+  | PmExprVar y <- varDeepLookup env x -- seems not forced
+  -- If it is involved (directly or indirectly) in any equality in the
+  -- worklist, we can assume that it is already indirectly evaluated,
+  -- as a side-effect of equality checking. If not, then we can assume
+  -- that the constraint is satisfiable.
+  = not $ any (isForcedByEq x) standby || any (isForcedByEq y) standby
+  -- Variable x is already in WHNF so the constraint is non-satisfiable
+  | otherwise = False
+
+  where
+    isForcedByEq :: Id -> 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 x e = case e of
+  PmExprVar y    -> x == y
+  PmExprCon _ es -> any (x `varIn`) es
+  PmExprLit _    -> False
+  PmExprEq e1 e2 -> (x `varIn` e1) || (x `varIn` e2)
+  PmExprOther _  -> False
+
+-- | Flatten the DAG (Could be improved in terms of performance.).
+flattenPmVarEnv :: PmVarEnv -> PmVarEnv
+flattenPmVarEnv env = Map.map (exprDeepLookup env) env
+
+-- | The state of the term oracle (includes complex constraints that cannot
+-- progress unless we get more information).
+type TmState = ([ComplexEq], TmOracleEnv)
+
+-- | Initial state of the oracle.
+initialTmState :: TmState
+initialTmState = ([], (False, Map.empty))
+
+-- | Solve a simple equality.
+solveSimpleEq :: TmState -> SimpleEq -> Maybe TmState
+solveSimpleEq solver_env@(_,(_,env)) simple
+  = solveComplexEq solver_env -- do the actual *merging* with existing state
+  $ simplifyComplexEq             -- simplify as much as you can
+  $ applySubstSimpleEq env simple -- replace everything we already know
+
+-- | Solve a complex equality.
+solveComplexEq :: TmState -> ComplexEq -> Maybe TmState
+solveComplexEq solver_state@(standby, (unhandled, env)) eq@(e1, e2) = case eq of
+  -- We cannot do a thing about these cases
+  (PmExprOther _,_)            -> Just (standby, (True, env))
+  (_,PmExprOther _)            -> Just (standby, (True, env))
+
+  (PmExprLit l1, PmExprLit l2) -> case eqPmLit l1 l2 of
+    Just True  -> Just solver_state           -- we are sure: equal
+    Just False -> Nothing                     -- we are sure: not equal
+    Nothing    -> Just (eq:standby, (unhandled, env)) -- no clue
+
+  (PmExprCon c1 ts1, PmExprCon c2 ts2)
+    | c1 == c2  -> foldlM solveComplexEq solver_state (zip ts1 ts2)
+    | otherwise -> Nothing
+  (PmExprCon c [], PmExprEq t1 t2)
+    | c == trueDataCon  -> solveComplexEq solver_state (t1, t2)
+    | c == falseDataCon -> Just (eq:standby, (unhandled, env))
+  (PmExprEq t1 t2, PmExprCon c [])
+    | c == trueDataCon  -> solveComplexEq solver_state (t1, t2)
+    | c == falseDataCon -> Just (eq:standby, (unhandled, env))
+
+  (PmExprVar x, PmExprVar y)
+    | x == y    -> Just solver_state
+    | otherwise -> extendSubstAndSolve x e2 solver_state
+
+  (PmExprVar x, _) -> extendSubstAndSolve x e2 solver_state
+  (_, PmExprVar x) -> extendSubstAndSolve x e1 solver_state
+
+  (PmExprEq _ _, PmExprEq _ _) -> Just (eq:standby, (unhandled, env))
+
+  _ -> Just (standby, (True, env)) -- I HATE CATCH-ALLS
+
+-- | Extend the substitution and solve the (possibly updated) constraints.
+extendSubstAndSolve :: Id -> PmExpr -> TmState -> Maybe TmState
+extendSubstAndSolve x e (standby, (unhandled, env))
+  = foldlM solveComplexEq new_incr_state (map simplifyComplexEq changed)
+  where
+    -- Apply the substitution to the worklist and partition them to the ones
+    -- that had some progress and the rest. Then, recurse over the ones that
+    -- had some progress.
+    (changed, unchanged) = partitionWith (substComplexEq x e) standby
+    new_incr_state       = (unchanged, (unhandled, Map.insert x e env))
+
+-- | Simplify a complex equality.
+simplifyComplexEq :: ComplexEq -> ComplexEq
+simplifyComplexEq (e1, e2) = (fst $ simplifyPmExpr e1, fst $ simplifyPmExpr e2)
+
+-- | Simplify an expression. The boolean indicates if there has been any
+-- simplification or if the operation was a no-op.
+simplifyPmExpr :: PmExpr -> (PmExpr, Bool)
+-- See Note [Deep equalities]
+simplifyPmExpr e = case e of
+  PmExprCon c ts -> case mapAndUnzip simplifyPmExpr ts of
+                      (ts', bs) -> (PmExprCon c ts', or bs)
+  PmExprEq t1 t2 -> simplifyEqExpr t1 t2
+  _other_expr    -> (e, False) -- the others are terminals
+
+-- | Simplify an equality expression. The equality is given in parts.
+simplifyEqExpr :: PmExpr -> PmExpr -> (PmExpr, Bool)
+-- See Note [Deep equalities]
+simplifyEqExpr e1 e2 = case (e1, e2) of
+  -- Varables
+  (PmExprVar x, PmExprVar y)
+    | x == y -> (truePmExpr, True)
+
+  -- Literals
+  (PmExprLit l1, PmExprLit l2) -> case eqPmLit l1 l2 of
+    Just True  -> (truePmExpr,  True)
+    Just False -> (falsePmExpr, True)
+    Nothing    -> (original,   False)
+
+  -- Can potentially be simplified
+  (PmExprEq {}, _) -> case (simplifyPmExpr e1, simplifyPmExpr e2) of
+    ((e1', True ), (e2', _    )) -> simplifyEqExpr e1' e2'
+    ((e1', _    ), (e2', True )) -> simplifyEqExpr e1' e2'
+    ((e1', False), (e2', False)) -> (PmExprEq e1' e2', False) -- cannot progress
+  (_, PmExprEq {}) -> case (simplifyPmExpr e1, simplifyPmExpr e2) of
+    ((e1', True ), (e2', _    )) -> simplifyEqExpr e1' e2'
+    ((e1', _    ), (e2', True )) -> simplifyEqExpr e1' e2'
+    ((e1', False), (e2', False)) -> (PmExprEq e1' e2', False) -- cannot progress
+
+  -- Constructors
+  (PmExprCon c1 ts1, PmExprCon c2 ts2)
+    | c1 == c2 ->
+        let (ts1', bs1) = mapAndUnzip simplifyPmExpr ts1
+            (ts2', bs2) = mapAndUnzip simplifyPmExpr ts2
+            (tss, _bss) = zipWithAndUnzip simplifyEqExpr ts1' ts2'
+            worst_case  = PmExprEq (PmExprCon c1 ts1') (PmExprCon c2 ts2')
+        in  if | not (or bs1 || or bs2) -> (worst_case, False) -- no progress
+               | all isTruePmExpr  tss  -> (truePmExpr, True)
+               | any isFalsePmExpr tss  -> (falsePmExpr, True)
+               | otherwise              -> (worst_case, False)
+    | otherwise -> (falsePmExpr, True)
+
+  -- We cannot do anything about the rest..
+  _other_equality -> (original, False)
+
+  where
+    original = PmExprEq e1 e2 -- reconstruct equality
+
+-- | Apply an (un-flattened) substitution on a simple equality.
+applySubstSimpleEq :: PmVarEnv -> SimpleEq -> ComplexEq
+applySubstSimpleEq env (x, e) = (varDeepLookup env x, exprDeepLookup env e)
+
+-- | Apply an (un-flattened) substitution on a variable.
+varDeepLookup :: PmVarEnv -> Id -> PmExpr
+varDeepLookup env x
+  | Just e <- Map.lookup x env = exprDeepLookup env e -- go deeper
+  | otherwise                  = PmExprVar x          -- terminal
+{-# INLINE varDeepLookup #-}
+
+-- | Apply an (un-flattened) substitution on an expression.
+exprDeepLookup :: PmVarEnv -> PmExpr -> PmExpr
+exprDeepLookup env (PmExprVar x)    = varDeepLookup env x
+exprDeepLookup env (PmExprCon c es) = PmExprCon c (map (exprDeepLookup env) es)
+exprDeepLookup env (PmExprEq e1 e2) = PmExprEq (exprDeepLookup env e1)
+                                               (exprDeepLookup env e2)
+exprDeepLookup _   other_expr       = other_expr -- PmExprLit, PmExprOther
+
+-- | External interface to the term oracle.
+tmOracle :: TmState -> [SimpleEq] -> Maybe TmState
+tmOracle tm_state eqs = foldlM solveSimpleEq tm_state eqs
+
+-- | Type of a PmLit
+pmLitType :: PmLit -> Type -- should be in PmExpr but gives cyclic imports :(
+pmLitType (PmSLit   lit) = hsLitType   lit
+pmLitType (PmOLit _ lit) = overLitType lit
+
+{- Note [Deep equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+Solving nested equalities is the most difficult part. The general strategy
+is the following:
+
+  * Equalities of the form (True ~ (e1 ~ e2)) are transformed to just
+    (e1 ~ e2) and then treated recursively.
+
+  * Equalities of the form (False ~ (e1 ~ e2)) cannot be analyzed unless
+    we know more about the inner equality (e1 ~ e2). That's exactly what
+    `simplifyEqExpr' tries to do: It takes e1 and e2 and either returns
+    truePmExpr, falsePmExpr or (e1' ~ e2') in case it is uncertain. Note
+    that it is not e but rather e', since it may perform some
+    simplifications deeper.
+
+Note [Undecidable Equality on Overloaded Literals]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Overloaded literals do not offer equality like constructors do. A literal @lit@
+is used to actually represent @from lit@. For example, we can have the
+following:
+
+  instance Num Bool where
+    ...
+    fromInteger 0 = False
+    fromInteger _ = True
+
+  g :: Bool -> Bool
+  g 4 = ...          -- clause A
+  g 2 = ...          -- clause B
+
+Both clauses A and B will match argunent @True@ so we have an overlap. Yet, we
+cannot detect this unless we unfold the @fromInteger@ function. So @eqPmLit@
+from deSugar/PmExpr.hs returns @Nothing@ in this case. This complexes things a
+lot. Consider the following (similar to test ds022 in deSugar/should_compile):
+
+  f l1 l2 = ...      -- clause A
+  f l3 l4 = ...      -- clause B
+  f l1 l2 = ...      -- clause C
+
+Assuming that the @from@ function is side-effect-free (and total), clauses C
+and D are redundant, independently of the implementation of @from@:
+
+  l1 == l2     ===>    from l1 == from l2
+  l1 /= l2     =/=>    from l1 /= from l2
+
+Now consider what we should generate for @f@ (covered and uncovered only):
+
+U0 = { [x y |> {}] }
+
+Clause A: l1 l2
+-------------------------------------------------------------------------------
+CA = { [l1 l2 |> { x ~ l1, y ~ l2 }] }
+
+UA = { [x  y  |> { False ~ (x ~ l1) }]
+     , [l1 y  |> { x ~ l1, False ~ (y ~ l2) }] }
+
+Clause B: l3 l4
+-------------------------------------------------------------------------------
+
+CB = { [l3 l4 |> { False ~ (x ~ l1), x ~ l3, y ~ l4}]
+         ..reduces to: False ~ (l3 ~ l1), y ~ l4
+
+     , [l1 l4 |> { x ~ l1, False ~ (y ~ l2), l3 ~ z, z ~ l1, y ~ l4}] }
+         ..reduces to: x ~ l1, False ~ (l4 ~ l2), l1 ~ l3
+
+UB = { [x  y  |> { False ~ (x ~ l1), False ~ (x ~ l3) }]
+     , [l3 y  |> { False ~ (x ~ l1), x ~ l3, False ~ (y ~ l4) }]
+         ..reduces to: False ~ (l1 ~ l3), False ~ (y ~ l4)
+     , [l1 y  |> { x ~ l1, False ~ (y ~ l2), False ~ (l1 ~ l3) }]
+     , [l1 y  |> { x ~ l1, False ~ (y ~ l2), l1 ~ l3, False ~ (y ~ l4) }] }
+
+Clause C: l1 l2
+-------------------------------------------------------------------------------
+
+CC = { [l1 l2 |> { False ~ (x ~ l1), False ~ (x ~ l3), x ~ l1, y ~ l2 }]
+         ..reduces to: False ~ (l1 ~ l1), False ~ (l1 ~ l3), x ~ l1
+                       False ~ True, False ~ (l1 ~ l3), x ~ l1
+                       INCONSISTENT
+     , [l3 l2 |> { False ~ (l1 ~ l3), False ~ (y ~ l4), l1 ~ l3, y ~ l2 }]
+         ..reduces to: False ~ (l1 ~ l3), False ~ (l2 ~ l4), l1 ~ l3
+     , [l1 l2 |> { x ~ l1, False ~ (y ~ l2), False ~ (l1 ~ l3), y ~ l2 }]
+         ..reduces to: x ~ l1, False ~ (l2 ~ l2), False ~ (l1 ~ l3)
+                       x ~ l1, False ~ True, False ~ (l1 ~ l3)
+                       INCONSISTENT
+     , [l1 l2 |> { x ~ l1,False ~ (y ~ l2),l1 ~ l3,False ~ (y ~ l4),y ~ l2 }] }
+         ..reduces to: x ~ l1, False ~ (l2 ~ l2), l1 ~ l3, False ~ (l2 ~ l4)
+                       x ~ l1, False ~ True, l1 ~ l3, False ~ (l2 ~ l4)
+                       INCONSISTENT
+-------------------------------------------------------------------------------
+
+PROBLEM 1:
+~~~~~~~~~~
+Now the first problem shows itself: Our basic unification-based term oracle
+cannot detect that constraint:
+
+    False ~ (l1 ~ l3), False ~ (l2 ~ l4), l1 ~ l3
+
+is inconsistent. That's what function @tryLitEqs@ (in comments) tries to do:
+use the equality l1 ~ l3 to replace False ~ (l1 ~ l3) with False ~ (l1 ~ l1)
+and expose the inconsistency.
+
+PROBLEM 2:
+~~~~~~~~~~
+Let's turn back to UB and assume we had only clauses A and B. UB is as follows:
+
+  UB = { [x  y  |> { False ~ (x ~ l1), False ~ (x ~ l3) }]
+       , [l3 y  |> { False ~ (l1 ~ l3), False ~ (y ~ l4) }]
+       , [l1 y  |> { x ~ l1, False ~ (y ~ l2), False ~ (l1 ~ l3) }]
+       , [l1 y  |> { x ~ l1, False ~ (y ~ l2), l1 ~ l3, False ~ (y ~ l4) }] }
+
+So we would get:
+
+    Pattern match(es) are non-exhaustive
+    In an equation for f:
+        Patterns not matched:
+          x y    where x not one of {l1, l3}
+          l3 y   where y not one of {l4}
+          l1 y   where y not one of {l2}
+          l1 y   where y not one of {l2, l4} -- (*)
+
+What about the last warning? It holds UNDER THE ASSUMPTION that l1 == l2. It is
+quite unintuitive for the user so at the moment we drop such cases (see
+function @pruneVSABound@ in deSugar/Check.hs). I (gkaracha) would prefer to
+issue a warning like:
+
+    Pattern match(es) are non-exhaustive
+    In an equation for f:
+        Patterns not matched:
+          ...
+          l1 y   where y not one of {l2, l4}
+                 under the assumption that l1 ~ l3
+
+It may be more complex but I would prefer to play on the safe side and (safely)
+issue all warnings and leave it up to the user to decide whether the assumption
+holds or not.
+
+At the moment, we use @containsEqLits@ and consider all constraints that
+include literal equalities inconsistent. We could achieve the same by replacing
+this clause of @eqPmLit@:
+
+  eqPmLit (PmOLit b1 l1) (PmOLit b2 l2)
+    | b1 == b2 && l1 == l2 = Just True
+    | otherwise            = Nothing
+
+with this:
+
+  eqPmLit (PmOLit b1 l1) (PmOLit b2 l2)
+    | b1 == b2 && l1 == l2 = Just True
+    | otherwise            = Just False
+
+which approximates on the unsafe side. Hopefully, literals always need a
+catch-all case to be considered exhaustive so in practice it makes small
+difference. I hate this but it gives the warnings the users are used to.
+-}
+
+{- Not Enabled at the moment
+
+-- | Check whether overloaded literal constraints exist in the state and if
+-- they can be used to detect further inconsistencies.
+tryLitEqs :: TmState -> Maybe Bool
+tryLitEqs tm_state@(stb,_) = do
+  ans <- exploitLitEqs (Just tm_state)
+  -- Three possible results:
+  --   Nothing    : Inconsistency found.
+  --   Just True  : Literal constraints exist but no inconsistency found.
+  --   Just False : There are no literal constraints in the state.
+  return (isJust $ exists isLitEq_mb stb)
+
+-- | Exploit overloaded literal constraints
+-- @lit1 ~ lit2@ to improve the term oracle's expressivity.
+exploitLitEqs :: Maybe TmState -> Maybe TmState
+exploitLitEqs tm_state = case tm_state of
+  -- The oracle did not find any inconsistency. Try and exploit
+  -- residual literal equalities for a more precise result.
+  Just st@(standby, (unhandled, env)) ->
+    case exists isLitEq_mb standby of
+      -- Such an equality exists. This means that we are under the assumption
+      -- that two overloaded literals reduce to the same value (for all we know
+      -- they do). Replace the one with the other in the rest residual
+      -- constraints and run the solver once more, looking for an inconsistency.
+      Just ((l1, l2), rest) ->
+        let new_env = Map.map (replaceLit l1 l2) env
+            new_stb = map (replaceLitSimplifyComplexEq l1 l2) rest
+        in  exploitLitEqs
+              (foldlM solveComplexEq ([], (unhandled, new_env)) new_stb)
+      -- We don't have anything. Just return what you had..
+      Nothing -> Just st
+  -- The oracle has already found an inconsistency.
+  -- No need to search further.
+  Nothing -> Nothing
+  where
+    replaceLitSimplifyComplexEq :: PmLit -> PmLit -> ComplexEq -> ComplexEq
+    replaceLitSimplifyComplexEq l1 l2 (e1,e2) =
+      simplifyComplexEq (replaceLit l1 l2 e1, replaceLit l1 l2 e2)
+
+-- | Replace a literal with another in an expression
+-- See Note [Undecidable Equality on Overloaded Literals]
+replaceLit :: PmLit -> PmLit -> PmExpr -> PmExpr
+replaceLit l1 l2 e = case e of
+  PmExprVar {}   -> e
+  PmExprCon c es -> PmExprCon c (map (replaceLit l1 l2) es)
+  PmExprLit l    -> case eqPmLit l l1 of
+                      Just True  -> PmExprLit l2
+                      Just False -> e
+                      Nothing    -> e
+  PmExprEq e1 e2 -> PmExprEq (replaceLit l1 l2 e1) (replaceLit l1 l2 e2)
+  PmExprOther {} -> e -- do nothing
+-}
+
+-- | Check whether the term oracle state
+-- contains any equalities between literals.
+containsEqLits :: TmState -> Bool
+containsEqLits (stb, _) = isJust (exists isLitEq_mb stb)
+
+exists :: (a -> Maybe b) -> [a] -> Maybe (b, [a])
+exists _ []     = Nothing
+exists p (x:xs) = case p x of
+  Just y  -> Just (y, xs)
+  Nothing -> do
+    (y, ys) <- exists p xs
+    return (y, x:ys)
+
+-- | Check whether a complex equality refers to literals only
+isLitEq_mb :: ComplexEq -> Maybe (PmLit, PmLit)
+isLitEq_mb (PmExprLit l1, PmExprLit l2) = Just (l1, l2)
+isLitEq_mb _other_eq                    = Nothing
diff --git a/compiler/ghc.cabal.in b/compiler/ghc.cabal.in
index 9ea5b66e90..1710321fd4 100644
--- a/compiler/ghc.cabal.in
+++ b/compiler/ghc.cabal.in
@@ -266,6 +266,8 @@ Library
         CoreStats
         MkCore
         PprCore
+        PmExpr
+        TmOracle
         Check
         Coverage
         Desugar
diff --git a/compiler/ghc.mk b/compiler/ghc.mk
index eb6292d5f7..bcf45281ac 100644
--- a/compiler/ghc.mk
+++ b/compiler/ghc.mk
@@ -536,6 +536,7 @@ compiler_stage2_dll0_MODULES = \
 	HsImpExp \
 	HsLit \
 	PlaceHolder \
+	PmExpr \
 	HsPat \
 	HsSyn \
 	HsTypes \
diff --git a/compiler/hsSyn/HsLit.hs b/compiler/hsSyn/HsLit.hs
index a53c67c103..e890b3bd93 100644
--- a/compiler/hsSyn/HsLit.hs
+++ b/compiler/hsSyn/HsLit.hs
@@ -174,3 +174,25 @@ instance Outputable OverLitVal where
   ppr (HsIntegral _ i)   = integer i
   ppr (HsFractional f)   = ppr f
   ppr (HsIsString _ s)   = pprHsString s
+
+-- | pmPprHsLit pretty prints literals and is used when pretty printing pattern
+-- match warnings. All are printed the same (i.e., without hashes if they are
+-- primitive and not wrapped in constructors if they are boxed). This happens
+-- mainly for too reasons:
+--  * We do not want to expose their internal representation
+--  * The warnings become too messy
+pmPprHsLit :: HsLit -> SDoc
+pmPprHsLit (HsChar _ c)       = pprHsChar c
+pmPprHsLit (HsCharPrim _ c)   = pprHsChar c
+pmPprHsLit (HsString _ s)     = pprHsString s
+pmPprHsLit (HsStringPrim _ s) = pprHsBytes s
+pmPprHsLit (HsInt _ i)        = integer i
+pmPprHsLit (HsIntPrim _ i)    = integer i
+pmPprHsLit (HsWordPrim _ w)   = integer w
+pmPprHsLit (HsInt64Prim _ i)  = integer i
+pmPprHsLit (HsWord64Prim _ w) = integer w
+pmPprHsLit (HsInteger _ i _)  = integer i
+pmPprHsLit (HsRat f _)        = ppr f
+pmPprHsLit (HsFloatPrim f)    = ppr f
+pmPprHsLit (HsDoublePrim d)   = ppr d
+
diff --git a/compiler/hsSyn/HsPat.hs b/compiler/hsSyn/HsPat.hs
index 359990a66a..91e5973ece 100644
--- a/compiler/hsSyn/HsPat.hs
+++ b/compiler/hsSyn/HsPat.hs
@@ -22,7 +22,7 @@ module HsPat (
         HsRecFields(..), HsRecField'(..), LHsRecField',
         HsRecField, LHsRecField,
         HsRecUpdField, LHsRecUpdField,
-        hsRecFields, hsRecFieldSel, hsRecFieldId,
+        hsRecFields, hsRecFieldSel, hsRecFieldId, hsRecFieldsArgs,
         hsRecUpdFieldId, hsRecUpdFieldOcc, hsRecUpdFieldRdr,
 
         mkPrefixConPat, mkCharLitPat, mkNilPat,
@@ -32,6 +32,8 @@ module HsPat (
         hsPatNeedsParens,
         isIrrefutableHsPat,
 
+        collectEvVarsPats,
+
         pprParendLPat, pprConArgs
     ) where
 
@@ -56,6 +58,7 @@ import Outputable
 import Type
 import SrcLoc
 import FastString
+import Bag -- collect ev vars from pats
 import Maybes
 -- libraries:
 import Data.Data hiding (TyCon,Fixity)
@@ -334,6 +337,10 @@ data HsRecField' id arg = HsRecField {
 hsRecFields :: HsRecFields id arg -> [PostRn id id]
 hsRecFields rbinds = map (unLoc . hsRecFieldSel . unLoc) (rec_flds rbinds)
 
+-- Probably won't typecheck at once, things have changed :/
+hsRecFieldsArgs :: HsRecFields id arg -> [arg]
+hsRecFieldsArgs rbinds = map (hsRecFieldArg . unLoc) (rec_flds rbinds)
+
 hsRecFieldSel :: HsRecField name arg -> Located (PostRn name name)
 hsRecFieldSel = fmap selectorFieldOcc . hsRecFieldLbl
 
@@ -610,3 +617,35 @@ conPatNeedsParens :: HsConDetails a b -> Bool
 conPatNeedsParens (PrefixCon args) = not (null args)
 conPatNeedsParens (InfixCon {})    = True
 conPatNeedsParens (RecCon {})      = True
+
+{-
+% Collect all EvVars from all constructor patterns
+-}
+
+-- May need to add more cases
+collectEvVarsPats :: [Pat id] -> Bag EvVar
+collectEvVarsPats = unionManyBags . map collectEvVarsPat
+
+collectEvVarsLPat :: LPat id -> Bag EvVar
+collectEvVarsLPat (L _ pat) = collectEvVarsPat pat
+
+collectEvVarsPat :: Pat id -> Bag EvVar
+collectEvVarsPat pat =
+  case pat of
+    LazyPat  p        -> collectEvVarsLPat p
+    AsPat _  p        -> collectEvVarsLPat p
+    ParPat   p        -> collectEvVarsLPat p
+    BangPat  p        -> collectEvVarsLPat p
+    ListPat  ps _ _   -> unionManyBags $ map collectEvVarsLPat ps
+    TuplePat ps _ _   -> unionManyBags $ map collectEvVarsLPat ps
+    PArrPat  ps _     -> unionManyBags $ map collectEvVarsLPat ps
+    ConPatOut {pat_dicts = dicts, pat_args  = args}
+                      -> unionBags (listToBag dicts)
+                                   $ unionManyBags
+                                   $ map collectEvVarsLPat
+                                   $ hsConPatArgs args
+    SigPatOut p _     -> collectEvVarsLPat p
+    CoPat _ p _       -> collectEvVarsPat  p
+    ConPatIn _  _     -> panic "foldMapPatBag: ConPatIn"
+    SigPatIn _ _      -> panic "foldMapPatBag: SigPatIn"
+    _other_pat        -> emptyBag
diff --git a/compiler/prelude/TysWiredIn.hs-boot b/compiler/prelude/TysWiredIn.hs-boot
index 309dfa22e1..a001338087 100644
--- a/compiler/prelude/TysWiredIn.hs-boot
+++ b/compiler/prelude/TysWiredIn.hs-boot
@@ -4,6 +4,6 @@ import {-# SOURCE #-} TyCon      (TyCon)
 import {-# SOURCE #-} TypeRep    (Type)
 
 
-eqTyCon, coercibleTyCon :: TyCon
+eqTyCon, listTyCon, coercibleTyCon :: TyCon
 typeNatKind, typeSymbolKind :: Type
 mkBoxedTupleTy :: [Type] -> Type
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index fb334eed34..ea8a11353e 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -28,6 +28,10 @@ module TcMType (
   newMetaDetails, isFilledMetaTyVar, isUnfilledMetaTyVar,
 
   --------------------------------
+  -- Creating fresh type variables for pm checking
+  genInstSkolTyVarsX,
+
+  --------------------------------
   -- Creating new evidence variables
   newEvVar, newEvVars, newEq, newDict,
   newTcEvBinds, addTcEvBind,
@@ -427,6 +431,17 @@ writeMetaTyVarRef tyvar ref ty
     ty_kind = typeKind ty
 
 {-
+% Generating fresh variables for pattern match check
+-}
+
+-- UNINSTANTIATED VERSION OF tcInstSkolTyVars
+genInstSkolTyVarsX :: SrcSpan -> TvSubst -> [TyVar] -> TcRnIf gbl lcl (TvSubst, [TcTyVar])
+-- Precondition: tyvars should be ordered (kind vars first)
+-- see Note [Kind substitution when instantiating]
+-- Get the location from the monad; this is a complete freshening operation
+genInstSkolTyVarsX loc subst tvs = instSkolTyVarsX (mkTcSkolTyVar loc False) subst tvs
+
+{-
 ************************************************************************
 *                                                                      *
         MetaTvs: TauTvs
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 82bf1be007..f66399dd11 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -131,6 +131,7 @@ import TcType
 import Annotations
 import InstEnv
 import FamInstEnv
+import PmExpr
 import IOEnv
 import RdrName
 import Name
@@ -317,7 +318,9 @@ instance ContainsModule DsGblEnv where
 
 data DsLclEnv = DsLclEnv {
         dsl_meta    :: DsMetaEnv,        -- Template Haskell bindings
-        dsl_loc     :: SrcSpan           -- to put in pattern-matching error msgs
+        dsl_loc     :: RealSrcSpan,      -- To put in pattern-matching error msgs
+        dsl_dicts   :: Bag EvVar,        -- Constraints from GADT pattern-matching
+        dsl_tm_cs   :: Bag SimpleEq
      }
 
 -- Inside [| |] brackets, the desugarer looks
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 4a4d7667d8..8ddb488504 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -1917,7 +1917,6 @@ lookupSolvedDict (IS { inert_solved_dicts = solved }) cls tys
       Just ev -> Just ev
       _       -> Nothing
 
-
 {- *********************************************************************
 *                                                                      *
                    Irreds
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index b8e193b0bf..fae58ade35 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -7,6 +7,7 @@ module TcSimplify(
        simplifyDefault,
        simplifyTop, simplifyInteractive,
        solveWantedsTcM,
+       tcCheckSatisfiability,
 
        -- For Rules we need these two
        solveWanteds, runTcS
@@ -360,6 +361,19 @@ simplifyDefault theta
 
        ; return () }
 
+------------------
+tcCheckSatisfiability :: Bag EvVar -> TcM Bool
+-- Return True if satisfiable, False if definitely contradictory
+tcCheckSatisfiability givens
+  = do { lcl_env <- TcRn.getLclEnv
+       ; let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env
+       ; traceTc "checkSatisfiabilty {" (ppr givens)
+       ; (res, _ev_binds) <- runTcS $
+             do { cts <- solveSimpleGivens given_loc (bagToList givens)
+                ; return (not (isEmptyBag cts)) }
+       ; traceTc "checkSatisfiabilty }" (ppr res)
+       ; return (not res) }
+
 {-
 *********************************************************************************
 *                                                                                 *
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 4e48d9f65e..60ab685418 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -148,6 +148,12 @@ module TcType (
   tyVarsOfTypeDSet, tyVarsOfTypesDSet, closeOverKindsDSet,
   tcTyVarsOfType, tcTyVarsOfTypes,
 
+  --------------------------------
+  -- Transforming Types to TcTypes
+  toTcType,    -- :: Type -> TcType
+  toTcTyVar,   -- :: TyVar -> TcTyVar
+  toTcTypeBag, -- :: Bag EvVar -> Bag EvVar
+
   pprKind, pprParendKind, pprSigmaType,
   pprType, pprParendType, pprTypeApp, pprTyThingCategory,
   pprTheta, pprThetaArrowTy, pprClassPred,
@@ -181,6 +187,7 @@ import PrelNames
 import TysWiredIn
 import BasicTypes
 import Util
+import Bag
 import Maybes
 import ListSetOps
 import Outputable
@@ -1545,6 +1552,41 @@ isRigidEqPred _ _ = False  -- Not an equality
 {-
 ************************************************************************
 *                                                                      *
+\subsection{Transformation of Types to TcTypes}
+*                                                                      *
+************************************************************************
+-}
+
+toTcType :: Type -> TcType
+toTcType ty = to_tc_type emptyVarSet ty
+   where
+    to_tc_type :: VarSet -> Type -> TcType
+    -- The constraint solver expects EvVars to have TcType, in which the
+    -- free type variables are TcTyVars. So we convert from Type to TcType here
+    -- A bit tiresome; but one day I expect the two types to be entirely separate
+    -- in which case we'll definitely need to do this
+    to_tc_type forall_tvs (TyVarTy tv)
+      | Just var <- lookupVarSet forall_tvs tv = TyVarTy var
+      | otherwise = TyVarTy (toTcTyVar tv)
+    to_tc_type  ftvs (FunTy t1 t2)     = FunTy (to_tc_type ftvs t1) (to_tc_type ftvs t2)
+    to_tc_type  ftvs (AppTy t1 t2)     = AppTy (to_tc_type ftvs t1) (to_tc_type ftvs t2)
+    to_tc_type  ftvs (TyConApp tc tys) = TyConApp tc (map (to_tc_type ftvs) tys)
+    to_tc_type  ftvs (ForAllTy tv ty)  = let tv' = toTcTyVar tv
+                                         in ForAllTy tv' (to_tc_type (ftvs `extendVarSet` tv') ty)
+    to_tc_type _ftvs (LitTy l)         = LitTy l
+
+toTcTyVar :: TyVar -> TcTyVar
+toTcTyVar tv
+  | isTcTyVar tv = setVarType tv (toTcType (tyVarKind tv))
+  | isId tv      = pprPanic "toTcTyVar: Id:" (ppr tv)
+  | otherwise    = mkTcTyVar (tyVarName tv) (toTcType (tyVarKind tv)) vanillaSkolemTv
+
+toTcTypeBag :: Bag EvVar -> Bag EvVar -- All TyVars are transformed to TcTyVars
+toTcTypeBag evvars = mapBag (\tv -> setTyVarKind tv (toTcType (tyVarKind tv))) evvars
+
+{-
+************************************************************************
+*                                                                      *
 \subsection{Misc}
 *                                                                      *
 ************************************************************************
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index a7d6ca96bf..13ac503d35 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -30,7 +30,7 @@ module Type (
         mkTyConApp, mkTyConTy,
         tyConAppTyCon_maybe, tyConAppArgs_maybe, tyConAppTyCon, tyConAppArgs,
         splitTyConApp_maybe, splitTyConApp, tyConAppArgN, nextRole,
-        splitTyConArgs,
+        splitTyConArgs, splitListTyConApp_maybe,
 
         mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys,
         mkPiKinds, mkPiType, mkPiTypes,
@@ -126,7 +126,7 @@ module Type (
         -- ** Performing substitution on types and kinds
         substTy, substTys, substTyWith, substTysWith, substTheta,
         substTyVar, substTyVars, substTyVarBndr,
-        cloneTyVarBndr, deShadowTy, lookupTyVar,
+        cloneTyVarBndr, cloneTyVarBndrs, deShadowTy, lookupTyVar,
         substKiWith, substKisWith,
 
         -- * Pretty-printing
@@ -164,7 +164,7 @@ import NameEnv
 import Class
 import TyCon
 import TysPrim
-import {-# SOURCE #-} TysWiredIn ( eqTyCon, coercibleTyCon, typeNatKind, typeSymbolKind )
+import {-# SOURCE #-} TysWiredIn ( eqTyCon, listTyCon, coercibleTyCon, typeNatKind, typeSymbolKind )
 import PrelNames ( eqTyConKey, coercibleTyConKey,
                    ipTyConKey, openTypeKindTyConKey,
                    constraintKindTyConKey, liftedTypeKindTyConKey,
@@ -178,6 +178,7 @@ import CoAxiom
 
 -- others
 import Unique           ( Unique, hasKey )
+import UniqSupply       ( UniqSupply, takeUniqFromSupply )
 import BasicTypes       ( Arity, RepArity )
 import Util
 import ListSetOps       ( getNth )
@@ -628,6 +629,13 @@ splitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
 splitTyConApp_maybe (FunTy arg res)   = Just (funTyCon, [arg,res])
 splitTyConApp_maybe _                 = Nothing
 
+-- | Attempts to tease a list type apart and gives the type of the elements if
+-- successful (looks through type synonyms)
+splitListTyConApp_maybe :: Type -> Maybe Type
+splitListTyConApp_maybe ty = case splitTyConApp_maybe ty of
+  Just (tc,[e]) | tc == listTyCon -> Just e
+  _other                          -> Nothing
+
 -- | What is the role assigned to the next parameter of this type? Usually,
 -- this will be 'Nominal', but if the type is a 'TyConApp', we may be able to
 -- do better. The type does *not* have to be well-kinded when applied for this
@@ -1716,6 +1724,14 @@ cloneTyVarBndr (TvSubst in_scope tv_env) tv uniq
     tv' = setVarUnique tv uniq  -- Simply set the unique; the kind
                                 -- has no type variables to worry about
 
+cloneTyVarBndrs :: TvSubst -> [TyVar] -> UniqSupply -> (TvSubst, [TyVar])
+cloneTyVarBndrs subst []     _usupply = (subst, [])
+cloneTyVarBndrs subst (t:ts)  usupply = (subst'', tv:tvs)
+  where
+    (uniq, usupply') = takeUniqFromSupply usupply
+    (subst' , tv )   = cloneTyVarBndr subst t uniq
+    (subst'', tvs)   = cloneTyVarBndrs subst' ts usupply'
+
 {-
 ----------------------------------------------------
 -- Kind Stuff
diff --git a/compiler/utils/Bag.hs b/compiler/utils/Bag.hs
index 09fc00acdc..4a826fbf4a 100644
--- a/compiler/utils/Bag.hs
+++ b/compiler/utils/Bag.hs
@@ -20,13 +20,15 @@ module Bag (
         listToBag, bagToList,
         foldrBagM, foldlBagM, mapBagM, mapBagM_,
         flatMapBagM, flatMapBagPairM,
-        mapAndUnzipBagM, mapAccumBagLM
+        mapAndUnzipBagM, mapAccumBagLM,
+        anyBagM, filterBagM
     ) where
 
 import Outputable
 import Util
 
 import MonadUtils
+import Control.Monad
 import Data.Data
 import Data.List ( partition )
 import qualified Data.Foldable as Foldable
@@ -93,12 +95,34 @@ filterBag pred (TwoBags b1 b2) = sat1 `unionBags` sat2
           sat2 = filterBag pred b2
 filterBag pred (ListBag vs)    = listToBag (filter pred vs)
 
+filterBagM :: Monad m => (a -> m Bool) -> Bag a -> m (Bag a)
+filterBagM _    EmptyBag = return EmptyBag
+filterBagM pred b@(UnitBag val) = do
+  flag <- pred val
+  if flag then return b
+          else return EmptyBag
+filterBagM pred (TwoBags b1 b2) = do
+  sat1 <- filterBagM pred b1
+  sat2 <- filterBagM pred b2
+  return (sat1 `unionBags` sat2)
+filterBagM pred (ListBag vs) = do
+  sat <- filterM pred vs
+  return (listToBag sat)
+
 anyBag :: (a -> Bool) -> Bag a -> Bool
 anyBag _ EmptyBag        = False
 anyBag p (UnitBag v)     = p v
 anyBag p (TwoBags b1 b2) = anyBag p b1 || anyBag p b2
 anyBag p (ListBag xs)    = any p xs
 
+anyBagM :: Monad m => (a -> m Bool) -> Bag a -> m Bool
+anyBagM _ EmptyBag        = return False
+anyBagM p (UnitBag v)     = p v
+anyBagM p (TwoBags b1 b2) = do flag <- anyBagM p b1
+                               if flag then return True
+                                       else anyBagM p b2
+anyBagM p (ListBag xs)    = anyM p xs
+
 concatBag :: Bag (Bag a) -> Bag a
 concatBag bss = foldrBag add emptyBag bss
   where
diff --git a/compiler/utils/MonadUtils.hs b/compiler/utils/MonadUtils.hs
index e20178c4f8..255a0f50f6 100644
--- a/compiler/utils/MonadUtils.hs
+++ b/compiler/utils/MonadUtils.hs
@@ -18,7 +18,7 @@ module MonadUtils
         , concatMapM
         , mapMaybeM
         , fmapMaybeM, fmapEitherM
-        , anyM, allM
+        , anyM, allM, orM
         , foldlM, foldlM_, foldrM
         , maybeMapM
         , whenM
@@ -149,6 +149,10 @@ allM :: Monad m => (a -> m Bool) -> [a] -> m Bool
 allM _ []     = return True
 allM f (b:bs) = (f b) >>= (\bv -> if bv then allM f bs else return False)
 
+-- | Monadic version of or
+orM :: Monad m => m Bool -> m Bool -> m Bool
+orM m1 m2 = m1 >>= \x -> if x then return True else m2
+
 -- | Monadic version of foldl
 foldlM :: (Monad m) => (a -> b -> m a) -> a -> [b] -> m a
 foldlM = foldM