Simon Peyton Jones pushed to branch wip/26543 at Glasgow Haskell Compiler / GHC Commits: 73e25771 by Simon Peyton Jones at 2025-11-27T15:53:24+00:00 Wibbles to guarded-ness - - - - - 4d849a99 by Simon Peyton Jones at 2025-11-27T17:49:35+00:00 Wibble - - - - - 1 changed file: - compiler/GHC/Tc/Gen/App.hs Changes: ===================================== compiler/GHC/Tc/Gen/App.hs ===================================== @@ -290,10 +290,9 @@ Now we split into two cases: 5. Case DoQL: use Quick Look - 5.1 Use `quickLookResultType` to take a quick look at the result type, - when in checking mode. This is the shaded part of APP-Downarrow - in Fig 5. It also implements the key part of - Note [Unify with expected type before typechecking arguments] + 5.1 Take a quick look at the result type, when in checking mode. This is the + shaded part of APP-Downarrow in Fig 5. It also implements the key part + of Note [Unify with expected type before typechecking arguments] 5.2 Check the arguments with `tcValArgs`. Importantly, this will monomorphise all the instantiation variables of the call. @@ -404,29 +403,28 @@ tcApp rn_expr exp_res_ty DoQL -> do { traceTc "tcApp:DoQL" (ppr rn_fun $$ ppr app_res_rho) -- Step 5.1: Take a quick look at the result type - ; quickLookResultType app_res_rho exp_res_ty - ; inst_args' <- mapM quickLookArg inst_args + ; inst_args_with_guards <- case exp_res_ty of + Check exp_rho -> do { qlUnify app_res_rho exp_rho + ; mapM reGuardArg inst_args } + Infer {} -> return inst_args - -- Step 5.2: typecheck the arguments, and monomorphise - -- any un-unified instantiation variables - ; tc_args <- tcValArgs DoQL inst_args' + ; inst_args_ql <- mapM quickLookArg inst_args_with_guards -- Step 5.3: zonk to expose the polymorphism hidden under -- QuickLook instantiation variables in `app_res_rho` ; app_res_rho <- liftZonkM $ zonkTcType app_res_rho -- Step 5.4: subsumption check against the expected type - ; res_wrap <- checkResultTy rn_expr tc_head inst_args + ; res_wrap <- checkResultTy rn_expr tc_head inst_args_ql app_res_rho exp_res_ty + + -- Step 5.2: typecheck the arguments, and monomorphise + -- any un-unified instantiation variables + ; tc_args <- tcValArgs DoQL inst_args_ql + -- Step 5.5: wrap up ; finishApp tc_head tc_args app_res_rho res_wrap } } -quickLookResultType :: TcRhoType -> ExpRhoType -> TcM () --- This function implements the shaded bit of rule APP-Downarrow in --- Fig 5 of the QL paper: "A quick look at impredicativity" (ICFP'20). -quickLookResultType app_res_rho (Check exp_rho) = qlUnify app_res_rho exp_rho -quickLookResultType _ _ = return () - -- | Variant of 'getDeepSubsumptionFlag' which enables a top-level subsumption -- in order to implement the plan of Note [Typechecking data constructors]. getDeepSubsumptionFlag_DataConHead :: HsExpr GhcTc -> TcM DeepSubsumptionFlag @@ -458,7 +456,7 @@ finishApp tc_head@(tc_fun,_) tc_args app_res_rho res_wrap -- This is usually just a unification, but with deep subsumption there is more to do. checkResultTy :: HsExpr GhcRn -> (HsExpr GhcTc, AppCtxt) -- Head - -> [HsExprArg p] -- Arguments, just error messages + -> [HsExprArg p] -- Arguments, just for error messages -> TcRhoType -- Inferred type of the application; zonked to -- expose foralls, but maybe not /deeply/ instantiated -> ExpRhoType -- Expected type; this is deeply skolemised @@ -1843,14 +1841,15 @@ This turned out to be more subtle than I expected. Wrinkles: -} -quickLookArg :: HsExprArg 'TcpInst - -> TcM (HsExprArg 'TcpInst) +quickLookArg :: HsExprArg 'TcpInst -> TcM (HsExprArg 'TcpInst) -- quickLookArg1 implements the "QL Argument" judgement in Fig 5 of the paper -- See Note [Quick Look at value arguments] quickLookArg e_arg@(EValArg { ea_ctxt = ctxt , ea_arg = larg@(L _ arg) - , ea_arg_ty = orig_arg_ty@(Scaled _ orig_arg_rho) }) - = do { is_rho <- tcIsDeepRho orig_arg_rho + , ea_arg_ty = orig_arg_ty }) + = do { let !(Scaled _ orig_arg_rho) = orig_arg_ty + -- NB: orig_arg_rho may not be zonked, but that's ok + ; is_rho <- tcIsDeepRho orig_arg_rho ; traceTc "qla" (ppr orig_arg_ty $$ ppr is_rho) ; if not is_rho then return e_arg @@ -1887,7 +1886,6 @@ quickLookArg e_arg@(EValArg { ea_ctxt = ctxt -- not usage constraints. See (QLA6) in Note [Quick Look at -- value arguments] -{- ; traceTc "quickLookArg 2" $ vcat [ text "arg:" <+> ppr arg , text "orig_arg_rho:" <+> ppr orig_arg_rho @@ -1895,36 +1893,29 @@ quickLookArg e_arg@(EValArg { ea_ctxt = ctxt -- Step 3: Check the two other premises of APP-lightning-bolt (Fig 5 in the paper) -- Namely: (A) is orig_arg_rho is guarded - -- or: (B) fiv(app_res_rho) = emptyset + -- or: (B) fiv(app_res_rho) = emptyset + -- then Step 4: do quick-look unification if either (A) or (B) hold + -- + -- For (B) see Note [The fiv test in quickLookArg] -- This tells us if the quick look at the argument yields information that -- influences the enclosing function call -- NB: `isGuardedTy` is computed based on the original, -- unzonked orig_arg_rho, so that we deliberately do not exploit -- guardedness that emerges a result of QL on earlier args -- In contrast, we must do the `anyFreeKappa` test /after/ tcInstFun; see (QLA3). - ; arg_influences_enclosing_call - <- if isGuardedTy orig_arg_rho - then return True - else not <$> anyFreeKappa app_res_rho -- (B) - -- For (B) see Note [The fiv test in quickLookArg] - - -- Step 4: do quick-look unification if either (A) or (B) hold - -- NB: orig_arg_rho may not be zonked, but that's ok - ; when arg_influences_enclosing_call $ - qlUnify app_res_rho orig_arg_rho --} - ; (arg_influences_call, inst_args') - <- if isGuardedTy orig_arg_rho + ; (arg_influences_call, inst_args_ql) + <- if isGuardedTy orig_arg_rho -- (A) then do { qlUnify app_res_rho orig_arg_rho - ; inst_args' <- mapM quickLookArg inst_args - ; return (True, inst_args') } - else do { inst_args' <- mapM quickLookArg inst_args - ; has_free_inst_vars <- anyFreeKappa app_res_rho + ; inst_args_with_guards <- mapM reGuardArg inst_args + ; inst_args_ql <- mapM quickLookArg inst_args_with_guards + ; return (True, inst_args_ql) } + else do { inst_args_ql <- mapM quickLookArg inst_args + ; has_free_inst_vars <- anyFreeKappa app_res_rho --(B) ; if has_free_inst_vars - then return (False, inst_args') + then return (False, inst_args_ql) else do { qlUnify app_res_rho orig_arg_rho - ; return (True, inst_args') } } + ; return (True, inst_args_ql) } } ; traceTc "quickLookArg done }" (ppr rn_fun) @@ -1933,7 +1924,7 @@ quickLookArg e_arg@(EValArg { ea_ctxt = ctxt , eaql_larg = larg , eaql_tc_fun = tc_head , eaql_fun_ue = fun_ue - , eaql_args = inst_args' + , eaql_args = inst_args_ql , eaql_wanted = wanted , eaql_encl = arg_influences_call , eaql_res_rho = app_res_rho }) }}}} @@ -1970,6 +1961,15 @@ tcIsDeepRho ty | otherwise = return True +reGuardArg :: HsExprArg 'TcpInst -> TcM (HsExprArg 'TcpInst) +-- Zonk the result type of an EValArg, so that a subseqent +-- call to isGuardedTy will see the unifications so far +reGuardArg arg@(EValArg { ea_arg_ty = arg_ty }) + = do { arg_ty' <- liftZonkM $ zonkScaledTcType arg_ty + ; return (arg { ea_arg_ty = arg_ty' }) } +reGuardArg arg + = return arg + isGuardedTy :: TcType -> Bool isGuardedTy ty | Just (tc,_) <- tcSplitTyConApp_maybe ty = isGenerativeTyCon tc Nominal View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/b6dea5cf14d690a961047db13944701... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/b6dea5cf14d690a961047db13944701... You're receiving this email because of your account on gitlab.haskell.org.