    {-# LANGUAGE NondecreasingIndentation #-}
    {-# OPTIONS_GHC -fno-warn-orphans #-}

    module Agda.Interaction.BasicOps where

    import Prelude hiding (null)

    import Control.Arrow          ( first )
    import Control.Monad.Except   ( MonadError(..) )
    import Control.Monad.State    ( MonadState(..), evalState )
    import Control.Monad.Identity ( runIdentity )
    import Control.Monad.Trans.Maybe

    import qualified Data.Map as Map
    import qualified Data.IntMap as IntMap
    import qualified Data.Map.Strict as MapS
    import qualified Data.Set as Set
    import qualified Data.List as List
    import Data.Maybe
    import Data.Monoid
    import Data.Function (on)
    import Data.Text (Text)
    import qualified Data.Text as T

    import Agda.Interaction.Base
    import Agda.Interaction.Output
    import Agda.Interaction.Options
    import Agda.Interaction.Response (Goals, ResponseContextEntry(..))

    import qualified Agda.Syntax.Concrete as C -- ToDo: Remove with instance of ToConcrete
    import Agda.Syntax.Position
    import Agda.Syntax.Abstract as A hiding (Open, Apply, Assign)
    import Agda.Syntax.Abstract.Views as A
    import Agda.Syntax.Abstract.Pretty
    import Agda.Syntax.Common
    import Agda.Syntax.Info (MetaInfo(..),emptyMetaInfo,exprNoRange,defaultAppInfo_,defaultAppInfo)
    import qualified Agda.Syntax.Info as Info
    import Agda.Syntax.Internal as I
    import Agda.Syntax.Literal
    import Agda.Syntax.Translation.InternalToAbstract
    import Agda.Syntax.Translation.AbstractToConcrete
    import Agda.Syntax.Translation.ConcreteToAbstract
    import Agda.Syntax.Scope.Base
    import Agda.Syntax.Scope.Monad
    import Agda.Syntax.Fixity(Precedence(..), argumentCtx_)
    import Agda.Syntax.Parser

    import Agda.TheTypeChecker
    import Agda.TypeChecking.Constraints
    import Agda.TypeChecking.Conversion
    import Agda.TypeChecking.Errors ( getAllWarnings, Verbalize(..) )
    import Agda.TypeChecking.Monad as M hiding (MetaInfo)
    import Agda.TypeChecking.MetaVars
    import Agda.TypeChecking.MetaVars.Mention
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope.Path
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.With
    import Agda.TypeChecking.Coverage
    import Agda.TypeChecking.Coverage.Match ( SplitPattern )
    import Agda.TypeChecking.Records
    import Agda.TypeChecking.Pretty ( PrettyTCM, prettyTCM )
    import Agda.TypeChecking.Pretty.Constraint (prettyRangeConstraint)
    import Agda.TypeChecking.IApplyConfluence
    import Agda.TypeChecking.Primitive
    import Agda.TypeChecking.ProjectionLike (reduceProjectionLike)
    import Agda.TypeChecking.Names
    import Agda.TypeChecking.Free
    import Agda.TypeChecking.CheckInternal
    import Agda.TypeChecking.SizedTypes.Solve
    import qualified Agda.TypeChecking.Pretty as TP
    import Agda.TypeChecking.Warnings
      ( warning, WhichWarnings(..), classifyWarnings, isMetaTCWarning
      , WarningsAndNonFatalErrors )

    import Agda.Termination.TermCheck (termMutual)

    import Agda.Utils.Function (applyWhen)
    import Agda.Utils.Functor
    import Agda.Utils.Lens
    import Agda.Utils.List
    import Agda.Utils.List1 (List1, pattern (:|))
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Syntax.Common.Pretty as P
    import Agda.Utils.Permutation
    import Agda.Utils.Size
    import Agda.Utils.String
    import Agda.Utils.WithDefault ( WithDefault'(Value) )

    import Agda.Utils.Impossible

    -- | Parses an expression.

    parseExpr :: Range -> String -> TCM C.Expr
    parseExpr :: Range -> ArgName -> TCM Expr
    parseExpr Range
    rng ArgName
    s = do
      (C.ExprWhere e wh, attrs) <-
        PM (ExprWhere, Attributes) -> TCM (ExprWhere, Attributes)
    forall a. PM a -> TCM a
    runPM (PM (ExprWhere, Attributes) -> TCM (ExprWhere, Attributes))
    -> PM (ExprWhere, Attributes) -> TCM (ExprWhere, Attributes)
    forall a b. (a -> b) -> a -> b
    $ Parser ExprWhere
    -> Position -> ArgName -> PM (ExprWhere, Attributes)
    forall a. Parser a -> Position -> ArgName -> PM (a, Attributes)
    parsePosString Parser ExprWhere
    exprWhereParser Position
    pos ArgName
    s
      checkAttributes attrs
      unless (null wh) $ interactionError UnexpectedWhere
      return e
      where pos :: Position
    pos = Position -> Maybe Position -> Position
    forall a. a -> Maybe a -> a
    fromMaybe (Maybe RangeFile -> Position
    startPos Maybe RangeFile
    forall a. Maybe a
    Nothing) (Maybe Position -> Position) -> Maybe Position -> Position
    forall a b. (a -> b) -> a -> b
    $ Range -> Maybe Position
    forall a. Range' a -> Maybe (Position' a)
    rStart Range
    rng

    parseExprIn :: InteractionId -> Range -> String -> TCM Expr
    parseExprIn :: InteractionId -> Range -> ArgName -> TCM Expr
    parseExprIn InteractionId
    ii Range
    rng ArgName
    s = do
        mId <- InteractionId -> TCMT IO MetaId
    forall (m :: * -> *).
    (ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m MetaId
    lookupInteractionId InteractionId
    ii
        updateMetaVarRange mId rng
        mi  <- getMetaInfo <$> lookupLocalMeta mId
        e   <- parseExpr rng s
        -- Andreas, 2019-08-19, issue #4007
        -- We need to be in the TCEnv of the meta variable
        -- such that the scope checker can label the clause
        -- of a parsed extended lambda as IsAbstract if the
        -- interaction point was created in AbstractMode.
        withMetaInfo mi $
          concreteToAbstract (clScope mi) e

    -- Type check the given expression and assign its value to the meta
    -- Precondition: we are in the context where the given meta was created.
    giveExpr :: UseForce -> Maybe InteractionId -> MetaId -> Expr -> TCM Term
    giveExpr :: UseForce -> Maybe InteractionId -> MetaId -> Expr -> TCM Term
    giveExpr UseForce
    force Maybe InteractionId
    mii MetaId
    mi Expr
    e = do
        mv <- MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    mi
        let t = case MetaVariable -> Judgement MetaId
    mvJudgement MetaVariable
    mv of
                  IsSort{}    -> Type
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                  HasType MetaId
    _ Comparison
    _ Type
    t -> Type
    t
        reportSDoc "interaction.give" 20 $
          "give: meta type =" TP.<+> prettyTCM t
        -- Here, we must be in the same context where the meta was created.
        -- Thus, we can safely apply its type to the context variables.
        ctx <- getContextArgs
        t' <- t `piApplyM` permute (takeP (length ctx) $ mvPermutation mv) ctx
        traceCall (CheckExprCall CmpLeq e t') $ do
          reportSDoc "interaction.give" 20 $ do
            a <- asksTC envAbstractMode
            TP.hsep
              [ TP.text ("give(" ++ show a ++ "): instantiated meta type =")
              , prettyTCM t'
              ]
          -- Andreas, 2020-05-27 AIM XXXII, issue #4679
          -- Clear envMutualBlock since cubical only executes
          -- certain checks (checkIApplyConfluence) for an extended lambda
          -- when not in a mutual block.
          v <- locallyTC eMutualBlock (const Nothing) $
            checkExpr e t'
          reportSDoc "interaction.give" 40 $ "give: checked expression:" TP.<+> pure (pretty v)
          case mvInstantiation mv of

            InstV{} -> TCMT IO Bool -> ScopeM () -> ScopeM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM (Relevance -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant (Relevance -> Bool) -> TCMT IO Relevance -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' TCEnv Relevance -> TCMT IO Relevance
    forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
    viewTC (Relevance -> f Relevance) -> TCEnv -> f TCEnv
    Lens' TCEnv Relevance
    eRelevance) (ScopeM () -> ScopeM ()) -> ScopeM () -> ScopeM ()
    forall a b. (a -> b) -> a -> b
    $ do
              v' <- Term -> TCM Term
    forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
    instantiate (Term -> TCM Term) -> Term -> TCM Term
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Elims -> Term
    MetaV MetaId
    mi (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Elim' Term) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply Args
    ctx
              reportSDoc "interaction.give" 20 $ TP.sep
                [ "meta was already set to value v' = " TP.<+> prettyTCM v'
                , "now comparing it to given value v = " TP.<+> prettyTCM v
                , "in context " TP.<+> inTopContext (prettyTCM ctx)
                ]
              equalTerm t' v v'

            MetaInstantiation
    _ -> do -- updateMeta mi v
              ArgName -> Int -> ArgName -> ScopeM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> ArgName -> m ()
    reportSLn ArgName
    "interaction.give" Int
    20 ArgName
    "give: meta unassigned, assigning..."
              args <- TCMT IO Args
    forall (m :: * -> *). MonadTCEnv m => m Args
    getContextArgs
              nowSolvingConstraints $ assign DirEq mi args v (AsTermsOf t')

          reportSDoc "interaction.give" 20 $ "give: meta variable updated!"
          unless (force == WithForce) $ redoChecks mii
          wakeupConstraints mi
          solveSizeConstraints DontDefaultToInfty
          cubical <- isJust <$> cubicalOption
          -- don't double check with cubical, because it gets in the way too often.
          unless (cubical || force == WithForce) $ do
            -- Double check.
            reportSDoc "interaction.give" 20 $ "give: double checking"
            vfull <- instantiateFull v
            checkInternal vfull CmpLeq t'
          return v

    -- | After a give, redo termination etc. checks for function which was complemented.
    redoChecks :: Maybe InteractionId -> TCM ()
    redoChecks :: Maybe InteractionId -> ScopeM ()
    redoChecks Maybe InteractionId
    Nothing = () -> ScopeM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
    redoChecks (Just InteractionId
    ii) = do
      ArgName -> Int -> ArgName -> ScopeM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> ArgName -> m ()
    reportSLn ArgName
    "interaction.give" Int
    20 (ArgName -> ScopeM ()) -> ArgName -> ScopeM ()
    forall a b. (a -> b) -> a -> b
    $
        ArgName
    "give: redoing termination check for function surrounding " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ InteractionId -> ArgName
    forall a. Show a => a -> ArgName
    show InteractionId
    ii
      ip <- InteractionId -> TCMT IO InteractionPoint
    forall (m :: * -> *).
    (ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m InteractionPoint
    lookupInteractionPoint InteractionId
    ii
      case ipClause ip of
        IPClause
    IPNoClause -> () -> ScopeM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        IPClause{ipcQName :: IPClause -> QName
    ipcQName = QName
    f} -> do
          mb <- Definition -> MutualId
    defMutual (Definition -> MutualId) -> TCMT IO Definition -> TCMT IO MutualId
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f
          terErrs <- localTC (\ TCEnv
    e -> TCEnv
    e { envMutualBlock = Just mb }) $ termMutual []
          List1.unlessNull terErrs $ warning . TerminationIssue
      -- TODO redo positivity check!

    -- | Auxiliary definition for 'give' and 'elaborate_give'.
    give_ ::
         Bool           -- ^ Elaborating?
      -> UseForce       -- ^ Skip safety checks?
      -> InteractionId  -- ^ Hole.
      -> Maybe Range
      -> Expr           -- ^ The expression to give.
      -> TCM Term       -- ^ Value of the expression
    give_ :: Bool
    -> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Term
    give_ Bool
    elaborating UseForce
    force InteractionId
    ii Maybe Range
    mr Expr
    e = do
      -- if Range is given, update the range of the interaction meta
      mi  <- InteractionId -> TCMT IO MetaId
    forall (m :: * -> *).
    (ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m MetaId
    lookupInteractionId InteractionId
    ii
      whenJust mr $ updateMetaVarRange mi
      reportSDoc "interaction.give" 10 $ "giving expression" TP.<+> prettyTCM e
      reportSDoc "interaction.give" 50 $ TP.text $ show $ deepUnscope e
      -- Try to give mi := e
      withInteractionId ii do
        setMetaOccursCheck mi DontRunMetaOccursCheck -- #589, #2710: Allow giving recursive solutions.
        applyWhen elaborating (locallyTC eCurrentlyElaborating $ const True) do
          -- Andreas, 2025-05-02, issue #7842 reproduces this error
          let err Blocker
    _blocker = TypeError -> TCM Term
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM Term) -> TypeError -> TCM Term
    forall a b. (a -> b) -> a -> b
    $ InteractionError -> TypeError
    InteractionError (InteractionError -> TypeError) -> InteractionError -> TypeError
    forall a b. (a -> b) -> a -> b
    $ Expr -> InteractionError
    CannotGive Expr
    e
          catchPatternErr err do
            giveExpr force (Just ii) mi e

    -- | Try to fill hole by expression.
    --
    --   Returns the given expression unchanged
    --   (for convenient generalization to @'refine'@).
    give ::
         UseForce       -- ^ Skip safety checks?
      -> InteractionId  -- ^ Hole.
      -> Maybe Range
      -> Expr           -- ^ The expression to give.
      -> TCM Expr       -- ^ If successful, the very expression is returned unchanged.
    give :: UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
    give UseForce
    force InteractionId
    ii Maybe Range
    mr Expr
    e = do
      _ <- Bool
    -> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Term
    give_ Bool
    False UseForce
    force InteractionId
    ii Maybe Range
    mr Expr
    e
      removeInteractionPoint ii
      return e

    -- | Try to fill hole by elaborated expression.
    elaborate_give
      :: Rewrite        -- ^ Normalise result?
      -> UseForce       -- ^ Skip safety checks?
      -> InteractionId  -- ^ Hole.
      -> Maybe Range
      -> Expr           -- ^ The expression to give.
      -> TCM Expr       -- ^ If successful, return the elaborated expression.
    elaborate_give :: Rewrite
    -> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
    elaborate_give Rewrite
    norm UseForce
    force InteractionId
    ii Maybe Range
    mr Expr
    e = InteractionId -> TCM Expr -> TCM Expr
    forall (m :: * -> *) a.
    (MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    ii (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
    forall a b. (a -> b) -> a -> b
    $ do
      v <- Bool
    -> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Term
    give_ Bool
    True UseForce
    force InteractionId
    ii Maybe Range
    mr Expr
    e
      reportSDoc "interaction.give" 40 $ "v = " TP.<+> pure (pretty v)
      -- Reduce projection-likes before quoting, otherwise instance
      -- selection may fail on reload (see #6203).
      nv <- reduceProjectionLike =<< normalForm norm v
      locallyTC ePrintMetasBare (const True) $ reify nv

    -- | Try to refine hole by expression @e@.
    --
    --   This amounts to successively try to give @e@, @e ?@, @e ? ?@, ...
    --   Returns the successfully given expression.
    refine
      :: UseForce       -- ^ Skip safety checks when giving?
      -> InteractionId  -- ^ Hole.
      -> Maybe Range
      -> Expr           -- ^ The expression to refine the hole with.
      -> TCM Expr       -- ^ The successfully given expression.
    refine :: UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
    refine UseForce
    force InteractionId
    ii Maybe Range
    mr Expr
    e = do
      mi <- InteractionId -> TCMT IO MetaId
    forall (m :: * -> *).
    (ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m MetaId
    lookupInteractionId InteractionId
    ii
      mv <- lookupLocalMeta mi
      let range = Range -> Maybe Range -> Range
    forall a. a -> Maybe a -> a
    fromMaybe (MetaVariable -> Range
    forall a. HasRange a => a -> Range
    getRange MetaVariable
    mv) Maybe Range
    mr
          scope = MetaVariable -> ScopeInfo
    M.getMetaScope MetaVariable
    mv
      reportSDoc "interaction.refine" 10 $
        "refining with expression" TP.<+> prettyTCM e
      reportSDoc "interaction.refine" 50 $
        TP.text $ show $ deepUnscope e
      -- We try to append up to 10 meta variables
      tryRefine 10 range scope e
      where
        tryRefine :: Int -> Range -> ScopeInfo -> Expr -> TCM Expr
        tryRefine :: Int -> Range -> ScopeInfo -> Expr -> TCM Expr
    tryRefine Int
    nrOfMetas Range
    r ScopeInfo
    scope = Int -> Maybe TCErr -> Expr -> TCM Expr
    try Int
    nrOfMetas Maybe TCErr
    forall a. Maybe a
    Nothing
          where
            try :: Int -> Maybe TCErr -> Expr -> TCM Expr
            try :: Int -> Maybe TCErr -> Expr -> TCM Expr
    try Int
    0 Maybe TCErr
    err Expr
    e = InteractionError -> TCM Expr
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    InteractionError -> m a
    interactionError (InteractionError -> TCM Expr) -> InteractionError -> TCM Expr
    forall a b. (a -> b) -> a -> b
    $ ArgName -> InteractionError
    CannotRefine (ArgName -> InteractionError) -> ArgName -> InteractionError
    forall a b. (a -> b) -> a -> b
    $ case Maybe TCErr
    err of
               Just (TypeError CallStack
    _ TCState
    _ Closure TypeError
    cl) | UnequalTerms Comparison
    _ I.Pi{} Term
    _ CompareAs
    _ <- Closure TypeError -> TypeError
    forall a. Closure a -> a
    clValue Closure TypeError
    cl ->
                 ArgName
    "functions with 10 or more arguments"
               Maybe TCErr
    _ -> ArgName
    ""
            try Int
    n Maybe TCErr
    _ Expr
    e = UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
    give UseForce
    force InteractionId
    ii (Range -> Maybe Range
    forall a. a -> Maybe a
    Just Range
    r) Expr
    e TCM Expr -> (TCErr -> TCM Expr) -> TCM Expr
    forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \TCErr
    err -> Int -> Maybe TCErr -> Expr -> TCM Expr
    try (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) (TCErr -> Maybe TCErr
    forall a. a -> Maybe a
    Just TCErr
    err) (Expr -> TCM Expr) -> TCM Expr -> TCM Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Expr -> TCM Expr
    appMeta Expr
    e

            -- Apply A.Expr to a new meta
            appMeta :: Expr -> TCM Expr
            appMeta :: Expr -> TCM Expr
    appMeta Expr
    e = do
              let rng :: Range
    rng = Range -> Range
    rightMargin Range
    r -- Andreas, 2013-05-01 conflate range to its right margin to ensure that appended metas are last in numbering.  This fixes issue 841.
              -- Make new interaction point
              ii <- Bool -> Range -> Maybe Int -> TCMT IO InteractionId
    forall (m :: * -> *).
    MonadInteractionPoints m =>
    Bool -> Range -> Maybe Int -> m InteractionId
    registerInteractionPoint Bool
    False Range
    rng Maybe Int
    forall a. Maybe a
    Nothing
              let info = Info.MetaInfo
                    { metaRange :: Range
    Info.metaRange = Range
    rng
                    , metaScope :: ScopeInfo
    Info.metaScope = Lens' ScopeInfo [Precedence] -> LensSet ScopeInfo [Precedence]
    forall o i. Lens' o i -> LensSet o i
    set ([Precedence] -> f [Precedence]) -> ScopeInfo -> f ScopeInfo
    Lens' ScopeInfo [Precedence]
    scopePrecedence [Precedence
    argumentCtx_] ScopeInfo
    scope
                        -- Ulf, 2017-09-07: The `argumentCtx_` above is causing #737.
                        -- If we're building an operator application the precedence
                        -- should be something else.
                    , metaNumber :: Maybe MetaId
    metaNumber = Maybe MetaId
    forall a. Maybe a
    Nothing -- in order to print just as ?, not ?n
                    , metaNameSuggestion :: ArgName
    metaNameSuggestion = ArgName
    ""
                    , metaKind :: MetaKind
    metaKind           = MetaKind
    Info.UnificationMeta
                    }
                  metaVar = MetaInfo -> InteractionId -> Expr
    QuestionMark MetaInfo
    info InteractionId
    ii

                  count Name
    x a
    e = Sum a -> a
    forall a. Sum a -> a
    getSum (Sum a -> a) -> Sum a -> a
    forall a b. (a -> b) -> a -> b
    $ (Expr -> Sum a) -> a -> Sum a
    forall m. FoldExprFn m a
    forall a m. ExprLike a => FoldExprFn m a
    foldExpr Expr -> Sum a
    isX a
    e
                    where isX :: Expr -> Sum a
    isX (A.Var Name
    y) | Name
    x Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name
    y = a -> Sum a
    forall a. a -> Sum a
    Sum a
    1
                          isX Expr
    _                  = Sum a
    forall a. Monoid a => a
    mempty

                  lamView (A.Lam ExprInfo
    _ (DomainFree TacticAttribute
    _ NamedArg Binder
    x) Expr
    e) = (Binder, Expr) -> Maybe (Binder, Expr)
    forall a. a -> Maybe a
    Just (NamedArg Binder -> Binder
    forall a. NamedArg a -> a
    namedArg NamedArg Binder
    x, Expr
    e)
                  lamView (A.Lam ExprInfo
    i (DomainFull (TBind Range
    r TypedBindingInfo
    t (NamedArg Binder
    x :| [NamedArg Binder]
    xs) Expr
    a)) Expr
    e) =
                    [NamedArg Binder]
    -> Maybe (Binder, Expr)
    -> (NonEmpty (NamedArg Binder) -> Maybe (Binder, Expr))
    -> Maybe (Binder, Expr)
    forall a b. [a] -> b -> (List1 a -> b) -> b
    List1.ifNull [NamedArg Binder]
    xs {-then-} ((Binder, Expr) -> Maybe (Binder, Expr)
    forall a. a -> Maybe a
    Just (NamedArg Binder -> Binder
    forall a. NamedArg a -> a
    namedArg NamedArg Binder
    x, Expr
    e)) {-else-} ((NonEmpty (NamedArg Binder) -> Maybe (Binder, Expr))
     -> Maybe (Binder, Expr))
    -> (NonEmpty (NamedArg Binder) -> Maybe (Binder, Expr))
    -> Maybe (Binder, Expr)
    forall a b. (a -> b) -> a -> b
    $ \ NonEmpty (NamedArg Binder)
    xs ->
                      (Binder, Expr) -> Maybe (Binder, Expr)
    forall a. a -> Maybe a
    Just (NamedArg Binder -> Binder
    forall a. NamedArg a -> a
    namedArg NamedArg Binder
    x, ExprInfo -> LamBinding -> Expr -> Expr
    A.Lam ExprInfo
    i (TypedBinding -> LamBinding
    DomainFull (TypedBinding -> LamBinding) -> TypedBinding -> LamBinding
    forall a b. (a -> b) -> a -> b
    $ Range
    -> TypedBindingInfo
    -> NonEmpty (NamedArg Binder)
    -> Expr
    -> TypedBinding
    TBind Range
    r TypedBindingInfo
    t NonEmpty (NamedArg Binder)
    xs Expr
    a) Expr
    e)
                  lamView Expr
    _ = Maybe (Binder, Expr)
    forall a. Maybe a
    Nothing

                  -- reduce beta-redexes where the argument is used at most once
                  smartApp AppInfo
    i Expr
    e NamedArg Expr
    arg =
                    case ((Binder, Expr) -> (BindName, Expr))
    -> Maybe (Binder, Expr) -> Maybe (BindName, Expr)
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Binder -> BindName) -> (Binder, Expr) -> (BindName, Expr)
    forall b c d. (b -> c) -> (b, d) -> (c, d)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (b, d) (c, d)
    first Binder -> BindName
    forall a. Binder' a -> a
    A.binderName) (Expr -> Maybe (Binder, Expr)
    lamView (Expr -> Maybe (Binder, Expr)) -> Expr -> Maybe (Binder, Expr)
    forall a b. (a -> b) -> a -> b
    $ Expr -> Expr
    unScope Expr
    e) of
                      Just (A.BindName{unBind :: BindName -> Name
    unBind = Name
    x}, Expr
    e) | Name -> Expr -> Integer
    forall {a} {a}. (Num a, ExprLike a) => Name -> a -> a
    count Name
    x Expr
    e Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    2 -> (Expr -> Expr) -> Expr -> Expr
    forall a. ExprLike a => (Expr -> Expr) -> a -> a
    mapExpr Expr -> Expr
    subX Expr
    e
                        where subX :: Expr -> Expr
    subX (A.Var Name
    y) | Name
    x Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name
    y = NamedArg Expr -> Expr
    forall a. NamedArg a -> a
    namedArg NamedArg Expr
    arg
                              subX Expr
    e = Expr
    e
                      Maybe (BindName, Expr)
    _ -> AppInfo -> Expr -> NamedArg Expr -> Expr
    App AppInfo
    i Expr
    e NamedArg Expr
    arg
              return $ smartApp (defaultAppInfo r) e $ defaultNamedArg metaVar

    {-| Evaluate the given expression in the current environment -}
    evalInCurrent :: ComputeMode -> Expr -> TCM Expr
    evalInCurrent :: ComputeMode -> Expr -> TCM Expr
    evalInCurrent ComputeMode
    cmode Expr
    e = do
      (v, _t) <- Expr -> TCM (Term, Type)
    inferExpr Expr
    e
      vb <- reduceB v
      reportSDoc "interaction.eval" 30 $ "evaluated to" TP.<+> TP.pretty vb
      v  <- pure $ ignoreBlocking vb
      reify =<< if cmode == HeadCompute then pure v else normalise v

    evalInMeta :: InteractionId -> ComputeMode -> Expr -> TCM Expr
    evalInMeta :: InteractionId -> ComputeMode -> Expr -> TCM Expr
    evalInMeta InteractionId
    ii ComputeMode
    cmode Expr
    e =
       do   m <- InteractionId -> TCMT IO MetaId
    forall (m :: * -> *).
    (ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m MetaId
    lookupInteractionId InteractionId
    ii
            mi <- getMetaInfo <$> lookupLocalMeta m
            withMetaInfo mi $
                evalInCurrent cmode e

    -- | Modifier for interactive commands,
    --   specifying the amount of normalization in the output.
    --
    normalForm :: (Reduce t, Simplify t, Instantiate t, Normalise t) => Rewrite -> t -> TCM t
    normalForm :: forall t.
    (Reduce t, Simplify t, Instantiate t, Normalise t) =>
    Rewrite -> t -> TCM t
    normalForm = \case
      Rewrite
    AsIs         -> t -> TCM t
    forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
    instantiate   -- #4975: reify will also instantiate by for goal-type-and-context-and-check
      Rewrite
    Instantiated -> t -> TCM t
    forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
    instantiate   --        we get a top-level fresh meta which has disappeared from state by the
      Rewrite
    HeadNormal   -> t -> TCM t
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce        --        time we get to reification. Hence instantiate here.
      Rewrite
    Simplified   -> t -> TCM t
    forall a (m :: * -> *). (Simplify a, MonadReduce m) => a -> m a
    simplify
      Rewrite
    Normalised   -> t -> TCM t
    forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
    normalise

    -- | Modifier for the interactive computation command,
    --   specifying the mode of computation and result display.
    --
    computeIgnoreAbstract :: ComputeMode -> Bool
    computeIgnoreAbstract :: ComputeMode -> Bool
    computeIgnoreAbstract ComputeMode
    DefaultCompute  = Bool
    False
    computeIgnoreAbstract ComputeMode
    HeadCompute     = Bool
    False
    computeIgnoreAbstract ComputeMode
    IgnoreAbstract  = Bool
    True
    computeIgnoreAbstract ComputeMode
    UseShowInstance = Bool
    False
      -- WRONG: UseShowInstance requires the result to be a string literal so respecting abstract can
      -- only ever break things.
      -- See #7191. Abstract definitions can come with rewrite rules to give nice show behaviour that
      -- breaks if we don't respect abstract.

    computeWrapInput :: ComputeMode -> String -> String
    computeWrapInput :: ComputeMode -> ArgName -> ArgName
    computeWrapInput ComputeMode
    UseShowInstance ArgName
    s = ArgName
    "show (" ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ ArgName
    s ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ ArgName
    ")"
    computeWrapInput ComputeMode
    _               ArgName
    s = ArgName
    s

    showComputed :: ComputeMode -> Expr -> TCM Doc
    showComputed :: ComputeMode -> Expr -> TCMT IO Doc
    showComputed ComputeMode
    UseShowInstance Expr
    e =
      case Expr
    e of
        A.Lit ExprInfo
    _ (LitString Text
    s) -> Doc -> TCMT IO Doc
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (ArgName -> Doc
    forall a. ArgName -> Doc a
    text (ArgName -> Doc) -> ArgName -> Doc
    forall a b. (a -> b) -> a -> b
    $ Text -> ArgName
    T.unpack Text
    s)
        Expr
    _                     -> (Doc
    "Expected applying `show` to the given value to produce a string literal, but got:" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    $$) (Doc -> Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyATop Expr
    e
    showComputed ComputeMode
    _ Expr
    e = Expr -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyATop Expr
    e

    -- | Modifier for interactive commands,
    --   specifying whether safety checks should be ignored.
    outputFormId :: OutputForm a b -> b
    outputFormId :: forall a b. OutputForm a b -> b
    outputFormId (OutputForm Range
    _ [ProblemId]
    _ Blocker
    _ OutputConstraint_boot TCErr a b
    o) = OutputConstraint_boot TCErr a b -> b
    forall {tcErr} {a} {b}. OutputConstraint_boot tcErr a b -> b
    out OutputConstraint_boot TCErr a b
    o
      where
        out :: OutputConstraint_boot tcErr a b -> b
    out = \case
          OfType b
    i a
    _                 -> b
    i
          CmpInType Comparison
    _ a
    _ b
    i b
    _          -> b
    i
          CmpElim [Polarity]
    _ a
    _ (b
    i:[b]
    _) [b]
    _        -> b
    i
          CmpElim [Polarity]
    _ a
    _ [] [b]
    _           -> b
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          JustType b
    i                 -> b
    i
          CmpLevels Comparison
    _ b
    i b
    _            -> b
    i
          CmpTypes Comparison
    _ b
    i b
    _             -> b
    i
          CmpTeles Comparison
    _ b
    i b
    _             -> b
    i
          JustSort b
    i                 -> b
    i
          CmpSorts Comparison
    _ b
    i b
    _             -> b
    i
          Assign b
    i a
    _                 -> b
    i
          TypedAssign b
    i a
    _ a
    _          -> b
    i
          PostponedCheckArgs b
    i [a]
    _ a
    _ a
    _ -> b
    i
          IsEmptyType a
    _              -> b
    forall a. HasCallStack => a
    __IMPOSSIBLE__   -- Should never be used on IsEmpty constraints
          SizeLtSat{}                -> b
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          FindInstanceOF b
    _ a
    _ [(a, a, a)]
    _        -> b
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          ResolveInstanceOF QName
    _        -> b
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          PTSInstance b
    i b
    _            -> b
    i
          PostponedCheckFunDef{}     -> b
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          DataSort QName
    _ b
    i               -> b
    i
          CheckLock b
    i b
    _              -> b
    i
          UsableAtMod Modality
    _ b
    i            -> b
    i

    instance Reify ProblemConstraint where
      type ReifiesTo ProblemConstraint = Closure (OutputForm Expr Expr)
      reify :: forall (m :: * -> *).
    MonadReify m =>
    ProblemConstraint -> m (ReifiesTo ProblemConstraint)
    reify (PConstr Set ProblemId
    pids Blocker
    unblock Closure Constraint
    cl) = Closure Constraint
    -> (Constraint -> m (OutputForm Expr Expr))
    -> m (Closure (OutputForm Expr Expr))
    forall (m :: * -> *) a b.
    (MonadTCEnv m, ReadTCState m) =>
    Closure a -> (a -> m b) -> m (Closure b)
    withClosure Closure Constraint
    cl ((Constraint -> m (OutputForm Expr Expr))
     -> m (Closure (OutputForm Expr Expr)))
    -> (Constraint -> m (OutputForm Expr Expr))
    -> m (Closure (OutputForm Expr Expr))
    forall a b. (a -> b) -> a -> b
    $ \ Constraint
    c ->
        Range
    -> [ProblemId]
    -> Blocker
    -> OutputConstraint_boot TCErr Expr Expr
    -> OutputForm Expr Expr
    forall tcErr a b.
    Range
    -> [ProblemId]
    -> Blocker
    -> OutputConstraint_boot tcErr a b
    -> OutputForm_boot tcErr a b
    OutputForm (Constraint -> Range
    forall a. HasRange a => a -> Range
    getRange Constraint
    c) (Set ProblemId -> [ProblemId]
    forall a. Set a -> [a]
    Set.toList Set ProblemId
    pids) Blocker
    unblock (OutputConstraint_boot TCErr Expr Expr -> OutputForm Expr Expr)
    -> m (OutputConstraint_boot TCErr Expr Expr)
    -> m (OutputForm Expr Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Constraint -> m (ReifiesTo Constraint)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    Constraint -> m (ReifiesTo Constraint)
    reify Constraint
    c

    reifyElimToExpr :: MonadReify m => I.Elim -> m Expr
    reifyElimToExpr :: forall (m :: * -> *). MonadReify m => Elim' Term -> m Expr
    reifyElimToExpr = \case
        I.IApply Term
    _ Term
    _ Term
    v -> Text -> Arg Expr -> Expr
    appl Text
    "iapply" (Arg Expr -> Expr) -> m (Arg Expr) -> m Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term -> m (ReifiesTo (Arg Term))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    Arg Term -> m (ReifiesTo (Arg Term))
    reify (Term -> Arg Term
    forall a. a -> Arg a
    defaultArg (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Term
    v) -- TODO Andrea: endpoints?
        I.Apply Arg Term
    v -> Text -> Arg Expr -> Expr
    appl Text
    "apply" (Arg Expr -> Expr) -> m (Arg Expr) -> m Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term -> m (ReifiesTo (Arg Term))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    Arg Term -> m (ReifiesTo (Arg Term))
    reify Arg Term
    v
        I.Proj ProjOrigin
    _o QName
    f -> Text -> Arg Expr -> Expr
    appl Text
    "proj" (Arg Expr -> Expr) -> m (Arg Expr) -> m Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term -> m (ReifiesTo (Arg Term))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    Arg Term -> m (ReifiesTo (Arg Term))
    reify ((Term -> Arg Term
    forall a. a -> Arg a
    defaultArg (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ QName -> Elims -> Term
    I.Def QName
    f []) :: Arg Term)
      where
        appl :: Text -> Arg Expr -> Expr
        appl :: Text -> Arg Expr -> Expr
    appl Text
    s Arg Expr
    v = AppInfo -> Expr -> NamedArg Expr -> Expr
    A.App AppInfo
    defaultAppInfo_ (ExprInfo -> Literal -> Expr
    A.Lit ExprInfo
    forall a. Null a => a
    empty (Text -> Literal
    LitString Text
    s)) (NamedArg Expr -> Expr) -> NamedArg Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ (Expr -> Named_ Expr) -> Arg Expr -> NamedArg Expr
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Expr -> Named_ Expr
    forall a name. a -> Named name a
    unnamed Arg Expr
    v

    instance Reify Constraint where
      type ReifiesTo Constraint = OutputConstraint Expr Expr

      reify :: forall (m :: * -> *).
    MonadReify m =>
    Constraint -> m (ReifiesTo Constraint)
    reify (ValueCmp Comparison
    cmp (AsTermsOf Type
    t) Term
    u Term
    v) = Comparison
    -> Expr -> Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr
    forall tcErr a b.
    Comparison -> a -> b -> b -> OutputConstraint_boot tcErr a b
    CmpInType Comparison
    cmp (Expr -> Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
    -> m Expr
    -> m (Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> m (ReifiesTo Type)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
    reify Type
    t m (Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
    -> m Expr -> m (Expr -> OutputConstraint_boot TCErr Expr Expr)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify Term
    u m (Expr -> OutputConstraint_boot TCErr Expr Expr)
    -> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify Term
    v
      reify (ValueCmp Comparison
    cmp CompareAs
    AsSizes Term
    u Term
    v) = Comparison
    -> Expr -> Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr
    forall tcErr a b.
    Comparison -> a -> b -> b -> OutputConstraint_boot tcErr a b
    CmpInType Comparison
    cmp (Expr -> Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
    -> m Expr
    -> m (Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Type -> m Expr
    Type -> m (ReifiesTo Type)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
    reify (Type -> m Expr) -> m Type -> m Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< m Type
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
    m Type
    sizeType) m (Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
    -> m Expr -> m (Expr -> OutputConstraint_boot TCErr Expr Expr)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify Term
    u m (Expr -> OutputConstraint_boot TCErr Expr Expr)
    -> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify Term
    v
      reify (ValueCmp Comparison
    cmp CompareAs
    AsTypes Term
    u Term
    v) = Comparison -> Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr
    forall tcErr a b.
    Comparison -> b -> b -> OutputConstraint_boot tcErr a b
    CmpTypes Comparison
    cmp (Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
    -> m Expr -> m (Expr -> OutputConstraint_boot TCErr Expr Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify Term
    u m (Expr -> OutputConstraint_boot TCErr Expr Expr)
    -> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify Term
    v
      reify (ValueCmpOnFace Comparison
    cmp Term
    p Type
    t Term
    u Term
    v) = Comparison
    -> Expr -> Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr
    forall tcErr a b.
    Comparison -> a -> b -> b -> OutputConstraint_boot tcErr a b
    CmpInType Comparison
    cmp (Expr -> Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
    -> m Expr
    -> m (Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Type -> m Expr
    Type -> m (ReifiesTo Type)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
    reify (Type -> m Expr) -> m Type -> m Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< m Type
    ty) m (Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
    -> m Expr -> m (Expr -> OutputConstraint_boot TCErr Expr Expr)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify (Term -> Term
    lam_o Term
    u) m (Expr -> OutputConstraint_boot TCErr Expr Expr)
    -> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify (Term -> Term
    lam_o Term
    v)
        where
          lam_o :: Term -> Term
    lam_o = ArgInfo -> Abs Term -> Term
    I.Lam ArgInfo
    defaultIrrelevantArgInfo (Abs Term -> Term) -> (Term -> Abs Term) -> Term -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ArgName -> Term -> Abs Term
    forall a. ArgName -> a -> Abs a
    NoAbs ArgName
    "_"
          ty :: m Type
    ty = Names -> NamesT m Type -> m Type
    forall (m :: * -> *) a. Names -> NamesT m a -> m a
    runNamesT [] (NamesT m Type -> m Type) -> NamesT m Type -> m Type
    forall a b. (a -> b) -> a -> b
    $ do
            p <- Term -> NamesT m (NamesT m Term)
    forall (m :: * -> *) a.
    (Monad m, Subst a) =>
    a -> NamesT m (NamesT m a)
    open Term
    p
            t <- open t
            pPi' "o" p (\ NamesT m Term
    o -> NamesT m Type
    t)
      reify (ElimCmp [Polarity]
    cmp [IsForced]
    _ Type
    t Term
    v Elims
    es1 Elims
    es2) =
        [Polarity]
    -> Expr
    -> [Expr]
    -> [Expr]
    -> OutputConstraint_boot TCErr Expr Expr
    forall tcErr a b.
    [Polarity] -> a -> [b] -> [b] -> OutputConstraint_boot tcErr a b
    CmpElim [Polarity]
    cmp (Expr -> [Expr] -> [Expr] -> OutputConstraint_boot TCErr Expr Expr)
    -> m Expr
    -> m ([Expr] -> [Expr] -> OutputConstraint_boot TCErr Expr Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> m (ReifiesTo Type)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
    reify Type
    t m ([Expr] -> [Expr] -> OutputConstraint_boot TCErr Expr Expr)
    -> m [Expr] -> m ([Expr] -> OutputConstraint_boot TCErr Expr Expr)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Elim' Term -> m Expr) -> Elims -> m [Expr]
    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 Elim' Term -> m Expr
    forall (m :: * -> *). MonadReify m => Elim' Term -> m Expr
    reifyElimToExpr Elims
    es1
                                m ([Expr] -> OutputConstraint_boot TCErr Expr Expr)
    -> m [Expr] -> m (OutputConstraint_boot TCErr Expr Expr)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Elim' Term -> m Expr) -> Elims -> m [Expr]
    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 Elim' Term -> m Expr
    forall (m :: * -> *). MonadReify m => Elim' Term -> m Expr
    reifyElimToExpr Elims
    es2
      reify (LevelCmp Comparison
    cmp Level
    t Level
    t')    = Comparison -> Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr
    forall tcErr a b.
    Comparison -> b -> b -> OutputConstraint_boot tcErr a b
    CmpLevels Comparison
    cmp (Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
    -> m Expr -> m (Expr -> OutputConstraint_boot TCErr Expr Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Level -> m (ReifiesTo Level)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Level -> m (ReifiesTo Level)
    reify Level
    t m (Expr -> OutputConstraint_boot TCErr Expr Expr)
    -> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Level -> m (ReifiesTo Level)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Level -> m (ReifiesTo Level)
    reify Level
    t'
      reify (SortCmp Comparison
    cmp Sort
    s Sort
    s')     = Comparison -> Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr
    forall tcErr a b.
    Comparison -> b -> b -> OutputConstraint_boot tcErr a b
    CmpSorts Comparison
    cmp (Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
    -> m Expr -> m (Expr -> OutputConstraint_boot TCErr Expr Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Sort -> m (ReifiesTo Sort)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Sort -> m (ReifiesTo Sort)
    reify Sort
    s m (Expr -> OutputConstraint_boot TCErr Expr Expr)
    -> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Sort -> m (ReifiesTo Sort)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Sort -> m (ReifiesTo Sort)
    reify Sort
    s'
      reify (UnquoteTactic Term
    tac Term
    _ Type
    goal) = do
          tac <- AppInfo -> Expr -> NamedArg Expr -> Expr
    A.App AppInfo
    defaultAppInfo_ (ExprInfo -> Expr
    A.Unquote ExprInfo
    exprNoRange) (NamedArg Expr -> Expr) -> (Expr -> NamedArg Expr) -> Expr -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Expr -> NamedArg Expr
    forall a. a -> NamedArg a
    defaultNamedArg (Expr -> Expr) -> m Expr -> m Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify Term
    tac
          OfType tac <$> reify goal
      reify (UnBlock MetaId
    m) = do
          mi <- MetaId -> m MetaInstantiation
    forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m MetaInstantiation
    lookupMetaInstantiation MetaId
    m
          m' <- reify (MetaV m [])
          case mi of
            BlockedConst Term
    t -> do
              e  <- Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify Term
    t
              return $ Assign m' e
            PostponedTypeCheckingProblem Closure TypeCheckingProblem
    cl -> Closure TypeCheckingProblem
    -> (TypeCheckingProblem
        -> m (OutputConstraint_boot TCErr Expr Expr))
    -> m (OutputConstraint_boot TCErr Expr Expr)
    forall (m :: * -> *) c a b.
    (MonadTCEnv m, ReadTCState m, LensClosure c a) =>
    c -> (a -> m b) -> m b
    enterClosure Closure TypeCheckingProblem
    cl ((TypeCheckingProblem -> m (OutputConstraint_boot TCErr Expr Expr))
     -> m (OutputConstraint_boot TCErr Expr Expr))
    -> (TypeCheckingProblem
        -> m (OutputConstraint_boot TCErr Expr Expr))
    -> m (OutputConstraint_boot TCErr Expr Expr)
    forall a b. (a -> b) -> a -> b
    $ \case
              CheckExpr Comparison
    cmp Expr
    e Type
    a -> do
                  a  <- Type -> m (ReifiesTo Type)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
    reify Type
    a
                  return $ TypedAssign m' e a
              CheckLambda Comparison
    cmp (Arg ArgInfo
    ai (List1 (WithHiding Name)
    xs, Maybe Type
    mt)) Expr
    body Type
    target -> do
                domType <- m Expr -> (Type -> m Expr) -> Maybe Type -> m Expr
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe (Expr -> m Expr
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr
    forall a. Underscore a => a
    underscore) Type -> m Expr
    Type -> m (ReifiesTo Type)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
    reify Maybe Type
    mt
                target  <- reify target
                let mkN (WithHiding Hiding
    h Name
    x) = Hiding -> NamedArg Binder -> NamedArg Binder
    forall a. LensHiding a => Hiding -> a -> a
    setHiding Hiding
    h (NamedArg Binder -> NamedArg Binder)
    -> NamedArg Binder -> NamedArg Binder
    forall a b. (a -> b) -> a -> b
    $ Binder -> NamedArg Binder
    forall a. a -> NamedArg a
    defaultNamedArg (Binder -> NamedArg Binder) -> Binder -> NamedArg Binder
    forall a b. (a -> b) -> a -> b
    $ Name -> Binder
    A.mkBinder_ Name
    x
                    bs = Range -> NonEmpty (NamedArg Binder) -> Expr -> TypedBinding
    mkTBind Range
    forall a. Range' a
    noRange ((WithHiding Name -> NamedArg Binder)
    -> List1 (WithHiding Name) -> NonEmpty (NamedArg Binder)
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap WithHiding Name -> NamedArg Binder
    mkN List1 (WithHiding Name)
    xs) Expr
    domType
                    e  = ExprInfo -> LamBinding -> Expr -> Expr
    A.Lam ExprInfo
    Info.exprNoRange (TypedBinding -> LamBinding
    DomainFull TypedBinding
    bs) Expr
    body
                return $ TypedAssign m' e target
              CheckArgs Comparison
    _ ExpandHidden
    _ Expr
    _ [NamedArg Expr]
    args Type
    t0 Type
    t1 ArgsCheckState CheckedTarget -> TCM Term
    _ -> do
                t0 <- Type -> m (ReifiesTo Type)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
    reify Type
    t0
                t1 <- reify t1
                return $ PostponedCheckArgs m' (map (namedThing . unArg) args) t0 t1
              CheckProjAppToKnownPrincipalArg Comparison
    cmp Expr
    e ProjOrigin
    _ List1 QName
    _ Expr
    _ [NamedArg Expr]
    _ Type
    t Int
    _ Term
    _ Type
    _ PrincipalArgTypeMetas
    _ -> Expr -> Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr
    forall tcErr a b. b -> a -> a -> OutputConstraint_boot tcErr a b
    TypedAssign Expr
    m' Expr
    e (Expr -> OutputConstraint_boot TCErr Expr Expr)
    -> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> m (ReifiesTo Type)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
    reify Type
    t
              DoQuoteTerm Comparison
    cmp Term
    v Type
    t -> do
                tm <- AppInfo -> Expr -> NamedArg Expr -> Expr
    A.App AppInfo
    defaultAppInfo_ (ExprInfo -> Expr
    A.QuoteTerm ExprInfo
    exprNoRange) (NamedArg Expr -> Expr) -> (Expr -> NamedArg Expr) -> Expr -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Expr -> NamedArg Expr
    forall a. a -> NamedArg a
    defaultNamedArg (Expr -> Expr) -> m Expr -> m Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify Term
    v
                OfType tm <$> reify t
              DisambiguateConstructor (ConstructorDisambiguationData QName
    c0 List1 (QName, Type, ConHead)
    _cands [NamedArg Expr]
    args Type
    t) ConHead -> TCM Term
    _cont -> do
                t <- Type -> m (ReifiesTo Type)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
    reify Type
    t
                return $ TypedAssign m' (foldl (A.App empty)  (A.Con $ unambiguous c0) args) t
            OpenMeta{}  -> m (OutputConstraint_boot TCErr Expr Expr)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            InstV{} -> m (OutputConstraint_boot TCErr Expr Expr)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      reify (FindInstance Range
    _ MetaId
    m Maybe [Candidate]
    mcands) = Expr
    -> Expr
    -> [(Expr, Expr, Expr)]
    -> OutputConstraint_boot TCErr Expr Expr
    forall tcErr a b.
    b -> a -> [(a, a, a)] -> OutputConstraint_boot tcErr a b
    FindInstanceOF
        (Expr
     -> Expr
     -> [(Expr, Expr, Expr)]
     -> OutputConstraint_boot TCErr Expr Expr)
    -> m Expr
    -> m (Expr
          -> [(Expr, Expr, Expr)] -> OutputConstraint_boot TCErr Expr Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify (MetaId -> Elims -> Term
    MetaV MetaId
    m [])
        m (Expr
       -> [(Expr, Expr, Expr)] -> OutputConstraint_boot TCErr Expr Expr)
    -> m Expr
    -> m ([(Expr, Expr, Expr)]
          -> OutputConstraint_boot TCErr Expr Expr)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Type -> m Expr
    Type -> m (ReifiesTo Type)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
    reify (Type -> m Expr) -> m Type -> m Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< MetaId -> m Type
    forall (m :: * -> *). ReadTCState m => MetaId -> m Type
    getMetaType MetaId
    m)
        m ([(Expr, Expr, Expr)] -> OutputConstraint_boot TCErr Expr Expr)
    -> m [(Expr, Expr, Expr)]
    -> m (OutputConstraint_boot TCErr Expr Expr)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [Candidate]
    -> (Candidate -> m (Expr, Expr, Expr)) -> m [(Expr, Expr, Expr)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM ([Candidate] -> Maybe [Candidate] -> [Candidate]
    forall a. a -> Maybe a -> a
    fromMaybe [] Maybe [Candidate]
    mcands) (\ (Candidate CandidateKind
    q Term
    tm Type
    ty OverlapMode
    _) -> do
              (,,) (Expr -> Expr -> Expr -> (Expr, Expr, Expr))
    -> m Expr -> m (Expr -> Expr -> (Expr, Expr, Expr))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify Term
    tm m (Expr -> Expr -> (Expr, Expr, Expr))
    -> m Expr -> m (Expr -> (Expr, Expr, Expr))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify Term
    tm m (Expr -> (Expr, Expr, Expr)) -> m Expr -> m (Expr, Expr, Expr)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Type -> m (ReifiesTo Type)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
    reify Type
    ty)
      reify (ResolveInstanceHead QName
    q) = ReifiesTo Constraint -> m (ReifiesTo Constraint)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ReifiesTo Constraint -> m (ReifiesTo Constraint))
    -> ReifiesTo Constraint -> m (ReifiesTo Constraint)
    forall a b. (a -> b) -> a -> b
    $ QName -> OutputConstraint_boot TCErr Expr Expr
    forall tcErr a b. QName -> OutputConstraint_boot tcErr a b
    ResolveInstanceOF QName
    q
      reify (IsEmpty Range
    r Type
    a) = Expr -> OutputConstraint_boot TCErr Expr Expr
    forall tcErr a b. a -> OutputConstraint_boot tcErr a b
    IsEmptyType (Expr -> OutputConstraint_boot TCErr Expr Expr)
    -> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> m (ReifiesTo Type)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
    reify Type
    a
      reify (CheckSizeLtSat Term
    a) = Expr -> OutputConstraint_boot TCErr Expr Expr
    forall tcErr a b. a -> OutputConstraint_boot tcErr a b
    SizeLtSat  (Expr -> OutputConstraint_boot TCErr Expr Expr)
    -> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify Term
    a
      reify (CheckFunDef DefInfo
    i QName
    q [Clause]
    cs TCErr
    err) = do
        a <- Type -> m Expr
    Type -> m (ReifiesTo Type)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
    reify (Type -> m Expr) -> m Type -> m Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Definition -> Type
    defType (Definition -> Type) -> m Definition -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
        return $ PostponedCheckFunDef q a err
      reify (HasBiggerSort Sort
    a) = Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr
    forall tcErr a b. b -> a -> OutputConstraint_boot tcErr a b
    OfType (Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
    -> m Expr -> m (Expr -> OutputConstraint_boot TCErr Expr Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Sort -> m (ReifiesTo Sort)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Sort -> m (ReifiesTo Sort)
    reify Sort
    a m (Expr -> OutputConstraint_boot TCErr Expr Expr)
    -> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Sort -> m (ReifiesTo Sort)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Sort -> m (ReifiesTo Sort)
    reify (Sort -> Sort
    forall t. Sort' t -> Sort' t
    UnivSort Sort
    a)
      reify (HasPTSRule Dom Type
    a Abs Sort
    b) = do
        (a,(x,b)) <- (Type, Abs Sort) -> m (ReifiesTo (Type, Abs Sort))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    (Type, Abs Sort) -> m (ReifiesTo (Type, Abs Sort))
    reify (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    a,Abs Sort
    b)
        return $ PTSInstance a b
      reify (CheckDataSort QName
    q Sort
    s) = QName -> Expr -> OutputConstraint_boot TCErr Expr Expr
    forall tcErr a b. QName -> b -> OutputConstraint_boot tcErr a b
    DataSort QName
    q (Expr -> OutputConstraint_boot TCErr Expr Expr)
    -> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Sort -> m (ReifiesTo Sort)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Sort -> m (ReifiesTo Sort)
    reify Sort
    s
      reify (CheckLockedVars Term
    t Type
    _ Arg Term
    lk Type
    _) = Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr
    forall tcErr a b. b -> b -> OutputConstraint_boot tcErr a b
    CheckLock (Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
    -> m Expr -> m (Expr -> OutputConstraint_boot TCErr Expr Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify Term
    t m (Expr -> OutputConstraint_boot TCErr Expr Expr)
    -> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    lk)
      reify (CheckMetaInst MetaId
    m) = do
        t <- Judgement MetaId -> Type
    forall a. Judgement a -> Type
    jMetaType (Judgement MetaId -> Type)
    -> (MetaVariable -> Judgement MetaId) -> MetaVariable -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MetaVariable -> Judgement MetaId
    mvJudgement (MetaVariable -> Type) -> m MetaVariable -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> m MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    m
        OfType <$> reify (MetaV m []) <*> reify t
      reify (CheckType Type
    t) = Expr -> OutputConstraint_boot TCErr Expr Expr
    forall tcErr a b. b -> OutputConstraint_boot tcErr a b
    JustType (Expr -> OutputConstraint_boot TCErr Expr Expr)
    -> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> m (ReifiesTo Type)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
    reify Type
    t
      reify (UsableAtModality WhyCheckModality
    _ Maybe Sort
    _ Modality
    mod Term
    t) = Modality -> Expr -> OutputConstraint_boot TCErr Expr Expr
    forall tcErr a b. Modality -> b -> OutputConstraint_boot tcErr a b
    UsableAtMod Modality
    mod (Expr -> OutputConstraint_boot TCErr Expr Expr)
    -> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify Term
    t
      {-# SPECIALIZE reify :: Constraint -> TCM (ReifiesTo Constraint) #-}

    instance (Pretty a, Pretty b) => PrettyTCM (OutputForm a b) where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => OutputForm a b -> m Doc
    prettyTCM (OutputForm Range
    r [ProblemId]
    pids Blocker
    unblock OutputConstraint_boot TCErr a b
    c) =
        Range -> [ProblemId] -> Blocker -> Doc -> m Doc
    forall (m :: * -> *) (f :: * -> *).
    (MonadPretty m, Foldable f, Null (f ProblemId)) =>
    Range -> f ProblemId -> Blocker -> Doc -> m Doc
    prettyRangeConstraint Range
    r [ProblemId]
    pids Blocker
    unblock (OutputConstraint_boot TCErr a b -> Doc
    forall a. Pretty a => a -> Doc
    pretty OutputConstraint_boot TCErr a b
    c)
      {-# SPECIALIZE prettyTCM :: (Pretty a, Pretty b) => (OutputForm a b) -> TCM Doc #-}

    instance (Pretty a, Pretty b) => Pretty (OutputForm a b) where
      pretty :: OutputForm a b -> Doc
    pretty (OutputForm Range
    r [ProblemId]
    pids Blocker
    unblock OutputConstraint_boot TCErr a b
    c) =
        OutputConstraint_boot TCErr a b -> Doc
    forall a. Pretty a => a -> Doc
    pretty OutputConstraint_boot TCErr a b
    c Doc -> Doc -> Doc
    <?>
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Range -> Doc
    forall {a} {a}. Pretty a => a -> Doc a
    prange Range
    r, Doc -> Doc
    parensNonEmpty ([Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [Blocker -> Doc
    blockedOn Blocker
    unblock, [ProblemId] -> Doc
    forall {a}. Pretty a => [a] -> Doc
    prPids [ProblemId]
    pids]) ]
        where
          prPids :: [a] -> Doc
    prPids []    = Doc
    forall a. Null a => a
    empty
          prPids [a
    pid] = Doc
    "belongs to problem" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    pid
          prPids [a]
    pids  = Doc
    "belongs to problems" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep (Doc -> [Doc] -> [Doc]
    forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
    punctuate Doc
    "," ([Doc] -> [Doc]) -> [Doc] -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ (a -> Doc) -> [a] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Doc
    forall a. Pretty a => a -> Doc
    pretty [a]
    pids)

          comma :: Doc
    comma | [ProblemId] -> Bool
    forall a. Null a => a -> Bool
    null [ProblemId]
    pids = Doc
    forall a. Null a => a
    empty
                | Bool
    otherwise = Doc
    ","

          blockedOn :: Blocker -> Doc
    blockedOn (UnblockOnAll Set Blocker
    bs) | Set Blocker -> Bool
    forall a. Set a -> Bool
    Set.null Set Blocker
    bs = Doc
    forall a. Null a => a
    empty
          blockedOn (UnblockOnAny Set Blocker
    bs) | Set Blocker -> Bool
    forall a. Set a -> Bool
    Set.null Set Blocker
    bs = Doc
    "stuck" Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    P.<> Doc
    comma
          blockedOn Blocker
    u = Doc
    "blocked on" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> (Blocker -> Doc
    forall a. Pretty a => a -> Doc
    pretty Blocker
    u Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    P.<> Doc
    comma)

          prange :: a -> Doc a
    prange a
    r | ArgName -> Bool
    forall a. Null a => a -> Bool
    null ArgName
    s = Doc a
    forall a. Null a => a
    empty
                   | Bool
    otherwise = ArgName -> Doc a
    forall a. ArgName -> Doc a
    text (ArgName -> Doc a) -> ArgName -> Doc a
    forall a b. (a -> b) -> a -> b
    $ ArgName
    " [ at " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ ArgName
    s ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ ArgName
    " ]"
            where s :: ArgName
    s = a -> ArgName
    forall a. Pretty a => a -> ArgName
    prettyShow a
    r

    instance (Pretty a, Pretty b) => Pretty (OutputConstraint a b) where
      pretty :: OutputConstraint a b -> Doc
    pretty OutputConstraint a b
    oc =
        case OutputConstraint a b
    oc of
          OfType b
    e a
    t           -> b -> Doc
    forall a. Pretty a => a -> Doc
    pretty b
    e Doc -> a -> Doc
    forall {a}. Pretty a => Doc -> a -> Doc
    .: a
    t
          JustType b
    e           -> Doc
    "Type" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> b -> Doc
    forall a. Pretty a => a -> Doc
    pretty b
    e
          JustSort b
    e           -> Doc
    "Sort" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> b -> Doc
    forall a. Pretty a => a -> Doc
    pretty b
    e
          CmpInType Comparison
    cmp a
    t b
    e b
    e' -> Comparison -> b -> b -> Doc
    forall {a} {a} {a}.
    (Pretty a, Pretty a, Pretty a) =>
    a -> a -> a -> Doc
    pcmp Comparison
    cmp b
    e b
    e' Doc -> a -> Doc
    forall {a}. Pretty a => Doc -> a -> Doc
    .: a
    t
          CmpElim [Polarity]
    cmp a
    t [b]
    e [b]
    e'   -> [Polarity] -> [b] -> [b] -> Doc
    forall {a} {a} {a}.
    (Pretty a, Pretty a, Pretty a) =>
    a -> a -> a -> Doc
    pcmp [Polarity]
    cmp [b]
    e [b]
    e' Doc -> a -> Doc
    forall {a}. Pretty a => Doc -> a -> Doc
    .: a
    t
          CmpTypes  Comparison
    cmp b
    t b
    t'   -> Comparison -> b -> b -> Doc
    forall {a} {a} {a}.
    (Pretty a, Pretty a, Pretty a) =>
    a -> a -> a -> Doc
    pcmp Comparison
    cmp b
    t b
    t'
          CmpLevels Comparison
    cmp b
    t b
    t'   -> Comparison -> b -> b -> Doc
    forall {a} {a} {a}.
    (Pretty a, Pretty a, Pretty a) =>
    a -> a -> a -> Doc
    pcmp Comparison
    cmp b
    t b
    t'
          CmpTeles  Comparison
    cmp b
    t b
    t'   -> Comparison -> b -> b -> Doc
    forall {a} {a} {a}.
    (Pretty a, Pretty a, Pretty a) =>
    a -> a -> a -> Doc
    pcmp Comparison
    cmp b
    t b
    t'
          CmpSorts Comparison
    cmp b
    s b
    s'    -> Comparison -> b -> b -> Doc
    forall {a} {a} {a}.
    (Pretty a, Pretty a, Pretty a) =>
    a -> a -> a -> Doc
    pcmp Comparison
    cmp b
    s b
    s'
          Assign b
    m a
    e           -> Doc -> Doc -> Doc -> Doc
    bin (b -> Doc
    forall a. Pretty a => a -> Doc
    pretty b
    m) Doc
    ":=" (a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    e)
          TypedAssign b
    m a
    e a
    a    -> Doc -> Doc -> Doc -> Doc
    bin (b -> Doc
    forall a. Pretty a => a -> Doc
    pretty b
    m) Doc
    ":=" (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc -> Doc -> Doc -> Doc
    bin (a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    e) Doc
    ":?" (a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    a)
          PostponedCheckArgs b
    m [a]
    es a
    t0 a
    t1 ->
            Doc -> Doc -> Doc -> Doc
    bin (b -> Doc
    forall a. Pretty a => a -> Doc
    pretty b
    m) Doc
    ":=" (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Doc -> Doc
    parens (Doc
    "_" Doc -> a -> Doc
    forall {a}. Pretty a => Doc -> a -> Doc
    .: a
    t0) Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ((a -> Doc) -> [a] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Doc -> Doc
    paren (Doc -> Doc) -> (a -> Doc) -> a -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Doc
    forall a. Pretty a => a -> Doc
    pretty) [a]
    es)) Doc -> a -> Doc
    forall {a}. Pretty a => Doc -> a -> Doc
    .: a
    t1
            where paren :: Doc -> Doc
    paren Doc
    d = Bool -> Doc -> Doc
    mparens ((Char -> Bool) -> ArgName -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (Char -> ArgName -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Char
    ' ', Char
    '\n']) (ArgName -> Bool) -> ArgName -> Bool
    forall a b. (a -> b) -> a -> b
    $ Doc -> ArgName
    forall a. Show a => a -> ArgName
    show Doc
    d) Doc
    d
          IsEmptyType a
    a        -> Doc
    "Is empty:" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    a
          SizeLtSat a
    a          -> Doc
    "Not empty type of sizes:" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    a
          FindInstanceOF b
    s a
    t [(a, a, a)]
    cs -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat
            [ Doc
    "Resolve instance argument" Doc -> Doc -> Doc
    <?> (b -> Doc
    forall a. Pretty a => a -> Doc
    pretty b
    s Doc -> a -> Doc
    forall {a}. Pretty a => Doc -> a -> Doc
    .: a
    t)
            , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "Candidate:"
            , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    4 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat [ Doc -> Doc -> Doc -> Doc
    bin (a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    q) Doc
    "=" (a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    v) Doc -> a -> Doc
    forall {a}. Pretty a => Doc -> a -> Doc
    .: a
    t | (a
    q, a
    v, a
    t) <- [(a, a, a)]
    cs ] ]
          ResolveInstanceOF QName
    q ->
            Doc
    "Resolve output type of instance" Doc -> Doc -> Doc
    <?> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    q
          PTSInstance b
    a b
    b      -> Doc
    "PTS instance for" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> (b, b) -> Doc
    forall a. Pretty a => a -> Doc
    pretty (b
    a, b
    b)
          PostponedCheckFunDef QName
    q a
    a TCErr
    _err ->
            [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat [ Doc
    "Check definition of" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    q Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    ":" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    a ]
                 -- , nest 2 "stuck because" <?> pretty err ] -- We don't have Pretty for TCErr
          DataSort QName
    q b
    s         -> Doc
    "Sort" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> b -> Doc
    forall a. Pretty a => a -> Doc
    pretty b
    s Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    "allows data/record definitions"
          CheckLock b
    t b
    lk       -> Doc
    "Check lock" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> b -> Doc
    forall a. Pretty a => a -> Doc
    pretty b
    lk Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    "allows" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> b -> Doc
    forall a. Pretty a => a -> Doc
    pretty b
    t
          UsableAtMod Modality
    mod b
    t    -> Doc
    "Is usable at" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> ArgName -> Doc
    forall a. ArgName -> Doc a
    text (Modality -> ArgName
    forall a. Verbalize a => a -> ArgName
    verbalize Modality
    mod) Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    "modality:" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> b -> Doc
    forall a. Pretty a => a -> Doc
    pretty b
    t
        where
          bin :: Doc -> Doc -> Doc -> Doc
    bin Doc
    a Doc
    op Doc
    b = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [Doc
    a, Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    op Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    b]
          pcmp :: a -> a -> a -> Doc
    pcmp a
    cmp a
    a a
    b = Doc -> Doc -> Doc -> Doc
    bin (a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    a) (a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    cmp) (a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    b)
          Doc
    val .: :: Doc -> a -> Doc
    .: a
    ty = Doc -> Doc -> Doc -> Doc
    bin Doc
    val Doc
    ":" (a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    ty)

    instance (ToConcrete a, ToConcrete b) => ToConcrete (OutputForm a b) where
        type ConOfAbs (OutputForm a b) = OutputForm (ConOfAbs a) (ConOfAbs b)
        toConcrete :: forall (m :: * -> *).
    MonadToConcrete m =>
    OutputForm a b -> m (ConOfAbs (OutputForm a b))
    toConcrete (OutputForm Range
    r [ProblemId]
    pid Blocker
    u OutputConstraint_boot TCErr a b
    c) = Range
    -> [ProblemId]
    -> Blocker
    -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
    -> OutputForm_boot TCErr (ConOfAbs a) (ConOfAbs b)
    forall tcErr a b.
    Range
    -> [ProblemId]
    -> Blocker
    -> OutputConstraint_boot tcErr a b
    -> OutputForm_boot tcErr a b
    OutputForm Range
    r [ProblemId]
    pid Blocker
    u (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
     -> OutputForm_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (OutputForm_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> OutputConstraint_boot TCErr a b
    -> m (ConOfAbs (OutputConstraint_boot TCErr a b))
    forall a (m :: * -> *).
    (ToConcrete a, MonadToConcrete m) =>
    a -> m (ConOfAbs a)
    forall (m :: * -> *).
    MonadToConcrete m =>
    OutputConstraint_boot TCErr a b
    -> m (ConOfAbs (OutputConstraint_boot TCErr a b))
    toConcrete OutputConstraint_boot TCErr a b
    c

    instance (ToConcrete a, ToConcrete b) => ToConcrete (OutputConstraint a b) where
        type ConOfAbs (OutputConstraint a b) = OutputConstraint (ConOfAbs a) (ConOfAbs b)

        toConcrete :: forall (m :: * -> *).
    MonadToConcrete m =>
    OutputConstraint a b -> m (ConOfAbs (OutputConstraint a b))
    toConcrete (OfType b
    e a
    t) = ConOfAbs b
    -> ConOfAbs a
    -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
    forall tcErr a b. b -> a -> OutputConstraint_boot tcErr a b
    OfType (ConOfAbs b
     -> ConOfAbs a
     -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs b)
    -> m (ConOfAbs a
          -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> b -> m (ConOfAbs b)
    forall a (m :: * -> *).
    (ToConcrete a, MonadToConcrete m) =>
    a -> m (ConOfAbs a)
    forall (m :: * -> *). MonadToConcrete m => b -> m (ConOfAbs b)
    toConcrete b
    e m (ConOfAbs a
       -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs a)
    -> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Precedence -> a -> m (ConOfAbs a)
    forall (m :: * -> *) a.
    (MonadToConcrete m, ToConcrete a) =>
    Precedence -> a -> m (ConOfAbs a)
    toConcreteCtx Precedence
    TopCtx a
    t
        toConcrete (JustType b
    e) = ConOfAbs b -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
    forall tcErr a b. b -> OutputConstraint_boot tcErr a b
    JustType (ConOfAbs b
     -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs b)
    -> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> b -> m (ConOfAbs b)
    forall a (m :: * -> *).
    (ToConcrete a, MonadToConcrete m) =>
    a -> m (ConOfAbs a)
    forall (m :: * -> *). MonadToConcrete m => b -> m (ConOfAbs b)
    toConcrete b
    e
        toConcrete (JustSort b
    e) = ConOfAbs b -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
    forall tcErr a b. b -> OutputConstraint_boot tcErr a b
    JustSort (ConOfAbs b
     -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs b)
    -> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> b -> m (ConOfAbs b)
    forall a (m :: * -> *).
    (ToConcrete a, MonadToConcrete m) =>
    a -> m (ConOfAbs a)
    forall (m :: * -> *). MonadToConcrete m => b -> m (ConOfAbs b)
    toConcrete b
    e
        toConcrete (CmpInType Comparison
    cmp a
    t b
    e b
    e') =
          Comparison
    -> ConOfAbs a
    -> ConOfAbs b
    -> ConOfAbs b
    -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
    forall tcErr a b.
    Comparison -> a -> b -> b -> OutputConstraint_boot tcErr a b
    CmpInType Comparison
    cmp (ConOfAbs a
     -> ConOfAbs b
     -> ConOfAbs b
     -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs a)
    -> m (ConOfAbs b
          -> ConOfAbs b
          -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Precedence -> a -> m (ConOfAbs a)
    forall (m :: * -> *) a.
    (MonadToConcrete m, ToConcrete a) =>
    Precedence -> a -> m (ConOfAbs a)
    toConcreteCtx Precedence
    TopCtx a
    t m (ConOfAbs b
       -> ConOfAbs b
       -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs b)
    -> m (ConOfAbs b
          -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Precedence -> b -> m (ConOfAbs b)
    forall (m :: * -> *) a.
    (MonadToConcrete m, ToConcrete a) =>
    Precedence -> a -> m (ConOfAbs a)
    toConcreteCtx Precedence
    TopCtx b
    e
                                                   m (ConOfAbs b
       -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs b)
    -> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Precedence -> b -> m (ConOfAbs b)
    forall (m :: * -> *) a.
    (MonadToConcrete m, ToConcrete a) =>
    Precedence -> a -> m (ConOfAbs a)
    toConcreteCtx Precedence
    TopCtx b
    e'
        toConcrete (CmpElim [Polarity]
    cmp a
    t [b]
    e [b]
    e') =
          [Polarity]
    -> ConOfAbs a
    -> [ConOfAbs b]
    -> [ConOfAbs b]
    -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
    forall tcErr a b.
    [Polarity] -> a -> [b] -> [b] -> OutputConstraint_boot tcErr a b
    CmpElim [Polarity]
    cmp (ConOfAbs a
     -> [ConOfAbs b]
     -> [ConOfAbs b]
     -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs a)
    -> m ([ConOfAbs b]
          -> [ConOfAbs b]
          -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Precedence -> a -> m (ConOfAbs a)
    forall (m :: * -> *) a.
    (MonadToConcrete m, ToConcrete a) =>
    Precedence -> a -> m (ConOfAbs a)
    toConcreteCtx Precedence
    TopCtx a
    t m ([ConOfAbs b]
       -> [ConOfAbs b]
       -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m [ConOfAbs b]
    -> m ([ConOfAbs b]
          -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Precedence -> [b] -> m (ConOfAbs [b])
    forall (m :: * -> *) a.
    (MonadToConcrete m, ToConcrete a) =>
    Precedence -> a -> m (ConOfAbs a)
    toConcreteCtx Precedence
    TopCtx [b]
    e m ([ConOfAbs b]
       -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m [ConOfAbs b]
    -> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Precedence -> [b] -> m (ConOfAbs [b])
    forall (m :: * -> *) a.
    (MonadToConcrete m, ToConcrete a) =>
    Precedence -> a -> m (ConOfAbs a)
    toConcreteCtx Precedence
    TopCtx [b]
    e'
        toConcrete (CmpTypes Comparison
    cmp b
    e b
    e') = Comparison
    -> ConOfAbs b
    -> ConOfAbs b
    -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
    forall tcErr a b.
    Comparison -> b -> b -> OutputConstraint_boot tcErr a b
    CmpTypes Comparison
    cmp (ConOfAbs b
     -> ConOfAbs b
     -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs b)
    -> m (ConOfAbs b
          -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Precedence -> b -> m (ConOfAbs b)
    forall (m :: * -> *) a.
    (MonadToConcrete m, ToConcrete a) =>
    Precedence -> a -> m (ConOfAbs a)
    toConcreteCtx Precedence
    TopCtx b
    e
                                                      m (ConOfAbs b
       -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs b)
    -> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Precedence -> b -> m (ConOfAbs b)
    forall (m :: * -> *) a.
    (MonadToConcrete m, ToConcrete a) =>
    Precedence -> a -> m (ConOfAbs a)
    toConcreteCtx Precedence
    TopCtx b
    e'
        toConcrete (CmpLevels Comparison
    cmp b
    e b
    e') = Comparison
    -> ConOfAbs b
    -> ConOfAbs b
    -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
    forall tcErr a b.
    Comparison -> b -> b -> OutputConstraint_boot tcErr a b
    CmpLevels Comparison
    cmp (ConOfAbs b
     -> ConOfAbs b
     -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs b)
    -> m (ConOfAbs b
          -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Precedence -> b -> m (ConOfAbs b)
    forall (m :: * -> *) a.
    (MonadToConcrete m, ToConcrete a) =>
    Precedence -> a -> m (ConOfAbs a)
    toConcreteCtx Precedence
    TopCtx b
    e
                                                        m (ConOfAbs b
       -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs b)
    -> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Precedence -> b -> m (ConOfAbs b)
    forall (m :: * -> *) a.
    (MonadToConcrete m, ToConcrete a) =>
    Precedence -> a -> m (ConOfAbs a)
    toConcreteCtx Precedence
    TopCtx b
    e'
        toConcrete (CmpTeles Comparison
    cmp b
    e b
    e') = Comparison
    -> ConOfAbs b
    -> ConOfAbs b
    -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
    forall tcErr a b.
    Comparison -> b -> b -> OutputConstraint_boot tcErr a b
    CmpTeles Comparison
    cmp (ConOfAbs b
     -> ConOfAbs b
     -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs b)
    -> m (ConOfAbs b
          -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> b -> m (ConOfAbs b)
    forall a (m :: * -> *).
    (ToConcrete a, MonadToConcrete m) =>
    a -> m (ConOfAbs a)
    forall (m :: * -> *). MonadToConcrete m => b -> m (ConOfAbs b)
    toConcrete b
    e m (ConOfAbs b
       -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs b)
    -> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> b -> m (ConOfAbs b)
    forall a (m :: * -> *).
    (ToConcrete a, MonadToConcrete m) =>
    a -> m (ConOfAbs a)
    forall (m :: * -> *). MonadToConcrete m => b -> m (ConOfAbs b)
    toConcrete b
    e'
        toConcrete (CmpSorts Comparison
    cmp b
    e b
    e') = Comparison
    -> ConOfAbs b
    -> ConOfAbs b
    -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
    forall tcErr a b.
    Comparison -> b -> b -> OutputConstraint_boot tcErr a b
    CmpSorts Comparison
    cmp (ConOfAbs b
     -> ConOfAbs b
     -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs b)
    -> m (ConOfAbs b
          -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Precedence -> b -> m (ConOfAbs b)
    forall (m :: * -> *) a.
    (MonadToConcrete m, ToConcrete a) =>
    Precedence -> a -> m (ConOfAbs a)
    toConcreteCtx Precedence
    TopCtx b
    e
                                                      m (ConOfAbs b
       -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs b)
    -> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Precedence -> b -> m (ConOfAbs b)
    forall (m :: * -> *) a.
    (MonadToConcrete m, ToConcrete a) =>
    Precedence -> a -> m (ConOfAbs a)
    toConcreteCtx Precedence
    TopCtx b
    e'
        toConcrete (Assign b
    m a
    e) = m (ConOfAbs (OutputConstraint a b))
    -> m (ConOfAbs (OutputConstraint a b))
    forall (m :: * -> *) a. MonadToConcrete m => m a -> m a
    noTakenNames (m (ConOfAbs (OutputConstraint a b))
     -> m (ConOfAbs (OutputConstraint a b)))
    -> m (ConOfAbs (OutputConstraint a b))
    -> m (ConOfAbs (OutputConstraint a b))
    forall a b. (a -> b) -> a -> b
    $ ConOfAbs b
    -> ConOfAbs a
    -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
    forall tcErr a b. b -> a -> OutputConstraint_boot tcErr a b
    Assign (ConOfAbs b
     -> ConOfAbs a
     -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs b)
    -> m (ConOfAbs a
          -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> b -> m (ConOfAbs b)
    forall a (m :: * -> *).
    (ToConcrete a, MonadToConcrete m) =>
    a -> m (ConOfAbs a)
    forall (m :: * -> *). MonadToConcrete m => b -> m (ConOfAbs b)
    toConcrete b
    m m (ConOfAbs a
       -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs a)
    -> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Precedence -> a -> m (ConOfAbs a)
    forall (m :: * -> *) a.
    (MonadToConcrete m, ToConcrete a) =>
    Precedence -> a -> m (ConOfAbs a)
    toConcreteCtx Precedence
    TopCtx a
    e
        toConcrete (TypedAssign b
    m a
    e a
    a) = ConOfAbs b
    -> ConOfAbs a
    -> ConOfAbs a
    -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
    forall tcErr a b. b -> a -> a -> OutputConstraint_boot tcErr a b
    TypedAssign (ConOfAbs b
     -> ConOfAbs a
     -> ConOfAbs a
     -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs b)
    -> m (ConOfAbs a
          -> ConOfAbs a
          -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> b -> m (ConOfAbs b)
    forall a (m :: * -> *).
    (ToConcrete a, MonadToConcrete m) =>
    a -> m (ConOfAbs a)
    forall (m :: * -> *). MonadToConcrete m => b -> m (ConOfAbs b)
    toConcrete b
    m m (ConOfAbs a
       -> ConOfAbs a
       -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs a)
    -> m (ConOfAbs a
          -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Precedence -> a -> m (ConOfAbs a)
    forall (m :: * -> *) a.
    (MonadToConcrete m, ToConcrete a) =>
    Precedence -> a -> m (ConOfAbs a)
    toConcreteCtx Precedence
    TopCtx a
    e
                                                                      m (ConOfAbs a
       -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs a)
    -> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Precedence -> a -> m (ConOfAbs a)
    forall (m :: * -> *) a.
    (MonadToConcrete m, ToConcrete a) =>
    Precedence -> a -> m (ConOfAbs a)
    toConcreteCtx Precedence
    TopCtx a
    a
        toConcrete (PostponedCheckArgs b
    m [a]
    args a
    t0 a
    t1) =
          ConOfAbs b
    -> [ConOfAbs a]
    -> ConOfAbs a
    -> ConOfAbs a
    -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
    forall tcErr a b.
    b -> [a] -> a -> a -> OutputConstraint_boot tcErr a b
    PostponedCheckArgs (ConOfAbs b
     -> [ConOfAbs a]
     -> ConOfAbs a
     -> ConOfAbs a
     -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs b)
    -> m ([ConOfAbs a]
          -> ConOfAbs a
          -> ConOfAbs a
          -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> b -> m (ConOfAbs b)
    forall a (m :: * -> *).
    (ToConcrete a, MonadToConcrete m) =>
    a -> m (ConOfAbs a)
    forall (m :: * -> *). MonadToConcrete m => b -> m (ConOfAbs b)
    toConcrete b
    m m ([ConOfAbs a]
       -> ConOfAbs a
       -> ConOfAbs a
       -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m [ConOfAbs a]
    -> m (ConOfAbs a
          -> ConOfAbs a
          -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [a] -> m (ConOfAbs [a])
    forall a (m :: * -> *).
    (ToConcrete a, MonadToConcrete m) =>
    a -> m (ConOfAbs a)
    forall (m :: * -> *). MonadToConcrete m => [a] -> m (ConOfAbs [a])
    toConcrete [a]
    args m (ConOfAbs a
       -> ConOfAbs a
       -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs a)
    -> m (ConOfAbs a
          -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> a -> m (ConOfAbs a)
    forall a (m :: * -> *).
    (ToConcrete a, MonadToConcrete m) =>
    a -> m (ConOfAbs a)
    forall (m :: * -> *). MonadToConcrete m => a -> m (ConOfAbs a)
    toConcrete a
    t0 m (ConOfAbs a
       -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs a)
    -> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> a -> m (ConOfAbs a)
    forall a (m :: * -> *).
    (ToConcrete a, MonadToConcrete m) =>
    a -> m (ConOfAbs a)
    forall (m :: * -> *). MonadToConcrete m => a -> m (ConOfAbs a)
    toConcrete a
    t1
        toConcrete (IsEmptyType a
    a) = ConOfAbs a -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
    forall tcErr a b. a -> OutputConstraint_boot tcErr a b
    IsEmptyType (ConOfAbs a
     -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs a)
    -> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Precedence -> a -> m (ConOfAbs a)
    forall (m :: * -> *) a.
    (MonadToConcrete m, ToConcrete a) =>
    Precedence -> a -> m (ConOfAbs a)
    toConcreteCtx Precedence
    TopCtx a
    a
        toConcrete (SizeLtSat a
    a) = ConOfAbs a -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
    forall tcErr a b. a -> OutputConstraint_boot tcErr a b
    SizeLtSat (ConOfAbs a
     -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs a)
    -> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Precedence -> a -> m (ConOfAbs a)
    forall (m :: * -> *) a.
    (MonadToConcrete m, ToConcrete a) =>
    Precedence -> a -> m (ConOfAbs a)
    toConcreteCtx Precedence
    TopCtx a
    a
        toConcrete (FindInstanceOF b
    s a
    t [(a, a, a)]
    cs) =
          ConOfAbs b
    -> ConOfAbs a
    -> [(ConOfAbs a, ConOfAbs a, ConOfAbs a)]
    -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
    forall tcErr a b.
    b -> a -> [(a, a, a)] -> OutputConstraint_boot tcErr a b
    FindInstanceOF (ConOfAbs b
     -> ConOfAbs a
     -> [(ConOfAbs a, ConOfAbs a, ConOfAbs a)]
     -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs b)
    -> m (ConOfAbs a
          -> [(ConOfAbs a, ConOfAbs a, ConOfAbs a)]
          -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> b -> m (ConOfAbs b)
    forall a (m :: * -> *).
    (ToConcrete a, MonadToConcrete m) =>
    a -> m (ConOfAbs a)
    forall (m :: * -> *). MonadToConcrete m => b -> m (ConOfAbs b)
    toConcrete b
    s m (ConOfAbs a
       -> [(ConOfAbs a, ConOfAbs a, ConOfAbs a)]
       -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs a)
    -> m ([(ConOfAbs a, ConOfAbs a, ConOfAbs a)]
          -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> a -> m (ConOfAbs a)
    forall a (m :: * -> *).
    (ToConcrete a, MonadToConcrete m) =>
    a -> m (ConOfAbs a)
    forall (m :: * -> *). MonadToConcrete m => a -> m (ConOfAbs a)
    toConcrete a
    t
                         m ([(ConOfAbs a, ConOfAbs a, ConOfAbs a)]
       -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m [(ConOfAbs a, ConOfAbs a, ConOfAbs a)]
    -> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> ((a, a, a) -> m (ConOfAbs a, ConOfAbs a, ConOfAbs a))
    -> [(a, a, a)] -> m [(ConOfAbs a, ConOfAbs a, ConOfAbs a)]
    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 (\(a
    q,a
    tm,a
    ty) -> (,,) (ConOfAbs a
     -> ConOfAbs a
     -> ConOfAbs a
     -> (ConOfAbs a, ConOfAbs a, ConOfAbs a))
    -> m (ConOfAbs a)
    -> m (ConOfAbs a
          -> ConOfAbs a -> (ConOfAbs a, ConOfAbs a, ConOfAbs a))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> m (ConOfAbs a)
    forall a (m :: * -> *).
    (ToConcrete a, MonadToConcrete m) =>
    a -> m (ConOfAbs a)
    forall (m :: * -> *). MonadToConcrete m => a -> m (ConOfAbs a)
    toConcrete a
    q m (ConOfAbs a
       -> ConOfAbs a -> (ConOfAbs a, ConOfAbs a, ConOfAbs a))
    -> m (ConOfAbs a)
    -> m (ConOfAbs a -> (ConOfAbs a, ConOfAbs a, ConOfAbs a))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> a -> m (ConOfAbs a)
    forall a (m :: * -> *).
    (ToConcrete a, MonadToConcrete m) =>
    a -> m (ConOfAbs a)
    forall (m :: * -> *). MonadToConcrete m => a -> m (ConOfAbs a)
    toConcrete a
    tm m (ConOfAbs a -> (ConOfAbs a, ConOfAbs a, ConOfAbs a))
    -> m (ConOfAbs a) -> m (ConOfAbs a, ConOfAbs a, ConOfAbs a)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> a -> m (ConOfAbs a)
    forall a (m :: * -> *).
    (ToConcrete a, MonadToConcrete m) =>
    a -> m (ConOfAbs a)
    forall (m :: * -> *). MonadToConcrete m => a -> m (ConOfAbs a)
    toConcrete a
    ty) [(a, a, a)]
    cs
        toConcrete (ResolveInstanceOF QName
    q) = ConOfAbs (OutputConstraint a b)
    -> m (ConOfAbs (OutputConstraint a b))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ConOfAbs (OutputConstraint a b)
     -> m (ConOfAbs (OutputConstraint a b)))
    -> ConOfAbs (OutputConstraint a b)
    -> m (ConOfAbs (OutputConstraint a b))
    forall a b. (a -> b) -> a -> b
    $ QName -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
    forall tcErr a b. QName -> OutputConstraint_boot tcErr a b
    ResolveInstanceOF QName
    q
        toConcrete (PTSInstance b
    a b
    b) = ConOfAbs b
    -> ConOfAbs b
    -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
    forall tcErr a b. b -> b -> OutputConstraint_boot tcErr a b
    PTSInstance (ConOfAbs b
     -> ConOfAbs b
     -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs b)
    -> m (ConOfAbs b
          -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> b -> m (ConOfAbs b)
    forall a (m :: * -> *).
    (ToConcrete a, MonadToConcrete m) =>
    a -> m (ConOfAbs a)
    forall (m :: * -> *). MonadToConcrete m => b -> m (ConOfAbs b)
    toConcrete b
    a m (ConOfAbs b
       -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs b)
    -> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> b -> m (ConOfAbs b)
    forall a (m :: * -> *).
    (ToConcrete a, MonadToConcrete m) =>
    a -> m (ConOfAbs a)
    forall (m :: * -> *). MonadToConcrete m => b -> m (ConOfAbs b)
    toConcrete b
    b
        toConcrete (DataSort QName
    a b
    b)  = QName
    -> ConOfAbs b
    -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
    forall tcErr a b. QName -> b -> OutputConstraint_boot tcErr a b
    DataSort QName
    a (ConOfAbs b
     -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs b)
    -> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> b -> m (ConOfAbs b)
    forall a (m :: * -> *).
    (ToConcrete a, MonadToConcrete m) =>
    a -> m (ConOfAbs a)
    forall (m :: * -> *). MonadToConcrete m => b -> m (ConOfAbs b)
    toConcrete b
    b
        toConcrete (CheckLock b
    a b
    b) = ConOfAbs b
    -> ConOfAbs b
    -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
    forall tcErr a b. b -> b -> OutputConstraint_boot tcErr a b
    CheckLock (ConOfAbs b
     -> ConOfAbs b
     -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs b)
    -> m (ConOfAbs b
          -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> b -> m (ConOfAbs b)
    forall a (m :: * -> *).
    (ToConcrete a, MonadToConcrete m) =>
    a -> m (ConOfAbs a)
    forall (m :: * -> *). MonadToConcrete m => b -> m (ConOfAbs b)
    toConcrete b
    a m (ConOfAbs b
       -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs b)
    -> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> b -> m (ConOfAbs b)
    forall a (m :: * -> *).
    (ToConcrete a, MonadToConcrete m) =>
    a -> m (ConOfAbs a)
    forall (m :: * -> *). MonadToConcrete m => b -> m (ConOfAbs b)
    toConcrete b
    b
        toConcrete (PostponedCheckFunDef QName
    q a
    a TCErr
    err) = QName
    -> ConOfAbs a
    -> TCErr
    -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
    forall tcErr a b.
    QName -> a -> tcErr -> OutputConstraint_boot tcErr a b
    PostponedCheckFunDef QName
    q (ConOfAbs a
     -> TCErr -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs a)
    -> m (TCErr
          -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> m (ConOfAbs a)
    forall a (m :: * -> *).
    (ToConcrete a, MonadToConcrete m) =>
    a -> m (ConOfAbs a)
    forall (m :: * -> *). MonadToConcrete m => a -> m (ConOfAbs a)
    toConcrete a
    a m (TCErr -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m TCErr
    -> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> TCErr -> m TCErr
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TCErr
    err
        toConcrete (UsableAtMod Modality
    a b
    b) = Modality
    -> ConOfAbs b
    -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
    forall tcErr a b. Modality -> b -> OutputConstraint_boot tcErr a b
    UsableAtMod Modality
    a (ConOfAbs b
     -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs b)
    -> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> b -> m (ConOfAbs b)
    forall a (m :: * -> *).
    (ToConcrete a, MonadToConcrete m) =>
    a -> m (ConOfAbs a)
    forall (m :: * -> *). MonadToConcrete m => b -> m (ConOfAbs b)
    toConcrete b
    b

    instance (Pretty a, Pretty b) => Pretty (OutputConstraint' a b) where
      pretty :: OutputConstraint' a b -> Doc
    pretty (OfType' b
    e a
    t) = b -> Doc
    forall a. Pretty a => a -> Doc
    pretty b
    e Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    ":" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    t

    instance (ToConcrete a, ToConcrete b) => ToConcrete (OutputConstraint' a b) where
      type ConOfAbs (OutputConstraint' a b) = OutputConstraint' (ConOfAbs a) (ConOfAbs b)
      toConcrete :: forall (m :: * -> *).
    MonadToConcrete m =>
    OutputConstraint' a b -> m (ConOfAbs (OutputConstraint' a b))
    toConcrete (OfType' b
    e a
    t) = ConOfAbs b
    -> ConOfAbs a -> OutputConstraint' (ConOfAbs a) (ConOfAbs b)
    forall a b. b -> a -> OutputConstraint' a b
    OfType' (ConOfAbs b
     -> ConOfAbs a -> OutputConstraint' (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs b)
    -> m (ConOfAbs a -> OutputConstraint' (ConOfAbs a) (ConOfAbs b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> b -> m (ConOfAbs b)
    forall a (m :: * -> *).
    (ToConcrete a, MonadToConcrete m) =>
    a -> m (ConOfAbs a)
    forall (m :: * -> *). MonadToConcrete m => b -> m (ConOfAbs b)
    toConcrete b
    e m (ConOfAbs a -> OutputConstraint' (ConOfAbs a) (ConOfAbs b))
    -> m (ConOfAbs a)
    -> m (OutputConstraint' (ConOfAbs a) (ConOfAbs b))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Precedence -> a -> m (ConOfAbs a)
    forall (m :: * -> *) a.
    (MonadToConcrete m, ToConcrete a) =>
    Precedence -> a -> m (ConOfAbs a)
    toConcreteCtx Precedence
    TopCtx a
    t

    instance Reify a => Reify (IPBoundary' a) where
      type ReifiesTo (IPBoundary' a) = IPBoundary' (ReifiesTo a)
      reify :: forall (m :: * -> *).
    MonadReify m =>
    IPBoundary' a -> m (ReifiesTo (IPBoundary' a))
    reify = (a -> m (ReifiesTo a))
    -> IPBoundary' a -> m (IPBoundary' (ReifiesTo a))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> IPBoundary' a -> f (IPBoundary' b)
    traverse a -> m (ReifiesTo a)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => a -> m (ReifiesTo a)
    reify

    instance ToConcrete a => ToConcrete (IPBoundary' a) where
      type ConOfAbs (IPBoundary' a) = IPBoundary' (ConOfAbs a)

      toConcrete :: forall (m :: * -> *).
    MonadToConcrete m =>
    IPBoundary' a -> m (ConOfAbs (IPBoundary' a))
    toConcrete = (a -> m (ConOfAbs a))
    -> IPBoundary' a -> m (IPBoundary' (ConOfAbs a))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> IPBoundary' a -> f (IPBoundary' b)
    traverse (Precedence -> a -> m (ConOfAbs a)
    forall (m :: * -> *) a.
    (MonadToConcrete m, ToConcrete a) =>
    Precedence -> a -> m (ConOfAbs a)
    toConcreteCtx Precedence
    TopCtx)

    instance Pretty c => Pretty (IPFace' c) where
      pretty :: IPFace' c -> Doc
    pretty (IPFace' [(c, c)]
    eqs c
    val) = do
        let
          xs :: [Doc]
    xs = ((c, c) -> Doc) -> [(c, c)] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (\ (c
    l,c
    r) -> c -> Doc
    forall a. Pretty a => a -> Doc
    pretty c
    l Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    "=" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> c -> Doc
    forall a. Pretty a => a -> Doc
    pretty c
    r) [(c, c)]
    eqs
          -- rhs = case over of
          --         Overapplied    -> "=" <+> pretty meta
          --         NotOverapplied -> mempty
        [Doc] -> Doc
    forall {a}. Pretty a => [a] -> Doc
    prettyList_ [Doc]
    xs Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    "⊢" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> c -> Doc
    forall a. Pretty a => a -> Doc
    pretty c
    val -- <+> rhs

    prettyConstraints :: [Closure Constraint] -> TCM [OutputForm C.Expr C.Expr]
    prettyConstraints :: [Closure Constraint] -> TCM [OutputForm Expr Expr]
    prettyConstraints [Closure Constraint]
    cs = do
      [Closure Constraint]
    -> (Closure Constraint -> TCMT IO (OutputForm Expr Expr))
    -> TCM [OutputForm Expr Expr]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [Closure Constraint]
    cs ((Closure Constraint -> TCMT IO (OutputForm Expr Expr))
     -> TCM [OutputForm Expr Expr])
    -> (Closure Constraint -> TCMT IO (OutputForm Expr Expr))
    -> TCM [OutputForm Expr Expr]
    forall a b. (a -> b) -> a -> b
    $ \ Closure Constraint
    c -> do
                cl <- ProblemConstraint -> TCMT IO (ReifiesTo ProblemConstraint)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    ProblemConstraint -> m (ReifiesTo ProblemConstraint)
    reify (Set ProblemId -> Blocker -> Closure Constraint -> ProblemConstraint
    PConstr Set ProblemId
    forall a. Set a
    Set.empty Blocker
    alwaysUnblock Closure Constraint
    c)
                enterClosure cl abstractToConcrete_

    getConstraints :: TCM [OutputForm C.Expr C.Expr]
    getConstraints :: TCM [OutputForm Expr Expr]
    getConstraints = (ProblemConstraint -> TCM ProblemConstraint)
    -> (ProblemConstraint -> Bool) -> TCM [OutputForm Expr Expr]
    getConstraints' ProblemConstraint -> TCM ProblemConstraint
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((ProblemConstraint -> Bool) -> TCM [OutputForm Expr Expr])
    -> (ProblemConstraint -> Bool) -> TCM [OutputForm Expr Expr]
    forall a b. (a -> b) -> a -> b
    $ Bool -> ProblemConstraint -> Bool
    forall a b. a -> b -> a
    const Bool
    True

    namedMetaOf :: OutputConstraint A.Expr a -> a
    namedMetaOf :: forall a. OutputConstraint Expr a -> a
    namedMetaOf (OfType a
    i Expr
    _) = a
    i
    namedMetaOf (JustType a
    i) = a
    i
    namedMetaOf (JustSort a
    i) = a
    i
    namedMetaOf (Assign a
    i Expr
    _) = a
    i
    namedMetaOf OutputConstraint_boot TCErr Expr a
    _ = a
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    getConstraintsMentioning :: Rewrite -> MetaId -> TCM [OutputForm C.Expr C.Expr]
    getConstraintsMentioning :: Rewrite -> MetaId -> TCM [OutputForm Expr Expr]
    getConstraintsMentioning Rewrite
    norm MetaId
    m = (ProblemConstraint -> TCM ProblemConstraint)
    -> (ProblemConstraint -> Bool) -> TCM [OutputForm Expr Expr]
    getConstrs ProblemConstraint -> TCM ProblemConstraint
    forall {m :: * -> *} {b}.
    (InstantiateFull b, MonadReduce m) =>
    b -> m b
    instantiateBlockingFull (MetaId -> ProblemConstraint -> Bool
    forall t. MentionsMeta t => MetaId -> t -> Bool
    mentionsMeta MetaId
    m)
      -- could be optimized by not doing a full instantiation up front, with a more clever mentionsMeta.
      where
        instantiateBlockingFull :: b -> m b
    instantiateBlockingFull b
    p
          = Lens' TCState Bool -> (Bool -> Bool) -> m b -> m b
    forall a b. Lens' TCState a -> (a -> a) -> m b -> m b
    forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' TCState a -> (a -> a) -> m b -> m b
    locallyTCState (Bool -> f Bool) -> TCState -> f TCState
    Lens' TCState Bool
    stInstantiateBlocking (Bool -> Bool -> Bool
    forall a b. a -> b -> a
    const Bool
    True) (m b -> m b) -> m b -> m b
    forall a b. (a -> b) -> a -> b
    $
              b -> m b
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull b
    p

        nay :: MaybeT TCM Elims
        nay :: MaybeT (TCMT IO) Elims
    nay = TCM (Maybe Elims) -> MaybeT (TCMT IO) Elims
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (TCM (Maybe Elims) -> MaybeT (TCMT IO) Elims)
    -> TCM (Maybe Elims) -> MaybeT (TCMT IO) Elims
    forall a b. (a -> b) -> a -> b
    $ Maybe Elims -> TCM (Maybe Elims)
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Maybe Elims
    forall a. Maybe a
    Nothing

        -- Trying to find the actual meta application, as long as it's not
        -- buried too deep.
        -- We could look further but probably not under binders as that would mess with
        -- the call to @unifyElimsMeta@ below.
        hasHeadMeta :: Constraint -> Maybe Elims
    hasHeadMeta Constraint
    c =
          case Constraint
    c of
            ValueCmp Comparison
    _ CompareAs
    _ Term
    u Term
    v           -> Term -> Maybe Elims
    isMeta Term
    u Maybe Elims -> Maybe Elims -> Maybe Elims
    forall a. Maybe a -> Maybe a -> Maybe a
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    `mplus` Term -> Maybe Elims
    isMeta Term
    v
            ValueCmpOnFace Comparison
    cmp Term
    p Type
    t Term
    u Term
    v -> Term -> Maybe Elims
    isMeta Term
    u Maybe Elims -> Maybe Elims -> Maybe Elims
    forall a. Maybe a -> Maybe a -> Maybe a
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    `mplus` Term -> Maybe Elims
    isMeta Term
    v
            -- TODO: extend to other comparisons?
            ElimCmp [Polarity]
    cmp [IsForced]
    fs Type
    t Term
    v Elims
    as Elims
    bs   -> Maybe Elims
    forall a. Maybe a
    Nothing
            LevelCmp Comparison
    cmp Level
    u Level
    v           -> Maybe Elims
    forall a. Maybe a
    Nothing
            SortCmp Comparison
    cmp Sort
    a Sort
    b            -> Maybe Elims
    forall a. Maybe a
    Nothing
            UnBlock{}                  -> Maybe Elims
    forall a. Maybe a
    Nothing
            FindInstance{}             -> Maybe Elims
    forall a. Maybe a
    Nothing
            ResolveInstanceHead{}      -> Maybe Elims
    forall a. Maybe a
    Nothing
            IsEmpty Range
    r Type
    t                -> Term -> Maybe Elims
    isMeta (Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t)
            CheckSizeLtSat Term
    t           -> Term -> Maybe Elims
    isMeta Term
    t
            CheckFunDef{}              -> Maybe Elims
    forall a. Maybe a
    Nothing
            HasBiggerSort Sort
    a            -> Maybe Elims
    forall a. Maybe a
    Nothing
            HasPTSRule Dom Type
    a Abs Sort
    b             -> Maybe Elims
    forall a. Maybe a
    Nothing
            UnquoteTactic{}            -> Maybe Elims
    forall a. Maybe a
    Nothing
            CheckDataSort QName
    _ Sort
    s          -> Sort -> Maybe Elims
    isMetaS Sort
    s
            CheckMetaInst{}            -> Maybe Elims
    forall a. Maybe a
    Nothing
            CheckType Type
    t                -> Term -> Maybe Elims
    isMeta (Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t)
            CheckLockedVars Term
    t Type
    _ Arg Term
    _ Type
    _    -> Term -> Maybe Elims
    isMeta Term
    t
            UsableAtModality WhyCheckModality
    _ Maybe Sort
    ms Modality
    _ Term
    t  -> Maybe Sort -> Maybe Elims -> (Sort -> Maybe Elims) -> Maybe Elims
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe Sort
    ms (Term -> Maybe Elims
    isMeta Term
    t) ((Sort -> Maybe Elims) -> Maybe Elims)
    -> (Sort -> Maybe Elims) -> Maybe Elims
    forall a b. (a -> b) -> a -> b
    $ \ Sort
    s -> Sort -> Maybe Elims
    isMetaS Sort
    s Maybe Elims -> Maybe Elims -> Maybe Elims
    forall a. Maybe a -> Maybe a -> Maybe a
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    `mplus` Term -> Maybe Elims
    isMeta Term
    t

        isMeta :: Term -> Maybe Elims
        isMeta :: Term -> Maybe Elims
    isMeta (MetaV MetaId
    m' Elims
    es_m) | MetaId
    m MetaId -> MetaId -> Bool
    forall a. Eq a => a -> a -> Bool
    == MetaId
    m' = Elims -> Maybe Elims
    forall a. a -> Maybe a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Elims
    es_m
        isMeta Term
    _  = Maybe Elims
    forall a. Maybe a
    Nothing

        isMetaS :: I.Sort -> Maybe Elims
        isMetaS :: Sort -> Maybe Elims
    isMetaS (MetaS MetaId
    m' Elims
    es_m)
          | MetaId
    m MetaId -> MetaId -> Bool
    forall a. Eq a => a -> a -> Bool
    == MetaId
    m' = Elims -> Maybe Elims
    forall a. a -> Maybe a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Elims
    es_m
        isMetaS Sort
    _  = Maybe Elims
    forall a. Maybe a
    Nothing

        getConstrs :: (ProblemConstraint -> TCM ProblemConstraint)
    -> (ProblemConstraint -> Bool) -> TCM [OutputForm Expr Expr]
    getConstrs ProblemConstraint -> TCM ProblemConstraint
    g ProblemConstraint -> Bool
    f = TCM [OutputForm Expr Expr] -> TCM [OutputForm Expr Expr]
    forall a. TCM a -> TCM a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM [OutputForm Expr Expr] -> TCM [OutputForm Expr Expr])
    -> TCM [OutputForm Expr Expr] -> TCM [OutputForm Expr Expr]
    forall a b. (a -> b) -> a -> b
    $ do
          cs <- Constraints -> Constraints
    stripConstraintPids (Constraints -> Constraints)
    -> (Constraints -> Constraints) -> Constraints -> Constraints
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ProblemConstraint -> Bool) -> Constraints -> Constraints
    forall a. (a -> Bool) -> [a] -> [a]
    filter ProblemConstraint -> Bool
    f (Constraints -> Constraints)
    -> TCMT IO Constraints -> TCMT IO Constraints
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((ProblemConstraint -> TCM ProblemConstraint)
    -> Constraints -> TCMT IO Constraints
    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 ProblemConstraint -> TCM ProblemConstraint
    g (Constraints -> TCMT IO Constraints)
    -> TCMT IO Constraints -> TCMT IO Constraints
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO Constraints
    forall (m :: * -> *). ReadTCState m => m Constraints
    M.getAllConstraints)
          cs <- caseMaybeM (traverse lookupInteractionPoint =<< isInteractionMeta m) (pure cs) $ \InteractionPoint
    ip -> do
            let
              boundary :: Set (IntMap Bool)
    boundary = Map (IntMap Bool) Term -> Set (IntMap Bool)
    forall k a. Map k a -> Set k
    MapS.keysSet (IPBoundary' Term -> Map (IntMap Bool) Term
    forall t. IPBoundary' t -> Map (IntMap Bool) t
    getBoundary (InteractionPoint -> IPBoundary' Term
    ipBoundary InteractionPoint
    ip))
              isRedundant :: Constraint -> TCMT IO Bool
    isRedundant Constraint
    c = case Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims (Elims -> Maybe Args) -> Maybe Elims -> Maybe Args
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Constraint -> Maybe Elims
    hasHeadMeta Constraint
    c of
                Just Args
    apps -> TCMT
      IO (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
    -> TCMT IO Bool
    -> ((MetaVariable, IntMap Bool, SubstCand, Substitution)
        -> TCMT IO Bool)
    -> TCMT IO Bool
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (MetaId
    -> Args
    -> TCMT
         IO (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
    isFaceConstraint MetaId
    m Args
    apps) (Bool -> TCMT IO Bool
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    False) (((MetaVariable, IntMap Bool, SubstCand, Substitution)
      -> TCMT IO Bool)
     -> TCMT IO Bool)
    -> ((MetaVariable, IntMap Bool, SubstCand, Substitution)
        -> TCMT IO Bool)
    -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $ \(MetaVariable
    _, IntMap Bool
    endps, SubstCand
    _, Substitution
    _) ->
                  Bool -> TCMT IO Bool
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> TCMT IO Bool) -> Bool -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $ IntMap Bool -> Set (IntMap Bool) -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member IntMap Bool
    endps Set (IntMap Bool)
    boundary
                Maybe Args
    Nothing -> Bool -> TCMT IO Bool
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    False
            (ProblemConstraint -> TCMT IO Bool)
    -> Constraints -> TCMT IO Constraints
    forall (m :: * -> *) a.
    Applicative m =>
    (a -> m Bool) -> [a] -> m [a]
    filterM ((Closure Constraint
     -> (Constraint -> TCMT IO Bool) -> TCMT IO Bool)
    -> (Constraint -> TCMT IO Bool)
    -> Closure Constraint
    -> TCMT IO Bool
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Closure Constraint -> (Constraint -> TCMT IO Bool) -> TCMT IO Bool
    forall (m :: * -> *) c a b.
    (MonadTCEnv m, ReadTCState m, LensClosure c a) =>
    c -> (a -> m b) -> m b
    enterClosure ((Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
    forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Bool -> Bool
    not (TCMT IO Bool -> TCMT IO Bool)
    -> (Constraint -> TCMT IO Bool) -> Constraint -> TCMT IO Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Constraint -> TCMT IO Bool
    isRedundant) (Closure Constraint -> TCMT IO Bool)
    -> (ProblemConstraint -> Closure Constraint)
    -> ProblemConstraint
    -> TCMT IO Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ProblemConstraint -> Closure Constraint
    theConstraint) Constraints
    cs

          reportSDoc "tc.constr.mentioning" 20 $ "getConstraintsMentioning"
          forM cs $ \(PConstr Set ProblemId
    s Blocker
    ub Closure Constraint
    c) -> do
            ArgName -> Int -> TCMT IO Doc -> ScopeM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.constr.mentioning" Int
    20 (TCMT IO Doc -> ScopeM ()) -> TCMT IO Doc -> ScopeM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "constraint:  " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    TP.<+> Closure Constraint -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Closure Constraint -> m Doc
    prettyTCM Closure Constraint
    c
            c <- Rewrite -> Closure Constraint -> TCM (Closure Constraint)
    forall t.
    (Reduce t, Simplify t, Instantiate t, Normalise t) =>
    Rewrite -> t -> TCM t
    normalForm Rewrite
    norm Closure Constraint
    c
            let hm = Constraint -> Maybe Elims
    hasHeadMeta (Closure Constraint -> Constraint
    forall a. Closure a -> a
    clValue Closure Constraint
    c)
            reportSDoc "tc.constr.mentioning" 20 $ "constraint:  " TP.<+> prettyTCM c
            reportSDoc "tc.constr.mentioning" 20 $ "hasHeadMeta: " TP.<+> prettyTCM hm
            case allApplyElims =<< hm of
              Just Args
    as_m -> do
                -- unifyElimsMeta tries to move the constraint into
                -- (an extension of) the context where @m@ comes from.
                MetaId
    -> Args
    -> Closure Constraint
    -> ([(Term, Term)] -> Constraint -> TCMT IO (OutputForm Expr Expr))
    -> TCMT IO (OutputForm Expr Expr)
    forall a.
    MetaId
    -> Args
    -> Closure Constraint
    -> ([(Term, Term)] -> Constraint -> TCM a)
    -> TCM a
    unifyElimsMeta MetaId
    m Args
    as_m Closure Constraint
    c (([(Term, Term)] -> Constraint -> TCMT IO (OutputForm Expr Expr))
     -> TCMT IO (OutputForm Expr Expr))
    -> ([(Term, Term)] -> Constraint -> TCMT IO (OutputForm Expr Expr))
    -> TCMT IO (OutputForm Expr Expr)
    forall a b. (a -> b) -> a -> b
    $ \ [(Term, Term)]
    eqs Constraint
    c -> do
                  (Closure (OutputForm Expr Expr)
     -> (OutputForm Expr Expr -> TCMT IO (OutputForm Expr Expr))
     -> TCMT IO (OutputForm Expr Expr))
    -> (OutputForm Expr Expr -> TCMT IO (OutputForm Expr Expr))
    -> Closure (OutputForm Expr Expr)
    -> TCMT IO (OutputForm Expr Expr)
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Closure (OutputForm Expr Expr)
    -> (OutputForm Expr Expr -> TCMT IO (OutputForm Expr Expr))
    -> TCMT IO (OutputForm Expr Expr)
    forall (m :: * -> *) c a b.
    (MonadTCEnv m, ReadTCState m, LensClosure c a) =>
    c -> (a -> m b) -> m b
    enterClosure OutputForm Expr Expr -> TCMT IO (OutputForm Expr Expr)
    OutputForm Expr Expr -> TCMT IO (ConOfAbs (OutputForm Expr Expr))
    forall a (m :: * -> *).
    (ToConcrete a, MonadAbsToCon m) =>
    a -> m (ConOfAbs a)
    abstractToConcrete_ (Closure (OutputForm Expr Expr) -> TCMT IO (OutputForm Expr Expr))
    -> TCMT IO (Closure (OutputForm Expr Expr))
    -> TCMT IO (OutputForm Expr Expr)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ProblemConstraint -> TCMT IO (Closure (OutputForm Expr Expr))
    ProblemConstraint -> TCMT IO (ReifiesTo ProblemConstraint)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    ProblemConstraint -> m (ReifiesTo ProblemConstraint)
    reify (ProblemConstraint -> TCMT IO (Closure (OutputForm Expr Expr)))
    -> (Closure Constraint -> ProblemConstraint)
    -> Closure Constraint
    -> TCMT IO (Closure (OutputForm Expr Expr))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Set ProblemId -> Blocker -> Closure Constraint -> ProblemConstraint
    PConstr Set ProblemId
    s Blocker
    ub (Closure Constraint -> TCMT IO (Closure (OutputForm Expr Expr)))
    -> TCM (Closure Constraint)
    -> TCMT IO (Closure (OutputForm Expr Expr))
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Constraint -> TCM (Closure Constraint)
    forall (m :: * -> *) a.
    (MonadTCEnv m, ReadTCState m) =>
    a -> m (Closure a)
    buildClosure Constraint
    c
              Maybe Args
    _ -> do
                cl <- ProblemConstraint -> TCMT IO (ReifiesTo ProblemConstraint)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    ProblemConstraint -> m (ReifiesTo ProblemConstraint)
    reify (ProblemConstraint -> TCMT IO (ReifiesTo ProblemConstraint))
    -> ProblemConstraint -> TCMT IO (ReifiesTo ProblemConstraint)
    forall a b. (a -> b) -> a -> b
    $ Set ProblemId -> Blocker -> Closure Constraint -> ProblemConstraint
    PConstr Set ProblemId
    s Blocker
    ub Closure Constraint
    c
                enterClosure cl abstractToConcrete_

    -- Copied from Agda.TypeChecking.Pretty.Warning.prettyConstraints
    stripConstraintPids :: Constraints -> Constraints
    stripConstraintPids :: Constraints -> Constraints
    stripConstraintPids Constraints
    cs = (ProblemConstraint -> ProblemConstraint -> Ordering)
    -> Constraints -> Constraints
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    List.sortBy (Bool -> Bool -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Bool -> Bool -> Ordering)
    -> (ProblemConstraint -> Bool)
    -> ProblemConstraint
    -> ProblemConstraint
    -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` ProblemConstraint -> Bool
    isBlocked) (Constraints -> Constraints) -> Constraints -> Constraints
    forall a b. (a -> b) -> a -> b
    $ (ProblemConstraint -> ProblemConstraint)
    -> Constraints -> Constraints
    forall a b. (a -> b) -> [a] -> [b]
    map ProblemConstraint -> ProblemConstraint
    stripPids Constraints
    cs
      where
        isBlocked :: ProblemConstraint -> Bool
    isBlocked = Bool -> Bool
    not (Bool -> Bool)
    -> (ProblemConstraint -> Bool) -> ProblemConstraint -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Set ProblemId -> Bool
    forall a. Null a => a -> Bool
    null (Set ProblemId -> Bool)
    -> (ProblemConstraint -> Set ProblemId)
    -> ProblemConstraint
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Blocker -> Set ProblemId
    allBlockingProblems (Blocker -> Set ProblemId)
    -> (ProblemConstraint -> Blocker)
    -> ProblemConstraint
    -> Set ProblemId
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ProblemConstraint -> Blocker
    constraintUnblocker
        interestingPids :: Set ProblemId
    interestingPids = [Set ProblemId] -> Set ProblemId
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions ([Set ProblemId] -> Set ProblemId)
    -> [Set ProblemId] -> Set ProblemId
    forall a b. (a -> b) -> a -> b
    $ (ProblemConstraint -> Set ProblemId)
    -> Constraints -> [Set ProblemId]
    forall a b. (a -> b) -> [a] -> [b]
    map (Blocker -> Set ProblemId
    allBlockingProblems (Blocker -> Set ProblemId)
    -> (ProblemConstraint -> Blocker)
    -> ProblemConstraint
    -> Set ProblemId
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ProblemConstraint -> Blocker
    constraintUnblocker) Constraints
    cs
        stripPids :: ProblemConstraint -> ProblemConstraint
    stripPids (PConstr Set ProblemId
    pids Blocker
    unblock Closure Constraint
    c) = Set ProblemId -> Blocker -> Closure Constraint -> ProblemConstraint
    PConstr (Set ProblemId -> Set ProblemId -> Set ProblemId
    forall a. Ord a => Set a -> Set a -> Set a
    Set.intersection Set ProblemId
    pids Set ProblemId
    interestingPids) Blocker
    unblock Closure Constraint
    c

    {-# SPECIALIZE interactionIdToMetaId :: InteractionId -> TCM MetaId #-}
    -- | Converts an 'InteractionId' to a 'MetaId'.
    interactionIdToMetaId :: ReadTCState m => InteractionId -> m MetaId
    interactionIdToMetaId :: forall (m :: * -> *). ReadTCState m => InteractionId -> m MetaId
    interactionIdToMetaId InteractionId
    i = do
      h <- m ModuleNameHash
    forall (m :: * -> *). ReadTCState m => m ModuleNameHash
    currentModuleNameHash
      return MetaId
        { metaId     = fromIntegral i
        , metaModule = h
        }

    getConstraints' :: (ProblemConstraint -> TCM ProblemConstraint) -> (ProblemConstraint -> Bool) -> TCM [OutputForm C.Expr C.Expr]
    getConstraints' :: (ProblemConstraint -> TCM ProblemConstraint)
    -> (ProblemConstraint -> Bool) -> TCM [OutputForm Expr Expr]
    getConstraints' ProblemConstraint -> TCM ProblemConstraint
    g ProblemConstraint -> Bool
    f = TCM [OutputForm Expr Expr] -> TCM [OutputForm Expr Expr]
    forall a. TCM a -> TCM a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM [OutputForm Expr Expr] -> TCM [OutputForm Expr Expr])
    -> TCM [OutputForm Expr Expr] -> TCM [OutputForm Expr Expr]
    forall a b. (a -> b) -> a -> b
    $ do
        cs <- Constraints -> Constraints
    stripConstraintPids (Constraints -> Constraints)
    -> (Constraints -> Constraints) -> Constraints -> Constraints
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ProblemConstraint -> Bool) -> Constraints -> Constraints
    forall a. (a -> Bool) -> [a] -> [a]
    filter ProblemConstraint -> Bool
    f (Constraints -> Constraints)
    -> TCMT IO Constraints -> TCMT IO Constraints
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((ProblemConstraint -> TCM ProblemConstraint)
    -> Constraints -> TCMT IO Constraints
    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 ProblemConstraint -> TCM ProblemConstraint
    g (Constraints -> TCMT IO Constraints)
    -> TCMT IO Constraints -> TCMT IO Constraints
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO Constraints
    forall (m :: * -> *). ReadTCState m => m Constraints
    M.getAllConstraints)
        cs <- forM cs $ \ProblemConstraint
    c -> do
                cl <- ProblemConstraint -> TCMT IO (ReifiesTo ProblemConstraint)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    ProblemConstraint -> m (ReifiesTo ProblemConstraint)
    reify ProblemConstraint
    c
                enterClosure cl abstractToConcrete_
        ss <- mapM toOutputForm =<< getSolvedInteractionPoints True AsIs -- get all
        return $ ss ++ cs
      where
        toOutputForm :: (InteractionId, MetaId, Expr) -> m (OutputForm Expr Expr)
    toOutputForm (InteractionId
    ii, MetaId
    mi, Expr
    e) = do
          mv <- MetaVariable -> Closure Range
    getMetaInfo (MetaVariable -> Closure Range)
    -> m MetaVariable -> m (Closure Range)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> m MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    mi
          withMetaInfo mv $ do
            mi <- interactionIdToMetaId ii
            let m = MetaInfo -> InteractionId -> Expr
    QuestionMark MetaInfo
    emptyMetaInfo{ metaNumber = Just mi } InteractionId
    ii
            let oform = Range
    -> [ProblemId]
    -> Blocker
    -> OutputConstraint_boot TCErr Expr Expr
    -> OutputForm Expr Expr
    forall tcErr a b.
    Range
    -> [ProblemId]
    -> Blocker
    -> OutputConstraint_boot tcErr a b
    -> OutputForm_boot tcErr a b
    OutputForm Range
    forall a. Range' a
    noRange [] Blocker
    alwaysUnblock (OutputConstraint_boot TCErr Expr Expr -> OutputForm Expr Expr)
    -> OutputConstraint_boot TCErr Expr Expr -> OutputForm Expr Expr
    forall a b. (a -> b) -> a -> b
    $ Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr
    forall tcErr a b. b -> a -> OutputConstraint_boot tcErr a b
    Assign Expr
    m Expr
    e :: OutputForm Expr Expr
            abstractToConcrete_ oform

    -- | Reify the boundary of an interaction point as something that can be
    -- shown to the user.
    getIPBoundary :: Rewrite -> InteractionId -> TCM [IPFace' C.Expr]
    getIPBoundary :: Rewrite -> InteractionId -> TCM [IPFace' Expr]
    getIPBoundary Rewrite
    norm InteractionId
    ii = InteractionId -> TCM [IPFace' Expr] -> TCM [IPFace' Expr]
    forall (m :: * -> *) a.
    (MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    ii (TCM [IPFace' Expr] -> TCM [IPFace' Expr])
    -> TCM [IPFace' Expr] -> TCM [IPFace' Expr]
    forall a b. (a -> b) -> a -> b
    $ do
      ip <- InteractionId -> TCMT IO InteractionPoint
    forall (m :: * -> *).
    (ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m InteractionPoint
    lookupInteractionPoint InteractionId
    ii

      io <- primIOne
      iz <- primIZero

      lookupInteractionMeta ii >>= \case
        Just MetaId
    mi -> do
          mv <- MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    mi

          let t = Judgement MetaId -> Type
    forall a. Judgement a -> Type
    jMetaType (Judgement MetaId -> Type) -> Judgement MetaId -> Type
    forall a b. (a -> b) -> a -> b
    $ MetaVariable -> Judgement MetaId
    mvJudgement MetaVariable
    mv
          telv@(TelV tel a) <- telView t

          reportSDoc "tc.ip.boundary" 30 $ TP.vcat
            [ "reifying interaction point boundary"
            , "tel:       " TP.<+> prettyTCM tel
            , "meta:      " TP.<+> prettyTCM mi
            ]
          reportSDoc "tc.ip.boundary" 30 $ "boundary:  " TP.<+> pure (pretty (getBoundary (ipBoundary ip)))

          withInteractionId ii $ do
          -- The boundary is a map associating terms (lambda abstractions)
          -- to IntMap Bools. The meta solver will wrap each LHS in lambdas
          -- corresponding to the interaction point's context. Each key of
          -- the boundary has a subset of (the interval variables in) the
          -- interaction point's context as a keysSet.
          as <- getContextArgs
          let
            c = Expr -> TCM Expr
    Expr -> TCMT IO (ConOfAbs Expr)
    forall a (m :: * -> *).
    (ToConcrete a, MonadAbsToCon m) =>
    a -> m (ConOfAbs a)
    abstractToConcrete_ (Expr -> TCM Expr) -> (Term -> TCM Expr) -> Term -> TCM Expr
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< Term -> TCM Expr
    Term -> TCMT IO (ReifiesTo Term)
    forall i. Reify i => i -> TCM (ReifiesTo i)
    reifyUnblocked (Term -> TCM Expr) -> (Term -> TCM Term) -> Term -> TCM Expr
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< Rewrite -> Term -> TCM Term
    forall t.
    (Reduce t, Simplify t, Instantiate t, Normalise t) =>
    Rewrite -> t -> TCM t
    normalForm Rewrite
    norm
            go (IntMap Bool
    im, Term
    rhs) = do
              ArgName -> Int -> TCMT IO Doc -> ScopeM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.ip.boundary" Int
    30 (TCMT IO Doc -> ScopeM ()) -> TCMT IO Doc -> ScopeM ()
    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
    TP.vcat
                [ TCMT IO Doc
    "reifying constraint for face" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    TP.<+> IntMap Bool -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    TP.pretty IntMap Bool
    im
                ]
              ArgName -> Int -> TCMT IO Doc -> ScopeM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.ip.boundary" Int
    30 (TCMT IO Doc -> ScopeM ()) -> TCMT IO Doc -> ScopeM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "term " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    TP.<+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    TP.prettyTCM Term
    rhs
              -- Since the RHS is a lambda we have to apply it to the
              -- context:
              rhs <- Term -> TCM Expr
    c (Term
    rhs Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` Args
    as)

              -- Reify the IntMap Bool as a list of (i = i0) (j = i1) terms:
              eqns <- forM (IntMap.toList im) $ \(Int
    a, Bool
    b) -> do
                a <- Term -> TCM Expr
    c (Int -> Elims -> Term
    I.Var Int
    a [])
                (,) a <$> c (if b then io else iz)
              pure $ IPFace' eqns rhs
          traverse go $ MapS.toList (getBoundary (ipBoundary ip))
        Maybe MetaId
    Nothing -> [IPFace' Expr] -> TCM [IPFace' Expr]
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure []

    typeAndFacesInMeta :: InteractionId -> Rewrite -> Expr -> TCM (Expr, [IPFace' C.Expr])
    typeAndFacesInMeta :: InteractionId -> Rewrite -> Expr -> TCM (Expr, [IPFace' Expr])
    typeAndFacesInMeta InteractionId
    ii Rewrite
    norm Expr
    expr = InteractionId
    -> TCM (Expr, [IPFace' Expr]) -> TCM (Expr, [IPFace' Expr])
    forall (m :: * -> *) a.
    (MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    ii (TCM (Expr, [IPFace' Expr]) -> TCM (Expr, [IPFace' Expr]))
    -> TCM (Expr, [IPFace' Expr]) -> TCM (Expr, [IPFace' Expr])
    forall a b. (a -> b) -> a -> b
    $ do
      (ex, ty) <- Expr -> TCM (Term, Type)
    inferExpr Expr
    expr
      ty <- normalForm norm ty
      ip <- lookupInteractionPoint ii

      io <- primIOne
      iz <- primIZero
      let
        go IntMap Bool
    im = do
          let
            c :: Term -> TCM Expr
    c = Expr -> TCM Expr
    Expr -> TCMT IO (ConOfAbs Expr)
    forall a (m :: * -> *).
    (ToConcrete a, MonadAbsToCon m) =>
    a -> m (ConOfAbs a)
    abstractToConcrete_ (Expr -> TCM Expr) -> (Term -> TCM Expr) -> Term -> TCM Expr
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< Term -> TCM Expr
    Term -> TCMT IO (ReifiesTo Term)
    forall i. Reify i => i -> TCM (ReifiesTo i)
    reifyUnblocked (Term -> TCM Expr) -> (Term -> TCM Term) -> Term -> TCM Expr
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< Rewrite -> Term -> TCM Term
    forall t.
    (Reduce t, Simplify t, Instantiate t, Normalise t) =>
    Rewrite -> t -> TCM t
    normalForm Rewrite
    norm
            fa :: [(Int, Bool)]
    fa = IntMap Bool -> [(Int, Bool)]
    forall a. IntMap a -> [(Int, a)]
    IntMap.toList IntMap Bool
    im
            face :: (Int, Bool) -> Substitution
    face (Int
    i, Bool
    m) = Int -> Term -> Substitution
    forall a. EndoSubst a => Int -> a -> Substitution' a
    inplaceS Int
    i (Term -> Substitution) -> Term -> Substitution
    forall a b. (a -> b) -> a -> b
    $ if Bool
    m then Term
    io else Term
    iz
            sub :: Substitution
    sub = ((Int, Bool) -> Substitution -> Substitution)
    -> Substitution -> [(Int, Bool)] -> Substitution
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (\(Int, Bool)
    f Substitution
    s -> Substitution -> Substitution -> Substitution
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    composeS ((Int, Bool) -> Substitution
    face (Int, Bool)
    f) Substitution
    s) Substitution
    forall a. Substitution' a
    idS [(Int, Bool)]
    fa
          eqns <- [(Int, Bool)]
    -> ((Int, Bool) -> TCMT IO (Expr, Expr)) -> TCMT IO [(Expr, Expr)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [(Int, Bool)]
    fa (((Int, Bool) -> TCMT IO (Expr, Expr)) -> TCMT IO [(Expr, Expr)])
    -> ((Int, Bool) -> TCMT IO (Expr, Expr)) -> TCMT IO [(Expr, Expr)]
    forall a b. (a -> b) -> a -> b
    $ \(Int
    a, Bool
    b) -> do
            a <- Term -> TCM Expr
    c (Int -> Elims -> Term
    I.Var Int
    a [])
            (,) a <$> c (if b then io else iz)
          fmap (IPFace' eqns) . c =<< simplify (applySubst sub ex)

      faces <- traverse go $ MapS.keys (getBoundary (ipBoundary ip))
      ty <- reifyUnblocked ty
      pure (ty, faces)

    -- | Goals and Warnings

    getGoals :: TCM Goals
    getGoals :: TCM Goals
    getGoals = Rewrite -> Rewrite -> TCM Goals
    getGoals' Rewrite
    AsIs Rewrite
    Simplified
      -- visible metas (as-is)
      -- hidden metas (unsolved implicit arguments simplified)

    getGoals'
      :: Rewrite    -- ^ Degree of normalization of goals.
      -> Rewrite    -- ^ Degree of normalization of hidden goals.
      -> TCM Goals
    getGoals' :: Rewrite -> Rewrite -> TCM Goals
    getGoals' Rewrite
    normVisible Rewrite
    normHidden = do
      visibleMetas <- Rewrite -> TCM [OutputConstraint_boot TCErr Expr InteractionId]
    typesOfVisibleMetas Rewrite
    normVisible
      hiddenMetas <- typesOfHiddenMetas normHidden
      return (visibleMetas, hiddenMetas)

    -- | Print open metas nicely.
    showGoals :: Goals -> TCM String
    showGoals :: Goals -> TCM ArgName
    showGoals ([OutputConstraint_boot TCErr Expr InteractionId]
    ims, [OutputConstraint Expr NamedMeta]
    hms) = do
      di <- [OutputConstraint_boot TCErr Expr InteractionId]
    -> (OutputConstraint_boot TCErr Expr InteractionId -> TCMT IO Doc)
    -> TCMT IO [Doc]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [OutputConstraint_boot TCErr Expr InteractionId]
    ims ((OutputConstraint_boot TCErr Expr InteractionId -> TCMT IO Doc)
     -> TCMT IO [Doc])
    -> (OutputConstraint_boot TCErr Expr InteractionId -> TCMT IO Doc)
    -> TCMT IO [Doc]
    forall a b. (a -> b) -> a -> b
    $ \ OutputConstraint_boot TCErr Expr InteractionId
    i ->
        InteractionId -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a.
    (MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId (OutputForm Expr InteractionId -> InteractionId
    forall a b. OutputForm a b -> b
    outputFormId (OutputForm Expr InteractionId -> InteractionId)
    -> OutputForm Expr InteractionId -> InteractionId
    forall a b. (a -> b) -> a -> b
    $ Range
    -> [ProblemId]
    -> Blocker
    -> OutputConstraint_boot TCErr Expr InteractionId
    -> OutputForm Expr InteractionId
    forall tcErr a b.
    Range
    -> [ProblemId]
    -> Blocker
    -> OutputConstraint_boot tcErr a b
    -> OutputForm_boot tcErr a b
    OutputForm Range
    forall a. Range' a
    noRange [] Blocker
    alwaysUnblock OutputConstraint_boot TCErr Expr InteractionId
    i) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $
          OutputConstraint_boot TCErr Expr InteractionId -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyATop OutputConstraint_boot TCErr Expr InteractionId
    i
      dh <- mapM showA' hms
      return $ unlines $ map show di ++ dh
      where
        showA' :: OutputConstraint A.Expr NamedMeta -> TCM String
        showA' :: OutputConstraint Expr NamedMeta -> TCM ArgName
    showA' OutputConstraint Expr NamedMeta
    m = do
          let i :: MetaId
    i = NamedMeta -> MetaId
    nmid (NamedMeta -> MetaId) -> NamedMeta -> MetaId
    forall a b. (a -> b) -> a -> b
    $ OutputConstraint Expr NamedMeta -> NamedMeta
    forall a. OutputConstraint Expr a -> a
    namedMetaOf OutputConstraint Expr NamedMeta
    m
          r <- MetaId -> TCMT IO Range
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m Range
    getMetaRange MetaId
    i
          d <- withMetaId i (prettyATop m)
          return $ show d ++ "  [ at " ++ prettyShow r ++ " ]"

    getWarningsAndNonFatalErrors :: TCM WarningsAndNonFatalErrors
    getWarningsAndNonFatalErrors :: TCM WarningsAndNonFatalErrors
    getWarningsAndNonFatalErrors = do
      mws <- WhichWarnings -> TCMT IO (Set TCWarning)
    forall (m :: * -> *).
    (ReadTCState m, MonadWarning m, MonadTCM m) =>
    WhichWarnings -> m (Set TCWarning)
    getAllWarnings WhichWarnings
    AllWarnings
      let notMetaWarnings = (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
    . TCWarning -> Bool
    isMetaTCWarning) ([TCWarning] -> [TCWarning]) -> [TCWarning] -> [TCWarning]
    forall a b. (a -> b) -> a -> b
    $ Set TCWarning -> [TCWarning]
    forall a. Set a -> [a]
    Set.toList Set TCWarning
    mws
      return $ case notMetaWarnings of
        ws :: [TCWarning]
    ws@(TCWarning
    _:[TCWarning]
    _) -> [TCWarning] -> WarningsAndNonFatalErrors
    classifyWarnings [TCWarning]
    ws
        [TCWarning]
    _ -> WarningsAndNonFatalErrors
    forall a. Null a => a
    empty

    -- | Collecting the context of the given meta-variable.
    getResponseContext
      :: Rewrite      -- ^ Normalise?
      -> InteractionId
      -> TCM [ResponseContextEntry]
    getResponseContext :: Rewrite -> InteractionId -> TCM [ResponseContextEntry]
    getResponseContext Rewrite
    norm InteractionId
    ii = InteractionId -> Rewrite -> TCM [ResponseContextEntry]
    contextOfMeta InteractionId
    ii Rewrite
    norm

    -- | @getSolvedInteractionPoints True@ returns all solutions,
    --   even if just solved by another, non-interaction meta.
    --
    --   @getSolvedInteractionPoints False@ only returns metas that
    --   are solved by a non-meta.

    getSolvedInteractionPoints :: Bool -> Rewrite -> TCM [(InteractionId, MetaId, Expr)]
    getSolvedInteractionPoints :: Bool -> Rewrite -> TCMT IO [(InteractionId, MetaId, Expr)]
    getSolvedInteractionPoints Bool
    all Rewrite
    norm = [[(InteractionId, MetaId, Expr)]]
    -> [(InteractionId, MetaId, Expr)]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([[(InteractionId, MetaId, Expr)]]
     -> [(InteractionId, MetaId, Expr)])
    -> TCMT IO [[(InteractionId, MetaId, Expr)]]
    -> TCMT IO [(InteractionId, MetaId, Expr)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
      ((InteractionId, MetaId)
     -> TCMT IO [(InteractionId, MetaId, Expr)])
    -> [(InteractionId, MetaId)]
    -> TCMT IO [[(InteractionId, MetaId, Expr)]]
    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 (InteractionId, MetaId) -> TCMT IO [(InteractionId, MetaId, Expr)]
    solution ([(InteractionId, MetaId)]
     -> TCMT IO [[(InteractionId, MetaId, Expr)]])
    -> TCMT IO [(InteractionId, MetaId)]
    -> TCMT IO [[(InteractionId, MetaId, Expr)]]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO [(InteractionId, MetaId)]
    forall (m :: * -> *). ReadTCState m => m [(InteractionId, MetaId)]
    getInteractionIdsAndMetas
      where
        solution :: (InteractionId, MetaId) -> TCMT IO [(InteractionId, MetaId, Expr)]
    solution (InteractionId
    i, MetaId
    m) = do
          mv <- MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    m
          withMetaInfo (getMetaInfo mv) $ do
            args  <- getContextArgs
            scope <- getScope
            let sol Term
    v = do
                  -- Andreas, 2014-02-17 exclude metas solved by metas
                  v <- Term -> TCM Term
    forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
    instantiate Term
    v
                  let isMeta = case Term
    v of MetaV{} -> Bool
    True; Term
    _ -> Bool
    False
                  if isMeta && not all then return [] else do
                    e <- blankNotInScope =<< reify =<< normalForm norm v
                    return [(i, m, ScopedExpr scope e)]
                unsol = [a] -> TCMT IO [a]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
            case mvInstantiation mv of
              InstV{}                        -> Term -> TCMT IO [(InteractionId, MetaId, Expr)]
    sol (MetaId -> Elims -> Term
    MetaV MetaId
    m (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Elim' Term) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply Args
    args)
              OpenMeta{}                     -> TCMT IO [(InteractionId, MetaId, Expr)]
    forall {a}. TCMT IO [a]
    unsol
              BlockedConst{}                 -> TCMT IO [(InteractionId, MetaId, Expr)]
    forall {a}. TCMT IO [a]
    unsol
              PostponedTypeCheckingProblem{} -> TCMT IO [(InteractionId, MetaId, Expr)]
    forall {a}. TCMT IO [a]
    unsol

    typeOfMetaMI :: Rewrite -> MetaId -> TCM (OutputConstraint Expr NamedMeta)
    typeOfMetaMI :: Rewrite -> MetaId -> TCM (OutputConstraint Expr NamedMeta)
    typeOfMetaMI Rewrite
    norm MetaId
    mi =
         do mv <- MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    mi
            withMetaInfo (getMetaInfo mv) $
              rewriteJudg mv (mvJudgement mv)
       where
        rewriteJudg :: MetaVariable -> Judgement MetaId ->
                       TCM (OutputConstraint Expr NamedMeta)
        rewriteJudg :: MetaVariable
    -> Judgement MetaId -> TCM (OutputConstraint Expr NamedMeta)
    rewriteJudg MetaVariable
    mv (HasType MetaId
    i Comparison
    cmp Type
    t) = do
          ms <- MetaId -> TCM ArgName
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m ArgName
    getMetaNameSuggestion MetaId
    i
          -- Andreas, 2019-03-17, issue #3638:
          -- Need to put meta type into correct context _before_ normalizing,
          -- otherwise rewrite rules in parametrized modules will not fire.
          vs <- getContextArgs
          t <- t `piApplyM` permute (takeP (size vs) $ mvPermutation mv) vs
          t <- normalForm norm t
          let x = ArgName -> MetaId -> NamedMeta
    NamedMeta ArgName
    ms MetaId
    i
          reportSDoc "interactive.meta" 10 $ TP.vcat
            [ TP.text $ unwords ["permuting", show i, "with", show $ mvPermutation mv]
            , TP.nest 2 $ TP.vcat
              [ "len  =" TP.<+> TP.text (show $ length vs)
              , "args =" TP.<+> prettyTCM vs
              , "t    =" TP.<+> prettyTCM t
              , "x    =" TP.<+> TP.pretty x
              ]
            ]
          reportSDoc "interactive.meta.scope" 20 $ TP.text $ show $ getMetaScope mv
          -- Andreas, 2016-01-19, issue #1783: need piApplyM instead of just piApply
          OfType x <$> reifyUnblocked t
        rewriteJudg MetaVariable
    mv (IsSort MetaId
    i Type
    t) = do
          ms <- MetaId -> TCM ArgName
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m ArgName
    getMetaNameSuggestion MetaId
    i
          return $ JustSort $ NamedMeta ms i

    typeOfMeta :: Rewrite -> InteractionId -> TCM (OutputConstraint Expr InteractionId)
    typeOfMeta :: Rewrite
    -> InteractionId
    -> TCM (OutputConstraint_boot TCErr Expr InteractionId)
    typeOfMeta Rewrite
    norm InteractionId
    ii = Rewrite
    -> (InteractionId, MetaId)
    -> TCM (OutputConstraint_boot TCErr Expr InteractionId)
    typeOfMeta' Rewrite
    norm ((InteractionId, MetaId)
     -> TCM (OutputConstraint_boot TCErr Expr InteractionId))
    -> (MetaId -> (InteractionId, MetaId))
    -> MetaId
    -> TCM (OutputConstraint_boot TCErr Expr InteractionId)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (InteractionId
    ii,) (MetaId -> TCM (OutputConstraint_boot TCErr Expr InteractionId))
    -> TCMT IO MetaId
    -> TCM (OutputConstraint_boot TCErr Expr InteractionId)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< InteractionId -> TCMT IO MetaId
    forall (m :: * -> *).
    (ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m MetaId
    lookupInteractionId InteractionId
    ii

    typeOfMeta' :: Rewrite -> (InteractionId, MetaId) -> TCM (OutputConstraint Expr InteractionId)
    typeOfMeta' :: Rewrite
    -> (InteractionId, MetaId)
    -> TCM (OutputConstraint_boot TCErr Expr InteractionId)
    typeOfMeta' Rewrite
    norm (InteractionId
    ii, MetaId
    mi) = (NamedMeta -> InteractionId)
    -> OutputConstraint Expr NamedMeta
    -> OutputConstraint_boot TCErr Expr InteractionId
    forall a b.
    (a -> b)
    -> OutputConstraint_boot TCErr Expr a
    -> OutputConstraint_boot TCErr Expr b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\NamedMeta
    _ -> InteractionId
    ii) (OutputConstraint Expr NamedMeta
     -> OutputConstraint_boot TCErr Expr InteractionId)
    -> TCM (OutputConstraint Expr NamedMeta)
    -> TCM (OutputConstraint_boot TCErr Expr InteractionId)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Rewrite -> MetaId -> TCM (OutputConstraint Expr NamedMeta)
    typeOfMetaMI Rewrite
    norm MetaId
    mi

    typesOfVisibleMetas :: Rewrite -> TCM [OutputConstraint Expr InteractionId]
    typesOfVisibleMetas :: Rewrite -> TCM [OutputConstraint_boot TCErr Expr InteractionId]
    typesOfVisibleMetas Rewrite
    norm =
      TCM [OutputConstraint_boot TCErr Expr InteractionId]
    -> TCM [OutputConstraint_boot TCErr Expr InteractionId]
    forall a. TCM a -> TCM a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM [OutputConstraint_boot TCErr Expr InteractionId]
     -> TCM [OutputConstraint_boot TCErr Expr InteractionId])
    -> TCM [OutputConstraint_boot TCErr Expr InteractionId]
    -> TCM [OutputConstraint_boot TCErr Expr InteractionId]
    forall a b. (a -> b) -> a -> b
    $ ((InteractionId, MetaId)
     -> TCM (OutputConstraint_boot TCErr Expr InteractionId))
    -> [(InteractionId, MetaId)]
    -> TCM [OutputConstraint_boot TCErr Expr InteractionId]
    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 (Rewrite
    -> (InteractionId, MetaId)
    -> TCM (OutputConstraint_boot TCErr Expr InteractionId)
    typeOfMeta' Rewrite
    norm) ([(InteractionId, MetaId)]
     -> TCM [OutputConstraint_boot TCErr Expr InteractionId])
    -> TCMT IO [(InteractionId, MetaId)]
    -> TCM [OutputConstraint_boot TCErr Expr InteractionId]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO [(InteractionId, MetaId)]
    forall (m :: * -> *). ReadTCState m => m [(InteractionId, MetaId)]
    getInteractionIdsAndMetas

    typesOfHiddenMetas :: Rewrite -> TCM [OutputConstraint Expr NamedMeta]
    typesOfHiddenMetas :: Rewrite -> TCM [OutputConstraint Expr NamedMeta]
    typesOfHiddenMetas Rewrite
    norm = TCM [OutputConstraint Expr NamedMeta]
    -> TCM [OutputConstraint Expr NamedMeta]
    forall a. TCM a -> TCM a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM [OutputConstraint Expr NamedMeta]
     -> TCM [OutputConstraint Expr NamedMeta])
    -> TCM [OutputConstraint Expr NamedMeta]
    -> TCM [OutputConstraint Expr NamedMeta]
    forall a b. (a -> b) -> a -> b
    $ do
      is    <- TCMT IO [MetaId]
    forall (m :: * -> *). ReadTCState m => m [MetaId]
    getInteractionMetas
      store <- MapS.filterWithKey (implicit is) <$> useR stOpenMetaStore
      mapM (typeOfMetaMI norm) $ MapS.keys store
      where
      implicit :: t a -> a -> MetaVariable -> Bool
    implicit t a
    is a
    x MetaVariable
    m | Maybe MetaId -> Bool
    forall a. Maybe a -> Bool
    isJust (MetaVariable -> Maybe MetaId
    mvTwin MetaVariable
    m) = Bool
    False
      implicit t a
    is a
    x MetaVariable
    m =
        case MetaVariable -> MetaInstantiation
    mvInstantiation MetaVariable
    m of
          M.InstV{} -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          M.OpenMeta MetaKind
    _ -> a
    x a -> t a -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` t a
    is  -- OR: True in case of InstanceMeta !?
          M.BlockedConst{} -> Bool
    False
          M.PostponedTypeCheckingProblem{} -> Bool
    False

    -- | Create type of application of new helper function that would solve the goal.
    metaHelperType :: Rewrite -> InteractionId -> Range -> String -> TCM (OutputConstraint' Expr Expr)
    metaHelperType :: Rewrite
    -> InteractionId
    -> Range
    -> ArgName
    -> TCM (OutputConstraint' Expr Expr)
    metaHelperType Rewrite
    norm InteractionId
    ii Range
    rng ArgName
    s = case ArgName -> Names
    words ArgName
    s of
      []    -> TCM (OutputConstraint' Expr Expr)
    forall {a}. TCMT IO a
    failure
      ArgName
    f : Names
    _ -> InteractionId
    -> TCM (OutputConstraint' Expr Expr)
    -> TCM (OutputConstraint' Expr Expr)
    forall (m :: * -> *) a.
    (MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    ii (TCM (OutputConstraint' Expr Expr)
     -> TCM (OutputConstraint' Expr Expr))
    -> TCM (OutputConstraint' Expr Expr)
    -> TCM (OutputConstraint' Expr Expr)
    forall a b. (a -> b) -> a -> b
    $ do
        ArgName -> ScopeM ()
    ensureName ArgName
    f
        A.Application h args <- Expr -> AppView' Expr
    A.appView (Expr -> AppView' Expr) -> (Expr -> Expr) -> Expr -> AppView' Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Expr -> Expr
    getBody (Expr -> Expr) -> (Expr -> Expr) -> Expr -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Expr -> Expr
    forall a. ExprLike a => a -> a
    deepUnscope (Expr -> AppView' Expr) -> TCM Expr -> TCMT IO (AppView' Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> InteractionId -> Range -> ArgName -> TCM Expr
    parseExprIn InteractionId
    ii Range
    rng (ArgName
    "let " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ ArgName
    f ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ ArgName
    " = _ in " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ ArgName
    s)
        inCxt   <- hasElem <$> getContextNames
        cxtArgs <- getContextArgs
        enclosingFunctionName <- ipcQName . envClause <$> getEnv
        a0      <- (`piApply` cxtArgs) <$> (getMetaType =<< lookupInteractionId ii)

        -- Konstantin, 2022-10-23: We don't want to print section parameters in helper type.
        freeVars <- getCurrentModuleFreeVars
        ctx <- getContext
        let contextForAbstracting = Int -> Context -> Context
    forall a. Int -> [a] -> [a]
    take (Context -> Int
    forall a. Sized a => a -> Int
    size Context
    ctx Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    freeVars) Context
    ctx

        -- Andreas, 2019-10-11: I actually prefer pi-types over ->.
        let runInPrintingEnvironment = (TCEnv -> TCEnv) -> TCM Expr -> TCM Expr
    forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC (\TCEnv
    e -> TCEnv
    e { envPrintDomainFreePi = True, envPrintMetasBare = True })
                                     (TCM Expr -> TCM Expr)
    -> (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Impossible -> Int -> TCM Expr -> TCM Expr
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Impossible -> Int -> m a -> m a
    escapeContext Impossible
    HasCallStack => Impossible
    impossible (Context -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Context
    contextForAbstracting)
                                     (TCM Expr -> TCM Expr)
    -> (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCM Expr -> TCM Expr
    forall (m :: * -> *) a. ReadTCState m => m a -> m a
    withoutPrintingGeneralization
                                     (TCM Expr -> TCM Expr)
    -> (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCM Expr -> TCM Expr
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    dontFoldLetBindings

        case mapM (isVar . namedArg) args >>= \ [Name]
    xs -> [Name]
    xs [Name] -> Maybe () -> Maybe [Name]
    forall a b. a -> Maybe b -> Maybe a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Bool -> Maybe ()
    forall b (m :: * -> *). (IsBool b, MonadPlus m) => b -> m ()
    guard ((Name -> Bool) -> [Name] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Name -> Bool
    inCxt [Name]
    xs) of

         -- Andreas, 2019-10-11
         -- If all arguments are variables, there is no need to abstract.
         -- We simply make exactly the given arguments visible and all other hidden.
         Just [Name]
    xs -> do
          let inXs :: Name -> Bool
    inXs = [Name] -> Name -> Bool
    forall a. Ord a => [a] -> a -> Bool
    hasElem [Name]
    xs
          let hideButXs :: ContextEntry -> ContextEntry
    hideButXs ContextEntry
    ce = Hiding -> ContextEntry -> ContextEntry
    forall a. LensHiding a => Hiding -> a -> a
    setHiding (if Name -> Bool
    inXs (ContextEntry -> Name
    ctxEntryName ContextEntry
    ce) then Hiding
    NotHidden else Hiding
    Hidden) ContextEntry
    ce
          let tel :: Telescope
    tel = Context -> Telescope
    contextToTel (Context -> Telescope)
    -> (Context -> Context) -> Context -> Telescope
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ContextEntry -> ContextEntry) -> Context -> Context
    forall a b. (a -> b) -> [a] -> [b]
    map ContextEntry -> ContextEntry
    hideButXs (Context -> Telescope) -> Context -> Telescope
    forall a b. (a -> b) -> a -> b
    $ Context
    contextForAbstracting
          Expr -> Expr -> OutputConstraint' Expr Expr
    forall a b. b -> a -> OutputConstraint' a b
    OfType' Expr
    h (Expr -> OutputConstraint' Expr Expr)
    -> TCM Expr -> TCM (OutputConstraint' Expr Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
            TCM Expr -> TCM Expr
    runInPrintingEnvironment (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
    forall a b. (a -> b) -> a -> b
    $ Type -> TCM (ReifiesTo Type)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
    reify (Type -> TCM (ReifiesTo Type)) -> Type -> TCM (ReifiesTo Type)
    forall a b. (a -> b) -> a -> b
    $ Telescope -> Type -> Type
    telePiVisible Telescope
    tel Type
    a0

         -- If some arguments are not variables (in this case, @args@ is not empty).
         Maybe [Name]
    Nothing -> do
          -- cleanupType relies on with arguments being named 'w',
          -- so we'd better rename any actual 'w's to avoid confusion.
          let tel :: Telescope
    tel = Identity Telescope -> Telescope
    forall a. Identity a -> a
    runIdentity (Identity Telescope -> Telescope)
    -> (Context -> Identity Telescope) -> Context -> Telescope
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ArgName -> Identity ArgName) -> Telescope -> Identity Telescope
    forall (f :: * -> *).
    Applicative f =>
    (ArgName -> f ArgName) -> Telescope -> f Telescope
    onNamesTel ArgName -> Identity ArgName
    forall {a} {m :: * -> *}. (Eq a, IsString a, Monad m) => a -> m a
    unW (Telescope -> Identity Telescope)
    -> (Context -> Telescope) -> Context -> Identity Telescope
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Context -> Telescope
    contextToTel (Context -> Telescope) -> Context -> Telescope
    forall a b. (a -> b) -> a -> b
    $ Context
    contextForAbstracting
          let a :: Type
    a = Identity Type -> Type
    forall a. Identity a -> a
    runIdentity (Identity Type -> Type) -> (Type -> Identity Type) -> Type -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ArgName -> Identity ArgName) -> Type -> Identity Type
    forall (m :: * -> *).
    Applicative m =>
    (ArgName -> m ArgName) -> Type -> m Type
    onNames ArgName -> Identity ArgName
    forall {a} {m :: * -> *}. (Eq a, IsString a, Monad m) => a -> m a
    unW (Type -> Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ Type
    a0
          vtys <- (NamedArg Expr -> TCMT IO (Arg (Term, EqualityView)))
    -> NonEmpty (NamedArg Expr)
    -> TCMT IO (NonEmpty (Arg (Term, EqualityView)))
    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) -> NonEmpty a -> m (NonEmpty b)
    mapM (\ NamedArg Expr
    a -> ((Term, Type) -> Arg (Term, EqualityView))
    -> TCM (Term, Type) -> TCMT IO (Arg (Term, EqualityView))
    forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (ArgInfo -> (Term, EqualityView) -> Arg (Term, EqualityView)
    forall e. ArgInfo -> e -> Arg e
    Arg (NamedArg Expr -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo NamedArg Expr
    a) ((Term, EqualityView) -> Arg (Term, EqualityView))
    -> ((Term, Type) -> (Term, EqualityView))
    -> (Term, Type)
    -> Arg (Term, EqualityView)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Type -> EqualityView) -> (Term, Type) -> (Term, EqualityView)
    forall a b. (a -> b) -> (Term, a) -> (Term, b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Type -> EqualityView
    OtherType) (TCM (Term, Type) -> TCMT IO (Arg (Term, EqualityView)))
    -> TCM (Term, Type) -> TCMT IO (Arg (Term, EqualityView))
    forall a b. (a -> b) -> a -> b
    $ Expr -> TCM (Term, Type)
    inferExpr (Expr -> TCM (Term, Type)) -> Expr -> TCM (Term, Type)
    forall a b. (a -> b) -> a -> b
    $ NamedArg Expr -> Expr
    forall a. NamedArg a -> a
    namedArg NamedArg Expr
    a) (NonEmpty (NamedArg Expr)
     -> TCMT IO (NonEmpty (Arg (Term, EqualityView))))
    -> NonEmpty (NamedArg Expr)
    -> TCMT IO (NonEmpty (Arg (Term, EqualityView)))
    forall a b. (a -> b) -> a -> b
    $
            NonEmpty (NamedArg Expr)
    -> [NamedArg Expr] -> NonEmpty (NamedArg Expr)
    forall a. List1 a -> [a] -> List1 a
    List1.fromListSafe NonEmpty (NamedArg Expr)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ [NamedArg Expr]
    args
          -- Remember the arity of a
          TelV atel _ <- telView a
          let arity = Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    atel
              (delta1, delta2, _, a', vtys') = splitTelForWith tel a vtys
          a <- runInPrintingEnvironment $ do
            reify =<< cleanupType arity args =<< normalForm norm =<< fst <$> withFunctionType delta1 vtys' delta2 a' empty
          reportSDoc "interaction.helper" 10 do
            let extractOtherType = \case { OtherType Type
    a -> Type
    a; EqualityView
    _ -> Type
    forall a. HasCallStack => a
    __IMPOSSIBLE__ }
            let (vs, as)   = List1.unzipWith (fmap extractOtherType . unArg) vtys
            let (vs', as') = List1.unzipWith (fmap extractOtherType . unArg) vtys'
            TP.vcat
              [ "generating helper function"
              , TP.nest 2 $ "tel    = " TP.<+> inTopContext (prettyTCM tel)
              , TP.nest 2 $ "a      = " TP.<+> prettyTCM a
              , TP.nest 2 $ "vs     = " TP.<+> prettyTCM vs
              , TP.nest 2 $ "as     = " TP.<+> prettyTCM as
              , TP.nest 2 $ "delta1 = " TP.<+> inTopContext (prettyTCM delta1)
              , TP.nest 2 $ "delta2 = " TP.<+> inTopContext (addContext delta1 $ prettyTCM delta2)
              , TP.nest 2 $ "a'     = " TP.<+> inTopContext (addContext delta1 $ addContext delta2 $ prettyTCM a')
              , TP.nest 2 $ "as'    = " TP.<+> inTopContext (addContext delta1 $ prettyTCM as')
              , TP.nest 2 $ "vs'    = " TP.<+> inTopContext (addContext delta1 $ prettyTCM vs')
              ]
          return $ OfType' h a
      where
        failure :: TCMT IO a
    failure = InteractionError -> TCMT IO a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    InteractionError -> m a
    interactionError InteractionError
    ExpectedApplication
        ensureName :: ArgName -> ScopeM ()
    ensureName ArgName
    f = do
          ce <- Range -> ArgName -> TCM Expr
    parseExpr Range
    rng ArgName
    f
          flip (caseMaybe $ isName ce) (\ Name
    _ -> () -> ScopeM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()) $ do
             reportSLn "interaction.helper" 10 $ "ce = " ++ show ce
             failure
        isVar :: A.Expr -> Maybe A.Name
        isVar :: Expr -> Maybe Name
    isVar = \case
          A.Var Name
    x -> Name -> Maybe Name
    forall a. a -> Maybe a
    Just Name
    x
          Expr
    _ -> Maybe Name
    forall a. Maybe a
    Nothing
        cleanupType :: Int -> [NamedArg Expr] -> Type -> TCMT IO Type
    cleanupType Int
    arity [NamedArg Expr]
    args Type
    t = do
          -- Get the arity of t
          TelV ttel _ <- Type -> TCMT IO TelView
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m TelView
    telView Type
    t
          -- Compute the number of pi-types subject to stripping.
          let n = Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    ttel Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    arity
          -- It cannot be negative, otherwise we would have performed a
          -- negative number of with-abstractions.
          unless (n >= 0) __IMPOSSIBLE__
          return $ evalState (renameVars $ stripUnused n t) args

        getBody :: Expr -> Expr
    getBody (A.Let ExprInfo
    _ List1 LetBinding
    _ Expr
    e)      = Expr
    e
        getBody Expr
    _                  = Expr
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        -- Strip the non-dependent abstractions from the first n abstractions.
        stripUnused :: a -> Type -> Type
    stripUnused a
    n (El Sort
    s Term
    v) = Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort
    s (Term -> Type) -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $ a -> Term -> Term
    strip a
    n Term
    v
        strip :: a -> Term -> Term
    strip a
    0 = Term -> Term
    forall a. a -> a
    id
        strip a
    n = \case
          I.Pi Dom Type
    a Abs Type
    b -> case a -> Type -> Type
    stripUnused (a
    na -> a -> a
    forall a. Num a => a -> a -> a
    -a
    1) (Type -> Type) -> Abs Type -> Abs Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Abs Type
    b of
            Abs Type
    b | Abs Type -> ArgName
    forall a. Abs a -> ArgName
    absName Abs Type
    b ArgName -> ArgName -> Bool
    forall a. Eq a => a -> a -> Bool
    == ArgName
    "w"   -> Dom Type -> Abs Type -> Term
    I.Pi Dom Type
    a Abs Type
    b
            NoAbs ArgName
    _ Type
    b              -> Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    b
            Abs ArgName
    s Type
    b | Int
    0 Int -> Type -> Bool
    forall a. Free a => Int -> a -> Bool
    `freeIn` Type
    b -> Dom Type -> Abs Type -> Term
    I.Pi (Dom Type -> Dom Type
    forall a. LensHiding a => a -> a
    hide Dom Type
    a) (ArgName -> Type -> Abs Type
    forall a. ArgName -> a -> Abs a
    Abs ArgName
    s Type
    b)
                    | Bool
    otherwise    -> Impossible -> Term -> Term
    forall a. Subst a => Impossible -> a -> a
    strengthen Impossible
    HasCallStack => Impossible
    impossible (Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    b)
          Term
    v -> Term
    v  -- todo: handle if goal type is a Pi

        -- renameVars = onNames (stringToArgName <.> renameVar . argNameToString)
        renameVars :: Type -> State [NamedArg Expr] Type
    renameVars = (ArgName -> StateT [NamedArg Expr] Identity ArgName)
    -> Type -> State [NamedArg Expr] Type
    forall (m :: * -> *).
    Applicative m =>
    (ArgName -> m ArgName) -> Type -> m Type
    onNames ArgName -> StateT [NamedArg Expr] Identity ArgName
    renameVar

        -- onNames :: Applicative m => (ArgName -> m ArgName) -> I.Type -> m I.Type
        onNames :: Applicative m => (String -> m String) -> I.Type -> m I.Type
        onNames :: forall (m :: * -> *).
    Applicative m =>
    (ArgName -> m ArgName) -> Type -> m Type
    onNames ArgName -> m ArgName
    f (El Sort
    s Term
    v) = Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort
    s (Term -> Type) -> m Term -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (ArgName -> m ArgName) -> Term -> m Term
    forall {f :: * -> *}.
    Applicative f =>
    (ArgName -> f ArgName) -> Term -> f Term
    onNamesTm ArgName -> m ArgName
    f Term
    v

        -- onNamesTel :: Applicative f => (ArgName -> f ArgName) -> I.Telescope -> f I.Telescope
        onNamesTel :: Applicative f => (String -> f String) -> I.Telescope -> f I.Telescope
        onNamesTel :: forall (f :: * -> *).
    Applicative f =>
    (ArgName -> f ArgName) -> Telescope -> f Telescope
    onNamesTel ArgName -> f ArgName
    f Telescope
    I.EmptyTel = Telescope -> f Telescope
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Telescope
    forall a. Tele a
    I.EmptyTel
        onNamesTel ArgName -> f ArgName
    f (I.ExtendTel Dom Type
    a Abs Telescope
    b) = Dom Type -> Abs Telescope -> Telescope
    forall a. a -> Abs (Tele a) -> Tele a
    I.ExtendTel (Dom Type -> Abs Telescope -> Telescope)
    -> f (Dom Type) -> f (Abs Telescope -> Telescope)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Type -> f Type) -> Dom Type -> f (Dom Type)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Dom' Term a -> f (Dom' Term b)
    traverse ((ArgName -> f ArgName) -> Type -> f Type
    forall (m :: * -> *).
    Applicative m =>
    (ArgName -> m ArgName) -> Type -> m Type
    onNames ArgName -> f ArgName
    f) Dom Type
    a f (Abs Telescope -> Telescope) -> f (Abs Telescope) -> f Telescope
    forall a b. f (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (ArgName -> f ArgName)
    -> ((ArgName -> f ArgName) -> Telescope -> f Telescope)
    -> Abs Telescope
    -> f (Abs Telescope)
    forall {f :: * -> *} {t} {a}.
    Applicative f =>
    (ArgName -> f ArgName)
    -> ((ArgName -> f ArgName) -> t -> f a) -> Abs t -> f (Abs a)
    onNamesAbs ArgName -> f ArgName
    f (ArgName -> f ArgName) -> Telescope -> f Telescope
    forall (f :: * -> *).
    Applicative f =>
    (ArgName -> f ArgName) -> Telescope -> f Telescope
    onNamesTel Abs Telescope
    b

        onNamesTm :: (ArgName -> f ArgName) -> Term -> f Term
    onNamesTm ArgName -> f ArgName
    f = \case
          I.Var Int
    x Elims
    es   -> Int -> Elims -> Term
    I.Var Int
    x (Elims -> Term) -> f Elims -> f Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (ArgName -> f ArgName) -> Elims -> f Elims
    onNamesElims ArgName -> f ArgName
    f Elims
    es
          I.Def QName
    q Elims
    es   -> QName -> Elims -> Term
    I.Def QName
    q (Elims -> Term) -> f Elims -> f Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (ArgName -> f ArgName) -> Elims -> f Elims
    onNamesElims ArgName -> f ArgName
    f Elims
    es
          I.Con ConHead
    c ConInfo
    ci Elims
    args -> ConHead -> ConInfo -> Elims -> Term
    I.Con ConHead
    c ConInfo
    ci (Elims -> Term) -> f Elims -> f Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (ArgName -> f ArgName) -> Elims -> f Elims
    onNamesArgs ArgName -> f ArgName
    f Elims
    args
          I.Lam ArgInfo
    i Abs Term
    b    -> ArgInfo -> Abs Term -> Term
    I.Lam ArgInfo
    i (Abs Term -> Term) -> f (Abs Term) -> f Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (ArgName -> f ArgName)
    -> ((ArgName -> f ArgName) -> Term -> f Term)
    -> Abs Term
    -> f (Abs Term)
    forall {f :: * -> *} {t} {a}.
    Applicative f =>
    (ArgName -> f ArgName)
    -> ((ArgName -> f ArgName) -> t -> f a) -> Abs t -> f (Abs a)
    onNamesAbs ArgName -> f ArgName
    f (ArgName -> f ArgName) -> Term -> f Term
    onNamesTm Abs Term
    b
          I.Pi Dom Type
    a Abs Type
    b     -> Dom Type -> Abs Type -> Term
    I.Pi (Dom Type -> Abs Type -> Term)
    -> f (Dom Type) -> f (Abs Type -> Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Type -> f Type) -> Dom Type -> f (Dom Type)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Dom' Term a -> f (Dom' Term b)
    traverse ((ArgName -> f ArgName) -> Type -> f Type
    forall (m :: * -> *).
    Applicative m =>
    (ArgName -> m ArgName) -> Type -> m Type
    onNames ArgName -> f ArgName
    f) Dom Type
    a f (Abs Type -> Term) -> f (Abs Type) -> f Term
    forall a b. f (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (ArgName -> f ArgName)
    -> ((ArgName -> f ArgName) -> Type -> f Type)
    -> Abs Type
    -> f (Abs Type)
    forall {f :: * -> *} {t} {a}.
    Applicative f =>
    (ArgName -> f ArgName)
    -> ((ArgName -> f ArgName) -> t -> f a) -> Abs t -> f (Abs a)
    onNamesAbs ArgName -> f ArgName
    f (ArgName -> f ArgName) -> Type -> f Type
    forall (m :: * -> *).
    Applicative m =>
    (ArgName -> m ArgName) -> Type -> m Type
    onNames Abs Type
    b
          I.DontCare Term
    v -> Term -> Term
    I.DontCare (Term -> Term) -> f Term -> f Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (ArgName -> f ArgName) -> Term -> f Term
    onNamesTm ArgName -> f ArgName
    f Term
    v
          v :: Term
    v@I.Lit{}    -> Term -> f Term
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    v
          v :: Term
    v@I.Sort{}   -> Term -> f Term
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    v
          v :: Term
    v@I.Level{}  -> Term -> f Term
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    v
          v :: Term
    v@I.MetaV{}  -> Term -> f Term
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    v
          v :: Term
    v@I.Dummy{}  -> Term -> f Term
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    v
        onNamesElims :: (ArgName -> f ArgName) -> Elims -> f Elims
    onNamesElims ArgName -> f ArgName
    f = (Elim' Term -> f (Elim' Term)) -> Elims -> f Elims
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse ((Elim' Term -> f (Elim' Term)) -> Elims -> f Elims)
    -> (Elim' Term -> f (Elim' Term)) -> Elims -> f Elims
    forall a b. (a -> b) -> a -> b
    $ (Term -> f Term) -> Elim' Term -> f (Elim' Term)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Elim' a -> f (Elim' b)
    traverse ((Term -> f Term) -> Elim' Term -> f (Elim' Term))
    -> (Term -> f Term) -> Elim' Term -> f (Elim' Term)
    forall a b. (a -> b) -> a -> b
    $ (ArgName -> f ArgName) -> Term -> f Term
    onNamesTm ArgName -> f ArgName
    f
        onNamesArgs :: (ArgName -> f ArgName) -> Elims -> f Elims
    onNamesArgs ArgName -> f ArgName
    f  = (Elim' Term -> f (Elim' Term)) -> Elims -> f Elims
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse ((Elim' Term -> f (Elim' Term)) -> Elims -> f Elims)
    -> (Elim' Term -> f (Elim' Term)) -> Elims -> f Elims
    forall a b. (a -> b) -> a -> b
    $ (Term -> f Term) -> Elim' Term -> f (Elim' Term)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Elim' a -> f (Elim' b)
    traverse ((Term -> f Term) -> Elim' Term -> f (Elim' Term))
    -> (Term -> f Term) -> Elim' Term -> f (Elim' Term)
    forall a b. (a -> b) -> a -> b
    $ (ArgName -> f ArgName) -> Term -> f Term
    onNamesTm ArgName -> f ArgName
    f
        onNamesAbs :: (ArgName -> f ArgName)
    -> ((ArgName -> f ArgName) -> t -> f a) -> Abs t -> f (Abs a)
    onNamesAbs ArgName -> f ArgName
    f   = (ArgName -> f ArgName)
    -> (ArgName -> f ArgName)
    -> ((ArgName -> f ArgName) -> t -> f a)
    -> Abs t
    -> f (Abs a)
    forall {f :: * -> *} {t} {t} {a}.
    Applicative f =>
    t
    -> (ArgName -> f ArgName) -> (t -> t -> f a) -> Abs t -> f (Abs a)
    onNamesAbs' ArgName -> f ArgName
    f (ArgName -> ArgName
    stringToArgName (ArgName -> ArgName)
    -> (ArgName -> f ArgName) -> ArgName -> f ArgName
    forall (m :: * -> *) b c a.
    Functor m =>
    (b -> c) -> (a -> m b) -> a -> m c
    <.> ArgName -> f ArgName
    f (ArgName -> f ArgName)
    -> (ArgName -> ArgName) -> ArgName -> f ArgName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ArgName -> ArgName
    argNameToString)
        onNamesAbs' :: t
    -> (ArgName -> f ArgName) -> (t -> t -> f a) -> Abs t -> f (Abs a)
    onNamesAbs' t
    f ArgName -> f ArgName
    f' t -> t -> f a
    nd (Abs   ArgName
    s t
    x) = ArgName -> a -> Abs a
    forall a. ArgName -> a -> Abs a
    Abs   (ArgName -> a -> Abs a) -> f ArgName -> f (a -> Abs a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ArgName -> f ArgName
    f' ArgName
    s f (a -> Abs a) -> f a -> f (Abs a)
    forall a b. f (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> t -> t -> f a
    nd t
    f t
    x
        onNamesAbs' t
    f ArgName -> f ArgName
    f' t -> t -> f a
    nd (NoAbs ArgName
    s t
    x) = ArgName -> a -> Abs a
    forall a. ArgName -> a -> Abs a
    NoAbs (ArgName -> a -> Abs a) -> f ArgName -> f (a -> Abs a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ArgName -> f ArgName
    f' ArgName
    s f (a -> Abs a) -> f a -> f (Abs a)
    forall a b. f (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> t -> t -> f a
    nd t
    f t
    x

        unW :: a -> m a
    unW a
    "w" = a -> m a
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    ".w"
        unW a
    s   = a -> m a
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    s

        renameVar :: ArgName -> StateT [NamedArg Expr] Identity ArgName
    renameVar ArgName
    "w" = StateT [NamedArg Expr] Identity ArgName
    betterName
        renameVar ArgName
    s   = ArgName -> StateT [NamedArg Expr] Identity ArgName
    forall a. a -> StateT [NamedArg Expr] Identity a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ArgName
    s

        betterName :: StateT [NamedArg Expr] Identity ArgName
    betterName = do
          xs <- StateT [NamedArg Expr] Identity [NamedArg Expr]
    forall s (m :: * -> *). MonadState s m => m s
    get
          case xs of
            []         -> StateT [NamedArg Expr] Identity ArgName
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            NamedArg Expr
    arg : [NamedArg Expr]
    args -> do
              [NamedArg Expr] -> StateT [NamedArg Expr] Identity ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put [NamedArg Expr]
    args
              ArgName -> StateT [NamedArg Expr] Identity ArgName
    forall a. a -> StateT [NamedArg Expr] Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ArgName -> StateT [NamedArg Expr] Identity ArgName)
    -> ArgName -> StateT [NamedArg Expr] Identity ArgName
    forall a b. (a -> b) -> a -> b
    $ if
                | Arg ArgInfo
    _ (Named Maybe NamedName
    _ (A.Var Name
    x)) <- NamedArg Expr
    arg -> Name -> ArgName
    forall a. Pretty a => a -> ArgName
    prettyShow (Name -> ArgName) -> Name -> ArgName
    forall a b. (a -> b) -> a -> b
    $ Name -> Name
    A.nameConcrete Name
    x
                | Just ArgName
    x <- NamedArg Expr -> Maybe ArgName
    forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe ArgName
    bareNameOf NamedArg Expr
    arg         -> ArgName -> ArgName
    argNameToString ArgName
    x
                | Bool
    otherwise                        -> ArgName
    "w"

    -- | Gives a list of names and corresponding types.
    --   This list includes not only the local variables in scope, but also the let-bindings.

    contextOfMeta :: InteractionId -> Rewrite -> TCM [ResponseContextEntry]
    contextOfMeta :: InteractionId -> Rewrite -> TCM [ResponseContextEntry]
    contextOfMeta InteractionId
    ii Rewrite
    norm = InteractionId
    -> TCM [ResponseContextEntry] -> TCM [ResponseContextEntry]
    forall (m :: * -> *) a.
    (MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    ii (TCM [ResponseContextEntry] -> TCM [ResponseContextEntry])
    -> TCM [ResponseContextEntry] -> TCM [ResponseContextEntry]
    forall a b. (a -> b) -> a -> b
    $ do
      info <- MetaVariable -> Closure Range
    getMetaInfo (MetaVariable -> Closure Range)
    -> TCMT IO MetaVariable -> TCMT IO (Closure Range)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta (MetaId -> TCMT IO MetaVariable)
    -> TCMT IO MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< InteractionId -> TCMT IO MetaId
    forall (m :: * -> *).
    (ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m MetaId
    lookupInteractionId InteractionId
    ii)
      withMetaInfo info $ do
        -- List of local variables.
        cxt <- getContext
        let localVars = (Int -> ContextEntry -> ContextEntry)
    -> [Int] -> Context -> Context
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Int -> ContextEntry -> ContextEntry
    forall a. Subst a => Int -> a -> a
    raise [Int
    1..] Context
    cxt
        -- List of let-bindings.
        letVars <- Map.toAscList <$> asksTC envLetBindings
        -- Reify the types and filter out bindings without a name.
        (++) <$> forMaybeM (reverse localVars) mkVar
             <*> forMaybeM letVars mkLet

      where
        mkVar :: ContextEntry -> TCM (Maybe ResponseContextEntry)
        mkVar :: ContextEntry -> TCMT IO (Maybe ResponseContextEntry)
    mkVar (CtxVar Name
    name Dom{ domInfo :: forall t e. Dom' t e -> ArgInfo
    domInfo = ArgInfo
    ai, unDom :: forall t e. Dom' t e -> e
    unDom = Type
    t }) = do
          if ArgInfo -> Name -> Bool
    shouldHide ArgInfo
    ai Name
    name then Maybe ResponseContextEntry -> TCMT IO (Maybe ResponseContextEntry)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe ResponseContextEntry
    forall a. Maybe a
    Nothing else ResponseContextEntry -> Maybe ResponseContextEntry
    forall a. a -> Maybe a
    Just (ResponseContextEntry -> Maybe ResponseContextEntry)
    -> TCMT IO ResponseContextEntry
    -> TCMT IO (Maybe ResponseContextEntry)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
            let n :: Name
    n = Name -> Name
    nameConcrete Name
    name
            x  <- Name -> TCMT IO (ConOfAbs Name)
    forall a (m :: * -> *).
    (ToConcrete a, MonadAbsToCon m) =>
    a -> m (ConOfAbs a)
    abstractToConcrete_ Name
    name
            let s = Name -> NameInScope
    forall a. LensInScope a => a -> NameInScope
    C.isInScope Name
    x
            ty <- reifyUnblocked =<< normalForm norm t
            return $ ResponseContextEntry n x (Arg ai ty) Nothing s

        mkLet :: (Name, Open M.LetBinding) -> TCM (Maybe ResponseContextEntry)
        mkLet :: (Name, Open LetBinding) -> TCMT IO (Maybe ResponseContextEntry)
    mkLet (Name
    name, Open LetBinding
    lb) = do
          LetBinding _ tm !dom <- Open LetBinding -> TCMT IO LetBinding
    forall a (m :: * -> *).
    (TermSubst a, MonadTCEnv m) =>
    Open a -> m a
    getOpen Open LetBinding
    lb
          if shouldHide (domInfo dom) name then return Nothing else Just <$> do
            let n = Name -> Name
    nameConcrete Name
    name
            x  <- abstractToConcrete_ name
            let s = Name -> NameInScope
    forall a. LensInScope a => a -> NameInScope
    C.isInScope Name
    x
            ty <- reifyUnblocked =<< normalForm norm dom
                  -- Remove let bindings from x and later, to avoid folding to x = x, or using bindings
                  -- not introduced when x was defined.
            v  <- removeLetBindingsFrom name $ reifyUnblocked =<< normalForm norm tm
            return $ ResponseContextEntry n x ty (Just v) s

        shouldHide :: ArgInfo -> A.Name -> Bool
        shouldHide :: ArgInfo -> Name -> Bool
    shouldHide ArgInfo
    ai Name
    n = Bool -> Bool
    not (ArgInfo -> Bool
    forall a. LensHiding a => a -> Bool
    isInstance ArgInfo
    ai) Bool -> Bool -> Bool
    && (Name -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName Name
    n Bool -> Bool -> Bool
    || Name -> Bool
    nameIsRecordName Name
    n)

    -- | Returns the type of the expression in the current environment
    --   We wake up irrelevant variables just in case the user want to
    --   invoke that command in an irrelevant context.
    typeInCurrent :: Rewrite -> Expr -> TCM Expr
    typeInCurrent :: Rewrite -> Expr -> TCM Expr
    typeInCurrent Rewrite
    norm Expr
    e =
        do  (_,t) <- TCM (Term, Type) -> TCM (Term, Type)
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    wakeIrrelevantVars (TCM (Term, Type) -> TCM (Term, Type))
    -> TCM (Term, Type) -> TCM (Term, Type)
    forall a b. (a -> b) -> a -> b
    $ Expr -> TCM (Term, Type)
    inferExpr Expr
    e
            v <- normalForm norm t
            reifyUnblocked v

    typeInMeta :: InteractionId -> Rewrite -> Expr -> TCM Expr
    typeInMeta :: InteractionId -> Rewrite -> Expr -> TCM Expr
    typeInMeta InteractionId
    ii Rewrite
    norm Expr
    e =
       do   m <- InteractionId -> TCMT IO MetaId
    forall (m :: * -> *).
    (ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m MetaId
    lookupInteractionId InteractionId
    ii
            mi <- getMetaInfo <$> lookupLocalMeta m
            withMetaInfo mi $
                typeInCurrent norm e

    -- | The intro tactic.
    --
    -- Returns the terms (as strings) that can be
    -- used to refine the goal. Uses the coverage checker
    -- to find out which constructors are possible.
    --
    introTactic :: Bool -> InteractionId -> TCM [String]
    introTactic :: Bool -> InteractionId -> TCMT IO Names
    introTactic Bool
    pmLambda InteractionId
    ii = do
      mi <- InteractionId -> TCMT IO MetaId
    forall (m :: * -> *).
    (ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m MetaId
    lookupInteractionId InteractionId
    ii
      mv <- lookupLocalMeta mi
      withMetaInfo (getMetaInfo mv) $ case mvJudgement mv of
        HasType MetaId
    _ Comparison
    _ Type
    t -> do
            t <- Type -> TCMT IO Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Type -> Args -> TCMT IO Type
    forall a (m :: * -> *).
    (PiApplyM a, MonadReduce m, HasBuiltins m) =>
    Type -> a -> m Type
    forall (m :: * -> *).
    (MonadReduce m, HasBuiltins m) =>
    Type -> Args -> m Type
    piApplyM Type
    t (Args -> TCMT IO Type) -> TCMT IO Args -> TCMT IO Type
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO Args
    forall (m :: * -> *). MonadTCEnv m => m Args
    getContextArgs
            -- Andreas, 2013-03-05 Issue 810: skip hidden domains in introduction
            -- of constructor.
            TelV tel' t <- telViewUpTo' (-1) notVisible t
            -- if we cannot introduce a constructor, we try a lambda
            let fallback = do
                  cubical <- Maybe Cubical -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe Cubical -> Bool) -> TCMT IO (Maybe Cubical) -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO (Maybe Cubical)
    forall (m :: * -> *). HasOptions m => m (Maybe Cubical)
    cubicalOption
                  TelV tel _ <- (if cubical then telViewPath else telView) t
                  reportSDoc "interaction.intro" 20 $ TP.sep
                    [ "introTactic/fallback"
                    , "tel' = " TP.<+> prettyTCM tel'
                    , "tel  = " TP.<+> prettyTCM tel
                    ]
                  case (tel', tel) of
                    (Telescope
    EmptyTel, Telescope
    EmptyTel) -> Names -> TCMT IO Names
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
                    (Telescope, Telescope)
    _ -> ListTel -> TCMT IO Names
    introFun (Telescope -> ListTel
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Telescope
    tel' ListTel -> ListTel -> ListTel
    forall a. [a] -> [a] -> [a]
    ++ Telescope -> ListTel
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Telescope
    tel)

            case unEl t of
              I.Def QName
    d Elims
    _ -> do
                def <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d
                case theDef def of
                  Datatype{}    -> Telescope -> TCMT IO Names -> TCMT IO Names
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    tel' (TCMT IO Names -> TCMT IO Names) -> TCMT IO Names -> TCMT IO Names
    forall a b. (a -> b) -> a -> b
    $ AllowAmbiguousNames -> Type -> TCMT IO Names
    introData AllowAmbiguousNames
    AmbiguousNothing Type
    t
                  Record{ recNamedCon :: Defn -> Bool
    recNamedCon = Bool
    name }
                    | Bool
    name      -> Telescope -> TCMT IO Names -> TCMT IO Names
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    tel' (TCMT IO Names -> TCMT IO Names) -> TCMT IO Names -> TCMT IO Names
    forall a b. (a -> b) -> a -> b
    $ AllowAmbiguousNames -> Type -> TCMT IO Names
    introData AllowAmbiguousNames
    AmbiguousConProjs Type
    t
                    | Bool
    otherwise -> Telescope -> TCMT IO Names -> TCMT IO Names
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    tel' (TCMT IO Names -> TCMT IO Names) -> TCMT IO Names -> TCMT IO Names
    forall a b. (a -> b) -> a -> b
    $ QName -> TCMT IO Names
    introRec QName
    d
                  Defn
    _ -> TCMT IO Names
    fallback
              Term
    _ -> TCMT IO Names
    fallback
         TCMT IO Names -> (TCErr -> TCMT IO Names) -> TCMT IO Names
    forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \TCErr
    _ -> Names -> TCMT IO Names
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
        Judgement MetaId
    _ -> TCMT IO Names
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      where
        conName :: [NamedArg SplitPattern] -> [I.ConHead]
        conName :: [NamedArg SplitPattern] -> [ConHead]
    conName [NamedArg SplitPattern
    p] = [ ConHead
    c | I.ConP ConHead
    c ConPatternInfo
    _ [NamedArg SplitPattern]
    _ <- [NamedArg SplitPattern -> SplitPattern
    forall a. NamedArg a -> a
    namedArg NamedArg SplitPattern
    p] ]
        conName [NamedArg SplitPattern]
    _   = [ConHead]
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        showUnambiguousConName :: AllowAmbiguousNames -> ConHead -> TCM String
        showUnambiguousConName :: AllowAmbiguousNames -> ConHead -> TCM ArgName
    showUnambiguousConName AllowAmbiguousNames
    amb ConHead
    c = Doc -> ArgName
    forall a. Doc a -> ArgName
    render (Doc -> ArgName) -> (QName -> Doc) -> QName -> ArgName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty (QName -> ArgName) -> TCMT IO QName -> TCM ArgName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
          AllowAmbiguousNames -> QName -> TCMT IO QName
    forall (m :: * -> *).
    MonadAbsToCon m =>
    AllowAmbiguousNames -> QName -> m QName
    abstractToConcreteQName AllowAmbiguousNames
    amb (QName -> TCMT IO QName) -> QName -> TCMT IO QName
    forall a b. (a -> b) -> a -> b
    $ ConHead -> QName
    I.conName ConHead
    c

        showTCM :: PrettyTCM a => a -> TCM String
        showTCM :: forall a. PrettyTCM a => a -> TCM ArgName
    showTCM = Doc -> ArgName
    forall a. Doc a -> ArgName
    render (Doc -> ArgName) -> (a -> TCMT IO Doc) -> a -> TCM ArgName
    forall (m :: * -> *) b c a.
    Functor m =>
    (b -> c) -> (a -> m b) -> a -> m c
    <.> a -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM

        introFun :: ListTel -> TCM [String]
        introFun :: ListTel -> TCMT IO Names
    introFun ListTel
    tel = Telescope -> TCMT IO Names -> TCMT IO Names
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    tel' (TCMT IO Names -> TCMT IO Names) -> TCMT IO Names -> TCMT IO Names
    forall a b. (a -> b) -> a -> b
    $ do
            ArgName -> Int -> TCMT IO Doc -> ScopeM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "interaction.intro" Int
    10 (TCMT IO Doc -> ScopeM ()) -> TCMT IO Doc -> ScopeM ()
    forall a b. (a -> b) -> a -> b
    $ do TCMT IO Doc
    "introFun" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    TP.<+> Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
    prettyTCM (ListTel -> Telescope
    telFromList ListTel
    tel)
            imp <- TCMT IO Bool
    forall (m :: * -> *). HasOptions m => m Bool
    showImplicitArguments
            let okHiding0 Hiding
    h = Bool
    imp Bool -> Bool -> Bool
    || Hiding
    h Hiding -> Hiding -> Bool
    forall a. Eq a => a -> a -> Bool
    == Hiding
    NotHidden
                -- if none of the vars were displayed, we would get a parse error
                -- thus, we switch to displaying all
                allHidden   = Bool -> Bool
    not ((Hiding -> Bool) -> [Hiding] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Hiding -> Bool
    okHiding0 [Hiding]
    hs)
                okHiding    = if Bool
    allHidden then Bool -> Hiding -> Bool
    forall a b. a -> b -> a
    const Bool
    True else Hiding -> Bool
    okHiding0
            vars <- -- setShowImplicitArguments (imp || allHidden) $
                    applyWhen allHidden withShowAllArguments $
                      mapM showTCM [ setHiding h $ defaultArg $ var i :: Arg Term
                                   | (h, i) <- zip hs $ downFrom n
                                   , okHiding h
                                   ]
            if pmLambda
               then return [ unwords $ ["λ", "{"] ++ vars ++ ["→", "?", "}"] ]
               else return [ unwords $ ["λ"]      ++ vars ++ ["→", "?"] ]
          where
            n :: Int
    n = ListTel -> Int
    forall a. Sized a => a -> Int
    size ListTel
    tel
            hs :: [Hiding]
    hs   = (Dom (ArgName, Type) -> Hiding) -> ListTel -> [Hiding]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom (ArgName, Type) -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding ListTel
    tel
            tel' :: Telescope
    tel' = ListTel -> Telescope
    telFromList [ ((ArgName, Type) -> (ArgName, Type))
    -> Dom (ArgName, Type) -> Dom (ArgName, Type)
    forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (ArgName, Type) -> (ArgName, Type)
    forall {a} {b}. (Eq a, IsString a) => (a, b) -> (a, b)
    makeName Dom (ArgName, Type)
    b | Dom (ArgName, Type)
    b <- ListTel
    tel ]
            makeName :: (a, b) -> (a, b)
    makeName (a
    "_", b
    t) = (a
    "x", b
    t)
            makeName (a
    x, b
    t)   = (a
    x, b
    t)

        contextDimensions :: TCM Int
        contextDimensions :: TCM Int
    contextDimensions = do
          let
            go :: t -> Telescope -> f t
    go t
    n Telescope
    EmptyTel = t -> f t
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure t
    n
            go t
    n (ExtendTel Dom Type
    dom Abs Telescope
    abs) = do
              n' <- Type -> f Bool
    forall (m :: * -> *). (MonadTCM m, MonadReduce m) => Type -> m Bool
    isInterval (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    dom) f Bool -> (Bool -> t) -> f t
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \case
                Bool
    True  -> t
    n t -> t -> t
    forall a. Num a => a -> a -> a
    + t
    1
                Bool
    False -> t
    n
              underAbstraction dom abs $ go n'
          Int -> Telescope -> TCM Int
    forall {f :: * -> *} {t}.
    (MonadTCM f, MonadReduce f, Num t, MonadAddContext f) =>
    t -> Telescope -> f t
    go Int
    0 (Telescope -> TCM Int) -> TCMT IO Telescope -> TCM Int
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO Telescope
    forall (m :: * -> *). MonadTCEnv m => m Telescope
    getContextTelescope

        introData :: AllowAmbiguousNames -> I.Type -> TCM [String]
        introData :: AllowAmbiguousNames -> Type -> TCMT IO Names
    introData AllowAmbiguousNames
    amb Type
    t = do
          let tel :: Telescope
    tel  = ListTel -> Telescope
    telFromList [(ArgName, Type) -> Dom (ArgName, Type)
    forall a. a -> Dom a
    defaultDom (ArgName
    "_", Type
    t)]
              pat :: [Arg (Named name DeBruijnPattern)]
    pat  = [Named name DeBruijnPattern -> Arg (Named name DeBruijnPattern)
    forall a. a -> Arg a
    defaultArg (Named name DeBruijnPattern -> Arg (Named name DeBruijnPattern))
    -> Named name DeBruijnPattern -> Arg (Named name DeBruijnPattern)
    forall a b. (a -> b) -> a -> b
    $ DeBruijnPattern -> Named name DeBruijnPattern
    forall a name. a -> Named name a
    unnamed (DeBruijnPattern -> Named name DeBruijnPattern)
    -> DeBruijnPattern -> Named name DeBruijnPattern
    forall a b. (a -> b) -> a -> b
    $ ArgName -> Int -> DeBruijnPattern
    forall a. DeBruijn a => ArgName -> Int -> a
    deBruijnNamedVar ArgName
    "c" Int
    0]
          -- Gallais, 2023-08-24: #6787 we need to locally ignore the
          -- --without-K or --cubical-compatible options to figure out
          -- that refl is a valid constructor for refl ≡ refl.

          cubical <- Maybe Cubical -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe Cubical -> Bool) -> TCMT IO (Maybe Cubical) -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO (Maybe Cubical)
    forall (m :: * -> *). HasOptions m => m (Maybe Cubical)
    cubicalOption
          r <- (if cubical then id else
                locallyTCState (stPragmaOptions . lensOptWithoutK) (const (Value False)))
               $ splitLast CoInductive tel pat

          -- If --cubical then we often get ambiguity because the coverage
          -- checker says most path constructors could also fit the hole. In
          -- that case we compute the number of interval variables in the
          -- context and drop any clauses that have more IApply patterns (=
          -- constructors that have a higher dimensionality) than the
          -- context.
          dim <- traverse (const contextDimensions) =<< cubicalOption
          let
            dimension SplitClause
    cl = case Maybe Int
    dim of
              Just Int
    n  -> [Int] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length ([NamedArg SplitPattern] -> [Int]
    forall p. IApplyVars p => p -> [Int]
    iApplyVars (SplitClause -> [NamedArg SplitPattern]
    scPats SplitClause
    cl)) Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    n
              Maybe Int
    Nothing -> Bool
    True

          case r of
            Left SplitError
    err -> Names -> TCMT IO Names
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
            Right Covering
    cov ->
               (ConHead -> TCM ArgName) -> [ConHead] -> TCMT IO Names
    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 (AllowAmbiguousNames -> ConHead -> TCM ArgName
    showUnambiguousConName AllowAmbiguousNames
    amb) ([ConHead] -> TCMT IO Names) -> [ConHead] -> TCMT IO Names
    forall a b. (a -> b) -> a -> b
    $ (SplitClause -> [ConHead]) -> [SplitClause] -> [ConHead]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap ([NamedArg SplitPattern] -> [ConHead]
    conName ([NamedArg SplitPattern] -> [ConHead])
    -> (SplitClause -> [NamedArg SplitPattern])
    -> SplitClause
    -> [ConHead]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SplitClause -> [NamedArg SplitPattern]
    scPats) ([SplitClause] -> [ConHead]) -> [SplitClause] -> [ConHead]
    forall a b. (a -> b) -> a -> b
    $ (SplitClause -> Bool) -> [SplitClause] -> [SplitClause]
    forall a. (a -> Bool) -> [a] -> [a]
    filter SplitClause -> Bool
    dimension ([SplitClause] -> [SplitClause]) -> [SplitClause] -> [SplitClause]
    forall a b. (a -> b) -> a -> b
    $ Covering -> [SplitClause]
    splitClauses Covering
    cov

        introRec :: QName -> TCM [String]
        introRec :: QName -> TCMT IO Names
    introRec QName
    d = do
          hfs <- QName -> TCMT IO [Dom Name]
    forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
    QName -> m [Dom Name]
    getRecordFieldNames QName
    d
          fs <- ifM showImplicitArguments
                (return $ map unDom hfs)
                (return [ unDom a | a <- hfs, visible a ])
          let e = KwRange -> Range -> RecordAssignments -> Expr
    C.Rec KwRange
    forall a. Null a => a
    empty Range
    forall a. Range' a
    noRange (RecordAssignments -> Expr) -> RecordAssignments -> Expr
    forall a b. (a -> b) -> a -> b
    $ [Name] -> (Name -> RecordAssignment) -> RecordAssignments
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    for [Name]
    fs ((Name -> RecordAssignment) -> RecordAssignments)
    -> (Name -> RecordAssignment) -> RecordAssignments
    forall a b. (a -> b) -> a -> b
    $ \ Name
    f ->
                FieldAssignment -> RecordAssignment
    forall a b. a -> Either a b
    Left (FieldAssignment -> RecordAssignment)
    -> FieldAssignment -> RecordAssignment
    forall a b. (a -> b) -> a -> b
    $ Name -> Expr -> FieldAssignment
    forall a. Name -> a -> FieldAssignment' a
    C.FieldAssignment Name
    f (Expr -> FieldAssignment) -> Expr -> FieldAssignment
    forall a b. (a -> b) -> a -> b
    $ Range -> Maybe Int -> Expr
    C.QuestionMark Range
    forall a. Range' a
    noRange Maybe Int
    forall a. Maybe a
    Nothing
          return [ prettyShow e ]
          -- Andreas, 2019-02-25, remark:
          -- prettyShow is ok here since we are just printing something like
          -- record { f1 = ? ; ... ; fn = ?}
          -- which does not involve any qualified names, and the fi are C.Name.

    -- | Runs the given computation as if in an anonymous goal at the end
    --   of the top-level module.
    --
    --   Sets up current module, scope, and context.
    atTopLevel :: TCM a -> TCM a
    atTopLevel :: forall a. TCM a -> TCM a
    atTopLevel TCM a
    m = TCM a -> TCM a
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    inConcreteMode (TCM a -> TCM a) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $ do
      let err :: a
    err = a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        -- Andreas, 2024-08-03: cannot trigger this error:
        -- let err = genericError "The file has not been loaded yet."
      TCMT IO (Maybe (ModuleName, TopLevelModuleName))
    -> TCM a -> ((ModuleName, TopLevelModuleName) -> TCM a) -> TCM a
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (Lens' TCState (Maybe (ModuleName, TopLevelModuleName))
    -> TCMT IO (Maybe (ModuleName, TopLevelModuleName))
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (Maybe (ModuleName, TopLevelModuleName)
     -> f (Maybe (ModuleName, TopLevelModuleName)))
    -> TCState -> f TCState
    Lens' TCState (Maybe (ModuleName, TopLevelModuleName))
    stCurrentModule) TCM a
    forall {a}. a
    err (((ModuleName, TopLevelModuleName) -> TCM a) -> TCM a)
    -> ((ModuleName, TopLevelModuleName) -> TCM a) -> TCM a
    forall a b. (a -> b) -> a -> b
    $ \(ModuleName
    current, TopLevelModuleName
    topCurrent) -> do
        TCMT IO (Maybe ModuleInfo)
    -> TCM a -> (ModuleInfo -> TCM a) -> TCM a
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (TopLevelModuleName -> TCMT IO (Maybe ModuleInfo)
    forall (m :: * -> *).
    ReadTCState m =>
    TopLevelModuleName -> m (Maybe ModuleInfo)
    getVisitedModule TopLevelModuleName
    topCurrent) TCM a
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ((ModuleInfo -> TCM a) -> TCM a) -> (ModuleInfo -> TCM a) -> TCM a
    forall a b. (a -> b) -> a -> b
    $ \ ModuleInfo
    mi -> do
          let scope :: ScopeInfo
    scope = Interface -> ScopeInfo
    iInsideScope (Interface -> ScopeInfo) -> Interface -> ScopeInfo
    forall a b. (a -> b) -> a -> b
    $ ModuleInfo -> Interface
    miInterface ModuleInfo
    mi
          tel <- ModuleName -> TCMT IO Telescope
    forall (m :: * -> *).
    (Functor m, ReadTCState m) =>
    ModuleName -> m Telescope
    lookupSection ModuleName
    current
          -- Get the names of the local variables from @scope@
          -- and put them into the context.
          --
          -- Andreas, 2017-04-24, issue #2552:
          --
          -- Delete the let-bound ones, since they are not represented
          -- in the module telescope.
          --
          -- This is a temporary fix until a better solution is available,
          -- e.g., when the module telescope represents let-bound variables.
          --
          -- Unfortunately, referring to let-bound variables
          -- from the top level module telescope will for now result in a not-in-scope error.
          let names :: [A.Name]
              names = (LocalVar -> Name) -> [LocalVar] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map LocalVar -> Name
    localVar ([LocalVar] -> [Name]) -> [LocalVar] -> [Name]
    forall a b. (a -> b) -> a -> b
    $ (LocalVar -> Bool) -> [LocalVar] -> [LocalVar]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ((BindingSource
    LetBound BindingSource -> BindingSource -> Bool
    forall a. Eq a => a -> a -> Bool
    /=) (BindingSource -> Bool)
    -> (LocalVar -> BindingSource) -> LocalVar -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . LocalVar -> BindingSource
    localBindingSource)
                                   ([LocalVar] -> [LocalVar]) -> [LocalVar] -> [LocalVar]
    forall a b. (a -> b) -> a -> b
    $ ((Name, LocalVar) -> LocalVar) -> [(Name, LocalVar)] -> [LocalVar]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name, LocalVar) -> LocalVar
    forall a b. (a, b) -> b
    snd ([(Name, LocalVar)] -> [LocalVar])
    -> [(Name, LocalVar)] -> [LocalVar]
    forall a b. (a -> b) -> a -> b
    $ [(Name, LocalVar)] -> [(Name, LocalVar)]
    forall a. [a] -> [a]
    reverse ([(Name, LocalVar)] -> [(Name, LocalVar)])
    -> [(Name, LocalVar)] -> [(Name, LocalVar)]
    forall a b. (a -> b) -> a -> b
    $ ScopeInfo
    scope ScopeInfo
    -> Lens' ScopeInfo [(Name, LocalVar)] -> [(Name, LocalVar)]
    forall o i. o -> Lens' o i -> i
    ^. ([(Name, LocalVar)] -> f [(Name, LocalVar)])
    -> ScopeInfo -> f ScopeInfo
    Lens' ScopeInfo [(Name, LocalVar)]
    scopeLocals
          -- Andreas, 2016-12-31, issue #2371
          -- The following is an unnecessary complication, as shadowed locals
          -- are not in scope anyway (they are ambiguous).
          -- -- Replace the shadowed names by fresh names (such that they do not shadow imports)
          -- let mnames :: [Maybe A.Name]
          --     mnames = map (notShadowedLocal . snd) $ reverse $ scopeLocals scope
          -- names <- mapM (maybe freshNoName_ return) mnames
          let types :: [Dom I.Type]
              types = (Dom (ArgName, Type) -> Dom Type) -> ListTel -> [Dom Type]
    forall a b. (a -> b) -> [a] -> [b]
    map ((ArgName, Type) -> Type
    forall a b. (a, b) -> b
    snd ((ArgName, Type) -> Type) -> Dom (ArgName, Type) -> Dom Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>) (ListTel -> [Dom Type]) -> ListTel -> [Dom Type]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> ListTel
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Telescope
    tel
              gamma :: ListTel' A.Name
              gamma = ListTel' Name -> Maybe (ListTel' Name) -> ListTel' Name
    forall a. a -> Maybe a -> a
    fromMaybe ListTel' Name
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe (ListTel' Name) -> ListTel' Name)
    -> Maybe (ListTel' Name) -> ListTel' Name
    forall a b. (a -> b) -> a -> b
    $
                        (Name -> Dom Type -> Dom' Term (Name, Type))
    -> [Name] -> [Dom Type] -> Maybe (ListTel' Name)
    forall a b c. (a -> b -> c) -> [a] -> [b] -> Maybe [c]
    zipWith' (\ Name
    x Dom Type
    dom -> (Name
    x,) (Type -> (Name, Type)) -> Dom Type -> Dom' Term (Name, Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom Type
    dom) [Name]
    names [Dom Type]
    types
          reportSDoc "interaction.top" 20 $ TP.vcat
            [ "BasicOps.atTopLevel"
            , "  names = " TP.<+> TP.sep (map prettyA   names)
            , "  types = " TP.<+> TP.sep (map prettyTCM types)
            ]
          M.withCurrentModule current $
            withScope_ scope $
              addContext gamma $ do
                -- We're going inside the top-level module, so we have to set the
                -- checkpoint for it and all its submodules to the new checkpoint.
                cp <- viewTC eCurrentCheckpoint
                stModuleCheckpoints `modifyTCLens` fmap (const cp)
                m

    -- | Parse a name.
    parseName :: Range -> String -> TCM C.QName
    parseName :: Range -> ArgName -> TCMT IO QName
    parseName Range
    r ArgName
    s = do
      e <- Range -> ArgName -> TCM Expr
    parseExpr Range
    r ArgName
    s
      maybe (interactionError $ ExpectedIdentifier e) return $ isQName e

    -- | Check whether an expression is a (qualified) identifier.
    isQName :: C.Expr -> Maybe C.QName
    isQName :: Expr -> Maybe QName
    isQName = \case
      C.Ident QName
    x                    -> QName -> Maybe QName
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return QName
    x
      Expr
    _ -> Maybe QName
    forall a. Maybe a
    Nothing

    isName :: C.Expr -> Maybe C.Name
    isName :: Expr -> Maybe Name
    isName = Expr -> Maybe QName
    isQName (Expr -> Maybe QName)
    -> (QName -> Maybe Name) -> Expr -> Maybe Name
    forall (m :: * -> *) a b c.
    Monad m =>
    (a -> m b) -> (b -> m c) -> a -> m c
    >=> \case
      C.QName Name
    x -> Name -> Maybe Name
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Name
    x
      QName
    _ -> Maybe Name
    forall a. Maybe a
    Nothing

    -- | Returns the contents of the given module or record.

    moduleContents
      :: Rewrite
         -- ^ How should the types be presented?
      -> Range
         -- ^ The range of the next argument.
      -> String
         -- ^ The module name.
      -> TCM ([C.Name], I.Telescope, [(C.Name, I.Type)])
         -- ^ Module names,
         --   context extension needed to print types,
         --   names paired up with corresponding types.

    moduleContents :: Rewrite
    -> Range -> ArgName -> TCM ([Name], Telescope, [(Name, Type)])
    moduleContents Rewrite
    norm Range
    rng ArgName
    s = Call
    -> TCM ([Name], Telescope, [(Name, Type)])
    -> TCM ([Name], Telescope, [(Name, Type)])
    forall a. Call -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
    traceCall Call
    ModuleContents (TCM ([Name], Telescope, [(Name, Type)])
     -> TCM ([Name], Telescope, [(Name, Type)]))
    -> TCM ([Name], Telescope, [(Name, Type)])
    -> TCM ([Name], Telescope, [(Name, Type)])
    forall a b. (a -> b) -> a -> b
    $ do
      if ArgName -> Bool
    forall a. Null a => a -> Bool
    null (ArgName -> ArgName
    trim ArgName
    s) then Rewrite -> Maybe QName -> TCM ([Name], Telescope, [(Name, Type)])
    getModuleContents Rewrite
    norm Maybe QName
    forall a. Maybe a
    Nothing else do
      e <- Range -> ArgName -> TCM Expr
    parseExpr Range
    rng ArgName
    s
      case isQName e of
        -- If the expression is not a single identifier, it is not a module name
        -- and treated as a record expression.
        Maybe QName
    Nothing -> Rewrite -> Expr -> TCM ([Name], Telescope, [(Name, Type)])
    getRecordContents Rewrite
    norm Expr
    e
        -- Otherwise, if it is not in scope as a module name, it is treated
        -- as a record name.
        Just QName
    x  -> do
          ms :: [AbstractModule] <- QName -> ScopeInfo -> [AbstractModule]
    forall a. InScope a => QName -> ScopeInfo -> [a]
    scopeLookup QName
    x (ScopeInfo -> [AbstractModule])
    -> TCMT IO ScopeInfo -> TCMT IO [AbstractModule]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO ScopeInfo
    forall (m :: * -> *). ReadTCState m => m ScopeInfo
    getScope
          if null ms then getRecordContents norm e else getModuleContents norm $ Just x

    -- | Returns the contents of the given record identifier.

    getRecordContents
      :: Rewrite  -- ^ Amount of normalization in types.
      -> C.Expr   -- ^ Expression presumably of record type.
      -> TCM ([C.Name], I.Telescope, [(C.Name, I.Type)])
                  -- ^ Module names,
                  --   context extension,
                  --   names paired up with corresponding types.
    getRecordContents :: Rewrite -> Expr -> TCM ([Name], Telescope, [(Name, Type)])
    getRecordContents Rewrite
    norm Expr
    ce = do
      (_, t) <- Expr -> TCM (Term, Type)
    inferExpr (Expr -> TCM (Term, Type)) -> TCM Expr -> TCM (Term, Type)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Expr -> ScopeM (AbsOfCon Expr)
    forall c. ToAbstract c => c -> ScopeM (AbsOfCon c)
    toAbstract Expr
    ce
      isRecordType t >>= \case
        Maybe (QName, Args, RecordData)
    Nothing -> TypeError -> TCM ([Name], Telescope, [(Name, Type)])
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ([Name], Telescope, [(Name, Type)]))
    -> TypeError -> TCM ([Name], Telescope, [(Name, Type)])
    forall a b. (a -> b) -> a -> b
    $ Type -> TypeError
    ShouldBeRecordType Type
    t
        Just (QName
    q, Args
    vs, RecordData{ _recFields :: RecordData -> [Dom QName]
    _recFields = [Dom QName]
    fs, _recTel :: RecordData -> Telescope
    _recTel = Telescope
    rtel }) -> do
          let xs :: [Name]
    xs   = (Dom QName -> Name) -> [Dom QName] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name -> Name
    nameConcrete (Name -> Name) -> (Dom QName -> Name) -> Dom QName -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Name
    qnameName (QName -> Name) -> (Dom QName -> QName) -> Dom QName -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom QName -> QName
    forall t e. Dom' t e -> e
    unDom) [Dom QName]
    fs
              tel :: Telescope
    tel  = Telescope -> Args -> Telescope
    forall t. Apply t => t -> Args -> t
    apply Telescope
    rtel Args
    vs
              doms :: [Dom Type]
    doms = Telescope -> [Dom Type]
    forall a. TermSubst a => Tele (Dom a) -> [Dom a]
    flattenTel Telescope
    tel
          -- Andreas, 2019-04-10, issue #3687: use flattenTel
          -- to bring types into correct scope.
          ArgName -> Int -> TCMT IO Doc -> ScopeM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "interaction.contents.record" Int
    20 (TCMT IO Doc -> ScopeM ()) -> TCMT IO Doc -> ScopeM ()
    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
    TP.vcat
            [ TCMT IO Doc
    "getRecordContents"
            , TCMT IO Doc
    "  cxt  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    TP.<+> (Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
    prettyTCM (Telescope -> TCMT IO Doc) -> TCMT IO Telescope -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO Telescope
    forall (m :: * -> *). MonadTCEnv m => m Telescope
    getContextTelescope)
            , TCMT IO Doc
    "  tel  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    TP.<+> Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
    prettyTCM Telescope
    tel
            , TCMT IO Doc
    "  doms = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    TP.<+> [Dom Type] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => [Dom Type] -> m Doc
    prettyTCM [Dom Type]
    doms
            , TCMT IO Doc
    "  doms'= " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    TP.<+> Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    tel ([Dom Type] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => [Dom Type] -> m Doc
    prettyTCM [Dom Type]
    doms)
            ]
          ts <- (Dom Type -> TCMT IO Type) -> [Dom Type] -> TCMT IO [Type]
    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 (Rewrite -> Type -> TCMT IO Type
    forall t.
    (Reduce t, Simplify t, Instantiate t, Normalise t) =>
    Rewrite -> t -> TCM t
    normalForm Rewrite
    norm (Type -> TCMT IO Type)
    -> (Dom Type -> Type) -> Dom Type -> TCMT IO Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom) [Dom Type]
    doms
          return ([], tel, zip xs ts)

    -- | Returns the contents of the given module.

    getModuleContents
      :: Rewrite
           -- ^ Amount of normalization in types.
      -> Maybe C.QName
           -- ^ Module name, @Nothing@ if top-level module.
      -> TCM ([C.Name], I.Telescope, [(C.Name, I.Type)])
           -- ^ Module names,
           --   context extension,
           --   names paired up with corresponding types.
    getModuleContents :: Rewrite -> Maybe QName -> TCM ([Name], Telescope, [(Name, Type)])
    getModuleContents Rewrite
    norm Maybe QName
    mm = do
      modScope <- case Maybe QName
    mm of
        Maybe QName
    Nothing -> TCMT IO Scope
    getCurrentScope
        Just QName
    m  -> ModuleName -> TCMT IO Scope
    getNamedScope (ModuleName -> TCMT IO Scope)
    -> (AbstractModule -> ModuleName)
    -> AbstractModule
    -> TCMT IO Scope
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbstractModule -> ModuleName
    amodName (AbstractModule -> TCMT IO Scope)
    -> TCMT IO AbstractModule -> TCMT IO Scope
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< QName -> TCMT IO AbstractModule
    resolveModule QName
    m
      let modules :: ThingsInScope AbstractModule
          modules = Scope -> ThingsInScope AbstractModule
    forall a. InScope a => Scope -> ThingsInScope a
    exportedNamesInScope Scope
    modScope
          names :: ThingsInScope AbstractName
          names = Scope -> ThingsInScope AbstractName
    forall a. InScope a => Scope -> ThingsInScope a
    exportedNamesInScope Scope
    modScope
          xns = [ (Name
    x,AbstractName
    n) | (Name
    x, List1 AbstractName
    ns) <- ThingsInScope AbstractName -> [(Name, List1 AbstractName)]
    forall k a. Map k a -> [(k, a)]
    Map.toList ThingsInScope AbstractName
    names, AbstractName
    n <- List1 AbstractName -> [Item (List1 AbstractName)]
    forall l. IsList l => l -> [Item l]
    List1.toList List1 AbstractName
    ns ]
      types <- forMaybeM xns $ \(Name
    x, AbstractName
    n) -> do
        QName -> TCMT IO (Either SigError Definition)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Either SigError Definition)
    getConstInfo' (AbstractName -> QName
    anameName AbstractName
    n) TCMT IO (Either SigError Definition)
    -> (Either SigError Definition -> TCMT IO (Maybe (Name, Type)))
    -> TCMT IO (Maybe (Name, Type))
    forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          Right Definition
    d -> do
            t <- Rewrite -> Type -> TCMT IO Type
    forall t.
    (Reduce t, Simplify t, Instantiate t, Normalise t) =>
    Rewrite -> t -> TCM t
    normalForm Rewrite
    norm (Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (Definition -> Type
    defType (Definition -> Type) -> TCMT IO Definition -> TCMT IO Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Definition -> TCMT IO Definition
    forall (m :: * -> *).
    (Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
     MonadTCEnv m, MonadDebug m) =>
    Definition -> m Definition
    instantiateDef Definition
    d)
            return $ Just (x, t)
          Left{} -> Maybe (Name, Type) -> TCMT IO (Maybe (Name, Type))
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (Name, Type)
    forall a. Maybe a
    Nothing
      return (Map.keys modules, EmptyTel, types)

    whyInScope :: FilePath -> String -> TCM WhyInScopeData
    whyInScope :: ArgName -> ArgName -> TCM WhyInScopeData
    whyInScope ArgName
    cwd ArgName
    s = do
      x     <- Range -> ArgName -> TCMT IO QName
    parseName Range
    forall a. Range' a
    noRange ArgName
    s
      scope <- getScope
      return $ WhyInScopeData
        x
        cwd
        (lookup x $ map (first C.QName) $ scope ^. scopeLocals)
        (scopeLookup x scope)
        (scopeLookup x scope)