Simon Peyton Jones pushed to branch wip/T23162-spj at Glasgow Haskell Compiler / GHC Commits: 02401833 by Simon Peyton Jones at 2025-08-10T00:14:42+01:00 Start to extend to equalities - - - - - 4 changed files: - compiler/GHC/Tc/Solver/Dict.hs - compiler/GHC/Tc/Solver/Equality.hs - compiler/GHC/Tc/Solver/FunDeps.hs - compiler/GHC/Tc/Solver/Monad.hs Changes: ===================================== compiler/GHC/Tc/Solver/Dict.hs ===================================== @@ -21,7 +21,7 @@ import GHC.Tc.Types.Constraint import GHC.Tc.Types.CtLoc import GHC.Tc.Types.Origin import GHC.Tc.Types.EvTerm( evCallStack ) -import GHC.Tc.Solver.FunDeps( doDictFunDepImprovement ) +import GHC.Tc.Solver.FunDeps( tryDictFunDeps ) import GHC.Tc.Solver.InertSet import GHC.Tc.Solver.Monad import GHC.Tc.Solver.Types @@ -95,7 +95,7 @@ solveDict dict_ct@(DictCt { di_ev = ev, di_cls = cls, di_tys = tys }) -- Try fundeps /after/ tryInstances: -- see (DFL2) in Note [Do fundeps last] - ; doDictFunDepImprovement dict_ct + ; tryDictFunDeps dict_ct ; simpleStage (updInertDicts dict_ct) ; stopWithStage (dictCtEvidence dict_ct) "Kept inert DictCt" } ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -16,9 +16,8 @@ import GHC.Tc.Solver.Irred( solveIrred ) import GHC.Tc.Solver.Dict( matchLocalInst, chooseInstance ) import GHC.Tc.Solver.Rewrite import GHC.Tc.Solver.Monad -import GHC.Tc.Solver.FunDeps( unifyAndEmitFunDepWanteds ) +import GHC.Tc.Solver.FunDeps( tryEqFunDeps ) import GHC.Tc.Solver.InertSet -import GHC.Tc.Solver.Types( findFunEqsByTyCon ) import GHC.Tc.Types.Evidence import GHC.Tc.Types.Constraint import GHC.Tc.Types.CtLoc @@ -26,7 +25,6 @@ import GHC.Tc.Types.Origin import GHC.Tc.Utils.Unify import GHC.Tc.Utils.TcType import GHC.Tc.Instance.Family ( tcTopNormaliseNewTypeTF_maybe ) -import GHC.Tc.Instance.FunDeps( FunDepEqn(..) ) import qualified GHC.Tc.Utils.Monad as TcM import GHC.Core.Type @@ -36,21 +34,15 @@ import GHC.Core.DataCon ( dataConName ) import GHC.Core.TyCon import GHC.Core.TyCo.Rep -- cleverly decomposes types, good for completeness checking import GHC.Core.Coercion -import GHC.Core.Coercion.Axiom import GHC.Core.Reduction -import GHC.Core.Unify( tcUnifyTyForInjectivity ) -import GHC.Core.FamInstEnv ( FamInstEnvs, FamInst(..), apartnessCheck - , lookupFamInstEnvByTyCon ) +import GHC.Core.FamInstEnv ( FamInstEnvs ) import GHC.Core - import GHC.Types.Var import GHC.Types.Var.Env import GHC.Types.Var.Set( anyVarSet ) import GHC.Types.Name.Reader import GHC.Types.Basic -import GHC.Builtin.Types.Literals ( tryInteractTopFam, tryInteractInertFam ) - import GHC.Utils.Outputable import GHC.Utils.Panic import GHC.Utils.Misc @@ -120,9 +112,9 @@ solveEquality ev eq_rel ty1 ty2 Left irred_ct -> do { tryQCsIrredEqCt irred_ct ; solveIrred irred_ct } ; - Right eq_ct -> do { tryInertEqs eq_ct - ; tryFunDeps eq_ct - ; tryQCsEqCt eq_ct + Right eq_ct -> do { tryInertEqs eq_ct + ; tryEqFunDeps eq_ct + ; tryQCsEqCt eq_ct ; simpleStage (updInertEqs eq_ct) ; stopWithStage (eqCtEvidence eq_ct) "Kept inert EqCt" } } } @@ -2025,7 +2017,7 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs evCoercion (mkNomReflCo final_rhs) -- Kick out any constraints that can now be rewritten - ; kickOutAfterUnification [tv] + ; recordUnification tv ; return (Stop new_ev (text "Solved by unification")) } @@ -2996,456 +2988,3 @@ lovely quantified constraint. Alas! This test arranges to ignore the instance-based solution under these (rare) circumstances. It's sad, but I really don't see what else we can do. -} - - -{- -********************************************************************** -* * - Functional dependencies for type families -* * -********************************************************************** - -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 wrapUnifierTcS, which will fail, adding these -to the work list. However, crucially, the work list operates like a *stack*. -So, because we add w1 and then w2, we process w2 first. This is silly: solving -w1 would unlock w2. So we make sure to add equalities to the work -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 heterogeneous kinds]). -However, the idea of working left-to-right still seems worthwhile, and so the calls -to 'reverse' remain. - -Note [Improvement orientation] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -See also Note [Fundeps with instances, and equality orientation], which describes -the Exact Same Problem, with the same solution, but for functional dependencies. - -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) -where G is injective; and wanted constraints - - [W] F (alpha, beta) ~ (Int, <some type>) - -The injectivity will give rise to constraints - - [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 -"Injective type families for Haskell" (HS'15). - -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 - [W] alpha ~ gamma1 -then we would unify alpha := gamma1; and kick out the wanted -constraint. But when we substitute it back in, it'd look like - [W] F (gamma1, beta) ~ fuv -and exactly the same thing would happen again! Infinite loop. - -This all seems fragile, and it might seem more robust to avoid -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 -equality with the template on the left. Delicate, but it works. - --} - --------------------- - -tryFunDeps :: EqCt -> SolverStage () -tryFunDeps work_item@(EqCt { eq_lhs = lhs, eq_ev = ev, eq_eq_rel = eq_rel }) - | NomEq <- eq_rel - , TyFamLHS tc args <- lhs - = Stage $ - do { inerts <- getInertCans - ; imp1 <- improveLocalFunEqs inerts tc args work_item - ; imp2 <- improveTopFunEqs tc args work_item - ; if (imp1 || imp2) - then startAgainWith (mkNonCanonical ev) - else continueWith () } - | otherwise - = nopStage () - --------------------- -improveTopFunEqs :: TyCon -> [TcType] -> EqCt -> TcS Bool --- TyCon is definitely a type family --- See Note [FunDep and implicit parameter reactions] -improveTopFunEqs fam_tc args (EqCt { eq_ev = ev, eq_rhs = rhs_ty }) - | isGiven ev = improveGivenTopFunEqs fam_tc args ev rhs_ty - | otherwise = improveWantedTopFunEqs fam_tc args ev rhs_ty - -improveGivenTopFunEqs :: TyCon -> [TcType] -> CtEvidence -> Xi -> TcS Bool --- TyCon is definitely a type family --- Work-item is a Given -improveGivenTopFunEqs fam_tc args ev rhs_ty - | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc - = do { traceTcS "improveGivenTopFunEqs" (ppr fam_tc <+> ppr args $$ ppr ev $$ ppr rhs_ty) - ; emitNewGivens (ctEvLoc ev) $ - [ (Nominal, new_co) - | (ax, _) <- tryInteractTopFam ops fam_tc args rhs_ty - , let new_co = mkAxiomCo ax [given_co] ] - ; return False } -- False: no unifications - | otherwise - = return False - where - given_co :: Coercion = ctEvCoercion ev - -improveWantedTopFunEqs :: TyCon -> [TcType] -> CtEvidence -> Xi -> TcS Bool --- TyCon is definitely a type family --- Work-item is a Wanted -improveWantedTopFunEqs fam_tc args ev rhs_ty - = do { eqns <- improve_wanted_top_fun_eqs fam_tc args rhs_ty - ; traceTcS "improveTopFunEqs" (vcat [ text "lhs:" <+> ppr fam_tc <+> ppr args - , text "rhs:" <+> ppr rhs_ty - , text "eqns:" <+> ppr eqns ]) - ; unifyFunDeps ev Nominal $ \uenv -> - uPairsTcM (bump_depth uenv) (reverse eqns) } - -- Missing that `reverse` causes T13135 and T13135_simple to loop. - -- See Note [Reverse order of fundep equations] - - where - bump_depth env = env { u_loc = bumpCtLocDepth (u_loc env) } - -- ToDo: this location is wrong; it should be FunDepOrigin2 - -- See #14778 - -improve_wanted_top_fun_eqs :: TyCon -> [TcType] -> Xi - -> TcS [TypeEqn] --- TyCon is definitely a type family -improve_wanted_top_fun_eqs fam_tc lhs_tys rhs_ty - | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc - = return (map snd $ tryInteractTopFam ops fam_tc lhs_tys rhs_ty) - - -- ToDo: use ideas in #23162 for closed type families; injectivity only for open - - -- See Note [Type inference for type families with injectivity] - -- Open, so look for inj - | Injective inj_args <- tyConInjectivityInfo fam_tc - = do { fam_envs <- getFamInstEnvs - ; top_eqns <- improve_injective_wanted_top fam_envs inj_args fam_tc lhs_tys rhs_ty - ; let local_eqns = improve_injective_wanted_famfam inj_args fam_tc lhs_tys rhs_ty - ; traceTcS "improve_wanted_top_fun_eqs" $ - vcat [ ppr fam_tc, text "local_eqns" <+> ppr local_eqns, text "top_eqns" <+> ppr top_eqns ] - -- xxx ToDo: this does both local and top => bug? - ; return (local_eqns ++ top_eqns) } - - | otherwise -- No injectivity - = return [] - -improve_injective_wanted_top :: FamInstEnvs -> [Bool] -> TyCon -> [TcType] -> Xi -> TcS [TypeEqn] --- Interact with top-level instance declarations --- See Section 5.2 in the Injective Type Families paper -improve_injective_wanted_top fam_envs inj_args fam_tc lhs_tys rhs_ty - = concatMapM do_one branches - where - branches :: [CoAxBranch] - branches | isOpenTypeFamilyTyCon fam_tc - , let fam_insts = lookupFamInstEnvByTyCon fam_envs fam_tc - = concatMap (fromBranches . coAxiomBranches . fi_axiom) fam_insts - - | Just ax <- isClosedSynFamilyTyConWithAxiom_maybe fam_tc - = fromBranches (coAxiomBranches ax) - - | otherwise - = [] - - do_one :: CoAxBranch -> TcS [TypeEqn] - do_one branch@(CoAxBranch { cab_tvs = branch_tvs, cab_lhs = branch_lhs_tys, cab_rhs = branch_rhs }) - | let in_scope1 = in_scope `extendInScopeSetList` branch_tvs - , Just subst <- tcUnifyTyForInjectivity False in_scope1 branch_rhs rhs_ty - -- False: matching, not unifying - = do { let inSubst tv = tv `elemVarEnv` getTvSubstEnv subst - unsubstTvs = filterOut inSubst branch_tvs - -- The order of unsubstTvs is important; it must be - -- in telescope order e.g. (k:*) (a:k) - - ; (_subst_tvs, subst1) <- instFlexiX subst unsubstTvs - -- If the current substitution bind [k -> *], and - -- one of the un-substituted tyvars is (a::k), we'd better - -- be sure to apply the current substitution to a's kind. - -- Hence instFlexiX. #13135 was an example. - - ; traceTcS "improve_inj_top" $ - vcat [ text "branch_rhs" <+> ppr branch_rhs - , text "rhs_ty" <+> ppr rhs_ty - , text "subst" <+> ppr subst - , text "subst1" <+> ppr subst1 ] - ; if apartnessCheck (substTys subst1 branch_lhs_tys) branch - then do { traceTcS "improv_inj_top1" (ppr branch_lhs_tys) - ; return (mkInjectivityEqns inj_args (map (substTy subst1) branch_lhs_tys) lhs_tys) } - -- NB: The fresh unification variables (from unsubstTvs) are on the left - -- See Note [Improvement orientation] - else do { traceTcS "improve_inj_top2" empty; return [] } } - | otherwise - = do { traceTcS "improve_inj_top:fail" (ppr branch_rhs $$ ppr rhs_ty $$ ppr in_scope $$ ppr branch_tvs) - ; return [] } - - in_scope = mkInScopeSet (tyCoVarsOfType rhs_ty) - - -improve_injective_wanted_famfam :: [Bool] -> TyCon -> [TcType] -> Xi -> [TypeEqn] --- Interact with itself, specifically F s1 s2 ~ F t1 t2 -improve_injective_wanted_famfam inj_args fam_tc lhs_tys rhs_ty - | Just (tc, rhs_tys) <- tcSplitTyConApp_maybe rhs_ty - , tc == fam_tc - = mkInjectivityEqns inj_args lhs_tys rhs_tys - | otherwise - = [] - -mkInjectivityEqns :: [Bool] -> [TcType] -> [TcType] -> [TypeEqn] --- When F s1 s2 s3 ~ F t1 t2 t3, and F has injectivity info [True,False,True] --- return the equations [Pair s1 t1, Pair s3 t3] -mkInjectivityEqns inj_args lhs_args rhs_args - = [ Pair lhs_arg rhs_arg | (True, lhs_arg, rhs_arg) <- zip3 inj_args lhs_args rhs_args ] - ---------------------------------------------- -improveLocalFunEqs :: InertCans - -> TyCon -> [TcType] -> EqCt -- F args ~ rhs - -> TcS Bool --- Emit equalities from interaction between two equalities -improveLocalFunEqs inerts fam_tc args (EqCt { eq_ev = work_ev, eq_rhs = rhs }) - | isGiven work_ev = improveGivenLocalFunEqs funeqs_for_tc fam_tc args work_ev rhs - | otherwise = improveWantedLocalFunEqs funeqs_for_tc fam_tc args work_ev rhs - where - funeqs = inert_funeqs inerts - funeqs_for_tc :: [EqCt] -- Mixture of Given and Wanted - funeqs_for_tc = [ funeq_ct | equal_ct_list <- findFunEqsByTyCon funeqs fam_tc - , funeq_ct <- equal_ct_list - , NomEq == eq_eq_rel funeq_ct ] - -- Representational equalities don't interact - -- with type family dependencies - - -improveGivenLocalFunEqs :: [EqCt] -- Inert items, mixture of Given and Wanted - -> TyCon -> [TcType] -> CtEvidence -> Xi -- Work item (Given) - -> TcS Bool -- Always False (no unifications) --- Emit equalities from interaction between two Given type-family equalities --- e.g. (x+y1~z, x+y2~z) => (y1 ~ y2) -improveGivenLocalFunEqs funeqs_for_tc fam_tc work_args work_ev work_rhs - | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc - = do { mapM_ (do_one ops) funeqs_for_tc - ; return False } -- False: no unifications - | otherwise - = return False - where - given_co :: Coercion = ctEvCoercion work_ev - - do_one :: BuiltInSynFamily -> EqCt -> TcS () - -- Used only work-item is Given - do_one ops EqCt { eq_ev = inert_ev, eq_lhs = inert_lhs, eq_rhs = inert_rhs } - | isGiven inert_ev -- Given/Given interaction - , TyFamLHS _ inert_args <- inert_lhs -- Inert item is F inert_args ~ inert_rhs - , work_rhs `tcEqType` inert_rhs -- Both RHSs are the same - , -- So we have work_ev : F work_args ~ rhs - -- inert_ev : F inert_args ~ rhs - let pairs :: [(CoAxiomRule, TypeEqn)] - pairs = tryInteractInertFam ops fam_tc work_args inert_args - , not (null pairs) - = do { traceTcS "improveGivenLocalFunEqs" (vcat[ ppr fam_tc <+> ppr work_args - , text "work_ev" <+> ppr work_ev - , text "inert_ev" <+> ppr inert_ev - , ppr work_rhs - , ppr pairs ]) - ; emitNewGivens (ctEvLoc inert_ev) (map mk_ax_co pairs) } - -- This CtLoc for the new Givens doesn't reflect the - -- fact that it's a combination of Givens, but I don't - -- this that matters. - where - inert_co = ctEvCoercion inert_ev - mk_ax_co (ax,_) = (Nominal, mkAxiomCo ax [combined_co]) - where - combined_co = given_co `mkTransCo` mkSymCo inert_co - -- given_co :: F work_args ~ rhs - -- inert_co :: F inert_args ~ rhs - -- the_co :: F work_args ~ F inert_args - - do_one _ _ = return () - -improveWantedLocalFunEqs - :: [EqCt] -- Inert items (Given and Wanted) - -> TyCon -> [TcType] -> CtEvidence -> Xi -- Work item (Wanted) - -> TcS Bool -- True <=> some unifications --- Emit improvement equalities for a Wanted constraint, by comparing --- the current work item with inert CFunEqs (both Given and Wanted) --- E.g. x + y ~ z, x + y' ~ z => [W] y ~ y' --- --- See Note [FunDep and implicit parameter reactions] -improveWantedLocalFunEqs funeqs_for_tc fam_tc args work_ev rhs - | null improvement_eqns - = return False - | otherwise - = do { traceTcS "interactFunEq improvements: " $ - vcat [ text "Eqns:" <+> ppr improvement_eqns - , text "Candidates:" <+> ppr funeqs_for_tc ] - ; unifyAndEmitFunDepWanteds work_ev improvement_eqns } - where - work_loc = ctEvLoc work_ev - work_pred = ctEvPred work_ev - fam_inj_info = tyConInjectivityInfo fam_tc - - -------------------- - improvement_eqns :: [FunDepEqn (CtLoc, RewriterSet)] - improvement_eqns - | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc - = -- Try built-in families, notably for arithmethic - concatMap (do_one_built_in ops rhs) funeqs_for_tc - - | Injective injective_args <- fam_inj_info - = -- Try improvement from type families with injectivity annotations - concatMap (do_one_injective injective_args rhs) funeqs_for_tc - - | otherwise - = [] - - -------------------- - do_one_built_in ops rhs (EqCt { eq_lhs = TyFamLHS _ iargs, eq_rhs = irhs, eq_ev = inert_ev }) - | irhs `tcEqType` rhs - = mk_fd_eqns inert_ev (map snd $ tryInteractInertFam ops fam_tc args iargs) - | otherwise - = [] - do_one_built_in _ _ _ = pprPanic "interactFunEq 1" (ppr fam_tc) -- TyVarLHS - - -------------------- - -- See Note [Type inference for type families with injectivity] - do_one_injective inj_args rhs (EqCt { eq_lhs = TyFamLHS _ inert_args - , eq_rhs = irhs, eq_ev = inert_ev }) - | rhs `tcEqType` irhs - = mk_fd_eqns inert_ev $ mkInjectivityEqns inj_args args inert_args - | otherwise - = [] - - do_one_injective _ _ _ = pprPanic "interactFunEq 2" (ppr fam_tc) -- TyVarLHS - - -------------------- - mk_fd_eqns :: CtEvidence -> [TypeEqn] -> [FunDepEqn (CtLoc, RewriterSet)] - mk_fd_eqns inert_ev eqns - | null eqns = [] - | otherwise = [ FDEqn { fd_qtvs = [], fd_eqs = eqns - , fd_loc = (loc, inert_rewriters) } ] - where - 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] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -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 Wanted constraint on -the injective argument - [W] t1 ~ t2 - -That in turn can help GHC solve constraints that would otherwise require -guessing. For example, consider the ambiguity check for - f :: F Int b -> Int -We get the constraint - [W] F Int b ~ F Int beta -where beta is a unification variable. Injectivity lets us pick beta ~ b. - -Injectivity information is also used at the call sites. For example: - g = f True -gives rise to - [W] F Int b ~ Bool -from which we can derive b. This requires looking at the defining equations of -a type family, ie. finding equation with a matching RHS (Bool in this example) -and inferring values of type variables (b in this example) from the LHS patterns -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 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 Wanteds in three places, depending on how we notice the -injectivity. - -1. When we have a [W] F tys1 ~ F tys2. This is handled in canEqCanLHS2, and -described in Note [Decomposing type family applications] in GHC.Tc.Solver.Equality - -2. When we have [W] F tys1 ~ T and [W] F tys2 ~ T. Note that neither of these -constraints rewrites the other, as they have different LHSs. This is done -in improveLocalFunEqs, called during the interactWithInertsStage. - -3. When we have [W] F tys ~ T and an equation for F that looks like F tys' = T. -This is done in improve_top_fun_eqs, called from the top-level reactions stage. - -See also Note [Injective type families] in GHC.Core.TyCon - -Note [Cache-caused loops] -~~~~~~~~~~~~~~~~~~~~~~~~~ -It is very dangerous to cache a rewritten wanted family equation as 'solved' in our -solved cache (which is the default behaviour or xCtEvidence), because the interaction -may not be contributing towards a solution. Here is an example: - -Initial inert set: - [W] g1 : F a ~ beta1 -Work item: - [W] g2 : F a ~ beta2 -The work item will react with the inert yielding the _same_ inert set plus: - (i) Will set g2 := g1 `cast` g3 - (ii) Will add to our solved cache that [S] g2 : F a ~ beta2 - (iii) Will emit [W] g3 : beta1 ~ beta2 -Now, the g3 work item will be spontaneously solved to [G] g3 : beta1 ~ beta2 -and then it will react the item in the inert ([W] g1 : F a ~ beta1). So it -will set - g1 := g ; sym g3 -and what is g? Well it would ideally be a new goal of type (F a ~ beta2) but -remember that we have this in our solved cache, and it is ... g2! In short we -created the evidence loop: - - g2 := g1 ; g3 - g3 := refl - g1 := g2 ; sym g3 - -To avoid this situation we do not cache as solved any workitems (or inert) -which did not really made a 'step' towards proving some goal. Solved's are -just an optimization so we don't lose anything in terms of completeness of -solving. --} ===================================== compiler/GHC/Tc/Solver/FunDeps.hs ===================================== @@ -4,7 +4,8 @@ -- | Solving Class constraints CDictCan module GHC.Tc.Solver.FunDeps ( unifyAndEmitFunDepWanteds, - doDictFunDepImprovement, + tryDictFunDeps, + tryEqFunDeps ) where import GHC.Prelude @@ -12,25 +13,34 @@ import GHC.Prelude import {-# SOURCE #-} GHC.Tc.Solver.Solve( solveSimpleWanteds ) import GHC.Tc.Instance.FunDeps -import GHC.Tc.Types.Evidence -import GHC.Tc.Types.Constraint -import GHC.Tc.Types.CtLoc -import GHC.Tc.Types.Origin import GHC.Tc.Solver.InertSet import GHC.Tc.Solver.Monad import GHC.Tc.Solver.Types import GHC.Tc.Utils.TcType import GHC.Tc.Utils.Unify( UnifyEnv(..) ) import GHC.Tc.Utils.Monad as TcM +import GHC.Tc.Types.Evidence +import GHC.Tc.Types.Constraint +import GHC.Tc.Types.CtLoc +import GHC.Tc.Types.Origin import GHC.Core.Type -import GHC.Core.InstEnv ( ClsInst(..) ) -import GHC.Core.Coercion.Axiom( TypeEqn ) - +import GHC.Core.FamInstEnv +import GHC.Core.Coercion +import GHC.Core.Predicate( EqRel(..) ) +import GHC.Core.TyCon +import GHC.Core.Unify( tcUnifyTyForInjectivity ) +import GHC.Core.InstEnv( ClsInst(..) ) +import GHC.Core.Coercion.Axiom + +import GHC.Builtin.Types.Literals( tryInteractTopFam, tryInteractInertFam ) import GHC.Types.Name import GHC.Types.Var.Set +import GHC.Types.Var.Env import GHC.Utils.Outputable +import GHC.Utils.Panic +import GHC.Utils.Misc( filterOut ) import GHC.Data.Bag import GHC.Data.Pair @@ -41,7 +51,7 @@ import Control.Monad {- ********************************************************************* * * -* Functional dependencies, instantiation of equations +* Functional dependencies for dictionaries * * ************************************************************************ @@ -296,24 +306,24 @@ as the fundeps. #7875 is a case in point. -} -doDictFunDepImprovement :: DictCt -> SolverStage () --- (doDictFunDepImprovement inst_envs cts) +tryDictFunDeps :: DictCt -> SolverStage () +-- (tryDictFunDeps inst_envs cts) -- * Generate the fundeps from interacting the -- top-level `inst_envs` with the constraints `cts` -- * Do the unifications and return any unsolved constraints -- See Note [Fundeps with instances, and equality orientation] --- doLocalFunDepImprovement does StartAgain if there +-- doLocalFunDeps does StartAgain if there -- are any fundeps: see (DFL1) in Note [Do fundeps last] -doDictFunDepImprovement dict_ct - = do { doDictFunDepImprovementLocal dict_ct - ; doDictFunDepImprovementTop dict_ct } +tryDictFunDeps dict_ct + = do { tryDictFunDepsLocal dict_ct + ; tryDictFunDepsTop dict_ct } -doDictFunDepImprovementLocal :: DictCt -> SolverStage () +tryDictFunDepsLocal :: DictCt -> SolverStage () -- Using functional dependencies, interact the DictCt with the -- inert Givens and Wanteds, to produce new equalities -doDictFunDepImprovementLocal dict_ct@(DictCt { di_cls = cls, di_ev = work_ev }) +tryDictFunDepsLocal dict_ct@(DictCt { di_cls = cls, di_ev = work_ev }) | isGiven work_ev = -- If work_ev is Given, there could in principle be some inert Wanteds -- but in practice there never are because we solve Givens first @@ -323,11 +333,11 @@ doDictFunDepImprovementLocal dict_ct@(DictCt { di_cls = cls, di_ev = work_ev }) = Stage $ do { inerts <- getInertCans - ; traceTcS "doDictFunDepImprovementLocal {" (ppr dict_ct) + ; traceTcS "tryDictFunDepsLocal {" (ppr dict_ct) ; imp <- solveFunDeps $ foldM do_interaction emptyCts $ findDictsByClass (inert_dicts inerts) cls - ; traceTcS "doDictFunDepImprovementLocal }" (text "imp =" <+> ppr imp) + ; traceTcS "tryDictFunDepsLocal }" (text "imp =" <+> ppr imp) ; if imp then startAgainWith (CDictCan dict_ct) else continueWith () } @@ -350,7 +360,7 @@ doDictFunDepImprovementLocal dict_ct@(DictCt { di_cls = cls, di_ev = work_ev }) improveFromAnother (deriv_loc, inert_rewriters) inert_pred work_pred - ; traceTcS "doDictFunDepImprovementLocal item" $ + ; traceTcS "tryDictFunDepsLocal item" $ vcat [ ppr work_ev, ppr new_eqs2 ] ; return (new_eqs1 `unionBags` new_eqs2) } @@ -369,17 +379,17 @@ doDictFunDepImprovementLocal dict_ct@(DictCt { di_cls = cls, di_ev = work_ev }) (ctLocOrigin inert_loc) (ctLocSpan inert_loc) -doDictFunDepImprovementTop :: DictCt -> SolverStage () -doDictFunDepImprovementTop dict_ct@(DictCt { di_ev = ev, di_cls = cls, di_tys = xis }) +tryDictFunDepsTop :: DictCt -> SolverStage () +tryDictFunDepsTop dict_ct@(DictCt { di_ev = ev, di_cls = cls, di_tys = xis }) = Stage $ do { inst_envs <- getInstEnvs - ; traceTcS "doDictFunDepImprovementTop {" (ppr dict_ct) + ; traceTcS "tryDictFunDepsTop {" (ppr dict_ct) ; let eqns :: [FunDepEqn (CtLoc, RewriterSet)] eqns = improveFromInstEnv inst_envs mk_ct_loc cls xis ; imp <- solveFunDeps $ unifyFunDepWanteds_new ev eqns - ; traceTcS "doDictFunDepImprovementTop }" (text "imp =" <+> ppr imp) + ; traceTcS "tryDictFunDepsTop }" (text "imp =" <+> ppr imp) ; if imp then startAgainWith (CDictCan dict_ct) else continueWith () } @@ -469,6 +479,464 @@ The bottom line: since we have no evidence for them, we should ignore Given/Give and Given/instance fundeps entirely. -} + + +{- +********************************************************************** +* * + Functional dependencies for type families +* * +********************************************************************** + +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 wrapUnifierTcS, which will fail, adding these +to the work list. However, crucially, the work list operates like a *stack*. +So, because we add w1 and then w2, we process w2 first. This is silly: solving +w1 would unlock w2. So we make sure to add equalities to the work +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 heterogeneous kinds]). +However, the idea of working left-to-right still seems worthwhile, and so the calls +to 'reverse' remain. + +Note [Improvement orientation] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +See also Note [Fundeps with instances, and equality orientation], which describes +the Exact Same Problem, with the same solution, but for functional dependencies. + +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) +where G is injective; and wanted constraints + + [W] F (alpha, beta) ~ (Int, <some type>) + +The injectivity will give rise to constraints + + [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 +"Injective type families for Haskell" (HS'15). + +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 + [W] alpha ~ gamma1 +then we would unify alpha := gamma1; and kick out the wanted +constraint. But when we substitute it back in, it'd look like + [W] F (gamma1, beta) ~ fuv +and exactly the same thing would happen again! Infinite loop. + +---> ToDo: all this fragility has gone away! Fix the Note! <--- + +This all seems fragile, and it might seem more robust to avoid +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 +equality with the template on the left. Delicate, but it works. + +-} + +-------------------- +tryEqFunDeps :: EqCt -> SolverStage () +tryEqFunDeps work_item@(EqCt { eq_lhs = lhs, eq_eq_rel = eq_rel }) + | NomEq <- eq_rel + , TyFamLHS tc args <- lhs + = do { improveLocalFunEqs tc args work_item + ; improveTopFunEqs tc args work_item } + | otherwise + = nopStage () + +-------------------- +improveTopFunEqs :: TyCon -> [TcType] -> EqCt -> SolverStage () +-- TyCon is definitely a type family +-- See Note [FunDep and implicit parameter reactions] +improveTopFunEqs fam_tc args eq_ct@(EqCt { eq_ev = ev, eq_rhs = rhs_ty }) + = Stage $ + do { imp <- if isGiven ev + then improveGivenTopFunEqs fam_tc args ev rhs_ty + else improveWantedTopFunEqs fam_tc args ev rhs_ty + ; if imp then startAgainWith (CEqCan eq_ct) + else continueWith () } + +improveGivenTopFunEqs :: TyCon -> [TcType] -> CtEvidence -> Xi -> TcS Bool +-- TyCon is definitely a type family +-- Work-item is a Given +improveGivenTopFunEqs fam_tc args ev rhs_ty + | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc + = do { traceTcS "improveGivenTopFunEqs" (ppr fam_tc <+> ppr args $$ ppr ev $$ ppr rhs_ty) + ; emitNewGivens (ctEvLoc ev) $ + [ (Nominal, new_co) + | (ax, _) <- tryInteractTopFam ops fam_tc args rhs_ty + , let new_co = mkAxiomCo ax [given_co] ] + ; return False } -- False: no unifications + | otherwise + = return False + where + given_co :: Coercion = ctEvCoercion ev + +improveWantedTopFunEqs :: TyCon -> [TcType] -> CtEvidence -> Xi -> TcS Bool +-- TyCon is definitely a type family +-- Work-item is a Wanted +improveWantedTopFunEqs fam_tc args ev rhs_ty + = do { eqns <- improve_wanted_top_fun_eqs fam_tc args rhs_ty + ; traceTcS "improveTopFunEqs" (vcat [ text "lhs:" <+> ppr fam_tc <+> ppr args + , text "rhs:" <+> ppr rhs_ty + , text "eqns:" <+> ppr eqns ]) + ; unifyFunDeps ev Nominal $ \uenv -> + uPairsTcM (bump_depth uenv) (reverse eqns) } + -- Missing that `reverse` causes T13135 and T13135_simple to loop. + -- See Note [Reverse order of fundep equations] + + where + bump_depth env = env { u_loc = bumpCtLocDepth (u_loc env) } + -- ToDo: this location is wrong; it should be FunDepOrigin2 + -- See #14778 + +improve_wanted_top_fun_eqs :: TyCon -> [TcType] -> Xi + -> TcS [TypeEqn] +-- TyCon is definitely a type family +improve_wanted_top_fun_eqs fam_tc lhs_tys rhs_ty + | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc + = return (map snd $ tryInteractTopFam ops fam_tc lhs_tys rhs_ty) + + -- ToDo: use ideas in #23162 for closed type families; injectivity only for open + + -- See Note [Type inference for type families with injectivity] + -- Open, so look for inj + | Injective inj_args <- tyConInjectivityInfo fam_tc + = do { fam_envs <- getFamInstEnvs + ; top_eqns <- improve_injective_wanted_top fam_envs inj_args fam_tc lhs_tys rhs_ty + ; let local_eqns = improve_injective_wanted_famfam inj_args fam_tc lhs_tys rhs_ty + ; traceTcS "improve_wanted_top_fun_eqs" $ + vcat [ ppr fam_tc, text "local_eqns" <+> ppr local_eqns, text "top_eqns" <+> ppr top_eqns ] + -- xxx ToDo: this does both local and top => bug? + ; return (local_eqns ++ top_eqns) } + + | otherwise -- No injectivity + = return [] + +improve_injective_wanted_top :: FamInstEnvs -> [Bool] -> TyCon -> [TcType] -> Xi -> TcS [TypeEqn] +-- Interact with top-level instance declarations +-- See Section 5.2 in the Injective Type Families paper +improve_injective_wanted_top fam_envs inj_args fam_tc lhs_tys rhs_ty + = concatMapM do_one branches + where + branches :: [CoAxBranch] + branches | isOpenTypeFamilyTyCon fam_tc + , let fam_insts = lookupFamInstEnvByTyCon fam_envs fam_tc + = concatMap (fromBranches . coAxiomBranches . fi_axiom) fam_insts + + | Just ax <- isClosedSynFamilyTyConWithAxiom_maybe fam_tc + = fromBranches (coAxiomBranches ax) + + | otherwise + = [] + + do_one :: CoAxBranch -> TcS [TypeEqn] + do_one branch@(CoAxBranch { cab_tvs = branch_tvs, cab_lhs = branch_lhs_tys, cab_rhs = branch_rhs }) + | let in_scope1 = in_scope `extendInScopeSetList` branch_tvs + , Just subst <- tcUnifyTyForInjectivity False in_scope1 branch_rhs rhs_ty + -- False: matching, not unifying + = do { let inSubst tv = tv `elemVarEnv` getTvSubstEnv subst + unsubstTvs = filterOut inSubst branch_tvs + -- The order of unsubstTvs is important; it must be + -- in telescope order e.g. (k:*) (a:k) + + ; (_subst_tvs, subst1) <- instFlexiX subst unsubstTvs + -- If the current substitution bind [k -> *], and + -- one of the un-substituted tyvars is (a::k), we'd better + -- be sure to apply the current substitution to a's kind. + -- Hence instFlexiX. #13135 was an example. + + ; traceTcS "improve_inj_top" $ + vcat [ text "branch_rhs" <+> ppr branch_rhs + , text "rhs_ty" <+> ppr rhs_ty + , text "subst" <+> ppr subst + , text "subst1" <+> ppr subst1 ] + ; if apartnessCheck (substTys subst1 branch_lhs_tys) branch + then do { traceTcS "improv_inj_top1" (ppr branch_lhs_tys) + ; return (mkInjectivityEqns inj_args (map (substTy subst1) branch_lhs_tys) lhs_tys) } + -- NB: The fresh unification variables (from unsubstTvs) are on the left + -- See Note [Improvement orientation] + else do { traceTcS "improve_inj_top2" empty; return [] } } + | otherwise + = do { traceTcS "improve_inj_top:fail" (ppr branch_rhs $$ ppr rhs_ty $$ ppr in_scope $$ ppr branch_tvs) + ; return [] } + + in_scope = mkInScopeSet (tyCoVarsOfType rhs_ty) + + +improve_injective_wanted_famfam :: [Bool] -> TyCon -> [TcType] -> Xi -> [TypeEqn] +-- Interact with itself, specifically F s1 s2 ~ F t1 t2 +improve_injective_wanted_famfam inj_args fam_tc lhs_tys rhs_ty + | Just (tc, rhs_tys) <- tcSplitTyConApp_maybe rhs_ty + , tc == fam_tc + = mkInjectivityEqns inj_args lhs_tys rhs_tys + | otherwise + = [] + +mkInjectivityEqns :: [Bool] -> [TcType] -> [TcType] -> [TypeEqn] +-- When F s1 s2 s3 ~ F t1 t2 t3, and F has injectivity info [True,False,True] +-- return the equations [Pair s1 t1, Pair s3 t3] +mkInjectivityEqns inj_args lhs_args rhs_args + = [ Pair lhs_arg rhs_arg | (True, lhs_arg, rhs_arg) <- zip3 inj_args lhs_args rhs_args ] + +--------------------------------------------- +improveLocalFunEqs :: TyCon -> [TcType] -> EqCt -- F args ~ rhs + -> SolverStage () +-- Emit equalities from interaction between two equalities +improveLocalFunEqs fam_tc args eq_ct@(EqCt { eq_ev = work_ev, eq_rhs = rhs }) + = Stage $ + do { inerts <- getInertCans + ; let my_funeqs = get_my_funeqs inerts + ; imp <- if isGiven work_ev + then improveGivenLocalFunEqs my_funeqs fam_tc args work_ev rhs + else improveWantedLocalFunEqs my_funeqs fam_tc args work_ev rhs + ; if imp then startAgainWith (CEqCan eq_ct) + else continueWith () } + where + get_my_funeqs :: InertCans -> [EqCt] -- Mixture of Given and Wanted + get_my_funeqs (IC { inert_funeqs = funeqs }) + = [ funeq_ct | equal_ct_list <- findFunEqsByTyCon funeqs fam_tc + , funeq_ct <- equal_ct_list + , NomEq == eq_eq_rel funeq_ct ] + -- Representational equalities don't interact + -- with type family dependencies + +improveGivenLocalFunEqs :: [EqCt] -- Inert items, mixture of Given and Wanted + -> TyCon -> [TcType] -> CtEvidence -> Xi -- Work item (Given) + -> TcS Bool -- Always False (no unifications) +-- Emit equalities from interaction between two Given type-family equalities +-- e.g. (x+y1~z, x+y2~z) => (y1 ~ y2) +improveGivenLocalFunEqs funeqs_for_tc fam_tc work_args work_ev work_rhs + | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc + = do { mapM_ (do_one ops) funeqs_for_tc + ; return False } -- False: no unifications + | otherwise + = return False + where + given_co :: Coercion = ctEvCoercion work_ev + + do_one :: BuiltInSynFamily -> EqCt -> TcS () + -- Used only work-item is Given + do_one ops EqCt { eq_ev = inert_ev, eq_lhs = inert_lhs, eq_rhs = inert_rhs } + | isGiven inert_ev -- Given/Given interaction + , TyFamLHS _ inert_args <- inert_lhs -- Inert item is F inert_args ~ inert_rhs + , work_rhs `tcEqType` inert_rhs -- Both RHSs are the same + , -- So we have work_ev : F work_args ~ rhs + -- inert_ev : F inert_args ~ rhs + let pairs :: [(CoAxiomRule, TypeEqn)] + pairs = tryInteractInertFam ops fam_tc work_args inert_args + , not (null pairs) + = do { traceTcS "improveGivenLocalFunEqs" (vcat[ ppr fam_tc <+> ppr work_args + , text "work_ev" <+> ppr work_ev + , text "inert_ev" <+> ppr inert_ev + , ppr work_rhs + , ppr pairs ]) + ; emitNewGivens (ctEvLoc inert_ev) (map mk_ax_co pairs) } + -- This CtLoc for the new Givens doesn't reflect the + -- fact that it's a combination of Givens, but I don't + -- this that matters. + where + inert_co = ctEvCoercion inert_ev + mk_ax_co (ax,_) = (Nominal, mkAxiomCo ax [combined_co]) + where + combined_co = given_co `mkTransCo` mkSymCo inert_co + -- given_co :: F work_args ~ rhs + -- inert_co :: F inert_args ~ rhs + -- the_co :: F work_args ~ F inert_args + + do_one _ _ = return () + +improveWantedLocalFunEqs + :: [EqCt] -- Inert items (Given and Wanted) + -> TyCon -> [TcType] -> CtEvidence -> Xi -- Work item (Wanted) + -> TcS Bool -- True <=> some unifications +-- Emit improvement equalities for a Wanted constraint, by comparing +-- the current work item with inert CFunEqs (both Given and Wanted) +-- E.g. x + y ~ z, x + y' ~ z => [W] y ~ y' +-- +-- See Note [FunDep and implicit parameter reactions] +improveWantedLocalFunEqs funeqs_for_tc fam_tc args work_ev rhs + | null improvement_eqns + = return False + | otherwise + = do { traceTcS "interactFunEq improvements: " $ + vcat [ text "Eqns:" <+> ppr improvement_eqns + , text "Candidates:" <+> ppr funeqs_for_tc ] + ; unifyAndEmitFunDepWanteds work_ev improvement_eqns } + where + work_loc = ctEvLoc work_ev + work_pred = ctEvPred work_ev + fam_inj_info = tyConInjectivityInfo fam_tc + + -------------------- + improvement_eqns :: [FunDepEqn (CtLoc, RewriterSet)] + improvement_eqns + | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc + = -- Try built-in families, notably for arithmethic + concatMap (do_one_built_in ops rhs) funeqs_for_tc + + | Injective injective_args <- fam_inj_info + = -- Try improvement from type families with injectivity annotations + concatMap (do_one_injective injective_args rhs) funeqs_for_tc + + | otherwise + = [] + + -------------------- + do_one_built_in ops rhs (EqCt { eq_lhs = TyFamLHS _ iargs, eq_rhs = irhs, eq_ev = inert_ev }) + | irhs `tcEqType` rhs + = mk_fd_eqns inert_ev (map snd $ tryInteractInertFam ops fam_tc args iargs) + | otherwise + = [] + do_one_built_in _ _ _ = pprPanic "interactFunEq 1" (ppr fam_tc) -- TyVarLHS + + -------------------- + -- See Note [Type inference for type families with injectivity] + do_one_injective inj_args rhs (EqCt { eq_lhs = TyFamLHS _ inert_args + , eq_rhs = irhs, eq_ev = inert_ev }) + | rhs `tcEqType` irhs + = mk_fd_eqns inert_ev $ mkInjectivityEqns inj_args args inert_args + | otherwise + = [] + + do_one_injective _ _ _ = pprPanic "interactFunEq 2" (ppr fam_tc) -- TyVarLHS + + -------------------- + mk_fd_eqns :: CtEvidence -> [TypeEqn] -> [FunDepEqn (CtLoc, RewriterSet)] + mk_fd_eqns inert_ev eqns + | null eqns = [] + | otherwise = [ FDEqn { fd_qtvs = [], fd_eqs = eqns + , fd_loc = (loc, inert_rewriters) } ] + where + 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] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +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 Wanted constraint on +the injective argument + [W] t1 ~ t2 + +That in turn can help GHC solve constraints that would otherwise require +guessing. For example, consider the ambiguity check for + f :: F Int b -> Int +We get the constraint + [W] F Int b ~ F Int beta +where beta is a unification variable. Injectivity lets us pick beta ~ b. + +Injectivity information is also used at the call sites. For example: + g = f True +gives rise to + [W] F Int b ~ Bool +from which we can derive b. This requires looking at the defining equations of +a type family, ie. finding equation with a matching RHS (Bool in this example) +and inferring values of type variables (b in this example) from the LHS patterns +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 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 Wanteds in three places, depending on how we notice the +injectivity. + +1. When we have a [W] F tys1 ~ F tys2. This is handled in canEqCanLHS2, and +described in Note [Decomposing type family applications] in GHC.Tc.Solver.Equality + +2. When we have [W] F tys1 ~ T and [W] F tys2 ~ T. Note that neither of these +constraints rewrites the other, as they have different LHSs. This is done +in improveLocalFunEqs, called during the interactWithInertsStage. + +3. When we have [W] F tys ~ T and an equation for F that looks like F tys' = T. +This is done in improve_top_fun_eqs, called from the top-level reactions stage. + +See also Note [Injective type families] in GHC.Core.TyCon + +Note [Cache-caused loops] +~~~~~~~~~~~~~~~~~~~~~~~~~ +It is very dangerous to cache a rewritten wanted family equation as 'solved' in our +solved cache (which is the default behaviour or xCtEvidence), because the interaction +may not be contributing towards a solution. Here is an example: + +Initial inert set: + [W] g1 : F a ~ beta1 +Work item: + [W] g2 : F a ~ beta2 +The work item will react with the inert yielding the _same_ inert set plus: + (i) Will set g2 := g1 `cast` g3 + (ii) Will add to our solved cache that [S] g2 : F a ~ beta2 + (iii) Will emit [W] g3 : beta1 ~ beta2 +Now, the g3 work item will be spontaneously solved to [G] g3 : beta1 ~ beta2 +and then it will react the item in the inert ([W] g1 : F a ~ beta1). So it +will set + g1 := g ; sym g3 +and what is g? Well it would ideally be a new goal of type (F a ~ beta2) but +remember that we have this in our solved cache, and it is ... g2! In short we +created the evidence loop: + + g2 := g1 ; g3 + g3 := refl + g1 := g2 ; sym g3 + +To avoid this situation we do not cache as solved any workitems (or inert) +which did not really made a 'step' towards proving some goal. Solved's are +just an optimization so we don't lose anything in terms of completeness of +solving. +-} + {- ************************************************************************ * * ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -67,9 +67,6 @@ module GHC.Tc.Solver.Monad ( getTcEvTyCoVars, getTcEvBindsMap, setTcEvBindsMap, tcLookupClass, tcLookupId, tcLookupTyCon, - getUnifiedRef, - - -- Inerts updInertSet, updInertCans, getHasGivenEqs, setInertCans, @@ -84,7 +81,7 @@ module GHC.Tc.Solver.Monad ( lookupInertDict, -- The Model - kickOutAfterUnification, kickOutRewritable, + recordUnification, recordUnifications, kickOutRewritable, -- Inert Safe Haskell safe-overlap failures insertSafeOverlapFailureTcS, @@ -212,8 +209,6 @@ import Control.Monad import Data.Foldable hiding ( foldr1 ) import Data.IORef import Data.List ( mapAccumL ) -import Data.List.NonEmpty ( nonEmpty ) -import qualified Data.List.NonEmpty as NE import GHC.Types.SrcLoc import GHC.Rename.Env import GHC.LanguageExtensions as LangExt @@ -450,33 +445,6 @@ kickOutRewritable ko_spec new_fr , text "kicked_out =" <+> ppr kicked_out , text "Residual inerts =" <+> ppr ics' ]) } } -kickOutAfterUnification :: [TcTyVar] -> TcS () -kickOutAfterUnification tv_list - = case nonEmpty tv_list of - Nothing -> return () - Just tvs -> do { traceTcS "kickOutAfterUnification" (ppr min_tv_lvl $$ ppr tv_list) - ; setUnificationFlagTo min_tv_lvl } - where - min_tv_lvl = foldr1 minTcLevel (NE.map tcTyVarLevel tvs) - -{- - { let tv_set = mkVarSet tv_list - - ; n_kicked <- kickOutRewritable (KOAfterUnify tv_set) (Given, NomEq) - -- Given because the tv := xi is given; NomEq because - -- only nominal equalities are solved by unification - - -- Set the unification flag if we have done outer unifications - -- that might affect an earlier implication constraint - ; let min_tv_lvl = foldr1 minTcLevel (NE.map tcTyVarLevel tvs) - ; ambient_lvl <- getTcLevel - ; when (ambient_lvl `strictlyDeeperThan` min_tv_lvl) $ - setUnificationFlagTo min_tv_lvl - - ; traceTcS "kickOutAfterUnification" (ppr tvs $$ text "n_kicked =" <+> ppr n_kicked) - ; return n_kicked } --} - kickOutAfterFillingCoercionHole :: CoercionHole -> TcS () -- See Wrinkle (URW2) in Note [Unify only if the rewriter set is empty] -- in GHC.Tc.Solver.Equality @@ -940,11 +908,6 @@ data TcSEnv = TcSEnv { tcs_ev_binds :: EvBindsVar, - tcs_unified :: IORef Int, - -- The number of unification variables we have filled - -- The important thing is whether it is non-zero, so it - -- could equally well be a Bool instead of an Int. - tcs_unif_lvl :: IORef (Maybe TcLevel), -- The Unification Level Flag -- Outermost level at which we have unified a meta tyvar @@ -1131,8 +1094,7 @@ runTcSWithEvBinds' :: TcSMode -> TcS a -> TcM a runTcSWithEvBinds' mode ev_binds_var thing_inside - = do { unified_var <- TcM.newTcRef 0 - ; step_count <- TcM.newTcRef 0 + = do { step_count <- TcM.newTcRef 0 -- Make a fresh, empty inert set -- Subtle point: see (TGE6) in Note [Tracking Given equalities] @@ -1143,7 +1105,6 @@ runTcSWithEvBinds' mode ev_binds_var thing_inside ; wl_var <- TcM.newTcRef emptyWorkList ; unif_lvl_var <- TcM.newTcRef Nothing ; let env = TcSEnv { tcs_ev_binds = ev_binds_var - , tcs_unified = unified_var , tcs_unif_lvl = unif_lvl_var , tcs_count = step_count , tcs_inerts = inert_var @@ -1354,9 +1315,6 @@ setTcSMode :: TcSMode -> TcS a -> TcS a setTcSMode mode thing_inside = TcS (\env -> unTcS thing_inside (env { tcs_mode = mode })) -getUnifiedRef :: TcS (IORef Int) -getUnifiedRef = TcS (return . tcs_unified) - -- Getter of inerts and worklist getInertSetRef :: TcS (IORef InertSet) getInertSetRef = TcS (return . tcs_inerts) @@ -1817,13 +1775,11 @@ produced the same Derived constraint.) unifyTyVar :: TcTyVar -> TcType -> TcS () -- Unify a meta-tyvar with a type --- We keep track of how many unifications have happened in tcs_unified, --- -- We should never unify the same variable twice! unifyTyVar tv ty = assertPpr (isMetaTyVar tv) (ppr tv) $ do { liftZonkTcS (TcM.writeMetaTyVar tv ty) -- Produces a trace message - ; setUnificationFlagTo (tcTyVarLevel tv) } + ; recordUnification tv } reportUnifications :: TcS a -> TcS (Bool, a) -- Record whether any unifications are done by thing_inside @@ -1887,6 +1843,18 @@ getUnificationFlag -> do { TcM.writeTcRef ref Nothing ; return True } } +recordUnification :: TcTyVar -> TcS () +recordUnification tv = setUnificationFlagTo (tcTyVarLevel tv) + +recordUnifications :: [TcTyVar] -> TcS () +recordUnifications tvs + = case tvs of + [] -> return () + (tv:tvs) -> do { traceTcS "recordUnifications" (ppr min_tv_lvl $$ ppr tvs) + ; setUnificationFlagTo min_tv_lvl } + where + min_tv_lvl = foldr (minTcLevel . tcTyVarLevel) (tcTyVarLevel tv) tvs + setUnificationFlagTo :: TcLevel -> TcS () -- (setUnificationFlag i) sets the unification level to (Just i) -- unless it already is (Just j) where j <= i @@ -2251,8 +2219,8 @@ unifyForAllBody :: CtEvidence -> Role -> (UnifyEnv -> TcM a) unifyForAllBody ev role unify_body = do { (res, cts, unified) <- wrapUnifierX ev role unify_body - -- Kick out any inert constraint that we have unified - ; kickOutAfterUnification unified + -- Record the unificaions we have done + ; recordUnifications unified ; return (res, cts) } @@ -2271,6 +2239,9 @@ wrapUnifierTcS :: CtEvidence -> Role wrapUnifierTcS ev role do_unifications = do { (res, cts, unified) <- wrapUnifierX ev role do_unifications + -- Record the unificaions we have done + ; recordUnifications unified + -- Emit the deferred constraints -- See Note [Work-list ordering] in GHC.Tc.Solved.Equality -- @@ -2280,17 +2251,13 @@ wrapUnifierTcS ev role do_unifications ; unless (isEmptyBag cts) $ updWorkListTcS (extendWorkListChildEqs ev cts) - -- And kick out any inert constraint that we have unified - ; kickOutAfterUnification unified - ; return (res, cts, unified) } wrapUnifierX :: CtEvidence -> Role -> (UnifyEnv -> TcM a) -- Some calls to uType -> TcS (a, Bag Ct, [TcTyVar]) wrapUnifierX ev role do_unifications - = do { unif_count_ref <- getUnifiedRef - ; given_eq_lvl <- getInnermostGivenEqLevel + = do { given_eq_lvl <- getInnermostGivenEqLevel ; wrapTcS $ do { defer_ref <- TcM.newTcRef emptyBag ; unified_ref <- TcM.newTcRef [] @@ -2308,12 +2275,6 @@ wrapUnifierX ev role do_unifications ; cts <- TcM.readTcRef defer_ref ; unified <- TcM.readTcRef unified_ref - - -- Don't forget to update the count of variables - -- unified, lest we forget to iterate (#24146) - ; unless (null unified) $ - TcM.updTcRef unif_count_ref (+ (length unified)) - ; return (res, cts, unified) } } View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0240183357637242886b779215b04ff6... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0240183357637242886b779215b04ff6... You're receiving this email because of your account on gitlab.haskell.org.