-- 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
--   <a>https://github.com/isovector/type-errors#readme</a>
@package type-errors
@version 0.2.0.2


-- | This module provides useful tools for writing better type-errors. For
--   a quickstart guide to the underlying <a>TypeError</a> machinery, check
--   out Dmitrii Kovanikov's excellent blog post <a>A story told by Type
--   Errors</a>.
module Type.Errors

-- | A description of a custom type error.
data () => ErrorMessage

-- | Show the text as is.
Text :: Symbol -> ErrorMessage

-- | Pretty print the type. <tt>ShowType :: k -&gt; ErrorMessage</tt>
ShowType :: 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.
--   
--   <pre>
--   &gt;&gt;&gt; :show_error PrettyPrintList '[Bool]
--   ...
--   ... 'Bool'
--   ...
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :show_error PrettyPrintList '[1, 2]
--   ...
--   ... '1', and '2'
--   ...
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :show_error PrettyPrintList '["hello", "world", "cool"]
--   ...
--   ... "hello", "world", and "cool"
--   ...
--   </pre>
type family PrettyPrintList (vs :: [k]) :: ErrorMessage

-- | Like <a>ShowType</a>, but quotes the type if necessary.
--   
--   <pre>
--   &gt;&gt;&gt; :show_error ShowTypeQuoted Int
--   ...
--   ... 'Int'
--   ...
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :show_error ShowTypeQuoted "symbols aren't quoted"
--   ...
--   ... "symbols aren't quoted"
--   ...
--   </pre>
type family ShowTypeQuoted (t :: k) :: ErrorMessage

-- | The type-level equivalent of <a>error</a>.
--   
--   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,
--   
--   <pre>
--   -- in a context
--   instance TypeError (Text "Cannot <tt>Show</tt> functions." :$$:
--                       Text "Perhaps there is a missing argument?")
--         =&gt; Show (a -&gt; b) where
--       showsPrec = error "unreachable"
--   </pre>
--   
--   It can also be placed on the right-hand side of a type-level function
--   to provide an error for an invalid case,
--   
--   <pre>
--   type family ByteSize x where
--      ByteSize Word16   = 2
--      ByteSize Word8    = 1
--      ByteSize a        = TypeError (Text "The type " :&lt;&gt;: ShowType a :&lt;&gt;:
--                                     Text " is not exportable.")
--   </pre>
type family TypeError (a :: ErrorMessage) :: b

-- | Error messages produced via <a>TypeError</a> are often <i>too
--   strict</i>, and will be emitted sooner than you'd like. The solution
--   is to use <a>DelayError</a>, which will switch the error messages to
--   being consumed lazily.
--   
--   <pre>
--   &gt;&gt;&gt; :{
--   foo :: TypeError ('Text "Too eager; prevents compilation") =&gt; ()
--   foo = ()
--   :}
--   ...
--   ... Too eager; prevents compilation
--   ...
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :{
--   foo :: DelayError ('Text "Lazy; emitted on use") =&gt; ()
--   foo = ()
--   :}
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; foo
--   ...
--   ... Lazy; emitted on use
--   ...
--   </pre>
type DelayError err = Eval (DelayErrorFcf err)

-- | Like <a>DelayError</a>, but implemented as a first-class family.
--   <a>DelayErrorFcf</a> is useful when used as the last argument to
--   <a>IfStuck</a> and <a>UnlessStuck</a>.
data DelayErrorFcf :: ErrorMessage -> Exp k

-- | A helper definition that <i>doesn't</i> emit a type error. This is
--   occassionally useful to leave as the residual constraint in
--   <a>IfStuck</a> when you only want to observe if an expression
--   <i>isn't</i> stuck.
type NoError = (() :: Constraint)

-- | Like <a>NoError</a>, but implemented as a first-class family.
--   <a>NoErrorFcf</a> is useful when used as the last argument to
--   <a>IfStuck</a> and <a>UnlessStuck</a>.
type NoErrorFcf = Pure NoError

-- | <tt><a>IfStuck</a> expr b c</tt> leaves <tt>b</tt> in the residual
--   constraints whenever <tt>expr</tt> is stuck, otherwise it
--   <a>Eval</a>uates <tt>c</tt>.
--   
--   Often you want to leave a <a>DelayError</a> in <tt>b</tt> in order to
--   report an error when <tt>expr</tt> is stuck.
--   
--   The <tt>c</tt> parameter is a first-class family, which allows you to
--   perform arbitrarily-complicated type-level computations whenever
--   <tt>expr</tt> isn't stuck. For example, you might want to produce a
--   typeclass <a>Constraint</a> here. Alternatively, you can nest calls to
--   <a>IfStuck</a> in order to do subsequent processing.
--   
--   This is a generalization of <a>kcsongor</a>'s <tt>Break</tt> machinery
--   described in <a>detecting the undetectable</a>.
type family IfStuck (expr :: k) (b :: k1) (c :: Exp k1) :: k1

-- | Like <a>IfStuck</a>, but specialized to the case when you don't want
--   to do anything if <tt>expr</tt> isn't stuck.
--   
--   <pre>
--   &gt;&gt;&gt; :{
--   observe_no_rep
--       :: WhenStuck
--            (Rep t)
--            (DelayError ('Text "No Rep instance for " ':&lt;&gt;: ShowTypeQuoted t))
--       =&gt; t
--       -&gt; ()
--   observe_no_rep _ = ()
--   :}
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; observe_no_rep HasNoRep
--   ...
--   ... No Rep instance for 'HasNoRep'
--   ...
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; observe_no_rep True
--   ()
--   </pre>
type WhenStuck expr b = IfStuck expr b NoErrorFcf

-- | Like <a>IfStuck</a>, but leaves no residual constraint when
--   <tt>expr</tt> is stuck. This can be used to ensure an expression
--   <i>isn't</i> stuck before analyzing it further.
--   
--   See the example under <a>UnlessPhantom</a> 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 <a>UnlessPhantom</a> asks you to mark
--   phantom variables via <a>PHANTOM</a>.
--   
--   Unfortunately, this substitution cannot reliably be performed via type
--   families, since it will too often get stuck. Instead we provide
--   <a>te</a>, which is capable of reasoning about types symbolically.
--   
--   Any type which comes with the warning <i>"This type family is always
--   stuck."</i> <b>must</b> be used in the context of <a>te</a> and the
--   magic <tt>[t|</tt> quasiquoter. To illustrate, the following is stuck:
--   
--   <pre>
--   &gt;&gt;&gt; :{
--   foo :: SubstVar VAR Bool
--   foo = True
--   :}
--   ...
--   ... Couldn't match expected type ...SubstVar VAR Bool...
--   ... with actual type ...Bool...
--   ...
--   </pre>
--   
--   But running it via <a>te</a> makes everything work:
--   
--   <pre>
--   &gt;&gt;&gt; :{
--   foo :: $(te[t| SubstVar VAR Bool |])
--   foo = True
--   :}
--   </pre>
--   
--   If you don't want to think about when to use <a>te</a>, it's a no-op
--   when used with everyday types:
--   
--   <pre>
--   &gt;&gt;&gt; :{
--   bar :: $(te[t| Bool |])
--   bar = True
--   :}
--   </pre>
te :: Q Type -> Q Type

-- | <b>This type family is always stuck. It must be used in the context of
--   <a>te</a>.</b>
--   
--   A meta-variable for marking which argument should be a phantom when
--   working with <a>UnlessPhantom</a>.
--   
--   <a>PHANTOM</a> is polykinded and can be used in several settings.
--   
--   See <a>UnlessPhantom</a> for examples.
type family PHANTOM :: k

-- | <b>This type family is always stuck. It must be used in the context of
--   <a>te</a>.</b>
--   
--   <tt><a>UnlessPhantom</a> expr err</tt> determines if the type
--   described by <tt>expr</tt> is phantom in the variables marked via
--   <a>PHANTOM</a>. If it's not, it produces the error message
--   <tt>err</tt>.
--   
--   For example, consider the definition:
--   
--   <pre>
--   &gt;&gt;&gt; :{
--   data Qux a b = Qux b
--   :}
--   </pre>
--   
--   which is phantom in <tt>a</tt>:
--   
--   <pre>
--   &gt;&gt;&gt; :eval_error $(te[t| UnlessPhantom (Qux PHANTOM Int) ('Text "Ok") |])
--   ()
--   </pre>
--   
--   but not in <tt>b</tt>:
--   
--   <pre>
--   &gt;&gt;&gt; :eval_error $(te[t| UnlessPhantom (Qux Int PHANTOM) ('Text "Bad!") |])
--   ...
--   ... Bad!
--   ...
--   </pre>
--   
--   Unfortunately there is no known way to emit an error message if the
--   variable <i>is</i> a phantom.
--   
--   Often you'll want to guard <a>UnlessPhantom</a> against
--   <a>IfStuck</a>, to ensure you don't get errors when things are merely
--   ambiguous. You can do this by writing your own fcf whose
--   implementation is <a>UnlessPhantom</a>:
--   
--   <pre>
--   &gt;&gt;&gt; :{
--   data NotPhantomErrorFcf :: k -&gt; Exp Constraint
--   type instance Eval (NotPhantomErrorFcf f) =
--     $(te[t| UnlessPhantom (f PHANTOM)
--                           ( ShowTypeQuoted f
--                      ':&lt;&gt;: 'Text " is not phantom in its argument!")
--           |])
--   :}
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :{
--   observe_phantom
--       :: UnlessStuck
--            f
--            (NotPhantomErrorFcf f)
--       =&gt; f p
--       -&gt; ()
--   observe_phantom _ = ()
--   :}
--   </pre>
--   
--   We then notice that using <tt>observe_phantom</tt> against
--   <a>Proxy</a> doesn't produce any errors, but against <a>Maybe</a>
--   does:
--   
--   <pre>
--   &gt;&gt;&gt; observe_phantom Proxy
--   ()
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; observe_phantom (Just 5)
--   ...
--   ... 'Maybe' is not phantom in its argument!
--   ...
--   </pre>
--   
--   Finally, we leave <tt>observe_phantom</tt> unsaturated, and therefore
--   <tt>f</tt> isn't yet known. Without guarding the <a>UnlessPhantom</a>
--   behind <a>UnlessStuck</a>, this would incorrectly produce the message
--   "<tt>f</tt> is not phantom in its argument!"
--   
--   <pre>
--   &gt;&gt;&gt; observe_phantom
--   ...
--   </pre>
type family UnlessPhantom :: k -> ErrorMessage -> Constraint

-- | <b>This type family is always stuck. It must be used in the context of
--   <a>te</a>.</b>
--   
--   <tt><a>Subst</a> expr a b</tt> substitutes all instances of <tt>a</tt>
--   for <tt>b</tt> in <tt>expr</tt>.
--   
--   <pre>
--   &gt;&gt;&gt; :kind! $(te[t| Subst (Either Int Int) Int Bool |])
--   ...
--   = Either Bool Bool
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! $(te[t| Subst (Either Int Bool) Int [Char] |])
--   ...
--   = Either [Char] Bool
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! $(te[t| Subst (Either Int Bool) Either (,) |])
--   ...
--   = (Int, Bool)
--   </pre>
type family Subst :: k1 -> k1 -> k2 -> k2

-- | <b>This type family is always stuck. It must be used in the context of
--   <a>te</a>.</b>
--   
--   <a>VAR</a> is a meta-varaible which marks a substitution in
--   <a>SubstVar</a>. The result of <tt><a>SubstVar</a> expr val</tt> is
--   <tt>expr[val/<a>VAR</a>]</tt>.
--   
--   <a>VAR</a> is polykinded and can be used in several settings.
--   
--   See <a>SubstVar</a> for examples.
type family VAR :: k

-- | <b>This type family is always stuck. It must be used in the context of
--   <a>te</a>.</b>
--   
--   Like <a>Subst</a>, but uses the explicit meta-variable <a>VAR</a> to
--   mark substitution points.
--   
--   <pre>
--   &gt;&gt;&gt; :kind! $(te[t| SubstVar (Either VAR VAR) Bool |])
--   ...
--   = Either Bool Bool
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! $(te[t| SubstVar (Either VAR Bool) [Char] |])
--   ...
--   = Either [Char] Bool
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! $(te[t| SubstVar (VAR Int Bool) (,) |])
--   ...
--   = (Int, Bool)
--   </pre>
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)
