[Git][ghc/ghc][wip/sand-witch/lazy-skol] More wibbles
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Sat Jan 27 22:22:54 UTC 2024
Simon Peyton Jones pushed to branch wip/sand-witch/lazy-skol at Glasgow Haskell Compiler / GHC
Commits:
900ecaad by Simon Peyton Jones at 2024-01-27T22:22:06+00:00
More wibbles
..especially putting implicationNeeded back into checkConstraints
- - - - -
6 changed files:
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Gen/Expr.hs
- compiler/GHC/Tc/Gen/Head.hs
- compiler/GHC/Tc/Gen/Match.hs
- compiler/GHC/Tc/Gen/Pat.hs
- compiler/GHC/Tc/Utils/Unify.hs
Changes:
=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -595,6 +595,7 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args
= go delta acc so_far fun_ty rest_args
-- Rule IALL from Fig 4 of the QL paper
+ -- Instantiate invisible foralls and dictionaries.
-- c.f. GHC.Tc.Utils.Instantiate.topInstantiate
go1 delta acc so_far fun_ty args
| (tvs, body1) <- tcSplitSomeForAllTyVars (inst_fun args) fun_ty
@@ -630,8 +631,10 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args
-- Rule ITVDQ from the GHC Proposal #281
go1 delta acc so_far fun_ty ((EValArg { eva_arg = ValArg arg }) : rest_args)
| Just (tvb, body) <- tcSplitForAllTyVarBinder_maybe fun_ty
- , binderFlag tvb == Required
- = do { (ty_arg, inst_body) <- tcVDQ fun_conc_tvs (tvb, body) arg
+ = assertPpr (binderFlag tvb == Required) (ppr fun_ty $$ ppr arg) $
+ -- Any invisible binders have been instantiated by IALL above,
+ -- so this forall must be visible (i.e. Required)
+ do { (ty_arg, inst_body) <- tcVDQ fun_conc_tvs (tvb, body) arg
; let wrap = mkWpTyApps [ty_arg]
; go delta (addArgWrap wrap acc) so_far inst_body rest_args }
@@ -709,15 +712,15 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args
go1 delta acc so_far fun_ty
(eva@(EValArg { eva_arg = ValArg arg, eva_ctxt = ctxt }) : rest_args)
= do { (wrap, arg_ty, res_ty) <-
- -- NB: matchActualFunTySigma does the rep-poly check.
+ -- NB: matchActualFunTy does the rep-poly check.
-- For example, suppose we have f :: forall r (a::TYPE r). a -> Int
-- In an application (f x), we need 'x' to have a fixed runtime
- -- representation; matchActualFunTySigma checks that when
+ -- representation; matchActualFunTy checks that when
-- taking apart the arrow type (a -> Int).
- matchActualFunTySigma
+ matchActualFunTy
(ExpectedFunTyArg (HsExprTcThing tc_fun) (unLoc arg))
(Just $ HsExprTcThing tc_fun)
- (n_val_args, so_far) fun_ty
+ (n_val_args, fun_sigma) fun_ty
; (delta', arg') <- if do_ql
then addArgCtxt ctxt arg $
-- Context needed for constraints
=====================================
compiler/GHC/Tc/Gen/Expr.hs
=====================================
@@ -941,8 +941,7 @@ tcSynArgA :: CtOrigin
-- and a wrapper to be applied to the overall expression
tcSynArgA orig op sigma_ty arg_shapes res_shape thing_inside
= do { (match_wrapper, arg_tys, res_ty)
- <- matchActualFunTysRho herald orig Nothing
- (length arg_shapes) sigma_ty
+ <- matchActualFunTys herald orig (length arg_shapes) sigma_ty
-- match_wrapper :: sigma_ty "->" (arg_tys -> res_ty)
; ((result, res_wrapper), arg_wrappers)
<- tc_syn_args_e (map scaledThing arg_tys) arg_shapes $ \ arg_results arg_res_mults ->
=====================================
compiler/GHC/Tc/Gen/Head.hs
=====================================
@@ -1074,8 +1074,7 @@ tcInferOverLit lit@(OverLit { ol_val = val
thing = NameThing from_name
mb_thing = Just thing
herald = ExpectedFunTyArg thing (HsLit noAnn hs_lit)
- ; (wrap2, sarg_ty, res_ty) <- matchActualFunTySigma herald mb_thing
- (1, []) from_ty
+ ; (wrap2, sarg_ty, res_ty) <- matchActualFunTy herald mb_thing (1, from_ty) from_ty
; co <- unifyType mb_thing (hsLitType hs_lit) (scaledThing sarg_ty)
-- See Note [Source locations for implicit function calls] in GHC.Iface.Ext.Ast
=====================================
compiler/GHC/Tc/Gen/Match.hs
=====================================
@@ -101,6 +101,7 @@ tcFunBindMatches :: UserTypeCtxt -> Name
-> ExpRhoType -- Expected type of function; caller
-- has skolemised any outer forall's
-> TcM (HsWrapper, MatchGroup GhcTc (LHsExpr GhcTc))
+-- See Note [Skolemisation overview] in GHC.Tc.Utils.Unify
tcFunBindMatches ctxt fun_name mult matches invis_pat_tys exp_ty
= assertPpr (funBindPrecondition matches) (pprMatches matches) $
do { -- Check that they all have the same no of arguments
=====================================
compiler/GHC/Tc/Gen/Pat.hs
=====================================
@@ -618,7 +618,7 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of
-- Expression must be a function
; let herald = ExpectedFunTyViewPat $ unLoc expr
; (expr_wrap1, Scaled _mult inf_arg_ty, inf_res_sigma)
- <- matchActualFunTySigma herald (Just . HsExprRnThing $ unLoc expr) (1,[]) expr_ty
+ <- matchActualFunTy herald (Just . HsExprRnThing $ unLoc expr) (1,expr_ty) expr_ty
-- See Note [View patterns and polymorphism]
-- expr_wrap1 :: expr_ty "->" (inf_arg_ty -> inf_res_sigma)
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -37,7 +37,7 @@ module GHC.Tc.Utils.Unify (
matchExpectedAppTy,
matchExpectedFunTys,
matchExpectedFunKind,
- matchActualFunTySigma, matchActualFunTysRho,
+ matchActualFunTy, matchActualFunTys,
checkTyEqRhs, recurseIntoTyConApp,
PuResult(..), failCheckWith, okCheckRefl, mapCheck,
@@ -107,15 +107,14 @@ import qualified Data.Semigroup as S ( (<>) )
-- in GHC.Tc.Utils.Concrete.
--
-- See Note [Return arguments with a fixed RuntimeRep].
-matchActualFunTySigma
+matchActualFunTy
:: ExpectedFunTyOrigin
-- ^ See Note [Herald for matchExpectedFunTys]
-> Maybe TypedThing
-- ^ The thing with type TcSigmaType
- -> (Arity, [Scaled TcSigmaType])
+ -> (Arity, TcType)
-- ^ Total number of value args in the call, and
- -- types of values args to which function has
- -- been applied already (reversed)
+ -- the original function type
-- (Both are used only for error messages)
-> TcRhoType
-- ^ Type to analyse: a TcRhoType
@@ -131,7 +130,7 @@ matchActualFunTySigma
-- then wrap :: fun_ty ~> (arg_ty -> res_ty)
-- and NB: res_ty is an (uninstantiated) SigmaType
-matchActualFunTySigma herald mb_thing err_info fun_ty
+matchActualFunTy herald mb_thing err_info fun_ty
= assertPpr (isRhoTy fun_ty) (ppr fun_ty) $
go fun_ty
where
@@ -185,18 +184,15 @@ matchActualFunTySigma herald mb_thing err_info fun_ty
------------
mk_ctxt :: TcType -> TidyEnv -> ZonkM (TidyEnv, SDoc)
- mk_ctxt res_ty = mkFunTysMsg herald n_val_args_in_call $
- mkScaledFunTys (reverse arg_tys_so_far) res_ty
- (n_val_args_in_call, arg_tys_so_far) = err_info
+ mk_ctxt _res_ty = mkFunTysMsg herald err_info
{- Note [matchActualFunTy error handling]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
matchActualFunTySigma is made much more complicated by the
desire to produce good error messages. Consider the application
f @Int x y
-In GHC.Tc.Gen.Expr.tcArgs we deal with visible type arguments,
-and then call matchActualFunTysPart for each individual value
-argument. It, in turn, must instantiate any type/dictionary args,
+In GHC.Tc.Gen.Head.tcInstFun we instantiate the function type, one
+argument at a time. It must instantiate any type/dictionary args,
before looking for an arrow type.
But if it doesn't find an arrow type, it wants to generate a message
@@ -218,18 +214,17 @@ Ugh!
-- INVARIANT: the returned argument types all have a syntactically fixed RuntimeRep
-- in the sense of Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete.
-- See Note [Return arguments with a fixed RuntimeRep].
-matchActualFunTysRho :: ExpectedFunTyOrigin -- ^ See Note [Herald for matchExpectedFunTys]
- -> CtOrigin
- -> Maybe TypedThing -- ^ the thing with type TcSigmaType
- -> Arity
- -> TcSigmaType
- -> TcM (HsWrapper, [Scaled TcSigmaTypeFRR], TcRhoType)
--- If matchActualFunTysRho n ty = (wrap, [t1,..,tn], res_ty)
+matchActualFunTys :: ExpectedFunTyOrigin -- ^ See Note [Herald for matchExpectedFunTys]
+ -> CtOrigin
+ -> Arity
+ -> TcSigmaType
+ -> TcM (HsWrapper, [Scaled TcSigmaTypeFRR], TcRhoType)
+-- If matchActualFunTys n ty = (wrap, [t1,..,tn], res_ty)
-- then wrap : ty ~> (t1 -> ... -> tn -> res_ty)
-- and res_ty is a RhoType
-- NB: the returned type is top-instantiated; it's a RhoType
-matchActualFunTysRho herald ct_orig mb_thing n_val_args_wanted fun_ty
- = go n_val_args_wanted [] fun_ty
+matchActualFunTys herald ct_orig n_val_args_wanted top_ty
+ = go n_val_args_wanted [] top_ty
where
go n so_far fun_ty
| not (isRhoTy fun_ty)
@@ -240,13 +235,13 @@ matchActualFunTysRho herald ct_orig mb_thing n_val_args_wanted fun_ty
go 0 _ fun_ty = return (idHsWrapper, [], fun_ty)
go n so_far fun_ty
- = do { (wrap_fun1, arg_ty1, res_ty1) <- matchActualFunTySigma
- herald mb_thing
- (n_val_args_wanted, so_far)
+ = do { (wrap_fun1, arg_ty1, res_ty1) <- matchActualFunTy
+ herald Nothing
+ (n_val_args_wanted, top_ty)
fun_ty
; (wrap_res, arg_tys, res_ty) <- go (n-1) (arg_ty1:so_far) res_ty1
; let wrap_fun2 = mkWpFun idHsWrapper wrap_res arg_ty1 res_ty
- -- NB: arg_ty1 comes from matchActualFunTySigma, so it has
+ -- NB: arg_ty1 comes from matchActualFunTy, so it has
-- a syntactically fixed RuntimeRep as needed to call mkWpFun.
; return (wrap_fun2 <.> wrap_fun1, arg_ty1:arg_tys, res_ty) }
@@ -320,7 +315,7 @@ Both ultimately handled by matchExpectedFunTys.
* tcSkolemiseGeneral when the polytpe just comes from the context e.g. (f e)
The former just calls the latter, so the two cases differ only slightly:
* Both do shallow skolemisation
- * Both go via tcSkolemiseGeneral, which uses implicationNeeded to decide whether
+ * Both go via checkConstraints, which uses implicationNeeded to decide whether
to build an implication constraint even if there /are/ no skolems.
See Note [When to build an implication] below.
@@ -395,28 +390,19 @@ tcSkolemiseGeneral
-> ([(Name, TcInvisTVBinder)] -> TcType -> TcM result)
-> TcM (HsWrapper, result)
tcSkolemiseGeneral ds_flag ctxt top_ty expected_ty thing_inside
- = do { implication_needed <- implicationNeeded ds_flag ctxt expected_ty
- ; if not implication_needed
- -- Fast path. We check every function argument with tcCheckPolyExpr,
- -- which uses tcTopSkolemise and hence checkConstraints.
- -- So this fast path is well-exercised
- then do { res <- thing_inside [] expected_ty
- ; return (idHsWrapper, res) }
- else
-
- -- So we need an implication constraint
- do { -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv]
+ = do { -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv]
-- in GHC.Tc.Utils.TcType
; rec { (wrap, tv_prs, given, rho_ty) <- case ds_flag of
Deep -> deeplySkolemise skol_info expected_ty
Shallow -> topSkolemise skol_info expected_ty
- ; skol_info <- mkSkolemInfo (SigSkol ctxt top_ty (map (fmap binderVar) tv_prs)) }
+ ; let sig_skol = SigSkol ctxt top_ty (map (fmap binderVar) tv_prs)
+ ; skol_info <- mkSkolemInfo sig_skol }
; let skol_tvs = map (binderVar . snd) tv_prs
- ; (ev_binds, result) <- checkConstraints (getSkolemInfo skol_info) skol_tvs given $
+ ; (ev_binds, result) <- checkConstraints sig_skol skol_tvs given $
thing_inside tv_prs rho_ty
- ; return (wrap <.> mkWpLet ev_binds, result) } }
+ ; return (wrap <.> mkWpLet ev_binds, result) }
-- The ev_binds returned by checkConstraints is very
-- often empty, in which case mkWpLet is a no-op
@@ -461,13 +447,24 @@ checkConstraints :: SkolemInfoAnon
-> [EvVar] -- Given
-> TcM result
-> TcM (TcEvBinds, result)
--- Always builds an implication
+-- checkConstraints is careful to build an implication even if
+-- `skol_tvs` and `given` are both empty, under certain circumstances
+-- See Note [When to build an implication]
checkConstraints skol_info skol_tvs given thing_inside
- = do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside
- ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info skol_tvs given wanted
- ; traceTc "checkConstraints" (ppr tclvl $$ ppr skol_tvs)
- ; emitImplications implics
- ; return (ev_binds, result) }
+ = do { implication_needed <- implicationNeeded skol_info skol_tvs given
+
+ ; if implication_needed
+ then do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside
+ ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info skol_tvs given wanted
+ ; traceTc "checkConstraints" (ppr tclvl $$ ppr skol_tvs)
+ ; emitImplications implics
+ ; return (ev_binds, result) }
+
+ else -- Fast path. We check every function argument with tcCheckPolyExpr,
+ -- which uses tcTopSkolemise and hence checkConstraints.
+ -- So this fast path is well-exercised
+ do { res <- thing_inside
+ ; return (emptyTcEvBinds, res) } }
checkTvConstraints :: SkolemInfo
-> [TcTyVar] -- Skolem tyvars
@@ -515,22 +512,27 @@ buildTvImplication skol_info skol_tvs tclvl wanted
; checkImplicationInvariants implic'
; return implic' }
-implicationNeeded :: DeepSubsumptionFlag -> UserTypeCtxt -> TcType -> TcM Bool
+implicationNeeded :: SkolemInfoAnon -> [TcTyVar] -> [EvVar] -> TcM Bool
-- See Note [When to build an implication]
-implicationNeeded ds_flag ctxt expected_ty
- | definitely_mono ds_flag expected_ty -- Check for no invisible quantifiers
- , not (alwaysBuildImplication ctxt)
+implicationNeeded skol_info skol_tvs given
+ | null skol_tvs
+ , null given
+ , not (alwaysBuildImplication skol_info)
= -- Empty skolems and givens
- -- Build an implication if any of the "defer" flags is on
- do { dflags <- getDynFlags
+ do { tc_lvl <- getTcLevel
+ ; if not (isTopTcLevel tc_lvl) -- No implication needed if we are
+ then return False -- already inside an implication
+ else
+ do { dflags <- getDynFlags -- If any deferral can happen,
+ -- we must build an implication
; return (gopt Opt_DeferTypeErrors dflags ||
gopt Opt_DeferTypedHoles dflags ||
- gopt Opt_DeferOutOfScopeVariables dflags) }
+ gopt Opt_DeferOutOfScopeVariables dflags) } }
| otherwise -- Non-empty skolems or givens
= return True -- Definitely need an implication
-alwaysBuildImplication :: UserTypeCtxt -> Bool
+alwaysBuildImplication :: SkolemInfoAnon -> Bool
-- See Note [When to build an implication]
alwaysBuildImplication _ = False
@@ -849,11 +851,11 @@ matchExpectedFunTys herald ctx arity (Check top_ty) thing_inside
-- But in that case we add specialized type into error context
-- anyway, because it may be useful. See also #9605.
check n_so_far rev_pat_tys res_ty
- = addErrCtxtM (mkFunTysMsg herald arity fun_ty) $
+ = addErrCtxtM (mkFunTysMsg herald (arity, top_ty)) $
defer n_so_far rev_pat_tys res_ty
- where
- res_exp_ty = mkCheckExpType res_ty
- fun_ty = reconstructCheckType (reverse rev_pat_tys) res_exp_ty
+-- where
+-- res_exp_ty = mkCheckExpType res_ty
+-- fun_ty = reconstructCheckType (reverse rev_pat_tys) res_exp_ty
------------
defer :: Arity -> [ExpPatType] -> TcRhoType -> TcM (HsWrapper, a)
@@ -880,21 +882,16 @@ new_check_arg_ty herald arg_pos -- Position for error messages only
; return (mkScaled mult arg_ty) }
mkFunTysMsg :: ExpectedFunTyOrigin
- -> Arity
- -> TcType
+ -> (Arity, TcType)
-> TidyEnv -> ZonkM (TidyEnv, SDoc)
-mkFunTysMsg herald n_val_args_in_call fun_ty env
+mkFunTysMsg herald (n_val_args_in_call, fun_ty) env
= do { (env', fun_ty) <- zonkTidyTcType env fun_ty
- ; let (all_arg_tys, _) =
- -- No invisible quantifiers here (neither `ctx => t` nor `forall x. t`)
- -- because `mkFunTysMsg` never gets those as input in the first place,
- -- so there is no need to filter them out.
- splitPiTys fun_ty
+ ; let (pi_ty_bndrs, _) = splitPiTys fun_ty
-- `all_arg_tys` contains visible quantifiers only, so their number matches
-- the number of arguments that the user needs to pass to the function.
- n_fun_args = length all_arg_tys
+ n_fun_args = count isVisiblePiTyBinder pi_ty_bndrs
msg | n_val_args_in_call <= n_fun_args -- Enough args, in the end
= text "In the result of a function call"
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/900ecaad187908028f67017819ca2720cfd5f2a2
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/900ecaad187908028f67017819ca2720cfd5f2a2
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/20240127/24eaa194/attachment-0001.html>
More information about the ghc-commits
mailing list