diff options
Diffstat (limited to 'compiler/GHC/Tc/Solver')
| -rw-r--r-- | compiler/GHC/Tc/Solver/Canonical.hs | 709 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver/InertSet.hs | 183 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver/Interact.hs | 530 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver/Monad.hs | 696 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver/Rewrite.hs | 195 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver/Types.hs | 108 |
6 files changed, 968 insertions, 1453 deletions
diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs index 1643a0ef46..f38c5de866 100644 --- a/compiler/GHC/Tc/Solver/Canonical.hs +++ b/compiler/GHC/Tc/Solver/Canonical.hs @@ -4,7 +4,7 @@ module GHC.Tc.Solver.Canonical( canonicalize, - unifyDerived, + unifyWanted, makeSuperClasses, StopOrContinue(..), stopWith, continueWith, andWhenContinue, solveCallStack -- For GHC.Tc.Solver @@ -59,8 +59,10 @@ import Data.Maybe ( isJust, isNothing ) import Data.List ( zip4 ) import GHC.Types.Basic +import qualified Data.Semigroup as S import Data.Bifunctor ( bimap ) import Data.Foldable ( traverse_ ) +import GHC.Tc.Utils.Monad (setTcLevel) {- ************************************************************************ @@ -162,7 +164,7 @@ canClassNC ev cls tys ; emitWork sc_cts ; canClass ev cls tys False fds } - | isWanted ev + | CtWanted { ctev_rewriters = rewriters } <- ev , Just ip_name <- isCallStackPred cls tys , isPushCallStackOrigin orig -- If we're given a CallStack constraint that arose from a function @@ -176,8 +178,9 @@ canClassNC ev cls tys -- We change the origin to IPOccOrigin so -- this rule does not fire again. -- See Note [Overview of implicit CallStacks] + -- in GHC.Tc.Types.Evidence - ; new_ev <- newWantedEvVarNC new_loc pred + ; new_ev <- newWantedEvVarNC new_loc rewriters pred -- Then we solve the wanted by pushing the call-site -- onto the newly emitted CallStack @@ -220,15 +223,14 @@ canClass :: CtEvidence canClass ev cls tys pend_sc fds = -- all classes do *nominal* matching assertPpr (ctEvRole ev == Nominal) (ppr ev $$ ppr cls $$ ppr tys) $ - do { redns@(Reductions _ xis) <- rewriteArgsNom ev cls_tc 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 , cc_fundeps = fds } - ; mb <- rewriteEvidence ev redn - + ; mb <- rewriteEvidence rewriters ev redn ; traceTcS "canClass" (vcat [ ppr ev , ppr xi, ppr mb ]) ; return (fmap mk_ct mb) } @@ -245,15 +247,14 @@ We need to add superclass constraints for two reasons: We get a Wanted (Eq a), which can only be solved from the superclass of the Given (Ord a). -* For wanteds [W], and deriveds [WD], [D], they may give useful +* For wanteds [W], they may give useful functional dependencies. E.g. class C a b | a -> b where ... class C a b => D a b where ... Now a [W] constraint (D Int beta) has (C Int beta) as a superclass and that might tell us about beta, via C's fundeps. We can get this - by generating a [D] (C Int beta) constraint. It's derived because - we don't actually have to cough up any evidence for it; it's only there - to generate fundep equalities. + by generating a [W] (C Int beta) constraint. We won't use the evidence, + but it may lead to unification. See Note [Why adding superclasses can help]. @@ -303,7 +304,7 @@ So here's the plan: GHC.Tc.Solver.simpl_loop and solveWanteds. This may succeed in generating (a finite number of) extra Givens, - and extra Deriveds. Both may help the proof. + and extra Wanteds. Both may help the proof. 3a An important wrinkle: only expand Givens from the current level. Two reasons: @@ -397,7 +398,7 @@ Examples of how adding superclasses can help: Suppose we want to solve [G] C a b [W] C a beta - Then adding [D] beta~b will let us solve it. + Then adding [W] beta~b will let us solve it. -- Example 2 (similar but using a type-equality superclass) class (F a ~ b) => C a b @@ -406,8 +407,8 @@ Examples of how adding superclasses can help: [W] C a beta Follow the superclass rules to add [G] F a ~ b - [D] F a ~ beta - Now we get [D] beta ~ b, and can solve that. + [W] F a ~ beta + Now we get [W] beta ~ b, and can solve that. -- Example (tcfail138) class L a b | a -> b @@ -422,9 +423,9 @@ Examples of how adding superclasses can help: [W] G (Maybe a) Use the instance decl to get [W] C a beta - Generate its derived superclass - [D] L a beta. Now using fundeps, combine with [G] L a b to get - [D] beta ~ b + Generate its superclass + [W] L a beta. Now using fundeps, combine with [G] L a b to get + [W] beta ~ b which is what we want. Note [Danger of adding superclasses during solving] @@ -441,8 +442,8 @@ Assume the generated wanted constraint is: If we were to be adding the superclasses during simplification we'd get: [W] RealOf e ~ e [W] Normed e - [D] RealOf e ~ fuv - [D] Num fuv + [W] RealOf e ~ fuv + [W] Num fuv ==> e := fuv, Num fuv, Normed fuv, RealOf fuv ~ fuv @@ -451,9 +452,6 @@ superclass of (Normed fuv) again we'd loop. By adding superclasses definitely only once, during canonicalisation, this situation can't happen. -Mind you, now that Wanteds cannot rewrite Derived, I think this particular -situation can't happen. - Note [Nested quantified constraint superclasses] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider (typecheck/should_compile/T17202) @@ -616,18 +614,19 @@ mk_strict_superclasses rec_clss (CtGiven { ctev_evar = evar, ctev_loc = loc }) mk_strict_superclasses rec_clss ev tvs theta cls tys | all noFreeVarsOfType tys - = return [] -- Wanteds with no variables yield no deriveds. + = return [] -- Wanteds with no variables yield no superclass constraints. -- See Note [Improvement from Ground Wanteds] - | otherwise -- Wanted/Derived case, just add Derived superclasses + | otherwise -- Wanted case, just add Wanted superclasses -- that can lead to improvement. = assertPpr (null tvs && null theta) (ppr tvs $$ ppr theta) $ - concatMapM do_one_derived (immSuperClasses cls tys) + concatMapM do_one (immSuperClasses cls tys) where - loc = ctEvLoc ev + loc = ctEvLoc ev `updateCtLocOrigin` WantedSuperclassOrigin (ctEvPred ev) - do_one_derived sc_pred - = do { sc_ev <- newDerivedNC loc sc_pred + do_one sc_pred + = do { traceTcS "mk_strict_superclasses Wanted" (ppr (mkClassPred cls tys) $$ ppr sc_pred) + ; sc_ev <- newWantedNC loc (ctEvRewriters ev) sc_pred ; mk_superclasses rec_clss sc_ev [] [] sc_pred } {- Note [Improvement from Ground Wanteds] @@ -635,8 +634,8 @@ mk_strict_superclasses rec_clss ev tvs theta cls tys Suppose class C b a => D a b and consider [W] D Int Bool -Is there any point in emitting [D] C Bool Int? No! The only point of -emitting superclass constraints for W/D constraints is to get +Is there any point in emitting [W] C Bool Int? No! The only point of +emitting superclass constraints for W constraints is to get improvement, extra unifications that result from functional dependencies. See Note [Why adding superclasses can help] above. @@ -734,8 +733,8 @@ canIrred :: CtEvidence -> TcS (StopOrContinue Ct) canIrred ev = do { let pred = ctEvPred ev ; traceTcS "can_pred" (text "IrredPred = " <+> ppr pred) - ; redn <- rewrite ev pred - ; rewriteEvidence ev redn `andWhenContinue` \ new_ev -> + ; (redn, rewriters) <- rewrite ev pred + ; rewriteEvidence rewriters ev redn `andWhenContinue` \ new_ev -> do { -- Re-classify, in case rewriting has improved its shape -- Code is like the canNC, except @@ -856,8 +855,8 @@ canForAll :: CtEvidence -> Bool -> TcS (StopOrContinue Ct) canForAll ev pend_sc = do { -- First rewrite it to apply the current substitution let pred = ctEvPred ev - ; redn <- rewrite ev pred - ; rewriteEvidence ev redn `andWhenContinue` \ new_ev -> + ; (redn, rewriters) <- rewrite ev pred + ; rewriteEvidence rewriters ev redn `andWhenContinue` \ new_ev -> do { -- Now decompose into its pieces and solve it -- (It takes a lot less code to rewrite before decomposing.) @@ -869,8 +868,8 @@ canForAll ev pend_sc solveForAll :: CtEvidence -> [TyVar] -> TcThetaType -> PredType -> Bool -> TcS (StopOrContinue Ct) -solveForAll ev tvs theta pred pend_sc - | CtWanted { ctev_dest = dest } <- ev +solveForAll ev@(CtWanted { ctev_dest = dest, ctev_rewriters = rewriters, ctev_loc = loc }) + tvs theta pred _pend_sc = -- See Note [Solving a Wanted forall-constraint] setLclEnv (ctLocEnv loc) $ -- This setLclEnv is important: the emitImplicationTcS uses that @@ -884,7 +883,7 @@ solveForAll ev tvs theta pred pend_sc ; (lvl, (w_id, wanteds)) <- pushLevelNoWorkList (ppr skol_info) $ - do { wanted_ev <- newWantedEvVarNC loc $ + do { wanted_ev <- newWantedEvVarNC loc rewriters $ substTy subst pred ; return ( ctEvEvId wanted_ev , unitBag (mkNonCanonical wanted_ev)) } @@ -898,15 +897,11 @@ solveForAll ev tvs theta pred pend_sc ; stopWith ev "Wanted forall-constraint" } - | isGiven ev -- See Note [Solving a Given forall-constraint] + -- See Note [Solving a Given forall-constraint] +solveForAll ev@(CtGiven {}) tvs _theta pred pend_sc = do { addInertForAll qci ; stopWith ev "Given forall-constraint" } - - | otherwise - = do { traceTcS "discarding derived forall-constraint" (ppr ev) - ; stopWith ev "Derived forall-constraint" } where - loc = ctEvLoc ev qci = QCI { qci_ev = ev, qci_tvs = tvs , qci_pred = pred, qci_pend_sc = pend_sc } @@ -976,6 +971,44 @@ here are some examples: ==> the second constraint can be decomposed again; 'RuntimeRep' and '[]' are concrete, so we get C: Concrete# Rep, C: Concrete# rr +Note [Solving Concrete constraints requires simplifyArgsWorker] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We have + [W] co :: Concrete# [LiftedRep, IntRep] +and wish to canonicalise it so that we can solve it. Of course, that's really + [W] co :: Concrete# ((:) @RuntimeRep LiftedRep ((:) @RuntimeRep IntRep ('[] @RuntimeRep))) + +We can decompose to + [W] co1 :: Concrete# RuntimeRep + [W] co2 :: Concrete# LiftedRep + [W] co3 :: Concrete# ((:) @RuntimeRep IntRep ('[] @RuntimeRep)) + +Recall (Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete) that the evidence for +a Concrete# ty constraint is a coercion of type ty ~# alpha, where we require a concrete +type (one that responds True to GHC.Core.Type.isConcrete) to fill in alpha when solving +the constraint. Accordingly, when we create these new Concrete# constraints, we create +new metavariables alpha1 :: Type, alpha2 :: RuntimeRep, alpha3 :: [RuntimeRep], with: + + co1 :: RuntimeRep ~# alpha1 + co2 :: LiftedRep ~# alpha2 + co3 :: '[IntRep] ~# alpha3 + +and we already have + + co :: [LiftedRep, IntRep] ~# alpha0 + +We are now solving co. What do we fill in alpha0 with? The naive answer is to say + + alpha0 := (:) alpha1 alpha2 alpha3 + +but this would be ill-kinded! The first problem is that `(:) alpha1` expects its next +argument to have kind alpha1. (The next argument -- alpha3 -- is problematic, too.) The +second problem is that alpha0 :: [RuntimeRep], but the right-hand side above has kind +[alpha1]. Happily, we have a solution close to hand: simplifyArgsWorker, which deals +with precisely this scenario, of replacing all the arguments to a function (in this case, (:)), +with new arguments but making sure the kinds line up. All we have to do is bundle the information +we have in a form simplifyArgsWorker likes, and then do the reverse from its result. + -} -- | Canonicalise a 'Concrete#' constraint. @@ -1026,13 +1059,29 @@ canDecomposableConcretePrim :: CtEvidence canDecomposableConcretePrim ev f_tc args = do { traceTcS "canDecomposableConcretePrim" $ vcat [text "args =" <+> ppr args, text "ev =" <+> ppr ev] - ; arg_cos <- mapM (emit_new_concretePrim_wanted (ctEvLoc ev)) args - ; case ev of - CtWanted { ctev_dest = dest } - -> setWantedEvTerm dest (evCoercion $ mkTyConAppCo Nominal f_tc arg_cos) - _ -> pprPanic "canDecomposableConcretePrim: non-Wanted" $ - vcat [ text "ev =" <+> ppr ev - , text "args =" <+> ppr args ] + ; let ev_lvl + | CtWanted { ctev_dest = HoleDest hole } <- ev + , (_, _, _, conc_rhs_ty, Nominal) <- coVarKindsTypesRole (coHoleCoVar hole) + , Just conc_rhs_tv <- getTyVar_maybe conc_rhs_ty + , Just lvl <- metaTyVarTcLevel_maybe conc_rhs_tv + = lvl + + | otherwise + = pprPanic "canDecomposableConcretePrim" (ppr ev) + + ; (arg_cos, rhs_args) + <- mapAndUnzipM (emit_new_concretePrim_wanted ev_lvl (ctEvLoc ev)) args + + -- See Note [Solving Concrete constraints requires simplifyArgsWorker] + ; let (tc_binders, tc_res_kind) = splitPiTys (tyConKind f_tc) + fvs_args = tyCoVarsOfTypes rhs_args + ArgsReductions reductions final_co + = simplifyArgsWorker tc_binders tc_res_kind fvs_args + (repeat Nominal) (zipWith mkReduction arg_cos rhs_args) + Reduction concrete_co uncasted_concrete_rhs = mkTyConAppRedn Nominal f_tc reductions + concrete_rhs = uncasted_concrete_rhs `mkCastTyMCo` mkSymMCo final_co + + ; solveConcretePrimWanted ev concrete_co concrete_rhs ; stopWith ev "Decomposed Concrete#" } -- | Canonicalise a non-decomposable 'Concrete#' constraint. @@ -1050,12 +1099,44 @@ canNonDecomposableConcretePrim ev ty ; continueWith new_ct } -- | Create a new 'Concrete#' Wanted constraint and immediately add it --- to the work list. -emit_new_concretePrim_wanted :: CtLoc -> Type -> TcS Coercion -emit_new_concretePrim_wanted loc ty - = do { (hole, wanted) <- wrapTcS $ newConcretePrimWanted loc ty +-- to the work list. Returns the evidence (a coercion hole) used for the +-- constraint, and the right-hand type (a metavariable) of that coercion +emit_new_concretePrim_wanted :: TcLevel -> CtLoc -> Type -> TcS (Coercion, TcType) +emit_new_concretePrim_wanted ev_lvl loc ty + = do { (hole, rhs_ty, wanted) <- wrapTcS $ setTcLevel ev_lvl $ newConcretePrimWanted loc ty ; emitWorkNC [wanted] - ; return $ mkHoleCo hole } + ; return (mkHoleCo hole, rhs_ty) } + +-- | Solve a Wanted 'Concrete#' constraint. +-- +-- Recall that, when we create a Wanted constraint of the form @Concrete# ty@, +-- we create a metavariable @concrete_tau@ and a coercion hole of type +-- @ty ~# concrete_tau@. +-- +-- When we want to solve this constraint, because we have found that +-- @ty@ is indeed equal to a concrete type @rhs@, we thus need to do +-- two things: +-- +-- 1. fill the metavariable @concrete_tau := rhs@, +-- 2. fill the coercion hole with the evidence for the equality @ty ~# rhs@. +solveConcretePrimWanted :: HasDebugCallStack + => CtEvidence -- ^ always a [W] Concrete# ty + -> Coercion -- ^ @co :: ty ~ rhs@ + -> TcType -- ^ @rhs@, which must be concrete + -> TcS () +solveConcretePrimWanted (CtWanted { ctev_dest = dest@(HoleDest hole) }) co rhs + = do { let Pair _ty concrete_tau = coVarTypes $ coHoleCoVar hole + tau_tv = getTyVar "solveConcretePrimWanted" concrete_tau + ; unifyTyVar tau_tv rhs + ; setWantedEq dest co } + +solveConcretePrimWanted ev co rhs + = pprPanic "solveConcretePrimWanted: no coercion hole to fill" $ + vcat [ text "ev =" <+> ppr ev <> semi <+> text "dest =" <+> case ev of + CtWanted { ctev_dest = EvVarDest var } -> text "var" <+> ppr var + _ -> text "XXX NOT EVEN A WANTED XXX" + , text "co =" <+> ppr co + , text "rhs =" <+> ppr rhs ] {- ********************************************************************** * * @@ -1220,9 +1301,9 @@ can_eq_nc' True _rdr_env _envs ev NomEq ty1 _ ty2 _ -- No similarity in type structure detected. Rewrite and try again. can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2 - = do { redn1@(Reduction _ xi1) <- rewrite ev ps_ty1 - ; redn2@(Reduction _ xi2) <- rewrite ev ps_ty2 - ; new_ev <- rewriteEqEvidence ev NotSwapped redn1 redn2 + = do { (redn1@(Reduction _ xi1), rewriters1) <- rewrite ev ps_ty1 + ; (redn2@(Reduction _ xi2), rewriters2) <- rewrite ev ps_ty2 + ; new_ev <- rewriteEqEvidence (rewriters1 S.<> rewriters2) ev NotSwapped redn1 redn2 ; can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 } ---------------------------- @@ -1340,7 +1421,7 @@ can_eq_nc_forall :: CtEvidence -> EqRel -- so we must proceed one binder at a time (#13879) can_eq_nc_forall ev eq_rel s1 s2 - | CtWanted { ctev_loc = loc, ctev_dest = orig_dest } <- ev + | CtWanted { ctev_loc = loc, ctev_dest = orig_dest, ctev_rewriters = rewriters } <- ev = do { let free_tvs = tyCoVarsOfTypes [s1,s2] (bndrs1, phi1) = tcSplitForAllTyVarBinders s1 (bndrs2, phi2) = tcSplitForAllTyVarBinders s2 @@ -1364,7 +1445,7 @@ can_eq_nc_forall ev eq_rel s1 s2 -> TcS (TcCoercion, Cts) go (skol_tv:skol_tvs) subst (bndr2:bndrs2) = do { let tv2 = binderVar bndr2 - ; (kind_co, wanteds1) <- unify loc Nominal (tyVarKind skol_tv) + ; (kind_co, wanteds1) <- unify loc rewriters Nominal (tyVarKind skol_tv) (substTy subst (tyVarKind tv2)) ; let subst' = extendTvSubstAndInScope subst tv2 (mkCastTy (mkTyVarTy skol_tv) kind_co) @@ -1376,8 +1457,8 @@ can_eq_nc_forall ev eq_rel s1 s2 -- Done: unify phi1 ~ phi2 go [] subst bndrs2 - = assert (null bndrs2 ) - unify loc (eqRelRole eq_rel) phi1' (substTyUnchecked subst phi2) + = assert (null bndrs2) $ + unify loc rewriters (eqRelRole eq_rel) phi1' (substTyUnchecked subst phi2) go _ _ _ = panic "cna_eq_nc_forall" -- case (s:ss) [] @@ -1396,14 +1477,14 @@ can_eq_nc_forall ev eq_rel s1 s2 ; stopWith ev "Discard given polytype equality" } where - unify :: CtLoc -> Role -> TcType -> TcType -> TcS (TcCoercion, Cts) + unify :: CtLoc -> RewriterSet -> Role -> TcType -> TcType -> TcS (TcCoercion, Cts) -- This version returns the wanted constraint rather -- than putting it in the work list - unify loc role ty1 ty2 + unify loc rewriters role ty1 ty2 | ty1 `tcEqType` ty2 = return (mkTcReflCo role ty1, emptyBag) | otherwise - = do { (wanted, co) <- newWantedEq loc role ty1 ty2 + = do { (wanted, co) <- newWantedEq loc rewriters role ty1 ty2 ; return (co, unitBag (mkNonCanonical wanted)) } --------------------------------- @@ -1641,7 +1722,7 @@ can_eq_newtype_nc ev swapped ty1 ((gres, co1), ty1') ty2 ps_ty2 ; let redn1 = mkReduction co1 ty1' - ; new_ev <- rewriteEqEvidence ev swapped + ; new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped redn1 (mkReflRedn Representational ps_ty2) ; can_eq_nc False new_ev ReprEq ty1' ty1' ty2 ps_ty2 } @@ -1661,16 +1742,12 @@ can_eq_app :: CtEvidence -- :: s1 t1 ~N s2 t2 -- to an irreducible constraint; see typecheck/should_compile/T10494 -- See Note [Decomposing AppTy at representational role] can_eq_app ev s1 t1 s2 t2 - | CtDerived {} <- ev - = do { unifyDeriveds loc [Nominal, Nominal] [s1, t1] [s2, t2] - ; stopWith ev "Decomposed [D] AppTy" } - - | CtWanted { ctev_dest = dest } <- ev - = do { co_s <- unifyWanted loc Nominal s1 s2 + | CtWanted { ctev_dest = dest, ctev_rewriters = rewriters } <- ev + = do { co_s <- unifyWanted rewriters loc Nominal s1 s2 ; let arg_loc | isNextArgVisible s1 = loc | otherwise = updateCtLocOrigin loc toInvisibleOrigin - ; co_t <- unifyWanted arg_loc Nominal t1 t2 + ; co_t <- unifyWanted rewriters arg_loc Nominal t1 t2 ; let co = mkAppCo co_s co_t ; setWantedEq dest co ; stopWith ev "Decomposed [W] AppTy" } @@ -1718,7 +1795,7 @@ canEqCast rewritten ev eq_rel swapped ty1 co1 ty2 ps_ty2 = do { traceTcS "Decomposing cast" (vcat [ ppr ev , ppr ty1 <+> text "|>" <+> ppr co1 , ppr ps_ty2 ]) - ; new_ev <- rewriteEqEvidence ev swapped + ; new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped (mkGReflLeftRedn role ty1 co1) (mkReflRedn role ps_ty2) ; can_eq_nc rewritten new_ev eq_rel ty1 ty1 ty2 ps_ty2 } @@ -1827,18 +1904,13 @@ So, in broad strokes, we want this rule: at role X. Pursuing the details requires exploring three axes: -* Flavour: Given vs. Derived vs. Wanted +* Flavour: Given vs. Wanted * Role: Nominal vs. Representational * TyCon species: datatype vs. newtype vs. data family vs. type family vs. type variable (A type variable isn't a TyCon, of course, but it's convenient to put the AppTy case in the same table.) -Right away, we can say that Derived behaves just as Wanted for the purposes -of decomposition. The difference between Derived and Wanted is the handling of -evidence. Since decomposition in these cases isn't a matter of soundness but of -guessing, we want the same behaviour regardless of evidence. - Here is a table (discussion following) detailing where decomposition of (T s1 ... sn) ~r (T t1 .. tn) is allowed. The first four lines (Data types ... type family) refer @@ -1865,7 +1937,7 @@ AppTy NO{4} NO{4} can_eq_nc' {1}: Type families can be injective in some, but not all, of their arguments, so we want to do partial decomposition. This is quite different than the way other decomposition is done, where the decomposed equalities replace the original -one. We thus proceed much like we do with superclasses, emitting new Deriveds +one. We thus proceed much like we do with superclasses, emitting new Wanteds when "decomposing" a partially-injective type family Wanted. Injective type families have no corresponding evidence of their injectivity, so we cannot decompose an injective-type-family Given. @@ -1879,6 +1951,27 @@ test case typecheck/should_fail/T10534. {4}: See Note [Decomposing AppTy at representational role] + Because type variables can stand in for newtypes, we conservatively do not + decompose AppTys over representational equality. Here are two examples that + demonstrate why we can't: + + 4a: newtype Phant a = MkPhant Int + [W] alpha Int ~R beta Bool + + If we eventually solve alpha := Phant and beta := Phant, then we can solve + this equality by unwrapping. But it would have been disastrous to decompose + the wanted to produce Int ~ Bool, which is definitely insoluble. + + 4b: newtype Age = MkAge Int + [W] alpha Age ~R Maybe Int + + First, a question: if we know that ty1 ~R ty2, can we conclude that + a ty1 ~R a ty2? Not for all a. This is precisely why we need role annotations + on type constructors. So, if we were to decompose, we would need to + decompose to [W] alpha ~R Maybe and [W] Age ~ Int. On the other hand, if we + later solve alpha := Maybe, then we would decompose to [W] Age ~R Int, and + that would be soluble. + In the implementation of can_eq_nc and friends, we don't directly pattern match using lines like in the tables above, as those tables don't cover all cases (what about PrimTyCon? tuples?). Instead we just ask about injectivity, @@ -2020,14 +2113,11 @@ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2 do { traceTcS "canDecomposableTyConAppOK" (ppr ev $$ ppr eq_rel $$ ppr tc $$ ppr tys1 $$ ppr tys2) ; case ev of - CtDerived {} - -> unifyDeriveds loc tc_roles tys1 tys2 - - CtWanted { ctev_dest = dest } + CtWanted { ctev_dest = dest, ctev_rewriters = rewriters } -- new_locs and tc_roles are both infinite, so -- we are guaranteed that cos has the same length -- as tys1 and tys2 - -> do { cos <- zipWith4M unifyWanted new_locs tc_roles tys1 tys2 + -> do { cos <- zipWith4M (unifyWanted rewriters) new_locs tc_roles tys1 tys2 ; setWantedEq dest (mkTyConAppCo role tc cos) } CtGiven { ctev_evar = evar } @@ -2077,14 +2167,14 @@ canEqFailure :: CtEvidence -> EqRel canEqFailure ev NomEq ty1 ty2 = canEqHardFailure ev ty1 ty2 canEqFailure ev ReprEq ty1 ty2 - = do { redn1 <- rewrite ev ty1 - ; redn2 <- rewrite ev ty2 + = do { (redn1, rewriters1) <- rewrite ev ty1 + ; (redn2, rewriters2) <- rewrite ev ty2 -- We must rewrite the types before putting them in the -- inert set, so that we are sure to kick them out when -- new equalities become available ; traceTcS "canEqFailure with ReprEq" $ vcat [ ppr ev, ppr redn1, ppr redn2 ] - ; new_ev <- rewriteEqEvidence ev NotSwapped redn1 redn2 + ; new_ev <- rewriteEqEvidence (rewriters1 S.<> rewriters2) ev NotSwapped redn1 redn2 ; continueWith (mkIrredCt ReprEqReason new_ev) } -- | Call when canonicalizing an equality fails with utterly no hope. @@ -2093,9 +2183,9 @@ canEqHardFailure :: CtEvidence -- See Note [Make sure that insolubles are fully rewritten] canEqHardFailure ev ty1 ty2 = do { traceTcS "canEqHardFailure" (ppr ty1 $$ ppr ty2) - ; redn1 <- rewrite ev ty1 - ; redn2 <- rewrite ev ty2 - ; new_ev <- rewriteEqEvidence ev NotSwapped redn1 redn2 + ; (redn1, rewriters1) <- rewrite ev ty1 + ; (redn2, rewriters2) <- rewrite ev ty2 + ; new_ev <- rewriteEqEvidence (rewriters1 S.<> rewriters2) ev NotSwapped redn1 redn2 ; continueWith (mkIrredCt ShapeMismatchReason new_ev) } {- @@ -2150,21 +2240,6 @@ Consider [G] (forall a. t1 ~ forall a. t2). Can we decompose this? No -- what would the evidence look like? So instead we simply discard this given evidence. - -Note [Combining insoluble constraints] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -As this point we have an insoluble constraint, like Int~Bool. - - * If it is Wanted, delete it from the cache, so that subsequent - Int~Bool constraints give rise to separate error messages - - * But if it is Derived, DO NOT delete from cache. A class constraint - may get kicked out of the inert set, and then have its functional - dependency Derived constraints generated a second time. In that - case we don't want to get two (or more) error messages by - generating two (or more) insoluble fundep constraints from the same - class constraint. - Note [No top-level newtypes on RHS of representational equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose we're in this situation: @@ -2190,8 +2265,8 @@ Ticket #10009, a very nasty example: g _ = f (undefined :: F a) For g we get [G] g1 : UnF (F a) ~ a - [WD] w1 : UnF (F beta) ~ beta - [WD] w2 : F a ~ F beta + [W] w1 : UnF (F beta) ~ beta + [W] w2 : F a ~ F beta g1 is canonical (CEqCan). It is oriented as above because a is not touchable. See canEqTyVarFunEq. @@ -2206,17 +2281,16 @@ of w2. We'll thus lose. But if w2 is swapped around, to - [D] w3 : F beta ~ F a + [W] w3 : F beta ~ F a -then (after emitting shadow Deriveds, etc. See GHC.Tc.Solver.Monad -Note [The improvement story and derived shadows]) we'll kick w1 out of the inert +then we'll kick w1 out of the inert set (it mentions the LHS of w3). We then rewrite w1 to - [D] w4 : UnF (F a) ~ beta + [W] w4 : UnF (F a) ~ beta and then, using g1, to - [D] w5 : a ~ beta + [W] w5 : a ~ beta at which point we can unify and go on to glory. (This rewriting actually happens all at once, in the call to rewrite during canonicalisation.) @@ -2243,7 +2317,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 ps_xi1 k1 xi2 ps_xi2 k2 + = canEqCanLHSHetero ev eq_rel swapped lhs1 k1 xi2 k2 where k1 = canEqLHSKind lhs1 @@ -2251,40 +2325,42 @@ canEqCanLHS ev eq_rel swapped lhs1 ps_xi1 xi2 ps_xi2 canEqCanLHSHetero :: CtEvidence -- :: (xi1 :: ki1) ~ (xi2 :: ki2) -> EqRel -> SwapFlag - -> CanEqLHS -> TcType -- xi1, pretty xi1 + -> CanEqLHS -- xi1 -> TcKind -- ki1 - -> TcType -> TcType -- xi2, pretty xi2 :: ki2 + -> TcType -- xi2 -> TcKind -- ki2 -> TcS (StopOrContinue Ct) -canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2 +canEqCanLHSHetero ev eq_rel swapped lhs1 ki1 xi2 ki2 -- See Note [Equalities with incompatible kinds] - = do { kind_co <- emit_kind_co -- :: ki2 ~N ki1 + = do { (kind_ev, kind_co) <- mk_kind_eq -- :: ki2 ~N ki1 ; let -- kind_co :: (ki2 :: *) ~N (ki1 :: *) (whether swapped or not) - -- co1 :: kind(tv1) ~N ki1 - ps_rhs' = ps_xi2 `mkCastTy` kind_co -- :: ki1 - lhs_redn = mkReflRedn role xi1 - rhs_redn@(Reduction _ rhs') - = mkGReflRightRedn role xi2 kind_co + rhs_redn = mkGReflRightRedn role xi2 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 ; traceTcS "Hetero equality gives rise to kind equality" (ppr kind_co <+> dcolon <+> sep [ ppr ki2, text "~#", ppr ki1 ]) - ; type_ev <- rewriteEqEvidence ev swapped lhs_redn rhs_redn + ; type_ev <- rewriteEqEvidence rewriters ev swapped lhs_redn rhs_redn - -- rewriteEqEvidence carries out the swap, so we're NotSwapped any more - ; canEqCanLHSHomo type_ev eq_rel NotSwapped lhs1 ps_xi1 rhs' ps_rhs' } + ; 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] + + ; canEqNC kind_ev NomEq ki2 ki1 } where - emit_kind_co :: TcS CoercionN - emit_kind_co - | CtGiven { ctev_evar = evar } <- ev - = do { let kind_co = maybe_sym $ mkTcKindCo (mkTcCoVarCo evar) -- :: k2 ~ k1 - ; kind_ev <- newGivenEvVar kind_loc (kind_pty, evCoercion kind_co) - ; emitWorkNC [kind_ev] - ; return (ctEvCoercion kind_ev) } + mk_kind_eq :: TcS (CtEvidence, CoercionN) + mk_kind_eq = case ev of + CtGiven { ctev_evar = evar } + -> do { let kind_co = maybe_sym $ mkTcKindCo (mkTcCoVarCo evar) -- :: k2 ~ k1 + ; kind_ev <- newGivenEvVar kind_loc (kind_pty, evCoercion kind_co) + ; return (kind_ev, ctEvCoercion kind_ev) } - | otherwise - = unifyWanted kind_loc Nominal ki2 ki1 + CtWanted { ctev_rewriters = rewriters } + -> newWantedEq kind_loc rewriters Nominal ki2 ki1 xi1 = canEqLHSType lhs1 loc = ctev_loc ev @@ -2354,7 +2430,7 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco , TyFamLHS fun_tc2 fun_args2 <- lhs2 = do { traceTcS "canEqCanLHS2 two type families" (ppr lhs1 $$ ppr lhs2) - -- emit derived equalities for injective type families + -- 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. @@ -2387,11 +2463,13 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco | otherwise -- ordinary, non-injective type family = [] - ; unless (isGiven ev) $ - mapM_ (unifyDerived (ctEvLoc ev) Nominal) inj_eqns + ; 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 - ; dflags <- getDynFlags ; let tvs1 = tyCoVarsOfTypes fun_args1 tvs2 = tyCoVarsOfTypes fun_args2 @@ -2402,9 +2480,9 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco -- If we have F a ~ F (F a), we want to swap. swap_for_occurs - | cterHasNoProblem $ checkTyFamEq dflags fun_tc2 fun_args2 + | cterHasNoProblem $ checkTyFamEq fun_tc2 fun_args2 (mkTyConApp fun_tc1 fun_args1) - , cterHasOccursCheck $ checkTyFamEq dflags fun_tc1 fun_args1 + , cterHasOccursCheck $ checkTyFamEq fun_tc1 fun_args1 (mkTyConApp fun_tc2 fun_args2) = True @@ -2448,10 +2526,9 @@ canEqTyVarFunEq :: CtEvidence -- :: lhs ~ (rhs |> mco) -> TcS (StopOrContinue Ct) canEqTyVarFunEq ev eq_rel swapped tv1 ps_xi1 fun_tc2 fun_args2 ps_xi2 mco = do { is_touchable <- touchabilityTest (ctEvFlavour ev) tv1 rhs - ; dflags <- getDynFlags ; if | case is_touchable of { Untouchable -> False; _ -> True } , cterHasNoProblem $ - checkTyVarEq dflags tv1 rhs `cterRemoveProblem` cteTypeFamily + checkTyVarEq tv1 rhs `cterRemoveProblem` cteTypeFamily -> canEqCanLHSFinish ev eq_rel swapped (TyVarLHS tv1) rhs | otherwise @@ -2478,10 +2555,11 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs -- guaranteed that tyVarKind lhs == typeKind rhs, for (TyEq:K) -- (TyEq:N) is checked in can_eq_nc', and (TyEq:TV) is handled in canEqCanLHS2 - = do { dflags <- getDynFlags - ; new_ev <- rewriteEqEvidence ev swapped - (mkReflRedn role lhs_ty) - (mkReflRedn role rhs) + = do { + -- this performs the swap if necessary + new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped + (mkReflRedn role lhs_ty) + (mkReflRedn role rhs) -- by now, (TyEq:K) is already satisfied ; massert (canEqLHSKind lhs `eqType` tcTypeKind rhs) @@ -2495,9 +2573,7 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs -- guarantees (TyEq:OC), (TyEq:F) -- Must do the occurs check even on tyvar/tyvar -- equalities, in case have x ~ (y :: ..x...); this is #12593. - -- This next line checks also for coercion holes (TyEq:H); see - -- Note [Equalities with incompatible kinds] - ; let result0 = checkTypeEq dflags lhs rhs `cterRemoveProblem` cteTypeFamily + ; let result0 = checkTypeEq lhs rhs `cterRemoveProblem` cteTypeFamily -- type families are OK here -- NB: no occCheckExpand here; see Note [Rewriting synonyms] in GHC.Tc.Solver.Rewrite @@ -2507,10 +2583,7 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs NomEq -> result0 ReprEq -> cterSetOccursCheckSoluble result0 - reason | result `cterHasOnlyProblem` cteHoleBlocker - = HoleBlockerReason (coercionHolesOfType rhs) - | otherwise - = NonCanonicalReason result + reason = NonCanonicalReason result ; if cterHasNoProblem result then do { traceTcS "CEqCan" (ppr lhs $$ ppr rhs) @@ -2531,14 +2604,15 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs ; traceTcS "new RHS:" (ppr new_rhs) -- This check is Detail (1) in the Note - ; if cterHasOccursCheck (checkTyVarEq dflags lhs_tv new_rhs) + ; if cterHasOccursCheck (checkTyVarEq lhs_tv new_rhs) then do { traceTcS "Note [Type variable cycles] Detail (1)" (ppr new_rhs) ; continueWith (mkIrredCt reason new_ev) } else do { -- See Detail (6) of Note [Type variable cycles] - new_new_ev <- rewriteEqEvidence new_ev NotSwapped + new_new_ev <- rewriteEqEvidence emptyRewriterSet + new_ev NotSwapped (mkReflRedn Nominal lhs_ty) rhs_redn @@ -2584,7 +2658,7 @@ rewriteCastedEquality :: CtEvidence -- :: lhs ~ (rhs |> mco), or (rhs |> mco -> TcS CtEvidence -- :: (lhs |> sym mco) ~ rhs -- result is independent of SwapFlag rewriteCastedEquality ev eq_rel swapped lhs rhs mco - = rewriteEqEvidence ev swapped lhs_redn rhs_redn + = rewriteEqEvidence emptyRewriterSet ev swapped lhs_redn rhs_redn where lhs_redn = mkGReflRightMRedn role lhs sym_mco rhs_redn = mkGReflLeftMRedn role rhs mco @@ -2603,78 +2677,38 @@ k2 and use this to cast. To wit, from [X] (tv :: k1) ~ (rhs :: k2) -(where [X] is [G], [W], or [D]), we go to +(where [X] is [G] or [W]), we go to - [noDerived X] co :: k2 ~ k1 - [X] (tv :: k1) ~ ((rhs |> co) :: k1) + [X] co :: k2 ~ k1 + [X] (tv :: k1) ~ ((rhs |> co) :: k1) -where - - noDerived G = G - noDerived _ = W - -For reasons described in Wrinkle (2) below, we want the [X] constraint to be "blocked"; -that is, it should be put aside, and not used to rewrite any other constraint, -until the kind-equality on which it depends (namely 'co' above) is solved. -To achieve this -* The [X] constraint is a CIrredCan -* With a cc_reason of HoleBlockerReason bchs -* Where 'bchs' is the set of "blocking coercion holes". The blocking coercion - holes are the free coercion holes of [X]'s type -* When all the blocking coercion holes in the CIrredCan are filled (solved), - we convert [X] to a CNonCanonical and put it in the work list. -All this is described in more detail in Wrinkle (2). +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) The noDerived step is because Derived equalities have no evidence. - And yet we absolutely need evidence to be able to proceed here. - Given evidence will use the KindCo coercion; Wanted evidence will - be a coercion hole. Even a Derived hetero equality begets a Wanted - kind equality. - - (2) Though it would be sound to do so, we must not mark the rewritten Wanted - [W] (tv :: k1) ~ ((rhs |> co) :: k1) - as canonical in the inert set. In particular, we must not unify tv. - If we did, the Wanted becomes a Given (effectively), and then can - rewrite other Wanteds. But that's bad: See Note [Wanteds do not rewrite Wanteds] - in GHC.Tc.Types.Constraint. The problem is about poor error messages. See #11198 for - tales of destruction. - - So, we have an invariant on CEqCan (TyEq:H) that the RHS does not have - any coercion holes. This is checked in checkTypeEq. Any equalities that - have such an RHS are turned into CIrredCans with a HoleBlockerReason. We also - must be sure to kick out any such CIrredCan constraints that mention coercion holes - when those holes get filled in, so that the unification step can now proceed. - - The kicking out is done in kickOutAfterFillingCoercionHole, and the inerts - are stored in the inert_blocked field of InertCans. - - However, we must be careful: we kick out only when no coercion holes are - left. The holes in the type are stored in the HoleBlockerReason CtIrredReason. - The extra check that there are no more remaining holes avoids - needless work when rewriting evidence (which fills coercion holes) and - aids efficiency. - - Moreover, kicking out when there are remaining unfilled holes can - cause a loop in the solver in this case: - [W] w1 :: (ty1 :: F a) ~ (ty2 :: s) - After canonicalisation, we discover that this equality is heterogeneous. - So we emit - [W] co_abc :: F a ~ s - and preserve the original as - [W] w2 :: (ty1 |> co_abc) ~ ty2 (blocked on co_abc) - Then, co_abc comes becomes the work item. It gets swapped in - canEqCanLHS2 and then back again in canEqTyVarFunEq. We thus get - co_abc := sym co_abd, and then co_abd := sym co_abe, with - [W] co_abe :: F a ~ s - This process has filled in co_abc. Suppose w2 were kicked out. - When it gets processed, - would get this whole chain going again. The solution is to - kick out a blocked constraint only when the result of filling - in the blocking coercion involves no further blocking coercions. - Alternatively, we could be careful not to do unnecessary swaps during - canonicalisation, but that seems hard to do, in general. + (1) 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 |> 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. + + On the other hand, w is perfectly suitable for rewriting, because of the + way we carefully track rewriter sets. + + 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 algorithm detailed here, producing [W] co :: k2 ~ k1, and adding @@ -2694,25 +2728,6 @@ Wrinkles: cast appears opposite a tyvar. This is implemented in the cast case of can_eq_nc'. - (4) Reporting an error for a constraint that is blocked with HoleBlockerReason - is hard: what would we say to users? And we don't - really need to report, because if a constraint is blocked, then - there is unsolved wanted blocking it; that unsolved wanted will - be reported. We thus push such errors to the bottom of the queue - in the error-reporting code; they should never be printed. - - (4a) It would seem possible to do this filtering just based on the - presence of a blocking coercion hole. However, this is no good, - as it suppresses e.g. no-instance-found errors. We thus record - a CtIrredReason in CIrredCan and filter based on this status. - This happened in T14584. An alternative approach is to expressly - look for *equalities* with blocking coercion holes, but actually - recording the blockage in a status field seems nicer. - - (4b) The error message might be printed with -fdefer-type-errors, - so it still must exist. This is the only reason why there is - a message at all. Otherwise, we could simply do nothing. - Historical note: We used to do this via emitting a Derived kind equality and then parking @@ -2772,7 +2787,7 @@ Consider this situation (from indexed-types/should_compile/GivenLoop): or (typecheck/should_compile/T19682b): instance C (a -> b) - *[WD] alpha ~ (Arg alpha -> Res alpha) + *[W] alpha ~ (Arg alpha -> Res alpha) [W] C alpha In order to solve the final Wanted, we must use the starred constraint @@ -2795,17 +2810,15 @@ via new equality constraints. Our situations thus become: or instance C (a -> b) - [WD] alpha ~ (cbv1 -> cbv2) - [WD] Arg alpha ~ cbv1 - [WD] Res alpha ~ cbv2 + [W] alpha ~ (cbv1 -> cbv2) + [W] Arg alpha ~ cbv1 + [W] Res alpha ~ cbv2 [W] C alpha This transformation (creating the new types and emitting new equality constraints) is done in breakTyVarCycle_maybe. -The details depend on whether we're working with a Given or a Derived. -(Note that the Wanteds are really WDs, above. This is because Wanteds -are not used for rewriting.) +The details depend on whether we're working with a Given or a Wanted. Given ----- @@ -2849,19 +2862,19 @@ Note that * The evidence for the new `F a ~ cbv` constraint is Refl, because we know this fill-in is ultimately going to happen. -Wanted/Derived --------------- +Wanted +------ The fresh cycle-breaker variables here must actually be normal, touchable metavariables. That is, they are TauTvs. Nothing at all unusual. Repeating the example from above, we have - *[WD] alpha ~ (Arg alpha -> Res alpha) + *[W] alpha ~ (Arg alpha -> Res alpha) and we turn this into - *[WD] alpha ~ (cbv1 -> cbv2) - [WD] Arg alpha ~ cbv1 - [WD] Res alpha ~ cbv2 + *[W] alpha ~ (cbv1 -> cbv2) + [W] Arg alpha ~ cbv1 + [W] Res alpha ~ cbv2 where cbv1 and cbv2 are fresh TauTvs. Why TauTvs? See [Why TauTvs] below. @@ -2875,11 +2888,11 @@ here (including further context from our original example, from the top of the Note): instance C (a -> b) - [WD] Arg (cbv1 -> cbv2) ~ cbv1 - [WD] Res (cbv1 -> cbv2) ~ cbv2 + [W] Arg (cbv1 -> cbv2) ~ cbv1 + [W] Res (cbv1 -> cbv2) ~ cbv2 [W] C (cbv1 -> cbv2) -The first two WD constraints reduce to reflexivity and are discarded, +The first two W constraints reduce to reflexivity and are discarded, and the last is easily soluble. [Why TauTvs]: @@ -2897,43 +2910,43 @@ to unify the cbvs: AllEqF '[] '[] = () AllEqF (x : xs) (y : ys) = (x ~ y, AllEq xs ys) - [WD] alpha ~ (Head alpha : Tail alpha) - [WD] AllEqF '[Bool] alpha + [W] alpha ~ (Head alpha : Tail alpha) + [W] AllEqF '[Bool] alpha Without the logic detailed in this Note, we're stuck here, as AllEqF cannot reduce and alpha cannot unify. Let's instead apply our cycle-breaker approach, just as described above. We thus invent cbv1 and cbv2 and unify alpha := cbv1 -> cbv2, yielding (after zonking) - [WD] Head (cbv1 : cbv2) ~ cbv1 - [WD] Tail (cbv1 : cbv2) ~ cbv2 - [WD] AllEqF '[Bool] (cbv1 : cbv2) + [W] Head (cbv1 : cbv2) ~ cbv1 + [W] Tail (cbv1 : cbv2) ~ cbv2 + [W] AllEqF '[Bool] (cbv1 : cbv2) -The first two WD constraints simplify to reflexivity and are discarded. +The first two W constraints simplify to reflexivity and are discarded. But the last reduces: - [WD] Bool ~ cbv1 - [WD] AllEq '[] cbv2 + [W] Bool ~ cbv1 + [W] AllEq '[] cbv2 The first of these is solved by unification: cbv1 := Bool. The second is solved by the instance for AllEq to become - [WD] AllEqF '[] cbv2 - [WD] SameShapeAs '[] cbv2 + [W] AllEqF '[] cbv2 + [W] SameShapeAs '[] cbv2 While the first of these is stuck, the second makes progress, to lead to - [WD] AllEqF '[] cbv2 - [WD] cbv2 ~ '[] + [W] AllEqF '[] cbv2 + [W] cbv2 ~ '[] This second constraint is solved by unification: cbv2 := '[]. We now have - [WD] AllEqF '[] '[] + [W] AllEqF '[] '[] which reduces to - [WD] () + [W] () which is trivially satisfiable. Hooray! @@ -2950,8 +2963,7 @@ We detect this scenario by the following characteristics: - and a nominal equality - and either - a Given flavour (but see also Detail (7) below) - - a Wanted/Derived or just plain Derived flavour, with a touchable metavariable - on the left + - a Wanted flavour, with a touchable metavariable on the left We don't use this trick for representational equalities, as there is no concrete use case where it is helpful (unlike for nominal equalities). @@ -3070,7 +3082,7 @@ Details: We track these equalities by giving them a special CtOrigin, CycleBreakerOrigin. This works for both Givens and WDs, as - we need the logic in the WD case for e.g. typecheck/should_fail/T17139. + we need the logic in the W case for e.g. typecheck/should_fail/T17139. (8) We really want to do this all only when there is a soluble occurs-check failure, not when other problems arise (such as an impredicative @@ -3116,7 +3128,9 @@ andWhenContinue tcs1 tcs2 ContinueWith ct -> tcs2 ct } infixr 0 `andWhenContinue` -- allow chaining with ($) -rewriteEvidence :: CtEvidence -- ^ old evidence +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 @@ -3126,7 +3140,7 @@ rewriteEvidence :: CtEvidence -- ^ old evidence 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/derived flag as old_ev +* 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 @@ -3135,7 +3149,7 @@ Main purpose: create new evidence for new_pred; flavour of same flavor ------------------------------------------------------------------- Wanted Already solved or in inert Nothing - or Derived Not Just new_evidence + Not Just new_evidence Given Already in inert Nothing Not Just new_evidence @@ -3150,37 +3164,33 @@ using new_pred. The rewriter preserves type synonyms, so they should appear in new_pred as well as in old_pred; that is important for good error messages. + +If we are rewriting with Refl, then there are no new rewriters to add to +the rewriter set. We check this with an assertion. -} -rewriteEvidence old_ev@(CtDerived {}) (Reduction _co new_pred) - = -- If derived, don't even look at the coercion. - -- This is very important, DO NOT re-order the equations for - -- rewriteEvidence to put the isTcReflCo test first! - -- Why? Because for *Derived* constraints, c, the coercion, which - -- was produced by rewriting, may contain suspended calls to - -- (ctEvExpr c), which fails for Derived constraints. - -- (Getting this wrong caused #7384.) - continueWith (setCtEvPredType old_ev new_pred) - -rewriteEvidence old_ev (Reduction co new_pred) +rewriteEvidence rewriters old_ev (Reduction co new_pred) | isTcReflCo co -- See Note [Rewriting with Refl] - = continueWith (setCtEvPredType old_ev new_pred) + = assert (isEmptyRewriterSet rewriters) $ + continueWith (setCtEvPredType old_ev new_pred) -rewriteEvidence ev@(CtGiven { ctev_evar = old_evar, ctev_loc = loc }) (Reduction co new_pred) - = do { new_ev <- newGivenEvVar loc (new_pred, new_tm) +rewriteEvidence rewriters ev@(CtGiven { ctev_evar = old_evar, ctev_loc = loc }) + (Reduction co new_pred) + = assert (isEmptyRewriterSet rewriters) $ -- this is a Given, not a wanted + do { new_ev <- newGivenEvVar loc (new_pred, new_tm) ; continueWith new_ev } where -- mkEvCast optimises ReflCo new_tm = mkEvCast (evId old_evar) (tcDowngradeRole Representational (ctEvRole ev) co) -rewriteEvidence ev@(CtWanted { ctev_dest = dest - , ctev_nosh = si - , ctev_loc = loc }) (Reduction co new_pred) - = do { mb_new_ev <- newWanted_SI si loc new_pred - -- The "_SI" variant ensures that we make a new Wanted - -- with the same shadow-info as the existing one (#16735) +rewriteEvidence new_rewriters + ev@(CtWanted { ctev_dest = dest + , ctev_loc = loc + , ctev_rewriters = rewriters }) + (Reduction co new_pred) + = do { mb_new_ev <- newWanted loc rewriters' new_pred ; massert (tcCoercionRole co == ctEvRole ev) ; setWantedEvTerm dest (mkEvCast (getEvExpr mb_new_ev) @@ -3188,9 +3198,14 @@ rewriteEvidence ev@(CtWanted { ctev_dest = dest ; case mb_new_ev of Fresh new_ev -> continueWith new_ev Cached _ -> stopWith ev "Cached wanted" } + where + rewriters' = rewriters S.<> new_rewriters -rewriteEqEvidence :: CtEvidence -- Old evidence :: olhs ~ orhs (not swapped) +rewriteEqEvidence :: RewriterSet -- New rewriters + -- See GHC.Tc.Types.Constraint + -- Note [Wanteds rewrite Wanteds] + -> CtEvidence -- Old evidence :: olhs ~ orhs (not swapped) -- or orhs ~ olhs (swapped) -> SwapFlag -> Reduction -- lhs_co :: olhs ~ nlhs @@ -3211,10 +3226,7 @@ rewriteEqEvidence :: CtEvidence -- Old evidence :: olhs ~ orhs (not swap -- w : orhs ~ olhs = rhs_co ; sym w1 ; sym lhs_co -- -- It's all a form of rewriteEvidence, specialised for equalities -rewriteEqEvidence old_ev swapped (Reduction lhs_co nlhs) (Reduction rhs_co nrhs) - | CtDerived {} <- old_ev -- Don't force the evidence for a Derived - = return (setCtEvPredType old_ev new_pred) - +rewriteEqEvidence new_rewriters old_ev swapped (Reduction lhs_co nlhs) (Reduction rhs_co nrhs) | NotSwapped <- swapped , isTcReflCo lhs_co -- See Note [Rewriting with Refl] , isTcReflCo rhs_co @@ -3226,17 +3238,21 @@ rewriteEqEvidence old_ev swapped (Reduction lhs_co nlhs) (Reduction rhs_co nrhs) `mkTcTransCo` rhs_co) ; newGivenEvVar loc' (new_pred, new_tm) } - | CtWanted { ctev_dest = dest, ctev_nosh = si } <- old_ev - = do { (new_ev, hole_co) <- newWantedEq_SI si loc' - (ctEvRole old_ev) nlhs nrhs - -- The "_SI" variant ensures that we make a new Wanted - -- with the same shadow-info as the existing one (#16735) + | 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 ; let co = maybeTcSymCo swapped $ lhs_co `mkTransCo` hole_co `mkTransCo` mkTcSymCo rhs_co ; setWantedEq dest co - ; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co]) + ; traceTcS "rewriteEqEvidence" (vcat [ ppr old_ev + , ppr nlhs + , ppr nrhs + , ppr co + , ppr new_rewriters ]) ; return new_ev } #if __GLASGOW_HASKELL__ <= 810 @@ -3259,11 +3275,10 @@ rewriteEqEvidence old_ev swapped (Reduction lhs_co nlhs) (Reduction rhs_co nrhs) * * ************************************************************************ -Note [unifyWanted and unifyDerived] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Note [unifyWanted] +~~~~~~~~~~~~~~~~~~ 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. -Similar remarks apply for Derived. Rather than making an equality test (which traverses the structure of the type, perhaps fruitlessly), unifyWanted traverses the common structure, and @@ -3272,32 +3287,32 @@ But where it succeeds in finding common structure, it just builds a coercion to reflect it. -} -unifyWanted :: CtLoc -> Role - -> TcType -> TcType -> TcS Coercion +unifyWanted :: RewriterSet -> CtLoc + -> Role -> TcType -> TcType -> TcS Coercion -- Return coercion witnessing the equality of the two types, -- emitting new work equalities where necessary to achieve that -- Very good short-cut when the two types are equal, or nearly so --- See Note [unifyWanted and unifyDerived] +-- See Note [unifyWanted] -- The returned coercion's role matches the input parameter -unifyWanted loc Phantom ty1 ty2 - = do { kind_co <- unifyWanted loc Nominal (tcTypeKind ty1) (tcTypeKind ty2) +unifyWanted rewriters loc Phantom ty1 ty2 + = do { kind_co <- unifyWanted rewriters loc Nominal (tcTypeKind ty1) (tcTypeKind ty2) ; return (mkPhantomCo kind_co ty1 ty2) } -unifyWanted loc role orig_ty1 orig_ty2 +unifyWanted rewriters loc role orig_ty1 orig_ty2 = go orig_ty1 orig_ty2 where go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2 go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2' go (FunTy _ w1 s1 t1) (FunTy _ w2 s2 t2) - = do { co_s <- unifyWanted loc role s1 s2 - ; co_t <- unifyWanted loc role t1 t2 - ; co_w <- unifyWanted loc Nominal w1 w2 + = 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 (mkFunCo role 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 loc) + = do { cos <- zipWith3M (unifyWanted rewriters loc) (tyConRolesX role tc1) tys1 tys2 ; return (mkTyConAppCo role tc1 cos) } @@ -3320,48 +3335,4 @@ unifyWanted loc role orig_ty1 orig_ty2 bale_out ty1 ty2 | ty1 `tcEqType` ty2 = return (mkTcReflCo role ty1) -- Check for equality; e.g. a ~ a, or (m a) ~ (m a) - | otherwise = emitNewWantedEq loc role orig_ty1 orig_ty2 - -unifyDeriveds :: CtLoc -> [Role] -> [TcType] -> [TcType] -> TcS () --- See Note [unifyWanted and unifyDerived] -unifyDeriveds loc roles tys1 tys2 = zipWith3M_ (unify_derived loc) roles tys1 tys2 - -unifyDerived :: CtLoc -> Role -> Pair TcType -> TcS () --- See Note [unifyWanted and unifyDerived] -unifyDerived loc role (Pair ty1 ty2) = unify_derived loc role ty1 ty2 - -unify_derived :: CtLoc -> Role -> TcType -> TcType -> TcS () --- Create new Derived and put it in the work list --- Should do nothing if the two types are equal --- See Note [unifyWanted and unifyDerived] -unify_derived _ Phantom _ _ = return () -unify_derived loc role orig_ty1 orig_ty2 - = go orig_ty1 orig_ty2 - where - go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2 - go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2' - - go (FunTy _ w1 s1 t1) (FunTy _ w2 s2 t2) - = do { unify_derived loc role s1 s2 - ; unify_derived loc role t1 t2 - ; unify_derived loc Nominal w1 w2 } - go (TyConApp tc1 tys1) (TyConApp tc2 tys2) - | tc1 == tc2, tys1 `equalLength` tys2 - , isInjectiveTyCon tc1 role - = unifyDeriveds loc (tyConRolesX role tc1) tys1 tys2 - 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 ty2 = bale_out ty1 ty2 - - bale_out ty1 ty2 - | ty1 `tcEqType` ty2 = return () - -- Check for equality; e.g. a ~ a, or (m a) ~ (m a) - | otherwise = emitNewDerivedEq loc role orig_ty1 orig_ty2 + | otherwise = emitNewWantedEq loc rewriters role orig_ty1 orig_ty2 diff --git a/compiler/GHC/Tc/Solver/InertSet.hs b/compiler/GHC/Tc/Solver/InertSet.hs index 53b6097ec7..b5aad268b5 100644 --- a/compiler/GHC/Tc/Solver/InertSet.hs +++ b/compiler/GHC/Tc/Solver/InertSet.hs @@ -1,4 +1,5 @@ {-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeApplications #-} {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} @@ -7,7 +8,7 @@ module GHC.Tc.Solver.InertSet ( -- * The work list WorkList(..), isEmptyWorkList, emptyWorkList, extendWorkListNonEq, extendWorkListCt, - extendWorkListCts, extendWorkListEq, extendWorkListDeriveds, + extendWorkListCts, extendWorkListEq, appendWorkList, extendWorkListImplic, workListSize, selectWorkItem, @@ -25,6 +26,7 @@ module GHC.Tc.Solver.InertSet ( -- * Inert equalities foldTyEqs, delEq, findEq, + partitionInertEqs, partitionFunEqs, -- * Kick-out kickOutRewritableLHS @@ -41,7 +43,6 @@ import GHC.Tc.Utils.TcType import GHC.Types.Var import GHC.Types.Var.Env -import GHC.Core.Class (Class(..)) import GHC.Core.Reduction import GHC.Core.Predicate import GHC.Core.TyCo.FVs @@ -50,12 +51,11 @@ import GHC.Core.TyCon import GHC.Core.Unify import GHC.Data.Bag -import GHC.Utils.Misc ( chkAppend, partitionWith ) +import GHC.Utils.Misc ( partitionWith ) import GHC.Utils.Outputable import GHC.Utils.Panic import Data.List ( partition ) -import Data.List.NonEmpty ( NonEmpty(..) ) {- ************************************************************************ @@ -89,13 +89,13 @@ It's very important to process equalities /first/: * (Avoiding fundep iteration) As #14723 showed, it's possible to get non-termination if we - - Emit the Derived fundep equalities for a class constraint, + - Emit the fundep equalities for a class constraint, generating some fresh unification variables. - That leads to some unification - Which kicks out the class constraint - - Which isn't solved (because there are still some more Derived + - Which isn't solved (because there are still some more equalities in the work-list), but generates yet more fundeps - Solution: prioritise derived equalities over class constraints + Solution: prioritise equalities over class constraints * (Class equalities) We need to prioritise equalities even if they are hidden inside a class constraint; @@ -106,12 +106,6 @@ It's very important to process equalities /first/: 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. -* (Derived equalities) Originally we tried to postpone processing - Derived equalities, in the hope that we might never need to deal - with them at all; but in fact we must process Derived equalities - eagerly, partly for the (Efficiency) reason, and more importantly - for (Avoiding fundep iteration). - Note [Prioritise class equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We prioritise equalities in the solver (see selectWorkItem). But class @@ -144,7 +138,7 @@ See GHC.Tc.Solver.Monad.deferTcSForAllEq -- See Note [WorkList priorities] data WorkList = WL { wl_eqs :: [Ct] -- CEqCan, CDictCan, CIrredCan - -- Given, Wanted, and Derived + -- Given and Wanted -- Contains both equality constraints and their -- class-level variants (a~b) and (a~~b); -- See Note [Prioritise equalities] @@ -176,10 +170,6 @@ extendWorkListNonEq :: Ct -> WorkList -> WorkList -- Extension by non equality extendWorkListNonEq ct wl = wl { wl_rest = ct : wl_rest wl } -extendWorkListDeriveds :: [CtEvidence] -> WorkList -> WorkList -extendWorkListDeriveds evs wl - = extendWorkListCts (map mkNonCanonical evs) wl - extendWorkListImplic :: Implication -> WorkList -> WorkList extendWorkListImplic implic wl = wl { wl_implics = implic `consBag` wl_implics wl } @@ -236,7 +226,7 @@ instance Outputable WorkList where data InertSet = IS { inert_cans :: InertCans - -- Canonical Given, Wanted, Derived + -- Canonical Given, Wanted -- Sometimes called "the inert set" , inert_cycle_breakers :: [(TcTyVar, TcType)] @@ -278,8 +268,7 @@ emptyInertCans , inert_safehask = emptyDictMap , inert_funeqs = emptyFunEqs , inert_insts = [] - , inert_irreds = emptyCts - , inert_blocked = emptyCts } + , inert_irreds = emptyCts } emptyInert :: InertSet emptyInert @@ -618,7 +607,7 @@ that the right variable is on the left of the equality when both are tyvars. You might wonder whether the skolem really needs to be bound "in the -very same implication" as the equuality constraint. +very same implication" as the equality constraint. Consider this (c.f. #15009): data S a where @@ -733,7 +722,7 @@ yet, we have a hard time noticing an occurs-check problem when building S, as the two equalities cannot rewrite one another. R2 actually restricts our ability to accept user-written programs. See -Note [Deriveds do rewrite Deriveds] in GHC.Tc.Types.Constraint for an example. +Note [Avoiding rewriting cycles] in GHC.Tc.Types.Constraint for an example. Note [Rewritable] ~~~~~~~~~~~~~~~~~ @@ -859,13 +848,6 @@ The idea is that us to kick out an inert wanted that mentions a, because of (K2a). This is a common case, hence good not to kick out. See also (K2a) below. -* Lemma (L2): if not (fw >= fw), then K0 holds and we kick out nothing - Proof: using Definition [Can-rewrite relation], fw can't rewrite anything - and so K0 holds. Intuitively, since fw can't rewrite anything (Lemma (L0)), - adding it cannot cause any loops - This is a common case, because Wanteds cannot rewrite Wanteds. - It's used to avoid even looking for constraint to kick out. - * Lemma (L1): The conditions of the Main Theorem imply that there is no (lhs -fs-> t) in S, s.t. (fs >= fw). Proof. Suppose the contrary (fs >= fw). Then because of (T1), @@ -937,10 +919,10 @@ Why we cannot drop the (fs >= fw) condition: can cause a loop. Example: Work: [G] b ~ a - Inert: [D] a ~ b + Inert: [W] a ~ b - (where G >= G, G >= D, and D >= D) - If we don't kick out the inert, then we get a loop on e.g. [D] a ~ Int. + (where G >= G, G >= W, and W >= W) + If we don't kick out the inert, then we get a loop on e.g. [W] a ~ Int. * Note that the above example is different if the inert is a Given G, because (T1) won't hold. @@ -1051,7 +1033,7 @@ Note [Flavours with roles] The system described in Note [inert_eqs: the inert equalities] discusses an abstract set of flavours. In GHC, flavours have two components: the flavour proper, -taken from {Wanted, Derived, Given} and the equality relation (often called +taken from {Wanted, Given} and the equality relation (often called role), taken from {NomEq, ReprEq}. When substituting w.r.t. the inert set, as described in Note [inert_eqs: the inert equalities], @@ -1080,7 +1062,7 @@ data InertCans -- See Note [Detailed InertCans Invariants] for more -- All CEqCans with a TyFamLHS; index is the whole family head type. -- LHS is fully rewritten (modulo eqCanRewrite constraints) -- wrt inert_eqs - -- Can include all flavours, [G], [W], [WD], [D] + -- Can include both [G] and [W] , inert_dicts :: DictMap Ct -- Dictionaries only @@ -1103,14 +1085,6 @@ data InertCans -- See Note [Detailed InertCans Invariants] for more -- and which don't interact with others (e.g. (c a)) -- and insoluble predicates (e.g. Int ~ Bool, or a ~ [a]) - , inert_blocked :: Cts - -- Equality predicates blocked on a coercion hole. - -- Each Ct is a CIrredCan with cc_reason = HoleBlockerReason - -- See Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical - -- wrinkle (2) - -- These are stored separately from inert_irreds because - -- they get kicked out for different reasons - , inert_given_eq_lvl :: TcLevel -- The TcLevel of the innermost implication that has a Given -- equality of the sort that make a unification variable untouchable @@ -1133,7 +1107,6 @@ instance Outputable InertCans where , inert_dicts = dicts , inert_safehask = safehask , inert_irreds = irreds - , inert_blocked = blocked , inert_given_eq_lvl = ge_lvl , inert_given_eqs = given_eqs , inert_insts = insts }) @@ -1150,15 +1123,13 @@ instance Outputable InertCans where text "Safe Haskell unsafe overlap =" <+> pprCts (dictsToBag safehask) , ppUnless (isEmptyCts irreds) $ text "Irreds =" <+> pprCts irreds - , ppUnless (isEmptyCts blocked) $ - text "Blocked =" <+> pprCts blocked , ppUnless (null insts) $ text "Given instances =" <+> vcat (map ppr insts) , text "Innermost given equalities =" <+> ppr ge_lvl , text "Given eqs at this level =" <+> ppr given_eqs ] where - folder (EqualCtList eqs) rest = nonEmptyToBag eqs `andCts` rest + folder eqs rest = listToBag eqs `andCts` rest {- ********************************************************************* * * @@ -1168,7 +1139,7 @@ instance Outputable InertCans where addTyEq :: InertEqs -> TcTyVar -> Ct -> InertEqs addTyEq old_eqs tv ct - = extendDVarEnv_C add_eq old_eqs tv (unitEqualCtList ct) + = extendDVarEnv_C add_eq old_eqs tv [ct] where add_eq old_eqs _ = addToEqualCtList ct old_eqs @@ -1178,15 +1149,14 @@ addCanFunEq old_eqs fun_tc fun_args ct = alterTcApp old_eqs fun_tc fun_args upd where upd (Just old_equal_ct_list) = Just $ addToEqualCtList ct old_equal_ct_list - upd Nothing = Just $ unitEqualCtList ct + upd Nothing = Just [ct] foldTyEqs :: (Ct -> b -> b) -> InertEqs -> b -> b foldTyEqs k eqs z - = foldDVarEnv (\(EqualCtList cts) z -> foldr k z cts) z eqs + = foldDVarEnv (\cts z -> foldr k z cts) z eqs findTyEqs :: InertCans -> TyVar -> [Ct] -findTyEqs icans tv = maybe [] id (fmap @Maybe equalCtListToList $ - lookupDVarEnv (inert_eqs icans) tv) +findTyEqs icans tv = concat @Maybe (lookupDVarEnv (inert_eqs icans) tv) delEq :: InertCans -> CanEqLHS -> TcType -> InertCans delEq ic lhs rhs = case lhs of @@ -1206,8 +1176,52 @@ delEq ic lhs rhs = case lhs of findEq :: InertCans -> CanEqLHS -> [Ct] findEq icans (TyVarLHS tv) = findTyEqs icans tv findEq icans (TyFamLHS fun_tc fun_args) - = maybe [] id (fmap @Maybe equalCtListToList $ - findFunEq (inert_funeqs icans) fun_tc fun_args) + = concat @Maybe (findFunEq (inert_funeqs icans) fun_tc fun_args) + +{-# INLINE partition_eqs_container #-} +partition_eqs_container + :: forall container + . container -- empty container + -> (forall b. (EqualCtList -> b -> b) -> b -> container -> b) -- folder + -> (container -> CanEqLHS -> EqualCtList -> container) -- extender + -> (Ct -> Bool) + -> container + -> ([Ct], container) +partition_eqs_container empty_container fold_container extend_container pred orig_inerts + = fold_container folder ([], empty_container) orig_inerts + where + folder :: EqualCtList -> ([Ct], container) -> ([Ct], container) + folder eqs (acc_true, acc_false) + = (eqs_true ++ acc_true, acc_false') + where + (eqs_true, eqs_false) = partition pred eqs + + acc_false' + | CEqCan { cc_lhs = lhs } : _ <- eqs_false + = extend_container acc_false lhs eqs_false + | otherwise + = acc_false + +partitionInertEqs :: (Ct -> Bool) -- Ct will always be a CEqCan with a TyVarLHS + -> InertEqs + -> ([Ct], InertEqs) +partitionInertEqs = partition_eqs_container emptyDVarEnv foldDVarEnv extendInertEqs + +-- precondition: CanEqLHS is a TyVarLHS +extendInertEqs :: InertEqs -> CanEqLHS -> EqualCtList -> InertEqs +extendInertEqs eqs (TyVarLHS tv) new_eqs = extendDVarEnv eqs tv new_eqs +extendInertEqs _ other _ = pprPanic "extendInertEqs" (ppr other) + +partitionFunEqs :: (Ct -> Bool) -- Ct will always be a CEqCan with a TyFamLHS + -> FunEqMap EqualCtList + -> ([Ct], FunEqMap EqualCtList) +partitionFunEqs + = partition_eqs_container emptyFunEqs (\ f z eqs -> foldFunEqs f eqs z) extendFunEqs + +-- precondition: CanEqLHS is a TyFamLHS +extendFunEqs :: FunEqMap EqualCtList -> CanEqLHS -> EqualCtList -> FunEqMap EqualCtList +extendFunEqs eqs (TyFamLHS tf args) new_eqs = insertTcApp eqs tf args new_eqs +extendFunEqs _ other _ = pprPanic "extendFunEqs" (ppr other) {- ********************************************************************* * * @@ -1225,18 +1239,13 @@ addInertItem tc_lvl TyFamLHS tc tys -> ics { inert_funeqs = addCanFunEq funeqs tc tys item } TyVarLHS tv -> ics { inert_eqs = addTyEq eqs tv item } -addInertItem tc_lvl ics@(IC { inert_blocked = blocked }) - item@(CIrredCan { cc_reason = HoleBlockerReason {}}) - = updateGivenEqs tc_lvl item $ -- this item is always an equality - ics { inert_blocked = blocked `snocBag` item } - addInertItem tc_lvl ics@(IC { inert_irreds = irreds }) item@(CIrredCan {}) = updateGivenEqs tc_lvl item $ -- An Irred might turn out to be an -- equality, so we play safe ics { inert_irreds = irreds `snocBag` item } addInertItem _ ics item@(CDictCan { cc_class = cls, cc_tyargs = tys }) - = ics { inert_dicts = addDictCt (inert_dicts ics) (classTyCon cls) tys item } + = ics { inert_dicts = addDict (inert_dicts ics) cls tys item } addInertItem _ ics@( IC { inert_irreds = irreds }) item@(CSpecialCan {}) = ics { inert_irreds = irreds `snocBag` item } @@ -1284,14 +1293,6 @@ kickOutRewritableLHS new_fr new_lhs , inert_funeqs = funeqmap , inert_irreds = irreds , inert_insts = old_insts }) - | not (new_fr `eqMayRewriteFR` new_fr) - = (emptyWorkList, ics) - -- If new_fr can't rewrite itself, it can't rewrite - -- anything else, so no need to kick out anything. - -- (This is a common case: wanteds can't rewrite wanteds) - -- Lemma (L2) in Note [Extending the inert equalities] - - | otherwise = (kicked_out, inert_cans_in) where -- inert_safehask stays unchanged; is that right? @@ -1313,12 +1314,10 @@ kickOutRewritableLHS new_fr new_lhs ((dicts_out `andCts` irs_out) `extendCtsList` insts_out) - (tv_eqs_out, tv_eqs_in) = foldDVarEnv (kick_out_eqs extend_tv_eqs) - ([], emptyDVarEnv) tv_eqs - (feqs_out, feqs_in) = foldFunEqs (kick_out_eqs extend_fun_eqs) - funeqmap ([], emptyFunEqs) - (dicts_out, dicts_in) = partitionDicts kick_out_ct dictmap - (irs_out, irs_in) = partitionBag kick_out_ct irreds + (tv_eqs_out, tv_eqs_in) = partitionInertEqs kick_out_eq tv_eqs + (feqs_out, feqs_in) = partitionFunEqs kick_out_eq funeqmap + (dicts_out, dicts_in) = partitionDicts kick_out_ct dictmap + (irs_out, irs_in) = partitionBag kick_out_ct irreds -- Kick out even insolubles: See Note [Rewrite insolubles] -- Of course we must kick out irreducibles like (c a), in case -- we can rewrite 'c' to something more useful @@ -1343,8 +1342,7 @@ kickOutRewritableLHS new_fr new_lhs fr_tv_can_rewrite_ty :: TyVar -> EqRel -> Type -> Bool fr_tv_can_rewrite_ty new_tv role ty - = anyRewritableTyVar True role can_rewrite ty - -- True: ignore casts and coercions + = anyRewritableTyVar role can_rewrite ty where can_rewrite :: EqRel -> TyVar -> Bool can_rewrite old_role tv = new_role `eqCanRewrite` old_role && tv == new_tv @@ -1367,7 +1365,7 @@ kickOutRewritableLHS new_fr new_lhs TyFamLHS new_tf new_tf_args -> fr_tf_can_rewrite_ty new_tf new_tf_args fr_may_rewrite :: CtFlavourRole -> Bool - fr_may_rewrite fs = new_fr `eqMayRewriteFR` fs + 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 @@ -1383,28 +1381,8 @@ kickOutRewritableLHS new_fr new_lhs fr_may_rewrite fs && fr_tf_can_rewrite_ty new_tf new_tf_args role (ctPred ct) - extend_tv_eqs :: InertEqs -> CanEqLHS -> EqualCtList -> InertEqs - extend_tv_eqs eqs (TyVarLHS tv) cts = extendDVarEnv eqs tv cts - extend_tv_eqs eqs other _cts = pprPanic "extend_tv_eqs" (ppr eqs $$ ppr other) - - extend_fun_eqs :: FunEqMap EqualCtList -> CanEqLHS -> EqualCtList - -> FunEqMap EqualCtList - extend_fun_eqs eqs (TyFamLHS fam_tc fam_args) cts - = insertTcApp eqs fam_tc fam_args cts - extend_fun_eqs eqs other _cts = pprPanic "extend_fun_eqs" (ppr eqs $$ ppr other) - - kick_out_eqs :: (container -> CanEqLHS -> EqualCtList -> container) - -> EqualCtList -> ([Ct], container) - -> ([Ct], container) - kick_out_eqs extend eqs (acc_out, acc_in) - = (eqs_out `chkAppend` acc_out, case listToEqualCtList eqs_in of - Nothing -> acc_in - Just eqs_in_ecl@(EqualCtList (eq1 :| _)) - -> extend acc_in (cc_lhs eq1) eqs_in_ecl) - where - (eqs_out, eqs_in) = partition kick_out_eq (equalCtListToList eqs) - -- Implements criteria K1-K3 in Note [Extending the inert equalities] + kick_out_eq :: Ct -> Bool kick_out_eq (CEqCan { cc_lhs = lhs, cc_rhs = rhs_ty , cc_ev = ev, cc_eq_rel = eq_rel }) | not (fr_may_rewrite fs) @@ -1413,7 +1391,7 @@ kickOutRewritableLHS new_fr new_lhs -- Below here (fr_may_rewrite fs) is True | TyVarLHS _ <- lhs - , fs `eqMayRewriteFR` new_fr + , fs `eqCanRewriteFR` new_fr = False -- (K4) Keep it in the inert set if the LHS is a tyvar and -- it can rewrite the work item. See Note [K4] @@ -1429,7 +1407,7 @@ kickOutRewritableLHS new_fr new_lhs where fs = (ctEvFlavour ev, eq_rel) kick_out_for_inertness - = (fs `eqMayRewriteFR` fs) -- (K2a) + = (fs `eqCanRewriteFR` fs) -- (K2a) && fr_can_rewrite_ty eq_rel rhs_ty -- (K2b) kick_out_for_completeness -- (K3) and Note [K3: completeness of solving] @@ -1437,7 +1415,7 @@ kickOutRewritableLHS new_fr new_lhs NomEq -> rhs_ty `eqType` canEqLHSType new_lhs -- (K3a) ReprEq -> is_can_eq_lhs_head new_lhs rhs_ty -- (K3b) - kick_out_eq ct = pprPanic "keep_eq" (ppr ct) + kick_out_eq ct = pprPanic "kick_out_eq" (ppr ct) is_can_eq_lhs_head (TyVarLHS tv) = go where @@ -1480,9 +1458,6 @@ new equality, to maintain the inert-set invariants. kick out constraints that mention type variables whose kinds contain this LHS! - - A Derived equality can kick out [D] constraints in inert_eqs, - inert_dicts, inert_irreds etc. - - We don't kick out constraints from inert_solved_dicts, and inert_solved_funeqs optimistically. But when we lookup we have to take the substitution into account diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs index 36e9afae98..b753a3c902 100644 --- a/compiler/GHC/Tc/Solver/Interact.hs +++ b/compiler/GHC/Tc/Solver/Interact.hs @@ -4,7 +4,7 @@ module GHC.Tc.Solver.Interact ( solveSimpleGivens, -- Solves [Ct] - solveSimpleWanteds, -- Solves Cts + solveSimpleWanteds -- Solves Cts ) where import GHC.Prelude @@ -31,7 +31,6 @@ import GHC.Core.Unify ( tcUnifyTyWithTFs, ruleMatchTyKiX ) import GHC.Tc.Types.Evidence import GHC.Utils.Outputable import GHC.Utils.Panic -import GHC.Utils.Panic.Plain import GHC.Tc.Types import GHC.Tc.Types.Constraint @@ -45,17 +44,18 @@ import GHC.Data.Bag import GHC.Utils.Monad ( concatMapM, foldlM ) import GHC.Core -import Data.List( partition, deleteFirstsBy ) +import Data.List( deleteFirstsBy ) +import Data.Function ( on ) import GHC.Types.SrcLoc import GHC.Types.Var.Env +import qualified Data.Semigroup as S import Control.Monad import GHC.Data.Pair (Pair(..)) import GHC.Types.Unique( hasKey ) import GHC.Driver.Session import GHC.Utils.Misc import qualified GHC.LanguageExtensions as LangExt -import Data.List.NonEmpty ( NonEmpty(..) ) import Control.Monad.Trans.Class import Control.Monad.Trans.Maybe @@ -187,9 +187,9 @@ runTcPluginsGiven ; if null solvers then return [] else do { givens <- getInertGivens ; if null givens then return [] else - do { p <- runTcPluginSolvers solvers (givens,[],[]) - ; let (solved_givens, _, _) = pluginSolvedCts p - insols = pluginBadCts p + do { p <- runTcPluginSolvers solvers (givens,[]) + ; let (solved_givens, _) = pluginSolvedCts p + insols = pluginBadCts p ; updInertCans (removeInertCts solved_givens) ; updInertIrreds (\irreds -> extendCtsList irreds insols) ; return (pluginNewCts p) } } } @@ -208,22 +208,20 @@ runTcPluginsWanted wc@(WC { wc_simple = simples1 }) ; if null solvers then return (False, wc) else do { given <- getInertGivens - ; simples1 <- zonkSimples simples1 -- Plugin requires zonked inputs - ; let (wanted, derived) = partition isWantedCt (bagToList simples1) - ; p <- runTcPluginSolvers solvers (given, derived, wanted) - ; let (_, _, solved_wanted) = pluginSolvedCts p - (_, unsolved_derived, unsolved_wanted) = pluginInputCts p + ; wanted <- zonkSimples simples1 -- Plugin requires zonked inputs + ; p <- runTcPluginSolvers solvers (given, bagToList wanted) + ; let (_, solved_wanted) = pluginSolvedCts p + (_, unsolved_wanted) = pluginInputCts p new_wanted = pluginNewCts p insols = pluginBadCts p -- SLPJ: I'm deeply suspicious of this --- ; updInertCans (removeInertCts $ solved_givens ++ solved_deriveds) +-- ; updInertCans (removeInertCts $ solved_givens) ; mapM_ setEv solved_wanted ; return ( notNull (pluginNewCts p) , wc { wc_simple = listToBag new_wanted `andCts` listToBag unsolved_wanted `andCts` - listToBag unsolved_derived `andCts` listToBag insols } ) } } where setEv :: (EvTerm,Ct) -> TcS () @@ -231,11 +229,11 @@ runTcPluginsWanted wc@(WC { wc_simple = simples1 }) CtWanted { ctev_dest = dest } -> setWantedEvTerm dest ev _ -> panic "runTcPluginsWanted.setEv: attempt to solve non-wanted!" --- | A triple of (given, derived, wanted) constraints to pass to plugins -type SplitCts = ([Ct], [Ct], [Ct]) +-- | A pair of (given, wanted) constraints to pass to plugins +type SplitCts = ([Ct], [Ct]) --- | A solved triple of constraints, with evidence for wanteds -type SolvedCts = ([Ct], [Ct], [(EvTerm,Ct)]) +-- | A solved pair of constraints, with evidence for wanteds +type SolvedCts = ([Ct], [(EvTerm,Ct)]) -- | Represents collections of constraints generated by typechecker -- plugins @@ -255,7 +253,7 @@ getTcPluginSolvers :: TcS [TcPluginSolver] getTcPluginSolvers = do { tcg_env <- getGblEnv; return (tcg_tc_plugin_solvers tcg_env) } --- | Starting from a triple of (given, derived, wanted) constraints, +-- | Starting from a pair of (given, wanted) constraints, -- invoke each of the typechecker constraint-solving plugins in turn and return -- -- * the remaining unmodified constraints, @@ -274,7 +272,7 @@ runTcPluginSolvers solvers all_cts where do_plugin :: TcPluginProgress -> TcPluginSolver -> TcS TcPluginProgress do_plugin p solver = do - result <- runTcPluginTcS (uncurry3 solver (pluginInputCts p)) + result <- runTcPluginTcS (uncurry solver (pluginInputCts p)) return $ progress p result progress :: TcPluginProgress -> TcPluginSolveResult -> TcPluginProgress @@ -291,11 +289,11 @@ runTcPluginSolvers solvers all_cts , pluginBadCts = bad_cts ++ pluginBadCts p } - initialProgress = TcPluginProgress all_cts ([], [], []) [] [] + initialProgress = TcPluginProgress all_cts ([], []) [] [] discard :: [Ct] -> SplitCts -> SplitCts - discard cts (xs, ys, zs) = - (xs `without` cts, ys `without` cts, zs `without` cts) + discard cts (xs, ys) = + (xs `without` cts, ys `without` cts) without :: [Ct] -> [Ct] -> [Ct] without = deleteFirstsBy eqCt @@ -308,10 +306,9 @@ runTcPluginSolvers solvers all_cts add xs scs = foldl' addOne scs xs addOne :: SolvedCts -> (EvTerm,Ct) -> SolvedCts - addOne (givens, deriveds, wanteds) (ev,ct) = case ctEvidence ct of - CtGiven {} -> (ct:givens, deriveds, wanteds) - CtDerived{} -> (givens, ct:deriveds, wanteds) - CtWanted {} -> (givens, deriveds, (ev,ct):wanteds) + addOne (givens, wanteds) (ev,ct) = case ctEvidence ct of + CtGiven {} -> (ct:givens, wanteds) + CtWanted {} -> (givens, (ev,ct):wanteds) type WorkItem = Ct @@ -414,7 +411,7 @@ It *is* true that [Solver Invariant] then the inert item must Given or, equivalently, If the work-item is Given, - and the inert item is Wanted/Derived + and the inert item is Wanted then there is no reaction -} @@ -441,30 +438,10 @@ data InteractResult -- (if the latter is Wanted; just discard it if not) | KeepWork -- Keep the work item, and solve the inert item from it - | KeepBoth -- See Note [KeepBoth] - instance Outputable InteractResult where - ppr KeepBoth = text "keep both" ppr KeepInert = text "keep inert" ppr KeepWork = text "keep work-item" -{- Note [KeepBoth] -~~~~~~~~~~~~~~~~~~ -Consider - Inert: [WD] C ty1 ty2 - Work item: [D] C ty1 ty2 - -Here we can simply drop the work item. But what about - Inert: [W] C ty1 ty2 - Work item: [D] C ty1 ty2 - -Here we /cannot/ drop the work item, becuase we lose the [D] form, and -that is essential for e.g. fundeps, see isImprovable. We could zap -the inert item to [WD], but the simplest thing to do is simply to keep -both. (They probably started as [WD] and got split; this is relatively -rare and it doesn't seem worth trying to put them back together again.) --} - solveOneFromTheOther :: CtEvidence -- Inert (Dict or Irred) -> CtEvidence -- WorkItem (same predicate as inert) -> TcS InteractResult @@ -477,37 +454,22 @@ solveOneFromTheOther :: CtEvidence -- Inert (Dict or Irred) -- two wanteds into one by solving one from the other solveOneFromTheOther ev_i ev_w - | CtDerived {} <- ev_w -- Work item is Derived - = case ev_i of - CtWanted { ctev_nosh = WOnly } -> return KeepBoth - _ -> return KeepInert - - | CtDerived {} <- ev_i -- Inert item is Derived - = case ev_w of - CtWanted { ctev_nosh = WOnly } -> return KeepBoth - _ -> return KeepWork - -- The ev_w is inert wrt earlier inert-set items, - -- so it's safe to continue on from this point - - -- After this, neither ev_i or ev_w are Derived | CtWanted { ctev_loc = loc_w } <- ev_w , prohibitedSuperClassSolve loc_i loc_w = -- inert must be Given do { traceTcS "prohibitedClassSolve1" (ppr ev_i $$ ppr ev_w) ; return KeepWork } - | CtWanted { ctev_nosh = nosh_w } <- ev_w + | CtWanted {} <- ev_w -- Inert is Given or Wanted - = case ev_i of - CtWanted { ctev_nosh = WOnly } - | WDeriv <- nosh_w -> return KeepWork - _ -> return KeepInert - -- Consider work item [WD] C ty1 ty2 - -- inert item [W] C ty1 ty2 - -- Then we must keep the work item. But if the - -- work item was [W] C ty1 ty2 - -- then we are free to discard the work item in favour of inert - -- Remember, no Deriveds at this point + = return $ case ev_i of + CtWanted {} -> choose_better_loc + -- both are Wanted; choice of which to keep is + -- arbitrary. So we look at the context to choose + -- which would make a better error message + + _ -> KeepInert + -- work is Wanted; inert is Given: easy choice. -- From here on the work-item is Given @@ -536,6 +498,27 @@ solveOneFromTheOther ev_i ev_w lvl_i = ctLocLevel loc_i lvl_w = ctLocLevel loc_w + choose_better_loc + -- if only one is a WantedSuperclassOrigin (arising from expanding + -- a Wanted class constraint), keep the other: wanted superclasses + -- may be unexpected by users + | is_wanted_superclass_loc loc_i + , not (is_wanted_superclass_loc loc_w) = KeepWork + + | not (is_wanted_superclass_loc loc_i) + , is_wanted_superclass_loc loc_w = KeepInert + + -- otherwise, just choose the lower span + -- reason: if we have something like (abs 1) (where the + -- Num constraint cannot be satisfied), it's better to + -- get an error about abs than about 1. + -- This test might become more elaborate if we see an + -- opportunity to improve the error messages + | ((<) `on` ctLocSpan) loc_i loc_w = KeepInert + | otherwise = KeepWork + + is_wanted_superclass_loc = isWantedSuperclassOrigin . ctLocOrigin + different_level_strategy -- Both Given | isIPLikePred pred = if lvl_w > lvl_i then KeepWork else KeepInert | otherwise = if lvl_w > lvl_i then KeepInert else KeepWork @@ -666,8 +649,6 @@ interactIrred inerts workItem@(CIrredCan { cc_ev = ev_w, cc_reason = reason }) -- For insolubles, don't allow the constraint to be dropped -- which can happen with solveOneFromTheOther, so that -- we get distinct error messages with -fdefer-type-errors - -- See Note [Do not add duplicate derived insolubles] - , not (isDroppableCt workItem) = continueWith workItem | let (matching_irreds, others) = findMatchingIrreds (inert_irreds inerts) ev_w @@ -677,7 +658,6 @@ interactIrred inerts workItem@(CIrredCan { cc_ev = ev_w, cc_reason = reason }) = do { what_next <- solveOneFromTheOther ev_i ev_w ; traceTcS "iteractIrred" (ppr workItem $$ ppr what_next $$ ppr ct_i) ; case what_next of - KeepBoth -> continueWith workItem KeepInert -> do { setEvBindIfWanted ev_w (swap_me swap ev_i) ; return (Stop ev_w (text "Irred equal" <+> parens (ppr what_next))) } KeepWork -> do { setEvBindIfWanted ev_i (swap_me swap ev_w) @@ -736,56 +716,6 @@ irreducible constraints to look for an identical one. When doing this lookup, findMatchingIrreds spots the equality case, and matches either way around. It has to return a swap-flag so we can generate evidence that is the right way round too. - -Note [Do not add duplicate derived insolubles] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -In general we *must* add an insoluble (Int ~ Bool) even if there is -one such there already, because they may come from distinct call -sites. Not only do we want an error message for each, but with --fdefer-type-errors we must generate evidence for each. But for -*derived* insolubles, we only want to report each one once. Why? - -(a) A constraint (C r s t) where r -> s, say, may generate the same fundep - equality many times, as the original constraint is successively rewritten. - -(b) Ditto the successive iterations of the main solver itself, as it traverses - the constraint tree. See example below. - -Also for *given* insolubles we may get repeated errors, as we -repeatedly traverse the constraint tree. These are relatively rare -anyway, so removing duplicates seems ok. (Alternatively we could take -the SrcLoc into account.) - -Note that the test does not need to be particularly efficient because -it is only used if the program has a type error anyway. - -Example of (b): assume a top-level class and instance declaration: - - class D a b | a -> b - instance D [a] [a] - -Assume we have started with an implication: - - forall c. Eq c => { wc_simple = [W] D [c] c } - -which we have simplified to, with a Derived constraing coming from -D's functional dependency: - - forall c. Eq c => { wc_simple = [W] D [c] c [W] - [D] (c ~ [c]) } - -When iterating the solver, we might try to re-solve this -implication. If we do not do a dropDerivedWC, then we will end up -trying to solve the following constraints the second time: - - [W] (D [c] c) - [D] (c ~ [c]) - -which will result in two Deriveds to end up in the insoluble set: - - wc_simple = [W] D [c] c - [D] (c ~ [c]) - [D] (c ~ [c]) -} {- @@ -1000,6 +930,68 @@ Passing along the solved_dicts important for two reasons: and to solve G2 we may need H. If we don't spot this sharing we may solve H twice; and if this pattern repeats we may get exponentially bad behaviour. + +Note [No Given/Given fundeps] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We do not create constraints from: +* Given/Given interactions via functional dependencies or type family + injectivity annotations. +* Given/instance fundep interactions via functional dependencies or + type family injectivity annotations. + +In this Note, all these interactions are called just "fundeps". + +We ingore such fundeps for several reasons: + +1. These fundeps will never serve a purpose in accepting more + programs: Given constraints do not contain metavariables that could + be unified via exploring fundeps. They *could* be useful in + discovering inaccessible code. However, the constraints will be + Wanteds, and as such will cause errors (not just warnings) if they + go unsolved. Maybe there is a clever way to get the right + inaccessible code warnings, but the path forward is far from + clear. #12466 has further commentary. + +2. Furthermore, here is a case where a Given/instance interaction is actively + harmful (from dependent/should_compile/RaeJobTalk): + + type family a == b :: Bool + type family Not a = r | r -> a where + Not False = True + Not True = False + + [G] Not (a == b) ~ True + + Reacting this Given with the equations for Not produces + + [W] a == b ~ False + + This is indeed a true consequence, and would make sense as a fresh Given. + But we don't have a way to produce evidence for fundeps, as a Wanted it + is /harmful/: we can't prove it, and so we'll report an error and reject + the program. (Previously fundeps gave rise to Deriveds, which + carried no evidence, so it didn't matter that they could not be proved.) + +3. #20922 showed a subtle different problem with Given/instance fundeps. + type family ZipCons (as :: [k]) (bssx :: [[k]]) = (r :: [[k]]) | r -> as bssx where + ZipCons (a ': as) (bs ': bss) = (a ': bs) ': ZipCons as bss + ... + + tclevel = 4 + [G] ZipCons is1 iss ~ (i : is2) : jss + + (The tclevel=4 means that this Given is at level 4.) The fundep tells us that + 'iss' must be of form (is2 : beta[4]) where beta[4] is a fresh unification + variable; we don't know what type it stands for. So we would emit + [W] iss ~ is2 : beta + + Again we can't prove that equality; and worse we'll rewrite iss to + (is2:beta) in deeply nested contraints inside this implication, + where beta is untouchable (under other equality constraints), leading + to other insoluble constraints. + +The bottom line: since we have no evidence for them, we should ignore Given/Given +and Given/instance fundeps entirely. -} interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct) @@ -1020,7 +1012,6 @@ interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs what_next <- solveOneFromTheOther ev_i ev_w ; traceTcS "lookupInertDict" (ppr what_next) ; case what_next of - KeepBoth -> continueWith workItem KeepInert -> do { setEvBindIfWanted ev_w (ctEvTerm ev_i) ; return $ Stop ev_w (text "Dict equal" <+> parens (ppr what_next)) } KeepWork -> do { setEvBindIfWanted ev_i (ctEvTerm ev_w) @@ -1109,7 +1100,7 @@ shortCutSolver dflags ev_w ev_i ; lift $ checkReductionDepth loc' pred - ; evc_vs <- mapM (new_wanted_cached loc' solved_dicts') preds + ; evc_vs <- mapM (new_wanted_cached ev loc' solved_dicts') preds -- Emit work for subgoals but use our local cache -- so we can solve recursive dictionaries. @@ -1128,50 +1119,45 @@ shortCutSolver dflags ev_w ev_i -- Use a local cache of solved dicts while emitting EvVars for new work -- We bail out of the entire computation if we need to emit an EvVar for -- a subgoal that isn't a ClassPred. - new_wanted_cached :: CtLoc -> DictMap CtEvidence -> TcPredType -> MaybeT TcS MaybeNew - new_wanted_cached loc cache pty + new_wanted_cached :: CtEvidence -> CtLoc + -> DictMap CtEvidence -> TcPredType -> MaybeT TcS MaybeNew + new_wanted_cached ev_w loc cache pty | ClassPred cls tys <- classifyPredType pty = lift $ case findDict cache loc_w cls tys of Just ctev -> return $ Cached (ctEvExpr ctev) - Nothing -> Fresh <$> newWantedNC loc pty + Nothing -> Fresh <$> newWantedNC loc (ctEvRewriters ev_w) pty | otherwise = mzero addFunDepWork :: InertCans -> CtEvidence -> Class -> TcS () --- Add derived constraints from type-class functional dependencies. +-- Add wanted constraints from type-class functional dependencies. addFunDepWork inerts work_ev cls - | isImprovable work_ev = 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) - | otherwise - = return () where work_pred = ctEvPred work_ev work_loc = ctEvLoc work_ev add_fds inert_ct - | isImprovable inert_ev = 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) ]) ; + , pprCtLoc derived_loc, ppr (isGivenLoc derived_loc) ]) - emitFunDepDeriveds $ - improveFromAnother derived_loc inert_pred work_pred + ; 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 - -- NB: We do create FDs for given to report insoluble equations that arise - -- from pairs of Givens, and also because of floating when we approximate - -- implications. The relevant test is: typecheck/should_fail/FDsFromGivens.hs + -- Do not create FDs from Given/Given interactions: See Note [No Given/Given fundeps] } - | otherwise - = return () 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 @@ -1281,24 +1267,22 @@ I can think of two ways to fix this: improveLocalFunEqs :: CtEvidence -> InertCans -> TyCon -> [TcType] -> TcType -> TcS () --- Generate derived improvement equalities, by comparing +-- Generate improvement equalities, by comparing -- the current work item with inert CFunEqs --- E.g. x + y ~ z, x + y' ~ z => [D] y ~ y' +-- E.g. x + y ~ z, x + y' ~ z => [W] y ~ y' -- -- See Note [FunDep and implicit parameter reactions] --- Precondition: isImprovable work_ev improveLocalFunEqs work_ev inerts fam_tc args rhs - = assert (isImprovable work_ev) $ - unless (null improvement_eqns) $ + = unless (null improvement_eqns) $ do { traceTcS "interactFunEq improvements: " $ vcat [ text "Eqns:" <+> ppr improvement_eqns , text "Candidates:" <+> ppr funeqs_for_tc , text "Inert eqs:" <+> ppr (inert_eqs inerts) ] - ; emitFunDepDeriveds improvement_eqns } + ; emitFunDepWanteds (ctEvRewriters work_ev) improvement_eqns } where funeqs = inert_funeqs inerts - funeqs_for_tc = [ funeq_ct | EqualCtList (funeq_ct :| _) - <- findFunEqsByTyCon funeqs fam_tc + funeqs_for_tc = [ funeq_ct | equal_ct_list <- findFunEqsByTyCon funeqs fam_tc + , funeq_ct <- equal_ct_list , NomEq == ctEqRel funeq_ct ] -- representational equalities don't interact -- with type family dependencies @@ -1307,7 +1291,7 @@ improveLocalFunEqs work_ev inerts fam_tc args rhs fam_inj_info = tyConInjectivityInfo fam_tc -------------------- - improvement_eqns :: [FunDepEqn CtLoc] + improvement_eqns :: [FunDepEqn (CtLoc, RewriterSet)] improvement_eqns | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc = -- Try built-in families, notably for arithmethic @@ -1322,15 +1306,19 @@ improveLocalFunEqs work_ev inerts fam_tc args rhs -------------------- do_one_built_in ops rhs (CEqCan { cc_lhs = TyFamLHS _ iargs, cc_rhs = irhs, cc_ev = inert_ev }) + | not (isGiven inert_ev && isGiven work_ev) -- See Note [No Given/Given fundeps] = mk_fd_eqns inert_ev (sfInteractInert ops args rhs iargs irhs) + | otherwise + = [] + do_one_built_in _ _ _ = pprPanic "interactFunEq 1" (ppr fam_tc) -------------------- -- See Note [Type inference for type families with injectivity] do_one_injective inj_args rhs (CEqCan { cc_lhs = TyFamLHS _ inert_args , cc_rhs = irhs, cc_ev = inert_ev }) - | isImprovable inert_ev + | not (isGiven inert_ev && isGiven work_ev) -- See Note [No Given/Given fundeps] , rhs `tcEqType` irhs = mk_fd_eqns inert_ev $ [ Pair arg iarg | (arg, iarg, True) <- zip3 args inert_args inj_args ] @@ -1340,17 +1328,25 @@ improveLocalFunEqs work_ev inerts fam_tc args rhs do_one_injective _ _ _ = pprPanic "interactFunEq 2" (ppr fam_tc) -------------------- - mk_fd_eqns :: CtEvidence -> [TypeEqn] -> [FunDepEqn CtLoc] + mk_fd_eqns :: CtEvidence -> [TypeEqn] -> [FunDepEqn (CtLoc, RewriterSet)] mk_fd_eqns inert_ev eqns | null eqns = [] | otherwise = [ FDEqn { fd_qtvs = [], fd_eqs = eqns , fd_pred1 = work_pred - , fd_pred2 = ctEvPred inert_ev - , fd_loc = loc } ] + , fd_pred2 = inert_pred + , fd_loc = (loc, inert_rewriters) } ] where - inert_loc = ctEvLoc inert_ev - loc = inert_loc { ctl_depth = ctl_depth inert_loc `maxSubGoalDepth` - ctl_depth work_loc } + initial_loc -- start with the location of the Wanted involved + | isGiven work_ev = inert_loc + | otherwise = work_loc + eqn_orig = InjTFOrigin1 work_pred (ctLocOrigin work_loc) (ctLocSpan work_loc) + inert_pred (ctLocOrigin inert_loc) (ctLocSpan inert_loc) + eqn_loc = setCtLocOrigin initial_loc eqn_orig + inert_pred = ctEvPred inert_ev + inert_loc = ctEvLoc inert_ev + inert_rewriters = ctEvRewriters inert_ev + loc = eqn_loc { ctl_depth = ctl_depth inert_loc `maxSubGoalDepth` + ctl_depth work_loc } {- Note [Type inference for type families with injectivity] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1358,9 +1354,9 @@ Suppose we have a type family with an injectivity annotation: type family F a b = r | r -> b Then if we have an equality like F s1 t1 ~ F s2 t2, -we can use the injectivity to get a new Derived constraint on +we can use the injectivity to get a new Wanted constraint on the injective argument - [D] t1 ~ t2 + [W] t1 ~ t2 That in turn can help GHC solve constraints that would otherwise require guessing. For example, consider the ambiguity check for @@ -1380,15 +1376,15 @@ of the matching equation. For closed type families we have to perform additional apartness check for the selected equation to check that the selected is guaranteed to fire for given LHS arguments. -These new constraints are simply *Derived* constraints; they have no evidence. +These new constraints are Wanted constraints, but we will not use the evidence. We could go further and offer evidence from decomposing injective type-function applications, but that would require new evidence forms, and an extension to FC, so we don't do that right now (Dec 14). -We generate these Deriveds in three places, depending on how we notice the +We generate these Wanteds in three places, depending on how we notice the injectivity. -1. When we have a [W/D] F tys1 ~ F tys2. This is handled in canEqCanLHS2, and +1. When we have a [W] F tys1 ~ F tys2. This is handled in canEqCanLHS2, and described in Note [Decomposing equality] in GHC.Tc.Solver.Canonical. 2. When we have [W] F tys1 ~ T and [W] F tys2 ~ T. Note that neither of these @@ -1455,10 +1451,7 @@ But it's not so simple: * We can only do g2 := g1 if g1 can discharge g2; that depends on (a) the role and (b) the flavour. E.g. a representational equality cannot discharge a nominal one; a Wanted cannot discharge a Given. - The predicate is eqCanDischargeFR. - -* If the inert is [W] and the work-item is [WD] we don't want to - forget the [D] part; hence the Bool result of inertsCanDischarge. + The predicate is eqCanRewriteFR. * Visibility. Suppose S :: forall k. k -> Type, and consider unifying S @Type (a::Type) ~ S @(Type->Type) (b::Type->Type) @@ -1479,9 +1472,7 @@ But it's not so simple: inertsCanDischarge :: InertCans -> Ct -> Maybe ( CtEvidence -- The evidence for the inert - , SwapFlag -- Whether we need mkSymCo - , Bool) -- True <=> keep a [D] version - -- of the [WD] constraint + , SwapFlag ) -- Whether we need mkSymCo inertsCanDischarge inerts (CEqCan { cc_lhs = lhs_w, cc_rhs = rhs_w , cc_ev = ev_w, cc_eq_rel = eq_rel }) | (ev_i : _) <- [ ev_i | CEqCan { cc_ev = ev_i, cc_rhs = rhs_i @@ -1491,7 +1482,7 @@ inertsCanDischarge inerts (CEqCan { cc_lhs = lhs_w, cc_rhs = rhs_w , inert_beats_wanted ev_i eq_rel ] = -- Inert: a ~ ty -- Work item: a ~ ty - Just (ev_i, NotSwapped, keep_deriv ev_i) + Just (ev_i, NotSwapped) | Just rhs_lhs <- canEqLHS_maybe rhs_w , (ev_i : _) <- [ ev_i | CEqCan { cc_ev = ev_i, cc_rhs = rhs_i @@ -1501,7 +1492,7 @@ inertsCanDischarge inerts (CEqCan { cc_lhs = lhs_w, cc_rhs = rhs_w , inert_beats_wanted ev_i eq_rel ] = -- Inert: a ~ b -- Work item: b ~ a - Just (ev_i, IsSwapped, keep_deriv ev_i) + Just (ev_i, IsSwapped) where loc_w = ctEvLoc ev_w @@ -1509,22 +1500,14 @@ inertsCanDischarge inerts (CEqCan { cc_lhs = lhs_w, cc_rhs = rhs_w fr_w = (flav_w, eq_rel) inert_beats_wanted ev_i eq_rel - = -- eqCanDischargeFR: see second bullet of Note [Combining equalities] + = -- eqCanRewriteFR: see second bullet of Note [Combining equalities] -- strictly_more_visible: see last bullet of Note [Combining equalities] - fr_i`eqCanDischargeFR` fr_w + fr_i `eqCanRewriteFR` fr_w && not ((loc_w `strictly_more_visible` ctEvLoc ev_i) - && (fr_w `eqCanDischargeFR` fr_i)) + && (fr_w `eqCanRewriteFR` fr_i)) where fr_i = (ctEvFlavour ev_i, eq_rel) - -- See Note [Combining equalities], third bullet - keep_deriv ev_i - | Wanted WOnly <- ctEvFlavour ev_i -- inert is [W] - , Wanted WDeriv <- flav_w -- work item is [WD] - = True -- Keep a derived version of the work item - | otherwise - = False -- Work item is fully discharged - -- See Note [Combining equalities], final bullet strictly_more_visible loc1 loc2 = not (isVisibleOrigin (ctLocOrigin loc2)) && @@ -1538,20 +1521,13 @@ interactEq inerts workItem@(CEqCan { cc_lhs = lhs , cc_rhs = rhs , cc_ev = ev , cc_eq_rel = eq_rel }) - | Just (ev_i, swapped, keep_deriv) <- inertsCanDischarge inerts workItem + | Just (ev_i, swapped) <- inertsCanDischarge inerts workItem = do { setEvBindIfWanted ev $ evCoercion (maybeTcSymCo swapped $ tcDowngradeRole (eqRelRole eq_rel) (ctEvRole ev_i) (ctEvCoercion ev_i)) - ; let deriv_ev = CtDerived { ctev_pred = ctEvPred ev - , ctev_loc = ctEvLoc ev } - ; when keep_deriv $ - emitWork [workItem { cc_ev = deriv_ev }] - -- As a Derived it might not be fully rewritten, - -- so we emit it as new work - ; stopWith ev "Solved from inert" } | ReprEq <- eq_rel -- See Note [Do not unify representational equalities] @@ -1562,9 +1538,7 @@ interactEq inerts workItem@(CEqCan { cc_lhs = lhs = case lhs of TyVarLHS tv -> tryToSolveByUnification workItem ev tv rhs - TyFamLHS tc args -> do { when (isImprovable ev) $ - -- Try improvement, if possible - improveLocalFunEqs ev inerts tc args rhs + TyFamLHS tc args -> do { improveLocalFunEqs ev inerts tc args rhs ; continueWith workItem } interactEq _ wi = pprPanic "interactEq" (ppr wi) @@ -1597,7 +1571,7 @@ tryToSolveByUnification work_item ev tv rhs solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS (StopOrContinue Ct) -- Solve with the identity coercion -- Precondition: kind(xi) equals kind(tv) --- Precondition: CtEvidence is Wanted or Derived +-- Precondition: CtEvidence is Wanted -- Precondition: CtEvidence is nominal -- Returns: workItem where -- workItem = the new Given constraint @@ -1710,7 +1684,7 @@ Note [FunDep and implicit parameter reactions] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Currently, our story of interacting two dictionaries (or a dictionary and top-level instances) for functional dependencies, and implicit -parameters, is that we simply produce new Derived equalities. So for example +parameters, is that we simply produce new Wanted equalities. So for example class D a b | a -> b where ... Inert: @@ -1719,7 +1693,7 @@ parameters, is that we simply produce new Derived equalities. So for example d2 :w D Int alpha We generate the extra work item - cv :d alpha ~ Bool + cv :w alpha ~ Bool where 'cv' is currently unused. However, this new item can perhaps be spontaneously solved to become given and react with d2, discharging it in favour of a new constraint d2' thus: @@ -1728,10 +1702,9 @@ parameters, is that we simply produce new Derived equalities. So for example Now d2' can be discharged from d1 We could be more aggressive and try to *immediately* solve the dictionary -using those extra equalities, but that requires those equalities to carry -evidence and derived do not carry evidence. +using those extra equalities. -If that were the case with the same inert set and work item we might dischard +If that were the case with the same inert set and work item we might discard d2 directly: cv :w alpha ~ Bool @@ -1756,10 +1729,10 @@ It's exactly the same with implicit parameters, except that the Note [Fundeps with instances] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ doTopFundepImprovement compares the constraint with all the instance -declarations, to see if we can produce any derived equalities. E.g +declarations, to see if we can produce any equalities. E.g class C2 a b | a -> b instance C Int Bool -Then the constraint (C Int ty) generates the Derived equality [D] ty ~ Bool. +Then the constraint (C Int ty) generates the equality [W] ty ~ Bool. There is a nasty corner in #19415 which led to the typechecker looping: class C s t b | s -> t @@ -1769,9 +1742,9 @@ 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 ==> {fundeps against instance; k0, y0 fresh unification vars} - [D] T kb0 (b0::kb0) ~ T k0 (y0::k0) + [W] T kb0 (b0::kb0) ~ T k0 (y0::k0) Add dwrk to inert set - ==> {solve that Derived kb0 := k0, b0 := y0 + ==> {solve that equality kb0 := k0, b0 := y0 Now kick out dwrk, since it mentions kb0 But now we are back to the start! Loop! @@ -1791,7 +1764,7 @@ is very simple: a) The class has fundeps b) We have not had a successful hit against instances yet -* In doTopFundepImprovement, if we emit some Deriveds we flip the flag +* In doTopFundepImprovement, if we emit some constraints we flip the flag to False, so that we won't try again with the same CDictCan. In our example, dwrk will have its flag set to False. @@ -1828,8 +1801,8 @@ The two instances don't actually conflict on their fundeps, although it's pretty strange. So they are both accepted. Now try [W] GHet (K Int) (K Bool) This triggers fundeps from both instance decls; - [D] K Bool ~ K [a] - [D] K Bool ~ K beta + [W] K Bool ~ K [a] + [W] K Bool ~ K beta And there's a risk of complaining about Bool ~ [a]. But in fact the Wanted matches the second instance, so we never get as far as the fundeps. @@ -1837,7 +1810,7 @@ as the fundeps. #7875 is a case in point. -} -doTopFundepImprovement ::Ct -> TcS (StopOrContinue Ct) +doTopFundepImprovement :: Ct -> TcS (StopOrContinue Ct) -- Try to functional-dependency improvement betweeen the constraint -- and the top-level instance declarations -- See Note [Fundeps with instances] @@ -1845,13 +1818,13 @@ doTopFundepImprovement ::Ct -> TcS (StopOrContinue Ct) doTopFundepImprovement work_item@(CDictCan { cc_ev = ev, cc_class = cls , cc_tyargs = xis , cc_fundeps = has_fds }) - | has_fds, isImprovable ev + | has_fds = do { traceTcS "try_fundeps" (ppr work_item) ; instEnvs <- getInstEnvs ; let fundep_eqns = improveFromInstEnv instEnvs mk_ct_loc cls xis ; case fundep_eqns of [] -> continueWith work_item -- No improvement - _ -> do { emitFunDepDeriveds fundep_eqns + _ -> do { emitFunDepWanteds (ctEvRewriters ev) fundep_eqns ; continueWith (work_item { cc_fundeps = False }) } } | otherwise = continueWith work_item @@ -1863,30 +1836,38 @@ doTopFundepImprovement work_item@(CDictCan { cc_ev = ev, cc_class = cls mk_ct_loc :: PredType -- From instance decl -> SrcSpan -- also from instance deol - -> CtLoc + -> (CtLoc, RewriterSet) mk_ct_loc inst_pred inst_loc - = dict_loc { ctl_origin = FunDepOrigin2 dict_pred dict_origin - inst_pred inst_loc } + = ( dict_loc { ctl_origin = FunDepOrigin2 dict_pred dict_origin + inst_pred inst_loc } + , emptyRewriterSet ) doTopFundepImprovement work_item = pprPanic "doTopFundepImprovement" (ppr work_item) -emitFunDepDeriveds :: [FunDepEqn CtLoc] -> TcS () +emitFunDepWanteds :: RewriterSet -- from the work item + -> [FunDepEqn (CtLoc, RewriterSet)] -> TcS () -- See Note [FunDep and implicit parameter reactions] -emitFunDepDeriveds fd_eqns +emitFunDepWanteds work_rewriters fd_eqns = mapM_ do_one_FDEqn fd_eqns where - do_one_FDEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = loc }) + do_one_FDEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = (loc, rewriters) }) | null tvs -- Common shortcut - = do { traceTcS "emitFunDepDeriveds 1" (ppr (ctl_depth loc) $$ ppr eqs $$ ppr (isGivenLoc loc)) - ; mapM_ (unifyDerived loc Nominal) eqs } + = 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 "emitFunDepDeriveds 2" (ppr (ctl_depth loc) $$ ppr tvs $$ ppr eqs) + = do { traceTcS "emitFunDepWanteds 2" (ppr (ctl_depth loc) $$ ppr tvs $$ ppr eqs) ; subst <- instFlexi tvs -- Takes account of kind substitution - ; mapM_ (do_one_eq loc subst) eqs } + ; mapM_ (do_one_eq loc all_rewriters subst) (reverse eqs) } + -- See Note [Reverse order of fundep equations] + where + all_rewriters = work_rewriters S.<> rewriters - do_one_eq loc subst (Pair ty1 ty2) - = unifyDerived loc Nominal $ - Pair (Type.substTyUnchecked subst ty1) (Type.substTyUnchecked subst ty2) + do_one_eq loc rewriters subst (Pair ty1 ty2) + = unifyWanted rewriters loc Nominal + (Type.substTyUnchecked subst ty1) (Type.substTyUnchecked subst ty2) {- ********************************************************************** @@ -1898,7 +1879,7 @@ emitFunDepDeriveds fd_eqns topReactionsStage :: WorkItem -> TcS (StopOrContinue Ct) -- The work item does not react with the inert set, --- so try interaction with top-level instances. Note: +-- so try interaction with top-level instances. topReactionsStage work_item = do { traceTcS "doTopReact" (ppr work_item) ; case work_item of @@ -1986,6 +1967,47 @@ See * Note [Evidence for quantified constraints] in GHC.Core.Predicate * Note [Equality superclasses in quantified constraints] in GHC.Tc.Solver.Canonical + +Note [Reverse order of fundep equations] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider this scenario (from dependent/should_fail/T13135_simple): + + type Sig :: Type -> Type + data Sig a = SigFun a (Sig a) + + type SmartFun :: forall (t :: Type). Sig t -> Type + type family SmartFun sig = r | r -> sig where + SmartFun @Type (SigFun @Type a sig) = a -> SmartFun @Type sig + + [W] SmartFun @kappa sigma ~ (Int -> Bool) + +The injectivity of SmartFun allows us to produce two new equalities: + + [W] w1 :: Type ~ kappa + [W] w2 :: SigFun @Type Int beta ~ sigma + +for some fresh (beta :: SigType). The second Wanted here is actually +heterogeneous: the LHS has type Sig Type while the RHS has type Sig kappa. +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 +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 +list in left-to-right order, which requires a few key calls to 'reverse'. + +This treatment is also used for class-based functional dependencies, although +we do not have a program yet known to exhibit a loop there. It just seems +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. + -} -------------------- @@ -1999,7 +2021,7 @@ doTopReactEq work_item = doTopReactOther work_item improveTopFunEqs :: CtEvidence -> TyCon -> [TcType] -> TcType -> TcS () -- See Note [FunDep and implicit parameter reactions] improveTopFunEqs ev fam_tc args rhs - | not (isImprovable ev) + | isGiven ev -- See Note [No Given/Given fundeps] = return () | otherwise @@ -2007,11 +2029,15 @@ improveTopFunEqs ev fam_tc args rhs ; eqns <- improve_top_fun_eqs fam_envs fam_tc args rhs ; traceTcS "improveTopFunEqs" (vcat [ ppr fam_tc <+> ppr args <+> ppr rhs , ppr eqns ]) - ; mapM_ (unifyDerived loc Nominal) eqns } + ; mapM_ (\(Pair ty1 ty2) -> unifyWanted rewriters loc Nominal ty1 ty2) + (reverse eqns) } + -- Missing that `reverse` causes T13135 and T13135_simple to loop. + -- See Note [Reverse order of fundep equations] where loc = bumpCtLocDepth (ctEvLoc ev) -- ToDo: this location is wrong; it should be FunDepOrigin2 -- See #14778 + rewriters = ctEvRewriters ev improve_top_fun_eqs :: FamInstEnvs -> TyCon -> [TcType] -> TcType @@ -2094,7 +2120,7 @@ we do *not* need to expand type synonyms because the matcher will do that for us Note [Improvement orientation] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -A very delicate point is the orientation of derived equalities +A very delicate point is the orientation of equalities arising from injectivity improvement (#12522). Suppose we have type family F x = t | t -> x type instance F (a, Int) = (Int, G a) @@ -2103,10 +2129,10 @@ where G is injective; and wanted constraints [W] TF (alpha, beta) ~ fuv [W] fuv ~ (Int, <some type>) -The injectivity will give rise to derived constraints +The injectivity will give rise to constraints - [D] gamma1 ~ alpha - [D] Int ~ beta + [W] gamma1 ~ alpha + [W] Int ~ beta The fresh unification variable gamma1 comes from the fact that we can only do "partial improvement" here; see Section 5.2 of @@ -2115,7 +2141,7 @@ can only do "partial improvement" here; see Section 5.2 of Now, it's very important to orient the equations this way round, so that the fresh unification variable will be eliminated in favour of alpha. If we instead had - [D] alpha ~ gamma1 + [W] alpha ~ gamma1 then we would unify alpha := gamma1; and kick out the wanted constraint. But when we grough it back in, it'd look like [W] TF (gamma1, beta) ~ fuv @@ -2126,7 +2152,7 @@ introducing gamma1 in the first place, in the case where the actual argument (alpha, beta) partly matches the improvement template. But that's a bit tricky, esp when we remember that the kinds much match too; so it's easier to let the normal machinery -handle it. Instead we are careful to orient the new derived +handle it. Instead we are careful to orient the new equality with the template on the left. Delicate, but it works. -} @@ -2142,13 +2168,14 @@ doTopReactDict :: InertSet -> Ct -> TcS (StopOrContinue Ct) doTopReactDict inerts work_item@(CDictCan { cc_ev = ev, cc_class = cls , cc_tyargs = xis }) | isGiven ev -- Never use instances for Given constraints - = doTopFundepImprovement work_item + = continueWith work_item + -- See Note [No Given/Given fundeps] | Just solved_ev <- lookupSolvedDict inerts dict_loc cls xis -- Cached = do { setEvBindIfWanted ev (ctEvTerm solved_ev) ; stopWith ev "Dict/Top (cached)" } - | otherwise -- Wanted or Derived, but not cached + | otherwise -- Wanted, but not cached = do { dflags <- getDynFlags ; lkup_res <- matchClassInst dflags inerts cls xis dict_loc ; case lkup_res of @@ -2174,32 +2201,16 @@ chooseInstance work_item , cir_mk_ev = mk_ev }) = do { traceTcS "doTopReact/found instance for" $ ppr ev ; deeper_loc <- checkInstanceOK loc what pred - ; if isDerived ev - then -- Use type-class instances for Deriveds, in the hope - -- of generating some improvements - -- C.f. Example 3 of Note [The improvement story and derived shadows] - -- It's easy because no evidence is involved - do { dflags <- getDynFlags - ; unless (subGoalDepthExceeded dflags (ctLocDepth deeper_loc)) $ - emitNewDeriveds deeper_loc theta - -- If we have a runaway Derived, let's not issue a - -- "reduction stack overflow" error, which is not particularly - -- friendly. Instead, just drop the Derived. - ; traceTcS "finish_derived" (ppr (ctl_depth deeper_loc)) - ; stopWith ev "Dict/Top (solved derived)" } - - else -- wanted - do { checkReductionDepth deeper_loc pred - ; evb <- getTcEvBindsVar - ; if isCoEvBindsVar evb - then continueWith work_item + ; checkReductionDepth deeper_loc pred + ; evb <- getTcEvBindsVar + ; if isCoEvBindsVar evb + then continueWith work_item -- See Note [Instances in no-evidence implications] - - else - do { evc_vars <- mapM (newWanted deeper_loc) theta + else + do { evc_vars <- mapM (newWanted deeper_loc (ctRewriters work_item)) theta ; setEvBindIfWanted ev (mk_ev (map getEvExpr evc_vars)) ; emitWorkNC (freshGoals evc_vars) - ; stopWith ev "Dict/Top (solved wanted)" }}} + ; stopWith ev "Dict/Top (solved wanted)" }} where ev = ctEvidence work_item pred = ctEvPred ev @@ -2212,8 +2223,7 @@ checkInstanceOK :: CtLoc -> InstanceWhat -> TcPredType -> TcS CtLoc -- Check that it's OK to use this insstance: -- (a) the use is well staged in the Template Haskell sense -- Returns the CtLoc to used for sub-goals --- Probably also want to call checkReductionDepth, but this function --- does not do so to enable special handling for Deriveds in chooseInstance +-- Probably also want to call checkReductionDepth checkInstanceOK loc what pred = do { checkWellStagedDFun loc what pred ; return deeper_loc } diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs index 2cd004053d..9f75491dd0 100644 --- a/compiler/GHC/Tc/Solver/Monad.hs +++ b/compiler/GHC/Tc/Solver/Monad.hs @@ -3,6 +3,7 @@ {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE ViewPatterns #-} @@ -13,8 +14,9 @@ module GHC.Tc.Solver.Monad ( -- The TcS monad - TcS, runTcS, runTcSDeriveds, runTcSDerivedsEarlyAbort, runTcSWithEvBinds, - runTcSInerts, failTcS, warnTcS, addErrTcS, wrapTcS, runTcSEqualities, + TcS, runTcS, runTcSEarlyAbort, runTcSWithEvBinds, runTcSInerts, + failTcS, warnTcS, addErrTcS, wrapTcS, + runTcSEqualities, nestTcS, nestImplicTcS, setEvBindsTcS, emitImplicationTcS, emitTvImplicationTcS, @@ -38,16 +40,14 @@ module GHC.Tc.Solver.Monad ( MaybeNew(..), freshGoals, isFresh, getEvExpr, newTcEvBinds, newNoTcEvBinds, - newWantedEq, newWantedEq_SI, emitNewWantedEq, - newWanted, newWanted_SI, newWantedEvVar, + newWantedEq, emitNewWantedEq, + newWanted, newWantedNC, newWantedEvVarNC, - newDerivedNC, newBoundEvVarId, unifyTyVar, reportUnifications, touchabilityTest, TouchabilityTestResult(..), setEvBind, setWantedEq, setWantedEvTerm, setEvBindIfWanted, newEvVar, newGivenEvVar, newGivenEvVars, - emitNewDeriveds, emitNewDerivedEq, checkReductionDepth, getSolvedDicts, setSolvedDicts, @@ -67,7 +67,6 @@ module GHC.Tc.Solver.Monad ( removeInertCts, getPendingGivenScs, addInertCan, insertFunEq, addInertForAll, emitWorkNC, emitWork, - isImprovable, lookupInertDict, -- The Model @@ -130,7 +129,8 @@ import qualified GHC.Tc.Utils.Monad as TcM import qualified GHC.Tc.Utils.TcMType as TcM import qualified GHC.Tc.Instance.Class as TcM( matchGlobalInst, ClsInstResult(..) ) import qualified GHC.Tc.Utils.Env as TcM - ( checkWellStaged, tcGetDefaultTys, tcLookupClass, tcLookupId, topIdLvl ) + ( checkWellStaged, tcGetDefaultTys, tcLookupClass, tcLookupId, topIdLvl + , tcInitTidyEnv ) import GHC.Tc.Instance.Class( InstanceWhat(..), safeOverlap, instanceReturnsDictCon ) import GHC.Tc.Utils.TcType import GHC.Driver.Session @@ -145,8 +145,8 @@ import GHC.Tc.Solver.InertSet import GHC.Tc.Types.Evidence import GHC.Core.Class import GHC.Core.TyCon -import GHC.Tc.Errors ( solverDepthErrorTcS ) import GHC.Tc.Errors.Types +import GHC.Types.Error ( mkPlainError, noHints ) import GHC.Types.Name import GHC.Types.TyThing @@ -167,15 +167,14 @@ import GHC.Tc.Types.Origin import GHC.Tc.Types.Constraint import GHC.Tc.Utils.Unify import GHC.Core.Predicate - -import GHC.Types.Unique.Set +import GHC.Types.Unique.Set (nonDetEltsUniqSet) +import GHC.Utils.Panic.Plain import Control.Monad import GHC.Utils.Monad import Data.IORef import GHC.Exts (oneShot) -import Data.List ( mapAccumL, partition ) -import Data.List.NonEmpty ( NonEmpty(..) ) +import Data.List ( mapAccumL, partition, find ) #if defined(DEBUG) import GHC.Data.Graph.Directed @@ -183,358 +182,6 @@ import GHC.Data.Graph.Directed {- ********************************************************************* * * - Shadow constraints and improvement -* * -************************************************************************ - -Note [The improvement story and derived shadows] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Because Wanteds cannot rewrite Wanteds (see Note [Wanteds do not -rewrite Wanteds] in GHC.Tc.Types.Constraint), we may miss some opportunities for -solving. Here's a classic example (indexed-types/should_fail/T4093a) - - Ambiguity check for f: (Foo e ~ Maybe e) => Foo e - - We get [G] Foo e ~ Maybe e (CEqCan) - [W] Foo ee ~ Foo e (CEqCan) -- ee is a unification variable - [W] Foo ee ~ Maybe ee (CEqCan) - - The first Wanted gets rewritten to - - [W] Foo ee ~ Maybe e - - But now we appear to be stuck, since we don't rewrite Wanteds with - Wanteds. This is silly because we can see that ee := e is the - only solution. - -The basic plan is - * generate Derived constraints that shadow Wanted constraints - * allow Derived to rewrite Derived - * in order to cause some unifications to take place - * that in turn solve the original Wanteds - -The ONLY reason for all these Derived equalities is to tell us how to -unify a variable: that is, what Mark Jones calls "improvement". - -The same idea is sometimes also called "saturation"; find all the -equalities that must hold in any solution. - -Or, equivalently, you can think of the derived shadows as implementing -the "model": a non-idempotent but no-occurs-check substitution, -reflecting *all* *Nominal* equalities (a ~N ty) that are not -immediately soluble by unification. - -More specifically, here's how it works (Oct 16): - -* Wanted constraints are born as [WD]; this behaves like a - [W] and a [D] paired together. - -* When we are about to add a [WD] to the inert set, if it can - be rewritten by a [D] a ~ ty, then we split it into [W] and [D], - putting the latter into the work list (see maybeEmitShadow). - -In the example above, we get to the point where we are stuck: - [WD] Foo ee ~ Foo e - [WD] Foo ee ~ Maybe ee - -But now when [WD] Foo ee ~ Maybe ee is about to be added, we'll -split it into [W] and [D], since the inert [WD] Foo ee ~ Foo e -can rewrite it. Then: - work item: [D] Foo ee ~ Maybe ee - inert: [W] Foo ee ~ Maybe ee - [WD] Foo ee ~ Maybe e - -See Note [Splitting WD constraints]. Now the work item is rewritten -by the [WD] and we soon get ee := e. - -Additional notes: - - * The derived shadow equalities live in inert_eqs, along with - the Givens and Wanteds; see Note [EqualCtList invariants] - in GHC.Tc.Solver.Types. - - * We make Derived shadows only for Wanteds, not Givens. So we - have only [G], not [GD] and [G] plus splitting. See - Note [Add derived shadows only for Wanteds] - - * We also get Derived equalities from functional dependencies - and type-function injectivity; see calls to unifyDerived. - - * It's worth having [WD] rather than just [W] and [D] because - * efficiency: silly to process the same thing twice - * inert_dicts is a finite map keyed by - the type; it's inconvenient for it to map to TWO constraints - -Another example requiring Deriveds is in -Note [Put touchable variables on the left] in GHC.Tc.Solver.Canonical. - -Note [Splitting WD constraints] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We are about to add a [WD] constraint to the inert set; and we -know that the inert set has fully rewritten it. Should we split -it into [W] and [D], and put the [D] in the work list for further -work? - -* CDictCan (C tys): - Yes if the inert set could rewrite tys to make the class constraint, - or type family, fire. That is, yes if the inert_eqs intersects - with the free vars of tys. For this test we use - (anyRewritableTyVar True) which ignores casts and coercions in tys, - because rewriting the casts or coercions won't make the thing fire - more often. - -* CEqCan (lhs ~ ty): Yes if the inert set could rewrite 'lhs' or 'ty'. - We need to check both 'lhs' and 'ty' against the inert set: - - Inert set contains [D] a ~ ty2 - Then we want to put [D] a ~ ty in the worklist, so we'll - get [D] ty ~ ty2 with consequent good things - - - Inert set contains [D] b ~ a, where b is in ty. - We can't just add [WD] a ~ ty[b] to the inert set, because - that breaks the inert-set invariants. If we tried to - canonicalise another [D] constraint mentioning 'a', we'd - get an infinite loop - - Moreover we must use (anyRewritableTyVar False) for the RHS, - because even tyvars in the casts and coercions could give - an infinite loop if we don't expose it - -* CIrredCan: Yes if the inert set can rewrite the constraint. - We used to think splitting irreds was unnecessary, but - see Note [Splitting Irred WD constraints] - -* Others: nothing is gained by splitting. - -Note [Splitting Irred WD constraints] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Splitting Irred constraints can make a difference. Here is the -scenario: - - a[sk] :: F v -- F is a type family - beta :: alpha - - work item: [WD] a ~ beta - -This is heterogeneous, so we emit a kind equality and make the work item an -inert Irred. - - work item: [D] F v ~ alpha - inert: [WD] (a |> co) ~ beta (CIrredCan) - -Can't make progress on the work item. Add to inert set. This kicks out the -old inert, because a [D] can rewrite a [WD]. - - work item: [WD] (a |> co) ~ beta - inert: [D] F v ~ alpha (CEqCan) - -Can't make progress on this work item either (although GHC tries by -decomposing the cast and rewriting... but that doesn't make a difference), -which is still hetero. Emit a new kind equality and add to inert set. But, -critically, we split the Irred. - - work list: - [D] F v ~ alpha (CEqCan) - [D] (a |> co) ~ beta (CIrred) -- this one was split off - inert: - [W] (a |> co) ~ beta - [D] F v ~ alpha - -We quickly solve the first work item, as it's the same as an inert. - - work item: [D] (a |> co) ~ beta - inert: - [W] (a |> co) ~ beta - [D] F v ~ alpha - -We decompose the cast, yielding - - [D] a ~ beta - -We then rewrite the kinds. The lhs kind is F v, which flattens to alpha. - - co' :: F v ~ alpha - [D] (a |> co') ~ beta - -Now this equality is homo-kinded. So we swizzle it around to - - [D] beta ~ (a |> co') - -and set beta := a |> co', and go home happy. - -If we don't split the Irreds, we loop. This is all dangerously subtle. - -This is triggered by test case typecheck/should_compile/SplitWD. - -Note [Add derived shadows only for Wanteds] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We only add shadows for Wanted constraints. That is, we have -[WD] but not [GD]; and maybeEmitShaodw looks only at [WD] -constraints. - -It does just possibly make sense ot add a derived shadow for a -Given. If we created a Derived shadow of a Given, it could be -rewritten by other Deriveds, and that could, conceivably, lead to a -useful unification. - -But (a) I have been unable to come up with an example of this - happening - (b) see #12660 for how adding the derived shadows - of a Given led to an infinite loop. - (c) It's unlikely that rewriting derived Givens will lead - to a unification because Givens don't mention touchable - unification variables - -For (b) there may be other ways to solve the loop, but simply -reraining from adding derived shadows of Givens is particularly -simple. And it's more efficient too! - -Still, here's one possible reason for adding derived shadows -for Givens. Consider - work-item [G] a ~ [b], inerts has [D] b ~ a. -If we added the derived shadow (into the work list) - [D] a ~ [b] -When we process it, we'll rewrite to a ~ [a] and get an -occurs check. Without it we'll miss the occurs check (reporting -inaccessible code); but that's probably OK. - -Note [Keep CDictCan shadows as CDictCan] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Suppose we have - class C a => D a b -and [G] D a b, [G] C a in the inert set. Now we insert -[D] b ~ c. We want to kick out a derived shadow for [D] D a b, -so we can rewrite it with the new constraint, and perhaps get -instance reduction or other consequences. - -BUT we do not want to kick out a *non-canonical* (D a b). If we -did, we would do this: - - rewrite it to [D] D a c, with pend_sc = True - - use expandSuperClasses to add C a - - go round again, which solves C a from the givens -This loop goes on for ever and triggers the simpl_loop limit. - -Solution: kick out the CDictCan which will have pend_sc = False, -because we've already added its superclasses. So we won't re-add -them. If we forget the pend_sc flag, our cunning scheme for avoiding -generating superclasses repeatedly will fail. - -See #11379 for a case of this. - -Note [Do not do improvement for WOnly] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We do improvement between two constraints (e.g. for injectivity -or functional dependencies) only if both are "improvable". And -we improve a constraint wrt the top-level instances only if -it is improvable. - -Improvable: [G] [WD] [D} -Not improvable: [W] - -Reasons: - -* It's less work: fewer pairs to compare - -* Every [W] has a shadow [D] so nothing is lost - -* Consider [WD] C Int b, where 'b' is a skolem, and - class C a b | a -> b - instance C Int Bool - We'll do a fundep on it and emit [D] b ~ Bool - That will kick out constraint [WD] C Int b - Then we'll split it to [W] C Int b (keep in inert) - and [D] C Int b (in work list) - When processing the latter we'll rewrite it to - [D] C Int Bool - At that point it would be /stupid/ to interact it - with the inert [W] C Int b in the inert set; after all, - it's the very constraint from which the [D] C Int Bool - was split! We can avoid this by not doing improvement - on [W] constraints. This came up in #12860. --} - -maybeEmitShadow :: InertCans -> Ct -> TcS Ct --- See Note [The improvement story and derived shadows] -maybeEmitShadow ics ct - | let ev = ctEvidence ct - , CtWanted { ctev_pred = pred, ctev_loc = loc - , ctev_nosh = WDeriv } <- ev - , shouldSplitWD (inert_eqs ics) (inert_funeqs ics) ct - = do { traceTcS "Emit derived shadow" (ppr ct) - ; let derived_ev = CtDerived { ctev_pred = pred - , ctev_loc = loc } - shadow_ct = ct { cc_ev = derived_ev } - -- Te shadow constraint keeps the canonical shape. - -- This just saves work, but is sometimes important; - -- see Note [Keep CDictCan shadows as CDictCan] - ; emitWork [shadow_ct] - - ; let ev' = ev { ctev_nosh = WOnly } - ct' = ct { cc_ev = ev' } - -- Record that it now has a shadow - -- This is /the/ place we set the flag to WOnly - ; return ct' } - - | otherwise - = return ct - -shouldSplitWD :: InertEqs -> FunEqMap EqualCtList -> Ct -> Bool --- Precondition: 'ct' is [WD], and is inert --- True <=> we should split ct ito [W] and [D] because --- the inert_eqs can make progress on the [D] --- See Note [Splitting WD constraints] - -shouldSplitWD inert_eqs fun_eqs (CDictCan { cc_tyargs = tys }) - = should_split_match_args inert_eqs fun_eqs tys - -- NB True: ignore coercions - -- See Note [Splitting WD constraints] - -shouldSplitWD inert_eqs fun_eqs (CEqCan { cc_lhs = TyVarLHS tv, cc_rhs = ty - , cc_eq_rel = eq_rel }) - = tv `elemDVarEnv` inert_eqs - || anyRewritableCanEqLHS eq_rel (canRewriteTv inert_eqs) (canRewriteTyFam fun_eqs) ty - -- NB False: do not ignore casts and coercions - -- See Note [Splitting WD constraints] - -shouldSplitWD inert_eqs fun_eqs (CEqCan { cc_ev = ev, cc_eq_rel = eq_rel }) - = anyRewritableCanEqLHS eq_rel (canRewriteTv inert_eqs) (canRewriteTyFam fun_eqs) - (ctEvPred ev) - -shouldSplitWD inert_eqs fun_eqs (CIrredCan { cc_ev = ev }) - = anyRewritableCanEqLHS (ctEvEqRel ev) (canRewriteTv inert_eqs) - (canRewriteTyFam fun_eqs) (ctEvPred ev) - -shouldSplitWD _ _ _ = False -- No point in splitting otherwise - -should_split_match_args :: InertEqs -> FunEqMap EqualCtList -> [TcType] -> Bool --- True if the inert_eqs can rewrite anything in the argument types -should_split_match_args inert_eqs fun_eqs tys - = any (anyRewritableCanEqLHS NomEq (canRewriteTv inert_eqs) (canRewriteTyFam fun_eqs)) tys - -- See Note [Splitting WD constraints] - -canRewriteTv :: InertEqs -> EqRel -> TyVar -> Bool -canRewriteTv inert_eqs eq_rel tv - | Just (EqualCtList (ct :| _)) <- lookupDVarEnv inert_eqs tv - , CEqCan { cc_eq_rel = eq_rel1 } <- ct - = eq_rel1 `eqCanRewrite` eq_rel - | otherwise - = False - -canRewriteTyFam :: FunEqMap EqualCtList -> EqRel -> TyCon -> [Type] -> Bool -canRewriteTyFam fun_eqs eq_rel tf args - | Just (EqualCtList (ct :| _)) <- findFunEq fun_eqs tf args - , CEqCan { cc_eq_rel = eq_rel1 } <- ct - = eq_rel1 `eqCanRewrite` eq_rel - | otherwise - = False - -isImprovable :: CtEvidence -> Bool --- See Note [Do not do improvement for WOnly] -isImprovable (CtWanted { ctev_nosh = WOnly }) = False -isImprovable _ = True - - -{- ********************************************************************* -* * Inert instances: inert_insts * * ********************************************************************* -} @@ -601,14 +248,28 @@ Note [Adding an equality to the InertCans] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When adding an equality to the inerts: -* Split [WD] into [W] and [D] if the inerts can rewrite the latter; - done by maybeEmitShadow. - * Kick out any constraints that can be rewritten by the thing we are adding. Done by kickOutRewritable. * Note that unifying a:=ty, is like adding [G] a~ty; just use kickOutRewritable with Nominal, Given. See kickOutAfterUnification. + +Note [Kick out existing binding for implicit parameter] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we have (typecheck/should_compile/ImplicitParamFDs) + flub :: (?x :: Int) => (Int, Integer) + flub = (?x, let ?x = 5 in ?x) +When we are checking the last ?x occurrence, we guess its type +to be a fresh unification variable alpha and emit an (IP "x" alpha) +constraint. But the given (?x :: Int) has been translated to an +IP "x" Int constraint, which has a functional dependency from the +name to the type. So fundep interaction tells us that alpha ~ Int, +and we get a type error. This is bad. + +Instead, we wish to excise any old given for an IP when adding a +new one. We also must make sure not to float out +any IP constraints outside an implication that binds an IP of +the same name; see GHC.Tc.Solver.floatConstraints. -} addInertCan :: Ct -> TcS () @@ -620,7 +281,6 @@ addInertCan ct = ; mkTcS (\TcSEnv{tcs_abort_on_insoluble=abort_flag} -> when (abort_flag && insolubleEqCt ct) TcM.failM) ; ics <- getInertCans - ; ct <- maybeEmitShadow ics ct ; ics <- maybeKickOut ics ct ; tclvl <- getTcLevel ; setInertCans (addInertItem tclvl ics ct) @@ -633,6 +293,27 @@ maybeKickOut ics ct | CEqCan { cc_lhs = lhs, cc_ev = ev, cc_eq_rel = eq_rel } <- ct = do { (_, ics') <- kickOutRewritable (ctEvFlavour ev, eq_rel) lhs ics ; return ics' } + + -- See [Kick out existing binding for implicit parameter] + | isGivenCt ct + , CDictCan { cc_class = cls, cc_tyargs = [ip_name_strty, _ip_ty] } <- ct + , isIPClass cls + , Just ip_name <- isStrLitTy ip_name_strty + -- Would this be more efficient if we used findDictsByClass and then delDict? + = let dict_map = inert_dicts ics + dict_map' = filterDicts doesn't_match_ip_name dict_map + + doesn't_match_ip_name :: Ct -> Bool + doesn't_match_ip_name ct + | Just (inert_ip_name, _inert_ip_ty) <- isIPPred_maybe (ctPred ct) + = inert_ip_name /= ip_name + + | otherwise + = True + + in + return (ics { inert_dicts = dict_map' }) + | otherwise = return ics @@ -682,8 +363,10 @@ kickOutAfterUnification new_tv ; return n_kicked } -- See Wrinkle (2) in Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical -kickOutAfterFillingCoercionHole :: CoercionHole -> Coercion -> TcS () -kickOutAfterFillingCoercionHole hole filled_co +-- 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 @@ -698,39 +381,25 @@ kickOutAfterFillingCoercionHole hole filled_co ; setInertCans ics' } where - holes_of_co = coercionHolesOfCo filled_co - kick_out :: InertCans -> (WorkList, InertCans) - kick_out ics@(IC { inert_blocked = blocked }) - = let (to_kick, to_keep) = partitionBagWith kick_ct blocked - - kicked_out = extendWorkListCts (bagToList to_kick) emptyWorkList - ics' = ics { inert_blocked = to_keep } - in - (kicked_out, ics') - - kick_ct :: Ct -> Either Ct Ct - -- Left: kick out; Right: keep. But even if we keep, we may need - -- to update the set of blocking holes - kick_ct ct@(CIrredCan { cc_reason = HoleBlockerReason holes }) - | hole `elementOfUniqSet` holes - = let new_holes = holes `delOneFromUniqSet` hole - `unionUniqSets` holes_of_co - updated_ct = ct { cc_reason = HoleBlockerReason new_holes } - in - if isEmptyUniqSet new_holes - then Left updated_ct - else Right updated_ct - - | otherwise - = Right ct - - kick_ct other = pprPanic "kickOutAfterFillingCoercionHole" (ppr other) + kick_out ics@(IC { inert_eqs = eqs, inert_funeqs = funeqs }) + = (kicked_out, ics { inert_eqs = eqs_to_keep, inert_funeqs = funeqs_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 (eqs_to_kick ++ funeqs_to_kick) emptyWorkList + + kick_ct :: Ct -> Bool + -- True: kick out; False: keep. + kick_ct (CEqCan { cc_rhs = rhs, cc_ev = ctev }) + = isWanted ctev && -- optimisation: givens don't have coercion holes anyway + rhs `hasThisCoercionHoleTy` hole + kick_ct other = pprPanic "kick_ct (coercion hole)" (ppr other) -------------- addInertSafehask :: InertCans -> Ct -> InertCans addInertSafehask ics item@(CDictCan { cc_class = cls, cc_tyargs = tys }) - = ics { inert_safehask = addDictCt (inert_dicts ics) (classTyCon cls) tys item } + = ics { inert_safehask = addDict (inert_dicts ics) cls tys item } addInertSafehask _ item = pprPanic "addInertSafehask: can't happen! Inserting " $ ppr item @@ -816,7 +485,7 @@ updInertIrreds :: (Cts -> Cts) -> TcS () updInertIrreds upd_fn = updInertCans $ \ ics -> ics { inert_irreds = upd_fn (inert_irreds ics) } -getInertEqs :: TcS (DTyVarEnv EqualCtList) +getInertEqs :: TcS InertEqs getInertEqs = do { inert <- getInertCans; return (inert_eqs inert) } getInnermostGivenEqLevel :: TcS TcLevel @@ -840,9 +509,8 @@ getInertGivens :: TcS [Ct] getInertGivens = do { inerts <- getInertCans ; let all_cts = foldDicts (:) (inert_dicts inerts) - $ foldFunEqs (\ecl out -> equalCtListToList ecl ++ out) - (inert_funeqs inerts) - $ concatMap equalCtListToList (dVarEnvElts (inert_eqs inerts)) + $ foldFunEqs (++) (inert_funeqs inerts) + $ foldDVarEnv (++) [] (inert_eqs inerts) ; return (filter isGivenCt all_cts) } getPendingGivenScs :: TcS [Ct] @@ -878,7 +546,7 @@ get_sc_pending this_lvl ic@(IC { inert_dicts = dicts, inert_insts = insts }) add :: Ct -> DictMap Ct -> DictMap Ct add ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) dicts - = addDictCt dicts (classTyCon cls) tys ct + = addDict dicts cls tys ct add ct _ = pprPanic "getPendingScDicts" (ppr ct) get_pending_inst :: [Ct] -> QCInst -> ([Ct], QCInst) @@ -895,27 +563,24 @@ get_sc_pending this_lvl ic@(IC { inert_dicts = dicts, inert_insts = insts }) getUnsolvedInerts :: TcS ( Bag Implication , Cts ) -- All simple constraints --- Return all the unsolved [Wanted] or [Derived] constraints +-- Return all the unsolved [Wanted] constraints -- -- Post-condition: the returned simple constraints are all fully zonked -- (because they come from the inert set) -- the unsolved implics may not be getUnsolvedInerts - = do { IC { inert_eqs = tv_eqs - , inert_funeqs = fun_eqs - , inert_irreds = irreds - , inert_blocked = blocked - , inert_dicts = idicts + = do { IC { inert_eqs = tv_eqs + , inert_funeqs = fun_eqs + , inert_irreds = irreds + , inert_dicts = idicts } <- getInertCans - ; let unsolved_tv_eqs = foldTyEqs add_if_unsolved tv_eqs emptyCts - unsolved_fun_eqs = foldFunEqs add_if_unsolveds fun_eqs emptyCts - unsolved_irreds = Bag.filterBag is_unsolved irreds - unsolved_blocked = blocked -- all blocked equalities are W/D - unsolved_dicts = foldDicts add_if_unsolved idicts emptyCts - unsolved_others = unionManyBags [ unsolved_irreds - , unsolved_dicts - , unsolved_blocked ] + ; let unsolved_tv_eqs = foldTyEqs add_if_unsolved tv_eqs emptyCts + unsolved_fun_eqs = foldFunEqs add_if_unsolveds fun_eqs emptyCts + unsolved_irreds = Bag.filterBag isWantedCt irreds + unsolved_dicts = foldDicts add_if_unsolved idicts emptyCts + unsolved_others = unionManyBags [ unsolved_irreds + , unsolved_dicts ] ; implics <- getWorkListImplics @@ -930,14 +595,11 @@ getUnsolvedInerts unsolved_others) } where add_if_unsolved :: Ct -> Cts -> Cts - add_if_unsolved ct cts | is_unsolved ct = ct `consCts` cts - | otherwise = cts + add_if_unsolved ct cts | isWantedCt ct = ct `consCts` cts + | otherwise = cts add_if_unsolveds :: EqualCtList -> Cts -> Cts - add_if_unsolveds new_cts old_cts = foldr add_if_unsolved old_cts - (equalCtListToList new_cts) - - is_unsolved ct = not (isGivenCt ct) -- Wanted or Derived + add_if_unsolveds new_cts old_cts = foldr add_if_unsolved old_cts new_cts getHasGivenEqs :: TcLevel -- TcLevel of this implication -> TcS ( HasGivenEqs -- are there Given equalities? @@ -970,15 +632,8 @@ getHasGivenEqs tclvl insoluble_given_equality ct = insolubleEqCt ct && isGivenCt ct -{- Note [Unsolved Derived equalities] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -In getUnsolvedInerts, we return a derived equality from the inert_eqs -because it is a candidate for floating out of this implication. We -only float equalities with a meta-tyvar on the left, so we only pull -those out here. - -Note [What might equal later?] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +{- Note [What might equal later?] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We must determine whether a Given might later equal a Wanted. We definitely need to account for the possibility that any metavariable might be arbitrarily instantiated. Yet we do *not* want @@ -1084,16 +739,17 @@ removeInertCt is ct = pprPanic "removeInertCt" (ppr "CSpecialCan" <+> parens (ppr special_pred)) -- | Looks up a family application in the inerts. -lookupFamAppInert :: TyCon -> [Type] -> TcS (Maybe (Reduction, CtFlavourRole)) -lookupFamAppInert fam_tc tys +lookupFamAppInert :: (CtFlavourRole -> Bool) -- can it rewrite the target? + -> TyCon -> [Type] -> TcS (Maybe (Reduction, CtFlavourRole)) +lookupFamAppInert rewrite_pred fam_tc tys = do { IS { inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts ; return (lookup_inerts inert_funeqs) } where lookup_inerts inert_funeqs - | Just (EqualCtList (CEqCan { cc_ev = ctev, cc_rhs = rhs } :| _)) - <- findFunEq inert_funeqs fam_tc tys - = Just (mkReduction (ctEvCoercion ctev) rhs - ,ctEvFlavourRole ctev) + | Just ecl <- findFunEq inert_funeqs fam_tc tys + , Just (CEqCan { cc_ev = ctev, cc_rhs = rhs }) + <- find (rewrite_pred . ctFlavourRole) ecl + = Just (mkReduction (ctEvCoercion ctev) rhs, ctEvFlavourRole ctev) | otherwise = Nothing lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence) @@ -1139,7 +795,6 @@ extendFamAppCache tc xi_args stuff@(Reduction _ ty) ; when (gopt Opt_FamAppCache dflags) $ do { traceTcS "extendFamAppCache" (vcat [ ppr tc <+> ppr xi_args , ppr ty ]) - -- 'co' can be bottom, in the case of derived items ; updInertTcS $ \ is@(IS { inert_famapp_cache = fc }) -> is { inert_famapp_cache = insertFunEq fc tc xi_args stuff } } } @@ -1330,19 +985,11 @@ runTcS tcs ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var ; return (res, ev_binds) } --- | This variant of 'runTcS' will keep solving, even when only Deriveds --- are left around. It also doesn't return any evidence, as callers won't --- need it. -runTcSDeriveds :: TcS a -> TcM a -runTcSDeriveds tcs - = do { ev_binds_var <- TcM.newTcEvBinds - ; runTcSWithEvBinds ev_binds_var tcs } - - --- | This variant of 'runTcSDeriveds' will immediatley fail upon encountering an --- insoluble ct. See Note [Speeding up valid hole-fits] -runTcSDerivedsEarlyAbort :: TcS a -> TcM a -runTcSDerivedsEarlyAbort tcs +-- | This variant of 'runTcS' will immediatley fail upon encountering an +-- insoluble ct. See Note [Speeding up valid hole-fits]. Its one usage +-- site does not need the ev_binds, so we do not return them. +runTcSEarlyAbort :: TcS a -> TcM a +runTcSEarlyAbort tcs = do { ev_binds_var <- TcM.newTcEvBinds ; runTcSWithEvBinds' True True ev_binds_var tcs } @@ -1915,7 +1562,7 @@ an example: * There's a deeply-nested chain of implication constraints. ?x:alpha => ?y1:beta1 => ... ?yn:betan => [W] ?x:Int - * From the innermost one we get a [D] alpha[1] ~ Int, + * From the innermost one we get a [W] alpha[1] ~ Int, so we can unify. * It's better not to iterate the inner implications, but go all the @@ -2082,7 +1729,7 @@ Yuk! fillCoercionHole :: CoercionHole -> Coercion -> TcS () fillCoercionHole hole co = do { wrapTcS $ TcM.fillCoercionHole hole co - ; kickOutAfterFillingCoercionHole hole co } + ; kickOutAfterFillingCoercionHole hole } setEvBindIfWanted :: CtEvidence -> EvTerm -> TcS () setEvBindIfWanted ev tm @@ -2119,103 +1766,69 @@ newBoundEvVarId pred rhs newGivenEvVars :: CtLoc -> [(TcPredType, EvTerm)] -> TcS [CtEvidence] newGivenEvVars loc pts = mapM (newGivenEvVar loc) pts -emitNewWantedEq :: CtLoc -> Role -> TcType -> TcType -> TcS Coercion +emitNewWantedEq :: CtLoc -> RewriterSet -> Role -> TcType -> TcType -> TcS Coercion -- | Emit a new Wanted equality into the work-list -emitNewWantedEq loc role ty1 ty2 - = do { (ev, co) <- newWantedEq loc role ty1 ty2 +emitNewWantedEq loc rewriters role ty1 ty2 + = do { (ev, co) <- newWantedEq loc rewriters role ty1 ty2 ; updWorkListTcS (extendWorkListEq (mkNonCanonical ev)) ; return co } -- | Make a new equality CtEvidence -newWantedEq :: CtLoc -> Role -> TcType -> TcType +newWantedEq :: CtLoc -> RewriterSet -> Role -> TcType -> TcType -> TcS (CtEvidence, Coercion) -newWantedEq = newWantedEq_SI WDeriv - -newWantedEq_SI :: ShadowInfo -> CtLoc -> Role - -> TcType -> TcType - -> TcS (CtEvidence, Coercion) -newWantedEq_SI si loc role ty1 ty2 +newWantedEq loc rewriters role ty1 ty2 = do { hole <- wrapTcS $ TcM.newCoercionHole pty ; traceTcS "Emitting new coercion hole" (ppr hole <+> dcolon <+> ppr pty) - ; return ( CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole - , ctev_nosh = si - , ctev_loc = loc} + ; return ( CtWanted { ctev_pred = pty + , ctev_dest = HoleDest hole + , ctev_loc = loc + , ctev_rewriters = rewriters } , mkHoleCo hole ) } where pty = mkPrimEqPredRole role ty1 ty2 -- no equalities here. Use newWantedEq instead -newWantedEvVarNC :: CtLoc -> TcPredType -> TcS CtEvidence -newWantedEvVarNC = newWantedEvVarNC_SI WDeriv - -newWantedEvVarNC_SI :: ShadowInfo -> CtLoc -> TcPredType -> TcS CtEvidence +newWantedEvVarNC :: CtLoc -> RewriterSet + -> TcPredType -> TcS CtEvidence -- Don't look up in the solved/inerts; we know it's not there -newWantedEvVarNC_SI si loc pty +newWantedEvVarNC loc rewriters pty = do { new_ev <- newEvVar pty ; traceTcS "Emitting new wanted" (ppr new_ev <+> dcolon <+> ppr pty $$ pprCtLoc loc) - ; return (CtWanted { ctev_pred = pty, ctev_dest = EvVarDest new_ev - , ctev_nosh = si - , ctev_loc = loc })} - -newWantedEvVar :: CtLoc -> TcPredType -> TcS MaybeNew -newWantedEvVar = newWantedEvVar_SI WDeriv + ; return (CtWanted { ctev_pred = pty + , ctev_dest = EvVarDest new_ev + , ctev_loc = loc + , ctev_rewriters = rewriters })} -newWantedEvVar_SI :: ShadowInfo -> CtLoc -> TcPredType -> TcS MaybeNew +newWantedEvVar :: CtLoc -> RewriterSet + -> TcPredType -> TcS MaybeNew -- For anything except ClassPred, this is the same as newWantedEvVarNC -newWantedEvVar_SI si loc pty - = do { mb_ct <- lookupInInerts loc pty +newWantedEvVar loc rewriters pty + = assert (not (isHoleDestPred pty)) $ + do { mb_ct <- lookupInInerts loc pty ; case mb_ct of Just ctev - | not (isDerived ctev) -> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev ; return $ Cached (ctEvExpr ctev) } - _ -> do { ctev <- newWantedEvVarNC_SI si loc pty + _ -> do { ctev <- newWantedEvVarNC loc rewriters pty ; return (Fresh ctev) } } -newWanted :: CtLoc -> PredType -> TcS MaybeNew +newWanted :: CtLoc -> RewriterSet -> PredType -> TcS MaybeNew -- Deals with both equalities and non equalities. Tries to look -- up non-equalities in the cache -newWanted = newWanted_SI WDeriv - -newWanted_SI :: ShadowInfo -> CtLoc -> PredType -> TcS MaybeNew -newWanted_SI si loc pty +newWanted loc rewriters pty | Just (role, ty1, ty2) <- getEqPredTys_maybe pty - = Fresh . fst <$> newWantedEq_SI si loc role ty1 ty2 + = Fresh . fst <$> newWantedEq loc rewriters role ty1 ty2 | otherwise - = newWantedEvVar_SI si loc pty + = newWantedEvVar loc rewriters pty -- deals with both equalities and non equalities. Doesn't do any cache lookups. -newWantedNC :: CtLoc -> PredType -> TcS CtEvidence -newWantedNC loc pty +newWantedNC :: CtLoc -> RewriterSet -> PredType -> TcS CtEvidence +newWantedNC loc rewriters pty | Just (role, ty1, ty2) <- getEqPredTys_maybe pty - = fst <$> newWantedEq loc role ty1 ty2 + = fst <$> newWantedEq loc rewriters role ty1 ty2 | otherwise - = newWantedEvVarNC loc pty - -emitNewDeriveds :: CtLoc -> [TcPredType] -> TcS () -emitNewDeriveds loc preds - | null preds - = return () - | otherwise - = do { evs <- mapM (newDerivedNC loc) preds - ; traceTcS "Emitting new deriveds" (ppr evs) - ; updWorkListTcS (extendWorkListDeriveds evs) } - -emitNewDerivedEq :: CtLoc -> Role -> TcType -> TcType -> TcS () --- Create new equality Derived and put it in the work list --- There's no caching, no lookupInInerts -emitNewDerivedEq loc role ty1 ty2 - = do { ev <- newDerivedNC loc (mkPrimEqPredRole role ty1 ty2) - ; traceTcS "Emitting new derived equality" (ppr ev $$ pprCtLoc loc) - ; updWorkListTcS (extendWorkListEq (mkNonCanonical ev)) } - -- Very important: put in the wl_eqs - -- See Note [Prioritise equalities] in GHC.Tc.Solver.InertSet - -- (Avoiding fundep iteration) - -newDerivedNC :: CtLoc -> TcPredType -> TcS CtEvidence -newDerivedNC loc pred - = return $ CtDerived { ctev_pred = pred, ctev_loc = loc } + = newWantedEvVarNC loc rewriters pty -- --------- Check done in GHC.Tc.Solver.Interact.selectNewWorkItem???? --------- -- | Checks if the depth of the given location is too much. Fails if @@ -2225,8 +1838,7 @@ checkReductionDepth :: CtLoc -> TcType -- ^ type being reduced checkReductionDepth loc ty = do { dflags <- getDynFlags ; when (subGoalDepthExceeded dflags (ctLocDepth loc)) $ - wrapErrTcS $ - solverDepthErrorTcS loc ty } + wrapErrTcS $ solverDepthError loc ty } matchFam :: TyCon -> [Type] -> TcS (Maybe ReductionN) matchFam tycon args = wrapTcS $ matchFamTcM tycon args @@ -2248,6 +1860,28 @@ matchFamTcM tycon args 2 (vcat [ text "Rewrites to:" <+> ppr ty , text "Coercion:" <+> ppr co ]) +solverDepthError :: CtLoc -> TcType -> TcM a +solverDepthError loc ty + = TcM.setCtLocM loc $ + do { ty <- TcM.zonkTcType ty + ; env0 <- TcM.tcInitTidyEnv + ; let tidy_env = tidyFreeTyCoVars env0 (tyCoVarsOfTypeList ty) + tidy_ty = tidyType tidy_env ty + msg = TcRnUnknownMessage $ mkPlainError noHints $ + vcat [ text "Reduction stack overflow; size =" <+> ppr depth + , hang (text "When simplifying the following type:") + 2 (ppr tidy_ty) + , note ] + ; TcM.failWithTcM (tidy_env, msg) } + where + depth = ctLocDepth loc + note = vcat + [ text "Use -freduction-depth=0 to disable this check" + , text "(any upper bound you could choose might fail unpredictably with" + , text " minor updates to GHC, so disabling the check is recommended if" + , text " you're sure that type checking should terminate)" ] + + {- ************************************************************************ * * @@ -2287,16 +1921,12 @@ breakTyVarCycle_maybe ev cte_result (TyVarLHS lhs_tv) rhs flavour = ctEvFlavour ev eq_rel = ctEvEqRel ev - final_check - | Given <- flavour - = return True - | ctFlavourContainsDerived flavour - = do { result <- touchabilityTest Derived lhs_tv rhs - ; return $ case result of - Untouchable -> False - _ -> True } - | otherwise - = return False + final_check = case flavour of + Given -> return True + Wanted -> do { result <- touchabilityTest Wanted lhs_tv rhs + ; return $ case result of + Untouchable -> False + _ -> True } -- This could be considerably more efficient. See Detail (5) of Note. go :: TcType -> TcS ReductionN @@ -2349,10 +1979,10 @@ breakTyVarCycle_maybe ev cte_result (TyVarLHS lhs_tv) rhs ; return $ mkReflRedn Nominal new_ty } -- Why reflexive? See Detail (4) of the Note - _derived_or_wd -> + Wanted -> do { new_tv <- wrapTcS (TcM.newFlexiTyVar fun_app_kind) ; let new_ty = mkTyVarTy new_tv - ; co <- emitNewWantedEq new_loc Nominal new_ty fun_app + ; co <- emitNewWantedEq new_loc (ctEvRewriters ev) Nominal new_ty fun_app ; return $ mkReduction (mkSymCo co) new_ty } -- See Detail (7) of the Note diff --git a/compiler/GHC/Tc/Solver/Rewrite.hs b/compiler/GHC/Tc/Solver/Rewrite.hs index b7573e7f09..6e8baf15a6 100644 --- a/compiler/GHC/Tc/Solver/Rewrite.hs +++ b/compiler/GHC/Tc/Solver/Rewrite.hs @@ -5,7 +5,7 @@ {-# OPTIONS_GHC -Wno-incomplete-record-updates #-} module GHC.Tc.Solver.Rewrite( - rewrite, rewriteKind, rewriteArgsNom, + rewrite, rewriteArgsNom, rewriteType ) where @@ -34,15 +34,14 @@ import GHC.Utils.Outputable import GHC.Utils.Panic import GHC.Utils.Panic.Plain import GHC.Tc.Solver.Monad as TcS -import GHC.Tc.Solver.Types + import GHC.Utils.Misc import GHC.Data.Maybe import GHC.Exts (oneShot) import Control.Monad -import GHC.Utils.Monad ( zipWith3M ) -import Data.List.NonEmpty ( NonEmpty(..) ) import Control.Applicative (liftA3) import GHC.Builtin.Types.Prim (tYPETyCon) +import Data.List ( find ) {- ************************************************************************ @@ -82,18 +81,23 @@ liftTcS thing_inside -- convenient wrapper when you have a CtEvidence describing -- the rewriting operation -runRewriteCtEv :: CtEvidence -> RewriteM a -> TcS a +runRewriteCtEv :: CtEvidence -> RewriteM a -> TcS (a, RewriterSet) runRewriteCtEv ev = runRewrite (ctEvLoc ev) (ctEvFlavour ev) (ctEvEqRel ev) -- Run thing_inside (which does the rewriting) -runRewrite :: CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS a +-- Also returns the set of Wanteds which rewrote a Wanted; +-- See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint +runRewrite :: CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, RewriterSet) runRewrite loc flav eq_rel thing_inside - = runRewriteM thing_inside fmode - where - fmode = FE { fe_loc = loc - , fe_flavour = flav - , fe_eq_rel = eq_rel } + = do { rewriters_ref <- newTcRef emptyRewriterSet + ; let fmode = RE { re_loc = loc + , re_flavour = flav + , re_eq_rel = eq_rel + , re_rewriters = rewriters_ref } + ; res <- runRewriteM thing_inside fmode + ; rewriters <- readTcRef rewriters_ref + ; return (res, rewriters) } traceRewriteM :: String -> SDoc -> RewriteM () traceRewriteM herald doc = liftTcS $ traceTcS herald doc @@ -108,13 +112,13 @@ getRewriteEnvField accessor = mkRewriteM $ \env -> return (accessor env) getEqRel :: RewriteM EqRel -getEqRel = getRewriteEnvField fe_eq_rel +getEqRel = getRewriteEnvField re_eq_rel getRole :: RewriteM Role getRole = eqRelRole <$> getEqRel getFlavour :: RewriteM CtFlavour -getFlavour = getRewriteEnvField fe_flavour +getFlavour = getRewriteEnvField re_flavour getFlavourRole :: RewriteM CtFlavourRole getFlavourRole @@ -123,7 +127,7 @@ getFlavourRole ; return (flavour, eq_rel) } getLoc :: RewriteM CtLoc -getLoc = getRewriteEnvField fe_loc +getLoc = getRewriteEnvField re_loc checkStackDepth :: Type -> RewriteM () checkStackDepth ty @@ -134,38 +138,32 @@ checkStackDepth ty setEqRel :: EqRel -> RewriteM a -> RewriteM a setEqRel new_eq_rel thing_inside = mkRewriteM $ \env -> - if new_eq_rel == fe_eq_rel env + if new_eq_rel == re_eq_rel env then runRewriteM thing_inside env - else runRewriteM thing_inside (env { fe_eq_rel = new_eq_rel }) + else runRewriteM thing_inside (env { re_eq_rel = new_eq_rel }) {-# INLINE setEqRel #-} --- | Make sure that rewriting actually produces a coercion (in other --- words, make sure our flavour is not Derived) --- Note [No derived kind equalities] -noBogusCoercions :: RewriteM a -> RewriteM a -noBogusCoercions thing_inside - = mkRewriteM $ \env -> - -- No new thunk is made if the flavour hasn't changed (note the bang). - let !env' = case fe_flavour env of - Derived -> env { fe_flavour = Wanted WDeriv } - _ -> env - in - runRewriteM thing_inside env' - bumpDepth :: RewriteM a -> RewriteM a bumpDepth (RewriteM thing_inside) = mkRewriteM $ \env -> do -- bumpDepth can be called a lot during rewriting so we force the -- new env to avoid accumulating thunks. - { let !env' = env { fe_loc = bumpCtLocDepth (fe_loc env) } + { let !env' = env { re_loc = bumpCtLocDepth (re_loc env) } ; thing_inside env' } +-- See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint +-- 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) +recordRewriter other = pprPanic "recordRewriter" (ppr other) + {- Note [Rewriter EqRels] ~~~~~~~~~~~~~~~~~~~~~~~ When rewriting, we need to know which equality relation -- nominal or representation -- we should be respecting. The only difference is -that we rewrite variables by representational equalities when fe_eq_rel +that we rewrite variables by representational equalities when re_eq_rel is ReprEq, and that we unwrap newtypes when rewriting w.r.t. representational equality. @@ -203,14 +201,6 @@ soon throw out the phantoms when decomposing a TyConApp. (Or, the canonicaliser will emit an insoluble, in which case we get a better error message anyway.) -Note [No derived kind equalities] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -A kind-level coercion can appear in types, via mkCastTy. So, whenever -we are generating a coercion in a dependent context (in other words, -in a kind) we need to make sure that our flavour is never Derived -(as Derived constraints have no evidence). The noBogusCoercions function -changes the flavour from Derived just for this purpose. - -} {- ********************************************************************* @@ -221,32 +211,21 @@ changes the flavour from Derived just for this purpose. -} -- | See Note [Rewriting]. --- If (xi, co) <- rewrite mode ev ty, then co :: xi ~r ty +-- If (xi, co, rewriters) <- rewrite mode ev ty, then co :: xi ~r ty -- where r is the role in @ev@. +-- rewriters is the set of coercion holes that have been used to rewrite +-- See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint rewrite :: CtEvidence -> TcType - -> TcS Reduction + -> TcS (Reduction, RewriterSet) rewrite ev ty = do { traceTcS "rewrite {" (ppr ty) - ; redn <- runRewriteCtEv ev (rewrite_one ty) + ; result@(redn, _) <- runRewriteCtEv ev (rewrite_one ty) ; traceTcS "rewrite }" (ppr $ reductionReducedType redn) - ; return redn } - --- specialized to rewriting kinds: never Derived, always Nominal --- See Note [No derived kind equalities] --- See Note [Rewriting] -rewriteKind :: CtLoc -> CtFlavour -> TcType -> TcS ReductionN -rewriteKind loc flav ty - = do { traceTcS "rewriteKind {" (ppr flav <+> ppr ty) - ; let flav' = case flav of - Derived -> Wanted WDeriv -- the WDeriv/WOnly choice matters not - _ -> flav - ; redn <- runRewrite loc flav' NomEq (rewrite_one ty) - ; traceTcS "rewriteKind }" (ppr redn) -- the coercion inside the reduction is never a panic - ; return redn } + ; return result } -- See Note [Rewriting] rewriteArgsNom :: CtEvidence -> TyCon -> [TcType] - -> TcS Reductions + -> TcS (Reductions, RewriterSet) -- Externally-callable, hence runRewrite -- Rewrite a vector of types all at once; in fact they are -- always the arguments of type family or class, so @@ -255,15 +234,15 @@ rewriteArgsNom :: CtEvidence -> TyCon -> [TcType] -- The kind passed in is the kind of the type family or class, call it T -- The kind of T args must be constant (i.e. not depend on the args) -- --- For Derived constraints the returned coercion may be undefined --- because rewriting may use a Derived equality ([D] a ~ ty) +-- Final return value returned which Wanteds rewrote another Wanted +-- See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint rewriteArgsNom ev tc tys = do { traceTcS "rewrite_args {" (vcat (map ppr tys)) - ; ArgsReductions redns@(Reductions _ tys') kind_co + ; (ArgsReductions redns@(Reductions _ tys') kind_co, rewriters) <- runRewriteCtEv ev (rewrite_args_tc tc Nothing tys) ; massert (isReflMCo kind_co) ; traceTcS "rewrite }" (vcat (map ppr tys')) - ; return redns } + ; return (redns, rewriters) } -- | Rewrite a type w.r.t. nominal equality. This is useful to rewrite -- a type w.r.t. any givens. It does not do type-family reduction. This @@ -271,10 +250,10 @@ rewriteArgsNom ev tc tys -- only givens. rewriteType :: CtLoc -> TcType -> TcS TcType rewriteType loc ty - = do { redn <- runRewrite loc Given NomEq $ - rewrite_one ty + = do { (redn, _) <- runRewrite loc Given NomEq $ + rewrite_one ty -- use Given flavor so that it is rewritten - -- only w.r.t. Givens, never Wanteds/Deriveds + -- only w.r.t. Givens, never Wanteds -- (Shouldn't matter, if only Givens are present -- anyway) ; return $ reductionReducedType redn } @@ -462,38 +441,20 @@ rewrite_args_slow :: [TyCoBinder] -> Kind -> TcTyCoVarSet -> [Role] -> [Type] -> RewriteM ArgsReductions rewrite_args_slow binders inner_ki fvs roles tys --- Arguments used dependently must be rewritten with proper coercions, but --- we're not guaranteed to get a proper coercion when rewriting with the --- "Derived" flavour. So we must call noBogusCoercions when rewriting arguments --- corresponding to binders that are dependent. However, we might legitimately --- have *more* arguments than binders, in the case that the inner_ki is a variable --- that gets instantiated with a Π-type. We conservatively choose not to produce --- bogus coercions for these, too. Note that this might miss an opportunity for --- a Derived rewriting a Derived. The solution would be to generate evidence for --- Deriveds, thus avoiding this whole noBogusCoercions idea. See also --- Note [No derived kind equalities] - = do { rewritten_args <- zipWith3M rw (map isNamedBinder binders ++ repeat True) - roles tys - ; return $ simplifyArgsWorker binders inner_ki fvs roles rewritten_args } + = do { rewritten_args <- zipWithM rw roles tys + ; return (simplifyArgsWorker binders inner_ki fvs roles rewritten_args) } where {-# INLINE rw #-} - rw :: Bool -- must we ensure to produce a real coercion here? - -- see comment at top of function - -> Role -> Type -> RewriteM Reduction - rw True r ty = noBogusCoercions $ rw1 r ty - rw False r ty = rw1 r ty - - {-# INLINE rw1 #-} - rw1 :: Role -> Type -> RewriteM Reduction - rw1 Nominal ty + rw :: Role -> Type -> RewriteM Reduction + rw Nominal ty = setEqRel NomEq $ rewrite_one ty - rw1 Representational ty + rw Representational ty = setEqRel ReprEq $ rewrite_one ty - rw1 Phantom ty + rw Phantom ty -- See Note [Phantoms in the rewriter] = do { ty <- liftTcS $ zonkTcType ty ; return $ mkReflRedn Phantom ty } @@ -859,17 +820,13 @@ rewrite_exact_fam_app tc tys where reduced = mkTyConApp tc xis -- STEP 3: try the inerts - ; result2 <- liftTcS $ lookupFamAppInert tc xis ; flavour <- getFlavour + ; result2 <- liftTcS $ lookupFamAppInert (`eqCanRewriteFR` (flavour, eq_rel)) tc xis ; case result2 of - { Just (redn, fr@(_, inert_eq_rel)) - - | fr `eqCanRewriteFR` (flavour, eq_rel) -> - do { traceRewriteM "rewrite family application with inert" $ - vcat [ ppr tc <+> ppr xis - , ppUnless (flavour == Derived) (ppr redn) ] - -- Deriveds have no evidence, so we can't print the reduction - ; finish True (homogenise downgraded_redn) } + { Just (redn, (inert_flavour, inert_eq_rel)) + -> do { traceRewriteM "rewrite family application with inert" + (ppr tc <+> ppr xis $$ ppr redn) + ; finish (inert_flavour == Given) (homogenise downgraded_redn) } -- this will sometimes duplicate an inert in the cache, -- but avoiding doing so had no impact on performance, and -- it seems easier not to weed out that special case @@ -890,18 +847,17 @@ rewrite_exact_fam_app tc tys -- call this if the above attempts made progress. -- This recursively rewrites the result and then adds to the cache finish :: Bool -- add to the cache? + -- Precondition: True ==> input coercion has + -- no coercion holes -> Reduction -> RewriteM Reduction finish use_cache redn = do { -- rewrite the result: FINISH 1 final_redn <- rewrite_reduction redn ; eq_rel <- getEqRel - ; flavour <- getFlavour -- extend the cache: FINISH 2 - ; when (use_cache && eq_rel == NomEq && flavour /= Derived) $ + ; when (use_cache && eq_rel == NomEq) $ -- the cache only wants Nominal eqs - -- and Wanteds can rewrite Deriveds; the cache - -- has only Givens liftTcS $ extendFamAppCache tc tys final_redn ; return final_redn } {-# INLINE finish #-} @@ -1034,32 +990,35 @@ rewrite_tyvar2 :: TcTyVar -> CtFlavourRole -> RewriteM RewriteTvResult rewrite_tyvar2 tv fr@(_, eq_rel) = do { ieqs <- liftTcS $ getInertEqs ; case lookupDVarEnv ieqs tv of - Just (EqualCtList (ct :| _)) -- If the first doesn't work, - -- the subsequent ones won't either - | CEqCan { cc_ev = ctev, cc_lhs = TyVarLHS tv + Just equal_ct_list + | Just ct <- find can_rewrite equal_ct_list + , CEqCan { cc_ev = ctev, cc_lhs = TyVarLHS tv , cc_rhs = rhs_ty, cc_eq_rel = ct_eq_rel } <- ct - , let ct_fr = (ctEvFlavour ctev, ct_eq_rel) - , ct_fr `eqCanRewriteFR` fr -- This is THE key call of eqCanRewriteFR - -> do { traceRewriteM "Following inert tyvar" - (ppr tv <+> - equals <+> - ppr rhs_ty $$ ppr ctev) - ; let rewriting_co1 = ctEvCoercion ctev - rewriting_co = case (ct_eq_rel, eq_rel) of - (ReprEq, _rel) -> assert (_rel == ReprEq ) - -- if this ASSERT fails, then + -> do { let wrw = isWantedCt ct + ; traceRewriteM "Following inert tyvar" $ + vcat [ ppr tv <+> equals <+> ppr rhs_ty + , ppr ctev + , text "wanted_rewrite_wanted:" <+> ppr wrw ] + ; when wrw $ recordRewriter ctev + + ; let rewriting_co1 = ctEvCoercion ctev + rewriting_co = case (ct_eq_rel, eq_rel) of + (ReprEq, _rel) -> assert (_rel == ReprEq) + -- if this assert fails, then -- eqCanRewriteFR answered incorrectly rewriting_co1 (NomEq, NomEq) -> rewriting_co1 (NomEq, ReprEq) -> mkSubCo rewriting_co1 - ; return $ RTRFollowed $ mkReduction rewriting_co rhs_ty } - -- NB: ct is Derived then fmode must be also, hence - -- we are not going to touch the returned coercion - -- so ctEvCoercion is fine. + ; return $ RTRFollowed $ mkReduction rewriting_co rhs_ty } _other -> return RTRNotFollowed } + where + can_rewrite :: Ct -> Bool + can_rewrite ct = ctFlavourRole ct `eqCanRewriteFR` fr + -- This is THE key call of eqCanRewriteFR + {- Note [An alternative story for the inert substitution] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/compiler/GHC/Tc/Solver/Types.hs b/compiler/GHC/Tc/Solver/Types.hs index 1b367e450e..d7a46a7c61 100644 --- a/compiler/GHC/Tc/Solver/Types.hs +++ b/compiler/GHC/Tc/Solver/Types.hs @@ -1,14 +1,12 @@ {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE GADTs #-} -{-# LANGUAGE GeneralizedNewtypeDeriving #-} -{-# LANGUAGE PatternSynonyms #-} {-# OPTIONS_GHC -Wno-incomplete-record-updates #-} -- | Utility types used within the constraint solver module GHC.Tc.Solver.Types ( -- Inert CDictCans - DictMap, emptyDictMap, findDictsByClass, addDict, addDictCt, + DictMap, emptyDictMap, findDictsByClass, addDict, addDictsByClass, delDict, foldDicts, filterDicts, findDict, dictsToBag, partitionDicts, @@ -19,9 +17,7 @@ module GHC.Tc.Solver.Types ( insertTcApp, alterTcApp, filterTcAppMap, tcAppMapToBag, foldTcAppMap, - EqualCtList, pattern EqualCtList, - equalCtListToList, filterEqualCtList, unitEqualCtList, - listToEqualCtList, addToEqualCtList, + EqualCtList, filterEqualCtList, addToEqualCtList ) where import GHC.Prelude @@ -39,12 +35,10 @@ import GHC.Core.TyCon.Env import GHC.Data.Bag import GHC.Data.Maybe import GHC.Data.TrieMap +import GHC.Utils.Constants import GHC.Utils.Outputable import GHC.Utils.Panic - -import Data.Foldable -import Data.List.NonEmpty ( NonEmpty(..), nonEmpty, cons ) -import qualified Data.List.NonEmpty as NE +import GHC.Utils.Panic.Plain {- ********************************************************************* * * @@ -157,26 +151,6 @@ delDict m cls tys = delTcApp m (classTyCon cls) tys addDict :: DictMap a -> Class -> [Type] -> a -> DictMap a addDict m cls tys item = insertTcApp m (classTyCon cls) tys item -addDictCt :: DictMap Ct -> TyCon -> [Type] -> Ct -> DictMap Ct --- Like addDict, but combines [W] and [D] to [WD] --- See Note [KeepBoth] in GHC.Tc.Solver.Interact -addDictCt m tc tys new_ct = alterTcApp m tc tys xt_ct - where - new_ct_ev = ctEvidence new_ct - - xt_ct :: Maybe Ct -> Maybe Ct - xt_ct (Just old_ct) - | CtWanted { ctev_nosh = WOnly } <- old_ct_ev - , CtDerived {} <- new_ct_ev - = Just (old_ct { cc_ev = old_ct_ev { ctev_nosh = WDeriv }}) - | CtDerived {} <- old_ct_ev - , CtWanted { ctev_nosh = WOnly } <- new_ct_ev - = Just (new_ct { cc_ev = new_ct_ev { ctev_nosh = WDeriv }}) - where - old_ct_ev = ctEvidence old_ct - - xt_ct _ = Just new_ct - addDictsByClass :: DictMap Ct -> Class -> Bag Ct -> DictMap Ct addDictsByClass m cls items = extendDTyConEnv m (classTyCon cls) (foldr add emptyTM items) @@ -213,7 +187,7 @@ We must /not/ solve this from the Given (?x::Int, C a), because of the intervening binding for (?x::Int). #14218. We deal with this by arranging that we always fail when looking up a -tuple constraint that hides an implicit parameter. Not that this applies +tuple constraint that hides an implicit parameter. Note that this applies * both to the inert_dicts (lookupInertDict) * and to the solved_dicts (looukpSolvedDict) An alternative would be not to extend these sets with such tuple @@ -263,7 +237,7 @@ findFunEq m tc tys = findTcApp m tc tys findFunEqsByTyCon :: FunEqMap a -> TyCon -> [a] -- Get inert function equation constraints that have the given tycon -- in their head. Not that the constraints remain in the inert set. --- We use this to check for derived interactions with built-in type-function +-- We use this to check for wanted interactions with built-in type-function -- constructors. findFunEqsByTyCon m tc | Just tm <- lookupDTyConEnv m tc = foldTM (:) tm [] @@ -281,52 +255,48 @@ insertFunEq m tc tys val = insertTcApp m tc tys val * * ********************************************************************* -} -{- Note [EqualCtList invariants] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +{- +Note [EqualCtList invariants] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ * All are equalities * All these equalities have the same LHS - * The list is never empty * No element of the list can rewrite any other - * Derived before Wanted - -From the fourth invariant it follows that the list is - - A single [G], or - - Zero or one [D] or [WD], followed by any number of [W] -The Wanteds can't rewrite anything which is why we put them last +Accordingly, this list is either empty, contains one element, or +contains a Given representational equality and a Wanted nominal one. -} -newtype EqualCtList = MkEqualCtList (NonEmpty Ct) - deriving newtype Outputable +type EqualCtList = [Ct] -- See Note [EqualCtList invariants] --- | Pattern synonym for easy unwrapping. NB: unidirectional to --- preserve invariants. -pattern EqualCtList :: NonEmpty Ct -> EqualCtList -pattern EqualCtList cts <- MkEqualCtList cts -{-# COMPLETE EqualCtList #-} - -unitEqualCtList :: Ct -> EqualCtList -unitEqualCtList ct = MkEqualCtList (ct :| []) - addToEqualCtList :: Ct -> EqualCtList -> EqualCtList --- NB: This function maintains the "derived-before-wanted" invariant of EqualCtList, --- but not the others. See Note [EqualCtList invariants] -addToEqualCtList ct (MkEqualCtList old_eqs) - | isWantedCt ct - , eq1 :| eqs <- old_eqs - = MkEqualCtList (eq1 :| ct : eqs) +-- See Note [EqualCtList invariants] +addToEqualCtList ct old_eqs + | debugIsOn + = case ct of + CEqCan { cc_lhs = TyVarLHS tv } -> + let shares_lhs (CEqCan { cc_lhs = TyVarLHS old_tv }) = tv == old_tv + shares_lhs _other = False + in + assert (all shares_lhs old_eqs) $ + assert (null ([ (ct1, ct2) | ct1 <- ct : old_eqs + , ct2 <- ct : old_eqs + , let { fr1 = ctFlavourRole ct1 + ; fr2 = ctFlavourRole ct2 } + , fr1 `eqCanRewriteFR` fr2 ])) $ + (ct : old_eqs) + + _ -> pprPanic "addToEqualCtList not CEqCan" (ppr ct) + | otherwise - = MkEqualCtList (ct `cons` old_eqs) + = ct : old_eqs +-- returns Nothing when the new list is empty, to keep the environments smaller filterEqualCtList :: (Ct -> Bool) -> EqualCtList -> Maybe EqualCtList -filterEqualCtList pred (MkEqualCtList cts) - = fmap MkEqualCtList (nonEmpty $ NE.filter pred cts) - -equalCtListToList :: EqualCtList -> [Ct] -equalCtListToList (MkEqualCtList cts) = toList cts - -listToEqualCtList :: [Ct] -> Maybe EqualCtList --- NB: This does not maintain invariants other than having the EqualCtList be --- non-empty -listToEqualCtList cts = MkEqualCtList <$> nonEmpty cts +filterEqualCtList pred cts + | null new_list + = Nothing + | otherwise + = Just new_list + where + new_list = filter pred cts |