[Git][ghc/ghc][wip/T24676] Wibbles
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Wed Apr 24 22:39:42 UTC 2024
Simon Peyton Jones pushed to branch wip/T24676 at Glasgow Haskell Compiler / GHC
Commits:
0a4233b3 by Simon Peyton Jones at 2024-04-25T00:39:22+02:00
Wibbles
- - - - -
2 changed files:
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Utils/Unify.hs
Changes:
=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -320,8 +320,7 @@ before tcValArgs.
-}
tcApp :: HsExpr GhcRn
- -> ExpRhoType -- DeepSubsumption <=> when checking, this type
- -- is deeply skolemised
+ -> ExpRhoType -- When checking, -XDeepSubsumption <=> deeply skolemised
-> TcM (HsExpr GhcTc)
-- See Note [tcApp: typechecking applications]
tcApp rn_expr exp_res_ty
@@ -348,11 +347,11 @@ tcApp rn_expr exp_res_ty
finishApp :: Bool -> HsExpr GhcRn -> (HsExpr GhcRn, AppCtxt)
-> HsExpr GhcTc -> [HsExprArg 'TcpInst]
- -> TcRhoType
- -> ExpRhoType
+ -> TcSigmaType
+ -> ExpRhoType -- When checking, -XDeepSubsumption <=> deeply skolemised
-> TcM (HsExpr GhcTc)
finishApp do_ql rn_expr (rn_fun, fun_ctxt) tc_fun inst_args app_res_rho exp_res_ty
- = do { do_ds <- xoptM LangExt.DeepSubsumption
+ = do { ds_flag <- getDeepSubsumptionFlag
-- Unify with expected type from the context
-- See Note [Unify with expected type before typechecking arguments]
@@ -360,15 +359,15 @@ finishApp do_ql rn_expr (rn_fun, fun_ctxt) tc_fun inst_args app_res_rho exp_res_
-- Match up app_res_rho: the result type of rn_expr
-- with exp_res_ty: the expected result type
; res_wrap <- perhaps_add_res_ty_ctxt $
- if not do_ds
- then -- No deep subsumption
+ case ds_flag of
+ Shallow -> -- No deep subsumption
-- app_res_rho and exp_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 <- unifyExpectedType rn_expr app_res_rho exp_res_ty
; return (mkWpCastN co) }
- else -- Deep subsumption
+ Deep -> -- Deep subsumption
-- Even though both app_res_rho and exp_res_ty are rho-types,
-- they may have nested polymorphism, so if deep subsumption
-- is on we must call tcSubType.
@@ -502,36 +501,36 @@ tcValArg do_ql (EValArgQL { eaql_ctxt = ctxt
do { arg_ty <- liftZonkM $ zonkQuickLook do_ql arg_ty
; traceTc "tcEValArgQL {" (vcat [ ppr rn_head
, text "mb_delta:" <+> ppr mb_delta
- , text "app_res_rho:" <+> ppr res_rho
+ , text "res_rho:" <+> ppr res_rho
, text "arg_ty:" <+> ppr arg_ty
, text "args:" <+> ppr inst_args ])
- ; arg' <- tcScalingUsage mult $
- do_skolemise arg_ty $ \arg_rho ->
- finishApp do_ql rn_expr rn_head tc_fun inst_args res_rho
- (Check arg_rho)
+ ; ds_flag <- getDeepSubsumptionFlag
+ ; (wrap, arg')
+ <- tcScalingUsage mult $
+ tcSkolemise ds_flag GenSigCtxt arg_ty $ \ arg_rho ->
+ -- Tricky point: with deep subsumption, even if mb_delta is Nothing
+ -- arg_ty will be a rho-type (no top-level foralls), but it may have
+ -- /nested/ foralls; so we should deeply skolemise it, in order to
+ -- pass a deeply-skolemised type to finishApp
+ -- Example from haskeline:System.Console.Haskeline.Backend.Terminfo
+ -- output $ blah
+ -- output :: TermAction -> ActionM ()
+ -- type ActionM a = forall m . (..) => ActionT (Draw m) a
+ do { case mb_delta of
+ Nothing -> return ()
+ Just (delta, wanted) -> do { demoteQLDelta delta
+ ; emitConstraints wanted }
+ ; finishApp do_ql rn_expr rn_head tc_fun inst_args res_rho
+ (Check arg_rho) }
+
; traceTc "tcEValArgQL }" $
vcat [ text "rn_head:" <+> ppr rn_head
, text "res_rho:" <+> ppr res_rho ]
; return (EValArg { ea_ctxt = ctxt
- , ea_arg = L arg_loc arg'
+ , ea_arg = L arg_loc (mkHsWrap wrap arg')
, ea_arg_ty = Scaled mult arg_ty }) }
- where
- do_skolemise arg_ty thing_inside = case mb_delta of
- Nothing -> thing_inside arg_ty
- Just (delta, wanted)
- -> do { ds_flag <- getDeepSubsumptionFlag
- ; lvl1 <- getTcLevel
- ; (wrap, arg') <- tcSkolemise ds_flag GenSigCtxt arg_ty $ \ arg_rho ->
- do { demoteQLDelta delta
- ; emitConstraints wanted
- ; lvl2 <- getTcLevel
- ; traceTc "EVQL 2" (vcat [ ppr lvl1 <+> ppr lvl2
- , ppr arg_ty, ppr arg_rho ])
- ; thing_inside arg_rho }
- ; return (mkHsWrap wrap arg') }
-
{- *********************************************************************
* *
@@ -1527,7 +1526,7 @@ isGuardedTy (Scaled _ ty)
| otherwise = False
quickLookArg1 :: Bool -> Delta -> AppCtxt -> LHsExpr GhcRn
- -> Scaled TcRhoType
+ -> Scaled TcRhoType -- Not deeply skolemised, even with -XDeepSubsumption
-> TcM (Delta, HsExprArg 'TcpInst)
-- quickLookArg1 implements the "QL Argument" judgement in Fig 5 of the paper
quickLookArg1 guarded delta ctxt larg@(L _ arg) sc_arg_ty@(Scaled _ arg_ty)
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -19,7 +19,7 @@ module GHC.Tc.Utils.Unify (
buildImplicationFor, buildTvImplication, emitResidualTvConstraint,
-- Skolemisation
- DeepSubsumptionFlag(..), getDeepSubsumptionFlag,
+ DeepSubsumptionFlag(..), getDeepSubsumptionFlag, isRhoTyDS,
tcSkolemise, tcSkolemiseCompleteSig, tcSkolemiseExpectedType,
-- Various unifications
@@ -402,7 +402,7 @@ tcSkolemiseGeneral
-> ([(Name, TcInvisTVBinder)] -> TcType -> TcM result)
-> TcM (HsWrapper, result)
tcSkolemiseGeneral ds_flag ctxt top_ty expected_ty thing_inside
- | definitely_mono ds_flag expected_ty
+ | isRhoTyDS ds_flag expected_ty
-- Fast path for a very very common case: no skolemisation to do
-- But still call checkConstraints in case we need an implication regardless
= do { let sig_skol = SigSkol ctxt top_ty []
@@ -1474,7 +1474,7 @@ tc_sub_type_ds :: DeepSubsumptionFlag
-- It takes an explicit DeepSubsumptionFlag
tc_sub_type_ds ds_flag unify inst_orig ctxt ty_actual ty_expected
| definitely_poly ty_expected -- See Note [Don't skolemise unnecessarily]
- , definitely_mono ds_flag ty_actual
+ , isRhoTyDS ds_flag ty_actual
= do { traceTc "tc_sub_type (drop to equality)" $
vcat [ text "ty_actual =" <+> ppr ty_actual
, text "ty_expected =" <+> ppr ty_expected ]
@@ -1506,12 +1506,6 @@ tc_sub_type_shallow unify inst_orig ty_actual sk_rho
; return (mkWpCastN cow <.> wrap) }
----------------------
-definitely_mono :: DeepSubsumptionFlag -> TcType -> Bool
-definitely_mono ds_flag ty
- = case ds_flag of
- Shallow -> isRhoTy ty -- isRhoTy: no top level forall or (=>)
- Deep -> isDeepRhoTy ty -- "deep" version: no nested forall or (=>)
-
definitely_poly :: TcType -> Bool
-- A very conservative test:
-- see Note [Don't skolemise unnecessarily]
@@ -1729,7 +1723,8 @@ getDeepSubsumptionFlag :: TcM DeepSubsumptionFlag
getDeepSubsumptionFlag = do { ds <- xoptM LangExt.DeepSubsumption
; if ds then return Deep else return Shallow }
-tc_sub_type_deep :: (TcType -> TcType -> TcM TcCoercionN) -- How to unify
+tc_sub_type_deep :: HasDebugCallStack
+ => (TcType -> TcType -> TcM TcCoercionN) -- How to unify
-> CtOrigin -- Used when instantiating
-> UserTypeCtxt -- Used when skolemising
-> TcSigmaType -- Actual; a sigma-type
@@ -1886,6 +1881,12 @@ isDeepRhoTy ty
| Just (_, res) <- tcSplitFunTy_maybe ty = isDeepRhoTy res
| otherwise = True -- No forall, (=>), or (->) at top
+isRhoTyDS :: DeepSubsumptionFlag -> TcType -> Bool
+isRhoTyDS ds_flag ty
+ = case ds_flag of
+ Shallow -> isRhoTy ty -- isRhoTy: no top level forall or (=>)
+ Deep -> isDeepRhoTy ty -- "deep" version: no nested forall or (=>)
+
{-
************************************************************************
* *
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0a4233b32de3cc054dda0d28accaffa216cd4085
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0a4233b32de3cc054dda0d28accaffa216cd4085
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20240424/45f568a1/attachment-0001.html>
More information about the ghc-commits
mailing list