Sjoerd Visscher pushed to branch wip/T18570 at Glasgow Haskell Compiler / GHC Commits: 8dc4ca41 by Sjoerd Visscher at 2025-05-12T15:24:20+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. - - - - - 9 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 - + 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 ===================================== @@ -725,7 +725,8 @@ tc_patsyn_finish lname dir is_infix lpat' prag_fn -- Selectors ; has_sel <- xopt_FieldSelectors <$> getDynFlags - ; let rn_rec_sel_binds = mkPatSynRecSelBinds patSyn (patSynFieldLabels patSyn) has_sel + -- ; linearEnabled <- xoptM LangExt.LinearTypes + ; let rn_rec_sel_binds = mkPatSynRecSelBinds True patSyn (patSynFieldLabels patSyn) has_sel tything = AConLike (PatSynCon patSyn) ; tcg_env <- tcExtendGlobalEnv [tything] $ tcRecSelBinds rn_rec_sel_binds @@ -835,12 +836,13 @@ tcPatSynMatcher (L loc ps_name) lpat prag_fn ; return ((matcher_name, matcher_sigma, is_unlifted), matcher_bind) } -mkPatSynRecSelBinds :: PatSyn +mkPatSynRecSelBinds :: Bool + -> PatSyn -> [FieldLabel] -- ^ Visible field labels -> FieldSelectors -> [(Id, LHsBind GhcRn)] -mkPatSynRecSelBinds ps fields has_sel - = [ mkOneRecordSelector [PatSynCon ps] (RecSelPatSyn ps) fld_lbl has_sel +mkPatSynRecSelBinds linearEnabled ps fields has_sel + = [ mkOneRecordSelector linearEnabled [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 linearEnabled tycons + = [ mkRecSelBind linearEnabled 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 linearEnabled tycon fl + = mkOneRecordSelector linearEnabled 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 linearEnabled all_cons idDetails fl has_sel = (sel_id, L (noAnnSrcSpan loc) sel_bind) where loc = getSrcSpan sel_name @@ -916,17 +918,23 @@ 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 + (mult_tvb, sel_mult) = if linearEnabled && not_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 @@ -952,7 +960,7 @@ mkOneRecordSelector all_cons idDetails fl has_sel -- Add catch-all default case unless the case is exhaustive -- We do this explicitly so that we get a nice error message that -- mentions this particular record selector - deflt | all dealt_with all_cons = [] + deflt | not_partial = [] | otherwise = [mkSimpleMatch match_ctxt (wrapGenSpan [genWildPat]) (genLHsApp (genHsVar (getName rEC_SEL_ERROR_ID)) @@ -967,6 +975,7 @@ mkOneRecordSelector all_cons idDetails fl has_sel -- data instance T Int a where -- A :: { fld :: Int } -> T Int Bool -- B :: { fld :: Int } -> T Int Char + not_partial = all dealt_with all_cons dealt_with :: ConLike -> Bool dealt_with (PatSynCon _) = False -- We can't predict overlap dealt_with con@(RealDataCon dc) ===================================== docs/users_guide/9.14.1-notes.rst ===================================== @@ -78,6 +78,11 @@ 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 applies to the selector of a newtype wrapper. + Compiler ~~~~~~~~ ===================================== 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/8dc4ca415059b4ac67a17000bbc43f02... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/8dc4ca415059b4ac67a17000bbc43f02... You're receiving this email because of your account on gitlab.haskell.org.