[Git][ghc/ghc][wip/t22707] 4 commits: Export getSolo from Data.Tuple

Simon Peyton Jones (@simonpj) gitlab at gitlab.haskell.org
Sat Mar 4 00:05:50 UTC 2023



Simon Peyton Jones pushed to branch wip/t22707 at Glasgow Haskell Compiler / GHC


Commits:
45af8482 by David Feuer at 2023-03-03T11:40:47-05:00
Export getSolo from Data.Tuple

Proposed in
[CLC proposal #113](https://github.com/haskell/core-libraries-committee/issues/113)
and
[approved by the CLC](https://github.com/haskell/core-libraries-committee/issues/113#issuecomment-1452452191)

- - - - -
0c694895 by David Feuer at 2023-03-03T11:40:47-05:00
Document getSolo

- - - - -
bd0536af by Simon Peyton Jones at 2023-03-03T11:41:23-05:00
More fixes for `type data` declarations

This MR fixes #23022 and #23023.  Specifically

* Beef up Note [Type data declarations] in GHC.Rename.Module,
  to make invariant (I1) explicit, and to name the several
  wrinkles.

  And add references to these specific wrinkles.

* Add a Lint check for invariant (I1) above.
  See GHC.Core.Lint.checkTypeDataConOcc

* Disable the `caseRules` for dataToTag# for `type data` values.
  See Wrinkle (W2c) in the Note above.  Fixes #23023.

* Refine the assertion in dataConRepArgTys, so that it does not
  complain about the absence of a wrapper for a `type data` constructor
  Fixes #23022.

Acked-by: Simon Peyton Jones <simon.peytonjones at gmail.com>

- - - - -
c7c1a73b by Simon Peyton Jones at 2023-03-04T00:05:43+00:00
Add test for T22793

- - - - -


17 changed files:

- compiler/GHC/Core/DataCon.hs
- compiler/GHC/Core/Lint.hs
- compiler/GHC/Core/Opt/ConstantFold.hs
- compiler/GHC/Core/Utils.hs
- compiler/GHC/HsToCore/Pmc/Solver.hs
- compiler/GHC/Rename/Module.hs
- compiler/GHC/Tc/Gen/App.hs
- docs/users_guide/9.8.1-notes.rst
- libraries/base/Data/Tuple.hs
- libraries/base/changelog.md
- libraries/ghc-prim/GHC/Tuple/Prim.hs
- + testsuite/tests/gadt/T23022.hs
- + testsuite/tests/gadt/T23023.hs
- testsuite/tests/gadt/all.T
- + testsuite/tests/polykinds/T22793.hs
- + testsuite/tests/polykinds/T22793.stderr
- testsuite/tests/polykinds/all.T


Changes:

=====================================
compiler/GHC/Core/DataCon.hs
=====================================
@@ -1669,13 +1669,25 @@ dataConOtherTheta dc = dcOtherTheta dc
 -- evidence, after any flattening has been done and without substituting for
 -- any type variables
 dataConRepArgTys :: DataCon -> [Scaled Type]
-dataConRepArgTys (MkData { dcRep = rep
-                         , dcEqSpec = eq_spec
+dataConRepArgTys (MkData { dcRep        = rep
+                         , dcEqSpec     = eq_spec
                          , dcOtherTheta = theta
-                         , dcOrigArgTys = orig_arg_tys })
+                         , dcOrigArgTys = orig_arg_tys
+                         , dcRepTyCon   = tc })
   = case rep of
-      NoDataConRep -> assert (null eq_spec) $ map unrestricted theta ++ orig_arg_tys
       DCR { dcr_arg_tys = arg_tys } -> arg_tys
+      NoDataConRep
+        | isTypeDataTyCon tc -> assert (null theta)   $
+                                orig_arg_tys
+          -- `type data` declarations can be GADTs (and hence have an eq_spec)
+          -- but no wrapper.  They cannot have a theta.
+          -- See Note [Type data declarations] in GHC.Rename.Module
+          -- You might wonder why we ever call dataConRepArgTys for `type data`;
+          -- I think it's because of the call in mkDataCon, which in turn feeds
+          -- into dcRepArity, which in turn is used in mkDataConWorkId.
+          -- c.f. #23022
+        | otherwise          -> assert (null eq_spec) $
+                                map unrestricted theta ++ orig_arg_tys
 
 -- | The string @package:module.name@ identifying a constructor, which is attached
 -- to its info table and used by the GHCi debugger and the heap profiler


=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -1021,6 +1021,9 @@ lintIdOcc var nargs
 
         ; checkDeadIdOcc var
         ; checkJoinOcc var nargs
+        ; case isDataConId_maybe var of
+             Nothing -> return ()
+             Just dc -> checkTypeDataConOcc "expression" dc
 
         ; usage <- varCallSiteUsage var
 
@@ -1107,6 +1110,13 @@ checkJoinOcc var n_args
   | otherwise
   = return ()
 
+checkTypeDataConOcc :: String -> DataCon -> LintM ()
+-- Check that the Id is not a data constructor of a `type data` declaration
+-- Invariant (I1) of Note [Type data declarations] in GHC.Rename.Module
+checkTypeDataConOcc what dc
+  = checkL (not (isTypeDataTyCon (dataConTyCon dc))) $
+    (text "type data constructor found in a" <+> text what <> colon <+> ppr dc)
+
 -- | This function checks that we are able to perform eta expansion for
 -- functions with no binding, in order to satisfy invariant I3
 -- from Note [Representation polymorphism invariants] in GHC.Core.
@@ -1561,10 +1571,11 @@ lintCoreAlt case_bndr scrut_ty _scrut_mult alt_ty alt@(Alt (DataAlt con) args rh
   = zeroUE <$ addErrL (mkNewTyDataConAltMsg scrut_ty alt)
   | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
   = addLoc (CaseAlt alt) $  do
-    {   -- First instantiate the universally quantified
-        -- type variables of the data constructor
-        -- We've already check
-      lintL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
+    { checkTypeDataConOcc "pattern" con
+    ; lintL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
+
+      -- Instantiate the universally quantified
+      -- type variables of the data constructor
     ; let { con_payload_ty = piResultTys (dataConRepType con) tycon_arg_tys
           ; binderMult (Named _)   = ManyTy
           ; binderMult (Anon st _) = scaledMult st


=====================================
compiler/GHC/Core/Opt/ConstantFold.hs
=====================================
@@ -55,7 +55,7 @@ import GHC.Core.TyCo.Compare( eqType )
 import GHC.Core.TyCon
    ( tyConDataCons_maybe, isAlgTyCon, isEnumerationTyCon
    , isNewTyCon, tyConDataCons
-   , tyConFamilySize )
+   , tyConFamilySize, isTypeDataTyCon )
 import GHC.Core.Map.Expr ( eqCoreExpr )
 
 import GHC.Builtin.PrimOps ( PrimOp(..), tagToEnumKey )
@@ -3184,6 +3184,8 @@ caseRules _ (App (App (Var f) (Type ty)) v)       -- dataToTag x
   | Just DataToTagOp <- isPrimOpId_maybe f
   , Just (tc, _) <- tcSplitTyConApp_maybe ty
   , isAlgTyCon tc
+  , not (isTypeDataTyCon tc) -- See wrinkle (W2c) in GHC.Rename.Module
+                             -- Note [Type data declarations]
   = Just (v, tx_con_dtt ty
            , \v -> App (App (Var f) (Type ty)) (Var v))
 


=====================================
compiler/GHC/Core/Utils.hs
=====================================
@@ -845,7 +845,8 @@ There are two exceptions where we avoid refining a DEFAULT case:
            __DEFAULT -> ()
 
   Namely, we do _not_ want to match on `A`, as it doesn't exist at the value
-  level!
+  level! See wrinkle (W2b) in Note [Type data declarations] in GHC.Rename.Module
+
 
 Note [Combine identical alternatives]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~


=====================================
compiler/GHC/HsToCore/Pmc/Solver.hs
=====================================
@@ -152,8 +152,8 @@ vanillaCompleteMatchTC tc =
                tc == tYPETyCon    = Just []
              | -- Similarly, treat `type data` declarations as empty data types on
                -- the term level, as `type data` data constructors only exist at
-               -- the type level (#22964).
-               -- See Note [Type data declarations] in GHC.Rename.Module.
+               -- the type level (#22964).  See wrinkle (W2a) in
+               -- Note [Type data declarations] in GHC.Rename.Module.
                isTypeDataTyCon tc = Just []
              | otherwise          = tyConDataCons_maybe tc
   in vanillaCompleteMatch . mkUniqDSet . map RealDataCon <$> mb_dcs


=====================================
compiler/GHC/Rename/Module.hs
=====================================
@@ -2073,9 +2073,79 @@ preceded by `type`, with the following restrictions:
 
 (R5) There are no deriving clauses.
 
+The data constructors of a `type data` declaration obey the following
+Core invariant:
+
+(I1) The data constructors of a `type data` declaration may be mentioned in
+     /types/, but never in /terms/ or the /pattern of a case alternative/.
+
+Wrinkles:
+
+(W0) Wrappers.  The data constructor of a `type data` declaration has a worker
+     (like every data constructor) but does /not/ have a wrapper.  Wrappers
+     only make sense for value-level data constructors. Indeed, the worker Id
+     is never used (invariant (I1)), so it barely makes sense to talk about
+     the worker. A `type data` constructor only shows up in types, where it
+     appears as a TyCon, specifically a PromotedDataCon -- no Id in sight.
+
+     See `wrapped_reqd` in GHC.Types.Id.Make.mkDataConRep` for the place where
+     this check is implemented.
+
+     This specifically includes `type data` declarations implemented as GADTs,
+     such as this example from #22948:
+
+        type data T a where
+          A :: T Int
+          B :: T a
+
+     If `T` were an ordinary `data` declaration, then `A` would have a wrapper
+     to account for the GADT-like equality in its return type. Because `T` is
+     declared as a `type data` declaration, however, the wrapper is omitted.
+
+(W1) To prevent users from conjuring up `type data` values at the term level,
+     we disallow using the tagToEnum# function on a type headed by a `type
+     data` type. For instance, GHC will reject this code:
+
+       type data Letter = A | B | C
+
+       f :: Letter
+       f = tagToEnum# 0#
+
+     See `GHC.Tc.Gen.App.checkTagToEnum`, specifically `check_enumeration`.
+
+(W2) Although `type data` data constructors do not exist at the value level,
+     it is still possible to match on a value whose type is headed by a `type data`
+     type constructor, such as this example from #22964:
+
+       type data T a where
+         A :: T Int
+         B :: T a
+
+       f :: T a -> ()
+       f x = case x of {}
+
+     And yet we must guarantee invariant (I1). This has three consequences:
+
+     (W2a) During checking the coverage of `f`'s pattern matches, we treat `T`
+           as if it were an empty data type so that GHC does not warn the user
+           to match against `A` or `B`. (Otherwise, you end up with the bug
+           reported in #22964.)  See GHC.HsToCore.Pmc.Solver.vanillaCompleteMatchTC.
+
+     (W2b) In `GHC.Core.Utils.refineDataAlt`, do /not/ fill in the DEFAULT case
+           with the data constructor, else (I1) is violated. See GHC.Core.Utils
+           Note [Refine DEFAULT case alternatives] Exception 2
+
+     (W2c) In `GHC.Core.Opt.ConstantFold.caseRules`, disable the rule for
+           `dataToTag#` in the case of `type data`.  We do not want to transform
+              case dataToTag# x of t -> blah
+           into
+              case x of { A -> ...; B -> .. }
+           because again that conjures up the type-level-only data contructors
+           `A` and `B` in a pattern, violating (I1) (#23023).
+
 The main parts of the implementation are:
 
-* (R0): The parser recognizes `type data` (but not `type newtype`).
+* The parser recognizes `type data` (but not `type newtype`); this ensures (R0).
 
 * During the initial construction of the AST,
   GHC.Parser.PostProcess.checkNewOrData sets the `Bool` argument of the
@@ -2134,54 +2204,6 @@ The main parts of the implementation are:
   `type data` declarations.  When these are converted back to Hs types
   in a splice, the constructors are placed in the TcCls namespace.
 
-* A `type data` declaration _never_ generates wrappers for its data
-  constructors, as they only make sense for value-level data constructors.
-  See `wrapped_reqd` in GHC.Types.Id.Make.mkDataConRep` for the place where
-  this check is implemented.
-
-  This includes `type data` declarations implemented as GADTs, such as
-  this example from #22948:
-
-    type data T a where
-      A :: T Int
-      B :: T a
-
-  If `T` were an ordinary `data` declaration, then `A` would have a wrapper
-  to account for the GADT-like equality in its return type. Because `T` is
-  declared as a `type data` declaration, however, the wrapper is omitted.
-
-* Although `type data` data constructors do not exist at the value level,
-  it is still possible to match on a value whose type is headed by a `type data`
-  type constructor, such as this example from #22964:
-
-    type data T a where
-      A :: T Int
-      B :: T a
-
-    f :: T a -> ()
-    f x = case x of {}
-
-  This has two consequences:
-
-  * During checking the coverage of `f`'s pattern matches, we treat `T` as if it
-    were an empty data type so that GHC does not warn the user to match against
-    `A` or `B`. (Otherwise, you end up with the bug reported in #22964.)
-    See GHC.HsToCore.Pmc.Solver.vanillaCompleteMatchTC.
-
-  * In `GHC.Core.Utils.refineDataAlt`, do /not/ fill in the DEFAULT case with
-    the data constructor. See
-    Note [Refine DEFAULT case alternatives] Exception 2, in GHC.Core.Utils.
-
-* To prevent users from conjuring up `type data` values at the term level, we
-  disallow using the tagToEnum# function on a type headed by a `type data`
-  type. For instance, GHC will reject this code:
-
-    type data Letter = A | B | C
-
-    f :: Letter
-    f = tagToEnum# 0#
-
-  See `GHC.Tc.Gen.App.checkTagToEnum`, specifically `check_enumeration`.
 -}
 
 warnNoDerivStrat :: Maybe (LDerivStrategy GhcRn)


=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -1222,7 +1222,8 @@ tcTagToEnum tc_fun fun_ctxt tc_args res_ty
     vanilla_result = rebuildHsApps tc_fun fun_ctxt tc_args res_ty
 
     check_enumeration ty' tc
-      | -- isTypeDataTyCon: see Note [Type data declarations] in GHC.Rename.Module
+      | -- isTypeDataTyCon: see wrinkle (W1) in
+        -- Note [Type data declarations] in GHC.Rename.Module
         isTypeDataTyCon tc    = addErrTc (TcRnTagToEnumResTyTypeData ty')
       | isEnumerationTyCon tc = return ()
       | otherwise             = addErrTc (TcRnTagToEnumResTyNotAnEnum ty')


=====================================
docs/users_guide/9.8.1-notes.rst
=====================================
@@ -46,6 +46,7 @@ Runtime system
 ``base`` library
 ~~~~~~~~~~~~~~~~
 
+- ``Data.Tuple`` now exports ``getSolo :: Solo a -> a``.
 
 ``ghc-prim`` library
 ~~~~~~~~~~~~~~~~~~~~


=====================================
libraries/base/Data/Tuple.hs
=====================================
@@ -17,6 +17,7 @@
 
 module Data.Tuple
   ( Solo (..)
+  , getSolo
   , fst
   , snd
   , curry
@@ -25,7 +26,7 @@ module Data.Tuple
   ) where
 
 import GHC.Base ()      -- Note [Depend on GHC.Tuple]
-import GHC.Tuple (Solo (..))
+import GHC.Tuple (Solo (..), getSolo)
 
 default ()              -- Double isn't available yet
 


=====================================
libraries/base/changelog.md
=====================================
@@ -7,6 +7,8 @@
   * Refactor `generalCategory` to stop very large literal string being inlined to call-sites.
       ([CLC proposal #130](https://github.com/haskell/core-libraries-committee/issues/130))
   * Add INLINABLE pragmas to `generic*` functions in Data.OldList ([CLC proposal #129](https://github.com/haskell/core-libraries-committee/issues/130))
+  * Export `getSolo` from `Data.Tuple`.
+      ([CLC proposal #113](https://github.com/haskell/core-libraries-committee/issues/113))
 
 ## 4.18.0.0 *TBA*
 


=====================================
libraries/ghc-prim/GHC/Tuple/Prim.hs
=====================================
@@ -79,6 +79,26 @@ data () = ()
 -- implementations of lazy and strict mapping functions.
 data Solo a = MkSolo a
 
+-- | Extract the value from a 'Solo'. Very often, values should be extracted
+-- directly using pattern matching, to control just what gets evaluated when.
+-- @getSolo@ is for convenience in situations where that is not the case:
+--
+-- When the result is passed to a /strict/ function, it makes no difference
+-- whether the pattern matching is done on the \"outside\" or on the
+-- \"inside\":
+--
+-- @
+-- Data.Set.insert (getSolo sol) set === case sol of Solo v -> Data.Set.insert v set
+-- @
+--
+-- A traversal may be performed in 'Solo' in order to control evaluation
+-- internally, while using @getSolo@ to extract the final result. A strict
+-- mapping function, for example, could be defined
+--
+-- @
+-- map' :: Traversable t => (a -> b) -> t a -> t b
+-- map' f = getSolo . traverse ((Solo $!) . f)
+-- @
 getSolo :: Solo a -> a
 -- getSolo is a standalone function, rather than a record field of Solo,
 -- because Solo is a wired-in TyCon, and a wired-in TyCon that  has


=====================================
testsuite/tests/gadt/T23022.hs
=====================================
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeData #-}
+module B where
+
+type data T a b where
+  MkT :: T a a
+
+f :: T a b -> T a b
+f x = x


=====================================
testsuite/tests/gadt/T23023.hs
=====================================
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeData, MagicHash #-}
+module B where
+
+import GHC.Exts
+
+type data T a b where
+  MkT :: T a a
+
+f :: T Int Bool -> Char
+f x = case dataToTag# x of
+         0# -> 'a'
+         _  -> 'b'


=====================================
testsuite/tests/gadt/all.T
=====================================
@@ -129,3 +129,5 @@ test('T22235', normal, compile, [''])
 test('T19847', normal, compile, [''])
 test('T19847a', normal, compile, ['-ddump-types'])
 test('T19847b', normal, compile, [''])
+test('T23022', normal, compile, ['-dcore-lint'])
+test('T23023', normal, compile, ['-dcore-lint'])


=====================================
testsuite/tests/polykinds/T22793.hs
=====================================
@@ -0,0 +1,17 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+module T22793 where
+
+import Data.Kind
+
+type Foo :: forall k. k -> k -> Constraint
+
+class Foo s a
+
+bob :: forall {k1} {ks} {ka} q (p :: k1 -> q -> Type)
+              (f :: ka -> q) (s :: ks) (t :: ks)
+              (a :: ka) (b :: ka). Foo s a
+     => p a (f b) -> p s (f t)
+bob f = undefined


=====================================
testsuite/tests/polykinds/T22793.stderr
=====================================
@@ -0,0 +1,44 @@
+
+T22793.hs:15:42: error: [GHC-25897]
+    • Couldn't match kind ‘ka’ with ‘k1’
+      Expected kind ‘ks’, but ‘a’ has kind ‘ka’
+      ‘ka’ is a rigid type variable bound by
+        the type signature for ‘bob’
+        at T22793.hs:13:26-27
+      ‘k1’ is a rigid type variable bound by
+        the type signature for ‘bob’
+        at T22793.hs:13:16-17
+    • In the second argument of ‘Foo’, namely ‘a’
+      In the type signature:
+        bob :: forall {k1}
+                      {ks}
+                      {ka}
+                      q
+                      (p :: k1 -> q -> Type)
+                      (f :: ka -> q)
+                      (s :: ks)
+                      (t :: ks)
+                      (a :: ka)
+                      (b :: ka). Foo s a => p a (f b) -> p s (f t)
+
+T22793.hs:16:11: error: [GHC-25897]
+    • Couldn't match kind ‘ks’ with ‘k1’
+      Expected kind ‘k1’, but ‘a’ has kind ‘ka’
+      ‘ks’ is a rigid type variable bound by
+        the type signature for ‘bob’
+        at T22793.hs:13:21-22
+      ‘k1’ is a rigid type variable bound by
+        the type signature for ‘bob’
+        at T22793.hs:13:16-17
+    • In the first argument of ‘p’, namely ‘a’
+      In the type signature:
+        bob :: forall {k1}
+                      {ks}
+                      {ka}
+                      q
+                      (p :: k1 -> q -> Type)
+                      (f :: ka -> q)
+                      (s :: ks)
+                      (t :: ks)
+                      (a :: ka)
+                      (b :: ka). Foo s a => p a (f b) -> p s (f t)


=====================================
testsuite/tests/polykinds/all.T
=====================================
@@ -243,3 +243,4 @@ test('T22379a', normal, compile, [''])
 test('T22379b', normal, compile, [''])
 test('T22743', normal, compile_fail, [''])
 test('T22742', normal, compile_fail, [''])
+test('T22793', normal, compile_fail, [''])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/6ba4a2dda4abf17d36b55cd7625bbfa160a5b1f9...c7c1a73b6e93e505b06736cbb6f8be79fdca32c1

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/6ba4a2dda4abf17d36b55cd7625bbfa160a5b1f9...c7c1a73b6e93e505b06736cbb6f8be79fdca32c1
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230303/545100df/attachment-0001.html>


More information about the ghc-commits mailing list