May 2025 - ghc-commits

[Git][ghc/ghc][wip/T26004] Wibbles
by Simon Peyton Jones (＠simonpj) 01 May '25

01 May '25

Simon Peyton Jones pushed to branch wip/T26004 at Glasgow Haskell Compiler / GHC Commits: 99fc2a5b by Simon Peyton Jones at 2025-05-01T12:09:28+01:00 Wibbles - - - - - 3 changed files: - compiler/GHC/Tc/Solver.hs - compiler/GHC/Tc/Solver/InertSet.hs - compiler/GHC/Tc/Solver/Monad.hs Changes: ===================================== compiler/GHC/Tc/Solver.hs ===================================== @@ -915,21 +915,22 @@ simplifyInfer top_lvl rhs_tclvl infer_mode sigs name_taus wanteds ; let psig_theta = concatMap sig_inst_theta partial_sigs -- First do full-blown solving - -- NB: we must gather up all the bindings from doing - -- this solving; hence (runTcSWithEvBinds ev_binds_var). - -- And note that since there are nested implications, - -- calling solveWanteds will side-effect their evidence - -- bindings, so we can't just revert to the input - -- constraint. - + -- NB: we must gather up all the bindings from doing this solving; hence + -- (runTcSWithEvBinds ev_binds_var). And note that since there are + -- nested implications, calling solveWanteds will side-effect their + -- evidence bindings, so we can't just revert to the input constraint. + -- + -- See also Note [Inferring principal types] ; ev_binds_var <- TcM.newTcEvBinds ; psig_evs <- newWanteds AnnOrigin psig_theta ; wanted_transformed <- runTcSWithEvBinds ev_binds_var $ - setTcLevelTcS rhs_tclvl $ -- ToDo: describe subtle placement + setTcLevelTcS rhs_tclvl $ solveWanteds (mkSimpleWC psig_evs `andWC` wanteds) + -- setLevelTcS: we do setLevel /inside/ the runTcS, so that + -- we initialise the InertSet inert_given_eq_lvl as far + -- out as possible, maximising oppportunities to unify -- psig_evs : see Note [Add signature contexts as wanteds] - -- See Note [Inferring principal types] -- Find quant_pred_candidates, the predicates that -- we'll consider quantifying over ===================================== compiler/GHC/Tc/Solver/InertSet.hs ===================================== @@ -678,6 +678,23 @@ should update inert_given_eq_lvl? imply nominal ones. For example, if (G a ~R G b) and G's argument's role is nominal, then we can deduce a ~N b. +(TEG6) A subtle point is this: when initialising the solver, giving it + an empty InertSet, we must conservatively initialise `inert_given_lvl` + to the /current/ TcLevel. This matters when doing let-generalisation. + Consider #26004: + f w e = case e of + T1 -> let y = not w in False -- T1 is a GADT + T2 -> True + When let-generalising `y`, we will have (w :: alpha[1]) in the type + envt; and we are under GADT pattern match. So when we solve the + constraints from y's RHS, in simplifyInfer, we must NOT unify + alpha[1] := Bool + Since we don't know what enclosing equalities there are, we just + conservatively assume that there are some. + + This initialisation in done in `runTcSWithEvBinds`, which passes + the current TcLevl to `emptyInert`. + Historical note: prior to #24938 we also ignored Given equalities that did not mention an "outer" type variable. But that is wrong, as #24938 showed. Another example is immortalised in test LocalGivenEqs2 ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -1224,8 +1224,13 @@ runTcSWithEvBinds' :: TcSMode runTcSWithEvBinds' mode ev_binds_var tcs = do { unified_var <- TcM.newTcRef 0 ; step_count <- TcM.newTcRef 0 + + -- Make a fresh, empty inert set + -- Subtle point: see (TEG6) in Note [Tracking Given equalities] + -- in GHC.Tc.Solver.InertSet ; tc_lvl <- TcM.getTcLevel ; inert_var <- TcM.newTcRef (emptyInert tc_lvl) + ; wl_var <- TcM.newTcRef emptyWorkList ; unif_lvl_var <- TcM.newTcRef Nothing ; let env = TcSEnv { tcs_ev_binds = ev_binds_var View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/99fc2a5b545cad180859a55109afb58… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/99fc2a5b545cad180859a55109afb58… You're receiving this email because of your account on gitlab.haskell.org.

1 0

[Git][ghc/ghc][wip/T26004] 3 commits: Wibbles
by Simon Peyton Jones (＠simonpj) 01 May '25

01 May '25

Simon Peyton Jones pushed to branch wip/T26004 at Glasgow Haskell Compiler / GHC Commits: 731d1d93 by Simon Peyton Jones at 2025-05-01T11:35:23+01:00 Wibbles - - - - - 6f213c9d by Simon Peyton Jones at 2025-05-01T11:39:37+01:00 Add test for T26004 - - - - - db5c721f by Simon Peyton Jones at 2025-05-01T11:48:46+01:00 Error messages improve - - - - - 6 changed files: - compiler/GHC/Tc/Solver.hs - compiler/GHC/Tc/Types/Constraint.hs - + testsuite/tests/typecheck/should_fail/T26004.hs - + testsuite/tests/typecheck/should_fail/T26004.stderr - testsuite/tests/typecheck/should_fail/T7453.stderr - testsuite/tests/typecheck/should_fail/all.T Changes: ===================================== compiler/GHC/Tc/Solver.hs ===================================== @@ -1430,15 +1430,15 @@ decideAndPromoteTyVars top_lvl rhs_tclvl infer_mode name_taus psigs wanted -- Step 1 of Note [decideAndPromoteTyVars] -- Get candidate constraints, decide which we can potentially quantify - (can_quant_cts, no_quant_cts) = approximateWCX wanted + -- The `no_quant_tvs` are free in constraints we can't quantify. + (can_quant_cts, no_quant_tvs) = approximateWCX False wanted can_quant = ctsPreds can_quant_cts - no_quant = ctsPreds no_quant_cts can_quant_tvs = tyCoVarsOfTypes can_quant - no_quant_tvs = tyCoVarsOfTypes no_quant -- Step 2 of Note [decideAndPromoteTyVars] -- Apply the monomorphism restriction (post_mr_quant, mr_no_quant) = applyMR dflags infer_mode can_quant + mr_no_quant_tvs = tyCoVarsOfTypes mr_no_quant -- The co_var_tvs are tvs mentioned in the types of covars or -- coercion holes. We can't quantify over these covars, so we @@ -1457,9 +1457,10 @@ decideAndPromoteTyVars top_lvl rhs_tclvl infer_mode name_taus psigs wanted -- Step 3 of Note [decideAndPromoteTyVars], (a-c) -- Identify mono_tvs: the type variables that we must not quantify over + -- At top level we are much less keen to create mono tyvars, to avoid + -- spooky action at a distance. mono_tvs_without_mr --- This does not work well (#26004) --- | is_top_level = outer_tvs + | is_top_level = outer_tvs -- See (DP2) | otherwise = outer_tvs -- (a) `unionVarSet` no_quant_tvs -- (b) `unionVarSet` co_var_tvs -- (c) @@ -1469,7 +1470,7 @@ decideAndPromoteTyVars top_lvl rhs_tclvl infer_mode name_taus psigs wanted = -- Even at top level, we don't quantify over type variables -- mentioned in constraints that the MR tells us not to quantify -- See Note [decideAndPromoteTyVars] (DP2) - mono_tvs_without_mr `unionVarSet` tyCoVarsOfTypes mr_no_quant + mono_tvs_without_mr `unionVarSet` mr_no_quant_tvs -------------------------------------------------------------------- -- Step 4 of Note [decideAndPromoteTyVars] @@ -1523,7 +1524,7 @@ decideAndPromoteTyVars top_lvl rhs_tclvl infer_mode name_taus psigs wanted , text "newly_mono_tvs =" <+> ppr newly_mono_tvs , text "can_quant =" <+> ppr can_quant , text "post_mr_quant =" <+> ppr post_mr_quant - , text "no_quant =" <+> ppr no_quant + , text "no_quant_tvs =" <+> ppr no_quant_tvs , text "mr_no_quant =" <+> ppr mr_no_quant , text "final_quant =" <+> ppr final_quant , text "co_vars =" <+> ppr co_vars ] @@ -1648,9 +1649,22 @@ Wrinkles promote type variables. But for bindings affected by the MR we have no choice but to promote. + An example is in #26004. + f w e = case e of + T1 -> let y = not w in False + T2 -> True + When generalising `f` we have a constraint + forall. (a ~ Bool) => alpha ~ Bool + where our provisional type for `f` is `f :: T alpha -> blah`. + In a /nested/ setting, we might simply not-generalise `f`, hoping to learn + about `alpha` from f's call sites (test T5266b is an example). But at top + level, to avoid spooky action at a distance. + Note [The top-level Any principle] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Key principle: we never want to show the programmer a type with `Any` in it. +Key principles: + * we never want to show the programmer a type with `Any` in it. + * avoid "spooky action at a distance" and silent defaulting Most /top level/ bindings have a type signature, so none of this arises. But where a top-level binding lacks a signature, we don't want to infer a type like @@ -1659,11 +1673,18 @@ and then subsequently default alpha[0]:=Any. Exposing `Any` to the user is bad bad bad. Better to report an error, which is what may well happen if we quantify over alpha instead. +Moreover, + * If (elsewhere in this module) we add a call to `f`, say (f True), then + `f` will get the type `Bool -> Int` + * If we add /another/ call, say (f 'x'), we will then get a type error. + * If we have no calls, the final exported type of `f` may get set by + defaulting, and might not be principal (#26004). + For /nested/ bindings, a monomorphic type like `f :: alpha[0] -> Int` is fine, because we can see all the call sites of `f`, and they will probably fix `alpha`. In contrast, we can't see all of (or perhaps any of) the calls of top-level (exported) functions, reducing the worries about "spooky action at a -distance". +distance". This also moves in the direction of `MonoLocalBinds`, which we like. Note [Do not quantify over constraints that determine a variable] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ===================================== compiler/GHC/Tc/Types/Constraint.hs ===================================== @@ -1743,24 +1743,21 @@ will be able to report a more informative error: ************************************************************************ -} -type ApproxWC = ( Bag Ct -- Free quantifiable constraints - , Bag Ct ) -- Free non-quantifiable constraints - -- due to shape, or enclosing equality +type ApproxWC = ( Bag Ct -- Free quantifiable constraints + , TcTyCoVarSet ) -- Free vars of non-quantifiable constraints + -- due to shape, or enclosing equality approximateWC :: Bool -> WantedConstraints -> Bag Ct approximateWC include_non_quantifiable cts - | include_non_quantifiable = quant `unionBags` no_quant - | otherwise = quant - where - (quant, no_quant) = approximateWCX cts + = fst (approximateWCX include_non_quantifiable cts) -approximateWCX :: WantedConstraints -> ApproxWC +approximateWCX :: Bool -> WantedConstraints -> ApproxWC -- The "X" means "extended"; -- we return both quantifiable and non-quantifiable constraints -- See Note [ApproximateWC] -- See Note [floatKindEqualities vs approximateWC] -approximateWCX wc - = float_wc False emptyVarSet wc (emptyBag, emptyBag) +approximateWCX include_non_quantifiable wc + = float_wc False emptyVarSet wc (emptyBag, emptyVarSet) where float_wc :: Bool -- True <=> there are enclosing equalities -> TcTyCoVarSet -- Enclosing skolem binders @@ -1786,17 +1783,23 @@ approximateWCX wc -- There can be (insoluble) Given constraints in wc_simple, -- there so that we get error reports for unreachable code -- See `given_insols` in GHC.Tc.Solver.Solve.solveImplication - | insolubleCt ct = acc - | tyCoVarsOfCt ct `intersectsVarSet` skol_tvs = acc - | otherwise - = case classifyPredType (ctPred ct) of + | insolubleCt ct = acc + | pred_tvs `intersectsVarSet` skol_tvs = acc + | include_non_quantifiable = add_to_quant + | is_quantifiable encl_eqs (ctPred ct) = add_to_quant + | otherwise = add_to_no_quant + where + pred = ctPred ct + pred_tvs = tyCoVarsOfType pred + add_to_quant = (ct `consBag` quant, no_quant) + add_to_no_quant = (quant, no_quant `unionVarSet` pred_tvs) + + is_quantifiable encl_eqs pred + = case classifyPredType pred of -- See the classification in Note [ApproximateWC] EqPred eq_rel ty1 ty2 - | encl_eqs -> acc - | quantify_equality eq_rel ty1 ty2 -> add_to_quant - | otherwise -> add_to_no_quant - -- encl_eqs: See Wrinkle (W1) - -- ToDo: explain acc + | encl_eqs -> False -- encl_eqs: See Wrinkle (W1) + | otherwise -> quantify_equality eq_rel ty1 ty2 ClassPred cls tys | Just {} <- isCallStackPred cls tys @@ -1804,17 +1807,14 @@ approximateWCX wc -- the constraints bubble up to be solved from the outer -- context, or be defaulted when we reach the top-level. -- See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence - -> add_to_no_quant + -> False | otherwise - -> add_to_quant -- See Wrinkle (W2) + -> True -- See Wrinkle (W2) - IrredPred {} -> add_to_quant -- See Wrinkle (W2) + IrredPred {} -> True -- See Wrinkle (W2) - ForAllPred {} -> add_to_no_quant -- Never quantify these - where - add_to_quant = (ct `consBag` quant, no_quant) - add_to_no_quant = (quant, ct `consBag` no_quant) + ForAllPred {} -> False -- Never quantify these -- See Note [Quantifying over equality constraints] quantify_equality NomEq ty1 ty2 = quant_fun ty1 || quant_fun ty2 ===================================== testsuite/tests/typecheck/should_fail/T26004.hs ===================================== @@ -0,0 +1,14 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE NoMonoLocalBinds #-} + +module T26004 where + +data T a where + T1 :: T Bool + T2 :: T a + +-- This funcion should be rejected: +-- we should not infer a non-principal type for `f` +f w e = case e of + T1 -> let y = not w in False + T2 -> True ===================================== testsuite/tests/typecheck/should_fail/T26004.stderr ===================================== @@ -0,0 +1,17 @@ + +T26004.hs:13:21: error: [GHC-25897] + • Could not deduce ‘p ~ Bool’ + from the context: a ~ Bool + bound by a pattern with constructor: T1 :: T Bool, + in a case alternative + at T26004.hs:13:3-4 + ‘p’ is a rigid type variable bound by + the inferred type of f :: p -> T a -> Bool + at T26004.hs:(12,1)-(14,12) + • In the first argument of ‘not’, namely ‘w’ + In the expression: not w + In an equation for ‘y’: y = not w + • Relevant bindings include + w :: p (bound at T26004.hs:12:3) + f :: p -> T a -> Bool (bound at T26004.hs:12:1) + Suggested fix: Consider giving ‘f’ a type signature ===================================== testsuite/tests/typecheck/should_fail/T7453.stderr ===================================== @@ -1,8 +1,5 @@ - -T7453.hs:9:15: error: [GHC-25897] - • Couldn't match type ‘t’ with ‘p’ - Expected: Id t - Actual: Id p +T7453.hs:10:30: error: [GHC-25897] + • Couldn't match expected type ‘t’ with actual type ‘p’ ‘t’ is a rigid type variable bound by the type signature for: z :: forall t. Id t @@ -10,29 +7,17 @@ T7453.hs:9:15: error: [GHC-25897] ‘p’ is a rigid type variable bound by the inferred type of cast1 :: p -> a at T7453.hs:(7,1)-(10,30) - • In the expression: aux - In an equation for ‘z’: - z = aux - where - aux = Id v - In an equation for ‘cast1’: - cast1 v - = runId z - where - z :: Id t - z = aux - where - aux = Id v + • In the first argument of ‘Id’, namely ‘v’ + In the expression: Id v + In an equation for ‘aux’: aux = Id v • Relevant bindings include - aux :: Id p (bound at T7453.hs:10:21) + aux :: Id t (bound at T7453.hs:10:21) z :: Id t (bound at T7453.hs:9:11) v :: p (bound at T7453.hs:7:7) cast1 :: p -> a (bound at T7453.hs:7:1) -T7453.hs:15:15: error: [GHC-25897] - • Couldn't match type ‘t1’ with ‘p’ - Expected: () -> t1 - Actual: () -> p +T7453.hs:16:33: error: [GHC-25897] + • Couldn't match expected type ‘t1’ with actual type ‘p’ ‘t1’ is a rigid type variable bound by the type signature for: z :: forall t1. () -> t1 @@ -40,21 +25,11 @@ T7453.hs:15:15: error: [GHC-25897] ‘p’ is a rigid type variable bound by the inferred type of cast2 :: p -> t at T7453.hs:(13,1)-(16,33) - • In the expression: aux - In an equation for ‘z’: - z = aux - where - aux = const v - In an equation for ‘cast2’: - cast2 v - = z () - where - z :: () -> t - z = aux - where - aux = const v + • In the first argument of ‘const’, namely ‘v’ + In the expression: const v + In an equation for ‘aux’: aux = const v • Relevant bindings include - aux :: forall {b}. b -> p (bound at T7453.hs:16:21) + aux :: b -> t1 (bound at T7453.hs:16:21) z :: () -> t1 (bound at T7453.hs:15:11) v :: p (bound at T7453.hs:13:7) cast2 :: p -> t (bound at T7453.hs:13:1) @@ -86,3 +61,4 @@ T7453.hs:21:15: error: [GHC-25897] z :: t1 (bound at T7453.hs:21:11) v :: p (bound at T7453.hs:19:7) cast3 :: p -> t (bound at T7453.hs:19:1) + ===================================== testsuite/tests/typecheck/should_fail/all.T ===================================== @@ -735,3 +735,4 @@ test('T24938', normal, compile_fail, ['']) test('T25325', normal, compile_fail, ['']) test('T25004', normal, compile_fail, ['']) test('T25004k', normal, compile_fail, ['']) +test('T26004', normal, compile_fail, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/ca6cd646c542ede632511448546b2c… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/ca6cd646c542ede632511448546b2c… You're receiving this email because of your account on gitlab.haskell.org.

1 0

[Git][ghc/ghc] Pushed new branch wip/9.10.2-final
by Zubin (＠wz1000) 01 May '25

01 May '25

Zubin pushed new branch wip/9.10.2-final at Glasgow Haskell Compiler / GHC -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/tree/wip/9.10.2-final You're receiving this email because of your account on gitlab.haskell.org.

1 0

[Git][ghc/ghc][wip/marge_bot_batch_merge_job] 4 commits: get-win32-tarballs.py: List tarball files to be downloaded if we cannot find them
by Marge Bot (＠marge-bot) 01 May '25

01 May '25

Marge Bot pushed to branch wip/marge_bot_batch_merge_job at Glasgow Haskell Compiler / GHC Commits: aba2a4a5 by Zubin Duggal at 2025-04-30T06:35:59-04:00 get-win32-tarballs.py: List tarball files to be downloaded if we cannot find them Fixes #25929 - - - - - d99a617b by Ben Gamari at 2025-04-30T06:36:40-04:00 Move Data ModuleName instance to Language.Haskell.Syntax.Module.Name Fixes #25968. - - - - - b24e95f1 by Serge S. Gulin at 2025-05-01T00:01:53+03:00 Support for ARM64 Windows (LLVM-enabled) (fixes #24603) submodule Co-authored-by: Cheng Shao <terrorjack(a)type.dance> Co-authored-by: Dmitrii Egorov <egorov.d.i(a)icloud.com> Co-authored-by: Andrei Borzenkov <root(a)sandwitch.dev> - - - - - 55a09eb4 by Javran Cheng at 2025-05-01T04:31:00-04:00 Suppress unused do-binding if discarded variable is Any or ZonkAny. Consider example (#25895): > do { forever (return ()); blah } where `forever :: forall a b. IO a -> IO b`. Nothing constrains `b`, so it will be instantiates with `Any` or `ZonkAny`. But we certainly don't want to complain about a discarded do-binding. Fixes #25895 - - - - - 43 changed files: - .gitlab-ci.yml - .gitlab/ci.sh - .gitlab/generate-ci/gen_ci.hs - .gitlab/hello.hs - .gitlab/jobs.yaml - compiler/CodeGen.Platform.h - compiler/GHC/Builtin/Types.hs - compiler/GHC/CmmToAsm/AArch64/CodeGen.hs - compiler/GHC/CmmToAsm/AArch64/Instr.hs - compiler/GHC/CmmToAsm/AArch64/Ppr.hs - compiler/GHC/CmmToAsm/Reg/Linear/AArch64.hs - compiler/GHC/Driver/Session.hs - compiler/GHC/HsToCore/Expr.hs - compiler/GHC/Platform/Regs.hs - compiler/GHC/Tc/Utils/TcType.hs - compiler/GHC/Unit/Types.hs - compiler/Language/Haskell/Syntax/Module/Name.hs - hadrian/src/Oracles/Setting.hs - hadrian/src/Rules/BinaryDist.hs - libraries/Cabal - libraries/Win32 - libraries/base/src/System/CPUTime/Windows.hsc - libraries/base/tests/perf/encodingAllocations.hs - libraries/directory - libraries/ghc-internal/jsbits/errno.js - libraries/ghc-internal/src/GHC/Internal/System/Posix/Internals.hs - libraries/haskeline - libraries/process - libraries/unix - llvm-targets - m4/fp_cc_supports_target.m4 - m4/fp_setup_windows_toolchain.m4 - m4/fptools_set_platform_vars.m4 - m4/ghc_tables_next_to_code.m4 - rts/StgCRun.c - rts/linker/PEi386.c - rts/win32/veh_excn.c - testsuite/tests/ghc-api/fixed-nodes/all.T - testsuite/tests/interface-stability/base-exports.stdout-javascript-unknown-ghcjs - testsuite/tests/printer/T17697.stderr - utils/ghc-toolchain/exe/Main.hs - utils/hsc2hs - utils/llvm-targets/gen-data-layout.sh The diff was not included because it is too large. View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/319b4d1024fa03a117e76e4a5a3cb8… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/319b4d1024fa03a117e76e4a5a3cb8… You're receiving this email because of your account on gitlab.haskell.org.

1 0

[Git][ghc/ghc] Pushed new branch wip/T25943
by Ben Gamari (＠bgamari) 01 May '25

01 May '25

Ben Gamari pushed new branch wip/T25943 at Glasgow Haskell Compiler / GHC -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/tree/wip/T25943 You're receiving this email because of your account on gitlab.haskell.org.

1 0