[Git][ghc/ghc][wip/T22194-flags] More wibbles, prompted by talking with Richard
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Sat Mar 18 00:02:21 UTC 2023
Simon Peyton Jones pushed to branch wip/T22194-flags at Glasgow Haskell Compiler / GHC
Commits:
6d0330f2 by Simon Peyton Jones at 2023-03-18T00:03:40+00:00
More wibbles, prompted by talking with Richard
- - - - -
6 changed files:
- compiler/GHC/Core/TyCon.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- compiler/GHC/Tc/Utils/Unify.hs
Changes:
=====================================
compiler/GHC/Core/TyCon.hs
=====================================
@@ -2002,6 +2002,10 @@ isInjectiveTyCon (TyCon { tyConDetails = details }) role
-- (where r is the role passed in):
-- If (T tys ~r t), then (t's head ~r T).
-- See also Note [Decomposing TyConApp equalities] in "GHC.Tc.Solver.Canonical"
+--
+-- NB: at Nominal role, isGenerativeTyCon is simple:
+-- isGenerativeTyCon tc Nominal
+-- = not (isTypeFamilyTyCon tc || isSynonymTyCon tc)
isGenerativeTyCon :: TyCon -> Role -> Bool
isGenerativeTyCon tc@(TyCon { tyConDetails = details }) role
= go role details
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -1534,7 +1534,8 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
| TyVarLHS tv1 <- lhs1
, TyVarLHS tv2 <- lhs2
- = do { traceTcS "canEqLHS2 swapOver" (ppr tv1 $$ ppr tv2 $$ ppr swapped)
+ = -- See Note [TyVar/TyVar orientation] in GHC.Tc.Utils.Unify
+ do { traceTcS "canEqLHS2 swapOver" (ppr tv1 $$ ppr tv2 $$ ppr swapped)
; if swapOverTyVars (isGiven ev) tv1 tv2
then finish_with_swapping
else finish_without_swapping }
@@ -1600,36 +1601,24 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
tvs2 = tyCoVarsOfTypes fun_args2
swap_for_rewriting = anyVarSet (isTouchableMetaTyVar tclvl) tvs2 &&
- -- swap 'em: Note [Put touchable variables on the left]
+ -- See Note [Put touchable variables on the left]
not (anyVarSet (isTouchableMetaTyVar tclvl) tvs1)
- -- this check is just to avoid unfruitful swapping
-
- swap_for_occurs = False
-
-{- ToDo: not sure about this
- -- If we have F a ~ F (F a), we want to swap.
- swap_for_occurs
- | cterHasNoProblem $ checkTyFamEq fun_tc2 fun_args2
- (mkTyConApp fun_tc1 fun_args1)
- , cterHasOccursCheck $ checkTyFamEq fun_tc1 fun_args1
- (mkTyConApp fun_tc2 fun_args2)
- = True
- | otherwise
- = False
--}
+ -- This second check is just to avoid unfruitful swapping
- ; if swap_for_rewriting || swap_for_occurs
+ ; if swap_for_rewriting
then finish_with_swapping
else finish_without_swapping }
where
sym_mco = mkSymMCo mco
- finish_without_swapping
- = canEqCanLHSFinish ev eq_rel swapped lhs1 (ps_xi2 `mkCastTyMCo` mco)
- finish_with_swapping
- = do { new_ev <- rewriteCastedEquality ev eq_rel swapped
- (canEqLHSType lhs1) (canEqLHSType lhs2) mco
- ; canEqCanLHSFinish new_ev eq_rel IsSwapped lhs2 (ps_xi1 `mkCastTyMCo` sym_mco) }
+ finish_without_swapping = canEqCanLHSFinish ev eq_rel swapped
+ lhs1 (ps_xi2 `mkCastTyMCo` mco)
+ finish_with_swapping = canEqCanLHSFinish ev eq_rel (flipSwap swapped)
+ lhs2 (ps_xi1 `mkCastTyMCo` sym_mco)
+
+-- = do { new_ev <- rewriteCastedEquality ev eq_rel swapped
+-- (canEqLHSType lhs1) (canEqLHSType lhs2) mco
+-- ; canEqCanLHSFinish new_ev eq_rel IsSwapped lhs2 (ps_xi1 `mkCastTyMCo` sym_mco) }
put_tyvar_on_lhs = isWanted ev && eq_rel == NomEq
-- See Note [Orienting TyVarLHS/TyFamLHS]
@@ -1713,7 +1702,7 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
= 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 tv can_rhs
+ -> swapAndFinish ev eq_rel swapped (mkTyVarTy tv) can_rhs
-- See Note [Orienting TyVarLHS/TyFamLHS]
| otherwise
@@ -1724,23 +1713,28 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
do { check_result <- checkTouchableTyVarEq ev tv rhs
; case check_result of {
PuFail reason
- | Just can_rhs <- canTyFamEqLHS_maybe rhs
- -> swapAndFinish ev eq_rel swapped tv can_rhs
- -- See Note [Orienting TyVarLHS/TyFamLHS]
+ | Just can_rhs <- canTyFamEqLHS_maybe rhs
+ -> swapAndFinish ev eq_rel swapped (mkTyVarTy tv) can_rhs
+ -- See Note [Orienting TyVarLHS/TyFamLHS]
- -- 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
- | reason `cterHasOnlyProblem` cteSkolemEscape
- -> canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
+ -- 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
+ | reason `cterHasOnlyProblem` cteSkolemEscape
+ -> canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
- | otherwise
- -> tryIrredInstead reason ev eq_rel swapped lhs rhs ;
+ | otherwise
+ -> tryIrredInstead reason ev eq_rel swapped lhs rhs ;
PuOK rhs_redn _ ->
-- Success: we can solve by unification
- do { -- Comment needed!
+ 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
@@ -1787,27 +1781,38 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
-- in case have x ~ (y :: ..x...); this is #12593.
; check_result <- checkTypeEq ev eq_rel lhs rhs
- ; case check_result of {
- PuFail reason -> tryIrredInstead reason ev eq_rel swapped lhs rhs ;
- PuOK rhs_redn _ ->
+ ; let lhs_ty = canEqLHSType lhs
+ ; case check_result of
+ PuFail reason
- do { new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped
- (mkReflRedn Nominal (canEqLHSType lhs)) rhs_redn
+ -- If we had F a ~ G (F a), which gives an occurs check,
+ -- then swap it to G (F a) ~ F a, which does not
+ | TyFamLHS {} <- lhs
+ , Just can_rhs <- canTyFamEqLHS_maybe rhs
+ , reason `cterHasOnlyProblem` cteSolubleOccurs
+ -> swapAndFinish ev eq_rel swapped lhs_ty can_rhs
- ; interactEq (EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel
- , eq_lhs = lhs
- , eq_rhs = reductionReducedType rhs_redn }) }}}
+ | otherwise
+ -> tryIrredInstead reason ev eq_rel swapped lhs rhs
+
+ PuOK rhs_redn _
+ -> do { new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped
+ (mkReflRedn (eqRelRole eq_rel) lhs_ty)
+ rhs_redn
+
+ ; interactEq (EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel
+ , eq_lhs = lhs
+ , eq_rhs = reductionReducedType rhs_redn }) } }
----------------------
swapAndFinish :: CtEvidence -> EqRel -> SwapFlag
- -> TcTyVar -> CanEqLHS -- a ~ F tys
+ -> TcType -> CanEqLHS -- ty ~ F tys
-> TcS (StopOrContinue Ct)
-- We have an equality alpha ~ F tys, that we can't unify e.g because 'tys'
-- mentions alpha, it would not be a canonical constraint as-is.
-- We want to flip it to (F tys ~ a), whereupon it is canonical
-swapAndFinish ev eq_rel swapped lhs_tv can_rhs
- = do { let lhs_ty = mkTyVarTy lhs_tv
- ; new_ev <- rewriteEqEvidence emptyRewriterSet ev (flipSwap swapped)
+swapAndFinish ev eq_rel swapped lhs_ty can_rhs
+ = do { new_ev <- rewriteEqEvidence emptyRewriterSet ev (flipSwap swapped)
(mkReflRedn role (canEqLHSType can_rhs))
(mkReflRedn role lhs_ty)
; interactEq (EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel
@@ -2302,6 +2307,7 @@ Details:
**********************************************************************
-}
+{-
rewriteCastedEquality :: CtEvidence -- :: lhs ~ (rhs |> mco), or (rhs |> mco) ~ lhs
-> EqRel -> SwapFlag
-> TcType -- lhs
@@ -2317,6 +2323,7 @@ rewriteCastedEquality ev eq_rel swapped lhs rhs mco
sym_mco = mkSymMCo mco
role = eqRelRole eq_rel
+-}
rewriteEqEvidence :: RewriterSet -- New rewriters
-- See GHC.Tc.Types.Constraint
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -2100,7 +2100,7 @@ checkTouchableTyVarEq ev lhs_tv rhs
flags | MetaTv { mtv_info = tv_info, mtv_tclvl = tv_lvl } <- tcTyVarDetails lhs_tv
= TEF { tef_foralls = isRuntimeUnkSkol lhs_tv
- , tef_fam_app = mkTEFA_Break ev (break_wanted tv_lvl)
+ , tef_fam_app = mkTEFA_Break ev (break_wanted tv_info tv_lvl)
, tef_unifying = Unifying tv_info tv_lvl LC_Promote
, tef_lhs = TyVarLHS lhs_tv
, tef_occurs = cteInsolubleOccurs }
@@ -2108,8 +2108,22 @@ checkTouchableTyVarEq ev lhs_tv rhs
arg_flags = famAppArgFlags flags
- break_wanted lhs_tv_lvl fam_app -- Occurs check or skolem escape; so flatten
- = do { new_tv_ty <- TcM.newMetaTyVarTyAtLevel lhs_tv_lvl (typeKind fam_app)
+ break_wanted lhs_tv_info lhs_tv_lvl 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 { let tv_info | isConcreteInfo lhs_tv_info = lhs_tv_info
+ | otherwise = TauTv
+ -- 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]
+ ; new_tv_ty <- TcM.newMetaTyVarTyWithInfo lhs_tv_lvl tv_info fam_app_kind
; let pty = mkPrimEqPredRole Nominal fam_app new_tv_ty
; hole <- TcM.newCoercionHole pty
; let new_ev = CtWanted { ctev_pred = pty
@@ -2117,7 +2131,7 @@ checkTouchableTyVarEq ev lhs_tv rhs
, ctev_loc = cb_loc
, ctev_rewriters = ctEvRewriters ev }
; return (PuOK (mkReduction (HoleCo hole) new_tv_ty)
- (singleCt (mkNonCanonical new_ev))) }
+ (singleCt (mkNonCanonical new_ev))) } }
-- See Detail (7) of the Note
cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -279,12 +279,11 @@ An EqCt is a canonical equality constraint. It satisfies these invariants:
See Note [No top-level newtypes on RHS of representational equalities]
in GHC.Tc.Solver.Canonical. (Applies only when constructor of newtype is
in scope.)
- * (TyEq:TV) If rhs (perhaps under a cast) is also CanEqLHS, then it is oriented
- to give best chance of unification happening; eg if rhs is touchable then lhs is too
- Note [TyVar/TyVar orientation] in GHC.Tc.Utils.Unify
+ * (TyEq:U) An EqCt is not immediately unifiable. If we can unify a:=ty, we
+ will not form an EqCt (a ~ ty).
-These invariants ensure that the EqCts in inert_eqs constitute a
-terminating generalised substitution. See Note [inert_eqs: the inert equalities]
+These invariants ensure that the EqCts in inert_eqs constitute a terminating
+generalised substitution. See Note [inert_eqs: the inert equalities]
in GHC.Tc.Solver.InertSet for what these words mean!
-}
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -23,7 +23,8 @@ module GHC.Tc.Utils.TcMType (
newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType]
newOpenFlexiTyVar, newOpenFlexiTyVarTy, newOpenTypeKind,
newOpenBoxedTypeKind,
- newMetaKindVar, newMetaKindVars, newMetaTyVarTyAtLevel,
+ newMetaKindVar, newMetaKindVars,
+ newMetaTyVarTyAtLevel, newMetaTyVarTyWithInfo,
newAnonMetaTyVar, newConcreteTyVar,
cloneMetaTyVar, cloneMetaTyVarWithInfo,
newCycleBreakerTyVar,
@@ -1131,6 +1132,15 @@ newMetaTyVarTyAtLevel tc_lvl kind
; name <- newMetaTyVarName (fsLit "p")
; return (mkTyVarTy (mkTcTyVar name kind details)) }
+newMetaTyVarTyWithInfo :: TcLevel -> MetaInfo -> TcKind -> TcM TcType
+newMetaTyVarTyWithInfo tc_lvl info kind
+ = do { ref <- newMutVar Flexi
+ ; let details = MetaTv { mtv_info = info
+ , mtv_ref = ref
+ , mtv_tclvl = tc_lvl }
+ ; name <- newMetaTyVarName (fsLit "p")
+ ; return (mkTyVarTy (mkTcTyVar name kind details)) }
+
{- *********************************************************************
* *
Finding variables to quantify over
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -36,7 +36,7 @@ module GHC.Tc.Utils.Unify (
checkTyEqRhs,
PuResult(..), failCheckWith, okCheckRefl, mapCheck,
TyEqFlags(..), TyEqFamApp(..), AreUnifying(..), LevelCheck(..), FamAppBreaker,
- famAppArgFlags, occursCheckTv, simpleUnifyCheck
+ famAppArgFlags, occursCheckTv, simpleUnifyCheck, checkPromoteFreeVars
) where
import GHC.Prelude
@@ -2593,6 +2593,7 @@ simpleUnifyCheck fam_ok lhs_tv rhs
go (LitTy {}) = True
go_co co = not (lhs_tv `elemVarSet` tyCoVarsOfCo co)
+ && not (hasCoercionHoleCo co)
{- *********************************************************************
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6d0330f20b6b0688e6d4a961fb7a39ce62d61207
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6d0330f20b6b0688e6d4a961fb7a39ce62d61207
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/20230317/eb65d05c/attachment-0001.html>
More information about the ghc-commits
mailing list