Marge Bot pushed to branch wip/marge_bot_batch_merge_job at Glasgow Haskell Compiler / GHC Commits: eb2ab1e2 by Oleg Grenrus at 2025-08-29T11:00:53-04:00 Generalise thNameToGhcName by adding HasHscEnv There were multiple single monad-specific `getHscEnv` across codebase. HasHscEnv is modelled on HasDynFlags. My first idea was to simply add thNameToGhcNameHsc and thNameToGhcNameTc, but those would been exactly the same as thNameToGhcName already. Also add an usage example to thNameToGhcName and mention that it's recommended way of looking up names in GHC plugins - - - - - 2d575a7f by fendor at 2025-08-29T11:01:36-04:00 configure: Bump minimal bootstrap GHC version to 9.10 - - - - - 450d7226 by Simon Peyton Jones at 2025-08-29T13:06:36-04: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. - - - - - 69889431 by sheaf at 2025-08-29T13:06:53-04:00 Back-compat for TH SpecialiseP data-con of Pragma This commit improves the backwards-compatibility story for the SpecialiseP constructor of the Template Haskell 'Pragma' datatype. Instead of keeping the constructor but deprecating it, this commit makes it into a bundled pattern synonym of the Pragma datatype. We no longer deprecate it; it's useful for handling old-form specialise pragmas. - - - - - 30 changed files: - .gitlab-ci.yml - compiler/GHC/Core/Opt/Monad.hs - compiler/GHC/Driver/Env.hs - compiler/GHC/Driver/Env/Types.hs - compiler/GHC/Driver/Main.hs - compiler/GHC/Plugins.hs - compiler/GHC/StgToByteCode.hs - 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 - compiler/GHC/ThToHs.hs - configure.ac - libraries/ghc-boot-th/GHC/Boot/TH/Ppr.hs - libraries/ghc-internal/src/GHC/Internal/TH/Syntax.hs - libraries/template-haskell/Language/Haskell/TH/Lib.hs - libraries/template-haskell/Language/Haskell/TH/Syntax.hs - libraries/template-haskell/changelog.md - testsuite/tests/interface-stability/template-haskell-exports.stdout - + testsuite/tests/patsyn/should_compile/T26331.hs - + testsuite/tests/patsyn/should_compile/T26331a.hs - testsuite/tests/patsyn/should_compile/all.T Changes: ===================================== .gitlab-ci.yml ===================================== @@ -104,6 +104,7 @@ workflow: # which versions of GHC to allow bootstrap with .bootstrap_matrix : &bootstrap_matrix matrix: + # If you update this version, be sure to also update 'MinBootGhcVersion' in configure.ac - GHC_VERSION: 9.10.1 DOCKER_IMAGE: "registry.gitlab.haskell.org/ghc/ci-images/x86_64-linux-deb12-ghc9_10:$DOCKER_REV" - GHC_VERSION: 9.12.2 ===================================== compiler/GHC/Core/Opt/Monad.hs ===================================== @@ -16,7 +16,7 @@ module GHC.Core.Opt.Monad ( mapDynFlagsCoreM, dropSimplCount, -- ** Reading from the monad - getHscEnv, getModule, + getModule, initRuleEnv, getExternalRuleBase, getDynFlags, getPackageFamInstEnv, getInteractiveContext, @@ -243,8 +243,8 @@ liftIOWithCount what = liftIO what >>= (\(count, x) -> addSimplCount count >> re ************************************************************************ -} -getHscEnv :: CoreM HscEnv -getHscEnv = read cr_hsc_env +instance HasHscEnv CoreM where + getHscEnv = read cr_hsc_env getHomeRuleBase :: CoreM RuleBase getHomeRuleBase = read cr_rule_base ===================================== compiler/GHC/Driver/Env.hs ===================================== @@ -2,6 +2,7 @@ module GHC.Driver.Env ( Hsc(..) , HscEnv (..) + , HasHscEnv (..) , hsc_mod_graph , setModuleGraph , hscUpdateFlags @@ -49,7 +50,7 @@ import GHC.Driver.Errors ( printOrThrowDiagnostics ) import GHC.Driver.Errors.Types ( GhcMessage ) import GHC.Driver.Config.Logger (initLogFlags) import GHC.Driver.Config.Diagnostic (initDiagOpts, initPrintConfig) -import GHC.Driver.Env.Types ( Hsc(..), HscEnv(..) ) +import GHC.Driver.Env.Types ( Hsc(..), HscEnv(..), HasHscEnv (..) ) import GHC.Runtime.Context import GHC.Runtime.Interpreter.Types (Interp) ===================================== compiler/GHC/Driver/Env/Types.hs ===================================== @@ -3,6 +3,7 @@ module GHC.Driver.Env.Types ( Hsc(..) , HscEnv(..) + , HasHscEnv(..) ) where import GHC.Driver.Errors.Types ( GhcMessage ) @@ -34,6 +35,9 @@ newtype Hsc a = Hsc (HscEnv -> Messages GhcMessage -> IO (a, Messages GhcMessage deriving (Functor, Applicative, Monad, MonadIO) via ReaderT HscEnv (StateT (Messages GhcMessage) IO) +instance HasHscEnv Hsc where + getHscEnv = Hsc $ \e w -> return (e, w) + instance HasDynFlags Hsc where getDynFlags = Hsc $ \e w -> return (hsc_dflags e, w) @@ -109,3 +113,5 @@ data HscEnv -- ^ LLVM configuration cache. } +class HasHscEnv m where + getHscEnv :: m HscEnv ===================================== compiler/GHC/Driver/Main.hs ===================================== @@ -368,9 +368,6 @@ clearDiagnostics = Hsc $ \_ _ -> return ((), emptyMessages) logDiagnostics :: Messages GhcMessage -> Hsc () logDiagnostics w = Hsc $ \_ w0 -> return ((), w0 `unionMessages` w) -getHscEnv :: Hsc HscEnv -getHscEnv = Hsc $ \e w -> return (e, w) - handleWarnings :: Hsc () handleWarnings = do diag_opts <- initDiagOpts <$> getDynFlags ===================================== compiler/GHC/Plugins.hs ===================================== @@ -143,7 +143,7 @@ import Data.Maybe import GHC.Iface.Env ( lookupNameCache ) import GHC.Prelude -import GHC.Utils.Monad ( mapMaybeM ) +import GHC.Utils.Monad ( MonadIO, mapMaybeM ) import GHC.ThToHs ( thRdrNameGuesses ) import GHC.Tc.Utils.Env ( lookupGlobal ) import GHC.Types.Name.Cache ( NameCache ) @@ -178,7 +178,22 @@ instance MonadThings CoreM where -- exactly. Qualified or unqualified TH names will be dynamically bound -- to names in the module being compiled, if possible. Exact TH names -- will be bound to the name they represent, exactly. -thNameToGhcName :: TH.Name -> CoreM (Maybe Name) +-- +-- 'thNameToGhcName' can be used in 'CoreM', 'Hsc' and 'TcM' monads. +-- +-- 'thNameToGhcName' is recommended way to lookup 'Name's in GHC plugins. +-- +-- @ +-- {-# LANGUAGE TemplateHaskellQuotes #-} +-- +-- getNames :: Hsc (Maybe Name, Maybe Name) +-- getNames = do +-- class_Eq <- thNameToGhcName ''Eq +-- fun_eq <- thNameToGhcName '(==) +-- return (classEq, fun_eq) +-- @ +-- +thNameToGhcName :: (MonadIO m, HasHscEnv m) => TH.Name -> m (Maybe Name) thNameToGhcName th_name = do hsc_env <- getHscEnv liftIO $ thNameToGhcNameIO (hsc_NC hsc_env) th_name ===================================== compiler/GHC/StgToByteCode.hs ===================================== @@ -2641,8 +2641,8 @@ runBc hsc_env this_mod mbs (BcM m) instance HasDynFlags BcM where getDynFlags = hsc_dflags <$> getHscEnv -getHscEnv :: BcM HscEnv -getHscEnv = BcM $ \env st -> return (bcm_hsc_env env, st) +instance HasHscEnv BcM where + getHscEnv = BcM $ \env st -> return (bcm_hsc_env env, st) getProfile :: BcM Profile getProfile = targetProfile <$> getDynFlags ===================================== 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 polymorphism 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 ===================================== compiler/GHC/ThToHs.hs ===================================== @@ -915,12 +915,6 @@ cvtPragmaD (OpaqueP nm) srcTxt = SourceText $ fsLit "{-# OPAQUE" ; returnJustLA $ Hs.SigD noExtField $ InlineSig noAnn nm' ip } -cvtPragmaD (SpecialiseP nm ty inline phases) - = do { nm' <- vNameN nm - ; ty' <- cvtSigType ty - ; let ip = cvtInlinePhases inline phases - ; returnJustLA $ Hs.SigD noExtField $ SpecSig noAnn nm' [ty'] ip } - cvtPragmaD (SpecialiseInstP ty) = do { ty' <- cvtSigType ty ; returnJustLA $ Hs.SigD noExtField $ ===================================== configure.ac ===================================== @@ -219,7 +219,7 @@ if test "$WithGhc" = "" then AC_MSG_ERROR([GHC is required.]) fi -MinBootGhcVersion="9.8" +MinBootGhcVersion="9.10" FP_COMPARE_VERSIONS([$GhcVersion],[-lt],[$MinBootGhcVersion], [AC_MSG_ERROR([GHC version $MinBootGhcVersion or later is required to compile GHC.])]) ===================================== libraries/ghc-boot-th/GHC/Boot/TH/Ppr.hs ===================================== @@ -646,13 +646,6 @@ instance Ppr Pragma where <+> text "#-}" ppr (OpaqueP n) = text "{-# OPAQUE" <+> pprName' Applied n <+> text "#-}" - ppr (SpecialiseP n ty inline phases) - = text "{-# SPECIALISE" - <+> maybe empty ppr inline - <+> ppr phases - <+> sep [ pprName' Applied n <+> dcolon - , nest 2 $ ppr ty ] - <+> text "#-}" ppr (SpecialiseEP ty_bndrs tm_bndrs spec_e inline phases) = sep [ text "{-# SPECIALISE" <+> maybe empty ppr inline ===================================== libraries/ghc-internal/src/GHC/Internal/TH/Syntax.hs ===================================== @@ -2115,12 +2115,8 @@ data Pragma = InlineP Name Inline RuleMatch Phases -- 'Inline' and 'RuleMatch'. | OpaqueP Name -- ^ @{ {\-\# OPAQUE T #-} }@ - | SpecialiseP Name Type (Maybe Inline) Phases - -- ^ @{ {\-\# SPECIALISE [INLINE] [phases] nm :: ty #-} }@ - -- - -- NB: this constructor is deprecated and will be removed in GHC 9.18 | SpecialiseEP (Maybe [TyVarBndr ()]) [RuleBndr] Exp (Maybe Inline) Phases - -- ^ @{ {\-\# SPECIALISE [INLINE] [phases] exp #-} }@ + -- ^ @{ {\-\# SPECIALISE [forall t_1 ... t_i]. [forall b_1 ... b_j] [INLINE] [phases] exp #-} }@ | SpecialiseInstP Type -- ^ @{ {\-\# SPECIALISE instance I #-} }@ | RuleP String (Maybe [TyVarBndr ()]) [RuleBndr] Exp Exp Phases ===================================== libraries/template-haskell/Language/Haskell/TH/Lib.hs ===================================== @@ -443,16 +443,14 @@ varStrictType :: Quote m => Name -> m StrictType -> m VarStrictType varStrictType = varBangType -------------------------------------------------------------------------------- --- * Specialisation pragmas (deprecated) +-- * Specialisation pragmas (backwards compatibility) -{-# DEPRECATED pragSpecD "Please use 'pragSpecED' instead. 'pragSpecD' will be removed in GHC 9.18." #-} pragSpecD :: Quote m => Name -> m Type -> Phases -> m Dec pragSpecD n ty phases = do ty1 <- ty pure $ PragmaD $ SpecialiseP n ty1 Nothing phases -{-# DEPRECATED pragSpecInlD "Please use 'pragSpecInlED' instead. 'pragSpecInlD' will be removed in GHC 9.18." #-} pragSpecInlD :: Quote m => Name -> m Type -> Inline -> Phases -> m Dec pragSpecInlD n ty inline phases = do ===================================== libraries/template-haskell/Language/Haskell/TH/Syntax.hs ===================================== @@ -1,4 +1,5 @@ {-# LANGUAGE MagicHash #-} +{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskellQuotes #-} @@ -157,7 +158,7 @@ module Language.Haskell.TH.Syntax ( PatSynType, Phases (..), PkgName (..), - Pragma (..), + Pragma (SpecialiseP, ..), Quasi (..), Range (..), Role (..), @@ -457,3 +458,12 @@ reassociate the tree as necessary. 'InfixT', 'PromotedInfixT, 'ParensE', 'ParensP', or 'ParensT' constructors. -} + +-------------------------------------------------------------------------------- +-- Back-compat for Specialise pragmas + +-- | Old-form specialise pragma @{ {\-\# SPECIALISE [INLINE] [phases] (var :: ty) #-} }@. +-- +-- Subsumed by the more general 'SpecialiseEP' constructor. +pattern SpecialiseP :: Name -> Type -> (Maybe Inline) -> Phases -> Pragma +pattern SpecialiseP nm ty inl phases = SpecialiseEP Nothing [] (SigE (VarE nm) ty) inl phases ===================================== libraries/template-haskell/changelog.md ===================================== @@ -7,16 +7,9 @@ * Introduce `dataToCodeQ` and `liftDataTyped`, typed variants of `dataToExpQ` and `liftData` respectively. - * As part of the implementation of [GHC proposal 493](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0493-sp...), - the ``SpecialiseP`` constructor of `Pragma`, as well as the helper functions - `pragSpecD` and `pragSpecInlD`, have been deprecated. - - They are replaced, respectively, by `SpecialiseEP`, `pragSpecED` and - `pragSpecInlED`. - * Remove the `Language.Haskell.TH.Lib.Internal` module. This module has long been deprecated, and exposes compiler internals. Users should use `Language.Haskell.TH.Lib` instead, which exposes a more stable version of this API. - + * Remove `addrToByteArrayName` and `addrToByteArray` from `Language.Haskell.TH.Syntax`. These were part of the implementation of the `Lift ByteArray` instance and were accidentally exported because this module lacked an explicit export list. They have no usages on Hackage. ## 2.23.0.0 ===================================== testsuite/tests/interface-stability/template-haskell-exports.stdout ===================================== @@ -347,7 +347,7 @@ module Language.Haskell.TH where ppr_list :: [a] -> GHC.Boot.TH.PprLib.Doc {-# MINIMAL ppr #-} type Pragma :: * - data Pragma = InlineP Name Inline RuleMatch Phases | OpaqueP Name | SpecialiseP Name Type (GHC.Internal.Maybe.Maybe Inline) Phases | SpecialiseEP (GHC.Internal.Maybe.Maybe [TyVarBndr ()]) [RuleBndr] Exp (GHC.Internal.Maybe.Maybe Inline) Phases | SpecialiseInstP Type | RuleP GHC.Internal.Base.String (GHC.Internal.Maybe.Maybe [TyVarBndr ()]) [RuleBndr] Exp Exp Phases | AnnP AnnTarget Exp | LineP GHC.Internal.Types.Int GHC.Internal.Base.String | CompleteP [Name] (GHC.Internal.Maybe.Maybe Name) | SCCP Name (GHC.Internal.Maybe.Maybe GHC.Internal.Base.String) + data Pragma = InlineP Name Inline RuleMatch Phases | OpaqueP Name | SpecialiseEP (GHC.Internal.Maybe.Maybe [TyVarBndr ()]) [RuleBndr] Exp (GHC.Internal.Maybe.Maybe Inline) Phases | SpecialiseInstP Type | RuleP GHC.Internal.Base.String (GHC.Internal.Maybe.Maybe [TyVarBndr ()]) [RuleBndr] Exp Exp Phases | AnnP AnnTarget Exp | LineP GHC.Internal.Types.Int GHC.Internal.Base.String | CompleteP [Name] (GHC.Internal.Maybe.Maybe Name) | SCCP Name (GHC.Internal.Maybe.Maybe GHC.Internal.Base.String) type Pred :: * type Pred = Type type PredQ :: * @@ -381,6 +381,7 @@ module Language.Haskell.TH where data SourceUnpackedness = NoSourceUnpackedness | SourceNoUnpack | SourceUnpack type SourceUnpackednessQ :: * type SourceUnpackednessQ = Q SourceUnpackedness + pattern SpecialiseP :: Name -> Type -> GHC.Internal.Maybe.Maybe Inline -> Phases -> Pragma type Specificity :: * data Specificity = SpecifiedSpec | InferredSpec type Stmt :: * @@ -1693,7 +1694,7 @@ module Language.Haskell.TH.Syntax where type PkgName :: * newtype PkgName = PkgName GHC.Internal.Base.String type Pragma :: * - data Pragma = InlineP Name Inline RuleMatch Phases | OpaqueP Name | SpecialiseP Name Type (GHC.Internal.Maybe.Maybe Inline) Phases | SpecialiseEP (GHC.Internal.Maybe.Maybe [TyVarBndr ()]) [RuleBndr] Exp (GHC.Internal.Maybe.Maybe Inline) Phases | SpecialiseInstP Type | RuleP GHC.Internal.Base.String (GHC.Internal.Maybe.Maybe [TyVarBndr ()]) [RuleBndr] Exp Exp Phases | AnnP AnnTarget Exp | LineP GHC.Internal.Types.Int GHC.Internal.Base.String | CompleteP [Name] (GHC.Internal.Maybe.Maybe Name) | SCCP Name (GHC.Internal.Maybe.Maybe GHC.Internal.Base.String) + data Pragma = InlineP Name Inline RuleMatch Phases | OpaqueP Name | SpecialiseEP (GHC.Internal.Maybe.Maybe [TyVarBndr ()]) [RuleBndr] Exp (GHC.Internal.Maybe.Maybe Inline) Phases | SpecialiseInstP Type | RuleP GHC.Internal.Base.String (GHC.Internal.Maybe.Maybe [TyVarBndr ()]) [RuleBndr] Exp Exp Phases | AnnP AnnTarget Exp | LineP GHC.Internal.Types.Int GHC.Internal.Base.String | CompleteP [Name] (GHC.Internal.Maybe.Maybe Name) | SCCP Name (GHC.Internal.Maybe.Maybe GHC.Internal.Base.String) type Pred :: * type Pred = Type type role Q nominal @@ -1748,6 +1749,7 @@ module Language.Haskell.TH.Syntax where data SourceStrictness = NoSourceStrictness | SourceLazy | SourceStrict type SourceUnpackedness :: * data SourceUnpackedness = NoSourceUnpackedness | SourceNoUnpack | SourceUnpack + pattern SpecialiseP :: Name -> Type -> GHC.Internal.Maybe.Maybe Inline -> Phases -> Pragma type Specificity :: * data Specificity = SpecifiedSpec | InferredSpec type Stmt :: * ===================================== 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/-/compare/52ba0a3d432d14765c5a33df3b8597f... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/52ba0a3d432d14765c5a33df3b8597f... You're receiving this email because of your account on gitlab.haskell.org.