Simon Peyton Jones pushed to branch wip/ani/no-ds-flag-cache at Glasgow Haskell Compiler / GHC Commits: 6986cae3 by Simon Peyton Jones at 2026-03-30T17:05:10+01:00 Wibbles from Simon - - - - - 7 changed files: - compiler/GHC/Tc/Gen/App.hs - compiler/GHC/Tc/Gen/Expr.hs - compiler/GHC/Tc/Gen/Expr.hs-boot - compiler/GHC/Tc/Gen/Head.hs - compiler/GHC/Tc/Gen/Match.hs - compiler/GHC/Tc/Utils/TcMType.hs - compiler/GHC/Tc/Utils/Unify.hs Changes: ===================================== compiler/GHC/Tc/Gen/App.hs ===================================== @@ -488,8 +488,8 @@ checkResultTy :: HsExpr GhcRn -- expose foralls, but maybe not /deeply/ instantiated -> ExpRhoType -- Expected type; this is deeply skolemised -> TcM HsWrapper -checkResultTy rn_expr (tc_fun, _) _ app_res_rho (Infer inf_res) - = do { ds_flag <- getDeepSubsumptionFlag_DataConHead tc_fun +checkResultTy rn_expr _ _ app_res_rho (Infer inf_res) + = do { ds_flag <- getDeepSubsumptionFlag ; fillInferResult ds_flag (exprCtOrigin rn_expr) app_res_rho inf_res } @@ -636,7 +636,8 @@ tcValArg _ pos (fun, fun_lspan) (EValArgQL { , text "app_lspan" <+> ppr lspan , text "head_lspan" <+> ppr fun_lspan , text "tc_head" <+> ppr tc_head]) - ; ds_flag <- getDeepSubsumptionFlag_DataConHead (fst tc_head) + ; ds_flag <- getDeepSubsumptionFlag + -- NB: whether to do deep /skolemisation/ is independent of data constructors ; (wrap, arg') <- tcScalingUsage mult $ tcSkolemise ds_flag GenSigCtxt exp_arg_ty $ \ exp_arg_rho -> @@ -894,8 +895,7 @@ tcInstFun do_ql inst_final (fun_orig, rn_fun, fun_lspan) tc_fun fun_sigma rn_arg matchActualFunTy herald (Just $ HsExprTcThing tc_fun) (n_val_args, fun_sigma) fun_ty - ; ds_flag <- getDeepSubsumptionFlag_DataConHead tc_fun - ; arg' <- quickLookArg ds_flag do_ql pos ctxt (rn_fun, fun_lspan) arg arg_ty + ; arg' <- quickLookArg do_ql pos ctxt (rn_fun, fun_lspan) arg arg_ty ; let acc' = arg' : addArgWrap (mkWpCastN fun_co) acc ; go (pos+1) acc' res_ty rest_args } @@ -1883,17 +1883,18 @@ This turned out to be more subtle than I expected. Wrinkles: -} -quickLookArg :: DeepSubsumptionFlag -> QLFlag -> Int +quickLookArg :: QLFlag -> Int -> SrcSpan -- ^ location span of the whole application -> (HsExpr GhcRn, SrcSpan) -- ^ Head of the application chain and its source span -> LHsExpr GhcRn -- ^ Argument -> Scaled TcSigmaTypeFRR -- ^ Type expected by the function -> TcM (HsExprArg 'TcpInst) -- See Note [Quick Look at value arguments] -quickLookArg _ NoQL _ app_lspan _ larg orig_arg_ty +quickLookArg NoQL _ app_lspan _ larg orig_arg_ty = skipQuickLook app_lspan larg orig_arg_ty -quickLookArg ds_flag DoQL pos app_lspan fun_and_lspan larg orig_arg_ty - = do { is_rho <- tcIsDeepRho ds_flag (scaledThing orig_arg_ty) +quickLookArg DoQL pos app_lspan fun_and_lspan larg orig_arg_ty + = do { ds_flag <- getDeepSubsumptionFlag + ; is_rho <- tcIsDeepRho ds_flag (scaledThing orig_arg_ty) ; traceTc "qla" (ppr orig_arg_ty $$ ppr is_rho) ; if not is_rho then skipQuickLook app_lspan larg orig_arg_ty ===================================== compiler/GHC/Tc/Gen/Expr.hs ===================================== @@ -13,7 +13,7 @@ module GHC.Tc.Gen.Expr ( tcCheckPolyExpr, tcCheckPolyExprNC, tcCheckMonoExpr, tcCheckMonoExprNC, - tcInferExpr, tcInferSigma, + tcInferExpr, tcInferSigma, tcInferExprSigma, tcInferRho, tcInferRhoNC, tcMonoLExpr, tcMonoLExprNC, tcInferRhoFRR, tcInferRhoFRRNC, @@ -237,6 +237,9 @@ tcPolyExprCheck expr res_ty tcInferSigma :: LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcSigmaType) tcInferSigma = tcInferExpr IIF_Sigma +tcInferExprSigma :: HsExpr GhcRn -> TcM (HsExpr GhcTc, TcSigmaType) +tcInferExprSigma e = runInfer IIF_Sigma IFRR_Any (tcExpr e) + tcInferRho, tcInferRhoNC :: LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcRhoType) -- Infer a *rho*-type. The return type is always instantiated. tcInferRho = tcInferExpr IIF_DeepRho @@ -321,7 +324,7 @@ tcExpr e@(HsAppType {}) res_ty = tcApp e res_ty tcExpr e@(ExprWithTySig {}) res_ty = tcApp e res_ty tcExpr (XExpr (ExpandedThingRn hse)) res_ty = tcHsExpansion hse res_ty -tcExpr e@(XExpr{}) res_ty = tcApp e res_ty +tcExpr e@(XExpr (HsRecSelRn {})) res_ty = tcApp e res_ty -- Typecheck an occurrence of an unbound Id -- @@ -527,8 +530,9 @@ tcExpr (HsCase ctxt scrut matches) res_ty tcExpr (HsIf x pred b1 b2) res_ty = do { pred' <- tcCheckMonoExpr pred boolTy - ; (u1,b1') <- tcCollectingUsage $ tcMonoLExpr b1 res_ty - ; (u2,b2') <- tcCollectingUsage $ tcMonoLExpr b2 res_ty + ; let res_ty' = adjustExpTypeForCaseBranches res_ty [b1,b2] + ; (u1,b1') <- tcCollectingUsage $ tcMonoLExpr b1 res_ty' + ; (u2,b2') <- tcCollectingUsage $ tcMonoLExpr b2 res_ty' ; tcEmitBindingUsage (supUE u1 u2) ; return (HsIf x pred' b1' b2') } ===================================== compiler/GHC/Tc/Gen/Expr.hs-boot ===================================== @@ -35,6 +35,8 @@ tcInferRho, tcInferRhoNC :: tcInferRhoFRR, tcInferRhoFRRNC :: FixedRuntimeRepContext -> LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcRhoType) +tcInferExprSigma :: HsExpr GhcRn -> TcM (HsExpr GhcTc, TcSigmaType) + tcInferExpr :: InferInstFlag -> LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcType) tcSyntaxOp :: CtOrigin ===================================== compiler/GHC/Tc/Gen/Head.hs ===================================== @@ -21,15 +21,14 @@ module GHC.Tc.Gen.Head , pprArgInst, addFunResCtxt ) where -import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcExpr, tcCheckPolyExprNC, tcPolyLExprSig ) +import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcCheckPolyExprNC, tcPolyLExprSig, tcInferExprSigma ) import {-# SOURCE #-} GHC.Tc.Gen.Splice( getUntypedSpliceBody ) -import {-# SOURCE #-} GHC.Tc.Gen.App( tcExprSigma ) import GHC.Prelude import GHC.Hs import GHC.Hs.Syn.Type -import GHC.Rename.Utils (mkExpandedTc, mkExpandedExprTc) +import GHC.Rename.Utils (mkExpandedExprTc) import GHC.Tc.Gen.HsType import GHC.Tc.Gen.Bind( chooseInferredQuantifiers ) @@ -446,7 +445,7 @@ tcInferAppHead (fun,fun_lspan) do { mb_tc_fun <- tcInferAppHead_maybe fun ; case mb_tc_fun of Just (fun', fun_sigma) -> return (fun', fun_sigma) - Nothing -> runInferRho (tcExpr fun) + Nothing -> tcInferExprSigma fun } @@ -465,13 +464,14 @@ tcInferAppHead_maybe fun = case fun of -> Just <$> tcInferOverLit lit XExpr (HsRecSelRn f) -> Just <$> tcInferRecSelId f - XExpr (ExpandedThingRn (HSE o (L loc e))) - -> setSrcSpan (locA loc) $ Just <$> - do { (e', ty) <- tcExprSigma False (hsCtxtCtOrigin o) e - ; return (mkExpandedTc o (L loc e'), ty) } - -- We do not want to instantiate the type of the head as there may be - -- visible type applications in the argument. - -- c.f. T19167 + +-- XExpr (ExpandedThingRn (HSE o (L loc e))) +-- -> setSrcSpan (locA loc) $ Just <$> +-- do { (e', ty) <- tcExprSigma False (hsCtxtCtOrigin o) e +-- ; return (mkExpandedTc o (L loc e'), ty) } +-- -- We do not want to instantiate the type of the head as there may be +-- -- visible type applications in the argument. +-- -- c.f. T19167 _ -> return Nothing ===================================== compiler/GHC/Tc/Gen/Match.hs ===================================== @@ -219,10 +219,10 @@ tcMatches :: (AnnoBody body, Outputable (body GhcTc)) -> MatchGroup GhcRn (LocatedA (body GhcRn)) -> TcM (MatchGroup GhcTc (LocatedA (body GhcTc))) -tcMatches ctxt tc_body pat_tys rhs_ty (MG { mg_alts = L l matches +tcMatches ctxt tc_body pat_tys exp_ty (MG { mg_alts = L l matches , mg_ext = origin }) | null matches -- Deal with case e of {} - -- Since there are no branches, no one else will fill in rhs_ty + -- Since there are no branches, no one else will fill in exp_ty -- when in inference mode, so we must do it ourselves, -- here, using expTypeToType = do { tcEmitBindingUsage bottomUE @@ -233,17 +233,19 @@ tcMatches ctxt tc_body pat_tys rhs_ty (MG { mg_alts = L l matches [ExpForAllPatTy tvb] -> failWithTc $ TcRnEmptyCase ctxt (EmptyCaseForall tvb) [] -> panic "tcMatches: no arguments in EmptyCase" _t1:(_t2:_ts) -> panic "tcMatches: multiple arguments in EmptyCase" - ; rhs_ty <- expTypeToType rhs_ty + ; rhs_ty <- expTypeToType exp_ty ; return (MG { mg_alts = L l [] , mg_ext = MatchGroupTc [pat_ty] rhs_ty origin }) } | otherwise - = do { umatches <- mapM (tcCollectingUsage . tcMatch tc_body pat_tys rhs_ty) matches - ; let (usages, matches') = unzip umatches + = do { let exp_ty' = adjustExpTypeForCaseBranches exp_ty matches + tc_match match = tcCollectingUsage $ + tcMatch tc_body pat_tys exp_ty' match + ; (usages, matches') <- mapAndUnzipM tc_match matches ; tcEmitBindingUsage $ supUEs usages ; pat_tys <- mapM readScaledExpType (filter_out_forall_pat_tys pat_tys) - ; rhs_ty <- readExpType rhs_ty + ; rhs_ty <- readExpType exp_ty ; traceTc "tcMatches" (ppr matches' $$ ppr pat_tys $$ ppr rhs_ty) ; return (MG { mg_alts = L l matches' , mg_ext = MatchGroupTc pat_tys rhs_ty origin ===================================== compiler/GHC/Tc/Utils/TcMType.hs ===================================== @@ -63,7 +63,7 @@ module GHC.Tc.Utils.TcMType ( mkCheckExpType, newInferExpType, newInferExpTypeFRR, runInfer, runInferRho, runInferSigma, runInferKind, runInferRhoFRR, runInferSigmaFRR, readExpType, readExpType_maybe, readScaledExpType, - expTypeToType, scaledExpTypeToType, + expTypeToType, scaledExpTypeToType, adjustExpTypeForCaseBranches, checkingExpType_maybe, checkingExpType, inferResultToType, ensureMonoType, promoteTcType, @@ -499,6 +499,17 @@ inferResultToType (IR { ir_uniq = u, ir_lvl = tc_lvl ; let conc_orig = ConcreteFRR $ FixedRuntimeRepOrigin tau frr ; return tau } +adjustExpTypeForCaseBranches :: ExpRhoType -> [branch] -> ExpRhoType +-- See Note [fillInferResult: multiple branches] +adjustExpTypeForCaseBranches exp_ty branches + = case exp_ty of + Infer ir | IR { ir_inst = IIF_Sigma } <- ir + , branches `lengthAtLeast` 2 + -> Infer (ir { ir_inst = IIF_DeepRho }) + | otherwise + -> exp_ty + Check {} -> exp_ty + {- Note [inferResultToType] ~~~~~~~~~~~~~~~~~~~~~~~~~~~ expTypeToType and inferResultType convert an InferResult to a monotype. ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -426,7 +426,7 @@ Some examples: tcSkolemiseGeneral :: HasDebugCallStack - => DeepSubsumptionFlag + => DeepSubsumptionFlag -- Ignores the DeepSubsumptionDepth -> UserTypeCtxt -> TcType -> TcType -- top_ty and expected_ty -- Here, top_ty is the type we started to skolemise; used only in SigSkol @@ -1169,7 +1169,7 @@ fillInferResultNoInst act_res_ty (IR { ir_uniq = u ; return final_co } } -fillInferResult :: DeepSubsumptionFlag -> CtOrigin -> TcType -> InferResult -> TcM HsWrapper +fillInferResult :: DeepSubsumptionFlag -> CtOrigin -> TcSigmaType -> InferResult -> TcM HsWrapper -- See Note [Instantiation of InferResult] fillInferResult ds_flag ct_orig res_ty ires@(IR { ir_inst = iif }) = case iif of @@ -1203,7 +1203,7 @@ There are two things to worry about: T1 -> e1 T2 -> e2 -Our typing rules are: +In general our typing rules are: * The RHS of a existential or GADT alternative must always be a monotype, regardless of the number of alternatives. @@ -1218,17 +1218,13 @@ Our typing rules are: We use choice (2) in that Section. (GHC 8.10 and earlier used choice (1).) - But note that - case e of - True -> hr - False -> \x -> hr x - will fail, because we still /infer/ both branches, so the \x will get - a (monotype) unification variable, which will fail to unify with - (forall a. a->a) +Note [fillInferResult: GADTs and existentials] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We can detect the GADT/existential situation, case (1) of Note [fillInferResult], +by seeing that the current TcLevel is greater than that stored in ir_lvl of the +Infer ExpType. We bump the level whenever we go past a GADT/existential match. -For (1) we can detect the GADT/existential situation by seeing that -the current TcLevel is greater than that stored in ir_lvl of the Infer -ExpType. We bump the level whenever we go past a GADT/existential match. +We insist that the RHS has a monotype, regardless of the number of alternatives. Then, before filling the hole use promoteTcType to promote the type to the outer ir_lvl. promoteTcType does this @@ -1239,11 +1235,6 @@ That forces the type to be a monotype (since unification variables can only unify with monotypes); and catches skolem-escapes because the alpha is untouchable until the equality floats out. -For (2), we simply look to see if the hole is filled already. - - if not, we promote (as above) and fill the hole - - if it is filled, we simply unify with the type that is - already there - (FIR1) There is one wrinkle. Suppose we have case e of T1 -> e1 :: (forall a. a->a) -> Int @@ -1258,7 +1249,36 @@ For (2), we simply look to see if the hole is filled already. So if we check G2 second, we still want to emit a constraint that restricts the RHS to be a monotype. This is done by ensureMonoType, and it works by simply generating a constraint (alpha ~ ty), where alpha is a fresh -unification variable. We discard the evidence. + unification variable. We discard the evidence. + +Note [fillInferResult: multiple branches] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +If there are multiple case branches, case (2) of Note [fillInferResult] +we simply look to see if the hole is filled already. + - if not, we promote (as above) and fill the hole + - if it is filled, we simply unify with the type that is already there + +But consider + case x of + True -> True + False -> error "urk" +and suppose we call `tcInferSigma` on this expression, so that the `ir_inst` +field of the expected result type is `IIF_Sigma`. The danger is that we'll +fill the hole with `Bool` (from the `True`) and then reject when we try to +unify that with `forall a. a->a`, from the call to `error`. + +To avoid this, we never infer a sigma-type from a multi-branch `case`. Instead +we just zap the `IIF_Sigma` to `IIF_DeepRho` when walking inside the branches +of multi-arm case-expression, or an if-expression. See calls to +`adjustExpTypeForCaseBranches`. + +Note that + case e of + True -> hr + False -> \x -> hr x + where hr :: (forall a. a->a) -> Int +will fail, because we still /infer/ both branches, so the \x will get a +(monotype) unification variable, which will fail to unify with (forall a. a->a) Note [Instantiation of InferResult] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2068,17 +2088,20 @@ getDeepSubsumptionFlag = -- | 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 - ; traceTc "getDeepSubsumptionFlag_DataConHead" (ppr app_head) - ; return $ - if | user_ds - -> Deep DeepSub - | XExpr (ConLikeTc (RealDataCon {})) <- app_head - -> Deep TopSub - | otherwise - -> Shallow - } +getDeepSubsumptionFlag_DataConHead app_head + = do { user_ds <- xoptM LangExt.DeepSubsumption + ; return $ if | user_ds -> Deep DeepSub + | dc_head app_head -> Deep TopSub + | otherwise -> Shallow } + where + dc_head (XExpr (ConLikeTc (RealDataCon {}))) = True + dc_head (XExpr (WrapExpr _ f)) = dc_head f + dc_head (HsApp _ (L _ f) _) = dc_head f + dc_head (HsAppType _ (L _ f) _) = dc_head f + dc_head (OpApp _ _ (L _ f) _) = dc_head f + dc_head (HsPar _ (L _ f)) = dc_head f + dc_head _ = False + -- | 'tc_sub_type_deep' is where the actual work happens for deep subsumption. -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6986cae3bb35153090fa566d1f88043b... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6986cae3bb35153090fa566d1f88043b... You're receiving this email because of your account on gitlab.haskell.org.