diff options
| -rw-r--r-- | compiler/deSugar/Check.hs | 89 | ||||
| -rw-r--r-- | compiler/typecheck/TcExpr.hs | 7 | ||||
| -rw-r--r-- | compiler/typecheck/TcMType.hs | 12 | ||||
| -rw-r--r-- | compiler/typecheck/TcSimplify.hs | 53 | ||||
| -rw-r--r-- | compiler/utils/MonadUtils.hs | 7 | ||||
| -rw-r--r-- | testsuite/tests/pmcheck/should_compile/T14813.hs | 28 | ||||
| -rw-r--r-- | testsuite/tests/pmcheck/should_compile/T15305.hs | 5 | ||||
| -rw-r--r-- | testsuite/tests/pmcheck/should_compile/T15305.stderr | 2 | ||||
| -rw-r--r-- | testsuite/tests/pmcheck/should_compile/all.T | 2 |
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, |