    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE PolyKinds #-}

    -- | Interface for compiler backend writers.
    module Agda.Compiler.Backend
      ( Backend(..), Backend'(..), Recompile(..), IsMain(..)
      , Flag
      , toTreeless
      , module Agda.Syntax.Treeless
      , module Agda.TypeChecking.Monad
      , module CheckResult
      , activeBackendMayEraseType
        -- For Agda.Main
      , backendInteraction
      , parseBackendOptions
        -- For InteractionTop
      , callBackend
        -- Tools
      , lookupBackend
      , activeBackend
      ) where

    import Control.DeepSeq
    import Control.Monad              ( (<=<) )
    import Control.Monad.Trans        ( lift )
    import Control.Monad.Trans.Maybe

    import qualified Data.List as List
    import Data.Maybe

    import Data.Map (Map)
    import qualified Data.Map as Map

    import GHC.Generics (Generic)

    import System.Console.GetOpt

    import Agda.Syntax.Treeless
    import Agda.TypeChecking.Errors (getAllWarnings)
    -- Agda.TypeChecking.Monad.Base imports us, relying on the .hs-boot file to
    -- resolve the circular dependency. Fine. However, ghci loads the module after
    -- compilation, so it brings in all of the symbols. That causes .Base to see
    -- getBenchmark (defined in Agda.TypeChecking.Monad.State) *and* the one
    -- defined in Agda.Utils.Benchmark, which causes an error. So we explicitly
    -- hide it here to prevent it from being seen there and causing an error.
    import Agda.TypeChecking.Monad hiding (getBenchmark)
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Pretty as P

    import Agda.Interaction.Options
    import Agda.Interaction.FindFile
    import Agda.Interaction.Imports as CheckResult (CheckResult(CheckResult), crInterface, crWarnings, crMode)
    import Agda.TypeChecking.Warnings

    import Agda.Utils.FileName
    import Agda.Utils.Functor
    import Agda.Utils.IndexedList
    import Agda.Utils.Lens
    import Agda.Utils.Monad

    import Agda.Compiler.ToTreeless
    import Agda.Compiler.Common

    import Agda.Utils.Impossible

    -- Public interface -------------------------------------------------------

    data Backend where
      Backend :: NFData opts => Backend' opts env menv mod def -> Backend

    data Backend' opts env menv mod def = Backend'
      { forall opts env menv mod def.
    Backend' opts env menv mod def -> [Char]
    backendName      :: String
      , forall opts env menv mod def.
    Backend' opts env menv mod def -> Maybe [Char]
    backendVersion   :: Maybe String
          -- ^ Optional version information to be printed with @--version@.
      , forall opts env menv mod def.
    Backend' opts env menv mod def -> opts
    options          :: opts
          -- ^ Default options
      , forall opts env menv mod def.
    Backend' opts env menv mod def -> [OptDescr (Flag opts)]
    commandLineFlags :: [OptDescr (Flag opts)]
          -- ^ Backend-specific command-line flags. Should at minimum contain a
          --   flag to enable the backend.
      , forall opts env menv mod def.
    Backend' opts env menv mod def -> opts -> Bool
    isEnabled        :: opts -> Bool
          -- ^ Unless the backend has been enabled, @runAgda@ will fall back to
          --   vanilla Agda behaviour.
      , forall opts env menv mod def.
    Backend' opts env menv mod def -> opts -> TCM env
    preCompile       :: opts -> TCM env
          -- ^ Called after type checking completes, but before compilation starts.
      , forall opts env menv mod def.
    Backend' opts env menv mod def
    -> env -> IsMain -> Map ModuleName mod -> TCM ()
    postCompile      :: env -> IsMain -> Map ModuleName mod -> TCM ()
          -- ^ Called after module compilation has completed. The @IsMain@ argument
          --   is @NotMain@ if the @--no-main@ flag is present.
      , forall opts env menv mod def.
    Backend' opts env menv mod def
    -> env
    -> IsMain
    -> ModuleName
    -> Maybe [Char]
    -> TCM (Recompile menv mod)
    preModule        :: env -> IsMain -> ModuleName -> Maybe FilePath -> TCM (Recompile menv mod)
          -- ^ Called before compilation of each module. Gets the path to the
          --   @.agdai@ file to allow up-to-date checking of previously written
          --   compilation results. Should return @Skip m@ if compilation is not
          --   required. Will be @Nothing@ if only scope checking.
      , forall opts env menv mod def.
    Backend' opts env menv mod def
    -> env -> menv -> IsMain -> ModuleName -> [def] -> TCM mod
    postModule       :: env -> menv -> IsMain -> ModuleName -> [def] -> TCM mod
          -- ^ Called after all definitions of a module have been compiled.
      , forall opts env menv mod def.
    Backend' opts env menv mod def
    -> env -> menv -> IsMain -> Definition -> TCM def
    compileDef       :: env -> menv -> IsMain -> Definition -> TCM def
          -- ^ Compile a single definition.
      , forall opts env menv mod def.
    Backend' opts env menv mod def -> Bool
    scopeCheckingSuffices :: Bool
          -- ^ True if the backend works if @--only-scope-checking@ is used.
      , forall opts env menv mod def.
    Backend' opts env menv mod def -> QName -> TCM Bool
    mayEraseType     :: QName -> TCM Bool
          -- ^ The treeless compiler may ask the Backend if elements
          --   of the given type maybe possibly erased.
          --   The answer should be 'False' if the compilation of the type
          --   is used by a third party, e.g. in a FFI binding.
      }
      deriving (forall x.
     Backend' opts env menv mod def
     -> Rep (Backend' opts env menv mod def) x)
    -> (forall x.
        Rep (Backend' opts env menv mod def) x
        -> Backend' opts env menv mod def)
    -> Generic (Backend' opts env menv mod def)
    forall x.
    Rep (Backend' opts env menv mod def) x
    -> Backend' opts env menv mod def
    forall x.
    Backend' opts env menv mod def
    -> Rep (Backend' opts env menv mod def) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    forall opts env menv mod def x.
    Rep (Backend' opts env menv mod def) x
    -> Backend' opts env menv mod def
    forall opts env menv mod def x.
    Backend' opts env menv mod def
    -> Rep (Backend' opts env menv mod def) x
    $cto :: forall opts env menv mod def x.
    Rep (Backend' opts env menv mod def) x
    -> Backend' opts env menv mod def
    $cfrom :: forall opts env menv mod def x.
    Backend' opts env menv mod def
    -> Rep (Backend' opts env menv mod def) x
    Generic

    data Recompile menv mod = Recompile menv | Skip mod

    -- | Call the 'compilerMain' function of the given backend.

    callBackend :: String -> IsMain -> CheckResult -> TCM ()
    callBackend :: [Char] -> IsMain -> CheckResult -> TCM ()
    callBackend [Char]
    name IsMain
    iMain CheckResult
    checkResult = [Char] -> TCM (Maybe Backend)
    lookupBackend [Char]
    name TCM (Maybe Backend) -> (Maybe Backend -> TCM ()) -> TCM ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
      Just (Backend Backend' opts env menv mod def
    b) -> Backend' opts env menv mod def -> IsMain -> CheckResult -> TCM ()
    forall opts env menv mod def.
    Backend' opts env menv mod def -> IsMain -> CheckResult -> TCM ()
    compilerMain Backend' opts env menv mod def
    b IsMain
    iMain CheckResult
    checkResult
      Maybe Backend
    Nothing -> do
        [Backend]
    backends <- Lens' [Backend] TCState -> TCMT IO [Backend]
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' [Backend] TCState
    stBackends
        [Char] -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    [Char] -> m a
    genericError ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          [Char]
    "No backend called '" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    name [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "' " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++
          [Char]
    "(installed backends: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++
          [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    List.intercalate [Char]
    ", "
            ([[Char]] -> [[Char]]
    forall a. Ord a => [a] -> [a]
    List.sort ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
    forall a b. (a -> b) -> a -> b
    $ [[Char]]
    otherBackends [[Char]] -> [[Char]] -> [[Char]]
    forall a. [a] -> [a] -> [a]
    ++
                         [ Backend' opts env menv mod def -> [Char]
    forall opts env menv mod def.
    Backend' opts env menv mod def -> [Char]
    backendName Backend' opts env menv mod def
    b | Backend Backend' opts env menv mod def
    b <- [Backend]
    backends ]) [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++
          [Char]
    ")"

    -- | Backends that are not included in the state, but still available
    --   to the user.

    otherBackends :: [String]
    otherBackends :: [[Char]]
    otherBackends = [[Char]
    "GHCNoMain", [Char]
    "QuickLaTeX"]

    -- | Look for a backend of the given name.

    lookupBackend :: BackendName -> TCM (Maybe Backend)
    lookupBackend :: [Char] -> TCM (Maybe Backend)
    lookupBackend [Char]
    name = Lens' [Backend] TCState -> TCMT IO [Backend]
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' [Backend] TCState
    stBackends TCMT IO [Backend]
    -> ([Backend] -> Maybe Backend) -> TCM (Maybe Backend)
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ [Backend]
    backends ->
      [Backend] -> Maybe Backend
    forall a. [a] -> Maybe a
    listToMaybe [ Backend
    b | b :: Backend
    b@(Backend Backend' opts env menv mod def
    b') <- [Backend]
    backends, Backend' opts env menv mod def -> [Char]
    forall opts env menv mod def.
    Backend' opts env menv mod def -> [Char]
    backendName Backend' opts env menv mod def
    b' [Char] -> [Char] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Char]
    name ]

    -- | Get the currently active backend (if any).

    activeBackend :: TCM (Maybe Backend)
    activeBackend :: TCM (Maybe Backend)
    activeBackend = MaybeT (TCMT IO) Backend -> TCM (Maybe Backend)
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT (MaybeT (TCMT IO) Backend -> TCM (Maybe Backend))
    -> MaybeT (TCMT IO) Backend -> TCM (Maybe Backend)
    forall a b. (a -> b) -> a -> b
    $ do
      [Char]
    bname <- TCMT IO (Maybe [Char]) -> MaybeT (TCMT IO) [Char]
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (TCMT IO (Maybe [Char]) -> MaybeT (TCMT IO) [Char])
    -> TCMT IO (Maybe [Char]) -> MaybeT (TCMT IO) [Char]
    forall a b. (a -> b) -> a -> b
    $ (TCEnv -> Maybe [Char]) -> TCMT IO (Maybe [Char])
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Maybe [Char]
    envActiveBackendName
      TCMT IO Backend -> MaybeT (TCMT IO) Backend
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO Backend -> MaybeT (TCMT IO) Backend)
    -> TCMT IO Backend -> MaybeT (TCMT IO) Backend
    forall a b. (a -> b) -> a -> b
    $ Backend -> Maybe Backend -> Backend
    forall a. a -> Maybe a -> a
    fromMaybe Backend
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Backend -> Backend)
    -> TCM (Maybe Backend) -> TCMT IO Backend
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Char] -> TCM (Maybe Backend)
    lookupBackend [Char]
    bname

    -- | Ask the active backend whether a type may be erased.
    --   See issue #3732.

    activeBackendMayEraseType :: QName -> TCM Bool
    activeBackendMayEraseType :: QName -> TCM Bool
    activeBackendMayEraseType QName
    q = do
      Backend Backend' opts env menv mod def
    b <- Backend -> Maybe Backend -> Backend
    forall a. a -> Maybe a -> a
    fromMaybe Backend
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Backend -> Backend)
    -> TCM (Maybe Backend) -> TCMT IO Backend
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCM (Maybe Backend)
    activeBackend
      Backend' opts env menv mod def -> QName -> TCM Bool
    forall opts env menv mod def.
    Backend' opts env menv mod def -> QName -> TCM Bool
    mayEraseType Backend' opts env menv mod def
    b QName
    q

    instance NFData Backend where
      rnf :: Backend -> ()
    rnf (Backend Backend' opts env menv mod def
    b) = Backend' opts env menv mod def -> ()
    forall a. NFData a => a -> ()
    rnf Backend' opts env menv mod def
    b

    instance NFData opts => NFData (Backend' opts env menv mod def) where
      rnf :: Backend' opts env menv mod def -> ()
    rnf (Backend' [Char]
    a Maybe [Char]
    b opts
    c [OptDescr (Flag opts)]
    d opts -> Bool
    e opts -> TCM env
    f env -> IsMain -> Map ModuleName mod -> TCM ()
    g env
    -> IsMain -> ModuleName -> Maybe [Char] -> TCM (Recompile menv mod)
    h env -> menv -> IsMain -> ModuleName -> [def] -> TCM mod
    i env -> menv -> IsMain -> Definition -> TCM def
    j Bool
    k QName -> TCM Bool
    l) =
        [Char] -> ()
    forall a. NFData a => a -> ()
    rnf [Char]
    a () -> () -> ()
    `seq` Maybe [Char] -> ()
    forall a. NFData a => a -> ()
    rnf Maybe [Char]
    b () -> () -> ()
    `seq` opts -> ()
    forall a. NFData a => a -> ()
    rnf opts
    c () -> () -> ()
    `seq` [OptDescr (Flag opts)] -> ()
    forall {a}. NFData a => [OptDescr a] -> ()
    rnf' [OptDescr (Flag opts)]
    d () -> () -> ()
    `seq` (opts -> Bool) -> ()
    forall a. NFData a => a -> ()
    rnf opts -> Bool
    e () -> () -> ()
    `seq`
        (opts -> TCM env) -> ()
    forall a. NFData a => a -> ()
    rnf opts -> TCM env
    f () -> () -> ()
    `seq` (env -> IsMain -> Map ModuleName mod -> TCM ()) -> ()
    forall a. NFData a => a -> ()
    rnf env -> IsMain -> Map ModuleName mod -> TCM ()
    g () -> () -> ()
    `seq` (env
     -> IsMain
     -> ModuleName
     -> Maybe [Char]
     -> TCM (Recompile menv mod))
    -> ()
    forall a. NFData a => a -> ()
    rnf env
    -> IsMain -> ModuleName -> Maybe [Char] -> TCM (Recompile menv mod)
    h () -> () -> ()
    `seq` (env -> menv -> IsMain -> ModuleName -> [def] -> TCM mod) -> ()
    forall a. NFData a => a -> ()
    rnf env -> menv -> IsMain -> ModuleName -> [def] -> TCM mod
    i () -> () -> ()
    `seq` (env -> menv -> IsMain -> Definition -> TCM def) -> ()
    forall a. NFData a => a -> ()
    rnf env -> menv -> IsMain -> Definition -> TCM def
    j () -> () -> ()
    `seq`
        Bool -> ()
    forall a. NFData a => a -> ()
    rnf Bool
    k () -> () -> ()
    `seq` (QName -> TCM Bool) -> ()
    forall a. NFData a => a -> ()
    rnf QName -> TCM Bool
    l
        where
        rnf' :: [OptDescr a] -> ()
    rnf' []                   = ()
        rnf' (Option [Char]
    a [[Char]]
    b ArgDescr a
    c [Char]
    d : [OptDescr a]
    e) =
          [Char] -> ()
    forall a. NFData a => a -> ()
    rnf [Char]
    a () -> () -> ()
    `seq` [[Char]] -> ()
    forall a. NFData a => a -> ()
    rnf [[Char]]
    b () -> () -> ()
    `seq` ArgDescr a -> ()
    forall {a}. NFData a => ArgDescr a -> ()
    rnf'' ArgDescr a
    c () -> () -> ()
    `seq` [Char] -> ()
    forall a. NFData a => a -> ()
    rnf [Char]
    d () -> () -> ()
    `seq` [OptDescr a] -> ()
    rnf' [OptDescr a]
    e

        rnf'' :: ArgDescr a -> ()
    rnf'' (NoArg a
    a)    = a -> ()
    forall a. NFData a => a -> ()
    rnf a
    a
        rnf'' (ReqArg [Char] -> a
    a [Char]
    b) = ([Char] -> a) -> ()
    forall a. NFData a => a -> ()
    rnf [Char] -> a
    a () -> () -> ()
    `seq` [Char] -> ()
    forall a. NFData a => a -> ()
    rnf [Char]
    b
        rnf'' (OptArg Maybe [Char] -> a
    a [Char]
    b) = (Maybe [Char] -> a) -> ()
    forall a. NFData a => a -> ()
    rnf Maybe [Char] -> a
    a () -> () -> ()
    `seq` [Char] -> ()
    forall a. NFData a => a -> ()
    rnf [Char]
    b

    -- Internals --------------------------------------------------------------

    data BackendWithOpts opts where
      BackendWithOpts ::
        NFData opts =>
        Backend' opts env menv mod def ->
        BackendWithOpts opts

    backendWithOpts :: Backend -> Some BackendWithOpts
    backendWithOpts :: Backend -> Some BackendWithOpts
    backendWithOpts (Backend Backend' opts env menv mod def
    backend) = BackendWithOpts opts -> Some BackendWithOpts
    forall {k} (f :: k -> *) (opts :: k). f opts -> Some f
    Some (Backend' opts env menv mod def -> BackendWithOpts opts
    forall opts opts env menv mod.
    NFData opts =>
    Backend' opts opts env menv mod -> BackendWithOpts opts
    BackendWithOpts Backend' opts env menv mod def
    backend)

    forgetOpts :: BackendWithOpts opts -> Backend
    forgetOpts :: forall opts. BackendWithOpts opts -> Backend
    forgetOpts (BackendWithOpts Backend' opts env menv mod def
    backend) = Backend' opts env menv mod def -> Backend
    forall opts env menv mod def.
    NFData opts =>
    Backend' opts env menv mod def -> Backend
    Backend Backend' opts env menv mod def
    backend

    bOptions :: Lens' opts (BackendWithOpts opts)
    bOptions :: forall opts. Lens' opts (BackendWithOpts opts)
    bOptions opts -> f opts
    f (BackendWithOpts Backend' opts env menv mod def
    b) = opts -> f opts
    f (Backend' opts env menv mod def -> opts
    forall opts env menv mod def.
    Backend' opts env menv mod def -> opts
    options Backend' opts env menv mod def
    b) f opts
    -> (opts -> BackendWithOpts opts) -> f (BackendWithOpts opts)
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ opts
    opts -> Backend' opts env menv mod def -> BackendWithOpts opts
    forall opts opts env menv mod.
    NFData opts =>
    Backend' opts opts env menv mod -> BackendWithOpts opts
    BackendWithOpts Backend' opts env menv mod def
    b{ options :: opts
    options = opts
    opts }

    embedFlag :: Lens' a b -> Flag a -> Flag b
    embedFlag :: forall a b. Lens' a b -> Flag a -> Flag b
    embedFlag Lens' a b
    l Flag a
    flag = Flag a -> b -> ExceptT [Char] Identity b
    Lens' a b
    l Flag a
    flag

    embedOpt :: Lens' a b -> OptDescr (Flag a) -> OptDescr (Flag b)
    embedOpt :: forall a b. Lens' a b -> OptDescr (Flag a) -> OptDescr (Flag b)
    embedOpt Lens' a b
    l = (Flag a -> Flag b) -> OptDescr (Flag a) -> OptDescr (Flag b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Lens' a b -> Flag a -> Flag b
    forall a b. Lens' a b -> Flag a -> Flag b
    embedFlag Lens' a b
    l)

    parseBackendOptions :: [Backend] -> [String] -> CommandLineOptions -> OptM ([Backend], CommandLineOptions)
    parseBackendOptions :: [Backend]
    -> [[Char]]
    -> CommandLineOptions
    -> OptM ([Backend], CommandLineOptions)
    parseBackendOptions [Backend]
    backends [[Char]]
    argv CommandLineOptions
    opts0 =
      case (Backend -> Some BackendWithOpts)
    -> [Backend] -> Some (All BackendWithOpts)
    forall {x} a (b :: x -> *). (a -> Some b) -> [a] -> Some (All b)
    makeAll Backend -> Some BackendWithOpts
    backendWithOpts [Backend]
    backends of
        Some All BackendWithOpts i
    bs -> do
          let agdaFlags :: [OptDescr (Flag (a, CommandLineOptions))]
    agdaFlags    = (OptDescr (Flag CommandLineOptions)
     -> OptDescr (Flag (a, CommandLineOptions)))
    -> [OptDescr (Flag CommandLineOptions)]
    -> [OptDescr (Flag (a, CommandLineOptions))]
    forall a b. (a -> b) -> [a] -> [b]
    map (Lens' CommandLineOptions (a, CommandLineOptions)
    -> OptDescr (Flag CommandLineOptions)
    -> OptDescr (Flag (a, CommandLineOptions))
    forall a b. Lens' a b -> OptDescr (Flag a) -> OptDescr (Flag b)
    embedOpt forall b a. Lens' b (a, b)
    Lens' CommandLineOptions (a, CommandLineOptions)
    lSnd) ([OptDescr (Flag CommandLineOptions)]
    deadStandardOptions [OptDescr (Flag CommandLineOptions)]
    -> [OptDescr (Flag CommandLineOptions)]
    -> [OptDescr (Flag CommandLineOptions)]
    forall a. [a] -> [a] -> [a]
    ++ [OptDescr (Flag CommandLineOptions)]
    standardOptions)
              backendFlags :: [OptDescr (Flag (All BackendWithOpts i, CommandLineOptions))]
    backendFlags = do
                Some Index i i
    i            <- (forall x1. Index i x1 -> Some (Index i))
    -> All (Index i) i -> [Some (Index i)]
    forall {x} (b :: x -> *) a (xs :: [x]).
    (forall (x1 :: x). b x1 -> a) -> All b xs -> [a]
    forgetAll forall x1. Index i x1 -> Some (Index i)
    forall {k} (f :: k -> *) (opts :: k). f opts -> Some f
    Some (All (Index i) i -> [Some (Index i)])
    -> All (Index i) i -> [Some (Index i)]
    forall a b. (a -> b) -> a -> b
    $ All BackendWithOpts i -> All (Index i) i
    forall {x} (p :: x -> *) (xs :: [x]). All p xs -> All (Index xs) xs
    allIndices All BackendWithOpts i
    bs
                BackendWithOpts Backend' i env menv mod def
    b <- [All BackendWithOpts i -> Index i i -> BackendWithOpts i
    forall {x1} (p :: x1 -> *) (xs :: [x1]) (x2 :: x1).
    All p xs -> Index xs x2 -> p x2
    lookupIndex All BackendWithOpts i
    bs Index i i
    i]
                OptDescr (Flag i)
    opt               <- Backend' i env menv mod def -> [OptDescr (Flag i)]
    forall opts env menv mod def.
    Backend' opts env menv mod def -> [OptDescr (Flag opts)]
    commandLineFlags Backend' i env menv mod def
    b
                OptDescr (Flag (All BackendWithOpts i, CommandLineOptions))
    -> [OptDescr (Flag (All BackendWithOpts i, CommandLineOptions))]
    forall (m :: * -> *) a. Monad m => a -> m a
    return (OptDescr (Flag (All BackendWithOpts i, CommandLineOptions))
     -> [OptDescr (Flag (All BackendWithOpts i, CommandLineOptions))])
    -> OptDescr (Flag (All BackendWithOpts i, CommandLineOptions))
    -> [OptDescr (Flag (All BackendWithOpts i, CommandLineOptions))]
    forall a b. (a -> b) -> a -> b
    $ Lens' i (All BackendWithOpts i, CommandLineOptions)
    -> OptDescr (Flag i)
    -> OptDescr (Flag (All BackendWithOpts i, CommandLineOptions))
    forall a b. Lens' a b -> OptDescr (Flag a) -> OptDescr (Flag b)
    embedOpt ((All BackendWithOpts i -> f (All BackendWithOpts i))
    -> (All BackendWithOpts i, CommandLineOptions)
    -> f (All BackendWithOpts i, CommandLineOptions)
    forall a b. Lens' a (a, b)
    lFst ((All BackendWithOpts i -> f (All BackendWithOpts i))
     -> (All BackendWithOpts i, CommandLineOptions)
     -> f (All BackendWithOpts i, CommandLineOptions))
    -> ((i -> f i)
        -> All BackendWithOpts i -> f (All BackendWithOpts i))
    -> (i -> f i)
    -> (All BackendWithOpts i, CommandLineOptions)
    -> f (All BackendWithOpts i, CommandLineOptions)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Index i i -> Lens' (BackendWithOpts i) (All BackendWithOpts i)
    forall {x1} (xs :: [x1]) (x2 :: x1) (p :: x1 -> *).
    Index xs x2 -> Lens' (p x2) (All p xs)
    lIndex Index i i
    i ((BackendWithOpts i -> f (BackendWithOpts i))
     -> All BackendWithOpts i -> f (All BackendWithOpts i))
    -> ((i -> f i) -> BackendWithOpts i -> f (BackendWithOpts i))
    -> (i -> f i)
    -> All BackendWithOpts i
    -> f (All BackendWithOpts i)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (i -> f i) -> BackendWithOpts i -> f (BackendWithOpts i)
    forall opts. Lens' opts (BackendWithOpts opts)
    bOptions) OptDescr (Flag i)
    opt
          (All BackendWithOpts i
    backends, CommandLineOptions
    opts) <- [[Char]]
    -> [OptDescr (Flag (All BackendWithOpts i, CommandLineOptions))]
    -> ([Char] -> Flag (All BackendWithOpts i, CommandLineOptions))
    -> Flag (All BackendWithOpts i, CommandLineOptions)
    forall opts.
    [[Char]]
    -> [OptDescr (Flag opts)] -> ([Char] -> Flag opts) -> Flag opts
    getOptSimple ([[Char]] -> [[Char]]
    stripRTS [[Char]]
    argv)
                                           ([OptDescr (Flag (All BackendWithOpts i, CommandLineOptions))]
    forall {a}. [OptDescr (Flag (a, CommandLineOptions))]
    agdaFlags [OptDescr (Flag (All BackendWithOpts i, CommandLineOptions))]
    -> [OptDescr (Flag (All BackendWithOpts i, CommandLineOptions))]
    -> [OptDescr (Flag (All BackendWithOpts i, CommandLineOptions))]
    forall a. [a] -> [a] -> [a]
    ++ [OptDescr (Flag (All BackendWithOpts i, CommandLineOptions))]
    backendFlags) (Lens'
      CommandLineOptions (All BackendWithOpts i, CommandLineOptions)
    -> Flag CommandLineOptions
    -> Flag (All BackendWithOpts i, CommandLineOptions)
    forall a b. Lens' a b -> Flag a -> Flag b
    embedFlag forall b a. Lens' b (a, b)
    Lens'
      CommandLineOptions (All BackendWithOpts i, CommandLineOptions)
    lSnd (Flag CommandLineOptions
     -> Flag (All BackendWithOpts i, CommandLineOptions))
    -> ([Char] -> Flag CommandLineOptions)
    -> [Char]
    -> Flag (All BackendWithOpts i, CommandLineOptions)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> Flag CommandLineOptions
    inputFlag)
                                           (All BackendWithOpts i
    bs, CommandLineOptions
    opts0)
          CommandLineOptions
    opts <- Flag CommandLineOptions
    checkOpts CommandLineOptions
    opts
          ([Backend], CommandLineOptions)
    -> OptM ([Backend], CommandLineOptions)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((forall opts. BackendWithOpts opts -> Backend)
    -> All BackendWithOpts i -> [Backend]
    forall {x} (b :: x -> *) a (xs :: [x]).
    (forall (x1 :: x). b x1 -> a) -> All b xs -> [a]
    forgetAll forall opts. BackendWithOpts opts -> Backend
    forgetOpts All BackendWithOpts i
    backends, CommandLineOptions
    opts)

    backendInteraction :: AbsolutePath -> [Backend] -> TCM () -> (AbsolutePath -> TCM CheckResult) -> TCM ()
    backendInteraction :: AbsolutePath
    -> [Backend]
    -> TCM ()
    -> (AbsolutePath -> TCM CheckResult)
    -> TCM ()
    backendInteraction AbsolutePath
    mainFile [Backend]
    backends TCM ()
    setup AbsolutePath -> TCM CheckResult
    check = do
      TCM ()
    setup
      CheckResult
    checkResult <- AbsolutePath -> TCM CheckResult
    check AbsolutePath
    mainFile

      -- reset warnings
      Lens' [TCWarning] TCState
    stTCWarnings Lens' [TCWarning] TCState -> [TCWarning] -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    `setTCLens` []

      Bool
    noMain <- PragmaOptions -> Bool
    optCompileNoMain (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions
      let isMain :: IsMain
    isMain | Bool
    noMain    = IsMain
    NotMain
                 | Bool
    otherwise = IsMain
    IsMain

      TCM Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM (PragmaOptions -> Bool
    optAllowUnsolved (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        let ws :: [TCWarning]
    ws = CheckResult -> [TCWarning]
    crWarnings CheckResult
    checkResult
            mode :: ModuleCheckMode
    mode = CheckResult -> ModuleCheckMode
    crMode CheckResult
    checkResult
        -- Possible warnings, but only scope checking: ok.
        -- (Compatibility with scope checking done during options validation).
        Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (ModuleCheckMode
    mode ModuleCheckMode -> ModuleCheckMode -> Bool
    forall a. Eq a => a -> a -> Bool
    == ModuleCheckMode
    ModuleScopeChecked Bool -> Bool -> Bool
    || [TCWarning] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [TCWarning]
    ws) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          [Char] -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    [Char] -> m a
    genericError ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "You can only compile modules without unsolved metavariables."

      [TCM ()] -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a.
    (Foldable t, Monad m) =>
    t (m a) -> m ()
    sequence_ [ Backend' opts env menv mod def -> IsMain -> CheckResult -> TCM ()
    forall opts env menv mod def.
    Backend' opts env menv mod def -> IsMain -> CheckResult -> TCM ()
    compilerMain Backend' opts env menv mod def
    backend IsMain
    isMain CheckResult
    checkResult | Backend Backend' opts env menv mod def
    backend <- [Backend]
    backends ]

      -- print warnings that might have accumulated during compilation
      [TCWarning]
    ws <- (TCWarning -> Bool) -> [TCWarning] -> [TCWarning]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Bool -> Bool
    not (Bool -> Bool) -> (TCWarning -> Bool) -> TCWarning -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Warning -> Bool
    isUnsolvedWarning (Warning -> Bool) -> (TCWarning -> Warning) -> TCWarning -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCWarning -> Warning
    tcWarning) ([TCWarning] -> [TCWarning])
    -> TCMT IO [TCWarning] -> TCMT IO [TCWarning]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> WhichWarnings -> TCMT IO [TCWarning]
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m, MonadWarning m) =>
    WhichWarnings -> m [TCWarning]
    getAllWarnings WhichWarnings
    AllWarnings
      Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([TCWarning] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [TCWarning]
    ws) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> VerboseLevel -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "warning" VerboseLevel
    1 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    P.vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCWarning -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    P.prettyTCM (TCWarning -> TCMT IO Doc) -> [TCWarning] -> [TCMT IO Doc]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [TCWarning]
    ws

    compilerMain :: Backend' opts env menv mod def -> IsMain -> CheckResult -> TCM ()
    compilerMain :: forall opts env menv mod def.
    Backend' opts env menv mod def -> IsMain -> CheckResult -> TCM ()
    compilerMain Backend' opts env menv mod def
    backend IsMain
    isMain0 CheckResult
    checkResult = CheckResult -> TCM () -> TCM ()
    forall a. CheckResult -> TCM a -> TCM a
    inCompilerEnv CheckResult
    checkResult (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
      Lens' (Maybe [Char]) TCEnv
    -> (Maybe [Char] -> Maybe [Char]) -> TCM () -> TCM ()
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' a TCEnv -> (a -> a) -> m b -> m b
    locallyTC Lens' (Maybe [Char]) TCEnv
    eActiveBackendName (Maybe [Char] -> Maybe [Char] -> Maybe [Char]
    forall a b. a -> b -> a
    const (Maybe [Char] -> Maybe [Char] -> Maybe [Char])
    -> Maybe [Char] -> Maybe [Char] -> Maybe [Char]
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just ([Char] -> Maybe [Char]) -> [Char] -> Maybe [Char]
    forall a b. (a -> b) -> a -> b
    $ Backend' opts env menv mod def -> [Char]
    forall opts env menv mod def.
    Backend' opts env menv mod def -> [Char]
    backendName Backend' opts env menv mod def
    backend) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        -- BEWARE: Do not use @optOnlyScopeChecking@ here; it does not authoritatively describe the type-checking mode!
        -- InteractionTop currently may invoke type-checking with scope checking regardless of that flag.
        Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Bool -> Bool
    not (Backend' opts env menv mod def -> Bool
    forall opts env menv mod def.
    Backend' opts env menv mod def -> Bool
    scopeCheckingSuffices Backend' opts env menv mod def
    backend) Bool -> Bool -> Bool
    && CheckResult -> ModuleCheckMode
    crMode CheckResult
    checkResult ModuleCheckMode -> ModuleCheckMode -> Bool
    forall a. Eq a => a -> a -> Bool
    == ModuleCheckMode
    ModuleScopeChecked) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          [Char] -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    [Char] -> m a
    genericError ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
            [Char]
    "The --only-scope-checking flag cannot be combined with " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++
            Backend' opts env menv mod def -> [Char]
    forall opts env menv mod def.
    Backend' opts env menv mod def -> [Char]
    backendName Backend' opts env menv mod def
    backend [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "."

        let i :: Interface
    i = CheckResult -> Interface
    crInterface CheckResult
    checkResult
        -- Andreas, 2017-08-23, issue #2714
        -- If the backend is invoked from Emacs, we can only get the --no-main
        -- pragma option now, coming from the interface file.
        IsMain
    isMain <- TCM Bool -> TCMT IO IsMain -> TCMT IO IsMain -> TCMT IO IsMain
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (PragmaOptions -> Bool
    optCompileNoMain (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions)
          {-then-} (IsMain -> TCMT IO IsMain
    forall (m :: * -> *) a. Monad m => a -> m a
    return IsMain
    NotMain)
          {-else-} (IsMain -> TCMT IO IsMain
    forall (m :: * -> *) a. Monad m => a -> m a
    return IsMain
    isMain0)

        env
    env  <- Backend' opts env menv mod def -> opts -> TCM env
    forall opts env menv mod def.
    Backend' opts env menv mod def -> opts -> TCM env
    preCompile Backend' opts env menv mod def
    backend (Backend' opts env menv mod def -> opts
    forall opts env menv mod def.
    Backend' opts env menv mod def -> opts
    options Backend' opts env menv mod def
    backend)
        Map ModuleName mod
    mods <- (IsMain -> Interface -> TCM (Map ModuleName mod))
    -> IsMain -> Interface -> TCM (Map ModuleName mod)
    forall r.
    Monoid r =>
    (IsMain -> Interface -> TCM r) -> IsMain -> Interface -> TCM r
    doCompile
            -- This inner function is called for both `Agda.Primitive` and the module in question,
            -- and all (distinct) imported modules. So avoid shadowing "isMain" or "i".
            (\IsMain
    ifaceIsMain Interface
    iface -> ModuleName -> mod -> Map ModuleName mod
    forall k a. k -> a -> Map k a
    Map.singleton (Interface -> ModuleName
    iModuleName Interface
    iface) (mod -> Map ModuleName mod)
    -> TCMT IO mod -> TCM (Map ModuleName mod)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Backend' opts env menv mod def
    -> env -> IsMain -> Interface -> TCMT IO mod
    forall opts env menv mod def.
    Backend' opts env menv mod def
    -> env -> IsMain -> Interface -> TCM mod
    compileModule Backend' opts env menv mod def
    backend env
    env IsMain
    ifaceIsMain Interface
    iface)
            IsMain
    isMain Interface
    i
        -- Note that `doCompile` calls `setInterface` for each distinct module in the graph prior to calling into
        -- `compileModule`. This last one is just to ensure it's reset to _this_ module.
        Interface -> TCM ()
    setInterface Interface
    i
        Backend' opts env menv mod def
    -> env -> IsMain -> Map ModuleName mod -> TCM ()
    forall opts env menv mod def.
    Backend' opts env menv mod def
    -> env -> IsMain -> Map ModuleName mod -> TCM ()
    postCompile Backend' opts env menv mod def
    backend env
    env IsMain
    isMain Map ModuleName mod
    mods

    compileModule :: Backend' opts env menv mod def -> env -> IsMain -> Interface -> TCM mod
    compileModule :: forall opts env menv mod def.
    Backend' opts env menv mod def
    -> env -> IsMain -> Interface -> TCM mod
    compileModule Backend' opts env menv mod def
    backend env
    env IsMain
    isMain Interface
    i = do
      TopLevelModuleName
    mName <- ModuleName -> TopLevelModuleName
    toTopLevelModuleName (ModuleName -> TopLevelModuleName)
    -> TCMT IO ModuleName -> TCMT IO TopLevelModuleName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO ModuleName
    forall (m :: * -> *). ReadTCState m => m ModuleName
    curMName
      -- The interface file will only exist if performing af full type-check, vs scoping.
      -- FIXME: Expecting backends to read the timestamp of the output path of the interface
      --        file for dirtiness checking is very roundabout and heavily couples backend
      --        implementations to the filesystem as the source of cache state.
      Maybe [Char]
    mifile <- ([Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just ([Char] -> Maybe [Char])
    -> (InterfaceFile -> [Char]) -> InterfaceFile -> Maybe [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbsolutePath -> [Char]
    filePath (AbsolutePath -> [Char])
    -> (InterfaceFile -> AbsolutePath) -> InterfaceFile -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . InterfaceFile -> AbsolutePath
    intFilePath (InterfaceFile -> Maybe [Char])
    -> Maybe InterfaceFile -> Maybe [Char]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<) (Maybe InterfaceFile -> Maybe [Char])
    -> TCMT IO (Maybe InterfaceFile) -> TCMT IO (Maybe [Char])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TopLevelModuleName -> TCMT IO (Maybe InterfaceFile)
    findInterfaceFile TopLevelModuleName
    mName
      Recompile menv mod
    r      <- Backend' opts env menv mod def
    -> env
    -> IsMain
    -> ModuleName
    -> Maybe [Char]
    -> TCM (Recompile menv mod)
    forall opts env menv mod def.
    Backend' opts env menv mod def
    -> env
    -> IsMain
    -> ModuleName
    -> Maybe [Char]
    -> TCM (Recompile menv mod)
    preModule Backend' opts env menv mod def
    backend env
    env IsMain
    isMain (Interface -> ModuleName
    iModuleName Interface
    i) Maybe [Char]
    mifile
      case Recompile menv mod
    r of
        Skip mod
    m         -> mod -> TCM mod
    forall (m :: * -> *) a. Monad m => a -> m a
    return mod
    m
        Recompile menv
    menv -> do
          [Definition]
    defs <- ((QName, Definition) -> Definition)
    -> [(QName, Definition)] -> [Definition]
    forall a b. (a -> b) -> [a] -> [b]
    map (QName, Definition) -> Definition
    forall a b. (a, b) -> b
    snd ([(QName, Definition)] -> [Definition])
    -> (Definitions -> [(QName, Definition)])
    -> Definitions
    -> [Definition]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definitions -> [(QName, Definition)]
    sortDefs (Definitions -> [Definition])
    -> TCMT IO Definitions -> TCMT IO [Definition]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Definitions
    forall (m :: * -> *). ReadTCState m => m Definitions
    curDefs
          [def]
    res  <- (Definition -> TCMT IO def) -> [Definition] -> TCMT IO [def]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Backend' opts env menv mod def
    -> env -> menv -> IsMain -> Definition -> TCMT IO def
    forall opts env menv mod def.
    Backend' opts env menv mod def
    -> env -> menv -> IsMain -> Definition -> TCM def
    compileDef' Backend' opts env menv mod def
    backend env
    env menv
    menv IsMain
    isMain (Definition -> TCMT IO def)
    -> (Definition -> TCMT IO Definition) -> Definition -> TCMT IO def
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< Definition -> TCMT IO Definition
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull) [Definition]
    defs
          Backend' opts env menv mod def
    -> env -> menv -> IsMain -> ModuleName -> [def] -> TCM mod
    forall opts env menv mod def.
    Backend' opts env menv mod def
    -> env -> menv -> IsMain -> ModuleName -> [def] -> TCM mod
    postModule Backend' opts env menv mod def
    backend env
    env menv
    menv IsMain
    isMain (Interface -> ModuleName
    iModuleName Interface
    i) [def]
    res

    compileDef' :: Backend' opts env menv mod def -> env -> menv -> IsMain -> Definition -> TCM def
    compileDef' :: forall opts env menv mod def.
    Backend' opts env menv mod def
    -> env -> menv -> IsMain -> Definition -> TCM def
    compileDef' Backend' opts env menv mod def
    backend env
    env menv
    menv IsMain
    isMain Definition
    def =
      QName -> TCMT IO def -> TCMT IO def
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange (Definition -> QName
    defName Definition
    def) (TCMT IO def -> TCMT IO def) -> TCMT IO def -> TCMT IO def
    forall a b. (a -> b) -> a -> b
    $
        Backend' opts env menv mod def
    -> env -> menv -> IsMain -> Definition -> TCMT IO def
    forall opts env menv mod def.
    Backend' opts env menv mod def
    -> env -> menv -> IsMain -> Definition -> TCM def
    compileDef Backend' opts env menv mod def
    backend env
    env menv
    menv IsMain
    isMain Definition
    def