[Git][ghc/ghc][wip/T24676] More comments in response to Richard

Simon Peyton Jones (@simonpj) gitlab at gitlab.haskell.org
Fri May 3 21:36:30 UTC 2024



Simon Peyton Jones pushed to branch wip/T24676 at Glasgow Haskell Compiler / GHC


Commits:
a17deb8a by Simon Peyton Jones at 2024-05-03T22:35:31+01:00
More comments in response to Richard

- - - - -


3 changed files:

- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Gen/Head.hs
- compiler/GHC/Tc/Utils/TcMType.hs


Changes:

=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -534,7 +534,7 @@ tcValArg do_ql (EValArgQL { eaql_status  = ql_status
        = return ()
     resume_ql_arg (QLIndependent delta wc) arg_rho
        = -- A tricky function!
-         -- See Note [Quick Look at value arguments] wrinkle (QLA4)
+         -- See Note [Quick Look at value arguments] wrinkle (QLA5)
          do { unless (isEmptyVarSet delta) $  -- Optimisation only
               do { demoteQLDelta delta
                  ; qlUnify delta arg_rho res_rho }
@@ -1565,18 +1565,19 @@ 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 `QLIndependent` case this was
+    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 ).  And so on recursively.  Key point: all these
+    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`.
 
-    When we resume typechecking the argument, we may now know that the arg is
-    a polytype.  E.g. suppose   f :: a -> [a], and we are checking that
+(QLA5) When we resume typechecking the argument (in the `EValArgQL` case of
+    `tcValArg`), we may now know that the arg is a polytype.
+     E.g. suppose   f :: a -> [a], and we are checking that
              f (g (h x)) :: [forall b. b->b]
     We will end up instantiating `f` at (forall b. b->b), and hence we need to
     check    (g (h x)) :: forall b. b -> b
@@ -1587,9 +1588,33 @@ This turned out to be more subtle than I expected.  Wrinkles:
     so we must instantiate g with type variables whose level numbers are inside
     the skolemise.
 
-    We call `demoteQLDelta` to do this. The demotion seems right but is not very
-    beautiful; e.g. `demoteDeltaTyVarTo` deliberately disobeys a sanity check
-    otherwise enforced by writeMetaTyVar.
+    We call `demoteQLDelta` to do this. Demotion seems like an unusual thing to
+    do, and indeed we need to carefully avoid calling `writeMetaTyVar` in order
+    to skip the check that we never unify with a type at a deeper level. But
+    the key insight is this:
+
+         We should think of instantiation variables
+         as not having a level number at all.
+
+    They don't need a level number (see next para), and in fact only have one
+    because we use normal unification variables as instantiation variables for
+    convenience. So `demoteQLDelta` should really be seen as creating fresh
+    unification variables (at the current, correct level), and then
+    substituting the instantiation variables to these fresh unification
+    variables.  So it's not really a demotion at all, but rather a substitution
+    from unleveled instantiation variables to fresh, leveled, unification
+    variables.
+
+(QLA6) Why do instantiation variables not need a level? Because their lifetime is
+    short; see Note [Instantiation variables are short lived].  They must /all/
+    be substituted by types (possibly with regular unification variables) before
+    we are done.  Now, it happens that a very common case is that we want to substitute
+    an instantiate variable with a fresh unification variable at the same level as
+    the original `tcApp` call.
+
+    By using a (levelled) unification variable as the implementation for an
+    (unlevelled) instantiation variable, we can make this common case into a
+    no-op; see the `when` short-cut in `demoteQLDelta`.
 -}
 
 quickLookArg :: Delta
@@ -1700,7 +1725,7 @@ quickLookArg1 guarded delta ctxt larg@(L _ arg) sc_arg_ty@(Scaled _ arg_ty)
                  ; qlUnify delta' arg_ty app_res_rho
                  ; emitConstraints wanted
                  ; traceTc "quickLookArg unify" (ppr rn_fun <+> ppr delta')
-                 ; return (delta', mk_ql_arg QLUnified) }
+                 ; return (delta', mk_ql_arg QLUnified) }o
 
          else -- Argument does not influence the enclosing call.
               -- So we treat this argument entirely independently:
@@ -1770,7 +1795,8 @@ which has no free instantiation variables, so we can QL-unify
 
 ---------------------
 qlUnify :: Delta -> TcType -> TcType -> TcM ()
--- Unify ty1 with ty2, unifying only variables in delta
+-- 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
 qlUnify delta ty1 ty2
   = assertPpr (not (isEmptyVarSet delta)) (ppr delta $$ ppr ty1 $$ ppr ty2) $


=====================================
compiler/GHC/Tc/Gen/Head.hs
=====================================
@@ -113,9 +113,8 @@ is a very local type, used only within this module and GHC.Tc.Gen.App
       The result of splitHsApps, which decomposes a HsExpr GhcRn
 
   - HsExprArg TcpInst:
-      The result of tcInstFun, which instantiates the function type
-      Adds EWrap nodes, the argument type in EValArg,
-      and the kind-checked type in ETypeArg
+      The result of tcInstFun, which instantiates the function type,
+      perhaps taking a quick look at arguments.
 
   - HsExprArg TcpTc:
       The result of tcArg, which typechecks the value args
@@ -124,19 +123,6 @@ is a very local type, used only within this module and GHC.Tc.Gen.App
 * rebuildPrefixApps is dual to splitHsApps, and zips an application
   back into a HsExpr
 
-Note [EValArg]
-~~~~~~~~~~~~~~
-The data type EValArg is the payload of the EValArg constructor of
-HsExprArg; i.e. a value argument of the application.  EValArg has two
-forms:
-
-* ValArg: payload is just the expression itself. Simple.
-
-* ValArgQL: captures the results of applying quickLookArg to the
-  argument in a ValArg.  When we later want to typecheck that argument
-  we can just carry on from where quick-look left off.  The fields of
-  ValArgQL exactly capture what is needed to complete the job.
-
 Invariants:
 
 1. With QL switched off, all arguments are ValArg; no ValArgQL
@@ -145,6 +131,17 @@ Invariants:
    under the conditions when quick-look should happen (eg the argument
    type is guarded) -- see quickLookArg
 
+Note [EValArgQL]
+~~~~~~~~~~~~~~~~
+Data constructor EValArgQL represents an argument that has been
+partly-type-checked by Quick Look: the first part of `tcApp` has been
+done, but not the second, `finishApp` part.
+
+The constuctor captures all the bits and pieces needed to complete
+typechecking.  (An alternative would to to store a function closure,
+but that's less concrete.)  See Note [Quick Look at value arguments]
+in GHC.Tc.Gen.App
+
 Note [splitHsApps]
 ~~~~~~~~~~~~~~~~~~
 The key function
@@ -176,17 +173,14 @@ type Delta = TcTyVarSet   -- Set of instantiation variables,
 
 data HsExprArg (p :: TcPass) where -- See Note [HsExprArg]
 
-  -- See Note [EValArg]
+  -- Data constructor EValArg represents a value argument
   EValArg :: { ea_ctxt   :: AppCtxt
              , ea_arg_ty :: !(XEVAType p)
              , ea_arg    :: LHsExpr (GhcPass (XPass p)) }
           -> HsExprArg p
 
-  -- This data constructor reprsents an argument that has been partly-type-checked;
-  -- The first part of `tcApp` has been done, but not the second, `finishApp` part.
-  -- The constuctor captures all the bits and pieces needed to complete typechecking.
-  -- (An alternative would to to store a function closure, but that's less concrete.)
-  -- See Note [Quick Look at value arguments] in GHC.Tc.Gen.App
+  -- Data constructor EValArgQL represents an argument that has been
+  -- partly-type-checked by Quick Look; see Note [EValArgQL]
   EValArgQL :: { eaql_status  :: QLArgStatus
                , eaql_ctxt    :: AppCtxt
                , eaql_arg_ty  :: Scaled TcSigmaType  -- Argument type expected by function


=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -2464,7 +2464,7 @@ demoteDeltaTyVarTo new_lvl tv
   = pprPanic "demoteDeltaTyVarTo" (ppr tv)
 
 demoteQLDelta :: TcTyVarSet -> TcM ()
--- See Note [Quick Look at value arguments] wrinkle (QLA4)
+-- See Note [Quick Look at value arguments] wrinkle (QLA5)
 --     in GHC.Tc.Gen.App
 demoteQLDelta delta
   = case tvs of
@@ -2472,6 +2472,9 @@ demoteQLDelta delta
       (tv1:_) -> do { tclvl <- getTcLevel
                     ; assertPpr (isMetaTyVar tv1) (ppr delta) $
                       when (tclvl `strictlyDeeperThan` tcTyVarLevel tv1) $
+                      -- This 'when' is just an optimisation
+                      -- See (QLA6) in Note [Quick Look at value arguments]
+                      -- in GHC.Tc.Gen.App.
                       mapM_ (demoteDeltaTyVarTo tclvl) tvs }
   where
     tvs = nonDetEltsUniqSet delta



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/a17deb8a491f23ff538e3b801429f81a8f2c7417

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/a17deb8a491f23ff538e3b801429f81a8f2c7417
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/20240503/61367e4e/attachment-0001.html>


More information about the ghc-commits mailing list