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.

1 files changed, 59 insertions, 5 deletions

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