diff options
| -rw-r--r-- | compiler/typecheck/TcCanonical.hs | 4 | ||||
| -rw-r--r-- | compiler/typecheck/TcFlatten.hs | 4 | ||||
| -rw-r--r-- | compiler/typecheck/TcInteract.hs | 49 | ||||
| -rw-r--r-- | compiler/typecheck/TcRnTypes.hs | 99 | ||||
| -rw-r--r-- | compiler/typecheck/TcSMonad.hs | 290 | ||||
| -rw-r--r-- | testsuite/tests/indexed-types/should_compile/IndTypesPerfMerge.hs | 44 | ||||
| -rw-r--r-- | testsuite/tests/indexed-types/should_compile/all.T | 1 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_fail/tcfail201.stderr | 4 |
8 files changed, 304 insertions, 191 deletions
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs index fa2b8c8cb5..031c5dbb3f 100644 --- a/compiler/typecheck/TcCanonical.hs +++ b/compiler/typecheck/TcCanonical.hs @@ -1453,9 +1453,9 @@ canEqTyVarTyVar ev eq_rel swapped tv1 tv2 kco2 -- the floating step looks for meta tyvars on the left | isMetaTyVar tv2 = True - -- So neither is a meta tyvar + -- So neither is a meta tyvar (including FlatMetaTv) - -- If only one is a flatten tyvar, put it on the left + -- If only one is a flatten skolem, put it on the left -- See Note [Eliminate flat-skols] | not (isFlattenTyVar tv1), isFlattenTyVar tv2 = True diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs index 20f77a7650..06ef6930cf 100644 --- a/compiler/typecheck/TcFlatten.hs +++ b/compiler/typecheck/TcFlatten.hs @@ -242,7 +242,7 @@ BUT this works badly for Trac #10340: 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 + [W] MonadState 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: @@ -1147,7 +1147,7 @@ flatten_exact_fam_app_fully tc tys ; fr <- getFlavourRole ; case mb_ct of Just (co, rhs_ty, flav) -- co :: F xis ~ fsk - | (flav, NomEq) `canDischargeFR` fr + | (flav, NomEq) `funEqCanDischargeFR` fr -> -- 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) diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs index 6d8567157a..37b86149c6 100644 --- a/compiler/typecheck/TcInteract.hs +++ b/compiler/typecheck/TcInteract.hs @@ -506,7 +506,7 @@ solveOneFromTheOther :: CtEvidence -- Inert -> TcS (InteractResult, StopNowFlag) -- Preconditions: -- 1) inert and work item represent evidence for the /same/ predicate --- 2) ip/class/irred evidence (no coercions) only +-- 2) ip/class/irred constraints only; not used for equalities solveOneFromTheOther ev_i ev_w | isDerived ev_w -- Work item is Derived; just discard it = return (IRKeep, True) @@ -843,7 +843,7 @@ 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 `canDischarge` ev + = if ev_i `funEqCanDischarge` ev then -- Rewrite work-item using inert do { traceTcS "reactFunEq (discharge work item):" $ vcat [ text "workItem =" <+> ppr workItem @@ -851,7 +851,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 `canDischarge` ev_i, ppr ev $$ ppr ev_i ) + ASSERT2( ev `funEqCanDischarge` ev_i, ppr ev $$ ppr ev_i ) do { traceTcS "reactFunEq (rewrite inert item):" $ vcat [ text "workItem =" <+> ppr workItem , text "inertItem=" <+> ppr ev_i ] @@ -881,15 +881,15 @@ improveLocalFunEqs loc inerts fam_tc args fsk = do { traceTcS "interactFunEq improvements: " $ vcat [ ptext (sLit "Eqns:") <+> ppr improvement_eqns , ptext (sLit "Candidates:") <+> ppr funeqs_for_tc - , ptext (sLit "TvEqs:") <+> ppr tv_eqs ] + , ptext (sLit "Model:") <+> ppr model ] ; mapM_ (unifyDerived loc Nominal) improvement_eqns } | otherwise = return () where - tv_eqs = inert_model inerts + model = inert_model inerts funeqs = inert_funeqs inerts funeqs_for_tc = findFunEqsByTyCon funeqs fam_tc - rhs = lookupFlattenTyVar tv_eqs fsk + rhs = lookupFlattenTyVar model fsk -------------------- improvement_eqns @@ -906,14 +906,14 @@ improveLocalFunEqs loc inerts fam_tc args fsk -------------------- do_one_built_in ops (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk }) - = sfInteractInert ops args rhs iargs (lookupFlattenTyVar tv_eqs ifsk) + = sfInteractInert ops args rhs iargs (lookupFlattenTyVar model ifsk) do_one_built_in _ _ = pprPanic "interactFunEq 1" (ppr fam_tc) -------------------- -- See Note [Type inference for type families with injectivity] do_one_injective injective_args (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk }) - | rhs `tcEqType` lookupFlattenTyVar tv_eqs ifsk + | rhs `tcEqType` lookupFlattenTyVar model ifsk = [Pair arg iarg | (arg, iarg, True) <- zip3 args iargs injective_args ] | otherwise @@ -922,8 +922,7 @@ improveLocalFunEqs loc inerts fam_tc args fsk ------------- lookupFlattenTyVar :: InertModel -> TcTyVar -> TcType --- ^ Look up a flatten-tyvar in the inert nominal TyVarEqs; --- this is used only when dealing with a CFunEqCan +-- See Note [lookupFlattenTyVar] lookupFlattenTyVar model ftv = case lookupVarEnv model ftv of Just (CTyEqCan { cc_rhs = rhs, cc_eq_rel = NomEq }) -> rhs @@ -950,7 +949,18 @@ reactFunEq from_this fsk1 solve_this fsk2 ; traceTcS "reactFunEq done" (ppr from_this $$ ppr fsk1 $$ ppr solve_this $$ ppr fsk2) } -{- +{- Note [lookupFlattenTyVar] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Supppose we have an injective function F and + inert_funeqs: F t1 ~ fsk1 + F t2 ~ fsk2 + model fsk1 ~ fsk2 + +We never rewrite the RHS (cc_fsk) of a CFunEqCan. But we /do/ want to +get the [D] t1 ~ t2 from the injectiveness of F. So we look up the +cc_fsk of CFunEqCans in the model when trying to find derived +equalities arising from injectivity. + Note [Type inference for type families with injectivity] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose we have a type family with an injectivity annotation: @@ -1086,10 +1096,10 @@ 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 `canDischarge` ev + , ev_i `eqCanDischarge` ev , rhs_i `tcEqType` rhs ] - = -- Inert: a ~ b - -- Work item: a ~ b + = -- Inert: a ~ ty + -- Work item: a ~ ty do { setEvBindIfWanted ev $ EvCoercion (tcDowngradeRole (eqRelRole eq_rel) (ctEvRole ev_i) @@ -1100,7 +1110,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 `canDischarge` ev + , ev_i `eqCanDischarge` ev , rhs_i `tcEqType` mkTyVarTy tv ] = -- Inert: a ~ b -- Work item: b ~ a @@ -1530,7 +1540,7 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args `mkTcTransCo` ctEvCoercion old_ev) ) ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk } - ; emitWorkCt new_ct + ; updWorkListTcS (extendWorkListFunEq new_ct) ; stopWith old_ev "Fun/Top (given, shortcut)" } | otherwise @@ -1549,8 +1559,9 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args (ax_co `mkTcTransCo` mkTcSymCo (mkTcTyConAppCo Nominal fam_tc cos) `mkTcTransCo` new_co) - ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk } - ; emitWorkCt new_ct + ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc + , cc_tyargs = xis, cc_fsk = fsk } + ; updWorkListTcS (extendWorkListFunEq new_ct) ; stopWith old_ev "Fun/Top (wanted, shortcut)" } where loc = ctEvLoc old_ev @@ -1631,7 +1642,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 `canDischarge` because both uses might (say) be Wanteds, +we must use `funEqCanDischarge` because both uses might (say) be Wanteds, and we *still* want to save the re-computation. Note [MATCHING-SYNONYMS] diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs index cdda69666e..6f2f2e3bdd 100644 --- a/compiler/typecheck/TcRnTypes.hs +++ b/compiler/typecheck/TcRnTypes.hs @@ -112,7 +112,8 @@ module TcRnTypes( CtFlavour(..), ctEvFlavour, CtFlavourRole, ctEvFlavourRole, ctFlavourRole, - eqCanRewrite, eqCanRewriteFR, canDischarge, canDischargeFR, + eqCanRewrite, eqCanRewriteFR, eqCanDischarge, + funEqCanDischarge, funEqCanDischargeFR, -- Pretty printing pprEvVarTheta, @@ -2273,54 +2274,74 @@ 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 [canDischarge] -~~~~~~~~~~~~~~~~~~~ -(x1:c1 `canDischarge` x2:c2) returns True if we can use c1 to -/discharge/ c2; that is, if we can simply drop (x2:c2) altogether, -perhaps adding a binding for x2 in terms of x1. We only ask this -question in two cases: - -* Identical equality constraints: - (x1:s~t) `canDischarge` (xs:s~t) - In this case we can just drop x2 in favour of x1. - -* Function calls with the same LHS: - (x1:F ts ~ f1) `canDischarge` (x2:F ts ~ f2) - Here we can drop x2 in favour of x1, either unifying - f2 (if it's a flatten meta-var) or adding a new Given - (f1 ~ f2), if x2 is a Given. - -This is different from eqCanRewrite; for exammple, a Wanted -can certainly discharge an identical Wanted. So canDicharge -does /not/ define a can-rewrite relation in the sense of -Definition [Can-rewrite relation] in TcSMonad. +Note [funEqCanDischarge] +~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we have two CFunEqCans with the same LHS: + (x1:F ts ~ f1) `funEqCanDischarge` (x2:F ts ~ f2) +Can we drop x2 in favour of x1, either unifying +f2 (if it's a flatten meta-var) or adding a new Given +(f1 ~ f2), if x2 is a Given? + +Answer: yes if funEqCanDischarge is true. + +Note [eqCanDischarge] +~~~~~~~~~~~~~~~~~~~~~ +Suppose we have two identicla equality constraints +(i.e. both LHS and RHS are the same) + (x1:s~t) `eqCanDischarge` (xs:s~t) +Can we just drop x2 in favour of x1? + +Answer: yes if eqCanDischarge is true. + +Note that we do /not/ allow Wanted to discharge Derived. +We must keep both. Why? Because the Derived may rewrite +other Deriveds in the model whereas the Wanted cannot. + +However a Wanted can certainly discharge an identical Wanted. So +eqCanDischarge does /not/ define a can-rewrite relation in the +sense of Definition [Can-rewrite relation] in TcSMonad. -} +----------------- eqCanRewrite :: CtEvidence -> CtEvidence -> Bool -eqCanRewrite ev1 ev2 = eqCanRewriteFR (ctEvFlavourRole ev1) - (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 _ _ = False +eqCanRewrite ev1 ev2 = eqCanRewriteFR (ctEvFlavourRole ev1) + (ctEvFlavourRole ev2) -canDischarge :: CtEvidence -> CtEvidence -> Bool --- See Note [canDischarge] -canDischarge ev1 ev2 = canDischargeFR (ctEvFlavourRole ev1) +eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool +eqCanRewriteFR (Given, NomEq) (_, _) = True +eqCanRewriteFR (Given, ReprEq) (_, ReprEq) = True +eqCanRewriteFR (Derived, NomEq) (Derived, NomEq) = True +eqCanRewriteFR _ _ = False + +----------------- +funEqCanDischarge :: CtEvidence -> CtEvidence -> Bool +-- See Note [funEqCanDischarge] +funEqCanDischarge ev1 ev2 = funEqCanDischargeFR (ctEvFlavourRole ev1) (ctEvFlavourRole ev2) -canDischargeFR :: CtFlavourRole -> CtFlavourRole -> Bool -canDischargeFR (_, ReprEq) (_, NomEq) = False -canDischargeFR (Given, _) _ = True -canDischargeFR (Wanted, _) (Wanted, _) = True -canDischargeFR (Wanted, _) (Derived, _) = True -canDischargeFR (Derived, _) (Derived, _) = True -canDischargeFR _ _ = False +funEqCanDischargeFR :: CtFlavourRole -> CtFlavourRole -> Bool +funEqCanDischargeFR (_, ReprEq) (_, NomEq) = False +funEqCanDischargeFR (Given, _) _ = True +funEqCanDischargeFR (Wanted, _) (Wanted, _) = True +funEqCanDischargeFR (Wanted, _) (Derived, _) = True +funEqCanDischargeFR (Derived, _) (Derived, _) = True +funEqCanDischargeFR _ _ = False + +----------------- +eqCanDischarge :: CtEvidence -> CtEvidence -> Bool +-- See Note [eqCanDischarge] +eqCanDischarge ev1 ev2 = eqCanDischargeFR (ctEvFlavourRole ev1) + (ctEvFlavourRole ev2) +eqCanDischargeFR :: CtFlavourRole -> CtFlavourRole -> Bool +eqCanDischargeFR (_, ReprEq) (_, NomEq) = False +eqCanDischargeFR (Given, _) (Given,_) = True +eqCanDischargeFR (Wanted, _) (Wanted, _) = True +eqCanDischargeFR (Derived, _) (Derived, _) = True +eqCanDischargeFR _ _ = False {- ************************************************************************ diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs index 697f3f9032..099be19d94 100644 --- a/compiler/typecheck/TcSMonad.hs +++ b/compiler/typecheck/TcSMonad.hs @@ -6,7 +6,8 @@ module TcSMonad ( -- The work list WorkList(..), isEmptyWorkList, emptyWorkList, extendWorkListNonEq, extendWorkListCt, extendWorkListDerived, - extendWorkListCts, extendWorkListEq, appendWorkList, + extendWorkListCts, extendWorkListEq, extendWorkListFunEq, + appendWorkList, selectNextWorkItem, workListSize, workListWantedCount, updWorkListTcS, @@ -53,7 +54,7 @@ module TcSMonad ( getUnsolvedInerts, removeInertCts, getPendingScDicts, isPendingScDict, addInertCan, addInertEq, insertFunEq, - emitInsoluble, emitWorkNC, emitWorkCt, + emitInsoluble, emitWorkNC, -- The Model InertModel, kickOutAfterUnification, @@ -243,7 +244,7 @@ extendWorkListDerived loc 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 + | otherwise = extendWorkListEqs (map mkNonCanonical evs) wl extendWorkListImplic :: Implication -> WorkList -> WorkList extendWorkListImplic implic wl = wl { wl_implics = implic `consBag` wl_implics wl } @@ -553,12 +554,16 @@ data InertCans -- See Note [Detailed InertCans Invariants] for more , inert_funeqs :: FunEqMap Ct -- All CFunEqCans; index is the whole family head type. -- All Nominal (that's an invarint of all CFunEqCans) + -- LHS is fully rewritten (modulo eqCanRewrite constraints) + -- wrt inert_eqs/inert_model -- We can get Derived ones from e.g. -- (a) flattening derived equalities -- (b) emitDerivedShadows , inert_dicts :: DictMap Ct -- Dictionaries only + -- All fully rewritten (modulo flavour constraints) + -- wrt inert_eqs/inert_model , inert_safehask :: DictMap Ct -- Failed dictionary resolution due to Safe Haskell overlapping @@ -634,34 +639,38 @@ Type-family equations, of form (ev : F tys ~ ty), live in three places 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. + * All the constraints in the model are Derived CTyEqCans + That is if (a -> ty) is in the model, then + we have an inert constraint [D] a ~N ty. * There are two sources of constraints in the model: + - Derived constraints arising from functional dependencies, or - decomposing injective arguments of type functions, and suchlike. + 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] + - A Derived "shadow copy" for every Given or Wanted (a ~N ty) in + inert_eqs. - * If (a -> ty) is in the model, then it is - as if we had an inert constraint [D] a ~N ty. + * The principal reason for maintaining the model is to generate + equalities that tell us how to unify a variable: that is, what + Mark Jones calls "improvement". The same idea is sometimes also + called "saturation"; find all the equalities that must hold in + any solution. - * Domain of the model = skolems + untouchables + * Domain of the model = skolems + untouchables. + A touchable unification variable wouuld have been unified first. * 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. + * However inert_dicts, inert_funeqs, inert_irreds + may well contain derived costraints. Note [inert_eqs: the inert equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -783,7 +792,7 @@ The idea is that * Lemma (L2): if not (fw >= fw), then K1-K3 all hold. Proof: using Definition [Can-rewrite relation], fw can't rewrite anything - and so K1-K3 hold. Intuitivel, since fw can't rewrite anything, + and so K1-K3 hold. Intuitively, since fw can't rewrite anything, adding it cannot cause any loops This is a common case, because Wanteds cannot rewrite Wanteds. @@ -1085,18 +1094,9 @@ Note [Adding an inert canonical constraint the InertCans] * 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 (they are in the model) + * Always (G/W/D) kick out constraints that can be rewritten + (respecting flavours) by the new constraint. This is done + by kickOutRewritable. Then, when adding: @@ -1104,7 +1104,7 @@ Note [Adding an inert canonical constraint the InertCans] 1. Add (a~ty) to the model NB: 'a' cannot be in fv(ty), because the constraint is canonical. - 2. (DShadow) Emit shadow-copies (emitDerivedShadows): + 2. (DShadow) Do emitDerivedShadows For every inert G/W constraint c, st (a) (a~ty) can rewrite c (see Note [Emitting shadow constraints]), and @@ -1114,18 +1114,18 @@ Note [Adding an inert canonical constraint the InertCans] generated a shadow copy * [Given/Wanted] a ~N ty - 1. Add it to inert_eqs - 2. If the model can rewrite (a~ty) - then (GWShadow) emit [D] a~ty - else (GWModel) Use emitDerivedShadows just like (DShadow) - and add a~ty to the model - (Reason:[D] a~ty is inert wrt model, and (K2b) holds) + 1. Add it to inert_eqs + 2. Emit [D] a~ty + As a result of (2), the current model will rewrite teh new [D] a~ty + during canonicalisation, and then it'll be added to the model using + the steps of [Derived] above. - * [Given/Wanted] a ~R ty: just add it to inert_eqs + * [Representational equalities] a ~R ty: just add it to inert_eqs -* 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: +* 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] @@ -1196,33 +1196,32 @@ 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 - , cc_rhs = rhs }) + , cc_rhs = _rhs }) + | ReprEq <- eq_rel + = return new_ics + +-- | isGiven ev +-- = return (new_ics { inert_model = extendVarEnv old_model tv ct }) } +-- No no! E.g. +-- work-item [G] a ~ [b], model has [D] b ~ a. +-- We must not add the given to the model as-is. Instead, +-- we put a shadow [D] a ~ [b] in the work-list +-- When we process it, we'll rewrite to a ~ [a] and get an occurs check + | isDerived ev = do { emitDerivedShadows ics tv ; return (ics { inert_model = extendVarEnv old_model tv ct }) } - | ReprEq <- eq_rel - = return new_ics - -- Nominal equality (tv ~N ty), Given/Wanted -- See Note [Emitting shadow constraints] - | modelCanRewrite old_model rw_tvs -- Shadow of new ct isn't inert; emit it - = do { emitNewDerivedEq loc (eqRelRole eq_rel) (mkTyVarTy tv) rhs + | otherwise -- modelCanRewrite old_model rw_tvs -- Shadow of new ct isn't inert; emit it + = do { emitNewDerived loc pred ; 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 loc = ctEvLoc ev pred = ctEvPred ev - rw_tvs = tyCoVarsOfType 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) @@ -1233,14 +1232,14 @@ emitDerivedShadows IC { inert_eqs = tv_eqs , inert_funeqs = funeqs , inert_irreds = irreds , inert_model = model } new_tv - = mapM_ emit_shadow shadows + | null shadows + = return () + | otherwise + = do { traceTcS "Emit derived shadows:" $ + vcat [ ptext (sLit "tyvar =") <+> ppr new_tv + , ptext (sLit "shadows =") <+> vcat (map ppr shadows) ] + ; emitWork 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 $ @@ -1248,18 +1247,56 @@ emitDerivedShadows IC { inert_eqs = tv_eqs foldTyEqs get_ct tv_eqs [] -- Ignore insolubles - get_ct ct cts | want_shadow ct = ct:cts + get_ct ct cts | want_shadow ct = mkShadowCt 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, yielding a -- different ct - && not (modelCanRewrite model rw_tvs)-- We have not alrady created a + && not (modelCanRewrite model rw_tvs)-- We have not already created a -- shadow where rw_tvs = rewritableTyCoVars ct +mkShadowCt :: Ct -> Ct +-- Produce a Derived shadow constraint from the input +-- If it is a CFunEqCan, make it NonCanonical, to avoid +-- duplicating the flatten-skolems +-- Otherwise keep the canonical shape. This just saves work, but +-- is sometimes important; see Note [Keep CDictCan shadows as CDictCan] +mkShadowCt ct + | CFunEqCan {} <- ct = CNonCanonical { cc_ev = derived_ev } + | otherwise = ct { cc_ev = derived_ev } + where + ev = ctEvidence ct + derived_ev = CtDerived { ctev_pred = ctEvPred ev + , ctev_loc = ctEvLoc ev } + +{- Note [Keep CDictCan shadows as CDictCan] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we have + class C a => D a b +and [G] D a b, [G] C a in the inert set. Now we insert +[D] b ~ c. We want to kick out a derived shadow for [D] D a b, +so we can rewrite it with the new constraint, and perhaps get +instance reduction or other consequences. + +BUT we do not want to kick out a *non-canonical* (D a b). If we +did, we would do this: + - rewrite it to [D] D a c, with pend_sc = True + - use expandSuperClasses to add C a + - go round again, which solves C a from the givens +This loop goes on for ever and triggers the simpl_loop limit. + +Solution: kick out the CDictCan which will have pend_sc = False, +becuase we've already added its superclasses. So we won't re-add +them. If we forget the pend_sc flag, our cunning scheme for avoiding +generating superclasses repeatedly will fail. + +See Trac #11379 for a case of this. +-} + modelCanRewrite :: InertModel -> TcTyCoVarSet -> Bool -- See Note [Emitting shadow constraints] -- True if there is any intersection between dom(model) and tvs @@ -1285,12 +1322,9 @@ addInertCan ct -- Emit shadow derived if necessary -- See Note [Emitting shadow constraints] - ; let ev = ctEvidence ct - pred = ctEvPred ev - rw_tvs = rewritableTyCoVars ct - - ; when (not (isDerived ev) && modelCanRewrite (inert_model ics) rw_tvs) - (emitNewDerived (ctEvLoc ev) pred) + ; let rw_tvs = rewritableTyCoVars ct + ; when (not (isDerivedCt ct) && modelCanRewrite (inert_model ics) rw_tvs) + (emitWork [mkShadowCt ct]) ; traceTcS "addInertCan }" $ empty } @@ -1328,39 +1362,23 @@ kickOutRewritable :: CtFlavourRole -- Flavour/role of the equality that -> 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_funeqs = funeqmap }) +-- See Note [kickOutRewritable] +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) - -- Lemma (L2) in Note [Extending the inert equalities] - = if isFlattenTyVar new_tv - then (emptyWorkList { wl_funeqs = feqs_out }, ics { inert_funeqs = feqs_in }) - else (emptyWorkList, ics) + = (emptyWorkList, ics) -- If new_fr can't rewrite itself, it can't rewrite -- anything else, so no need to kick out anything. -- (This is a common case: wanteds can't rewrite wanteds) - -- - -- ExCEPT (tiresomely) that we should kick out any CFunEqCans - -- that we should re-examine for their fundeps, even though - -- they can't be *rewrittten*. - -- See Note [Kicking out CFunEqCan for fundeps] - where - (feqs_out, feqs_in) = partitionFunEqs kick_out_fe funeqmap + -- Lemma (L2) in Note [Extending the inert equalities] - kick_out_fe :: Ct -> Bool - kick_out_fe (CFunEqCan { cc_fsk = fsk }) = fsk == new_tv - kick_out_fe _ = False -- Can't happen - -kickOutRewritable new_fr new_tv (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 }) + | otherwise = (kicked_out, inert_cans_in) where inert_cans_in = IC { inert_eqs = tv_eqs_in @@ -1388,20 +1406,24 @@ kickOutRewritable new_fr new_tv (IC { inert_eqs = tv_eqs -- Kick out even insolubles; see Note [Kick out insolubles] fr_can_rewrite :: CtEvidence -> Bool - fr_can_rewrite = (new_fr `eqCanRewriteFR`) . ctEvFlavourRole + fr_can_rewrite ev = new_fr `eqCanRewriteFR` (ctEvFlavourRole ev) kick_out_ct :: Ct -> Bool - kick_out_ct ct = kick_out_ctev (ctEvidence ct) + -- Kick it out if the new CTyEqCan can rewrite the inert + -- one. See Note [kickOutRewritable] + kick_out_ct ct + = fr_can_rewrite ev + && new_tv `elemVarSet` tyCoVarsOfType (ctEvPred ev) + where + ev = ctEvidence ct kick_out_fe :: Ct -> Bool - kick_out_fe (CFunEqCan { cc_ev = ev, cc_fsk = fsk }) - = kick_out_ctev ev || fsk == new_tv - kick_out_fe _ = False -- Can't happen - - kick_out_ctev :: CtEvidence -> Bool - kick_out_ctev ev = fr_can_rewrite ev - && new_tv `elemVarSet` tyCoVarsOfType (ctEvPred ev) - -- See Note [Kicking out inert constraints] + kick_out_fe (CFunEqCan { cc_ev = ev, cc_tyargs = tys, cc_fsk = fsk }) + = new_tv == fsk -- If RHS is new_tvs, kick out /regardless of flavour/ + -- See Note [Kicking out CFunEqCan for fundeps] + || (fr_can_rewrite ev + && new_tv `elemVarSet` tyCoVarsOfTypes tys) + kick_out_fe ct = pprPanic "kick_out_fe" (ppr ct) kick_out_eqs :: EqualCtList -> ([Ct], TyVarEnv EqualCtList) -> ([Ct], TyVarEnv EqualCtList) @@ -1477,20 +1499,39 @@ kickOutModel new_tv ics@(IC { inert_model = model, inert_eqs = eqs }) | 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! + +{- Note [kickOutRewritable] +~~~~~~~~~~~~~~~~~~~~~~~~~~~ +See also Note [inert_eqs: the inert equalities]. + +When we add a new inert equality (a ~N ty) to the inert set, +we must kick out any inert items that could be rewritten by the +new equality, to maintain the inert-set invariants. + + - 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 tyCoVarsOfCt, 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! + + - 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 (they are in the model) + + - We don't kick out constraints from inert_solved_dicts, and + inert_solved_funeqs optimistically. But when we lookup we have to + take the substitution into account + Note [Kick out insolubles] ~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2550,11 +2591,6 @@ emitWork cts = do { traceTcS "Emitting fresh work" (vcat (map ppr cts)) ; updWorkListTcS (extendWorkListCts cts) } -emitWorkCt :: Ct -> TcS () -emitWorkCt ct - = do { traceTcS "Emitting fresh (canonical) work" (ppr ct) - ; updWorkListTcS (extendWorkListCt ct) } - emitInsoluble :: Ct -> TcS () -- Emits a non-canonical constraint that will stand for a frozen error in the inerts. emitInsoluble ct diff --git a/testsuite/tests/indexed-types/should_compile/IndTypesPerfMerge.hs b/testsuite/tests/indexed-types/should_compile/IndTypesPerfMerge.hs index f011bcf465..7cfd19f751 100644 --- a/testsuite/tests/indexed-types/should_compile/IndTypesPerfMerge.hs +++ b/testsuite/tests/indexed-types/should_compile/IndTypesPerfMerge.hs @@ -51,6 +51,50 @@ merge :: -} merge x y = mkMerge (merger x y) x y + +{- ------------- NASTY TYPE FOR merge ----------------- + -- See Trac #11408 + + x:tx, y:ty + mkMerge @ gamma + merger @ alpha beta + merge :: tx -> ty -> tr + +Constraints generated: + gamma ~ MergerType alpha beta + UnmergedLeft gamma ~ tx + UnmergedRight gamma ~ ty + alpha ~ tx + beta ~ ty + tr ~ Merged gamma + Mergeable tx ty + Merger gamma + +One solve path: + gamma := t + tx := alpha := UnmergedLeft t + ty := beta := UnmergedRight t + + Mergeable (UnmergedLeft t) (UnmergedRight t) + Merger t + t ~ MergerType (UnmergedLeft t) (UnmergedRight t) + + LEADS TO AMBIGUOUS TYPE + +Another solve path: + tx := alpha + ty := beta + gamma := MergerType alpha beta + + UnmergedLeft (MergerType alpah beta) ~ alpha + UnmergedRight (MergerType alpah beta) ~ beta + Merger (MergerType alpha beta) + Mergeable alpha beta + + LEADS TO NON-AMBIGUOUS TYPE +--------------- -} + + data TakeRight a data TakeLeft a data DiscardRightHead a b c d diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T index 15c5b3e027..fe2688e109 100644 --- a/testsuite/tests/indexed-types/should_compile/all.T +++ b/testsuite/tests/indexed-types/should_compile/all.T @@ -270,3 +270,4 @@ test('T11067', normal, compile, ['']) test('T10318', normal, compile, ['']) test('UnusedTyVarWarnings', normal, compile, ['-W']) test('UnusedTyVarWarningsNamedWCs', normal, compile, ['-W']) +test('T11408', normal, compile, ['']) diff --git a/testsuite/tests/typecheck/should_fail/tcfail201.stderr b/testsuite/tests/typecheck/should_fail/tcfail201.stderr index 9aef660dbd..b142cb18bd 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail201.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail201.stderr @@ -1,6 +1,6 @@ tcfail201.hs:17:56: error: - • Couldn't match type ‘a’ with ‘HsDoc id0’ + • Couldn't match type ‘a’ with ‘HsDoc t0’ ‘a’ is a rigid type variable bound by the type signature for: gfoldl' :: forall (c :: * -> *) a. @@ -8,7 +8,7 @@ tcfail201.hs:17:56: error: -> (forall g. g -> c g) -> a -> c a at tcfail201.hs:15:12 Expected type: c a - Actual type: c (HsDoc id0) + Actual type: c (HsDoc t0) • In the expression: z DocEmpty In a case alternative: DocEmpty -> z DocEmpty In the expression: case hsDoc of { DocEmpty -> z DocEmpty } |