[Git][ghc/ghc][wip/T26331] Fix deep subsumption again

Simon Peyton Jones pushed to branch wip/T26331 at Glasgow Haskell Compiler / GHC Commits: 299b483c by Simon Peyton Jones at 2025-08-28T10:56:11+01:00 Fix deep subsumption again This commit fixed #26255: commit 56b32c5a2d5d7cad89a12f4d74dc940e086069d1 Author: sheaf Date: Mon Aug 11 15:50:47 2025 +0200 Improve deep subsumption This commit improves the DeepSubsumption sub-typing implementation in GHC.Tc.Utils.Unify.tc_sub_type_deep by being less eager to fall back to unification. But alas it still wasn't quite right for view patterns: #26331 This MR does a generalisation to fix it. A bit of a sledgehammer to crack a nut, but nice. * Add a field `ir_inst :: InferInstFlag` to `InferResult`, where ``` data InferInstFlag = IIF_Sigma | IIF_ShallowRho | IIF_DeepRho ``` * The flag says exactly how much `fillInferResult` should instantiate before filling the hole. * We can also use this to replace the previous very ad-hoc `tcInferSigma` that was used to implement GHCi's `:type` command. - - - - - 15 changed files: - compiler/GHC/Tc/Gen/App.hs - compiler/GHC/Tc/Gen/Bind.hs - compiler/GHC/Tc/Gen/Expr.hs - compiler/GHC/Tc/Gen/Expr.hs-boot - compiler/GHC/Tc/Gen/Head.hs - compiler/GHC/Tc/Gen/HsType.hs - compiler/GHC/Tc/Gen/Match.hs - compiler/GHC/Tc/Gen/Pat.hs - compiler/GHC/Tc/Module.hs - compiler/GHC/Tc/Utils/TcMType.hs - compiler/GHC/Tc/Utils/TcType.hs - compiler/GHC/Tc/Utils/Unify.hs - + testsuite/tests/patsyn/should_compile/T26331.hs - + testsuite/tests/patsyn/should_compile/T26331a.hs - testsuite/tests/patsyn/should_compile/all.T Changes: ===================================== compiler/GHC/Tc/Gen/App.hs ===================================== @@ -16,7 +16,6 @@ module GHC.Tc.Gen.App ( tcApp - , tcInferSigma , tcExprPrag ) where import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcPolyExpr ) @@ -165,26 +164,6 @@ Note [Instantiation variables are short lived] -} -{- ********************************************************************* -* * - tcInferSigma -* * -********************************************************************* -} - -tcInferSigma :: Bool -> LHsExpr GhcRn -> TcM TcSigmaType --- Used only to implement :type; see GHC.Tc.Module.tcRnExpr --- True <=> instantiate -- return a rho-type --- False <=> don't instantiate -- return a sigma-type -tcInferSigma inst (L loc rn_expr) - = addExprCtxt rn_expr $ - setSrcSpanA loc $ - do { (fun@(rn_fun,fun_ctxt), rn_args) <- splitHsApps rn_expr - ; do_ql <- wantQuickLook rn_fun - ; (tc_fun, fun_sigma) <- tcInferAppHead fun - ; (inst_args, app_res_sigma) <- tcInstFun do_ql inst (tc_fun, fun_ctxt) fun_sigma rn_args - ; _ <- tcValArgs do_ql inst_args - ; return app_res_sigma } - {- ********************************************************************* * * Typechecking n-ary applications @@ -219,7 +198,7 @@ using the application chain route, and we can just recurse to tcExpr. A "head" has three special cases (for which we can infer a polytype using tcInferAppHead_maybe); otherwise is just any old expression (for -which we can infer a rho-type (via tcInfer). +which we can infer a rho-type (via runInferExpr). There is no special treatment for HsHole (HsVar ...), HsOverLit, etc, because we can't get a polytype from them. @@ -403,13 +382,22 @@ tcApp rn_expr exp_res_ty -- Step 2: Infer the type of `fun`, the head of the application ; (tc_fun, fun_sigma) <- tcInferAppHead fun ; let tc_head = (tc_fun, fun_ctxt) + -- inst_final: top-instantiate the result type of the application, + -- EXCEPT if we are trying to infer a sigma-type + inst_final = case exp_res_ty of + Check {} -> True + Infer (IR {ir_inst=iif}) -> + case iif of + IIF_ShallowRho -> True + IIF_DeepRho -> True + IIF_Sigma -> False -- Step 3: Instantiate the function type (taking a quick look at args) ; do_ql <- wantQuickLook rn_fun ; (inst_args, app_res_rho) <- setQLInstLevel do_ql $ -- See (TCAPP1) and (TCAPP2) in -- Note [tcApp: typechecking applications] - tcInstFun do_ql True tc_head fun_sigma rn_args + tcInstFun do_ql inst_final tc_head fun_sigma rn_args ; case do_ql of NoQL -> do { traceTc "tcApp:NoQL" (ppr rn_fun $$ ppr app_res_rho) @@ -420,6 +408,7 @@ tcApp rn_expr exp_res_ty app_res_rho exp_res_ty -- Step 4.2: typecheck the arguments ; tc_args <- tcValArgs NoQL inst_args + -- Step 4.3: wrap up ; finishApp tc_head tc_args app_res_rho res_wrap } @@ -427,15 +416,18 @@ tcApp rn_expr exp_res_ty -- Step 5.1: Take a quick look at the result type ; quickLookResultType app_res_rho exp_res_ty + -- Step 5.2: typecheck the arguments, and monomorphise -- any un-unified instantiation variables ; tc_args <- tcValArgs DoQL inst_args + -- Step 5.3: zonk to expose the polymophism hidden under -- QuickLook instantiation variables in `app_res_rho` ; app_res_rho <- liftZonkM $ zonkTcType app_res_rho + -- Step 5.4: subsumption check against the expected type ; res_wrap <- checkResultTy rn_expr tc_head inst_args - app_res_rho exp_res_ty + app_res_rho exp_res_ty -- Step 5.5: wrap up ; finishApp tc_head tc_args app_res_rho res_wrap } } @@ -470,32 +462,12 @@ checkResultTy :: HsExpr GhcRn -> (HsExpr GhcTc, AppCtxt) -- Head -> [HsExprArg p] -- Arguments, just error messages -> TcRhoType -- Inferred type of the application; zonked to - -- expose foralls, but maybe not deeply instantiated + -- expose foralls, but maybe not /deeply/ instantiated -> ExpRhoType -- Expected type; this is deeply skolemised -> TcM HsWrapper checkResultTy rn_expr _fun _inst_args app_res_rho (Infer inf_res) - = fillInferResultDS (exprCtOrigin rn_expr) app_res_rho inf_res - -- See Note [Deeply instantiate in checkResultTy when inferring] - -{- Note [Deeply instantiate in checkResultTy when inferring] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -To accept the following program (T26225b) with -XDeepSubsumption, we need to -deeply instantiate when inferring in checkResultTy: - - f :: Int -> (forall a. a->a) - g :: Int -> Bool -> Bool - - test b = - case b of - True -> f - False -> g - -If we don't deeply instantiate in the branches of the case expression, we will -try to unify the type of 'f' with that of 'g', which fails. If we instead -deeply instantiate 'f', we will fill the 'InferResult' with 'Int -> alpha -> alpha' -which then successfully unifies with the type of 'g' when we come to fill the -'InferResult' hole a second time for the second case branch. --} + = fillInferResult (exprCtOrigin rn_expr) app_res_rho inf_res + -- fillInferResult does deep instantiation if DeepSubsumption is on checkResultTy rn_expr (tc_fun, fun_ctxt) inst_args app_res_rho (Check res_ty) -- Unify with expected type from the context @@ -651,18 +623,16 @@ quickLookKeys = [dollarIdKey, leftSectionKey, rightSectionKey] ********************************************************************* -} tcInstFun :: QLFlag - -> Bool -- False <=> Instantiate only /inferred/ variables at the end + -> Bool -- False <=> Instantiate only /top-level, inferred/ variables; -- so may return a sigma-type - -- True <=> Instantiate all type variables at the end: - -- return a rho-type - -- The /only/ call site that passes in False is the one - -- in tcInferSigma, which is used only to implement :type - -- Otherwise we do eager instantiation; in Fig 5 of the paper + -- True <=> Instantiate /top-level, invisible/ type variables; + -- always return a rho-type (but not a deep-rho type) + -- Generally speaking we pass in True; in Fig 5 of the paper -- |-inst returns a rho-type -> (HsExpr GhcTc, AppCtxt) -> TcSigmaType -> [HsExprArg 'TcpRn] -> TcM ( [HsExprArg 'TcpInst] - , TcSigmaType ) + , TcSigmaType ) -- Does not instantiate trailing invisible foralls -- 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). @@ -704,13 +674,9 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args _ -> False inst_fun :: [HsExprArg 'TcpRn] -> ForAllTyFlag -> Bool - -- True <=> instantiate a tyvar with this ForAllTyFlag + -- True <=> instantiate a tyvar that has this ForAllTyFlag inst_fun [] | inst_final = isInvisibleForAllTyFlag | otherwise = const False - -- Using `const False` for `:type` avoids - -- `forall {r1} (a :: TYPE r1) {r2} (b :: TYPE r2). a -> b` - -- turning into `forall a {r2} (b :: TYPE r2). a -> b`. - -- See #21088. inst_fun (EValArg {} : _) = isInvisibleForAllTyFlag inst_fun _ = isInferredForAllTyFlag ===================================== compiler/GHC/Tc/Gen/Bind.hs ===================================== @@ -1305,8 +1305,8 @@ tcMonoBinds is_rec sig_fn no_gen do { mult <- newMultiplicityVar ; ((co_fn, matches'), rhs_ty') - <- tcInferFRR (FRRBinder name) $ \ exp_ty -> - -- tcInferFRR: the type of a let-binder must have + <- runInferRhoFRR (FRRBinder name) $ \ exp_ty -> + -- runInferRhoFRR: the type of a let-binder must have -- a fixed runtime rep. See #23176 tcExtendBinderStack [TcIdBndr_ExpType name exp_ty NotTopLevel] $ -- We extend the error context even for a non-recursive @@ -1333,8 +1333,8 @@ tcMonoBinds is_rec sig_fn no_gen = addErrCtxt (PatMonoBindsCtxt pat grhss) $ do { mult <- tcMultAnnOnPatBind mult_ann - ; (grhss', pat_ty) <- tcInferFRR FRRPatBind $ \ exp_ty -> - -- tcInferFRR: the type of each let-binder must have + ; (grhss', pat_ty) <- runInferRhoFRR FRRPatBind $ \ exp_ty -> + -- runInferRhoFRR: the type of each let-binder must have -- a fixed runtime rep. See #23176 tcGRHSsPat mult grhss exp_ty @@ -1522,7 +1522,7 @@ tcLhs sig_fn no_gen (PatBind { pat_lhs = pat, pat_rhs = grhss, pat_mult = mult_a -- See Note [Typechecking pattern bindings] ; ((pat', nosig_mbis), pat_ty) <- addErrCtxt (PatMonoBindsCtxt pat grhss) $ - tcInferFRR FRRPatBind $ \ exp_ty -> + runInferSigmaFRR FRRPatBind $ \ exp_ty -> tcLetPat inst_sig_fun no_gen pat (Scaled mult exp_ty) $ -- The above inferred type get an unrestricted multiplicity. It may be -- worth it to try and find a finer-grained multiplicity here ===================================== compiler/GHC/Tc/Gen/Expr.hs ===================================== @@ -19,7 +19,7 @@ module GHC.Tc.Gen.Expr ( tcCheckPolyExpr, tcCheckPolyExprNC, tcCheckMonoExpr, tcCheckMonoExprNC, tcMonoExpr, tcMonoExprNC, - tcInferRho, tcInferRhoNC, + tcInferExpr, tcInferSigma, tcInferRho, tcInferRhoNC, tcPolyLExpr, tcPolyExpr, tcExpr, tcPolyLExprSig, tcSyntaxOp, tcSyntaxOpGen, SyntaxOpType(..), synKnownType, tcCheckId, @@ -233,17 +233,24 @@ tcPolyExprCheck expr res_ty * * ********************************************************************* -} +tcInferSigma :: LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcSigmaType) +tcInferSigma = tcInferExpr IIF_Sigma + tcInferRho, tcInferRhoNC :: LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcRhoType) -- Infer a *rho*-type. The return type is always instantiated. -tcInferRho (L loc expr) - = setSrcSpanA loc $ -- Set location /first/; see GHC.Tc.Utils.Monad +tcInferRho = tcInferExpr IIF_DeepRho +tcInferRhoNC = tcInferExprNC IIF_DeepRho + +tcInferExpr, tcInferExprNC :: InferInstFlag -> LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcType) +tcInferExpr iif (L loc expr) + = setSrcSpanA loc $ -- Set location /first/; see GHC.Tc.Utils.Monad addExprCtxt expr $ -- Note [Error contexts in generated code] - do { (expr', rho) <- tcInfer (tcExpr expr) + do { (expr', rho) <- runInfer iif IFRR_Any (tcExpr expr) ; return (L loc expr', rho) } -tcInferRhoNC (L loc expr) - = setSrcSpanA loc $ - do { (expr', rho) <- tcInfer (tcExpr expr) +tcInferExprNC iif (L loc expr) + = setSrcSpanA loc $ + do { (expr', rho) <- runInfer iif IFRR_Any (tcExpr expr) ; return (L loc expr', rho) } --------------- @@ -878,7 +885,7 @@ tcInferTupArgs boxity args ; return (Missing (Scaled mult arg_ty), arg_ty) } tc_infer_tup_arg i (Present x lexpr@(L l expr)) = do { (expr', arg_ty) <- case boxity of - Unboxed -> tcInferFRR (FRRUnboxedTuple i) (tcPolyExpr expr) + Unboxed -> runInferRhoFRR (FRRUnboxedTuple i) (tcPolyExpr expr) Boxed -> do { arg_ty <- newFlexiTyVarTy liftedTypeKind ; L _ expr' <- tcCheckPolyExpr lexpr arg_ty ; return (expr', arg_ty) } ===================================== compiler/GHC/Tc/Gen/Expr.hs-boot ===================================== @@ -1,8 +1,8 @@ module GHC.Tc.Gen.Expr where import GHC.Hs ( HsExpr, LHsExpr, SyntaxExprRn , SyntaxExprTc ) -import GHC.Tc.Utils.TcType ( TcRhoType, TcSigmaType, TcSigmaTypeFRR - , SyntaxOpType +import GHC.Tc.Utils.TcType ( TcType, TcRhoType, TcSigmaType, TcSigmaTypeFRR + , SyntaxOpType, InferInstFlag , ExpType, ExpRhoType, ExpSigmaType ) import GHC.Tc.Types ( TcM ) import GHC.Tc.Types.BasicTypes( TcCompleteSig ) @@ -33,6 +33,8 @@ tcExpr :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc) tcInferRho, tcInferRhoNC :: LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcRhoType) +tcInferExpr :: InferInstFlag -> LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcType) + tcSyntaxOp :: CtOrigin -> SyntaxExprRn -> [SyntaxOpType] -- ^ shape of syntax operator arguments ===================================== compiler/GHC/Tc/Gen/Head.hs ===================================== @@ -556,7 +556,7 @@ tcInferAppHead (fun,ctxt) do { mb_tc_fun <- tcInferAppHead_maybe fun ; case mb_tc_fun of Just (fun', fun_sigma) -> return (fun', fun_sigma) - Nothing -> tcInfer (tcExpr fun) } + Nothing -> runInferRho (tcExpr fun) } tcInferAppHead_maybe :: HsExpr GhcRn -> TcM (Maybe (HsExpr GhcTc, TcSigmaType)) ===================================== compiler/GHC/Tc/Gen/HsType.hs ===================================== @@ -1063,9 +1063,9 @@ tc_infer_lhs_type mode (L span ty) -- | Infer the kind of a type and desugar. This is the "up" type-checker, -- as described in Note [Bidirectional type checking] tc_infer_hs_type :: TcTyMode -> HsType GhcRn -> TcM (TcType, TcKind) - tc_infer_hs_type mode rn_ty - = tcInfer $ \exp_kind -> tcHsType mode rn_ty exp_kind + = runInferKind $ \exp_kind -> + tcHsType mode rn_ty exp_kind {- Note [Typechecking HsCoreTys] @@ -1985,7 +1985,7 @@ checkExpKind rn_ty ty ki (Check ki') = checkExpKind _rn_ty ty ki (Infer cell) = do -- NB: do not instantiate. -- See Note [Do not always instantiate eagerly in types] - co <- fillInferResult ki cell + co <- fillInferResultNoInst ki cell pure (ty `mkCastTy` co) --------------------------- ===================================== compiler/GHC/Tc/Gen/Match.hs ===================================== @@ -1034,7 +1034,7 @@ tcDoStmt ctxt (RecStmt { recS_stmts = L l stmts, recS_later_ids = later_names ; tcExtendIdEnv tup_ids $ do { ((stmts', (ret_op', tup_rets)), stmts_ty) - <- tcInfer $ \ exp_ty -> + <- runInferRho $ \ exp_ty -> tcStmtsAndThen ctxt tcDoStmt stmts exp_ty $ \ inner_res_ty -> do { tup_rets <- zipWithM tcCheckId tup_names (map mkCheckExpType tup_elt_tys) @@ -1046,7 +1046,7 @@ tcDoStmt ctxt (RecStmt { recS_stmts = L l stmts, recS_later_ids = later_names ; return (ret_op', tup_rets) } ; ((_, mfix_op'), mfix_res_ty) - <- tcInfer $ \ exp_ty -> + <- runInferRho $ \ exp_ty -> tcSyntaxOp DoOrigin mfix_op [synKnownType (mkVisFunTyMany tup_ty stmts_ty)] exp_ty $ \ _ _ -> return () @@ -1172,7 +1172,7 @@ tcApplicativeStmts tcApplicativeStmts ctxt pairs rhs_ty thing_inside = do { body_ty <- newFlexiTyVarTy liftedTypeKind ; let arity = length pairs - ; ts <- replicateM (arity-1) $ newInferExpType + ; ts <- replicateM (arity-1) $ newInferExpType IIF_DeepRho ; exp_tys <- replicateM arity $ newFlexiTyVarTy liftedTypeKind ; pat_tys <- replicateM arity $ newFlexiTyVarTy liftedTypeKind ; let fun_ty = mkVisFunTysMany pat_tys body_ty ===================================== compiler/GHC/Tc/Gen/Pat.hs ===================================== @@ -26,7 +26,7 @@ where import GHC.Prelude -import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcSyntaxOp, tcSyntaxOpGen, tcInferRho ) +import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcSyntaxOp, tcSyntaxOpGen, tcInferExpr ) import GHC.Hs import GHC.Hs.Syn.Type @@ -220,7 +220,7 @@ tcInferPat :: FixedRuntimeRepContext -> TcM a -> TcM ((LPat GhcTc, a), TcSigmaTypeFRR) tcInferPat frr_orig ctxt pat thing_inside - = tcInferFRR frr_orig $ \ exp_ty -> + = runInferSigmaFRR frr_orig $ \ exp_ty -> tc_lpat (unrestricted exp_ty) penv pat thing_inside where penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = PatOrigin } @@ -694,15 +694,17 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of -- restriction need to be put in place, if any, for linear view -- patterns to desugar to type-correct Core. - ; (expr',expr_ty) <- tcInferRho expr - -- Note [View patterns and polymorphism] + ; (expr', expr_rho) <- tcInferExpr IIF_ShallowRho expr + -- IIF_ShallowRho: do not perform deep instantiation, regardless of + -- DeepSubsumption (Note [View patterns and polymorphism]) + -- But we must do top-instantiation to expose the arrow to matchActualFunTy -- Expression must be a function ; let herald = ExpectedFunTyViewPat $ unLoc expr ; (expr_wrap1, Scaled _mult inf_arg_ty, inf_res_sigma) - <- matchActualFunTy herald (Just . HsExprRnThing $ unLoc expr) (1,expr_ty) expr_ty + <- matchActualFunTy herald (Just . HsExprRnThing $ unLoc expr) (1,expr_rho) expr_rho -- See Note [View patterns and polymorphism] - -- expr_wrap1 :: expr_ty "->" (inf_arg_ty -> inf_res_sigma) + -- expr_wrap1 :: expr_rho "->" (inf_arg_ty -> inf_res_sigma) -- Check that overall pattern is more polymorphic than arg type ; expr_wrap2 <- tc_sub_type penv (scaledThing pat_ty) inf_arg_ty @@ -715,18 +717,18 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of ; pat_ty <- readExpType h_pat_ty ; let expr_wrap2' = mkWpFun expr_wrap2 idHsWrapper (Scaled w pat_ty) inf_res_sigma - -- expr_wrap2' :: (inf_arg_ty -> inf_res_sigma) "->" - -- (pat_ty -> inf_res_sigma) - -- NB: pat_ty comes from matchActualFunTy, so it has a - -- fixed RuntimeRep, as needed to call mkWpFun. - ; let + -- expr_wrap2' :: (inf_arg_ty -> inf_res_sigma) "->" + -- (pat_ty -> inf_res_sigma) + -- NB: pat_ty comes from matchActualFunTy, so it has a + -- fixed RuntimeRep, as needed to call mkWpFun. + expr_wrap = expr_wrap2' <.> expr_wrap1 ; return $ (ViewPat pat_ty (mkLHsWrap expr_wrap expr') pat', res) } {- Note [View patterns and polymorphism] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider this exotic example: +Consider this exotic example (test T26331a): pair :: forall a. Bool -> a -> forall b. b -> (a,b) f :: Int -> blah @@ -735,11 +737,15 @@ Consider this exotic example: The expression (pair True) should have type pair True :: Int -> forall b. b -> (Int,b) so that it is ready to consume the incoming Int. It should be an -arrow type (t1 -> t2); hence using (tcInferRho expr). +arrow type (t1 -> t2); and we must not instantiate that `forall b`, +/even with DeepSubsumption/. Hence using `IIF_ShallowRho`; this is the only +place where `IIF_ShallowRho` is used. Then, when taking that arrow apart we want to get a *sigma* type (forall b. b->(Int,b)), because that's what we want to bind 'x' to. Fortunately that's what matchActualFunTy returns anyway. + +Another example is #26331. -} -- Type signatures in patterns @@ -768,8 +774,7 @@ Fortunately that's what matchActualFunTy returns anyway. penv pats thing_inside ; pat_ty <- readExpType (scaledThing pat_ty) ; return (mkHsWrapPat coi - (ListPat elt_ty pats') pat_ty, res) -} + (ListPat elt_ty pats') pat_ty, res) } TuplePat _ pats boxity -> do { let arity = length pats ===================================== compiler/GHC/Tc/Module.hs ===================================== @@ -62,7 +62,6 @@ import GHC.Tc.Gen.Match import GHC.Tc.Utils.Unify( checkConstraints, tcSubTypeSigma ) import GHC.Tc.Zonk.Type import GHC.Tc.Gen.Expr -import GHC.Tc.Gen.App( tcInferSigma ) import GHC.Tc.Utils.Monad import GHC.Tc.Gen.Export import GHC.Tc.Types.Evidence @@ -2628,10 +2627,11 @@ tcRnExpr hsc_env mode rdr_expr failIfErrsM ; -- Typecheck the expression - ((tclvl, res_ty), lie) + ((tclvl, (_tc_expr, res_ty)), lie) <- captureTopConstraints $ pushTcLevelM $ - tcInferSigma inst rn_expr ; + (if inst then tcInferRho rn_expr + else tcInferSigma rn_expr); -- Generalise uniq <- newUnique ; ===================================== compiler/GHC/Tc/Utils/TcMType.hs ===================================== @@ -65,7 +65,7 @@ module GHC.Tc.Utils.TcMType ( -- Expected types ExpType(..), ExpSigmaType, ExpRhoType, mkCheckExpType, newInferExpType, newInferExpTypeFRR, - tcInfer, tcInferFRR, + runInfer, runInferRho, runInferSigma, runInferKind, runInferRhoFRR, runInferSigmaFRR, readExpType, readExpType_maybe, readScaledExpType, expTypeToType, scaledExpTypeToType, checkingExpType_maybe, checkingExpType, @@ -438,30 +438,29 @@ See test case T21325. -- actual data definition is in GHC.Tc.Utils.TcType -newInferExpType :: TcM ExpType -newInferExpType = new_inferExpType Nothing +newInferExpType :: InferInstFlag -> TcM ExpType +newInferExpType iif = new_inferExpType iif IFRR_Any -newInferExpTypeFRR :: FixedRuntimeRepContext -> TcM ExpTypeFRR -newInferExpTypeFRR frr_orig +newInferExpTypeFRR :: InferInstFlag -> FixedRuntimeRepContext -> TcM ExpTypeFRR +newInferExpTypeFRR iif frr_orig = do { th_lvl <- getThLevel - ; if - -- See [Wrinkle: Typed Template Haskell] - -- in Note [hasFixedRuntimeRep] in GHC.Tc.Utils.Concrete. - | TypedBrack _ <- th_lvl - -> new_inferExpType Nothing + ; let mb_frr = case th_lvl of + TypedBrack {} -> IFRR_Any + _ -> IFRR_Check frr_orig + -- mb_frr: see [Wrinkle: Typed Template Haskell] + -- in Note [hasFixedRuntimeRep] in GHC.Tc.Utils.Concrete. - | otherwise - -> new_inferExpType (Just frr_orig) } + ; new_inferExpType iif mb_frr } -new_inferExpType :: Maybe FixedRuntimeRepContext -> TcM ExpType -new_inferExpType mb_frr_orig +new_inferExpType :: InferInstFlag -> InferFRRFlag -> TcM ExpType +new_inferExpType iif ifrr = do { u <- newUnique ; tclvl <- getTcLevel ; traceTc "newInferExpType" (ppr u <+> ppr tclvl) ; ref <- newMutVar Nothing ; return (Infer (IR { ir_uniq = u, ir_lvl = tclvl - , ir_ref = ref - , ir_frr = mb_frr_orig })) } + , ir_inst = iif, ir_frr = ifrr + , ir_ref = ref })) } -- | Extract a type out of an ExpType, if one exists. But one should always -- exist. Unless you're quite sure you know what you're doing. @@ -515,12 +514,12 @@ inferResultToType (IR { ir_uniq = u, ir_lvl = tc_lvl where -- See Note [TcLevel of ExpType] new_meta = case mb_frr of - Nothing -> do { rr <- newMetaTyVarTyAtLevel tc_lvl runtimeRepTy + IFRR_Any -> do { rr <- newMetaTyVarTyAtLevel tc_lvl runtimeRepTy ; newMetaTyVarTyAtLevel tc_lvl (mkTYPEapp rr) } - Just frr -> mdo { rr <- newConcreteTyVarTyAtLevel conc_orig tc_lvl runtimeRepTy - ; tau <- newMetaTyVarTyAtLevel tc_lvl (mkTYPEapp rr) - ; let conc_orig = ConcreteFRR $ FixedRuntimeRepOrigin tau frr - ; return tau } + IFRR_Check frr -> mdo { rr <- newConcreteTyVarTyAtLevel conc_orig tc_lvl runtimeRepTy + ; tau <- newMetaTyVarTyAtLevel tc_lvl (mkTYPEapp rr) + ; let conc_orig = ConcreteFRR $ FixedRuntimeRepOrigin tau frr + ; return tau } {- Note [inferResultToType] ~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -537,20 +536,31 @@ Note [fillInferResult] in GHC.Tc.Utils.Unify. -- | Infer a type using a fresh ExpType -- See also Note [ExpType] in "GHC.Tc.Utils.TcMType" -- --- Use 'tcInferFRR' if you require the type to have a fixed +-- Use 'runInferFRR' if you require the type to have a fixed -- runtime representation. -tcInfer :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType) -tcInfer = tc_infer Nothing +runInferSigma :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType) +runInferSigma = runInfer IIF_Sigma IFRR_Any --- | Like 'tcInfer', except it ensures that the resulting type +runInferRho :: (ExpRhoType -> TcM a) -> TcM (a, TcRhoType) +runInferRho = runInfer IIF_DeepRho IFRR_Any + +runInferKind :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType) +-- Used for kind-checking types, where we never want deep instantiation, +-- nor FRR checks +runInferKind = runInfer IIF_Sigma IFRR_Any + +-- | Like 'runInferRho', except it ensures that the resulting type -- has a syntactically fixed RuntimeRep as per Note [Fixed RuntimeRep] in -- GHC.Tc.Utils.Concrete. -tcInferFRR :: FixedRuntimeRepContext -> (ExpSigmaTypeFRR -> TcM a) -> TcM (a, TcSigmaTypeFRR) -tcInferFRR frr_orig = tc_infer (Just frr_orig) +runInferRhoFRR :: FixedRuntimeRepContext -> (ExpRhoTypeFRR -> TcM a) -> TcM (a, TcRhoTypeFRR) +runInferRhoFRR frr_orig = runInfer IIF_DeepRho (IFRR_Check frr_orig) + +runInferSigmaFRR :: FixedRuntimeRepContext -> (ExpSigmaTypeFRR -> TcM a) -> TcM (a, TcSigmaTypeFRR) +runInferSigmaFRR frr_orig = runInfer IIF_Sigma (IFRR_Check frr_orig) -tc_infer :: Maybe FixedRuntimeRepContext -> (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType) -tc_infer mb_frr tc_check - = do { res_ty <- new_inferExpType mb_frr +runInfer :: InferInstFlag -> InferFRRFlag -> (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType) +runInfer iif mb_frr tc_check + = do { res_ty <- new_inferExpType iif mb_frr ; result <- tc_check res_ty ; res_ty <- readExpType res_ty ; return (result, res_ty) } ===================================== compiler/GHC/Tc/Utils/TcType.hs ===================================== @@ -24,14 +24,14 @@ module GHC.Tc.Utils.TcType ( -------------------------------- -- Types TcType, TcSigmaType, TcTypeFRR, TcSigmaTypeFRR, - TcRhoType, TcTauType, TcPredType, TcThetaType, + TcRhoType, TcRhoTypeFRR, TcTauType, TcPredType, TcThetaType, TcTyVar, TcTyVarSet, TcDTyVarSet, TcTyCoVarSet, TcDTyCoVarSet, TcKind, TcCoVar, TcTyCoVar, TcTyVarBinder, TcInvisTVBinder, TcReqTVBinder, TcTyCon, MonoTcTyCon, PolyTcTyCon, TcTyConBinder, KnotTied, - ExpType(..), ExpKind, InferResult(..), + ExpType(..), ExpKind, InferResult(..), InferInstFlag(..), InferFRRFlag(..), ExpTypeFRR, ExpSigmaType, ExpSigmaTypeFRR, - ExpRhoType, + ExpRhoType, ExpRhoTypeFRR, mkCheckExpType, checkingExpType_maybe, checkingExpType, @@ -380,6 +380,7 @@ type TcSigmaType = TcType -- See Note [Return arguments with a fixed RuntimeRep. type TcSigmaTypeFRR = TcSigmaType -- TODO: consider making this a newtype. +type TcRhoTypeFRR = TcRhoType type TcRhoType = TcType -- Note [TcRhoType] type TcTauType = TcType @@ -408,9 +409,13 @@ data InferResult , ir_lvl :: TcLevel -- ^ See Note [TcLevel of ExpType] in GHC.Tc.Utils.TcMType - , ir_frr :: Maybe FixedRuntimeRepContext + , ir_frr :: InferFRRFlag -- ^ See Note [FixedRuntimeRep context in ExpType] in GHC.Tc.Utils.TcMType + , ir_inst :: InferInstFlag + -- ^ True <=> when DeepSubsumption is on, deeply instantiate before filling, + -- See Note [Instantiation of InferResult] in GHC.Tc.Utils.Unify + , ir_ref :: IORef (Maybe TcType) } -- ^ The type that fills in this hole should be a @Type@, -- that is, its kind should be @TYPE rr@ for some @rr :: RuntimeRep@. @@ -419,26 +424,48 @@ data InferResult -- @rr@ must be concrete, in the sense of Note [Concrete types] -- in GHC.Tc.Utils.Concrete. -type ExpSigmaType = ExpType +data InferFRRFlag + = IFRR_Check -- Check that the result type has a fixed runtime rep + FixedRuntimeRepContext -- Typically used for function arguments and lambdas + + | IFRR_Any -- No need to check for fixed runtime-rep + +data InferInstFlag -- Specifies whether the inference should return an uninstantiated + -- SigmaType, or a (possibly deeply) instantiated RhoType + -- See Note [Instantiation of InferResult] in GHC.Tc.Utils.Unify + + = IIF_Sigma -- Trying to infer a SigmaType + -- Don't instantiate at all, regardless of DeepSubsumption + -- Typically used when inferring the type of a pattern + + | IIF_ShallowRho -- Trying to infer a shallow RhoType (no foralls or => at the top) + -- Top-instantiate (only, regardless of DeepSubsumption) before filling the hole + -- Typically used when inferring the type of an expression + + | IIF_DeepRho -- Trying to infer a possibly-deep RhoType (depending on DeepSubsumption) + -- If DeepSubsumption is off, same as IIF_ShallowRho + -- If DeepSubsumption is on, instantiate deeply before filling the hole + +type ExpSigmaType = ExpType +type ExpRhoType = ExpType + -- Invariant: in ExpRhoType, if -XDeepSubsumption is on, + -- and we are in checking mode (i.e. the ExpRhoType is (Check rho)), + -- then the `rho` is deeply skolemised -- | An 'ExpType' which has a fixed RuntimeRep. -- -- For a 'Check' 'ExpType', the stored 'TcType' must have -- a fixed RuntimeRep. For an 'Infer' 'ExpType', the 'ir_frr' --- field must be of the form @Just frr_orig@. -type ExpTypeFRR = ExpType +-- field must be of the form @IFRR_Check frr_orig@. +type ExpTypeFRR = ExpType -- | Like 'TcSigmaTypeFRR', but for an expected type. -- -- See 'ExpTypeFRR'. type ExpSigmaTypeFRR = ExpTypeFRR +type ExpRhoTypeFRR = ExpTypeFRR -- TODO: consider making this a newtype. -type ExpRhoType = ExpType - -- Invariant: if -XDeepSubsumption is on, - -- and we are checking (i.e. the ExpRhoType is (Check rho)), - -- then the `rho` is deeply skolemised - -- | Like 'ExpType', but on kind level type ExpKind = ExpType @@ -447,12 +474,17 @@ instance Outputable ExpType where ppr (Infer ir) = ppr ir instance Outputable InferResult where - ppr (IR { ir_uniq = u, ir_lvl = lvl, ir_frr = mb_frr }) - = text "Infer" <> mb_frr_text <> braces (ppr u <> comma <> ppr lvl) + ppr (IR { ir_uniq = u, ir_lvl = lvl, ir_frr = mb_frr, ir_inst = inst }) + = text "Infer" <> parens (pp_inst <> pp_frr) + <> braces (ppr u <> comma <> ppr lvl) where - mb_frr_text = case mb_frr of - Just _ -> text "FRR" - Nothing -> empty + pp_inst = case inst of + IIF_Sigma -> text "Sigma" + IIF_ShallowRho -> text "ShallowRho" + IIF_DeepRho -> text "DeepRho" + pp_frr = case mb_frr of + IFRR_Check {} -> text ",FRR" + IFRR_Any -> empty -- | Make an 'ExpType' suitable for checking. mkCheckExpType :: TcType -> ExpType ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -27,7 +27,7 @@ module GHC.Tc.Utils.Unify ( -- Skolemisation DeepSubsumptionFlag(..), getDeepSubsumptionFlag, isRhoTyDS, tcSkolemise, tcSkolemiseCompleteSig, tcSkolemiseExpectedType, - deeplyInstantiate, + dsInstantiate, -- Various unifications unifyType, unifyKind, unifyInvisibleType, @@ -40,7 +40,6 @@ module GHC.Tc.Utils.Unify ( -------------------------------- -- Holes - tcInfer, matchExpectedListTy, matchExpectedTyConApp, matchExpectedAppTy, @@ -60,7 +59,7 @@ module GHC.Tc.Utils.Unify ( simpleUnifyCheck, UnifyCheckCaller(..), SimpleUnifyResult(..), - fillInferResult, fillInferResultDS + fillInferResult, fillInferResultNoInst ) where import GHC.Prelude @@ -801,13 +800,13 @@ matchExpectedFunTys :: forall a. -- If exp_ty is Infer {}, then [ExpPatType] and ExpRhoType results are all Infer{} matchExpectedFunTys herald _ctxt arity (Infer inf_res) thing_inside = do { arg_tys <- mapM (new_infer_arg_ty herald) [1 .. arity] - ; res_ty <- newInferExpType + ; res_ty <- newInferExpType (ir_inst inf_res) ; result <- thing_inside (map ExpFunPatTy arg_tys) res_ty ; arg_tys <- mapM (\(Scaled m t) -> Scaled m <$> readExpType t) arg_tys ; res_ty <- readExpType res_ty -- NB: mkScaledFunTys arg_tys res_ty does not contain any foralls -- (even nested ones), so no need to instantiate. - ; co <- fillInferResult (mkScaledFunTys arg_tys res_ty) inf_res + ; co <- fillInferResultNoInst (mkScaledFunTys arg_tys res_ty) inf_res ; return (mkWpCastN co, result) } matchExpectedFunTys herald ctx arity (Check top_ty) thing_inside @@ -914,10 +913,10 @@ matchExpectedFunTys herald ctx arity (Check top_ty) thing_inside ; co <- unifyType Nothing (mkScaledFunTys more_arg_tys res_ty) fun_ty ; return (mkWpCastN co, result) } -new_infer_arg_ty :: ExpectedFunTyOrigin -> Int -> TcM (Scaled ExpSigmaTypeFRR) +new_infer_arg_ty :: ExpectedFunTyOrigin -> Int -> TcM (Scaled ExpRhoTypeFRR) new_infer_arg_ty herald arg_pos -- position for error messages only = do { mult <- newFlexiTyVarTy multiplicityTy - ; inf_hole <- newInferExpTypeFRR (FRRExpectedFunTy herald arg_pos) + ; inf_hole <- newInferExpTypeFRR IIF_DeepRho (FRRExpectedFunTy herald arg_pos) ; return (mkScaled mult inf_hole) } new_check_arg_ty :: ExpectedFunTyOrigin -> Int -> TcM (Scaled TcType) @@ -1075,18 +1074,6 @@ matchExpectedAppTy orig_ty * ********************************************************************** -} -{- Note [inferResultToType] -~~~~~~~~~~~~~~~~~~~~~~~~~~~ -expTypeToType and inferResultType convert an InferResult to a monotype. -It must be a monotype because if the InferResult isn't already filled in, -we fill it in with a unification variable (hence monotype). So to preserve -order-independence we check for mono-type-ness even if it *is* filled in -already. - -See also Note [TcLevel of ExpType] in GHC.Tc.Utils.TcType, and -Note [fillInferResult]. --} - -- | Fill an 'InferResult' with the given type. -- -- If @co = fillInferResult t1 infer_res@, then @co :: t1 ~# t2@, @@ -1098,14 +1085,14 @@ Note [fillInferResult]. -- The stored type @t2@ is at the same level as given by the -- 'ir_lvl' field. -- - FRR invariant. --- Whenever the 'ir_frr' field is not @Nothing@, @t2@ is guaranteed +-- Whenever the 'ir_frr' field is `IFRR_Check`, @t2@ is guaranteed -- to have a syntactically fixed RuntimeRep, in the sense of -- Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete. -fillInferResult :: TcType -> InferResult -> TcM TcCoercionN -fillInferResult act_res_ty (IR { ir_uniq = u - , ir_lvl = res_lvl - , ir_frr = mb_frr - , ir_ref = ref }) +fillInferResultNoInst :: TcType -> InferResult -> TcM TcCoercionN +fillInferResultNoInst act_res_ty (IR { ir_uniq = u + , ir_lvl = res_lvl + , ir_frr = mb_frr + , ir_ref = ref }) = do { mb_exp_res_ty <- readTcRef ref ; case mb_exp_res_ty of Just exp_res_ty @@ -1126,7 +1113,7 @@ fillInferResult act_res_ty (IR { ir_uniq = u ppr u <> colon <+> ppr act_res_ty <+> char '~' <+> ppr exp_res_ty ; cur_lvl <- getTcLevel ; unless (cur_lvl `sameDepthAs` res_lvl) $ - ensureMonoType act_res_ty + ensureMonoType act_res_ty -- See (FIR1) ; unifyType Nothing act_res_ty exp_res_ty } Nothing -> do { traceTc "Filling inferred ExpType" $ @@ -1140,16 +1127,28 @@ fillInferResult act_res_ty (IR { ir_uniq = u -- fixed RuntimeRep (if necessary, i.e. 'mb_frr' is not 'Nothing'). ; (frr_co, act_res_ty) <- case mb_frr of - Nothing -> return (mkNomReflCo act_res_ty, act_res_ty) - Just frr_orig -> hasFixedRuntimeRep frr_orig act_res_ty + IFRR_Any -> return (mkNomReflCo act_res_ty, act_res_ty) + IFRR_Check frr_orig -> hasFixedRuntimeRep frr_orig act_res_ty -- Compose the two coercions. ; let final_co = prom_co `mkTransCo` frr_co ; writeTcRef ref (Just act_res_ty) - ; return final_co } - } + ; return final_co } } + +fillInferResult :: CtOrigin -> TcType -> InferResult -> TcM HsWrapper +-- See Note [Instantiation of InferResult] +fillInferResult ct_orig res_ty ires@(IR { ir_inst = iif }) + = case iif of + IIF_Sigma -> do { co <- fillInferResultNoInst res_ty ires + ; return (mkWpCastN co) } + IIF_ShallowRho -> do { (wrap, res_ty') <- topInstantiate ct_orig res_ty + ; co <- fillInferResultNoInst res_ty' ires + ; return (mkWpCastN co <.> wrap) } + IIF_DeepRho -> do { (wrap, res_ty') <- dsInstantiate ct_orig res_ty + ; co <- fillInferResultNoInst res_ty' ires + ; return (mkWpCastN co <.> wrap) } {- Note [fillInferResult] ~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1210,39 +1209,96 @@ For (2), we simply look to see if the hole is filled already. - if it is filled, we simply unify with the type that is already there -There is one wrinkle. Suppose we have - case e of - T1 -> e1 :: (forall a. a->a) -> Int - G2 -> e2 -where T1 is not GADT or existential, but G2 is a GADT. Then suppose the -T1 alternative fills the hole with (forall a. a->a) -> Int, which is fine. -But now the G2 alternative must not *just* unify with that else we'd risk -allowing through (e2 :: (forall a. a->a) -> Int). If we'd checked G2 first -we'd have filled the hole with a unification variable, which enforces a -monotype. - -So if we check G2 second, we still want to emit a constraint that restricts -the RHS to be a monotype. This is done by ensureMonoType, and it works -by simply generating a constraint (alpha ~ ty), where alpha is a fresh +(FIR1) There is one wrinkle. Suppose we have + case e of + T1 -> e1 :: (forall a. a->a) -> Int + G2 -> e2 + where T1 is not GADT or existential, but G2 is a GADT. Then suppose the + T1 alternative fills the hole with (forall a. a->a) -> Int, which is fine. + But now the G2 alternative must not *just* unify with that else we'd risk + allowing through (e2 :: (forall a. a->a) -> Int). If we'd checked G2 first + we'd have filled the hole with a unification variable, which enforces a + monotype. + + So if we check G2 second, we still want to emit a constraint that restricts + the RHS to be a monotype. This is done by ensureMonoType, and it works + by simply generating a constraint (alpha ~ ty), where alpha is a fresh unification variable. We discard the evidence. --} +Note [Instantiation of InferResult] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When typechecking expressions (not types, not patterns), we always almost +always instantiate before filling in `InferResult`, so that the result is a +TcRhoType. This behaviour is controlled by the `ir_inst :: InferInstFlag` +field of `InferResult`. --- | A version of 'fillInferResult' that also performs deep instantiation --- when deep subsumption is enabled. --- --- See also Note [Instantiation of InferResult]. -fillInferResultDS :: CtOrigin -> TcRhoType -> InferResult -> TcM HsWrapper -fillInferResultDS ct_orig rho inf_res - = do { massertPpr (isRhoTy rho) $ - vcat [ text "fillInferResultDS: input type is not a rho-type" - , text "ty:" <+> ppr rho ] - ; ds_flag <- getDeepSubsumptionFlag - ; case ds_flag of - Shallow -> mkWpCastN <$> fillInferResult rho inf_res - Deep -> do { (inst_wrap, rho') <- deeplyInstantiate ct_orig rho - ; co <- fillInferResult rho' inf_res - ; return (mkWpCastN co <.> inst_wrap) } } +If we do instantiate (ir_inst = IIF_DeepRho), and DeepSubsumption is enabled, +we instantiate deeply. See `tcInferResult`. + +Usually this field is `IIF_DeepRho` meaning "return a (possibly deep) rho-type". +Why is this the common case? See #17173 for discussion. Here are some examples +of why: + +1. Consider + f x = (*) + We want to instantiate the type of (*) before returning, else we + will infer the type + f :: forall {a}. a -> forall b. Num b => b -> b -> b + This is surely confusing for users. + + And worse, the monomorphism restriction won't work properly. The MR is + dealt with in simplifyInfer, and simplifyInfer has no way of + instantiating. This could perhaps be worked around, but it may be + hard to know even when instantiation should happen. + +2. Another reason. Consider + f :: (?x :: Int) => a -> a + g y = let ?x = 3::Int in f + Here want to instantiate f's type so that the ?x::Int constraint + gets discharged by the enclosing implicit-parameter binding. + +3. Suppose one defines plus = (+). If we instantiate lazily, we will + infer plus :: forall a. Num a => a -> a -> a. However, the monomorphism + restriction compels us to infer + plus :: Integer -> Integer -> Integer + (or similar monotype). Indeed, the only way to know whether to apply + the monomorphism restriction at all is to instantiate + +HOWEVER, not always! Here are places where we want `IIF_Sigma` meaning +"return a sigma-type": + +* IIF_Sigma: In GHC.Tc.Module.tcRnExpr, which implements GHCi's :type + command, we want to return a completely uninstantiated type. + See Note [Implementing :type] in GHC.Tc.Module. + +* IIF_Sigma: In types we can't lambda-abstract, so we must be careful not to instantiate + at all. See calls to `runInferHsType` + +* IIF_Sigma: in patterns we don't want to instantiate at all. See the use of + `runInferSigmaFRR` in GHC.Tc.Gen.Pat + +* IIF_ShallowRho: in the expression part of a view pattern, we must top-instantiate + but /not/ deeply instantiate (#26331). See Note [View patterns and polymorphism] + in GHC.Tc.Gen.Pat. This the only place we use IIF_ShallowRho. + +Why do we want to deeply instantiate, ever? Why isn't top-instantiation enough? +Answer: to accept the following program (T26225b) with -XDeepSubsumption, we +need to deeply instantiate when inferring in checkResultTy: + + f :: Int -> (forall a. a->a) + g :: Int -> Bool -> Bool + + test b = + case b of + True -> f + False -> g + +If we don't deeply instantiate in the branches of the case expression, we will +try to unify the type of 'f' with that of 'g', which fails. If we instead +deeply instantiate 'f', we will fill the 'InferResult' with 'Int -> alpha -> alpha' +which then successfully unifies with the type of 'g' when we come to fill the +'InferResult' hole a second time for the second case branch. +-} {- ************************************************************************ @@ -1337,7 +1393,7 @@ tcSubTypeMono rn_expr act_ty exp_ty , text "act_ty:" <+> ppr act_ty , text "rn_expr:" <+> ppr rn_expr]) $ case exp_ty of - Infer inf_res -> fillInferResult act_ty inf_res + Infer inf_res -> fillInferResultNoInst act_ty inf_res Check exp_ty -> unifyType (Just $ HsExprRnThing rn_expr) act_ty exp_ty ------------------------ @@ -1351,7 +1407,7 @@ tcSubTypePat inst_orig ctxt (Check ty_actual) ty_expected = tc_sub_type unifyTypeET inst_orig ctxt ty_actual ty_expected tcSubTypePat _ _ (Infer inf_res) ty_expected - = do { co <- fillInferResult ty_expected inf_res + = do { co <- fillInferResultNoInst ty_expected inf_res -- In patterns we do not instantatiate ; return (mkWpCastN (mkSymCo co)) } @@ -1377,7 +1433,7 @@ tcSubTypeDS rn_expr act_rho exp_rho -- | Checks that the 'actual' type is more polymorphic than the 'expected' type. tcSubType :: CtOrigin -- ^ Used when instantiating -> UserTypeCtxt -- ^ Used when skolemising - -> Maybe TypedThing -- ^ The expression that has type 'actual' (if known) + -> Maybe TypedThing -- ^ The expression that has type 'actual' (if known) -> TcSigmaType -- ^ Actual type -> ExpRhoType -- ^ Expected type -> TcM HsWrapper @@ -1386,10 +1442,7 @@ tcSubType inst_orig ctxt m_thing ty_actual res_ty Check ty_expected -> tc_sub_type (unifyType m_thing) inst_orig ctxt ty_actual ty_expected - Infer inf_res -> do { (wrap, rho) <- topInstantiate inst_orig ty_actual - -- See Note [Instantiation of InferResult] - ; inst <- fillInferResultDS inst_orig rho inf_res - ; return (inst <.> wrap) } + Infer inf_res -> fillInferResult inst_orig ty_actual inf_res --------------- tcSubTypeSigma :: CtOrigin -- where did the actual type arise / why are we @@ -1428,47 +1481,6 @@ addSubTypeCtxt ty_actual ty_expected thing_inside ; return (tidy_env, SubTypeCtxt ty_expected ty_actual) } -{- Note [Instantiation of InferResult] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -When typechecking expressions (not types, not patterns), we always instantiate -before filling in InferResult, so that the result is a TcRhoType. -See #17173 for discussion. - -For example: - -1. Consider - f x = (*) - We want to instantiate the type of (*) before returning, else we - will infer the type - f :: forall {a}. a -> forall b. Num b => b -> b -> b - This is surely confusing for users. - - And worse, the monomorphism restriction won't work properly. The MR is - dealt with in simplifyInfer, and simplifyInfer has no way of - instantiating. This could perhaps be worked around, but it may be - hard to know even when instantiation should happen. - -2. Another reason. Consider - f :: (?x :: Int) => a -> a - g y = let ?x = 3::Int in f - Here want to instantiate f's type so that the ?x::Int constraint - gets discharged by the enclosing implicit-parameter binding. - -3. Suppose one defines plus = (+). If we instantiate lazily, we will - infer plus :: forall a. Num a => a -> a -> a. However, the monomorphism - restriction compels us to infer - plus :: Integer -> Integer -> Integer - (or similar monotype). Indeed, the only way to know whether to apply - the monomorphism restriction at all is to instantiate - -There is one place where we don't want to instantiate eagerly, -namely in GHC.Tc.Module.tcRnExpr, which implements GHCi's :type -command. See Note [Implementing :type] in GHC.Tc.Module. - -This also means that, if DeepSubsumption is enabled, we should also instantiate -deeply; we do this by using fillInferResultDS. --} - --------------- tc_sub_type :: (TcType -> TcType -> TcM TcCoercionN) -- How to unify -> CtOrigin -- Used when instantiating @@ -2133,7 +2145,17 @@ deeplySkolemise skol_info ty = return (idHsWrapper, [], [], substTy subst ty) -- substTy is a quick no-op on an empty substitution +dsInstantiate :: CtOrigin -> TcType -> TcM (HsWrapper, Type) +-- Do topInstantiate or deeplyInstantiate, depending on -XDeepSubsumption +dsInstantiate orig ty + = do { ds_flag <- getDeepSubsumptionFlag + ; case ds_flag of + Shallow -> topInstantiate orig ty + Deep -> deeplyInstantiate orig ty } + deeplyInstantiate :: CtOrigin -> TcType -> TcM (HsWrapper, Type) +-- Instantiate invisible foralls, even ones nested +-- (to the right) under arrows deeplyInstantiate orig ty = go init_subst ty where ===================================== testsuite/tests/patsyn/should_compile/T26331.hs ===================================== @@ -0,0 +1,47 @@ +{-# LANGUAGE DeepSubsumption #-} + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE TypeAbstractions #-} +{-# LANGUAGE StandaloneKindSignatures #-} + +module T26331 where + +import Data.Kind (Constraint, Type) + +type Apply :: (k1 ~> k2) -> k1 -> k2 +type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 + +type (~>) :: Type -> Type -> Type +type a ~> b = TyFun a b -> Type +infixr 0 ~> + +data TyFun :: Type -> Type -> Type + +type Sing :: k -> Type +type family Sing @k :: k -> Type + +type SingFunction2 :: (a1 ~> a2 ~> b) -> Type +type SingFunction2 (f :: a1 ~> a2 ~> b) = + forall t1 t2. Sing t1 -> Sing t2 -> Sing (f `Apply` t1 `Apply` t2) + +unSingFun2 :: forall f. Sing f -> SingFunction2 f +-- unSingFun2 :: forall f. Sing f -> forall t1 t2. blah +unSingFun2 sf x = error "urk" + +singFun2 :: forall f. SingFunction2 f -> Sing f +singFun2 f = error "urk" + +-------- This is the tricky bit ------- +pattern SLambda2 :: forall f. SingFunction2 f -> Sing f +pattern SLambda2 x <- (unSingFun2 -> x) -- We want to push down (SingFunction2 f) + -- /uninstantiated/ into the pattern `x` + where + SLambda2 lam2 = singFun2 lam2 + ===================================== testsuite/tests/patsyn/should_compile/T26331a.hs ===================================== @@ -0,0 +1,11 @@ +{-# LANGUAGE DeepSubsumption #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE RankNTypes #-} + +module T26331a where + +pair :: forall a. Bool -> a -> forall b. b -> (a,b) +pair = error "urk" + +f :: Int -> ((Int,Bool),(Int,Char)) +f (pair True -> x) = (x True, x 'c') -- (x :: forall b. b -> (Int,b)) ===================================== testsuite/tests/patsyn/should_compile/all.T ===================================== @@ -85,3 +85,5 @@ test('T21531', [ grep_errmsg(r'INLINE') ], compile, ['-ddump-ds']) test('T22521', normal, compile, ['']) test('T23038', normal, compile_fail, ['']) test('T22328', normal, compile, ['']) +test('T26331', normal, compile, ['']) +test('T26331a', normal, compile, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/299b483c9e86a26467ab3e460c137179... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/299b483c9e86a26467ab3e460c137179... You're receiving this email because of your account on gitlab.haskell.org.