[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