[Git][ghc/ghc][wip/T24676] Add notes
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Mon Jun 3 19:05:48 UTC 2024
Simon Peyton Jones pushed to branch wip/T24676 at Glasgow Haskell Compiler / GHC
Commits:
6d030891 by Simon Peyton Jones at 2024-06-03T20:05:17+01:00
Add notes
- - - - -
3 changed files:
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Zonk/TcType.hs
Changes:
=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -82,8 +82,8 @@ import GHC.Prelude
* *
********************************************************************* -}
-{- Note [Quick Look]
-~~~~~~~~~~~~~~~~~~~~
+{- Note [Quick Look overview]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The implementation of Quick Look closely follows the QL paper
A quick look at impredicativity, Serrano et al, ICFP 2020
https://www.microsoft.com/en-us/research/publication/a-quick-look-at-impredicativity/
@@ -121,6 +121,7 @@ Note [Instantiation variables are short lived]
* 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 also Note [QuickLook zonking] in GHC.Tc.Zonk.TcType
See Section 4.3 "Applications and instantiation" of the paper.
@@ -396,6 +397,7 @@ finishApp :: QLFlag -> HsExpr GhcRn
-> TcM (HsExpr GhcTc)
finishApp do_ql rn_expr tc_head@(tc_fun,_) inst_args app_res_rho exp_res_ty
= do { -- Step 6: qlZonk the type of the result of the call
+ -- See Note [QuickLook zonking] in GHC.Tc.Zonk.TcType
traceTc "finishApp" $ vcat [ ppr app_res_rho, ppr exp_res_ty ]
; app_res_rho <- case do_ql of
DoQL -> liftZonkM $ qlZonkTcType app_res_rho
@@ -508,6 +510,7 @@ 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]
+ -- and Note [QuickLook zonking] in GHC.Tc.Zonk.TcType
; Scaled mult exp_arg_ty <- case do_ql of
DoQL -> liftZonkM $ qlZonkScaledTcType sc_arg_ty
NoQL -> return sc_arg_ty
@@ -540,9 +543,15 @@ tcValArg _ (EValArgQL { eaql_wanted = wanted
; (wrap, arg')
<- tcScalingUsage mult $
tcSkolemise ds_flag GenSigCtxt exp_arg_ty $ \ exp_arg_rho ->
- do { emitConstraints wanted
+ do { -- Emit saved-up constraints, /under/ the tcSkolemise
+ -- See (QLA4) in Note [Quick Look at value arguments]
+ emitConstraints wanted
+
+ -- Unify with context if we have no already done so
+ -- See (QLA4) in Note [Quick Look at value arguments]
; unless arg_influences_enclosing_call $ -- Don't repeat
qlUnify app_res_rho exp_arg_rho -- the qlUnify
+
; finishApp DoQL rn_expr tc_head inst_args
app_res_rho (mkCheckExpType exp_arg_rho) }
@@ -764,7 +773,7 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args
-- Fill in kappa := nu_1 -> .. -> nu_n -> res_nu
-- NB: kappa is uninstantiated ('go' already checked that)
; kind_co <- unifyKind Nothing liftedTypeKind (tyVarKind kappa)
- -- unifyKind: see (UQL3) in Note [Actual unification during QuickLook]
+ -- unifyKind: see (UQL3) in Note [QuickLook unification]
; liftZonkM (writeMetaTyVar kappa (mkCastTy fun_ty' kind_co))
; let co_wrap = mkWpCastN (mkGReflLeftCo Nominal fun_ty' kind_co)
@@ -1561,59 +1570,18 @@ This turned out to be more subtle than I expected. Wrinkles:
(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,
+ - 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`.
+
+ - quickLookArg may or may not have done `qlUnify` with the calling context.
+ If not (eaql_encl = False) must do so now. Example: choose [] ids,
where ids :: [forall a. a->a]
choose :: a -> a -> a
We instantiate choose with `kappa` and discover from `ids` that
(kappa = [forall a. a->a]). Now we resume typechecking argument [], and
we must take advantage of what we have now discovered about `kappa`,
to typecheck [] :: [forall a. a->a]
-
- - 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`.
-
-(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
- The `tcSkolemise` in `tcValArg` for EValArgQL skolemises that forall b; but
- we are now at a deeper level, and those carefully-preserved kappas are from
- the /outer/ level. We want it to be /as if/ we had always known that we were
- checking (g (h x)) :: forall b. b -> b
- so we must instantiate g with type variables whose level numbers are inside
- the skolemise.
-
- 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 :: QLFlag -> AppCtxt
@@ -1743,64 +1711,18 @@ quickLookArg1 ctxt larg@(L _ arg) sc_arg_ty@(Scaled _ orig_arg_rho)
* *
********************************************************************* -}
-{- Note [Monomorphise instantiation variables]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-`monomorphiseQLInstVars` turns /instantiation/ variables into regular
-/unification/ variables. It does so by looking at the arguments and
-result type of the call, seaching for free instatiation variables.
-This is the lower-case 'theta' (a mono-substitution) in the APP-DOWN rule
-of Fig 5 of the Quick Look paper.
-
-(MIV1) When monomorphising an instantiation variable, don't forget to
- monomorphise its kind. It might have type (a :: TYPE k), where both
- `a` and `k` are instantiation variables.
-
-(MIV2) In `qlUnify`, `make_kinds_ok` may unify
- a :: k1 ~ b :: k2
- making a cast
- a := b |> (co :: k1 ~ k2)
- But now suppose k1 is an instantiation variable. Then that coercion hole
- `co` is the only place that `k1` will show up in the traversal, and yet
- we want to monomrphise it. Hence the do_hole in `foldQLInstTyVars`
-
--}
-
-{-
-monomorphiseQLInstVars :: [HsExprArg 'TcpInst] -> TcRhoType -> TcM ()
-monomorphiseQLInstVars inst_args res_rho
- = do { traceTc "monomorphiseQLInstVars {" $
- vcat [ text "inst_args:" <+> vcat (map pprArgInst inst_args)
- , text "res_rho:" <+> ppr res_rho ]
- ; go_val_arg_ql inst_args res_rho
- ; traceTc "monomorphiseQLInstVars }" empty }
- where
- go_val_arg_ql :: [HsExprArg 'TcpInst] -> TcRhoType -> TcM ()
- go_val_arg_ql inst_args rho = do { mapM_ go_arg inst_args; go_ty rho }
-
- go_arg :: HsExprArg 'TcpInst -> TcM ()
- go_arg (EValArg { ea_arg_ty = arg_ty }) = go_ty (scaledThing arg_ty)
- go_arg (EValArgQL { eaql_arg_ty = arg_ty }) = go_ty (scaledThing arg_ty)
- go_arg _ = return ()
-
- go_ty :: TcType -> TcM ()
- go_ty ty = unTcMUnit (foldQLInstVars go_tv ty)
-
- go_tv :: TcTyVar -> TcMUnit
- go_tv tv = assertPpr (isQLInstTyVar tv) (ppr tv) $
- TCMU $ do { traceTc "momomorphiseQLInstVar" (ppr tv)
- ; info <- readMetaTyVar tv
- ; case info of
- Indirect ty -> go_ty ty
- Flexi -> do { go_ty (tyVarKind tv)
- ; monomorphiseQLInstVar tv } }
- -- For the tyVarKind see (MIV1) in Note [Monomorphise instantiation variables]
-
-
-newtype TcMUnit = TCMU { unTcMUnit :: TcM () }
-instance Semigroup TcMUnit where
- TCMU ml <> TCMU mr = TCMU (ml >> mr)
-instance Monoid TcMUnit where
- mempty = TCMU (return ())
+{- Note [The fiv test in quickLookArg]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In rule APP-lightning-bolt in Fig 5 of the paper, we have to test rho_r
+for having no free instantiation variables. We do this in Step 3 of quickLookArg1,
+using anyFreeKappa. Example:
+ Suppose ids :: [forall a. a->a]
+ and consider Just (ids++ids)
+We will instantiate Just with kappa, say, and then call
+ quickLookArg1 False {kappa} (ids ++ ids) kappa
+The call to tcInstFun will return with app_res_rho = [forall a. a->a]
+which has no free instantiation variables, so we can QL-unify
+ kappa ~ [Forall a. a->a]
-}
anyFreeKappa :: TcType -> TcM Bool
@@ -1841,22 +1763,12 @@ foldQLInstVars check_tv ty
do_tv _ tv | isQLInstTyVar tv = check_tv tv
| otherwise = mempty
-----------------
-{- Note [The fiv test in quickLookArg]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-In rule APP-lightning-bolt in Fig 5 of the paper, we have to test rho_r
-for having no free instantiation variables. We do this in Step 3 of quickLookArg1,
-using anyFreeKappa. Example:
- Suppose ids :: [forall a. a->a]
- and consider Just (ids++ids)
-We will instantiate Just with kappa, say, and then call
- quickLookArg1 False {kappa} (ids ++ ids) kappa
-The call to tcInstFun will return with app_res_rho = [forall a. a->a]
-which has no free instantiation variables, so we can QL-unify
- kappa ~ [Forall a. a->a]
--}
+{- *********************************************************************
+* *
+ QuickLook unification
+* *
+********************************************************************* -}
----------------------
qlUnify :: TcType -> TcType -> TcM ()
-- Unify ty1 with ty2:
-- * It unifies /only/ instantiation variables;
@@ -1876,7 +1788,8 @@ qlUnify ty1 ty2
-- for the corresponding type. Don't unify with these.
go bvs (TyVarTy tv) ty2
| isQLInstTyVar tv = go_kappa bvs tv ty2
-
+ -- Only unify QL instantiation variables
+ -- See (UQL3) in Note [QuickLook unification]
go (bvs1, bvs2) ty1 (TyVarTy tv)
| isQLInstTyVar tv = go_kappa (bvs2,bvs1) tv ty1
@@ -1950,7 +1863,7 @@ qlUnify ty1 ty2
= go_flexi1 bvs kappa ty2
go_flexi1 (_,bvs2) kappa ty2 -- ty2 is zonked
- | -- See Note [Actual unification during QuickLook] (UQL1)
+ | -- See Note [QuickLook unification] (UQL1)
let ty2_tvs = shallowTyCoVarsOfType ty2
, not (ty2_tvs `intersectsVarSet` bvs2)
-- Can't instantiate a delta-var to a forall-bound variable
@@ -1958,55 +1871,21 @@ qlUnify ty1 ty2
-- Passes the occurs check
, not (isConcreteTyVar kappa) || isConcreteType ty2
-- Don't unify a concrete instantiatiation variable with a non-concrete type
- = do { ty2' <- make_kinds_ok kappa ty2
+ = do { co <- unifyKind (Just (TypeThing ty2)) ty2_kind kappa_kind
+ -- unifyKind: see (UQL2) in Note [QuickLook unification]
+ ; let ty2' = mkCastTy ty2 co
; traceTc "qlUnify:update" $
ppr kappa <+> text ":=" <+> ppr ty2
; liftZonkM $ writeMetaTyVar kappa ty2' }
| otherwise
= return () -- Occurs-check or forall-bound variable
-
- make_kinds_ok :: TcTyVar -> TcType -> TcM TcType
- -- Don't call unifyKind! Instead try to make the kinds equal with
- -- unifyKind; and if that fails just emit an equality
- -- See Note [Actual unification during QuickLook] (UQL2)
- make_kinds_ok kappa ty2
- = do { co <- unifyKind (Just (TypeThing ty2)) ty2_kind kappa_kind
- -- unifyKind: see Note [Actual unification during QuickLook]
- ; return (mkCastTy ty2 co) }
where
kappa_kind = tyVarKind kappa
ty2_kind = typeKind ty2
-{-
- | kind1 `tcEqType` kind2
- = return ty2
- | otherwise
- = do { qlUnify kind1 kind2
- ; (kind1, kind2) <- liftZonkM $
- do { kind1 <- zonkTcType kind1
- ; kind2 <- zonkTcType kind2
- ; return (kind1, kind2) }
- ; if (kind1 `tcEqType` kind2)
- then return ty2
- else
- do { co <- emitWantedEq orig KindLevel Nominal kind2 kind1
- ; traceTc "make_kinds_ok" $
- vcat [ hang (ppr kappa <+> dcolon <+> ppr kind1 <+> text ":=")
- 2 (ppr ty2 <+> dcolon <+> ppr kind2)
- , text "co:" <+> ppr co ]
- ; return (mkCastTy ty2 co) } }
- where
- kind1 = tyVarKind kappa
- kind2 = typeKind ty2
- orig = TypeEqOrigin { uo_actual = kind2
- , uo_expected = kind1
- , uo_thing = Just (TypeThing ty2)
- , uo_visible = True }
--}
-
-{- Note [Actual unification during QuickLook]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [QuickLook unification]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In qlUnify, if we find (kappa ~ ty), we are going to update kappa := ty.
That is the entire point of qlUnify! Wrinkles:
@@ -2028,38 +1907,30 @@ That is the entire point of qlUnify! Wrinkles:
- type families; relates to a very specific and exotic performance
question, that is unlikely to bite here
-(UQL2) What if kappa and ty have different kinds? So we:
- * Check to see if the kinds are already the same
- * If not, use qlUnify to unify them, and
- * Then check again for equality
- We insist on actual equality, without any casts. The whole point of
+(UQL2) What if kappa and ty have different kinds? We simply call the
+ ordinary unifier and use the coercion to connect the two.
+
+ If that coercion is not Refl, it is all in vain: The whole point of
qlUnify is to impredicatively unify (kappa := forall a. blah). It is
no good to unify (kappa := (forall a.blah) |> co) because we can't
use that casted polytype.
- There is a small worry that we might have
- qlUnify( (kappa :: alpha), (forall a. a->a :: Type) )
- where `alpha` is a regular unification variable, not an instantiation
- variable; so qlUnify won't unify it, and hence won't unify `kappa`.
- But maybe `alpha` turns out to be Type anyway, so it'd be fine. But
- we are very wary about unifying non-instantiation variables here; see
- wrinkle (UQL3). So there is a remote danger of order dependence; whether
- Quick Look succeeds depends on when `alpha` gets unified.
+ BUT: the kind-unifer has emitted constraint(s) so we may as well use
+ them. (An alternative; use uType directly, and discard constraints
+ if the result is not Refl.)
(UQL3) qlUnify (and Quick Look generally) is very careful only to unify
instantiation variables, not regular unification variables. Why?
Because instantiation variables don't really have a settled level yet;
- see Note [Quick Look at value arguments] wrinkle (QLA6). So we should be
- worried that we might unify
- alpha[1] := Maybe kappa[??]
+ they have level QLInstVar (see Note [The QLInstVar TcLevel] in GHC.Tc.Utils.TcType.
+ So we should be worried that we might unify
+ alpha[1] := Maybe kappa[qlinst]
and later this kappa turns out to be a level-2 variable, and we have committed
a skolem-escape error. Boo!
- Solution: Quick Look only unifies instantiation variables.
-
- Small exception: In the IVAR rule we want (tyVarKind kappa ~ liftedTypeKind),
- and that cannot possibly cause skolem escape, so do allow regular unification
- for this case, via the call to `unifyKind`.
+ Solution: Quick Look only unifies instantiation variables, and the regular
+ unifier wont' do this unification because QL instantiation variables have
+ level infinity.
-}
{- *********************************************************************
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -699,6 +699,7 @@ data TcLevel = TcLevel Int#
| QLInstVar
-- See Note [TcLevel invariants] for what this Int is
-- See also Note [TcLevel assignment]
+ -- See also Note [The TcLevel QLInstVar]
{-
Note [TcLevel invariants]
@@ -733,14 +734,35 @@ Note [TcLevel invariants]
The level of a MetaTyVar also governs its untouchability. See
Note [Unification preconditions] in GHC.Tc.Utils.Unify.
+ -- See also Note [The TcLevel QLInstVar]
+
Note [TcLevel assignment]
~~~~~~~~~~~~~~~~~~~~~~~~~
We arrange the TcLevels like this
- 0 Top level
- 1 First-level implication constraints
- 2 Second-level implication constraints
+ 0 Top level
+ 1 First-level implication constraints
+ 2 Second-level implication constraints
...etc...
+ QLInstVar The level for QuickLook instantiation variables
+ See Note [The QLInstVar TcLevel]
+
+Note [The QLInstVar TcLevel]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+QuickLook instantiation variables are identified by having a TcLevel
+of QLInstVar. See Note [Quick Look overview] in GHC.Tc.Gen.App.
+
+The QLInstVar level behaves like infinity: it is greater than any
+other TcLevel. See `strictlyDeeperThan` and friends in this module.
+That ensures that we never unify an ordinary unification variable
+with a QL instantiation variable, e.g.
+ alpha[tau:3] := Maybe beta[tau:qlinstvar]
+(This is an immediate consequence of our general rule that we never
+unify a variable with a type mentioning deeper variables; the skolem
+escape check.
+
+QL instantation variables are eventually turned into ordinary unificaiton
+variables; see (QL3) in Note [Quick Look overview].
Note [GivenInv]
~~~~~~~~~~~~~~~
@@ -818,12 +840,14 @@ pushTcLevel (TcLevel us) = TcLevel (us +# 1#)
pushTcLevel QLInstVar = QLInstVar
strictlyDeeperThan :: TcLevel -> TcLevel -> Bool
+-- See Note [The QLInstVar TcLevel]
strictlyDeeperThan (TcLevel tv_tclvl) (TcLevel ctxt_tclvl)
= isTrue# (tv_tclvl ># ctxt_tclvl)
strictlyDeeperThan QLInstVar (TcLevel {}) = True
strictlyDeeperThan _ _ = False
deeperThanOrSame :: TcLevel -> TcLevel -> Bool
+-- See Note [The QLInstVar TcLevel]
deeperThanOrSame (TcLevel tv_tclvl) (TcLevel ctxt_tclvl)
= isTrue# (tv_tclvl >=# ctxt_tclvl)
deeperThanOrSame (TcLevel {}) QLInstVar = False
=====================================
compiler/GHC/Tc/Zonk/TcType.hs
=====================================
@@ -199,17 +199,35 @@ See for example test T5631, which regresses without this change.
{-
************************************************************************
* *
- Zonking -- the main work-horses: zonkTcType, zonkTcTyVar
+ QuickLook zonking
* *
************************************************************************
-}
+{- Note [QuickLook zonking]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When we are done with the QuickLook, we must
+* Expose the polytypes hidden inside now-unified instantiation
+ variables, by zonking the types involved.
+* Turn any still-un-unified QL instantiation variables into regular
+ unification variables, with a now-known level.
+
+These tasks are performed simultaneously by `qlZonkTcType`. It behaves very
+similarly to the regular `zonkTcType`, except that /in addition/ it turns any
+un-filled-in instantiation variable kappa into a monotype, using
+`monomorphiseQLInstVar`. The latter creates a fresh unification variable, say
+alpha[lvl], and unifiying kappa := alpha.
+
+It is very simple and satisfying that the two tasks can be done as one.
+-}
+
qlZonkScaledTcType :: Scaled TcType -> ZonkM (Scaled TcType)
qlZonkScaledTcType (Scaled m ty)
= Scaled <$> qlZonkTcType m <*> qlZonkTcType ty
qlZonkTcType :: TcType -> ZonkM TcType
qlZonkCo :: Coercion -> ZonkM Coercion
+-- See Note [QuickLook zonking]
(qlZonkTcType, _, qlZonkCo, _)
= mapTyCo mapper
where
@@ -274,6 +292,15 @@ monomorphiseQLInstTyVar tv info
new_tv = mkTcTyVar (tyVarName tv) kind details
; return (mkTyVarTy new_tv) }
+
+{-
+************************************************************************
+* *
+ Zonking -- the main work-horses: zonkTcType, zonkTcTyVar
+* *
+************************************************************************
+-}
+
-- 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
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6d030891a12aa0a8af4afea64d142dcde956b5e9
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6d030891a12aa0a8af4afea64d142dcde956b5e9
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/20240603/c7ed0b0f/attachment-0001.html>
More information about the ghc-commits
mailing list