[Git][ghc/ghc][master] Improve GHC.Tc.Solver.defaultEquality
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Wed Sep 25 21:12:57 UTC 2024
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
6863503c by Simon Peyton Jones at 2024-09-25T17:11:37-04:00
Improve GHC.Tc.Solver.defaultEquality
This MR improves GHC.Tc.Solver.defaultEquality to solve #25251.
The main change is to use checkTyEqRhs to check the equality, so
that we do promotion properly.
But within that we needed a small enhancement to LC_Promote. See
Note [Defaulting equalites] (DE4) and (DE5)
The tricky case is (alas) hard to trigger, so I have not added a
regression test.
- - - - -
3 changed files:
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Utils/Unify.hs
Changes:
=====================================
compiler/GHC/Tc/Solver.hs
=====================================
@@ -29,30 +29,13 @@ module GHC.Tc.Solver(
import GHC.Prelude
-import GHC.Data.Bag
-import GHC.Core.Class
-import GHC.Core
-import GHC.Core.DataCon
-import GHC.Core.Make
-import GHC.Core.Coercion( mkNomReflCo )
-import GHC.Driver.DynFlags
-import GHC.Data.FastString
-import GHC.Data.List.SetOps
-import GHC.Types.Name
-import GHC.Types.DefaultEnv ( ClassDefaults (..), defaultList )
-import GHC.Types.Unique.Set
-import GHC.Types.Id
-import GHC.Utils.Outputable
-import GHC.Builtin.Utils
-import GHC.Builtin.Names
import GHC.Tc.Errors
import GHC.Tc.Errors.Types
import GHC.Tc.Types.Evidence
import GHC.Tc.Solver.Solve ( solveSimpleGivens, solveSimpleWanteds )
import GHC.Tc.Solver.Dict ( makeSuperClasses, solveCallStack )
import GHC.Tc.Solver.Rewrite ( rewriteType )
-import GHC.Tc.Utils.Unify ( buildTvImplication, touchabilityAndShapeTest
- , simpleUnifyCheck, UnifyCheckCaller(..) )
+import GHC.Tc.Utils.Unify
import GHC.Tc.Utils.TcMType as TcM
import GHC.Tc.Utils.Monad as TcM
import GHC.Tc.Zonk.TcType as TcM
@@ -61,17 +44,30 @@ import GHC.Tc.Solver.Monad as TcS
import GHC.Tc.Types.Constraint
import GHC.Tc.Types.CtLoc( mkGivenLoc )
import GHC.Tc.Instance.FunDeps
-import GHC.Core.Predicate
import GHC.Tc.Types.Origin
import GHC.Tc.Utils.TcType
+
+import GHC.Core.Class
+import GHC.Core.Reduction( Reduction, reductionCoercion )
+import GHC.Core
+import GHC.Core.DataCon
+import GHC.Core.Make
+import GHC.Core.Coercion( mkNomReflCo, isReflCo )
+import GHC.Core.Unify ( tcMatchTyKis )
+import GHC.Core.Predicate
import GHC.Core.Type
import GHC.Core.Ppr
import GHC.Core.TyCon ( TyCon, TyConBinder, isTypeFamilyTyCon )
+
+import GHC.Types.Name
+import GHC.Types.DefaultEnv ( ClassDefaults (..), defaultList )
+import GHC.Types.Unique.Set
+import GHC.Types.Id
+
+import GHC.Builtin.Utils
+import GHC.Builtin.Names
import GHC.Builtin.Types
-import GHC.Core.Unify ( tcMatchTyKis )
-import GHC.Unit.Module ( getModule )
-import GHC.Utils.Misc
-import GHC.Utils.Panic
+
import GHC.Types.TyThing ( MonadThings(lookupId) )
import GHC.Types.Var
import GHC.Types.Var.Env
@@ -79,6 +75,18 @@ import GHC.Types.Var.Set
import GHC.Types.Basic
import GHC.Types.Id.Make ( unboxedUnitExpr )
import GHC.Types.Error
+
+import GHC.Driver.DynFlags
+import GHC.Unit.Module ( getModule )
+
+import GHC.Utils.Misc
+import GHC.Utils.Panic
+import GHC.Utils.Outputable
+
+import GHC.Data.FastString
+import GHC.Data.List.SetOps
+import GHC.Data.Bag
+
import qualified GHC.LanguageExtensions as LangExt
import Control.Monad
@@ -515,7 +523,7 @@ tryDefaulting wc
; wc2 <- tryConstraintDefaulting wc1
; wc3 <- tryTypeClassDefaulting wc2
; wc4 <- tryUnsatisfiableGivens wc3
- ; traceTcS "tryDefaulting:after" (ppr wc)
+ ; traceTcS "tryDefaulting:after" (ppr wc4)
; return wc4 }
solveAgainIf :: Bool -> WantedConstraints -> TcS WantedConstraints
@@ -771,35 +779,66 @@ defaultEquality :: CtDefaultingStrategy
-- See Note [Defaulting equalities]
defaultEquality ct
| EqPred NomEq ty1 ty2 <- classifyPredType (ctPred ct)
- , Just tv1 <- getTyVar_maybe ty1
= do { -- Remember: `ct` may not be zonked;
-- see (DE3) in Note [Defaulting equalities]
- z_ty1 <- TcS.zonkTcTyVar tv1
- ; z_ty2 <- TcS.zonkTcType ty2
- ; case getTyVar_maybe z_ty1 of
- Just z_tv1 | defaultable z_tv1 z_ty2
- -> do { default_tv z_tv1 z_ty2
- ; return True }
- _ -> return False }
- | otherwise
- = return False
+ z_ty1 <- TcS.zonkTcType ty1
+ ; z_ty2 <- TcS.zonkTcType ty2
+
+ -- Now see if either LHS or RHS is a bare type variable
+ -- You might think the type variable will only be on the LHS
+ -- but with a type function we might get F t1 ~ alpha
+ ; case (getTyVar_maybe z_ty1, getTyVar_maybe z_ty2) of
+ (Just z_tv1, _) -> try_default_tv z_tv1 z_ty2
+ (_, Just z_tv2) -> try_default_tv z_tv2 z_ty1
+ _ -> return False }
+ | otherwise
+ = return False
+
where
- defaultable tv1 ty2
- = -- Do the standard unification checks;
- -- c.f. uUnfilledVar2 in GHC.Tc.Utils.Unify
- -- EXCEPT drop the untouchability test
- tyVarKind tv1 `tcEqType` typeKind ty2
- && touchabilityAndShapeTest topTcLevel tv1 ty2
- -- topTcLevel makes the untoucability test vacuous,
- -- which is the Whole Point of `defaultEquality`
- -- See (DE2) in Note [Defaulting equalities]
- && simpleUnifyCheck UC_Defaulting tv1 ty2
-
- default_tv tv1 ty2
- = do { unifyTyVar tv1 ty2 -- NB: unifyTyVar adds to the
- -- TcS unification counter
- ; setEvBindIfWanted (ctEvidence ct) EvCanonical $
- evCoercion (mkNomReflCo ty2) }
+ try_default_tv lhs_tv rhs_ty
+ | MetaTv { mtv_info = info, mtv_tclvl = lvl } <- tcTyVarDetails lhs_tv
+ , tyVarKind lhs_tv `tcEqType` typeKind rhs_ty
+ , checkTopShape info rhs_ty
+ -- Do not test for touchability of lhs_tv; that is the whole point!
+ -- See (DE2) in Note [Defaulting equalities]
+ = do { traceTcS "defaultEquality 1" (ppr lhs_tv $$ ppr rhs_ty)
+
+ -- checkTyEqRhs: check that we can in fact unify lhs_tv := rhs_ty
+ -- See Note [Defaulting equalities]
+ -- LC_Promote: promote deeper unification variables (DE4)
+ -- LC_Promote True: ...including under type families (DE5)
+ ; let flags :: TyEqFlags ()
+ flags = TEF { tef_foralls = False
+ , tef_fam_app = TEFA_Recurse
+ , tef_lhs = TyVarLHS lhs_tv
+ , tef_unifying = Unifying info lvl (LC_Promote True)
+ , tef_occurs = cteInsolubleOccurs }
+ ; res :: PuResult () Reduction <- wrapTcS (checkTyEqRhs flags rhs_ty)
+
+ ; case res of
+ PuFail {} -> cant_default_tv "checkTyEqRhs"
+ PuOK _ redn -> assertPpr (isReflCo (reductionCoercion redn)) (ppr redn) $
+ -- With TEFA_Recurse we never get any reductions
+ default_tv }
+ | otherwise
+ = cant_default_tv "fall through"
+
+ where
+ cant_default_tv msg
+ = do { traceTcS ("defaultEquality fails: " ++ msg) $
+ vcat [ ppr lhs_tv <+> char '~' <+> ppr rhs_ty
+ , ppr (tyVarKind lhs_tv)
+ , ppr (typeKind rhs_ty) ]
+ ; return False }
+
+ -- All tests passed: do the unification
+ default_tv
+ = do { traceTcS "defaultEquality success:" (ppr rhs_ty)
+ ; unifyTyVar lhs_tv rhs_ty -- NB: unifyTyVar adds to the
+ -- TcS unification counter
+ ; setEvBindIfWanted (ctEvidence ct) EvCanonical $
+ evCoercion (mkNomReflCo rhs_ty)
+ ; return True }
combineStrategies :: CtDefaultingStrategy -> CtDefaultingStrategy -> CtDefaultingStrategy
combineStrategies default1 default2 ct
@@ -884,22 +923,20 @@ Wrinkles:
given equality is at top level.
(DE3) The contraint we are looking at may not be fully zonked; for example,
- an earlier deafaulting might have affected it. So we zonk-on-the fly in
+ an earlier defaulting might have affected it. So we zonk-on-the fly in
`defaultEquality`.
-Note [Don't default in syntactic equalities]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When there are unsolved syntactic equalities such as
+(DE4) Promotion. Suppose we see alpha[2] := Maybe beta[4]. We want to promote
+ beta[4] to level 2 and unify alpha[2] := Maybe beta'[2]. This is done by
+ checkTyEqRhs.
- rr[sk] ~S# alpha[conc]
+(DE5) Promotion. Suppose we see alpha[2] := F beta[4], where F is a type
+ family. Then we still want to promote beta to beta'[2], and unify. This is
+ unusual: more commonly, we don't promote unification variables under a
+ type family. But here we want to. (This mattered in #25251.)
-we should not default alpha, lest we obtain a poor error message such as
-
- Couldn't match kind `rr' with `LiftedRep'
-
-We would rather preserve the original syntactic equality to be
-reported to the user, especially as the concrete metavariable alpha
-might store an informative origin for the user.
+ Hence the Bool flag on LC_Promote, and its use in `tef_unifying` in
+ `defaultEquality`.
Note [Must simplify after defaulting]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -2102,7 +2102,7 @@ checkTouchableTyVarEq
-- 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
+ | 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)) }
@@ -2135,12 +2135,13 @@ checkTouchableTyVarEq ev lhs_tv 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
+ , 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
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -25,7 +25,7 @@ module GHC.Tc.Utils.Unify (
-- Various unifications
unifyType, unifyKind, unifyInvisibleType, unifyExpectedType,
unifyExprType, unifyTypeAndEmit, promoteTcType,
- swapOverTyVars, touchabilityAndShapeTest, lhsPriority,
+ swapOverTyVars, touchabilityAndShapeTest, checkTopShape, lhsPriority,
UnifyEnv(..), updUEnvLoc, setUEnvRole,
uType,
@@ -3134,6 +3134,9 @@ data LevelCheck
| LC_Promote -- Do a level check between the LHS tyvar and the occurrence tyvar
-- If the level check fails, and the occurrence is a unification
-- variable, promote it
+ Bool -- False <=> don't promote under type families (the common case)
+ -- True <=> promote even under type families
+ -- see Note [Defaulting equalities] in GHC.Tc.Solver
instance Outputable (TyEqFlags a) where
ppr (TEF { .. }) = text "TEF" <> braces (
@@ -3145,7 +3148,7 @@ instance Outputable (TyEqFlags a) where
instance Outputable (TyEqFamApp a) where
ppr TEFA_Fail = text "TEFA_Fail"
- ppr TEFA_Recurse = text "TEFA_Fail"
+ ppr TEFA_Recurse = text "TEFA_Recurse"
ppr (TEFA_Break {}) = text "TEFA_Break"
instance Outputable AreUnifying where
@@ -3154,9 +3157,9 @@ instance Outputable AreUnifying where
braces (ppr mi <> comma <+> ppr lvl <> comma <+> ppr lc)
instance Outputable LevelCheck where
- ppr LC_None = text "LC_None"
- ppr LC_Check = text "LC_Check"
- ppr LC_Promote = text "LC_Promote"
+ ppr LC_None = text "LC_None"
+ ppr LC_Check = text "LC_Check"
+ ppr (LC_Promote b) = text "LC_Promote" <> ppWhen b (text "(deep)")
famAppArgFlags :: TyEqFlags a -> TyEqFlags a
-- Adjust the flags when going undter a type family
@@ -3170,15 +3173,18 @@ famAppArgFlags flags@(TEF { tef_unifying = unifying })
, tef_occurs = cteSolubleOccurs }
-- tef_occurs: under a type family, an occurs check is not definitely-insoluble
where
- zap_promotion (Unifying info lvl LC_Promote) = Unifying info lvl LC_Check
- zap_promotion unifying = unifying
+ zap_promotion (Unifying info lvl (LC_Promote deeply))
+ | 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)
-checkTyEqRhs :: forall a. TyEqFlags a -> TcType -> TcM (PuResult a Reduction)
+checkTyEqRhs :: forall a. TyEqFlags a
+ -> TcType -- Already zonked
+ -> TcM (PuResult a Reduction)
checkTyEqRhs flags ty
= case ty of
LitTy {} -> okCheckRefl ty
@@ -3229,7 +3235,7 @@ checkCo (TEF { tef_lhs = TyVarLHS lhs_tv
= failCheckWith (cteProblem cteCoercionHole)
-- Occurs check (can promote)
- | Unifying _ lhs_tv_lvl LC_Promote <- unifying
+ | Unifying _ lhs_tv_lvl (LC_Promote {}) <- unifying
= do { reason <- checkPromoteFreeVars occ_prob lhs_tv lhs_tv_lvl (tyCoVarsOfCo co)
; if cterHasNoProblem reason
then return (pure co)
@@ -3404,8 +3410,9 @@ checkFamApp flags@(TEF { tef_unifying = unifying, tef_occurs = occ_prob
= case fam_app_flag of
TEFA_Fail -> failCheckWith (cteProblem cteTypeFamily)
+ -- Occurs check: F ty ~ ...(F ty)...
_ | TyFamLHS lhs_tc lhs_tys <- lhs
- , tcEqTyConApps lhs_tc lhs_tys tc tys -- F ty ~ ...(F ty)...
+ , tcEqTyConApps lhs_tc lhs_tys tc tys
-> case fam_app_flag of
TEFA_Recurse -> failCheckWith (cteProblem occ_prob)
TEFA_Break breaker -> breaker fam_app
@@ -3421,7 +3428,11 @@ checkFamApp flags@(TEF { tef_unifying = unifying, tef_occurs = occ_prob
; traceTc "under" (ppr tc $$ pprPur tys_res $$ ppr flags)
; return (mkTyConAppRedn Nominal tc <$> tys_res) }
- TEFA_Break breaker -- Recurse; and break if there is a problem
+ -- For TEFA_Break, try recursion; and break if there is a problem
+ -- e.g. alpha[2] ~ Maybe (F beta[2]) No problem: just unify
+ -- 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
; case tys_res of
PuOK cts redns -> return (PuOK cts (mkTyConAppRedn Nominal tc redns))
@@ -3458,7 +3469,7 @@ checkTyVar (TEF { tef_lhs = lhs, tef_unifying = unifying, tef_occurs = occ_prob
Nothing -> check_unif info lvl prom lhs_tv }
---------------------
- -- We are in the Unifying branch of AreUnifing
+ -- We are in the Unifying branch of AreUnifying; and occ_tv is unfilled
check_unif :: MetaInfo -> TcLevel -> LevelCheck
-> TcTyVar -> TcM (PuResult a Reduction)
check_unif lhs_tv_info lhs_tv_lvl prom lhs_tv
@@ -3472,7 +3483,7 @@ checkTyVar (TEF { tef_lhs = lhs, tef_unifying = unifying, tef_occurs = occ_prob
= case prom of
LC_None -> pprPanic "check_unif" (ppr lhs_tv $$ ppr occ_tv)
LC_Check -> failCheckWith (cteProblem cteSkolemEscape)
- LC_Promote
+ LC_Promote {}
| isSkolemTyVar occ_tv -> failCheckWith (cteProblem cteSkolemEscape)
| otherwise -> promote lhs_tv lhs_tv_info lhs_tv_lvl
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6863503cf3240f78549436819f20f9e1adc578d3
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6863503cf3240f78549436819f20f9e1adc578d3
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20240925/7f493862/attachment-0001.html>
More information about the ghc-commits
mailing list