Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC Commits: 67a177b4 by sheaf at 2025-05-21T10:17:04-04: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 - - - - - 4020972c by sheaf at 2025-05-21T10:17:04-04:00 FixedRuntimeRepError: omit unhelpful explanation This commit tweaks the FixedRuntimeRepError case of pprTcSolverReportMsg, to avoid including an explanation which refers to a type variable that appears nowhere else. For example, the old error message could look like the following: The pattern binding does not have a fixed runtime representation. Its type is: T :: TYPE R Cannot unify ‘R’ with the type variable ‘c0’ because the former is not a concrete ‘RuntimeRep’. With this commit, we now omit the last two lines, because the concrete type variable (here 'c0') does not appear in the type displayed to the user (here 'T :: TYPE R'). - - - - - 15 changed files: - compiler/GHC/Tc/Errors/Ppr.hs - 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/RepPolyTuple4.stderr - testsuite/tests/rep-poly/T19709b.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/all.T - + testsuite/tests/typecheck/should_fail/T25950.hs - + testsuite/tests/typecheck/should_fail/T25950.stderr - testsuite/tests/typecheck/should_fail/all.T Changes: ===================================== compiler/GHC/Tc/Errors/Ppr.hs ===================================== @@ -4043,9 +4043,13 @@ pprTcSolverReportMsg _ (FixedRuntimeRepError frr_origs) = Nothing -> empty Just o -> other_context o , case mb_not_conc of - Nothing -> empty - Just (conc_tv, not_conc) -> - unsolved_concrete_eq_explanation conc_tv not_conc ] + Just (conc_tv, not_conc) + | conc_tv `elemVarSet` tyCoVarsOfType ty + -- Only show this message if 'conc_tv' appears somewhere + -- in the type, otherwise it's not helpful. + -> unsolved_concrete_eq_explanation conc_tv not_conc + _ -> empty + ] -- Don't print out the type (only the kind), if the type includes -- a confusing cast, unless the user passed -fprint-explicit-coercions. ===================================== compiler/GHC/Tc/Gen/App.hs ===================================== @@ -2066,18 +2066,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 - = 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,5 +1,6 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DuplicateRecordFields #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiWayIf #-} module GHC.Tc.Solver.Equality( @@ -1888,81 +1889,102 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs | 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 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 + , 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 @@ -1989,6 +2011,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 @@ -2005,6 +2038,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 @@ -2297,8 +2342,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. @@ -2307,7 +2353,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 ===================================== @@ -129,7 +129,7 @@ module GHC.Tc.Solver.Monad ( pprEq, -- Enforcing invariants for type equalities - checkTypeEq, checkTouchableTyVarEq + checkTypeEq ) where import GHC.Prelude @@ -228,8 +228,6 @@ import GHC.Data.Graph.Directed import qualified Data.Set as Set import GHC.Unit.Module.Graph -import GHC.Data.Maybe - {- ********************************************************************* * * SolverStage and StopOrContinue @@ -2416,81 +2414,31 @@ 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 = metaTyVarInfo lhs_tv -- lhs_tv should be a meta-tyvar - - is_concrete_lhs_tv = isJust $ concreteInfo_maybe 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 return $ PuFail (cteProblem cteConcrete) - else recurseIntoFamTyConApp flags tc tys - | otherwise - = checkTyEqRhs flags rhs - - flags = unifyingLHSMetaTyVar_TEFTask ev lhs_tv - ------------------------- 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 - = recurseIntoFamTyConApp given_flags tc tys - | otherwise - = checkTyEqRhs given_flags rhs - + wanted_flags :: TyEqFlags TcM Ct wanted_flags = notUnifying_TEFTask occ_prob lhs -- checkTypeEq deals only with the non-unifying case @@ -2532,31 +2480,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 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. - Note [Don't cycle-break Wanteds when not unifying] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consdier ===================================== compiler/GHC/Tc/Types/Constraint.hs ===================================== @@ -279,10 +279,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 ===================================== @@ -29,7 +29,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, mightEqualLater, @@ -55,7 +55,7 @@ module GHC.Tc.Utils.Unify ( TyEqFamApp(..), FamAppBreaker(..), checkPromoteFreeVars, - simpleUnifyCheck, UnifyCheckCaller(..), + simpleUnifyCheck, UnifyCheckCaller(..), SimpleUnifyResult(..), fillInferResult, ) where @@ -2482,10 +2482,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 @@ -2530,8 +2529,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 @@ -2590,9 +2589,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: @@ -2688,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 @@ -2929,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 @@ -2945,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 (tyVarName lhs_tv) @@ -2967,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 :: Name -> (TcType -> Bool, TcCoercion -> Bool) @@ -3078,8 +3105,13 @@ We must jolly well use that reductionReduced type, even though the reductionCoercion is Refl. See `canEqCanLHSFinish_no_unification`. -} -data PuResult a b = PuFail CheckTyEqResult - | PuOK (Bag a) b +data PuResult a b + -- | Pure unifier failure. + -- + -- Invariant: the CheckTyEqResult is not 'cteOK'; that it, it specifies a problem. + = PuFail CheckTyEqResult + -- | Pure unifier success. + | PuOK (Bag a) b deriving stock (Functor, Foldable, Traversable) instance Applicative (PuResult a) where @@ -3414,15 +3446,15 @@ famAppBreaker (BreakWanted ev lhs_tv) fam_app ; return (PuOK (singleCt (mkNonCanonical $ CtWanted new_ev)) (mkReduction (HoleCo hole) new_tv_ty)) } } where + fam_app_kind = typeKind fam_app (lhs_tv_info, lhs_tv_lvl) = case tcTyVarDetails lhs_tv of MetaTv { mtv_info = info, mtv_tclvl = lvl } -> (info,lvl) -- lhs_tv should be a meta-tyvar - _ -> pprPanic "checkTouchableTyVarEq" (ppr lhs_tv) - fam_app_kind = typeKind fam_app - -- See Detail (7) of the Note + _ -> pprPanic "famAppBreaker BreakWanted: lhs_tv is not a meta-tyvar" + (ppr lhs_tv) cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin - + -- CycleBreakerOrigin: see Detail (7) of Note [Type equality cycles] instance Outputable (TyEqFlags m a) where ppr = \case @@ -3492,12 +3524,95 @@ famAppArgFlags flags = case flags of -> LC_Check { lc_lvlc = lvl, lc_lenient = False } lc -> lc +{- Note [checkTyEqRhs] +~~~~~~~~~~~~~~~~~~~~~~ +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, +invariants described by `ty_eq_flags`. It can succeded or fail; in +the latter case it returns a `CheckTyEqResult` that describes why it +failed. + +When `lhs` is a touchable type variable, so unification might happen, then +`checkTyEqRhs` enforces the unification preconditions of Note [Unification preconditions]. + +Notably, it can check for things like: + * Insoluble occurs check + e.g. alpha[tau] ~ [alpha] + or F Int ~ [F Int] + * Potentially-soluble occurs check + e.g. alpha[tau] ~ [F alpha beta] + * Impredicativity error: + e.g. alpha[tau] ~ (forall a. a->a) + * Skolem escape + e.g alpha[1] ~ (b[sk:2], Int) + * Concreteness error + e.g. alpha[conc] ~ r[sk] + +Its specific behaviour is governed by the `TyEqFlags` that are passed +to it; see Note [TyEqFlags]. + +Note, however, that `checkTyEqRhs` specifically does /not/ check for: + * Touchability of the LHS (in the case of a unification variable) + * Shape of the LHS (e.g. we can't unify Int with a TyVarTv) +These things are checked by `simpleUnifyCheck`. +-} + + +-- | Perform the checks specified by the 'TyEqFlags' on the RHS, in order to +-- enforce the unification preconditions of Note [Unification preconditions]. +-- +-- See Note [checkTyEqRhs]. checkTyEqRhs :: forall m a . Monad m => TyEqFlags m a -> TcType -- Already zonked -> m (PuResult a Reduction) -checkTyEqRhs flags ty +checkTyEqRhs flags rhs + -- 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] + | 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. +-} + +check_ty_eq_rhs :: forall m a + . Monad m + => TyEqFlags m a + -> TcType -- Already zonked + -> m (PuResult a Reduction) +check_ty_eq_rhs flags ty = case ty of LitTy {} -> return $ okCheckRefl ty TyConApp tc tys -> checkTyConApp flags ty tc tys @@ -3510,16 +3625,16 @@ checkTyEqRhs flags ty | isInvisibleFunArg af -- e.g. Num a => blah -> return $ PuFail 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) } @@ -3527,7 +3642,7 @@ checkTyEqRhs flags ty ; return (mkReflCoRedn Nominal <$> co_res) } ForAllTy {} -> return $ PuFail impredicativeProblem -- Not allowed (TyEq:F) -{-# INLINEABLE checkTyEqRhs #-} +{-# INLINEABLE check_ty_eq_rhs #-} ------------------- checkCo :: Monad m => TyEqFlags m a -> Coercion -> m (PuResult a Coercion) @@ -3702,14 +3817,14 @@ checkTyConApp flags tc_app tc tys 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 + ; 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) = return $ PuFail impredicativeProblem @@ -3727,7 +3842,7 @@ recurseIntoTyConApp :: Monad m -> TyCon -> [TcType] -> m (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) } recurseIntoFamTyConApp :: Monad m @@ -3888,7 +4003,7 @@ checkTyVar flags occ_tv -- 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 <- checkTyEqRhs flags occ_kind + ; 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 @@ -4010,16 +4125,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/RepPolyTuple4.stderr ===================================== @@ -6,8 +6,6 @@ RepPolyTuple4.hs:8:7: error: [GHC-55287] When unifying: • a0 -> b0 -> (# a0, b0 #) • a -> a -> (# a, a #) - Cannot unify ‘r’ with the type variable ‘w1’ - because the former is not a concrete ‘RuntimeRep’. • The second component of the unboxed tuple does not have a fixed runtime representation. Its type is: @@ -15,8 +13,6 @@ RepPolyTuple4.hs:8:7: error: [GHC-55287] When unifying: • a0 -> b0 -> (# a0, b0 #) • a -> a -> (# a, a #) - Cannot unify ‘r’ with the type variable ‘w0’ - because the former is not a concrete ‘RuntimeRep’. • In the expression: (#,#) @_ @_ In an equation for ‘bar’: bar = (#,#) @_ @_ ===================================== testsuite/tests/rep-poly/T19709b.stderr ===================================== @@ -2,11 +2,8 @@ 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 - When unifying: - • a0 - • a1 - Cannot unify ‘Any’ with the type variable ‘r0’ + a1 :: 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/T23903.stderr ===================================== @@ -2,11 +2,8 @@ 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 - When unifying: - • t0 -> () - • a #-> () - Cannot unify ‘Rep a’ with the type variable ‘cx0’ + t0 :: 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/all.T ===================================== @@ -887,6 +887,7 @@ test('T21909b', normal, compile, ['']) test('T21443', normal, compile, ['']) test('T22194', normal, compile, ['']) test('T25744', normal, compile, ['']) +test('T26030', normal, compile, ['']) test('QualifiedRecordUpdate', [ extra_files(['QualifiedRecordUpdate_aux.hs']) ] , multimod_compile, ['QualifiedRecordUpdate', '-v0']) ===================================== testsuite/tests/typecheck/should_fail/T25950.hs ===================================== @@ -0,0 +1,6 @@ +{-# LANGUAGE PartialTypeSignatures #-} + +module T25950 where + +fails :: _ => a +fails = id $ () ===================================== testsuite/tests/typecheck/should_fail/T25950.stderr ===================================== @@ -0,0 +1,9 @@ +T25950.hs:6:9: error: [GHC-25897] + • Couldn't match expected type ‘a’ with actual type ‘()’ + ‘a’ is a rigid type variable bound by + the inferred type of fails :: a + at T25950.hs:5:1-15 + • In the expression: id $ () + In an equation for ‘fails’: fails = id $ () + • Relevant bindings include fails :: a (bound at T25950.hs:6:1) + ===================================== testsuite/tests/typecheck/should_fail/all.T ===================================== @@ -726,6 +726,7 @@ test('T17594c', normal, compile_fail, ['']) test('T17594d', normal, compile_fail, ['']) test('T17594g', normal, compile_fail, ['']) +test('T25950', normal, compile_fail, ['']) test('T24470a', normal, compile_fail, ['']) test('T24553', normal, compile_fail, ['']) test('T23739b', normal, compile_fail, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/202b201c968de68f864f4c8abbfec71... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/202b201c968de68f864f4c8abbfec71... You're receiving this email because of your account on gitlab.haskell.org.