Simon Peyton Jones pushed to branch wip/26543 at Glasgow Haskell Compiler / GHC Commits: a429ef71 by Simon Peyton Jones at 2025-11-20T08:46:06+00:00 Tyvar priority If necy, eliminate a vanilla tv in favour of a *concrete* tv. That is, concreteness is more important that QLInstVar - - - - - 214cbb19 by Simon Peyton Jones at 2025-11-20T14:12:14+00:00 Expermimental patch to QuickLook cf #26598/#26599 - - - - - 2 changed files: - compiler/GHC/Tc/Gen/App.hs - compiler/GHC/Tc/Utils/Unify.hs Changes: ===================================== compiler/GHC/Tc/Gen/App.hs ===================================== @@ -385,8 +385,7 @@ tcApp rn_expr exp_res_ty -- Step 3: Instantiate the function type (taking a quick look at args) ; do_ql <- wantQuickLook rn_fun - ; (inst_args, app_res_rho) - <- tcInstFun do_ql inst_final tc_head fun_sigma rn_args + ; (inst_args, app_res_rho) <- tcInstFun do_ql inst_final tc_head fun_sigma rn_args ; case do_ql of NoQL -> do { traceTc "tcApp:NoQL" (ppr rn_fun $$ ppr app_res_rho) @@ -406,10 +405,11 @@ tcApp rn_expr exp_res_ty -- Step 5.1: Take a quick look at the result type ; quickLookResultType app_res_rho exp_res_ty + ; inst_args' <- mapM quickLookArg inst_args -- Step 5.2: typecheck the arguments, and monomorphise -- any un-unified instantiation variables - ; tc_args <- tcValArgs DoQL inst_args + ; tc_args <- tcValArgs DoQL inst_args' -- Step 5.3: zonk to expose the polymorphism hidden under -- QuickLook instantiation variables in `app_res_rho` @@ -841,9 +841,11 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args (Just $ HsExprTcThing tc_fun) (n_val_args, fun_sigma) fun_ty - ; ds_flag <- getDeepSubsumptionFlag_DataConHead tc_fun - ; arg' <- quickLookArg ds_flag do_ql ctxt arg arg_ty - ; let acc' = arg' : addArgWrap (mkWpCastN fun_co) acc + ; let arg' = EValArg { ea_ctxt = ctxt + , ea_arg = arg + , ea_arg_ty = arg_ty } + acc' = arg' : addArgWrap (mkWpCastN fun_co) acc + ; go (pos+1) acc' res_ty rest_args } new_arg_ty :: LHsExpr GhcRn -> Int -> TcM (Scaled TcType) @@ -1841,68 +1843,20 @@ This turned out to be more subtle than I expected. Wrinkles: -} -quickLookArg :: DeepSubsumptionFlag - -> QLFlag -> AppCtxt - -> LHsExpr GhcRn -- ^ Argument - -> Scaled TcSigmaTypeFRR -- ^ Type expected by the function +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 _ NoQL ctxt larg orig_arg_ty - = skipQuickLook ctxt larg orig_arg_ty -quickLookArg ds_flag DoQL ctxt larg orig_arg_ty - = do { is_rho <- tcIsDeepRho ds_flag (scaledThing orig_arg_ty) +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 ; traceTc "qla" (ppr orig_arg_ty $$ ppr is_rho) ; if not is_rho - then skipQuickLook ctxt larg orig_arg_ty - else quickLookArg1 ctxt larg orig_arg_ty } - -skipQuickLook :: AppCtxt -> LHsExpr GhcRn -> Scaled TcRhoType - -> TcM (HsExprArg 'TcpInst) -skipQuickLook ctxt larg arg_ty - = return (EValArg { ea_ctxt = ctxt - , ea_arg = larg - , ea_arg_ty = arg_ty }) - -whenQL :: QLFlag -> ZonkM () -> TcM () -whenQL DoQL thing_inside = liftZonkM thing_inside -whenQL NoQL _ = return () - -tcIsDeepRho :: DeepSubsumptionFlag -> TcType -> TcM Bool --- This top-level zonk step, which is the reason we need a local 'go' loop, --- is subtle. See Section 9 of the QL paper - -tcIsDeepRho ds_flag = go - where - go ty - | isSigmaTy ty - = return False - - | Just kappa <- getTyVar_maybe ty - , isQLInstTyVar kappa - = do { info <- readMetaTyVar kappa - ; case info of - Indirect arg_ty' -> go arg_ty' - Flexi -> return True } - - | Deep {} <- ds_flag - , Just (_, res_ty) <- tcSplitFunTy_maybe ty - = go res_ty - - | otherwise - = return True + then return e_arg + else -isGuardedTy :: TcType -> Bool -isGuardedTy ty - | Just (tc,_) <- tcSplitTyConApp_maybe ty = isGenerativeTyCon tc Nominal - | Just {} <- tcSplitAppTy_maybe ty = True - | otherwise = False - -quickLookArg1 :: AppCtxt -> LHsExpr GhcRn - -> Scaled TcRhoType -- Deeply skolemised - -> TcM (HsExprArg 'TcpInst) --- quickLookArg1 implements the "QL Argument" judgement in Fig 5 of the paper -quickLookArg1 ctxt larg@(L _ arg) sc_arg_ty@(Scaled _ orig_arg_rho) - = addArgCtxt ctxt larg $ -- Context needed for constraints + addArgCtxt ctxt larg $ -- Context needed for constraints -- generated by calls in arg do { ((rn_fun, fun_ctxt), rn_args) <- splitHsApps arg @@ -1920,7 +1874,7 @@ quickLookArg1 ctxt larg@(L _ arg) sc_arg_ty@(Scaled _ orig_arg_rho) , text "args:" <+> ppr rn_args ] ; case mb_fun_ty of { - Nothing -> skipQuickLook ctxt larg sc_arg_ty ; -- fun is too complicated + Nothing -> return e_arg ; -- fun is too complicated Just (tc_fun, fun_sigma) -> -- step 2: use |-inst to instantiate the head applied to the arguments @@ -1930,9 +1884,10 @@ quickLookArg1 ctxt larg@(L _ arg) sc_arg_ty@(Scaled _ orig_arg_rho) <- captureConstraints $ tcInstFun do_ql True tc_head fun_sigma rn_args -- We must capture type-class and equality constraints here, but - -- not equality constraints. See (QLA6) in Note [Quick Look at + -- 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 @@ -1943,10 +1898,10 @@ quickLookArg1 ctxt larg@(L _ arg) sc_arg_ty@(Scaled _ orig_arg_rho) -- or: (B) fiv(app_res_rho) = emptyset -- This tells us if the quick look at the argument yields information that -- influences the enclosing function call - -- NB: guardedness 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 - -- We must do the anyFreeKappa test /after/ tcInstFun; see (QLA3). + -- 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 @@ -1957,18 +1912,69 @@ quickLookArg1 ctxt larg@(L _ arg) sc_arg_ty@(Scaled _ orig_arg_rho) -- 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 + 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 + ; if has_free_inst_vars + then return (False, inst_args') + else do { qlUnify app_res_rho orig_arg_rho + ; return (True, inst_args') } } ; traceTc "quickLookArg done }" (ppr rn_fun) ; return (EValArgQL { eaql_ctxt = ctxt - , eaql_arg_ty = sc_arg_ty + , eaql_arg_ty = orig_arg_ty , eaql_larg = larg , eaql_tc_fun = tc_head , eaql_fun_ue = fun_ue - , eaql_args = inst_args + , eaql_args = inst_args' , eaql_wanted = wanted - , eaql_encl = arg_influences_enclosing_call - , eaql_res_rho = app_res_rho }) }}} + , eaql_encl = arg_influences_call + , eaql_res_rho = app_res_rho }) }}}} + +quickLookArg other_arg = return other_arg + +whenQL :: QLFlag -> ZonkM () -> TcM () +whenQL DoQL thing_inside = liftZonkM thing_inside +whenQL NoQL _ = return () + +tcIsDeepRho :: TcType -> TcM Bool +-- This top-level zonk step, which is the reason we need a local 'go' loop, +-- is subtle. See Section 9 of the QL paper + +tcIsDeepRho ty + = do { ds_flag <- getDeepSubsumptionFlag + ; go ds_flag ty } + where + go ds_flag ty + | isSigmaTy ty + = return False + + | Just kappa <- getTyVar_maybe ty + , isQLInstTyVar kappa + = do { info <- readMetaTyVar kappa + ; case info of + Indirect arg_ty' -> go ds_flag arg_ty' + Flexi -> return True } + + | Deep {} <- ds_flag + , Just (_, res_ty) <- tcSplitFunTy_maybe ty + = go ds_flag res_ty + + | otherwise + = return True + +isGuardedTy :: TcType -> Bool +isGuardedTy ty + | Just (tc,_) <- tcSplitTyConApp_maybe ty = isGenerativeTyCon tc Nominal + | Just {} <- tcSplitAppTy_maybe ty = True + | otherwise = False {- ********************************************************************* * * @@ -2075,13 +2081,14 @@ 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] + kappa ~ [forall a. a->a] -} anyFreeKappa :: TcType -> TcM Bool -- True if there is a free instantiation variable -- in the argument type, after zonking -- See Note [The fiv test in quickLookArg] +-- The function is monadic; it does not require a zonked type as input anyFreeKappa ty = unTcMBool (foldQLInstVars go_tv ty) where go_tv tv = TCMB $ do { info <- readMetaTyVar tv ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -3076,15 +3076,16 @@ lhsPriority tv RuntimeUnk -> 0 SkolemTv {} -> 0 MetaTv { mtv_info = info, mtv_tclvl = lvl } - | QLInstVar <- lvl - -> 5 -- Eliminate instantiation variables first - | otherwise -> case info of CycleBreakerTv -> 0 TyVarTv -> 1 - ConcreteTv {} -> 2 - TauTv -> 3 - RuntimeUnkTv -> 4 + ConcreteTv {} -> qli 2 -- 2,3 + TauTv -> qli 4 -- 4,5 + RuntimeUnkTv -> 6 + where + qli n = case lvl of + QLInstVar -> n+1 -- Eliminate instantiation variables first + _ -> n {- Note [Unification preconditions] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/85877603abca70b6c3679067229eb53... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/85877603abca70b6c3679067229eb53... You're receiving this email because of your account on gitlab.haskell.org.