-- 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.2.0.0
-- | This module provides useful tools for writing better type-errors. For
-- a quickstart guide to the underlying TypeError machinery, check
-- out Dmitrii Kovanikov's excellent blog post A story told by Type
-- Errors.
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 UnlessPhantom for an example of this
-- use-case.
type UnlessStuck expr c = IfStuck expr NoError c
-- | This library provides tools for performing lexical substitutions over
-- types. For example, the function UnlessPhantom asks you to mark
-- phantom variables via PHANTOM.
--
-- Unfortunately, this substitution cannot reliably be performed via type
-- families, since it will too often get stuck. Instead we provide
-- te, which is capable of reasoning about types symbolically.
--
-- Any type which comes with the warning "This type family is always
-- stuck." must be used in the context of te and the
-- magic [t| quasiquoter. To illustrate, the following is stuck:
--
--
-- >>> :{
-- foo :: SubstVar VAR Bool
-- foo = True
-- :}
-- ...
-- ... Couldn't match expected type ...SubstVar VAR Bool...
-- ... with actual type ...Bool...
-- ...
--
--
-- But running it via te makes everything work:
--
--
-- >>> :{
-- foo :: $(te[t| SubstVar VAR Bool |])
-- foo = True
-- :}
--
--
-- If you don't want to think about when to use te, it's a no-op
-- when used with everyday types:
--
--
-- >>> :{
-- bar :: $(te[t| Bool |])
-- bar = True
-- :}
--
te :: Q Type -> Q Type
-- | This type family is always stuck. It must be used in the context of
-- te.
--
-- A meta-variable for marking which argument should be a phantom when
-- working with UnlessPhantom.
--
-- PHANTOM is polykinded and can be used in several settings.
--
-- See UnlessPhantom for examples.
type family PHANTOM :: k
-- | This type family is always stuck. It must be used in the context of
-- te.
--
-- 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 $(te[t| UnlessPhantom (Qux PHANTOM Int) ('Text "Ok") |])
-- ()
--
--
-- but not in b:
--
--
-- >>> :eval_error $(te[t| UnlessPhantom (Qux Int PHANTOM) ('Text "Bad!") |])
-- ...
-- ... Bad!
-- ...
--
--
-- Unfortunately there is no known way to emit an error message if the
-- variable is a phantom.
--
-- Often you'll want to guard UnlessPhantom against
-- IfStuck, to ensure you don't get errors when things are merely
-- ambiguous. You can do this by writing your own fcf whose
-- implementation is UnlessPhantom:
--
--
-- >>> :{
-- data NotPhantomErrorFcf :: k -> Exp Constraint
-- type instance Eval (NotPhantomErrorFcf f) =
-- $(te[t| UnlessPhantom (f PHANTOM)
-- ( ShowTypeQuoted f
-- ':<>: 'Text " is not phantom in its argument!")
-- |])
-- :}
--
--
--
-- >>> :{
-- observe_phantom
-- :: UnlessStuck
-- f
-- (NotPhantomErrorFcf f)
-- => f p
-- -> ()
-- observe_phantom _ = ()
-- :}
--
--
-- We then notice that using observe_phantom against
-- Proxy doesn't produce any errors, but against Maybe
-- does:
--
--
-- >>> observe_phantom Proxy
-- ()
--
--
--
-- >>> observe_phantom (Just 5)
-- ...
-- ... 'Maybe' is not phantom in its argument!
-- ...
--
--
-- Finally, we leave observe_phantom unsaturated, and therefore
-- f isn't yet known. Without guarding the UnlessPhantom
-- behind UnlessStuck, this would incorrectly produce the message
-- "f is not phantom in its argument!"
--
--
-- >>> observe_phantom
-- ...
-- ... No instance for (Show (f0 p0 -> ()))
-- ...
--
type family UnlessPhantom :: k -> ErrorMessage -> Constraint
-- | This type family is always stuck. It must be used in the context of
-- te.
--
-- Subst expr a b substitutes all instances of a
-- for b in expr.
--
--
-- >>> :kind! $(te[t| Subst (Either Int Int) Int Bool |])
-- ...
-- = Either Bool Bool
--
--
--
-- >>> :kind! $(te[t| Subst (Either Int Bool) Int [Char] |])
-- ...
-- = Either [Char] Bool
--
--
--
-- >>> :kind! $(te[t| Subst (Either Int Bool) Either (,) |])
-- ...
-- = (Int, Bool)
--
type family Subst :: k1 -> k1 -> k2 -> k2
-- | This type family is always stuck. It must be used in the context of
-- te.
--
-- 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 family VAR :: k
-- | This type family is always stuck. It must be used in the context of
-- te.
--
-- Like Subst, but uses the explicit meta-variable VAR to
-- mark substitution points.
--
--
-- >>> :kind! $(te[t| SubstVar (Either VAR VAR) Bool |])
-- ...
-- = Either Bool Bool
--
--
--
-- >>> :kind! $(te[t| SubstVar (Either VAR Bool) [Char] |])
-- ...
-- = Either [Char] Bool
--
--
--
-- >>> :kind! $(te[t| SubstVar (VAR Int Bool) (,) |])
-- ...
-- = (Int, Bool)
--
type family SubstVar :: k1 -> k2 -> k2
-- | 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