[Git][ghc/ghc][wip/marge_bot_batch_merge_job] 5 commits: Export getSolo from Data.Tuple

Marge Bot (@marge-bot) gitlab at gitlab.haskell.org
Sat Mar 4 03:47:50 UTC 2023



Marge Bot pushed to branch wip/marge_bot_batch_merge_job 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>

- - - - -
858f34d5 by Oleg Grenrus at 2023-03-04T01:13:55+02:00
Add decideSymbol, decideChar, decideNat, decTypeRep, decT and hdecT

These all type-level equality decision procedures.

Implementes a CLC proposal https://github.com/haskell/core-libraries-committee/issues/98

- - - - -
1121bb3a by Simon Peyton Jones at 2023-03-03T22:47:38-05:00
Add test for T22793

- - - - -


23 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/Data/Typeable.hs
- libraries/base/Data/Typeable/Internal.hs
- libraries/base/GHC/TypeLits.hs
- libraries/base/GHC/TypeNats.hs
- libraries/base/Type/Reflection.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/ghci/scripts/T9181.stdout
- + 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/Data/Typeable.hs
=====================================
@@ -58,6 +58,8 @@ module Data.Typeable
     , cast
     , eqT
     , heqT
+    , decT
+    , hdecT
     , gcast                -- a generalisation of cast
 
       -- * Generalized casts for higher-order kinds
@@ -99,6 +101,7 @@ import qualified Data.Typeable.Internal as I
 import Data.Typeable.Internal (Typeable)
 import Data.Type.Equality
 
+import Data.Either
 import Data.Maybe
 import Data.Proxy
 import GHC.Fingerprint.Type
@@ -140,6 +143,14 @@ eqT
   | Just HRefl <- heqT @a @b = Just Refl
   | otherwise                = Nothing
 
+-- | Decide an equality of two types
+--
+-- @since 4.19.0.0
+decT :: forall a b. (Typeable a, Typeable b) => Either (a :~: b -> Void) (a :~: b)
+decT = case hdecT @a @b of
+  Right HRefl -> Right Refl
+  Left p      -> Left (\Refl -> p HRefl)
+
 -- | Extract a witness of heterogeneous equality of two types
 --
 -- @since 4.18.0.0
@@ -149,6 +160,15 @@ heqT = ta `I.eqTypeRep` tb
     ta = I.typeRep :: I.TypeRep a
     tb = I.typeRep :: I.TypeRep b
 
+-- | Decide heterogeneous equality of two types.
+--
+-- @since 4.19.0.0
+hdecT :: forall a b. (Typeable a, Typeable b) => Either (a :~~: b -> Void) (a :~~: b)
+hdecT = ta `I.decTypeRep` tb
+  where
+    ta = I.typeRep :: I.TypeRep a
+    tb = I.typeRep :: I.TypeRep b
+
 -- | A flexible variation parameterised in a type constructor
 gcast :: forall a b c. (Typeable a, Typeable b) => c a -> Maybe (c b)
 gcast x = fmap (\Refl -> x) (eqT :: Maybe (a :~: b))


=====================================
libraries/base/Data/Typeable/Internal.hs
=====================================
@@ -66,6 +66,7 @@ module Data.Typeable.Internal (
     typeRepFingerprint,
     rnfTypeRep,
     eqTypeRep,
+    decTypeRep,
     typeRepKind,
     splitApps,
 
@@ -88,6 +89,7 @@ module Data.Typeable.Internal (
 
 import GHC.Base
 import qualified GHC.Arr as A
+import Data.Either (Either (..))
 import Data.Type.Equality
 import GHC.List ( splitAt, foldl', elem )
 import GHC.Word
@@ -611,14 +613,48 @@ typeRepTyCon (TrFun {})               = typeRepTyCon $ typeRep @(->)
 -- @since 4.10
 eqTypeRep :: forall k1 k2 (a :: k1) (b :: k2).
              TypeRep a -> TypeRep b -> Maybe (a :~~: b)
-eqTypeRep a b
-  | sameTypeRep a b = Just (unsafeCoerce HRefl)
-  | otherwise       = Nothing
--- We want GHC to inline eqTypeRep to get rid of the Maybe
--- in the usual case that it is scrutinized immediately. We
--- split eqTypeRep into a worker and wrapper because otherwise
--- it's much larger than anything we'd want to inline.
-{-# INLINABLE eqTypeRep #-}
+eqTypeRep a b = case inline decTypeRep a b of
+                  -- inline: see wrinkle (I1) in Note [Inlining eqTypeRep/decTypeRep]
+  Right p -> Just p
+  Left _  -> Nothing
+
+-- | Type equality decision
+--
+-- @since 4.19.0.0
+decTypeRep :: forall k1 k2 (a :: k1) (b :: k2).
+             TypeRep a -> TypeRep b -> Either (a :~~: b -> Void) (a :~~: b)
+decTypeRep a b
+  | sameTypeRep a b = Right (unsafeCoerce HRefl)
+  | otherwise       = Left (\HRefl -> errorWithoutStackTrace ("decTypeRep: Impossible equality proof " ++ show a ++ " :~: " ++ show b))
+
+{-# INLINEABLE eqTypeRep #-}
+{-# INLINEABLE decTypeRep #-}
+
+{-
+Note [Inlining eqTypeRep/decTypeRep]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+We want GHC to inline eqTypeRep and decTypeRep to get rid of the Maybe
+and Either in the usual case that it is scrutinized immediately. We
+split them into a worker (sameTypeRep) and wrappers because otherwise
+it's much larger than anything we'd want to inline.
+
+We need INLINEABLE on the eqTypeRep and decTypeRep as GHC
+seems to want to inline sameTypeRep here, making tham bigger.
+By exposing exact RHS, they stay small and other optimizations may
+fire first, so GHC can realise that inlining sameTypeRep is often
+(but not always) a bad idea.
+
+Wrinkle I1:
+
+`inline decTypeRep` in eqTypeRep implementation is to ensure that `decTypeRep`
+is inlined, even it's somewhat big of expression, but we know that big Left
+branch will be optimized away.
+
+See discussion in https://gitlab.haskell.org/ghc/ghc/-/merge_requests/9524
+and also https://gitlab.haskell.org/ghc/ghc/-/issues/22635
+
+-}
 
 sameTypeRep :: forall k1 k2 (a :: k1) (b :: k2).
                TypeRep a -> TypeRep b -> Bool


=====================================
libraries/base/GHC/TypeLits.hs
=====================================
@@ -44,6 +44,7 @@ module GHC.TypeLits
   , N.SomeNat(..), SomeSymbol(..), SomeChar(..)
   , someNatVal, someSymbolVal, someCharVal
   , N.sameNat, sameSymbol, sameChar
+  , N.decideNat, decideSymbol, decideChar
   , OrderingI(..)
   , N.cmpNat, cmpSymbol, cmpChar
     -- ** Singleton values
@@ -68,7 +69,8 @@ module GHC.TypeLits
   ) where
 
 import GHC.Base ( Eq(..), Functor(..), Ord(..), Ordering(..), String
-                , (.), otherwise, withDict )
+                , (.), otherwise, withDict, Void, (++)
+                , errorWithoutStackTrace)
 import GHC.Types(Symbol, Char, TYPE)
 import GHC.TypeError(ErrorMessage(..), TypeError)
 import GHC.Num(Integer, fromInteger)
@@ -76,7 +78,8 @@ import GHC.Show(Show(..), appPrec, appPrec1, showParen, showString)
 import GHC.Read(Read(..))
 import GHC.Real(toInteger)
 import GHC.Prim(Proxy#)
-import Data.Maybe(Maybe(..))
+import Data.Either (Either (..))
+import Data.Maybe (Maybe(..))
 import Data.Proxy (Proxy(..))
 import Data.Type.Coercion (Coercion(..), TestCoercion(..))
 import Data.Type.Equality((:~:)(Refl), TestEquality(..))
@@ -224,6 +227,20 @@ sameSymbol :: forall a b proxy1 proxy2.
               proxy1 a -> proxy2 b -> Maybe (a :~: b)
 sameSymbol _ _ = testEquality (symbolSing @a) (symbolSing @b)
 
+-- | We either get evidence that this function was instantiated with the
+-- same type-level symbols, or that the type-level symbols are distinct.
+--
+-- @since 4.19.0.0
+decideSymbol :: forall a b proxy1 proxy2.
+              (KnownSymbol a, KnownSymbol b) =>
+              proxy1 a -> proxy2 b -> Either (a :~: b -> Void) (a :~: b)
+decideSymbol _ _ = decSymbol (symbolSing @a) (symbolSing @b)
+
+-- Not exported: See [Not exported decNat, decSymbol and decChar]
+decSymbol :: SSymbol a -> SSymbol b -> Either (a :~: b -> Void) (a :~: b)
+decSymbol (UnsafeSSymbol x) (UnsafeSSymbol y)
+  | x == y    = Right (unsafeCoerce Refl)
+  | otherwise = Left (\Refl -> errorWithoutStackTrace ("decideSymbol: Impossible equality proof " ++ show x ++ " :~: " ++ show y))
 
 -- | We either get evidence that this function was instantiated with the
 -- same type-level characters, or 'Nothing'.
@@ -234,6 +251,21 @@ sameChar :: forall a b proxy1 proxy2.
             proxy1 a -> proxy2 b -> Maybe (a :~: b)
 sameChar _ _ = testEquality (charSing @a) (charSing @b)
 
+-- | We either get evidence that this function was instantiated with the
+-- same type-level characters, or that the type-level characters are distinct.
+--
+-- @since 4.19.0.0
+decideChar :: forall a b proxy1 proxy2.
+            (KnownChar a, KnownChar b) =>
+            proxy1 a -> proxy2 b -> Either (a :~: b -> Void) (a :~: b)
+decideChar _ _ = decChar (charSing @a) (charSing @b)
+
+-- Not exported: See [Not exported decNat, decSymbol and decChar]
+decChar :: SChar a -> SChar b -> Either (a :~: b -> Void) (a :~: b)
+decChar (UnsafeSChar x) (UnsafeSChar y)
+  | x == y    = Right (unsafeCoerce Refl)
+  | otherwise = Left (\Refl -> errorWithoutStackTrace ("decideChar: Impossible equality proof " ++ show x ++ " :~: " ++ show y))
+
 -- | Like 'sameSymbol', but if the symbols aren't equal, this additionally
 -- provides proof of LT or GT.
 --
@@ -352,9 +384,9 @@ instance Show (SSymbol s) where
 
 -- | @since 4.18.0.0
 instance TestEquality SSymbol where
-  testEquality (UnsafeSSymbol x) (UnsafeSSymbol y)
-    | x == y    = Just (unsafeCoerce Refl)
-    | otherwise = Nothing
+  testEquality a b = case decSymbol a b of
+    Right p -> Just p
+    Left _  -> Nothing
 
 -- | @since 4.18.0.0
 instance TestCoercion SSymbol where
@@ -445,9 +477,9 @@ instance Show (SChar c) where
 
 -- | @since 4.18.0.0
 instance TestEquality SChar where
-  testEquality (UnsafeSChar x) (UnsafeSChar y)
-    | x == y    = Just (unsafeCoerce Refl)
-    | otherwise = Nothing
+  testEquality a b = case decChar a b of
+    Right p -> Just p
+    Left _  -> Nothing
 
 -- | @since 4.18.0.0
 instance TestCoercion SChar where


=====================================
libraries/base/GHC/TypeNats.hs
=====================================
@@ -33,6 +33,7 @@ module GHC.TypeNats
   , SomeNat(..)
   , someNatVal
   , sameNat
+  , decideNat
     -- ** Singleton values
   , SNat
   , pattern SNat
@@ -48,12 +49,14 @@ module GHC.TypeNats
 
   ) where
 
-import GHC.Base(Eq(..), Functor(..), Ord(..), WithDict(..), (.), otherwise)
+import GHC.Base( Eq(..), Functor(..), Ord(..), WithDict(..), (.), otherwise
+               , Void, errorWithoutStackTrace, (++))
 import GHC.Types
 import GHC.Num.Natural(Natural)
 import GHC.Show(Show(..), appPrec, appPrec1, showParen, showString)
 import GHC.Read(Read(..))
 import GHC.Prim(Proxy#)
+import Data.Either(Either(..))
 import Data.Maybe(Maybe(..))
 import Data.Proxy (Proxy(..))
 import Data.Type.Coercion (Coercion(..), TestCoercion(..))
@@ -239,6 +242,73 @@ sameNat :: forall a b proxy1 proxy2.
            proxy1 a -> proxy2 b -> Maybe (a :~: b)
 sameNat _ _ = testEquality (natSing @a) (natSing @b)
 
+-- | We either get evidence that this function was instantiated with the
+-- same type-level numbers, or that the type-level numbers are distinct.
+--
+-- @since 4.19.0.0
+decideNat :: forall a b proxy1 proxy2.
+           (KnownNat a, KnownNat b) =>
+           proxy1 a -> proxy2 b -> Either (a :~: b -> Void) (a :~: b)
+decideNat _ _ = decNat (natSing @a) (natSing @b)
+
+-- Not exported: See [Not exported decNat, decSymbol and decChar]
+decNat :: SNat a -> SNat b -> Either (a :~: b -> Void) (a :~: b)
+decNat (UnsafeSNat x) (UnsafeSNat y)
+  | x == y    = Right (unsafeCoerce Refl)
+  | otherwise = Left (\Refl -> errorWithoutStackTrace ("decideNat: Impossible equality proof " ++ show x ++ " :~: " ++ show y))
+
+{-
+Note [Not exported decNat, decSymbol and decChar]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+The decNat, decSymbol and decChar are not (yet) exported.
+
+There are two development paths:
+1. export them.
+2. Add `decideEquality :: f a -> f b -> Either (a :~: b -> Void) (a :~: b)`
+   to the `Data.Type.Equality.TestEquality` typeclass.
+
+The second option looks nicer given the current base API:
+there aren't `eqNat :: SNat a -> SNat b -> Maybe (a :~: b)` like functions,
+they are abstracted by `TestEquality` typeclass.
+
+Also TestEquality class has a law that testEquality result
+should be Just Refl iff the types applied to are equal:
+
+testEquality (x :: f a) (y :: f b) = Just Refl  <=> a = b
+
+As consequence we have that testEquality should be Nothing
+iff the types applied are inequal:
+
+testEquality (x :: f a) (y :: f b) = Nothing   <=> a /= b
+
+And the decideEquality would enforce that.
+
+However, adding a new method is a breaking change,
+as default implementation cannot be (safely) provided.
+Also there are unlawful instances of `TestEquality` out there,
+(e.g. https://hackage.haskell.org/package/parameterized-utils Index instance
+      https://hackage.haskell.org/package/witness various types)
+which makes adding unsafe default implementation a bad idea.
+
+Adding own typeclass:
+
+class TestEquality f => DecideEquality f where
+  decideEquality :: f a -> f b -> Either (a :~: b -> Void) (a :~: b)
+
+is bad design, as `TestEquality` already implies that it should be possible.
+In other words, every f with (lawful) `TestEquality` instance should have
+`DecideEquality` instance as well.
+
+We hold on doing either 1. or 2. yet, as doing 2. is "harder",
+but if it is done eventually, doing 1. is pointless.
+In other words the paths can be thought as mutually exclusive.
+
+Fortunately the dec* functions can be simulated using decide* variants
+if needed, so there is no hurry to commit to either development paths.
+
+-}
+
 -- | Like 'sameNat', but if the numbers aren't equal, this additionally
 -- provides proof of LT or GT.
 --
@@ -318,9 +388,9 @@ instance Show (SNat n) where
 
 -- | @since 4.18.0.0
 instance TestEquality SNat where
-  testEquality (UnsafeSNat x) (UnsafeSNat y)
-    | x == y    = Just (unsafeCoerce Refl)
-    | otherwise = Nothing
+  testEquality a b = case decNat a b of
+    Right x -> Just x
+    Left _  -> Nothing
 
 -- | @since 4.18.0.0
 instance TestCoercion SNat where


=====================================
libraries/base/Type/Reflection.hs
=====================================
@@ -44,6 +44,7 @@ module Type.Reflection
     , I.typeRepTyCon
     , I.rnfTypeRep
     , I.eqTypeRep
+    , I.decTypeRep
     , I.typeRepKind
     , I.splitApps
 


=====================================
libraries/base/changelog.md
=====================================
@@ -7,6 +7,10 @@
   * 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))
+  * Add `Type.Reflection.decTypeRep`, `Data.Typeable.decT` and `Data.Typeable.hdecT` equality decisions functions.
+      ([CLC proposal #98](https://github.com/haskell/core-libraries-committee/issues/98))
 
 ## 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/ghci/scripts/T9181.stdout
=====================================
@@ -48,6 +48,20 @@ GHC.TypeLits.cmpChar ::
 GHC.TypeLits.cmpSymbol ::
   (GHC.TypeLits.KnownSymbol a, GHC.TypeLits.KnownSymbol b) =>
   proxy1 a -> proxy2 b -> Data.Type.Ord.OrderingI a b
+GHC.TypeLits.decideChar ::
+  (GHC.TypeLits.KnownChar a, GHC.TypeLits.KnownChar b) =>
+  proxy1 a
+  -> proxy2 b
+  -> Either
+       ((a Data.Type.Equality.:~: b) -> GHC.Base.Void)
+       (a Data.Type.Equality.:~: b)
+GHC.TypeLits.decideSymbol ::
+  (GHC.TypeLits.KnownSymbol a, GHC.TypeLits.KnownSymbol b) =>
+  proxy1 a
+  -> proxy2 b
+  -> Either
+       ((a Data.Type.Equality.:~: b) -> GHC.Base.Void)
+       (a Data.Type.Equality.:~: b)
 GHC.TypeLits.fromSChar :: GHC.TypeLits.SChar c -> Char
 GHC.TypeLits.fromSNat :: GHC.TypeNats.SNat n -> Integer
 GHC.TypeLits.fromSSymbol :: GHC.TypeLits.SSymbol s -> String
@@ -172,6 +186,13 @@ type family (GHC.TypeNats.^) a b
 GHC.TypeNats.cmpNat ::
   (GHC.TypeNats.KnownNat a, GHC.TypeNats.KnownNat b) =>
   proxy1 a -> proxy2 b -> Data.Type.Ord.OrderingI a b
+GHC.TypeNats.decideNat ::
+  (GHC.TypeNats.KnownNat a, GHC.TypeNats.KnownNat b) =>
+  proxy1 a
+  -> proxy2 b
+  -> Either
+       ((a Data.Type.Equality.:~: b) -> GHC.Base.Void)
+       (a Data.Type.Equality.:~: b)
 GHC.TypeNats.sameNat ::
   (GHC.TypeNats.KnownNat a, GHC.TypeNats.KnownNat b) =>
   proxy1 a -> proxy2 b -> Maybe (a Data.Type.Equality.:~: b)


=====================================
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/20d09ee2373cc340e76edfd01c31220864d778c6...1121bb3a87c4d05725b0491441113641a90a3bc7

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/20d09ee2373cc340e76edfd01c31220864d778c6...1121bb3a87c4d05725b0491441113641a90a3bc7
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/66cdde1e/attachment-0001.html>


More information about the ghc-commits mailing list