Apoorv Ingle pushed to branch wip/ani/better-expansion at Glasgow Haskell Compiler / GHC Commits: a091fcbb by Apoorv Ingle at 2026-04-01T09:43:04-05:00 Do expansions properly - move splitHsTypes out of tcApp - splitHsApps now looks through HsExpansions - create a new file for expansions Co-authored-by: simonpj - - - - - 11 changed files: - compiler/GHC/Tc/Gen/App.hs - − compiler/GHC/Tc/Gen/App.hs-boot - + compiler/GHC/Tc/Gen/Expand.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 - compiler/ghc.cabal.in - testsuite/tests/partial-sigs/should_compile/SplicesUsed.stderr Changes: ===================================== compiler/GHC/Tc/Gen/App.hs ===================================== @@ -11,7 +11,6 @@ module GHC.Tc.Gen.App ( tcApp - , tcExprSigma , tcExprPrag ) where import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcPolyExpr ) @@ -165,34 +164,6 @@ Note [Instantiation variables are short lived] -} -{- ********************************************************************* -* * - tcInferSigma -* * -********************************************************************* -} - --- Very similar to tcApp, but returns a sigma (uninstantiated) type --- CAUTION: Any changes to tcApp should be reflected here --- cf. T19167. the head is an expanded expression applied to a type --- Caution: Currently we assume that the expression is compiler generated/expanded --- Because that is what T19167 test case expects. --- This function should go away after MR!15778 lands -tcExprSigma :: Bool -> CtOrigin -> HsExpr GhcRn -> TcM (HsExpr GhcTc, TcSigmaType) -tcExprSigma inst fun_orig rn_expr - = do { (fun@(rn_fun,fun_lspan), rn_args) <- splitHsApps rn_expr - ; do_ql <- wantQuickLook rn_fun - ; (tc_fun, fun_sigma) <- tcInferAppHead fun - ; inGenCode <- inGeneratedCode - ; traceTc "tcExprSigma" (vcat [ text "rn_expr:" <+> ppr rn_expr - , text "tc_fun" <+> ppr tc_fun - , text "inGeneratedCode:" <+> ppr inGenCode]) - ; (inst_args, app_res_sigma) <- tcInstFun do_ql inst (fun_orig, rn_fun, fun_lspan) - tc_fun fun_sigma rn_args - ; tc_args <- tcValArgs do_ql (rn_fun, fun_lspan) inst_args - ; let tc_expr = rebuildHsApps (tc_fun, fun_lspan) tc_args - ; return (tc_expr, app_res_sigma) } - - {- ********************************************************************* * * Typechecking n-ary applications @@ -379,24 +350,22 @@ Unify result type /before/ typechecking the args The latter is much better. That is why we call `checkResultTy` before tcValArgs. -} --- CAUTION: Any changes to tcApp should be reflected in tcExprSigma -tcApp :: HsExpr GhcRn + +-------------------- +tcApp :: HsExpr GhcRn -- The whole application + -> HsExpr GhcRn -> [HsExprArg 'TcpRn] -- Function and arguments -> ExpRhoType -- When checking, -XDeepSubsumption <=> deeply skolemised -> TcM (HsExpr GhcTc) -- See Note [tcApp: typechecking applications] -tcApp rn_expr exp_res_ty - = do { -- Step 1: Split the application chain - (fun@(rn_fun, fun_lspan), rn_args) <- splitHsApps rn_expr - ; inGenCode <- inGeneratedCode +tcApp rn_expr rn_fun rn_args exp_res_ty + = do { fun_lspan <- getFunSrcSpan rn_args ; traceTc "tcApp {" $ - vcat [ text "generated? " <+> ppr inGenCode - , text "rn_expr:" <+> ppr rn_expr - , text "rn_fun:" <+> ppr rn_fun + vcat [ text "rn_fun:" <+> ppr rn_fun , text "fun_lspan:" <+> ppr fun_lspan , text "rn_args:" <+> ppr rn_args ] -- Step 2: Infer the type of `fun`, the head of the application - ; (tc_fun, fun_sigma) <- tcInferAppHead fun + ; (tc_fun, fun_sigma) <- tcInferAppHead (rn_fun, fun_lspan) ; let tc_head = (tc_fun, fun_lspan) -- inst_final: top-instantiate the result type of the application, -- EXCEPT if we are trying to infer a sigma-type @@ -411,22 +380,12 @@ tcApp rn_expr exp_res_ty -- Step 3.1: Instantiate the function type (taking a quick look at args) ; do_ql <- wantQuickLook rn_fun - -- Setp 3.2 Set the correct origin to blame for the error message - -- What should be the origin for this function call? - -- If the head of the function is user written - -- then it can be used in the error message - -- If it is generated code location span, blame it on the - -- origin that can be retrived from the top of the error ctxt stack. - -- See Note [Error contexts in generated code] - ; fun_orig <- mk_origin fun_lspan rn_fun - ; traceTc "tcApp:inferAppHead" $ vcat [ text "tc_fun:" <+> ppr tc_fun , text "fun_sigma:" <+> ppr fun_sigma - , text "fun_origin" <+> ppr fun_orig , text "do_ql:" <+> ppr do_ql] ; (inst_args, app_res_rho) - <- tcInstFun do_ql inst_final (fun_orig, rn_fun, fun_lspan) tc_fun fun_sigma rn_args + <- tcInstFun do_ql inst_final (rn_fun, fun_lspan) tc_fun fun_sigma rn_args -- See (TCAPP1) and (TCAPP2) in -- Note [tcApp: typechecking applications] @@ -440,7 +399,7 @@ tcApp rn_expr exp_res_ty -- Step 4.2: typecheck the arguments ; tc_args <- tcValArgs NoQL (rn_fun, fun_lspan) inst_args -- Step 4.3: wrap up - ; finishApp tc_head tc_args app_res_rho res_wrap } + ; finishApp tc_fun tc_args app_res_rho res_wrap } DoQL -> do { traceTc "tcApp:DoQL" (ppr rn_fun $$ ppr app_res_rho) @@ -458,7 +417,7 @@ tcApp rn_expr exp_res_ty ; res_wrap <- checkResultTy rn_expr tc_head inst_args app_res_rho exp_res_ty -- Step 5.5: wrap up - ; finishApp tc_head tc_args app_res_rho res_wrap } } + ; finishApp tc_fun tc_args app_res_rho res_wrap } } quickLookResultType :: TcRhoType -> ExpRhoType -> TcM () -- This function implements the shaded bit of rule APP-Downarrow in @@ -466,16 +425,16 @@ quickLookResultType :: TcRhoType -> ExpRhoType -> TcM () quickLookResultType app_res_rho (Check exp_rho) = qlUnify app_res_rho exp_rho quickLookResultType _ _ = return () -finishApp :: (HsExpr GhcTc, SrcSpan) -> [HsExprArg 'TcpTc] +finishApp :: HsExpr GhcTc -> [HsExprArg 'TcpTc] -> TcRhoType -> HsWrapper -> TcM (HsExpr GhcTc) -- Do final checks and wrap up the result -finishApp tc_head@(tc_fun,_) tc_args app_res_rho res_wrap +finishApp tc_fun tc_args app_res_rho res_wrap = do { -- Reconstruct, with a 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) + then tcTagToEnum tc_fun tc_args app_res_rho + else return (rebuildHsApps tc_fun tc_args) ; traceTc "End tcApp }" (ppr tc_fun) ; return (mkHsWrap res_wrap res_expr) } @@ -488,11 +447,12 @@ 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) +checkResultTy rn_expr (tc_fun,_) _ app_res_rho (Infer inf_res) = do { ds_flag <- getDeepSubsumptionFlag_DataConHead tc_fun + -- Why the "DataConHead" bit? See (IIR5) in + -- Note [Instantiation of InferResult] in GHC.Tc.Utils.Unify. ; fillInferResult ds_flag (exprCtOrigin rn_expr) app_res_rho inf_res } - checkResultTy rn_expr (tc_fun, fun_loc) inst_args app_res_rho (Check res_ty) -- Unify with expected type from the context -- See Note [Unify with expected type before typechecking arguments] @@ -561,7 +521,7 @@ tcValArgs do_ql (fun, fun_lspan) args = go do_ql 0 args | EValArgQL{} <- arg = pos + 1 | ETypeArg{ ea_loc_span = l } <- arg - , not (isGeneratedSrcSpan l) + , not (isGeneratedSrcSpan (locA l)) = pos + 1 | otherwise = pos @@ -618,7 +578,7 @@ tcValArg _ pos (fun, fun_lspan) (EValArgQL { , eaql_loc_span = lspan , eaql_arg_ty = sc_arg_ty , eaql_larg = larg@(L arg_loc rn_expr) - , eaql_tc_fun = tc_head + , eaql_tc_fun = tc_head@(tc_fun,_) , eaql_rn_fun = rn_fun , eaql_fun_ue = head_ue , eaql_args = inst_args @@ -636,7 +596,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 -> @@ -656,7 +617,7 @@ tcValArg _ pos (fun, fun_lspan) (EValArgQL { ; app_res_rho <- liftZonkM $ zonkTcType app_res_rho ; res_wrap <- checkResultTy rn_expr tc_head inst_args app_res_rho (mkCheckExpType exp_arg_rho) - ; finishApp tc_head tc_args app_res_rho res_wrap } + ; finishApp tc_fun tc_args app_res_rho res_wrap } ; traceTc "tcEValArgQL }" $ vcat [ text "app_res_rho:" <+> ppr app_res_rho ] @@ -690,26 +651,48 @@ tcInstFun :: QLFlag -- always return a rho-type (but not a deep-rho type) -- Generally speaking we pass in True; in Fig 5 of the paper -- |-inst returns a rho-type - -> (CtOrigin, HsExpr GhcRn, SrcSpan) + -> (HsExpr GhcRn, SrcSpan) -> HsExpr GhcTc -> TcSigmaType -> [HsExprArg 'TcpRn] -> TcM ( [HsExprArg 'TcpInst] , TcSigmaType ) -- Does not instantiate trailing invisible foralls --- This crucial function implements the |-inst judgement in Fig 4, plus the --- modification in Fig 5, of the QL paper: +-- This crucial function implements the |-inst judgement in Fig 4, +-- plus the modification in Fig 5, of the QL paper: -- "A quick look at impredicativity" (ICFP'20). -tcInstFun do_ql inst_final (fun_orig, rn_fun, fun_lspan) tc_fun fun_sigma rn_args - = do { traceTc "tcInstFun" (vcat [ text "origin" <+> ppr fun_orig - , text "tc_fun" <+> ppr tc_fun +tcInstFun do_ql inst_final rn_head@(_, fun_lspan) tc_fun fun_sigma rn_args + = do { traceTc "tcInstFun" (vcat [ text "tc_fun" <+> ppr tc_fun + , text "rn_fun" <+> ppr rn_head , text "fun_sigma" <+> ppr fun_sigma , text "args:" <+> ppr rn_args - , text "do_ql" <+> ppr do_ql - , text "ctx" <+> ppr fun_lspan]) - ; res@(_, fun_ty) <- go 1 [] fun_sigma rn_args + , text "do_ql" <+> ppr do_ql]) + ; fun_origin <- mk_origin rn_head + ; res@(_, fun_ty) <- go fun_origin 1 [] fun_sigma rn_args ; traceTc "tcInstFun:ret" (ppr fun_ty) ; return res } where + -- What should be the origin for this function call? + -- If the head of the function is user written + -- then it can be used in the error message + -- If it is generated code location span, blame it on the + -- origin that can be retrived from the top of the error ctxt stack. + -- See Note [Error contexts in generated code] + mk_origin :: (HsExpr GhcRn, SrcSpan) -- The head of the application chain and its location + -> TcM CtOrigin + mk_origin (rn_fun, fun_lspan) + | not (isGeneratedSrcSpan fun_lspan) + = return $ exprCtOrigin rn_fun + + | otherwise -- If the location is generated, the best we can do is to + -- approximate by looking on top of the error message stack + = do { err_ctxt_stack <- getErrCtxt + ; let hs_ctxt = case err_ctxt_stack of + (c:_) -> c + [] -> pprPanic "mk_origin" (ppr rn_fun) + ; traceTc "mk_origin" (pprHsCtxt hs_ctxt) + ; return $ hsCtxtCtOrigin hs_ctxt + } + -- These are the type variables which must be instantiated to concrete -- types. See Note [Representation-polymorphic Ids with no binding] -- in GHC.Tc.Utils.Concrete @@ -741,34 +724,35 @@ tcInstFun do_ql inst_final (fun_orig, rn_fun, fun_lspan) tc_fun fun_sigma rn_arg inst_fun _ = isInferredForAllTyFlag ----------- - go, go1 :: Int -- Value-argument position of next arg + go, go1 :: CtOrigin -- Of the function + -> Int -- Value-argument position of next arg -> [HsExprArg 'TcpInst] -- Accumulator, reversed -> TcSigmaType -> [HsExprArg 'TcpRn] -> TcM ([HsExprArg 'TcpInst], TcSigmaType) -- go: If fun_ty=kappa, look it up in Theta - go pos acc fun_ty args + go fun_orig pos acc fun_ty args | Just kappa <- getTyVar_maybe fun_ty , isQLInstTyVar kappa = do { cts <- readMetaTyVar kappa ; case cts of - Indirect fun_ty' -> go pos acc fun_ty' args - Flexi -> go1 pos acc fun_ty args } + Indirect fun_ty' -> go fun_orig pos acc fun_ty' args + Flexi -> go1 fun_orig pos acc fun_ty args } | otherwise - = go1 pos acc fun_ty args + = go1 fun_orig pos acc fun_ty args -- go1: fun_ty is not filled-in instantiation variable -- ('go' dealt with that case) -- Handle out-of-scope functions gracefully - go1 pos acc fun_ty (arg : rest_args) + go1 fun_orig pos acc fun_ty (arg : rest_args) | fun_is_out_of_scope, looks_like_type_arg arg -- See Note [VTA for out-of-scope functions] - = go pos acc fun_ty rest_args + = go fun_orig pos acc fun_ty rest_args -- Rule IALL from Fig 4 of the QL paper; applies even if args = [] -- Instantiate invisible foralls and dictionaries. -- c.f. GHC.Tc.Utils.Instantiate.topInstantiate - go1 pos acc fun_ty args + go1 fun_orig pos acc fun_ty args | (tvs, body1) <- tcSplitSomeForAllTyVars (inst_fun args) fun_ty , (theta, body2) <- if inst_fun args Inferred then tcSplitPhiTy body1 @@ -797,12 +781,12 @@ tcInstFun do_ql inst_final (fun_orig, rn_fun, fun_lspan) tc_fun fun_sigma rn_arg -- argument of (#,#) to @LiftedRep, but want to rule out the -- second instantiation @r. - ; go pos (addArgWrap wrap acc) fun_rho args } + ; go fun_orig pos (addArgWrap wrap acc) fun_rho args } -- Going around again means we deal easily with -- nested forall a. Eq a => forall b. Show b => blah -- Rule IRESULT from Fig 4 of the QL paper; no more arguments - go1 _pos acc fun_ty [] + go1 _fun_orig _pos acc fun_ty [] | XExpr (ConLikeTc (RealDataCon dc)) <- tc_fun , isNewDataCon dc , [Scaled _ orig_arg_ty] <- dataConOrigArgTys dc @@ -822,30 +806,30 @@ tcInstFun do_ql inst_final (fun_orig, rn_fun, fun_lspan) tc_fun fun_sigma rn_arg = return (reverse acc, fun_ty) -- Rule ITVDQ from the GHC Proposal #281 - go1 pos acc fun_ty ((EValArg { ea_arg = arg }) : rest_args) + go1 fun_orig pos acc fun_ty ((EValArg { ea_arg = arg }) : rest_args) | Just (tvb, body) <- tcSplitForAllTyVarBinder_maybe fun_ty = assertPpr (binderFlag tvb == Required) (ppr fun_ty $$ ppr arg) $ -- Any invisible binders have been instantiated by IALL above, -- so this forall must be visible (i.e. Required) do { (ty_arg, inst_body) <- tcVDQ fun_conc_tvs (tvb, body) arg ; let wrap = mkWpTyApps [ty_arg] - ; go (pos+1) (addArgWrap wrap acc) inst_body rest_args } + ; go fun_orig (pos+1) (addArgWrap wrap acc) inst_body rest_args } - go1 pos acc fun_ty (EWrap w : args) - = go1 pos (EWrap w : acc) fun_ty args + go1 fun_orig pos acc fun_ty (EWrap w : args) + = go1 fun_orig pos (EWrap w : acc) fun_ty args - go1 pos acc fun_ty (EPrag sp prag : args) - = go1 pos (EPrag sp prag : acc) fun_ty args + go1 fun_orig pos acc fun_ty (EPrag sp prag : args) + = go1 fun_orig pos (EPrag sp prag : acc) fun_ty args -- Rule ITYARG from Fig 4 of the QL paper - go1 pos acc fun_ty ( ETypeArg { ea_loc_span = ctxt, ea_hs_ty = hs_ty } - : rest_args ) + go1 fun_orig pos acc fun_ty ( ETypeArg { ea_loc_span = ctxt, ea_hs_ty = hs_ty } + : rest_args ) = do { (ty_arg, inst_ty) <- tcVTA fun_conc_tvs fun_ty hs_ty ; let arg' = ETypeArg { ea_loc_span = ctxt, ea_hs_ty = hs_ty, ea_ty_arg = ty_arg } - ; go pos (arg' : acc) inst_ty rest_args } + ; go fun_orig pos (arg' : acc) inst_ty rest_args } -- Rule IVAR from Fig 4 of the QL paper: - go1 pos acc fun_ty args@(EValArg {} : _) + go1 fun_orig pos acc fun_ty args@(EValArg {} : _) | Just kappa <- getTyVar_maybe fun_ty , isQLInstTyVar kappa = -- Function type was of form f :: forall a b. t1 -> t2 -> b @@ -861,7 +845,7 @@ tcInstFun do_ql inst_final (fun_orig, rn_fun, fun_lspan) tc_fun fun_sigma rn_arg -- - We must be sure to actually update the variable right now, -- not defer in any way, because this is a QL instantiation variable. -- It's easier just to do the job directly here. - do { arg_tys <- zipWithM new_arg_ty (leadingValArgs args) [pos..] + do { arg_tys <- zipWithM (new_arg_ty fun_orig) (leadingValArgs args) [pos..] ; res_ty <- newOpenFlexiTyVarTyQL do_ql TauTv ; let fun_ty' = mkScaledFunTys arg_tys res_ty @@ -877,12 +861,12 @@ tcInstFun do_ql inst_final (fun_orig, rn_fun, fun_lspan) tc_fun fun_sigma rn_arg -- Then fun_ty :: kk, fun_ty' :: Type, kind_co :: Type ~ kk -- co_wrap :: (fun_ty' |> kind_co) ~ fun_ty' - ; go pos acc' fun_ty' args } + ; go fun_orig pos acc' fun_ty' args } -- Rule IARG from Fig 4 of the QL paper: - go1 pos acc fun_ty + go1 fun_orig pos acc fun_ty (EValArg { ea_arg = arg, ea_loc_span = ctxt } : rest_args) - = do { let herald = mk_herald tc_fun (unLoc arg) + = do { let herald = mk_herald fun_orig tc_fun (unLoc arg) ; (fun_co, arg_ty, res_ty) <- -- NB: matchActualFunTy does the rep-poly check. -- For example, suppose we have f :: forall r (a::TYPE r). a -> Int @@ -894,16 +878,15 @@ 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_head arg arg_ty ; let acc' = arg' : addArgWrap (mkWpCastN fun_co) acc - ; go (pos+1) acc' res_ty rest_args } + ; go fun_orig (pos+1) acc' res_ty rest_args } - new_arg_ty :: LHsExpr GhcRn -> Int -> TcM (Scaled TcType) + new_arg_ty :: CtOrigin -> LHsExpr GhcRn -> Int -> TcM (Scaled TcType) -- Make a fresh nus for each argument in rule IVAR - new_arg_ty (L _ arg) i + new_arg_ty fun_orig (L _ arg) i = do { arg_nu <- newArgTyVarTyQL do_ql $ - FRRExpectedFunTy (mk_herald tc_fun arg) i + FRRExpectedFunTy (mk_herald fun_orig tc_fun arg) i -- Following matchActualFunTy, we create nu_i :: TYPE kappa_i[conc], -- thereby ensuring that the arguments have concrete runtime representations @@ -913,12 +896,13 @@ tcInstFun do_ql inst_final (fun_orig, rn_fun, fun_lspan) tc_fun fun_sigma rn_arg ; return (mkScaled mult_ty arg_nu) } - mk_herald :: HsExpr GhcTc -> HsExpr GhcRn -> ExpectedFunTyCtxt - mk_herald tc_fun arg + mk_herald :: CtOrigin -> HsExpr GhcTc -> HsExpr GhcRn -> ExpectedFunTyCtxt + mk_herald fun_orig tc_fun arg = case fun_orig of DoStmtOrigin -> ExpectedFunTySyntaxOp DoStmtOrigin tc_fun _ -> ExpectedFunTyArg (HsExprTcThing tc_fun) arg + -- Is the argument supposed to instantiate a forall? -- -- In other words, given a function application `fn arg`, @@ -1883,23 +1867,23 @@ This turned out to be more subtle than I expected. Wrinkles: -} -quickLookArg :: DeepSubsumptionFlag -> QLFlag -> Int - -> SrcSpan -- ^ location span of the whole application +quickLookArg :: QLFlag -> Int + -> HsExprLoc -- ^ 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 { is_rho <- qlArgHasRhoType (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 else quickLookArg1 pos app_lspan fun_and_lspan larg orig_arg_ty } -skipQuickLook :: SrcSpan -> LHsExpr GhcRn -> Scaled TcRhoType +skipQuickLook :: HsExprLoc -> LHsExpr GhcRn -> Scaled TcRhoType -> TcM (HsExprArg 'TcpInst) skipQuickLook app_lspan larg arg_ty = return (EValArg { ea_loc_span = app_lspan @@ -1910,13 +1894,26 @@ 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 +qlArgHasRhoType :: TcType -> TcM Bool +-- `qlArgHasRhoType` checks that the expected argument type in rule +-- App-lightning-bolt (Fig 5 in the paper) is indeed a rho-type. +-- +-- It must apply the current QL substitution, so it any QLInstTyVar that it +-- comes across. Why? See Section 5.7 in the paper; argument order matters. +-- +-- What if we find an /un-filled/ QLInstVar? We treat this as a rho-type +-- even though a later argument might force it to be sigma-type. See +-- Section 9 in the paper. +-- +-- With -XDeepSubsunption we need a /deep/ rho-type. +-- (We don't need getDeepSubsumptionFlag_DataConHead here because this +-- is only about QuickLook.) -tcIsDeepRho ds_flag = go +qlArgHasRhoType ty + = do { ds_flag <- getDeepSubsumptionFlag + ; go ds_flag ty } where - go ty + go ds_flag ty | isSigmaTy ty = return False @@ -1924,12 +1921,12 @@ tcIsDeepRho ds_flag = go , isQLInstTyVar kappa = do { info <- readMetaTyVar kappa ; case info of - Indirect arg_ty' -> go arg_ty' + Indirect arg_ty' -> go ds_flag arg_ty' Flexi -> return True } | Deep {} <- ds_flag , Just (_, res_ty) <- tcSplitFunTy_maybe ty - = go res_ty + = go ds_flag res_ty | otherwise = return True @@ -1940,14 +1937,20 @@ isGuardedTy ty | Just {} <- tcSplitAppTy_maybe ty = True | otherwise = False -quickLookArg1 :: Int -> SrcSpan -> (HsExpr GhcRn, SrcSpan) -> LHsExpr GhcRn +quickLookArg1 :: Int -> HsExprLoc -> (HsExpr GhcRn, SrcSpan) -> LHsExpr GhcRn -> Scaled TcRhoType -- Deeply skolemised -> TcM (HsExprArg 'TcpInst) -- quickLookArg1 implements the "QL Argument" judgement in Fig 5 of the paper quickLookArg1 pos app_lspan (fun, fun_lspan) larg@(L _ arg) sc_arg_ty@(Scaled _ orig_arg_rho) = addArgCtxt pos (fun, fun_lspan) larg $ -- Context needed for constraints - -- generated by calls in arg - do { ((rn_fun_arg, fun_lspan_arg), rn_args) <- splitHsApps arg + -- generated by calls in arg + do { traceTc "qla1" (ppr arg) + + ; (rn_fun_arg, rn_args) <- splitHsApps arg + + ; traceTc "qla2" (ppr arg) + + ; fun_lspan_arg <- getFunSrcSpan rn_args -- Step 1: get the type of the head of the argument ; (fun_ue, mb_fun_ty) <- tcCollectingUsage $ tcInferAppHead_maybe rn_fun_arg @@ -1970,17 +1973,15 @@ quickLookArg1 pos app_lspan (fun, fun_lspan) larg@(L _ arg) sc_arg_ty@(Scaled _ do { let arg_tc_head = (tc_fun_arg_head, fun_lspan_arg) ; do_ql <- wantQuickLook rn_fun_arg - ; arg_orig <- mk_origin fun_lspan_arg rn_fun_arg ; ((inst_args, app_res_rho), wanted) <- captureConstraints $ - tcInstFun do_ql True (arg_orig, rn_fun_arg, fun_lspan_arg) tc_fun_arg_head fun_sigma_arg_head rn_args + tcInstFun do_ql True (rn_fun_arg, fun_lspan_arg) tc_fun_arg_head fun_sigma_arg_head rn_args -- We must capture type-class and equality constraints here, but -- not usage information. See (QLA6) in Note [Quick Look at -- value arguments] ; traceTc "quickLookArg 2" $ vcat [ text "arg:" <+> ppr arg - , text "orig:" <+> ppr arg_orig , text "orig_arg_rho:" <+> ppr orig_arg_rho , text "app_res_rho:" <+> ppr app_res_rho ] @@ -2018,24 +2019,6 @@ quickLookArg1 pos app_lspan (fun, fun_lspan) larg@(L _ arg) sc_arg_ty@(Scaled _ , eaql_res_rho = app_res_rho }) }}} -mk_origin :: SrcSpan -- SrcSpan of the function - -> HsExpr GhcRn -- The head of the expression application chain - -> TcM CtOrigin -mk_origin fun_lspan rn_fun - | not (isGeneratedSrcSpan fun_lspan) - = return $ exprCtOrigin rn_fun - - | otherwise -- If the location is generated, the best we can do is to - -- approximate by looking on top of the error message stack - = do { err_ctxt_stack <- getErrCtxt - ; let hs_ctxt = case err_ctxt_stack of - (c:_) -> c - [] -> pprPanic "mk_origin" (ppr rn_fun) - ; traceTc "mk_origin" (pprHsCtxt hs_ctxt) - ; return $ hsCtxtCtOrigin hs_ctxt - } - - {- ********************************************************************* * * Folding over instantiation variables @@ -2437,12 +2420,11 @@ isTagToEnum :: HsExpr GhcTc -> Bool isTagToEnum (HsVar _ (L _ fun_id)) = fun_id `hasKey` tagToEnumKey isTagToEnum _ = False -tcTagToEnum :: (HsExpr GhcTc, SrcSpan) -> [HsExprArg 'TcpTc] - -> TcRhoType +tcTagToEnum :: HsExpr GhcTc -> [HsExprArg 'TcpTc] -> TcRhoType -> TcM (HsExpr GhcTc) -- tagToEnum# :: forall a. Int# -> a -- See Note [tagToEnum#] Urgh! -tcTagToEnum (tc_fun, fun_lspan) tc_args res_ty +tcTagToEnum tc_fun tc_args res_ty | [val_arg] <- dropWhile (not . isHsValArg) tc_args = do { res_ty <- liftZonkM $ zonkTcType res_ty @@ -2464,14 +2446,14 @@ tcTagToEnum (tc_fun, fun_lspan) tc_args res_ty ; let rep_ty = mkTyConApp rep_tc rep_args tc_fun' = mkHsWrap (WpTyApp rep_ty) tc_fun df_wrap = mkWpCastR (mkSymCo coi) - tc_expr = rebuildHsApps (tc_fun', fun_lspan) [val_arg] + tc_expr = rebuildHsApps tc_fun' [val_arg] ; return (mkHsWrap df_wrap tc_expr) }}}}} | otherwise = failWithTc TcRnTagToEnumMissingValArg where - vanilla_result = return (rebuildHsApps (tc_fun, fun_lspan) tc_args) + vanilla_result = return (rebuildHsApps tc_fun tc_args) check_enumeration ty' tc | -- isTypeDataTyCon: see wrinkle (W1) in ===================================== compiler/GHC/Tc/Gen/App.hs-boot deleted ===================================== @@ -1,12 +0,0 @@ -module GHC.Tc.Gen.App where - -import GHC.Hs ( HsExpr ) -import GHC.Tc.Types ( TcM ) -import GHC.Tc.Types.Origin ( CtOrigin ) -import GHC.Tc.Utils.TcType ( TcSigmaType ) -import GHC.Hs.Extension ( GhcRn, GhcTc ) - - -import GHC.Prelude (Bool) - -tcExprSigma :: Bool -> CtOrigin -> HsExpr GhcRn -> TcM (HsExpr GhcTc, TcSigmaType) ===================================== compiler/GHC/Tc/Gen/Expand.hs ===================================== @@ -0,0 +1,107 @@ +{-# LANGUAGE TypeFamilies #-} + +{- +(c) The University of Glasgow 2006 +(c) The GRASP/AQUA Project, Glasgow University, 1992-1998 +-} + +module GHC.Tc.Gen.Expand( tcExpand ) where + +import GHC.Prelude + +import {-# SOURCE #-} GHC.Tc.Gen.Splice( getUntypedSpliceBody ) + +import GHC.Hs + +import GHC.Tc.Utils.Monad +import GHC.Tc.Types.ErrCtxt + +import GHC.Rename.Utils + +{- Note [Typechecking by expansion: overview] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +For many constructs, rather than typechecking the user-written code +directly, it's much easier to + * Expand (or desugar) the code to something simpler + * Typecheck that simpler expression + +Example: Typechecking the do expression. The typechecker looks (somewhat) like this: + + tcExpr e@(HsDo _ stmts) rho = do { hse <- expandDoStmts stmts + ; tcHsExpansion hse rho } + +The `expandDoStmts` replaces the HsDo { x <- e1; return x } +with something like + HSE { hse_ctxt = ExprCtxt e + , hse_exp = e1 >>= \ x -> x } +and we then typecheck the expression `e1 >>= \ x -> x` + +See also Note [Handling overloaded and rebindable constructs] + and Note [Doing XXExprGhcRn in the Renamer vs Typechecker] + +The Big Question is how to ensure that error messages mention +only user-written source code, and never talk about the expanded code. +The rest of this Note explains how that is done. + +* The expansion process typically takes a user written thing + L lspan ue + and returns + L lspan (XExpr (ExpandedThingRn (HSE { hse_ctxt = ue + , hse_exp = ee } )) + where `ee` is the expansion of the user written thing `ue` + +* The type checker context has 3 key fields that describe the context: + TcLclCtxt { tcl_loc :: RealSrcSpan + , tcl_in_gen_code :: Bool + , tcl_err_ctxt :: ErrCtxtStack + , ... } + Note `tcl_loc` always points to a real place in the source code, + hence `RealSrcSpan`. + + The `tcl_err_ctxt` is a stack of contexts, each saying something + like "In the expression: x+y" or "In second argument of `$` namely 'r { x=2 }'" + + The `tcl_in_gen_code` is a boolean that keeps track of whether + the current expression being typechecked is compiler generated + or user generated. + + INVARIANT: `tcl_loc` and `tcl_in_gen_code` are modified only in `setSrcSpan`. + +* Now, when + tcMonoLExpr :: LHsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc) + gets a located expression, it does 3 things: + (a) Calls `setSrcSpanA` to set the ambient source-code location + (b) Calls `addExprCtxt` to push a suitable `HsCtxt` on top of the `tcl_err_ctxt`. + (c) Calls `tcExpr` to typecheck the expression. + +* In these calls, if the `span` is generated (see `isGeneratedSrcSpan`), then + - `setSrcSpanA` sets `tcl_in_gen_code` to `True`, and leaves `tcl_loc` unchanged + - `addExprCtxt` is a no-op if `tcl_in_gen_code` is True + The result is that `tcl_loc` has the span from the innermost /user/ tree node; + and the ErrCtxtStack in `tcl_err_ctxt` only has contexts arisign from user code. + +* Note that inside an expansion we have sub-expressions from the original program. + As soon as we enter one of those, identified by a /user/ span, `setSrcSpanA` will + sets the `tcl_loc` to reflect that span, and switch off `tcl_in_gen_code`. Nice! +-} + +--------------- +tcExpand :: HsExpr GhcRn -> TcM (Maybe (HsExpansion GhcRn)) +tcExpand e@(OpApp _ arg1 op arg2) + = return $ Just $ + HSE { hse_ctxt = ExprCtxt e + , hse_exp = foldl ap op [arg1,arg2] } + where + ap f a = wrapGenSpan (HsApp noExtField f a) + +tcExpand (XExpr (ExpandedThingRn hse)) + = return (Just hse) + +tcExpand e@(HsUntypedSplice splice_res _) +-- See Note [Looking through Template Haskell splices in splitHsApps] + = do { fun <- getUntypedSpliceBody splice_res + ; return $ Just $ + HSE { hse_ctxt = ExprCtxt e + , hse_exp = wrapGenSpan fun } } + +tcExpand _ = return Nothing ===================================== 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, @@ -30,10 +30,10 @@ import {-# SOURCE #-} GHC.Tc.Gen.Splice import GHC.Hs import GHC.Hs.Syn.Type - import GHC.Rename.Utils import GHC.Rename.Env ( addUsedGRE, getUpdFieldLbls ) +import GHC.Tc.Gen.Expand( tcExpand ) import GHC.Tc.Gen.App import GHC.Tc.Gen.Head import GHC.Tc.Gen.Do @@ -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 @@ -291,6 +294,12 @@ tcMonoLExprNC (L loc expr) res_ty do { expr' <- tcExpr expr res_ty ; return (L loc expr') } +--------------- +tcCollectApp :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc) +tcCollectApp the_app res_ty + = do { (fun, args) <- splitHsApps the_app + ; tcApp the_app fun args res_ty } + --------------- tcExpr :: HsExpr GhcRn -> ExpRhoType -- DeepSubsumption <=> when checking, this type @@ -312,19 +321,11 @@ tcExpr :: HsExpr GhcRn -- - ones taken apart by GHC.Tc.Gen.Head.splitHsApps -- - ones understood by GHC.Tc.Gen.Head.tcInferAppHead_maybe -- See Note [Application chains and heads] in GHC.Tc.Gen.App -tcExpr e@(HsVar {}) res_ty = tcApp e res_ty -tcExpr e@(HsApp {}) res_ty = tcApp e res_ty -tcExpr e@(OpApp {}) res_ty = tcApp e res_ty -tcExpr e@(HsAppType {}) res_ty = tcApp e res_ty -tcExpr e@(ExprWithTySig {}) res_ty = tcApp e res_ty -tcExpr e@(XExpr (HsRecSelRn{})) res_ty = tcApp e res_ty - --- Renamer expanded expressions (eg. Right/Left sections) --- or tcExpr expanded expressions (eg. Do statements and Record updates) --- are type checked using tcHsExpansion. --- See Note [Typechecking by expansion: overview] -tcExpr (XExpr (ExpandedThingRn hse)) res_ty = tcHsExpansion hse res_ty - +tcExpr e@(HsVar {}) res_ty = tcApp e e [] res_ty +tcExpr e@(ExprWithTySig {}) res_ty = tcApp e e [] res_ty +tcExpr e@(XExpr (HsRecSelRn{})) res_ty = tcApp e e [] res_ty +tcExpr e@(HsAppType {}) res_ty = tcCollectApp e res_ty +tcExpr e@(HsApp {}) res_ty = tcCollectApp e res_ty -- Typecheck an occurrence of an unbound Id -- @@ -392,7 +393,7 @@ tcExpr e@(HsOverLit _ lit) res_ty -- See Note [Short cut for overloaded literals] in GHC.Tc.Utils.TcMType ; case mb_res of Just lit' -> return (HsOverLit noExtField lit') - Nothing -> tcApp e res_ty } + Nothing -> tcApp e e [] res_ty } -- Why go via tcApp? See Note [Typechecking overloaded literals] {- Note [Typechecking overloaded literals] @@ -530,8 +531,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') } @@ -730,19 +732,6 @@ tcExpr e@(RecordUpd { rupd_flds = OverloadedRecUpdFields {}}) _ tcExpr (ArithSeq _ witness seq) res_ty = tcArithSeq witness seq res_ty -{- -************************************************************************ -* * - Record dot syntax -* * -************************************************************************ --} - --- These terms have been replaced by their expanded expressions in the renamer. See --- Note [Overview of record dot syntax]. -tcExpr (HsGetField _ _ _) _ = panic "GHC.Tc.Gen.Expr: tcExpr: HsGetField: Not implemented" -tcExpr (HsProjection _ _) _ = panic "GHC.Tc.Gen.Expr: tcExpr: HsProjection: Not implemented" - {- ************************************************************************ * * @@ -755,17 +744,7 @@ tcExpr (HsProjection _ _) _ = panic "GHC.Tc.Gen.Expr: tcExpr: HsProjection: Not -- See Note [Delaying modFinalizers in untyped splices] in GHC.Rename.Splice. tcExpr (HsTypedSplice ext splice) res_ty = tcTypedSplice ext splice res_ty tcExpr e@(HsTypedBracket _ext body) res_ty = tcTypedBracket e body res_ty - tcExpr e@(HsUntypedBracket ps body) res_ty = tcUntypedBracket e body ps res_ty -tcExpr (HsUntypedSplice splice _) res_ty - -- Since `tcApp` deals with `HsUntypedSplice` (in `splitHsApps`), you might - -- wonder why we don't delegate to `tcApp` as we do for `HsVar`, etc. - -- (See the initial block of equations for `tcExpr`.) But we can't do this - -- for `HsUntypedSplice`; to see why, read Wrinkle (UTS1) in - -- Note [Looking through Template Haskell splices in splitHsApps] in - -- GHC.Tc.Gen.Head. - = do { expr <- getUntypedSpliceBody splice - ; tcExpr expr res_ty } {- ************************************************************************ @@ -775,10 +754,12 @@ tcExpr (HsUntypedSplice splice _) res_ty ************************************************************************ -} -tcExpr (HsOverLabel {}) ty = pprPanic "tcExpr:HsOverLabel" (ppr ty) -tcExpr (SectionL {}) ty = pprPanic "tcExpr:SectionL" (ppr ty) -tcExpr (SectionR {}) ty = pprPanic "tcExpr:SectionR" (ppr ty) - +-- See Note [Typechecking by expansion: overview] +tcExpr e res_ty + = do { mb_hse <- tcExpand e + ; case mb_hse of + Just hse -> tcHsExpansion hse res_ty + Nothing -> pprPanic "tcExpr: unhandled case:" (ppr e) } {- ************************************************************************ @@ -788,73 +769,6 @@ tcExpr (SectionR {}) ty = pprPanic "tcExpr:SectionR" (ppr ty) ************************************************************************ -} -{- Note [Typechecking by expansion: overview] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -For many constructs, rather than typechecking the user-written code -directly, it's much easier to - * Expand (or desugar) the code to something simpler - * Typecheck that simpler expression - -Example: Typechecking the do expression. The typechecker looks (somewhat) like this: - - tcExpr e@(HsDo _ stmts) rho = do { hse <- expandDoStmts stmts - ; tcHsExpansion hse rho } - -The `expandDoStmts` replaces the HsDo { x <- e1; return x } -with something like - HSE { hse_ctxt = ExprCtxt e - , hse_exp = e1 >>= \ x -> x } -and we then typecheck the expression `e1 >>= \ x -> x` - -See also Note [Handling overloaded and rebindable constructs] - and Note [Doing XXExprGhcRn in the Renamer vs Typechecker] - -The Big Question is how to ensure that error messages mention -only user-written source code, and never talk about the expanded code. -The rest of this Note explains how that is done. - -* The expansion process typically takes a user written thing - L lspan ue - and returns - L lspan (XExpr (ExpandedThingRn (HSE { hse_ctxt = ue - , hse_exp = ee } )) - where `ee` is the expansion of the user written thing `ue` - -* The type checker context has 3 key fields that describe the context: - TcLclCtxt { tcl_loc :: RealSrcSpan - , tcl_in_gen_code :: Bool - , tcl_err_ctxt :: ErrCtxtStack - , ... } - Note `tcl_loc` always points to a real place in the source code, - hence `RealSrcSpan`. - - The `tcl_err_ctxt` is a stack of contexts, each saying something - like "In the expression: x+y" or "In second argument of `$` namely 'r { x=2 }'" - - The `tcl_in_gen_code` is a boolean that keeps track of whether - the current expression being typechecked is compiler generated - or user generated. - - INVARIANT: `tcl_loc` and `tcl_in_gen_code` are modified only in `setSrcSpan`. - -* Now, when - tcMonoLExpr :: LHsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc) - gets a located expression, it does 3 things: - (a) Calls `setSrcSpanA` to set the ambient source-code location - (b) Calls `addExprCtxt` to push a suitable `HsCtxt` on top of the `tcl_err_ctxt`. - (c) Calls `tcExpr` to typecheck the expression. - -* In these calls, if the `span` is generated (see `isGeneratedSrcSpan`), then - - `setSrcSpanA` sets `tcl_in_gen_code` to `True`, and leaves `tcl_loc` unchanged - - `addExprCtxt` is a no-op if `tcl_in_gen_code` is True - The result is that `tcl_loc` has the span from the innermost /user/ tree node; - and the ErrCtxtStack in `tcl_err_ctxt` only has contexts arisign from user code. - -* Note that inside an expansion we have sub-expressions from the original program. - As soon as we enter one of those, identified by a /user/ span, `setSrcSpanA` will - sets the `tcl_loc` to reflect that span, and switch off `tcl_in_gen_code`. Nice! --} - tcHsExpansion :: HsExpansion GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc) tcHsExpansion (HSE { hse_ctxt = o, hse_exp = e }) res_ty = do { e' <- tcMonoLExpr e res_ty ===================================== 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 ===================================== @@ -9,9 +9,9 @@ -} module GHC.Tc.Gen.Head - ( HsExprArg(..), TcPass(..), QLFlag(..), EWrap(..) + ( HsExprArg(..), HsExprLoc, TcPass(..), QLFlag(..), EWrap(..) , splitHsApps, rebuildHsApps - , addArgWrap, isHsValArg + , addArgWrap, isHsValArg, getFunSrcSpan , leadingValArgs, isVisibleArg, getDeepSubsumptionFlag_DataConHead , tcInferAppHead, tcInferAppHead_maybe @@ -22,16 +22,13 @@ module GHC.Tc.Gen.Head , pprArgInst, addFunResCtxt ) where import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcExpr, tcCheckPolyExprNC, tcPolyLExprSig ) -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.Tc.Gen.HsType +import GHC.Tc.Gen.Expand( tcExpand ) import GHC.Tc.Gen.Bind( chooseInferredQuantifiers ) import GHC.Tc.Gen.Sig( tcUserTypeSig, tcInstSig ) import GHC.Tc.TyCl.PatSyn( patSynBuilderOcc ) @@ -86,7 +83,7 @@ import GHC.Data.Maybe The data type HsExprArg :: TcPass -> Type is a very local type, used only within this module and GHC.Tc.Gen.App -* It's really a zipper for an application chain +* It's just a bog-standard zipper for an application chain See Note [Application chains and heads] in GHC.Tc.Gen.App for what an "application chain" is. @@ -147,6 +144,8 @@ takes apart either an HsApp, or an infix OpApp, returning * We do not look through expanded expressions (except PopErrCtxt.) -} +type HsExprLoc = EpAnn AnnListItem -- The location attached to a HsExpr + data TcPass = TcpRn -- Arguments decomposed | TcpInst -- Function instantiated | TcpTc -- Typechecked @@ -154,34 +153,34 @@ data TcPass = TcpRn -- Arguments decomposed data HsExprArg (p :: TcPass) where -- See Note [HsExprArg] -- Data constructor EValArg represents a value argument - EValArg :: { ea_loc_span :: SrcSpan - , ea_arg_ty :: !(XEVAType p) - , ea_arg :: LHsExpr (GhcPass (XPass p)) } + EValArg :: { ea_loc_span :: HsExprLoc + , ea_arg_ty :: !(XEVAType p) + , ea_arg :: LHsExpr (GhcPass (XPass p)) } -> HsExprArg p -- Data constructor EValArgQL represents an argument that has been -- partly-type-checked by Quick Look; see Note [EValArgQL] - EValArgQL :: { eaql_loc_span :: SrcSpan - , eaql_arg_ty :: Scaled TcSigmaType -- Argument type expected by function - , eaql_larg :: LHsExpr GhcRn -- Original application, for - -- location and error msgs - , eaql_rn_fun :: HsExpr GhcRn -- Head of the argument if it is an application - , eaql_tc_fun :: (HsExpr GhcTc, SrcSpan) -- Typechecked head and its location span - , eaql_fun_ue :: UsageEnv -- Usage environment of the typechecked head (QLA5) - , eaql_args :: [HsExprArg 'TcpInst] -- Args: instantiated, not typechecked - , eaql_wanted :: WantedConstraints - , eaql_encl :: Bool -- True <=> we have already qlUnified - -- eaql_arg_ty and eaql_res_rho - , eaql_res_rho :: TcRhoType } -- Result type of the application + EValArgQL :: { eaql_loc_span :: HsExprLoc + , eaql_arg_ty :: Scaled TcSigmaType -- Argument type expected by function + , eaql_larg :: LHsExpr GhcRn -- Original application, for + -- location and error msgs + , eaql_rn_fun :: HsExpr GhcRn -- Head of the argument if it is an application + , eaql_tc_fun :: (HsExpr GhcTc, SrcSpan) -- Typechecked head and its location span + , eaql_fun_ue :: UsageEnv -- Usage environment of the typechecked head (QLA5) + , eaql_args :: [HsExprArg 'TcpInst] -- Args: instantiated, not typechecked + , eaql_wanted :: WantedConstraints + , eaql_encl :: Bool -- True <=> we have already qlUnified + -- eaql_arg_ty and eaql_res_rho + , eaql_res_rho :: TcRhoType } -- Result type of the application -> HsExprArg 'TcpInst -- Only exists in TcpInst phase - ETypeArg :: { ea_loc_span :: SrcSpan - , ea_hs_ty :: LHsWcType GhcRn -- The type arg - , ea_ty_arg :: !(XETAType p) } -- Kind-checked type arg + ETypeArg :: { ea_loc_span :: HsExprLoc + , ea_hs_ty :: LHsWcType GhcRn -- The type arg + , ea_ty_arg :: !(XETAType p) } -- Kind-checked type arg -> HsExprArg p - EPrag :: SrcSpan -> (HsPragE (GhcPass (XPass p))) -> HsExprArg p - EWrap :: EWrap -> HsExprArg p + EPrag :: HsExprLoc -> (HsPragE (GhcPass (XPass p))) -> HsExprArg p + EWrap :: EWrap -> HsExprArg p type family XETAType (p :: TcPass) where -- Type arguments XETAType 'TcpRn = NoExtField @@ -193,8 +192,8 @@ type family XEVAType (p :: TcPass) where -- Value arguments data QLFlag = DoQL | NoQL -data EWrap = EPar SrcSpan - | EExpand (HsExpr GhcRn) +data EWrap = EPar HsExprLoc + | EExpand HsExprLoc HsCtxt | EHsWrap HsWrapper @@ -207,11 +206,11 @@ type family XPass (p :: TcPass) where XPass 'TcpInst = 'Renamed XPass 'TcpTc = 'Typechecked -mkEValArg :: SrcSpan -> LHsExpr GhcRn -> HsExprArg 'TcpRn +mkEValArg :: HsExprLoc -> LHsExpr GhcRn -> HsExprArg 'TcpRn mkEValArg src_loc e = EValArg { ea_arg = e, ea_loc_span = src_loc , ea_arg_ty = noExtField } -mkETypeArg :: SrcSpan -> LHsWcType GhcRn -> HsExprArg 'TcpRn +mkETypeArg :: HsExprLoc -> LHsWcType GhcRn -> HsExprArg 'TcpRn mkETypeArg src_loc hs_ty = ETypeArg { ea_loc_span = src_loc , ea_hs_ty = hs_ty @@ -223,74 +222,17 @@ addArgWrap wrap args | otherwise = EWrap (EHsWrap wrap) : args -splitHsApps :: HsExpr GhcRn - -> TcM ( (HsExpr GhcRn, SrcSpan) -- Head - , [HsExprArg 'TcpRn]) -- Args --- See Note [splitHsApps]. --- --- This uses the TcM monad solely because we must run modFinalizers when looking --- through HsUntypedSplices --- (see Note [Looking through Template Haskell splices in splitHsApps]). -splitHsApps e = go e noSrcSpan [] - where - go :: HsExpr GhcRn -> SrcSpan -> [HsExprArg 'TcpRn] - -> TcM ((HsExpr GhcRn, SrcSpan), [HsExprArg 'TcpRn]) - -- Modify the SrcSpan as we walk inwards, so it describes the next argument - go (HsPar _ (L l fun)) lspan args = go fun (locA l) (EWrap (EPar lspan) : args) - go (HsPragE _ p (L l fun)) lspan args = go fun (locA l) (EPrag lspan p : args) - 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 - ; go fun lspan' (EWrap (EExpand e) : args) } - where - lspan' :: SrcSpan - lspan' = case splice of - 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 - = pure ( (op, locA l) - , mkEValArg noSrcSpan arg1 - : mkEValArg noSrcSpan arg2 - -- noSrcSpan because this the span of the call, - -- and its hard to say exactly what that is - : EWrap (EExpand e) - : args ) - - go e lspan args = pure ((e, lspan), args) - - --- | Rebuild an application: takes a type-checked application head --- expression together with arguments in the form of typechecked 'HsExprArg's --- and returns a typechecked application of the head to the arguments. -rebuildHsApps :: (HsExpr GhcTc, SrcSpan) - -- ^ the function being applied - -> [HsExprArg 'TcpTc] - -- ^ the arguments to the function - -> HsExpr GhcTc -rebuildHsApps (fun, _) [] = fun -rebuildHsApps (fun, sloc) (arg : args) - = case arg of - EValArg { ea_arg = arg, ea_loc_span = sloc' } - -> rebuildHsApps (HsApp noExtField lfun arg, sloc') args - ETypeArg { ea_hs_ty = hs_ty, ea_ty_arg = ty, ea_loc_span = sloc' } - -> rebuildHsApps (HsAppType ty lfun hs_ty, sloc') args - EPrag sloc' p - -> rebuildHsApps (HsPragE noExtField p lfun, sloc') args - EWrap (EPar sloc') - -> rebuildHsApps (gHsPar lfun, sloc') args - EWrap (EExpand o) - -> rebuildHsApps (mkExpandedExprTc o fun, sloc) args - EWrap (EHsWrap wrap) - -> rebuildHsApps (mkHsWrap wrap fun, sloc) args - where - lfun = L (noAnnSrcSpan sloc) fun +-------------------- +getFunSrcSpan :: [HsExprArg 'TcpRn] -> TcM SrcSpan +getFunSrcSpan [] = getSrcSpanM +getFunSrcSpan (ETypeArg { ea_loc_span = l } : _) = return (locA l) +getFunSrcSpan (EValArg { ea_loc_span = l } : _) = return (locA l) +getFunSrcSpan (EPrag l _ : _) = return (locA l) +getFunSrcSpan (EWrap (EPar l) : _) = return (locA l) +getFunSrcSpan (EWrap (EExpand l _) : _) = return (locA l) +getFunSrcSpan (EWrap (EHsWrap {}) : args) = getFunSrcSpan args +-------------------- isHsValArg :: HsExprArg id -> Bool isHsValArg (EValArg {}) = True isHsValArg _ = False @@ -334,13 +276,60 @@ pprArgInst (EValArgQL { eaql_tc_fun = fun, eaql_args = args, eaql_res_rho = ty}) 2 (vcat [ vcat (map pprArgInst args), text "ea_ql_ty:" <+> ppr ty ]) instance Outputable EWrap where - ppr (EPar _) = text "EPar" - ppr (EHsWrap w) = text "EHsWrap" <+> ppr w - ppr (EExpand orig) = text "EExpand" <+> ppr orig + ppr (EPar _) = text "EPar" + ppr (EHsWrap w) = text "EHsWrap" <+> ppr w + ppr (EExpand _ _) = text "EExpand" -- No Outputable instance for HsCtxt yet + + + +{- ********************************************************************* +* * + Splitting and rebuilding +* * +********************************************************************* -} + +splitHsApps :: HsExpr GhcRn -> TcM (HsExpr GhcRn, [HsExprArg 'TcpRn]) +splitHsApps e = go e [] + where + go (HsPar _ (L l fun)) args = go fun (EWrap (EPar l) : args) + go (HsPragE _ p (L l fun)) args = go fun (EPrag l p : args) + go (HsAppType _ (L l fun) ty) args = go fun (mkETypeArg l ty : args) + go (HsApp _ (L l fun) arg) args = go fun (mkEValArg l arg : args) + go fun args = do { mb_hse <- tcExpand fun + ; case mb_hse of + Just (HSE { hse_ctxt = orig, hse_exp = L l fun' }) + -> go fun' (EWrap (EExpand l orig) : args) + Nothing + -> return (fun, args) } + +-- | Rebuild an application: takes a type-checked application head +-- expression together with arguments in the form of typechecked 'HsExprArg's +-- and returns a typechecked application of the head to the arguments. +rebuildHsApps :: HsExpr GhcTc + -- ^ the function being applied + -> [HsExprArg 'TcpTc] + -- ^ the arguments to the function + -> HsExpr GhcTc +rebuildHsApps fun [] = fun +rebuildHsApps fun (arg : args) + = case arg of + EValArg { ea_arg = arg, ea_loc_span = l } + -> rebuildHsApps (HsApp noExtField (L l fun) arg) args + ETypeArg { ea_hs_ty = hs_ty, ea_ty_arg = ty, ea_loc_span = l } + -> rebuildHsApps (HsAppType ty (L l fun) hs_ty) args + EPrag l p + -> rebuildHsApps (HsPragE noExtField p (L l fun)) args + EWrap (EPar l) + -> rebuildHsApps (HsPar noExtField (L l fun)) args + EWrap (EExpand l o) + -> rebuildHsApps (XExpr (ExpandedThingTc (HSE o (L l fun)))) args + EWrap (EHsWrap wrap) + -> rebuildHsApps (mkHsWrap wrap fun) args + {- Note [Desugar OpApp in the typechecker] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Operator sections are desugared in the renamer; see GHC.Rename.Expr +pOperator sections are desugared in the renamer; see GHC.Rename.Expr Note [Handling overloaded and rebindable constructs]. But for reasons explained there, we rename OpApp to OpApp. Then, here in the typechecker, we desugar it to a use of ExpandedThingRn. @@ -401,6 +390,8 @@ handling splices and quasiquotes has already been performed by the renamer by the time we get to `splitHsApps`. Wrinkle (UTS1): +*** TODO *** put this somewhere else + `tcExpr` has a separate case for `HsUntypedSplice`s that do /not/ occur at the head of an application. This is important to handle programs like this one: @@ -446,9 +437,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 -> runInferRho (tcExpr fun) } tcInferAppHead_maybe :: HsExpr GhcRn -> TcM (Maybe (HsExpr GhcTc, TcSigmaType)) @@ -457,23 +446,11 @@ tcInferAppHead_maybe :: HsExpr GhcRn -- XExpr's although complicated needs to be looked through, useful for QL things when -- the argument is an XExpr tcInferAppHead_maybe fun = case fun of - HsVar _ nm - -> Just <$> tcInferId nm - ExprWithTySig _ e hs_ty - -> Just <$>tcExprWithSig e hs_ty - HsOverLit _ lit - -> 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 - _ - -> return Nothing + HsVar _ nm -> Just <$> tcInferId nm + ExprWithTySig _ e hs_ty -> Just <$> tcExprWithSig e hs_ty + HsOverLit _ lit -> Just <$> tcInferOverLit lit + XExpr (HsRecSelRn f) -> Just <$> tcInferRecSelId f + _ -> 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 ===================================== @@ -99,13 +99,12 @@ import qualified GHC.LanguageExtensions as LangExt import GHC.Builtin.Types import GHC.Types.Name -import GHC.Types.Id( idType, isDataConId ) +import GHC.Types.Id( idType ) import GHC.Types.Var as Var import GHC.Types.Var.Set import GHC.Types.Var.Env import GHC.Types.Basic import GHC.Types.Unique.Set (nonDetEltsUniqSet) -import GHC.Types.SrcLoc (unLoc, GenLocated (..)) import GHC.Utils.Misc import GHC.Utils.Outputable as Outputable @@ -426,7 +425,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 +1168,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 +1202,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 +1217,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 +1234,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 +1248,47 @@ 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 -> undefined +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 `undefined`. + +Another example: + case x of + True -> (e1 :: forall a b. a->b) + False -> (e3 :: forall b a. a->b) + +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`. + +This does mean that this would work: + (let x = 77+55 in h x x) @Int +where + h :: Int -> Int -> forall a. a->a +The `@Int` would instantiate the `forall a`. + +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] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1274,7 +1304,7 @@ Usually this field is `IIF_DeepRho` meaning "return a (possibly deep) rho-type". Why is this the common case? See #17173 for discussion. Here are some examples of why: -1. Consider +(IIR1) Consider f x = (*) We want to instantiate the type of (*) before returning, else we will infer the type @@ -1286,21 +1316,46 @@ of why: instantiating. This could perhaps be worked around, but it may be hard to know even when instantiation should happen. -2. Another reason. Consider +(IIR2) Another reason. Consider f :: (?x :: Int) => a -> a g y = let ?x = 3::Int in f Here want to instantiate f's type so that the ?x::Int constraint gets discharged by the enclosing implicit-parameter binding. -3. Suppose one defines plus = (+). If we instantiate lazily, we will +(IIR3) Suppose one defines plus = (+). If we instantiate lazily, we will infer plus :: forall a. Num a => a -> a -> a. However, the monomorphism restriction compels us to infer plus :: Integer -> Integer -> Integer (or similar monotype). Indeed, the only way to know whether to apply the monomorphism restriction at all is to instantiate -HOWEVER, not always! Here are places where we want `IIF_Sigma` meaning -"return a sigma-type": +(IIR4) When -XDeepSubsumption is on, we /deeply/ instantiate. Why isn't + top-instantiation enough? Answer: to accept the following program (T26225b) with + -XDeepSubsumption, we need to deeply instantiate when inferring in checkResultTy: + + f :: Int -> (forall a. a->a) + g :: Int -> Bool -> Bool + + test b = case b of + True -> f + False -> g + + If we don't deeply instantiate in the branches of the case expression, we will + try to unify the type of `f` with that of `g`, which fails. If we instead + deeply instantiate `f`, we will fill the `InferResult` with `Int -> alpha -> alpha` + which then successfully unifies with the type of `g` when we come to fill the + `InferResult` hole a second time for the second case branch. + +(IIR5) When inferring, even /without/ -XDeepSubsumption, we must deeply instantiate + the types of data constructors. E.g + data T = MkT Int int + f = MkT 3 + We must infer MkT 3 :: Int ->{mu} T (fresh mu) + and not MkT 3 :: Int ->{one} T + See Note [Typechecking data constructors] in GHC.Tc.Gen.Head + Hence the use of `getDeepSubsumptionFlag_DataConHead` in `checkResultTy`. + +HOWEVER, `ir_inst` is not always `IIF_DeepRho`! Here are places when it isn't: * IIF_Sigma: In GHC.Tc.Module.tcRnExpr, which implements GHCi's :type command, we want to return a completely uninstantiated type. @@ -1316,23 +1371,6 @@ 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? -Answer: to accept the following program (T26225b) with -XDeepSubsumption, we -need to deeply instantiate when inferring in checkResultTy: - - f :: Int -> (forall a. a->a) - g :: Int -> Bool -> Bool - - test b = - case b of - True -> f - False -> g - -If we don't deeply instantiate in the branches of the case expression, we will -try to unify the type of 'f' with that of 'g', which fails. If we instead -deeply instantiate 'f', we will fill the 'InferResult' with 'Int -> alpha -> alpha' -which then successfully unifies with the type of 'g' when we come to fill the -'InferResult' hole a second time for the second case branch. -} {- @@ -2068,24 +2106,14 @@ 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 - | otherwise - -> go app_head - } +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 - go :: HsExpr GhcTc -> DeepSubsumptionFlag - go (XExpr (ConLikeTc (RealDataCon {}))) = Deep TopSub - go (XExpr (ExpandedThingTc (HSE _ (L _ f)))) = go f - go (XExpr (WrapExpr _ f)) = go f - go (HsApp _ f _) = go (unLoc f) - go (HsAppType _ f _) = go (unLoc f) - go _ = Shallow - + dc_head (XExpr (ConLikeTc (RealDataCon {}))) = True + dc_head _ = False -- | 'tc_sub_type_deep' is where the actual work happens for deep subsumption. -- ===================================== compiler/ghc.cabal.in ===================================== @@ -832,6 +832,7 @@ Library GHC.Tc.Gen.Bind GHC.Tc.Gen.Default GHC.Tc.Gen.Do + GHC.Tc.Gen.Expand GHC.Tc.Gen.Export GHC.Tc.Gen.Expr GHC.Tc.Gen.Foreign ===================================== testsuite/tests/partial-sigs/should_compile/SplicesUsed.stderr ===================================== @@ -1,6 +1,5 @@ [1 of 2] Compiling Splices ( Splices.hs, Splices.o ) [2 of 2] Compiling SplicesUsed ( SplicesUsed.hs, SplicesUsed.o ) - SplicesUsed.hs:7:15: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)] • Found type wildcard ‘_’ standing for ‘Maybe Bool’ • In the type signature: maybeBool :: _ @@ -21,8 +20,7 @@ SplicesUsed.hs:8:26: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefau • Found type wildcard ‘_’ standing for ‘Bool’ • In the first argument of ‘Maybe’, namely ‘_’ In an expression type signature: Maybe _ - In the first argument of ‘id :: _a -> _a’, namely - ‘(Just True :: Maybe _)’ + In the expression: Just True :: Maybe _ • Relevant bindings include maybeBool :: Maybe Bool (bound at SplicesUsed.hs:8:1) @@ -78,3 +76,4 @@ SplicesUsed.hs:18:2: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefau the inferred type of bar :: Bool -> w -> (Bool, w) at SplicesUsed.hs:18:2-11 • In the type signature: bar :: _a -> _b -> (_a, _b) + View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/a091fcbb975d514542e66e4d456bb99f... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/a091fcbb975d514542e66e4d456bb99f... You're receiving this email because of your account on gitlab.haskell.org.