Simon Peyton Jones pushed to branch wip/T27844 at Glasgow Haskell Compiler / GHC Commits: 7807b4d3 by Simon Peyton Jones at 2026-10-12T17:01:47+01:00 Refactor and simplify solver's unification code Ticket #27844 showed that GHC's constraint solver could miss an occurs check, and thereby build an infinite type. This patch significantly simplifes the code in GHC.Tc.Solver.Equality.canEqCanLHSFinish_try_unification GHC.Tc.Solver.Equality.canEqCanLHSFinish_no_unification It is now significantly simpler, and requires much less subtle reasoning to understand. Main changes * If `canEqCanLHSFinish_try_unification` fails to unify, it now /always/ calls `canEqCanLHSFinish_no_unification` rather than trying to finish the job itself. * `GHC.Tc.Solver.Monad.checkTypeEq` is moved from Monad into Equality, and renamed to `GHC.Tc.Solver.Equality.checkTypeEqNoUnification`. * `canEqCanLHSFinish_no_unification` calls `checkTypeEqNoUnification` to test the invariants for an inert equality. Before this MR there was a special case for `do_not_prevent_rewriting`, but that has gone; instead it's just a consequence of the flags passed to `checkTyEqRhs`, documented in the `PuOK` case of `canEqCanLHSFinish_no_unification`. * There is only one bit of "swap back" code, in `finish_no_unify` in `canEqCanLHSFinish_try_unification. Previously this code was duplicated. * `kickOutAfterFillingCoercionHole` should account for equalities with a TyFamLHS. See (KOC5) in Note [Kick out after filling a coercion hole] * No need to gather coercion holes in the `PuOK` case of `canEqCanLHSFinish_no_unification`. See documentation with that code. - - - - - 13 changed files: - + changelog.d/T27844 - compiler/GHC/Runtime/Heap/Inspect.hs - compiler/GHC/Tc/Errors.hs - compiler/GHC/Tc/Solver/Equality.hs - compiler/GHC/Tc/Solver/InertSet.hs - compiler/GHC/Tc/Solver/Monad.hs - compiler/GHC/Tc/Types/Constraint.hs - compiler/GHC/Tc/Utils/Unify.hs - testsuite/tests/indexed-types/should_fail/T9662.stderr - testsuite/tests/typecheck/should_fail/T12785b.stderr - + testsuite/tests/typecheck/should_fail/T27844.hs - + testsuite/tests/typecheck/should_fail/T27844.stderr - testsuite/tests/typecheck/should_fail/all.T Changes: ===================================== changelog.d/T27844 ===================================== @@ -0,0 +1,9 @@ +section: compiler +issues: #27844 +mrs: !16723 +synopsis: + Reinstate a missing occurs check in the constraint solver +description: + Simplifies code in GHC's type-constraint solver, thereby fixing an outright + compiler loop (via a missing occurs check). + ===================================== compiler/GHC/Runtime/Heap/Inspect.hs ===================================== @@ -630,7 +630,7 @@ be sigmas and not taus. ~~~~~~~~~~~~~~~~~~~~~~ In the GHCi debugger we use unification variables whose MetaInfo is RuntimeUnkTv. The special property of a RuntimeUnkTv is that it can -unify with a polytype (see GHC.Tc.Utils.Unify.checkTypeEq). +unify with a polytype (see GHC.Tc.Solver.Equality.checkTypeEqNoUnification). If we don't do this `:print <term>` will fail if the type of <term> has nested `forall`s or `=>`s. ===================================== compiler/GHC/Tc/Errors.hs ===================================== @@ -581,7 +581,6 @@ mkErrorItem ct CtGiven {} -> Nothing CtWanted (WantedCt { ctev_dest = dest }) -> Just dest - m_reason = case ct of CIrredCan (IrredCt { ir_reason = reason }) -> Just reason _ -> Nothing ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -21,6 +21,7 @@ import GHC.Tc.Types.Evidence import GHC.Tc.Types.Constraint import GHC.Tc.Types.CtLoc import GHC.Tc.Types.Origin +import GHC.Tc.Types( TcM ) import GHC.Tc.Utils.Unify import GHC.Tc.Utils.TcType import GHC.Tc.Instance.Family ( tcUnwrapNewtype_maybe ) @@ -36,8 +37,8 @@ import GHC.Core.Coercion import GHC.Core.Reduction import GHC.Core.FamInstEnv ( FamInstEnvs ) import GHC.Core -import GHC.Types.Var +import GHC.Types.Var import GHC.Types.Basic import GHC.Types.Name.Reader import GHC.Types.Var.Env @@ -49,6 +50,8 @@ import GHC.Utils.Misc import GHC.Utils.Monad import GHC.Data.Pair +import GHC.Data.Bag + import Control.Monad import Data.Maybe ( isJust, isNothing ) import Data.List ( zip4 ) @@ -406,11 +409,13 @@ canonicaliseEquality -- hold. canonicaliseEquality ev eq_rel ty1 ty2 - = Stage $ do { traceTcS "canonicaliseEquality" $ + = Stage $ do { traceTcS "canonicaliseEquality {" $ vcat [ ppr ev, ppr eq_rel, ppr ty1, ppr ty2 ] ; rdr_env <- getGlobalRdrEnvTcS ; fam_insts <- getFamInstEnvs - ; can_eq_nc initCanEqState rdr_env fam_insts ev eq_rel ty1 ty1 ty2 ty2 } + ; res <- can_eq_nc initCanEqState rdr_env fam_insts ev eq_rel ty1 ty1 ty2 ty2 + ; traceTcS "canonicaliseEquality }" (ppr res) + ; return res } -- | Main worker function for 'canonicaliseEquality'. -- @@ -1822,7 +1827,7 @@ Ticket #10009, a very nasty example: g :: forall a. (UnF (F a) ~ a) => a -> () g _ = f (undefined :: F a) -For g we get [G] g1 : UnF (F a) ~ a +For g we get [G] g1 : UnF (F a) ~ a [W] w1 : UnF (F beta) ~ beta [W] w2 : F a ~ F beta @@ -1982,7 +1987,7 @@ canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2 finish rewriters kind_co = do { traceTcS "Hetero equality gives rise to kind equality" (ppr swapped $$ - ppr kind_co <+> dcolon <+> sep [ ppr ki1, text "~#", ppr ki2 ]) + ppr kind_co <+> dcolon <+> sep [ ppr ki2, text "~#", ppr ki1 ]) ; new_ev <- rewriteEqEvidence ev swapped lhs_redn rhs_redn rewriters -- rewriteEqEvidence adds any as-yet-unsolved equalities -- from the kind equality (namely `rewriters`) to the @@ -2040,15 +2045,15 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco then finish_with_swapping else finish_without_swapping } - | TyVarLHS {} <- lhs1 + | TyVarLHS tv <- lhs1 , TyFamLHS {} <- lhs2 - = if put_tyvar_on_lhs + = if mightPossiblyUnify ev eq_rel tv then finish_without_swapping else finish_with_swapping | TyFamLHS {} <- lhs1 - , TyVarLHS {} <- lhs2 - = if put_tyvar_on_lhs + , TyVarLHS tv <- lhs2 + = if mightPossiblyUnify ev eq_rel tv then finish_with_swapping else finish_without_swapping @@ -2096,10 +2101,6 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco ; new_ev <-rewriteEqEvidence ev swapped lhs1_redn lhs2_redn emptyCoHoleSet ; canEqCanLHSFinish new_ev eq_rel IsSwapped lhs2 (ps_xi1 `mkCastTyMCo` sym_mco) } - put_tyvar_on_lhs = isWanted ev && eq_rel == NomEq - -- See Note [Orienting TyVarLHS/TyFamLHS] - -- Same conditions as for canEqCanLHSFinish_try_unification - -- which we are setting ourselves up for here {- Note [Orienting TyVarLHS/TyFamLHS] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2108,16 +2109,16 @@ Which to put on the left? Answer: * If there is no chance of unifying, put the type family on the left, (F tys ~ a), because it's generally better to rewrite away function - calls. See `put_tyvar_on_lhs` in canEqCanLHS2; and - Note [Orienting TyVarLHS/TyFamLHS] + calls. For the "no chance of unifying" test, see calls to + `mightPossiblyUnify` in `canEqCanLHS2; and Note [Orienting TyVarLHS/TyFamLHS] * But if there /is/ a chance of unifying, put the tyvar on the left, (a ~ F tys), as this may be our only shot to unify. Again see - `put_tyvar_on_lhs`. + `mightPossiblyUnify`. * But if we /fail/ to unify then flip back to (F tys ~ a) because it's - generally better to rewrite away function calls. See the call to - `swapAndFinish` in `canEqCanLHSFinish_try_unification` + generally better to rewrite away function calls. See the swapping-back + code in `finish_on_unify` in `canEqCanLHSFinish_try_unification` It's important to flip back. Consider [W] F alpha ~ alpha @@ -2197,71 +2198,64 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs = return True ----------------------- -canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs - -- Try unification; for Wanted, Nominal equalities with a meta-tyvar on the LHS - | CtWanted wev <- ev -- See Note [Do not unify Givens] +mightPossiblyUnify :: CtEvidence -> EqRel -> TcTyVar -> Bool +-- Is this equality (tv ~ ty) one we could perhaps solve by unification? +-- True <=> perhaps yes +-- False <=> definitely not +mightPossiblyUnify ev eq_rel tv + | isMetaTyVar tv + , CtWanted wev <- ev -- See Note [Do not unify Givens] , NomEq <- eq_rel -- See Note [Do not unify representational equalities] , wantedCtHasNoRewriters wev -- See Note [Unify only if the rewriter set is empty] - , TyVarLHS lhs_tv <- lhs + = True + | otherwise + = False + +canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs + -- Try unification; for Wanted, Nominal equalities with a meta-tyvar on the LHS + | TyVarLHS lhs_tv <- lhs + , mightPossiblyUnify ev eq_rel lhs_tv = do { given_eq_lvl <- getInnermostGivenEqLevel ; case simpleUnifyCheck UC_Solver given_eq_lvl lhs_tv rhs of - SUC_CanUnify -> - unify lhs_tv (mkReflRedn Nominal rhs) - SUC_CannotUnify - | Just can_rhs <- canTyFamEqLHS_maybe rhs - -> swap_and_finish lhs_tv can_rhs -- See Note [Orienting TyVarLHS/TyFamLHS] - | otherwise - -> finish_no_unify - SUC_NotSure -> - -- We have a touchable unification variable on the left, + SUC_CannotUnify -> finish_no_unify + SUC_CanUnify -> do_unification lhs_tv (mkReflRedn Nominal rhs) + SUC_NotSure -> + -- We have a touchable, unfilled unification variable on the left, -- and the top-shape check succeeded. These are both guaranteed -- by the fact that simpleUnifyCheck did not return SUC_CannotUnify. + -- + -- Next, do a full `checkTyEqRhs` check to see if we can unify + -- See Note [checkTyEqRhs] in GHC.Tc.Utils.Unify do { let flags = unifyingLHSMetaTyVar_TEFTask ev lhs_tv ; check_result <- wrapTcS (checkTyEqRhs flags rhs) + ; traceTcS "canEqCanLHSFinish_try_unification" $ + vcat [ text "lhs" <+> ppr lhs + , text "rhs" <+> ppr rhs + , text "check_result" <+> ppr check_result ] ; case check_result of - PuOK cts rhs_redn -> - do { emitWork cts - ; unify lhs_tv rhs_redn } - PuFail reason - | Just can_rhs <- canTyFamEqLHS_maybe rhs - -> swap_and_finish lhs_tv can_rhs -- See Note [Orienting TyVarLHS/TyFamLHS] - | reason `cterHasOnlyProblems` do_not_prevent_rewriting - -> - -- ContinueWith, to allow using this constraint for - -- rewriting (e.g. alpha[2] ~ beta[3]). - do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped lhs rhs - ; continueWith $ Right $ - EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel - , eq_lhs = lhs , eq_rhs = rhs } - } - | otherwise - -> try_irred reason - } + PuFail {} -> finish_no_unify + PuOK cts rhs_redn -> do { emitWork cts + ; do_unification lhs_tv rhs_redn } } } -- Otherwise unification is off the table | otherwise = finish_no_unify where - -- We can't unify, but this equality can go in the inert set - -- and be used to rewrite other constraints. - finish_no_unify = - canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs - - -- We can't unify, and this equality should not be used to rewrite - -- other constraints (e.g. because it has an occurs check). - -- So add it to the inert Irreds. - try_irred reason = - tryIrredInstead reason ev eq_rel swapped lhs rhs - - -- We can't unify as-is, and want to flip the equality around. - -- Example: alpha ~ F tys, flip it around to become the canonical - -- equality f tys ~ alpha. - swap_and_finish tv can_rhs = - swapAndFinish ev eq_rel swapped (mkTyVarTy tv) can_rhs - - -- Phew! Finally! We can unify; go ahead and do so. - unify tv rhs_redn = + -- finish_no_unify: abandon the attempt to unify, and instead hand off to + -- canEqCanLHSFinish_no_unification + -- First, though, if we have (tv ~ F tys) + -- swap it over so we get (F tys ~ tv), with `F tys` on the LHS + -- See Note [Orienting TyVarLHS/TyFamLHS] + finish_no_unify + | TyVarLHS lhs_tv <- lhs + , Just can_rhs <- canTyFamEqLHS_maybe rhs + = canEqCanLHSFinish_no_unification ev eq_rel (flipSwap swapped) can_rhs (mkTyVarTy lhs_tv) + | otherwise + = canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs + + -- do_unification: Phew! Finally! We can unify; go ahead and do so. + do_unification tv rhs_redn = do { -- In the common case where rhs_redn is Refl, we don't need to rewrite -- the evidence, even if swapped=IsSwapped. Suppose the original was -- [W] co : Int ~ alpha @@ -2273,7 +2267,8 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs else rewriteEqEvidence ev swapped (mkReflRedn Nominal (mkTyVarTy tv)) rhs_redn emptyCoHoleSet - -- emptyCoHoleSet: rhs_redn has no CoercionHoles + -- emptyCoHoleSet: we are about to /solve/ this + -- constraint, so its CoHoleSet doesn't matter ; let tv_ty = mkTyVarTy tv final_rhs = reductionReducedType rhs_redn @@ -2297,45 +2292,48 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs ; return (Stop new_ev (text "Solved by unification")) } --------------------------- --- Unification is off the table canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs - = do { -- Do checkTypeEq to guarantee (TyEq:OC), (TyEq:F) + -- We can't unify, but we can see if this equality can go in the inert set + -- and be used to rewrite other constraints. + -- See Note [Equalities where unification fails] + = do { -- Do checkTypeEqNoUnification to guarantee (TyEq:OC), (TyEq:F) -- Must do the occurs check even on tyvar/tyvar equalities, -- in case have x ~ (y :: ..x...); this is #12593. - ; check_result <- checkTypeEq ev eq_rel lhs rhs - - ; let lhs_ty = canEqLHSType lhs + ; check_result <- checkTypeEqNoUnification ev eq_rel lhs rhs ; case check_result of PuFail reason - - -- If we had F a ~ G (F a), which gives an occurs check, - -- then swap it to G (F a) ~ F a, which does not - -- However `swap_for_size` above will orient it with (G (F a)) on - -- the left anwyway. `swap_for_rewriting` "wins", but that doesn't - -- matter: in the occurs check case swap_for_rewriting will be moot. - -- TL;DR: the next four lines of code are redundant - -- I'm leaving them here in case they become relevant again --- | TyFamLHS {} <- lhs --- , Just can_rhs <- canTyFamEqLHS_maybe rhs --- , reason `cterHasOnlyProblem` cteSolubleOccurs --- -> swapAndFinish ev eq_rel swapped lhs_ty can_rhs --- | otherwise - - | reason `cterHasOnlyProblems` do_not_prevent_rewriting - -> do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped lhs rhs - ; continueWith $ Right $ - EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel - , eq_lhs = lhs , eq_rhs = rhs } - } - - | otherwise - -> tryIrredInstead reason ev eq_rel swapped lhs rhs + -> -- We can't unify, and this equality should not be used to rewrite + -- other constraints (e.g. because it has an occurs check). + -- So add it to the inert Irreds. + -- NB: The `reason` will never include `cteConcrete` or `cteSkolemEscape` + -- because checkTypeEqNoUnification doesn't check for those things; + -- they do not prevent the equality being canonical. So you can't + -- rely on `reason` reporting those points, nor do we need to. + do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped lhs rhs + ; finishCanWithIrred (NonCanonicalReason reason) new_ev } PuOK new_eqs rhs_redn - -> do { emitWork new_eqs - ; let new_holes = rewriterSetFromCts new_eqs + -> -- Put this constraint into the inert set, so that it will be used + -- to solve or rewrite other constraints. + -- + -- NB: checkTypeEqNoUnification does not check for + -- (a) skolem-escape (tefTyVar_levelCheck = LC_None) + -- (b) concreteness (tefTyVar_concreteCheck = CC_None) + -- So an equality whose only problem is e.g. skolem-escape will + -- return PuOK, will be put in the inert set, will be used for + -- rewriting. That is fine. + -- + -- assertPpr (isEmptyCts new_eqs): + -- checkTypeEqNoUnification does neither promotion nor type-family + -- flattening for Wanteds, and hence creates no equalities to solve + assertPpr (isEmptyCts new_eqs) + (vcat [ text "new_eqs" <+> ppr new_eqs + , text "rhs_redn" <+> ppr rhs_redn + , text "lhs" <+> ppr lhs + , text "rhs" <+> ppr rhs ]) $ + do { let lhs_ty = canEqLHSType lhs lhs_redn = mkReflRedn (eqRelRole eq_rel) lhs_ty - ; new_ev <- rewriteEqEvidence ev swapped lhs_redn rhs_redn new_holes + ; new_ev <- rewriteEqEvidence ev swapped lhs_redn rhs_redn emptyCoHoleSet -- Important: even if the coercion is Refl, -- * new_ev has reductionReducedType on the RHS @@ -2346,45 +2344,56 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs , eq_lhs = lhs , eq_rhs = reductionReducedType rhs_redn } } } --- | Some problems prevent /unification/ but not /rewriting/: --- --- Skolem-escape: if we have [W] alpha[2] ~ Maybe b[3] --- we can't unify (skolem-escape); but it /is/ canonical, --- and hence we /can/ use it for rewriting --- --- Concrete-ness: alpha[conc] ~ b[sk] --- We can use it to rewrite; we still have to solve the original -do_not_prevent_rewriting :: CheckTyEqResult -do_not_prevent_rewriting = cteProblem cteSkolemEscape S.<> - cteProblem cteConcrete +checkTypeEqNoUnification :: CtEvidence -> EqRel -> CanEqLHS -> TcType + -> TcS (PuResult Ct Reduction) +-- Used for general CanEqLHSs, when we have decided that we cannot unify +checkTypeEqNoUnification ev eq_rel lhs rhs = + case ev of + CtGiven {} -> + do { traceTcS "checkTypeEqNoUnification (given) {" (vcat [ text "lhs:" <+> ppr lhs + , text "rhs:" <+> ppr rhs ]) + ; check_result <- wrapTcS (checkTyEqRhs given_flags rhs) + ; traceTcS "checkTypeEqNoUnification }" (ppr check_result) + ; case check_result of + PuFail reason -> return (PuFail reason) + PuOK prs redn -> do { new_givens <- mapBagM mk_new_given prs + ; emitWork new_givens + ; updInertSet (addCycleBreakerBindings prs) + ; return (pure redn) } } + CtWanted {} -> do { traceTcS "checkTypeEqNoUnification (wanted) {" $ + vcat [ text "lhs:" <+> ppr lhs + , text "rhs:" <+> ppr rhs ] + ; check_result <- wrapTcS (checkTyEqRhs wanted_flags rhs) + ; traceTcS "checkTypeEqNoUnification }" (ppr check_result) + ; return check_result } + where + wanted_flags :: TyEqFlags TcM Ct + wanted_flags = notUnifying_TEFTask occ_prob lhs + -- See Note [Don't cycle-break Wanteds when not unifying] + + given_flags :: TyEqFlags TcM (TcTyVar, TcType) + given_flags = wanted_flags { tef_fam_app = mkTEFA_Break ev eq_rel BreakGiven } + -- TEFA_Break used for: [G] a ~ Maybe (F a) + -- or [G] F a ~ Maybe (F a) + + -- occ_prob: see Note [Occurs check and representational equality] + occ_prob = case eq_rel of + NomEq -> cteInsolubleOccurs + ReprEq -> cteSolubleOccurs + + --------------------------- + mk_new_given :: (TcTyVar, TcType) -> TcS Ct + mk_new_given (new_tv, fam_app) + = mkNonCanonical . CtGiven <$> newGivenEv cb_loc (given_pred, given_term) + where + new_ty = mkTyVarTy new_tv + given_pred = mkNomEqPred fam_app new_ty + given_term = evCoercion $ mkNomReflCo new_ty -- See Detail (4) of Note ----------------------- -swapAndFinish :: CtEvidence -> EqRel -> SwapFlag - -> TcType -> CanEqLHS -- ty ~ F tys - -> TcS (StopOrContinue (Either unused EqCt)) --- We have an equality alpha ~ F tys, that we can't unify e.g because 'tys' --- mentions alpha, it would not be a canonical constraint as-is. --- We want to flip it to (F tys ~ a), whereupon it is canonical -swapAndFinish ev eq_rel swapped lhs_ty can_rhs - = do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel (flipSwap swapped) can_rhs lhs_ty - ; continueWith $ Right $ - EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel - , eq_lhs = can_rhs, eq_rhs = lhs_ty } } + -- See Detail (7) of the Note + cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin ---------------------- -tryIrredInstead :: CheckTyEqResult -> CtEvidence - -> EqRel -> SwapFlag -> CanEqLHS -> TcType - -> TcS (StopOrContinue (Either IrredCt unused)) --- We have a non-canonical equality --- We still swap it if 'swapped' says so, so that it is oriented --- in the direction that the error-reporting machinery --- expects it; e.g. (m ~ t m) rather than (t m ~ m) --- This is not very important, and only affects error reporting. -tryIrredInstead reason ev eq_rel swapped lhs rhs - = do { traceTcS "cantMakeCanonical" (ppr reason $$ ppr lhs $$ ppr rhs) - ; new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped lhs rhs - ; finishCanWithIrred (NonCanonicalReason reason) new_ev } - finishCanWithIrred :: CtIrredReason -> CtEvidence -> TcS (StopOrContinue (Either IrredCt a)) finishCanWithIrred reason ev @@ -2404,8 +2413,63 @@ canEqReflexive ev eq_rel ty = do { setEqIfWanted ev (mkReflCPH eq_rel ty) ; stopWith ev "Solved by reflexivity" } -{- Note [Equalities with heterogeneous kinds] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +{- Note [Equalities where unification fails] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +If we can't unify, but the equality is canonical, we still want to add it to the +inert set so that it can be used to rewrite other Wanteds. (There are many +reasons that unification might not happen: the LHS is not a touchable unification +variable, it has rewriters, it's a Given etc.) + +* In this case we call `checkTypeEqNoUnification` to see whether it is canonical + (which in turn calls `checkTypeEqRhs` with suitable flags). + +* NB: we do /not/ try to take advantage of the case where + `canEqCanLHSFinish_try_unification` has already called `checkTyEqRhs`; doing so + caused #27844. (The first call did fam-app breaking, which concealed a genuine + occurs check.) It's just too clever; better to do the simple thing. + +Note [Don't cycle-break Wanteds when not unifying] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider + [W] a[2] ~ Maybe (F a[2]) + +Should we cycle-break this Wanted, thus? + + [W] a[2] ~ Maybe delta[2] + [W] delta[2] ~ F a[2] + +For a start, this is dodgy because we might just unify delta, thus undoing +what we have done, and getting an infinite loop in the solver. Even if we +somehow prevented ourselves from doing so, is there any merit in the split? +Maybe: perhaps we can use that equality on `a` to unlock other constraints? +Consider + type instance F (Maybe _) = Bool + + [G] g1: a ~ Maybe Bool + [W] w1: a ~ Maybe (F a) + +If we loop-break w1 to get + [W] w1': a ~ Maybe gamma + [W] w3: gamma ~ F a +Now rewrite w3 with w1' + [W] w3': gamma ~ F (Maybe gamma) +Now use the type instance to get + gamma := Bool +Now we are left with + [W] w1': a ~ Maybe Bool +which we can solve from the Given. + +BUT in this situation we could have rewritten the +/original/ Wanted from the Given, like this: + [W] w1': Maybe Bool ~ Maybe (F (Maybe Bool)) +and that is readily soluble. + +In short: loop-breaking Wanteds, when we aren't unifying, +seems of no merit. Hence TEFA_Recurse, rather than TEFA_Break, +in `wanted_flags` in `checkTypeEqNoUnification`. + +Note [Equalities with heterogeneous kinds] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ What do we do when we have an equality (tv :: k1) ~ (rhs :: k2) @@ -2587,8 +2651,8 @@ The details depend on whether we're working with a Given or a Wanted. Given ----- We emit a new Given, [G] F a ~ cbv, equating the type family application -to our new cbv. This is actually done by `break_given` in -`GHC.Tc.Solver.Monad.checkTypeEq`. +to our new cbv. This is actually done by `BreakGiven` in the `given_flags` +in `checkTypeEqNoUnification`. Note its orientation: The type family ends up on the left; see Note [Orienting TyFamLHS/TyFamLHS]. No special treatment for @@ -2629,7 +2693,7 @@ Note that Wanted ------ First, we do not cycle-break unless the LHS is a unifiable type variable -See Note [Don't cycle-break Wanteds when not unifying] in GHC.Tc.Solver.Monad. +See Note [Don't cycle-break Wanteds when not unifying]. OK, so suppose the LHS is a unifiable type variable. The fresh cycle-breaker variables here must actually be normal, touchable metavariables. That is, they @@ -3073,11 +3137,10 @@ inertsEqsCanDischarge inerts (EqCt { eq_lhs = lhs_w, eq_rhs = rhs_w || (empty_rw_w && not (isEmptyCoHoleSet (ctEvRewriters ev_i))) -- Prefer the one that has no rewriters -- See (CE4) in Note [Combining equalities] + -- and (WRW10) in Note [Wanteds rewrite Wanteds: rewriter-sets] inertsEqsCanDischarge _ _ = Nothing - - {- Note [Do not unify Givens] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider this GADT match @@ -3143,34 +3206,6 @@ Wrinkles: we should kick out `co` so that we can now unify it, which might unlock other stuff. See `kickOutAfterFillingCoercionHole` in GHC.Tc.Solver.Monad. - -Note [Solve by unification] -~~~~~~~~~~~~~~~~~~~~~~~~~~~ -If we solve - alpha[n] ~ ty -by unification, there are two cases to consider - -* TouchableSameLevel: if the ambient level is 'n', then - we can simply update alpha := ty, and do nothing else - -* TouchableOuterLevel free_metas n: if the ambient level is greater than - 'n' (the level of alpha), in addition to setting alpha := ty we must - do two other things: - - 1. Promote all the free meta-vars of 'ty' to level n. After all, - alpha[n] is at level n, and so if we set, say, - alpha[n] := Maybe beta[m], - we must ensure that when unifying beta we do skolem-escape checks - etc relevant to level n. Simple way to do that: promote beta to - level n. - - 2. Set the Unification Level Flag to record that a level-n unification has - taken place. See Note [WhatUnifications] in GHC.Tc.Utils.Unify - -NB: TouchableSameLevel is just an optimisation for TouchableOuterLevel. Promotion -would be a no-op, and setting the unification flag unnecessarily would just -make the solver iterate more often. (We don't need to iterate when unifying -at the ambient level because of the kick-out mechanism.) -} ===================================== compiler/GHC/Tc/Solver/InertSet.hs ===================================== @@ -22,7 +22,7 @@ module GHC.Tc.Solver.InertSet ( InertEqs, foldTyEqs, delEq, findEq, partitionInertEqs, partitionFunEqs, transformAndPartitionTyVarEqs, - filterInertEqs, filterFunEqs, + filterInertEqs, filterFunEqs, transformAndPartitionFunEqs, foldFunEqs, addEqToCans, -- * Inert Dicts @@ -128,7 +128,7 @@ Further refinements: * Among the equalities we prioritise ones with an empty rewriter set; see Note [Wanteds rewrite Wanteds: rewriter-sets] in GHC.Tc.Types.Constraint, - wrinkle (WRW8). + wrinkle (WRW7). * Among equalities with an empty rewriter set, we prioritise nominal equalities. * They have more rewriting power, so doing them first is better. @@ -983,7 +983,7 @@ How do we establish these conditions? with S(fw,_). * (T3) is guaranteed by an occurs-check on the work item. - This is done during canonicalisation, in checkTypeEq; invariant + This is done during canonicalisation, in checkTyEqRhs; invariant (TyEq:OC) of CEqCan. See also Note [EqCt occurs check] in GHC.Tc.Types.Constraint. * (T4) is established by GHC.Tc.Solver.Monad.kickOutRewritable. If the inert @@ -1422,6 +1422,19 @@ addCanFunEq old_eqs fun_tc fun_args ct foldFunEqs :: (EqCt -> b -> b) -> FunEqMap EqualCtList -> b -> b foldFunEqs k fun_eqs z = foldTcAppMap (\eqs z -> foldr k z eqs) fun_eqs z +transformAndPartitionFunEqs + :: (EqCt -> Either EqCt EqCt) -- Left => chuck out, Right => keep + -> InertFunEqs + -> ([EqCt], InertFunEqs) -- (chuck-out, keep) +transformAndPartitionFunEqs pred orig_inerts + = foldFunEqs folder orig_inerts ([], emptyFunEqs) + where + folder :: EqCt -> ([EqCt], InertFunEqs) -> ([EqCt], InertFunEqs) + folder eq_ct (acc_true, acc_false) + = case pred eq_ct of + Left eq_ct' -> (eq_ct' : acc_true, acc_false) + Right eq_ct' -> (acc_true, addFunEqs eq_ct' acc_false) + partitionFunEqs :: (EqCt -> Bool) -- EqCt will have a TyFamLHS -> InertFunEqs -> ([EqCt], InertFunEqs) ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -117,10 +117,7 @@ module GHC.Tc.Solver.Monad ( getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS, matchFam, matchFamTcM, checkWellLevelledDFun, - pprEq, - - -- Enforcing invariants for type equalities - checkTypeEq + pprEq ) where import GHC.Prelude @@ -436,32 +433,48 @@ we should kick out `co` so that we can now unify it, which might unlock other st See Note [Unify only if the rewriter set is empty] in GHC.Tc.Solver.Equality for why solving `kco` might unlock `co`, especially (URW2). -Hence `kickOutAfterFillingCoercionHole`. It looks at inert constraints that are +Hence `kickOutAfterFillingCoercionHole`. It looks at inert constraints + [W] co :: ty1 ~ tys +that are * Wanted - * Of the form alpha ~ rhs, where alpha is a unification variable -and kicks out any that will have an empty rewriter set after filling the hole. + * Of the form (alpha ~ rhs) + or (F tys ~ alpha) + or (F tys ~ alpha |> co) + where alpha is a unification variable + and kicks out any that have an empty rewriter set after filling the hole. Wrinkles: + (KOC1) If co's rewriter-set is {kco, xco}, there is no point in kicking it out, because it still can't be unified. So we only kick out if the co's rewriter-set becomes empty. -(KOC2) `kco` might itself have a rewriter set. This is fairly common. E.g. +(KOC2) `kco` might itself have been rewritten by other as-yet-unsolved new_holes. + This is fairly common. E.g. kco : a[sk] ~ beta[tau] Assuming we can't unify it for some reason, we may swap that over to give kco2 : beta[tau] ~ a[sk] kco := sym kco2 So `kco` is "solved" but the coercion that solves it has free coercion holes! So rather than kick out `co`, we should just change its rewriter-set to depend - on `kco2` instead of `kco`. Hence the `new_holes` passed to - `kickOutAfterFillingCoercionHole` + on `kco2` instead of `kco`. -(KOC3) It's possible that this could just go ahead and unify, but could there - be occurs-check problems? Seems simpler just to kick out. + Hence the `new_holes` passed to `kickOutAfterFillingCoercionHole` + +(KOC3) It's possible that this could just go ahead and unify on the spot, but could + there be occurs-check problems? Seems simpler just to kick out. (KOC4) Kick-out is undesirable, so it'd be better to solve `kco` before `co`. So the solver prioritises equalities with an empty rewriter set, to try to avoid unnecessary kick-out. See GHC.Tc.Types.Constraint Note [Prioritise Wanteds with empty CoHoleSet] esp (PER1) + +(KOC5) We kick out from both `inert_eqs` and `inert_funeqs`. The latter is needed + in case we have (F tys ~ alpha), which might (if it now has an empty rewriter + set) allow unifying alpha. + +(KOC6) Annoyingly, we /also/ need to look for (F tys ~ (alpha |> co)), with a cast, + because that may be unifiable by moving the cast to the other side. Hence + `getCastedTyVar_maybe`. -} kickOutRewritable :: KickOutSpec -> CtFlavourRole -> TcS () @@ -526,27 +539,36 @@ kickOutAfterFillingCoercionHole hole (CPH { cph_holes = new_holes }) ; setInertCans ics' } where kick_out :: InertCans -> ([EqCt], InertCans) - kick_out ics@(IC { inert_eqs = eqs }) - = (eqs_to_kick, ics { inert_eqs = eqs_to_keep }) + kick_out ics@(IC { inert_eqs = eqs, inert_funeqs = funeqs }) + = ( kick_funeqs ++ kick_eqs + , ics { inert_eqs = keep_eqs, inert_funeqs = keep_funeqs }) where - (eqs_to_kick, eqs_to_keep) = transformAndPartitionTyVarEqs kick_out_eq eqs + (kick_eqs, keep_eqs) = transformAndPartitionTyVarEqs kick_out_eq eqs + (kick_funeqs, keep_funeqs) = transformAndPartitionFunEqs kick_out_eq funeqs + -- Kick out from funeqs as well as eqs. + -- See (KOC5) in Note [Kick out after filling a coercion hole] kick_out_eq :: EqCt -> Either EqCt EqCt - kick_out_eq eq_ct@(EqCt { eq_ev = ev, eq_lhs = lhs }) + kick_out_eq eq_ct@(EqCt { eq_ev = ev }) | CtWanted (wev@(WantedCt { ctev_rewriters = rewriters })) <- ev - , TyVarLHS tv <- lhs - , isMetaTyVar tv , hole `elemCoHoleSet` rewriters - , let holes' = (rewriters `delCoHoleSet` hole) `mappend` new_holes - -- Adding new_holes and deleting hole: see (KOC2) - eq_ct' = eq_ct { eq_ev = CtWanted (wev { ctev_rewriters = holes' }) } - = if isEmptyCoHoleSet holes' + , is_meta_tv_equality eq_ct + , let rewriters' = (rewriters `delCoHoleSet` hole) `mappend` new_holes + -- Adding new_holes and deleting hole: see (KOC2) + eq_ct' = eq_ct { eq_ev = CtWanted (wev { ctev_rewriters = rewriters' }) } + = if isEmptyCoHoleSet rewriters' then Left eq_ct' -- Kick out, if new rewriter set is empty (KOC1) else Right eq_ct' -- Keep, but with trimmed holes see (KOC2) + | otherwise = Right eq_ct --------------- + is_meta_tv_equality (EqCt { eq_lhs = lhs, eq_rhs = rhs }) + | TyVarLHS tv <- lhs = isMetaTyVar tv + | Just (tv,_) <- getCastedTyVar_maybe rhs = isMetaTyVar tv + | otherwise = False + -- getCastedTyVar: see (KOC5) in Note [Kick out after filling a coercion hole] + insertSafeOverlapFailureTcS :: InstanceWhat -> DictCt -> TcS () -- See Note [Safe Haskell Overlapping Instances Implementation] in GHC.Tc.Solver insertSafeOverlapFailureTcS what item @@ -2302,52 +2324,6 @@ wrapUnifier rws loc role do_unifications ************************************************************************ -} -checkTypeEq :: CtEvidence -> EqRel -> CanEqLHS -> TcType - -> TcS (PuResult Ct Reduction) --- Used for general CanEqLHSs, ones that do --- not have a touchable type variable on the LHS (i.e. not unifying) -checkTypeEq ev eq_rel lhs rhs = - case ev of - CtGiven {} -> - do { traceTcS "checkTypeEq {" (vcat [ text "lhs:" <+> ppr lhs - , text "rhs:" <+> ppr rhs ]) - ; check_result <- wrapTcS (checkTyEqRhs given_flags rhs) - ; traceTcS "checkTypeEq }" (ppr check_result) - ; case check_result of - PuFail reason -> return (PuFail reason) - PuOK prs redn -> do { new_givens <- mapBagM mk_new_given prs - ; emitWork new_givens - ; updInertSet (addCycleBreakerBindings prs) - ; return (pure redn) } } - CtWanted {} -> wrapTcS (checkTyEqRhs wanted_flags rhs) - where - wanted_flags :: TyEqFlags TcM Ct - wanted_flags = notUnifying_TEFTask occ_prob lhs - -- checkTypeEq deals only with the non-unifying case - - given_flags :: TyEqFlags TcM (TcTyVar, TcType) - given_flags = wanted_flags { tef_fam_app = mkTEFA_Break ev eq_rel BreakGiven } - -- TEFA_Break used for: [G] a ~ Maybe (F a) - -- or [W] F a ~ Maybe (F a) - - -- occ_prob: see Note [Occurs check and representational equality] - occ_prob = case eq_rel of - NomEq -> cteInsolubleOccurs - ReprEq -> cteSolubleOccurs - - --------------------------- - mk_new_given :: (TcTyVar, TcType) -> TcS Ct - mk_new_given (new_tv, fam_app) - = mkNonCanonical . CtGiven <$> newGivenEv cb_loc (given_pred, given_term) - where - new_ty = mkTyVarTy new_tv - given_pred = mkNomEqPred fam_app new_ty - given_term = evCoercion $ mkNomReflCo new_ty -- See Detail (4) of Note - - -- See Detail (7) of the Note - cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin - -------------------------- -- | Fill in CycleBreakerTvs with the variables they stand for. -- See Note [Type equality cycles] in GHC.Tc.Solver.Equality restoreTyVarCycles :: InertSet -> TcM () @@ -2363,43 +2339,4 @@ restoreTyVarCycles is (a ~R# b a) is soluble if b later turns out to be Identity So we treat this as a "soluble occurs check". -Note [Don't cycle-break Wanteds when not unifying] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consdier - [W] a[2] ~ Maybe (F a[2]) - -Should we cycle-break this Wanted, thus? - - [W] a[2] ~ Maybe delta[2] - [W] delta[2] ~ F a[2] - -For a start, this is dodgy because we might just unify delta, thus undoing -what we have done, and getting an infinite loop in the solver. Even if we -somehow prevented ourselves from doing so, is there any merit in the split? -Maybe: perhaps we can use that equality on `a` to unlock other constraints? -Consider - type instance F (Maybe _) = Bool - - [G] g1: a ~ Maybe Bool - [W] w1: a ~ Maybe (F a) - -If we loop-break w1 to get - [W] w1': a ~ Maybe gamma - [W] w3: gamma ~ F a -Now rewrite w3 with w1' - [W] w3': gamma ~ F (Maybe gamma) -Now use the type instance to get - gamma := Bool -Now we are left with - [W] w1': a ~ Maybe Bool -which we can solve from the Given. - -BUT in this situation we could have rewritten the -/original/ Wanted from the Given, like this: - [W] w1': Maybe Bool ~ Maybe (F (Maybe Bool)) -and that is readily soluble. - -In short: loop-breaking Wanteds, when we aren't unifying, -seems of no merit. Hence TEFA_Recurse, rather than TEFA_Break, -in `wanted_flags` in `checkTypeEq`. -} ===================================== compiler/GHC/Tc/Types/Constraint.hs ===================================== @@ -524,7 +524,7 @@ isInsolubleReason (InsolubleFunDepReason {}) = True ------------------------------------------------------------------------------ -- | A /set/ of problems in checking the validity of a type equality. --- See 'checkTypeEq'. +-- See 'GHC.Tc.Utils.Unify.checkTyEqRhs'. newtype CheckTyEqResult = CTER Word8 -- | No problems in checking the validity of a type equality. @@ -2603,19 +2603,24 @@ The rewriter-set plan thereby dropping the reference to `co`. I'm not certain whether this actually happens or not. -(WRW7) In error reporting, we simply suppress any errors that have been rewritten - by /unsolved/ wanteds. This suppression happens in GHC.Tc.Errors.mkErrorItem, +(WRW7) When we fill a coercion hole `h` we kick out any inert Wanted that has `h` + in its rewriter set. See `kickOutAfterFilling CoercionHole`. + See Note [Kick out after filling a coercion hole] in GHC.Tc.Solver.Monad. + + Furthermore, when we select a work item, in `selectNextWorkItem` we zonk the + rewriter set so that it accurately reflects the unsolved coercion holes. That + sets it up ready for the no-rewriter check in (WR5), when we process the equality. + + In `selectNextWorkItem`, we also prioritise equalities with no rewiters. + See Note [Prioritise Wanteds with empty CoHoleSet] in GHC.Tc.Types.Constraint + wrinkle (PER1). + +(WRW8) In error reporting, we suppress any errors that have been rewritten + by /unsolved/ wanteds. This suppression happens in `GHC.Tc.Errors.mkErrorItem`, which uses `GHC.Tc.Zonk.Type.zonkCoHoleSet` to look through any filled coercion holes. The idea is that we wish to report the "root cause" -- the error that rewrote all the others. -(WRW8) In `selectNextWorkItem`, priorities equalities with no rewiters. See - Note [Prioritise Wanteds with empty CoHoleSet] in GHC.Tc.Types.Constraint - wrinkle (PER1). - -(WRW9) In error reporting, we prioritise Wanteds that have an empty CoHoleSet: - see Note [Prioritise Wanteds with empty CoHoleSet]. - Let's continue our first example above: inert: [W] w1 :: a ~ Char @@ -2641,8 +2646,10 @@ Wrinkles: (WRW11) When zonking a constraint (with `zonkCt` and `zonkCtEvidence`) we take the opportunity to zonk its `CoHoleSet`, which eliminates solved ones. - This doesn't guarantee that rewriter sets are always up to date -- c.f. - (WRW10) -- but it helps, and it de-clutters debug output. + This doesn't guarantee that rewriter sets are always up to date (c.f. (WRW10)) + but it helps, and it de-clutters debug output. + + See also (WRW7) which does the crucial just-in-time zonking of the rewriters. Note [Prioritise Wanteds with empty CoHoleSet] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2685,9 +2692,8 @@ in our simplify_loop iteration, we happened to start with co_aym. All would have been well if we'd started with the (not-rewritten) co_ayb and gotten it into the inert set. -With that in mind, we /prioritise/ the work-list to put -constraints with no rewriters first. This prioritisation -is done in `GHC.Tc.Solver.Monad.selectNextWorkItem`. +With that in mind, we /prioritise/ the work-list to put constraints with no rewriters +first. This prioritisation is done in `GHC.Tc.Solver.Monad.selectNextWorkItem`. Wrinkles @@ -2700,8 +2706,8 @@ Wrinkles order to report /some/ error in this case, we simply report all the Wanteds. The user will get a perhaps-confusing error message, but they've written a confusing program! (T22707 and T22793 were close, but they do - not exhibit this behaviour.) So belt and braces: see the `suppress` - stuff in GHC.Tc.Errors.mkErrorItem. + not exhibit this behaviour.) So belt and braces: + see `GHC.Tc.Errors.reportWanteds`. Note [Avoiding rewriting cycles] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -3617,15 +3617,20 @@ instance Outputable SimpleUnifyResult where simpleUnifyCheck :: UnifyCheckCaller -> TcLevel -> TcTyVar -> TcType -> SimpleUnifyResult -- ^ A fast check for unification. May return "not sure", in which case -- unification might still be OK, but it'll take more work to do --- (use the full 'checkTypeEq'). +-- (use the full 'checkTyEqRhs'). -- --- * Rejects if lhs_tv occurs in rhs_ty (occurs check) --- * Rejects foralls unless --- lhs_tv is RuntimeUnk (used by GHCi debugger) --- or is a QL instantiation variable --- * Rejects a non-concrete type if lhs_tv is concrete --- * Rejects type families unless fam_ok=True --- * Does a level-check for type variables, to avoid skolem escape +-- It returns SUC_CannotUnify for +-- * Touchability failure +-- * Top level-shape failure +-- +-- It returns SUC_NotSure for +-- * Occurs check: lhs_tv occurs in rhs_ty +-- * Type families unless fam_ok=True +-- * Foralls unless +-- lhs_tv is RuntimeUnk (used by GHCi debugger) +-- or is a QL instantiation variable +-- * Concreteness: lhs_tv is concrete and rhs is a non-concrete type +-- * Skolem-escape: a level-check for type variables, to avoid skolem escape -- -- This function is pretty heavily used, so it's optimised not to allocate simpleUnifyCheck caller given_eq_lvl lhs_tv rhs @@ -3753,8 +3758,8 @@ Consider [W] alpha[2] ~ Maybe (S beta[4] gamma[2]) We don't want to promote beta to level 2; rather, we should -expand the synonym. (Currently, in checkTypeEqRhs promotion -is irrevocable, by side effect.) +expand the synonym. (Currently, in `checkTyEqRhs` promotion +is irrevocable, by side effect in `promote` in `checkTyVar`.) To avoid this risk we eagerly expand forgetful synonyms. This also means we won't get an occurs check in @@ -4198,7 +4203,7 @@ famAppArgFlags flags = case flags of The key function `checkTyEqRhs ty_eq_flags rhs` is called on the RHS of a type equality lhs ~ rhs -and checks to see if `rhs` satisfies, or can be made to satisfy, +and checks to see if `rhs` satisfies, /or can be made to satisfy/, invariants described by `ty_eq_flags`. It can succeded or fail; in the latter case it returns a `CheckTyEqResult` that describes why it failed. @@ -4219,6 +4224,15 @@ Notably, it can check for things like: * Concreteness error e.g. alpha[conc] ~ r[sk] +Note "or can be made to satisfy the preconditions"! `checkTyEqRhs` may transform +the RHS by + + * Turning a type-family application into a type variable, perhaps to avoid + an occurs check. See Note Note [Family applications in canonical constraints] + + * Promoting any nested unification variables, in order to satisfy the + level invariant. See Note [Promotion and level-checking] + Its specific behaviour is governed by the `TyEqFlags` that are passed to it; see Note [TyEqFlags]. @@ -4275,7 +4289,7 @@ NB: We never see a TyVarLHS here, such as [G] a ~ F tys here because we'd have swapped it to [G] F tys ~ a -in canEqCanLHS2, before getting to checkTypeEq. +in canEqCanLHS2, before getting to checkTyEqRhs. -} check_ty_eq_rhs :: forall m a @@ -4799,7 +4813,6 @@ promote_meta_tyvar info dest_lvl occ_tv touchabilityTest :: TcLevel -> TcTyVar -> Bool -- ^ This is the key test for untouchability: -- See Note [Unification preconditions] in GHC.Tc.Utils.Unify --- and Note [Solve by unification] in GHC.Tc.Solver.Equality -- -- @True@ <=> the variable is touchable touchabilityTest given_eq_lvl tv ===================================== testsuite/tests/indexed-types/should_fail/T9662.stderr ===================================== @@ -1,12 +1,12 @@ T9662.hs:49:8: error: [GHC-25897] - • Couldn't match type ‘n’ with ‘Int’ + • Couldn't match type ‘m’ with ‘Int’ Expected: Exp (((sh :. k) :. m) :. n) -> Exp (((sh :. m) :. n) :. k) Actual: Exp (Tuple (((Atom a0 :. Atom Int) :. Atom Int) :. Atom Int)) -> Exp (Plain (((Unlifted (Atom a0) :. Exp Int) :. Exp Int) :. Exp Int)) - ‘n’ is a rigid type variable bound by + ‘m’ is a rigid type variable bound by the type signature for: test :: forall sh k m n. Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k) ===================================== testsuite/tests/typecheck/should_fail/T12785b.stderr ===================================== @@ -1,6 +1,5 @@ - T12785b.hs:30:65: error: [GHC-25897] - • Could not deduce ‘s ~ Payload (S n) (Payload n s1)’ + • Could not deduce ‘Payload (S n) (Payload n s1) ~ s’ arising from a use of ‘SBranchX’ from the context: m ~ S n bound by a pattern with constructor: @@ -25,3 +24,4 @@ T12785b.hs:30:65: error: [GHC-25897] a :: STree (S m) f s (bound at T12785b.hs:30:12) nest :: HTree m (Hidden (S m) f) -> Hidden m (STree (S m) f) (bound at T12785b.hs:28:1) + ===================================== testsuite/tests/typecheck/should_fail/T27844.hs ===================================== @@ -0,0 +1,14 @@ +-- Repro.hs +-- The call to f forces c ~ (b, F c) inside the scope of the skolem b. +-- Correct behaviour: a type error at the first argument of const +-- (as GHC 9.12.4 reports). + +{-# LANGUAGE RankNTypes, TypeFamilies #-} +module T27844 where + +type family F a + +f :: (forall b. b -> (b, F c)) -> c -> () +f _ _ = () + +g x = f (\_ -> const x (show x)) x ===================================== testsuite/tests/typecheck/should_fail/T27844.stderr ===================================== @@ -0,0 +1,12 @@ +T27844.hs:14:22: error: [GHC-25897] + • Couldn't match expected type ‘(b, F c)’ with actual type ‘c’ + ‘c’ is a rigid type variable bound by + the inferred type of g :: Show c => c -> () + at T27844.hs:14:1-34 + • In the first argument of ‘const’, namely ‘x’ + In the expression: const x (show x) + In the first argument of ‘f’, namely ‘(\ _ -> const x (show x))’ + • Relevant bindings include + x :: c (bound at T27844.hs:14:3) + g :: c -> () (bound at T27844.hs:14:1) + ===================================== testsuite/tests/typecheck/should_fail/all.T ===================================== @@ -766,3 +766,5 @@ test('T26862', normal, compile_fail, ['']) test('T27210', normal, compile_fail, ['']) test('T26532', normal, compile_fail, ['']) test('T27731', normal, compile_fail, ['']) +test('T27844', normal, compile_fail, ['']) + View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/7807b4d3ef52aa36b42b39c58d7cafa8... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/7807b4d3ef52aa36b42b39c58d7cafa8... You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help