- ghc-commits - Haskell.org

[Git][ghc/ghc][wip/T27844] Switch off `do_not_prevent_rewriting` to see why it is useful
by Simon Peyton Jones (＠simonpj) 28 Sep '26

28 Sep '26

Simon Peyton Jones pushed to branch wip/T27844 at Glasgow Haskell Compiler / GHC Commits: 4f82c588 by Simon Peyton Jones at 2026-09-28T07:59:40+01:00 Switch off `do_not_prevent_rewriting` to see why it is useful - - - - - 1 changed file: - compiler/GHC/Tc/Solver/Equality.hs Changes: ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -2291,6 +2291,7 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs ; check_result <- checkTypeEq ev eq_rel lhs rhs ; case check_result of PuFail reason +{- | reason `cterHasOnlyProblems` do_not_prevent_rewriting -> do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped lhs rhs ; continueWith $ Right $ @@ -2298,6 +2299,7 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs , eq_lhs = lhs , eq_rhs = rhs } } | otherwise +-} -> -- 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. @@ -2328,6 +2330,7 @@ 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] @@ -2339,6 +2342,8 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs do_not_prevent_rewriting :: CheckTyEqResult do_not_prevent_rewriting = cteProblem cteSkolemEscape S.<> cteProblem cteConcrete +-} + ---------------------- finishCanWithIrred :: CtIrredReason -> CtEvidence -> TcS (StopOrContinue (Either IrredCt a)) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/4f82c588e8cfcf0540006d5c6532732… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/4f82c588e8cfcf0540006d5c6532732… 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] Switch off `do_not_prevent_rewriting` to see why it is useful
by Simon Peyton Jones (＠simonpj) 28 Sep '26

28 Sep '26

Simon Peyton Jones pushed to branch wip/T27844 at Glasgow Haskell Compiler / GHC Commits: 7efb4ae9 by Simon Peyton Jones at 2026-09-27T23:48:39+01:00 Switch off `do_not_prevent_rewriting` to see why it is useful - - - - - 1 changed file: - compiler/GHC/Tc/Solver/Equality.hs Changes: ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -2291,6 +2291,7 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs ; check_result <- checkTypeEq ev eq_rel lhs rhs ; case check_result of PuFail reason +{- | reason `cterHasOnlyProblems` do_not_prevent_rewriting -> do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped lhs rhs ; continueWith $ Right $ @@ -2298,6 +2299,7 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs , eq_lhs = lhs , eq_rhs = rhs } } | otherwise +-} -> -- 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. View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/7efb4ae9f22d9b73266e2c2cfa750b9… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/7efb4ae9f22d9b73266e2c2cfa750b9… 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/T27731] Wibbles [skip-ci]
by Simon Peyton Jones (＠simonpj) 28 Sep '26

28 Sep '26

Simon Peyton Jones pushed to branch wip/T27731 at Glasgow Haskell Compiler / GHC Commits: d2286d58 by Simon Peyton Jones at 2026-09-27T23:43:04+01:00 Wibbles [skip-ci] - - - - - 2 changed files: - compiler/GHC/Tc/Utils/Monad.hs - testsuite/tests/typecheck/should_fail/ClassOperator.stderr Changes: ===================================== compiler/GHC/Tc/Utils/Monad.hs ===================================== @@ -69,7 +69,7 @@ module GHC.Tc.Utils.Monad( wrapLocM, wrapLocFstM, wrapLocFstMA, wrapLocSndM, wrapLocSndMA, wrapLocM_, wrapLocMA_,wrapLocMA, getErrsVar, setErrsVar, - addErr, + addErr, captureMessagesTcM, failWith, failAt, addErrAt, addErrs, checkErr, checkErrAt, @@ -1604,26 +1604,26 @@ tcTryM thing_inside -- built-in in exception; see IOEnv.failM ----------------------- -capture_constraints :: TcM r -> TcM (r, WantedConstraints) --- capture_constraints simply captures and returns the +captureConstraintsTcM :: TcM r -> TcM (r, WantedConstraints) +-- captureConstraintsTcM simply captures and returns the -- constraints generated by thing_inside -- Precondition: thing_inside must not throw an exception! -- Reason for precondition: an exception would blow past the place -- where we read the lie_var, and we'd lose the constraints altogether -capture_constraints thing_inside +captureConstraintsTcM thing_inside = do { lie_var <- newTcRef emptyWC ; res <- updLclEnv (\ env -> env { tcl_lie = lie_var }) $ thing_inside ; lie <- readTcRef lie_var ; return (res, lie) } -capture_messages :: TcM r -> TcM (r, Messages TcRnMessage) --- capture_messages simply captures and returns the +captureMessagesTcM :: TcM r -> TcM (r, Messages TcRnMessage) +-- captureMessagesTcM simply captures and returns the -- errors and warnings generated by thing_inside -- Precondition: thing_inside must not throw an exception! -- Reason for precondition: an exception would blow past the place -- where we read the msg_var, and we'd lose the constraints altogether -capture_messages thing_inside +captureMessagesTcM thing_inside = do { msg_var <- newTcRef emptyMessages ; res <- setErrsVar msg_var thing_inside ; msgs <- readTcRef msg_var @@ -1643,8 +1643,8 @@ capture_messages thing_inside -- propagate any errors/warnings generated by m askErrsFound :: TcRn a -> TcRn (a, Bool) askErrsFound thing_inside - = do { ((mb_res, lie), msgs) <- capture_messages $ - capture_constraints $ + = do { ((mb_res, lie), msgs) <- captureMessagesTcM $ + captureConstraintsTcM $ tcTryM thing_inside ; addMessages msgs @@ -1665,7 +1665,7 @@ tryCaptureConstraints :: TcM a -> TcM (Maybe a, WantedConstraints) -- it returns Nothing and the /insoluble/ constraints -- Error messages are propagated tryCaptureConstraints thing_inside - = do { (mb_res, lie) <- capture_constraints $ + = do { (mb_res, lie) <- captureConstraintsTcM $ tcTryM thing_inside -- See Note [Constraints and errors] @@ -1794,7 +1794,7 @@ tryTc :: TcRn a -> TcRn (Maybe a, Messages TcRnMessage) -- It also returns all the errors and warnings accumulated by m -- It always succeeds (never raises an exception) tryTc thing_inside - = capture_messages (attemptM thing_inside) + = captureMessagesTcM (attemptM thing_inside) ----------------------- discardErrs :: TcRn a -> TcRn a @@ -1827,8 +1827,8 @@ tryTcDiscardingErrs' :: (WantedConstraints -> Messages TcRnMessage -> r -> Bool) -- otherwise discard everything from 'thing_inside', including errors, -- and try 'recover' instead. tryTcDiscardingErrs' validate recover_invalid recover_error thing_inside - = do { ((mb_res, lie), msgs) <- capture_messages $ - capture_constraints $ + = do { ((mb_res, lie), msgs) <- captureMessagesTcM $ + captureConstraintsTcM $ tcTryM thing_inside ; case mb_res of Just res | not (errorsFound msgs) ===================================== testsuite/tests/typecheck/should_fail/ClassOperator.stderr ===================================== @@ -1,52 +1,52 @@ - ClassOperator.hs:14:3: error: [GHC-39999] • Could not deduce ‘a ><> b0’ from the context: a ><> b bound by the type signature for: - (**>) :: forall a b. (a ><> b) => a -> a -> () + (<**) :: forall a b. (a ><> b) => a -> a -> () at ClassOperator.hs:14:3-44 The type variable ‘b0’ is ambiguous - • In the ambiguity check for ‘**>’ + • In the ambiguity check for ‘<**’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes When checking the class method: - (**>) :: forall a b. (a ><> b) => a -> a -> () + (<**) :: forall a b. (a ><> b) => a -> a -> () In the class declaration for ‘><>’ ClassOperator.hs:14:3: error: [GHC-39999] • Could not deduce ‘a ><> b0’ from the context: a ><> b bound by the type signature for: - (**<) :: forall a b. (a ><> b) => a -> a -> () + (>**) :: forall a b. (a ><> b) => a -> a -> () at ClassOperator.hs:14:3-44 The type variable ‘b0’ is ambiguous - • In the ambiguity check for ‘**<’ + • In the ambiguity check for ‘>**’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes When checking the class method: - (**<) :: forall a b. (a ><> b) => a -> a -> () + (>**) :: forall a b. (a ><> b) => a -> a -> () In the class declaration for ‘><>’ ClassOperator.hs:14:3: error: [GHC-39999] • Could not deduce ‘a ><> b0’ from the context: a ><> b bound by the type signature for: - (>**) :: forall a b. (a ><> b) => a -> a -> () + (**<) :: forall a b. (a ><> b) => a -> a -> () at ClassOperator.hs:14:3-44 The type variable ‘b0’ is ambiguous - • In the ambiguity check for ‘>**’ + • In the ambiguity check for ‘**<’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes When checking the class method: - (>**) :: forall a b. (a ><> b) => a -> a -> () + (**<) :: forall a b. (a ><> b) => a -> a -> () In the class declaration for ‘><>’ ClassOperator.hs:14:3: error: [GHC-39999] • Could not deduce ‘a ><> b0’ from the context: a ><> b bound by the type signature for: - (<**) :: forall a b. (a ><> b) => a -> a -> () + (**>) :: forall a b. (a ><> b) => a -> a -> () at ClassOperator.hs:14:3-44 The type variable ‘b0’ is ambiguous - • In the ambiguity check for ‘<**’ + • In the ambiguity check for ‘**>’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes When checking the class method: - (<**) :: forall a b. (a ><> b) => a -> a -> () + (**>) :: forall a b. (a ><> b) => a -> a -> () In the class declaration for ‘><>’ + View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/d2286d58c40bba550efdf12b2870b66… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/d2286d58c40bba550efdf12b2870b66… 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/az/exactprint-annotation-rationalisation] 59 commits: Correct the documentation of `explicitUnits`
by Alan Zimmerman (＠alanz) 27 Sep '26

27 Sep '26

Alan Zimmerman pushed to branch wip/az/exactprint-annotation-rationalisation at Glasgow Haskell Compiler / GHC Commits: 53eead15 by Wolfgang Jeltsch at 2026-09-24T20:12:03-04:00 Correct the documentation of `explicitUnits` Resolves #27787. - - - - - 35bf6f4b by Simon Jakobi at 2026-09-24T20:12:49-04:00 Remove stale specHeader bullet from Note [Don't make fillers for constraint types] The Note said that Specialise.specHeader also calls mkAbsentFiller. abfc224a27c removed that call: the specialiser no longer drops dead arguments at all, see Note [Do not drop dead args from specialisations] in GHC.Core.Opt.Specialise. Assisted-by: Claude Fable 5.1 - - - - - 1abef1ef by Wolfgang Jeltsch at 2026-09-25T17:02:07-04:00 Improve the `mhu-closure` makefile - - - - - a79a68ea by Wolfgang Jeltsch at 2026-09-25T17:02:07-04:00 Make `ghci-multi` hide all unneeded packages - - - - - d6e72450 by Wolfgang Jeltsch at 2026-09-25T17:02:07-04:00 Improve the definition of the home unit closure property - - - - - c9a2766d by Wolfgang Jeltsch at 2026-09-25T17:02:07-04:00 Re-implement the home unit closure check Compared to the previous implementation, the new one has the following advantages: * It is correct. - It distinguishes between units that have the same unit ID but different ABI hashes. - When `-hide-all-packages` is not used, it considers as home unit dependencies also units that are made implicitly available because they are in the package database. * It seems to be faster in usual settings. - In particular, it does not have a preparation phase in which it merges the dependency information from all home units, so that its running time does not grow linearly with the size of the package database in normal Cabal scenarios. * It is (hopefully) clearer. * It is better documented. - - - - - fa96acf8 by Wolfgang Jeltsch at 2026-09-25T17:02:07-04:00 Remove erroneous GHC flag in `hadrian-multi` The flag was `-Werror=-Wno-error=incomplete-record-selectors`. Its purpose was to permit incomplete record selectors, but because of the illegal combination of `-Werror=` and `-Wno-error` it was ignored, without any negative consequences. - - - - - 9f48a5b9 by Alan Zimmerman at 2026-09-25T17:02:50-04:00 EPA: Add specific layout field to AnnList Up to now AnnList has effectively served to represent lists of things having layout, regardless of whether they do or not. In Haskell, layout is optional in many places, as there is also an alternative syntax using braces and semi-colons, which is free-form. This commit introduces AnnListLayout, a data structure capturing this distinction. It is deliberately set up similarly to EpLayout, so that these two can be merged in time. The transition is done mechanically, where AnnListBraces is not used yet, the original Nothing case maps to AnnListNoLayout, and the Just case to AnnListLayout. Later commits will fine tune these against the actual parser layout. - - - - - 81e219fd by Alan Zimmerman at 2026-09-27T09:57:12+01: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. - - - - - 89ff21da by Alan Zimmerman at 2026-09-27T10:11:11+01:00 EPA: Use vocurly as basis for AnnListLayout For the existing cases that populate AnnList. This also shows up AnnList usages that can never capture layout. - - - - - 6bc967fa by Alan Zimmerman at 2026-09-27T10:11:11+01:00 EPA: AnnList clean up patch for empty where clause - - - - - d091def3 by Alan Zimmerman at 2026-09-27T10:11:11+01:00 EPA: Add TTG fields to FamilyInfo This commit is a simple add, with unused extension fields. It lays the groundwork for using them for exact print annotations - - - - - b4437661 by Alan Zimmerman at 2026-09-27T10:11:11+01:00 WIP annclassdecl - - - - - ee3e8896 by Alan Zimmerman at 2026-09-27T10:11:11+01:00 EPA: Update AnnClsInstDecl to contain AnnList It was already separately tracking the '{', '}' and leading ';' values. This aligns it with layout-introducing parser productions ('vocurly'), so the layout processing can be handled uniformly - - - - - 9312f068 by Alan Zimmerman at 2026-09-27T10:11:11+01:00 EPA: Tidy up markAnnListA' It takes an action which can modify the AnnList, but this is never used. So remove it. - - - - - 97f2bb65 by Alan Zimmerman at 2026-09-27T10:11:11+01:00 EPA: Use AnnList for GADT declarations - - - - - bf81506e by Alan Zimmerman at 2026-09-27T10:11:11+01:00 EPA: Use AnnList in AnnClassDecl - - - - - f930eea8 by Alan Zimmerman at 2026-09-27T10:11:11+01:00 MOVE EPA: Plan for Fixing AnnList Layout Properly - - - - - af4534ac by Alan Zimmerman at 2026-09-27T10:11:11+01:00 EPA: Make local binds located Use LHsLocalBinds instead of HsLocalBinds This reverses an earlier change, and brings processing of local binds into alignement with the exact printing principle that the LocatedA contents provide the location and extent of the enclosed item, together with any comments or context-specific trailing items like commas or semi colons. The internal TTG extension points only carry exact print annotations related to printing the item within its bounds. This change brings back the problem of EmptyLocalBinds, which by definition cannot have a location. These get a noSrcSpan location, which is ignored in the exact printing process. - - - - - 5bc8abf7 by Alan Zimmerman at 2026-09-27T10:11:11+01:00 EPA: Use AnnList in HsMultiIf It introduces layout, capture it - - - - - 701dbb38 by Alan Zimmerman at 2026-09-27T10:11:11+01:00 EPA: Use AnnList in DecBrl - - - - - b21856e1 by Alan Zimmerman at 2026-09-27T10:11:11+01:00 EPA: Replace AnnListLayout / AnnListBrackets with EpLayout - - - - - 3d1b5cee by Alan Zimmerman at 2026-09-27T10:11:11+01:00 WIP: setLayoutBoth inside markAnnListA Current problem is it is a global one-shot, and MG has one too Check: is it needed? if so, honouring EpLayout may be needed - - - - - 517d9c62 by Alan Zimmerman at 2026-09-27T10:11:11+01:00 EPA some tests for layout. WIP - - - - - 250e388f by Alan Zimmerman at 2026-09-27T10:11:11+01:00 MOVE: Exactprint layout scope plan. Do not commit - - - - - a8bda73c by Alan Zimmerman at 2026-09-27T10:11:11+01:00 EPA: tidy up a bit. Combine somewhere else - - - - - b0623353 by Alan Zimmerman at 2026-09-27T10:11:11+01:00 EPA: Introduce LayoutFrame stacks in ExactPrint state - - - - - 0d74271f by Alan Zimmerman at 2026-09-27T10:11:11+01:00 Align with ghc-exactprint - - - - - 4c71a47a by Alan Zimmerman at 2026-09-27T10:11:11+01:00 EPA: Fix AnnList leading semis when layout When there is layout, anything printed triggers it, including leading semis. Add some test case examples too - - - - - f3198746 by Alan Zimmerman at 2026-09-27T10:11:11+01:00 Exactprint: tidy up layout capturing - - - - - b01f993d by Alan Zimmerman at 2026-09-27T10:11:11+01:00 EPA: add makeDelta test for Test20297 The original #20297 related to comment placement for exact printing after running ExactPrint.makeDelta on ParsedSource. Add an additional test that explicitly tests this. - - - - - a462788f by Alan Zimmerman at 2026-09-27T10:11:11+01:00 EPA: Make ValBinds LocatedA in HsLocalBindsLR If we have items with an AnnList Annotation, as part of another, which has different content, it must be LocatedA. This is a technical requirement due to the way comment allocation happens during the makeDelta processing. Comments are queued for printing, and as soon as any non-comment is to be printed, the pending comments before that position are printed, and in makeDelta processing these attached as preceding comments to the thing just printed. The means they end up captured inside the layout region of the AnnList item. So for foo = x where -- comment x = 3 the comment ends up as a preceding comment of `x = 3`, inside the layout, and prints as foo = x where -- comment x = 3 - - - - - 366a7f4c by Alan Zimmerman at 2026-09-27T10:11:11+01:00 EPA: Make IPBinds LocatedA - - - - - 859c4ead by Alan Zimmerman at 2026-09-27T10:11:11+01:00 EPA: Make ClsInstDecl decls LocatedA - - - - - 6333e313 by Alan Zimmerman at 2026-09-27T10:11:11+01:00 EPA: Make ClassDecls decls LocatedA - - - - - 5f5e4bd2 by Alan Zimmerman at 2026-09-27T10:11:11+01:00 EPA: Make ClosedTypeFamily equations Located For FamilyDecl/ClosedTypeFamily - - - - - ddb07ab0 by Alan Zimmerman at 2026-09-27T10:11:11+01:00 EPA: Make dd_cons located - - - - - 90ca508c by Alan Zimmerman at 2026-09-27T10:11:11+01:00 EPA: Make HsMultiIf options located - - - - - e32e1d5d by Alan Zimmerman at 2026-09-27T10:11:11+01:00 EPA: Make DecBrl contents LocatedA - - - - - d48bd4ed by Alan Zimmerman at 2026-09-27T10:11:11+01:00 EPA: Located do statements - - - - - 5acd759a by Alan Zimmerman at 2026-09-27T10:11:11+01:00 EPA: Print RecStmt located - - - - - d1d40ffb by Alan Zimmerman at 2026-09-27T10:11:11+01:00 EPA: HsCmdDo Located - - - - - a60b28fa by Alan Zimmerman at 2026-09-27T10:11:11+01:00 Extend Test20297 for additional occurrences - - - - - cef6a257 by Alan Zimmerman at 2026-09-27T10:11:11+01:00 EPA: Tweak PatSynBind location for comments - - - - - 4d9588bc by Alan Zimmerman at 2026-09-27T10:11:11+01:00 EPA: WIP, add test for where ;; ValBinds - - - - - fc91c514 by Alan Zimmerman at 2026-09-27T10:11:11+01:00 EPA: Make EpVirtualBraces noSpanAnchor if no contents Otherwise the vocurly is emitted at the start of the next item parsed Check: is this needed, or just a check for empty contents? - - - - - 9914ff22 by Alan Zimmerman at 2026-09-27T16:09:47+01:00 EPA: Use EpNoLayout in AnnList with empty contents and no explicit braces TODO: get rid of unused first arg to epVirtualBraces - - - - - c13ed1d8 by Alan Zimmerman at 2026-09-27T16:10:19+01:00 TODO: XClassDecl: remove additional EpLayout - - - - - fd49b138 by Alan Zimmerman at 2026-09-27T16:10:19+01:00 WIP: turn off exactprint debug printing - - - - - 2ca50511 by Alan Zimmerman at 2026-09-27T16:10:19+01:00 EPA: Remove CanUpdateAnchorOnly - - - - - 53f9429e by Alan Zimmerman at 2026-09-27T16:10:19+01:00 EPA: Sync with ghc-exactprint after EPWriter -> CPS - - - - - eb753e22 by Alan Zimmerman at 2026-09-27T18:43:49+01:00 EPA: Fix EpVirtualBraces for HsDo The start of layout must include the leading semi, so we comb3 to ensure it is included if the initial stmts are empty - - - - - 23f600c3 by Alan Zimmerman at 2026-09-27T18:45:21+01:00 Plan update DO NOT COMMIT - - - - - 3ba8e610 by Alan Zimmerman at 2026-09-27T18:45:21+01:00 EPA: First pass implementation of HsList, for ClassDecls Just as a straight list replacement to start with, no payload. This shows the scope and invasiveness of the initial change - - - - - badd3010 by Alan Zimmerman at 2026-09-27T18:45:21+01:00 EPA: HsList attempt WIP - - - - - 850a5f08 by Alan Zimmerman at 2026-09-27T18:45:21+01:00 Enable ppr test for Haddock1. It currently fails - - - - - f1d8367c by Alan Zimmerman at 2026-09-27T18:45:21+01:00 WIP on removing NoEpAnn. Likely abandon - - - - - 26d9b114 by Alan Zimmerman at 2026-09-27T18:45:21+01:00 EPA: Add an overview doc for exact printing - - - - - 0a75a65b by Simon Peyton Jones at 2026-09-27T18:45:21+01:00 Added an intro section - - - - - 115 changed files: - .gitlab-ci.yml - + ANNLIST-LAYOUT-PLAN.md - + ExactPrint.md - + LAYOUT-SCOPE-PLAN.md - compiler/GHC/Core/Opt/WorkWrap/Utils.hs - compiler/GHC/Driver/Backpack.hs - compiler/GHC/Driver/Downsweep.hs - compiler/GHC/Driver/Errors/Ppr.hs - compiler/GHC/Driver/Errors/Types.hs - compiler/GHC/Driver/Main/Interactive.hs - compiler/GHC/Hs.hs - compiler/GHC/Hs/Binds.hs - compiler/GHC/Hs/Decls.hs - compiler/GHC/Hs/DocString.hs - compiler/GHC/Hs/Dump.hs - compiler/GHC/Hs/Expr.hs - compiler/GHC/Hs/ImpExp.hs - compiler/GHC/Hs/Instances.hs - compiler/GHC/Hs/Stats.hs - compiler/GHC/Hs/Utils.hs - compiler/GHC/HsToCore/Arrows.hs - compiler/GHC/HsToCore/Docs.hs - compiler/GHC/HsToCore/Expr.hs - compiler/GHC/HsToCore/Expr.hs-boot - compiler/GHC/HsToCore/Match.hs - compiler/GHC/HsToCore/Pmc/Desugar.hs - compiler/GHC/HsToCore/Quote.hs - compiler/GHC/HsToCore/Ticks.hs - compiler/GHC/Iface/Ext/Ast.hs - compiler/GHC/Parser.y - compiler/GHC/Parser/Annotation.hs - compiler/GHC/Parser/PostProcess.hs - compiler/GHC/Parser/PostProcess/Haddock.hs - compiler/GHC/Rename/Bind.hs - compiler/GHC/Rename/Expr.hs - compiler/GHC/Rename/Module.hs - compiler/GHC/Rename/Names.hs - compiler/GHC/Rename/Splice.hs - compiler/GHC/Rename/Utils.hs - compiler/GHC/Runtime/Eval.hs - compiler/GHC/Tc/Deriv.hs - compiler/GHC/Tc/Deriv/Functor.hs - compiler/GHC/Tc/Deriv/Generate.hs - compiler/GHC/Tc/Gen/Arrow.hs - compiler/GHC/Tc/Gen/Bind.hs - compiler/GHC/Tc/Gen/Expr.hs - compiler/GHC/Tc/Gen/Match.hs - compiler/GHC/Tc/Module.hs - compiler/GHC/Tc/TyCl.hs - compiler/GHC/Tc/TyCl/Instance.hs - compiler/GHC/Tc/TyCl/PatSyn.hs - compiler/GHC/Tc/Types/Origin.hs - compiler/GHC/Tc/Utils/Env.hs - compiler/GHC/Tc/Zonk/Type.hs - compiler/GHC/ThToHs.hs - compiler/GHC/Unit/Env.hs - compiler/GHC/Unit/State.hs - compiler/Language/Haskell/Syntax.hs - compiler/Language/Haskell/Syntax/Basic.hs - compiler/Language/Haskell/Syntax/Binds.hs - compiler/Language/Haskell/Syntax/Decls.hs - compiler/Language/Haskell/Syntax/Expr.hs - compiler/Language/Haskell/Syntax/Extension.hs - ghc/GHCi/UI.hs - hadrian/ghci-multi-cabal.in - testsuite/tests/driver/multipleHomeUnits/mhu-closure/Makefile - testsuite/tests/driver/multipleHomeUnits/mhu-closure/mhu-closure.stderr - testsuite/tests/driver/multipleHomeUnits/mhu-closure/mhu-closure.stdout - 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/DumpRenamedAst.stderr - testsuite/tests/parser/should_compile/DumpSemis.hs - testsuite/tests/parser/should_compile/DumpSemis.stderr - testsuite/tests/parser/should_compile/DumpTypecheckedAst.stderr - testsuite/tests/parser/should_compile/KindSigs.stderr - testsuite/tests/parser/should_compile/T14189.stderr - testsuite/tests/parser/should_compile/T15279.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/hard_hole_fits.stderr - testsuite/tests/printer/AnnotationNoListTuplePuns.stdout - + testsuite/tests/printer/Layout.hs - testsuite/tests/printer/Makefile - testsuite/tests/printer/Ppr003.hs - testsuite/tests/printer/T18791.stderr - + testsuite/tests/printer/Test20297.expected.hs - testsuite/tests/printer/Test20297.hs - testsuite/tests/printer/Test20297.stdout - + testsuite/tests/printer/Test20297MD.stdout - testsuite/tests/printer/Test24533.stdout - testsuite/tests/printer/all.T - utils/check-exact/ExactPrint.hs - utils/check-exact/Main.hs - utils/check-exact/Parsers.hs - utils/check-exact/Transform.hs - utils/check-exact/Utils.hs - utils/haddock/haddock-api/src/Haddock/Backends/Hoogle.hs - utils/haddock/haddock-api/src/Haddock/Backends/LaTeX.hs - utils/haddock/haddock-api/src/Haddock/Backends/Xhtml/Decl.hs - utils/haddock/haddock-api/src/Haddock/Convert.hs - utils/haddock/haddock-api/src/Haddock/GhcUtils.hs - utils/haddock/haddock-api/src/Haddock/Interface/Create.hs - utils/haddock/haddock-api/src/Haddock/Interface/Rename.hs - utils/haddock/haddock-api/src/Haddock/Types.hs The diff was not included because it is too large. View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/88562119b53de864156349b1b274f7… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/88562119b53de864156349b1b274f7… 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/io-manager-deadlock-detection] 33 commits: Correct the documentation of `explicitUnits`
by Duncan Coutts (＠dcoutts) 27 Sep '26

27 Sep '26

Duncan Coutts pushed to branch wip/io-manager-deadlock-detection at Glasgow Haskell Compiler / GHC Commits: 53eead15 by Wolfgang Jeltsch at 2026-09-24T20:12:03-04:00 Correct the documentation of `explicitUnits` Resolves #27787. - - - - - 35bf6f4b by Simon Jakobi at 2026-09-24T20:12:49-04:00 Remove stale specHeader bullet from Note [Don't make fillers for constraint types] The Note said that Specialise.specHeader also calls mkAbsentFiller. abfc224a27c removed that call: the specialiser no longer drops dead arguments at all, see Note [Do not drop dead args from specialisations] in GHC.Core.Opt.Specialise. Assisted-by: Claude Fable 5.1 - - - - - 1abef1ef by Wolfgang Jeltsch at 2026-09-25T17:02:07-04:00 Improve the `mhu-closure` makefile - - - - - a79a68ea by Wolfgang Jeltsch at 2026-09-25T17:02:07-04:00 Make `ghci-multi` hide all unneeded packages - - - - - d6e72450 by Wolfgang Jeltsch at 2026-09-25T17:02:07-04:00 Improve the definition of the home unit closure property - - - - - c9a2766d by Wolfgang Jeltsch at 2026-09-25T17:02:07-04:00 Re-implement the home unit closure check Compared to the previous implementation, the new one has the following advantages: * It is correct. - It distinguishes between units that have the same unit ID but different ABI hashes. - When `-hide-all-packages` is not used, it considers as home unit dependencies also units that are made implicitly available because they are in the package database. * It seems to be faster in usual settings. - In particular, it does not have a preparation phase in which it merges the dependency information from all home units, so that its running time does not grow linearly with the size of the package database in normal Cabal scenarios. * It is (hopefully) clearer. * It is better documented. - - - - - fa96acf8 by Wolfgang Jeltsch at 2026-09-25T17:02:07-04:00 Remove erroneous GHC flag in `hadrian-multi` The flag was `-Werror=-Wno-error=incomplete-record-selectors`. Its purpose was to permit incomplete record selectors, but because of the illegal combination of `-Werror=` and `-Wno-error` it was ignored, without any negative consequences. - - - - - 9f48a5b9 by Alan Zimmerman at 2026-09-25T17:02:50-04:00 EPA: Add specific layout field to AnnList Up to now AnnList has effectively served to represent lists of things having layout, regardless of whether they do or not. In Haskell, layout is optional in many places, as there is also an alternative syntax using braces and semi-colons, which is free-form. This commit introduces AnnListLayout, a data structure capturing this distinction. It is deliberately set up similarly to EpLayout, so that these two can be merged in time. The transition is done mechanically, where AnnListBraces is not used yet, the original Nothing case maps to AnnListNoLayout, and the Just case to AnnListLayout. Later commits will fine tune these against the actual parser layout. - - - - - 388f9c66 by Duncan Coutts at 2026-09-27T18:43:02+01:00 Move idle GC tracking to its own file, step 1 of 2 Add a new IdleGC.{c,h} module. Move the RecentActivity type, recent_activity variable and {get,set}RecentActivity wrappers. - - - - - fac92964 by Duncan Coutts at 2026-09-27T18:43:02+01:00 Move idle GC functionality to its own file, step 2 of 2 We can now fully encapsulate the recent_activity state, exposing just three hooks, and one query used in the scheduler and timer tick. This is a prelude to making changes to the implementation of tracking when to perform an idle gc. - - - - - 39167176 by Duncan Coutts at 2026-09-27T18:43:02+01:00 Correct comments in idle GC code The comments still referred to stopTimer/startTimer. These were replaced recently by pauseTimer/unpauseTimer, but the comment was not updated. - - - - - 6ceae159 by Duncan Coutts at 2026-09-27T18:43:02+01:00 Make signal handling be a responsibility of the I/O manager(s) Previously it was scattered between I/O managers and the scheduler, and especially the scheduler's deadlock detection. Previously the scheduler would poll for pending signals each iteration of the scheduler loop. The scheduler also had some hairy signal functionality in the deadlock detection: in the non-threaded RTS (only) if there were still no threads running after deadlock detection then it would block waiting for signals. But signals can and (in my opinion) should be thought of as just a funny kind of I/O, and thus should be a responsibility of the I/O manager. So now we have the I/O managers poll for signals when they are polling for I/O completion (and removing the separate poll in the scheduler). And when I/O managers block waiting for I/O then they now also start signal handlers if they get interrupted by a signal. Crucially, if there is no pending I/O or timers, the awaitCompletedTimeoutsOrIO will still block waiting for signals. This patch puts us into an intermediate state: it temporarily breaks deadlock detection in the non-threaded RTS. The waiting on I/O currently happens before deadlock detection. This means we'll now wait forever on signals before doing deadlock detection. We need to move waiting after deadlock detection. We'll do that in a later patch. - - - - - 2d010a57 by Duncan Coutts at 2026-09-27T18:43:02+01:00 Clean up the RTS internal signal handling API Now that the I/O manager is responsible for signals, we can simplify the API we present for signal handling. We now just need startPendingSignalHandlers, which is called from the I/O managers. We can get rid of awaitUserSignals. We also don't need RtsSignals.h to re-export the platform-specific posix/Signals.h or win32/ConsoleHandler.h We can also hide more of the implementation of signals. Less has to be exposed in posix/Signals.h or win32/ConsoleHandler.h. Indeed, posix/Signals.h becomes empty and we remove it. Partly this is because we don't need inline functions (or macros) in the interface. Also remove signal_handlers from RTS ABI exported symbols list. It does not appear to have any users in the core libs, and its really an internal implementation detail. It should not be exposed unless it's really necessary. - - - - - 345837c6 by Duncan Coutts at 2026-09-27T18:43:02+01:00 In the scheduler, move I/O blocking after deadlock detection To make deadlock detection effective in the non-threaded RTS when there are deadlocked threads and other unrelated threads waiting on I/O, we need to arrange to do deadlock detection before we block in scheduler to wait on I/O. The solution is to: 1. adjust scheduleFindWork, which runs before deadlock detection, to only poll for I/O and not block; and 2. add a step after deadlock detection to wait on I/O if there are still no threads to run (and there's any I/O or timeouts outstanding) The scheduleCheckBlockedThreads is now so simple that it made more sense to inline it into scheduleFindWork. - - - - - 2456bc80 by Duncan Coutts at 2026-09-27T18:43:02+01:00 Remove bogus anyPendingTimeoutsOrIO guard from scheduleDetectDeadlock The deadlock detection was only invoked if both of these conditions hold: 1. the run queue is empty 2. there is no pending I/O or timeouts The second condition is unnecessary. The deadlock detection mechanism can find deadlocks even if there are other threads waiting on I/O or timers. Having this extra condition means that we fail to detect blocked threads if there are any threads waiting on I/O or timers. Part of fixing issue #26408 - - - - - 84a9ada4 by Duncan Coutts at 2026-09-27T18:43:02+01:00 Don't consider pending I/O for early context switch optimisation Context switches are normally initiated by the timer signal. If however the user specifies "context switch as often as possible", with +RTS -C0 then the scheduler arranges for an early context switch (when it's just about to run a Haskell thread). Context switching very often is expensive, so as an optimisation there cases where we do not arrange an early context switch: 1. if there's no other threads to run 2. if there is no pending I/O or timers This patch eliminates case 2, leaving only case 1. The rationale is as follows. The use of this was inconsistent across platforms and threaded/non-threaded RTS ways. It only worked on the non-threaded RTS and on Windows only worked for the win32-legacy I/O manager. On all other combinations anyPendingTimeoutsOrIO would always return false. The fact that nobody noticed and complained about this inconsistency suggests that the feature is not relied upon. If however it turns out that applications do rely on this, then the proper thing to do is not to restore this check, but to add a new I/O manager hint function that returns if there is any pending events that are likely to happen *soon*: for example timeouts expiring within one timeslice, or I/O waits on things likely to complete soon like disk I/O, but not for example socket/pipe I/O. The motivation to avoid this use of anyPendingTimeoutsOrIO is to allow us to eliminate anyPendingTimeoutsOrIO entirely. All other uses of this are just guards on {await,poll}CompletedTimeoutsOrIO and the guards can safely be folded into those functions. This will better cope with some I/O managers having no proper implementation of anyPendingTimeoutsOrIO. Ultimately this will let us simplify the scheduler which currently has to have special #ifdef mingw32_HOST_OS cases to cope with the lack of a working anyPendingTimeoutsOrIO for some Windows I/O managers - - - - - 0bfa75e3 by Duncan Coutts at 2026-09-27T18:43:02+01:00 Remove anyPendingTimeoutsOrIO guarding {poll,await}CompletedTimeoutsOrIO Previously the API of the I/O manager used a two step process: check anyPendingTimeoutsOrIO and then call {poll,await}CompletedTimeoutsOrIO. This was primarily there as a performance thing, to cheaply check if we need to do anything. And then because anyPendingTimeoutsOrIO existed, it was used for other things too. We have now eliminated the other uses, and are just left with the performance pattern. But this was problematic because not all I/O managers correctly implement anyPendingTimeoutsOrIO (specifically the win32 ones), and now that we also make I/O managers responsible for signals then we need to poll/await even if there is no pending I/O or timeouts. If there is no pending I/O or timeouts then await needs to degenerate to just waiting forever for any signals. - - - - - 1af20d4f by Duncan Coutts at 2026-09-27T18:43:02+01:00 Remove anyPendingTimeoutsOrIO, it is no longer used And this avoids the problems arising from the win32 I/O managers having had a bogus implementation. - - - - - b89c0adc by Duncan Coutts at 2026-09-27T18:43:02+01:00 Remove second scheduler call to awaitCompletedTimeoutsOrIO Previously awaitCompletedTimeoutsOrIO was called both before and after deadlock detection in the scheduler. The reason for that was that the win32 I/O managers had a bogus implementation of anyPendingTimeoutsOrIO and this was used to guard the call of awaitCompletedTimeoutsOrIO prior to deadlock detection. This meant the first call site was never actually called when using the win32 I/O managers. This was the reason for the second call: the first one was never used. What a mess. So now we have a simple design in the scheduler: 1. poll for completed I/O, timers or signals 2. if no runnable threads: do deadlock detection 3. if still no runnable threads: block waiting for I/O, timers or signals. - - - - - e9d80b12 by Duncan Coutts at 2026-09-27T18:43:03+01:00 Lift emptyRunQueue guard out of scheduleDetectDeadlock this improved the clarity of the logic when reading the scheduler code. And improve the comment about scheduleDoGC that was rather unclear. - - - - - f446219c by Duncan Coutts at 2026-09-27T18:43:03+01:00 Make interruptIOManager work for WinIO (non-threaded) Fixes #27403 The idle GC scheme now fundamentally relies on interruptIOManager working, so it's no longer acceptable for it to be missing for WinIO. Not having it would cause lock ups. - - - - - 901ef7bb by Duncan Coutts at 2026-09-27T18:43:03+01:00 Make non-threaded deadlock detection also rely on idle GC Only do deadlock detection GC when idle GC kicks in. This also relies on using wakeUpRts, so now do this unconditionally. Previously wakeUpRts was for the threaded rts only. - - - - - 6c43daa1 by Duncan Coutts at 2026-09-27T18:43:03+01:00 Enable idle GC by default on non-threaded RTS The behaviour is now uniform between the threaded and non-threaded RTS ways. The deadlock detection now relies on idle GC for both threaded and non-threaded ways. Previously deadlock detection did not rely on idle GC for the non-threaded way. Also tweak test T7275 to account for idle GC. This test's output is sensitive to the number of major GCs run. Since this commit enables idle GC for the non-threaded RTS, for this test that increases the number of major GCs, since the test program is frequently idle for more than 300ms. - - - - - 32e5b061 by Duncan Coutts at 2026-09-27T18:43:03+01:00 Fix state of idle GC control vars with +RTS -V0 Currently when the user uses +RTS -I0, then doIdleGC is set to false. But if the master tick interval -V is set to 0 then the idleGCDelayTime was being set to 0 but doIdleGC was not being set to false, which is inconsistent, and almost certainly buggy. - - - - - e2cdb1a0 by Duncan Coutts at 2026-09-27T18:43:03+01:00 Add a long Note [Deadlock detection] It describes the historical and modern designs and their trade-offs. The point is we've now unified the code for deadlock detection between the threaded and non-threaded ways, by changing the non-threaded to follow the same design as the threaded. - - - - - 9f15516c by Duncan Coutts at 2026-09-27T18:43:03+01:00 Refactor the utils providing the I/O timeout for different system APIs We have to provide a timeout in three different time formats (int milliseconds, struct timeval *, and struct timespec *). These are for platform APIs including poll, select, ppoll, pselect, epoll_wait, epoll_wait2 and in future kevent and io_uring. Previously we had one util for each format that both worked out what the timeout should be and converted it into the particular format. This duplicates some logic and it also makes it awkward to modify the timeout value (since there's no common format). Modifying the timeout value is exactly what we want to do, in a subsequent commit, where we want to adjust the timeout to take account of idle GC. - - - - - bbf4dbb7 by Duncan Coutts at 2026-09-27T18:43:03+01:00 Update the old select I/O manager to use the new timeout utils This will make it much easier to adjust the timeout to take account of idle GC. - - - - - 97a922ba by Duncan Coutts at 2026-09-27T18:43:03+01:00 Add opportunistic deadlock detection without idle GC Our general design is now that comprehensive deadlock detection relies on idle GC. This allows us to detect partial deadlocks that are not system deadlocks. But it's not prompt. It's a nice to have feature to be able to promptly detect the cases that are system deadlocks. There's no hope to do this in the threaded RTS with -N > 1, but it can be done for the non-threaded RTS and _could_ be done for the threaded RTS with -N1. We can integrate this feature into the general design without too many contortions. We just need the I/O managers to check before sleeping if they would be about to sleep indefinately with no I/O and no registered signal handlers. If so, they can notify the idle GC that we're deadlocked and we schedule and idle GC. - - - - - aada868f by Duncan Coutts at 2026-09-27T18:43:03+01:00 Add idle GC mode for !HAVE_PREEMPTION We have to do idle GC (and thus deadlock detection) differently when we do not have the ticker and the ability to interrupt the I/O manager when it's blocking. - - - - - e81a7fd7 by Duncan Coutts at 2026-09-27T18:43:03+01:00 Add and use USED_IF_PREEMPTION to avoid warnings - - - - - aade1797 by Duncan Coutts at 2026-09-27T18:43:03+01:00 Add performDeadlockDetection and export via ghc-experimental When documenting the idle GC and deadlock detection behaviour in the user guide, it becomes obiovus that in some cases one would want manual control over deadlock detection. In particular, for applications that disable idle GC, for debugging or robustness, they may want to invoke deadlock detecting GC manually. Bind it in ghc-internal GHC.Internal.System.Mem and re-export via ghc-experimental in System.Mem.Experimental. It is clearly implementation specific behaviour, especially since in GHC the deadlock detection is tied to doing a major GC. - - - - - d0af4f3d by Duncan Coutts at 2026-09-27T18:43:03+01:00 Add tests for deadlock detection, issue #26408 We have three tests: T26408a: make sure that we can detect a /partial deadlock/ that is not also a /system deadlock/ T26408b: make sure that we can detect a /system deadlock/ promptly without relying on idle GC T26408c: make sure that we do not falsely detect a deadlock when there is nothing to do except wait on signals - - - - - e5743b87 by Duncan Coutts at 2026-09-27T18:43:03+01:00 Update the user guide with the revised idle GC behaviour It's now not just for the threaded RTS, but general. Add a new section in the RTS chapter: Idle GC and deadlock detection. Provide general documentation on both topics. In particular, document the behaviour of deadlock detection and how it depends on idle GC. Move the existing entries for -I and -Iw to this section. Add a changelog entry. - - - - - 78 changed files: - .gitlab-ci.yml - + changelog.d/idle-gc-and-deadlock-detection - compiler/GHC/Core/Opt/WorkWrap/Utils.hs - compiler/GHC/Driver/Downsweep.hs - compiler/GHC/Driver/Errors/Ppr.hs - compiler/GHC/Driver/Errors/Types.hs - compiler/GHC/Parser.y - compiler/GHC/Parser/Annotation.hs - compiler/GHC/Parser/PostProcess.hs - compiler/GHC/Unit/Env.hs - compiler/GHC/Unit/State.hs - docs/users_guide/profiling.rst - docs/users_guide/runtime_control.rst - hadrian/ghci-multi-cabal.in - libraries/ghc-experimental/src/System/Mem/Experimental.hs - libraries/ghc-internal/src/GHC/Internal/System/Mem.hs - rts/Capability.c - rts/IOManager.c - rts/IOManager.h - + rts/IdleGC.c - + rts/IdleGC.h - rts/Linker.c - rts/RtsFlags.c - rts/RtsSignals.h - rts/RtsStartup.c - rts/RtsSymbols.c - rts/Schedule.c - rts/Schedule.h - rts/Timer.c - rts/include/rts/OSThreads.h - rts/include/rts/storage/GC.h - rts/posix/Poll.c - rts/posix/Poll.h - rts/posix/Select.c - rts/posix/SelectBis.c - rts/posix/SelectBis.h - rts/posix/Signals.c - − rts/posix/Signals.h - rts/posix/Timeout.c - rts/posix/Timeout.h - rts/rts.cabal - rts/win32/AsyncMIO.c - rts/win32/AsyncMIO.h - rts/win32/AsyncWinIO.c - rts/win32/AsyncWinIO.h - rts/win32/AwaitEvent.c - rts/win32/ConsoleHandler.c - rts/win32/ConsoleHandler.h - testsuite/tests/driver/multipleHomeUnits/mhu-closure/Makefile - testsuite/tests/driver/multipleHomeUnits/mhu-closure/mhu-closure.stderr - testsuite/tests/driver/multipleHomeUnits/mhu-closure/mhu-closure.stdout - testsuite/tests/ghc-api/exactprint/T22919.stderr - testsuite/tests/ghc-api/exactprint/ZeroWidthSemi.stderr - testsuite/tests/interface-stability/ghc-experimental-exports.stdout - testsuite/tests/interface-stability/ghc-experimental-exports.stdout-mingw32 - testsuite/tests/module/mod185.stderr - testsuite/tests/parser/should_compile/DumpParsedAst.stderr - testsuite/tests/parser/should_compile/DumpParsedAstComments.stderr - testsuite/tests/parser/should_compile/DumpRenamedAst.stderr - testsuite/tests/parser/should_compile/DumpSemis.stderr - testsuite/tests/parser/should_compile/KindSigs.stderr - testsuite/tests/parser/should_compile/T15279.stderr - testsuite/tests/parser/should_compile/T20718.stderr - testsuite/tests/parser/should_compile/T20846.stderr - testsuite/tests/printer/Test20297.stdout - testsuite/tests/printer/Test24533.stdout - testsuite/tests/profiling/should_run/Makefile - testsuite/tests/rts/Makefile - + testsuite/tests/rts/T26408a.hs - + testsuite/tests/rts/T26408a.stderr - + testsuite/tests/rts/T26408b.hs - + testsuite/tests/rts/T26408b.stderr - + testsuite/tests/rts/T26408c.hs - + testsuite/tests/rts/T26408c.stdout - testsuite/tests/rts/all.T - utils/check-exact/ExactPrint.hs - utils/check-exact/Main.hs - utils/check-exact/Transform.hs The diff was not included because it is too large. View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/f3468063892902795d7fd9fc26b2b7… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/f3468063892902795d7fd9fc26b2b7… 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/T26543b] Wibbles
by Simon Peyton Jones (＠simonpj) 27 Sep '26

27 Sep '26

Simon Peyton Jones pushed to branch wip/T26543b at Glasgow Haskell Compiler / GHC Commits: 96bc4a6e by Simon Peyton Jones at 2026-09-27T18:39:25+01:00 Wibbles - - - - - 9 changed files: - compiler/GHC/Core/TyCo/FVs.hs - compiler/GHC/Tc/Gen/App.hs - compiler/GHC/Tc/Utils/Unify.hs - testsuite/tests/default/default-fail05.stderr - testsuite/tests/ghci.debugger/scripts/T14628.stderr - testsuite/tests/indexed-types/should_fail/T1897b.stderr - testsuite/tests/typecheck/should_fail/T22707.stderr - + testsuite/tests/typecheck/should_fail/T26543a.hs - testsuite/tests/typecheck/should_fail/all.T Changes: ===================================== compiler/GHC/Core/TyCo/FVs.hs ===================================== @@ -55,7 +55,6 @@ module GHC.Core.TyCo.FVs ) where import GHC.Prelude -import GHC.Exts( inline ) import {-# SOURCE #-} GHC.Core.Type( partitionInvisibleTypes, coreView, rewriterView ) @@ -852,8 +851,11 @@ invisibleVarsOfTypes = foldr (unionVarSet . invisibleVarsOfType) emptyVarSet {- Note [Any-free-var folder] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The "any-free-var" folders take a `check_fv` predicate (TyCoVar -> Bool) and -check if any free variable of the type/coercion satisfies it. Our main folders -look like: +check if any /deep/ free variable of the type/coercion satisfies it. So + + anyFreeVarsOfType p ty = anyVarSet p (tyCoVarsOfType ty) + +Our main folders look like: afv_type :: Type -> FV (BoundVars, TyVar -> Bool) Any @@ -871,7 +873,7 @@ nice tight loops. {-# INLINE afvFolder #-} -- See Note [Any-free-var folder] afvFolder :: TyCoFolder (FV (BoundVars, TyCoVar -> Bool) DM.Any) -- 'afvFolder' is short for "any-free-var folder", good for checking --- if any shallow free var of a type satisfies a predicate `check_fv` +-- if any /deep/ free var of a type satisfies a predicate `check_fv` -- The "env" of the (FV env Any) is a pair (bvs,pred) of -- the bound variables (which are definitely not free), and -- an "interesting var" predicate which the client supplies @@ -881,8 +883,11 @@ afvFolder = TyCoFolder { tcf_view = noView -- See Note [Free vars and synonyms] , tcf_hole = do_hole , tcf_tycobinder = addBndrSelectiveFV } where - do_tcv tv = MkFV $ \ (bvs,check_fv) -> - Any (not (tv `elemVarSet` bvs) && check_fv tv) + -- Check the variable itself with check_fv, + -- and check its kind (this is a deep folder) + do_tcv tcv = MkFV $ \ (bvs,check_fv) -> + Any (not (tcv `elemVarSet` bvs) && + (check_fv tcv || runAny check_fv (afv_type (varType tcv)))) do_hole hole = do_tcv (coHoleCoVar hole) afv_type :: Type -> FV (BoundVars, TyVar -> Bool) DM.Any @@ -892,7 +897,7 @@ afv_co :: Coercion -> FV (BoundVars, TyVar -> Bool) DM.Any runAny :: (TyVar -> Bool) -> FV (BoundVars, TyCoVar -> Bool) DM.Any -> Bool {-# INLINE runAny #-} -runAny check_fv fvs = DM.getAny $ runFV fvs (emptyVarSet, check_fv) +runAny check_fv fvs = DM.getAny (runFV fvs (emptyVarSet, check_fv)) anyFreeVarsOfType :: (TyCoVar -> Bool) -> Type -> Bool {-# INLINE anyFreeVarsOfType #-} ===================================== compiler/GHC/Tc/Gen/App.hs ===================================== @@ -2196,10 +2196,9 @@ qlUnify ty1 ty2 -- the main point of QuickLook (allowing meta-variables to be unified -- with qualified types). - go' (TyVarTy tv) ty2 - | isQLInstTyVar tv = go_kappa tv ty2 - go' ty1 (TyVarTy tv) - | isQLInstTyVar tv = go_kappa tv ty1 + -- Type variables; see (UQL6) in Note [QuickLook unification] + go' (TyVarTy tv) ty2 | isQLInstTyVar tv = go_kappa tv ty2 + go' ty1 (TyVarTy tv) | isQLInstTyVar tv = go_kappa tv ty1 go' (CastTy ty1 _) ty2 = go ty1 ty2 go' ty1 (CastTy ty2 _) = go ty1 ty2 @@ -2242,6 +2241,8 @@ qlUnify ty1 ty2 ---------------- go_flexi kappa ty2 -- ty2 is zonked + | isConcreteTyVar kappa -- See (UQL7) in Note [QuickLook unification] + = return () | anyFreeVarsOfType (== kappa) ty2 = return () -- Occurs check | otherwise @@ -2340,6 +2341,22 @@ That is the entire point of qlUnify! Wrinkles: constraint arrows =>, so that (UQL4) applies to them as well. See Note [Multiplicity in deep subsumption]. +(UQL6) What if `qlUnify` sees a regular (monotyped) unification variable, `alpha`, rather + than an instantiation variable `kappa`? Thus (alpha ~ ty). It's tempting to just + unify it, but the regular, on-the-fly unifier has lots of careful checks (levels, + concreteness etc). In regular unification it doesn't matter whether we unify on-the-fly + or later -- it's just an efficiency issue -- but here it matters because `qlUnify` has + /user-visible/ consequences. This led to #26543. + + The simplest thing is to say that `qlUnify` unifies /only/ instantiation variables + (see calls to `isQLInstTyVar`). We could be more ambitious, perhaps, in future. + +(UQL7) If `qlUnify` sees a concrete `kaapa`, thus + kappa[conc] ~ some-type + we just give up. It's tiresome to do all the checks for concreteness; and concrete + type variables are never unified with polytypes, so it's fine to leave it for the + regular unifier. + Sadly discarded design alternative ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ It is very tempting to use `unifyType` rather than `qlUnify`, killing off the ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -3596,7 +3596,6 @@ matchExpectedFunKind hs_ty n k = go n k data UnifyCheckCaller = UC_OnTheFly -- Called from the on-the-fly unifier - | UC_QuickLook -- Called from Quick Look | UC_Solver -- Called from constraint solver -- | The result type of 'simpleUnifyCheck'. @@ -3649,9 +3648,7 @@ simpleUnifyCheck caller given_eq_lvl lhs_tv rhs lhs_tv_is_concrete = isConcreteTyVar lhs_tv lhs_tv_nm = tyVarName lhs_tv - forall_ok = case caller of - UC_QuickLook -> isQLInstTyVar lhs_tv - _ -> isRuntimeUnkTyVar lhs_tv + forall_ok = isRuntimeUnkTyVar lhs_tv -- This fam_ok thing relates to a very specific perf problem -- See Note [Prevent unification with type families] @@ -3660,7 +3657,6 @@ simpleUnifyCheck caller given_eq_lvl lhs_tv rhs -- see if it bites us) fam_ok = case caller of UC_Solver -> True - UC_QuickLook -> True UC_OnTheFly -> False rhs_tcv_is_bad tcv ===================================== testsuite/tests/default/default-fail05.stderr ===================================== @@ -1,45 +1,45 @@ default-fail05.hs:11:10: error: [GHC-39999] - • Ambiguous type variable ‘f0’ arising from a use of ‘toList’ - prevents the constraint ‘(Foldable f0)’ from being solved. - Probable fix: use a type annotation to specify what ‘f0’ should be. + • Ambiguous type variable ‘t0’ arising from a use of ‘toList’ + prevents the constraint ‘(Foldable t0)’ from being solved. + Probable fix: use a type annotation to specify what ‘t0’ should be. Potentially matching instances: instance Foldable (Either a) -- Defined in ‘GHC.Internal.Data.Foldable’ instance Foldable Maybe -- Defined in ‘GHC.Internal.Data.Foldable’ ...plus three others - ...plus 26 instances involving out-of-scope types + ...plus 11 instances involving out-of-scope types (use -fprint-potential-instances to see them all) • In the first argument of ‘($)’, namely ‘toList’ In the first argument of ‘print’, namely ‘(toList $ pure 21)’ In a stmt of a 'do' block: print (toList $ pure 21) default-fail05.hs:11:19: error: [GHC-39999] - • Ambiguous type variable ‘f0’ arising from a use of ‘pure’ - prevents the constraint ‘(Applicative f0)’ from being solved. - Probable fix: use a type annotation to specify what ‘f0’ should be. + • Ambiguous type variable ‘t0’ arising from a use of ‘pure’ + prevents the constraint ‘(Applicative t0)’ from being solved. + Probable fix: use a type annotation to specify what ‘t0’ should be. Potentially matching instances: instance Applicative IO -- Defined in ‘GHC.Internal.Base’ instance Applicative Maybe -- Defined in ‘GHC.Internal.Base’ ...plus six others - ...plus 9 instances involving out-of-scope types + ...plus five instances involving out-of-scope types (use -fprint-potential-instances to see them all) • In the second argument of ‘($)’, namely ‘pure 21’ In the first argument of ‘print’, namely ‘(toList $ pure 21)’ In a stmt of a 'do' block: print (toList $ pure 21) default-fail05.hs:12:3: error: [GHC-39999] - • Ambiguous type variable ‘t0’ arising from a use of ‘traverse’ - prevents the constraint ‘(Traversable t0)’ from being solved. + • Ambiguous type variable ‘t1’ arising from a use of ‘traverse’ + prevents the constraint ‘(Traversable t1)’ from being solved. Relevant bindings include - main :: IO (t0 ()) (bound at default-fail05.hs:10:1) - Probable fix: use a type annotation to specify what ‘t0’ should be. + main :: IO (t1 ()) (bound at default-fail05.hs:10:1) + Probable fix: use a type annotation to specify what ‘t1’ should be. Potentially matching instances: instance Traversable (Either a) -- Defined in ‘GHC.Internal.Data.Traversable’ instance Traversable Maybe -- Defined in ‘GHC.Internal.Data.Traversable’ ...plus three others - ...plus 28 instances involving out-of-scope types + ...plus 13 instances involving out-of-scope types (use -fprint-potential-instances to see them all) • In a stmt of a 'do' block: traverse print (pure 42) In the expression: @@ -51,16 +51,16 @@ default-fail05.hs:12:3: error: [GHC-39999] traverse print (pure 42) default-fail05.hs:12:19: error: [GHC-39999] - • Ambiguous type variable ‘t0’ arising from a use of ‘pure’ - prevents the constraint ‘(Applicative t0)’ from being solved. + • Ambiguous type variable ‘t1’ arising from a use of ‘pure’ + prevents the constraint ‘(Applicative t1)’ from being solved. Relevant bindings include - main :: IO (t0 ()) (bound at default-fail05.hs:10:1) - Probable fix: use a type annotation to specify what ‘t0’ should be. + main :: IO (t1 ()) (bound at default-fail05.hs:10:1) + Probable fix: use a type annotation to specify what ‘t1’ should be. Potentially matching instances: instance Applicative IO -- Defined in ‘GHC.Internal.Base’ instance Applicative Maybe -- Defined in ‘GHC.Internal.Base’ ...plus six others - ...plus 9 instances involving out-of-scope types + ...plus five instances involving out-of-scope types (use -fprint-potential-instances to see them all) • In the second argument of ‘traverse’, namely ‘(pure 42)’ In a stmt of a 'do' block: traverse print (pure 42) ===================================== testsuite/tests/ghci.debugger/scripts/T14628.stderr ===================================== @@ -1,9 +1,9 @@ - -<interactive>:4:17: error: [GHC-25897] +<interactive>:4:7: error: [GHC-25897] • Couldn't match type ‘m’ with ‘(,) a0’ - Expected: StateT Int ((,) a0) () - Actual: StateT Int m () + Expected: (a0, ((), Int)) + Actual: m ((), Int) ‘m’ is an interactive-debugger skolem - • In the first argument of ‘runStateT’, namely ‘_result’ - In the second argument of ‘($)’, namely ‘runStateT _result 0’ + • In the second argument of ‘($)’, namely ‘runStateT _result 0’ In the expression: snd $ runStateT _result 0 + In an equation for ‘it’: it = snd $ runStateT _result 0 + ===================================== testsuite/tests/indexed-types/should_fail/T1897b.stderr ===================================== @@ -1,14 +1,14 @@ T1897b.hs:16:1: error: [GHC-83865] - • Couldn't match type: Depend b0 - with: Depend b - Expected: t (Depend b) -> Bool - Actual: t (Depend b0) -> Bool + • Couldn't match type: Depend a0 + with: Depend a + Expected: t (Depend a) -> Bool + Actual: t (Depend a0) -> Bool Note: ‘Depend’ is a non-injective type family. - The type variable ‘b0’ is ambiguous + The type variable ‘a0’ is ambiguous • In the ambiguity check for the inferred type for ‘isValid’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes When checking the inferred type - isValid :: forall {t :: * -> *} {b}. - (Foldable t, Bug b) => - t (Depend b) -> Bool + isValid :: forall {t :: * -> *} {a}. + (Foldable t, Bug a) => + t (Depend a) -> Bool ===================================== testsuite/tests/typecheck/should_fail/T22707.stderr ===================================== @@ -1,38 +1,11 @@ -T22707.hs:6:59: error: [GHC-25897] - • Couldn't match expected type ‘i1’ - with actual type ‘m0 - GHC.Internal.Types.LiftedRep GHC.Internal.Types.LiftedRep b0’ - ‘i1’ is a rigid type variable bound by - the type signature for: - t1 :: forall i2 o i1 a. Cont (i2 -> o) i1 a -> Cont o i2 (a -> i1) - at T22707.hs:5:1-47 - • In the expression: evalCont (t1 c) >>== \ ati1 -> return ati1 xa - In the second argument of ‘($)’, namely - ‘\ xa -> evalCont (t1 c) >>== \ ati1 -> return ati1 xa’ - In the second argument of ‘runCont’, namely - ‘(ati1tti2 $ \ xa -> evalCont (t1 c) >>== \ ati1 -> return ...)’ - • Relevant bindings include - ati1tti2 :: (a -> i1) -> i2 (bound at T22707.hs:6:16) - c :: Cont (i2 -> o) i1 a (bound at T22707.hs:6:4) - t1 :: Cont (i2 -> o) i1 a -> Cont o i2 (a -> i1) - (bound at T22707.hs:6:1) - T22707.hs:6:72: error: [GHC-25897] - • Couldn't match type ‘o’ - with ‘m0 - GHC.Internal.Types.LiftedRep - GHC.Internal.Types.LiftedRep - (m0 GHC.Internal.Types.LiftedRep GHC.Internal.Types.LiftedRep b0)’ + • Couldn't match type ‘i2’ with ‘a -> i1’ Expected: Cont - ((a -> i1) - -> m0 - GHC.Internal.Types.LiftedRep - GHC.Internal.Types.LiftedRep - (m0 GHC.Internal.Types.LiftedRep GHC.Internal.Types.LiftedRep b0)) + ((a -> i1) -> m0 (a -> i1) (a -> i1) (m0 (a -> i1) (a -> i1) b0)) i1 a Actual: Cont (i2 -> o) i1 a - ‘o’ is a rigid type variable bound by + ‘i2’ is a rigid type variable bound by the type signature for: t1 :: forall i2 o i1 a. Cont (i2 -> o) i1 a -> Cont o i2 (a -> i1) at T22707.hs:5:1-47 @@ -40,6 +13,9 @@ T22707.hs:6:72: error: [GHC-25897] In the first argument of ‘evalCont’, namely ‘(t1 c)’ In the first argument of ‘(>>==)’, namely ‘evalCont (t1 c)’ • Relevant bindings include + xa :: a (bound at T22707.hs:6:53) + ati1tti2 :: (a -> m0 (a -> i1) (a -> i1) b0) -> a -> i1 + (bound at T22707.hs:6:16) c :: Cont (i2 -> o) i1 a (bound at T22707.hs:6:4) t1 :: Cont (i2 -> o) i1 a -> Cont o i2 (a -> i1) (bound at T22707.hs:6:1) ===================================== testsuite/tests/typecheck/should_fail/T26543a.hs ===================================== @@ -0,0 +1,18 @@ +{-# LANGUAGE ImpredicativeTypes, PolyKinds #-} + +-- Should be rejected via an occurs-check in the kinds, +-- but was erroneously accpeted with ImpredicativeTypes +-- See !16566 + +module T26543 where + +import Data.Kind +import Data.Proxy + +h :: forall k (m :: k -> Type) (a :: k). (Proxy k, Proxy (m a)) +h = (Proxy, Proxy) + +use2 :: forall t. (Proxy t, Proxy t) -> () +use2 _ = () + +test = use2 h ===================================== 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('T26543a', normal, compile_fail, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/96bc4a6e5f7285e907e682705867b4f… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/96bc4a6e5f7285e907e682705867b4f… 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: Further wibbles
by Simon Peyton Jones (＠simonpj) 27 Sep '26

27 Sep '26

Simon Peyton Jones pushed to branch wip/T27844 at Glasgow Haskell Compiler / GHC Commits: 0f5ff61c by Simon Peyton Jones at 2026-09-27T17:31:10+01:00 Further wibbles - - - - - 26bd3aa5 by Simon Peyton Jones at 2026-09-27T18:37:50+01:00 More wibbles ...incl a new assert in the _no_unification case - - - - - 4 changed files: - compiler/GHC/Tc/Solver/Equality.hs - compiler/GHC/Tc/Solver/Monad.hs - compiler/GHC/Tc/Utils/Unify.hs - testsuite/tests/indexed-types/should_fail/T9662.stderr Changes: ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -1824,7 +1824,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 @@ -2213,6 +2213,9 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs -- 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" $ @@ -2229,21 +2232,19 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs = finish_no_unify where - -- We can't unify, but we can see if 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 + -- 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 - -- Phew! Finally! We can unify; go ahead and do so. + -- 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 @@ -2280,39 +2281,41 @@ 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 + -- 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 checkTypeEq 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 ; 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 - -- See Note [Orienting TyVarLHS/TyFamLHS] - -- ToDo: fix me ... also needed for a ~ G (F a) - -- 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 - | Just can_rhs <- canTyFamEqLHS_maybe rhs - , reason `cterHasOnlyProblem` cteSolubleOccurs - -> finishWith ev eq_rel (flipSwap swapped) can_rhs lhs_ty - | reason `cterHasOnlyProblems` do_not_prevent_rewriting - -> finishWith ev eq_rel swapped lhs rhs + -> 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 + -> -- Claim: there should be no new_eqs + -- The non-unification check does non promotion nor type-family + -- flattening for Wanteds + 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 { emitWork new_eqs ; let new_holes = rewriterSetFromCts new_eqs + lhs_ty = canEqLHSType lhs lhs_redn = mkReflRedn (eqRelRole eq_rel) lhs_ty ; new_ev <- rewriteEqEvidence ev swapped lhs_redn rhs_redn new_holes @@ -2336,45 +2339,7 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs do_not_prevent_rewriting :: CheckTyEqResult do_not_prevent_rewriting = cteProblem cteSkolemEscape S.<> cteProblem cteConcrete - ----------------------- -finishWith :: CtEvidence -> EqRel -> SwapFlag - -> CanEqLHS -> TcType - -> TcS (StopOrContinue (Either unused EqCt)) -finishWith ev eq_rel swapped can_lhs rhs_ty - = do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped can_lhs rhs_ty - ; continueWith $ Right $ - EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel - , eq_lhs = can_lhs , eq_rhs = rhs_ty } } - -{- -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 } } --} - ---------------------- -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 @@ -2394,8 +2359,26 @@ 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 `checkTypeEq`to see if it is canonical (which in turn + calls `checkTypeEqRhs`). + +* Even if `checkTypeEq` returns `PuFail`, we may /still/ be able to add it to the inert + set, depending on the reason for failure; examples are given in `do_not_prevent_rewriting`. + +* 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 [Equalities with heterogeneous kinds] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ What do we do when we have an equality (tv :: k1) ~ (rhs :: k2) @@ -3066,8 +3049,6 @@ inertsEqsCanDischarge inerts (EqCt { eq_lhs = lhs_w, eq_rhs = rhs_w inertsEqsCanDischarge _ _ = Nothing - - {- Note [Do not unify Givens] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider this GADT match @@ -3133,34 +3114,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/Monad.hs ===================================== @@ -2333,7 +2333,7 @@ checkTypeEq ev eq_rel lhs rhs = 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) + -- or [G] F a ~ Maybe (F a) -- occ_prob: see Note [Occurs check and representational equality] occ_prob = case eq_rel of ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -4203,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. @@ -4224,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]. ===================================== 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) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/f3b36989d97f7839876ec4f47142cf… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/f3b36989d97f7839876ec4f47142cf… 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/az/epa-tidy-locatedxxx-26
by Alan Zimmerman (＠alanz) 27 Sep '26

27 Sep '26

Alan Zimmerman pushed new branch wip/az/epa-tidy-locatedxxx-26 at Glasgow Haskell Compiler / GHC -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/tree/wip/az/epa-tidy-locatedxxx-26 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/apk/tag-strict-bot] Fix a few tag inference bugs.
by Andreas Klebinger (＠AndreasK) 26 Sep '26

26 Sep '26

Andreas Klebinger pushed to branch wip/apk/tag-strict-bot at Glasgow Haskell Compiler / GHC Commits: 44222807 by Andreas Klebinger at 2026-09-26T13:12:34+00:00 Fix a few tag inference bugs. * Treat bottoming functions and nullary join points as functions. * When generating bytecode don't rely on imported tag sigs. Fixes #27831, #27841 and #27842. - - - - - 23 changed files: - + changelog.d/T27831-bottoming-strict-field - + changelog.d/T27842-bytecode-imported-tags - compiler/GHC/Stg/EnforceEpt.hs - compiler/GHC/Stg/EnforceEpt/Rewrite.hs - compiler/GHC/Stg/EnforceEpt/Types.hs - + testsuite/tests/bytecode/T27842.hs - + testsuite/tests/bytecode/T27842.stdout - + testsuite/tests/bytecode/T27842A.hs - + testsuite/tests/bytecode/T27842N.hs - testsuite/tests/bytecode/all.T - testsuite/tests/simplStg/should_compile/all.T - + testsuite/tests/simplStg/should_compile/inferTags005.hs - + testsuite/tests/simplStg/should_compile/inferTags005.stderr - + testsuite/tests/simplStg/should_compile/inferTags006.hs - + testsuite/tests/simplStg/should_compile/inferTags006.stderr - + testsuite/tests/simplStg/should_run/InferTags007_A.hs - + testsuite/tests/simplStg/should_run/T27831.hs - + testsuite/tests/simplStg/should_run/T27831.stdout - + testsuite/tests/simplStg/should_run/T27857.hs - + testsuite/tests/simplStg/should_run/T27857.stdout - testsuite/tests/simplStg/should_run/all.T - + testsuite/tests/simplStg/should_run/inferTags007.hs - + testsuite/tests/simplStg/should_run/inferTags007.stdout Changes: ===================================== changelog.d/T27831-bottoming-strict-field ===================================== @@ -0,0 +1,8 @@ +section: compiler +issues: #27831 +mrs: !16719 +synopsis: + Fix a segfault that could occur when a bottoming function was stored in a strict field. +description: + This was happening when a function that always diverges (e.g. ``\_ -> error "..."``) was stored in a strict field, and the constructor was pattern matched on + in "nearby" code where the structure of the constructor application was still visible to GHC. ===================================== changelog.d/T27842-bytecode-imported-tags ===================================== @@ -0,0 +1,6 @@ +section: bytecode +issues: #27842 +mrs: !16719 +synopsis: + Fix a segfault caused by reusing interface files generated with + ``-fbyte-code-and-object-code`` for interpreter sessions using ``-fprefer-byte-code``. ===================================== compiler/GHC/Stg/EnforceEpt.hs ===================================== @@ -334,9 +334,15 @@ a) Tags for let-bindings: b) When referencing ids from other modules the Cmm backend will try to put a proper tag on these references through various means. When doing analysis we usually predict these cases to improve precision of the analysis. - But to my knowledge the bytecode generator makes no such attempts so we must - not infer imported bindings as tagged. - This is handled in GHC.Stg.EnforceEpt.Types.lookupInfo + The bytecode generator gives fewer guarantees about what it tags. + So we simply assume it fails to tag binders, even in the cases where it does. + + This is handled in GHC.Stg.EnforceEpt.Types.argTagInfo + + Eventually we will want to update the Analysis and bco code gen to uphold and + take advantage of tag inference at least to some degree. But for now it's + not a perf benefit for interpreted code, and essentially only run to uphold + the "strict field invariant"/EPT Invariant described in EPT enforcement. -} @@ -359,7 +365,7 @@ enforceEpt ppr_opts !for_bytecode logger this_mod stg_binds = do -- Rewrite STG to uphold the strict field invariant us_t <- mkSplitUniqSupply StgTag - let rewritten_binds = {-# SCC "StgEptRewrite" #-} rewriteTopBinds this_mod us_t stg_binds_w_tags :: [TgStgTopBinding] + let rewritten_binds = {-# SCC "StgEptRewrite" #-} rewriteTopBinds for_bytecode this_mod us_t stg_binds_w_tags :: [TgStgTopBinding] return (rewritten_binds,export_tag_info) @@ -414,12 +420,14 @@ inferTagExpr env (StgApp fun args) | isDeadEndAppSig (idDmdSig fun) (length args) = TagBottoming - | fun_arity == 0 -- Unknown arity => Thunk or unknown call + | not (isJoinId fun) -- zero arity join ids behave like functions. + , fun_arity == 0 -- Unknown arity => Thunk or unknown call = TagDunno -- Imported function with known return tag | Just (TagFun res_info) <- tagSigInfo (idInfo fun) , fun_arity == length args -- Saturated + , not (te_bytecode env) -- #27842 = res_info -- Local function with known return tag @@ -613,8 +621,8 @@ it safely any tag sig we like. So we give it TagBottoming, as it allows the combined tag sig of the case expression to be the combination of all non-bottoming branches. -NB: After the analysis is done we go back to treating bottoming functions as -untagged to ensure they are evaluated as expected in code like: +NB: We now distinguish functions from values. Allowing us to treat bottom functions +as tagged, while still doing the right thing for bottom values in code like: case bottom_id of { ...} ===================================== compiler/GHC/Stg/EnforceEpt/Rewrite.hs ===================================== @@ -13,7 +13,7 @@ import GHC.Builtin.PrimOps ( PrimOp(..) ) import GHC.Types.Basic ( CbvMark (..), isMarkedCbv , TopLevelFlag(..), isTopLevel ) import GHC.Types.Id -import GHC.Types.Name +import GHC.Types.Name ( nameIsLocalOrFrom ) import GHC.Types.Unique.Supply import GHC.Types.Unique.FM import GHC.Types.RepType @@ -22,10 +22,7 @@ import GHC.Unit.Types import GHC.Core.DataCon import GHC.Core ( AltCon(..) ) -import GHC.Core.Type - -import GHC.StgToCmm.Types -import GHC.StgToCmm.Closure (importedIdLFInfo) +import GHC.Core.Type ( definitelyLiftedType ) import GHC.Stg.Utils import GHC.Stg.Syntax as StgSyn @@ -41,7 +38,7 @@ import GHC.Stg.EnforceEpt.Types import Control.Monad -newtype RM a = RM { unRM :: (State (UniqFM Id TagSig, UniqSupply, Module, IdSet) a) } +newtype RM a = RM { unRM :: (State (UniqFM Id TagSig, UniqSupply, Module, IdSet, Bool) a) } deriving (Functor, Monad, Applicative) ------------------------------------------------------------ @@ -108,29 +105,34 @@ when building the free variable list. instance MonadUnique RM where getUniqueSupplyM = RM $ do - (m, us, mod,lcls) <- get + (m, us, mod,lcls,for_bytecode) <- get let (us1, us2) = splitUniqSupply us - (put) (m,us2,mod,lcls) + (put) (m,us2,mod,lcls,for_bytecode) return us1 getMap :: RM (UniqFM Id TagSig) -getMap = RM $ ((\(fst,_,_,_) -> fst) <$> get) +getMap = RM $ ((\(fst,_,_,_,_) -> fst) <$> get) setMap :: (UniqFM Id TagSig) -> RM () setMap !m = RM $ do - (_,us,mod,lcls) <- get - put (m, us,mod,lcls) - -getMod :: RM Module -getMod = RM $ ( (\(_,_,thrd,_) -> thrd) <$> get) + (_,us,mod,lcls,for_bytecode) <- get + put (m, us,mod,lcls,for_bytecode) getFVs :: RM IdSet -getFVs = RM $ ((\(_,_,_,lcls) -> lcls) <$> get) +getFVs = RM $ ((\(_,_,_,lcls,_) -> lcls) <$> get) setFVs :: IdSet -> RM () setFVs !fvs = RM $ do - (tag_map,us,mod,_lcls) <- get - put (tag_map, us,mod,fvs) + (tag_map,us,mod,_lcls,for_bytecode) <- get + put (tag_map, us,mod,fvs,for_bytecode) + +getMod :: RM Module +getMod = RM $ ( (\(_,_,c,_,_) -> c) <$> get) + +-- | When generating bytecode certain bindings might be untagged. So we have to +-- have a way to check for that. +getForBytecode :: RM Bool +getForBytecode = RM $ ((\(_,_,_,_,for_bytecode) -> for_bytecode) <$> get) -- Rewrite the RHS(s) while making the id and it's sig available -- to determine if things are tagged/need to be captured as FV. @@ -238,51 +240,26 @@ indicates a bug in the tag inference implementation. For this reason we assert that we are running in interactive mode if a lookup fails. -} isTagged :: Id -> RM Bool -isTagged v - -- See Note [Bottom functions are TagBottoming] - | isDeadEndId v = pure False - | otherwise = do +isTagged v = do + for_bytecode <- getForBytecode this_mod <- getMod - -- See Note [Tag inference for interactive contexts] - let lookupDefault v = assertPpr (isInteractiveModule this_mod) - (text "unknown Id:" <> ppr this_mod <+> ppr v) - (TagVal TagDunno) - case nameIsLocalOrFrom this_mod (idName v) of - True - | definitelyUnliftedType (idType v) - -- NB: v might be the Id of a representation-polymorphic join point, - -- so we shouldn't use isUnliftedType here. See T22212. - -> return True - | otherwise -> do -- Local binding - !s <- getMap - let !sig = lookupWithDefaultUFM s (lookupDefault v) v - return $ case sig of - TagFun _ -> True -- function closure is tagged - TagVal TagDunno -> False - TagVal TagEPT -> True - TagVal TagBottoming -> True - TagVal (TagTuple _) -> True -- Consider unboxed tuples tagged. - -- Imported - False -> return $! - -- Determine whether it is tagged from the LFInfo of the imported id. - -- See Note [The LFInfo of Imported Ids] - case importedIdLFInfo v of - -- Function, applied not entered. - LFReEntrant {} - -> True - -- Thunks need to be entered. - LFThunk {} - -> False - -- LFCon means we already know the tag, and it's tagged. - LFCon {} - -> True - LFUnknown {} - -> False - LFUnlifted {} -- Unboxed, tagging irrelevant - -> True - LFLetNoEscape {} - -- Shouldn't be possible. I don't think we can export letNoEscapes - -> True + s <- getMap + let get_env_sig = lookupUFM s + massertPpr + -- Assert the env is complete for local lifted binders, which means either + -- - The binder is present in the env + -- - The binder is not a local lifted binder *or* comes from a ghci context + (isJust (get_env_sig v) + -- See Note [Tag inference for interactive contexts] + || isInteractiveModule this_mod + || not (nameIsLocalOrFrom this_mod (idName v)) + || not (definitelyLiftedType (idType v))) + (text "unknown Id:" <> ppr this_mod <+> ppr v) + -- TODO: We could refactor the whole pass such that we also set id_tagSig + -- for every imported id. But this likely comes with a heavy allocation + -- overhead so for now we just ensure to use the same logic across analysis + -- and rewriter. + pure $! isTaggedInfo $ argTagInfo for_bytecode (get_env_sig v) (StgVarArg v) isArgTagged :: StgArg -> RM Bool @@ -299,11 +276,12 @@ mkLocalArgId id = do --------------------------- -rewriteTopBinds :: Module -> UniqSupply -> [GenStgTopBinding 'InferTaggedBinders] -> [TgStgTopBinding] -rewriteTopBinds mod us binds = +rewriteTopBinds :: Bool -- ^ Generating bytecode? + -> Module -> UniqSupply -> [GenStgTopBinding 'InferTaggedBinders] -> [TgStgTopBinding] +rewriteTopBinds for_bytecode mod us binds = let doBinds = mapM rewriteTop binds - in evalState (unRM doBinds) (mempty, us, mod, mempty) + in evalState (unRM doBinds) (mempty, us, mod, mempty, for_bytecode) rewriteTop :: InferStgTopBinding -> RM TgStgTopBinding rewriteTop (StgTopStringLit v s) = return $! (StgTopStringLit v s) ===================================== compiler/GHC/Stg/EnforceEpt/Types.hs ===================================== @@ -12,7 +12,7 @@ where import GHC.Prelude import GHC.Core.DataCon -import GHC.Core.Type (isUnliftedType) +import GHC.Core.Type (isUnliftedType, definitelyUnliftedType) import GHC.Types.Id import GHC.Stg.Syntax import GHC.Stg.EnforceEpt.TagSig as TagSig @@ -22,6 +22,7 @@ import GHC.Utils.Misc( zipWithEqual ) import GHC.Utils.Panic import GHC.StgToCmm.Types +import GHC.StgToCmm.Closure (importedIdLFInfo) {- ********************************************************************* * * @@ -97,31 +98,39 @@ lookupReturnInfo env fun = case lookupVarEnv (te_env env) fun of Just (TagVal _) -> Nothing Nothing -> Nothing --- | Look up a value-level tag for an argument: either from the env (where --- a function-typed argument flattens to TagEPT — its closure is tagged) --- or derived from information on the variable itself. -lookupInfo :: TagEnv p -> StgArg -> TagInfo -lookupInfo env (StgVarArg var) +-- | Look up a value-level tag. +-- +-- If the tag info is completely determined by Id info we use that tag. +-- If the tag info is dependent on the analysis/call site use the passed TagSig. +-- If the passed TagSig is Nothing we fall back to safe tag info based on id properties. +argTagInfo :: Bool -> (Maybe TagSig) -> StgArg -> TagInfo +{-# INLINE argTagInfo #-} -- Specialize for the call site. +argTagInfo _for_bytecode _env_sig (StgLitArg{}) = TagEPT +argTagInfo for_bytecode env_sig (StgVarArg var) -- Nullary data constructors like True, False | Just dc <- isDataConWorkId_maybe var , isNullaryRepDataCon dc , not for_bytecode = TagEPT - | isUnliftedType (idType var) + -- NB: v might be the Id of a representation-polymorphic join point, + -- so we shouldn't use isUnliftedType here. See T22212. + | definitelyUnliftedType (idType var) = TagEPT -- Variables in the environment. A function binding flattens to TagEPT -- since a function closure pointer is properly tagged; its return info -- is not relevant when the function is used as a value. - | Just sig <- lookupVarEnv (te_env env) var + | Just sig <- env_sig = case sig of TagVal info -> info TagFun _ -> TagEPT - | Just lf_info <- idLFInfo_maybe var - , not for_bytecode - = case lf_info of +-- Always save defaults. + | lf_info <- importedIdLFInfo var -- will make up LFInfo if not present. + = if for_bytecode then TagDunno + else + case lf_info of -- Function, tagged (with arity) LFReEntrant {} -> TagEPT @@ -138,13 +147,12 @@ lookupInfo env (StgVarArg var) -- Shouldn't be possible. I don't think we can export letNoEscapes LFLetNoEscape {} -> panic "LFLetNoEscape exported" - | otherwise - = TagDunno - where - for_bytecode = te_bytecode env - -lookupInfo _ (StgLitArg {}) - = TagEPT +-- | Get tag info using the environment. +lookupInfo :: TagEnv p -> StgArg -> TagInfo +lookupInfo env arg@(StgVarArg var) = + let env_sig = (lookupVarEnv (te_env env) var) + in argTagInfo (te_bytecode env) env_sig arg +lookupInfo _env (StgLitArg{}) = TagEPT isDunnoSig :: TagSig -> Bool isDunnoSig (TagVal TagDunno) = True ===================================== testsuite/tests/bytecode/T27842.hs ===================================== @@ -0,0 +1,42 @@ +{-# LANGUAGE UnboxedTuples #-} +{-# OPTIONS_GHC -fno-worker-wrapper -fno-cpr-anal #-} +-- Regression test for #27842. +-- +-- The basic rundown is this: +-- We produce one interface file, however we store information dependent on the +-- code generation method in the interface file. +-- +-- We happen to pick the native code information to store in the interface file. +-- +-- When we compile a module M this way, and then generate byte code for code +-- depending on M based on M.hi we will assume certain exported definitions are EPT +-- tagged, despite the interpreter doing no such thing. +-- +-- This then led to crashes in the interpreter. +-- +-- We test three kinds of imported definitions: +-- * mk uses fun, a function whose TagSig says its result is tagged. +-- * bar uses just_con, a value whose LFInfo says it is a constructor. +-- * baz uses gt_con, the same for a nullary constructor. +module Main where + +import T27842A (fun, just_con, gt_con) +import T27842N (S(..), use_S, M(..), use_M, N(..), use_N) + +mk :: Int -> S +mk x = case fun x of (# xs, _ #) -> S xs +{-# NOINLINE mk #-} + +bar :: M +bar = M just_con +{-# NOINLINE bar #-} + +baz :: N +baz = N gt_con +{-# NOINLINE baz #-} + +main :: IO () +main = do + print (use_S (mk 42)) + print (use_M bar) + print (use_N baz) ===================================== testsuite/tests/bytecode/T27842.stdout ===================================== @@ -0,0 +1,3 @@ +42 +42 +3 ===================================== testsuite/tests/bytecode/T27842A.hs ===================================== @@ -0,0 +1,19 @@ +{-# LANGUAGE UnboxedTuples #-} +{-# OPTIONS_GHC -fno-worker-wrapper -fno-cpr-anal #-} +module T27842A (fun, just_con, gt_con) where + +-- The native EPT run gives fun the TagSig TagFun[TagTuple[TagEPT, TagDunno]]: +fun :: Int -> (# [Int], Int #) +fun x = let xs = x : xs in (# xs, x #) +{-# NOINLINE fun #-} + +-- In native code a static constructor, in bytecode an unevaluated closure. +just_con :: Maybe Int +just_con = Just 42 +{-# NOINLINE just_con #-} + +-- The same for a nullary constructor. Without its pointer tag, the object code +-- in T27842N would take the LT alternative, so GT shows the difference. +gt_con :: Ordering +gt_con = GT +{-# NOINLINE gt_con #-} ===================================== testsuite/tests/bytecode/T27842N.hs ===================================== @@ -0,0 +1,26 @@ +{-# OPTIONS_GHC -fno-byte-code-and-object-code #-} +-- We compile this module as native code, depending on A's interface file. +-- A itself is loaded into GHCi, despite it's interface file being generated based +-- on native code generation. +module T27842N (S(..), use_S, M(..), use_M, N(..), use_N) where + +data S = S ![Int] + +-- We take apart the strict constructor value and branch on the value in its field. +-- If the field content is not EPT this causes undefined behaviour. + +use_S :: S -> Int +use_S (S xs) = case xs of { (y:_) -> y; [] -> -1 } +{-# NOINLINE use_S #-} + +data M = M !(Maybe Int) + +use_M :: M -> Int +use_M (M m) = case m of { Just x -> x; Nothing -> -1 } +{-# NOINLINE use_M #-} + +data N = N !Ordering + +use_N :: N -> Int +use_N (N o) = case o of { LT -> 1; EQ -> 2; GT -> 3 } +{-# NOINLINE use_N #-} ===================================== testsuite/tests/bytecode/all.T ===================================== @@ -17,3 +17,12 @@ test('T26216', extra_files(["T26216_aux.hs"]), ghci_script, ['T26216.script']) test('T27001', [extra_files(['T27001.hs']), req_interp], run_command, ['{compiler} -e main -O -fno-unoptimized-core-for-interpreter T27001.hs']) + +# Bytecode must not trust tag information from imported interfaces, which +# comes from native code (#27842): neither the TagSig of an imported function +# nor the LFInfo of an imported value (with and without constructor fields). +test('T27842', [extra_files(['T27842A.hs', 'T27842N.hs']), req_interp], + run_command, + ['{compiler} -e main -O -fno-unoptimized-core-for-interpreter ' + '-fobject-code -fbyte-code-and-object-code -fwrite-byte-code -fprefer-byte-code ' + 'T27842.hs']) ===================================== testsuite/tests/simplStg/should_compile/all.T ===================================== @@ -25,5 +25,17 @@ test('inferTags003', [ only_ways(['optasm']), ], compile, ['-ddump-cmm -dno-typeable-binds -O']) test('inferTags004', normal, compile, ['-O -ddump-stg-tags -dno-typeable-binds -dsuppress-uniques']) test('T27005b', normal, compile, ['-O -ddump-stg-tags -dno-typeable-binds -dsuppress-uniques']) +# Both f and the join point j should have a signature TagTuple[TagEPT, TagEPT] +test('inferTags005', + grep_errmsg(r'(TagTuple\[TagEPT, TagEPT\])', [1]), + compile, + ['-O -fno-worker-wrapper -fno-cpr-anal -ddump-stg-tags ' + '-dno-typeable-binds -dsuppress-uniques']) +# The function needs to have a signature TagTuple[TagEPT, TagEPT] +test('inferTags006', + grep_errmsg(r'(TagTuple\[TagEPT, TagEPT\])', [1]), + compile, + ['-O -fno-worker-wrapper -fno-cpr-anal -fno-full-laziness -ddump-stg-tags ' + '-dno-typeable-binds -dsuppress-uniques']) test('T24806', grep_errmsg('^\\(T24806\\.\\$wgo'), compile, ['-O -ddump-stg-tags -dno-typeable-binds -dsuppress-uniques']) ===================================== testsuite/tests/simplStg/should_compile/inferTags005.hs ===================================== @@ -0,0 +1,39 @@ +{-# LANGUAGE UnboxedTuples #-} +module EnforceEpt005 where + +-- If we have +-- f x y = +-- join j = +-- <rhs> -- <TagTuple[TagEPT, TagEPT]]> +-- in case x of +-- 1 -> j +-- 2 -> j +-- _ -> +-- <something> -- <TagTuple[TagEPT, TagEPT]]> + +-- Consider the case where rhs and something both represent a tag value of <TagTuple[TagEPT, TagEPT]]> +-- In this case we want `f` to also give rise to TagFun [TagTuple[TagEPT, TagEPT]]] + +-- To achieve this we have to recognize j as a zero-arity function equivalent +-- which is what this test checks. + +-- The payoff is in `g` `r` is then known to be tagged, so `S r` needs no eval. +-- Only an unboxed tuple result exposes this. + +-- We disable worker/wrapper and CPR so `f` matches more closely the tests source. + +data T = A Int Int Int Int Int Int | B + +f :: Int -> Int -> (# T, T #) +f x y = case x of + 0 -> j + 1 -> j + _ -> (# B, B #) + where + j = (# A (y+1) (y*2) (y-3) (y*y) (y+x) (y*x), B #) +{-# NOINLINE f #-} + +data S = S !T + +g :: Int -> Int -> S +g x y = case f x y of (# r, _ #) -> S r ===================================== testsuite/tests/simplStg/should_compile/inferTags005.stderr ===================================== @@ -0,0 +1,2 @@ +TagTuple[TagEPT, TagEPT] +TagTuple[TagEPT, TagEPT] ===================================== testsuite/tests/simplStg/should_compile/inferTags006.hs ===================================== @@ -0,0 +1,31 @@ +{-# LANGUAGE UnboxedTuples #-} +module EnforceEpt006 where + +-- If we have +-- f x y = +-- join j = +-- <rhs> -- TagBottoming +-- in case x of +-- 1 -> j +-- 2 -> j +-- _ -> +-- <something> -- <TagTuple[TagEPT, TagEPT]]> + +-- Similar to inferTage005 we want to give `f` the signature: TagFun <TagTuple[TagEPT, TagEPT]]> +-- This requires us to give `j` a `TagFun[TagBottoming]` signature, which is safe because +-- either its execution will diverge, or the resulting tuple *will* have two +-- tagged values. + +data T = A Int Int Int Int Int Int | B + +f :: Int -> Int -> (# T, T #) +-- This case-of-case is just here to be optimized into a nullary join point. +f x y = case (case x of { 0 -> False; 1 -> False; _ -> True }) of + False -> error ("f: bad input " ++ show x ++ " " ++ show y ++ " " ++ show (x*y)) + True -> (# A (y+1) (y*2) (y-3) (y*y) (y+x) (y*x), B #) +{-# NOINLINE f #-} + +data S = S !T + +g :: Int -> Int -> S +g x y = case f x y of (# r, _ #) -> S r ===================================== testsuite/tests/simplStg/should_compile/inferTags006.stderr ===================================== @@ -0,0 +1 @@ +TagTuple[TagEPT, TagEPT] ===================================== testsuite/tests/simplStg/should_run/InferTags007_A.hs ===================================== @@ -0,0 +1,20 @@ +-- We suppress arity and LfInfo with the option. +{-# OPTIONS_GHC -fomit-interface-pragmas #-} +module InferTags007_A (fun, caf, bot, con) where + +fun :: Int -> Int +fun x = x + 1 +{-# NOINLINE fun #-} + +-- A CAF/thunk +caf :: [Int] +caf = map (* 2) [1 .. 10] +{-# NOINLINE caf #-} + +bot :: Int -> Int +bot _ = error "bot called" +{-# NOINLINE bot #-} + +con :: Maybe Int +con = Just 42 +{-# NOINLINE con #-} ===================================== testsuite/tests/simplStg/should_run/T27831.hs ===================================== @@ -0,0 +1,35 @@ +-- Regression test for #27831: a bottoming function stored in a strict +-- constructor field. +-- +-- Different parts of the tag inference machinery didn't agree on weither or not +-- a bottoming function should be treated as a EPT value, leading to a segfault. +module Main (main) where + +import Control.Exception +import GHC.Exts.Heap (GenClosure(..), getClosureData) +import System.Exit + +data T = MkT Int !(Int -> Int) + +t :: T +t = MkT 1 (\_ -> error "T27831") +{-# NOINLINE t #-} + +f :: () -> T +f _ = t +{-# OPAQUE f #-} + +main :: IO () +main = do + c <- getClosureData t + case c of + ThunkClosure{} -> putStrLn "FAIL: ThunkClosure" >> exitFailure + APClosure{} -> putStrLn "FAIL: APClosure" >> exitFailure + _ -> putStrLn "OK: not a thunk" + + case f () of MkT n _ -> print n + + r <- try (evaluate (case t of MkT _ g -> g 1)) + case r of + Left (ErrorCall msg) -> putStrLn ("OK: " ++ msg) + Right v -> putStrLn ("FAIL: got " ++ show v) >> exitFailure ===================================== testsuite/tests/simplStg/should_run/T27831.stdout ===================================== @@ -0,0 +1,3 @@ +OK: not a thunk +1 +OK: T27831 ===================================== testsuite/tests/simplStg/should_run/T27857.hs ===================================== @@ -0,0 +1,45 @@ +{-# LANGUAGE StrictData #-} +-- Regression test from #27857: We store a function that loops indefinitely +-- in a strict field. +module Main (main) where +import Control.Monad + +data Body + = BNone + | BStream ((Int -> IO ()) -> IO () -> IO ()) + | BIface (Int -> IO ()) + | BBuilder String + | BFile Int + +data Obj = Obj [String] Body Int + +newtype Resp = Resp Obj + +stream :: Int -> [String] -> ((Int -> IO ()) -> IO () -> IO ()) -> Resp +stream st hdr b = Resp $ Obj (show st : hdr) (BStream b) 0 + +noBody :: Int -> [String] -> Resp +noBody st hdr = Resp $ Obj (show st : hdr) BNone 0 + +infinite :: Resp +infinite = stream 200 ["text/plain"] body + where + body :: (Int -> IO ()) -> IO () -> IO () + body write flush = do + let go n = write n *> flush *> go (succ n) + go (0 :: Int) + +other :: Resp +other = noBody 404 [] + +name :: Body -> String +name b = case b of + BNone -> "None" + BStream _ -> "Stream" + BIface _ -> "Iface" + BBuilder _ -> "Builder" + BFile _ -> "File" + +main :: IO () +main = forM_ [("infinite", infinite), ("other", other)] $ \(n, Resp (Obj _ b _)) -> + putStrLn $ n ++ "=" ++ name b ===================================== testsuite/tests/simplStg/should_run/T27857.stdout ===================================== @@ -0,0 +1,2 @@ +infinite=Stream +other=None ===================================== testsuite/tests/simplStg/should_run/all.T ===================================== @@ -3,13 +3,15 @@ # extra run flags # expected process return value, if not zero -# Only compile with optimisation +# Only run optimised code, native and interpreted: +# We now generate bytecode from STG so we should test native and bytecode. def f( name, opts ): - opts.only_ways = ['optasm'] + opts.only_ways = ['optasm', 'ghci-opt'] setTestOpts(f) -test('T9291', normal, compile_and_run, ['']) +# Breakpoint ticks would break CSE which this tests. +test('T9291', [omit_ways(['ghci']), extra_hc_opts('-fno-break-points')], compile_and_run, ['']) test('T13536', normal, compile_and_run, ['']) test('T13536a', @@ -20,6 +22,16 @@ test('T13536a', test('inferTags001', normal, multimod_compile_and_run, ['inferTags001', 'inferTags001_a']) test('T22042', [extra_files(['T22042a.hs']),only_ways('normal'),unless(have_dynamic(), skip)], makefile_test, ['T22042']) -test('T23783', normal, multimod_compile_and_run, ['T23783', '-O -v0']) -test('unpack_enum', normal, compile_and_run, ['']) -test('T27005a', normal, compile_and_run, ['']) + +# Depends on tag inference being similarly effective for bytecode which it is not yet. +test('T23783', omit_ghci, multimod_compile_and_run, ['T23783', '-O -v0']) + +# Requires UNPACK which needs -O +test('unpack_enum', omit_ways(['ghci']), compile_and_run, ['']) + +# Tests that tag inference optimizes well, which is not the case for bytecode or +# when we insert profiling ticks. +test('T27005a', omit_ways(ghci_ways + prof_ways), compile_and_run, ['']) +test('T27831', omit_ways(ghci_ways + prof_ways), compile_and_run, ['']) +test('inferTags007', [extra_files(['InferTags007_A.hs'])], multimod_compile_and_run, ['inferTags007', '-O -v0']) +test('T27857', normal, compile_and_run, ['']) ===================================== testsuite/tests/simplStg/should_run/inferTags007.hs ===================================== @@ -0,0 +1,109 @@ +{-# LANGUAGE MagicHash #-} +-- This test sanity checks the tag info we generate for imported binders which +-- have no real info in the .hi file. +-- +-- This is important to avoid running into cases where we optimistically +-- generated better information based on things like type than the +-- compiled code actually provided. For example GHCi doesn't ensure tagging +-- of constructors. +module Main (main) where + +import Control.Exception +import Control.Monad +import GHC.Exts (Addr#) +import GHC.Exts.Heap (GenClosure(..), getClosureData) +import GHC.Internal.Control.Exception.Base (patError) +import System.Exit + +import qualified InferTags007_A as A + +data S a = S !a + +data P = MkP !(Addr# -> Int) + +-- Put the imported values into a strict field of a top level Con +con_top_fun :: S (Int -> Int) +con_top_fun = S A.fun +{-# NOINLINE con_top_fun #-} + +con_top_caf :: S [Int] +con_top_caf = S A.caf +{-# NOINLINE con_top_caf #-} + +con_top_bot :: S (Int -> Int) +con_top_bot = S A.bot +{-# NOINLINE con_top_bot #-} + +con_top_con :: S (Maybe Int) +con_top_con = S A.con +{-# NOINLINE con_top_con #-} + +con_top_pat :: P +con_top_pat = MkP patError +{-# NOINLINE con_top_pat #-} + +-- Put the imported values into a strict field of a Con inside a rhs +expr_fun :: () -> S (Int -> Int) +expr_fun _ = S A.fun +{-# OPAQUE expr_fun #-} + +expr_caf :: () -> S [Int] +expr_caf _ = S A.caf +{-# OPAQUE expr_caf #-} + +expr_bot :: () -> S (Int -> Int) +expr_bot _ = S A.bot +{-# OPAQUE expr_bot #-} + +expr_con :: () -> S (Maybe Int) +expr_con _ = S A.con +{-# OPAQUE expr_con #-} + +-- Actually use the field. +use_S_head :: S [Int] -> Int +use_S_head (S xs) = case xs of { (y:_) -> y; [] -> -1 } +{-# NOINLINE use_S_head #-} + +use_S_fromJust :: S (Maybe Int) -> Int +use_S_fromJust (S m) = case m of { Just x -> x; Nothing -> -1 } +{-# NOINLINE use_S_fromJust #-} + +use_S_apply :: S (Int -> Int) -> Int +use_S_apply (S f) = f 1 +{-# NOINLINE use_S_apply #-} + +checkNotThunk :: String -> a -> IO () +checkNotThunk name x = do + c <- getClosureData x + case c of + ThunkClosure{} -> putStrLn ("FAIL: " ++ name ++ " is a thunk") >> exitFailure + APClosure{} -> putStrLn ("FAIL: " ++ name ++ " is an AP") >> exitFailure + _ -> pure () + +-- Pattern matching binds the field itself, so no selector thunk is involved. +checkField :: String -> S a -> IO () +checkField name (S x) = checkNotThunk name x +{-# NOINLINE checkField #-} + +main :: IO () +main = do + -- Check if the pointer in the strict field is a thunk. + checkField "con_top_caf" con_top_caf + checkField "con_top_fun" con_top_fun + checkField "con_top_bot" con_top_bot + checkField "con_top_con" con_top_con + case con_top_pat of MkP f -> checkNotThunk "con_top_pat" f + checkField "expr_caf" (expr_caf ()) + checkField "expr_fun" (expr_fun ()) + checkField "expr_bot" (expr_bot ()) + checkField "expr_con" (expr_con ()) + + -- Actually execute a case on the contents of the field. + print (use_S_head con_top_caf, use_S_head (expr_caf ())) + print (use_S_fromJust con_top_con, use_S_fromJust (expr_con ())) + print (use_S_apply con_top_fun, use_S_apply (expr_fun ())) + forM_ [con_top_bot, expr_bot ()] $ \s -> do + r <- try (evaluate (use_S_apply s)) + case r of + Left (ErrorCall msg) -> putStrLn ("OK: " ++ msg) + Right v -> putStrLn ("FAIL: got " ++ show v) >> exitFailure ===================================== testsuite/tests/simplStg/should_run/inferTags007.stdout ===================================== @@ -0,0 +1,5 @@ +(2,2) +(42,42) +(2,2) +OK: bot called +OK: bot called View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/4422280758a803eebf97e8ffc62a9d8… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/4422280758a803eebf97e8ffc62a9d8… 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/T27828] Refactor fundeps again
by Simon Peyton Jones (＠simonpj) 26 Sep '26

26 Sep '26

Simon Peyton Jones pushed to branch wip/T27828 at Glasgow Haskell Compiler / GHC Commits: cac84324 by Simon Peyton Jones at 2026-09-26T12:27:34+01:00 Refactor fundeps again This MR fixes #27828; there was a bad scoping error in `trim_qtvs`. The main changes are * Refactor `trim_qtvs` completely to eliminate the bug. * Remove a redundant `apartnessCheck` from `mkTopOpenFamEqFDs`. * Lots of improvements to the Notes in FunDeps.hs I also did a couple of pure refactors: * I realised that we were carefully caching `cab_incomps` in each `CoAxBranch`, to make it more efficient to reduce a type family application, but we were not doing the same thing when computing relevance for functional dependencies; see Note [Relevance] in GHC.Tc.Solver.FunDeps. So I added `cab_overlaps`, which is now used in `noEarlierMatch`. * Use a proper data types, `AmIUnifying` and `OuterKindsFlag`, for two previously-Boolean arguments to `tc_unify_tys`. This is a pure refactor. - - - - - 15 changed files: - + changelog.d/T27828 - compiler/GHC/Builtin/WiredIn/Types/Box.hs - compiler/GHC/Core/Coercion/Axiom.hs - compiler/GHC/Core/FamInstEnv.hs - compiler/GHC/Core/Unify.hs - compiler/GHC/Iface/Decl.hs - compiler/GHC/Iface/Syntax.hs - compiler/GHC/IfaceToCore.hs - compiler/GHC/Tc/Instance/FunDeps.hs - compiler/GHC/Tc/Solver/FunDeps.hs - compiler/GHC/Tc/TyCl.hs - + testsuite/tests/indexed-types/should_compile/T27828.hs - + testsuite/tests/indexed-types/should_compile/T27828a.hs - + testsuite/tests/indexed-types/should_compile/T27828b.hs - testsuite/tests/indexed-types/should_compile/all.T Changes: ===================================== changelog.d/T27828 ===================================== @@ -0,0 +1,8 @@ +section: compiler +synopsis: Fix a "No skolem info" compiler crash +issues: #27828 +mrs: !16714 + +description: { + There was a bug in the implementation of functional dependencies for type families. +} ===================================== compiler/GHC/Builtin/WiredIn/Types/Box.hs ===================================== @@ -329,7 +329,8 @@ mkWiredInNewTyCon tc_name dc_name nt_co_uniq bndrs roles nt_fld_ty = , cab_roles = roles , cab_lhs = mkTyVarTys tvs , cab_rhs = nt_fld_ty - , cab_incomps = [] } + , cab_overlaps = [] + , cab_incomps = [] } -- | The wired-in @Box@ newtype: -- ===================================== compiler/GHC/Core/Coercion/Axiom.hs ===================================== @@ -18,7 +18,7 @@ module GHC.Core.Coercion.Axiom ( coAxiomSingleBranch, coAxBranchTyVars, coAxBranchCoVars, coAxBranchRoles, coAxBranchLHS, coAxBranchRHS, coAxBranchSpan, coAxBranchIncomps, - placeHolderIncomps, + placeHolderIncomps, placeHolderOverlaps, Role(..), @@ -195,23 +195,44 @@ mapAccumBranches f (MkBranches arr) Note [Storing compatibility] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -During axiom application, we need to be aware of which branches are compatible -with which others. The full explanation is in Note [Compatibility] in -GHc.Core.FamInstEnv. (The code is placed there to avoid a dependency from -GHC.Core.Coercion.Axiom on the unification algorithm.) Although we could -theoretically compute compatibility on the fly, this is silly, so we store it -in a CoAxiom. +A `CoAxBranch` caches some useful information in `cab_incomps` and `cab_overlaps`: -Specifically, each branch refers to all other branches with which it is -incompatible. This list might well be empty, and it will always be for the -first branch of any axiom. +* `cab_overlaps`: when computing "relevance", in the function + `GHC.Tc.Solver.FunDeps.getRelevantBranches`, we need to know which ealier branches + can match this one -- see `noEarlierMatch`. -CoAxBranches that do not (yet) belong to a CoAxiom should have a panic thunk -stored in cab_incomps. The incompatibilities are properly a property of the -axiom as a whole, and they are computed only when the final axiom is built. + Again we could look at all earlier branches, but instead we cache in `cab_overlaps` + a list of all earlier branches that could overlap with this one. -During serialization, the list is converted into a list of the indices -of the branches. +* `cab_incomps`: during axiom application, we need to be aware of which branches are + /compatible/ with which others. The full explanation is in Note [Compatibility] in + GHC.Core.FamInstEnv. (The code is placed there to avoid a dependency from + GHC.Core.Coercion.Axiom on the unification algorithm.) + + Although we could readily compute compatibility on the fly, this is silly, so we + cache in `cab_incomps` a list of earlier branches that are /incompatible/ with + this one. (See Note [Compatibility] for a definition.) + + Always a sub-list of `cab_overlaps`. + +Both lists can be empty, and always be for the first branch of any axiom. + +Some extra points: + +(SC1) A `CoAxBranch` that does not (yet) belong to a CoAxiom is initialised with panic + thunks, `placeHolderOverlaps` or `placeHolderIncomps`, for the two fields; see `mkCoAxBranch`. + + Then, when a bunch of branches is grouped together in an axiom, we analyse the + branches as a whole and initialise the fields properly, using `computeAxiomIncomps`. + (For open type families, whose axioms have only one branch, we null out both lists + with `noAxiomIncomps`. + +(SC2) We don't need to serialise `cab_overlaps` and `cab_incomps` into an interface + file, because we recompute them in `computeAxiomIncomps`. However, annoyingly, + the pretty printer converts to IfaceSyn before printing, and we do want to show + `cab_incomps` (see Note [Displaying axiom incompatibilities]). So, tiresomely, + `IfaceAxBranch` has a `ifaxbIncomps` field, used only for printing. For historical + reasons this is actually serialised. Yuk. Note [CoAxioms are homogeneous] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -230,7 +251,9 @@ This is checked in FamInstEnv.mkCoAxBranch. -- If you edit this type, you may need to update the GHC formalism -- See Note [GHC Formalism] in GHC.Core.Lint data CoAxiom br - = CoAxiom -- Type equality axiom. + = -- `br` is Unbranched for each of the many axioms of an open type family + -- Branched for the single multi-branch axiom of a closed type family + CoAxiom -- Type equality axiom. { co_ax_unique :: Unique -- Unique identifier , co_ax_name :: Name -- Name for pretty-printing , co_ax_role :: Role -- Role of the axiom's equality @@ -268,8 +291,15 @@ data CoAxBranch , cab_rhs :: Type -- ^ Right-hand side of the equality -- See Note [CoAxioms are homogeneous] + + , cab_overlaps :: [CoAxBranch] + -- ^ The preceding branches whose LHSs are /unify with/ this one + -- Order is unimportant + -- See Note [Storing compatibility] + , cab_incomps :: [CoAxBranch] - -- ^ The previous incompatible branches + -- ^ The preceding branches that are /incompatible/ with this one + -- Order is unimportant -- See Note [Storing compatibility] } deriving Data.Data @@ -342,8 +372,9 @@ coAxBranchIncomps :: CoAxBranch -> [CoAxBranch] coAxBranchIncomps = cab_incomps -- See Note [Compatibility] in GHC.Core.FamInstEnv -placeHolderIncomps :: [CoAxBranch] -placeHolderIncomps = panic "placeHolderIncomps" +placeHolderIncomps, placeHolderOverlaps :: [CoAxBranch] +placeHolderIncomps = panic "placeHolderIncomps" +placeHolderOverlaps = panic "placeHolderOverlaps" {- Note [CoAxBranch type variables] ===================================== compiler/GHC/Core/FamInstEnv.hs ===================================== @@ -19,7 +19,7 @@ module GHC.Core.FamInstEnv ( FamInstMatch(..), lookupFamInstEnv, lookupFamInstEnvConflicts, lookupFamInstEnvByTyCon, - isDominatedBy, apartnessCheck, compatibleBranches, + isDominatedBy, apartnessCheck, noEarlierMatchCheck, compatibleBranches, -- Injectivity InjectivityCheckResult(..), @@ -487,20 +487,45 @@ in GHC.Core.Unify.) Note [Compatibility] ~~~~~~~~~~~~~~~~~~~~ -Two patterns are /compatible/ if either of the following conditions hold: -1) The patterns are apart. -2) The patterns unify with a substitution S, and their right hand sides -equal under that substitution. +Consider a closed type family with two equations (X1) and (X2) + type family F a where + F lhs1 = rhs1 -- (X1) + ... + F lhs2 = rhs2 -- (X2) + ... +Then equations (X1) and (X2) are /compatible/ if any target (F ty) that +matches both equations yields the very same right hand side. Example: + And True True = True + And a True = a +The target (And True True) matches both equations but they then both +produce the same reduct True. + +More precisely (X1) and (X2) are /compatible/ iff + If LHSs unify with a substitution S, then S(rhs1) = S(rhs2) + +Conversely, (X1) and (X2) are /incompatible/ if + Their LHSs unify with S, and S(rhs1) /= S(rhs2) For open type families, only compatible instances are allowed. For closed -type families, the story is slightly more complicated. Consider the following: +families, we use the Closed Family Matching Rule (see function `findBranch`): -type family F a where - F Int = Bool - F a = Int + When looking up a target (F ty) in a closed type family F, + find an equation (branch) such that: + * the LHS matches the target + * the target is apart from every previous /incompatible/ equation for F -g :: Show a => a -> F a -g x = length (show x) +We don't need to check the earlier equations that are compatible with the +matching equation, because they are either irrelevant (clause 1 of compatible) +or benign (clause 2 of compatible). + +Some examples: + + type family F a where + F Int = Bool + F a = Int + + g :: Show a => a -> F a + g x = length (show x) Should that type-check? No. We need to allow for the possibility that 'a' might be Int and therefore 'F a' should be Bool. We can simplify 'F a' to Int @@ -516,12 +541,12 @@ potentially-overlapping group is closed. As another example, consider this: -type family G x where - G Int = Bool - G a = Double + type family G x where + G Int = Bool + G a = Double -type family H y --- no instances + type family H y + -- no instances Now, we want to simplify (G (H Char)). We can't, because (H Char) might later simplify to be Int. So, (G (H Char)) is stuck, for now. @@ -529,18 +554,13 @@ simplify to be Int. So, (G (H Char)) is stuck, for now. While everything above is quite sound, it isn't as expressive as we'd like. Consider this: -type family J a where - J Int = Int - J a = a + type family J a where + J Int = Int + J a = a Can we simplify (J b) to b? Sure we can. Yes, the first equation matches if b is instantiated with Int, but the RHSs coincide there, so it's all OK. - -So, the rule is this: when looking up a branch in a closed type family, we -find a branch that matches the target, but then we make sure that the target -is apart from every previous *incompatible* branch. We don't check the -branches that are compatible with the matching branch, because they are either -irrelevant (clause 1 of compatible) or benign (clause 2 of compatible). +Hence the Closed Family Matching Rule. Note [Compatibility of eta-reduced axioms] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -572,15 +592,32 @@ fails anyway. -- See Note [Compatibility] compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool -compatibleBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 }) - (CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 }) +compatibleBranches b1 b2 + = case compareBranches b1 b2 of + BC_Apart -> True + BC_Compat -> True + BC_Incompat -> False + +data BranchCompatibility + = BC_Apart -- LHSs are apart + | BC_Compat -- LHSs unify with S, and S(rhs1)=S(rhs2) + | BC_Incompat -- LHSs unify with S, and S(rhs1)/=S(rhs2) + +compareBranches :: CoAxBranch -> CoAxBranch -> BranchCompatibility +compareBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 }) + (CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 }) = case tcUnifyTysFG alwaysBindFam alwaysBindTv commonlhs1 commonlhs2 of -- Here we need the cab_tvs of the two branches to be disinct. -- See Note [CoAxBranch type variables] in GHC.Core.Coercion.Axiom. - SurelyApart -> True - MaybeApart {} -> False - Unifiable subst -> Type.substTyAddInScope subst rhs1 `eqType` + SurelyApart -> BC_Apart + Unifiable subst | Type.substTyAddInScope subst rhs1 `eqType` Type.substTyAddInScope subst rhs2 + -> BC_Compat + | otherwise + -> BC_Incompat + MaybeApart {} -> BC_Incompat + -- An occurs check yields MaybeApart; + -- see Note [Infinitary substitutions] in GHC.Core.Unify where (commonlhs1, commonlhs2) = zipAndUnzip lhs1 lhs2 -- See Note [Compatibility of eta-reduced axioms] @@ -603,8 +640,7 @@ injectiveBranches injectivity ax1@(CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 }) ax2@(CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 }) -- See Note [Verifying injectivity annotation], case 1. - = case tcUnifyTysForInjectivity True [rhs1] [rhs2] of - -- True = two-way pre-unification + = case tcUnifyTysForInjectivity Unifying [rhs1] [rhs2] of Nothing -> InjectivityAccepted -- RHS are different, so equations are injective. -- This is case 1A from Note [Verifying injectivity annotation] @@ -629,10 +665,11 @@ injectiveBranches injectivity lhs1Subst = Type.substTys subst (getInjArgs lhs1) lhs2Subst = Type.substTys subst (getInjArgs lhs2) --- takes a CoAxiom with unknown branch incompatibilities and computes --- the compatibilities --- See Note [Storing compatibility] in GHC.Core.Coercion.Axiom computeAxiomIncomps :: [CoAxBranch] -> [CoAxBranch] +-- Takes a CoAxiom for a closed type family that has place-holder +-- `cab_incomps` and `cab_overlaps` fields, and computes those fields +-- properly from the list of branches. +-- See Note [Storing compatibility] in GHC.Core.Coercion.Axiom computeAxiomIncomps branches = snd (mapAccumL go [] branches) where @@ -640,11 +677,23 @@ computeAxiomIncomps branches go prev_brs cur_br = (new_br : prev_brs, new_br) where - new_br = cur_br { cab_incomps = mk_incomps prev_brs cur_br } - - mk_incomps :: [CoAxBranch] -> CoAxBranch -> [CoAxBranch] - mk_incomps prev_brs cur_br - = filter (not . compatibleBranches cur_br) prev_brs + (overlaps,incomps) = get_cab [] [] prev_brs + new_br = cur_br { cab_overlaps = overlaps, cab_incomps = incomps } + + get_cab :: [CoAxBranch] -> [CoAxBranch] -- Accumulators + -> [CoAxBranch] + -> ([CoAxBranch], [CoAxBranch]) + get_cab overlaps incomps [] = (overlaps,incomps) + get_cab overlaps incomps (br:brs) + = case compareBranches cur_br br of + BC_Apart -> get_cab overlaps incomps brs + BC_Compat -> get_cab (br:overlaps) incomps brs + BC_Incompat -> get_cab (br:overlaps) (br:incomps) brs + +noAxiomIncomps :: CoAxBranch -> CoAxBranch +-- Overwrite the placeholders for `cab_incomps` and `cab_overlaps` +-- with [], because unbranched axioms have no "preceding" equations +noAxiomIncomps branch = branch { cab_incomps = [], cab_overlaps = [] } {- ************************************************************************ @@ -715,14 +764,17 @@ mkCoAxBranch :: [TyVar] -- original, possibly stale, tyvars -> SrcSpan -> CoAxBranch mkCoAxBranch tvs eta_tvs cvs lhs rhs roles loc - = CoAxBranch { cab_tvs = tvs' - , cab_eta_tvs = eta_tvs' - , cab_cvs = cvs' - , cab_lhs = tidyTypes env lhs - , cab_roles = roles - , cab_rhs = tidyType env rhs - , cab_loc = loc - , cab_incomps = placeHolderIncomps } + = CoAxBranch { cab_tvs = tvs' + , cab_eta_tvs = eta_tvs' + , cab_cvs = cvs' + , cab_lhs = tidyTypes env lhs + , cab_roles = roles + , cab_rhs = tidyType env rhs + , cab_loc = loc + + -- See (SC1) in Note [Storing compatibility] + , cab_overlaps = placeHolderOverlaps + , cab_incomps = placeHolderIncomps } where (env1, tvs') = tidyVarBndrs init_tidy_env tvs (env2, eta_tvs') = tidyVarBndrs env1 eta_tvs @@ -736,14 +788,16 @@ mkCoAxBranch tvs eta_tvs cvs lhs rhs roles loc -- all of the following code is here to avoid mutual dependencies with -- Coercion -mkBranchedCoAxiom :: Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched -mkBranchedCoAxiom ax_name fam_tc branches +mkBranchedCoAxiom :: Role -> Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched +mkBranchedCoAxiom role ax_name fam_tc branches = CoAxiom { co_ax_unique = nameUnique ax_name , co_ax_name = ax_name , co_ax_tc = fam_tc - , co_ax_role = Nominal + , co_ax_role = role , co_ax_implicit = False , co_ax_branches = manyBranches (computeAxiomIncomps branches) } + -- computeAxiomIncomps: see (SC1) in + -- Note [Storing compatibility] mkUnbranchedCoAxiom :: Name -> TyCon -> CoAxBranch -> CoAxiom Unbranched mkUnbranchedCoAxiom ax_name fam_tc branch @@ -752,7 +806,9 @@ mkUnbranchedCoAxiom ax_name fam_tc branch , co_ax_tc = fam_tc , co_ax_role = Nominal , co_ax_implicit = False - , co_ax_branches = unbranched (branch { cab_incomps = [] }) } + , co_ax_branches = unbranched (noAxiomIncomps branch) } + -- noAxiomIncomps: see (SC1) in + -- Note [Storing compatibility] mkSingleCoAxiom :: Role -> Name -> [TyVar] -> [TyVar] -> [CoVar] @@ -767,7 +823,9 @@ mkSingleCoAxiom role ax_name tvs eta_tvs cvs fam_tc lhs_tys rhs_ty , co_ax_tc = fam_tc , co_ax_role = role , co_ax_implicit = False - , co_ax_branches = unbranched (branch { cab_incomps = [] }) } + , co_ax_branches = unbranched (noAxiomIncomps branch) } + -- noAxiomIncomps: see (SC1) in + -- Note [Storing compatibility] where branch = mkCoAxBranch tvs eta_tvs cvs lhs_tys rhs_ty (map (const Nominal) tvs) @@ -785,7 +843,9 @@ mkNewTypeCoAxiom name tycon tvs roles rhs_ty , co_ax_implicit = True -- See Note [Implicit axioms] in GHC.Core.TyCon , co_ax_role = Representational , co_ax_tc = tycon - , co_ax_branches = unbranched (branch { cab_incomps = [] }) } + , co_ax_branches = unbranched (noAxiomIncomps branch) } + -- noAxiomIncomps: see (SC1) in + -- Note [Storing compatibility] where branch = mkCoAxBranch tvs [] [] (mkTyVarTys tvs) rhs_ty roles (getSrcSpan name) @@ -1223,7 +1283,9 @@ findBranch :: Array BranchIndex CoAxBranch -> Maybe (BranchIndex, [Type], [Coercion]) -- coercions relate requested types to returned axiom LHS at role N findBranch branches target_tys - = foldr go Nothing (assocs branches) + = -- Implements the Closed Family Matching Rule + -- in Note [Compatibility] + foldr go Nothing (assocs branches) where go :: (BranchIndex, CoAxBranch) -> Maybe (BranchIndex, [Type], [Coercion]) @@ -1258,6 +1320,20 @@ apartnessCheck target (CoAxBranch { cab_incomps = incomps }) isSurelyApart SurelyApart = True isSurelyApart _ = False +-- | Check whether an earlier branch matches these target types +noEarlierMatchCheck + :: [Type] + -> CoAxBranch -- ^ The candidate equation we wish to use + -> Bool -- ^ True <=> equation can fire +noEarlierMatchCheck target (CoAxBranch { cab_overlaps = overlaps }) + -- NB: this is the /only/ use of the `cab_overlaps` field + -- See Note [Storing compatibility] and + -- (RW4) in Note [Relevance] + = not (any matches overlaps) + where + matches earlier_branch + = isJust (tcMatchTys (coAxBranchLHS earlier_branch) target) + {- ************************************************************************ * * ===================================== compiler/GHC/Core/Unify.hs ===================================== @@ -9,6 +9,7 @@ module GHC.Core.Unify ( tcMatchTyX_BM, ruleMatchTyKiX, -- Side-effect free unification + AmIUnifying(..), tcUnifyTy, tcUnifyTys, tcUnifyFunDeps, tcUnifyDebugger, tcUnifyTysFG, tcUnifyTysForInjectivity, BindTvFun, BindFamFun, BindFlag(..), @@ -597,14 +598,14 @@ tcMatchTyX_BM :: HasDebugCallStack => BindTvFun -> Subst -> Type -> Type -> Maybe Subst tcMatchTyX_BM bind_tv subst ty1 ty2 - = tc_match_tys_x bind_tv False subst [ty1] [ty2] + = tc_match_tys_x bind_tv IgnoreOuterKinds subst [ty1] [ty2] -- | Like 'tcMatchTy', but allows the kinds of the types to differ, -- and thus matches them as well. -- See also Note [tcMatchTy vs tcMatchTyKi] tcMatchTyKi :: HasDebugCallStack => Type -> Type -> Maybe Subst tcMatchTyKi ty1 ty2 - = tc_match_tys alwaysBindTv True [ty1] [ty2] + = tc_match_tys alwaysBindTv CheckOuterKinds [ty1] [ty2] -- | This is similar to 'tcMatchTy', but extends a substitution -- See also Note [tcMatchTy vs tcMatchTyKi] @@ -614,7 +615,7 @@ tcMatchTyX :: HasDebugCallStack -> Type -- ^ Target -> Maybe Subst tcMatchTyX subst ty1 ty2 - = tc_match_tys_x alwaysBindTv False subst [ty1] [ty2] + = tc_match_tys_x alwaysBindTv IgnoreOuterKinds subst [ty1] [ty2] -- | Like 'tcMatchTy' but over a list of types. -- See also Note [tcMatchTy vs tcMatchTyKi] @@ -625,7 +626,7 @@ tcMatchTys :: HasDebugCallStack -- variables could be free in the target -- See (CU6) in Note [The Core unifier] tcMatchTys tys1 tys2 - = tc_match_tys alwaysBindTv False tys1 tys2 + = tc_match_tys alwaysBindTv IgnoreOuterKinds tys1 tys2 -- | Like 'tcMatchTyKi' but over a list of types. -- See also Note [tcMatchTy vs tcMatchTyKi] @@ -635,7 +636,7 @@ tcMatchTyKis :: HasDebugCallStack -> Maybe Subst -- ^ One-shot substitution -- See (CU6) in Note [The Core unifier] tcMatchTyKis tys1 tys2 - = tc_match_tys alwaysBindTv True tys1 tys2 + = tc_match_tys alwaysBindTv CheckOuterKinds tys1 tys2 -- | Like 'tcMatchTys', but extending a substitution -- See also Note [tcMatchTy vs tcMatchTyKi] @@ -645,7 +646,7 @@ tcMatchTysX :: HasDebugCallStack -> [Type] -- ^ Target -> Maybe Subst -- ^ One-shot substitution tcMatchTysX subst tys1 tys2 - = tc_match_tys_x alwaysBindTv False subst tys1 tys2 + = tc_match_tys_x alwaysBindTv IgnoreOuterKinds subst tys1 tys2 -- | Like 'tcMatchTyKis', but extending a substitution -- See also Note [tcMatchTy vs tcMatchTyKi] @@ -655,12 +656,12 @@ tcMatchTyKisX :: HasDebugCallStack -> [Type] -- ^ Target -> Maybe Subst -- ^ One-shot substitution tcMatchTyKisX subst tys1 tys2 - = tc_match_tys_x alwaysBindTv True subst tys1 tys2 + = tc_match_tys_x alwaysBindTv CheckOuterKinds subst tys1 tys2 -- | Same as tc_match_tys_x, but starts with an empty substitution tc_match_tys :: HasDebugCallStack => BindTvFun - -> Bool -- ^ match kinds? + -> OuterKindsFlag -- ^ Match kinds? -> [Type] -> [Type] -> Maybe Subst @@ -672,7 +673,7 @@ tc_match_tys bind_me match_kis tys1 tys2 -- | Worker for 'tcMatchTysX' and 'tcMatchTyKisX' tc_match_tys_x :: HasDebugCallStack => BindTvFun - -> Bool -- ^ match kinds? + -> OuterKindsFlag -- ^ Match kinds? -> Subst -> [Type] -> [Type] @@ -680,8 +681,8 @@ tc_match_tys_x :: HasDebugCallStack tc_match_tys_x bind_tv match_kis (Subst in_scope id_env tv_env cv_env) tys1 tys2 = case tc_unify_tys neverBindFam -- (ATF7) in Note [Apartness and type families] bind_tv - False -- Matching, not unifying - False -- Not an injectivity check + Matching -- Matching, not unifying + False -- Not an injectivity check match_kis RespectMultiplicities (mkRnEnv2 in_scope) tv_env cv_env tys1 tys2 of @@ -706,9 +707,9 @@ ruleMatchTyKiX tmpl_tvs rn_env tenv tmpl target -- But even if it did, (ATF8) in Note [Apartness and type families] -- says it doesn't matter becuase here we only care about Unifiable. -- So neverBindFam is efficient, and sufficient. - False -- Matching, not unifying + Matching -- Matching, not unifying False -- No doing an injectivity check - True -- Match the kinds + CheckOuterKinds -- Match the kinds IgnoreMultiplicities -- See Note [Rewrite rules ignore multiplicities in FunTy] rn_env tenv emptyCvSubstEnv [tmpl] [target] of @@ -784,7 +785,7 @@ tcUnifyTy t1 t2 = tcUnifyTys alwaysBindTv [t1] [t2] tcUnifyDebugger :: Type -> Type -> Maybe Subst tcUnifyDebugger t1 t2 = case tc_unify_tys_fg - True -- Unify kinds + CheckOuterKinds -- Unify kinds neverBindFam -- Does not affect Unifiable, so pick max efficient -- See (ATF8) in Note [Apartness and type families] alwaysBindTv @@ -798,7 +799,7 @@ tcUnifyFunDeps :: TyCoVarSet -> Maybe Subst tcUnifyFunDeps qtvs tys1 tys2 = case tc_unify_tys_fg - True -- Unify kinds + CheckOuterKinds -- Unify kinds dontCareBindFam -- Class-instance heads never mention type families (matchBindTv qtvs) tys1 tys2 of @@ -821,7 +822,7 @@ tcUnifyTysForInjectivity unif tys1 tys2 = case tc_unify_tys alwaysBindFam alwaysBindTv unif -- Am I unifying? True -- Do injectivity checks - False -- Don't check outermost kinds + IgnoreOuterKinds -- Don't check outermost kinds RespectMultiplicities rn_env emptyTvSubstEnv emptyCvSubstEnv tys1 tys2 of @@ -838,8 +839,9 @@ tcUnifyTysForInjectivity unif tys1 tys2 -- should never actually be done maybe_fix tv_subst - | unif = niFixSubst in_scope tv_subst - | otherwise = mkTvSubst in_scope tv_subst + = case unif of + Unifying -> niFixSubst in_scope tv_subst + Matching -> mkTvSubst in_scope tv_subst -- When matching, don't confuse domain with range; no fixpoint! ----------------- @@ -866,15 +868,15 @@ tcUnifyTysFG :: BindFamFun -> BindTvFun -> [Type] -> [Type] -> UnifyResult tcUnifyTysFG bind_fam bind_tv tys1 tys2 - = tc_unify_tys_fg False bind_fam bind_tv tys1 tys2 + = tc_unify_tys_fg IgnoreOuterKinds bind_fam bind_tv tys1 tys2 -tc_unify_tys_fg :: Bool +tc_unify_tys_fg :: OuterKindsFlag -> BindFamFun -> BindTvFun -> [Type] -> [Type] -> UnifyResult tc_unify_tys_fg match_kis bind_fam bind_tv tys1 tys2 = do { (tv_env, _) <- tc_unify_tys bind_fam bind_tv - True -- Unifying + Unifying False -- Not doing an injectivity check match_kis -- Match outer kinds RespectMultiplicities rn_env @@ -888,10 +890,10 @@ tc_unify_tys_fg match_kis bind_fam bind_tv tys1 tys2 -- | This function is actually the one to call the unifier -- a little -- too general for outside clients, though. tc_unify_tys :: BindFamFun -> BindTvFun - -> AmIUnifying -- ^ True <=> unify; False <=> match - -> Bool -- ^ True <=> doing an injectivity check - -> Bool -- ^ True <=> treat the kinds as well - -> MultiplicityFlag -- ^ see Note [Rewrite rules ignore multiplicities in FunTy] in GHC.Core.Unify + -> AmIUnifying -- ^ Unifying or matching + -> Bool -- ^ True <=> doing an injectivity check + -> OuterKindsFlag -- ^ Check outer kinds or not + -> MultiplicityFlag -- ^ see Note [Rewrite rules ignore multiplicities in FunTy] in GHC.Core.Unify -> RnEnv2 -> TvSubstEnv -- ^ substitution to extend -> CvSubstEnv @@ -910,8 +912,9 @@ tc_unify_tys :: BindFamFun -> BindTvFun -- See also Note [tcMatchTy vs tcMatchTyKi]. tc_unify_tys bind_fam bind_tv unif inj_check match_kis match_mults rn_env tv_env cv_env tys1 tys2 = initUM tv_env cv_env $ - do { when match_kis $ - unify_tys env kis1 kis2 + do { case match_kis of + CheckOuterKinds -> unify_tys env kis1 kis2 + IgnoreOuterKinds -> return () ; unify_tys env tys1 tys2 } where env = UMEnv { um_bind_tv_fun = bind_tv @@ -926,6 +929,11 @@ tc_unify_tys bind_fam bind_tv unif inj_check match_kis match_mults rn_env tv_env kis2 = map typeKind tys2 +data OuterKindsFlag + = CheckOuterKinds -- Unify or match the /kind/ of the two types + | IgnoreOuterKinds -- Just unify of match the types, ignoring kinds + -- (typically, we already know they are equal) + {- ********************************************************************* * * UnifyResult, MaybeApart etc @@ -1583,8 +1591,7 @@ c.f. Note [Comparing type synonyms] in GHC.Core.TyCo.Compare -------------- unify_ty: the main workhorse ----------- -type AmIUnifying = Bool -- True <=> Unifying - -- False <=> Matching +data AmIUnifying = Matching | Unifying type InType = Type -- Before applying the RnEnv2 type OutCoercion = Coercion -- After applying the RnEnv2 @@ -1618,7 +1625,7 @@ unify_ty env (CastTy ty1 co1) ty2 kco -- See (KCU1) in Note [Kind coercions in Unify] = maybeApart MARCast -- See (KCU2) - | um_unif env + | Unifying <- um_unif env = unify_ty env ty1 ty2 (co1 `mkTransCo` kco) | otherwise -- We are matching, not unifying @@ -1661,7 +1668,7 @@ unify_ty env (CoercionTy co1) (CoercionTy co2) kco = do { c_subst <- getCvSubstEnv ; case co1 of CoVarCo cv - | not (um_unif env) + | Matching <- um_unif env , not (cv `elemVarEnv` c_subst) -- Not forall-bound , let (_mult_co, co_l, co_r) = decomposeFunCo kco -- Because the coercion is used in a type, it should be safe to @@ -1682,7 +1689,7 @@ unify_ty env (TyVarTy tv1) ty2 kco = uVarOrFam env (TyVarLHS tv1) ty2 kco unify_ty env ty1 (TyVarTy tv2) kco - | um_unif env -- If unifying, can swap args; but not when matching + | Unifying <- um_unif env -- If unifying, can swap args; but not when matching = uVarOrFam (umSwapRn env) (TyVarLHS tv2) ty1 (mkSymCo kco) -- Deal with TyConApps @@ -1692,7 +1699,7 @@ unify_ty env ty1 ty2 kco | Just (tc,tys) <- mb_sat_fam_app1 = uVarOrFam env (TyFamLHS tc tys) ty2 kco - | um_unif env + | Unifying <- um_unif env , Just (tc,tys) <- mb_sat_fam_app2 = uVarOrFam (umSwapRn env) (TyFamLHS tc tys) ty1 (mkSymCo kco) @@ -1820,7 +1827,7 @@ uVarOrFam env ty1 ty2 kco go swapped substs lhs@(TyVarLHS tv1) ty2 kco | Just ty1' <- lookupVarEnv (um_tv_env substs) tv1' = -- We already have a substitution for tv1 - if | um_unif env -> unify_ty env ty1' ty2 kco + if | Unifying <- um_unif env -> unify_ty env ty1' ty2 kco | (ty1' `mkCastTy` kco) `tcEqType` ty2 -> return () | otherwise -> surelyApart -- Unifying: recurse into unify_ty @@ -1842,9 +1849,9 @@ uVarOrFam env ty1 ty2 kco | TyVarTy tv2 <- ty2 , let tv2' = umRnOccR env tv2 , tv1' == tv2' - = if | um_unif env -> return () - | tv1_is_bindable -> extendTvEnv tv1' ty2 - | otherwise -> return () + = if | Unifying <- um_unif env -> return () + | tv1_is_bindable -> extendTvEnv tv1' ty2 + | otherwise -> return () | tv1_is_bindable , not (mentionsForAllBoundTyVarsR env ty2_fvs) @@ -1858,9 +1865,9 @@ uVarOrFam env ty1 ty2 kco -- e.g. a ~ F p q with `a` not bindable: we might succeed with go_fam -- e.g. a ~ beta with `a` not bindable: we might be able to bind `beta` -- e.g. beta ~ F beta Int occurs check; but MaybeApart after swapping - | um_unif env + | Unifying <- um_unif env , NotSwapped <- swapped -- If we have swapped already, don't do so again - , Just lhs2 <- canEqLHS_maybe ty2 + , Just lhs2 <- canEqLHS_maybe ty2 = go IsSwapped substs lhs2 (mkTyVarTy tv1) (mkSymCo kco) | occurs_check = maybeApart MARInfinite -- Occurs check @@ -1879,7 +1886,9 @@ uVarOrFam env ty1 ty2 kco | otherwise = False - occurs_check = um_unif env && uOccursCheck substs foralld_tvs lhs rhs + occurs_check = case um_unif env of + Unifying -> uOccursCheck substs foralld_tvs lhs rhs + Matching -> False -- Occurs check, only when unifying -- see Note [Infinitary substitutions] -- Make sure you include `kco` in rhs #14846 @@ -1893,7 +1902,7 @@ uVarOrFam env ty1 ty2 kco -- Hence the RnEnv2 is empty | not under_forall , Just ty1' <- lookupFamEnv (um_fam_env substs) tc1 tys1 - = if | um_unif env -> unify_ty env ty1' ty2 kco + = if | Unifying <- um_unif env -> unify_ty env ty1' ty2 kco -- Below here we are matching -- The return () case deals with: -- Template: (F a)..(F a) @@ -1930,9 +1939,9 @@ uVarOrFam env ty1 ty2 kco -- NB: a type family can appear on the template when matching -- see (ATF6) in Note [Apartness and type families] -- (Only worth doing this if we are not under a forall.) - | um_unif env + | Unifying <- um_unif env , NotSwapped <- swapped - , Just lhs2 <- canEqLHS_maybe ty2 + , Just lhs2 <- canEqLHS_maybe ty2 = go IsSwapped substs lhs2 (mkTyConApp tc1 tys1) (mkSymCo kco) | otherwise -- See (ATF5) in Note [Apartness and type families] @@ -1962,9 +1971,9 @@ uVarOrFam env ty1 ty2 kco (inj_tys2, noninj_tys2) = partitionByList inj tys2 bind_fam_if_poss - | not (um_unif env) -- Not when matching (ATF11-1) + | Matching <- um_unif env -- Not when matching (ATF11-1) = return () - | under_forall -- Not under a forall (ATF3) + | under_forall -- Not under a forall (ATF3) = return () | BindMe <- um_bind_fam_fun env tc tys1 rhs1 = unless (uOccursCheck substs emptyVarSet (TyFamLHS tc tys1) rhs1) $ ===================================== compiler/GHC/Iface/Decl.hs ===================================== @@ -112,7 +112,7 @@ coAxBranchToIfaceBranch tc lhs_s , ifaxbRoles = roles , ifaxbRHS = toIfaceType rhs , ifaxbIncomps = iface_incomps } - where + where iface_incomps = map (expectJust . flip findIndex lhs_s . eqTypes ===================================== compiler/GHC/Iface/Syntax.hs ===================================== @@ -338,7 +338,12 @@ data IfaceAxBranch = IfaceAxBranch { ifaxbTyVars :: [IfaceTvBndr] , ifaxbRoles :: [Role] , ifaxbRHS :: IfaceType , ifaxbIncomps :: [BranchIndex] } - -- See Note [Storing compatibility] in GHC.Core.Coercion.Axiom + -- We store the incompatibilities in IfaceAxBranch + -- just for (perhaps unnecessary) display purposes: + -- see Note [Displaying axiom incompatibilities] + -- When we construct a real CoAxBranch we compute cab_incomps directly + -- from the equations, ignoring the ifaxbIncomps. + -- We could consider getting rid of ifaxbIncomps altogether. data IfaceConDecls = IfAbstractTyCon -- c.f TyCon.AbstractTyCon @@ -779,14 +784,13 @@ that is what is seen by importing module with --make Note [Displaying axiom incompatibilities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -With -fprint-axiom-incomps we display which closed type family equations -are incompatible with which. This information is sometimes necessary -because GHC doesn't try equations in order: any equation can be used when -all preceding equations that are incompatible with it do not apply. - -For example, the last "a && a = a" equation in Data.Type.Bool.&& is -actually compatible with all previous equations, and can reduce at any -time. +With -fprint-axiom-incomps we display which closed type family equations are +incompatible with which (see #15546). This information is sometimes necessary +because GHC doesn't try equations in order: any equation can be used when all +preceding equations that are incompatible with it do not apply. + +For example, the last "a && a = a" equation in Data.Type.Bool.&& is actually +compatible with all previous equations, and can reduce at any time. This is displayed as: Prelude> :i Data.Type.Equality.== ===================================== compiler/GHC/IfaceToCore.hs ===================================== @@ -91,7 +91,6 @@ import GHC.Utils.Logger import GHC.Data.Bag import GHC.Data.Maybe import GHC.Data.FastString -import GHC.Data.List.SetOps import GHC.Types.Annotations import GHC.Types.SourceFile @@ -903,12 +902,7 @@ tc_iface_decl _ _ (IfaceAxiom { ifName = tc_name, ifTyCon = tc -- See #13803 ; tc_branches <- forkM (text "Axiom branches" <+> ppr tc_name) $ tc_ax_branches branches - ; let axiom = CoAxiom { co_ax_unique = nameUnique tc_name - , co_ax_name = tc_name - , co_ax_tc = tc_tycon - , co_ax_role = role - , co_ax_branches = manyBranches tc_branches - , co_ax_implicit = False } + ; let axiom = mkBranchedCoAxiom role tc_name tc_tycon tc_branches ; return (ACoAxiom axiom) } tc_iface_decl _ _ (IfacePatSyn{ ifName = name @@ -1116,15 +1110,14 @@ tc_fd (tvs1, tvs2) = do { tvs1' <- mapM tcIfaceTyVar tvs1 ; return (tvs1', tvs2') } tc_ax_branches :: [IfaceAxBranch] -> IfL [CoAxBranch] -tc_ax_branches if_branches = foldlM tc_ax_branch [] if_branches +tc_ax_branches if_branches = mapM tc_ax_branch if_branches -tc_ax_branch :: [CoAxBranch] -> IfaceAxBranch -> IfL [CoAxBranch] -tc_ax_branch prev_branches - (IfaceAxBranch { ifaxbTyVars = tv_bndrs +tc_ax_branch :: IfaceAxBranch -> IfL CoAxBranch +tc_ax_branch (IfaceAxBranch { ifaxbTyVars = tv_bndrs , ifaxbEtaTyVars = eta_tv_bndrs , ifaxbCoVars = cv_bndrs , ifaxbLHS = lhs, ifaxbRHS = rhs - , ifaxbRoles = roles, ifaxbIncomps = incomps }) + , ifaxbRoles = roles }) = bindIfaceTyConBinders_AT (map (\b -> Bndr (IfaceTvBndr b) (NamedTCB Inferred)) tv_bndrs) $ \ tvs -> -- The _AT variant is needed here; see Note [CoAxBranch type variables] in GHC.Core.Coercion.Axiom @@ -1135,15 +1128,15 @@ tc_ax_branch prev_branches ; this_mod <- getIfModule ; let loc = mkGeneralSrcSpan (fsLit "module " `appendFS` moduleNameFS (moduleName this_mod)) - br = CoAxBranch { cab_loc = loc - , cab_tvs = binderVars tvs - , cab_eta_tvs = eta_tvs - , cab_cvs = cvs - , cab_lhs = tc_lhs - , cab_roles = roles - , cab_rhs = tc_rhs - , cab_incomps = map (prev_branches `getNth`) incomps } - ; return (prev_branches ++ [br]) } + ; return (CoAxBranch { cab_loc = loc + , cab_tvs = binderVars tvs + , cab_eta_tvs = eta_tvs + , cab_cvs = cvs + , cab_lhs = tc_lhs + , cab_roles = roles + , cab_rhs = tc_rhs + , cab_overlaps = placeHolderOverlaps + , cab_incomps = placeHolderIncomps }) } tcIfaceDataCons :: Name -> TyCon -> IfaceConDecls -> IfL AlgTyConRhs tcIfaceDataCons tycon_name tycon if_cons ===================================== compiler/GHC/Tc/Instance/FunDeps.hs ===================================== @@ -136,10 +136,10 @@ data FunDepEqns -- Plural becuase fd_eqs has multiple equations -- to fresh unification vars, -- See (IMP2) in Note [Improving against instances] - , fd_eqs :: [TypeEqn] -- Make these pairs of types equal - -- Invariant: In each (Pair ty1 ty2), the fd_qtvs may be - -- free in ty1 but not in ty2. See Wrinkle (1) of - -- Note [Improving against instances] + , fd_eqs :: [TypeEqn] -- Make these pairs of types equal + -- Invariant: In each (Pair ty1 ty2), the fd_qtvs may be + -- free in ty1 but not in ty2. See Wrinkle (1) of + -- Note [Improving against instances] } instance Outputable FunDepEqns where ===================================== compiler/GHC/Tc/Solver/FunDeps.hs ===================================== @@ -26,20 +26,23 @@ import GHC.Core.Coercion import GHC.Core.TyCo.Rep( Type(..) ) import GHC.Core.Predicate( EqRel(..) ) import GHC.Core.TyCon -import GHC.Core.Unify( tcUnifyTysForInjectivity, typeListsAreApart ) +import GHC.Core.Unify( AmIUnifying(..) + , tcUnifyTysForInjectivity, typeListsAreApart ) import GHC.Core.Coercion.Axiom import GHC.Core.TyCo.Subst( elemSubst ) import GHC.Builtin.WiredIn.TypeLits( tryInteractTopFam, tryInteractInertFam ) +import GHC.Types.Var( TyVar, tyVarKind, setTyVarKind ) import GHC.Types.Var.Set +import GHC.Types.Var.Env( mkInScopeSet ) import GHC.Utils.Outputable import GHC.Utils.Panic import Control.Monad( unless ) import GHC.Data.Pair -import Data.Maybe( isNothing, isJust, mapMaybe ) +import Data.Maybe( isJust, mapMaybe ) {- Note [Overview of functional dependencies in type inference] @@ -109,7 +112,6 @@ Wrinkles from fundeps, but that would require new evidence forms, and an extension to FC, so we don't do that right now (Dec 14). - Note [FunDep and implicit parameter reactions] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Currently, our story of interacting two dictionaries (or a dictionary @@ -573,6 +575,7 @@ tryEqFunDeps work_item@(EqCt { eq_lhs = work_lhs tryFamEqFunDeps :: TcSMode -> [EqCt] -> TyCon -> [TcType] -> EqCt -> SolverStage () +-- See Note [Type inference for type families with injectivity] tryFamEqFunDeps mode eqs_for_me fam_tc work_args work_item@(EqCt { eq_ev = ev, eq_rhs = work_rhs }) | Just ops <- builtInClosedTyFamTyCon_maybe fam_tc @@ -583,6 +586,7 @@ tryFamEqFunDeps mode eqs_for_me fam_tc work_args ; tryFDEqns False fam_tc work_args work_item eqns ; unless (hasRelevantGiven eqs_for_me work_args work_item) $ + -- hasRelevantGiven: See (CF1) in Note [Exploiting closed type families] do { eqns <- mkTopBuiltinFamEqFDs fam_tc ops work_args work_rhs ; tryFDEqns True fam_tc work_args work_item eqns } } @@ -599,8 +603,11 @@ tryFamEqFunDeps mode eqs_for_me fam_tc work_args NotInjective -> nopStage () Injective inj -> do { eqns <- mkLocalFamEqFDs eqs_for_me fam_tc inj work_args work_rhs ; tryFDEqns False fam_tc work_args work_item eqns } + -- NB: tryFDEqns bales out on an insoluble fundep + -- See (CF4) in Note [Exploiting closed type families] ; unless (hasRelevantGiven eqs_for_me work_args work_item) $ + -- hasRelevantGiven: See (CF1) in Note [Exploiting closed type families] do { eqns <- mkTopFamEqFDs fam_tc work_args work_item ; tryFDEqns True fam_tc work_args work_item eqns } } @@ -638,10 +645,11 @@ tryFDEqns is_top fam_tc work_args work_item@(EqCt { eq_ev = ev, eq_rhs= rhs }) f -- User-defined type families ----------------------------------------- mkTopClosedFamEqFDs :: CoAxiom Branched -> [TcType] -> EqCt -> SolverStage [FunDepEqns] +-- Implements (INJFAM:Wanted/top-closed) +-- See Note [Exploiting closed type families] -- Look at the top-level axioms; we effectively infer injectivity, --- so we don't need tyConInjectivtyInfo. This works fine for closed +-- so we don't need tyConInjectivityInfo. This works fine for closed -- type families without injectivity info --- See Note [Exploiting closed type families] mkTopClosedFamEqFDs ax work_args (EqCt { eq_ev = ev, eq_rhs = work_rhs }) | isGenerativeType work_rhs -- See (CF5) in Note [Exploiting closed type families] = Stage $ @@ -679,39 +687,46 @@ hasRelevantGiven eqs_for_me work_args (EqCt { eq_rhs = work_rhs }) relevant (EqCt { eq_ev = ev, eq_lhs = lhs, eq_rhs = rhs_ty }) | isGiven ev , TyFamLHS _ lhs_tys <- lhs - = isJust (tcUnifyTysForInjectivity True work_tys (rhs_ty:lhs_tys)) + = isJust (tcUnifyTysForInjectivity Unifying work_tys (rhs_ty:lhs_tys)) | otherwise = False getRelevantBranches :: CoAxiom Branched -> [TcType] -> Xi -> [FunDepEqns] -- Return the FunDepEqns that arise from each relevant branch +-- Implements Note [Relevance] getRelevantBranches ax work_args work_rhs - = go [] (fromBranches (coAxiomBranches ax)) + = go (fromBranches (coAxiomBranches ax)) where work_tys = work_rhs : work_args - go _ [] = [] - go preceding (branch:branches) + go [] = [] + go (branch:branches) = case is_relevant branch of - Just eqn -> eqn : go (branch:preceding) branches - Nothing -> go (branch:preceding) branches + Just eqn -> eqn : go branches + Nothing -> go branches where - is_relevant (CoAxBranch { cab_tvs = qtvs, cab_lhs = lhs_tys, cab_rhs = rhs_ty }) - | Just subst <- tcUnifyTysForInjectivity True (rhs_ty:lhs_tys) work_tys - , let (subst', qtvs') = trim_qtvs subst qtvs - lhs_tys' = substTys subst' lhs_tys - rhs_ty' = substTy subst' rhs_ty - , all (no_match lhs_tys') preceding + is_relevant branch@(CoAxBranch { cab_tvs = qtvs + , cab_lhs = lhs_tys + , cab_rhs = rhs_ty }) + | Just subst <- tcUnifyTysForInjectivity Unifying (rhs_ty:lhs_tys) work_tys + -- See (RW1)-(RW3) in Note [Relevance] + -- This is a pre-/unification/ check (not matching) + -- so `subst` can bind both `qtvs` and fvs(work_tys) + , let (subst',qtvs') = trim_qtvs subst qtvs + lhs_tys' = substTys subst' lhs_tys + rhs_ty' = substTy subst' rhs_ty + branch_tys' = rhs_ty' : lhs_tys' + , noEarlierMatchCheck lhs_tys' branch -- See (RW4) in Note [Relevance] = Just (FDEqns { fd_qtvs = qtvs' - , fd_eqs = zipWith Pair (rhs_ty':lhs_tys') work_tys }) + , fd_eqs = zipWith Pair branch_tys' work_tys }) + -- Do not apply the substition to `work_tys`; + -- See (CF7) in Note [Exploiting closed type families] | otherwise = Nothing - no_match lhs_tys (CoAxBranch { cab_lhs = lhs_tys1 }) - = isNothing (tcUnifyTysForInjectivity False lhs_tys1 lhs_tys) - mkTopOpenFamEqFDs :: TyCon -> [Bool] -> [TcType] -> EqCt -> TcS [FunDepEqns] --- Implements (INJFAM:Wanted/top) +-- Implements (INJFAM:Wanted/top-open) +-- See Note [Exploiting open type families] mkTopOpenFamEqFDs fam_tc inj_flags work_args (EqCt { eq_rhs = work_rhs }) = do { fam_envs <- getFamInstEnvs ; let branches :: [CoAxBranch] @@ -720,15 +735,15 @@ mkTopOpenFamEqFDs fam_tc inj_flags work_args (EqCt { eq_rhs = work_rhs }) ; return (mapMaybe do_one branches) } where do_one :: CoAxBranch -> Maybe FunDepEqns - do_one branch@(CoAxBranch { cab_tvs = branch_tvs - , cab_lhs = branch_lhs_tys - , cab_rhs = branch_rhs }) - | Just subst <- tcUnifyTysForInjectivity False [branch_rhs] [work_rhs] - -- False: matching, not unifying - , let (subst', qtvs) = trim_qtvs subst branch_tvs + do_one (CoAxBranch { cab_tvs = branch_qtvs + , cab_lhs = branch_lhs_tys + , cab_rhs = branch_rhs }) + | Just subst <- tcUnifyTysForInjectivity Matching [branch_rhs] [work_rhs] + , let (subst', qtvs') = trim_qtvs subst branch_qtvs branch_lhs_tys' = substTys subst' branch_lhs_tys - , apartnessCheck branch_lhs_tys' branch -- See (TIF3) - = Just (mkInjectivityFDEqn inj_flags qtvs branch_lhs_tys' work_args) + -- No need for an apartness check here; for open type families + -- there are no "preceding" equations + = Just (mkInjectivityFDEqn inj_flags qtvs' branch_lhs_tys' work_args) | otherwise = Nothing @@ -736,7 +751,7 @@ mkTopOpenFamEqFDs fam_tc inj_flags work_args (EqCt { eq_rhs = work_rhs }) mkLocalFamEqFDs :: [EqCt] -> TyCon -> [Bool] -> [TcType] -> Xi -> SolverStage [FunDepEqns] -- Wanted constraints only -- Both open and closed type families, but only ones with declared injectivity --- See Note [Type inference for type families with injectivity] esp (TIF2) +-- See Note [Exploiting local type-family injectivity] mkLocalFamEqFDs eqs_for_me fam_tc inj_flags work_args work_rhs = do { let -- eqns_from_inerts: see (INJFAM:Wanted/other) eqns_from_inerts = mapMaybe do_one eqs_for_me @@ -755,15 +770,23 @@ mkLocalFamEqFDs eqs_for_me fam_tc inj_flags work_args work_rhs mk_eqn iargs = mkInjectivityFDEqn inj_flags [] work_args iargs -trim_qtvs :: Subst -> [TcTyVar] -> (Subst,[TcTyVar]) --- Tricky stuff: see (TIF1) in --- Note [Type inference for type families with injectivity] -trim_qtvs subst [] = (subst, []) -trim_qtvs subst (tv:tvs) - | tv `elemSubst` subst = trim_qtvs subst tvs - | otherwise = let !(subst1, tv') = substTyVarBndr subst tv - !(subst', tvs') = trim_qtvs subst1 tvs - in (subst', tv':tvs') +trim_qtvs :: Subst -> [TyVar] -> (Subst, [TyVar]) +-- Tricky stuff: see (OF1) in Note [Exploiting open type families] +-- The returned substitution is identical to the incoming one, except that +-- its in-scope set is extended with the returned [TyVar] +trim_qtvs unif_subst qtvs + = go unif_subst qtvs + where + go :: Subst -> [TyVar] -> (Subst, [TyVar]) + go subst [] = (subst, []) + go subst (tv:tvs) + | tv `elemSubst` unif_subst = go subst tvs + | otherwise = (subst'', tv':tvs') + where + tv' = tv `setTyVarKind` substTy subst (tyVarKind tv) + subst' = subst `extendSubstInScope` tv' + !(subst'', tvs') = go subst' tvs + ----------------------------------------- -- Built-in type families @@ -924,15 +947,20 @@ we attempt to exploit injectivity, via `mkLocalFamEqFDs`: * (INJFAM:Wanted/other) see `mkLocalFamEqFDs` work item: [W] F s1 s2 ~ rhs -- Wanted inert: [G/W] F t2 t2 ~ rhs -- Same `rhs`, Given or Wanted - We can generate FunDepEqns: (s2 ~ t2) + See Note [Exploiting local type-family injectivity] + +* (INJFAM:Wanted/top-open) for open type families: `mkTopOpenFamEqFDs` + type family F a b = r | r -> b + type instance F Int (Maybe a) = [G Int] -- G is a type family + [W] F alpha beta = [ty] + We can generate (Maybe gamma ~ beta) + See Note [Exploiting open type families] -* (INJFAM:Wanted/top) see `mkTopUserFamEqFDs` - work item: [W] F s1 s2 ~ rhs - type instance forall a b c. F t1 t2 ~ top_rhs - and we can /match/ the LHS, so that - S(top_rhs) = rhs - then we can generate the FunDepEqns: forall a c. s2 ~ S(t2) - But see wrinkle (TIF1), (TIF3) +* (INJFAM:Wanted/top-closed) for closed type families: `mkTopClosedFamEqFDs` + type family F a b where { ...eqns... } + [W] F alpha ~ Int + We may be able to generate some extra equalities to constraint `alpha` + See very clever Note [Exploiting closed type families] For /built-in/ type families, it's pretty similar, except that @@ -945,45 +973,36 @@ For /built-in/ type families, it's pretty similar, except that * mkLocalBuiltinFamEqFDs * mkTopBuiltinFamEqFDs -(TIF1) Generating fundeps from a top-level type instance is covered in - Section 5.2 in the Injective Type Families paper. It's a bit tricky. - Consider - type family F @k (a::k) (b::k) = r | r -> k b - type instance forall k (a::k) (b::k). F @k (Proxy @k a) (Proxy @k b) = Proxy @k a - [W] F @kappa alpha beta ~ Maybe (Proxy @kappa (delta::kappa)) +Note [Exploiting local type-family injectivity] see `mkLocalFamEqFDs` +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we have a type family with declared injectivity: + type family F a b = r | r -> b +and we have + work item: [W] F s1 s2 ~ F t1 t2 +or + work item: [W] F s1 s2 ~ rhs -- Wanted + inert: [G/W] F t2 t2 ~ rhs -- Same `rhs`, Given or Wanted - we match (Proxy @kappa delta) against the template (Proxy k a), succeeding - with substitution [k:->kappa, a:->delta]. We want to generate this FunDepEqns - FDEqn { fd_qtvs = [b:kappa], fd_eqs = [ beta ~ Proxy @kappa b ] } - Notice that - * we must quantify the FunDepEqns over `b`, which is not matched; for this - we will generate a fresh unification variable in `instantiateFunDepEqn`. - * we must substitute `k:->kappa` in the kind of `b`. - This fancy footwork for `fd_qtvs` is done by `trim_qtvs` in - `mkInjWantedFamEqTopEqns`. +Then we can generate FunDepEqns: (s2 ~ t2) + +This applies equally to /closed/ type families; it is /not/ subsumed +by Note [Exploiting closed type families]. Consider: -(TIF2) All this applies equally to /closed/ type families; it is /not/ - subsumed by Note [Exploiting closed type families]. Consider: type family F a | r -> a where { .... } [W] F t1 ~ a [W] F t2 ~ a - Then since F is declared injective, we can generate t1~t2. +Then since F is declared injective, we can generate t1~t2. - As for open type families, we insist on /user-declared/ injectivity only; we - don't try to /infer/ injectivity even for a closed family. See Section 3.4 - of the "Injective type families" paper. (Arguably, we could /infer/ - injectivity for closed type families, and that would be more in the spirit of - Note [Exploiting closed type families].) +As for open type families, we insist on /user-declared/ injectivity only; we +don't try to /infer/ injectivity even for a closed family. See Section 3.4 +of the "Injective type families" paper. (Arguably, we could /infer/ +injectivity for closed type families, and that would be more in the spirit of +Note [Exploiting closed type families].) -(TIF3) Further to (TIF1), if we are considering a /closed/ type family, we - must ensure (see Section 5.2 of the paper) that after matching that - equation would indeed be the one to fire. So we call `apartnessCheck` - on the branch to ensure this, in `mkTopUserFamEqFDs`. - -Definition [Relevance] -~~~~~~~~~~~~~~~~~~~~~~ +Note [Relevance] +~~~~~~~~~~~~~~~~ We say that a closed-type-family equation `F lhs = rhs` is /relevant/ for a Wanted [W] F wlhs ~ wrhs iff @@ -992,6 +1011,10 @@ iff (R2) There is no earlier equation that matches S(lhs). See (RW4) below. +The relevance check is implemented by `getRelevantBranches`, which acutally +returns the [FunDepEqns] described in the Closed Family Fundep Algorithm in +Note [Exploiting closed type families]. + (RW1) Pre-unification treats type-family applications as binding to anything, rather like type variables. If two types don't even pre-unify, we say that they are /apart/. It is done by `tcUnifyTysForInjectivity`. @@ -1014,24 +1037,99 @@ iff Clearly the RHS is apart from the first equation and we want to fire injectivity on the second equation. -(RW4) Why "no earlier equation matches" in conditoin (R2)? Consider the family +(RW4) Why "no earlier equation matches" in condition (R2)? Consider the family type family Bak a = r where Bak Int = Char -- B1 Bak Char = Int -- B2 Bak a = a -- B3 - and [W] Bak alpha ~ Char. In fact, only (B2) is relevant for this Wanted. + and [W] Bak alpha ~ Char. In fact, only (B1) is relevant for this Wanted. You might think that (B3) could be instantiated to Bak Char ~ Char; but actually that instantiation will never fire because (B2) Bak Char ~ Int would - fire first. So the only way to return a Char is if the argment is Int; so we - can emit [W] alpha ~ Int. Hence (B3) is not relevant; only (B2) is relevant. + fire first. So the only way to return a Char is via (B1); so we + can emit [W] alpha ~ Int. Hence (B3) is not relevant; only (B1) is relevant. That is the reason for condition (R2) in the definition of Relevance above. A watertight proof that this is the Right Thing is not very easy. See more - discussion in #23162. + discussion in #23162, and Section 5.2 of the paper. + + How, precisely, do we implement (R2)? We check that there is no earlier equation + that fires on S(lhs), in this case (on Bak Char). Notice that this is different + from the `apartnessCheck`, which checks that all preceding equations are apart + from S(lhs). Apartness checking uses /unification/; here we want /matching/. + Hence using `noEarlierMatchCheck`, not `apartnessCheck`. + + Here's a good example from T27171_aux. T + type family TMessage m where + {- T1 -} TMessage @f @t (CustomMethod s :: Method f t) = () + {- T2 -} TMessage @f @Req (m :: Method f Req) = TRequestMessage m + {- T3 -} TMessage @f @Not (m :: Method f Not) = TNotificationMessage m + + [W] TMessage @SC @Req alpha ~# TRequestMessage alpha + + There is only one relevant equation, namely (T2). If we apply its + pre-unification substitution [f :-> SC, m :-> alpha] to its LHS we get + TMessage @SC @Req alpha + and equation (T1) does not match that. (It does unify, but we don't care.) + +(RW5) `noEarlierMatchCheck`: in (RW4) We really do need to check that /no/ + earlier equation matches, not just no earlier /incompatible/ equation + matches. Consider T27282a: + type family F a where + F Int = Int -- B1 + F Char = Bool -- B2 + F a = a -- B3 + + [W] F alpha ~ Int + + (B1) is relevant, and (B2) is not. What about (B3)? It pre-unifies with + the Wanted via [alpha :-> Int, a :-> Int]. But under that substitution + (B1) would fire, so (B3) is not relevant. + + And yet, (B1) is /compatible/ with (B3), so it's no good just looking at + the `cab_incomps` of (B3). Instead we look at `cab_overlaps`. + +Note [Exploiting open type families] see `mkTopOpenFamEqFDs` +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Generating fundeps from a top-level type instance is covered in Section 5.2 in +the Injective Type Families paper. For open type families, suppose we have + + type family F a b = r | r -> b + type instance F Int (Maybe a) = [G Int] -- G is a type family + + [W] F alpha beta = [ty] + +Then, since F has been checked as injective, and the RHS [G Int] +pre-unifies with [ty], we can add a derived FunDepEqns + FDEqns{ fd_qtvs = a, fd_eqs = [ Maybe a ~ beta ] } +and thereby emit + [W] Maybe gamma ~ beta -- Fresh gamma + +Wrinkles + +(OF1) Consider + type family F @k (a::k) (b::k) = r | r -> k b + type instance forall k (a::k) (b::k). + F @k (Proxy @k a) (Proxy @k b) = Maybe (Proxy @k a) -Note [Exploiting closed type families] + [W] F @kappa alpha beta ~ Maybe (Proxy @kappa (delta::kappa)) + + We match the target (Maybe (Proxy @kappa delta)) + against the template (Maybe (Proxy @k a)) + succeeding with substitution [k:->kappa, a:->delta]. We want to generate this: + FDEqn { fd_qtvs = [b::kappa], fd_eqs = [ Proxy @kappa b ] ~ beta } + Notice that + * we must quantify the FunDepEqns over `b`, which is not matched; for this + we will generate a fresh unification variable in `instantiateFunDepEqn`. + * we must substitute `k:->kappa` in the kind of `b`. + + This fancy footwork for `fd_qtvs` is done by `trim_qtvs`. It + * Drops a quantified tyvar that /is/ matched + * Substitutes in the kind of a quantified tyvar that is /not/ matched + * Adds the not-matched tyvar to the in-scope set of the substitution + +Note [Exploiting closed type families] see `mkTopClosedFamEqFDs` ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose we have type family F a b where @@ -1042,17 +1140,18 @@ Suppose we have [W] F Int alpha ~ Char The /only/ way to solve this Wanted is using (F2), so we can safely unify -alpha:=Char without risking losing any solutions. That is what -`mkTopClosedFamEqFDs` does. Ticket #23162 has lots of background detail +alpha:=Char without risking losing any solutions. We don't even need any +injectivity annotations. Ticket #23162 has lots of background detail. -More precisely, here is the Closed Family Fundep Algorithm (CFFA) +More precisely, here is the very clever Closed Family Fundep Algorithm (CFFA) IF * F a is a closed type family. * We are trying to solve [W] F wlhs ~ wrhs. - * There are no "relevant" Givens [G] F lhs ~ rhs. See (CF1) below. - * F has exactly one equation, F lhs = rhs that is "relevant" for that Wanted + * There are no "relevant Givens" [G] F lhs ~ rhs. See (CF1) below. + * F has exactly one equation, F lhs = rhs that is "relevant" for + that Wanted (see Note [Relevance]) THEN - we can emit and solve the fundep equalities: + we can emit and solve the fundeps :: [FunDepEqns]: [W] wlhs1 ~ lhs1 ... [W] wlhsn ~ lhsn @@ -1060,7 +1159,10 @@ More precisely, here is the Closed Family Fundep Algorithm (CFFA) with fresh unification vars in lhs and rhs for the quantified variables of the equation. -See Definition [Relevance] for what "relevant" means. + Actually we take advantage of the substitution generated by the relevance + check, see (CF7) below. + +See Note [Relevance] for what "relevant" means. We need to take care about non-termination; see (CF3). Key point: equations that are not relevant do not need to be considered for fundeps at all. @@ -1166,6 +1268,8 @@ Key point: equations that are not relevant do not need to be considered for fund I was looking at non-termination for closed type families, but it's a small improvement in general. + This bale-out is implementedn in `tryFDEqns`. + (CF5) Consider (see "Yikes5" in #23162): type family F a where F (Just x) = Int @@ -1196,7 +1300,7 @@ Key point: equations that are not relevant do not need to be considered for fund type family I t = res | res -> t where I TInt = Int |> g -- where g :: Type ~# IK k and [W] I alpha ~ Int |> g2 - Here we definiteily want to take advantage of injectivity. + Here we definitely want to take advantage of injectivity. (CF6) This machinery can also have a significant positive effect on the size of proof terms. For example (simplification of T26426): @@ -1204,7 +1308,8 @@ Key point: equations that are not relevant do not need to be considered for fund type family (++) a b where { '[] ++ ys = ys; (x:xs) ++ ys = x : (xs ++ ys) } type family MapId a where { MapId '[] = '[]; MapId (x:xs) = x : MapId xs } - app :: (MapId xs ++ MapId ys ~ MapId (xs ++ ys)) => Proxy xs -> Proxy ys -> Proxy (xs ++ ys) + app :: (MapId xs ++ MapId ys ~ MapId (xs ++ ys)) + => Proxy xs -> Proxy ys -> Proxy (xs ++ ys) test :: Proxy [ty_1, ..., ty_n] test = Proxy @'[ty_1] @@ -1248,6 +1353,30 @@ Key point: equations that are not relevant do not need to be considered for fund instead of relying on recursively built sub-proof terms, which brings down coercion sizes (in certain situations) from O(n^3) to O(n^2). +(CF7) Relevance. When computing relevance in the Closed Family Fundep Algorithm, + for [W] F wlhs1 wlhs2 ~ wrhs, against an equation F lhs1 lhs2 ~ rhs + we get back a pre-unifying substitution S that makes the two as equal as poss. + Then we use `trim_qtvs` in exactly the same way as in + (OF1) of Note [Exploiting closed type families], to generate qtvs' and S' + Then we generate + FDEqns { fd_qtvs = qtvs', fd_eqs [ S'(lhs1) ~ wlhs1 + , S'(lhs2) ~ wlhs2 + , S'(rhs) ~ wrhs ] } + Notice that we do /not/ apply S' to wlhs/wrhs. These type contain unification + variables that we must actually unify! Example + type familiy F a b where + F [a] (Maybe b) = (a, G b) + [W] F alpha beta ~ (Int, [gamma]) + Pre-unification gives [alpha :-> [a], beta :-> Maybe b, a :-> Int] + This substitution eliminates the quantified variable `a` but not `b`, so we + want this: + FDEqns { fd_qtvs = [b], fd_eqs [ [Int] ~ alpha + , Maybe b ~ beta + , (Int,G b) ~ (Int, [gamma]) ] } + + Notice also that by applying the substitution to the template but not to the + Wanted, we uphold the `fd_eqs` invariant in `FDEqns` (see its data type decl) + Note [Cache-caused loops] ~~~~~~~~~~~~~~~~~~~~~~~~~ It is very dangerous to cache a rewritten wanted family equation as 'solved' in @@ -1340,28 +1469,34 @@ solveFunDeps work_ev fd_eqns ; uPairsTcM uenv eqs } instantiateFunDepEqns :: FunDepEqns -> TcM [TypeEqn] -instantiateFunDepEqns (FDEqns { fd_qtvs = tvs, fd_eqs = eqs }) - | null tvs +-- See GHC.Tc.Instance.Fundeps Note [Improving against instances] +-- Wrinkle (IMP1) +instantiateFunDepEqns (FDEqns { fd_qtvs = qtvs, fd_eqs = eqs }) + | null qtvs = return rev_eqs | otherwise - = do { TcM.traceTc "instantiateFunDepEqns" (ppr tvs $$ ppr eqs) - ; (_, subst) <- instFlexiXTcM emptySubst tvs -- Takes account of kind substitution + = do { TcM.traceTc "instantiateFunDepEqns" (ppr qtvs $$ ppr eqs) + ; (_, subst) <- instFlexiXTcM empty_subst qtvs -- Takes account of kind substitution ; return (map (subst_pair subst) rev_eqs) } where rev_eqs = reverse eqs -- (reverse eqs): See Note [Reverse order of fundep equations] + -- The kinds of `qtvs` can have free variables, because of `trim_qtvs` + -- Example: T27828b + empty_subst = mkEmptySubst $ mkInScopeSet $ + tyCoVarsOfTypes (map tyVarKind qtvs) + subst_pair subst (Pair ty1 ty2) - = Pair (substTyUnchecked subst' ty1) ty2 - -- ty2 does not mention fd_qtvs, so no need to subst it. - -- See GHC.Tc.Instance.Fundeps Note [Improving against instances] - -- Wrinkle (1) + = Pair (substTy subst' ty1) ty2 + -- NB: ty2 does not mention fd_qtvs, so no need to subst it. + -- See invariant on `fv_eqs` in `data FunDepEqns`. where subst' = extendSubstInScopeSet subst (tyCoVarsOfType ty1) -- The free vars of ty1 aren't just fd_qtvs: ty1 is the result -- of matching with the [W] constraint. So we add its free -- vars to InScopeSet, to satisfy substTy's invariants, even - -- though ty1 will never (currently) be a poytype, so this + -- though ty1 will never (currently) be a polytype, so this -- InScopeSet will never be looked at. ===================================== compiler/GHC/Tc/TyCl.hs ===================================== @@ -3462,7 +3462,7 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info ; let mb_co_ax | null eqns = Nothing -- mkBranchedCoAxiom fails on empty list - | otherwise = Just (mkBranchedCoAxiom co_ax_name fam_tc branches) + | otherwise = Just (mkBranchedCoAxiom Nominal co_ax_name fam_tc branches) fam_tc = mkFamilyTyCon tc_name kind tc_bndrs 0 res_kind (resultVariableName sig) (ClosedTypeFamilyTyCon $ CTF mb_co_ax) parent inj' ===================================== testsuite/tests/indexed-types/should_compile/T27828.hs ===================================== @@ -0,0 +1,50 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeAbstractions #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} +module Bug where + +import Data.Functor.Identity (Identity(..)) +import Data.Kind (Type) +import Data.Proxy (Proxy(..)) +import Data.Type.Equality ((:~:)(..)) + +type TyFun :: Type -> Type -> Type +data TyFun a b + +type (~>) :: Type -> Type -> Type +type a ~> b = TyFun a b -> Type +infixr 0 ~> + +type Apply :: (k1 ~> k2) -> k1 -> k2 +type family Apply f x + +type Rep1 :: (k -> Type) -> k -> Type +type family Rep1 f + +type To1 :: Rep1 f a -> f a +type family To1 z + +type Par1 :: Type -> Type +newtype Par1 p = Par1 p + +type To1Sym0 :: forall k (f :: k -> Type) (a :: k). Rep1 f a ~> f a +data To1Sym0 z + +applyTo1Sym0 :: forall k (f :: k -> Type) (a :: k) (x :: Rep1 f a). Proxy x -> Apply @(Rep1 f a) @(f a) To1Sym0 x :~: To1 x +applyTo1Sym0 _ = undefined + +type IdentitySym0 :: a ~> Identity a +data IdentitySym0 z +type instance Apply IdentitySym0 x = 'Identity x + +type Aux :: Rep1 Identity a -> Rep1 Identity a -> Identity a +type family Aux x y where + Aux x ('Par1 wombat) = Apply IdentitySym0 wombat + +type instance Rep1 Identity = Par1 +type instance To1 @Identity y = Aux y y + +lemma :: forall a (z :: a). Apply @(Rep1 Identity a) @(Identity a) To1Sym0 ('Par1 z) :~: 'Identity z +lemma = applyTo1Sym0 @Type @Identity @a (Proxy @('Par1 z)) +-- lemma = applyTo1Sym0 @Type @Identity @a @('Par1 z) (Proxy @('Par1 z)) ===================================== testsuite/tests/indexed-types/should_compile/T27828a.hs ===================================== @@ -0,0 +1,16 @@ +{-# LANGUAGE TypeFamilies #-} + +module T27828a where + +import Data.Proxy + +type family F a where + F Int = Int -- B1 + F Char = Bool -- B2 + F a = a -- B3 + +h :: (F a ~ Int) => Proxy a -> () +h = error "urk" + +k :: () +k = h Proxy -- [W] F alpha ~ Int ===================================== testsuite/tests/indexed-types/should_compile/T27828b.hs ===================================== @@ -0,0 +1,12 @@ +{-# LANGUAGE TypeFamilies, KindSignatures, AllowAmbiguousTypes #-} + +module T27878b where + +type family IsJust (m :: Maybe k) :: Bool where + IsJust ('Just x) = 'True + IsJust 'Nothing = 'False + +f :: forall k (m :: Maybe k). (IsJust m ~ 'True) => Int -> Int +f = error "urk" + +g _ = f 3 -- Triggered checkValidSubst error in `instantiateFunDepEqns`o ===================================== testsuite/tests/indexed-types/should_compile/all.T ===================================== @@ -316,3 +316,6 @@ test('T25611b', normal, compile, ['']) test('T25611c', normal, compile, ['']) test('T25611d', normal, compile, ['']) test('T25657', normal, compile, ['']) +test('T27828', normal, compile, ['']) +test('T27828a', normal, compile, ['']) +test('T27828b', normal, compile, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/cac84324f535b94e941767f4250fb79… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/cac84324f535b94e941767f4250fb79… 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