[Git][ghc/ghc][wip/T24676] Respond to Richard's review
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Thu Jun 6 23:18:24 UTC 2024
Simon Peyton Jones pushed to branch wip/T24676 at Glasgow Haskell Compiler / GHC
Commits:
6afa552f by Simon Peyton Jones at 2024-06-07T00:18:05+01:00
Respond to Richard's review
- - - - -
4 changed files:
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Utils/Instantiate.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- compiler/GHC/Tc/Utils/TcType.hs
Changes:
=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -43,7 +43,6 @@ import GHC.Core.DataCon ( dataConConcreteTyVars, isNewDataCon, dataConTyCon )
import GHC.Core.TyCon
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Ppr
-import GHC.Core.TyCo.FVs ( shallowTyCoVarsOfType )
import GHC.Core.TyCo.Subst ( substTyWithInScope )
import GHC.Core.Type
import GHC.Core.Coercion
@@ -58,7 +57,6 @@ import GHC.Types.Name.Env
import GHC.Types.Name.Reader
import GHC.Types.SrcLoc
import GHC.Types.Var.Env ( emptyTidyEnv, mkInScopeSet )
-import GHC.Types.Var.Set
import GHC.Data.Maybe
@@ -103,7 +101,7 @@ Some notes relative to the paper
(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
+ revealing all the polytypes), and updates any instantiation variables with
ordinary unification variables.
See Note [Instantiation variables are short lived].
@@ -118,9 +116,11 @@ Note [Instantiation variables are short lived]
* 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 `zonkTcType` (see "Crucial step" in tcValArgs).
-
+* When we start typechecking the argments of the call, in tcValArgs, we will
+ (a) monomorphise any un-filled-in instantiation variables
+ (see Note [Monomorphise instantiation variables])
+ (b) zonk the argument type to reveal any polytypes before typechecking that
+ argument (see calls to `zonkTcType` and "Crucial step" in tcValArg)..
See Section 4.3 "Applications and instantiation" of the paper.
* The constraint solver never sees an instantiation variable [not quite true;
@@ -522,6 +522,7 @@ tcValArg _ (EPrag l p) = return (EPrag l (tcExprPrag p))
tcValArg _ (ETypeArg l hty ty) = return (ETypeArg l hty ty)
tcValArg do_ql (EWrap (EHsWrap w)) = do { whenQL do_ql $ qlMonoHsWrapper w
; return (EWrap (EHsWrap w)) }
+ -- qlMonoHsWrapper: see Note [Monomorphise instantiation variables]
tcValArg _ (EWrap ew) = return (EWrap ew)
tcValArg do_ql (EValArg { ea_ctxt = ctxt
@@ -608,17 +609,6 @@ 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
--}
-
{- *********************************************************************
* *
Instantiating the call
@@ -1576,7 +1566,7 @@ This turned out to be more subtle than I expected. Wrinkles:
quick-look-arg judgement APP-QL are satisfied; this is captured in
`arg_influences_enclosing_call`.
-(QLA1) We avoid zonking, so the `arg_influences_enclosing_call` sees the
+(QLA2) 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`.
@@ -1598,7 +1588,13 @@ 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`.
+ now emit them with `emitConstraints`. This must be done /under/ the skolemisation
+ of the argument's type (see `tcSkolemise` in `tcValArg` for EValArgQL { ...}.
+ Example: f :: (forall b. Ord b => b -> b -> Bool) -> ...
+ Call: f (==)
+ we must skolemise the argument type (forall b. Ord b => b -> b -> Bool)
+ before emitting the [W] Eq alpha constraint arising from the call to (==).
+ It will be solved from the Ord b!
- quickLookArg may or may not have done `qlUnify` with the calling context.
If not (eaql_encl = False) must do so now. Example: choose [] ids,
@@ -1753,6 +1749,11 @@ See `qlMonoHsWrapper`.
By going left to right, we are sure to monomorphise instantiation variables
before we encounter them in an argument type (in `tcValArg`).
+All instantiation variables for a call will be reachable from the type(s)
+at which the function is instantiated -- i.e. those WpTyApps. Even instantiation
+variables allocoated by tcInstFun itself, such as in the IRESULT rule, end up
+connected to the original type(s) at which the function is instantiated.
+
To monomorphise the free QL instantiation variables of a type, we use
`foldQLInstVars`.
@@ -1772,11 +1773,13 @@ Wrinkles:
-}
qlMonoHsWrapper :: HsWrapper -> ZonkM ()
+-- See Note [Monomorphise instantiation variables]
qlMonoHsWrapper (WpCompose w1 w2) = qlMonoHsWrapper w1 >> qlMonoHsWrapper w2
qlMonoHsWrapper (WpTyApp ty) = qlMonoTcType ty
qlMonoHsWrapper _ = return ()
qlMonoTcType :: TcType -> ZonkM ()
+-- See Note [Monomorphise instantiation variables]
qlMonoTcType ty
= do { traceZonk "monomorphiseQLInstVars {" (ppr ty)
; go_ty ty
@@ -1856,6 +1859,7 @@ foldQLInstVars check_tv ty
folder :: TyCoFolder () a
folder = TyCoFolder { tcf_view = noView -- See Note [Free vars and synonyms]
+ -- in GHC.Core.TyCo.FVs
, tcf_tyvar = do_tv, tcf_covar = mempty
, tcf_hole = do_hole, tcf_tycobinder = do_bndr }
@@ -1876,106 +1880,98 @@ foldQLInstVars check_tv ty
qlUnify :: TcType -> TcType -> TcM ()
-- Unify ty1 with ty2:
--- * It unifies /only/ instantiation variables;
--- it /never/ unifies ordinary unification variables
+-- * It unifies /only/ instantiation variables.
+-- It does not itself unify ordinary unification variables,
+-- although it calls unifyKind which can do so. (It'd be ok for it to
+-- unify ordinary unification variables, subject to the usual checks.)
-- * It never produces errors, even for mis-matched types
-- * It does not return a coercion (unlike unifyType); it is called
-- for the sole purpose of unifying instantiation variables
-- * It may return without having made the argument types equal, of course;
-- it just makes best efforts.
qlUnify ty1 ty2
- = go (emptyVarSet,emptyVarSet) ty1 ty2
+ = go ty1 ty2
where
- go :: (TyVarSet, TcTyVarSet)
- -> TcType -> TcType
+ go :: TcType -> TcType
-> TcM ()
-- The TyVarSets give the variables bound by enclosing foralls
-- for the corresponding type. Don't unify with these.
- go bvs (TyVarTy tv) ty2
- | isQLInstTyVar tv = go_kappa bvs tv ty2
+ go (TyVarTy tv) ty2
+ | isQLInstTyVar tv = go_kappa 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
+ go ty1 (TyVarTy tv)
+ | isQLInstTyVar tv = go_kappa tv ty1
- go bvs (CastTy ty1 _) ty2 = go bvs ty1 ty2
- go bvs ty1 (CastTy ty2 _) = go bvs ty1 ty2
+ go (CastTy ty1 _) ty2 = go ty1 ty2
+ go ty1 (CastTy ty2 _) = go ty1 ty2
- go _ (TyConApp tc1 []) (TyConApp tc2 [])
+ go (TyConApp tc1 []) (TyConApp tc2 [])
| tc1 == tc2 -- See GHC.Tc.Utils.Unify
= return () -- Note [Expanding synonyms during unification]
-- Now, and only now, expand synonyms
- go bvs rho1 rho2
- | Just rho1 <- coreView rho1 = go bvs rho1 rho2
- | Just rho2 <- coreView rho2 = go bvs rho1 rho2
+ go rho1 rho2
+ | Just rho1 <- coreView rho1 = go rho1 rho2
+ | Just rho2 <- coreView rho2 = go rho1 rho2
- go bvs (TyConApp tc1 tys1) (TyConApp tc2 tys2)
+ go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
| tc1 == tc2
, not (isTypeFamilyTyCon tc1)
, tys1 `equalLength` tys2
- = zipWithM_ (go bvs) tys1 tys2
+ = zipWithM_ go tys1 tys2
-- Decompose (arg1 -> res1) ~ (arg2 -> res2)
-- and (c1 => res1) ~ (c2 => res2)
-- But for the latter we only learn instantiation info from res1~res2
-- We look at the multiplicity too, although the chances of getting
-- impredicative instantiation info from there seems...remote.
- go bvs (FunTy { ft_af = af1, ft_arg = arg1, ft_res = res1, ft_mult = mult1 })
- (FunTy { ft_af = af2, ft_arg = arg2, ft_res = res2, ft_mult = mult2 })
+ go (FunTy { ft_af = af1, ft_arg = arg1, ft_res = res1, ft_mult = mult1 })
+ (FunTy { ft_af = af2, ft_arg = arg2, ft_res = res2, ft_mult = mult2 })
| af1 == af2 -- Match the arrow TyCon
- = do { when (isVisibleFunArg af1) (go bvs arg1 arg2)
- ; when (isFUNArg af1) (go bvs mult1 mult2)
- ; go bvs res1 res2 }
+ = do { when (isVisibleFunArg af1) (go arg1 arg2)
+ ; when (isFUNArg af1) (go mult1 mult2)
+ ; go res1 res2 }
-- ToDo: c.f. Tc.Utils.unify.uType,
-- which does not split FunTy here
-- Also NB tcSplitAppTyNoView here, which does not split (c => t)
- go bvs (AppTy t1a t1b) ty2
+ go (AppTy t1a t1b) ty2
| Just (t2a, t2b) <- tcSplitAppTyNoView_maybe ty2
- = do { go bvs t1a t2a; go bvs t1b t2b }
+ = do { go t1a t2a; go t1b t2b }
- go bvs ty1 (AppTy t2a t2b)
+ go ty1 (AppTy t2a t2b)
| Just (t1a, t1b) <- tcSplitAppTyNoView_maybe ty1
- = do { go bvs t1a t2a; go bvs t1b t2b }
-
- go (bvs1, bvs2) (ForAllTy bv1 ty1) (ForAllTy bv2 ty2)
- = go (bvs1',bvs2') ty1 ty2
- where
- bvs1' = bvs1 `extendVarSet` binderVar bv1
- bvs2' = bvs2 `extendVarSet` binderVar bv2
+ = do { go t1a t2a; go t1b t2b }
- go _ _ _ = return ()
+ go _ _ = return ()
----------------
- go_kappa bvs kappa ty2
+ go_kappa kappa ty2
= assertPpr (isMetaTyVar kappa) (ppr kappa) $
do { info <- readMetaTyVar kappa
; case info of
- Indirect ty1 -> go bvs ty1 ty2
+ Indirect ty1 -> go ty1 ty2
Flexi -> do { ty2 <- liftZonkM $ zonkTcType ty2
- ; go_flexi bvs kappa ty2 } }
+ ; go_flexi kappa ty2 } }
----------------
-- Swap (kappa1[conc] ~ kappa2[tau])
-- otherwise we'll fail to unify and emit a coercion.
-- Just an optimisation: emitting a coercion is fine
- go_flexi bvs kappa (TyVarTy tv2)
+ go_flexi kappa (TyVarTy tv2)
| isQLInstTyVar tv2, lhsPriority tv2 > lhsPriority kappa
- = go_flexi1 bvs tv2 (TyVarTy kappa)
- go_flexi bvs kappa ty2
- = go_flexi1 bvs kappa ty2
+ = go_flexi1 tv2 (TyVarTy kappa)
+ go_flexi kappa ty2
+ = go_flexi1 kappa ty2
- go_flexi1 (_,bvs2) kappa ty2 -- ty2 is zonked
+ go_flexi1 kappa ty2 -- ty2 is zonked
| -- 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
- , Just ty2 <- occCheckExpand [kappa] ty2
+ Just ty2 <- occCheckExpand [kappa] ty2
-- Passes the occurs check
, not (isConcreteTyVar kappa) || isConcreteType ty2
- -- Don't unify a concrete instantiatiation variable with a non-concrete type
+ -- Don't unify a concrete instantiation variable with a non-concrete type
= do { co <- unifyKind (Just (TypeThing ty2)) ty2_kind kappa_kind
-- unifyKind: see (UQL2) in Note [QuickLook unification]
; let ty2' = mkCastTy ty2 co
@@ -1997,9 +1993,6 @@ That is the entire point of qlUnify! Wrinkles:
(UQL1) Before unifying an instantiation variable in `go_flexi`, we must check
the usual unification conditions: see `GHC.Tc.Utils.Unify.simpleUnifyCheck`
In particular:
- * We must not unify with anything bound by an enclosing forall; e.g.
- (forall a. kappa -> Int) ~ forall a. a -> Int)
- That's tracked by the 'bvs' arg of 'go'.
* We must not make an occurs-check; we use occCheckExpand for that.
@@ -2020,12 +2013,15 @@ That is the entire point of qlUnify! Wrinkles:
no good to unify (kappa := (forall a.blah) |> co) because we can't
use that casted polytype.
- 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.)
+ BUT: unifyKind has emitted constraint(s) into the Tc monad, so we may as well
+ use them. (An alternative; use uType directly, if the result is not Refl,
+ discard the constraints and the coercion, and do not update the instantiation
+ variable.)
+
+(UQL3) qlUnify (and Quick Look generally) is only unifies instantiation
+ variables, not regular unification variables. Why? Nothing fundamental.
+ We would need to
-(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;
they have level QLInstVar (see Note [The QLInstVar TcLevel] in GHC.Tc.Utils.TcType.
So we should be worried that we might unify
=====================================
compiler/GHC/Tc/Utils/Instantiate.hs
=====================================
@@ -426,10 +426,12 @@ right here. But note
See Note [Let-bound skolems] in GHC.Tc.Solver.InertSet.
If we substitute aggressively (including zonking) that abbreviation could work. But
- again it affects what is typeable.
+ again it affects what is typeable. And we don't support equalities over polytypes,
+ currently, anyway.
* There is little point in trying to optimise for
- - (s ~# t), because few functions have primitive equalities in their context
+ - (s ~# t), because this has kind Constraint#, not Constraint, and so will not be
+ in the theta instantiated in instCalll
- (s ~~ t), becaues heterogeneous equality is rare, and more complicated.
Anyway, for now we don't take advantage of these potential effects.
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -80,7 +80,7 @@ module GHC.Tc.Utils.TcMType (
defaultTyVar, promoteMetaTyVarTo, promoteTyVarSet,
quantifyTyVars, isQuantifiableTv,
zonkAndSkolemise, skolemiseQuantifiedTyVar,
- doNotQuantifyTyVars, demoteQLDelta,
+ doNotQuantifyTyVars,
candidateQTyVarsOfType, candidateQTyVarsOfKind,
candidateQTyVarsOfTypes, candidateQTyVarsOfKinds,
@@ -2446,48 +2446,6 @@ promoteTyVarSet tvs
-- Non-determinism is OK because order of promotion doesn't matter
; return (or bools) }
-demoteDeltaTyVarTo :: TcLevel -> TcTyVar -> TcM ()
--- See Note [Quick Look at value arguments] wrinkle (QLA4)
--- in GHC.Tc.Gen.App
-demoteDeltaTyVarTo new_lvl tv
- | MetaTv { mtv_ref = ref, mtv_tclvl = tv_lvl } <- tcTyVarDetails tv
- = assertPpr (new_lvl `strictlyDeeperThan` tv_lvl) (ppr new_lvl <+> ppr tv) $
- do { info <- readTcRef ref
- ; case info of {
- Indirect {} -> return () ; -- The instantiation variable has already
- -- been filled in; skip entirely
- Flexi ->
- do { cloned_tv <- cloneMetaTyVar tv
- ; let rhs_tv = setMetaTyVarTcLevel cloned_tv new_lvl
- ; liftZonkM $ writeTcRef ref (Indirect (TyVarTy rhs_tv))
- -- Do not go via writeMetaTyVar! In debug-mode it makes sanity check
- -- on level numbers which /demoting/ deliberately disobeys
- ; traceTc "demoteTyVar" (ppr tv <+> text "-->" <+> ppr rhs_tv)
- ; return () } } }
- | otherwise
- = pprPanic "demoteDeltaTyVarTo" (ppr tv)
-
-demoteQLDelta :: TcTyVarSet -> TcM ()
--- See Note [Quick Look at value arguments] wrinkle (QLA5)
--- in GHC.Tc.Gen.App
---
--- Invariant: all elements of delta have the same level (namely
--- the level of the original tcApp), so we need only
--- check the first one
-demoteQLDelta delta
- = case tvs of
- [] -> return () -- Could panic: we are always called with a non-empty set
- (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
- -- Non-determinism is OK because order of demotion doesn't matter
-
{-
%************************************************************************
%* *
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -242,8 +242,6 @@ import Data.IORef ( IORef )
import Data.List.NonEmpty( NonEmpty(..) )
import Data.List ( partition, nub, (\\) )
-import GHC.Exts
-
{-
************************************************************************
* *
@@ -695,7 +693,7 @@ noConcreteTyVars = emptyNameEnv
* *
********************************************************************* -}
-data TcLevel = TcLevel Int#
+data TcLevel = TcLevel {-# UNPACK #-} !Int
| QLInstVar
-- See Note [TcLevel invariants] for what this Int is
-- See also Note [TcLevel assignment]
@@ -759,7 +757,7 @@ 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.
+escape check.)
QL instantation variables are eventually turned into ordinary unificaiton
variables; see (QL3) in Note [Quick Look overview].
@@ -813,14 +811,14 @@ touchable; but then 'b' has escaped its scope into the outer implication.
-}
maxTcLevel :: TcLevel -> TcLevel -> TcLevel
-maxTcLevel(TcLevel a) (TcLevel b)
- | isTrue# (a ># b) = TcLevel a
- | otherwise = TcLevel b
-maxTcLevel _ _ = QLInstVar
+maxTcLevel (TcLevel a) (TcLevel b)
+ | a > b = TcLevel a
+ | otherwise = TcLevel b
+maxTcLevel _ _ = QLInstVar
minTcLevel :: TcLevel -> TcLevel -> TcLevel
minTcLevel tcla@(TcLevel a) tclb@(TcLevel b)
- | isTrue# (a <# b) = tcla
+ | a < b = tcla
| otherwise = tclb
minTcLevel tcla@(TcLevel {}) QLInstVar = tcla
minTcLevel QLInstVar tclb@(TcLevel {}) = tclb
@@ -828,34 +826,34 @@ minTcLevel QLInstVar QLInstVar = QLInstVar
topTcLevel :: TcLevel
-- See Note [TcLevel assignment]
-topTcLevel = TcLevel 0# -- 0 = outermost level
+topTcLevel = TcLevel 0 -- 0 = outermost level
isTopTcLevel :: TcLevel -> Bool
-isTopTcLevel (TcLevel 0#) = True
+isTopTcLevel (TcLevel 0) = True
isTopTcLevel _ = False
pushTcLevel :: TcLevel -> TcLevel
-- See Note [TcLevel assignment]
-pushTcLevel (TcLevel us) = TcLevel (us +# 1#)
+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)
+ = 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)
+ = tv_tclvl >= ctxt_tclvl
deeperThanOrSame (TcLevel {}) QLInstVar = False
deeperThanOrSame QLInstVar _ = True
sameDepthAs :: TcLevel -> TcLevel -> Bool
sameDepthAs (TcLevel ctxt_tclvl) (TcLevel tv_tclvl)
- = isTrue# (ctxt_tclvl ==# tv_tclvl)
+ = ctxt_tclvl == tv_tclvl
-- NB: invariant ctxt_tclvl >= tv_tclvl
-- So <= would be equivalent
sameDepthAs QLInstVar QLInstVar = True
@@ -887,7 +885,7 @@ tcTypeLevel ty
| otherwise = lvl
instance Outputable TcLevel where
- ppr (TcLevel n) = ppr (I# n)
+ ppr (TcLevel n) = ppr n
ppr QLInstVar = text "qlinst"
{- *********************************************************************
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6afa552f643fc4a78e94562234e2f95b0166c19d
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6afa552f643fc4a78e94562234e2f95b0166c19d
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/20240606/469859a4/attachment-0001.html>
More information about the ghc-commits
mailing list