Sjoerd Visscher pushed to branch wip/T18570 at Glasgow Haskell Compiler / GHC Commits: ce06db66 by Sjoerd Visscher at 2025-06-06T16:59:52+02:00 Calculate multiplicity for record selector functions Until now record selector functions always had multiplicity Many, but when all the other fields have been declared with multiplicity Many (including the case when there are no other fields), then the selector function is allowed to be used linearly too, as it is allowed to discard all the other fields. Since in that case the multiplicity can be both One and Many, the selector function is made multiplicity-polymorphic. - - - - - 10 changed files: - compiler/GHC/Core/DataCon.hs - compiler/GHC/Tc/TyCl/PatSyn.hs - compiler/GHC/Tc/TyCl/Utils.hs - docs/users_guide/9.14.1-notes.rst - docs/users_guide/exts/linear_types.rst - + testsuite/tests/linear/should_compile/LinearRecordSelector.hs - testsuite/tests/linear/should_compile/all.T - + testsuite/tests/linear/should_fail/LinearRecordSelectorFail.hs - + testsuite/tests/linear/should_fail/LinearRecordSelectorFail.stderr - testsuite/tests/linear/should_fail/all.T Changes: ===================================== compiler/GHC/Core/DataCon.hs ===================================== @@ -44,6 +44,7 @@ module GHC.Core.DataCon ( dataConInstOrigArgTys, dataConRepArgTys, dataConResRepTyArgs, dataConInstUnivs, dataConFieldLabels, dataConFieldType, dataConFieldType_maybe, + dataConOtherFieldsAllMultMany, dataConSrcBangs, dataConSourceArity, dataConRepArity, dataConIsInfix, @@ -1405,6 +1406,15 @@ dataConFieldType_maybe :: DataCon -> FieldLabelString dataConFieldType_maybe con label = find ((== label) . flLabel . fst) (dcFields con `zip` (scaledThing <$> dcOrigArgTys con)) +-- | Check if all the fields of the 'DataCon' have multiplicity 'Many', +-- except for the given labelled field. In this case the selector +-- of the given field can be a linear function, since it is allowed +-- to discard all the other fields. +dataConOtherFieldsAllMultMany :: DataCon -> FieldLabelString -> Bool +dataConOtherFieldsAllMultMany con label + = all (\(fld, mult) -> flLabel fld == label || isManyTy mult) + (dcFields con `zip` (scaledMult <$> dcOrigArgTys con)) + -- | Strictness/unpack annotations, from user; or, for imported -- DataCons, from the interface file -- The list is in one-to-one correspondence with the arity of the 'DataCon' ===================================== compiler/GHC/Tc/TyCl/PatSyn.hs ===================================== @@ -841,7 +841,7 @@ mkPatSynRecSelBinds :: PatSyn -> FieldSelectors -> [(Id, LHsBind GhcRn)] mkPatSynRecSelBinds ps fields has_sel - = [ mkOneRecordSelector [PatSynCon ps] (RecSelPatSyn ps) fld_lbl has_sel + = [ mkOneRecordSelector False [PatSynCon ps] (RecSelPatSyn ps) fld_lbl has_sel | fld_lbl <- fields ] isUnidirectional :: HsPatSynDir a -> Bool ===================================== compiler/GHC/Tc/TyCl/Utils.hs ===================================== @@ -32,7 +32,7 @@ import GHC.Tc.Utils.Env import GHC.Tc.Gen.Bind( tcValBinds ) import GHC.Tc.Utils.TcType -import GHC.Builtin.Types( unitTy ) +import GHC.Builtin.Types( unitTy, manyDataConTy, multiplicityTy ) import GHC.Builtin.Uniques ( mkBuiltinUnique ) import GHC.Hs @@ -71,6 +71,7 @@ import GHC.Types.Name.Env import GHC.Types.Name.Reader ( mkRdrUnqual ) import GHC.Types.Id import GHC.Types.Id.Info +import GHC.Types.Var (mkTyVar) import GHC.Types.Var.Env import GHC.Types.Var.Set import GHC.Types.Unique.Set @@ -765,7 +766,8 @@ addTyConsToGblEnv tyclss do { traceTc "tcAddTyCons" $ vcat [ text "tycons" <+> ppr tyclss , text "implicits" <+> ppr implicit_things ] - ; gbl_env <- tcRecSelBinds (mkRecSelBinds tyclss) + ; linearEnabled <- xoptM LangExt.LinearTypes + ; gbl_env <- tcRecSelBinds (mkRecSelBinds linearEnabled tyclss) ; th_bndrs <- tcTyThBinders implicit_things ; return (gbl_env, th_bndrs) } @@ -848,24 +850,24 @@ tcRecSelBinds sel_bind_prs , let loc = getSrcSpan sel_id ] binds = [(NonRecursive, [bind]) | (_, bind) <- sel_bind_prs] -mkRecSelBinds :: [TyCon] -> [(Id, LHsBind GhcRn)] +mkRecSelBinds :: Bool -> [TyCon] -> [(Id, LHsBind GhcRn)] -- NB We produce *un-typechecked* bindings, rather like 'deriving' -- This makes life easier, because the later type checking will add -- all necessary type abstractions and applications -mkRecSelBinds tycons - = map mkRecSelBind [ (tc,fld) | tc <- tycons - , fld <- tyConFieldLabels tc ] +mkRecSelBinds allowMultiplicity tycons + = [ mkRecSelBind allowMultiplicity tc fld | tc <- tycons + , fld <- tyConFieldLabels tc ] -mkRecSelBind :: (TyCon, FieldLabel) -> (Id, LHsBind GhcRn) -mkRecSelBind (tycon, fl) - = mkOneRecordSelector all_cons (RecSelData tycon) fl +mkRecSelBind :: Bool -> TyCon -> FieldLabel -> (Id, LHsBind GhcRn) +mkRecSelBind allowMultiplicity tycon fl + = mkOneRecordSelector allowMultiplicity all_cons (RecSelData tycon) fl FieldSelectors -- See Note [NoFieldSelectors and naughty record selectors] where all_cons = map RealDataCon (tyConDataCons tycon) -mkOneRecordSelector :: [ConLike] -> RecSelParent -> FieldLabel -> FieldSelectors +mkOneRecordSelector :: Bool -> [ConLike] -> RecSelParent -> FieldLabel -> FieldSelectors -> (Id, LHsBind GhcRn) -mkOneRecordSelector all_cons idDetails fl has_sel +mkOneRecordSelector allowMultiplicity all_cons idDetails fl has_sel = (sel_id, L (noAnnSrcSpan loc) sel_bind) where loc = getSrcSpan sel_name @@ -916,17 +918,24 @@ mkOneRecordSelector all_cons idDetails fl has_sel -- thus suppressing making a binding -- A slight hack! + all_other_fields_unrestricted = all all_other_unrestricted all_cons + where + all_other_unrestricted PatSynCon{} = False + all_other_unrestricted (RealDataCon dc) = dataConOtherFieldsAllMultMany dc lbl + sel_ty | is_naughty = unitTy -- See Note [Naughty record selectors] - | otherwise = mkForAllTys (tyVarSpecToBinders sel_tvbs) $ + | otherwise = mkForAllTys (tyVarSpecToBinders (sel_tvbs ++ mult_tvb)) $ -- Urgh! See Note [The stupid context] in GHC.Core.DataCon - mkPhiTy (conLikeStupidTheta con1) $ + mkPhiTy (conLikeStupidTheta con1) $ -- req_theta is empty for normal DataCon - mkPhiTy req_theta $ - mkVisFunTyMany data_ty $ - -- Record selectors are always typed with Many. We - -- could improve on it in the case where all the - -- fields in all the constructor have multiplicity Many. + mkPhiTy req_theta $ + mkVisFunTy sel_mult data_ty $ field_ty + non_partial = length all_cons == length cons_w_field -- See Note [Multiplicity and partial selectors] + (mult_tvb, sel_mult) = if allowMultiplicity && non_partial && all_other_fields_unrestricted + then ([mkForAllTyBinder InferredSpec mult_var], mkTyVarTy mult_var) + else ([], manyDataConTy) + mult_var = mkTyVar (mkSysTvName (mkBuiltinUnique 1) (fsLit "m")) multiplicityTy -- make the binding: sel (C2 { fld = x }) = x -- sel (C7 { fld = x }) = x @@ -1165,4 +1174,13 @@ Therefore, when used in the right-hand side of `unT`, GHC attempts to instantiate `a` with `(forall b. b -> b) -> Int`, which is impredicative. To make sure that GHC is OK with this, we enable ImpredicativeTypes internally when typechecking these HsBinds so that the user does not have to. + +Note [Multiplicity and partial selectors] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +While all logic for making record selectors multiplicity-polymorphic also applies +to partial selectors, there is a technical difficulty: the catch-all default case +that is added throws away its argument, and so cannot be linear. A simple workaround +was not found. There may exist a more complicated workaround, but the combination of +linear types and partial selectors is not expected to be very popular in practice, so +it was decided to not allow multiplicity-polymorphic partial selectors at all. -} ===================================== docs/users_guide/9.14.1-notes.rst ===================================== @@ -67,6 +67,13 @@ Language This causes the constructor to have type ``Rec :: Int %'Many -> Char %1 -> Record``. + Also record selector functions are now multiplicity-polymorphic when possible. + In the above example the selector function ``y`` now has type + ``y :: Record %m -> Char``, because the ``x`` field is allowed to be discarded. + In particular this always applies to the selector of a newtype wrapper. + (Note that in theory this should also work with partial record selectors, + but for technical reasons this is not supported.) + * The :extension:`ExplicitNamespaces` extension now allows the ``data`` namespace specifier in import and export lists. ===================================== docs/users_guide/exts/linear_types.rst ===================================== @@ -238,7 +238,7 @@ to use ``MkT1`` in higher order functions. The additional multiplicity argument ``m`` is marked as inferred (see :ref:`inferred-vs-specified`), so that there is no conflict with visible type application. When displaying types, unless -``-XLinearTypes`` is enabled, multiplicity polymorphic functions are +``-XLinearTypes`` is enabled, multiplicity-polymorphic functions are printed as regular functions (see :ref:`printing-linear-types`); therefore constructors appear to have regular function types. @@ -256,21 +256,33 @@ using GADT syntax or record syntax. Given :: data T2 a b c where - MkT2 :: a -> b %1 -> c %1 -> T2 a b c -- Note unrestricted arrow in the first argument + MkT2 :: a -> b %1 -> c -> T2 a b c -- Note unrestricted arrow in the first argument -the value ``MkT2 x y z`` can be constructed only if ``x`` is -unrestricted. On the other hand, a linear function which is matching -on ``MkT2 x y z`` must consume ``y`` and ``z`` exactly once, but there -is no restriction on ``x``. The same example can be written using record syntax: +the value ``MkT2 x y z`` can be constructed only if ``x`` and +``z`` are unrestricted. On the other hand, a linear function which is +matching on ``MkT2 x y z`` must consume ``y`` exactly once, but there +is no restriction on ``x`` and ``z``. +The same example can be written using record syntax: :: - data T2 a b c = MkT2 { x %'Many :: a, y :: b, z :: c } + data T2 a b c = MkT2 { x %'Many :: a, y :: b, z %'Many :: c } Again, the constructor ``MkT2`` has type ``MkT2 :: a -> b %1 -> c %1 -> T2 a b c``. Note that by default record fields are linear, only unrestricted fields -require a multiplicity annotation. The annotation has no effect on the record selectors. -So ``x`` has type ``x :: T2 a b c -> a`` and similarly ``y`` has type ``y :: T2 a b c -> b``. +require a multiplicity annotation. + +The multiplicity of record selectors is inferred from the multiplicity of the fields. Note that +the effect of a selector is to discard all the other fields, so it can only be linear if all the +other fields are unrestricted. So ``x`` has type ``x :: T2 a b c -> a``, because the ``y`` field +is not unrestricted. But the ``x`` and ``z`` fields are unrestricted, so the selector for ``y`` +can be linear, and therefore it is made to be multiplicity-polymorphic: ``y :: T2 a b c %m -> b``. +In particular this always applies to the selector of a newtype wrapper. + +In the case of multiple constructors, this logic is repeated for each constructor. So a selector +is only made multiplicity-polymorphic if for every constructor all the other fields are unrestricted. +(For technical reasons, partial record selectors cannot be made multiplicity-polymorphic, so they +are always unrestricted.) It is also possible to define a multiplicity-polymorphic field: ===================================== testsuite/tests/linear/should_compile/LinearRecordSelector.hs ===================================== @@ -0,0 +1,25 @@ +{-# LANGUAGE LinearTypes, DataKinds, OverloadedRecordDot, RebindableSyntax #-} +module LinearRecordSelector where + +import GHC.Exts (Multiplicity(..)) +import Prelude + +getField :: () +getField = () + +data Test = A { test :: Int, test2 %Many :: String } | B { test %Many :: Int, test3 %Many :: Char } + +test1 :: Test %1 -> Int +test1 a = test a + +testM :: Test -> Int +testM a = test a + +testX :: Test %m -> Int +testX = test + +newtype NT = NT { unNT :: Int } + +nt :: NT %m -> Int +nt a = unNT a + ===================================== testsuite/tests/linear/should_compile/all.T ===================================== @@ -36,6 +36,7 @@ test('LinearTH3', normal, compile, ['']) test('LinearTH4', req_th, compile, ['']) test('LinearHole', normal, compile, ['']) test('LinearDataConSections', normal, compile, ['']) +test('LinearRecordSelector', normal, compile, ['-dcore-lint']) test('T18731', normal, compile, ['']) test('T19400', unless(compiler_debugged(), skip), compile, ['']) test('T20023', normal, compile, ['']) ===================================== testsuite/tests/linear/should_fail/LinearRecordSelectorFail.hs ===================================== @@ -0,0 +1,20 @@ +{-# LANGUAGE LinearTypes, DataKinds, OverloadedRecordDot, RebindableSyntax #-} +module LinearRecordSelector where + +import GHC.Exts (Multiplicity(..)) +import Prelude + +getField :: () +getField = () + +data Test1 = A1 { testA11 :: Int, testA12 :: String } + +-- Fails because testA12 is linear +test1 :: Test1 %1 -> Int +test1 a = testA11 a + +data Test2 = A2 { testA2 :: Int } | B2 { testB2 %Many :: Char } + +-- Fails because testA2 is partial +test2 :: Test2 %1 -> Int +test2 a = testA2 a \ No newline at end of file ===================================== testsuite/tests/linear/should_fail/LinearRecordSelectorFail.stderr ===================================== @@ -0,0 +1,10 @@ +LinearRecordSelectorFail.hs:14:7: error: [GHC-18872] + • Couldn't match type ‘Many’ with ‘One’ + arising from multiplicity of ‘a’ + • In an equation for ‘test1’: test1 a = testA11 a + +LinearRecordSelectorFail.hs:20:7: error: [GHC-18872] + • Couldn't match type ‘Many’ with ‘One’ + arising from multiplicity of ‘a’ + • In an equation for ‘test2’: test2 a = testA2 a + ===================================== testsuite/tests/linear/should_fail/all.T ===================================== @@ -11,6 +11,7 @@ test('LinearNoExt', normal, compile_fail, ['']) test('LinearNoExtU', normal, compile_fail, ['']) test('LinearAsPat', normal, compile_fail, ['']) test('LinearLazyPat', normal, compile_fail, ['']) +test('LinearRecordSelectorFail', normal, compile_fail, ['']) test('LinearRecordUpdate', normal, compile_fail, ['']) test('LinearSeq', normal, compile_fail, ['']) test('LinearViewPattern', normal, compile_fail, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ce06db6666461a9d9dfa6a7da5a603c2... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ce06db6666461a9d9dfa6a7da5a603c2... You're receiving this email because of your account on gitlab.haskell.org.