[Git][ghc/ghc][wip/T26003] 4 commits: Fix infelicities in the Specialiser

Simon Peyton Jones pushed to branch wip/T26003 at Glasgow Haskell Compiler / GHC Commits: ce616f49 by Simon Peyton Jones at 2025-04-27T21:10:25+01:00 Fix infelicities in the Specialiser On the way to #23109 (unary classes) I discovered some infelicities (or maybe tiny bugs, I forget) in the type-class specialiser. I also tripped over #25965, an outright bug in the rule matcher Specifically: * Refactor: I enhanced `wantCallsFor`, whih previously always said `True`, to discard calls of class-ops, data constructors etc. This is a bit more efficient; and it means we don't need to worry about filtering them out later. * Fix: I tidied up some tricky logic that eliminated redundant specialisations. It wasn't working correctly. See the expanded Note [Specialisations already covered], and (MP3) in Note [Specialising polymorphic dictionaries]. See also the new top-level `alreadyCovered` function, which now goes via `GHC.Core.Rules.ruleLhsIsMoreSpecific` I also added a useful Note [The (CI-KEY) invariant] * Fix #25965: fixed a tricky bug in the `go_fam_fam` in `GHC.Core.Unify.uVarOrFam`, which allows matching to succeed without binding all type varibles. I enhanced Note [Apartness and type families] some more * #25703. This ticket "just works" with -fpolymorphic-specialisation; but I was surprised that it worked! In this MR I added documentation to Note [Interesting dictionary arguments] to explain; and tests to ensure it stays fixed. - - - - - 22d11fa8 by Simon Peyton Jones at 2025-04-28T18:05:19-04:00 Track rewriter sets more accurately in constraint solving The key change, which fixed #25440, is to call `recordRewriter` in GHC.Tc.Solver.Rewrite.rewrite_exact_fam_app. This missing call meant that we were secretly rewriting a Wanted with a Wanted, but not really noticing; and that led to a very bad error message, as you can see in the ticket. But of course that led me into rabbit hole of other refactoring around the RewriteSet code: * Improve Notes [Wanteds rewrite Wanteds] * Zonk the RewriterSet in `zonkCtEvidence` rather than only in GHC.Tc.Errors. This is tidier anyway (e.g. de-clutters debug output), and helps with the next point. * In GHC.Tc.Solver.Equality.inertsCanDischarge, don't replace a constraint with no rewriters with an equal constraint that has many. See See (CE4) in Note [Combining equalities] * Move zonkRewriterSet and friends from GHC.Tc.Zonk.Type into GHC.Tc.Zonk.TcType, where they properly belong. A handful of tests get better error messages. For some reason T24984 gets 12% less compiler allocation -- good Metric Decrease: T24984 - - - - - 4ab20fe4 by Simon Peyton Jones at 2025-04-29T09:36:41+01:00 Wip on #26003 - - - - - c31925a1 by Simon Peyton Jones at 2025-04-29T10:04:02+01:00 Wibbles - - - - - 27 changed files: - compiler/GHC/Core/Coercion.hs - compiler/GHC/Core/Opt/Specialise.hs - compiler/GHC/Core/Rules.hs - compiler/GHC/Core/Unify.hs - compiler/GHC/Tc/Errors.hs - compiler/GHC/Tc/Solver/Default.hs - compiler/GHC/Tc/Solver/Equality.hs - compiler/GHC/Tc/Solver/InertSet.hs - compiler/GHC/Tc/Solver/Monad.hs - compiler/GHC/Tc/Solver/Rewrite.hs - compiler/GHC/Tc/Types/Constraint.hs - compiler/GHC/Tc/Utils/TcMType.hs - compiler/GHC/Tc/Utils/Unify.hs - compiler/GHC/Tc/Zonk/TcType.hs - compiler/GHC/Tc/Zonk/Type.hs - compiler/GHC/Types/Basic.hs - testsuite/tests/indexed-types/should_fail/T3330c.stderr - testsuite/tests/indexed-types/should_fail/T4174.stderr - testsuite/tests/indexed-types/should_fail/T8227.stderr - + testsuite/tests/simplCore/should_compile/T25703.hs - + testsuite/tests/simplCore/should_compile/T25703.stderr - + testsuite/tests/simplCore/should_compile/T25703a.hs - + testsuite/tests/simplCore/should_compile/T25703a.stderr - + testsuite/tests/simplCore/should_compile/T25965.hs - testsuite/tests/simplCore/should_compile/all.T - testsuite/tests/typecheck/should_compile/T25266a.stderr - testsuite/tests/typecheck/should_fail/T18851.stderr Changes: ===================================== compiler/GHC/Core/Coercion.hs ===================================== @@ -120,7 +120,7 @@ module GHC.Core.Coercion ( multToCo, mkRuntimeRepCo, - hasCoercionHoleTy, hasCoercionHoleCo, hasThisCoercionHoleTy, + hasHeteroKindCoercionHoleTy, hasHeteroKindCoercionHoleCo, setCoHoleType ) where @@ -2795,24 +2795,12 @@ has_co_hole_co :: Coercion -> Monoid.Any -- | Is there a hetero-kind coercion hole in this type? -- (That is, a coercion hole with ch_hetero_kind=True.) -- See wrinkle (EIK2) of Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Equality -hasCoercionHoleTy :: Type -> Bool -hasCoercionHoleTy = Monoid.getAny . has_co_hole_ty +hasHeteroKindCoercionHoleTy :: Type -> Bool +hasHeteroKindCoercionHoleTy = Monoid.getAny . has_co_hole_ty -- | Is there a hetero-kind coercion hole in this coercion? -hasCoercionHoleCo :: Coercion -> Bool -hasCoercionHoleCo = Monoid.getAny . has_co_hole_co - -hasThisCoercionHoleTy :: Type -> CoercionHole -> Bool -hasThisCoercionHoleTy ty hole = Monoid.getAny (f ty) - where - (f, _, _, _) = foldTyCo folder () - - folder = TyCoFolder { tcf_view = noView - , tcf_tyvar = const2 (Monoid.Any False) - , tcf_covar = const2 (Monoid.Any False) - , tcf_hole = \ _ h -> Monoid.Any (getUnique h == getUnique hole) - , tcf_tycobinder = const2 - } +hasHeteroKindCoercionHoleCo :: Coercion -> Bool +hasHeteroKindCoercionHoleCo = Monoid.getAny . has_co_hole_co -- | Set the type of a 'CoercionHole' setCoHoleType :: CoercionHole -> Type -> CoercionHole ===================================== compiler/GHC/Core/Opt/Specialise.hs ===================================== @@ -1243,14 +1243,15 @@ specExpr env (Let bind body) -- Note [Fire rules in the specialiser] fireRewriteRules :: SpecEnv -> InExpr -> [OutExpr] -> (InExpr, [OutExpr]) fireRewriteRules env (Var f) args - | Just (rule, expr) <- specLookupRule env f args InitialPhase (getRules (se_rules env) f) + | let rules = getRules (se_rules env) f + , Just (rule, expr) <- specLookupRule env f args activeInInitialPhase rules , let rest_args = drop (ruleArity rule) args -- See Note [Extra args in the target] zapped_subst = Core.zapSubst (se_subst env) expr' = simpleOptExprWith defaultSimpleOpts zapped_subst expr -- simplOptExpr needed because lookupRule returns -- (\x y. rhs) arg1 arg2 - , (fun, args) <- collectArgs expr' - = fireRewriteRules env fun (args++rest_args) + , (fun', args') <- collectArgs expr' + = fireRewriteRules env fun' (args'++rest_args) fireRewriteRules _ fun args = (fun, args) -------------- @@ -1620,7 +1621,7 @@ specCalls :: Bool -- True => specialising imported fn -- This function checks existing rules, and does not create -- duplicate ones. So the caller does not need to do this filtering. --- See 'already_covered' +-- See `alreadyCovered` type SpecInfo = ( [CoreRule] -- Specialisation rules , [(Id,CoreExpr)] -- Specialised definition @@ -1644,15 +1645,13 @@ specCalls spec_imp env existing_rules calls_for_me fn rhs = -- pprTrace "specCalls: some" (vcat -- [ text "function" <+> ppr fn - -- , text "calls:" <+> ppr calls_for_me - -- , text "subst" <+> ppr (se_subst env) ]) $ + -- , text "calls:" <+> ppr calls_for_me + -- , text "subst" <+> ppr (se_subst env) ]) $ foldlM spec_call ([], [], emptyUDs) calls_for_me | otherwise -- No calls or RHS doesn't fit our preconceptions - = warnPprTrace (not (exprIsTrivial rhs) && notNull calls_for_me && not (isClassOpId fn)) + = warnPprTrace (not (exprIsTrivial rhs) && notNull calls_for_me) "Missed specialisation opportunity for" (ppr fn $$ trace_doc) $ - -- isClassOpId: class-op Ids never inline; we specialise them - -- through fireRewriteRules. So don't complain about missed opportunities -- Note [Specialisation shape] -- pprTrace "specCalls: none" (ppr fn <+> ppr calls_for_me) $ return ([], [], emptyUDs) @@ -1664,6 +1663,10 @@ specCalls spec_imp env existing_rules calls_for_me fn rhs fn_unf = realIdUnfolding fn -- Ignore loop-breaker-ness here inl_prag = idInlinePragma fn inl_act = inlinePragmaActivation inl_prag + is_active = isActive (beginPhase inl_act) :: Activation -> Bool + -- is_active: inl_act is the activation we are going to put in the new + -- SPEC rule; so we want to see if it is covered by another rule with + -- that same activation. is_local = isLocalId fn is_dfun = isDFunId fn dflags = se_dflags env @@ -1674,16 +1677,6 @@ specCalls spec_imp env existing_rules calls_for_me fn rhs (rhs_bndrs, rhs_body) = collectBindersPushingCo rhs -- See Note [Account for casts in binding] - already_covered :: SpecEnv -> [CoreRule] -> [CoreExpr] -> Bool - already_covered env new_rules args -- Note [Specialisations already covered] - = isJust (specLookupRule env fn args (beginPhase inl_act) - (new_rules ++ existing_rules)) - -- Rules: we look both in the new_rules (generated by this invocation - -- of specCalls), and in existing_rules (passed in to specCalls) - -- inl_act: is the activation we are going to put in the new SPEC - -- rule; so we want to see if it is covered by another rule with - -- that same activation. - ---------------------------------------------------------- -- Specialise to one particular call pattern spec_call :: SpecInfo -- Accumulating parameter @@ -1717,8 +1710,12 @@ specCalls spec_imp env existing_rules calls_for_me fn rhs -- , ppr dx_binds ]) $ -- return () + ; let all_rules = rules_acc ++ existing_rules + -- all_rules: we look both in the rules_acc (generated by this invocation + -- of specCalls), and in existing_rules (passed in to specCalls) ; if not useful -- No useful specialisation - || already_covered rhs_env2 rules_acc rule_lhs_args + || alreadyCovered rhs_env2 rule_bndrs fn rule_lhs_args is_active all_rules + -- See (SC1) in Note [Specialisations already covered] then return spec_acc else do { -- Run the specialiser on the specialised RHS @@ -1780,7 +1777,7 @@ specCalls spec_imp env existing_rules calls_for_me fn rhs spec_fn_details = case idDetails fn of JoinId join_arity _ -> JoinId (join_arity - join_arity_decr) Nothing - DFunId is_nt -> DFunId is_nt + DFunId unary -> DFunId unary _ -> VanillaId ; spec_fn <- newSpecIdSM (idName fn) spec_fn_ty spec_fn_details spec_fn_info @@ -1804,6 +1801,8 @@ specCalls spec_imp env existing_rules calls_for_me fn rhs , ppr spec_fn <+> dcolon <+> ppr spec_fn_ty , ppr rhs_bndrs, ppr call_args , ppr spec_rule + , text "acc" <+> ppr rules_acc + , text "existing" <+> ppr existing_rules ] ; -- pprTrace "spec_call: rule" _rule_trace_doc @@ -1812,19 +1811,35 @@ specCalls spec_imp env existing_rules calls_for_me fn rhs , spec_uds `thenUDs` uds_acc ) } } +alreadyCovered :: SpecEnv + -> [Var] -> Id -> [CoreExpr] -- LHS of possible new rule + -> (Activation -> Bool) -- Which rules are active + -> [CoreRule] -> Bool +-- Note [Specialisations already covered] esp (SC2) +alreadyCovered env bndrs fn args is_active rules + = case specLookupRule env fn args is_active rules of + Nothing -> False + Just (rule, _) + | isAutoRule rule -> -- Discard identical rules + -- We know that (fn args) is an instance of RULE + -- Check if RULE is an instance of (fn args) + ruleLhsIsMoreSpecific in_scope bndrs args rule + | otherwise -> True -- User rules dominate + where + in_scope = substInScopeSet (se_subst env) + -- Convenience function for invoking lookupRule from Specialise -- The SpecEnv's InScopeSet should include all the Vars in the [CoreExpr] specLookupRule :: SpecEnv -> Id -> [CoreExpr] - -> CompilerPhase -- Look up rules as if we were in this phase + -> (Activation -> Bool) -- Which rules are active -> [CoreRule] -> Maybe (CoreRule, CoreExpr) -specLookupRule env fn args phase rules +specLookupRule env fn args is_active rules = lookupRule ropts in_scope_env is_active fn args rules where dflags = se_dflags env in_scope = substInScopeSet (se_subst env) in_scope_env = ISE in_scope (whenActiveUnfoldingFun is_active) ropts = initRuleOpts dflags - is_active = isActive phase {- Note [Specialising DFuns] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2323,21 +2338,24 @@ This plan is implemented in the Rec case of specBindItself. Note [Specialisations already covered] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We obviously don't want to generate two specialisations for the same -argument pattern. There are two wrinkles - -1. We do the already-covered test in specDefn, not when we generate -the CallInfo in mkCallUDs. We used to test in the latter place, but -we now iterate the specialiser somewhat, and the Id at the call site -might therefore not have all the RULES that we can see in specDefn - -2. What about two specialisations where the second is an *instance* -of the first? If the more specific one shows up first, we'll generate -specialisations for both. If the *less* specific one shows up first, -we *don't* currently generate a specialisation for the more specific -one. (See the call to lookupRule in already_covered.) Reasons: - (a) lookupRule doesn't say which matches are exact (bad reason) - (b) if the earlier specialisation is user-provided, it's - far from clear that we should auto-specialise further +argument pattern. Wrinkles + +(SC1) We do the already-covered test in specDefn, not when we generate + the CallInfo in mkCallUDs. We used to test in the latter place, but + we now iterate the specialiser somewhat, and the Id at the call site + might therefore not have all the RULES that we can see in specDefn + +(SC2) What about two specialisations where the second is an *instance* + of the first? It's a bit arbitrary, but here's what we do: + * If the existing one is user-specified, via a SPECIALISE pragma, we + suppress the further specialisation. + * If the existing one is auto-generated, we generate a second RULE + for the more specialised version. + The latter is important because we don't want the accidental order + of calls to determine what specialisations we generate. + +(SC3) Annoyingly, we /also/ eliminate duplicates in `filterCalls`. + See (MP3) in Note [Specialising polymorphic dictionaries] Note [Auto-specialisation and RULES] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2800,12 +2818,10 @@ non-dictionary bindings too. Note [Specialising polymorphic dictionaries] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - Note June 2023: This has proved to be quite a tricky optimisation to get right see (#23469, #23109, #21229, #23445) so it is now guarded by a flag `-fpolymorphic-specialisation`. - Consider class M a where { foo :: a -> Int } @@ -2845,11 +2861,26 @@ Here are the moving parts: function. (MP3) If we have f :: forall m. Monoid m => blah, and two calls - (f @(Endo b) (d :: Monoid (Endo b)) - (f @(Endo (c->c)) (d :: Monoid (Endo (c->c))) + (f @(Endo b) (d1 :: Monoid (Endo b)) + (f @(Endo (c->c)) (d2 :: Monoid (Endo (c->c))) we want to generate a specialisation only for the first. The second is just a substitution instance of the first, with no greater specialisation. - Hence the call to `remove_dups` in `filterCalls`. + Hence the use of `removeDupCalls` in `filterCalls`. + + You might wonder if `d2` might be more specialised than `d1`; but no. + This `removeDupCalls` thing is at the definition site of `f`, and both `d1` + and `d2` are in scope. So `d1` is simply more polymorphic than `d2`, but + is just as specialised. + + This distinction is sadly lost once we build a RULE, so `alreadyCovered` + can't be so clever. E.g if we have an existing RULE + forall @a (d1:Ord Int) (d2: Eq a). f @a @Int d1 d2 = ... + and a putative new rule + forall (d1:Ord Int) (d2: Eq Int). f @Int @Int d1 d2 = ... + we /don't/ want the existing rule to subsume the new one. + + So we sadly put up with having two rather different places where we + eliminate duplicates: `alreadyCovered` and `removeDupCalls`. All this arose in #13873, in the unexpected form that a SPECIALISE pragma made the program slower! The reason was that the specialised @@ -2947,16 +2978,29 @@ data CallInfoSet = CIS Id (Bag CallInfo) -- The list of types and dictionaries is guaranteed to -- match the type of f -- The Bag may contain duplicate calls (i.e. f @T and another f @T) - -- These dups are eliminated by already_covered in specCalls + -- These dups are eliminated by alreadyCovered in specCalls data CallInfo - = CI { ci_key :: [SpecArg] -- All arguments + = CI { ci_key :: [SpecArg] -- Arguments of the call + -- See Note [The (CI-KEY) invariant] + , ci_fvs :: IdSet -- Free Ids of the ci_key call -- /not/ including the main id itself, of course -- NB: excluding tyvars: -- See Note [Specialising polymorphic dictionaries] } +{- Note [The (CI-KEY) invariant] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Invariant (CI-KEY): + In the `ci_key :: [SpecArg]` field of `CallInfo`, + * The list is non-empty + * The least element is always a `SpecDict` + +In this way the RULE has as few args as possible, which broadens its +applicability, since rules only fire when saturated. +-} + type DictExpr = CoreExpr ciSetFilter :: (CallInfo -> Bool) -> CallInfoSet -> CallInfoSet @@ -3045,10 +3089,7 @@ mkCallUDs' env f args ci_key :: [SpecArg] ci_key = dropWhileEndLE (not . isSpecDict) $ zipWith mk_spec_arg args pis - -- Drop trailing args until we get to a SpecDict - -- In this way the RULE has as few args as possible, - -- which broadens its applicability, since rules only - -- fire when saturated + -- Establish (CI-KEY): drop trailing args until we get to a SpecDict mk_spec_arg :: OutExpr -> PiTyBinder -> SpecArg mk_spec_arg arg (Named bndr) @@ -3086,34 +3127,76 @@ site, so we only look through ticks that RULE matching looks through -} wantCallsFor :: SpecEnv -> Id -> Bool -wantCallsFor _env _f = True - -- We could reduce the size of the UsageDetails by being less eager - -- about collecting calls for LocalIds: there is no point for - -- ones that are lambda-bound. We can't decide this by looking at - -- the (absence of an) unfolding, because unfoldings for local - -- functions are discarded by cloneBindSM, so no local binder will - -- have an unfolding at this stage. We'd have to keep a candidate - -- set of let-binders. - -- - -- Not many lambda-bound variables have dictionary arguments, so - -- this would make little difference anyway. - -- - -- For imported Ids we could check for an unfolding, but we have to - -- do so anyway in canSpecImport, and it seems better to have it - -- all in one place. So we simply collect usage info for imported - -- overloaded functions. - -{- Note [Interesting dictionary arguments] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider this - \a.\d:Eq a. let f = ... in ...(f d)... -There really is not much point in specialising f wrt the dictionary d, -because the code for the specialised f is not improved at all, because -d is lambda-bound. We simply get junk specialisations. - -What is "interesting"? Just that it has *some* structure. But what about -variables? We look in the variable's /unfolding/. And that means -that we must be careful to ensure that dictionaries have unfoldings, +-- See Note [wantCallsFor] +wantCallsFor _env f + = case idDetails f of + RecSelId {} -> False + DataConWorkId {} -> False + DataConWrapId {} -> False + ClassOpId {} -> False + PrimOpId {} -> False + FCallId {} -> False + TickBoxOpId {} -> False + CoVarId {} -> False + + DFunId {} -> True + VanillaId {} -> True + JoinId {} -> True + WorkerLikeId {} -> True + RepPolyId {} -> True + +{- Note [wantCallsFor] +~~~~~~~~~~~~~~~~~~~~~~ +`wantCallsFor env f` says whether the Specialiser should collect calls for +function `f`; other thing being equal, the fewer calls we collect the better. It +is False for things we can't specialise: + +* ClassOpId: never inline and we don't have a defn to specialise; we specialise + them through fireRewriteRules. +* PrimOpId: are never overloaded +* Data constructors: we never specialise them + +We could reduce the size of the UsageDetails by being less eager about +collecting calls for some LocalIds: there is no point for ones that are +lambda-bound. We can't decide this by looking at the (absence of an) unfolding, +because unfoldings for local functions are discarded by cloneBindSM, so no local +binder will have an unfolding at this stage. We'd have to keep a candidate set +of let-binders. + +Not many lambda-bound variables have dictionary arguments, so this would make +little difference anyway. + +For imported Ids we could check for an unfolding, but we have to do so anyway in +canSpecImport, and it seems better to have it all in one place. So we simply +collect usage info for imported overloaded functions. + +Note [Interesting dictionary arguments] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +In `mkCallUDs` we only use `SpecDict` for dictionaries of which +`interestingDict` holds. Otherwise we use `UnspecArg`. Two reasons: + +* Consider this + \a.\d:Eq a. let f = ... in ...(f d)... + There really is not much point in specialising f wrt the dictionary d, + because the code for the specialised f is not improved at all, because + d is lambda-bound. We simply get junk specialisations. + +* Consider this (#25703): + f :: (Eq a, Show b) => a -> b -> INt + goo :: forall x. (Eq x) => x -> blah + goo @x (d:Eq x) (arg:x) = ...(f @x @Int d $fShowInt)... + If we built a `ci_key` with a (SpecDict d) for `d`, we would end up + discarding the call at the `\d`. But if we use `UnspecArg` for that + uninteresting `d`, we'll get a `ci_key` of + f @x @Int UnspecArg (SpecDict $fShowInt) + and /that/ can float out to f's definition and specialise nicely. + Hooray. (NB: the call can float only if `-fpolymorphic-specialisation` + is on; otherwise it'll be trapped by the `\@x -> ...`.)( + +What is "interesting"? (See `interestingDict`.) Just that it has *some* +structure. But what about variables? We look in the variable's /unfolding/. +And that means that we must be careful to ensure that dictionaries /have/ +unfoldings, * cloneBndrSM discards non-Stable unfoldings * specBind updates the unfolding after specialisation @@ -3159,7 +3242,7 @@ Now `f` turns into: meth @a dc .... When we specialise `f`, at a=Int say, that superclass selection can -nfire (via rewiteClassOps), but that info (that 'dc' is now a +fire (via rewiteClassOps), but that info (that 'dc' is now a particular dictionary `C`, of type `C Int`) must be available to the call `meth @a dc`, so that we can fire the `meth` class-op, and thence specialise `wombat`. @@ -3286,7 +3369,11 @@ dumpUDs :: [CoreBndr] -> UsageDetails -> (UsageDetails, OrdList DictBind) -- Used at a lambda or case binder; just dump anything mentioning the binder dumpUDs bndrs uds@(MkUD { ud_binds = orig_dbs, ud_calls = orig_calls }) | null bndrs = (uds, nilOL) -- Common in case alternatives - | otherwise = -- pprTrace "dumpUDs" (ppr bndrs $$ ppr free_uds $$ ppr dump_dbs) $ + | otherwise = -- pprTrace "dumpUDs" (vcat + -- [ text "bndrs" <+> ppr bndrs + -- , text "uds" <+> ppr uds + -- , text "free_uds" <+> ppr free_uds + -- , text "dump-dbs" <+> ppr dump_dbs ]) $ (free_uds, dump_dbs) where free_uds = uds { ud_binds = free_dbs, ud_calls = free_calls } @@ -3325,20 +3412,17 @@ callsForMe fn uds@MkUD { ud_binds = orig_dbs, ud_calls = orig_calls } calls_for_me = case lookupDVarEnv orig_calls fn of Nothing -> [] Just cis -> filterCalls cis orig_dbs - -- filterCalls: drop calls that (directly or indirectly) - -- refer to fn. See Note [Avoiding loops (DFuns)] ---------------------- filterCalls :: CallInfoSet -> FloatedDictBinds -> [CallInfo] --- Remove dominated calls (Note [Specialising polymorphic dictionaries]) --- and loopy DFuns (Note [Avoiding loops (DFuns)]) +-- Remove +-- (a) dominated calls: (MP3) in Note [Specialising polymorphic dictionaries] +-- (b) loopy DFuns: Note [Avoiding loops (DFuns)] filterCalls (CIS fn call_bag) (FDB { fdb_binds = dbs }) - | isDFunId fn -- Note [Avoiding loops (DFuns)] applies only to DFuns - = filter ok_call de_dupd_calls - | otherwise -- Do not apply it to non-DFuns - = de_dupd_calls -- See Note [Avoiding loops (non-DFuns)] + | isDFunId fn = filter ok_call de_dupd_calls -- Deals with (b) + | otherwise = de_dupd_calls where - de_dupd_calls = remove_dups call_bag + de_dupd_calls = removeDupCalls call_bag -- Deals with (a) dump_set = foldl' go (unitVarSet fn) dbs -- This dump-set could also be computed by splitDictBinds @@ -3352,10 +3436,10 @@ filterCalls (CIS fn call_bag) (FDB { fdb_binds = dbs }) ok_call (CI { ci_fvs = fvs }) = fvs `disjointVarSet` dump_set -remove_dups :: Bag CallInfo -> [CallInfo] +removeDupCalls :: Bag CallInfo -> [CallInfo] -- Calls involving more generic instances beat more specific ones. -- See (MP3) in Note [Specialising polymorphic dictionaries] -remove_dups calls = foldr add [] calls +removeDupCalls calls = foldr add [] calls where add :: CallInfo -> [CallInfo] -> [CallInfo] add ci [] = [ci] @@ -3364,12 +3448,20 @@ remove_dups calls = foldr add [] calls | otherwise = ci2 : add ci1 cis beats_or_same :: CallInfo -> CallInfo -> Bool +-- (beats_or_same ci1 ci2) is True if specialising on ci1 subsumes ci2 +-- That is: ci1's types are less specialised than ci2 +-- ci1 specialises on the same dict args as ci2 beats_or_same (CI { ci_key = args1 }) (CI { ci_key = args2 }) = go args1 args2 where - go [] _ = True + go [] [] = True go (arg1:args1) (arg2:args2) = go_arg arg1 arg2 && go args1 args2 - go (_:_) [] = False + + -- If one or the other runs dry, the other must still have a SpecDict + -- because of the (CI-KEY) invariant. So neither subsumes the other; + -- one is more specialised (faster code) but the other is more generally + -- applicable. + go _ _ = False go_arg (SpecType ty1) (SpecType ty2) = isJust (tcMatchTy ty1 ty2) go_arg UnspecType UnspecType = True ===================================== compiler/GHC/Core/Rules.hs ===================================== @@ -9,7 +9,7 @@ -- The 'CoreRule' datatype itself is declared elsewhere. module GHC.Core.Rules ( -- ** Looking up rules - lookupRule, matchExprs, + lookupRule, matchExprs, ruleLhsIsMoreSpecific, -- ** RuleBase, RuleEnv RuleBase, RuleEnv(..), mkRuleEnv, emptyRuleEnv, @@ -587,8 +587,8 @@ findBest :: InScopeSet -> (Id, [CoreExpr]) findBest _ _ (rule,ans) [] = (rule,ans) findBest in_scope target (rule1,ans1) ((rule2,ans2):prs) - | isMoreSpecific in_scope rule1 rule2 = findBest in_scope target (rule1,ans1) prs - | isMoreSpecific in_scope rule2 rule1 = findBest in_scope target (rule2,ans2) prs + | ruleIsMoreSpecific in_scope rule1 rule2 = findBest in_scope target (rule1,ans1) prs + | ruleIsMoreSpecific in_scope rule2 rule1 = findBest in_scope target (rule2,ans2) prs | debugIsOn = let pp_rule rule = ifPprDebug (ppr rule) (doubleQuotes (ftext (ruleName rule))) @@ -603,15 +603,25 @@ findBest in_scope target (rule1,ans1) ((rule2,ans2):prs) where (fn,args) = target -isMoreSpecific :: InScopeSet -> CoreRule -> CoreRule -> Bool --- The call (rule1 `isMoreSpecific` rule2) +ruleIsMoreSpecific :: InScopeSet -> CoreRule -> CoreRule -> Bool +-- The call (rule1 `ruleIsMoreSpecific` rule2) -- sees if rule2 can be instantiated to look like rule1 --- See Note [isMoreSpecific] -isMoreSpecific _ (BuiltinRule {}) _ = False -isMoreSpecific _ (Rule {}) (BuiltinRule {}) = True -isMoreSpecific in_scope (Rule { ru_bndrs = bndrs1, ru_args = args1 }) - (Rule { ru_bndrs = bndrs2, ru_args = args2 }) - = isJust (matchExprs in_scope_env bndrs2 args2 args1) +-- See Note [ruleIsMoreSpecific] +ruleIsMoreSpecific in_scope rule1 rule2 + = case rule1 of + BuiltinRule {} -> False + Rule { ru_bndrs = bndrs1, ru_args = args1 } + -> ruleLhsIsMoreSpecific in_scope bndrs1 args1 rule2 + +ruleLhsIsMoreSpecific :: InScopeSet + -> [Var] -> [CoreExpr] -- LHS of a possible new rule + -> CoreRule -- An existing rule + -> Bool -- New one is more specific +ruleLhsIsMoreSpecific in_scope bndrs1 args1 rule2 + = case rule2 of + BuiltinRule {} -> True + Rule { ru_bndrs = bndrs2, ru_args = args2 } + -> isJust (matchExprs in_scope_env bndrs2 args2 args1) where full_in_scope = in_scope `extendInScopeSetList` bndrs1 in_scope_env = ISE full_in_scope noUnfoldingFun @@ -620,9 +630,9 @@ isMoreSpecific in_scope (Rule { ru_bndrs = bndrs1, ru_args = args1 }) noBlackList :: Activation -> Bool noBlackList _ = False -- Nothing is black listed -{- Note [isMoreSpecific] +{- Note [ruleIsMoreSpecific] ~~~~~~~~~~~~~~~~~~~~~~~~ -The call (rule1 `isMoreSpecific` rule2) +The call (rule1 `ruleIsMoreSpecific` rule2) sees if rule2 can be instantiated to look like rule1. Wrinkle: @@ -825,7 +835,7 @@ bound on the LHS: The rule looks like forall (a::*) (d::Eq Char) (x :: Foo a Char). - f (Foo a Char) d x = True + f @(Foo a Char) d x = True Matching the rule won't bind 'a', and legitimately so. We fudge by pretending that 'a' is bound to (Any :: *). ===================================== compiler/GHC/Core/Unify.hs ===================================== @@ -331,35 +331,57 @@ Wrinkles `DontBindMe`, the unifier must return `SurelyApart`, not `MaybeApart`. See `go_fam` in `uVarOrFam` -(ATF6) You might think that when /matching/ the um_fam_env will always be empty, - because type-class-instance and type-family-instance heads can't include type - families. E.g. instance C (F a) where ... -- Illegal - - But you'd be wrong: when "improving" type family constraint we may have a - type family on the LHS of a match. Consider +(ATF6) When /matching/ can we ever have a type-family application on the LHS, in + the template? You might think not, because type-class-instance and + type-family-instance heads can't include type families. E.g. + instance C (F a) where ... -- Illegal + + But you'd be wrong: even when matching, we can see type families in the LHS template: + * In `checkValidClass`, in `check_dm` we check that the default method has the + right type, using matching, both ways. And that type may have type-family + applications in it. Example in test CoOpt_Singletons. + + * In the specialiser: see the call to `tcMatchTy` in + `GHC.Core.Opt.Specialise.beats_or_same` + + * With -fpolymorphic-specialsation, we might get a specialiation rule like + RULE forall a (d :: Eq (Maybe (F a))) . + f @(Maybe (F a)) d = ... + See #25965. + + * A user-written RULE could conceivably have a type-family application + in the template. It might not be a good rule, but I don't think we currently + check for this. + + In all these cases we are only interested in finding a substitution /for + type variables/ that makes the match work. So we simply want to recurse into + the arguments of the type family. E.g. + Template: forall a. Maybe (F a) + Target: Mabybe (F Int) + We want to succeed with substitution [a :-> Int]. See (ATF9). + + Conclusion: where we enter via `tcMatchTy`, `tcMatchTys`, `tc_match_tys`, + etc, we always end up in `tc_match_tys_x`. There we invoke the unifier + but we do not distinguish between `SurelyApart` and `MaybeApart`. So in + these cases we can set `um_bind_fam_fun` to `neverBindFam`. + +(ATF7) There is one other, very special case of matching where we /do/ want to + bind type families in `um_fam_env`, namely in GHC.Tc.Solver.Equality, the call + to `tcUnifyTyForInjectivity False` in `improve_injective_wanted_top`. + Consider + of a match. Consider type family G6 a = r | r -> a type instance G6 [a] = [G a] type instance G6 Bool = Int - and the Wanted constraint [W] G6 alpha ~ [Int]. We /match/ each type instance - RHS against [Int]! So we try - [G a] ~ [Int] + and suppose we haev a Wanted constraint + [W] G6 alpha ~ [Int] +. According to Section 5.2 of "Injective type families for Haskell", we /match/ + the RHS each type instance [Int]. So we try + Template: [G a] Target: [Int] and we want to succeed with MaybeApart, so that we can generate the improvement - constraint [W] alpha ~ [beta] where beta is fresh. - See Section 5.2 of "Injective type families for Haskell". - - A second place that we match with type-fams on the LHS is in `checkValidClass`. - In `check_dm` we check that the default method has the right type, using matching, - both ways. And that type may have type-family applications in it. Example in - test CoOpt_Singletons. - -(ATF7) You might think that (ATF6) is a very special case, and in /other/ uses of - matching, where we enter via `tc_match_tys_x` we will never see a type-family - in the template. But actually we do see that case in the specialiser: see - the call to `tcMatchTy` in `GHC.Core.Opt.Specialise.beats_or_same` - - Also: a user-written RULE could conceivably have a type-family application - in the template. It might not be a good rule, but I don't think we currently - check for this. + constraint + [W] alpha ~ [beta] + where beta is fresh. We do this by binding [G a :-> Int] (ATF8) The treatment of type families is governed by um_bind_fam_fun :: BindFamFun @@ -399,6 +421,8 @@ Wrinkles Key point: when decomposing (F tys1 ~ F tys2), we should /also/ extend the type-family substitution. + (ATF11-1) All this cleverness only matters when unifying, not when matching + (ATF12) There is a horrid exception for the injectivity check. See (UR1) in in Note [Specification of unification]. @@ -595,7 +619,7 @@ tc_match_tys_x :: HasDebugCallStack -> [Type] -> Maybe Subst tc_match_tys_x bind_tv match_kis (Subst in_scope id_env tv_env cv_env) tys1 tys2 - = case tc_unify_tys alwaysBindFam -- (ATF7) in Note [Apartness and type families] + = case tc_unify_tys neverBindFam -- (ATF7) in Note [Apartness and type families] bind_tv False -- Matching, not unifying False -- Not an injectivity check @@ -1857,6 +1881,7 @@ uVarOrFam env ty1 ty2 kco = go_fam_fam tc1 tys1 tys2 kco -- Now check if we can bind the (F tys) to the RHS + -- This can happen even when matching: see (ATF7) | BindMe <- um_bind_fam_fun env tc1 tys1 rhs = -- ToDo: do we need an occurs check here? do { extendFamEnv tc1 tys1 rhs @@ -1881,11 +1906,6 @@ uVarOrFam env ty1 ty2 kco -- go_fam_fam: LHS and RHS are both saturated type-family applications, -- for the same type-family F go_fam_fam tc tys1 tys2 kco - | tcEqTyConAppArgs tys1 tys2 - -- Detect (F tys ~ F tys); otherwise we'd build an infinite substitution - = return () - - | otherwise -- Decompose (F tys1 ~ F tys2): (ATF9) -- Use injectivity information of F: (ATF10) -- But first bind the type-fam if poss: (ATF11) @@ -1902,13 +1922,19 @@ uVarOrFam env ty1 ty2 kco (inj_tys1, noninj_tys1) = partitionByList inj tys1 (inj_tys2, noninj_tys2) = partitionByList inj tys2 - bind_fam_if_poss | BindMe <- um_bind_fam_fun env tc tys1 rhs1 - = extendFamEnv tc tys1 rhs1 - | um_unif env - , BindMe <- um_bind_fam_fun env tc tys2 rhs2 - = extendFamEnv tc tys2 rhs2 - | otherwise - = return () + bind_fam_if_poss + | not (um_unif env) -- Not when matching (ATF11-1) + = return () + | tcEqTyConAppArgs tys1 tys2 -- Detect (F tys ~ F tys); + = return () -- otherwise we'd build an infinite substitution + | BindMe <- um_bind_fam_fun env tc tys1 rhs1 + = extendFamEnv tc tys1 rhs1 + | um_unif env + , BindMe <- um_bind_fam_fun env tc tys2 rhs2 + = extendFamEnv tc tys2 rhs2 + | otherwise + = return () + rhs1 = mkTyConApp tc tys2 `mkCastTy` mkSymCo kco rhs2 = mkTyConApp tc tys1 `mkCastTy` kco @@ -1993,7 +2019,7 @@ data UMState = UMState -- in um_foralls; i.e. variables bound by foralls inside the types being unified -- When /matching/ um_fam_env is usually empty; but not quite always. - -- See (ATF6) and (ATF7) of Note [Apartness and type families] + -- See (ATF7) of Note [Apartness and type families] newtype UM a = UM' { unUM :: UMState -> UnifyResultM (UMState, a) } ===================================== compiler/GHC/Tc/Errors.hs ===================================== @@ -466,13 +466,12 @@ mkErrorItem ct = do { let loc = ctLoc ct flav = ctFlavour ct - ; (suppress, m_evdest) <- case ctEvidence ct of - -- For this `suppress` stuff - -- see Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint - CtGiven {} -> return (False, Nothing) - CtWanted (WantedCt { ctev_rewriters = rewriters, ctev_dest = dest }) - -> do { rewriters' <- zonkRewriterSet rewriters - ; return (not (isEmptyRewriterSet rewriters'), Just dest) } + (suppress, m_evdest) = case ctEvidence ct of + -- For this `suppress` stuff + -- see Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint + CtGiven {} -> (False, Nothing) + CtWanted (WantedCt { ctev_rewriters = rws, ctev_dest = dest }) + -> (not (isEmptyRewriterSet rws), Just dest) ; let m_reason = case ct of CIrredCan (IrredCt { ir_reason = reason }) -> Just reason @@ -503,7 +502,7 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics , text "tidy_errs =" <+> ppr tidy_errs ]) -- Catch an awkward (and probably rare) case in which /all/ errors are - -- suppressed: see Wrinkle (WRW2) in Note [Prioritise Wanteds with empty + -- suppressed: see Wrinkle (PER2) in Note [Prioritise Wanteds with empty -- RewriterSet] in GHC.Tc.Types.Constraint. -- -- Unless we are sure that an error will be reported some other way @@ -1788,7 +1787,8 @@ mkTyVarEqErr ctxt item casted_tv1 ty2 mkTyVarEqErr' :: SolverReportErrCtxt -> ErrorItem -> (TcTyVar, TcCoercionN) -> TcType -> TcM TcSolverReportMsg -mkTyVarEqErr' ctxt item (tv1, co1) ty2 +mkTyVarEqErr' ctxt item (tv1, _co1) ty2 + -- ToDo: eliminate _co1??? -- Is this a representation-polymorphism error, e.g. -- alpha[conc] ~# rr[sk] ? If so, handle that first. @@ -1818,11 +1818,13 @@ mkTyVarEqErr' ctxt item (tv1, co1) ty2 -- to be helpful since this is just an unimplemented feature. return main_msg +{- -- Incompatible kinds -- This is wrinkle (EIK2) in Note [Equalities with incompatible kinds] -- in GHC.Tc.Solver.Equality - | hasCoercionHoleCo co1 || hasCoercionHoleTy ty2 + | hasHeteroKindCoercionHoleCo co1 || hasHeteroKindCoercionHoleTy ty2 = return $ mkBlockedEqErr item +-} | isSkolemTyVar tv1 -- ty2 won't be a meta-tyvar; we would have -- swapped in Solver.Equality.canEqTyVarHomo @@ -2007,6 +2009,7 @@ misMatchOrCND ctxt item ty1 ty2 -- Keep only UserGivens that have some equalities. -- See Note [Suppress redundant givens during error reporting] +{- -- These are for the "blocked" equalities, as described in GHC.Tc.Solver.Equality -- Note [Equalities with incompatible kinds], wrinkle (EIK2). There should -- always be another unsolved wanted around, which will ordinarily suppress @@ -2014,6 +2017,7 @@ misMatchOrCND ctxt item ty1 ty2 -- (sigh), so we must produce a message. mkBlockedEqErr :: ErrorItem -> TcSolverReportMsg mkBlockedEqErr item = BlockedEquality item +-} {- Note [Suppress redundant givens during error reporting] ===================================== compiler/GHC/Tc/Solver/Default.hs ===================================== @@ -1081,9 +1081,9 @@ disambigProposalSequences orig_wanteds wanteds proposalSequences allConsistent ; successes <- fmap catMaybes $ nestImplicTcS fake_ev_binds_var (pushTcLevel tclvl) $ mapM firstSuccess proposalSequences - ; traceTcS "disambigProposalSequences" (vcat [ ppr wanteds - , ppr proposalSequences - , ppr successes ]) + ; traceTcS "disambigProposalSequences {" (vcat [ ppr wanteds + , ppr proposalSequences + , ppr successes ]) -- Step (4) in Note [How type-class constraints are defaulted] ; case successes of success@(tvs, subst) : rest ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -1613,54 +1613,59 @@ canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2 -- NotSwapped: -- ev :: (lhs1:ki1) ~r# (xi2:ki2) -- kind_co :: k11 ~# ki2 -- Same orientation as ev --- type_ev :: lhs1 ~r# (xi2 |> sym kind_co) +-- new_ev :: lhs1 ~r# (xi2 |> sym kind_co) -- Swapped -- ev :: (xi2:ki2) ~r# (lhs1:ki1) -- kind_co :: ki2 ~# ki1 -- Same orientation as ev --- type_ev :: (xi2 |> kind_co) ~r# lhs1 +-- new_ev :: (xi2 |> kind_co) ~r# lhs1 +-- Note that we need the `sym` when we are /not/ swapped; hence `mk_sym_co` - = do { (kind_co, rewriters, unifs_happened) <- mk_kind_eq -- :: ki1 ~N ki2 - ; if unifs_happened - -- Unifications happened, so start again to do the zonking - -- Otherwise we might put something in the inert set that isn't inert - then startAgainWith (mkNonCanonical ev) - else - do { let lhs_redn = mkReflRedn role ps_xi1 - rhs_redn = mkGReflRightRedn role xi2 mb_sym_kind_co - mb_sym_kind_co = case swapped of - NotSwapped -> mkSymCo kind_co - IsSwapped -> kind_co - - ; traceTcS "Hetero equality gives rise to kind equality" - (ppr swapped $$ - ppr kind_co <+> dcolon <+> sep [ ppr ki1, text "~#", ppr ki2 ]) - ; type_ev <- rewriteEqEvidence rewriters ev swapped lhs_redn rhs_redn - - ; let new_xi2 = mkCastTy ps_xi2 mb_sym_kind_co - ; canEqCanLHSHomo type_ev eq_rel NotSwapped lhs1 ps_xi1 new_xi2 new_xi2 }} - - where - mk_kind_eq :: TcS (CoercionN, RewriterSet, Bool) - -- Returned kind_co has kind (k1 ~ k2) if NotSwapped, (k2 ~ k1) if Swapped - -- Returned Bool = True if unifications happened, so we should retry - mk_kind_eq = case ev of + = case ev of CtGiven (GivenCt { ctev_evar = evar, ctev_loc = loc }) -> do { let kind_co = mkKindCo (mkCoVarCo evar) pred_ty = unSwap swapped mkNomEqPred ki1 ki2 kind_loc = mkKindEqLoc xi1 xi2 loc ; kind_ev <- newGivenEvVar kind_loc (pred_ty, evCoercion kind_co) ; emitWorkNC [CtGiven kind_ev] - ; return (givenCtEvCoercion kind_ev, emptyRewriterSet, False) } + ; finish emptyRewriterSet (givenCtEvCoercion kind_ev) } CtWanted {} - -> do { (kind_co, cts, unifs) <- wrapUnifierTcS ev Nominal $ \uenv -> - let uenv' = updUEnvLoc uenv (mkKindEqLoc xi1 xi2) - in unSwap swapped (uType uenv') ki1 ki2 - ; return (kind_co, rewriterSetFromCts cts, not (null unifs)) } - + -> do { (kind_co, cts, unifs) <- wrapUnifierTcS ev Nominal $ \uenv -> + let uenv' = updUEnvLoc uenv (mkKindEqLoc xi1 xi2) + in unSwap swapped (uType uenv') ki1 ki2 + ; if not (null unifs) + then -- Unifications happened, so start again to do the zonking + -- Otherwise we might put something in the inert set that isn't inert + startAgainWith (mkNonCanonical ev) + else + + assertPpr (not (isEmptyCts cts)) (ppr ev $$ ppr ki1 $$ ppr ki2) $ + -- The constraints won't be empty because the two kinds differ, and there + -- are no unifications, so we must have emitted one or more constraints + finish (rewriterSetFromCts cts) kind_co } + where xi1 = canEqLHSType lhs1 role = eqRelRole eq_rel + finish rewriters kind_co + = do { traceTcS "Hetero equality gives rise to kind equality" + (ppr swapped $$ + ppr kind_co <+> dcolon <+> sep [ ppr ki1, text "~#", ppr ki2 ]) + ; new_ev <- rewriteEqEvidence rewriters ev swapped lhs_redn rhs_redn + ; canEqCanLHSHomo new_ev eq_rel NotSwapped lhs1 ps_xi1 new_xi2 new_xi2 } + + where + -- kind_co :: ki1 ~N ki2 + lhs_redn = mkReflRedn role ps_xi1 + rhs_redn = mkGReflRightRedn role xi2 sym_kind_co + new_xi2 = mkCastTy ps_xi2 sym_kind_co + + -- Apply mkSymCo when /not/ swapped + sym_kind_co = case swapped of + NotSwapped -> mkSymCo kind_co + IsSwapped -> kind_co + + canEqCanLHSHomo :: CtEvidence -- lhs ~ rhs -- or, if swapped: rhs ~ lhs -> EqRel -> SwapFlag @@ -1863,9 +1868,10 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs ----------------------- canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs -- Try unification; for Wanted, Nominal equalities with a meta-tyvar on the LHS - | isWanted ev -- See Note [Do not unify Givens] - , NomEq <- eq_rel -- See Note [Do not unify representational equalities] + | CtWanted wev <- ev -- See Note [Do not unify Givens] + , NomEq <- eq_rel -- See Note [Do not unify representational equalities] , TyVarLHS tv <- lhs + , isEmptyRewriterSet (ctev_rewriters wev) -- Only unify if the rewriter set is empty = do { given_eq_lvl <- getInnermostGivenEqLevel ; if not (touchabilityAndShapeTest given_eq_lvl tv rhs) then if | Just can_rhs <- canTyFamEqLHS_maybe rhs @@ -2044,19 +2050,20 @@ What do we do when we have an equality where k1 and k2 differ? Easy: we create a coercion that relates k1 and k2 and use this to cast. To wit, from - [X] (tv :: k1) ~ (rhs :: k2) + [X] co1 :: (tv :: k1) ~ (rhs :: k2) (where [X] is [G] or [W]), we go to - [X] co :: k1 ~ k2 - [X] (tv :: k1) ~ ((rhs |> sym co) :: k1) + co1 = co2 ; sym (GRefl kco) + [X] co2 :: (tv :: k1) ~ ((rhs |> sym kco) :: k1) + [X] kco :: k1 ~ k2 Wrinkles: -(EIK1) When X is W, the new type-level wanted is effectively rewritten by the - kind-level one. We thus include the kind-level wanted in the RewriterSet - for the type-level one. See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint. - This is done in canEqCanLHSHetero. +(EIK1) When X=Wanted, the new type-level wanted for `co` is effectively rewritten by + the kind-level one. We thus include the kind-level wanted in the RewriterSet + for the type-level one. See Note [Wanteds rewrite Wanteds] in + GHC.Tc.Types.Constraint. This is done in canEqCanLHSHetero. (EIK2) Suppose we have [W] (a::Type) ~ (b::Type->Type). The above rewrite will produce [W] w : a ~ (b |> kw) @@ -2076,13 +2083,17 @@ Wrinkles: Instead, it lands in the inert_irreds in the inert set, awaiting solution of that `kw`. - (EIK2a) We must later indeed unify if/when the kind-level wanted, `kw` gets - solved. This is done in kickOutAfterFillingCoercionHole, which kicks out + (EIK2a) We must later indeed unify if/when the kind-level wanted, `kw` gets + solved. This is done in `kickOutAfterFillingCoercionHole`, which kicks out all equalities whose RHS mentions the filled-in coercion hole. Note that it looks for type family equalities, too, because of the use of unifyTest in canEqTyVarFunEq. - (EIK2b) What if the RHS mentions /other/ coercion holes? How can that happen? The + To do this, we slightly-hackily use the `ctev_rewriters` field of the inert, + which records that `w` has been rewritten by `kw`. + See (WRW3) in Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint. + + (EIK2b) What if the RHS mentions /other/ coercion holes? How can that happen? The main way is like this. Assume F :: forall k. k -> Type [W] kw : k ~ Type [W] w : a ~ F k t @@ -2093,15 +2104,32 @@ Wrinkles: rewriting. Indeed tests JuanLopez only typechecks if we do. So we'd like to treat this kind of equality as canonical. - Hence the ch_hetero_kind field in CoercionHole: it is True of constraints - created by `canEqCanLHSHetero` to fix up hetero-kinded equalities; and False otherwise: + So here is our implementation: + * The `ch_hetero_kind` field in CoercionHole identifies a coercion hole created + by `canEqCanLHSHetero` to fix up hetero-kinded equalities. + + * An equality constraint is non-canonical if it mentions a /hetero-kind/ + CoercionHole on the RHS. This (and only this) is the (TyEq:CH) invariant + for canonical equalities (see Note [Canonical equalities]) + + * The invariant is checked by the `hasHeterKindCoercionHoleCo` test in + GHC.Tc.Utils.Unify.checkCo; and not satisfying this invariant is what + `cteCoercionHole` in `CheckTyEqResult` means. - * An equality constraint is non-canonical if it mentions a hetero-kind - CoercionHole on the RHS. See the `hasCoercionHoleCo` test in GHC.Tc.Utils.checkCo. + * These special hetero-kind CoercionHoles are created by the `uType` unifier when + the parent's CtOrigin is KindEqOrigin: see GHC.Tc.Utils.TcMType.newCoercionHole + and friends. - * Hetero-kind CoercionHoles are created when the parent's CtOrigin is - KindEqOrigin: see GHC.Tc.Utils.TcMType.newCoercionHole and friends. We - set this origin, via `mkKindLoc`, in `mk_kind_eq` in `canEqCanLHSHetero`. + We set this origin, via `updUEnvLoc`, in `mk_kind_eq` in `canEqCanLHSHetero`. + + * We /also/ add the coercion hole to the `RewriterSet` of the constraint, + in `canEqCanLHSHetero` + + * When filling one of these special hetero-kind coercion holes, we kick out + any IrredCt's that mention this hole; maybe it is now canonical. + See `kickOutAfterFillingCoercionHole`. + + Gah! This is bizarrely complicated. (EIK3) Suppose we have [W] (a :: k1) ~ (rhs :: k2). We duly follow the algorithm detailed here, producing [W] co :: k1 ~ k2, and adding @@ -2576,17 +2604,17 @@ Suppose we have Then we can simply solve g2 from g1, thus g2 := g1. Easy! But it's not so simple: -* If t is a type variable, the equalties might be oriented differently: +(CE1) If t is a type variable, the equalties might be oriented differently: e.g. (g1 :: a~b) and (g2 :: b~a) So we look both ways round. Hence the SwapFlag result to inertsCanDischarge. -* We can only do g2 := g1 if g1 can discharge g2; that depends on +(CE2) We can only do g2 := g1 if g1 can discharge g2; that depends on (a) the role and (b) the flavour. E.g. a representational equality cannot discharge a nominal one; a Wanted cannot discharge a Given. The predicate is eqCanRewriteFR. -* Visibility. Suppose S :: forall k. k -> Type, and consider unifying +(CE3) Visibility. Suppose S :: forall k. k -> Type, and consider unifying S @Type (a::Type) ~ S @(Type->Type) (b::Type->Type) From the first argument we get (Type ~ Type->Type); from the second argument we get (a ~ b) which in turn gives (Type ~ Type->Type). @@ -2601,6 +2629,24 @@ But it's not so simple: So when combining two otherwise-identical equalites, we want to keep the visible one, and discharge the invisible one. Hence the call to strictly_more_visible. + +(CE4) Suppose we have this set up (#25440): + Inert: [W] g1: F a ~ a Int (arising from (F a ~ a Int) + Work item: [W] g2: F alpha ~ F a (arising from (F alpha ~ F a) + We rewrite g2 with g1, to give + [W] g2{rw:g1} : F alpha ~ a Int + Now if F is injective we can get [W] alpha~a, and hence alpha:=a, and + we kick out g1. Now we have two constraints + [W] g1 : F a ~ a Int (arising from (F a ~ a Int) + [W] g2{rw:g1} : F a ~ a Int (arising from (F alpha ~ F a) + If we end up with g2 in the inert set (not g1) we'll get a very confusing + error message that we can solve (F a ~ a Int) + arising from F a ~ F a + + TL;DR: Better to hang on to `g1` (with no rewriters), in preference + to `g2` (which has a rewriter). + + See (WRW1) in Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint. -} tryInertEqs :: EqCt -> SolverStage () @@ -2646,21 +2692,27 @@ inertsCanDischarge inerts (EqCt { eq_lhs = lhs_w, eq_rhs = rhs_w loc_w = ctEvLoc ev_w flav_w = ctEvFlavour ev_w fr_w = (flav_w, eq_rel) + empty_rw_w = isEmptyRewriterSet (ctEvRewriters ev_w) inert_beats_wanted ev_i eq_rel = -- eqCanRewriteFR: see second bullet of Note [Combining equalities] - -- strictly_more_visible: see last bullet of Note [Combining equalities] fr_i `eqCanRewriteFR` fr_w - && not ((loc_w `strictly_more_visible` ctEvLoc ev_i) - && (fr_w `eqCanRewriteFR` fr_i)) + && not (prefer_wanted ev_i && (fr_w `eqCanRewriteFR` fr_i)) where fr_i = (ctEvFlavour ev_i, eq_rel) - -- See Note [Combining equalities], final bullet + -- See (CE3) in Note [Combining equalities] strictly_more_visible loc1 loc2 = not (isVisibleOrigin (ctLocOrigin loc2)) && isVisibleOrigin (ctLocOrigin loc1) + prefer_wanted ev_i + = (loc_w `strictly_more_visible` ctEvLoc ev_i) + -- strictly_more_visible: see (CE3) in Note [Combining equalities] + || (empty_rw_w && not (isEmptyRewriterSet (ctEvRewriters ev_i))) + -- Prefer the one that has no rewriters + -- See (CE4) in Note [Combining equalities] + inertsCanDischarge _ _ = Nothing @@ -3017,6 +3069,7 @@ improve_wanted_top_fun_eqs fam_tc lhs_tys rhs_ty improve_injective_wanted_top :: FamInstEnvs -> [Bool] -> TyCon -> [TcType] -> Xi -> TcS [TypeEqn] -- Interact with top-level instance declarations +-- See Section 5.2 in the Injective Type Families paper improve_injective_wanted_top fam_envs inj_args fam_tc lhs_tys rhs_ty = concatMapM do_one branches where @@ -3035,6 +3088,7 @@ improve_injective_wanted_top fam_envs inj_args fam_tc lhs_tys rhs_ty do_one branch@(CoAxBranch { cab_tvs = branch_tvs, cab_lhs = branch_lhs_tys, cab_rhs = branch_rhs }) | let in_scope1 = in_scope `extendInScopeSetList` branch_tvs , Just subst <- tcUnifyTyForInjectivity False in_scope1 branch_rhs rhs_ty + -- False: matching, not unifying = do { let inSubst tv = tv `elemVarEnv` getTvSubstEnv subst unsubstTvs = filterOut inSubst branch_tvs -- The order of unsubstTvs is important; it must be ===================================== compiler/GHC/Tc/Solver/InertSet.hs ===================================== @@ -9,9 +9,9 @@ module GHC.Tc.Solver.InertSet ( extendWorkListNonEq, extendWorkListCt, extendWorkListCts, extendWorkListCtList, extendWorkListEq, extendWorkListEqs, + extendWorkListRewrittenEqs, appendWorkList, extendWorkListImplic, workListSize, - selectWorkItem, -- * The inert set InertSet(..), @@ -172,6 +172,7 @@ See GHC.Tc.Solver.Monad.deferTcSForAllEq data WorkList = WL { wl_eqs_N :: [Ct] -- /Nominal/ equalities (s ~#N t), (s ~ t), (s ~~ t) -- with empty rewriter set + , wl_eqs_X :: [Ct] -- CEqCan, CDictCan, CIrredCan -- with empty rewriter set -- All other equalities: contains both equality constraints and @@ -179,9 +180,8 @@ data WorkList -- See Note [Prioritise equalities] -- See Note [Prioritise class equalities] - , wl_rw_eqs :: [Ct] -- Like wl_eqs, but ones that have a non-empty - -- rewriter set; or, more precisely, did when - -- added to the WorkList + , wl_rw_eqs :: [Ct] -- Like wl_eqs, but ones that may have a non-empty + -- rewriter set -- We prioritise wl_eqs over wl_rw_eqs; -- see Note [Prioritise Wanteds with empty RewriterSet] -- in GHC.Tc.Types.Constraint for more details. @@ -258,6 +258,11 @@ extendWorkListEqs rewriters new_eqs -- push_on_front puts the new equlities on the front of the queue push_on_front new_eqs eqs = foldr (:) eqs new_eqs +extendWorkListRewrittenEqs :: [EqCt] -> WorkList -> WorkList +-- Don't bother checking the RewriterSet: just pop them into wl_rw_eqs +extendWorkListRewrittenEqs new_eqs wl@(WL { wl_rw_eqs = rw_eqs }) + = wl { wl_rw_eqs = foldr ((:) . CEqCan) rw_eqs new_eqs } + extendWorkListNonEq :: Ct -> WorkList -> WorkList -- Extension by non equality extendWorkListNonEq ct wl = wl { wl_rest = ct : wl_rest wl } @@ -296,16 +301,6 @@ emptyWorkList :: WorkList emptyWorkList = WL { wl_eqs_N = [], wl_eqs_X = [] , wl_rw_eqs = [], wl_rest = [], wl_implics = emptyBag } -selectWorkItem :: WorkList -> Maybe (Ct, WorkList) --- See Note [Prioritise equalities] -selectWorkItem wl@(WL { wl_eqs_N = eqs_N, wl_eqs_X = eqs_X - , wl_rw_eqs = rw_eqs, wl_rest = rest }) - | ct:cts <- eqs_N = Just (ct, wl { wl_eqs_N = cts }) - | ct:cts <- eqs_X = Just (ct, wl { wl_eqs_X = cts }) - | ct:cts <- rw_eqs = Just (ct, wl { wl_rw_eqs = cts }) - | ct:cts <- rest = Just (ct, wl { wl_rest = cts }) - | otherwise = Nothing - -- Pretty printing instance Outputable WorkList where ppr (WL { wl_eqs_N = eqs_N, wl_eqs_X = eqs_X, wl_rw_eqs = rw_eqs ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -150,7 +150,6 @@ import qualified GHC.Tc.Utils.Env as TcM ) import GHC.Tc.Zonk.Monad ( ZonkM ) import qualified GHC.Tc.Zonk.TcType as TcM -import qualified GHC.Tc.Zonk.Type as TcM import GHC.Driver.DynFlags @@ -475,16 +474,16 @@ kickOutAfterUnification tv_list = case nonEmpty tv_list of ; return n_kicked } kickOutAfterFillingCoercionHole :: CoercionHole -> TcS () --- See Wrinkle (EIK2a) in Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Equality +-- See Wrinkle (EIK2) in Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Equality -- It's possible that this could just go ahead and unify, but could there be occurs-check -- problems? Seems simpler just to kick out. kickOutAfterFillingCoercionHole hole = do { ics <- getInertCans ; let (kicked_out, ics') = kick_out ics - n_kicked = lengthBag kicked_out + n_kicked = length kicked_out ; unless (n_kicked == 0) $ - do { updWorkListTcS (extendWorkListCts (fmap CIrredCan kicked_out)) + do { updWorkListTcS (extendWorkListRewrittenEqs kicked_out) ; csTraceTcS $ hang (text "Kick out, hole =" <+> ppr hole) 2 (vcat [ text "n-kicked =" <+> int n_kicked @@ -493,24 +492,18 @@ kickOutAfterFillingCoercionHole hole ; setInertCans ics' } where - kick_out :: InertCans -> (Bag IrredCt, InertCans) - kick_out ics@(IC { inert_irreds = irreds }) - = -- We only care about irreds here, because any constraint blocked - -- by a coercion hole is an irred. See wrinkle (EIK2a) in - -- Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical - (irreds_to_kick, ics { inert_irreds = irreds_to_keep }) + kick_out :: InertCans -> ([EqCt], InertCans) + kick_out ics@(IC { inert_eqs = eqs }) + = (eqs_to_kick, ics { inert_eqs = eqs_to_keep }) where - (irreds_to_kick, irreds_to_keep) = partitionBag kick_ct irreds - - kick_ct :: IrredCt -> Bool - -- True: kick out; False: keep. - kick_ct ct - | IrredCt { ir_ev = ev, ir_reason = reason } <- ct - , CtWanted (WantedCt { ctev_rewriters = RewriterSet rewriters }) <- ev - , NonCanonicalReason ctyeq <- reason - , ctyeq `cterHasProblem` cteCoercionHole - , hole `elementOfUniqSet` rewriters - = True + (eqs_to_kick, eqs_to_keep) = partitionInertEqs kick_out_eq eqs + + kick_out_eq :: EqCt -> Bool -- True: kick out; False: keep. + kick_out_eq (EqCt { eq_ev = ev ,eq_lhs = lhs }) + | CtWanted (WantedCt { ctev_rewriters = RewriterSet rewriters }) <- ev + , TyVarLHS tv <- lhs + , isMetaTyVar tv + = hole `elementOfUniqSet` rewriters | otherwise = False @@ -847,17 +840,15 @@ removeInertCt is ct -- | Looks up a family application in the inerts. lookupFamAppInert :: (CtFlavourRole -> Bool) -- can it rewrite the target? - -> TyCon -> [Type] -> TcS (Maybe (Reduction, CtFlavourRole)) + -> TyCon -> [Type] -> TcS (Maybe EqCt) lookupFamAppInert rewrite_pred fam_tc tys = do { IS { inert_cans = IC { inert_funeqs = inert_funeqs } } <- getInertSet ; return (lookup_inerts inert_funeqs) } where lookup_inerts inert_funeqs - | Just ecl <- findFunEq inert_funeqs fam_tc tys - , Just (EqCt { eq_ev = ctev, eq_rhs = rhs }) - <- find (rewrite_pred . eqCtFlavourRole) ecl - = Just (mkReduction (ctEvCoercion ctev) rhs, ctEvFlavourRole ctev) - | otherwise = Nothing + = case findFunEq inert_funeqs fam_tc tys of + Nothing -> Nothing + Just (ecl :: [EqCt]) -> find (rewrite_pred . eqCtFlavourRole) ecl lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence) -- Is this exact predicate type cached in the solved or canonicals of the InertSet? @@ -1418,62 +1409,6 @@ getInertSet = getInertSetRef >>= readTcRef setInertSet :: InertSet -> TcS () setInertSet is = do { r <- getInertSetRef; writeTcRef r is } -getTcSWorkListRef :: TcS (IORef WorkList) -getTcSWorkListRef = TcS (return . tcs_worklist) - -getWorkListImplics :: TcS (Bag Implication) -getWorkListImplics - = do { wl_var <- getTcSWorkListRef - ; wl_curr <- readTcRef wl_var - ; return (wl_implics wl_curr) } - -pushLevelNoWorkList :: SDoc -> TcS a -> TcS (TcLevel, a) --- Push the level and run thing_inside --- However, thing_inside should not generate any work items -#if defined(DEBUG) -pushLevelNoWorkList err_doc (TcS thing_inside) - = TcS (\env -> TcM.pushTcLevelM $ - thing_inside (env { tcs_worklist = wl_panic }) - ) - where - wl_panic = pprPanic "GHC.Tc.Solver.Monad.buildImplication" err_doc - -- This panic checks that the thing-inside - -- does not emit any work-list constraints -#else -pushLevelNoWorkList _ (TcS thing_inside) - = TcS (\env -> TcM.pushTcLevelM (thing_inside env)) -- Don't check -#endif - -updWorkListTcS :: (WorkList -> WorkList) -> TcS () -updWorkListTcS f - = do { wl_var <- getTcSWorkListRef - ; updTcRef wl_var f } - -emitWorkNC :: [CtEvidence] -> TcS () -emitWorkNC evs - | null evs - = return () - | otherwise - = emitWork (listToBag (map mkNonCanonical evs)) - -emitWork :: Cts -> TcS () -emitWork cts - | isEmptyBag cts -- Avoid printing, among other work - = return () - | otherwise - = do { traceTcS "Emitting fresh work" (pprBag cts) - -- Zonk the rewriter set of Wanteds, because that affects - -- the prioritisation of the work-list. Suppose a constraint - -- c1 is rewritten by another, c2. When c2 gets solved, - -- c1 has no rewriters, and can be prioritised; see - -- Note [Prioritise Wanteds with empty RewriterSet] - -- in GHC.Tc.Types.Constraint wrinkle (WRW1) - ; cts <- wrapTcS $ mapBagM TcM.zonkCtRewriterSet cts - ; updWorkListTcS (extendWorkListCts cts) } - -emitImplication :: Implication -> TcS () -emitImplication implic - = updWorkListTcS (extendWorkListImplic implic) newTcRef :: a -> TcS (TcRef a) newTcRef x = wrapTcS (TcM.newTcRef x) @@ -1532,23 +1467,6 @@ reportUnifications (TcS thing_inside) getDefaultInfo :: TcS (DefaultEnv, Bool) getDefaultInfo = wrapTcS TcM.tcGetDefaultTys -getWorkList :: TcS WorkList -getWorkList = do { wl_var <- getTcSWorkListRef - ; wrapTcS (TcM.readTcRef wl_var) } - -selectNextWorkItem :: TcS (Maybe Ct) --- Pick which work item to do next --- See Note [Prioritise equalities] -selectNextWorkItem - = do { wl_var <- getTcSWorkListRef - ; wl <- readTcRef wl_var - ; case selectWorkItem wl of { - Nothing -> return Nothing ; - Just (ct, new_wl) -> - do { -- checkReductionDepth (ctLoc ct) (ctPred ct) - -- This is done by GHC.Tc.Solver.Dict.chooseInstance - ; writeTcRef wl_var new_wl - ; return (Just ct) } } } -- Just get some environments needed for instance looking up and matching -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1805,6 +1723,116 @@ pprKicked :: Int -> SDoc pprKicked 0 = empty pprKicked n = parens (int n <+> text "kicked out") + +{- ********************************************************************* +* * +* The work list +* * +********************************************************************* -} + + +getTcSWorkListRef :: TcS (IORef WorkList) +getTcSWorkListRef = TcS (return . tcs_worklist) + +getWorkList :: TcS WorkList +getWorkList = do { wl_var <- getTcSWorkListRef + ; readTcRef wl_var } + +getWorkListImplics :: TcS (Bag Implication) +getWorkListImplics + = do { wl_var <- getTcSWorkListRef + ; wl_curr <- readTcRef wl_var + ; return (wl_implics wl_curr) } + +updWorkListTcS :: (WorkList -> WorkList) -> TcS () +updWorkListTcS f + = do { wl_var <- getTcSWorkListRef + ; updTcRef wl_var f } + +emitWorkNC :: [CtEvidence] -> TcS () +emitWorkNC evs + | null evs + = return () + | otherwise + = emitWork (listToBag (map mkNonCanonical evs)) + +emitWork :: Cts -> TcS () +emitWork cts + | isEmptyBag cts -- Avoid printing, among other work + = return () + | otherwise + = do { traceTcS "Emitting fresh work" (pprBag cts) + ; updWorkListTcS (extendWorkListCts cts) } + +emitImplication :: Implication -> TcS () +emitImplication implic + = updWorkListTcS (extendWorkListImplic implic) + +selectNextWorkItem :: TcS (Maybe Ct) +-- Pick which work item to do next +-- See Note [Prioritise equalities] +-- +-- Postcondition: if the returned item is a Wanted equality, +-- then its rewriter set is fully zonked. +-- +-- Suppose a constraint c1 is rewritten by another, c2. When c2 +-- gets solved, c1 has no rewriters, and can be prioritised; see +-- Note [Prioritise Wanteds with empty RewriterSet] in +-- GHC.Tc.Types.Constraint wrinkle (PER1) + +-- ToDo: if wl_rw_eqs is long, we'll re-zonk it each time we pick +-- a new item from wl_rest. Bad. +selectNextWorkItem + = do { wl_var <- getTcSWorkListRef + ; wl <- readTcRef wl_var + + ; case wl of { WL { wl_eqs_N = eqs_N, wl_eqs_X = eqs_X + , wl_rw_eqs = rw_eqs, wl_rest = rest } + | ct:cts <- eqs_N -> pick_me ct (wl { wl_eqs_N = cts }) + | ct:cts <- eqs_X -> pick_me ct (wl { wl_eqs_X = cts }) + | otherwise -> try_rws [] rw_eqs + where + pick_me :: Ct -> WorkList -> TcS (Maybe Ct) + pick_me ct new_wl + = do { writeTcRef wl_var new_wl + ; return (Just ct) } + -- NB: no need for checkReductionDepth (ctLoc ct) (ctPred ct) + -- This is done by GHC.Tc.Solver.Dict.chooseInstance + + -- try_rws looks through rw_eqs to find one that has an empty + -- rewriter set, after zonking. If none such, call try_rest. + try_rws acc (ct:cts) + = do { ct' <- liftZonkTcS (TcM.zonkCtRewriterSet ct) + ; if ctHasNoRewriters ct' + then pick_me ct' (wl { wl_rw_eqs = cts ++ acc }) + else try_rws (ct':acc) cts } + try_rws acc [] = try_rest acc + + try_rest zonked_rws + | ct:cts <- rest = pick_me ct (wl { wl_rw_eqs = zonked_rws, wl_rest = cts }) + | ct:cts <- zonked_rws = pick_me ct (wl { wl_rw_eqs = cts }) + | otherwise = return Nothing + } } + + +pushLevelNoWorkList :: SDoc -> TcS a -> TcS (TcLevel, a) +-- Push the level and run thing_inside +-- However, thing_inside should not generate any work items +#if defined(DEBUG) +pushLevelNoWorkList err_doc (TcS thing_inside) + = TcS (\env -> TcM.pushTcLevelM $ + thing_inside (env { tcs_worklist = wl_panic }) + ) + where + wl_panic = pprPanic "GHC.Tc.Solver.Monad.buildImplication" err_doc + -- This panic checks that the thing-inside + -- does not emit any work-list constraints +#else +pushLevelNoWorkList _ (TcS thing_inside) + = TcS (\env -> TcM.pushTcLevelM (thing_inside env)) -- Don't check +#endif + + {- ********************************************************************* * * * The Unification Level Flag * @@ -2340,7 +2368,7 @@ wrapUnifierX ev role do_unifications ; wrapTcS $ do { defer_ref <- TcM.newTcRef emptyBag ; unified_ref <- TcM.newTcRef [] - ; rewriters <- TcM.zonkRewriterSet (ctEvRewriters ev) + ; rewriters <- TcM.liftZonkM (TcM.zonkRewriterSet (ctEvRewriters ev)) ; let env = UE { u_role = role , u_rewriters = rewriters , u_loc = ctEvLoc ev ===================================== compiler/GHC/Tc/Solver/Rewrite.hs ===================================== @@ -150,13 +150,16 @@ bumpDepth (RewriteM thing_inside) { let !env' = env { re_loc = bumpCtLocDepth (re_loc env) } ; thing_inside env' } +recordRewriter :: CtEvidence -> RewriteM () +-- Record that we have rewritten the target with this (equality) evidence -- See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint --- Precondition: the WantedCtEvidence is for an equality constraint -recordRewriter :: WantedCtEvidence -> RewriteM () -recordRewriter (WantedCt { ctev_dest = HoleDest hole }) - = RewriteM $ \env -> updTcRef (re_rewriters env) (`addRewriter` hole) -recordRewriter other = - pprPanic "recordRewriter: non-equality constraint" (ppr other) +-- Precondition: the CtEvidence is for an equality constraint +recordRewriter (CtGiven {}) + = return () +recordRewriter (CtWanted (WantedCt { ctev_dest = dest })) + = case dest of + HoleDest hole -> RewriteM $ \env -> updTcRef (re_rewriters env) (`addRewriter` hole) + other -> pprPanic "recordRewriter: non-equality constraint" (ppr other) {- Note [Rewriter EqRels] ~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -848,16 +851,18 @@ rewrite_exact_fam_app tc tys -- STEP 3: try the inerts ; flavour <- getFlavour - ; result2 <- liftTcS $ lookupFamAppInert (`eqCanRewriteFR` (flavour, eq_rel)) tc xis - ; case result2 of - { Just (redn, (inert_flavour, inert_eq_rel)) + ; mb_eq <- liftTcS $ lookupFamAppInert (`eqCanRewriteFR` (flavour, eq_rel)) tc xis + ; case mb_eq of + { Just (EqCt { eq_ev = inert_ev, eq_rhs = inert_rhs, eq_eq_rel = inert_eq_rel }) -> do { traceRewriteM "rewrite family application with inert" (ppr tc <+> ppr xis $$ ppr redn) - ; finish (inert_flavour == Given) (homogenise downgraded_redn) } - -- this will sometimes duplicate an inert in the cache, + ; recordRewriter inert_ev + ; finish (isGiven inert_ev) (homogenise downgraded_redn) } + -- This will sometimes duplicate an inert in the cache, -- but avoiding doing so had no impact on performance, and -- it seems easier not to weed out that special case where + redn = mkReduction (ctEvCoercion inert_ev) inert_rhs inert_role = eqRelRole inert_eq_rel role = eqRelRole eq_rel downgraded_redn = downgradeRedn role inert_role redn @@ -1024,11 +1029,8 @@ rewrite_tyvar2 tv fr@(_, eq_rel) -> do { traceRewriteM "Following inert tyvar" $ vcat [ ppr tv <+> equals <+> ppr rhs_ty , ppr ctev ] - ; case ctev of - CtGiven {} -> return () - CtWanted wtd -> + ; recordRewriter ctev -- See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint - recordRewriter wtd ; let rewriting_co1 = ctEvCoercion ctev rewriting_co = case (ct_eq_rel, eq_rel) of ===================================== compiler/GHC/Tc/Types/Constraint.hs ===================================== @@ -17,7 +17,7 @@ module GHC.Tc.Types.Constraint ( isUnsatisfiableCt_maybe, ctEvidence, updCtEvidence, ctLoc, ctPred, ctFlavour, ctEqRel, ctOrigin, - ctRewriters, + ctRewriters, ctHasNoRewriters, ctEvId, wantedEvId_maybe, mkTcEqPredLikeEv, mkNonCanonical, mkGivens, tyCoVarsOfCt, tyCoVarsOfCts, @@ -240,18 +240,24 @@ instance Outputable DictCt where {- Note [Canonical equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ An EqCt is a canonical equality constraint, one that can live in the inert set, -and that can be used to rewrite other constrtaints. It satisfies these invariants: +and that can be used to rewrite other constraints. It satisfies these invariants: + * (TyEq:OC) lhs does not occur in rhs (occurs check) Note [EqCt occurs check] + * (TyEq:F) rhs has no foralls (this avoids substituting a forall for the tyvar in other types) + * (TyEq:K) typeKind lhs `tcEqKind` typeKind rhs; Note [Ct kind invariant] + * (TyEq:N) If the equality is representational, rhs is not headed by a saturated application of a newtype TyCon. See GHC.Tc.Solver.Equality Note [No top-level newtypes on RHS of representational equalities]. (Applies only when constructor of newtype is in scope.) + * (TyEq:U) An EqCt is not immediately unifiable. If we can unify a:=ty, we will not form an EqCt (a ~ ty). + * (TyEq:CH) rhs does not mention any coercion holes that resulted from fixing up a hetero-kinded equality. See Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Equality, wrinkle (EIK2) @@ -534,9 +540,12 @@ cteSolubleOccurs = CTEP (bit 3) -- Occurs-check under a type function, or in -- cteSolubleOccurs must be one bit to the left of cteInsolubleOccurs -- See also Note [Insoluble mis-match] in GHC.Tc.Errors -cteCoercionHole = CTEP (bit 4) -- Coercion hole encountered +cteCoercionHole = CTEP (bit 4) -- Kind-equality coercion hole encountered + -- See (EIK2) in Note [Equalities with incompatible kinds] + cteConcrete = CTEP (bit 5) -- Type variable that can't be made concrete -- e.g. alpha[conc] ~ Maybe beta[tv] + cteSkolemEscape = CTEP (bit 6) -- Skolem escape e.g. alpha[2] ~ b[sk,4] cteProblem :: CheckTyEqProblem -> CheckTyEqResult @@ -2220,6 +2229,12 @@ ctEvRewriters :: CtEvidence -> RewriterSet ctEvRewriters (CtWanted (WantedCt { ctev_rewriters = rws })) = rws ctEvRewriters (CtGiven {}) = emptyRewriterSet +ctHasNoRewriters :: Ct -> Bool +ctHasNoRewriters ct + = case ctEvidence ct of + CtWanted (WantedCt { ctev_rewriters = rws }) -> isEmptyRewriterSet rws + CtGiven {} -> True + -- | Set the rewriter set of a Wanted constraint. setWantedCtEvRewriters :: WantedCtEvidence -> RewriterSet -> WantedCtEvidence setWantedCtEvRewriters ev rs = ev { ctev_rewriters = rs } @@ -2444,19 +2459,29 @@ We thus want Wanteds to rewrite Wanteds in order to accept more programs, but we don't want Wanteds to rewrite Wanteds because doing so can create inscrutable error messages. To solve this dilemma: -* We allow Wanteds to rewrite Wanteds, but... +* We allow Wanteds to rewrite Wanteds, but each Wanted tracks the set of Wanteds + it has been rewritten by, in its RewriterSet, stored in the ctev_rewriters + field of the CtWanted constructor of CtEvidence. (Only Wanteds have + RewriterSets.) + +* A RewriterSet is just a set of unfilled CoercionHoles. This is sufficient + because only equalities (evidenced by coercion holes) are used for rewriting; + other (dictionary) constraints cannot ever rewrite. + +* The rewriter (in e.g. GHC.Tc.Solver.Rewrite.rewrite) tracks and returns a RewriterSet, + consisting of the evidence (a CoercionHole) for any Wanted equalities used in + rewriting. -* Each Wanted tracks the set of Wanteds it has been rewritten by, in its - RewriterSet, stored in the ctev_rewriters field of the CtWanted - constructor of CtEvidence. (Only Wanteds have RewriterSets.) +* Then GHC.Tc.Solver.Solve.rewriteEvidence and GHC.Tc.Solver.Equality.rewriteEqEvidence + add this RewriterSet to the rewritten constraint's rewriter set. * In error reporting, we simply suppress any errors that have been rewritten by /unsolved/ wanteds. This suppression happens in GHC.Tc.Errors.mkErrorItem, - which uses GHC.Tc.Zonk.Type.zonkRewriterSet to look through any filled + which uses `GHC.Tc.Zonk.Type.zonkRewriterSet` to look through any filled coercion holes. The idea is that we wish to report the "root cause" -- the error that rewrote all the others. -* We prioritise Wanteds that have an empty RewriterSet: +* In error reporting, we prioritise Wanteds that have an empty RewriterSet: see Note [Prioritise Wanteds with empty RewriterSet]. Let's continue our first example above: @@ -2471,19 +2496,30 @@ Because Wanteds can rewrite Wanteds, w1 will rewrite w2, yielding The {w1} in the second line of output is the RewriterSet of w1. -A RewriterSet is just a set of unfilled CoercionHoles. This is sufficient -because only equalities (evidenced by coercion holes) are used for rewriting; -other (dictionary) constraints cannot ever rewrite. The rewriter (in -e.g. GHC.Tc.Solver.Rewrite.rewrite) tracks and returns a RewriterSet, -consisting of the evidence (a CoercionHole) for any Wanted equalities used in -rewriting. Then GHC.Tc.Solver.Solve.rewriteEvidence and -GHC.Tc.Solver.Equality.rewriteEqEvidence add this RewriterSet to the rewritten -constraint's rewriter set. +Wrinkles: + +(WRW1) When we find a constraint identical to one already in the inert set, + we solve one from the other. Other things being equal, keep the one + that has fewer (better still no) rewriters. + See (CE4) in Note [Combining equalities] in GHC.Tc.Solver.Equality. + + To this accurately we should use `zonkRewriterSet` during canonicalisation, + to eliminate rewriters that have now been solved. Currently we only do so + during error reporting; but perhaps we should change that. + +(WRW2) When zonking a constraint (with `zonkCt` and `zonkCtEvidence`) we take + the opportunity to zonk its `RewriterSet`, which eliminates solved ones. + This doesn't guarantee that rewriter sets are always up to date -- see + (WRW1) -- but it helps, and it de-clutters debug output. + +(WRW3) We use the rewriter set for a slightly different purpose, in (EIK2) + of Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Equality. + This is a bit of a hack. Note [Prioritise Wanteds with empty RewriterSet] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When extending the WorkList, in GHC.Tc.Solver.InertSet.extendWorkListEq, -we priorities constraints that have no rewriters. Here's why. +we prioritise constraints that have no rewriters. Here's why. Consider this, which came up in T22793: inert: {} @@ -2527,11 +2563,11 @@ GHC.Tc.Solver.InertSet.extendWorkListEq, and extendWorkListEqs. Wrinkles -(WRW1) Before checking for an empty RewriterSet, we zonk the RewriterSet, +(PER1) Before checking for an empty RewriterSet, we zonk the RewriterSet, because some of those CoercionHoles may have been filled in since we last looked: see GHC.Tc.Solver.Monad.emitWork. -(WRW2) Despite the prioritisation, it is hard to be /certain/ that we can't end up +(PER2) Despite the prioritisation, it is hard to be /certain/ that we can't end up in a situation where all of the Wanteds have rewritten each other. In order to report /some/ error in this case, we simply report all the Wanteds. The user will get a perhaps-confusing error message, but they've ===================================== compiler/GHC/Tc/Utils/TcMType.hs ===================================== @@ -49,7 +49,6 @@ module GHC.Tc.Utils.TcMType ( newCoercionHole, newCoercionHoleO, newVanillaCoercionHole, fillCoercionHole, isFilledCoercionHole, - unpackCoercionHole, unpackCoercionHole_maybe, checkCoercionHole, newImplication, @@ -115,7 +114,6 @@ import GHC.Tc.Types.CtLoc( CtLoc, ctLocOrigin ) import GHC.Tc.Utils.Monad -- TcType, amongst others import GHC.Tc.Utils.TcType import GHC.Tc.Errors.Types -import GHC.Tc.Zonk.Type import GHC.Tc.Zonk.TcType import GHC.Builtin.Names @@ -371,6 +369,7 @@ newCoercionHoleO (KindEqOrigin {}) pty = new_coercion_hole True pty newCoercionHoleO _ pty = new_coercion_hole False pty new_coercion_hole :: Bool -> TcPredType -> TcM CoercionHole +-- For the Bool, see (EIK2) in Note [Equalities with incompatible kinds] new_coercion_hole hetero_kind pred_ty = do { co_var <- newEvVar pred_ty ; traceTc "New coercion hole:" (ppr co_var <+> dcolon <+> ppr pred_ty) @@ -1583,7 +1582,7 @@ collect_cand_qtvs_co orig_ty cur_lvl bound = go_co go_co dv (SubCo co) = go_co dv co go_co dv (HoleCo hole) - = do m_co <- unpackCoercionHole_maybe hole + = do m_co <- liftZonkM (unpackCoercionHole_maybe hole) case m_co of Just co -> go_co dv co Nothing -> go_cv dv (coHoleCoVar hole) ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -2649,8 +2649,9 @@ There are five reasons not to unify: we can fill beta[tau] := beta[conc]. This is why we call 'makeTypeConcrete' in startSolvingByUnification. -5. (COERCION-HOLE) Confusing coercion holes - Suppose our equality is +5. (COERCION-HOLE) rhs does not mention any coercion holes that resulted from + fixing up a hetero-kinded equality. This is the same as (TyEq:CH) in + Note [Canonical equalities]. Suppose our equality is (alpha :: k) ~ (Int |> {co}) where co :: Type ~ k is an unsolved wanted. Note that this equality is homogeneous; both sides have kind k. We refrain from unifying here, because @@ -3546,11 +3547,13 @@ checkCo flags co = | case conc of { CC_None -> False; _ -> True } -> return $ PuFail (cteProblem cteConcrete) +{- Trying NOT doing this -- # -- Check for coercion holes, if unifying. -- See (COERCION-HOLE) in Note [Unification preconditions] | case lc of { LC_None {} -> False; _ -> True } -- equivalent to "we are unifying"; see Note [TyEqFlags] - , hasCoercionHoleCo co + , hasHeteroKindCoercionHoleCo co -> return $ PuFail (cteProblem cteCoercionHole) +-} -- Occurs check (can promote) | OC_Check lhs_tv occ_prob <- occ ===================================== compiler/GHC/Tc/Zonk/TcType.hs ===================================== @@ -1,3 +1,5 @@ +{-# LANGUAGE DuplicateRecordFields #-} + {- (c) The University of Glasgow 2006 (c) The AQUA Project, Glasgow University, 1996-1998 @@ -36,6 +38,13 @@ module GHC.Tc.Zonk.TcType -- ** Zonking constraints , zonkCt, zonkWC, zonkSimples, zonkImplication + -- * Rewriter sets + , zonkRewriterSet, zonkCtRewriterSet, zonkCtEvRewriterSet + + -- * Coercion holes + , isFilledCoercionHole, unpackCoercionHole, unpackCoercionHole_maybe + + -- * Tidying , tcInitTidyEnv, tcInitOpenTidyEnv , tidyCt, tidyEvVar, tidyDelayedError @@ -81,7 +90,7 @@ import GHC.Core.Coercion import GHC.Core.Predicate import GHC.Utils.Constants -import GHC.Utils.Outputable +import GHC.Utils.Outputable as Outputable import GHC.Utils.Misc import GHC.Utils.Monad ( mapAccumLM ) import GHC.Utils.Panic @@ -89,6 +98,9 @@ import GHC.Utils.Panic import GHC.Data.Bag import GHC.Data.Pair +import Data.Semigroup +import Data.Maybe + {- ********************************************************************* * * Writing to metavariables @@ -366,8 +378,8 @@ checkCoercionHole cv co ; return $ assertPpr (ok cv_ty) (text "Bad coercion hole" <+> - ppr cv <> colon <+> vcat [ ppr t1, ppr t2, ppr role - , ppr cv_ty ]) + ppr cv Outputable.<> colon + <+> vcat [ ppr t1, ppr t2, ppr role, ppr cv_ty ]) co } | otherwise = return co @@ -494,9 +506,15 @@ zonkCt ct ; return (mkNonCanonical fl') } zonkCtEvidence :: CtEvidence -> ZonkM CtEvidence -zonkCtEvidence ctev - = do { pred' <- zonkTcType (ctEvPred ctev) - ; return (setCtEvPredType ctev pred') } +-- Zonks the ctev_pred and the ctev_rewriters; but not ctev_evar +-- For ctev_rewriters, see (WRW2) in Note [Wanteds rewrite Wanteds] +zonkCtEvidence (CtGiven (GivenCt { ctev_pred = pred, ctev_evar = var, ctev_loc = loc })) + = do { pred' <- zonkTcType pred + ; return (CtGiven (GivenCt { ctev_pred = pred', ctev_evar = var, ctev_loc = loc })) } +zonkCtEvidence (CtWanted wanted@(WantedCt { ctev_pred = pred, ctev_rewriters = rws })) + = do { pred' <- zonkTcType pred + ; rws' <- zonkRewriterSet rws + ; return (CtWanted (wanted { ctev_pred = pred', ctev_rewriters = rws' })) } zonkSkolemInfo :: SkolemInfo -> ZonkM SkolemInfo zonkSkolemInfo (SkolemInfo u sk) = SkolemInfo u <$> zonkSkolemInfoAnon sk @@ -530,6 +548,103 @@ win. But c.f Note [Sharing when zonking to Type] in GHC.Tc.Zonk.Type. +%************************************************************************ +%* * + Zonking rewriter sets +* * +************************************************************************ +-} + +zonkCtRewriterSet :: Ct -> ZonkM Ct +zonkCtRewriterSet ct + | isGivenCt ct + = return ct + | otherwise + = case ct of + CEqCan eq@(EqCt { eq_ev = ev }) -> do { ev' <- zonkCtEvRewriterSet ev + ; return (CEqCan (eq { eq_ev = ev' })) } + CIrredCan ir@(IrredCt { ir_ev = ev }) -> do { ev' <- zonkCtEvRewriterSet ev + ; return (CIrredCan (ir { ir_ev = ev' })) } + CDictCan di@(DictCt { di_ev = ev }) -> do { ev' <- zonkCtEvRewriterSet ev + ; return (CDictCan (di { di_ev = ev' })) } + CQuantCan {} -> return ct + CNonCanonical ev -> do { ev' <- zonkCtEvRewriterSet ev + ; return (CNonCanonical ev') } + +zonkCtEvRewriterSet :: CtEvidence -> ZonkM CtEvidence +zonkCtEvRewriterSet ev@(CtGiven {}) + = return ev +zonkCtEvRewriterSet ev@(CtWanted wtd) + = do { rewriters' <- zonkRewriterSet (ctEvRewriters ev) + ; return (CtWanted $ setWantedCtEvRewriters wtd rewriters') } + +-- | Zonk a rewriter set; if a coercion hole in the set has been filled, +-- find all the free un-filled coercion holes in the coercion that fills it +zonkRewriterSet :: RewriterSet -> ZonkM RewriterSet +zonkRewriterSet (RewriterSet set) + = nonDetStrictFoldUniqSet go (return emptyRewriterSet) set + -- This does not introduce non-determinism, because the only + -- monadic action is to read, and the combining function is + -- commutative + where + go :: CoercionHole -> ZonkM RewriterSet -> ZonkM RewriterSet + go hole m_acc = unionRewriterSet <$> check_hole hole <*> m_acc + + check_hole :: CoercionHole -> ZonkM RewriterSet + check_hole hole + = do { m_co <- unpackCoercionHole_maybe hole + ; case m_co of + Nothing -> return (unitRewriterSet hole) -- Not filled + Just co -> unUCHM (check_co co) } -- Filled: look inside + + check_ty :: Type -> UnfilledCoercionHoleMonoid + check_co :: Coercion -> UnfilledCoercionHoleMonoid + (check_ty, _, check_co, _) = foldTyCo folder () + + folder :: TyCoFolder () UnfilledCoercionHoleMonoid + folder = TyCoFolder { tcf_view = noView + , tcf_tyvar = \ _ tv -> check_ty (tyVarKind tv) + , tcf_covar = \ _ cv -> check_ty (varType cv) + , tcf_hole = \ _ -> UCHM . check_hole + , tcf_tycobinder = \ _ _ _ -> () } + +newtype UnfilledCoercionHoleMonoid = UCHM { unUCHM :: ZonkM RewriterSet } + +instance Semigroup UnfilledCoercionHoleMonoid where + UCHM l <> UCHM r = UCHM (unionRewriterSet <$> l <*> r) + +instance Monoid UnfilledCoercionHoleMonoid where + mempty = UCHM (return emptyRewriterSet) + + +{- +************************************************************************ +* * + Checking for coercion holes +* * +************************************************************************ +-} + +-- | Is a coercion hole filled in? +isFilledCoercionHole :: CoercionHole -> ZonkM Bool +isFilledCoercionHole (CoercionHole { ch_ref = ref }) + = isJust <$> readTcRef ref + +-- | Retrieve the contents of a coercion hole. Panics if the hole +-- is unfilled +unpackCoercionHole :: CoercionHole -> ZonkM Coercion +unpackCoercionHole hole + = do { contents <- unpackCoercionHole_maybe hole + ; case contents of + Just co -> return co + Nothing -> pprPanic "Unfilled coercion hole" (ppr hole) } + +-- | Retrieve the contents of a coercion hole, if it is filled +unpackCoercionHole_maybe :: CoercionHole -> ZonkM (Maybe Coercion) +unpackCoercionHole_maybe (CoercionHole { ch_ref = ref }) = readTcRef ref + + +{- %************************************************************************ %* * Tidying ===================================== compiler/GHC/Tc/Zonk/Type.hs ===================================== @@ -28,12 +28,6 @@ module GHC.Tc.Zonk.Type ( -- ** 'ZonkEnv', and the 'ZonkT' and 'ZonkBndrT' monad transformers module GHC.Tc.Zonk.Env, - -- * Coercion holes - isFilledCoercionHole, unpackCoercionHole, unpackCoercionHole_maybe, - - -- * Rewriter sets - zonkRewriterSet, zonkCtRewriterSet, zonkCtEvRewriterSet, - -- * Tidying tcInitTidyEnv, tcInitOpenTidyEnv, @@ -55,7 +49,6 @@ import GHC.Tc.TyCl.Build ( TcMethInfo, MethInfo ) import GHC.Tc.Utils.Env ( tcLookupGlobalOnly ) import GHC.Tc.Utils.TcType import GHC.Tc.Utils.Monad ( newZonkAnyType, setSrcSpanA, liftZonkM, traceTc, addErr ) -import GHC.Tc.Types.Constraint import GHC.Tc.Types.Evidence import GHC.Tc.Errors.Types import GHC.Tc.Zonk.Env @@ -88,7 +81,6 @@ import GHC.Types.Id import GHC.Types.TypeEnv import GHC.Types.Basic import GHC.Types.SrcLoc -import GHC.Types.Unique.Set import GHC.Types.Unique.FM import GHC.Types.TyThing @@ -99,7 +91,6 @@ import GHC.Data.Bag import Control.Monad import Control.Monad.Trans.Class ( lift ) -import Data.Semigroup import Data.List.NonEmpty ( NonEmpty ) import Data.Foldable ( toList ) @@ -1956,89 +1947,3 @@ finding the free type vars of an expression is necessarily monadic operation. (consider /\a -> f @ b, where b is side-effected to a) -} -{- -************************************************************************ -* * - Checking for coercion holes -* * -************************************************************************ --} - --- | Is a coercion hole filled in? -isFilledCoercionHole :: CoercionHole -> TcM Bool -isFilledCoercionHole (CoercionHole { ch_ref = ref }) - = isJust <$> readTcRef ref - --- | Retrieve the contents of a coercion hole. Panics if the hole --- is unfilled -unpackCoercionHole :: CoercionHole -> TcM Coercion -unpackCoercionHole hole - = do { contents <- unpackCoercionHole_maybe hole - ; case contents of - Just co -> return co - Nothing -> pprPanic "Unfilled coercion hole" (ppr hole) } - --- | Retrieve the contents of a coercion hole, if it is filled -unpackCoercionHole_maybe :: CoercionHole -> TcM (Maybe Coercion) -unpackCoercionHole_maybe (CoercionHole { ch_ref = ref }) = readTcRef ref - -zonkCtRewriterSet :: Ct -> TcM Ct -zonkCtRewriterSet ct - | isGivenCt ct - = return ct - | otherwise - = case ct of - CEqCan eq@(EqCt { eq_ev = ev }) -> do { ev' <- zonkCtEvRewriterSet ev - ; return (CEqCan (eq { eq_ev = ev' })) } - CIrredCan ir@(IrredCt { ir_ev = ev }) -> do { ev' <- zonkCtEvRewriterSet ev - ; return (CIrredCan (ir { ir_ev = ev' })) } - CDictCan di@(DictCt { di_ev = ev }) -> do { ev' <- zonkCtEvRewriterSet ev - ; return (CDictCan (di { di_ev = ev' })) } - CQuantCan {} -> return ct - CNonCanonical ev -> do { ev' <- zonkCtEvRewriterSet ev - ; return (CNonCanonical ev') } - -zonkCtEvRewriterSet :: CtEvidence -> TcM CtEvidence -zonkCtEvRewriterSet ev@(CtGiven {}) - = return ev -zonkCtEvRewriterSet ev@(CtWanted wtd) - = do { rewriters' <- zonkRewriterSet (ctEvRewriters ev) - ; return (CtWanted $ setWantedCtEvRewriters wtd rewriters') } - --- | Check whether any coercion hole in a RewriterSet is still unsolved. --- Does this by recursively looking through filled coercion holes until --- one is found that is not yet filled in, at which point this aborts. -zonkRewriterSet :: RewriterSet -> TcM RewriterSet -zonkRewriterSet (RewriterSet set) - = nonDetStrictFoldUniqSet go (return emptyRewriterSet) set - -- this does not introduce non-determinism, because the only - -- monadic action is to read, and the combining function is - -- commutative - where - go :: CoercionHole -> TcM RewriterSet -> TcM RewriterSet - go hole m_acc = unionRewriterSet <$> check_hole hole <*> m_acc - - check_hole :: CoercionHole -> TcM RewriterSet - check_hole hole = do { m_co <- unpackCoercionHole_maybe hole - ; case m_co of - Nothing -> return (unitRewriterSet hole) - Just co -> unUCHM (check_co co) } - - check_ty :: Type -> UnfilledCoercionHoleMonoid - check_co :: Coercion -> UnfilledCoercionHoleMonoid - (check_ty, _, check_co, _) = foldTyCo folder () - - folder :: TyCoFolder () UnfilledCoercionHoleMonoid - folder = TyCoFolder { tcf_view = noView - , tcf_tyvar = \ _ tv -> check_ty (tyVarKind tv) - , tcf_covar = \ _ cv -> check_ty (varType cv) - , tcf_hole = \ _ -> UCHM . check_hole - , tcf_tycobinder = \ _ _ _ -> () } - -newtype UnfilledCoercionHoleMonoid = UCHM { unUCHM :: TcM RewriterSet } - -instance Semigroup UnfilledCoercionHoleMonoid where - UCHM l <> UCHM r = UCHM (unionRewriterSet <$> l <*> r) - -instance Monoid UnfilledCoercionHoleMonoid where - mempty = UCHM (return emptyRewriterSet) ===================================== compiler/GHC/Types/Basic.hs ===================================== @@ -87,7 +87,7 @@ module GHC.Types.Basic ( CompilerPhase(..), PhaseNum, beginPhase, nextPhase, laterPhase, Activation(..), isActive, competesWith, - isNeverActive, isAlwaysActive, activeInFinalPhase, + isNeverActive, isAlwaysActive, activeInFinalPhase, activeInInitialPhase, activateAfterInitial, activateDuringFinal, activeAfter, RuleMatchInfo(..), isConLike, isFunLike, ===================================== testsuite/tests/indexed-types/should_fail/T3330c.stderr ===================================== @@ -1,16 +1,24 @@ - -T3330c.hs:25:43: error: [GHC-18872] - • Couldn't match kind ‘* -> *’ with ‘*’ - When matching types - f1 :: * -> * - f1 x :: * - Expected: Der ((->) x) (Der f1 x) - Actual: R f1 - • In the first argument of ‘plug’, namely ‘rf’ +T3330c.hs:25:38: error: [GHC-25897] + • Could not deduce ‘Der f1 ~ f1’ + from the context: f ~ (f1 :+: g) + bound by a pattern with constructor: + RSum :: forall (f :: * -> *) (g :: * -> *). + R f -> R g -> R (f :+: g), + in an equation for ‘plug'’ + at T3330c.hs:25:8-17 + Expected: x -> f1 x + Actual: x -> Der f1 x + ‘f1’ is a rigid type variable bound by + a pattern with constructor: + RSum :: forall (f :: * -> *) (g :: * -> *). + R f -> R g -> R (f :+: g), + in an equation for ‘plug'’ + at T3330c.hs:25:8-17 + • The function ‘plug’ is applied to three visible arguments, + but its type ‘Rep f => Der f x -> x -> f x’ has only two 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:25:29) df :: Der f1 x (bound at T3330c.hs:25:25) rf :: R f1 (bound at T3330c.hs:25:13) - plug' :: R f -> Der f x -> x -> f x (bound at T3330c.hs:25:1) + ===================================== testsuite/tests/indexed-types/should_fail/T4174.stderr ===================================== @@ -1,6 +1,16 @@ - -T4174.hs:45:12: error: [GHC-18872] - • Couldn't match type ‘False’ with ‘True’ - arising from a use of ‘sync_large_objects’ +T4174.hs:45:12: error: [GHC-25897] + • Couldn't match type ‘a’ with ‘SmStep’ + Expected: m (Field (Way (GHC6'8 minor) n t p) a b) + Actual: m (Field (WayOf m) SmStep RtsSpinLock) + ‘a’ is a rigid type variable bound by + the type signature for: + testcase :: forall (m :: * -> *) minor n t p a b. + Monad m => + m (Field (Way (GHC6'8 minor) n t p) a b) + at T4174.hs:44:1-63 • In the expression: sync_large_objects In an equation for ‘testcase’: testcase = sync_large_objects + • Relevant bindings include + testcase :: m (Field (Way (GHC6'8 minor) n t p) a b) + (bound at T4174.hs:45:1) + ===================================== testsuite/tests/indexed-types/should_fail/T8227.stderr ===================================== @@ -13,12 +13,3 @@ T8227.hs:24:27: error: [GHC-83865] absoluteToParam :: Scalar (V a) -> a -> Scalar (V a) (bound at T8227.hs:24:1) -T8227.hs:24:48: error: [GHC-27958] - • Couldn't match type ‘p0’ with ‘Scalar (V p0)’ - arising from a type equality Scalar (V a) ~ Scalar (V p0) -> p0 - The type variable ‘p0’ is ambiguous - • In the second argument of ‘arcLengthToParam’, namely ‘eps’ - In the expression: arcLengthToParam eps eps - In an equation for ‘absoluteToParam’: - absoluteToParam eps seg = arcLengthToParam eps eps - ===================================== testsuite/tests/simplCore/should_compile/T25703.hs ===================================== @@ -0,0 +1,7 @@ +module T25703 where + +f :: (Eq a, Show b) => a -> b -> Int +f x y = f x y + +goo :: forall x. (Eq x) => x -> Int +goo arg = f arg (3::Int) ===================================== testsuite/tests/simplCore/should_compile/T25703.stderr ===================================== @@ -0,0 +1,2 @@ +Rule fired: SPEC f @_ @Int (T25703) +Rule fired: SPEC f @_ @Int (T25703) ===================================== testsuite/tests/simplCore/should_compile/T25703a.hs ===================================== @@ -0,0 +1,69 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} + +{-# OPTIONS_GHC -O2 -fspecialise-aggressively #-} + +-- This pragma is just here to pretend that the function body of 'foo' is huge +-- and should never be inlined. +{-# OPTIONS_GHC -funfolding-use-threshold=-200 #-} + +module T25703a where + +import Data.Kind +import Data.Type.Equality +import Data.Proxy +import GHC.TypeNats + +-- Pretend this is some big dictionary that absolutely must get +-- specialised away for performance reasons. +type C :: Nat -> Constraint +class C i where + meth :: Proxy i -> Double +instance C 0 where + meth _ = 0.1 +instance C 1 where + meth _ = 1.1 +instance C 2 where + meth _ = 2.1 + +{-# INLINEABLE foo #-} +foo :: forall a (n :: Nat) (m :: Nat) + . ( Eq a, C n, C m ) + => a -> ( Proxy n, Proxy m ) -> Int -> Double +-- Pretend this is a big complicated function, too big to inline, +-- for which we absolutely must specialise away the 'C n', 'C m' +-- dictionaries for performance reasons. +foo a b c + = if a == a + then meth @n Proxy + fromIntegral c + else 2 * meth @m Proxy + +-- Runtime dispatch to a specialisation of 'foo' +foo_spec :: forall a (n :: Nat) (m :: Nat) + . ( Eq a, KnownNat n, KnownNat m ) + => a -> ( Proxy n, Proxy m ) -> Int -> Double +foo_spec a b c + | Just Refl <- sameNat @n @0 Proxy Proxy + , Just Refl <- sameNat @m @0 Proxy Proxy + = foo @a @0 @0 a b c + | Just Refl <- sameNat @n @0 Proxy Proxy + , Just Refl <- sameNat @m @1 Proxy Proxy + = foo @a @0 @1 a b c + | Just Refl <- sameNat @n @1 Proxy Proxy + , Just Refl <- sameNat @m @1 Proxy Proxy + = foo @a @1 @1 a b c + | Just Refl <- sameNat @n @0 Proxy Proxy + , Just Refl <- sameNat @m @2 Proxy Proxy + = foo @a @0 @2 a b c + | Just Refl <- sameNat @n @1 Proxy Proxy + , Just Refl <- sameNat @m @2 Proxy Proxy + = foo @a @1 @2 a b c + | Just Refl <- sameNat @n @2 Proxy Proxy + , Just Refl <- sameNat @m @2 Proxy Proxy + = foo @a @2 @2 a b c + | otherwise + = error $ unlines + [ "f: no specialisation" + , "n: " ++ show (natVal @n Proxy) + , "m: " ++ show (natVal @m Proxy) + ] ===================================== testsuite/tests/simplCore/should_compile/T25703a.stderr ===================================== @@ -0,0 +1,6 @@ +Rule fired: SPEC foo @_ @2 @2 (T25703a) +Rule fired: SPEC foo @_ @1 @2 (T25703a) +Rule fired: SPEC foo @_ @0 @2 (T25703a) +Rule fired: SPEC foo @_ @1 @1 (T25703a) +Rule fired: SPEC foo @_ @0 @1 (T25703a) +Rule fired: SPEC foo @_ @0 @0 (T25703a) ===================================== testsuite/tests/simplCore/should_compile/T25965.hs ===================================== @@ -0,0 +1,18 @@ +{-# LANGUAGE TypeFamilies #-} +{-# OPTIONS_GHC -O -fpolymorphic-specialisation #-} + +module Foo where + +type family F a + +data T a = T1 + +instance Eq (T a) where { (==) x y = False } + +foo :: Eq a => a -> Bool +foo x | x==x = True + | otherwise = foo x + +bar :: forall b. b -> T (F b) -> Bool +bar y x = foo x + ===================================== testsuite/tests/simplCore/should_compile/all.T ===================================== @@ -543,3 +543,8 @@ test('T25883c', normal, compile_grep_core, ['']) test('T25883d', [extra_files(['T25883d_import.hs'])], multimod_compile_filter, ['T25883d', '-O -ddump-simpl -dno-typeable-binds -dsuppress-all -dsuppress-uniques', r'grep -e "y ="']) test('T25976', [grep_errmsg('Dead Code')], compile, ['-O -ddump-simpl -dsuppress-uniques -dno-typeable-binds']) + +test('T25965', normal, compile, ['-O']) +test('T25703', [grep_errmsg(r'SPEC')], compile, ['-O -fpolymorphic-specialisation -ddump-rule-firings']) +test('T25703a', [grep_errmsg(r'SPEC')], compile, ['-O -fpolymorphic-specialisation -ddump-rule-firings']) + ===================================== testsuite/tests/typecheck/should_compile/T25266a.stderr ===================================== @@ -1,16 +1,16 @@ -T25266a.hs:10:41: error: [GHC-25897] - • Could not deduce ‘p1 ~ p2’ +T25266a.hs:10:39: error: [GHC-25897] + • Could not deduce ‘p2 ~ p1’ from the context: a ~ Int bound by a pattern with constructor: T1 :: T Int, in a case alternative at T25266a.hs:10:23-24 - ‘p1’ is a rigid type variable bound by + ‘p2’ is a rigid type variable bound by the inferred type of f :: p1 -> p2 -> T a -> Int at T25266a.hs:(9,1)-(11,40) - ‘p2’ is a rigid type variable bound by + ‘p1’ is a rigid type variable bound by the inferred type of f :: p1 -> p2 -> T a -> Int at T25266a.hs:(9,1)-(11,40) - • In the expression: y + • In the expression: x In the first argument of ‘length’, namely ‘[x, y]’ In the expression: length [x, y] • Relevant bindings include ===================================== testsuite/tests/typecheck/should_fail/T18851.stderr ===================================== @@ -1,7 +1,7 @@ - T18851.hs:35:5: error: [GHC-18872] - • Couldn't match type ‘B’ with ‘A’ - arising from a superclass required to satisfy ‘C int0 A’, + • Couldn't match type ‘Bool’ with ‘B’ + arising from a superclass required to satisfy ‘C Int B’, arising from a use of ‘f’ • In the expression: f @A @B In an equation for ‘g’: g = f @A @B + View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/22070ca0b415d0f9d644033d30538f0... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/22070ca0b415d0f9d644033d30538f0... You're receiving this email because of your account on gitlab.haskell.org.