[Git][ghc/ghc][wip/T24676] Improved zonking!
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Thu May 30 22:56:00 UTC 2024
Simon Peyton Jones pushed to branch wip/T24676 at Glasgow Haskell Compiler / GHC
Commits:
1e1d4ee8 by Simon Peyton Jones at 2024-05-30T23:55:18+01:00
Improved zonking!
And some Notes are better too
- - - - -
5 changed files:
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Gen/Head.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- compiler/GHC/Tc/Zonk/Monad.hs
- compiler/GHC/Tc/Zonk/TcType.hs
Changes:
=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -93,53 +93,59 @@ because it deal with n-ary application. The main workhorse is tcApp.
Some notes relative to the paper
-* The "instantiation variables" of the paper are ordinary unification
+(QL1) The "instantiation variables" of the paper are ordinary unification
variables. We keep track of which variables are instantiation variables
- by keeping a set Delta of instantiation variables.
+ by giving them a TcLevel of QLInstVar, which is like "infinity".
-* When we learn what an instantiation variable must be, we simply unify
+(QL2) When we learn what an instantiation variable must be, we simply unify
it with that type; this is done in qlUnify, which is the function mgu_ql(t1,t2)
of the paper. This may fill in a (mutable) instantiation variable with
a polytype.
-* When QL is done, we don't need to turn the un-filled-in
- instantiation variables into unification variables -- they
- already /are/ unification variables! See also
- Note [Instantiation variables are short lived].
+(QL3) When QL is done, we turn the instantiation variables into ordinary unification
+ variables, using qlZonkTcType. This function fully zonks the type (thereby
+ revealing all the polytypes, and updates any instantaition variables with
+ ordinary unification variables.
+ See Note [Instantiation variables are short lived].
-* We cleverly avoid the quadratic cost of QL, alluded to in the paper.
+(QL4) We cleverly avoid the quadratic cost of QL, alluded to in the paper.
See Note [Quick Look at value arguments]
Note [Instantiation variables are short lived]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-By the time QL is done, all filled-in occurrences of instantiation
-variables have been zonked away (see "Crucial step" in tcValArgs),
-and so the constraint /generator/ never subsequently sees a meta-type
-variable filled in with a polytype -- a meta type variable stands
-(only) for a monotype. See Section 4.3 "Applications and instantiation"
-of the paper.
-
-However, the constraint /solver/ can see a meta-type-variable filled
-in with a polytype (#18987). Suppose
- f :: forall a. Dict a => [a] -> [a]
- xs :: [forall b. b->b]
-and consider the call (f xs). QL will
-* Instantiate f, with a := kappa, where kappa is an instantiation variable
-* Emit a constraint (Dict kappa), via instantiateSigma, called from tcInstFun
-* Do QL on the argument, to discover kappa := forall b. b->b
-
-But by the time the third step has happened, the constraint has been
-emitted into the monad. The constraint solver will later find it, and
-rewrite it to (Dict (forall b. b->b)). That's fine -- the constraint
-solver does no implicit instantiation (which is what makes it so
-tricky to have foralls hiding inside unification variables), so there
-is no difficulty with allowing those filled-in kappa's to persist.
-(We could find them and zonk them away, but that would cost code and
-execution time, for no purpose.)
-
-Since the constraint solver does not do implicit instantiation (as the
-constraint generator does), the fact that a unification variable might
-stand for a polytype does not matter.
+* An instantation variable is a mutable meta-type-variable, whose level number
+ is QLInstVar.
+
+* Ordinary unifcation variables always stand for monotypes; only instantiation
+ variables can be unified with a polytype (by `qlUnify`).
+
+* By the time QL is done, all filled-in occurrences of instantiation variables
+ have been zonked away with `qlZonkTcType` (see "Crucial step" in tcValArgs).
+
+ See Section 4.3 "Applications and instantiation" of the paper.
+
+* The constraint solver never sees an instantiation variable.
+
+ However, the constraint solver can see a meta-type-variable filled
+ in with a polytype (#18987). Suppose
+ f :: forall a. Dict a => [a] -> [a]
+ xs :: [forall b. b->b]
+ and consider the call (f xs). QL will
+ * Instantiate f, with a := kappa, where kappa is an instantiation variable
+ * Emit a constraint (Dict kappa), via instantiateSigma, called from tcInstFun
+ * Do QL on the argument, to discover kappa := forall b. b->b
+
+ But by the time the third step has happened, the constraint has been emitted
+ into the monad. The constraint solver will later find it, and rewrite it to
+ (Dict (forall b. b->b)). That's fine -- the constraint solver does no implicit
+ instantiation (which is what makes it so tricky to have foralls hiding inside
+ unification variables), so there is no difficulty with allowing those
+ filled-in kappa's to persist. (We could find them and zonk them away, but
+ that would cost code and execution time, for no purpose.)
+
+ Since the constraint solver does not do implicit instantiation (as the
+ constraint generator does), the fact that a unification variable might stand
+ for a polytype does not matter.
-}
@@ -250,26 +256,42 @@ tcApp works like this:
Otherwise, delegate back to tcExpr, which
infers an (instantiated) TcRhoType
-3. Use tcInstFun to instantiate the function, Quick-Looking as we go.
- This implements the |-inst judgement in Fig 4, plus the
- modification in Fig 5, of the QL paper:
- "A quick look at impredicativity" (ICFP'20).
+3. Use tcInstFun to instantiate the function, Quick-Looking as we go. This
+ implements the |-inst judgement in Fig 4, plus the modification in Fig 5, of
+ the QL paper: "A quick look at impredicativity" (ICFP'20).
- In tcInstFun we take a quick look at value arguments, using
- quickLookArg. See Note [Quick Look at value arguments].
+ In tcInstFun we take a quick look at value arguments, using quickLookArg.
+ See Note [Quick Look at value arguments].
+
+ (TCAPP1) Crucially, just before `tcApp` calls `tcInstFun`, it sets the
+ ambient TcLevel to QLInstVar, so all unification variables allocated by
+ tcInstFun, and in the quick-looks it does at the arguments, will be
+ instantiation variables.
+
+ Consider (f (g (h x))).`tcApp` instantiates the call to `f`, and in doing
+ so quick-looks at the argument(s), in this case (g (h x)). But
+ `quickLookArg` on (g (h x)) in turn instantiates `g` and quick-looks at
+ /its/ argument(s), in this case (h x). And so on recursively. Key
+ point: all these instantiations make instantiation variables.
4. Use quickLookResultType to take a quick look at the result type,
when in checking mode. This is the shaded part of APP-Downarrow
in Fig 5.
-5. Use unifyResultType to match up the result type of the call
+5. Then we call finishApp to finish the job
+
+6. finishApp uses qlZonkTcType to expose what we have learned from
+ Quick Look (if Quick Look is being used for this application)
+
+7. Then call checkResultTy to match up the result type of the call
with that expected by the context. See Note [Unify with
expected type before typechecking arguments]
-6. Use tcValArgs to typecheck the value arguments
+8. Use tcValArgs to typecheck the value arguments
-7. After a gruesome special case for tagToEnum, rebuild the result.
+9. Horrible newtype check
+10. After a gruesome special case for tagToEnum, rebuild the result.
Some cases that /won't/ work:
@@ -323,8 +345,7 @@ Unify result type /before/ typechecking the args
Actual: String
• In the first argument of ‘Pair’, namely ‘"yes"’
-The latter is much better. That is why we call unifyExpectedType
-before tcValArgs.
+The latter is much better. That is why we call checkResultType before tcValArgs.
-}
tcApp :: HsExpr GhcRn
@@ -332,60 +353,63 @@ tcApp :: HsExpr GhcRn
-> TcM (HsExpr GhcTc)
-- See Note [tcApp: typechecking applications]
tcApp rn_expr exp_res_ty
- = do { (fun@(rn_fun, fun_ctxt), rn_args) <- splitHsApps rn_expr
+ = do { -- Step 1: Split the application chain
+ (fun@(rn_fun, fun_ctxt), rn_args) <- splitHsApps rn_expr
; traceTc "tcApp {" $
vcat [ text "rn_expr:" <+> ppr rn_expr
, text "rn_fun:" <+> ppr rn_fun
, text "fun_ctxt:" <+> ppr fun_ctxt
, text "rn_args:" <+> ppr rn_args ]
- -- Infer the type of `fun`, the head of the application
+ -- Step 2: Infer the type of `fun`, the head of the application
; (tc_fun, fun_sigma) <- tcInferAppHead fun
- -- Instantiate
+ -- Step 3: Instantiate the function type (taking a quick look at args)
; do_ql <- wantQuickLook rn_fun
; (inst_args, app_res_rho)
- <- setQLInstLevel do_ql $
+ <- setQLInstLevel do_ql $ -- See (TCAPP1) in
+ -- Note [tcApp: typechecking applications]
tcInstFun do_ql True fun_ctxt tc_fun fun_sigma rn_args
- ; 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
- ; ds_flag <- getDeepSubsumptionFlag
- ; finishApp do_ql ds_flag rn_expr fun_ctxt tc_fun inst_args app_res_rho exp_res_ty }
+ -- Step 3: Take a quick look at the result type
+ ; quickLookResultType do_ql app_res_rho exp_res_ty
+
+ -- Finish up
+ ; finishApp do_ql 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 :: QLFlag -> DeepSubsumptionFlag -> HsExpr GhcRn -> AppCtxt
+quickLookResultType :: QLFlag -> TcRhoType -> ExpRhoType -> TcM ()
+-- This function implements the shaded bit of rule APP-Downarrow in
+-- Fig 5 of the QL paper: "A quick look at impredicativity" (ICFP'20).
+quickLookResultType DoQL app_res_rho (Check exp_rho) = qlUnify app_res_rho exp_rho
+quickLookResultType _ _ _ = return ()
+
+finishApp :: QLFlag -> HsExpr GhcRn -> AppCtxt
-> HsExpr GhcTc -> [HsExprArg 'TcpInst]
- -> TcRhoType -- Inferred type of the application;
- -- zonked, but maybe not deeply instantiated
+ -> TcRhoType -- Inferred type of the application
-> ExpRhoType -- Expected type; this is deeply skolemised
-> TcM (HsExpr GhcTc)
--- At this point there are no more instantiation variables
-finishApp do_ql 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
+finishApp do_ql rn_expr fun_ctxt tc_fun inst_args app_res_rho exp_res_ty
+ = do { -- Step 6: qlZonk the type of the result of the call
+ traceTc "finishApp" $ vcat [ ppr app_res_rho, ppr exp_res_ty ]
+ ; app_res_rho <- case do_ql of
+ DoQL -> liftZonkM $ qlZonkTcType app_res_rho
+ NoQL -> return app_res_rho
+
+ -- Step 7: check the result type
+ ; res_wrap <- checkResultTy rn_expr fun_ctxt tc_fun inst_args
+ app_res_rho exp_res_ty
- -- Typecheck the value arguments
+ -- step 8: Typecheck the value arguments
; tc_args <- mapM (tcValArg do_ql) inst_args
- -- Horrible newtype check
+ -- Step 9: Horrible newtype check
; rejectRepPolyNewtypes tc_fun app_res_rho
- -- Reconstruct, with a special case for tagToEnum#.
+ -- Step 10: econstruct, with a special case for tagToEnum#.
; tc_expr <- if isTagToEnum tc_fun
then tcTagToEnum tc_fun fun_ctxt tc_args app_res_rho
else return (rebuildHsApps tc_fun fun_ctxt tc_args)
@@ -401,26 +425,27 @@ finishApp do_ql ds_flag rn_expr fun_ctxt tc_fun inst_args app_res_rho exp_res_ty
; return (mkHsWrap res_wrap tc_expr) }
-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
+checkResultTy :: 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
-- 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)
+checkResultTy _ _ _ _ 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)
+checkResultTy 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]
--
-- Match up app_res_rho: the result type of rn_expr
-- with res_ty: the expected result type
= perhaps_add_res_ty_ctxt $
- do { traceTc "checkResTy {" $
+ do { ds_flag <- getDeepSubsumptionFlag
+ ; traceTc "checkResultTy {" $
vcat [ text "tc_fun:" <+> ppr tc_fun
, text "app_res_rho:" <+> ppr app_res_rho
, text "res_ty:" <+> ppr res_ty
@@ -431,7 +456,7 @@ checkResTy ds_flag rn_expr fun_ctxt tc_fun inst_args app_res_rho (Check res_ty)
-- so with simple subsumption we can just unify them
-- No need to zonk; the unifier does that
do { co <- unifyExprType rn_expr app_res_rho res_ty
- ; traceTc "checkResTy 1 }" (ppr co)
+ ; traceTc "checkResultTy 1 }" (ppr co)
; return (mkWpCastN co) }
Deep -> -- Deep subsumption
@@ -441,7 +466,7 @@ checkResTy ds_flag rn_expr fun_ctxt tc_fun inst_args app_res_rho (Check res_ty)
-- 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 "checkResTy 2 }" (ppr app_res_rho $$ ppr res_ty)
+ ; traceTc "checkResultTy 2 }" (ppr app_res_rho $$ ppr res_ty)
; return wrap } }
where
-- perhaps_add_res_ty_ctxt: Inside an expansion, the addFunResCtxt stuff is
@@ -455,31 +480,7 @@ checkResTy ds_flag rn_expr fun_ctxt tc_fun inst_args app_res_rho (Check res_ty)
= addFunResCtxt tc_fun inst_args app_res_rho (mkCheckExpType res_ty) $
thing_inside
-
---------------------
-wantQuickLook :: HsExpr GhcRn -> TcM QLFlag
-wantQuickLook (HsVar _ (L _ f))
- | getUnique f `elem` quickLookKeys = return DoQL
-wantQuickLook _ = do { impred <- xoptM LangExt.ImpredicativeTypes
- ; if impred then return DoQL else return NoQL }
-
-quickLookKeys :: [Unique]
--- See Note [Quick Look for particular Ids]
-quickLookKeys = [dollarIdKey, leftSectionKey, rightSectionKey]
-
--- zonkArg is used *only* during debug-tracing, to make it easier to
--- see what is going on. For that reason, it is not a full zonk: add
--- more if you need it.
-zonkArg :: HsExprArg 'TcpInst -> ZonkM (HsExprArg 'TcpInst)
-zonkArg eva@(EValArg { ea_arg_ty = Scaled m ty })
- = do { ty' <- zonkTcType ty
- ; return (eva { ea_arg_ty = Scaled m ty' }) }
-zonkArg arg = return arg
-
-
-
----------------
-
tcValArg :: QLFlag -> HsExprArg 'TcpInst -- Actual argument
-> TcM (HsExprArg 'TcpTc) -- Resulting argument
tcValArg _ (EPrag l p) = return (EPrag l (tcExprPrag p))
@@ -488,11 +489,11 @@ tcValArg _ (ETypeArg l hs_ty ty) = return (ETypeArg l hs_ty ty)
tcValArg do_ql (EValArg { ea_ctxt = ctxt
, ea_arg = larg@(L arg_loc arg)
- , ea_arg_ty = Scaled mult exp_arg_ty })
+ , ea_arg_ty = sc_arg_ty })
= addArgCtxt ctxt larg $
do { traceTc "tcValArg" $
vcat [ ppr ctxt
- , text "arg type:" <+> ppr exp_arg_ty
+ , text "arg type:" <+> ppr sc_arg_ty
, text "arg:" <+> ppr arg ]
-- Crucial step: expose QL results before checking exp_arg_ty
@@ -504,9 +505,9 @@ tcValArg do_ql (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]
- ; exp_arg_ty <- case do_ql of
- DoQL -> liftZonkM $ zonkTcType exp_arg_ty
- NoQL -> return exp_arg_ty
+ ; Scaled mult exp_arg_ty <- case do_ql of
+ DoQL -> liftZonkM $ qlZonkScaledTcType sc_arg_ty
+ NoQL -> return sc_arg_ty
-- Now check the argument
; arg' <- tcScalingUsage mult $
@@ -518,16 +519,16 @@ tcValArg do_ql (EValArg { ea_ctxt = ctxt
tcValArg _ (EValArgQL { eaql_wanted = wanted
, eaql_ctxt = ctxt
- , eaql_arg_ty = Scaled mult exp_arg_ty
+ , eaql_arg_ty = sc_arg_ty
, eaql_larg = larg@(L arg_loc rn_expr)
, eaql_head = rn_head
, eaql_tc_fun = tc_fun
, eaql_args = inst_args
+ , eaql_encl = arg_influences_enclosing_call
, eaql_res_rho = app_res_rho })
= addArgCtxt ctxt larg $
- tcScalingUsage mult $
do { -- Expose QL results to tcSkolemise, as in EValArg case
- exp_arg_ty <- liftZonkM $ zonkTcType exp_arg_ty
+ Scaled mult exp_arg_ty <- liftZonkM $ qlZonkScaledTcType sc_arg_ty
; traceTc "tcEValArgQL {" (vcat [ ppr rn_head
, text "app_res_rho:" <+> ppr app_res_rho
@@ -536,12 +537,12 @@ tcValArg _ (EValArgQL { eaql_wanted = wanted
; ds_flag <- getDeepSubsumptionFlag
; (wrap, arg')
- <- tcSkolemise ds_flag GenSigCtxt exp_arg_ty $ \ exp_arg_rho ->
+ <- tcScalingUsage mult $
+ tcSkolemise ds_flag GenSigCtxt exp_arg_ty $ \ exp_arg_rho ->
do { emitConstraints wanted
- ; qlUnify app_res_rho exp_arg_rho
- ; monomorphiseQLInstVars inst_args app_res_rho
- ; app_res_rho <- liftZonkM $ zonkTcType app_res_rho
- ; finishApp DoQL ds_flag rn_expr ctxt tc_fun inst_args
+ ; unless arg_influences_enclosing_call $ -- Don't repeat
+ qlUnify app_res_rho exp_arg_rho -- the qlUnify
+ ; finishApp DoQL rn_expr ctxt tc_fun inst_args
app_res_rho (mkCheckExpType exp_arg_rho) }
; traceTc "tcEValArgQL }" $
@@ -552,26 +553,26 @@ tcValArg _ (EValArgQL { eaql_wanted = wanted
, ea_arg = L arg_loc (mkHsWrap wrap arg')
, ea_arg_ty = noExtField }) }
--- case ql_status of
--- QLUnified -- We have decided to unify (no generalisation or deep subsumption)
--- -> -- So pass Shallow to finishApp
--- do { tc_app <- finishApp DoQL 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 tc_app
--- , ea_arg_ty = noExtField }) }
---
--- QLIndependent wc
+--------------------
+wantQuickLook :: HsExpr GhcRn -> TcM QLFlag
+wantQuickLook (HsVar _ (L _ f))
+ | getUnique f `elem` quickLookKeys = return DoQL
+wantQuickLook _ = do { impred <- xoptM LangExt.ImpredicativeTypes
+ ; if impred then return DoQL else return NoQL }
+
+quickLookKeys :: [Unique]
+-- See Note [Quick Look for particular Ids]
+quickLookKeys = [dollarIdKey, leftSectionKey, rightSectionKey]
- -- Tricky point: with deep subsumption, even if ql_status=QLUnified
- -- arg_ty will be a rho-type (no top-level foralls), but it may have
- -- /nested/ foralls; so if -XDeepSubsumption is on we should deeply
- -- skolemise it, in order to pass a deeply-skolemised type to finishApp.
- -- Example from haskeline:System.Console.Haskeline.Backend.Terminfo
- -- output $ blah
- -- output :: TermAction -> ActionM ()
- -- type ActionM a = forall m . (..) => ActionT (Draw m) a
+-- zonkArg is used *only* during debug-tracing, to make it easier to
+-- see what is going on. For that reason, it is not a full zonk: add
+-- more if you need it.
+zonkArg :: HsExprArg 'TcpInst -> ZonkM (HsExprArg 'TcpInst)
+zonkArg eva@(EValArg { ea_arg_ty = Scaled m ty })
+ = do { ty' <- zonkTcType ty
+ ; return (eva { ea_arg_ty = Scaled m ty' }) }
+zonkArg arg = return arg
{- *********************************************************************
* *
@@ -1539,46 +1540,29 @@ record, and /resume/ it later. The way to think of it is this:
This turned out to be more subtle than I expected. Wrinkles:
-(QLA1) We avoid zonking, so quickLookArg thereby sees the argument type /before/
- the QL substitution Theta is applied to it. So we achieve argument-order
- independence for free (see 5.7 in the paper). See the `guarded` predicate
- in `quickLookArg`.
-
-(QLA2) `quickLookArg` decides whether or not premises (A) and (B) of the
- quick-look-arg jugement APP-QL are satisfied; this is captured in `can_do_ql`:
-
- - can_do_ql=True:
- get info from argument by unifying the argument result type with
- the type expected by the caller, using `qlUnify` in `quickLookResultType`
- Capture the work done in EValArgQL with eaql_status = QLUnified.
+(QLA1) `quickLookArg` decides whether or not premises (A) and (B) of the
+ quick-look-arg judgement APP-QL are satisfied; this is captured in
+ `arg_influences_enclosing_call`.
- - can_do_ql=False:
- do not get info from argument; no `qlUnify`. Instead just save the
- work done in EValArgQL, with eaql_status = QLIndependent.
-
- We need to save the decision in eaql_status because the code that
- resumes checking the argument must behave differently in the two cases;
- see the EValArgQL case of `tcValArg` and (QLA4) below.
+(QLA1) We avoid zonking, so the `arg_influences_enclosing_call` sees the
+ argument type /before/ the QL substitution Theta is applied to it. So we
+ achieve argument-order independence for free (see 5.7 in the paper). See the
+ `isGuardedTy orig_arg_rho` test in `quickLookArg`.
(QLA3) Deciding whether the premises are satisfied involves calling `tcInstFun`
(which takes quite some work becuase it calls quickLookArg on nested calls).
That's why we want to capture the work done, in EValArgQL.
- Do we really have to call `tcInstFun` before deciding `can_do_ql`? Yes.
+ Do we really have to call `tcInstFun` before deciding (B) of
+ `arg_influences_enclosing_call`? Yes (#24686).
Suppose ids :: [forall a. a->a], and consider
(:) (reverse ids) blah
`tcApp` on the outer call will instantiate (:) with `kappa`, and take a
quick look at (reverse ids). Only after instantiating `reverse` with kappa2,
quick-looking at `ids` can we discover that (kappa2:=forall a. a->a), which
- satisfies premise (B) of can_do_ql.
-
-(QLA4) When we resume typechecking an argument, in `tcValArg`, we need to behave
- differently depending on `eaql_status` (see (QLA2)).
+ satisfies premise (B) of `arg_influence_enclosing_call`.
- It's fairly easy if eaql_status=QLUnified: just skolemise the type expected
- by the function (eaql_arg_ty), and call `finishApp` just like `tcApp` does.
-
- But for QLIndependent things are a bit tricky; see function `resume_ql_arg`:
+(QLA4) When we resume typechecking an argument, in `tcValArg` on `EValArgQL`
- quickLookArg has not yet done `qlUnify` with the calling context. We
must do so now. Example: choose [] ids,
@@ -1591,15 +1575,7 @@ This turned out to be more subtle than I expected. Wrinkles:
- Calling `tcInstFun` on the argument may have emitted some constraints, which
we carefully captured in `quickLookArg` and stored in the EValArgQL. We must
- now emit them with `emitConstraints`. (In the `QLUnified` case this was
- done in `quickLookArg`.)
-
- - Consider (f (g (h x))).`tcApp` instantiates the call to `f`, and in doing so
- quick-looks at the argument(s), in this case (g (h x)). But `quickLookArg`
- on (g (h x)) in turn instantiates `g` and quick-looks at /its/ argument(s),
- in this case (h x). And so on recursively. Key point: all these
- instantiations make instantiation variables whose level number is that of
- the /original/ `tcApp`.
+ now emit them with `emitConstraints`.
(QLA5) When we resume typechecking the argument (in the `EValArgQL` case of
`tcValArg`), we may now know that the arg is a polytype.
@@ -1740,6 +1716,7 @@ quickLookArg1 ctxt larg@(L _ arg) sc_arg_ty@(Scaled _ 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
+ -- We must do the anyFreeKappa test /after/ tcInstFun; see (QLA3).
; arg_influences_enclosing_call
<- if isGuardedTy orig_arg_rho
then return True
@@ -1760,41 +1737,9 @@ quickLookArg1 ctxt larg@(L _ arg) sc_arg_ty@(Scaled _ orig_arg_rho)
, eaql_tc_fun = tc_fun
, eaql_args = inst_args
, eaql_wanted = wanted
+ , eaql_encl = arg_influences_enclosing_call
, eaql_res_rho = app_res_rho }) }}}
--- ; 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 }
--- then -- No generalisation will take place for this argument! So we can:
--- -- * emit the constraints from the argument right now, and
--- -- * unify with the expected type
--- -- No skolemisation of orig_arg_ty needed here:
--- -- tcIsDeepRho checked that there are no foralls to skolemise
--- Try doing everything with QLIndependent
--- do { emitConstraints wanted
--- ; qlUnify app_res_rho orig_arg_rho
--- ; traceTc "quickLookArg unify" (ppr rn_fun)
--- ; return (mk_ql_arg QLUnified) }
--- do { qlUnify app_res_rho orig_arg_rho
--- ; return (mk_ql_arg (QLIndependent wanted)) }
---
--- else -- Argument does not influence the enclosing call.
--- -- Quick-look on this argument was in vain (but we still don't want to waste
--- -- the work). So we treat this argument entirely independently:
--- -- capture delta and wanted in QLIndependent for later resumption
--- do { traceTc "quickLookArg indep" (ppr rn_fun)
--- ; return (mk_ql_arg (QLIndependent wanted)) }
-
-
-
{- *********************************************************************
* *
Folding over instantiation variables
@@ -1823,6 +1768,7 @@ of Fig 5 of the Quick Look paper.
-}
+{-
monomorphiseQLInstVars :: [HsExprArg 'TcpInst] -> TcRhoType -> TcM ()
monomorphiseQLInstVars inst_args res_rho
= do { traceTc "monomorphiseQLInstVars {" $
@@ -1858,6 +1804,7 @@ instance Semigroup TcMUnit where
TCMU ml <> TCMU mr = TCMU (ml >> mr)
instance Monoid TcMUnit where
mempty = TCMU (return ())
+-}
anyFreeKappa :: TcType -> TcM Bool
-- True if there is a free instantiation variable (member of Delta)
@@ -1898,31 +1845,6 @@ foldQLInstVars check_tv ty
| otherwise = mempty
----------------
-{-
-quickLookResultType :: Delta -> TcRhoType -> ExpRhoType -> TcM TcRhoType
--- This function implements the shaded bit of rule APP-Downarrow in
--- Fig 5 of the QL paper: "A quick look at impredicativity" (ICFP'20).
--- It returns its second argument, but with any variables in Delta
--- substituted out, so no variables in Delta escape
-
-quickLookResultType delta app_res_rho (Check exp_rho)
- = -- In checking mode only, do qlUnify with the expected result type
- do { unless (isEmptyVarSet delta) $ -- Optimisation only
- qlUnify delta app_res_rho exp_rho
- ; return app_res_rho }
-
-quickLookResultType _ app_res_rho (Infer {})
- = liftZonkM $ zonkTcType app_res_rho
- -- Zonk the result type, to ensure that we substitute out any
- -- filled-in instantiation variable before calling
- -- unifyExpectedType. In the Check case, this isn't necessary,
- -- because unifyExpectedType just drops to tcUnify; but in the
- -- Infer case a filled-in instantiation variable (filled in by
- -- tcInstFun) might perhaps escape into the constraint
- -- generator. The safe thing to do is to zonk any instantiation
- -- variables away. See Note [Instantiation variables are short lived]
--}
-
{- Note [The fiv test in quickLookArg]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In rule APP-lightning-bolt in Fig 5 of the paper, we have to test rho_r
=====================================
compiler/GHC/Tc/Gen/Head.hs
=====================================
@@ -182,6 +182,8 @@ data HsExprArg (p :: TcPass) where -- See Note [HsExprArg]
, eaql_tc_fun :: HsExpr GhcTc -- Typechecked function
, eaql_args :: [HsExprArg 'TcpInst] -- Args, instantiated
, eaql_wanted :: WantedConstraints
+ , eaql_encl :: Bool -- True <=> we have already qlUnified
+ -- eaql_arg_ty and eaql_res_rho
, eaql_res_rho :: TcRhoType } -- Result type of the application
-> HsExprArg 'TcpInst -- Only exists in TcpInst phase
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -32,8 +32,6 @@ module GHC.Tc.Utils.TcMType (
cloneMetaTyVar, cloneMetaTyVarWithInfo,
newCycleBreakerTyVar,
- monomorphiseQLInstVar,
-
newMultiplicityVar,
readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
newTauTvDetailsAtLevel, newMetaDetails, newMetaTyVarName,
@@ -822,16 +820,6 @@ newPatTyVar name kind
; traceTc "newPatTyVar" (ppr tyvar)
; return tyvar }
-monomorphiseQLInstVar :: TcTyVar -> TcM ()
-monomorphiseQLInstVar tv
- | assertPpr (isQLInstTyVar tv) (ppr tv) True
- , MetaTv { mtv_info = info, mtv_ref = ref } <- tcTyVarDetails tv
- = do { details <- newMetaDetails info
- ; let mono_ty = mkTyVarTy (mkTcTyVar (tyVarName tv) (tyVarKind tv) details)
- ; liftZonkM $ writeMetaTyVarRef tv ref mono_ty }
- | otherwise
- = pprPanic "monomorphiseQLInstVar" (ppr tv)
-
cloneAnonMetaTyVar :: MetaInfo -> TyVar -> TcKind -> TcM TcTyVar
-- Make a fresh MetaTyVar, basing the name
-- on that of the supplied TyVar
=====================================
compiler/GHC/Tc/Zonk/Monad.hs
=====================================
@@ -9,7 +9,7 @@
module GHC.Tc.Zonk.Monad
( -- * The 'ZonkM' monad, a stripped down 'TcM' for zonking
ZonkM(ZonkM,runZonkM)
- , ZonkGblEnv(..), getZonkGblEnv
+ , ZonkGblEnv(..), getZonkGblEnv, getZonkTcLevel
-- ** Logging within 'ZonkM'
, traceZonk
@@ -97,6 +97,9 @@ getZonkGblEnv :: ZonkM ZonkGblEnv
getZonkGblEnv = ZonkM return
{-# INLINE getZonkGblEnv #-}
+getZonkTcLevel :: ZonkM TcLevel
+getZonkTcLevel = ZonkM (\env -> return (zge_tc_level env))
+
-- | Same as 'traceTc', but for the 'ZonkM' monad.
traceZonk :: String -> SDoc -> ZonkM ()
traceZonk herald doc = ZonkM $
=====================================
compiler/GHC/Tc/Zonk/TcType.hs
=====================================
@@ -21,6 +21,9 @@ module GHC.Tc.Zonk.TcType
, zonkInvisTVBinder
, zonkCo
+ -- ** Quick-look zonking
+ , qlZonkTcType, qlZonkScaledTcType
+
-- ** Zonking 'TyCon's
, zonkTcTyCon
@@ -201,6 +204,76 @@ See for example test T5631, which regresses without this change.
************************************************************************
-}
+qlZonkScaledTcType :: Scaled TcType -> ZonkM (Scaled TcType)
+qlZonkScaledTcType (Scaled m ty)
+ = Scaled <$> qlZonkTcType m <*> qlZonkTcType ty
+
+qlZonkTcType :: TcType -> ZonkM TcType
+qlZonkCo :: Coercion -> ZonkM Coercion
+(qlZonkTcType, _, qlZonkCo, _)
+ = mapTyCo mapper
+ where
+ mapper :: TyCoMapper () ZonkM
+ mapper = TyCoMapper
+ { tcm_tyvar = const qlzonk_tc_tyvar
+ , tcm_covar = const (\cv -> mkCoVarCo <$> qlzonk_tcv cv)
+ , tcm_hole = qlzonk_hole
+ , tcm_tycobinder = \ _env tcv _vis k -> qlzonk_tcv tcv >>= k ()
+ , tcm_tycon = return }
+
+ qlzonk_hole :: () -> CoercionHole -> ZonkM Coercion
+ qlzonk_hole _ hole@(CoercionHole { ch_ref = ref, ch_co_var = cv })
+ = do { contents <- readTcRef ref
+ ; case contents of
+ Just co -> qlZonkCo co
+ Nothing -> do { cv' <- qlzonk_tcv cv
+ ; return $ HoleCo (hole { ch_co_var = cv' }) } }
+
+ qlzonk_tcv :: TyCoVar -> ZonkM TyCoVar
+ qlzonk_tcv tcv = do { kind' <- qlZonkTcType (varType tcv)
+ ; return (setVarType tcv kind') }
+
+ qlzonk_tc_tyvar :: TcTyVar -> ZonkM TcType
+ qlzonk_tc_tyvar tv
+ | isTcTyVar tv
+ = case tcTyVarDetails tv of
+ SkolemTv {} -> qlzonk_kind_and_return tv
+ RuntimeUnk {} -> qlzonk_kind_and_return tv
+ MetaTv { mtv_ref = ref, mtv_tclvl = lvl, mtv_info = info }
+ -> do { cts <- readTcRef ref
+ ; case cts of
+ Indirect ty -> do { ty' <- qlZonkTcType ty
+ ; writeTcRef ref (Indirect ty')
+ -- See Note [Sharing in zonking]
+ ; return ty' }
+ Flexi | QLInstVar <- lvl
+ -> do { ty' <- monomorphiseQLInstTyVar tv info
+ ; writeTcRef ref (Indirect ty')
+ ; return ty' }
+ | otherwise
+ -> qlzonk_kind_and_return tv }
+
+ | otherwise -- coercion variable
+ = qlzonk_kind_and_return tv
+ where
+
+ qlzonk_kind_and_return :: TcTyVar -> ZonkM TcType
+ qlzonk_kind_and_return tv
+ = do { tv' <- qlzonk_tcv tv
+ ; return (mkTyVarTy tv') }
+
+monomorphiseQLInstTyVar :: TcTyVar -> MetaInfo -> ZonkM TcType
+-- Make a fresh ordinary unification variable, with the same
+-- Name and MetaInfo as the current one
+-- Precondition: the MetaInfo argument is that of the TcTyVar
+monomorphiseQLInstTyVar tv info
+ = do { ref <- newTcRef Flexi
+ ; lvl <- getZonkTcLevel
+ ; kind <- qlZonkTcType (tyVarKind tv)
+ ; let details = MetaTv {mtv_info = info, mtv_ref = ref, mtv_tclvl = lvl }
+ new_tv = mkTcTyVar (tyVarName tv) kind details
+ ; return (mkTyVarTy new_tv) }
+
-- For unbound, mutable tyvars, zonkType uses the function given to it
-- For tyvars bound at a for-all, zonkType zonks them to an immutable
-- type variable and zonks the kind too
@@ -209,25 +282,25 @@ zonkTcTypes :: [TcType] -> ZonkM [TcType]
zonkCo :: Coercion -> ZonkM Coercion
(zonkTcType, zonkTcTypes, zonkCo, _)
= mapTyCo zonkTcTypeMapper
-
--- | A suitable TyCoMapper for zonking a type during type-checking,
--- before all metavars are filled in.
-zonkTcTypeMapper :: TyCoMapper () ZonkM
-zonkTcTypeMapper = TyCoMapper
- { tcm_tyvar = const zonkTcTyVar
- , tcm_covar = const (\cv -> mkCoVarCo <$> zonkTyCoVarKind cv)
- , tcm_hole = hole
- , tcm_tycobinder = \ _env tcv _vis k -> zonkTyCoVarKind tcv >>= k ()
- , tcm_tycon = zonkTcTyCon }
where
- hole :: () -> CoercionHole -> ZonkM Coercion
- hole _ hole@(CoercionHole { ch_ref = ref, ch_co_var = cv })
- = do { contents <- readTcRef ref
- ; case contents of
- Just co -> do { co' <- zonkCo co
- ; checkCoercionHole cv co' }
- Nothing -> do { cv' <- zonkCoVar cv
- ; return $ HoleCo (hole { ch_co_var = cv' }) } }
+ -- | A suitable TyCoMapper for zonking a type during type-checking,
+ -- before all metavars are filled in.
+ zonkTcTypeMapper :: TyCoMapper () ZonkM
+ zonkTcTypeMapper = TyCoMapper
+ { tcm_tyvar = const zonkTcTyVar
+ , tcm_covar = const (\cv -> mkCoVarCo <$> zonkTyCoVarKind cv)
+ , tcm_hole = hole
+ , tcm_tycobinder = \ _env tcv _vis k -> zonkTyCoVarKind tcv >>= k ()
+ , tcm_tycon = zonkTcTyCon }
+ where
+ hole :: () -> CoercionHole -> ZonkM Coercion
+ hole _ hole@(CoercionHole { ch_ref = ref, ch_co_var = cv })
+ = do { contents <- readTcRef ref
+ ; case contents of
+ Just co -> do { co' <- zonkCo co
+ ; checkCoercionHole cv co' }
+ Nothing -> do { cv' <- zonkCoVar cv
+ ; return $ HoleCo (hole { ch_co_var = cv' }) } }
zonkTcTyCon :: TcTyCon -> ZonkM TcTyCon
-- Only called on TcTyCons
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1e1d4ee8770be56adb6229db4d7bf0fd974f8b7f
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1e1d4ee8770be56adb6229db4d7bf0fd974f8b7f
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/20240530/a3b90d7c/attachment-0001.html>
More information about the ghc-commits
mailing list