[Git][ghc/ghc][wip/T24676] Fix a QuickLook bug
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Fri Apr 26 06:10:12 UTC 2024
Simon Peyton Jones pushed to branch wip/T24676 at Glasgow Haskell Compiler / GHC
Commits:
3b28a6c9 by Simon Peyton Jones at 2024-04-26T08:15:43+02:00
Fix a QuickLook bug
This MR fixes the bug exposed by #24676. The problem was that
quickLookArg was trying to avoid calling tcInstFun unnecessarily; but
it was in fact necessary. But that in turn forced me into a
significant refactoring, putting more fields into EValArgQL.
I added a lot of new material to
Note [Quick Look at value arguments]
It is a bit more subtle than I would like, but the overall plan
is rather clearer now than it was.
- - - - -
10 changed files:
- compiler/GHC/Core/TyCo/FVs.hs
- 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
- + testsuite/tests/impredicative/T24676.hs
- testsuite/tests/impredicative/all.T
- testsuite/tests/typecheck/should_fail/T2846b.stderr
Changes:
=====================================
compiler/GHC/Core/TyCo/FVs.hs
=====================================
@@ -29,6 +29,7 @@ module GHC.Core.TyCo.FVs
-- Any and No Free vars
anyFreeVarsOfType, anyFreeVarsOfTypes, anyFreeVarsOfCo,
noFreeVarsOfType, noFreeVarsOfTypes, noFreeVarsOfCo,
+ anyFreeVarsOfTypeM,
-- * Free type constructors
tyConsOfType, tyConsOfTypes,
@@ -58,7 +59,7 @@ import {-# SOURCE #-} GHC.Core.Coercion( coercionLKind )
import GHC.Builtin.Types.Prim( funTyFlagTyCon )
-import Data.Monoid as DM ( Endo(..), Any(..) )
+import Data.Monoid as DM ( Any(..) )
import GHC.Core.TyCo.Rep
import GHC.Core.TyCon
import GHC.Core.Coercion.Axiom( coAxiomTyCon )
@@ -74,6 +75,8 @@ import GHC.Utils.Misc
import GHC.Utils.Panic
import GHC.Data.Pair
+import Data.Semigroup
+
{-
%************************************************************************
%* *
@@ -974,6 +977,36 @@ noFreeVarsOfCo co = not $ DM.getAny (f co)
where (_, _, f, _) = foldTyCo (afvFolder (const True)) emptyVarSet
+{- *********************************************************************
+* *
+ Folding over free vars
+* *
+********************************************************************* -}
+
+newtype AnyM m = AM { unAnyM :: m Bool }
+
+instance Monad m => Semigroup (AnyM m) where
+ AM ml <> AM mr = AM (do { l <- ml; if l then return True else mr })
+
+instance Monad m => Monoid (AnyM m) where
+ mempty = AM (return False)
+
+{-# INLINE afvFolderM #-} -- so that specialization to (const True) works
+afvFolderM :: Monad m => (TyCoVar -> m Bool) -> TyCoFolder TyCoVarSet (AnyM m)
+afvFolderM check_fv = TyCoFolder { tcf_view = noView
+ , tcf_tyvar = do_tv, tcf_covar = mempty
+ , tcf_hole = mempty, tcf_tycobinder = do_bndr }
+ where
+ do_bndr is tcv _ = extendVarSet is tcv
+ do_tv is tv | tv `elemVarSet` is = AM (return False)
+ | otherwise = AM (check_fv tv)
+
+anyFreeVarsOfTypeM :: Monad m => (TyCoVar -> m Bool) -> Type -> m Bool
+-- Returns True if check_fv returns True of any free var of the type
+anyFreeVarsOfTypeM check_fv ty = unAnyM (f ty)
+ where (f, _, _, _) = foldTyCo (afvFolderM check_fv) emptyVarSet
+
+
{- *********************************************************************
* *
scopedSort
=====================================
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,9 @@ The latter is much better. That is why we call unifyExpectedType
before tcValArgs.
-}
-tcApp :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)
+tcApp :: HsExpr GhcRn
+ -> ExpRhoType -- When checking, -XDeepSubsumption <=> 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,40 +335,39 @@ 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]
+ -> 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 { ds_flag <- getDeepSubsumptionFlag
+
-- 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
+ 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.
@@ -387,11 +388,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 +399,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 +440,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 +452,93 @@ 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_status = ql_status
+ , eaql_ctxt = ctxt
+ , eaql_arg_ty = Scaled mult arg_ty
+ , eaql_larg = larg@(L arg_loc rn_expr)
+ , eaql_head = rn_head
+ , 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
+ do { -- Expose QL results
+ arg_ty <- liftZonkM $ zonkQuickLook do_ql arg_ty
+
+ ; traceTc "tcEValArgQL {" (vcat [ ppr rn_head
+ , text "status:" <+> ppr ql_status
+ , text "res_rho:" <+> ppr res_rho
+ , text "arg_ty:" <+> ppr arg_ty
+ , text "args:" <+> ppr inst_args ])
+
+ ; ds_flag <- getDeepSubsumptionFlag
+ ; (wrap, arg')
+ <- tcScalingUsage mult $
+ tcSkolemise ds_flag GenSigCtxt arg_ty $ \ arg_rho ->
+ -- Tricky point: with deep subsumption, even if ql_status=QLUnified
+ -- arg_ty will be a rho-type (no top-level foralls), but it may have
+ -- /nested/ foralls; so if -XDeepSubsumption is on 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 { resume_ql_arg ql_status arg_rho
+ ; finishApp do_ql rn_expr rn_head tc_fun inst_args res_rho
+ (Check arg_rho) }
- ; co <- unifyType Nothing app_res_rho exp_arg_sigma
- ; arg' <- mkHsWrapCo co <$> rebuildHsApps inner_fun fun_ctxt tc_args app_res_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 (mkHsWrap wrap arg')
+ , ea_arg_ty = Scaled mult arg_ty }) }
+ where
+ resume_ql_arg QLUnified _
+ = return ()
+ resume_ql_arg (QLIndependent delta wc) arg_rho
+ = -- A tricky function!
+ -- See Note [Quick Look at value arguments] wrinkle (QLA4)
+ do { unless (isEmptyVarSet delta) $ -- Optimisation only
+ do { demoteQLDelta delta
+ ; qlUnify delta arg_rho res_rho }
+ ; emitConstraints wc }
{- *********************************************************************
* *
@@ -503,11 +546,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,17 +555,18 @@ 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]
-> TcM ( Delta
, [HsExprArg 'TcpInst]
, TcSigmaType )
--- This function implements the |-inst judgement in Fig 4, plus the
+-- This crucial 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 +574,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 +675,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 +696,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 +730,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 +756,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 +774,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 +793,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`.
@@ -1440,109 +1474,233 @@ need to zonk `body` before performing the substitution above. See test case
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The function quickLookArg implements the "QL argument" judgement of
the QL paper, in Fig 5 of "A quick look at impredicativity" (ICFP 2020),
-rather directly.
+rather directly. The key rule, implemented by `quickLookArg` is
-Wrinkles:
+ G |-h h:sg -- Find the type of the head
+ G |-inst sg;pis ~> phis;rho_r -- tcInstFun on the args
+ (A) rho = T sgs OR (B) fiv(phis) = emptyset -- can_do_ql
+ -------------------------------------- APP-QL
+ G |-ql h pis : rho ~> qlUnify( rho, rho_r )
-* We avoid zonking, so quickLookArg thereby sees the argument type /before/
- the QL substitution Theta is applied to it. So we achieve argument-order
- independence for free (see 5.7 in the paper).
+(The paper uses a lightning-bolt where we use "ql".) The most straightforward
+way to implement this rule for a call (f e1 ... en) would be:
+
+ 1. Take a quick look at the argumets e1..en to guide instantiation
+ of the function f.
+ 2. Then typecheck e1..en from scratch.
+
+That's wasteful, because in Step 1, the quick look at each argument, say (g
+h1..hm), involves instantiating `h` and taking a quick look at /its/
+arguments. Then in Step 2 we typecheck (g h1..hm) and again take a quick look
+at its arguments. This is quadratic in the nesting depth of the arguments.
+
+Instead, after the quick look, we /save/ the work we have done in an EValArgQL
+record, and /resume/ it later. The way to think of it is this:
+
+ * `tcApp` typechecks an application. It is strutured into two:
+ - the "initial" part, especially `tcInstFun`
+ - the "finish" part, `finishApp`, which completes the job
-* When we quick-look at an argument, we save the work done, by returning
- an EValArg with a ValArgQL inside it. (It started life with a ValArg
- inside.) The ValArgQL remembers all the work that QL did (notably,
- decomposing the argument and instantiating) so that tcValArgs does
- not need to repeat it. Rather neat, and remarkably easy.
+ * quickLookArg (which takes a quick look at the argument)
+
+ - Does the "initial" part of `tcApp`, especially `tcInstFun`
+
+ - Captures the result in an EValArgQL record
+
+ - Later, `tcValArg` starts from the EValArgQL record, and
+ completes the job of tpyechecking the appication by calling
+ `finishApp`
+
+This turned out to be more subtle than I expected. Wrinkles:
+
+(QLA1) We avoid zonking, so quickLookArg thereby sees the argument type /before/
+ the QL substitution Theta is applied to it. So we achieve argument-order
+ independence for free (see 5.7 in the paper). See the `guarded` predictate
+ in `quickLookArg`.
+
+(QLA2) `quickLookArg` decides whether or not premises (A) and (B) of the
+ quick-look-arg jugement APP-QL are satisfied; this is captured in `can_do_ql`:
+
+ - can_do_ql=True:
+ get info from argument by unifying the argument result type with
+ the type expected by the caller, using `qlUnify` in `quickLookResultType`
+ Capture the work done in EValArgQL with eaql_status = QLUnified.
+
+ - can_do_ql=False:
+ do not get info from argument; no `qlUnify`. Instead just save the
+ work done in EValArgQL, with eaql_status = QLIndependent.
+
+(QLA3) Deciding whether the premises are satisfied involves calling `tcInstFun`
+ (which takes quite some work becuase it calls quickLookArg on nested calls).
+ That's why we want to capture the work done, in EValArgQL.
+
+ Do we really have to call `tcInstFun` before deciding `can_do_ql`? Yes.
+ Suppose ids :: [forall a. a->a], and consider
+ (:) (reverse ids) blah
+ `tcApp` on the outer call will instantiate (:) with `kappa`, and take a
+ quick look at (reverse ids). Only after instantiating `reverse` with kappa2,
+ quick-looking at `ids` can we discover that (kappa2:=forall a. a->a), which
+ satisfies premise (B) of can_do_ql.
+
+(QLA4) When we resume typechecking an argument, in `tcValArg`, it's fairly
+ easy if eaql_status=QLUnified (see (QLA2)). But for QLIndependent things
+ are a bit tricky; see function `resume_ql-arg`:
+
+ - quickLookArg has not yet done `qlUnify` with the calling context. We
+ must do so now. Example: choose [] ids,
+ where ids :: [forall a. a->a]
+ choose :: a -> a -> a
+ We instantiate choose with `kappa` and discover from `ids` that
+ (kappa = [forall a. a->a]). Now we resume typechecking argument [], and
+ we must take advantage of what we have now discovered about `kappa`,
+ to typecheck [] :: [forall a. a->a]
+
+ - Calling `tcInstFun` on the argument may have emitted some constraints, which
+ we carefully captured in `quickLookArg` and stored in the EValArgQL. We must
+ now emit them with `emitConstraints`
+
+ - When we quick-looked at the argument we instantiated with say kappa2. But
+ the /level-number/ on kappa2 will be from the original `tcApp`, whereas
+ we may now be more deeply nested; see the `tcSkolemise` in `tcValArg` for
+ EValArgQL. We carefully kept those kappas, and we now /demote/ them to the
+ ambient level with `demoteQLDelta`.
+
+ The demotion seems right butis not very beautiful; e.g. `demoteDeltaTyVarTo`
+ deliberately disobeys a sanity check otherwise enforced by writeMetaTyVar.
-}
-----------------
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, so 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
-
- -- 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 }
-
- | otherwise
- = quickLookArg1 guarded delta larg arg_ty
-
-isGuardedTy :: TcType -> Bool
-isGuardedTy ty
+ -- unzonked arg_ty (before calling `go`), so that we deliberately do
+ -- not exploit guardedness that emerges a result of QL on earlier args
+
+ 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 (Scaled mult arg_ty'')
+ Flexi -> quickLookArg1 guarded delta ctxt larg sc_arg_ty }
+
+ | otherwise
+ = quickLookArg1 guarded delta ctxt larg sc_arg_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 guarded delta larg@(L _ arg) arg_ty
- = do { ((rn_fun, fun_ctxt), rn_args) <- splitHsApps arg
+quickLookArg1 :: Bool -- Guarded
+ -> Delta -- Always non-empty
+ -> AppCtxt -> LHsExpr GhcRn
+ -> 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)
+ = 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
; traceTc "quickLookArg 1" $
vcat [ text "arg:" <+> ppr arg
+ , text "arg_ty:" <+> ppr arg_ty
, text "head:" <+> ppr rn_fun <+> dcolon <+> ppr mb_fun_ty
, text "args:" <+> ppr rn_args ]
; case mb_fun_ty of {
- Nothing -> -- fun is too complicated
- skipQuickLook delta larg ;
+ Nothing -> skipQuickLook delta ctxt larg sc_arg_ty ; -- fun is too complicated
Just (tc_fun, fun_sigma) ->
- do { let no_free_kappas = findNoQuantVars fun_sigma rn_args
- ; traceTc "quickLookArg 2" $
- vcat [ text "no_free_kappas:" <+> ppr no_free_kappas
- , text "guarded:" <+> ppr guarded
- , text "tc_fun:" <+> ppr tc_fun
- , text "fun_sigma:" <+> ppr fun_sigma ]
- ; if not (guarded || no_free_kappas)
- then skipQuickLook delta larg
- else
+ -- 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
- ; traceTc "quickLookArg 3" $
+ ; ((delta_app, inst_args, app_res_rho), wanted)
+ <- captureConstraints $
+ tcInstFun do_ql True fun_ctxt tc_fun fun_sigma rn_args
+
+ ; let -- mk_ql_arg captures the results so far, for resumption in tcValArg
+ mk_ql_arg status
+ = EValArgQL { eaql_status = status
+ , eaql_ctxt = ctxt
+ , eaql_arg_ty = sc_arg_ty
+ , eaql_larg = larg
+ , eaql_head = rn_head
+ , eaql_tc_fun = tc_fun
+ , eaql_args = inst_args
+ , eaql_res_rho = app_res_rho }
+
+ ; traceTc "quickLookArg 2" $
vcat [ text "arg:" <+> ppr arg
, text "delta:" <+> ppr delta
, text "delta_app:" <+> ppr delta_app
, text "arg_ty:" <+> ppr arg_ty
, text "app_res_rho:" <+> ppr app_res_rho ]
- -- Do quick-look unification
- -- NB: arg_ty may not be zonked, but that's ok
- ; let delta' = delta `unionVarSet` delta_app
- ; qlUnify delta' arg_ty app_res_rho
-
- ; 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) } } } }
+ -- Step 3: check the two other premises of APP-lightning-bolt (Fig 5 in the paper)
+ -- Namely: (A) is rho guarded, and (B) fiv(rho_r) = emptyset
+ ; can_do_ql <- if guarded -- (A)
+ then return True
+ else not <$> anyFreeKappa delta_app app_res_rho -- (B)
+ -- For (B) see Note [The fiv test in quickLookArg]
-skipQuickLook :: Delta -> LHsExpr GhcRn -> TcM (Delta, EValArg 'TcpInst)
-skipQuickLook delta larg = return (delta, ValArg larg)
+ -- Step 4: do quick-look unification if either (A) or (B) hold
+ -- NB: arg_ty may not be zonked, but that's ok
+ ; if can_do_ql
+ then -- No generalisation will take place for this argument
+ -- So we can emit the constraints right now, and join its
+ -- instantiation variables (delta_app) with those of the caller (delta)
+ 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', mk_ql_arg QLUnified) }
+
+ else -- Treat this argument independently
+ -- Capture delta and wanted in QLIndependent for later resumption
+ do { traceTc "quickLookArg indep" (ppr rn_fun <+> ppr delta_app)
+ ; return (delta, mk_ql_arg (QLIndependent delta_app wanted)) }
+ }}}
+
+anyFreeKappa :: Delta -> TcType -> TcM Bool
+-- True if there is a free instantiation variable (member of Delta)
+-- in the argument type, after zonking
+-- See Note [The fiv test in quickLookArg]
+anyFreeKappa delta ty
+ = anyFreeVarsOfTypeM is_free_kappa ty
+ where
+ is_free_kappa :: TcTyVar -> TcM Bool
+ is_free_kappa tv | tv `elemVarSet` delta
+ = do { info <- readMetaTyVar tv
+ ; case info of
+ Indirect ty -> anyFreeKappa delta ty
+ Flexi -> return True }
+ | otherwise
+ = return False
+
+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
@@ -1553,7 +1711,7 @@ quickLookResultType :: Delta -> TcRhoType -> ExpRhoType -> TcM TcRhoType
quickLookResultType delta app_res_rho (Check exp_rho)
= -- In checking mode only, do qlUnify with the expected result type
- do { unless (isEmptyVarSet delta) $ -- Optimisation only
+ do { unless (isEmptyVarSet delta) $ -- Optimisation only
qlUnify delta app_res_rho exp_rho
; return app_res_rho }
@@ -1568,11 +1726,28 @@ quickLookResultType _ app_res_rho (Infer {})
-- generator. The safe thing to do is to zonk any instantiation
-- variables away. See Note [Instantiation variables are short lived]
+{- Note [The fiv test in quickLookArg]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In rule APP-lightning-bolt in Fig 5 of the paper, we have to test rho_r
+for having no free instantiation variables. We do this in Step 3 of quickLookArg1,
+using anyFreeKappa. Example:
+ Suppose ids :: [forall a. a->a]
+ and consider Just (ids++ids)
+We will instantiate Just with kappa, say, and then call
+ quickLookArg1 False {kappa} (ids ++ ids) kappa
+The call to tcInstFun will return with app_res_rho = [forall a. a->a]
+which has no free instantiation variables, so we can QL-unify
+ kappa ~ [Forall a. a->a]
+-}
+
---------------------
qlUnify :: Delta -> TcType -> TcType -> TcM ()
-- Unify ty1 with ty2, unifying only variables in delta
qlUnify delta ty1 ty2
- = do { traceTc "qlUnify" (ppr delta $$ ppr ty1 $$ ppr ty2)
+ = assertPpr (not (isEmptyVarSet delta)) (ppr delta $$ ppr ty1 $$ ppr ty2) $
+ -- Only called with a non-empty delta
+ -- Empty <=> nothing to do
+ do { traceTc "qlUnify" (ppr delta $$ ppr ty1 $$ ppr ty2)
; go (emptyVarSet,emptyVarSet) ty1 ty2 }
where
go :: (TyVarSet, TcTyVarSet)
@@ -1709,54 +1884,6 @@ That is the entire point of qlUnify! Wrinkles:
TL;DR Calling unifyKind seems like the lesser evil.
-}
-{- *********************************************************************
-* *
- Guardedness
-* *
-********************************************************************* -}
-
-findNoQuantVars :: TcSigmaType -> [HsExprArg 'TcpRn] -> Bool
--- True <=> there are no free quantified variables
--- in the result of the call
--- E.g. in the call (f e1 e2), if
--- f :: forall a b. a -> b -> Int return True
--- f :: forall a b. a -> b -> b return False (b is free)
-findNoQuantVars fun_ty args
- = go emptyVarSet fun_ty args
- where
- need_instantiation [] = True
- need_instantiation (EValArg {} : _) = True
- need_instantiation _ = False
-
- go :: TyVarSet -> TcSigmaType -> [HsExprArg 'TcpRn] -> Bool
- go bvs fun_ty args
- | need_instantiation args
- , (tvs, theta, rho) <- tcSplitSigmaTy fun_ty
- , not (null tvs && null theta)
- = go (bvs `extendVarSetList` tvs) rho args
-
- go bvs fun_ty [] = tyCoVarsOfType fun_ty `disjointVarSet` bvs
-
- go bvs fun_ty (EWrap {} : args) = go bvs fun_ty args
- go bvs fun_ty (EPrag {} : args) = go bvs fun_ty args
-
- go bvs fun_ty args@(ETypeArg {} : rest_args)
- | (tvs, body1) <- tcSplitSomeForAllTyVars (== Inferred) fun_ty
- , (theta, body2) <- tcSplitPhiTy body1
- , not (null tvs && null theta)
- = go (bvs `extendVarSetList` tvs) body2 args
- | Just (_tv, res_ty) <- tcSplitForAllTyVarBinder_maybe fun_ty
- = go bvs res_ty rest_args
- | otherwise
- = False -- E.g. head ids @Int
-
- go bvs fun_ty (EValArg {} : rest_args)
- | Just (_, res_ty) <- tcSplitFunTy_maybe fun_ty
- = go bvs res_ty rest_args
- | otherwise
- = False -- E.g. head id 'x'
-
-
{- *********************************************************************
* *
tagToEnum#
=====================================
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, QLArgStatus(..)
, 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,55 @@ 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
+
+ EValArgQL :: { eaql_status :: QLArgStatus
+ , 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_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 { eva_ctxt :: AppCtxt
- , eva_hs_ty :: LHsWcType GhcRn -- The type arg
- , eva_ty :: !(XETAType p) } -- Kind-checked type arg
+ 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)))
+ EPrag :: AppCtxt -> (HsPragE (GhcPass (XPass p))) -> HsExprArg p
+ EWrap :: EWrap -> HsExprArg p
- | EWrap EWrap
+type family XETAType p where -- Type arguments
+ XETAType 'TcpRn = NoExtField
+ XETAType _ = Type
+
+type family XEVAType p where -- Value arguments
+ XEVAType 'TcpRn = NoExtField
+ XEVAType _ = Scaled TcSigmaType
+
+data QLArgStatus -- See (QLA2) in Note [Quick Look at value arguments] in GHC.Tc.Gen.App
+ = QLUnified -- Unified with caller
+ | QLIndependent Delta WantedConstraints -- Independent of caller
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 +273,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 +403,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 +747,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 +764,25 @@ 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 QLArgStatus where
+ ppr QLUnified = text "QLUnified"
+ ppr (QLIndependent delta wc) = text "QLIndependent" <> braces (sep [ppr delta, ppr wc])
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 +1526,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,40 @@ promoteTyVarSet tvs
-- Non-determinism is OK because order of promotion doesn't matter
; return (or bools) }
+demoteDeltaTyVarTo :: TcLevel -> TcTyVar -> TcM ()
+demoteDeltaTyVarTo new_lvl tv
+ | MetaTv { mtv_ref = ref, mtv_tclvl = tv_lvl } <- tcTyVarDetails tv
+ = assertPpr (new_lvl `strictlyDeeperThan` tv_lvl) (ppr new_lvl <+> ppr tv) $
+ do { info <- readTcRef ref
+ ; case info of {
+ Indirect {} -> return () ;
+ Flexi ->
+ do { cloned_tv <- cloneMetaTyVar tv
+ ; let rhs_tv = setMetaTyVarTcLevel cloned_tv new_lvl
+ ; liftZonkM $ writeTcRef ref (Indirect (TyVarTy rhs_tv))
+ -- Do not go via writeMetaTyVar! In debug-mode it makes sanity check
+ -- on level numbers which /demoting/ deliberately disobeys
+ ; traceTc "demoteTyVar" (ppr tv <+> text "-->" <+> ppr rhs_tv)
+ ; return () } } }
+ | otherwise
+ = pprPanic "demoteDeltaTyVarTo" (ppr tv)
+
+demoteQLDelta :: TcTyVarSet -> TcM ()
+-- See Note [Quick Look at value arguments] wrinkle (QLA4)
+-- in GHC.Tc.Gen.App
+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
=====================================
@@ -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 []
@@ -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) }
@@ -1472,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 ]
@@ -1485,25 +1487,25 @@ 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) }
----------------------
-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 (=>)
+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_poly :: TcType -> Bool
-- A very conservative test:
-- see Note [Don't skolemise unnecessarily]
@@ -1721,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
@@ -1734,7 +1737,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 }
@@ -1877,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 (=>)
+
{-
************************************************************************
* *
=====================================
testsuite/tests/impredicative/T24676.hs
=====================================
@@ -0,0 +1,30 @@
+{-# LANGUAGE ImpredicativeTypes #-}
+
+module T24676 where
+
+ids :: [forall a. a -> a]
+ids = take 5 (repeat id)
+-- take :: Int -> [a] -> [a]
+-- repeat :: b -> [b]
+
+test :: [forall a. a->a]
+test = ids ++ ids
+
+-- typechecks with signature, without signature, and inlining "test"
+f1a = test
+
+f1b :: [forall a. a -> a]
+f1b = test
+
+-- typechecks with or without signature
+f2a = Just test
+
+f2b :: Maybe [forall a. a->a]
+f2b = Just test
+
+-- only typechecks with a signature
+
+f3a = Just (ids ++ ids)
+
+f3b :: Maybe [forall a. a -> a]
+f3b = Just (ids ++ ids)
=====================================
testsuite/tests/impredicative/all.T
=====================================
@@ -21,3 +21,4 @@ test('T8808', normal, compile, [''])
test('T17332', normal, compile_fail, [''])
test('expr-sig', normal, compile, [''])
test('Dict', normal, compile, [''])
+test('T24676', normal, compile, [''])
=====================================
testsuite/tests/typecheck/should_fail/T2846b.stderr
=====================================
@@ -1,5 +1,5 @@
-T2846b.hs:5:11: error: [GHC-91028]
+T2846b.hs:5:10: error: [GHC-91028]
• Couldn't match expected type ‘a1’
with actual type ‘[Num a0 => a0]’
Cannot instantiate unification variable ‘a1’
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/3b28a6c93502a3c8bad8329791a494434bfe8604
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/3b28a6c93502a3c8bad8329791a494434bfe8604
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/20240426/97daa833/attachment-0001.html>
More information about the ghc-commits
mailing list