Normalise EmptyCase types using the constraint solver

Summary:
Certain `EmptyCase` expressions were mistakently producing
warnings since their types did not have as many type families reduced
as they could have. The most direct way to fix this is to normalise
these types initially using the constraint solver to solve for any
local equalities that may be in scope.

Test Plan: make test TEST=T14813

Reviewers: simonpj, bgamari, goldfire

Reviewed By: simonpj

Subscribers: rwbarton, carter

GHC Trac Issues: #14813

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

9 files changed, 162 insertions, 43 deletions

diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs
index 24ce3a9ebb..4cd5601c9b 100644
--- a/compiler/deSugar/Check.hs
+++ b/compiler/deSugar/Check.hs
@@ -12,10 +12,7 @@ module Check (
         checkSingle, checkMatches, checkGuardMatches, isAnyPmCheckEnabled,
 
         -- See Note [Type and Term Equality Propagation]
-        genCaseTmCs1, genCaseTmCs2,
-
-        -- Pattern-match-specific type operations
-        pmIsClosedType, pmTopNormaliseType_maybe
+        genCaseTmCs1, genCaseTmCs2
     ) where
 
 #include "HsVersions.h"
@@ -60,6 +57,7 @@ import Data.Maybe    (catMaybes, isJust, fromMaybe)
 import Control.Monad (forM, when, forM_, zipWithM)
 import Coercion
 import TcEvidence
+import TcSimplify    (tcNormalise)
 import IOEnv
 import qualified Data.Semigroup as Semi
 
@@ -430,8 +428,7 @@ checkMatches' vars matches
 checkEmptyCase' :: Id -> PmM PmResult
 checkEmptyCase' var = do
   tm_ty_css     <- pmInitialTmTyCs
-  fam_insts     <- liftD dsGetFamInstEnvs
-  mb_candidates <- inhabitationCandidates fam_insts (idType var)
+  mb_candidates <- inhabitationCandidates (delta_ty_cs tm_ty_css) (idType var)
   case mb_candidates of
     -- Inhabitation checking failed / the type is trivially inhabited
     Left ty -> return (uncoveredWithTy ty)
@@ -483,7 +480,8 @@ pmIsClosedType ty
     is_algebraic_like :: TyCon -> Bool
     is_algebraic_like tc = isAlgTyCon tc || tc == tYPETyCon
 
-pmTopNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe (Type, [DataCon], Type)
+pmTopNormaliseType_maybe :: FamInstEnvs -> Bag EvVar -> Type
+                         -> PmM (Maybe (Type, [DataCon], Type))
 -- ^ Get rid of *outermost* (or toplevel)
 --      * type function redex
 --      * data family redex
@@ -492,9 +490,18 @@ pmTopNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe (Type, [DataCon], Type)
 -- Behaves exactly like `topNormaliseType_maybe`, but instead of returning a
 -- coercion, it returns useful information for issuing pattern matching
 -- warnings. See Note [Type normalisation for EmptyCase] for details.
-pmTopNormaliseType_maybe env typ
-  = do ((ty_f,tm_f), ty) <- topNormaliseTypeX stepper comb typ
-       return (eq_src_ty ty (typ : ty_f [ty]), tm_f [], ty)
+pmTopNormaliseType_maybe env ty_cs typ
+  = do (_, mb_typ') <- liftD $ initTcDsForSolver $ tcNormalise ty_cs typ
+         -- Before proceeding, we chuck typ into the constraint solver, in case
+         -- solving for given equalities may reduce typ some. See
+         -- "Wrinkle: local equalities" in
+         -- Note [Type normalisation for EmptyCase].
+       pure $ do typ' <- mb_typ'
+                 ((ty_f,tm_f), ty) <- topNormaliseTypeX stepper comb typ'
+                 -- We need to do topNormaliseTypeX in addition to tcNormalise,
+                 -- since topNormaliseX looks through newtypes, which
+                 -- tcNormalise does not do.
+                 Just (eq_src_ty ty (typ' : ty_f [ty]), tm_f [], ty)
   where
     -- Find the first type in the sequence of rewrites that is a data type,
     -- newtype, or a data family application (not the representation tycon!).
@@ -645,9 +652,10 @@ tmTyCsAreSatisfiable
 checkAllNonVoid :: RecTcChecker -> Delta -> [Type] -> PmM Bool
 checkAllNonVoid rec_ts amb_cs strict_arg_tys = do
   fam_insts <- liftD dsGetFamInstEnvs
-  let tys_to_check = filterOut (definitelyInhabitedType fam_insts)
-                               strict_arg_tys
-      rec_max_bound | tys_to_check `lengthExceeds` 1
+  let definitely_inhabited =
+        definitelyInhabitedType fam_insts (delta_ty_cs amb_cs)
+  tys_to_check <- filterOutM definitely_inhabited strict_arg_tys
+  let rec_max_bound | tys_to_check `lengthExceeds` 1
                     = 1
                     | otherwise
                     = defaultRecTcMaxBound
@@ -667,8 +675,7 @@ nonVoid
                   --   'False' if it is definitely uninhabitable by anything
                   --   (except bottom).
 nonVoid rec_ts amb_cs strict_arg_ty = do
-  fam_insts <- liftD dsGetFamInstEnvs
-  mb_cands <- inhabitationCandidates fam_insts strict_arg_ty
+  mb_cands <- inhabitationCandidates (delta_ty_cs amb_cs) strict_arg_ty
   case mb_cands of
     Right (tc, cands)
       |  Just rec_ts' <- checkRecTc rec_ts tc
@@ -707,12 +714,12 @@ nonVoid rec_ts amb_cs strict_arg_ty = do
 --
 -- See the \"Strict argument type constraints\" section of
 -- @Note [Extensions to GADTs Meet Their Match]@.
-definitelyInhabitedType :: FamInstEnvs -> Type -> Bool
-definitelyInhabitedType env ty
-  | Just (_, cons, _) <- pmTopNormaliseType_maybe env ty
-  = any meets_criteria cons
-  | otherwise
-  = False
+definitelyInhabitedType :: FamInstEnvs -> Bag EvVar -> Type -> PmM Bool
+definitelyInhabitedType env ty_cs ty = do
+  mb_res <- pmTopNormaliseType_maybe env ty_cs ty
+  pure $ case mb_res of
+           Just (_, cons, _) -> any meets_criteria cons
+           Nothing           -> False
   where
     meets_criteria :: DataCon -> Bool
     meets_criteria con =
@@ -733,7 +740,8 @@ It returns 3 results instead of one, because there are 2 subtle points:
 2. The representational data family tycon is used internally but should not be
    shown to the user
 
-Hence, if pmTopNormaliseType_maybe env ty = Just (src_ty, dcs, core_ty), then
+Hence, if pmTopNormaliseType_maybe env ty_cs ty = Just (src_ty, dcs, core_ty),
+then
   (a) src_ty is the rewritten type which we can show to the user. That is, the
       type we get if we rewrite type families but not data families or
       newtypes.
@@ -741,7 +749,7 @@ Hence, if pmTopNormaliseType_maybe env ty = Just (src_ty, dcs, core_ty), then
       newtype to it's core representation, we keep track of the source data
       constructor.
   (c) core_ty is the rewritten type. That is,
-        pmTopNormaliseType_maybe env ty = Just (src_ty, dcs, core_ty)
+        pmTopNormaliseType_maybe env ty_cs ty = Just (src_ty, dcs, core_ty)
       implies
         topNormaliseType_maybe env ty = Just (co, core_ty)
       for some coercion co.
@@ -761,13 +769,34 @@ To see how all cases come into play, consider the following example:
   type instance F Int  = F Char
   type instance F Char = G2
 
-In this case pmTopNormaliseType_maybe env (F Int) results in
+In this case pmTopNormaliseType_maybe env ty_cs (F Int) results in
 
   Just (G2, [MkG2,MkG1], R:TInt)
 
 Which means that in source Haskell:
   - G2 is equivalent to F Int (in contrast, G1 isn't).
   - if (x : R:TInt) then (MkG2 (MkG1 x) : F Int).
+
+-----
+-- Wrinkle: Local equalities
+-----
+
+Given the following type family:
+
+  type family F a
+  type instance F Int = Void
+
+Should the following program (from #14813) be considered exhaustive?
+
+  f :: (i ~ Int) => F i -> a
+  f x = case x of {}
+
+You might think "of course, since `x` is obviously of type Void". But the
+idType of `x` is technically F i, not Void, so if we pass F i to
+inhabitationCandidates, we'll mistakenly conclude that `f` is non-exhaustive.
+In order to avoid this pitfall, we need to normalise the type passed to
+pmTopNormaliseType_maybe, using the constraint solver to solve for any local
+equalities (such as i ~ Int) that may be in scope.
 -}
 
 -- | Generate all 'InhabitationCandidate's for a given type. The result is
@@ -776,12 +805,14 @@ Which means that in source Haskell:
 -- if it can. In this case, the candidates are the signature of the tycon, each
 -- one accompanied by the term- and type- constraints it gives rise to.
 -- See also Note [Checking EmptyCase Expressions]
-inhabitationCandidates :: FamInstEnvs -> Type
+inhabitationCandidates :: Bag EvVar -> Type
                        -> PmM (Either Type (TyCon, [InhabitationCandidate]))
-inhabitationCandidates fam_insts ty
-  = case pmTopNormaliseType_maybe fam_insts ty of
-      Just (src_ty, dcs, core_ty) -> alts_to_check src_ty core_ty dcs
-      Nothing                     -> alts_to_check ty     ty      []
+inhabitationCandidates ty_cs ty = do
+  fam_insts   <- liftD dsGetFamInstEnvs
+  mb_norm_res <- pmTopNormaliseType_maybe fam_insts ty_cs ty
+  case mb_norm_res of
+    Just (src_ty, dcs, core_ty) -> alts_to_check src_ty core_ty dcs
+    Nothing                     -> alts_to_check ty     ty      []
   where
     -- All these types are trivially inhabited
     trivially_inhabited = [ charTyCon, doubleTyCon, floatTyCon
diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs
index b70276da7e..519fa5373c 100644
--- a/compiler/typecheck/TcExpr.hs
+++ b/compiler/typecheck/TcExpr.hs
@@ -1849,12 +1849,7 @@ tcUnboundId rn_expr unbound res_ty
       ; let occ = unboundVarOcc unbound
       ; name <- newSysName occ
       ; let ev = mkLocalId name ty
-      ; loc <- getCtLocM HoleOrigin Nothing
-      ; let can = CHoleCan { cc_ev = CtWanted { ctev_pred = ty
-                                              , ctev_dest = EvVarDest ev
-                                              , ctev_nosh = WDeriv
-                                              , ctev_loc  = loc}
-                           , cc_hole = ExprHole unbound }
+      ; can <- newHoleCt (ExprHole unbound) ev ty
       ; emitInsoluble can
       ; tcWrapResultO (UnboundOccurrenceOf occ) rn_expr (HsVar noExt (noLoc ev))
                                                                      ty res_ty }
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index 26d1a33486..fb5f1b515a 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -39,7 +39,7 @@ module TcMType (
   --------------------------------
   -- Creating new evidence variables
   newEvVar, newEvVars, newDict,
-  newWanted, newWanteds, cloneWanted, cloneWC,
+  newWanted, newWanteds, newHoleCt, cloneWanted, cloneWC,
   emitWanted, emitWantedEq, emitWantedEvVar, emitWantedEvVars,
   newTcEvBinds, newNoTcEvBinds, addTcEvBind,
 
@@ -179,6 +179,16 @@ newWanted orig t_or_k pty
 newWanteds :: CtOrigin -> ThetaType -> TcM [CtEvidence]
 newWanteds orig = mapM (newWanted orig Nothing)
 
+-- | Create a new 'CHoleCan' 'Ct'.
+newHoleCt :: Hole -> Id -> Type -> TcM Ct
+newHoleCt hole ev ty = do
+  loc <- getCtLocM HoleOrigin Nothing
+  pure $ CHoleCan { cc_ev = CtWanted { ctev_pred = ty
+                                     , ctev_dest = EvVarDest ev
+                                     , ctev_nosh = WDeriv
+                                     , ctev_loc  = loc }
+                  , cc_hole = hole }
+
 ----------------------------------------------
 -- Cloning constraints
 ----------------------------------------------
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index 2a89ab2d41..6675a931e5 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -10,6 +10,7 @@ module TcSimplify(
        solveEqualities, solveLocalEqualities,
        simplifyWantedsTcM,
        tcCheckSatisfiability,
+       tcNormalise,
 
        captureTopConstraints,
 
@@ -32,13 +33,15 @@ import Class         ( Class, classKey, classTyCon )
 import DynFlags      ( WarningFlag ( Opt_WarnMonomorphism )
                      , WarnReason ( Reason )
                      , DynFlags( solverIterations ) )
-import Id            ( idType )
+import HsExpr        ( UnboundVar(..) )
+import Id            ( idType, mkLocalId )
 import Inst
 import ListSetOps
 import Name
 import Outputable
 import PrelInfo
 import PrelNames
+import RdrName       ( emptyGlobalRdrEnv )
 import TcErrors
 import TcEvidence
 import TcInteract
@@ -546,6 +549,35 @@ tcCheckSatisfiability given_ids
            ; solveSimpleGivens new_given
            ; getInertInsols }
 
+-- | Normalise a type as much as possible using the given constraints.
+-- See @Note [tcNormalise]@.
+tcNormalise :: Bag EvVar -> Type -> TcM Type
+tcNormalise given_ids ty
+  = do { lcl_env <- TcM.getLclEnv
+       ; let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env
+       ; wanted_ct <- mk_wanted_ct
+       ; (res, _ev_binds) <- runTcS $
+             do { traceTcS "tcNormalise {" (ppr given_ids)
+                ; let given_cts = mkGivens given_loc (bagToList given_ids)
+                ; solveSimpleGivens given_cts
+                ; wcs <- solveSimpleWanteds (unitBag wanted_ct)
+                  -- It's an invariant that this wc_simple will always be
+                  -- a singleton Ct, since that's what we fed in as input.
+                ; let ty' = case bagToList (wc_simple wcs) of
+                              (ct:_) -> ctEvPred (ctEvidence ct)
+                              cts    -> pprPanic "tcNormalise" (ppr cts)
+                ; traceTcS "tcNormalise }" (ppr ty')
+                ; pure ty' }
+       ; return res }
+  where
+    mk_wanted_ct :: TcM Ct
+    mk_wanted_ct = do
+      let occ = mkVarOcc "$tcNorm"
+      name <- newSysName occ
+      let ev = mkLocalId name ty
+          hole = ExprHole $ OutOfScope occ emptyGlobalRdrEnv
+      newHoleCt hole ev ty
+
 {- Note [Superclasses and satisfiability]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Expand superclasses before starting, because (Int ~ Bool), has
@@ -566,6 +598,25 @@ the constraints /are/ satisfiable (Trac #10592 comment:12!).
 For stratightforard situations without type functions the try_harder
 step does nothing.
 
+Note [tcNormalise]
+~~~~~~~~~~~~~~~~~~
+tcNormalise is a rather atypical entrypoint to the constraint solver. Whereas
+most invocations of the constraint solver are intended to simplify a set of
+constraints or to decide if a particular set of constraints is satisfiable,
+the purpose of tcNormalise is to take a type, plus some local constraints, and
+normalise the type as much as possible with respect to those constraints.
+
+Why is this useful? As one example, when coverage-checking an EmptyCase
+expression, it's possible that the type of the scrutinee will only reduce
+if some local equalities are solved for. See "Wrinkle: Local equalities"
+in Note [Type normalisation for EmptyCase] in Check.
+
+To accomplish its stated goal, tcNormalise first feeds the local constraints
+into solveSimpleGivens, then stuffs the argument type in a CHoleCan, and feeds
+that singleton Ct into solveSimpleWanteds, which reduces the type in the
+CHoleCan as much as possible with respect to the local given constraints. When
+solveSimpleWanteds is finished, we dig out the type from the CHoleCan and
+return that.
 
 ***********************************************************************************
 *                                                                                 *
diff --git a/compiler/utils/MonadUtils.hs b/compiler/utils/MonadUtils.hs
index 39a76e1cf2..e86bc49708 100644
--- a/compiler/utils/MonadUtils.hs
+++ b/compiler/utils/MonadUtils.hs
@@ -21,6 +21,7 @@ module MonadUtils
         , foldlM, foldlM_, foldrM
         , maybeMapM
         , whenM, unlessM
+        , filterOutM
         ) where
 
 -------------------------------------------------------------------------------
@@ -31,6 +32,7 @@ import GhcPrelude
 
 import Maybes
 
+import Control.Applicative
 import Control.Monad
 import Control.Monad.Fix
 import Control.Monad.IO.Class
@@ -199,3 +201,8 @@ whenM mb thing = do { b <- mb
 unlessM :: Monad m => m Bool -> m () -> m ()
 unlessM condM acc = do { cond <- condM
                        ; unless cond acc }
+
+-- | Like 'filterM', only it reverses the sense of the test.
+filterOutM :: (Applicative m) => (a -> m Bool) -> [a] -> m [a]
+filterOutM p =
+  foldr (\ x -> liftA2 (\ flg -> if flg then id else (x:)) (p x)) (pure [])
diff --git a/testsuite/tests/pmcheck/should_compile/T14813.hs b/testsuite/tests/pmcheck/should_compile/T14813.hs
new file mode 100644
index 0000000000..1dcfe756f9
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T14813.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# OPTIONS_GHC -Wall #-}
+module T14813 where
+
+import Data.Kind
+import Data.Void
+
+data SBool (z :: Bool) where
+  SFalse :: SBool 'False
+  STrue  :: SBool 'True
+
+type family F (b :: Bool) (a :: Type) :: Type where
+  F 'True  a = a
+  F 'False _ = Void
+
+dispatch :: forall (b :: Bool) (a :: Type). SBool b -> F b a -> a
+dispatch STrue  x = x
+dispatch SFalse x = case x of {}
+
+type family G a
+type instance G Int = Void
+
+fun :: i ~ Int => G i -> a
+fun x = case x of {}
diff --git a/testsuite/tests/pmcheck/should_compile/T15305.hs b/testsuite/tests/pmcheck/should_compile/T15305.hs
index 82214b7e19..8ee1a18385 100644
--- a/testsuite/tests/pmcheck/should_compile/T15305.hs
+++ b/testsuite/tests/pmcheck/should_compile/T15305.hs
@@ -36,15 +36,10 @@ data HsImplicitBndrs pass
 
 fun2 :: HsImplicitBndrs (GhcPass pass) -> ()
 fun2 UsefulConstructor = ()
-{-
-NB: the seemingly equivalent function
 
 fun2' :: (p ~ GhcPass pass) => HsImplicitBndrs p -> ()
 fun2' UsefulConstructor = ()
 
-Is mistakenly deemed non-exhaustive at the moment due to #14813.
--}
-
 -- Example 3
 
 data Abyss = MkAbyss !Abyss
diff --git a/testsuite/tests/pmcheck/should_compile/T15305.stderr b/testsuite/tests/pmcheck/should_compile/T15305.stderr
index bb88a9be5b..54cb90af5e 100644
--- a/testsuite/tests/pmcheck/should_compile/T15305.stderr
+++ b/testsuite/tests/pmcheck/should_compile/T15305.stderr
@@ -1,4 +1,4 @@
 
-T15305.hs:53:23: warning: [-Wincomplete-patterns (in -Wextra)]
+T15305.hs:48:23: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
     In a case alternative: Patterns not matched: (MkAbyss _)
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index 20eef3ff95..079978b5f5 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -63,6 +63,8 @@ test('T14086', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T14098', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T14813', normal, compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T15305', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T15385', normal, compile,