-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Runtime type assertions for testing
--   
--   This package provides a way to make runtime assertions about types
--   that cooperate with the typechecker, intended for use in testing. For
--   more information, see the module documentation for
--   <a>Test.TypeAssertions</a>.
@package type-assertions
@version 0.1.0.0


-- | This module provides a set of runtime assertions about types that
--   propogates information back to the type system, using <a>Typeable</a>
--   and <a>:~:</a>. These are intended to be used in a test suite (and
--   exclusively in a test suite) to create monomorphic implementations of
--   polymorphic functions. Specifically, this is intended to be used with
--   a package like <a>test-fixture</a> to stub out polymorphic typeclass
--   methods with monomorphic implementations.
--   
--   For example, consider the following typeclass:
--   
--   <pre>
--   class Monad m =&gt; MonadDB m where
--     get :: DBRecord r =&gt; Id r -&gt; m [r]
--     ...
--   </pre>
--   
--   The <tt>get</tt> method might be used in another function to retrieve
--   a record of a specific type, such as a <tt>User</tt>. In a test, it
--   might be useful to stub out the <tt>get</tt> method to provide a
--   well-known user:
--   
--   <pre>
--   let fixture = def { _get = \_ -&gt; User { ... } }
--   </pre>
--   
--   However, this will not typecheck, since the type of record should be
--   chosen by the <i>caller</i> of <tt>get</tt>. We might know that the
--   type is guaranteed to be <tt>User</tt> in this particular case, but
--   GHC cannot prove that, and it will reject attempts to write a stubbed
--   implementation.
--   
--   To work around this issue, we can effectively defer the type error to
--   runtime by using the functions in this module. For example, we can use
--   <a>withAssertEqT</a> to assert that the types are the same:
--   
--   <pre>
--   {-# LANGUAGE ScopedTypeVariables, TypeApplications #-}
--   
--   let fixture = def { _get = \(_ :: Id r) -&gt;
--         withAssertEqT @r @User $
--           User { ... } }
--   </pre>
--   
--   This will properly convince GHC that the <tt>User</tt> value will only
--   be returned when the argument is actually an <tt>Id User</tt>. If it
--   isn’t, <a>withAssertEqT</a> will throw.
module Test.TypeAssertions

-- | Asserts that a value has a particular type, and raises an exception if
--   it does not.
--   
--   <pre>
--   &gt;&gt;&gt; assertHasT @Bool True
--   Refl
--   
--   &gt;&gt;&gt; assertHasT @Bool "hello"
--   *** Exception: expected value of type ‘Bool’, but got ‘"hello"’, which is of type ‘[Char]’
--   </pre>
assertHasT :: forall b a. (HasCallStack, Show a, Typeable a, Typeable b) => a -> (a :~: b)

-- | Like <a>assertHasT</a>, but instead of returning a witness upon
--   success, <a>withAssertHasT</a> returns its second argument. The second
--   argument can be an expression that typechecks under the assumption
--   that <tt>a ~ b</tt>.
--   
--   <pre>
--   foo :: (Show a, Typeable a) =&gt; a -&gt; a
--   foo x = withAssertHasT @String x $ map toUpper x
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; foo "hello"
--   "HELLO"
--   
--   &gt;&gt;&gt; foo True
--   *** Exception: expected value of type ‘[Char]’, but got ‘True’, which is of type ‘Bool’
--   CallStack (from HasCallStack):
--     withAssertHasT, called at &lt;interactive&gt;:17:13 in interactive:Ghci1
--   </pre>
withAssertHasT :: forall b a c. (HasCallStack, Show a, Typeable a, Typeable b) => a -> ((a ~ b) => c) -> c

-- | Like <a>assertHasT</a>, but asserts that two types are the same
--   instead of asserting that a value has a type. Generally, prefer
--   <a>assertHasT</a> when possible, since it will produce better error
--   messages, but <a>assertEqT</a> can be necessary when the type does not
--   have a runtime representation (such as if it is phantom).
--   
--   <pre>
--   &gt;&gt;&gt; assertEqT @Bool @Bool
--   Refl
--   
--   &gt;&gt;&gt; assertEqT @Bool @Int
--   *** Exception: expected type ‘Int’, but got type ‘Bool’
--   </pre>
assertEqT :: forall a b. (HasCallStack, Typeable a, Typeable b) => (a :~: b)

-- | Like <a>assertEqT</a> but with the type propogation behavior of
--   <a>withAssertHasT</a>. Generally, prefer <a>withAssertHasT</a> when
--   possible, since it will produce better error messages, but
--   <a>withAssertEqT</a> can be necessary when the type does not have a
--   runtime representation (such as if it is phantom).
--   
--   <pre>
--   foo :: forall a proxy. (Show a, Typeable a) =&gt; proxy a -&gt; a
--   foo _ = withAssertEqT @Bool @a True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; foo (Proxy @Bool)
--   True
--   
--   &gt;&gt;&gt; foo (Proxy @Int)
--   *** Exception: expected type ‘Int’, but got type ‘Bool’
--   </pre>
withAssertEqT :: forall a b c. (HasCallStack, Typeable a, Typeable b) => ((a ~ b) => c) -> c

-- | Propositional equality. If <tt>a :~: b</tt> is inhabited by some
--   terminating value, then the type <tt>a</tt> is the same as the type
--   <tt>b</tt>. To use this equality in practice, pattern-match on the
--   <tt>a :~: b</tt> to get out the <tt>Refl</tt> constructor; in the body
--   of the pattern-match, the compiler knows that <tt>a ~ b</tt>.
data (:~:) k (a :: k) (b :: k) :: forall k. k -> k -> *
[Refl] :: (:~:) k a a