diff options
| author | Simon Peyton Jones <simonpj@microsoft.com> | 2016-10-25 17:41:45 +0100 |
|---|---|---|
| committer | Simon Peyton Jones <simonpj@microsoft.com> | 2016-11-25 11:18:52 +0000 |
| commit | 1eec1f21268af907f59b5d5c071a9a25de7369c7 (patch) | |
| tree | 818ea9214d94e0a3896ba675b52b737018a74a98 | |
| parent | 0123efde8090fc60a6bfef5943ba35440cec0c69 (diff) | |
| download | haskell-1eec1f21268af907f59b5d5c071a9a25de7369c7.tar.gz | |
Another major constraint-solver refactoring
This patch takes further my refactoring of the constraint
solver, which I've been doing over the last couple of months
in consultation with Richard.
It fixes a number of tricky bugs that made the constraint
solver actually go into a loop, including
Trac #12526
Trac #12444
Trac #12538
The main changes are these
* Flatten unification variables (fmvs/fuvs) appear on the LHS
of a tvar/tyvar equality; thus
fmv ~ alpha
and not
alpha ~ fmv
See Note [Put flatten unification variables on the left]
in TcUnify. This is implemented by TcUnify.swapOverTyVars.
* Don't reduce a "loopy" CFunEqCan where the fsk appears on
the LHS:
F t1 .. tn ~ fsk
where 'fsk' is free in t1..tn.
See Note [FunEq occurs-check principle] in TcInteract
This neatly stops some infinite loops that people reported;
and it allows us to delete some crufty code in reduce_top_fun_eq.
And it appears to be no loss whatsoever.
As well as fixing loops, ContextStack2 and T5837 both terminate
when they didn't before.
* Previously we generated "derived shadow" constraints from
Wanteds, but we could (and sometimes did; Trac #xxxx) repeatedly
generate a derived shadow from the same Wanted.
A big change in this patch is to have two kinds of Wanteds:
[WD] behaves like a pair of a Wanted and a Derived
[W] behaves like a Wanted only
See CtFlavour and ShadowInfo in TcRnTypes, and the ctev_nosh
field of a Wanted.
This turned out to be a lot simpler. A [WD] gets split into a
[W] and a [D] in TcSMonad.maybeEmitShaodow.
See TcSMonad Note [The improvement story and derived shadows]
* Rather than have a separate inert_model in the InertCans, I've
put the derived equalities back into inert_eqs. We weren't
gaining anything from a separate field.
* Previously we had a mode for the constraint solver in which it
would more aggressively solve Derived constraints; it was used
for simplifying the context of a 'deriving' clause, or a 'default'
delcaration, for example.
But the complexity wasn't worth it; now I just make proper Wanted
constraints. See TcMType.cloneWC
* Don't generate injectivity improvement for Givens; see
Note [No FunEq improvement for Givens] in TcInteract
* solveSimpleWanteds leaves the insolubles in-place rather than
returning them. Simpler.
I also did lots of work on comments, including fixing Trac #12821.
48 files changed, 1882 insertions, 1609 deletions
diff --git a/compiler/iface/ToIface.hs b/compiler/iface/ToIface.hs index 48a95a97b2..7e892b68c7 100644 --- a/compiler/iface/ToIface.hs +++ b/compiler/iface/ToIface.hs @@ -107,6 +107,8 @@ toIfaceKind = toIfaceType toIfaceType :: Type -> IfaceType -- Synonyms are retained in the interface type toIfaceType (TyVarTy tv) = IfaceTyVar (toIfaceTyVar tv) +-- | isTcTyVar tv = IfaceTyVar (toIfaceTyVar tv `appendFS` consFS '_' (mkFastString (showSDocUnsafe (ppr (getUnique tv))))) +-- | otherwise toIfaceType (AppTy t1 t2) = IfaceAppTy (toIfaceType t1) (toIfaceType t2) toIfaceType (LitTy n) = IfaceLitTy (toIfaceTyLit n) toIfaceType (ForAllTy b t) = IfaceForAllTy (toIfaceForAllBndr b) (toIfaceType t) diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs index 209eec978f..5aeeeb8e18 100644 --- a/compiler/typecheck/TcCanonical.hs +++ b/compiler/typecheck/TcCanonical.hs @@ -3,7 +3,7 @@ module TcCanonical( canonicalize, unifyDerived, - makeSuperClasses, + makeSuperClasses, maybeSym, StopOrContinue(..), stopWith, continueWith ) where diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs index d73c94f046..276a6b8201 100644 --- a/compiler/typecheck/TcErrors.hs +++ b/compiler/typecheck/TcErrors.hs @@ -2682,13 +2682,14 @@ relevantBindings want_filtering ctxt ct -- et really should be filled in by now. But there's a chance -- it hasn't, if, say, we're reporting a kind error en route to -- checking a term. See test indexed-types/should_fail/T8129 - ; ty <- case mb_ty of - Just ty -> return ty - Nothing -> do { traceTc "Defaulting an ExpType in relevantBindings" - (ppr et) - ; expTypeToType et } - ; go2 name ty top_lvl } + -- Or we are reporting errors from the ambiguity check on + -- a local type signature + ; case mb_ty of + Just ty -> go2 name ty top_lvl + Nothing -> discard_it -- No info; discard + } where + discard_it = go tidy_env ct_tvs n_left tvs_seen docs discards tc_bndrs go2 id_name id_type top_lvl = do { (tidy_env', tidy_ty) <- zonkTidyTcType tidy_env id_type ; traceTc "relevantBindings 1" (ppr id_name <+> dcolon <+> ppr tidy_ty) @@ -2702,17 +2703,19 @@ relevantBindings want_filtering ctxt ct && id_tvs `disjointVarSet` ct_tvs) -- We want to filter out this binding anyway -- so discard it silently - then go tidy_env ct_tvs n_left tvs_seen docs discards tc_bndrs + then discard_it else if isTopLevel top_lvl && not (isNothing n_left) -- It's a top-level binding and we have not specified -- -fno-max-relevant-bindings, so discard it silently - then go tidy_env ct_tvs n_left tvs_seen docs discards tc_bndrs + then discard_it else if run_out n_left && id_tvs `subVarSet` tvs_seen -- We've run out of n_left fuel and this binding only -- mentions aleady-seen type variables, so discard it - then go tidy_env ct_tvs n_left tvs_seen docs True tc_bndrs + then go tidy_env ct_tvs n_left tvs_seen docs + True -- Record that we have now discarded something + tc_bndrs -- Keep this binding, decrement fuel else go tidy_env' ct_tvs (dec_max n_left) new_seen (doc:docs) discards tc_bndrs } diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs index 4c7417fa21..39a88844b6 100644 --- a/compiler/typecheck/TcExpr.hs +++ b/compiler/typecheck/TcExpr.hs @@ -1669,6 +1669,7 @@ tcUnboundId unbound res_ty ; loc <- getCtLocM HoleOrigin Nothing ; let can = CHoleCan { cc_ev = CtWanted { ctev_pred = ty , ctev_dest = EvVarDest ev + , ctev_nosh = WDeriv , ctev_loc = loc} , cc_hole = ExprHole unbound } ; emitInsoluble can diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs index 6987191443..3adbee1808 100644 --- a/compiler/typecheck/TcFlatten.hs +++ b/compiler/typecheck/TcFlatten.hs @@ -22,6 +22,7 @@ import VarEnv import NameEnv import Outputable import TcSMonad as TcS +import BasicTypes( SwapFlag(..) ) import Util import Bag @@ -62,11 +63,16 @@ Note [The flattening story] then xis1 /= xis2 i.e. at most one CFunEqCan with a particular LHS -* Each canonical CFunEqCan x : F xis ~ fsk/fmv has its own - distinct evidence variable x and flatten-skolem fsk/fmv. +* Each canonical [G], [W], or [WD] CFunEqCan x : F xis ~ fsk/fmv + has its own distinct evidence variable x and flatten-skolem fsk/fmv. Why? We make a fresh fsk/fmv when the constraint is born; and we never rewrite the RHS of a CFunEqCan. + In contrast a [D] CFunEqCan shares its fmv with its partner [W], + but does not "own" it. If we reduce a [D] F Int ~ fmv, where + say type instance F Int = ty, then we don't discharge fmv := ty. + Rather we simply generate [D] fmv ~ ty + * Function applications can occur in the RHS of a CTyEqCan. No reason not allow this, and it reduces the amount of flattening that must occur. @@ -144,7 +150,7 @@ But since fsk = F alpha Int, this is really an occurs check error. If that is all we know about alpha, we will succeed in constraint solving, producing a program with an infinite type. -Even if we did finally get (g : fsk ~ Boo)l by solving (F alpha Int ~ fsk) +Even if we did finally get (g : fsk ~ Bool) by solving (F alpha Int ~ fsk) using axiom, zonking would not see it, so (x::alpha) sitting in the tree will get zonked to an infinite type. (Zonking always only does refl stuff.) @@ -161,8 +167,9 @@ Look at Simple13, with unification-fmvs only [W] x : F a ~ fmv --> subst a in x - x = F g' ; x2 - [W] x2 : F [fmv] ~ fmv + g' = g;[x] + x = F g' ; x2 + [W] x2 : F [fmv] ~ fmv And now we have an evidence cycle between g' and x! @@ -203,67 +210,32 @@ 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 [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 - [G] F a ~ fsk, fsk ~ a - -Now if we flatten we get - [W] alpha ~ fmv, F alpha ~ fmv, alpha ~ a - -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. +Look at Trac #10340: + type family Any :: * -- No instances + get :: MonadState s m => m s + instance MonadState s (State s) where ... -Old solution: always put fmvs on the left, so we get - [W] fmv ~ alpha, F alpha ~ fmv, alpha ~ a - -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 + 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 + [WD] MonadState ss mm, [WD] mm ss ~ State Any Any Flatten, and decompose - [W] MonadState ss mm, [W] Any ~ fmv, [W] mm ~ State fmv, [W] fmv ~ ss + [WD] MonadState ss mm, [WD] Any ~ fmv + [WD] mm ~ State fmv, [WD] 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 (in - unflatten_eq in TcFlatten.unflatten) iterate the entire process. - This is done by the 'go' loop in solveSimpleWanteds. + [WD] MonadState ss (State fmv) + [WD] Any ~ fmv, [WD] fmv ~ ss +Now we are stuck; the instance does not match!! So unflatten: + fmv := Any + ss := Any (*) + [WD] MonadState Any (State Any) + +The unification (*) represents progress, so we must do a second +round of solving; this time it succeeds. 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. @@ -271,26 +243,6 @@ iteration only happens in pretty obscure circumstances. ************************************************************************ * * -* Other notes (Oct 14) - I have not revisted these, but I didn't want to discard them -* * -************************************************************************ - - -Try: rewrite wanted with wanted only for fmvs (not all meta-tyvars) - -But: fmv ~ alpha[0] - alpha[0] ~ fmv’ -Now we don’t see that fmv ~ fmv’, which is a problem for injectivity detection. - -Conclusion: rewrite wanteds with wanted for all untouchables. - -skol ~ untch, must re-orieint to untch ~ skol, so that we can use it to rewrite. - - - -************************************************************************ -* * * Examples Here is a long series of examples I had to work through * * @@ -313,9 +265,6 @@ axiom F [a] = [F a] [G] a ~ [fsk2] [G] fsk ~ a - ------------------------------------ - ---------------------------------------- indexed-types/should_compile/T44984 @@ -510,6 +459,16 @@ data FlattenMode -- Postcondition for all three: inert wrt the type substitutio -- -- * If flat_top is True, top level is not a function application -- -- (but under type constructors is ok e.g. [F a]) +instance Outputable FlattenMode where + ppr FM_FlattenAll = text "FM_FlattenAll" + ppr FM_SubstOnly = text "FM_SubstOnly" + +eqFlattenMode :: FlattenMode -> FlattenMode -> Bool +eqFlattenMode FM_FlattenAll FM_FlattenAll = True +eqFlattenMode FM_SubstOnly FM_SubstOnly = True +-- FM_Avoid tv1 b1 `eq` FM_Avoid tv2 b2 = tv1 == tv2 && b1 == b2 +eqFlattenMode _ _ = False + mkFlattenEnv :: FlattenMode -> CtEvidence -> FlatWorkListRef -> FlattenEnv mkFlattenEnv fm ctev ref = FE { fe_mode = fm , fe_loc = ctEvLoc ctev @@ -612,14 +571,9 @@ setEqRel new_eq_rel thing_inside setMode :: FlattenMode -> FlatM a -> FlatM a setMode new_mode thing_inside = FlatM $ \env -> - if new_mode `eq` fe_mode env + if new_mode `eqFlattenMode` fe_mode env then runFlatM thing_inside env else runFlatM thing_inside (env { fe_mode = new_mode }) - where - FM_FlattenAll `eq` FM_FlattenAll = True - FM_SubstOnly `eq` FM_SubstOnly = True --- FM_Avoid tv1 b1 `eq` FM_Avoid tv2 b2 = tv1 == tv2 && b1 == b2 - _ `eq` _ = False -- | Use when flattening kinds/kind coercions. See -- Note [No derived kind equalities] in TcCanonical @@ -628,7 +582,7 @@ flattenKinds thing_inside = FlatM $ \env -> let kind_flav = case fe_flavour env of Given -> Given - _ -> Wanted + _ -> Wanted WDeriv in runFlatM thing_inside (env { fe_eq_rel = NomEq, fe_flavour = kind_flav }) @@ -637,15 +591,6 @@ bumpDepth (FlatM thing_inside) = FlatM $ \env -> do { let env' = env { fe_loc = bumpCtLocDepth (fe_loc env) } ; thing_inside env' } --- Flatten skolems --- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -newFlattenSkolemFlatM :: TcType -- F xis - -> FlatM (CtEvidence, Coercion, TcTyVar) -- [W] x:: F xis ~ fsk -newFlattenSkolemFlatM ty - = do { flavour <- getFlavour - ; loc <- getLoc - ; liftTcS $ newFlattenSkolem flavour loc ty } - {- Note [The flattening work list] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -795,6 +740,7 @@ flattenManyNom ev tys ; traceTcS "flatten }" (vcat (map ppr tys')) ; return (tys', cos) } + {- ********************************************************************* * * * The main flattening functions @@ -1113,15 +1059,14 @@ flatten_exact_fam_app tc tys = do { mode <- getMode ; role <- getRole ; case mode of - FM_FlattenAll -> flatten_exact_fam_app_fully tc tys - - FM_SubstOnly -> do { (xis, cos) <- flatten_many roles tys + -- These roles are always going to be Nominal for now, + -- but not if #8177 is implemented + FM_SubstOnly -> do { let roles = tyConRolesX role tc + ; (xis, cos) <- flatten_many roles tys ; return ( mkTyConApp tc xis , mkTyConAppCo role tc cos ) } - where - -- These are always going to be Nominal for now, - -- but not if #8177 is implemented - roles = tyConRolesX role tc } + + FM_FlattenAll -> flatten_exact_fam_app_fully tc tys } -- FM_Avoid tv flat_top -> -- do { (xis, cos) <- flatten_many fmode roles tys @@ -1134,20 +1079,22 @@ flatten_exact_fam_app_fully tc tys -- See Note [Reduce type family applications eagerly] = try_to_reduce tc tys False id $ do { -- First, flatten the arguments - ; (xis, cos) <- setEqRel NomEq $ flatten_many_nom tys - ; eq_rel <- getEqRel + ; (xis, cos) <- setEqRel NomEq $ + flatten_many_nom tys + ; eq_rel <- getEqRel + ; cur_flav <- getFlavour ; let role = eqRelRole eq_rel ret_co = mkTyConAppCo role tc cos -- ret_co :: F xis ~ F tys -- Now, look in the cache ; mb_ct <- liftTcS $ lookupFlatCache tc xis - ; fr <- getFlavourRole ; case mb_ct of Just (co, rhs_ty, flav) -- co :: F xis ~ fsk - | (flav, NomEq) `funEqCanDischargeFR` fr + -- flav is [G] or [WD] + -- See Note [Type family equations] in TcSMonad + | (NotSwapped, _) <- flav `funEqCanDischargeF` cur_flav -> -- 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) ; (fsk_xi, fsk_co) <- flatten_one rhs_ty -- The fsk may already have been unified, so flatten it @@ -1161,11 +1108,8 @@ flatten_exact_fam_app_fully tc tys -- Try to reduce the family application right now -- See Note [Reduce type family applications eagerly] _ -> try_to_reduce tc xis True (`mkTransCo` ret_co) $ - do { let fam_ty = mkTyConApp tc xis - ; (ev, co, fsk) <- newFlattenSkolemFlatM fam_ty - ; let fsk_ty = mkTyVarTy fsk - ; liftTcS $ extendFlatCache tc xis ( co - , fsk_ty, ctEvFlavour ev) + do { loc <- getLoc + ; (ev, co, fsk) <- liftTcS $ newFlattenSkolem cur_flav loc tc xis -- The new constraint (F xis ~ fsk) is not necessarily inert -- (e.g. the LHS may be a redex) so we must put it in the work list @@ -1175,12 +1119,13 @@ flatten_exact_fam_app_fully tc tys , cc_fsk = fsk } ; emitFlatWork ct - ; traceFlat "flatten/flat-cache miss" $ (ppr fam_ty $$ ppr fsk $$ ppr ev) - ; (fsk_xi, fsk_co) <- flatten_one fsk_ty - ; return (fsk_xi, fsk_co - `mkTransCo` - maybeSubCo eq_rel (mkSymCo co) - `mkTransCo` ret_co ) } + ; traceFlat "flatten/flat-cache miss" $ + (ppr tc <+> ppr xis $$ ppr fsk $$ ppr ev) + + -- NB: fsk's kind is already flattend because + -- the xis are flattened + ; return (mkTyVarTy fsk, maybeSubCo eq_rel (mkSymCo co) + `mkTransCo` ret_co ) } } where @@ -1322,31 +1267,25 @@ flatten_tyvar1 tv ; return (FTRFollowed ty (mkReflCo role ty)) } ; Nothing -> do { traceFlat "Unfilled tyvar" (ppr tv) ; fr <- getFlavourRole - ; flatten_tyvar2 tv fr } } + ; flatten_tyvar2 tv fr } } flatten_tyvar2 :: TcTyVar -> CtFlavourRole -> FlatM FlattenTvResult +-- The tyvar is not a filled-in meta-tyvar -- Try in the inert equalities -- See Definition [Applying a generalised substitution] in TcSMonad -- See Note [Stability of flattening] in TcSMonad -flatten_tyvar2 tv fr@(flavour, eq_rel) - | Derived <- flavour -- For derived equalities, consult the inert_model (only) - = do { model <- liftTcS $ getInertModel - ; case lookupDVarEnv model tv of - Just (CTyEqCan { cc_rhs = rhs }) - -> return (FTRFollowed rhs (pprPanic "flatten_tyvar2" (ppr tv $$ ppr rhs))) - -- Evidence is irrelevant for Derived contexts - _ -> return FTRNotFollowed } - - | otherwise -- For non-derived equalities, consult the inert_eqs (only) +flatten_tyvar2 tv fr@(_, eq_rel) = do { ieqs <- liftTcS $ getInertEqs + ; mode <- getMode ; case lookupDVarEnv ieqs tv of Just (ct:_) -- If the first doesn't work, -- the subsequent ones won't either | CTyEqCan { cc_ev = ctev, cc_tyvar = tv, cc_rhs = rhs_ty } <- ct - , ctEvFlavourRole ctev `eqCanRewriteFR` fr - -> do { traceFlat "Following inert tyvar" (ppr tv <+> equals <+> ppr rhs_ty $$ ppr ctev) - ; let rewrite_co1 = mkSymCo $ ctEvCoercion ctev + , let ct_fr = ctEvFlavourRole ctev + , ct_fr `eqCanRewriteFR` fr -- This is THE key call of eqCanRewriteFR + -> do { traceFlat "Following inert tyvar" (ppr mode <+> ppr tv <+> equals <+> ppr rhs_ty $$ ppr ctev) + ; let rewrite_co1 = mkSymCo (ctEvCoercion ctev) rewrite_co = case (ctEvEqRel ctev, eq_rel) of (ReprEq, _rel) -> ASSERT( _rel == ReprEq ) -- if this ASSERT fails, then @@ -1366,7 +1305,7 @@ flatten_tyvar2 tv fr@(flavour, eq_rel) Note [An alternative story for the inert substitution] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ (This entire note is just background, left here in case we ever want - to return the the previousl state of affairs) + to return the the previous state of affairs) We used (GHC 7.8) to have this story for the inert substitution inert_eqs @@ -1484,7 +1423,7 @@ unflatten tv_eqs funeqs ---------------- unflatten_funeq :: Ct -> Cts -> TcS Cts unflatten_funeq ct@(CFunEqCan { cc_fun = tc, cc_tyargs = xis - , cc_fsk = fmv, cc_ev = ev }) rest + , cc_fsk = fmv, cc_ev = ev }) 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 @@ -1492,8 +1431,7 @@ unflatten tv_eqs funeqs rhs' <- zonkTcType (mkTyConApp tc xis) ; case occCheckExpand fmv rhs' of Just rhs'' -- Normal case: fill the tyvar - -> do { setEvBindIfWanted ev - (EvCoercion (mkTcReflCo (ctEvRole ev) rhs'')) + -> do { setReflEvidence ev NomEq rhs'' ; unflattenFmv fmv rhs'' ; return rest } @@ -1512,17 +1450,22 @@ unflatten tv_eqs funeqs ---------------- unflatten_eq :: TcLevel -> Ct -> Cts -> TcS Cts - unflatten_eq tclvl ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = rhs }) rest + unflatten_eq tclvl ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv + , cc_rhs = rhs, cc_eq_rel = eq_rel }) rest | isFmvTyVar tv -- Previously these fmvs were untouchable, -- but now they are touchable - -- NB: unlike unflattenFmv, filling a fmv here does + -- 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 tv rhs ev - ; if lhs_elim then return rest else - do { rhs_elim <- try_fill tclvl ev rhs (mkTyVarTy tv) - ; if rhs_elim then return rest else - return (ct `consCts` rest) } } + , tyVarKind tv `eqType` typeKind rhs + = do { is_filled <- isFilledMetaTyVar tv + ; elim <- case is_filled of + False -> do { traceTcS "unflatten_eq 2" (ppr ct) + ; tryFill ev eq_rel tv rhs } + True -> do { traceTcS "unflatten_eq 2" (ppr ct) + ; try_fill_rhs ev eq_rel tclvl tv rhs } + ; if elim then return rest + else return (ct `consCts` rest) } | otherwise = return (ct `consCts` rest) @@ -1530,51 +1473,67 @@ unflatten tv_eqs funeqs unflatten_eq _ ct _ = pprPanic "unflatten_irred" (ppr ct) ---------------- + try_fill_rhs ev eq_rel tclvl lhs_tv rhs + -- Constraint is lhs_tv ~ rhs_tv, + -- and lhs_tv is filled, so try RHS + | Just (rhs_tv, co) <- getCastedTyVar_maybe rhs + -- co :: kind(rhs_tv) ~ kind(lhs_tv) + , isFmvTyVar rhs_tv || (isTouchableMetaTyVar tclvl rhs_tv + && not (isSigTyVar rhs_tv)) + -- LHS is a filled fmv, and so is a type + -- family application, which a SigTv should + -- not unify with + = do { is_filled <- isFilledMetaTyVar rhs_tv + ; if is_filled then return False + else tryFill ev eq_rel rhs_tv + (mkTyVarTy lhs_tv `mkCastTy` mkSymCo co) } + + | otherwise + = return False + + ---------------- finalise_eq :: Ct -> Cts -> TcS Cts finalise_eq (CTyEqCan { cc_ev = ev, cc_tyvar = tv , cc_rhs = rhs, cc_eq_rel = eq_rel }) rest | isFmvTyVar tv = do { ty1 <- zonkTcTyVar tv - ; ty2 <- zonkTcType rhs - ; let is_refl = ty1 `tcEqType` ty2 - ; if is_refl then do { setEvBindIfWanted ev - (EvCoercion $ - mkTcReflCo (eqRelRole eq_rel) rhs) - ; return rest } - else return (mkNonCanonical ev `consCts` rest) } + ; rhs' <- zonkTcType rhs + ; if ty1 `tcEqType` rhs' + then do { setReflEvidence ev eq_rel rhs' + ; return rest } + else return (mkNonCanonical ev `consCts` rest) } + | otherwise = return (mkNonCanonical ev `consCts` rest) finalise_eq ct _ = pprPanic "finalise_irred" (ppr ct) - ---------------- - try_fill tclvl ev ty1 ty2 - | Just tv1 <- tcGetTyVar_maybe ty1 - , isTouchableOrFmv tclvl tv1 - , typeKind ty1 `eqType` tyVarKind tv1 - = tryFill tv1 ty2 ev - | otherwise - = return False - -tryFill :: TcTyVar -> TcType -> CtEvidence -> TcS Bool --- (tryFill tv rhs ev) sees if 'tv' is an un-filled MetaTv --- If so, and if tv does not appear in 'rhs', set tv := rhs --- bind the evidence (which should be a CtWanted) to Refl<rhs> --- and return True. Otherwise return False -tryFill tv rhs ev +tryFill :: CtEvidence -> EqRel -> TcTyVar -> TcType -> TcS Bool +-- (tryFill tv rhs ev) assumes 'tv' is an /un-filled/ MetaTv +-- If tv does not appear in 'rhs', it set tv := rhs, +-- binds the evidence (which should be a CtWanted) to Refl<rhs> +-- and return True. Otherwise returns False +tryFill ev eq_rel tv rhs = ASSERT2( not (isGiven ev), ppr ev ) - do { is_filled <- isFilledMetaTyVar tv - ; if is_filled then return False else do { rhs' <- zonkTcType rhs - ; case occCheckExpand tv rhs' of + ; case tcGetTyVar_maybe rhs' of { + Just tv' | tv == tv' -> do { setReflEvidence ev eq_rel rhs + ; return True } ; + _other -> + do { case occCheckExpand tv rhs' of Just rhs'' -- Normal case: fill the tyvar - -> do { setEvBindIfWanted ev - (EvCoercion (mkTcReflCo (ctEvRole ev) rhs'')) + -> do { setReflEvidence ev eq_rel rhs'' ; unifyTyVar tv rhs'' ; return True } Nothing -> -- Occurs check - return False } } + return False } } } + +setReflEvidence :: CtEvidence -> EqRel -> TcType -> TcS () +setReflEvidence ev eq_rel rhs + = setEvBindIfWanted ev (EvCoercion refl_co) + where + refl_co = mkTcReflCo (eqRelRole eq_rel) rhs {- Note [Unflatten using funeqs first] diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs index 005be19f6e..cb0b44ff2b 100644 --- a/compiler/typecheck/TcInteract.hs +++ b/compiler/typecheck/TcInteract.hs @@ -9,7 +9,8 @@ module TcInteract ( #include "HsVersions.h" -import BasicTypes ( infinity, IntWithInf, intGtLimit ) +import BasicTypes ( SwapFlag(..), isSwapped, + infinity, IntWithInf, intGtLimit ) import HsTypes ( HsIPName(..) ) import TcCanonical import TcFlatten @@ -133,16 +134,14 @@ that prepareInertsForImplications will discard the insolubles, so we must keep track of them separately. -} -solveSimpleGivens :: [Ct] -> TcS Cts +solveSimpleGivens :: [Ct] -> TcS () solveSimpleGivens givens | null givens -- Shortcut for common case - = return emptyCts + = return () | otherwise = do { traceTcS "solveSimpleGivens {" (ppr givens) ; go givens - ; given_insols <- takeGivenInsolubles - ; traceTcS "End solveSimpleGivens }" (text "Insoluble:" <+> pprCts given_insols) - ; return given_insols } + ; traceTcS "End solveSimpleGivens }" empty } where go givens = do { solveSimples (listToBag givens) ; new_givens <- runTcPluginsGiven @@ -183,7 +182,8 @@ solveSimpleWanteds simples ; if unif_count == 0 && not rerun_plugin then return (n, wc2) -- Done - else do { traceTcS "solveSimple going round again:" (ppr rerun_plugin) + else do { traceTcS "solveSimple going round again:" $ + ppr unif_count $$ ppr rerun_plugin ; go (n+1) limit wc2 } } -- Loop @@ -355,11 +355,8 @@ runTcPlugins plugins all_cts without = deleteFirstsBy eqCt eqCt :: Ct -> Ct -> Bool - eqCt c c' = case (ctEvidence c, ctEvidence c') of - (CtGiven pred _ _, CtGiven pred' _ _) -> pred `eqType` pred' - (CtWanted pred _ _, CtWanted pred' _ _) -> pred `eqType` pred' - (CtDerived pred _ , CtDerived pred' _ ) -> pred `eqType` pred' - (_ , _ ) -> False + eqCt c c' = ctFlavour c == ctFlavour c' + && ctPred c `tcEqType` ctPred c' add :: [(EvTerm,Ct)] -> SolvedCts -> SolvedCts add xs scs = foldl' addOne scs xs @@ -386,19 +383,19 @@ runSolverPipeline pipeline workItem ; bumpStepCountTcS -- One step for each constraint processed ; final_res <- run_pipeline pipeline (ContinueWith workItem) - - ; final_is <- getTcSInerts ; case final_res of Stop ev s -> do { traceFireTcS ev s + ; final_is <- getTcSInerts ; traceTcS "End solver pipeline (discharged) }" (text "inerts =" <+> ppr final_is) ; return () } ContinueWith ct -> do { traceFireTcS (ctEvidence ct) (text "Kept as inert") + ; addInertCan ct + ; final_is <- getTcSInerts ; traceTcS "End solver pipeline (kept as inert) }" $ vcat [ text "final_item =" <+> ppr ct , pprTyVars $ tyCoVarsOfCtList ct - , text "inerts =" <+> ppr final_is] - ; addInertCan ct } + , text "inerts =" <+> ppr final_is] } } where run_pipeline :: [(String,SimplifierStage)] -> StopOrContinue Ct -> TcS (StopOrContinue Ct) @@ -740,6 +737,7 @@ addFunDepWork inerts work_ev cls where work_pred = ctEvPred work_ev work_loc = ctEvLoc work_ev + add_fds inert_ct = emitFunDepDeriveds $ improveFromAnother derived_loc inert_pred work_pred @@ -819,7 +817,6 @@ So the inner binding for ?x::Bool *overrides* the outer one. All this works for the normal cases but it has an odd side effect in some pathological programs like this: - -- This is accepted, the second parameter shadows f1 :: (?x :: Int, ?x :: Char) => Char f1 = ?x @@ -852,57 +849,77 @@ I can think of two ways to fix this: interactFunEq :: InertCans -> Ct -> TcS (StopOrContinue Ct) -- Try interacting the work item with the inert set -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 `funEqCanDischarge` ev - then -- Rewrite work-item using inert - do { traceTcS "reactFunEq (discharge work item):" $ - vcat [ text "workItem =" <+> ppr workItem - , text "inertItem=" <+> ppr ev_i ] - ; reactFunEq ev_i fsk_i ev fsk - ; stopWith ev "Inert rewrites work item" } - else -- Rewrite inert using work-item - 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 ] - ; updInertFunEqs $ \ feqs -> insertFunEq feqs tc args workItem - -- Do the updInertFunEqs before the reactFunEq, so that - -- we don't kick out the inertItem as well as consuming it! - ; reactFunEq ev fsk ev_i fsk_i - ; stopWith ev "Work item rewrites inert" } +interactFunEq inerts work_item@(CFunEqCan { cc_ev = ev, cc_fun = tc + , cc_tyargs = args, cc_fsk = fsk }) + | Just inert_ct@(CFunEqCan { cc_ev = ev_i + , cc_fsk = fsk_i }) + <- findFunEq (inert_funeqs inerts) tc args + , pr@(swap_flag, upgrade_flag) <- ev_i `funEqCanDischarge` ev + = do { traceTcS "reactFunEq (rewrite inert item):" $ + vcat [ text "work_item =" <+> ppr work_item + , text "inertItem=" <+> ppr ev_i + , text "(swap_flag, upgrade)" <+> ppr pr ] + ; if isSwapped swap_flag + then do { -- Rewrite inert using work-item + let work_item' | upgrade_flag = upgradeWanted work_item + | otherwise = work_item + ; updInertFunEqs $ \ feqs -> insertFunEq feqs tc args work_item' + -- Do the updInertFunEqs before the reactFunEq, so that + -- we don't kick out the inertItem as well as consuming it! + ; reactFunEq ev fsk ev_i fsk_i + ; stopWith ev "Work item rewrites inert" } + else do { -- Rewrite work-item using inert + ; when upgrade_flag $ + updInertFunEqs $ \ feqs -> insertFunEq feqs tc args + (upgradeWanted inert_ct) + ; reactFunEq ev_i fsk_i ev fsk + ; stopWith ev "Inert rewrites work item" } } | otherwise -- Try improvement - = do { improveLocalFunEqs loc inerts tc args fsk - ; continueWith workItem } - where - loc = ctEvLoc ev - funeqs = inert_funeqs inerts - matching_inerts = findFunEq funeqs tc args + = do { improveLocalFunEqs ev inerts tc args fsk + ; continueWith work_item } -interactFunEq _ workItem = pprPanic "interactFunEq" (ppr workItem) +interactFunEq _ work_item = pprPanic "interactFunEq" (ppr work_item) -improveLocalFunEqs :: CtLoc -> InertCans -> TyCon -> [TcType] -> TcTyVar +upgradeWanted :: Ct -> Ct +-- We are combining a [W] F tys ~ fmv1 and [D] F tys ~ fmv2 +-- so upgrade the [W] to [WD] before putting it in the inert set +upgradeWanted ct = ct { cc_ev = upgrade_ev (cc_ev ct) } + where + upgrade_ev ev = ASSERT2( isWanted ev, ppr ct ) + ev { ctev_nosh = WDeriv } + +improveLocalFunEqs :: CtEvidence -> InertCans -> TyCon -> [TcType] -> TcTyVar -> TcS () -- Generate derived improvement equalities, by comparing -- the current work item with inert CFunEqs -- E.g. x + y ~ z, x + y' ~ z => [D] y ~ y' -improveLocalFunEqs loc inerts fam_tc args fsk - | not (null improvement_eqns) - = do { traceTcS "interactFunEq improvements: " $ +-- +-- See Note [FunDep and implicit parameter reactions] +improveLocalFunEqs ev inerts fam_tc args fsk + | isGiven ev -- See Note [No FunEq improvement for Givens] + = return () + + | null improvement_eqns + = do { traceTcS "improveLocalFunEqs no improvements: " $ + vcat [ text "Candidates:" <+> ppr funeqs_for_tc + , text "Inert eqs:" <+> ppr ieqs ] + ; return () } + + | otherwise + = do { traceTcS "improveLocalFunEqs improvements: " $ vcat [ text "Eqns:" <+> ppr improvement_eqns , text "Candidates:" <+> ppr funeqs_for_tc - , text "Model:" <+> ppr model ] + , text "Inert eqs:" <+> ppr ieqs ] ; mapM_ (unifyDerived loc Nominal) improvement_eqns } - | otherwise - = return () + where - model = inert_model inerts + loc = ctEvLoc ev + ieqs = inert_eqs inerts funeqs = inert_funeqs inerts funeqs_for_tc = findFunEqsByTyCon funeqs fam_tc - rhs = lookupFlattenTyVar model fsk + rhs = lookupFlattenTyVar ieqs fsk + fam_inj_info = familyTyConInjectivityInfo fam_tc -------------------- improvement_eqns @@ -910,37 +927,30 @@ improveLocalFunEqs loc inerts fam_tc args fsk = -- Try built-in families, notably for arithmethic concatMap (do_one_built_in ops) funeqs_for_tc - | Injective injective_args <- familyTyConInjectivityInfo fam_tc + | Injective injective_args <- fam_inj_info = -- Try improvement from type families with injectivity annotations - concatMap (do_one_injective injective_args) funeqs_for_tc + concatMap (do_one_injective injective_args) funeqs_for_tc | otherwise = [] -------------------- do_one_built_in ops (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk }) - = sfInteractInert ops args rhs iargs (lookupFlattenTyVar model ifsk) + = sfInteractInert ops args rhs iargs (lookupFlattenTyVar ieqs 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 model ifsk - = [Pair arg iarg | (arg, iarg, True) - <- zip3 args iargs injective_args ] - | otherwise - = [] + do_one_injective inj_args (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk }) + | rhs `tcEqType` lookupFlattenTyVar ieqs ifsk + = [ Pair arg iarg + | (arg, iarg, True) <- zip3 args iargs inj_args ] + + | otherwise = [] + do_one_injective _ _ = pprPanic "interactFunEq 2" (ppr fam_tc) ------------- -lookupFlattenTyVar :: InertModel -> TcTyVar -> TcType --- See Note [lookupFlattenTyVar] -lookupFlattenTyVar model ftv - = case lookupDVarEnv model ftv of - Just (CTyEqCan { cc_rhs = rhs, cc_eq_rel = NomEq }) -> rhs - _ -> mkTyVarTy ftv - reactFunEq :: CtEvidence -> TcTyVar -- From this :: F args1 ~ fsk1 -> CtEvidence -> TcTyVar -- Solve this :: F args2 ~ fsk2 -> TcS () @@ -955,26 +965,20 @@ reactFunEq from_this fsk1 solve_this fsk2 ; new_ev <- newGivenEvVar loc (fsk_eq_pred, EvCoercion fsk_eq_co) ; emitWorkNC [new_ev] } - | otherwise + | CtDerived { ctev_loc = loc } <- solve_this + = do { traceTcS "reactFunEq (Derived)" (ppr from_this $$ ppr fsk1 $$ + ppr solve_this $$ ppr fsk2) + ; emitNewDerivedEq loc Nominal (mkTyVarTy fsk1) (mkTyVarTy fsk2) } + -- FunEqs are always at Nominal role + + | otherwise -- Wanted = do { traceTcS "reactFunEq" (ppr from_this $$ ppr fsk1 $$ ppr solve_this $$ ppr fsk2) ; dischargeFmv solve_this fsk2 (ctEvCoercion from_this) (mkTyVarTy fsk1) ; 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] +{- Note [Type inference for type families with injectivity] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose we have a type family with an injectivity annotation: type family F a b = r | r -> b @@ -1101,24 +1105,19 @@ test when solving pairwise CFunEqCan. ********************************************************************** -} -interactTyVarEq :: InertCans -> Ct -> TcS (StopOrContinue Ct) --- CTyEqCans are always consumed, so always returns Stop -interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv - , cc_rhs = rhs - , cc_ev = ev - , cc_eq_rel = eq_rel }) +inertsCanDischarge :: InertCans -> TcTyVar -> TcType -> CtEvidence + -> Maybe ( CtEvidence -- The evidence for the inert + , SwapFlag -- Whether we need mkSymCo + , Bool) -- True <=> keep a [D] version + -- of the [WD] constraint +inertsCanDischarge inerts tv rhs ev | (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i } <- findTyEqs inerts tv , ev_i `eqCanDischarge` ev , rhs_i `tcEqType` rhs ] = -- Inert: a ~ ty -- Work item: a ~ ty - do { setEvBindIfWanted ev $ - EvCoercion (tcDowngradeRole (eqRelRole eq_rel) - (ctEvRole ev_i) - (ctEvCoercion ev_i)) - - ; stopWith ev "Solved from inert" } + Just (ev_i, NotSwapped, keep_deriv ev_i) | Just tv_rhs <- getTyVar_maybe rhs , (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i } @@ -1127,13 +1126,41 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv , rhs_i `tcEqType` mkTyVarTy tv ] = -- Inert: a ~ b -- Work item: b ~ a - do { setEvBindIfWanted ev $ - EvCoercion (mkTcSymCo $ - tcDowngradeRole (eqRelRole eq_rel) - (ctEvRole ev_i) - (ctEvCoercion ev_i)) + Just (ev_i, IsSwapped, keep_deriv ev_i) + + | otherwise + = Nothing + + where + keep_deriv ev_i + | Wanted WOnly <- ctEvFlavour ev_i -- inert is [W] + , Wanted WDeriv <- ctEvFlavour ev -- work item is [WD] + = True -- Keep a derived verison of the work item + | otherwise + = False -- Work item is fully discharged + +interactTyVarEq :: InertCans -> Ct -> TcS (StopOrContinue Ct) +-- CTyEqCans are always consumed, so always returns Stop +interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv + , cc_rhs = rhs + , cc_ev = ev + , cc_eq_rel = eq_rel }) + | Just (ev_i, swapped, keep_deriv) + <- inertsCanDischarge inerts tv rhs ev + = do { setEvBindIfWanted ev $ + EvCoercion (maybeSym swapped $ + tcDowngradeRole (eqRelRole eq_rel) + (ctEvRole ev_i) + (ctEvCoercion ev_i)) + + ; let deriv_ev = CtDerived { ctev_pred = ctEvPred ev + , ctev_loc = ctEvLoc ev } + ; when keep_deriv $ + emitWork [workItem { cc_ev = deriv_ev }] + -- As a Derived it might not be fully rewritten, + -- so we emit it as new work - ; stopWith ev "Solved from inert (r)" } + ; stopWith ev "Solved from inert" } | ReprEq <- eq_rel -- We never solve representational = unsolved_inert -- equalities by unification @@ -1159,7 +1186,7 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv <+> text "is" <+> ppr (metaTyVarTcLevel tv)) , text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs) ]) ; addInertEq workItem - ; return (Stop ev (text "Kept as inert")) } + ; stopWith ev "Kept as inert" } interactTyVarEq _ wi = pprPanic "interactTyVarEq" (ppr wi) @@ -1233,9 +1260,78 @@ constraint right away. This avoids two dangers To achieve this required some refactoring of FunDeps.hs (nicer now!). + +Note [FunDep and implicit parameter reactions] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Currently, our story of interacting two dictionaries (or a dictionary +and top-level instances) for functional dependencies, and implicit +parameters, is that we simply produce new Derived equalities. So for example + + class D a b | a -> b where ... + Inert: + d1 :g D Int Bool + WorkItem: + d2 :w D Int alpha + + We generate the extra work item + cv :d alpha ~ Bool + where 'cv' is currently unused. However, this new item can perhaps be + spontaneously solved to become given and react with d2, + discharging it in favour of a new constraint d2' thus: + d2' :w D Int Bool + d2 := d2' |> D Int cv + Now d2' can be discharged from d1 + +We could be more aggressive and try to *immediately* solve the dictionary +using those extra equalities, but that requires those equalities to carry +evidence and derived do not carry evidence. + +If that were the case with the same inert set and work item we might dischard +d2 directly: + + cv :w alpha ~ Bool + d2 := d1 |> D Int cv + +But in general it's a bit painful to figure out the necessary coercion, +so we just take the first approach. Here is a better example. Consider: + class C a b c | a -> b +And: + [Given] d1 : C T Int Char + [Wanted] d2 : C T beta Int +In this case, it's *not even possible* to solve the wanted immediately. +So we should simply output the functional dependency and add this guy +[but NOT its superclasses] back in the worklist. Even worse: + [Given] d1 : C T Int beta + [Wanted] d2: C T beta Int +Then it is solvable, but its very hard to detect this on the spot. + +It's exactly the same with implicit parameters, except that the +"aggressive" approach would be much easier to implement. + +Note [Weird fundeps] +~~~~~~~~~~~~~~~~~~~~ +Consider class Het a b | a -> b where + het :: m (f c) -> a -> m b + + class GHet (a :: * -> *) (b :: * -> *) | a -> b + instance GHet (K a) (K [a]) + instance Het a b => GHet (K a) (K b) + +The two instances don't actually conflict on their fundeps, +although it's pretty strange. So they are both accepted. Now +try [W] GHet (K Int) (K Bool) +This triggers fundeps from both instance decls; + [D] K Bool ~ K [a] + [D] K Bool ~ K beta +And there's a risk of complaining about Bool ~ [a]. But in fact +the Wanted matches the second instance, so we never get as far +as the fundeps. + +Trac #7875 is a case in point. -} emitFunDepDeriveds :: [FunDepEqn CtLoc] -> TcS () +-- See Note [FunDep and implicit parameter reactions] emitFunDepDeriveds fd_eqns = mapM_ do_one_FDEqn fd_eqns where @@ -1282,121 +1378,45 @@ doTopReact work_item _ -> -- Any other work item does not react with any top-level equations continueWith work_item } --------------------- -doTopReactDict :: InertSet -> Ct -> TcS (StopOrContinue Ct) --- Try to use type-class instance declarations to simplify the constraint -doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls - , cc_tyargs = xis }) - | isGiven fl -- Never use instances for Given constraints - = do { try_fundep_improvement - ; continueWith work_item } - - | Just ev <- lookupSolvedDict inerts cls xis -- Cached - = do { setEvBindIfWanted fl (ctEvTerm ev) - ; stopWith fl "Dict/Top (cached)" } - - | isDerived fl -- Use type-class instances for Deriveds, in the hope - -- of generating some improvements - -- C.f. Example 3 of Note [The improvement story] - -- It's easy because no evidence is involved - = do { dflags <- getDynFlags - ; lkup_inst_res <- matchClassInst dflags inerts cls xis dict_loc - ; case lkup_inst_res of - GenInst { lir_new_theta = preds - , lir_safe_over = s } -> - do { emitNewDeriveds dict_loc preds - ; unless s $ insertSafeOverlapFailureTcS work_item - ; stopWith fl "Dict/Top (solved)" } - - NoInstance -> - do { -- If there is no instance, try improvement - try_fundep_improvement - ; continueWith work_item } } - - | otherwise -- Wanted, but not cached - = do { dflags <- getDynFlags - ; lkup_inst_res <- matchClassInst dflags inerts cls xis dict_loc - ; case lkup_inst_res of - GenInst { lir_new_theta = theta - , lir_mk_ev = mk_ev - , lir_safe_over = s } -> - do { addSolvedDict fl cls xis - ; unless s $ insertSafeOverlapFailureTcS work_item - ; solve_from_instance theta mk_ev } - NoInstance -> - do { try_fundep_improvement - ; continueWith work_item } } - where - dict_pred = mkClassPred cls xis - dict_loc = ctEvLoc fl - dict_origin = ctLocOrigin dict_loc - deeper_loc = zap_origin (bumpCtLocDepth dict_loc) - - zap_origin loc -- After applying an instance we can set ScOrigin to - -- infinity, so that prohibitedSuperClassSolve never fires - | ScOrigin {} <- dict_origin - = setCtLocOrigin loc (ScOrigin infinity) - | otherwise - = loc - - solve_from_instance :: [TcPredType] - -> ([EvTerm] -> EvTerm) -> TcS (StopOrContinue Ct) - -- Precondition: evidence term matches the predicate workItem - solve_from_instance theta mk_ev - | null theta - = do { traceTcS "doTopReact/found nullary instance for" $ ppr fl - ; setWantedEvBind (ctEvId fl) (mk_ev []) - ; stopWith fl "Dict/Top (solved, no new work)" } - | otherwise - = do { checkReductionDepth deeper_loc dict_pred - ; traceTcS "doTopReact/found non-nullary instance for" $ ppr fl - ; evc_vars <- mapM (newWanted deeper_loc) theta - ; setWantedEvBind (ctEvId fl) (mk_ev (map getEvTerm evc_vars)) - ; emitWorkNC (freshGoals evc_vars) - ; stopWith fl "Dict/Top (solved, more work)" } - - -- We didn't solve it; so try functional dependencies with - -- the instance environment, and return - -- See also Note [Weird fundeps] - try_fundep_improvement - = do { traceTcS "try_fundeps" (ppr work_item) - ; instEnvs <- getInstEnvs - ; emitFunDepDeriveds $ - improveFromInstEnv instEnvs mk_ct_loc dict_pred } - - mk_ct_loc :: PredType -- From instance decl - -> SrcSpan -- also from instance deol - -> CtLoc - mk_ct_loc inst_pred inst_loc - = dict_loc { ctl_origin = FunDepOrigin2 dict_pred dict_origin - inst_pred inst_loc } - -doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w) -------------------- doTopReactFunEq :: Ct -> TcS (StopOrContinue Ct) doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc , cc_tyargs = args, cc_fsk = fsk }) + + | fsk `elemVarSet` tyCoVarsOfTypes args + = no_reduction -- See Note [FunEq occurs-check principle] + + | otherwise -- Note [Reduction for Derived CFunEqCans] = do { match_res <- matchFam fam_tc args -- Look up in top-level instances, or built-in axiom -- See Note [MATCHING-SYNONYMS] ; case match_res of - Nothing -> do { improveTopFunEqs (ctEvLoc old_ev) fam_tc args fsk - ; continueWith work_item } - Just (ax_co, rhs_ty) - -> reduce_top_fun_eq old_ev fsk ax_co rhs_ty } + Nothing -> no_reduction + Just match_info -> reduce_top_fun_eq old_ev fsk match_info } + where + no_reduction + = do { improveTopFunEqs old_ev fam_tc args fsk + ; continueWith work_item } doTopReactFunEq w = pprPanic "doTopReactFunEq" (ppr w) -reduce_top_fun_eq :: CtEvidence -> TcTyVar -> TcCoercion -> TcType +reduce_top_fun_eq :: CtEvidence -> TcTyVar -> (TcCoercion, TcType) -> TcS (StopOrContinue Ct) --- Found an applicable top-level axiom: use it to reduce -reduce_top_fun_eq old_ev fsk ax_co rhs_ty +-- We have found an applicable top-level axiom: use it to reduce +-- Precondition: fsk is not free in rhs_ty +-- old_ev is not Derived +reduce_top_fun_eq old_ev fsk (ax_co, rhs_ty) + | isDerived old_ev + = do { emitNewDerivedEq loc Nominal (mkTyVarTy fsk) rhs_ty + ; stopWith old_ev "Fun/Top (derived)" } + | Just (tc, tc_args) <- tcSplitTyConApp_maybe rhs_ty , isTypeFamilyTyCon tc , tc_args `lengthIs` tyConArity tc -- Short-cut - = shortCutReduction old_ev fsk ax_co tc tc_args - -- Try shortcut; see Note [Short cut for top-level reaction] + = -- RHS is another type-family application + -- Try shortcut; see Note [Top-level reductions for type functions] + shortCutReduction old_ev fsk ax_co tc tc_args | isGiven old_ev -- Not shortcut = do { let final_co = mkTcSymCo (ctEvCoercion old_ev) `mkTcTransCo` ax_co @@ -1406,50 +1426,36 @@ reduce_top_fun_eq old_ev fsk ax_co rhs_ty ; emitWorkNC [new_ev] -- Non-cannonical; that will mean we flatten rhs_ty ; stopWith old_ev "Fun/Top (given)" } - -- So old_ev is Wanted or Derived - | not (fsk `elemVarSet` tyCoVarsOfType rhs_ty) - = do { dischargeFmv old_ev fsk ax_co rhs_ty + | otherwise -- So old_ev is Wanted (cannot be Derived) + = ASSERT2( not (fsk `elemVarSet` tyCoVarsOfType rhs_ty) + , ppr old_ev $$ ppr rhs_ty ) + -- Guaranteed by Note [FunEq occurs-check principle] + do { dischargeFmv old_ev fsk ax_co rhs_ty ; traceTcS "doTopReactFunEq" $ vcat [ text "old_ev:" <+> ppr old_ev , nest 2 (text ":=") <+> ppr ax_co ] ; stopWith old_ev "Fun/Top (wanted)" } - | otherwise -- We must not assign ufsk := ...ufsk...! - = do { alpha_ty <- newFlexiTcSTy (tyVarKind fsk) - ; new_co <- case old_ev of - CtWanted {} -> emitNewWantedEq loc Nominal alpha_ty rhs_ty - CtDerived {} -> do { ev <- newDerivedNC loc pred - ; updWorkListTcS (extendWorkListDerived loc ev) - ; return (ctEvCoercion ev) } -- Coercion is bottom - where pred = mkPrimEqPred alpha_ty rhs_ty - _ -> pprPanic "reduce_top_fun_eq" (ppr old_ev) - - -- By emitting this as non-canonical, we deal with all - -- flattening, occurs-check, and ufsk := ufsk issues - ; let final_co = ax_co `mkTcTransCo` mkTcSymCo new_co - -- ax_co :: fam_tc args ~ rhs_ty - -- ev :: alpha ~ rhs_ty - -- ufsk := alpha - -- final_co :: fam_tc args ~ alpha - ; dischargeFmv old_ev fsk final_co alpha_ty - ; traceTcS "doTopReactFunEq (occurs)" $ - vcat [ text "old_ev:" <+> ppr old_ev - , nest 2 (text ":=") <+> - if isDerived old_ev then text "(derived)" - else ppr final_co - , text "new_co:" <+> ppr new_co ] - ; stopWith old_ev "Fun/Top (wanted)" } where loc = ctEvLoc old_ev deeper_loc = bumpCtLocDepth loc -improveTopFunEqs :: CtLoc -> TyCon -> [TcType] -> TcTyVar -> TcS () -improveTopFunEqs loc fam_tc args fsk - = do { model <- getInertModel +improveTopFunEqs :: CtEvidence -> TyCon -> [TcType] -> TcTyVar -> TcS () +-- See Note [FunDep and implicit parameter reactions] +improveTopFunEqs ev fam_tc args fsk + | isGiven ev -- See Note [No FunEq improvement for Givens] + = return () + + | otherwise + = do { ieqs <- getInertEqs ; fam_envs <- getFamInstEnvs ; eqns <- improve_top_fun_eqs fam_envs fam_tc args - (lookupFlattenTyVar model fsk) + (lookupFlattenTyVar ieqs fsk) + ; traceTcS "improveTopFunEqs" (vcat [ ppr fam_tc <+> ppr args <+> ppr fsk + , ppr eqns ]) ; mapM_ (unifyDerived loc Nominal) eqns } + where + loc = ctEvLoc ev improve_top_fun_eqs :: FamInstEnvs -> TyCon -> [TcType] -> TcType @@ -1475,7 +1481,8 @@ improve_top_fun_eqs fam_envs fam_tc args rhs_ty | otherwise = return [] - where + + where buildImprovementData :: [a] -- axioms for a TF (FamInst or CoAxBranch) -> (a -> [Type]) -- get LHS of an axiom @@ -1535,11 +1542,7 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args `mkTcTransCo` mkTcSymCo ax_co `mkTcTransCo` ctEvCoercion old_ev) ) - Derived -> newDerivedNC deeper_loc $ - mkPrimEqPred (mkTyConApp fam_tc xis) - (mkTyVarTy fsk) - - Wanted -> + Wanted {} -> do { (new_ev, new_co) <- newWantedEq deeper_loc Nominal (mkTyConApp fam_tc xis) (mkTyVarTy fsk) ; setWantedEq (ctev_dest old_ev) $ @@ -1548,6 +1551,8 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args `mkTcTransCo` new_co ; return new_ev } + Derived -> pprPanic "shortCutReduction" (ppr old_ev) + ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc , cc_tyargs = xis, cc_fsk = fsk } ; updWorkListTcS (extendWorkListFunEq new_ct) @@ -1559,19 +1564,21 @@ dischargeFmv :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS () -- (dischargeFmv x fmv co ty) -- [W] ev :: F tys ~ fmv -- co :: F tys ~ xi --- Precondition: fmv is not filled, and fuv `notElem` xi +-- Precondition: fmv is not filled, and fmv `notElem` xi +-- ev is Wanted -- -- Then set fmv := xi, --- set ev := co +-- set ev := co -- kick out any inert things that are now rewritable -- -- Does not evaluate 'co' if 'ev' is Derived -dischargeFmv ev fmv co xi +dischargeFmv ev@(CtWanted { ctev_dest = dest }) fmv co xi = ASSERT2( not (fmv `elemVarSet` tyCoVarsOfType xi), ppr ev $$ ppr fmv $$ ppr xi ) - do { setEvBindIfWanted ev (EvCoercion co) + do { setWantedEvTerm dest (EvCoercion co) ; unflattenFmv fmv xi ; n_kicked <- kickOutAfterUnification fmv ; traceTcS "dischargeFmv" (ppr fmv <+> equals <+> ppr xi $$ ppr_kicked n_kicked) } +dischargeFmv ev _ _ _ = pprPanic "dischargeFmv" (ppr ev) {- Note [Top-level reductions for type functions] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1585,15 +1592,14 @@ Here is what we do, in four cases: instantiate axiom: ax_co : F tys ~ rhs Then: - Discharge fmv := alpha + Discharge fmv := rhs Discharge x := ax_co ; sym x2 - New wanted [W] x2 : alpha ~ rhs (Non-canonical) This is *the* way that fmv's get unified; even though they are "untouchable". - NB: it can be the case that fmv appears in the (instantiated) rhs. - In that case the new Non-canonical wanted will be loopy, but that's - ok. But it's good reason NOT to claim that it is canonical! + NB: Given Note [FunEq occurs-check principle], fmv does not appear + in tys, and hence does not appear in the instantiated RHS. So + the unification can't make an infinite type. * Wanteds: short cut firing rule Applies when the RHS of the axiom is another type-function application @@ -1625,6 +1631,36 @@ Here is what we do, in four cases: - Add new Canonical given [G] (sym (G flat_cos) ; co ; g) : G flat_tys ~ fsk (CFunEqCan) +Note [FunEq occurs-check principle] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +I have spent a lot of time finding a good way to deal with +CFunEqCan constraints like + F (fuv, a) ~ fuv +where flatten-skolem occurs on the LHS. Now in principle we +might may progress by doing a reduction, but in practice its +hard to find examples where it is useful, and easy to find examples +where we fall into an infinite reduction loop. A rule that works +very well is this: + + *** FunEq occurs-check principle *** + + Do not reduce a CFunEqCan + F tys ~ fsk + if fsk appears free in tys + Instead we treat it as stuck. + +Examples: + +* Trac #5837 has [G] a ~ TF (a,Int), with an instance + type instance TF (a,b) = (TF a, TF b) + This readily loops when solving givens. But with the FunEq occurs + check principle, it rapidly gets stuck which is fine. + +* Trac #12444 is a good example, explained in comment:2. We have + type instance F (Succ x) = Succ (F x) + [W] alpha ~ Succ (F alpha) + If we allow the reduction to happen, we get an infinite loop + Note [Cached solved FunEqs] ~~~~~~~~~~~~~~~~~~~~~~~~~~~ When trying to solve, say (FunExpensive big-type ~ ty), it's important @@ -1639,87 +1675,6 @@ When trying to match a dictionary (D tau) to a top-level instance, or a type family equation (F taus_1 ~ tau_2) to a top-level family instance, we do *not* need to expand type synonyms because the matcher will do that for us. - -Note [RHS-FAMILY-SYNONYMS] -~~~~~~~~~~~~~~~~~~~~~~~~~~ -The RHS of a family instance is represented as yet another constructor which is -like a type synonym for the real RHS the programmer declared. Eg: - type instance F (a,a) = [a] -Becomes: - :R32 a = [a] -- internal type synonym introduced - F (a,a) ~ :R32 a -- instance - -When we react a family instance with a type family equation in the work list -we keep the synonym-using RHS without expansion. - -Note [FunDep and implicit parameter reactions] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Currently, our story of interacting two dictionaries (or a dictionary -and top-level instances) for functional dependencies, and implicit -parameters, is that we simply produce new Derived equalities. So for example - - class D a b | a -> b where ... - Inert: - d1 :g D Int Bool - WorkItem: - d2 :w D Int alpha - - We generate the extra work item - cv :d alpha ~ Bool - where 'cv' is currently unused. However, this new item can perhaps be - spontaneously solved to become given and react with d2, - discharging it in favour of a new constraint d2' thus: - d2' :w D Int Bool - d2 := d2' |> D Int cv - Now d2' can be discharged from d1 - -We could be more aggressive and try to *immediately* solve the dictionary -using those extra equalities, but that requires those equalities to carry -evidence and derived do not carry evidence. - -If that were the case with the same inert set and work item we might dischard -d2 directly: - - cv :w alpha ~ Bool - d2 := d1 |> D Int cv - -But in general it's a bit painful to figure out the necessary coercion, -so we just take the first approach. Here is a better example. Consider: - class C a b c | a -> b -And: - [Given] d1 : C T Int Char - [Wanted] d2 : C T beta Int -In this case, it's *not even possible* to solve the wanted immediately. -So we should simply output the functional dependency and add this guy -[but NOT its superclasses] back in the worklist. Even worse: - [Given] d1 : C T Int beta - [Wanted] d2: C T beta Int -Then it is solvable, but its very hard to detect this on the spot. - -It's exactly the same with implicit parameters, except that the -"aggressive" approach would be much easier to implement. - -Note [Weird fundeps] -~~~~~~~~~~~~~~~~~~~~ -Consider class Het a b | a -> b where - het :: m (f c) -> a -> m b - - class GHet (a :: * -> *) (b :: * -> *) | a -> b - instance GHet (K a) (K [a]) - instance Het a b => GHet (K a) (K b) - -The two instances don't actually conflict on their fundeps, -although it's pretty strange. So they are both accepted. Now -try [W] GHet (K Int) (K Bool) -This triggers fundeps from both instance decls; - [D] K Bool ~ K [a] - [D] K Bool ~ K beta -And there's a risk of complaining about Bool ~ [a]. But in fact -the Wanted matches the second instance, so we never get as far -as the fundeps. - -Trac #7875 is a case in point. - Note [Improvement orientation] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ A very delicate point is the orientation of derived equalities @@ -1756,10 +1711,170 @@ template. But that's a bit tricky, esp when we remember that the kinds much match too; so it's easier to let the normal machinery handle it. Instead we are careful to orient the new derived equality with the template on the left. Delicate, but it works. + +Note [No FunEq improvement for Givens] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We don't do improvements (injectivity etc) for Givens. Why? + +* It generates Derived constraints on skolems, which don't do us + much good, except perhaps identify inaccessible branches. + (They'd be perfectly valid though.) + +* For type-nat stuff the derived constraints include type families; + e.g. (a < b), (b < c) ==> a < c If we generate a Derived for this, + we'll generate a Derived/Wanted CFunEqCan; and, since the same + InertCans (after solving Givens) are used for each iteration, that + massively confused the unflattening step (TcFlatten.unflatten). + + In fact it led to some infinite loops: + indexed-types/should_compile/T10806 + indexed-types/should_compile/T10507 + polykinds/T10742 + +Note [Reduction for Derived CFunEqCans] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +You may wonder if it's important to use top-level instances to +simplify [D] CFunEqCan's. But it is. Here's an example (T10226). + + type instance F Int = Int + type instance FInv Int = Int + +Suppose we have to solve + [WD] FInv (F alpha) ~ alpha + [WD] F alpha ~ Int + + --> flatten + [WD] F alpha ~ fuv0 + [WD] FInv fuv0 ~ fuv1 -- (A) + [WD] fuv1 ~ alpha + [WD] fuv0 ~ Int -- (B) + + --> Rewwrite (A) with (B), splitting it + [WD] F alpha ~ fuv0 + [W] FInv fuv0 ~ fuv1 + [D] FInv Int ~ fuv1 -- (C) + [WD] fuv1 ~ alpha + [WD] fuv0 ~ Int + + --> Reduce (C) with top-level instance + **** This is the key step *** + [WD] F alpha ~ fuv0 + [W] FInv fuv0 ~ fuv1 + [D] fuv1 ~ Int -- (D) + [WD] fuv1 ~ alpha -- (E) + [WD] fuv0 ~ Int + + --> Rewrite (D) with (E) + [WD] F alpha ~ fuv0 + [W] FInv fuv0 ~ fuv1 + [D] alpha ~ Int -- (F) + [WD] fuv1 ~ alpha + [WD] fuv0 ~ Int + + --> unify (F) alpha := Int, and that solves it + +Another example is indexed-types/should_compile/T10634 -} {- ******************************************************************* * * + Top-level reaction for class constraints (CDictCan) +* * +**********************************************************************-} + +doTopReactDict :: InertSet -> Ct -> TcS (StopOrContinue Ct) +-- Try to use type-class instance declarations to simplify the constraint +doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls + , cc_tyargs = xis }) + | isGiven fl + = do { try_fundep_improvement + ; continueWith work_item } + + | Just ev <- lookupSolvedDict inerts cls xis -- Cached + = do { setEvBindIfWanted fl (ctEvTerm ev) + ; stopWith fl "Dict/Top (cached)" } + + | isDerived fl -- Use type-class instances for Deriveds, in the hope + -- of generating some improvements + -- C.f. Example 3 of Note [The improvement story] + -- It's easy because no evidence is involved + = do { dflags <- getDynFlags + ; lkup_inst_res <- matchClassInst dflags inerts cls xis dict_loc + ; case lkup_inst_res of + GenInst { lir_new_theta = preds + , lir_safe_over = s } -> + do { emitNewDeriveds dict_loc preds + ; unless s $ insertSafeOverlapFailureTcS work_item + ; stopWith fl "Dict/Top (solved)" } + + NoInstance -> + do { -- If there is no instance, try improvement + try_fundep_improvement + ; continueWith work_item } } + + | otherwise -- Wanted, but not cached + = do { dflags <- getDynFlags + ; lkup_inst_res <- matchClassInst dflags inerts cls xis dict_loc + ; case lkup_inst_res of + GenInst { lir_new_theta = theta + , lir_mk_ev = mk_ev + , lir_safe_over = s } -> + do { addSolvedDict fl cls xis + ; unless s $ insertSafeOverlapFailureTcS work_item + ; solve_from_instance theta mk_ev } + NoInstance -> + do { try_fundep_improvement + ; continueWith work_item } } + where + dict_pred = mkClassPred cls xis + dict_loc = ctEvLoc fl + dict_origin = ctLocOrigin dict_loc + deeper_loc = zap_origin (bumpCtLocDepth dict_loc) + + zap_origin loc -- After applying an instance we can set ScOrigin to + -- infinity, so that prohibitedSuperClassSolve never fires + | ScOrigin {} <- dict_origin + = setCtLocOrigin loc (ScOrigin infinity) + | otherwise + = loc + + solve_from_instance :: [TcPredType] + -> ([EvTerm] -> EvTerm) -> TcS (StopOrContinue Ct) + -- Precondition: evidence term matches the predicate workItem + solve_from_instance theta mk_ev + | null theta + = do { traceTcS "doTopReact/found nullary instance for" $ ppr fl + ; setWantedEvBind (ctEvId fl) (mk_ev []) + ; stopWith fl "Dict/Top (solved, no new work)" } + | otherwise + = do { checkReductionDepth deeper_loc dict_pred + ; traceTcS "doTopReact/found non-nullary instance for" $ ppr fl + ; evc_vars <- mapM (newWanted deeper_loc) theta + ; setWantedEvBind (ctEvId fl) (mk_ev (map getEvTerm evc_vars)) + ; emitWorkNC (freshGoals evc_vars) + ; stopWith fl "Dict/Top (solved, more work)" } + + -- We didn't solve it; so try functional dependencies with + -- the instance environment, and return + -- See also Note [Weird fundeps] + try_fundep_improvement + = do { traceTcS "try_fundeps" (ppr work_item) + ; instEnvs <- getInstEnvs + ; emitFunDepDeriveds $ + improveFromInstEnv instEnvs mk_ct_loc dict_pred } + + mk_ct_loc :: PredType -- From instance decl + -> SrcSpan -- also from instance deol + -> CtLoc + mk_ct_loc inst_pred inst_loc + = dict_loc { ctl_origin = FunDepOrigin2 dict_pred dict_origin + inst_pred inst_loc } + +doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w) + + +{- ******************************************************************* +* * Class lookup * * **********************************************************************-} diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs index ff0ee9ea49..c200b4efb8 100644 --- a/compiler/typecheck/TcMType.hs +++ b/compiler/typecheck/TcMType.hs @@ -43,7 +43,7 @@ module TcMType ( -------------------------------- -- Creating new evidence variables newEvVar, newEvVars, newDict, - newWanted, newWanteds, + newWanted, newWanteds, cloneWanted, cloneWC, emitWanted, emitWantedEq, emitWantedEvVar, emitWantedEvVars, newTcEvBinds, addTcEvBind, @@ -170,11 +170,30 @@ newWanted orig t_or_k pty else EvVarDest <$> newEvVar pty return $ CtWanted { ctev_dest = d , ctev_pred = pty + , ctev_nosh = WDeriv , ctev_loc = loc } newWanteds :: CtOrigin -> ThetaType -> TcM [CtEvidence] newWanteds orig = mapM (newWanted orig Nothing) +cloneWanted :: Ct -> TcM CtEvidence +cloneWanted ct + = newWanted (ctEvOrigin ev) Nothing (ctEvPred ev) + where + ev = ctEvidence ct + +cloneWC :: WantedConstraints -> TcM WantedConstraints +cloneWC wc@(WC { wc_simple = simples, wc_impl = implics }) + = do { simples' <- mapBagM clone_one simples + ; implics' <- mapBagM clone_implic implics + ; return (wc { wc_simple = simples', wc_impl = implics' }) } + where + clone_one ct = do { ev <- cloneWanted ct; return (mkNonCanonical ev) } + + clone_implic implic@(Implic { ic_wanted = inner_wanted }) + = do { inner_wanted' <- cloneWC inner_wanted + ; return (implic { ic_wanted = inner_wanted' }) } + -- | Emits a new Wanted. Deals with both equalities and non-equalities. emitWanted :: CtOrigin -> TcPredType -> TcM EvTerm emitWanted origin pty @@ -188,7 +207,8 @@ emitWantedEq origin t_or_k role ty1 ty2 = do { hole <- newCoercionHole ; loc <- getCtLocM origin (Just t_or_k) ; emitSimple $ mkNonCanonical $ - CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole, ctev_loc = loc } + CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole + , ctev_nosh = WDeriv, ctev_loc = loc } ; return (mkHoleCo hole role ty1 ty2) } where pty = mkPrimEqPredRole role ty1 ty2 @@ -201,6 +221,7 @@ emitWantedEvVar origin ty ; loc <- getCtLocM origin Nothing ; let ctev = CtWanted { ctev_dest = EvVarDest new_cv , ctev_pred = ty + , ctev_nosh = WDeriv , ctev_loc = loc } ; emitSimple $ mkNonCanonical ctev ; return new_cv } diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs index ce541c3f54..fd6d74cfe1 100644 --- a/compiler/typecheck/TcRnTypes.hs +++ b/compiler/typecheck/TcRnTypes.hs @@ -78,10 +78,8 @@ module TcRnTypes( ctEvTerm, ctEvCoercion, ctEvId, tyCoVarsOfCt, tyCoVarsOfCts, tyCoVarsOfCtList, tyCoVarsOfCtsList, - toDerivedCt, WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC, - toDerivedWC, andWC, unionsWC, mkSimpleWC, mkImplicWC, addInsols, getInsolubles, addSimples, addImplics, tyCoVarsOfWC, dropDerivedWC, dropDerivedSimples, dropDerivedInsols, @@ -107,7 +105,7 @@ module TcRnTypes( CtEvidence(..), TcEvDest(..), mkGivenLoc, mkKindLoc, toKindLoc, - isWanted, isGiven, isDerived, + isWanted, isGiven, isDerived, isGivenOrWDeriv, ctEvRole, -- Constraint solver plugins @@ -115,10 +113,11 @@ module TcRnTypes( TcPluginM, runTcPluginM, unsafeTcPluginTcM, getEvBindsTcPluginM, - CtFlavour(..), ctEvFlavour, + CtFlavour(..), ShadowInfo(..), ctEvFlavour, CtFlavourRole, ctEvFlavourRole, ctFlavourRole, - eqCanRewrite, eqCanRewriteFR, eqCanDischarge, - funEqCanDischarge, funEqCanDischargeFR, + eqCanRewriteFR, eqMayRewriteFR, + eqCanDischarge, + funEqCanDischarge, funEqCanDischargeF, -- Pretty printing pprEvVarTheta, @@ -174,6 +173,7 @@ import ListSetOps import FastString import qualified GHC.LanguageExtensions as LangExt import Fingerprint +import Util import Control.Monad (ap, liftM, msum) #if __GLASGOW_HASKELL__ > 710 @@ -1509,7 +1509,8 @@ data Ct cc_tyvar :: TcTyVar, cc_rhs :: TcType, -- Not necessarily function-free (hence not Xi) -- See invariants above - cc_eq_rel :: EqRel + + cc_eq_rel :: EqRel -- INVARIANT: cc_eq_rel = ctEvEqRel cc_ev } | CFunEqCan { -- F xis ~ fsk @@ -1625,16 +1626,6 @@ ctPred :: Ct -> PredType -- See Note [Ct/evidence invariant] ctPred ct = ctEvPred (cc_ev ct) --- | Convert a Wanted to a Derived -toDerivedCt :: Ct -> Ct -toDerivedCt ct - = case ctEvidence ct of - CtWanted { ctev_pred = pred, ctev_loc = loc } - -> ct {cc_ev = CtDerived {ctev_pred = pred, ctev_loc = loc}} - - CtDerived {} -> ct - CtGiven {} -> pprPanic "to_derived" (ppr ct) - -- | Makes a new equality predicate with the same role as the given -- evidence. mkTcEqPredLikeEv :: CtEvidence -> TcType -> TcType -> TcType @@ -2074,16 +2065,6 @@ andWC (WC { wc_simple = f1, wc_impl = i1, wc_insol = n1 }) unionsWC :: [WantedConstraints] -> WantedConstraints unionsWC = foldr andWC emptyWC --- | Convert all Wanteds into Deriveds (ignoring insolubles) -toDerivedWC :: WantedConstraints -> WantedConstraints -toDerivedWC wc@(WC { wc_simple = simples, wc_impl = implics }) - = wc { wc_simple = mapBag toDerivedCt simples - , wc_impl = mapBag to_derived_implic implics } - where - to_derived_implic implic@(Implic { ic_wanted = inner_wanted }) - = implic { ic_wanted = toDerivedWC inner_wanted } - - addSimples :: WantedConstraints -> Bag Ct -> WantedConstraints addSimples wc cts = wc { wc_simple = wc_simple wc `unionBags` cts } @@ -2113,21 +2094,23 @@ isInsolubleStatus _ = False insolubleImplic :: Implication -> Bool insolubleImplic ic = isInsolubleStatus (ic_status ic) -insolubleWC :: TcLevel -> WantedConstraints -> Bool -insolubleWC tc_lvl (WC { wc_impl = implics, wc_insol = insols }) - = anyBag (trulyInsoluble tc_lvl) insols +insolubleWC :: WantedConstraints -> Bool +insolubleWC (WC { wc_impl = implics, wc_insol = insols }) + = anyBag trulyInsoluble insols || anyBag insolubleImplic implics -trulyInsoluble :: TcLevel -> Ct -> Bool +trulyInsoluble :: Ct -> Bool -- Constraints in the wc_insol set which ARE NOT -- treated as truly insoluble: -- a) type holes, arising from PartialTypeSignatures, -- b) "true" expression holes arising from TypedHoles -- --- Out-of-scope variables masquerading as expression holes --- ARE treated as truly insoluble. +-- A "expression hole" or "type hole" constraint isn't really an error +-- at all; it's a report saying "_ :: Int" here. But an out-of-scope +-- variable masquerading as expression holes IS treated as truly +-- insoluble, so that it trumps other errors during error reporting. -- Yuk! -trulyInsoluble _tc_lvl insol +trulyInsoluble insol | isHoleCt insol = isOutOfScopeCt insol | otherwise = True @@ -2342,22 +2325,25 @@ data TcEvDest -- See Note [Coercion holes] in TyCoRep data CtEvidence - = CtGiven { ctev_pred :: TcPredType -- See Note [Ct/evidence invariant] - , ctev_evar :: EvVar -- See Note [Evidence field of CtEvidence] - , ctev_loc :: CtLoc } - -- Truly given, not depending on subgoals - -- NB: Spontaneous unifications belong here - - | CtWanted { ctev_pred :: TcPredType -- See Note [Ct/evidence invariant] - , ctev_dest :: TcEvDest - , ctev_loc :: CtLoc } - -- Wanted goal - - | CtDerived { ctev_pred :: TcPredType - , ctev_loc :: CtLoc } - -- A goal that we don't really have to solve and can't immediately - -- rewrite anything other than a derived (there's no evidence!) - -- but if we do manage to solve it may help in solving other goals. + = CtGiven -- Truly given, not depending on subgoals + -- NB: Spontaneous unifications belong here + { ctev_pred :: TcPredType -- See Note [Ct/evidence invariant] + , ctev_evar :: EvVar -- See Note [Evidence field of CtEvidence] + , ctev_loc :: CtLoc } + + + | CtWanted -- Wanted goal + { ctev_pred :: TcPredType -- See Note [Ct/evidence invariant] + , ctev_dest :: TcEvDest + , ctev_nosh :: ShadowInfo -- See Note [Constraint flavours] + , ctev_loc :: CtLoc } + + | CtDerived -- A goal that we don't really have to solve and can't + -- immediately rewrite anything other than a derived + -- (there's no evidence!) but if we do manage to solve + -- it may help in solving other goals. + { ctev_pred :: TcPredType + , ctev_loc :: CtLoc } ctEvPred :: CtEvidence -> TcPredType -- The predicate of a flavor @@ -2399,11 +2385,12 @@ instance Outputable TcEvDest where ppr (EvVarDest ev) = ppr ev instance Outputable CtEvidence where - ppr fl = case fl of - CtGiven {} -> text "[G]" <+> ppr (ctev_evar fl) <+> ppr_pty - CtWanted {} -> text "[W]" <+> ppr (ctev_dest fl) <+> ppr_pty - CtDerived {} -> text "[D]" <+> text "_" <+> ppr_pty - where ppr_pty = dcolon <+> ppr (ctEvPred fl) + ppr ev = ppr (ctEvFlavour ev) <+> pp_ev <+> dcolon <+> ppr (ctEvPred ev) + where + pp_ev = case ev of + CtGiven { ctev_evar = v } -> ppr v + CtWanted {ctev_dest = d } -> ppr d + CtDerived {} -> text "_" isWanted :: CtEvidence -> Bool isWanted (CtWanted {}) = True @@ -2424,23 +2411,62 @@ isDerived _ = False %* * %************************************************************************ -Just an enum type that tracks whether a constraint is wanted, derived, -or given, when we need to separate that info from the constraint itself. +Note [Constraint flavours] +~~~~~~~~~~~~~~~~~~~~~~~~~~ +Constraints come in four flavours: + +* [G] Given: we have evidence + +* [W] Wanted WOnly: we want evidence + +* [D] Derived: any solution must satisfy this constraint, but + we don't need evidence for it. Examples include: + - superclasses of [W] class constraints + - equalities arising from functional dependencies + or injectivity +* [WD] Wanted WDeriv: a single constraint that represents + both [W] and [D] + We keep them paired as one both for efficiency, and because + when we have a finite map F tys -> CFunEqCan, it's inconvenient + to have two CFunEqCans in the range + +The ctev_nosh field of a Wanted distinguishes between [W] and [WD] + +Wanted constraints are born as [WD], but are split into [W] and its +"shadow" [D] in TcSMonad.maybeEmitShadow. + +See Note [The improvement story and derived shadows] in TcSMonad -} -data CtFlavour = Given | Wanted | Derived +data CtFlavour -- See Note [Constraint flavours] + = Given + | Wanted ShadowInfo + | Derived deriving Eq +data ShadowInfo + = WDeriv -- [WD] This Wanted constraint has no Derived shadow, + -- so it behaves like a pair of a Wanted and a Derived + | WOnly -- [W] It has a separate derived shadow + -- See Note [Derived shadows] + deriving( Eq ) + +isGivenOrWDeriv :: CtFlavour -> Bool +isGivenOrWDeriv Given = True +isGivenOrWDeriv (Wanted WDeriv) = True +isGivenOrWDeriv _ = False + instance Outputable CtFlavour where - ppr Given = text "[G]" - ppr Wanted = text "[W]" - ppr Derived = text "[D]" + ppr Given = text "[G]" + ppr (Wanted WDeriv) = text "[WD]" + ppr (Wanted WOnly) = text "[W]" + ppr Derived = text "[D]" ctEvFlavour :: CtEvidence -> CtFlavour -ctEvFlavour (CtWanted {}) = Wanted -ctEvFlavour (CtGiven {}) = Given -ctEvFlavour (CtDerived {}) = Derived +ctEvFlavour (CtWanted { ctev_nosh = nosh }) = Wanted nosh +ctEvFlavour (CtGiven {}) = Given +ctEvFlavour (CtDerived {}) = Derived -- | Whether or not one 'Ct' can rewrite another is determined by its -- flavour and its equality relation. See also @@ -2456,7 +2482,7 @@ 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] in @@ -2498,9 +2524,31 @@ 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 [funEqCanDischarge] -~~~~~~~~~~~~~~~~~~~~~~~~~ +eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool +-- Can fr1 actually rewrite fr2? +-- 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 (Wanted WDeriv, NomEq) (Derived, NomEq) = True +eqCanRewriteFR (Derived, NomEq) (Derived, NomEq) = True +eqCanRewriteFR _ _ = False + +eqMayRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool +-- Is it /possible/ that fr1 can rewrite fr2? +-- This is used when deciding which inerts to kick out, +-- at which time a [WD] inert may be split into [W] and [D] +eqMayRewriteFR (Wanted WDeriv, NomEq) (Wanted WDeriv, NomEq) = True +eqMayRewriteFR (Derived, NomEq) (Wanted WDeriv, NomEq) = True +eqMayRewriteFR fr1 fr2 = eqCanRewriteFR fr1 fr2 + +----------------- +{- 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 @@ -2508,12 +2556,37 @@ 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 +funEqCanDischarge + :: CtEvidence -> CtEvidence + -> ( SwapFlag -- NotSwapped => lhs can discharge rhs + -- Swapped => rhs can discharge lhs + , Bool) -- True <=> upgrade non-discharded one + -- from [W] to [WD] +-- See Note [funEqCanDischarge] +funEqCanDischarge ev1 ev2 + = ASSERT2( ctEvEqRel ev1 == NomEq, ppr ev1 ) + ASSERT2( ctEvEqRel ev2 == NomEq, ppr ev2 ) + -- CFunEqCans are all Nominal, hence asserts + funEqCanDischargeF (ctEvFlavour ev1) (ctEvFlavour ev2) + +funEqCanDischargeF :: CtFlavour -> CtFlavour -> (SwapFlag, Bool) +funEqCanDischargeF Given _ = (NotSwapped, False) +funEqCanDischargeF _ Given = (IsSwapped, False) +funEqCanDischargeF (Wanted WDeriv) _ = (NotSwapped, False) +funEqCanDischargeF _ (Wanted WDeriv) = (IsSwapped, True) +funEqCanDischargeF (Wanted WOnly) (Wanted WOnly) = (NotSwapped, False) +funEqCanDischargeF (Wanted WOnly) Derived = (NotSwapped, True) +funEqCanDischargeF Derived (Wanted WOnly) = (IsSwapped, True) +funEqCanDischargeF Derived Derived = (NotSwapped, False) + + +{- Note [eqCanDischarge] +~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we have two identical CTyEqCan equality constraints (i.e. both LHS and RHS are the same) - (x1:s~t) `eqCanDischarge` (xs:s~t) + (x1:a~t) `eqCanDischarge` (xs:a~t) Can we just drop x2 in favour of x1? Answer: yes if eqCanDischarge is true. @@ -2525,48 +2598,27 @@ 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 --- Very important function! --- See Note [eqCanRewrite] --- See Note [Wanteds do not rewrite Wanteds] --- See Note [Deriveds do rewrite Deriveds] -eqCanRewrite ev1 ev2 = eqCanRewriteFR (ctEvFlavourRole ev1) - (ctEvFlavourRole ev2) +We /do/ say that a [W] can discharge a [WD]. In evidence terms it +certainly can, and the /caller/ arranges that the otherwise-lost [D] +is spat out as a new Derived. -} -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) - -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 +eqCanDischargeFR (_, ReprEq) (_, NomEq) = False +eqCanDischargeFR (f1,_) (f2, _) = eqCanDischargeF f1 f2 + +eqCanDischargeF :: CtFlavour -> CtFlavour -> Bool +eqCanDischargeF Given _ = True +eqCanDischargeF (Wanted _) (Wanted _) = True +eqCanDischargeF (Wanted WDeriv) Derived = True +eqCanDischargeF Derived Derived = True +eqCanDischargeF _ _ = False + {- ************************************************************************ diff --git a/compiler/typecheck/TcRules.hs b/compiler/typecheck/TcRules.hs index 4cfccb6bf0..2983ccb612 100644 --- a/compiler/typecheck/TcRules.hs +++ b/compiler/typecheck/TcRules.hs @@ -287,16 +287,14 @@ EvVar for the coercion, fill the hole with the invented EvVar, and then quantify over the EvVar. Not too tricky -- just some impedence matching, really. -Note [Simplify *derived* constraints] +Note [Simplify cloned constraints] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ At this stage, we're simplifying constraints only for insolubility and for unification. Note that all the evidence is quickly discarded. -We make this explicit by working over derived constraints, for which -there is no evidence. Using derived constraints also prevents solved -equalities from being written to coercion holes. If we don't do this, +We use a clone of the real constraint. If we don't do this, then RHS coercion-hole constraints get filled in, only to get filled in *again* when solving the implications emitted from tcRule. That's -terrible, so we avoid the problem by using derived constraints. +terrible, so we avoid the problem by cloning the constraints. -} @@ -310,15 +308,16 @@ simplifyRule :: RuleName simplifyRule name lhs_wanted rhs_wanted = do { -- We allow ourselves to unify environment -- variables: runTcS runs with topTcLevel - ; tc_lvl <- getTcLevel + ; lhs_clone <- cloneWC lhs_wanted + ; rhs_clone <- cloneWC rhs_wanted ; insoluble <- runTcSDeriveds $ do { -- First solve the LHS and *then* solve the RHS -- See Note [Solve order for RULES] - -- See Note [Simplify *derived* constraints] - lhs_resid <- solveWanteds $ toDerivedWC lhs_wanted - ; rhs_resid <- solveWanteds $ toDerivedWC rhs_wanted - ; return ( insolubleWC tc_lvl lhs_resid || - insolubleWC tc_lvl rhs_resid ) } + -- See Note [Simplify cloned constraints] + lhs_resid <- solveWanteds lhs_clone + ; rhs_resid <- solveWanteds rhs_clone + ; return ( insolubleWC lhs_resid || + insolubleWC rhs_resid ) } ; zonked_lhs_simples <- zonkSimples (wc_simple lhs_wanted) diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs index 0d20122553..dd9a82ba03 100644 --- a/compiler/typecheck/TcSMonad.hs +++ b/compiler/typecheck/TcSMonad.hs @@ -49,8 +49,9 @@ module TcSMonad ( InertSet(..), InertCans(..), updInertTcS, updInertCans, updInertDicts, updInertIrreds, getNoGivenEqs, setInertCans, - getInertEqs, getInertCans, getInertModel, getInertGivens, - emptyInert, getTcSInerts, setTcSInerts, takeGivenInsolubles, + getInertEqs, getInertCans, getInertGivens, + getInertInsols, + emptyInert, getTcSInerts, setTcSInerts, matchableGivens, prohibitedSuperClassSolve, getUnsolvedInerts, removeInertCts, getPendingScDicts, @@ -58,7 +59,7 @@ module TcSMonad ( emitInsoluble, emitWorkNC, emitWork, -- The Model - InertModel, kickOutAfterUnification, + kickOutAfterUnification, -- Inert Safe Haskell safe-overlap failures addInertSafehask, insertSafeOverlapFailureTcS, updInertSafehask, @@ -70,6 +71,7 @@ module TcSMonad ( -- Inert CTyEqCans EqualCtList, findTyEqs, foldTyEqs, isInInertEqs, + lookupFlattenTyVar, lookupInertTyVar, -- Inert solved dictionaries addSolvedDict, lookupSolvedDict, @@ -81,7 +83,7 @@ module TcSMonad ( lookupFlatCache, extendFlatCache, newFlattenSkolem, -- Flatten skolems -- Inert CFunEqCans - updInertFunEqs, findFunEq, sizeFunEqMap, + updInertFunEqs, findFunEq, findFunEqsByTyCon, instDFunType, -- Instantiation @@ -341,8 +343,7 @@ selectNextWorkItem ; try (selectWorkItem wl) $ do { ics <- getInertCans - ; solve_deriveds <- keepSolvingDeriveds - ; if inert_count ics == 0 && not solve_deriveds + ; if inert_count ics == 0 then return Nothing else try (selectDerivedWorkItem wl) (return Nothing) } } @@ -375,13 +376,14 @@ instance Outputable WorkList where data InertSet = IS { inert_cans :: InertCans - -- Canonical Given, Wanted, Derived (no Solved) + -- Canonical Given, Wanted, Derived -- Sometimes called "the inert set" , inert_flat_cache :: ExactFunEqMap (TcCoercion, TcType, CtFlavour) -- See Note [Type family equations] - -- If F tys :-> (co, ty, ev), - -- then co :: F tys ~ ty + -- If F tys :-> (co, rhs, flav), + -- then co :: F tys ~ rhs + -- flav is [G] or [WD] -- -- Just a hash-cons cache for use when flattening only -- These include entirely un-processed goals, so don't use @@ -410,8 +412,7 @@ emptyInert , inert_safehask = emptyDicts , inert_funeqs = emptyFunEqs , inert_irreds = emptyCts - , inert_insols = emptyCts - , inert_model = emptyDVarEnv } + , inert_insols = emptyCts } , inert_flat_cache = emptyExactFunEqs , inert_solved_dicts = emptyDictMap } @@ -584,26 +585,23 @@ Result ********************************************************************* -} data InertCans -- See Note [Detailed InertCans Invariants] for more - = IC { inert_model :: InertModel - -- See Note [inert_model: the inert model] - - , inert_eqs :: DTyVarEnv EqualCtList + = IC { inert_eqs :: InertEqs -- See Note [inert_eqs: the inert equalities] - -- All Given/Wanted CTyEqCans; index is the LHS tyvar + -- All CTyEqCans; index is the LHS tyvar + -- Domain = skolems and untouchables; a touchable would be unified , 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 + -- wrt inert_eqs + -- Can include all flavours, [G], [W], [WD], [D] + -- See Note [Type family equations] , inert_dicts :: DictMap Ct -- Dictionaries only -- All fully rewritten (modulo flavour constraints) - -- wrt inert_eqs/inert_model + -- wrt inert_eqs , inert_safehask :: DictMap Ct -- Failed dictionary resolution due to Safe Haskell overlapping @@ -627,15 +625,11 @@ data InertCans -- See Note [Detailed InertCans Invariants] for more -- When non-zero, keep trying to solved } -type InertModel = DTyVarEnv 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 - +type InertEqs = DTyVarEnv EqualCtList +type EqualCtList = [Ct] -- See Note [EqualCtList invariants] {- Note [Detailed InertCans Invariants] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The InertCans represents a collection of constraints with the following properties: * All canonical @@ -657,69 +651,58 @@ The InertCans represents a collection of constraints with the following properti * CTyEqCan equalities: see Note [Applying the inert substitution] in TcFlatten +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 + * Derived before Wanted + +From the fourth invariant it follows that the list is + - A single [G], or + - Zero or one [D] or [WD], followd by any number of [W] + +The Wanteds can't rewrite anything which is why we put them last + Note [Type family equations] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Type-family equations, of form (ev : F tys ~ ty), live in three places +Type-family equations, CFunEqCans, of form (ev : F tys ~ ty), +live in three places * The work-list, of course + * The inert_funeqs are un-solved but fully processed, and in + the InertCans. They can be [G], [W], [WD], or [D]. + * 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. + sharing. Everthing in the inert_flat_cache is [G] or [WD] + + 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. +The CFunEqCan Ownership Invariant: -Note [inert_model: the inert model] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -* Part of the inert set is the “model” + * Each [G/W/WD] CFunEqCan has a distinct fsk or fmv + It "owns" that fsk/fmv, in the sense that: + - reducing a [W/WD] CFunEqCan fills in the fmv + - unflattening a [W/WD] CFunEqCan fills in the fmv + (in both cases unless an occurs-check would result) - * 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. + * In contrast a [D] CFunEqCan does not "own" its fmv: + - reducing a [D] CFunEqCan does not fill in the fmv; + it just generates an equality + - unflattening ignores [D] CFunEqCans altogether - * 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. - - - A Derived "shadow copy" for every Wanted (a ~N ty) in - inert_eqs. (Originally included every Given too; but - see Note [Add derived shadows only for Wanteds]) - - * The model is not subject to "kicking-out". Reason: we make a Derived - shadow copy of any Wanted (a ~ ty), and that Derived copy will - be fully rewritten by the model before it is added - - * 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. - A touchable unification variable would have been unified first. - - * The inert_eqs are all Given/Wanted. The Derived ones are in the - inert_model only. - - * However inert_dicts, inert_funeqs, inert_irreds - may well contain derived constraints. 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 @@ -937,26 +920,6 @@ 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 [inert_eqs: the inert equalities] @@ -979,126 +942,10 @@ 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 substitution 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] in TcFlatten - [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 (IC { inert_model = model, inert_eqs = eqs + ppr (IC { inert_eqs = eqs , inert_funeqs = funeqs, inert_dicts = dicts , inert_safehask = safehask, inert_irreds = irreds , inert_insols = insols, inert_count = count }) @@ -1116,218 +963,160 @@ instance Outputable InertCans where text "Irreds =" <+> pprCts irreds , ppUnless (isEmptyCts insols) $ text "Insolubles =" <+> pprCts insols - , ppUnless (isEmptyDVarEnv model) $ - text "Model =" <+> pprCts (foldDVarEnv consCts emptyCts model) , text "Unsolved goals =" <+> int count ] {- ********************************************************************* * * - Adding an inert + Shadow constraints and improvement * * ************************************************************************ -Note [Adding an inert canonical constraint the InertCans] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -* Adding any constraint c *other* than a CTyEqCan (TcSMonad.addInertCan): - - * If c can be rewritten by model, emit the shadow constraint [D] c - as NonCanonical. See Note [Emitting shadow constraints] - - * 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). - - (A) Always (G/W/D) kick out constraints that can be rewritten - (respecting flavours) by the new constraint. This is done - by kickOutRewritable. - - (B) Applies only to nominal equalities: a ~ ty. Four cases: - - [Representational] [G/W/D] a ~R ty: - Just add it to inert_eqs - - [Derived Nominal] [D] a ~N ty: - 1. Add (a~ty) to the model - NB: 'a' cannot be in fv(ty), because the constraint is canonical. - - 2. (DShadow) Do emitDerivedShadows - For every inert [W] constraint c, st - (a) (a~ty) can rewrite c (see Note [Emitting shadow constraints]), - 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 - See Note [Add derived shadows only for Wanteds] - - [Given/Wanted Nominal] [G/W] a ~N ty: - 1. Add it to inert_eqs - 2. For [W], Emit [D] a~ty - Step (2) is needed to allow the current model to fully - rewrite [D] a~ty before adding it using the [Derived Nominal] - steps above. - See Note [Add derived shadows only for Wanteds] - -* 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 [Emitting shadow constraints] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - * Given a new model element [D] a ~ ty, we want to emit shadow - [D] constraints for any inert constraints 'c' that can be - rewritten [D] a-> ty +Note [The improvement story and derived shadows] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Because Wanteds cannot rewrite Wanteds (see Note [Wanteds do not +rewrite Wanteds] in TcRnTypes), we may miss some opportunities for +solving. Here's a classic example (indexed-types/should_fail/T4093a) - * And similarly given a new Given/Wanted 'c', we want to emit a - shadow 'c' if the model can rewrite [D] c + Ambiguity check for f: (Foo e ~ Maybe e) => Foo e -See modelCanRewrite. + We get [G] Foo e ~ Maybe e + [W] Foo e ~ Foo ee -- ee is a unification variable + [W] Foo ee ~ Maybe ee -NB the use of rewritableTyVars. You might wonder whether, given the new -constraint [D] fmv ~ ty and the inert [W] F alpha ~ fmv, do we want to -emit a shadow constraint [D] F alpha ~ fmv? No, we don't, because -it'll literally be a duplicate (since we do not rewrite the RHS of a -CFunEqCan) and hence immediately eliminated again. Insetad we simply -want to *kick-out* the [W] F alpha ~ fmv, so that it is reconsidered -from a fudep point of view. See Note [Kicking out CFunEqCan for -fundeps] + Flatten: [G] Foo e ~ fsk + [G] fsk ~ Maybe e -- (A) -Note [Kicking out CFunEqCan for fundeps] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider: - New: [D] fmv1 ~ fmv2 - Inert: [W] F alpha ~ fmv1 - [W] F beta ~ fmv2 + [W] Foo ee ~ fmv + [W] fmv ~ fsk -- (B) From Foo e ~ Foo ee + [W] fmv ~ Maybe ee -The new (derived) equality certainly can't rewrite the inerts. But we -*must* kick out the first one, to get: + --> rewrite (B) with (A) + [W] Foo ee ~ fmv + [W] fmv ~ Maybe e + [W] fmv ~ Maybe ee - New: [W] F alpha ~ fmv1 - Inert: [W] F beta ~ fmv2 - Model: [D] fmv1 ~ fmv2 + But now we appear to be stuck, since we don't rewrite Wanteds with + Wanteds. This is silly because we can see that ee := e is the + only solution. -and now improvement will discover [D] alpha ~ beta. This is important; -eg in Trac #9587. --} +The basic plan is + * generate Derived constraints that shadow Wanted constraints + * allow Derived to rewrite Derived + * in order to cause some unifications to take place + * that in turn solve the original Wanteds -addInertEq :: Ct -> TcS () --- This is a key function, because of the kick-out stuff --- Precondition: item /is/ canonical -addInertEq ct@(CTyEqCan { cc_tyvar = tv }) - = do { traceTcS "addInertEq {" $ - text "Adding new inert equality:" <+> ppr ct - ; ics <- getInertCans +The ONLY reason for all these Derived equalities is to tell us how to +unify a variable: that is, what Mark Jones calls "improvement". - ; let (kicked_out, ics1) = kickOutRewritable (ctFlavourRole ct) tv ics - ; ics2 <- add_inert_eq ics1 ct +The same idea is sometimes also called "saturation"; find all the +equalities that must hold in any solution. - ; setInertCans ics2 +Or, equivalently, you can think of the derived shadows as implementing +the "model": an non-idempotent but no-occurs-check substitution, +reflecting *all* *Nominal* equalities (a ~N ty) that are not +immediately soluble by unification. - ; unless (isEmptyWorkList kicked_out) $ - do { updWorkListTcS (appendWorkList kicked_out) - ; csTraceTcS $ - hang (text "Kick out, tv =" <+> ppr tv) - 2 (vcat [ text "n-kicked =" <+> int (workListSize kicked_out) - , ppr kicked_out ]) } +More specifically, here's how it works (Oct 16): - ; 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 - , cc_rhs = _rhs }) - | ReprEq <- eq_rel - = return new_ics - - | isDerived ev - = do { emitDerivedShadows ics tv - ; return (ics { inert_model = extendDVarEnv old_model tv ct }) } - - | otherwise -- Given/Wanted Nominal equality [W] tv ~N ty - = do { emitNewDerived loc pred - ; return new_ics } - where - loc = ctEvLoc ev - pred = ctEvPred ev - new_ics = ics { inert_eqs = addTyEq old_eqs tv ct - , inert_count = bumpUnsolvedCount ev n } - -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 - | null shadows - = return () - | otherwise - = do { traceTcS "Emit derived shadows:" $ - vcat [ text "tyvar =" <+> ppr new_tv - , text "shadows =" <+> vcat (map ppr shadows) ] - ; emitWork shadows } - where - 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 = mkShadowCt ct : cts - | otherwise = cts - - want_shadow ct - = isWantedCt ct -- See Note [Add shadows only for Wanteds] - && (new_tv `elemVarSet` rw_tvs) -- New tv can rewrite ct, yielding a - -- different ct - && 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 } +* Wanted constraints are born as [WD]; this behaves like a + [W] and a [D] paired together. -{- Note [Add derived shadows only for Wanteds] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We now only add shadows for Wanted constraints. Why add derived -shadows for Givens? After all, Givens can rewrite Deriveds. But -Deriveds can't rewrite Givens. So in principle, if we created a -Derived shadow of a Given, it could be rewritten by other Deriveds, -and that could, conceivably, lead to a useful unification. +* When we are about to add a [WD] to the inert set, if it can + be rewritten by a [D] a ~ ty, then we split it into [W] and [D], + putting the latter into the work list (see maybeEmitShadow). + +In the example above, we get to the point where we are stuck: + [WD] Foo ee ~ fmv + [WD] fmv ~ Maybe e + [WD] fmv ~ Maybe ee + +But now when [WD] fmv ~ Maybe ee is about to be added, we'll +split it into [W] and [D], since the inert [WD] fmv ~ Maybe e +can rewrite it. Then: + work item: [D] fmv ~ Maybe ee + inert: [W] fmv ~ Maybe ee + [WD] fmv ~ Maybe e -- (C) + [WD] Foo ee ~ fmv + +Now the work item is rewritten by (C) and we soon get ee := e. + +Additional notes: + + * The derived shadow equalities live in inert_eqs, along with + the Givens and Wanteds; see Note [EqualCtList invariants]. + + * We make Derived shadows only for Wanteds, not Givens. So we + have only [G], not [GD] and [G] plus splitting. See + Note [Add derived shadows only for Wanteds] + + * We also get Derived equalities from functional dependencies + and type-function injectivity; see calls to unifyDerived. + + * This splitting business applies to CFunEqCans too; and then + we do apply type-function reductions to the [D] CFunEqCan. + See Note [Reduction for Derived CFunEqCans] + + * It's worth having [WD] rather than just [W] and [D] because + * efficiency: silly to process the same thing twice + * inert_funeqs, inert_dicts is a finite map keyed by + the type; it's inconvenient for it to map to TWO constraints + +Note [Examples of how Derived shadows helps completeness] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Trac #10009, a very 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 + [WD] UnF (F beta) ~ beta + [WD] 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 + + [WD] w1: F beta ~ fmv1 + [WD] w2: UnF fmv1 ~ fmv2 + [WD] w3: fmv2 ~ beta + [WD] w4: fmv1 ~ fsk1 -- From F a ~ F beta using flat-cache + -- and re-orient to put meta-var on left + +Rewrite w2 with w4: [D] d1: UnF fsk1 ~ fmv2 +React that with g2: [D] d2: fmv2 ~ fsk2 +React that with w3: [D] beta ~ fsk2 + and g3: [D] beta ~ a -- Hooray beta := a +And that is enough to solve everything + +Note [Add derived shadows only for Wanteds] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We only add shadows for Wanted constraints. That is, we have +[WD] but not [GD]; and maybeEmitShaodw looks only at [WD] +constraints. + +It does just possibly make sense ot add a derived shadow for a +Given. If we created a Derived shadow of a Given, it could be +rewritten by other Deriveds, and that could, conceivably, lead to a +useful unification. But (a) I have been unable to come up with an example of this -happening and (b) see Trac #12660 for how adding the derived shadows -of a Given led to an infinite loop. For (b) there may be other -ways to solve the loop, but simply reraining from adding -derived shadows of Givens is particularly simple. And it's more -efficient too! + happening + (b) see Trac #12660 for how adding the derived shadows + of a Given led to an infinite loop. + (c) It's unlikely that rewriting derived Givens will lead + to a unification becuse Givens don't mention touchable + unification variables + +For (b) there may be other ways to solve the loop, but simply +reraining from adding derived shadows of Givens is particularly +simple. And it's more efficient too! Still, here's one possible reason for adding derived shadows for Givens. Consider - work-item [G] a ~ [b], model has [D] b ~ a. + work-item [G] a ~ [b], inerts has [D] b ~ a. If we added the derived shadow (into the work list) [D] a ~ [b] When we process it, we'll rewrite to a ~ [a] and get an @@ -1358,36 +1147,178 @@ 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 -modelCanRewrite model tvs = not (disjointUdfmUfm model tvs) - -- The low-level use of disjointUFM might e surprising. - -- InertModel = TyVarEnv Ct, and we want to see if its domain - -- is disjoint from that of a TcTyCoVarSet. So we drop down - -- to the underlying UniqFM. A bit yukky, but efficient. +maybeEmitShadow :: InertCans -> Ct -> TcS Ct +-- See Note [The improvement story and derived shadows] +maybeEmitShadow ics ct + | let ev = ctEvidence ct + , CtWanted { ctev_pred = pred, ctev_loc = loc + , ctev_nosh = WDeriv } <- ev + , shouldSplitWD (inert_eqs ics) ct + = do { traceTcS "Emit derived shadow" (ppr ct) + ; let derived_ev = CtDerived { ctev_pred = pred + , ctev_loc = loc } + shadow_ct = ct { cc_ev = derived_ev } + -- Te shadow constraint keeps the canonical shape. + -- This just saves work, but is sometimes important; + -- see Note [Keep CDictCan shadows as CDictCan] + ; emitWork [shadow_ct] + + ; let ev' = ev { ctev_nosh = WOnly } + ct' = ct { cc_ev = ev' } + -- Record that it now has a shadow + -- This is /the/ place we set the flag to WOnly + ; return ct' } + + | otherwise + = return ct + +shouldSplitWD :: InertEqs -> Ct -> Bool +-- Precondition: 'ct' is [WD], and is inert +-- True <=> we should split ct ito [W] and [D] because +-- the inert_eqs can make progress on the [D] + +shouldSplitWD inert_eqs (CFunEqCan { cc_tyargs = tys }) + = inert_eqs `intersects_with` rewritableTyVarsOfTypes tys + -- We don't need to split if the tv is the RHS fsk + +shouldSplitWD inert_eqs ct + = inert_eqs `intersects_with` rewritableTyVarsOfType (ctPred ct) + -- Otherwise split if the tv is mentioned at all + +intersects_with :: InertEqs -> TcTyVarSet -> Bool +intersects_with inert_eqs free_vars + = not (disjointUdfmUfm inert_eqs free_vars) + -- Test whether the inert equalities could rewrite + -- a derived version of this constraint + -- The low-level use of disjointUFM might seem surprising. + -- InertEqs = TyVarEnv EqualCtList, and we want to see if its domain + -- is disjoint from that of a TcTyCoVarSet. So we drop down + -- to the underlying UniqFM. A bit yukky, but efficient. + + +{- ********************************************************************* +* * + Inert equalities +* * +********************************************************************* -} + +addTyEq :: InertEqs -> TcTyVar -> Ct -> InertEqs +addTyEq old_eqs tv ct + = extendDVarEnv_C add_eq old_eqs tv [ct] + where + add_eq old_eqs _ + | isWantedCt ct + , (eq1 : eqs) <- old_eqs + = eq1 : ct : eqs + | otherwise + = ct : old_eqs + +foldTyEqs :: (Ct -> b -> b) -> InertEqs -> b -> b +foldTyEqs k eqs z + = foldDVarEnv (\cts z -> foldr k z cts) z eqs + +findTyEqs :: InertCans -> TyVar -> EqualCtList +findTyEqs icans tv = lookupDVarEnv (inert_eqs icans) tv `orElse` [] + +delTyEq :: InertEqs -> TcTyVar -> TcType -> InertEqs +delTyEq m tv t = modifyDVarEnv (filter (not . isThisOne)) m tv + where isThisOne (CTyEqCan { cc_rhs = t1 }) = eqType t t1 + isThisOne _ = False + +lookupInertTyVar :: InertEqs -> TcTyVar -> Maybe TcType +lookupInertTyVar ieqs tv + = case lookupDVarEnv ieqs tv of + Just (CTyEqCan { cc_rhs = rhs, cc_eq_rel = NomEq } : _ ) -> Just rhs + _ -> Nothing + +lookupFlattenTyVar :: InertEqs -> TcTyVar -> TcType +-- See Note [lookupFlattenTyVar] +lookupFlattenTyVar ieqs ftv + = lookupInertTyVar ieqs ftv `orElse` mkTyVarTy ftv + +{- Note [lookupFlattenTyVar] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Supppose we have an injective function F and + inert_funeqs: F t1 ~ fsk1 + F t2 ~ fsk2 + inert_eqs: 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 inert_eqs when trying to find derived +equalities arising from injectivity. +-} + -rewritableTyCoVars :: Ct -> TcTyVarSet --- The tyvars of a Ct that can be rewritten -rewritableTyCoVars (CFunEqCan { cc_tyargs = tys }) = tyCoVarsOfTypes tys -rewritableTyCoVars ct = tyCoVarsOfType (ctPred ct) +{- ********************************************************************* +* * + Adding an inert +* * +************************************************************************ + +Note [Adding an equality to the InertCans] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When adding an equality to the inerts: + +* Split [WD] into [W] and [D] if the inerts can rewrite the latter; + done by maybeEmitShadow. + +* Kick out any constraints that can be rewritten by the thing + we are adding. Done by kickOutRewritable. + +* Note that unifying a:=ty, is like adding [G] a~ty; just use + kickOutRewritable with Nominal, Given. See kickOutAfterUnification. + +Note [Kicking out CFunEqCan for fundeps] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider: + New: [D] fmv1 ~ fmv2 + Inert: [W] F alpha ~ fmv1 + [W] F beta ~ fmv2 + +where F is injective. The new (derived) equality certainly can't +rewrite the inerts. But we *must* kick out the first one, to get: + + New: [W] F alpha ~ fmv1 + Inert: [W] F beta ~ fmv2 + [D] fmv1 ~ fmv2 + +and now improvement will discover [D] alpha ~ beta. This is important; +eg in Trac #9587. + +So in kickOutRewritable we look at all the tyvars of the +CFunEqCan, including the fsk. +-} + +addInertEq :: Ct -> TcS () +-- This is a key function, because of the kick-out stuff +-- Precondition: item /is/ canonical +-- See Note [Adding an equality to the InertCans] +addInertEq ct + = do { traceTcS "addInertEq {" $ + text "Adding new inert equality:" <+> ppr ct + ; ics <- getInertCans + + ; ct@(CTyEqCan { cc_tyvar = tv, cc_ev = ev }) <- maybeEmitShadow ics ct + + ; (_, ics1) <- kickOutRewritable (ctEvFlavourRole ev) tv ics + + ; let ics2 = ics1 { inert_eqs = addTyEq (inert_eqs ics1) tv ct + , inert_count = bumpUnsolvedCount ev (inert_count ics1) } + ; setInertCans ics2 + + ; traceTcS "addInertEq }" $ empty } -------------- addInertCan :: Ct -> TcS () -- Constraints *other than* equalities addInertCan ct = do { traceTcS "insertInertCan {" $ - text "Trying to insert new inert item:" <+> ppr ct + text "Trying to insert new non-eq inert item:" <+> ppr ct ; ics <- getInertCans + ; ct <- maybeEmitShadow ics ct ; setInertCans (add_item ics ct) - -- Emit shadow derived if necessary - -- See Note [Emitting shadow constraints] - ; let rw_tvs = rewritableTyCoVars ct - ; when (isWantedCt ct && modelCanRewrite (inert_model ics) rw_tvs) - -- See Note [Add shadows only for Wanteds] - (emitWork [mkShadowCt ct]) - ; traceTcS "addInertCan }" $ empty } add_item :: InertCans -> Ct -> InertCans @@ -1419,21 +1350,39 @@ bumpUnsolvedCount ev n | isWanted ev = n+1 ----------------------------------------- -kickOutRewritable :: CtFlavourRole -- Flavour/role of the equality that - -- is being added to the inert set - -> TcTyVar -- The new equality is tv ~ ty - -> InertCans - -> (WorkList, InertCans) +kickOutRewritable :: CtFlavourRole -- Flavour/role of the equality that + -- is being added to the inert set + -> TcTyVar -- The new equality is tv ~ ty + -> InertCans + -> TcS (Int, InertCans) +kickOutRewritable new_fr new_tv ics + = do { let (kicked_out, ics') = kick_out_rewritable new_fr new_tv ics + n_kicked = workListSize kicked_out + + ; unless (n_kicked == 0) $ + do { updWorkListTcS (appendWorkList kicked_out) + ; csTraceTcS $ + hang (text "Kick out, tv =" <+> ppr new_tv) + 2 (vcat [ text "n-kicked =" <+> int n_kicked + , text "kicked_out =" <+> ppr kicked_out + , text "Residual inerts =" <+> ppr ics' ]) } + + ; return (n_kicked, ics') } + +kick_out_rewritable :: CtFlavourRole -- Flavour/role of the equality that + -- is being added to the inert set + -> TcTyVar -- The new equality is tv ~ ty + -> InertCans + -> (WorkList, InertCans) -- See Note [kickOutRewritable] -kickOutRewritable new_fr new_tv ics@(IC { inert_eqs = tv_eqs +kick_out_rewritable 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) + , inert_count = n }) + | not (new_fr `eqMayRewriteFR` new_fr) = (emptyWorkList, ics) -- If new_fr can't rewrite itself, it can't rewrite -- anything else, so no need to kick out anything. @@ -1449,9 +1398,7 @@ kickOutRewritable new_fr new_tv ics@(IC { inert_eqs = tv_eqs , 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 + , inert_count = n - workListWantedCount kicked_out } kicked_out = WL { wl_eqs = tv_eqs_out , wl_funeqs = feqs_out @@ -1461,31 +1408,32 @@ kickOutRewritable new_fr new_tv ics@(IC { inert_eqs = tv_eqs , wl_implics = emptyBag } (tv_eqs_out, tv_eqs_in) = foldDVarEnv kick_out_eqs ([], emptyDVarEnv) tv_eqs - (feqs_out, feqs_in) = partitionFunEqs kick_out_fe funeqmap + (feqs_out, feqs_in) = partitionFunEqs kick_out_ct funeqmap + -- See Note [Kicking out CFunEqCan for fundeps] (dicts_out, dicts_in) = partitionDicts kick_out_ct dictmap (irs_out, irs_in) = partitionBag kick_out_ct irreds (insols_out, insols_in) = partitionBag kick_out_ct insols -- Kick out even insolubles; see Note [Kick out insolubles] - fr_can_rewrite :: CtEvidence -> Bool - fr_can_rewrite ev = new_fr `eqCanRewriteFR` (ctEvFlavourRole ev) + fr_may_rewrite :: CtFlavourRole -> Bool + fr_may_rewrite fs = new_fr `eqMayRewriteFR` fs + -- Can the new item rewrite the inert item? kick_out_ct :: Ct -> Bool -- 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 + -- Or if it has no shadow and the shadow + kick_out_ct ct = kick_out_ev (ctEvidence ct) - kick_out_fe :: Ct -> Bool - 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_ev :: CtEvidence -> Bool + -- Kick it out if the new CTyEqCan can rewrite the inert + -- one. See Note [kickOutRewritable] + kick_out_ev ev = fr_may_rewrite (ctEvFlavourRole ev) + && new_tv `elemVarSet` rewritableTyVarsOfType (ctEvPred ev) + -- NB: this includes the fsk of a CFunEqCan. It can't + -- actually be rewritten, but we need to kick it out + -- so we get to take advantage of injectivity + -- See Note [Kicking out CFunEqCan for fundeps] kick_out_eqs :: EqualCtList -> ([Ct], DTyVarEnv EqualCtList) -> ([Ct], DTyVarEnv EqualCtList) @@ -1500,19 +1448,19 @@ kickOutRewritable new_fr new_tv ics@(IC { inert_eqs = tv_eqs keep_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs_ty, cc_ev = ev , cc_eq_rel = eq_rel }) | tv == new_tv - = not (fr_can_rewrite ev) -- (K1) + = not (fr_may_rewrite fs) -- (K1) | otherwise = check_k2 && check_k3 where fs = ctEvFlavourRole ev - check_k2 = not (fs `eqCanRewriteFR` fs) -- (K2a) - || (fs `eqCanRewriteFR` new_fr) -- (K2b) - || not (new_fr `eqCanRewriteFR` fs) -- (K2c) + check_k2 = not (fs `eqMayRewriteFR` fs) -- (K2a) + || (fs `eqMayRewriteFR` new_fr) -- (K2b) + || not (fr_may_rewrite fs) -- (K2c) || not (new_tv `elemVarSet` tyCoVarsOfType rhs_ty) -- (K2d) check_k3 - | new_fr `eqCanRewriteFR` fs + | fr_may_rewrite fs = case eq_rel of NomEq -> not (rhs_ty `eqType` mkTyVarTy new_tv) ReprEq -> not (isTyVarExposed new_tv rhs_ty) @@ -1525,42 +1473,13 @@ kickOutRewritable new_fr new_tv ics@(IC { inert_eqs = tv_eqs 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 + ; (n_kicked, ics2) <- kickOutRewritable (Given,NomEq) + new_tv ics -- 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 (text "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 }) - = (foldDVarEnv add emptyWorkList der_out, ics { inert_model = new_model }) - where - (der_out, new_model) = partitionDVarEnv 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` tyCoVarsOfType 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 + ; setInertCans ics2 + ; return n_kicked } {- Note [kickOutRewritable] ~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1582,13 +1501,8 @@ new equality, to maintain the inert-set invariants. 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) + - A Derived equality can kick out [D] constraints in inert_eqs, + inert_dicts, inert_irreds etc. - We don't kick out constraints from inert_solved_dicts, and inert_solved_funeqs optimistically. But when we lookup we have to @@ -1657,35 +1571,6 @@ getInertCans = do { inerts <- getTcSInerts; return (inert_cans inerts) } setInertCans :: InertCans -> TcS () setInertCans ics = updInertTcS $ \ inerts -> inerts { inert_cans = ics } -takeGivenInsolubles :: TcS Cts --- See Note [The inert set after solving Givens] -takeGivenInsolubles - = updRetInertCans $ \ cans -> - ( inert_insols cans - , cans { inert_insols = emptyBag - , inert_funeqs = filterFunEqs isGivenCt (inert_funeqs cans) } ) - -{- Note [The inert set after solving Givens] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -After solving the Givens we take two things out of the inert set - - a) The insolubles; we return these to report inaccessible code - We return these separately. We don't want to leave them in - the inert set, lest we confuse them with insolubles arising from - solving wanteds - - b) Any Derived CFunEqCans. Derived CTyEqCans are in the - inert_model and do no harm. In contrast, Derived CFunEqCans - get mixed up with the Wanteds later and confuse the - post-solve-wanted unflattening (Trac #10507). - E.g. From [G] 1 <= m, [G] m <= n - We get [D] 1 <= n, and we must remove it! - Otherwise we unflatten it more then once, and assign - to its fmv more than once...disaster. - It's ok to remove them because they turned out not to - yield an insoluble, and hence have now done their work. --} - updRetInertCans :: (InertCans -> (a, InertCans)) -> TcS a -- Modify the inert set with the supplied function updRetInertCans upd_fn @@ -1723,8 +1608,8 @@ updInertIrreds upd_fn getInertEqs :: TcS (DTyVarEnv EqualCtList) getInertEqs = do { inert <- getInertCans; return (inert_eqs inert) } -getInertModel :: TcS InertModel -getInertModel = do { inert <- getInertCans; return (inert_model inert) } +getInertInsols :: TcS Cts +getInertInsols = do { inert <- getInertCans; return (inert_insols inert) } getInertGivens :: TcS [Ct] -- Returns the Given constraints in the inert set, @@ -1776,42 +1661,42 @@ getUnsolvedInerts , inert_irreds = irreds , inert_dicts = idicts , inert_insols = insols - , inert_model = model } <- getInertCans - ; keep_derived <- keepSolvingDeriveds + } <- getInertCans - ; let der_tv_eqs = foldDVarEnv (add_der_eq keep_derived tv_eqs) - emptyCts model - unsolved_tv_eqs = foldTyEqs add_if_unsolved tv_eqs der_tv_eqs - unsolved_fun_eqs = foldFunEqs add_if_unsolved fun_eqs emptyCts + ; let unsolved_tv_eqs = foldTyEqs add_if_unsolved tv_eqs emptyCts + unsolved_fun_eqs = foldFunEqs add_if_wanted fun_eqs emptyCts unsolved_irreds = Bag.filterBag is_unsolved irreds unsolved_dicts = foldDicts add_if_unsolved idicts emptyCts - others = unsolved_irreds `unionBags` unsolved_dicts + unsolved_others = unsolved_irreds `unionBags` unsolved_dicts + unsolved_insols = filterBag is_unsolved insols ; implics <- getWorkListImplics ; traceTcS "getUnsolvedInerts" $ vcat [ text " tv eqs =" <+> ppr unsolved_tv_eqs , text "fun eqs =" <+> ppr unsolved_fun_eqs - , text "insols =" <+> ppr insols - , text "others =" <+> ppr others + , text "insols =" <+> ppr unsolved_insols + , text "others =" <+> ppr unsolved_others , text "implics =" <+> ppr implics ] - ; return ( implics, unsolved_tv_eqs, unsolved_fun_eqs, insols, others) } - -- Keep even the given insolubles - -- so that we can report dead GADT pattern match branches + ; return ( implics, unsolved_tv_eqs, unsolved_fun_eqs + , unsolved_insols, unsolved_others) } where - add_der_eq keep_derived tv_eqs ct cts - -- See Note [Unsolved Derived equalities] - | CTyEqCan { cc_tyvar = tv, cc_rhs = rhs } <- ct - , isMetaTyVar tv || keep_derived - , 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 + -- For CFunEqCans we ignore the Derived ones, and keep + -- only the Wanteds for flattening. The Derived ones + -- share a unification variable with the corresponding + -- Wanted, so we definitely don't want to to participate + -- in unflattening + -- See Note [Type family equations] + add_if_wanted ct cts | isWantedCt ct = ct `consCts` cts + | otherwise = cts + isInInertEqs :: DTyVarEnv EqualCtList -> TcTyVar -> TcType -> Bool -- True if (a ~N ty) is in the inert set, in either Given or Wanted isInInertEqs eqs tv rhs @@ -1827,22 +1712,23 @@ isInInertEqs eqs tv rhs getNoGivenEqs :: TcLevel -- TcLevel of this implication -> [TcTyVar] -- Skolems of this implication - -> Cts -- Given insolubles from solveGivens - -> TcS Bool -- True <=> definitely no residual given equalities + -> TcS ( Bool -- True <=> definitely no residual given equalities + , Cts ) -- Insoluble constraints arising from givens -- See Note [When does an implication have given equalities?] -getNoGivenEqs tclvl skol_tvs given_insols +getNoGivenEqs tclvl skol_tvs = do { inerts@(IC { inert_eqs = ieqs, inert_irreds = iirreds - , inert_funeqs = funeqs }) - <- getInertCans + , inert_funeqs = funeqs + , inert_insols = insols }) + <- getInertCans ; let local_fsks = foldFunEqs add_fsk funeqs emptyVarSet has_given_eqs = foldrBag ((||) . ev_given_here . ctEvidence) False - (iirreds `unionBags` given_insols) + (iirreds `unionBags` insols) || anyDVarEnv (eqs_given_here local_fsks) ieqs ; traceTcS "getNoGivenEqs" (vcat [ ppr has_given_eqs, ppr inerts - , ppr given_insols]) - ; return (not has_given_eqs) } + , ppr insols]) + ; return (not has_given_eqs, insols) } where eqs_given_here :: VarSet -> EqualCtList -> Bool eqs_given_here local_fsks [CTyEqCan { cc_tyvar = tv, cc_ev = ev }] @@ -1921,17 +1807,10 @@ prohibitedSuperClassSolve from_loc solve_loc {- Note [Unsolved Derived equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -In getUnsolvedInerts, we return a derived equality from the model -for two possible reasons: - - * Because it is a candidate for floating out of this implication. - We only float equalities with a meta-tyvar on the left, so we only - pull those out here. - - * If we are only solving derived constraints (i.e. tcs_need_derived - is true; see Note [Solving for Derived constraints]), then we - those Derived constraints are effectively unsolved, and we need - them! +In getUnsolvedInerts, we return a derived equality from the inert_eqs +because it is a candidate for floating out of this implication. We +only float equalities with a meta-tyvar on the left, so we only pull +those out here. Note [When does an implication have given equalities?] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2029,7 +1908,7 @@ lookupFlatCache fam_tc tys lookup_inerts inert_funeqs | Just (CFunEqCan { cc_ev = ctev, cc_fsk = fsk, cc_tyargs = xis }) <- findFunEq inert_funeqs fam_tc tys - , tys `eqTypes` xis -- the lookup might find a near-match; see + , tys `eqTypes` xis -- The lookup might find a near-match; see -- Note [Use loose types in inert set] = Just (ctEvCoercion ctev, mkTyVarTy fsk, ctEvFlavour ctev) | otherwise = Nothing @@ -2076,42 +1955,6 @@ 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 --} - -addTyEq :: DTyVarEnv EqualCtList -> TcTyVar -> Ct -> DTyVarEnv EqualCtList -addTyEq old_list tv it = extendDVarEnv_C (\old_eqs _new_eqs -> it : old_eqs) - old_list tv [it] - -foldTyEqs :: (Ct -> b -> b) -> DTyVarEnv EqualCtList -> b -> b -foldTyEqs k eqs z - = foldDVarEnv (\cts z -> foldr k z cts) z eqs - -findTyEqs :: InertCans -> TyVar -> EqualCtList -findTyEqs icans tv = lookupDVarEnv (inert_eqs icans) tv `orElse` [] - -delTyEq :: DTyVarEnv EqualCtList -> TcTyVar -> TcType -> DTyVarEnv EqualCtList -delTyEq m tv t = modifyDVarEnv (filter (not . isThisOne)) m tv - where isThisOne (CTyEqCan { cc_rhs = t1 }) = eqType t t1 - isThisOne _ = False - -{- ********************************************************************* -* * TcAppMap * * ************************************************************************ @@ -2245,9 +2088,6 @@ type FunEqMap a = TcAppMap a -- A map whose key is a (TyCon, [Type]) pair emptyFunEqs :: TcAppMap a emptyFunEqs = emptyTcAppMap -sizeFunEqMap :: FunEqMap a -> Int -sizeFunEqMap m = foldFunEqs (\ _ x -> x+1) m 0 - findFunEq :: FunEqMap a -> TyCon -> [Type] -> Maybe a findFunEq m tc tys = findTcApp m (getUnique tc) tys @@ -2269,8 +2109,8 @@ foldFunEqs = foldTcAppMap -- mapFunEqs :: (a -> b) -> FunEqMap a -> FunEqMap b -- mapFunEqs = mapTcApp -filterFunEqs :: (Ct -> Bool) -> FunEqMap Ct -> FunEqMap Ct -filterFunEqs = filterTcAppMap +-- filterFunEqs :: (Ct -> Bool) -> FunEqMap Ct -> FunEqMap Ct +-- filterFunEqs = filterTcAppMap insertFunEq :: FunEqMap a -> TyCon -> [Type] -> a -> FunEqMap a insertFunEq m tc tys val = insertTcApp m (getUnique tc) tys val @@ -2324,16 +2164,6 @@ All you can do is Filling in a dictionary evidence variable means to create a binding for it, so TcS carries a mutable location where the binding can be added. This is initialised from the innermost implication constraint. - -Note [Solving for Derived constraints] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Sometimes we invoke the solver on a bunch of Derived constraints, not to -generate any evidence, but just to cause unification side effects or to -produce a simpler set of constraints. If that is what we are doing, we -should do two things differently: - a) Don't stop when you've solved all the Wanteds; instead keep going - if there are any Deriveds in the work queue. - b) In getInertUnsolved, include Derived ones -} data TcSEnv @@ -2350,11 +2180,7 @@ data TcSEnv -- The main work-list and the flattening worklist -- See Note [Work list priorities] and - tcs_worklist :: IORef WorkList, -- Current worklist - - tcs_need_deriveds :: Bool - -- Keep solving, even if all the unsolved constraints are Derived - -- See Note [Solving for Derived constraints] + tcs_worklist :: IORef WorkList -- Current worklist } --------------- @@ -2450,7 +2276,7 @@ runTcS :: TcS a -- What to run -> TcM (a, EvBindMap) runTcS tcs = do { ev_binds_var <- TcM.newTcEvBinds - ; res <- runTcSWithEvBinds False ev_binds_var tcs + ; res <- runTcSWithEvBinds ev_binds_var tcs ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var ; return (res, ev_binds) } @@ -2460,19 +2286,18 @@ runTcS tcs runTcSDeriveds :: TcS a -> TcM a runTcSDeriveds tcs = do { ev_binds_var <- TcM.newTcEvBinds - ; runTcSWithEvBinds True ev_binds_var tcs } + ; runTcSWithEvBinds ev_binds_var tcs } -- | This can deal only with equality constraints. runTcSEqualities :: TcS a -> TcM a runTcSEqualities thing_inside = do { ev_binds_var <- TcM.newTcEvBinds - ; runTcSWithEvBinds False ev_binds_var thing_inside } + ; runTcSWithEvBinds ev_binds_var thing_inside } -runTcSWithEvBinds :: Bool -- ^ keep running even if only Deriveds are left? - -> EvBindsVar +runTcSWithEvBinds :: EvBindsVar -> TcS a -> TcM a -runTcSWithEvBinds solve_deriveds ev_binds_var tcs +runTcSWithEvBinds ev_binds_var tcs = do { unified_var <- TcM.newTcRef 0 ; step_count <- TcM.newTcRef 0 ; inert_var <- TcM.newTcRef emptyInert @@ -2481,8 +2306,7 @@ runTcSWithEvBinds solve_deriveds ev_binds_var tcs , tcs_unified = unified_var , tcs_count = step_count , tcs_inerts = inert_var - , tcs_worklist = wl_var - , tcs_need_deriveds = solve_deriveds } + , tcs_worklist = wl_var } -- Run the computation ; res <- unTcS tcs env @@ -2536,7 +2360,6 @@ nestImplicTcS ref inner_tclvl (TcS thing_inside) = TcS $ \ TcSEnv { tcs_unified = unified_var , tcs_inerts = old_inert_var , tcs_count = count - , tcs_need_deriveds = solve_deriveds } -> do { inerts <- TcM.readTcRef old_inert_var ; let nest_inert = inerts { inert_flat_cache = emptyExactFunEqs } @@ -2547,8 +2370,7 @@ nestImplicTcS ref inner_tclvl (TcS thing_inside) , tcs_unified = unified_var , tcs_count = count , tcs_inerts = new_inert_var - , tcs_worklist = new_wl_var - , tcs_need_deriveds = solve_deriveds } + , tcs_worklist = new_wl_var } ; res <- TcM.setTcLevel inner_tclvl $ thing_inside nest_env @@ -2642,10 +2464,6 @@ updWorkListTcS f ; let new_work = f wl_curr ; wrapTcS (TcM.writeTcRef wl_var new_work) } --- | Should we keep solving even only deriveds are left? -keepSolvingDeriveds :: TcS Bool -keepSolvingDeriveds = TcS (return . tcs_need_deriveds) - emitWorkNC :: [CtEvidence] -> TcS () emitWorkNC evs | null evs @@ -2869,35 +2687,44 @@ which will result in two Deriveds to end up in the insoluble set: -- Flatten skolems -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ newFlattenSkolem :: CtFlavour -> CtLoc - -> TcType -- F xis - -> TcS (CtEvidence, Coercion, TcTyVar) -- [W] x:: F xis ~ fsk -newFlattenSkolem Given loc fam_ty - = do { fsk <- newFsk fam_ty - ; let co = mkNomReflCo fam_ty - ; ev <- newGivenEvVar loc (mkPrimEqPred fam_ty (mkTyVarTy fsk), - EvCoercion co) - ; return (ev, co, fsk) } - -newFlattenSkolem Wanted loc fam_ty - = do { fmv <- newFmv fam_ty - ; (ev, hole_co) <- newWantedEq loc Nominal fam_ty (mkTyVarTy fmv) - ; return (ev, hole_co, fmv) } - -newFlattenSkolem Derived loc fam_ty - = do { fmv <- newFmv fam_ty - ; ev <- newDerivedNC loc (mkPrimEqPred fam_ty (mkTyVarTy fmv)) - ; return (ev, pprPanic "newFlattenSkolem [D]" (ppr fam_ty), fmv) } - -newFsk, newFmv :: TcType -> TcS TcTyVar -newFsk fam_ty = wrapTcS (TcM.newFskTyVar fam_ty) -newFmv fam_ty = wrapTcS (TcM.newFmvTyVar fam_ty) + -> TyCon -> [TcType] -- F xis + -> TcS (CtEvidence, Coercion, TcTyVar) -- [G/WD] x:: F xis ~ fsk +newFlattenSkolem flav loc tc xis + = do { stuff@(ev, co, fsk) <- new_skolem + ; let fsk_ty = mkTyVarTy fsk + ; extendFlatCache tc xis (co, fsk_ty, ctEvFlavour ev) + ; return stuff } + where + fam_ty = mkTyConApp tc xis + + new_skolem + | Given <- flav + = do { fsk <- wrapTcS (TcM.newFskTyVar fam_ty) + ; let co = mkNomReflCo fam_ty + ; ev <- newGivenEvVar loc (mkPrimEqPred fam_ty (mkTyVarTy fsk), + EvCoercion co) + ; return (ev, co, fsk) } + + | otherwise -- Generate a [WD] for both Wanted and Derived + -- See Note [No Derived CFunEqCans] + = do { fmv <- wrapTcS (TcM.newFmvTyVar fam_ty) + ; (ev, hole_co) <- newWantedEq loc Nominal fam_ty (mkTyVarTy fmv) + ; return (ev, hole_co, fmv) } extendFlatCache :: TyCon -> [Type] -> (TcCoercion, TcType, CtFlavour) -> TcS () -extendFlatCache tc xi_args stuff +extendFlatCache tc xi_args stuff@(_, ty, fl) + | isGivenOrWDeriv fl -- Maintain the invariant that inert_flat_cache + -- only has [G] and [WD] CFunEqCans = do { dflags <- getDynFlags ; when (gopt Opt_FlatCache dflags) $ - updInertTcS $ \ is@(IS { inert_flat_cache = fc }) -> - is { inert_flat_cache = insertExactFunEq fc tc xi_args stuff } } + do { traceTcS "extendFlatCache" (vcat [ ppr tc <+> ppr xi_args + , ppr fl, ppr ty ]) + -- 'co' can be bottom, in the case of derived items + ; updInertTcS $ \ is@(IS { inert_flat_cache = fc }) -> + is { inert_flat_cache = insertExactFunEq fc tc xi_args stuff } } } + + | otherwise + = return () -- Instantiations -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -3039,6 +2866,7 @@ newWantedEq loc role ty1 ty2 = do { hole <- wrapTcS $ TcM.newCoercionHole ; traceTcS "Emitting new coercion hole" (ppr hole <+> dcolon <+> ppr pty) ; return ( CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole + , ctev_nosh = WDeriv , ctev_loc = loc} , mkHoleCo hole role ty1 ty2 ) } where @@ -3048,11 +2876,11 @@ newWantedEq loc role ty1 ty2 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 - ; new_ev <- newEvVar pty + = do { new_ev <- newEvVar pty ; traceTcS "Emitting new wanted" (ppr new_ev <+> dcolon <+> ppr pty $$ pprCtLoc loc) ; return (CtWanted { ctev_pred = pty, ctev_dest = EvVarDest new_ev + , ctev_nosh = WDeriv , ctev_loc = loc })} newWantedEvVar :: CtLoc -> TcPredType -> TcS MaybeNew diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs index c23b3171ab..a9548f292e 100644 --- a/compiler/typecheck/TcSimplify.hs +++ b/compiler/typecheck/TcSimplify.hs @@ -413,8 +413,7 @@ simplifyAmbiguityCheck ty wanteds -- inaccessible code ; allow_ambiguous <- xoptM LangExt.AllowAmbiguousTypes ; traceTc "reportUnsolved(ambig) {" empty - ; tc_lvl <- TcM.getTcLevel - ; unless (allow_ambiguous && not (insolubleWC tc_lvl final_wc)) + ; unless (allow_ambiguous && not (insolubleWC final_wc)) (discardResult (reportUnsolved final_wc)) ; traceTc "reportUnsolved(ambig) }" empty @@ -431,11 +430,8 @@ simplifyDefault :: ThetaType -- Wanted; has no type variables in it -> TcM () -- Succeeds if the constraint is soluble simplifyDefault theta = do { traceTc "simplifyDefault" empty - ; loc <- getCtLocM DefaultOrigin Nothing - ; let wanted = [ CtDerived { ctev_pred = pred - , ctev_loc = loc } - | pred <- theta ] - ; unsolved <- runTcSDeriveds (solveWanteds (mkSimpleWC wanted)) + ; wanteds <- newWanteds DefaultOrigin theta + ; unsolved <- runTcSDeriveds (solveWantedsAndDrop (mkSimpleWC wanteds)) ; traceTc "reportUnsolved {" empty ; reportAllUnsolved unsolved ; traceTc "reportUnsolved }" empty @@ -451,7 +447,8 @@ tcCheckSatisfiability given_ids do { traceTcS "checkSatisfiability {" (ppr given_ids) ; let given_cts = mkGivens given_loc (bagToList given_ids) -- See Note [Superclasses and satisfiability] - ; insols <- solveSimpleGivens given_cts + ; solveSimpleGivens given_cts + ; insols <- getInertInsols ; insols <- try_harder insols ; traceTcS "checkSatisfiability }" (ppr insols) ; return (isEmptyBag insols) } @@ -467,7 +464,8 @@ tcCheckSatisfiability given_ids | otherwise = do { pending_given <- getPendingScDicts ; new_given <- makeSuperClasses pending_given - ; solveSimpleGivens new_given } + ; solveSimpleGivens new_given + ; getInertInsols } {- Note [Superclasses and satisfiability] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -573,7 +571,7 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds ; psig_theta_vars <- mapM TcM.newEvVar psig_theta ; wanted_transformed_incl_derivs <- setTcLevel rhs_tclvl $ - runTcSWithEvBinds False ev_binds_var $ + runTcSWithEvBinds ev_binds_var $ do { let loc = mkGivenLoc rhs_tclvl UnkSkol tc_lcl_env psig_givens = mkGivens loc psig_theta_vars ; _ <- solveSimpleGivens psig_givens @@ -590,7 +588,7 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds ; let wanted_transformed = dropDerivedWC wanted_transformed_incl_derivs ; quant_pred_candidates -- Fully zonked - <- if insolubleWC rhs_tclvl wanted_transformed_incl_derivs + <- if insolubleWC wanted_transformed_incl_derivs then return [] -- See Note [Quantification with errors] -- NB: must include derived errors in this test, -- hence "incl_derivs" @@ -615,15 +613,11 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds ; mapM_ def_tyvar meta_tvs ; mapM_ (promoteTyVar rhs_tclvl) meta_tvs + ; clone_wanteds <- mapM cloneWanted (bagToList quant_cand) ; WC { wc_simple = simples } <- setTcLevel rhs_tclvl $ - runTcSDeriveds $ - solveSimpleWanteds $ - mapBag toDerivedCt quant_cand - -- NB: we don't want evidence, - -- so use Derived constraints - - ; simples <- TcM.zonkSimples simples + simplifyWantedsTcM clone_wanteds + -- Discard evidence; result is zonked ; return [ ctEvPred ev | ct <- bagToList simples , let ev = ctEvidence ct ] } @@ -1074,7 +1068,7 @@ simplifyWantedsTcM :: [CtEvidence] -> TcM WantedConstraints -- Postcondition: fully zonked and unflattened constraints simplifyWantedsTcM wanted = do { traceTc "simplifyWantedsTcM {" (ppr wanted) - ; (result, _) <- runTcS (solveWantedsAndDrop $ mkSimpleWC wanted) + ; (result, _) <- runTcS (solveWantedsAndDrop (mkSimpleWC wanted)) ; result <- TcM.zonkWC result ; traceTc "simplifyWantedsTcM }" (ppr result) ; return result } @@ -1093,20 +1087,19 @@ solveWanteds :: WantedConstraints -> TcS WantedConstraints solveWanteds wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics }) = do { traceTcS "solveWanteds {" (ppr wc) - -- Try the simple bit, including insolubles. Solving insolubles a - -- second time round is a bit of a waste; but the code is simple - -- and the program is wrong anyway, and we don't run the danger - -- of adding Derived insolubles twice; see - -- TcSMonad Note [Do not add duplicate derived insolubles] ; wc1 <- solveSimpleWanteds simples - ; (no_new_scs, wc1) <- expandSuperClasses wc1 ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1 ; (floated_eqs, implics2) <- solveNestedImplications (implics `unionBags` implics1) + ; (no_new_scs, simples2) <- expandSuperClasses simples1 + + ; traceTcS "solveWanteds middle" $ vcat [ text "simples1 =" <+> ppr simples1 + , text "simples2 =" <+> ppr simples2 ] ; dflags <- getDynFlags - ; final_wc <- simpl_loop 0 (solverIterations dflags) floated_eqs no_new_scs - (WC { wc_simple = simples1, wc_impl = implics2 + ; final_wc <- simpl_loop 0 (solverIterations dflags) floated_eqs + no_new_scs + (WC { wc_simple = simples2, wc_impl = implics2 , wc_insol = insols `unionBags` insols1 }) ; bb <- TcS.getTcEvBindsMap @@ -1119,9 +1112,9 @@ solveWanteds wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics simpl_loop :: Int -> IntWithInf -> Cts -> Bool -> WantedConstraints -> TcS WantedConstraints -simpl_loop n limit floated_eqs no_new_scs +simpl_loop n limit floated_eqs no_new_deriveds wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics }) - | isEmptyBag floated_eqs && no_new_scs + | isEmptyBag floated_eqs && no_new_deriveds = return wc -- Done! | n `intGtLimit` limit @@ -1134,8 +1127,8 @@ simpl_loop n limit floated_eqs no_new_scs 2 (vcat [ text "Unsolved:" <+> ppr wc , ppUnless (isEmptyBag floated_eqs) $ text "Floated equalities:" <+> ppr floated_eqs - , ppUnless no_new_scs $ - text "New superclasses found" + , ppUnless no_new_deriveds $ + text "New deriveds found" , text "Set limit with -fconstraint-solver-iterations=n; n=0 for no limit" ])) ; return wc } @@ -1144,7 +1137,7 @@ simpl_loop n limit floated_eqs no_new_scs = do { let n_floated = lengthBag floated_eqs ; csTraceTcS $ text "simpl_loop iteration=" <> int n - <+> (parens $ hsep [ text "no new scs =" <+> ppr no_new_scs <> comma + <+> (parens $ hsep [ text "no new deriveds =" <+> ppr no_new_deriveds <> comma , int n_floated <+> text "floated eqs" <> comma , int (lengthBag simples) <+> text "simples to solve" ]) @@ -1155,8 +1148,8 @@ simpl_loop n limit floated_eqs no_new_scs -- NB: the floated_eqs may include /derived/ equalities -- arising from fundeps inside an implication - ; (no_new_scs, wc1) <- expandSuperClasses wc1 ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1 + ; (no_new_scs, simples2) <- expandSuperClasses simples1 -- We have already tried to solve the nested implications once -- Try again only if we have unified some meta-variables @@ -1167,36 +1160,36 @@ simpl_loop n limit floated_eqs no_new_scs else solveNestedImplications (implics `unionBags` implics1) ; simpl_loop (n+1) limit floated_eqs2 no_new_scs - (WC { wc_simple = simples1, wc_impl = implics2 + (WC { wc_simple = simples2, wc_impl = implics2 , wc_insol = insols `unionBags` insols1 }) } -expandSuperClasses :: WantedConstraints -> TcS (Bool, WantedConstraints) --- If there are any unsolved wanteds, expand one step of superclasses for --- unsolved wanteds or givens +expandSuperClasses :: Cts -> TcS (Bool, Cts) +-- If there are any unsolved wanteds, expand one step of +-- superclasses for deriveds +-- Returned Bool is True <=> no new superclass constraints added -- See Note [The superclass story] in TcCanonical -expandSuperClasses wc@(WC { wc_simple = unsolved, wc_insol = insols }) +expandSuperClasses unsolved | not (anyBag superClassesMightHelp unsolved) - = return (True, wc) + = return (True, unsolved) | otherwise = do { traceTcS "expandSuperClasses {" empty ; let (pending_wanted, unsolved') = mapAccumBagL get [] unsolved - get acc ct = case isPendingScDict ct of - Just ct' -> (ct':acc, ct') - Nothing -> (acc, ct) + get acc ct | Just ct' <- isPendingScDict ct + = (ct':acc, ct') + | otherwise + = (acc, ct) ; pending_given <- getPendingScDicts ; if null pending_given && null pending_wanted then do { traceTcS "End expandSuperClasses no-op }" empty - ; return (True, wc) } + ; return (True, unsolved) } else do { new_given <- makeSuperClasses pending_given - ; new_insols <- solveSimpleGivens new_given + ; solveSimpleGivens new_given ; new_wanted <- makeSuperClasses pending_wanted ; traceTcS "End expandSuperClasses }" (vcat [ text "Given:" <+> ppr pending_given - , text "Insols from given:" <+> ppr new_insols , text "Wanted:" <+> ppr new_wanted ]) - ; return (False, wc { wc_simple = unsolved' `unionBags` listToBag new_wanted - , wc_insol = insols `unionBags` new_insols }) } } + ; return (False, unsolved' `unionBags` listToBag new_wanted) } } solveNestedImplications :: Bag Implication -> TcS (Cts, Bag Implication) @@ -1244,17 +1237,17 @@ solveImplication imp@(Implic { ic_tclvl = tclvl -- Solve the nested constraints ; (no_given_eqs, given_insols, residual_wanted) - <- nestImplicTcS ev_binds_var tclvl $ + <- nestImplicTcS ev_binds_var tclvl $ do { let loc = mkGivenLoc tclvl info env givens = mkGivens loc given_ids - ; given_insols <- solveSimpleGivens givens + ; solveSimpleGivens givens ; residual_wanted <- solveWanteds wanteds -- solveWanteds, *not* solveWantedsAndDrop, because -- we want to retain derived equalities so we can float -- them out in floatEqualities - ; no_eqs <- getNoGivenEqs tclvl skols given_insols + ; (no_eqs, given_insols) <- getNoGivenEqs tclvl skols -- Call getNoGivenEqs /after/ solveWanteds, because -- solveWanteds can augment the givens, via expandSuperClasses, -- to reveal given superclass equalities @@ -1289,7 +1282,6 @@ setImplicationStatus :: Implication -> TcS (Maybe Implication) -- Return Nothing if we can discard the implication altogether setImplicationStatus implic@(Implic { ic_binds = ev_binds_var , ic_info = info - , ic_tclvl = tc_lvl , ic_wanted = wc , ic_given = givens }) | some_insoluble @@ -1299,10 +1291,13 @@ setImplicationStatus implic@(Implic { ic_binds = ev_binds_var , wc_insol = pruned_insols } } | some_unsolved - = return $ Just $ + = do { traceTcS "setImplicationStatus" $ + vcat [ppr givens $$ ppr simples $$ ppr insols $$ ppr mb_implic_needs] + ; return $ Just $ implic { ic_status = IC_Unsolved , ic_wanted = wc { wc_simple = pruned_simples , wc_insol = pruned_insols } } + } | otherwise -- Everything is solved; look at the implications -- See Note [Tracking redundant constraints] @@ -1342,7 +1337,7 @@ setImplicationStatus implic@(Implic { ic_binds = ev_binds_var where WC { wc_simple = simples, wc_impl = implics, wc_insol = insols } = wc - some_insoluble = insolubleWC tc_lvl wc + some_insoluble = insolubleWC wc some_unsolved = not (isEmptyBag simples && isEmptyBag insols) || isNothing mb_implic_needs @@ -1510,23 +1505,13 @@ works: ----- Shortcomings -After I introduced -Wredundant-constraints there was extensive discussion -about cases where it reported a redundant constraint but the programmer -really wanted it. See +Consider (see Trac #9939) + f2 :: (Eq a, Ord a) => a -> a -> Bool + -- Ord a redundant, but Eq a is reported + f2 x y = (x == y) - * #11370 (removed it from -Wdefault) - * #10635 (removed it from -Wall as well) - * #12142 - * #11474, #10100 (class not used, but its fundeps are) - * #11099 (redundant, but still desired) - * #10183 (constraint necessary to exclude omitted case) - - * #9939: f2 :: (Eq a, Ord a) => a -> a -> Bool - -- Ord a redundant, but Eq a is reported - f2 x y = (x == y) - - We report (Eq a) as redundant, whereas actually (Ord a) is. - But it's really not easy to detect that! +We report (Eq a) as redundant, whereas actually (Ord a) is. But it's +really not easy to detect that! Note [Cutting off simpl_loop] @@ -1770,29 +1755,6 @@ beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs: in (g1 '3', g2 undefined) -Note [Solving Family Equations] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -After we are done with simplification we may be left with constraints of the form: - [Wanted] F xis ~ beta -If 'beta' is a touchable unification variable not already bound in the TyBinds -then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'. - -When is it ok to do so? - 1) 'beta' must not already be defaulted to something. Example: - - [Wanted] F Int ~ beta <~ Will default [beta := F Int] - [Wanted] F Char ~ beta <~ Already defaulted, can't default again. We - have to report this as unsolved. - - 2) However, we must still do an occurs check when defaulting (F xis ~ beta), to - set [beta := F xis] only if beta is not among the free variables of xis. - - 3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS - of type family equations. See Inert Set invariants in TcInteract. - -This solving is now happening during zonking, see Note [Unflattening while zonking] -in TcMType. - ********************************************************************************* * * diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs index 99927aab38..e2644c537f 100644 --- a/compiler/typecheck/TcType.hs +++ b/compiler/typecheck/TcType.hs @@ -102,6 +102,7 @@ module TcType ( -- * Finding "exact" (non-dead) type variables exactTyCoVarsOfType, exactTyCoVarsOfTypes, splitDepVarsOfType, splitDepVarsOfTypes, TcDepVars(..), tcDepVarSet, + rewritableTyVarsOfTypes, rewritableTyVarsOfType, -- * Extracting bound variables allBoundVariables, allBoundVariabless, @@ -835,6 +836,23 @@ exactTyCoVarsOfType ty exactTyCoVarsOfTypes :: [Type] -> TyVarSet exactTyCoVarsOfTypes tys = mapUnionVarSet exactTyCoVarsOfType tys +rewritableTyVarsOfTypes :: [TcType] -> TcTyVarSet +rewritableTyVarsOfTypes tys = mapUnionVarSet rewritableTyVarsOfType tys + +rewritableTyVarsOfType :: TcType -> TcTyVarSet +rewritableTyVarsOfType ty + = go ty + where + go (TyVarTy tv) = unitVarSet tv + go (LitTy {}) = emptyVarSet + go (TyConApp _ tys) = rewritableTyVarsOfTypes tys + go (AppTy fun arg) = go fun `unionVarSet` go arg + go (FunTy arg res) = go arg `unionVarSet` go res + go ty@(ForAllTy {}) = pprPanic "rewriteableTyVarOfType" (ppr ty) + go (CastTy ty _co) = go ty + go (CoercionTy _co) = emptyVarSet + + {- ********************************************************************* * * Bound variables in a type diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs index d194321fe4..566594f40b 100644 --- a/compiler/typecheck/TcUnify.hs +++ b/compiler/typecheck/TcUnify.hs @@ -1509,8 +1509,10 @@ maybe_sym IsSwapped = mkSymCo maybe_sym NotSwapped = id swapOverTyVars :: TcTyVar -> TcTyVar -> Bool --- See Note [Canonical orientation for tyvar/tyvar equality constraints] swapOverTyVars tv1 tv2 + | isFmvTyVar tv1 = False -- See Note [Fmv Orientation Invariant] + | isFmvTyVar tv2 = True + | Just lvl1 <- metaTyVarTcLevel_maybe tv1 -- If tv1 is touchable, swap only if tv2 is also -- touchable and it's strictly better to update the latter @@ -1565,7 +1567,46 @@ canSolveByUnification tclvl tv xi FlatSkol {} -> False RuntimeUnk -> True -{- +{- Note [Fmv Orientation Invariant] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + * We always orient a constraint + fmv ~ alpha + with fmv on the left, even if alpha is + a touchable unification variable + +Reason: doing it the other way round would unify alpha:=fmv, but that +really doesn't add any info to alpha. But a later constraint alpha ~ +Int might unlock everything. Comment:9 of #12526 gives a detailed +example. + +WARNING: I've gone to and fro on this one several times. +I'm now pretty sure that unifying alpha:=fmv is a bad idea! +So orienting with fmvs on the left is a good thing. + +This example comes from IndTypesPerfMerge. (Others include +T10226, T10009.) + From the ambiguity check for + f :: (F a ~ a) => a + we get: + [G] F a ~ a + [WD] F alpha ~ alpha, alpha ~ a + + From Givens we get + [G] F a ~ fsk, fsk ~ a + + Now if we flatten we get + [WD] alpha ~ fmv, F alpha ~ fmv, alpha ~ a + + Now, if we unified alpha := fmv, we'd get + [WD] F fmv ~ fmv, [WD] fmv ~ a + And now we are stuck. + +So instead the Fmv Orientation Invariant puts te fmv on the +left, giving + [WD] fmv ~ alpha, [WD] F alpha ~ fmv, [WD] alpha ~ a + + Now we get alpha:=a, and everything works out + Note [Prevent unification with type families] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We prevent unification with type families because of an uneasy compromise. diff --git a/testsuite/tests/indexed-types/should_compile/T10226.hs b/testsuite/tests/indexed-types/should_compile/T10226.hs index 14d3a3eb31..77ce29a69d 100644 --- a/testsuite/tests/indexed-types/should_compile/T10226.hs +++ b/testsuite/tests/indexed-types/should_compile/T10226.hs @@ -42,6 +42,30 @@ showFromF fa = undefined showFromF' :: (Show (FInv b), F (FInv b) ~ b) => b -> String showFromF' = showFromF +{- [G] F (FInv b) ~ b + [W] FInv (F alpha) ~ alpha + [W] F alpha ~ b +--> + [G] g1: FInv b ~ fsk1 + [G] g2: F fsk1 ~ fsk2 + [G} g3: fsk2 ~ b + + [W] F alpha ~ fmv1 + [W] FInv fmv1 ~ fmv2 + [W] fmv2 ~ alpha + [W] fmv1 ~ b + + [D] d1: F alpha ~ fmv1 + [D] d2: FInv fmv1 ~ fmv2 + [D] d3: fmv2 ~ alpha + [D] d4: fmv1 ~ b + +--> d2 + d4: [D] FInv b ~ fmv2 + + g1: [D] fmv2 ~ b +--> d3: b ~ alpha, and we are done + +-} + {------------------------------------------------------------------------------- In 7.10 the definition of showFromF' is not accepted, but it gets stranger. In 7.10 we cannot _call_ showFromF at all, even at a concrete type. Below @@ -57,3 +81,36 @@ type instance FInv Int = Int test :: String test = showFromF (0 :: Int) + +{- + + [WD] FInv (F alpha) ~ alpha + [WD] F alpha ~ Int + +--> + [WD] F alpha ~ fuv0 +* [WD] FInv fuv0 ~ fuv1 + [WD] fuv1 ~ alpha + [WD] fuv0 ~ Int + +--> + [WD] F alpha ~ fuv0 + [W] FInv fuv0 ~ fuv1 +* [D] FInv Int ~ fuv1 + [WD] fuv1 ~ alpha + [WD] fuv0 ~ Int + +--> + [WD] F alpha ~ fuv0 + [W] FInv fuv0 ~ fuv1 +* [D] fuv1 ~ Int + [WD] fuv1 ~ alpha + [WD] fuv0 ~ Int + +--> + [WD] F alpha ~ fuv0 + [W] FInv fuv0 ~ fuv1 + [D] alpha := Int + [WD] fuv1 ~ alpha + [WD] fuv0 ~ Int +-} diff --git a/testsuite/tests/indexed-types/should_compile/T10634.hs b/testsuite/tests/indexed-types/should_compile/T10634.hs index f02cf810da..0b52ef534a 100644 --- a/testsuite/tests/indexed-types/should_compile/T10634.hs +++ b/testsuite/tests/indexed-types/should_compile/T10634.hs @@ -21,3 +21,18 @@ instance Convert Int32 where x :: Int8 x = down 8 + +{- From x = down 8 + +[WD] Num alpha +[WD] Convert alpha +[WD] Down alpha ~ Int8 + +--> superclasses +[D] Up (Down alpha) ~ alpha + +--> substitute (Down alpha ~ Int8) +[D] Up Int8 ~ alpha + +--> alpha := Int16 +-} diff --git a/testsuite/tests/indexed-types/should_compile/T12526.hs b/testsuite/tests/indexed-types/should_compile/T12526.hs new file mode 100644 index 0000000000..35a653a544 --- /dev/null +++ b/testsuite/tests/indexed-types/should_compile/T12526.hs @@ -0,0 +1,69 @@ +{-# LANGUAGE TypeFamilies, MonoLocalBinds #-} +module T12526 where + +type family P (s :: * -> *) :: * -> * -> * +type instance P Signal = Causal + +type family S (p :: * -> * -> *) :: * -> * +type instance S Causal = Signal + +class (P (S p) ~ p) => CP p +instance CP Causal + +data Signal a = Signal +data Causal a b = Causal + +shapeModOsci :: CP p => p Float Float +shapeModOsci = undefined + +f :: Causal Float Float -> Bool +f = undefined + +-- This fails +ping :: Bool +ping = let osci = shapeModOsci in f osci + + +-- This works +-- ping :: Bool +-- ping = f shapeModOsci + + +{- + + osci :: p Float Float + [W] CP p, [D] P (S p) ~ p +--> + [W] CP p, [D] P fuv1 ~ fuv2, S p ~ fuv1, fuv2 ~ p +--> + p := fuv2 + [W] CP fuv2, [D] P fuv1 ~ fuv2, S fuv2 ~ fuv1 + +-} + +-- P (S p) ~ p +-- p Float Float ~ Causal Float Float + + +{- + P (S p) ~ p + p Float Float ~ Causal Float Float + +---> + S p ~ fuv1 (FunEq) + P fuv1 ~ fuv2 (FunEq) + fuv2 ~ p + p F F ~ Causal F F + +---> + p := fuv2 + + fuv2 ~ Causal + S fuv2 ~ fuv1 (FunEq) + P fuv1 ~ fuv2 (FunEq) + +---> unflatten + fuv1 := S fuv2 + fuv2 := Causal + +-} diff --git a/testsuite/tests/indexed-types/should_compile/T12538.hs b/testsuite/tests/indexed-types/should_compile/T12538.hs new file mode 100644 index 0000000000..9aff36e47d --- /dev/null +++ b/testsuite/tests/indexed-types/should_compile/T12538.hs @@ -0,0 +1,40 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} + +module T12538 where + +data Tagged t a = Tagged a + +type family Tag a where + Tag (Tagged t a) = Tagged t a + Tag a = Tagged Int a + +class (r ~ Tag a) => TagImpl a r | a -> r where + tag :: a -> r + +instance {-# OVERLAPPING #-} (r ~ Tag (Tagged t a)) => TagImpl (Tagged t a) r where + tag = id + +#ifdef WRONG +instance {-# OVERLAPPING #-} (r ~ Tagged t a, r ~ Tag a) => TagImpl a r where +#else +instance {-# OVERLAPPING #-} (r ~ Tagged Int a, r ~ Tag a) => TagImpl a r where +#endif + tag = Tagged @Int + +data family DF x +data instance DF (Tagged t a) = DF (Tagged t a) + +class ToDF a b | a -> b where + df :: a -> b + +instance (TagImpl a a', b ~ DF a') => ToDF a b where + df = DF . tag + +main :: IO () +main = pure () diff --git a/testsuite/tests/indexed-types/should_compile/T12538.stderr b/testsuite/tests/indexed-types/should_compile/T12538.stderr new file mode 100644 index 0000000000..ca106246e7 --- /dev/null +++ b/testsuite/tests/indexed-types/should_compile/T12538.stderr @@ -0,0 +1,13 @@ + +T12538.hs:37:8: error: + • Could not deduce: a' ~ Tagged Int a + from the context: (TagImpl a a', b ~ DF a') + bound by the instance declaration at T12538.hs:36:10-46 + ‘a'’ is a rigid type variable bound by + the instance declaration at T12538.hs:36:10-46 + Expected type: a -> b + Actual type: a -> DF (Tagged Int a) + • In the expression: DF . tag + In an equation for ‘df’: df = DF . tag + In the instance declaration for ‘ToDF a b’ + • Relevant bindings include df :: a -> b (bound at T12538.hs:37:3) diff --git a/testsuite/tests/indexed-types/should_compile/T3017.stderr b/testsuite/tests/indexed-types/should_compile/T3017.stderr index 29877bf2aa..b11c95eb6c 100644 --- a/testsuite/tests/indexed-types/should_compile/T3017.stderr +++ b/testsuite/tests/indexed-types/should_compile/T3017.stderr @@ -4,7 +4,7 @@ TYPE SIGNATURES emptyL :: forall a. ListColl a insert :: forall c. Coll c => Elem c -> c -> c test2 :: - forall a b c. (Elem c ~ (a, b), Coll c, Num a, Num b) => c -> c + forall a b c. (Elem c ~ (a, b), Num b, Num a, Coll c) => c -> c TYPE CONSTRUCTORS class Coll c where type family Elem c :: * open diff --git a/testsuite/tests/indexed-types/should_compile/T4338.hs b/testsuite/tests/indexed-types/should_compile/T4338.hs index 6fa2ae85ac..64e224e11d 100644 --- a/testsuite/tests/indexed-types/should_compile/T4338.hs +++ b/testsuite/tests/indexed-types/should_compile/T4338.hs @@ -17,7 +17,40 @@ instance Foo Char Int where tickle = (+1) test :: (Foo a b) => a -> a -test = back . tickle . there +test x = back (tickle (there x)) main :: IO () main = print $ test 'F' + +{- + +[G] Foo a b +[G] There a ~ b +[G] Back b ~ a + +[W] Foo a beta -- from 'there' +[W] Foo alpha beta -- from tickle +[W] Foo a beta -- from back + +[D] There a ~ beta +[D] Back beta ~ a + +[D] There alpha ~ beta +[D] Back beta ~ alpha + + +-- Hence beta = b +-- alpha = a + + + +[W] Foo a (There t_a1jL) +[W] Foo t_a1jL (There t_a1jL) +[W] Back (There t_a1jL) ~ t_a1jL + +[D] There a ~ There t_a1jL + hence There t_a1jL ~ b +[D] Back (There t_a1jL) ~ a +[D] There t_a1jL ~ There t_a1jL +[D] Back (There t_a1jL) ~ t_a1jL +-} diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T index b093128a41..eb71a2866e 100644 --- a/testsuite/tests/indexed-types/should_compile/all.T +++ b/testsuite/tests/indexed-types/should_compile/all.T @@ -278,3 +278,5 @@ test('T12175', normal, compile, ['']) test('T12522', normal, compile, ['']) test('T12522b', normal, compile, ['']) test('T12676', normal, compile, ['']) +test('T12526', normal, compile, ['']) +test('T12538', normal, compile_fail, ['']) diff --git a/testsuite/tests/indexed-types/should_fail/T2544.stderr b/testsuite/tests/indexed-types/should_fail/T2544.stderr index 6375c8f79e..b943db2087 100644 --- a/testsuite/tests/indexed-types/should_fail/T2544.stderr +++ b/testsuite/tests/indexed-types/should_fail/T2544.stderr @@ -1,4 +1,16 @@ +T2544.hs:17:12: error: + • Couldn't match type ‘IxMap r’ with ‘IxMap i1’ + Expected type: IxMap (l :|: r) [Int] + Actual type: BiApp (IxMap l) (IxMap i1) [Int] + NB: ‘IxMap’ is a type function, and may not be injective + The type variable ‘i1’ is ambiguous + • In the expression: BiApp empty empty + In an equation for ‘empty’: empty = BiApp empty empty + In the instance declaration for ‘Ix (l :|: r)’ + • Relevant bindings include + empty :: IxMap (l :|: r) [Int] (bound at T2544.hs:17:4) + T2544.hs:17:18: error: • Couldn't match type ‘IxMap i0’ with ‘IxMap l’ Expected type: IxMap l [Int] @@ -10,15 +22,3 @@ T2544.hs:17:18: error: In an equation for ‘empty’: empty = BiApp empty empty • Relevant bindings include empty :: IxMap (l :|: r) [Int] (bound at T2544.hs:17:4) - -T2544.hs:17:24: error: - • Couldn't match type ‘IxMap i1’ with ‘IxMap r’ - Expected type: IxMap r [Int] - Actual type: IxMap i1 [Int] - NB: ‘IxMap’ is a type function, and may not be injective - The type variable ‘i1’ is ambiguous - • In the second argument of ‘BiApp’, namely ‘empty’ - In the expression: BiApp empty empty - In an equation for ‘empty’: empty = BiApp empty empty - • Relevant bindings include - empty :: IxMap (l :|: r) [Int] (bound at T2544.hs:17:4) diff --git a/testsuite/tests/indexed-types/should_fail/T2627b.stderr b/testsuite/tests/indexed-types/should_fail/T2627b.stderr index 11e1b8e8fd..63f11b97f1 100644 --- a/testsuite/tests/indexed-types/should_fail/T2627b.stderr +++ b/testsuite/tests/indexed-types/should_fail/T2627b.stderr @@ -1,9 +1,9 @@ T2627b.hs:20:24: error: • Occurs check: cannot construct the infinite type: - t0 ~ Dual (Dual t0) + b0 ~ Dual (Dual b0) arising from a use of ‘conn’ - The type variable ‘t0’ is ambiguous + 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 diff --git a/testsuite/tests/indexed-types/should_fail/T3330c.stderr b/testsuite/tests/indexed-types/should_fail/T3330c.stderr index 8526c17f5e..829bca1400 100644 --- a/testsuite/tests/indexed-types/should_fail/T3330c.stderr +++ b/testsuite/tests/indexed-types/should_fail/T3330c.stderr @@ -3,14 +3,14 @@ T3330c.hs:23:43: error: • Couldn't match kind ‘* -> *’ with ‘*’ When matching types f1 :: * -> * - Der f1 x :: * - Expected type: Der ((->) x) (Der f1 x) + f1 x :: * + Expected type: Der ((->) x) (f1 x) Actual type: R f1 • In the first argument of ‘plug’, namely ‘rf’ In the first argument of ‘Inl’, namely ‘(plug rf df x)’ In the expression: Inl (plug rf df x) • Relevant bindings include x :: x (bound at T3330c.hs:23:29) - df :: Der f1 x (bound at T3330c.hs:23:25) + df :: f1 x (bound at T3330c.hs:23:25) rf :: R f1 (bound at T3330c.hs:23:13) plug' :: R f -> Der f x -> x -> f x (bound at T3330c.hs:23:1) diff --git a/testsuite/tests/indexed-types/should_fail/T4179.stderr b/testsuite/tests/indexed-types/should_fail/T4179.stderr index 91244c4ce7..516bdf3802 100644 --- a/testsuite/tests/indexed-types/should_fail/T4179.stderr +++ b/testsuite/tests/indexed-types/should_fail/T4179.stderr @@ -1,13 +1,13 @@ T4179.hs:26:16: error: - • Couldn't match type ‘A3 (x (A2 (FCon x) -> A3 (FCon x)))’ - with ‘A3 (FCon x)’ + • Couldn't match type ‘A2 (x (A2 (FCon x) -> A3 (FCon x)))’ + with ‘A2 (FCon x)’ Expected type: x (A2 (FCon x) -> A3 (FCon x)) -> A2 (FCon x) -> A3 (FCon x) Actual type: x (A2 (FCon x) -> A3 (FCon x)) -> A2 (x (A2 (FCon x) -> A3 (FCon x))) -> A3 (x (A2 (FCon x) -> A3 (FCon x))) - NB: ‘A3’ is a type function, and may not be injective + NB: ‘A2’ is a type function, and may not be injective • In the first argument of ‘foldDoC’, namely ‘op’ In the expression: foldDoC op In an equation for ‘fCon’: fCon = foldDoC op diff --git a/testsuite/tests/indexed-types/should_fail/T6123.stderr b/testsuite/tests/indexed-types/should_fail/T6123.stderr index 3c77040f95..0ae1a5e3c1 100644 --- a/testsuite/tests/indexed-types/should_fail/T6123.stderr +++ b/testsuite/tests/indexed-types/should_fail/T6123.stderr @@ -1,9 +1,9 @@ T6123.hs:10:14: error: - • Occurs check: cannot construct the infinite type: t0 ~ Id t0 + • Occurs check: cannot construct the infinite type: a0 ~ Id a0 arising from a use of ‘cid’ - The type variable ‘t0’ is ambiguous + The type variable ‘a0’ is ambiguous • In the expression: cid undefined In an equation for ‘cundefined’: cundefined = cid undefined • Relevant bindings include - cundefined :: t0 (bound at T6123.hs:10:1) + cundefined :: a0 (bound at T6123.hs:10:1) diff --git a/testsuite/tests/indexed-types/should_fail/T7786.hs b/testsuite/tests/indexed-types/should_fail/T7786.hs index 839a1fb83d..2a5c7f5983 100644 --- a/testsuite/tests/indexed-types/should_fail/T7786.hs +++ b/testsuite/tests/indexed-types/should_fail/T7786.hs @@ -55,17 +55,17 @@ type family Intersect (l :: Inventory a) (r :: Inventory a) :: Inventory a where Intersect l Empty = Empty Intersect (More ls l) r = InterAppend (Intersect ls r) r l -type family InterAppend (l :: Inventory a) - (r :: Inventory a) - (one :: a) +type family InterAppend (l :: Inventory a) + (r :: Inventory a) + (one :: a) :: Inventory a where InterAppend acc Empty one = acc InterAppend acc (More rs one) one = More acc one InterAppend acc (More rs r) one = InterAppend acc rs one -type family BuriedUnder (sub :: Inventory [KeySegment]) - (post :: [KeySegment]) - (inv :: Inventory [KeySegment]) +type family BuriedUnder (sub :: Inventory [KeySegment]) + (post :: [KeySegment]) + (inv :: Inventory [KeySegment]) :: Inventory [KeySegment] where BuriedUnder Empty post inv = inv BuriedUnder (More ps p) post inv = More ((ps `BuriedUnder` post) inv) (p `Under` post) @@ -82,9 +82,23 @@ foo :: Database inv foo db k sub = buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db -} +foogle :: Database inv + -> Sing post + -> Database sub + -> Maybe (Sing (Intersect (BuriedUnder sub post 'Empty) inv)) + +foogle db k sub = return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db) + + addSub :: Database inv -> Sing k -> Database sub -> Maybe (Database ((sub `BuriedUnder` k) inv)) -addSub db k sub = do Nil :: Sing xxx <- return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db) +addSub db k sub = do Nil :: Sing xxx <- foogle db k sub + return $ Sub db k sub + +{- +addSub :: Database inv -> Sing k -> Database sub -> Maybe (Database ((sub `BuriedUnder` k) inv)) +addSub db k sub = do Nil :: Sing xxx <- foogle db sub k -- Nil :: Sing ((sub `BuriedUnder` k) Empty `Intersect` inv) <- return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db) -- Nil :: Sing Empty <- return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db) -- Nil <- return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db) return $ Sub db k sub +-} diff --git a/testsuite/tests/indexed-types/should_fail/T7786.stderr b/testsuite/tests/indexed-types/should_fail/T7786.stderr index ca3e9ecbda..8fdb49bd8e 100644 --- a/testsuite/tests/indexed-types/should_fail/T7786.stderr +++ b/testsuite/tests/indexed-types/should_fail/T7786.stderr @@ -1,29 +1,29 @@ -T7786.hs:86:49: error: +T7786.hs:94:41: error: • Couldn't match type ‘xxx’ with ‘Intersect (BuriedUnder sub k 'Empty) inv’ - Expected type: Sing xxx - Actual type: Sing (Intersect (BuriedUnder sub k 'Empty) inv) - • In the first argument of ‘return’, namely - ‘(buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)’ - In a stmt of a 'do' block: - Nil :: Sing xxx <- return - (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db) + Expected type: Maybe (Sing xxx) + Actual type: Maybe + (Sing (Intersect (BuriedUnder sub k 'Empty) inv)) + • In a stmt of a 'do' block: Nil :: Sing xxx <- foogle db k sub In the expression: - do { Nil :: Sing xxx <- return - (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db); + do { Nil :: Sing xxx <- foogle db k sub; return $ Sub db k sub } + In an equation for ‘addSub’: + addSub db k sub + = do { Nil :: Sing xxx <- foogle db k sub; + return $ Sub db k sub } • Relevant bindings include - sub :: Database sub (bound at T7786.hs:86:13) - k :: Sing k (bound at T7786.hs:86:11) - db :: Database inv (bound at T7786.hs:86:8) + sub :: Database sub (bound at T7786.hs:94:13) + k :: Sing k (bound at T7786.hs:94:11) + db :: Database inv (bound at T7786.hs:94:8) addSub :: Database inv -> Sing k -> Database sub -> Maybe (Database (BuriedUnder sub k inv)) - (bound at T7786.hs:86:1) + (bound at T7786.hs:94:1) -T7786.hs:90:31: error: +T7786.hs:95:31: error: • Could not deduce: Intersect (BuriedUnder sub k 'Empty) inv ~ 'Empty @@ -32,19 +32,18 @@ T7786.hs:90:31: error: bound by a pattern with constructor: Nil :: forall a. Sing 'Empty, in a pattern binding in 'do' block - at T7786.hs:86:22-24 + at T7786.hs:94:22-24 • In the second argument of ‘($)’, namely ‘Sub db k sub’ In a stmt of a 'do' block: return $ Sub db k sub In the expression: - do { Nil :: Sing xxx <- return - (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db); + do { Nil :: Sing xxx <- foogle db k sub; return $ Sub db k sub } • Relevant bindings include - sub :: Database sub (bound at T7786.hs:86:13) - k :: Sing k (bound at T7786.hs:86:11) - db :: Database inv (bound at T7786.hs:86:8) + sub :: Database sub (bound at T7786.hs:94:13) + k :: Sing k (bound at T7786.hs:94:11) + db :: Database inv (bound at T7786.hs:94:8) addSub :: Database inv -> Sing k -> Database sub -> Maybe (Database (BuriedUnder sub k inv)) - (bound at T7786.hs:86:1) + (bound at T7786.hs:94:1) diff --git a/testsuite/tests/indexed-types/should_fail/T8227.stderr b/testsuite/tests/indexed-types/should_fail/T8227.stderr index 6dec5d0191..88f4732df1 100644 --- a/testsuite/tests/indexed-types/should_fail/T8227.stderr +++ b/testsuite/tests/indexed-types/should_fail/T8227.stderr @@ -1,10 +1,11 @@ -T8227.hs:16:44: error: - • Couldn't match expected type ‘Scalar (V (Scalar (V a)))’ - with actual type ‘Scalar (V a)’ - NB: ‘Scalar’ is a type function, and may not be injective - • In the first argument of ‘arcLengthToParam’, namely ‘eps’ - In the expression: arcLengthToParam eps eps +T8227.hs:16:27: error: + • Couldn't match type ‘Scalar (V a)’ + with ‘Scalar (V a) -> Scalar (V a)’ + Expected type: Scalar (V a) + Actual type: Scalar (V (Scalar (V a) -> Scalar (V a))) + -> Scalar (V (Scalar (V a) -> Scalar (V a))) + • In the expression: arcLengthToParam eps eps In an equation for ‘absoluteToParam’: absoluteToParam eps seg = arcLengthToParam eps eps • Relevant bindings include diff --git a/testsuite/tests/partial-sigs/should_compile/T10403.stderr b/testsuite/tests/partial-sigs/should_compile/T10403.stderr index 23c059e720..0588c1b5bc 100644 --- a/testsuite/tests/partial-sigs/should_compile/T10403.stderr +++ b/testsuite/tests/partial-sigs/should_compile/T10403.stderr @@ -60,18 +60,3 @@ T10403.hs:28:8: warning: [-Wdeferred-type-errors (in -Wdefault)] In an equation for ‘app2’: app2 = h2 (H . I) (B ()) • Relevant bindings include app2 :: H (B t) (bound at T10403.hs:28:1) - -T10403.hs:28:20: warning: [-Wdeferred-type-errors (in -Wdefault)] - • Couldn't match type ‘f0’ with ‘B t’ - because type variable ‘t’ would escape its scope - This (rigid, skolem) type variable is bound by - the type signature for: - app2 :: H (B t) - at T10403.hs:27:1-15 - Expected type: f0 () - Actual type: B t () - • In the second argument of ‘h2’, namely ‘(B ())’ - In the expression: h2 (H . I) (B ()) - In an equation for ‘app2’: app2 = h2 (H . I) (B ()) - • Relevant bindings include - app2 :: H (B t) (bound at T10403.hs:28:1) diff --git a/testsuite/tests/perf/compiler/T5837.hs b/testsuite/tests/perf/compiler/T5837.hs index 6ebbd65bd5..0a500fb826 100644 --- a/testsuite/tests/perf/compiler/T5837.hs +++ b/testsuite/tests/perf/compiler/T5837.hs @@ -13,26 +13,35 @@ t = undefined [G] a ~ TF (a,Int) -- a = a_am1 --> [G] TF (a,Int) ~ fsk -- fsk = fsk_am8 + inert [G] fsk ~ a ----> - [G] fsk ~ (TF a, TF Int) +---> reduce + [G] fsk ~ (TF a, TF Int) + inert [G] fsk ~ a ----> - a ~ (TF a, TF Int) +---> substitute for fsk and flatten + [G] TF a ~ fsk1 + [G] TF Int ~ fsk2 + inert [G] fsk ~ a + [G] a ~ (fsk1, fsk2) ----> (attempting to flatten (TF a) so that it does not mention a - TF a ~ fsk2 -inert a ~ (fsk2, TF Int) -inert fsk ~ (fsk2, TF Int) +---> (substitute for a in first constraint) + TF (fsk1, fsk2) ~ fsk1 (C1) + TF Int ~ fsk2 ----> (substitute for a) - TF (fsk2, TF Int) ~ fsk2 inert a ~ (fsk2, TF Int) inert fsk ~ (fsk2, TF Int) + +------- At this point we are stuck because of +-- the recursion in the first constraint C1 +-- Hooray + +-- Before, we reduced C1, which led to a loop + ---> (top-level reduction, re-orient) fsk2 ~ (TF fsk2, TF Int) inert a ~ (fsk2, TF Int) @@ -50,4 +59,4 @@ inert fsk2 ~ (fsk3, TF Int) inert a ~ ((fsk3, TF Int), TF Int) inert fsk ~ ((fsk3, TF Int), TF Int) --}
\ No newline at end of file +-} diff --git a/testsuite/tests/perf/compiler/T5837.stderr b/testsuite/tests/perf/compiler/T5837.stderr deleted file mode 100644 index 324e817947..0000000000 --- a/testsuite/tests/perf/compiler/T5837.stderr +++ /dev/null @@ -1,91 +0,0 @@ - -T5837.hs:8:6: error: - Reduction stack overflow; size = 51 - When simplifying the following type: - TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - a)))))))))))))))))))))))) - ~ (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - a))))))))))))))))))))))))), - TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - (TF - Int)))))))))))))))))))))))))) - 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 - you're sure that type checking should terminate) - In the ambiguity check for ‘t’ - In the type signature: - t :: (a ~ TF (a, Int)) => Int diff --git a/testsuite/tests/perf/compiler/all.T b/testsuite/tests/perf/compiler/all.T index 72c58c7592..7c8f55ab24 100644 --- a/testsuite/tests/perf/compiler/all.T +++ b/testsuite/tests/perf/compiler/all.T @@ -594,7 +594,7 @@ test('T5837', # 2014-12-08: 115905208 Constraint solver perf improvements (esp kick-out) # 2016-04-06: 24199320 (x86/Linux, 64-bit machine) TypeInType - (wordsize(64), 41832056, 10)]) + (wordsize(64), 52597024, 10)]) # sample: 3926235424 (amd64/Linux, 15/2/2012) # 2012-10-02 81879216 # 2012-09-20 87254264 amd64/Linux @@ -615,8 +615,11 @@ test('T5837', # for other optimisations # 2016-09-15 42445672 Linux; fixing #12422 # 2016-09-25 41832056 amd64/Linux, Rework handling of names (D2469) + # 2016-10-25 52597024 amd64/Linux, the test now passes (hooray), and so + # allocates more because it goes right down the + # compilation pipeline ], - compile_fail,['-freduction-depth=50']) + compile, ['-freduction-depth=50']) test('T6048', [ only_ways(['optasm']), diff --git a/testsuite/tests/polykinds/T12444.hs b/testsuite/tests/polykinds/T12444.hs new file mode 100644 index 0000000000..746c6448ef --- /dev/null +++ b/testsuite/tests/polykinds/T12444.hs @@ -0,0 +1,65 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} + +module T12444 where + +data Nat = Zero | Succ Nat + +data SNat (n :: Nat) where + SZero :: SNat Zero + SSucc :: SNat n -> SNat (Succ n) + +type family (:+:) (a :: Nat) (b :: Nat) :: Nat where + m :+: Zero = m + m :+: (Succ n) = Succ (m :+: n) + +foo :: SNat (Succ c) -> SNat b -> SNat (Succ (c :+: b)) +foo _ x = x + + +{- +sadd :: ((Succ n1 :+: n) ~ Succ (n1 :+: n), (Succ n1) ~ m) + => SNat m -> SNat n -> SNat (m :+: n) +sadd SZero n = n +-} + +{- [G] a ~ Succ c + Succ c + b ~ Succ (c+b) + a ~ Zero + +--> + Zero ~ Succ c TyEq + fsk1 ~ Succ fsk2 TyEq + fsk1 ~ (Succ c) + b FunEq + fsk2 ~ c+b FunEq +---- +[W] b ~ a+b ---> b ~ Succ (c+b) + + +Derived + a ~ Succ c + fsk1 ~ Succ fsk2 + b ~ Succ fsk2 + +work (Succ c) + b ~ fsk1 + c+b ~ fsk2 + + +-} + +{- + +[G] a ~ [b] +--> Derived shadow [D] a ~ [b] + When adding this to the model + don't kick out a derived shadow again! + +[G] (a ~ b) --> sc a ~~ b, a ~# b + Silly to then kick out (a~b) and (a~~b) + and rewrite them to (a~a) and (a~~a) + +Insoluble constraint does not halt solving; +indeed derived version stays. somehow +-} diff --git a/testsuite/tests/polykinds/T12444.stderr b/testsuite/tests/polykinds/T12444.stderr new file mode 100644 index 0000000000..0ebd2986cf --- /dev/null +++ b/testsuite/tests/polykinds/T12444.stderr @@ -0,0 +1,16 @@ + +T12444.hs:19:11: error: + • Couldn't match type ‘b’ with ‘'Succ (c :+: b)’ + ‘b’ is a rigid type variable bound by + the type signature for: + foo :: forall (c :: Nat) (b :: Nat). + SNat ('Succ c) -> SNat b -> SNat ('Succ (c :+: b)) + at T12444.hs:18:1-55 + Expected type: SNat ('Succ (c :+: b)) + Actual type: SNat b + • In the expression: x + In an equation for ‘foo’: foo _ x = x + • Relevant bindings include + x :: SNat b (bound at T12444.hs:19:7) + foo :: SNat ('Succ c) -> SNat b -> SNat ('Succ (c :+: b)) + (bound at T12444.hs:19:1) diff --git a/testsuite/tests/polykinds/T9222.stderr b/testsuite/tests/polykinds/T9222.stderr index df97578029..dc1b92c202 100644 --- a/testsuite/tests/polykinds/T9222.stderr +++ b/testsuite/tests/polykinds/T9222.stderr @@ -1,12 +1,12 @@ T9222.hs:13:3: error: - • Couldn't match type ‘b0’ with ‘b’ - ‘b0’ is untouchable + • Couldn't match type ‘c0’ with ‘c’ + ‘c0’ is untouchable inside the constraints: a ~ '(b0, c0) bound by the type of the constructor ‘Want’: a ~ '(b0, c0) => Proxy b0 at T9222.hs:13:3 - ‘b’ is a rigid type variable bound by + ‘c’ is a rigid type variable bound by the type of the constructor ‘Want’: forall i1 j1 (a :: (i1, j1)) (b :: i1) (c :: j1). (a ~ '(b, c) => Proxy b) -> Want a diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T index 6ec2a439e6..0e0d66a676 100644 --- a/testsuite/tests/polykinds/all.T +++ b/testsuite/tests/polykinds/all.T @@ -154,3 +154,4 @@ test('T12055a', normal, compile_fail, ['']) test('T12593', normal, compile_fail, ['']) test('T12668', normal, compile, ['']) test('T12718', normal, compile, ['']) +test('T12444', normal, compile_fail, ['']) diff --git a/testsuite/tests/typecheck/should_compile/Improvement.hs b/testsuite/tests/typecheck/should_compile/Improvement.hs index e7e11901a8..8df81c26a7 100644 --- a/testsuite/tests/typecheck/should_compile/Improvement.hs +++ b/testsuite/tests/typecheck/should_compile/Improvement.hs @@ -1,5 +1,15 @@ {-# LANGUAGE TypeFamilies, FlexibleContexts, MultiParamTypeClasses, FlexibleInstances #-} {-# OPTIONS_GHC -fno-warn-redundant-constraints #-} + +-- This one relies on doing instance reduction +-- on a /derived/ class +-- [W] C (F a0) a0, F a0 ~ Bool +-- Currently (Oct 16) I've disabled this because it seems like +-- overkill. +-- +-- See Note Note [No reduction for Derived class constraints] +-- in TcInteract + module Foo where type family F a @@ -14,5 +24,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/T6018.hs b/testsuite/tests/typecheck/should_compile/T6018.hs index 5fdb03b220..91a67c5e57 100644 --- a/testsuite/tests/typecheck/should_compile/T6018.hs +++ b/testsuite/tests/typecheck/should_compile/T6018.hs @@ -8,6 +8,38 @@ module T6018 where +{- +barapp2 :: Int +barapp2 = bar 1 + +bar :: Bar a -> Bar a +bar x = x + +type family Bar a = r | r -> a where + Bar Int = Bool + Bar Bool = Int + Bar Bool = Char + +type family F a b c = (result :: k) | result -> a b c + +type family FClosed a b c = result | result -> a b c where + FClosed Int Char Bool = Bool + FClosed Char Bool Int = Int + FClosed Bool Int Char = Char +-} +{- +g6_use :: [Char] +g6_use = g6_id "foo" + +g6_id :: G6 a -> G6 a +g6_id x = x + +type family G6 a = r | r -> a +type instance G6 [a] = [Gi a] +type family Gi a = r | r -> a +type instance Gi Int = Char +-} + import T6018a -- defines G, identical to F type family F a b c = (result :: k) | result -> a b c diff --git a/testsuite/tests/typecheck/should_compile/T6018.stderr b/testsuite/tests/typecheck/should_compile/T6018.stderr index 91d6b300d6..57eed50c46 100644 --- a/testsuite/tests/typecheck/should_compile/T6018.stderr +++ b/testsuite/tests/typecheck/should_compile/T6018.stderr @@ -2,10 +2,10 @@ [2 of 3] Compiling T6018a (.hs -> .o) [3 of 3] Compiling T6018 (.hs -> .o) -T6018.hs:75:5: warning: +T6018.hs:107:5: warning: Type family instance equation is overlapped: - Foo Bool = Bool -- Defined at T6018.hs:75:5 + Foo Bool = Bool -- Defined at T6018.hs:107:5 -T6018.hs:82:5: warning: +T6018.hs:114:5: warning: Type family instance equation is overlapped: - Bar Bool = Char -- Defined at T6018.hs:82:5 + Bar Bool = Char -- Defined at T6018.hs:114:5 diff --git a/testsuite/tests/typecheck/should_fail/ContextStack2.hs b/testsuite/tests/typecheck/should_fail/ContextStack2.hs index f3f93eb912..d66103c880 100644 --- a/testsuite/tests/typecheck/should_fail/ContextStack2.hs +++ b/testsuite/tests/typecheck/should_fail/ContextStack2.hs @@ -5,6 +5,8 @@ module ContextStack2 where type family TF a :: * type instance TF (a,b) = (TF a, TF b) +-- Succeeds with new approach to fuvs +-- Aug 2016 t :: (a ~ TF (a,Int)) => Int t = undefined diff --git a/testsuite/tests/typecheck/should_fail/ContextStack2.stderr b/testsuite/tests/typecheck/should_fail/ContextStack2.stderr deleted file mode 100644 index f76d1f486c..0000000000 --- a/testsuite/tests/typecheck/should_fail/ContextStack2.stderr +++ /dev/null @@ -1,13 +0,0 @@ - -ContextStack2.hs:8:6: error: - • Reduction stack overflow; size = 11 - When simplifying the following type: - TF (TF (TF (TF (TF a)))) - ~ (TF (TF (TF (TF (TF (TF a))))), TF (TF (TF (TF (TF (TF Int)))))) - 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 - you're sure that type checking should terminate) - • In the ambiguity check for ‘t’ - In the type signature: - t :: (a ~ TF (a, Int)) => Int diff --git a/testsuite/tests/typecheck/should_fail/Makefile b/testsuite/tests/typecheck/should_fail/Makefile index 9101fbd40a..f994435d03 100644 --- a/testsuite/tests/typecheck/should_fail/Makefile +++ b/testsuite/tests/typecheck/should_fail/Makefile @@ -1,3 +1,8 @@ TOP=../../.. include $(TOP)/mk/boilerplate.mk include $(TOP)/mk/test.mk + +.PHONEY: foo + +foo: + echo hello diff --git a/testsuite/tests/typecheck/should_fail/T5691.stderr b/testsuite/tests/typecheck/should_fail/T5691.stderr index 9d4e587166..ad5c7e452f 100644 --- a/testsuite/tests/typecheck/should_fail/T5691.stderr +++ b/testsuite/tests/typecheck/should_fail/T5691.stderr @@ -1,12 +1,12 @@ -T5691.hs:15:24: error: +T5691.hs:14:9: error: • Couldn't match type ‘p’ with ‘PrintRuleInterp’ Expected type: PrintRuleInterp a Actual type: p a - • In the first argument of ‘printRule_’, namely ‘f’ - In the second argument of ‘($)’, namely ‘printRule_ f’ - In the expression: MkPRI $ printRule_ f - • Relevant bindings include f :: p a (bound at T5691.hs:14:9) + • When checking that the pattern signature: p a + fits the type of its context: PrintRuleInterp a + In the pattern: f :: p a + In an equation for ‘test’: test (f :: p a) = MkPRI $ printRule_ f T5691.hs:24:10: error: • No instance for (Alternative RecDecParser) diff --git a/testsuite/tests/typecheck/should_fail/T5853.stderr b/testsuite/tests/typecheck/should_fail/T5853.stderr index 62385ea1df..719895af6c 100644 --- a/testsuite/tests/typecheck/should_fail/T5853.stderr +++ b/testsuite/tests/typecheck/should_fail/T5853.stderr @@ -1,22 +1,22 @@ T5853.hs:15:46: error: - • Could not deduce: Subst (Subst t2 t) t1 ~ Subst t2 t1 + • Could not deduce: Subst (Subst fa a) b ~ Subst fa b arising from a use of ‘<$>’ - from the context: (F t2, - Elem t2 ~ Elem t2, - Elem (Subst t2 t1) ~ t1, - Subst t2 t1 ~ Subst t2 t1, - Subst (Subst t2 t1) (Elem t2) ~ t2, - F (Subst t2 t), - Elem (Subst t2 t) ~ t, - Elem t2 ~ Elem t2, - Subst (Subst t2 t) (Elem t2) ~ t2, - Subst t2 t ~ Subst t2 t) + from the context: (F fa, + Elem fa ~ Elem fa, + Elem (Subst fa b) ~ b, + Subst fa b ~ Subst fa b, + Subst (Subst fa b) (Elem fa) ~ fa, + F (Subst fa a), + Elem (Subst fa a) ~ a, + Elem fa ~ Elem fa, + Subst (Subst fa a) (Elem fa) ~ fa, + Subst fa a ~ Subst fa a) bound by the RULE "map/map" at T5853.hs:15:2-57 NB: ‘Subst’ is a type function, and may not be injective • In the expression: (f . g) <$> xs When checking the transformation rule "map/map" • Relevant bindings include - f :: Elem t2 -> t1 (bound at T5853.hs:15:19) - g :: t -> Elem t2 (bound at T5853.hs:15:21) - xs :: Subst t2 t (bound at T5853.hs:15:23) + f :: Elem fa -> b (bound at T5853.hs:15:19) + g :: a -> Elem fa (bound at T5853.hs:15:21) + xs :: Subst fa a (bound at T5853.hs:15:23) diff --git a/testsuite/tests/typecheck/should_fail/T8450.stderr b/testsuite/tests/typecheck/should_fail/T8450.stderr index 8ba84a76f1..7503f4d37e 100644 --- a/testsuite/tests/typecheck/should_fail/T8450.stderr +++ b/testsuite/tests/typecheck/should_fail/T8450.stderr @@ -1,11 +1,15 @@ -T8450.hs:8:7: error: - • Couldn't match expected type ‘a’ with actual type ‘()’ +T8450.hs:8:20: error: + • Couldn't match type ‘a’ with ‘Bool’ ‘a’ is a rigid type variable bound by the type signature for: run :: forall a. a at T8450.hs:7:1-18 - • In the expression: runEffect $ (undefined :: Either a ()) + Expected type: Either Bool () + Actual type: Either a () + • In the second argument of ‘($)’, namely + ‘(undefined :: Either a ())’ + In the expression: runEffect $ (undefined :: Either a ()) In an equation for ‘run’: run = runEffect $ (undefined :: Either a ()) • Relevant bindings include run :: a (bound at T8450.hs:8:1) diff --git a/testsuite/tests/typecheck/should_fail/T9260.stderr b/testsuite/tests/typecheck/should_fail/T9260.stderr index 0773da2bf5..f55f474904 100644 --- a/testsuite/tests/typecheck/should_fail/T9260.stderr +++ b/testsuite/tests/typecheck/should_fail/T9260.stderr @@ -1,7 +1,8 @@ -T9260.hs:12:8: error: - • Couldn't match type ‘2’ with ‘1’ - Expected type: Fin 1 - Actual type: Fin (1 + 1) - • In the expression: Fsucc Fzero +T9260.hs:12:14: error: + • Couldn't match type ‘1’ with ‘0’ + Expected type: Fin 0 + Actual type: Fin (0 + 1) + • In the first argument of ‘Fsucc’, namely ‘Fzero’ + In the expression: Fsucc Fzero In an equation for ‘test’: test = Fsucc Fzero diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T index 4d58d4f0de..6f99a94ff4 100644 --- a/testsuite/tests/typecheck/should_fail/all.T +++ b/testsuite/tests/typecheck/should_fail/all.T @@ -336,7 +336,7 @@ test('T8428', normal, compile_fail, ['']) test('T8450', normal, compile_fail, ['']) test('T8514', normal, compile_fail, ['']) test('ContextStack1', normal, compile_fail, ['-freduction-depth=10']) -test('ContextStack2', normal, compile_fail, ['-freduction-depth=10']) +test('ContextStack2', normal, compile, ['']) test('T8570', extra_clean(['T85570a.o', 'T8570a.hi','T85570b.o', 'T8570b.hi']), multimod_compile_fail, ['T8570', '-v0']) test('T8603', normal, compile_fail, ['']) |