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

6 files changed, 181 insertions, 20 deletions

diff --git a/libraries/base/Data/Typeable.hs b/libraries/base/Data/Typeable.hs
index 6885152308..9b90698e81 100644
--- a/libraries/base/Data/Typeable.hs
+++ b/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))
diff --git a/libraries/base/Data/Typeable/Internal.hs b/libraries/base/Data/Typeable/Internal.hs
index 51ee0f745e..5ecdd49036 100644
--- a/libraries/base/Data/Typeable/Internal.hs
+++ 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
diff --git a/libraries/base/GHC/TypeLits.hs b/libraries/base/GHC/TypeLits.hs
index ebd93232e8..288ec39fc2 100644
--- a/libraries/base/GHC/TypeLits.hs
+++ b/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
diff --git a/libraries/base/GHC/TypeNats.hs b/libraries/base/GHC/TypeNats.hs
index 5a460d11c6..66361d66db 100644
--- a/libraries/base/GHC/TypeNats.hs
+++ b/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
diff --git a/libraries/base/Type/Reflection.hs b/libraries/base/Type/Reflection.hs
index cf10412a9d..e2db4a93d2 100644
--- a/libraries/base/Type/Reflection.hs
+++ b/libraries/base/Type/Reflection.hs
@@ -44,6 +44,7 @@ module Type.Reflection
     , I.typeRepTyCon
     , I.rnfTypeRep
     , I.eqTypeRep
+    , I.decTypeRep
     , I.typeRepKind
     , I.splitApps
 
diff --git a/libraries/base/changelog.md b/libraries/base/changelog.md
index 6772033780..9285d8994f 100644
--- a/libraries/base/changelog.md
+++ b/libraries/base/changelog.md
@@ -9,6 +9,8 @@
   * 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*