Sjoerd Visscher pushed to branch wip/T18570 at Glasgow Haskell Compiler / GHC
Commits:
33b192c2 by Sjoerd Visscher at 2025-06-30T15:48:12+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.
- - - - -
5c2e78f2 by Sjoerd Visscher at 2025-06-30T15:50:52+02:00
Fix hole fits
In case all type arguments are inferred, a useless "with a" was added to hole fits.
- - - - -
1c037b30 by Sjoerd Visscher at 2025-06-30T16:02:09+02:00
Fix field type mismatch error handling
Errors in check_fields don't fail in the monad. (This commit also makes this more clear in the code.) So they didn't trigger the recovery code in checkValidTyCl.
Fixes issue #26149
- - - - -
22 changed files:
- compiler/GHC/Core/DataCon.hs
- compiler/GHC/Tc/Errors/Ppr.hs
- compiler/GHC/Tc/TyCl.hs
- compiler/GHC/Tc/TyCl/Utils.hs
- docs/users_guide/9.14.1-notes.rst
- docs/users_guide/bugs.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
- testsuite/tests/overloadedrecflds/should_fail/DRFHoleFits.stderr
- testsuite/tests/overloadedrecflds/should_run/overloadedrecfldsrun04.stdout
- testsuite/tests/perf/compiler/T16875.stderr
- testsuite/tests/simplCore/should_compile/OpaqueNoCastWW.stderr
- testsuite/tests/typecheck/should_fail/CommonFieldTypeMismatch.stderr
- testsuite/tests/typecheck/should_fail/T12083a.hs
- testsuite/tests/typecheck/should_fail/T12083a.stderr
- testsuite/tests/typecheck/should_fail/T9739.hs
- testsuite/tests/typecheck/should_fail/T9739.stderr
- utils/haddock/html-test/ref/Bug294.html
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, dataConVisArity, dataConRepArity,
dataConIsInfix,
@@ -1406,6 +1407,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/Errors/Ppr.hs
=====================================
@@ -3541,12 +3541,12 @@ pprHoleFit :: HoleFitDispConfig -> HoleFit -> SDoc
pprHoleFit _ (RawHoleFit sd) = sd
pprHoleFit (HFDC sWrp sWrpVars sTy sProv sMs) (TcHoleFit (HoleFit {..})) =
hang display 2 provenance
- where tyApp = sep $ zipWithEqual pprArg vars hfWrap
+ where tyApps = concat $ zipWithEqual pprArg vars hfWrap
where pprArg b arg = case binderFlag b of
- Specified -> text "@" <> pprParendType arg
+ Specified -> [text "@" <> pprParendType arg]
-- Do not print type application for inferred
-- variables (#16456)
- Inferred -> empty
+ Inferred -> []
Required -> pprPanic "pprHoleFit: bad Required"
(ppr b <+> ppr arg)
tyAppVars = sep $ punctuate comma $
@@ -3573,9 +3573,9 @@ pprHoleFit (HFDC sWrp sWrpVars sTy sProv sMs) (TcHoleFit (HoleFit {..})) =
IdHFCand id_ -> pprPrefixOcc id_
tyDisp = ppWhen sTy $ dcolon <+> ppr hfType
has = not . null
- wrapDisp = ppWhen (has hfWrap && (sWrp || sWrpVars))
+ wrapDisp = ppWhen (has tyApps && (sWrp || sWrpVars))
$ text "with" <+> if sWrp || not sTy
- then occDisp <+> tyApp
+ then occDisp <+> sep tyApps
else tyAppVars
docs = case hfDoc of
Just d -> pprHsDocStrings d
=====================================
compiler/GHC/Tc/TyCl.hs
=====================================
@@ -4787,6 +4787,7 @@ checkValidTyCl tc
= setSrcSpan (getSrcSpan tc) $
addTyConCtxt tc $
recoverM recovery_code $
+ checkNoErrs $
do { traceTc "Starting validity for tycon" (ppr tc)
; checkValidTyCon tc
; checkTyConConsistentWithBoot tc -- See Note [TyCon boot consistency checking]
@@ -4818,6 +4819,9 @@ See indexed-types/should_fail/BadSock and #10896
Some notes:
+* Not all errors in `checkValidTyCon` fail in the monad. To make sure
+ we also recover from these, we use `checkNoErrs`. See (#26149)
+
* We must make fakes for promoted DataCons too. Consider (#15215)
data T a = MkT ...
data S a = ...T...MkT....
@@ -4991,7 +4995,7 @@ checkValidTyCon tc
check_fields ((label, con1) :| other_fields)
-- These fields all have the same name, but are from
-- different constructors in the data type
- = recoverM (return ()) $ mapM_ checkOne other_fields
+ = mapM_ checkOne other_fields
-- Check that all the fields in the group have the same type
-- NB: this check assumes that all the constructors of a given
-- data type use the same type variables
@@ -5001,8 +5005,9 @@ checkValidTyCon tc
lbl = flLabel label
checkOne (_, con2) -- Do it both ways to ensure they are structurally identical
- = do { checkFieldCompat lbl con1 con2 res1 res2 fty1 fty2
- ; checkFieldCompat lbl con2 con1 res2 res1 fty2 fty1 }
+ = traverse_ addErrTc $ firstJust -- Don't report the same error twice
+ (checkFieldCompat lbl con1 con2 res1 res2 fty1 fty2)
+ (checkFieldCompat lbl con2 con1 res2 res1 fty2 fty1)
where
res2 = dataConOrigResTy con2
fty2 = dataConFieldType con2 lbl
@@ -5027,10 +5032,13 @@ checkPartialRecordField all_cons fld
inst_tys = dataConResRepTyArgs con1
checkFieldCompat :: FieldLabelString -> DataCon -> DataCon
- -> Type -> Type -> Type -> Type -> TcM ()
+ -> Type -> Type -> Type -> Type -> Maybe TcRnMessage
checkFieldCompat fld con1 con2 res1 res2 fty1 fty2
- = do { checkTc (isJust mb_subst1) (TcRnCommonFieldResultTypeMismatch con1 con2 fld)
- ; checkTc (isJust mb_subst2) (TcRnCommonFieldTypeMismatch con1 con2 fld) }
+ = if isNothing mb_subst1
+ then Just $ TcRnCommonFieldResultTypeMismatch con1 con2 fld
+ else if isNothing mb_subst2
+ then Just $ TcRnCommonFieldTypeMismatch con1 con2 fld
+ else Nothing
where
mb_subst1 = tcMatchTy res1 res2
mb_subst2 = tcMatchTyX (expectJust mb_subst1) fty1 fty2
=====================================
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
@@ -853,11 +854,11 @@ mkRecSelBinds :: [TyCon] -> [(Id, LHsBind GhcRn)]
-- 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 ]
+ = [ mkRecSelBind tc fld | tc <- tycons
+ , fld <- tyConFieldLabels tc ]
-mkRecSelBind :: (TyCon, FieldLabel) -> (Id, LHsBind GhcRn)
-mkRecSelBind (tycon, fl)
+mkRecSelBind :: TyCon -> FieldLabel -> (Id, LHsBind GhcRn)
+mkRecSelBind tycon fl
= mkOneRecordSelector all_cons (RecSelData tycon) fl
FieldSelectors -- See Note [NoFieldSelectors and naughty record selectors]
where
@@ -916,17 +917,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 sel_tvbs $
+ | otherwise = mkForAllTys (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 non_partial && all_other_fields_unrestricted
+ then ([mkForAllTyBinder (Invisible 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 +1173,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/bugs.rst
=====================================
@@ -701,6 +701,9 @@ Bugs in GHC
- Because of a toolchain limitation we are unable to support full Unicode paths
on Windows. On Windows we support up to Latin-1. See :ghc-ticket:`12971` for more.
+- For technical reasons, partial record selectors cannot be made
+ multiplicity-polymorphic, so they are always unrestricted.
+
.. _bugs-ghci:
Bugs in GHCi (the interactive GHC)
=====================================
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 the unrestricted arrows on a and c
-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,21 @@
+{-# LANGUAGE LinearTypes, DataKinds, OverloadedRecordDot, RebindableSyntax #-}
+module LinearRecordSelector where
+
+import GHC.Exts (Multiplicity(..))
+import Prelude
+
+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,17 @@
+{-# LANGUAGE LinearTypes, DataKinds, OverloadedRecordDot, RebindableSyntax #-}
+module LinearRecordSelector where
+
+import GHC.Exts (Multiplicity(..))
+import Prelude
+
+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
=====================================
testsuite/tests/linear/should_fail/LinearRecordSelectorFail.stderr
=====================================
@@ -0,0 +1,10 @@
+LinearRecordSelectorFail.hs:11: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:17: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, [''])
=====================================
testsuite/tests/overloadedrecflds/should_fail/DRFHoleFits.stderr
=====================================
@@ -1,4 +1,3 @@
-
DRFHoleFits.hs:7:7: error: [GHC-88464]
• Found hole: _ :: T -> Int
• In the expression: _ :: T -> Int
@@ -6,8 +5,8 @@ DRFHoleFits.hs:7:7: error: [GHC-88464]
• Relevant bindings include
bar :: T -> Int (bound at DRFHoleFits.hs:7:1)
Valid hole fits include
- foo :: T -> Int (defined at DRFHoleFits.hs:5:16)
bar :: T -> Int (defined at DRFHoleFits.hs:7:1)
+ foo :: T -> Int (defined at DRFHoleFits.hs:5:16)
DRFHoleFits.hs:8:7: error: [GHC-88464]
• Found hole: _ :: A.S -> Int
@@ -20,3 +19,4 @@ DRFHoleFits.hs:8:7: error: [GHC-88464]
A.foo :: A.S -> Int
(imported qualified from ‘DRFHoleFits_A’ at DRFHoleFits.hs:3:1-35
(and originally defined at DRFHoleFits_A.hs:5:16-18))
+
=====================================
testsuite/tests/overloadedrecflds/should_run/overloadedrecfldsrun04.stdout
=====================================
@@ -1,5 +1,8 @@
data Main.R = Main.MkR {Main.foo :: GHC.Internal.Types.Int}
-Main.foo :: Main.R -> GHC.Internal.Types.Int
-Main.foo :: Main.R -> GHC.Internal.Types.Int
-Main.foo :: Main.R -> GHC.Internal.Types.Int
+Main.foo :: forall {m_0 :: GHC.Internal.Types.Multiplicity} .
+ Main.R %m_0 -> GHC.Internal.Types.Int
+Main.foo :: forall {m_0 :: GHC.Internal.Types.Multiplicity} .
+ Main.R %m_0 -> GHC.Internal.Types.Int
+Main.foo :: forall {m_0 :: GHC.Internal.Types.Multiplicity} .
+ Main.R %m_0 -> GHC.Internal.Types.Int
42
=====================================
testsuite/tests/perf/compiler/T16875.stderr
=====================================
@@ -6,7 +6,5 @@ T16875.hs:12:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
• In an equation for ‘a’: a = _
• Relevant bindings include a :: p (bound at T16875.hs:12:1)
Valid hole fits include
- a :: forall {p}. p
- with a
- (defined at T16875.hs:12:1)
+ a :: forall {p}. p (defined at T16875.hs:12:1)
=====================================
testsuite/tests/simplCore/should_compile/OpaqueNoCastWW.stderr
=====================================
@@ -1,22 +1,32 @@
==================== Tidy Core ====================
Result size of Tidy Core
- = {terms: 82, types: 52, coercions: 29, joins: 0/0}
+ = {terms: 83, types: 55, coercions: 31, joins: 0/0}
--- RHS size: {terms: 3, types: 3, coercions: 0, joins: 0/0}
-unsafeToInteger1 :: forall (n :: Nat). Signed n -> Signed n
+-- RHS size: {terms: 4, types: 4, coercions: 0, joins: 0/0}
+unsafeToInteger1
+ :: forall (n :: Nat) (m :: GHC.Internal.Types.Multiplicity).
+ Signed n %m -> Signed n
[GblId, Arity=1, Unf=OtherCon []]
-unsafeToInteger1 = \ (@(n :: Nat)) (ds :: Signed n) -> ds
+unsafeToInteger1
+ = \ (@(n :: Nat))
+ (@(m :: GHC.Internal.Types.Multiplicity))
+ (ds :: Signed n) ->
+ ds
--- RHS size: {terms: 1, types: 0, coercions: 8, joins: 0/0}
-unsafeToInteger :: forall (n :: Nat). Signed n -> Integer
+-- RHS size: {terms: 1, types: 0, coercions: 10, joins: 0/0}
+unsafeToInteger
+ :: forall (n :: Nat) {m :: GHC.Internal.Types.Multiplicity}.
+ Signed n %m -> Integer
[GblId[[RecSel]], Arity=1, Unf=OtherCon []]
unsafeToInteger
= unsafeToInteger1
- `cast` (forall (n :: <Nat>_N).
- <Signed n>_R %<Many>_N ->_R OpaqueNoCastWW.N:Signed <n>_P
- :: (forall (n :: Nat). Signed n -> Signed n)
- ~R# (forall (n :: Nat). Signed n -> Integer))
+ `cast` (forall (n :: <Nat>_N) (m ::
participants (1)
-
Sjoerd Visscher (＠trac-sjoerd_visscher)