[Git][ghc/ghc][wip/T24676] Wibbles
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Wed May 29 10:33:07 UTC 2024
Simon Peyton Jones pushed to branch wip/T24676 at Glasgow Haskell Compiler / GHC
Commits:
1faefc72 by Simon Peyton Jones at 2024-05-29T11:32:48+01:00
Wibbles
- - - - -
2 changed files:
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Gen/Head.hs
Changes:
=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -43,7 +43,8 @@ import GHC.Core.DataCon ( dataConConcreteTyVars, isNewDataCon, dataConTyCon )
import GHC.Core.TyCon
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Ppr
-import GHC.Core.TyCo.Subst (substTyWithInScope)
+import GHC.Core.TyCo.FVs ( shallowTyCoVarsOfType )
+import GHC.Core.TyCo.Subst ( substTyWithInScope )
import GHC.Core.Type
import GHC.Core.Coercion
@@ -58,6 +59,8 @@ import GHC.Types.Name.Env
import GHC.Types.Name.Reader
import GHC.Types.SrcLoc
import GHC.Types.Var.Env ( emptyTidyEnv, mkInScopeSet )
+import GHC.Types.Var.Set
+import GHC.Types.Basic ( TypeOrKind(..) )
import GHC.Data.Maybe
@@ -346,41 +349,39 @@ tcApp rn_expr exp_res_ty
<- setQLInstLevel do_ql $
tcInstFun do_ql True fun_ctxt tc_fun fun_sigma rn_args
- -- Monomorphise any leftover instantiation variables
- ; res_wrap <- case do_ql of
- NoQL -> case exp_res_ty of
- Check res_ty ->
- unifyResTy rn_expr fun_ctxt tc_fun inst_args app_res_rho res_ty
- Infer inf_res ->
- do { co <- fillInferResult app_res_rho inf_res
- ; return (mkWpCastN co) }
-
- DoQL -> case exp_res_ty of
- Check res_ty ->
- do { qlUnify app_res_rho res_ty
- ; monomorphiseQLInstVars inst_args app_res_rho
- ; unifyResTy rn_expr fun_ctxt tc_fun inst_args app_res_rho res_ty }
- Infer inf_res ->
- do { monomorphiseQLInstVars inst_args app_res_rho
- ; co <- fillInferResult app_res_rho inf_res
- ; return (mkWpCastN co) }
+ ; app_res_rho <- case do_ql of
+ NoQL -> return app_res_rho
+ DoQL -> do { -- QL-unify with result type
+ case exp_res_ty of
+ Check res_ty -> qlUnify app_res_rho res_ty
+ Infer {} -> return ()
+ -- Monomorphise any leftover instantiation variables
+ ; monomorphiseQLInstVars inst_args app_res_rho
+
+ -- Zonk the return type to expose any foralls
+ ; liftZonkM $ zonkTcType app_res_rho }
-- Typecheck the arguments
- ; tc_app <- finishApp fun_ctxt tc_fun inst_args app_res_rho
- ; return (mkHsWrap res_wrap tc_app) }
+ ; ds_flag <- getDeepSubsumptionFlag
+ ; finishApp ds_flag rn_expr fun_ctxt tc_fun inst_args app_res_rho exp_res_ty }
setQLInstLevel :: QLFlag -> TcM a -> TcM a
setQLInstLevel DoQL thing_inside = setTcLevel QLInstVar thing_inside
setQLInstLevel NoQL thing_inside = thing_inside
-finishApp :: AppCtxt
+finishApp :: DeepSubsumptionFlag -> HsExpr GhcRn -> AppCtxt
-> HsExpr GhcTc -> [HsExprArg 'TcpInst]
- -> TcRhoType
+ -> TcRhoType -- Inferred type of the application;
+ -- zonked, but maybe not deeply instantiated
+ -> ExpRhoType -- Expected type; this is deeply skolemised
-> TcM (HsExpr GhcTc)
-- At this point there are no more instantiation variables
-finishApp fun_ctxt tc_fun inst_args app_res_rho
- = do { -- Typecheck the value arguments
- ; tc_args <- tcValArgs inst_args
+finishApp ds_flag rn_expr fun_ctxt tc_fun inst_args app_res_rho exp_res_ty
+ = do { res_wrap <- checkResTy ds_flag rn_expr fun_ctxt tc_fun inst_args
+ app_res_rho exp_res_ty
+
+ -- Typecheck the value arguments
+ ; tc_args <- tcValArgs inst_args
-- Horrible newtype check
; rejectRepPolyNewtypes tc_fun app_res_rho
@@ -398,14 +399,22 @@ finishApp fun_ctxt tc_fun inst_args app_res_rho
, text "tc_args:" <+> ppr tc_args
, text "tc_expr:" <+> ppr tc_expr ]) }
- ; return tc_expr }
+ ; return (mkHsWrap res_wrap tc_expr) }
-unifyResTy :: HsExpr GhcRn -> AppCtxt -> HsExpr GhcTc
- -> [HsExprArg p]
- -> TcType -> TcRhoType
+checkResTy :: DeepSubsumptionFlag -> HsExpr GhcRn -> AppCtxt
+ -> HsExpr GhcTc -> [HsExprArg p]
+ -> TcRhoType -- Inferred type of the application; zonked to
+ -- expose foralls, but maybe not deeply instantiated
+ -> ExpRhoType -- Expected type; this is deeply skolemised
-> TcM HsWrapper
-unifyResTy rn_expr fun_ctxt tc_fun inst_args app_res_rho res_ty
+-- Connect up the inferred type of the application with the expected type
+-- This is usually just a unification, but with deep subsumption there is more to do
+checkResTy _ _ _ _ _ app_res_rho (Infer inf_res)
+ = do { co <- fillInferResult app_res_rho inf_res
+ ; return (mkWpCastN co) }
+
+checkResTy ds_flag rn_expr fun_ctxt tc_fun inst_args app_res_rho (Check res_ty)
-- Unify with expected type from the context
-- See Note [Unify with expected type before typechecking arguments]
--
@@ -416,7 +425,6 @@ unifyResTy rn_expr fun_ctxt tc_fun inst_args app_res_rho res_ty
vcat [ text "tc_fun:" <+> ppr tc_fun
, text "app_res_rho:" <+> ppr app_res_rho
, text "res_ty:" <+> ppr res_ty ]
- ; ds_flag <- getDeepSubsumptionFlag
; case ds_flag of
Shallow -> -- No deep subsumption
-- app_res_rho and res_ty are both rho-types,
@@ -430,11 +438,11 @@ unifyResTy rn_expr fun_ctxt tc_fun inst_args app_res_rho res_ty
-- Even though both app_res_rho and res_ty are rho-types,
-- they may have nested polymorphism, so if deep subsumption
-- is on we must call tcSubType.
- -- No need to zonk app_res_rho first; although QL may have instantiated some
- -- delta variables to polytypes, tcSubType can cope with that
- do { wrap <- tcSubTypeDS rn_expr app_res_rho res_ty
- ; traceTc "unifyResTy 2 }" (ppr wrap)
- ; return wrap } }
+ -- Zonk app_res_rho first, because QL may have instantiated some
+ -- delta variables to polytypes, and tcSubType doesn't expect that
+ do { wrap <- tcSubTypeDS rn_expr app_res_rho res_ty
+ ; traceTc "unifyResTy 2 }" (ppr app_res_rho $$ ppr res_ty)
+ ; return wrap } }
where
-- perhaps_add_res_ty_ctxt: Inside an expansion, the addFunResCtxt stuff is
-- more confusing than helpful because the function at the head isn't in
@@ -484,14 +492,14 @@ tcValArg (ETypeArg l hs_ty ty) = return (ETypeArg l hs_ty ty)
tcValArg (EValArg { ea_ctxt = ctxt
, ea_arg = larg@(L arg_loc arg)
- , ea_arg_ty = (do_zonk, Scaled mult arg_ty) })
+ , ea_arg_ty = (do_zonk, Scaled mult exp_arg_ty) })
= addArgCtxt ctxt larg $
do { traceTc "tcValArg" $
vcat [ ppr ctxt
- , text "arg type:" <+> ppr arg_ty
+ , text "arg type:" <+> ppr exp_arg_ty
, text "arg:" <+> ppr arg ]
- -- Crucial step: expose QL results before checking arg_ty
+ -- Crucial step: expose QL results before checking exp_arg_ty
-- So far as the paper is concerned, this step applies
-- the poly-substitution Theta, learned by QL, so that we
-- "see" the polymorphism in that argument type. E.g.
@@ -500,13 +508,13 @@ tcValArg (EValArg { ea_ctxt = ctxt
-- Then Theta = [p :-> forall a. a->a], and we want
-- to check 'e' with expected type (forall a. a->a)
-- See Note [Instantiation variables are short lived]
- ; arg_ty <- case do_zonk of
- DoQL -> liftZonkM $ zonkTcType arg_ty
- NoQL -> return arg_ty
+ ; exp_arg_ty <- case do_zonk of
+ DoQL -> liftZonkM $ zonkTcType exp_arg_ty
+ NoQL -> return exp_arg_ty
-- Now check the argument
; arg' <- tcScalingUsage mult $
- tcPolyExpr arg (mkCheckExpType arg_ty)
+ tcPolyExpr arg (mkCheckExpType exp_arg_ty)
; return (EValArg { ea_ctxt = ctxt
, ea_arg = L arg_loc arg'
@@ -514,43 +522,46 @@ tcValArg (EValArg { ea_ctxt = ctxt
tcValArg (EValArgQL { eaql_status = ql_status
, eaql_ctxt = ctxt
- , eaql_arg_ty = Scaled mult arg_ty
+ , eaql_arg_ty = Scaled mult exp_arg_ty
, eaql_larg = larg@(L arg_loc rn_expr)
, eaql_head = rn_head
, eaql_tc_fun = tc_fun
, eaql_args = inst_args
- , eaql_res_rho = res_rho })
+ , eaql_res_rho = app_res_rho })
= addArgCtxt ctxt larg $
tcScalingUsage mult $
case ql_status of
- QLUnified res_wrap
- -> do { tc_app <- finishApp ctxt tc_fun inst_args res_rho
+ QLUnified -- We have decided to unify (no generalisation or deep subsumption)
+ -> -- So pass Shallow to finishAPp
+ do { tc_app <- finishApp Shallow rn_expr ctxt tc_fun inst_args app_res_rho
+ (mkCheckExpType exp_arg_ty)
; return (EValArg { ea_ctxt = ctxt
- , ea_arg = L arg_loc (mkHsWrap res_wrap tc_app)
+ , ea_arg = L arg_loc tc_app
, ea_arg_ty = noExtField }) }
QLIndependent wc
- -> do { -- Expose QL results, as in the EValArg case
- ; arg_ty <- liftZonkM $ zonkTcType arg_ty
+ -> do { -- Expose QL results to tcSkolemise, as in EValArg case
+ exp_arg_ty <- liftZonkM $ zonkTcType exp_arg_ty
; traceTc "tcEValArgQL {" (vcat [ ppr rn_head
, text "status:" <+> ppr ql_status
- , text "res_rho:" <+> ppr res_rho
- , text "arg_ty:" <+> ppr arg_ty
+ , text "app_res_rho:" <+> ppr app_res_rho
+ , text "exp_arg_ty:" <+> ppr exp_arg_ty
, text "args:" <+> ppr inst_args ])
; ds_flag <- getDeepSubsumptionFlag
; (wrap, arg')
- <- tcSkolemise ds_flag GenSigCtxt arg_ty $ \ arg_rho ->
+ <- tcSkolemise ds_flag GenSigCtxt exp_arg_ty $ \ exp_arg_rho ->
do { emitConstraints wc
- ; res_wrap <- unifyResTy rn_expr ctxt tc_fun inst_args res_rho arg_rho
- ; monomorphiseQLInstVars inst_args res_rho
- ; tc_app <- finishApp ctxt tc_fun inst_args res_rho
- ; return (mkHsWrap res_wrap tc_app) }
+ ; qlUnify app_res_rho exp_arg_rho
+ ; monomorphiseQLInstVars inst_args app_res_rho
+ ; app_res_rho <- liftZonkM $ zonkTcType app_res_rho
+ ; finishApp ds_flag rn_expr ctxt tc_fun inst_args app_res_rho
+ (mkCheckExpType exp_arg_rho) }
; traceTc "tcEValArgQL }" $
vcat [ text "rn_head:" <+> ppr rn_head
- , text "res_rho:" <+> ppr res_rho ]
+ , text "app_res_rho:" <+> ppr app_res_rho ]
; return (EValArg { ea_ctxt = ctxt
, ea_arg = L arg_loc (mkHsWrap wrap arg')
@@ -705,6 +716,11 @@ tcInstFun do_ql inst_final fun_ctxt tc_fun fun_sigma rn_args
-- Going around again means we deal easily with
-- nested forall a. Eq a => forall b. Show b => blah
+ -- Rule IRESULT from Fig 4 of the QL paper; no more arguments
+ go1 _pos delta acc fun_ty []
+ = do { traceTc "tcInstFun:ret" (ppr fun_ty)
+ ; return (delta, reverse acc, fun_ty) }
+
-- Rule ITVDQ from the GHC Proposal #281
go1 pos delta acc fun_ty ((EValArg { ea_arg = arg }) : rest_args)
| Just (tvb, body) <- tcSplitForAllTyVarBinder_maybe fun_ty
@@ -715,11 +731,6 @@ tcInstFun do_ql inst_final fun_ctxt tc_fun fun_sigma rn_args
; let wrap = mkWpTyApps [ty_arg]
; go (pos+1) delta (addArgWrap wrap acc) inst_body rest_args }
- -- Rule IRESULT from Fig 4 of the QL paper
- go1 _pos delta acc fun_ty []
- = do { traceTc "tcInstFun:ret" (ppr fun_ty)
- ; return (delta, reverse acc, fun_ty) }
-
go1 pos delta acc fun_ty (EWrap w : args)
= go1 pos delta (EWrap w : acc) fun_ty args
@@ -1720,40 +1731,39 @@ quickLookArg1 ctxt larg@(L _ arg) sc_arg_ty@(Scaled _ orig_arg_rho)
<- captureConstraints $
tcInstFun do_ql True fun_ctxt tc_fun fun_sigma rn_args
- ; let -- mk_ql_arg captures the results so far, for resumption in tcValArg
- mk_ql_arg :: QLArgStatus -> HsExprArg 'TcpInst
- mk_ql_arg status
- = EValArgQL { eaql_status = status
- , eaql_ctxt = ctxt
- , eaql_arg_ty = sc_arg_ty
- , eaql_larg = larg
- , eaql_head = rn_head
- , eaql_tc_fun = tc_fun
- , eaql_args = inst_args
- , eaql_res_rho = app_res_rho }
-
- guarded = isGuardedTy orig_arg_rho
- -- NB: guardedness is computed based on the original,
- -- unzonked orig_arg_rho, so that we deliberately do
- -- not exploit guardedness that emerges a result of QL on earlier args
-
; traceTc "quickLookArg 2" $
vcat [ text "arg:" <+> ppr arg
, text "orig_arg_rho:" <+> ppr orig_arg_rho
, text "app_res_rho:" <+> ppr app_res_rho ]
-- Step 3: Check the two other premises of APP-lightning-bolt (Fig 5 in the paper)
- -- Namely: (A) is rho guarded, and (B) fiv(rho_r) = emptyset
+ -- Namely: (A) is orig_arg_rho is guarded
+ -- or: (B) fiv(app_res_rho) = emptyset
-- This tells us if the quick look at the argument yields information that
-- influences the enclosing function call
+ -- NB: guardedness is computed based on the original,
+ -- unzonked orig_arg_rho, so that we deliberately do
+ -- not exploit guardedness that emerges a result of QL on earlier args
; arg_influences_enclosing_call
- <- if guarded -- (A)
+ <- if isGuardedTy orig_arg_rho
then return True
else not <$> anyFreeKappa app_res_rho -- (B)
-- For (B) see Note [The fiv test in quickLookArg]
-- Step 4: do quick-look unification if either (A) or (B) hold
-- NB: orig_arg_rho may not be zonked, but that's ok
+ ; let -- mk_ql_arg captures the results so far, for resumption in tcValArg
+ mk_ql_arg :: QLArgStatus -> HsExprArg 'TcpInst
+ mk_ql_arg status
+ = EValArgQL { eaql_status = status
+ , eaql_ctxt = ctxt
+ , eaql_arg_ty = sc_arg_ty
+ , eaql_larg = larg
+ , eaql_head = rn_head
+ , eaql_tc_fun = tc_fun
+ , eaql_args = inst_args
+ , eaql_res_rho = app_res_rho }
+
; if arg_influences_enclosing_call
then -- No generalisation will take place for this argument! So we can:
-- * emit the constraints from the argument right now, and
@@ -1761,9 +1771,9 @@ quickLookArg1 ctxt larg@(L _ arg) sc_arg_ty@(Scaled _ orig_arg_rho)
-- No skolemisation of orig_arg_ty needed here:
-- tcIsDeepRho checked that there are no foralls to skolemise
do { emitConstraints wanted
- ; res_wrap <- unifyResTy arg fun_ctxt tc_fun inst_args app_res_rho orig_arg_rho
+ ; qlUnify app_res_rho orig_arg_rho
; traceTc "quickLookArg unify" (ppr rn_fun)
- ; return (mk_ql_arg (QLUnified res_wrap)) }
+ ; return (mk_ql_arg QLUnified) }
else -- Argument does not influence the enclosing call.
-- Quick-look on this argument was in vain (but we still don't want to waste
@@ -1887,19 +1897,14 @@ which has no free instantiation variables, so we can QL-unify
-}
---------------------
-{-
-qlUnify :: Delta -> TcType -> TcType -> TcM ()
+qlUnify :: TcType -> TcType -> TcM ()
-- Unify ty1 with ty2, unifying /only/ instantiation variables in delta
-- (it /never/ unifies ordinary unification variables)
-- It never produces errors, even for mis-matched types
-- It may return without having made the types equal, of course;
-- it just makes best efforts.
-qlUnify delta ty1 ty2
- = assertPpr (not (isEmptyVarSet delta)) (ppr delta $$ ppr ty1 $$ ppr ty2) $
- -- Only called with a non-empty delta
- -- Empty <=> nothing to do
- do { traceTc "qlUnify" (ppr delta $$ ppr ty1 $$ ppr ty2)
- ; go (emptyVarSet,emptyVarSet) ty1 ty2 }
+qlUnify ty1 ty2
+ = go (emptyVarSet,emptyVarSet) ty1 ty2
where
go :: (TyVarSet, TcTyVarSet)
-> TcType -> TcType
@@ -1907,10 +1912,10 @@ qlUnify delta ty1 ty2
-- The TyVarSets give the variables bound by enclosing foralls
-- for the corresponding type. Don't unify with these.
go bvs (TyVarTy tv) ty2
- | tv `elemVarSet` delta = go_kappa bvs tv ty2
+ | isQLInstTyVar tv = go_kappa bvs tv ty2
go (bvs1, bvs2) ty1 (TyVarTy tv)
- | tv `elemVarSet` delta = go_kappa (bvs2,bvs1) tv ty1
+ | isQLInstTyVar tv = go_kappa (bvs2,bvs1) tv ty1
go bvs (CastTy ty1 _) ty2 = go bvs ty1 ty2
go bvs ty1 (CastTy ty2 _) = go bvs ty1 ty2
@@ -1997,7 +2002,7 @@ qlUnify delta ty1 ty2
| kind1 `tcEqType` kind2
= return ty2
| otherwise
- = do { qlUnify delta kind1 kind2
+ = do { qlUnify kind1 kind2
; (kind1, kind2) <- liftZonkM $
do { kind1 <- zonkTcType kind1
; kind2 <- zonkTcType kind2
@@ -2018,7 +2023,7 @@ qlUnify delta ty1 ty2
, uo_expected = kind1
, uo_thing = Just (TypeThing ty2)
, uo_visible = True }
--}
+
{- Note [Actual unification during QuickLook]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In qlUnify, if we find (kappa ~ ty), we are going to update kappa := ty.
=====================================
compiler/GHC/Tc/Gen/Head.hs
=====================================
@@ -208,7 +208,7 @@ type family XEVAType (p :: TcPass) where -- Value arguments
data QLFlag = DoQL | NoQL
data QLArgStatus -- See (QLA2) in Note [Quick Look at value arguments] in GHC.Tc.Gen.App
- = QLUnified HsWrapper -- Unified with caller
+ = QLUnified -- Unified with caller
| QLIndependent WantedConstraints -- Independent of caller
data EWrap = EPar AppCtxt
@@ -441,7 +441,7 @@ instance OutputableBndrId (XPass p) => Outputable (HsExprArg p) where
2 (vcat [ ppr args, text "ea_ql_ty:" <+> ppr ty ])
instance Outputable QLArgStatus where
- ppr (QLUnified wrap) = text "QLUnified" <> braces (ppr wrap)
+ ppr QLUnified = text "QLUnified"
ppr (QLIndependent wc) = text "QLIndependent" <> braces (ppr wc)
instance Outputable EWrap where
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1faefc72a12680b3d70333f2cdf5482e468c7726
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1faefc72a12680b3d70333f2cdf5482e468c7726
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/20240529/a7e718f5/attachment-0001.html>
More information about the ghc-commits
mailing list