[Git][ghc/ghc][wip/derived-refactor] 3 commits: Checkpoint. About to never report WRW errors
Richard Eisenberg
gitlab at gitlab.haskell.org
Thu Jun 25 13:14:18 UTC 2020
Richard Eisenberg pushed to branch wip/derived-refactor at Glasgow Haskell Compiler / GHC
Commits:
e8581f1b by Richard Eisenberg at 2020-06-20T22:14:24+01:00
Checkpoint. About to never report WRW errors
- - - - -
ef71e5ce by Richard Eisenberg at 2020-06-25T11:38:37+01:00
Suppress errors using RewriterSet
- - - - -
5d3804ae by Richard Eisenberg at 2020-06-25T14:13:43+01:00
More propagation of rewriters
- - - - -
16 changed files:
- compiler/GHC/Core/TyCo/FVs.hs
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/Tc/Errors.hs
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Solver/Flatten.hs
- compiler/GHC/Tc/Solver/Interact.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- testsuite/tests/partial-sigs/should_fail/T10999.stderr
- testsuite/tests/typecheck/should_fail/T12785b.stderr
- testsuite/tests/typecheck/should_fail/T15648.stderr
- testsuite/tests/typecheck/should_fail/T8450.stderr
Changes:
=====================================
compiler/GHC/Core/TyCo/FVs.hs
=====================================
@@ -266,9 +266,6 @@ runTyCoVars :: Endo TyCoVarSet -> TyCoVarSet
{-# INLINE runTyCoVars #-}
runTyCoVars f = appEndo f emptyVarSet
-noView :: Type -> Maybe Type
-noView _ = Nothing
-
{- *********************************************************************
* *
Deep free variables
@@ -379,8 +376,8 @@ shallowTcvFolder = TyCoFolder { tcf_view = noView
********************************************************************* -}
-{- Note [Finding free coercion varibles]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Finding free coercion variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Here we are only interested in the free /coercion/ variables.
We can achieve this through a slightly differnet TyCo folder.
@@ -389,6 +386,7 @@ Notice that we look deeply, into kinds.
See #14880.
-}
+-- See Note [Finding free coercion variables]
coVarsOfType :: Type -> CoVarSet
coVarsOfTypes :: [Type] -> CoVarSet
coVarsOfCo :: Coercion -> CoVarSet
@@ -429,7 +427,6 @@ deepCoVarFolder = TyCoFolder { tcf_view = noView
-- See Note [CoercionHoles and coercion free variables]
-- in GHC.Core.TyCo.Rep
-
{- *********************************************************************
* *
Closing over kinds
@@ -981,4 +978,3 @@ tyCoVarsOfTypeWellScoped = scopedSort . tyCoVarsOfTypeList
-- | Get the free vars of types in scoped order
tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
tyCoVarsOfTypesWellScoped = scopedSort . tyCoVarsOfTypesList
-
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -62,7 +62,7 @@ module GHC.Core.TyCo.Rep (
pickLR,
-- ** Analyzing types
- TyCoFolder(..), foldTyCo,
+ TyCoFolder(..), foldTyCo, noView,
-- * Sizes
typeSize, coercionSize, provSize
@@ -87,6 +87,7 @@ import GHC.Core.TyCon
import GHC.Core.Coercion.Axiom
-- others
+import GHC.Types.Unique ( Uniquable(..) )
import GHC.Types.Basic ( LeftOrRight(..), pickLR )
import GHC.Utils.Outputable
import GHC.Data.FastString
@@ -1567,6 +1568,9 @@ instance Data.Data CoercionHole where
instance Outputable CoercionHole where
ppr (CoercionHole { ch_co_var = cv }) = braces (ppr cv)
+instance Uniquable CoercionHole where
+ getUnique (CoercionHole { ch_co_var = v }) = getUnique v
+
instance Outputable BlockSubstFlag where
ppr YesBlockSubst = text "YesBlockSubst"
ppr NoBlockSubst = text "NoBlockSubst"
@@ -1775,7 +1779,7 @@ We were also worried about
`extendVarSet` tv
Here deep_fvs and deep_tcf are mutually recursive, unlike fvs and tcf.
-But, amazingly, we get good code here too. GHC is careful not to makr
+But, amazingly, we get good code here too. GHC is careful not to mark
TyCoFolder data constructor for deep_tcf as a loop breaker, so the
record selections still cancel. And eta expansion still happens too.
-}
@@ -1784,8 +1788,8 @@ data TyCoFolder env a
= TyCoFolder
{ tcf_view :: Type -> Maybe Type -- Optional "view" function
-- E.g. expand synonyms
- , tcf_tyvar :: env -> TyVar -> a
- , tcf_covar :: env -> CoVar -> a
+ , tcf_tyvar :: env -> TyVar -> a -- Does not automatically recur
+ , tcf_covar :: env -> CoVar -> a -- into kinds of variables
, tcf_hole :: env -> CoercionHole -> a
-- ^ What to do with coercion holes.
-- See Note [Coercion holes] in GHC.Core.TyCo.Rep.
@@ -1854,6 +1858,10 @@ foldTyCo (TyCoFolder { tcf_view = view
go_prov env (ProofIrrelProv co) = go_co env co
go_prov _ (PluginProv _) = mempty
+-- | A view function that looks through nothing.
+noView :: Type -> Maybe Type
+noView _ = Nothing
+
{- *********************************************************************
* *
typeSize, coercionSize
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -83,7 +83,7 @@ module GHC.Core.Type (
-- ** Analyzing types
TyCoMapper(..), mapTyCo, mapTyCoX,
- TyCoFolder(..), foldTyCo,
+ TyCoFolder(..), foldTyCo, noView,
-- (Newtypes)
newTyConInstRhs,
=====================================
compiler/GHC/Tc/Errors.hs
=====================================
@@ -22,8 +22,7 @@ import GHC.Tc.Utils.Monad
import GHC.Tc.Types.Constraint
import GHC.Core.Predicate
import GHC.Tc.Utils.TcMType
-import GHC.Tc.Utils.Unify( occCheckForErrors, MetaTyVarUpdateResult(..), swapOverTyVars
- , canSolveByUnification )
+import GHC.Tc.Utils.Unify( occCheckForErrors, MetaTyVarUpdateResult(..) )
import GHC.Tc.Utils.Env( tcInitTidyEnv )
import GHC.Tc.Utils.TcType
import GHC.Tc.Types.Origin
@@ -51,7 +50,6 @@ import GHC.Types.Id
import GHC.Types.Var
import GHC.Types.Var.Set
import GHC.Types.Var.Env
-import GHC.Types.Unique.Set
import GHC.Types.Name.Set
import GHC.Data.Bag
import GHC.Utils.Error ( ErrMsg, errDoc, pprLocErrMsg )
@@ -236,8 +234,7 @@ report_unsolved type_errors expr_holes
-- See #15539 and c.f. setting ic_status
-- in GHC.Tc.Solver.setImplicationStatus
, cec_warn_redundant = warn_redundant
- , cec_binds = binds_var
- , cec_already_reported = emptyUniqSet }
+ , cec_binds = binds_var }
; tc_lvl <- getTcLevel
; reportWanteds err_ctxt tc_lvl wanted
@@ -345,8 +342,6 @@ data ReportErrCtxt
-- so create bindings if need be, but
-- don't issue any more errors/warnings
-- See Note [Suppressing error messages]
- , cec_already_reported :: UniqSet Unique
- -- See Note [Avoid reporting duplicates]
}
instance Outputable ReportErrCtxt where
@@ -531,66 +526,47 @@ This only matters in instance declarations..
-- | A predicate with its arising location; used to encapsulate a constraint
-- that will give rise to a warning.
data ErrorItem
- = EI { ei_pred :: PredType -- report about this
+ = EI { ei_pred :: PredType -- report about this
-- The ei_pred field will never be an unboxed equality with
- -- a (casted) tyvar on the right; these are reoriented in mkErrorItem,
- -- so that the filtering in e.g. reportWanteds can be simpler
- , ei_type :: Type -- produce evidence of this type
- -- see Note [Evidence types]
- , ei_evdest :: Maybe TcEvDest -- for Wanteds, where to put evidence
- , ei_flavour :: CtFlavour
- , ei_loc :: CtLoc
- , ei_unique :: Unique
- -- for deduplication; see Note [Avoid reporting duplicates]
+ -- a (casted) tyvar on the right; this is guaranteed by the solver
+ , ei_evdest :: Maybe TcEvDest -- for Wanteds, where to put evidence
+ , ei_flavour :: CtFlavour
+ , ei_loc :: CtLoc
+ , ei_suppress :: Bool -- Suppress because of Note [Wanteds rewrite Wanteds]
+ -- in GHC.Tc.Constraint
}
instance Outputable ErrorItem where
- ppr (EI { ei_pred = pred
- , ei_evdest = m_evdest
- , ei_flavour = flav })
- = ppr flav <+> pp_dest m_evdest <+> ppr pred
+ ppr (EI { ei_pred = pred
+ , ei_evdest = m_evdest
+ , ei_flavour = flav
+ , ei_suppress = supp })
+ = pp_supp <+> ppr flav <+> pp_dest m_evdest <+> ppr pred
where
pp_dest Nothing = empty
pp_dest (Just ev) = ppr ev <+> dcolon
+ pp_supp = if supp then text "suppress:" else empty
+
-- | Makes an error item based on the predicate-at-birth of the provided
-- constraint. This should be rewritten w.r.t. givens before reported.
-mkErrorItem :: Ct -> ErrorItem
-mkErrorItem ct = EI { ei_pred = tyvar_first pred
- , ei_type = ctPred ct
- , ei_evdest = m_evdest
- , ei_flavour = ctFlavour ct
- , ei_loc = loc
- , ei_unique = unique }
- where
- loc = ctLoc ct
- (m_evdest, pred, unique)
- | CtWanted { ctev_dest = dest
- , ctev_report_as = report_as
- , ctev_pred = ct_pred } <- ctEvidence ct
- , (u, p) <- ctPredToReport dest ct_pred report_as
- = (Just dest, p, u)
-
- | otherwise
- = (Nothing, ctPred ct, ctUnique ct)
-
- -- We reorient any tyvar equalities to put the tyvar first; this
- -- allows fewer cases when choosing how to treat errors. Forgetting
- -- to do this causes mischaracterization of errors.
- tyvar_first pred
- | Just (r, ty1, ty2) <- getEqPredTys_maybe pred
- , Just (tv2, co2) <- getCastedTyVar_maybe ty2
- = let swapped_pred = mkPrimEqPredRole r (mkTyVarTy tv2)
- (ty1 `mkCastTy` mkSymCo co2)
- in
- case getCastedTyVar_maybe ty1 of
- -- tyvar originally on right; non-tyvar originally on left: swap
- Nothing -> swapped_pred
- Just (tv1, _)
- | swapOverTyVars tv1 tv2 -> swapped_pred
- | otherwise -> pred
- | otherwise
- = pred
+mkErrorItem :: Ct -> TcM ErrorItem
+mkErrorItem ct
+ = do { let loc = ctLoc ct
+ flav = ctFlavour ct
+
+ ; (suppress, m_evdest) <- case ctEvidence ct of
+ CtGiven {} -> return (False, Nothing)
+ CtWanted { ctev_rewriters = rewriters, ctev_dest = dest }
+ -> do { supp <- anyUnfilledCoercionHoles rewriters
+ ; return (supp, Just dest) }
+ CtDerived {} -> return (False, Nothing)
+
+ ; return $ EI { ei_pred = ctPred ct
+ , ei_evdest = m_evdest
+ , ei_flavour = flav
+ , ei_loc = loc
+ , ei_suppress = suppress }}
{- "RAE"
tidyErrorItem :: TidyEnv -> ErrorItem -> ErrorItem
@@ -607,10 +583,7 @@ errorItemEqRel = predTypeEqRel . ei_pred
reportWanteds :: ReportErrCtxt -> TcLevel -> WantedConstraints -> TcM ()
reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics
, wc_holes = holes })
- = do { traceTc "reportWanteds 1" (vcat [ text "Simples =" <+> ppr simples
- , text "Suppress =" <+> ppr (cec_suppress ctxt)
- , text "tidy_items =" <+> ppr tidy_items
- , text "tidy_holes =" <+> ppr tidy_holes ])
+ = do {
{- "RAE"
-- rewrite all the errors with respect to the givens
; let givens = errCtxtGivens ctxt
@@ -629,6 +602,14 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics
; traceTc "reportWanteds 2" (vcat [ text "tidy_items =" <+> ppr tidy_items
, text "tidy_holes =" <+> ppr tidy_holes ])
-}
+
+ ; tidy_items <- mapM mkErrorItem tidy_cts
+ ; traceTc "reportWanteds 1" (vcat [ text "Simples =" <+> ppr simples
+ , text "Suppress =" <+> ppr (cec_suppress ctxt)
+ , text "tidy_cts =" <+> ppr tidy_cts
+ , text "tidy_items =" <+> ppr tidy_items
+ , text "tidy_holes =" <+> ppr tidy_holes ])
+
-- First, deal with any out-of-scope errors:
; let (out_of_scope, other_holes) = partition isOutOfScopeHole tidy_holes
-- don't suppress out-of-scope errors
@@ -646,8 +627,7 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics
-- holes never suppress
-- See Note [Suppressing confusing errors]
- ; dflags <- getDynFlags
- ; let (suppressed_items, items0) = partition (suppress dflags) tidy_items
+ ; let (suppressed_items, items0) = partition suppress tidy_items
; traceTc "reportWanteds suppressed:" (ppr suppressed_items)
; (ctxt1, items1) <- tryReporters ctxt_for_insols report1 items0
@@ -663,13 +643,11 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics
-- to report unsolved Derived goals as errors
-- See Note [Do not report derived but soluble errors]
- ; let inner_ctxt = ctxt2 { cec_already_reported = cec_already_reported ctxt3 }
+ ; mapBagM_ (reportImplic ctxt2) implics
-- NB ctxt2: don't suppress inner insolubles if there's only a
-- wanted insoluble here; but do suppress inner insolubles
-- if there's a *given* insoluble here (= inaccessible code)
- ; mapBagM_ (reportImplic inner_ctxt) implics
-
-- Only now, if there are no errors, do we report suppressed ones
-- See Note [Suppressing confusing errors]
-- We don't need to update the context further because of the
@@ -679,30 +657,12 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics
; MASSERT2( null more_leftovers, ppr more_leftovers ) } }
where
env = cec_tidy ctxt
- tidy_items = bagToList (mapBag (mkErrorItem . tidyCt env) simples)
+ tidy_cts = bagToList (mapBag (tidyCt env) simples)
tidy_holes = bagToList (mapBag (tidyHole env) holes)
-- See Note [Suppressing confusing errors]
- suppress :: DynFlags -> ErrorItem -> Bool
- suppress dflags item@(EI { ei_pred = pred })
- | badCoercionHole pred
- = True
-
- -- See Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical;
- -- point (4c)
- | Just (_, ty1, ty2) <- getEqPredTys_maybe pred
- , Just tv1 <- getTyVar_maybe ty1
- , canSolveByUnification tc_lvl tv1 ty2
- , MTVU_OK () <- occCheckForErrors dflags tv1 ty2
- -- this last line checks for e.g. impredicative situations; we don't
- -- want to suppress an error if the problem is impredicativity
- = True
-
- | is_ww_fundep_item item
- = True
-
- | otherwise
- = False
+ suppress :: ErrorItem -> Bool
+ suppress item = is_ww_fundep_item item
-- report1: ones that should *not* be suppressed by
-- an insoluble somewhere else in the tree
@@ -734,8 +694,7 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics
-- report3: suppressed errors should be reported as categorized by either report1
-- or report2.
- report3 = [ ("wanted/wanted fundeps", is_ww_fundep, True, mkGroupReporter mkEqErr)
- , ("Blocked eqs", is_equality, True, mkGroupReporter mkBlockedEqErr) ]
+ report3 = [ ("wanted/wanted fundeps", is_ww_fundep, True, mkGroupReporter mkEqErr) ]
-- rigid_nom_eq, rigid_nom_tv_eq,
is_dict, is_equality, is_ip, is_irred :: ErrorItem -> Pred -> Bool
@@ -828,12 +787,9 @@ isTyFun_maybe ty = case tcSplitTyConApp_maybe ty of
Certain errors we might encounter are potentially confusing to users.
If there are any other errors to report, at all, we want to suppress these.
-Which errors:
+Which errors (right now, only 1, but this may grow):
-1) Errors which are blocked by a coercion hole. This is described
- in point (4) of Note [Equalities with incompatible kinds] in Tc.Solver.Canonical.
-
-2) Errors which arise from the interaction of two Wanted fun-dep constraints.
+ Errors which arise from the interaction of two Wanted fun-dep constraints.
Example:
class C a b | a -> b where
@@ -867,27 +823,6 @@ We use the `suppress` function within reportWanteds to filter out these two
cases, then report all other errors. Lastly, we return to these suppressed
ones and report them only if there have been no errors so far.
-Note [Avoid reporting duplicates]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-It would be embarrassing to report two identical errors to the user. We
-avoid doing so by logging a Unique associated with every error, in the
-cec_already_reported field of a ReportErrCtxt. These Uniques come from:
-
- * For Givens: it's the Unique on the ctev_evar storing the Given evidence.
-
- * For Wanteds with CtReportAsSame: it's the Unique associated with the
- TcEvDest.
-
- * For Wanteds with CtReportAsOther: it's the Unique in the CtReportAsOther,
- which in turn comes from the TcEvDest of the originating Wanted, as placed
- there in updateReportAs.
-
-We still must be sure to process all errors, including duplicates, because
-of the possibility of -fdefer-type-errors; each duplicate may carry its own
-evidence (in the case of several constraints sharing the same CtReportAsOther).
-But when an error appears already in the cec_already_reported, we suppress
-the user-visible error report.
-
-}
@@ -1089,12 +1024,11 @@ maybeReportError ctxt items err
| cec_suppress ctxt -- Some worse error has occurred;
= return () -- so suppress this error/warning
- | any ((`elementOfUniqSet` cec_already_reported ctxt) . ei_unique) items
+ | all ei_suppress items -- if they're all to be suppressed, report nothing
+ -- if at least one is not suppressed, do report:
+ -- the function that generates the error message
+ -- should look for an unsuppressed error item
= return ()
- -- suppress the group if any have been reported. Ideally, we'd like
- -- to suppress exactly those that have been reported, but this is
- -- awkward, and it's more embarrassing to report the same error
- -- twice than to suppress too eagerly
| otherwise
= case cec_defer_type_errors ctxt of
@@ -1104,8 +1038,7 @@ maybeReportError ctxt items err
addDeferredBinding :: ReportErrCtxt -> ErrMsg -> ErrorItem -> TcM ()
-- See Note [Deferring coercion errors to runtime]
--- See Note [Evidence types]
-addDeferredBinding ctxt err (EI { ei_evdest = Just dest, ei_type = item_ty })
+addDeferredBinding ctxt err (EI { ei_evdest = Just dest, ei_pred = item_ty })
-- if evdest is Just, then the constraint was from a wanted
| deferringAnyBindings ctxt
= do { dflags <- getDynFlags
@@ -1175,15 +1108,9 @@ tryReporter ctxt (str, keep_me, suppress_after, reporter) items
| otherwise
= do { traceTc "tryReporter{ " (text str <+> ppr yeses)
; (_, no_errs) <- askNoErrs (reporter ctxt yeses)
- ; let suppress_these = cec_suppress ctxt
- suppress_now = not no_errs && suppress_after
+ ; let suppress_now = not no_errs && suppress_after
-- See Note [Suppressing error messages]
- already_reported = cec_already_reported ctxt
- already_reported'
- | suppress_these = already_reported
- | otherwise = addListToUniqSet already_reported (map ei_unique yeses)
- ctxt' = ctxt { cec_suppress = suppress_now || suppress_these
- , cec_already_reported = already_reported' }
+ ctxt' = ctxt { cec_suppress = suppress_now || cec_suppress ctxt }
; traceTc "tryReporter end }" (text str <+> ppr (cec_suppress ctxt) <+> ppr suppress_after)
; return (ctxt', nos) }
where
@@ -1269,16 +1196,6 @@ from that EvVar, filling the hole with that coercion. Because coercions'
types are unlifted, the error is guaranteed to be hit before we get to the
coercion.
-Note [Evidence types]
-~~~~~~~~~~~~~~~~~~~~~
-As explained in Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint,
-we report errors about predicates that have been rewritten only with respect
-to givens, never wanteds. However, when we are generating evidence for
-deferred errors in addDeferredBinding, we need this evidence to have the
-type that the context expects, which is the one rewritten w.r.t. all other
-constraints, including Wanteds. So we keep this type in ErrorItem and
-use it in addDeferredBinding. Nothing hard, but it's easy to forget to do.
-
Note [No ancestors in addDeferredBinding]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Generally, we wish to report errors about the *ancestors* of constraints, not
@@ -1348,12 +1265,20 @@ mkIrredErr :: ReportErrCtxt -> [ErrorItem] -> TcM ErrMsg
mkIrredErr ctxt items
= do { (ctxt, binds_msg, item1) <- relevantBindings True ctxt item1
; let orig = errorItemOrigin item1
- msg = couldNotDeduce (getUserGivens ctxt) (map ei_pred items, orig)
+ msg = couldNotDeduce (getUserGivens ctxt) (preds, orig)
; mkErrorMsgFromItem ctxt item1 $
important msg `mappend` mk_relevant_bindings binds_msg }
where
(item1:_) = items
+ filtered_preds = [ pred | item <- items
+ , not (ei_suppress item)
+ , let pred = ei_pred item ]
+
+ preds | null filtered_preds = map ei_pred items
+ -- they're all suppressed; must report *something*
+ | otherwise = filtered_preds
+
----------------
mkHoleError :: [ErrorItem] -> ReportErrCtxt -> Hole -> TcM ErrMsg
mkHoleError _tidy_simples _ctxt hole@(Hole { hole_occ = occ
@@ -1482,7 +1407,7 @@ validHoleFits ctxt@(CEC { cec_encl = implics
, ctev_dest = dest
, ctev_nosh = WDeriv
, ctev_loc = loc
- , ctev_report_as = CtReportAsSame }
+ , ctev_rewriters = emptyRewriterSet }
mk_wanted item = pprPanic "validHoleFits no evdest" (ppr item)
-- See Note [Constraints include ...]
@@ -1503,6 +1428,9 @@ givenConstraintsMsg ctxt =
----------------
mkIPErr :: ReportErrCtxt -> [ErrorItem] -> TcM ErrMsg
+-- What would happen if an item is suppressed because of
+-- Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint? Very unclear
+-- what's best. Let's not worry about this.
mkIPErr ctxt items
= do { (ctxt, binds_msg, item1) <- relevantBindings True ctxt item1
; let orig = errorItemOrigin item1
@@ -1580,8 +1508,16 @@ any more. So we don't assert that it is.
-- Don't have multiple equality errors from the same location
-- E.g. (Int,Bool) ~ (Bool,Int) one error will do!
mkEqErr :: ReportErrCtxt -> [ErrorItem] -> TcM ErrMsg
-mkEqErr ctxt (item:_) = mkEqErr1 ctxt item
-mkEqErr _ [] = panic "mkEqErr"
+mkEqErr ctxt items
+ | item:_ <- filter (not . ei_suppress) items
+ = mkEqErr1 ctxt item
+
+ | item:_ <- items -- they're all suppressed. still need an error message
+ -- for -fdefer-type-errors though
+ = mkEqErr1 ctxt item
+
+ | otherwise
+ = panic "mkEqErr" -- guaranteed to have at least one item
mkEqErr1 :: ReportErrCtxt -> ErrorItem -> TcM ErrMsg
mkEqErr1 ctxt item -- Wanted or derived;
@@ -1794,6 +1730,11 @@ mkTyVarEqErr' dflags ctxt report item oriented tv1 ty2
-- to be helpful since this is just an unimplemented feature.
; mkErrorMsgFromItem ctxt item $ report { report_important = [msg] } }
+ -- This is wrinkle (4) in Note [Equalities with incompatible kinds] in
+ -- GHC.Tc.Solver.Canonical
+ | MTVU_HoleBlocker <- occ_check_expand
+ = mkBlockedEqErr ctxt item
+
-- If the immediately-enclosing implication has 'tv' a skolem, and
-- we know by now its an InferSkol kind of skolem, then presumably
-- it started life as a TyVarTv, else it'd have been unified, given
@@ -1945,8 +1886,8 @@ pp_givens givens
-- always be another unsolved wanted around, which will ordinarily suppress
-- this message. But this can still be printed out with -fdefer-type-errors
-- (sigh), so we must produce a message.
-mkBlockedEqErr :: ReportErrCtxt -> [ErrorItem] -> TcM ErrMsg
-mkBlockedEqErr ctxt (item:_) = mkErrorMsgFromItem ctxt item report
+mkBlockedEqErr :: ReportErrCtxt -> ErrorItem -> TcM ErrMsg
+mkBlockedEqErr ctxt item = mkErrorMsgFromItem ctxt item report
where
report = important msg
msg = vcat [ hang (text "Cannot use equality for substitution:")
@@ -1956,7 +1897,6 @@ mkBlockedEqErr ctxt (item:_) = mkErrorMsgFromItem ctxt item report
-- has -fprint-explicit-kinds on, they will see that the two
-- sides have the same kind, as there is an invisible cast.
-- I really don't know how to do better.
-mkBlockedEqErr _ [] = panic "mkBlockedEqErr no constraints"
{-
Note [Suppress redundant givens during error reporting]
@@ -2490,7 +2430,7 @@ Warn of loopy local equalities that were dropped.
-}
mkDictErr :: ReportErrCtxt -> [ErrorItem] -> TcM ErrMsg
-mkDictErr ctxt items
+mkDictErr ctxt orig_items
= ASSERT( not (null items) )
do { inst_envs <- tcGetInstEnvs
; let (item1:_) = items -- ct1 just for its location
@@ -2506,6 +2446,11 @@ mkDictErr ctxt items
; (ctxt, err) <- mk_dict_err ctxt (head (no_inst_items ++ overlap_items))
; mkErrorMsgFromItem ctxt item1 (important err) }
where
+ filtered_items = filter (not . ei_suppress) orig_items
+ items | null filtered_items = orig_items -- all suppressed, but must report
+ -- something for -fdefer-type-errors
+ | otherwise = filtered_items -- common case
+
no_givens = null (getUserGivens ctxt)
is_no_inst (item, (matches, unifiers, _))
=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -48,7 +48,6 @@ module GHC.Tc.Gen.HsType (
tcHsLiftedTypeNC, tcHsOpenTypeNC,
tcLHsType, tcLHsTypeUnsaturated, tcCheckLHsType,
tcHsMbContext, tcHsContext, tcLHsPredType, tcInferApps,
- failIfEmitsConstraints,
solveEqualities, -- useful re-export
typeLevelMode, kindLevelMode,
@@ -84,7 +83,6 @@ import GHC.Tc.Solver
import GHC.Tc.Utils.Zonk
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Ppr
-import GHC.Tc.Errors ( reportAllUnsolved )
import GHC.Tc.Utils.TcType
import GHC.Tc.Utils.Instantiate ( tcInstInvisibleTyBinders, tcInstInvisibleTyBinder )
import GHC.Core.Type
@@ -3513,19 +3511,6 @@ promotionErr name err
-}
--- | If the inner action emits constraints, report them as errors and fail;
--- otherwise, propagates the return value. Useful as a wrapper around
--- 'tcImplicitTKBndrs', which uses solveLocalEqualities, when there won't be
--- another chance to solve constraints
-failIfEmitsConstraints :: TcM a -> TcM a
-failIfEmitsConstraints thing_inside
- = checkNoErrs $ -- We say that we fail if there are constraints!
- -- c.f same checkNoErrs in solveEqualities
- do { (res, lie) <- captureConstraints thing_inside
- ; reportAllUnsolved lie
- ; return res
- }
-
-- | Make an appropriate message for an error in a function argument.
-- Used for both expressions and types.
funAppCtxt :: (Outputable fun, Outputable arg) => fun -> arg -> Int -> SDoc
=====================================
compiler/GHC/Tc/Solver.hs
=====================================
@@ -814,7 +814,7 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
, ctev_dest = EvVarDest psig_theta_var
, ctev_nosh = WDeriv
, ctev_loc = ct_loc
- , ctev_report_as = CtReportAsSame }
+ , ctev_rewriters = emptyRewriterSet }
| psig_theta_var <- psig_theta_vars ]
-- Now construct the residual constraint
@@ -2647,13 +2647,12 @@ disambigGroup (default_ty:default_tys) group@(the_tv, wanteds)
= do { lcl_env <- TcS.getLclEnv
; tc_lvl <- TcS.getTcLevel
; let loc = mkGivenLoc tc_lvl UnkSkol lcl_env
- ; wanted_evs <- sequence [ newWantedEvVarNC loc report_as' pred'
+ ; wanted_evs <- sequence [ newWantedEvVarNC loc rewriters pred'
| wanted <- wanteds
, CtWanted { ctev_pred = pred
- , ctev_report_as = report_as }
+ , ctev_rewriters = rewriters }
<- return (ctEvidence wanted)
- , let pred' = substTy subst pred
- report_as' = substCtReportAs subst report_as ]
+ , let pred' = substTy subst pred ]
; fmap isEmptyWC $
solveSimpleWanteds $ listToBag $
map mkNonCanonical wanted_evs }
=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -3,7 +3,7 @@
module GHC.Tc.Solver.Canonical(
canonicalize,
- unifyDerived,
+ unifyWanted,
makeSuperClasses, maybeSym,
StopOrContinue(..), stopWith, continueWith,
solveCallStack -- For GHC.Tc.Solver
@@ -154,7 +154,7 @@ canClassNC ev cls tys
; emitWork sc_cts
; canClass ev cls tys False }
- | CtWanted { ctev_report_as = report_as } <- ev
+ | CtWanted { ctev_rewriters = rewriters } <- ev
, Just ip_name <- isCallStackPred cls tys
, OccurrenceOf func <- ctLocOrigin loc
-- If we're given a CallStack constraint that arose from a function
@@ -169,7 +169,7 @@ canClassNC ev cls tys
-- this rule does not fire again.
-- See Note [Overview of implicit CallStacks]
- ; new_ev <- newWantedEvVarNC new_loc report_as pred
+ ; new_ev <- newWantedEvVarNC new_loc rewriters pred
-- Then we solve the wanted by pushing the call-site
-- onto the newly emitted CallStack
@@ -205,7 +205,7 @@ canClass :: CtEvidence
canClass ev cls tys pend_sc
= -- all classes do *nominal* matching
ASSERT2( ctEvRole ev == Nominal, ppr ev $$ ppr cls $$ ppr tys )
- do { (xis, cos, _kind_co, wrw) <- flattenArgsNom ev cls_tc tys
+ do { (xis, cos, _kind_co, rewriters) <- flattenArgsNom ev cls_tc tys
; MASSERT( isTcReflCo _kind_co )
; let co = mkTcTyConAppCo Nominal cls_tc cos
xi = mkClassPred cls xis
@@ -213,7 +213,7 @@ canClass ev cls tys pend_sc
, cc_tyargs = xis
, cc_class = cls
, cc_pend_sc = pend_sc }
- ; mb <- rewriteEvidence wrw ev xi co
+ ; mb <- rewriteEvidence rewriters ev xi co
; traceTcS "canClass" (vcat [ ppr ev
, ppr xi, ppr mb ])
; return (fmap mk_ct mb) }
@@ -598,7 +598,7 @@ mk_strict_superclasses rec_clss ev tvs theta cls tys
loc = ctEvLoc ev
do_one_derived sc_pred
- = do { sc_ev <- newDerivedNC loc sc_pred
+ = do { sc_ev <- newDerivedNC loc (ctEvRewriters ev) sc_pred
; mk_superclasses rec_clss sc_ev [] [] sc_pred }
{- Note [Improvement from Ground Wanteds]
@@ -705,8 +705,8 @@ canIrred :: CtIrredStatus -> CtEvidence -> TcS (StopOrContinue Ct)
canIrred status ev
= do { let pred = ctEvPred ev
; traceTcS "can_pred" (text "IrredPred = " <+> ppr pred)
- ; (xi,co,wrw) <- flatten FM_FlattenAll ev pred -- co :: xi ~ pred
- ; rewriteEvidence wrw ev xi co `andWhenContinue` \ new_ev ->
+ ; (xi,co,rewriters) <- flatten FM_FlattenAll ev pred -- co :: xi ~ pred
+ ; rewriteEvidence rewriters ev xi co `andWhenContinue` \ new_ev ->
do { -- Re-classify, in case flattening has improved its shape
; case classifyPredType (ctEvPred new_ev) of
ClassPred cls tys -> canClassNC new_ev cls tys
@@ -815,8 +815,8 @@ canForAll ev pend_sc
-- do them under a forall anyway (c.f. Flatten.flatten_one
-- on a forall type)
let pred = ctEvPred ev
- ; (xi,co,wrw) <- flatten FM_SubstOnly ev pred -- co :: xi ~ pred
- ; rewriteEvidence wrw ev xi co `andWhenContinue` \ new_ev ->
+ ; (xi,co,rewriters) <- flatten FM_SubstOnly ev pred -- co :: xi ~ pred
+ ; rewriteEvidence rewriters ev xi co `andWhenContinue` \ new_ev ->
do { -- Now decompose into its pieces and solve it
-- (It takes a lot less code to flatten before decomposing.)
@@ -829,7 +829,7 @@ canForAll ev pend_sc
solveForAll :: CtEvidence -> [TyVar] -> TcThetaType -> PredType -> Bool
-> TcS (StopOrContinue Ct)
solveForAll ev tvs theta pred pend_sc
- | CtWanted { ctev_dest = dest, ctev_report_as = report_as } <- ev
+ | CtWanted { ctev_dest = dest, ctev_rewriters = rewriters } <- ev
= -- See Note [Solving a Wanted forall-constraint]
do { let skol_info = QuantCtxtSkol
empty_subst = mkEmptyTCvSubst $ mkInScopeSet $
@@ -839,7 +839,7 @@ solveForAll ev tvs theta pred pend_sc
; (lvl, (w_id, wanteds))
<- pushLevelNoWorkList (ppr skol_info) $
- do { wanted_ev <- newWantedEvVarNC loc report_as $
+ do { wanted_ev <- newWantedEvVarNC loc rewriters $
substTy subst pred
; return ( ctEvEvId wanted_ev
, unitBag (mkNonCanonical wanted_ev)) }
@@ -1030,9 +1030,9 @@ can_eq_nc' True _rdr_env _envs ev eq_rel ty1 _ (AppTy t2 s2) _
-- No similarity in type structure detected. Flatten and try again.
can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
- = do { (xi1, co1, wrw1) <- flatten FM_FlattenAll ev ps_ty1
- ; (xi2, co2, wrw2) <- flatten FM_FlattenAll ev ps_ty2
- ; new_ev <- rewriteEqEvidence (wrw1 S.<> wrw2) ev NotSwapped xi1 xi2 co1 co2
+ = do { (xi1, co1, rewriters1) <- flatten FM_FlattenAll ev ps_ty1
+ ; (xi2, co2, rewriters2) <- flatten FM_FlattenAll ev ps_ty2
+ ; new_ev <- rewriteEqEvidence (rewriters1 S.<> rewriters2) ev NotSwapped xi1 xi2 co1 co2
; can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 }
-- We've flattened and the types don't match. Give up.
@@ -1066,7 +1066,7 @@ can_eq_nc_forall :: CtEvidence -> EqRel
-- so we must proceed one binder at a time (#13879)
can_eq_nc_forall ev eq_rel s1 s2
- | CtWanted { ctev_loc = loc, ctev_dest = orig_dest, ctev_report_as = report_as } <- ev
+ | CtWanted { ctev_loc = loc, ctev_dest = orig_dest, ctev_rewriters = rewriters } <- ev
= do { let free_tvs = tyCoVarsOfTypes [s1,s2]
(bndrs1, phi1) = tcSplitForAllVarBndrs s1
(bndrs2, phi2) = tcSplitForAllVarBndrs s2
@@ -1090,7 +1090,7 @@ can_eq_nc_forall ev eq_rel s1 s2
-> TcS (TcCoercion, Cts)
go (skol_tv:skol_tvs) subst (bndr2:bndrs2)
= do { let tv2 = binderVar bndr2
- ; (kind_co, wanteds1) <- unify loc report_as Nominal (tyVarKind skol_tv)
+ ; (kind_co, wanteds1) <- unify loc rewriters Nominal (tyVarKind skol_tv)
(substTy subst (tyVarKind tv2))
; let subst' = extendTvSubstAndInScope subst tv2
(mkCastTy (mkTyVarTy skol_tv) kind_co)
@@ -1103,7 +1103,7 @@ can_eq_nc_forall ev eq_rel s1 s2
-- Done: unify phi1 ~ phi2
go [] subst bndrs2
= ASSERT( null bndrs2 )
- unify loc report_as (eqRelRole eq_rel) phi1' (substTyUnchecked subst phi2)
+ unify loc rewriters (eqRelRole eq_rel) phi1' (substTyUnchecked subst phi2)
go _ _ _ = panic "cna_eq_nc_forall" -- case (s:ss) []
@@ -1122,14 +1122,14 @@ can_eq_nc_forall ev eq_rel s1 s2
; stopWith ev "Discard given polytype equality" }
where
- unify :: CtLoc -> CtReportAs -> Role -> TcType -> TcType -> TcS (TcCoercion, Cts)
+ unify :: CtLoc -> RewriterSet -> Role -> TcType -> TcType -> TcS (TcCoercion, Cts)
-- This version returns the wanted constraint rather
-- than putting it in the work list
- unify loc report_as role ty1 ty2
+ unify loc rewriters role ty1 ty2
| ty1 `tcEqType` ty2
= return (mkTcReflCo role ty1, emptyBag)
| otherwise
- = do { (wanted, co) <- newWantedEq loc report_as role ty1 ty2
+ = do { (wanted, co) <- newWantedEq loc rewriters role ty1 ty2
; return (co, unitBag (mkNonCanonical wanted)) }
---------------------------------
@@ -1364,7 +1364,7 @@ can_eq_newtype_nc ev swapped ty1 ((gres, co), ty1') ty2 ps_ty2
-- module, don't warn about it being unused.
-- See Note [Tracking unused binding and imports] in GHC.Tc.Utils.
- ; new_ev <- rewriteEqEvidence NoWRW ev swapped ty1' ps_ty2
+ ; new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped ty1' ps_ty2
(mkTcSymCo co) (mkTcReflCo Representational ps_ty2)
; can_eq_nc False new_ev ReprEq ty1' ty1' ty2 ps_ty2 }
where
@@ -1387,12 +1387,12 @@ can_eq_app ev s1 t1 s2 t2
= do { unifyDeriveds loc [Nominal, Nominal] [s1, t1] [s2, t2]
; stopWith ev "Decomposed [D] AppTy" }
- | CtWanted { ctev_dest = dest, ctev_report_as = report_as } <- ev
- = do { co_s <- unifyWanted report_as loc Nominal s1 s2
+ | CtWanted { ctev_dest = dest, ctev_rewriters = rewriters } <- ev
+ = do { co_s <- unifyWanted rewriters loc Nominal s1 s2
; let arg_loc
| isNextArgVisible s1 = loc
| otherwise = updateCtLocOrigin loc toInvisibleOrigin
- ; co_t <- unifyWanted report_as arg_loc Nominal t1 t2
+ ; co_t <- unifyWanted rewriters arg_loc Nominal t1 t2
; let co = mkAppCo co_s co_t
; setWantedEq dest co
; stopWith ev "Decomposed [W] AppTy" }
@@ -1440,7 +1440,7 @@ canEqCast flat ev eq_rel swapped ty1 co1 ty2 ps_ty2
= do { traceTcS "Decomposing cast" (vcat [ ppr ev
, ppr ty1 <+> text "|>" <+> ppr co1
, ppr ps_ty2 ])
- ; new_ev <- rewriteEqEvidence NoWRW ev swapped ty1 ps_ty2
+ ; new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped ty1 ps_ty2
(mkTcGReflRightCo role ty1 co1)
(mkTcReflCo role ps_ty2)
; can_eq_nc flat new_ev eq_rel ty1 ty1 ty2 ps_ty2 }
@@ -1682,11 +1682,11 @@ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
CtDerived {}
-> unifyDeriveds loc tc_roles tys1 tys2
- CtWanted { ctev_dest = dest, ctev_report_as = report_as }
+ CtWanted { ctev_dest = dest, ctev_rewriters = rewriters }
-- new_locs and tc_roles are both infinite, so
-- we are guaranteed that cos has the same length
-- as tys1 and tys2
- -> do { cos <- zipWith4M (unifyWanted report_as) new_locs tc_roles tys1 tys2
+ -> do { cos <- zipWith4M (unifyWanted rewriters) new_locs tc_roles tys1 tys2
; setWantedEq dest (mkTyConAppCo role tc cos) }
CtGiven { ctev_evar = evar }
@@ -1733,14 +1733,14 @@ canEqFailure :: CtEvidence -> EqRel
canEqFailure ev NomEq ty1 ty2
= canEqHardFailure ev ty1 ty2
canEqFailure ev ReprEq ty1 ty2
- = do { (xi1, co1, wrw1) <- flatten FM_FlattenAll ev ty1
- ; (xi2, co2, wrw2) <- flatten FM_FlattenAll ev ty2
+ = do { (xi1, co1, rewriters1) <- flatten FM_FlattenAll ev ty1
+ ; (xi2, co2, rewriters2) <- flatten FM_FlattenAll ev ty2
-- We must flatten the types before putting them in the
-- inert set, so that we are sure to kick them out when
-- new equalities become available
; traceTcS "canEqFailure with ReprEq" $
vcat [ ppr ev, ppr ty1, ppr ty2, ppr xi1, ppr xi2 ]
- ; new_ev <- rewriteEqEvidence (wrw1 S.<> wrw2) ev NotSwapped xi1 xi2 co1 co2
+ ; new_ev <- rewriteEqEvidence (rewriters1 S.<> rewriters2) ev NotSwapped xi1 xi2 co1 co2
; continueWith (mkIrredCt OtherCIS new_ev) }
-- | Call when canonicalizing an equality fails with utterly no hope.
@@ -1748,9 +1748,9 @@ canEqHardFailure :: CtEvidence
-> TcType -> TcType -> TcS (StopOrContinue Ct)
-- See Note [Make sure that insolubles are fully rewritten]
canEqHardFailure ev ty1 ty2
- = do { (s1, co1, wrw1) <- flatten FM_SubstOnly ev ty1
- ; (s2, co2, wrw2) <- flatten FM_SubstOnly ev ty2
- ; new_ev <- rewriteEqEvidence (wrw1 S.<> wrw2) ev NotSwapped s1 s2 co1 co2
+ = do { (s1, co1, rewriters1) <- flatten FM_SubstOnly ev ty1
+ ; (s2, co2, rewriters2) <- flatten FM_SubstOnly ev ty2
+ ; new_ev <- rewriteEqEvidence (rewriters1 S.<> rewriters2) ev NotSwapped s1 s2 co1 co2
; continueWith (mkIrredCt InsolubleCIS new_ev) }
{-
@@ -1885,7 +1885,7 @@ canCFunEqCan :: CtEvidence
-- Instead, flatten the args. The RHS is an fsk, which we
-- must *not* substitute.
canCFunEqCan ev fn tys fsk
- = do { (tys', cos, kind_co, wrw) <- flattenArgsNom ev fn tys
+ = do { (tys', cos, kind_co, new_rewriters) <- flattenArgsNom ev fn tys
-- cos :: tys' ~ tys
; let lhs_co = mkTcTyConAppCo Nominal fn cos
@@ -1894,12 +1894,12 @@ canCFunEqCan ev fn tys fsk
flav = ctEvFlavour ev
- report_as = updateReportAs wrw (ctEvUnique ev) (ctEvPred ev) (ctEvReportAs ev)
+ rewriters = ctEvRewriters ev S.<> new_rewriters
; (ev', fsk')
<- if isTcReflexiveCo kind_co -- See Note [canCFunEqCan]
then do { traceTcS "canCFunEqCan: refl" (ppr new_lhs)
; let fsk_ty = mkTyVarTy fsk
- ; ev' <- rewriteEqEvidence wrw ev NotSwapped new_lhs fsk_ty
+ ; ev' <- rewriteEqEvidence new_rewriters ev NotSwapped new_lhs fsk_ty
lhs_co (mkTcNomReflCo fsk_ty)
; return (ev', fsk) }
else do { traceTcS "canCFunEqCan: non-refl" $
@@ -1910,7 +1910,7 @@ canCFunEqCan ev fn tys fsk
, text "New LHS" <+> hang (ppr new_lhs)
2 (dcolon <+> ppr (tcTypeKind new_lhs)) ]
; (ev', new_co, new_fsk)
- <- newFlattenSkolem flav (ctEvLoc ev) report_as fn tys'
+ <- newFlattenSkolem flav (ctEvLoc ev) rewriters fn tys'
; let xi = mkTyVarTy new_fsk `mkCastTy` kind_co
-- sym lhs_co :: F tys ~ F tys'
-- new_co :: F tys' ~ new_fsk
@@ -1968,11 +1968,12 @@ canEqTyVarHetero ev eq_rel swapped tv1 ps_tv1 ki1 xi2 ps_xi2 ki2
lhs' = mkTyVarTy tv1 -- same as old lhs
lhs_co = mkTcReflCo role lhs'
+ rewriters = rewriterSetFromCo kind_co
+
; traceTcS "Hetero equality gives rise to kind equality"
(ppr kind_co <+> dcolon <+> sep [ ppr ki2, text "~#", ppr ki1 ])
- -- YesWRW: we've just emitted a new wanted and rewrote with it
-- See Note [Equalities with incompatible kinds]
- ; type_ev <- rewriteEqEvidence YesWRW ev swapped lhs' rhs' lhs_co rhs_co
+ ; type_ev <- rewriteEqEvidence rewriters ev swapped lhs' rhs' lhs_co rhs_co
-- rewriteEqEvidence carries out the swap, so we're NotSwapped any more
; canEqTyVarHomo type_ev eq_rel NotSwapped tv1 ps_tv1 rhs' ps_rhs' }
@@ -1985,11 +1986,11 @@ canEqTyVarHetero ev eq_rel swapped tv1 ps_tv1 ki1 xi2 ps_xi2 ki2
; emitWorkNC [kind_ev]
; return (ctEvCoercion kind_ev) }
- CtWanted { ctev_report_as = report_as }
- -> unifyWanted report_as kind_loc Nominal ki2 ki1
+ CtWanted { ctev_rewriters = rewriters }
+ -> unifyWanted rewriters kind_loc Nominal ki2 ki1
CtDerived {}
- -> unifyWanted CtReportAsSame kind_loc Nominal ki2 ki1
+ -> unifyWanted emptyRewriterSet kind_loc Nominal ki2 ki1
loc = ctev_loc ev
role = eqRelRole eq_rel
@@ -2027,7 +2028,7 @@ canEqTyVarHomo ev eq_rel swapped tv1 ps_xi1 xi2 _
new_rhs = mkTyVarTy tv2
rhs_co = mkTcGReflRightCo role new_rhs co2
- ; new_ev <- rewriteEqEvidence NoWRW ev swapped new_lhs new_rhs lhs_co rhs_co
+ ; new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped new_lhs new_rhs lhs_co rhs_co
; dflags <- getDynFlags
; canEqTyVar2 dflags new_ev eq_rel IsSwapped tv2 (ps_xi1 `mkCastTy` sym_co2) }
@@ -2059,14 +2060,16 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 rhs
-- equalities, in case have x ~ (y :: ..x...)
-- #12593
-- guarantees (TyEq:OC), (TyEq:F), and (TyEq:H)
- = do { new_ev <- rewriteEqEvidence NoWRW ev swapped lhs rhs' rewrite_co1 rewrite_co2
+ = do { new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped lhs rhs'
+ rewrite_co1 rewrite_co2
; continueWith (CTyEqCan { cc_ev = new_ev, cc_tyvar = tv1
, cc_rhs = rhs', cc_eq_rel = eq_rel }) }
| otherwise -- For some reason (occurs check, or forall) we can't unify
-- We must not use it for further rewriting!
= do { traceTcS "canEqTyVar2 can't unify" (ppr tv1 $$ ppr rhs)
- ; new_ev <- rewriteEqEvidence NoWRW ev swapped lhs rhs rewrite_co1 rewrite_co2
+ ; new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped lhs rhs
+ rewrite_co1 rewrite_co2
; let status | isInsolubleOccursCheck eq_rel tv1 rhs
= InsolubleCIS
-- If we have a ~ [a], it is not canonical, and in particular
@@ -2298,8 +2301,7 @@ andWhenContinue tcs1 tcs2
ContinueWith ct -> tcs2 ct }
infixr 0 `andWhenContinue` -- allow chaining with ($)
-rewriteEvidence :: WRWFlag -- did wanteds rewrite wanteds?
- -- See Note [Wanteds rewrite Wanteds]
+rewriteEvidence :: RewriterSet -- See Note [Wanteds rewrite Wanteds]
-- in GHC.Tc.Types.Constraint
-> CtEvidence -- old evidence
-> TcPredType -- new predicate
@@ -2339,7 +2341,7 @@ as well as in old_pred; that is important for good error messages.
-}
-rewriteEvidence _wrw old_ev@(CtDerived {}) new_pred _co
+rewriteEvidence _rewriters old_ev@(CtDerived {}) new_pred _co
= -- If derived, don't even look at the coercion.
-- This is very important, DO NOT re-order the equations for
-- rewriteEvidence to put the isTcReflCo test first!
@@ -2349,12 +2351,12 @@ rewriteEvidence _wrw old_ev@(CtDerived {}) new_pred _co
-- (Getting this wrong caused #7384.)
continueWith (old_ev { ctev_pred = new_pred })
-rewriteEvidence _wrw old_ev new_pred co
+rewriteEvidence _rewriters old_ev new_pred co
| isTcReflCo co -- See Note [Rewriting with Refl]
= continueWith (old_ev { ctev_pred = new_pred })
-rewriteEvidence wrw ev@(CtGiven { ctev_evar = old_evar, ctev_loc = loc }) new_pred co
- = ASSERT( wrw == NoWRW ) -- this is a Given, not a wanted
+rewriteEvidence rewriters ev@(CtGiven { ctev_evar = old_evar, ctev_loc = loc }) new_pred co
+ = ASSERT( isEmptyRewriterSet rewriters ) -- this is a Given, not a wanted
do { new_ev <- newGivenEvVar loc (new_pred, new_tm)
; continueWith new_ev }
where
@@ -2363,12 +2365,12 @@ rewriteEvidence wrw ev@(CtGiven { ctev_evar = old_evar, ctev_loc = loc }) new_pr
(ctEvRole ev)
(mkTcSymCo co))
-rewriteEvidence wrw ev@(CtWanted { ctev_pred = old_pred
- , ctev_dest = dest
- , ctev_nosh = si
- , ctev_loc = loc
- , ctev_report_as = report_as }) new_pred co
- = do { mb_new_ev <- newWanted_SI si loc report_as' new_pred
+rewriteEvidence new_rewriters
+ ev@(CtWanted { ctev_dest = dest
+ , ctev_nosh = si
+ , ctev_loc = loc
+ , ctev_rewriters = rewriters }) new_pred co
+ = do { mb_new_ev <- newWanted_SI si loc rewriters' new_pred
-- The "_SI" variant ensures that we make a new Wanted
-- with the same shadow-info as the existing one
-- with the same shadow-info as the existing one (#16735)
@@ -2380,10 +2382,11 @@ rewriteEvidence wrw ev@(CtWanted { ctev_pred = old_pred
Fresh new_ev -> continueWith new_ev
Cached _ -> stopWith ev "Cached wanted" }
where
- report_as' = updateReportAs wrw (tcEvDestUnique dest) old_pred report_as
+ rewriters' = rewriters S.<> new_rewriters
-rewriteEqEvidence :: WRWFlag -- YesWRW <=> a wanted rewrote a wanted
+rewriteEqEvidence :: RewriterSet -- See GHC.Tc.Types.Constraint
+ -- Note [Wanteds rewrite Wanteds]
-> CtEvidence -- Old evidence :: olhs ~ orhs (not swapped)
-- or orhs ~ olhs (swapped)
-> SwapFlag
@@ -2406,7 +2409,7 @@ rewriteEqEvidence :: WRWFlag -- YesWRW <=> a wanted rewrote a wanted
-- w : orhs ~ olhs = sym rhs_co ; sym w1 ; lhs_co
--
-- It's all a form of rewwriteEvidence, specialised for equalities
-rewriteEqEvidence wrw old_ev swapped nlhs nrhs lhs_co rhs_co
+rewriteEqEvidence new_rewriters old_ev swapped nlhs nrhs lhs_co rhs_co
| CtDerived {} <- old_ev -- Don't force the evidence for a Derived
= return (old_ev { ctev_pred = new_pred })
@@ -2421,14 +2424,13 @@ rewriteEqEvidence wrw old_ev swapped nlhs nrhs lhs_co rhs_co
`mkTcTransCo` mkTcSymCo rhs_co)
; newGivenEvVar loc' (new_pred, new_tm) }
- | CtWanted { ctev_pred = old_pred
- , ctev_dest = dest
+ | CtWanted { ctev_dest = dest
, ctev_nosh = si
- , ctev_report_as = report_as } <- old_ev
- , let report_as' = updateReportAs wrw (tcEvDestUnique dest) old_pred report_as
+ , ctev_rewriters = rewriters } <- old_ev
+ , let rewriters' = rewriters S.<> new_rewriters
= case dest of
HoleDest hole ->
- do { (new_ev, hole_co) <- newWantedEq_SI (ch_blocker hole) si loc' report_as'
+ do { (new_ev, hole_co) <- newWantedEq_SI (ch_blocker hole) si loc' rewriters'
(ctEvRole old_ev) nlhs nrhs
-- The "_SI" variant ensures that we make a new Wanted
-- with the same shadow-info as the existing one (#16735)
@@ -2468,31 +2470,31 @@ But where it succeeds in finding common structure, it just builds a coercion
to reflect it.
-}
-unifyWanted :: CtReportAs -> CtLoc
+unifyWanted :: RewriterSet -> CtLoc
-> Role -> TcType -> TcType -> TcS Coercion
-- Return coercion witnessing the equality of the two types,
-- emitting new work equalities where necessary to achieve that
-- Very good short-cut when the two types are equal, or nearly so
-- See Note [unifyWanted and unifyDerived]
-- The returned coercion's role matches the input parameter
-unifyWanted report_as loc Phantom ty1 ty2
- = do { kind_co <- unifyWanted report_as loc Nominal (tcTypeKind ty1) (tcTypeKind ty2)
+unifyWanted rewriters loc Phantom ty1 ty2
+ = do { kind_co <- unifyWanted rewriters loc Nominal (tcTypeKind ty1) (tcTypeKind ty2)
; return (mkPhantomCo kind_co ty1 ty2) }
-unifyWanted report_as loc role orig_ty1 orig_ty2
+unifyWanted rewriters loc role orig_ty1 orig_ty2
= go orig_ty1 orig_ty2
where
go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
go (FunTy _ s1 t1) (FunTy _ s2 t2)
- = do { co_s <- unifyWanted report_as loc role s1 s2
- ; co_t <- unifyWanted report_as loc role t1 t2
+ = do { co_s <- unifyWanted rewriters loc role s1 s2
+ ; co_t <- unifyWanted rewriters loc role t1 t2
; return (mkFunCo role co_s co_t) }
go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
| tc1 == tc2, tys1 `equalLength` tys2
, isInjectiveTyCon tc1 role -- don't look under newtypes at Rep equality
- = do { cos <- zipWith3M (unifyWanted report_as loc)
+ = do { cos <- zipWith3M (unifyWanted rewriters loc)
(tyConRolesX role tc1) tys1 tys2
; return (mkTyConAppCo role tc1 cos) }
@@ -2515,16 +2517,12 @@ unifyWanted report_as loc role orig_ty1 orig_ty2
bale_out ty1 ty2
| ty1 `tcEqType` ty2 = return (mkTcReflCo role ty1)
-- Check for equality; e.g. a ~ a, or (m a) ~ (m a)
- | otherwise = emitNewWantedEq loc report_as role orig_ty1 orig_ty2
+ | otherwise = emitNewWantedEq loc rewriters role orig_ty1 orig_ty2
unifyDeriveds :: CtLoc -> [Role] -> [TcType] -> [TcType] -> TcS ()
-- See Note [unifyWanted and unifyDerived]
unifyDeriveds loc roles tys1 tys2 = zipWith3M_ (unify_derived loc) roles tys1 tys2
-unifyDerived :: CtLoc -> Role -> Pair TcType -> TcS ()
--- See Note [unifyWanted and unifyDerived]
-unifyDerived loc role (Pair ty1 ty2) = unify_derived loc role ty1 ty2
-
unify_derived :: CtLoc -> Role -> TcType -> TcType -> TcS ()
-- Create new Derived and put it in the work list
-- Should do nothing if the two types are equal
=====================================
compiler/GHC/Tc/Solver/Flatten.hs
=====================================
@@ -456,13 +456,13 @@ wanteds, we will
type FlatWorkListRef = TcRef [Ct] -- See Note [The flattening work list]
data FlattenEnv
- = FE { fe_mode :: !FlattenMode
- , fe_loc :: CtLoc -- See Note [Flattener CtLoc]
+ = FE { fe_mode :: !FlattenMode
+ , fe_loc :: CtLoc -- See Note [Flattener CtLoc]
-- unbanged because it's bogus in rewriteTyVar
- , fe_flavour :: !CtFlavour
- , fe_eq_rel :: !EqRel -- See Note [Flattener EqRels]
- , fe_work :: !FlatWorkListRef -- See Note [The flattening work list]
- , fe_wrw :: !(TcRef WRWFlag) } -- See Note [Flattening wanteds]
+ , fe_flavour :: !CtFlavour
+ , fe_eq_rel :: !EqRel -- See Note [Flattener EqRels]
+ , fe_work :: !FlatWorkListRef -- See Note [The flattening work list]
+ , fe_rewriters :: !(TcRef RewriterSet) } -- See Note [Flattening wanteds]
data FlattenMode -- Postcondition for all three: inert wrt the type substitution
= FM_FlattenAll -- Postcondition: function-free
@@ -512,7 +512,7 @@ emitFlatWork ct = FlatM $ \env -> updTcRef (fe_work env) (ct :)
-- convenient wrapper when you have a CtEvidence describing
-- the flattening operation
-runFlattenCtEv :: FlattenMode -> CtEvidence -> FlatM a -> TcS (a, WRWFlag)
+runFlattenCtEv :: FlattenMode -> CtEvidence -> FlatM a -> TcS (a, RewriterSet)
runFlattenCtEv mode ev
= runFlatten mode (ctEvLoc ev) (ctEvFlavour ev) (ctEvEqRel ev)
@@ -520,22 +520,23 @@ runFlattenCtEv mode ev
-- the work it generates onto the main work list
-- See Note [The flattening work list]
-- Also returns whether a wanted rewrote a wanted; see Note [Flattening wanteds]
-runFlatten :: FlattenMode -> CtLoc -> CtFlavour -> EqRel -> FlatM a -> TcS (a, WRWFlag)
+runFlatten :: FlattenMode -> CtLoc -> CtFlavour -> EqRel -> FlatM a
+ -> TcS (a, RewriterSet)
runFlatten mode loc flav eq_rel thing_inside
= do { flat_ref <- newTcRef []
- ; wrw_ref <- newTcRef NoWRW
+ ; rewriters_ref <- newTcRef emptyRewriterSet
; let fmode = FE { fe_mode = mode
, fe_loc = bumpCtLocDepth loc
-- See Note [Flatten when discharging CFunEqCan]
, fe_flavour = flav
, fe_eq_rel = eq_rel
, fe_work = flat_ref
- , fe_wrw = wrw_ref }
+ , fe_rewriters = rewriters_ref }
; res <- runFlatM thing_inside fmode
; new_flats <- readTcRef flat_ref
; updWorkListTcS (add_flats new_flats)
- ; wrw <- readTcRef wrw_ref
- ; return (res, wrw) }
+ ; rewriters <- readTcRef rewriters_ref
+ ; return (res, rewriters) }
where
add_flats new_flats wl
= wl { wl_funeqs = add_funeqs new_flats (wl_funeqs wl) }
@@ -617,9 +618,11 @@ bumpDepth (FlatM thing_inside)
; thing_inside env' }
-- See Note [Flattening wanteds]
-recordWRW :: WRWFlag -> FlatM ()
-recordWRW YesWRW = FlatM $ \env -> writeTcRef (fe_wrw env) YesWRW
-recordWRW NoWRW = return ()
+-- Precondition: the CtEvidence is a CtWanted of an equality
+recordRewriter :: CtEvidence -> FlatM ()
+recordRewriter (CtWanted { ctev_dest = HoleDest hole })
+ = FlatM $ \env -> updTcRef (fe_rewriters env) (`addRewriterSet` hole)
+recordRewriter other = pprPanic "recordRewriter" (ppr other)
{-
Note [The flattening work list]
@@ -787,23 +790,20 @@ when trying to find derived equalities arising from injectivity.
-}
-- | See Note [Flattening].
--- If (xi, co, wrw) <- flatten mode ev ty, then co :: xi ~r ty
+-- If (xi, co, rewriters) <- flatten mode ev ty, then co :: xi ~r ty
-- where r is the role in @ev at . If @mode@ is 'FM_FlattenAll',
-- then 'xi' is almost function-free (Note [Almost function-free]
-- in GHC.Tc.Types).
--- wrw is True <=> a wanted rewrote a wanted.
+-- rewriters is the set of coercion holes that have been used to rewrite
-- See Note [Wanteds rewrite wanteds] in GHC.Tc.Types.Constraint
-- and Note [Flattening wanteds]
flatten :: FlattenMode -> CtEvidence -> TcType
- -> TcS (Xi, TcCoercion, WRWFlag)
+ -> TcS (Xi, TcCoercion, RewriterSet)
flatten mode ev ty
= do { traceTcS "flatten {" (ppr mode <+> ppr ty)
- ; ((ty', co), wrw) <- runFlattenCtEv mode ev (flatten_one ty)
- ; traceTcS "flatten }" (ppr ty' $$ pp_wrw wrw)
- ; return (ty', co, wrw) }
- where
- pp_wrw YesWRW = text "YesWRW: wanted rewrote wanted"
- pp_wrw _ = empty
+ ; ((ty', co), rewriters) <- runFlattenCtEv mode ev (flatten_one ty)
+ ; traceTcS "flatten }" (ppr ty' $$ ppr rewriters)
+ ; return (ty', co, rewriters) }
-- Apply the inert set as an *inert generalised substitution* to
-- a variable, zonking along the way.
@@ -825,7 +825,7 @@ rewriteTyVar tv
-- See Note [Flattening]
flattenArgsNom :: CtEvidence -> TyCon -> [TcType]
- -> TcS ([Xi], [TcCoercion], TcCoercionN, WRWFlag)
+ -> TcS ([Xi], [TcCoercion], TcCoercionN, RewriterSet)
-- Externally-callable, hence runFlatten
-- Flatten a vector of types all at once; in fact they are
-- always the arguments of type family or class, so
@@ -841,10 +841,10 @@ flattenArgsNom :: CtEvidence -> TyCon -> [TcType]
-- See Note [Flattening wanteds]
flattenArgsNom ev tc tys
= do { traceTcS "flatten_args {" (vcat (map ppr tys))
- ; ((tys', cos, kind_co), wrw)
+ ; ((tys', cos, kind_co), rewriters)
<- runFlattenCtEv FM_FlattenAll ev (flatten_args_tc tc (repeat Nominal) tys)
; traceTcS "flatten }" (vcat (map ppr tys'))
- ; return (tys', cos, kind_co, wrw) }
+ ; return (tys', cos, kind_co, rewriters) }
-- | Flatten a type w.r.t. nominal equality. This is useful to rewrite
-- a type w.r.t. any givens. It does not do type-family reduction. This
@@ -1461,7 +1461,7 @@ flatten_exact_fam_app_fully tc tys
Nothing -> do
{ loc <- getLoc
; (ev, co, fsk) <- liftTcS $
- newFlattenSkolem cur_flav loc CtReportAsSame tc xis
+ newFlattenSkolem cur_flav loc emptyRewriterSet tc xis
-- The new constraint (F xis ~ fsk) is not
-- necessarily inert (e.g. the LHS may be a
@@ -1660,7 +1660,7 @@ flatten_tyvar2 tv fr@(_, eq_rel)
vcat [ sep [ ppr mode, ppr tv, equals, ppr rhs_ty]
, ppr ctev
, text "wanted_rewrite_wanted:" <+> ppr wrw ]
- ; recordWRW wrw
+ ; when wrw $ recordRewriter ctev
; let rewrite_co1 = mkSymCo (ctEvCoercion ctev)
rewrite_co = case (ct_eq_rel, eq_rel) of
=====================================
compiler/GHC/Tc/Solver/Interact.hs
=====================================
@@ -52,6 +52,7 @@ import Data.List( partition, deleteFirstsBy )
import GHC.Types.SrcLoc
import GHC.Types.Var.Env
+import qualified Data.Semigroup as S
import Control.Monad
import GHC.Data.Maybe( isJust )
import GHC.Data.Pair (Pair(..))
@@ -1124,7 +1125,7 @@ shortCutSolver dflags ev_w ev_i
; lift $ traceTcS "shortCutSolver: found instance" (ppr preds)
; loc' <- lift $ checkInstanceOK loc what pred
- ; evc_vs <- mapM (new_wanted_cached loc' solved_dicts') preds
+ ; evc_vs <- mapM (new_wanted_cached ev loc' solved_dicts') preds
-- Emit work for subgoals but use our local cache
-- so we can solve recursive dictionaries.
@@ -1143,12 +1144,13 @@ shortCutSolver dflags ev_w ev_i
-- Use a local cache of solved dicts while emitting EvVars for new work
-- We bail out of the entire computation if we need to emit an EvVar for
-- a subgoal that isn't a ClassPred.
- new_wanted_cached :: CtLoc -> DictMap CtEvidence -> TcPredType -> MaybeT TcS MaybeNew
- new_wanted_cached loc cache pty
+ new_wanted_cached :: CtEvidence -> CtLoc
+ -> DictMap CtEvidence -> TcPredType -> MaybeT TcS MaybeNew
+ new_wanted_cached ev_w loc cache pty
| ClassPred cls tys <- classifyPredType pty
= lift $ case findDict cache loc_w cls tys of
Just ctev -> return $ Cached (ctEvExpr ctev)
- Nothing -> Fresh <$> newWantedNC loc pty
+ Nothing -> Fresh <$> newWantedNC loc (ctEvRewriters ev_w) pty
| otherwise = mzero
addFunDepWork :: InertCans -> CtEvidence -> Class -> TcS ()
@@ -1174,8 +1176,8 @@ addFunDepWork inerts work_ev cls
, pprCtLoc inert_loc, ppr (isGivenLoc inert_loc)
, pprCtLoc derived_loc, ppr (isGivenLoc derived_loc) ]) ;
- emitFunDepDeriveds $
- improveFromAnother derived_loc inert_pred work_pred
+ emitFunDepDeriveds (ctEvRewriters work_ev) $
+ improveFromAnother (derived_loc, inert_rewriters) inert_pred work_pred
-- We don't really rewrite tys2, see below _rewritten_tys2, so that's ok
-- NB: We do create FDs for given to report insoluble equations that arise
-- from pairs of Givens, and also because of floating when we approximate
@@ -1187,6 +1189,7 @@ addFunDepWork inerts work_ev cls
inert_ev = ctEvidence inert_ct
inert_pred = ctEvPred inert_ev
inert_loc = ctEvLoc inert_ev
+ inert_rewriters = ctRewriters inert_ct
derived_loc = work_loc { ctl_depth = ctl_depth work_loc `maxSubGoalDepth`
ctl_depth inert_loc
, ctl_origin = FunDepOrigin1 work_pred
@@ -1355,7 +1358,7 @@ improveLocalFunEqs work_ev inerts fam_tc args fsk
vcat [ text "Eqns:" <+> ppr eqns
, text "Candidates:" <+> ppr funeqs_for_tc
, text "Inert eqs:" <+> ppr (inert_eqs inerts) ]
- ; emitFunDepDeriveds eqns }
+ ; emitFunDepDeriveds (ctEvRewriters work_ev) eqns }
else return () }
where
@@ -1366,7 +1369,7 @@ improveLocalFunEqs work_ev inerts fam_tc args fsk
fam_inj_info = tyConInjectivityInfo fam_tc
--------------------
- improvement_eqns :: TcS [FunDepEqn CtLoc]
+ improvement_eqns :: TcS [FunDepEqn (CtLoc, RewriterSet)]
improvement_eqns
| Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
= -- Try built-in families, notably for arithmethic
@@ -1390,6 +1393,7 @@ improveLocalFunEqs work_ev inerts fam_tc args fsk
--------------------
-- See Note [Type inference for type families with injectivity]
+ do_one_injective :: [Bool] -> TcType -> Ct -> TcS [FunDepEqn (CtLoc, RewriterSet)]
do_one_injective inj_args rhs (CFunEqCan { cc_tyargs = inert_args
, cc_fsk = ifsk, cc_ev = inert_ev })
| isImprovable inert_ev
@@ -1405,15 +1409,16 @@ improveLocalFunEqs work_ev inerts fam_tc args fsk
do_one_injective _ _ _ = pprPanic "interactFunEq 2" (ppr fam_tc)
--------------------
- mk_fd_eqns :: CtEvidence -> [TypeEqn] -> [FunDepEqn CtLoc]
+ mk_fd_eqns :: CtEvidence -> [TypeEqn] -> [FunDepEqn (CtLoc, RewriterSet)]
mk_fd_eqns inert_ev eqns
| null eqns = []
| otherwise = [ FDEqn { fd_qtvs = [], fd_eqs = eqns
, fd_pred1 = work_pred
, fd_pred2 = ctEvPred inert_ev
- , fd_loc = loc } ]
+ , fd_loc = (loc, inert_rewriters) } ]
where
- inert_loc = ctEvLoc inert_ev
+ inert_loc = ctEvLoc inert_ev
+ inert_rewriters = ctEvRewriters inert_ev
loc = inert_loc { ctl_depth = ctl_depth inert_loc `maxSubGoalDepth`
ctl_depth work_loc }
@@ -1784,23 +1789,26 @@ as the fundeps.
#7875 is a case in point.
-}
-emitFunDepDeriveds :: [FunDepEqn CtLoc] -> TcS ()
+emitFunDepDeriveds :: RewriterSet -- from the work item
+ -> [FunDepEqn (CtLoc, RewriterSet)] -> TcS ()
-- See Note [FunDep and implicit parameter reactions]
-emitFunDepDeriveds fd_eqns
+emitFunDepDeriveds work_rewriters fd_eqns
= mapM_ do_one_FDEqn fd_eqns
where
- do_one_FDEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = loc })
+ do_one_FDEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = (loc, rewriters) })
| null tvs -- Common shortcut
= do { traceTcS "emitFunDepDeriveds 1" (ppr (ctl_depth loc) $$ ppr eqs $$ ppr (isGivenLoc loc))
- ; mapM_ (unifyDerived loc Nominal) eqs }
+ ; mapM_ (\(Pair ty1 ty2) -> unifyWanted all_rewriters loc Nominal ty1 ty2) eqs }
| otherwise
= do { traceTcS "emitFunDepDeriveds 2" (ppr (ctl_depth loc) $$ ppr tvs $$ ppr eqs)
; subst <- instFlexi tvs -- Takes account of kind substitution
- ; mapM_ (do_one_eq loc subst) eqs }
+ ; mapM_ (do_one_eq loc all_rewriters subst) eqs }
+ where
+ all_rewriters = work_rewriters S.<> rewriters
- do_one_eq loc subst (Pair ty1 ty2)
- = unifyDerived loc Nominal $
- Pair (Type.substTyUnchecked subst ty1) (Type.substTyUnchecked subst ty2)
+ do_one_eq loc rewriters subst (Pair ty1 ty2)
+ = unifyWanted rewriters loc Nominal
+ (Type.substTyUnchecked subst ty1) (Type.substTyUnchecked subst ty2)
{-
**********************************************************************
@@ -1985,7 +1993,7 @@ reduce_top_fun_eq old_ev fsk (ax_co, rhs_ty)
= ASSERT2( not (fsk `elemVarSet` tyCoVarsOfType rhs_ty)
, ppr old_ev $$ ppr rhs_ty )
-- Guaranteed by Note [FunEq occurs-check principle]
- do { (rhs_xi, flatten_co, _wrw) <- flatten FM_FlattenAll old_ev rhs_ty
+ do { (rhs_xi, flatten_co, _rewriters) <- flatten FM_FlattenAll old_ev rhs_ty
-- flatten_co :: rhs_xi ~ rhs_ty
-- See Note [Flatten when discharging CFunEqCan]
; let total_co = ax_co `mkTcTransCo` mkTcSymCo flatten_co
@@ -2008,11 +2016,12 @@ improveTopFunEqs ev fam_tc args fsk
; eqns <- improve_top_fun_eqs fam_envs fam_tc args rhs
; traceTcS "improveTopFunEqs" (vcat [ ppr fam_tc <+> ppr args <+> ppr rhs
, ppr eqns ])
- ; mapM_ (unifyDerived loc Nominal) eqns }
+ ; mapM_ (\(Pair ty1 ty2) -> unifyWanted rewriters loc Nominal ty1 ty2) eqns }
where
loc = bumpCtLocDepth (ctEvLoc ev)
-- ToDo: this location is wrong; it should be FunDepOrigin2
-- See #14778
+ rewriters = ctEvRewriters ev
improve_top_fun_eqs :: FamInstEnvs
-> TyCon -> [TcType] -> TcType
@@ -2103,10 +2112,10 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args
, evCoercion (mkTcSymCo ax_co
`mkTcTransCo` ctEvCoercion old_ev) )
- CtWanted { ctev_report_as = report_as } ->
+ CtWanted { ctev_rewriters = rewriters } ->
-- See TcCanonical Note [Equalities with incompatible kinds] about NoBlockSubst
do { (new_ev, new_co) <- newWantedEq_SI NoBlockSubst WDeriv deeper_loc
- report_as Nominal
+ rewriters Nominal
(mkTyConApp fam_tc tc_args) (mkTyVarTy fsk)
; setWantedEq (ctev_dest old_ev) $ ax_co `mkTcTransCo` new_co
; return new_ev }
@@ -2356,15 +2365,16 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = ev, cc_class = cls
try_fundep_improvement
= do { traceTcS "try_fundeps" (ppr work_item)
; instEnvs <- getInstEnvs
- ; emitFunDepDeriveds $
+ ; emitFunDepDeriveds (ctEvRewriters ev) $
improveFromInstEnv instEnvs mk_ct_loc dict_pred }
mk_ct_loc :: PredType -- From instance decl
-> SrcSpan -- also from instance deol
- -> CtLoc
+ -> (CtLoc, RewriterSet)
mk_ct_loc inst_pred inst_loc
- = dict_loc { ctl_origin = FunDepOrigin2 dict_pred dict_origin
- inst_pred inst_loc }
+ = ( dict_loc { ctl_origin = FunDepOrigin2 dict_pred dict_origin
+ inst_pred inst_loc }
+ , emptyRewriterSet )
doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
@@ -2392,7 +2402,7 @@ chooseInstance work_item
then -- See Note [Instances in no-evidence implications]
continueWith work_item
else
- do { evc_vars <- mapM (newWanted loc (ctReportAs work_item)) theta
+ do { evc_vars <- mapM (newWanted loc (ctRewriters work_item)) theta
; setEvBindIfWanted ev (mk_ev (map getEvExpr evc_vars))
; emitWorkNC (freshGoals evc_vars)
; stopWith ev "Dict/Top (solved wanted)" } }
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -3201,10 +3201,10 @@ zonkTyCoVarKind tv = wrapTcS (TcM.zonkTyCoVarKind tv)
* *
********************************************************************* -}
-newFlattenSkolem :: CtFlavour -> CtLoc -> CtReportAs
+newFlattenSkolem :: CtFlavour -> CtLoc -> RewriterSet
-> TyCon -> [TcType] -- F xis
-> TcS (CtEvidence, Coercion, TcTyVar) -- [G/WD] x:: F xis ~ fsk
-newFlattenSkolem flav loc report_as tc xis
+newFlattenSkolem flav loc rewriters tc xis
= do { stuff@(ev, co, fsk) <- new_skolem
; let fsk_ty = mkTyVarTy fsk
; extendFlatCache tc xis (co, fsk_ty, ctEvFlavour ev)
@@ -3230,7 +3230,7 @@ newFlattenSkolem flav loc report_as tc xis
= do { fmv <- wrapTcS (TcM.newFmvTyVar fam_ty)
-- See (2a) in TcCanonical
-- Note [Equalities with incompatible kinds]
- ; (ev, hole_co) <- newWantedEq_SI NoBlockSubst WDeriv loc report_as
+ ; (ev, hole_co) <- newWantedEq_SI NoBlockSubst WDeriv loc rewriters
Nominal fam_ty (mkTyVarTy fmv)
; return (ev, hole_co, fmv) }
@@ -3494,43 +3494,43 @@ newBoundEvVarId pred rhs
newGivenEvVars :: CtLoc -> [(TcPredType, EvTerm)] -> TcS [CtEvidence]
newGivenEvVars loc pts = mapM (newGivenEvVar loc) pts
-emitNewWantedEq :: CtLoc -> CtReportAs -> Role -> TcType -> TcType -> TcS Coercion
+emitNewWantedEq :: CtLoc -> RewriterSet -> Role -> TcType -> TcType -> TcS Coercion
-- | Emit a new Wanted equality into the work-list
-emitNewWantedEq loc report_as role ty1 ty2
- = do { (ev, co) <- newWantedEq loc report_as role ty1 ty2
+emitNewWantedEq loc rewriters role ty1 ty2
+ = do { (ev, co) <- newWantedEq loc rewriters role ty1 ty2
; updWorkListTcS (extendWorkListEq (mkNonCanonical ev))
; return co }
-- | Make a new equality CtEvidence
-newWantedEq :: CtLoc -> CtReportAs -> Role -> TcType -> TcType
+newWantedEq :: CtLoc -> RewriterSet -> Role -> TcType -> TcType
-> TcS (CtEvidence, Coercion)
-newWantedEq loc report_as role ty1 ty2
- = newWantedEq_SI YesBlockSubst WDeriv loc report_as role ty1 ty2
+newWantedEq loc rewriters role ty1 ty2
+ = newWantedEq_SI YesBlockSubst WDeriv loc rewriters role ty1 ty2
-newWantedEq_SI :: BlockSubstFlag -> ShadowInfo -> CtLoc -> CtReportAs -> Role
+newWantedEq_SI :: BlockSubstFlag -> ShadowInfo -> CtLoc -> RewriterSet -> Role
-> TcType -> TcType
-> TcS (CtEvidence, Coercion)
-newWantedEq_SI blocker si loc report_as role ty1 ty2
+newWantedEq_SI blocker si loc rewriters role ty1 ty2
= do { hole <- wrapTcS $ TcM.newCoercionHole blocker pty
; traceTcS "Emitting new coercion hole" (ppr hole <+> dcolon <+> ppr pty)
; return ( CtWanted { ctev_pred = pty
, ctev_dest = HoleDest hole
, ctev_nosh = si
, ctev_loc = loc
- , ctev_report_as = report_as }
+ , ctev_rewriters = rewriters }
, mkHoleCo hole ) }
where
pty = mkPrimEqPredRole role ty1 ty2
-- no equalities here. Use newWantedEq instead
-newWantedEvVarNC :: CtLoc -> CtReportAs
+newWantedEvVarNC :: CtLoc -> RewriterSet
-> TcPredType -> TcS CtEvidence
newWantedEvVarNC = newWantedEvVarNC_SI WDeriv
-newWantedEvVarNC_SI :: ShadowInfo -> CtLoc -> CtReportAs
+newWantedEvVarNC_SI :: ShadowInfo -> CtLoc -> RewriterSet
-> TcPredType -> TcS CtEvidence
-- Don't look up in the solved/inerts; we know it's not there
-newWantedEvVarNC_SI si loc report_as pty
+newWantedEvVarNC_SI si loc rewriters pty
= do { new_ev <- newEvVar pty
; traceTcS "Emitting new wanted" (ppr new_ev <+> dcolon <+> ppr pty $$
pprCtLoc loc)
@@ -3538,48 +3538,48 @@ newWantedEvVarNC_SI si loc report_as pty
, ctev_dest = EvVarDest new_ev
, ctev_nosh = si
, ctev_loc = loc
- , ctev_report_as = report_as })}
+ , ctev_rewriters = rewriters })}
-newWantedEvVar_SI :: ShadowInfo -> CtLoc -> CtReportAs
+newWantedEvVar_SI :: ShadowInfo -> CtLoc -> RewriterSet
-> TcPredType -> TcS MaybeNew
-- For anything except ClassPred, this is the same as newWantedEvVarNC
-newWantedEvVar_SI si loc report_as pty
+newWantedEvVar_SI si loc rewriters pty
= do { mb_ct <- lookupInInerts loc pty
; case mb_ct of
Just ctev
| not (isDerived ctev)
-> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev
; return $ Cached (ctEvExpr ctev) }
- _ -> do { ctev <- newWantedEvVarNC_SI si loc report_as pty
+ _ -> do { ctev <- newWantedEvVarNC_SI si loc rewriters pty
; return (Fresh ctev) } }
-newWanted :: CtLoc -> CtReportAs -> PredType -> TcS MaybeNew
+newWanted :: CtLoc -> RewriterSet -> PredType -> TcS MaybeNew
-- Deals with both equalities and non equalities. Tries to look
-- up non-equalities in the cache
newWanted = newWanted_SI WDeriv
-newWanted_SI :: ShadowInfo -> CtLoc -> CtReportAs
+newWanted_SI :: ShadowInfo -> CtLoc -> RewriterSet
-> PredType -> TcS MaybeNew
-newWanted_SI si loc report_as pty
+newWanted_SI si loc rewriters pty
| Just (role, ty1, ty2) <- getEqPredTys_maybe pty
- = Fresh . fst <$> newWantedEq_SI YesBlockSubst si loc report_as role ty1 ty2
+ = Fresh . fst <$> newWantedEq_SI YesBlockSubst si loc rewriters role ty1 ty2
| otherwise
- = newWantedEvVar_SI si loc report_as pty
+ = newWantedEvVar_SI si loc rewriters pty
-- deals with both equalities and non equalities. Doesn't do any cache lookups.
-newWantedNC :: CtLoc -> PredType -> TcS CtEvidence
-newWantedNC loc pty
+newWantedNC :: CtLoc -> RewriterSet -> PredType -> TcS CtEvidence
+newWantedNC loc rewriters pty
| Just (role, ty1, ty2) <- getEqPredTys_maybe pty
- = fst <$> newWantedEq loc CtReportAsSame role ty1 ty2
+ = fst <$> newWantedEq loc rewriters role ty1 ty2
| otherwise
- = newWantedEvVarNC loc CtReportAsSame pty
+ = newWantedEvVarNC loc rewriters pty
emitNewDeriveds :: CtLoc -> [TcPredType] -> TcS ()
emitNewDeriveds loc preds
| null preds
= return ()
| otherwise
- = do { evs <- mapM (newDerivedNC loc) preds
+ = do { evs <- mapM (newDerivedNC loc emptyRewriterSet) preds
; traceTcS "Emitting new deriveds" (ppr evs)
; updWorkListTcS (extendWorkListDeriveds evs) }
@@ -3587,13 +3587,13 @@ emitNewDerivedEq :: CtLoc -> Role -> TcType -> TcType -> TcS ()
-- Create new equality Derived and put it in the work list
-- There's no caching, no lookupInInerts
emitNewDerivedEq loc role ty1 ty2
- = do { ev <- newDerivedNC loc (mkPrimEqPredRole role ty1 ty2)
+ = do { ev <- newDerivedNC loc emptyRewriterSet (mkPrimEqPredRole role ty1 ty2)
; traceTcS "Emitting new derived equality" (ppr ev $$ pprCtLoc loc)
; updWorkListTcS (extendWorkListEq (mkNonCanonical ev)) }
-- Very important: put in the wl_eqs
-- See Note [Prioritise equalities] (Avoiding fundep iteration)
-newDerivedNC :: CtLoc -> TcPredType -> TcS CtEvidence
+newDerivedNC :: CtLoc -> RewriterSet -> TcPredType -> TcS CtEvidence
newDerivedNC = newWantedNC {- "RAE"
= do { -- checkReductionDepth loc pred
; return (CtDerived { ctev_pred = pred, ctev_loc = loc }) } -}
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -1,4 +1,4 @@
-{-# LANGUAGE CPP, GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE CPP, GeneralizedNewtypeDeriving, DerivingStrategies, TypeApplications #-}
{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
@@ -17,12 +17,13 @@ module GHC.Tc.Types.Constraint (
isCNonCanonical, isWantedCt, isDerivedCt, isGivenCt,
isUserTypeError, getUserTypeErrorMsg,
ctEvidence, ctLoc, setCtLoc, ctPred, ctFlavour, ctEqRel, ctOrigin,
+ ctRewriters,
ctEvId, mkTcEqPredLikeEv,
mkNonCanonical, mkNonCanonicalCt, mkGivens,
mkIrredCt,
ctEvPred, ctEvLoc, ctEvOrigin, ctEvEqRel,
ctEvExpr, ctEvTerm, ctEvCoercion, ctEvEvId,
- ctReportAs, ctUnique,
+ ctEvRewriters,
tyCoVarsOfCt, tyCoVarsOfCts,
tyCoVarsOfCtList, tyCoVarsOfCtsList,
@@ -51,10 +52,11 @@ module GHC.Tc.Types.Constraint (
isWanted, isGiven, isDerived, isGivenOrWDeriv,
ctEvRole, setCtEvLoc, arisesFromGivens,
tyCoVarsOfCtEvList, tyCoVarsOfCtEv, tyCoVarsOfCtEvsList,
- ctEvReportAs, ctEvUnique, tcEvDestUnique,
+ ctEvUnique, tcEvDestUnique,
- CtReportAs(..), ctPredToReport, substCtReportAs,
- updateReportAs, WRWFlag(..), wantedRewriteWanted,
+ RewriterSet(..), emptyRewriterSet, isEmptyRewriterSet,
+ -- exported concretely only for anyUnfilledCoercionHoles
+ wantedRewriteWanted, rewriterSetFromCo, addRewriterSet,
wrapType,
@@ -98,13 +100,16 @@ import GHC.Types.Var.Set
import GHC.Driver.Session
import GHC.Types.Basic
import GHC.Types.Unique
+import GHC.Types.Unique.Set
import GHC.Utils.Outputable
import GHC.Types.SrcLoc
import GHC.Data.Bag
import GHC.Utils.Misc
-import qualified Data.Semigroup
+import Data.Coerce
+import Data.Monoid ( Endo(..) )
+import qualified Data.Semigroup as S
import Control.Monad ( msum )
{-
@@ -439,6 +444,9 @@ ctPred :: Ct -> PredType
-- See Note [Ct/evidence invariant]
ctPred ct = ctEvPred (ctEvidence ct)
+ctRewriters :: Ct -> RewriterSet
+ctRewriters = ctEvRewriters . ctEvidence
+
ctEvId :: Ct -> EvVar
-- The evidence Id for this Ct
ctEvId ct = ctEvEvId (ctEvidence ct)
@@ -461,17 +469,6 @@ ctFlavour = ctEvFlavour . ctEvidence
ctEqRel :: Ct -> EqRel
ctEqRel = ctEvEqRel . ctEvidence
--- | Extract a 'CtReportAs' from a 'Ct'. Works only for Wanteds;
--- will panic on other arguments
-ctReportAs :: Ct -> CtReportAs
-ctReportAs ct = case ctEvidence ct of
- CtWanted { ctev_report_as = report_as } -> report_as
- _ -> pprPanic "ctReportAs" (ppr ct)
-
--- | Extract a Unique from a 'Ct'
-ctUnique :: Ct -> Unique
-ctUnique = ctEvUnique . ctEvidence
-
instance Outputable Ct where
ppr ct = ppr (ctEvidence ct) <+> parens pp_sort
where
@@ -932,13 +929,8 @@ pprCts cts = vcat (map ppr (bagToList cts))
************************************************************************
* *
Wanted constraints
- These are forced to be in GHC.Tc.Types because
- TcLclEnv mentions WantedConstraints
- WantedConstraint mentions CtLoc
- CtLoc mentions ErrCtxt
- ErrCtxt mentions TcM
* *
-v%************************************************************************
+************************************************************************
-}
data WantedConstraints
@@ -1413,24 +1405,6 @@ data TcEvDest
-- HoleDest is always used for type-equalities
-- See Note [Coercion holes] in GHC.Core.TyCo.Rep
--- | What should we report to the user when reporting this Wanted?
--- See Note [Wanteds rewrite Wanteds]
-data CtReportAs
- = CtReportAsSame -- just report the predicate in the Ct
- | CtReportAsOther Unique TcPredType -- report this other type
- -- See GHC.Tc.Errors Note [Avoid reporting duplicates] about the Unique
-
--- | Did a wanted rewrite a wanted?
--- See Note [Wanteds rewrite Wanteds]
-data WRWFlag
- = YesWRW
- | NoWRW
- deriving Eq
-
-instance Semigroup WRWFlag where
- NoWRW <> NoWRW = NoWRW
- _ <> _ = YesWRW
-
data CtEvidence
= CtGiven -- Truly given, not depending on subgoals
{ ctev_pred :: TcPredType -- See Note [Ct/evidence invariant]
@@ -1443,7 +1417,7 @@ data CtEvidence
, ctev_dest :: TcEvDest
, ctev_nosh :: ShadowInfo -- See Note [Constraint flavours]
, ctev_loc :: CtLoc
- , ctev_report_as :: CtReportAs } -- See Note [Wanteds rewrite Wanteds]
+ , ctev_rewriters :: RewriterSet } -- See Note [Wanteds rewrite Wanteds]
| CtDerived -- A goal that we don't really have to solve and can't
-- immediately rewrite anything other than a derived
@@ -1473,6 +1447,14 @@ ctEvRole = eqRelRole . ctEvEqRel
ctEvTerm :: CtEvidence -> EvTerm
ctEvTerm ev = EvExpr (ctEvExpr ev)
+-- | Extract the set of rewriters from a 'CtEvidence'
+-- See Note [Wanteds rewrite Wanteds]
+-- If the provided CtEvidence is not for a Wanted, just
+-- return an empty set.
+ctEvRewriters :: CtEvidence -> RewriterSet
+ctEvRewriters (CtWanted { ctev_rewriters = rewriters }) = rewriters
+ctEvRewriters _other = emptyRewriterSet
+
ctEvExpr :: CtEvidence -> EvExpr
ctEvExpr ev@(CtWanted { ctev_dest = HoleDest _ })
= Coercion $ ctEvCoercion ev
@@ -1512,48 +1494,14 @@ arisesFromGivens Given _ = True
arisesFromGivens (Wanted {}) loc = isGivenLoc loc -- could be a Given FunDep
arisesFromGivens Derived loc = isGivenLoc loc
--- | Return a 'CtReportAs' from a 'CtEvidence'. Returns
--- 'CtReportAsSame' for non-wanteds.
-ctEvReportAs :: CtEvidence -> CtReportAs
-ctEvReportAs (CtWanted { ctev_report_as = report_as }) = report_as
-ctEvReportAs _ = CtReportAsSame
-
--- | Given the pred in a CtWanted and its 'CtReportAs', get
--- the pred to report. See Note [Wanteds rewrite Wanteds]
-ctPredToReport :: TcEvDest -> TcPredType -> CtReportAs -> (Unique, TcPredType)
-ctPredToReport dest pred CtReportAsSame = (tcEvDestUnique dest, pred)
-ctPredToReport _ _ (CtReportAsOther u pred) = (u, pred)
-
--- | Substitute in a 'CtReportAs'
-substCtReportAs :: TCvSubst -> CtReportAs -> CtReportAs
-substCtReportAs _ CtReportAsSame = CtReportAsSame
-substCtReportAs subst (CtReportAsOther u pred) = CtReportAsOther u (substTy subst pred)
-
--- | After rewriting a Wanted, update the 'CtReportAs' for the new Wanted.
--- If the old CtReportAs is CtReportAsSame and a wanted rewrote a wanted,
--- record the old pred as the new CtReportAs.
--- See Note [Wanteds rewrite Wanteds]
-updateReportAs :: WRWFlag -> Unique -> TcPredType -- _old_ pred type
- -> CtReportAs -> CtReportAs
-updateReportAs YesWRW unique old_pred CtReportAsSame = CtReportAsOther unique old_pred
-updateReportAs _ _ _ report_as = report_as
-
instance Outputable TcEvDest where
ppr (HoleDest h) = text "hole" <> ppr h
ppr (EvVarDest ev) = ppr ev
-instance Outputable CtReportAs where
- ppr CtReportAsSame = text "CtReportAsSame"
- ppr (CtReportAsOther u pred) = parens $ text "CtReportAsOther" <+> ppr u <+> ppr pred
-
-instance Outputable WRWFlag where
- ppr NoWRW = text "NoWRW"
- ppr YesWRW = text "YesWRW"
-
instance Outputable CtEvidence where
ppr ev = ppr (ctEvFlavour ev)
<+> pp_ev
- <+> braces (ppr (ctl_depth (ctEvLoc ev))) <> dcolon
+ <+> braces (ppr (ctl_depth (ctEvLoc ev)) <> pp_rewriters) <> dcolon
-- Show the sub-goal depth too
<+> ppr (ctEvPred ev)
where
@@ -1562,6 +1510,10 @@ instance Outputable CtEvidence where
CtWanted {ctev_dest = d } -> ppr d
CtDerived {} -> text "_"
+ rewriters = ctEvRewriters ev
+ pp_rewriters | isEmptyRewriterSet rewriters = empty
+ | otherwise = semi <> ppr rewriters
+
isWanted :: CtEvidence -> Bool
isWanted (CtWanted {}) = True
isWanted _ = False
@@ -1575,11 +1527,50 @@ isDerived (CtDerived {}) = True
isDerived _ = False
{-
-%************************************************************************
-%* *
- CtFlavour
-%* *
-%************************************************************************
+************************************************************************
+* *
+ RewriterSet
+* *
+************************************************************************
+-}
+
+-- | Stores a set of CoercionHoles that have been used to rewrite a constraint.
+-- See Note [Wanteds rewrite Wanteds].
+newtype RewriterSet = RewriterSet (UniqSet CoercionHole)
+ deriving newtype (Outputable, Semigroup, Monoid)
+
+emptyRewriterSet :: RewriterSet
+emptyRewriterSet = RewriterSet emptyUniqSet
+
+isEmptyRewriterSet :: RewriterSet -> Bool
+isEmptyRewriterSet (RewriterSet set) = isEmptyUniqSet set
+
+addRewriterSet :: RewriterSet -> CoercionHole -> RewriterSet
+addRewriterSet = coerce (addOneToUniqSet @CoercionHole)
+
+-- | Makes a 'RewriterSet' from all the coercion holes that occur in the
+-- given coercion.
+rewriterSetFromCo :: Coercion -> RewriterSet
+rewriterSetFromCo co = appEndo (go_co co) emptyRewriterSet
+ where
+ go_co :: Coercion -> Endo RewriterSet
+ (go_ty, _, go_co, _) = foldTyCo folder ()
+
+ folder :: TyCoFolder () (Endo RewriterSet)
+ folder = TyCoFolder
+ { tcf_view = noView
+ , tcf_tyvar = \ _ tv -> go_ty (tyVarKind tv)
+ , tcf_covar = \ _ cv -> go_ty (varType cv)
+ , tcf_hole = \ _ hole -> coerce (`addOneToUniqSet` hole) S.<>
+ go_ty (varType (coHoleCoVar hole))
+ , tcf_tycobinder = \ _ _ _ -> () }
+
+{-
+************************************************************************
+* *
+ CtFlavour
+* *
+************************************************************************
Note [Constraint flavours]
~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1743,9 +1734,9 @@ eqMayRewriteFR fr1 fr2 = eqCanRewriteFR fr1 fr2
-- | Checks if the first flavour rewriting the second is a wanted
-- rewriting a wanted. See Note [Wanteds rewrite Wanteds]
-wantedRewriteWanted :: CtFlavourRole -> CtFlavourRole -> WRWFlag
-wantedRewriteWanted (Wanted _, _) _ = YesWRW
-wantedRewriteWanted _ _ = NoWRW
+wantedRewriteWanted :: CtFlavourRole -> CtFlavourRole -> Bool
+wantedRewriteWanted (Wanted _, _) _ = True
+wantedRewriteWanted _ _ = False
-- It doesn't matter what the second argument is; it can only
-- be Wanted or Derived anyway
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -89,7 +89,11 @@ module GHC.Tc.Utils.TcMType (
------------------------------
-- Levity polymorphism
- ensureNotLevPoly, checkForLevPoly, checkForLevPolyX, formatLevPolyErr
+ ensureNotLevPoly, checkForLevPoly, checkForLevPolyX, formatLevPolyErr,
+
+ ------------------------------
+ -- Other
+ anyUnfilledCoercionHoles
) where
#include "HsVersions.h"
@@ -190,7 +194,7 @@ newWanted orig t_or_k pty
, ctev_pred = pty
, ctev_nosh = WDeriv
, ctev_loc = loc
- , ctev_report_as = CtReportAsSame }
+ , ctev_rewriters = emptyRewriterSet }
newWanteds :: CtOrigin -> ThetaType -> TcM [CtEvidence]
newWanteds orig = mapM (newWanted orig Nothing)
@@ -254,7 +258,7 @@ emitWantedEq origin t_or_k role ty1 ty2
, ctev_dest = HoleDest hole
, ctev_nosh = WDeriv
, ctev_loc = loc
- , ctev_report_as = CtReportAsSame }
+ , ctev_rewriters = emptyRewriterSet }
; return (HoleCo hole) }
where
pty = mkPrimEqPredRole role ty1 ty2
@@ -269,7 +273,7 @@ emitWantedEvVar origin ty
, ctev_pred = ty
, ctev_nosh = WDeriv
, ctev_loc = loc
- , ctev_report_as = CtReportAsSame }
+ , ctev_rewriters = emptyRewriterSet }
; emitSimple $ mkNonCanonical ctev
; return new_cv }
@@ -2077,18 +2081,13 @@ zonkCtEvidence ctev@(CtGiven { ctev_pred = pred })
= do { pred' <- zonkTcType pred
; return (ctev { ctev_pred = pred'}) }
zonkCtEvidence ctev@(CtWanted { ctev_pred = pred
- , ctev_dest = dest
- , ctev_report_as = report_as })
+ , ctev_dest = dest })
= do { pred' <- zonkTcType pred
; let dest' = case dest of
EvVarDest ev -> EvVarDest $ setVarType ev pred'
-- necessary in simplifyInfer
HoleDest h -> HoleDest h
- ; report_as' <- case report_as of
- CtReportAsSame -> return CtReportAsSame
- CtReportAsOther u report_pred -> CtReportAsOther u <$> zonkTcType report_pred
- ; return (ctev { ctev_pred = pred', ctev_dest = dest'
- , ctev_report_as = report_as' }) }
+ ; return (ctev { ctev_pred = pred', ctev_dest = dest' }) }
zonkCtEvidence ctev@(CtDerived { ctev_pred = pred })
= do { pred' <- zonkTcType pred
; return (ctev { ctev_pred = pred' }) }
@@ -2103,14 +2102,11 @@ zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
zonkSkolemInfo skol_info = return skol_info
{-
-%************************************************************************
-%* *
-\subsection{Zonking -- the main work-horses: zonkTcType, zonkTcTyVar}
+************************************************************************
* *
-* For internal use only! *
+ Zonking -- the main work-horses: zonkTcType, zonkTcTyVar
* *
************************************************************************
-
-}
-- For unbound, mutable tyvars, zonkType uses the function given to it
@@ -2275,12 +2271,6 @@ tidyCt env ct = ct { cc_ev = tidyCtEvidence env (ctEvidence ct) }
tidyCtEvidence :: TidyEnv -> CtEvidence -> CtEvidence
-- NB: we do not tidy the ctev_evar field because we don't
-- show it in error messages
- -- But definitely do tidy the report_as field, as that's reported.
-tidyCtEvidence env ctev@(CtWanted { ctev_pred = pred, ctev_report_as = report_as })
- = ctev { ctev_pred = tidyType env pred, ctev_report_as = tidy_report_as report_as }
- where tidy_report_as CtReportAsSame = CtReportAsSame
- tidy_report_as (CtReportAsOther u report_pred)
- = CtReportAsOther u (tidyType env report_pred)
tidyCtEvidence env ctev = ctev { ctev_pred = tidyType env ty }
where
ty = ctev_pred ctev
@@ -2330,11 +2320,11 @@ tidySigSkol env cx ty tv_prs
-------------------------------------------------------------------------
{-
-%************************************************************************
-%* *
+************************************************************************
+* *
Levity polymorphism checks
-* *
-*************************************************************************
+* *
+************************************************************************
See Note [Levity polymorphism checking] in GHC.HsToCore.Monad
@@ -2424,3 +2414,46 @@ naughtyQuantification orig_ty tv escapees
]
; failWithTcM (env, doc) }
+
+{-
+************************************************************************
+* *
+ Checking for coercion holes
+* *
+************************************************************************
+-}
+
+-- | Check whether any coercion hole in a RewriterSet is still unsolved.
+-- Does this by recursively looking through filled coercion holes until
+-- one is found that is not yet filled in, at which point this aborts.
+anyUnfilledCoercionHoles :: RewriterSet -> TcM Bool
+anyUnfilledCoercionHoles (RewriterSet set)
+ = nonDetFoldUniqSet go (return False) set
+ where
+ go :: CoercionHole -> TcM Bool -> TcM Bool
+ go hole m_acc = m_acc <||> check_hole hole
+
+ check_hole :: CoercionHole -> TcM Bool
+ check_hole hole = do { m_co <- unpackCoercionHole_maybe hole
+ ; case m_co of
+ Nothing -> return True -- unfilled hole
+ Just co -> unUCHM (check_co co) }
+
+ check_ty :: Type -> UnfilledCoercionHoleMonoid
+ check_co :: Coercion -> UnfilledCoercionHoleMonoid
+ (check_ty, _, check_co, _) = foldTyCo folder ()
+
+ folder :: TyCoFolder () UnfilledCoercionHoleMonoid
+ folder = TyCoFolder { tcf_view = noView
+ , tcf_tyvar = \ _ tv -> check_ty (tyVarKind tv)
+ , tcf_covar = \ _ cv -> check_ty (varType cv)
+ , tcf_hole = \ _ -> UCHM . check_hole
+ , tcf_tycobinder = \ _ _ _ -> () }
+
+newtype UnfilledCoercionHoleMonoid = UCHM { unUCHM :: TcM Bool }
+
+instance Semigroup UnfilledCoercionHoleMonoid where
+ UCHM l <> UCHM r = UCHM (l <||> r)
+
+instance Monoid UnfilledCoercionHoleMonoid where
+ mempty = UCHM (return False)
=====================================
testsuite/tests/partial-sigs/should_fail/T10999.stderr
=====================================
@@ -17,15 +17,15 @@ T10999.hs:5:17: error:
In the type signature: f :: _ => () -> _
T10999.hs:8:28: error:
- • Ambiguous type variable ‘b0’ arising from a use of ‘f’
- prevents the constraint ‘(Ord b0)’ from being solved.
- Relevant bindings include g :: [b0] (bound at T10999.hs:8:1)
- Probable fix: use a type annotation to specify what ‘b0’ should be.
+ • Ambiguous type variable ‘b1’ arising from a use of ‘f’
+ prevents the constraint ‘(Ord b1)’ from being solved.
+ Relevant bindings include g :: [b1] (bound at T10999.hs:8:1)
+ Probable fix: use a type annotation to specify what ‘b1’ should be.
These potential instances exist:
instance Ord a => Ord (Set.Set a) -- Defined in ‘Data.Set.Internal’
instance Ord Ordering -- Defined in ‘GHC.Classes’
instance Ord Integer
- -- Defined in ‘integer-gmp-1.0.1.0:GHC.Integer.Type’
+ -- Defined in ‘integer-gmp-1.0.3.0:GHC.Integer.Type’
...plus 22 others
...plus three instances involving out-of-scope types
(use -fprint-potential-instances to see them all)
=====================================
testsuite/tests/typecheck/should_fail/T12785b.stderr
=====================================
@@ -1,6 +1,6 @@
T12785b.hs:29:65: error:
- • Could not deduce: s ~ Payload ('S n) (Payload n s1)
+ • Could not deduce: Payload ('S n) (Payload n s1) ~ s
arising from a use of ‘SBranchX’
from the context: m ~ 'S n
bound by a pattern with constructor:
=====================================
testsuite/tests/typecheck/should_fail/T15648.stderr
=====================================
@@ -11,13 +11,20 @@ T15648.hs:23:21: error:
legitToJank :: LegitEquality a b -> JankyEquality a b
(bound at T15648.hs:23:1)
-T15648.hs:30:10: error:
- • Couldn't match expected type ‘(a GHC.Prim.~# b)
- -> b GHC.Prim.~# a’
- with actual type ‘b GHC.Prim.~# a’
- • In the expression: unJank $ legitToJank $ mkLegit @b @a
- In an equation for ‘ueqSym’:
- ueqSym = unJank $ legitToJank $ mkLegit @b @a
+T15648.hs:30:33: error:
+ • Couldn't match expected type ‘a’ with actual type ‘b’
+ ‘b’ is a rigid type variable bound by
+ the type signature for:
+ ueqSym :: forall a b. (a GHC.Prim.~# b) -> b GHC.Prim.~# a
+ at T15648.hs:(28,1)-(29,32)
+ ‘a’ is a rigid type variable bound by
+ the type signature for:
+ ueqSym :: forall a b. (a GHC.Prim.~# b) -> b GHC.Prim.~# a
+ at T15648.hs:(28,1)-(29,32)
+ • In the second argument of ‘($)’, namely ‘mkLegit @b @a’
+ In the second argument of ‘($)’, namely
+ ‘legitToJank $ mkLegit @b @a’
+ In the expression: unJank $ legitToJank $ mkLegit @b @a
• Relevant bindings include
ueqSym :: (a GHC.Prim.~# b) -> b GHC.Prim.~# a
(bound at T15648.hs:30:1)
=====================================
testsuite/tests/typecheck/should_fail/T8450.stderr
=====================================
@@ -1,11 +1,15 @@
-T8450.hs:8:7: error:
- • Couldn't match expected type ‘a’ with actual type ‘()’
+T8450.hs:8:20: error:
+ • Couldn't match type ‘a’ with ‘Bool’
‘a’ is a rigid type variable bound by
the type signature for:
run :: forall a. a
at T8450.hs:7:1-18
- • In the expression: runEffect $ (undefined :: Either a ())
+ Expected type: Either Bool ()
+ Actual type: Either a ()
+ • In the second argument of ‘($)’, namely
+ ‘(undefined :: Either a ())’
+ In the expression: runEffect $ (undefined :: Either a ())
In an equation for ‘run’:
run = runEffect $ (undefined :: Either a ())
• Relevant bindings include run :: a (bound at T8450.hs:8:1)
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/f5433f0bc06f65deb96a44b62d47875ec4bc5b38...5d3804aec65f0801363c28ca3bb8a15f4ef3e6db
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/f5433f0bc06f65deb96a44b62d47875ec4bc5b38...5d3804aec65f0801363c28ca3bb8a15f4ef3e6db
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20200625/42b03fc5/attachment-0001.html>
More information about the ghc-commits
mailing list