September 2026 - ghc-commits

[Git][ghc/ghc] Pushed new branch wip/27845
by Zubin (＠wz1000) 30 Sep '26

30 Sep '26

Zubin pushed new branch wip/27845 at Glasgow Haskell Compiler / GHC -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/tree/wip/27845 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

1 0

[Git][ghc/ghc] Pushed new branch wip/sjakobi/T27838-t13820-window
by Simon Jakobi (＠sjakobi) 30 Sep '26

30 Sep '26

Simon Jakobi pushed new branch wip/sjakobi/T27838-t13820-window at Glasgow Haskell Compiler / GHC -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/tree/wip/sjakobi/T27838-t13820-window 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

1 0

[Git][ghc/ghc][wip/marge_bot_batch_merge_job] 4 commits: RTS: Update flag parsing/handling:
by Marge Bot (＠marge-bot) 30 Sep '26

30 Sep '26

Marge Bot pushed to branch wip/marge_bot_batch_merge_job at Glasgow Haskell Compiler / GHC Commits: 5f1a9d3b by Andreas Klebinger at 2026-09-30T07:03:47-04:00 RTS: Update flag parsing/handling: Using 0 as argument to any of these flags now resets the flags setting to default: - ``-n0`` disables nursery chunking. - ``-K0`` (or a bare ``-K``) removes the stack size limit. - ``-M0`` removes the heap size limit. - ``-H0`` resets the suggested heap size, including the nursery scaling set by ``-H``. - ``-AL0`` makes the large object allocation limit follow ``-A`` again. GC Generations are now limited to 64. -n larger than -A now emits a warning and disables chunking. Fixes #27830 #27829 - - - - - d52cd364 by Andreas Klebinger at 2026-09-30T07:03:47-04:00 Fix MultiLayerModules timeout multiplier. We accidentally used the compile multiplier for ghci commands which use the run timeout setting to set the timeout. Fixes #26263 and #27796. - - - - - f47949c4 by Andreas Klebinger at 2026-09-30T07:03:47-04:00 testsuite: Include runtime in JUnit report. - - - - - bbe2fea0 by Alan Zimmerman at 2026-09-30T07:03:48-04:00 EPA: Use EpaLocation in EpVirtualBraces Haddock processing uses EpLayout.EpVirtualBraces to record the current layout column, for allocating haddock comments correctly. For exact printing, we need the line as well as the col, so we know how many lines to skip when the indented code block starts. This commit updates EpLayout.EpVirtualBraces so that it carries an EpaLocation instead of just the Int column, to allow it to be used for both purposes. It is a simple mechanical change, with no other impact, but it allows us to use EpLayout instead of AnnListLayout in AnnList, in the next commit in this series. - - - - - 38 changed files: - + changelog.d/T27830-rts-flag-bounds - compiler/GHC/Parser.y - compiler/GHC/Parser/Annotation.hs - compiler/GHC/Parser/PostProcess/Haddock.hs - docs/users_guide/runtime_control.rst - rts/RtsFlags.c - rts/include/rts/Flags.h - rts/include/rts/storage/GC.h - rts/sm/GC.c - rts/sm/Storage.c - testsuite/driver/junit.py - testsuite/driver/testglobals.py - testsuite/driver/testlib.py - testsuite/tests/ghc-api/exactprint/T22919.stderr - testsuite/tests/ghc-api/exactprint/Test20239.stderr - testsuite/tests/ghc-api/exactprint/ZeroWidthSemi.stderr - testsuite/tests/haddock/should_compile_flag_haddock/T17544.stderr - testsuite/tests/haddock/should_compile_flag_haddock/T17544_kw.stderr - testsuite/tests/haddock/should_compile_flag_haddock/T24221.stderr - testsuite/tests/module/mod185.stderr - testsuite/tests/parser/should_compile/DumpParsedAst.stderr - testsuite/tests/parser/should_compile/DumpParsedAstComments.stderr - testsuite/tests/parser/should_compile/DumpSemis.stderr - testsuite/tests/parser/should_compile/KindSigs.stderr - testsuite/tests/parser/should_compile/T15323.stderr - testsuite/tests/parser/should_compile/T20452.stderr - testsuite/tests/parser/should_compile/T20718.stderr - testsuite/tests/parser/should_compile/T20718b.stderr - testsuite/tests/parser/should_compile/T20846.stderr - testsuite/tests/parser/should_compile/T23315/T23315.stderr - testsuite/tests/perf/compiler/all.T - testsuite/tests/printer/AnnotationNoListTuplePuns.stdout - testsuite/tests/printer/T18791.stderr - testsuite/tests/printer/Test20297.stdout - testsuite/tests/printer/Test24533.stdout - testsuite/tests/rts/all.T - testsuite/tests/rts/rtsflags001.stderr-ws-32 - testsuite/tests/rts/rtsflags001.stderr-ws-64 The diff was not included because it is too large. View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/77dc8c705444377422d3c2926d8cc1… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/77dc8c705444377422d3c2926d8cc1… 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

1 0

[Git][ghc/ghc][wip/T27844] Refactor and simplify solver's unification code
by Simon Peyton Jones (＠simonpj) 30 Sep '26

30 Sep '26

Simon Peyton Jones pushed to branch wip/T27844 at Glasgow Haskell Compiler / GHC Commits: 19aa83cb by Simon Peyton Jones at 2026-09-30T11:32:38+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. * `kickOutAfterFillingCoercionHole` should account for equalities with a TyFamLHS. See (KOC5) in Note [Kick out after filling a coercion hole] * No need to gather coercion holes in the `PuOK` case of `canEqCanLHSFinish_no_unification`. See documentation with that code. - - - - - 12 changed files: - + changelog.d/T27844 - compiler/GHC/Runtime/Heap/Inspect.hs - compiler/GHC/Tc/Errors.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/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/Errors.hs ===================================== @@ -478,6 +478,7 @@ mkErrorItem ct -- For this `suppress` stuff see -- Note [Wanteds rewrite Wanteds: rewriter-sets] in GHC.Tc.Types.Constraint + -- especiallly (WRW8) (suppress, m_evdest) = case ctEvidence ct of CtGiven {} -> (False, Nothing) CtWanted (WantedCt { ctev_rewriters = rws, ctev_dest = dest }) ===================================== 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 @@ -3073,11 +3125,10 @@ inertsEqsCanDischarge inerts (EqCt { eq_lhs = lhs_w, eq_rhs = rhs_w || (empty_rw_w && not (isEmptyCoHoleSet (ctEvRewriters ev_i))) -- Prefer the one that has no rewriters -- See (CE4) in Note [Combining equalities] + -- and (WRW10) in Note Note [Wanteds rewrite Wanteds: rewriter-sets] inertsEqsCanDischarge _ _ = Nothing - - {- Note [Do not unify Givens] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider this GADT match @@ -3143,34 +3194,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 ===================================== @@ -22,7 +22,7 @@ module GHC.Tc.Solver.InertSet ( InertEqs, foldTyEqs, delEq, findEq, partitionInertEqs, partitionFunEqs, transformAndPartitionTyVarEqs, - filterInertEqs, filterFunEqs, + filterInertEqs, filterFunEqs, transformAndPartitionFunEqs, foldFunEqs, addEqToCans, -- * Inert Dicts @@ -128,7 +128,7 @@ Further refinements: * Among the equalities we prioritise ones with an empty rewriter set; see Note [Wanteds rewrite Wanteds: rewriter-sets] in GHC.Tc.Types.Constraint, - wrinkle (WRW8). + wrinkle (WRW7). * Among equalities with an empty rewriter set, we prioritise nominal equalities. * They have more rewriting power, so doing them first is better. @@ -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 @@ -1422,6 +1422,19 @@ addCanFunEq old_eqs fun_tc fun_args ct foldFunEqs :: (EqCt -> b -> b) -> FunEqMap EqualCtList -> b -> b foldFunEqs k fun_eqs z = foldTcAppMap (\eqs z -> foldr k z eqs) fun_eqs z +transformAndPartitionFunEqs + :: (EqCt -> Either EqCt EqCt) -- Left => chuck out, Right => keep + -> InertFunEqs + -> ([EqCt], InertFunEqs) -- (chuck-out, keep) +transformAndPartitionFunEqs pred orig_inerts + = foldFunEqs folder orig_inerts ([], emptyFunEqs) + where + folder :: EqCt -> ([EqCt], InertFunEqs) -> ([EqCt], InertFunEqs) + folder eq_ct (acc_true, acc_false) + = case pred eq_ct of + Left eq_ct' -> (eq_ct' : acc_true, acc_false) + Right eq_ct' -> (acc_true, addFunEqs eq_ct' acc_false) + partitionFunEqs :: (EqCt -> Bool) -- EqCt will have a TyFamLHS -> InertFunEqs -> ([EqCt], InertFunEqs) ===================================== 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 @@ -438,10 +435,12 @@ why solving `kco` might unlock `co`, especially (URW2). Hence `kickOutAfterFillingCoercionHole`. It looks at inert constraints that are * Wanted - * Of the form alpha ~ rhs, where alpha is a unification variable -and kicks out any that will have an empty rewriter set after filling the hole. + * Of the form (alpha ~ rhs), or (F tys ~ alpha) + where alpha is a unification variable +and kicks out any that have an empty rewriter set after filling the hole. Wrinkles: + (KOC1) If co's rewriter-set is {kco, xco}, there is no point in kicking it out, because it still can't be unified. So we only kick out if the co's rewriter-set becomes empty. @@ -455,13 +454,17 @@ Wrinkles: on `kco2` instead of `kco`. Hence the `new_holes` passed to `kickOutAfterFillingCoercionHole` -(KOC3) It's possible that this could just go ahead and unify, but could there - be occurs-check problems? Seems simpler just to kick out. +(KOC3) It's possible that this could just go ahead and unify on the spot, but could + there be occurs-check problems? Seems simpler just to kick out. (KOC4) Kick-out is undesirable, so it'd be better to solve `kco` before `co`. So the solver prioritises equalities with an empty rewriter set, to try to avoid unnecessary kick-out. See GHC.Tc.Types.Constraint Note [Prioritise Wanteds with empty CoHoleSet] esp (PER1) + +(KOC5) We kick out from both `inert_eqs` and `inert_funeqs`. The latter is needed + in case we have (F tys ~ alpha), which might (if it now has an empty rewriter + set) allou unifying alpha. -} kickOutRewritable :: KickOutSpec -> CtFlavourRole -> TcS () @@ -526,23 +529,32 @@ kickOutAfterFillingCoercionHole hole (CPH { cph_holes = new_holes }) ; setInertCans ics' } where kick_out :: InertCans -> ([EqCt], InertCans) - kick_out ics@(IC { inert_eqs = eqs }) - = (eqs_to_kick, ics { inert_eqs = eqs_to_keep }) + kick_out ics@(IC { inert_eqs = eqs, inert_funeqs = funeqs }) + = ( kick_funeqs ++ kick_eqs + , ics { inert_eqs = keep_eqs, inert_funeqs = keep_funeqs }) where - (eqs_to_kick, eqs_to_keep) = transformAndPartitionTyVarEqs kick_out_eq eqs + (kick_eqs, keep_eqs) = transformAndPartitionTyVarEqs kick_out_eq eqs + (kick_funeqs, keep_funeqs) = transformAndPartitionFunEqs kick_out_eq funeqs + -- Kick out from funeqs as well as eqs. + -- See (KOC5) in Note [Kick out after filling a coercion hole] + + is_meta_tv_equality (EqCt { eq_lhs = lhs, eq_rhs = rhs }) + | TyVarLHS tv <- lhs = isMetaTyVar tv + | Just tv <- getTyVar_maybe rhs = isMetaTyVar tv + | otherwise = False kick_out_eq :: EqCt -> Either EqCt EqCt - kick_out_eq eq_ct@(EqCt { eq_ev = ev, eq_lhs = lhs }) + kick_out_eq eq_ct@(EqCt { eq_ev = ev }) | CtWanted (wev@(WantedCt { ctev_rewriters = rewriters })) <- ev - , TyVarLHS tv <- lhs - , isMetaTyVar tv , hole `elemCoHoleSet` rewriters - , let holes' = (rewriters `delCoHoleSet` hole) `mappend` new_holes - -- Adding new_holes and deleting hole: see (KOC2) - eq_ct' = eq_ct { eq_ev = CtWanted (wev { ctev_rewriters = holes' }) } - = if isEmptyCoHoleSet holes' + , is_meta_tv_equality eq_ct + , let rewriters' = (rewriters `delCoHoleSet` hole) `mappend` new_holes + -- Adding new_holes and deleting hole: see (KOC2) + eq_ct' = eq_ct { eq_ev = CtWanted (wev { ctev_rewriters = rewriters' }) } + = if isEmptyCoHoleSet rewriters' then Left eq_ct' -- Kick out, if new rewriter set is empty (KOC1) else Right eq_ct' -- Keep, but with trimmed holes see (KOC2) + | otherwise = Right eq_ct @@ -2302,52 +2314,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 +2329,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. @@ -2623,19 +2623,24 @@ The rewriter-set plan thereby dropping the reference to `co`. I'm not certain whether this actually happens or not. -(WRW7) In error reporting, we simply suppress any errors that have been rewritten - by /unsolved/ wanteds. This suppression happens in GHC.Tc.Errors.mkErrorItem, +(WRW7) When we fill a coercion hole `h` we kick out any inert Wanted that has `h` + in its rewriter set. See `kickOutAfterFilling CoercionHole`. + See Note [Kick out after filling a coercion hole] in GHC.Tc.Solver.Monad. + + Furthermore, when we select a work item, in `selectNextWorkItem` we zonk the + rewriter set so that it accurately reflects the unsolved coercion holes. That + sets it up ready for the no-rewriter check in (WR5), when we process the equality. + + In `selectNextWorkItem`, we also prioritise equalities with no rewiters. + See Note [Prioritise Wanteds with empty CoHoleSet] in GHC.Tc.Types.Constraint + wrinkle (PER1). + +(WRW8) In error reporting, we suppress any errors that have been rewritten + by /unsolved/ wanteds. This suppression happens in `GHC.Tc.Errors.mkErrorItem`, which uses `GHC.Tc.Zonk.Type.zonkCoHoleSet` 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. -(WRW8) In `selectNextWorkItem`, priorities equalities with no rewiters. See - Note [Prioritise Wanteds with empty CoHoleSet] in GHC.Tc.Types.Constraint - wrinkle (PER1). - -(WRW9) In error reporting, we prioritise Wanteds that have an empty CoHoleSet: - see Note [Prioritise Wanteds with empty CoHoleSet]. - Let's continue our first example above: inert: [W] w1 :: a ~ Char @@ -2661,8 +2666,10 @@ Wrinkles: (WRW11) When zonking a constraint (with `zonkCt` and `zonkCtEvidence`) we take the opportunity to zonk its `CoHoleSet`, which eliminates solved ones. - This doesn't guarantee that rewriter sets are always up to date -- c.f. - (WRW10) -- but it helps, and it de-clutters debug output. + This doesn't guarantee that rewriter sets are always up to date (c.f. (WRW10)) + but it helps, and it de-clutters debug output. + + See also (WRW7) which does the crucial just-in-time zonking of the rewriters. Note [Prioritise Wanteds with empty CoHoleSet] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2705,9 +2712,8 @@ in our simplify_loop iteration, we happened to start with co_aym. All would have been well if we'd started with the (not-rewritten) co_ayb and gotten it into the inert set. -With that in mind, we /prioritise/ the work-list to put -constraints with no rewriters first. This prioritisation -is done in `GHC.Tc.Solver.Monad.selectNextWorkItem`. +With that in mind, we /prioritise/ the work-list to put constraints with no rewriters +first. This prioritisation is done in `GHC.Tc.Solver.Monad.selectNextWorkItem`. Wrinkles @@ -2720,8 +2726,8 @@ Wrinkles 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 written a confusing program! (T22707 and T22793 were close, but they do - not exhibit this behaviour.) So belt and braces: see the `suppress` - stuff in GHC.Tc.Errors.mkErrorItem. + not exhibit this behaviour.) So belt and braces: + see `GHC.Tc.Errors.reportWanteds`. Note [Avoiding rewriting cycles] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ===================================== 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/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:14: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/-/commit/19aa83cbbe2af18310c48dfe7667509… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/19aa83cbbe2af18310c48dfe7667509… 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

1 0

[Git][ghc/ghc][wip/fendor/27834] Extend the `TrustOverlay` for wired-in units
by Hannes Siebenhandl (＠fendor) 30 Sep '26

30 Sep '26

Hannes Siebenhandl pushed to branch wip/fendor/27834 at Glasgow Haskell Compiler / GHC Commits: 665b4608 by Hannes Siebenhandl at 2026-09-30T11:10:44+02:00 Extend the `TrustOverlay` for wired-in units The TrustOverlay only contained the `UnitId` of all on-disk units. However, wired-in units are referred to by their wired-in unit id, which is not the same as the on-disk unit id. Thus, trust checks for wired-in units failed because the lookup was using the wired-in unit, which wasn't present in the `TrustOverlay`. We fix #27834, by copying the trust info for wired-in unit ids. - - - - - 6 changed files: - changelog.d/unit-index - compiler/GHC/Unit/State.hs - + testsuite/tests/ghci/scripts/T27834.hs - + testsuite/tests/ghci/scripts/T27834.script - + testsuite/tests/ghci/scripts/T27834.stdout - testsuite/tests/ghci/scripts/all.T Changes: ===================================== changelog.d/unit-index ===================================== @@ -1,7 +1,7 @@ section: compiler synopsis: Use global ``UnitIndex`` to deduplicate ``UnitInfo``s over multiple home units -issues: #27500 #26423 #27748 -mrs: !16115 !16598 +issues: #27500 #26423 #27748 #27834 +mrs: !16115 !16598 !16743 description: { The ``UnitState`` used to be duplicated for all ``HomeUnitEnv``, not sharing any of the ``UnitInfo``s. ===================================== compiler/GHC/Unit/State.hs ===================================== @@ -286,6 +286,21 @@ trustUnits elements (TrustOverlay to) = TrustOverlay $ foldl' (\ acc uid -> addT emptyTrustOverlay :: TrustOverlay emptyTrustOverlay = TrustOverlay emptyUniqMap +-- | For all values in the 'WireMap', copy the recorded trust/distrust +-- for the wired-in unit id. +-- +extendForWireMap :: TrustOverlay -> WireMap -> TrustOverlay +extendForWireMap to wmap = + foldl' go to (listWireMap wmap) + where + go overlay (onDiskUid, wiredInUid) = + case lookupTrustOverlay overlay onDiskUid of + Nothing -> overlay + Just Trusted -> + trustUnits [wiredInUid] overlay + Just Distrusted -> + distrustUnits [wiredInUid] overlay + {- Note [Sharing 'UnitInfo's across the 'UnitEnv'] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -957,7 +972,7 @@ mkUnitState logger unit_index cfg = do , explicitUnits = explicit_pkgs , homeUnitDepends = home_unit_deps , unitInfoMap = pkg_db - , trustedUnits = trustUnitsOverlay + , trustedUnits = trustUnitsOverlay `extendForWireMap` wired_map , moduleNameProvidersMap = mod_map , pluginModuleNameProvidersMap = mkModuleNameProvidersMap logger (unitConfigAllowVirtual cfg) pkg_db plugin_vis_map , packageNameMap = pkgname_map ===================================== testsuite/tests/ghci/scripts/T27834.hs ===================================== @@ -0,0 +1,9 @@ +{-# LANGUAGE Haskell2010 #-} +{-# LANGUAGE Safe #-} +module Main where + +-- Importing a wired-in in module should honour trustworthiness +import GHC.Internal.Char (chr) + +main :: IO () +main = print (chr 120) ===================================== testsuite/tests/ghci/scripts/T27834.script ===================================== @@ -0,0 +1,2 @@ +:load T27834 +putStrLn "Can import trusted module from ghc-internal" ===================================== testsuite/tests/ghci/scripts/T27834.stdout ===================================== @@ -0,0 +1 @@ +Can import trusted module from ghc-internal ===================================== testsuite/tests/ghci/scripts/all.T ===================================== @@ -402,3 +402,4 @@ test('GhciPackageRename', ghci_script, ['GhciPackageRename.script']) test('T26233', normal, ghci_script, ['T26233.script']) +test('T27834', [extra_hc_opts("-fpackage-trust -trust base -trust ghc-internal -package ghc-internal")], ghci_script, ['T27834.script']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/665b4608905b11dbdf1a87915a521da… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/665b4608905b11dbdf1a87915a521da… 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

1 0

[Git][ghc/ghc] Pushed new branch wip/fendor/27834
by Hannes Siebenhandl (＠fendor) 30 Sep '26

30 Sep '26

Hannes Siebenhandl pushed new branch wip/fendor/27834 at Glasgow Haskell Compiler / GHC -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/tree/wip/fendor/27834 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

1 0

[Git][ghc/ghc][wip/marge_bot_batch_merge_job] 5 commits: Enable -fexpose-overloaded-unfoldings by default when optimizations are on.
by Marge Bot (＠marge-bot) 29 Sep '26

29 Sep '26

Marge Bot pushed to branch wip/marge_bot_batch_merge_job at Glasgow Haskell Compiler / GHC Commits: ac08fb6f by Andreas Klebinger at 2026-09-30T02:52:29-04:00 Enable -fexpose-overloaded-unfoldings by default when optimizations are on. I also made the -fexpose-*-unfoldings flags optimization flags rather than codeGen flags. This was needed to fix a test and is the correct place for them. Performance numbers: In general this averages out to ~1% more file size across the GHC build. Compiler allocations grow by 0.14% on nofib as the compiler needs to deal with more available unfoldings. On the cabal test it's awash. With some configurations getting slightly faster, some slightly slower. It's all in the +/- 0.2% range. On nofib itself we produce exactly the same code. Which is expected, as it doesn't use -fspecialize-aggresively anywhere afaik which is needed to take advantage of cross module specialization. Fixes #13090 ------------------------- Metric Increase: LinkableUsage01 LinkableUsage02 hard_hole_fits ------------------------- - - - - - 316488bd by Andreas Klebinger at 2026-09-30T02:52:30-04:00 RTS: Update flag parsing/handling: Using 0 as argument to any of these flags now resets the flags setting to default: - ``-n0`` disables nursery chunking. - ``-K0`` (or a bare ``-K``) removes the stack size limit. - ``-M0`` removes the heap size limit. - ``-H0`` resets the suggested heap size, including the nursery scaling set by ``-H``. - ``-AL0`` makes the large object allocation limit follow ``-A`` again. GC Generations are now limited to 64. -n larger than -A now emits a warning and disables chunking. Fixes #27830 #27829 - - - - - cd6191f7 by Andreas Klebinger at 2026-09-30T02:52:31-04:00 Fix MultiLayerModules timeout multiplier. We accidentally used the compile multiplier for ghci commands which use the run timeout setting to set the timeout. Fixes #26263 and #27796. - - - - - 55b36507 by Andreas Klebinger at 2026-09-30T02:52:31-04:00 testsuite: Include runtime in JUnit report. - - - - - 77dc8c70 by Alan Zimmerman at 2026-09-30T02:52:32-04:00 EPA: Use EpaLocation in EpVirtualBraces Haddock processing uses EpLayout.EpVirtualBraces to record the current layout column, for allocating haddock comments correctly. For exact printing, we need the line as well as the col, so we know how many lines to skip when the indented code block starts. This commit updates EpLayout.EpVirtualBraces so that it carries an EpaLocation instead of just the Int column, to allow it to be used for both purposes. It is a simple mechanical change, with no other impact, but it allows us to use EpLayout instead of AnnListLayout in AnnList, in the next commit in this series. - - - - - 44 changed files: - + changelog.d/T13090-expose-overloaded-unfoldings - + changelog.d/T27830-rts-flag-bounds - compiler/GHC/Driver/DynFlags.hs - compiler/GHC/Driver/Flags.hs - compiler/GHC/Iface/Tidy.hs - compiler/GHC/Parser.y - compiler/GHC/Parser/Annotation.hs - compiler/GHC/Parser/PostProcess/Haddock.hs - docs/users_guide/runtime_control.rst - docs/users_guide/using-optimisation.rst - rts/RtsFlags.c - rts/include/rts/Flags.h - rts/include/rts/storage/GC.h - rts/sm/GC.c - rts/sm/Storage.c - testsuite/driver/junit.py - testsuite/driver/testglobals.py - testsuite/driver/testlib.py - testsuite/tests/dmdanal/should_compile/T23398.stderr - testsuite/tests/ghc-api/exactprint/T22919.stderr - testsuite/tests/ghc-api/exactprint/Test20239.stderr - testsuite/tests/ghc-api/exactprint/ZeroWidthSemi.stderr - testsuite/tests/haddock/should_compile_flag_haddock/T17544.stderr - testsuite/tests/haddock/should_compile_flag_haddock/T17544_kw.stderr - testsuite/tests/haddock/should_compile_flag_haddock/T24221.stderr - testsuite/tests/module/mod185.stderr - testsuite/tests/parser/should_compile/DumpParsedAst.stderr - testsuite/tests/parser/should_compile/DumpParsedAstComments.stderr - testsuite/tests/parser/should_compile/DumpSemis.stderr - testsuite/tests/parser/should_compile/KindSigs.stderr - testsuite/tests/parser/should_compile/T15323.stderr - testsuite/tests/parser/should_compile/T20452.stderr - testsuite/tests/parser/should_compile/T20718.stderr - testsuite/tests/parser/should_compile/T20718b.stderr - testsuite/tests/parser/should_compile/T20846.stderr - testsuite/tests/parser/should_compile/T23315/T23315.stderr - testsuite/tests/perf/compiler/all.T - testsuite/tests/printer/AnnotationNoListTuplePuns.stdout - testsuite/tests/printer/T18791.stderr - testsuite/tests/printer/Test20297.stdout - testsuite/tests/printer/Test24533.stdout - testsuite/tests/rts/all.T - testsuite/tests/rts/rtsflags001.stderr-ws-32 - testsuite/tests/rts/rtsflags001.stderr-ws-64 The diff was not included because it is too large. View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/0fbfb27f6425e3d1ddf5ec65f27f11… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/0fbfb27f6425e3d1ddf5ec65f27f11… 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

1 0

[Git][ghc/ghc][wip/marge_bot_batch_merge_job] 5 commits: Enable -fexpose-overloaded-unfoldings by default when optimizations are on.
by Marge Bot (＠marge-bot) 29 Sep '26

29 Sep '26

Marge Bot pushed to branch wip/marge_bot_batch_merge_job at Glasgow Haskell Compiler / GHC Commits: 79c6b7ad by Andreas Klebinger at 2026-09-29T23:43:21-04:00 Enable -fexpose-overloaded-unfoldings by default when optimizations are on. I also made the -fexpose-*-unfoldings flags optimization flags rather than codeGen flags. This was needed to fix a test and is the correct place for them. Performance numbers: In general this averages out to ~1% more file size across the GHC build. Compiler allocations grow by 0.14% on nofib as the compiler needs to deal with more available unfoldings. On the cabal test it's awash. With some configurations getting slightly faster, some slightly slower. It's all in the +/- 0.2% range. On nofib itself we produce exactly the same code. Which is expected, as it doesn't use -fspecialize-aggresively anywhere afaik which is needed to take advantage of cross module specialization. Fixes #13090 ------------------------- Metric Increase: LinkableUsage01 LinkableUsage02 hard_hole_fits ------------------------- - - - - - a37fd9e5 by Andreas Klebinger at 2026-09-29T23:43:22-04:00 RTS: Update flag parsing/handling: Using 0 as argument to any of these flags now resets the flags setting to default: - ``-n0`` disables nursery chunking. - ``-K0`` (or a bare ``-K``) removes the stack size limit. - ``-M0`` removes the heap size limit. - ``-H0`` resets the suggested heap size, including the nursery scaling set by ``-H``. - ``-AL0`` makes the large object allocation limit follow ``-A`` again. GC Generations are now limited to 64. -n larger than -A now emits a warning and disables chunking. Fixes #27830 #27829 - - - - - 26103499 by Andreas Klebinger at 2026-09-29T23:43:23-04:00 Fix MultiLayerModules timeout multiplier. We accidentally used the compile multiplier for ghci commands which use the run timeout setting to set the timeout. Fixes #26263 and #27796. - - - - - a661eb86 by Andreas Klebinger at 2026-09-29T23:43:23-04:00 testsuite: Include runtime in JUnit report. - - - - - 0fbfb27f by Alan Zimmerman at 2026-09-29T23:43:23-04:00 EPA: Use EpaLocation in EpVirtualBraces Haddock processing uses EpLayout.EpVirtualBraces to record the current layout column, for allocating haddock comments correctly. For exact printing, we need the line as well as the col, so we know how many lines to skip when the indented code block starts. This commit updates EpLayout.EpVirtualBraces so that it carries an EpaLocation instead of just the Int column, to allow it to be used for both purposes. It is a simple mechanical change, with no other impact, but it allows us to use EpLayout instead of AnnListLayout in AnnList, in the next commit in this series. - - - - - 44 changed files: - + changelog.d/T13090-expose-overloaded-unfoldings - + changelog.d/T27830-rts-flag-bounds - compiler/GHC/Driver/DynFlags.hs - compiler/GHC/Driver/Flags.hs - compiler/GHC/Iface/Tidy.hs - compiler/GHC/Parser.y - compiler/GHC/Parser/Annotation.hs - compiler/GHC/Parser/PostProcess/Haddock.hs - docs/users_guide/runtime_control.rst - docs/users_guide/using-optimisation.rst - rts/RtsFlags.c - rts/include/rts/Flags.h - rts/include/rts/storage/GC.h - rts/sm/GC.c - rts/sm/Storage.c - testsuite/driver/junit.py - testsuite/driver/testglobals.py - testsuite/driver/testlib.py - testsuite/tests/dmdanal/should_compile/T23398.stderr - testsuite/tests/ghc-api/exactprint/T22919.stderr - testsuite/tests/ghc-api/exactprint/Test20239.stderr - testsuite/tests/ghc-api/exactprint/ZeroWidthSemi.stderr - testsuite/tests/haddock/should_compile_flag_haddock/T17544.stderr - testsuite/tests/haddock/should_compile_flag_haddock/T17544_kw.stderr - testsuite/tests/haddock/should_compile_flag_haddock/T24221.stderr - testsuite/tests/module/mod185.stderr - testsuite/tests/parser/should_compile/DumpParsedAst.stderr - testsuite/tests/parser/should_compile/DumpParsedAstComments.stderr - testsuite/tests/parser/should_compile/DumpSemis.stderr - testsuite/tests/parser/should_compile/KindSigs.stderr - testsuite/tests/parser/should_compile/T15323.stderr - testsuite/tests/parser/should_compile/T20452.stderr - testsuite/tests/parser/should_compile/T20718.stderr - testsuite/tests/parser/should_compile/T20718b.stderr - testsuite/tests/parser/should_compile/T20846.stderr - testsuite/tests/parser/should_compile/T23315/T23315.stderr - testsuite/tests/perf/compiler/all.T - testsuite/tests/printer/AnnotationNoListTuplePuns.stdout - testsuite/tests/printer/T18791.stderr - testsuite/tests/printer/Test20297.stdout - testsuite/tests/printer/Test24533.stdout - testsuite/tests/rts/all.T - testsuite/tests/rts/rtsflags001.stderr-ws-32 - testsuite/tests/rts/rtsflags001.stderr-ws-64 The diff was not included because it is too large. View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/aa3c0f1fa6cb59f3ffaab4721eebbe… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/aa3c0f1fa6cb59f3ffaab4721eebbe… 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

1 0

[Git][ghc/ghc][wip/marge_bot_batch_merge_job] 5 commits: Enable -fexpose-overloaded-unfoldings by default when optimizations are on.
by Marge Bot (＠marge-bot) 29 Sep '26

29 Sep '26

Marge Bot pushed to branch wip/marge_bot_batch_merge_job at Glasgow Haskell Compiler / GHC Commits: 9e2756ed by Andreas Klebinger at 2026-09-29T20:05:12-04:00 Enable -fexpose-overloaded-unfoldings by default when optimizations are on. I also made the -fexpose-*-unfoldings flags optimization flags rather than codeGen flags. This was needed to fix a test and is the correct place for them. Performance numbers: In general this averages out to ~1% more file size across the GHC build. Compiler allocations grow by 0.14% on nofib as the compiler needs to deal with more available unfoldings. On the cabal test it's awash. With some configurations getting slightly faster, some slightly slower. It's all in the +/- 0.2% range. On nofib itself we produce exactly the same code. Which is expected, as it doesn't use -fspecialize-aggresively anywhere afaik which is needed to take advantage of cross module specialization. Fixes #13090 ------------------------- Metric Increase: LinkableUsage01 LinkableUsage02 hard_hole_fits ------------------------- - - - - - 926c00d1 by Andreas Klebinger at 2026-09-29T20:05:13-04:00 RTS: Update flag parsing/handling: Using 0 as argument to any of these flags now resets the flags setting to default: - ``-n0`` disables nursery chunking. - ``-K0`` (or a bare ``-K``) removes the stack size limit. - ``-M0`` removes the heap size limit. - ``-H0`` resets the suggested heap size, including the nursery scaling set by ``-H``. - ``-AL0`` makes the large object allocation limit follow ``-A`` again. GC Generations are now limited to 64. -n larger than -A now emits a warning and disables chunking. Fixes #27830 #27829 - - - - - 8dca2645 by Andreas Klebinger at 2026-09-29T20:05:14-04:00 Fix MultiLayerModules timeout multiplier. We accidentally used the compile multiplier for ghci commands which use the run timeout setting to set the timeout. Fixes #26263 and #27796. - - - - - d0e3ad8c by Andreas Klebinger at 2026-09-29T20:05:14-04:00 testsuite: Include runtime in JUnit report. - - - - - aa3c0f1f by Alan Zimmerman at 2026-09-29T20:05:15-04:00 EPA: Use EpaLocation in EpVirtualBraces Haddock processing uses EpLayout.EpVirtualBraces to record the current layout column, for allocating haddock comments correctly. For exact printing, we need the line as well as the col, so we know how many lines to skip when the indented code block starts. This commit updates EpLayout.EpVirtualBraces so that it carries an EpaLocation instead of just the Int column, to allow it to be used for both purposes. It is a simple mechanical change, with no other impact, but it allows us to use EpLayout instead of AnnListLayout in AnnList, in the next commit in this series. - - - - - 44 changed files: - + changelog.d/T13090-expose-overloaded-unfoldings - + changelog.d/T27830-rts-flag-bounds - compiler/GHC/Driver/DynFlags.hs - compiler/GHC/Driver/Flags.hs - compiler/GHC/Iface/Tidy.hs - compiler/GHC/Parser.y - compiler/GHC/Parser/Annotation.hs - compiler/GHC/Parser/PostProcess/Haddock.hs - docs/users_guide/runtime_control.rst - docs/users_guide/using-optimisation.rst - rts/RtsFlags.c - rts/include/rts/Flags.h - rts/include/rts/storage/GC.h - rts/sm/GC.c - rts/sm/Storage.c - testsuite/driver/junit.py - testsuite/driver/testglobals.py - testsuite/driver/testlib.py - testsuite/tests/dmdanal/should_compile/T23398.stderr - testsuite/tests/ghc-api/exactprint/T22919.stderr - testsuite/tests/ghc-api/exactprint/Test20239.stderr - testsuite/tests/ghc-api/exactprint/ZeroWidthSemi.stderr - testsuite/tests/haddock/should_compile_flag_haddock/T17544.stderr - testsuite/tests/haddock/should_compile_flag_haddock/T17544_kw.stderr - testsuite/tests/haddock/should_compile_flag_haddock/T24221.stderr - testsuite/tests/module/mod185.stderr - testsuite/tests/parser/should_compile/DumpParsedAst.stderr - testsuite/tests/parser/should_compile/DumpParsedAstComments.stderr - testsuite/tests/parser/should_compile/DumpSemis.stderr - testsuite/tests/parser/should_compile/KindSigs.stderr - testsuite/tests/parser/should_compile/T15323.stderr - testsuite/tests/parser/should_compile/T20452.stderr - testsuite/tests/parser/should_compile/T20718.stderr - testsuite/tests/parser/should_compile/T20718b.stderr - testsuite/tests/parser/should_compile/T20846.stderr - testsuite/tests/parser/should_compile/T23315/T23315.stderr - testsuite/tests/perf/compiler/all.T - testsuite/tests/printer/AnnotationNoListTuplePuns.stdout - testsuite/tests/printer/T18791.stderr - testsuite/tests/printer/Test20297.stdout - testsuite/tests/printer/Test24533.stdout - testsuite/tests/rts/all.T - testsuite/tests/rts/rtsflags001.stderr-ws-32 - testsuite/tests/rts/rtsflags001.stderr-ws-64 The diff was not included because it is too large. View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/ae66d1d9fb1ae303e95730efe2c497… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/ae66d1d9fb1ae303e95730efe2c497… 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

1 0

[Git][ghc/ghc][wip/T27844] 2 commits: Add regression test for #7803
by Simon Peyton Jones (＠simonpj) 29 Sep '26

29 Sep '26

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/0437d21cf0698b5b325be793df6d26… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/0437d21cf0698b5b325be793df6d26… 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

1 0