[Git][ghc/ghc][wip/T22194] 2 commits: Wibbles
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Mon Mar 13 16:26:33 UTC 2023
Simon Peyton Jones pushed to branch wip/T22194 at Glasgow Haskell Compiler / GHC
Commits:
cf015be3 by Simon Peyton Jones at 2023-03-13T11:00:31+00:00
Wibbles
- - - - -
32f9a72a by Simon Peyton Jones at 2023-03-13T16:27:40+00:00
Wibbles
- - - - -
3 changed files:
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Utils/Unify.hs
Changes:
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -1539,15 +1539,17 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
then finish_with_swapping
else finish_without_swapping }
- -- See Note [Always put TyVarLHS on the left]
| TyVarLHS {} <- lhs1
, TyFamLHS {} <- lhs2
- = finish_without_swapping
+ = if put_tyvar_on_lhs
+ then finish_without_swapping
+ else finish_with_swapping
- -- See Note [Always put TyVarLHS on the left]
| TyFamLHS {} <- lhs1
, TyVarLHS {} <- lhs2
- = finish_with_swapping
+ = if put_tyvar_on_lhs
+ then finish_with_swapping
+ else finish_without_swapping
| TyFamLHS fun_tc1 fun_args1 <- lhs1
, TyFamLHS fun_tc2 fun_args2 <- lhs2
@@ -1629,10 +1631,15 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
(canEqLHSType lhs1) (canEqLHSType lhs2) mco
; canEqCanLHSFinish new_ev eq_rel IsSwapped lhs2 (ps_xi1 `mkCastTyMCo` sym_mco) }
-{- Note [Always put TyVarLHS on the left]
+ put_tyvar_on_lhs = isWanted ev && eq_rel == NomEq
+ -- See Note [Orienting TyVarLHS/TyFamLHS]
+ -- Same conditions as for canEqCanLHSFinish_try_unification
+ -- which we are setting ourselves up for here
+
+{- Note [Orienting TyVarLHS/TyFamLHS]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-What if one side is a tyvar and the other is a type family
-application, (a ~ F tys) ? Which to put on the left? Answer:
+What if one side is a TyVarLHS and the other is a TyFamLHS, (a ~ F tys)?
+Which to put on the left? Answer:
* Put the tyvar on the left, (a ~ F tys) as this may be our only shot to unify.
* But if we fail to unify and end up in cantMakeCanonical,
then flip back to (F tys ~ a) because it's generally better
@@ -1836,6 +1843,9 @@ Wrinkles:
and unifying alpha effectively promotes this wanted to a given. Doing so
means we lose track of the rewriter set associated with the wanted.
+ In short: we must not have a co_hole in a Given, and unification
+ effectively makes a Given
+
On the other hand, w is perfectly suitable for rewriting, because of the
way we carefully track rewriter sets.
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -166,6 +166,7 @@ import GHC.Types.Name.Reader
import GHC.Types.Var
import GHC.Types.Var.Set
import GHC.Types.Unique.Supply
+import GHC.Types.Unique.Set (nonDetEltsUniqSet)
import GHC.Unit.Module ( HasModule, getModule, extractModule )
import qualified GHC.Rename.Env as TcM
@@ -189,7 +190,6 @@ import Data.Foldable
import qualified Data.Semigroup as S
#if defined(DEBUG)
-import GHC.Types.Unique.Set (nonDetEltsUniqSet)
import GHC.Data.Graph.Directed
#endif
@@ -2074,23 +2074,23 @@ checkTouchableTyVarEq
-- with extra wanteds 'cts'
-- If it returns (PuFail reason) we can't unify, and the reason explains why.
checkTouchableTyVarEq ev lhs_tv rhs
- | MetaTv { mtv_info = lhs_tv_info, mtv_tclvl = lhs_tv_lvl } <- tcTyVarDetails lhs_tv
= do { traceTcS "checkTouchableTyVarEq" (ppr lhs_tv $$ ppr rhs)
- ; check_result <- wrapTcS (check_rhs lhs_tv_info lhs_tv_lvl)
+ ; check_result <- wrapTcS check_rhs
; traceTcS "checkTouchableTyVarEq 2" (ppr lhs_tv $$ ppr check_result)
; case check_result of
PuFail reason -> return (PuFail reason)
PuOK redn cts -> do { emitWork (bagToList cts)
; return (pure redn) } }
-
- | otherwise = pprPanic "checkTouchableTyVarEq" (ppr lhs_tv)
where
ghci_tv = isRuntimeUnkSkol lhs_tv
-
- check_rhs lhs_tv_info lhs_tv_lvl = case coreFullView rhs of
- TyConApp tc tys | isTypeFamilyTyCon tc
- , not (isConcreteTyVar lhs_tv)
- -> -- Special case for lhs ~ F tys
+ (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)
+
+ check_rhs = case splitTyConApp_maybe rhs of
+ Just (tc, tys) | isTypeFamilyTyCon tc
+ , not (isConcreteTyVar lhs_tv)
+ -> -- Special case for alpha ~ F tys
-- We don't want to flatten that (F tys)
do { tys_res <- mapCheck (simple_check lhs_tv_lvl) tys
; return (mkTyConAppRedn Nominal tc <$> tys_res) }
@@ -2267,31 +2267,47 @@ checkTypeEq ev eq_rel lhs rhs
where
ghci_tv = False
- check_given :: TcType -> TcM (PuResult (TcTyVar,TcType) Reduction)
- check_given = case lhs of
- TyFamLHS {} -> checkTyEqRhs ghci_tv refl_tv check_given_fam_app refl_co
- TyVarLHS tv -> checkTyEqRhs ghci_tv (check_tv tv) check_given_fam_app (check_co tv)
-
+ ---------------------- Wanted ------------------
check_wanted :: TcType -> TcM (PuResult Ct Reduction)
check_wanted = case lhs of
- TyFamLHS {} -> checkTyEqRhs ghci_tv refl_tv check_wanted_fam_app refl_co
- TyVarLHS tv -> checkTyEqRhs ghci_tv (check_tv tv) check_wanted_fam_app (check_co tv)
+ TyFamLHS tc tys -> checkTyEqRhs ghci_tv refl_tv (cfa_wanted_fam tc tys) refl_co
+ TyVarLHS tv -> checkTyEqRhs ghci_tv (check_tv tv) cfa_wanted_tv (check_co tv)
+
+ -- Family-application (G tys) in [W] F lhs_tys ~ (...(G tys)...)
+ cfa_wanted_fam :: TyCon -> [TcType]
+ -> TcType -> TyCon -> [TcType]
+ -> TcM (PuResult Ct Reduction)
+ cfa_wanted_fam lhs_tc lhs_tys fam_app tc tys
+ | tcEqTyConApps lhs_tc lhs_tys tc tys
+ = failCheckWith (occursProblem eq_rel)
+ | otherwise
+ = recurseFamApp check_wanted fam_app tc tys
- check_wanted_fam_app _ tc tys -- Just recurse; if there is an
- -- occurs check etc, just fail
- = do { tys_res <- mapCheck check_wanted tys
- ; return (mkTyConAppRedn Nominal tc <$> tys_res) }
+ cfa_wanted_tv fam_app tc tys = recurseFamApp check_wanted fam_app tc tys
- check_given_fam_app fam_app tc tys
+ ---------------------- Given ------------------
+ check_given :: TcType -> TcM (PuResult (TcTyVar,TcType) Reduction)
+ check_given = case lhs of
+ TyFamLHS tc tys -> checkTyEqRhs ghci_tv refl_tv (cfa_given_fam tc tys) refl_co
+ TyVarLHS tv -> checkTyEqRhs ghci_tv (check_tv tv) cfa_given_tv (check_co tv)
+
+ cfa_given_fam lhs_tc lhs_tys fam_app tc tys
+ | tcEqTyConApps lhs_tc lhs_tys tc tys
+ = break_cycle fam_app
+ | otherwise
+ = recurseFamApp check_given fam_app tc tys
+
+ cfa_given_tv fam_app tc tys
= -- Try just checking the arguments
do { tys_res <- mapCheck check_given tys
; case tys_res of {
PuOK redns cts -> return (PuOK (mkTyConAppRedn Nominal tc redns) cts) ;
- PuFail {} ->
+ PuFail {} -> break_cycle fam_app } }
- do { new_tv <- TcM.newCycleBreakerTyVar (typeKind fam_app)
+ break_cycle fam_app
+ = do { new_tv <- TcM.newCycleBreakerTyVar (typeKind fam_app)
; return (PuOK (mkReflRedn Nominal (mkTyVarTy new_tv))
- (unitBag (new_tv, fam_app))) } }}
+ (unitBag (new_tv, fam_app))) }
-- Why reflexive? See Detail (4) of the Note
refl_tv tv = okCheckRefl (mkTyVarTy tv)
@@ -2318,6 +2334,13 @@ checkTypeEq ev eq_rel lhs rhs
cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin
+recurseFamApp :: (TcType -> TcM (PuResult a Reduction))
+ -> TcType -> TyCon -> [TcType] -> TcM (PuResult a Reduction)
+-- Just recurse; if there is an occurs check etc, just fail
+recurseFamApp check _ tc tys
+ = do { tys_res <- mapCheck check tys
+ ; return (mkTyConAppRedn Nominal tc <$> tys_res) }
+
-------------------------
checkFreeVars :: TcTyVar -> TcLevel -> TyCoVarSet -> TcM CheckTyEqResult
-- Check this set of TyCoVars for
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -2664,9 +2664,8 @@ occursCheckTv lhs_tv occ_tv
uTypeCheckTouchableTyVarEq :: TcTyVar -> TcType -> TcM (PuResult () ())
uTypeCheckTouchableTyVarEq lhs_tv rhs
- | MetaTv { mtv_info = tv_info } <- tcTyVarDetails lhs_tv
= do { check_result <- checkTyEqRhs False
- (simple_check_tv (isConcreteInfo tv_info))
+ simple_check_tv
dont_flatten
(simpleCheckCo lhs_tv True)
rhs
@@ -2676,15 +2675,17 @@ uTypeCheckTouchableTyVarEq lhs_tv rhs
PuOK redn _ -> assertPpr (isReflCo (reductionCoercion redn))
(ppr lhs_tv $$ ppr rhs $$ ppr redn) $
return (PuOK () emptyBag) }
-
- -- Only called on meta-tyvars
- | otherwise = pprPanic "uTypeCHeckTouchableTyVarEq" (ppr lhs_tv)
where
+ lhs_tv_info = case tcTyVarDetails lhs_tv of
+ MetaTv { mtv_info = tv_info } -> tv_info
+ _ -> pprPanic "uTypeCheckTouchableTyVarEq" (ppr lhs_tv)
+
dont_flatten :: TcType -> TyCon -> [TcType] -> TcM (PuResult () Reduction)
dont_flatten _ _ _ = failCheckWith (cteProblem cteTypeFamily)
-- See Note [Prevent unification with type families]
- simple_check_tv lhs_tv_is_concrete occ_tv
+ lhs_tv_is_concrete = isConcreteInfo lhs_tv_info
+ simple_check_tv occ_tv
| occursCheckTv lhs_tv occ_tv
= failCheckWith insolubleOccursProblem
| lhs_tv_is_concrete, not (isConcreteTyVar occ_tv)
@@ -2710,8 +2711,11 @@ simpleCheckCo lhs_tv unifying co
checkTyEqRhs :: forall a.
Bool -- RuntimeUnk tyvar on the LHS; accept foralls
-> (TcTyVar -> TcM (PuResult a Reduction))
+ -- What to do for tyvars
-> (TcType -> TyCon -> [TcType] -> TcM (PuResult a Reduction))
+ -- What to do for family applications; guaranteed precisely saturated
-> (TcCoercion -> TcM (PuResult a TcCoercion))
+ -- What to do for coercions
-> TcType
-> TcM (PuResult a Reduction)
checkTyEqRhs ghci_tv check_tv flatten_fam_app check_co rhs
@@ -2750,16 +2754,27 @@ checkTyEqRhs ghci_tv check_tv flatten_fam_app check_co rhs
go_tc :: TcType -> TyCon -> [TcType] -> TcM (PuResult a Reduction)
go_tc ty tc tys
| isTypeFamilyTyCon tc
- = flatten_fam_app ty tc tys
-
- | not (isFamFreeTyCon tc) -- e.g. S a where type S a = F [a]
+ , let arity = tyConArity tc
+ = if tys `lengthIs` arity
+ then flatten_fam_app ty tc tys -- Common case
+ else do { let (fun_args, extra_args) = splitAt (tyConArity tc) tys
+ fun_app = mkTyConApp tc fun_args
+ ; fun_res <- flatten_fam_app fun_app tc fun_args
+ ; extra_res <- mapCheck go extra_args
+ ; return (mkAppRedns <$> fun_res <*> extra_res) }
+
+ | not (isFamFreeTyCon tc) || isForgetfulSynTyCon tc
+ -- e.g. S a where type S a = F [a]
+ -- or type S a = Int
+ -- ToDo: explain why
, Just ty' <- coreView ty -- Only synonyms and type families reply
= go ty' -- False to isFamFreeTyCon
- | otherwise
+ | otherwise -- Recurse on arguments
= do { tys_res <- mapCheck go tys
- ; if | PuFail {} <- tys_res, Just ty' <- coreView ty
- -> go ty' -- Expand synonyms on failure
+ ; if | PuFail {} <- tys_res
+ , Just ty' <- coreView ty -- Expand synonyms on failure
+ -> go ty' -- e.g a ~ P a where type P a = Int
| not (isTauTyCon tc || ghci_tv)
-> failCheckWith impredicativeProblem
| otherwise
@@ -2778,20 +2793,20 @@ touchabilityTest given_eq_lvl tv rhs
= False
-------------------------
--- | checkTopShape checks (TYVAR-TV), (COERCION-HOLE) and (CONCRETE) of
+-- | checkTopShape checks (TYVAR-TV)
-- Note [Unification preconditions]; returns True if these conditions
-- are satisfied. But see the Note for other preconditions, too.
checkTopShape :: MetaInfo -> TcType -> Bool
checkTopShape info xi
= case info of
- CycleBreakerTv -> False
TyVarTv ->
- case getTyVar_maybe xi of
+ case getTyVar_maybe xi of -- Looks through type synonyms
Nothing -> False
Just tv -> case tcTyVarDetails tv of -- (TYVAR-TV) wrinkle
SkolemTv {} -> True
RuntimeUnk -> True
MetaTv { mtv_info = TyVarTv } -> True
_ -> False
+ CycleBreakerTv -> False -- We never unify these
_ -> True
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/26ce990bef18ba7a9c8af12628085d1fb890e856...32f9a72a8a7efd62122f4f185e4cf76126778eb9
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/26ce990bef18ba7a9c8af12628085d1fb890e856...32f9a72a8a7efd62122f4f185e4cf76126778eb9
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/20230313/c726cf66/attachment-0001.html>
More information about the ghc-commits
mailing list