Sjoerd Visscher pushed to branch wip/T18570 at Glasgow Haskell Compiler / GHC

Commits:

10 changed files:

Changes:

  • compiler/GHC/Core/DataCon.hs
    ... ... @@ -44,6 +44,7 @@ module GHC.Core.DataCon (
    44 44 
             dataConInstOrigArgTys, dataConRepArgTys, dataConResRepTyArgs,
    45 45 
             dataConInstUnivs,
    46 46 
             dataConFieldLabels, dataConFieldType, dataConFieldType_maybe,
    47 
    +        dataConOtherFieldsAllMultMany,
    47 48 
             dataConSrcBangs,
    48 49 
             dataConSourceArity, dataConRepArity,
    49 50 
             dataConIsInfix,
    ... ... @@ -1405,6 +1406,15 @@ dataConFieldType_maybe :: DataCon -> FieldLabelString
    1405 1406 
     dataConFieldType_maybe con label
    1406 1407 
       = find ((== label) . flLabel . fst) (dcFields con `zip` (scaledThing <$> dcOrigArgTys con))
    1407 1408
    1409 
    +-- | Check if all the fields of the 'DataCon' have multiplicity 'Many',
    1410 
    +-- except for the given labelled field. In this case the selector
    1411 
    +-- of the given field can be a linear function, since it is allowed
    1412 
    +-- to discard all the other fields.
    1413 
    +dataConOtherFieldsAllMultMany :: DataCon -> FieldLabelString -> Bool
    1414 
    +dataConOtherFieldsAllMultMany con label
    1415 
    +  = all (\(fld, mult) -> flLabel fld == label || isManyTy mult)
    1416 
    +      (dcFields con `zip` (scaledMult <$> dcOrigArgTys con))
    1417 
    +
    1408 1418 
     -- | Strictness/unpack annotations, from user; or, for imported
    1409 1419 
     -- DataCons, from the interface file
    1410 1420 
     -- 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
    841 841 
                         -> FieldSelectors
    842 842 
                         -> [(Id, LHsBind GhcRn)]
    843 843 
     mkPatSynRecSelBinds ps fields has_sel
    844 
    -  = [ mkOneRecordSelector [PatSynCon ps] (RecSelPatSyn ps) fld_lbl has_sel
    844 
    +  = [ mkOneRecordSelector False [PatSynCon ps] (RecSelPatSyn ps) fld_lbl has_sel
    845 845 
         | fld_lbl <- fields ]
    846 846
    847 847 
     isUnidirectional :: HsPatSynDir a -> Bool

  • compiler/GHC/Tc/TyCl/Utils.hs
    ... ... @@ -32,7 +32,7 @@ import GHC.Tc.Utils.Env
    32 32 
     import GHC.Tc.Gen.Bind( tcValBinds )
    33 33 
     import GHC.Tc.Utils.TcType
    34 34
    35 
    -import GHC.Builtin.Types( unitTy )
    35 
    +import GHC.Builtin.Types( unitTy, manyDataConTy, multiplicityTy )
    36 36 
     import GHC.Builtin.Uniques ( mkBuiltinUnique )
    37 37
    38 38 
     import GHC.Hs
    ... ... @@ -71,6 +71,7 @@ import GHC.Types.Name.Env
    71 71 
     import GHC.Types.Name.Reader ( mkRdrUnqual )
    72 72 
     import GHC.Types.Id
    73 73 
     import GHC.Types.Id.Info
    74 
    +import GHC.Types.Var (mkTyVar)
    74 75 
     import GHC.Types.Var.Env
    75 76 
     import GHC.Types.Var.Set
    76 77 
     import GHC.Types.Unique.Set
    ... ... @@ -765,7 +766,8 @@ addTyConsToGblEnv tyclss
    765 766 
         do { traceTc "tcAddTyCons" $ vcat
    766 767 
                 [ text "tycons" <+> ppr tyclss
    767 768 
                 , text "implicits" <+> ppr implicit_things ]
    768 
    -       ; gbl_env <- tcRecSelBinds (mkRecSelBinds tyclss)
    769 
    +       ; linearEnabled <- xoptM LangExt.LinearTypes
    770 
    +       ; gbl_env <- tcRecSelBinds (mkRecSelBinds linearEnabled tyclss)
    769 771 
            ; th_bndrs <- tcTyThBinders implicit_things
    770 772 
            ; return (gbl_env, th_bndrs)
    771 773 
            }
    ... ... @@ -848,24 +850,24 @@ tcRecSelBinds sel_bind_prs
    848 850 
                                                  , let loc = getSrcSpan sel_id ]
    849 851 
         binds = [(NonRecursive, [bind]) | (_, bind) <- sel_bind_prs]
    850 852
    851 
    -mkRecSelBinds :: [TyCon] -> [(Id, LHsBind GhcRn)]
    853 
    +mkRecSelBinds :: Bool -> [TyCon] -> [(Id, LHsBind GhcRn)]
    852 854 
     -- NB We produce *un-typechecked* bindings, rather like 'deriving'
    853 855 
     --    This makes life easier, because the later type checking will add
    854 856 
     --    all necessary type abstractions and applications
    855 
    -mkRecSelBinds tycons
    856 
    -  = map mkRecSelBind [ (tc,fld) | tc <- tycons
    857 
    -                                , fld <- tyConFieldLabels tc ]
    857 
    +mkRecSelBinds allowMultiplicity tycons
    858 
    +  = [ mkRecSelBind allowMultiplicity tc fld | tc <- tycons
    859 
    +                                        , fld <- tyConFieldLabels tc ]
    858 860
    859 
    -mkRecSelBind :: (TyCon, FieldLabel) -> (Id, LHsBind GhcRn)
    860 
    -mkRecSelBind (tycon, fl)
    861 
    -  = mkOneRecordSelector all_cons (RecSelData tycon) fl
    861 
    +mkRecSelBind :: Bool -> TyCon -> FieldLabel -> (Id, LHsBind GhcRn)
    862 
    +mkRecSelBind allowMultiplicity tycon fl
    863 
    +  = mkOneRecordSelector allowMultiplicity all_cons (RecSelData tycon) fl
    862 864 
             FieldSelectors  -- See Note [NoFieldSelectors and naughty record selectors]
    863 865 
       where
    864 866 
         all_cons = map RealDataCon (tyConDataCons tycon)
    865 867
    866 
    -mkOneRecordSelector :: [ConLike] -> RecSelParent -> FieldLabel -> FieldSelectors
    868 
    +mkOneRecordSelector :: Bool -> [ConLike] -> RecSelParent -> FieldLabel -> FieldSelectors
    867 869 
                         -> (Id, LHsBind GhcRn)
    868 
    -mkOneRecordSelector all_cons idDetails fl has_sel
    870 
    +mkOneRecordSelector allowMultiplicity all_cons idDetails fl has_sel
    869 871 
       = (sel_id, L (noAnnSrcSpan loc) sel_bind)
    870 872 
       where
    871 873 
         loc      = getSrcSpan sel_name
    ... ... @@ -916,17 +918,24 @@ mkOneRecordSelector all_cons idDetails fl has_sel
    916 918 
                                                       -- thus suppressing making a binding
    917 919 
                                                       -- A slight hack!
    918 920
    921 
    +    all_other_fields_unrestricted = all all_other_unrestricted all_cons
    922 
    +      where
    923 
    +        all_other_unrestricted PatSynCon{} = False
    924 
    +        all_other_unrestricted (RealDataCon dc) = dataConOtherFieldsAllMultMany dc lbl
    925 
    +
    919 926 
         sel_ty | is_naughty = unitTy  -- See Note [Naughty record selectors]
    920 
    -           | otherwise  = mkForAllTys (tyVarSpecToBinders sel_tvbs) $
    927 
    +           | otherwise  = mkForAllTys (tyVarSpecToBinders (sel_tvbs ++ mult_tvb)) $
    921 928 
                               -- Urgh! See Note [The stupid context] in GHC.Core.DataCon
    922 
    -                          mkPhiTy (conLikeStupidTheta con1) $
    929 
    +                          mkPhiTy (conLikeStupidTheta con1)                       $
    923 930 
                               -- req_theta is empty for normal DataCon
    924 
    -                          mkPhiTy req_theta                 $
    925 
    -                          mkVisFunTyMany data_ty            $
    926 
    -                            -- Record selectors are always typed with Many. We
    927 
    -                            -- could improve on it in the case where all the
    928 
    -                            -- fields in all the constructor have multiplicity Many.
    931 
    +                          mkPhiTy req_theta                                       $
    932 
    +                          mkVisFunTy sel_mult data_ty                             $
    929 933 
                               field_ty
    934 
    +    non_partial = length all_cons == length cons_w_field -- See Note [Multiplicity and partial selectors]
    935 
    +    (mult_tvb, sel_mult) = if allowMultiplicity && non_partial && all_other_fields_unrestricted
    936 
    +      then ([mkForAllTyBinder InferredSpec mult_var], mkTyVarTy mult_var)
    937 
    +      else ([], manyDataConTy)
    938 
    +    mult_var = mkTyVar (mkSysTvName (mkBuiltinUnique 1) (fsLit "m")) multiplicityTy
    930 939
    931 940 
         -- make the binding: sel (C2 { fld = x }) = x
    932 941 
         --                   sel (C7 { fld = x }) = x
    ... ... @@ -1165,4 +1174,13 @@ Therefore, when used in the right-hand side of `unT`, GHC attempts to
    1165 1174 
     instantiate `a` with `(forall b. b -> b) -> Int`, which is impredicative.
    1166 1175 
     To make sure that GHC is OK with this, we enable ImpredicativeTypes internally
    1167 1176 
     when typechecking these HsBinds so that the user does not have to.
    1177 
    +
    1178 
    +Note [Multiplicity and partial selectors]
    1179 
    +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    1180 
    +While all logic for making record selectors multiplicity-polymorphic also applies
    1181 
    +to partial selectors, there is a technical difficulty: the catch-all default case
    1182 
    +that is added throws away its argument, and so cannot be linear. A simple workaround
    1183 
    +was not found. There may exist a more complicated workaround, but the combination of
    1184 
    +linear types and partial selectors is not expected to be very popular in practice, so
    1185 
    +it was decided to not allow multiplicity-polymorphic partial selectors at all.
    1168 1186 
     -}

  • docs/users_guide/9.14.1-notes.rst
    ... ... @@ -67,6 +67,13 @@ Language
    67 67
    68 68 
       This causes the constructor to have type ``Rec :: Int %'Many -> Char %1 -> Record``.
    69 69
    70 
    +  Also record selector functions are now multiplicity-polymorphic when possible.
    71 
    +  In the above example the selector function ``y`` now has type
    72 
    +  ``y :: Record %m -> Char``, because the ``x`` field is allowed to be discarded.
    73 
    +  In particular this always applies to the selector of a newtype wrapper.
    74 
    +  (Note that in theory this should also work with partial record selectors,
    75 
    +  but for technical reasons this is not supported.)
    76 
    +
    70 77 
     * The :extension:`ExplicitNamespaces` extension now allows the ``data``
    71 78 
       namespace specifier in import and export lists.
    72 79

  • docs/users_guide/exts/linear_types.rst
    ... ... @@ -238,7 +238,7 @@ to use ``MkT1`` in higher order functions. The additional multiplicity
    238 238 
     argument ``m`` is marked as inferred (see
    239 239 
     :ref:`inferred-vs-specified`), so that there is no conflict with
    240 240 
     visible type application. When displaying types, unless
    241 
    -``-XLinearTypes`` is enabled, multiplicity polymorphic functions are
    241 
    +``-XLinearTypes`` is enabled, multiplicity-polymorphic functions are
    242 242 
     printed as regular functions (see :ref:`printing-linear-types`);
    243 243 
     therefore constructors appear to have regular function types.
    244 244
    ... ... @@ -256,21 +256,33 @@ using GADT syntax or record syntax. Given
    256 256 
     ::
    257 257
    258 258 
         data T2 a b c where
    259 
    -        MkT2 :: a -> b %1 -> c %1 -> T2 a b c -- Note unrestricted arrow in the first argument
    259 
    +        MkT2 :: a -> b %1 -> c -> T2 a b c -- Note unrestricted arrow in the first argument
    260 260
    261 
    -the value ``MkT2 x y z`` can be constructed only if ``x`` is
    262 
    -unrestricted. On the other hand, a linear function which is matching
    263 
    -on ``MkT2 x y z`` must consume ``y`` and ``z`` exactly once, but there
    264 
    -is no restriction on ``x``. The same example can be written using record syntax:
    261 
    +the value ``MkT2 x y z`` can be constructed only if ``x`` and
    262 
    +``z`` are unrestricted. On the other hand, a linear function which is
    263 
    +matching on ``MkT2 x y z`` must consume ``y`` exactly once, but there
    264 
    +is no restriction on ``x`` and ``z``.
    265 
    +The same example can be written using record syntax:
    265 266
    266 267 
     ::
    267 268
    268 
    -    data T2 a b c = MkT2 { x %'Many :: a, y :: b, z :: c }
    269 
    +    data T2 a b c = MkT2 { x %'Many :: a, y :: b, z %'Many :: c }
    269 270
    270 271 
     Again, the constructor ``MkT2`` has type ``MkT2 :: a -> b %1 -> c %1 -> T2 a b c``.
    271 272 
     Note that by default record fields are linear, only unrestricted fields
    272 
    -require a multiplicity annotation. The annotation has no effect on the record selectors.
    273 
    -So ``x`` has type ``x :: T2 a b c -> a`` and similarly ``y`` has type ``y :: T2 a b c -> b``.
    273 
    +require a multiplicity annotation.
    274 
    +
    275 
    +The multiplicity of record selectors is inferred from the multiplicity of the fields. Note that
    276 
    +the effect of a selector is to discard all the other fields, so it can only be linear if all the
    277 
    +other fields are unrestricted. So ``x`` has type ``x :: T2 a b c -> a``, because the ``y`` field
    278 
    +is not unrestricted. But the ``x`` and ``z`` fields are unrestricted, so the selector for ``y``
    279 
    +can be linear, and therefore it is made to be multiplicity-polymorphic: ``y :: T2 a b c %m -> b``.
    280 
    +In particular this always applies to the selector of a newtype wrapper.
    281 
    +
    282 
    +In the case of multiple constructors, this logic is repeated for each constructor. So a selector
    283 
    +is only made multiplicity-polymorphic if for every constructor all the other fields are unrestricted.
    284 
    +(For technical reasons, partial record selectors cannot be made multiplicity-polymorphic, so they
    285 
    +are always unrestricted.)
    274 286
    275 287 
     It is also possible to define a multiplicity-polymorphic field:
    276 288

  • testsuite/tests/linear/should_compile/LinearRecordSelector.hs
    1 
    +{-# LANGUAGE LinearTypes, DataKinds, OverloadedRecordDot, RebindableSyntax #-}
    2 
    +module LinearRecordSelector where
    3 
    +
    4 
    +import GHC.Exts (Multiplicity(..))
    5 
    +import Prelude
    6 
    +
    7 
    +getField :: ()
    8 
    +getField = ()
    9 
    +
    10 
    +data Test = A { test :: Int, test2 %Many :: String } | B { test %Many :: Int, test3 %Many :: Char }
    11 
    +
    12 
    +test1 :: Test %1 -> Int
    13 
    +test1 a = test a
    14 
    +
    15 
    +testM :: Test -> Int
    16 
    +testM a = test a
    17 
    +
    18 
    +testX :: Test %m -> Int
    19 
    +testX = test
    20 
    +
    21 
    +newtype NT = NT { unNT :: Int }
    22 
    +
    23 
    +nt :: NT %m -> Int
    24 
    +nt a = unNT a
    25 
    +

  • testsuite/tests/linear/should_compile/all.T
    ... ... @@ -36,6 +36,7 @@ test('LinearTH3', normal, compile, [''])
    36 36 
     test('LinearTH4', req_th, compile, [''])
    37 37 
     test('LinearHole', normal, compile, [''])
    38 38 
     test('LinearDataConSections', normal, compile, [''])
    39 
    +test('LinearRecordSelector', normal, compile, ['-dcore-lint'])
    39 40 
     test('T18731', normal, compile, [''])
    40 41 
     test('T19400', unless(compiler_debugged(), skip), compile, [''])
    41 42 
     test('T20023', normal, compile, [''])

  • testsuite/tests/linear/should_fail/LinearRecordSelectorFail.hs
    1 
    +{-# LANGUAGE LinearTypes, DataKinds, OverloadedRecordDot, RebindableSyntax #-}
    2 
    +module LinearRecordSelector where
    3 
    +
    4 
    +import GHC.Exts (Multiplicity(..))
    5 
    +import Prelude
    6 
    +
    7 
    +getField :: ()
    8 
    +getField = ()
    9 
    +
    10 
    +data Test1 = A1 { testA11 :: Int, testA12 :: String }
    11 
    +
    12 
    +-- Fails because testA12 is linear
    13 
    +test1 :: Test1 %1 -> Int
    14 
    +test1 a = testA11 a
    15 
    +
    16 
    +data Test2 = A2 { testA2 :: Int } | B2 { testB2 %Many :: Char }
    17 
    +
    18 
    +-- Fails because testA2 is partial
    19 
    +test2 :: Test2 %1 -> Int
    20 
    +test2 a = testA2 a
    \ No newline at end of file

  • testsuite/tests/linear/should_fail/LinearRecordSelectorFail.stderr
    1 
    +LinearRecordSelectorFail.hs:14:7: error: [GHC-18872]
    2 
    +    • Couldn't match type ‘Many’ with ‘One’
    3 
    +        arising from multiplicity of ‘a’
    4 
    +    • In an equation for ‘test1’: test1 a = testA11 a
    5 
    +
    6 
    +LinearRecordSelectorFail.hs:20:7: error: [GHC-18872]
    7 
    +    • Couldn't match type ‘Many’ with ‘One’
    8 
    +        arising from multiplicity of ‘a’
    9 
    +    • In an equation for ‘test2’: test2 a = testA2 a
    10 
    +

  • testsuite/tests/linear/should_fail/all.T
    ... ... @@ -11,6 +11,7 @@ test('LinearNoExt', normal, compile_fail, [''])
    11 11 
     test('LinearNoExtU', normal, compile_fail, [''])
    12 12 
     test('LinearAsPat', normal, compile_fail, [''])
    13 13 
     test('LinearLazyPat', normal, compile_fail, [''])
    14 
    +test('LinearRecordSelectorFail', normal, compile_fail, [''])
    14 15 
     test('LinearRecordUpdate', normal, compile_fail, [''])
    15 16 
     test('LinearSeq', normal, compile_fail, [''])
    16 17 
     test('LinearViewPattern', normal, compile_fail, [''])

    • —
    View it on GitLab.
    You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications · Help