Simon Peyton Jones pushed to branch wip/ani/tc-expand at Glasgow Haskell Compiler / GHC Commits: 87447590 by Simon Peyton Jones at 2026-03-26T13:04:10+00:00 Fixes from Simon [skip ci] ..need documentation. - - - - - 7 changed files: - compiler/GHC/Tc/Gen/App.hs - compiler/GHC/Tc/Gen/Expr.hs - compiler/GHC/Tc/Gen/Head.hs - compiler/GHC/Tc/Gen/Match.hs - compiler/GHC/Tc/Utils/TcMType.hs - compiler/GHC/Tc/Utils/TcType.hs - compiler/GHC/Tc/Utils/Unify.hs Changes: ===================================== compiler/GHC/Tc/Gen/App.hs ===================================== @@ -1915,8 +1915,12 @@ quickLookArg1 pos app_lspan (fun, fun_lspan) larg@(L _ arg) sc_arg_ty@(Scaled _ -- generated by calls in arg do { ((rn_fun_arg, fun_lspan_arg), rn_args) <- splitHsApps arg + ; if tooComplicatedForQuickLook rn_fun_arg + then skipQuickLook app_lspan larg sc_arg_ty + else + -- Step 1: get the type of the head of the argument - ; (fun_ue, (tc_fun_arg_head, fun_sigma_arg_head)) <- tcCollectingUsage $ tcInferExprSigma rn_fun_arg + do { (fun_ue, (tc_fun_arg_head, fun_sigma_arg_head)) <- tcCollectingUsage $ tcInferExprSigma rn_fun_arg -- tcCollectingUsage: the use of an Id at the head generates usage-info -- See the call to `tcEmitBindingUsage` in `check_local_id`. So we must -- capture and save it in the `EValArgQL`. See (QLA6) in @@ -1978,7 +1982,7 @@ quickLookArg1 pos app_lspan (fun, fun_lspan) larg@(L _ arg) sc_arg_ty@(Scaled _ , eaql_wanted = wanted , eaql_encl = arg_influences_enclosing_call , eaql_res_rho = app_res_rho }) - } + }} mk_origin :: SrcSpan -- SrcSpan of the function @@ -1999,6 +2003,16 @@ mk_origin fun_lspan rn_fun } +tooComplicatedForQuickLook :: HsExpr GhcRn -> Bool +tooComplicatedForQuickLook expr + = case expr of + HsVar {} -> False + ExprWithTySig {} -> False + XExpr (HsRecSelRn {}) -> False + HsOverLit {} -> False + _ -> True -- Too complicated + + {- ********************************************************************* * * Folding over instantiation variables ===================================== compiler/GHC/Tc/Gen/Expr.hs ===================================== @@ -323,6 +323,7 @@ tcExpr :: HsExpr GhcRn -- Se Note [Typechecking by expansion: overview] tcExpr e@(HsVar _ v_rn) res_ty = do { (v_tc, sigma_ty) <- tcInferId v_rn + ; traceTc "tcExpr:HsVar" (ppr v_tc <+> dcolon <+> ppr sigma_ty $$ ppr res_ty) ; tcWrapResult e v_tc sigma_ty res_ty } tcExpr e@(ExprWithTySig _ e_rn e_ty) res_ty @@ -545,8 +546,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/Head.hs ===================================== @@ -232,6 +232,7 @@ splitHsApps e = go e noSrcSpan [] go (HsAppType _ (L l fun) ty) lspan args = go fun (locA l) (mkETypeArg lspan ty : args) go (HsApp _ (L l fun) arg) lspan args = go fun (locA l) (mkEValArg lspan arg : args) +{- -- See Note [Looking through Template Haskell splices in splitHsApps] go e@(HsUntypedSplice splice_res splice) _ args = do { fun <- getUntypedSpliceBody splice_res @@ -242,6 +243,7 @@ splitHsApps e = go e noSrcSpan [] HsUntypedSpliceExpr _ (L l _) -> locA l -- l :: SrcAnn AnnListItem HsQuasiQuote _ _ (L l _) -> locA l -- l :: SrcAnn NoEpAnns (XUntypedSplice (HsImplicitLiftSplice _ _ _ (L l _))) -> locA l +-} -- See Note [Desugar OpApp in the typechecker] go e@(OpApp _ arg1 (L l op) arg2) _ args @@ -342,6 +344,8 @@ where Note [Looking through ExpandedThingRn] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +**** TODO **** this note is out of date. Fix me. + When creating an application chain in splitHsApps, we must deal with ExpandedThingRn f1 (f `HsApp` e1) `HsApp` e2 `HsApp` e3 ===================================== 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/TcType.hs ===================================== @@ -441,11 +441,12 @@ data InferInstFlag -- Specifies whether the inference should return an uninstan | IIF_ShallowRho -- Trying to infer a shallow RhoType (no foralls or => at the top) -- Top-instantiate (only, regardless of DeepSubsumption) before filling the hole - -- Typically used when inferring the type of an expression + -- Used only for view patterns; see Note [View patterns and polymorphism] | IIF_DeepRho -- Trying to infer a possibly-deep RhoType (depending on DeepSubsumption) -- If DeepSubsumption is off, same as IIF_ShallowRho -- If DeepSubsumption is on, instantiate deeply before filling the hole + -- Typically used when inferring the type of an expression type ExpSigmaType = ExpType type ExpRhoType = ExpType ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -1197,13 +1197,15 @@ There are two things to worry about: 1. What if it is under a GADT or existential pattern match? - GADTs: a unification variable (and Infer's hole is similar) is untouchable - Existentials: be careful about skolem-escape + See Note [fillInferResult: GADTs and existentials] 2. What if it is filled in more than once? E.g. multiple branches of a case case e of T1 -> e1 T2 -> e2 + See Note [fillInferResult: multiple branches] -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 +1220,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 +1237,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 +1251,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] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1316,7 +1338,7 @@ HOWEVER, not always! Here are places where we want `IIF_Sigma` meaning but /not/ deeply instantiate (#26331). See Note [View patterns and polymorphism] in GHC.Tc.Gen.Pat. This the only place we use IIF_ShallowRho. -Why do we want to deeply instantiate, ever? Why isn't top-instantiation enough? +Why do we want to /deeply/ instantiate, ever? Why isn't top-instantiation enough? Answer: to accept the following program (T26225b) with -XDeepSubsumption, we need to deeply instantiate when inferring in checkResultTy: View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/87447590958fad8c6209f444140b6f0b... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/87447590958fad8c6209f444140b6f0b... You're receiving this email because of your account on gitlab.haskell.org.