diff options
author | Christiaan Baaij <christiaan.baaij@gmail.com> | 2021-06-24 19:39:51 +0200 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2021-09-17 09:35:18 -0400 |
commit | 885f17c89919d21815365da71eb7f9c489e5bfa3 (patch) | |
tree | f58aa1111ef2d229b3568a0ef00db6ec24ce8574 | |
parent | 64923cf295ea914db458547432237a5ed1eff571 (diff) | |
download | haskell-885f17c89919d21815365da71eb7f9c489e5bfa3.tar.gz |
Improve error messages involving operators from Data.Type.Ord
Fixes #20009
-rw-r--r-- | compiler/GHC/Builtin/Names.hs | 13 | ||||
-rw-r--r-- | docs/users_guide/9.2.1-notes.rst | 4 | ||||
-rw-r--r-- | libraries/base/Data/Type/Ord.hs | 17 | ||||
-rw-r--r-- | libraries/base/GHC/TypeError.hs | 141 | ||||
-rw-r--r-- | libraries/base/GHC/TypeLits.hs | 50 | ||||
-rw-r--r-- | libraries/base/base.cabal | 1 | ||||
-rw-r--r-- | libraries/base/changelog.md | 7 | ||||
-rw-r--r-- | testsuite/tests/ghci/scripts/T9181.stdout | 32 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/OrdErr.hs | 36 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/OrdErr.stderr | 9 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/all.T | 1 |
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, ['']) |