Magnus pushed to branch ghc-9.12 at Glasgow Haskell Compiler / GHC Commits: 3f46addc by sheaf at 2026-05-11T12:15:06+02:00 QuickLook: do a shape test before unifying This commit ensures we do a shape test before unifying. This ensures we don't try to unify a TyVarTv with a non-tyvar, e.g. alpha[tyv] := Int On the way, we refactor simpleUnifyCheck: 1. Move the checkTopShape check into simpleUnifyCheck 2. Refactors simpleUnifyCheck to return a value of the new type SimpleUnifyResult type. Now, simpleUnifyCheck returns "can unify", "cannot unify" or "dunno" (with "cannot unify" being the new result it can return). Now: - touchabilityTest is included; it it fails we return "cannot unify" - checkTopShape now returns "cannot unify" instead of "dunno" upon failure 3. Move the call to simpleUnifyCheck out of checkTouchableTyVarEq. After that, checkTouchableTyVarEq becames a simple call to checkTyEqRhs, so we inline it. This allows the logic in canEqCanLHSFinish_try_unification to be simplified. In particular, we now avoid calling 'checkTopShape' twice. Two further changes suggested by Simon were also implemented: - In canEqCanLHSFinish, if checkTyEqRhs returns PuFail with 'do_not_prevent_rewriting', we now **continue with this constraint**. This allows us to use the constraint for rewriting. - checkTyEqRhs now has a top-level check to avoid flattening a tyfam app in a top-level equality of the form alpha ~ F tys, as this is going around in circles. This simplifies the implementation without any change in behaviour. Fixes #25950 Fixes #26030 (cherry picked from commit 67a177b412a4d2517e89ba48e3e22e43c84bff07) - - - - - 5846d4f9 by sheaf at 2026-05-11T12:15:06+02:00 Add regression test for #27149 This is the same bug as #26030, but another regression test ensures that this bug is fixed and stays fixed. - - - - - 12 changed files: - compiler/GHC/Tc/Gen/App.hs - compiler/GHC/Tc/Solver/Equality.hs - compiler/GHC/Tc/Solver/Monad.hs - compiler/GHC/Tc/Types/Constraint.hs - compiler/GHC/Tc/Utils/Unify.hs - testsuite/tests/rep-poly/T19709b.stderr - testsuite/tests/rep-poly/T23154.stderr - testsuite/tests/rep-poly/T23903.stderr - testsuite/tests/simplCore/should_compile/simpl017.stderr - + testsuite/tests/typecheck/should_compile/T26030.hs - + testsuite/tests/typecheck/should_compile/T27149.hs - testsuite/tests/typecheck/should_compile/all.T Changes: ===================================== compiler/GHC/Tc/Gen/App.hs ===================================== @@ -2038,22 +2038,22 @@ qlUnify ty1 ty2 = go_flexi1 kappa ty2 go_flexi1 kappa ty2 -- ty2 is zonked - | -- See Note [QuickLook unification] (UQL1) - simpleUnifyCheck UC_QuickLook kappa ty2 - , checkTopShape (metaTyVarInfo kappa) ty2 - -- NB: don't forget to do a shape check, as we might be dealing - -- with an ordinary metavariable (and not a quick-look instantiation variable). - -- (Forgetting this led to #25950.) - = do { co <- unifyKind (Just (TypeThing ty2)) ty2_kind kappa_kind - -- unifyKind: see (UQL2) in Note [QuickLook unification] - -- and (MIV2) in Note [Monomorphise instantiation variables] - ; let ty2' = mkCastTy ty2 co - ; traceTc "qlUnify:update" $ - ppr kappa <+> text ":=" <+> ppr ty2 - ; liftZonkM $ writeMetaTyVar kappa ty2' } - - | otherwise - = return () -- Occurs-check or forall-bound variable + = do { cur_lvl <- getTcLevel + -- See Note [Unification preconditions], (UNTOUCHABLE) wrinkles + -- Here we are in the TcM monad, which does not track enclosing + -- Given equalities; so for quick-look unification we conservatively + -- treat /any/ level outside this one as untouchable. Hence cur_lvl. + ; case simpleUnifyCheck UC_QuickLook cur_lvl kappa ty2 of + SUC_CanUnify -> + do { co <- unifyKind (Just (TypeThing ty2)) ty2_kind kappa_kind + -- unifyKind: see (UQL2) in Note [QuickLook unification] + -- and (MIV2) in Note [Monomorphise instantiation variables] + ; let ty2' = mkCastTy ty2 co + ; traceTc "qlUnify:update" $ + ppr kappa <+> text ":=" <+> ppr ty2 + ; liftZonkM $ writeMetaTyVar kappa ty2' } + _ -> return () -- e.g. occurs-check or forall-bound variable + } where kappa_kind = tyVarKind kappa ty2_kind = typeKind ty2 ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -1,4 +1,6 @@ {-# LANGUAGE CPP #-} +{-# LANGUAGE DuplicateRecordFields #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiWayIf #-} module GHC.Tc.Solver.Equality( @@ -1884,83 +1886,104 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs ----------------------- canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs -- Try unification; for Wanted, Nominal equalities with a meta-tyvar on the LHS - | isWanted ev -- See Note [Do not unify Givens] - , NomEq <- eq_rel -- See Note [Do not unify representational equalities] - , TyVarLHS tv <- lhs - = do { given_eq_lvl <- getInnermostGivenEqLevel - ; if not (touchabilityAndShapeTest given_eq_lvl tv rhs) - then if | Just can_rhs <- canTyFamEqLHS_maybe rhs - -> swapAndFinish ev eq_rel swapped (mkTyVarTy tv) can_rhs - -- See Note [Orienting TyVarLHS/TyFamLHS] - - | otherwise - -> canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs - else - - -- We have a touchable unification variable on the left - do { check_result <- checkTouchableTyVarEq ev tv rhs - ; case check_result of { - PuFail reason + | isWanted ev -- See Note [Do not unify Givens] + , NomEq <- eq_rel -- See Note [Do not unify representational equalities] + , TyVarLHS lhs_tv <- lhs + = 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 - -> swapAndFinish ev eq_rel swapped (mkTyVarTy tv) can_rhs - -- Swap back: see Note [Orienting TyVarLHS/TyFamLHS] - - | reason `cterHasOnlyProblems` do_not_prevent_rewriting - -> canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs - + -> swap_and_finish lhs_tv can_rhs -- See Note [Orienting TyVarLHS/TyFamLHS] | otherwise - -> tryIrredInstead reason ev eq_rel swapped lhs rhs ; - - PuOK _ rhs_redn -> - - -- Success: we can solve by unification - 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 - -- We unify alpha := Int, and set co := <Int>. No need to - -- swap to co = sym co' - -- co' = <Int> - new_ev <- if isReflCo (reductionCoercion rhs_redn) - then return ev - else rewriteEqEvidence emptyRewriterSet ev swapped - (mkReflRedn Nominal (mkTyVarTy tv)) rhs_redn - - ; let tv_ty = mkTyVarTy tv - final_rhs = reductionReducedType rhs_redn - - ; traceTcS "Sneaky unification:" $ - vcat [text "Unifies:" <+> ppr tv <+> text ":=" <+> ppr final_rhs, - text "Coercion:" <+> pprEq tv_ty final_rhs, - text "Left Kind is:" <+> ppr (typeKind tv_ty), - text "Right Kind is:" <+> ppr (typeKind final_rhs) ] - - -- Update the unification variable itself - ; unifyTyVar tv final_rhs - - -- Provide Refl evidence for the constraint - -- Ignore 'swapped' because it's Refl! - ; setEvBindIfWanted new_ev EvCanonical $ - evCoercion (mkNomReflCo final_rhs) - - -- Kick out any constraints that can now be rewritten - ; kickOutAfterUnification [tv] - - ; return (Stop new_ev (text "Solved by unification")) }}}} - + -> finish_no_unify + SUC_NotSure -> + -- 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. + do { let flags = unifyingLHSMetaTyVar_TEFTask ev lhs_tv + ; check_result <- wrapTcS (checkTyEqRhs flags rhs) + ; 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 { let role = eqRelRole eq_rel + ; new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped + (mkReflRedn role (canEqLHSType lhs)) + (mkReflRedn role rhs) + ; continueWith $ Right $ + EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel + , eq_lhs = lhs , eq_rhs = rhs } + } + | otherwise + -> try_irred reason + } + } -- Otherwise unification is off the table | otherwise - = canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs + = finish_no_unify where - -- 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 + -- 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 + + -- We can unify; go ahead and do so. + unify 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 + -- We unify alpha := Int, and set co := <Int>. No need to + -- swap to co = sym co' + -- co' = <Int> + new_ev <- if isReflCo (reductionCoercion rhs_redn) + then return ev + else rewriteEqEvidence emptyRewriterSet ev swapped + (mkReflRedn Nominal (mkTyVarTy tv)) rhs_redn + + ; let tv_ty = mkTyVarTy tv + final_rhs = reductionReducedType rhs_redn + + ; traceTcS "Sneaky unification:" $ + vcat [text "Unifies:" <+> ppr tv <+> text ":=" <+> ppr final_rhs, + text "Coercion:" <+> pprEq tv_ty final_rhs, + text "Left Kind is:" <+> ppr (typeKind tv_ty), + text "Right Kind is:" <+> ppr (typeKind final_rhs) ] + + -- Update the unification variable itself + ; unifyTyVar tv final_rhs + + -- Provide Refl evidence for the constraint + -- Ignore 'swapped' because it's Refl! + ; setEvBindIfWanted new_ev EvCanonical $ + evCoercion (mkNomReflCo final_rhs) + + -- Kick out any constraints that can now be rewritten + ; kickOutAfterUnification [tv] + + ; return (Stop new_ev (text "Solved by unification")) } --------------------------- -- Unification is off the table @@ -1987,6 +2010,17 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs -- -> swapAndFinish ev eq_rel swapped lhs_ty can_rhs -- | otherwise + | reason `cterHasOnlyProblems` do_not_prevent_rewriting + -> do { let role = eqRelRole eq_rel + ; new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped + (mkReflRedn role (canEqLHSType lhs)) + (mkReflRedn role 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 PuOK _ rhs_redn @@ -2003,6 +2037,18 @@ 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 + ---------------------- swapAndFinish :: CtEvidence -> EqRel -> SwapFlag -> TcType -> CanEqLHS -- ty ~ F tys @@ -2308,8 +2354,9 @@ and we turn this into [W] Arg alpha ~ cbv1 [W] Res alpha ~ cbv2 -where cbv1 and cbv2 are fresh TauTvs. This is actually done by `break_wanted` -in `GHC.Tc.Solver.Monad.checkTouchableTyVarEq`. +where cbv1 and cbv2 are fresh TauTvs. This is actually done within checkTyEqRhs, +called within canEqCanLHSFinish_try_unification, which will use the BreakWanted +FamAppBreaker. Why TauTvs? See [Why TauTvs] below. @@ -2318,7 +2365,7 @@ directly instead of calling wrapUnifierTcS. (Otherwise, we'd end up unifying cbv1 and cbv2 immediately, achieving nothing.) Next, we unify alpha := cbv1 -> cbv2, having eliminated the occurs check. This unification happens immediately following a successful call to -checkTouchableTyVarEq, in canEqCanLHSFinish_try_unification. +checkTyEqRhs, in canEqCanLHSFinish_try_unification. Now, we're here (including further context from our original example, from the top of the Note): ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -122,7 +122,7 @@ module GHC.Tc.Solver.Monad ( pprEq, -- Enforcing invariants for type equalities - checkTypeEq, checkTouchableTyVarEq + checkTypeEq ) where import GHC.Prelude @@ -2169,129 +2169,36 @@ wrapUnifierX ev role do_unifications ************************************************************************ -} -checkTouchableTyVarEq - :: CtEvidence - -> TcTyVar -- A touchable meta-tyvar - -> TcType -- The RHS - -> TcS (PuResult () Reduction) --- Used for Nominal, Wanted equalities, with a touchable meta-tyvar on LHS --- If checkTouchableTyVarEq tv ty = PuOK cts redn --- then we can unify --- tv := ty |> redn --- with extra wanteds 'cts' --- If it returns (PuFail reason) we can't unify, and the reason explains why. -checkTouchableTyVarEq ev lhs_tv rhs - | simpleUnifyCheck UC_Solver lhs_tv rhs -- An (optional) short-cut - = do { traceTcS "checkTouchableTyVarEq: simple-check wins" (ppr lhs_tv $$ ppr rhs) - ; return (pure (mkReflRedn Nominal rhs)) } - - | otherwise - = do { traceTcS "checkTouchableTyVarEq {" (ppr lhs_tv $$ ppr rhs) - ; check_result <- wrapTcS (check_rhs rhs) - ; traceTcS "checkTouchableTyVarEq }" (ppr lhs_tv $$ ppr check_result) - ; case check_result of - PuFail reason -> return (PuFail reason) - PuOK cts redn -> do { emitWork cts - ; return (pure redn) } } - - where - (lhs_tv_info, lhs_tv_lvl) = case tcTyVarDetails lhs_tv of - MetaTv { mtv_info = info, mtv_tclvl = lvl } -> (info,lvl) - _ -> pprPanic "checkTouchableTyVarEq" (ppr lhs_tv) - -- lhs_tv should be a meta-tyvar - - is_concrete_lhs_tv = isConcreteInfo lhs_tv_info - - check_rhs rhs - -- Crucial special case for alpha ~ F tys - -- We don't want to flatten that (F tys)! - | Just (TyFamLHS tc tys) <- canTyFamEqLHS_maybe rhs - = if is_concrete_lhs_tv - then failCheckWith (cteProblem cteConcrete) - else recurseIntoTyConApp arg_flags tc tys - | otherwise - = checkTyEqRhs flags rhs - - flags = TEF { tef_foralls = False -- isRuntimeUnkSkol lhs_tv - , tef_fam_app = mkTEFA_Break ev NomEq break_wanted - , tef_unifying = Unifying lhs_tv_info lhs_tv_lvl (LC_Promote False) - , tef_lhs = TyVarLHS lhs_tv - , tef_occurs = cteInsolubleOccurs } - - arg_flags = famAppArgFlags flags - - break_wanted :: FamAppBreaker Ct - break_wanted fam_app - -- Occurs check or skolem escape; so flatten - = do { let fam_app_kind = typeKind fam_app - ; reason <- checkPromoteFreeVars cteInsolubleOccurs - lhs_tv lhs_tv_lvl (tyCoVarsOfType fam_app_kind) - ; if not (cterHasNoProblem reason) -- Failed to promote free vars - then failCheckWith reason - else - do { new_tv_ty <- - case lhs_tv_info of - ConcreteTv conc_info -> - -- Make a concrete tyvar if lhs_tv is concrete - -- e.g. alpha[2,conc] ~ Maybe (F beta[4]) - -- We want to flatten to - -- alpha[2,conc] ~ Maybe gamma[2,conc] - -- gamma[2,conc] ~ F beta[4] - TcM.newConcreteTyVarTyAtLevel conc_info lhs_tv_lvl fam_app_kind - _ -> TcM.newMetaTyVarTyAtLevel lhs_tv_lvl fam_app_kind - - ; let pty = mkPrimEqPredRole Nominal fam_app new_tv_ty - ; hole <- TcM.newVanillaCoercionHole pty - ; let new_ev = CtWanted { ctev_pred = pty - , ctev_dest = HoleDest hole - , ctev_loc = cb_loc - , ctev_rewriters = ctEvRewriters ev } - ; return (PuOK (singleCt (mkNonCanonical new_ev)) - (mkReduction (HoleCo hole) new_tv_ty)) } } - - -- See Detail (7) of the Note - cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin - ------------------------- checkTypeEq :: CtEvidence -> EqRel -> CanEqLHS -> TcType -> TcS (PuResult () 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 - | isGiven ev - = do { traceTcS "checkTypeEq {" (vcat [ text "lhs:" <+> ppr lhs - , text "rhs:" <+> ppr rhs ]) - ; check_result <- wrapTcS (check_given_rhs 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) } } - - | otherwise -- Wanted - = do { check_result <- wrapTcS (checkTyEqRhs wanted_flags rhs) - ; case check_result of - PuFail reason -> return (PuFail reason) - PuOK cts redn -> do { emitWork cts - ; return (pure redn) } } +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 {} -> + do { check_result <- wrapTcS (checkTyEqRhs wanted_flags rhs) + ; case check_result of + PuFail reason -> return (PuFail reason) + PuOK cts redn -> do { emitWork cts + ; return (pure redn) } } where - check_given_rhs :: TcType -> TcM (PuResult (TcTyVar,TcType) Reduction) - check_given_rhs rhs - -- See Note [Special case for top-level of Given equality] - | Just (TyFamLHS tc tys) <- canTyFamEqLHS_maybe rhs - = recurseIntoTyConApp arg_flags tc tys - | otherwise - = checkTyEqRhs given_flags rhs - - arg_flags = famAppArgFlags given_flags given_flags :: TyEqFlags (TcTyVar,TcType) given_flags = TEF { tef_lhs = lhs , tef_foralls = False , tef_unifying = NotUnifying - , tef_fam_app = mkTEFA_Break ev eq_rel break_given + , tef_fam_app = mkTEFA_Break ev eq_rel BreakGiven , tef_occurs = occ_prob } -- TEFA_Break used for: [G] a ~ Maybe (F a) -- or [W] F a ~ Maybe (F a) @@ -2308,13 +2215,6 @@ checkTypeEq ev eq_rel lhs rhs NomEq -> cteInsolubleOccurs ReprEq -> cteSolubleOccurs - break_given :: TcType -> TcM (PuResult (TcTyVar,TcType) Reduction) - break_given fam_app - = do { new_tv <- TcM.newCycleBreakerTyVar (typeKind fam_app) - ; return (PuOK (unitBag (new_tv, fam_app)) - (mkReflRedn Nominal (mkTyVarTy new_tv))) } - -- Why reflexive? See Detail (4) of the Note - --------------------------- mk_new_given :: (TcTyVar, TcType) -> TcS Ct mk_new_given (new_tv, fam_app) @@ -2327,20 +2227,6 @@ checkTypeEq ev eq_rel lhs rhs -- See Detail (7) of the Note cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin -mkTEFA_Break :: CtEvidence -> EqRel -> FamAppBreaker a -> TyEqFamApp a -mkTEFA_Break ev eq_rel breaker - | NomEq <- eq_rel - , not cycle_breaker_origin - = TEFA_Break breaker - | otherwise - = TEFA_Recurse - where - -- cycle_breaker_origin: see Detail (7) of Note [Type equality cycles] - -- in GHC.Tc.Solver.Equality - cycle_breaker_origin = case ctLocOrigin (ctEvLoc ev) of - CycleBreakerOrigin {} -> True - _ -> False - ------------------------- -- | Fill in CycleBreakerTvs with the variables they stand for. -- See Note [Type equality cycles] in GHC.Tc.Solver.Equality @@ -2357,31 +2243,6 @@ 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 [Special case for top-level of Given equality] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We take care when examining - [G] F ty ~ G (...(F ty)...) -where both sides are TyFamLHSs. We don't want to flatten that RHS to - [G] F ty ~ cbv - [G] G (...(F ty)...) ~ cbv -Instead we'd like to say "occurs-check" and swap LHS and RHS, which yields a -canonical constraint - [G] G (...(F ty)...) ~ F ty -That tents to rewrite a big type to smaller one. This happens in T15703, -where we had: - [G] Pure g ~ From1 (To1 (Pure g)) -Making a loop breaker and rewriting left to right just makes much bigger -types than swapping it over. - -(We might hope to have swapped it over before getting to checkTypeEq, -but better safe than sorry.) - -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. - Note [Don't cycle-break Wanteds when not unifying] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consdier ===================================== compiler/GHC/Tc/Types/Constraint.hs ===================================== @@ -257,10 +257,10 @@ We thus perform an occurs-check. There is, of course, some subtlety: * For type variables, the occurs-check looks deeply including kinds of type variables. This is because a CEqCan over a meta-variable is - also used to inform unification, in - GHC.Tc.Solver.Monad.checkTouchableTyVarEq. If the LHS appears - anywhere in the RHS, at all, unification will create an infinite - structure which is bad. + also used to inform unification, via `checkTyEqRhs`, called in + `canEqCanLHSFinish_try_unification`. + If the LHS appears anywhere in the RHS, at all, unification will create + an infinite structure, which is bad. * For type family applications, the occurs-check is shallow; it looks only in places where we might rewrite. (Specifically, it does not ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -1,3 +1,6 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE RecursiveDo #-} @@ -25,7 +28,7 @@ module GHC.Tc.Utils.Unify ( -- Various unifications unifyType, unifyKind, unifyInvisibleType, unifyExpectedType, unifyExprType, unifyTypeAndEmit, promoteTcType, - swapOverTyVars, touchabilityAndShapeTest, checkTopShape, lhsPriority, + swapOverTyVars, touchabilityTest, checkTopShape, lhsPriority, UnifyEnv(..), updUEnvLoc, setUEnvRole, uType, @@ -39,11 +42,12 @@ module GHC.Tc.Utils.Unify ( matchExpectedFunKind, matchActualFunTy, matchActualFunTys, - checkTyEqRhs, recurseIntoTyConApp, + checkTyEqRhs, recurseIntoTyConApp, recurseIntoFamTyConApp, PuResult(..), failCheckWith, okCheckRefl, mapCheck, - TyEqFlags(..), TyEqFamApp(..), AreUnifying(..), LevelCheck(..), FamAppBreaker, - famAppArgFlags, checkPromoteFreeVars, - simpleUnifyCheck, UnifyCheckCaller(..), + TyEqFlags(..), TyEqFamApp(..), AreUnifying(..), LevelCheck(..), FamAppBreaker(..), + famAppArgFlags, checkPromoteFreeVars, + notUnifying_TEFTask, unifyingLHSMetaTyVar_TEFTask, mkTEFA_Break, + simpleUnifyCheck, UnifyCheckCaller(..), SimpleUnifyResult(..), fillInferResult, ) where @@ -60,7 +64,8 @@ import GHC.Tc.Utils.TcMType import GHC.Tc.Utils.TcType import GHC.Tc.Types.Evidence import GHC.Tc.Types.Constraint -import GHC.Tc.Types.CtLoc( CtLoc, mkKindEqLoc, adjustCtLoc ) +import GHC.Tc.Types.CtLoc( CtLoc, mkKindEqLoc, adjustCtLoc + , ctLocOrigin, updateCtLocOrigin ) import GHC.Tc.Types.Origin import GHC.Tc.Zonk.TcType @@ -71,6 +76,7 @@ import GHC.Core.TyCo.Ppr( debugPprType {- pprTyVar -} ) import GHC.Core.TyCon import GHC.Core.Coercion import GHC.Core.Multiplicity +import GHC.Core.Predicate ( EqRel(..) ) import GHC.Core.Reduction import qualified GHC.LanguageExtensions as LangExt @@ -96,6 +102,7 @@ import GHC.Data.FastString( fsLit ) import Control.Monad import Data.Monoid as DM ( Any(..) ) import qualified Data.Semigroup as S ( (<>) ) +import Data.Traversable ( for ) {- ********************************************************************* * * @@ -2477,10 +2484,9 @@ uUnfilledVar2 :: UnifyEnv -- Precondition: u_role==Nominal uUnfilledVar2 env@(UE { u_defer = def_eq_ref }) swapped tv1 ty2 = do { cur_lvl <- getTcLevel -- See Note [Unification preconditions], (UNTOUCHABLE) wrinkles - -- Here we don't know about given equalities here; so we treat + -- Here we don't know about given equalities; so we treat -- /any/ level outside this one as untouchable. Hence cur_lvl. - ; if not (touchabilityAndShapeTest cur_lvl tv1 ty2 - && simpleUnifyCheck UC_OnTheFly tv1 ty2) + ; if simpleUnifyCheck UC_OnTheFly cur_lvl tv1 ty2 /= SUC_CanUnify then not_ok_so_defer cur_lvl else do { def_eqs <- readTcRef def_eq_ref -- Capture current state of def_eqs @@ -2525,8 +2531,8 @@ uUnfilledVar2 env@(UE { u_defer = def_eq_ref }) swapped tv1 ty2 do { traceTc "uUnfilledVar2 not ok" $ vcat [ text "tv1:" <+> ppr tv1 , text "ty2:" <+> ppr ty2 - , text "simple-unify-chk:" <+> ppr (simpleUnifyCheck UC_OnTheFly tv1 ty2) - , text "touchability:" <+> ppr (touchabilityAndShapeTest cur_lvl tv1 ty2)] + , text "simple-unify-chk:" <+> ppr (simpleUnifyCheck UC_OnTheFly cur_lvl tv1 ty2) + ] -- Occurs check or an untouchable: just defer -- NB: occurs check isn't necessarily fatal: -- eg tv1 occurred in type family parameter @@ -2585,9 +2591,8 @@ lhsPriority tv ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Question: given a homogeneous equality (alpha ~# ty), when is it OK to unify alpha := ty? - -This note only applied to /homogeneous/ equalities, in which both -sides have the same kind. +(This note only applies to /homogeneous/ equalities, in which both +sides have the same kind.) There are five reasons not to unify: @@ -2681,7 +2686,7 @@ Needless to say, all there are wrinkles: * In the constraint solver, we track where Given equalities occur and use that to guard unification in - GHC.Tc.Utils.Unify.touchabilityAndShapeTest. More details in + GHC.Tc.Utils.Unify.touchabilityTest. More details in Note [Tracking Given equalities] in GHC.Tc.Solver.InertSet Historical note: in the olden days (pre 2021) the constraint solver @@ -2922,12 +2927,34 @@ data UnifyCheckCaller = UC_OnTheFly -- Called from the on-the-fly unifier | UC_QuickLook -- Called from Quick Look | UC_Solver -- Called from constraint solver - | UC_Defaulting -- Called when doing top-level defaulting -simpleUnifyCheck :: UnifyCheckCaller -> TcTyVar -> TcType -> Bool --- simpleUnifyCheck does a fast check: True <=> unification is OK --- If it says 'False' then unification might still be OK, but --- it'll take more work to do -- use the full checkTypeEq +-- | The result type of 'simpleUnifyCheck'. +data SimpleUnifyResult + -- | Definitely cannot unify (untouchable variable or incompatible top-shape) + = SUC_CannotUnify + -- | The variable is touchable and the top-shape test passed, but + -- it may or may not be OK to unify + | SUC_NotSure + -- | Definitely OK to unify + | SUC_CanUnify + deriving stock (Eq, Ord, Show) +instance Semigroup SimpleUnifyResult where + no@SUC_CannotUnify <> _ = no + SUC_CanUnify <> r = r + _ <> no@SUC_CannotUnify = no + r <> SUC_CanUnify = r + ns@SUC_NotSure <> SUC_NotSure = ns + +instance Outputable SimpleUnifyResult where + ppr = \case + SUC_CannotUnify -> text "SUC_CannotUnify" + SUC_NotSure -> text "SUC_NotSure" + SUC_CanUnify -> text "SUC_CanUnify" + +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'). -- -- * Rejects if lhs_tv occurs in rhs_ty (occurs check) -- * Rejects foralls unless @@ -2938,9 +2965,17 @@ simpleUnifyCheck :: UnifyCheckCaller -> TcTyVar -> TcType -> Bool -- * Does 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 lhs_tv rhs - = go rhs +simpleUnifyCheck caller given_eq_lvl lhs_tv rhs + | not $ touchabilityTest given_eq_lvl lhs_tv + = SUC_CannotUnify + | not $ checkTopShape lhs_info rhs + = SUC_CannotUnify + | rhs_is_ok rhs + = SUC_CanUnify + | otherwise + = SUC_NotSure where + lhs_info = metaTyVarInfo lhs_tv !(occ_in_ty, occ_in_co) = mkOccFolders lhs_tv @@ -2960,33 +2995,32 @@ simpleUnifyCheck caller lhs_tv rhs UC_Solver -> True UC_QuickLook -> True UC_OnTheFly -> False - UC_Defaulting -> True - go (TyVarTy tv) + rhs_is_ok (TyVarTy tv) | lhs_tv == tv = False | tcTyVarLevel tv `strictlyDeeperThan` lhs_tv_lvl = False | lhs_tv_is_concrete, not (isConcreteTyVar tv) = False | occ_in_ty $! (tyVarKind tv) = False | otherwise = True - go (FunTy {ft_af = af, ft_mult = w, ft_arg = a, ft_res = r}) + rhs_is_ok (FunTy {ft_af = af, ft_mult = w, ft_arg = a, ft_res = r}) | not forall_ok, isInvisibleFunArg af = False - | otherwise = go w && go a && go r + | otherwise = rhs_is_ok w && rhs_is_ok a && rhs_is_ok r - go (TyConApp tc tys) + rhs_is_ok (TyConApp tc tys) | lhs_tv_is_concrete, not (isConcreteTyCon tc) = False | not forall_ok, not (isTauTyCon tc) = False | not fam_ok, not (isFamFreeTyCon tc) = False - | otherwise = all go tys + | otherwise = all rhs_is_ok tys - go (ForAllTy (Bndr tv _) ty) - | forall_ok = go (tyVarKind tv) && (tv == lhs_tv || go ty) + rhs_is_ok (ForAllTy (Bndr tv _) ty) + | forall_ok = rhs_is_ok (tyVarKind tv) && (tv == lhs_tv || rhs_is_ok ty) | otherwise = False - go (AppTy t1 t2) = go t1 && go t2 - go (CastTy ty co) = not (occ_in_co co) && go ty - go (CoercionTy co) = not (occ_in_co co) - go (LitTy {}) = True + rhs_is_ok (AppTy t1 t2) = rhs_is_ok t1 && rhs_is_ok t2 + rhs_is_ok (CastTy ty co) = not (occ_in_co co) && rhs_is_ok ty + rhs_is_ok (CoercionTy co) = not (occ_in_co co) + rhs_is_ok (LitTy {}) = True mkOccFolders :: TcTyVar -> (TcType -> Bool, TcCoercion -> Bool) @@ -3073,10 +3107,7 @@ reductionCoercion is Refl. See `canEqCanLHSFinish_no_unification`. data PuResult a b = PuFail CheckTyEqResult | PuOK (Bag a) b - -instance Functor (PuResult a) where - fmap _ (PuFail prob) = PuFail prob - fmap f (PuOK cts x) = PuOK cts (f x) + deriving stock (Functor, Foldable, Traversable) instance Applicative (PuResult a) where pure x = PuOK emptyBag x @@ -3192,15 +3223,147 @@ famAppArgFlags flags@(TEF { tef_unifying = unifying }) | not deeply = Unifying info lvl LC_Check zap_promotion unifying = unifying -type FamAppBreaker a = TcType -> TcM (PuResult a Reduction) - -- Given a family-application ty, return a Reduction :: ty ~ cvb - -- where 'cbv' is a fresh loop-breaker tyvar (for Given), or - -- just a fresh TauTv (for Wanted) +-- | How to break a family-application cycle when checking a type equality. +-- Given a family-application @fam_app@, return a @'Reduction' :: fam_app ~ cbv@ +-- where @cbv@ is a fresh cycle-breaker tyvar (for Given), or +-- a fresh 'TauTv' (for Wanted). +data FamAppBreaker a where + BreakGiven :: FamAppBreaker (TcTyVar, TcType) + BreakWanted :: CtEvidence -> TcTyVar -> FamAppBreaker Ct + +-- | Dispatch on a 'FamAppBreaker' to break a family-application cycle. +-- See Note [Type equality cycles] in GHC.Tc.Solver.Equality. +famAppBreaker :: FamAppBreaker a -> TcType -> TcM (PuResult a Reduction) +famAppBreaker BreakGiven fam_app + -- Why reflexive? See Detail (4) of Note [Type equality cycles] in GHC.Tc.Solver.Equality + = do { new_tv <- newCycleBreakerTyVar (typeKind fam_app) + ; return (PuOK (unitBag (new_tv, fam_app)) + (mkReflRedn Nominal (mkTyVarTy new_tv))) } +famAppBreaker (BreakWanted ev lhs_tv) fam_app + -- Occurs check or skolem escape; so flatten. + = do { let fam_app_kind = typeKind fam_app + ; reason <- checkPromoteFreeVars cteInsolubleOccurs + lhs_tv lhs_tv_lvl (tyCoVarsOfType fam_app_kind) + ; if not (cterHasNoProblem reason) -- Failed to promote free vars + then return $ PuFail reason + else + do { new_tv_ty <- + case lhs_tv_info of + ConcreteTv conc_info -> + -- Make a concrete tyvar if lhs_tv is concrete + -- e.g. alpha[2,conc] ~ Maybe (F beta[4]) + -- We want to flatten to + -- alpha[2,conc] ~ Maybe gamma[2,conc] + -- gamma[2,conc] ~ F beta[4] + newConcreteTyVarTyAtLevel conc_info lhs_tv_lvl fam_app_kind + _ -> newMetaTyVarTyAtLevel lhs_tv_lvl fam_app_kind + ; let pty = mkPrimEqPredRole Nominal fam_app new_tv_ty + ; hole <- newVanillaCoercionHole pty + ; let new_ev = CtWanted { ctev_pred = pty + , ctev_dest = HoleDest hole + , ctev_loc = cb_loc + , ctev_rewriters = ctEvRewriters ev } + ; return (PuOK (singleCt (mkNonCanonical new_ev)) + (mkReduction (HoleCo hole) new_tv_ty)) } } + where + (lhs_tv_info, lhs_tv_lvl) = case tcTyVarDetails lhs_tv of + MetaTv { mtv_info = info, mtv_tclvl = lvl } -> (info,lvl) + _ -> pprPanic "famAppBreaker BreakWanted: lhs_tv is not a meta-tyvar" (ppr lhs_tv) + -- See Detail (7) of Note [Type equality cycles] in GHC.Tc.Solver.Equality + cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin + +instance Outputable (FamAppBreaker a) where + ppr BreakGiven = text "BreakGiven" + ppr (BreakWanted ev tv) = parens $ text "BreakWanted" <+> ppr ev <+> ppr tv + +tefConcrete :: TyEqFlags a -> Bool +tefConcrete (TEF { tef_unifying = Unifying info _ _ }) = isConcreteInfo info +tefConcrete (TEF { tef_unifying = NotUnifying }) = False + +mkTEFA_Break :: CtEvidence -> EqRel -> FamAppBreaker a -> TyEqFamApp a +mkTEFA_Break ev eq_rel breaker + | NomEq <- eq_rel + , not cycle_breaker_origin + = TEFA_Break breaker + | otherwise + = TEFA_Recurse + where + -- cycle_breaker_origin: see Detail (7) of Note [Type equality cycles] + -- in GHC.Tc.Solver.Equality + cycle_breaker_origin = case ctLocOrigin (ctEvLoc ev) of + CycleBreakerOrigin {} -> True + _ -> False + +notUnifying_TEFTask :: CheckTyEqProblem -> CanEqLHS -> TyEqFlags a +-- Used for the non-unifying cases (checkTypeEq in Solver.Monad) +notUnifying_TEFTask occ_prob lhs + = TEF { tef_foralls = False + , tef_lhs = lhs + , tef_unifying = NotUnifying + , tef_fam_app = TEFA_Recurse + , tef_occurs = occ_prob } + +unifyingLHSMetaTyVar_TEFTask :: CtEvidence -> TcTyVar -> TyEqFlags Ct +-- Used for the unifying case (canEqCanLHSFinish_try_unification in Solver.Equality) +unifyingLHSMetaTyVar_TEFTask ev lhs_tv + = TEF { tef_foralls = False + , tef_fam_app = mkTEFA_Break ev NomEq (BreakWanted ev lhs_tv) + , tef_unifying = Unifying lhs_tv_info lhs_tv_lvl (LC_Promote False) + , tef_lhs = TyVarLHS lhs_tv + , tef_occurs = cteInsolubleOccurs } + where + (lhs_tv_info, lhs_tv_lvl) = case tcTyVarDetails lhs_tv of + MetaTv { mtv_info = info, mtv_tclvl = lvl } -> (info, lvl) + _ -> pprPanic "unifyingLHSMetaTyVar_TEFTask: not a meta-tyvar" (ppr lhs_tv) checkTyEqRhs :: forall a. TyEqFlags a -> TcType -- Already zonked -> TcM (PuResult a Reduction) -checkTyEqRhs flags ty +-- Crucial special case for a top-level equality of the form 'alpha ~ F tys'. +-- We don't want to flatten that (F tys), as this gets us right back to where +-- we started! +-- See also Note [Special case for top-level of Given equality] +checkTyEqRhs flags rhs + | Just (TyFamLHS tc tys) <- canTyFamEqLHS_maybe rhs + , not $ tefConcrete flags + = recurseIntoFamTyConApp flags tc tys + | otherwise + = check_ty_eq_rhs flags rhs + +{- Note [Special case for top-level of Given equality] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We take care when examining + [G] F ty ~ G (...(F ty)...) +where both sides are TyFamLHSs. We don't want to flatten that RHS to + [G] F ty ~ cbv + [G] G (...(F ty)...) ~ cbv +Instead we'd like to say "occurs-check" and swap LHS and RHS, which yields a +canonical constraint + [G] G (...(F ty)...) ~ F ty +That tends to rewrite a big type to smaller one. This happens in T15703, +where we had: + [G] Pure g ~ From1 (To1 (Pure g)) +Making a loop breaker and rewriting left to right just makes much bigger +types than swapping it over. + +(We might hope to have swapped it over before getting to checkTypeEq, +but better safe than sorry.) + +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. +-} + +recurseIntoFamTyConApp :: TyEqFlags a -> TyCon -> [TcType] -> TcM (PuResult a Reduction) +recurseIntoFamTyConApp flags tc tys + = recurseIntoTyConApp (famAppArgFlags flags) tc tys + +check_ty_eq_rhs :: forall a. TyEqFlags a + -> TcType -- Already zonked + -> TcM (PuResult a Reduction) +check_ty_eq_rhs flags ty = case ty of LitTy {} -> okCheckRefl ty TyConApp tc tys -> checkTyConApp flags ty tc tys @@ -3214,26 +3377,24 @@ checkTyEqRhs flags ty , not (tef_foralls flags) -> failCheckWith impredicativeProblem -- Not allowed (TyEq:F) | otherwise - -> do { w_res <- checkTyEqRhs flags w - ; a_res <- checkTyEqRhs flags a - ; r_res <- checkTyEqRhs flags r + -> do { w_res <- check_ty_eq_rhs flags w + ; a_res <- check_ty_eq_rhs flags a + ; r_res <- check_ty_eq_rhs flags r ; return (mkFunRedn Nominal af <$> w_res <*> a_res <*> r_res) } - AppTy fun arg -> do { fun_res <- checkTyEqRhs flags fun - ; arg_res <- checkTyEqRhs flags arg + AppTy fun arg -> do { fun_res <- check_ty_eq_rhs flags fun + ; arg_res <- check_ty_eq_rhs flags arg ; return (mkAppRedn <$> fun_res <*> arg_res) } - CastTy ty co -> do { ty_res <- checkTyEqRhs flags ty + CastTy ty co -> do { ty_res <- check_ty_eq_rhs flags ty ; co_res <- checkCo flags co ; return (mkCastRedn1 Nominal ty <$> co_res <*> ty_res) } CoercionTy co -> do { co_res <- checkCo flags co ; return (mkReflCoRedn Nominal <$> co_res) } - ForAllTy {} - | tef_foralls flags -> okCheckRefl ty - | otherwise -> failCheckWith impredicativeProblem -- Not allowed (TyEq:F) - + ForAllTy {} -> return $ PuFail impredicativeProblem -- Not allowed (TyEq:F) +{-# INLINEABLE check_ty_eq_rhs #-} ------------------- checkCo :: TyEqFlags a -> Coercion -> TcM (PuResult a Coercion) @@ -3388,15 +3549,14 @@ checkTyConApp flags@(TEF { tef_unifying = unifying, tef_foralls = foralls_ok }) else do { let (fun_args, extra_args) = splitAt (tyConArity tc) tys fun_app = mkTyConApp tc fun_args ; fun_res <- checkFamApp flags fun_app tc fun_args - ; extra_res <- mapCheck (checkTyEqRhs flags) extra_args - ; traceTc "Over-sat" (ppr tc <+> ppr tys $$ ppr arity $$ pprPur fun_res $$ pprPur extra_res) + ; extra_res <- mapCheck (check_ty_eq_rhs flags) extra_args ; return (mkAppRedns <$> fun_res <*> extra_res) } | Just ty' <- rewriterView tc_app -- e.g. S a where type S a = F [a] -- or type S a = Int -- See Note [Forgetful synonyms in checkTyConApp] - = checkTyEqRhs flags ty' + = check_ty_eq_rhs flags ty' | not (isTauTyCon tc || foralls_ok) = failCheckWith impredicativeProblem @@ -3411,7 +3571,7 @@ checkTyConApp flags@(TEF { tef_unifying = unifying, tef_foralls = foralls_ok }) recurseIntoTyConApp :: TyEqFlags a -> TyCon -> [TcType] -> TcM (PuResult a Reduction) recurseIntoTyConApp flags tc tys - = do { tys_res <- mapCheck (checkTyEqRhs flags) tys + = do { tys_res <- mapCheck (check_ty_eq_rhs flags) tys ; return (mkTyConAppRedn Nominal tc <$> tys_res) } ------------------- @@ -3430,16 +3590,16 @@ checkFamApp flags@(TEF { tef_unifying = unifying, tef_occurs = occ_prob , tcEqTyConApps lhs_tc lhs_tys tc tys -> case fam_app_flag of TEFA_Recurse -> failCheckWith (cteProblem occ_prob) - TEFA_Break breaker -> breaker fam_app + TEFA_Break breaker -> famAppBreaker breaker fam_app _ | Unifying lhs_info _ _ <- unifying , isConcreteInfo lhs_info -> case fam_app_flag of TEFA_Recurse -> failCheckWith (cteProblem cteConcrete) - TEFA_Break breaker -> breaker fam_app + TEFA_Break breaker -> famAppBreaker breaker fam_app TEFA_Recurse - -> do { tys_res <- mapCheck (checkTyEqRhs arg_flags) tys + -> do { tys_res <- mapCheck (check_ty_eq_rhs arg_flags) tys ; traceTc "under" (ppr tc $$ pprPur tys_res $$ ppr flags) ; return (mkTyConAppRedn Nominal tc <$> tys_res) } @@ -3448,16 +3608,16 @@ checkFamApp flags@(TEF { tef_unifying = unifying, tef_occurs = occ_prob -- alpha[2] ~ Maybe (F beta[4]) Level-check problem: break -- NB: in the latter case, don't promote beta[4]; hence arg_flags! TEFA_Break breaker - -> do { tys_res <- mapCheck (checkTyEqRhs arg_flags) tys + -> do { tys_res <- mapCheck (check_ty_eq_rhs arg_flags) tys ; case tys_res of PuOK cts redns -> return (PuOK cts (mkTyConAppRedn Nominal tc redns)) - PuFail {} -> breaker fam_app } + PuFail {} -> famAppBreaker breaker fam_app } where arg_flags = famAppArgFlags flags ------------------- checkTyVar :: forall a. TyEqFlags a -> TcTyVar -> TcM (PuResult a Reduction) -checkTyVar (TEF { tef_lhs = lhs, tef_unifying = unifying, tef_occurs = occ_prob }) occ_tv +checkTyVar flags@(TEF { tef_lhs = lhs, tef_unifying = unifying, tef_occurs = occ_prob }) occ_tv = case lhs of TyFamLHS {} -> success -- Nothing to do if the LHS is a type-family TyVarLHS lhs_tv -> check_tv unifying lhs_tv @@ -3491,7 +3651,7 @@ checkTyVar (TEF { tef_lhs = lhs, tef_unifying = unifying, tef_occurs = occ_prob | isConcreteInfo lhs_tv_info , not (isConcreteTyVar occ_tv) = if can_make_concrete occ_tv - then promote lhs_tv lhs_tv_info lhs_tv_lvl + then promote lhs_tv_info lhs_tv_lvl else failCheckWith (cteProblem cteConcrete) | lvl_occ `strictlyDeeperThan` lhs_tv_lvl @@ -3500,7 +3660,7 @@ checkTyVar (TEF { tef_lhs = lhs, tef_unifying = unifying, tef_occurs = occ_prob LC_Check -> failCheckWith (cteProblem cteSkolemEscape) LC_Promote {} | isSkolemTyVar occ_tv -> failCheckWith (cteProblem cteSkolemEscape) - | otherwise -> promote lhs_tv lhs_tv_info lhs_tv_lvl + | otherwise -> promote lhs_tv_info lhs_tv_lvl | otherwise = simple_occurs_check lhs_tv @@ -3525,7 +3685,7 @@ checkTyVar (TEF { tef_lhs = lhs, tef_unifying = unifying, tef_occurs = occ_prob --------------------- -- occ_tv is definitely a MetaTyVar - promote lhs_tv lhs_tv_info lhs_tv_lvl + promote lhs_tv_info lhs_tv_lvl | MetaTv { mtv_info = info_occ, mtv_tclvl = lvl_occ } <- tcTyVarDetails occ_tv = do { let new_info | isConcreteInfo lhs_tv_info = lhs_tv_info | otherwise = info_occ @@ -3534,12 +3694,23 @@ checkTyVar (TEF { tef_lhs = lhs, tef_unifying = unifying, tef_occurs = occ_prob -- c[tau,2] ~ p[tau,3]: want to clone p:=p'[tau,2] -- Check the kind of occ_tv - ; reason <- checkPromoteFreeVars occ_prob lhs_tv lhs_tv_lvl (tyCoVarsOfType (tyVarKind occ_tv)) - - ; if cterHasNoProblem reason -- Successfully promoted - then do { new_tv_ty <- promote_meta_tyvar new_info new_lvl occ_tv - ; okCheckRefl new_tv_ty } - else failCheckWith reason } + -- + -- This is important for several reasons: + -- + -- 1. To ensure there is no occurs check or skolem-escape + -- in the kind of occ_tv. + -- 2. If the LHS is a concrete type variable and the RHS is an + -- unfilled meta-tyvar, we need to ensure that the kind of + -- 'occ_tv' is concrete. Test cases: T23051, T23176. + ; let occ_kind = tyVarKind occ_tv + ; kind_result <- check_ty_eq_rhs flags occ_kind + ; for kind_result $ \ kind_redn -> + do { let kind_co = reductionCoercion kind_redn + new_kind = reductionReducedType kind_redn + occ_tv' = setTyVarKind occ_tv new_kind + ; new_tv_ty <- promote_meta_tyvar new_info new_lvl occ_tv' + ; return $ mkGReflLeftRedn Nominal new_tv_ty (mkSymCo kind_co) + } } | otherwise = pprPanic "promote" (ppr occ_tv) @@ -3591,16 +3762,15 @@ promote_meta_tyvar info dest_lvl occ_tv ------------------------- -touchabilityAndShapeTest :: TcLevel -> TcTyVar -> TcType -> Bool --- This is the key test for untouchability: +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 <=> touchability and shape are OK -touchabilityAndShapeTest given_eq_lvl tv rhs - | MetaTv { mtv_info = info, mtv_tclvl = tv_lvl } <- tcTyVarDetails tv - , tv_lvl `deeperThanOrSame` given_eq_lvl - , checkTopShape info rhs - = True +-- +-- @True@ <=> the variable is touchable +touchabilityTest given_eq_lvl tv + | MetaTv { mtv_tclvl = tv_lvl } <- tcTyVarDetails tv + = tv_lvl `deeperThanOrSame` given_eq_lvl | otherwise = False ===================================== testsuite/tests/rep-poly/T19709b.stderr ===================================== @@ -1,10 +1,9 @@ - T19709b.hs:11:15: error: [GHC-55287] • The argument ‘(error @Any "e2")’ of ‘levfun’ does not have a fixed runtime representation. Its type is: - a1 :: TYPE r0 - Cannot unify ‘Any’ with the type variable ‘r0’ + a0 :: TYPE c0 + Cannot unify ‘Any’ with the type variable ‘c0’ because the former is not a concrete ‘RuntimeRep’. • In the first argument of ‘levfun’, namely ‘(error @Any "e2")’ In the first argument of ‘seq’, namely ‘levfun (error @Any "e2")’ ===================================== testsuite/tests/rep-poly/T23154.stderr ===================================== @@ -8,3 +8,8 @@ T23154.hs:7:1: error: [GHC-52083] The first pattern in the equation for ‘f’ cannot be assigned a fixed runtime representation, not even by defaulting. Suggested fix: Add a type signature. + +T23154.hs:7:1: error: [GHC-52083] + The first pattern in the equation for ‘f’ + cannot be assigned a fixed runtime representation, not even by defaulting. + Suggested fix: Add a type signature. ===================================== testsuite/tests/rep-poly/T23903.stderr ===================================== @@ -1,10 +1,9 @@ - T23903.hs:21:1: error: [GHC-55287] • The first pattern in the equation for ‘f’ does not have a fixed runtime representation. Its type is: - t0 :: TYPE cx0 - Cannot unify ‘Rep a’ with the type variable ‘cx0’ + Unbox a :: TYPE c0 + Cannot unify ‘Rep a’ with the type variable ‘c0’ because the former is not a concrete ‘RuntimeRep’. • The equation for ‘f’ has one visible argument, but its type ‘a #-> ()’ has none ===================================== testsuite/tests/simplCore/should_compile/simpl017.stderr ===================================== @@ -1,20 +1,25 @@ -simpl017.hs:55:12: error: [GHC-46956] - • Couldn't match type ‘v0’ with ‘v’ - Expected: [E m i] -> E' v m a - Actual: [E m i] -> E' v0 m a - because type variable ‘v’ would escape its scope - This (rigid, skolem) type variable is bound by - a type expected by the context: - forall v. [E m i] -> E' v m a - at simpl017.hs:55:12 - • In the first argument of ‘return’, namely ‘f’ - In a stmt of a 'do' block: return f +simpl017.hs:55:5: error: [GHC-83865] + • Couldn't match type: [E m i] -> E' v0 m a + with: forall v. [E m i] -> E' v m a + Expected: m (forall v. [E m i] -> E' v m a) + Actual: m ([E m i] -> E' v0 m a) + • In a stmt of a 'do' block: return f In the first argument of ‘E’, namely ‘(do let ix :: [E m i] -> m i ix [i] = runE i {-# INLINE f #-} .... return f)’ + In the expression: + E (do let ix :: [E m i] -> m i + ix [i] = runE i + {-# INLINE f #-} + .... + return f) • Relevant bindings include f :: [E m i] -> E' v0 m a (bound at simpl017.hs:54:9) + ix :: [E m i] -> m i (bound at simpl017.hs:52:9) + a :: arr i a (bound at simpl017.hs:50:11) + liftArray :: arr i a -> E m (forall v. [E m i] -> E' v m a) + (bound at simpl017.hs:50:1) ===================================== testsuite/tests/typecheck/should_compile/T26030.hs ===================================== @@ -0,0 +1,25 @@ +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE GADTs #-} + +-- This program was rejected by GHC 9.12 due to a bug with +-- unification in QuickLook. +module T26030 where + +import Data.Kind + +type S :: Type -> Type +data S a where + S1 :: S Bool + S2 :: S Char + +type F :: Type -> Type +type family F a where + F Bool = Bool + F Char = Char + +foo :: forall a. S a -> IO (F a) +foo sa1 = do + () <- return () + case sa1 of + S1 -> return $ False + S2 -> return 'x' ===================================== testsuite/tests/typecheck/should_compile/T27149.hs ===================================== @@ -0,0 +1,18 @@ +{-# LANGUAGE TypeFamilies #-} +module T27149 where + +import Data.Kind (Type) + +type T :: Type -> Type +data T a where + MkT :: T Bool + +type F :: Type -> Type +type family F a where + F Bool = Int + +f :: IO (T a) -> (Bool -> Int) -> IO (F a) +f mt g = do + t <- mt + case t of + MkT -> return $ g True ===================================== testsuite/tests/typecheck/should_compile/all.T ===================================== @@ -889,6 +889,8 @@ test('T21909', normal, compile, ['']) test('T21909b', normal, compile, ['']) test('T21443', normal, compile, ['']) test('T22194', normal, compile, ['']) +test('T26030', normal, compile, ['']) +test('T27149', normal, compile, ['']) test('QualifiedRecordUpdate', [ extra_files(['QualifiedRecordUpdate_aux.hs']) ] , multimod_compile, ['QualifiedRecordUpdate', '-v0']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/97981d8bc1596b9e06d10c5938d13cd... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/97981d8bc1596b9e06d10c5938d13cd... You're receiving this email because of your account on gitlab.haskell.org.