diff options
| author | Simon Peyton Jones <simonpj@microsoft.com> | 2015-05-07 09:07:51 +0100 |
|---|---|---|
| committer | Simon Peyton Jones <simonpj@microsoft.com> | 2015-06-11 13:32:27 +0100 |
| commit | ddbb97d00fdbc5870a4076ed15af8e607b161cb2 (patch) | |
| tree | efc9b18c9786fa059e0ff8999a790e24f82ecb60 | |
| parent | ca39b96ee783e124909a89ea3ad366bf99defa7b (diff) | |
| download | haskell-ddbb97d00fdbc5870a4076ed15af8e607b161cb2.tar.gz | |
Another major improvement of "improvement"
I wasn't very happy with my fix to Trac #10009. This is much better.
The main idea is that the inert set now contains a "model", which
embodies *all* the (nominal) equalities that we know about, with
a view to exposing unifications. This requires a lot fewer iterations
of the solver than before.
There are extensive comments in
TcSMonad: Note [inert_model: the inert model]
Note [Adding an inert canonical constraint the InertCans]
The big changes are
* New inert_model field in InertCans
* Functions addInertEq, addInertCan deal with adding a
constraint, maintaining the model
* A nice improvement is that unification variables can
unify with fmvs, so that from, say alpha ~ fmv
we get alpha := fmv
See Note [Orientation of equalities with fmvs] in TcFlatten
It's still not perfect, as the Note explains
New flag -fconstraint-solver-iterations=n, allows us to control
the number of constraint solver iterations, and in particular
will flag up when it's more than a small number.
Performance is generally slightly better:
T5837 is a lot better for some reason.
30 files changed, 1811 insertions, 1361 deletions
diff --git a/compiler/basicTypes/BasicTypes.hs b/compiler/basicTypes/BasicTypes.hs index fe6c2a4834..d15295d4a2 100644 --- a/compiler/basicTypes/BasicTypes.hs +++ b/compiler/basicTypes/BasicTypes.hs @@ -88,7 +88,7 @@ module BasicTypes( SourceText, - IntWithInf, infinity, treatZeroAsInf, mkIntWithInf + IntWithInf, infinity, treatZeroAsInf, mkIntWithInf, intGtLimit ) where import FastString @@ -1165,6 +1165,10 @@ instance Num IntWithInf where (-) = panic "subtracting IntWithInfs" +intGtLimit :: Int -> IntWithInf -> Bool +intGtLimit _ Infinity = False +intGtLimit n (Int m) = n > m + -- | Add two 'IntWithInf's plusWithInf :: IntWithInf -> IntWithInf -> IntWithInf plusWithInf Infinity _ = Infinity diff --git a/compiler/main/Constants.hs b/compiler/main/Constants.hs index 229e007a8f..6e48539ec5 100644 --- a/compiler/main/Constants.hs +++ b/compiler/main/Constants.hs @@ -25,6 +25,11 @@ mAX_CTUPLE_SIZE = 16 -- Should match the number of decls in GHC.Classes mAX_REDUCTION_DEPTH :: Int mAX_REDUCTION_DEPTH = 200 +-- | Default maximum constraint-solver iterations +-- Typically there should be very few +mAX_SOLVER_ITERATIONS :: Int +mAX_SOLVER_ITERATIONS = 4 + wORD64_SIZE :: Int wORD64_SIZE = 8 diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs index 26f89c3a15..d5ba294d35 100644 --- a/compiler/main/DynFlags.hs +++ b/compiler/main/DynFlags.hs @@ -691,6 +691,8 @@ data DynFlags = DynFlags { mainModIs :: Module, mainFunIs :: Maybe String, reductionDepth :: IntWithInf, -- ^ Typechecker maximum stack depth + solverIterations :: IntWithInf, -- ^ Number of iterations in the constraints solver + -- Typically only 1 is needed thisPackage :: PackageKey, -- ^ name of package currently being compiled @@ -1440,6 +1442,7 @@ defaultDynFlags mySettings = mainModIs = mAIN, mainFunIs = Nothing, reductionDepth = treatZeroAsInf mAX_REDUCTION_DEPTH, + solverIterations = treatZeroAsInf mAX_SOLVER_ITERATIONS, thisPackage = mainPackageKey, @@ -2593,6 +2596,8 @@ dynamic_flags = [ (sepArg (\s d -> d{ ruleCheck = Just s })) , defFlag "freduction-depth" (intSuffix (\n d -> d{ reductionDepth = treatZeroAsInf n })) + , defFlag "fconstraint-solver-iterations" + (intSuffix (\n d -> d{ solverIterations = treatZeroAsInf n })) , defFlag "fcontext-stack" (intSuffixM (\n d -> do { deprecate $ "use -freduction-depth=" ++ show n ++ " instead" diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs index 5bbab219a5..f295e95eb9 100644 --- a/compiler/typecheck/TcCanonical.hs +++ b/compiler/typecheck/TcCanonical.hs @@ -316,9 +316,6 @@ situation can't happen. newSCWorkFromFlavored :: CtEvidence -> Class -> [Xi] -> TcS () -- Returns superclasses, see Note [Adding superclasses] newSCWorkFromFlavored flavor cls xis - | CtWanted {} <- flavor - = return () - | CtGiven { ctev_evar = evar, ctev_loc = loc } <- flavor = do { let size = sizePred (mkClassPred cls xis) loc' = case ctLocOrigin loc of @@ -342,7 +339,7 @@ newSCWorkFromFlavored flavor cls xis impr_theta = filter isImprovementPred sc_rec_theta loc = ctEvLoc flavor ; traceTcS "newSCWork/Derived" $ text "impr_theta =" <+> ppr impr_theta - ; mapM_ (emitNewDerived loc) impr_theta } + ; emitNewDeriveds loc impr_theta } {- @@ -623,7 +620,7 @@ can_eq_app :: CtEvidence -- :: s1 t1 ~N s2 t2 -> TcS (StopOrContinue Ct) can_eq_app ev s1 t1 s2 t2 | CtDerived { ctev_loc = loc } <- ev - = do { emitNewDerived loc (mkTcEqPred t1 t2) + = do { emitNewDerivedEq loc (mkTcEqPred t1 t2) ; canEqNC ev NomEq s1 s2 } | CtWanted { ctev_evar = evar, ctev_loc = loc } <- ev = do { ev_s <- newWantedEvVarNC loc (mkTcEqPred s1 s2) @@ -947,9 +944,13 @@ canEqTyVarTyVar ev eq_rel swapped tv1 tv2 = do { setEvBindIfWanted ev (EvCoercion $ mkTcReflCo role xi1) ; stopWith ev "Equal tyvars" } - | incompat_kind = incompat - | isFmvTyVar tv1 = do_fmv swapped tv1 xi1 xi2 co1 co2 - | isFmvTyVar tv2 = do_fmv (flipSwap swapped) tv2 xi2 xi1 co2 co1 + | incompat_kind = incompatibleKind ev xi1 k1 xi2 k2 + +-- We don't do this any more +-- See Note [Orientation of equalities with fmvs] in TcSMonad +-- | isFmvTyVar tv1 = do_fmv swapped tv1 xi1 xi2 co1 co2 +-- | isFmvTyVar tv2 = do_fmv (flipSwap swapped) tv2 xi2 xi1 co2 co1 + | same_kind = if swap_over then do_swap else no_swap | k1_sub_k2 = do_swap -- Note [Kind orientation for CTyEqCan] | otherwise = no_swap -- k2_sub_k1 @@ -976,12 +977,21 @@ canEqTyVarTyVar ev eq_rel swapped tv1 tv2 continueWith (CTyEqCan { cc_ev = new_ev, cc_tyvar = tv1 , cc_rhs = xi2, cc_eq_rel = eq_rel }) - -- See Note [Orient equalities with flatten-meta-vars on the left] in TcFlatten +{- We don't do this any more + See Note [Orientation of equalities with fmvs] in TcSMonad + -- tv1 is the flatten meta-var do_fmv swapped tv1 xi1 xi2 co1 co2 | same_kind = canon_eq swapped tv1 xi1 xi2 co1 co2 - | otherwise -- Presumably tv1 `subKind` tv2, which is the wrong way round - = ASSERT2( tyVarKind tv1 `isSubKind` typeKind xi2, + | otherwise -- Presumably tv1 :: *, since it is a flatten meta-var, + -- at a kind that has some interesting sub-kind structure. + -- Since the two kinds are not the same, we must have + -- tv1 `subKind` tv2, which is the wrong way round + -- e.g. (fmv::*) ~ (a::OpenKind) + -- So make a new meta-var and use that: + -- fmv ~ (beta::*) + -- (a::OpenKind) ~ (beta::*) + = ASSERT2( k1_sub_k2, ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1) $$ ppr xi2 <+> dcolon <+> ppr (typeKind xi2) ) ASSERT2( isWanted ev, ppr ev ) -- Only wanteds have flatten meta-vars @@ -991,8 +1001,7 @@ canEqTyVarTyVar ev eq_rel swapped tv1 tv2 tv_ty xi2) ; emitWorkNC [new_ev] ; canon_eq swapped tv1 xi1 tv_ty co1 (ctEvCoercion new_ev) } - - incompat = incompatibleKind ev xi1 k1 xi2 k2 +-} swap_over -- If tv1 is touchable, swap only if tv2 is also @@ -1050,7 +1059,7 @@ incompatibleKind new_ev s1 k1 s2 k2 -- See Note [Equalities with incompatible do { traceTcS "canEqLeaf: incompatible kinds" (vcat [ppr k1, ppr k2]) -- Create a derived kind-equality, and solve it - ; emitNewDerived kind_co_loc (mkTcEqPred k1 k2) + ; emitNewDerivedEq kind_co_loc (mkTcEqPred k1 k2) -- Put the not-currently-soluble thing into the inert set ; continueWith (CIrredEvCan { cc_ev = new_ev }) } @@ -1279,7 +1288,7 @@ as well as in old_pred; that is important for good error messages. -} -rewriteEvidence old_ev@(CtDerived { ctev_loc = loc }) new_pred _co +rewriteEvidence old_ev@(CtDerived {}) new_pred _co = -- If derived, don't even look at the coercion. -- This is very important, DO NOT re-order the equations for -- rewriteEvidence to put the isTcReflCo test first! @@ -1287,18 +1296,15 @@ rewriteEvidence old_ev@(CtDerived { ctev_loc = loc }) new_pred _co -- was produced by flattening, may contain suspended calls to -- (ctEvTerm c), which fails for Derived constraints. -- (Getting this wrong caused Trac #7384.) - do { mb_ev <- newDerived loc new_pred - ; case mb_ev of - Just new_ev -> continueWith new_ev - Nothing -> stopWith old_ev "Cached derived" } + continueWith (old_ev { ctev_pred = new_pred }) rewriteEvidence old_ev new_pred co | isTcReflCo co -- See Note [Rewriting with Refl] - = return (ContinueWith (old_ev { ctev_pred = new_pred })) + = continueWith (old_ev { ctev_pred = new_pred }) rewriteEvidence ev@(CtGiven { ctev_evar = old_evar , ctev_loc = loc }) new_pred co = do { new_ev <- newGivenEvVar loc (new_pred, new_tm) - ; return (ContinueWith new_ev) } + ; continueWith new_ev } where -- mkEvCast optimises ReflCo new_tm = mkEvCast (EvId old_evar) (tcDowngradeRole Representational @@ -1340,23 +1346,20 @@ rewriteEqEvidence :: CtEvidence -- Old evidence :: olhs ~ orhs (not swap -- -- It's all a form of rewwriteEvidence, specialised for equalities rewriteEqEvidence old_ev eq_rel swapped nlhs nrhs lhs_co rhs_co + | CtDerived {} <- old_ev -- Don't force the evidence for a Derived + = continueWith (old_ev { ctev_pred = new_pred }) + | NotSwapped <- swapped , isTcReflCo lhs_co -- See Note [Rewriting with Refl] , isTcReflCo rhs_co - = return (ContinueWith (old_ev { ctev_pred = new_pred })) - - | CtDerived {} <- old_ev - = do { mb <- newDerived loc' new_pred - ; case mb of - Just new_ev -> continueWith new_ev - Nothing -> stopWith old_ev "Cached derived" } + = continueWith (old_ev { ctev_pred = new_pred }) | CtGiven { ctev_evar = old_evar } <- old_ev = do { let new_tm = EvCoercion (lhs_co `mkTcTransCo` maybeSym swapped (mkTcCoVarCo old_evar) `mkTcTransCo` mkTcSymCo rhs_co) ; new_ev <- newGivenEvVar loc' (new_pred, new_tm) - ; return (ContinueWith new_ev) } + ; continueWith new_ev } | CtWanted { ctev_evar = evar } <- old_ev = do { new_evar <- newWantedEvVarNC loc' new_pred @@ -1366,7 +1369,7 @@ rewriteEqEvidence old_ev eq_rel swapped nlhs nrhs lhs_co rhs_co `mkTcTransCo` rhs_co ; setWantedEvBind evar (EvCoercion co) ; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co]) - ; return (ContinueWith new_evar) } + ; continueWith new_evar } | otherwise = panic "rewriteEvidence" @@ -1469,7 +1472,7 @@ unify_derived loc role orig_ty1 orig_ty2 Nothing -> bale_out } go _ _ = bale_out - bale_out = emitNewDerived loc (mkTcEqPredRole role orig_ty1 orig_ty2) + bale_out = emitNewDerivedEq loc (mkTcEqPredRole role orig_ty1 orig_ty2) maybeSym :: SwapFlag -> TcCoercion -> TcCoercion maybeSym IsSwapped co = mkTcSymCo co diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs index 09ed3402b8..5ecec903fd 100644 --- a/compiler/typecheck/TcFlatten.hs +++ b/compiler/typecheck/TcFlatten.hs @@ -5,9 +5,6 @@ module TcFlatten( flatten, flattenManyNom, unflatten, - - eqCanRewrite, eqCanRewriteFR, canRewriteOrSame, - CtFlavourRole, ctEvFlavourRole, ctFlavourRole ) where #include "HsVersions.h" @@ -201,40 +198,77 @@ Consider g (x:Int) (y:Bool) Here we get (F Int ~ Int, F Int ~ Bool), which flattens to (fmv ~ Int, fmv ~ Bool) -But there are really TWO separate errors. We must not complain -about Int~Bool. Moreover these two errors could arise in entirely -unrelated parts of the code. (In the alpha case, there must be -*some* connection (eg v:alpha in common envt).) +But there are really TWO separate errors. + + ** We must not complain about Int~Bool. ** + +Moreover these two errors could arise in entirely unrelated parts of +the code. (In the alpha case, there must be *some* connection (eg +v:alpha in common envt).) -Note [Orient equalities with flatten-meta-vars on the left] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -This example comes from IndTypesPerfMerge +Note [Orientation of equalities with fmvs] and +Note [Unflattening can force the solver to iterate] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Here is a bad dilemma concerning flatten meta-vars (fmvs). +This example comes from IndTypesPerfMerge, T10226, T10009. From the ambiguity check for f :: (F a ~ a) => a we get: [G] F a ~ a [W] F alpha ~ alpha, alpha ~ a - From Givens we get +From Givens we get [G] F a ~ fsk, fsk ~ a - Now if we flatten we get +Now if we flatten we get [W] alpha ~ fmv, F alpha ~ fmv, alpha ~ a - Now, processing the first one first, choosing alpha := fmv +Now, processing the first one first, choosing alpha := fmv [W] F fmv ~ fmv, fmv ~ a - And now we are stuck. We must either *unify* fmv := a, or - use the fmv ~ a to rewrite F fmv ~ fmv, so we can make it - meet up with the given F a ~ blah. +And now we are stuck. We must either *unify* fmv := a, or +use the fmv ~ a to rewrite F fmv ~ fmv, so we can make it +meet up with the given F a ~ blah. -Solution: always put fmvs on the left, so we get +Old solution: always put fmvs on the left, so we get [W] fmv ~ alpha, F alpha ~ fmv, alpha ~ a - The point is that fmvs are very uninformative, so doing alpha := fmv - is a bad idea. We want to use other constraints on alpha first. +BUT this works badly for Trac #10340: + get :: MonadState s m => m s + instance MonadState s (State s) where ... + + foo :: State Any Any + foo = get + +For 'foo' we instantiate 'get' at types mm ss + [W] MonadState ss mm, [W] mm ss ~ State Any Any +Flatten, and decompose + [W] MnadState ss mm, [W] Any ~ fmv, [W] mm ~ State fmv, [W] fmv ~ ss +Unify mm := State fmv: + [W] MonadState ss (State fmv), [W] Any ~ fmv, [W] fmv ~ ss +If we orient with (untouchable) fmv on the left we are now stuck: +alas, the instance does not match!! But if instead we orient with +(touchable) ss on the left, we unify ss:=fmv, to get + [W] MonadState fmv (State fmv), [W] Any ~ fmv +Now we can solve. +This is a real dilemma. CURRENT SOLUTION: + * Orient with touchable variables on the left. This is the + simple, uniform thing to do. So we would orient ss ~ fmv, + not the other way round. + + * In the 'f' example, we get stuck with + F fmv ~ fmv, fmv ~ a + But during unflattening we will fail to dischargeFmv for the + CFunEqCan F fmv ~ fmv, because fmv := F fmv would make an ininite + type. Instead we unify fmv:=a, AND record that we have done so. + + If any such "non-CFunEqCan unifications" take place, iterate the + entire process. This is done by the 'go' loop in solveSimpleWanteds. + +This story does not feel right but it's the best I can do; and the +iteration only happens in pretty obscure circumstances. ************************************************************************ @@ -1052,10 +1086,10 @@ flatten_exact_fam_app_fully tc tys -- Now, look in the cache ; mb_ct <- liftTcS $ lookupFlatCache tc xis - ; flavour_role <- getFlavourRole + ; flavour <- getFlavour ; case mb_ct of Just (co, rhs_ty, flav) -- co :: F xis ~ fsk - | (flav, NomEq) `canRewriteOrSameFR` flavour_role + | flav `canDischargeF` flavour -> -- Usable hit in the flat-cache -- We certainly *can* use a Wanted for a Wanted do { traceFlat "flatten/flat-cache hit" $ (ppr tc <+> ppr xis $$ ppr rhs_ty) @@ -1160,224 +1194,7 @@ have any knowledge as to *why* these facts are true. * * Flattening a type variable * * -************************************************************************ - - -Note [The inert equalities] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -Definition [Can-rewrite relation] -A "can-rewrite" relation between flavours, written f1 >= f2, is a -binary relation with the following properties - - R1. >= is transitive - R2. If f1 >= f, and f2 >= f, - then either f1 >= f2 or f2 >= f1 - -Lemma. If f1 >= f then f1 >= f1 -Proof. By property (R2), with f1=f2 - -Definition [Generalised substitution] -A "generalised substitution" S is a set of triples (a -f-> t), where - a is a type variable - t is a type - f is a flavour -such that - (WF1) if (a -f1-> t1) in S - (a -f2-> t2) in S - then neither (f1 >= f2) nor (f2 >= f1) hold - (WF2) if (a -f-> t) is in S, then t /= a - -Definition [Applying a generalised substitution] -If S is a generalised substitution - S(f,a) = t, if (a -fs-> t) in S, and fs >= f - = a, otherwise -Application extends naturally to types S(f,t), modulo roles. -See Note [Flavours with roles]. - -Theorem: S(f,a) is well defined as a function. -Proof: Suppose (a -f1-> t1) and (a -f2-> t2) are both in S, - and f1 >= f and f2 >= f - Then by (R2) f1 >= f2 or f2 >= f1, which contradicts (WF) - -Notation: repeated application. - S^0(f,t) = t - S^(n+1)(f,t) = S(f, S^n(t)) - -Definition: inert generalised substitution -A generalised substitution S is "inert" iff - - (IG1) there is an n such that - for every f,t, S^n(f,t) = S^(n+1)(f,t) - - (IG2) if (b -f-> t) in S, and f >= f, then S(f,t) = t - that is, each individual binding is "self-stable" - ----------------------------------------------------------------- -Our main invariant: - the inert CTyEqCans should be an inert generalised substitution ----------------------------------------------------------------- - -Note that inertness is not the same as idempotence. To apply S to a -type, you may have to apply it recursive. But inertness does -guarantee that this recursive use will terminate. - ----------- The main theorem -------------- - Suppose we have a "work item" - a -fw-> t - and an inert generalised substitution S, - such that - (T1) S(fw,a) = a -- LHS of work-item is a fixpoint of S(fw,_) - (T2) S(fw,t) = t -- RHS of work-item is a fixpoint of S(fw,_) - (T3) a not in t -- No occurs check in the work item - - (K1) if (a -fs-> s) is in S then not (fw >= fs) - (K2) if (b -fs-> s) is in S, where b /= a, then - (K2a) not (fs >= fs) - or (K2b) not (fw >= fs) - or (K2c) a not in s - (K3) If (b -fs-> s) is in S with (fw >= fs), then - (K3a) If the role of fs is nominal: s /= a - (K3b) If the role of fs is representational: EITHER - a not in s, OR - the path from the top of s to a includes at least one non-newtype - - then the extended substition T = S+(a -fw-> t) - is an inert generalised substitution. - -The idea is that -* (T1-2) are guaranteed by exhaustively rewriting the work-item - with S(fw,_). - -* T3 is guaranteed by a simple occurs-check on the work item. - -* (K1-3) are the "kick-out" criteria. (As stated, they are really the - "keep" criteria.) If the current inert S contains a triple that does - not satisfy (K1-3), then we remove it from S by "kicking it out", - and re-processing it. - -* Note that kicking out is a Bad Thing, because it means we have to - re-process a constraint. The less we kick out, the better. - TODO: Make sure that kicking out really *is* a Bad Thing. We've assumed - this but haven't done the empirical study to check. - -* Assume we have G>=G, G>=W, D>=D, and that's all. Then, when performing - a unification we add a new given a -G-> ty. But doing so does NOT require - us to kick out an inert wanted that mentions a, because of (K2a). This - is a common case, hence good not to kick out. - -* Lemma (L1): The conditions of the Main Theorem imply that there is no - (a fs-> t) in S, s.t. (fs >= fw). - Proof. Suppose the contrary (fs >= fw). Then because of (T1), - S(fw,a)=a. But since fs>=fw, S(fw,a) = s, hence s=a. But now we - have (a -fs-> a) in S, which contradicts (WF2). - -* The extended substitution satisfies (WF1) and (WF2) - - (K1) plus (L1) guarantee that the extended substiution satisfies (WF1). - - (T3) guarantees (WF2). - -* (K2) is about inertness. Intuitively, any infinite chain T^0(f,t), - T^1(f,t), T^2(f,T).... must pass through the new work item infnitely - often, since the substution without the work item is inert; and must - pass through at least one of the triples in S infnitely often. - - - (K2a): if not(fs>=fs) then there is no f that fs can rewrite (fs>=f), - and hence this triple never plays a role in application S(f,a). - It is always safe to extend S with such a triple. - - (NB: we could strengten K1) in this way too, but see K3. - - - (K2b): If this holds, we can't pass through this triple infinitely - often, because if we did then fs>=f, fw>=f, hence fs>=fw, - contradicting (L1), or fw>=fs contradicting K2b. - - - (K2c): if a not in s, we hae no further opportunity to apply the - work item. - - NB: this reasoning isn't water tight. - -Key lemma to make it watertight. - Under the conditions of the Main Theorem, - forall f st fw >= f, a is not in S^k(f,t), for any k - -Also, consider roles more carefully. See Note [Flavours with roles]. - -Completeness -~~~~~~~~~~~~~ -K3: completeness. (K3) is not necessary for the extended substitution -to be inert. In fact K1 could be made stronger by saying - ... then (not (fw >= fs) or not (fs >= fs)) -But it's not enough for S to be inert; we also want completeness. -That is, we want to be able to solve all soluble wanted equalities. -Suppose we have - - work-item b -G-> a - inert-item a -W-> b - -Assuming (G >= W) but not (W >= W), this fulfills all the conditions, -so we could extend the inerts, thus: - - inert-items b -G-> a - a -W-> b - -But if we kicked-out the inert item, we'd get - - work-item a -W-> b - inert-item b -G-> a - -Then rewrite the work-item gives us (a -W-> a), which is soluble via Refl. -So we add one more clause to the kick-out criteria - -Another way to understand (K3) is that we treat an inert item - a -f-> b -in the same way as - b -f-> a -So if we kick out one, we should kick out the other. The orientation -is somewhat accidental. - -When considering roles, we also need the second clause (K3b). Consider - - inert-item a -W/R-> b c - work-item c -G/N-> a - -The work-item doesn't get rewritten by the inert, because (>=) doesn't hold. -We've satisfied conditions (T1)-(T3) and (K1) and (K2). If all we had were -condition (K3a), then we would keep the inert around and add the work item. -But then, consider if we hit the following: - - work-item2 b -G/N-> Id - -where - - newtype Id x = Id x - -For similar reasons, if we only had (K3a), we wouldn't kick the -representational inert out. And then, we'd miss solving the inert, which -now reduced to reflexivity. The solution here is to kick out representational -inerts whenever the tyvar of a work item is "exposed", where exposed means -not under some proper data-type constructor, like [] or Maybe. See -isTyVarExposed in TcType. This is encoded in (K3b). - -Note [Flavours with roles] -~~~~~~~~~~~~~~~~~~~~~~~~~~ -The system described in Note [The inert equalities] discusses an abstract -set of flavours. In GHC, flavours have two components: the flavour proper, -taken from {Wanted, Derived, Given}; and the equality relation (often called -role), taken from {NomEq, ReprEq}. When substituting w.r.t. the inert set, -as described in Note [The inert equalities], we must be careful to respect -roles. For example, if we have - - inert set: a -G/R-> Int - b -G/R-> Bool - - type role T nominal representational - -and we wish to compute S(W/R, T a b), the correct answer is T a Bool, NOT -T Int Bool. The reason is that T's first parameter has a nominal role, and -thus rewriting a to Int in T a b is wrong. Indeed, this non-congruence of -subsitution means that the proof in Note [The inert equalities] may need -to be revisited, but we don't think that the end conclusion is wrong. --} +********************************************************************* -} flatten_tyvar :: TcTyVar -> FlatM (Either TyVar (TcType, TcCoercion)) @@ -1390,22 +1207,36 @@ flatten_tyvar :: TcTyVar flatten_tyvar tv | not (isTcTyVar tv) -- Happens when flatten under a (forall a. ty) - = Left `liftM` flattenTyVarFinal tv - -- So ty contains refernces to the non-TcTyVar a + = flatten_tyvar3 tv + -- So ty contains references to the non-TcTyVar a | otherwise = do { mb_ty <- liftTcS $ isFilledMetaTyVar_maybe tv ; role <- getRole - ; case mb_ty of { + ; case mb_ty of Just ty -> do { traceFlat "Following filled tyvar" (ppr tv <+> equals <+> ppr ty) ; return (Right (ty, mkTcReflCo role ty)) } ; - Nothing -> - - -- Try in the inert equalities - -- See Definition [Applying a generalised substitution] - do { ieqs <- liftTcS $ getInertEqs - ; flavour_role <- getFlavourRole - ; eq_rel <- getEqRel + Nothing -> do { flavour_role <- getFlavourRole + ; flatten_tyvar2 tv flavour_role } } + +flatten_tyvar2 :: TcTyVar -> CtFlavourRole + -> FlatM (Either TyVar (TcType, TcCoercion)) +-- Try in the inert equalities +-- See Definition [Applying a generalised substitution] in TcSMonad +-- See Note [Stability of flattening] in TcSMonad + +flatten_tyvar2 tv flavour_role@(flavour, eq_rel) + | Derived <- flavour -- For derived equalities, consult the inert_model (only) + = ASSERT( eq_rel == NomEq ) -- All derived equalities are nominal + do { model <- liftTcS $ getInertModel + ; case lookupVarEnv model tv of + Just (CTyEqCan { cc_rhs = rhs }) + -> return (Right (rhs, pprPanic "flatten_tyvar2" (ppr tv $$ ppr rhs))) + -- Evidence is irrelevant for Derived contexts + _ -> flatten_tyvar3 tv } + + | otherwise -- For non-derived equalities, consult the inert_eqs (only) + = do { ieqs <- liftTcS $ getInertEqs ; case lookupVarEnv ieqs tv of Just (ct:_) -- If the first doesn't work, -- the subsequent ones won't either @@ -1426,15 +1257,15 @@ flatten_tyvar tv -- we are not going to touch the returned coercion -- so ctEvCoercion is fine. - _other -> Left `liftM` flattenTyVarFinal tv - } } } + _other -> flatten_tyvar3 tv } -flattenTyVarFinal :: TcTyVar -> FlatM TyVar -flattenTyVarFinal tv +flatten_tyvar3 :: TcTyVar -> FlatM (Either TyVar a) +-- Always returns Left! +flatten_tyvar3 tv = -- Done, but make sure the kind is zonked - do { let kind = tyVarKind tv + do { let kind = tyVarKind tv ; (new_knd, _kind_co) <- setMode FM_SubstOnly $ flatten_one kind - ; return (setVarType tv new_knd) } + ; return (Left (setVarType tv new_knd)) } {- Note [An alternative story for the inert substitution] @@ -1504,89 +1335,7 @@ is an example; all the constraints here are Givens Because the incoming given rewrites all the inert givens, we get more and more duplication in the inert set. But this really only happens in pathalogical casee, so we don't care. --} -eqCanRewrite :: CtEvidence -> CtEvidence -> Bool -eqCanRewrite ev1 ev2 = ctEvFlavourRole ev1 `eqCanRewriteFR` ctEvFlavourRole ev2 - --- | Whether or not one 'Ct' can rewrite another is determined by its --- flavour and its equality relation -type CtFlavourRole = (CtFlavour, EqRel) - --- | Extract the flavour and role from a 'CtEvidence' -ctEvFlavourRole :: CtEvidence -> CtFlavourRole -ctEvFlavourRole ev = (ctEvFlavour ev, ctEvEqRel ev) - --- | Extract the flavour and role from a 'Ct' -ctFlavourRole :: Ct -> CtFlavourRole -ctFlavourRole = ctEvFlavourRole . cc_ev - -eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool --- Very important function! --- See Note [eqCanRewrite] --- See Note [Wanteds do not rewrite Wanteds] --- See Note [Deriveds do rewrite Deriveds] -eqCanRewriteFR (Given, NomEq) (_, _) = True -eqCanRewriteFR (Given, ReprEq) (_, ReprEq) = True -eqCanRewriteFR (Derived, NomEq) (Derived, NomEq) = True -eqCanRewriteFR _ _ = False - -canRewriteOrSame :: CtEvidence -> CtEvidence -> Bool --- See Note [canRewriteOrSame] -canRewriteOrSame ev1 ev2 = ev1 `eqCanRewrite` ev2 || - ctEvFlavourRole ev1 == ctEvFlavourRole ev2 - -canRewriteOrSameFR :: CtFlavourRole -> CtFlavourRole -> Bool -canRewriteOrSameFR fr1 fr2 = fr1 `eqCanRewriteFR` fr2 || fr1 == fr2 - -{- Note [eqCanRewrite] -~~~~~~~~~~~~~~~~~~~ -(eqCanRewrite ct1 ct2) holds if the constraint ct1 (a CTyEqCan of form -tv ~ ty) can be used to rewrite ct2. It must satisfy the properties of -a can-rewrite relation, see Definition [Can-rewrite relation] - -With the solver handling Coercible constraints like equality constraints, -the rewrite conditions must take role into account, never allowing -a representational equality to rewrite a nominal one. - -Note [Wanteds do not rewrite Wanteds] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We don't allow Wanteds to rewrite Wanteds, because that can give rise -to very confusing type error messages. A good example is Trac #8450. -Here's another - f :: a -> Bool - f x = ( [x,'c'], [x,True] ) `seq` True -Here we get - [W] a ~ Char - [W] a ~ Bool -but we do not want to complain about Bool ~ Char! - -Note [Deriveds do rewrite Deriveds] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -However we DO allow Deriveds to rewrite Deriveds, because that's how -improvement works; see Note [The improvement story] in TcInteract. - -However, for now at least I'm only letting (Derived,NomEq) rewrite -(Derived,NomEq) and not doing anything for ReprEq. If we have - eqCanRewriteFR (Derived, NomEq) (Derived, _) = True -then we lose the property of Note [Can-rewrite relation] - R2. If f1 >= f, and f2 >= f, - then either f1 >= f2 or f2 >= f1 -Consider f1 = (Given, ReprEq) - f2 = (Derived, NomEq) - f = (Derived, ReprEq) - -I thought maybe we could never get Derived ReprEq constraints, but -we can; straight from the Wanteds during improvment. And from a Derived -ReprEq we could conceivably get a Derived NomEq improvment (by decomposing -a type constructor with Nomninal role), and hence unify. - -Note [canRewriteOrSame] -~~~~~~~~~~~~~~~~~~~~~~~ -canRewriteOrSame is similar but - * returns True for Wanted/Wanted. - * works for all kinds of constraints, not just CTyEqCans -See the call sites for explanations. ************************************************************************ * * @@ -1642,10 +1391,20 @@ unflatten tv_eqs funeqs unflatten_funeq :: DynFlags -> Ct -> Cts -> TcS Cts unflatten_funeq dflags ct@(CFunEqCan { cc_fun = tc, cc_tyargs = xis , cc_fsk = fmv, cc_ev = ev }) rest - = do { -- fmv should be a flatten meta-tv; we now fix its final - -- value, and then zonking will eliminate it - filled <- tryFill dflags fmv (mkTyConApp tc xis) ev - ; return (if filled then rest else ct `consCts` rest) } + = do { -- fmv should be an un-filled flatten meta-tv; + -- we now fix its final value by filling it, being careful + -- to observe the occurs check. Zonking will eliminate it + -- altogether in due course + rhs' <- zonkTcType (mkTyConApp tc xis) + ; case occurCheckExpand dflags fmv rhs' of + OC_OK rhs'' -- Normal case: fill the tyvar + -> do { setEvBindIfWanted ev + (EvCoercion (mkTcReflCo (ctEvRole ev) rhs'')) + ; unflattenFmv fmv rhs'' + ; return rest } + + _ -> -- Occurs check + return (ct `consCts` rest) } unflatten_funeq _ other_ct _ = pprPanic "unflatten_funeq" (ppr other_ct) @@ -1660,7 +1419,11 @@ unflatten tv_eqs funeqs ---------------- unflatten_eq :: DynFlags -> TcLevel -> Ct -> Cts -> TcS Cts unflatten_eq dflags tclvl ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = rhs }) rest - | isFmvTyVar tv + | isFmvTyVar tv -- Previously these fmvs were untouchable, + -- but now they are touchable + -- NB: unlike unflattenFmv, filling a fmv here does + -- bump the unification count; it is "improvement" + -- Note [Unflattening can force the solver to iterate] = do { lhs_elim <- tryFill dflags tv rhs ev ; if lhs_elim then return rest else do { rhs_elim <- try_fill dflags tclvl ev rhs (mkTyVarTy tv) diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs index 5a550b4530..0000ff04f0 100644 --- a/compiler/typecheck/TcInteract.hs +++ b/compiler/typecheck/TcInteract.hs @@ -1,21 +1,20 @@ {-# LANGUAGE CPP #-} module TcInteract ( - solveSimpleGivens, -- Solves [EvVar],GivenLoc - solveSimpleWanteds, -- Solves Cts - usefulToFloat + solveSimpleGivens, -- Solves [EvVar],GivenLoc + solveSimpleWanteds -- Solves Cts ) where #include "HsVersions.h" -import BasicTypes ( infinity ) +import BasicTypes ( infinity, IntWithInf, intGtLimit ) import HsTypes ( hsIPNameFS ) import FastString import TcCanonical import TcFlatten import VarSet import Type -import Kind ( isKind, isConstraintKind, isSubKind ) +import Kind ( isKind, isConstraintKind ) import Unify import InstEnv( DFunInstType, lookupInstEnv, instanceDFunId ) import CoAxiom(sfInteractTop, sfInteractInert) @@ -35,9 +34,7 @@ import Inst( tyVarsOfCt ) import TcEvidence import Outputable -import qualified TcRnMonad as TcM import TcRnTypes -import TcErrors import TcSMonad import Bag @@ -150,285 +147,67 @@ solveSimpleWanteds :: Cts -> TcS WantedConstraints -- out from a nested implication. So don't discard deriveds! solveSimpleWanteds simples = do { traceTcS "solveSimples {" (ppr simples) - ; (n,wc) <- go 1 (emptyWC { wc_simple = simples }) + ; dflags <- getDynFlags + ; (n,wc) <- go 1 (solverIterations dflags) (emptyWC { wc_simple = simples }) ; traceTcS "solveSimples end }" $ vcat [ ptext (sLit "iterations =") <+> ppr n , ptext (sLit "residual =") <+> ppr wc ] ; return wc } where - go :: Int -> WantedConstraints -> TcS (Int, WantedConstraints) - go n wc - | n > 10 - = do { wrapWarnTcS $ TcM.addWarnTc $ - hang (ptext (sLit "solveSimpleWanteds: possible loop?")) - 2 (pprCts simples) - ; return (n,wc) } + go :: Int -> IntWithInf -> WantedConstraints -> TcS (Int, WantedConstraints) + go n limit wc + | n `intGtLimit` limit + = failTcS (hang (ptext (sLit "solveSimpleWanteds: too many iterations") + <+> parens (ptext (sLit "limit =") <+> ppr limit)) + 2 (vcat [ ptext (sLit "Set limit with -fsolver-iterations=n; n=0 for no limit") + , ptext (sLit "Simples =") <+> ppr simples + , ptext (sLit "WC =") <+> ppr wc ])) | isEmptyBag (wc_simple wc) = return (n,wc) | otherwise = do { -- Solve - (unifs1, wc1) <- solve_simple_wanteds wc - - -- Try improvement - -- See Note [The improvement story] - ; (unifs2, wc2) <- try_improvement wc1 + (unif_count, wc1) <- solve_simple_wanteds wc -- Run plugins - ; (rerun_plugin, wc3) <- runTcPluginsWanted wc2 + ; (rerun_plugin, wc2) <- runTcPluginsWanted wc1 -- See Note [Running plugins on unflattened wanteds] - ; if unifs1 || unifs2 || rerun_plugin - then go (n+1) wc3 -- Loop - else return (n,wc3) } + ; if unif_count == 0 && not rerun_plugin + then return (n, wc2) -- Done + else do { traceTcS "solveSimple going round again:" (ppr rerun_plugin) + ; go (n+1) limit wc2 } } -- Loop + -solve_simple_wanteds :: WantedConstraints -> TcS (Bool, WantedConstraints) +solve_simple_wanteds :: WantedConstraints -> TcS (Int, WantedConstraints) -- Try solving these constraints --- Return True iff some unification happened *during unflattening* --- because this is a form of improvement --- See Note [The improvement story] -- Affects the unification state (of course) but not the inert set solve_simple_wanteds (WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 }) = nestTcS $ do { solveSimples simples1 ; (implics2, tv_eqs, fun_eqs, insols2, others) <- getUnsolvedInerts - ; (unifs_happened, unflattened_eqs) <- reportUnifications $ - unflatten tv_eqs fun_eqs + ; (unif_count, unflattened_eqs) <- reportUnifications $ + unflatten tv_eqs fun_eqs -- See Note [Unflatten after solving the simple wanteds] - ; return ( unifs_happened + ; return ( unif_count , WC { wc_simple = others `andCts` unflattened_eqs , wc_insol = insols1 `andCts` insols2 , wc_impl = implics1 `unionBags` implics2 }) } -try_improvement :: WantedConstraints -> TcS (Bool, WantedConstraints) --- See Note [The improvement story] --- Try doing improvement on these simple constraints --- Return True iff some unification happened --- Affects the unification state (of course) but not the inert set -try_improvement wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics }) - | isEmptyBag simples - = return (False, wc) - | otherwise - = nestTcS $ reportUnifications $ - do { traceTcS "try_improvement {" (ppr wc) - ; solveSimples init_derived - ; (_, tv_eqs, fun_eqs, derived_insols, _) <- getUnsolvedInerts - ; derived_eqs <- unflatten tv_eqs fun_eqs - ; let new_derived = filterBag (usefulToFloat is_new) derived_eqs - wc1 = WC { wc_simple = simples1 `andCts` new_derived - , wc_insol = dropDerivedSimples insols `andCts` derived_insols - -- See Note [Insolubles and improvement] - , wc_impl = implics } - ; traceTcS "try_improvement end }" (ppr wc1) - ; return wc1 } - where - is_new pred = not (any (pred `eqType`) init_eq_preds) - -- Sigh: an equality in init_derived may well show up in derived_eqs, - -- if no progress has been made, and we don't want to duplicate it. - -- But happily these lists are both usually very short. - - -- Drop all derived constraints; we are about to re-generate them! - simples1 = dropDerivedSimples simples - init_derived = mapBag mk_derived simples1 - init_eq_preds = [ pred | ct <- bagToList init_derived - , let pred = ctPred ct - , isEqPred pred ] - - mk_derived :: Ct -> Ct -- Always non-canonical (so that we generate superclasses) - mk_derived ct = mkNonCanonical (CtDerived { ctev_pred = pred, ctev_loc = loc }) - where - pred = ctEvPred ev - loc = ctEvLoc ev - ev = ctEvidence ct - - -usefulToFloat :: (TcPredType -> Bool) -> Ct -> Bool -usefulToFloat is_useful_pred ct -- The constraint is un-flattened and de-canonicalised - = is_meta_var_eq pred && is_useful_pred pred - where - pred = ctPred ct - - -- Float out alpha ~ ty, or ty ~ alpha - -- which might be unified outside - -- See Note [Do not float kind-incompatible equalities] - is_meta_var_eq pred - | EqPred NomEq ty1 ty2 <- classifyPredType pred - , let k1 = typeKind ty1 - k2 = typeKind ty2 - = case (tcGetTyVar_maybe ty1, tcGetTyVar_maybe ty2) of - (Just tv1, _) | isMetaTyVar tv1 - , k2 `isSubKind` k1 - -> True - (_, Just tv2) | isMetaTyVar tv2 - , k1 `isSubKind` k2 - -> True - _ -> False - | otherwise - = False - -{- Note [The improvement story] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The goal of "improvement" is to use functional dependencies, -type-function injectivity, etc, to derive some extra equalities that -could let us unify one or more meta-variables, and hence make progress. - +{- Note [The solveSimpleWanteds loop] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Solving a bunch of simple constraints is done in a loop, (the 'go' loop of 'solveSimpleWanteds'): - 1. Try to solve them; some improvement happens here - 2. Try improvement on any unsolved residual constraints - 3. If step 2 led to any unifications, go back to step 1 - -We actually perform step 2 improvement as follows: - * Make the residual Wanteds into Deriveds - * Solve them, aggressively rewriting Derived with Derived - -Some notes about this - * As well as allowing unification, the aggressive rewriting may also - expose an equality on an /untouchable/ unification variable. We - want to keep this derived equality so that it can float out and - unify there. Hence 'usefulToFloat'. - - * Non-obviously, improvement can also take place during the unflattening - that takes place in step (1). See Example 1 below. - - * During Step 1 we do improvement only for Givens, not for Wanteds; - See Note [When improvement happens during solving] - ------------ Example 1 (Trac #10340) - get :: MonadState s m => m s - instance MonadState s (State s) where ... - - foo :: State Any Any - foo = get - - For 'foo' we instantiate 'get' at types mm ss - [W] MonadState ss mm, [W] mm ss ~ State Any Any - Flatten, and decompose - [W] MnadState ss mm, [W] Any ~ fmv, [W] mm ~ State fmv, [W] fmv ~ ss - NB: orientation of fmv ~ ss; see TcFlatten - Note [Orient equalities with flatten-meta-vars on the left] - Unify mm := State fmv: - [W] MonadState ss (State fmv), [W] Any ~ fmv, [W] fmv ~ ss - Alas the instance does not match!! So now we are stuck. - - Unflatten: with fmv := Any, and ss := Any - [W] MonadState Any (State Any) - - Note that the unification of 'ss' represents progress!! We must loop! - ------------ Example 2 (indexed-types/should_fail/T4093a) - Ambiguity check for f: (Foo e ~ Maybe e) => Foo e - - We get [G] Foo e ~ Maybe e - [W] Foo e ~ Foo ee -- ee is a unification variable - [W] Foo ee ~ Maybe ee - - Flatten: [G] Foo e ~ fsk - [G] fsk ~ Maybe e -- (A) - - [W] Foo ee ~ fmv - [W] fmv ~ fsk -- (B) From Foo e ~ Foo ee - [W] fmv ~ Maybe ee - - --> rewrite (B) with (A) - [W] Foo ee ~ fmv - [W] fmv ~ Maybe e - [W] fmv ~ Maybe ee - - But now we are stuck, since we don't rewrite Wanteds with Wanteds - Unflatten: - [W] Foo ee ~ Maybe e - [W] Foo ee ~ Maybe ee - - Improvement; start by flattening again - [D] Foo ee ~ fmv - [D] fmv ~ Maybe e -- (A) - [D] fmv ~ Maybe ee -- (B) - - Now we /can/ rewrite (A) with (B), by aggressive rewriting of Deriveds - and that soon yields ee := e, and all is well - ------------ Example 3 (typecheck/should_compile/Improvement.hs) - type instance F Int = Bool - instance (b~Int) => C Bool b - - [W] w1 : C (F alpha) alpha, [W] w2 : F alpha ~ Bool - - If we rewrote wanteds with wanteds, we could rewrite w1 to - C Bool alpha, use the instance to get alpha ~ Int, and solve - the whole thing. - - In improvement (step 2), we make both constraints Derived, - rewrite one with the other, and do type-class reduction on - the Derived constraint - ------------ Example 4 (Trac #10009, a nasty example): - - f :: (UnF (F b) ~ b) => F b -> () - - g :: forall a. (UnF (F a) ~ a) => a -> () - g _ = f (undefined :: F a) - - For g we get [G] UnF (F a) ~ a - [W] UnF (F beta) ~ beta - [W] F a ~ F beta - Flatten: - [G] g1: F a ~ fsk1 fsk1 := F a - [G] g2: UnF fsk1 ~ fsk2 fsk2 := UnF fsk1 - [G] g3: fsk2 ~ a - - [W] w1: F beta ~ fmv1 - [W] w2: UnF fmv1 ~ fmv2 - [W] w3: fmv2 ~ beta - [W] w5: fsk1 ~ fmv1 -- From F a ~ F beta - -- using flat-cache - - Solving (step 1) makes no progress. So unflatten again - [W] w3: UnF (F beta) ~ beta - [W] w5: fsk1 ~ F beta - - Try improvement: - [D] F beta ~ fmv1 - [D] UnF fmv1 ~ fmv2 -- (A) - [D] fmv2 ~ beta - [D] fmv1 ~ fsk1 -- (B) From F a ~ F beta - -- NB: put fmv on left - - --> rewrite (A) with (B), and match with g2 - [D] F beta ~ fmv1 - [D] fmv2 ~ fsk2 -- (C) - [D] fmv2 ~ beta -- (D) - [D] fmv1 ~ fsk1 - - --> rewrite (D) with (C) and re-orient - [D] F beta ~ fmv1 - [D] fmv2 ~ fsk2 - [D] beta ~ fsk2 -- (E) - [D] fmv1 ~ fsk1 - - -- Now we can unify beta! Hallelujah! - - -Note [Insolubles and improvement] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We drop all the derived wanted insolubles before improvement, because -they will all be regenerated by the improvement step. - -We want to keep all the derived insolubles, because they are looked -at by simplifyInfer, to decide whether to generalise. Example: - [W] a ~ Int, [W] a ~ Bool -During improvement we get [D] Int ~ Bool, and indeed the constraints -are insoluble, and we want simplifyInfer to see that, even though we -don't ultimately want to generate an (inexplicable) error message from -it. - -Note [Do not float kind-incompatible equalities] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -If we have (t::* ~ s::*->*), we'll get a Derived insoluble equality. -If we float the equality outwards, we'll get *another* Derived -insoluble equality one level out, so the same error will be reported -twice. So we refrain from floating such equalities. + 1. Try to solve them; unflattening may lead to improvement that + was not exploitable during solving + 2. Try the plugin + 3. If step 1 did improvement during unflattening; or if the plugin + wants to run again, go back to step 1 + +Non-obviously, improvement can also take place during +the unflattening that takes place in step (1). See TcFlatten, +See Note [Unflattening can force the solver to iterate] -} -- The main solver loop implements Note [Basic Simplifier Plan] @@ -447,14 +226,9 @@ solveSimples cts = {-# SCC "solve_loop" #-} do { sel <- selectNextWorkItem ; case sel of - NoWorkRemaining -- Done, successfuly (modulo frozen) - -> return () - MaxDepthExceeded ct -- Failure, depth exceeded - -> wrapErrTcS $ solverDepthErrorTcS (ctLoc ct) (ctPred ct) - NextWorkItem ct -- More work, loop around! - -> do { runSolverPipeline thePipeline ct - ; solve_loop } } - + Nothing -> return () + Just ct -> do { runSolverPipeline thePipeline ct + ; solve_loop } } -- | Extract the (inert) givens and invoke the plugins on them. -- Remove solved givens from the inert set and emit insolubles, but @@ -593,30 +367,6 @@ runTcPlugins plugins all_cts type WorkItem = Ct type SimplifierStage = WorkItem -> TcS (StopOrContinue Ct) -data SelectWorkItem - = NoWorkRemaining -- No more work left (effectively we're done!) - | MaxDepthExceeded Ct - -- More work left to do but this constraint has exceeded - -- the maximum depth and we must stop - | NextWorkItem Ct -- More work left, here's the next item to look at - -selectNextWorkItem :: TcS SelectWorkItem -selectNextWorkItem - = do { dflags <- getDynFlags - ; updWorkListTcS_return (pick_next dflags) } - where - pick_next :: DynFlags -> WorkList -> (SelectWorkItem, WorkList) - pick_next dflags wl - = case selectWorkItem wl of - (Nothing,_) - -> (NoWorkRemaining,wl) -- No more work - (Just ct, new_wl) - | subGoalDepthExceeded dflags (ctLocDepth (ctLoc ct)) - -> (MaxDepthExceeded ct,new_wl) -- Depth exceeded - - | otherwise - -> (NextWorkItem ct, new_wl) -- New workitem and worklist - runSolverPipeline :: [(String,SimplifierStage)] -- The pipeline -> WorkItem -- The work item -> TcS () @@ -637,11 +387,11 @@ runSolverPipeline pipeline workItem (ptext (sLit "inerts =") <+> ppr final_is) ; return () } ContinueWith ct -> do { traceFireTcS (ctEvidence ct) (ptext (sLit "Kept as inert")) - ; traceTcS "End solver pipeline (not discharged) }" $ + ; traceTcS "End solver pipeline (kept as inert) }" $ vcat [ ptext (sLit "final_item =") <+> ppr ct , pprTvBndrs (varSetElems $ tyVarsOfCt ct) , ptext (sLit "inerts =") <+> ppr final_is] - ; insertInertItemTcS ct } + ; addInertCan ct } } where run_pipeline :: [(String,SimplifierStage)] -> StopOrContinue Ct -> TcS (StopOrContinue Ct) @@ -754,13 +504,12 @@ solveOneFromTheOther :: CtEvidence -- Inert -- 1) inert and work item represent evidence for the /same/ predicate -- 2) ip/class/irred evidence (no coercions) only solveOneFromTheOther ev_i ev_w - | isDerived ev_w + | isDerived ev_w -- Work item is Derived; just discard it = return (IRKeep, True) - | isDerived ev_i -- The inert item is Derived, we can just throw it away, - -- The ev_w is inert wrt earlier inert-set items, - -- so it's safe to continue on from this point - = return (IRDelete, False) + | isDerived ev_i -- The inert item is Derived, we can just throw it away, + = return (IRDelete, False) -- The ev_w is inert wrt earlier inert-set items, + -- so it's safe to continue on from this point | CtWanted { ctev_loc = loc_w } <- ev_w , prohibitedSuperClassSolve (ctEvLoc ev_i) loc_w @@ -936,9 +685,8 @@ interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs -- don't ever try to solve CallStack IPs directly from other dicts, -- we always build new dicts instead. -- See Note [Overview of implicit CallStacks] - | [_ip, ty] <- tys + | Just mkEvCs <- isCallStackIP (ctEvLoc ev_w) cls tys , isWanted ev_w - , Just mkEvCs <- isCallStackIP (ctEvLoc ev_w) cls ty = do let ev_cs = case lookupInertDict inerts cls tys of Just ev | isGiven ev -> mkEvCs (ctEvTerm ev) @@ -969,20 +717,42 @@ interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = interactGivenIP inerts workItem | otherwise - = do { -- Try improvement via functional dependencies; - -- but only for Givens and Deriveds - -- See Note [When improvement happens during solving] - unless (isWanted ev_w) $ - mapBagM_ (addFunDepWork workItem) - (findDictsByClass (inert_dicts inerts) cls) + = do { addFunDepWork inerts ev_w cls + ; continueWith workItem } + +interactDict _ wi = pprPanic "interactDict" (ppr wi) + +addFunDepWork :: InertCans -> CtEvidence -> Class -> TcS () +-- Add derived constraints from type-class functional dependencies. +addFunDepWork inerts work_ev cls + = mapBagM_ add_fds (findDictsByClass (inert_dicts inerts) cls) -- No need to check flavour; fundeps work between -- any pair of constraints, regardless of flavour -- Importantly we don't throw workitem back in the -- worklist because this can cause loops (see #5236) + where + work_pred = ctEvPred work_ev + work_loc = ctEvLoc work_ev + add_fds inert_ct + = emitFunDepDeriveds $ + improveFromAnother derived_loc 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 + where + inert_pred = ctPred inert_ct + inert_loc = ctLoc inert_ct + derived_loc = work_loc { ctl_origin = FunDepOrigin1 work_pred work_loc + inert_pred inert_loc } - ; continueWith workItem } - -interactDict _ wi = pprPanic "interactDict" (ppr wi) +{- +********************************************************************************* +* * + Implicit parameters +* * +********************************************************************************* +-} interactGivenIP :: InertCans -> Ct -> TcS (StopOrContinue Ct) -- Work item is Given (?x:ty) @@ -1004,24 +774,6 @@ interactGivenIP inerts workItem@(CDictCan { cc_ev = ev, cc_class = cls interactGivenIP _ wi = pprPanic "interactGivenIP" (ppr wi) -addFunDepWork :: Ct -> Ct -> TcS () --- Add derived constraints from type-class functional dependencies. -addFunDepWork work_ct inert_ct - = emitFunDepDeriveds $ - improveFromAnother derived_loc 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 - -- Also see Note [When improvement happens during solving] - where - work_pred = ctPred work_ct - inert_pred = ctPred inert_ct - work_loc = ctLoc work_ct - inert_loc = ctLoc inert_ct - derived_loc = work_loc { ctl_origin = FunDepOrigin1 work_pred work_loc - inert_pred inert_loc } - {- Note [Shadowing of Implicit Parameters] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1085,7 +837,7 @@ interactFunEq :: InertCans -> Ct -> TcS (StopOrContinue Ct) interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc , cc_tyargs = args, cc_fsk = fsk }) | Just (CFunEqCan { cc_ev = ev_i, cc_fsk = fsk_i }) <- matching_inerts - = if ev_i `canRewriteOrSame` ev + = if ev_i `canDischarge` ev then -- Rewrite work-item using inert do { traceTcS "reactFunEq (discharge work item):" $ vcat [ text "workItem =" <+> ppr workItem @@ -1093,7 +845,7 @@ interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc ; reactFunEq ev_i fsk_i ev fsk ; stopWith ev "Inert rewrites work item" } else -- Rewrite inert using work-item - ASSERT2( ev `canRewriteOrSame` ev_i, ppr ev $$ ppr ev_i ) + ASSERT2( ev `canDischarge` ev_i, ppr ev $$ ppr ev_i ) do { traceTcS "reactFunEq (rewrite inert item):" $ vcat [ text "workItem =" <+> ppr workItem , text "inertItem=" <+> ppr ev_i ] @@ -1103,9 +855,7 @@ interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc ; reactFunEq ev fsk ev_i fsk_i ; stopWith ev "Work item rewrites inert" } - | not (isWanted ev) -- Try improvement only for Given/Derived - -- See Note [When improvement happens during solving] - , Just ops <- isBuiltInSynFamTyCon_maybe tc + | Just ops <- isBuiltInSynFamTyCon_maybe tc = do { let matching_funeqs = findFunEqsByTyCon funeqs tc ; let interact = sfInteractInert ops args (lookupFlattenTyVar eqs fsk) do_one (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk, cc_ev = iev }) @@ -1248,7 +998,7 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv , cc_eq_rel = eq_rel }) | (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i } <- findTyEqs inerts tv - , ev_i `canRewriteOrSame` ev + , ev_i `canDischarge` ev , rhs_i `tcEqType` rhs ] = -- Inert: a ~ b -- Work item: a ~ b @@ -1258,7 +1008,7 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv | Just tv_rhs <- getTyVar_maybe rhs , (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i } <- findTyEqs inerts tv_rhs - , ev_i `canRewriteOrSame` ev + , ev_i `canDischarge` ev , rhs_i `tcEqType` mkTyVarTy tv ] = -- Inert: a ~ b -- Work item: b ~ a @@ -1270,11 +1020,8 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv = do { tclvl <- getTcLevel ; if canSolveByUnification tclvl ev eq_rel tv rhs then do { solveByUnification ev tv rhs - ; n_kicked <- kickOutRewritable Given NomEq tv - -- Given because the tv := xi is given - -- NomEq because only nom. equalities are solved - -- by unification - ; return (Stop ev (ptext (sLit "Spontaneously solved") <+> ppr_kicked n_kicked)) } + ; n_kicked <- kickOutAfterUnification tv + ; return (Stop ev (ptext (sLit "Solved by unification") <+> ppr_kicked n_kicked)) } else do { traceTcS "Can't solve tyvar equality" (vcat [ text "LHS:" <+> ppr tv <+> dcolon <+> ppr (tyVarKind tv) @@ -1283,11 +1030,8 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv <+> text "is" <+> ppr (metaTyVarTcLevel tv)) , text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs) , text "TcLevel =" <+> ppr tclvl ]) - ; n_kicked <- kickOutRewritable (ctEvFlavour ev) - (ctEvEqRel ev) - tv - ; updInertCans (\ ics -> addInertCan ics workItem) - ; return (Stop ev (ptext (sLit "Kept as inert") <+> ppr_kicked n_kicked)) } } + ; addInertEq workItem + ; return (Stop ev (ptext (sLit "Kept as inert"))) } } interactTyVarEq _ wi = pprPanic "interactTyVarEq" (ppr wi) @@ -1354,161 +1098,12 @@ solveByUnification wd tv xi ; unifyTyVar tv xi' ; setEvBindIfWanted wd (EvCoercion (mkTcNomReflCo xi')) } - ppr_kicked :: Int -> SDoc ppr_kicked 0 = empty ppr_kicked n = parens (int n <+> ptext (sLit "kicked out")) -kickOutRewritable :: CtFlavour -- Flavour of the equality that is - -- being added to the inert set - -> EqRel -- of the new equality - -> TcTyVar -- The new equality is tv ~ ty - -> TcS Int -kickOutRewritable new_flavour new_eq_rel new_tv - | not ((new_flavour, new_eq_rel) `eqCanRewriteFR` (new_flavour, new_eq_rel)) - = return 0 -- If new_flavour can't rewrite itself, it can't rewrite - -- anything else, so no need to kick out anything - -- This is a common case: wanteds can't rewrite wanteds - - | otherwise - = do { ics <- getInertCans - ; let (kicked_out, ics') = kick_out new_flavour new_eq_rel new_tv ics - ; setInertCans ics' - ; updWorkListTcS (appendWorkList kicked_out) - - ; unless (isEmptyWorkList kicked_out) $ - csTraceTcS $ - hang (ptext (sLit "Kick out, tv =") <+> ppr new_tv) - 2 (vcat [ text "n-kicked =" <+> int (workListSize kicked_out) - , text "n-kept fun-eqs =" <+> int (sizeFunEqMap (inert_funeqs ics')) - , ppr kicked_out ]) - ; return (workListSize kicked_out) } - -kick_out :: CtFlavour -> EqRel -> TcTyVar -> InertCans -> (WorkList, InertCans) -kick_out new_flavour new_eq_rel new_tv (IC { inert_eqs = tv_eqs - , inert_dicts = dictmap - , inert_safehask = safehask - , inert_funeqs = funeqmap - , inert_irreds = irreds - , inert_insols = insols }) - = (kicked_out, inert_cans_in) - where - -- NB: Notice that don't rewrite - -- inert_solved_dicts, and inert_solved_funeqs - -- optimistically. But when we lookup we have to - -- take the substitution into account - 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_insols = insols_in } - - kicked_out = WL { wl_eqs = tv_eqs_out - , wl_funeqs = feqs_out - , wl_rest = bagToList (dicts_out `andCts` irs_out - `andCts` insols_out) - , wl_implics = emptyBag } - - (tv_eqs_out, tv_eqs_in) = foldVarEnv kick_out_eqs ([], emptyVarEnv) tv_eqs - (feqs_out, feqs_in) = partitionFunEqs kick_out_ct funeqmap - (dicts_out, dicts_in) = partitionDicts kick_out_ct dictmap - (irs_out, irs_in) = partitionBag kick_out_irred irreds - (insols_out, insols_in) = partitionBag kick_out_ct insols - -- Kick out even insolubles; see Note [Kick out insolubles] - - can_rewrite :: CtEvidence -> Bool - can_rewrite = ((new_flavour, new_eq_rel) `eqCanRewriteFR`) . ctEvFlavourRole - - kick_out_ct :: Ct -> Bool - kick_out_ct ct = kick_out_ctev (ctEvidence ct) - - kick_out_ctev :: CtEvidence -> Bool - kick_out_ctev ev = can_rewrite ev - && new_tv `elemVarSet` tyVarsOfType (ctEvPred ev) - -- See Note [Kicking out inert constraints] - - kick_out_irred :: Ct -> Bool - kick_out_irred ct = can_rewrite (cc_ev ct) - && new_tv `elemVarSet` closeOverKinds (tyVarsOfCt ct) - -- See Note [Kicking out Irreds] - - kick_out_eqs :: EqualCtList -> ([Ct], TyVarEnv EqualCtList) - -> ([Ct], TyVarEnv EqualCtList) - kick_out_eqs eqs (acc_out, acc_in) - = (eqs_out ++ acc_out, case eqs_in of - [] -> acc_in - (eq1:_) -> extendVarEnv acc_in (cc_tyvar eq1) eqs_in) - where - (eqs_in, eqs_out) = partition keep_eq eqs - - -- implements criteria K1-K3 in Note [The inert equalities] in TcFlatten - keep_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs_ty, cc_ev = ev - , cc_eq_rel = eq_rel }) - | tv == new_tv - = not (can_rewrite ev) -- (K1) - - | otherwise - = check_k2 && check_k3 - where - check_k2 = not (ev `eqCanRewrite` ev) - || not (can_rewrite ev) - || not (new_tv `elemVarSet` tyVarsOfType rhs_ty) - - check_k3 - | can_rewrite ev - = case eq_rel of - NomEq -> not (rhs_ty `eqType` mkTyVarTy new_tv) - ReprEq -> not (isTyVarExposed new_tv rhs_ty) - - | otherwise - = True - - keep_eq ct = pprPanic "keep_eq" (ppr ct) - -{- -Note [Kicking out inert constraints] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Given a new (a -> ty) inert, we want to kick out an existing inert -constraint if - a) the new constraint can rewrite the inert one - b) 'a' is free in the inert constraint (so that it *will*) - rewrite it if we kick it out. - -For (b) we use tyVarsOfCt, which returns the type variables /and -the kind variables/ that are directly visible in the type. Hence we -will have exposed all the rewriting we care about to make the most -precise kinds visible for matching classes etc. No need to kick out -constraints that mention type variables whose kinds contain this -variable! (Except see Note [Kicking out Irreds].) - -Note [Kicking out Irreds] -~~~~~~~~~~~~~~~~~~~~~~~~~ -There is an awkward special case for Irreds. When we have a -kind-mis-matched equality constraint (a:k1) ~ (ty:k2), we turn it into -an Irred (see Note [Equalities with incompatible kinds] in -TcCanonical). So in this case the free kind variables of k1 and k2 -are not visible. More precisely, the type looks like - (~) k1 (a:k1) (ty:k2) -because (~) has kind forall k. k -> k -> Constraint. So the constraint -itself is ill-kinded. We can "see" k1 but not k2. That's why we use -closeOverKinds to make sure we see k2. - -This is not pretty. Maybe (~) should have kind - (~) :: forall k1 k1. k1 -> k2 -> Constraint - -Note [Kick out insolubles] -~~~~~~~~~~~~~~~~~~~~~~~~~~ -Suppose we have an insoluble alpha ~ [alpha], which is insoluble -because an occurs check. And then we unify alpha := [Int]. -Then we really want to rewrite the insouluble to [Int] ~ [[Int]]. -Now it can be decomposed. Otherwise we end up with a "Can't match -[Int] ~ [[Int]]" which is true, but a bit confusing because the -outer type constructors match. - - -Note [Avoid double unifications] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +{- Note [Avoid double unifications] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The spontaneous solver has to return a given which mentions the unified unification variable *on the left* of the equality. Here is what happens if not: Original wanted: (a ~ alpha), (alpha ~ Int) @@ -1616,7 +1211,7 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls = do { dflags <- getDynFlags ; lkup_inst_res <- matchClassInst dflags inerts cls xis dict_loc ; case lkup_inst_res of - GenInst preds _ s -> do { mapM_ (emitNewDerived dict_loc) preds + GenInst preds _ s -> do { emitNewDeriveds dict_loc preds ; unless s $ insertSafeOverlapFailureTcS work_item ; stopWith fl "Dict/Top (solved)" } @@ -1633,7 +1228,8 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls ; unless s $ insertSafeOverlapFailureTcS work_item ; solve_from_instance theta mk_ev } - NoInstance -> continueWith work_item } + NoInstance -> do { try_fundep_improvement + ; continueWith work_item } } where dict_pred = mkClassPred cls xis dict_loc = ctEvLoc fl @@ -1664,11 +1260,10 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls -- We didn't solve it; so try functional dependencies with -- the instance environment, and return - -- We just land here for Given and Derived; - -- See Note [When improvement happens during solving] -- See also Note [Weird fundeps] try_fundep_improvement - = do { instEnvs <- getInstEnvs + = do { traceTcS "try_fundeps" (ppr work_item) + ; instEnvs <- getInstEnvs ; emitFunDepDeriveds $ improveFromInstEnv instEnvs mk_ct_loc dict_pred } @@ -1740,9 +1335,7 @@ doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc deeper_loc = bumpCtLocDepth loc try_improve - | not (isWanted old_ev) -- Try improvement only for Given/Derived constraints - -- See Note [When improvement happens during solving] - , Just ops <- isBuiltInSynFamTyCon_maybe fam_tc + | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc = do { inert_eqs <- getInertEqs ; let eqns = sfInteractTop ops args (lookupFlattenTyVar inert_eqs fsk) ; mapM_ (unifyDerived loc Nominal) eqns } @@ -1807,13 +1400,10 @@ dischargeFmv :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS () -- kick out any inert things that are now rewritable dischargeFmv ev fmv co xi = ASSERT2( not (fmv `elemVarSet` tyVarsOfType xi), ppr ev $$ ppr fmv $$ ppr xi ) - do { case ev of - CtWanted { ctev_evar = evar } -> setWantedEvBind evar (EvCoercion co) - CtDerived {} -> return () -- Happens during improvement - CtGiven {} -> pprPanic "dischargeFmv" (ppr ev) - ; unifyTyVar fmv xi - ; n_kicked <- kickOutRewritable Given NomEq fmv - ; traceTcS "dischargeFuv" (ppr fmv <+> equals <+> ppr xi $$ ppr_kicked n_kicked) } + do { setEvBindIfWanted ev (EvCoercion co) + ; unflattenFmv fmv xi + ; n_kicked <- kickOutAfterUnification fmv + ; traceTcS "dischargeFmv" (ppr fmv <+> equals <+> ppr xi $$ ppr_kicked n_kicked) } {- Note [Top-level reductions for type functions] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1872,7 +1462,7 @@ Note [Cached solved FunEqs] When trying to solve, say (FunExpensive big-type ~ ty), it's important to see if we have reduced (FunExpensive big-type) before, lest we simply repeat it. Hence the lookup in inert_solved_funeqs. Moreover -we must use `canRewriteOrSame` because both uses might (say) be Wanteds, +we must use `canDischarge` because both uses might (say) be Wanteds, and we *still* want to save the re-computation. Note [MATCHING-SYNONYMS] @@ -1943,6 +1533,7 @@ It's exactly the same with implicit parameters, except that the Note [When improvement happens during solving] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +During solving we maintain at "model" in the InertCans Improvement for functional dependencies or type-function injectivity means emitting a Derived equality constraint by interacting the work item with an inert item, or with the top-level instances. e.g. @@ -2225,26 +1816,24 @@ Other notes: -} -- | Is the constraint for an implicit CallStack parameter? -isCallStackIP :: CtLoc -> Class -> Type -> Maybe (EvTerm -> EvCallStack) -isCallStackIP loc cls ty - | Just (tc, []) <- splitTyConApp_maybe ty - , cls `hasKey` ipClassNameKey && tc `hasKey` callStackTyConKey +-- i.e. (IP "name" CallStack) +isCallStackIP :: CtLoc -> Class -> [Type] -> Maybe (EvTerm -> EvCallStack) +isCallStackIP loc cls tys + | cls `hasKey` ipClassNameKey + , [_ip_name, ty] <- tys + , Just (tc, _) <- splitTyConApp_maybe ty + , tc `hasKey` callStackTyConKey = occOrigin (ctLocOrigin loc) - where - -- We only want to grab constraints that arose due to the use of an IP or a - -- function call. See Note [Overview of implicit CallStacks] - occOrigin (OccurrenceOf n) - = Just (EvCsPushCall n locSpan) - occOrigin (IPOccOrigin n) - = Just (EvCsTop ('?' `consFS` hsIPNameFS n) locSpan) - occOrigin _ - = Nothing - locSpan - = ctLocSpan loc -isCallStackIP _ _ _ + | otherwise = Nothing + where + locSpan = ctLocSpan loc - + -- We only want to grab constraints that arose due to the use of an IP or a + -- function call. See Note [Overview of implicit CallStacks] + occOrigin (OccurrenceOf n) = Just (EvCsPushCall n locSpan) + occOrigin (IPOccOrigin n) = Just (EvCsTop ('?' `consFS` hsIPNameFS n) locSpan) + occOrigin _ = Nothing -- | Assumes that we've checked that this is the 'Typeable' class, -- and it was applied to the correct argument. diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs index a70759fa7d..1509356721 100644 --- a/compiler/typecheck/TcRnTypes.hs +++ b/compiler/typecheck/TcRnTypes.hs @@ -63,7 +63,7 @@ module TcRnTypes( WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC, andWC, unionsWC, addSimples, addImplics, mkSimpleWC, addInsols, dropDerivedWC, dropDerivedSimples, dropDerivedInsols, - insolubleImplic, trulyInsoluble, + isDroppableDerivedLoc, insolubleImplic, trulyInsoluble, Implication(..), ImplicStatus(..), isInsolubleStatus, SubGoalDepth, initialSubGoalDepth, @@ -87,6 +87,8 @@ module TcRnTypes( getEvBindsTcPluginM_maybe, CtFlavour(..), ctEvFlavour, + CtFlavourRole, ctEvFlavourRole, ctFlavourRole, + eqCanRewrite, eqCanRewriteFR, canDischarge, canDischargeF, -- Pretty printing pprEvVarTheta, @@ -1293,17 +1295,18 @@ dropDerivedInsols :: Cts -> Cts dropDerivedInsols insols = filterBag keep insols where -- insols can include Given keep ct - | isDerivedCt ct = keep_orig (ctLocOrigin (ctLoc ct)) + | isDerivedCt ct = not (isDroppableDerivedLoc (ctLoc ct)) | otherwise = True - keep_orig :: CtOrigin -> Bool - keep_orig (KindEqOrigin {}) = True - keep_orig (GivenOrigin {}) = True - keep_orig (FunDepOrigin1 {}) = True - keep_orig (FunDepOrigin2 {}) = True --- keep_orig (FunDepOrigin1 _ loc _ _) = keep_orig (ctLocOrigin loc) --- keep_orig (FunDepOrigin2 _ orig _ _) = keep_orig orig - keep_orig _ = False +isDroppableDerivedLoc :: CtLoc -> Bool +-- Note [Dropping derived constraints] +isDroppableDerivedLoc loc + = case ctLocOrigin loc of + KindEqOrigin {} -> False + GivenOrigin {} -> False + FunDepOrigin1 {} -> False + FunDepOrigin2 {} -> False + _ -> True {- Note [Dropping derived constraints] @@ -1331,6 +1334,14 @@ But (tiresomely) we do keep *some* Derived insolubles: - For Wanteds it is arguably better to get a fundep error than a no-instance error (Trac #9612) +Moreover, we keep *all* derived insolubles under some circumstances: + + * They are looked at by simplifyInfer, to decide whether to + generalise. Example: [W] a ~ Int, [W] a ~ Bool + We get [D] Int ~ Bool, and indeed the constraints are insoluble, + and we want simplifyInfer to see that, even though we don't + ultimately want to generate an (inexplicable) error message from + To distinguish these cases we use the CtOrigin. @@ -1803,6 +1814,93 @@ ctEvFlavour (CtWanted {}) = Wanted ctEvFlavour (CtGiven {}) = Given ctEvFlavour (CtDerived {}) = Derived +-- | Whether or not one 'Ct' can rewrite another is determined by its +-- flavour and its equality relation +type CtFlavourRole = (CtFlavour, EqRel) + +-- | Extract the flavour and role from a 'CtEvidence' +ctEvFlavourRole :: CtEvidence -> CtFlavourRole +ctEvFlavourRole ev = (ctEvFlavour ev, ctEvEqRel ev) + +-- | Extract the flavour and role from a 'Ct' +ctFlavourRole :: Ct -> CtFlavourRole +ctFlavourRole = ctEvFlavourRole . cc_ev + +{- Note [eqCanRewrite] +~~~~~~~~~~~~~~~~~~~ +(eqCanRewrite ct1 ct2) holds if the constraint ct1 (a CTyEqCan of form +tv ~ ty) can be used to rewrite ct2. It must satisfy the properties of +a can-rewrite relation, see Definition [Can-rewrite relation] + +With the solver handling Coercible constraints like equality constraints, +the rewrite conditions must take role into account, never allowing +a representational equality to rewrite a nominal one. + +Note [Wanteds do not rewrite Wanteds] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We don't allow Wanteds to rewrite Wanteds, because that can give rise +to very confusing type error messages. A good example is Trac #8450. +Here's another + f :: a -> Bool + f x = ( [x,'c'], [x,True] ) `seq` True +Here we get + [W] a ~ Char + [W] a ~ Bool +but we do not want to complain about Bool ~ Char! + +Note [Deriveds do rewrite Deriveds] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +However we DO allow Deriveds to rewrite Deriveds, because that's how +improvement works; see Note [The improvement story] in TcInteract. + +However, for now at least I'm only letting (Derived,NomEq) rewrite +(Derived,NomEq) and not doing anything for ReprEq. If we have + eqCanRewriteFR (Derived, NomEq) (Derived, _) = True +then we lose the property of Note [Can-rewrite relation] + R2. If f1 >= f, and f2 >= f, + then either f1 >= f2 or f2 >= f1 +Consider f1 = (Given, ReprEq) + f2 = (Derived, NomEq) + f = (Derived, ReprEq) + +I thought maybe we could never get Derived ReprEq constraints, but +we can; straight from the Wanteds during improvment. And from a Derived +ReprEq we could conceivably get a Derived NomEq improvment (by decomposing +a type constructor with Nomninal role), and hence unify. + +Note [canRewriteOrSame] +~~~~~~~~~~~~~~~~~~~~~~~ +canRewriteOrSame is similar but + * returns True for Wanted/Wanted. + * works for all kinds of constraints, not just CTyEqCans +See the call sites for explanations. +-} + +eqCanRewrite :: CtEvidence -> CtEvidence -> Bool +eqCanRewrite ev1 ev2 = ctEvFlavourRole ev1 `eqCanRewriteFR` ctEvFlavourRole ev2 + +eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool +-- Very important function! +-- See Note [eqCanRewrite] +-- See Note [Wanteds do not rewrite Wanteds] +-- See Note [Deriveds do rewrite Deriveds] +eqCanRewriteFR (Given, NomEq) (_, _) = True +eqCanRewriteFR (Given, ReprEq) (_, ReprEq) = True +eqCanRewriteFR (Derived, NomEq) (Derived, NomEq) = True +eqCanRewriteFR _ _ = False + +canDischarge :: CtEvidence -> CtEvidence -> Bool +-- See Note [canRewriteOrSame] +canDischarge ev1 ev2 = ctEvFlavour ev1 `canDischargeF` ctEvFlavour ev2 + +canDischargeF :: CtFlavour -> CtFlavour -> Bool +canDischargeF Given _ = True +canDischargeF Wanted Wanted = True +canDischargeF Wanted Derived = True +canDischargeF Derived Derived = True +canDischargeF _ _ = False + + {- ************************************************************************ * * diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs index 3a3f91246f..f067d7499d 100644 --- a/compiler/typecheck/TcSMonad.hs +++ b/compiler/typecheck/TcSMonad.hs @@ -5,9 +5,10 @@ module TcSMonad ( -- The work list WorkList(..), isEmptyWorkList, emptyWorkList, - extendWorkListNonEq, extendWorkListCt, - extendWorkListCts, appendWorkList, selectWorkItem, - workListSize, + extendWorkListNonEq, extendWorkListCt, extendWorkListDerived, + extendWorkListCts, appendWorkList, + selectNextWorkItem, + workListSize, workListWantedCount, updWorkListTcS, updWorkListTcS_return, -- The TcS monad @@ -25,10 +26,11 @@ module TcSMonad ( Freshness(..), freshGoals, isFresh, newTcEvBinds, newWantedEvVar, newWantedEvVarNC, - unifyTyVar, reportUnifications, + unifyTyVar, unflattenFmv, reportUnifications, setEvBind, setWantedEvBind, setEvBindIfWanted, newEvVar, newGivenEvVar, newGivenEvVars, - newDerived, emitNewDerived, checkReductionDepth, + emitNewDerived, emitNewDeriveds, emitNewDerivedEq, + checkReductionDepth, getInstEnvs, getFamInstEnvs, -- Getting the environments getTopEnv, getGblEnv, getTcEvBinds, getTcLevel, @@ -37,34 +39,40 @@ module TcSMonad ( -- Inerts InertSet(..), InertCans(..), updInertTcS, updInertCans, updInertDicts, updInertIrreds, - getNoGivenEqs, setInertCans, getInertEqs, getInertCans, getInertGivens, + getNoGivenEqs, setInertCans, + getInertEqs, getInertCans, getInertModel, getInertGivens, emptyInert, getTcSInerts, setTcSInerts, takeInertInsolubles, - getUnsolvedInerts, checkAllSolved, + getUnsolvedInerts, removeInertCts, - prepareInertsForImplications, - addInertCan, insertInertItemTcS, insertFunEq, + addInertCan, addInertEq, insertFunEq, emitInsoluble, emitWorkNC, emitWorkCt, - EqualCtList, + + -- The Model + InertModel, kickOutAfterUnification, -- Inert Safe Haskell safe-overlap failures addInertSafehask, insertSafeOverlapFailureTcS, updInertSafehask, getSafeOverlapFailures, -- Inert CDictCans - lookupInertDict, findDictsByClass, addDict, addDictsByClass, delDict, partitionDicts, + lookupInertDict, findDictsByClass, addDict, addDictsByClass, + delDict, partitionDicts, foldDicts, filterDicts, -- Inert CTyEqCans - findTyEqs, + EqualCtList, findTyEqs, foldTyEqs, isInInertEqs, -- Inert solved dictionaries addSolvedDict, lookupSolvedDict, + -- Irreds + foldIrreds, + -- The flattening cache lookupFlatCache, extendFlatCache, newFlattenSkolem, -- Flatten skolems -- Inert CFunEqCans - updInertFunEqs, findFunEq, sizeFunEqMap, - findFunEqsByTyCon, findFunEqs, partitionFunEqs, + updInertFunEqs, findFunEq, sizeFunEqMap, filterFunEqs, + findFunEqsByTyCon, findFunEqs, partitionFunEqs, foldFunEqs, instDFunType, -- Instantiation @@ -74,7 +82,7 @@ module TcSMonad ( TcLevel, isTouchableMetaTyVarTcS, isFilledMetaTyVar_maybe, isFilledMetaTyVar, - zonkTyVarsAndFV, zonkTcType, zonkTcTyVar, zonkSimples, zonkWC, + zonkTyVarsAndFV, zonkTcType, zonkTcTypes, zonkTcTyVar, zonkSimples, zonkWC, -- References newTcRef, readTcRef, updTcRef, @@ -122,7 +130,6 @@ import VarSet import Outputable import Bag import UniqSupply - import FastString import Util import TcRnTypes @@ -136,7 +143,7 @@ import Control.Arrow ( first ) import Control.Monad( ap, when, unless, MonadPlus(..) ) import MonadUtils import Data.IORef -import Data.List ( foldl' ) +import Data.List ( foldl', partition ) #ifdef DEBUG import Digraph @@ -164,6 +171,12 @@ so that it's easier to deal with them first, but the separation is not strictly necessary. Notice that non-canonical constraints are also parts of the worklist. +Note [Process derived items last] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We can often solve all goals without processing *any* derived constraints. +The derived constraints are just there to help us if we get stuck. So +we keep them in a separate list. + -} -- See Note [WorkList priorities] @@ -171,39 +184,56 @@ data WorkList = WL { wl_eqs :: [Ct] , wl_funeqs :: [Ct] -- LIFO stack of goals , wl_rest :: [Ct] + , wl_deriv :: [CtEvidence] -- Implicitly non-canonical + -- See Note [Process derived items last] , wl_implics :: Bag Implication -- See Note [Residual implications] } appendWorkList :: WorkList -> WorkList -> WorkList appendWorkList - (WL { wl_eqs = eqs1, wl_funeqs = funeqs1, wl_rest = rest1, wl_implics = implics1 }) - (WL { wl_eqs = eqs2, wl_funeqs = funeqs2, wl_rest = rest2, wl_implics = implics2 }) + (WL { wl_eqs = eqs1, wl_funeqs = funeqs1, wl_rest = rest1 + , wl_deriv = ders1, wl_implics = implics1 }) + (WL { wl_eqs = eqs2, wl_funeqs = funeqs2, wl_rest = rest2 + , wl_deriv = ders2, wl_implics = implics2 }) = WL { wl_eqs = eqs1 ++ eqs2 , wl_funeqs = funeqs1 ++ funeqs2 , wl_rest = rest1 ++ rest2 + , wl_deriv = ders1 ++ ders2 , wl_implics = implics1 `unionBags` implics2 } - workListSize :: WorkList -> Int -workListSize (WL { wl_eqs = eqs, wl_funeqs = funeqs, wl_rest = rest }) - = length eqs + length funeqs + length rest +workListSize (WL { wl_eqs = eqs, wl_funeqs = funeqs, wl_deriv = ders, wl_rest = rest }) + = length eqs + length funeqs + length rest + length ders + +workListWantedCount :: WorkList -> Int +workListWantedCount (WL { wl_eqs = eqs, wl_rest = rest }) + = count isWantedCt eqs + count isWantedCt rest extendWorkListEq :: Ct -> WorkList -> WorkList -extendWorkListEq ct wl - = wl { wl_eqs = ct : wl_eqs wl } +extendWorkListEq ct wl = wl { wl_eqs = ct : wl_eqs wl } + +extendWorkListEqs :: [Ct] -> WorkList -> WorkList +extendWorkListEqs cts wl = wl { wl_eqs = cts ++ wl_eqs wl } extendWorkListFunEq :: Ct -> WorkList -> WorkList -extendWorkListFunEq ct wl - = wl { wl_funeqs = ct : wl_funeqs wl } +extendWorkListFunEq ct wl = wl { wl_funeqs = ct : wl_funeqs wl } extendWorkListNonEq :: Ct -> WorkList -> WorkList -- Extension by non equality -extendWorkListNonEq ct wl - = wl { wl_rest = ct : wl_rest wl } +extendWorkListNonEq ct wl = wl { wl_rest = ct : wl_rest wl } + +extendWorkListDerived :: CtLoc -> CtEvidence -> WorkList -> WorkList +extendWorkListDerived loc ev wl + | isDroppableDerivedLoc loc = wl { wl_deriv = ev : wl_deriv wl } + | otherwise = extendWorkListEq (mkNonCanonical ev) wl + +extendWorkListDeriveds :: CtLoc -> [CtEvidence] -> WorkList -> WorkList +extendWorkListDeriveds loc evs wl + | isDroppableDerivedLoc loc = wl { wl_deriv = evs ++ wl_deriv wl } + | otherwise = extendWorkListEqs (map mkNonCanonical evs) wl extendWorkListImplic :: Implication -> WorkList -> WorkList -extendWorkListImplic implic wl - = wl { wl_implics = implic `consBag` wl_implics wl } +extendWorkListImplic implic wl = wl { wl_implics = implic `consBag` wl_implics wl } extendWorkListCt :: Ct -> WorkList -> WorkList -- Agnostic @@ -224,25 +254,51 @@ extendWorkListCts cts wl = foldr extendWorkListCt wl cts isEmptyWorkList :: WorkList -> Bool isEmptyWorkList (WL { wl_eqs = eqs, wl_funeqs = funeqs - , wl_rest = rest, wl_implics = implics }) - = null eqs && null rest && null funeqs && isEmptyBag implics + , wl_rest = rest, wl_deriv = ders, wl_implics = implics }) + = null eqs && null rest && null funeqs && isEmptyBag implics && null ders emptyWorkList :: WorkList emptyWorkList = WL { wl_eqs = [], wl_rest = [] - , wl_funeqs = [], wl_implics = emptyBag } + , wl_funeqs = [], wl_deriv = [], wl_implics = emptyBag } + +selectWorkItem :: WorkList -> Maybe (Ct, WorkList) +selectWorkItem wl@(WL { wl_eqs = eqs, wl_funeqs = feqs + , wl_rest = rest }) + | ct:cts <- eqs = Just (ct, wl { wl_eqs = cts }) + | ct:fes <- feqs = Just (ct, wl { wl_funeqs = fes }) + | ct:cts <- rest = Just (ct, wl { wl_rest = cts }) + | otherwise = Nothing + +selectDerivedWorkItem :: WorkList -> Maybe (Ct, WorkList) +selectDerivedWorkItem wl@(WL { wl_deriv = ders }) + | ev:evs <- ders = Just (mkNonCanonical ev, wl { wl_deriv = evs }) + | otherwise = Nothing + +selectNextWorkItem :: TcS (Maybe Ct) +selectNextWorkItem + = do { wl_var <- getTcSWorkListRef + ; wl <- wrapTcS (TcM.readTcRef wl_var) + + ; let try :: Maybe (Ct,WorkList) -> TcS (Maybe Ct) -> TcS (Maybe Ct) + try mb_work do_this_if_fail + | Just (ct, new_wl) <- mb_work + = do { checkReductionDepth (ctLoc ct) (ctPred ct) + ; wrapTcS (TcM.writeTcRef wl_var new_wl) + ; return (Just ct) } + | otherwise + = do_this_if_fail -selectWorkItem :: WorkList -> (Maybe Ct, WorkList) -selectWorkItem wl@(WL { wl_eqs = eqs, wl_funeqs = feqs, wl_rest = rest }) - = case (eqs,feqs,rest) of - (ct:cts,_,_) -> (Just ct, wl { wl_eqs = cts }) - (_,ct:fes,_) -> (Just ct, wl { wl_funeqs = fes }) - (_,_,ct:cts) -> (Just ct, wl { wl_rest = cts }) - (_,_,_) -> (Nothing,wl) + ; try (selectWorkItem wl) $ + + do { ics <- getInertCans + ; if inert_count ics == 0 + then return Nothing + else try (selectDerivedWorkItem wl) (return Nothing) } } -- Pretty printing instance Outputable WorkList where ppr (WL { wl_eqs = eqs, wl_funeqs = feqs - , wl_rest = rest, wl_implics = implics }) + , wl_rest = rest, wl_implics = implics, wl_deriv = ders }) = text "WL" <+> (braces $ vcat [ ppUnless (null eqs) $ ptext (sLit "Eqs =") <+> vcat (map ppr eqs) @@ -250,62 +306,63 @@ instance Outputable WorkList where ptext (sLit "Funeqs =") <+> vcat (map ppr feqs) , ppUnless (null rest) $ ptext (sLit "Non-eqs =") <+> vcat (map ppr rest) + , ppUnless (null ders) $ + ptext (sLit "Derived =") <+> vcat (map ppr ders) , ppUnless (isEmptyBag implics) $ ptext (sLit "Implics =") <+> vcat (map ppr (bagToList implics)) ]) -{- -************************************************************************ + +{- ********************************************************************* * * -* Inert Sets * + InertSet: the inert set * * * * -************************************************************************ - -Note [Detailed InertCans Invariants] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The InertCans represents a collection of constraints with the following properties: - - * All canonical +********************************************************************* -} - * No two dictionaries with the same head - * No two CIrreds with the same type - - * Family equations inert wrt top-level family axioms - - * Dictionaries have no matching top-level instance - - * Given family or dictionary constraints don't mention touchable - unification variables - - * Non-CTyEqCan constraints are fully rewritten with respect - to the CTyEqCan equalities (modulo canRewrite of course; - eg a wanted cannot rewrite a given) - - * CTyEqCan equalities: see Note [Applying the inert substitution] - in TcFlatten +data InertSet + = IS { inert_cans :: InertCans + -- Canonical Given, Wanted, Derived (no Solved) + -- Sometimes called "the inert set" -Note [Type family equations] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Type-family equations, of form (ev : F tys ~ ty), live in three places + , inert_flat_cache :: FunEqMap (TcCoercion, TcType, CtFlavour) + -- See Note [Type family equations] + -- If F tys :-> (co, ty, ev), + -- then co :: F tys ~ ty + -- + -- Just a hash-cons cache for use when flattening only + -- These include entirely un-processed goals, so don't use + -- them to solve a top-level goal, else you may end up solving + -- (w:F ty ~ a) by setting w:=w! We just use the flat-cache + -- when allocating a new flatten-skolem. + -- Not necessarily inert wrt top-level equations (or inert_cans) - * The work-list, of course + , inert_solved_dicts :: DictMap CtEvidence + -- Of form ev :: C t1 .. tn + -- See Note [Solved dictionaries] + -- and Note [Do not add superclasses of solved dictionaries] + } - * The inert_flat_cache. This is used when flattening, to get maximal - sharing. It contains lots of things that are still in the work-list. - E.g Suppose we have (w1: F (G a) ~ Int), and (w2: H (G a) ~ Int) in the - work list. Then we flatten w1, dumping (w3: G a ~ f1) in the work - list. Now if we flatten w2 before we get to w3, we still want to - share that (G a). +instance Outputable InertSet where + ppr is = vcat [ ppr $ inert_cans is + , text "Solved dicts" <+> vcat (map ppr (bagToList (dictsToBag (inert_solved_dicts is)))) ] - Because it contains work-list things, DO NOT use the flat cache to solve - a top-level goal. Eg in the above example we don't want to solve w3 - using w3 itself! +emptyInert :: InertSet +emptyInert + = IS { inert_cans = IC { inert_count = 0 + , inert_eqs = emptyVarEnv + , inert_dicts = emptyDicts + , inert_safehask = emptyDicts + , inert_funeqs = emptyFunEqs + , inert_irreds = emptyCts + , inert_insols = emptyCts + , inert_model = emptyVarEnv } + , inert_flat_cache = emptyFunEqs + , inert_solved_dicts = emptyDictMap } - * The inert_funeqs are un-solved but fully processed and in the InertCans. -Note [Solved dictionaries] -~~~~~~~~~~~~~~~~~~~~~~~~~~ +{- Note [Solved dictionaries] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When we apply a top-level instance declararation, we add the "solved" dictionary to the inert_solved_dicts. In general, we use it to avoid creating a new EvVar when we have a new goal that we have solved in @@ -464,14 +521,23 @@ Result d5 := d0 -} --- All Given (fully known) or Wanted or Derived --- See Note [Detailed InertCans Invariants] for more -data InertCans - = IC { inert_eqs :: TyVarEnv EqualCtList - -- All CTyEqCans with NomEq; index is the LHS tyvar +{- ********************************************************************* +* * + InertCans: the canonical inerts +* * +* * +********************************************************************* -} + +data InertCans -- See Note [Detailed InertCans Invariants] for more + = IC { inert_model :: InertModel + + , inert_eqs :: TyVarEnv EqualCtList + -- All Given/Wanted CTyEqCans; index is the LHS tyvar , inert_funeqs :: FunEqMap Ct -- All CFunEqCans; index is the whole family head type. + -- Hence (by CFunEqCan invariants), + -- all Nominal, and all Given/Wanted (no Derived) , inert_dicts :: DictMap Ct -- Dictionaries only, index is the class @@ -492,118 +558,873 @@ data InertCans , inert_insols :: Cts -- Frozen errors (as non-canonicals) + + , inert_count :: Int + -- Number of Wanted goals in + -- inert_eqs, inert_dicts, inert_safehask, inert_irreds + -- Does not include insolubles + -- When non-zero, keep trying to solved } -type EqualCtList = [Ct] -{- -Note [EqualCtList invariants] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - * All are equalities - * All these equalities have the same LHS - * The list is never empty - * No element of the list can rewrite any other +type InertModel = TyVarEnv Ct + -- If a -> ct, then ct is a + -- nominal, Derived, canonical CTyEqCan for [D] (a ~N rhs) + -- The index of the TyVarEnv is the 'a' + -- All saturated info for Given, Wanted, Derived is here - From the fourth invariant it follows that the list is - - A single Given, or - - Any number of Wanteds and/or Deriveds --} --- The Inert Set -data InertSet - = IS { inert_cans :: InertCans - -- Canonical Given, Wanted, Derived (no Solved) - -- Sometimes called "the inert set" +{- Note [Detailed InertCans Invariants] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The InertCans represents a collection of constraints with the following properties: - , inert_flat_cache :: FunEqMap (TcCoercion, TcType, CtFlavour) - -- See Note [Type family equations] - -- If F tys :-> (co, ty, ev), - -- then co :: F tys ~ ty - -- - -- Just a hash-cons cache for use when flattening only - -- These include entirely un-processed goals, so don't use - -- them to solve a top-level goal, else you may end up solving - -- (w:F ty ~ a) by setting w:=w! We just use the flat-cache - -- when allocating a new flatten-skolem. - -- Not necessarily inert wrt top-level equations (or inert_cans) + * All canonical - , inert_solved_dicts :: DictMap CtEvidence - -- Of form ev :: C t1 .. tn - -- See Note [Solved dictionaries] - -- and Note [Do not add superclasses of solved dictionaries] - } + * No two dictionaries with the same head + * No two CIrreds with the same type + + * Family equations inert wrt top-level family axioms + + * Dictionaries have no matching top-level instance + + * Given family or dictionary constraints don't mention touchable + unification variables + + * Non-CTyEqCan constraints are fully rewritten with respect + to the CTyEqCan equalities (modulo canRewrite of course; + eg a wanted cannot rewrite a given) + + * CTyEqCan equalities: see Note [Applying the inert substitution] + in TcFlatten + +Note [Type family equations] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Type-family equations, of form (ev : F tys ~ ty), live in three places + + * The work-list, of course + + * The inert_flat_cache. This is used when flattening, to get maximal + sharing. It contains lots of things that are still in the work-list. + E.g Suppose we have (w1: F (G a) ~ Int), and (w2: H (G a) ~ Int) in the + work list. Then we flatten w1, dumping (w3: G a ~ f1) in the work + list. Now if we flatten w2 before we get to w3, we still want to + share that (G a). + + Because it contains work-list things, DO NOT use the flat cache to solve + a top-level goal. Eg in the above example we don't want to solve w3 + using w3 itself! + + * The inert_funeqs are un-solved but fully processed and in the InertCans. + +Note [inert_model: the inert model] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +* Part of the inert set is the “model” + * The “Model” is an non-idempotent but no-occurs-check + substitution, reflecting *all* *Nominal* equalities (a ~N ty) + that are not immediately soluble by unification. + + * The principal reason for maintaining the model is to generate equalities + that tell us how unify a variable: that is, what Mark Jones calls + "improvement". The same idea is sometimes also called "saturation"; + find all the equalities that must hold in any solution. + + * There are two sources of constraints in the model: + - Derived constraints arising from functional dependencies, or + decomposing injective arguments of type functions, and suchlike. + + - A "shadow copy" for every Given or Wanted (a ~N ty) in + inert_eqs. We imagine that every G/W immediately generates its shadow + constraint, but we refrain from actually generating the constraint itself + until necessary. See (DShadow) and (GWShadow) in + Note [Adding an inert canonical constraint the InertCans] + + * If (a -> ty) is in the model, then it is + as if we had an inert constraint [D] a ~N ty. + + * Domain of the model = skolems + untouchables + + * The inert_eqs are all Given/Wanted. The Derived ones are in the + inert_model only. + + * However inert_dicts, inert_irreds may well contain derived costraints. + +Note [inert_eqs: the inert equalities] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Definition [Can-rewrite relation] +A "can-rewrite" relation between flavours, written f1 >= f2, is a +binary relation with the following properties + + R1. >= is transitive + R2. If f1 >= f, and f2 >= f, + then either f1 >= f2 or f2 >= f1 + +Lemma. If f1 >= f then f1 >= f1 +Proof. By property (R2), with f1=f2 + +Definition [Generalised substitution] +A "generalised substitution" S is a set of triples (a -f-> t), where + a is a type variable + t is a type + f is a flavour +such that + (WF1) if (a -f1-> t1) in S + (a -f2-> t2) in S + then neither (f1 >= f2) nor (f2 >= f1) hold + (WF2) if (a -f-> t) is in S, then t /= a + +Definition [Applying a generalised substitution] +If S is a generalised substitution + S(f,a) = t, if (a -fs-> t) in S, and fs >= f + = a, otherwise +Application extends naturally to types S(f,t), modulo roles. +See Note [Flavours with roles]. + +Theorem: S(f,a) is well defined as a function. +Proof: Suppose (a -f1-> t1) and (a -f2-> t2) are both in S, + and f1 >= f and f2 >= f + Then by (R2) f1 >= f2 or f2 >= f1, which contradicts (WF) + +Notation: repeated application. + S^0(f,t) = t + S^(n+1)(f,t) = S(f, S^n(t)) + +Definition: inert generalised substitution +A generalised substitution S is "inert" iff + + (IG1) there is an n such that + for every f,t, S^n(f,t) = S^(n+1)(f,t) + + (IG2) if (b -f-> t) in S, and f >= f, then S(f,t) = t + that is, each individual binding is "self-stable" + +---------------------------------------------------------------- +Our main invariant: + the inert CTyEqCans should be an inert generalised substitution +---------------------------------------------------------------- + +Note that inertness is not the same as idempotence. To apply S to a +type, you may have to apply it recursive. But inertness does +guarantee that this recursive use will terminate. + +---------- The main theorem -------------- + Suppose we have a "work item" + a -fw-> t + and an inert generalised substitution S, + such that + (T1) S(fw,a) = a -- LHS of work-item is a fixpoint of S(fw,_) + (T2) S(fw,t) = t -- RHS of work-item is a fixpoint of S(fw,_) + (T3) a not in t -- No occurs check in the work item + + (K1) for every (a -fs-> s) in S, then not (fw >= fs) + + (K2) for every (b -fs-> s) in S, where b /= a, then + (K2a) not (fs >= fs) + or (K2b) fs >= fw + or (K2c) not (fw >= fs) + or (K2d) a not in s + + (K3) If (b -fs-> s) is in S with (fw >= fs), then + (K3a) If the role of fs is nominal: s /= a + (K3b) If the role of fs is representational: EITHER + a not in s, OR + the path from the top of s to a includes at least one non-newtype + + then the extended substition T = S+(a -fw-> t) + is an inert generalised substitution. + +The idea is that +* (T1-2) are guaranteed by exhaustively rewriting the work-item + with S(fw,_). + +* T3 is guaranteed by a simple occurs-check on the work item. + +* (K1-3) are the "kick-out" criteria. (As stated, they are really the + "keep" criteria.) If the current inert S contains a triple that does + not satisfy (K1-3), then we remove it from S by "kicking it out", + and re-processing it. + +* Note that kicking out is a Bad Thing, because it means we have to + re-process a constraint. The less we kick out, the better. + TODO: Make sure that kicking out really *is* a Bad Thing. We've assumed + this but haven't done the empirical study to check. + +* Assume we have G>=G, G>=W, D>=D, and that's all. Then, when performing + a unification we add a new given a -G-> ty. But doing so does NOT require + us to kick out an inert wanted that mentions a, because of (K2a). This + is a common case, hence good not to kick out. + +* Lemma (L1): The conditions of the Main Theorem imply that there is no + (a -fs-> t) in S, s.t. (fs >= fw). + Proof. Suppose the contrary (fs >= fw). Then because of (T1), + S(fw,a)=a. But since fs>=fw, S(fw,a) = s, hence s=a. But now we + have (a -fs-> a) in S, which contradicts (WF2). + +* The extended substitution satisfies (WF1) and (WF2) + - (K1) plus (L1) guarantee that the extended substiution satisfies (WF1). + - (T3) guarantees (WF2). + +* (K2) is about inertness. Intuitively, any infinite chain T^0(f,t), + T^1(f,t), T^2(f,T).... must pass through the new work item infnitely + often, since the substution without the work item is inert; and must + pass through at least one of the triples in S infnitely often. + + - (K2a): if not(fs>=fs) then there is no f that fs can rewrite (fs>=f), + and hence this triple never plays a role in application S(f,a). + It is always safe to extend S with such a triple. + + (NB: we could strengten K1) in this way too, but see K3. + + - (K2b): If this holds then, by (T2), b is not in t. So applying the + work item does not genenerate any new opportunities for applying S + + - (K2c): If this holds, we can't pass through this triple infinitely + often, because if we did then fs>=f, fw>=f, hence by (R2) + * either fw>=fs, contradicting K2c + * or fs>=fw; so by the agument in K2b we can't have a loop + + - (K2d): if a not in s, we hae no further opportunity to apply the + work item, similar to (K2b) + + NB: Dimitrios has a PDF that does this in more detail + +Key lemma to make it watertight. + Under the conditions of the Main Theorem, + forall f st fw >= f, a is not in S^k(f,t), for any k + +Also, consider roles more carefully. See Note [Flavours with roles]. + +Completeness +~~~~~~~~~~~~~ +K3: completeness. (K3) is not necessary for the extended substitution +to be inert. In fact K1 could be made stronger by saying + ... then (not (fw >= fs) or not (fs >= fs)) +But it's not enough for S to be inert; we also want completeness. +That is, we want to be able to solve all soluble wanted equalities. +Suppose we have + + work-item b -G-> a + inert-item a -W-> b + +Assuming (G >= W) but not (W >= W), this fulfills all the conditions, +so we could extend the inerts, thus: + + inert-items b -G-> a + a -W-> b + +But if we kicked-out the inert item, we'd get + + work-item a -W-> b + inert-item b -G-> a + +Then rewrite the work-item gives us (a -W-> a), which is soluble via Refl. +So we add one more clause to the kick-out criteria + +Another way to understand (K3) is that we treat an inert item + a -f-> b +in the same way as + b -f-> a +So if we kick out one, we should kick out the other. The orientation +is somewhat accidental. + +When considering roles, we also need the second clause (K3b). Consider + + inert-item a -W/R-> b c + work-item c -G/N-> a + +The work-item doesn't get rewritten by the inert, because (>=) doesn't hold. +We've satisfied conditions (T1)-(T3) and (K1) and (K2). If all we had were +condition (K3a), then we would keep the inert around and add the work item. +But then, consider if we hit the following: + + work-item2 b -G/N-> Id + +where + + newtype Id x = Id x + +For similar reasons, if we only had (K3a), we wouldn't kick the +representational inert out. And then, we'd miss solving the inert, which +now reduced to reflexivity. The solution here is to kick out representational +inerts whenever the tyvar of a work item is "exposed", where exposed means +not under some proper data-type constructor, like [] or Maybe. See +isTyVarExposed in TcType. This is encoded in (K3b). + +Note [Stability of flattening] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The inert_eqs and inert_model, *considered separately* are each stable; +that is, substituting using them will terminate. Considered *together* +they are not. E.g. + + Add: [G] a~[b] to inert set with model [D] b~[a] + + We add [G] a~[b] to inert_eqs, and emit [D] a~[b]. At this point + the combination of inert_eqs and inert_model is not stable. + + Then we canonicalise [D] a~[b] to [D] a~[[a]], and add that to + insolubles as an occurs check. + +* When canonicalizing, the flattener respects flavours. In particular, + when flattening a type variable 'a': + * Derived: look up 'a' in the inert_model + * Given/Wanted: look up 'a' in the inert_eqs + + +Note [Flavours with roles] +~~~~~~~~~~~~~~~~~~~~~~~~~~ +The system described in Note [The inert equalities] discusses an abstract +set of flavours. In GHC, flavours have two components: the flavour proper, +taken from {Wanted, Derived, Given}; and the equality relation (often called +role), taken from {NomEq, ReprEq}. When substituting w.r.t. the inert set, +as described in Note [The inert equalities], we must be careful to respect +roles. For example, if we have + + inert set: a -G/R-> Int + b -G/R-> Bool + + type role T nominal representational + +and we wish to compute S(W/R, T a b), the correct answer is T a Bool, NOT +T Int Bool. The reason is that T's first parameter has a nominal role, and +thus rewriting a to Int in T a b is wrong. Indeed, this non-congruence of +subsitution means that the proof in Note [The inert equalities] may need +to be revisited, but we don't think that the end conclusion is wrong. + +Note [Examples of how the inert_model helps completeness] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +----------- Example 2 (indexed-types/should_fail/T4093a) + Ambiguity check for f: (Foo e ~ Maybe e) => Foo e + + We get [G] Foo e ~ Maybe e + [W] Foo e ~ Foo ee -- ee is a unification variable + [W] Foo ee ~ Maybe ee + + Flatten: [G] Foo e ~ fsk + [G] fsk ~ Maybe e -- (A) + + [W] Foo ee ~ fmv + [W] fmv ~ fsk -- (B) From Foo e ~ Foo ee + [W] fmv ~ Maybe ee + + --> rewrite (B) with (A) + [W] Foo ee ~ fmv + [W] fmv ~ Maybe e + [W] fmv ~ Maybe ee + + But now awe appear to be stuck, since we don't rewrite Wanteds with + Wanteds. But inert_model to the rescue. In the model we first added + fmv -> Maybe e + Then when adding [W] fmv -> Maybe ee to the inert set, we noticed + that the model can rewrite the constraint, and so emit [D] fmv ~ Maybe ee. + That canonicalises to + [D] Maybe e ~ Maybe ee + and that soon yields ee := e, and all is well + +----------- Example 3 (typecheck/should_compile/Improvement.hs) + type instance F Int = Bool + instance (b~Int) => C Bool b + + [W] w1 : C (F alpha) alpha, [W] w2 : F alpha ~ Bool + + If we rewrote wanteds with wanteds, we could rewrite w1 to + C Bool alpha, use the instance to get alpha ~ Int, and solve + the whole thing. + + And that is exactly what happens, in the *Derived* constraints. + In effect we get + + [D] F alpha ~ fmv + [D] C fmv alpha + [D] fmv ~ Bool + + and now we can rewrite (C fmv alpha) with (fmv ~ Bool), ane + we are off to the races. + +----------- Example 4 (Trac #10009, a nasty example): + + f :: (UnF (F b) ~ b) => F b -> () + + g :: forall a. (UnF (F a) ~ a) => a -> () + g _ = f (undefined :: F a) + + For g we get [G] UnF (F a) ~ a + [W] UnF (F beta) ~ beta + [W] F a ~ F beta + Flatten: + [G] g1: F a ~ fsk1 fsk1 := F a + [G] g2: UnF fsk1 ~ fsk2 fsk2 := UnF fsk1 + [G] g3: fsk2 ~ a + + [W] w1: F beta ~ fmv1 + [W] w2: UnF fmv1 ~ fmv2 + [W] w3: beta ~ fmv2 + [W] w5: fmv1 ~ fsk1 -- From F a ~ F beta using flat-cache + -- and re-orient to put meta-var on left + + Unify beta := fmv2 + [W] w1: F fmv2 ~ fmv1 + [W] w2: UnF fmv1 ~ fmv2 + [W] w5: fmv1 ~ fsk1 + + In the model, we have the shadow Deriveds of w1 and w2 + (I name them for convenience even though they are anonymous) + [D] d1: F fmv2 ~ fmv1d + [D] d2: fmv1d ~ fmv1 + [D] d3: UnF fmv1 ~ fmv2d + [D] d4: fmv2d ~ fmv2 + + Now we can rewrite d3 with w5, and match with g2, to get + fmv2d := fsk2 + [D] d1: F fmv2 ~ fmv1d + [D] d2: fmv1d ~ fmv1 + [D] d4: fmv2 ~ fsk2 + + Use g2 to rewrite fsk2 to a. + [D] d1: F fmv2 ~ fmv1d + [D] d2: fmv1d ~ fmv1 + [D] d4: fmv2 ~ a + + Use d4 to rewrite d1, rewrite with g3, + match with g1, to get + fmv1d := fsk1 + [D] d2: fmv1 ~ fsk1 + [D] d4: fmv2 ~ a + + At this point we are stuck so we unflatten this set: + See Note [Orientation of equalities with fmvs] + [W] w1: F fmv2 ~ fmv1 + [W] w2: UnF fmv1 ~ fmv2 + [W] w5: fmv1 ~ fsk1 + [D] d4: fmv2 ~ a + + Unflattening will discharge w1: fmv1 := F fmv2 + It can't discharge w2, so it is kept. But we can + unify fmv2 := fsk2, and that is "progress". Result + [W] w2: UnF (F a) ~ a + [W] w5: F a ~ fsk1 + + And now both of these are easily proved in the next iteration. Phew! +-} instance Outputable InertCans where - ppr ics = vcat [ ptext (sLit "Equalities:") - <+> pprCts (foldVarEnv (\eqs rest -> listToBag eqs `andCts` rest) - emptyCts (inert_eqs ics)) - , ptext (sLit "Type-function equalities:") - <+> pprCts (funEqsToBag (inert_funeqs ics)) - , ptext (sLit "Dictionaries:") - <+> pprCts (dictsToBag (inert_dicts ics)) - , ptext (sLit "Safe Haskell unsafe overlap:") - <+> pprCts (dictsToBag (inert_safehask ics)) - , ptext (sLit "Irreds:") - <+> pprCts (inert_irreds ics) - , text "Insolubles =" <+> -- Clearly print frozen errors - braces (vcat (map ppr (Bag.bagToList $ inert_insols ics))) - ] + ppr (IC { inert_model = model, inert_eqs = eqs + , inert_funeqs = funeqs, inert_dicts = dicts + , inert_safehask = safehask, inert_irreds = irreds + , inert_insols = insols, inert_count = count }) + = braces $ vcat + [ ppUnless (isEmptyVarEnv eqs) $ + ptext (sLit "Equalities:") + <+> pprCts (foldVarEnv (\eqs rest -> listToBag eqs `andCts` rest) emptyCts eqs) + , ppUnless (isEmptyTcAppMap funeqs) $ + ptext (sLit "Type-function equalities =") <+> pprCts (funEqsToBag funeqs) + , ppUnless (isEmptyTcAppMap dicts) $ + ptext (sLit "Dictionaries =") <+> pprCts (dictsToBag dicts) + , ppUnless (isEmptyTcAppMap safehask) $ + ptext (sLit "Safe Haskell unsafe overlap =") <+> pprCts (dictsToBag safehask) + , ppUnless (isEmptyCts irreds) $ + ptext (sLit "Irreds =") <+> pprCts irreds + , ppUnless (isEmptyCts insols) $ + text "Insolubles =" <+> pprCts insols + , ppUnless (isEmptyVarEnv model) $ + text "Model =" <+> pprCts (foldVarEnv consCts emptyCts model) + , text "Unsolved goals =" <+> int count + ] + +{- ********************************************************************* +* * + Adding an inert +* * +************************************************************************ -instance Outputable InertSet where - ppr is = vcat [ ppr $ inert_cans is - , text "Solved dicts" <+> vcat (map ppr (bagToList (dictsToBag (inert_solved_dicts is)))) ] +Note [Adding an inert canonical constraint the InertCans] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +* Adding any constraint c *other* than a CTyEqCan (TcSMonad.addInertCan): -emptyInert :: InertSet -emptyInert - = IS { inert_cans = IC { inert_eqs = emptyVarEnv - , inert_dicts = emptyDicts - , inert_safehask = emptyDicts - , inert_funeqs = emptyFunEqs - , inert_irreds = emptyCts - , inert_insols = emptyCts - } - , inert_flat_cache = emptyFunEqs - , inert_solved_dicts = emptyDictMap } + * If c can be rewritten by model, emit [D] c, as NonCanonical. + See Note [Can be rewritten by model] ---------------- -addInertCan :: InertCans -> Ct -> InertCans + * Reason for non-canonical: a CFunEqCan has a unique fmv on the RHS, + so we must not duplicate it. + +* Adding a *nominal* CTyEqCan (a ~N ty) to the inert set (TcSMonad.addInertEq). + + * We always (G/W/D) kick out constraints that can be rewritten + (respecting flavours) by the new constraint. + - This is done by kickOutRewritable; + see Note [inert_eqs: the inert equalities]. + + - We do not need to kick anything out from the model; we only + add [D] constraints to the model (in effect) and they are + fully rewritten by the model, so (K2b) holds + + - A Derived equality can kick out [D] constraints in inert_dicts, + inert_irreds etc. Nothing in inert_eqs because there are no + Derived constraints in inert_eqs. + + Then, when adding: + + * [Given/Wanted] a ~N ty + 1. (GWShadow) If the model can rewrite (a~ty), then emit [D] a~ty + (GWModel) Otherwise just add a~ty to the model + (Reason: [D] a~ty is inert wrt model, and (K2b) holds) + + 2. Add it to inert_eqs + + * [Given/Wanted] a ~R ty: just add it to inert_eqs + + * [Derived] a ~N ty + 1. (DShadow) Emit shadow-copies (emitDerivedShadows): + For every inert G/W constraint c, st + (a) (a~ty) can rewrite c (see Note [Can be rewritten]), and + (b) the model cannot rewrite c + kick out a Derived *copy*, leaving the original unchanged. + Reason for (b) if the model can rewrite c, then we have already + generated a shadow copy + + 2. Add (a~ty) to the model + NB: 'a' cannot be in fv(ty), because the constraint is canonical. + +* Unifying a:=ty, is like adding [G] a~ty, but we can't make a [D] a~ty, as in + step (1) of the [G/W] case above. So instead, do kickOutAfterUnification: + - Kick out from the model any equality (b~ty2) that mentions 'a' + (i.e. a=b or a in ty2). Example: + [G] a ~ [b], model [D] b ~ [a] + +Note [Can be rewritten] +~~~~~~~~~~~~~~~~~~~~~~~ +What does it mean to say "Constraint c can be rewritten by the model". +See modelCanRewrite, rewritableTyVars. + +Basically it means fvs(c) intersects dom(model). But can the model + [fmv -> ty] rewrite CFunEqCan F Int ~ fmv ? +No: we just look at the LHS of a CFunEqCan. +-} + +addInertEq :: Ct -> TcS () -- Precondition: item /is/ canonical -addInertCan ics item@(CTyEqCan {}) - = ics { inert_eqs = add_eq (inert_eqs ics) item } +addInertEq ct@(CTyEqCan { cc_ev = ev, cc_eq_rel = eq_rel, cc_tyvar = tv }) + = do { traceTcS "addInertEq {" $ + text "Adding new inert equality:" <+> ppr ct + ; ics <- getInertCans + + ; let (kicked_out, ics1) = kickOutRewritable (ctEvFlavour ev, eq_rel) tv ics + ; ics2 <- add_inert_eq ics1 ct + + ; setInertCans ics2 + + ; unless (isEmptyWorkList kicked_out) $ + do { updWorkListTcS (appendWorkList kicked_out) + ; csTraceTcS $ + hang (ptext (sLit "Kick out, tv =") <+> ppr tv) + 2 (vcat [ text "n-kicked =" <+> int (workListSize kicked_out) + , ppr kicked_out ]) } + + ; traceTcS "addInertEq }" $ empty } +addInertEq ct = pprPanic "addInertEq" (ppr ct) + +add_inert_eq :: InertCans -> Ct -> TcS InertCans +add_inert_eq ics@(IC { inert_count = n + , inert_eqs = old_eqs + , inert_model = old_model }) + ct@(CTyEqCan { cc_ev = ev, cc_eq_rel = eq_rel, cc_tyvar = tv }) + | isDerived ev + = do { emitDerivedShadows ics tv + ; return (ics { inert_model = extendVarEnv old_model tv ct }) } + + | ReprEq <- eq_rel + = return new_ics + + -- Nominal equality, Given/Wanted + | modelCanRewrite old_model rw_tvs -- Shadow of new constraint is + = do { emitNewDerivedEq loc pred -- not inert, so emit it + ; return new_ics } + + | otherwise -- Shadow of new constraint is inert wrt model + -- so extend model, and create shadows it can now rewrite + = do { emitDerivedShadows ics tv + ; return (new_ics { inert_model = new_model }) } + where - add_eq :: TyVarEnv EqualCtList -> Ct -> TyVarEnv EqualCtList - add_eq old_list it - = extendVarEnv_C (\old_eqs _new_eqs -> it : old_eqs) - old_list (cc_tyvar it) [it] + loc = ctEvLoc ev + pred = ctEvPred ev + rw_tvs = tyVarsOfType pred + new_ics = ics { inert_eqs = addTyEq old_eqs tv ct + , inert_count = bumpUnsolvedCount ev n } + new_model = extendVarEnv old_model tv derived_ct + derived_ct = ct { cc_ev = CtDerived { ctev_loc = loc, ctev_pred = pred } } + +add_inert_eq _ ct = pprPanic "addInertEq" (ppr ct) + +emitDerivedShadows :: InertCans -> TcTyVar -> TcS () +emitDerivedShadows IC { inert_eqs = tv_eqs + , inert_dicts = dicts + , inert_safehask = safehask + , inert_funeqs = funeqs + , inert_irreds = irreds + , inert_model = model } new_tv + = mapM_ emit_shadow shadows + where + emit_shadow ct = emitNewDerived loc pred + where + ev = ctEvidence ct + pred = ctEvPred ev + loc = ctEvLoc ev + + shadows = foldDicts get_ct dicts $ + foldDicts get_ct safehask $ + foldFunEqs get_ct funeqs $ + foldIrreds get_ct irreds $ + foldTyEqs get_ct tv_eqs [] + -- Ignore insolubles + + get_ct ct cts | want_shadow ct = ct:cts + | otherwise = cts + + want_shadow ct + = not (isDerivedCt ct) -- No need for a shadow of a Derived! + && (new_tv `elemVarSet` rw_tvs) -- New tv can rewrite ct + && not (modelCanRewrite model rw_tvs) -- We have not alrady created a shadow + where + rw_tvs = rewritableTyVars ct + +modelCanRewrite :: InertModel -> TcTyVarSet -> Bool +-- True if there is any intersection between dom(model) and pred +modelCanRewrite model tvs = foldVarSet ((||) . (`elemVarEnv` model)) False tvs + +rewritableTyVars :: Ct -> TcTyVarSet +rewritableTyVars (CFunEqCan { cc_tyargs = tys }) = tyVarsOfTypes tys +rewritableTyVars ct = tyVarsOfType (ctPred ct) -addInertCan ics item@(CFunEqCan { cc_fun = tc, cc_tyargs = tys }) +-------------- +addInertCan :: Ct -> TcS () -- Constraints *other than* equalities +addInertCan ct + = do { traceTcS "insertInertCan {" $ + text "Trying to insert new inert item:" <+> ppr ct + + ; ics <- getInertCans + ; let ics' = add_item ics ct + ; setInertCans ics' + + -- Emit shadow derived if necessary + ; when (not (isDerived ev) && modelCanRewrite (inert_model ics) rw_tvs) + (emitNewDerived (ctEvLoc ev) pred) + + ; traceTcS "addInertCan }" $ empty } + where + rw_tvs = rewritableTyVars ct + ev = ctEvidence ct + pred = ctEvPred ev + +add_item :: InertCans -> Ct -> InertCans +add_item ics item@(CFunEqCan { cc_fun = tc, cc_tyargs = tys }) = ics { inert_funeqs = insertFunEq (inert_funeqs ics) tc tys item } -addInertCan ics item@(CIrredEvCan {}) - = ics { inert_irreds = inert_irreds ics `Bag.snocBag` item } +add_item ics item@(CIrredEvCan { cc_ev = ev }) + = ics { inert_irreds = inert_irreds ics `Bag.snocBag` item + , inert_count = bumpUnsolvedCount ev (inert_count ics) } -- The 'False' is because the irreducible constraint might later instantiate -- to an equality. -- But since we try to simplify first, if there's a constraint function FC with -- type instance FC Int = Show -- we'll reduce a constraint (FC Int a) to Show a, and never add an inert irreducible -addInertCan ics item@(CDictCan { cc_class = cls, cc_tyargs = tys }) - = ics { inert_dicts = addDict (inert_dicts ics) cls tys item } +add_item ics item@(CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys }) + = ics { inert_dicts = addDict (inert_dicts ics) cls tys item + , inert_count = bumpUnsolvedCount ev (inert_count ics) } -addInertCan _ item +add_item _ item = pprPanic "upd_inert set: can't happen! Inserting " $ - ppr item -- Can't be CNonCanonical, CHoleCan, + ppr item -- CTyEqCan is dealt with by addInertEq + -- Can't be CNonCanonical, CHoleCan, -- because they only land in inert_insols --------------- -insertInertItemTcS :: Ct -> TcS () --- Add a new item in the inerts of the monad -insertInertItemTcS item - = do { traceTcS "insertInertItemTcS {" $ - text "Trying to insert new inert item:" <+> ppr item +bumpUnsolvedCount :: CtEvidence -> Int -> Int +bumpUnsolvedCount ev n | isWanted ev = n+1 + | otherwise = n + + +----------------------------------------- +kickOutRewritable :: CtFlavourRole -- Flavour and role of the equality that is + -- being added to the inert set + -> TcTyVar -- The new equality is tv ~ ty + -> InertCans + -> (WorkList, InertCans) + -- NB: Notice that don't kick out constraints from + -- inert_solved_dicts, and inert_solved_funeqs + -- optimistically. But when we lookup we have to + -- take the substitution into account +kickOutRewritable new_fr new_tv + ics@(IC { inert_eqs = tv_eqs + , inert_dicts = dictmap + , inert_safehask = safehask + , inert_funeqs = funeqmap + , inert_irreds = irreds + , inert_insols = insols + , inert_count = n + , inert_model = model }) + | not (new_fr `eqCanRewriteFR` new_fr) + = (emptyWorkList, ics) -- If new_flavour can't rewrite itself, it can't rewrite + -- anything else, so no need to kick out anything + -- This is a common case: wanteds can't rewrite wanteds + + | 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_insols = insols_in + , inert_count = n - workListWantedCount kicked_out + , inert_model = model } + -- Leave the model unchanged + + kicked_out = WL { wl_eqs = tv_eqs_out + , wl_funeqs = feqs_out + , wl_deriv = [] + , wl_rest = bagToList (dicts_out `andCts` irs_out + `andCts` insols_out) + , wl_implics = emptyBag } + + (tv_eqs_out, tv_eqs_in) = foldVarEnv kick_out_eqs ([], emptyVarEnv) tv_eqs + (feqs_out, feqs_in) = partitionFunEqs kick_out_ct funeqmap + (dicts_out, dicts_in) = partitionDicts kick_out_ct dictmap + (irs_out, irs_in) = partitionBag kick_out_irred irreds + (insols_out, insols_in) = partitionBag kick_out_ct insols + -- Kick out even insolubles; see Note [Kick out insolubles] + + can_rewrite :: CtEvidence -> Bool + can_rewrite = (new_fr `eqCanRewriteFR`) . ctEvFlavourRole + + kick_out_ct :: Ct -> Bool + kick_out_ct ct = kick_out_ctev (ctEvidence ct) + + kick_out_ctev :: CtEvidence -> Bool + kick_out_ctev ev = can_rewrite ev + && new_tv `elemVarSet` tyVarsOfType (ctEvPred ev) + -- See Note [Kicking out inert constraints] + + kick_out_irred :: Ct -> Bool + kick_out_irred ct = can_rewrite (cc_ev ct) + && new_tv `elemVarSet` closeOverKinds (TcM.tyVarsOfCt ct) + -- See Note [Kicking out Irreds] + + kick_out_eqs :: EqualCtList -> ([Ct], TyVarEnv EqualCtList) + -> ([Ct], TyVarEnv EqualCtList) + kick_out_eqs eqs (acc_out, acc_in) + = (eqs_out ++ acc_out, case eqs_in of + [] -> acc_in + (eq1:_) -> extendVarEnv acc_in (cc_tyvar eq1) eqs_in) + where + (eqs_in, eqs_out) = partition keep_eq eqs + + -- implements criteria K1-K3 in Note [The inert equalities] in TcFlatten + keep_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs_ty, cc_ev = ev + , cc_eq_rel = eq_rel }) + | tv == new_tv + = not (can_rewrite ev) -- (K1) + + | otherwise + = check_k2 && check_k3 + where + ev_fr = ctEvFlavourRole ev + check_k2 = not (ev_fr `eqCanRewriteFR` ev_fr) + || not (new_fr `eqCanRewriteFR` ev_fr) + || (ev_fr `eqCanRewriteFR` new_fr) + || not (new_tv `elemVarSet` tyVarsOfType rhs_ty) + + check_k3 + | new_fr `eqCanRewriteFR` ev_fr + = case eq_rel of + NomEq -> not (rhs_ty `eqType` mkTyVarTy new_tv) + ReprEq -> not (isTyVarExposed new_tv rhs_ty) + + | otherwise + = True + + keep_eq ct = pprPanic "keep_eq" (ppr ct) + +kickOutAfterUnification :: TcTyVar -> TcS Int +kickOutAfterUnification new_tv + = do { ics <- getInertCans + ; let (kicked_out1, ics1) = kickOutModel new_tv ics + (kicked_out2, ics2) = kickOutRewritable (Given,NomEq) new_tv ics1 + -- Given because the tv := xi is given; NomEq because + -- only nominal equalities are solved by unification + kicked_out = appendWorkList kicked_out1 kicked_out2 + ; setInertCans ics2 + ; updWorkListTcS (appendWorkList kicked_out) + + ; unless (isEmptyWorkList kicked_out) $ + csTraceTcS $ + hang (ptext (sLit "Kick out (unify), tv =") <+> ppr new_tv) + 2 (vcat [ text "n-kicked =" <+> int (workListSize kicked_out) + , text "kicked_out =" <+> ppr kicked_out + , text "Residual inerts =" <+> ppr ics2 ]) + ; return (workListSize kicked_out) } + +kickOutModel :: TcTyVar -> InertCans -> (WorkList, InertCans) +kickOutModel new_tv ics@(IC { inert_model = model, inert_eqs = eqs }) + = (foldVarEnv add emptyWorkList der_out, ics { inert_model = new_model }) + where + (der_out, new_model) = partitionVarEnv kick_out_der model + + kick_out_der :: Ct -> Bool + kick_out_der (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs }) + = new_tv == tv || new_tv `elemVarSet` tyVarsOfType rhs + kick_out_der _ = False + + add :: Ct -> WorkList -> WorkList + -- Don't kick out a Derived if there is a Given or Wanted with + -- the same predicate. The model is just a shadow copy, and the + -- Given/Wanted will serve the purpose. + add (CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = rhs }) wl + | not (isInInertEqs eqs tv rhs) = extendWorkListDerived (ctEvLoc ev) ev wl + add _ wl = wl + +{- +Note [Kicking out inert constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Given a new (a -> ty) inert, we want to kick out an existing inert +constraint if + a) the new constraint can rewrite the inert one + b) 'a' is free in the inert constraint (so that it *will*) + rewrite it if we kick it out. + +For (b) we use tyVarsOfCt, which returns the type variables /and +the kind variables/ that are directly visible in the type. Hence we +will have exposed all the rewriting we care about to make the most +precise kinds visible for matching classes etc. No need to kick out +constraints that mention type variables whose kinds contain this +variable! (Except see Note [Kicking out Irreds].) + +Note [Kicking out Irreds] +~~~~~~~~~~~~~~~~~~~~~~~~~ +There is an awkward special case for Irreds. When we have a +kind-mis-matched equality constraint (a:k1) ~ (ty:k2), we turn it into +an Irred (see Note [Equalities with incompatible kinds] in +TcCanonical). So in this case the free kind variables of k1 and k2 +are not visible. More precisely, the type looks like + (~) k1 (a:k1) (ty:k2) +because (~) has kind forall k. k -> k -> Constraint. So the constraint +itself is ill-kinded. We can "see" k1 but not k2. That's why we use +closeOverKinds to make sure we see k2. + +This is not pretty. Maybe (~) should have kind + (~) :: forall k1 k1. k1 -> k2 -> Constraint + +Note [Kick out insolubles] +~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we have an insoluble alpha ~ [alpha], which is insoluble +because an occurs check. And then we unify alpha := [Int]. +Then we really want to rewrite the insouluble to [Int] ~ [[Int]]. +Now it can be decomposed. Otherwise we end up with a "Can't match +[Int] ~ [[Int]]" which is true, but a bit confusing because the +outer type constructors match. +-} - ; updInertCans (\ics -> addInertCan ics item) - ; traceTcS "insertInertItemTcS }" $ empty } -------------- addInertSafehask :: InertCans -> Ct -> InertCans @@ -634,6 +1455,12 @@ addSolvedDict item cls tys ; updInertTcS $ \ ics -> ics { inert_solved_dicts = addDict (inert_solved_dicts ics) cls tys item } } +{- ********************************************************************* +* * + Other inert-set operations +* * +********************************************************************* -} + updInertTcS :: (InertSet -> InertSet) -> TcS () -- Modify the inert set with the supplied function updInertTcS upd_fn @@ -683,65 +1510,11 @@ updInertIrreds upd_fn = updInertCans $ \ ics -> ics { inert_irreds = upd_fn (inert_irreds ics) } -prepareInertsForImplications :: InertSet -> InertSet --- See Note [Preparing inert set for implications] -prepareInertsForImplications is@(IS { inert_cans = cans }) - = is { inert_cans = getGivens cans - , inert_flat_cache = emptyFunEqs } -- See Note [Do not inherit the flat cache] - where - getGivens (IC { inert_eqs = eqs - , inert_irreds = irreds - , inert_funeqs = funeqs - , inert_dicts = dicts - , inert_safehask = safehask }) - = IC { inert_eqs = filterVarEnv is_given_ecl eqs - , inert_funeqs = filterFunEqs isGivenCt funeqs - , inert_irreds = Bag.filterBag isGivenCt irreds - , inert_dicts = filterDicts isGivenCt dicts - , inert_safehask = filterDicts isGivenCt safehask - , inert_insols = emptyCts } - - is_given_ecl :: EqualCtList -> Bool - is_given_ecl (ct:rest) | isGivenCt ct = ASSERT( null rest ) True - is_given_ecl _ = False - -{- -Note [Do not inherit the flat cache] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We do not want to inherit the flat cache when processing nested -implications. Consider - a ~ F b, forall c. b~Int => blah -If we have F b ~ fsk in the flat-cache, and we push that into the -nested implication, we might miss that F b can be rewritten to F Int, -and hence perhpas solve it. Moreover, the fsk from outside is -flattened out after solving the outer level, but and we don't -do that flattening recursively. - -Note [Preparing inert set for implications] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Before solving the nested implications, we trim the inert set, -retaining only Givens. These givens can be used when solving -the inner implications. - -There might be cases where interactions between wanteds at different levels -could help to solve a constraint. For example - - class C a b | a -> b - (C Int alpha), (forall d. C d blah => C Int a) - -If we pushed the (C Int alpha) inwards, as a given, it can produce a -fundep (alpha~a) and this can float out again and be used to fix -alpha. (In general we can't float class constraints out just in case -(C d blah) might help to solve (C Int a).) But we ignore this possiblity. - -For Derived constraints we don't have evidence, so we do not turn -them into Givens. There can *be* deriving CFunEqCans; see Trac #8129. --} - getInertEqs :: TcS (TyVarEnv EqualCtList) -getInertEqs - = do { inert <- getInertCans - ; return (inert_eqs inert) } +getInertEqs = do { inert <- getInertCans; return (inert_eqs inert) } + +getInertModel :: TcS InertModel +getInertModel = do { inert <- getInertCans; return (inert_model inert) } getInertGivens :: TcS [Ct] -- Returns the Given constraints in the inert set, @@ -766,11 +1539,11 @@ getUnsolvedInerts , inert_funeqs = fun_eqs , inert_irreds = irreds , inert_dicts = idicts - , inert_insols = insols } <- getInertCans + , inert_insols = insols + , inert_model = model } <- getInertCans - ; let unsolved_tv_eqs = foldVarEnv (\cts rest -> - foldr add_if_unsolved rest cts) - emptyCts tv_eqs + ; let der_tv_eqs = foldVarEnv (add_der tv_eqs) emptyCts model -- Want to float these + unsolved_tv_eqs = foldTyEqs add_if_unsolved tv_eqs der_tv_eqs unsolved_fun_eqs = foldFunEqs add_if_unsolved fun_eqs emptyCts unsolved_irreds = Bag.filterBag is_unsolved irreds unsolved_dicts = foldDicts add_if_unsolved idicts emptyCts @@ -789,12 +1562,29 @@ getUnsolvedInerts -- Keep even the given insolubles -- so that we can report dead GADT pattern match branches where + add_der tv_eqs ct cts + | CTyEqCan { cc_tyvar = tv, cc_rhs = rhs } <- ct + , not (isInInertEqs tv_eqs tv rhs) = ct `consBag` cts + | otherwise = cts add_if_unsolved :: Ct -> Cts -> Cts add_if_unsolved ct cts | is_unsolved ct = ct `consCts` cts | otherwise = cts is_unsolved ct = not (isGivenCt ct) -- Wanted or Derived +isInInertEqs :: TyVarEnv EqualCtList -> TcTyVar -> TcType -> Bool +-- True if (a ~N ty) is in the inert set, in either Given or Wanted +isInInertEqs eqs tv rhs + = case lookupVarEnv eqs tv of + Nothing -> False + Just cts -> any (same_pred rhs) cts + where + same_pred rhs ct + | CTyEqCan { cc_rhs = rhs2, cc_eq_rel = eq_rel } <- ct + , NomEq <- eq_rel + , rhs `eqType` rhs2 = True + | otherwise = False + getNoGivenEqs :: TcLevel -- TcLevel of this implication -> [TcTyVar] -- Skolems of this implication -> TcS Bool -- True <=> definitely no residual given equalities @@ -922,25 +1712,6 @@ removeInertCt is ct = CHoleCan {} -> panic "removeInertCt: CHoleCan" -checkAllSolved :: TcS Bool --- True if there are no unsolved wanteds --- Ignore Derived for this purpose, unless in insolubles -checkAllSolved - = do { is <- getTcSInerts - - ; let icans = inert_cans is - unsolved_irreds = Bag.anyBag isWantedCt (inert_irreds icans) - unsolved_dicts = foldDicts ((||) . isWantedCt) - (inert_dicts icans) False - unsolved_funeqs = foldFunEqs ((||) . isWantedCt) - (inert_funeqs icans) False - unsolved_eqs = foldVarEnv ((||) . any isWantedCt) False - (inert_eqs icans) - - ; return (not (unsolved_eqs || unsolved_irreds - || unsolved_dicts || unsolved_funeqs - || not (isEmptyBag (inert_insols icans)))) } - lookupFlatCache :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType, CtFlavour)) lookupFlatCache fam_tc tys = do { IS { inert_flat_cache = flat_cache @@ -980,36 +1751,66 @@ lookupSolvedDict (IS { inert_solved_dicts = solved }) cls tys Just ev -> Just ev _ -> Nothing -{- -************************************************************************ + +{- ********************************************************************* * * - TyEqMap + Irreds * * -************************************************************************ +********************************************************************* -} + +foldIrreds :: (Ct -> b -> b) -> Cts -> b -> b +foldIrreds k irreds z = foldrBag k z irreds + + +{- ********************************************************************* +* * + Type equalities +* * +********************************************************************* -} + +type EqualCtList = [Ct] + +{- Note [EqualCtList invariants] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + * All are equalities + * All these equalities have the same LHS + * The list is never empty + * No element of the list can rewrite any other + + From the fourth invariant it follows that the list is + - A single Given, or + - Any number of Wanteds and/or Deriveds -} -type TyEqMap a = TyVarEnv a +addTyEq :: TyVarEnv EqualCtList -> TcTyVar -> Ct -> TyVarEnv EqualCtList +addTyEq old_list tv it = extendVarEnv_C (\old_eqs _new_eqs -> it : old_eqs) + old_list tv [it] + +foldTyEqs :: (Ct -> b -> b) -> TyVarEnv EqualCtList -> b -> b +foldTyEqs k eqs z + = foldVarEnv (\cts z -> foldr k z cts) z eqs findTyEqs :: InertCans -> TyVar -> EqualCtList findTyEqs icans tv = lookupVarEnv (inert_eqs icans) tv `orElse` [] -delTyEq :: TyEqMap EqualCtList -> TcTyVar -> TcType -> TyEqMap EqualCtList +delTyEq :: TyVarEnv EqualCtList -> TcTyVar -> TcType -> TyVarEnv EqualCtList delTyEq m tv t = modifyVarEnv (filter (not . isThisOne)) m tv where isThisOne (CTyEqCan { cc_rhs = t1 }) = eqType t t1 isThisOne _ = False -{- -************************************************************************ +{- ********************************************************************* * * - TcAppMap, DictMap, FunEqMap + TcAppMap * * -************************************************************************ --} +********************************************************************* -} type TcAppMap a = UniqFM (ListMap TypeMap a) -- Indexed by tycon then the arg types -- Used for types and classes; hence UniqFM +isEmptyTcAppMap :: TcAppMap a -> Bool +isEmptyTcAppMap m = isNullUFM m + emptyTcAppMap :: TcAppMap a emptyTcAppMap = emptyUFM @@ -1048,7 +1849,13 @@ tcAppMapToBag m = foldTcAppMap consBag m emptyBag foldTcAppMap :: (a -> b -> b) -> TcAppMap a -> b -> b foldTcAppMap k m z = foldUFM (foldTM k) z m -------------------------- + +{- ********************************************************************* +* * + DictMap +* * +********************************************************************* -} + type DictMap a = TcAppMap a emptyDictMap :: DictMap a @@ -1099,7 +1906,13 @@ foldDicts = foldTcAppMap emptyDicts :: DictMap a emptyDicts = emptyTcAppMap ------------------------- + +{- ********************************************************************* +* * + FunEqMap +* * +********************************************************************* -} + type FunEqMap a = TcAppMap a -- A map whose key is a (TyCon, [Type]) pair emptyFunEqs :: TcAppMap a @@ -1184,9 +1997,9 @@ data TcSEnv = TcSEnv { tcs_ev_binds :: EvBindsVar, - tcs_unified :: IORef Bool, - -- The "dirty-flag" Bool is set True when - -- we unify a unification variable + tcs_unified :: IORef Int, + -- The number of unification variables we have filled + -- The important thing is whether it is non-zero tcs_count :: IORef Int, -- Global step count @@ -1290,7 +2103,7 @@ runTcSWithEvBinds :: EvBindsVar -> TcS a -> TcM a runTcSWithEvBinds ev_binds_var tcs - = do { unified_var <- TcM.newTcRef False + = do { unified_var <- TcM.newTcRef 0 ; step_count <- TcM.newTcRef 0 ; inert_var <- TcM.newTcRef is ; wl_var <- TcM.newTcRef emptyWorkList @@ -1364,6 +2177,19 @@ nestImplicTcS ref inner_tclvl (TcS thing_inside) ; return res } +{- Note [Do not inherit the flat cache] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We do not want to inherit the flat cache when processing nested +implications. Consider + a ~ F b, forall c. b~Int => blah +If we have F b ~ fsk in the flat-cache, and we push that into the +nested implication, we might miss that F b can be rewritten to F Int, +and hence perhpas solve it. Moreover, the fsk from outside is +flattened out after solving the outer level, but and we don't +do that flattening recursively. +-} + + recoverTcS :: TcS a -> TcS a -> TcS a recoverTcS (TcS recovery_code) (TcS thing_inside) = TcS $ \ env -> @@ -1404,7 +2230,7 @@ tryTcS :: TcS a -> TcS a tryTcS (TcS thing_inside) = TcS $ \env -> do { is_var <- TcM.newTcRef emptyInert - ; unified_var <- TcM.newTcRef False + ; unified_var <- TcM.newTcRef 0 ; ev_binds_var <- TcM.newTcEvBinds ; wl_var <- TcM.newTcRef emptyWorkList ; let nest_env = env { tcs_ev_binds = ev_binds_var @@ -1516,8 +2342,7 @@ getTcEvBindsMap unifyTyVar :: TcTyVar -> TcType -> TcS () -- Unify a meta-tyvar with a type --- We keep track of whether we have done any unifications in tcs_unified, --- but only for *non-flatten* meta-vars +-- We keep track of how many unifications have happened in tcs_unified, -- -- We should never unify the same variable twice! unifyTyVar tv ty @@ -1525,18 +2350,25 @@ unifyTyVar tv ty TcS $ \ env -> do { TcM.traceTc "unifyTyVar" (ppr tv <+> text ":=" <+> ppr ty) ; TcM.writeMetaTyVar tv ty - ; unless (isFmvTyVar tv) $ -- Flatten meta-vars are born and die locally - -- so do not track them in tcs_unified - TcM.writeTcRef (tcs_unified env) True } + ; TcM.updTcRef (tcs_unified env) (+ 1) } + +unflattenFmv :: TcTyVar -> TcType -> TcS () +-- Fill a flatten-meta-var, simply by unifying it. +-- This does NOT count as a unification in tcs_unified. +unflattenFmv tv ty + = ASSERT2( isMetaTyVar tv, ppr tv ) + TcS $ \ _ -> + do { TcM.traceTc "unflattenFmv" (ppr tv <+> text ":=" <+> ppr ty) + ; TcM.writeMetaTyVar tv ty } -reportUnifications :: TcS a -> TcS (Bool, a) +reportUnifications :: TcS a -> TcS (Int, a) reportUnifications (TcS thing_inside) = TcS $ \ env -> - do { inner_unified <- TcM.newTcRef False + do { inner_unified <- TcM.newTcRef 0 ; res <- thing_inside (env { tcs_unified = inner_unified }) - ; dirty <- TcM.readTcRef inner_unified - ; TcM.updTcRef (tcs_unified env) (|| dirty) -- Inner unifications affect - ; return (dirty, res) } -- the outer scope too + ; n_unifs <- TcM.readTcRef inner_unified + ; TcM.updTcRef (tcs_unified env) (+ n_unifs) -- Inner unifications affect + ; return (n_unifs, res) } -- the outer scope too getDefaultInfo :: TcS ([Type], (Bool, Bool)) getDefaultInfo = wrapTcS TcM.tcGetDefaultTys @@ -1602,6 +2434,9 @@ zonkTyVarsAndFV tvs = wrapTcS (TcM.zonkTyVarsAndFV tvs) zonkTcType :: TcType -> TcS TcType zonkTcType ty = wrapTcS (TcM.zonkTcType ty) +zonkTcTypes :: [TcType] -> TcS [TcType] +zonkTcTypes tys = wrapTcS (TcM.zonkTcTypes tys) + zonkTcTyVar :: TcTyVar -> TcS TcType zonkTcTyVar tv = wrapTcS (TcM.zonkTcTyVar tv) @@ -1692,9 +2527,10 @@ newFsk fam_ty newFmv fam_ty = wrapTcS $ do { uniq <- TcM.newUnique ; ref <- TcM.newMutVar Flexi + ; cur_lvl <- TcM.getTcLevel ; let details = MetaTv { mtv_info = FlatMetaTv , mtv_ref = ref - , mtv_tclvl = fskTcLevel } + , mtv_tclvl = fmvTcLevel cur_lvl } name = TcM.mkTcTyVarName uniq (fsLit "s") ; return (mkTcTyVar name (typeKind fam_ty) details) } @@ -1787,7 +2623,7 @@ newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence -- See Note [Do not create Given kind equalities] newGivenEvVar loc (pred, rhs) = ASSERT2( not (isKindEquality pred), ppr pred $$ pprCtOrigin (ctLocOrigin loc) ) - do { checkReductionDepth loc pred + do { -- checkReductionDepth loc pred ; new_ev <- newEvVar pred ; setEvBind (mkGivenEvBind new_ev rhs) ; return (CtGiven { ctev_pred = pred, ctev_evar = new_ev, ctev_loc = loc }) } @@ -1841,7 +2677,7 @@ TcCanonical), and will do no harm. newWantedEvVarNC :: CtLoc -> TcPredType -> TcS CtEvidence -- Don't look up in the solved/inerts; we know it's not there newWantedEvVarNC loc pty - = do { checkReductionDepth loc pty + = do { -- checkReductionDepth loc pty ; new_ev <- newEvVar pty ; return (CtWanted { ctev_pred = pty, ctev_evar = new_ev, ctev_loc = loc })} @@ -1858,29 +2694,34 @@ newWantedEvVar loc pty ; return (ctev, Fresh) } } emitNewDerived :: CtLoc -> TcPredType -> TcS () --- Create new Derived and put it in the work list emitNewDerived loc pred - = do { mb_ev <- newDerived loc pred - ; case mb_ev of - Nothing -> return () - Just ev -> do { traceTcS "Emitting [D]" (ppr ev) - ; updWorkListTcS (extendWorkListCt (mkNonCanonical ev)) } } - -newDerived :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence) --- Returns Nothing if cached, --- Just pred if not cached -newDerived loc pred - = do { mb_ct <- lookupInInerts pred - ; case mb_ct of - Just {} -> return Nothing - Nothing -> do { ev <- newDerivedNC loc pred - ; return (Just ev) } } + = do { ev <- newDerivedNC loc pred + ; traceTcS "Emitting new derived" (ppr ev) + ; updWorkListTcS (extendWorkListDerived loc ev) } + +emitNewDeriveds :: CtLoc -> [TcPredType] -> TcS () +emitNewDeriveds loc preds + | null preds + = return () + | otherwise + = do { evs <- mapM (newDerivedNC loc) preds + ; traceTcS "Emitting new deriveds" (ppr evs) + ; updWorkListTcS (extendWorkListDeriveds loc evs) } + +emitNewDerivedEq :: CtLoc -> TcPredType -> TcS () +-- Create new equality Derived and put it in the work list +-- There's no caching, no lookupInInerts +emitNewDerivedEq loc pred + = do { ev <- newDerivedNC loc pred + ; traceTcS "Emitting new derived equality" (ppr ev) + ; updWorkListTcS (extendWorkListDerived loc ev) } newDerivedNC :: CtLoc -> TcPredType -> TcS CtEvidence newDerivedNC loc pred - = do { checkReductionDepth loc pred + = do { -- checkReductionDepth loc pred ; return (CtDerived { ctev_pred = pred, ctev_loc = loc }) } +-- --------- Check done in TcInteract.selectNewWorkItem???? --------- -- | Checks if the depth of the given location is too much. Fails if -- it's too big, with an appropriate error message. checkReductionDepth :: CtLoc -> TcType -- ^ type being reduced diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs index 4deba5b15e..2bcf5eb72d 100644 --- a/compiler/typecheck/TcSimplify.hs +++ b/compiler/typecheck/TcSimplify.hs @@ -18,12 +18,11 @@ import Bag import Class ( classKey ) import Class ( Class ) import DynFlags ( ExtensionFlag( Opt_AllowAmbiguousTypes - , Opt_FlexibleContexts ) ) -import ErrUtils ( emptyMessages ) -import FastString -import Id ( idType ) + , Opt_FlexibleContexts ) + , DynFlags( solverIterations ) ) import Inst -import Kind ( isKind, defaultKind_maybe ) +import Id ( idType ) +import Kind ( isKind, isSubKind, defaultKind_maybe ) import ListSetOps import Maybes ( isNothing ) import Name @@ -45,6 +44,9 @@ import Unify ( tcMatchTy ) import Util import Var import VarSet +import BasicTypes ( IntWithInf, intGtLimit ) +import ErrUtils ( emptyMessages ) +import FastString import Control.Monad ( unless ) import Data.List ( partition ) @@ -862,7 +864,8 @@ solveWanteds wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics ; (floated_eqs, implics2) <- solveNestedImplications (implics `unionBags` implics1) - ; final_wc <- simpl_loop 0 floated_eqs + ; dflags <- getDynFlags + ; final_wc <- simpl_loop 0 (solverIterations dflags) floated_eqs (WC { wc_simple = simples1, wc_impl = implics2 , wc_insol = insols `unionBags` insols1 }) @@ -873,13 +876,16 @@ solveWanteds wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics ; return final_wc } -simpl_loop :: Int -> Cts +simpl_loop :: Int -> IntWithInf -> Cts -> WantedConstraints -> TcS WantedConstraints -simpl_loop n floated_eqs +simpl_loop n limit floated_eqs wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics }) - | n > 10 - = do { traceTcS "solveWanteds: loop!" (ppr wc); return wc } + | n `intGtLimit` limit + = failTcS (hang (ptext (sLit "solveWanteds: too many iterations") + <+> parens (ptext (sLit "limit =") <+> ppr limit)) + 2 (vcat [ ptext (sLit "Set limit with -fsolver-iterations=n; n=0 for no limit") + , ppr wc ] )) | no_floated_eqs = return wc -- Done! @@ -888,22 +894,20 @@ simpl_loop n floated_eqs = do { traceTcS "simpl_loop, iteration" (int n) -- solveSimples may make progress if either float_eqs hold - ; (unifs_happened1, wc1) <- if no_floated_eqs - then return (False, emptyWC) - else reportUnifications $ - solveSimpleWanteds (floated_eqs `unionBags` simples) - -- Put floated_eqs first so they get solved first - -- NB: the floated_eqs may include /derived/ equalities - -- arising from fundeps inside an implication + ; (unifs1, wc1) <- reportUnifications $ + solveSimpleWanteds (floated_eqs `unionBags` simples) + -- Put floated_eqs first so they get solved first + -- NB: the floated_eqs may include /derived/ equalities + -- arising from fundeps inside an implication ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1 -- solveImplications may make progress only if unifs2 holds - ; (floated_eqs2, implics2) <- if not unifs_happened1 && isEmptyBag implics1 + ; (floated_eqs2, implics2) <- if unifs1 == 0 && isEmptyBag implics1 then return (emptyBag, implics) else solveNestedImplications (implics `unionBags` implics1) - ; simpl_loop (n+1) floated_eqs2 + ; simpl_loop (n+1) limit floated_eqs2 (WC { wc_simple = simples1, wc_impl = implics2 , wc_insol = insols `unionBags` insols1 }) } @@ -970,6 +974,7 @@ solveImplication imp@(Implic { ic_tclvl = tclvl ; (floated_eqs, residual_wanted) <- floatEqualities skols no_given_eqs residual_wanted + ; traceTcS "solveImplication 2" (ppr given_insols $$ ppr residual_wanted) ; let final_wanted = residual_wanted `addInsols` given_insols ; res_implic <- setImplicationStatus (imp { ic_no_eqs = no_given_eqs @@ -1565,6 +1570,30 @@ floatEqualities skols no_given_eqs wanteds@(WC { wc_simple = simples }) (float_eqs, remaining_simples) = partitionBag (usefulToFloat is_useful) simples is_useful pred = tyVarsOfType pred `disjointVarSet` skol_set +usefulToFloat :: (TcPredType -> Bool) -> Ct -> Bool +usefulToFloat is_useful_pred ct -- The constraint is un-flattened and de-canonicalised + = is_meta_var_eq pred && is_useful_pred pred + where + pred = ctPred ct + + -- Float out alpha ~ ty, or ty ~ alpha + -- which might be unified outside + -- See Note [Do not float kind-incompatible equalities] + is_meta_var_eq pred + | EqPred NomEq ty1 ty2 <- classifyPredType pred + , let k1 = typeKind ty1 + k2 = typeKind ty2 + = case (tcGetTyVar_maybe ty1, tcGetTyVar_maybe ty2) of + (Just tv1, _) | isMetaTyVar tv1 + , k2 `isSubKind` k1 + -> True + (_, Just tv2) | isMetaTyVar tv2 + , k1 `isSubKind` k2 + -> True + _ -> False + | otherwise + = False + {- Note [Float equalities from under a skolem binding] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Which of the simple equalities can we float out? Obviously, only @@ -1588,6 +1617,13 @@ We had a very complicated rule previously, but this is nice and simple. (To see the notes, look at this Note in a version of TcSimplify prior to Oct 2014). +Note [Do not float kind-incompatible equalities] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +If we have (t::* ~ s::*->*), we'll get a Derived insoluble equality. +If we float the equality outwards, we'll get *another* Derived +insoluble equality one level out, so the same error will be reported +twice. So we refrain from floating such equalities. + Note [Skolem escape] ~~~~~~~~~~~~~~~~~~~~ You might worry about skolem escape with all this floating. diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs index 485c1ba1fd..75d0a5cfd9 100644 --- a/compiler/typecheck/TcType.hs +++ b/compiler/typecheck/TcType.hs @@ -25,7 +25,7 @@ module TcType ( -- TcLevel TcLevel(..), topTcLevel, pushTcLevel, - strictlyDeeperThan, sameDepthAs, fskTcLevel, + strictlyDeeperThan, sameDepthAs, fmvTcLevel, -------------------------------- -- MetaDetails @@ -485,15 +485,14 @@ the whole implication disappears but when we pop out again we are left with uf will get unified *once more* to (F Int). -} -fskTcLevel :: TcLevel -fskTcLevel = TcLevel 0 -- 0 = Outside the outermost level: - -- flatten skolems +fmvTcLevel :: TcLevel -> TcLevel +fmvTcLevel (TcLevel n) = TcLevel (n-1) topTcLevel :: TcLevel topTcLevel = TcLevel 1 -- 1 = outermost level pushTcLevel :: TcLevel -> TcLevel -pushTcLevel (TcLevel us) = TcLevel (us+1) +pushTcLevel (TcLevel us) = TcLevel (us + 2) strictlyDeeperThan :: TcLevel -> TcLevel -> Bool strictlyDeeperThan (TcLevel tv_tclvl) (TcLevel ctxt_tclvl) diff --git a/docs/users_guide/flags.xml b/docs/users_guide/flags.xml index de6c2c8ed8..04157b10bb 100644 --- a/docs/users_guide/flags.xml +++ b/docs/users_guide/flags.xml @@ -712,8 +712,18 @@ </thead> <tbody> <row> + <entry><option>-fconstraint-solver-iterations=</option><replaceable>n</replaceable></entry> + <entry>Set the iteration limit for the type-constraint solver. + The default limit is 4. Typically one iteration + suffices; so please yell if you find you need to set + it higher than the default. Zero means infinity. </entry> + <entry>dynamic</entry> + <entry></entry> + </row> + <row> <entry><option>-freduction-depth=</option><replaceable>n</replaceable></entry> - <entry>set the <link linkend="undecidable-instances">limit for type simplification</link>. Default is 200.</entry> + <entry>Set the <link linkend="undecidable-instances">limit for type simplification</link>. + Default is 200; zero means infinity.</entry> <entry>dynamic</entry> <entry></entry> </row> diff --git a/testsuite/tests/indexed-types/should_fail/T2544.stderr b/testsuite/tests/indexed-types/should_fail/T2544.stderr index 7a1f564c56..0245cb7b6a 100644 --- a/testsuite/tests/indexed-types/should_fail/T2544.stderr +++ b/testsuite/tests/indexed-types/should_fail/T2544.stderr @@ -1,11 +1,22 @@ -
-T2544.hs:17:12:
- Couldn't match type ‘IxMap l’ with ‘IxMap i0’
- NB: ‘IxMap’ is a type function, and may not be injective
- The type variable ‘i0’ is ambiguous
- Expected type: IxMap (l :|: r) [Int]
- Actual type: BiApp (IxMap i0) (IxMap i1) [Int]
- Relevant bindings include
- empty :: IxMap (l :|: r) [Int] (bound at T2544.hs:17:4)
- In the expression: BiApp empty empty
- In an equation for ‘empty’: empty = BiApp empty empty
+ +T2544.hs:17:18: error: + Couldn't match type ‘IxMap i0’ with ‘IxMap l’ + NB: ‘IxMap’ is a type function, and may not be injective + The type variable ‘i0’ is ambiguous + Expected type: IxMap l [Int] + Actual type: IxMap i0 [Int] + Relevant bindings include + empty :: IxMap (l :|: r) [Int] (bound at T2544.hs:17:4) + In the first argument of ‘BiApp’, namely ‘empty’ + In the expression: BiApp empty empty + +T2544.hs:17:24: error: + Couldn't match type ‘IxMap i1’ with ‘IxMap r’ + NB: ‘IxMap’ is a type function, and may not be injective + The type variable ‘i1’ is ambiguous + Expected type: IxMap r [Int] + Actual type: IxMap i1 [Int] + Relevant bindings include + empty :: IxMap (l :|: r) [Int] (bound at T2544.hs:17:4) + In the second argument of ‘BiApp’, namely ‘empty’ + In the expression: BiApp empty empty diff --git a/testsuite/tests/indexed-types/should_fail/T2627b.stderr b/testsuite/tests/indexed-types/should_fail/T2627b.stderr index d6daef1ce9..0b18041825 100644 --- a/testsuite/tests/indexed-types/should_fail/T2627b.stderr +++ b/testsuite/tests/indexed-types/should_fail/T2627b.stderr @@ -1,8 +1,8 @@ -
-T2627b.hs:20:24:
- Occurs check: cannot construct the infinite type:
- b0 ~ Dual (Dual b0)
- The type variable ‘b0’ is ambiguous
- In the expression: conn undefined undefined
- In an equation for ‘conn’:
- conn (Rd k) (Wr a r) = conn undefined undefined
+ +T2627b.hs:20:24: error: + Occurs check: cannot construct the infinite type: + t0 ~ Dual (Dual t0) + The type variable ‘t0’ is ambiguous + In the expression: conn undefined undefined + In an equation for ‘conn’: + conn (Rd k) (Wr a r) = conn undefined undefined diff --git a/testsuite/tests/indexed-types/should_fail/T3330c.stderr b/testsuite/tests/indexed-types/should_fail/T3330c.stderr index 97a54ec5cf..61881d340f 100644 --- a/testsuite/tests/indexed-types/should_fail/T3330c.stderr +++ b/testsuite/tests/indexed-types/should_fail/T3330c.stderr @@ -1,14 +1,14 @@ -T3330c.hs:23:43: +T3330c.hs:23:43: error: Couldn't match kind ‘*’ with ‘* -> *’ When matching types Der ((->) x) :: * -> * R :: (* -> *) -> * - Expected type: Der ((->) x) (f1 x) + Expected type: Der ((->) x) (Der f1 x) Actual type: R f1 Relevant bindings include x :: x (bound at T3330c.hs:23:29) - df :: f1 x (bound at T3330c.hs:23:25) + df :: Der f1 x (bound at T3330c.hs:23:25) plug' :: R f -> Der f x -> x -> f x (bound at T3330c.hs:23:1) In the first argument of ‘plug’, namely ‘rf’ In the first argument of ‘Inl’, namely ‘(plug rf df x)’ diff --git a/testsuite/tests/indexed-types/should_fail/T4254.stderr b/testsuite/tests/indexed-types/should_fail/T4254.stderr index e22fd380ef..e69de29bb2 100644 --- a/testsuite/tests/indexed-types/should_fail/T4254.stderr +++ b/testsuite/tests/indexed-types/should_fail/T4254.stderr @@ -1,4 +0,0 @@ - -T4254.hs:18:10: warning: - Redundant constraint: FD a b - In the type signature for: fails :: (a ~ Int, FD a b) => a -> Bool diff --git a/testsuite/tests/indexed-types/should_fail/T6123.stderr b/testsuite/tests/indexed-types/should_fail/T6123.stderr index 5aec1761e9..8431c4d9fb 100644 --- a/testsuite/tests/indexed-types/should_fail/T6123.stderr +++ b/testsuite/tests/indexed-types/should_fail/T6123.stderr @@ -1,7 +1,7 @@ -T6123.hs:10:14: - Occurs check: cannot construct the infinite type: a0 ~ Id a0 - The type variable ‘a0’ is ambiguous - Relevant bindings include cundefined :: a0 (bound at T6123.hs:10:1) +T6123.hs:10:14: error: + Occurs check: cannot construct the infinite type: t0 ~ Id t0 + The type variable ‘t0’ is ambiguous + Relevant bindings include cundefined :: t0 (bound at T6123.hs:10:1) In the expression: cid undefined In an equation for ‘cundefined’: cundefined = cid undefined diff --git a/testsuite/tests/indexed-types/should_fail/T9662.stderr b/testsuite/tests/indexed-types/should_fail/T9662.stderr index e37e4e907d..596c16c724 100644 --- a/testsuite/tests/indexed-types/should_fail/T9662.stderr +++ b/testsuite/tests/indexed-types/should_fail/T9662.stderr @@ -1,25 +1,25 @@ -T9662.hs:47:8: error: - Couldn't match type ‘k’ with ‘Int’ +T9662.hs:49:7: error: + Couldn't match type ‘k’ with ‘n’ ‘k’ is a rigid type variable bound by the type signature for: test :: Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k) at T9662.hs:44:9 - Expected type: Exp (((sh :. k) :. m) :. n) - -> Exp (((sh :. m) :. n) :. k) - Actual type: Exp - (Tuple (((Atom a0 :. Atom Int) :. Atom Int) :. Atom Int)) - -> Exp - (Plain (((Unlifted (Atom a0) :. Exp Int) :. Exp Int) :. Exp Int)) + ‘n’ is a rigid type variable bound by + the type signature for: + test :: Shape (((sh :. k) :. m) :. n) + -> Shape (((sh :. m) :. n) :. k) + at T9662.hs:44:9 + Expected type: Exp (((sh :. m) :. n) :. k) + -> Exp (((sh :. k) :. m) :. n) + Actual type: Exp (((sh :. k) :. m) :. n) + -> Exp (((sh :. k) :. m) :. n) Relevant bindings include test :: Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k) (bound at T9662.hs:45:1) - In the first argument of ‘backpermute’, namely - ‘(modify - (atom :. atom :. atom :. atom) - (\ (sh :. k :. m :. n) -> (sh :. m :. n :. k)))’ + In the second argument of ‘backpermute’, namely ‘id’ In the expression: backpermute (modify @@ -27,27 +27,27 @@ T9662.hs:47:8: error: (\ (sh :. k :. m :. n) -> (sh :. m :. n :. k))) id -T9662.hs:47:8: error: - Couldn't match type ‘m’ with ‘Int’ +T9662.hs:49:7: error: + Couldn't match type ‘m’ with ‘k’ ‘m’ is a rigid type variable bound by the type signature for: test :: Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k) at T9662.hs:44:9 - Expected type: Exp (((sh :. k) :. m) :. n) - -> Exp (((sh :. m) :. n) :. k) - Actual type: Exp - (Tuple (((Atom a0 :. Atom Int) :. Atom Int) :. Atom Int)) - -> Exp - (Plain (((Unlifted (Atom a0) :. Exp Int) :. Exp Int) :. Exp Int)) + ‘k’ is a rigid type variable bound by + the type signature for: + test :: Shape (((sh :. k) :. m) :. n) + -> Shape (((sh :. m) :. n) :. k) + at T9662.hs:44:9 + Expected type: Exp (((sh :. m) :. n) :. k) + -> Exp (((sh :. k) :. m) :. n) + Actual type: Exp (((sh :. k) :. m) :. n) + -> Exp (((sh :. k) :. m) :. n) Relevant bindings include test :: Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k) (bound at T9662.hs:45:1) - In the first argument of ‘backpermute’, namely - ‘(modify - (atom :. atom :. atom :. atom) - (\ (sh :. k :. m :. n) -> (sh :. m :. n :. k)))’ + In the second argument of ‘backpermute’, namely ‘id’ In the expression: backpermute (modify @@ -55,27 +55,27 @@ T9662.hs:47:8: error: (\ (sh :. k :. m :. n) -> (sh :. m :. n :. k))) id -T9662.hs:47:8: error: - Couldn't match type ‘n’ with ‘Int’ +T9662.hs:49:7: error: + Couldn't match type ‘n’ with ‘m’ ‘n’ is a rigid type variable bound by the type signature for: test :: Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k) at T9662.hs:44:9 - Expected type: Exp (((sh :. k) :. m) :. n) - -> Exp (((sh :. m) :. n) :. k) - Actual type: Exp - (Tuple (((Atom a0 :. Atom Int) :. Atom Int) :. Atom Int)) - -> Exp - (Plain (((Unlifted (Atom a0) :. Exp Int) :. Exp Int) :. Exp Int)) + ‘m’ is a rigid type variable bound by + the type signature for: + test :: Shape (((sh :. k) :. m) :. n) + -> Shape (((sh :. m) :. n) :. k) + at T9662.hs:44:9 + Expected type: Exp (((sh :. m) :. n) :. k) + -> Exp (((sh :. k) :. m) :. n) + Actual type: Exp (((sh :. k) :. m) :. n) + -> Exp (((sh :. k) :. m) :. n) Relevant bindings include test :: Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k) (bound at T9662.hs:45:1) - In the first argument of ‘backpermute’, namely - ‘(modify - (atom :. atom :. atom :. atom) - (\ (sh :. k :. m :. n) -> (sh :. m :. n :. k)))’ + In the second argument of ‘backpermute’, namely ‘id’ In the expression: backpermute (modify diff --git a/testsuite/tests/perf/compiler/all.T b/testsuite/tests/perf/compiler/all.T index ea7e2931d2..bc3e2f1e18 100644 --- a/testsuite/tests/perf/compiler/all.T +++ b/testsuite/tests/perf/compiler/all.T @@ -500,8 +500,8 @@ test('T5837', # 2014-09-03: 37096484 (Windows laptop, w/w for INLINABLE things # 2014-12-01: 135914136 (Windows laptop, regression see below) # 2014-12-08 115905208 Constraint solver perf improvements (esp kick-out) - - (wordsize(64), 53424304, 10)]) + + (wordsize(64), 38834096, 10)]) # sample: 3926235424 (amd64/Linux, 15/2/2012) # 2012-10-02 81879216 # 2012-09-20 87254264 amd64/Linux @@ -516,6 +516,7 @@ test('T5837', # 2014-12-16 231155640 Mac Flattener parameterized over roles; # some optimization # 2015-03-17 53424304 Mac Better depth checking; fails earlier + # 2015-06-09 38834096 Better "improvement"; I'm not sure whey it improves things ], compile_fail,['-freduction-depth=50']) diff --git a/testsuite/tests/typecheck/should_compile/Improvement.hs b/testsuite/tests/typecheck/should_compile/Improvement.hs index fba84ffdec..e7e11901a8 100644 --- a/testsuite/tests/typecheck/should_compile/Improvement.hs +++ b/testsuite/tests/typecheck/should_compile/Improvement.hs @@ -14,4 +14,5 @@ blug = error "Urk" foo :: Bool foo = blug undefined +-- [W] C (F a0) a0, F a0 ~ Bool diff --git a/testsuite/tests/typecheck/should_compile/T10009.hs b/testsuite/tests/typecheck/should_compile/T10009.hs index 5b756b2231..dccab5e434 100644 --- a/testsuite/tests/typecheck/should_compile/T10009.hs +++ b/testsuite/tests/typecheck/should_compile/T10009.hs @@ -14,7 +14,7 @@ g _ = f (undefined :: F a) {- --------------- -[G] UnF (F a) ~ a +[G] UnF (F b) ~ b [W] UnF (F beta) ~ beta [W] F a ~ F beta @@ -60,3 +60,91 @@ g _ = f (undefined :: F a) -- Now we can unify beta! -} + + + +{- + +----- +Inert: [G] fsk_amA ~ b_amr + [G] UnF fsk_amy ~ fsk_amA + [G} F b_amr ~ fsk_amy + +wl: [W] F b_amr ~ F b_amt + +work item: [W] UnF (F b_amt) ~ b_amt + b_amt is the unification variable + +===> b_amt := s_amF + +Inert: [G] fsk_amA ~ b_amr + [G] UnF fsk_amy ~ fsk_amA + [G} F b_amr ~ fsk_amy + +wl: [W] F b_amr ~ F b_amt + [W] UnF s_amD ~ s_amF + +work item: [W] F b_amt ~ s_amD + + +===> +wl: [W] F b_amr ~ F b_amt + [W] UnF s_amD ~ s_amF + +Inert: [G] fsk_amA ~ b_amr + [G] UnF fsk_amy ~ fsk_amA + [G} F b_amr ~ fsk_amy + [W] F s_amF ~ s_amD + +===> +wl: [W] F b_amr ~ F b_amt + +Inert: [G] fsk_amA ~ b_amr + [G] UnF fsk_amy ~ fsk_amA + [G} F b_amr ~ fsk_amy + [W] F s_amF ~ s_amD + [W] UnF s_amD ~ s_amF + +===> +Inert: [G] fsk_amA ~ b_amr + [G] UnF fsk_amy ~ fsk_amA + [G} F b_amr ~ fsk_amy + [W] UnF s_amD ~ s_amF + [W] F s_amF ~ s_amD + +wl: + +work-item: [W] F b_amr ~ F b_amt +--> fsk_amy ~ s_amD +--> s_amD ~ fsk_amy + +===> +Inert: [G] fsk_amA ~ b_amr + [G] UnF fsk_amy ~ fsk_amA + [G} F b_amr ~ fsk_amy + [W] UnF s_amD ~ s_amF + [W] F s_amF ~ s_amD + [W] s_amD ~ fsk_amy + +wl: + +work item: [D] UnF s_amD ~ s_amF + +--> [D] UnF fsk_amy ~ s_amF +--> [D] s_amF ~ fsk_amA + +===> +Inert: [G] fsk_amA ~ b_amr + [G] UnF fsk_amy ~ fsk_amA + [G} F b_amr ~ fsk_amy + [W] UnF s_amD ~ s_amF + [W] F s_amF ~ s_amD + [W] s_amD ~ fsk_amy + [D] s_amF ~ fsk_amA + +wl: + +work item: [D] F s_amF ~ s_amD +--> F fsk_amA ~ s_amD +--> s_amd ~ b_amr +-} diff --git a/testsuite/tests/typecheck/should_compile/tc237.hs b/testsuite/tests/typecheck/should_compile/tc237.hs index 70fcce7bf5..00dc056940 100644 --- a/testsuite/tests/typecheck/should_compile/tc237.hs +++ b/testsuite/tests/typecheck/should_compile/tc237.hs @@ -2,20 +2,23 @@ {-# LANGUAGE RankNTypes, MultiParamTypeClasses, FunctionalDependencies #-} -- This one caught a bug in the implementation of functional --- dependencies, where improvement must happen when +-- dependencies, where improvement must happen when -- checking the call in 'test4' module ShouldCompile where -newtype M s a = M a +newtype M s a = M a class Modular s a | s -> a -wim :: forall a w. Integral a +wim :: forall a w. Integral a => a -> (forall s. Modular s a => M s w) -> w wim i k = error "urk" test4' :: (Modular s a, Integral a) => M s a test4' = error "urk" - + test4 = wim 4 test4' +-- Integral a0, (Modular s a0 => Modular s1 a1, Integral a1, M s1 a1 ~ M s w0) +-- Under the implication, [D] a1 ~ a0, [W] a1 ~ w0 +-- Hence a1 := w0, [D] w0 ~ a0 diff --git a/testsuite/tests/typecheck/should_fail/IPFail.stderr b/testsuite/tests/typecheck/should_fail/IPFail.stderr index d176d931fe..963ccd8b54 100644 --- a/testsuite/tests/typecheck/should_fail/IPFail.stderr +++ b/testsuite/tests/typecheck/should_fail/IPFail.stderr @@ -1,9 +1,9 @@ - -IPFail.hs:6:18: - Could not deduce (Num Bool) arising from the literal ‘5’ - from the context: ?x::Int - bound by the type signature for: f0 :: (?x::Int) => () -> Bool - at IPFail.hs:5:7-31 - In the expression: 5 - In the expression: let ?x = 5 in ?x - In an equation for ‘f0’: f0 () = let ?x = 5 in ?x +
+IPFail.hs:6:18: error:
+ Could not deduce (Num Bool) arising from the literal ‘5’
+ from the context: ?x::Int
+ bound by the type signature for: f0 :: (?x::Int) => () -> Bool
+ at IPFail.hs:5:7-31
+ In the expression: 5
+ In the expression: let ?x = 5 in ?x
+ In an equation for ‘f0’: f0 () = let ?x = 5 in ?x
diff --git a/testsuite/tests/typecheck/should_fail/T5236.hs b/testsuite/tests/typecheck/should_fail/T5236.hs index 07b31c3218..bbef9bb187 100644 --- a/testsuite/tests/typecheck/should_fail/T5236.hs +++ b/testsuite/tests/typecheck/should_fail/T5236.hs @@ -1,6 +1,6 @@ {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts #-} -module Main where +module T5236 where data A data B @@ -13,9 +13,5 @@ instance Id B B loop :: Id A B => Bool loop = True -f :: Bool -f = loop - - -main :: IO () -main = return ()
\ No newline at end of file +-- f :: Bool +-- f = loop diff --git a/testsuite/tests/typecheck/should_fail/T5853.stderr b/testsuite/tests/typecheck/should_fail/T5853.stderr index 3dc36ad758..1489583154 100644 --- a/testsuite/tests/typecheck/should_fail/T5853.stderr +++ b/testsuite/tests/typecheck/should_fail/T5853.stderr @@ -1,19 +1,18 @@ -
-T5853.hs:15:52:
- Could not deduce: fb ~ Subst (Subst (Subst fb b) a) (Elem fb)
- from the context: (F (Subst fb b),
- Elem (Subst fb b) ~ b,
- Subst (Subst fb b) (Elem fb) ~ fb,
- F (Subst (Subst fb b) a),
- Elem (Subst (Subst fb b) a) ~ a,
- Elem (Subst fb b) ~ b,
- Subst (Subst (Subst fb b) a) b ~ Subst fb b)
- bound by the RULE "map/map" at T5853.hs:15:2-57
- ‘fb’ is a rigid type variable bound by
- the RULE "map/map" at T5853.hs:15:2
- Relevant bindings include
- f :: b -> Elem fb (bound at T5853.hs:15:19)
- g :: a -> b (bound at T5853.hs:15:21)
- xs :: Subst (Subst fb b) a (bound at T5853.hs:15:23)
- In the expression: (f . g) <$> xs
- When checking the transformation rule "map/map"
+ +T5853.hs:15:52: error: + Could not deduce: t2 ~ Subst t1 (Elem t2) + from the context: (F t, + Subst t (Elem t2) ~ t2, + Subst t2 (Elem t) ~ t, + F t1, + Subst t1 (Elem t) ~ t, + Subst t (Elem t1) ~ t1) + bound by the RULE "map/map" at T5853.hs:15:2-57 + ‘t2’ is a rigid type variable bound by + the RULE "map/map" at T5853.hs:15:2 + Relevant bindings include + f :: Elem t -> Elem t2 (bound at T5853.hs:15:19) + g :: Elem t1 -> Elem t (bound at T5853.hs:15:21) + xs :: t1 (bound at T5853.hs:15:23) + In the expression: (f . g) <$> xs + When checking the transformation rule "map/map" diff --git a/testsuite/tests/typecheck/should_fail/T5978.hs b/testsuite/tests/typecheck/should_fail/T5978.hs index 2c761ddc98..93633c5a47 100644 --- a/testsuite/tests/typecheck/should_fail/T5978.hs +++ b/testsuite/tests/typecheck/should_fail/T5978.hs @@ -20,6 +20,9 @@ polyBar = undefined monoBar :: Double
monoBar = polyBar id monoFoo
+-- fromA = Float, fromB = Double, toA = toB
+-- [W] C Float to, C Double to
+-- => [D] to ~ Char, [D] to ~ Bool
monoFoo :: Float
monoFoo = polyFoo
diff --git a/testsuite/tests/typecheck/should_fail/T5978.stderr b/testsuite/tests/typecheck/should_fail/T5978.stderr index 9fae4e28fe..bc339695ea 100644 --- a/testsuite/tests/typecheck/should_fail/T5978.stderr +++ b/testsuite/tests/typecheck/should_fail/T5978.stderr @@ -1,8 +1,8 @@ T5978.hs:22:11: error: - Couldn't match type ‘Char’ with ‘Bool’ + Couldn't match type ‘Bool’ with ‘Char’ arising from a functional dependency between: - constraint ‘C Float Bool’ arising from a use of ‘polyBar’ - instance ‘C Float Char’ at T5978.hs:7:10-21 + constraint ‘C Double Char’ arising from a use of ‘polyBar’ + instance ‘C Double Bool’ at T5978.hs:8:10-22 In the expression: polyBar id monoFoo In an equation for ‘monoBar’: monoBar = polyBar id monoFoo diff --git a/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr b/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr index da367d227d..434d5e34a7 100644 --- a/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr +++ b/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr @@ -1,11 +1,11 @@ -TcCoercibleFail.hs:11:8: +TcCoercibleFail.hs:11:8: error: Couldn't match representation of type ‘Int’ with that of ‘()’ In the expression: coerce In the expression: coerce $ one :: () In an equation for ‘foo1’: foo1 = coerce $ one :: () -TcCoercibleFail.hs:14:8: +TcCoercibleFail.hs:14:8: error: Couldn't match representation of type ‘m Int’ with that of ‘m Age’ NB: We cannot know what roles the parameters to ‘m’ have; we must assume that the role is nominal @@ -15,7 +15,7 @@ TcCoercibleFail.hs:14:8: In the expression: coerce $ (return one :: m Int) In an equation for ‘foo2’: foo2 = coerce $ (return one :: m Int) -TcCoercibleFail.hs:16:8: +TcCoercibleFail.hs:16:8: error: Couldn't match type ‘Int’ with ‘Age’ arising from trying to show that the representations of ‘Map Int ()’ and @@ -25,7 +25,7 @@ TcCoercibleFail.hs:16:8: In the expression: coerce $ Map one () :: Map Age () In an equation for ‘foo3’: foo3 = coerce $ Map one () :: Map Age () -TcCoercibleFail.hs:18:8: +TcCoercibleFail.hs:18:8: error: Couldn't match representation of type ‘Int’ with that of ‘Down Int’ Relevant role signatures: type role Down representational The data constructor ‘Down’ of newtype ‘Down’ is not in scope @@ -33,22 +33,21 @@ TcCoercibleFail.hs:18:8: In the expression: coerce $ one :: Down Int In an equation for ‘foo4’: foo4 = coerce $ one :: Down Int -TcCoercibleFail.hs:21:8: +TcCoercibleFail.hs:21:8: error: Couldn't match representation of type ‘Void’ with that of ‘()’ In the expression: coerce :: Void -> () In an equation for ‘foo5’: foo5 = coerce :: Void -> () -TcCoercibleFail.hs:24:9: +TcCoercibleFail.hs:24:9: error: Couldn't match representation of type ‘VoidBad ()’ with that of ‘()’ Relevant role signatures: type role VoidBad phantom In the expression: coerce :: (VoidBad ()) -> () In an equation for ‘foo5'’: foo5' = coerce :: (VoidBad ()) -> () -TcCoercibleFail.hs:28:8: +TcCoercibleFail.hs:28:8: error: Reduction stack overflow; size = 201 - When simplifying the following type: - Coercible (Either Int (Fix (Either Int))) (Fix (Either Age)) + When simplifying the following type: Fix (Either Age) Use -freduction-depth=0 to disable this check (any upper bound you could choose might fail unpredictably with minor updates to GHC, so disabling the check is recommended if @@ -57,7 +56,7 @@ TcCoercibleFail.hs:28:8: In an equation for ‘foo6’: foo6 = coerce :: Fix (Either Int) -> Fix (Either Age) -TcCoercibleFail.hs:29:8: +TcCoercibleFail.hs:29:8: error: Couldn't match representation of type ‘Either Int (Fix (Either Int))’ with that of ‘()’ diff --git a/testsuite/tests/typecheck/should_fail/tcfail138.hs b/testsuite/tests/typecheck/should_fail/tcfail138.hs index bc9992dc17..63485a32df 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail138.hs +++ b/testsuite/tests/typecheck/should_fail/tcfail138.hs @@ -15,7 +15,7 @@ -- think that we'd generate the superclasses (L a b') and (L a b), and now -- the fundep will force b=b'. But GHC is very cautious about generating -- superclasses when doing context reduction for instance declarations, --- becasue of the danger of superclass loops. +-- because of the danger of superclass loops. -- -- So, today, this program fails. It's trivial to fix by adding a fundep for C -- class (G a, L a b) => C a b | a -> b diff --git a/testsuite/tests/typecheck/should_fail/tcfail143.stderr b/testsuite/tests/typecheck/should_fail/tcfail143.stderr index 7c26762a66..14c73d98da 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail143.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail143.stderr @@ -1,8 +1,8 @@ tcfail143.hs:29:9: error: - Couldn't match type ‘Z’ with ‘S Z’ + Couldn't match type ‘S Z’ with ‘Z’ arising from a functional dependency between: constraint ‘MinMax (S Z) Z Z Z’ arising from a use of ‘extend’ - instance ‘MinMax Z b Z b’ at tcfail143.hs:12:10-23 + instance ‘MinMax a Z Z a’ at tcfail143.hs:11:10-23 In the expression: n1 `extend` n0 In an equation for ‘t2’: t2 = n1 `extend` n0 diff --git a/testsuite/tests/typecheck/should_fail/tcfail201.stderr b/testsuite/tests/typecheck/should_fail/tcfail201.stderr index f548f0e72c..3e67742bc8 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail201.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail201.stderr @@ -1,6 +1,6 @@ tcfail201.hs:17:58: error: - Couldn't match expected type ‘a’ with actual type ‘HsDoc t0’ + Couldn't match expected type ‘a’ with actual type ‘HsDoc id0’ ‘a’ is a rigid type variable bound by the type signature for: gfoldl' :: (forall a1 b. c (a1 -> b) -> a1 -> c b) |