GitLab

Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC

Commits:

9797052b

by Simon Peyton Jones at 2026-04-28T13:25:37-04: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  -> True
 +          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

 +{-# 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

 +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, [''])