[Git][ghc/ghc][wip/T24676] Fix bugs
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Wed Apr 24 12:10:05 UTC 2024
Simon Peyton Jones pushed to branch wip/T24676 at Glasgow Haskell Compiler / GHC
Commits:
18712afb by Simon Peyton Jones at 2024-04-24T14:09:20+02:00
Fix bugs
expanding EValArgQL
- - - - -
6 changed files:
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Gen/Expr.hs
- compiler/GHC/Tc/Gen/Head.hs
- compiler/GHC/Tc/Gen/Match.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- compiler/GHC/Tc/Utils/Unify.hs
Changes:
=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -151,7 +151,7 @@ tcInferSigma inst (L loc rn_expr)
do { (fun@(rn_fun,fun_ctxt), rn_args) <- splitHsApps rn_expr
; do_ql <- wantQuickLook rn_fun
; (tc_fun, fun_sigma) <- tcInferAppHead fun
- ; (_delta, inst_args, app_res_sigma) <- tcInstFun do_ql inst (tc_fun, fun_ctxt) fun_sigma rn_args
+ ; (_delta, inst_args, app_res_sigma) <- tcInstFun do_ql inst fun_ctxt tc_fun fun_sigma rn_args
; _tc_args <- tcValArgs do_ql inst_args
; return app_res_sigma }
@@ -319,7 +319,10 @@ The latter is much better. That is why we call unifyExpectedType
before tcValArgs.
-}
-tcApp :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)
+tcApp :: HsExpr GhcRn
+ -> ExpRhoType -- DeepSubsumption <=> when checking, this type
+ -- is deeply skolemised
+ -> TcM (HsExpr GhcTc)
-- See Note [tcApp: typechecking applications]
tcApp rn_expr exp_res_ty
= do { (fun@(rn_fun, fun_ctxt), rn_args) <- splitHsApps rn_expr
@@ -333,30 +336,29 @@ tcApp rn_expr exp_res_ty
-- Instantiate
; do_ql <- wantQuickLook rn_fun
- ; (delta, inst_args, app_res_rho) <- tcInstFun do_ql True (tc_fun, fun_ctxt) fun_sigma rn_args
+ ; (delta, inst_args, app_res_rho)
+ <- tcInstFun do_ql True fun_ctxt tc_fun fun_sigma rn_args
-- Quick look at result
; app_res_rho <- if do_ql
then quickLookResultType delta app_res_rho exp_res_ty
else return app_res_rho
+ ; finishApp do_ql rn_expr fun tc_fun inst_args app_res_rho exp_res_ty }
+
+finishApp :: Bool -> HsExpr GhcRn -> (HsExpr GhcRn, AppCtxt)
+ -> HsExpr GhcTc -> [HsExprArg 'TcpInst]
+ -> TcRhoType
+ -> ExpRhoType
+ -> 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
+
-- Unify with expected type from the context
-- See Note [Unify with expected type before typechecking arguments]
--
- -- 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
- -- the source program; it was added by the renamer. See
- -- Note [Handling overloaded and rebindable constructs] in GHC.Rename.Expr
- ; let perhaps_add_res_ty_ctxt thing_inside
- | insideExpansion fun_ctxt
- = addHeadCtxt fun_ctxt thing_inside
- | otherwise
- = addFunResCtxt rn_fun rn_args app_res_rho exp_res_ty $
- thing_inside
-
-- Match up app_res_rho: the result type of rn_expr
-- with exp_res_ty: the expected result type
- ; do_ds <- xoptM LangExt.DeepSubsumption
; res_wrap <- perhaps_add_res_ty_ctxt $
if not do_ds
then -- No deep subsumption
@@ -387,11 +389,8 @@ tcApp rn_expr exp_res_ty
; whenDOptM Opt_D_dump_tc_trace $
do { inst_args <- liftZonkM $ mapM zonkArg inst_args -- Only when tracing
; traceTc "tcApp }" (vcat [ text "rn_fun:" <+> ppr rn_fun
- , text "rn_args:" <+> ppr rn_args
, text "inst_args" <+> brackets (pprWithCommas pprHsExprArgTc inst_args)
, text "do_ql: " <+> ppr do_ql
- , text "fun_sigma: " <+> ppr fun_sigma
- , text "delta: " <+> ppr delta
, text "app_res_rho:" <+> ppr app_res_rho
, text "exp_res_ty:" <+> ppr exp_res_ty
, text "rn_expr:" <+> ppr rn_expr
@@ -401,6 +400,18 @@ tcApp rn_expr exp_res_ty
-- Wrap the result
; return (mkHsWrap res_wrap tc_expr) }
+ 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
+ -- the source program; it was added by the renamer. See
+ -- Note [Handling overloaded and rebindable constructs] in GHC.Rename.Expr
+ perhaps_add_res_ty_ctxt thing_inside
+ | insideExpansion fun_ctxt
+ = addHeadCtxt fun_ctxt thing_inside
+ | otherwise
+ = addFunResCtxt rn_fun inst_args app_res_rho exp_res_ty $
+ thing_inside
+
--------------------
wantQuickLook :: HsExpr GhcRn -> TcM Bool
@@ -430,9 +441,9 @@ zonkQuickLook do_ql ty
-- see what is going on. For that reason, it is not a full zonk: add
-- more if you need it.
zonkArg :: HsExprArg 'TcpInst -> ZonkM (HsExprArg 'TcpInst)
-zonkArg eva@(EValArg { eva_arg_ty = Scaled m ty })
+zonkArg eva@(EValArg { ea_arg_ty = Scaled m ty })
= do { ty' <- zonkTcType ty
- ; return (eva { eva_arg_ty = Scaled m ty' }) }
+ ; return (eva { ea_arg_ty = Scaled m ty' }) }
zonkArg arg = return arg
@@ -442,60 +453,85 @@ zonkArg arg = return arg
tcValArgs :: Bool -- Quick-look on?
-> [HsExprArg 'TcpInst] -- Actual argument
-> TcM [HsExprArg 'TcpTc] -- Resulting argument
-tcValArgs do_ql args
- = mapM tc_arg args
- where
- tc_arg :: HsExprArg 'TcpInst -> TcM (HsExprArg 'TcpTc)
- tc_arg (EPrag l p) = return (EPrag l (tcExprPrag p))
- tc_arg (EWrap w) = return (EWrap w)
- tc_arg (ETypeArg l hs_ty ty) = return (ETypeArg l hs_ty ty)
-
- tc_arg eva@(EValArg { eva_arg = arg, eva_arg_ty = Scaled mult arg_ty
- , eva_ctxt = ctxt })
- = do { -- Crucial step: expose QL results before checking arg_ty
- -- So far as the paper is concerned, this step applies
- -- the poly-substitution Theta, learned by QL, so that we
- -- "see" the polymorphism in that argument type. E.g.
- -- (:) e ids, where ids :: [forall a. a->a]
- -- (:) :: forall p. p->[p]->[p]
- -- Then Theta = [p :-> forall a. a->a], and we want
- -- to check 'e' with expected type (forall a. a->a)
- -- See Note [Instantiation variables are short lived]
- arg_ty <- liftZonkM $ zonkQuickLook do_ql arg_ty
-
- -- Now check the argument
- ; arg' <- tcScalingUsage mult $
- do { traceTc "tcEValArg" $
- vcat [ ppr ctxt
- , text "arg type:" <+> ppr arg_ty
- , text "arg:" <+> ppr arg ]
- ; tcEValArg ctxt arg arg_ty }
-
- ; return (eva { eva_arg = ValArg arg'
- , eva_arg_ty = Scaled mult arg_ty }) }
-
-tcEValArg :: AppCtxt -> EValArg 'TcpInst -> TcSigmaTypeFRR -> TcM (LHsExpr GhcTc)
--- Typecheck one value argument of a function call
-tcEValArg ctxt (ValArg larg@(L arg_loc arg)) exp_arg_sigma
+tcValArgs do_ql args = mapM (tcValArg do_ql) args
+
+tcValArg :: Bool -- Quick-look on?
+ -> HsExprArg 'TcpInst -- Actual argument
+ -> TcM (HsExprArg 'TcpTc) -- Resulting argument
+tcValArg _ (EPrag l p) = return (EPrag l (tcExprPrag p))
+tcValArg _ (EWrap w) = return (EWrap w)
+tcValArg _ (ETypeArg l hs_ty ty) = return (ETypeArg l hs_ty ty)
+
+tcValArg do_ql (EValArg { ea_ctxt = ctxt
+ , ea_arg = larg@(L arg_loc arg)
+ , ea_arg_ty = Scaled mult arg_ty })
= addArgCtxt ctxt larg $
- do { arg' <- tcPolyExpr arg (mkCheckExpType exp_arg_sigma)
- ; return (L arg_loc arg') }
-
-tcEValArg ctxt (ValArgQL { va_expr = larg@(L arg_loc _)
- , va_fun = (inner_fun, fun_ctxt)
- , va_args = inner_args
- , va_ty = app_res_rho }) exp_arg_sigma
+ do { traceTc "tcValArg" $
+ vcat [ ppr ctxt
+ , text "arg type:" <+> ppr arg_ty
+ , text "arg:" <+> ppr arg ]
+
+ -- Crucial step: expose QL results before checking arg_ty
+ -- So far as the paper is concerned, this step applies
+ -- the poly-ubstitution Theta, learned by QL, so that we
+ -- "see" the polymorphism in that argument type. E.g.
+ -- (:) e ids, where ids :: [forall a. a->a]
+ -- (:) :: forall p. p->[p]->[p]
+ -- Then Theta = [p :-> forall a. a->a], and we want
+ -- to check 'e' with expected type (forall a. a->a)
+ -- See Note [Instantiation variables are short lived]
+ ; arg_ty <- liftZonkM $ zonkQuickLook do_ql arg_ty
+
+ -- Now check the argument
+ ; arg' <- tcScalingUsage mult $
+ tcPolyExpr arg (mkCheckExpType arg_ty)
+
+ ; return (EValArg { ea_ctxt = ctxt
+ , ea_arg = L arg_loc arg'
+ , ea_arg_ty = Scaled mult arg_ty }) }
+
+tcValArg do_ql (EValArgQL { eaql_ctxt = ctxt
+ , eaql_arg_ty = Scaled mult arg_ty
+ , eaql_larg = larg@(L arg_loc rn_expr)
+ , eaql_head = rn_head
+ , eaql_delta = mb_delta
+ , eaql_tc_fun = tc_fun
+ , eaql_args = inst_args
+ , eaql_res_rho = res_rho })
= addArgCtxt ctxt larg $
- do { traceTc "tcEValArgQL {" (vcat [ ppr inner_fun <+> ppr inner_args ])
- ; tc_args <- tcValArgs True inner_args
-
- ; co <- unifyType Nothing app_res_rho exp_arg_sigma
- ; arg' <- mkHsWrapCo co <$> rebuildHsApps inner_fun fun_ctxt tc_args app_res_rho
+ 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 "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)
; traceTc "tcEValArgQL }" $
- vcat [ text "inner_fun:" <+> ppr inner_fun
- , text "app_res_rho:" <+> ppr app_res_rho
- , text "exp_arg_sigma:" <+> ppr exp_arg_sigma ]
- ; return (L arg_loc arg') }
+ 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_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') }
+
{- *********************************************************************
* *
@@ -503,11 +539,6 @@ tcEValArg ctxt (ValArgQL { va_expr = larg@(L arg_loc _)
* *
********************************************************************* -}
-type Delta = TcTyVarSet -- Set of instantiation variables,
- -- written \kappa in the QL paper
- -- Just a set of ordinary unification variables,
- -- but ones that QL may fill in with polytypes
-
tcInstFun :: Bool -- True <=> Do quick-look
-> Bool -- False <=> Instantiate only /inferred/ variables at the end
-- so may return a sigma-type
@@ -517,7 +548,8 @@ tcInstFun :: Bool -- True <=> Do quick-look
-- in tcInferSigma, which is used only to implement :type
-- Otherwise we do eager instantiation; in Fig 5 of the paper
-- |-inst returns a rho-type
- -> (HsExpr GhcTc, AppCtxt)
+ -> AppCtxt
+ -> HsExpr GhcTc
-- ^ For error messages and to retrieve concreteness information
-- of the function
-> TcSigmaType -> [HsExprArg 'TcpRn]
@@ -527,7 +559,7 @@ tcInstFun :: Bool -- True <=> Do quick-look
-- This 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 (tc_fun, fun_ctxt) fun_sigma rn_args
+tcInstFun do_ql inst_final fun_ctxt tc_fun fun_sigma rn_args
= do { traceTc "tcInstFun" (vcat [ text "tc_fun" <+> ppr tc_fun
, text "fun_sigma" <+> ppr fun_sigma
, text "fun_ctxt" <+> ppr fun_ctxt
@@ -535,15 +567,11 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args
, text "do_ql" <+> ppr do_ql ])
; go emptyVarSet [] [] fun_sigma rn_args }
where
- fun_orig
- | VAExpansion (OrigStmt{}) _ _ <- fun_ctxt
- = DoOrigin
- | VAExpansion (OrigPat pat) _ _ <- fun_ctxt
- = DoPatOrigin pat
- | VAExpansion (OrigExpr e) _ _ <- fun_ctxt
- = exprCtOrigin e
- | VACall e _ _ <- fun_ctxt
- = exprCtOrigin e
+ fun_orig = case fun_ctxt of
+ VAExpansion (OrigStmt{}) _ _ -> DoOrigin
+ VAExpansion (OrigPat pat) _ _ -> DoPatOrigin pat
+ VAExpansion (OrigExpr e) _ _ -> exprCtOrigin e
+ VACall e _ _ -> exprCtOrigin e
-- These are the type variables which must be instantiated to concrete
-- types. See Note [Representation-polymorphic Ids with no binding]
@@ -640,7 +668,7 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args
-- nested forall a. Eq a => forall b. Show b => blah
-- Rule ITVDQ from the GHC Proposal #281
- go1 delta acc so_far fun_ty ((EValArg { eva_arg = ValArg arg }) : rest_args)
+ go1 delta acc so_far 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,
@@ -661,10 +689,10 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args
= go1 delta (EPrag sp prag : acc) so_far fun_ty args
-- Rule ITYARG from Fig 4 of the QL paper
- go1 delta acc so_far fun_ty ( ETypeArg { eva_ctxt = ctxt, eva_hs_ty = hs_ty }
+ go1 delta acc so_far fun_ty ( ETypeArg { ea_ctxt = ctxt, ea_hs_ty = hs_ty }
: rest_args )
= do { (ty_arg, inst_ty) <- tcVTA fun_conc_tvs fun_ty hs_ty
- ; let arg' = ETypeArg { eva_ctxt = ctxt, eva_hs_ty = hs_ty, eva_ty = ty_arg }
+ ; let arg' = ETypeArg { ea_ctxt = ctxt, ea_hs_ty = hs_ty, ea_ty_arg = ty_arg }
; go delta (arg' : acc) so_far inst_ty rest_args }
-- Rule IVAR from Fig 4 of the QL paper:
@@ -695,7 +723,7 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args
-- When we come to unify the nus (in qlUnify), we will call
-- unifyKind on the kinds. This will do the right thing, even though
-- we are manually filling in the nu metavariables.
- new_arg_tv (ValArg (L _ arg)) i =
+ new_arg_tv (L _ arg) i =
newOpenFlexiFRRTyVar $
FRRExpectedFunTy (ExpectedFunTyArg (HsExprTcThing tc_fun) arg) i
; arg_nus <- zipWithM new_arg_tv
@@ -721,7 +749,7 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args
-- Rule IARG from Fig 4 of the QL paper:
go1 delta acc so_far fun_ty
- (eva@(EValArg { eva_arg = ValArg arg, eva_ctxt = ctxt }) : rest_args)
+ (eva@(EValArg { ea_arg = arg, ea_ctxt = ctxt }) : rest_args)
= do { let herald = case fun_ctxt of
VAExpansion (OrigStmt{}) _ _ -> ExpectedFunTySyntaxOp DoOrigin tc_fun
_ -> ExpectedFunTyArg (HsExprTcThing tc_fun) (unLoc arg)
@@ -739,10 +767,9 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args
then addArgCtxt ctxt arg $
-- Context needed for constraints
-- generated by calls in arg
- quickLookArg delta arg arg_ty
- else return (delta, ValArg arg)
- ; let acc' = eva { eva_arg = arg', eva_arg_ty = arg_ty }
- : addArgWrap wrap acc
+ quickLookArg delta ctxt arg arg_ty
+ else return (delta, eva { ea_arg_ty = arg_ty })
+ ; let acc' = arg' : addArgWrap wrap acc
; go delta' acc' (arg_ty:so_far) res_ty rest_args }
-- Is the argument supposed to instantiate a forall?
@@ -759,7 +786,7 @@ looks_like_type_arg ETypeArg{} =
-- The argument is clearly supposed to instantiate an invisible forall,
-- i.e. when we see `f @a`, we expect `f :: forall x. t`.
True
-looks_like_type_arg EValArg{ eva_arg = ValArg (L _ e) } =
+looks_like_type_arg EValArg{ ea_arg = L _ e } =
-- Check if the argument is supposed to instantiate a visible forall,
-- i.e. when we see `f (type Int)`, we expect `f :: forall x -> t`,
-- but not if we see `f True`.
@@ -1457,51 +1484,54 @@ Wrinkles:
----------------
quickLookArg :: Delta
+ -> AppCtxt
-> LHsExpr GhcRn -- ^ Argument
-> Scaled TcSigmaTypeFRR -- ^ Type expected by the function
- -> TcM (Delta, EValArg 'TcpInst)
+ -> TcM (Delta, HsExprArg 'TcpInst)
-- See Note [Quick Look at value arguments]
--
-- The returned Delta is a superset of the one passed in
-- with added instantiation variables from
-- (a) the call itself
-- (b) the arguments of the call
-quickLookArg delta larg (Scaled _ arg_ty)
- | isEmptyVarSet delta = skipQuickLook delta larg
- | otherwise = go arg_ty
+quickLookArg delta ctxt larg orig_arg_ty
+ | isEmptyVarSet delta = skipQuickLook delta ctxt larg orig_arg_ty
+ | otherwise = go orig_arg_ty
where
- guarded = isGuardedTy arg_ty
+ guarded = isGuardedTy orig_arg_ty
-- NB: guardedness is computed based on the original,
-- unzonked arg_ty (before calling `go`), so that we deliberately do
-- not exploit guardedness that emerges a result of QL on earlier args
- go arg_ty | not (isRhoTy arg_ty)
- = skipQuickLook delta larg
+ go sc_arg_ty@(Scaled mult arg_ty)
+ | not (isRhoTy arg_ty)
+ = skipQuickLook delta ctxt larg sc_arg_ty
- -- This top-level zonk step, which is the reason
- -- we need a local 'go' loop, is subtle
- -- See Section 9 of the QL paper
- | Just kappa <- getTyVar_maybe arg_ty
- , kappa `elemVarSet` delta
- = do { info <- readMetaTyVar kappa
- ; case info of
- Indirect arg_ty' -> go arg_ty'
- Flexi -> quickLookArg1 guarded delta larg arg_ty }
+ -- This top-level zonk step, which is the reason
+ -- we need a local 'go' loop, is subtle
+ -- See Section 9 of the QL paper
+ | Just kappa <- getTyVar_maybe arg_ty
+ , kappa `elemVarSet` delta
+ = do { info <- readMetaTyVar kappa
+ ; case info of
+ Indirect arg_ty'' -> go (Scaled mult arg_ty'')
+ Flexi -> quickLookArg1 guarded delta ctxt larg sc_arg_ty }
- | otherwise
- = quickLookArg1 guarded delta larg arg_ty
+ | otherwise
+ = quickLookArg1 guarded delta ctxt larg sc_arg_ty
-isGuardedTy :: TcType -> Bool
-isGuardedTy ty
+isGuardedTy :: Scaled TcType -> Bool
+isGuardedTy (Scaled _ ty)
| Just (tc,_) <- tcSplitTyConApp_maybe ty = isGenerativeTyCon tc Nominal
| Just {} <- tcSplitAppTy_maybe ty = True
| otherwise = False
-quickLookArg1 :: Bool -> Delta -> LHsExpr GhcRn -> TcSigmaTypeFRR
- -> TcM (Delta, EValArg 'TcpInst)
+quickLookArg1 :: Bool -> Delta -> AppCtxt -> LHsExpr GhcRn
+ -> Scaled TcRhoType
+ -> TcM (Delta, HsExprArg 'TcpInst)
-- quickLookArg1 implements the "QL Argument" judgement in Fig 5 of the paper
-quickLookArg1 guarded delta larg@(L _ arg) arg_ty
- = do { ((rn_fun, fun_ctxt), rn_args) <- splitHsApps arg
+quickLookArg1 guarded delta ctxt larg@(L _ arg) sc_arg_ty@(Scaled _ arg_ty)
+ = do { (rn_head@(rn_fun, fun_ctxt), rn_args) <- splitHsApps arg
-- Step 1: get the type of the head of the argument
; mb_fun_ty <- tcInferAppHead_maybe rn_fun
@@ -1512,12 +1542,22 @@ quickLookArg1 guarded delta larg@(L _ arg) arg_ty
, text "args:" <+> ppr rn_args ]
; case mb_fun_ty of {
- Nothing -> skipQuickLook delta larg ; -- fun is too complicated
+ Nothing -> skipQuickLook delta ctxt larg sc_arg_ty ; -- fun is too complicated
Just (tc_fun, fun_sigma) ->
-- Step 2: use |-inst to instantiate the head applied to the arguments
do { do_ql <- wantQuickLook rn_fun
- ; (delta_app, inst_args, app_res_rho) <- tcInstFun do_ql True (tc_fun, fun_ctxt) fun_sigma rn_args
+ ; ((delta_app, inst_args, app_res_rho), wanted)
+ <- captureConstraints $
+ tcInstFun do_ql True fun_ctxt tc_fun fun_sigma rn_args
+ ; let ql_arg = EValArgQL { eaql_ctxt = ctxt
+ , eaql_arg_ty = sc_arg_ty
+ , eaql_larg = larg
+ , eaql_head = rn_head
+ , eaql_delta = Nothing
+ , eaql_tc_fun = tc_fun
+ , eaql_args = inst_args
+ , eaql_res_rho = app_res_rho }
; traceTc "quickLookArg 2" $
vcat [ text "arg:" <+> ppr arg
@@ -1535,19 +1575,18 @@ quickLookArg1 guarded delta larg@(L _ arg) arg_ty
-- Step 4: do quick-look unification if either (A) or (B) hold
-- NB: arg_ty may not be zonked, but that's ok
- ; let delta' = delta `unionVarSet` delta_app
- ; when can_do_ql $
- qlUnify delta' arg_ty app_res_rho
-
- ; traceTc "quickLookArg 3" $
- vcat [ text "tc_fun:" <+> ppr tc_fun
- , text "fun_sigma:" <+> ppr fun_sigma ]
-
- ; let ql_arg = ValArgQL { va_expr = larg
- , va_fun = (tc_fun, fun_ctxt)
- , va_args = inst_args
- , va_ty = app_res_rho }
- ; return (delta', ql_arg) } } }
+ ; if can_do_ql
+ then do { let delta' = delta `unionVarSet` delta_app
+ ; qlUnify delta' arg_ty app_res_rho
+ ; emitConstraints wanted
+ ; traceTc "quickLookArg unify" (ppr rn_fun <+> ppr delta')
+ ; return (delta', ql_arg) }
+
+ else -- Treat this argument independently
+ do { let ql_arg' = ql_arg { eaql_delta = Just (delta_app, wanted) }
+ ; traceTc "quickLookArg indep" (ppr rn_fun <+> ppr delta_app)
+ ; return (delta, ql_arg') }
+ }}}
anyFreeKappa :: Delta -> TcType -> TcM Bool
-- True if there is a free instantiation variable (member of Delta)
@@ -1565,8 +1604,10 @@ anyFreeKappa delta ty
| otherwise
= return False
-skipQuickLook :: Delta -> LHsExpr GhcRn -> TcM (Delta, EValArg 'TcpInst)
-skipQuickLook delta larg = return (delta, ValArg larg)
+skipQuickLook :: Delta -> AppCtxt -> LHsExpr GhcRn -> Scaled TcRhoType
+ -> TcM (Delta, HsExprArg 'TcpInst)
+skipQuickLook delta ctxt larg arg_ty
+ = return (delta, EValArg { ea_ctxt = ctxt, ea_arg = larg, ea_arg_ty = arg_ty })
----------------
quickLookResultType :: Delta -> TcRhoType -> ExpRhoType -> TcM TcRhoType
=====================================
compiler/GHC/Tc/Gen/Expr.hs
=====================================
@@ -268,7 +268,10 @@ tcMonoExprNC (L loc expr) res_ty
; return (L loc expr') }
---------------
-tcExpr :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)
+tcExpr :: HsExpr GhcRn
+ -> ExpRhoType -- DeepSubsumption <=> when checking, this type
+ -- is deeply skolemised
+ -> TcM (HsExpr GhcTc)
-- Use tcApp to typecheck applications, which are treated specially
-- by Quick Look. Specifically:
=====================================
compiler/GHC/Tc/Gen/Head.hs
=====================================
@@ -16,7 +16,7 @@
-}
module GHC.Tc.Gen.Head
- ( HsExprArg(..), EValArg(..), TcPass(..)
+ ( HsExprArg(..), TcPass(..), Delta
, AppCtxt(..), appCtxtLoc, insideExpansion
, splitHsApps, rebuildHsApps
, addArgWrap, isHsValArg
@@ -47,18 +47,19 @@ import GHC.Tc.Utils.Unify
import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_syntactic )
import GHC.Tc.Utils.Instantiate
import GHC.Tc.Instance.Family ( tcLookupDataFamInst )
-import GHC.Core.FamInstEnv ( FamInstEnvs )
-import GHC.Core.UsageEnv ( singleUsageUE )
import GHC.Tc.Errors.Types
import GHC.Tc.Solver ( InferMode(..), simplifyInfer )
import GHC.Tc.Utils.Env
import GHC.Tc.Utils.TcMType
import GHC.Tc.Types.Origin
+import GHC.Tc.Types.Constraint( WantedConstraints )
import GHC.Tc.Utils.TcType as TcType
import GHC.Tc.Types.Evidence
import GHC.Tc.Zonk.TcType
+import GHC.Core.FamInstEnv ( FamInstEnvs )
+import GHC.Core.UsageEnv ( singleUsageUE )
import GHC.Core.PatSyn( PatSyn )
import GHC.Core.ConLike( ConLike(..) )
import GHC.Core.DataCon
@@ -168,37 +169,53 @@ data TcPass = TcpRn -- Arguments decomposed
| TcpInst -- Function instantiated
| TcpTc -- Typechecked
-data HsExprArg (p :: TcPass)
- = -- See Note [HsExprArg]
- EValArg { eva_ctxt :: AppCtxt
- , eva_arg :: EValArg p
- , eva_arg_ty :: !(XEVAType p) }
+type Delta = TcTyVarSet -- Set of instantiation variables,
+ -- written \kappa in the QL paper
+ -- Just a set of ordinary unification variables,
+ -- but ones that QL may fill in with polytypes
+
+data HsExprArg (p :: TcPass) where -- See Note [HsExprArg]
+
+ -- See Note [EValArg]
+ EValArg :: { ea_ctxt :: AppCtxt
+ , ea_arg_ty :: !(XEVAType p)
+ , ea_arg :: LHsExpr (GhcPass (XPass p)) }
+ -> HsExprArg p
- | ETypeArg { eva_ctxt :: AppCtxt
- , eva_hs_ty :: LHsWcType GhcRn -- The type arg
- , eva_ty :: !(XETAType p) } -- Kind-checked type arg
+ EValArgQL :: { eaql_ctxt :: AppCtxt
+ , eaql_arg_ty :: !(XEVAType 'TcpInst) -- Type expected by function
+ , eaql_larg :: LHsExpr GhcRn -- Original application
+ -- For location and error msgs
+ , eaql_head :: (HsExpr GhcRn, AppCtxt) -- Function of the application,
+ -- typechecked, plus its context
+ , eaql_delta :: Maybe (Delta, WantedConstraints)
+ -- Nothing <=> unified with caller
+ -- Just delta <=> independent
+ , eaql_tc_fun :: HsExpr GhcTc
+ , eaql_args :: [HsExprArg 'TcpInst] -- Args, instantiated
+ , eaql_res_rho :: TcRhoType } -- Result type of the application
+ -> HsExprArg 'TcpInst -- Only exists in TcpInst phase
+
+ ETypeArg :: { ea_ctxt :: AppCtxt
+ , ea_hs_ty :: LHsWcType GhcRn -- The type arg
+ , ea_ty_arg :: !(XETAType p) } -- Kind-checked type arg
+ -> HsExprArg p
+
+ EPrag :: AppCtxt -> (HsPragE (GhcPass (XPass p))) -> HsExprArg p
+ EWrap :: EWrap -> HsExprArg p
- | EPrag AppCtxt
- (HsPragE (GhcPass (XPass p)))
+type family XETAType p where -- Type arguments
+ XETAType 'TcpRn = NoExtField
+ XETAType _ = Type
- | EWrap EWrap
+type family XEVAType p where -- Value arguments
+ XEVAType 'TcpRn = NoExtField
+ XEVAType _ = Scaled TcSigmaType
data EWrap = EPar AppCtxt
| EExpand HsThingRn
| EHsWrap HsWrapper
-data EValArg (p :: TcPass) where -- See Note [EValArg]
- ValArg :: LHsExpr (GhcPass (XPass p))
- -> EValArg p
-
- ValArgQL :: { va_expr :: LHsExpr GhcRn -- Original application
- -- For location and error msgs
- , va_fun :: (HsExpr GhcTc, AppCtxt) -- Function of the application,
- -- typechecked, plus its context
- , va_args :: [HsExprArg 'TcpInst] -- Args, instantiated
- , va_ty :: TcRhoType } -- Result type
- -> EValArg 'TcpInst -- Only exists in TcpInst phase
-
data AppCtxt
= VAExpansion
HsThingRn
@@ -254,23 +271,15 @@ type family XPass p where
XPass 'TcpInst = 'Renamed
XPass 'TcpTc = 'Typechecked
-type family XETAType p where -- Type arguments
- XETAType 'TcpRn = NoExtField
- XETAType _ = Type
-
-type family XEVAType p where -- Value arguments
- XEVAType 'TcpRn = NoExtField
- XEVAType _ = Scaled Type
-
mkEValArg :: AppCtxt -> LHsExpr GhcRn -> HsExprArg 'TcpRn
-mkEValArg ctxt e = EValArg { eva_arg = ValArg e, eva_ctxt = ctxt
- , eva_arg_ty = noExtField }
+mkEValArg ctxt e = EValArg { ea_arg = e, ea_ctxt = ctxt
+ , ea_arg_ty = noExtField }
mkETypeArg :: AppCtxt -> LHsWcType GhcRn -> HsExprArg 'TcpRn
mkETypeArg ctxt hs_ty =
- ETypeArg { eva_ctxt = ctxt
- , eva_hs_ty = hs_ty
- , eva_ty = noExtField }
+ ETypeArg { ea_ctxt = ctxt
+ , ea_hs_ty = hs_ty
+ , ea_ty_arg = noExtField }
addArgWrap :: HsWrapper -> [HsExprArg p] -> [HsExprArg p]
addArgWrap wrap args
@@ -392,9 +401,9 @@ rebuild_hs_apps :: HsExpr GhcTc
rebuild_hs_apps fun _ [] = fun
rebuild_hs_apps fun ctxt (arg : args)
= case arg of
- EValArg { eva_arg = ValArg arg, eva_ctxt = ctxt' }
+ EValArg { ea_arg = arg, ea_ctxt = ctxt' }
-> rebuild_hs_apps (HsApp noExtField lfun arg) ctxt' args
- ETypeArg { eva_hs_ty = hs_ty, eva_ty = ty, eva_ctxt = ctxt' }
+ ETypeArg { ea_hs_ty = hs_ty, ea_ty_arg = ty, ea_ctxt = ctxt' }
-> rebuild_hs_apps (HsAppType ty lfun hs_ty) ctxt' args
EPrag ctxt' p
-> rebuild_hs_apps (HsPragE noExtField p lfun) ctxt' args
@@ -736,12 +745,12 @@ isHsValArg :: HsExprArg id -> Bool
isHsValArg (EValArg {}) = True
isHsValArg _ = False
-leadingValArgs :: [HsExprArg id] -> [EValArg id]
-leadingValArgs [] = []
-leadingValArgs (arg@(EValArg {}) : args) = eva_arg arg : leadingValArgs args
-leadingValArgs (EWrap {} : args) = leadingValArgs args
-leadingValArgs (EPrag {} : args) = leadingValArgs args
-leadingValArgs (ETypeArg {} : _) = []
+leadingValArgs :: [HsExprArg 'TcpRn] -> [LHsExpr GhcRn]
+leadingValArgs [] = []
+leadingValArgs (EValArg { ea_arg = arg } : args) = arg : leadingValArgs args
+leadingValArgs (EWrap {} : args) = leadingValArgs args
+leadingValArgs (EPrag {} : args) = leadingValArgs args
+leadingValArgs (ETypeArg {} : _) = []
isValArg :: HsExprArg id -> Bool
isValArg (EValArg {}) = True
@@ -753,24 +762,22 @@ isVisibleArg (ETypeArg {}) = True
isVisibleArg _ = False
instance OutputableBndrId (XPass p) => Outputable (HsExprArg p) where
- ppr (EValArg { eva_arg = arg }) = text "EValArg" <+> ppr arg
+ ppr (EValArg { ea_arg = arg }) = text "EValArg" <+> ppr arg
ppr (EPrag _ p) = text "EPrag" <+> ppr p
- ppr (ETypeArg { eva_hs_ty = hs_ty }) = char '@' <> ppr hs_ty
+ ppr (ETypeArg { ea_hs_ty = hs_ty }) = char '@' <> ppr hs_ty
ppr (EWrap wrap) = ppr wrap
+ ppr (EValArgQL { eaql_head = fun, eaql_args = args, eaql_res_rho = ty})
+ = hang (text "EValArgQL" <+> ppr fun)
+ 2 (vcat [ ppr 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
-instance OutputableBndrId (XPass p) => Outputable (EValArg p) where
- ppr (ValArg e) = ppr e
- ppr (ValArgQL { va_fun = fun, va_args = args, va_ty = ty})
- = hang (text "ValArgQL" <+> ppr fun)
- 2 (vcat [ ppr args, text "va_ty:" <+> ppr ty ])
-
pprHsExprArgTc :: HsExprArg 'TcpInst -> SDoc
-pprHsExprArgTc (EValArg { eva_arg = tm, eva_arg_ty = ty })
+pprHsExprArgTc (EValArg { ea_arg = tm, ea_arg_ty = ty })
= text "EValArg" <+> hang (ppr tm) 2 (dcolon <+> ppr ty)
pprHsExprArgTc arg = ppr arg
@@ -1514,7 +1521,7 @@ naughtiness in both branches. c.f. GHC.Tc.TyCl.Utils.mkRecSelBinds.
* *
********************************************************************* -}
-addFunResCtxt :: HsExpr GhcRn -> [HsExprArg 'TcpRn]
+addFunResCtxt :: HsExpr GhcRn -> [HsExprArg p]
-> TcType -> ExpRhoType
-> TcM a -> TcM a
-- When we have a mis-match in the return type of a function
=====================================
compiler/GHC/Tc/Gen/Match.hs
=====================================
@@ -361,12 +361,14 @@ tcDoStmts doExpr@(DoExpr _) ss@(L l stmts) res_ty
; return (HsDo res_ty doExpr (L l stmts')) }
else do { expanded_expr <- expandDoStmts doExpr stmts
-- Do expansion on the fly
- ; mkExpandedExprTc (HsDo noExtField doExpr ss) <$> tcExpr (unLoc expanded_expr) res_ty }
+ ; mkExpandedExprTc (HsDo noExtField doExpr ss) <$>
+ tcExpr (unLoc expanded_expr) res_ty }
}
tcDoStmts mDoExpr@(MDoExpr _) ss@(L _ stmts) res_ty
= do { expanded_expr <- expandDoStmts mDoExpr stmts -- Do expansion on the fly
- ; mkExpandedExprTc (HsDo noExtField mDoExpr ss) <$> tcExpr (unLoc expanded_expr) res_ty }
+ ; mkExpandedExprTc (HsDo noExtField mDoExpr ss) <$>
+ tcExpr (unLoc expanded_expr) res_ty }
tcDoStmts MonadComp (L l stmts) res_ty
= do { stmts' <- tcStmts (HsDoStmt MonadComp) tcMcStmt stmts res_ty
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -80,7 +80,7 @@ module GHC.Tc.Utils.TcMType (
defaultTyVar, promoteMetaTyVarTo, promoteTyVarSet,
quantifyTyVars, isQuantifiableTv,
zonkAndSkolemise, skolemiseQuantifiedTyVar,
- doNotQuantifyTyVars,
+ doNotQuantifyTyVars, demoteQLDelta,
candidateQTyVarsOfType, candidateQTyVarsOfKind,
candidateQTyVarsOfTypes, candidateQTyVarsOfKinds,
@@ -2443,6 +2443,37 @@ promoteTyVarSet tvs
-- Non-determinism is OK because order of promotion doesn't matter
; return (or bools) }
+demoteDeltaTyVarTo :: TcLevel -> TcTyVar -> TcM ()
+demoteDeltaTyVarTo tclvl tv
+ | MetaTv { mtv_ref = ref, mtv_tclvl = tv_lvl } <- tcTyVarDetails tv
+ = assertPpr (tclvl `strictlyDeeperThan` tcTyVarLevel tv) (ppr tclvl <+> ppr tv) $
+ do { info <- readTcRef ref
+ ; case info of {
+ Indirect {} -> return () ;
+ Flexi ->
+ do { cloned_tv <- cloneMetaTyVar tv
+ ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
+ ; liftZonkM $ writeTcRef ref (Indirect (TyVarTy rhs_tv))
+ -- Do not go via writeMetaTyVar!
+ ; traceTc "demoteTyVar" (ppr tv <+> text "-->" <+> ppr rhs_tv)
+ ; return () } } }
+ | otherwise
+ = pprPanic "demoteDeltaTyVarTo" (ppr tv)
+
+demoteQLDelta :: TcTyVarSet -> TcM ()
+demoteQLDelta delta
+ | null tvs
+ = return ()
+ | otherwise
+ = do { tclvl <- getTcLevel
+ ; assertPpr (isMetaTyVar tv1) (ppr delta) $
+ when (tclvl `strictlyDeeperThan` tcTyVarLevel tv1) $
+ mapM_ (demoteDeltaTyVarTo tclvl) tvs }
+ where
+ tv1 = head tvs
+ tvs = nonDetEltsUniqSet delta
+ -- Non-determinism is OK because order of promotion doesn't matter
+
{-
%************************************************************************
%* *
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -1332,15 +1332,17 @@ tcSubType orig ctxt ty_actual ty_expected
---------------
tcSubTypeDS :: HsExpr GhcRn
- -> TcRhoType -- Actual -- a rho-type not a sigma-type
- -> ExpRhoType -- Expected
+ -> TcRhoType -- Actual type -- a rho-type not a sigma-type
+ -> ExpRhoType -- Expected type
+ -- DeepSubsumption <=> when checking, this type
+ -- is deeply skolemised
-> TcM HsWrapper
-- Similar signature to unifyExpectedType; does deep subsumption
-- Only one call site, in GHC.Tc.Gen.App.tcApp
tcSubTypeDS rn_expr act_rho res_ty
= case res_ty of
- Check exp_rho -> tc_sub_type_ds Deep (unifyType m_thing) orig
- GenSigCtxt act_rho exp_rho
+ Check exp_rho -> tc_sub_type_deep (unifyType m_thing) orig
+ GenSigCtxt act_rho exp_rho
Infer inf_res -> do { co <- fillInferResult act_rho inf_res
; return (mkWpCastN co) }
@@ -1485,18 +1487,24 @@ tc_sub_type_ds ds_flag unify inst_orig ctxt ty_actual ty_expected
, text "ty_expected =" <+> ppr ty_expected ]
; (sk_wrap, inner_wrap)
- <- case ds_flag of
- Shallow -> -- Shallow: skolemise, instantiate and unify
- tcSkolemise Shallow ctxt ty_expected $ \sk_rho ->
- do { (wrap, rho_a) <- topInstantiate inst_orig ty_actual
- ; cow <- unify rho_a sk_rho
- ; return (mkWpCastN cow <.> wrap) }
- Deep -> -- Deep: we have co/contra work to do
- tcSkolemise Deep ctxt ty_expected $ \sk_rho ->
- tc_sub_type_deep unify inst_orig ctxt ty_actual sk_rho
+ <- tcSkolemise ds_flag ctxt ty_expected $ \sk_rho ->
+ case ds_flag of
+ Deep -> tc_sub_type_deep unify inst_orig ctxt ty_actual sk_rho
+ Shallow -> tc_sub_type_shallow unify inst_orig ty_actual sk_rho
; return (sk_wrap <.> inner_wrap) }
+----------------------
+tc_sub_type_shallow :: (TcType -> TcType -> TcM TcCoercionN)
+ -> CtOrigin
+ -> TcSigmaType
+ -> TcRhoType -- Skolemised (shallow-ly)
+ -> TcM HsWrapper
+tc_sub_type_shallow unify inst_orig ty_actual sk_rho
+ = do { (wrap, rho_a) <- topInstantiate inst_orig ty_actual
+ ; cow <- unify rho_a sk_rho
+ ; return (mkWpCastN cow <.> wrap) }
+
----------------------
definitely_mono :: DeepSubsumptionFlag -> TcType -> Bool
definitely_mono ds_flag ty
@@ -1734,7 +1742,8 @@ tc_sub_type_deep :: (TcType -> TcType -> TcM TcCoercionN) -- How to unify
-- Precondition: ty_expected is deeply skolemised
tc_sub_type_deep unify inst_orig ctxt ty_actual ty_expected
- = do { traceTc "tc_sub_type_deep" $
+ = assertPpr (isDeepRhoTy ty_expected) (ppr ty_expected) $
+ do { traceTc "tc_sub_type_deep" $
vcat [ text "ty_actual =" <+> ppr ty_actual
, text "ty_expected =" <+> ppr ty_expected ]
; go ty_actual ty_expected }
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/18712afb58bb9eb6da2f429253c1c0fa99181ea2
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/18712afb58bb9eb6da2f429253c1c0fa99181ea2
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/0a36ba0d/attachment-0001.html>
More information about the ghc-commits
mailing list