-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Tools for writing better type errors
--
-- Please see the README on GitHub at
-- https://github.com/isovector/type-errors#readme
@package type-errors
@version 0.1.0.0
module Type.Errors
-- | A description of a custom type error.
data ErrorMessage
-- | Show the text as is.
[Text] :: () => Symbol -> ErrorMessage
-- | Pretty print the type. ShowType :: k -> ErrorMessage
[ShowType] :: forall t. () => t -> ErrorMessage
-- | Put two pieces of error message next to each other.
[:<>:] :: () => ErrorMessage -> ErrorMessage -> ErrorMessage
-- | Stack two pieces of error message on top of each other.
[:$$:] :: () => ErrorMessage -> ErrorMessage -> ErrorMessage
infixl 6 :<>:
infixl 5 :$$:
-- | Pretty print a list.
--
--
-- >>> :show_error PrettyPrintList '[Bool]
-- ...
-- ... 'Bool'
-- ...
--
--
--
-- >>> :show_error PrettyPrintList '[1, 2]
-- ...
-- ... '1', and '2'
-- ...
--
--
--
-- >>> :show_error PrettyPrintList '["hello", "world", "cool"]
-- ...
-- ... "hello", "world", and "cool"
-- ...
--
type family PrettyPrintList (vs :: [k]) :: ErrorMessage
-- | Like ShowType, but quotes the type if necessary.
--
--
-- >>> :show_error ShowTypeQuoted Int
-- ...
-- ... 'Int'
-- ...
--
--
--
-- >>> :show_error ShowTypeQuoted "symbols aren't quoted"
-- ...
-- ... "symbols aren't quoted"
-- ...
--
type family ShowTypeQuoted (t :: k) :: ErrorMessage
-- | The type-level equivalent of 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.")
--
type family TypeError (a :: ErrorMessage) :: b
-- | Error messages produced via TypeError are often too
-- strict, and will be emitted sooner than you'd like. The solution
-- is to use DelayError, which will switch the error messages to
-- being consumed lazily.
--
--
-- >>> :{
-- foo :: TypeError ('Text "Too eager; prevents compilation") => ()
-- foo = ()
-- :}
-- ...
-- ... Too eager; prevents compilation
-- ...
--
--
--
-- >>> :{
-- foo :: DelayError ('Text "Lazy; emitted on use") => ()
-- foo = ()
-- :}
--
--
--
-- >>> foo
-- ...
-- ... Lazy; emitted on use
-- ...
--
type DelayError err = Eval (DelayErrorFcf err)
-- | Like DelayError, but implemented as a first-class family.
-- DelayErrorFcf is useful when used as the last argument to
-- IfStuck and UnlessStuck.
data DelayErrorFcf :: ErrorMessage -> Exp k
-- | A helper definition that doesn't emit a type error. This is
-- occassionally useful to leave as the residual constraint in
-- IfStuck when you only want to observe if an expression
-- isn't stuck.
type NoError = (() :: Constraint)
-- | Like NoError, but implemented as a first-class family.
-- NoErrorFcf is useful when used as the last argument to
-- IfStuck and UnlessStuck.
type NoErrorFcf = Pure NoError
-- | IfStuck expr b c leaves b in the residual
-- constraints whenever expr is stuck, otherwise it
-- Evaluates c.
--
-- Often you want to leave a DelayError in b in order to
-- report an error when expr is stuck.
--
-- The c parameter is a first-class family, which allows you to
-- perform arbitrarily-complicated type-level computations whenever
-- expr isn't stuck. For example, you might want to produce a
-- typeclass Constraint here. Alternatively, you can nest calls to
-- IfStuck in order to do subsequent processing.
--
-- This is a generalization of kcsongor's Break machinery
-- described in detecting the undetectable.
type family IfStuck (expr :: k) (b :: k1) (c :: Exp k1) :: k1
-- | Like IfStuck, but specialized to the case when you don't want
-- to do anything if expr isn't stuck.
--
--
-- >>> :{
-- observe_no_rep
-- :: WhenStuck
-- (Rep t)
-- (DelayError ('Text "No Rep instance for " ':<>: ShowTypeQuoted t))
-- => t
-- -> ()
-- observe_no_rep _ = ()
-- :}
--
--
--
-- >>> observe_no_rep HasNoRep
-- ...
-- ... No Rep instance for 'HasNoRep'
-- ...
--
--
--
-- >>> observe_no_rep True
-- ()
--
type WhenStuck expr b = IfStuck expr b NoErrorFcf
-- | Like IfStuck, but leaves no residual constraint when
-- expr is stuck. This can be used to ensure an expression
-- isn't stuck before analyzing it further.
--
-- See the example under UnlessPhantomFcf for an example of this
-- use-case.
type UnlessStuck expr c = IfStuck expr NoError c
-- | A meta-variable for marking which argument should be a phantom when
-- working with UnlessPhantom and UnlessPhantomFcf.
--
-- PHANTOM is polykinded and can be used in several settings.
--
-- See UnlessPhantom for examples.
type PHANTOM = VAR
-- | UnlessPhantom expr err determines if the type
-- described by expr is phantom in the variables marked via
-- PHANTOM. If it's not, it produces the error message
-- err.
--
-- For example, consider the definition:
--
--
-- >>> :{
-- data Qux a b = Qux b
-- :}
--
--
-- which is phantom in a:
--
--
-- >>> :eval_error UnlessPhantom (Qux PHANTOM Int) ('Text "Ok")
-- ()
--
--
-- but not in b:
--
--
-- >>> :eval_error UnlessPhantom (Qux Int PHANTOM) ('Text "Bad!")
-- ...
-- ... Bad!
-- ...
--
--
-- Unfortunately there is no known way to emit an error message if the
-- variable is a phantom.
type UnlessPhantom exp err = Eval (UnlessPhantomFcf exp err)
-- | Like UnlessPhantom, but implemented as a first-class family. As
-- such, this allows UnlessPhantomFcf to be chained after
-- IfStuck to only be run if an expression isn't stuck.
--
-- This can be used to avoid emitting false error messages when a type
-- variable isn't phantom, just ambiguous.
--
--
-- >>> :{
-- observe_phantom
-- :: UnlessStuck
-- f
-- (UnlessPhantomFcf
-- (f PHANTOM)
-- ('Text "It's not phantom!"))
-- => f p
-- -> ()
-- observe_phantom _ = ()
-- :}
--
--
--
-- >>> observe_phantom Proxy
-- ()
--
--
--
-- >>> observe_phantom (Just 5)
-- ...
-- ... It's not phantom!
-- ...
--
--
-- In the next example, we leave observe_phantom unsaturated,
-- and therefore f isn't yet known. Without guarding the
-- UnlessPhantomFcf behind UnlessStuck, this would
-- incorrectly produce the message "It's not phantom!"
--
--
-- >>> observe_phantom
-- ...
-- ... No instance for (Show ...
-- ...
--
data UnlessPhantomFcf :: k -> ErrorMessage -> Exp Constraint
-- | Subst expr a b substitutes all instances of a
-- for b in expr.
--
--
-- >>> :kind! Subst (Either Int Int) Int Bool
-- ...
-- = Either Bool Bool
--
--
--
-- >>> :kind! Subst (Either Int Bool) Int [Char]
-- ...
-- = Either [Char] Bool
--
--
--
-- >>> :kind! Subst (Either Int Bool) Either (->)
-- ...
-- = Int -> Bool
--
type family Subst (e :: k1) (var :: k2) (sub :: k2) :: k1
-- | VAR is a meta-varaible which marks a substitution in
-- SubstVar. The result of SubstVar expr val is
-- expr[val/VAR].
--
-- VAR is polykinded and can be used in several settings.
--
-- See SubstVar for examples.
type VAR = SubMe Var
-- | Like Subst, but uses the explicit meta-variable VAR to
-- mark substitution points.
--
--
-- >>> :kind! SubstVar (Either VAR Bool) [Char]
-- ...
-- = Either [Char] Bool
--
--
--
-- >>> :kind! SubstVar (VAR Int Bool :: Type) (->)
-- ...
-- = Int -> Bool
--
type family SubstVar (e :: k1) (r :: k2) :: k1
-- | Kind of type-level expressions indexed by their result type.
type Exp a = a -> Type
-- | Expression evaluator.
type family Eval (e :: Exp a) :: a
data Pure (b :: a) (c :: a) :: forall a. () => a -> a -> Type