Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC Commits: 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 - - - - - 9 changed files: - compiler/GHC/HsToCore/Pmc/Solver/Types.hs - compiler/GHC/Tc/Solver.hs - compiler/GHC/Tc/Solver/InertSet.hs - compiler/GHC/Tc/Solver/Monad.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/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/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 ===================================== @@ -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 - | 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 +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 @@ -1852,7 +1852,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 ===================================== 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/-/commit/165f98d86f59b783511f8015dc1e5471... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/165f98d86f59b783511f8015dc1e5471... You're receiving this email because of your account on gitlab.haskell.org.