[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