Simon Peyton Jones pushed to branch wip/T27844 at Glasgow Haskell Compiler / GHC Commits: 234bab08 by Vladislav Zavialov at 2026-09-29T17:22:54-04:00 Add regression test for #7803 Commit 2effe18ab5, first shipped with GHC 8.2.1, fixed #7803 "Superclass methods are left unspecialized". This change turns the example from the ticket description into a regression test, checking that foo1 is fully specialised at Double, with no calls to the overloaded exp5Tail. Closes #7803 Assisted-by: Claude Opus 5 - - - - - b780800d by Simon Peyton Jones at 2026-09-29T23:42:10+01:00 Refactor and simplify solver's unification code Ticket #27844 showed that GHC's constraint solver could miss an occurs check, and thereby build an infinite type. This patch significantly simplifes the code in GHC.Tc.Solver.Equality.canEqCanLHSFinish_try_unification GHC.Tc.Solver.Equality.canEqCanLHSFinish_no_unification It is now significantly simpler, and requires much less subtle reasoning to understand. Main changes * If `canEqCanLHSFinish_try_unification` fails to unify, it now /always/ calls `canEqCanLHSFinish_no_unification` rather than trying to finish the job itself. * `GHC.Tc.Solver.Monad.checkTypeEq` is moved from Monad into Equality, and renamed to `GHC.Tc.Solver.Equality.checkTypeEqNoUnification`. * `canEqCanLHSFinish_no_unification` calls `checkTypeEqNoUnification` to test the invariants for an inert equality. Before this MR there was a special case for `do_not_prevent_rewriting`, but that has gone; instead it's just a consequence of the flags passed to `checkTyEqRhs`, documented in the `PuOK` case of `canEqCanLHSFinish_no_unification`. * There is only one bit of "swap back" code, in `finish_no_unify` in `canEqCanLHSFinish_try_unification. Previously this code was duplicated. * No need to gather coercion holes in the `PuOK` case of `canEqCanLHSFinish_no_unification`. See documentation with that code. - - - - - 15 changed files: - + changelog.d/T27844 - compiler/GHC/Runtime/Heap/Inspect.hs - compiler/GHC/Tc/Solver/Equality.hs - compiler/GHC/Tc/Solver/InertSet.hs - compiler/GHC/Tc/Solver/Monad.hs - compiler/GHC/Tc/Types/Constraint.hs - compiler/GHC/Tc/Utils/Unify.hs - testsuite/tests/indexed-types/should_fail/T9662.stderr - + testsuite/tests/simplCore/should_compile/T7803.hs - + testsuite/tests/simplCore/should_compile/T7803.stderr - + testsuite/tests/simplCore/should_compile/T7803a.hs - testsuite/tests/simplCore/should_compile/all.T - + testsuite/tests/typecheck/should_fail/T27844.hs - + testsuite/tests/typecheck/should_fail/T27844.stderr - testsuite/tests/typecheck/should_fail/all.T Changes: ===================================== changelog.d/T27844 ===================================== @@ -0,0 +1,9 @@ +section: compiler +issues: #27844 +mrs: !16723 +synopsis: + Reinstate a missing occurs check in the constraint solver +description: + Simplifies code in GHC's type-constraint solver, thereby fixing an outright + compiler loop (via a missing occurs check). + ===================================== compiler/GHC/Runtime/Heap/Inspect.hs ===================================== @@ -630,7 +630,7 @@ be sigmas and not taus. ~~~~~~~~~~~~~~~~~~~~~~ In the GHCi debugger we use unification variables whose MetaInfo is RuntimeUnkTv. The special property of a RuntimeUnkTv is that it can -unify with a polytype (see GHC.Tc.Utils.Unify.checkTypeEq). +unify with a polytype (see GHC.Tc.Solver.Equality.checkTypeEqNoUnification). If we don't do this `:print <term>` will fail if the type of <term> has nested `forall`s or `=>`s. ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -21,6 +21,7 @@ import GHC.Tc.Types.Evidence import GHC.Tc.Types.Constraint import GHC.Tc.Types.CtLoc import GHC.Tc.Types.Origin +import GHC.Tc.Types( TcM ) import GHC.Tc.Utils.Unify import GHC.Tc.Utils.TcType import GHC.Tc.Instance.Family ( tcUnwrapNewtype_maybe ) @@ -36,8 +37,8 @@ import GHC.Core.Coercion import GHC.Core.Reduction import GHC.Core.FamInstEnv ( FamInstEnvs ) import GHC.Core -import GHC.Types.Var +import GHC.Types.Var import GHC.Types.Basic import GHC.Types.Name.Reader import GHC.Types.Var.Env @@ -49,6 +50,8 @@ import GHC.Utils.Misc import GHC.Utils.Monad import GHC.Data.Pair +import GHC.Data.Bag + import Control.Monad import Data.Maybe ( isJust, isNothing ) import Data.List ( zip4 ) @@ -406,11 +409,13 @@ canonicaliseEquality -- hold. canonicaliseEquality ev eq_rel ty1 ty2 - = Stage $ do { traceTcS "canonicaliseEquality" $ + = Stage $ do { traceTcS "canonicaliseEquality {" $ vcat [ ppr ev, ppr eq_rel, ppr ty1, ppr ty2 ] ; rdr_env <- getGlobalRdrEnvTcS ; fam_insts <- getFamInstEnvs - ; can_eq_nc initCanEqState rdr_env fam_insts ev eq_rel ty1 ty1 ty2 ty2 } + ; res <- can_eq_nc initCanEqState rdr_env fam_insts ev eq_rel ty1 ty1 ty2 ty2 + ; traceTcS "canonicaliseEquality }" (ppr res) + ; return res } -- | Main worker function for 'canonicaliseEquality'. -- @@ -1822,7 +1827,7 @@ Ticket #10009, a very nasty example: g :: forall a. (UnF (F a) ~ a) => a -> () g _ = f (undefined :: F a) -For g we get [G] g1 : UnF (F a) ~ a +For g we get [G] g1 : UnF (F a) ~ a [W] w1 : UnF (F beta) ~ beta [W] w2 : F a ~ F beta @@ -2205,63 +2210,45 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs , TyVarLHS lhs_tv <- lhs = do { given_eq_lvl <- getInnermostGivenEqLevel ; case simpleUnifyCheck UC_Solver given_eq_lvl lhs_tv rhs of - SUC_CanUnify -> - unify lhs_tv (mkReflRedn Nominal rhs) - SUC_CannotUnify - | Just can_rhs <- canTyFamEqLHS_maybe rhs - -> swap_and_finish lhs_tv can_rhs -- See Note [Orienting TyVarLHS/TyFamLHS] - | otherwise - -> finish_no_unify - SUC_NotSure -> + SUC_CannotUnify -> finish_no_unify + SUC_CanUnify -> do_unification lhs_tv (mkReflRedn Nominal rhs) + SUC_NotSure -> -- We have a touchable unification variable on the left, -- and the top-shape check succeeded. These are both guaranteed -- by the fact that simpleUnifyCheck did not return SUC_CannotUnify. + -- + -- Next, do a fully `checkTyEqRhs` check to see if we can unify + -- See Note [checkTyEqRhs] in GHC.Tc.Utils.Unify do { let flags = unifyingLHSMetaTyVar_TEFTask ev lhs_tv ; check_result <- wrapTcS (checkTyEqRhs flags rhs) + ; traceTcS "canEqCanLHSFinish_try_unification" $ + vcat [ text "lhs" <+> ppr lhs + , text "rhs" <+> ppr rhs + , text "check_result" <+> ppr check_result ] ; case check_result of - PuOK cts rhs_redn -> - do { emitWork cts - ; unify lhs_tv rhs_redn } - PuFail reason - | Just can_rhs <- canTyFamEqLHS_maybe rhs - -> swap_and_finish lhs_tv can_rhs -- See Note [Orienting TyVarLHS/TyFamLHS] - | reason `cterHasOnlyProblems` do_not_prevent_rewriting - -> - -- ContinueWith, to allow using this constraint for - -- rewriting (e.g. alpha[2] ~ beta[3]). - do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped lhs rhs - ; continueWith $ Right $ - EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel - , eq_lhs = lhs , eq_rhs = rhs } - } - | otherwise - -> try_irred reason - } + PuFail {} -> finish_no_unify + PuOK cts rhs_redn -> do { emitWork cts + ; do_unification lhs_tv rhs_redn } } } -- Otherwise unification is off the table | otherwise = finish_no_unify where - -- We can't unify, but this equality can go in the inert set - -- and be used to rewrite other constraints. - finish_no_unify = - canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs - - -- We can't unify, and this equality should not be used to rewrite - -- other constraints (e.g. because it has an occurs check). - -- So add it to the inert Irreds. - try_irred reason = - tryIrredInstead reason ev eq_rel swapped lhs rhs - - -- We can't unify as-is, and want to flip the equality around. - -- Example: alpha ~ F tys, flip it around to become the canonical - -- equality f tys ~ alpha. - swap_and_finish tv can_rhs = - swapAndFinish ev eq_rel swapped (mkTyVarTy tv) can_rhs - - -- Phew! Finally! We can unify; go ahead and do so. - unify tv rhs_redn = + -- finish_no_unify: abandon the attempt to unify, and instead hand off to + -- canEqCanLHSFinish_no_unification + -- First, though, if we have (tv ~ F tys) + -- swap it over so we get (F tys ~ tv), with `F tys` on the LHS + -- See Note [Orienting TyVarLHS/TyFamLHS] + finish_no_unify + | TyVarLHS lhs_tv <- lhs + , Just can_rhs <- canTyFamEqLHS_maybe rhs + = canEqCanLHSFinish_no_unification ev eq_rel (flipSwap swapped) can_rhs (mkTyVarTy lhs_tv) + | otherwise + = canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs + + -- do_unification: Phew! Finally! We can unify; go ahead and do so. + do_unification tv rhs_redn = do { -- In the common case where rhs_redn is Refl, we don't need to rewrite -- the evidence, even if swapped=IsSwapped. Suppose the original was -- [W] co : Int ~ alpha @@ -2273,7 +2260,8 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs else rewriteEqEvidence ev swapped (mkReflRedn Nominal (mkTyVarTy tv)) rhs_redn emptyCoHoleSet - -- emptyCoHoleSet: rhs_redn has no CoercionHoles + -- emptyCoHoleSet: we are about to /solve/ this + -- constraint, so its CoHoleSet doesn't matter ; let tv_ty = mkTyVarTy tv final_rhs = reductionReducedType rhs_redn @@ -2297,45 +2285,44 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs ; return (Stop new_ev (text "Solved by unification")) } --------------------------- --- Unification is off the table canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs - = do { -- Do checkTypeEq to guarantee (TyEq:OC), (TyEq:F) + -- We can't unify, but we can see if this equality can go in the inert set + -- and be used to rewrite other constraints. + -- See Note [Equalities where unification fails] + = do { -- Do checkTypeEqNoUnfication to guarantee (TyEq:OC), (TyEq:F) -- Must do the occurs check even on tyvar/tyvar equalities, -- in case have x ~ (y :: ..x...); this is #12593. - ; check_result <- checkTypeEq ev eq_rel lhs rhs - - ; let lhs_ty = canEqLHSType lhs + ; check_result <- checkTypeEqNoUnification ev eq_rel lhs rhs ; case check_result of PuFail reason - - -- If we had F a ~ G (F a), which gives an occurs check, - -- then swap it to G (F a) ~ F a, which does not - -- However `swap_for_size` above will orient it with (G (F a)) on - -- the left anwyway. `swap_for_rewriting` "wins", but that doesn't - -- matter: in the occurs check case swap_for_rewriting will be moot. - -- TL;DR: the next four lines of code are redundant - -- I'm leaving them here in case they become relevant again --- | TyFamLHS {} <- lhs --- , Just can_rhs <- canTyFamEqLHS_maybe rhs --- , reason `cterHasOnlyProblem` cteSolubleOccurs --- -> swapAndFinish ev eq_rel swapped lhs_ty can_rhs --- | otherwise - - | reason `cterHasOnlyProblems` do_not_prevent_rewriting - -> do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped lhs rhs - ; continueWith $ Right $ - EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel - , eq_lhs = lhs , eq_rhs = rhs } - } - - | otherwise - -> tryIrredInstead reason ev eq_rel swapped lhs rhs + -> -- We can't unify, and this equality should not be used to rewrite + -- other constraints (e.g. because it has an occurs check). + -- So add it to the inert Irreds. + do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped lhs rhs + ; finishCanWithIrred (NonCanonicalReason reason) new_ev } PuOK new_eqs rhs_redn - -> do { emitWork new_eqs - ; let new_holes = rewriterSetFromCts new_eqs + -> -- Put this constraint into the inert set, so that it will be used + -- to solve or rewrite other constraints. + -- + -- NB: checkTypeEqNoUnification does not check for + -- (b) skolem-escape (tefTyVar_levelCheck = LC_None) + -- (a) concreteness (tefTyVar_concreteCheck = CC_None) + -- So an equality whose only problem is e.g. skolem-escape will + -- return PuOK, will be put in the inert set, will be used for + -- rewriting. That is fine. + -- + -- assertPpr (isEmptyCts new_eqs): + -- checkTypeEqNoUnification does neither promotion nor type-family + -- flattening for Wanteds, and hence creates no equalities to solve + assertPpr (isEmptyCts new_eqs) + (vcat [ text "new_eqs" <+> ppr new_eqs + , text "rhs_redn" <+> ppr rhs_redn + , text "lhs" <+> ppr lhs + , text "rhs" <+> ppr rhs ]) $ + do { let lhs_ty = canEqLHSType lhs lhs_redn = mkReflRedn (eqRelRole eq_rel) lhs_ty - ; new_ev <- rewriteEqEvidence ev swapped lhs_redn rhs_redn new_holes + ; new_ev <- rewriteEqEvidence ev swapped lhs_redn rhs_redn emptyCoHoleSet -- Important: even if the coercion is Refl, -- * new_ev has reductionReducedType on the RHS @@ -2346,45 +2333,56 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs , eq_lhs = lhs , eq_rhs = reductionReducedType rhs_redn } } } --- | Some problems prevent /unification/ but not /rewriting/: --- --- Skolem-escape: if we have [W] alpha[2] ~ Maybe b[3] --- we can't unify (skolem-escape); but it /is/ canonical, --- and hence we /can/ use it for rewriting --- --- Concrete-ness: alpha[conc] ~ b[sk] --- We can use it to rewrite; we still have to solve the original -do_not_prevent_rewriting :: CheckTyEqResult -do_not_prevent_rewriting = cteProblem cteSkolemEscape S.<> - cteProblem cteConcrete +checkTypeEqNoUnification :: CtEvidence -> EqRel -> CanEqLHS -> TcType + -> TcS (PuResult Ct Reduction) +-- Used for general CanEqLHSs, when we have decided that we cannot unify +checkTypeEqNoUnification ev eq_rel lhs rhs = + case ev of + CtGiven {} -> + do { traceTcS "checkTypeEqNoUnification (given) {" (vcat [ text "lhs:" <+> ppr lhs + , text "rhs:" <+> ppr rhs ]) + ; check_result <- wrapTcS (checkTyEqRhs given_flags rhs) + ; traceTcS "checkTypeEqNoUnification }" (ppr check_result) + ; case check_result of + PuFail reason -> return (PuFail reason) + PuOK prs redn -> do { new_givens <- mapBagM mk_new_given prs + ; emitWork new_givens + ; updInertSet (addCycleBreakerBindings prs) + ; return (pure redn) } } + CtWanted {} -> do { traceTcS "checkTypeEqNoUnification (wanted) {" $ + vcat [ text "lhs:" <+> ppr lhs + , text "rhs:" <+> ppr rhs ] + ; check_result <- wrapTcS (checkTyEqRhs wanted_flags rhs) + ; traceTcS "checkTypeEqNoUnification }" (ppr check_result) + ; return check_result } + where + wanted_flags :: TyEqFlags TcM Ct + wanted_flags = notUnifying_TEFTask occ_prob lhs + -- See Note [Don't cycle-break Wanteds when not unifying] + + given_flags :: TyEqFlags TcM (TcTyVar, TcType) + given_flags = wanted_flags { tef_fam_app = mkTEFA_Break ev eq_rel BreakGiven } + -- TEFA_Break used for: [G] a ~ Maybe (F a) + -- or [G] F a ~ Maybe (F a) + + -- occ_prob: see Note [Occurs check and representational equality] + occ_prob = case eq_rel of + NomEq -> cteInsolubleOccurs + ReprEq -> cteSolubleOccurs + + --------------------------- + mk_new_given :: (TcTyVar, TcType) -> TcS Ct + mk_new_given (new_tv, fam_app) + = mkNonCanonical . CtGiven <$> newGivenEv cb_loc (given_pred, given_term) + where + new_ty = mkTyVarTy new_tv + given_pred = mkNomEqPred fam_app new_ty + given_term = evCoercion $ mkNomReflCo new_ty -- See Detail (4) of Note ----------------------- -swapAndFinish :: CtEvidence -> EqRel -> SwapFlag - -> TcType -> CanEqLHS -- ty ~ F tys - -> TcS (StopOrContinue (Either unused EqCt)) --- We have an equality alpha ~ F tys, that we can't unify e.g because 'tys' --- mentions alpha, it would not be a canonical constraint as-is. --- We want to flip it to (F tys ~ a), whereupon it is canonical -swapAndFinish ev eq_rel swapped lhs_ty can_rhs - = do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel (flipSwap swapped) can_rhs lhs_ty - ; continueWith $ Right $ - EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel - , eq_lhs = can_rhs, eq_rhs = lhs_ty } } + -- See Detail (7) of the Note + cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin ---------------------- -tryIrredInstead :: CheckTyEqResult -> CtEvidence - -> EqRel -> SwapFlag -> CanEqLHS -> TcType - -> TcS (StopOrContinue (Either IrredCt unused)) --- We have a non-canonical equality --- We still swap it if 'swapped' says so, so that it is oriented --- in the direction that the error-reporting machinery --- expects it; e.g. (m ~ t m) rather than (t m ~ m) --- This is not very important, and only affects error reporting. -tryIrredInstead reason ev eq_rel swapped lhs rhs - = do { traceTcS "cantMakeCanonical" (ppr reason $$ ppr lhs $$ ppr rhs) - ; new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped lhs rhs - ; finishCanWithIrred (NonCanonicalReason reason) new_ev } - finishCanWithIrred :: CtIrredReason -> CtEvidence -> TcS (StopOrContinue (Either IrredCt a)) finishCanWithIrred reason ev @@ -2404,8 +2402,63 @@ canEqReflexive ev eq_rel ty = do { setEqIfWanted ev (mkReflCPH eq_rel ty) ; stopWith ev "Solved by reflexivity" } -{- Note [Equalities with heterogeneous kinds] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +{- Note [Equalities where unification fails] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +If we can't unify, but the equality is canonical, we still want to add it to the +inert set so that it can be used to rewrite other Wanteds. (There are many +reasons by unification might not happen: the LHS is not a touchable unification +variable, it has rewriters, it's a Given etc.) + +* In this case we call `checkTypeEqNoUnification`to see if it is canonical (which + in turn calls `checkTypeEqRhs` with suitable flags). + +* NB: we do /not/ try to take advantage of the case where + `canEqCanLHSFinish_try_unification` has already called `checkTyEqRhs`; doing so + caused #27844. (The first call did fam-app breaking, which concealed a genuine + occurs check.) It's just too clever; better to do the simple thing. + +Note [Don't cycle-break Wanteds when not unifying] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consdier + [W] a[2] ~ Maybe (F a[2]) + +Should we cycle-break this Wanted, thus? + + [W] a[2] ~ Maybe delta[2] + [W] delta[2] ~ F a[2] + +For a start, this is dodgy because we might just unify delta, thus undoing +what we have done, and getting an infinite loop in the solver. Even if we +somehow prevented ourselves from doing so, is there any merit in the split? +Maybe: perhaps we can use that equality on `a` to unlock other constraints? +Consider + type instance F (Maybe _) = Bool + + [G] g1: a ~ Maybe Bool + [W] w1: a ~ Maybe (F a) + +If we loop-break w1 to get + [W] w1': a ~ Maybe gamma + [W] w3: gamma ~ F a +Now rewrite w3 with w1' + [W] w3': gamma ~ F (Maybe gamma) +Now use the type instance to get + gamma := Bool +Now we are left with + [W] w1': a ~ Maybe Bool +which we can solve from the Given. + +BUT in this situation we could have rewritten the +/original/ Wanted from the Given, like this: + [W] w1': Maybe Bool ~ Maybe (F (Maybe Bool)) +and that is readily soluble. + +In short: loop-breaking Wanteds, when we aren't unifying, +seems of no merit. Hence TEFA_Recurse, rather than TEFA_Break, +in `wanted_flags` in `checkTypeEqNoUnification`. + +Note [Equalities with heterogeneous kinds] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ What do we do when we have an equality (tv :: k1) ~ (rhs :: k2) @@ -2587,8 +2640,7 @@ The details depend on whether we're working with a Given or a Wanted. Given ----- We emit a new Given, [G] F a ~ cbv, equating the type family application -to our new cbv. This is actually done by `break_given` in -`GHC.Tc.Solver.Monad.checkTypeEq`. +to our new cbv. This is actually done by `break_given` in `checkTypeEqNoUnification`. Note its orientation: The type family ends up on the left; see Note [Orienting TyFamLHS/TyFamLHS]. No special treatment for @@ -3076,8 +3128,6 @@ inertsEqsCanDischarge inerts (EqCt { eq_lhs = lhs_w, eq_rhs = rhs_w inertsEqsCanDischarge _ _ = Nothing - - {- Note [Do not unify Givens] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider this GADT match @@ -3143,34 +3193,6 @@ Wrinkles: we should kick out `co` so that we can now unify it, which might unlock other stuff. See `kickOutAfterFillingCoercionHole` in GHC.Tc.Solver.Monad. - -Note [Solve by unification] -~~~~~~~~~~~~~~~~~~~~~~~~~~~ -If we solve - alpha[n] ~ ty -by unification, there are two cases to consider - -* TouchableSameLevel: if the ambient level is 'n', then - we can simply update alpha := ty, and do nothing else - -* TouchableOuterLevel free_metas n: if the ambient level is greater than - 'n' (the level of alpha), in addition to setting alpha := ty we must - do two other things: - - 1. Promote all the free meta-vars of 'ty' to level n. After all, - alpha[n] is at level n, and so if we set, say, - alpha[n] := Maybe beta[m], - we must ensure that when unifying beta we do skolem-escape checks - etc relevant to level n. Simple way to do that: promote beta to - level n. - - 2. Set the Unification Level Flag to record that a level-n unification has - taken place. See Note [WhatUnifications] in GHC.Tc.Utils.Unify - -NB: TouchableSameLevel is just an optimisation for TouchableOuterLevel. Promotion -would be a no-op, and setting the unification flag unnecessarily would just -make the solver iterate more often. (We don't need to iterate when unifying -at the ambient level because of the kick-out mechanism.) -} ===================================== compiler/GHC/Tc/Solver/InertSet.hs ===================================== @@ -983,7 +983,7 @@ How do we establish these conditions? with S(fw,_). * (T3) is guaranteed by an occurs-check on the work item. - This is done during canonicalisation, in checkTypeEq; invariant + This is done during canonicalisation, in checkTyEqRhs; invariant (TyEq:OC) of CEqCan. See also Note [EqCt occurs check] in GHC.Tc.Types.Constraint. * (T4) is established by GHC.Tc.Solver.Monad.kickOutRewritable. If the inert ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -117,10 +117,7 @@ module GHC.Tc.Solver.Monad ( getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS, matchFam, matchFamTcM, checkWellLevelledDFun, - pprEq, - - -- Enforcing invariants for type equalities - checkTypeEq + pprEq ) where import GHC.Prelude @@ -2302,52 +2299,6 @@ wrapUnifier rws loc role do_unifications ************************************************************************ -} -checkTypeEq :: CtEvidence -> EqRel -> CanEqLHS -> TcType - -> TcS (PuResult Ct Reduction) --- Used for general CanEqLHSs, ones that do --- not have a touchable type variable on the LHS (i.e. not unifying) -checkTypeEq ev eq_rel lhs rhs = - case ev of - CtGiven {} -> - do { traceTcS "checkTypeEq {" (vcat [ text "lhs:" <+> ppr lhs - , text "rhs:" <+> ppr rhs ]) - ; check_result <- wrapTcS (checkTyEqRhs given_flags rhs) - ; traceTcS "checkTypeEq }" (ppr check_result) - ; case check_result of - PuFail reason -> return (PuFail reason) - PuOK prs redn -> do { new_givens <- mapBagM mk_new_given prs - ; emitWork new_givens - ; updInertSet (addCycleBreakerBindings prs) - ; return (pure redn) } } - CtWanted {} -> wrapTcS (checkTyEqRhs wanted_flags rhs) - where - wanted_flags :: TyEqFlags TcM Ct - wanted_flags = notUnifying_TEFTask occ_prob lhs - -- checkTypeEq deals only with the non-unifying case - - given_flags :: TyEqFlags TcM (TcTyVar, TcType) - given_flags = wanted_flags { tef_fam_app = mkTEFA_Break ev eq_rel BreakGiven } - -- TEFA_Break used for: [G] a ~ Maybe (F a) - -- or [W] F a ~ Maybe (F a) - - -- occ_prob: see Note [Occurs check and representational equality] - occ_prob = case eq_rel of - NomEq -> cteInsolubleOccurs - ReprEq -> cteSolubleOccurs - - --------------------------- - mk_new_given :: (TcTyVar, TcType) -> TcS Ct - mk_new_given (new_tv, fam_app) - = mkNonCanonical . CtGiven <$> newGivenEv cb_loc (given_pred, given_term) - where - new_ty = mkTyVarTy new_tv - given_pred = mkNomEqPred fam_app new_ty - given_term = evCoercion $ mkNomReflCo new_ty -- See Detail (4) of Note - - -- See Detail (7) of the Note - cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin - -------------------------- -- | Fill in CycleBreakerTvs with the variables they stand for. -- See Note [Type equality cycles] in GHC.Tc.Solver.Equality restoreTyVarCycles :: InertSet -> TcM () @@ -2363,43 +2314,4 @@ restoreTyVarCycles is (a ~R# b a) is soluble if b later turns out to be Identity So we treat this as a "soluble occurs check". -Note [Don't cycle-break Wanteds when not unifying] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consdier - [W] a[2] ~ Maybe (F a[2]) - -Should we cycle-break this Wanted, thus? - - [W] a[2] ~ Maybe delta[2] - [W] delta[2] ~ F a[2] - -For a start, this is dodgy because we might just unify delta, thus undoing -what we have done, and getting an infinite loop in the solver. Even if we -somehow prevented ourselves from doing so, is there any merit in the split? -Maybe: perhaps we can use that equality on `a` to unlock other constraints? -Consider - type instance F (Maybe _) = Bool - - [G] g1: a ~ Maybe Bool - [W] w1: a ~ Maybe (F a) - -If we loop-break w1 to get - [W] w1': a ~ Maybe gamma - [W] w3: gamma ~ F a -Now rewrite w3 with w1' - [W] w3': gamma ~ F (Maybe gamma) -Now use the type instance to get - gamma := Bool -Now we are left with - [W] w1': a ~ Maybe Bool -which we can solve from the Given. - -BUT in this situation we could have rewritten the -/original/ Wanted from the Given, like this: - [W] w1': Maybe Bool ~ Maybe (F (Maybe Bool)) -and that is readily soluble. - -In short: loop-breaking Wanteds, when we aren't unifying, -seems of no merit. Hence TEFA_Recurse, rather than TEFA_Break, -in `wanted_flags` in `checkTypeEq`. -} ===================================== compiler/GHC/Tc/Types/Constraint.hs ===================================== @@ -524,7 +524,7 @@ isInsolubleReason (InsolubleFunDepReason {}) = True ------------------------------------------------------------------------------ -- | A /set/ of problems in checking the validity of a type equality. --- See 'checkTypeEq'. +-- See 'GHC.Tc.Utils.Unify.checkTyEqRhs'. newtype CheckTyEqResult = CTER Word8 -- | No problems in checking the validity of a type equality. ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -3617,15 +3617,20 @@ instance Outputable SimpleUnifyResult where simpleUnifyCheck :: UnifyCheckCaller -> TcLevel -> TcTyVar -> TcType -> SimpleUnifyResult -- ^ A fast check for unification. May return "not sure", in which case -- unification might still be OK, but it'll take more work to do --- (use the full 'checkTypeEq'). +-- (use the full 'checkTyEqRhs'). -- --- * Rejects if lhs_tv occurs in rhs_ty (occurs check) --- * Rejects foralls unless --- lhs_tv is RuntimeUnk (used by GHCi debugger) --- or is a QL instantiation variable --- * Rejects a non-concrete type if lhs_tv is concrete --- * Rejects type families unless fam_ok=True --- * Does a level-check for type variables, to avoid skolem escape +-- It returns SUC_CannotUnify for +-- * Touchability failure +-- * Top level-shape failure +-- +-- It returns SUC_NotSure for +-- * Occurs check: lhs_tv occurs in rhs_ty +-- * Type families unless fam_ok=True +-- * Foralls unless +-- lhs_tv is RuntimeUnk (used by GHCi debugger) +-- or is a QL instantiation variable +-- * Concreteness: lhs_tv is concrete and rhs is a non-concrete type +-- * Skolem-escape: a level-check for type variables, to avoid skolem escape -- -- This function is pretty heavily used, so it's optimised not to allocate simpleUnifyCheck caller given_eq_lvl lhs_tv rhs @@ -4198,7 +4203,7 @@ famAppArgFlags flags = case flags of The key function `checkTyEqRhs ty_eq_flags rhs` is called on the RHS of a type equality lhs ~ rhs -and checks to see if `rhs` satisfies, or can be made to satisfy, +and checks to see if `rhs` satisfies, /or can be made to satisfy/, invariants described by `ty_eq_flags`. It can succeded or fail; in the latter case it returns a `CheckTyEqResult` that describes why it failed. @@ -4219,6 +4224,15 @@ Notably, it can check for things like: * Concreteness error e.g. alpha[conc] ~ r[sk] +Note "or can be made to satisfy the preconditions"! `checkTyEqRhs` may transform +the RHS by + + * Turning a type-family application into a type variable, perhaps to avoid + an occurs check. See Note Note [Family applications in canonical constraints] + + * Promoting any nested unification variables, in order to satisfy the + level invariant. See Note [Promotion and level-checking] + Its specific behaviour is governed by the `TyEqFlags` that are passed to it; see Note [TyEqFlags]. @@ -4275,7 +4289,7 @@ NB: We never see a TyVarLHS here, such as [G] a ~ F tys here because we'd have swapped it to [G] F tys ~ a -in canEqCanLHS2, before getting to checkTypeEq. +in canEqCanLHS2, before getting to checkTyEqRhs. -} check_ty_eq_rhs :: forall m a @@ -4799,7 +4813,6 @@ promote_meta_tyvar info dest_lvl occ_tv touchabilityTest :: TcLevel -> TcTyVar -> Bool -- ^ This is the key test for untouchability: -- See Note [Unification preconditions] in GHC.Tc.Utils.Unify --- and Note [Solve by unification] in GHC.Tc.Solver.Equality -- -- @True@ <=> the variable is touchable touchabilityTest given_eq_lvl tv ===================================== testsuite/tests/indexed-types/should_fail/T9662.stderr ===================================== @@ -1,12 +1,12 @@ T9662.hs:49:8: error: [GHC-25897] - • Couldn't match type ‘n’ with ‘Int’ + • Couldn't match type ‘m’ with ‘Int’ Expected: Exp (((sh :. k) :. m) :. n) -> Exp (((sh :. m) :. n) :. k) Actual: Exp (Tuple (((Atom a0 :. Atom Int) :. Atom Int) :. Atom Int)) -> Exp (Plain (((Unlifted (Atom a0) :. Exp Int) :. Exp Int) :. Exp Int)) - ‘n’ is a rigid type variable bound by + ‘m’ is a rigid type variable bound by the type signature for: test :: forall sh k m n. Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k) ===================================== testsuite/tests/simplCore/should_compile/T7803.hs ===================================== @@ -0,0 +1,23 @@ +{-# OPTIONS_GHC -ddump-simpl #-} + +-- #7803: foo1 should be fully specialised at Double. In the bug report +-- it ended up calling the overloaded exp5Tail (with a dictionary argument), +-- because the specialiser ran before the overloaded call was floated to +-- the top level. So the dumped Core for this module must mention no +-- exp5Tail at all. +module T7803 (foo1) where + +import T7803a + +bar :: Floating a => a -> a -> a +bar z = subtract (evaluate integ z) . evaluate integ + where + integ = indefinite (Piecewise [Poly4 1]) +{-# SPECIALIZE bar :: Double -> Double -> Double #-} + +foo :: Floating a => a -> a -> a +foo x = bar x +{-# SPECIALIZE foo :: Double -> Double -> Double #-} + +foo1 :: Double -> Double -> Double +foo1 x = foo x ===================================== testsuite/tests/simplCore/should_compile/T7803.stderr ===================================== @@ -0,0 +1 @@ +foo1 ===================================== testsuite/tests/simplCore/should_compile/T7803a.hs ===================================== @@ -0,0 +1,73 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE UndecidableSuperClasses #-} + +module T7803a + ( Evaluate (..) + , HasIntegral (..) + , Poly4 (..) + , Domain + , IntOfLogPoly4 (..) + , Piecewise (..) + ) where + +import Data.Kind (Constraint, Type) + +class Evaluate poly where + evaluate :: (Domain' poly a) => poly a -> a -> a + +class Evaluate (IntegralOf poly) => HasIntegral poly where + type IntegralOf poly :: Type -> Type + indefinite :: (Domain' poly a, Domain' (IntegralOf poly) a) + => poly a -> IntegralOf poly a + +type family Domain (f :: Type -> Type) a :: Constraint + +class Domain f a => Domain' f a +instance Domain f a => Domain' f a + +newtype Poly4 a = Poly4 { poly4_a :: a } + +type instance Domain Poly4 a = Fractional a + +data IntOfLogPoly4 a = IntOfLogPoly4 { ilp4_k :: !a, ilp4_u :: !a } + +type instance Domain IntOfLogPoly4 a = Floating a + +instance Evaluate IntOfLogPoly4 where + evaluate (IntOfLogPoly4 k _) x = k + x * exp5Tail (- log x) + {-# INLINE evaluate #-} + +{-# RULES "exp5Tail/Double" exp5Tail = exp5TailDouble #-} +{-# NOINLINE exp5Tail #-} + +exp5Tail :: (Floating a) => a -> a +exp5Tail x = x / 120 + +exp5TailDouble :: Double -> Double +exp5TailDouble x = x / 120 + +instance HasIntegral Poly4 where + type IntegralOf Poly4 = IntOfLogPoly4 + indefinite = \ (Poly4 a) -> IntOfLogPoly4 0 a + {-# INLINE indefinite #-} + +newtype Piecewise poly a = Piecewise { unPiecewise :: [poly a] } + +type instance Domain (Piecewise poly) a = (Domain poly a, Num a) + +instance (Evaluate poly) => Evaluate (Piecewise poly) where + evaluate = \ (Piecewise pp) x -> + case pp of + p : _ -> evaluate p x + [] -> error "evaluate: empty Piecewise" + {-# INLINE evaluate #-} + +instance (HasIntegral poly) => HasIntegral (Piecewise poly) where + type IntegralOf (Piecewise poly) = Piecewise (IntegralOf poly) + indefinite (Piecewise m) = Piecewise $ map indefinite m + {-# INLINE indefinite #-} ===================================== testsuite/tests/simplCore/should_compile/all.T ===================================== @@ -148,6 +148,13 @@ test('T7785', [ only_ways(['optasm']), grep_errmsg(r'SPEC') ], compile, ['-ddump-cse']) +# T7803: we expect NO calls to the overloaded 'exp5Tail' in T7803.hs +# In the bug report #7803, the unspecialised call was signalled by 'exp5Tail' +# in foo1's Core, so we grep for that; also for 'foo1', lest we dump nothing +# One module, T7803.hs, has OPTIONS_GHC -ddump-simpl +test('T7803', [ grep_errmsg(r'exp5Tail|foo1') ], + multimod_compile, ['T7803', '-O2 -v0 -dsuppress-all -dsuppress-uniques -dno-typeable-binds']) + test('T7702', [extra_files(['T7702plugin']), pre_cmd('$MAKE -s --no-print-directory -C T7702plugin package.T7702 TOP={top}'), ===================================== testsuite/tests/typecheck/should_fail/T27844.hs ===================================== @@ -0,0 +1,14 @@ +-- Repro.hs +-- The call to f forces c ~ (b, F c) inside the scope of the skolem b. +-- Correct behaviour: a type error at the first argument of const +-- (as GHC 9.12.4 reports). + +{-# LANGUAGE RankNTypes, TypeFamilies #-} +module T27844 where + +type family F a + +f :: (forall b. b -> (b, F c)) -> c -> () +f _ _ = () + +g x = f (\_ -> const x (show x)) x ===================================== testsuite/tests/typecheck/should_fail/T27844.stderr ===================================== @@ -0,0 +1,11 @@ +T27844.hs:13:22: error: [GHC-25897] + • Couldn't match expected type ‘(b, F c)’ with actual type ‘c’ + ‘c’ is a rigid type variable bound by + the inferred type of g :: Show c => c -> () + at T27844.hs:143:1-34 + • In the first argument of ‘const’, namely ‘x’ + In the expression: const x (show x) + In the first argument of ‘f’, namely ‘(\ _ -> const x (show x))’ + • Relevant bindings include + x :: c (bound at T27844.hs:14:3) + g :: c -> () (bound at T27844.hs:14:1) ===================================== testsuite/tests/typecheck/should_fail/all.T ===================================== @@ -763,3 +763,4 @@ test('T26861', normal, compile_fail, ['']) test('T26862', normal, compile_fail, ['']) test('T27210', normal, compile_fail, ['']) test('T26532', normal, compile_fail, ['']) +test('T27844', normal, compile_fail, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/0437d21cf0698b5b325be793df6d26f... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/0437d21cf0698b5b325be793df6d26f... You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help