diff options
author | Sebastian Graf <sebastian.graf@kit.edu> | 2019-05-22 18:46:37 +0200 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2019-06-07 10:21:21 -0400 |
commit | e963beb54a243f011396942d2add644e3f3dd8ae (patch) | |
tree | 169670dd67cafacf288d0cd0fd68b560dd51797f | |
parent | d3915b304f297b8a2534f6abf9c2984837792921 (diff) | |
download | haskell-e963beb54a243f011396942d2add644e3f3dd8ae.tar.gz |
TmOracle: Replace negative term equalities by refutable PmAltCons
The `PmExprEq` business was a huge hack and was at the same time vastly
too powerful and not powerful enough to encode negative term equalities,
i.e. facts of the form "forall y. x ≁ Just y".
This patch introduces the concept of 'refutable shapes': What matters
for the pattern match checker is being able to encode knowledge of the
kind "x can no longer be the literal 5". We encode this knowledge in a
`PmRefutEnv`, mapping a set of newly introduced `PmAltCon`s (which are
just `PmLit`s at the moment) to each variable denoting above
inequalities.
So, say we have `x ≁ 42 ∈ refuts` in the term oracle context and
try to solve an equality like `x ~ 42`. The entry in the refutable
environment will immediately lead to a contradiction.
This machinery renders the whole `PmExprEq` and `ComplexEq` business
unnecessary, getting rid of a lot of (mostly dead) code.
See the Note [Refutable shapes] in TmOracle for a place to start.
Metric Decrease:
T11195
-rw-r--r-- | compiler/basicTypes/NameEnv.hs | 4 | ||||
-rw-r--r-- | compiler/deSugar/Check.hs | 150 | ||||
-rw-r--r-- | compiler/deSugar/DsMonad.hs | 4 | ||||
-rw-r--r-- | compiler/deSugar/PmExpr.hs | 288 | ||||
-rw-r--r-- | compiler/deSugar/PmPpr.hs | 191 | ||||
-rw-r--r-- | compiler/deSugar/TmOracle.hs | 469 | ||||
-rw-r--r-- | compiler/ghc.cabal.in | 1 | ||||
-rw-r--r-- | compiler/typecheck/TcEvidence.hs | 18 | ||||
-rw-r--r-- | compiler/typecheck/TcRnTypes.hs | 4 | ||||
-rw-r--r-- | compiler/utils/ListSetOps.hs | 9 | ||||
-rw-r--r-- | testsuite/tests/pmcheck/should_compile/CyclicSubst.hs | 15 | ||||
-rw-r--r-- | testsuite/tests/pmcheck/should_compile/PmExprVars.hs | 44 | ||||
-rw-r--r-- | testsuite/tests/pmcheck/should_compile/T12949.hs | 16 | ||||
-rw-r--r-- | testsuite/tests/pmcheck/should_compile/all.T | 5 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_compile/T5490.stderr | 4 |
15 files changed, 672 insertions, 550 deletions
diff --git a/compiler/basicTypes/NameEnv.hs b/compiler/basicTypes/NameEnv.hs index 632ea7742e..0b1cf435bc 100644 --- a/compiler/basicTypes/NameEnv.hs +++ b/compiler/basicTypes/NameEnv.hs @@ -25,6 +25,7 @@ module NameEnv ( emptyDNameEnv, lookupDNameEnv, + delFromDNameEnv, mapDNameEnv, alterDNameEnv, -- ** Dependency analysis @@ -147,6 +148,9 @@ emptyDNameEnv = emptyUDFM lookupDNameEnv :: DNameEnv a -> Name -> Maybe a lookupDNameEnv = lookupUDFM +delFromDNameEnv :: DNameEnv a -> Name -> DNameEnv a +delFromDNameEnv = delFromUDFM + mapDNameEnv :: (a -> b) -> DNameEnv a -> DNameEnv b mapDNameEnv = mapUDFM diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs index 4a27d485c0..4147a78ad2 100644 --- a/compiler/deSugar/Check.hs +++ b/compiler/deSugar/Check.hs @@ -25,6 +25,7 @@ module Check ( import GhcPrelude import TmOracle +import PmPpr import Unify( tcMatchTy ) import DynFlags import HsSyn @@ -579,7 +580,7 @@ pmTopNormaliseType_maybe env ty_cs typ pmInitialTmTyCs :: PmM Delta pmInitialTmTyCs = do ty_cs <- liftD getDictsDs - tm_cs <- map toComplex . bagToList <$> liftD getTmCsDs + tm_cs <- bagToList <$> liftD getTmCsDs sat_ty <- tyOracle ty_cs let initTyCs = if sat_ty then ty_cs else emptyBag initTmState = fromMaybe initialTmState (tmOracle initialTmState tm_cs) @@ -627,7 +628,7 @@ that we expect. pmIsSatisfiable :: Delta -- ^ The ambient term and type constraints -- (known to be satisfiable). - -> ComplexEq -- ^ The new term constraint. + -> TmVarCt -- ^ The new term constraint. -> Bag EvVar -- ^ The new type constraints. -> [Type] -- ^ The strict argument types. -> PmM (Maybe Delta) @@ -653,7 +654,7 @@ pmIsSatisfiable amb_cs new_tm_c new_ty_cs strict_arg_tys = do tmTyCsAreSatisfiable :: Delta -- ^ The ambient term and type constraints -- (known to be satisfiable). - -> ComplexEq -- ^ The new term constraint. + -> TmVarCt -- ^ The new term constraint. -> Bag EvVar -- ^ The new type constraints. -> PmM (Maybe Delta) -- ^ @'Just' delta@ if the constraints (@delta@) are @@ -1463,7 +1464,7 @@ pmPatType PmFake = pmPatType truePattern data InhabitationCandidate = InhabitationCandidate { ic_val_abs :: ValAbs - , ic_tm_ct :: ComplexEq + , ic_tm_ct :: TmVarCt , ic_ty_cs :: Bag EvVar , ic_strict_arg_tys :: [Type] } @@ -1660,7 +1661,7 @@ mkOneConFull x con = do strict_arg_tys = filterByList arg_is_banged arg_tys' return $ InhabitationCandidate { ic_val_abs = con_abs - , ic_tm_ct = (PmExprVar (idName x), vaToPmExpr con_abs) + , ic_tm_ct = TVC x (vaToPmExpr con_abs) , ic_ty_cs = listToBag evvars , ic_strict_arg_tys = strict_arg_tys } @@ -1678,21 +1679,15 @@ mkGuard pv e = do | PmExprOther {} <- expr -> pure PmFake | otherwise -> pure (PmGrd pv expr) --- | Create a term equality of the form: `(False ~ (x ~ lit))` -mkNegEq :: Id -> PmLit -> ComplexEq -mkNegEq x l = (falsePmExpr, PmExprVar (idName x) `PmExprEq` PmExprLit l) -{-# INLINE mkNegEq #-} - -- | Create a term equality of the form: `(x ~ lit)` -mkPosEq :: Id -> PmLit -> ComplexEq -mkPosEq x l = (PmExprVar (idName x), PmExprLit l) +mkPosEq :: Id -> PmLit -> TmVarCt +mkPosEq x l = TVC x (PmExprLit l) {-# INLINE mkPosEq #-} -- | Create a term equality of the form: `(x ~ x)` -- (always discharged by the term oracle) -mkIdEq :: Id -> ComplexEq -mkIdEq x = (PmExprVar name, PmExprVar name) - where name = idName x +mkIdEq :: Id -> TmVarCt +mkIdEq x = TVC x (PmExprVar (idName x)) {-# INLINE mkIdEq #-} -- | Generate a variable pattern of a given type @@ -2059,8 +2054,7 @@ pmcheckHd :: Pattern -> PatVec -> [PatVec] -> ValAbs -> ValVec -- Var pmcheckHd (PmVar x) ps guards va (ValVec vva delta) - | Just tm_state <- solveOneEq (delta_tm_cs delta) - (PmExprVar (idName x), vaToPmExpr va) + | Just tm_state <- solveOneEq (delta_tm_cs delta) (TVC x (vaToPmExpr va)) = ucon va <$> pmcheckI ps guards (ValVec vva (delta {delta_tm_cs = tm_state})) | otherwise = return mempty @@ -2122,7 +2116,8 @@ pmcheckHd (p@(PmLit l)) ps guards (PmVar x) (ValVec vva delta) ValVec vva (delta {delta_tm_cs = tm_state}) Nothing -> return mempty where - us | Just tm_state <- solveOneEq (delta_tm_cs delta) (mkNegEq x l) + -- See Note [Refutable shapes] in TmOracle + us | Just tm_state <- addSolveRefutableAltCon (delta_tm_cs delta) x (PmAltLit l) = [ValVec (PmNLit x [l] : vva) (delta { delta_tm_cs = tm_state })] | otherwise = [] @@ -2142,7 +2137,8 @@ pmcheckHd (p@(PmLit l)) ps guards (ValVec vva (delta { delta_tm_cs = tm_state })) | otherwise = return non_matched where - us | Just tm_state <- solveOneEq (delta_tm_cs delta) (mkNegEq x l) + -- See Note [Refutable shapes] in TmOracle + us | Just tm_state <- addSolveRefutableAltCon (delta_tm_cs delta) x (PmAltLit l) = [ValVec (PmNLit x (l:lits) : vva) (delta { delta_tm_cs = tm_state })] | otherwise = [] @@ -2407,22 +2403,22 @@ these constraints. genCaseTmCs2 :: Maybe (LHsExpr GhcTc) -- Scrutinee -> [Pat GhcTc] -- LHS (should have length 1) -> [Id] -- MatchVars (should have length 1) - -> DsM (Bag SimpleEq) + -> DsM (Bag TmVarCt) genCaseTmCs2 Nothing _ _ = return emptyBag genCaseTmCs2 (Just scr) [p] [var] = do fam_insts <- dsGetFamInstEnvs [e] <- map vaToPmExpr . coercePatVec <$> translatePat fam_insts p let scr_e = lhsExprToPmExpr scr - return $ listToBag [(var, e), (var, scr_e)] + return $ listToBag [(TVC var e), (TVC 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 GhcTc) -> [Id] -> Bag SimpleEq +genCaseTmCs1 :: Maybe (LHsExpr GhcTc) -> [Id] -> Bag TmVarCt genCaseTmCs1 Nothing _ = emptyBag -genCaseTmCs1 (Just scr) [var] = unitBag (var, lhsExprToPmExpr scr) +genCaseTmCs1 (Just scr) [var] = unitBag (TVC var (lhsExprToPmExpr scr)) genCaseTmCs1 _ _ = panic "genCaseTmCs1: HsCase" {- Note [Literals in PmPat] @@ -2484,21 +2480,15 @@ isAnyPmCheckEnabled dflags (DsMatchContext kind _loc) instance Outputable ValVec where ppr (ValVec vva delta) - = let (residual_eqs, subst) = wrapUpTmState (delta_tm_cs delta) - vector = substInValAbs subst vva - in ppr_uncovered (vector, residual_eqs) + = let (subst, refuts) = wrapUpTmState (delta_tm_cs delta) + vector = substInValAbs subst vva + in pprUncovered (vector, refuts) -- | Apply a term substitution to a value vector abstraction. All VAs are -- transformed to PmExpr (used only before pretty printing). -substInValAbs :: PmVarEnv -> [ValAbs] -> [PmExpr] +substInValAbs :: TmVarCtEnv -> [ValAbs] -> [PmExpr] substInValAbs subst = map (exprDeepLookup subst . vaToPmExpr) --- | 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) - -- | Issue all the warnings (coverage, exhaustiveness, inaccessibility) dsPmWarn :: DynFlags -> DsMatchContext -> PmResult -> DsM () dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result @@ -2538,10 +2528,11 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result maxPatterns = maxUncoveredPatterns dflags -- Print a single clause (for redundant/with-inaccessible-rhs) - pprEqn q txt = pp_context True ctx (text txt) $ \f -> ppr_eqn f kind q + pprEqn q txt = pprContext True ctx (text txt) $ \f -> + f (pprPats kind (map unLoc q)) -- Print several clauses (for uncovered clauses) - pprEqns qs = pp_context False ctx (text "are non-exhaustive") $ \_ -> + pprEqns qs = pprContext False ctx (text "are non-exhaustive") $ \_ -> case qs of -- See #11245 [ValVec [] _] -> text "Guards do not cover entire pattern space" @@ -2552,7 +2543,7 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result -- Print a type-annotated wildcard (for non-exhaustive `EmptyCase`s for -- which we only know the type and have no inhabitants at hand) - warnEmptyCase ty = pp_context False ctx (text "are non-exhaustive") $ \_ -> + warnEmptyCase ty = pprContext False ctx (text "are non-exhaustive") $ \_ -> hang (text "Patterns not matched:") 4 (underscore <+> dcolon <+> ppr ty) {- Note [Inaccessible warnings for record updates] @@ -2624,8 +2615,8 @@ exhaustiveWarningFlag (StmtCtxt {}) = Nothing -- Don't warn about incomplete pat -- incomplete -- True <==> singular -pp_context :: Bool -> DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc -pp_context singular (DsMatchContext kind _loc) msg rest_of_msg_fun +pprContext :: Bool -> DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc +pprContext singular (DsMatchContext kind _loc) msg rest_of_msg_fun = vcat [text txt <+> msg, sep [ text "In" <+> ppr_match <> char ':' , nest 4 (rest_of_msg_fun pref)]] @@ -2639,87 +2630,10 @@ pp_context singular (DsMatchContext kind _loc) msg rest_of_msg_fun -> (pprMatchContext kind, \ pp -> ppr fun <+> pp) _ -> (pprMatchContext kind, \ pp -> pp) -ppr_pats :: HsMatchContext Name -> [Pat GhcTc] -> SDoc -ppr_pats kind pats +pprPats :: HsMatchContext Name -> [Pat GhcTc] -> SDoc +pprPats kind pats = sep [sep (map ppr pats), matchSeparator kind, text "..."] -ppr_eqn :: (SDoc -> SDoc) -> HsMatchContext Name -> [LPat GhcTc] -> SDoc -ppr_eqn prefixF kind eqn = prefixF (ppr_pats kind (map unLoc eqn)) - -ppr_constraint :: (SDoc,[PmLit]) -> SDoc -ppr_constraint (var, lits) = var <+> text "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 $ - text "where" <+> vcat (map ppr_constraint cs) - where - sdoc_vec = mapM pprPmExprWithParens expr_vec - (vec,cs) = runPmPprM sdoc_vec (filterComplex complex) - -{- Note [Representation of Term Equalities] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -In the paper, term constraints always take the form (x ~ e). Of course, a more -general constraint of the form (e1 ~ e1) can always be transformed to an -equivalent set of the former constraints, by introducing a fresh, intermediate -variable: { y ~ e1, y ~ e1 }. Yet, implementing this representation gave rise -to #11160 (incredibly bad performance for literal pattern matching). Two are -the main sources of this problem (the actual problem is how these two interact -with each other): - -1. Pattern matching on literals generates twice as many constraints as needed. - Consider the following (tests/ghci/should_run/ghcirun004): - - foo :: Int -> Int - foo 1 = 0 - ... - foo 5000 = 4999 - - The covered and uncovered set *should* look like: - U0 = { x |> {} } - - C1 = { 1 |> { x ~ 1 } } - U1 = { x |> { False ~ (x ~ 1) } } - ... - C10 = { 10 |> { False ~ (x ~ 1), .., False ~ (x ~ 9), x ~ 10 } } - U10 = { x |> { False ~ (x ~ 1), .., False ~ (x ~ 9), False ~ (x ~ 10) } } - ... - - If we replace { False ~ (x ~ 1) } with { y ~ False, y ~ (x ~ 1) } - we get twice as many constraints. Also note that half of them are just the - substitution [x |-> False]. - -2. The term oracle (`tmOracle` in deSugar/TmOracle) uses equalities of the form - (x ~ e) as substitutions [x |-> e]. More specifically, function - `extendSubstAndSolve` applies such substitutions in the residual constraints - and partitions them in the affected and non-affected ones, which are the new - worklist. Essentially, this gives quadradic behaviour on the number of the - residual constraints. (This would not be the case if the term oracle used - mutable variables but, since we use it to handle disjunctions on value set - abstractions (`Union` case), we chose a pure, incremental interface). - -Now the problem becomes apparent (e.g. for clause 300): - * Set U300 contains 300 substituting constraints [y_i |-> False] and 300 - constraints that we know that will not reduce (stay in the worklist). - * To check for consistency, we apply the substituting constraints ONE BY ONE - (since `tmOracle` is called incrementally, it does not have all of them - available at once). Hence, we go through the (non-progressing) constraints - over and over, achieving over-quadradic behaviour. - -If instead we allow constraints of the form (e ~ e), - * All uncovered sets Ui contain no substituting constraints and i - non-progressing constraints of the form (False ~ (x ~ lit)) so the oracle - behaves linearly. - * All covered sets Ci contain exactly (i-1) non-progressing constraints and - a single substituting constraint. So the term oracle goes through the - constraints only once. - -The performance improvement becomes even more important when more arguments are -involved. --} - -- Debugging Infrastructre tracePm :: String -> SDoc -> PmM () @@ -2757,3 +2671,5 @@ pprValAbs ps = hang (text "ValAbs:") 2 pprValVecDebug :: ValVec -> SDoc pprValVecDebug (ValVec vas _d) = text "ValVec" <+> parens (pprValAbs vas) + -- <not a haddock> $$ ppr (delta_tm_cs _d) + -- <not a haddock> $$ ppr (delta_ty_cs _d) diff --git a/compiler/deSugar/DsMonad.hs b/compiler/deSugar/DsMonad.hs index 8e3021fd8a..9534b4e20b 100644 --- a/compiler/deSugar/DsMonad.hs +++ b/compiler/deSugar/DsMonad.hs @@ -396,11 +396,11 @@ 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 :: DsM (Bag TmVarCt) getTmCsDs = do { env <- getLclEnv; return (dsl_tm_cs env) } -- | Add in-scope term constraints (pm check) -addTmCsDs :: Bag SimpleEq -> DsM a -> DsM a +addTmCsDs :: Bag TmVarCt -> DsM a -> DsM a addTmCsDs tm_cs = updLclEnv (\env -> env { dsl_tm_cs = unionBags tm_cs (dsl_tm_cs env) }) diff --git a/compiler/deSugar/PmExpr.hs b/compiler/deSugar/PmExpr.hs index bd0e12e850..3697dd8cc1 100644 --- a/compiler/deSugar/PmExpr.hs +++ b/compiler/deSugar/PmExpr.hs @@ -6,12 +6,11 @@ Haskell expressions (as used by the pattern matching checker) and utilities. {-# LANGUAGE CPP #-} {-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} module PmExpr ( - PmExpr(..), PmLit(..), SimpleEq, ComplexEq, toComplex, eqPmLit, - truePmExpr, falsePmExpr, isTruePmExpr, isFalsePmExpr, isNotPmExprOther, - lhsExprToPmExpr, hsExprToPmExpr, substComplexEq, filterComplex, - pprPmExprWithParens, runPmPprM + PmExpr(..), PmLit(..), PmAltCon(..), TmVarCt(..), + eqPmLit, isNotPmExprOther, lhsExprToPmExpr, hsExprToPmExpr ) where #include "HsVersions.h" @@ -23,19 +22,14 @@ import FastString (FastString, unpackFS) import HsSyn import Id import Name -import NameSet import DataCon import ConLike +import TcEvidence (isErasableHsWrapper) import TcType (isStringTy) import TysWiredIn import Outputable -import Util import SrcLoc -import Data.Maybe (mapMaybe) -import Data.List (groupBy, sortBy, nubBy) -import Control.Monad.Trans.State.Lazy - {- %************************************************************************ %* * @@ -61,7 +55,6 @@ refer to variables that are otherwise substituted away. data PmExpr = PmExprVar Name | PmExprCon ConLike [PmExpr] | PmExprLit PmLit - | PmExprEq PmExpr PmExpr -- Syntactic equality | PmExprOther (HsExpr GhcTc) -- Note [PmExprOther in PmExpr] @@ -79,6 +72,16 @@ eqPmLit (PmOLit b1 l1) (PmOLit b2 l2) = b1 == b2 && l1 == l2 -- See Note [Undecidable Equality for Overloaded Literals] eqPmLit _ _ = False +-- | Represents a match against a literal. We mostly use it to to encode shapes +-- for a variable that immediately lead to a refutation. +-- +-- See Note [Refutable shapes] in TmOracle. Really similar to 'CoreSyn.AltCon'. +newtype PmAltCon = PmAltLit PmLit + deriving Outputable + +instance Eq PmAltCon where + PmAltLit l1 == PmAltLit l2 = eqPmLit l1 l2 + {- Note [Undecidable Equality for Overloaded Literals] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Equality on overloaded literals is undecidable in the general case. Consider @@ -145,24 +148,11 @@ impact of this is the following: appearance of the warnings and is, in practice safe. -} -nubPmLit :: [PmLit] -> [PmLit] -nubPmLit = nubBy eqPmLit +-- | A term constraint. @TVC x e@ encodes that @x@ is equal to @e@. +data TmVarCt = TVC !Id !PmExpr --- | Term equalities -type SimpleEq = (Id, PmExpr) -- We always use this orientation -type ComplexEq = (PmExpr, PmExpr) - --- | Lift a `SimpleEq` to a `ComplexEq` -toComplex :: SimpleEq -> ComplexEq -toComplex (x,e) = (PmExprVar (idName x), e) - --- | Expression `True' -truePmExpr :: PmExpr -truePmExpr = mkPmExprData trueDataCon [] - --- | Expression `False' -falsePmExpr :: PmExpr -falsePmExpr = mkPmExprData falseDataCon [] +instance Outputable TmVarCt where + ppr (TVC x e) = ppr x <+> char '~' <+> ppr e -- ---------------------------------------------------------------------------- -- ** Predicates on PmExpr @@ -172,66 +162,6 @@ 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 == RealDataCon trueDataCon -isTruePmExpr _other_expr = False - --- | Check whether a PmExpr is syntactically equal to term `False'. -isFalsePmExpr :: PmExpr -> Bool -isFalsePmExpr (PmExprCon c []) = c == RealDataCon falseDataCon -isFalsePmExpr _other_expr = False - --- | Check whether a PmExpr is syntactically e -isNilPmExpr :: PmExpr -> Bool -isNilPmExpr (PmExprCon c _) = c == RealDataCon 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 :: Name -> 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 :: Name -> 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 @@ -240,8 +170,20 @@ lhsExprToPmExpr (dL->L _ e) = hsExprToPmExpr e hsExprToPmExpr :: HsExpr GhcTc -> PmExpr +-- Translating HsVar to flexible meta variables in the unification problem is +-- morally wrong, but it does the right thing for now. +-- In contrast to the situation in pattern matches, HsVars in expression syntax +-- are object language variables, most similar to rigid variables with an +-- unknown solution. The correct way would be to handle them through PmExprOther +-- and identify syntactically equal occurrences by the same rigid meta variable, +-- but we can't compare the wrapped HsExpr for equality. Hence we are stuck with +-- this hack. hsExprToPmExpr (HsVar _ x) = PmExprVar (idName (unLoc x)) -hsExprToPmExpr (HsConLikeOut _ c) = PmExprVar (conLikeName c) + +-- Translating HsConLikeOut to a flexible meta variable is misleading. +-- For an example why, consider `consAreRigid` in +-- `testsuite/tests/pmcheck/should_compile/PmExprVars.hs`. +-- hsExprToPmExpr (HsConLikeOut _ c) = PmExprVar (conLikeName c) -- Desugar literal strings as a list of characters. For other literal values, -- keep it as it is. @@ -294,7 +236,12 @@ hsExprToPmExpr (HsTickPragma _ _ _ _ e) = lhsExprToPmExpr e hsExprToPmExpr (HsSCC _ _ _ e) = lhsExprToPmExpr e hsExprToPmExpr (HsCoreAnn _ _ _ e) = lhsExprToPmExpr e hsExprToPmExpr (ExprWithTySig _ e _) = lhsExprToPmExpr e -hsExprToPmExpr (HsWrap _ _ e) = hsExprToPmExpr e +hsExprToPmExpr (HsWrap _ w e) + -- A dictionary application spoils e and we have no choice but to return an + -- PmExprOther. Same thing for other stuff that can't erased in the + -- compilation process. Otherwise this bites in + -- teststuite/tests/pmcheck/should_compile/PmExprVars.hs. + | isErasableHsWrapper w = hsExprToPmExpr e hsExprToPmExpr e = PmExprOther e -- the rest are not handled by the oracle stringExprToList :: SourceText -> FastString -> PmExpr @@ -312,155 +259,22 @@ stringExprToList src s = foldr cons nil (map charToPmExpr (unpackFS s)) %************************************************************************ -} -{- 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 = (Name, (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 text ["p","q","r","s","t"] ++ - [ text ('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, emptyNameSet) - - is_used (x,(name, lits)) - | elemNameSet x used = Just (name, lits) - | otherwise = Nothing - -type PmPprM a = State ([PmNegLitCt], NameSet) a --- (the first part of the state is read only. make it a reader?) - -addUsed :: Name -> PmPprM () -addUsed x = modify (\(negated, used) -> (negated, extendNameSet used x)) - -checkNegation :: Name -> 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 (RealDataCon c) es) - | isTupleDataCon c - || isConsDataCon c || null es = False - | otherwise = True -needsParens (PmExprCon (PatSynCon _) es) = not (null es) - -pprPmExprWithParens :: PmExpr -> PmPprM SDoc -pprPmExprWithParens expr - | needsParens expr = parens <$> pprPmExpr expr - | otherwise = pprPmExpr expr - -pprPmExprCon :: ConLike -> [PmExpr] -> PmPprM SDoc -pprPmExprCon (RealDataCon con) args - | isTupleDataCon con = mkTuple <$> mapM pprPmExpr args - | isConsDataCon con = pretty_list - where - mkTuple :: [SDoc] -> SDoc - mkTuple = parens . 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, RealDataCon nilDataCon == c - = ASSERT(null es) [x,y] - | PmExprCon c es <- y, RealDataCon consDataCon == c - = x : list_elements es - | otherwise = [x,y] - list_elements list = pprPanic "list_elements:" (ppr list) -pprPmExprCon cl args - | conLikeIsInfix cl = case args of - [x, y] -> do x' <- pprPmExprWithParens x - y' <- pprPmExprWithParens y - return (x' <+> ppr cl <+> y') - -- can it be infix but have more than two arguments? - list -> pprPanic "pprPmExprCon:" (ppr list) - | null args = return (ppr cl) - | otherwise = do args' <- mapM pprPmExprWithParens args - return (fsep (ppr cl : args')) - 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) [] + ppr = go (0 :: Int) + where + go _ (PmExprLit l) = ppr l + go _ (PmExprVar v) = ppr v + go _ (PmExprOther e) = angleBrackets (ppr e) + go _ (PmExprCon (RealDataCon dc) args) + | isTupleDataCon dc = parens $ comma_sep $ map ppr args + | dc == consDataCon = brackets $ comma_sep $ map ppr (list_cells args) + where + comma_sep = fsep . punctuate comma + list_cells (hd:tl) = hd : list_cells tl + list_cells _ = [] + go prec (PmExprCon cl args) + = cparen (null args || prec > 0) (hcat (ppr cl:map (go 1) args)) diff --git a/compiler/deSugar/PmPpr.hs b/compiler/deSugar/PmPpr.hs new file mode 100644 index 0000000000..06b60a6806 --- /dev/null +++ b/compiler/deSugar/PmPpr.hs @@ -0,0 +1,191 @@ +{-# LANGUAGE CPP #-} + +-- | Provides factilities for pretty-printing 'PmExpr's in a way approriate for +-- user facing pattern match warnings. +module PmPpr ( + pprUncovered + ) where + +#include "HsVersions.h" + +import GhcPrelude + +import Name +import NameEnv +import NameSet +import UniqDFM +import UniqSet +import ConLike +import DataCon +import TysWiredIn +import Outputable +import Control.Monad.Trans.State.Strict +import Maybes +import Util + +import TmOracle + +-- | Pretty-print the guts of an uncovered value vector abstraction, i.e., its +-- components and refutable shapes associated to any mentioned variables. +-- +-- Example for @([Just p, q], [p :-> [3,4], q :-> [0,5]]): +-- +-- @ +-- (Just p) q +-- where p is not one of {3, 4} +-- q is not one of {0, 5} +-- @ +pprUncovered :: ([PmExpr], PmRefutEnv) -> SDoc +pprUncovered (expr_vec, refuts) + | null cs = fsep vec -- there are no literal constraints + | otherwise = hang (fsep vec) 4 $ + text "where" <+> vcat (map pprRefutableShapes cs) + where + sdoc_vec = mapM pprPmExprWithParens expr_vec + (vec,cs) = runPmPpr sdoc_vec (prettifyRefuts refuts) + +-- | Output refutable shapes of a variable in the form of @var is not one of {2, +-- Nothing, 3}@. +pprRefutableShapes :: (SDoc,[PmAltCon]) -> SDoc +pprRefutableShapes (var, alts) + = var <+> text "is not one of" <+> braces (pprWithCommas ppr_alt alts) + where + ppr_alt (PmAltLit lit) = ppr lit + +{- 1. Literals +~~~~~~~~~~~~~~ +Starting with a function definition like: + + f :: Int -> Bool + f 5 = True + f 6 = True + +The uncovered set looks like: + { var |> var /= 5, var /= 6 } + +Yet, we would like to print this nicely as follows: + x , where x not one of {5,6} + +Since these variables will be shown to the programmer, we give them better names +(t1, t2, ..) in 'prettifyRefuts', hence the SDoc in 'PrettyPmRefutEnv'. + +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 precise. +-} + +-- | A 'PmRefutEnv' with pretty names for the occuring variables. +type PrettyPmRefutEnv = DNameEnv (SDoc, [PmAltCon]) + +-- | Assigns pretty names to constraint variables in the domain of the given +-- 'PmRefutEnv'. +prettifyRefuts :: PmRefutEnv -> PrettyPmRefutEnv +prettifyRefuts = listToUDFM . zipWith rename nameList . udfmToList + where + rename new (old, lits) = (old, (new, lits)) + -- Try nice names p,q,r,s,t before using the (ugly) t_i + nameList :: [SDoc] + nameList = map text ["p","q","r","s","t"] ++ + [ text ('t':show u) | u <- [(0 :: Int)..] ] + +type PmPprM a = State (PrettyPmRefutEnv, NameSet) a +-- (the first part of the state is read only. make it a reader?) + +runPmPpr :: PmPprM a -> PrettyPmRefutEnv -> (a, [(SDoc,[PmAltCon])]) +runPmPpr m lit_env = (result, mapMaybe is_used (udfmToList lit_env)) + where + (result, (_lit_env, used)) = runState m (lit_env, emptyNameSet) + + is_used (k,v) + | elemUniqSet_Directly k used = Just v + | otherwise = Nothing + +addUsed :: Name -> PmPprM () +addUsed x = modify (\(negated, used) -> (negated, extendNameSet used x)) + +checkNegation :: Name -> PmPprM (Maybe SDoc) -- the clean name if it is negated +checkNegation x = do + negated <- gets fst + return $ case lookupDNameEnv negated x 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 (PmExprOther _) = return underscore -- don't show + +needsParens :: PmExpr -> Bool +needsParens (PmExprVar {}) = False +needsParens (PmExprLit l) = isNegatedPmLit l +needsParens (PmExprOther {}) = False -- will become a wildcard +needsParens (PmExprCon (RealDataCon c) es) + | isTupleDataCon c + || isConsDataCon c || null es = False + | otherwise = True +needsParens (PmExprCon (PatSynCon _) es) = not (null es) + +pprPmExprWithParens :: PmExpr -> PmPprM SDoc +pprPmExprWithParens expr + | needsParens expr = parens <$> pprPmExpr expr + | otherwise = pprPmExpr expr + +pprPmExprCon :: ConLike -> [PmExpr] -> PmPprM SDoc +pprPmExprCon (RealDataCon con) args + | isTupleDataCon con = mkTuple <$> mapM pprPmExpr args + | isConsDataCon con = pretty_list + where + mkTuple :: [SDoc] -> SDoc + mkTuple = parens . 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, RealDataCon nilDataCon == c + = ASSERT(null es) [x,y] + | PmExprCon c es <- y, RealDataCon consDataCon == c + = x : list_elements es + | otherwise = [x,y] + list_elements list = pprPanic "list_elements:" (ppr list) +pprPmExprCon cl args + | conLikeIsInfix cl = case args of + [x, y] -> do x' <- pprPmExprWithParens x + y' <- pprPmExprWithParens y + return (x' <+> ppr cl <+> y') + -- can it be infix but have more than two arguments? + list -> pprPanic "pprPmExprCon:" (ppr list) + | null args = return (ppr cl) + | otherwise = do args' <- mapM pprPmExprWithParens args + return (fsep (ppr cl : args')) + +-- | Check whether a literal is negated +isNegatedPmLit :: PmLit -> Bool +isNegatedPmLit (PmOLit b _) = b +isNegatedPmLit _other_lit = False + +-- | Check whether a PmExpr is syntactically e +isNilPmExpr :: PmExpr -> Bool +isNilPmExpr (PmExprCon c _) = c == RealDataCon nilDataCon +isNilPmExpr _other_expr = False + +-- | Check if a DataCon is (:). +isConsDataCon :: DataCon -> Bool +isConsDataCon con = consDataCon == con diff --git a/compiler/deSugar/TmOracle.hs b/compiler/deSugar/TmOracle.hs index 87e5f0a268..db3ce6d770 100644 --- a/compiler/deSugar/TmOracle.hs +++ b/compiler/deSugar/TmOracle.hs @@ -1,23 +1,27 @@ {- Author: George Karachalias <george.karachalias@cs.kuleuven.be> - -The term equality oracle. The main export of the module is function `tmOracle'. -} {-# LANGUAGE CPP, MultiWayIf #-} +-- | The term equality oracle. The main export of the module are the functions +-- 'tmOracle', 'solveOneEq' and 'addSolveRefutableAltCon'. +-- +-- If you are looking for an oracle that can solve type-level constraints, look +-- at 'TcSimplify.tcCheckSatisfiability'. module TmOracle ( -- re-exported from PmExpr - PmExpr(..), PmLit(..), SimpleEq, ComplexEq, PmVarEnv, falsePmExpr, - eqPmLit, filterComplex, isNotPmExprOther, runPmPprM, lhsExprToPmExpr, - hsExprToPmExpr, pprPmExprWithParens, + PmExpr(..), PmLit(..), PmAltCon(..), TmVarCt(..), TmVarCtEnv, + PmRefutEnv, eqPmLit, isNotPmExprOther, lhsExprToPmExpr, hsExprToPmExpr, -- the term oracle - tmOracle, TmState, initialTmState, solveOneEq, extendSubst, canDiverge, + tmOracle, TmState, initialTmState, wrapUpTmState, solveOneEq, + extendSubst, canDiverge, isRigid, + addSolveRefutableAltCon, lookupRefutableAltCons, -- misc. - toComplex, exprDeepLookup, pmLitType, flattenPmVarEnv + exprDeepLookup, pmLitType ) where #include "HsVersions.h" @@ -26,16 +30,19 @@ import GhcPrelude import PmExpr +import Util import Id import Name import Type import HsLit import TcHsSyn import MonadUtils -import Util +import ListSetOps (insertNoDup, unionLists) +import Maybes import Outputable - import NameEnv +import UniqFM +import UniqDFM {- %************************************************************************ @@ -45,202 +52,261 @@ import NameEnv %************************************************************************ -} --- | The type of substitutions. -type PmVarEnv = NameEnv PmExpr +-- | Pretty much a @['TmVarCt']@ association list where the domain is 'Name' +-- instead of 'Id'. This is the type of 'tm_pos', where we store solutions for +-- rigid pattern match variables. +type TmVarCtEnv = NameEnv PmExpr + +-- | An environment assigning shapes to variables that immediately lead to a +-- refutation. So, if this maps @x :-> [3]@, then trying to solve a 'TmVarCt' +-- like @x ~ 3@ immediately leads to a contradiction. +-- Determinism is important since we use this for warning messages in +-- 'PmPpr.pprUncovered'. We don't do the same for 'TmVarCtEnv', so that is a plain +-- 'NameEnv'. +-- +-- See also Note [Refutable shapes] in TmOracle. +type PmRefutEnv = DNameEnv [PmAltCon] + +-- | The state of the term oracle. Tracks all term-level facts of the form "x is +-- @True@" ('tm_pos') and "x is not @5@" ('tm_neg'). +-- +-- Subject to Note [The Pos/Neg invariant]. +data TmState = TmS + { tm_pos :: !TmVarCtEnv + -- ^ A substitution with solutions we extend with every step and return as a + -- result. The substitution is in /triangular form/: It might map @x@ to @y@ + -- where @y@ itself occurs in the domain of 'tm_pos', rendering lookup + -- non-idempotent. This means that 'varDeepLookup' potentially has to walk + -- along a chain of var-to-var mappings until we find the solution but has the + -- advantage that when we update the solution for @y@ above, we automatically + -- update the solution for @x@ in a union-find-like fashion. + -- Invariant: Only maps to other variables ('PmExprVar') or to WHNFs + -- ('PmExprLit', 'PmExprCon'). Ergo, never maps to a 'PmExprOther'. + , tm_neg :: !PmRefutEnv + -- ^ Maps each variable @x@ to a list of 'PmAltCon's that @x@ definitely + -- cannot match. Example, @x :-> [3, 4]@ means that @x@ cannot match a literal + -- 3 or 4. Should we later solve @x@ to a variable @y@ + -- ('extendSubstAndSolve'), we merge the refutable shapes of @x@ into those of + -- @y@. See also Note [The Pos/Neg invariant]. + } + +{- Note [The Pos/Neg invariant] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Invariant: In any 'TmState', The domains of 'tm_pos' and 'tm_neg' are disjoint. + +For example, it would make no sense to say both + tm_pos = [...x :-> 3 ...] + tm_neg = [...x :-> [4,42]... ] +The positive information is strictly more informative than the negative. + +Suppose we are adding the (positive) fact @x :-> e@ to 'tm_pos'. Then we must +delete any binding for @x@ from 'tm_neg', to uphold the invariant. + +But there is more! Suppose we are adding @x :-> y@ to 'tm_pos', and 'tm_neg' +contains @x :-> cs, y :-> ds@. Then we want to update 'tm_neg' to +@y :-> (cs ++ ds)@, to make use of the negative information we have about @x@. +-} + +instance Outputable TmState where + ppr state = braces (fsep (punctuate comma (pos ++ neg))) + where + pos = map pos_eq (nonDetUFMToList (tm_pos state)) + neg = map neg_eq (udfmToList (tm_neg state)) + pos_eq (l, r) = ppr l <+> char '~' <+> ppr r + neg_eq (l, r) = ppr l <+> char '≁' <+> ppr r + +-- | Initial state of the oracle. +initialTmState :: TmState +initialTmState = TmS emptyNameEnv emptyDNameEnv + +-- | Wrap up the term oracle's state once solving is complete. Return the +-- flattened 'tm_pos' and 'tm_neg'. +wrapUpTmState :: TmState -> (TmVarCtEnv, PmRefutEnv) +wrapUpTmState solver_state + = (flattenTmVarCtEnv (tm_pos solver_state), tm_neg solver_state) --- | 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) +-- | Flatten the triangular subsitution. +flattenTmVarCtEnv :: TmVarCtEnv -> TmVarCtEnv +flattenTmVarCtEnv env = mapNameEnv (exprDeepLookup env) env -- | Check whether a constraint (x ~ BOT) can succeed, -- given the resulting state of the term oracle. canDiverge :: Name -> TmState -> Bool -canDiverge x (standby, (_unhandled, env)) +canDiverge x TmS{ tm_pos = pos, tm_neg = neg } -- 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 + -- constraint x ~ BOT to be satisfiable. That's the case when we haven't found + -- a solution (i.e. some equivalent literal or constructor) for it yet. + | (_, PmExprVar y) <- varDeepLookup pos x -- seems not forced + -- Even if we don't have a solution yet, it might be involved in a negative + -- constraint, in which case we must already have evaluated it earlier. + , Nothing <- lookupDNameEnv neg y + = True + -- Variable x is already in WHNF or we know some refutable shape, so the + -- constraint is non-satisfiable | otherwise = False - where - isForcedByEq :: Name -> 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 :: Name -> 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 = mapNameEnv (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, emptyNameEnv)) - --- | Solve a complex equality (top-level). -solveOneEq :: TmState -> ComplexEq -> Maybe TmState -solveOneEq solver_env@(_,(_,env)) complex - = solveComplexEq solver_env -- do the actual *merging* with existing state - $ simplifyComplexEq -- simplify as much as you can - $ applySubstComplexEq env complex -- replace everything we already know - --- | Solve a complex equality. --- Nothing => definitely unsatisfiable --- Just tms => I have added the complex equality and added --- it to the tmstate; the result may or may not be --- satisfiable -solveComplexEq :: TmState -> ComplexEq -> Maybe TmState -solveComplexEq solver_state@(standby, (unhandled, env)) eq@(e1, e2) = case eq of +-- | Check whether the equality @x ~ e@ leads to a refutation. Make sure that +-- @x@ and @e@ are completely substituted before! +isRefutable :: Name -> PmExpr -> PmRefutEnv -> Bool +isRefutable x e env + = fromMaybe False $ elem <$> exprToAlt e <*> lookupDNameEnv env x + +-- | Solve an equality (top-level). +solveOneEq :: TmState -> TmVarCt -> Maybe TmState +solveOneEq solver_env (TVC x e) = unify solver_env (PmExprVar (idName x), e) + +exprToAlt :: PmExpr -> Maybe PmAltCon +exprToAlt (PmExprLit l) = Just (PmAltLit l) +exprToAlt _ = Nothing + +-- | Record that a particular 'Id' can't take the shape of a 'PmAltCon' in the +-- 'TmState' and return @Nothing@ if that leads to a contradiction. +addSolveRefutableAltCon :: TmState -> Id -> PmAltCon -> Maybe TmState +addSolveRefutableAltCon original@TmS{ tm_pos = pos, tm_neg = neg } x nalt + = case exprToAlt e of + -- We have to take care to preserve Note [The Pos/Neg invariant] + Nothing -> Just extended -- Not solved yet + Just alt -- We have a solution + | alt == nalt -> Nothing -- ... which is contradictory + | otherwise -> Just original -- ... which is compatible, rendering the + where -- refutation redundant + (y, e) = varDeepLookup pos (idName x) + extended = original { tm_neg = neg' } + neg' = alterDNameEnv (delNulls (insertNoDup nalt)) neg y + +-- | When updating 'tm_neg', we want to delete any 'null' entries. This adapter +-- intends to provide a suitable interface for 'alterDNameEnv'. +delNulls :: ([a] -> [a]) -> Maybe [a] -> Maybe [a] +delNulls f mb_entry + | ret@(_:_) <- f (fromMaybe [] mb_entry) = Just ret + | otherwise = Nothing + +-- | Return all 'PmAltCon' shapes that are impossible for 'Id' to take, i.e. +-- would immediately lead to a refutation by the term oracle. +lookupRefutableAltCons :: Id -> TmState -> [PmAltCon] +lookupRefutableAltCons x TmS { tm_neg = neg } + = fromMaybe [] (lookupDNameEnv neg (idName x)) + +-- | Is the given variable /rigid/ (i.e., we have a solution for it) or +-- /flexible/ (i.e., no solution)? Returns the solution if /rigid/. A +-- semantically helpful alias for 'lookupNameEnv'. +isRigid :: TmState -> Name -> Maybe PmExpr +isRigid TmS{ tm_pos = pos } x = lookupNameEnv pos x + +-- | @isFlexible tms = isNothing . 'isRigid' tms@ +isFlexible :: TmState -> Name -> Bool +isFlexible tms = isNothing . isRigid tms + +-- | Try to unify two 'PmExpr's and record the gained knowledge in the +-- 'TmState'. +-- +-- Returns @Nothing@ when there's a contradiction. Returns @Just tms@ +-- when the constraint was compatible with prior facts, in which case @tms@ has +-- integrated the knowledge from the equality constraint. +unify :: TmState -> (PmExpr, PmExpr) -> Maybe TmState +unify tms eq@(e1, e2) = case eq of -- We cannot do a thing about these cases - (PmExprOther _,_) -> Just (standby, (True, env)) - (_,PmExprOther _) -> Just (standby, (True, env)) + (PmExprOther _,_) -> boring + (_,PmExprOther _) -> boring (PmExprLit l1, PmExprLit l2) -> case eqPmLit l1 l2 of -- See Note [Undecidable Equality for Overloaded Literals] - True -> Just solver_state - False -> Nothing + True -> boring + False -> unsat (PmExprCon c1 ts1, PmExprCon c2 ts2) - | c1 == c2 -> foldlM solveComplexEq solver_state (zip ts1 ts2) - | otherwise -> Nothing - (PmExprCon _ [], PmExprEq t1 t2) - | isTruePmExpr e1 -> solveComplexEq solver_state (t1, t2) - | isFalsePmExpr e1 -> Just (eq:standby, (unhandled, env)) - (PmExprEq t1 t2, PmExprCon _ []) - | isTruePmExpr e2 -> solveComplexEq solver_state (t1, t2) - | isFalsePmExpr e2 -> Just (eq:standby, (unhandled, env)) + | c1 == c2 -> foldlM unify tms (zip ts1 ts2) + | otherwise -> unsat (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)) - - _ -> WARN( True, text "solveComplexEq: Catch all" <+> ppr eq ) - Just (standby, (True, env)) -- I HATE CATCH-ALLS - --- | Extend the substitution and solve the (possibly updated) constraints. -extendSubstAndSolve :: Name -> PmExpr -> TmState -> Maybe TmState -extendSubstAndSolve x e (standby, (unhandled, env)) - = foldlM solveComplexEq new_incr_state (map simplifyComplexEq changed) + | x == y -> boring + + -- It's important to handle both rigid cases first, otherwise we get cyclic + -- substitutions. Cf. 'extendSubstAndSolve' and + -- @testsuite/tests/pmcheck/should_compile/CyclicSubst.hs@. + (PmExprVar x, _) + | Just e1' <- isRigid tms x -> unify tms (e1', e2) + (_, PmExprVar y) + | Just e2' <- isRigid tms y -> unify tms (e1, e2') + (PmExprVar x, PmExprVar y) -> Just (equate x y tms) + (PmExprVar x, _) -> trySolve x e2 tms + (_, PmExprVar y) -> trySolve y e1 tms + + _ -> WARN( True, text "unify: Catch all" <+> ppr eq) + boring -- I HATE CATCH-ALLS + where + boring = Just tms + unsat = Nothing + +-- | Merges the equivalence classes of @x@ and @y@ by extending the substitution +-- with @x :-> y@. +-- Preconditions: @x /= y@ and both @x@ and @y@ are flexible (cf. +-- 'isFlexible'/'isRigid'). +equate :: Name -> Name -> TmState -> TmState +equate x y tms@TmS{ tm_pos = pos, tm_neg = neg } + = ASSERT( x /= y ) + ASSERT( isFlexible tms x ) + ASSERT( isFlexible tms y ) + tms' 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. Careful about performance: - -- See Note [Representation of Term Equalities] in deSugar/Check.hs - (changed, unchanged) = partitionWith (substComplexEq x e) standby - new_incr_state = (unchanged, (unhandled, extendNameEnv env x e)) + pos' = extendNameEnv pos x (PmExprVar y) + -- Be careful to uphold Note [The Pos/Neg invariant] by merging the refuts + -- of x into those of y + nalts = fromMaybe [] (lookupDNameEnv neg x) + neg' = alterDNameEnv (delNulls (unionLists nalts)) neg y + `delFromDNameEnv` x + tms' = TmS { tm_pos = pos', tm_neg = neg' } + +-- | Extend the substitution with a mapping @x: -> e@ if compatible with +-- refutable shapes of @x@ and its solution, reject (@Nothing@) otherwise. +-- +-- Precondition: @x@ is flexible (cf. 'isFlexible'/'isRigid'). +-- Precondition: @e@ is a 'PmExprCon' or 'PmExprLit' +trySolve:: Name -> PmExpr -> TmState -> Maybe TmState +trySolve x e _tms@TmS{ tm_pos = pos, tm_neg = neg } + | ASSERT( isFlexible _tms x ) + ASSERT( _is_whnf e ) + isRefutable x e neg + = Nothing + | otherwise + = Just (TmS (extendNameEnv pos x e) (delFromDNameEnv neg x)) + where + _is_whnf PmExprCon{} = True + _is_whnf PmExprLit{} = True + _is_whnf _ = False -- | When we know that a variable is fresh, we do not actually have to -- check whether anything changes, we know that nothing does. Hence, --- `extendSubst` simply extends the substitution, unlike what --- `extendSubstAndSolve` does. +-- @extendSubst@ simply extends the substitution, unlike what +-- 'extendSubstAndSolve' does. extendSubst :: Id -> PmExpr -> TmState -> TmState -extendSubst y e (standby, (unhandled, env)) +extendSubst y e solver_state@TmS{ tm_pos = pos } | isNotPmExprOther simpl_e - = (standby, (unhandled, extendNameEnv env x simpl_e)) - | otherwise = (standby, (True, env)) + = solver_state { tm_pos = extendNameEnv pos x simpl_e } + | otherwise = solver_state where x = idName y - simpl_e = fst $ simplifyPmExpr $ exprDeepLookup env e - --- | 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 - -- See Note [Undecidable Equality for Overloaded Literals] - True -> (truePmExpr, True) - False -> (falsePmExpr, True) - - -- 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 to a simple equality. -applySubstComplexEq :: PmVarEnv -> ComplexEq -> ComplexEq -applySubstComplexEq env (e1,e2) = (exprDeepLookup env e1, exprDeepLookup env e2) - --- | Apply an (un-flattened) substitution to a variable. -varDeepLookup :: PmVarEnv -> Name -> PmExpr -varDeepLookup env x - | Just e <- lookupNameEnv env x = exprDeepLookup env e -- go deeper - | otherwise = PmExprVar x -- terminal + simpl_e = exprDeepLookup pos e + +-- | Apply an (un-flattened) substitution to a variable and return its +-- representative in the triangular substitution @env@ and the completely +-- substituted expression. The latter may just be the representative wrapped +-- with 'PmExprVar' if we haven't found a solution for it yet. +varDeepLookup :: TmVarCtEnv -> Name -> (Name, PmExpr) +varDeepLookup env x = case lookupNameEnv env x of + Just (PmExprVar y) -> varDeepLookup env y + Just e -> (x, exprDeepLookup env e) -- go deeper + Nothing -> (x, PmExprVar x) -- terminal {-# INLINE varDeepLookup #-} -- | Apply an (un-flattened) substitution to an expression. -exprDeepLookup :: PmVarEnv -> PmExpr -> PmExpr -exprDeepLookup env (PmExprVar x) = varDeepLookup env x +exprDeepLookup :: TmVarCtEnv -> PmExpr -> PmExpr +exprDeepLookup env (PmExprVar x) = snd (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 -> [ComplexEq] -> Maybe TmState +tmOracle :: TmState -> [TmVarCt] -> Maybe TmState tmOracle tm_state eqs = foldlM solveOneEq tm_state eqs -- | Type of a PmLit @@ -248,18 +314,49 @@ 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: +{- Note [Refutable shapes] +~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Consider a pattern match like + + foo x + | 0 <- x = 42 + | 0 <- x = 43 + | 1 <- x = 44 + | otherwise = 45 + +This will result in the following initial matching problem: + + PatVec: x (0 <- x) + ValVec: $tm_y + +Where the first line is the pattern vector and the second line is the value +vector abstraction. When we handle the first pattern guard in Check, it will be +desugared to a match of the form + + PatVec: x 0 + ValVec: $tm_y x + +In LitVar, this will split the value vector abstraction for `x` into a positive +`PmLit 0` and a negative `PmLit x [0]` value abstraction. While the former is +immediately matched against the pattern vector, the latter (vector value +abstraction `~[0] $tm_y`) is completely uncovered by the clause. + +`pmcheck` proceeds by *discarding* the the value vector abstraction involving +the guard to accomodate for the desugaring. But this also discards the valuable +information that `x` certainly is not the literal 0! Consequently, we wouldn't +be able to report the second clause as redundant. - * Equalities of the form (True ~ (e1 ~ e2)) are transformed to just - (e1 ~ e2) and then treated recursively. +That's a typical example of why we need the term oracle, and in this specific +case, the ability to encode that `x` certainly is not the literal 0. Now the +term oracle can immediately refute the constraint `x ~ 0` generated by the +second clause and report the clause as redundant. After the third clause, the +set of such *refutable* literals is again extended to `[0, 1]`. - * 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. +In general, we want to store a set of refutable shapes (`PmAltCon`) for each +variable. That's the purpose of the `PmRefutEnv`. `addSolveRefutableAltCon` will +add such a refutable mapping to the `PmRefutEnv` in the term oracles state and +check if causes any immediate contradiction. Whenever we record a solution in +the substitution via `extendSubstAndSolve`, the refutable environment is checked +for any matching refutable `PmAltCon`. -} diff --git a/compiler/ghc.cabal.in b/compiler/ghc.cabal.in index e2d789b172..e8e6bf7317 100644 --- a/compiler/ghc.cabal.in +++ b/compiler/ghc.cabal.in @@ -327,6 +327,7 @@ Library MkCore PprCore PmExpr + PmPpr TmOracle Check Coverage diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs index 72aed23505..eb65d1e093 100644 --- a/compiler/typecheck/TcEvidence.hs +++ b/compiler/typecheck/TcEvidence.hs @@ -8,7 +8,8 @@ module TcEvidence ( HsWrapper(..), (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, mkWpLams, mkWpLet, mkWpCastN, mkWpCastR, collectHsWrapBinders, - mkWpFun, mkWpFuns, idHsWrapper, isIdHsWrapper, pprHsWrapper, + mkWpFun, mkWpFuns, idHsWrapper, isIdHsWrapper, isErasableHsWrapper, + pprHsWrapper, -- Evidence bindings TcEvBinds(..), EvBindsVar(..), @@ -355,6 +356,21 @@ isIdHsWrapper :: HsWrapper -> Bool isIdHsWrapper WpHole = True isIdHsWrapper _ = False +-- | Is the wrapper erasable, i.e., will not affect runtime semantics? +isErasableHsWrapper :: HsWrapper -> Bool +isErasableHsWrapper = go + where + go WpHole = True + go (WpCompose wrap1 wrap2) = go wrap1 && go wrap2 + -- not so sure about WpFun. But it eta-expands, so... + go WpFun{} = False + go WpCast{} = True + go WpEvLam{} = False -- case in point + go WpEvApp{} = False + go WpTyLam{} = True + go WpTyApp{} = True + go WpLet{} = False + collectHsWrapBinders :: HsWrapper -> ([Var], HsWrapper) -- Collect the outer lambda binders of a HsWrapper, -- stopping as soon as you get to a non-lambda binder diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs index bc307568f8..8957014036 100644 --- a/compiler/typecheck/TcRnTypes.hs +++ b/compiler/typecheck/TcRnTypes.hs @@ -391,7 +391,7 @@ data DsLclEnv = DsLclEnv { -- These two fields are augmented as we walk inwards, -- through each patttern match in turn dsl_dicts :: Bag EvVar, -- Constraints from GADT pattern-matching - dsl_tm_cs :: Bag SimpleEq, -- Constraints form term-level pattern matching + dsl_tm_cs :: Bag TmVarCt, -- Constraints form term-level pattern matching dsl_pm_iter :: IORef Int -- Number of iterations for pmcheck so far -- We fail if this gets too big @@ -1020,7 +1020,7 @@ splice. In particular it is not set when the splice is renamed or typechecked. 'RunSplice' is needed to provide a reference where 'addModFinalizer' can insert the finalizer (see Note [Delaying modFinalizers in untyped splices]), and 'addModFinalizer' runs when doing Q things. Therefore, It doesn't make sense to -set 'RunSplice' when renaming or typechecking the splice, where 'Splice', +set 'RunSplice' when renaming or typechecking the splice, where 'Splice', 'Brack' or 'Comp' are used instead. -} diff --git a/compiler/utils/ListSetOps.hs b/compiler/utils/ListSetOps.hs index 1a134d5dc8..8a6e07d84a 100644 --- a/compiler/utils/ListSetOps.hs +++ b/compiler/utils/ListSetOps.hs @@ -14,7 +14,7 @@ module ListSetOps ( Assoc, assoc, assocMaybe, assocUsing, assocDefault, assocDefaultUsing, -- Duplicate handling - hasNoDups, removeDups, findDupsEq, + hasNoDups, removeDups, findDupsEq, insertNoDup, equivClasses, -- Indexing @@ -169,3 +169,10 @@ findDupsEq _ [] = [] findDupsEq eq (x:xs) | null eq_xs = findDupsEq eq xs | otherwise = (x :| eq_xs) : findDupsEq eq neq_xs where (eq_xs, neq_xs) = partition (eq x) xs + +-- | \( O(n) \). @'insertNoDup' x xs@ treats @xs@ as a set, inserting @x@ only +-- when an equal element couldn't be found in @xs@. +insertNoDup :: (Eq a) => a -> [a] -> [a] +insertNoDup x set + | elem x set = set + | otherwise = x:set diff --git a/testsuite/tests/pmcheck/should_compile/CyclicSubst.hs b/testsuite/tests/pmcheck/should_compile/CyclicSubst.hs new file mode 100644 index 0000000000..fde022c5cb --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/CyclicSubst.hs @@ -0,0 +1,15 @@ +-- | The following match demonstrates why we need to detect cyclic solutions +-- when extending 'TmOracle.tm_pos'. +-- +-- TLDR; solving @x :-> y@ where @x@ is the representative of @y@'s equivalence +-- class can easily lead to a cycle in the substitution. +module CyclicSubst where + +-- | The match is translated to @b | a <- b@, the initial unification variable +-- is @a@ (for some reason). VarVar will assign @b :-> a@ in the match of @a@ +-- against @b@ (vars occuring in a pattern are flexible). The @PmGrd a b@ is +-- desugared as a match of @$pm_x@ against @a@, where @$pm_x :-> b@, which is +-- stored as @$pm_x :-> a@ due to the previous solution. Now, VarVar will +-- assign @a :-> $pm_x@, causing a cycle. +foo :: Int -> Int +foo a@b = a + b diff --git a/testsuite/tests/pmcheck/should_compile/PmExprVars.hs b/testsuite/tests/pmcheck/should_compile/PmExprVars.hs new file mode 100644 index 0000000000..7b17cd5b66 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/PmExprVars.hs @@ -0,0 +1,44 @@ +module PmExprVars where + +-- | Demonstrates why we can't lower constructors as flexible meta variables. +-- If we did, we'd get a warning that cases 1 and 2 were redundant, implying +-- cases 0 and 3 are not. Arguably this might be better than not warning at +-- all, but it's very surprising having to supply the third case but not the +-- first two cases. And it's probably buggy somwhere else. Delete this when we +-- detect that all but the last case is redundant. +consAreRigid :: Int +consAreRigid = case False of + False -> case False of + False -> 0 + True -> 1 + True -> case False of + False -> 2 + True -> 3 + +data D a = A | B + +class C a where + d :: D a + +instance C Int where + d = A + +instance C Bool where + d = B + +-- | Demonstrates why we can't translate arbitrary 'HsVar' +-- occurrences as 'PmExprVar's (i.e., meta variables). If we did, the following +-- would warn that the cases 1 and 2 were redundant, which is clearly wrong +-- (case 1 is the only match). This is an artifact of translating from the +-- non-desugared 'HsExpr'. If we were to implement 'hsExprToPmExpr' in terms of +-- 'CoreExpr', we'd see the dictionary application and all would be well. The +-- solution is to look into the outer 'HsWrap' and determine whether we apply +-- or abstract over any evidence variables. +dictVarsAreTypeIndexed:: Int +dictVarsAreTypeIndexed = case d :: D Int of + A -> case d :: D Bool of + A -> 0 + B -> 1 + B -> case d :: D Bool of + A -> 2 + B -> 3 diff --git a/testsuite/tests/pmcheck/should_compile/T12949.hs b/testsuite/tests/pmcheck/should_compile/T12949.hs new file mode 100644 index 0000000000..90fe024067 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T12949.hs @@ -0,0 +1,16 @@ +{-# LANGUAGE ScopedTypeVariables #-} +module T12949 where + +class Foo a where + foo :: Maybe a + +data Result a b = Neither | This a | That b | Both a b + +q :: forall a b . (Foo a, Foo b) => Result a b +q = case foo :: Maybe a of + Nothing -> case foo :: Maybe b of + Nothing -> Neither + Just c -> That c + Just i -> case foo :: Maybe b of + Nothing -> This i + Just c -> Both i c diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T index e04f2cf07c..5fe7d9edd1 100644 --- a/testsuite/tests/pmcheck/should_compile/all.T +++ b/testsuite/tests/pmcheck/should_compile/all.T @@ -94,8 +94,13 @@ test('pmc007', [], compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns']) test('T11245', [], compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns']) +test('T12949', [], compile, ['-fwarn-overlapping-patterns']) test('T12957', [], compile, ['-fwarn-overlapping-patterns']) test('T12957a', [], compile, ['-fwarn-overlapping-patterns']) +test('PmExprVars', [], compile, + ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns']) +test('CyclicSubst', [], compile, + ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns']) # EmptyCase test('T10746', [], compile, diff --git a/testsuite/tests/typecheck/should_compile/T5490.stderr b/testsuite/tests/typecheck/should_compile/T5490.stderr index 3cf5b3e866..93ae57550f 100644 --- a/testsuite/tests/typecheck/should_compile/T5490.stderr +++ b/testsuite/tests/typecheck/should_compile/T5490.stderr @@ -1,8 +1,4 @@ -T5490.hs:246:5: warning: [-Woverlapping-patterns (in -Wdefault)] - Pattern match is redundant - In a case alternative: HDropZero -> ... - T5490.hs:295:5: warning: [-Woverlapping-patterns (in -Wdefault)] Pattern match is redundant In a case alternative: _ -> ... |