Marge Bot pushed to branch wip/marge_bot_batch_merge_job at Glasgow Haskell Compiler / GHC Commits: 029cd285 by sheaf at 2025-08-12T05:18:21-04:00 Improve deep subsumption This commit improves the DeepSubsumption sub-typing implementation in GHC.Tc.Utils.Unify.tc_sub_type_deep by being less eager to fall back to unification. For example, we now are properly able to prove the subtyping relationship ((∀ a. a->a) -> Int) -> Bool <= β[tau] Bool for an unfilled metavariable β. In this case (with an AppTy on the right), we used to fall back to unification. No longer: now, given that the LHS is a FunTy and that the RHS is a deep rho type (does not need any instantiation), we try to make the RHS into a FunTy, viz. β := (->) γ We can then continue using covariance & contravariance of the function arrow, which allows us to prove the subtyping relationship, instead of trying to unify which would cause us to error out with: Couldn't match expected type ‘β’ with actual type ‘(->) ((∀ a. a -> a) -> Int) See Note [FunTy vs non-FunTy case in tc_sub_type_deep] in GHC.Tc.Utils.Unify. The other main improvement in this patch concerns type inference. The main subsumption logic happens (before & after this patch) in GHC.Tc.Gen.App.checkResultTy. However, before this patch, all of the DeepSubsumption logic only kicked in in 'check' mode, not in 'infer' mode. This patch adds deep instantiation in the 'infer' mode of checkResultTy when we are doing deep subsumption, which allows us to accept programs such as: f :: Int -> (forall a. a->a) g :: Int -> Bool -> Bool test1 b = case b of True -> f False -> g test2 b = case b of True -> g False -> f See Note [Deeply instantiate in checkResultTy when inferring]. Finally, we add representation-polymorphism checks to ensure that the lambda abstractions we introduce when doing subsumption obey the representation polymorphism invariants of Note [Representation polymorphism invariants] in GHC.Core. See Note [FunTy vs FunTy case in tc_sub_type_deep]. This is accompanied by a courtesy change to `(<.>) :: HsWrapper -> HsWrapper -> HsWrapper`, adding the equation: WpCast c1 <.> WpCast c2 = WpCast (c1 `mkTransCo` c2) This is useful because mkWpFun does not introduce an eta-expansion when both of the argument & result wrappers are casts; so this change allows us to avoid introducing lambda abstractions when casts suffice. Fixes #26225 - - - - - f8345920 by Sylvain Henry at 2025-08-12T05:18:46-04:00 Add regression test for #18619 - - - - - 530a27ba by Sylvain Henry at 2025-08-12T05:18:52-04:00 RTS: remove some TSAN annotations (#20464) Use RELAXED_LOAD_ALWAYS macro instead. - - - - - 64fad685 by Ben Gamari at 2025-08-12T05:18:53-04:00 Bump time submodule to 1.15 Also required bumps of Cabal, directory, and hpc. - - - - - 38 changed files: - compiler/GHC/Builtin/PrimOps/Ids.hs - compiler/GHC/HsToCore.hs - compiler/GHC/Tc/Gen/App.hs - compiler/GHC/Tc/Gen/Expr.hs - compiler/GHC/Tc/Gen/HsType.hs - compiler/GHC/Tc/Types/Evidence.hs - compiler/GHC/Tc/Types/Origin.hs - compiler/GHC/Tc/Utils/Concrete.hs - compiler/GHC/Tc/Utils/Unify.hs - compiler/GHC/Types/Id/Make.hs - compiler/ghc.cabal.in - ghc/ghc-bin.cabal.in - libraries/Cabal - libraries/directory - libraries/hpc - libraries/time - libraries/unix - rts/posix/ticker/Pthread.c - rts/posix/ticker/TimerFd.c - testsuite/tests/corelint/LintEtaExpand.stderr - testsuite/tests/indexed-types/should_fail/T5439.stderr - + testsuite/tests/numeric/should_run/T18619.hs - + testsuite/tests/numeric/should_run/T18619.stderr - testsuite/tests/numeric/should_run/all.T - testsuite/tests/partial-sigs/should_compile/T10403.stderr - testsuite/tests/partial-sigs/should_fail/T10615.stderr - + testsuite/tests/rep-poly/NoEtaRequired.hs - testsuite/tests/rep-poly/T21906.stderr - testsuite/tests/rep-poly/all.T - + testsuite/tests/typecheck/should_compile/T26225.hs - + testsuite/tests/typecheck/should_compile/T26225b.hs - testsuite/tests/typecheck/should_compile/all.T - − testsuite/tests/typecheck/should_fail/T12563.stderr - testsuite/tests/typecheck/should_fail/T14618.stderr - testsuite/tests/typecheck/should_fail/T6022.stderr - testsuite/tests/typecheck/should_fail/T8883.stderr - testsuite/tests/typecheck/should_fail/all.T - testsuite/tests/typecheck/should_fail/tcfail140.stderr The diff was not included because it is too large. View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/081487ad8f0d44957517b68bebb3a36... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/081487ad8f0d44957517b68bebb3a36... You're receiving this email because of your account on gitlab.haskell.org.