Simon Peyton Jones pushed to branch wip/26543 at Glasgow Haskell Compiler / GHC Commits: f225ae07 by Simon Peyton Jones at 2025-11-28T10:40:57+00:00 More refactoring - - - - - 50b70db3 by Simon Peyton Jones at 2025-11-28T10:43:46+00:00 Fix Notes about CoercionHoles - - - - - 4 changed files: - compiler/GHC/Core/TyCo/FVs.hs - compiler/GHC/Core/TyCo/Rep.hs - compiler/GHC/Tc/Gen/App.hs - compiler/GHC/Tc/Utils/Unify.hs Changes: ===================================== compiler/GHC/Core/TyCo/FVs.hs ===================================== @@ -1022,7 +1022,7 @@ afvFolder check_fv = TyCoFolder { tcf_view = noView -- See Note [Free vars and do_tcv is tv = Any (not (tv `elemVarSet` is) && check_fv tv) do_bndr is tv _ = is `extendVarSet` tv do_hole _ hole = Any (anyFreeVarsOfType check_fv (varType (coHoleCoVar hole))) - -- See Note [CoercionHoles and their variables] + -- See Note [CoercionHoles and their free variables] -- NB: that call to `anyFreeVarsOfType` on the kind starts again with the -- empty in-scope set; see Note [Closing over free variable kinds] ===================================== compiler/GHC/Core/TyCo/Rep.hs ===================================== @@ -1817,7 +1817,7 @@ Other notes about CoercionHole and HoleCo: * It carries a type which makes `coercionKind` and `coercionRole` work * It has a Unique, which gives the hole an identity; see calls to `ctEvEvId` -(COH3) See Note [CoercionHoles and coercion free variables] in GHC.Core.TyCo.FVs +(COH3) See Note [CoercionHoles and their free variables] in GHC.Core.TyCo.FVs (COH4) Coercion holes can be compared for equality like other coercions: by looking at the types coerced. ===================================== compiler/GHC/Tc/Gen/App.hs ===================================== @@ -424,68 +424,43 @@ tcApp rn_expr exp_res_ty ; do_ql <- wantQuickLook rn_fun ; (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) - - -- Step 4.1: subsumption check against expected result type - -- See Note [Unify with expected type before typechecking arguments] - ; res_wrap <- checkResultTy rn_expr tc_head inst_args - app_res_rho exp_res_ty - - -- Step 4.2: typecheck the arguments - ; tc_args <- tcValArgs NoQL inst_args - - -- Step 4.3: wrap up - ; finishApp tc_head tc_args app_res_rho res_wrap } - - DoQL -> do { traceTc "tcApp:DoQL" (ppr rn_fun $$ ppr app_res_rho) - - -- Step 5.1: Take a quick look at the result type + ; app_res_rho <- case do_ql of + NoQL -> return app_res_rho + DoQL -> do { -- Step 5.1: Take a quick look at the result type -- See Note [QuickLook: arguments before result] - ; case exp_res_ty of - Check exp_rho -> quickLookResultType app_res_rho exp_rho - Infer {} -> return () + case exp_res_ty of + Check exp_rho -> quickLookResultType app_res_rho exp_rho + Infer {} -> return () -- 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 + -- from either quickLookArg or quickLookResultType + ; liftZonkM $ zonkTcType app_res_rho } - -- Step 5.4: subsumption check against the expected type - -- See Note [Unify with expected type before typechecking arguments] - ; res_wrap <- checkResultTy rn_expr tc_head inst_args - 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 - - -- Step 5.5: wrap up - ; finishApp tc_head tc_args app_res_rho res_wrap } } - --- | 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 -getDeepSubsumptionFlag_DataConHead app_head = - do { user_ds <- xoptM LangExt.DeepSubsumption - ; return $ - if | user_ds - -> Deep DeepSub - | XExpr (ConLikeTc (RealDataCon {})) <- app_head - -> Deep TopSub - | otherwise - -> Shallow - } + ; finishApp do_ql rn_expr tc_head inst_args app_res_rho exp_res_ty } -finishApp :: (HsExpr GhcTc, AppCtxt) -> [HsExprArg 'TcpTc] - -> TcRhoType -> HsWrapper +finishApp :: QLFlag -> HsExpr GhcRn + -> (HsExpr GhcTc, AppCtxt) -> [HsExprArg 'TcpInst] + -> TcRhoType -> ExpRhoType -> TcM (HsExpr GhcTc) -- Do final checks and wrap up the result -finishApp tc_head@(tc_fun,_) tc_args app_res_rho res_wrap - = do { - -- Reconstruct, with a horrible special case for tagToEnum#. - res_expr <- if isTagToEnum tc_fun +-- Precondition: app_res_rho has no polymorphism hidden under instantiation variables +finishApp do_ql rn_expr tc_head@(tc_fun,_) inst_args + app_res_rho exp_res_ty + = do { -- Step 5.4: subsumption check against the expected type + -- See Note [Unify with expected type before typechecking arguments] + res_wrap <- checkResultTy rn_expr tc_head inst_args + app_res_rho exp_res_ty + + -- Step 5.2: Typecheck the arguments, and monomorphise + -- any un-unified instantiation variables + ; tc_args <- tcValArgs do_ql inst_args + + -- Horrible special case for tagToEnum#. + ; res_expr <- if isTagToEnum tc_fun then tcTagToEnum tc_head tc_args app_res_rho else return (rebuildHsApps tc_head tc_args) + ; traceTc "End tcApp }" (ppr tc_fun) ; return (mkHsWrap res_wrap res_expr) } @@ -630,10 +605,8 @@ tcValArg _ (EValArgQL { eaql_wanted = wanted quickLookResultType app_res_rho exp_arg_rho -- the qlUnify ; app_res_rho <- liftZonkM $ zonkTcType app_res_rho - ; res_wrap <- checkResultTy rn_expr tc_head inst_args - app_res_rho (mkCheckExpType exp_arg_rho) - ; tc_args <- tcValArgs DoQL inst_args - ; finishApp tc_head tc_args app_res_rho res_wrap } + ; finishApp DoQL rn_expr tc_head inst_args app_res_rho + (mkCheckExpType exp_arg_rho) } ; traceTc "tcEValArgQL }" $ vcat [ text "app_res_rho:" <+> ppr app_res_rho ] @@ -644,6 +617,20 @@ tcValArg _ (EValArgQL { eaql_wanted = wanted -------------------- +-- | 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 +getDeepSubsumptionFlag_DataConHead app_head = + do { user_ds <- xoptM LangExt.DeepSubsumption + ; return $ + if | user_ds + -> Deep DeepSub + | XExpr (ConLikeTc (RealDataCon {})) <- app_head + -> Deep TopSub + | otherwise + -> Shallow + } + whenQL :: QLFlag -> ZonkM () -> TcM () whenQL DoQL thing_inside = liftZonkM thing_inside whenQL NoQL _ = return () ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -3555,7 +3555,7 @@ mkOccFolders lhs_tv = (getAny . check_ty, getAny . check_co) do_hole _is hole = check_ty (varType (coHoleCoVar hole)) -- For coercion holes, look in the kind of the hole - -- See Note [CorecionHoles and their free variables] in GHC.Core.TyCo.FVs + -- See Note [CoercionHoles and their free variables] in GHC.Core.TyCo.FVs {- ********************************************************************* * * @@ -4190,7 +4190,7 @@ checkCo flags co = else PuFail reason } -- Occurs check (no promotion) - -- See Note [CorecionHoles and their free variables] in GHC.Core.TyCo.FVs + -- See Note [CoercionHoles and their free variables] in GHC.Core.TyCo.FVs | OC_Check lhs_tv occ_prob <- occ , let (_, check_co) = mkOccFolders lhs_tv , check_co co View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/fa545237fe7514276f690ae5fdfa789... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/fa545237fe7514276f690ae5fdfa789... You're receiving this email because of your account on gitlab.haskell.org.