Simon Peyton Jones pushed to branch wip/T27844 at Glasgow Haskell Compiler / GHC Commits: 0f5ff61c by Simon Peyton Jones at 2026-09-27T17:31:10+01:00 Further wibbles - - - - - 26bd3aa5 by Simon Peyton Jones at 2026-09-27T18:37:50+01:00 More wibbles ...incl a new assert in the _no_unification case - - - - - 4 changed files: - compiler/GHC/Tc/Solver/Equality.hs - compiler/GHC/Tc/Solver/Monad.hs - compiler/GHC/Tc/Utils/Unify.hs - testsuite/tests/indexed-types/should_fail/T9662.stderr Changes: ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -1824,7 +1824,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 @@ -2213,6 +2213,9 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs -- We have a touchable 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 fully `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" $ @@ -2229,21 +2232,19 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs = finish_no_unify where - -- We can't unify, but we can see if 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 + -- 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 - -- Phew! Finally! We can unify; go ahead and do so. + -- 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 @@ -2280,39 +2281,41 @@ 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 + -- 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 checkTypeEq 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 ; 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 - -- See Note [Orienting TyVarLHS/TyFamLHS] - -- ToDo: fix me ... also needed for a ~ G (F a) - -- 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 - | Just can_rhs <- canTyFamEqLHS_maybe rhs - , reason `cterHasOnlyProblem` cteSolubleOccurs - -> finishWith ev eq_rel (flipSwap swapped) can_rhs lhs_ty - | reason `cterHasOnlyProblems` do_not_prevent_rewriting - -> finishWith ev eq_rel swapped lhs rhs + -> 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. + do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped lhs rhs + ; finishCanWithIrred (NonCanonicalReason reason) new_ev } PuOK new_eqs rhs_redn - -> do { emitWork new_eqs + -> -- Claim: there should be no new_eqs + -- The non-unification check does non promotion nor type-family + -- flattening for Wanteds + 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 { emitWork new_eqs ; let new_holes = rewriterSetFromCts new_eqs + lhs_ty = canEqLHSType lhs lhs_redn = mkReflRedn (eqRelRole eq_rel) lhs_ty ; new_ev <- rewriteEqEvidence ev swapped lhs_redn rhs_redn new_holes @@ -2336,45 +2339,7 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs do_not_prevent_rewriting :: CheckTyEqResult do_not_prevent_rewriting = cteProblem cteSkolemEscape S.<> cteProblem cteConcrete - ----------------------- -finishWith :: CtEvidence -> EqRel -> SwapFlag - -> CanEqLHS -> TcType - -> TcS (StopOrContinue (Either unused EqCt)) -finishWith ev eq_rel swapped can_lhs rhs_ty - = do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped can_lhs rhs_ty - ; continueWith $ Right $ - EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel - , eq_lhs = can_lhs , eq_rhs = rhs_ty } } - -{- -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 } } --} - ---------------------- -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 @@ -2394,8 +2359,26 @@ 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 by 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 `checkTypeEq`to see if it is canonical (which in turn + calls `checkTypeEqRhs`). + +* Even if `checkTypeEq` returns `PuFail`, we may /still/ be able to add it to the inert + set, depending on the reason for failure; examples are given in `do_not_prevent_rewriting`. + +* 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 [Equalities with heterogeneous kinds] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ What do we do when we have an equality (tv :: k1) ~ (rhs :: k2) @@ -3066,8 +3049,6 @@ inertsEqsCanDischarge inerts (EqCt { eq_lhs = lhs_w, eq_rhs = rhs_w inertsEqsCanDischarge _ _ = Nothing - - {- Note [Do not unify Givens] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider this GADT match @@ -3133,34 +3114,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/Monad.hs ===================================== @@ -2333,7 +2333,7 @@ checkTypeEq ev eq_rel lhs rhs = 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) + -- or [G] F a ~ Maybe (F a) -- occ_prob: see Note [Occurs check and representational equality] occ_prob = case eq_rel of ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -4203,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. @@ -4224,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]. ===================================== 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) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/f3b36989d97f7839876ec4f47142cf0... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/f3b36989d97f7839876ec4f47142cf0... 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