diff options
Diffstat (limited to 'compiler/GHC/Tc')
| -rw-r--r-- | compiler/GHC/Tc/Errors.hs | 32 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Errors/Types.hs | 2 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Gen/HsType.hs | 12 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Gen/Rule.hs | 38 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Plugin.hs | 2 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver.hs | 13 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver/Canonical.hs | 87 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver/Dict.hs | 112 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver/Equality.hs | 488 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver/InertSet.hs | 202 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver/Interact.hs | 79 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver/Monad.hs | 435 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver/Rewrite.hs | 5 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Types/Constraint.hs | 226 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Types/Evidence.hs | 2 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Types/Origin.hs | 5 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/Concrete.hs | 3 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/TcMType.hs | 102 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/TcType.hs | 13 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/Unify.hs | 409 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/Unify.hs-boot | 5 |
21 files changed, 1324 insertions, 948 deletions
diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs index ed102d9bb5..66f0cf118a 100644 --- a/compiler/GHC/Tc/Errors.hs +++ b/compiler/GHC/Tc/Errors.hs @@ -462,8 +462,8 @@ mkErrorItem 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) } + -> do { rewriters' <- zonkRewriterSet rewriters + ; return (not (isEmptyRewriterSet rewriters'), Just dest) } ; let m_reason = case ct of CIrredCan { cc_reason = reason } -> Just reason _ -> Nothing @@ -492,20 +492,24 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics , text "tidy_items1 =" <+> ppr tidy_items1 , text "tidy_errs =" <+> ppr tidy_errs ]) - -- Catch an awkward case in which /all/ errors are suppressed: - -- see Wrinkle at end of Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint - -- Unless we are sure that an error will be reported some other way (details - -- in the defn of tidy_items) un-suppress the lot. This makes sure we don't forget to - -- report an error at all, which is catastrophic: GHC proceeds to desguar and optimise - -- the program, even though it is full of type errors (#22702, #22793) + -- Catch an awkward (and probably rare) case in which /all/ errors are + -- suppressed: see Wrinkle (WRW2) in Note [Prioritise Wanteds with empty + -- RewriterSet] in GHC.Tc.Types.Constraint. + -- + -- Unless we are sure that an error will be reported some other way + -- (details in the defn of tidy_items) un-suppress the lot. This makes + -- sure we don't forget to report an error at all, which is + -- catastrophic: GHC proceeds to desguar and optimise the program, even + -- though it is full of type errors (#22702, #22793) ; errs_already <- ifErrsM (return True) (return False) ; let tidy_items | not errs_already -- Have not already reported an error (perhaps -- from an outer implication); see #21405 , not (any ignoreConstraint simples) -- No error is ignorable (is reported elsewhere) , all ei_suppress tidy_items1 -- All errors are suppressed - = map unsuppressErrorItem tidy_items1 - | otherwise = tidy_items1 + = map unsuppressErrorItem tidy_items1 + | otherwise + = tidy_items1 -- First, deal with any out-of-scope errors: ; let (out_of_scope, other_holes, not_conc_errs) = partition_errors tidy_errs @@ -1804,8 +1808,8 @@ mkTyVarEqErr' ctxt item (tv1, co1) ty2 return (main_msg, []) -- Incompatible kinds - -- This is wrinkle (4) in Note [Equalities with incompatible kinds] in - -- GHC.Tc.Solver.Canonical + -- This is wrinkle (EIK2) in Note [Equalities with incompatible kinds] + -- in GHC.Tc.Solver.Equality | hasCoercionHoleCo co1 || hasCoercionHoleTy ty2 = return (mkBlockedEqErr item, []) @@ -1987,8 +1991,8 @@ misMatchOrCND insoluble_occurs_check ctxt item ty1 ty2 -- Keep only UserGivens that have some equalities. -- See Note [Suppress redundant givens during error reporting] --- These are for the "blocked" equalities, as described in TcCanonical --- Note [Equalities with incompatible kinds], wrinkle (2). There should +-- These are for the "blocked" equalities, as described in GHC.Tc.Solver.Equality +-- Note [Equalities with incompatible kinds], wrinkle (EIK2). There should -- 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. diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs index 68c5ca2869..4c2d29a0b5 100644 --- a/compiler/GHC/Tc/Errors/Types.hs +++ b/compiler/GHC/Tc/Errors/Types.hs @@ -4755,7 +4755,7 @@ data TcSolverReportMsg | BlockedEquality ErrorItem -- These are for the "blocked" equalities, as described in -- Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical, - -- wrinkle (2). There should always be another unsolved wanted around, + -- wrinkle (EIK2). There should 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. diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs index 9e8375b47d..dd1b0c0eca 100644 --- a/compiler/GHC/Tc/Gen/HsType.hs +++ b/compiler/GHC/Tc/Gen/HsType.hs @@ -388,11 +388,11 @@ kcClassSigType :: [LocatedN Name] -> LHsSigType GhcRn -> TcM () -- meth :: forall a (x :: f a). Proxy x -> () -- When instantiating Proxy with kappa, we must unify kappa := f a. But we're -- still working out the kind of f, and thus f a will have a coercion in it. --- Coercions block unification (Note [Equalities with incompatible kinds] in --- TcCanonical) and so we fail to unify. If we try to kind-generalize, we'll --- end up promoting kappa to the top level (because kind-generalization is --- normally done right before adding a binding to the context), and then we --- can't set kappa := f a, because a is local. +-- Coercions may block unification (Note [Equalities with incompatible kinds] in +-- GHC.Tc.Solver.Equality, wrinkle (EIK2)) and so we fail to unify. If we try to +-- kind-generalize, we'll end up promoting kappa to the top level (because +-- kind-generalization is normally done right before adding a binding to the context), +-- and then we can't set kappa := f a, because a is local. kcClassSigType names sig_ty@(L _ (HsSig { sig_bndrs = hs_outer_bndrs, sig_body = hs_ty })) = addSigCtxt (funsSigCtxt names) sig_ty $ @@ -1932,7 +1932,7 @@ checkExpectedKind hs_ty ty act_kind exp_kind ; if act_kind' `tcEqType` exp_kind then return res_ty -- This is very common - else do { co_k <- uType KindLevel origin act_kind' exp_kind + else do { co_k <- unifyTypeAndEmit KindLevel origin act_kind' exp_kind ; traceTc "checkExpectedKind" (vcat [ ppr act_kind , ppr exp_kind , ppr co_k ]) diff --git a/compiler/GHC/Tc/Gen/Rule.hs b/compiler/GHC/Tc/Gen/Rule.hs index 121c43b987..397acd214c 100644 --- a/compiler/GHC/Tc/Gen/Rule.hs +++ b/compiler/GHC/Tc/Gen/Rule.hs @@ -133,7 +133,7 @@ tcRule (HsRule { rd_ext = ext , ppr lhs_wanted , ppr rhs_wanted ]) - ; (lhs_evs, residual_lhs_wanted) + ; (lhs_evs, residual_lhs_wanted, dont_default) <- simplifyRule name tc_lvl lhs_wanted rhs_wanted -- SimplifyRule Plan, step 4 @@ -153,15 +153,14 @@ tcRule (HsRule { rd_ext = ext -- See Note [Re-quantify type variables in rules] ; forall_tkvs <- candidateQTyVarsOfTypes (rule_ty : map idType tpl_ids) - ; let don't_default = nonDefaultableTyVarsOfWC residual_lhs_wanted - ; let weed_out = (`dVarSetMinusVarSet` don't_default) + ; let weed_out = (`dVarSetMinusVarSet` dont_default) quant_cands = forall_tkvs { dv_kvs = weed_out (dv_kvs forall_tkvs) , dv_tvs = weed_out (dv_tvs forall_tkvs) } ; qtkvs <- quantifyTyVars skol_info DefaultNonStandardTyVars quant_cands ; traceTc "tcRule" (vcat [ pprFullRuleName (snd ext) rname , text "forall_tkvs:" <+> ppr forall_tkvs , text "quant_cands:" <+> ppr quant_cands - , text "don't_default:" <+> ppr don't_default + , text "dont_default:" <+> ppr dont_default , text "residual_lhs_wanted:" <+> ppr residual_lhs_wanted , text "qtkvs:" <+> ppr qtkvs , text "rule_ty:" <+> ppr rule_ty @@ -401,7 +400,8 @@ simplifyRule :: RuleName -> WantedConstraints -- Constraints from LHS -> WantedConstraints -- Constraints from RHS -> TcM ( [EvVar] -- Quantify over these LHS vars - , WantedConstraints) -- Residual un-quantified LHS constraints + , WantedConstraints -- Residual un-quantified LHS constraints + , TcTyVarSet ) -- Don't default these -- See Note [The SimplifyRule Plan] -- NB: This consumes all simple constraints on the LHS, but not -- any LHS implication constraints. @@ -413,14 +413,23 @@ simplifyRule name tc_lvl lhs_wanted rhs_wanted -- Why clone? See Note [Simplify cloned constraints] ; lhs_clone <- cloneWC lhs_wanted ; rhs_clone <- cloneWC rhs_wanted - ; setTcLevel tc_lvl $ - discardResult $ - runTcS $ - do { _ <- solveWanteds lhs_clone - ; _ <- solveWanteds rhs_clone - -- Why do them separately? - -- See Note [Solve order for RULES] - ; return () } + ; (dont_default, _) + <- setTcLevel tc_lvl $ + runTcS $ + do { lhs_wc <- solveWanteds lhs_clone + ; _rhs_wc <- solveWanteds rhs_clone + -- Why do them separately? + -- See Note [Solve order for RULES] + + ; let dont_default = nonDefaultableTyVarsOfWC lhs_wc + -- If lhs_wanteds has + -- (a[sk] :: TYPE rr[sk]) ~ (b0[tau] :: TYPE r0[conc]) + -- we want r0 to be non-defaultable; + -- see nonDefaultableTyVarsOfWC. Simplest way to get + -- this is to look at the post-simplified lhs_wc, which + -- will contain (rr[sk] ~ r0[conc)]. An example is in + -- test rep-poly/RepPolyRule1 + ; return dont_default } -- Note [The SimplifyRule Plan] step 2 ; lhs_wanted <- zonkWC lhs_wanted @@ -435,9 +444,10 @@ simplifyRule name tc_lvl lhs_wanted rhs_wanted , text "rhs_wanted" <+> ppr rhs_wanted , text "quant_cts" <+> ppr quant_cts , text "residual_lhs_wanted" <+> ppr residual_lhs_wanted + , text "dont_default" <+> ppr dont_default ] - ; return (quant_evs, residual_lhs_wanted) } + ; return (quant_evs, residual_lhs_wanted, dont_default) } where mk_quant_ev :: Ct -> TcM EvVar diff --git a/compiler/GHC/Tc/Plugin.hs b/compiler/GHC/Tc/Plugin.hs index 30f5ef7520..df532f7ac2 100644 --- a/compiler/GHC/Tc/Plugin.hs +++ b/compiler/GHC/Tc/Plugin.hs @@ -184,7 +184,7 @@ newEvVar = unsafeTcPluginTcM . TcM.newEvVar -- | Create a fresh coercion hole. -- This should only be invoked within 'tcPluginSolve'. newCoercionHole :: PredType -> TcPluginM CoercionHole -newCoercionHole = unsafeTcPluginTcM . TcM.newCoercionHole +newCoercionHole = unsafeTcPluginTcM . TcM.newVanillaCoercionHole -- | Bind an evidence variable. -- diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs index eaa62e44ea..9c371af463 100644 --- a/compiler/GHC/Tc/Solver.hs +++ b/compiler/GHC/Tc/Solver.hs @@ -3088,6 +3088,18 @@ neededEvVars implic@(Implic { ic_given = givens ------------------------------------------------- simplifyDelayedErrors :: Bag DelayedError -> TcS (Bag DelayedError) +-- Simplify any delayed errors: e.g. type and term holes +-- NB: At this point we have finished with all the simple +-- constraints; they are in wc_simple, not in the inert set. +-- So those Wanteds will not rewrite these delayed errors. +-- That's probably no bad thing. +-- +-- However if we have [W] alpha ~ Maybe a, [W] alpha ~ Int +-- and _ : alpha, then we'll /unify/ alpha with the first of +-- the Wanteds we get, and thereby report (_ : Maybe a) or +-- (_ : Int) unpredictably, depending on which we happen to see +-- first. Doesn't matter much; there is a type error anyhow. +-- T17139 is a case in point. simplifyDelayedErrors = mapBagM simpl_err where simpl_err :: DelayedError -> TcS DelayedError @@ -3104,6 +3116,7 @@ simplifyDelayedErrors = mapBagM simpl_err -- code, because we have all the givens already set up simpl_hole h@(Hole { hole_ty = ty, hole_loc = loc }) = do { ty' <- rewriteType loc ty + ; traceTcS "simpl_hole" (ppr ty $$ ppr ty') ; return (h { hole_ty = ty' }) } {- Note [Delete dead Given evidence bindings] diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs index 187cdc9c8b..49210cefa8 100644 --- a/compiler/GHC/Tc/Solver/Canonical.hs +++ b/compiler/GHC/Tc/Solver/Canonical.hs @@ -5,7 +5,6 @@ module GHC.Tc.Solver.Canonical( canonicalize, - unifyWanted, makeSuperClasses, StopOrContinue(..), stopWith, continueWith, andWhenContinue, solveCallStack -- For GHC.Tc.Solver @@ -144,7 +143,7 @@ canClassNC ev cls tys = do { dflags <- getDynFlags ; sc_cts <- mkStrictSuperClasses (givensFuel dflags) ev [] [] cls tys -- givensFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel] - ; emitWork sc_cts + ; emitWork (listToBag sc_cts) ; canClass ev cls tys doNotExpand } -- doNotExpand: We have already expanded superclasses for /this/ dict -- so set the fuel to doNotExpand to avoid repeating expansion @@ -211,15 +210,13 @@ canClass ev cls tys pend_sc = -- all classes do *nominal* matching assertPpr (ctEvRole ev == Nominal) (ppr ev $$ ppr cls $$ ppr tys) $ do { (redns@(Reductions _ xis), rewriters) <- rewriteArgsNom ev cls_tc tys - ; let redn@(Reduction _ xi) = mkClassPredRedn cls redns - mk_ct new_ev = CDictCan { cc_ev = new_ev - , cc_tyargs = xis - , cc_class = cls - , cc_pend_sc = pend_sc } - ; mb <- rewriteEvidence rewriters ev redn - ; traceTcS "canClass" (vcat [ ppr ev - , ppr xi, ppr mb ]) - ; return (fmap mk_ct mb) } + ; let redn = mkClassPredRedn cls redns + ; rewriteEvidence rewriters ev redn $ \new_ev -> + do { traceTcS "canClass" (vcat [ ppr new_ev, ppr (reductionReducedType redn) ]) + ; continueWith (CDictCan { cc_ev = new_ev + , cc_tyargs = xis + , cc_class = cls + , cc_pend_sc = pend_sc }) }} where cls_tc = classTyCon cls @@ -738,7 +735,7 @@ canIrred ev = do { let pred = ctEvPred ev ; traceTcS "can_pred" (text "IrredPred = " <+> ppr pred) ; (redn, rewriters) <- rewrite ev pred - ; rewriteEvidence rewriters ev redn `andWhenContinue` \ new_ev -> + ; rewriteEvidence rewriters ev redn $ \ new_ev -> do { -- Re-classify, in case rewriting has improved its shape -- Code is like the canNC, except @@ -843,7 +840,7 @@ canForAllNC ev tvs theta pred = do { dflags <- getDynFlags ; sc_cts <- mkStrictSuperClasses (givensFuel dflags) ev tvs theta cls tys -- givensFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel] - ; emitWork sc_cts + ; emitWork (listToBag sc_cts) ; canForAll ev doNotExpand } -- doNotExpand: as we have already (eagerly) expanded superclasses for this class @@ -863,9 +860,8 @@ canForAll :: CtEvidence -> ExpansionFuel -> TcS (StopOrContinue Ct) -- We have a constraint (forall as. blah => C tys) canForAll ev fuel = do { -- First rewrite it to apply the current substitution - let pred = ctEvPred ev - ; (redn, rewriters) <- rewrite ev pred - ; rewriteEvidence rewriters ev redn `andWhenContinue` \ new_ev -> + ; (redn, rewriters) <- rewrite ev (ctEvPred ev) + ; rewriteEvidence rewriters ev redn $ \ new_ev -> do { -- Now decompose into its pieces and solve it -- (It takes a lot less code to rewrite before decomposing.) @@ -979,32 +975,29 @@ rewriteEvidence :: RewriterSet -- ^ See Note [Wanteds rewrite Wanteds] -- in GHC.Tc.Types.Constraint -> CtEvidence -- ^ old evidence -> Reduction -- ^ new predicate + coercion, of type <type of old evidence> ~ new predicate - -> TcS (StopOrContinue CtEvidence) --- Returns Just new_ev iff either (i) 'co' is reflexivity --- or (ii) 'co' is not reflexivity, and 'new_pred' not cached --- In either case, there is nothing new to do with new_ev -{- - rewriteEvidence old_ev new_pred co -Main purpose: create new evidence for new_pred; - unless new_pred is cached already -* Returns a new_ev : new_pred, with same wanted/given flag as old_ev -* If old_ev was wanted, create a binding for old_ev, in terms of new_ev -* If old_ev was given, AND not cached, create a binding for new_ev, in terms of old_ev -* Returns Nothing if new_ev is already cached - - Old evidence New predicate is Return new evidence - flavour of same flavor - ------------------------------------------------------------------- - Wanted Already solved or in inert Nothing - Not Just new_evidence - - Given Already in inert Nothing - Not Just new_evidence - -Note [Rewriting with Refl] -~~~~~~~~~~~~~~~~~~~~~~~~~~ + -> (CtEvidence -> TcS (StopOrContinue Ct)) + -> TcS (StopOrContinue Ct) +-- (rewriteEvidence old_ev new_pred co do_next) +-- Main purpose: create new evidence for new_pred; +-- unless new_pred is cached already +-- * Calls do_next with (new_ev :: new_pred), with same wanted/given flag as old_ev +-- * If old_ev was wanted, create a binding for old_ev, in terms of new_ev +-- * If old_ev was given, AND not cached, create a binding for new_ev, in terms of old_ev +-- * Stops if new_ev is already cached +-- +-- Old evidence New predicate is Return new evidence +-- flavour of same flavor +-- ------------------------------------------------------------------- +-- Wanted Already solved or in inert Stop +-- Not do_next new_evidence +-- +-- Given Already in inert Stop +-- Not do_next new_evidence + +{- Note [Rewriting with Refl] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ If the coercion is just reflexivity then you may re-use the same -variable. But be careful! Although the coercion is Refl, new_pred +evidence variable. But be careful! Although the coercion is Refl, new_pred may reflect the result of unification alpha := ty, so new_pred might not _look_ the same as old_pred, and it's vital to proceed from now on using new_pred. @@ -1017,16 +1010,16 @@ the rewriter set. We check this with an assertion. -} -rewriteEvidence rewriters old_ev (Reduction co new_pred) +rewriteEvidence rewriters old_ev (Reduction co new_pred) do_next | isReflCo co -- See Note [Rewriting with Refl] = assert (isEmptyRewriterSet rewriters) $ - continueWith (setCtEvPredType old_ev new_pred) + do_next (setCtEvPredType old_ev new_pred) rewriteEvidence rewriters ev@(CtGiven { ctev_evar = old_evar, ctev_loc = loc }) - (Reduction co new_pred) + (Reduction co new_pred) do_next = assert (isEmptyRewriterSet rewriters) $ -- this is a Given, not a wanted do { new_ev <- newGivenEvVar loc (new_pred, new_tm) - ; continueWith new_ev } + ; do_next new_ev } where -- mkEvCast optimises ReflCo new_tm = mkEvCast (evId old_evar) @@ -1036,14 +1029,14 @@ rewriteEvidence new_rewriters ev@(CtWanted { ctev_dest = dest , ctev_loc = loc , ctev_rewriters = rewriters }) - (Reduction co new_pred) + (Reduction co new_pred) do_next = do { mb_new_ev <- newWanted loc rewriters' new_pred ; massert (coercionRole co == ctEvRole ev) ; setWantedEvTerm dest IsCoherent $ mkEvCast (getEvExpr mb_new_ev) (downgradeRole Representational (ctEvRole ev) (mkSymCo co)) ; case mb_new_ev of - Fresh new_ev -> continueWith new_ev + Fresh new_ev -> do_next new_ev Cached _ -> stopWith ev "Cached wanted" } where rewriters' = rewriters S.<> new_rewriters diff --git a/compiler/GHC/Tc/Solver/Dict.hs b/compiler/GHC/Tc/Solver/Dict.hs index 6893322f9a..c0f7dc7a49 100644 --- a/compiler/GHC/Tc/Solver/Dict.hs +++ b/compiler/GHC/Tc/Solver/Dict.hs @@ -16,6 +16,7 @@ import GHC.Tc.Types.Constraint import GHC.Tc.Types.Origin import GHC.Tc.Solver.InertSet import GHC.Tc.Solver.Monad +import GHC.Tc.Solver.Types import GHC.Builtin.Names ( coercibleTyConKey, heqTyConKey, eqTyConKey ) @@ -31,6 +32,7 @@ import GHC.Types.SrcLoc import GHC.Types.Var.Env import GHC.Types.Unique( hasKey ) +import GHC.Utils.Monad ( foldlM ) import GHC.Utils.Outputable import GHC.Utils.Panic import GHC.Utils.Misc @@ -69,22 +71,33 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = ev, cc_class = cls ; addSolvedDict what ev cls xis ; chooseInstance ev lkup_res } _ -> -- NoInstance or NotSure - -- We didn't solve it; so try functional dependencies with - -- the instance environment - do { doTopFundepImprovement work_item - ; tryLastResortProhibitedSuperclass inerts work_item } } + -- We didn't solve it; so try functional dependencies + tryFunDeps work_item } where dict_loc = ctEvLoc ev - doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w) --- | As a last resort, we TEMPORARILY allow a prohibited superclass solve, +tryFunDeps :: Ct -> TcS (StopOrContinue Ct) +-- Try functional dependencies +-- We do local improvement, then try top level; and we do all this last +-- See Note [Do fundeps last] +tryFunDeps work_item + = do { improved <- doLocalFunDepImprovement work_item + ; if improved then startAgainWith work_item else + + do { improved <- doTopFunDepImprovement work_item + ; if improved then startAgainWith work_item else + + do { inerts <- getTcSInerts + ; tryLastResortProhibitedSuperclass inerts work_item } } } + +tryLastResortProhibitedSuperclass :: InertSet -> Ct -> TcS (StopOrContinue Ct) +-- ^ As a last resort, we TEMPORARILY allow a prohibited superclass solve, -- emitting a loud warning when doing so: we might be creating non-terminating -- evidence (as we are in T22912 for example). -- -- See Note [Migrating away from loopy superclass solving] in GHC.Tc.TyCl.Instance. -tryLastResortProhibitedSuperclass :: InertSet -> Ct -> TcS (StopOrContinue Ct) tryLastResortProhibitedSuperclass inerts work_item@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = xis }) | let loc_w = ctEvLoc ev_w @@ -654,7 +667,7 @@ This Note describes a delicate interaction that constrains the orientation of equalities. This one is about fundeps, but the /exact/ same thing arises for type-family injectivity constraints: see Note [Improvement orientation]. -doTopFundepImprovement compares the constraint with all the instance +doTopFunDepImprovement compares the constraint with all the instance declarations, to see if we can produce any equalities. E.g class C2 a b | a -> b instance C Int Bool @@ -668,7 +681,7 @@ There is a nasty corner in #19415 which led to the typechecker looping: work_item: dwrk :: C (T @ka (a::ka)) (T @kb0 (b0::kb0)) Char where kb0, b0 are unification vars - ==> {doTopFundepImprovement: compare work_item with instance, + ==> {doTopFunDepImprovement: compare work_item with instance, generate /fresh/ unification variables kfresh0, yfresh0, emit a new Wanted, and add dwrk to inert set} @@ -694,10 +707,10 @@ We solve the problem by (#21703): carefully orienting the new Wanted so that all the freshly-generated unification variables are on the LHS. - Thus we emit - [W] T kfresh0 (yfresh0::kfresh0) ~ T kb0 (b0::kb0) + Thus we call unifyWanteds on + T kfresh0 (yfresh0::kfresh0) ~ T kb0 (b0::kb0) and /NOT/ - [W] T kb0 (b0::kb0) ~ T kfresh0 (yfresh0::kfresh0) + T kb0 (b0::kb0) ~ T kfresh0 (yfresh0::kfresh0) Now we'll unify kfresh0:=kb0, yfresh0:=b0, and all is well. The general idea is that we want to preferentially eliminate those freshly-generated @@ -784,6 +797,29 @@ wanteds. This solution was not complete, and caused a failures while trying to solve for transitive functional dependencies (test case: T21703) -- End of Historical note: Failed Alternative Plan (3) -- +Note [Do fundeps last] +~~~~~~~~~~~~~~~~~~~~~~ +Consider T4254b: + class FD a b | a -> b where { op :: a -> b } + + instance FD Int Bool + + foo :: forall a b. (a~Int,FD a b) => a -> Bool + foo = op + +From the ambiguity check on the type signature we get + [G] FD Int b + [W] FD Int beta +Interacting these gives beta:=b; then we start again and solve without +trying fundeps between the new [W] FD Int b and the top-level instance. +If we did, we'd generate [W] b ~ Bool, which fails. + +From the definition `foo = op` we get + [G] FD Int b + [W] FD Int Bool +We solve this from the top level instance before even trying fundeps. +If we did try fundeps, we'd generate [W] b ~ Bool, which fails. + Note [Weird fundeps] ~~~~~~~~~~~~~~~~~~~~ Consider class Het a b | a -> b where @@ -806,17 +842,58 @@ as the fundeps. #7875 is a case in point. -} -doTopFundepImprovement :: Ct -> TcS () +doLocalFunDepImprovement :: Ct -> TcS Bool +-- Add wanted constraints from type-class functional dependencies. +doLocalFunDepImprovement (CDictCan { cc_ev = work_ev, cc_class = cls }) + = do { inerts <- getInertCans + ; foldlM add_fds False (findDictsByClass (inert_dicts inerts) cls) } + where + work_pred = ctEvPred work_ev + work_loc = ctEvLoc work_ev + + add_fds :: Bool -> Ct -> TcS Bool + add_fds so_far inert_ct + | isGiven work_ev && isGiven inert_ev + -- Do not create FDs from Given/Given interactions: See Note [No Given/Given fundeps] + = return so_far + | otherwise + = do { traceTcS "doLocalFunDepImprovement" (vcat + [ ppr work_ev + , pprCtLoc work_loc, ppr (isGivenLoc work_loc) + , pprCtLoc inert_loc, ppr (isGivenLoc inert_loc) + , pprCtLoc derived_loc, ppr (isGivenLoc derived_loc) ]) + + ; unifs <- emitFunDepWanteds work_ev $ + improveFromAnother (derived_loc, inert_rewriters) + inert_pred work_pred + ; return (so_far || unifs) + } + where + 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 + (ctLocOrigin work_loc) + (ctLocSpan work_loc) + inert_pred + (ctLocOrigin inert_loc) + (ctLocSpan inert_loc) } + +doLocalFunDepImprovement work_item = pprPanic "doLocalFunDepImprovement" (ppr work_item) + +doTopFunDepImprovement :: Ct -> TcS Bool -- Try to functional-dependency improvement between the constraint -- and the top-level instance declarations -- See Note [Fundeps with instances, and equality orientation] -- See also Note [Weird fundeps] -doTopFundepImprovement work_item@(CDictCan { cc_ev = ev, cc_class = cls - , cc_tyargs = xis }) +doTopFunDepImprovement work_item@(CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = xis }) = do { traceTcS "try_fundeps" (ppr work_item) ; instEnvs <- getInstEnvs ; let fundep_eqns = improveFromInstEnv instEnvs mk_ct_loc cls xis - ; emitFunDepWanteds (ctEvRewriters ev) fundep_eqns } + ; emitFunDepWanteds ev fundep_eqns } where dict_pred = mkClassPred cls xis dict_loc = ctEvLoc ev @@ -830,5 +907,4 @@ doTopFundepImprovement work_item@(CDictCan { cc_ev = ev, cc_class = cls inst_pred inst_loc } , emptyRewriterSet ) -doTopFundepImprovement work_item = pprPanic "doTopFundepImprovement" (ppr work_item) - +doTopFunDepImprovement work_item = pprPanic "doTopFunDepImprovement" (ppr work_item) diff --git a/compiler/GHC/Tc/Solver/Equality.hs b/compiler/GHC/Tc/Solver/Equality.hs index ed4cd500aa..6bb894b8b4 100644 --- a/compiler/GHC/Tc/Solver/Equality.hs +++ b/compiler/GHC/Tc/Solver/Equality.hs @@ -179,10 +179,10 @@ can_eq_nc' _rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2 -- Then, get rid of casts can_eq_nc' rewritten _rdr_env _envs ev eq_rel (CastTy ty1 co1) _ ty2 ps_ty2 - | isNothing (canEqLHS_maybe ty2) -- See (3) in Note [Equalities with incompatible kinds] + | isNothing (canEqLHS_maybe ty2) -- See (EIK3) in Note [Equalities with incompatible kinds] = canEqCast rewritten ev eq_rel NotSwapped ty1 co1 ty2 ps_ty2 can_eq_nc' rewritten _rdr_env _envs ev eq_rel ty1 ps_ty1 (CastTy ty2 co2) _ - | isNothing (canEqLHS_maybe ty1) -- See (3) in Note [Equalities with incompatible kinds] + | isNothing (canEqLHS_maybe ty1) -- See (EIK3) in Note [Equalities with incompatible kinds] = canEqCast rewritten ev eq_rel IsSwapped ty2 co2 ty1 ps_ty1 ---------------------- @@ -253,10 +253,12 @@ can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2 -- See also Note [No top-level newtypes on RHS of representational equalities] can_eq_nc' True _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2 | Just can_eq_lhs1 <- canEqLHS_maybe ty1 - = canEqCanLHS ev eq_rel NotSwapped can_eq_lhs1 ps_ty1 ty2 ps_ty2 + = do { traceTcS "can_eq1" (ppr ty1 $$ ppr ty2) + ; canEqCanLHS ev eq_rel NotSwapped can_eq_lhs1 ps_ty1 ty2 ps_ty2 } | Just can_eq_lhs2 <- canEqLHS_maybe ty2 - = canEqCanLHS ev eq_rel IsSwapped can_eq_lhs2 ps_ty2 ty1 ps_ty1 + = do { traceTcS "can_eq2" (ppr ty1 $$ ppr ty2) + ; canEqCanLHS ev eq_rel IsSwapped can_eq_lhs2 ps_ty2 ty1 ps_ty1 } -- If the type is TyConApp tc1 args1, then args1 really can't be less -- than tyConArity tc1. It could be *more* than tyConArity, but then we @@ -651,13 +653,18 @@ can_eq_app :: CtEvidence -- :: s1 t1 ~N s2 t2 -- to an irreducible constraint; see typecheck/should_compile/T10494 -- See Note [Decomposing AppTy equalities] can_eq_app ev s1 t1 s2 t2 - | 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 rewriters arg_loc Nominal t1 t2 - ; let co = mkAppCo co_s co_t + | CtWanted { ctev_dest = dest } <- ev + = do { traceTcS "can_eq_app" (vcat [ text "s1:" <+> ppr s1, text "t1:" <+> ppr t1 + , text "s2:" <+> ppr s2, text "t2:" <+> ppr t2 + , text "vis:" <+> ppr (isNextArgVisible s1) ]) + ; (co,_,_) <- wrapUnifierTcS ev Nominal $ \uenv -> + -- Unify arguments t1/t2 before function s1/s2, because + -- the former have smaller kinds, and hence simpler error messages + -- c.f. GHC.Tc.Utils.Unify.uType (go_app) + do { let arg_env = updUEnvLoc uenv (adjustCtLoc (isNextArgVisible s1) False) + ; co_t <- uType arg_env t1 t2 + ; co_s <- uType uenv s1 s2 + ; return (mkAppCo co_s co_t) } ; setWantedEq dest co ; stopWith ev "Decomposed [W] AppTy" } @@ -717,7 +724,6 @@ canTyConApp :: CtEvidence -> EqRel -> TyCon -> [TcType] -> TcS (StopOrContinue Ct) -- See Note [Decomposing TyConApp equalities] --- See Note [Decomposing Dependent TyCons and Processing Wanted Equalities] -- Neither tc1 nor tc2 is a saturated funTyCon, nor a type family -- But they can be data families. canTyConApp ev eq_rel tc1 tys1 tc2 tys2 @@ -804,8 +810,8 @@ then we will just decompose s1~s2, and it might be better to do so on the spot. An important special case is where s1=s2, and we get just Refl. -So canDecomposableTyConAppOK uses unifyWanted etc to short-cut that work. -See also Note [Decomposing Dependent TyCons and Processing Wanted Equalities] +So canDecomposableTyConAppOK uses wrapUnifierTcS etc to short-cut +that work. See also Note [Work-list ordering]. Note [Decomposing TyConApp equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -908,6 +914,36 @@ that is for isInjectiveTyCon to be true: This is implemented in `can_decompose` in `canTyConApp`; it looks at injectivity, just as specified above. +Note [Work-list ordering] +~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider decomposing a TyCon equality + + (0) [W] T k_fresh (t1::k_fresh) ~ T k1 (t2::k1) + +This gives rise to 2 equalities in the solver worklist + + (1) [W] k_fresh ~ k1 + (2) [W] t1::k_fresh ~ t2::k1 + +We would like to solve (1) before looking at (2), so that we don't end +up in the complexities of canEqLHSHetero. To do this: + +* `canDecomposableTyConAppOK` calls `uType` on the arguments + /left-to-right/. See the call to zipWith4M in that function. + +* `uType` keeps the bag of emitted constraints in the same + left-to-right order. See the use of `snocBag` in `uType_defer`. + +* `wrapUnifierTcS` adds the bag of deferred constraints from + `do_unifications` to the work-list using `extendWorkListEqs`. + +* `extendWorkListEqs` and `selectWorkItem` together arrange that the + list of constraints given to `extendWorkListEqs` is processed in + left-to-right order. + +This is not a very big deal. It reduces the number of solver steps +in the test RaeJobTalk from 1830 to 1815, a 1% reduction. But still, +it doesn't cost anything either. Note [Decomposing type family applications] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1174,25 +1210,24 @@ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2 do { traceTcS "canDecomposableTyConAppOK" (ppr ev $$ ppr eq_rel $$ ppr tc $$ ppr tys1 $$ ppr tys2) ; case ev of - CtWanted { ctev_dest = dest, ctev_rewriters = rewriters } - -- new_locs and tc_roles are both infinite, so - -- we are guaranteed that cos has the same lengthm - -- as tys1 and tys2 - -- See Note [Fast path when decomposing TyConApps] - -- Caution: unifyWanteds is order sensitive - -- See Note [Decomposing Dependent TyCons and Processing Wanted Equalities] - -> do { cos <- unifyWanteds rewriters new_locs tc_roles tys1 tys2 - ; setWantedEq dest (mkTyConAppCo role tc cos) } + CtWanted { ctev_dest = dest } + -- new_locs and tc_roles are both infinite, so we are + -- guaranteed that cos has the same length as tys1 and tys2 + -- See Note [Fast path when decomposing TyConApps] + -> do { (co, _, _) <- wrapUnifierTcS ev role $ \uenv -> + do { cos <- zipWith4M (u_arg uenv) new_locs tc_roles tys1 tys2 + -- zipWith4M: see Note [Work-list ordering] + -- in GHC.Tc.Solved.Equality + ; return (mkTyConAppCo role tc cos) } + ; setWantedEq dest co } CtGiven { ctev_evar = evar } - -> do { let ev_co = mkCoVarCo evar - ; given_evs <- newGivenEvVars loc $ - [ ( mkPrimEqPredRole r ty1 ty2 - , evCoercion $ mkSelCo (SelTyCon i r) ev_co ) - | (r, ty1, ty2, i) <- zip4 tc_roles tys1 tys2 [0..] - , r /= Phantom - , not (isCoercionTy ty1) && not (isCoercionTy ty2) ] - ; emitWorkNC given_evs } + | let ev_co = mkCoVarCo evar + -> emitNewGivens loc + [ (r, ty1, ty2, mkSelCo (SelTyCon i r) ev_co) + | (r, ty1, ty2, i) <- zip4 tc_roles tys1 tys2 [0..] + , r /= Phantom + , not (isCoercionTy ty1) && not (isCoercionTy ty2) ] ; stopWith ev "Decomposed TyConApp" } @@ -1200,6 +1235,11 @@ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2 loc = ctEvLoc ev role = eqRelRole eq_rel + u_arg uenv arg_loc arg_role = uType arg_env + where + arg_env = uenv `setUEnvRole` arg_role + `updUEnvLoc` const arg_loc + -- Infinite, to allow for over-saturated TyConApps tc_roles = tyConRoleListX role tc @@ -1213,14 +1253,8 @@ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2 -- do either of these changes. (Forgetting to do so led to #16188) -- -- NB: infinite in length - new_locs = [ new_loc - | bndr <- tyConBinders tc - , let new_loc0 | isNamedTyConBinder bndr = toKindLoc loc - | otherwise = loc - new_loc | isInvisibleTyConBinder bndr - = updateCtLocOrigin new_loc0 toInvisibleOrigin - | otherwise - = new_loc0 ] + new_locs = [ adjustCtLocTyConBinder bndr loc + | bndr <- tyConBinders tc ] ++ repeat loc canDecomposableFunTy :: CtEvidence -> EqRel -> FunTyFlag @@ -1231,29 +1265,29 @@ canDecomposableFunTy ev eq_rel af f1@(m1,a1,r1) f2@(m2,a2,r2) = do { traceTcS "canDecomposableFunTy" (ppr ev $$ ppr eq_rel $$ ppr f1 $$ ppr f2) ; case ev of - CtWanted { ctev_dest = dest, ctev_rewriters = rewriters } - -> do { mult <- unifyWanted rewriters mult_loc (funRole role SelMult) m1 m2 - ; arg <- unifyWanted rewriters loc (funRole role SelArg) a1 a2 - ; res <- unifyWanted rewriters loc (funRole role SelRes) r1 r2 - ; setWantedEq dest (mkNakedFunCo1 role af mult arg res) } + CtWanted { ctev_dest = dest } + -> do { (co, _, _) <- wrapUnifierTcS ev Nominal $ \ uenv -> + do { let mult_env = uenv `updUEnvLoc` toInvisibleLoc + `setUEnvRole` funRole role SelMult + ; mult <- uType mult_env m1 m2 + ; arg <- uType (uenv `setUEnvRole` funRole role SelArg) a1 a2 + ; res <- uType (uenv `setUEnvRole` funRole role SelRes) r1 r2 + ; return (mkNakedFunCo role af mult arg res) } + ; setWantedEq dest co } CtGiven { ctev_evar = evar } - -> do { let ev_co = mkCoVarCo evar - ; given_evs <- newGivenEvVars loc $ - [ ( mkPrimEqPredRole role' ty1 ty2 - , evCoercion $ mkSelCo (SelFun fs) ev_co ) - | (fs, ty1, ty2) <- [(SelMult, m1, m2) - ,(SelArg, a1, a2) - ,(SelRes, r1, r2)] - , let role' = funRole role fs ] - ; emitWorkNC given_evs } + | let ev_co = mkCoVarCo evar + -> emitNewGivens loc + [ (funRole role fs, ty1, ty2, mkSelCo (SelFun fs) ev_co) + | (fs, ty1, ty2) <- [ (SelMult, m1, m2) + , (SelArg, a1, a2) + , (SelRes, r1, r2)] ] ; stopWith ev "Decomposed TyConApp" } where - loc = ctEvLoc ev - role = eqRelRole eq_rel - mult_loc = updateCtLocOrigin loc toInvisibleOrigin + loc = ctEvLoc ev + role = eqRelRole eq_rel -- | Call when canonicalizing an equality fails, but if the equality is -- representational, there is some hope for the future. @@ -1408,7 +1442,7 @@ canEqCanLHS ev eq_rel swapped lhs1 ps_xi1 xi2 ps_xi2 = canEqCanLHSHomo ev eq_rel swapped lhs1 ps_xi1 xi2 ps_xi2 | otherwise - = canEqCanLHSHetero ev eq_rel swapped lhs1 k1 xi2 k2 + = canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 k1 xi2 ps_xi2 k2 where k1 = canEqLHSKind lhs1 @@ -1444,64 +1478,75 @@ But this sent solver in an infinite loop (see #19415). -} canEqCanLHSHetero :: CtEvidence -- :: (xi1 :: ki1) ~ (xi2 :: ki2) + -- (or reversed if SwapFlag=IsSwapped) -> EqRel -> SwapFlag - -> CanEqLHS -- xi1 + -> CanEqLHS -> TcType -- xi1 -> TcKind -- ki1 - -> TcType -- xi2 + -> TcType -> TcType -- xi2 -> TcKind -- ki2 -> TcS (StopOrContinue Ct) -canEqCanLHSHetero ev eq_rel swapped lhs1 ki1 xi2 ki2 - -- See Note [Equalities with incompatible kinds] - -- See Note [Kind Equality Orientation] - -- NB: preserve left-to-right orientation!! - -- See Note [Fundeps with instances, and equality orientation] - -- wrinkle (W2) in GHC.Tc.Solver.Interact - = do { (kind_ev, kind_co) <- mk_kind_eq -- :: ki1 ~N ki2 - - ; let -- kind_co :: (ki1 :: *) ~N (ki2 :: *) (whether swapped or not) - lhs_redn = mkReflRedn role xi1 - rhs_redn = mkGReflRightRedn role xi2 (mkSymCo kind_co) - - -- See Note [Equalities with incompatible kinds], Wrinkle (1) - -- This will be ignored in rewriteEqEvidence if the work item is a Given - rewriters = rewriterSetFromCo kind_co +canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2 +-- See Note [Equalities with incompatible kinds] +-- See Note [Kind Equality Orientation] + +-- NB: preserve left-to-right orientation!! See wrinkle (W2) in +-- Note [Fundeps with instances, and equality orientation] in GHC.Tc.Solver.Interact +-- NotSwapped: +-- ev :: (lhs1:ki1) ~r# (xi2:ki2) +-- kind_co :: k11 ~# ki2 -- Same orientiation as ev +-- type_ev :: lhs1 ~r# (xi2 |> sym kind_co) +-- Swapped +-- ev :: (xi2:ki2) ~r# (lhs1:ki1) +-- kind_co :: ki2 ~# ki1 -- Same orientiation as ev +-- type_ev :: (xi2 |> kind_co) ~r# lhs1 + + = do { (kind_co, rewriters, unifs_happened) <- mk_kind_eq -- :: ki1 ~N ki2 + ; if unifs_happened + -- Unifications happened, so start again to do the zonking + -- Otherwise we might put something in the inert set that isn't inert + then startAgainWith (mkNonCanonical ev) + else + do { let lhs_redn = mkReflRedn role ps_xi1 + rhs_redn = mkGReflRightRedn role xi2 mb_sym_kind_co + mb_sym_kind_co = case swapped of + NotSwapped -> mkSymCo kind_co + IsSwapped -> kind_co ; traceTcS "Hetero equality gives rise to kind equality" - (ppr kind_co <+> dcolon <+> sep [ ppr ki1, text "~#", ppr ki2 ]) + (ppr swapped $$ + ppr kind_co <+> dcolon <+> sep [ ppr ki1, text "~#", ppr ki2 ]) ; type_ev <- rewriteEqEvidence rewriters ev swapped lhs_redn rhs_redn - ; emitWorkNC [type_ev] -- delay the type equality until after we've finished - -- the kind equality, which may unlock things - -- See Note [Equalities with incompatible kinds] + ; let new_xi2 = mkCastTy ps_xi2 mb_sym_kind_co + ; canEqCanLHSHomo type_ev eq_rel NotSwapped lhs1 ps_xi1 new_xi2 new_xi2 }} - ; solveNonCanonicalEquality kind_ev NomEq ki1 ki2 } where - mk_kind_eq :: TcS (CtEvidence, CoercionN) + mk_kind_eq :: TcS (CoercionN, RewriterSet, Bool) + -- Returned kind_co has kind (k1 ~ k2) if NotSwapped, (k2 ~ k1) if Swapped + -- Returned Bool = True if unifications happened, so we should retry mk_kind_eq = case ev of CtGiven { ctev_evar = evar } - -> do { let kind_co = maybe_sym $ mkKindCo (mkCoVarCo evar) -- :: k1 ~ k2 - ; kind_ev <- newGivenEvVar kind_loc (kind_pty, evCoercion kind_co) - ; return (kind_ev, ctEvCoercion kind_ev) } - - CtWanted { ctev_rewriters = rewriters } - -> newWantedEq kind_loc rewriters Nominal ki1 ki2 - - xi1 = canEqLHSType lhs1 - loc = ctev_loc ev - role = eqRelRole eq_rel - kind_loc = mkKindLoc xi1 xi2 loc - kind_pty = mkHeteroPrimEqPred liftedTypeKind liftedTypeKind ki1 ki2 - - maybe_sym = case swapped of - IsSwapped -> mkSymCo -- if the input is swapped, then we - -- will have k2 ~ k1, so flip it to k1 ~ k2 - NotSwapped -> id + -> do { let kind_co = mkKindCo (mkCoVarCo evar) + pred_ty = unSwap swapped (mkNomPrimEqPred liftedTypeKind) ki1 ki2 + kind_loc = mkKindEqLoc xi1 xi2 (ctev_loc ev) + ; kind_ev <- newGivenEvVar kind_loc (pred_ty, evCoercion kind_co) + ; emitWorkNC [kind_ev] + ; return (ctEvCoercion kind_ev, emptyRewriterSet, False) } + + CtWanted {} + -> do { (kind_co, cts, unifs) <- wrapUnifierTcS ev Nominal $ \uenv -> + let uenv' = updUEnvLoc uenv (mkKindEqLoc xi1 xi2) + in unSwap swapped (uType uenv') ki1 ki2 + ; return (kind_co, rewriterSetFromCts cts, not (null unifs)) } + + xi1 = canEqLHSType lhs1 + role = eqRelRole eq_rel -canEqCanLHSHomo :: CtEvidence +canEqCanLHSHomo :: CtEvidence -- lhs ~ rhs + -- or, if swapped: rhs ~ lhs -> EqRel -> SwapFlag - -> CanEqLHS -- lhs (or, if swapped, rhs) - -> TcType -- pretty lhs - -> TcType -> TcType -- rhs, pretty rhs + -> CanEqLHS -> TcType -- lhs, pretty lhs + -> TcType -> TcType -- rhs, pretty rhs -> TcS (StopOrContinue Ct) -- Guaranteed that typeKind lhs == typeKind rhs canEqCanLHSHomo ev eq_rel swapped lhs1 ps_xi1 xi2 ps_xi2 @@ -1557,46 +1602,13 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco -- See Note [Decomposing type family applications] = do { traceTcS "canEqCanLHS2 two type families" (ppr lhs1 $$ ppr lhs2) - -- emit wanted equalities for injective type families - ; let inj_eqns :: [TypeEqn] -- TypeEqn = Pair Type - inj_eqns - | ReprEq <- eq_rel = [] -- injectivity applies only for nom. eqs. - | fun_tc1 /= fun_tc2 = [] -- if the families don't match, stop. - - | Injective inj <- tyConInjectivityInfo fun_tc1 - = [ Pair arg1 arg2 - | (arg1, arg2, True) <- zip3 fun_args1 fun_args2 inj ] - - -- built-in synonym families don't have an entry point - -- for this use case. So, we just use sfInteractInert - -- and pass two equal RHSs. We *could* add another entry - -- point, but then there would be a burden to make - -- sure the new entry point and existing ones were - -- internally consistent. This is slightly distasteful, - -- but it works well in practice and localises the - -- problem. - | Just ops <- isBuiltInSynFamTyCon_maybe fun_tc1 - = let ki1 = canEqLHSKind lhs1 - ki2 | MRefl <- mco - = ki1 -- just a small optimisation - | otherwise - = canEqLHSKind lhs2 - - fake_rhs1 = anyTypeOfKind ki1 - fake_rhs2 = anyTypeOfKind ki2 - in - sfInteractInert ops fun_args1 fake_rhs1 fun_args2 fake_rhs2 - - | otherwise -- ordinary, non-injective type family - = [] - - ; case ev of - CtWanted { ctev_rewriters = rewriters } -> - mapM_ (\ (Pair t1 t2) -> unifyWanted rewriters (ctEvLoc ev) Nominal t1 t2) inj_eqns - CtGiven {} -> return () - -- See Note [No Given/Given fundeps] in GHC.Tc.Solver.Interact - - ; tclvl <- getTcLevel + ; unifications_done <- tryFamFamInjectivity ev eq_rel + fun_tc1 fun_args1 fun_tc2 fun_args2 mco + ; if unifications_done + then -- Go round again, since the unifications affect lhs/rhs + startAgainWith (mkNonCanonical ev) + else + do { tclvl <- getTcLevel ; let tvs1 = tyCoVarsOfTypes fun_args1 tvs2 = tyCoVarsOfTypes fun_args2 @@ -1611,7 +1623,7 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco ; if swap_for_rewriting || swap_for_size then finish_with_swapping - else finish_without_swapping } + else finish_without_swapping } } where sym_mco = mkSymMCo mco role = eqRelRole eq_rel @@ -1762,11 +1774,11 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs | otherwise -> tryIrredInstead reason ev eq_rel swapped lhs rhs ; - PuOK rhs_redn _ -> + PuOK _ rhs_redn -> -- Success: we can solve by unification do { -- In the common case where rhs_redn is Refl, we don't need to rewrite - -- the evidence even if swapped=IsSwapped. Suppose the original was + -- the evidence, even if swapped=IsSwapped. Suppose the original was -- [W] co : Int ~ alpha -- We unify alpha := Int, and set co := <Int>. No need to -- swap to co = sym co' @@ -1778,7 +1790,6 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs ; let tv_ty = mkTyVarTy tv final_rhs = reductionReducedType rhs_redn - tv_lvl = tcTyVarLevel tv ; traceTcS "Sneaky unification:" $ vcat [text "Unifies:" <+> ppr tv <+> text ":=" <+> ppr final_rhs, @@ -1794,14 +1805,8 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs ; setEvBindIfWanted new_ev IsCoherent $ evCoercion (mkNomReflCo final_rhs) - -- Set the unification flag if we have done outer unifications - -- that might affect an earlier implication constraint - ; ambient_lvl <- getTcLevel - ; when (ambient_lvl `strictlyDeeperThan` tv_lvl) $ - setUnificationFlag tv_lvl - -- Kick out any constraints that can now be rewritten - ; n_kicked <- kickOutAfterUnification tv + ; n_kicked <- kickOutAfterUnification [tv] ; return (Stop new_ev (text "Solved by unification" <+> pprKicked n_kicked)) }}}} @@ -1816,12 +1821,9 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs -- and hence we /can/ use it for rewriting -- Concrete-ness: alpha[conc] ~ b[sk] -- We can use it to rewrite; we still have to solve the original - -- Coercion holes: see wrinkle (2) of - -- Note [Equalities with incompatible kinds] do_not_prevent_rewriting :: CheckTyEqResult do_not_prevent_rewriting = cteProblem cteSkolemEscape S.<> - cteProblem cteConcrete S.<> - cteProblem cteCoercionHole + cteProblem cteConcrete --------------------------- -- Unification is off the table @@ -1848,7 +1850,7 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs -> tryIrredInstead reason ev eq_rel swapped lhs rhs - PuOK rhs_redn _ + PuOK _ rhs_redn -> do { new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped (mkReflRedn (eqRelRole eq_rel) lhs_ty) rhs_redn @@ -1921,42 +1923,59 @@ k2 and use this to cast. To wit, from [X] co :: k1 ~ k2 [X] (tv :: k1) ~ ((rhs |> sym co) :: k1) -We carry on with the *kind equality*, not the type equality, because -solving the former may unlock the latter. This choice is made in -canEqCanLHSHetero. It is important: otherwise, T13135 loops. - Wrinkles: - (1) When X is W, the new type-level wanted is effectively rewritten by the +(EIK1) When X is W, the new type-level wanted is effectively rewritten by the kind-level one. We thus include the kind-level wanted in the RewriterSet for the type-level one. See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint. This is done in canEqCanLHSHetero. - (2) If we have [W] w :: alpha ~ (rhs |> sym co_hole), should we unify alpha? No. - The problem is that the wanted w is effectively rewritten by another wanted, - and unifying alpha effectively promotes this wanted to a given. Doing so - means we lose track of the rewriter set associated with the wanted. - - Another way to say it: we must not have a co_hole in a Given, and - unification effectively makes a Given. (This is not very well motivated; - may need to dig deeper if anything goes wrong.) - - On the other hand, w is perfectly suitable for rewriting, because of the - way we carefully track rewriter sets. So we include cteCoercionHole in - `do_not_prevent_rewriting` in `canEqCanLHSFinish_try_unification`. (Side - note: I think this is an open choice. Maybe we'd get better error - messages if we did not use these equalities for rewriting.) - - We thus allow w to be a CEqCan, but we prevent unification. See - Note [Unification preconditions] in GHC.Tc.Utils.Unify. - - The only tricky part is that we must later indeed unify if/when the kind-level - wanted gets solved. This is done in kickOutAfterFillingCoercionHole, - which kicks out all equalities whose RHS mentions the filled-in coercion hole. - Note that it looks for type family equalities, too, because of the use of - unifyTest in canEqTyVarFunEq. - - (3) Suppose we have [W] (a :: k1) ~ (rhs :: k2). We duly follow the +(EIK2) Suppose we have [W] (a::Type) ~ (b::Type->Type). The above rewrite will produce + [W] w : a ~ (b |> kw) + [W] kw : Type ~ (Type->Type) + + But we do /not/ want to regard `w` as canonical, and use it for rewriting + other constraints: `kw` is insoluble, and replacing something of kind + `Type` with something of kind `Type->Type` (even wrapped in an insouluble + cast) does not help, and doing so turns out to lead to much worse error + messages. (In particular, if 'a' is a unification variable, we might + unify, losing the tracking info that it depends on solving `kw`.) + + Conclusion: if a RHS contains a corecion hole arising from fixing a hetero-kinded + equality, treat the equality (`w` in this case) as non-canonical, so that + * It will not be used for unification + * It will not be used for rewriting + Instead, it lands in the inert_irreds in the inert set, awaiting solution of + that `kw`. + + (EIK2a) We must later indeed unify if/when the kind-level wanted, `kw` gets + solved. This is done in kickOutAfterFillingCoercionHole, which kicks out + all equalities whose RHS mentions the filled-in coercion hole. Note that + it looks for type family equalities, too, because of the use of unifyTest + in canEqTyVarFunEq. + + (EIK2b) What if the RHS mentions /other/ coercion holes? How can that happen? The + main way is like this. Assume F :: forall k. k -> Type + [W] kw : k ~ Type + [W] w : a ~ F k t + We can rewrite `w` with `kw` like this: + [W] w' : a ~ F Type (t |> kw) + The cast on the second argument of `F` is necessary to keep the appliation well-kinded. + There is nothing special here; no reason not treat w' as canonical, and use it for + rewriting. Indeed tests JuanLopez only typechecks if we do. So we'd like to treat + this kind of equality as canonical. + + Hence the ch_hetero_kind field in CoercionHole: it is True of constraints + created by `canEqCanLHSHetero` to fix up hetero-kinded equalities; and False otherwise: + + * An equality constraint is non-canonical if it mentions a hetero-kind + CoercionHole on the RHS. See the `hasCoercionHoleCo` test in GHC.Tc.Utils.checkCo. + + * Hetero-kind CoercionHoles are created when the parent's CtOrigin is + KindEqOrigin: see GHC.Tc.Utils.TcMType.newCoercionHole and friends. We + set this origin, via `mkKindLoc`, in `mk_kind_eq` in `canEqCanLHSHetero`. + +(EIK3) Suppose we have [W] (a :: k1) ~ (rhs :: k2). We duly follow the algorithm detailed here, producing [W] co :: k1 ~ k2, and adding [W] (a :: k1) ~ ((rhs |> sym co) :: k1) to the irreducibles. Some time later, we solve co, and fill in co's coercion hole. This kicks out @@ -2146,7 +2165,7 @@ in `GHC.Tc.Solver.Monad.checkTouchableTyVarEq`. Why TauTvs? See [Why TauTvs] below. Critically, we emit the two new constraints (the last two above) -directly instead of calling unifyWanted. (Otherwise, we'd end up +directly instead of calling wrapUnifierTcS. (Otherwise, we'd end up unifying cbv1 and cbv2 immediately, achieving nothing.) Next, we unify alpha := cbv1 -> cbv2, having eliminated the occurs check. This unification happens immediately following a successful call to @@ -2400,12 +2419,9 @@ rewriteEqEvidence new_rewriters old_ev swapped (Reduction lhs_co nlhs) (Reductio | CtWanted { ctev_dest = dest , ctev_rewriters = rewriters } <- old_ev , let rewriters' = rewriters S.<> new_rewriters - = do { (new_ev, hole_co) <- newWantedEq loc rewriters' - (ctEvRole old_ev) nlhs nrhs + = do { (new_ev, hole_co) <- newWantedEq loc rewriters' (ctEvRole old_ev) nlhs nrhs ; let co = maybeSymCo swapped $ - lhs_co - `mkTransCo` hole_co - `mkTransCo` mkSymCo rhs_co + lhs_co `mkTransCo` hole_co `mkTransCo` mkSymCo rhs_co ; setWantedEq dest co ; traceTcS "rewriteEqEvidence" (vcat [ ppr old_ev , ppr nlhs @@ -2480,9 +2496,11 @@ interactEq work_item@(EqCt { eq_lhs = lhs, eq_ev = ev, eq_eq_rel = eq_rel }) | otherwise -> case lhs of TyVarLHS {} -> finishEqCt work_item - TyFamLHS tc args -> do { improveLocalFunEqs inerts tc args work_item - ; improveTopFunEqs tc args work_item - ; finishEqCt work_item } } + TyFamLHS tc args -> do { imp1 <- improveLocalFunEqs inerts tc args work_item + ; imp2 <- improveTopFunEqs tc args work_item + ; if (imp1 || imp2) + then startAgainWith (mkNonCanonical ev) + else finishEqCt work_item } } inertsCanDischarge :: InertCans -> EqCt @@ -2746,7 +2764,7 @@ Of course, if we solve the first wanted first, the second becomes homogeneous. When looking for injectivity-inspired equalities, we work left-to-right, producing the two equalities in the order written above. However, these -equalities are then passed into unifyWanted, which will fail, adding these +equalities are then passed into wrapUnifierTcS, which will fail, adding these to the work list. However, crucially, the work list operates like a *stack*. So, because we add w1 and then w2, we process w2 first. This is silly: solving w1 would unlock w2. So we make sure to add equalities to the work @@ -2758,9 +2776,9 @@ like the right thing to do. When this was originally conceived, it was necessary to avoid a loop in T13135. That loop is now avoided by continuing with the kind equality (not the type -equality) in canEqCanLHSHetero (see Note [Equalities with incompatible kinds] -in GHC.Tc.Solver.Canonical). However, the idea of working left-to-right still -seems worthwhile, and so the calls to 'reverse' remain. +equality) in canEqCanLHSHetero (see Note [Equalities with incompatible kinds]). +However, the idea of working left-to-right still seems worthwhile, and so the calls +to 'reverse' remain. Note [Improvement orientation] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2804,28 +2822,72 @@ equality with the template on the left. Delicate, but it works. -} +tryFamFamInjectivity :: CtEvidence -> EqRel + -> TyCon -> [TcType] -> TyCon -> [TcType] -> MCoercion + -> TcS Bool -- True <=> some unification happened +tryFamFamInjectivity ev eq_rel fun_tc1 fun_args1 fun_tc2 fun_args2 mco + | ReprEq <- eq_rel + = return False -- Injectivity applies only for Nominal equalities + | fun_tc1 /= fun_tc2 + = return False -- If the families don't match, stop. + | isGiven ev + = return False -- See Note [No Given/Given fundeps] in GHC.Tc.Solver.Interact + + -- So this is a [W] (F tys1 ~N# F tys2) + + -- Is F an injective type family + | Injective inj <- tyConInjectivityInfo fun_tc1 + = unifyFunDeps ev Nominal $ \uenv -> + uPairsTcM uenv [ Pair ty1 ty2 + | (ty1,ty2,True) <- zip3 fun_args1 fun_args2 inj ] + + -- Built-in synonym families don't have an entry point for this + -- use case. So, we just use sfInteractInert and pass two equal + -- RHSs. We *could* add another entry point, but then there would + -- be a burden to make sure the new entry point and existing ones + -- were internally consistent. This is slightly distasteful, but + -- it works well in practice and localises the problem. Ugh. + | Just ops <- isBuiltInSynFamTyCon_maybe fun_tc1 + = let tc_kind = tyConKind fun_tc1 + ki1 = piResultTys tc_kind fun_args1 + ki2 | MRefl <- mco + = ki1 -- just a small optimisation + | otherwise + = piResultTys tc_kind fun_args2 + + fake_rhs1 = anyTypeOfKind ki1 + fake_rhs2 = anyTypeOfKind ki2 + + eqs :: [TypeEqn] + eqs = sfInteractInert ops fun_args1 fake_rhs1 fun_args2 fake_rhs2 + in + unifyFunDeps ev Nominal $ \uenv -> + uPairsTcM uenv eqs + + | otherwise -- ordinary, non-injective type family + = return False + -------------------- -improveTopFunEqs :: TyCon -> [TcType] -> EqCt -> TcS () +improveTopFunEqs :: TyCon -> [TcType] -> EqCt -> TcS Bool -- See Note [FunDep and implicit parameter reactions] improveTopFunEqs fam_tc args (EqCt { eq_ev = ev, eq_rhs = rhs }) - - | isGiven ev = return () -- See Note [No Given/Given fundeps] + | isGiven ev + = return False -- See Note [No Given/Given fundeps] | otherwise = do { fam_envs <- getFamInstEnvs ; eqns <- improve_top_fun_eqs fam_envs fam_tc args rhs ; traceTcS "improveTopFunEqs" (vcat [ ppr fam_tc <+> ppr args <+> ppr rhs - , ppr eqns ]) - ; mapM_ (\(Pair ty1 ty2) -> unifyWanted rewriters loc Nominal ty1 ty2) - (reverse eqns) } + , ppr eqns ]) + ; unifyFunDeps ev Nominal $ \uenv -> + uPairsTcM (bump_depth uenv) (reverse eqns) } -- Missing that `reverse` causes T13135 and T13135_simple to loop. -- See Note [Reverse order of fundep equations] where - loc = bumpCtLocDepth (ctEvLoc ev) + bump_depth env = env { u_loc = bumpCtLocDepth (u_loc env) } -- ToDo: this location is wrong; it should be FunDepOrigin2 -- See #14778 - rewriters = ctEvRewriters ev improve_top_fun_eqs :: FamInstEnvs -> TyCon -> [TcType] -> TcType @@ -2903,19 +2965,21 @@ improve_top_fun_eqs fam_envs fam_tc args rhs_ty , (ax_arg, arg, True) <- zip3 ax_args args inj_args ] } -improveLocalFunEqs :: InertCans -> TyCon -> [TcType] -> EqCt -> TcS () +improveLocalFunEqs :: InertCans -> TyCon -> [TcType] -> EqCt -> TcS Bool -- Generate improvement equalities, by comparing -- the current work item with inert CFunEqs -- E.g. x + y ~ z, x + y' ~ z => [W] y ~ y' -- -- See Note [FunDep and implicit parameter reactions] improveLocalFunEqs inerts fam_tc args (EqCt { eq_ev = work_ev, eq_rhs = rhs }) - = unless (null improvement_eqns) $ - do { traceTcS "interactFunEq improvements: " $ + | null improvement_eqns + = return False + | otherwise + = do { traceTcS "interactFunEq improvements: " $ vcat [ text "Eqns:" <+> ppr improvement_eqns , text "Candidates:" <+> ppr funeqs_for_tc , text "Inert eqs:" <+> ppr (inert_eqs inerts) ] - ; emitFunDepWanteds (ctEvRewriters work_ev) improvement_eqns } + ; emitFunDepWanteds work_ev improvement_eqns } where funeqs = inert_funeqs inerts funeqs_for_tc :: [EqCt] diff --git a/compiler/GHC/Tc/Solver/InertSet.hs b/compiler/GHC/Tc/Solver/InertSet.hs index ab5ee70ac1..ab3f8c9638 100644 --- a/compiler/GHC/Tc/Solver/InertSet.hs +++ b/compiler/GHC/Tc/Solver/InertSet.hs @@ -8,7 +8,8 @@ module GHC.Tc.Solver.InertSet ( -- * The work list WorkList(..), isEmptyWorkList, emptyWorkList, extendWorkListNonEq, extendWorkListCt, - extendWorkListCts, extendWorkListEq, + extendWorkListCts, extendWorkListCtList, + extendWorkListEq, extendWorkListEqs, appendWorkList, extendWorkListImplic, workListSize, selectWorkItem, @@ -31,7 +32,7 @@ module GHC.Tc.Solver.InertSet ( foldFunEqs, -- * Kick-out - kickOutRewritableLHS, + KickOutSpec(..), kickOutRewritableLHS, -- * Cycle breaker vars CycleBreakerVarStack, @@ -50,6 +51,7 @@ import GHC.Tc.Utils.TcType import GHC.Types.Var import GHC.Types.Var.Env +import GHC.Types.Var.Set import GHC.Core.Reduction import GHC.Core.Predicate @@ -60,6 +62,7 @@ import GHC.Core.TyCon import GHC.Core.Unify import GHC.Data.Bag + import GHC.Utils.Misc ( partitionWith ) import GHC.Utils.Outputable import GHC.Utils.Panic @@ -93,7 +96,7 @@ As a simple form of priority queue, our worklist separates out Note [Prioritise equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -It's very important to process equalities /first/: +It's very important to process equalities over class constraints: * (Efficiency) The general reason to do so is that if we process a class constraint first, we may end up putting it into the inert set @@ -111,14 +114,17 @@ It's very important to process equalities /first/: Solution: prioritise equalities over class constraints * (Class equalities) We need to prioritise equalities even if they - are hidden inside a class constraint; - see Note [Prioritise class equalities] + are hidden inside a class constraint; see Note [Prioritise class equalities] * (Kick-out) We want to apply this priority scheme to kicked-out - constraints too (see the call to extendWorkListCt in kick_out_rewritable + constraints too (see the call to extendWorkListCt in kick_out_rewritable) E.g. a CIrredCan can be a hetero-kinded (t1 ~ t2), which may become homo-kinded when kicked out, and hence we want to prioritise it. +Among the equalities we prioritise ones with an empty rewriter set; +see Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint, wrinkle (W1). + + Note [Prioritise class equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We prioritise equalities in the solver (see selectWorkItem). But class @@ -157,6 +163,13 @@ data WorkList -- See Note [Prioritise equalities] -- See Note [Prioritise class equalities] + , wl_rw_eqs :: [Ct] -- Like wl_eqs, but ones that have a non-empty + -- rewriter set; or, more precisely, did when + -- added to the WorkList + -- We prioritise wl_eqs over wl_rw_eqs; + -- see Note [Prioritise Wanteds with empty RewriterSet] + -- in GHC.Tc.Types.Constraint for more details. + , wl_rest :: [Ct] , wl_implics :: Bag Implication -- See Note [Residual implications] @@ -164,20 +177,41 @@ data WorkList appendWorkList :: WorkList -> WorkList -> WorkList appendWorkList - (WL { wl_eqs = eqs1, wl_rest = rest1 - , wl_implics = implics1 }) - (WL { wl_eqs = eqs2, wl_rest = rest2 - , wl_implics = implics2 }) + (WL { wl_eqs = eqs1, wl_rw_eqs = rw_eqs1 + , wl_rest = rest1, wl_implics = implics1 }) + (WL { wl_eqs = eqs2, wl_rw_eqs = rw_eqs2 + , wl_rest = rest2, wl_implics = implics2 }) = WL { wl_eqs = eqs1 ++ eqs2 + , wl_rw_eqs = rw_eqs1 ++ rw_eqs2 , wl_rest = rest1 ++ rest2 , wl_implics = implics1 `unionBags` implics2 } workListSize :: WorkList -> Int -workListSize (WL { wl_eqs = eqs, wl_rest = rest }) - = length eqs + length rest - -extendWorkListEq :: Ct -> WorkList -> WorkList -extendWorkListEq ct wl = wl { wl_eqs = ct : wl_eqs wl } +workListSize (WL { wl_eqs = eqs, wl_rw_eqs = rw_eqs, wl_rest = rest }) + = length eqs + length rw_eqs + length rest + +extendWorkListEq :: RewriterSet -> Ct -> WorkList -> WorkList +extendWorkListEq rewriters ct wl + | isEmptyRewriterSet rewriters -- A wanted that has not been rewritten + -- isEmptyRewriterSet: see Note [Prioritise Wanteds with empty RewriterSet] + -- in GHC.Tc.Types.Constraint + = wl { wl_eqs = ct : wl_eqs wl } + | otherwise + = wl { wl_rw_eqs = ct : wl_rw_eqs wl } + +extendWorkListEqs :: RewriterSet -> Bag Ct -> WorkList -> WorkList +-- Add [eq1,...,eqn] to the work-list +-- They all have the same rewriter set +-- The constraints will be solved in left-to-right order: +-- see Note [Work-list ordering] in GHC.Tc.Solved.Equality +extendWorkListEqs rewriters eqs wl + | isEmptyRewriterSet rewriters + -- isEmptyRewriterSet: see Note [Prioritise Wanteds with empty RewriterSet] + -- in GHC.Tc.Types.Constraint + = wl { wl_eqs = foldr (:) (wl_eqs wl) eqs } + -- The foldr just appends wl_eqs to the bag of eqs + | otherwise + = wl { wl_rw_eqs = foldr (:) (wl_rw_eqs wl) eqs } extendWorkListNonEq :: Ct -> WorkList -> WorkList -- Extension by non equality @@ -187,20 +221,25 @@ extendWorkListImplic :: Implication -> WorkList -> WorkList extendWorkListImplic implic wl = wl { wl_implics = implic `consBag` wl_implics wl } extendWorkListCt :: Ct -> WorkList -> WorkList --- Agnostic +-- Agnostic about what kind of constraint extendWorkListCt ct wl - = case classifyPredType (ctPred ct) of + = case classifyPredType (ctEvPred ev) of EqPred {} - -> extendWorkListEq ct wl + -> extendWorkListEq rewriters ct wl ClassPred cls _ -- See Note [Prioritise class equalities] | isEqPredClass cls - -> extendWorkListEq ct wl + -> extendWorkListEq rewriters ct wl _ -> extendWorkListNonEq ct wl + where + ev = ctEvidence ct + rewriters = ctEvRewriters ev -extendWorkListCts :: [Ct] -> WorkList -> WorkList --- Agnostic +extendWorkListCtList :: [Ct] -> WorkList -> WorkList +extendWorkListCtList cts wl = foldr extendWorkListCt wl cts + +extendWorkListCts :: Cts -> WorkList -> WorkList extendWorkListCts cts wl = foldr extendWorkListCt wl cts isEmptyWorkList :: WorkList -> Bool @@ -208,21 +247,24 @@ isEmptyWorkList (WL { wl_eqs = eqs, wl_rest = rest, wl_implics = implics }) = null eqs && null rest && isEmptyBag implics emptyWorkList :: WorkList -emptyWorkList = WL { wl_eqs = [], wl_rest = [], wl_implics = emptyBag } +emptyWorkList = WL { wl_eqs = [], wl_rw_eqs = [], wl_rest = [], wl_implics = emptyBag } selectWorkItem :: WorkList -> Maybe (Ct, WorkList) -- See Note [Prioritise equalities] -selectWorkItem wl@(WL { wl_eqs = eqs, wl_rest = rest }) - | ct:cts <- eqs = Just (ct, wl { wl_eqs = cts }) - | ct:cts <- rest = Just (ct, wl { wl_rest = cts }) - | otherwise = Nothing +selectWorkItem wl@(WL { wl_eqs = eqs, wl_rw_eqs = rw_eqs, wl_rest = rest }) + | ct:cts <- eqs = Just (ct, wl { wl_eqs = cts }) + | ct:cts <- rw_eqs = Just (ct, wl { wl_rw_eqs = cts }) + | ct:cts <- rest = Just (ct, wl { wl_rest = cts }) + | otherwise = Nothing -- Pretty printing instance Outputable WorkList where - ppr (WL { wl_eqs = eqs, wl_rest = rest, wl_implics = implics }) + ppr (WL { wl_eqs = eqs, wl_rw_eqs = rw_eqs, wl_rest = rest, wl_implics = implics }) = text "WL" <+> (braces $ vcat [ ppUnless (null eqs) $ text "Eqs =" <+> vcat (map ppr eqs) + , ppUnless (null rw_eqs) $ + text "RwEqs =" <+> vcat (map ppr rw_eqs) , ppUnless (null rest) $ text "Non-eqs =" <+> vcat (map ppr rest) , ppUnless (isEmptyBag implics) $ @@ -1298,13 +1340,27 @@ updateGivenEqs tclvl ct inerts@(IC { inert_given_eq_lvl = ge_lvl }) not_equality (CDictCan {}) = True not_equality _ = False -kickOutRewritableLHS :: CtFlavourRole -- Flavour/role of the equality that - -- is being added to the inert set - -> CanEqLHS -- The new equality is lhs ~ ty - -> InertCans - -> (WorkList, InertCans) +data KickOutSpec -- See Note [KickOutSpec] + = KOAfterUnify TcTyVarSet -- We have unified these tyvars + | KOAfterAdding CanEqLHS -- We are adding to the inert set a canonical equality + -- constraint with this LHS + +{- Note [KickOutSpec] +~~~~~~~~~~~~~~~~~~~~~~ +KickOutSpec explains why we are kicking out. + +Important property: + KOAfterAdding (TyVarLHS tv) should behave exactly like + KOAfterUnifying (unitVarSet tv) + +The main reasons for treating the two separately are +* More efficient in the single-tyvar case +* The code is far more perspicuous +-} + +kickOutRewritableLHS :: KickOutSpec -> CtFlavourRole -> InertCans -> (Cts, InertCans) -- See Note [kickOutRewritable] -kickOutRewritableLHS new_fr new_lhs +kickOutRewritableLHS ko_spec new_fr@(_, new_role) ics@(IC { inert_eqs = tv_eqs , inert_dicts = dictmap , inert_funeqs = funeqmap @@ -1319,18 +1375,11 @@ kickOutRewritableLHS new_fr new_lhs , inert_irreds = irs_in , inert_insts = insts_in } - kicked_out :: WorkList - -- NB: use extendWorkList to ensure that kicked-out equalities get priority - -- See Note [Prioritise equalities] (Kick-out). - -- The irreds may include non-canonical (hetero-kinded) equality - -- constraints, which perhaps may have become soluble after new_lhs - -- is substituted; ditto the dictionaries, which may include (a~b) - -- or (a~~b) constraints. - kicked_out = foldr extendWorkListCt - (emptyWorkList { wl_eqs = map CEqCan tv_eqs_out ++ - map CEqCan feqs_out }) - ((dicts_out `andCts` irs_out) - `extendCtsList` insts_out) + kicked_out :: Cts + kicked_out = (dicts_out `andCts` irs_out) + `extendCtsList` insts_out + `extendCtsList` map CEqCan tv_eqs_out + `extendCtsList` map CEqCan feqs_out (tv_eqs_out, tv_eqs_in) = partitionInertEqs kick_out_eq tv_eqs (feqs_out, feqs_in) = partitionFunEqs kick_out_eq funeqmap @@ -1356,14 +1405,12 @@ kickOutRewritableLHS new_fr new_lhs | otherwise = Right qci - (_, new_role) = new_fr - - fr_tv_can_rewrite_ty :: TyVar -> EqRel -> Type -> Bool - fr_tv_can_rewrite_ty new_tv role ty + fr_tv_can_rewrite_ty :: (TyVar -> Bool) -> EqRel -> Type -> Bool + fr_tv_can_rewrite_ty ok_tv role ty = anyRewritableTyVar role can_rewrite ty where can_rewrite :: EqRel -> TyVar -> Bool - can_rewrite old_role tv = new_role `eqCanRewrite` old_role && tv == new_tv + can_rewrite old_role tv = new_role `eqCanRewrite` old_role && ok_tv tv fr_tf_can_rewrite_ty :: TyCon -> [TcType] -> EqRel -> Type -> Bool fr_tf_can_rewrite_ty new_tf new_tf_args role ty @@ -1376,28 +1423,23 @@ kickOutRewritableLHS new_fr new_lhs -- it's possible for old_tf_args to have too many. This is fine; -- we'll only check what we need to. - {-# INLINE fr_can_rewrite_ty #-} -- perform the check here only once + {-# INLINE fr_can_rewrite_ty #-} -- Perform case analysis on ko_spec only once fr_can_rewrite_ty :: EqRel -> Type -> Bool - fr_can_rewrite_ty = case new_lhs of - TyVarLHS new_tv -> fr_tv_can_rewrite_ty new_tv - TyFamLHS new_tf new_tf_args -> fr_tf_can_rewrite_ty new_tf new_tf_args + fr_can_rewrite_ty = case ko_spec of -- See Note [KickOutSpec] + KOAfterUnify tvs -> fr_tv_can_rewrite_ty (`elemVarSet` tvs) + KOAfterAdding (TyVarLHS tv) -> fr_tv_can_rewrite_ty (== tv) + KOAfterAdding (TyFamLHS tf tf_args) -> fr_tf_can_rewrite_ty tf tf_args fr_may_rewrite :: CtFlavourRole -> Bool fr_may_rewrite fs = new_fr `eqCanRewriteFR` fs -- Can the new item rewrite the inert item? - {-# INLINE kick_out_ct #-} -- perform case on new_lhs here only once kick_out_ct :: Ct -> Bool -- Kick it out if the new CEqCan can rewrite the inert one -- See Note [kickOutRewritable] - kick_out_ct = case new_lhs of - TyVarLHS new_tv -> \ct -> let fs@(_,role) = ctFlavourRole ct in - fr_may_rewrite fs - && fr_tv_can_rewrite_ty new_tv role (ctPred ct) - TyFamLHS new_tf new_tf_args - -> \ct -> let fs@(_, role) = ctFlavourRole ct in - fr_may_rewrite fs - && fr_tf_can_rewrite_ty new_tf new_tf_args role (ctPred ct) + kick_out_ct ct = fr_may_rewrite fs && fr_can_rewrite_ty role (ctPred ct) + where + fs@(_,role) = ctFlavourRole ct -- Implements criteria K1-K3 in Note [Extending the inert equalities] kick_out_eq :: EqCt -> Bool @@ -1430,13 +1472,31 @@ kickOutRewritableLHS new_fr new_lhs kick_out_for_completeness -- (K3) and Note [K3: completeness of solving] = case eq_rel of - NomEq -> rhs_ty `eqType` canEqLHSType new_lhs -- (K3a) - ReprEq -> is_can_eq_lhs_head new_lhs rhs_ty -- (K3b) - - - is_can_eq_lhs_head (TyVarLHS tv) = go + NomEq -> is_new_lhs rhs_ty -- (K3a) + ReprEq -> head_is_new_lhs rhs_ty -- (K3b) + + is_new_lhs :: Type -> Bool + is_new_lhs = case ko_spec of -- See Note [KickOutSpec] + KOAfterUnify tvs -> is_tyvar_ty_for tvs + KOAfterAdding lhs -> (`eqType` canEqLHSType lhs) + + is_tyvar_ty_for :: TcTyVarSet -> Type -> Bool + -- True if the type is equal to one of the tyvars + is_tyvar_ty_for tvs ty + = case getTyVar_maybe ty of + Nothing -> False + Just tv -> tv `elemVarSet` tvs + + head_is_new_lhs :: Type -> Bool + head_is_new_lhs = case ko_spec of -- See Note [KickOutSpec] + KOAfterUnify tvs -> tv_at_head (`elemVarSet` tvs) + KOAfterAdding (TyVarLHS tv) -> tv_at_head (== tv) + KOAfterAdding (TyFamLHS tf tf_args) -> fam_at_head tf tf_args + + tv_at_head :: (TyVar -> Bool) -> Type -> Bool + tv_at_head is_tv = go where - go (Rep.TyVarTy tv') = tv == tv' + go (Rep.TyVarTy tv) = is_tv tv go (Rep.AppTy fun _) = go fun go (Rep.CastTy ty _) = go ty go (Rep.TyConApp {}) = False @@ -1444,7 +1504,9 @@ kickOutRewritableLHS new_fr new_lhs go (Rep.ForAllTy {}) = False go (Rep.FunTy {}) = False go (Rep.CoercionTy {}) = False - is_can_eq_lhs_head (TyFamLHS fun_tc fun_args) = go + + fam_at_head :: TyCon -> [Type] -> Type -> Bool + fam_at_head fun_tc fun_args = go where go (Rep.TyVarTy {}) = False go (Rep.AppTy {}) = False -- no TyConApp to the left of an AppTy diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs index 809c71100b..e40478279c 100644 --- a/compiler/GHC/Tc/Solver/Interact.hs +++ b/compiler/GHC/Tc/Solver/Interact.hs @@ -11,7 +11,6 @@ import GHC.Tc.Solver.Canonical import GHC.Tc.Solver.Dict import GHC.Tc.Errors.Types import GHC.Tc.Utils.TcType -import GHC.Tc.Instance.FunDeps import GHC.Tc.Instance.Class ( safeOverlap ) import GHC.Tc.Types.Evidence import GHC.Tc.Types @@ -22,7 +21,6 @@ import GHC.Tc.Solver.InertSet import GHC.Tc.Solver.Monad import GHC.Core.InstEnv ( Coherence(..) ) -import GHC.Core.Class import GHC.Core.Predicate import GHC.Core.Coercion @@ -155,8 +153,7 @@ solveSimples :: Cts -> TcS () solveSimples cts = {-# SCC "solveSimples" #-} - do { updWorkListTcS (\wl -> foldr extendWorkListCt wl cts) - ; solve_loop } + do { emitWork cts; solve_loop } where solve_loop = {-# SCC "solve_loop" #-} @@ -308,7 +305,7 @@ runSolverPipeline :: [(String,SimplifierStage)] -- The pipeline -> WorkItem -- The work item -> TcS () -- Run this item down the pipeline, leaving behind new work and inerts -runSolverPipeline pipeline workItem +runSolverPipeline full_pipeline workItem = do { wl <- getWorkList ; inerts <- getTcSInerts ; tclevel <- getTcLevel @@ -320,7 +317,7 @@ runSolverPipeline pipeline workItem , text "rest of worklist =" <+> ppr wl ] ; bumpStepCountTcS -- One step for each constraint processed - ; final_res <- run_pipeline pipeline (ContinueWith workItem) + ; final_res <- run_pipeline full_pipeline workItem ; case final_res of Stop ev s -> do { traceFireTcS ev s @@ -330,26 +327,29 @@ runSolverPipeline pipeline workItem ; traceFireTcS (ctEvidence ct) (text "Kept as inert") ; traceTcS "End solver pipeline (kept as inert) }" $ (text "final_item =" <+> ppr ct) } + StartAgain ct -> pprPanic "runSolverPipeline: StartAgain" (ppr ct) } - where run_pipeline :: [(String,SimplifierStage)] -> StopOrContinue Ct - -> TcS (StopOrContinue Ct) - run_pipeline [] res = return res - run_pipeline _ (Stop ev s) = return (Stop ev s) - run_pipeline ((stg_name,stg):stgs) (ContinueWith ct) - = do { traceTcS ("runStage " ++ stg_name ++ " {") - (text "workitem = " <+> ppr ct) - ; res <- stg ct - ; traceTcS ("end stage " ++ stg_name ++ " }") empty - ; run_pipeline stgs res } + where + run_pipeline :: [(String,SimplifierStage)] -> Ct -> TcS (StopOrContinue Ct) + run_pipeline [] ct = return (ContinueWith ct) + run_pipeline ((stage_name,stage):stages) ct + = do { traceTcS ("runStage " ++ stage_name ++ " {") + (text "workitem = " <+> ppr ct) + ; res <- stage ct + ; traceTcS ("end stage " ++ stage_name ++ " }") (ppr res) + ; case res of + Stop {} -> return res + StartAgain ct -> run_pipeline full_pipeline ct + ContinueWith ct -> run_pipeline stages ct } {- Example 1: Inert: {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given) Reagent: a ~ [b] (given) -React with (c~d) ==> IR (ContinueWith (a~[b])) True [] -React with (F a ~ t) ==> IR (ContinueWith (a~[b])) False [F [b] ~ t] -React with (b ~ Int) ==> IR (ContinueWith (a~[Int]) True [] +React with (c~d) ==> IR (ContinueWith (a~[b])) True [] +React with (F a ~ t) ==> IR (ContinueWith (a~[b])) False [F [b] ~ t] +React with (b ~ Int) ==> IR (ContinueWith (a~[Int])) True [] Example 2: Inert: {c ~w d, F a ~g t, b ~w Int, a ~w ty} @@ -1025,8 +1025,7 @@ interactDict inerts ct_w@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = t = interactGivenIP inerts ct_w | otherwise - = do { addFunDepWork inerts ev_w cls - ; continueWith ct_w } + = continueWith ct_w interactDict _ wi = pprPanic "interactDict" (ppr wi) @@ -1131,44 +1130,6 @@ shortCutSolver dflags ev_w ev_i Nothing -> Fresh <$> newWantedNC loc (ctEvRewriters ev_w) pty | otherwise = mzero -addFunDepWork :: InertCans -> CtEvidence -> Class -> TcS () --- Add wanted constraints from type-class functional dependencies. -addFunDepWork inerts work_ev cls - = mapBagM_ add_fds (findDictsByClass (inert_dicts inerts) cls) - -- No need to check flavour; fundeps work between - -- any pair of constraints, regardless of flavour - -- Importantly we don't throw workitem back in the - -- worklist because this can cause loops (see #5236) - where - work_pred = ctEvPred work_ev - work_loc = ctEvLoc work_ev - - add_fds inert_ct - = do { traceTcS "addFunDepWork" (vcat - [ ppr work_ev - , pprCtLoc work_loc, ppr (isGivenLoc work_loc) - , pprCtLoc inert_loc, ppr (isGivenLoc inert_loc) - , pprCtLoc derived_loc, ppr (isGivenLoc derived_loc) ]) - - ; unless (isGiven work_ev && isGiven inert_ev) $ - emitFunDepWanteds (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 - -- Do not create FDs from Given/Given interactions: See Note [No Given/Given fundeps] - } - where - 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 - (ctLocOrigin work_loc) - (ctLocSpan work_loc) - inert_pred - (ctLocOrigin inert_loc) - (ctLocSpan inert_loc) } {- ********************************************************************** diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs index befc9e212e..91e20becf8 100644 --- a/compiler/GHC/Tc/Solver/Monad.hs +++ b/compiler/GHC/Tc/Solver/Monad.hs @@ -33,6 +33,7 @@ module GHC.Tc.Solver.Monad ( -- The pipeline StopOrContinue(..), continueWith, stopWith, andWhenContinue, + startAgainWith, -- Tracing etc panicTcS, traceTcS, @@ -51,7 +52,7 @@ module GHC.Tc.Solver.Monad ( unifyTyVar, reportUnifications, touchabilityAndShapeTest, setEvBind, setWantedEq, setWantedEvTerm, setEvBindIfWanted, - newEvVar, newGivenEvVar, newGivenEvVars, + newEvVar, newGivenEvVar, emitNewGivens, checkReductionDepth, getSolvedDicts, setSolvedDicts, @@ -95,7 +96,7 @@ module GHC.Tc.Solver.Monad ( instDFunType, -- Unification - unifyWanted, unifyWanteds, + wrapUnifierTcS, unifyFunDeps, uPairsTcM, -- MetaTyVars newFlexiTcSTy, instFlexiX, @@ -159,6 +160,7 @@ import GHC.Builtin.Names ( unsatisfiableClassNameKey ) import GHC.Core.Type import GHC.Core.TyCo.Rep as Rep import GHC.Core.Coercion +import GHC.Core.Coercion.Axiom( TypeEqn ) import GHC.Core.Predicate import GHC.Core.Reduction import GHC.Core.Class @@ -171,6 +173,7 @@ import GHC.Types.Name.Reader import GHC.Types.Var import GHC.Types.Var.Set import GHC.Types.Unique.Supply +import GHC.Types.Unique.Set( elementOfUniqSet ) import GHC.Unit.Module ( HasModule, getModule, extractModule ) import qualified GHC.Rename.Env as TcM @@ -184,12 +187,11 @@ import GHC.Data.Bag as Bag import GHC.Data.Pair import GHC.Utils.Monad -import GHC.Utils.Misc( equalLength ) import GHC.Exts (oneShot) import Control.Monad import Data.IORef -import Data.List ( mapAccumL, zip4 ) +import Data.List ( mapAccumL ) import Data.Foldable import qualified Data.Semigroup as S @@ -205,7 +207,10 @@ import GHC.Data.Graph.Directed ********************************************************************* -} data StopOrContinue a - = ContinueWith a -- The constraint was not solved, although it may have + = StartAgain a -- Constraint is not solved, but some unifications + -- happened, so go back to the beginning of the pipeline + + | ContinueWith a -- The constraint was not solved, although it may have -- been rewritten | Stop CtEvidence -- The (rewritten) constraint was solved @@ -216,21 +221,25 @@ data StopOrContinue a instance Outputable a => Outputable (StopOrContinue a) where ppr (Stop ev s) = text "Stop" <> parens s <+> ppr ev ppr (ContinueWith w) = text "ContinueWith" <+> ppr w + ppr (StartAgain w) = text "StartAgain" <+> ppr w + +startAgainWith :: a -> TcS (StopOrContinue a) +startAgainWith ct = return (StartAgain ct) continueWith :: a -> TcS (StopOrContinue a) -continueWith = return . ContinueWith +continueWith ct = return (ContinueWith ct) stopWith :: CtEvidence -> String -> TcS (StopOrContinue a) stopWith ev s = return (Stop ev (text s)) andWhenContinue :: TcS (StopOrContinue a) - -> (a -> TcS (StopOrContinue b)) - -> TcS (StopOrContinue b) + -> (a -> TcS (StopOrContinue a)) + -> TcS (StopOrContinue a) andWhenContinue tcs1 tcs2 = do { r <- tcs1 ; case r of - Stop ev s -> return (Stop ev s) - ContinueWith ct -> tcs2 ct } + ContinueWith ct -> tcs2 ct + _ -> return r } infixr 0 `andWhenContinue` -- allow chaining with ($) @@ -340,8 +349,9 @@ addInertCan ct = maybeKickOut :: InertCans -> Ct -> TcS InertCans -- For a CEqCan, kick out any inert that can be rewritten by the CEqCan maybeKickOut ics ct - | CEqCan (EqCt { eq_lhs = lhs, eq_ev = ev, eq_eq_rel = eq_rel }) <- ct - = do { (_, ics') <- kickOutRewritable (ctEvFlavour ev, eq_rel) lhs ics + | CEqCan eq_ct <- ct + = do { (_, ics') <- kickOutRewritable (KOAfterAdding (eqCtLHS eq_ct)) + (eqCtFlavourRole eq_ct) ics ; return ics' } -- See [Kick out existing binding for implicit parameter] @@ -368,61 +378,73 @@ maybeKickOut ics ct = return ics ----------------------------------------- -kickOutRewritable :: CtFlavourRole -- Flavour/role of the equality that - -- is being added to the inert set - -> CanEqLHS -- The new equality is lhs ~ ty - -> InertCans - -> TcS (Int, InertCans) -kickOutRewritable new_fr new_lhs ics - = do { let (kicked_out, ics') = kickOutRewritableLHS new_fr new_lhs ics - n_kicked = workListSize kicked_out +kickOutRewritable :: KickOutSpec -> CtFlavourRole + -> InertCans -> TcS (Int, InertCans) +kickOutRewritable ko_spec new_fr ics + = do { let (kicked_out, ics') = kickOutRewritableLHS ko_spec new_fr ics + n_kicked = lengthBag kicked_out - ; unless (n_kicked == 0) $ - do { updWorkListTcS (appendWorkList kicked_out) + ; unless (isEmptyBag kicked_out) $ + do { emitWork kicked_out -- The famapp-cache contains Given evidence from the inert set. -- If we're kicking out Givens, we need to remove this evidence -- from the cache, too. - ; let kicked_given_ev_vars = - [ ev_var | ct <- wl_eqs kicked_out - , CtGiven { ctev_evar = ev_var } <- [ctEvidence ct] ] + ; let kicked_given_ev_vars = foldr add_one emptyVarSet kicked_out + add_one :: Ct -> VarSet -> VarSet + add_one ct vs | CtGiven { ctev_evar = ev_var } <- ctEvidence ct + = vs `extendVarSet` ev_var + | otherwise = vs + ; when (new_fr `eqCanRewriteFR` (Given, NomEq) && -- if this isn't true, no use looking through the constraints - not (null kicked_given_ev_vars)) $ + not (isEmptyVarSet kicked_given_ev_vars)) $ do { traceTcS "Given(s) have been kicked out; drop from famapp-cache" (ppr kicked_given_ev_vars) - ; dropFromFamAppCache (mkVarSet kicked_given_ev_vars) } + ; dropFromFamAppCache kicked_given_ev_vars } ; csTraceTcS $ - hang (text "Kick out, lhs =" <+> ppr new_lhs) + hang (text "Kick out") 2 (vcat [ text "n-kicked =" <+> int n_kicked , text "kicked_out =" <+> ppr kicked_out , text "Residual inerts =" <+> ppr ics' ]) } ; return (n_kicked, ics') } -kickOutAfterUnification :: TcTyVar -> TcS Int -kickOutAfterUnification new_tv +kickOutAfterUnification :: [TcTyVar] -> TcS Int +kickOutAfterUnification tvs + | null tvs + = return 0 + | otherwise = do { ics <- getInertCans - ; (n_kicked, ics2) <- kickOutRewritable (Given,NomEq) - (TyVarLHS new_tv) ics - -- Given because the tv := xi is given; NomEq because - -- only nominal equalities are solved by unification - + ; let tv_set = mkVarSet tvs + ; (n_kicked, ics2) <- kickOutRewritable (KOAfterUnify tv_set) + (Given, NomEq) ics + -- Given because the tv := xi is given; NomEq because + -- only nominal equalities are solved by unification ; setInertCans ics2 + + -- Set the unification flag if we have done outer unifications + -- that might affect an earlier implication constraint + ; let min_tv_lvl = foldr1 minTcLevel (map tcTyVarLevel tvs) + ; ambient_lvl <- getTcLevel + ; when (ambient_lvl `strictlyDeeperThan` min_tv_lvl) $ + setUnificationFlag min_tv_lvl + + ; traceTcS "kickOutAfterUnification" (ppr tvs $$ text "n_kicked =" <+> ppr n_kicked) ; return n_kicked } --- See Wrinkle (2) in Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical +kickOutAfterFillingCoercionHole :: CoercionHole -> TcS () +-- See Wrinkle (EIK2) in Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical -- It's possible that this could just go ahead and unify, but could there be occurs-check -- problems? Seems simpler just to kick out. -kickOutAfterFillingCoercionHole :: CoercionHole -> TcS () kickOutAfterFillingCoercionHole hole = do { ics <- getInertCans ; let (kicked_out, ics') = kick_out ics - n_kicked = workListSize kicked_out + n_kicked = lengthBag kicked_out ; unless (n_kicked == 0) $ - do { updWorkListTcS (appendWorkList kicked_out) + do { updWorkListTcS (extendWorkListCts kicked_out) ; csTraceTcS $ hang (text "Kick out, hole =" <+> ppr hole) 2 (vcat [ text "n-kicked =" <+> int n_kicked @@ -431,19 +453,26 @@ kickOutAfterFillingCoercionHole hole ; setInertCans ics' } where - kick_out :: InertCans -> (WorkList, InertCans) - kick_out ics@(IC { inert_eqs = eqs, inert_funeqs = funeqs }) - = (kicked_out, ics { inert_eqs = eqs_to_keep, inert_funeqs = funeqs_to_keep }) + kick_out :: InertCans -> (Cts, InertCans) + kick_out ics@(IC { inert_irreds = irreds }) + = -- We only care about irreds here, because any constraint blocked + -- by a coercion hole is an irred. See wrinkle (EIK2a) in + -- Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical + (irreds_to_kick, ics { inert_irreds = irreds_to_keep }) where - (eqs_to_kick, eqs_to_keep) = partitionInertEqs kick_ct eqs - (funeqs_to_kick, funeqs_to_keep) = partitionFunEqs kick_ct funeqs - kicked_out = extendWorkListCts (map CEqCan (eqs_to_kick ++ funeqs_to_kick)) emptyWorkList + (irreds_to_kick, irreds_to_keep) = partitionBag kick_ct irreds - kick_ct :: EqCt -> Bool + kick_ct :: Ct -> Bool -- True: kick out; False: keep. - kick_ct (EqCt { eq_rhs = rhs, eq_ev = ctev }) - = isWanted ctev && -- optimisation: givens don't have coercion holes anyway - rhs `hasThisCoercionHoleTy` hole + kick_ct ct + | CIrredCan { cc_ev = ev, cc_reason = reason } <- ct + , CtWanted { ctev_rewriters = RewriterSet rewriters } <- ev + , NonCanonicalReason ctyeq <- reason + , ctyeq `cterHasProblem` cteCoercionHole + , hole `elementOfUniqSet` rewriters + = True + | otherwise + = False -------------- addInertSafehask :: InertCans -> Ct -> InertCans @@ -1258,12 +1287,21 @@ emitWorkNC evs | null evs = return () | otherwise - = emitWork (map mkNonCanonical evs) + = emitWork (listToBag (map mkNonCanonical evs)) -emitWork :: [Ct] -> TcS () -emitWork [] = return () -- avoid printing, among other work +emitWork :: Cts -> TcS () emitWork cts - = do { traceTcS "Emitting fresh work" (vcat (map ppr cts)) + | isEmptyBag cts -- Avoid printing, among other work + = return () + | otherwise + = do { traceTcS "Emitting fresh work" (pprBag cts) + -- Zonk the rewriter set of Wanteds, because that affects + -- the prioritisation of the work-list. Suppose a constraint + -- c1 is rewritten by another, c2. When c2 gets solved, + -- c1 has no rewriters, and can be prioritised; see + -- Note [Prioritise Wanteds with empty RewriterSet] + -- in GHC.Tc.Types.Constraint wrinkle (WRW1) + ; cts <- wrapTcS $ mapBagM TcM.zonkCtRewriterSet cts ; updWorkListTcS (extendWorkListCts cts) } emitImplication :: Implication -> TcS () @@ -1553,7 +1591,7 @@ track of - Whether any unifications at all have taken place (Nothing => no unifications) - If so, what is the outermost level that has seen a unification (Just lvl) -The iteration done in the simplify_loop/maybe_simplify_again loop in GHC.Tc.Solver. +The iteration is done in the simplify_loop/maybe_simplify_again loop in GHC.Tc.Solver. It helpful not to iterate unless there is a chance of progress. #8474 is an example: @@ -1627,20 +1665,22 @@ cloneMetaTyVar :: TcTyVar -> TcS TcTyVar cloneMetaTyVar tv = wrapTcS (TcM.cloneMetaTyVar tv) instFlexiX :: Subst -> [TKVar] -> TcS Subst -instFlexiX subst tvs - = wrapTcS (foldlM instFlexiHelper subst tvs) +instFlexiX subst tvs = wrapTcS (instFlexiXTcM subst tvs) -instFlexiHelper :: Subst -> TKVar -> TcM Subst +instFlexiXTcM :: Subst -> [TKVar] -> TcM Subst -- Makes fresh tyvar, extends the substitution, and the in-scope set -instFlexiHelper subst tv +-- Takes account of the case [k::Type, a::k, ...], +-- where we must substitute for k in a's kind +instFlexiXTcM subst [] + = return subst +instFlexiXTcM subst (tv:tvs) = do { uniq <- TcM.newUnique ; details <- TcM.newMetaDetails TauTv ; let name = setNameUnique (tyVarName tv) uniq kind = substTyUnchecked subst (tyVarKind tv) tv' = mkTcTyVar name kind details subst' = extendTvSubstWithClone subst tv tv' - ; TcM.traceTc "instFlexi" (ppr tv') - ; return (extendTvSubst subst' tv (mkTyVarTy tv')) } + ; instFlexiXTcM subst' tvs } matchGlobalInst :: DynFlags -> Bool -- True <=> caller is the short-cut solver @@ -1761,14 +1801,19 @@ newBoundEvVarId pred rhs ; setEvBind (mkGivenEvBind new_ev rhs) ; return new_ev } -newGivenEvVars :: CtLoc -> [(TcPredType, EvTerm)] -> TcS [CtEvidence] -newGivenEvVars loc pts = mapM (newGivenEvVar loc) pts +emitNewGivens :: CtLoc -> [(Role,TcType,TcType,TcCoercion)] -> TcS () +emitNewGivens loc pts + = do { evs <- mapM (newGivenEvVar loc) $ + [ (mkPrimEqPredRole role ty1 ty2, evCoercion co) + | (role, ty1, ty2, co) <- pts + , not (ty1 `tcEqType` ty2) ] -- Kill reflexive Givens at birth + ; emitWorkNC evs } emitNewWantedEq :: CtLoc -> RewriterSet -> Role -> TcType -> TcType -> TcS Coercion -- | Emit a new Wanted equality into the work-list emitNewWantedEq loc rewriters role ty1 ty2 = do { (ev, co) <- newWantedEq loc rewriters role ty1 ty2 - ; updWorkListTcS (extendWorkListEq (mkNonCanonical ev)) + ; updWorkListTcS (extendWorkListEq rewriters (mkNonCanonical ev)) ; return co } -- | Create a new Wanted constraint holding a coercion hole @@ -1776,8 +1821,7 @@ emitNewWantedEq loc rewriters role ty1 ty2 newWantedEq :: CtLoc -> RewriterSet -> Role -> TcType -> TcType -> TcS (CtEvidence, Coercion) newWantedEq loc rewriters role ty1 ty2 - = do { hole <- wrapTcS $ TcM.newCoercionHole pty - ; traceTcS "Emitting new coercion hole" (ppr hole <+> dcolon <+> ppr pty) + = do { hole <- wrapTcS $ TcM.newCoercionHole loc pty ; return ( CtWanted { ctev_pred = pty , ctev_dest = HoleDest hole , ctev_loc = loc @@ -1906,43 +1950,47 @@ solverDepthError loc ty ************************************************************************ -} -emitFunDepWanteds :: RewriterSet -- from the work item - -> [FunDepEqn (CtLoc, RewriterSet)] -> TcS () +emitFunDepWanteds :: CtEvidence -- The work item + -> [FunDepEqn (CtLoc, RewriterSet)] + -> TcS Bool -- True <=> some unification happened -emitFunDepWanteds _ [] = return () -- common case noop +emitFunDepWanteds _ [] = return False -- common case noop -- See Note [FunDep and implicit parameter reactions] -emitFunDepWanteds work_rewriters fd_eqns - = mapM_ do_one_FDEqn fd_eqns +emitFunDepWanteds ev fd_eqns + = unifyFunDeps ev Nominal do_fundeps where - do_one_FDEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = (loc, rewriters) }) - | null tvs -- Common shortcut - = do { traceTcS "emitFunDepWanteds 1" (ppr (ctl_depth loc) $$ ppr eqs $$ ppr (isGivenLoc loc)) - ; mapM_ (\(Pair ty1 ty2) -> unifyWanted all_rewriters loc Nominal ty1 ty2) - (reverse eqs) } - -- See Note [Reverse order of fundep equations] - - | otherwise - = do { traceTcS "emitFunDepWanteds 2" (ppr (ctl_depth loc) $$ ppr tvs $$ ppr eqs) - ; subst <- instFlexiX emptySubst tvs -- Takes account of kind substitution - ; mapM_ (do_one_eq loc all_rewriters subst) (reverse eqs) } - -- See Note [Reverse order of fundep equations] - where - all_rewriters = work_rewriters S.<> rewriters - - do_one_eq loc rewriters subst (Pair ty1 ty2) - = unifyWanted rewriters loc Nominal (substTyUnchecked subst' ty1) ty2 - -- ty2 does not mention fd_qtvs, so no need to subst it. - -- See GHC.Tc.Instance.Fundeps Note [Improving against instances] - -- Wrinkle (1) + do_fundeps :: UnifyEnv -> TcM () + do_fundeps env = mapM_ (do_one env) fd_eqns + + do_one :: UnifyEnv -> FunDepEqn (CtLoc, RewriterSet) -> TcM () + do_one uenv (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = (loc, rewriters) }) + = do { eqs' <- instantiate_eqs tvs (reverse eqs) + -- (reverse eqs): See Note [Reverse order of fundep equations] + ; uPairsTcM env_one eqs' } where - subst' = extendSubstInScopeSet subst (tyCoVarsOfType ty1) - -- The free vars of ty1 aren't just fd_qtvs: ty1 is the result - -- of matching with the [W] constraint. So we add its free - -- vars to InScopeSet, to satisfy substTy's invariants, even - -- though ty1 will never (currently) be a poytype, so this - -- InScopeSet will never be looked at. + env_one = uenv { u_rewriters = u_rewriters uenv S.<> rewriters + , u_loc = loc } + instantiate_eqs :: [TyVar] -> [TypeEqn] -> TcM [TypeEqn] + instantiate_eqs tvs eqs + | null tvs + = return eqs + | otherwise + = do { TcM.traceTc "emitFunDepWanteds 2" (ppr tvs $$ ppr eqs) + ; subst <- instFlexiXTcM emptySubst tvs -- Takes account of kind substitution + ; return [ Pair (substTyUnchecked subst' ty1) ty2 + -- ty2 does not mention fd_qtvs, so no need to subst it. + -- See GHC.Tc.Instance.Fundeps Note [Improving against instances] + -- Wrinkle (1) + | Pair ty1 ty2 <- eqs + , let subst' = extendSubstInScopeSet subst (tyCoVarsOfType ty1) ] + -- The free vars of ty1 aren't just fd_qtvs: ty1 is the result + -- of matching with the [W] constraint. So we add its free + -- vars to InScopeSet, to satisfy substTy's invariants, even + -- though ty1 will never (currently) be a poytype, so this + -- InScopeSet will never be looked at. + } {- ************************************************************************ @@ -1951,121 +1999,86 @@ emitFunDepWanteds work_rewriters fd_eqns * * ************************************************************************ -Note [unifyWanted] -~~~~~~~~~~~~~~~~~~ +Note [wrapUnifierTcS] +~~~~~~~~~~~~~~~~~~~ When decomposing equalities we often create new wanted constraints for (s ~ t). But what if s=t? Then it'd be faster to return Refl right away. -Rather than making an equality test (which traverses the structure of the -type, perhaps fruitlessly), unifyWanted traverses the common structure, and -bales out when it finds a difference by creating a new Wanted constraint. -But where it succeeds in finding common structure, it just builds a coercion -to reflect it. +Rather than making an equality test (which traverses the structure of the type, +perhaps fruitlessly), we call uType (via wrapUnifierTcS) to traverse the common +structure, and bales out when it finds a difference by creating a new deferred +Wanted constraint. But where it succeeds in finding common structure, it just +builds a coercion to reflect it. + +This is all much faster than creating a new constraint, putting it in the +work list, picking it out, canonicalising it, etc etc. + +Note [unifyFunDeps] +~~~~~~~~~~~~~~~~~~~ +The Bool returned by `unifyFunDeps` is True if we have unified a variable +that occurs in the constraint we are trying to solve; it is not in the +inert set so `wrapUnifierTcS` won't kick it out. Instead we want to send it +back to the start of the pipeline. Hence the Bool. + +It's vital that we don't return (not (null unified)) because the fundeps +may create fresh variables; unifying them (alone) should not make us send +the constraint back to the start, or we'll get an infinite loop. See +Note [Fundeps with instances, and equality orientation] in GHC.Tc.Solver.Dict +and Note [Improvement orientation] in GHC.Tc.Solver.Equality. -} -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] --- The returned coercion's role matches the input parameter -unifyWanted rewriters loc Phantom ty1 ty2 - = do { kind_co <- unifyWanted rewriters loc Nominal (typeKind ty1) (typeKind ty2) - ; return (mkPhantomCo kind_co ty1 ty2) } - -unifyWanted rewriters loc role orig_ty1 orig_ty2 - = go orig_ty1 orig_ty2 - where - go ty1 ty2 | Just ty1' <- coreView ty1 = go ty1' ty2 - go ty1 ty2 | Just ty2' <- coreView ty2 = go ty1 ty2' - - go (FunTy af1 w1 s1 t1) (FunTy af2 w2 s2 t2) - | af1 == af2 -- Important! See #21530 - = do { co_s <- unifyWanted rewriters loc role s1 s2 - ; co_t <- unifyWanted rewriters loc role t1 t2 - ; co_w <- unifyWanted rewriters loc Nominal w1 w2 - ; return (mkNakedFunCo1 role af1 co_w 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 rewriters loc) - (tyConRoleListX role tc1) tys1 tys2 - ; return (mkTyConAppCo role tc1 cos) } - - go ty1@(TyVarTy tv) ty2 - = do { mb_ty <- isFilledMetaTyVar_maybe tv - ; case mb_ty of - Just ty1' -> go ty1' ty2 - Nothing -> bale_out ty1 ty2} - go ty1 ty2@(TyVarTy tv) - = do { mb_ty <- isFilledMetaTyVar_maybe tv - ; case mb_ty of - Just ty2' -> go ty1 ty2' - Nothing -> bale_out ty1 ty2 } - - go ty1@(CoercionTy {}) (CoercionTy {}) - = return (mkReflCo role ty1) -- we just don't care about coercions! - - go ty1 ty2 = bale_out ty1 ty2 - - bale_out ty1 ty2 - | ty1 `tcEqType` ty2 = return (mkReflCo role ty1) - -- Check for equality; e.g. a ~ a, or (m a) ~ (m a) - | otherwise = emitNewWantedEq loc rewriters role orig_ty1 orig_ty2 - - -{- -Note [Decomposing Dependent TyCons and Processing Wanted Equalities] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -When we decompose a dependent tycon we obtain a list of -mixed wanted type and kind equalities. Ideally we want -all the kind equalities to get solved first so that we avoid -generating duplicate kind equalities - -For example, consider decomposing a TyCon equality +uPairsTcM :: UnifyEnv -> [TypeEqn] -> TcM () +uPairsTcM uenv eqns = mapM_ (\(Pair ty1 ty2) -> uType uenv ty1 ty2) eqns - (0) [W] T k_fresh (t1::k_fresh) ~ T k1 (t2::k_fresh) - -This gives rise to 2 equalities in the solver worklist +unifyFunDeps :: CtEvidence -> Role + -> (UnifyEnv -> TcM ()) + -> TcS Bool +unifyFunDeps ev role do_unifications + = do { (_, _, unified) <- wrapUnifierTcS ev role do_unifications + ; return (any (`elemVarSet` fvs) unified) } + -- See Note [unifyFunDeps] + where + fvs = tyCoVarsOfType (ctEvPred ev) + +wrapUnifierTcS :: CtEvidence -> Role + -> (UnifyEnv -> TcM a) -- Some calls to uType + -> TcS (a, Bag Ct, [TcTyVar]) +-- Invokes the do_unifications argument, with a suitable UnifyEnv. +-- Emit deferred equalities and kick-out from the inert set as a +-- result of any unifications. +-- Very good short-cut when the two types are equal, or nearly so +-- See Note [wrapUnifierTcS] +-- +-- The [TcTyVar] is the list of unification variables that were +-- unified the process; the (Bag Ct) are the deferred constraints. - (1) [W] k_fresh ~ k1 - (2) [W] t1::k_fresh ~ t2::k1 +wrapUnifierTcS ev role do_unifications + = do { (cos, unified, rewriters, cts) <- wrapTcS $ + do { defer_ref <- TcM.newTcRef emptyBag + ; unified_ref <- TcM.newTcRef [] + ; rewriters <- TcM.zonkRewriterSet (ctEvRewriters ev) + ; let env = UE { u_role = role + , u_rewriters = rewriters + , u_loc = ctEvLoc ev + , u_defer = defer_ref + , u_unified = Just unified_ref} -The solver worklist is processed in LIFO order: -see GHC.Tc.Solver.InertSet.selectWorkItem. -i.e. (2) is processed _before_ (1). Now, while solving (2) -we would call `canEqCanLHSHetero` and that would emit a -wanted kind equality + ; cos <- do_unifications env - (3) [W] k_fresh ~ k1 + ; cts <- TcM.readTcRef defer_ref + ; unified <- TcM.readTcRef unified_ref + ; return (cos, unified, rewriters, cts) } -But (3) is exactly the same as (1)! + -- Emit the deferred constraints + -- See Note [Work-list ordering] in GHC.Tc.Solved.Equality + ; unless (isEmptyBag cts) $ + updWorkListTcS (extendWorkListEqs rewriters cts) -To avoid such duplicate wanted constraints from being added to the worklist, -we ensure that (2) is processed before (1). Since we are processing -the worklist in a LIFO ordering, we do it by emitting (1) before (2). -This is exactly what we do in `unifyWanteds`. + -- And kick out any inert constraint that we have unified + ; _ <- kickOutAfterUnification unified -NB: This ordering is not needed when we decompose FunTyCons as they are not dependently typed --} + ; return (cos, cts, unified) } --- NB: Length of [CtLoc] and [Roles] may be infinite --- but list of RHS [TcType] and LHS [TcType] is finite and both are of equal length -unifyWanteds :: RewriterSet -> [CtLoc] -> [Role] - -> [TcType] -- List of RHS types - -> [TcType] -- List of LHS types - -> TcS [Coercion] -unifyWanteds rewriters ctlocs roles rhss lhss = unify_wanteds rewriters $ zip4 ctlocs roles rhss lhss - where - -- Order is important here - -- See Note [Decomposing Dependent TyCons and Processing Wanted Equalities] - unify_wanteds _ [] = return [] - unify_wanteds rewriters ((new_loc, tc_role, ty1, ty2) : rest) - = do { cos <- unify_wanteds rewriters rest - ; co <- unifyWanted rewriters new_loc tc_role ty1 ty2 - ; return (co:cos) } {- ************************************************************************ @@ -2081,7 +2094,7 @@ checkTouchableTyVarEq -> TcType -- The RHS -> TcS (PuResult () Reduction) -- Used for Nominal, Wanted equalities, with a touchable meta-tyvar on LHS --- If checkTouchableTyVarEq tv ty = PuOK redn cts +-- If checkTouchableTyVarEq tv ty = PuOK cts redn -- then we can unify -- tv := ty |> redn -- with extra wanteds 'cts' @@ -2098,7 +2111,7 @@ checkTouchableTyVarEq ev lhs_tv rhs ; traceTcS "checkTouchableTyVarEq }" (ppr lhs_tv $$ ppr check_result) ; case check_result of PuFail reason -> return (PuFail reason) - PuOK redn cts -> do { emitWork (bagToList cts) + PuOK cts redn -> do { emitWork cts ; return (pure redn) } } where @@ -2147,13 +2160,13 @@ checkTouchableTyVarEq ev lhs_tv rhs _ -> TcM.newMetaTyVarTyAtLevel lhs_tv_lvl fam_app_kind ; let pty = mkPrimEqPredRole Nominal fam_app new_tv_ty - ; hole <- TcM.newCoercionHole pty + ; hole <- TcM.newVanillaCoercionHole pty ; let new_ev = CtWanted { ctev_pred = pty , ctev_dest = HoleDest hole , ctev_loc = cb_loc , ctev_rewriters = ctEvRewriters ev } - ; return (PuOK (mkReduction (HoleCo hole) new_tv_ty) - (singleCt (mkNonCanonical new_ev))) } } + ; return (PuOK (singleCt (mkNonCanonical new_ev)) + (mkReduction (HoleCo hole) new_tv_ty)) } } -- See Detail (7) of the Note cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin @@ -2171,8 +2184,8 @@ checkTypeEq ev eq_rel lhs rhs ; traceTcS "checkTypeEq }" (ppr check_result) ; case check_result of PuFail reason -> return (PuFail reason) - PuOK redn prs -> do { new_givens <- mapBagM mk_new_given prs - ; emitWorkNC (bagToList new_givens) + PuOK prs redn -> do { new_givens <- mapBagM mk_new_given prs + ; emitWork new_givens ; updInertTcS (addCycleBreakerBindings prs) ; return (pure redn) } } @@ -2180,9 +2193,10 @@ checkTypeEq ev eq_rel lhs rhs = do { check_result <- wrapTcS (checkTyEqRhs wanted_flags rhs) ; case check_result of PuFail reason -> return (PuFail reason) - PuOK redn cts -> do { emitWork (bagToList cts) + PuOK cts redn -> do { emitWork cts ; return (pure redn) } } where + check_given_rhs :: TcType -> TcM (PuResult (TcTyVar,TcType) Reduction) check_given_rhs rhs -- See Note [Special case for top-level of Given equality] | Just (TyFamLHS tc tys) <- canTyFamEqLHS_maybe rhs @@ -2192,6 +2206,7 @@ checkTypeEq ev eq_rel lhs rhs arg_flags = famAppArgFlags given_flags + given_flags :: TyEqFlags (TcTyVar,TcType) given_flags = TEF { tef_lhs = lhs , tef_foralls = False , tef_unifying = NotUnifying @@ -2215,14 +2230,14 @@ checkTypeEq ev eq_rel lhs rhs break_given :: TcType -> TcM (PuResult (TcTyVar,TcType) Reduction) break_given fam_app = do { new_tv <- TcM.newCycleBreakerTyVar (typeKind fam_app) - ; return (PuOK (mkReflRedn Nominal (mkTyVarTy new_tv)) - (unitBag (new_tv, fam_app))) } + ; return (PuOK (unitBag (new_tv, fam_app)) + (mkReflRedn Nominal (mkTyVarTy new_tv))) } -- Why reflexive? See Detail (4) of the Note --------------------------- - mk_new_given :: (TcTyVar, TcType) -> TcS CtEvidence + mk_new_given :: (TcTyVar, TcType) -> TcS Ct mk_new_given (new_tv, fam_app) - = newGivenEvVar cb_loc (given_pred, given_term) + = mkNonCanonical <$> newGivenEvVar cb_loc (given_pred, given_term) where new_ty = mkTyVarTy new_tv given_pred = mkPrimEqPred fam_app new_ty diff --git a/compiler/GHC/Tc/Solver/Rewrite.hs b/compiler/GHC/Tc/Solver/Rewrite.hs index 6508a21420..64d590cbe9 100644 --- a/compiler/GHC/Tc/Solver/Rewrite.hs +++ b/compiler/GHC/Tc/Solver/Rewrite.hs @@ -41,6 +41,7 @@ import Control.Applicative (liftA3) import GHC.Builtin.Types (tYPETyCon) import Data.List ( find ) import GHC.Data.List.Infinite (Infinite) +import GHC.Data.Bag( listToBag ) import qualified GHC.Data.List.Infinite as Inf {- @@ -155,7 +156,7 @@ bumpDepth (RewriteM thing_inside) -- Precondition: the CtEvidence is a CtWanted of an equality recordRewriter :: CtEvidence -> RewriteM () recordRewriter (CtWanted { ctev_dest = HoleDest hole }) - = RewriteM $ \env -> updTcRef (re_rewriters env) (`addRewriterSet` hole) + = RewriteM $ \env -> updTcRef (re_rewriters env) (`addRewriter` hole) recordRewriter other = pprPanic "recordRewriter" (ppr other) {- @@ -945,7 +946,7 @@ runTcPluginRewriters rewriteEnv rewriterFunctions tys TcPluginRewriteTo { tcPluginReduction = redn , tcRewriterNewWanteds = wanteds - } -> do { emitWork wanteds; return $ Just redn } + } -> do { emitWork (listToBag wanteds); return $ Just redn } TcPluginNoRewrite {} -> runRewriters givens rewriters {- diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs index d99f9067df..78c1134475 100644 --- a/compiler/GHC/Tc/Types/Constraint.hs +++ b/compiler/GHC/Tc/Types/Constraint.hs @@ -10,7 +10,7 @@ module GHC.Tc.Types.Constraint ( QCInst(..), pendingScInst_maybe, -- Canonical constraints - Xi, Ct(..), EqCt(..), Cts, + Xi, Ct(..), Cts, singleCt, listToCts, ctsElts, consCts, snocCts, extendCtsList, isEmptyCts, emptyCts, andCts, ctsPreds, isPendingScDict, pendingScDict_maybe, @@ -43,6 +43,8 @@ module GHC.Tc.Types.Constraint ( cterHasNoProblem, cterHasProblem, cterHasOnlyProblem, cterHasOnlyProblems, cterRemoveProblem, cterHasOccursCheck, cterFromKind, + + EqCt(..), eqCtLHS, eqCtEvidence, CanEqLHS(..), canEqLHS_maybe, canTyFamEqLHS_maybe, canEqLHSKind, canEqLHSType, eqCanEqLHS, @@ -68,11 +70,11 @@ module GHC.Tc.Types.Constraint ( ctLocTypeOrKind_maybe, ctLocDepth, bumpCtLocDepth, isGivenLoc, setCtLocOrigin, updateCtLocOrigin, setCtLocEnv, setCtLocSpan, - pprCtLoc, + pprCtLoc, adjustCtLoc, adjustCtLocTyConBinder, -- CtEvidence CtEvidence(..), TcEvDest(..), - mkKindLoc, toKindLoc, mkGivenLoc, + mkKindEqLoc, toKindLoc, toInvisibleLoc, mkGivenLoc, isWanted, isGiven, ctEvRole, setCtEvPredType, setCtEvLoc, arisesFromGivens, tyCoVarsOfCtEvList, tyCoVarsOfCtEv, tyCoVarsOfCtEvsList, @@ -80,8 +82,7 @@ module GHC.Tc.Types.Constraint ( RewriterSet(..), emptyRewriterSet, isEmptyRewriterSet, -- exported concretely only for anyUnfilledCoercionHoles - rewriterSetFromType, rewriterSetFromTypes, rewriterSetFromCo, - addRewriterSet, + addRewriter, unitRewriterSet, unionRewriterSet, rewriterSetFromCts, wrapType, @@ -132,7 +133,6 @@ import GHC.Utils.Constants (debugIsOn) import GHC.Types.Name.Reader import Data.Coerce -import Data.Monoid ( Endo(..) ) import qualified Data.Semigroup as S import Control.Monad ( msum, when ) import Data.Maybe ( mapMaybe, isJust ) @@ -234,8 +234,8 @@ data Ct -- look like this, with the payload in an -- auxiliary type -{- Note [Invariants of EqCt] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +{- Note [Canonical equalities] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ An EqCt is a canonical equality constraint, one that can live in the inert set, and that can be used to rewrite other constrtaints. It satisfies these invariants: * (TyEq:OC) lhs does not occur in rhs (occurs check) @@ -249,6 +249,9 @@ and that can be used to rewrite other constrtaints. It satisfies these invariant (Applies only when constructor of newtype is in scope.) * (TyEq:U) An EqCt is not immediately unifiable. If we can unify a:=ty, we will not form an EqCt (a ~ ty). + * (TyEq:CH) rhs does not mention any coercion holes that resulted from fixing up + a hetero-kinded equality. See Note [Equalities with incompatible kinds] in + GHC.Tc.Solver.Equality, wrinkle (EIK2) These invariants ensure that the EqCts in inert_eqs constitute a terminating generalised substitution. See Note [inert_eqs: the inert equalities] @@ -286,7 +289,7 @@ and forms condition T3 in Note [Extending the inert equalities] in GHC.Tc.Solver.InertSet. -} -data EqCt -- An equality constraint; see Note [Invariants of EqCt] +data EqCt -- An equality constraint; see Note [Canonical equalities] = EqCt { -- CanEqLHS ~ rhs eq_ev :: CtEvidence, -- See Note [Ct/evidence invariant] eq_lhs :: CanEqLHS, @@ -294,6 +297,12 @@ data EqCt -- An equality constraint; see Note [Invariants of EqCt] eq_eq_rel :: EqRel -- INVARIANT: cc_eq_rel = ctEvEqRel cc_ev } +eqCtEvidence :: EqCt -> CtEvidence +eqCtEvidence = eq_ev + +eqCtLHS :: EqCt -> CanEqLHS +eqCtLHS = eq_lhs + ------------ -- | A 'CanEqLHS' is a type that can appear on the left of a canonical -- equality: a type variable or /exactly-saturated/ type family application. @@ -2083,41 +2092,26 @@ newtype RewriterSet = RewriterSet (UniqSet CoercionHole) emptyRewriterSet :: RewriterSet emptyRewriterSet = RewriterSet emptyUniqSet +unitRewriterSet :: CoercionHole -> RewriterSet +unitRewriterSet = coerce (unitUniqSet @CoercionHole) + +unionRewriterSet :: RewriterSet -> RewriterSet -> RewriterSet +unionRewriterSet = coerce (unionUniqSets @CoercionHole) + 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 (rewriter_set_from_co co) emptyRewriterSet - --- | Makes a 'RewriterSet' from all the coercion holes that occur in the --- given type. -rewriterSetFromType :: Type -> RewriterSet -rewriterSetFromType ty = appEndo (rewriter_set_from_ty ty) emptyRewriterSet - --- | Makes a 'RewriterSet' from all the coercion holes that occur in the --- given types. -rewriterSetFromTypes :: [Type] -> RewriterSet -rewriterSetFromTypes tys = appEndo (rewriter_set_from_tys tys) emptyRewriterSet - -rewriter_set_from_ty :: Type -> Endo RewriterSet -rewriter_set_from_tys :: [Type] -> Endo RewriterSet -rewriter_set_from_co :: Coercion -> Endo RewriterSet -(rewriter_set_from_ty, rewriter_set_from_tys, rewriter_set_from_co, _) - = foldTyCo folder () +isEmptyRewriterSet = coerce (isEmptyUniqSet @CoercionHole) + +addRewriter :: RewriterSet -> CoercionHole -> RewriterSet +addRewriter = coerce (addOneToUniqSet @CoercionHole) + +rewriterSetFromCts :: Bag Ct -> RewriterSet +-- Take a bag of Wanted equalities, and collect them as a RewriterSet +rewriterSetFromCts cts + = foldr add emptyRewriterSet cts where - folder :: TyCoFolder () (Endo RewriterSet) - folder = TyCoFolder - { tcf_view = noView - , tcf_tyvar = \ _ tv -> rewriter_set_from_ty (tyVarKind tv) - , tcf_covar = \ _ cv -> rewriter_set_from_ty (varType cv) - , tcf_hole = \ _ hole -> coerce (`addOneToUniqSet` hole) S.<> - rewriter_set_from_ty (varType (coHoleCoVar hole)) - , tcf_tycobinder = \ _ _ _ -> () } + add ct rw_set = case ctEvidence ct of + CtWanted { ctev_dest = HoleDest hole } -> rw_set `addRewriter` hole + _ -> rw_set {- ************************************************************************ @@ -2202,10 +2196,22 @@ TL;DR we want equality saturation. We thus want Wanteds to rewrite Wanteds in order to accept more programs, but we don't want Wanteds to rewrite Wanteds because doing so can create -inscrutable error messages. We choose to allow the rewriting, but -every Wanted tracks the set of Wanteds it has been rewritten by. This is -called a RewriterSet, stored in the ctev_rewriters field of the CtWanted -constructor of CtEvidence. (Only Wanteds have RewriterSets.) +inscrutable error messages. To solve this dilemma: + +* We allow Wanteds to rewrite Wanteds, but... + +* Each Wanted tracks the set of Wanteds it has been rewritten by, in its + RewriterSet, stored in the ctev_rewriters field of the CtWanted + constructor of CtEvidence. (Only Wanteds have RewriterSets.) + +* In error reporting, we simply suppress any errors that have been rewritten + by /unsolved/ wanteds. This suppression happens in GHC.Tc.Errors.mkErrorItem, + which uses GHC.Tc.Utils.anyUnfilledCoercionHoles to look through any filled + coercion holes. The idea is that we wish to report the "root cause" -- the + error that rewrote all the others. + +* We prioritise Wanteds that have an empty RewriterSet: + see Note [Prioritise Wanteds with empty RewriterSet]. Let's continue our first example above: @@ -2219,25 +2225,72 @@ Because Wanteds can rewrite Wanteds, w1 will rewrite w2, yielding The {w1} in the second line of output is the RewriterSet of w1. -A RewriterSet is just a set of unfilled CoercionHoles. This is -sufficient because only equalities (evidenced by coercion holes) are -used for rewriting; other (dictionary) constraints cannot ever -rewrite. The rewriter (in e.g. GHC.Tc.Solver.Rewrite.rewrite) tracks -and returns a RewriterSet, consisting of the evidence (a CoercionHole) -for any Wanted equalities used in rewriting. Then rewriteEvidence and -rewriteEqEvidence (in GHC.Tc.Solver.Canonical) add this RewriterSet to -the rewritten constraint's rewriter set. - -In error reporting, we simply suppress any errors that have been rewritten by -/unsolved/ wanteds. This suppression happens in GHC.Tc.Errors.mkErrorItem, which -uses GHC.Tc.Utils.anyUnfilledCoercionHoles to look through any filled coercion -holes. The idea is that we wish to report the "root cause" -- the error that -rewrote all the others. - -Wrinkle: In #22707, we have a case where all of the Wanteds have rewritten -each other. In order to report /some/ error in this case, we simply report -all the Wanteds. The user will get a perhaps-confusing error message, but -they've written a confusing program! +A RewriterSet is just a set of unfilled CoercionHoles. This is sufficient +because only equalities (evidenced by coercion holes) are used for rewriting; +other (dictionary) constraints cannot ever rewrite. The rewriter (in +e.g. GHC.Tc.Solver.Rewrite.rewrite) tracks and returns a RewriterSet, +consisting of the evidence (a CoercionHole) for any Wanted equalities used in +rewriting. Then rewriteEvidence and rewriteEqEvidence (in GHC.Tc.Solver.Canonical) +add this RewriterSet to the rewritten constraint's arewriter set. + +Note [Prioritise Wanteds with empty RewriterSet] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When extending the WorkList, in GHC.Tc.Solver.InertSet.extendWorkListEq, +we priorities constraints that have no rewriters. Here's why. + +Consider this, which came up in T22793: + inert: {} + work list: [W] co_ayf : awq ~ awo + work item: [W] co_ayb : awq ~ awp + + ==> {just put work item in inert set} + inert: co_ayb : awq ~ awp + work list: {} + work: [W] co_ayf : awq ~ awo + + ==> {rewrite ayf with co_ayb} + work list: {} + inert: co_ayb : awq ~ awp + co_aym{co_ayb} : awp ~ awo + ^ rewritten by ayb + + ----- start again in simplify_loop in Solver.hs ----- + inert: {} + work list: [W] co_ayb : awq ~ awp + work: co_aym{co_ayb} : awp ~ awo + + ==> {add to inert set} + inert: co_aym{co_ayb} : awp ~ awo + work list: {} + work: co_ayb : awq ~ awp + + ==> {rewrite co_ayb} + inert: co_aym{co_ayb} : awp ~ awo + co_ayp{co_aym} : awq ~ awo + work list: {} + +Now both wanteds have been rewriten by the other! This happened because +in our simplify_loop iteration, we happened to start with co_aym. All would have +been well if we'd started with the (not-rewritten) co_ayb and gotten it into the +inert set. + +With that in mind, we /prioritise/ the work-list to put constraints +with no rewriters first. This prioritisation is done in +GHC.Tc.Solver.InertSet.extendWorkListEq, and extendWorkListEqs. + +Wrinkles + +(WRW1) Before checking for an empty RewriterSet, we zonk the RewriterSet, + because some of those CoercionHoles may have been filled in since we last + looked: see GHC.Tc.Solver.Monad.emitWork. + +(WRW2) Despite the prioritisation, it is hard to be /certain/ that we can't end up + in a situation where all of the Wanteds have rewritten each other. In + order to report /some/ error in this case, we simply report all the + Wanteds. The user will get a perhaps-confusing error message, but they've + written a confusing program! (T22707 and T22793 were close, but they do + not exhibit this behaviour.) So belt and braces: see the `suppress` + stuff in GHC.Tc.Errors.mkErrorItem. Note [Avoiding rewriting cycles] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2416,10 +2469,11 @@ dictionaries don't appear in the original source code. -} -data CtLoc = CtLoc { ctl_origin :: CtOrigin - , ctl_env :: TcLclEnv - , ctl_t_or_k :: Maybe TypeOrKind -- OK if we're not sure - , ctl_depth :: !SubGoalDepth } +data CtLoc + = CtLoc { ctl_origin :: CtOrigin + , ctl_env :: TcLclEnv + , ctl_t_or_k :: Maybe TypeOrKind -- Used only to improve error messages + , ctl_depth :: !SubGoalDepth } -- The TcLclEnv includes particularly -- source location: tcl_loc :: RealSrcSpan @@ -2427,16 +2481,40 @@ data CtLoc = CtLoc { ctl_origin :: CtOrigin -- binder stack: tcl_bndrs :: TcBinderStack -- level: tcl_tclvl :: TcLevel -mkKindLoc :: TcType -> TcType -- original *types* being compared - -> CtLoc -> CtLoc -mkKindLoc s1 s2 loc = setCtLocOrigin (toKindLoc loc) - (KindEqOrigin s1 s2 (ctLocOrigin loc) - (ctLocTypeOrKind_maybe loc)) +mkKindEqLoc :: TcType -> TcType -- original *types* being compared + -> CtLoc -> CtLoc +mkKindEqLoc s1 s2 ctloc + | CtLoc { ctl_t_or_k = t_or_k, ctl_origin = origin } <- ctloc + = ctloc { ctl_origin = KindEqOrigin s1 s2 origin t_or_k + , ctl_t_or_k = Just KindLevel } + +adjustCtLocTyConBinder :: TyConBinder -> CtLoc -> CtLoc +-- Adjust the CtLoc when decomposing a type constructor +adjustCtLocTyConBinder tc_bndr loc + = adjustCtLoc is_vis is_kind loc + where + is_vis = isVisibleTyConBinder tc_bndr + is_kind = isNamedTyConBinder tc_bndr + +adjustCtLoc :: Bool -- True <=> A visible argument + -> Bool -- True <=> A kind argument + -> CtLoc -> CtLoc +-- Adjust the CtLoc when decomposing a type constructor, application, etc +adjustCtLoc is_vis is_kind loc + = loc2 + where + loc1 | is_kind = toKindLoc loc + | otherwise = loc + loc2 | is_vis = loc1 + | otherwise = toInvisibleLoc loc1 -- | Take a CtLoc and moves it to the kind level toKindLoc :: CtLoc -> CtLoc toKindLoc loc = loc { ctl_t_or_k = Just KindLevel } +toInvisibleLoc :: CtLoc -> CtLoc +toInvisibleLoc loc = updateCtLocOrigin loc toInvisibleOrigin + mkGivenLoc :: TcLevel -> SkolemInfoAnon -> TcLclEnv -> CtLoc mkGivenLoc tclvl skol_info env = CtLoc { ctl_origin = GivenOrigin skol_info diff --git a/compiler/GHC/Tc/Types/Evidence.hs b/compiler/GHC/Tc/Types/Evidence.hs index 139d46fc98..4216613c4a 100644 --- a/compiler/GHC/Tc/Types/Evidence.hs +++ b/compiler/GHC/Tc/Types/Evidence.hs @@ -230,7 +230,7 @@ mkWpEta xs wrap = foldr eta_one wrap xs mk_wp_fun_co :: Mult -> TcCoercionR -> TcCoercionR -> TcCoercionR mk_wp_fun_co mult arg_co res_co - = mkNakedFunCo1 Representational FTF_T_T (multToCo mult) arg_co res_co + = mkNakedFunCo Representational FTF_T_T (multToCo mult) arg_co res_co -- FTF_T_T: WpFun is always (->) mkWpCastR :: TcCoercionR -> HsWrapper diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs index 41b48b6e71..794ef7986b 100644 --- a/compiler/GHC/Tc/Types/Origin.hs +++ b/compiler/GHC/Tc/Types/Origin.hs @@ -1000,6 +1000,11 @@ data FixedRuntimeRepOrigin -- ^ What context requires a fixed runtime representation? } +instance Outputable FixedRuntimeRepOrigin where + ppr (FixedRuntimeRepOrigin { frr_type = ty, frr_context = cxt }) + = text "FrOrigin" <> braces (vcat [ text "frr_type:" <+> ppr ty + , text "frr_context:" <+> ppr cxt ]) + -- | The context in which a representation-polymorphism check was performed. -- -- Does not include the type on which the check was performed; see diff --git a/compiler/GHC/Tc/Utils/Concrete.hs b/compiler/GHC/Tc/Utils/Concrete.hs index a07401ec74..85f79d81cf 100644 --- a/compiler/GHC/Tc/Utils/Concrete.hs +++ b/compiler/GHC/Tc/Utils/Concrete.hs @@ -521,7 +521,8 @@ ensureConcrete :: HasDebugCallStack -> TcType -> TcM TcType ensureConcrete frr_orig ty - = do { (ty', errs) <- makeTypeConcrete conc_orig ty + = do { traceTc "ensureConcrete {" (ppr frr_orig $$ ppr ty) + ; (ty', errs) <- makeTypeConcrete conc_orig ty ; case errs of { err:errs -> do { traceTc "ensureConcrete } failure" $ diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs index 873ff2979a..7db80cfccb 100644 --- a/compiler/GHC/Tc/Utils/TcMType.hs +++ b/compiler/GHC/Tc/Utils/TcMType.hs @@ -44,7 +44,8 @@ module GHC.Tc.Utils.TcMType ( newTcEvBinds, newNoTcEvBinds, addTcEvBind, emitNewExprHole, - newCoercionHole, fillCoercionHole, isFilledCoercionHole, + newCoercionHole, newCoercionHoleO, newVanillaCoercionHole, + fillCoercionHole, isFilledCoercionHole, unpackCoercionHole, unpackCoercionHole_maybe, checkCoercionHole, @@ -103,7 +104,7 @@ module GHC.Tc.Utils.TcMType ( ------------------------------ -- Other - anyUnfilledCoercionHoles + zonkRewriterSet, zonkCtRewriterSet, zonkCtEvRewriterSet ) where import GHC.Prelude @@ -111,6 +112,7 @@ import GHC.Prelude import GHC.Driver.Session import qualified GHC.LanguageExtensions as LangExt +import {-# SOURCE #-} GHC.Tc.Utils.Unify( unifyInvisibleType ) import GHC.Tc.Types.Origin import GHC.Tc.Types.Constraint import GHC.Tc.Types.Evidence @@ -198,7 +200,7 @@ newEvVar ty = do { name <- newSysName (predTypeOccName ty) newWantedWithLoc :: CtLoc -> PredType -> TcM CtEvidence newWantedWithLoc loc pty = do dst <- case classifyPredType pty of - EqPred {} -> HoleDest <$> newCoercionHole pty + EqPred {} -> HoleDest <$> newCoercionHole loc pty _ -> EvVarDest <$> newEvVar pty return $ CtWanted { ctev_dest = dst , ctev_pred = pty @@ -223,9 +225,9 @@ newWanteds orig = mapM (newWanted orig Nothing) ---------------------------------------------- cloneWantedCtEv :: CtEvidence -> TcM CtEvidence -cloneWantedCtEv ctev@(CtWanted { ctev_pred = pty, ctev_dest = HoleDest _ }) +cloneWantedCtEv ctev@(CtWanted { ctev_pred = pty, ctev_dest = HoleDest _, ctev_loc = loc }) | isEqPrimPred pty - = do { co_hole <- newCoercionHole pty + = do { co_hole <- newCoercionHole loc pty ; return (ctev { ctev_dest = HoleDest co_hole }) } | otherwise = pprPanic "cloneWantedCtEv" (ppr pty) @@ -273,13 +275,13 @@ emitWantedEqs origin pairs -- | Emits a new equality constraint emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion emitWantedEq origin t_or_k role ty1 ty2 - = do { hole <- newCoercionHole pty - ; loc <- getCtLocM origin (Just t_or_k) + = do { hole <- newCoercionHoleO origin pty + ; loc <- getCtLocM origin (Just t_or_k) ; emitSimple $ mkNonCanonical $ - CtWanted { ctev_pred = pty - , ctev_dest = HoleDest hole - , ctev_loc = loc - , ctev_rewriters = rewriterSetFromTypes [ty1, ty2] } + CtWanted { ctev_pred = pty + , ctev_dest = HoleDest hole + , ctev_loc = loc + , ctev_rewriters = emptyRewriterSet } ; return (HoleCo hole) } where pty = mkPrimEqPredRole role ty1 ty2 @@ -290,8 +292,8 @@ emitWantedEvVar :: CtOrigin -> TcPredType -> TcM EvVar emitWantedEvVar origin ty = do { new_cv <- newEvVar ty ; loc <- getCtLocM origin Nothing - ; let ctev = CtWanted { ctev_dest = EvVarDest new_cv - , ctev_pred = ty + ; let ctev = CtWanted { ctev_pred = ty + , ctev_dest = EvVarDest new_cv , ctev_loc = loc , ctev_rewriters = emptyRewriterSet } ; emitSimple $ mkNonCanonical ctev @@ -353,12 +355,23 @@ newImplication ************************************************************************ -} -newCoercionHole :: TcPredType -> TcM CoercionHole -newCoercionHole pred_ty +newVanillaCoercionHole :: TcPredType -> TcM CoercionHole +newVanillaCoercionHole = new_coercion_hole False + +newCoercionHole :: CtLoc -> TcPredType -> TcM CoercionHole +newCoercionHole loc = newCoercionHoleO (ctLocOrigin loc) + +newCoercionHoleO :: CtOrigin -> TcPredType -> TcM CoercionHole +newCoercionHoleO (KindEqOrigin {}) = new_coercion_hole True +newCoercionHoleO _ = new_coercion_hole False + +new_coercion_hole :: Bool -> TcPredType -> TcM CoercionHole +new_coercion_hole hetero_kind pred_ty = do { co_var <- newEvVar pred_ty ; traceTc "New coercion hole:" (ppr co_var <+> dcolon <+> ppr pred_ty) ; ref <- newMutVar Nothing - ; return $ CoercionHole { ch_co_var = co_var, ch_ref = ref } } + ; return $ CoercionHole { ch_co_var = co_var, ch_ref = ref + , ch_hetero_kind = hetero_kind } } -- | Put a value in a coercion hole fillCoercionHole :: CoercionHole -> Coercion -> TcM () @@ -621,12 +634,7 @@ ensureMonoType res_ty = return () | otherwise = do { mono_ty <- newOpenFlexiTyVarTy - ; let eq_orig = TypeEqOrigin { uo_actual = res_ty - , uo_expected = mono_ty - , uo_thing = Nothing - , uo_visible = False } - - ; _co <- emitWantedEq eq_orig TypeLevel Nominal res_ty mono_ty + ; _co <- unifyInvisibleType res_ty mono_ty ; return () } promoteTcType :: TcLevel -> TcType -> TcM (TcCoercionN, TcType) @@ -652,12 +660,7 @@ promoteTcType dest_lvl ty -- where alpha and rr are fresh and from level dest_lvl = do { rr <- newMetaTyVarTyAtLevel dest_lvl runtimeRepTy ; prom_ty <- newMetaTyVarTyAtLevel dest_lvl (mkTYPEapp rr) - ; let eq_orig = TypeEqOrigin { uo_actual = ty - , uo_expected = prom_ty - , uo_thing = Nothing - , uo_visible = False } - - ; co <- emitWantedEq eq_orig TypeLevel Nominal ty prom_ty + ; co <- unifyInvisibleType ty prom_ty ; return (co, prom_ty) } {- Note [Promoting a type] @@ -2471,8 +2474,7 @@ zonkCt ct zonkCtEvidence :: CtEvidence -> TcM CtEvidence zonkCtEvidence ctev = do { pred' <- zonkTcType (ctev_pred ctev) - ; return (setCtEvPredType ctev pred') - } + ; return (setCtEvPredType ctev pred') } zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo zonkSkolemInfo (SkolemInfo u sk) = SkolemInfo u <$> zonkSkolemInfoAnon sk @@ -2788,23 +2790,43 @@ naughtyQuantification orig_ty tv escapees ************************************************************************ -} +zonkCtRewriterSet :: Ct -> TcM Ct +zonkCtRewriterSet ct + | isGiven ev = return ct + | otherwise + = case ct of + CQuantCan {} -> return ct + CEqCan eq@(EqCt { eq_ev = ev }) -> do { ev' <- zonkCtEvRewriterSet ev + ; return (CEqCan (eq { eq_ev = ev' })) } + _ -> do { ev' <- zonkCtEvRewriterSet ev + ; return (ct { cc_ev = ev' }) } + where + ev = ctEvidence ct + +zonkCtEvRewriterSet :: CtEvidence -> TcM CtEvidence +zonkCtEvRewriterSet ev@(CtGiven {}) + = return ev +zonkCtEvRewriterSet ev@(CtWanted { ctev_rewriters = rewriters }) + = do { rewriters' <- zonkRewriterSet rewriters + ; return (ev { ctev_rewriters = rewriters' }) } + -- | 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) - = nonDetStrictFoldUniqSet go (return False) set +zonkRewriterSet :: RewriterSet -> TcM RewriterSet +zonkRewriterSet (RewriterSet set) + = nonDetStrictFoldUniqSet go (return emptyRewriterSet) set -- this does not introduce non-determinism, because the only -- monadic action is to read, and the combining function is -- commutative where - go :: CoercionHole -> TcM Bool -> TcM Bool - go hole m_acc = m_acc <||> check_hole hole + go :: CoercionHole -> TcM RewriterSet -> TcM RewriterSet + go hole m_acc = unionRewriterSet <$> (check_hole hole) <*> m_acc - check_hole :: CoercionHole -> TcM Bool + check_hole :: CoercionHole -> TcM RewriterSet check_hole hole = do { m_co <- unpackCoercionHole_maybe hole ; case m_co of - Nothing -> return True -- unfilled hole + Nothing -> return (unitRewriterSet hole) Just co -> unUCHM (check_co co) } check_ty :: Type -> UnfilledCoercionHoleMonoid @@ -2818,10 +2840,10 @@ anyUnfilledCoercionHoles (RewriterSet set) , tcf_hole = \ _ -> UCHM . check_hole , tcf_tycobinder = \ _ _ _ -> () } -newtype UnfilledCoercionHoleMonoid = UCHM { unUCHM :: TcM Bool } +newtype UnfilledCoercionHoleMonoid = UCHM { unUCHM :: TcM RewriterSet } instance Semigroup UnfilledCoercionHoleMonoid where - UCHM l <> UCHM r = UCHM (l <||> r) + UCHM l <> UCHM r = UCHM (unionRewriterSet <$> l <*> r) instance Monoid UnfilledCoercionHoleMonoid where - mempty = UCHM (return False) + mempty = UCHM (return emptyRewriterSet) diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs index 1a03cd1c4b..ae25678600 100644 --- a/compiler/GHC/Tc/Utils/TcType.hs +++ b/compiler/GHC/Tc/Utils/TcType.hs @@ -205,7 +205,7 @@ module GHC.Tc.Utils.TcType ( --------------------------------- -- argument visibility - tcTyConVisibilities, isNextTyConArgVisible, isNextArgVisible + tyConVisibilities, isNextTyConArgVisible, isNextArgVisible ) where @@ -2307,8 +2307,8 @@ Reason: the back end falls over with panic "primRepHint:VoidRep"; -- | For every arg a tycon can take, the returned list says True if the argument -- is taken visibly, and False otherwise. Ends with an infinite tail of Trues to -- allow for oversaturation. -tcTyConVisibilities :: TyCon -> [Bool] -tcTyConVisibilities tc = tc_binder_viss ++ tc_return_kind_viss ++ repeat True +tyConVisibilities :: TyCon -> [Bool] +tyConVisibilities tc = tc_binder_viss ++ tc_return_kind_viss ++ repeat True where tc_binder_viss = map isVisibleTyConBinder (tyConBinders tc) tc_return_kind_viss = map isVisiblePiTyBinder (fst $ tcSplitPiTys (tyConResKind tc)) @@ -2316,13 +2316,14 @@ tcTyConVisibilities tc = tc_binder_viss ++ tc_return_kind_viss ++ repeat True -- | If the tycon is applied to the types, is the next argument visible? isNextTyConArgVisible :: TyCon -> [Type] -> Bool isNextTyConArgVisible tc tys - = tcTyConVisibilities tc `getNth` length tys + = tyConVisibilities tc `getNth` length tys -- | Should this type be applied to a visible argument? +-- E.g. (s t): is `t` a visible argument of `s`? isNextArgVisible :: TcType -> Bool isNextArgVisible ty - | Just (bndr, _) <- tcSplitPiTy_maybe ty = isVisiblePiTyBinder bndr - | otherwise = True + | Just (bndr, _) <- tcSplitPiTy_maybe (typeKind ty) = isVisiblePiTyBinder bndr + | otherwise = True -- this second case might happen if, say, we have an unzonked TauTv. -- But TauTvs can't range over types that take invisible arguments diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs index fc5728cc81..428eba5d69 100644 --- a/compiler/GHC/Tc/Utils/Unify.hs +++ b/compiler/GHC/Tc/Utils/Unify.hs @@ -20,9 +20,11 @@ module GHC.Tc.Utils.Unify ( buildImplicationFor, buildTvImplication, emitResidualTvConstraint, -- Various unifications - unifyType, unifyKind, unifyExpectedType, - uType, promoteTcType, + unifyType, unifyKind, unifyInvisibleType, unifyExpectedType, + unifyTypeAndEmit, promoteTcType, swapOverTyVars, touchabilityAndShapeTest, + UnifyEnv(..), updUEnvLoc, setUEnvRole, + uType, -------------------------------- -- Holes @@ -1145,7 +1147,7 @@ tcEqMult origin w_actual w_expected = do { -- Note that here we do not call to `submult`, so we check -- for strict equality. - ; coercion <- uType TypeLevel origin w_actual w_expected + ; coercion <- unifyTypeAndEmit TypeLevel origin w_actual w_expected ; return $ if isReflCo coercion then WpHole else WpMultCoercion coercion } @@ -1711,18 +1713,30 @@ unifyType :: Maybe TypedThing -- ^ If present, the thing that has type ty1 -- Actual and expected types -- Returns a coercion : ty1 ~ ty2 unifyType thing ty1 ty2 - = uType TypeLevel origin ty1 ty2 + = unifyTypeAndEmit TypeLevel origin ty1 ty2 where origin = TypeEqOrigin { uo_actual = ty1 , uo_expected = ty2 , uo_thing = thing , uo_visible = True } +unifyInvisibleType :: TcTauType -> TcTauType -- ty1 (actual), ty2 (expected) + -> TcM TcCoercionN -- :: ty1 ~# ty2 +-- Actual and expected types +-- Returns a coercion : ty1 ~ ty2 +unifyInvisibleType ty1 ty2 + = unifyTypeAndEmit TypeLevel origin ty1 ty2 + where + origin = TypeEqOrigin { uo_actual = ty1 + , uo_expected = ty2 + , uo_thing = Nothing + , uo_visible = False } -- This is the "invisible" bit + unifyTypeET :: TcTauType -> TcTauType -> TcM CoercionN -- Like unifyType, but swap expected and actual in error messages -- This is used when typechecking patterns unifyTypeET ty1 ty2 - = uType TypeLevel origin ty1 ty2 + = unifyTypeAndEmit TypeLevel origin ty1 ty2 where origin = TypeEqOrigin { uo_actual = ty2 -- NB swapped , uo_expected = ty1 -- NB swapped @@ -1732,13 +1746,28 @@ unifyTypeET ty1 ty2 unifyKind :: Maybe TypedThing -> TcKind -> TcKind -> TcM CoercionN unifyKind mb_thing ty1 ty2 - = uType KindLevel origin ty1 ty2 + = unifyTypeAndEmit KindLevel origin ty1 ty2 where origin = TypeEqOrigin { uo_actual = ty1 , uo_expected = ty2 , uo_thing = mb_thing , uo_visible = True } +unifyTypeAndEmit :: TypeOrKind -> CtOrigin -> TcType -> TcType -> TcM CoercionN +-- Make a ref-cell, unify, emit the collected constraints +unifyTypeAndEmit t_or_k orig ty1 ty2 + = do { ref <- newTcRef emptyBag + ; loc <- getCtLocM orig (Just t_or_k) + ; let env = UE { u_loc = loc, u_role = Nominal + , u_rewriters = emptyRewriterSet -- ToDo: check this + , u_defer = ref, u_unified = Nothing } + + -- The hard work happens here + ; co <- uType env ty1 ty2 + + ; cts <- readTcRef ref + ; unless (null cts) (emitSimples cts) + ; return co } {- %************************************************************************ @@ -1747,45 +1776,110 @@ unifyKind mb_thing ty1 ty2 %* * %************************************************************************ -uType is the heart of the unifier. +Note [The eager unifier] +~~~~~~~~~~~~~~~~~~~~~~~~ +The eager unifier, `uType`, is called by + + * The constraint generator (e.g. in GHC.Tc.Gen.Expr), + via the wrappers `unifyType`, `unifyKind` etc + + * The constraint solver (e.g. in GHC.Tc.Solver.Equality), + via `GHC.Tc.Solver.Monad.wrapUnifierTcS`. + +`uType` runs in the TcM monad, but it carries a UnifyEnv that tells it +what to do when unifying a variable or deferring a constraint. Specifically, + * it collects deferred constraints in `u_defer`, and + * it records which unification variables it has unified in `u_unified` +Then it is up to the wrappers (one for the constraint generator, one for +the constraint solver) to deal with these collected sets. + +Although `uType` runs in the TcM monad for convenience, really it could +operate just with the ability to + * write to the accumulators of deferred constraints + and unification variables in UnifyEnv. + * read and update existing unification variables + * zonk types befire unifying (`zonkTcType` in `uUnfilledVar`, and + `zonkTyCoVarKind` in `uUnfilledVar1` + * create fresh coercion holes (`newCoercionHole`) + * emit tracing info for debugging + * look at the ambient TcLevel: `getTcLevel` +A job for the future. -} +data UnifyEnv + = UE { u_role :: Role + , u_loc :: CtLoc + , u_rewriters :: RewriterSet + + -- Deferred constraints + , u_defer :: TcRef (Bag Ct) + + -- Which variables are unified; + -- if Nothing, we don't care + , u_unified :: Maybe (TcRef [TcTyVar]) + } + +setUEnvRole :: UnifyEnv -> Role -> UnifyEnv +setUEnvRole uenv role = uenv { u_role = role } + +updUEnvLoc :: UnifyEnv -> (CtLoc -> CtLoc) -> UnifyEnv +updUEnvLoc uenv@(UE { u_loc = loc }) upd = uenv { u_loc = upd loc } + +mkKindEnv :: UnifyEnv -> TcType -> TcType -> UnifyEnv +-- Modify the UnifyEnv to be right for unifing +-- the kinds of these two types +mkKindEnv env@(UE { u_loc = ctloc }) ty1 ty2 + = env { u_role = Nominal, u_loc = mkKindEqLoc ty1 ty2 ctloc } + uType, uType_defer - :: TypeOrKind - -> CtOrigin + :: UnifyEnv -> TcType -- ty1 is the *actual* type -> TcType -- ty2 is the *expected* type -> TcM CoercionN --------------- -- It is always safe to defer unification to the main constraint solver -- See Note [Deferred unification] --- ty1 is "actual" --- ty2 is "expected" -uType_defer t_or_k origin ty1 ty2 - = do { co <- emitWantedEq origin t_or_k Nominal ty1 ty2 +uType_defer (UE { u_loc = loc, u_defer = ref + , u_role = role, u_rewriters = rewriters }) + ty1 ty2 -- ty1 is "actual", ty2 is "expected" + = do { let pred_ty = mkPrimEqPredRole role ty1 ty2 + ; hole <- newCoercionHole loc pred_ty + ; let ct = mkNonCanonical $ + CtWanted { ctev_pred = pred_ty + , ctev_dest = HoleDest hole + , ctev_loc = loc + , ctev_rewriters = rewriters } + co = HoleCo hole + ; updTcRef ref (`snocBag` ct) + -- snocBag: see Note [Work-list ordering] in GHC.Tc.Solver.Equality -- Error trace only -- NB. do *not* call mkErrInfo unless tracing is on, -- because it is hugely expensive (#5631) - ; whenDOptM Opt_D_dump_tc_trace $ do - { ctxt <- getErrCtxt - ; doc <- mkErrInfo emptyTidyEnv ctxt - ; traceTc "utype_defer" (vcat [ debugPprType ty1 + ; whenDOptM Opt_D_dump_tc_trace $ + do { ctxt <- getErrCtxt + ; doc <- mkErrInfo emptyTidyEnv ctxt + ; traceTc "utype_defer" (vcat [ ppr role + , debugPprType ty1 , debugPprType ty2 - , pprCtOrigin origin , doc]) - ; traceTc "utype_defer2" (ppr co) - } + ; traceTc "utype_defer2" (ppr co) } + ; return co } + -------------- -uType t_or_k origin orig_ty1 orig_ty2 +uType env@(UE { u_role = role }) orig_ty1 orig_ty2 + | Phantom <- role + = do { kind_co <- uType (mkKindEnv env orig_ty1 orig_ty2) + (typeKind orig_ty1) (typeKind orig_ty2) + ; return (mkPhantomCo kind_co orig_ty1 orig_ty2) } + + | otherwise = do { tclvl <- getTcLevel ; traceTc "u_tys" $ vcat [ text "tclvl" <+> ppr tclvl - , sep [ ppr orig_ty1, text "~", ppr orig_ty2] - , pprCtOrigin origin] + , sep [ ppr orig_ty1, text "~" <> ppr role, ppr orig_ty2] ] ; co <- go orig_ty1 orig_ty2 ; if isReflCo co then traceTc "u_tys yields no coercion" Outputable.empty @@ -1800,12 +1894,12 @@ uType t_or_k origin orig_ty1 orig_ty2 -- recognize (t |> co) ~ (t |> co), which is nice. Previously, we -- didn't do it this way, and then the unification above was deferred. go (CastTy t1 co1) t2 - = do { co_tys <- uType t_or_k origin t1 t2 - ; return (mkCoherenceLeftCo Nominal t1 co1 co_tys) } + = do { co_tys <- uType env t1 t2 + ; return (mkCoherenceLeftCo role t1 co1 co_tys) } go t1 (CastTy t2 co2) - = do { co_tys <- uType t_or_k origin t1 t2 - ; return (mkCoherenceRightCo Nominal t2 co2 co_tys) } + = do { co_tys <- uType env t1 t2 + ; return (mkCoherenceRightCo role t2 co2 co_tys) } -- Variables; go for uUnfilledVar -- Note that we pass in *original* (before synonym expansion), @@ -1815,19 +1909,20 @@ uType t_or_k origin orig_ty1 orig_ty2 = do { lookup_res <- isFilledMetaTyVar_maybe tv1 ; case lookup_res of Just ty1 -> do { traceTc "found filled tyvar" (ppr tv1 <+> text ":->" <+> ppr ty1) - ; go ty1 ty2 } - Nothing -> uUnfilledVar origin t_or_k NotSwapped tv1 ty2 } + ; uType env ty1 orig_ty2 } + Nothing -> uUnfilledVar env NotSwapped tv1 ty2 } + go ty1 (TyVarTy tv2) = do { lookup_res <- isFilledMetaTyVar_maybe tv2 ; case lookup_res of Just ty2 -> do { traceTc "found filled tyvar" (ppr tv2 <+> text ":->" <+> ppr ty2) - ; go ty1 ty2 } - Nothing -> uUnfilledVar origin t_or_k IsSwapped tv2 ty1 } + ; uType env orig_ty1 ty2 } + Nothing -> uUnfilledVar env IsSwapped tv2 ty1 } -- See Note [Expanding synonyms during unification] go ty1@(TyConApp tc1 []) (TyConApp tc2 []) | tc1 == tc2 - = return $ mkNomReflCo ty1 + = return $ mkReflCo role ty1 -- See Note [Expanding synonyms during unification] -- @@ -1842,14 +1937,14 @@ uType t_or_k origin orig_ty1 orig_ty2 | Just ty2' <- coreView ty2 = go ty1 ty2' -- Functions (t1 -> t2) just check the two parts - -- Do not attempt (c => t); just defer go (FunTy { ft_af = af1, ft_mult = w1, ft_arg = arg1, ft_res = res1 }) (FunTy { ft_af = af2, ft_mult = w2, ft_arg = arg2, ft_res = res2 }) - | isVisibleFunArg af1, af1 == af2 - = do { co_l <- uType t_or_k origin arg1 arg2 - ; co_r <- uType t_or_k origin res1 res2 - ; co_w <- uType t_or_k origin w1 w2 - ; return $ mkNakedFunCo1 Nominal af1 co_w co_l co_r } + | isVisibleFunArg af1 -- Do not attempt (c => t); just defer + , af1 == af2 -- Important! See #21530 + = do { co_w <- uType (env { u_role = funRole role SelMult }) w1 w2 + ; co_l <- uType (env { u_role = funRole role SelArg }) arg1 arg2 + ; co_r <- uType (env { u_role = funRole role SelRes }) res1 res2 + ; return $ mkNakedFunCo role af1 co_w co_l co_r } -- Always defer if a type synonym family (type function) -- is involved. (Data families behave rigidly.) @@ -1861,41 +1956,40 @@ uType t_or_k origin orig_ty1 orig_ty2 go (TyConApp tc1 tys1) (TyConApp tc2 tys2) -- See Note [Mismatched type lists and application decomposition] | tc1 == tc2, equalLength tys1 tys2 - = assertPpr (isGenerativeTyCon tc1 Nominal) (ppr tc1) $ - do { cos <- zipWith3M (uType t_or_k) origins' tys1 tys2 - ; return $ mkTyConAppCo Nominal tc1 cos } - where - origins' = map (\is_vis -> if is_vis then origin else toInvisibleOrigin origin) - (tcTyConVisibilities tc1) + , isInjectiveTyCon tc1 role -- don't look under newtypes at Rep equality + = assertPpr (isGenerativeTyCon tc1 role) (ppr tc1) $ + do { traceTc "go-tycon" (ppr tc1 $$ ppr tys1 $$ ppr tys2 $$ ppr (take 10 (tyConRoleListX role tc1))) + ; cos <- zipWith4M u_tc_arg (tyConVisibilities tc1) -- Infinite + (tyConRoleListX role tc1) -- Infinite + tys1 tys2 + ; return $ mkTyConAppCo role tc1 cos } go (LitTy m) ty@(LitTy n) | m == n - = return $ mkNomReflCo ty + = return $ mkReflCo role ty -- See Note [Care with type applications] -- Do not decompose FunTy against App; -- it's often a type error, so leave it for the constraint solver - go (AppTy s1 t1) (AppTy s2 t2) - = go_app (isNextArgVisible s1) s1 t1 s2 t2 + go ty1@(AppTy s1 t1) ty2@(AppTy s2 t2) + = go_app (isNextArgVisible s1) ty1 s1 t1 ty2 s2 t2 - go (AppTy s1 t1) (TyConApp tc2 ts2) + go ty1@(AppTy s1 t1) ty2@(TyConApp tc2 ts2) | Just (ts2', t2') <- snocView ts2 = assert (not (tyConMustBeSaturated tc2)) $ - go_app (isNextTyConArgVisible tc2 ts2') s1 t1 (TyConApp tc2 ts2') t2' + go_app (isNextTyConArgVisible tc2 ts2') + ty1 s1 t1 ty2 (TyConApp tc2 ts2') t2' - go (TyConApp tc1 ts1) (AppTy s2 t2) + go ty1@(TyConApp tc1 ts1) ty2@(AppTy s2 t2) | Just (ts1', t1') <- snocView ts1 = assert (not (tyConMustBeSaturated tc1)) $ - go_app (isNextTyConArgVisible tc1 ts1') (TyConApp tc1 ts1') t1' s2 t2 + go_app (isNextTyConArgVisible tc1 ts1') + ty1 (TyConApp tc1 ts1') t1' ty2 s2 t2 - go (CoercionTy co1) (CoercionTy co2) - = do { let ty1 = coercionType co1 - ty2 = coercionType co2 - ; kco <- uType KindLevel - (KindEqOrigin orig_ty1 orig_ty2 origin - (Just t_or_k)) - ty1 ty2 - ; return $ mkProofIrrelCo Nominal kco co1 co2 } + go ty1@(CoercionTy co1) ty2@(CoercionTy co2) + = do { kco <- uType (mkKindEnv env ty1 ty2) + (coercionType co1) (coercionType co2) + ; return $ mkProofIrrelCo role kco co1 co2 } -- Anything else fails -- E.g. unifying for-all types, which is relative unusual @@ -1903,17 +1997,33 @@ uType t_or_k origin orig_ty1 orig_ty2 ------------------ defer ty1 ty2 -- See Note [Check for equality before deferring] - | ty1 `tcEqType` ty2 = return (mkNomReflCo ty1) - | otherwise = uType_defer t_or_k origin ty1 ty2 + | ty1 `tcEqType` ty2 = return (mkReflCo role ty1) + | otherwise = uType_defer env orig_ty1 orig_ty2 + ------------------ - go_app vis s1 t1 s2 t2 - = do { co_s <- uType t_or_k origin s1 s2 - ; let arg_origin - | vis = origin - | otherwise = toInvisibleOrigin origin - ; co_t <- uType t_or_k arg_origin t1 t2 + u_tc_arg is_vis role ty1 ty2 + = do { traceTc "u_tc_arg" (ppr role $$ ppr ty1 $$ ppr ty2) + ; uType env_arg ty1 ty2 } + where + env_arg = env { u_loc = adjustCtLoc is_vis False (u_loc env) + , u_role = role } + + ------------------ + -- For AppTy, decompose only nominal equalities + -- See Note [Decomposing AppTy equalities] in GHC.Tc.Solver.Equality + go_app vis ty1 s1 t1 ty2 s2 t2 + | Nominal <- role + = -- Unify arguments t1/t2 before function s1/s2, because + -- the former have smaller kinds, and hence simpler error messages + -- c.f. GHC.Tc.Solver.Equality.can_eq_app + -- Example: test T8603 + do { let env_arg = env { u_loc = adjustCtLoc vis False (u_loc env) } + ; co_t <- uType env_arg t1 t2 + ; co_s <- uType env s1 s2 ; return $ mkAppCo co_s co_t } + | otherwise + = defer ty1 ty2 {- Note [Check for equality before deferring] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2009,38 +2119,35 @@ back into @uTys@ if it turns out that the variable is already bound. -} ---------- -uUnfilledVar :: CtOrigin - -> TypeOrKind - -> SwapFlag - -> TcTyVar -- Tyvar 1: not necessarily a meta-tyvar - -- definitely not a /filled/ meta-tyvar - -> TcTauType -- Type 2 - -> TcM Coercion +uUnfilledVar, uUnfilledVar1 + :: UnifyEnv + -> SwapFlag + -> TcTyVar -- Tyvar 1: not necessarily a meta-tyvar + -- definitely not a /filled/ meta-tyvar + -> TcTauType -- Type 2 + -> TcM CoercionN -- "Unfilled" means that the variable is definitely not a filled-in meta tyvar -- It might be a skolem, or untouchable, or meta - -uUnfilledVar origin t_or_k swapped tv1 ty2 - = do { ty2 <- zonkTcType ty2 - -- Zonk to expose things to the - -- occurs check, and so that if ty2 - -- looks like a type variable then it - -- /is/ a type variable - ; uUnfilledVar1 origin t_or_k swapped tv1 ty2 } - ----------- -uUnfilledVar1 :: CtOrigin - -> TypeOrKind - -> SwapFlag - -> TcTyVar -- Tyvar 1: not necessarily a meta-tyvar - -- definitely not a /filled/ meta-tyvar - -> TcTauType -- Type 2, zonked - -> TcM Coercion -uUnfilledVar1 origin t_or_k swapped tv1 ty2 +uUnfilledVar env swapped tv1 ty2 + | Nominal <- u_role env + = do { ty2 <- zonkTcType ty2 -- Zonk to expose things to the occurs check, and so + -- that if ty2 looks like a type variable then it + -- /is/ a type variable + ; uUnfilledVar1 env swapped tv1 ty2 } + + | otherwise -- See Note [Do not unify representational equalities] + -- in GHC.Tc.Solver.Equality + = unSwap swapped (uType_defer env) (mkTyVarTy tv1) ty2 + +uUnfilledVar1 env -- Precondition: u_role==Nominal + swapped + tv1 + ty2 -- ty2 is zonked | Just tv2 <- getTyVar_maybe ty2 = go tv2 | otherwise - = uUnfilledVar2 origin t_or_k swapped tv1 ty2 + = uUnfilledVar2 env swapped tv1 ty2 where -- 'go' handles the case where both are @@ -2056,21 +2163,19 @@ uUnfilledVar1 origin t_or_k swapped tv1 ty2 -- not have happened yet, and it's an invariant of -- uUnfilledTyVar2 that ty2 is fully zonked -- Omitting this caused #16902 - ; uUnfilledVar2 origin t_or_k (flipSwap swapped) - tv2 (mkTyVarTy tv1) } + ; uUnfilledVar2 env (flipSwap swapped) tv2 (mkTyVarTy tv1) } | otherwise - = uUnfilledVar2 origin t_or_k swapped tv1 ty2 + = uUnfilledVar2 env swapped tv1 ty2 ---------- -uUnfilledVar2 :: CtOrigin - -> TypeOrKind +uUnfilledVar2 :: UnifyEnv -- Precondition: u_role==Nominal -> SwapFlag -> TcTyVar -- Tyvar 1: not necessarily a meta-tyvar -- definitely not a /filled/ meta-tyvar -> TcTauType -- Type 2, zonked - -> TcM Coercion -uUnfilledVar2 origin t_or_k swapped tv1 ty2 + -> TcM CoercionN +uUnfilledVar2 env@(UE { u_defer = def_eq_ref }) swapped tv1 ty2 = do { cur_lvl <- getTcLevel -- See Note [Unification preconditions], (UNTOUCHABLE) wrinkles -- Here we don't know about given equalities here; so we treat @@ -2079,7 +2184,10 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2 && simpleUnifyCheck False tv1 ty2) then not_ok_so_defer else - do { co_k <- uType KindLevel kind_origin (typeKind ty2) (tyVarKind tv1) + do { def_eqs <- readTcRef def_eq_ref -- Capture current state of def_eqs + + -- Attempt to unify kinds + ; co_k <- uType (mkKindEnv env ty1 ty2) (typeKind ty2) (tyVarKind tv1) ; traceTc "uUnfilledVar2 ok" $ vcat [ ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1) , ppr ty2 <+> dcolon <+> ppr (typeKind ty2) @@ -2090,17 +2198,22 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2 -- NB: tv1 should still be unfilled, despite the kind unification -- because tv1 is not free in ty2' (or, hence, in its kind) then do { writeMetaTyVar tv1 ty2 - ; return (mkNomReflCo ty2) } - - else defer -- This cannot be solved now. See GHC.Tc.Solver.Canonical - -- Note [Equalities with incompatible kinds] for how - -- this will be dealt with in the solver + ; case u_unified env of + Nothing -> return () + Just uref -> updTcRef uref (tv1 :) + ; return (mkNomReflCo ty2) } -- Unification is always Nominal + + else -- The kinds don't match yet, so give up defer instead. + do { writeTcRef def_eq_ref def_eqs + -- Since we are discarding co_k, also discard any constraints + -- emitted by kind unification; they are just useless clutter. + -- Do this dicarding by simply restoring the previous state + -- of def_eqs; a bit imperative/yukky but works fine. + ; defer } }} where ty1 = mkTyVarTy tv1 - kind_origin = KindEqOrigin ty1 ty2 origin (Just t_or_k) - - defer = unSwap swapped (uType_defer t_or_k origin) ty1 ty2 + defer = unSwap swapped (uType_defer env) ty1 ty2 not_ok_so_defer = do { traceTc "uUnfilledVar2 not ok" (ppr tv1 $$ ppr ty2) @@ -2219,18 +2332,10 @@ There are five reasons not to unify: 5. (COERCION-HOLE) Confusing coercion holes Suppose our equality is (alpha :: k) ~ (Int |> {co}) - where co :: Type ~ k is an unsolved wanted. Note that this - equality is homogeneous; both sides have kind k. Unifying here - is sensible, but it can lead to very confusing error messages. - It's very much like a Wanted rewriting a Wanted. Even worse, - unifying a variable essentially turns an equality into a Given, - and so we could not use the tracking mechanism in - Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint. - We thus simply do not unify in this case. - - This is expanded as Wrinkle (2) in Note [Equalities with incompatible kinds] - in GHC.Tc.Solver.Equality - + where co :: Type ~ k is an unsolved wanted. Note that this equality + is homogeneous; both sides have kind k. We refrain from unifying here, because + of the coercion hole in the RHS -- see Wrinkle (EIK2) in + Note [Equalities with incompatible kinds] in GHC.Solver.Equality. Needless to say, all there are wrinkles: @@ -2500,7 +2605,7 @@ matchExpectedFunKind hs_ty n k = go n k go n (FunTy { ft_af = af, ft_mult = w, ft_arg = arg, ft_res = res }) | isVisibleFunArg af = do { co <- go (n-1) res - ; return (mkNakedFunCo1 Nominal af (mkNomReflCo w) (mkNomReflCo arg) co) } + ; return (mkNakedFunCo Nominal af (mkNomReflCo w) (mkNomReflCo arg) co) } go n other = defer n other @@ -2514,7 +2619,7 @@ matchExpectedFunKind hs_ty n k = go n k , uo_thing = Just hs_ty , uo_visible = True } - ; uType KindLevel origin k new_fun } + ; unifyTypeAndEmit KindLevel origin k new_fun } {- ********************************************************************* * * @@ -2523,40 +2628,6 @@ matchExpectedFunKind hs_ty n k = go n k * * ********************************************************************* -} -{- Commented out because I think we can just use the simple, - efficient simpleUnifyCheck instead; we can always defer. - -uTypeCheckTouchableTyVarEq :: TcTyVar -> TcType -> TcM (PuResult () TcType) --- The check may expand type synonyms to avoid an occurs check, --- so we must use the return type --- --- Precondition: rhs is fully zonked -uTypeCheckTouchableTyVarEq lhs_tv rhs - | simpleUnifyCheck False lhs_tv rhs -- Do a fast-path check - -- False <=> See Note [Prevent unification with type families] - = return (pure rhs) - - | otherwise - = do { traceTc "uTypeCheckTouchableTyVarEq {" (pprTyVar lhs_tv $$ ppr rhs) - ; check_result <- checkTyEqRhs flags rhs :: TcM (PuResult () Reduction) - ; traceTc "uTypeCheckTouchableTyVarEq }" (ppr check_result) - ; case check_result of - PuFail reason -> return (PuFail reason) - PuOK redn _ -> assertPpr (isReflCo (reductionCoercion redn)) - (ppr lhs_tv $$ ppr rhs $$ ppr redn) $ - return (pure (reductionReducedType redn)) } - where - flags | MetaTv { mtv_info = tv_info, mtv_tclvl = tv_lvl } <- tcTyVarDetails lhs_tv - = TEF { tef_foralls = isRuntimeUnkSkol lhs_tv - , tef_fam_app = TEFA_Fail - , tef_unifying = Unifying tv_info tv_lvl LC_None - , tef_lhs = TyVarLHS lhs_tv - , tef_occurs = cteInsolubleOccurs } - | otherwise - = pprPanic "uTypeCheckTouchableTyVarEq" (ppr lhs_tv) - -- TEFA_Fail: See Note [Prevent unification with type families] --} - simpleUnifyCheck :: Bool -> TcTyVar -> TcType -> Bool -- A fast check: True <=> unification is OK -- If it says 'False' then unification might still be OK, but @@ -2690,22 +2761,22 @@ reductionCoercion is Refl. See `canEqCanLHSFinish_no_unification`. -} data PuResult a b = PuFail CheckTyEqResult - | PuOK b (Bag a) + | PuOK (Bag a) b instance Functor (PuResult a) where fmap _ (PuFail prob) = PuFail prob - fmap f (PuOK x cts) = PuOK (f x) cts + fmap f (PuOK cts x) = PuOK cts (f x) instance Applicative (PuResult a) where - pure x = PuOK x emptyBag + pure x = PuOK emptyBag x PuFail p1 <*> PuFail p2 = PuFail (p1 S.<> p2) PuFail p1 <*> PuOK {} = PuFail p1 PuOK {} <*> PuFail p2 = PuFail p2 - PuOK f c1 <*> PuOK x c2 = PuOK (f x) (c1 `unionBags` c2) + PuOK c1 f <*> PuOK c2 x = PuOK (c1 `unionBags` c2) (f x) instance (Outputable a, Outputable b) => Outputable (PuResult a b) where ppr (PuFail prob) = text "PuFail" <+> (ppr prob) - ppr (PuOK x cts) = text "PuOK" <> braces + ppr (PuOK cts x) = text "PuOK" <> braces (vcat [ text "redn:" <+> ppr x , text "cts:" <+> ppr cts ]) @@ -2715,7 +2786,7 @@ pprPur (PuFail prob) = text "PuFail:" <> ppr prob pprPur (PuOK {}) = text "PuOK" okCheckRefl :: TcType -> TcM (PuResult a Reduction) -okCheckRefl ty = return (PuOK (mkReflRedn Nominal ty) emptyBag) +okCheckRefl ty = return (PuOK emptyBag (mkReflRedn Nominal ty)) failCheckWith :: CheckTyEqResult -> TcM (PuResult a b) failCheckWith p = return (PuFail p) @@ -2851,15 +2922,14 @@ checkTyEqRhs flags ty checkCo :: TyEqFlags a -> Coercion -> TcM (PuResult a Coercion) -- See Note [checkCo] checkCo (TEF { tef_lhs = TyFamLHS {} }) co - = return (PuOK co emptyBag) + = return (pure co) checkCo (TEF { tef_lhs = TyVarLHS lhs_tv , tef_unifying = unifying , tef_occurs = occ_prob }) co -- Check for coercion holes, if unifying -- See (COERCION-HOLE) in Note [Unification preconditions] - | Unifying {} <- unifying - , hasCoercionHoleCo co + | hasCoercionHoleCo co = failCheckWith (cteProblem cteCoercionHole) -- Occurs check (can promote) @@ -2874,7 +2944,7 @@ checkCo (TEF { tef_lhs = TyVarLHS lhs_tv = failCheckWith (cteProblem occ_prob) | otherwise - = return (PuOK co emptyBag) + = return (pure co) {- Note [checkCo] ~~~~~~~~~~~~~~~~~ @@ -3058,7 +3128,7 @@ checkFamApp flags@(TEF { tef_unifying = unifying, tef_occurs = occ_prob TEFA_Break breaker -- Recurse; and break if there is a problem -> do { tys_res <- mapCheck (checkTyEqRhs arg_flags) tys ; case tys_res of - PuOK redns cts -> return (PuOK (mkTyConAppRedn Nominal tc redns) cts) + PuOK cts redns -> return (PuOK cts (mkTyConAppRedn Nominal tc redns)) PuFail {} -> breaker fam_app } where arg_flags = famAppArgFlags flags @@ -3228,4 +3298,3 @@ checkTopShape info xi _ -> False CycleBreakerTv -> False -- We never unify these _ -> True - diff --git a/compiler/GHC/Tc/Utils/Unify.hs-boot b/compiler/GHC/Tc/Utils/Unify.hs-boot index 0d82ea613e..9b75cea113 100644 --- a/compiler/GHC/Tc/Utils/Unify.hs-boot +++ b/compiler/GHC/Tc/Utils/Unify.hs-boot @@ -9,8 +9,9 @@ import GHC.Tc.Types.Origin ( CtOrigin, TypedThing ) -- This boot file exists only to tie the knot between --- GHC.Tc.Utils.Unify and GHC.Tc.Utils.Instantiate +-- GHC.Tc.Utils.Unify and GHC.Tc.Utils.Instantiate/GHC.Tc.Utils.TcMType -unifyType :: Maybe TypedThing -> TcTauType -> TcTauType -> TcM TcCoercion +unifyType :: Maybe TypedThing -> TcTauType -> TcTauType -> TcM TcCoercion +unifyInvisibleType :: TcTauType -> TcTauType -> TcM TcCoercion tcSubMult :: CtOrigin -> Mult -> Mult -> TcM HsWrapper |