diff options
Diffstat (limited to 'compiler/GHC/Tc/Solver/Interact.hs')
| -rw-r--r-- | compiler/GHC/Tc/Solver/Interact.hs | 530 |
1 files changed, 270 insertions, 260 deletions
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 } |