Simon Peyton Jones pushed to branch wip/T26015 at Glasgow Haskell Compiler / GHC Commits: e46c6b18 by Rodrigo Mesquita at 2025-05-06T09:01:57-04:00 Refactor mkTopLevImportedEnv out of mkTopLevEnv This makes the code clearer and allows the top-level import context to be fetched directly from the HomeModInfo through the API (e.g. useful for the debugger). - - - - - 0ce0d263 by Rodrigo Mesquita at 2025-05-06T09:01:57-04:00 Export sizeOccEnv from GHC.Types.Name.Occurrence Counts the number of OccNames in an OccEnv - - - - - 165f98d8 by Simon Peyton Jones at 2025-05-06T09:02:39-04:00 Fix a bad untouchability bug im simplifyInfer This patch addresses #26004. The root cause was that simplifyInfer was willing to unify variables "far out". The fix, in runTcSWithEvBinds', is to initialise the inert set given-eq level with the current level. See (TGE6) in Note [Tracking Given equalities] in GHC.Tc.Solver.InertSet Two loosely related refactors: * Refactored approximateWCX to return just the free type variables of the un-quantified constraints. That avoids duplication of work (these free vars are needed in simplifyInfer) and makes it clearer that the constraints themselves are irrelevant. * A little local refactor of TcSMode, which reduces the number of parameters to runTcSWithEvBinds - - - - - 6a7d917b by Simon Peyton Jones at 2025-05-08T09:28:29+01:00 Slighty improve `dropMisleading` Fix #26105, by upgrading the (horrible, hacky) `dropMisleading` function. This fix makes things a bit better but does not cure the underlying problem. - - - - - 14 changed files: - compiler/GHC/HsToCore/Pmc/Solver/Types.hs - compiler/GHC/Runtime/Eval.hs - compiler/GHC/Tc/Solver.hs - compiler/GHC/Tc/Solver/InertSet.hs - compiler/GHC/Tc/Solver/Monad.hs - compiler/GHC/Tc/Types/Constraint.hs - compiler/GHC/Tc/Utils/Monad.hs - compiler/GHC/Types/Name/Occurrence.hs - + testsuite/tests/typecheck/should_fail/T26004.hs - + testsuite/tests/typecheck/should_fail/T26004.stderr - + testsuite/tests/typecheck/should_fail/T26015.hs - + testsuite/tests/typecheck/should_fail/T26015.stderr - testsuite/tests/typecheck/should_fail/T7453.stderr - testsuite/tests/typecheck/should_fail/all.T Changes: ===================================== compiler/GHC/HsToCore/Pmc/Solver/Types.hs ===================================== @@ -64,7 +64,7 @@ import GHC.Builtin.Names import GHC.Builtin.Types import GHC.Builtin.Types.Prim import GHC.Tc.Solver.InertSet (InertSet, emptyInert) -import GHC.Tc.Utils.TcType (isStringTy) +import GHC.Tc.Utils.TcType (isStringTy, topTcLevel) import GHC.Types.CompleteMatch import GHC.Types.SourceText (SourceText(..), mkFractionalLit, FractionalLit , fractionalLitFromRational @@ -129,7 +129,7 @@ instance Outputable TyState where ppr (TySt n inert) = ppr n <+> ppr inert initTyState :: TyState -initTyState = TySt 0 emptyInert +initTyState = TySt 0 (emptyInert topTcLevel) -- | The term oracle state. Stores 'VarInfo' for encountered 'Id's. These -- entries are possibly shared when we figure out that two variables must be ===================================== compiler/GHC/Runtime/Eval.hs ===================================== @@ -23,7 +23,7 @@ module GHC.Runtime.Eval ( setupBreakpoint, back, forward, setContext, getContext, - mkTopLevEnv, + mkTopLevEnv, mkTopLevImportedEnv, getNamesInScope, getRdrNamesInScope, moduleIsInterpreted, @@ -836,29 +836,36 @@ mkTopLevEnv hsc_env modl Nothing -> pure $ Left "not a home module" Just details -> case mi_top_env (hm_iface details) of - (IfaceTopEnv exports imports) -> do - imports_env <- - runInteractiveHsc hsc_env - $ ioMsgMaybe $ hoistTcRnMessage $ runTcInteractive hsc_env - $ fmap (foldr plusGlobalRdrEnv emptyGlobalRdrEnv) - $ forM imports $ \iface_import -> do - let ImpUserSpec spec details = tcIfaceImport iface_import - iface <- loadInterfaceForModule (text "imported by GHCi") (is_mod spec) - pure $ case details of - ImpUserAll -> importsFromIface hsc_env iface spec Nothing - ImpUserEverythingBut ns -> importsFromIface hsc_env iface spec (Just ns) - ImpUserExplicit x _parents_of_implicits -> - -- TODO: Not quite right, is_explicit should refer to whether the user wrote A(..) or A(x,y). - -- It is only used for error messages. It seems dubious even to add an import context to these GREs as - -- they are not "imported" into the top-level scope of the REPL. I changed this for now so that - -- the test case produce the same output as before. - let spec' = ImpSpec { is_decl = spec, is_item = ImpSome { is_explicit = True, is_iloc = noSrcSpan } } - in mkGlobalRdrEnv $ gresFromAvails hsc_env (Just spec') x + (IfaceTopEnv exports _imports) -> do + imports_env <- mkTopLevImportedEnv hsc_env details let exports_env = mkGlobalRdrEnv $ gresFromAvails hsc_env Nothing (getDetOrdAvails exports) pure $ Right $ plusGlobalRdrEnv imports_env exports_env where hpt = hsc_HPT hsc_env +-- | Make the top-level environment with all bindings imported by this module. +-- Exported bindings from this module are not included in the result. +mkTopLevImportedEnv :: HscEnv -> HomeModInfo -> IO GlobalRdrEnv +mkTopLevImportedEnv hsc_env details = do + runInteractiveHsc hsc_env + $ ioMsgMaybe $ hoistTcRnMessage $ runTcInteractive hsc_env + $ fmap (foldr plusGlobalRdrEnv emptyGlobalRdrEnv) + $ forM imports $ \iface_import -> do + let ImpUserSpec spec details = tcIfaceImport iface_import + iface <- loadInterfaceForModule (text "imported by GHCi") (is_mod spec) + pure $ case details of + ImpUserAll -> importsFromIface hsc_env iface spec Nothing + ImpUserEverythingBut ns -> importsFromIface hsc_env iface spec (Just ns) + ImpUserExplicit x _parents_of_implicits -> + -- TODO: Not quite right, is_explicit should refer to whether the user wrote A(..) or A(x,y). + -- It is only used for error messages. It seems dubious even to add an import context to these GREs as + -- they are not "imported" into the top-level scope of the REPL. I changed this for now so that + -- the test case produce the same output as before. + let spec' = ImpSpec { is_decl = spec, is_item = ImpSome { is_explicit = True, is_iloc = noSrcSpan } } + in mkGlobalRdrEnv $ gresFromAvails hsc_env (Just spec') x + where + IfaceTopEnv _ imports = mi_top_env (hm_iface details) + -- | Get the interactive evaluation context, consisting of a pair of the -- set of modules from which we take the full top-level scope, and the set -- of modules from which we take just the exports respectively. ===================================== 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 - <- setTcLevel rhs_tclvl $ - runTcSWithEvBinds ev_binds_var $ + <- runTcSWithEvBinds ev_binds_var $ + 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 @@ -1430,13 +1431,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 -- 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 @@ -1448,30 +1451,33 @@ decideAndPromoteTyVars top_lvl rhs_tclvl infer_mode name_taus psigs wanted ++ tau_tys ++ post_mr_quant) co_var_tvs = closeOverKinds co_vars - -- outer_tvs are mentioned in `wanted, and belong to some outer level. + -- outer_tvs are mentioned in `wanted`, and belong to some outer level. -- We definitely can't quantify over them outer_tvs = outerLevelTyVars rhs_tclvl $ - tyCoVarsOfTypes can_quant `unionVarSet` tyCoVarsOfTypes no_quant + can_quant_tvs `unionVarSet` no_quant_tvs - -- Step 3 of Note [decideAndPromoteTyVars] + -- 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 - | is_top_level = outer_tvs - | otherwise = outer_tvs -- (a) - `unionVarSet` tyCoVarsOfTypes no_quant -- (b) - `unionVarSet` co_var_tvs -- (c) + | is_top_level = outer_tvs -- See (DP2) + | otherwise = outer_tvs -- (a) + `unionVarSet` no_quant_tvs -- (b) + `unionVarSet` co_var_tvs -- (c) + -- Step 3 of Note [decideAndPromoteTyVars], (d) mono_tvs_with_mr = -- 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] -- Use closeWrtFunDeps to find any other variables that are determined by mono_tvs - add_determined tvs = closeWrtFunDeps post_mr_quant tvs - `delVarSetList` psig_qtvs + add_determined tvs preds = closeWrtFunDeps preds tvs + `delVarSetList` psig_qtvs -- Why delVarSetList psig_qtvs? -- If the user has explicitly asked for quantification, then that -- request "wins" over the MR. @@ -1480,8 +1486,8 @@ decideAndPromoteTyVars top_lvl rhs_tclvl infer_mode name_taus psigs wanted -- (i.e. says "no" to isQuantifiableTv)? That's OK: explanation -- in Step 2 of Note [Deciding quantification]. - mono_tvs_with_mr_det = add_determined mono_tvs_with_mr - mono_tvs_without_mr_det = add_determined mono_tvs_without_mr + mono_tvs_with_mr_det = add_determined mono_tvs_with_mr post_mr_quant + mono_tvs_without_mr_det = add_determined mono_tvs_without_mr can_quant -------------------------------------------------------------------- -- Step 5 of Note [decideAndPromoteTyVars] @@ -1518,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 ] @@ -1605,8 +1611,8 @@ The plan The body of z tries to unify the type of x (call it alpha[1]) with (beta[2] -> gamma[2]). This unification fails because alpha is untouchable, leaving [W] alpha[1] ~ (beta[2] -> gamma[2]) - We need to know not to quantify over beta or gamma, because they are in the - equality constraint with alpha. Actual test case: typecheck/should_compile/tc213 + We don't want to quantify over beta or gamma because they are fixed by alpha, + which is monomorphic. Actual test case: typecheck/should_compile/tc213 Another example. Suppose we have class C a b | a -> b @@ -1643,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 @@ -1654,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/Solver/InertSet.hs ===================================== @@ -374,20 +374,20 @@ instance Outputable InertSet where where dicts = bagToList (dictsToBag solved_dicts) -emptyInertCans :: InertCans -emptyInertCans +emptyInertCans :: TcLevel -> InertCans +emptyInertCans given_eq_lvl = IC { inert_eqs = emptyTyEqs , inert_funeqs = emptyFunEqs - , inert_given_eq_lvl = topTcLevel + , inert_given_eq_lvl = given_eq_lvl , inert_given_eqs = False , inert_dicts = emptyDictMap , inert_safehask = emptyDictMap , inert_insts = [] , inert_irreds = emptyBag } -emptyInert :: InertSet -emptyInert - = IS { inert_cans = emptyInertCans +emptyInert :: TcLevel -> InertSet +emptyInert given_eq_lvl + = IS { inert_cans = emptyInertCans given_eq_lvl , inert_cycle_breakers = emptyBag :| [] , inert_famapp_cache = emptyFunEqs , inert_solved_dicts = emptyDictMap } @@ -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. +(TGE6) 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 ===================================== @@ -20,7 +20,7 @@ module GHC.Tc.Solver.Monad ( runTcSSpecPrag, failTcS, warnTcS, addErrTcS, wrapTcS, ctLocWarnTcS, runTcSEqualities, - nestTcS, nestImplicTcS, setEvBindsTcS, + nestTcS, nestImplicTcS, setEvBindsTcS, setTcLevelTcS, emitImplicationTcS, emitTvImplicationTcS, emitImplication, emitFunDepWanteds, @@ -947,8 +947,9 @@ added. This is initialised from the innermost implication constraint. -- | See Note [TcSMode] data TcSMode = TcSVanilla -- ^ Normal constraint solving + | TcSPMCheck -- ^ Used when doing patterm match overlap checks | TcSEarlyAbort -- ^ Abort early on insoluble constraints - | TcSSpecPrag -- ^ Fully solve all constraints + | TcSSpecPrag -- ^ Fully solve all constraints deriving (Eq) {- Note [TcSMode] @@ -957,6 +958,11 @@ The constraint solver can operate in different modes: * TcSVanilla: Normal constraint solving mode. This is the default. +* TcSPMCheck: Used by the pattern match overlap checker. + Like TcSVanilla, but the idea is that the returned InertSet will + later be resumed, so we do not want to restore type-equality cycles + See also Note [Type equality cycles] in GHC.Tc.Solver.Equality + * TcSEarlyAbort: Abort (fail in the monad) as soon as we come across an insoluble constraint. This is used to fail-fast when checking for hole-fits. See Note [Speeding up valid hole-fits]. @@ -1135,7 +1141,7 @@ runTcS tcs runTcSEarlyAbort :: TcS a -> TcM a runTcSEarlyAbort tcs = do { ev_binds_var <- TcM.newTcEvBinds - ; runTcSWithEvBinds' True TcSEarlyAbort ev_binds_var tcs } + ; runTcSWithEvBinds' TcSEarlyAbort ev_binds_var tcs } -- | Run the 'TcS' monad in 'TcSSpecPrag' mode, which either fully solves -- individual Wanted quantified constraints or leaves them alone. @@ -1143,7 +1149,7 @@ runTcSEarlyAbort tcs -- See Note [TcSSpecPrag]. runTcSSpecPrag :: EvBindsVar -> TcS a -> TcM a runTcSSpecPrag ev_binds_var tcs - = runTcSWithEvBinds' True TcSSpecPrag ev_binds_var tcs + = runTcSWithEvBinds' TcSSpecPrag ev_binds_var tcs {- Note [TcSSpecPrag] ~~~~~~~~~~~~~~~~~~~~~ @@ -1200,7 +1206,7 @@ runTcSEqualities thing_inside runTcSInerts :: InertSet -> TcS a -> TcM (a, InertSet) runTcSInerts inerts tcs = do ev_binds_var <- TcM.newTcEvBinds - runTcSWithEvBinds' False TcSVanilla ev_binds_var $ do + runTcSWithEvBinds' TcSPMCheck ev_binds_var $ do setInertSet inerts a <- tcs new_inerts <- getInertSet @@ -1209,21 +1215,23 @@ runTcSInerts inerts tcs = do runTcSWithEvBinds :: EvBindsVar -> TcS a -> TcM a -runTcSWithEvBinds = runTcSWithEvBinds' True TcSVanilla +runTcSWithEvBinds = runTcSWithEvBinds' TcSVanilla -runTcSWithEvBinds' :: Bool -- True <=> restore type equality cycles - -- Don't if you want to reuse the InertSet. - -- See also Note [Type equality cycles] - -- in GHC.Tc.Solver.Equality - -> TcSMode +runTcSWithEvBinds' :: TcSMode -> EvBindsVar -> TcS a -> TcM a -runTcSWithEvBinds' restore_cycles mode ev_binds_var tcs +runTcSWithEvBinds' mode ev_binds_var tcs = do { unified_var <- TcM.newTcRef 0 - ; step_count <- TcM.newTcRef 0 - ; inert_var <- TcM.newTcRef emptyInert - ; wl_var <- TcM.newTcRef emptyWorkList + ; step_count <- TcM.newTcRef 0 + + -- Make a fresh, empty inert set + -- Subtle point: see (TGE6) 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 , tcs_unified = unified_var @@ -1240,9 +1248,13 @@ runTcSWithEvBinds' restore_cycles mode ev_binds_var tcs ; when (count > 0) $ csTraceTcM $ return (text "Constraint solver steps =" <+> int count) - ; when restore_cycles $ - do { inert_set <- TcM.readTcRef inert_var - ; restoreTyVarCycles inert_set } + -- Restore tyvar cycles: see Note [Type equality cycles] in + -- GHC.Tc.Solver.Equality + -- But /not/ in TCsPMCheck mode: see Note [TcSMode] + ; case mode of + TcSPMCheck -> return () + _ -> do { inert_set <- TcM.readTcRef inert_var + ; restoreTyVarCycles inert_set } #if defined(DEBUG) ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var @@ -1284,6 +1296,10 @@ setEvBindsTcS :: EvBindsVar -> TcS a -> TcS a setEvBindsTcS ref (TcS thing_inside) = TcS $ \ env -> thing_inside (env { tcs_ev_binds = ref }) +setTcLevelTcS :: TcLevel -> TcS a -> TcS a +setTcLevelTcS lvl (TcS thing_inside) + = TcS $ \ env -> TcM.setTcLevel lvl (thing_inside env) + nestImplicTcS :: EvBindsVar -> TcLevel -> TcS a -> TcS a ===================================== compiler/GHC/Tc/Types/Constraint.hs ===================================== @@ -1181,9 +1181,12 @@ dropMisleading (WC { wc_simple = simples, wc_impl = implics, wc_errors = errors , wc_impl = mapBag drop_implic implics , wc_errors = filterBag keep_delayed_error errors } - keep_ct ct = case classifyPredType (ctPred ct) of - ClassPred {} -> False - _ -> True + keep_ct ct + = case classifyPredType (ctPred ct) of + ClassPred cls _ -> isEqualityClass cls + -- isEqualityClass: see (CERR2) in Note [Constraints and errors] + -- in GHC.Tc.Utils.Monad + _ -> True keep_delayed_error (DE_Hole hole) = isOutOfScopeHole hole keep_delayed_error (DE_NotConcrete {}) = True @@ -1743,24 +1746,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 +1786,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 - | not encl_eqs -- See Wrinkle (W1) - , quantify_equality eq_rel ty1 ty2 - -> add_to_quant - | otherwise - -> add_to_no_quant + | encl_eqs -> False -- encl_eqs: See Wrinkle (W1) + | otherwise -> quantify_equality eq_rel ty1 ty2 ClassPred cls tys | Just {} <- isCallStackPred cls tys @@ -1804,17 +1810,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 @@ -1852,7 +1855,7 @@ We proceed by classifying the constraint: Wrinkle (W1) When inferring most-general types (in simplifyInfer), we - do *not* float an equality constraint if the implication binds + do *not* quantify over equality constraint if the implication binds equality constraints, because that defeats the OutsideIn story. Consider data T a where { TInt :: T Int; MkT :: T a } f TInt = 3::Int ===================================== compiler/GHC/Tc/Utils/Monad.hs ===================================== @@ -1385,11 +1385,13 @@ tryCaptureConstraints thing_inside tcTryM thing_inside -- See Note [Constraints and errors] - ; let lie_to_keep = case mb_res of - Nothing -> dropMisleading lie - Just {} -> lie - - ; return (mb_res, lie_to_keep) } + ; case mb_res of + Just {} -> return (mb_res, lie) + Nothing -> do { let pruned_lie = dropMisleading lie + ; traceTc "tryCaptureConstraints" $ + vcat [ text "lie:" <+> ppr lie + , text "dropMisleading lie:" <+> ppr pruned_lie ] + ; return (Nothing, pruned_lie) } } captureConstraints :: TcM a -> TcM (a, WantedConstraints) -- (captureConstraints m) runs m, and returns the type constraints it generates @@ -2066,28 +2068,51 @@ It's distressingly delicate though: emitted some constraints with skolem-escape problems. * If we discard too /few/ constraints, we may get the misleading - class constraints mentioned above. But we may /also/ end up taking - constraints built at some inner level, and emitting them at some - outer level, and then breaking the TcLevel invariants - See Note [TcLevel invariants] in GHC.Tc.Utils.TcType - -So dropMisleading has a horridly ad-hoc structure. It keeps only -/insoluble/ flat constraints (which are unlikely to very visibly trip -up on the TcLevel invariant, but all /implication/ constraints (except -the class constraints inside them). The implication constraints are -OK because they set the ambient level before attempting to solve any -inner constraints. Ugh! I hate this. But it seems to work. - -However note that freshly-generated constraints like (Int ~ Bool), or -((a -> b) ~ Int) are all CNonCanonical, and hence won't be flagged as -insoluble. The constraint solver does that. So they'll be discarded. -That's probably ok; but see th/5358 as a not-so-good example: - t1 :: Int - t1 x = x -- Manifestly wrong - - foo = $(...raises exception...) -We report the exception, but not the bug in t1. Oh well. Possible -solution: make GHC.Tc.Utils.Unify.uType spot manifestly-insoluble constraints. + class constraints mentioned above. + + We may /also/ end up taking constraints built at some inner level, and + emitting them (via the exception catching in `tryCaptureConstraints` at some + outer level, and then breaking the TcLevel invariants See Note [TcLevel + invariants] in GHC.Tc.Utils.TcType + +So `dropMisleading` has a horridly ad-hoc structure: + +* It keeps only /insoluble/ flat constraints (which are unlikely to very visibly + trip up on the TcLevel invariant + +* But it keeps all /implication/ constraints (except the class constraints + inside them). The implication constraints are OK because they set the ambient + level before attempting to solve any inner constraints. + +Ugh! I hate this. But it seems to work. + +Other wrinkles + +(CERR1) Note that freshly-generated constraints like (Int ~ Bool), or + ((a -> b) ~ Int) are all CNonCanonical, and hence won't be flagged as + insoluble. The constraint solver does that. So they'll be discarded. + That's probably ok; but see th/5358 as a not-so-good example: + t1 :: Int + t1 x = x -- Manifestly wrong + + foo = $(...raises exception...) + We report the exception, but not the bug in t1. Oh well. Possible + solution: make GHC.Tc.Utils.Unify.uType spot manifestly-insoluble constraints. + +(CERR2) In #26015 I found that from the constraints + [W] alpha ~ Int -- A class constraint + [W] F alpha ~# Bool -- An equality constraint + we were dropping the first (becuase it's a class constraint) but not the + second, and then getting a misleading error message from the second. As + #25607 shows, we can get not just one but a zillion bogus messages, which + conceal the one genuine error. Boo. + + For now I have added an even more ad-hoc "drop class constraints except + equality classes (~) and (~~)"; see `dropMisleading`. That just kicks the can + down the road; but this problem seems somewhat rare anyway. The code in + `dropMisleading` hasn't changed for years. + +It would be great to have a more systematic solution to this entire mess. ************************************************************************ ===================================== compiler/GHC/Types/Name/Occurrence.hs ===================================== @@ -92,6 +92,7 @@ module GHC.Types.Name.Occurrence ( plusOccEnv, plusOccEnv_C, extendOccEnv_Acc, filterOccEnv, delListFromOccEnv, delFromOccEnv, alterOccEnv, minusOccEnv, minusOccEnv_C, minusOccEnv_C_Ns, + sizeOccEnv, pprOccEnv, forceOccEnv, intersectOccEnv_C, @@ -803,6 +804,10 @@ minusOccEnv_C_Ns f (MkOccEnv as) (MkOccEnv bs) = then Nothing else Just m +sizeOccEnv :: OccEnv a -> Int +sizeOccEnv (MkOccEnv as) = + nonDetStrictFoldUFM (\ m !acc -> acc + sizeUFM m) 0 as + instance Outputable a => Outputable (OccEnv a) where ppr x = pprOccEnv ppr x ===================================== 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/T26015.hs ===================================== @@ -0,0 +1,17 @@ +{-# LANGUAGE MonoLocalBinds, GADTs, TypeFamilies #-} + +module Foo where + +type family F a +type instance F Int = Bool + +data T where + T1 :: a -> T + T2 :: Int -> T + +woo :: (a ~ Int) => Int -> F a +woo = error "urk" + +f x = case x of + T1 y -> not (woo 3) + T2 -> True ===================================== testsuite/tests/typecheck/should_fail/T26015.stderr ===================================== @@ -0,0 +1,9 @@ +T26015.hs:17:10: error: [GHC-27346] + • The data constructor ‘T2’ should have 1 argument, but has been given none + • In the pattern: T2 + In a case alternative: T2 -> True + In the expression: + case x of + T1 y -> not (woo 3) + T2 -> True + ===================================== 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/50b07512f0788fe9415010b1c6cddd9... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/50b07512f0788fe9415010b1c6cddd9... You're receiving this email because of your account on gitlab.haskell.org.