diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2020-11-25 11:33:11 +0000 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2020-12-19 02:14:07 -0500 |
commit | c2430398481f5aab12fd94e6549c7b9bbd1e43fe (patch) | |
tree | 02abc39374f93b9e8d84b764ac4f7174e09b9588 /compiler | |
parent | 59a07641090eec9dcaf5af97026b94911ca3191c (diff) | |
download | haskell-c2430398481f5aab12fd94e6549c7b9bbd1e43fe.tar.gz |
Quick Look: zonk result type
Provoked by #18987, this patch adds a missing zonkQuickLook of
app_res_rho in tcApp.
Most of the time this zonk is unnecesary. In fact, I can't think of a
concrete case where it is needed -- hence no test. But even if it
isn't necessary, the reasoning that allows it to be omitted is very
subtle. So I've put it in.
However, adding this zonk does /not/ affect the emitted constraints,
so the reported symptoms for #18987 remain, but harmlessly so, and now
documented in a new Note [Instantiation variables are short lived]
in GHC.Tc.Gen.App.
No change in behaviour, no tests.
Diffstat (limited to 'compiler')
-rw-r--r-- | compiler/GHC/Tc/Gen/App.hs | 86 | ||||
-rw-r--r-- | compiler/GHC/Tc/Solver/Rewrite.hs | 5 |
2 files changed, 72 insertions, 19 deletions
diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs index eb5540c539..5f17621b62 100644 --- a/compiler/GHC/Tc/Gen/App.hs +++ b/compiler/GHC/Tc/Gen/App.hs @@ -86,17 +86,43 @@ Some notes relative to the paper a polytype. * When QL is done, we don't need to turn the un-filled-in - instantiation variables into unification variables -- they already - are! - - Moreover, all filled-in occurrences of instantiation variables - have been zonked away (see "Crucial step" in tcValArgs), and - so the rest of the type checker never sees a meta-type variable - filled in with a polytype. For the rest of the typechecker, - a meta type variable stands (only) for a monotype. + instantiation variables into unification variables -- they + already /are/ unification varibles! See also + Note [Instantiation variables are short lived]. * 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. -} @@ -263,6 +289,15 @@ tcApp rn_expr exp_res_ty -- Typecheck the value arguments ; tc_args <- tcValArgs do_ql tc_fun inst_args + -- Zonk the result type, to ensure that we substitute out + -- any filled-in instantiation variable before calling tcWrapResultMono + -- In the Check case, this isn't really necessary, becuase tcWrapResultMono + -- just drops to tcUnify; but in the Infer case a filled-in instantiation + -- variable might perhaps escape into the constraint generator. The safe + -- thing to do is to any instantaition variables away. + -- See Note [Instantiation variables are short lived] + ; app_res_rho <- zonkQuickLook do_ql app_res_rho + -- Special case for tagToEnum# ; if isTagToEnum rn_fun then tcTagToEnum rn_expr tc_fun tc_args app_res_rho exp_res_ty @@ -272,11 +307,29 @@ tcApp rn_expr exp_res_ty ; let tc_expr = rebuild tc_fun tc_args -- Wrap the result - -- NB: app_res_ty may be a polytype, via zonkQuickLook ; addFunResCtxt tc_fun tc_args app_res_rho exp_res_ty $ - tcWrapResult rn_expr tc_expr app_res_rho exp_res_ty } } + tcWrapResultMono rn_expr tc_expr app_res_rho exp_res_ty } } -------------------- +wantQuickLook :: HsExpr GhcRn -> TcM Bool +-- GHC switches on impredicativity all the time for ($) +wantQuickLook (HsVar _ f) | unLoc f `hasKey` dollarIdKey = return True +wantQuickLook _ = xoptM LangExt.ImpredicativeTypes + +zonkQuickLook :: Bool -> TcType -> TcM TcType +-- After all Quick Look unifications are done, zonk to ensure that all +-- instantation variables are substituted away +-- +-- So far as the paper is concerned, this step applies +-- the poly-substitution Theta, learned by QL, so that we +-- "see" the polymorphism in that type +-- +-- In implementation terms this ensures that no unification variable +-- linger on that have been filled in with a polytype +zonkQuickLook do_ql ty + | do_ql = zonkTcType ty + | otherwise = return ty + -- 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. @@ -287,18 +340,13 @@ zonkArg eva@(EValArg { eva_arg_ty = Scaled m ty }) zonkArg arg = return arg -wantQuickLook :: HsExpr GhcRn -> TcM Bool --- GHC switches on impredicativity all the time for ($) -wantQuickLook (HsVar _ f) | unLoc f `hasKey` dollarIdKey = return True -wantQuickLook _ = xoptM LangExt.ImpredicativeTypes - ---------------- tcValArgs :: Bool -- Quick-look on? -> HsExpr GhcTc -- The function (for error messages) -> [HsExprArg 'TcpInst] -- Actual argument -> TcM [HsExprArg 'TcpTc] -- Resulting argument -tcValArgs quick_look fun args +tcValArgs do_ql fun args = go 1 args where go _ [] = return [] @@ -321,8 +369,8 @@ tcValArgs quick_look fun args -- (:) :: forall p. p->[p]->[p] -- Then Theta = [p :-> forall a. a->a], and we want -- to check 'e' with expected type (forall a. a->a) - arg_ty <- if quick_look then zonkTcType arg_ty - else return arg_ty + -- See Note [Instantiation variables are short lived] + arg_ty <- zonkQuickLook do_ql arg_ty -- Now check the argument ; arg' <- addErrCtxt (funAppCtxt fun (eValArgExpr arg) n) $ @@ -1062,7 +1110,7 @@ tcTagToEnum expr fun args app_res_ty res_ty vanilla_result = do { let expr' = rebuildPrefixApps fun args - ; tcWrapResult expr expr' app_res_ty res_ty } + ; tcWrapResultMono expr expr' app_res_ty res_ty } check_enumeration ty' tc | isEnumerationTyCon tc = return () diff --git a/compiler/GHC/Tc/Solver/Rewrite.hs b/compiler/GHC/Tc/Solver/Rewrite.hs index 7e4993ad8d..42a00d73ba 100644 --- a/compiler/GHC/Tc/Solver/Rewrite.hs +++ b/compiler/GHC/Tc/Solver/Rewrite.hs @@ -897,6 +897,11 @@ data RewriteTvResult -- ^ The tyvar rewrites to a not-necessarily rewritten other type. -- co :: new type ~r old type, where the role is determined by -- the RewriteEnv + -- + -- With Quick Look, the returned TcType can be a polytype; + -- that is, in the constraint solver, a unification variable + -- can contain a polytype. See GHC.Tc.Gen.App + -- Note [Instantiation variables are short lived] rewriteTyVar :: TyVar -> RewriteM (Xi, Coercion) rewriteTyVar tv |