Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC Commits: 93fc7265 by sheaf at 2025-11-06T21:33:24-05:00 Correct hasFixedRuntimeRep in matchExpectedFunTys This commit fixes a bug in the representation-polymormorphism check in GHC.Tc.Utils.Unify.matchExpectedFunTys. The problem was that we put the coercion resulting from hasFixedRuntimeRep in the wrong place, leading to the Core Lint error reported in #26528. The change is that we have to be careful when using 'mkWpFun': it expects **both** the expected and actual argument types to have a syntactically fixed RuntimeRep, as explained in Note [WpFun-FRR-INVARIANT] in GHC.Tc.Types.Evidence. On the way, this patch improves some of the commentary relating to other usages of 'mkWpFun' in the compiler, in particular in the view pattern case of 'tc_pat'. No functional changes, but some stylistic changes to make the code more readable, and make it easier to understand how we are upholding the WpFun-FRR-INVARIANT. Fixes #26528 - - - - - 7 changed files: - compiler/GHC/Tc/Gen/Expr.hs - compiler/GHC/Tc/Gen/Pat.hs - compiler/GHC/Tc/Types/Evidence.hs - compiler/GHC/Tc/Utils/Instantiate.hs - compiler/GHC/Tc/Utils/Unify.hs - + testsuite/tests/rep-poly/T26528.hs - testsuite/tests/rep-poly/all.T Changes: ===================================== compiler/GHC/Tc/Gen/Expr.hs ===================================== @@ -957,7 +957,7 @@ tcSynArgE :: CtOrigin -> SyntaxOpType -- ^ shape it is expected to have -> ([TcSigmaTypeFRR] -> [Mult] -> TcM a) -- ^ check the arguments -> TcM (a, HsWrapper) - -- ^ returns a wrapper :: (type of right shape) "->" (type passed in) + -- ^ returns a wrapper :: (type of right shape) ~~> (type passed in) tcSynArgE orig op sigma_ty syn_ty thing_inside = do { (skol_wrap, (result, ty_wrapper)) <- tcSkolemise Shallow GenSigCtxt sigma_ty $ \rho_ty -> @@ -978,10 +978,10 @@ tcSynArgE orig op sigma_ty syn_ty thing_inside ; return (result, mkWpCastN list_co) } go rho_ty (SynFun arg_shape res_shape) - = do { ( match_wrapper -- :: (arg_ty -> res_ty) "->" rho_ty + = do { ( match_wrapper -- :: (arg_ty -> res_ty) ~~> rho_ty , ( ( (result, arg_ty, res_ty, op_mult) - , res_wrapper ) -- :: res_ty_out "->" res_ty - , arg_wrapper1, [], arg_wrapper2 ) ) -- :: arg_ty "->" arg_ty_out + , res_wrapper ) -- :: res_ty_out ~~> res_ty + , arg_wrapper1, [], arg_wrapper2 ) ) -- :: arg_ty ~~> arg_ty_out <- matchExpectedFunTys herald GenSigCtxt 1 (mkCheckExpType rho_ty) $ \ [ExpFunPatTy arg_ty] res_ty -> do { arg_tc_ty <- expTypeToType (scaledThing arg_ty) @@ -1031,7 +1031,7 @@ tcSynArgA :: CtOrigin tcSynArgA orig op sigma_ty arg_shapes res_shape thing_inside = do { (match_wrapper, arg_tys, res_ty) <- matchActualFunTys herald orig (length arg_shapes) sigma_ty - -- match_wrapper :: sigma_ty "->" (arg_tys -> res_ty) + -- match_wrapper :: sigma_ty ~~> (arg_tys -> res_ty) ; ((result, res_wrapper), arg_wrappers) <- tc_syn_args_e (map scaledThing arg_tys) arg_shapes $ \ arg_results arg_res_mults -> tc_syn_arg res_ty res_shape $ \ res_results -> @@ -1061,12 +1061,12 @@ tcSynArgA orig op sigma_ty arg_shapes res_shape thing_inside ; return (result, idHsWrapper) } tc_syn_arg res_ty SynRho thing_inside = do { (inst_wrap, rho_ty) <- topInstantiate orig res_ty - -- inst_wrap :: res_ty "->" rho_ty + -- inst_wrap :: res_ty ~~> rho_ty ; result <- thing_inside [rho_ty] ; return (result, inst_wrap) } tc_syn_arg res_ty SynList thing_inside = do { (inst_wrap, rho_ty) <- topInstantiate orig res_ty - -- inst_wrap :: res_ty "->" rho_ty + -- inst_wrap :: res_ty ~~> rho_ty ; (list_co, elt_ty) <- matchExpectedListTy rho_ty -- list_co :: [elt_ty] ~N rho_ty ; result <- thing_inside [elt_ty] ===================================== compiler/GHC/Tc/Gen/Pat.hs ===================================== @@ -329,7 +329,7 @@ tcPatBndr penv@(PE { pe_ctxt = LetPat { pc_lvl = bind_lvl -- Note [Typechecking pattern bindings] in GHC.Tc.Gen.Bind | Just bndr_id <- sig_fn bndr_name -- There is a signature - = do { wrap <- tc_sub_type penv (scaledThing exp_pat_ty) (idType bndr_id) + = do { wrap <- tcSubTypePat_GenSigCtxt penv (scaledThing exp_pat_ty) (idType bndr_id) -- See Note [Subsumption check at pattern variables] ; traceTc "tcPatBndr(sig)" (ppr bndr_id $$ ppr (idType bndr_id) $$ ppr exp_pat_ty) ; return (wrap, bndr_id) } @@ -376,10 +376,12 @@ newLetBndr LetLclBndr name w ty newLetBndr (LetGblBndr prags) name w ty = addInlinePrags (mkLocalId name w ty) (lookupPragEnv prags name) -tc_sub_type :: PatEnv -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper --- tcSubTypeET with the UserTypeCtxt specialised to GenSigCtxt --- Used during typechecking patterns -tc_sub_type penv t1 t2 = tcSubTypePat (pe_orig penv) GenSigCtxt t1 t2 +-- | A version of 'tcSubTypePat' specialised to 'GenSigCtxt'. +-- +-- Used during typechecking of patterns. +tcSubTypePat_GenSigCtxt :: PatEnv -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper +tcSubTypePat_GenSigCtxt penv t1 t2 = + tcSubTypePat (pe_orig penv) GenSigCtxt t1 t2 {- Note [Subsumption check at pattern variables] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -618,111 +620,123 @@ tc_pat :: Scaled ExpSigmaTypeFRR -> Checker (Pat GhcRn) (Pat GhcTc) -- ^ Translated pattern -tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of - - VarPat x (L l name) -> do - { (wrap, id) <- tcPatBndr penv name pat_ty - ; res <- tcCheckUsage name (scaledMult pat_ty) $ - tcExtendIdEnv1 name id thing_inside - ; pat_ty <- readExpType (scaledThing pat_ty) - ; return (mkHsWrapPat wrap (VarPat x (L l id)) pat_ty, res) } - - ParPat x pat -> do - { (pat', res) <- tc_lpat pat_ty penv pat thing_inside - ; return (ParPat x pat', res) } - - BangPat x pat -> do - { (pat', res) <- tc_lpat pat_ty penv pat thing_inside - ; return (BangPat x pat', res) } - - OrPat _ pats -> do -- See Note [Implementation of OrPatterns], Typechecker (1) - { let pats_list = NE.toList pats - ; (pats_list', (res, pat_ct)) <- tc_lpats (map (const pat_ty) pats_list) penv pats_list (captureConstraints thing_inside) - ; let pats' = NE.fromList pats_list' -- tc_lpats preserves non-emptiness - ; emitConstraints pat_ct - -- captureConstraints/extendConstraints: - -- like in Note [Hopping the LIE in lazy patterns] - ; pat_ty <- expTypeToType (scaledThing pat_ty) - ; return (OrPat pat_ty pats', res) } - - LazyPat x pat -> do - { checkManyPattern LazyPatternReason (noLocA ps_pat) pat_ty - ; (pat', (res, pat_ct)) - <- tc_lpat pat_ty (makeLazy penv) pat $ - captureConstraints thing_inside - -- Ignore refined penv', revert to penv - - ; emitConstraints pat_ct - -- captureConstraints/extendConstraints: - -- see Note [Hopping the LIE in lazy patterns] - - -- Check that the expected pattern type is itself lifted - ; pat_ty <- readExpType (scaledThing pat_ty) - ; _ <- unifyType Nothing (typeKind pat_ty) liftedTypeKind - - ; return ((LazyPat x pat'), res) } - - WildPat _ -> do - { checkManyPattern OtherPatternReason (noLocA ps_pat) pat_ty - ; res <- thing_inside - ; pat_ty <- expTypeToType (scaledThing pat_ty) - ; return (WildPat pat_ty, res) } - - AsPat x (L nm_loc name) pat -> do - { checkManyPattern OtherPatternReason (noLocA ps_pat) pat_ty - ; (wrap, bndr_id) <- setSrcSpanA nm_loc (tcPatBndr penv name pat_ty) - ; (pat', res) <- tcExtendIdEnv1 name bndr_id $ - tc_lpat (pat_ty `scaledSet`(mkCheckExpType $ idType bndr_id)) - penv pat thing_inside - -- NB: if we do inference on: - -- \ (y@(x::forall a. a->a)) = e - -- we'll fail. The as-pattern infers a monotype for 'y', which then - -- fails to unify with the polymorphic type for 'x'. This could - -- perhaps be fixed, but only with a bit more work. - -- - -- If you fix it, don't forget the bindInstsOfPatIds! - ; pat_ty <- readExpType (scaledThing pat_ty) - ; return (mkHsWrapPat wrap (AsPat x (L nm_loc bndr_id) pat') pat_ty, res) } - - ViewPat _ expr pat -> do - { checkManyPattern ViewPatternReason (noLocA ps_pat) pat_ty - -- - -- It should be possible to have view patterns at linear (or otherwise - -- non-Many) multiplicity. But it is not clear at the moment what - -- restriction need to be put in place, if any, for linear view - -- patterns to desugar to type-correct Core. - - ; (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_co1, Scaled _mult inf_arg_ty, inf_res_sigma) - <- matchActualFunTy herald (Just . HsExprRnThing $ unLoc expr) (1,expr_rho) expr_rho - -- See Note [View patterns and polymorphism] - -- 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 - -- expr_wrap2 :: pat_ty "->" inf_arg_ty - - -- Pattern must have inf_res_sigma - ; (pat', res) <- tc_lpat (pat_ty `scaledSet` mkCheckExpType inf_res_sigma) penv pat thing_inside - - ; let Scaled w h_pat_ty = pat_ty - ; 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. - - expr_wrap = expr_wrap2' <.> mkWpCastN expr_co1 - - ; return $ (ViewPat pat_ty (mkLHsWrap expr_wrap expr') pat', res) } +tc_pat scaled_exp_pat_ty@(Scaled w_pat exp_pat_ty) penv ps_pat thing_inside = + + case ps_pat of + + VarPat x (L l name) -> do + { (wrap, id) <- tcPatBndr penv name scaled_exp_pat_ty + ; res <- tcCheckUsage name w_pat $ tcExtendIdEnv1 name id thing_inside + ; pat_ty <- readExpType exp_pat_ty + ; return (mkHsWrapPat wrap (VarPat x (L l id)) pat_ty, res) } + + ParPat x pat -> do + { (pat', res) <- tc_lpat scaled_exp_pat_ty penv pat thing_inside + ; return (ParPat x pat', res) } + + BangPat x pat -> do + { (pat', res) <- tc_lpat scaled_exp_pat_ty penv pat thing_inside + ; return (BangPat x pat', res) } + + OrPat _ pats -> do -- See Note [Implementation of OrPatterns], Typechecker (1) + { let pats_list = NE.toList pats + pat_exp_tys = map (const scaled_exp_pat_ty) pats_list + ; (pats_list', (res, pat_ct)) <- tc_lpats pat_exp_tys penv pats_list (captureConstraints thing_inside) + ; let pats' = NE.fromList pats_list' -- tc_lpats preserves non-emptiness + ; emitConstraints pat_ct + -- captureConstraints/extendConstraints: + -- like in Note [Hopping the LIE in lazy patterns] + ; pat_ty <- expTypeToType exp_pat_ty + ; return (OrPat pat_ty pats', res) } + + LazyPat x pat -> do + { checkManyPattern LazyPatternReason (noLocA ps_pat) scaled_exp_pat_ty + ; (pat', (res, pat_ct)) + <- tc_lpat scaled_exp_pat_ty (makeLazy penv) pat $ + captureConstraints thing_inside + -- Ignore refined penv', revert to penv + + ; emitConstraints pat_ct + -- captureConstraints/extendConstraints: + -- see Note [Hopping the LIE in lazy patterns] + + -- Check that the expected pattern type is itself lifted + ; pat_ty <- readExpType exp_pat_ty + ; _ <- unifyType Nothing (typeKind pat_ty) liftedTypeKind + + ; return ((LazyPat x pat'), res) } + + WildPat _ -> do + { checkManyPattern OtherPatternReason (noLocA ps_pat) scaled_exp_pat_ty + ; res <- thing_inside + ; pat_ty <- expTypeToType exp_pat_ty + ; return (WildPat pat_ty, res) } + + AsPat x (L nm_loc name) pat -> do + { checkManyPattern OtherPatternReason (noLocA ps_pat) scaled_exp_pat_ty + ; (wrap, bndr_id) <- setSrcSpanA nm_loc (tcPatBndr penv name scaled_exp_pat_ty) + ; (pat', res) <- tcExtendIdEnv1 name bndr_id $ + tc_lpat (Scaled w_pat (mkCheckExpType $ idType bndr_id)) + penv pat thing_inside + -- NB: if we do inference on: + -- \ (y@(x::forall a. a->a)) = e + -- we'll fail. The as-pattern infers a monotype for 'y', which then + -- fails to unify with the polymorphic type for 'x'. This could + -- perhaps be fixed, but only with a bit more work. + -- + -- If you fix it, don't forget the bindInstsOfPatIds! + ; pat_ty <- readExpType exp_pat_ty + ; return (mkHsWrapPat wrap (AsPat x (L nm_loc bndr_id) pat') pat_ty, res) } + + ViewPat _ view_expr inner_pat -> do + + -- The pattern is a view pattern, 'pat = (view_expr -> inner_pat)'. + -- First infer the type of 'view_expr'; the overall type of the pattern + -- is the argument type of 'view_expr', and the inner pattern type is + -- checked against the result type of 'view_expr'. + + { checkManyPattern ViewPatternReason (noLocA ps_pat) scaled_exp_pat_ty + -- It should be possible to have view patterns at linear (or otherwise + -- non-Many) multiplicity. But it is not clear at the moment what + -- restrictions need to be put in place, if any, for linear view + -- patterns to desugar to type-correct Core. + + -- Infer the type of 'view_expr'. + ; (view_expr', view_expr_rho) <- tcInferExpr IIF_ShallowRho view_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 + + -- 'view_expr' must be a function; expose its argument/result types + -- using 'matchActualFunTy'. + ; let herald = ExpectedFunTyViewPat $ unLoc view_expr + ; (view_expr_co1, Scaled _mult view_arg_ty, view_res_ty) + <- matchActualFunTy herald (Just . HsExprRnThing $ unLoc view_expr) + (1, view_expr_rho) view_expr_rho + -- See Note [View patterns and polymorphism] + -- view_expr_co1 :: view_expr_rho ~~> (view_arg_ty -> view_res_ty) + + -- Check that the overall pattern's type is more polymorphic than + -- the view function argument type. + ; view_expr_wrap2 <- tcSubTypePat_GenSigCtxt penv exp_pat_ty view_arg_ty + -- view_expr_wrap2 :: pat_ty ~~> view_arg_ty + + -- The inner pattern must have type 'view_res_ty'. + ; (inner_pat', res) <- tc_lpat (Scaled w_pat (mkCheckExpType view_res_ty)) penv inner_pat thing_inside + + ; pat_ty <- readExpType exp_pat_ty + ; let view_expr_wrap2' = + mkWpFun view_expr_wrap2 idHsWrapper + (Scaled w_pat pat_ty) view_res_ty + -- view_expr_wrap2' :: (view_arg_ty -> view_res_ty) + -- ~~> (pat_ty -> view_res_ty) + -- This satisfies WpFun-FRR-INVARIANT: + -- 'view_arg_ty' was returned by matchActualFunTy, hence FRR + -- 'pat_ty' was passed in and is an 'ExpSigmaTypeFRR' + + view_expr_wrap = view_expr_wrap2' <.> mkWpCastN view_expr_co1 + + ; return $ (ViewPat pat_ty (mkLHsWrap view_expr_wrap view_expr') inner_pat', res) } {- Note [View patterns and polymorphism] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -748,93 +762,91 @@ Another example is #26331. -- Type signatures in patterns -- See Note [Pattern coercions] below - SigPat _ pat sig_ty -> do - { (inner_ty, tv_binds, wcs, wrap) <- tcPatSig (inPatBind penv) - sig_ty (scaledThing pat_ty) - -- Using tcExtendNameTyVarEnv is appropriate here - -- because we're not really bringing fresh tyvars into scope. - -- We're *naming* existing tyvars. Note that it is OK for a tyvar - -- from an outer scope to mention one of these tyvars in its kind. - ; (pat', res) <- tcExtendNameTyVarEnv wcs $ - tcExtendNameTyVarEnv tv_binds $ - tc_lpat (pat_ty `scaledSet` mkCheckExpType inner_ty) penv pat thing_inside - ; pat_ty <- readExpType (scaledThing pat_ty) - ; return (mkHsWrapPat wrap (SigPat inner_ty pat' sig_ty) pat_ty, res) } + SigPat _ pat sig_ty -> do + { (inner_ty, tv_binds, wcs, wrap) <- + tcPatSig (inPatBind penv) sig_ty exp_pat_ty + -- Using tcExtendNameTyVarEnv is appropriate here + -- because we're not really bringing fresh tyvars into scope. + -- We're *naming* existing tyvars. Note that it is OK for a tyvar + -- from an outer scope to mention one of these tyvars in its kind. + ; (pat', res) <- tcExtendNameTyVarEnv wcs $ + tcExtendNameTyVarEnv tv_binds $ + tc_lpat (Scaled w_pat $ mkCheckExpType inner_ty) penv pat thing_inside + ; pat_ty <- readExpType exp_pat_ty + ; return (mkHsWrapPat wrap (SigPat inner_ty pat' sig_ty) pat_ty, res) } ------------------------ -- Lists, tuples, arrays -- Necessarily a built-in list pattern, not an overloaded list pattern. -- See Note [Desugaring overloaded list patterns]. - ListPat _ pats -> do - { (coi, elt_ty) <- matchExpectedPatTy matchExpectedListTy penv (scaledThing pat_ty) - ; (pats', res) <- tcMultiple (tc_lpat (pat_ty `scaledSet` mkCheckExpType elt_ty)) - penv pats thing_inside - ; pat_ty <- readExpType (scaledThing pat_ty) - ; return (mkHsWrapPat coi - (ListPat elt_ty pats') pat_ty, res) } - - TuplePat _ pats boxity -> do - { let arity = length pats - tc = tupleTyCon boxity arity - -- NB: tupleTyCon does not flatten 1-tuples - -- See Note [Don't flatten tuples from HsSyn] in GHC.Core.Make - ; checkTupSize arity - ; (coi, arg_tys) <- matchExpectedPatTy (matchExpectedTyConApp tc) - penv (scaledThing pat_ty) - -- Unboxed tuples have RuntimeRep vars, which we discard: - -- See Note [Unboxed tuple RuntimeRep vars] in GHC.Core.TyCon - ; let con_arg_tys = case boxity of Unboxed -> drop arity arg_tys - Boxed -> arg_tys - ; (pats', res) <- tc_lpats (map (scaledSet pat_ty . mkCheckExpType) con_arg_tys) + ListPat _ pats -> do + { (coi, elt_ty) <- matchExpectedPatTy matchExpectedListTy penv exp_pat_ty + ; (pats', res) <- tcMultiple (tc_lpat (Scaled w_pat $ mkCheckExpType elt_ty)) penv pats thing_inside - - ; dflags <- getDynFlags - - -- Under flag control turn a pattern (x,y,z) into ~(x,y,z) - -- so that we can experiment with lazy tuple-matching. - -- This is a pretty odd place to make the switch, but - -- it was easy to do. - ; let - unmangled_result = TuplePat con_arg_tys pats' boxity - -- pat_ty /= pat_ty iff coi /= IdCo - possibly_mangled_result - | gopt Opt_IrrefutableTuples dflags && - isBoxed boxity = LazyPat noExtField (noLocA unmangled_result) - | otherwise = unmangled_result - - ; pat_ty <- readExpType (scaledThing pat_ty) - ; massert (con_arg_tys `equalLength` pats) -- Syntactically enforced - ; return (mkHsWrapPat coi possibly_mangled_result pat_ty, res) - } - - SumPat _ pat alt arity -> do - { let tc = sumTyCon arity - ; (coi, arg_tys) <- matchExpectedPatTy (matchExpectedTyConApp tc) - penv (scaledThing pat_ty) - ; -- Drop levity vars, we don't care about them here - let con_arg_tys = drop arity arg_tys - ; (pat', res) <- tc_lpat (pat_ty `scaledSet` mkCheckExpType (con_arg_tys `getNth` (alt - 1))) - penv pat thing_inside - ; pat_ty <- readExpType (scaledThing pat_ty) - ; return (mkHsWrapPat coi (SumPat con_arg_tys pat' alt arity) pat_ty - , res) - } + ; pat_ty <- readExpType exp_pat_ty + ; return (mkHsWrapPat coi + (ListPat elt_ty pats') pat_ty, res) } + + TuplePat _ pats boxity -> do + { let arity = length pats + tc = tupleTyCon boxity arity + -- NB: tupleTyCon does not flatten 1-tuples + -- See Note [Don't flatten tuples from HsSyn] in GHC.Core.Make + ; checkTupSize arity + ; (coi, arg_tys) <- matchExpectedPatTy (matchExpectedTyConApp tc) penv exp_pat_ty + -- Unboxed tuples have RuntimeRep vars, which we discard: + -- See Note [Unboxed tuple RuntimeRep vars] in GHC.Core.TyCon + ; let con_arg_tys = case boxity of Unboxed -> drop arity arg_tys + Boxed -> arg_tys + ; (pats', res) <- tc_lpats (map (Scaled w_pat . mkCheckExpType) con_arg_tys) + penv pats thing_inside + + ; dflags <- getDynFlags + + -- Under flag control turn a pattern (x,y,z) into ~(x,y,z) + -- so that we can experiment with lazy tuple-matching. + -- This is a pretty odd place to make the switch, but + -- it was easy to do. + ; let + unmangled_result = TuplePat con_arg_tys pats' boxity + -- pat_ty /= pat_ty iff coi /= IdCo + possibly_mangled_result + | gopt Opt_IrrefutableTuples dflags && + isBoxed boxity = LazyPat noExtField (noLocA unmangled_result) + | otherwise = unmangled_result + + ; pat_ty <- readExpType exp_pat_ty + ; massert (con_arg_tys `equalLength` pats) -- Syntactically enforced + ; return (mkHsWrapPat coi possibly_mangled_result pat_ty, res) + } + + SumPat _ pat alt arity -> do + { let tc = sumTyCon arity + ; (coi, arg_tys) <- matchExpectedPatTy (matchExpectedTyConApp tc) penv exp_pat_ty + ; -- Drop levity vars, we don't care about them here + let con_arg_tys = drop arity arg_tys + ; (pat', res) <- tc_lpat (Scaled w_pat $ mkCheckExpType (con_arg_tys `getNth` (alt - 1))) + penv pat thing_inside + ; pat_ty <- readExpType exp_pat_ty + ; return (mkHsWrapPat coi (SumPat con_arg_tys pat' alt arity) pat_ty + , res) + } ------------------------ -- Data constructors - ConPat _ con arg_pats -> - tcConPat penv con pat_ty arg_pats thing_inside + ConPat _ con arg_pats -> + tcConPat penv con scaled_exp_pat_ty arg_pats thing_inside ------------------------ -- Literal patterns - LitPat x simple_lit -> do - { let lit_ty = hsLitType simple_lit - ; wrap <- tc_sub_type penv (scaledThing pat_ty) lit_ty - ; res <- thing_inside - ; pat_ty <- readExpType (scaledThing pat_ty) - ; return ( mkHsWrapPat wrap (LitPat x (convertLit simple_lit)) pat_ty - , res) } + LitPat x simple_lit -> do + { let lit_ty = hsLitType simple_lit + ; wrap <- tcSubTypePat_GenSigCtxt penv exp_pat_ty lit_ty + ; res <- thing_inside + ; pat_ty <- readExpType exp_pat_ty + ; return ( mkHsWrapPat wrap (LitPat x (convertLit simple_lit)) pat_ty + , res) } ------------------------ -- Overloaded patterns: n, and n+k @@ -854,31 +866,31 @@ Another example is #26331. -- where lit_ty is the type of the overloaded literal 5. -- -- When there is no negation, neg_lit_ty and lit_ty are the same - NPat _ (L l over_lit) mb_neg eq -> do - { checkManyPattern OtherPatternReason (noLocA ps_pat) pat_ty - -- It may be possible to refine linear pattern so that they work in - -- linear environments. But it is not clear how useful this is. - ; let orig = LiteralOrigin over_lit - ; ((lit', mb_neg'), eq') - <- tcSyntaxOp orig eq [SynType (scaledThing pat_ty), SynAny] - (mkCheckExpType boolTy) $ - \ [neg_lit_ty] _ -> - let new_over_lit lit_ty = newOverloadedLit over_lit - (mkCheckExpType lit_ty) - in case mb_neg of - Nothing -> (, Nothing) <$> new_over_lit neg_lit_ty - Just neg -> -- Negative literal - -- The 'negate' is re-mappable syntax - second Just <$> - (tcSyntaxOp orig neg [SynRho] (mkCheckExpType neg_lit_ty) $ - \ [lit_ty] _ -> new_over_lit lit_ty) - -- applied to a closed literal: linearity doesn't matter as - -- literals are typed in an empty environment, hence have - -- all multiplicities. - - ; res <- thing_inside - ; pat_ty <- readExpType (scaledThing pat_ty) - ; return (NPat pat_ty (L l lit') mb_neg' eq', res) } + NPat _ (L l over_lit) mb_neg eq -> do + { checkManyPattern OtherPatternReason (noLocA ps_pat) scaled_exp_pat_ty + -- It may be possible to refine linear pattern so that they work in + -- linear environments. But it is not clear how useful this is. + ; let orig = LiteralOrigin over_lit + ; ((lit', mb_neg'), eq') + <- tcSyntaxOp orig eq [SynType exp_pat_ty, SynAny] + (mkCheckExpType boolTy) $ + \ [neg_lit_ty] _ -> + let new_over_lit lit_ty = newOverloadedLit over_lit + (mkCheckExpType lit_ty) + in case mb_neg of + Nothing -> (, Nothing) <$> new_over_lit neg_lit_ty + Just neg -> -- Negative literal + -- The 'negate' is re-mappable syntax + second Just <$> + (tcSyntaxOp orig neg [SynRho] (mkCheckExpType neg_lit_ty) $ + \ [lit_ty] _ -> new_over_lit lit_ty) + -- applied to a closed literal: linearity doesn't matter as + -- literals are typed in an empty environment, hence have + -- all multiplicities. + + ; res <- thing_inside + ; pat_ty <- readExpType exp_pat_ty + ; return (NPat pat_ty (L l lit') mb_neg' eq', res) } {- Note [NPlusK patterns] @@ -904,68 +916,67 @@ AST is used for the subtraction operation. -} -- See Note [NPlusK patterns] - NPlusKPat _ (L nm_loc name) - (L loc lit) _ ge minus -> do - { checkManyPattern OtherPatternReason (noLocA ps_pat) pat_ty - ; let pat_exp_ty = scaledThing pat_ty - orig = LiteralOrigin lit - ; (lit1', ge') - <- tcSyntaxOp orig ge [SynType pat_exp_ty, SynRho] - (mkCheckExpType boolTy) $ - \ [lit1_ty] _ -> - newOverloadedLit lit (mkCheckExpType lit1_ty) - ; ((lit2', minus_wrap, bndr_id), minus') - <- tcSyntaxOpGen orig minus [SynType pat_exp_ty, SynRho] SynAny $ - \ [lit2_ty, var_ty] _ -> - do { lit2' <- newOverloadedLit lit (mkCheckExpType lit2_ty) - ; (wrap, bndr_id) <- setSrcSpanA nm_loc $ - tcPatBndr penv name (unrestricted $ mkCheckExpType var_ty) - -- co :: var_ty ~ idType bndr_id - - -- minus_wrap is applicable to minus' - ; return (lit2', wrap, bndr_id) } - - ; pat_ty <- readExpType pat_exp_ty - - -- The Report says that n+k patterns must be in Integral - -- but it's silly to insist on this in the RebindableSyntax case - ; unlessM (xoptM LangExt.RebindableSyntax) $ - do { icls <- tcLookupClass integralClassName - ; instStupidTheta orig [mkClassPred icls [pat_ty]] } - - ; res <- tcExtendIdEnv1 name bndr_id thing_inside - - ; let minus'' = case minus' of - NoSyntaxExprTc -> pprPanic "tc_pat NoSyntaxExprTc" (ppr minus') - -- this should be statically avoidable - -- Case (3) from Note [NoSyntaxExpr] in "GHC.Hs.Expr" - SyntaxExprTc { syn_expr = minus'_expr - , syn_arg_wraps = minus'_arg_wraps - , syn_res_wrap = minus'_res_wrap } - -> SyntaxExprTc { syn_expr = minus'_expr - , syn_arg_wraps = minus'_arg_wraps - , syn_res_wrap = minus_wrap <.> minus'_res_wrap } - -- Oy. This should really be a record update, but - -- we get warnings if we try. #17783 - pat' = NPlusKPat pat_ty (L nm_loc bndr_id) (L loc lit1') lit2' - ge' minus'' - ; return (pat', res) } + NPlusKPat _ (L nm_loc name) + (L loc lit) _ ge minus -> do + { checkManyPattern OtherPatternReason (noLocA ps_pat) scaled_exp_pat_ty + ; let orig = LiteralOrigin lit + ; (lit1', ge') + <- tcSyntaxOp orig ge [SynType exp_pat_ty, SynRho] + (mkCheckExpType boolTy) $ + \ [lit1_ty] _ -> + newOverloadedLit lit (mkCheckExpType lit1_ty) + ; ((lit2', minus_wrap, bndr_id), minus') + <- tcSyntaxOpGen orig minus [SynType exp_pat_ty, SynRho] SynAny $ + \ [lit2_ty, var_ty] _ -> + do { lit2' <- newOverloadedLit lit (mkCheckExpType lit2_ty) + ; (wrap, bndr_id) <- setSrcSpanA nm_loc $ + tcPatBndr penv name (unrestricted $ mkCheckExpType var_ty) + -- co :: var_ty ~ idType bndr_id + + -- minus_wrap is applicable to minus' + ; return (lit2', wrap, bndr_id) } + + ; pat_ty <- readExpType exp_pat_ty + + -- The Report says that n+k patterns must be in Integral + -- but it's silly to insist on this in the RebindableSyntax case + ; unlessM (xoptM LangExt.RebindableSyntax) $ + do { icls <- tcLookupClass integralClassName + ; instStupidTheta orig [mkClassPred icls [pat_ty]] } + + ; res <- tcExtendIdEnv1 name bndr_id thing_inside + + ; let minus'' = case minus' of + NoSyntaxExprTc -> pprPanic "tc_pat NoSyntaxExprTc" (ppr minus') + -- this should be statically avoidable + -- Case (3) from Note [NoSyntaxExpr] in "GHC.Hs.Expr" + SyntaxExprTc { syn_expr = minus'_expr + , syn_arg_wraps = minus'_arg_wraps + , syn_res_wrap = minus'_res_wrap } + -> SyntaxExprTc { syn_expr = minus'_expr + , syn_arg_wraps = minus'_arg_wraps + , syn_res_wrap = minus_wrap <.> minus'_res_wrap } + -- Oy. This should really be a record update, but + -- we get warnings if we try. #17783 + pat' = NPlusKPat pat_ty (L nm_loc bndr_id) (L loc lit1') lit2' + ge' minus'' + ; return (pat', res) } -- Here we get rid of it and add the finalizers to the global environment. -- See Note [Delaying modFinalizers in untyped splices] in GHC.Rename.Splice. - SplicePat (HsUntypedSpliceTop mod_finalizers pat) _ -> do + SplicePat (HsUntypedSpliceTop mod_finalizers pat) _ -> do { addModFinalizersWithLclEnv mod_finalizers - ; tc_pat pat_ty penv pat thing_inside } + ; tc_pat scaled_exp_pat_ty penv pat thing_inside } - SplicePat (HsUntypedSpliceNested _) _ -> panic "tc_pat: nested splice in splice pat" + SplicePat (HsUntypedSpliceNested _) _ -> panic "tc_pat: nested splice in splice pat" - EmbTyPat _ _ -> failWith TcRnIllegalTypePattern + EmbTyPat _ _ -> failWith TcRnIllegalTypePattern - InvisPat _ _ -> panic "tc_pat: invisible pattern appears recursively in the pattern" + InvisPat _ _ -> panic "tc_pat: invisible pattern appears recursively in the pattern" - XPat (HsPatExpanded lpat rpat) -> do - { (rpat', res) <- tc_pat pat_ty penv rpat thing_inside - ; return (XPat $ ExpansionPat lpat rpat', res) } + XPat (HsPatExpanded lpat rpat) -> do + { (rpat', res) <- tc_pat scaled_exp_pat_ty penv rpat thing_inside + ; return (XPat $ ExpansionPat lpat rpat', res) } {- Note [Hopping the LIE in lazy patterns] @@ -1295,7 +1306,7 @@ tcPatSynPat (L con_span con_name) pat_syn pat_ty penv arg_pats thing_inside ; (univ_ty_args, ex_ty_args, val_arg_pats) <- splitConTyArgs con_like arg_pats - ; wrap <- tc_sub_type penv (scaledThing pat_ty) ty' + ; wrap <- tcSubTypePat_GenSigCtxt penv (scaledThing pat_ty) ty' ; traceTc "tcPatSynPat" $ vcat [ text "Pat syn:" <+> ppr pat_syn @@ -1405,8 +1416,9 @@ matchExpectedConTy :: PatEnv -- In the case of a data family, this would -- mention the /family/ TyCon -> TcM (HsWrapper, [TcSigmaType]) --- See Note [Matching constructor patterns] --- Returns a wrapper : pat_ty "->" T ty1 ... tyn +-- ^ See Note [Matching constructor patterns] +-- +-- Returns a wrapper : pat_ty ~~> T ty1 ... tyn matchExpectedConTy (PE { pe_orig = orig }) data_tc exp_pat_ty | Just (fam_tc, fam_args, co_tc) <- tyConFamInstSig_maybe data_tc -- Comments refer to Note [Matching constructor patterns] ===================================== compiler/GHC/Tc/Types/Evidence.hs ===================================== @@ -197,29 +197,29 @@ that it is a no-op. Here's our solution: * we /must/ optimise subtype-HsWrappers (that's the point of this Note!) * there is little point in attempting to optimise any other HsWrappers -Note [WpFun-RR-INVARIANT] -~~~~~~~~~~~~~~~~~~~~~~~~~ +Note [WpFun-FRR-INVARIANT] +~~~~~~~~~~~~~~~~~~~~~~~~~~ Given wrap = WpFun wrap1 wrap2 sty1 ty2 where: wrap1 :: exp_arg ~~> act_arg wrap2 :: act_res ~~> exp_res wrap :: (act_arg -> act_res) ~~> (exp_arg -> exp_res) we have - WpFun-RR-INVARIANT: + WpFun-FRR-INVARIANT: the input (exp_arg) and output (act_arg) types of `wrap1` both have a fixed runtime-rep Reason: We desugar wrap[e] into \(x:exp_arg). wrap2[ e wrap1[x] ] -And then, because of Note [Representation polymorphism invariants], we need: +And then, because of Note [Representation polymorphism invariants]: * `exp_arg` must have a fixed runtime rep, so that lambda obeys the the FRR rules * `act_arg` must have a fixed runtime rep, - so the that application (e wrap1[x]) obeys the FRR tules + so that the application (e wrap1[x]) obeys the FRR rules -Hence WpFun-INVARIANT. +Hence WpFun-FRR-INVARIANT. -} data HsWrapper @@ -246,7 +246,7 @@ data HsWrapper -- (WpFun wrap1 wrap2 (w, t1) t2)[e] = \(x:_w exp_arg). wrap2[ e wrap1[x] ] -- -- INVARIANT: both input and output types of `wrap1` have a fixed runtime-rep - -- See Note [WpFun-RR-INVARIANT] + -- See Note [WpFun-FRR-INVARIANT] -- -- Typing rules: -- If e :: act_arg -> act_res @@ -319,7 +319,7 @@ mkWpFun :: HsWrapper -> HsWrapper -- ^ Smart constructor for `WpFun` -- Just removes clutter and optimises some common cases. -- --- PRECONDITION: same as Note [WpFun-RR-INVARIANT] +-- PRECONDITION: same as Note [WpFun-FRR-INVARIANT] -- -- Unfortunately, we can't check PRECONDITION with an assertion here, because of -- [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep] in GHC.Tc.Utils.Concrete. ===================================== compiler/GHC/Tc/Utils/Instantiate.hs ===================================== @@ -277,7 +277,7 @@ skolemiseRequired skolem_info n_req sigma topInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType) -- Instantiate outer invisible binders (both Inferred and Specified) -- If top_instantiate ty = (wrap, inner_ty) --- then wrap :: inner_ty "->" ty +-- then wrap :: inner_ty ~~> ty -- NB: returns a type with no (=>), -- and no invisible forall at the top topInstantiate orig sigma ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -66,7 +66,6 @@ module GHC.Tc.Utils.Unify ( import GHC.Prelude import GHC.Hs - import GHC.Tc.Errors.Types ( ErrCtxtMsg(..) ) import GHC.Tc.Errors.Ppr ( pprErrCtxtMsg ) import GHC.Tc.Utils.Concrete @@ -256,24 +255,24 @@ matchActualFunTys :: ExpectedFunTyOrigin -- ^ See Note [Herald for matchExpected -- and res_ty is a RhoType -- NB: the returned type is top-instantiated; it's a RhoType matchActualFunTys herald ct_orig n_val_args_wanted top_ty - = go n_val_args_wanted [] top_ty + = go n_val_args_wanted top_ty where - go n so_far fun_ty + go n fun_ty | not (isRhoTy fun_ty) = do { (wrap1, rho) <- topInstantiate ct_orig fun_ty - ; (wrap2, arg_tys, res_ty) <- go n so_far rho + ; (wrap2, arg_tys, res_ty) <- go n rho ; return (wrap2 <.> wrap1, arg_tys, res_ty) } - go 0 _ fun_ty = return (idHsWrapper, [], fun_ty) + go 0 fun_ty = return (idHsWrapper, [], fun_ty) - go n so_far fun_ty - = do { (co1, arg_ty1, res_ty1) <- matchActualFunTy herald Nothing - (n_val_args_wanted, top_ty) fun_ty - ; (wrap_res, arg_tys, res_ty) <- go (n-1) (arg_ty1:so_far) res_ty1 - ; let wrap_fun2 = mkWpFun idHsWrapper wrap_res arg_ty1 res_ty - -- NB: arg_ty1 comes from matchActualFunTy, so it has - -- a syntactically fixed RuntimeRep - ; return (wrap_fun2 <.> mkWpCastN co1, arg_ty1:arg_tys, res_ty) } + go n fun_ty + = do { (co1, arg1_ty_frr, res_ty1) <- + matchActualFunTy herald Nothing (n_val_args_wanted, top_ty) fun_ty + ; (wrap_res, arg_tys, res_ty) <- go (n-1) res_ty1 + ; let wrap_fun2 = mkWpFun idHsWrapper wrap_res arg1_ty_frr res_ty + -- This call to mkWpFun satisfies WpFun-FRR-INVARIANT: + -- 'arg1_ty_frr' comes from matchActualFunTy, so is FRR. + ; return (wrap_fun2 <.> mkWpCastN co1, arg1_ty_frr:arg_tys, res_ty) } {- ************************************************************************ @@ -866,12 +865,30 @@ matchExpectedFunTys herald ctx arity (Check top_ty) thing_inside = assert (isVisibleFunArg af) $ do { let arg_pos = arity - n_req + 1 -- 1 for the first argument etc ; (arg_co, arg_ty_frr) <- hasFixedRuntimeRep (FRRExpectedFunTy herald arg_pos) arg_ty - ; let arg_sty_frr = Scaled mult arg_ty_frr - ; (wrap_res, result) <- check (n_req - 1) - (mkCheckExpFunPatTy arg_sty_frr : rev_pat_tys) + ; let scaled_arg_ty_frr = Scaled mult arg_ty_frr + ; (res_wrap, result) <- check (n_req - 1) + (mkCheckExpFunPatTy scaled_arg_ty_frr : rev_pat_tys) res_ty - ; let wrap_arg = mkWpCastN arg_co - fun_wrap = mkWpFun wrap_arg wrap_res arg_sty_frr res_ty + + -- arg_co :: arg_ty ~ arg_ty_frr + -- res_wrap :: act_res_ty ~~> res_ty + ; let fun_wrap1 -- :: (arg_ty_frr -> act_res_ty) ~~> (arg_ty_frr -> res_ty) + = mkWpFun idHsWrapper res_wrap scaled_arg_ty_frr res_ty + -- Satisfies WpFun-FRR-INVARIANT because arg_sty_frr is FRR + + fun_wrap2 -- :: (arg_ty_frr -> res_ty) ~~> (arg_ty -> res_ty) + = mkWpCastN (mkFunCo Nominal af (mkNomReflCo mult) (mkSymCo arg_co) (mkNomReflCo res_ty)) + + fun_wrap -- :: (arg_ty_frr -> act_res_ty) ~~> (arg_ty -> res_ty) + = fun_wrap2 <.> fun_wrap1 + +-- NB: in the common case, 'arg_ty' is already FRR (in the sense of +-- Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete), hence 'arg_co' is 'Refl'. +-- Then 'fun_wrap' will collapse down to 'fun_wrap1'. This applies recursively; +-- as 'mkWpFun WpHole WpHole' is 'WpHole', this means that 'fun_wrap' will +-- typically just be 'WpHole'; no clutter. +-- This is important because 'matchExpectedFunTys' is called a lot. + ; return (fun_wrap, result) } ---------------------------- @@ -1404,7 +1421,7 @@ tcSubTypeMono rn_expr act_ty exp_ty ------------------------ tcSubTypePat :: CtOrigin -> UserTypeCtxt - -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper + -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper -- Used in patterns; polarity is backwards compared -- to tcSubType -- If wrap = tc_sub_type_et t1 t2 ===================================== testsuite/tests/rep-poly/T26528.hs ===================================== @@ -0,0 +1,17 @@ +{-# LANGUAGE GHC2024, TypeFamilies #-} + +module T26528 where + +import Data.Kind +import GHC.Exts + +type F :: Type -> RuntimeRep +type family F a where + F Int = LiftedRep + +g :: forall (r::RuntimeRep). + (forall (a :: TYPE r). a -> forall b. b -> b) -> Int +g _ = 3 +{-# NOINLINE g #-} + +foo = g @(F Int) (\x y -> y) ===================================== testsuite/tests/rep-poly/all.T ===================================== @@ -42,6 +42,7 @@ test('T23883b', normal, compile_fail, ['']) test('T23883c', normal, compile_fail, ['']) test('T23903', normal, compile_fail, ['']) test('T26107', js_broken(22364), compile, ['-O']) +test('T26528', normal, compile, ['']) test('EtaExpandDataCon', normal, compile, ['-O']) test('EtaExpandStupid1', normal, compile, ['-Wno-deprecated-flags']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/93fc72651bc911827bb92e7551eca01a... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/93fc72651bc911827bb92e7551eca01a... You're receiving this email because of your account on gitlab.haskell.org.