    -- | See "Test.Inspection".
    --
    {-# LANGUAGE CPP #-}
    {-# LANGUAGE RecordWildCards #-}
    {-# LANGUAGE MultiWayIf #-}
    {-# LANGUAGE TemplateHaskell #-}
    {-# LANGUAGE LambdaCase #-}
    module Test.Inspection.Plugin
      ( plugin
      , checkProperty
      , CheckResult(..)
      , prettyProperty
      ) where

    import Control.Monad
    import System.Exit
    import Data.Either
    import Data.Maybe
    import Data.Bifunctor
    import Data.List
    import qualified Data.Map.Strict as M
    import qualified Language.Haskell.TH.Syntax as TH

    #if MIN_VERSION_ghc(9,4,0)
    import GHC.Types.Error
    import GHC.Driver.Session
    #endif

    #if MIN_VERSION_ghc(9,0,0)
    import GHC.Plugins hiding (SrcLoc)
    import GHC.Utils.Outputable as Outputable
    #else
    import GhcPlugins hiding (SrcLoc)
    import Outputable
    #endif

    #if MIN_VERSION_ghc(9,2,0)
    import GHC.Types.TyThing
    #endif

    import Test.Inspection (Obligation(..), Equivalence (..), Property(..), Result(..))
    import Test.Inspection.Core

    -- | The plugin. It supports some options:
    --
    -- * @-fplugin-opt=Test.Inspection.Plugin:keep-going@ to keep building despite failing obligations
    -- * @-fplugin-opt=Test.Inspection.Plugin:keep-going-O0@ to keep building despite failing obligations, when optimisations are off
    -- * @-fplugin-opt=Test.Inspection.Plugin:skip-O0@ to skip performing inspections when optimisations are off
    -- * @-fplugin-opt=Test.Inspection.Plugin:quiet@ to be silent if all obligations are fulfilled
    --
    -- It makes sense to enable only one of @keep-going@, @keep-going-O0@ and
    -- @skip-O0@ at a time. @skip-O0@ is useful when working with GHCi, to suppress
    -- inspection failure messages and eliminate the overhead of inspection when
    -- loading.

    plugin :: Plugin
    plugin :: Plugin
    plugin = Plugin
    defaultPlugin
        { installCoreToDos = install
    #if __GLASGOW_HASKELL__ >= 806
        , pluginRecompile = \[String]
    _args -> PluginRecompile -> IO PluginRecompile
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure PluginRecompile
    NoForceRecompile
    #endif
        }

    data UponFailure = AbortCompilation | KeepGoingO0 | SkipO0 | KeepGoing deriving UponFailure -> UponFailure -> Bool
    (UponFailure -> UponFailure -> Bool)
    -> (UponFailure -> UponFailure -> Bool) -> Eq UponFailure
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: UponFailure -> UponFailure -> Bool
    == :: UponFailure -> UponFailure -> Bool
    $c/= :: UponFailure -> UponFailure -> Bool
    /= :: UponFailure -> UponFailure -> Bool
    Eq

    data ReportingMode = Verbose | Quiet deriving ReportingMode -> ReportingMode -> Bool
    (ReportingMode -> ReportingMode -> Bool)
    -> (ReportingMode -> ReportingMode -> Bool) -> Eq ReportingMode
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: ReportingMode -> ReportingMode -> Bool
    == :: ReportingMode -> ReportingMode -> Bool
    $c/= :: ReportingMode -> ReportingMode -> Bool
    /= :: ReportingMode -> ReportingMode -> Bool
    Eq

    data ResultTarget = PrintAndAbort | StoreAt Name

    install :: [CommandLineOption] -> [CoreToDo] -> CoreM [CoreToDo]
    install :: [String] -> [CoreToDo] -> CoreM [CoreToDo]
    install [String]
    args [CoreToDo]
    passes = [CoreToDo] -> CoreM [CoreToDo]
    forall a. a -> CoreM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([CoreToDo] -> CoreM [CoreToDo]) -> [CoreToDo] -> CoreM [CoreToDo]
    forall a b. (a -> b) -> a -> b
    $ [CoreToDo]
    passes [CoreToDo] -> [CoreToDo] -> [CoreToDo]
    forall a. [a] -> [a] -> [a]
    ++ [CoreToDo
    pass]
      where
        pass :: CoreToDo
    pass = String -> CorePluginPass -> CoreToDo
    CoreDoPluginPass String
    "Test.Inspection.Plugin" (UponFailure -> ReportingMode -> CorePluginPass
    proofPass UponFailure
    upon_failure ReportingMode
    report)
        upon_failure :: UponFailure
    upon_failure | String
    "keep-going" String -> [String] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [String]
    args    = UponFailure
    KeepGoing
                     | String
    "keep-going-O0" String -> [String] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [String]
    args = UponFailure
    KeepGoingO0
                     | String
    "skip-O0" String -> [String] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [String]
    args       = UponFailure
    SkipO0
                     | Bool
    otherwise                   = UponFailure
    AbortCompilation
        report :: ReportingMode
    report | String
    "quiet" String -> [String] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [String]
    args = ReportingMode
    Quiet
               | Bool
    otherwise           = ReportingMode
    Verbose

    extractObligations :: ModGuts -> (ModGuts, [(ResultTarget, Obligation)])
    extractObligations :: ModGuts -> (ModGuts, [(ResultTarget, Obligation)])
    extractObligations ModGuts
    guts = (ModGuts
    guts', [(ResultTarget, Obligation)]
    obligations)
      where
        ([Annotation]
    anns_clean, [(ResultTarget, Obligation)]
    obligations) = (Annotation -> Maybe (ResultTarget, Obligation))
    -> [Annotation] -> ([Annotation], [(ResultTarget, Obligation)])
    forall a b. (a -> Maybe b) -> [a] -> ([a], [b])
    partitionMaybe Annotation -> Maybe (ResultTarget, Obligation)
    findObligationAnn (ModGuts -> [Annotation]
    mg_anns ModGuts
    guts)
        guts' :: ModGuts
    guts' = ModGuts
    guts { mg_anns = anns_clean }

    findObligationAnn :: Annotation -> Maybe (ResultTarget, Obligation)
    findObligationAnn :: Annotation -> Maybe (ResultTarget, Obligation)
    findObligationAnn (Annotation (ModuleTarget Module
    _) AnnPayload
    payload)
        | Just Obligation
    obl <- ([Word8] -> Obligation) -> AnnPayload -> Maybe Obligation
    forall a. Typeable a => ([Word8] -> a) -> AnnPayload -> Maybe a
    fromSerialized [Word8] -> Obligation
    forall a. Data a => [Word8] -> a
    deserializeWithData AnnPayload
    payload
        = (ResultTarget, Obligation) -> Maybe (ResultTarget, Obligation)
    forall a. a -> Maybe a
    Just (ResultTarget
    PrintAndAbort, Obligation
    obl)
    findObligationAnn (Annotation (NamedTarget Name
    n) AnnPayload
    payload)
        | Just Obligation
    obl <- ([Word8] -> Obligation) -> AnnPayload -> Maybe Obligation
    forall a. Typeable a => ([Word8] -> a) -> AnnPayload -> Maybe a
    fromSerialized [Word8] -> Obligation
    forall a. Data a => [Word8] -> a
    deserializeWithData AnnPayload
    payload
        = (ResultTarget, Obligation) -> Maybe (ResultTarget, Obligation)
    forall a. a -> Maybe a
    Just (Name -> ResultTarget
    StoreAt Name
    n, Obligation
    obl)
    findObligationAnn Annotation
    _
        = Maybe (ResultTarget, Obligation)
    forall a. Maybe a
    Nothing

    prettyObligation :: Module -> Obligation -> String -> String
    prettyObligation :: Module -> Obligation -> String -> String
    prettyObligation Module
    mod (Obligation {Bool
    Maybe String
    Maybe Loc
    Name
    Property
    target :: Name
    property :: Property
    testName :: Maybe String
    expectFail :: Bool
    srcLoc :: Maybe Loc
    storeResult :: Maybe String
    storeResult :: Obligation -> Maybe String
    srcLoc :: Obligation -> Maybe Loc
    expectFail :: Obligation -> Bool
    testName :: Obligation -> Maybe String
    property :: Obligation -> Property
    target :: Obligation -> Name
    ..}) String
    result =
        String -> (Loc -> String) -> Maybe Loc -> String
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe String
    "" Loc -> String
    myPrettySrcLoc Maybe Loc
    srcLoc String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ": " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    name String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    result
      where
        name :: String
    name = case Maybe String
    testName of
            Just String
    n -> String
    n
            Maybe String
    Nothing -> (Name -> String) -> Name -> Property -> String
    prettyProperty (Module -> Name -> String
    showTHName Module
    mod) Name
    target Property
    property

    prettyProperty :: (TH.Name -> String) -> TH.Name -> Property -> String
    prettyProperty :: (Name -> String) -> Name -> Property -> String
    prettyProperty Name -> String
    showName Name
    target = \case
      EqualTo Name
    n2 Equivalence
    eqv   -> Name -> String
    showName Name
    target String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Equivalence -> String
    showEquiv Equivalence
    eqv String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Name -> String
    showName Name
    n2
      NoTypes [Name
    t]      -> Name -> String
    showName Name
    target String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " `hasNoType` " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Name -> String
    showName Name
    t
      NoTypes [Name]
    ts       -> Name -> String
    showName Name
    target String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " mentions none of " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    ", " ((Name -> String) -> [Name] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> String
    showName [Name]
    ts)
      Property
    NoAllocation     -> Name -> String
    showName Name
    target String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " does not allocate"
      NoTypeClasses [] -> Name -> String
    showName Name
    target String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " does not contain dictionary values"
      NoTypeClasses [Name]
    ts -> Name -> String
    showName Name
    target String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " does not contain dictionary values except of " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    ", " ((Name -> String) -> [Name] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> String
    showName [Name]
    ts)
      NoUseOf [Name]
    ns       -> Name -> String
    showName Name
    target String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " uses none of " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    ", " ((Name -> String) -> [Name] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> String
    showName [Name]
    ns)
      Property
    CoreOf           -> Name -> String
    showName Name
    target String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " core dump" -- :)
      where
        showEquiv :: Equivalence -> String
    showEquiv Equivalence
    StrictEquiv              = String
    "==="
        showEquiv Equivalence
    IgnoreTypesAndTicksEquiv = String
    "==-"
        showEquiv Equivalence
    UnorderedLetsEquiv       = String
    "==~"

    -- | Like show, but omit the module name if it is he current module
    showTHName :: Module -> TH.Name -> String
    showTHName :: Module -> Name -> String
    showTHName Module
    mod (TH.Name OccName
    occ (TH.NameQ ModName
    m))
        | ModuleName -> String
    moduleNameString (Module -> ModuleName
    forall unit. GenModule unit -> ModuleName
    moduleName Module
    mod) String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == ModName -> String
    TH.modString ModName
    m = OccName -> String
    TH.occString OccName
    occ
    showTHName Module
    mod (TH.Name OccName
    occ (TH.NameG NameSpace
    _ PkgName
    _ ModName
    m))
        | ModuleName -> String
    moduleNameString (Module -> ModuleName
    forall unit. GenModule unit -> ModuleName
    moduleName Module
    mod) String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == ModName -> String
    TH.modString ModName
    m = OccName -> String
    TH.occString OccName
    occ
    showTHName Module
    _ Name
    n = Name -> String
    forall a. Show a => a -> String
    show Name
    n

    data Stat = ExpSuccess | ExpFailure | UnexpSuccess | UnexpFailure | StoredResult
        deriving (Int -> Stat
    Stat -> Int
    Stat -> [Stat]
    Stat -> Stat
    Stat -> Stat -> [Stat]
    Stat -> Stat -> Stat -> [Stat]
    (Stat -> Stat)
    -> (Stat -> Stat)
    -> (Int -> Stat)
    -> (Stat -> Int)
    -> (Stat -> [Stat])
    -> (Stat -> Stat -> [Stat])
    -> (Stat -> Stat -> [Stat])
    -> (Stat -> Stat -> Stat -> [Stat])
    -> Enum Stat
    forall a.
    (a -> a)
    -> (a -> a)
    -> (Int -> a)
    -> (a -> Int)
    -> (a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> a -> [a])
    -> Enum a
    $csucc :: Stat -> Stat
    succ :: Stat -> Stat
    $cpred :: Stat -> Stat
    pred :: Stat -> Stat
    $ctoEnum :: Int -> Stat
    toEnum :: Int -> Stat
    $cfromEnum :: Stat -> Int
    fromEnum :: Stat -> Int
    $cenumFrom :: Stat -> [Stat]
    enumFrom :: Stat -> [Stat]
    $cenumFromThen :: Stat -> Stat -> [Stat]
    enumFromThen :: Stat -> Stat -> [Stat]
    $cenumFromTo :: Stat -> Stat -> [Stat]
    enumFromTo :: Stat -> Stat -> [Stat]
    $cenumFromThenTo :: Stat -> Stat -> Stat -> [Stat]
    enumFromThenTo :: Stat -> Stat -> Stat -> [Stat]
    Enum, Stat -> Stat -> Bool
    (Stat -> Stat -> Bool) -> (Stat -> Stat -> Bool) -> Eq Stat
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Stat -> Stat -> Bool
    == :: Stat -> Stat -> Bool
    $c/= :: Stat -> Stat -> Bool
    /= :: Stat -> Stat -> Bool
    Eq, Eq Stat
    Eq Stat =>
    (Stat -> Stat -> Ordering)
    -> (Stat -> Stat -> Bool)
    -> (Stat -> Stat -> Bool)
    -> (Stat -> Stat -> Bool)
    -> (Stat -> Stat -> Bool)
    -> (Stat -> Stat -> Stat)
    -> (Stat -> Stat -> Stat)
    -> Ord Stat
    Stat -> Stat -> Bool
    Stat -> Stat -> Ordering
    Stat -> Stat -> Stat
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: Stat -> Stat -> Ordering
    compare :: Stat -> Stat -> Ordering
    $c< :: Stat -> Stat -> Bool
    < :: Stat -> Stat -> Bool
    $c<= :: Stat -> Stat -> Bool
    <= :: Stat -> Stat -> Bool
    $c> :: Stat -> Stat -> Bool
    > :: Stat -> Stat -> Bool
    $c>= :: Stat -> Stat -> Bool
    >= :: Stat -> Stat -> Bool
    $cmax :: Stat -> Stat -> Stat
    max :: Stat -> Stat -> Stat
    $cmin :: Stat -> Stat -> Stat
    min :: Stat -> Stat -> Stat
    Ord, Stat
    Stat -> Stat -> Bounded Stat
    forall a. a -> a -> Bounded a
    $cminBound :: Stat
    minBound :: Stat
    $cmaxBound :: Stat
    maxBound :: Stat
    Bounded)
    type Stats = M.Map Stat Int

    type Updates = [(Name, Result)]

    tick :: Stat -> Stats
    tick :: Stat -> Stats
    tick Stat
    s = Stat -> Int -> Stats
    forall k a. k -> a -> Map k a
    M.singleton Stat
    s Int
    1

    checkObligation :: ReportingMode -> ModGuts -> (ResultTarget, Obligation) -> CoreM (Updates, Stats)
    checkObligation :: ReportingMode
    -> ModGuts -> (ResultTarget, Obligation) -> CoreM (Updates, Stats)
    checkObligation ReportingMode
    report ModGuts
    guts (ResultTarget
    reportTarget, Obligation
    obl) = do

        res <- ModGuts -> Name -> Property -> CoreM CheckResult
    checkProperty ModGuts
    guts (Obligation -> Name
    target Obligation
    obl) (Obligation -> Property
    property Obligation
    obl)
        case reportTarget of
            ResultTarget
    PrintAndAbort -> do
                category <- case (CheckResult
    res, Obligation -> Bool
    expectFail Obligation
    obl) of
                    -- Property holds
                    (CheckResult
    ResSuccess, Bool
    False) -> do
                        Bool -> CoreM () -> CoreM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (ReportingMode
    report ReportingMode -> ReportingMode -> Bool
    forall a. Eq a => a -> a -> Bool
    == ReportingMode
    Quiet) (CoreM () -> CoreM ()) -> CoreM () -> CoreM ()
    forall a b. (a -> b) -> a -> b
    $
                            String -> CoreM ()
    putMsgS (String -> CoreM ()) -> String -> CoreM ()
    forall a b. (a -> b) -> a -> b
    $ Module -> Obligation -> String -> String
    prettyObligation (ModGuts -> Module
    mg_module ModGuts
    guts) Obligation
    obl String
    expSuccess
                        Stat -> CoreM Stat
    forall a. a -> CoreM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Stat
    ExpSuccess
                    (CheckResult
    ResSuccess, Bool
    True) -> do
                        String -> CoreM ()
    putMsgS (String -> CoreM ()) -> String -> CoreM ()
    forall a b. (a -> b) -> a -> b
    $ Module -> Obligation -> String -> String
    prettyObligation (ModGuts -> Module
    mg_module ModGuts
    guts) Obligation
    obl String
    unexpSuccess
                        Stat -> CoreM Stat
    forall a. a -> CoreM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Stat
    UnexpSuccess
                    -- Property holds, with extra message
                    (ResSuccessWithMessage SDoc
    reportDoc, Bool
    False) -> do
                        Bool -> CoreM () -> CoreM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (ReportingMode
    report ReportingMode -> ReportingMode -> Bool
    forall a. Eq a => a -> a -> Bool
    == ReportingMode
    Quiet) (CoreM () -> CoreM ()) -> CoreM () -> CoreM ()
    forall a b. (a -> b) -> a -> b
    $ do
                            String -> CoreM ()
    putMsgS (String -> CoreM ()) -> String -> CoreM ()
    forall a b. (a -> b) -> a -> b
    $ Module -> Obligation -> String -> String
    prettyObligation (ModGuts -> Module
    mg_module ModGuts
    guts) Obligation
    obl String
    expSuccess
                            SDoc -> CoreM ()
    putMsg SDoc
    reportDoc
                        Stat -> CoreM Stat
    forall a. a -> CoreM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Stat
    ExpSuccess
                    (ResSuccessWithMessage SDoc
    reportDoc, Bool
    True) -> do
                        String -> CoreM ()
    putMsgS (String -> CoreM ()) -> String -> CoreM ()
    forall a b. (a -> b) -> a -> b
    $ Module -> Obligation -> String -> String
    prettyObligation (ModGuts -> Module
    mg_module ModGuts
    guts) Obligation
    obl String
    unexpSuccess
                        SDoc -> CoreM ()
    putMsg SDoc
    reportDoc
                        Stat -> CoreM Stat
    forall a. a -> CoreM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Stat
    UnexpSuccess
                    -- Property does not hold
                    (ResFailure SDoc
    reportDoc, Bool
    False) -> do
                        String -> CoreM ()
    putMsgS (String -> CoreM ()) -> String -> CoreM ()
    forall a b. (a -> b) -> a -> b
    $ Module -> Obligation -> String -> String
    prettyObligation (ModGuts -> Module
    mg_module ModGuts
    guts) Obligation
    obl String
    unexpFailure
                        SDoc -> CoreM ()
    putMsg (SDoc -> CoreM ()) -> SDoc -> CoreM ()
    forall a b. (a -> b) -> a -> b
    $ SDoc
    reportDoc
                        Stat -> CoreM Stat
    forall a. a -> CoreM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Stat
    UnexpFailure
                    (ResFailure SDoc
    _, Bool
    True) -> do
                        Bool -> CoreM () -> CoreM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (ReportingMode
    report ReportingMode -> ReportingMode -> Bool
    forall a. Eq a => a -> a -> Bool
    == ReportingMode
    Quiet) (CoreM () -> CoreM ()) -> CoreM () -> CoreM ()
    forall a b. (a -> b) -> a -> b
    $
                            String -> CoreM ()
    putMsgS (String -> CoreM ()) -> String -> CoreM ()
    forall a b. (a -> b) -> a -> b
    $ Module -> Obligation -> String -> String
    prettyObligation (ModGuts -> Module
    mg_module ModGuts
    guts) Obligation
    obl String
    expFailure
                        Stat -> CoreM Stat
    forall a. a -> CoreM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Stat
    ExpFailure
                return ([], tick category)
            StoreAt Name
    name -> do
                dflags <- CoreM DynFlags
    forall (m :: * -> *). HasDynFlags m => m DynFlags
    getDynFlags
                let result = case CheckResult
    res of
                        CheckResult
    ResSuccess -> String -> Result
    Success (String -> Result) -> String -> Result
    forall a b. (a -> b) -> a -> b
    $ DynFlags -> SDoc -> String
    showSDoc DynFlags
    dflags (SDoc -> String) -> SDoc -> String
    forall a b. (a -> b) -> a -> b
    $
                            String -> SDoc
    forall doc. IsLine doc => String -> doc
    text (Module -> Obligation -> String -> String
    prettyObligation (ModGuts -> Module
    mg_module ModGuts
    guts) Obligation
    obl String
    expSuccess)
                        ResSuccessWithMessage SDoc
    msg -> String -> Result
    Success (String -> Result) -> String -> Result
    forall a b. (a -> b) -> a -> b
    $ DynFlags -> SDoc -> String
    showSDoc DynFlags
    dflags (SDoc -> String) -> SDoc -> String
    forall a b. (a -> b) -> a -> b
    $
                            String -> SDoc
    forall doc. IsLine doc => String -> doc
    text (Module -> Obligation -> String -> String
    prettyObligation (ModGuts -> Module
    mg_module ModGuts
    guts) Obligation
    obl String
    expSuccess) SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$
                            SDoc
    msg
                        ResFailure SDoc
    reportMsg -> String -> Result
    Failure (String -> Result) -> String -> Result
    forall a b. (a -> b) -> a -> b
    $ DynFlags -> SDoc -> String
    showSDoc DynFlags
    dflags (SDoc -> String) -> SDoc -> String
    forall a b. (a -> b) -> a -> b
    $
                            String -> SDoc
    forall doc. IsLine doc => String -> doc
    text (Module -> Obligation -> String -> String
    prettyObligation (ModGuts -> Module
    mg_module ModGuts
    guts) Obligation
    obl String
    unexpFailure) SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$
                            SDoc
    reportMsg
                pure ([(name, result)], tick StoredResult)

      where
        expSuccess :: String
    expSuccess   = String
    "passed."
        unexpSuccess :: String
    unexpSuccess = String
    "passed unexpectedly!"
        unexpFailure :: String
    unexpFailure = String
    "failed:"
        expFailure :: String
    expFailure   = String
    "failed expectedly."

    data CheckResult
        = ResSuccess
        | ResSuccessWithMessage SDoc
        | ResFailure SDoc

    lookupNameInGuts :: ModGuts -> Name -> Maybe (Var, CoreExpr)
    lookupNameInGuts :: ModGuts -> Name -> Maybe (CoreBndr, CoreExpr)
    lookupNameInGuts ModGuts
    guts Name
    n = [(CoreBndr, CoreExpr)] -> Maybe (CoreBndr, CoreExpr)
    forall a. [a] -> Maybe a
    listToMaybe
        [ (CoreBndr
    v,CoreExpr
    e)
        | (CoreBndr
    v,CoreExpr
    e) <- [Bind CoreBndr] -> [(CoreBndr, CoreExpr)]
    forall b. [Bind b] -> [(b, Expr b)]
    flattenBinds (ModGuts -> [Bind CoreBndr]
    mg_binds ModGuts
    guts)
        , CoreBndr -> Name
    forall a. NamedThing a => a -> Name
    getName CoreBndr
    v Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name
    n
        ]

    updateNameInGuts :: Name -> CoreExpr -> ModGuts -> ModGuts
    updateNameInGuts :: Name -> CoreExpr -> ModGuts -> ModGuts
    updateNameInGuts Name
    n CoreExpr
    expr ModGuts
    guts =
        ModGuts
    guts {mg_binds = map (updateNameInGut n expr) (mg_binds guts) }

    updateNameInGut :: Name -> CoreExpr -> CoreBind -> CoreBind
    updateNameInGut :: Name -> CoreExpr -> Bind CoreBndr -> Bind CoreBndr
    updateNameInGut Name
    n CoreExpr
    e (NonRec CoreBndr
    v CoreExpr
    _) | CoreBndr -> Name
    forall a. NamedThing a => a -> Name
    getName CoreBndr
    v Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name
    n = CoreBndr -> CoreExpr -> Bind CoreBndr
    forall b. b -> Expr b -> Bind b
    NonRec CoreBndr
    v CoreExpr
    e
    updateNameInGut Name
    _ CoreExpr
    _ Bind CoreBndr
    bind                          = Bind CoreBndr
    bind

    checkProperty :: ModGuts -> TH.Name -> Property -> CoreM CheckResult
    checkProperty :: ModGuts -> Name -> Property -> CoreM CheckResult
    checkProperty ModGuts
    guts Name
    thn1 (EqualTo Name
    thn2 Equivalence
    ignore_types) = do
        n1 <- Name -> CoreM Name
    fromTHName Name
    thn1
        n2 <- fromTHName thn2

        let p1 = ModGuts -> Name -> Maybe (CoreBndr, CoreExpr)
    lookupNameInGuts ModGuts
    guts Name
    n1
        let p2 = ModGuts -> Name -> Maybe (CoreBndr, CoreExpr)
    lookupNameInGuts ModGuts
    guts Name
    n2

        if | n1 == n2
           -> pure ResSuccess
           -- Ok if one points to another
           | Just (_, Var other) <- p1, getName other == n2
           -> pure ResSuccess
           | Just (_, Var other) <- p2, getName other == n1
           -> pure ResSuccess
           | Just (v1, _) <- p1
           , Just (v2, _) <- p2
           , let slice1 = [(CoreBndr, CoreExpr)] -> CoreBndr -> [(CoreBndr, CoreExpr)]
    slice [(CoreBndr, CoreExpr)]
    binds CoreBndr
    v1
           , let slice2 = [(CoreBndr, CoreExpr)] -> CoreBndr -> [(CoreBndr, CoreExpr)]
    slice [(CoreBndr, CoreExpr)]
    binds CoreBndr
    v2
           -> case eqSlice' ignore_types slice1 slice2 of
                -- OK if they have the same expression
                Right ()
    _ -> CheckResult -> CoreM CheckResult
    forall a. a -> CoreM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CheckResult
    ResSuccess
              -- Not ok if the expression differ
                Left SDoc
    err -> CheckResult -> CoreM CheckResult
    forall a. a -> CoreM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (CheckResult -> CoreM CheckResult)
    -> (SDoc -> CheckResult) -> SDoc -> CoreM CheckResult
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SDoc -> CheckResult
    ResFailure (SDoc -> CoreM CheckResult) -> SDoc -> CoreM CheckResult
    forall a b. (a -> b) -> a -> b
    $ SDoc
    err SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$ [(CoreBndr, CoreExpr)] -> [(CoreBndr, CoreExpr)] -> SDoc
    pprSliceDifference [(CoreBndr, CoreExpr)]
    slice1 [(CoreBndr, CoreExpr)]
    slice2
           -- Not ok if both names are bound externally
           | Nothing <- p1
           , Nothing <- p2
           -> pure . ResFailure $ ppr n1 <+> text " and " <+> ppr n2 <+>
                    text "are different external names"
           | Nothing <- p1
           -> pure . ResFailure $ ppr n1 <+> text "is an external name"
           | Nothing <- p2
           -> pure . ResFailure $ ppr n2 <+> text "is an external name"
      where
        binds :: [(CoreBndr, CoreExpr)]
    binds = [Bind CoreBndr] -> [(CoreBndr, CoreExpr)]
    forall b. [Bind b] -> [(b, Expr b)]
    flattenBinds (ModGuts -> [Bind CoreBndr]
    mg_binds ModGuts
    guts)

    checkProperty ModGuts
    guts Name
    thn (NoUseOf [Name]
    thns) = do
        n <- Name -> CoreM Name
    fromTHName Name
    thn
        ns <- mapM fromTHName thns
        case lookupNameInGuts guts n of
            Maybe (CoreBndr, CoreExpr)
    Nothing -> CheckResult -> CoreM CheckResult
    forall a. a -> CoreM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (CheckResult -> CoreM CheckResult)
    -> (SDoc -> CheckResult) -> SDoc -> CoreM CheckResult
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SDoc -> CheckResult
    ResFailure (SDoc -> CoreM CheckResult) -> SDoc -> CoreM CheckResult
    forall a b. (a -> b) -> a -> b
    $ Name -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Name
    n SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "is not a local name"
            Just (CoreBndr
    v, CoreExpr
    _) -> case [(CoreBndr, CoreExpr)] -> [Name] -> Maybe (CoreBndr, CoreExpr)
    freeOfTerm ([(CoreBndr, CoreExpr)] -> CoreBndr -> [(CoreBndr, CoreExpr)]
    slice [(CoreBndr, CoreExpr)]
    binds CoreBndr
    v) [Name]
    ns of
                Just (CoreBndr, CoreExpr)
    _ -> CheckResult -> CoreM CheckResult
    forall a. a -> CoreM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (CheckResult -> CoreM CheckResult)
    -> (SDoc -> CheckResult) -> SDoc -> CoreM CheckResult
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SDoc -> CheckResult
    ResFailure (SDoc -> CoreM CheckResult) -> SDoc -> CoreM CheckResult
    forall a b. (a -> b) -> a -> b
    $ [(CoreBndr, CoreExpr)] -> SDoc
    pprSlice ([(CoreBndr, CoreExpr)] -> CoreBndr -> [(CoreBndr, CoreExpr)]
    slice [(CoreBndr, CoreExpr)]
    binds CoreBndr
    v)
                Maybe (CoreBndr, CoreExpr)
    Nothing -> CheckResult -> CoreM CheckResult
    forall a. a -> CoreM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CheckResult
    ResSuccess
      where binds :: [(CoreBndr, CoreExpr)]
    binds = [Bind CoreBndr] -> [(CoreBndr, CoreExpr)]
    forall b. [Bind b] -> [(b, Expr b)]
    flattenBinds (ModGuts -> [Bind CoreBndr]
    mg_binds ModGuts
    guts)

    checkProperty ModGuts
    guts Name
    thn (NoTypes [Name]
    thts) = do
        n <- Name -> CoreM Name
    fromTHName Name
    thn
        ts <- mapM fromTHName thts
        case lookupNameInGuts guts n of
            Maybe (CoreBndr, CoreExpr)
    Nothing -> CheckResult -> CoreM CheckResult
    forall a. a -> CoreM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (CheckResult -> CoreM CheckResult)
    -> (SDoc -> CheckResult) -> SDoc -> CoreM CheckResult
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SDoc -> CheckResult
    ResFailure (SDoc -> CoreM CheckResult) -> SDoc -> CoreM CheckResult
    forall a b. (a -> b) -> a -> b
    $ Name -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Name
    n SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "is not a local name"
            Just (CoreBndr
    v, CoreExpr
    _) -> case [(CoreBndr, CoreExpr)] -> [Name] -> Maybe (CoreBndr, CoreExpr)
    freeOfType ([(CoreBndr, CoreExpr)] -> CoreBndr -> [(CoreBndr, CoreExpr)]
    slice [(CoreBndr, CoreExpr)]
    binds CoreBndr
    v) [Name]
    ts of
                Just (CoreBndr, CoreExpr)
    _ -> CheckResult -> CoreM CheckResult
    forall a. a -> CoreM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (CheckResult -> CoreM CheckResult)
    -> (SDoc -> CheckResult) -> SDoc -> CoreM CheckResult
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SDoc -> CheckResult
    ResFailure (SDoc -> CoreM CheckResult) -> SDoc -> CoreM CheckResult
    forall a b. (a -> b) -> a -> b
    $ [(CoreBndr, CoreExpr)] -> SDoc
    pprSlice ([(CoreBndr, CoreExpr)] -> CoreBndr -> [(CoreBndr, CoreExpr)]
    slice [(CoreBndr, CoreExpr)]
    binds CoreBndr
    v)
                Maybe (CoreBndr, CoreExpr)
    Nothing -> CheckResult -> CoreM CheckResult
    forall a. a -> CoreM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CheckResult
    ResSuccess
      where binds :: [(CoreBndr, CoreExpr)]
    binds = [Bind CoreBndr] -> [(CoreBndr, CoreExpr)]
    forall b. [Bind b] -> [(b, Expr b)]
    flattenBinds (ModGuts -> [Bind CoreBndr]
    mg_binds ModGuts
    guts)

    checkProperty ModGuts
    guts Name
    thn Property
    NoAllocation = do
        n <- Name -> CoreM Name
    fromTHName Name
    thn
        case lookupNameInGuts guts n of
            Maybe (CoreBndr, CoreExpr)
    Nothing -> CheckResult -> CoreM CheckResult
    forall a. a -> CoreM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (CheckResult -> CoreM CheckResult)
    -> (SDoc -> CheckResult) -> SDoc -> CoreM CheckResult
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SDoc -> CheckResult
    ResFailure (SDoc -> CoreM CheckResult) -> SDoc -> CoreM CheckResult
    forall a b. (a -> b) -> a -> b
    $ Name -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Name
    n SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "is not a local name"
            Just (CoreBndr
    v, CoreExpr
    _) -> case [(CoreBndr, CoreExpr)] -> Maybe (CoreBndr, CoreExpr)
    doesNotAllocate ([(CoreBndr, CoreExpr)] -> CoreBndr -> [(CoreBndr, CoreExpr)]
    slice [(CoreBndr, CoreExpr)]
    binds CoreBndr
    v) of
                Just (CoreBndr
    v',CoreExpr
    e') -> CheckResult -> CoreM CheckResult
    forall a. a -> CoreM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (CheckResult -> CoreM CheckResult)
    -> (SDoc -> CheckResult) -> SDoc -> CoreM CheckResult
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SDoc -> CheckResult
    ResFailure (SDoc -> CoreM CheckResult) -> SDoc -> CoreM CheckResult
    forall a b. (a -> b) -> a -> b
    $ Int -> SDoc -> SDoc
    nest Int
    4 (CoreBndr -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr CoreBndr
    v' SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "=" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> CoreExpr -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr CoreExpr
    e')
                Maybe (CoreBndr, CoreExpr)
    Nothing -> CheckResult -> CoreM CheckResult
    forall a. a -> CoreM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CheckResult
    ResSuccess
      where binds :: [(CoreBndr, CoreExpr)]
    binds = [Bind CoreBndr] -> [(CoreBndr, CoreExpr)]
    forall b. [Bind b] -> [(b, Expr b)]
    flattenBinds (ModGuts -> [Bind CoreBndr]
    mg_binds ModGuts
    guts)

    checkProperty ModGuts
    guts Name
    thn (NoTypeClasses [Name]
    thts) = do
        n <- Name -> CoreM Name
    fromTHName Name
    thn
        ts <- mapM fromTHName thts
        case lookupNameInGuts guts n of
            Maybe (CoreBndr, CoreExpr)
    Nothing -> CheckResult -> CoreM CheckResult
    forall a. a -> CoreM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (CheckResult -> CoreM CheckResult)
    -> (SDoc -> CheckResult) -> SDoc -> CoreM CheckResult
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SDoc -> CheckResult
    ResFailure (SDoc -> CoreM CheckResult) -> SDoc -> CoreM CheckResult
    forall a b. (a -> b) -> a -> b
    $ Name -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Name
    n SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "is not a local name"
            Just (CoreBndr
    v, CoreExpr
    _) -> case [(CoreBndr, CoreExpr)]
    -> [Name] -> Maybe (CoreBndr, CoreExpr, [TyCon])
    doesNotContainTypeClasses ([(CoreBndr, CoreExpr)] -> CoreBndr -> [(CoreBndr, CoreExpr)]
    slice [(CoreBndr, CoreExpr)]
    binds CoreBndr
    v) [Name]
    ts of
                Just (CoreBndr
    v',CoreExpr
    e',[TyCon]
    tc) -> CheckResult -> CoreM CheckResult
    forall a. a -> CoreM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (CheckResult -> CoreM CheckResult)
    -> (SDoc -> CheckResult) -> SDoc -> CoreM CheckResult
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SDoc -> CheckResult
    ResFailure
                    (SDoc -> CoreM CheckResult) -> SDoc -> CoreM CheckResult
    forall a b. (a -> b) -> a -> b
    $ Int -> SDoc -> SDoc
    nest Int
    4 (SDoc -> SDoc) -> SDoc -> SDoc
    forall a b. (a -> b) -> a -> b
    $ [SDoc] -> SDoc
    forall doc. IsDoc doc => [doc] -> doc
    vcat
                        [ String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "Found type classes: " SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> [TyCon] -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr [TyCon]
    tc
                        , CoreBndr -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr CoreBndr
    v' SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "=" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> CoreExpr -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr CoreExpr
    e'
                        ]
                Maybe (CoreBndr, CoreExpr, [TyCon])
    Nothing -> CheckResult -> CoreM CheckResult
    forall a. a -> CoreM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CheckResult
    ResSuccess
      where binds :: [(CoreBndr, CoreExpr)]
    binds = [Bind CoreBndr] -> [(CoreBndr, CoreExpr)]
    forall b. [Bind b] -> [(b, Expr b)]
    flattenBinds (ModGuts -> [Bind CoreBndr]
    mg_binds ModGuts
    guts)

    checkProperty ModGuts
    guts Name
    thn Property
    CoreOf = do
        n <- Name -> CoreM Name
    fromTHName Name
    thn
        case lookupNameInGuts guts n of
            Maybe (CoreBndr, CoreExpr)
    Nothing -> CheckResult -> CoreM CheckResult
    forall a. a -> CoreM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (CheckResult -> CoreM CheckResult)
    -> (SDoc -> CheckResult) -> SDoc -> CoreM CheckResult
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SDoc -> CheckResult
    ResFailure (SDoc -> CoreM CheckResult) -> SDoc -> CoreM CheckResult
    forall a b. (a -> b) -> a -> b
    $ Name -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Name
    n SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "is not a local name"
            Just (CoreBndr
    v, CoreExpr
    _) -> do
                let s :: [(CoreBndr, CoreExpr)]
    s = [(CoreBndr, CoreExpr)] -> CoreBndr -> [(CoreBndr, CoreExpr)]
    slice [(CoreBndr, CoreExpr)]
    binds CoreBndr
    v
                CheckResult -> CoreM CheckResult
    forall a. a -> CoreM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (CheckResult -> CoreM CheckResult)
    -> CheckResult -> CoreM CheckResult
    forall a b. (a -> b) -> a -> b
    $ SDoc -> CheckResult
    ResSuccessWithMessage (SDoc -> CheckResult) -> SDoc -> CheckResult
    forall a b. (a -> b) -> a -> b
    $ Int -> SDoc -> SDoc
    nest Int
    4 (SDoc -> SDoc) -> SDoc -> SDoc
    forall a b. (a -> b) -> a -> b
    $ [(CoreBndr, CoreExpr)] -> SDoc
    pprSlice [(CoreBndr, CoreExpr)]
    s
      where binds :: [(CoreBndr, CoreExpr)]
    binds = [Bind CoreBndr] -> [(CoreBndr, CoreExpr)]
    forall b. [Bind b] -> [(b, Expr b)]
    flattenBinds (ModGuts -> [Bind CoreBndr]
    mg_binds ModGuts
    guts)

    fromTHName :: TH.Name -> CoreM Name
    fromTHName :: Name -> CoreM Name
    fromTHName Name
    thn = Name -> CoreM (Maybe Name)
    thNameToGhcName Name
    thn CoreM (Maybe Name) -> (Maybe Name -> CoreM Name) -> CoreM Name
    forall a b. CoreM a -> (a -> CoreM b) -> CoreM b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Maybe Name
    Nothing -> do
            SDoc -> CoreM ()
    errorMsg (SDoc -> CoreM ()) -> SDoc -> CoreM ()
    forall a b. (a -> b) -> a -> b
    $ String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "Could not resolve TH name" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text (Name -> String
    forall a. Show a => a -> String
    show Name
    thn)
            IO Name -> CoreM Name
    forall a. IO a -> CoreM a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO Name -> CoreM Name) -> IO Name -> CoreM Name
    forall a b. (a -> b) -> a -> b
    $ IO Name
    forall a. IO a
    exitFailure -- kill the compiler. Is there a nicer way?
        Just Name
    n -> Name -> CoreM Name
    forall a. a -> CoreM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Name
    n

    storeResults :: Updates -> ModGuts -> CoreM ModGuts
    storeResults :: Updates -> CorePluginPass
    storeResults = (ModGuts -> Updates -> CoreM ModGuts) -> Updates -> CorePluginPass
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip ((ModGuts -> (Name, Result) -> CoreM ModGuts)
    -> ModGuts -> Updates -> CoreM ModGuts
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM (((Name, Result) -> CorePluginPass)
    -> ModGuts -> (Name, Result) -> CoreM ModGuts
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip ((Name -> Result -> CorePluginPass)
    -> (Name, Result) -> CorePluginPass
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Name -> Result -> CorePluginPass
    go)))
      where
        go :: Name -> Result -> ModGuts -> CoreM ModGuts
        go :: Name -> Result -> CorePluginPass
    go Name
    name Result
    res ModGuts
    guts = do
            e <- Result -> CoreM CoreExpr
    resultToExpr Result
    res
            pure $ updateNameInGuts name e guts

    dcExpr :: TH.Name -> CoreM CoreExpr
    dcExpr :: Name -> CoreM CoreExpr
    dcExpr Name
    thn = do
        name <- Name -> CoreM Name
    fromTHName Name
    thn
        dc <- lookupDataCon name
        pure $ Var (dataConWrapId dc)

    resultToExpr :: Result -> CoreM CoreExpr
    resultToExpr :: Result -> CoreM CoreExpr
    resultToExpr (Success String
    s) = CoreExpr -> CoreExpr -> CoreExpr
    forall b. Expr b -> Expr b -> Expr b
    App (CoreExpr -> CoreExpr -> CoreExpr)
    -> CoreM CoreExpr -> CoreM (CoreExpr -> CoreExpr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Name -> CoreM CoreExpr
    dcExpr 'Success CoreM (CoreExpr -> CoreExpr) -> CoreM CoreExpr -> CoreM CoreExpr
    forall a b. CoreM (a -> b) -> CoreM a -> CoreM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> String -> CoreM CoreExpr
    forall (m :: * -> *). MonadThings m => String -> m CoreExpr
    mkStringExpr String
    s
    resultToExpr (Failure String
    s) = CoreExpr -> CoreExpr -> CoreExpr
    forall b. Expr b -> Expr b -> Expr b
    App (CoreExpr -> CoreExpr -> CoreExpr)
    -> CoreM CoreExpr -> CoreM (CoreExpr -> CoreExpr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Name -> CoreM CoreExpr
    dcExpr 'Failure CoreM (CoreExpr -> CoreExpr) -> CoreM CoreExpr -> CoreM CoreExpr
    forall a b. CoreM (a -> b) -> CoreM a -> CoreM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> String -> CoreM CoreExpr
    forall (m :: * -> *). MonadThings m => String -> m CoreExpr
    mkStringExpr String
    s

    proofPass :: UponFailure -> ReportingMode -> ModGuts -> CoreM ModGuts
    proofPass :: UponFailure -> ReportingMode -> CorePluginPass
    proofPass UponFailure
    upon_failure ReportingMode
    report ModGuts
    guts = do
        case UponFailure
    upon_failure of
            UponFailure
    SkipO0 -> CorePluginPass
    forall a. a -> CoreM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ModGuts
    guts
            UponFailure
    _ -> do
                let (ModGuts
    guts', [(ResultTarget, Obligation)]
    obligations) = ModGuts -> (ModGuts, [(ResultTarget, Obligation)])
    extractObligations ModGuts
    guts
                (toStore, stats) <- ([Updates] -> Updates
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([Updates] -> Updates)
    -> ([Stats] -> Stats) -> ([Updates], [Stats]) -> (Updates, Stats)
    forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
    forall (p :: * -> * -> *) a b c d.
    Bifunctor p =>
    (a -> b) -> (c -> d) -> p a c -> p b d
    `bimap` (Int -> Int -> Int) -> [Stats] -> Stats
    forall (f :: * -> *) k a.
    (Foldable f, Ord k) =>
    (a -> a -> a) -> f (Map k a) -> Map k a
    M.unionsWith Int -> Int -> Int
    forall a. Num a => a -> a -> a
    (+)) (([Updates], [Stats]) -> (Updates, Stats))
    -> ([(Updates, Stats)] -> ([Updates], [Stats]))
    -> [(Updates, Stats)]
    -> (Updates, Stats)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [(Updates, Stats)] -> ([Updates], [Stats])
    forall a b. [(a, b)] -> ([a], [b])
    unzip ([(Updates, Stats)] -> (Updates, Stats))
    -> CoreM [(Updates, Stats)] -> CoreM (Updates, Stats)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
                    ((ResultTarget, Obligation) -> CoreM (Updates, Stats))
    -> [(ResultTarget, Obligation)] -> CoreM [(Updates, Stats)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (ReportingMode
    -> ModGuts -> (ResultTarget, Obligation) -> CoreM (Updates, Stats)
    checkObligation ReportingMode
    report ModGuts
    guts') [(ResultTarget, Obligation)]
    obligations
                let n = Stats -> Int
    forall a. Num a => Map Stat a -> a
    forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
    sum Stats
    stats :: Int

                guts'' <- storeResults toStore  guts'

                let q :: Stat -> Int
                    q Stat
    s = Int -> Maybe Int -> Int
    forall a. a -> Maybe a -> a
    fromMaybe Int
    0 (Maybe Int -> Int) -> Maybe Int -> Int
    forall a b. (a -> b) -> a -> b
    $ Stat -> Stats -> Maybe Int
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup Stat
    s Stats
    stats

                let summary_message = Int -> SDoc -> SDoc
    nest Int
    2 (SDoc -> SDoc) -> SDoc -> SDoc
    forall a b. (a -> b) -> a -> b
    $
                        [SDoc] -> SDoc
    forall doc. IsDoc doc => [doc] -> doc
    vcat [ Int -> SDoc -> SDoc
    nest Int
    2 (Stat -> SDoc
    desc Stat
    s) SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    Outputable.<> SDoc
    forall doc. IsLine doc => doc
    colon SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Int -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (Stat -> Int
    q Stat
    s)
                             | Stat
    s <- [Stat
    forall a. Bounded a => a
    minBound..Stat
    forall a. Bounded a => a
    maxBound], Stat -> Int
    q Stat
    s Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0 ]

                -- Only print a message if there are some compile-time results to report
                unless (q StoredResult == n) $ do
                    if q ExpSuccess + q ExpFailure + q StoredResult == n
                    then unless (report == Quiet) $
                            putMsg $ text "inspection testing successful" $$ summary_message
                    else do
                        errorMsg $ text "inspection testing unsuccessful" $$ summary_message
                        case upon_failure of
                            UponFailure
    KeepGoing           -> () -> CoreM ()
    forall a. a -> CoreM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                            UponFailure
    _                   -> IO () -> CoreM ()
    forall a. IO a -> CoreM a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> CoreM ()) -> IO () -> CoreM ()
    forall a b. (a -> b) -> a -> b
    $ IO ()
    forall a. IO a
    exitFailure -- kill the compiler. Is there a nicer way?

                return guts''

    desc :: Stat -> SDoc
    desc :: Stat -> SDoc
    desc Stat
    ExpSuccess   = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "  expected successes"
    desc Stat
    UnexpSuccess = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "unexpected successes"
    desc Stat
    ExpFailure   = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "   expected failures"
    desc Stat
    UnexpFailure = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    " unexpected failures"
    desc Stat
    StoredResult = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "      results stored"

    partitionMaybe :: (a -> Maybe b) -> [a] -> ([a], [b])
    partitionMaybe :: forall a b. (a -> Maybe b) -> [a] -> ([a], [b])
    partitionMaybe a -> Maybe b
    f = [Either a b] -> ([a], [b])
    forall a b. [Either a b] -> ([a], [b])
    partitionEithers ([Either a b] -> ([a], [b]))
    -> ([a] -> [Either a b]) -> [a] -> ([a], [b])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> Either a b) -> [a] -> [Either a b]
    forall a b. (a -> b) -> [a] -> [b]
    map (\a
    x -> Either a b -> (b -> Either a b) -> Maybe b -> Either a b
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe (a -> Either a b
    forall a b. a -> Either a b
    Left a
    x) b -> Either a b
    forall a b. b -> Either a b
    Right (a -> Maybe b
    f a
    x))

    -- | like prettySrcLoc, but omits the module name
    myPrettySrcLoc :: TH.Loc -> String
    myPrettySrcLoc :: Loc -> String
    myPrettySrcLoc TH.Loc {String
    CharPos
    loc_filename :: String
    loc_package :: String
    loc_module :: String
    loc_start :: CharPos
    loc_end :: CharPos
    loc_end :: Loc -> CharPos
    loc_start :: Loc -> CharPos
    loc_module :: Loc -> String
    loc_package :: Loc -> String
    loc_filename :: Loc -> String
    ..}
      = (String -> String -> String) -> String -> [String] -> String
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr String -> String -> String
    forall a. [a] -> [a] -> [a]
    (++) String
    ""
          [ String
    loc_filename, String
    ":"
          , Int -> String
    forall a. Show a => a -> String
    show (CharPos -> Int
    forall a b. (a, b) -> a
    fst CharPos
    loc_start), String
    ":"
          , Int -> String
    forall a. Show a => a -> String
    show (CharPos -> Int
    forall a b. (a, b) -> b
    snd CharPos
    loc_start)
          ]