Simon Peyton Jones pushed to branch wip/ani/tc-expand at Glasgow Haskell Compiler / GHC Commits: a5163a87 by Simon Peyton Jones at 2026-03-26T23:14:13+00:00 Fixes from Simon Looking much nicer now - - - - - 8 changed files: - compiler/GHC/Tc/Errors/Ppr.hs - compiler/GHC/Tc/Gen/App.hs - compiler/GHC/Tc/Gen/Expr.hs - compiler/GHC/Tc/Gen/Head.hs - compiler/GHC/Tc/Types/ErrCtxt.hs - compiler/GHC/Tc/Utils/TcType.hs - compiler/GHC/Tc/Utils/Unify.hs - compiler/GHC/Tc/Zonk/TcType.hs Changes: ===================================== compiler/GHC/Tc/Errors/Ppr.hs ===================================== @@ -7709,12 +7709,8 @@ pprHsCtxt = \case PatSigErrCtxt sig_ty res_ty -> vcat [ hang (text "When checking that the pattern signature:") 4 (ppr sig_ty) - , nest 2 (hang (text "fits the type of its context:") 2 pp_res_ty) ] - where - -- Zonking will have turned Infer into Check - pp_res_ty = case res_ty of - Check ty -> ppr ty - Infer ir -> text "OOPS" <+> ppr ir + , nest 2 (hang (text "fits the type of its context:") + 2 (ppr (getCheckExpType res_ty))) ] PatCtxt pat -> hang (text "In the pattern:") 2 (ppr pat) @@ -7776,7 +7772,7 @@ pprHsCtxt = \case full_herald = pprExpectedFunTyHerald herald <+> speakNOf n_vis_args_in_call (text "visible argument") -- What are "visible" arguments? See Note [Visibility and arity] in GHC.Types.Basic - FunResCtxt fun n_val_args res_fun res_env n_fun n_env + FunResCtxt fun n_val_args fun_res_ty env_ty | -- Check for too few args -- fun_tau = a -> b, res_tau = Int n_fun > n_env @@ -7800,6 +7796,18 @@ pprHsCtxt = \case -> empty -- text "Debug" <+> vcat [ppr fun, ppr n_val_args, ppr res_fun, ppr res_env, ppr n_fun, ppr n_env] where + -- See Note [Splitting nested sigma types in mismatched + -- function types] + -- env_ty is an ExpRhoTy, but with simple subsumption it + -- is not /deeply/ skolemised, so still use tcSplitNestedSigmaTys + + (_,_,fun_tau) = tcSplitNestedSigmaTys fun_res_ty + (_, _, env_tau) = tcSplitNestedSigmaTys (getCheckExpType env_ty) + (args_fun, res_fun) = tcSplitFunTys fun_tau + (args_env, res_env) = tcSplitFunTys env_tau + n_fun = length args_fun + n_env = length args_env + not_fun ty -- ty is definitely not an arrow type, -- and cannot conceivably become one = case tcSplitTyConApp_maybe ty of ===================================== compiler/GHC/Tc/Gen/App.hs ===================================== @@ -354,6 +354,7 @@ tcApp :: HsExpr GhcRn -> ExpRhoType -- When checking, -XDeepSubsumption <=> deeply skolemised -> TcM (HsExpr GhcTc) -- See Note [tcApp: typechecking applications] +-- INVARIANT: the expression is an application of some kind tcApp rn_expr exp_res_ty = do { -- Step 1: Split the application chain ((rn_fun, fun_lspan), rn_args) <- splitHsApps rn_expr @@ -366,6 +367,8 @@ tcApp rn_expr exp_res_ty , text "rn_args:" <+> ppr rn_args ] -- Step 2: Infer the type of `fun`, the head of the application + -- NB: we are certain that there is at least one argument, so inferring is + -- ; (tc_fun, fun_sigma) <- tcInferExprSigma rn_fun ; let tc_head = (tc_fun, fun_lspan) -- inst_final: top-instantiate the result type of the application, @@ -458,44 +461,9 @@ 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 - ; 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] --- --- Match up app_res_rho: the result type of rn_expr --- with res_ty: the expected result type - = perhaps_add_res_ty_ctxt $ - do { ds_flag <- getDeepSubsumptionFlag_DataConHead tc_fun - ; traceTc "checkResultTy {" $ - vcat [ text "tc_fun:" <+> ppr tc_fun - , text "app_res_rho:" <+> ppr app_res_rho - , text "res_ty:" <+> ppr res_ty - , text "ds_flag:" <+> ppr ds_flag ] - ; case ds_flag of - Shallow -> -- No deep subsumption - -- app_res_rho and res_ty are both rho-types, - -- so with simple subsumption we can just unify them - -- No need to zonk; the unifier does that - do { co <- unifyExprType rn_expr app_res_rho res_ty - ; traceTc "checkResultTy 1 }" (ppr co) - ; return (mkWpCastN co) } - - Deep ds_reason -> -- Deep subsumption - -- Even though both app_res_rho and res_ty are rho-types, - -- they may have nested polymorphism, so if deep subsumption - -- is on we must call tcSubType. - do { wrap <- tcSubTypeDS tc_fun ds_reason rn_expr app_res_rho res_ty - ; traceTc "checkResultTy 2 }" $ - vcat [ text "app_res_rho:" <+> ppr app_res_rho - , text "res_ty:" <+> ppr res_ty - , text "wrap:" <+> ppr wrap - ] - ; return wrap } } +checkResultTy rn_expr (tc_fun, fun_loc) inst_args app_res_ty res_ty + = perhaps_add_res_ty_ctxt $ + tcCheckAppResult rn_expr tc_fun app_res_ty res_ty where -- perhaps_add_res_ty_ctxt: Inside an expansion, the addFunResCtxt stuff is -- more confusing than helpful because the function at the head isn't in @@ -505,7 +473,7 @@ checkResultTy rn_expr (tc_fun, fun_loc) inst_args app_res_rho (Check res_ty) | isGeneratedSrcSpan fun_loc = thing_inside | otherwise - = addFunResCtxt tc_fun inst_args app_res_rho (mkCheckExpType res_ty) $ + = addFunResCtxt tc_fun inst_args app_res_ty res_ty $ thing_inside ---------------- @@ -1915,12 +1883,15 @@ 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 + -- See Note [The head of an application] + ; if not (headOkForQuickLook rn_fun_arg) then skipQuickLook app_lspan larg sc_arg_ty else -- Step 1: get the type of the head of the argument - do { (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 @@ -2003,15 +1974,30 @@ mk_origin fun_lspan rn_fun } -tooComplicatedForQuickLook :: HsExpr GhcRn -> Bool -tooComplicatedForQuickLook expr +headOkForQuickLook :: HsExpr GhcRn -> Bool +headOkForQuickLook expr = case expr of - HsVar {} -> False - ExprWithTySig {} -> False - XExpr (HsRecSelRn {}) -> False - HsOverLit {} -> False - _ -> True -- Too complicated + HsVar {} -> True + ExprWithTySig {} -> True + XExpr (HsRecSelRn {}) -> True + HsOverLit {} -> True + HsUntypedSplice {} -> True -- See #21077 + _ -> False -- Too complicated + +{- Note [The head of an application] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider (f $ (\x -> blah)) + where f :: (forall a. a->a) -> Int +We really, really need to push down that (forall a. a->a) to the \x. + +But when doing QuickLook on the second argument of ($) in `quickLookArg1`, namely +(\x -> blah), the `splitHsApps` will return an empty argument list, and a function +part of (\x -> blah). We must NOT infer the type of the argument (\x -> blah), +via `tcInferExprSigma`, because that will give a monotype to `x`. +Instead we give up. Which is exactly what the paper says; QuickLook only does something +when the head of the application is a variable. +-} {- ********************************************************************* * * ===================================== compiler/GHC/Tc/Gen/Expr.hs ===================================== @@ -304,41 +304,37 @@ tcExpr :: HsExpr GhcRn -- is deeply skolemised -> TcM (HsExpr GhcTc) +-- Deal with expansions +tcExpr (XExpr (ExpandedThingRn hse)) res_ty = tcHsExpansion hse res_ty + +tcExpr e@(HsVar _ v_rn) res_ty + = do { (v_tc, sigma_ty) <- tcInferId v_rn + ; wrap <- tcCheckAppResult e v_tc sigma_ty res_ty + ; return (mkHsWrap wrap v_tc) } + +tcExpr e@(ExprWithTySig _ e_rn e_ty) res_ty + = do { (e_tc, sigma_ty) <- tcExprWithSig e_rn e_ty + ; wrap <- tcCheckAppResult e e_tc sigma_ty res_ty + ; return (mkHsWrap wrap e_tc) } + +tcExpr e@(XExpr(HsRecSelRn f)) res_ty + = do { (e_tc, sigma_ty) <- tcInferRecSelId f + ; wrap <- tcCheckAppResult e e_tc sigma_ty res_ty + ; return (mkHsWrap wrap e_tc) } + -- Use tcApp to typecheck applications, which are treated specially -- by Quick Look. Specifically: --- - HsVar lone variables, to ensure that they can get an --- impredicative instantiation (via Quick Look --- driven by res_ty (in checking mode)). -- - HsApp value applications -- - HsAppType type applications --- - ExprWithTySig (e :: type) --- - HsRecSel overloaded record fields --- - ExpandedThingRn renamer/pre-typechecker expansions -- - HsOpApp operator applications --- - HsOverLit overloaded literals -- These constructors are the union of -- - 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 -- 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 - = do { (e_tc, sigma_ty) <- tcExprWithSig e_rn e_ty - ; tcWrapResult e e_tc sigma_ty res_ty } - -tcExpr e@(XExpr(HsRecSelRn f)) res_ty - = do { (e_tc, sigma_ty) <- tcInferRecSelId f - ; tcWrapResult e e_tc sigma_ty res_ty } - -tcExpr (XExpr (ExpandedThingRn hse)) res_ty = tcHsExpansion hse 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@(HsApp {}) res_ty = tcApp e res_ty +tcExpr e@(HsAppType {}) res_ty = tcApp e res_ty +tcExpr e@(OpApp {}) res_ty = tcApp e res_ty -- Typecheck an occurrence of an unbound Id -- @@ -488,7 +484,8 @@ tcExpr expr@(ExplicitTuple x tup_args boxity) res_ty ; traceTc "ExplicitTuple" (ppr act_res_ty $$ ppr res_ty) - ; tcWrapResultMono expr expr' act_res_ty res_ty } + ; co <- tcSubTypeMono expr act_res_ty res_ty + ; return (mkHsWrapCo co expr') } tcExpr (ExplicitSum _ alt arity expr) res_ty = do { let sum_tc = sumTyCon arity @@ -682,8 +679,6 @@ tcExpr expr@(RecordCon { rcon_con = L loc qcon@(WithUserRdr _ con_name) , rcon_con = L loc con_like , rcon_flds = rbinds' } - ; ret <- tcWrapResultMono expr expr' actual_res_ty res_ty - -- Check for missing fields. We do this after type-checking to get -- better types in error messages (cf #18869). For example: -- data T a = MkT { x :: a, y :: a } @@ -694,7 +689,8 @@ tcExpr expr@(RecordCon { rcon_con = L loc qcon@(WithUserRdr _ con_name) -- via a new `HoleSort`. But that seems too much work. ; checkMissingFields con_like rbinds arg_tys - ; return ret } + ; co <- tcSubTypeMono expr actual_res_ty res_ty + ; return (mkHsWrapCo co expr') } where orig = OccurrenceOf con_name @@ -721,14 +717,13 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr -- NB: it's important to use ds_res_ty and not res_ty here. -- Test case: T18802b. - ; tcWrapResultMono expr expr' ds_res_ty res_ty + ; co <- tcSubTypeMono expr ds_res_ty res_ty -- We need to unify the result type of the expanded -- expression with the expected result type. -- -- See Note [Unifying result types in tcRecordUpd]. -- Test case: T10808. - } - } + ; return (mkHsWrapCo co expr') } } tcExpr e@(RecordUpd { rupd_flds = OverloadedRecUpdFields {}}) _ = pprPanic "tcExpr: unexpected overloaded-dot RecordUpd" $ ppr e ===================================== compiler/GHC/Tc/Gen/Head.hs ===================================== @@ -21,8 +21,6 @@ module GHC.Tc.Gen.Head , pprArgInst, addFunResCtxt ) where -import {-# SOURCE #-} GHC.Tc.Gen.Splice( getUntypedSpliceBody ) - import GHC.Prelude import GHC.Hs import GHC.Hs.Syn.Type @@ -63,7 +61,6 @@ import GHC.Builtin.Names import GHC.Driver.DynFlags import GHC.Utils.Misc import GHC.Utils.Outputable as Outputable -import GHC.Utils.Panic {- ********************************************************************* @@ -765,10 +762,11 @@ nonBidirectionalErr = TcRnPatSynNotBidirectional {- Note [Typechecking data constructors] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -As per Note [Polymorphisation of linear fields] in -GHC.Core.Multiplicity, when we use a data constructor as a term, we want to -consider its field to have polymorphic multiplicities. That is, -Note [Data constructors are linear by default] says: +As per Note [Polymorphisation of linear fields] in GHC.Core.Multiplicity, +when we use a data constructor as a term, we want to consider its field to +have polymorphic multiplicities. + +That is, Note [Data constructors are linear by default] says: Just :: a. a %1 -> Maybe a @@ -934,7 +932,8 @@ See Note [-fno-code mode]. * * ********************************************************************* -} -addFunResCtxt :: HsExpr GhcTc -> [HsExprArg p] +addFunResCtxt :: HasDebugCallStack + => HsExpr GhcTc -> [HsExprArg p] -> TcType -> ExpRhoType -> TcM a -> TcM a -- When we have a mis-match in the return type of a function @@ -942,33 +941,10 @@ addFunResCtxt :: HsExpr GhcTc -> [HsExprArg p] -- But not in generated code, where we don't want -- to mention internal (rebindable syntax) function names addFunResCtxt fun args fun_res_ty env_ty thing_inside - = do { env_tv <- newFlexiTyVarTy liftedTypeKind - ; dumping <- doptM Opt_D_dump_tc_trace - ; msg <- mk_msg dumping env_tv - ; addErrCtxt msg thing_inside } + = addErrCtxt (FunResCtxt fun (count isValArg args) fun_res_ty env_ty) $ + thing_inside -- NB: use a landmark error context, so that an empty context -- doesn't suppress some more useful context - where - mk_msg dumping env_tv - = do { mb_env_ty <- readExpType_maybe env_ty - -- by the time the message is rendered, the ExpType - -- will be filled in (except if we're debugging) - ; env' <- case mb_env_ty of - Just env_ty -> return env_ty - Nothing -> do { massert dumping; return env_tv } - ; let -- See Note [Splitting nested sigma types in mismatched - -- function types] - (_, _, fun_tau) = tcSplitNestedSigmaTys fun_res_ty - (_, _, env_tau) = tcSplitNestedSigmaTys env' - -- env_ty is an ExpRhoTy, but with simple subsumption it - -- is not deeply skolemised, so still use tcSplitNestedSigmaTys - (args_fun, res_fun) = tcSplitFunTys fun_tau - (args_env, res_env) = tcSplitFunTys env_tau - info = - FunResCtxt fun (count isValArg args) res_fun res_env - (length args_fun) (length args_env) - ; return info } - {- Note [Splitting nested sigma types in mismatched function types] ===================================== compiler/GHC/Tc/Types/ErrCtxt.hs ===================================== @@ -251,7 +251,10 @@ data HsCtxt -- | In the instance type signature of a class method. | MethSigCtxt !Name !TcType !TcType -- | In a pattern type signature. + | PatSigErrCtxt !TcType !ExpType + -- ExpType: see Note [ExpType in HsCtxt] + -- | In a pattern. | PatCtxt !(Pat GhcRn) -- | In a pattern synonym declaration. @@ -268,7 +271,10 @@ data HsCtxt -- | In a function call. | FunTysCtxt !ExpectedFunTyCtxt !Type !Int !Int -- | In the result of a function call. - | FunResCtxt !(HsExpr GhcTc) !Int !Type !Type !Int !Int + + | FunResCtxt !(HsExpr GhcTc) !Int !TcType !ExpType + -- ExpType: see Note [ExpType in HsCtxt] + -- | In the declaration of a type constructor. | TyConDeclCtxt !Name !(TyConFlavour TyCon) -- | In a type or data family instance (or default instance). @@ -377,3 +383,14 @@ isHsCtxtLandmark (DerivBindCtxt{}) = True isHsCtxtLandmark (FunResCtxt{}) = True isHsCtxtLandmark (VDQWarningCtxt{}) = True isHsCtxtLandmark _ = False + +{- Note [ExpType in HsCtxt] +~~~~~~~~~~~~~~~~~~~~~~~~~~~ +A couple of HsCtxt constructors have ExpTypes in them. When zonking the +Infer{} case we read the hole, which should be filled in by now, and zonk +that type. Now we want to put it back: we use (Check ty') for this, so that +clients of a zonked HsCtxt don't need to be monadic. + +Result: after zonking, these ExpTypes are always (Check ty). It woudl be nice +to guarantee this statically, but it's hard to do so. +-} ===================================== compiler/GHC/Tc/Utils/TcType.hs ===================================== @@ -28,7 +28,7 @@ module GHC.Tc.Utils.TcType ( ExpType(..), ExpKind, InferResult(..), InferInstFlag(..), InferFRRFlag(..), ExpTypeFRR, ExpSigmaType, ExpSigmaTypeFRR, ExpRhoType, ExpRhoTypeFRR, - mkCheckExpType, + mkCheckExpType, getCheckExpType, checkingExpType_maybe, checkingExpType, ExpPatType(..), mkCheckExpFunPatTy, mkInvisExpPatType, @@ -492,6 +492,12 @@ instance Outputable InferResult where mkCheckExpType :: TcType -> ExpType mkCheckExpType = Check +getCheckExpType :: HasDebugCallStack => ExpType -> TcType +-- Expect a (Check ty). +-- See Note [ExpType in HsCtxt] in GHC.Tc.Types.ErrCtxt +getCheckExpType (Check ty) = ty +getCheckExpType (Infer ir) = pprPanic "getCheckExpType" (ppr ir) + -- | Returns the expected type when in checking mode. checkingExpType_maybe :: ExpType -> Maybe TcType checkingExpType_maybe (Check ty) = Just ty ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -10,10 +10,10 @@ -- | Type subsumption and unification module GHC.Tc.Utils.Unify ( -- Full-blown subsumption - tcWrapResult, tcWrapResultO, tcWrapResultMono, - tcSubType, tcSubTypeSigma, tcSubTypePat, tcSubTypeDS, tcSubTypeHoleFit, - addSubTypeCtxt, - tcSubTypeAmbiguity, tcSubMult, + tcWrapResult, tcWrapResultO, + addSubTypeCtxt, tcCheckAppResult, + tcSubType, tcSubTypeSigma, tcSubTypePat, tcSubTypeHoleFit, + tcSubTypeAmbiguity, tcSubMult, tcSubTypeMono, checkConstraints, checkTvConstraints, buildImplicationFor, buildTvImplication, emitResidualTvConstraint, @@ -99,13 +99,13 @@ 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.Types.SrcLoc( GenLocated(..) ) import GHC.Utils.Misc import GHC.Utils.Outputable as Outputable @@ -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 @@ -1425,18 +1425,29 @@ tcWrapResultO orig rn_expr expr actual_ty res_ty ; wrap <- tcSubType orig GenSigCtxt (Just $ HsExprRnThing rn_expr) actual_ty res_ty ; return (mkHsWrap wrap expr) } --- | A version of 'tcWrapResult' to use when the actual type is a --- rho-type, so nothing to instantiate; just go straight to unify. --- It means we don't need to pass in a CtOrigin. -tcWrapResultMono :: HasDebugCallStack - => HsExpr GhcRn -> HsExpr GhcTc - -> TcRhoType -- ^ Actual; a rho-type, not a sigma-type - -> ExpRhoType -- ^ Expected - -> TcM (HsExpr GhcTc) -tcWrapResultMono rn_expr expr act_ty res_ty - = do { co <- tcSubTypeMono rn_expr act_ty res_ty - ; return (mkHsWrapCo co expr) } +tcCheckAppResult :: HsExpr GhcRn -- The entire application (GhcRn) + -> HsExpr GhcTc -- Head of the application (GhcTc) + -> TcSigmaType -- Inferred type of the application; zonked to + -- expose foralls, but maybe not /deeply/ instantiated + -> ExpRhoType -- Expected type; this is deeply skolemised + -> TcM HsWrapper +-- Unify with expected type from the context +-- See Note [Unify with expected type before typechecking arguments] +-- +-- Match up app_res_ty: the result type of rn_expr +-- with res_ty: the expected result type +tcCheckAppResult rn_expr tc_fun app_res_ty exp_ty + = do { ds_flag <- getDeepSubsumptionFlag_DataConHead tc_fun + ; traceTc "tcCheckResult" (ppr tc_fun $$ ppr ds_flag) + ; let origin = exprCtOrigin rn_expr + ; case exp_ty of + Infer inf_res -> fillInferResult ds_flag origin app_res_ty inf_res + Check res_ty -> tcSubTypeDS (Just tc_fun) ds_flag + (unifyExprType rn_expr) + origin GenSigCtxt + app_res_ty res_ty } +------------------------ -- | A version of 'tcSubType' to use when the actual type is a rho-type, -- so that no instantiation is needed. tcSubTypeMono :: HasDebugCallStack @@ -1460,37 +1471,17 @@ tcSubTypePat :: CtOrigin -> UserTypeCtxt -- to tcSubType -- If wrap = tc_sub_type_et t1 t2 -- => wrap :: t1 ~~> t2 -tcSubTypePat inst_orig ctxt (Check ty_actual) ty_expected - = tc_sub_type unifyTypeET inst_orig ctxt ty_actual ty_expected - -tcSubTypePat _ _ (Infer inf_res) ty_expected - = do { co <- fillInferResultNoInst ty_expected inf_res - -- In patterns we do not instantatiate - - ; return (mkWpCastN (mkSymCo co)) } - ---------------- +tcSubTypePat inst_orig ctxt exp_actual ty_expected + = do { ds_flag <- getDeepSubsumptionFlag + ; case exp_actual of + Infer inf_res -> do { co <- fillInferResultNoInst ty_expected inf_res + -- NoInst: in patterns we do not instantatiate + ; return (mkWpCastN (mkSymCo co)) } --- | A subtype check that performs deep subsumption. --- See also 'tcSubTypeMono', for when no instantiation is required. -tcSubTypeDS :: HsExpr GhcTc -- ^ App head (for error messages only) - -> DeepSubsumptionDepth - -> HsExpr GhcRn - -> TcRhoType -- ^ Actual type; a rho-type, not a sigma-type - -> TcRhoType -- ^ Expected type - -- DeepSubsumption <=> when checking, this type - -- is deeply skolemised - -> TcM HsWrapper --- Only one call site, in GHC.Tc.Gen.App.checkResultTy -tcSubTypeDS tc_fun ds_depth rn_expr act_rho exp_rho - = do { wrap <- tc_sub_type_deep (Just tc_fun, Top) ds_depth - (unifyExprType rn_expr) - (exprCtOrigin rn_expr) - GenSigCtxt act_rho exp_rho - ; return (mkWpSubType wrap) } + Check ty_actual -> tcSubTypeDS Nothing ds_flag unifyTypeET + inst_orig ctxt ty_actual ty_expected } --------------- - -- | Checks that the 'actual' type is more polymorphic than the 'expected' type. tcSubType :: CtOrigin -- ^ Used when instantiating -> UserTypeCtxt -- ^ Used when skolemising @@ -1499,13 +1490,12 @@ tcSubType :: CtOrigin -- ^ Used when instantiating -> ExpRhoType -- ^ Expected type -> TcM HsWrapper tcSubType inst_orig ctxt m_thing ty_actual res_ty - = case res_ty of - Check ty_expected -> tc_sub_type (unifyType m_thing) inst_orig ctxt - ty_actual ty_expected + = do { ds_flag <- getDeepSubsumptionFlag + ; case res_ty of + Infer inf_res -> fillInferResult ds_flag inst_orig ty_actual inf_res + Check ty_expected -> tcSubTypeDS Nothing ds_flag (unifyType m_thing) + inst_orig ctxt ty_actual ty_expected } - Infer inf_res -> - do { ds_flag <- getDeepSubsumptionFlag - ; fillInferResult ds_flag inst_orig ty_actual inf_res } --------------- tcSubTypeSigma :: CtOrigin -- where did the actual type arise / why are we @@ -1516,24 +1506,26 @@ tcSubTypeSigma :: CtOrigin -- where did the actual type arise / why are we -- Checks that actual <= expected -- Returns HsWrapper :: actual ~~> expected tcSubTypeSigma orig ctxt ty_actual ty_expected - = tc_sub_type (unifyType Nothing) orig ctxt ty_actual ty_expected + = do { ds_flag <- getDeepSubsumptionFlag + ; tcSubTypeDS Nothing ds_flag (unifyType Nothing) + orig ctxt ty_actual ty_expected } tcSubTypeHoleFit :: DeepSubsumptionFlag -> CtOrigin -> TcSigmaType -- ^ Candidate expression type -> TcSigmaType -- ^ Expected type (= hole type) -> TcM HsWrapper -tcSubTypeHoleFit ds_flag orig cand_ty hole_ty = +tcSubTypeHoleFit ds_flag orig cand_ty hole_ty -- See Note [Deep subsumption in tcCheckHoleFit] - tc_sub_type_ds (Nothing, Top) ds_flag (unifyType Nothing) - orig (ExprSigCtxt NoRRC) cand_ty hole_ty + = tcSubTypeDS Nothing ds_flag (unifyType Nothing) + orig (ExprSigCtxt NoRRC) cand_ty hole_ty --------------- tcSubTypeAmbiguity :: UserTypeCtxt -- Where did this type arise -> TcSigmaType -> TcSigmaType -> TcM HsWrapper -- See Note [Ambiguity check and deep subsumption] tcSubTypeAmbiguity ctxt ty_actual ty_expected - = tc_sub_type_ds (Nothing, Top) + = tcSubTypeDS Nothing Shallow (unifyType Nothing) (AmbiguityCheckOrigin ctxt) @@ -1550,25 +1542,19 @@ addSubTypeCtxt ty_actual ty_expected thing_inside addErrCtxt (SubTypeCtxt ty_expected ty_actual) $ thing_inside ---------------- -tc_sub_type :: (TcType -> TcType -> TcM TcCoercionN) -- How to unify - -> CtOrigin -- Used when instantiating - -> UserTypeCtxt -- Used when skolemising - -> TcSigmaType -- Actual; a sigma-type - -> TcSigmaType -- Expected; also a sigma-type - -> TcM HsWrapper --- Checks that actual_ty is more polymorphic than expected_ty --- If wrap = tc_sub_type t1 t2 --- => wrap :: t1 ~~> t2 --- --- The "how to unify argument" is always a call to `uType TypeLevel orig`, --- but with different ways of constructing the CtOrigin `orig` from --- the argument types and context. - ---------------------- -tc_sub_type unify inst_orig ctxt ty_actual ty_expected - = do { ds_flag <- getDeepSubsumptionFlag - ; wrap <- tc_sub_type_ds (Nothing, Top) ds_flag unify inst_orig ctxt ty_actual ty_expected +tcSubTypeDS :: Maybe (HsExpr GhcTc) + -- ^ app head, and position in its type (for error messages only) + -> DeepSubsumptionFlag + -> (TcType -> TcType -> TcM TcCoercionN) + -> CtOrigin -> UserTypeCtxt -> TcSigmaType + -> TcSigmaType -> TcM HsWrapper +-- tcSubTypeDS is the main subsumption worker function +-- It takes an explicit DeepSubsumptionFlag +-- It adds the WpSubType tag; see Note [Deep subsumption and WpSubType] +tcSubTypeDS tc_fun ds_flag unify inst_orig ctxt ty_actual ty_expected + = do { wrap <- tc_sub_type_ds (tc_fun, Top) ds_flag unify + inst_orig ctxt ty_actual ty_expected ; return (mkWpSubType wrap) } ---------------------- @@ -1578,8 +1564,6 @@ tc_sub_type_ds :: (Maybe (HsExpr GhcTc), Position p) -> (TcType -> TcType -> TcM TcCoercionN) -> CtOrigin -> UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper --- tc_sub_type_ds is the main subsumption worker function --- It takes an explicit DeepSubsumptionFlag tc_sub_type_ds pos ds_flag unify inst_orig ctxt ty_actual ty_expected | definitely_poly ty_expected -- See Note [Don't skolemise unnecessarily] , isRhoTyDS ds_flag ty_actual @@ -1764,8 +1748,8 @@ The effects are in these main places: signatures (e.g. f :: ty; f = e), we must deeply skolemise the type; see the call to tcDeeplySkolemise in tcSkolemiseScoped. -4. In GHC.Tc.Gen.App.tcApp we call tcSubTypeDS to match the result - type. Without deep subsumption, tcSubTypeMono would be sufficent. +4. In GHC.Tc.Gen.App.tcApp we call tcCheckAppResult to check the result type + This does a deep subsumption check when necessary. In all these cases note that the deep skolemisation must be done /first/. Consider (1) @@ -2046,8 +2030,8 @@ instance Outputable DeepSubsumptionFlag where getDeepSubsumptionFlag :: TcM DeepSubsumptionFlag getDeepSubsumptionFlag = - do { ds <- xoptM LangExt.DeepSubsumption - ; if ds + do { user_ds <- xoptM LangExt.DeepSubsumption + ; if user_ds then return $ Deep DeepSub else return Shallow } @@ -2055,38 +2039,19 @@ 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 app_head - | XExpr (ConLikeTc (RealDataCon {})) <- app_head - = Deep TopSub - | XExpr (ExpandedThingTc (HSE _ (L _ f))) <- app_head - = go f - | XExpr (WrapExpr _ f) <- app_head - = go f - | HsVar _ f <- app_head - , isDataConId (unLoc f) - = Deep TopSub - | HsApp _ f _ <- app_head - = go (unLoc f) - | HsAppType _ f _ <- app_head - = go (unLoc f) - | OpApp _ _ f _ <- app_head - = go (unLoc f) - | HsPar _ f <- app_head - = go (unLoc f) - | otherwise - = Shallow - + 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. -- @@ -2347,7 +2312,8 @@ deeplyInstantiate :: CtOrigin -> TcType -> TcM (HsWrapper, Type) -- Instantiate invisible foralls, even ones nested -- (to the right) under arrows deeplyInstantiate orig ty - = go init_subst ty + = traceTc "deeplyInstantiate" (ppr ty) >> + go init_subst ty where init_subst = mkEmptySubst (mkInScopeSet (tyCoVarsOfType ty)) @@ -2356,10 +2322,10 @@ deeplyInstantiate orig ty = do { let tvs = binderVars bndrs -- As per Note [Multiplicity in deep subsumption], -- we treat (a %1 -> b) as if it were forall m. a %m -> b. - ; arg_tys <- traverse oneToMeta arg_tys ; (subst', tvs') <- newMetaTyVarsX subst tvs ; let arg_tys' = substScaledTys subst' arg_tys theta' = substTheta subst' theta + ; arg_tys' <- traverse oneToMeta arg_tys' ; ids1 <- newSysLocalIds (fsLit "di") arg_tys' ; wrap1 <- instCall orig (mkTyVarTys tvs') theta' ; (wrap2, rho2) <- go subst' rho @@ -2371,10 +2337,9 @@ deeplyInstantiate orig ty ; return (idHsWrapper, ty') } oneToMeta :: Scaled TcType -> TcM (Scaled TcType) - oneToMeta (Scaled OneTy ty) - = do { mu <- newMultiplicityVar - ; return $ Scaled mu ty } - oneToMeta ty = return ty + oneToMeta (Scaled OneTy ty) = do { mu <- newMultiplicityVar + ; return $ Scaled mu ty } + oneToMeta ty = return ty tcDeepSplitSigmaTy_maybe ===================================== compiler/GHC/Tc/Zonk/TcType.hs ===================================== @@ -818,19 +818,26 @@ zonkTidyHsCtxt env e@(FunAppCtxt{}) = return (env, e) zonkTidyHsCtxt env (FunTysCtxt ctxt ty i1 i2) = do (env', ty') <- zonkTidyTcType env ty return $ (env', FunTysCtxt ctxt ty' i1 i2) -zonkTidyHsCtxt env (FunResCtxt e i1 ty1 ty2 i2 i3) = do - (env', ty1') <- zonkTidyTcType env ty1 - (env', ty2') <- zonkTidyTcType env' ty2 - return $ (env', FunResCtxt e i1 ty1' ty2' i2 i3) +zonkTidyHsCtxt env (FunResCtxt e n ty1 env_ty) = do + (env', ty1') <- zonkTidyTcType env ty1 + (env', env_ty') <- zonkExpType env' env_ty + return $ (env', FunResCtxt e n ty1' env_ty') zonkTidyHsCtxt env (PatSigErrCtxt sig_ty res_ty) = do (env', sig_ty') <- zonkTidyTcType env sig_ty - (env', res_ty') <- - case res_ty of - Check ty -> zonkTidyTcType env' ty - Infer (IR {ir_ref = ref}) -> do -- inlining readExpTyp_maybe to avoid module dep loops - mb_ty <- liftIO $ readIORef ref - case mb_ty of - Nothing -> error "zonkTidyHsCtxt PatSigErrCtxt" - Just ty -> zonkTidyTcType env' ty - return (env', PatSigErrCtxt sig_ty' (Check res_ty')) + (env', res_ty') <- zonkExpType env' res_ty + return (env', PatSigErrCtxt sig_ty' res_ty') zonkTidyHsCtxt env p = return (env, p) + +zonkExpType :: TidyEnv -> ExpType -> ZonkM (TidyEnv, ExpType) +-- Zonk Infer{} to Check. The hole should have been filled in by now +zonkExpType env (Check ty) + = do { (env', ty') <- zonkTidyTcType env ty + ; return (env', Check ty') } +zonkExpType env (Infer ir@(IR { ir_ref = ref })) + = do { -- inlining readExpTyp_maybe to avoid module dep loops + ; mb_ty <- liftIO $ readIORef ref + ; case mb_ty of + Nothing -> pprPanic "zonkTidyHsCtxt PatSigErrCtxt" (ppr ir) + Just ty -> do { (env', ty') <- zonkTidyTcType env ty + ; return (env', Check ty') } } + View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/a5163a8749ec29dc38403674de5f5831... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/a5163a8749ec29dc38403674de5f5831... You're receiving this email because of your account on gitlab.haskell.org.