- ghc-commits - Haskell.org

[Git][ghc/ghc][wip/T26315] Solve forall-constraints via an implication, again
by Simon Peyton Jones (＠simonpj) 08 Sep '25

08 Sep '25

Simon Peyton Jones pushed to branch wip/T26315 at Glasgow Haskell Compiler / GHC Commits: 2905ad3d by Simon Peyton Jones at 2025-09-08T14:24:14+01:00 Solve forall-constraints via an implication, again In this earlier commit: commit 953fd8f1dc080f1c56e3a60b4b7157456949be29 Author: Simon Peyton Jones <simon.peytonjones(a)gmail.com> Date: Mon Jul 21 10:06:43 2025 +0100 Solve forall-constraints immediately, or not at all I used a all-or-nothing strategy for quantified constraints (aka forall-constraints). But alas that fell foul of #26315, and #26376. So this MR goes back to solving a quantified constraint by turning it into an implication; UNLESS we are simplifying constraints from a SPECIALISE pragma, in which case the all-or-nothing strategy is great. See: Note [Solving a Wanted forall-constraint] Other stuff in this MR: * TcSMode becomes a record of flags, rather than an enumeration type; much nicer. * Some fancy footwork to avoid error messages worsening again (The above MR made them better; we want to retain that.) See `GHC.Tc.Errors.Ppr.pprQCOriginExtra`. - - - - - 44 changed files: - compiler/GHC/HsToCore/Binds.hs - compiler/GHC/Tc/Deriv/Utils.hs - compiler/GHC/Tc/Errors/Ppr.hs - compiler/GHC/Tc/Gen/Sig.hs - compiler/GHC/Tc/Solver.hs - compiler/GHC/Tc/Solver/Default.hs - compiler/GHC/Tc/Solver/Dict.hs - compiler/GHC/Tc/Solver/Equality.hs - compiler/GHC/Tc/Solver/InertSet.hs - compiler/GHC/Tc/Solver/Monad.hs - compiler/GHC/Tc/Solver/Solve.hs - compiler/GHC/Tc/Solver/Solve.hs-boot - compiler/GHC/Tc/Types/Constraint.hs - compiler/GHC/Tc/Types/Evidence.hs - compiler/GHC/Tc/Types/Origin.hs - compiler/GHC/Tc/Utils/Monad.hs - compiler/GHC/Tc/Zonk/TcType.hs - compiler/GHC/Tc/Zonk/Type.hs - testsuite/tests/backpack/should_fail/bkpfail11.stderr - testsuite/tests/backpack/should_fail/bkpfail43.stderr - testsuite/tests/deriving/should_fail/T12768.stderr - testsuite/tests/deriving/should_fail/T1496.stderr - testsuite/tests/deriving/should_fail/T21302.stderr - testsuite/tests/deriving/should_fail/T22696b.stderr - testsuite/tests/deriving/should_fail/T5498.stderr - testsuite/tests/deriving/should_fail/T7148.stderr - testsuite/tests/deriving/should_fail/T7148a.stderr - testsuite/tests/impredicative/T17332.stderr - testsuite/tests/quantified-constraints/T19690.stderr - testsuite/tests/quantified-constraints/T19921.stderr - testsuite/tests/quantified-constraints/T21006.stderr - testsuite/tests/roles/should_fail/RolesIArray.stderr - testsuite/tests/simplCore/should_compile/DsSpecPragmas.hs - testsuite/tests/simplCore/should_compile/DsSpecPragmas.stderr - testsuite/tests/typecheck/should_compile/T14434.hs - + testsuite/tests/typecheck/should_compile/T26376.hs - testsuite/tests/typecheck/should_compile/all.T - testsuite/tests/typecheck/should_fail/T15801.stderr - testsuite/tests/typecheck/should_fail/T19627.stderr - testsuite/tests/typecheck/should_fail/T20666.stderr - testsuite/tests/typecheck/should_fail/T20666a.stderr - testsuite/tests/typecheck/should_fail/T20666b.stderr - testsuite/tests/typecheck/should_fail/T22912.stderr - testsuite/tests/typecheck/should_fail/T23427.stderr The diff was not included because it is too large. View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2905ad3d427b01d67f36e373006fdc1… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2905ad3d427b01d67f36e373006fdc1… You're receiving this email because of your account on gitlab.haskell.org.

1 0

[Git][ghc/ghc][wip/9.10.3-backports] Prepare 9.10.3 final
by Zubin (＠wz1000) 08 Sep '25

08 Sep '25

Zubin pushed to branch wip/9.10.3-backports at Glasgow Haskell Compiler / GHC Commits: 5004b538 by Zubin Duggal at 2025-09-08T14:26:26+05:30 Prepare 9.10.3 final - - - - - 4 changed files: - .gitlab/rel_eng/fetch-gitlab-artifacts/fetch_gitlab.py - .gitlab/rel_eng/upload.sh - configure.ac - docs/users_guide/9.10.3-notes.rst Changes: ===================================== .gitlab/rel_eng/fetch-gitlab-artifacts/fetch_gitlab.py ===================================== @@ -129,7 +129,7 @@ def fetch_artifacts(release: str, pipeline_id: int, for f in doc_files: subprocess.run(['tar', '-xf', f, '-C', dest]) logging.info(f'extracted docs {f} to {dest}') - index_path = destdir / 'docs' / 'index.html' + index_path = destdir / 'index.html' index_path.replace(dest / 'index.html') pdfs = list(destdir.glob('*.pdf')) for f in pdfs: @@ -165,3 +165,4 @@ def main(): gl = gitlab.Gitlab.from_config(args.profile) fetch_artifacts(args.release, args.pipeline, dest_dir=args.output, gl=gl) +main() ===================================== .gitlab/rel_eng/upload.sh ===================================== @@ -1,5 +1,4 @@ -#!/usr/bin/env nix-shell -#! nix-shell -i bash -p moreutils lzip zip lftp gnupg +#!/usr/bin/bash set -Eeuo pipefail @@ -41,7 +40,7 @@ set -Eeuo pipefail : ${ver:=$(ls ghc-*.tar.* | sed -ne 's/ghc-$[0-9]\+\.[0-9]\+\.[0-9]\+\(\.[0-9]\+$\?\).\+/\1/p' | head -n1)} if [ -z "$ver" ]; then echo "Failed to infer \$ver"; exit 1; fi -host="gitlab-storage.haskell.org" +host="gitlab.haskell.org:2222" usage() { echo "Usage: [rel_name=<name>] ver=7.10.3-rc2 $0 <action>" ===================================== configure.ac ===================================== @@ -13,7 +13,7 @@ dnl # see what flags are available. (Better yet, read the documentation!) # -AC_INIT([The Glorious Glasgow Haskell Compilation System], [9.10.2], [glasgow-haskell-bugs(a)haskell.org] [ghc-AC_PACKAGE_VERSION]) +AC_INIT([The Glorious Glasgow Haskell Compilation System], [9.10.3], [glasgow-haskell-bugs(a)haskell.org] [ghc-AC_PACKAGE_VERSION]) # Version on master must be X.Y (not X.Y.Z) for ProjectVersionMunged variable # to be useful (cf #19058). However, the version must have three components # (X.Y.Z) on stable branches (e.g. ghc-9.2) to ensure that pre-releases are @@ -22,7 +22,7 @@ AC_INIT([The Glorious Glasgow Haskell Compilation System], [9.10.2], [glasgow-ha AC_CONFIG_MACRO_DIRS([m4]) # Set this to YES for a released version, otherwise NO -: ${RELEASE=NO} +: ${RELEASE=YES} # The primary version (e.g. 7.5, 7.4.1) is set in the AC_INIT line # above. If this is not a released version, then we will append the ===================================== docs/users_guide/9.10.3-notes.rst ===================================== @@ -22,9 +22,6 @@ Compiler - Fix GHC.SysTools.Ar archive member size writing logic that was emitting wrong archive member sizes in headers. (:ghc-ticket:`26120`, :ghc-ticket:`22586`) -- Fix multiple bugs in name resolution of subordinate import lists related to - type namespace specifiers and hiding clauses. (:ghc-ticket:`22581`, :ghc-ticket:`25983`, :ghc-ticket:`25984`, :ghc-ticket:`25991`) - - Use mkTrAppChecked in ds_ev_typeable to avoid false negatives for type equality involving function types. (:ghc-ticket:`25998`) @@ -40,6 +37,9 @@ Compiler - Introduce a separate argument limit for forced specs via SPEC argument with warning when limit is exceeded. (:ghc-ticket:`25197`) +- Fix compiler crash in the renamer with certain programs referencing out of + scope record fields (:ghc-ticket:`25056`) + Build system and packaging ~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -79,6 +79,8 @@ WebAssembly backend Runtime system ~~~~~~~~~~~~~~ +- rts: Fix a segfault involving STM (:ghc-ticket:`26205`). + - rts: Implement WEAK EXTERNAL undef redirection by target symbol name. - rts: Handle API set symbol versioning conflicts. @@ -97,12 +99,12 @@ Runtime system ``base`` library ~~~~~~~~~~~~~~~~ -- base: Expose Backtraces constructor and fields. (:ghc-ticket:`26049`) - - base: Note strictness changes made in 4.16.0.0. (:ghc-ticket:`25886`) - Fix bugs in ``integerRecipMod`` and ``integerPowMod`` return values. (:ghc-ticket:`26017`) +- Fix incorrect results for ``naturalAndNot`` (:ghc-ticket:`26230`) + ``ghc`` library ~~~~~~~~~~~~~~~ @@ -112,9 +114,6 @@ Runtime system Build tools ~~~~~~~~~~~ -- configure: Drop probing of ld.gold since `gold` has been dropped from - binutils-2.44. (:ghc-ticket:`25716`) - - get-win32-tarballs.py: List tarball files to be downloaded if we cannot find them. (:ghc-ticket:`25929`) @@ -162,4 +161,4 @@ for further change information. libraries/transformers/transformers.cabal: Dependency of ``ghc`` library libraries/unix/unix.cabal: Dependency of ``ghc`` library libraries/Win32/Win32.cabal: Dependency of ``ghc`` library - libraries/xhtml/xhtml.cabal: Dependency of ``haddock`` executable \ No newline at end of file + libraries/xhtml/xhtml.cabal: Dependency of ``haddock`` executable View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5004b538d31aaaa220469ddae319c0e… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5004b538d31aaaa220469ddae319c0e… You're receiving this email because of your account on gitlab.haskell.org.

1 0

[Git][ghc/ghc][wip/T26315] 5 commits: Refactor ForAllCo
by Simon Peyton Jones (＠simonpj) 08 Sep '25

08 Sep '25

Simon Peyton Jones pushed to branch wip/T26315 at Glasgow Haskell Compiler / GHC Commits: 94b62aa7 by Simon Peyton Jones at 2025-09-08T03:37:14-04:00 Refactor ForAllCo This is a pure refactor, addressing #26389. It arranges that the kind coercion in a ForAllCo is a MCoercion, rather than a plain Coercion, thus removing redundancy in the common case. See (FC8) in Note [ForAllCo] It's a nice cleanup. - - - - - 624afa4a by sheaf at 2025-09-08T03:38:05-04:00 Use tcMkScaledFunTys in matchExpectedFunTys We should use tcMkScaledFunTys rather than mkScaledFunTys in GHC.Tc.Utils.Unify.matchExpectedFunTys, as the latter crashes when the kind of the result type is a bare metavariable. We know the result is always Type-like, so we don't need scaledFunTys to try to rediscover that from the kind. Fixes #26277 - - - - - 0975d2b6 by sheaf at 2025-09-08T03:38:54-04:00 Revert "Remove hptAllFamInstances usage during upsweep" This reverts commit 3bf6720eff5e86e673568e756161e6d6150eb440. - - - - - 0cf34176 by soulomoon at 2025-09-08T03:38:54-04:00 Family consistency checks: add test for #26154 This commit adds the test T26154, to make sure that GHC doesn't crash when performing type family consistency checks. This test case was extracted from Agda. Fixes #26154 - - - - - c249ca34 by Simon Peyton Jones at 2025-09-08T09:20:53+01:00 Solve forall-constraints via an implication, again In this earlier commit: commit 953fd8f1dc080f1c56e3a60b4b7157456949be29 Author: Simon Peyton Jones <simon.peytonjones(a)gmail.com> Date: Mon Jul 21 10:06:43 2025 +0100 Solve forall-constraints immediately, or not at all I used a all-or-nothing strategy for quantified constraints (aka forall-constraints). But alas that fell foul of #26315, and #26376. So this MR goes back to solving a quantified constraint by turning it into an implication; UNLESS we are simplifying constraints from a SPECIALISE pragma, in which case the all-or-nothing strategy is great. See: Note [Solving a Wanted forall-constraint] Other stuff in this MR: * TcSMode becomes a record of flags, rather than an enumeration type; much nicer. * Some fancy footwork to avoid error messages worsening again (The above MR made them better; we want to retain that.) See `GHC.Tc.Errors.Ppr.pprQCOriginExtra`. - - - - - 78 changed files: - compiler/GHC/Core/Coercion.hs - compiler/GHC/Core/Coercion.hs-boot - compiler/GHC/Core/Coercion/Opt.hs - compiler/GHC/Core/Lint.hs - compiler/GHC/Core/Opt/Arity.hs - compiler/GHC/Core/Reduction.hs - compiler/GHC/Core/TyCo/FVs.hs - compiler/GHC/Core/TyCo/Rep.hs - compiler/GHC/Core/TyCo/Subst.hs - compiler/GHC/Core/TyCo/Tidy.hs - compiler/GHC/Core/Type.hs - compiler/GHC/Core/Unify.hs - compiler/GHC/CoreToIface.hs - compiler/GHC/Driver/Env.hs - compiler/GHC/HsToCore/Binds.hs - compiler/GHC/Iface/Rename.hs - compiler/GHC/Iface/Syntax.hs - compiler/GHC/Iface/Type.hs - compiler/GHC/IfaceToCore.hs - compiler/GHC/Tc/Deriv/Utils.hs - compiler/GHC/Tc/Errors/Ppr.hs - compiler/GHC/Tc/Gen/Sig.hs - compiler/GHC/Tc/Instance/Family.hs - compiler/GHC/Tc/Module.hs - compiler/GHC/Tc/Solver.hs - compiler/GHC/Tc/Solver/Default.hs - compiler/GHC/Tc/Solver/Dict.hs - compiler/GHC/Tc/Solver/Equality.hs - compiler/GHC/Tc/Solver/InertSet.hs - compiler/GHC/Tc/Solver/Monad.hs - compiler/GHC/Tc/Solver/Solve.hs - compiler/GHC/Tc/Solver/Solve.hs-boot - compiler/GHC/Tc/TyCl/Utils.hs - compiler/GHC/Tc/Types/Constraint.hs - compiler/GHC/Tc/Types/Evidence.hs - compiler/GHC/Tc/Types/Origin.hs - compiler/GHC/Tc/Utils/Monad.hs - compiler/GHC/Tc/Utils/TcMType.hs - compiler/GHC/Tc/Utils/TcType.hs - compiler/GHC/Tc/Utils/Unify.hs - compiler/GHC/Tc/Zonk/TcType.hs - compiler/GHC/Tc/Zonk/Type.hs - compiler/GHC/Types/Id/Make.hs - compiler/GHC/Unit/Home/Graph.hs - compiler/GHC/Unit/Home/PackageTable.hs - testsuite/tests/backpack/should_fail/bkpfail11.stderr - testsuite/tests/backpack/should_fail/bkpfail43.stderr - testsuite/tests/deriving/should_fail/T12768.stderr - testsuite/tests/deriving/should_fail/T1496.stderr - testsuite/tests/deriving/should_fail/T21302.stderr - testsuite/tests/deriving/should_fail/T22696b.stderr - testsuite/tests/deriving/should_fail/T5498.stderr - testsuite/tests/deriving/should_fail/T7148.stderr - testsuite/tests/deriving/should_fail/T7148a.stderr - testsuite/tests/impredicative/T17332.stderr - testsuite/tests/quantified-constraints/T19690.stderr - testsuite/tests/quantified-constraints/T19921.stderr - testsuite/tests/quantified-constraints/T21006.stderr - testsuite/tests/roles/should_fail/RolesIArray.stderr - testsuite/tests/simplCore/should_compile/DsSpecPragmas.hs - testsuite/tests/simplCore/should_compile/DsSpecPragmas.stderr - testsuite/tests/simplCore/should_compile/OpaqueNoCastWW.stderr - testsuite/tests/typecheck/should_compile/T14434.hs - + testsuite/tests/typecheck/should_compile/T26154.hs - + testsuite/tests/typecheck/should_compile/T26154_A.hs - + testsuite/tests/typecheck/should_compile/T26154_B.hs - + testsuite/tests/typecheck/should_compile/T26154_B.hs-boot - + testsuite/tests/typecheck/should_compile/T26154_Other.hs - + testsuite/tests/typecheck/should_compile/T26277.hs - + testsuite/tests/typecheck/should_compile/T26376.hs - testsuite/tests/typecheck/should_compile/all.T - testsuite/tests/typecheck/should_fail/T15801.stderr - testsuite/tests/typecheck/should_fail/T19627.stderr - testsuite/tests/typecheck/should_fail/T20666.stderr - testsuite/tests/typecheck/should_fail/T20666a.stderr - testsuite/tests/typecheck/should_fail/T20666b.stderr - testsuite/tests/typecheck/should_fail/T22912.stderr - testsuite/tests/typecheck/should_fail/T23427.stderr The diff was not included because it is too large. View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/9e50a25df9dc8e52d8c0da621756d7… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/9e50a25df9dc8e52d8c0da621756d7… You're receiving this email because of your account on gitlab.haskell.org.

1 0

[Git][ghc/ghc][master] 2 commits: Revert "Remove hptAllFamInstances usage during upsweep"
by Marge Bot (＠marge-bot) 08 Sep '25

08 Sep '25

Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC Commits: 0975d2b6 by sheaf at 2025-09-08T03:38:54-04:00 Revert "Remove hptAllFamInstances usage during upsweep" This reverts commit 3bf6720eff5e86e673568e756161e6d6150eb440. - - - - - 0cf34176 by soulomoon at 2025-09-08T03:38:54-04:00 Family consistency checks: add test for #26154 This commit adds the test T26154, to make sure that GHC doesn't crash when performing type family consistency checks. This test case was extracted from Agda. Fixes #26154 - - - - - 11 changed files: - compiler/GHC/Driver/Env.hs - compiler/GHC/Tc/Instance/Family.hs - compiler/GHC/Tc/Module.hs - compiler/GHC/Unit/Home/Graph.hs - compiler/GHC/Unit/Home/PackageTable.hs - + testsuite/tests/typecheck/should_compile/T26154.hs - + testsuite/tests/typecheck/should_compile/T26154_A.hs - + testsuite/tests/typecheck/should_compile/T26154_B.hs - + testsuite/tests/typecheck/should_compile/T26154_B.hs-boot - + testsuite/tests/typecheck/should_compile/T26154_Other.hs - testsuite/tests/typecheck/should_compile/all.T Changes: ===================================== compiler/GHC/Driver/Env.hs ===================================== @@ -246,7 +246,7 @@ hugCompleteSigsBelow hsc uid mn = foldr (++) [] <$> hugSomeThingsBelowUs (md_complete_matches . hm_details) False hsc uid mn -- | Find instances visible from the given set of imports -hugInstancesBelow :: HscEnv -> UnitId -> ModuleNameWithIsBoot -> IO (InstEnv, [(Module, FamInstEnv)]) +hugInstancesBelow :: HscEnv -> UnitId -> ModuleNameWithIsBoot -> IO (InstEnv, [FamInst]) hugInstancesBelow hsc_env uid mnwib = do let mn = gwib_mod mnwib (insts, famInsts) <- @@ -256,7 +256,7 @@ hugInstancesBelow hsc_env uid mnwib = do -- Don't include instances for the current module in if moduleName (mi_module (hm_iface mod_info)) == mn then [] - else [(md_insts details, [(mi_module $ hm_iface mod_info, extendFamInstEnvList emptyFamInstEnv $ md_fam_insts details)])]) + else [(md_insts details, md_fam_insts details)]) True -- Include -hi-boot hsc_env uid ===================================== compiler/GHC/Tc/Instance/Family.hs ===================================== @@ -286,8 +286,8 @@ why we still do redundant checks. -- We don't need to check the current module, this is done in -- tcExtendLocalFamInstEnv. -- See Note [The type family instance consistency story]. -checkFamInstConsistency :: ModuleEnv FamInstEnv -> [Module] -> TcM () -checkFamInstConsistency hpt_fam_insts directlyImpMods +checkFamInstConsistency :: [Module] -> TcM () +checkFamInstConsistency directlyImpMods = do { (eps, hug) <- getEpsAndHug ; traceTc "checkFamInstConsistency" (ppr directlyImpMods) ; let { -- Fetch the iface of a given module. Must succeed as @@ -317,6 +317,7 @@ checkFamInstConsistency hpt_fam_insts directlyImpMods -- See Note [Order of type family consistency checks] } + ; hpt_fam_insts <- liftIO $ HUG.allFamInstances hug ; debug_consistent_set <- mapM (\x -> (\y -> (x, length y)) <$> modConsistent x) directlyImpMods ; traceTc "init_consistent_set" (ppr debug_consistent_set) ; let init_consistent_set = map fst (reverse (sortOn snd debug_consistent_set)) ===================================== compiler/GHC/Tc/Module.hs ===================================== @@ -119,7 +119,7 @@ import GHC.Core.TyCo.Ppr( debugPprType ) import GHC.Core.TyCo.Tidy( tidyTopType ) import GHC.Core.FamInstEnv ( FamInst, pprFamInst, famInstsRepTyCons, orphNamesOfFamInst - , famInstEnvElts, extendFamInstEnvList, normaliseType, emptyFamInstEnv, unionFamInstEnv ) + , famInstEnvElts, extendFamInstEnvList, normaliseType ) import GHC.Parser.Header ( mkPrelImports ) @@ -464,8 +464,8 @@ tcRnImports hsc_env import_decls = do { (rn_imports, imp_user_spec, rdr_env, imports) <- rnImports import_decls -- Get the default declarations for the classes imported by this module -- and group them by class. - ; tc_defaults <- NE.groupBy ((==) `on` cd_class) . (concatMap defaultList) - <$> tcGetClsDefaults (M.keys $ imp_mods imports) + ; tc_defaults <-(NE.groupBy ((==) `on` cd_class) . (concatMap defaultList)) + <$> tcGetClsDefaults (M.keys $ imp_mods imports) ; this_mod <- getModule ; gbl_env <- getGblEnv ; let unitId = homeUnitId $ hsc_home_unit hsc_env @@ -477,10 +477,8 @@ tcRnImports hsc_env import_decls -- filtering also ensures that we don't see instances from -- modules batch (@--make@) compiled before this one, but -- which are not below this one. - ; (home_insts, home_mod_fam_inst_env) <- liftIO $ + ; (home_insts, home_fam_insts) <- liftIO $ hugInstancesBelow hsc_env unitId mnwib - ; let home_fam_inst_env = foldl' unionFamInstEnv emptyFamInstEnv $ snd <$> home_mod_fam_inst_env - ; let hpt_fam_insts = mkModuleEnv home_mod_fam_inst_env -- We use 'unsafeInterleaveIO' to avoid redundant memory allocations -- See Note [Lazily loading COMPLETE pragmas] from GHC.HsToCore.Monad @@ -506,7 +504,8 @@ tcRnImports hsc_env import_decls tcg_rn_imports = rn_imports, tcg_default = foldMap subsume tc_defaults, tcg_inst_env = tcg_inst_env gbl `unionInstEnv` home_insts, - tcg_fam_inst_env = unionFamInstEnv (tcg_fam_inst_env gbl) home_fam_inst_env + tcg_fam_inst_env = extendFamInstEnvList (tcg_fam_inst_env gbl) + home_fam_insts }) $ do { ; traceRn "rn1" (ppr (imp_direct_dep_mods imports)) @@ -536,7 +535,7 @@ tcRnImports hsc_env import_decls $ imports } ; logger <- getLogger ; withTiming logger (text "ConsistencyCheck"<+>brackets (ppr this_mod)) (const ()) - $ checkFamInstConsistency hpt_fam_insts dir_imp_mods + $ checkFamInstConsistency dir_imp_mods ; traceRn "rn1: } checking family instance consistency" empty ; gbl_env <- getGblEnv ===================================== compiler/GHC/Unit/Home/Graph.hs ===================================== @@ -43,6 +43,7 @@ module GHC.Unit.Home.Graph -- * Very important queries , allInstances + , allFamInstances , allAnns , allCompleteSigs @@ -109,6 +110,10 @@ allInstances hug = foldr go (pure (emptyInstEnv, [])) hug where go hue = liftA2 (\(a,b) (a',b') -> (a `unionInstEnv` a', b ++ b')) (hptAllInstances (homeUnitEnv_hpt hue)) +allFamInstances :: HomeUnitGraph -> IO (ModuleEnv FamInstEnv) +allFamInstances hug = foldr go (pure emptyModuleEnv) hug where + go hue = liftA2 plusModuleEnv (hptAllFamInstances (homeUnitEnv_hpt hue)) + allAnns :: HomeUnitGraph -> IO AnnEnv allAnns hug = foldr go (pure emptyAnnEnv) hug where go hue = liftA2 plusAnnEnv (hptAllAnnotations (homeUnitEnv_hpt hue)) ===================================== compiler/GHC/Unit/Home/PackageTable.hs ===================================== @@ -41,6 +41,7 @@ module GHC.Unit.Home.PackageTable -- * Queries about home modules , hptCompleteSigs , hptAllInstances + , hptAllFamInstances , hptAllAnnotations -- ** More Traversal-based queries @@ -207,6 +208,14 @@ hptAllInstances hpt = do let (insts, famInsts) = unzip hits return (foldl' unionInstEnv emptyInstEnv insts, concat famInsts) +-- | Find all the family instance declarations from the HPT +hptAllFamInstances :: HomePackageTable -> IO (ModuleEnv FamInstEnv) +hptAllFamInstances = fmap mkModuleEnv . concatHpt (\hmi -> [(hmiModule hmi, hmiFamInstEnv hmi)]) + where + hmiModule = mi_module . hm_iface + hmiFamInstEnv = extendFamInstEnvList emptyFamInstEnv + . md_fam_insts . hm_details + -- | All annotations from the HPT hptAllAnnotations :: HomePackageTable -> IO AnnEnv hptAllAnnotations = fmap mkAnnEnv . concatHpt (md_anns . hm_details) ===================================== testsuite/tests/typecheck/should_compile/T26154.hs ===================================== @@ -0,0 +1,5 @@ + +module T26154 where + +import {-# SOURCE #-} T26154_B +import T26154_Other ===================================== testsuite/tests/typecheck/should_compile/T26154_A.hs ===================================== @@ -0,0 +1,9 @@ + +{-# LANGUAGE TypeFamilies #-} + +module T26154_A where + +import {-# SOURCE #-} T26154_B + +type family F a b +type instance F a b = b ===================================== testsuite/tests/typecheck/should_compile/T26154_B.hs ===================================== @@ -0,0 +1,9 @@ +{-# LANGUAGE TypeFamilies #-} + +module T26154_B where + +import T26154_A + +type family FAA a b + +type instance FAA a b = b \ No newline at end of file ===================================== testsuite/tests/typecheck/should_compile/T26154_B.hs-boot ===================================== @@ -0,0 +1,3 @@ +{-# LANGUAGE TypeFamilies #-} + +module T26154_B where ===================================== testsuite/tests/typecheck/should_compile/T26154_Other.hs ===================================== @@ -0,0 +1,7 @@ +{-# LANGUAGE TypeFamilies #-} + +module T26154_Other where + +type family OtherF a b + +type instance OtherF a b = b \ No newline at end of file ===================================== testsuite/tests/typecheck/should_compile/all.T ===================================== @@ -947,6 +947,7 @@ test('T25992', normal, compile, ['']) test('T14010', normal, compile, ['']) test('T26256a', normal, compile, ['']) test('T25992a', normal, compile, ['']) +test('T26154', [extra_files(['T26154_A.hs', 'T26154_B.hs', 'T26154_B.hs-boot', 'T26154_Other.hs'])], multimod_compile, ['T26154', '-v0']) test('T26346', normal, compile, ['']) test('T26358', expect_broken(26358), compile, ['']) test('T26345', normal, compile, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/624afa4a65caa8ec23f85e70574dfb… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/624afa4a65caa8ec23f85e70574dfb… You're receiving this email because of your account on gitlab.haskell.org.

1 0

[Git][ghc/ghc][master] Use tcMkScaledFunTys in matchExpectedFunTys
by Marge Bot (＠marge-bot) 08 Sep '25

08 Sep '25

Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC Commits: 624afa4a by sheaf at 2025-09-08T03:38:05-04:00 Use tcMkScaledFunTys in matchExpectedFunTys We should use tcMkScaledFunTys rather than mkScaledFunTys in GHC.Tc.Utils.Unify.matchExpectedFunTys, as the latter crashes when the kind of the result type is a bare metavariable. We know the result is always Type-like, so we don't need scaledFunTys to try to rediscover that from the kind. Fixes #26277 - - - - - 3 changed files: - compiler/GHC/Tc/Utils/Unify.hs - + testsuite/tests/typecheck/should_compile/T26277.hs - testsuite/tests/typecheck/should_compile/all.T Changes: ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -804,9 +804,13 @@ matchExpectedFunTys herald _ctxt arity (Infer inf_res) thing_inside ; result <- thing_inside (map ExpFunPatTy arg_tys) res_ty ; arg_tys <- mapM (\(Scaled m t) -> Scaled m <$> readExpType t) arg_tys ; res_ty <- readExpType res_ty - -- NB: mkScaledFunTys arg_tys res_ty does not contain any foralls - -- (even nested ones), so no need to instantiate. - ; co <- fillInferResultNoInst (mkScaledFunTys arg_tys res_ty) inf_res + -- Remarks: + -- 1. use tcMkScaledFunTys rather than mkScaledFunTys, as we might + -- have res_ty :: kappa[tau] for a meta ty-var kappa, in which case + -- mkScaledFunTys would crash. See #26277. + -- 2. tcMkScaledFunTys arg_tys res_ty does not contain any foralls + -- (even nested ones), so no need to instantiate. + ; co <- fillInferResultNoInst (tcMkScaledFunTys arg_tys res_ty) inf_res ; return (mkWpCastN co, result) } matchExpectedFunTys herald ctx arity (Check top_ty) thing_inside ===================================== testsuite/tests/typecheck/should_compile/T26277.hs ===================================== @@ -0,0 +1,13 @@ +module T26277 where + +import Data.Kind ( Type, Constraint ) +import GHC.Exts ( TYPE ) + +type FunLike :: forall {k}. (k -> k -> Type) -> Constraint +class FunLike p where + myId :: p a a +instance FunLike (->) where + myId x = x + +-- This caused a panic +test x = myId @(->) x ===================================== testsuite/tests/typecheck/should_compile/all.T ===================================== @@ -907,6 +907,7 @@ test('T22560e', normal, compile, ['']) test('T23514b', normal, compile, ['']) test('T23514c', normal, compile, ['']) test('T22537', normal, compile, ['']) +test('T26277', normal, compile, ['']) test('T18986a', normal, compile, ['']) test('T18986b', normal, compile, ['']) test('T23413', normal, compile, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/624afa4a65caa8ec23f85e70574dfb6… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/624afa4a65caa8ec23f85e70574dfb6… You're receiving this email because of your account on gitlab.haskell.org.

1 0

[Git][ghc/ghc][master] Refactor ForAllCo
by Marge Bot (＠marge-bot) 08 Sep '25

08 Sep '25

Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC Commits: 94b62aa7 by Simon Peyton Jones at 2025-09-08T03:37:14-04:00 Refactor ForAllCo This is a pure refactor, addressing #26389. It arranges that the kind coercion in a ForAllCo is a MCoercion, rather than a plain Coercion, thus removing redundancy in the common case. See (FC8) in Note [ForAllCo] It's a nice cleanup. - - - - - 22 changed files: - compiler/GHC/Core/Coercion.hs - compiler/GHC/Core/Coercion.hs-boot - compiler/GHC/Core/Coercion/Opt.hs - compiler/GHC/Core/Lint.hs - compiler/GHC/Core/Opt/Arity.hs - compiler/GHC/Core/Reduction.hs - compiler/GHC/Core/TyCo/FVs.hs - compiler/GHC/Core/TyCo/Rep.hs - compiler/GHC/Core/TyCo/Subst.hs - compiler/GHC/Core/TyCo/Tidy.hs - compiler/GHC/Core/Type.hs - compiler/GHC/Core/Unify.hs - compiler/GHC/CoreToIface.hs - compiler/GHC/Iface/Rename.hs - compiler/GHC/Iface/Syntax.hs - compiler/GHC/Iface/Type.hs - compiler/GHC/IfaceToCore.hs - compiler/GHC/Tc/TyCl/Utils.hs - compiler/GHC/Tc/Utils/TcMType.hs - compiler/GHC/Tc/Utils/TcType.hs - compiler/GHC/Types/Id/Make.hs - testsuite/tests/simplCore/should_compile/OpaqueNoCastWW.stderr Changes: ===================================== compiler/GHC/Core/Coercion.hs ===================================== @@ -47,7 +47,7 @@ module GHC.Core.Coercion ( mkProofIrrelCo, downgradeRole, mkGReflRightCo, mkGReflLeftCo, mkCoherenceLeftCo, mkCoherenceRightCo, - mkKindCo, + mkKindCo, forAllCoKindCo, castCoercionKind, castCoercionKind1, castCoercionKind2, -- ** Decomposition @@ -66,11 +66,14 @@ module GHC.Core.Coercion ( tyConRoleListX, tyConRoleListRepresentational, funRole, pickLR, - isGReflCo, isReflCo, isReflCo_maybe, isGReflCo_maybe, isReflexiveCo, isReflexiveCo_maybe, - isReflCoVar_maybe, isGReflMCo, mkGReflLeftMCo, mkGReflRightMCo, + isReflKindCo,isReflKindMCo, + isReflCo, isReflCo_maybe, + isReflexiveMCo, isReflexiveCo, isReflexiveCo_maybe, + isReflCoVar_maybe, mkGReflLeftMCo, mkGReflRightMCo, mkCoherenceRightMCo, - coToMCo, mkTransMCo, mkTransMCoL, mkTransMCoR, mkCastTyMCo, mkSymMCo, + coToMCo, kindCoToMKindCo, + mkTransMCo, mkTransMCoL, mkTransMCoR, mkCastTyMCo, mkSymMCo, mkFunResMCo, mkPiMCos, isReflMCo, checkReflexiveMCo, @@ -85,7 +88,7 @@ module GHC.Core.Coercion ( -- ** Substitution CvSubstEnv, emptyCvSubstEnv, lookupCoVar, - substCo, substCos, substCoVar, substCoVars, substCoWith, + substCo, substCos, substCoVar, substCoVars, substCoWithInScope, substCoVarBndr, extendTvSubstAndInScope, getCvSubstEnv, @@ -317,23 +320,23 @@ coToMCo :: Coercion -> MCoercion coToMCo co | isReflCo co = MRefl | otherwise = MCo co +kindCoToMKindCo :: KindCoercion -> KindMCoercion +-- Convert a KindCoercion to a KindMCoercion, +-- coToMCo doesn't eliminate GRefl, but kindCoToMCo can +-- See Note [KindCoercion] +kindCoToMKindCo co | isReflKindCo co = MRefl + | otherwise = MCo co + checkReflexiveMCo :: MCoercion -> MCoercion checkReflexiveMCo MRefl = MRefl checkReflexiveMCo (MCo co) | isReflexiveCo co = MRefl | otherwise = MCo co --- | Tests if this MCoercion is obviously generalized reflexive --- Guaranteed to work very quickly. -isGReflMCo :: MCoercion -> Bool -isGReflMCo MRefl = True -isGReflMCo (MCo co) | isGReflCo co = True -isGReflMCo _ = False - -- | Make a generalized reflexive coercion mkGReflCo :: Role -> Type -> MCoercionN -> Coercion mkGReflCo r ty mco - | isGReflMCo mco = if r == Nominal then Refl ty - else GRefl r ty MRefl + | isReflKindMCo mco = if r == Nominal then Refl ty + else GRefl r ty MRefl | otherwise = -- I'd like to have this assert, but sadly it's not true during type -- inference because the types are not fully zonked @@ -565,10 +568,13 @@ splitFunCo_maybe :: Coercion -> Maybe (Coercion, Coercion) splitFunCo_maybe (FunCo { fco_arg = arg, fco_res = res }) = Just (arg, res) splitFunCo_maybe _ = Nothing -splitForAllCo_maybe :: Coercion -> Maybe (TyCoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion) +splitForAllCo_maybe :: Coercion + -> Maybe (TyCoVar, ForAllTyFlag, ForAllTyFlag, KindCoercion, Coercion) +-- You might think that this function should return KindMCoercion (rather +-- than a KindCoercion), but in fact most of the clients want a KindCoercion. splitForAllCo_maybe (ForAllCo { fco_tcv = tv, fco_visL = vL, fco_visR = vR - , fco_kind = k_co, fco_body = co }) - = Just (tv, vL, vR, k_co, co) + , fco_kind = k_mco, fco_body = co }) + = Just (tv, vL, vR, forAllCoKindCo tv k_mco, co) splitForAllCo_maybe co | Just (ty, r) <- isReflCo_maybe co , Just (Bndr tcv vis, body_ty) <- splitForAllForAllTyBinder_maybe ty @@ -576,7 +582,8 @@ splitForAllCo_maybe co splitForAllCo_maybe _ = Nothing -- | Like 'splitForAllCo_maybe', but only returns Just for tyvar binder -splitForAllCo_ty_maybe :: Coercion -> Maybe (TyVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion) +splitForAllCo_ty_maybe :: Coercion + -> Maybe (TyVar, ForAllTyFlag, ForAllTyFlag, KindCoercion, Coercion) splitForAllCo_ty_maybe co | Just stuff@(tv, _, _, _, _) <- splitForAllCo_maybe co , isTyVar tv @@ -584,7 +591,8 @@ splitForAllCo_ty_maybe co splitForAllCo_ty_maybe _ = Nothing -- | Like 'splitForAllCo_maybe', but only returns Just for covar binder -splitForAllCo_co_maybe :: Coercion -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion) +splitForAllCo_co_maybe :: Coercion + -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, KindCoercion, Coercion) splitForAllCo_co_maybe co | Just stuff@(cv, _, _, _, _) <- splitForAllCo_maybe co , isCoVar cv @@ -676,34 +684,50 @@ isReflCoVar_maybe cv | otherwise = Nothing --- | Tests if this coercion is obviously a generalized reflexive coercion. +-- | Tests whether this is a "kind coercion": +-- that is, Nominal and between two types of kind @Type@. +-- See Note [KindCoercion] in GHC.Core.TyCo.Rep +isKindCo :: Coercion -> Bool +isKindCo co + = role == Nominal && isLiftedTypeKind kk1 && isLiftedTypeKind kk2 + where + (Pair kk1 kk2, role) = coercionKindRole co + +-- | Tests if this /kind/ coercion is Refl +-- Guaranteed to work very quickly. +-- PRECONDITION: the argument is a KindCoercion +-- So if it sees (GRefl k (MCo kk)) :: k ~ (k |> kk) +-- then we know that kk must be reflexive. +-- And hence if co = GRefl {} then it is equivalent to Refl, +-- because GRefl N ty MRefl = Refl ty +-- so we return True +-- See Note [KindCoercion] in GHC.Core.TyCo.Rep +isReflKindCo :: HasDebugCallStack => KindCoercion -> Bool +isReflKindCo co@(GRefl {}) = assertPpr (isKindCo co) (ppr co) $ + True +isReflKindCo (Refl{}) = True -- Refl ty == GRefl N ty MRefl +isReflKindCo _ = False + +-- | Tests if this /kind/ MCoercion is obviously generalized reflexive -- Guaranteed to work very quickly. -isGReflCo :: Coercion -> Bool -isGReflCo (GRefl{}) = True -isGReflCo (Refl{}) = True -- Refl ty == GRefl N ty MRefl -isGReflCo _ = False +isReflKindMCo :: KindMCoercion -> Bool +isReflKindMCo MRefl = True +isReflKindMCo (MCo co) = isReflKindCo co -- | Tests if this coercion is obviously reflexive. Guaranteed to work -- very quickly. Sometimes a coercion can be reflexive, but not obviously -- so. c.f. 'isReflexiveCo' isReflCo :: Coercion -> Bool isReflCo (Refl{}) = True -isReflCo (GRefl _ _ mco) | isGReflMCo mco = True +isReflCo (GRefl _ _ mco) | isReflKindMCo mco = True isReflCo _ = False --- | Returns the type coerced if this coercion is a generalized reflexive --- coercion. Guaranteed to work very quickly. -isGReflCo_maybe :: Coercion -> Maybe (Type, Role) -isGReflCo_maybe (GRefl r ty _) = Just (ty, r) -isGReflCo_maybe (Refl ty) = Just (ty, Nominal) -isGReflCo_maybe _ = Nothing - -- | Returns the type coerced if this coercion is reflexive. Guaranteed -- to work very quickly. Sometimes a coercion can be reflexive, but not -- obviously so. c.f. 'isReflexiveCo_maybe' isReflCo_maybe :: Coercion -> Maybe (Type, Role) isReflCo_maybe (Refl ty) = Just (ty, Nominal) -isReflCo_maybe (GRefl r ty mco) | isGReflMCo mco = Just (ty, r) +isReflCo_maybe (GRefl r ty mco) | isReflKindMCo mco = Just (ty, r) isReflCo_maybe _ = Nothing -- | Slowly checks if the coercion is reflexive. Don't call this in a loop, @@ -711,11 +735,15 @@ isReflCo_maybe _ = Nothing isReflexiveCo :: Coercion -> Bool isReflexiveCo = isJust . isReflexiveCo_maybe +isReflexiveMCo :: MCoercion -> Bool +isReflexiveMCo MRefl = True +isReflexiveMCo (MCo co) = isReflexiveCo co + -- | Extracts the coerced type from a reflexive coercion. This potentially -- walks over the entire coercion, so avoid doing this in a loop. isReflexiveCo_maybe :: Coercion -> Maybe (Type, Role) isReflexiveCo_maybe (Refl ty) = Just (ty, Nominal) -isReflexiveCo_maybe (GRefl r ty mco) | isGReflMCo mco = Just (ty, r) +isReflexiveCo_maybe (GRefl r ty mco) | isReflKindMCo mco = Just (ty, r) isReflexiveCo_maybe co | ty1 `eqType` ty2 = Just (ty1, r) @@ -723,6 +751,10 @@ isReflexiveCo_maybe co = Nothing where (Pair ty1 ty2, r) = coercionKindRole co +forAllCoKindCo :: TyCoVar -> KindMCoercion -> KindCoercion +-- Get the kind coercion from a ForAllCo +forAllCoKindCo _ (MCo co) = co +forAllCoKindCo tcv MRefl = mkNomReflCo (varType tcv) {- %************************************************************************ @@ -939,10 +971,11 @@ mkAppCos co1 cos = foldl' mkAppCo co1 cos -- | Make a Coercion from a tycovar, a kind coercion, and a body coercion. -mkForAllCo :: HasDebugCallStack => TyCoVar -> ForAllTyFlag -> ForAllTyFlag -> CoercionN -> Coercion -> Coercion +mkForAllCo :: HasDebugCallStack => TyCoVar -> ForAllTyFlag -> ForAllTyFlag + -> KindMCoercion -> Coercion -> Coercion mkForAllCo v visL visR kind_co co | Just (ty, r) <- isReflCo_maybe co - , isReflCo kind_co + , isReflMCo kind_co , visL `eqForAllVis` visR = mkReflCo r (mkTyCoForAllTy v visL ty) @@ -955,8 +988,7 @@ mkForAllCo v visL visR kind_co co mkForAllVisCos :: HasDebugCallStack => [ForAllTyBinder] -> Coercion -> Coercion mkForAllVisCos bndrs orig_co = foldr go orig_co bndrs where - go (Bndr tv vis) - = mkForAllCo tv coreTyLamForAllTyFlag vis (mkNomReflCo (varType tv)) + go (Bndr tv vis) = mkForAllCo tv coreTyLamForAllTyFlag vis MRefl -- | Make a Coercion quantified over a type/coercion variable; -- the variable has the same kind and visibility in both sides of the coercion @@ -967,29 +999,30 @@ mkHomoForAllCos vs orig_co | otherwise = foldr go orig_co vs where - go (Bndr var vis) co - = mkForAllCo_NoRefl var vis vis (mkNomReflCo (varType var)) co + go :: ForAllTyBinder -> Coercion -> Coercion + go (Bndr var vis) = mkForAllCo_NoRefl var vis vis MRefl -- | Like 'mkForAllCo', but there is no need to check that the inner coercion isn't Refl; -- the caller has done that. (For example, it is guaranteed in 'mkHomoForAllCos'.) -- The kind of the tycovar should be the left-hand kind of the kind coercion. -mkForAllCo_NoRefl :: TyCoVar -> ForAllTyFlag -> ForAllTyFlag -> CoercionN -> Coercion -> Coercion +mkForAllCo_NoRefl :: TyCoVar -> ForAllTyFlag -> ForAllTyFlag + -> KindMCoercion -> Coercion -> Coercion mkForAllCo_NoRefl tcv visL visR kind_co co = assertGoodForAllCo tcv visL visR kind_co co $ - assertPpr (not (isReflCo co && isReflCo kind_co && visL == visR)) (ppr co) $ + assertPpr (not (isReflCo co && isReflMCo kind_co && visL == visR)) (ppr co) $ ForAllCo { fco_tcv = tcv, fco_visL = visL, fco_visR = visR , fco_kind = kind_co, fco_body = co } assertGoodForAllCo :: HasDebugCallStack - => TyCoVar -> ForAllTyFlag -> ForAllTyFlag - -> CoercionN -> Coercion -> a -> a + => TyCoVar -> ForAllTyFlag -> ForAllTyFlag + -> KindMCoercion -> Coercion -> a -> a -- Check ForAllCo invariants; see Note [ForAllCo] in GHC.Core.TyCo.Rep assertGoodForAllCo tcv visL visR kind_co co | isTyVar tcv - = assertPpr (tcv_type `eqType` kind_co_lkind) doc + = assertPpr tcv_kind_co_agree doc | otherwise - = assertPpr (tcv_type `eqType` kind_co_lkind) doc + = assertPpr tcv_kind_co_agree doc -- The kind of the tycovar should be the left-hand kind of the kind coercion. . assertPpr (almostDevoidCoVarOfCo tcv co) doc -- See (FC6) in Note [ForAllCo] in GHC.Core.TyCo.Rep @@ -998,13 +1031,17 @@ assertGoodForAllCo tcv visL visR kind_co co -- See (FC7) in Note [ForAllCo] in GHC.Core.TyCo.Rep where tcv_type = varType tcv - kind_co_lkind = coercionLKind kind_co + tcv_kind_co_agree = case kind_co of + MRefl -> True + MCo co -> tcv_type `eqType` coercionLKind co doc = vcat [ text "Var:" <+> ppr tcv <+> dcolon <+> ppr tcv_type , text "Vis:" <+> ppr visL <+> ppr visR - , text "kind_co:" <+> ppr kind_co - , text "kind_co_lkind" <+> ppr kind_co_lkind + , text "kind_co:" <+> pp_kind_co , text "body_co" <+> ppr co ] + pp_kind_co = case kind_co of + MRefl -> text "MRefl" + MCo co -> ppr co <+> dcolon <+> ppr (coercionKind co) mkNakedForAllCo :: TyVar -- Never a CoVar @@ -1024,7 +1061,7 @@ mkNakedForAllCo tv visL visR kind_co co = mkReflCo r (mkForAllTy (Bndr tv visL) ty) | otherwise = ForAllCo { fco_tcv = tv, fco_visL = visL, fco_visR = visR - , fco_kind = kind_co, fco_body = co } + , fco_kind = MCo kind_co, fco_body = co } mkCoVarCo :: CoVar -> Coercion @@ -1149,7 +1186,7 @@ mkSymCo co | isReflCo co = co mkSymCo (SymCo co) = co mkSymCo (SubCo (SymCo co)) = SubCo co mkSymCo co@(ForAllCo { fco_kind = kco, fco_body = body_co }) - | isReflCo kco = co { fco_body = mkSymCo body_co } + | isReflMCo kco = co { fco_body = mkSymCo body_co } mkSymCo co = SymCo co -- | mkTransCo creates a new 'Coercion' by composing the two @@ -1193,8 +1230,8 @@ mkSelCo_maybe cs co go cs co where - go SelForAll (ForAllCo { fco_kind = kind_co }) - = Just kind_co + go SelForAll (ForAllCo { fco_tcv = tcv, fco_kind = kind_co }) + = Just (forAllCoKindCo tcv kind_co) -- If co :: (forall a1:k1. t1) ~ (forall a2:k2. t2) -- then (nth SelForAll co :: k1 ~N k2) -- If co :: (forall a1:t1 ~ t2. t1) ~ (forall a2:t3 ~ t4. t2) @@ -1312,46 +1349,45 @@ mkInstCo :: Coercion -> CoercionN -> Coercion mkInstCo co_fun co_arg | Just (tcv, _, _, kind_co, body_co) <- splitForAllCo_maybe co_fun , Just (arg, _) <- isReflCo_maybe co_arg + , let in_scope = mkInScopeSet $ + tyCoVarsOfType arg `unionVarSet` tyCoVarsOfCo body_co + subst = extendTCvSubst (mkEmptySubst in_scope) tcv arg = assertPpr (isReflexiveCo kind_co) (ppr co_fun $$ ppr co_arg) $ -- If the arg is Refl, then kind_co must be reflexive too - substCoUnchecked (zipTCvSubst [tcv] [arg]) body_co + substCo subst body_co mkInstCo co arg = InstCo co arg -- | Given @ty :: k1@, @co :: k1 ~ k2@, -- produces @co' :: ty ~r (ty |> co)@ -mkGReflRightCo :: Role -> Type -> CoercionN -> Coercion +mkGReflRightCo :: Role -> Type -> KindCoercion -> Coercion mkGReflRightCo r ty co - | isGReflCo co = mkReflCo r ty - -- the kinds of @k1@ and @k2@ are the same, thus @isGReflCo@ - -- instead of @isReflCo@ - | otherwise = mkGReflMCo r ty co + | isReflKindCo co = mkReflCo r ty -- Homo (tested) AND nominal (I promise) => Refl + | otherwise = mkGReflMCo r ty co -- | Given @r@, @ty :: k1@, and @co :: k1 ~N k2@, -- produces @co' :: (ty |> co) ~r ty@ -mkGReflLeftCo :: Role -> Type -> CoercionN -> Coercion +mkGReflLeftCo :: Role -> Type -> KindCoercion -> Coercion mkGReflLeftCo r ty co - | isGReflCo co = mkReflCo r ty - -- the kinds of @k1@ and @k2@ are the same, thus @isGReflCo@ - -- instead of @isReflCo@ - | otherwise = mkSymCo $ mkGReflMCo r ty co + | isReflKindCo co = mkReflCo r ty + | otherwise = mkSymCo $ mkGReflMCo r ty co -- | Given @ty :: k1@, @co :: k1 ~ k2@, @co2:: ty ~r ty'@, -- produces @co' :: (ty |> co) ~r ty' -- It is not only a utility function, but it saves allocation when co -- is a GRefl coercion. -mkCoherenceLeftCo :: Role -> Type -> CoercionN -> Coercion -> Coercion +mkCoherenceLeftCo :: Role -> Type -> KindCoercion -> Coercion -> Coercion mkCoherenceLeftCo r ty co co2 - | isGReflCo co = co2 - | otherwise = (mkSymCo $ mkGReflMCo r ty co) `mkTransCo` co2 + | isReflKindCo co = co2 + | otherwise = (mkSymCo $ mkGReflMCo r ty co) `mkTransCo` co2 -- | Given @ty :: k1@, @co :: k1 ~ k2@, @co2:: ty' ~r ty@, -- produces @co' :: ty' ~r (ty |> co) -- It is not only a utility function, but it saves allocation when co -- is a GRefl coercion. -mkCoherenceRightCo :: HasDebugCallStack => Role -> Type -> CoercionN -> Coercion -> Coercion +mkCoherenceRightCo :: HasDebugCallStack => Role -> Type -> KindCoercion -> Coercion -> Coercion mkCoherenceRightCo r ty co co2 - | isGReflCo co = co2 - | otherwise = co2 `mkTransCo` mkGReflMCo r ty co + | isReflKindCo co = co2 + | otherwise = co2 `mkTransCo` mkGReflMCo r ty co -- | Given @co :: (a :: k) ~ (b :: k')@ produce @co' :: k ~ k'@. mkKindCo :: Coercion -> Coercion @@ -1411,18 +1447,19 @@ downgradeRole r1 r2 co Nothing -> pprPanic "downgradeRole" (ppr co) -- | Make a "coercion between coercions". -mkProofIrrelCo :: Role -- ^ role of the created coercion, "r" - -> CoercionN -- ^ :: phi1 ~N phi2 - -> Coercion -- ^ g1 :: phi1 - -> Coercion -- ^ g2 :: phi2 - -> Coercion -- ^ :: g1 ~r g2 +mkProofIrrelCo :: Role -- ^ role of the created coercion, "r" + -> KindCoercion -- ^ :: phi1 ~N phi2 + -> Coercion -- ^ g1 :: phi1 + -> Coercion -- ^ g2 :: phi2 + -> Coercion -- ^ :: g1 ~r g2 -- if the two coercion prove the same fact, I just don't care what -- the individual coercions are. -mkProofIrrelCo r co g _ | isGReflCo co = mkReflCo r (mkCoercionTy g) - -- kco is a kind coercion, thus @isGReflCo@ rather than @isReflCo@ -mkProofIrrelCo r kco g1 g2 = mkUnivCo ProofIrrelProv [kco] r - (mkCoercionTy g1) (mkCoercionTy g2) +mkProofIrrelCo r kco g1 g2 + | isReflKindCo kco = mkReflCo r (mkCoercionTy g1) + -- kco is a kind coercion, thus @isReflKindCo@ rather than @isReflCo@ + | otherwise = mkUnivCo ProofIrrelProv [kco] r + (mkCoercionTy g1) (mkCoercionTy g2) {- %************************************************************************ @@ -2165,16 +2202,17 @@ ty_co_subst !lc role ty go r (TyConApp tc tys) = mkTyConAppCo r tc (zipWith go (tyConRoleListX r tc) tys) go r (FunTy af w t1 t2) = mkFunCo r af (go Nominal w) (go r t1) (go r t2) go r t@(ForAllTy (Bndr v vis) ty) - = let (lc', v', h) = liftCoSubstVarBndr lc v - body_co = ty_co_subst lc' r ty in - if isTyVar v' || almostDevoidCoVarOfCo v' body_co + = let (lc', v', k_co) = liftCoSubstVarBndr lc v + body_co = ty_co_subst lc' r ty + k_mco = kindCoToMKindCo k_co + in if isTyVar v' || almostDevoidCoVarOfCo v' body_co -- Lifting a ForAllTy over a coercion variable could fail as ForAllCo -- imposes an extra restriction on where a covar can appear. See -- (FC6) of Note [ForAllCo] in GHC.Tc.TyCo.Rep -- We specifically check for this and panic because we know that -- there's a hole in the type system here (see (FC6), and we'd rather -- panic than fall into it. - then mkForAllCo v' vis vis h body_co + then mkForAllCo v' vis vis k_mco body_co else pprPanic "ty_co_subst: covar is not almost devoid" (ppr t) go r ty@(LitTy {}) = assert (r == Nominal) $ mkNomReflCo ty @@ -2262,6 +2300,7 @@ liftCoSubstVarBndr :: LiftingContext -> TyCoVar liftCoSubstVarBndr lc tv = liftCoSubstVarBndrUsing id callback lc tv where + callback :: LiftingContext -> Type -> Coercion callback lc' ty' = ty_co_subst lc' Nominal ty' -- the callback must produce a nominal coercion @@ -2424,7 +2463,7 @@ seqCo (SubCo co) = seqCo co seqCo (AxiomCo _ cs) = seqCos cs seqCo (ForAllCo tv visL visR k co) = seqType (varType tv) `seq` rnf visL `seq` rnf visR `seq` - seqCo k `seq` seqCo co + seqMCo k `seq` seqCo co seqCo (FunCo r af1 af2 w co1 co2) = r `seq` af1 `seq` af2 `seq` seqCo w `seq` seqCo co1 `seq` seqCo co2 seqCo (UnivCo { uco_prov = p, uco_role = r @@ -2522,7 +2561,7 @@ coercion_lr_kind which orig_co , fco_kind = k_co, fco_body = co1 }) = case which of CLeft -> mkTyCoForAllTy tv1 visL (go co1) - CRight | isGReflCo k_co -- kind_co always has kind `Type`, thus `isGReflCo` + CRight | isReflKindMCo k_co -> mkTyCoForAllTy tv1 visR (go co1) | otherwise -> go_forall_right empty_subst co @@ -2577,43 +2616,47 @@ coercion_lr_kind which orig_co ------------- go_forall_right subst (ForAllCo { fco_tcv = tv1, fco_visR = visR - , fco_kind = k_co, fco_body = co }) + , fco_kind = k_mco, fco_body = co }) -- See Note [Nested ForAllCos] | isTyVar tv1 - = mkForAllTy (Bndr tv2 visR) (go_forall_right subst' co) - where - k2 = coercionRKind k_co - tv2 = setTyVarKind tv1 (substTy subst k2) - subst' | isGReflCo k_co = extendSubstInScope subst tv1 - -- kind_co always has kind @Type@, thus @isGReflCo@ - | otherwise = extendTvSubst (extendSubstInScope subst tv2) tv1 $ - TyVarTy tv2 `mkCastTy` mkSymCo k_co + = case k_mco of + MRefl -> mkForAllTy (Bndr tv1 visR) (go_forall_right subst' co) + where + subst' = extendSubstInScope subst tv1 + MCo k_co -> mkForAllTy (Bndr tv2 visR) (go_forall_right subst' co) + where + k2 = coercionRKind k_co + tv2 = setTyVarKind tv1 (substTy subst k2) + subst' = extendTvSubst (extendSubstInScope subst tv2) tv1 $ + TyVarTy tv2 `mkCastTy` mkSymCo k_co go_forall_right subst (ForAllCo { fco_tcv = cv1, fco_visR = visR - , fco_kind = k_co, fco_body = co }) + , fco_kind = k_mco, fco_body = co }) | isCoVar cv1 - = mkTyCoForAllTy cv2 visR (go_forall_right subst' co) - where - k2 = coercionRKind k_co - r = coVarRole cv1 - k_co' = downgradeRole r Nominal k_co - eta1 = mkSelCo (SelTyCon 2 r) k_co' - eta2 = mkSelCo (SelTyCon 3 r) k_co' - - -- k_co :: (t1 ~r t2) ~N (s1 ~r s2) - -- k1 = t1 ~r t2 - -- k2 = s1 ~r s2 - -- cv1 :: t1 ~r t2 - -- cv2 :: s1 ~r s2 - -- eta1 :: t1 ~r s1 - -- eta2 :: t2 ~r s2 - -- n_subst = (eta1 ; cv2 ; sym eta2) :: t1 ~r t2 - - cv2 = setVarType cv1 (substTy subst k2) - n_subst = eta1 `mkTransCo` (mkCoVarCo cv2) `mkTransCo` (mkSymCo eta2) - subst' | isReflCo k_co = extendSubstInScope subst cv1 - | otherwise = extendCvSubst (extendSubstInScope subst cv2) - cv1 n_subst + = case k_mco of + MRefl -> mkTyCoForAllTy cv1 visR (go_forall_right subst' co) + where + subst' = extendSubstInScope subst cv1 + MCo k_co -> mkTyCoForAllTy cv2 visR (go_forall_right subst' co) + where + k2 = coercionRKind k_co + r = coVarRole cv1 + k_co' = downgradeRole r Nominal k_co + eta1 = mkSelCo (SelTyCon 2 r) k_co' + eta2 = mkSelCo (SelTyCon 3 r) k_co' + + -- k_co :: (t1 ~r t2) ~N (s1 ~r s2) + -- k1 = t1 ~r t2 + -- k2 = s1 ~r s2 + -- cv1 :: t1 ~r t2 + -- cv2 :: s1 ~r s2 + -- eta1 :: t1 ~r s1 + -- eta2 :: t2 ~r s2 + -- n_subst = (eta1 ; cv2 ; sym eta2) :: t1 ~r t2 + + cv2 = setVarType cv1 (substTy subst k2) + n_subst = eta1 `mkTransCo` (mkCoVarCo cv2) `mkTransCo` (mkSymCo eta2) + subst' = extendCvSubst (extendSubstInScope subst cv2) cv1 n_subst go_forall_right subst other_co -- when other_co is not a ForAllCo @@ -2729,7 +2772,7 @@ buildCoercion orig_ty1 orig_ty2 = go orig_ty1 orig_ty2 go (ForAllTy (Bndr tv1 flag1) ty1) (ForAllTy (Bndr tv2 flag2) ty2) | isTyVar tv1 = assert (isTyVar tv2) $ - mkForAllCo tv1 flag1 flag2 kind_co (go ty1 ty2') + mkForAllCo tv1 flag1 flag2 (kindCoToMKindCo kind_co) (go ty1 ty2') where kind_co = go (tyVarKind tv1) (tyVarKind tv2) in_scope = mkInScopeSet $ tyCoVarsOfType ty2 `unionVarSet` tyCoVarsOfCo kind_co ty2' = substTyWithInScope in_scope [tv2] @@ -2738,7 +2781,7 @@ buildCoercion orig_ty1 orig_ty2 = go orig_ty1 orig_ty2 go (ForAllTy (Bndr cv1 flag1) ty1) (ForAllTy (Bndr cv2 flag2) ty2) = assert (isCoVar cv1 && isCoVar cv2) $ - mkForAllCo cv1 flag1 flag2 kind_co (go ty1 ty2') + mkForAllCo cv1 flag1 flag2 (kindCoToMKindCo kind_co) (go ty1 ty2') where s1 = varType cv1 s2 = varType cv2 kind_co = go s1 s2 @@ -2755,7 +2798,7 @@ buildCoercion orig_ty1 orig_ty2 = go orig_ty1 orig_ty2 eta2 = mkSelCo (SelTyCon 3 r) kind_co' subst = mkEmptySubst $ mkInScopeSet $ - tyCoVarsOfType ty2 `unionVarSet` tyCoVarsOfCo kind_co + tyCoVarsOfType ty2 `unionVarSet` tyCoVarsOfCo kind_co ty2' = substTy (extendCvSubst subst cv2 $ mkSymCo eta1 `mkTransCo` mkCoVarCo cv1 `mkTransCo` eta2) ===================================== compiler/GHC/Core/Coercion.hs-boot ===================================== @@ -16,7 +16,7 @@ import GHC.Utils.Misc mkReflCo :: Role -> Type -> Coercion mkTyConAppCo :: HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion mkAppCo :: Coercion -> Coercion -> Coercion -mkForAllCo :: HasDebugCallStack => TyCoVar -> ForAllTyFlag -> ForAllTyFlag -> Coercion -> Coercion -> Coercion +mkForAllCo :: HasDebugCallStack => TyCoVar -> ForAllTyFlag -> ForAllTyFlag -> MCoercion -> Coercion -> Coercion mkFunCo :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion mkNakedFunCo :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion mkFunCo2 :: Role -> FunTyFlag -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion @@ -37,7 +37,6 @@ mkAxiomCo :: CoAxiomRule -> [Coercion] -> Coercion funRole :: Role -> FunSel -> Role -isGReflCo :: Coercion -> Bool isReflCo :: Coercion -> Bool isReflexiveCo :: Coercion -> Bool decomposePiCos :: HasDebugCallStack => Coercion -> Pair Type -> [Type] -> ([Coercion], Coercion) ===================================== compiler/GHC/Core/Coercion/Opt.hs ===================================== @@ -177,12 +177,12 @@ optCoercion opts env co = optCoercion' env co {- - = pprTrace "optCoercion {" (text "Co:" <> ppr (coercionSize co)) $ + = pprTrace "optCoercion {" (text "Co:" <> ppr co) $ let result = optCoercion' env co in pprTrace "optCoercion }" (vcat [ text "Co:" <+> ppr (coercionSize co) , text "Optco:" <+> ppWhen (isReflCo result) (text "(refl)") - <+> ppr (coercionSize result) ]) $ + <+> ppr result ]) $ result -} @@ -317,7 +317,7 @@ opt_co4' env sym rep r (GRefl _r ty (MCo kco)) (text "Expected role:" <+> ppr r $$ text "Found role:" <+> ppr _r $$ text "Type:" <+> ppr ty) $ - if isGReflCo kco || isGReflCo kco' + if isReflKindCo kco || isReflKindCo kco' then wrapSym sym ty_co else wrapSym sym $ mk_coherence_right_co r' (coercionRKind ty_co) kco' ty_co -- ty :: k1 @@ -841,55 +841,58 @@ opt_trans_rule is co1 co2@(AppCo co2a co2b) -- Push transitivity inside forall -- forall over types. opt_trans_rule is co1 co2 - | Just (tv1, visL1, _visR1, eta1, r1) <- splitForAllCo_ty_maybe co1 - , Just (tv2, _visL2, visR2, eta2, r2) <- etaForAllCo_ty_maybe co2 - = push_trans tv1 eta1 r1 tv2 eta2 r2 visL1 visR2 + | Just (tv1, visL1, _visR1, kco1, r1) <- splitForAllCo_ty_maybe co1 + , Just (tv2, _visL2, visR2, kco2, r2) <- etaForAllCo_ty_maybe co2 + = push_trans tv1 kco1 r1 tv2 kco2 r2 visL1 visR2 - | Just (tv2, _visL2, visR2, eta2, r2) <- splitForAllCo_ty_maybe co2 - , Just (tv1, visL1, _visR1, eta1, r1) <- etaForAllCo_ty_maybe co1 - = push_trans tv1 eta1 r1 tv2 eta2 r2 visL1 visR2 + | Just (tv2, _visL2, visR2, kco2, r2) <- splitForAllCo_ty_maybe co2 + , Just (tv1, visL1, _visR1, kco1, r1) <- etaForAllCo_ty_maybe co1 + = push_trans tv1 kco1 r1 tv2 kco2 r2 visL1 visR2 where - push_trans tv1 eta1 r1 tv2 eta2 r2 visL visR + push_trans tv1 kco1 r1 tv2 kco2 r2 visL visR -- Given: - -- co1 = /\ tv1 : eta1 <visL, visM>. r1 - -- co2 = /\ tv2 : eta2 <visM, visR>. r2 + -- co1 = /\ tv1 : kco1 <visL, visM>. r1 + -- co2 = /\ tv2 : kco2 <visM, visR>. r2 -- Wanted: - -- /\tv1 : (eta1;eta2) <visL, visR>. (r1; r2[tv2 |-> tv1 |> eta1]) + -- /\tv1 : (kco1;kco2) <visL, visR>. (r1; r2[tv2 |-> tv1 |> kco1]) = fireTransRule "EtaAllTy_ty" co1 co2 $ - mkForAllCo tv1 visL visR (opt_trans is eta1 eta2) (opt_trans is' r1 r2') + mkForAllCo tv1 visL visR + (kindCoToMKindCo (opt_trans is kco1 kco2)) + (opt_trans is' r1 r2') where is' = is `extendInScopeSet` tv1 - r2' = substCoWithUnchecked [tv2] [mkCastTy (TyVarTy tv1) eta1] r2 + r2' = substCoWithInScope is' [tv2] [mkCastTy (TyVarTy tv1) kco1] r2 -- Push transitivity inside forall -- forall over coercions. opt_trans_rule is co1 co2 - | Just (cv1, visL1, _visR1, eta1, r1) <- splitForAllCo_co_maybe co1 - , Just (cv2, _visL2, visR2, eta2, r2) <- etaForAllCo_co_maybe co2 - = push_trans cv1 eta1 r1 cv2 eta2 r2 visL1 visR2 + | Just (cv1, visL1, _visR1, kco1, r1) <- splitForAllCo_co_maybe co1 + , Just (cv2, _visL2, visR2, kco2, r2) <- etaForAllCo_co_maybe co2 + = push_trans cv1 kco1 r1 cv2 kco2 r2 visL1 visR2 - | Just (cv2, _visL2, visR2, eta2, r2) <- splitForAllCo_co_maybe co2 - , Just (cv1, visL1, _visR1, eta1, r1) <- etaForAllCo_co_maybe co1 - = push_trans cv1 eta1 r1 cv2 eta2 r2 visL1 visR2 + | Just (cv2, _visL2, visR2, kco2, r2) <- splitForAllCo_co_maybe co2 + , Just (cv1, visL1, _visR1, kco1, r1) <- etaForAllCo_co_maybe co1 + = push_trans cv1 kco1 r1 cv2 kco2 r2 visL1 visR2 where - push_trans cv1 eta1 r1 cv2 eta2 r2 visL visR + push_trans cv1 kco1 r1 cv2 kco2 r2 visL visR -- Given: - -- co1 = /\ (cv1 : eta1) <visL, visM>. r1 - -- co2 = /\ (cv2 : eta2) <visM, visR>. r2 + -- co1 = /\ (cv1 : kco1) <visL, visM>. r1 + -- co2 = /\ (cv2 : kco2) <visM, visR>. r2 -- Wanted: - -- n1 = nth 2 eta1 - -- n2 = nth 3 eta1 - -- nco = /\ cv1 : (eta1;eta2). (r1; r2[cv2 |-> (sym n1);cv1;n2]) + -- n1 = nth 2 kco1 + -- n2 = nth 3 kco1 + -- nco = /\ cv1 : (kco1;kco2). (r1; r2[cv2 |-> (sym n1);cv1;n2]) = fireTransRule "EtaAllTy_co" co1 co2 $ - mkForAllCo cv1 visL visR (opt_trans is eta1 eta2) (opt_trans is' r1 r2') + mkForAllCo cv1 visL visR (coToMCo (opt_trans is kco1 kco2)) + (opt_trans is' r1 r2') where is' = is `extendInScopeSet` cv1 role = coVarRole cv1 - eta1' = downgradeRole role Nominal eta1 - n1 = mkSelCo (SelTyCon 2 role) eta1' - n2 = mkSelCo (SelTyCon 3 role) eta1' + kco1' = downgradeRole role Nominal kco1 + n1 = mkSelCo (SelTyCon 2 role) kco1' + n2 = mkSelCo (SelTyCon 3 role) kco1' r2' = substCo (zipCvSubst [cv2] [(mkSymCo n1) `mk_trans_co` (mkCoVarCo cv1) `mk_trans_co` n2]) r2 @@ -1285,7 +1288,8 @@ Here, eta2 = mkSelCo (SelTyCon 3 r) h1 :: (s2 ~ s4) h2 = mkInstCo g (cv1 ~ (sym eta1;c1;eta2)) -} -etaForAllCo_ty_maybe :: Coercion -> Maybe (TyVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion) +etaForAllCo_ty_maybe :: Coercion + -> Maybe (TyVar, ForAllTyFlag, ForAllTyFlag, KindCoercion, Coercion) -- Try to make the coercion be of form (forall tv:kind_co. co) etaForAllCo_ty_maybe co | Just (tv, visL, visR, kind_co, r) <- splitForAllCo_ty_maybe co @@ -1305,7 +1309,8 @@ etaForAllCo_ty_maybe co | otherwise = Nothing -etaForAllCo_co_maybe :: Coercion -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion) +etaForAllCo_co_maybe :: Coercion + -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, KindCoercion, Coercion) -- Try to make the coercion be of form (forall cv:kind_co. co) etaForAllCo_co_maybe co | Just (cv, visL, visR, kind_co, r) <- splitForAllCo_co_maybe co @@ -1428,13 +1433,17 @@ But if sym=Swapped, things are trickier. Here is an identity that helps: -} optForAllCoBndr :: LiftingContext -> SwapFlag - -> TyCoVar -> Coercion - -> (LiftingContext, TyCoVar, Coercion) + -> TyCoVar -> MCoercionN + -> (LiftingContext, TyCoVar, MCoercionN) -- See Note [Optimising ForAllCo] -optForAllCoBndr env sym tcv kco - = (env', tcv', kco') +optForAllCoBndr env sym tcv k_mco + = (env', tcv', k_mco') where - kco' = opt_co4 env sym False Nominal kco -- Push sym into kco + -- Push sym into kco + k_mco' = case k_mco of + MRefl -> MRefl + MCo co -> MCo (opt_co4 env sym False Nominal co) + (env', tcv') = updateLCSubst env upd_subst upd_subst :: Subst -> (Subst, TyCoVar) @@ -1443,26 +1452,32 @@ optForAllCoBndr env sym tcv kco | otherwise = upd_subst_cv subst upd_subst_tv subst - | notSwapped sym || isReflCo kco' = (subst1, tv1) - | otherwise = (subst2, tv2) + = case k_mco' of + MCo k_co' | isSwapped sym -> (subst2, tv2) + where + -- In the Swapped case, we re-kind the type variable, AND + -- override the substitution for the original variable to the + -- re-kinded one, suitably casted + tv2 = tv1 `setTyVarKind` coercionLKind k_co' + subst2 = (extendTvSubst subst1 tcv (mkTyVarTy tv2 `CastTy` k_co')) + `extendSubstInScope` tv2 + + _ -> (subst1, tv1) where -- subst1,tv1: apply the substitution to the binder and its kind -- NB: varKind tv = coercionLKind kco (subst1, tv1) = substTyVarBndr subst tcv - -- In the Swapped case, we re-kind the type variable, AND - -- override the substitution for the original variable to the - -- re-kinded one, suitably casted - tv2 = tv1 `setTyVarKind` coercionLKind kco' - subst2 = (extendTvSubst subst1 tcv (mkTyVarTy tv2 `CastTy` kco')) - `extendSubstInScope` tv2 upd_subst_cv subst -- ToDo: probably not right yet - | notSwapped sym || isReflCo kco' = (subst1, cv1) - | otherwise = (subst2, cv2) - where + = case k_mco' of + MCo k_co' | isSwapped sym -> (subst2, cv2) + where + cv2 = cv1 `setTyVarKind` coercionLKind k_co' + subst2 = subst1 `extendSubstInScope` cv2 + + _ -> (subst1, cv1) + where (subst1, cv1) = substCoVarBndr subst tcv - cv2 = cv1 `setTyVarKind` coercionLKind kco' - subst2 = subst1 `extendSubstInScope` cv2 {- ********************************************************************** ===================================== compiler/GHC/Core/Lint.hs ===================================== @@ -2424,15 +2424,19 @@ lintCoercion co@(ForAllCo {}) go :: [OutTyCoVar] -- Binders in reverse order -> InCoercion -> LintM Role go tcvs co@(ForAllCo { fco_tcv = tcv, fco_visL = visL, fco_visR = visR - , fco_kind = kind_co, fco_body = body_co }) + , fco_kind = kind_mco, fco_body = body_co }) | not (isTyCoVar tcv) = failWithL (text "Non tyco binder in ForAllCo:" <+> ppr co) | otherwise - = do { lk <- lintStarCoercion kind_co + = do { mb_lk <- case kind_mco of + MRefl -> return Nothing + MCo kind_co -> Just <$> lintStarCoercion kind_co ; lintTyCoBndr tcv $ \tcv' -> - do { ensureEqTys (varType tcv') lk $ - text "Kind mis-match in ForallCo" <+> ppr co + do { case mb_lk of + Nothing -> return () + Just lk -> ensureEqTys (varType tcv') lk $ + text "Kind mis-match in ForallCo" <+> ppr co -- I'm not very sure about this part, because it traverses body_co -- but at least it's on a cold path (a ForallCo for a CoVar) ===================================== compiler/GHC/Core/Opt/Arity.hs ===================================== @@ -2367,8 +2367,7 @@ mkEtaForAllMCo (Bndr tcv vis) ty mco | otherwise -> mk_fco (mkRepReflCo ty) MCo co -> mk_fco co where - mk_fco co = MCo (mkForAllCo tcv vis coreTyLamForAllTyFlag - (mkNomReflCo (varType tcv)) co) + mk_fco co = MCo (mkForAllCo tcv vis coreTyLamForAllTyFlag MRefl co) -- coreTyLamForAllTyFlag: See Note [The EtaInfo mechanism], particularly -- the (EtaInfo Invariant). (sym co) wraps a lambda that always has -- a ForAllTyFlag of coreTyLamForAllTyFlag; see Note [Required foralls in Core] @@ -2808,11 +2807,10 @@ tryEtaReduce rec_ids bndrs body eval_sd | Just tv <- getTyVar_maybe arg_ty , bndr == tv = case splitForAllForAllTyBinder_maybe fun_ty of Just (Bndr _ vis, _) -> Just (fco, []) - where !fco = mkForAllCo tv vis coreTyLamForAllTyFlag kco co + where !fco = mkForAllCo tv vis coreTyLamForAllTyFlag MRefl co -- The lambda we are eta-reducing always has visibility -- 'coreTyLamForAllTyFlag' which may or may not match -- the visibility on the inner function (#24014) - kco = mkNomReflCo (tyVarKind tv) Nothing -> pprPanic "tryEtaReduce: type arg to non-forall type" (text "fun:" <+> ppr bndr $$ text "arg:" <+> ppr arg_ty ===================================== compiler/GHC/Core/Reduction.hs ===================================== @@ -373,7 +373,7 @@ mkForAllRedn :: ForAllTyFlag -> Reduction mkForAllRedn vis tv1 (Reduction h ki') (Reduction co ty) = mkReduction - (mkForAllCo tv1 vis vis h co) + (mkForAllCo tv1 vis vis (kindCoToMKindCo h) co) (mkForAllTy (Bndr tv2 vis) ty) where tv2 = setTyVarKind tv1 ki' ===================================== compiler/GHC/Core/TyCo/FVs.hs ===================================== @@ -51,7 +51,6 @@ module GHC.Core.TyCo.FVs import GHC.Prelude import {-# SOURCE #-} GHC.Core.Type( partitionInvisibleTypes, coreView, rewriterView ) -import {-# SOURCE #-} GHC.Core.Coercion( coercionLKind ) import GHC.Builtin.Types.Prim( funTyFlagTyCon ) @@ -641,8 +640,10 @@ tyCoVarsOfCoList :: Coercion -> [TyCoVar] tyCoVarsOfCoList co = fvVarList $ tyCoFVsOfCo co tyCoFVsOfMCo :: MCoercion -> FV -tyCoFVsOfMCo MRefl = emptyFV -tyCoFVsOfMCo (MCo co) = tyCoFVsOfCo co +tyCoFVsOfMCo mco fv_cand in_scope acc + = case mco of + MRefl -> emptyFV fv_cand in_scope acc + MCo co -> tyCoFVsOfCo co fv_cand in_scope acc tyCoFVsOfCo :: Coercion -> FV -- Extracts type and coercion variables from a coercion @@ -655,7 +656,7 @@ tyCoFVsOfCo (TyConAppCo _ _ cos) fv_cand in_scope acc = tyCoFVsOfCos cos fv_cand tyCoFVsOfCo (AppCo co arg) fv_cand in_scope acc = (tyCoFVsOfCo co `unionFV` tyCoFVsOfCo arg) fv_cand in_scope acc tyCoFVsOfCo (ForAllCo { fco_tcv = tv, fco_kind = kind_co, fco_body = co }) fv_cand in_scope acc - = (tyCoFVsVarBndr tv (tyCoFVsOfCo co) `unionFV` tyCoFVsOfCo kind_co) fv_cand in_scope acc + = (tyCoFVsVarBndr tv (tyCoFVsOfCo co) `unionFV` tyCoFVsOfMCo kind_co) fv_cand in_scope acc tyCoFVsOfCo (FunCo { fco_mult = w, fco_arg = co1, fco_res = co2 }) fv_cand in_scope acc = (tyCoFVsOfCo co1 `unionFV` tyCoFVsOfCo co2 `unionFV` tyCoFVsOfCo w) fv_cand in_scope acc tyCoFVsOfCo (CoVarCo v) fv_cand in_scope acc @@ -693,6 +694,10 @@ almostDevoidCoVarOfCo :: CoVar -> Coercion -> Bool almostDevoidCoVarOfCo cv co = almost_devoid_co_var_of_co co cv +almost_devoid_co_var_of_mco :: MCoercion -> CoVar -> Bool +almost_devoid_co_var_of_mco MRefl _ = True +almost_devoid_co_var_of_mco (MCo co) cv = almost_devoid_co_var_of_co co cv + almost_devoid_co_var_of_co :: Coercion -> CoVar -> Bool almost_devoid_co_var_of_co (Refl {}) _ = True -- covar is allowed in Refl and almost_devoid_co_var_of_co (GRefl {}) _ = True -- GRefl, so we don't look into @@ -703,7 +708,7 @@ almost_devoid_co_var_of_co (AppCo co arg) cv = almost_devoid_co_var_of_co co cv && almost_devoid_co_var_of_co arg cv almost_devoid_co_var_of_co (ForAllCo { fco_tcv = v, fco_kind = kind_co, fco_body = co }) cv - = almost_devoid_co_var_of_co kind_co cv + = almost_devoid_co_var_of_mco kind_co cv && (v == cv || almost_devoid_co_var_of_co co cv) almost_devoid_co_var_of_co (FunCo { fco_mult = w, fco_arg = co1, fco_res = co2 }) cv = almost_devoid_co_var_of_co w cv @@ -1032,7 +1037,7 @@ tyConsOfType ty go_co (TyConAppCo _ tc args) = go_tc tc `unionUniqSets` go_cos args go_co (AppCo co arg) = go_co co `unionUniqSets` go_co arg go_co (ForAllCo { fco_kind = kind_co, fco_body = co }) - = go_co kind_co `unionUniqSets` go_co co + = go_mco kind_co `unionUniqSets` go_co co go_co (FunCo { fco_mult = m, fco_arg = a, fco_res = r }) = go_co m `unionUniqSets` go_co a `unionUniqSets` go_co r go_co (AxiomCo ax args) = go_ax ax `unionUniqSets` go_cos args @@ -1230,14 +1235,14 @@ occCheckExpand vs_to_avoid ty go_co cxt (SubCo co) = do { co' <- go_co cxt co ; return (SubCo co') } - go_co cxt@(as, env) co@(ForAllCo { fco_tcv = tv, fco_kind = kind_co, fco_body = body_co }) - = do { kind_co' <- go_co cxt kind_co - ; let tv' = setVarType tv $ - coercionLKind kind_co' - env' = extendVarEnv env tv tv' - as' = as `delVarSet` tv + go_co cxt@(as, env) co@(ForAllCo { fco_tcv = tcv, fco_kind = kind_co, fco_body = body_co }) + = do { ki' <- go cxt (varType tcv) + ; let tcv' = setVarType tcv ki' + env' = extendVarEnv env tcv tcv' + as' = as `delVarSet` tcv + ; kind_co' <- go_mco cxt kind_co ; body' <- go_co (as', env') body_co - ; return (co { fco_tcv = tv', fco_kind = kind_co', fco_body = body' }) } + ; return (co { fco_tcv = tcv', fco_kind = kind_co', fco_body = body' }) } go_co cxt co@(FunCo { fco_mult = w, fco_arg = co1 ,fco_res = co2 }) = do { co1' <- go_co cxt co1 ===================================== compiler/GHC/Core/TyCo/Rep.hs ===================================== @@ -39,7 +39,7 @@ module GHC.Core.TyCo.Rep ( UnivCoProvenance(..), CoercionHole(..), coHoleCoVar, setCoHoleCoVar, CoercionN, CoercionR, CoercionP, KindCoercion, - MCoercion(..), MCoercionR, MCoercionN, + MCoercion(..), MCoercionR, MCoercionN, KindMCoercion, -- * Functions over types mkNakedTyConTy, mkTyVarTy, mkTyVarTys, @@ -806,6 +806,34 @@ tcMkScaledFunTy (Scaled mult arg) res = tcMkVisFunTy mult arg res %************************************************************************ -} +type CoercionN = Coercion -- always Nominal +type CoercionR = Coercion -- always Representational +type CoercionP = Coercion -- always Phantom + +type MCoercionN = MCoercion -- alwyas Nominal +type MCoercionR = MCoercion -- always Representational + +{- Note [KindCoercion] +~~~~~~~~~~~~~~~~~~~~~~ +A KindCoercion kco :: k1 ~r k2 is a Coercion with these properties: + (a) It is Nominal; that is r=Nominal + (b) Both (k1::Type) and (k2::Type); it is homogeneous + +The coercion in (a) ForAllCo and (b) CastTy is a KindCoercion. + +The invariants of KindCoercion allow `isReflKindCo` to elminate GRefl, +whereas isReflCo cannot. In particular, consider a KindCoercion + kco = GRefl r k (MCo kk)) :: k ~ (k |> kk) +Since `kco`is a KindCoercion, we know that + r = Nominal + k :: Type and (k |> kk) :: Type +Hence kk must be Refl. And hence kco = GRefl N k MRefl, which is +the same as Refl. See `isReflKindCo`. +-} + +type KindCoercion = CoercionN -- See Note [KindCoercion] +type KindMCoercion = MCoercionN -- See Note [KindCoercion] + -- | A 'Coercion' is concrete evidence of the equality/convertibility -- of two types. @@ -829,7 +857,7 @@ data Coercion -- GRefl :: "e" -> _ -> Maybe N -> e -- See Note [Generalized reflexive coercion] - | GRefl Role Type MCoercionN -- See Note [Refl invariant] + | GRefl Role Type KindMCoercion -- See Note [Refl invariant] -- Use (Refl ty), not (GRefl Nominal ty MRefl) -- Use (GRefl Representational _ _), not (SubCo (GRefl Nominal _ _)) @@ -853,7 +881,7 @@ data Coercion , fco_visL :: !ForAllTyFlag -- Visibility of coercionLKind , fco_visR :: !ForAllTyFlag -- Visibility of coercionRKind -- See (FC7) of Note [ForAllCo] - , fco_kind :: KindCoercion + , fco_kind :: KindMCoercion -- See (FC8) of Note [ForAllCo] , fco_body :: Coercion } -- ForAllCo :: _ -> N -> e -> e @@ -911,6 +939,15 @@ data Coercion -- Only present during typechecking deriving Data.Data +-- | A semantically more meaningful type to represent what may or may not be a +-- useful 'Coercion'. +data MCoercion + = MRefl + -- A trivial Reflexivity coercion + | MCo Coercion + -- Other coercions + deriving Data.Data + data CoSel -- See Note [SelCo] = SelTyCon Int Role -- Decomposes (T co1 ... con); zero-indexed -- Invariant: Given: SelCo (SelTyCon i r) co @@ -932,11 +969,6 @@ data FunSel -- See Note [SelCo] | SelRes -- Result of function deriving( Eq, Data.Data, Ord ) -type CoercionN = Coercion -- always nominal -type CoercionR = Coercion -- always representational -type CoercionP = Coercion -- always phantom -type KindCoercion = CoercionN -- always nominal - instance Outputable Coercion where ppr = pprCo @@ -980,17 +1012,6 @@ instance NFData CoSel where rnf SelForAll = () rnf (SelFun fs) = rnf fs `seq` () --- | A semantically more meaningful type to represent what may or may not be a --- useful 'Coercion'. -data MCoercion - = MRefl - -- A trivial Reflexivity coercion - | MCo Coercion - -- Other coercions - deriving Data.Data -type MCoercionR = MCoercion -type MCoercionN = MCoercion - instance Outputable MCoercion where ppr MRefl = text "MRefl" ppr (MCo co) = text "MCo" <+> ppr co @@ -1278,6 +1299,14 @@ Several things to note here fco_visL = fco_visR = coreTyLamForAllTyFlag c.f. (FT2) in Note [ForAllTy] +(FC8) We /represent/ a ForAllCo { fco_tcv = tcv, fco_kind = kmco } as follows: + * The tcv::TyCoVar has a kind (like any Var), say tcv::ki + * The kind-coercion `kmco` is a KindMCoercion: + - If kmco = MRefl, then the coercion in the typing rule is (Refl ki) + - If kmco = MCo kco, then the coercion in the typing rule is `co`, + /and/ ki = coercionLKind kco + So in the common MRefl case, the kind of `tcv` plays a useful role. + Note [Predicate coercions] ~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose we have @@ -1937,11 +1966,14 @@ foldTyCo (TyCoFolder { tcf_view = view go_co env (FunCo { fco_mult = cw, fco_arg = c1, fco_res = c2 }) = go_co env cw `mappend` go_co env c1 `mappend` go_co env c2 - go_co env (ForAllCo tv _vis1 _vis2 kind_co co) - = go_co env kind_co `mappend` go_ty env (varType tv) - `mappend` go_co env' co + go_co env (ForAllCo { fco_tcv = tcv, fco_kind = kind_co, fco_body = co }) + = go_mco env kind_co `mappend` go_ty env (varType tcv) + `mappend` go_co env' co where - env' = tycobinder env tv Inferred + env' = tycobinder env tcv Inferred + + go_mco _ MRefl = mempty + go_mco env (MCo co) = go_co env co -- | A view function that looks through nothing. noView :: Type -> Maybe Type @@ -1983,18 +2015,19 @@ typesSize tys = foldr ((+) . typeSize) 0 tys coercionSize :: Coercion -> Int coercionSize (Refl ty) = typeSize ty -coercionSize (GRefl _ ty MRefl) = typeSize ty -coercionSize (GRefl _ ty (MCo co)) = 1 + typeSize ty + coercionSize co +coercionSize (GRefl _ ty mco) = typeSize ty + mCoercionSize mco coercionSize (TyConAppCo _ _ args) = 1 + sum (map coercionSize args) coercionSize (AppCo co arg) = coercionSize co + coercionSize arg coercionSize (ForAllCo { fco_kind = h, fco_body = co }) - = 1 + coercionSize co + coercionSize h + = 1 + coercionSize co + mCoercionSize h coercionSize (FunCo _ _ _ w c1 c2) = 1 + coercionSize c1 + coercionSize c2 + coercionSize w coercionSize (CoVarCo _) = 1 coercionSize (HoleCo _) = 1 coercionSize (AxiomCo _ cs) = 1 + sum (map coercionSize cs) -coercionSize (UnivCo { uco_lty = t1, uco_rty = t2 }) = 1 + typeSize t1 + typeSize t2 +coercionSize (UnivCo { uco_lty = t1, uco_rty = t2, uco_deps = deps }) + = 1 + typeSize t1 + typeSize t2 + + sum (map coercionSize deps) coercionSize (SymCo co) = 1 + coercionSize co coercionSize (TransCo co1 co2) = 1 + coercionSize co1 + coercionSize co2 coercionSize (SelCo _ co) = 1 + coercionSize co @@ -2003,6 +2036,10 @@ coercionSize (InstCo co arg) = 1 + coercionSize co + coercionSize arg coercionSize (KindCo co) = 1 + coercionSize co coercionSize (SubCo co) = 1 + coercionSize co +mCoercionSize :: MCoercion -> Int +mCoercionSize MRefl = 0 +mCoercionSize (MCo co) = coercionSize co + {- ************************************************************************ * * ===================================== compiler/GHC/Core/TyCo/Subst.hs ===================================== @@ -29,11 +29,10 @@ module GHC.Core.TyCo.Subst mkTvSubstPrs, substTyWith, substTyWithCoVars, substTysWith, substTysWithCoVars, - substCoWith, + substCoWithInScope, substTy, substTyAddInScope, substScaledTy, substTyUnchecked, substTysUnchecked, substScaledTysUnchecked, substThetaUnchecked, substTyWithUnchecked, substScaledTyUnchecked, - substCoUnchecked, substCoWithUnchecked, substTyWithInScope, substTys, substScaledTys, substTheta, lookupTyVar, @@ -44,8 +43,8 @@ module GHC.Core.TyCo.Subst substCoVarBndr, substDCoVarSet, substTyVar, substTyVars, substTyVarToTyVar, substTyCoVars, - substTyCoBndr, substForAllCoBndr, - substVarBndrUsing, substForAllCoBndrUsing, + substTyCoBndr, + substVarBndrUsing, checkValidSubst, isValidTCvSubst, ) where @@ -60,7 +59,7 @@ import {-# SOURCE #-} GHC.Core.Coercion , mkAxiomCo, mkAppCo, mkGReflCo , mkInstCo, mkLRCo, mkTyConAppCo , mkCoercionType - , coercionLKind, coVarTypesRole ) + , coVarTypesRole ) import {-# SOURCE #-} GHC.Core.TyCo.Ppr ( pprTyVar ) import {-# SOURCE #-} GHC.Core.Ppr ( ) -- instance Outputable CoreExpr import {-# SOURCE #-} GHC.Core ( CoreExpr ) @@ -618,28 +617,19 @@ substTyWithUnchecked tvs tys -- Pre-condition: the 'in_scope' set should satisfy Note [The substitution -- invariant]; specifically it should include the free vars of 'tys', -- and of 'ty' minus the domain of the subst. -substTyWithInScope :: HasDebugCallStack => InScopeSet -> [TyVar] -> [Type] -> Type -> Type +substTyWithInScope :: HasDebugCallStack + => InScopeSet -> [TyVar] -> [Type] -> Type -> Type substTyWithInScope in_scope tvs tys ty = assert (tvs `equalLength` tys ) substTy (mkTvSubst in_scope tenv) ty where tenv = zipTyEnv tvs tys -- | Coercion substitution, see 'zipTvSubst' -substCoWith :: HasDebugCallStack => [TyVar] -> [Type] -> Coercion -> Coercion -substCoWith tvs tys = assert (tvs `equalLength` tys ) - substCo (zipTvSubst tvs tys) - --- | Coercion substitution, see 'zipTvSubst'. Disables sanity checks. --- The problems that the sanity checks in substCo catch are described in --- Note [The substitution invariant]. --- The goal of #11371 is to migrate all the calls of substCoUnchecked to --- substCo and remove this function. Please don't use in new code. -substCoWithUnchecked :: [TyVar] -> [Type] -> Coercion -> Coercion -substCoWithUnchecked tvs tys +substCoWithInScope :: HasDebugCallStack + => InScopeSet -> [TyVar] -> [Type] -> Coercion -> Coercion +substCoWithInScope in_scope tvs tys co = assert (tvs `equalLength` tys ) - substCoUnchecked (zipTvSubst tvs tys) - - + substCo (mkTvSubst in_scope (zipTyEnv tvs tys)) co -- | Substitute covars within a type substTyWithCoVars :: [CoVar] -> [Coercion] -> Type -> Type @@ -800,10 +790,10 @@ subst_ty subst ty !res' = go res in ty { ft_mult = mult', ft_arg = arg', ft_res = res' } go (ForAllTy (Bndr tv vis) ty) - = case substVarBndrUnchecked subst tv of - (subst', tv') -> - (ForAllTy $! ((Bndr $! tv') vis)) $! - (subst_ty subst' ty) + = (ForAllTy $! ((Bndr $! tv') vis)) $! (subst_ty subst' ty) + where + !(subst',tv') = substVarBndrUnchecked subst tv + -- Unchecked because subst_ty is used from substTyUnchecked go (LitTy n) = LitTy $! n go (CastTy ty co) = (mkCastTy $! (go ty)) $! (subst_co subst co) go (CoercionTy co) = CoercionTy $! (subst_co subst co) @@ -850,16 +840,6 @@ substCo subst co | isEmptyTCvSubst subst = co | otherwise = checkValidSubst subst [] [co] $ subst_co subst co --- | Substitute within a 'Coercion' disabling sanity checks. --- The problems that the sanity checks in substCo catch are described in --- Note [The substitution invariant]. --- The goal of #11371 is to migrate all the calls of substCoUnchecked to --- substCo and remove this function. Please don't use in new code. -substCoUnchecked :: Subst -> Coercion -> Coercion -substCoUnchecked subst co - | isEmptyTCvSubst subst = co - | otherwise = subst_co subst co - -- | Substitute within several 'Coercion's -- The substitution has to satisfy the invariants described in -- Note [The substitution invariant]. @@ -868,7 +848,7 @@ substCos subst cos | isEmptyTCvSubst subst = cos | otherwise = checkValidSubst subst [] cos $ map (subst_co subst) cos -subst_co :: Subst -> Coercion -> Coercion +subst_co :: HasDebugCallStack => Subst -> Coercion -> Coercion subst_co subst co = go co where @@ -885,10 +865,14 @@ subst_co subst co go (TyConAppCo r tc args)= mkTyConAppCo r tc $! go_cos args go (AxiomCo con cos) = mkAxiomCo con $! go_cos cos go (AppCo co arg) = (mkAppCo $! go co) $! go arg - go (ForAllCo tv visL visR kind_co co) - = case substForAllCoBndrUnchecked subst tv kind_co of - (subst', tv', kind_co') -> - ((mkForAllCo $! tv') visL visR $! kind_co') $! subst_co subst' co + go (ForAllCo { fco_tcv = tcv, fco_visL = visL, fco_visR = visR + , fco_kind = kind_co, fco_body = co }) + = ((mkForAllCo $! tcv') visL visR + $! go_mco kind_co) + $! subst_co subst' co + where + !(subst', tcv') = substVarBndrUnchecked subst tcv + -- Unchecked because used from substTyUnchecked go (FunCo r afl afr w co1 co2) = ((mkFunCo2 r afl afr $! go w) $! go co1) $! go co2 go (CoVarCo cv) = substCoVar subst cv go (UnivCo { uco_prov = p, uco_role = r @@ -917,75 +901,6 @@ substDCoVarSet :: Subst -> DCoVarSet -> DCoVarSet substDCoVarSet subst cvs = coVarsOfCosDSet $ map (substCoVar subst) $ dVarSetElems cvs -substForAllCoBndr :: Subst -> TyCoVar -> KindCoercion - -> (Subst, TyCoVar, Coercion) -substForAllCoBndr subst - = substForAllCoBndrUsing (substCo subst) subst - --- | Like 'substForAllCoBndr', but disables sanity checks. --- The problems that the sanity checks in substCo catch are described in --- Note [The substitution invariant]. --- The goal of #11371 is to migrate all the calls of substCoUnchecked to --- substCo and remove this function. Please don't use in new code. -substForAllCoBndrUnchecked :: Subst -> TyCoVar -> KindCoercion - -> (Subst, TyCoVar, Coercion) -substForAllCoBndrUnchecked subst - = substForAllCoBndrUsing (substCoUnchecked subst) subst - --- See Note [Sym and ForAllCo] -substForAllCoBndrUsing :: (Coercion -> Coercion) -- transformation to kind co - -> Subst -> TyCoVar -> KindCoercion - -> (Subst, TyCoVar, KindCoercion) -substForAllCoBndrUsing sco subst old_var - | isTyVar old_var = substForAllCoTyVarBndrUsing sco subst old_var - | otherwise = substForAllCoCoVarBndrUsing sco subst old_var - -substForAllCoTyVarBndrUsing :: (Coercion -> Coercion) -- transformation to kind co - -> Subst -> TyVar -> KindCoercion - -> (Subst, TyVar, KindCoercion) -substForAllCoTyVarBndrUsing sco (Subst in_scope idenv tenv cenv) old_var old_kind_co - = assert (isTyVar old_var ) - ( Subst (in_scope `extendInScopeSet` new_var) idenv new_env cenv - , new_var, new_kind_co ) - where - new_env | no_change = delVarEnv tenv old_var - | otherwise = extendVarEnv tenv old_var (TyVarTy new_var) - - no_kind_change = noFreeVarsOfCo old_kind_co - no_change = no_kind_change && (new_var == old_var) - - new_kind_co | no_kind_change = old_kind_co - | otherwise = sco old_kind_co - - new_ki1 = coercionLKind new_kind_co - -- We could do substitution to (tyVarKind old_var). We don't do so because - -- we already substituted new_kind_co, which contains the kind information - -- we want. We don't want to do substitution once more. Also, in most cases, - -- new_kind_co is a Refl, in which case coercionKind is really fast. - - new_var = uniqAway in_scope (setTyVarKind old_var new_ki1) - -substForAllCoCoVarBndrUsing :: (Coercion -> Coercion) -- transformation to kind co - -> Subst -> CoVar -> KindCoercion - -> (Subst, CoVar, KindCoercion) -substForAllCoCoVarBndrUsing sco (Subst in_scope idenv tenv cenv) - old_var old_kind_co - = assert (isCoVar old_var ) - ( Subst (in_scope `extendInScopeSet` new_var) idenv tenv new_cenv - , new_var, new_kind_co ) - where - new_cenv | no_change = delVarEnv cenv old_var - | otherwise = extendVarEnv cenv old_var (mkCoVarCo new_var) - - no_kind_change = noFreeVarsOfCo old_kind_co - no_change = no_kind_change && (new_var == old_var) - - new_kind_co | no_kind_change = old_kind_co - | otherwise = sco old_kind_co - - new_ki1 = coercionLKind new_kind_co - new_var = uniqAway in_scope $ mkCoVar (varName old_var) new_ki1 - substCoVar :: Subst -> CoVar -> Coercion substCoVar (Subst _ _ _ cenv) cv = case lookupVarEnv cenv cv of ===================================== compiler/GHC/Core/TyCo/Tidy.hs ===================================== @@ -334,7 +334,7 @@ tidyCo env co go (TyConAppCo r tc cos) = TyConAppCo r tc $! strictMap go cos go (AppCo co1 co2) = (AppCo $! go co1) $! go co2 go (ForAllCo tv visL visR h co) - = ((((ForAllCo $! tvp) $! visL) $! visR) $! (go h)) $! (tidyCo envp co) + = ((((ForAllCo $! tvp) $! visL) $! visR) $! (go_mco h)) $! (tidyCo envp co) where (envp, tvp) = tidyVarBndr env tv -- the case above duplicates a bit of work in tidying h and the kind -- of tv. But the alternative is to use coercionKind, which seems worse. ===================================== compiler/GHC/Core/Type.hs ===================================== @@ -210,7 +210,7 @@ module GHC.Core.Type ( substTyAddInScope, substTyUnchecked, substTysUnchecked, substScaledTyUnchecked, substScaledTysUnchecked, substThetaUnchecked, substTyWithUnchecked, - substCo, substCoUnchecked, substCoWithUnchecked, + substCo, substCoWithInScope, substTyVarBndr, substTyVarBndrs, substTyVar, substTyVars, substVarBndr, substVarBndrs, substTyCoBndr, substTyVarToTyVar, @@ -530,10 +530,13 @@ expandTypeSynonyms ty = mkTyConAppCo r tc (map (go_co subst) args) go_co subst (AppCo co arg) = mkAppCo (go_co subst co) (go_co subst arg) - go_co subst (ForAllCo { fco_tcv = tv, fco_visL = visL, fco_visR = visR + go_co subst (ForAllCo { fco_tcv = tcv, fco_visL = visL, fco_visR = visR , fco_kind = kind_co, fco_body = co }) - = let (subst', tv', kind_co') = go_cobndr subst tv kind_co in - mkForAllCo tv' visL visR kind_co' (go_co subst' co) + = mkForAllCo tcv' visL visR + (go_mco subst kind_co) + (go_co subst' co) + where + (subst', tcv') = substVarBndr subst tcv go_co subst (FunCo r afl afr w co1 co2) = mkFunCo2 r afl afr (go_co subst w) (go_co subst co1) (go_co subst co2) go_co subst (CoVarCo cv) @@ -559,8 +562,6 @@ expandTypeSynonyms ty go_co _ (HoleCo h) = pprPanic "expandTypeSynonyms hit a hole" (ppr h) - go_cobndr subst = substForAllCoBndrUsing (go_co subst) subst - {- Notes on type synonyms ~~~~~~~~~~~~~~~~~~~~~~~~~ The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try @@ -971,7 +972,7 @@ mapTyCoX (TyCoMapper { tcm_tyvar = tyvar = mkTyConAppCo r tc <$> go_cos env cos go_co !env (ForAllCo { fco_tcv = tv, fco_visL = visL, fco_visR = visR , fco_kind = kind_co, fco_body = co }) - = do { kind_co' <- go_co env kind_co + = do { kind_co' <- go_mco env kind_co ; tycobinder env tv visL $ \env' tv' -> do ; co' <- go_co env' co ; return $ mkForAllCo tv' visL visR kind_co' co' } ===================================== compiler/GHC/Core/Unify.hs ===================================== @@ -2414,14 +2414,15 @@ ty_co_match menv subst (FunTy { ft_mult = w, ft_arg = ty1, ft_res = ty2 }) -- not doing so caused #21205. ty_co_match menv subst (ForAllTy (Bndr tv1 vis1t) ty1) - (ForAllCo tv2 vis1c vis2c kind_co2 co2) + (ForAllCo tv2 vis1c vis2c kind_mco2 co2) lkco rkco | isTyVar tv1 && isTyVar tv2 , vis1t == vis1c && vis1c == vis2c -- Is this necessary? -- Is this visibility check necessary? @rae says: yes, I think the -- check is necessary, if we're caring about visibility (and we are). -- But ty_co_match is a dark and not important corner. - = do { subst1 <- ty_co_match menv subst (tyVarKind tv1) kind_co2 + = do { subst1 <- ty_co_match menv subst (tyVarKind tv1) + (forAllCoKindCo tv2 kind_mco2) ki_ki_co ki_ki_co ; let rn_env0 = me_env menv rn_env1 = rnBndr2 rn_env0 tv1 tv2 @@ -2522,6 +2523,6 @@ pushRefl co = -> Just (TyConAppCo r tc (zipWith mkReflCo (tyConRoleListX r tc) tys)) Just (ForAllTy (Bndr tv vis) ty, r) -> Just (ForAllCo { fco_tcv = tv, fco_visL = vis, fco_visR = vis - , fco_kind = mkNomReflCo (varType tv) + , fco_kind = MRefl , fco_body = mkReflCo r ty }) _ -> Nothing ===================================== compiler/GHC/CoreToIface.hs ===================================== @@ -312,7 +312,7 @@ toIfaceCoercionX fr co = IfaceForAllCo (toIfaceBndr tv) visL visR - (toIfaceCoercionX fr' k) + (go_mco k) (toIfaceCoercionX fr' co) where fr' = fr `delVarSet` tv ===================================== compiler/GHC/Iface/Rename.hs ===================================== @@ -689,7 +689,7 @@ rnIfaceCo (IfaceAxiomCo ax cos) = IfaceAxiomCo ax <$> mapM rnIfaceCo cos rnIfaceCo (IfaceKindCo c) = IfaceKindCo <$> rnIfaceCo c rnIfaceCo (IfaceForAllCo bndr visL visR co1 co2) = (\bndr' co1' co2' -> IfaceForAllCo bndr' visL visR co1' co2') - <$> rnIfaceBndr bndr <*> rnIfaceCo co1 <*> rnIfaceCo co2 + <$> rnIfaceBndr bndr <*> rnIfaceMCo co1 <*> rnIfaceCo co2 rnIfaceCo (IfaceUnivCo s r t1 t2 deps) = IfaceUnivCo s r <$> rnIfaceType t1 <*> rnIfaceType t2 <*> mapM rnIfaceCo deps ===================================== compiler/GHC/Iface/Syntax.hs ===================================== @@ -2076,7 +2076,7 @@ freeNamesIfCoercion (IfaceTyConAppCo _ tc cos) freeNamesIfCoercion (IfaceAppCo c1 c2) = freeNamesIfCoercion c1 &&& freeNamesIfCoercion c2 freeNamesIfCoercion (IfaceForAllCo _tcv _visL _visR kind_co co) - = freeNamesIfCoercion kind_co &&& freeNamesIfCoercion co + = freeNamesIfMCoercion kind_co &&& freeNamesIfCoercion co freeNamesIfCoercion (IfaceFreeCoVar _) = emptyNameSet freeNamesIfCoercion (IfaceCoVarCo _) = emptyNameSet freeNamesIfCoercion (IfaceHoleCo _) = emptyNameSet ===================================== compiler/GHC/Iface/Type.hs ===================================== @@ -132,7 +132,7 @@ data IfaceBndr -- Local (non-top-level) binders deriving (Eq, Ord) -type IfaceIdBndr = (IfaceType, IfLclName, IfaceType) +type IfaceIdBndr = (IfaceType, IfLclName, IfaceType) -- (multiplicity, name, type) type IfaceTvBndr = (IfLclName, IfaceKind) ifaceTvBndrName :: IfaceTvBndr -> IfLclName @@ -479,7 +479,7 @@ data IfaceCoercion | IfaceFunCo Role IfaceCoercion IfaceCoercion IfaceCoercion | IfaceTyConAppCo Role IfaceTyCon [IfaceCoercion] | IfaceAppCo IfaceCoercion IfaceCoercion - | IfaceForAllCo IfaceBndr !ForAllTyFlag !ForAllTyFlag IfaceCoercion IfaceCoercion + | IfaceForAllCo IfaceBndr !ForAllTyFlag !ForAllTyFlag IfaceMCoercion IfaceCoercion | IfaceCoVarCo IfLclName | IfaceAxiomCo IfaceAxiomRule [IfaceCoercion] -- ^ There are only a fixed number of CoAxiomRules, so it suffices @@ -1454,10 +1454,9 @@ pprIfaceForAllPartMust :: [IfaceForAllBndr] -> [IfacePredType] -> SDoc -> SDoc pprIfaceForAllPartMust tvs ctxt sdoc = ppr_iface_forall_part ShowForAllMust tvs ctxt sdoc -pprIfaceForAllCoPart :: [(IfLclName, IfaceCoercion, ForAllTyFlag, ForAllTyFlag)] +pprIfaceForAllCoPart :: [(IfaceBndr, IfaceMCoercion, ForAllTyFlag, ForAllTyFlag)] -> SDoc -> SDoc -pprIfaceForAllCoPart tvs sdoc - = sep [ pprIfaceForAllCo tvs, sdoc ] +pprIfaceForAllCoPart tvs sdoc = sep [ pprIfaceForAllCo tvs, sdoc ] ppr_iface_forall_part :: ShowForAllFlag -> [IfaceForAllBndr] -> [IfacePredType] -> SDoc -> SDoc @@ -1494,11 +1493,11 @@ ppr_itv_bndrs all_bndrs@(bndr@(Bndr _ vis) : bndrs) vis1 | otherwise = (all_bndrs, []) ppr_itv_bndrs [] _ = ([], []) -pprIfaceForAllCo :: [(IfLclName, IfaceCoercion, ForAllTyFlag, ForAllTyFlag)] -> SDoc +pprIfaceForAllCo :: [(IfaceBndr, IfaceMCoercion, ForAllTyFlag, ForAllTyFlag)] -> SDoc pprIfaceForAllCo [] = empty pprIfaceForAllCo tvs = text "forall" <+> pprIfaceForAllCoBndrs tvs <> dot -pprIfaceForAllCoBndrs :: [(IfLclName, IfaceCoercion, ForAllTyFlag, ForAllTyFlag)] -> SDoc +pprIfaceForAllCoBndrs :: [(IfaceBndr, IfaceMCoercion, ForAllTyFlag, ForAllTyFlag)] -> SDoc pprIfaceForAllCoBndrs bndrs = hsep $ map pprIfaceForAllCoBndr bndrs pprIfaceForAllBndr :: IfaceForAllBndr -> SDoc @@ -1513,10 +1512,17 @@ pprIfaceForAllBndr bndr = -- See Note [Suppressing binder signatures] suppress_sig = SuppressBndrSig False -pprIfaceForAllCoBndr :: (IfLclName, IfaceCoercion, ForAllTyFlag, ForAllTyFlag) -> SDoc -pprIfaceForAllCoBndr (tv, kind_co, visL, visR) - = parens (ppr tv <> pp_vis <+> dcolon <+> pprIfaceCoercion kind_co) +pprIfaceForAllCoBndr :: (IfaceBndr, IfaceMCoercion, ForAllTyFlag, ForAllTyFlag) -> SDoc +pprIfaceForAllCoBndr (tcv, kind_mco, visL, visR) + = parens (ppr (ifaceBndrName tcv) <> pp_vis + <+> text "::~" <+> pprIfaceCoercion kind_co) + -- We print (tcv ::~ kind_co), with the "::~" reminding us the type of tcv + -- isn't kind_co; rather it's (coercionLKind kind_co). We used "::" previously + -- which grievously confused me. where + kind_co = case kind_mco of + IfaceMRefl -> IfaceReflCo (ifaceBndrType tcv) + IfaceMCo co -> co pp_vis | visL == coreTyLamForAllTyFlag , visR == coreTyLamForAllTyFlag = empty @@ -2069,10 +2075,8 @@ ppr_co ctxt_prec co@(IfaceForAllCo {}) where (tvs, inner_co) = split_co co - split_co (IfaceForAllCo (IfaceTvBndr (name, _)) visL visR kind_co co') - = let (tvs, co'') = split_co co' in ((name,kind_co,visL,visR):tvs,co'') - split_co (IfaceForAllCo (IfaceIdBndr (_, name, _)) visL visR kind_co co') - = let (tvs, co'') = split_co co' in ((name,kind_co,visL,visR):tvs,co'') + split_co (IfaceForAllCo bndr visL visR kind_co co') + = let (tvs, co'') = split_co co' in ((bndr,kind_co,visL,visR):tvs,co'') split_co co' = ([], co') -- Why these three? See Note [Free TyVars and CoVars in IfaceType] ===================================== compiler/GHC/IfaceToCore.hs ===================================== @@ -1576,9 +1576,12 @@ tcIfaceCo = go go (IfaceFunCo r w c1 c2) = mkFunCoNoFTF r <$> go w <*> go c1 <*> go c2 go (IfaceTyConAppCo r tc cs) = TyConAppCo r <$> tcIfaceTyCon tc <*> mapM go cs go (IfaceAppCo c1 c2) = AppCo <$> go c1 <*> go c2 - go (IfaceForAllCo tv visL visR k c) = do { k' <- go k - ; bindIfaceBndr tv $ \ tv' -> - ForAllCo tv' visL visR k' <$> go c } + go (IfaceForAllCo tcv visL visR k co) + = do { k' <- go_mco k + ; bindIfaceBndr tcv $ \ tv' -> + do { co' <- go co + ; return (ForAllCo { fco_tcv = tv', fco_visL = visL, fco_visR = visR + , fco_kind = k', fco_body = co' }) } } go (IfaceCoVarCo n) = CoVarCo <$> go_var n go (IfaceUnivCo p r t1 t2 ds) = do { t1' <- tcIfaceType t1; t2' <- tcIfaceType t2 ; ds' <- mapM go ds ===================================== compiler/GHC/Tc/TyCl/Utils.hs ===================================== @@ -135,7 +135,7 @@ synonymTyConsOfType ty go_co (TyConAppCo _ tc cs) = go_tc tc `plusNameEnv` go_co_s cs go_co (AppCo co co') = go_co co `plusNameEnv` go_co co' go_co (ForAllCo { fco_kind = kind_co, fco_body = body_co }) - = go_co kind_co `plusNameEnv` go_co body_co + = go_mco kind_co `plusNameEnv` go_co body_co go_co (FunCo { fco_mult = m, fco_arg = a, fco_res = r }) = go_co m `plusNameEnv` go_co a `plusNameEnv` go_co r go_co (CoVarCo _) = emptyNameEnv ===================================== compiler/GHC/Tc/Utils/TcMType.hs ===================================== @@ -1586,7 +1586,7 @@ collect_cand_qtvs_co orig_ty cur_lvl bound = go_co go_co dv (CoVarCo cv) = go_cv dv cv go_co dv (ForAllCo { fco_tcv = tcv, fco_kind = kind_co, fco_body = co }) - = do { dv1 <- go_co dv kind_co + = do { dv1 <- go_mco dv kind_co ; collect_cand_qtvs_co orig_ty cur_lvl (bound `extendVarSet` tcv) dv1 co } go_mco dv MRefl = return dv ===================================== compiler/GHC/Tc/Utils/TcType.hs ===================================== @@ -176,7 +176,6 @@ module GHC.Tc.Utils.TcType ( substTyUnchecked, substTysUnchecked, substScaledTyUnchecked, substThetaUnchecked, substTyWithUnchecked, - substCoUnchecked, substCoWithUnchecked, substTheta, isUnliftedType, ===================================== compiler/GHC/Types/Id/Make.hs ===================================== @@ -1206,10 +1206,11 @@ wrapCo co rep_ty (unbox_rep, box_rep) -- co :: arg_ty ~ rep_ty boxer = Boxer $ \ subst -> do { (rep_ids, rep_expr) <- case box_rep of - UnitBox -> do { rep_id <- newLocal (fsLit "cowrap_bx") (linear $ TcType.substTy subst rep_ty) + UnitBox -> do { rep_id <- newLocal (fsLit "cowrap_bx") + (linear $ TcType.substTy subst rep_ty) ; return ([rep_id], Var rep_id) } Boxer boxer -> boxer subst - ; let sco = substCoUnchecked subst co + ; let sco = substCo subst co ; return (rep_ids, rep_expr `Cast` mkSymCo sco) } ------------------------ ===================================== testsuite/tests/simplCore/should_compile/OpaqueNoCastWW.stderr ===================================== @@ -1,24 +1,24 @@ ==================== Tidy Core ==================== Result size of Tidy Core - = {terms: 82, types: 52, coercions: 29, joins: 0/0} + = {terms: 82, types: 52, coercions: 26, joins: 0/0} -- RHS size: {terms: 3, types: 3, coercions: 0, joins: 0/0} unsafeToInteger1 :: forall (n :: Nat). Signed n -> Signed n [GblId, Arity=1, Unf=OtherCon []] unsafeToInteger1 = \ (@(n :: Nat)) (ds :: Signed n) -> ds --- RHS size: {terms: 1, types: 0, coercions: 8, joins: 0/0} +-- RHS size: {terms: 1, types: 0, coercions: 7, joins: 0/0} unsafeToInteger :: forall (n :: Nat). Signed n -> Integer [GblId[[RecSel]], Arity=1, Unf=OtherCon []] unsafeToInteger = unsafeToInteger1 - `cast` (forall (n :: <Nat>_N). + `cast` (forall (n ::~ <Nat>_N). <Signed n>_R %<Many>_N ->_R OpaqueNoCastWW.N:Signed <n>_P :: (forall (n :: Nat). Signed n -> Signed n) ~R# (forall (n :: Nat). Signed n -> Integer)) --- RHS size: {terms: 8, types: 7, coercions: 21, joins: 0/0} +-- RHS size: {terms: 8, types: 7, coercions: 19, joins: 0/0} times [InlPrag=OPAQUE] :: forall (m :: Nat) (n :: Nat). Signed m -> Signed n -> Signed (m + n) @@ -33,7 +33,7 @@ times (ds `cast` (OpaqueNoCastWW.N:Signed <m>_P :: Signed m ~R# Integer)) (ds1 `cast` (OpaqueNoCastWW.N:Signed <n>_P :: Signed n ~R# Integer))) - `cast` (forall (m :: <Nat>_N) (n :: <Nat>_N). + `cast` (forall (m ::~ <Nat>_N) (n ::~ <Nat>_N). <Signed m>_R %<Many>_N ->_R <Signed n>_R %<Many>_N ->_R Sym (OpaqueNoCastWW.N:Signed <m + n>_P) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/94b62aa7e7b40b53442161a0c4f3809… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/94b62aa7e7b40b53442161a0c4f3809… You're receiving this email because of your account on gitlab.haskell.org.

1 0

[Git][ghc/ghc] Pushed new branch wip/angerman/test-darwin-underscore
by Moritz Angermann (＠angerman) 08 Sep '25

08 Sep '25

Moritz Angermann pushed new branch wip/angerman/test-darwin-underscore at Glasgow Haskell Compiler / GHC -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/tree/wip/angerman/test-darwin-undersco… You're receiving this email because of your account on gitlab.haskell.org.

1 0

[Git][ghc/ghc] Pushed new branch wip/angerman/windows-darwin-locale
by Moritz Angermann (＠angerman) 08 Sep '25

08 Sep '25

Moritz Angermann pushed new branch wip/angerman/windows-darwin-locale at Glasgow Haskell Compiler / GHC -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/tree/wip/angerman/windows-darwin-locale You're receiving this email because of your account on gitlab.haskell.org.

1 0

[Git][ghc/ghc][wip/angerman/testsuite-fix-exec_signals] testsuite: Fix broken exec_signals_child.c
by Moritz Angermann (＠angerman) 08 Sep '25

08 Sep '25

Moritz Angermann pushed to branch wip/angerman/testsuite-fix-exec_signals at Glasgow Haskell Compiler / GHC Commits: 57f53914 by Moritz Angermann at 2025-09-08T13:03:39+09:00 testsuite: Fix broken exec_signals_child.c There is no signal 0. The signal mask is 1-32. - - - - - 1 changed file: - testsuite/tests/rts/exec_signals_child.c Changes: ===================================== testsuite/tests/rts/exec_signals_child.c ===================================== @@ -2,8 +2,11 @@ #include <stdio.h> #include <errno.h> -// Prints the state of the signal handlers to stdout -int main() +// Prints the state of the signal handlers to stdout. +// NOTE: We intentionally start at signal 1 (not 0). Signal number 0 is not a +// real signal; passing 0 to sigismember/sigaction is undefined behaviour and +// on Darwin was observed to yield memory corruption / junk bytes in output. +int main(void) { int open = 0, i; sigset_t blockedsigs; @@ -11,7 +14,7 @@ int main() printf("ChildInfo { masked = ["); sigprocmask(SIG_BLOCK, NULL, &blockedsigs); - for(i = 0; i < NSIG; ++i) + for(i = 1; i < NSIG; ++i) { int ret = sigismember(&blockedsigs, i); if(ret >= 0) @@ -26,7 +29,7 @@ int main() printf("], handlers = ["); open = 0; - for(i = 0; i < NSIG; ++i) + for(i = 1; i < NSIG; ++i) { struct sigaction old; if(sigaction(i, NULL, &old) >= 0) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/57f53914a1011bdeeebb091c5e84d0f… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/57f53914a1011bdeeebb091c5e84d0f… You're receiving this email because of your account on gitlab.haskell.org.

1 0

[Git][ghc/ghc] Pushed new branch wip/angerman/testsuite-fix-exec_signals
by Moritz Angermann (＠angerman) 08 Sep '25

08 Sep '25

Moritz Angermann pushed new branch wip/angerman/testsuite-fix-exec_signals at Glasgow Haskell Compiler / GHC -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/tree/wip/angerman/testsuite-fix-exec_s… You're receiving this email because of your account on gitlab.haskell.org.

1 0