[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