diff options
Diffstat (limited to 'compiler/GHC/Tc/Solver')
| -rw-r--r-- | compiler/GHC/Tc/Solver/Canonical.hs | 121 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver/Interact.hs | 128 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver/Monad.hs | 561 |
3 files changed, 545 insertions, 265 deletions
diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs index ce8bf24632..7586bd5ed5 100644 --- a/compiler/GHC/Tc/Solver/Canonical.hs +++ b/compiler/GHC/Tc/Solver/Canonical.hs @@ -4,9 +4,9 @@ module GHC.Tc.Solver.Canonical( canonicalize, - unifyDerived, + unifyDerived, unifyTest, UnifyTestResult(..), makeSuperClasses, - StopOrContinue(..), stopWith, continueWith, + StopOrContinue(..), stopWith, continueWith, andWhenContinue, solveCallStack -- For GHC.Tc.Solver ) where @@ -51,7 +51,8 @@ import GHC.Data.Bag import GHC.Utils.Monad import Control.Monad import Data.Maybe ( isJust, isNothing ) -import Data.List ( zip4 ) +import Data.List ( zip4, partition ) +import GHC.Types.Unique.Set( nonDetEltsUniqSet ) import GHC.Types.Basic import Data.Bifunctor ( bimap ) @@ -2246,10 +2247,10 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco -- If we have F a ~ F (F a), we want to swap. swap_for_occurs - | MTVU_OK () <- checkTyFamEq dflags fun_tc2 fun_args2 - (mkTyConApp fun_tc1 fun_args1) - , MTVU_Occurs <- checkTyFamEq dflags fun_tc1 fun_args1 - (mkTyConApp fun_tc2 fun_args2) + | CTE_OK <- checkTyFamEq dflags fun_tc2 fun_args2 + (mkTyConApp fun_tc1 fun_args1) + , CTE_Occurs <- checkTyFamEq dflags fun_tc1 fun_args1 + (mkTyConApp fun_tc2 fun_args2) = True | otherwise @@ -2274,8 +2275,8 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco -- This function handles the case where one side is a tyvar and the other is -- a type family application. Which to put on the left? --- If we can unify the variable, put it on the left, as this may be our only --- shot to unify. +-- If the tyvar is a touchable meta-tyvar, put it on the left, as this may +-- be our only shot to unify. -- Otherwise, put the function on the left, because it's generally better to -- rewrite away function calls. This makes types smaller. And it seems necessary: -- [W] F alpha ~ alpha @@ -2283,22 +2284,20 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco -- [W] G alpha beta ~ Int ( where we have type instance G a a = a ) -- If we end up with a stuck alpha ~ F alpha, we won't be able to solve this. -- Test case: indexed-types/should_compile/CEqCanOccursCheck --- It would probably work to always put the variable on the left, but we think --- it would be less efficient. canEqTyVarFunEq :: CtEvidence -- :: lhs ~ (rhs |> mco) -- or (rhs |> mco) ~ lhs if swapped -> EqRel -> SwapFlag - -> TyVar -> TcType -- lhs, pretty lhs - -> TyCon -> [Xi] -> TcType -- rhs fun, rhs args, pretty rhs + -> TyVar -> TcType -- lhs (or if swapped rhs), pretty lhs + -> TyCon -> [Xi] -> TcType -- rhs (or if swapped lhs) fun and args, pretty rhs -> MCoercion -- :: kind(rhs) ~N kind(lhs) -> TcS (StopOrContinue Ct) canEqTyVarFunEq ev eq_rel swapped tv1 ps_xi1 fun_tc2 fun_args2 ps_xi2 mco - = do { tclvl <- getTcLevel - ; dflags <- getDynFlags - ; if | isTouchableMetaTyVar tclvl tv1 - , MTVU_OK _ <- checkTyVarEq dflags YesTypeFamilies tv1 (ps_xi2 `mkCastTyMCo` mco) - -> canEqCanLHSFinish ev eq_rel swapped (TyVarLHS tv1) - (ps_xi2 `mkCastTyMCo` mco) + = do { can_unify <- unifyTest ev tv1 rhs + ; dflags <- getDynFlags + ; if | case can_unify of { NoUnify -> False; _ -> True } + , CTE_OK <- checkTyVarEq dflags YesTypeFamilies tv1 rhs + -> canEqCanLHSFinish ev eq_rel swapped (TyVarLHS tv1) rhs + | otherwise -> do { new_ev <- rewriteCastedEquality ev eq_rel swapped (mkTyVarTy tv1) (mkTyConApp fun_tc2 fun_args2) @@ -2308,6 +2307,82 @@ canEqTyVarFunEq ev eq_rel swapped tv1 ps_xi1 fun_tc2 fun_args2 ps_xi2 mco (ps_xi1 `mkCastTyMCo` sym_mco) } } where sym_mco = mkTcSymMCo mco + rhs = ps_xi2 `mkCastTyMCo` mco + +data UnifyTestResult + -- See Note [Solve by unification] in GHC.Tc.Solver.Interact + -- which points out that having UnifySameLevel is just an optimisation; + -- we could manage with UnifyOuterLevel alone (suitably renamed) + = UnifySameLevel + | UnifyOuterLevel [TcTyVar] -- Promote these + TcLevel -- ..to this level + | NoUnify + +instance Outputable UnifyTestResult where + ppr UnifySameLevel = text "UnifySameLevel" + ppr (UnifyOuterLevel tvs lvl) = text "UnifyOuterLevel" <> parens (ppr lvl <+> ppr tvs) + ppr NoUnify = text "NoUnify" + +unifyTest :: CtEvidence -> TcTyVar -> TcType -> TcS UnifyTestResult +-- This is the key test for untouchability: +-- See Note [Unification preconditions] in GHC.Tc.Utils.Unify +-- and Note [Solve by unification] in GHC.Tc.Solver.Interact +unifyTest ev tv1 rhs + | not (isGiven ev) -- See Note [Do not unify Givens] + , MetaTv { mtv_tclvl = tv_lvl, mtv_info = info } <- tcTyVarDetails tv1 + , canSolveByUnification info rhs + = do { ambient_lvl <- getTcLevel + ; given_eq_lvl <- getInnermostGivenEqLevel + + ; if | tv_lvl `sameDepthAs` ambient_lvl + -> return UnifySameLevel + + | tv_lvl `deeperThanOrSame` given_eq_lvl -- No intervening given equalities + , all (does_not_escape tv_lvl) free_skols -- No skolem escapes + -> return (UnifyOuterLevel free_metas tv_lvl) + + | otherwise + -> return NoUnify } + | otherwise + = return NoUnify + where + (free_metas, free_skols) = partition isPromotableMetaTyVar $ + nonDetEltsUniqSet $ + tyCoVarsOfType rhs + + does_not_escape tv_lvl fv + | isTyVar fv = tv_lvl `deeperThanOrSame` tcTyVarLevel fv + | otherwise = True + -- Coercion variables are not an escape risk + -- If an implication binds a coercion variable, it'll have equalities, + -- so the "intervening given equalities" test above will catch it + -- Coercion holes get filled with coercions, so again no problem. + +{- Note [Do not unify Givens] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider this GADT match + data T a where + T1 :: T Int + ... + + f x = case x of + T1 -> True + ... + +So we get f :: T alpha[1] -> beta[1] + x :: T alpha[1] +and from the T1 branch we get the implication + forall[2] (alpha[1] ~ Int) => beta[1] ~ Bool + +Now, clearly we don't want to unify alpha:=Int! Yet at the moment we +process [G] alpha[1] ~ Int, we don't have any given-equalities in the +inert set, and hence there are no given equalities to make alpha untouchable. + +(NB: if it were alpha[2] ~ Int, this argument wouldn't hold. But that +almost never happens, and will never happen at all if we cure #18929.) + +Simple solution: never unify in Givens! +-} -- The RHS here is either not CanEqLHS, or it's one that we -- want to rewrite the LHS to (as per e.g. swapOverTyVars) @@ -2427,11 +2502,11 @@ canEqOK :: DynFlags -> EqRel -> CanEqLHS -> Xi -> CanEqOK canEqOK dflags eq_rel lhs rhs = ASSERT( good_rhs ) case checkTypeEq dflags YesTypeFamilies lhs rhs of - MTVU_OK () -> CanEqOK - MTVU_Bad -> CanEqNotOK OtherCIS + CTE_OK -> CanEqOK + CTE_Bad -> CanEqNotOK OtherCIS -- Violation of TyEq:F - MTVU_HoleBlocker -> CanEqNotOK (BlockedCIS holes) + CTE_HoleBlocker -> CanEqNotOK (BlockedCIS holes) where holes = coercionHolesOfType rhs -- This is the case detailed in -- Note [Equalities with incompatible kinds] @@ -2440,7 +2515,7 @@ canEqOK dflags eq_rel lhs rhs -- These are both a violation of TyEq:OC, but we -- want to differentiate for better production of -- error messages - MTVU_Occurs | TyVarLHS tv <- lhs + CTE_Occurs | TyVarLHS tv <- lhs , isInsolubleOccursCheck eq_rel tv rhs -> CanEqNotOK InsolubleCIS -- If we have a ~ [a], it is not canonical, and in particular -- we don't want to rewrite existing inerts with it, otherwise diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs index dc20b90260..e8ab8ad82a 100644 --- a/compiler/GHC/Tc/Solver/Interact.hs +++ b/compiler/GHC/Tc/Solver/Interact.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE CPP #-} +{-# LANGUAGE CPP, MultiWayIf #-} {-# OPTIONS_GHC -Wno-incomplete-record-updates #-} {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} @@ -14,7 +14,6 @@ import GHC.Prelude import GHC.Types.Basic ( SwapFlag(..), infinity, IntWithInf, intGtLimit ) import GHC.Tc.Solver.Canonical -import GHC.Tc.Utils.Unify( canSolveByUnification ) import GHC.Types.Var.Set import GHC.Core.Type as Type import GHC.Core.InstEnv ( DFunInstType ) @@ -39,6 +38,7 @@ import GHC.Tc.Types import GHC.Tc.Types.Constraint import GHC.Core.Predicate import GHC.Tc.Types.Origin +import GHC.Tc.Utils.TcMType( promoteMetaTyVarTo ) import GHC.Tc.Solver.Monad import GHC.Data.Bag import GHC.Utils.Monad ( concatMapM, foldlM ) @@ -106,8 +106,6 @@ solveSimpleGivens givens go new_givens } solveSimpleWanteds :: Cts -> TcS WantedConstraints --- NB: 'simples' may contain /derived/ equalities, floated --- out from a nested implication. So don't discard deriveds! -- The result is not necessarily zonked solveSimpleWanteds simples = do { traceTcS "solveSimpleWanteds {" (ppr simples) @@ -430,12 +428,11 @@ interactWithInertsStage :: WorkItem -> TcS (StopOrContinue Ct) interactWithInertsStage wi = do { inerts <- getTcSInerts - ; lvl <- getTcLevel ; let ics = inert_cans inerts ; case wi of - CEqCan {} -> interactEq lvl ics wi - CIrredCan {} -> interactIrred ics wi - CDictCan {} -> interactDict ics wi + CEqCan {} -> interactEq ics wi + CIrredCan {} -> interactIrred ics wi + CDictCan {} -> interactDict ics wi _ -> pprPanic "interactWithInerts" (ppr wi) } -- CNonCanonical have been canonicalised @@ -734,25 +731,26 @@ Example of (b): assume a top-level class and instance declaration: Assume we have started with an implication: - forall c. Eq c => { wc_simple = D [c] c [W] } + forall c. Eq c => { wc_simple = [W] D [c] c } -which we have simplified to: +which we have simplified to, with a Derived constraing coming from +D's functional dependency: - forall c. Eq c => { wc_simple = D [c] c [W] - (c ~ [c]) [D] } + forall c. Eq c => { wc_simple = [W] D [c] c [W] + [D] (c ~ [c]) } -For some reason, e.g. because we floated an equality somewhere else, -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: +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: - (D [c] c) [W] - (c ~ [c]) [D] + [W] (D [c] c) + [D] (c ~ [c]) which will result in two Deriveds to end up in the insoluble set: - wc_simple = D [c] c [W] - (c ~ [c]) [D], (c ~ [c]) [D] + wc_simple = [W] D [c] c + [D] (c ~ [c]) + [D] (c ~ [c]) -} {- @@ -1439,8 +1437,8 @@ inertsCanDischarge inerts lhs rhs fr | otherwise = False -- Work item is fully discharged -interactEq :: TcLevel -> InertCans -> Ct -> TcS (StopOrContinue Ct) -interactEq tclvl inerts workItem@(CEqCan { cc_lhs = lhs +interactEq :: InertCans -> Ct -> TcS (StopOrContinue Ct) +interactEq inerts workItem@(CEqCan { cc_lhs = lhs , cc_rhs = rhs , cc_ev = ev , cc_eq_rel = eq_rel }) @@ -1465,24 +1463,43 @@ interactEq tclvl inerts workItem@(CEqCan { cc_lhs = lhs = do { traceTcS "Not unifying representational equality" (ppr workItem) ; continueWith workItem } - -- try improvement, if possible - | TyFamLHS fam_tc fam_args <- lhs - , isImprovable ev - = do { improveLocalFunEqs ev inerts fam_tc fam_args rhs - ; continueWith workItem } - - | TyVarLHS tv <- lhs - , canSolveByUnification tclvl tv rhs - = do { solveByUnification ev tv rhs - ; n_kicked <- kickOutAfterUnification tv - ; return (Stop ev (text "Solved by unification" <+> pprKicked n_kicked)) } - | otherwise - = continueWith workItem - -interactEq _ _ wi = pprPanic "interactEq" (ppr wi) - -solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS () + = 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 + ; continueWith workItem } + +interactEq _ wi = pprPanic "interactEq" (ppr wi) + +---------------------- +-- We have a meta-tyvar on the left, and metaTyVarUpateOK has said "yes" +-- So try to solve by unifying. +-- Three reasons why not: +-- Skolem escape +-- Given equalities (GADTs) +-- Unifying a TyVarTv with a non-tyvar type +tryToSolveByUnification :: Ct -> CtEvidence + -> TcTyVar -- LHS tyvar + -> TcType -- RHS + -> TcS (StopOrContinue Ct) +tryToSolveByUnification work_item ev tv rhs + = do { can_unify <- unifyTest ev tv rhs + ; traceTcS "tryToSolveByUnification" (vcat [ ppr tv <+> char '~' <+> ppr rhs + , ppr can_unify ]) + + ; case can_unify of + NoUnify -> continueWith work_item + -- For the latter two cases see Note [Solve by unification] + UnifySameLevel -> solveByUnification ev tv rhs + UnifyOuterLevel free_metas tv_lvl + -> do { wrapTcS $ mapM_ (promoteMetaTyVarTo tv_lvl) free_metas + ; setUnificationFlag tv_lvl + ; solveByUnification 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 @@ -1504,9 +1521,10 @@ solveByUnification wd tv xi text "Coercion:" <+> pprEq tv_ty xi, text "Left Kind is:" <+> ppr (tcTypeKind tv_ty), text "Right Kind is:" <+> ppr (tcTypeKind xi) ] - ; unifyTyVar tv xi - ; setEvBindIfWanted wd (evCoercion (mkTcNomReflCo xi)) } + ; setEvBindIfWanted wd (evCoercion (mkTcNomReflCo xi)) + ; n_kicked <- kickOutAfterUnification tv + ; return (Stop wd (text "Solved by unification" <+> pprKicked n_kicked)) } {- Note [Avoid double unifications] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1542,6 +1560,34 @@ and we want to get alpha := N b. See also #15144, which was caused by unifying a representational equality. +Note [Solve by unification] +~~~~~~~~~~~~~~~~~~~~~~~~~~~ +If we solve + alpha[n] ~ ty +by unification, there are two cases to consider + +* UnifySameLevel: if the ambient level is 'n', then + we can simply update alpha := ty, and do nothing else + +* UnifyOuterLevel free_metas n: if the ambient level is greater than + 'n' (the level of alpha), in addition to setting alpha := ty we must + do two other things: + + 1. Promote all the free meta-vars of 'ty' to level n. After all, + alpha[n] is at level n, and so if we set, say, + alpha[n] := Maybe beta[m], + we must ensure that when unifying beta we do skolem-escape checks + etc relevent to level n. Simple way to do that: promote beta to + level n. + + 2. Set the Unification Level Flag to record that a level-n unification has + taken place. See Note [The Unification Level Flag] in GHC.Tc.Solver.Monad + +NB: UnifySameLevel is just an optimisation for UnifyOuterLevel. Promotion +would be a no-op, and setting the unification flag unnecessarily would just +make the solver iterate more often. (We don't need to iterate when unifying +at the ambient level becuase of the kick-out mechanism.) + ************************************************************************ * * diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs index 76d9316bf6..2560a8e185 100644 --- a/compiler/GHC/Tc/Solver/Monad.hs +++ b/compiler/GHC/Tc/Solver/Monad.hs @@ -17,7 +17,7 @@ module GHC.Tc.Solver.Monad ( -- The TcS monad TcS, runTcS, runTcSDeriveds, runTcSWithEvBinds, runTcSInerts, - failTcS, warnTcS, addErrTcS, + failTcS, warnTcS, addErrTcS, wrapTcS, runTcSEqualities, nestTcS, nestImplicTcS, setEvBindsTcS, emitImplicationTcS, emitTvImplicationTcS, @@ -31,6 +31,7 @@ module GHC.Tc.Solver.Monad ( panicTcS, traceTcS, traceFireTcS, bumpStepCountTcS, csTraceTcS, wrapErrTcS, wrapWarnTcS, + resetUnificationFlag, setUnificationFlag, -- Evidence creation and transformation MaybeNew(..), freshGoals, isFresh, getEvExpr, @@ -60,7 +61,7 @@ module GHC.Tc.Solver.Monad ( updInertTcS, updInertCans, updInertDicts, updInertIrreds, getHasGivenEqs, setInertCans, getInertEqs, getInertCans, getInertGivens, - getInertInsols, + getInertInsols, getInnermostGivenEqLevel, getTcSInerts, setTcSInerts, matchableGivens, prohibitedSuperClassSolve, mightMatchLater, getUnsolvedInerts, @@ -186,7 +187,6 @@ import Control.Monad import GHC.Utils.Monad import Data.IORef import Data.List ( partition, mapAccumL ) -import qualified Data.Semigroup as S import Data.List.NonEmpty ( NonEmpty(..), cons, toList, nonEmpty ) import qualified Data.List.NonEmpty as NE import Control.Arrow ( first ) @@ -418,12 +418,14 @@ instance Outputable InertSet where emptyInertCans :: InertCans emptyInertCans - = IC { inert_eqs = emptyDVarEnv - , inert_dicts = emptyDicts - , inert_safehask = emptyDicts - , inert_funeqs = emptyFunEqs - , inert_insts = [] - , inert_irreds = emptyCts } + = IC { inert_eqs = emptyDVarEnv + , inert_given_eq_lvl = topTcLevel + , inert_given_eqs = False + , inert_dicts = emptyDicts + , inert_safehask = emptyDicts + , inert_funeqs = emptyFunEqs + , inert_insts = [] + , inert_irreds = emptyCts } emptyInert :: InertSet emptyInert @@ -697,6 +699,19 @@ data InertCans -- See Note [Detailed InertCans Invariants] for more -- Irreducible predicates that cannot be made canonical, -- and which don't interact with others (e.g. (c a)) -- and insoluble predicates (e.g. Int ~ Bool, or a ~ [a]) + + , inert_given_eq_lvl :: TcLevel + -- The TcLevel of the innermost implication that has a Given + -- equality of the sort that make a unification variable untouchable + -- (see Note [Unification preconditions] in GHC.Tc.Utils.Unify). + -- See Note [Tracking Given equalities] below + + , inert_given_eqs :: Bool + -- True <=> The inert Givens *at this level* (tcl_tclvl) + -- could includes at least one equality /other than/ a + -- let-bound skolem equality. + -- Reason: report these givens when reporting a failed equality + -- See Note [Tracking Given equalities] } type InertEqs = DTyVarEnv EqualCtList @@ -730,7 +745,126 @@ listToEqualCtList :: [Ct] -> Maybe EqualCtList -- non-empty listToEqualCtList cts = EqualCtList <$> nonEmpty cts -{- Note [Detailed InertCans Invariants] +{- Note [Tracking Given equalities] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +For reasons described in (UNTOUCHABLE) in GHC.Tc.Utils.Unify +Note [Unification preconditions], we can't unify + alpha[2] ~ Int +under a level-4 implication if there are any Given equalities +bound by the implications at level 3 of 4. To that end, the +InertCans tracks + + inert_given_eq_lvl :: TcLevel + -- The TcLevel of the innermost implication that has a Given + -- equality of the sort that make a unification variable untouchable + -- (see Note [Unification preconditions] in GHC.Tc.Utils.Unify). + +We update inert_given_eq_lvl whenever we add a Given to the +inert set, in updateGivenEqs. + +Then a unification variable alpha[n] is untouchable iff + n < inert_given_eq_lvl +that is, if the unification variable was born outside an +enclosing Given equality. + +Exactly which constraints should trigger (UNTOUCHABLE), and hence +should update inert_given_eq_lvl? + +* We do /not/ need to worry about let-bound skolems, such ast + forall[2] a. a ~ [b] => blah + See Note [Let-bound skolems] + +* Consider an implication + forall[2]. beta[1] => alpha[1] ~ Int + where beta is a unification variable that has already been unified + to () in an outer scope. Then alpha[1] is perfectly touchable and + we can unify alpha := Int. So when deciding whether the givens contain + an equality, we should canonicalise first, rather than just looking at + the /original/ givens (#8644). + + * However, we must take account of *potential* equalities. Consider the + same example again, but this time we have /not/ yet unified beta: + forall[2] beta[1] => ...blah... + + Because beta might turn into an equality, updateGivenEqs conservatively + treats it as a potential equality, and updates inert_give_eq_lvl + + * What about something like forall[2] a b. a ~ F b => [W] alpha[1] ~ X y z? + + That Given cannot affect the Wanted, because the Given is entirely + *local*: it mentions only skolems bound in the very same + implication. Such equalities need not make alpha untouchable. (Test + case typecheck/should_compile/LocalGivenEqs has a real-life + motivating example, with some detailed commentary.) + Hence the 'mentionsOuterVar' test in updateGivenEqs. + + However, solely to support better error messages + (see Note [HasGivenEqs] in GHC.Tc.Types.Constraint) we also track + these "local" equalities in the boolean inert_given_eqs field. + This field is used only to set the ic_given_eqs field to LocalGivenEqs; + see the function getHasGivenEqs. + + Here is a simpler case that triggers this behaviour: + + data T where + MkT :: F a ~ G b => a -> b -> T + + f (MkT _ _) = True + + Because of this behaviour around local equality givens, we can infer the + type of f. This is typecheck/should_compile/LocalGivenEqs2. + + * We need not look at the equality relation involved (nominal vs + representational), because representational equalities can still + imply nominal ones. For example, if (G a ~R G b) and G's argument's + role is nominal, then we can deduce a ~N b. + +Note [Let-bound skolems] +~~~~~~~~~~~~~~~~~~~~~~~~ +If * the inert set contains a canonical Given CEqCan (a ~ ty) +and * 'a' is a skolem bound in this very implication, + +then: +a) The Given is pretty much a let-binding, like + f :: (a ~ b->c) => a -> a + Here the equality constraint is like saying + let a = b->c in ... + It is not adding any new, local equality information, + and hence can be ignored by has_given_eqs + +b) 'a' will have been completely substituted out in the inert set, + so we can safely discard it. + +For an example, see #9211. + +See also GHC.Tc.Utils.Unify Note [Deeper level on the left] for how we ensure +that the right variable is on the left of the equality when both are +tyvars. + +You might wonder whether the skolem really needs to be bound "in the +very same implication" as the equuality constraint. +Consider this (c.f. #15009): + + data S a where + MkS :: (a ~ Int) => S a + + g :: forall a. S a -> a -> blah + g x y = let h = \z. ( z :: Int + , case x of + MkS -> [y,z]) + in ... + +From the type signature for `g`, we get `y::a` . Then when we +encounter the `\z`, we'll assign `z :: alpha[1]`, say. Next, from the +body of the lambda we'll get + + [W] alpha[1] ~ Int -- From z::Int + [W] forall[2]. (a ~ Int) => [W] alpha[1] ~ a -- From [y,z] + +Now, unify alpha := a. Now we are stuck with an unsolved alpha~Int! +So we must treat alpha as untouchable under the forall[2] implication. + +Note [Detailed InertCans Invariants] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The InertCans represents a collection of constraints with the following properties: @@ -1027,6 +1161,8 @@ instance Outputable InertCans where ppr (IC { inert_eqs = eqs , inert_funeqs = funeqs, inert_dicts = dicts , inert_safehask = safehask, inert_irreds = irreds + , inert_given_eq_lvl = ge_lvl + , inert_given_eqs = given_eqs , inert_insts = insts }) = braces $ vcat @@ -1043,6 +1179,8 @@ instance Outputable InertCans where text "Irreds =" <+> pprCts irreds , ppUnless (null insts) $ text "Given instances =" <+> vcat (map ppr insts) + , text "Innermost given equalities =" <+> ppr ge_lvl + , text "Given eqs at this level =" <+> ppr given_eqs ] where folder (EqualCtList eqs) rest = nonEmptyToBag eqs `andCts` rest @@ -1456,20 +1594,32 @@ findEq icans (TyFamLHS fun_tc fun_args) addInertForAll :: QCInst -> TcS () -- Add a local Given instance, typically arising from a type signature addInertForAll new_qci - = do { ics <- getInertCans - ; insts' <- add_qci (inert_insts ics) - ; setInertCans (ics { inert_insts = insts' }) } + = do { ics <- getInertCans + ; ics1 <- add_qci ics + + -- Update given equalities. C.f updateGivenEqs + ; tclvl <- getTcLevel + ; let pred = qci_pred new_qci + not_equality = isClassPred pred && not (isEqPred pred) + -- True <=> definitely not an equality + -- A qci_pred like (f a) might be an equality + + ics2 | not_equality = ics1 + | otherwise = ics1 { inert_given_eq_lvl = tclvl + , inert_given_eqs = True } + + ; setInertCans ics2 } where - add_qci :: [QCInst] -> TcS [QCInst] + add_qci :: InertCans -> TcS InertCans -- See Note [Do not add duplicate quantified instances] - add_qci qcis + add_qci ics@(IC { inert_insts = qcis }) | any same_qci qcis = do { traceTcS "skipping duplicate quantified instance" (ppr new_qci) - ; return qcis } + ; return ics } | otherwise = do { traceTcS "adding new inert quantified instance" (ppr new_qci) - ; return (new_qci : qcis) } + ; return (ics { inert_insts = new_qci : qcis }) } same_qci old_qci = tcEqType (ctEvPred (qci_ev old_qci)) (ctEvPred (qci_ev new_qci)) @@ -1523,7 +1673,8 @@ addInertCan ct ; ics <- getInertCans ; ct <- maybeEmitShadow ics ct ; ics <- maybeKickOut ics ct - ; setInertCans (add_item ics ct) + ; tclvl <- getTcLevel + ; setInertCans (add_item tclvl ics ct) ; traceTcS "addInertCan }" $ empty } @@ -1536,23 +1687,54 @@ maybeKickOut ics ct | otherwise = return ics -add_item :: InertCans -> Ct -> InertCans -add_item ics item@(CEqCan { cc_lhs = TyFamLHS tc tys }) - = ics { inert_funeqs = addCanFunEq (inert_funeqs ics) tc tys item } - -add_item ics item@(CEqCan { cc_lhs = TyVarLHS tv }) - = ics { inert_eqs = addTyEq (inert_eqs ics) tv item } - -add_item ics@(IC { inert_irreds = irreds }) item@(CIrredCan {}) - = ics { inert_irreds = irreds `Bag.snocBag` item } - -add_item ics item@(CDictCan { cc_class = cls, cc_tyargs = tys }) +add_item :: TcLevel -> InertCans -> Ct -> InertCans +add_item tc_lvl + ics@(IC { inert_funeqs = funeqs, inert_eqs = eqs }) + item@(CEqCan { cc_lhs = lhs }) + = updateGivenEqs tc_lvl item $ + case lhs of + TyFamLHS tc tys -> ics { inert_funeqs = addCanFunEq funeqs tc tys item } + TyVarLHS tv -> ics { inert_eqs = addTyEq eqs tv item } + +add_item tc_lvl ics@(IC { inert_irreds = irreds }) item@(CIrredCan {}) + = updateGivenEqs tc_lvl item $ -- An Irred might turn out to be an + -- equality, so we play safe + ics { inert_irreds = irreds `Bag.snocBag` item } + +add_item _ ics item@(CDictCan { cc_class = cls, cc_tyargs = tys }) = ics { inert_dicts = addDict (inert_dicts ics) cls tys item } -add_item _ item +add_item _ _ item = pprPanic "upd_inert set: can't happen! Inserting " $ ppr item -- Can't be CNonCanonical because they only land in inert_irreds +updateGivenEqs :: TcLevel -> Ct -> InertCans -> InertCans +-- Set the inert_given_eq_level to the current level (tclvl) +-- if the constraint is a given equality that should prevent +-- filling in an outer unification variable. +-- See See Note [Tracking Given equalities] +updateGivenEqs tclvl ct inerts@(IC { inert_given_eq_lvl = ge_lvl }) + | not (isGivenCt ct) = inerts + | not_equality ct = inerts -- See Note [Let-bound skolems] + | otherwise = inerts { inert_given_eq_lvl = ge_lvl' + , inert_given_eqs = True } + where + ge_lvl' | mentionsOuterVar tclvl (ctEvidence ct) + -- Includes things like (c a), which *might* be an equality + = tclvl + | otherwise + = ge_lvl + + not_equality :: Ct -> Bool + -- True <=> definitely not an equality of any kind + -- except for a let-bound skolem, which doesn't count + -- See Note [Let-bound skolems] + -- NB: no need to spot the boxed CDictCan (a ~ b) because its + -- superclass (a ~# b) will be a CEqCan + not_equality (CEqCan { cc_lhs = TyVarLHS tv }) = not (isOuterTyVar tclvl tv) + not_equality (CDictCan {}) = True + not_equality _ = False + ----------------------------------------- kickOutRewritable :: CtFlavourRole -- Flavour/role of the equality that -- is being added to the inert set @@ -1596,7 +1778,6 @@ kick_out_rewritable :: CtFlavourRole -- Flavour/role of the equality that kick_out_rewritable new_fr new_lhs ics@(IC { inert_eqs = tv_eqs , inert_dicts = dictmap - , inert_safehask = safehask , inert_funeqs = funeqmap , inert_irreds = irreds , inert_insts = old_insts }) @@ -1610,12 +1791,12 @@ kick_out_rewritable new_fr new_lhs | otherwise = (kicked_out, inert_cans_in) where - inert_cans_in = IC { inert_eqs = tv_eqs_in - , inert_dicts = dicts_in - , inert_safehask = safehask -- ?? - , inert_funeqs = feqs_in - , inert_irreds = irs_in - , inert_insts = insts_in } + -- inert_safehask stays unchanged; is that right? + inert_cans_in = ics { inert_eqs = tv_eqs_in + , inert_dicts = dicts_in + , inert_funeqs = feqs_in + , inert_irreds = irs_in + , inert_insts = insts_in } kicked_out :: WorkList -- NB: use extendWorkList to ensure that kicked-out equalities get priority @@ -1968,6 +2149,10 @@ updInertIrreds upd_fn getInertEqs :: TcS (DTyVarEnv EqualCtList) getInertEqs = do { inert <- getInertCans; return (inert_eqs inert) } +getInnermostGivenEqLevel :: TcS TcLevel +getInnermostGivenEqLevel = do { inert <- getInertCans + ; return (inert_given_eq_lvl inert) } + getInertInsols :: TcS Cts -- Returns insoluble equality constraints -- specifically including Givens @@ -2077,63 +2262,46 @@ getUnsolvedInerts getHasGivenEqs :: TcLevel -- TcLevel of this implication -> TcS ( HasGivenEqs -- are there Given equalities? , Cts ) -- Insoluble equalities arising from givens --- See Note [When does an implication have given equalities?] +-- See Note [Tracking Given equalities] getHasGivenEqs tclvl - = do { inerts@(IC { inert_eqs = ieqs, inert_funeqs = funeqs, inert_irreds = irreds }) + = do { inerts@(IC { inert_irreds = irreds + , inert_given_eqs = given_eqs + , inert_given_eq_lvl = ge_lvl }) <- getInertCans - ; let has_given_eqs = foldMap check_local_given_ct irreds - S.<> foldMap (lift_equal_ct_list check_local_given_tv_eq) ieqs - S.<> foldMapFunEqs (lift_equal_ct_list check_local_given_ct) funeqs - insols = filterBag insolubleEqCt irreds + ; let insols = filterBag insolubleEqCt irreds -- Specifically includes ones that originated in some -- outer context but were refined to an insoluble by -- a local equality; so do /not/ add ct_given_here. + -- See Note [HasGivenEqs] in GHC.Tc.Types.Constraint, and + -- Note [Tracking Given equalities] in this module + has_ge | ge_lvl == tclvl = MaybeGivenEqs + | given_eqs = LocalGivenEqs + | otherwise = NoGivenEqs + ; traceTcS "getHasGivenEqs" $ - vcat [ text "has_given_eqs:" <+> ppr has_given_eqs + vcat [ text "given_eqs:" <+> ppr given_eqs + , text "ge_lvl:" <+> ppr ge_lvl + , text "ambient level:" <+> ppr tclvl , text "Inerts:" <+> ppr inerts , text "Insols:" <+> ppr insols] - ; return (has_given_eqs, insols) } - where - check_local_given_ct :: Ct -> HasGivenEqs - check_local_given_ct ct - | given_here ev = if mentions_outer_var ev then MaybeGivenEqs else LocalGivenEqs - | otherwise = NoGivenEqs - where - ev = ctEvidence ct - - lift_equal_ct_list :: (Ct -> HasGivenEqs) -> EqualCtList -> HasGivenEqs - -- returns NoGivenEqs for non-singleton lists, as Given lists are always - -- singletons - lift_equal_ct_list check (EqualCtList (ct :| [])) = check ct - lift_equal_ct_list _ _ = NoGivenEqs - - check_local_given_tv_eq :: Ct -> HasGivenEqs - check_local_given_tv_eq (CEqCan { cc_lhs = TyVarLHS tv, cc_ev = ev}) - | given_here ev - = if is_outer_var tv then MaybeGivenEqs else NoGivenEqs - -- See Note [Let-bound skolems] - | otherwise - = NoGivenEqs - check_local_given_tv_eq other_ct = check_local_given_ct other_ct - - given_here :: CtEvidence -> Bool - -- True for a Given bound by the current implication, - -- i.e. the current level - given_here ev = isGiven ev - && tclvl == ctLocLevel (ctEvLoc ev) - - mentions_outer_var :: CtEvidence -> Bool - mentions_outer_var = anyFreeVarsOfType is_outer_var . ctEvPred - - is_outer_var :: TyCoVar -> Bool - is_outer_var tv - -- NB: a meta-tv alpha[3] may end up unifying with skolem b[2], - -- so treat it as an "outer" var, even at level 3. - -- This will become redundant after fixing #18929. - | isTyVar tv = isTouchableMetaTyVar tclvl tv || - tclvl `strictlyDeeperThan` tcTyVarLevel tv - | otherwise = False + ; return (has_ge, insols) } + +mentionsOuterVar :: TcLevel -> CtEvidence -> Bool +mentionsOuterVar tclvl ev + = anyFreeVarsOfType (isOuterTyVar tclvl) $ + ctEvPred ev + +isOuterTyVar :: TcLevel -> TyCoVar -> Bool +-- True of a type variable that comes from a +-- shallower level than the ambient level (tclvl) +isOuterTyVar tclvl tv + | isTyVar tv = tclvl `strictlyDeeperThan` tcTyVarLevel tv + || isPromotableMetaTyVar tv + -- isPromotable: a meta-tv alpha[3] may end up unifying with skolem b[2], + -- so treat it as an "outer" var, even at level 3. + -- This will become redundant after fixing #18929. + | otherwise = False -- Coercion variables; doesn't much matter -- | Returns Given constraints that might, -- potentially, match the given pred. This is used when checking to see if a @@ -2267,112 +2435,6 @@ Examples: This treatment fixes #18910 and is tested in typecheck/should_compile/InstanceGivenOverlap{,2} -Note [When does an implication have given equalities?] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider an implication - beta => alpha ~ Int -where beta is a unification variable that has already been unified -to () in an outer scope. Then we can float the (alpha ~ Int) out -just fine. So when deciding whether the givens contain an equality, -we should canonicalise first, rather than just looking at the original -givens (#8644). - -So we simply look at the inert, canonical Givens and see if there are -any equalities among them, the calculation of has_given_eqs. There -are some wrinkles: - - * We must know which ones are bound in *this* implication and which - are bound further out. We can find that out from the TcLevel - of the Given, which is itself recorded in the tcl_tclvl field - of the TcLclEnv stored in the Given (ev_given_here). - - What about interactions between inner and outer givens? - - Outer given is rewritten by an inner given, then there must - have been an inner given equality, hence the “given-eq” flag - will be true anyway. - - - Inner given rewritten by outer, retains its level (ie. The inner one) - - * We must take account of *potential* equalities, like the one above: - beta => ...blah... - If we still don't know what beta is, we conservatively treat it as potentially - becoming an equality. Hence including 'irreds' in the calculation or has_given_eqs. - Note that we can't really know what's in an irred, so any irred is considered - a potential equality. - - * What about something like forall a b. a ~ F b => [W] c ~ X y z? That Given - cannot affect the Wanted, because the Given is entirely *local*: it mentions - only skolems bound in the very same implication. Such equalities need not - prevent floating. (Test case typecheck/should_compile/LocalGivenEqs has a - real-life motivating example, with some detailed commentary.) These - equalities are noted with LocalGivenEqs: they do not prevent floating, but - they also are allowed to show up in error messages. See - Note [Suppress redundant givens during error reporting] in GHC.Tc.Errors. - The difference between what stops floating and what is suppressed from - error messages is why we need three options for HasGivenEqs. - - There is also a simpler case that triggers this behaviour: - - data T where - MkT :: F a ~ G b => a -> b -> T - - f (MkT _ _) = True - - Because of this behaviour around local equality givens, we can infer the - type of f. This is typecheck/should_compile/LocalGivenEqs2. - - * See Note [Let-bound skolems] for another wrinkle - - * We need not look at the equality relation involved (nominal vs representational), - because representational equalities can still imply nominal ones. For example, - if (G a ~R G b) and G's argument's role is nominal, then we can deduce a ~N b. - -Note [Let-bound skolems] -~~~~~~~~~~~~~~~~~~~~~~~~ -If * the inert set contains a canonical Given CEqCan (a ~ ty) -and * 'a' is a skolem bound in this very implication, - -then: -a) The Given is pretty much a let-binding, like - f :: (a ~ b->c) => a -> a - Here the equality constraint is like saying - let a = b->c in ... - It is not adding any new, local equality information, - and hence can be ignored by has_given_eqs - -b) 'a' will have been completely substituted out in the inert set, - so we can safely discard it. - -For an example, see #9211. - -See also GHC.Tc.Utils.Unify Note [Deeper level on the left] for how we ensure -that the right variable is on the left of the equality when both are -tyvars. - -You might wonder whether the skokem really needs to be bound "in the -very same implication" as the equuality constraint. -(c.f. #15009) Consider this: - - data S a where - MkS :: (a ~ Int) => S a - - g :: forall a. S a -> a -> blah - g x y = let h = \z. ( z :: Int - , case x of - MkS -> [y,z]) - in ... - -From the type signature for `g`, we get `y::a` . Then when we -encounter the `\z`, we'll assign `z :: alpha[1]`, say. Next, from the -body of the lambda we'll get - - [W] alpha[1] ~ Int -- From z::Int - [W] forall[2]. (a ~ Int) => [W] alpha[1] ~ a -- From [y,z] - -Now, suppose we decide to float `alpha ~ a` out of the implication -and then unify `alpha := a`. Now we are stuck! But if treat -`alpha ~ Int` first, and unify `alpha := Int`, all is fine. -But we absolutely cannot float that equality or we will get stuck. -} removeInertCts :: [Ct] -> InertCans -> InertCans @@ -2552,9 +2614,6 @@ tcAppMapToBag m = foldTcAppMap consBag m emptyBag foldTcAppMap :: (a -> b -> b) -> TcAppMap a -> b -> b foldTcAppMap k m z = foldDTyConEnv (foldTM k) z m -foldMapTcAppMap :: Monoid m => (a -> m) -> TcAppMap a -> m -foldMapTcAppMap f = foldMap (foldMap f) - {- ********************************************************************* * * @@ -2688,9 +2747,6 @@ findFunEqsByTyCon m tc foldFunEqs :: (a -> b -> b) -> FunEqMap a -> b -> b foldFunEqs = foldTcAppMap -foldMapFunEqs :: Monoid m => (a -> m) -> FunEqMap a -> m -foldMapFunEqs = foldMapTcAppMap - insertFunEq :: FunEqMap a -> TyCon -> [Type] -> a -> FunEqMap a insertFunEq m tc tys val = insertTcApp m tc tys val @@ -2723,6 +2779,12 @@ data TcSEnv -- The number of unification variables we have filled -- The important thing is whether it is non-zero + tcs_unif_lvl :: IORef (Maybe TcLevel), + -- The Unification Level Flag + -- Outermost level at which we have unified a meta tyvar + -- Starts at Nothing, then (Just i), then (Just j) where j<i + -- See Note [The Unification Level Flag] + tcs_count :: IORef Int, -- Global step count tcs_inerts :: IORef InertSet, -- Current inert set @@ -2877,8 +2939,10 @@ runTcSWithEvBinds' restore_cycles ev_binds_var tcs ; step_count <- TcM.newTcRef 0 ; inert_var <- TcM.newTcRef emptyInert ; 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 , tcs_worklist = wl_var } @@ -2941,15 +3005,19 @@ nestImplicTcS ref inner_tclvl (TcS thing_inside) = TcS $ \ TcSEnv { tcs_unified = unified_var , tcs_inerts = old_inert_var , tcs_count = count + , tcs_unif_lvl = unif_lvl } -> do { inerts <- TcM.readTcRef old_inert_var - ; let nest_inert = inerts { inert_cycle_breakers = [] } - -- all other InertSet fields are inherited + ; let nest_inert = inerts { inert_cycle_breakers = [] + , inert_cans = (inert_cans inerts) + { inert_given_eqs = False } } + -- All other InertSet fields are inherited ; new_inert_var <- TcM.newTcRef nest_inert ; new_wl_var <- TcM.newTcRef emptyWorkList - ; let nest_env = TcSEnv { tcs_ev_binds = ref + ; let nest_env = TcSEnv { tcs_count = count -- Inherited + , tcs_unif_lvl = unif_lvl -- Inherited + , tcs_ev_binds = ref , tcs_unified = unified_var - , tcs_count = count , tcs_inerts = new_inert_var , tcs_worklist = new_wl_var } ; res <- TcM.setTcLevel inner_tclvl $ @@ -3262,6 +3330,97 @@ pprKicked n = parens (int n <+> text "kicked out") {- ********************************************************************* * * +* The Unification Level Flag * +* * +********************************************************************* -} + +{- Note [The Unification Level Flag] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider a deep tree of implication constraints + forall[1] a. -- Outer-implic + C alpha[1] -- Simple + forall[2] c. ....(C alpha[1]).... -- Implic-1 + forall[2] b. ....(alpha[1] ~ Int).... -- Implic-2 + +The (C alpha) is insoluble until we know alpha. We solve alpha +by unifying alpha:=Int somewhere deep inside Implic-2. But then we +must try to solve the Outer-implic all over again. This time we can +solve (C alpha) both in Outer-implic, and nested inside Implic-1. + +When should we iterate solving a level-n implication? +Answer: if any unification of a tyvar at level n takes place + in the ic_implics of that implication. + +* What if a unification takes place at level n-1? Then don't iterate + level n, because we'll iterate level n-1, and that will in turn iterate + level n. + +* What if a unification takes place at level n, in the ic_simples of + level n? No need to track this, because the kick-out mechanism deals + with it. (We can't drop kick-out in favour of iteration, becuase kick-out + works for skolem-equalities, not just unifications.) + +So the monad-global Unification Level Flag, kept in tcs_unif_lvl keeps +track of + - Whether any unifications at all have taken place (Nothing => no unifications) + - If so, what is the outermost level that has seen a unification (Just lvl) + +The iteration done in the simplify_loop/maybe_simplify_again loop in GHC.Tc.Solver. + +It helpful not to iterate unless there is a chance of progress. #8474 is +an example: + + * There's a deeply-nested chain of implication constraints. + ?x:alpha => ?y1:beta1 => ... ?yn:betan => [W] ?x:Int + + * From the innermost one we get a [D] alpha[1] ~ Int, + so we can unify. + + * It's better not to iterate the inner implications, but go all the + way out to level 1 before iterating -- because iterating level 1 + will iterate the inner levels anyway. + +(In the olden days when we "floated" thse Derived constraints, this was +much, much more important -- we got exponential behaviour, as each iteration +produced the same Derived constraint.) +-} + + +resetUnificationFlag :: TcS Bool +-- We are at ambient level i +-- If the unification flag = Just i, reset it to Nothing and return True +-- Otherwise leave it unchanged and return False +resetUnificationFlag + = TcS $ \env -> + do { let ref = tcs_unif_lvl env + ; ambient_lvl <- TcM.getTcLevel + ; mb_lvl <- TcM.readTcRef ref + ; TcM.traceTc "resetUnificationFlag" $ + vcat [ text "ambient:" <+> ppr ambient_lvl + , text "unif_lvl:" <+> ppr mb_lvl ] + ; case mb_lvl of + Nothing -> return False + Just unif_lvl | ambient_lvl `strictlyDeeperThan` unif_lvl + -> return False + | otherwise + -> do { TcM.writeTcRef ref Nothing + ; return True } } + +setUnificationFlag :: TcLevel -> TcS () +-- (setUnificationFlag i) sets the unification level to (Just i) +-- unless it already is (Just j) where j <= i +setUnificationFlag lvl + = TcS $ \env -> + do { let ref = tcs_unif_lvl env + ; mb_lvl <- TcM.readTcRef ref + ; case mb_lvl of + Just unif_lvl | lvl `deeperThanOrSame` unif_lvl + -> return () + _ -> TcM.writeTcRef ref (Just lvl) } + + +{- ********************************************************************* +* * * Instantiation etc. * * ********************************************************************* -} |