diff options
Diffstat (limited to 'libraries')
| -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 |
5 files changed, 160 insertions, 56 deletions
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 |