diff options
87 files changed, 3062 insertions, 913 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 diff --git a/testsuite/tests/deSugar/should_compile/T2395.stderr b/testsuite/tests/deSugar/should_compile/T2395.stderr index 940f263412..a2ed232e78 100644 --- a/testsuite/tests/deSugar/should_compile/T2395.stderr +++ b/testsuite/tests/deSugar/should_compile/T2395.stderr @@ -1,4 +1,4 @@ -T2395.hs:12:1: Warning: - Pattern match(es) are overlapped +T2395.hs:12:1: warning: + Pattern match(es) are redundant In an equation for ‘bar’: bar _ = ... diff --git a/testsuite/tests/deSugar/should_compile/T5117.stderr b/testsuite/tests/deSugar/should_compile/T5117.stderr index 93de2cf9e7..954844d5f9 100644 --- a/testsuite/tests/deSugar/should_compile/T5117.stderr +++ b/testsuite/tests/deSugar/should_compile/T5117.stderr @@ -1,4 +1,4 @@ T5117.hs:15:1: Warning: - Pattern match(es) are overlapped + Pattern match(es) are redundant In an equation for ‘f3’: f3 (MyString "a") = ... diff --git a/testsuite/tests/deSugar/should_compile/all.T b/testsuite/tests/deSugar/should_compile/all.T index c6b024f1b9..dbc327f237 100644 --- a/testsuite/tests/deSugar/should_compile/all.T +++ b/testsuite/tests/deSugar/should_compile/all.T @@ -63,7 +63,6 @@ test('ds056', normal, compile, ['-Wall -fno-warn-tabs']) test('ds057', normal, compile, ['']) test('ds058', normal, compile, ['-W -fno-warn-tabs']) test('ds059', normal, compile, ['-W']) -test('ds060', expect_broken(322), compile, ['']) test('ds062', normal, compile, ['']) test('ds063', normal, compile, ['']) diff --git a/testsuite/tests/deSugar/should_compile/ds002.stderr b/testsuite/tests/deSugar/should_compile/ds002.stderr index fe4ec94873..3810c1b77b 100644 --- a/testsuite/tests/deSugar/should_compile/ds002.stderr +++ b/testsuite/tests/deSugar/should_compile/ds002.stderr @@ -1,10 +1,10 @@ ds002.hs:7:1: Warning: - Pattern match(es) are overlapped + Pattern match(es) are redundant In an equation for ‘f’: f y = ... f z = ... ds002.hs:11:1: Warning: - Pattern match(es) are overlapped + Pattern match(es) are redundant In an equation for ‘g’: g x y z = ... diff --git a/testsuite/tests/deSugar/should_compile/ds003.stderr b/testsuite/tests/deSugar/should_compile/ds003.stderr index 1b4c018b62..fdde26f10e 100644 --- a/testsuite/tests/deSugar/should_compile/ds003.stderr +++ b/testsuite/tests/deSugar/should_compile/ds003.stderr @@ -1,6 +1,6 @@ ds003.hs:5:1: Warning: - Pattern match(es) are overlapped + Pattern match(es) are redundant In an equation for ‘f’: f (x : x1 : x2 : x3) ~(y, ys) z = ... f x y True = ... diff --git a/testsuite/tests/deSugar/should_compile/ds019.stderr b/testsuite/tests/deSugar/should_compile/ds019.stderr index 4d6e60f1fa..0a99306cd2 100644 --- a/testsuite/tests/deSugar/should_compile/ds019.stderr +++ b/testsuite/tests/deSugar/should_compile/ds019.stderr @@ -1,6 +1,6 @@ ds019.hs:5:1: Warning: - Pattern match(es) are overlapped + Pattern match(es) are redundant In an equation for ‘f’: f d (j, k) p = ... f (e, f, g) l q = ... diff --git a/testsuite/tests/deSugar/should_compile/ds020.stderr b/testsuite/tests/deSugar/should_compile/ds020.stderr index 4120a957d3..8775bc6d6e 100644 --- a/testsuite/tests/deSugar/should_compile/ds020.stderr +++ b/testsuite/tests/deSugar/should_compile/ds020.stderr @@ -1,18 +1,18 @@ ds020.hs:8:1: Warning: - Pattern match(es) are overlapped + Pattern match(es) are redundant In an equation for ‘a’: a ~(~[], ~[], ~[]) = ... ds020.hs:11:1: Warning: - Pattern match(es) are overlapped + Pattern match(es) are redundant In an equation for ‘b’: b ~(~x : ~xs : ~ys) = ... ds020.hs:16:1: Warning: - Pattern match(es) are overlapped + Pattern match(es) are redundant In an equation for ‘d’: d ~(n+43) = ... d ~(n+999) = ... ds020.hs:22:1: Warning: - Pattern match(es) are overlapped + Pattern match(es) are redundant In an equation for ‘f’: f x@(~[]) = ... diff --git a/testsuite/tests/deSugar/should_compile/ds022.hs b/testsuite/tests/deSugar/should_compile/ds022.hs index 2ac429f95b..a857ef44b0 100644 --- a/testsuite/tests/deSugar/should_compile/ds022.hs +++ b/testsuite/tests/deSugar/should_compile/ds022.hs @@ -1,5 +1,7 @@ -- !!! ds022 -- literal patterns (wimp version) -- +{-# OPTIONS_GHC -fwarn-overlapping-patterns #-} + module ShouldCompile where f 1 1.1 = [] diff --git a/testsuite/tests/deSugar/should_compile/ds022.stderr b/testsuite/tests/deSugar/should_compile/ds022.stderr index 45fe3d8a95..17b62fee02 100644 --- a/testsuite/tests/deSugar/should_compile/ds022.stderr +++ b/testsuite/tests/deSugar/should_compile/ds022.stderr @@ -1,6 +1,6 @@ -ds022.hs:20:1: Warning: - Pattern match(es) are overlapped +ds022.hs:22:1: Warning: + Pattern match(es) are redundant In an equation for ‘i’: i 1 0.011e2 = ... i 2 2.20000 = ... diff --git a/testsuite/tests/deSugar/should_compile/ds043.stderr b/testsuite/tests/deSugar/should_compile/ds043.stderr index 8529a8c737..0339745bab 100644 --- a/testsuite/tests/deSugar/should_compile/ds043.stderr +++ b/testsuite/tests/deSugar/should_compile/ds043.stderr @@ -1,4 +1,4 @@ -ds043.hs:8:2: - Warning: Pattern match(es) are overlapped - In a case alternative: B {e = True, f = False} -> ... +ds043.hs:8:2: warning: + Pattern match(es) are redundant + In a case alternative: B {e = True, f = False} -> ... diff --git a/testsuite/tests/deSugar/should_compile/ds051.stderr b/testsuite/tests/deSugar/should_compile/ds051.stderr index 76bc4d3968..4777dfcc2d 100644 --- a/testsuite/tests/deSugar/should_compile/ds051.stderr +++ b/testsuite/tests/deSugar/should_compile/ds051.stderr @@ -1,12 +1,12 @@ ds051.hs:6:1: Warning: - Pattern match(es) are overlapped + Pattern match(es) are redundant In an equation for ‘f1’: f1 "ab" = ... ds051.hs:11:1: Warning: - Pattern match(es) are overlapped + Pattern match(es) are redundant In an equation for ‘f2’: f2 ('a' : 'b' : []) = ... ds051.hs:16:1: Warning: - Pattern match(es) are overlapped + Pattern match(es) are redundant In an equation for ‘f3’: f3 "ab" = ... diff --git a/testsuite/tests/deSugar/should_compile/ds056.stderr b/testsuite/tests/deSugar/should_compile/ds056.stderr index 3f44267f2a..bcea3fdb07 100644 --- a/testsuite/tests/deSugar/should_compile/ds056.stderr +++ b/testsuite/tests/deSugar/should_compile/ds056.stderr @@ -1,4 +1,4 @@ -ds056.hs:8:1: Warning: - Pattern match(es) are overlapped +ds056.hs:8:1: warning: + Pattern match(es) are redundant In an equation for ‘g’: g _ = ... diff --git a/testsuite/tests/deSugar/should_compile/ds058.stderr b/testsuite/tests/deSugar/should_compile/ds058.stderr index fb504cc514..82f8141280 100644 --- a/testsuite/tests/deSugar/should_compile/ds058.stderr +++ b/testsuite/tests/deSugar/should_compile/ds058.stderr @@ -1,4 +1,4 @@ -ds058.hs:5:7: - Warning: Pattern match(es) are overlapped - In a case alternative: Just _ -> ... +ds058.hs:5:7: warning: + Pattern match(es) are redundant + In a case alternative: Just _ -> ... diff --git a/testsuite/tests/deSugar/should_compile/ds060.hs b/testsuite/tests/deSugar/should_compile/ds060.hs deleted file mode 100644 index b822605742..0000000000 --- a/testsuite/tests/deSugar/should_compile/ds060.hs +++ /dev/null @@ -1,25 +0,0 @@ - --- Test for trac #322 - -module ShouldCompile where - -instance (Num a) => Num (Maybe a) where - (Just a) + (Just b) = Just (a + b) - _ + _ = Nothing - (Just a) - (Just b) = Just (a - b) - _ - _ = Nothing - (Just a) * (Just b) = Just (a * b) - _ * _ = Nothing - negate (Just a) = Just (negate a) - negate _ = Nothing - abs (Just a) = Just (abs a) - abs _ = Nothing - signum (Just a) = Just (signum a) - signum _ = Nothing - fromInteger = Just . fromInteger - -f :: Maybe Int -> Int -f 1 = 1 -f Nothing = 2 -- Gives bogus "Warning: Pattern match(es) are overlapped" -f _ = 3 - diff --git a/testsuite/tests/driver/werror.stderr b/testsuite/tests/driver/werror.stderr index 5541dfc2e7..20770fa8bc 100644 --- a/testsuite/tests/driver/werror.stderr +++ b/testsuite/tests/driver/werror.stderr @@ -19,12 +19,12 @@ werror.hs:10:1: Warning: f :: forall t t1. [t] -> [t1] werror.hs:10:1: Warning: - Pattern match(es) are overlapped + Pattern match(es) are redundant In an equation for ‘f’: f [] = ... werror.hs:10:1: Warning: Pattern match(es) are non-exhaustive - In an equation for ‘f’: Patterns not matched: _ : _ + In an equation for ‘f’: Patterns not matched: (_:_) <no location info>: Failing due to -Werror. diff --git a/testsuite/tests/gadt/Gadt17_help.hs b/testsuite/tests/gadt/Gadt17_help.hs index e3b8e3a918..5161fdcdb7 100644 --- a/testsuite/tests/gadt/Gadt17_help.hs +++ b/testsuite/tests/gadt/Gadt17_help.hs @@ -16,7 +16,6 @@ instance (Eq a) => Eq (TypeWitness a) where (==) TWBool TWBool = True (==) TWFloat TWFloat = True (==) TWDouble TWDouble = True - (==) _ _ = False data TernOp a b c d where OpIf :: TypeWitness a -> TernOp Bool a a a diff --git a/testsuite/tests/gadt/T7294.stderr b/testsuite/tests/gadt/T7294.stderr index b4379b10bb..0fa7f5386c 100644 --- a/testsuite/tests/gadt/T7294.stderr +++ b/testsuite/tests/gadt/T7294.stderr @@ -1,4 +1,8 @@ +T7294.hs:23:1: warning:
+ Pattern match(es) are redundant
+ In an equation for ‘nth’: nth Nil _ = ...
+
T7294.hs:25:5: Warning:
Couldn't match type ‘'True’ with ‘'False’
Inaccessible code in
diff --git a/testsuite/tests/ghci/scripts/Defer02.stderr b/testsuite/tests/ghci/scripts/Defer02.stderr index 83e9f7d157..8b63df689a 100644 --- a/testsuite/tests/ghci/scripts/Defer02.stderr +++ b/testsuite/tests/ghci/scripts/Defer02.stderr @@ -12,6 +12,10 @@ • In the expression: 'p' In an equation for ‘a’: a = 'p' +../../typecheck/should_run/Defer01.hs:25:1: warning: + Pattern match(es) have inaccessible right hand side + In an equation for ‘c’: c (C2 x) = ... + ../../typecheck/should_run/Defer01.hs:25:4: warning: • Couldn't match type ‘Int’ with ‘Bool’ Inaccessible code in @@ -91,6 +95,10 @@ In the type signature: k :: (Int ~ Bool) => Int -> Bool +../../typecheck/should_run/Defer01.hs:46:1: warning: + Pattern match(es) are redundant + In an equation for ‘k’: k x = ... + ../../typecheck/should_run/Defer01.hs:49:5: warning: • Couldn't match expected type ‘IO a0’ with actual type ‘Char -> IO ()’ diff --git a/testsuite/tests/pmcheck/Makefile b/testsuite/tests/pmcheck/Makefile new file mode 100644 index 0000000000..9a36a1c5fe --- /dev/null +++ b/testsuite/tests/pmcheck/Makefile @@ -0,0 +1,3 @@ +TOP=../.. +include $(TOP)/mk/boilerplate.mk +include $(TOP)/mk/test.mk diff --git a/testsuite/tests/pmcheck/should_compile/Makefile b/testsuite/tests/pmcheck/should_compile/Makefile new file mode 100644 index 0000000000..9101fbd40a --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/Makefile @@ -0,0 +1,3 @@ +TOP=../../.. +include $(TOP)/mk/boilerplate.mk +include $(TOP)/mk/test.mk diff --git a/testsuite/tests/pmcheck/should_compile/T2006.hs b/testsuite/tests/pmcheck/should_compile/T2006.hs new file mode 100644 index 0000000000..00cd783fb2 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T2006.hs @@ -0,0 +1,13 @@ +{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-overlapping-patterns #-} +{-# LANGUAGE GADTs #-} + +module T2006 where + +data Expr a vs where + EPrim :: String -> a -> Expr a vs + EVar :: Expr a (a,vs) + +interpret :: Expr a () -> a +interpret (EPrim _ a) = a +-- interpret EVar = error "unreachable" + diff --git a/testsuite/tests/pmcheck/should_compile/T2006.stderr b/testsuite/tests/pmcheck/should_compile/T2006.stderr new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T2006.stderr diff --git a/testsuite/tests/pmcheck/should_compile/T2204.hs b/testsuite/tests/pmcheck/should_compile/T2204.hs new file mode 100644 index 0000000000..0f2dbec7e0 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T2204.hs @@ -0,0 +1,9 @@ +{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-overlapping-patterns #-} + +module T2204 where + +f :: String -> Int +f "01" = 0 + +g :: Int -> Int +g 0 = 0 diff --git a/testsuite/tests/pmcheck/should_compile/T2204.stderr b/testsuite/tests/pmcheck/should_compile/T2204.stderr new file mode 100644 index 0000000000..e6ad7cf9ae --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T2204.stderr @@ -0,0 +1,14 @@ +T2204.hs:6:1: warning: + Pattern match(es) are non-exhaustive + In an equation for ‘f’: + Patterns not matched: + ('0':'1':_:_) + ('0':p:_) where p is not one of {'1'} + ['0'] + (p:_) where p is not one of {'0'} + ... + +T2204.hs:9:1: warning: + Pattern match(es) are non-exhaustive + In an equation for ‘g’: + Patterns not matched: p where p is not one of {0} diff --git a/testsuite/tests/pmcheck/should_compile/T3078.hs b/testsuite/tests/pmcheck/should_compile/T3078.hs new file mode 100644 index 0000000000..f6d6362faf --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T3078.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE PatternGuards #-} +{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-overlapping-patterns #-} + +module T3078 where + +data T = A Int | B Int + +funny :: T -> Int +funny t = n + where + n | A x <- t = x + | B x <- t = x diff --git a/testsuite/tests/pmcheck/should_compile/T3078.stderr b/testsuite/tests/pmcheck/should_compile/T3078.stderr new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T3078.stderr diff --git a/testsuite/tests/pmcheck/should_compile/T322.hs b/testsuite/tests/pmcheck/should_compile/T322.hs new file mode 100644 index 0000000000..3b8f1a9c7c --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T322.hs @@ -0,0 +1,29 @@ +{-# OPTIONS -fwarn-incomplete-patterns -fwarn-overlapping-patterns -Werror #-} + +module T322 where + +instance (Num a) => Num (Maybe a) where + (Just a) + (Just b) = Just (a + b) + _ + _ = Nothing + + (Just a) - (Just b) = Just (a - b) + _ - _ = Nothing + + (Just a) * (Just b) = Just (a * b) + _ * _ = Nothing + + negate (Just a) = Just (negate a) + negate _ = Nothing + + abs (Just a) = Just (abs a) + abs _ = Nothing + + signum (Just a) = Just (signum a) + signum _ = Nothing + + fromInteger = Just . fromInteger + +f :: Maybe Int -> Int +f 1 = 1 +f Nothing = 2 +f _ = 3 diff --git a/testsuite/tests/pmcheck/should_compile/T322.stderr b/testsuite/tests/pmcheck/should_compile/T322.stderr new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T322.stderr diff --git a/testsuite/tests/pmcheck/should_compile/T366.hs b/testsuite/tests/pmcheck/should_compile/T366.hs new file mode 100644 index 0000000000..f0090acfe3 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T366.hs @@ -0,0 +1,10 @@ +{-# OPTIONS_GHC -XGADTs -fwarn-incomplete-patterns -fwarn-overlapping-patterns #-} + +module T366 where + +data T a where + C1 :: T Char + C2 :: T Float + +exhaustive :: T Char -> Char +exhaustive C1 = ' ' diff --git a/testsuite/tests/pmcheck/should_compile/T366.stderr b/testsuite/tests/pmcheck/should_compile/T366.stderr new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T366.stderr diff --git a/testsuite/tests/pmcheck/should_compile/T3927.hs b/testsuite/tests/pmcheck/should_compile/T3927.hs new file mode 100644 index 0000000000..f1ec01ee7f --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T3927.hs @@ -0,0 +1,13 @@ +{-# LANGUAGE GADTs #-} +{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-overlapping-patterns #-} + +module T3927 where + +data T a where + T1 :: T Int + T2 :: T Bool + +-- f1 is exhaustive +f1 :: T a -> T a -> Bool +f1 T1 T1 = True +f1 T2 T2 = False diff --git a/testsuite/tests/pmcheck/should_compile/T3927.stderr b/testsuite/tests/pmcheck/should_compile/T3927.stderr new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T3927.stderr diff --git a/testsuite/tests/pmcheck/should_compile/T3927a.hs b/testsuite/tests/pmcheck/should_compile/T3927a.hs new file mode 100644 index 0000000000..62fb68b607 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T3927a.hs @@ -0,0 +1,15 @@ +{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-overlapping-patterns #-} +{-# LANGUAGE GADTs, TypeFamilies #-} + +module T3927a where + +type family F a +type instance F a = () + +data Foo a where + FooA :: Foo () + FooB :: Foo Int + +f :: a -> Foo (F a) -> () -- F a can only be () so only FooA is accepted +f _ FooA = () + diff --git a/testsuite/tests/pmcheck/should_compile/T3927a.stderr b/testsuite/tests/pmcheck/should_compile/T3927a.stderr new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T3927a.stderr diff --git a/testsuite/tests/pmcheck/should_compile/T3927b.hs b/testsuite/tests/pmcheck/should_compile/T3927b.hs new file mode 100644 index 0000000000..d2eb8cd6cb --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T3927b.hs @@ -0,0 +1,75 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-overlapping-patterns #-} + +module T3927b where + +import Data.Proxy +import GHC.Exts + +data Message + +data SocketType = Dealer | Push | Pull + +data SocketOperation = Read | Write + +type family Restrict (a :: SocketOperation) (as :: [SocketOperation]) :: Constraint where + Restrict a (a ': as) = () + Restrict x (a ': as) = Restrict x as + Restrict x '[] = ("Error!" ~ "Tried to apply a restricted type!") + +type family Implements (t :: SocketType) :: [SocketOperation] where + Implements Dealer = ['Read, Write] + Implements Push = '[Write] + Implements Pull = '[ 'Read] + +data SockOp :: SocketType -> SocketOperation -> * where + SRead :: SockOp sock 'Read + SWrite :: SockOp sock Write + +data Socket :: SocketType -> * where + Socket :: proxy sock + -> (forall op . Restrict op (Implements sock) => SockOp sock op -> Operation op) + -> Socket sock + +type family Operation (op :: SocketOperation) :: * where + Operation 'Read = IO Message + Operation Write = Message -> IO () + +class Restrict 'Read (Implements t) => Readable t where + readSocket :: Socket t -> Operation 'Read + readSocket (Socket _ f) = f (SRead :: SockOp t 'Read) + +instance Readable Dealer + +type family Writable (t :: SocketType) :: Constraint where + Writable Dealer = () + Writable Push = () + +dealer :: Socket Dealer +dealer = Socket (Proxy :: Proxy Dealer) f + where + f :: Restrict op (Implements Dealer) => SockOp Dealer op -> Operation op + f SRead = undefined + f SWrite = undefined + +push :: Socket Push +push = Socket (Proxy :: Proxy Push) f + where + f :: Restrict op (Implements Push) => SockOp Push op -> Operation op + f SWrite = undefined + +pull :: Socket Pull +pull = Socket (Proxy :: Proxy Pull) f + where + f :: Restrict op (Implements Pull) => SockOp Pull op -> Operation op + f SRead = undefined + +foo :: IO Message +foo = readSocket dealer diff --git a/testsuite/tests/pmcheck/should_compile/T3927b.stderr b/testsuite/tests/pmcheck/should_compile/T3927b.stderr new file mode 100644 index 0000000000..fb4449ced9 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T3927b.stderr @@ -0,0 +1,39 @@ +T3927b.hs:58:5: warning: + • Redundant constraint: Restrict op (Implements 'Dealer) + • In the type signature for: + f :: Restrict op (Implements 'Dealer) => + SockOp 'Dealer op -> Operation op + In an equation for ‘dealer’: + dealer + = Socket (Proxy :: Proxy Dealer) f + where + f :: + Restrict op (Implements Dealer) => SockOp Dealer op -> Operation op + f SRead = undefined + f SWrite = undefined + +T3927b.hs:65:5: warning: + • Redundant constraint: Restrict op (Implements 'Push) + • In the type signature for: + f :: Restrict op (Implements 'Push) => + SockOp 'Push op -> Operation op + In an equation for ‘push’: + push + = Socket (Proxy :: Proxy Push) f + where + f :: + Restrict op (Implements Push) => SockOp Push op -> Operation op + f SWrite = undefined + +T3927b.hs:71:5: warning: + • Redundant constraint: Restrict op (Implements 'Pull) + • In the type signature for: + f :: Restrict op (Implements 'Pull) => + SockOp 'Pull op -> Operation op + In an equation for ‘pull’: + pull + = Socket (Proxy :: Proxy Pull) f + where + f :: + Restrict op (Implements Pull) => SockOp Pull op -> Operation op + f SRead = undefined diff --git a/testsuite/tests/pmcheck/should_compile/T4139.hs b/testsuite/tests/pmcheck/should_compile/T4139.hs new file mode 100644 index 0000000000..4f6d4abab5 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T4139.hs @@ -0,0 +1,28 @@ +{-# LANGUAGE GADTs #-} +{-# OPTIONS_GHC -fwarn-incomplete-patterns #-} + +module T4139 where + +data F a where + FInt :: F Int + FBool :: F Bool + +class Baz a where + baz :: F a -> G a +instance Baz Int where + baz _ = GInt +instance Baz Bool where + baz _ = GBool + +data G a where + GInt :: G Int + GBool :: G Bool + +bar :: Baz a => F a -> () +bar a@(FInt) = + case baz a of + GInt -> () + -- GBool -> () +bar _ = () + + diff --git a/testsuite/tests/pmcheck/should_compile/T4139.stderr b/testsuite/tests/pmcheck/should_compile/T4139.stderr new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T4139.stderr diff --git a/testsuite/tests/pmcheck/should_compile/T6124.hs b/testsuite/tests/pmcheck/should_compile/T6124.hs new file mode 100644 index 0000000000..e4f18b3364 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T6124.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE GADTs #-} +{-# OPTIONS_GHC -fwarn-incomplete-patterns #-} + +module T6124 where + +newtype A = MkA Int +newtype B = MkB Char + +data T a where + A :: T A + B :: T B + +f :: T A -> A +f A = undefined diff --git a/testsuite/tests/pmcheck/should_compile/T6124.stderr b/testsuite/tests/pmcheck/should_compile/T6124.stderr new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T6124.stderr diff --git a/testsuite/tests/pmcheck/should_compile/T7669.hs b/testsuite/tests/pmcheck/should_compile/T7669.hs new file mode 100644 index 0000000000..6744d8afb0 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T7669.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE EmptyCase #-} +{-# OPTIONS_GHC -fwarn-incomplete-patterns #-} + +module T7669 where + +data Void + +foo :: Void -> () +foo x = case x of {} diff --git a/testsuite/tests/pmcheck/should_compile/T7669.stderr b/testsuite/tests/pmcheck/should_compile/T7669.stderr new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T7669.stderr diff --git a/testsuite/tests/pmcheck/should_compile/T8970.hs b/testsuite/tests/pmcheck/should_compile/T8970.hs new file mode 100644 index 0000000000..37e3756918 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T8970.hs @@ -0,0 +1,22 @@ +{-# LANGUAGE DataKinds, KindSignatures, GADTs, TypeFamilies #-} +{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-overlapping-patterns #-} + +module T8970 where + +data K = Foo + | Bar + +data D1 :: K -> * where + F1 :: D1 Foo + B1 :: D1 Bar + +class C (a :: K -> *) where + data D2 a :: K -> * + foo :: a k -> D2 a k -> Bool + +instance C D1 where + data D2 D1 k where + F2 :: D2 D1 Foo + B2 :: D2 D1 Bar + foo F1 F2 = True + foo B1 B2 = True diff --git a/testsuite/tests/pmcheck/should_compile/T8970.stderr b/testsuite/tests/pmcheck/should_compile/T8970.stderr new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T8970.stderr diff --git a/testsuite/tests/pmcheck/should_compile/T9951.hs b/testsuite/tests/pmcheck/should_compile/T9951.hs new file mode 100644 index 0000000000..f1740fd733 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T9951.hs @@ -0,0 +1,10 @@ +{-# LANGUAGE OverloadedLists #-} +{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-overlapping-patterns #-} + +module T9951 where + +f :: [a] -> () +f x = case x of + [] -> () + (_:_) -> () + diff --git a/testsuite/tests/pmcheck/should_compile/T9951.stderr b/testsuite/tests/pmcheck/should_compile/T9951.stderr new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T9951.stderr diff --git a/testsuite/tests/pmcheck/should_compile/T9951b.hs b/testsuite/tests/pmcheck/should_compile/T9951b.hs new file mode 100644 index 0000000000..6ae875dfbb --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T9951b.hs @@ -0,0 +1,7 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-overlapping-patterns #-} + +module T9951b where + +f :: String -> Bool +f "ab" = True diff --git a/testsuite/tests/pmcheck/should_compile/T9951b.stderr b/testsuite/tests/pmcheck/should_compile/T9951b.stderr new file mode 100644 index 0000000000..6a9d0ce112 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T9951b.stderr @@ -0,0 +1,9 @@ +T9951b.hs:7:1: warning: + Pattern match(es) are non-exhaustive + In an equation for ‘f’: + Patterns not matched: + ('a':'b':_:_) + ('a':p:_) where p is not one of {'b'} + ['a'] + (p:_) where p is not one of {'a'} + ... diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T new file mode 100644 index 0000000000..3aac879976 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/all.T @@ -0,0 +1,35 @@ + +# Tests for pattern match checker (coverage and exhaustiveness) + +# Just do the normal way... +def f( name, opts ): + opts.only_ways = ['normal'] + +setTestOpts(f) + +# Bug reports / feature requests +test('T2006', only_compiler_types(['ghc']), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns']) +test('T2204', only_compiler_types(['ghc']), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns']) +test('T3078', only_compiler_types(['ghc']), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns']) +test('T322', only_compiler_types(['ghc']), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns']) +test('T366', only_compiler_types(['ghc']), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns']) +test('T3927a',only_compiler_types(['ghc']), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns']) +test('T3927b',only_compiler_types(['ghc']), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns']) +test('T3927', only_compiler_types(['ghc']), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns']) +test('T4139', only_compiler_types(['ghc']), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns']) +test('T6124', only_compiler_types(['ghc']), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns']) +test('T7669', only_compiler_types(['ghc']), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns']) +test('T8970', only_compiler_types(['ghc']), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns']) +test('T9951b',only_compiler_types(['ghc']), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns']) +test('T9951', only_compiler_types(['ghc']), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns']) + +# Other tests +test('pmc001', only_compiler_types(['ghc']), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns']) +test('pmc002', only_compiler_types(['ghc']), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns']) +test('pmc003', only_compiler_types(['ghc']), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns']) +test('pmc004', only_compiler_types(['ghc']), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns']) +test('pmc005', only_compiler_types(['ghc']), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns']) +test('pmc006', only_compiler_types(['ghc']), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns']) +test('pmc007', only_compiler_types(['ghc']), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns']) + + diff --git a/testsuite/tests/pmcheck/should_compile/pmc001.hs b/testsuite/tests/pmcheck/should_compile/pmc001.hs new file mode 100644 index 0000000000..89cb484349 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/pmc001.hs @@ -0,0 +1,22 @@ +{-# LANGUAGE TypeFamilies, GADTs #-} +{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-overlapping-patterns #-} + +module PMC001 where + +data family T a + +data instance T [a] where + MkT1 :: T [Int] + MkT2 :: Char -> T [Char] + MkT3 :: T [a] + +f :: T [a] -> T [a] -> Bool +f MkT1 MkT1 = True +f (MkT2 _) (MkT2 _) = True +f MkT3 MkT3 = True + +g :: T [a] -> T [a] -> Bool +g x y + | MkT1 <- x, MkT1 <- y = True + | (MkT2 _) <- x, (MkT2 _) <- y = True + | MkT3 <- x, MkT3 <- y = True diff --git a/testsuite/tests/pmcheck/should_compile/pmc001.stderr b/testsuite/tests/pmcheck/should_compile/pmc001.stderr new file mode 100644 index 0000000000..c6145432f0 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/pmc001.stderr @@ -0,0 +1,17 @@ +pmc001.hs:14:1: warning: + Pattern match(es) are non-exhaustive + In an equation for ‘f’: + Patterns not matched: + MkT3 (MkT2 _) + MkT3 MkT1 + (MkT2 _) MkT3 + MkT1 MkT3 + +pmc001.hs:19:1: warning: + Pattern match(es) are non-exhaustive + In an equation for ‘g’: + Patterns not matched: + MkT3 (MkT2 _) + MkT3 MkT1 + (MkT2 _) MkT3 + MkT1 MkT3 diff --git a/testsuite/tests/pmcheck/should_compile/pmc002.hs b/testsuite/tests/pmcheck/should_compile/pmc002.hs new file mode 100644 index 0000000000..ae823069c5 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/pmc002.hs @@ -0,0 +1,7 @@ +{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-overlapping-patterns #-} + +module PMC002 where + +f :: [a] -> Bool +f [] = True +f x | (_:_) <- x = False -- exhaustive diff --git a/testsuite/tests/pmcheck/should_compile/pmc002.stderr b/testsuite/tests/pmcheck/should_compile/pmc002.stderr new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/pmc002.stderr diff --git a/testsuite/tests/pmcheck/should_compile/pmc003.hs b/testsuite/tests/pmcheck/should_compile/pmc003.hs new file mode 100644 index 0000000000..dd5a8681c7 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/pmc003.hs @@ -0,0 +1,9 @@ +{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-overlapping-patterns #-} + +module PMC003 where + +f :: Bool -> Bool -> () +f _ False = () +f True False = () +f _ _ = () + diff --git a/testsuite/tests/pmcheck/should_compile/pmc003.stderr b/testsuite/tests/pmcheck/should_compile/pmc003.stderr new file mode 100644 index 0000000000..4006b0c042 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/pmc003.stderr @@ -0,0 +1,3 @@ +pmc003.hs:6:1: warning: + Pattern match(es) have inaccessible right hand side + In an equation for ‘f’: f True False = ... diff --git a/testsuite/tests/pmcheck/should_compile/pmc004.hs b/testsuite/tests/pmcheck/should_compile/pmc004.hs new file mode 100644 index 0000000000..90a60c823a --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/pmc004.hs @@ -0,0 +1,16 @@ +{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-overlapping-patterns #-} +{-# LANGUAGE GADTs #-} + +module PMC004 where + +data F a where + F1 :: F Int + F2 :: F Bool + +data G a where + G1 :: G Int + G2 :: G Char + +h :: F a -> G a -> () +h F1 G1 = () +h _ G1 = () diff --git a/testsuite/tests/pmcheck/should_compile/pmc004.stderr b/testsuite/tests/pmcheck/should_compile/pmc004.stderr new file mode 100644 index 0000000000..53f590dd4e --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/pmc004.stderr @@ -0,0 +1,3 @@ +pmc004.hs:15:1: warning: + Pattern match(es) have inaccessible right hand side + In an equation for ‘h’: h _ G1 = ... diff --git a/testsuite/tests/pmcheck/should_compile/pmc005.hs b/testsuite/tests/pmcheck/should_compile/pmc005.hs new file mode 100644 index 0000000000..d05b2d435c --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/pmc005.hs @@ -0,0 +1,12 @@ +{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-overlapping-patterns #-} +{-# LANGUAGE GADTs #-} + +module PMC005 where + +data T a where + TList :: T [a] + TBool :: T Bool + +foo :: T c -> T c -> () +foo TList _ = () +foo _ TList = () diff --git a/testsuite/tests/pmcheck/should_compile/pmc005.stderr b/testsuite/tests/pmcheck/should_compile/pmc005.stderr new file mode 100644 index 0000000000..940dd3a1e9 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/pmc005.stderr @@ -0,0 +1,7 @@ +pmc005.hs:11:1: warning: + Pattern match(es) have inaccessible right hand side + In an equation for ‘foo’: foo _ TList = ... + +pmc005.hs:11:1: warning: + Pattern match(es) are non-exhaustive + In an equation for ‘foo’: Patterns not matched: TBool TBool diff --git a/testsuite/tests/pmcheck/should_compile/pmc006.hs b/testsuite/tests/pmcheck/should_compile/pmc006.hs new file mode 100644 index 0000000000..7099dea23d --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/pmc006.hs @@ -0,0 +1,22 @@ +{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-overlapping-patterns #-} + +module PMC006 where + +len :: [a] -> Int +len xs = case xs of + [] -> 0 + (_:ys) -> case () of + () | (_:_) <- xs -> 1 + len ys + +-- -- we would like these to work too but they don't yet +-- +-- len :: [a] -> Int +-- len [] = 0 +-- len xs = case xs of +-- (_:ys) -> 1 + len ys +-- +-- len :: [a] -> Int +-- len xs = case xs of +-- [] -> 0 +-- ys -> case ys of +-- (_:zs) -> 1 + len zs diff --git a/testsuite/tests/pmcheck/should_compile/pmc006.stderr b/testsuite/tests/pmcheck/should_compile/pmc006.stderr new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/pmc006.stderr diff --git a/testsuite/tests/pmcheck/should_compile/pmc007.hs b/testsuite/tests/pmcheck/should_compile/pmc007.hs new file mode 100644 index 0000000000..301cdbbac2 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/pmc007.hs @@ -0,0 +1,20 @@ +{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-overlapping-patterns #-} +{-# LANGUAGE OverloadedStrings #-} + +module PMC007 where + +-- overloaded +f "ab" = () +f "ac" = () + +-- non-overloaded +g :: String -> () +g "ab" = () +g "ac" = () + +-- non-overloaded due to type inference +h :: String -> () +h s = let s' = s + in case s' of + "ab" -> () + "ac" -> () diff --git a/testsuite/tests/pmcheck/should_compile/pmc007.stderr b/testsuite/tests/pmcheck/should_compile/pmc007.stderr new file mode 100644 index 0000000000..bb011be5aa --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/pmc007.stderr @@ -0,0 +1,24 @@ +pmc007.hs:7:1: warning: + Pattern match(es) are non-exhaustive + In an equation for ‘f’: + Patterns not matched: p where p is not one of {"ac", "ab"} + +pmc007.hs:12:1: warning: + Pattern match(es) are non-exhaustive + In an equation for ‘g’: + Patterns not matched: + ('a':'b':_:_) + ('a':'c':_:_) + ('a':p:_) where p is not one of {'c', 'b'} + ['a'] + ... + +pmc007.hs:18:11: warning: + Pattern match(es) are non-exhaustive + In a case alternative: + Patterns not matched: + ('a':'b':_:_) + ('a':'c':_:_) + ('a':p:_) where p is not one of {'c', 'b'} + ['a'] + ... diff --git a/testsuite/tests/typecheck/should_compile/T5490.stderr b/testsuite/tests/typecheck/should_compile/T5490.stderr new file mode 100644 index 0000000000..7a32e9d7ad --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T5490.stderr @@ -0,0 +1,8 @@ + +T5490.hs:245:15: warning: + Pattern match(es) are redundant + In a case alternative: HDropZero -> ... + +T5490.hs:288:3: warning: + Pattern match(es) are redundant + In a case alternative: _ -> ... |