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/ca6cd646c542ede632511448546b2ca... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/ca6cd646c542ede632511448546b2ca... You're receiving this email because of your account on gitlab.haskell.org.