Simon Peyton Jones pushed to branch wip/T27210 at Glasgow Haskell Compiler / GHC Commits: ee946dfa by Simon Peyton Jones at 2026-04-24T15:25:15+01:00 Fix assertion check in checkResultTy As #27210 shows, the assertion was a little bit too eager. I refactored a bit by moving some code from GHC.Tc.Gen.App to GHC.Tc.Utils.Unify; see the new function tcSubTypeApp, which replaces tcSubTypeDS - - - - - 6 changed files: - compiler/GHC/Tc/Gen/App.hs - compiler/GHC/Tc/Gen/Head.hs - compiler/GHC/Tc/Utils/Unify.hs - + testsuite/tests/typecheck/should_fail/T27210.hs - + testsuite/tests/typecheck/should_fail/T27210.stderr - testsuite/tests/typecheck/should_fail/all.T Changes: ===================================== compiler/GHC/Tc/Gen/App.hs ===================================== @@ -458,45 +458,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 - -- 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] --- --- Match up app_res_rho: the result type of rn_expr --- with res_ty: the expected result type +checkResultTy rn_expr (tc_fun, fun_loc) inst_args app_res_rho res_ty = 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 } } + tcSubTypeApp rn_expr tc_fun app_res_rho 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 @@ -506,7 +470,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_rho res_ty $ thing_inside ---------------- ===================================== compiler/GHC/Tc/Gen/Head.hs ===================================== @@ -791,10 +791,9 @@ 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. Note [Data constructors are linear by default] says: Just :: a. a %1 -> Maybe a ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -11,7 +11,7 @@ module GHC.Tc.Utils.Unify ( -- Full-blown subsumption tcWrapResult, tcWrapResultO, tcWrapResultMono, - tcSubType, tcSubTypeSigma, tcSubTypePat, tcSubTypeDS, tcSubTypeHoleFit, + tcSubType, tcSubTypeSigma, tcSubTypePat, tcSubTypeApp, tcSubTypeHoleFit, addSubTypeCtxt, tcSubTypeAmbiguity, tcSubMult, checkConstraints, checkTvConstraints, @@ -1488,24 +1488,62 @@ tcSubTypePat _ _ (Infer inf_res) ty_expected --------------- --- | 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 +-- | Connect up the inferred type of an application with the expected type. +-- This is usually just a unification, but with deep subsumption there is more to do. +tcSubTypeApp :: HsExpr GhcRn + -> HsExpr GhcTc -- Head + -> TcRhoType -- Inferred type of the application; zonked to + -- expose foralls, but maybe not /deeply/ instantiated + -> ExpRhoType -- Expected type; this is deeply skolemised + -> TcM HsWrapper +tcSubTypeApp 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 } + +tcSubTypeApp rn_expr tc_fun app_res_rho (Check exp_rho) + = do { ds_flag <- getDeepSubsumptionFlag_DataConHead tc_fun + ; traceTc "tcSubTypeApp {" $ + vcat [ text "tc_fun:" <+> ppr tc_fun + , text "app_res_rho:" <+> ppr app_res_rho + , text "exp_rho:" <+> ppr exp_rho + , text "ds_flag:" <+> ppr ds_flag ] + ; wrap <- 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 exp_rho + ; return (mkWpCastN co) } + + Deep ds_depth -- Deep subsumption is ON + -- 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. + -> tc_sub_type_deep (Just tc_fun, Top) ds_depth + (unifyExprType rn_expr) + (exprCtOrigin rn_expr) + GenSigCtxt app_res_rho exp_rho + + ; traceTc "tcSubTypeApp }" $ + vcat [ text "tc_fun:" <+> ppr tc_fun + , text "wrap:" <+> ppr wrap ] + ; return (mkWpSubType wrap) } +-- | Variant of 'getDeepSubsumptionFlag' which enables a top-level subsumption +-- in order to implement the plan of Note [Typechecking data constructors]. +getDeepSubsumptionFlag_DataConHead :: HsExpr GhcTc -> TcM DeepSubsumptionFlag +getDeepSubsumptionFlag_DataConHead app_head + = do { user_ds <- xoptM LangExt.DeepSubsumption + ; return $ if | user_ds + -> Deep DeepSub + | XExpr (ConLikeTc (RealDataCon {})) <- app_head + -> Deep TopSub + | otherwise + -> Shallow } + --------------- -- | Checks that the 'actual' type is more polymorphic than the 'expected' type. @@ -2104,18 +2142,6 @@ getDeepSubsumptionFlag = else return Shallow } --- | Variant of 'getDeepSubsumptionFlag' which enables a top-level subsumption --- in order to implement the plan of Note [Typechecking data constructors]. -getDeepSubsumptionFlag_DataConHead :: HsExpr GhcTc -> TcM DeepSubsumptionFlag -getDeepSubsumptionFlag_DataConHead app_head - = do { user_ds <- xoptM LangExt.DeepSubsumption - ; return $ if | user_ds - -> Deep DeepSub - | XExpr (ConLikeTc (RealDataCon {})) <- app_head - -> Deep TopSub - | otherwise - -> Shallow } - -- | 'tc_sub_type_deep' is where the actual work happens for deep subsumption. -- @@ -2132,11 +2158,7 @@ tc_sub_type_deep :: HasDebugCallStack -> TcRhoType -- ^ Expected; deeply skolemised -> TcM HsWrapper tc_sub_type_deep fun_pos@(tc_fun, pos) ds_depth unify inst_orig ctxt ty_actual ty_expected - = assertPpr (isDeeplySkolemised ty_expected) - (vcat [ text "tc_sub_type_deep: expected type is not a deep rho type" - , text "ty_expected:" <+> ppr ty_expected - , text "ty_actual:" <+> ppr ty_actual - ]) $ + = assert_precondition $ do { traceTc "tc_sub_type_deep" $ vcat [ text "ty_actual =" <+> ppr ty_actual , text "ty_expected =" <+> ppr ty_expected ] @@ -2250,6 +2272,27 @@ tc_sub_type_deep fun_pos@(tc_fun, pos) ds_depth unify inst_orig ctxt ty_actual t where given_orig = GivenOrigin (SigSkol GenSigCtxt exp_arg []) + -- Assertion check. + -- If DeepSubsumption is on (ds_depth = Deep DeepSub) then `exp_rho` + -- should already be deeply skolemised; the assertion checks this + -- But if DeepSubsumption is NOT on, but there is a data constructor at the + -- head, we must still call `tc_sub_type_deep` (for the multiplicity arrows) + -- Hence ds_flag = Deep TopSub, but `exp_rho` will only be /top-level/ skolemised + -- So we can only check for top-level skolemisation (`isRhoTy`) + -- Example of the latter (see #27210), with -XNoDeepSubsumption + -- foo :: forall a. a -> forall b. b -> (a,b) + -- foo = (,) + -- We will only shallowly-skolemise the expected type + assert_precondition = assertPpr ty_expected_is_ok $ + vcat [ text "tc_sub_type_deep: expected type is not a deep rho type" + , text "ty_expected:" <+> ppr ty_expected + , text "ty_actual:" <+> ppr ty_actual ] + ty_expected_is_ok + = case ds_depth of + TopSub -> isRhoTy ty_expected + DeepSub -> isDeeplySkolemised ty_expected + + -- | Whether to do deep subsumption when recurring inside arguments. recurInArgumentDSFlag :: DeepSubsumptionDepth -> DeepSubsumptionFlag recurInArgumentDSFlag = \case @@ -5145,5 +5188,3 @@ lookupCycleBreakerVar cbv (IS { inert_cycle_breakers = cbvs_stack }) = tyfam_app | otherwise = pprPanic "lookupCycleBreakerVar found an unbound cycle breaker" (ppr cbv $$ ppr cbvs_stack) - --------------------------------------------------------------------------------- ===================================== testsuite/tests/typecheck/should_fail/T27210.hs ===================================== @@ -0,0 +1,11 @@ +{-# LANGUAGE RankNTypes, ExistentialQuantification #-} + +-- NB: No deep subsumption + +module T27210 where + +data Parser a + = forall x. BindP (Parser x) (x -> Parser a) + +oneM :: Parser a -> ( forall x. (a -> Parser x) -> Parser x ) +oneM = BindP ===================================== testsuite/tests/typecheck/should_fail/T27210.stderr ===================================== @@ -0,0 +1,9 @@ +T27210.hs:11:8: error: [GHC-83865] + • Couldn't match expected type: forall x. + (a -> Parser x) -> Parser x + with actual type: (a -> Parser a0) -> Parser a0 + • In the expression: BindP + In an equation for ‘oneM’: oneM = BindP + • Relevant bindings include + oneM :: Parser a -> forall x. (a -> Parser x) -> Parser x + (bound at T27210.hs:11:1) ===================================== testsuite/tests/typecheck/should_fail/all.T ===================================== @@ -758,3 +758,4 @@ test('T23162d', normal, compile, ['']) test('T26823', normal, compile_fail, ['']) test('T26861', normal, compile_fail, ['']) test('T26862', normal, compile_fail, ['']) +test('T27210', normal, compile_fail, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ee946dfa797ccbeffa5f29b651773728... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ee946dfa797ccbeffa5f29b651773728... You're receiving this email because of your account on gitlab.haskell.org.