    -- |
    -- Description : Inspection Testing for Haskell
    -- Copyright   : (c) Joachim Breitner, 2017
    -- License     : MIT
    -- Maintainer  : mail@joachim-breitner.de
    -- Portability : GHC specifc
    --
    -- This module supports the accompanying GHC plugin "Test.Inspection.Plugin" and adds
    -- to GHC the ability to do inspection testing.

    {-# LANGUAGE TemplateHaskell #-}
    {-# LANGUAGE DeriveDataTypeable #-}
    {-# LANGUAGE StandaloneDeriving #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE CPP #-}
    module Test.Inspection (
        -- * Synopsis
        -- $synopsis

        -- * Registering obligations
        inspect,
        inspectTest,
        Result(..),
        -- * Defining obligations
        Obligation(..), mkObligation, Equivalence (..), Property(..),
        -- * Convenience functions
        -- $convenience
        (===), (==-), (=/=), (=/-), (==~), (=/~),
        hasNoType, hasNoGenerics,
        hasNoTypeClasses, hasNoTypeClassesExcept,
        doesNotUse, coreOf,
    ) where

    import Language.Haskell.TH
    import Language.Haskell.TH.Syntax (Quasi(qNewName), liftData, addTopDecls)
    #if MIN_VERSION_GLASGOW_HASKELL(8,4,0,0)
    import Language.Haskell.TH.Syntax (addCorePlugin)
    #endif
    import Data.Data
    import Data.Maybe
    import GHC.Exts (lazy)
    import GHC.Generics (V1(), U1(), M1(), K1(), (:+:), (:*:), (:.:), Rec1, Par1)

    {- $synopsis

    To use inspection testing, you need to

     1. enable the @TemplateHaskell@ language extension
     2. declare your proof obligations using 'inspect' or 'inspectTest'

    An example module is

    @
    {&#45;\# LANGUAGE TemplateHaskell \#&#45;}
    module Simple where

    import Test.Inspection
    import Data.Maybe

    lhs, rhs :: (a -> b) -> Maybe a -> Bool
    lhs f x = isNothing (fmap f x)
    rhs f Nothing = True
    rhs f (Just _) = False

    inspect $ 'lhs === 'rhs
    @

    On GHC < 8.4, you have to explicitly load the plugin:
    @
    {&#45;\# OPTIONS_GHC -fplugin=Test.Inspection.Plugin \#&#45;}
    @
    -}

    -- Description of test obligations

    -- | This data type describes an inspection testing obligation.
    --
    -- It is recommended to build it using 'mkObligation', for backwards
    -- compatibility when new fields are added. You can also use the more
    -- mnemonic convenience functions like '(===)' or 'hasNoType'.
    --
    -- The obligation needs to be passed to 'inspect' or 'inspectTest'.
    --
    -- @since 0.1
    data Obligation = Obligation
        { Obligation -> Name
    target      :: Name
            -- ^ The target of a test obligation; invariably the name of a local
            -- definition. To get the name of a function @foo@, write @'foo@. This requires
            -- @{&#45;\# LANGUAGE TemplateHaskell \#&#45;}@.
        , Obligation -> Property
    property    :: Property
            -- ^ The property of the target to be checked.
        , Obligation -> Maybe String
    testName :: Maybe String
            -- ^ An optional name for the test
        , Obligation -> Bool
    expectFail  :: Bool
            -- ^ Do we expect this property to fail?
            -- (Only used by 'inspect', not by 'inspectTest')
        , Obligation -> Maybe Loc
    srcLoc :: Maybe Loc
            -- ^ The source location where this obligation is defined.
            -- This is filled in by 'inspect'.
        , Obligation -> Maybe String
    storeResult :: Maybe String
            -- ^ If this is 'Nothing', then report errors during compilation.
            -- Otherwise, update the top-level definition with this name.
            --
            -- @since 0.2
        }
        deriving Typeable Obligation
    Typeable Obligation =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> Obligation -> c Obligation)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c Obligation)
    -> (Obligation -> Constr)
    -> (Obligation -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c Obligation))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e))
        -> Maybe (c Obligation))
    -> ((forall b. Data b => b -> b) -> Obligation -> Obligation)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> Obligation -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> Obligation -> r)
    -> (forall u. (forall d. Data d => d -> u) -> Obligation -> [u])
    -> (forall u.
        Int -> (forall d. Data d => d -> u) -> Obligation -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> Obligation -> m Obligation)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Obligation -> m Obligation)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Obligation -> m Obligation)
    -> Data Obligation
    Obligation -> Constr
    Obligation -> DataType
    (forall b. Data b => b -> b) -> Obligation -> Obligation
    forall a.
    Typeable a =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> Obligation -> u
    forall u. (forall d. Data d => d -> u) -> Obligation -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Obligation -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Obligation -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Obligation -> m Obligation
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Obligation -> m Obligation
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Obligation
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Obligation -> c Obligation
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Obligation)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Obligation)
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Obligation -> c Obligation
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Obligation -> c Obligation
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Obligation
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Obligation
    $ctoConstr :: Obligation -> Constr
    toConstr :: Obligation -> Constr
    $cdataTypeOf :: Obligation -> DataType
    dataTypeOf :: Obligation -> DataType
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Obligation)
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Obligation)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Obligation)
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Obligation)
    $cgmapT :: (forall b. Data b => b -> b) -> Obligation -> Obligation
    gmapT :: (forall b. Data b => b -> b) -> Obligation -> Obligation
    $cgmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Obligation -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Obligation -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Obligation -> r
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Obligation -> r
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> Obligation -> [u]
    gmapQ :: forall u. (forall d. Data d => d -> u) -> Obligation -> [u]
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Obligation -> u
    gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Obligation -> u
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Obligation -> m Obligation
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Obligation -> m Obligation
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Obligation -> m Obligation
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Obligation -> m Obligation
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Obligation -> m Obligation
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Obligation -> m Obligation
    Data

    -- | Properties of the obligation target to be checked.
    --
    -- @since 0.1
    data Property
        -- | Are the two functions equal?
        --
        -- More precisely: @f@ is equal to @g@ if either the definition of @f@ is
        -- @f = g@, or the definition of @g@ is @g = f@, or if the definitions are
        -- @f = e@ and @g = e@.
        --
        -- In general @f@ and @g@ need to be defined in this module, so that their
        -- actual defintions can be inspected.
        --
        -- The `Equivalence` indicates how strict to check for equality
        = EqualTo Name Equivalence

        -- | Do none of these types appear anywhere in the definition of the function
        -- (neither locally bound nor passed as arguments)
        --
        -- @since 0.3
        | NoTypes [Name]

        -- | Does this function perform no heap allocations.
        | NoAllocation

        -- | Does this value contain dictionaries (/except/ of the listed classes).
        --
        -- @since 0.3
        | NoTypeClasses [Name]

        -- | Does not contain this value (in terms or patterns)
        --
        -- @since 0.4.1
        | NoUseOf [Name]

        -- | Always satisfied, but dumps the value in non-quiet mode.
        --
        -- @since 0.4.2
        | CoreOf
        deriving Typeable Property
    Typeable Property =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> Property -> c Property)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c Property)
    -> (Property -> Constr)
    -> (Property -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c Property))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Property))
    -> ((forall b. Data b => b -> b) -> Property -> Property)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> Property -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> Property -> r)
    -> (forall u. (forall d. Data d => d -> u) -> Property -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> Property -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> Property -> m Property)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Property -> m Property)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Property -> m Property)
    -> Data Property
    Property -> Constr
    Property -> DataType
    (forall b. Data b => b -> b) -> Property -> Property
    forall a.
    Typeable a =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> Property -> u
    forall u. (forall d. Data d => d -> u) -> Property -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Property -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Property -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Property -> m Property
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Property -> m Property
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Property
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Property -> c Property
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Property)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Property)
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Property -> c Property
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Property -> c Property
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Property
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Property
    $ctoConstr :: Property -> Constr
    toConstr :: Property -> Constr
    $cdataTypeOf :: Property -> DataType
    dataTypeOf :: Property -> DataType
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Property)
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Property)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Property)
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Property)
    $cgmapT :: (forall b. Data b => b -> b) -> Property -> Property
    gmapT :: (forall b. Data b => b -> b) -> Property -> Property
    $cgmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Property -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Property -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Property -> r
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Property -> r
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> Property -> [u]
    gmapQ :: forall u. (forall d. Data d => d -> u) -> Property -> [u]
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Property -> u
    gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Property -> u
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Property -> m Property
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Property -> m Property
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Property -> m Property
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Property -> m Property
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Property -> m Property
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Property -> m Property
    Data

    -- | Equivalence of terms.
    --
    -- @since 0.5
    data Equivalence
        = StrictEquiv               -- ^ strict term equality
        | IgnoreTypesAndTicksEquiv  -- ^ ignore types and hpc ticks during the comparison
        | UnorderedLetsEquiv        -- ^ allow permuted let bindings, ignore types and hpc tick during comparison
        deriving Typeable Equivalence
    Typeable Equivalence =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> Equivalence -> c Equivalence)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c Equivalence)
    -> (Equivalence -> Constr)
    -> (Equivalence -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c Equivalence))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e))
        -> Maybe (c Equivalence))
    -> ((forall b. Data b => b -> b) -> Equivalence -> Equivalence)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> Equivalence -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> Equivalence -> r)
    -> (forall u. (forall d. Data d => d -> u) -> Equivalence -> [u])
    -> (forall u.
        Int -> (forall d. Data d => d -> u) -> Equivalence -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> Equivalence -> m Equivalence)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Equivalence -> m Equivalence)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Equivalence -> m Equivalence)
    -> Data Equivalence
    Equivalence -> Constr
    Equivalence -> DataType
    (forall b. Data b => b -> b) -> Equivalence -> Equivalence
    forall a.
    Typeable a =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> Equivalence -> u
    forall u. (forall d. Data d => d -> u) -> Equivalence -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Equivalence -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Equivalence -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Equivalence -> m Equivalence
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Equivalence -> m Equivalence
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Equivalence
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Equivalence -> c Equivalence
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Equivalence)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c Equivalence)
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Equivalence -> c Equivalence
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Equivalence -> c Equivalence
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Equivalence
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Equivalence
    $ctoConstr :: Equivalence -> Constr
    toConstr :: Equivalence -> Constr
    $cdataTypeOf :: Equivalence -> DataType
    dataTypeOf :: Equivalence -> DataType
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Equivalence)
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Equivalence)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c Equivalence)
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c Equivalence)
    $cgmapT :: (forall b. Data b => b -> b) -> Equivalence -> Equivalence
    gmapT :: (forall b. Data b => b -> b) -> Equivalence -> Equivalence
    $cgmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Equivalence -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Equivalence -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Equivalence -> r
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Equivalence -> r
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> Equivalence -> [u]
    gmapQ :: forall u. (forall d. Data d => d -> u) -> Equivalence -> [u]
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Equivalence -> u
    gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Equivalence -> u
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Equivalence -> m Equivalence
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Equivalence -> m Equivalence
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Equivalence -> m Equivalence
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Equivalence -> m Equivalence
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Equivalence -> m Equivalence
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Equivalence -> m Equivalence
    Data

    -- | Creates an inspection obligation for the given function name
    -- with default values for the optional fields.
    --
    -- @since 0.1
    mkObligation :: Name -> Property -> Obligation
    mkObligation :: Name -> Property -> Obligation
    mkObligation Name
    target Property
    prop = Obligation
        { target :: Name
    target = Name
    target
        , property :: Property
    property = Property
    prop
        , testName :: Maybe String
    testName = Maybe String
    forall a. Maybe a
    Nothing
        , srcLoc :: Maybe Loc
    srcLoc = Maybe Loc
    forall a. Maybe a
    Nothing
        , expectFail :: Bool
    expectFail = Bool
    False
        , storeResult :: Maybe String
    storeResult = Maybe String
    forall a. Maybe a
    Nothing
        }

    {- $convenience

    These convenience functions create common test obligations directly.
    -}

    -- | Declare two functions to be equal (see 'EqualTo')
    --
    -- @since 0.1
    (===) :: Name -> Name -> Obligation
    === :: Name -> Name -> Obligation
    (===) = Bool -> Equivalence -> Name -> Name -> Obligation
    mkEquality Bool
    False Equivalence
    StrictEquiv
    infix 9 ===

    -- | Declare two functions to be equal, but ignoring
    -- type lambdas, type arguments, type casts and hpc ticks (see 'EqualTo').
    -- Note that @-fhpc@ can prevent some optimizations; build without for more reliable analysis.
    --
    -- @since 0.1.1
    (==-) :: Name -> Name -> Obligation
    ==- :: Name -> Name -> Obligation
    (==-) = Bool -> Equivalence -> Name -> Name -> Obligation
    mkEquality Bool
    False Equivalence
    IgnoreTypesAndTicksEquiv
    infix 9 ==-

    -- | Declare two functions to be equal as @('==-')@ but also ignoring
    -- let bindings ordering (see 'EqualTo').
    --
    -- @since 0.5
    (==~) :: Name -> Name -> Obligation
    ==~ :: Name -> Name -> Obligation
    (==~) = Bool -> Equivalence -> Name -> Name -> Obligation
    mkEquality Bool
    False Equivalence
    UnorderedLetsEquiv
    infix 9 ==~

    -- | Declare two functions to be equal, but expect the test to fail (see 'EqualTo' and 'expectFail')
    -- (This is useful for documentation purposes, or as a TODO list.)
    --
    -- @since 0.1
    (=/=) :: Name -> Name -> Obligation
    =/= :: Name -> Name -> Obligation
    (=/=) = Bool -> Equivalence -> Name -> Name -> Obligation
    mkEquality Bool
    True Equivalence
    StrictEquiv
    infix 9 =/=

    -- | Declare two functions to be equal up to types (see '(==-)'),
    -- but expect the test to fail (see 'expectFail').
    --
    -- @since 0.4.3.0
    (=/-) :: Name -> Name -> Obligation
    =/- :: Name -> Name -> Obligation
    (=/-) = Bool -> Equivalence -> Name -> Name -> Obligation
    mkEquality Bool
    True Equivalence
    IgnoreTypesAndTicksEquiv
    infix 9 =/-

    -- | Declare two functions to be equal up to let binding ordering (see '(==~)'),
    -- but expect the test to fail (see 'expectFail').
    --
    -- @since 0.5
    (=/~) :: Name -> Name -> Obligation
    =/~ :: Name -> Name -> Obligation
    (=/~) = Bool -> Equivalence -> Name -> Name -> Obligation
    mkEquality Bool
    True Equivalence
    UnorderedLetsEquiv
    infix 9 =/~

    mkEquality :: Bool -> Equivalence -> Name -> Name -> Obligation
    mkEquality :: Bool -> Equivalence -> Name -> Name -> Obligation
    mkEquality Bool
    expectFail Equivalence
    ignore_types Name
    n1 Name
    n2 =
        (Name -> Property -> Obligation
    mkObligation Name
    n1 (Name -> Equivalence -> Property
    EqualTo Name
    n2 Equivalence
    ignore_types))
            { expectFail = expectFail }

    -- | Declare that in a function’s implementation, the given type does not occur.
    --
    -- More precisely: No locally bound variable (let-bound, lambda-bound or
    -- pattern-bound) has a type that contains the given type constructor.
    --
    -- @'inspect' $ fusedFunction ``hasNoType`` ''[]@
    --
    -- @since 0.1
    hasNoType :: Name -> Name -> Obligation
    hasNoType :: Name -> Name -> Obligation
    hasNoType Name
    n Name
    tn = Name -> Property -> Obligation
    mkObligation Name
    n ([Name] -> Property
    NoTypes [Name
    tn])

    -- | Declare that a function’s implementation does not contain any generic types.
    -- This is just 'hasNoType' applied to the usual type constructors used in
    -- "GHC.Generics".
    --
    -- @inspect $ hasNoGenerics genericFunction@
    --
    -- @since 0.3
    hasNoGenerics :: Name -> Obligation
    hasNoGenerics :: Name -> Obligation
    hasNoGenerics Name
    n =
        Name -> Property -> Obligation
    mkObligation Name
    n
            ([Name] -> Property
    NoTypes [ ''V1, ''U1, ''M1, ''K1, ''(:+:), ''(:*:), ''(:.:), ''Rec1
                     , ''Par1
                     ])

    -- | Declare that a function's implementation does not include dictionaries.
    --
    -- More precisely: No locally bound variable (let-bound, lambda-bound or
    -- pattern-bound) has a type that contains a type that mentions a type class.
    --
    -- @'inspect' $ 'hasNoTypeClasses' specializedFunction@
    --
    -- @since 0.3
    hasNoTypeClasses :: Name -> Obligation
    hasNoTypeClasses :: Name -> Obligation
    hasNoTypeClasses Name
    n = Name -> [Name] -> Obligation
    hasNoTypeClassesExcept Name
    n []

    -- | A variant of 'hasNoTypeClasses', which white-lists some type-classes.
    --
    -- @'inspect' $ fieldLens ``hasNoTypeClassesExcept`` [''Functor]@
    --
    -- @since 0.3
    hasNoTypeClassesExcept :: Name -> [Name] -> Obligation
    hasNoTypeClassesExcept :: Name -> [Name] -> Obligation
    hasNoTypeClassesExcept Name
    n [Name]
    tns = Name -> Property -> Obligation
    mkObligation Name
    n ([Name] -> Property
    NoTypeClasses [Name]
    tns)

    -- | Declare that a function's implementation does not use the given
    -- variable (either in terms or -- if it is a constructor -- in patterns).
    --
    -- @'inspect' $ foo ``doesNotUse`` 'error@
    --
    -- @since 0.4.1
    doesNotUse :: Name -> Name -> Obligation
    doesNotUse :: Name -> Name -> Obligation
    doesNotUse Name
    n Name
    ns = Name -> Property -> Obligation
    mkObligation Name
    n ([Name] -> Property
    NoUseOf [Name
    ns])

    -- | Dump the Core of the value.
    --
    -- @'inspect' $ 'coreOf' 'foo@
    --
    -- This is useful when you need to inspect some values manually.
    --
    -- @since 0.4.2
    coreOf :: Name -> Obligation
    coreOf :: Name -> Obligation
    coreOf Name
    n = Name -> Property -> Obligation
    mkObligation Name
    n Property
    CoreOf

    -- The exported TH functions

    inspectCommon :: AnnTarget -> Obligation -> Q [Dec]
    inspectCommon :: AnnTarget -> Obligation -> Q [Dec]
    inspectCommon AnnTarget
    annTarget Obligation
    obl = do
    #if MIN_VERSION_GLASGOW_HASKELL(8,4,0,0)
        String -> Q ()
    addCorePlugin String
    "Test.Inspection.Plugin"
    #endif
        loc <- Q Loc
    location
        annExpr <- liftData (obl { srcLoc = Just $ fromMaybe loc $ srcLoc obl })
        pure [PragmaD (AnnP annTarget annExpr)]

    -- | As seen in the example above, the entry point to inspection testing is the
    -- 'inspect' function, to which you pass an 'Obligation'.
    -- It will report test failures at compile time.
    --
    -- @since 0.1
    inspect :: Obligation -> Q [Dec]
    inspect :: Obligation -> Q [Dec]
    inspect = AnnTarget -> Obligation -> Q [Dec]
    inspectCommon AnnTarget
    ModuleAnnotation

    -- | The result of 'inspectTest', which has a more or less helpful text message
    --
    -- @since 0.2
    data Result = Failure String | Success String
        deriving Int -> Result -> ShowS
    [Result] -> ShowS
    Result -> String
    (Int -> Result -> ShowS)
    -> (Result -> String) -> ([Result] -> ShowS) -> Show Result
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Result -> ShowS
    showsPrec :: Int -> Result -> ShowS
    $cshow :: Result -> String
    show :: Result -> String
    $cshowList :: [Result] -> ShowS
    showList :: [Result] -> ShowS
    Show

    didNotRunPluginError :: Result
    didNotRunPluginError :: Result
    didNotRunPluginError = Result -> Result
    forall a. a -> a
    lazy (String -> Result
    forall a. HasCallStack => String -> a
    error String
    "Test.Inspection.Plugin did not run")
    {-# NOINLINE didNotRunPluginError #-}

    -- | This is a variant of 'inspect' that allows compilation to succeed in any case,
    -- and instead indicates the result as a value of type 'Result',
    -- which allows seamless integration into test frameworks.
    --
    -- This variant ignores the 'expectFail' field of the obligation. Instead,
    -- it is expected that you use the corresponding functionality in your test
    -- framework (e.g. [@tasty-expected-failure@](https://hackage.haskell.org/package/tasty-expected-failure))
    --
    -- @since 0.2
    inspectTest :: Obligation -> Q Exp
    inspectTest :: Obligation -> Q Exp
    inspectTest Obligation
    obl = do
        nameS <- Q String
    genName
        name <- newUniqueName nameS
        anns <- inspectCommon (ValueAnnotation name) obl
        addTopDecls $
            [ SigD name (ConT ''Result)
            , ValD (VarP name) (NormalB (VarE 'didNotRunPluginError)) []
            , PragmaD (InlineP name NoInline FunLike AllPhases)
            ] ++ anns
        return $ VarE name
      where
        genName :: Q String
    genName = do
            (r,c) <- Loc -> (Int, Int)
    loc_start (Loc -> (Int, Int)) -> Q Loc -> Q (Int, Int)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Q Loc
    location
            return $ "inspect_" ++ show r ++ "_" ++ show c

    -- | Like newName, but even more unique (unique across different splices),
    -- and with unique @nameBase@s. Precondition: the string is a valid Haskell
    -- alphanumeric identifier (could be upper- or lower-case).
    newUniqueName :: Quasi q => String -> q Name
    newUniqueName :: forall (q :: * -> *). Quasi q => String -> q Name
    newUniqueName String
    str = do
      n <- String -> q Name
    forall (q :: * -> *). Quasi q => String -> q Name
    qNewName String
    str
      qNewName $ show n
    -- This is from https://ghc.haskell.org/trac/ghc/ticket/13054#comment:1