Improve error messages involving operators from Data.Type.Ord

Fixes #20009

11 files changed, 234 insertions, 77 deletions

diff --git a/compiler/GHC/Builtin/Names.hs b/compiler/GHC/Builtin/Names.hs
index 913b8a4ed9..d5da296cb6 100644
--- a/compiler/GHC/Builtin/Names.hs
+++ b/compiler/GHC/Builtin/Names.hs
@@ -559,7 +559,7 @@ gHC_PRIM, gHC_PRIM_PANIC, gHC_PRIM_EXCEPTION,
     tYPEABLE, tYPEABLE_INTERNAL, gENERICS,
     rEAD_PREC, lEX, gHC_INT, gHC_WORD, mONAD, mONAD_FIX, mONAD_ZIP, mONAD_FAIL,
     aRROW, gHC_DESUGAR, rANDOM, gHC_EXTS,
-    cONTROL_EXCEPTION_BASE, gHC_TYPELITS, gHC_TYPELITS_INTERNAL,
+    cONTROL_EXCEPTION_BASE, gHC_TYPEERROR, gHC_TYPELITS, gHC_TYPELITS_INTERNAL,
     gHC_TYPENATS, gHC_TYPENATS_INTERNAL,
     dATA_COERCE, dEBUG_TRACE, uNSAFE_COERCE :: Module
 
@@ -621,6 +621,7 @@ rANDOM          = mkBaseModule (fsLit "System.Random")
 gHC_EXTS        = mkBaseModule (fsLit "GHC.Exts")
 cONTROL_EXCEPTION_BASE = mkBaseModule (fsLit "Control.Exception.Base")
 gHC_GENERICS    = mkBaseModule (fsLit "GHC.Generics")
+gHC_TYPEERROR   = mkBaseModule (fsLit "GHC.TypeError")
 gHC_TYPELITS    = mkBaseModule (fsLit "GHC.TypeLits")
 gHC_TYPELITS_INTERNAL = mkBaseModule (fsLit "GHC.TypeLits.Internal")
 gHC_TYPENATS    = mkBaseModule (fsLit "GHC.TypeNats")
@@ -1455,19 +1456,19 @@ errorMessageTypeErrorFamName
   :: Name
 
 errorMessageTypeErrorFamName =
-  tcQual gHC_TYPELITS (fsLit "TypeError") errorMessageTypeErrorFamKey
+  tcQual gHC_TYPEERROR (fsLit "TypeError") errorMessageTypeErrorFamKey
 
 typeErrorTextDataConName =
-  dcQual gHC_TYPELITS (fsLit "Text") typeErrorTextDataConKey
+  dcQual gHC_TYPEERROR (fsLit "Text") typeErrorTextDataConKey
 
 typeErrorAppendDataConName =
-  dcQual gHC_TYPELITS (fsLit ":<>:") typeErrorAppendDataConKey
+  dcQual gHC_TYPEERROR (fsLit ":<>:") typeErrorAppendDataConKey
 
 typeErrorVAppendDataConName =
-  dcQual gHC_TYPELITS (fsLit ":$$:") typeErrorVAppendDataConKey
+  dcQual gHC_TYPEERROR (fsLit ":$$:") typeErrorVAppendDataConKey
 
 typeErrorShowTypeDataConName =
-  dcQual gHC_TYPELITS (fsLit "ShowType") typeErrorShowTypeDataConKey
+  dcQual gHC_TYPEERROR (fsLit "ShowType") typeErrorShowTypeDataConKey
 
 -- Unsafe coercion proofs
 unsafeEqualityProofName, unsafeEqualityTyConName, unsafeCoercePrimName,
diff --git a/docs/users_guide/9.2.1-notes.rst b/docs/users_guide/9.2.1-notes.rst
index c1b8d94661..a80218098e 100644
--- a/docs/users_guide/9.2.1-notes.rst
+++ b/docs/users_guide/9.2.1-notes.rst
@@ -393,3 +393,7 @@ Eventlog
       (True,  True)  -> 1
       (False, False) -> 2
       (True,  False) | considerAccessible -> 3 -- No warning!
+
+- A new ``GHC.TypeError`` module is created which exposes functionality related
+  to custom type errors. ``TypeError`` is re-exported from ``GHC.TypeLits`` for
+  backwards compatibility.
diff --git a/libraries/base/Data/Type/Ord.hs b/libraries/base/Data/Type/Ord.hs
index 87c17c00cd..fa84754115 100644
--- a/libraries/base/Data/Type/Ord.hs
+++ b/libraries/base/Data/Type/Ord.hs
@@ -3,7 +3,7 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE NoImplicitPrelude #-}
 {-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE StandaloneKindSignatures #-}
 {-# LANGUAGE TypeFamilies #-}
@@ -35,6 +35,7 @@ module Data.Type.Ord (
   ) where
 
 import GHC.Show(Show(..))
+import GHC.TypeError
 import GHC.TypeLits.Internal
 import GHC.TypeNats.Internal
 import Data.Bool
@@ -64,29 +65,31 @@ data OrderingI a b where
 deriving instance Show (OrderingI a b)
 deriving instance Eq   (OrderingI a b)
 
-
 infix 4 <=?, <=, >=?, >=, <?, <, >?, >
 
 -- | Comparison (<=) of comparable types, as a constraint.
 --
 -- @since 4.16.0.0
-type x <= y = (x <=? y) ~ 'True
+type x <= y = Assert (x <=? y) (LeErrMsg x y)
+type LeErrMsg x y = TypeError ('Text "Cannot satisfy: " ':<>: 'ShowType x ':<>: 'Text " <= " ':<>: 'ShowType y)
 
 -- | Comparison (>=) of comparable types, as a constraint.
 --
 -- @since 4.16.0.0
-type x >= y = (x >=? y) ~ 'True
+type x >= y = Assert (x >=? y) (GeErrMsg x y)
+type GeErrMsg x y = TypeError ('Text "Cannot satisfy: " ':<>: 'ShowType x ':<>: 'Text " >= " ':<>: 'ShowType y)
 
 -- | Comparison (<) of comparable types, as a constraint.
 --
 -- @since 4.16.0.0
-type x < y = (x >? y) ~ 'True
+type x < y = Assert (x <? y) (LtErrMsg x y)
+type LtErrMsg x y = TypeError ('Text "Cannot satisfy: " ':<>: 'ShowType x ':<>: 'Text " < " ':<>: 'ShowType y)
 
 -- | Comparison (>) of comparable types, as a constraint.
 --
 -- @since 4.16.0.0
-type x > y = (x >? y) ~ 'True
-
+type x > y = Assert (x >? y) (GtErrMsg x y)
+type GtErrMsg x y = TypeError ('Text "Cannot satisfy: " ':<>: 'ShowType x ':<>: 'Text " > " ':<>: 'ShowType y)
 
 -- | Comparison (<=) of comparable types, as a function.
 --
diff --git a/libraries/base/GHC/TypeError.hs b/libraries/base/GHC/TypeError.hs
new file mode 100644
index 0000000000..a74f573ae2
--- /dev/null
+++ b/libraries/base/GHC/TypeError.hs
@@ -0,0 +1,141 @@
+{-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# OPTIONS_HADDOCK not-home #-}
+
+{-|
+This module exports the TypeError family, which is used to provide custom type
+errors, and the ErrorMessage kind used to define these custom error messages.
+This is a type-level analogue to the term level error function.
+
+@since 4.16.0.0
+-}
+
+module GHC.TypeError
+  ( ErrorMessage (..)
+  , TypeError
+  , Assert
+  ) where
+
+import Data.Bool
+import GHC.Num.Integer () -- See Note [Depend on GHC.Num.Integer] in GHC.Base
+import GHC.Types (Constraint, Symbol)
+
+{-
+Note [Custom type errors]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+TypeError is used to provide custom type errors, similar to the term-level
+error function. TypeError is somewhat magical: when the constraint solver
+encounters a constraint where the RHS is TypeError, it reports the error to
+GHC. Later, GHC renders this error for display to the user (see the function
+GHC.Tc.Errors.mkUserTypeErrorReporter).
+
+See also the wiki page on custom type errors:
+https://gitlab.haskell.org/ghc/ghc/-/wikis/proposal/custom-type-errors
+-}
+
+-- | A description of a custom type error.
+data {-kind-} ErrorMessage = Text Symbol
+                             -- ^ Show the text as is.
+
+                           | forall t. ShowType t
+                             -- ^ Pretty print the type.
+                             -- @ShowType :: k -> ErrorMessage@
+
+                           | ErrorMessage :<>: ErrorMessage
+                             -- ^ Put two pieces of error message next
+                             -- to each other.
+
+                           | ErrorMessage :$$: ErrorMessage
+                             -- ^ Stack two pieces of error message on top
+                             -- of each other.
+
+infixl 5 :$$:
+infixl 6 :<>:
+
+-- | The type-level equivalent of 'Prelude.error'.
+--
+-- The polymorphic kind of this type allows it to be used in several settings.
+-- For instance, it can be used as a constraint, e.g. to provide a better error
+-- message for a non-existent instance,
+--
+-- @
+-- -- in a context
+-- instance TypeError (Text "Cannot 'Show' functions." :$$:
+--                     Text "Perhaps there is a missing argument?")
+--       => Show (a -> b) where
+--     showsPrec = error "unreachable"
+-- @
+--
+-- It can also be placed on the right-hand side of a type-level function
+-- to provide an error for an invalid case,
+--
+-- @
+-- type family ByteSize x where
+--    ByteSize Word16   = 2
+--    ByteSize Word8    = 1
+--    ByteSize a        = TypeError (Text "The type " :<>: ShowType a :<>:
+--                                   Text " is not exportable.")
+-- @
+--
+-- @since 4.9.0.0
+type family TypeError (a :: ErrorMessage) :: b where
+
+{-
+Note [Getting good error messages from boolean comparisons]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We want to write types like
+
+  f :: forall (x :: Int) (y :: Int). (x <= y) => T x -> T y
+
+so we need (<=) :: Int -> Int -> Constraint. We already have
+(<=?) :: Int -> Int -> Bool, defined in Data.Type.Ord. One obvious way to get
+(<=) is to say
+
+  type (<=) x y = (x <=? y) ~ True
+
+But suppose we call (f @4 @2); then we get the constraint (4 <=? 2) ~ True
+which simplifies to False ~ True, which gives a very poor error message.
+
+So we adopt a different idiom:
+
+  type (<=) x y = Assert (x <=? y) (LeErrMsg x y)
+
+The Assert function is defined so that
+
+  Assert True msg ===> ()
+
+so as soon as (x <=? y) evaluates to True, the Assert disappears. But as soon
+as (x <=? y) is apart from True (i.e. cannot evaluate to True) the second
+equation of Assert kicks in, and
+
+  Assert non-true msg ==> msg
+-}
+
+-- | A type-level assert function.
+--
+-- If the first argument evaluates to true, then the empty constraint is
+-- returned, otherwise the second argument (which is intended to be something
+-- which reduces to 'TypeError' is used).
+--
+-- For example, given some type level predicate @P' :: Type -> Bool@, it is
+-- possible to write the type synonym
+--
+-- @
+-- type P a = Assert (P' a) (NotPError a)
+-- @
+--
+-- where @NotPError@ reduces to a @TypeError@ which is reported if the
+-- assertion fails.
+--
+-- @since 4.16.0.0
+--
+type Assert :: Bool -> Constraint -> Constraint
+type family Assert check errMsg where
+  Assert 'True _      = ()
+  Assert _     errMsg = errMsg
+  -- See Note [Getting good error messages from boolean comparisons]
diff --git a/libraries/base/GHC/TypeLits.hs b/libraries/base/GHC/TypeLits.hs
index 79759f2b87..97b922c79e 100644
--- a/libraries/base/GHC/TypeLits.hs
+++ b/libraries/base/GHC/TypeLits.hs
@@ -10,7 +10,6 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE NoImplicitPrelude #-}
 {-# LANGUAGE MagicHash #-}
-{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE TypeApplications #-}
 
 {-|
@@ -61,6 +60,7 @@ module GHC.TypeLits
 
 import GHC.Base(Eq(..), Ord(..), Ordering(..), String, otherwise, withDict)
 import GHC.Types(Symbol, Char)
+import GHC.TypeError(ErrorMessage(..), TypeError)
 import GHC.Num(Integer, fromInteger)
 import GHC.Show(Show(..))
 import GHC.Read(Read(..))
@@ -181,54 +181,6 @@ instance Read SomeChar where
 -- @since 4.10.0.0
 type family AppendSymbol (m ::Symbol) (n :: Symbol) :: Symbol
 
--- | A description of a custom type error.
-data {-kind-} ErrorMessage = Text Symbol
-                             -- ^ Show the text as is.
-
-                           | forall t. ShowType t
-                             -- ^ Pretty print the type.
-                             -- @ShowType :: k -> ErrorMessage@
-
-                           | ErrorMessage :<>: ErrorMessage
-                             -- ^ Put two pieces of error message next
-                             -- to each other.
-
-                           | ErrorMessage :$$: ErrorMessage
-                             -- ^ Stack two pieces of error message on top
-                             -- of each other.
-
-infixl 5 :$$:
-infixl 6 :<>:
-
--- | The type-level equivalent of 'Prelude.error'.
---
--- The polymorphic kind of this type allows it to be used in several settings.
--- For instance, it can be used as a constraint, e.g. to provide a better error
--- message for a non-existent instance,
---
--- @
--- -- in a context
--- instance TypeError (Text "Cannot 'Show' functions." :$$:
---                     Text "Perhaps there is a missing argument?")
---       => Show (a -> b) where
---     showsPrec = error "unreachable"
--- @
---
--- It can also be placed on the right-hand side of a type-level function
--- to provide an error for an invalid case,
---
--- @
--- type family ByteSize x where
---    ByteSize Word16   = 2
---    ByteSize Word8    = 1
---    ByteSize a        = TypeError (Text "The type " :<>: ShowType a :<>:
---                                   Text " is not exportable.")
--- @
---
--- @since 4.9.0.0
-type family TypeError (a :: ErrorMessage) :: b where
-
-
 -- Char-related type families
 
 -- | Extending a type-level symbol with a type-level character
diff --git a/libraries/base/base.cabal b/libraries/base/base.cabal
index 7e09412839..9b9d5ba2d2 100644
--- a/libraries/base/base.cabal
+++ b/libraries/base/base.cabal
@@ -275,6 +275,7 @@ Library
         GHC.Stats
         GHC.Storable
         GHC.TopHandler
+        GHC.TypeError
         GHC.TypeLits
         GHC.TypeLits.Internal
         GHC.TypeNats
diff --git a/libraries/base/changelog.md b/libraries/base/changelog.md
index 525cdbab72..a38c768f64 100644
--- a/libraries/base/changelog.md
+++ b/libraries/base/changelog.md
@@ -71,6 +71,13 @@
   * Functions in `Data.List` are specialized to list.
     `Data.OldList` and `GHC.List` modules are removed.
 
+  * Add `GHC.TypeError` module to contain functionality related to custom type
+    errors. `TypeError` is re-exported from `GHC.TypeLits` for backwards
+    compatibility.
+
+  * Comparison constraints in `Data.Type.Ord` (e.g. `<=`) now use the new
+    `GHC.TypeError.Assert` type family instead of type equality with `~`.
+
 ## 4.15.0.0 *TBA*
 
   * `openFile` now calls the `open` system call with an `interruptible` FFI
diff --git a/testsuite/tests/ghci/scripts/T9181.stdout b/testsuite/tests/ghci/scripts/T9181.stdout
index 89c18c2f6b..d6bfea3843 100644
--- a/testsuite/tests/ghci/scripts/T9181.stdout
+++ b/testsuite/tests/ghci/scripts/T9181.stdout
@@ -6,16 +6,6 @@ type family GHC.TypeLits.CharToNat a
 type GHC.TypeLits.ConsSymbol :: Char
                                 -> GHC.Types.Symbol -> GHC.Types.Symbol
 type family GHC.TypeLits.ConsSymbol a b
-type GHC.TypeLits.ErrorMessage :: *
-data GHC.TypeLits.ErrorMessage
-  = GHC.TypeLits.Text GHC.Types.Symbol
-  | forall t. GHC.TypeLits.ShowType t
-  | GHC.TypeLits.ErrorMessage
-    GHC.TypeLits.:<>:
-    GHC.TypeLits.ErrorMessage
-  | GHC.TypeLits.ErrorMessage
-    GHC.TypeLits.:$$:
-    GHC.TypeLits.ErrorMessage
 type GHC.TypeLits.KnownChar :: Char -> Constraint
 class GHC.TypeLits.KnownChar n where
   GHC.TypeLits.charSing :: GHC.TypeLits.SChar n
@@ -36,9 +26,6 @@ data GHC.TypeLits.SomeSymbol
   = forall (n :: GHC.Types.Symbol).
     GHC.TypeLits.KnownSymbol n =>
     GHC.TypeLits.SomeSymbol (Data.Proxy.Proxy n)
-type GHC.TypeLits.TypeError :: forall b.
-                               GHC.TypeLits.ErrorMessage -> b
-type family GHC.TypeLits.TypeError a where
 type GHC.TypeLits.UnconsSymbol :: GHC.Types.Symbol
                                   -> Maybe (Char, GHC.Types.Symbol)
 type family GHC.TypeLits.UnconsSymbol a
@@ -77,9 +64,11 @@ type family (GHC.TypeNats.+) a b
 type (GHC.TypeNats.-) :: GHC.Num.Natural.Natural
                          -> GHC.Num.Natural.Natural -> GHC.Num.Natural.Natural
 type family (GHC.TypeNats.-) a b
-type (Data.Type.Ord.<=) :: forall {k}. k -> k -> Constraint
+type (Data.Type.Ord.<=) :: forall {t}. t -> t -> Constraint
 type (Data.Type.Ord.<=) x y =
-  (x Data.Type.Ord.<=? y) ~ 'True :: Constraint
+  GHC.TypeError.Assert
+    (x Data.Type.Ord.<=? y) (Data.Type.Ord.LeErrMsg x y)
+  :: Constraint
 type (Data.Type.Ord.<=?) :: forall k. k -> k -> Bool
 type (Data.Type.Ord.<=?) m n =
   Data.Type.Ord.OrdCond
@@ -96,6 +85,16 @@ type family GHC.TypeLits.Internal.CmpSymbol a b
 type GHC.TypeNats.Div :: GHC.Num.Natural.Natural
                          -> GHC.Num.Natural.Natural -> GHC.Num.Natural.Natural
 type family GHC.TypeNats.Div a b
+type GHC.TypeError.ErrorMessage :: *
+data GHC.TypeError.ErrorMessage
+  = GHC.TypeError.Text GHC.Types.Symbol
+  | forall t. GHC.TypeError.ShowType t
+  | GHC.TypeError.ErrorMessage
+    GHC.TypeError.:<>:
+    GHC.TypeError.ErrorMessage
+  | GHC.TypeError.ErrorMessage
+    GHC.TypeError.:$$:
+    GHC.TypeError.ErrorMessage
 type GHC.TypeNats.KnownNat :: GHC.TypeNats.Nat -> Constraint
 class GHC.TypeNats.KnownNat n where
   GHC.TypeNats.natSing :: GHC.TypeNats.SNat n
@@ -131,6 +130,9 @@ data GHC.TypeNats.SomeNat
     GHC.TypeNats.SomeNat (Data.Proxy.Proxy n)
 type GHC.Types.Symbol :: *
 data GHC.Types.Symbol
+type GHC.TypeError.TypeError :: forall b.
+                                GHC.TypeError.ErrorMessage -> b
+type family GHC.TypeError.TypeError a where
 type (GHC.TypeNats.^) :: GHC.Num.Natural.Natural
                          -> GHC.Num.Natural.Natural -> GHC.Num.Natural.Natural
 type family (GHC.TypeNats.^) a b
diff --git a/testsuite/tests/typecheck/should_fail/OrdErr.hs b/testsuite/tests/typecheck/should_fail/OrdErr.hs
new file mode 100644
index 0000000000..8c10746f37
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/OrdErr.hs
@@ -0,0 +1,36 @@
+{-# LANGUAGE DataKinds, TypeFamilies #-}
+module OrdErr where
+
+import GHC.TypeNats
+import Data.Proxy
+
+proxyInEq :: (a <= b) => Proxy a -> Proxy b -> ()
+proxyInEq _ _ = ()
+
+-- Throws an error
+proxyInEq1 :: Proxy a -> Proxy (a+1) -> ()
+proxyInEq1 = proxyInEq
+
+-- Throws an error
+proxyInEq2 :: Proxy 5 -> Proxy 3 -> ()
+proxyInEq2 = proxyInEq
+
+-- No error
+proxyInEq3 :: Proxy 3 -> Proxy 4 -> ()
+proxyInEq3 = proxyInEq
+
+-- No error
+proxyInEq4 :: (a <=? (a + 1)) ~ True => Proxy a -> Proxy (a + 1) -> ()
+proxyInEq4 = proxyInEq
+
+-- No error
+proxyInEq5 :: (a <= (a + 1)) => Proxy a -> Proxy (a + 1) -> ()
+proxyInEq5 = proxyInEq
+
+-- No error
+proxyInEq6 :: (CmpNat a (a + 1) ~ EQ) => Proxy a -> Proxy (a + 1) -> ()
+proxyInEq6 = proxyInEq
+
+-- No error
+proxyInEq7 :: (CmpNat a (a + 1) ~ LT) => Proxy a -> Proxy (a + 1) -> ()
+proxyInEq7 = proxyInEq
diff --git a/testsuite/tests/typecheck/should_fail/OrdErr.stderr b/testsuite/tests/typecheck/should_fail/OrdErr.stderr
new file mode 100644
index 0000000000..01dba4924a
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/OrdErr.stderr
@@ -0,0 +1,9 @@
+OrdErr.hs:12:14: error:
+    • Cannot satisfy: a <= a + 1
+    • In the expression: proxyInEq
+      In an equation for ‘proxyInEq1’: proxyInEq1 = proxyInEq
+
+OrdErr.hs:16:14: error:
+    • Cannot satisfy: 5 <= 3
+    • In the expression: proxyInEq
+      In an equation for ‘proxyInEq2’: proxyInEq2 = proxyInEq
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 155500ab9f..1d308d7529 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -635,3 +635,4 @@ test('T17817_elab', normal, compile_fail, ['-fprint-typechecker-elaboration'])
 test('T19978', normal, compile_fail, [''])
 test('T20122', normal, compile_fail, [''])
 test('T20241b', normal, compile_fail, [''])
+test('OrdErr', normal, compile_fail, [''])