    {-# OPTIONS_GHC -Wunused-imports #-}

    {-# LANGUAGE NondecreasingIndentation #-}

    module Agda.TypeChecking.InstanceArguments
      ( findInstance
      , isInstanceConstraint
      , solveAwakeInstanceConstraints
      , shouldPostponeInstanceSearch
      , postponeInstanceConstraints
      , flushInstanceConstraints
      , getInstanceCandidates
      , getInstanceDefs
      , OutputTypeName(..)
      , getOutputTypeName
      , addTypedInstance
      , readdTypedInstance
      , addTypedInstance'
      , pruneTemporaryInstances
      , resolveInstanceHead
      ) where

    import Control.Monad.Except   (ExceptT(..), runExceptT, MonadError(..))

    import qualified Data.Map.Strict as Map
    import qualified Data.Set as Set
    import qualified Data.List as List
    import Data.Function (on)
    import Data.Monoid hiding ((<>))
    import Data.Foldable (toList, foldrM)

    import Agda.Interaction.Options (optQualifiedInstances, lensOptExperimentalLazyInstances)

    import Agda.Syntax.Common
    import Agda.Syntax.Concrete.Name (isQualified)
    import Agda.Syntax.Position
    import Agda.Syntax.Internal as I
    import Agda.Syntax.Internal.MetaVars
    import Agda.Syntax.Scope.Base (isNameInScope, inverseScopeLookupName', AllowAmbiguousNames(..))

    import qualified Agda.TypeChecking.Monad.Benchmark as Bench
    import Agda.TypeChecking.Conversion.Pure (pureEqualTermB)
    import Agda.TypeChecking.Errors () --instance only
    import Agda.TypeChecking.Implicit (implicitArgs)
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Records
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Warnings
    import Agda.TypeChecking.Datatypes

    import {-# SOURCE #-} Agda.TypeChecking.Constraints
    import {-# SOURCE #-} Agda.TypeChecking.Conversion

    import qualified Agda.Benchmarking as Benchmark
    import Agda.TypeChecking.Monad.Benchmark (billTo)

    import Agda.Utils.Lens
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Size
    import Agda.Utils.Tuple
    import Agda.Syntax.Common.Pretty (prettyShow)

    import qualified Agda.Utils.ProfileOptions as Profile
    -- import qualified Agda.Utils.HashTable as HashTable
    import Agda.Utils.WithDefault (lensCollapseDefault)
    import Agda.Utils.Impossible
    -- import Agda.Utils.HashTable (HashTable)

    import Agda.TypeChecking.DiscrimTree
    -- import GHC.IO (unsafePerformIO)

    -- | Compute a list of instance candidates.
    --   'Nothing' if target type or any context type is a meta, error if
    --   type is not eligible for instance search.
    initialInstanceCandidates :: Bool -> Type -> TCM (Either Blocker [Candidate])
    initialInstanceCandidates :: Bool -> Type -> TCM (Either Blocker [Candidate])
    initialInstanceCandidates Bool
    blockOverlap Type
    instTy = do
      (_, _, otn) <- Type -> TCM (Telescope, Term, OutputTypeName)
    getOutputTypeName Type
    instTy
      case otn of
        OutputTypeName
    NoOutputTypeName -> TypeError -> TCM (Either Blocker [Candidate])
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM (Either Blocker [Candidate]))
    -> TypeError -> TCM (Either Blocker [Candidate])
    forall a b. (a -> b) -> a -> b
    $ Type -> WhyInvalidInstanceType -> TypeError
    InvalidInstanceHeadType Type
    instTy WhyInvalidInstanceType
    ImproperInstHead
        OutputTypeName
    OutputTypeVisiblePi -> TypeError -> TCM (Either Blocker [Candidate])
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM (Either Blocker [Candidate]))
    -> TypeError -> TCM (Either Blocker [Candidate])
    forall a b. (a -> b) -> a -> b
    $ Type -> WhyInvalidInstanceType -> TypeError
    InvalidInstanceHeadType Type
    instTy WhyInvalidInstanceType
    ImproperInstTele
        OutputTypeNameNotYetKnown Blocker
    b -> do
          [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.instance.cands" Int
    30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Instance type is not yet known. "
          Either Blocker [Candidate] -> TCM (Either Blocker [Candidate])
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Blocker -> Either Blocker [Candidate]
    forall a b. a -> Either a b
    Left Blocker
    b)
        OutputTypeName
    OutputTypeVar -> do
          [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.instance.cands" Int
    30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Instance type is a variable. "
          BlockT (TCMT IO) [Candidate] -> TCM (Either Blocker [Candidate])
    forall (m :: * -> *) a.
    Monad m =>
    BlockT m a -> m (Either Blocker a)
    runBlocked (Maybe QName -> BlockT (TCMT IO) [Candidate]
    getContextCands Maybe QName
    forall a. Maybe a
    Nothing)
        OutputTypeName QName
    n -> Account (BenchPhase (TCMT IO))
    -> TCM (Either Blocker [Candidate])
    -> TCM (Either Blocker [Candidate])
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [BenchPhase (TCMT IO)
    Phase
    Bench.Typing, BenchPhase (TCMT IO)
    Phase
    Bench.InstanceSearch, BenchPhase (TCMT IO)
    Phase
    Bench.InitialCandidates] do
          [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.instance.cands" Int
    30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Found instance type head: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    n
          BlockT (TCMT IO) [Candidate] -> TCM (Either Blocker [Candidate])
    forall (m :: * -> *) a.
    Monad m =>
    BlockT m a -> m (Either Blocker a)
    runBlocked do
            local  <- Maybe QName -> BlockT (TCMT IO) [Candidate]
    getContextCands (QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    n)
            global <- getScopeDefs n
            lift $ tickCandidates n $ length local + length global
            pure $ local <> global
      where
        -- Ticky profiling for statistics about a class.
        tickCandidates :: a -> a -> m ()
    tickCandidates a
    n a
    size = ProfileOption -> m () -> m ()
    forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
    whenProfile ProfileOption
    Profile.Instances do
          n <- a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM a
    n
          let pref = [Char]
    "class " [Char] -> [Char] -> [Char]
    forall a. Semigroup a => a -> a -> a
    <> Doc -> [Char]
    forall a. Show a => a -> [Char]
    show Doc
    n

          -- Number of instance constraints of this class that have gotten a
          -- set of candidates
          tick $ pref <> ": attempts"
          -- Per-class info: number of constraints where there was only one
          -- candidate (awesome) + the total number of candidates we've gone
          -- through.
          when (size == 1) $ tick $ pref <> ": only one candidate"
          when (size >= 1) $ tickN
            (pref <> ": total candidates visited")
            (fromIntegral size)

        -- get a list of variables with their type, relative to current context
        getContextCands :: Maybe QName -> BlockT TCM [Candidate]
        getContextCands :: Maybe QName -> BlockT (TCMT IO) [Candidate]
    getContextCands Maybe QName
    cls = do
          ctx <- BlockT (TCMT IO) Context
    forall (m :: * -> *). MonadTCEnv m => m Context
    getContext
          reportSDoc "tc.instance.cands" 40 $ hang "Getting candidates from context" 2 (inTopContext $ prettyTCM $ PrettyContext ctx)
              -- Context variables with their types lifted to live in the full context
          let varsAndRaisedTypes = [(Term, Dom Type)] -> [(Term, Dom Type)]
    forall a. [a] -> [a]
    reverse ([(Term, Dom Type)] -> [(Term, Dom Type)])
    -> [(Term, Dom Type)] -> [(Term, Dom Type)]
    forall a b. (a -> b) -> a -> b
    $ [Term] -> [Dom Type] -> [(Term, Dom Type)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip (Context -> [Term]
    contextTerms Context
    ctx) (Telescope -> [Dom Type]
    forall a. TermSubst a => Tele (Dom a) -> [Dom a]
    flattenTel (Telescope -> [Dom Type]) -> Telescope -> [Dom Type]
    forall a b. (a -> b) -> a -> b
    $ Context -> Telescope
    contextToTel Context
    ctx)
              vars = [ CandidateKind -> Term -> Type -> OverlapMode -> Candidate
    Candidate CandidateKind
    LocalCandidate Term
    x Type
    t (ArgInfo -> OverlapMode
    forall a. LensArgInfo a => a -> OverlapMode
    infoOverlapMode ArgInfo
    info)
                     | (Term
    x, Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
    domInfo = ArgInfo
    info, unDom :: forall t e. Dom' t e -> e
    unDom = Type
    t}) <- [(Term, Dom Type)]
    varsAndRaisedTypes
                     , ArgInfo -> Bool
    forall a. LensHiding a => a -> Bool
    isInstance ArgInfo
    info
                     ]

          -- {{}}-fields of variables are also candidates
          let cxtAndTypes = [ (CandidateKind
    LocalCandidate, Term
    x, Type
    t) | (Term
    x, Dom{unDom :: forall t e. Dom' t e -> e
    unDom = Type
    t}) <- [(Term, Dom Type)]
    varsAndRaisedTypes ]
          fields <- concat <$> mapM instanceFields (reverse cxtAndTypes)
          reportSDoc "tc.instance.fields" 30 $
            if null fields then "no instance field candidates" else
              "instance field candidates" $$ do
                nest 2 $ vcat (map debugCandidate fields)

          -- get let bindings
          env <- asksTC envLetBindings
          env <- mapM (traverse getOpen) $ Map.toList env
          let lets = [ CandidateKind -> Term -> Type -> OverlapMode -> Candidate
    Candidate CandidateKind
    LocalCandidate Term
    v Type
    t OverlapMode
    DefaultOverlap
                     | (Name
    _, LetBinding Origin
    _ Term
    v Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
    domInfo = ArgInfo
    info, unDom :: forall t e. Dom' t e -> e
    unDom = Type
    t}) <- [(Name, LetBinding)]
    env
                     , ArgInfo -> Bool
    forall a. LensHiding a => a -> Bool
    isInstance ArgInfo
    info
                     , ArgInfo -> Bool
    forall a. LensModality a => a -> Bool
    usableModality ArgInfo
    info
                     ]
          filterM (sameHead cls . candidateType) $ vars ++ fields ++ lets

        sameHead :: Maybe QName -> Type -> BlockT TCM Bool
        sameHead :: Maybe QName -> Type -> BlockT (TCMT IO) Bool
    sameHead Maybe QName
    Nothing Type
    _ = Bool -> BlockT (TCMT IO) Bool
    forall a. a -> BlockT (TCMT IO) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    True
        sameHead (Just QName
    cls) Type
    t = TCM OutputTypeName -> BlockT (TCMT IO) OutputTypeName
    forall (m :: * -> *) a. Monad m => m a -> BlockT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift ((Telescope, Term, OutputTypeName) -> OutputTypeName
    forall a b c. (a, b, c) -> c
    thd3 ((Telescope, Term, OutputTypeName) -> OutputTypeName)
    -> TCM (Telescope, Term, OutputTypeName) -> TCM OutputTypeName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> TCM (Telescope, Term, OutputTypeName)
    getOutputTypeName Type
    t) BlockT (TCMT IO) OutputTypeName
    -> (OutputTypeName -> BlockT (TCMT IO) Bool)
    -> BlockT (TCMT IO) Bool
    forall a b.
    BlockT (TCMT IO) a
    -> (a -> BlockT (TCMT IO) b) -> BlockT (TCMT IO) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          OutputTypeName            QName
    inst -> Bool -> BlockT (TCMT IO) Bool
    forall a. a -> BlockT (TCMT IO) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (QName
    inst QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    cls)
          OutputTypeNameNotYetKnown Blocker
    b    -> Blocker -> BlockT (TCMT IO) Bool
    forall a. Blocker -> BlockT (TCMT IO) a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    b
          OutputTypeName
    _                              -> Bool -> BlockT (TCMT IO) Bool
    forall a. a -> BlockT (TCMT IO) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    False

        infoOverlapMode :: LensArgInfo a => a -> OverlapMode
        infoOverlapMode :: forall a. LensArgInfo a => a -> OverlapMode
    infoOverlapMode a
    info = if ArgInfo -> Bool
    forall a. LensHiding a => a -> Bool
    isYesOverlap (a -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo a
    info) then OverlapMode
    FieldOverlap else OverlapMode
    DefaultOverlap

        etaExpand :: (MonadTCM m, PureTCM m)
                  => Bool -> Type -> m (Maybe (QName, Args))
        etaExpand :: forall (m :: * -> *).
    (MonadTCM m, PureTCM m) =>
    Bool -> Type -> m (Maybe (QName, Args))
    etaExpand Bool
    etaOnce Type
    t =
          Type -> m (Maybe (QName, Args))
    forall (m :: * -> *).
    HasConstInfo m =>
    Type -> m (Maybe (QName, Args))
    isEtaRecordType Type
    t m (Maybe (QName, Args))
    -> (Maybe (QName, Args) -> m (Maybe (QName, Args)))
    -> m (Maybe (QName, Args))
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
            Maybe (QName, Args)
    Nothing | Bool
    etaOnce -> do
              Type -> m (Maybe (QName, Args, RecordData))
    forall (m :: * -> *).
    PureTCM m =>
    Type -> m (Maybe (QName, Args, RecordData))
    isRecordType Type
    t m (Maybe (QName, Args, RecordData))
    -> (Maybe (QName, Args, RecordData) -> m (Maybe (QName, Args)))
    -> m (Maybe (QName, Args))
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
                Maybe (QName, Args, RecordData)
    Nothing         -> Maybe (QName, Args) -> m (Maybe (QName, Args))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (QName, Args)
    forall a. Maybe a
    Nothing
                Just (QName
    r, Args
    vs, RecordData
    _) -> do
                  m <- m ModuleName
    forall (m :: * -> *). MonadTCEnv m => m ModuleName
    currentModule
                  -- Are we inside the record module? If so it's safe and desirable
                  -- to eta-expand once (issue #2320).
                  if qnameToList0 r `List.isPrefixOf` mnameToList m
                    then return (Just (r, vs))
                    else return Nothing
            Maybe (QName, Args)
    r -> Maybe (QName, Args) -> m (Maybe (QName, Args))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (QName, Args)
    r

        instanceFields :: (CandidateKind,Term,Type) -> BlockT TCM [Candidate]
        instanceFields :: (CandidateKind, Term, Type) -> BlockT (TCMT IO) [Candidate]
    instanceFields = Bool -> (CandidateKind, Term, Type) -> BlockT (TCMT IO) [Candidate]
    instanceFields' Bool
    True

        instanceFields' :: Bool -> (CandidateKind,Term,Type) -> BlockT TCM [Candidate]
        instanceFields' :: Bool -> (CandidateKind, Term, Type) -> BlockT (TCMT IO) [Candidate]
    instanceFields' Bool
    etaOnce (CandidateKind
    q, Term
    v, Type
    t) =
          Type
    -> (Blocker -> Type -> BlockT (TCMT IO) [Candidate])
    -> (NotBlocked -> Type -> BlockT (TCMT IO) [Candidate])
    -> BlockT (TCMT IO) [Candidate]
    forall t (m :: * -> *) a.
    (Reduce t, IsMeta t, MonadReduce m) =>
    t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
    ifBlocked Type
    t (\ Blocker
    m Type
    _ -> Blocker -> BlockT (TCMT IO) [Candidate]
    forall a. Blocker -> BlockT (TCMT IO) a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    m) ((NotBlocked -> Type -> BlockT (TCMT IO) [Candidate])
     -> BlockT (TCMT IO) [Candidate])
    -> (NotBlocked -> Type -> BlockT (TCMT IO) [Candidate])
    -> BlockT (TCMT IO) [Candidate]
    forall a b. (a -> b) -> a -> b
    $ \ NotBlocked
    _ Type
    t -> do
          BlockT (TCMT IO) (Maybe (QName, Args))
    -> BlockT (TCMT IO) [Candidate]
    -> ((QName, Args) -> BlockT (TCMT IO) [Candidate])
    -> BlockT (TCMT IO) [Candidate]
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (Bool -> Type -> BlockT (TCMT IO) (Maybe (QName, Args))
    forall (m :: * -> *).
    (MonadTCM m, PureTCM m) =>
    Bool -> Type -> m (Maybe (QName, Args))
    etaExpand Bool
    etaOnce Type
    t) ([Candidate] -> BlockT (TCMT IO) [Candidate]
    forall a. a -> BlockT (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []) (((QName, Args) -> BlockT (TCMT IO) [Candidate])
     -> BlockT (TCMT IO) [Candidate])
    -> ((QName, Args) -> BlockT (TCMT IO) [Candidate])
    -> BlockT (TCMT IO) [Candidate]
    forall a b. (a -> b) -> a -> b
    $ \ (QName
    r, Args
    pars) -> do
            (tel, args) <- TCM (Telescope, Args) -> BlockT (TCMT IO) (Telescope, Args)
    forall (m :: * -> *) a. Monad m => m a -> BlockT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM (Telescope, Args) -> BlockT (TCMT IO) (Telescope, Args))
    -> TCM (Telescope, Args) -> BlockT (TCMT IO) (Telescope, Args)
    forall a b. (a -> b) -> a -> b
    $ QName -> Args -> Term -> TCM (Telescope, Args)
    forall (m :: * -> *).
    (HasConstInfo m, MonadDebug m, ReadTCState m,
     MonadError TCErr m) =>
    QName -> Args -> Term -> m (Telescope, Args)
    forceEtaExpandRecord QName
    r Args
    pars Term
    v
            let types = (Dom Type -> Type) -> [Dom Type] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom ([Dom Type] -> [Type]) -> [Dom Type] -> [Type]
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg [Dom Type]) -> [Dom Type] -> [Dom Type]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst ([SubstArg [Dom Type]] -> Substitution' (SubstArg [Dom Type])
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS ([SubstArg [Dom Type]] -> Substitution' (SubstArg [Dom Type]))
    -> [SubstArg [Dom Type]] -> Substitution' (SubstArg [Dom Type])
    forall a b. (a -> b) -> a -> b
    $ [SubstArg [Dom Type]] -> [SubstArg [Dom Type]]
    forall a. [a] -> [a]
    reverse ([SubstArg [Dom Type]] -> [SubstArg [Dom Type]])
    -> [SubstArg [Dom Type]] -> [SubstArg [Dom Type]]
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Term) -> Args -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Term
    forall e. Arg e -> e
    unArg Args
    args) (Telescope -> [Dom Type]
    forall a. TermSubst a => Tele (Dom a) -> [Dom a]
    flattenTel Telescope
    tel)
            fmap concat $ forM (zip args types) $ \ (Arg Term
    arg, Type
    t) ->
              ([ CandidateKind -> Term -> Type -> OverlapMode -> Candidate
    Candidate CandidateKind
    LocalCandidate (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    arg) Type
    t (Arg Term -> OverlapMode
    forall a. LensArgInfo a => a -> OverlapMode
    infoOverlapMode Arg Term
    arg)
               | Arg Term -> Bool
    forall a. LensHiding a => a -> Bool
    isInstance Arg Term
    arg
               ] [Candidate] -> [Candidate] -> [Candidate]
    forall a. [a] -> [a] -> [a]
    ++) ([Candidate] -> [Candidate])
    -> BlockT (TCMT IO) [Candidate] -> BlockT (TCMT IO) [Candidate]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
              Bool -> (CandidateKind, Term, Type) -> BlockT (TCMT IO) [Candidate]
    instanceFields' Bool
    False (CandidateKind
    LocalCandidate, Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    arg, Type
    t)

        -- Compute whether we should block this instance constraint at the
        -- discrimination tree stage.
        shouldBlockOverlap :: Blocker -> Set.Set QName -> TCM Bool
        shouldBlockOverlap :: Blocker -> Set QName -> TCM Bool
    shouldBlockOverlap Blocker
    bs Set QName
    cands = do
          let
            recursive :: TCM Bool
    recursive = Lens' TCState Bool -> TCM Bool
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (Bool -> f Bool) -> TCState -> f TCState
    Lens' TCState Bool
    stConsideringInstance
            hack :: TCM Bool
    hack      = Lens' TCState Bool -> TCM Bool
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (Bool -> f Bool) -> TCState -> f TCState
    Lens' TCState Bool
    stInstanceHack
            enabled :: TCM Bool
    enabled   = Lens' TCState Bool -> TCM Bool
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC ((PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
    Lens' TCState PragmaOptions
    stPragmaOptions ((PragmaOptions -> f PragmaOptions) -> TCState -> f TCState)
    -> ((Bool -> f Bool) -> PragmaOptions -> f PragmaOptions)
    -> (Bool -> f Bool)
    -> TCState
    -> f TCState
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptExperimentalLazyInstances ((WithDefault 'False -> f (WithDefault 'False))
     -> PragmaOptions -> f PragmaOptions)
    -> ((Bool -> f Bool)
        -> WithDefault 'False -> f (WithDefault 'False))
    -> (Bool -> f Bool)
    -> PragmaOptions
    -> f PragmaOptions
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Bool -> f Bool) -> WithDefault 'False -> f (WithDefault 'False)
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    Lens' (WithDefault' a b) a
    Lens' (WithDefault 'False) Bool
    lensCollapseDefault)
            mutual :: TCMT IO (Set QName)
    mutual    = TCMT IO (Maybe MutualId)
    -> TCMT IO (Set QName)
    -> (MutualId -> TCMT IO (Set QName))
    -> TCMT IO (Set QName)
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM ((TCEnv -> Maybe MutualId) -> TCMT IO (Maybe MutualId)
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Maybe MutualId
    envMutualBlock) (Set QName -> TCMT IO (Set QName)
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Set QName
    forall a. Monoid a => a
    mempty) \ MutualId
    mb ->
              MutualBlock -> Set QName
    mutualNames (MutualBlock -> Set QName)
    -> TCMT IO MutualBlock -> TCMT IO (Set QName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MutualId -> TCMT IO MutualBlock
    forall (tcm :: * -> *).
    ReadTCState tcm =>
    MutualId -> tcm MutualBlock
    lookupMutualBlock MutualId
    mb

          [TCM Bool] -> TCM Bool
    forall (f :: * -> *) (m :: * -> *).
    (Foldable f, Monad m) =>
    f (m Bool) -> m Bool
    andM
            [ Bool -> TCM Bool
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    blockOverlap
              -- For the getInstances reflection primitive, we don't want
              -- to block on overlap, so that the user can do their thing.

            , TCM Bool
    enabled
              -- Also disable it depending on the pragma option.

            , Bool -> TCM Bool
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> TCM Bool) -> Bool -> TCM Bool
    forall a b. (a -> b) -> a -> b
    $ Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Set MetaId -> Bool
    forall a. Set a -> Bool
    Set.null (Set MetaId -> Bool) -> Set MetaId -> Bool
    forall a b. (a -> b) -> a -> b
    $ Blocker -> Set MetaId
    allBlockingMetas Blocker
    bs
              -- Don't block if there's no metas to block on

            , Bool -> TCM Bool
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> TCM Bool) -> Bool -> TCM Bool
    forall a b. (a -> b) -> a -> b
    $ Set QName -> Peano
    forall a. Sized a => a -> Peano
    natSize Set QName
    cands Peano -> Peano -> Bool
    forall a. Ord a => a -> a -> Bool
    > Peano
    1
              -- It's possible that the discrimination tree forced a
              -- metavariable even if there's exactly one candidate. In this
              -- case, we should not block, because this instance constraint
              -- might be the only thing that can solve the blocking metas.

            , Bool -> Bool
    not (Bool -> Bool) -> TCM Bool -> TCM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCM Bool
    hack
              -- To support 'inert improvement' (see ImproveInertRHS), we
              -- try all the candidates even if the discrimination tree
              -- thinks that there will be overlap. This is because it's
              -- possible we have e.g.
              --
              --   instance ?1 : Foo ?0, candidates {Foo T, Foo S}
              --      blocker ?0
              --   ?0 X = T X (blocked on ?0)
              --
              -- If we block ?1 on ?0 again (as we would've done during the
              -- body), then both of these go unsolved. But if we try all
              -- the candidates, we'll see that 'Foo T' is the only possible
              -- candidate, thus solving both constraints.

            , TCMT IO (Set QName)
    mutual TCMT IO (Set QName) -> (Set QName -> Bool) -> TCM Bool
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> (Set QName -> Set QName -> Bool
    forall a. Ord a => Set a -> Set a -> Bool
    `Set.disjoint` Set QName
    cands)
              -- Work around for #7186: the result of termination checking
              -- depends on whether we solve instance metas eagerly or late.
              -- Consider
              --
              --   instance Show-List = record { show = go }
              --   go (x ∷ xs) = show x <> show ⦃ ?0 ⦄ xs
              --
              -- If we solve ?0 eagerly, the term we use is the literal
              -- record constructor. The 'show' projection unfolds in 'go'
              -- and the termination check is happy.
              --
              -- If we solve it late, we run the risk of the clause
              -- compiler applying copattern translation to Show-List. The
              -- 'show' projection does not eagerly unfold, and the
              -- termination check explodes.

            , Bool -> Bool
    not (Bool -> Bool) -> TCM Bool -> TCM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCM Bool
    recursive
              -- Blocking instance selection *on a meta* while considering
              -- an instance causes the recursive instance constraint to
              -- get repeatedly woken up. Not good for performance.
            ]

        getScopeDefs :: QName -> BlockT TCM [Candidate]
        getScopeDefs :: QName -> BlockT (TCMT IO) [Candidate]
    getScopeDefs QName
    n = do
          rel <- Lens' TCEnv Relevance -> BlockT (TCMT IO) Relevance
    forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
    viewTC (Relevance -> f Relevance) -> TCEnv -> f TCEnv
    Lens' TCEnv Relevance
    eRelevance

          InstanceTable tree counts <- lift getInstanceDefs
          QueryResult qs blocker <- lift $ lookupDT (unEl instTy) tree

          reportSDoc "tc.instance.candidates.search" 20 $ vcat
            [ "instance candidates from signature for goal:"
            , nest 2 (prettyTCM =<< instantiateFull instTy)
            , nest 2 (prettyTCM qs)
            , "length:" <+> prettyTCM (length qs)
            , "blocker:"
            , nest 2 (prettyTCM blocker)
            ]

          cands <- catMaybes <$> mapM (lift . candidate rel) (toList qs)

          should <- lift (shouldBlockOverlap blocker qs)
          when (length cands > 1 && should) do
            reportSDoc "tc.instance.defer" 20 $ vcat
              [ "Postponing because of discrimination tree overlap."
              ]
            patternViolation blocker

          -- Some more class-specific profiling.
          lift $ whenProfile Profile.Instances case Map.lookup n counts of
            Just Int
    tot -> do
              n <- QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    n
              -- Record the overall total number of candidates that were
              -- skipped by lookup in the discrimination tree, and record
              -- this per-class, as well.
              let diff = Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int
    tot Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - [Candidate] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Candidate]
    cands)
              tickN "instances discarded early" diff
              tickN ("class " <> show n <> ": discarded early") diff
            Maybe Int
    Nothing  -> () -> TCMT IO ()
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()

          pure cands

        candidate :: Relevance -> QName -> TCM (Maybe Candidate)
        candidate :: Relevance -> QName -> TCM (Maybe Candidate)
    candidate Relevance
    rel QName
    q = TCM Bool
    -> TCM (Maybe Candidate)
    -> TCM (Maybe Candidate)
    -> TCM (Maybe Candidate)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifNotM (QName -> ScopeInfo -> Bool
    isNameInScope QName
    q (ScopeInfo -> Bool) -> TCMT IO ScopeInfo -> TCM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO ScopeInfo
    forall (m :: * -> *). ReadTCState m => m ScopeInfo
    getScope) (Maybe Candidate -> TCM (Maybe Candidate)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Candidate
    forall a. Maybe a
    Nothing) (TCM (Maybe Candidate) -> TCM (Maybe Candidate))
    -> TCM (Maybe Candidate) -> TCM (Maybe Candidate)
    forall a b. (a -> b) -> a -> b
    $ do
          -- Jesper, 2020-03-16: When using --no-qualified-instances,
          -- filter out instances that are only in scope under a qualified
          -- name.
          TCM (Maybe Candidate) -> TCM (Maybe Candidate)
    filterQualified (TCM (Maybe Candidate) -> TCM (Maybe Candidate))
    -> TCM (Maybe Candidate) -> TCM (Maybe Candidate)
    forall a b. (a -> b) -> a -> b
    $ do
          -- Andreas, 2012-07-07:
          -- we try to get the info for q
          -- while opening a module, q may be in scope but not in the signature
          -- in this case, we just ignore q (issue 674)
          (TCM (Maybe Candidate)
     -> (TCErr -> TCM (Maybe Candidate)) -> TCM (Maybe Candidate))
    -> (TCErr -> TCM (Maybe Candidate))
    -> TCM (Maybe Candidate)
    -> TCM (Maybe Candidate)
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip TCM (Maybe Candidate)
    -> (TCErr -> TCM (Maybe Candidate)) -> TCM (Maybe Candidate)
    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 -> TCM (Maybe Candidate)
    forall {m :: * -> *} {a}.
    MonadError TCErr m =>
    TCErr -> m (Maybe a)
    handle (TCM (Maybe Candidate) -> TCM (Maybe Candidate))
    -> TCM (Maybe Candidate) -> TCM (Maybe Candidate)
    forall a b. (a -> b) -> a -> b
    $ do
            def <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
            if not (getRelevance def `moreRelevant` rel) then return Nothing else do
              -- Andreas, 2017-01-14: instantiateDef is a bit of an overkill
              -- if we anyway get the freeVarsToApply
              -- WAS: t <- defType <$> instantiateDef def
              args <- freeVarsToApply q
              let
                t   = Definition -> Type
    defType Definition
    def Type -> Args -> Type
    `piApply` Args
    args
                rel = ArgInfo -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance (ArgInfo -> Relevance) -> ArgInfo -> Relevance
    forall a b. (a -> b) -> a -> b
    $ Definition -> ArgInfo
    defArgInfo Definition
    def

                v = case Definition -> Defn
    theDef Definition
    def of
                  -- drop parameters if it's a projection function...
                  Function{ funProjection :: Defn -> Either ProjectionLikenessMissing Projection
    funProjection = Right Projection
    p } -> Projection -> ProjOrigin -> Relevance -> Args -> Term
    projDropParsApply Projection
    p ProjOrigin
    ProjSystem Relevance
    rel Args
    args

                  -- Andreas, 2014-08-19: constructors cannot be declared as
                  -- instances (at least as of now).
                  -- I do not understand why the Constructor case is not impossible.
                  -- Ulf, 2014-08-20: constructors are always instances.
                  Constructor{ conSrcCon :: Defn -> ConHead
    conSrcCon = ConHead
    c }       -> ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ConOSystem []
                  Defn
    _                                  -> QName -> Elims -> Term
    Def QName
    q (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Elim) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply Args
    args

                mode = case Definition -> Maybe InstanceInfo
    defInstance Definition
    def of
                  Just InstanceInfo
    i  -> InstanceInfo -> OverlapMode
    instanceOverlap InstanceInfo
    i
                  Maybe InstanceInfo
    Nothing -> OverlapMode
    DefaultOverlap

              -- Amy, 2025-04-10: it's possible that an instance in the
              -- discrimination tree has a type which, in the current
              -- context, has visible quantifiers (e.g. because we're
              -- outside the parametrised module it was defined in).
              --
              -- Discard them early so that they don't count towards
              -- potentially blocking on "overlap".
              TelV tele _ <- telView t
              return do
                guard (all (not . visible) tele)
                Just $ Candidate (GlobalCandidate q) v t mode
          where
            -- unbound constant throws an internal error
            handle :: TCErr -> m (Maybe a)
    handle (TypeError CallStack
    _ TCState
    _ (Closure {clValue :: forall a. Closure a -> a
    clValue = InternalError [Char]
    _})) = Maybe a -> m (Maybe a)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe a
    forall a. Maybe a
    Nothing
            handle TCErr
    err                                                   = TCErr -> m (Maybe a)
    forall a. TCErr -> m a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError TCErr
    err

            filterQualified :: TCM (Maybe Candidate) -> TCM (Maybe Candidate)
            filterQualified :: TCM (Maybe Candidate) -> TCM (Maybe Candidate)
    filterQualified TCM (Maybe Candidate)
    m = TCM Bool
    -> TCM (Maybe Candidate)
    -> TCM (Maybe Candidate)
    -> TCM (Maybe Candidate)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (PragmaOptions -> Bool
    optQualifiedInstances (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions) TCM (Maybe Candidate)
    m (TCM (Maybe Candidate) -> TCM (Maybe Candidate))
    -> TCM (Maybe Candidate) -> TCM (Maybe Candidate)
    forall a b. (a -> b) -> a -> b
    $ do
              qc <- AllowAmbiguousNames -> QName -> ScopeInfo -> [QName]
    inverseScopeLookupName' AllowAmbiguousNames
    AmbiguousAnything QName
    q (ScopeInfo -> [QName]) -> TCMT IO ScopeInfo -> TCMT IO [QName]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO ScopeInfo
    forall (m :: * -> *). ReadTCState m => m ScopeInfo
    getScope
              let isQual = Bool -> (QName -> Bool) -> Maybe QName -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Bool
    True QName -> Bool
    isQualified (Maybe QName -> Bool) -> Maybe QName -> Bool
    forall a b. (a -> b) -> a -> b
    $ [QName] -> Maybe QName
    forall a. [a] -> Maybe a
    listToMaybe [QName]
    qc
              reportSDoc "tc.instance.qualified" 30 $
                if isQual then
                  "dropping qualified instance" <+> prettyTCM q
                else
                  "keeping instance" <+> prettyTCM q <+>
                  "since it is in scope as" <+> prettyTCM qc
              if isQual then return Nothing else m

    -- | @findInstance m (v,a)s@ tries to instantiate on of the types @a@s
    --   of the candidate terms @v@s to the type @t@ of the metavariable @m@.
    --   If successful, meta @m@ is solved with the instantiation of @v@.
    --   If unsuccessful, the constraint is regenerated, with possibly reduced
    --   candidate set.
    --   The list of candidates is equal to @Nothing@ when the type of the meta
    --   wasn't known when the constraint was generated. In that case, try to find
    --   its type again.
    findInstance :: MetaId -> Maybe [Candidate] -> TCM ()
    findInstance :: MetaId -> Maybe [Candidate] -> TCMT IO ()
    findInstance MetaId
    m Maybe [Candidate]
    Nothing = do
      r <- MetaId -> TCMT IO Range
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m Range
    getMetaRange MetaId
    m
      ifM canDropRecursiveInstance (addConstraint neverUnblock (FindInstance r m Nothing)) $ do
      -- Getting initial candidates can fail, in which case we should postpone (#7286)
      catchConstraint (FindInstance r m Nothing) $ do
      -- Andreas, 2015-02-07: New metas should be created with range of the
      -- current instance meta, thus, we set the range.
      mv <- lookupLocalMeta m
      setCurrentRange mv $ do
        reportSLn "tc.instance" 20 $ "The type of the FindInstance constraint isn't known, trying to find it again."
        t <- instantiate =<< getMetaTypeInContext m
        reportSLn "tc.instance" 70 $ "findInstance 1: t: " ++ prettyShow t

        -- Issue #2577: If the target is a function type the arguments are
        -- potential candidates, so we add them to the context to make
        -- initialInstanceCandidates pick them up.
        TelV tel t <- telViewUpTo' (-1) notVisible t
        cands <- addContext tel $ initialInstanceCandidates True t
        case cands of
          Left Blocker
    unblock -> do
            [Char] -> Int -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.instance" Int
    20 [Char]
    "Can't figure out target of instance goal. Postponing constraint."
            Blocker -> Constraint -> TCMT IO ()
    forall (m :: * -> *).
    MonadConstraint m =>
    Blocker -> Constraint -> m ()
    addConstraint Blocker
    unblock (Constraint -> TCMT IO ()) -> Constraint -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Range -> MetaId -> Maybe [Candidate] -> Constraint
    FindInstance Range
    r MetaId
    m Maybe [Candidate]
    forall a. Maybe a
    Nothing
          Right [Candidate]
    cs -> MetaId -> Maybe [Candidate] -> TCMT IO ()
    findInstance MetaId
    m ([Candidate] -> Maybe [Candidate]
    forall a. a -> Maybe a
    Just [Candidate]
    cs)

    findInstance MetaId
    m (Just [Candidate]
    cands) = do                       -- Note: if no blocking meta variable this will not unblock until the end of the mutual block
      r <- MetaId -> TCMT IO Range
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m Range
    getMetaRange MetaId
    m
      whenJustM (findInstance' m cands) $ (\ ([Candidate]
    cands, Blocker
    b) -> Blocker -> Constraint -> TCMT IO ()
    forall (m :: * -> *).
    MonadConstraint m =>
    Blocker -> Constraint -> m ()
    addConstraint Blocker
    b (Constraint -> TCMT IO ()) -> Constraint -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Range -> MetaId -> Maybe [Candidate] -> Constraint
    FindInstance Range
    r MetaId
    m (Maybe [Candidate] -> Constraint)
    -> Maybe [Candidate] -> Constraint
    forall a b. (a -> b) -> a -> b
    $ [Candidate] -> Maybe [Candidate]
    forall a. a -> Maybe a
    Just [Candidate]
    cands)

    -- | Entry point for `tcGetInstances` primitive
    getInstanceCandidates :: MetaId -> TCM (Either Blocker [Candidate])
    getInstanceCandidates :: MetaId -> TCM (Either Blocker [Candidate])
    getInstanceCandidates MetaId
    m = TCM (Either Blocker [Candidate])
    wrapper where
      wrapper :: TCM (Either Blocker [Candidate])
    wrapper = do
        mv <- MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    m
        setCurrentRange mv $ do
          t <- instantiate =<< getMetaTypeInContext m
          TelV tel t' <- telViewUpTo' (-1) notVisible t
          addContext tel $ runExceptT (worker t')

      insertCandidate :: Candidate -> [Candidate] -> TCM [Candidate]
      insertCandidate :: Candidate -> [Candidate] -> TCM [Candidate]
    insertCandidate Candidate
    x []     = [Candidate] -> TCM [Candidate]
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [Candidate
    x]
      insertCandidate Candidate
    x (Candidate
    y:[Candidate]
    xs) = Candidate -> Candidate -> TCM Bool
    doesCandidateSpecialise Candidate
    x Candidate
    y TCM Bool -> (Bool -> TCM [Candidate]) -> TCM [Candidate]
    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
        Bool
    True  -> [Candidate] -> TCM [Candidate]
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Candidate
    xCandidate -> [Candidate] -> [Candidate]
    forall a. a -> [a] -> [a]
    :Candidate
    yCandidate -> [Candidate] -> [Candidate]
    forall a. a -> [a] -> [a]
    :[Candidate]
    xs)
        Bool
    False -> (Candidate
    yCandidate -> [Candidate] -> [Candidate]
    forall a. a -> [a] -> [a]
    :) ([Candidate] -> [Candidate]) -> TCM [Candidate] -> TCM [Candidate]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Candidate -> [Candidate] -> TCM [Candidate]
    insertCandidate Candidate
    x [Candidate]
    xs

      worker :: Type -> ExceptT Blocker TCM [Candidate]
      worker :: Type -> ExceptT Blocker (TCMT IO) [Candidate]
    worker Type
    t' = do
        cands <- TCM (Either Blocker [Candidate])
    -> ExceptT Blocker (TCMT IO) [Candidate]
    forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
    ExceptT (Bool -> Type -> TCM (Either Blocker [Candidate])
    initialInstanceCandidates Bool
    False Type
    t')
        cands <- lift (checkCandidates m t' cands) <&> \case
          Maybe ([(Candidate, TCErr)], [(Candidate, Term)])
    Nothing         -> [Candidate]
    cands
          Just ([(Candidate, TCErr)]
    _, [(Candidate, Term)]
    cands) -> (Candidate, Term) -> Candidate
    forall a b. (a, b) -> a
    fst ((Candidate, Term) -> Candidate)
    -> [(Candidate, Term)] -> [Candidate]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [(Candidate, Term)]
    cands
        cands <- Bench.billTo [Bench.Typing, Bench.InstanceSearch, Bench.OrderCandidates] $
          lift (foldrM insertCandidate [] cands)

        reportSDoc "tc.instance.sort" 20 $ nest 2 $
          "sorted candidates" $$ vcat (map debugCandidate cands)

        pure cands

    -- | @'doesCandidateSpecialise' c1 c2@ checks whether the instance
    -- candidate @c1@ /specialises/ the instance candidate @c2@, i.e.,
    -- whether the type of @c2@ is a substitution instance of @c1@'s type.
    --
    -- Only the final return type of the instances is considered: the
    -- presence of unsolvable instance arguments in the types of @c1@ or
    -- @c2@ does not affect the results of 'doesCandidateSpecialise'.
    doesCandidateSpecialise :: Candidate -> Candidate -> TCM Bool
    doesCandidateSpecialise :: Candidate -> Candidate -> TCM Bool
    doesCandidateSpecialise c1 :: Candidate
    c1@Candidate{candidateType :: Candidate -> Type
    candidateType = Type
    t1} c2 :: Candidate
    c2@Candidate{candidateType :: Candidate -> Type
    candidateType = Type
    t2} = do
      ProfileOption -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
    whenProfile ProfileOption
    Profile.Instances (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TCMT IO ()
    forall (m :: * -> *). MonadStatistics m => [Char] -> m ()
    tick [Char]
    "doesCandidateSpecialise"

      -- We compare
      --    c1 : ∀ {Γ} → T
      -- against
      --    c2 : ∀ {Δ} → S
      -- by moving to the context Γ ⊢, so that any variables in T's type are
      -- "rigid", but *instantiating* S[?/Δ], so its variables are
      -- "flexible"; then calling the conversion checker.

      let
        handle :: a -> m Bool
    handle a
    e = do
          [Char] -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.instance.sort" Int
    30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 TCMT IO Doc
    "=> NOT specialisation"
          [Char] -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.instance.sort" Int
    40 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ a -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM a
    e
          Bool -> m Bool
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    False

        wrap :: TCM Bool -> TCM Bool
    wrap = (TCM Bool -> (TCErr -> TCM Bool) -> TCM Bool)
    -> (TCErr -> TCM Bool) -> TCM Bool -> TCM Bool
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip TCM Bool -> (TCErr -> TCM Bool) -> TCM Bool
    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 -> TCM Bool
    forall {m :: * -> *} {a}.
    (MonadDebug m, PrettyTCM a) =>
    a -> m Bool
    handle
            -- Turn failures into returning false
            (TCM Bool -> TCM Bool)
    -> (TCM Bool -> TCM Bool) -> TCM Bool -> TCM Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCM Bool -> TCM Bool
    forall a. TCM a -> TCM a
    localTCState
            -- Discard any changes to the TC state (metas from
            -- instantiating t2, recursive instance constraints, etc)
            (TCM Bool -> TCM Bool)
    -> (TCM Bool -> TCM Bool) -> TCM Bool -> TCM Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Lens' TCState Bool -> (Bool -> Bool) -> TCM Bool -> TCM Bool
    forall a b. Lens' TCState a -> (a -> a) -> TCMT IO b -> TCMT IO 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
    stPostponeInstanceSearch (Bool -> Bool -> Bool
    forall a b. a -> b -> a
    const Bool
    True)
            -- Don't spend any time looking for instances in the contexts
            (TCM Bool -> TCM Bool)
    -> (TCM Bool -> TCM Bool) -> TCM Bool -> TCM Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCM Bool -> TCM Bool
    forall (m :: * -> *) a. ReadTCState m => m a -> m a
    nowConsideringInstance
            -- Don't execute tactics either

      TelV tel t1 <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView Type
    t1
      addContext tel $ wrap $ do
        -- Amy, 2025-02-28: Have to raise the type of the other candidate to
        -- live in t1's context!
        (args, t2) <- implicitArgs (-1) (\Hiding
    h -> Hiding -> Bool
    forall a. LensHiding a => a -> Bool
    notVisible Hiding
    h) (raise (length tel) t2)

        reportSDoc "tc.instance.sort" 30 $ "Does" <+> prettyTCM (raise (length tel) c1) <+> "specialise" <+> (prettyTCM (raise (length tel) c2) <> "?")
        reportSDoc "tc.instance.sort" 60 $ vcat
          [ "Comparing candidate"
          , nest 2 (prettyTCM c1 <+> colon <+> prettyTCM t1)
          , "vs"
          , nest 2 (prettyTCM c2 <+> colon <+> prettyTCM t2)
          ]

        leqType t2 t1
        reportSDoc "tc.instance.sort" 30 $ nest 2 "=> IS specialisation"
        pure True

    -- | Checks whether an instance overlaps another. This involves a strict
    -- specificity check (the new instance should be more specific than the
    -- old instance but not vice-versa) and the consideration of whether
    -- these instances are overlappable/overlapping at all.
    --
    -- Fails early if the new candidate is not overlapping and the old
    -- candidate is not overlappable.
    doesCandidateOverlap :: Candidate -> Candidate -> TCM Bool
    doesCandidateOverlap :: Candidate -> Candidate -> TCM Bool
    doesCandidateOverlap Candidate
    new Candidate
    old = if Candidate -> Bool
    forall a. HasOverlapMode a => a -> Bool
    isOverlapping Candidate
    new Bool -> Bool -> Bool
    || Candidate -> Bool
    forall a. HasOverlapMode a => a -> Bool
    isOverlappable Candidate
    old
      then [TCM Bool] -> TCM Bool
    forall (f :: * -> *) (m :: * -> *).
    (Foldable f, Monad m) =>
    f (m Bool) -> m Bool
    andM [ Candidate -> Candidate -> TCM Bool
    doesCandidateSpecialise Candidate
    new Candidate
    old
                , (Bool -> Bool) -> TCM Bool -> TCM 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 (Candidate -> Candidate -> TCM Bool
    doesCandidateSpecialise Candidate
    old Candidate
    new) ]
      else Bool -> TCM Bool
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    False

    -- | Result says whether we need to add constraint, and if so, the set of
    --   remaining candidates and an eventual blocking metavariable.
    findInstance' :: MetaId -> [Candidate] -> TCM (Maybe ([Candidate], Blocker))
    findInstance' :: MetaId -> [Candidate] -> TCMT IO (Maybe ([Candidate], Blocker))
    findInstance' MetaId
    m [Candidate]
    cands = do
      let
        frozen :: TCMT IO (Maybe ([Candidate], Blocker))
    frozen = do
          [Char] -> Int -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.instance.defer" Int
    20 [Char]
    "Refusing to solve frozen instance meta."
          ProfileOption -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
    whenProfile ProfileOption
    Profile.Instances (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TCMT IO ()
    forall (m :: * -> *). MonadStatistics m => [Char] -> m ()
    tick [Char]
    "findInstance: frozen"
          Maybe ([Candidate], Blocker)
    -> TCMT IO (Maybe ([Candidate], Blocker))
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (([Candidate], Blocker) -> Maybe ([Candidate], Blocker)
    forall a. a -> Maybe a
    Just ([Candidate]
    cands, Blocker
    neverUnblock))

        recursive :: TCMT IO (Maybe ([Candidate], Blocker))
    recursive = do
          recur <- Lens' TCState Bool -> TCM Bool
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (Bool -> f Bool) -> TCState -> f TCState
    Lens' TCState Bool
    stConsideringInstance
          reportSLn "tc.instance.defer" 20
            if recur
              then "Postponing recursive instance search."
              else "Postponing possibly recursive instance search."
          whenProfile Profile.Instances $ tick "findInstance: recursive"
          return $ Just (cands, neverUnblock)

      TCM Bool
    -> TCMT IO (Maybe ([Candidate], Blocker))
    -> TCMT IO (Maybe ([Candidate], Blocker))
    -> TCMT IO (Maybe ([Candidate], Blocker))
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (MetaId -> TCM Bool
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m Bool
    isFrozen MetaId
    m) TCMT IO (Maybe ([Candidate], Blocker))
    frozen do
      TCM Bool
    -> TCMT IO (Maybe ([Candidate], Blocker))
    -> TCMT IO (Maybe ([Candidate], Blocker))
    -> TCMT IO (Maybe ([Candidate], Blocker))
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM TCM Bool
    forall (m :: * -> *). (ReadTCState m, HasOptions m) => m Bool
    shouldPostponeInstanceSearch TCMT IO (Maybe ([Candidate], Blocker))
    recursive do
      Account (BenchPhase (TCMT IO))
    -> TCMT IO (Maybe ([Candidate], Blocker))
    -> TCMT IO (Maybe ([Candidate], Blocker))
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    billTo [BenchPhase (TCMT IO)
    Phase
    Benchmark.Typing, BenchPhase (TCMT IO)
    Phase
    Benchmark.InstanceSearch] do

      -- Andreas, 2015-02-07: New metas should be created with range of the
      -- current instance meta, thus, we set the range.
      mv <- MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    m
      setCurrentRange mv $ do
          reportSLn "tc.instance" 15 $
            "findInstance 2: constraint: " ++ prettyShow m ++ "; candidates left: " ++ show (length cands)
          reportSDoc "tc.instance" 60 $ nest 2 $ vcat $ map debugCandidate cands
          reportSDoc "tc.instance" 70 $ "raw" $$ do
           nest 2 $ vcat $ map debugCandidateRaw cands

          t <- getMetaTypeInContext m
          reportSLn "tc.instance" 70 $ "findInstance 2: t: " ++ prettyShow t

          insidePi t $ \ Type
    t -> do
          [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.instance" Int
    15 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "findInstance 3: t =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t
          [Char] -> Int -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.instance" Int
    70 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "findInstance 3: t: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Type -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Type
    t

          mcands <-
            -- Temporarily remove other instance constraints to avoid
            -- redundant solution attempts
            (ConstraintStatus -> ProblemConstraint -> Bool)
    -> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
    -> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
    forall a.
    (ConstraintStatus -> ProblemConstraint -> Bool) -> TCM a -> TCM a
    holdConstraints ((ProblemConstraint -> Bool)
    -> ConstraintStatus -> ProblemConstraint -> Bool
    forall a b. a -> b -> a
    const ProblemConstraint -> Bool
    isInstanceProblemConstraint) (TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
     -> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)])))
    -> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
    -> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
    forall a b. (a -> b) -> a -> b
    $
            MetaId
    -> Type
    -> [Candidate]
    -> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
    checkCandidates MetaId
    m Type
    t [Candidate]
    cands

          debugConstraints
          case mcands of
            Just ([(Candidate
    _, TCErr
    err)], []) -> do
              [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.instance" Int
    15 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
                TCMT IO Doc
    "findInstance 5: the only viable candidate failed..."
              TCErr -> TCMT IO (Maybe ([Candidate], Blocker))
    forall a. TCErr -> TCMT IO a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError TCErr
    err

            Just ([(Candidate, TCErr)]
    errs, []) -> do
              if [(Candidate, TCErr)] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(Candidate, TCErr)]
    errs then [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.instance" Int
    15 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "findInstance 5: no viable candidate found..."
                           else [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.instance" Int
    15 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "findInstance 5: all viable candidates failed..."
              -- #3676: Sort the candidates based on the size of the range for the errors and
              --        set the range of the full error to the range of the most precise candidate
              --        error.
              let sortedErrs :: [(Candidate, TCErr)]
    sortedErrs = ((Candidate, TCErr) -> (Candidate, TCErr) -> Ordering)
    -> [(Candidate, TCErr)] -> [(Candidate, TCErr)]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    List.sortBy (Word32 -> Word32 -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Word32 -> Word32 -> Ordering)
    -> ((Candidate, TCErr) -> Word32)
    -> (Candidate, TCErr)
    -> (Candidate, TCErr)
    -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` (Candidate, TCErr) -> Word32
    precision) [(Candidate, TCErr)]
    errs
                    where precision :: (Candidate, TCErr) -> Word32
    precision (Candidate
    _, TCErr
    err) = Word32
    -> (Interval' () -> Word32) -> Maybe (Interval' ()) -> Word32
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Word32
    infinity Interval' () -> Word32
    forall a. Interval' a -> Word32
    iLength (Maybe (Interval' ()) -> Word32) -> Maybe (Interval' ()) -> Word32
    forall a b. (a -> b) -> a -> b
    $ Range -> Maybe (Interval' ())
    forall a. Range' a -> Maybe (Interval' ())
    rangeToInterval (Range -> Maybe (Interval' ())) -> Range -> Maybe (Interval' ())
    forall a b. (a -> b) -> a -> b
    $ TCErr -> Range
    forall a. HasRange a => a -> Range
    getRange TCErr
    err
                          infinity :: Word32
    infinity = Word32
    1000000000
              [TCErr]
    -> TCMT IO (Maybe ([Candidate], Blocker))
    -> TCMT IO (Maybe ([Candidate], Blocker))
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange (Int -> [TCErr] -> [TCErr]
    forall a. Int -> [a] -> [a]
    take Int
    1 ([TCErr] -> [TCErr]) -> [TCErr] -> [TCErr]
    forall a b. (a -> b) -> a -> b
    $ ((Candidate, TCErr) -> TCErr) -> [(Candidate, TCErr)] -> [TCErr]
    forall a b. (a -> b) -> [a] -> [b]
    map (Candidate, TCErr) -> TCErr
    forall a b. (a, b) -> b
    snd [(Candidate, TCErr)]
    sortedErrs) (TCMT IO (Maybe ([Candidate], Blocker))
     -> TCMT IO (Maybe ([Candidate], Blocker)))
    -> TCMT IO (Maybe ([Candidate], Blocker))
    -> TCMT IO (Maybe ([Candidate], Blocker))
    forall a b. (a -> b) -> a -> b
    $
                TypeError -> TCMT IO (Maybe ([Candidate], Blocker))
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO (Maybe ([Candidate], Blocker)))
    -> TypeError -> TCMT IO (Maybe ([Candidate], Blocker))
    forall a b. (a -> b) -> a -> b
    $ Type -> [(Term, TCErr)] -> TypeError
    InstanceNoCandidate Type
    t [ (Candidate -> Term
    candidateTerm Candidate
    c, TCErr
    err) | (Candidate
    c, TCErr
    err) <- [(Candidate, TCErr)]
    sortedErrs ]

            Just ([(Candidate, TCErr)]
    errs, [(c :: Candidate
    c@(Candidate CandidateKind
    q Term
    term Type
    t' OverlapMode
    _), Term
    v)]) -> do
              [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.instance" Int
    15 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    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
    vcat
                [ TCMT IO Doc
    "instance search: attempting"
                , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ MetaId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
    prettyTCM MetaId
    m TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    ":=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    v
                ]

              [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.instance" Int
    70 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $
                TCMT IO Doc
    "candidate v = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Term
    v

              ctxElims <- (Arg Term -> Elim) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply (Args -> Elims) -> TCMT IO Args -> TCMT IO Elims
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Args
    forall (m :: * -> *). MonadTCEnv m => m Args
    getContextArgs
              equalTerm t (MetaV m ctxElims) v

              reportSDoc "tc.instance" 15 $ vcat
                [ "findInstance 5: solved by instance search using the only candidate"
                , nest 2 $ prettyTCM c <+> "=" <+> prettyTCM term
                , "of type " <+> prettyTCM t'
                , "for type" <+> prettyTCM t
                ]

              -- If we actually solved the constraints we should wake up any held
              -- instance constraints, to make sure we don't forget about them.
              wakeupInstanceConstraints
              return Nothing  -- We’re done

            Maybe ([(Candidate, TCErr)], [(Candidate, Term)])
    _ -> do
              let cs :: [Candidate]
    cs = [Candidate]
    -> (([(Candidate, TCErr)], [(Candidate, Term)]) -> [Candidate])
    -> Maybe ([(Candidate, TCErr)], [(Candidate, Term)])
    -> [Candidate]
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe [Candidate]
    cands (((Candidate, Term) -> Candidate)
    -> [(Candidate, Term)] -> [Candidate]
    forall a b. (a -> b) -> [a] -> [b]
    map (Candidate, Term) -> Candidate
    forall a b. (a, b) -> a
    fst ([(Candidate, Term)] -> [Candidate])
    -> (([(Candidate, TCErr)], [(Candidate, Term)])
        -> [(Candidate, Term)])
    -> ([(Candidate, TCErr)], [(Candidate, Term)])
    -> [Candidate]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([(Candidate, TCErr)], [(Candidate, Term)]) -> [(Candidate, Term)]
    forall a b. (a, b) -> b
    snd) Maybe ([(Candidate, TCErr)], [(Candidate, Term)])
    mcands -- keep the current candidates if Nothing
              [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.instance" Int
    15 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
                [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char]
    "findInstance 5: refined candidates: ") TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
                [Term] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => [Term] -> m Doc
    prettyTCM ((Candidate -> Term) -> [Candidate] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    List.map Candidate -> Term
    candidateTerm [Candidate]
    cs)
              ProfileOption -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
    whenProfile ProfileOption
    Profile.Instances (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TCMT IO ()
    forall (m :: * -> *). MonadStatistics m => [Char] -> m ()
    tick [Char]
    "findInstance: multiple candidates"
              Maybe ([Candidate], Blocker)
    -> TCMT IO (Maybe ([Candidate], Blocker))
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (([Candidate], Blocker) -> Maybe ([Candidate], Blocker)
    forall a. a -> Maybe a
    Just ([Candidate]
    cs, Blocker
    neverUnblock))

    insidePi :: Type -> (Type -> TCM a) -> TCM a
    insidePi :: forall a. Type -> (Type -> TCM a) -> TCM a
    insidePi Type
    t Type -> TCM a
    ret = Term -> TCMT IO Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t) TCMT IO Term -> (Term -> TCM a) -> TCM a
    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
        Pi Dom Type
    a Abs Type
    b     -> ([Char], Dom Type) -> TCM a -> TCM a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    ([Char], Dom Type) -> m a -> m a
    addContext (Abs Type -> [Char]
    forall a. Abs a -> [Char]
    absName Abs Type
    b, Dom Type
    a) (TCM a -> TCM a) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $ Type -> (Type -> TCM a) -> TCM a
    forall a. Type -> (Type -> TCM a) -> TCM a
    insidePi (Abs Type -> Type
    forall a. Subst a => Abs a -> a
    absBody Abs Type
    b) Type -> TCM a
    ret
        Def{}      -> Type -> TCM a
    ret Type
    t
        Var{}      -> Type -> TCM a
    ret Type
    t
        Sort{}     -> TCM a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Con{}      -> TCM a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Lam{}      -> TCM a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Lit{}      -> TCM a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Level{}    -> TCM a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        MetaV{}    -> TCM a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        DontCare{} -> TCM a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Dummy [Char]
    s Elims
    _  -> [Char] -> TCM a
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    [Char] -> m a
    __IMPOSSIBLE_VERBOSE__ [Char]
    s

    -- | Apply the computation to every argument in turn by resetting the state every
    --   time. Return the list of the arguments giving the result True.
    --
    --   If the resulting list contains exactly one element, then the state is the
    --   same as the one obtained after running the corresponding computation. In
    --   all the other cases, the state is reset.
    --
    --   Also returns the candidates that pass type checking but fails constraints,
    --   so that the error messages can be reported if there are no successful
    --   candidates.
    filterResettingState
      :: MetaId
      -> [Candidate]
      -> (Candidate -> TCM YesNo)
      -> TCM ([(Candidate, TCErr)], [(Candidate, Term)])
    filterResettingState :: MetaId
    -> [Candidate]
    -> (Candidate -> TCM YesNo)
    -> TCM ([(Candidate, TCErr)], [(Candidate, Term)])
    filterResettingState MetaId
    m [Candidate]
    cands Candidate -> TCM YesNo
    f = do
      ctxArgs  <- TCMT IO Args
    forall (m :: * -> *). MonadTCEnv m => m Args
    getContextArgs
      let ctxElims = (Arg Term -> Elim) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply Args
    ctxArgs
      result <- mapM (\Candidate
    c -> do bs <- TCM YesNo -> TCM (YesNo, TCState)
    forall a. TCM a -> TCM (a, TCState)
    localTCStateSaving (Candidate -> TCM YesNo
    f Candidate
    c); return (c, bs)) cands

      -- Check that there aren't any hard failures
      case [ err | (_, (HellNo err, _)) <- result ] of
        TCErr
    err : [TCErr]
    _ -> TCErr -> TCMT IO ()
    forall a. TCErr -> TCMT IO a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError TCErr
    err
        []      -> () -> TCMT IO ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

      -- c : Candidate
      -- r : YesNo
      -- a : Type         (fully instantiated)
      -- s : TCState
      let
        result' = [ (Candidate
    c, Term
    v, TCState
    s) | (Candidate
    c, (YesNo
    r, TCState
    s)) <- [(Candidate, (YesNo, TCState))]
    result, Term
    v <- Maybe Term -> [Term]
    forall a. Maybe a -> [a]
    maybeToList (YesNo -> Maybe Term
    fromYes YesNo
    r) ]
        overlap = (((Candidate, (YesNo, TCState)) -> Bool)
     -> [(Candidate, (YesNo, TCState))] -> Bool)
    -> [(Candidate, (YesNo, TCState))]
    -> ((Candidate, (YesNo, TCState)) -> Bool)
    -> Bool
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip ((Candidate, (YesNo, TCState)) -> Bool)
    -> [(Candidate, (YesNo, TCState))] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all [(Candidate, (YesNo, TCState))]
    result \(Candidate
    c, (YesNo
    r, TCState
    s)) -> case YesNo
    r of
          Yes Term
    _ Bool
    False -> Bool
    False
          YesNo
    _ -> Bool
    True
      result'' <- dropSameCandidates m overlap result'
      case result'' of
        [(Candidate
    c, Term
    v, TCState
    s)] -> ([], [(Candidate
    c, Term
    v)]) ([(Candidate, TCErr)], [(Candidate, Term)])
    -> TCMT IO () -> TCM ([(Candidate, TCErr)], [(Candidate, Term)])
    forall a b. a -> TCMT IO b -> TCMT IO a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ TCState -> TCMT IO ()
    forall (m :: * -> *). MonadTCState m => TCState -> m ()
    putTC TCState
    s
        [(Candidate, Term, TCState)]
    _           -> do
          let bad :: [(Candidate, TCErr)]
    bad  = [ (Candidate
    c, TCErr
    err) | (Candidate
    c, (NoBecause TCErr
    err, TCState
    _)) <- [(Candidate, (YesNo, TCState))]
    result ]
              good :: [(Candidate, Term)]
    good = [ (Candidate
    c, Term
    v) | (Candidate
    c, Term
    v, TCState
    _) <- [(Candidate, Term, TCState)]
    result'' ]
          ([(Candidate, TCErr)], [(Candidate, Term)])
    -> TCM ([(Candidate, TCErr)], [(Candidate, Term)])
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(Candidate, TCErr)]
    bad, [(Candidate, Term)]
    good)

    -- | The state used to reduce a list of candidates according to the
    -- overlap rules.
    data OverlapState item = OverlapState
      { forall item. OverlapState item -> [item]
    survivingCands :: [item]
        -- ^ The reduced list.

      , forall item. OverlapState item -> [Candidate]
    guardingCands  :: [Candidate]
        -- ^ Overlapping candidates that have been discarded, which are kept
        -- around because they might still discard some overlappable
        -- candidates.
      }

    -- | Apply the instance overlap rules to reduce the list of candidates.
    resolveInstanceOverlap
      :: forall item.
         Bool
      -> Relevance
      -> (item -> Candidate)
      -> [item]
      -> TCM [item]
    resolveInstanceOverlap :: forall item.
    Bool -> Relevance -> (item -> Candidate) -> [item] -> TCM [item]
    resolveInstanceOverlap Bool
    overlapOk Relevance
    rel item -> Candidate
    itemC [item]
    cands = TCMT IO [item]
    wrapper where
      wrapper :: TCMT IO [item]
    wrapper
        -- If all the candidates are incoherent: choose the leftmost candidate.
        | (item -> Bool) -> [item] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (OverlapMode -> Bool
    forall a. HasOverlapMode a => a -> Bool
    isIncoherent (OverlapMode -> Bool) -> (item -> OverlapMode) -> item -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Candidate -> OverlapMode
    candidateOverlap (Candidate -> OverlapMode)
    -> (item -> Candidate) -> item -> OverlapMode
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . item -> Candidate
    itemC) [item]
    cands
        , (item
    c:[item]
    _) <- [item]
    cands = [item] -> TCMT IO [item]
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [item
    c]

        -- If all the candidates are record field overlap: choose the leftmost candidate.
        | (item -> Bool) -> [item] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all ((OverlapMode -> OverlapMode -> Bool
    forall a. Eq a => a -> a -> Bool
    == OverlapMode
    FieldOverlap) (OverlapMode -> Bool) -> (item -> OverlapMode) -> item -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Candidate -> OverlapMode
    candidateOverlap (Candidate -> OverlapMode)
    -> (item -> Candidate) -> item -> OverlapMode
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . item -> Candidate
    itemC) [item]
    cands
        , (item
    c:[item]
    _) <- [item]
    cands = [item] -> TCMT IO [item]
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [item
    c]

        -- If none of the candidates have a special overlap mode: there's no
        -- reason to do any work.
        | (item -> Bool) -> [item] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all ((OverlapMode
    DefaultOverlap OverlapMode -> OverlapMode -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (OverlapMode -> Bool) -> (item -> OverlapMode) -> item -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Candidate -> OverlapMode
    candidateOverlap (Candidate -> OverlapMode)
    -> (item -> Candidate) -> item -> OverlapMode
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . item -> Candidate
    itemC) [item]
    cands = [item] -> TCMT IO [item]
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [item]
    cands

        | Bool -> Bool
    not Bool
    overlapOk = [item] -> TCMT IO [item]
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [item]
    cands

        -- If some of the candidates are overlappable/overlapping, then we
        -- should do the work.
        | Bool
    otherwise = Account (BenchPhase (TCMT IO)) -> TCMT IO [item] -> TCMT IO [item]
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [BenchPhase (TCMT IO)
    Phase
    Bench.Typing, BenchPhase (TCMT IO)
    Phase
    Bench.InstanceSearch, BenchPhase (TCMT IO)
    Phase
    Bench.CheckOverlap] do
          [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.instance.overlap" Int
    30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "overlapping instances:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ((item -> TCMT IO Doc) -> [item] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Candidate -> TCMT IO Doc
    forall (m :: * -> *). MonadPretty m => Candidate -> m Doc
    debugCandidate (Candidate -> TCMT IO Doc)
    -> (item -> Candidate) -> item -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . item -> Candidate
    itemC) [item]
    cands)

          [item] -> [item]
    sinkIncoherent ([item] -> [item])
    -> (OverlapState item -> [item]) -> OverlapState item -> [item]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . OverlapState item -> [item]
    forall item. OverlapState item -> [item]
    survivingCands (OverlapState item -> [item])
    -> TCMT IO (OverlapState item) -> TCMT IO [item]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (item -> OverlapState item -> TCMT IO (OverlapState item))
    -> OverlapState item -> [item] -> TCMT IO (OverlapState item)
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> b -> m b) -> b -> t a -> m b
    foldrM item -> OverlapState item -> TCMT IO (OverlapState item)
    insert ([item] -> [Candidate] -> OverlapState item
    forall item. [item] -> [Candidate] -> OverlapState item
    OverlapState [] []) [item]
    cands

      isGlobal :: Candidate -> Bool
    isGlobal Candidate{candidateKind :: Candidate -> CandidateKind
    candidateKind = GlobalCandidate QName
    _} = Bool
    True
      isGlobal Candidate
    _ = Bool
    False

      -- At the end of the process, we might still have some incoherent and
      -- non-incoherent candidates, since the user might have an instance
      -- which fixes some arguments in a way that prevents it from serving
      -- as a specialisation (see test/Succeed/Overlap1).
      --
      -- See test/Succeed/OverlapDupe for a case where this is necessary.
      sinkIncoherent :: [item] -> [item]
      sinkIncoherent :: [item] -> [item]
    sinkIncoherent [item]
    cands = case (item -> Bool) -> [item] -> ([item], [item])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    List.partition (Candidate -> Bool
    forall a. HasOverlapMode a => a -> Bool
    isIncoherent (Candidate -> Bool) -> (item -> Candidate) -> item -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . item -> Candidate
    itemC) [item]
    cands of
        ([item]
    as, [item
    c]) | (item -> Bool) -> [item] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (Candidate -> Bool
    isGlobal (Candidate -> Bool) -> (item -> Candidate) -> item -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . item -> Candidate
    itemC) [item]
    as -> item -> [item]
    forall a. a -> [a]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure item
    c
        ([item]
    as, [item]
    cs)  | (item -> Bool) -> [item] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (Candidate -> Bool
    isGlobal (Candidate -> Bool) -> (item -> Candidate) -> item -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . item -> Candidate
    itemC) [item]
    as -> [item]
    cs [item] -> [item] -> [item]
    forall a. [a] -> [a] -> [a]
    ++ [item]
    as
        ([item], [item])
    _                                     -> [item]
    cands

      -- Insert a new item into the overlap state.
      insertNew
        :: OverlapState item  -- The state to insert into
        -> item               -- The item to insert
        -> [item]             -- Old items which we might overlap/be overlapped by
        -> TCM (OverlapState item)
      insertNew :: OverlapState item -> item -> [item] -> TCMT IO (OverlapState item)
    insertNew OverlapState item
    oldState item
    new [] = OverlapState item -> TCMT IO (OverlapState item)
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure OverlapState item
    oldState{ survivingCands = [new] }
      insertNew OverlapState item
    oldState item
    newItem oldItems :: [item]
    oldItems@(item
    oldItem:[item]
    olds) = do
        let
          new :: Candidate
    new = item -> Candidate
    itemC item
    newItem
          old :: Candidate
    old = item -> Candidate
    itemC item
    oldItem

        [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.instance.overlap" Int
    50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    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
    vcat
          [ TCMT IO Doc
    "comparing new candidate"
          , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (Candidate -> TCMT IO Doc
    forall (m :: * -> *). MonadPretty m => Candidate -> m Doc
    debugCandidate Candidate
    new)
          , TCMT IO Doc
    "versus old candidate"
          , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (Candidate -> TCMT IO Doc
    forall (m :: * -> *). MonadPretty m => Candidate -> m Doc
    debugCandidate Candidate
    old)
          ]

        let
          -- If the new candidate overrides the old, drop it. But if the old
          -- candidate was overlapping (and the new one isn't), we keep it
          -- as a guard, since it might knock out future candidates.
          newold :: TCMT IO (OverlapState item)
    newold = OverlapState item -> item -> [item] -> TCMT IO (OverlapState item)
    insertNew OverlapState item
    oldState item
    newItem [item]
    olds TCMT IO (OverlapState item)
    -> (OverlapState item -> OverlapState item)
    -> TCMT IO (OverlapState item)
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \case
            OverlapState [item]
    items [Candidate]
    guards ->
              if Bool -> Bool
    not (Candidate -> Bool
    forall a. HasOverlapMode a => a -> Bool
    isOverlapping Candidate
    new) Bool -> Bool -> Bool
    && Candidate -> Bool
    forall a. HasOverlapMode a => a -> Bool
    isOverlapping Candidate
    old
                then [item] -> [Candidate] -> OverlapState item
    forall item. [item] -> [Candidate] -> OverlapState item
    OverlapState [item]
    items [Candidate]
    guards
                else [item] -> [Candidate] -> OverlapState item
    forall item. [item] -> [Candidate] -> OverlapState item
    OverlapState [item]
    items (Candidate
    oldCandidate -> [Candidate] -> [Candidate]
    forall a. a -> [a] -> [a]
    :[Candidate]
    guards)

          -- If the old candidate overrides the new, then stop inserting.
          -- But if the new candidate is overlapping, it can be added as a
          -- guard.
          oldnew :: TCMT IO (OverlapState item)
    oldnew = do
            if Candidate -> Bool
    forall a. HasOverlapMode a => a -> Bool
    isOverlapping Candidate
    old Bool -> Bool -> Bool
    || Bool -> Bool
    not (Candidate -> Bool
    forall a. HasOverlapMode a => a -> Bool
    isOverlapping Candidate
    new) then OverlapState item -> TCMT IO (OverlapState item)
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure OverlapState item
    oldState{ survivingCands = oldItems } else do
              let OverlapState{ guardingCands :: forall item. OverlapState item -> [Candidate]
    guardingCands = [Candidate]
    guards } = OverlapState item
    oldState
              [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.instance.overlap" Int
    40 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    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
    vcat
                [ TCMT IO Doc
    "will become guard:"
                , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (Candidate -> TCMT IO Doc
    forall (m :: * -> *). MonadPretty m => Candidate -> m Doc
    debugCandidate Candidate
    new)
                , TCMT IO Doc
    "old items:"
                , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ((item -> TCMT IO Doc) -> [item] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Candidate -> TCMT IO Doc
    forall (m :: * -> *). MonadPretty m => Candidate -> m Doc
    debugCandidate (Candidate -> TCMT IO Doc)
    -> (item -> Candidate) -> item -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . item -> Candidate
    itemC) [item]
    oldItems))
                ]

              -- But we can't /just/ add it to the list of guards: the new
              -- item might conflict with some of the other old candidates.
              -- We must remove those.
              alive <- (item -> TCM Bool) -> [item] -> TCMT IO [item]
    forall (m :: * -> *) a.
    Applicative m =>
    (a -> m Bool) -> [a] -> m [a]
    filterM ((Bool -> Bool) -> TCM Bool -> TCM 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 (TCM Bool -> TCM Bool) -> (item -> TCM Bool) -> item -> TCM Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Candidate -> Candidate -> TCM Bool
    doesCandidateOverlap Candidate
    new (Candidate -> TCM Bool) -> (item -> Candidate) -> item -> TCM Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . item -> Candidate
    itemC) [item]
    oldItems
              pure $ OverlapState alive (new:guards)

          -- If neither overrides the other, keep both!
          neither :: TCMT IO (OverlapState item)
    neither = OverlapState item -> item -> [item] -> TCMT IO (OverlapState item)
    insertNew OverlapState item
    oldState item
    newItem [item]
    olds TCMT IO (OverlapState item)
    -> (OverlapState item -> OverlapState item)
    -> TCMT IO (OverlapState item)
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \case
            OverlapState [item]
    items [Candidate]
    guards -> [item] -> [Candidate] -> OverlapState item
    forall item. [item] -> [Candidate] -> OverlapState item
    OverlapState (item
    oldItemitem -> [item] -> [item]
    forall a. a -> [a] -> [a]
    :[item]
    items) [Candidate]
    guards

        TCM Bool
    -> TCMT IO (OverlapState item)
    -> TCMT IO (OverlapState item)
    -> TCMT IO (OverlapState item)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (Candidate
    new Candidate -> Candidate -> TCM Bool
    `doesCandidateOverlap` Candidate
    old)
          {- then -} TCMT IO (OverlapState item)
    newold
          {- else -} (TCM Bool
    -> TCMT IO (OverlapState item)
    -> TCMT IO (OverlapState item)
    -> TCMT IO (OverlapState item)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (Candidate
    old Candidate -> Candidate -> TCM Bool
    `doesCandidateOverlap` Candidate
    new)
            {- then -} TCMT IO (OverlapState item)
    oldnew
            {- else -} TCMT IO (OverlapState item)
    neither)

      -- Insert a new instance into the given overlap set.
      insert :: item -> OverlapState item -> TCM (OverlapState item)
      insert :: item -> OverlapState item -> TCMT IO (OverlapState item)
    insert item
    newItem oldState :: OverlapState item
    oldState@(OverlapState [item]
    oldItems [Candidate]
    guards) = do
        let new :: Candidate
    new = item -> Candidate
    itemC item
    newItem
        -- If the new candidate is overridden by any of the guards, we can
        -- ditch it immediately.
        guarded <- (Candidate -> TCM Bool) -> [Candidate] -> TCM Bool
    forall (f :: * -> *) (m :: * -> *) a.
    (Foldable f, Monad m) =>
    (a -> m Bool) -> f a -> m Bool
    anyM (Candidate -> Candidate -> TCM Bool
    `doesCandidateOverlap` Candidate
    new) [Candidate]
    guards

        reportSDoc "tc.instance.overlap" 40 $ vcat
          [ "inserting new candidate:"
          , nest 2 (debugCandidate new)
          , "against old candidates"
          , nest 2 (vcat (map (debugCandidate . itemC) oldItems))
          , "and guarding candidates"
          , nest 2 (vcat (map debugCandidate guards))
          , "is guarded?" <+> prettyTCM guarded
          ]

        if guarded then pure oldState else insertNew oldState newItem oldItems

    -- Drop all candidates which are judgmentally equal to the first one.
    -- This is sufficient to reduce the list to a singleton should all be equal.
    dropSameCandidates :: MetaId -> Bool -> [(Candidate, Term, TCState)] -> TCM [(Candidate, Term, TCState)]
    dropSameCandidates :: MetaId
    -> Bool
    -> [(Candidate, Term, TCState)]
    -> TCM [(Candidate, Term, TCState)]
    dropSameCandidates MetaId
    m Bool
    overlapOk [(Candidate, Term, TCState)]
    cands0 = [Char]
    -> Int
    -> [Char]
    -> TCM [(Candidate, Term, TCState)]
    -> TCM [(Candidate, Term, TCState)]
    forall a. [Char] -> Int -> [Char] -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a.
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m a -> m a
    verboseBracket [Char]
    "tc.instance" Int
    30 [Char]
    "dropSameCandidates" (TCM [(Candidate, Term, TCState)]
     -> TCM [(Candidate, Term, TCState)])
    -> TCM [(Candidate, Term, TCState)]
    -> TCM [(Candidate, Term, TCState)]
    forall a b. (a -> b) -> a -> b
    $ do
      !nextMeta    <- TCMT IO MetaId
    forall (m :: * -> *). ReadTCState m => m MetaId
    nextLocalMeta
      isRemoteMeta <- isRemoteMeta

      -- Does "it" contain any fresh meta-variables?
      let freshMetas = Any -> Bool
    getAny (Any -> Bool) -> (Term -> Any) -> Term -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (MetaId -> Any) -> Term -> Any
    forall m. Monoid m => (MetaId -> m) -> Term -> m
    forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas (\MetaId
    m -> Bool -> Any
    Any (Bool -> Bool
    not (MetaId -> Bool
    isRemoteMeta MetaId
    m Bool -> Bool -> Bool
    || MetaId
    m MetaId -> MetaId -> Bool
    forall a. Ord a => a -> a -> Bool
    < MetaId
    nextMeta)))

      rel <- getRelevance <$> lookupMetaModality m

      -- Take overlappable candidates into account
      cands <- resolveInstanceOverlap overlapOk rel fst3 cands0
      reportSDoc "tc.instance.overlap" 30 $ "instances after resolving overlap:" $$ vcat (map (debugCandidate . fst3) cands)

      reportSDoc "tc.instance" 50 $ vcat
        [ "valid candidates:"
        , nest 2 $ vcat [ if freshMetas v then "(redacted)" else
                          sep [ prettyTCM v ]
                        | (_, v, _) <- cands ] ]

      case cands of
        [] -> [(Candidate, Term, TCState)] -> TCM [(Candidate, Term, TCState)]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [(Candidate, Term, TCState)]
    cands
        (Candidate, Term, TCState)
    cvd : [(Candidate, Term, TCState)]
    _ | Relevance -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant Relevance
    rel -> do
          [Char] -> Int -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.instance" Int
    30 [Char]
    "dropSameCandidates: Meta is irrelevant so any candidate will do."
          [(Candidate, Term, TCState)] -> TCM [(Candidate, Term, TCState)]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [(Candidate, Term, TCState)
    cvd]

        -- If there's nothing, try not to reduce the candidate.
        [(Candidate, Term, TCState)
    cvd] -> [(Candidate, Term, TCState)] -> TCM [(Candidate, Term, TCState)]
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [(Candidate, Term, TCState)
    cvd]

        cvd :: (Candidate, Term, TCState)
    cvd@(Candidate
    _, Term
    v, TCState
    _) : [(Candidate, Term, TCState)]
    vas -> do
          let
            equal :: (Candidate, Term, a) -> TCM Bool
            equal :: forall a. (Candidate, Term, a) -> TCM Bool
    equal (Candidate
    c, Term
    v', a
    _)
                | Candidate -> Bool
    forall a. HasOverlapMode a => a -> Bool
    isIncoherent Candidate
    c = Bool -> TCM Bool
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True   -- See 'sinkIncoherent'
                | Term -> Bool
    freshMetas Term
    v'  = Bool -> TCM Bool
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False  -- If there are fresh metas we can't compare
                | Bool
    otherwise      =
              [Char] -> Int -> [Char] -> TCM Bool -> TCM Bool
    forall a. [Char] -> Int -> [Char] -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a.
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m a -> m a
    verboseBracket [Char]
    "tc.instance" Int
    30 [Char]
    "dropSameCandidates: " (TCM Bool -> TCM Bool) -> TCM Bool -> TCM Bool
    forall a b. (a -> b) -> a -> b
    $ do
              [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.instance" Int
    30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    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
    sep [ Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "==", Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    v' ]
              a <- (Type -> Args -> TCMT IO Type) -> (Type, Args) -> TCMT IO Type
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry 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, Args) -> TCMT IO Type)
    -> TCMT IO (Type, Args) -> TCMT IO Type
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ((,) (Type -> Args -> (Type, Args))
    -> TCMT IO Type -> TCMT IO (Args -> (Type, Args))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> TCMT IO Type
    forall (m :: * -> *). ReadTCState m => MetaId -> m Type
    getMetaType MetaId
    m TCMT IO (Args -> (Type, Args))
    -> TCMT IO Args -> TCMT IO (Type, Args)
    forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> TCMT IO Args
    forall (m :: * -> *). MonadTCEnv m => m Args
    getContextArgs)
              pureEqualTermB a v v' <&> \case
                Left{}  -> Bool
    False
                Right Bool
    b -> Bool
    b

          -- If we do actually have to remove overlap then we have to reduce
          -- the candidate to eliminate any "phantom" dependencies on fresh
          -- metas.
          v <- Term -> TCMT IO Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Term
    v
          if
            | freshMetas v -> do
              reportSLn "tc.instance" 30 "dropSameCandidates: Solution of instance meta has fresh metas so we don't filter equal candidates yet"
              return (cvd : vas)
            | otherwise -> (cvd :) <$> dropWhileM equal vas

    data YesNo = Yes Term Bool | No | NoBecause TCErr | HellNo TCErr
      deriving (Int -> YesNo -> [Char] -> [Char]
    [YesNo] -> [Char] -> [Char]
    YesNo -> [Char]
    (Int -> YesNo -> [Char] -> [Char])
    -> (YesNo -> [Char]) -> ([YesNo] -> [Char] -> [Char]) -> Show YesNo
    forall a.
    (Int -> a -> [Char] -> [Char])
    -> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
    $cshowsPrec :: Int -> YesNo -> [Char] -> [Char]
    showsPrec :: Int -> YesNo -> [Char] -> [Char]
    $cshow :: YesNo -> [Char]
    show :: YesNo -> [Char]
    $cshowList :: [YesNo] -> [Char] -> [Char]
    showList :: [YesNo] -> [Char] -> [Char]
    Show)

    fromYes :: YesNo -> Maybe Term
    fromYes :: YesNo -> Maybe Term
    fromYes (Yes Term
    t Bool
    _) = Term -> Maybe Term
    forall a. a -> Maybe a
    Just Term
    t
    fromYes YesNo
    _         = Maybe Term
    forall a. Maybe a
    Nothing

    debugCandidate' :: MonadPretty m => Bool -> Bool -> Candidate -> m Doc
    debugCandidate' :: forall (m :: * -> *).
    MonadPretty m =>
    Bool -> Bool -> Candidate -> m Doc
    debugCandidate' Bool
    raw Bool
    term c :: Candidate
    c@(Candidate CandidateKind
    q Term
    v Type
    t OverlapMode
    overlap) =
      let
        cand :: m Doc
    cand
          | Bool
    term      = Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    v
          | Bool
    otherwise = Candidate -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Candidate -> m Doc
    prettyTCM Candidate
    c

        ty :: m Doc
    ty
          | Bool
    raw       = Int -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (Type -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Type
    t)
          | Bool
    otherwise = Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t

        head :: m Doc
    head = [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep [ m Doc
    "-", OverlapMode -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty OverlapMode
    overlap, m Doc
    cand, m Doc
    ":" ]
      in if | Bool
    raw       -> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ m Doc
    head, m Doc
    ty ]
            | Bool
    otherwise -> m Doc
    head m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    ty

    debugCandidate :: MonadPretty m => Candidate -> m Doc
    debugCandidate :: forall (m :: * -> *). MonadPretty m => Candidate -> m Doc
    debugCandidate = Bool -> Bool -> Candidate -> m Doc
    forall (m :: * -> *).
    MonadPretty m =>
    Bool -> Bool -> Candidate -> m Doc
    debugCandidate' Bool
    False Bool
    False

    debugCandidateRaw :: MonadPretty m => Candidate -> m Doc
    debugCandidateRaw :: forall (m :: * -> *). MonadPretty m => Candidate -> m Doc
    debugCandidateRaw = Bool -> Bool -> Candidate -> m Doc
    forall (m :: * -> *).
    MonadPretty m =>
    Bool -> Bool -> Candidate -> m Doc
    debugCandidate' Bool
    True Bool
    False

    debugCandidateTerm :: MonadPretty m => Candidate -> m Doc
    debugCandidateTerm :: forall (m :: * -> *). MonadPretty m => Candidate -> m Doc
    debugCandidateTerm = Bool -> Bool -> Candidate -> m Doc
    forall (m :: * -> *).
    MonadPretty m =>
    Bool -> Bool -> Candidate -> m Doc
    debugCandidate' Bool
    False Bool
    True

    -- | Given a meta @m@ of type @t@ and a list of candidates @cands@,
    -- @checkCandidates m t cands@ returns a refined list of valid candidates and
    -- candidates that failed some constraints.
    checkCandidates :: MetaId -> Type -> [Candidate] -> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
    checkCandidates :: MetaId
    -> Type
    -> [Candidate]
    -> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
    checkCandidates MetaId
    m Type
    t [Candidate]
    cands =
      [Char]
    -> Int
    -> [Char]
    -> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
    -> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
    forall a. [Char] -> Int -> [Char] -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a.
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m a -> m a
    verboseBracket [Char]
    "tc.instance.candidates" Int
    20 ([Char]
    "checkCandidates " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ MetaId -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow MetaId
    m) (TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
     -> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)])))
    -> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
    -> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
    forall a b. (a -> b) -> a -> b
    $
      TCM Bool
    -> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
    -> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
    -> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM ([Candidate] -> TCM Bool
    anyMetaTypes [Candidate]
    cands) (Maybe ([(Candidate, TCErr)], [(Candidate, Term)])
    -> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe ([(Candidate, TCErr)], [(Candidate, Term)])
    forall a. Maybe a
    Nothing) (TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
     -> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)])))
    -> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
    -> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
    forall a b. (a -> b) -> a -> b
    $ ([(Candidate, TCErr)], [(Candidate, Term)])
    -> Maybe ([(Candidate, TCErr)], [(Candidate, Term)])
    forall a. a -> Maybe a
    Just (([(Candidate, TCErr)], [(Candidate, Term)])
     -> Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
    -> TCM ([(Candidate, TCErr)], [(Candidate, Term)])
    -> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
        [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.instance.candidates" Int
    20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "target:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t
        [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.instance.candidates" Int
    20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    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
    vcat
          [ TCMT IO Doc
    "candidates", [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ((Candidate -> TCMT IO Doc) -> [Candidate] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Candidate -> TCMT IO Doc
    forall (m :: * -> *). MonadPretty m => Candidate -> m Doc
    debugCandidate [Candidate]
    cands) ]

        t <- Type -> TCMT IO Type
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull Type
    t
        cands'@(_, okay) <- filterResettingState m cands (checkCandidateForMeta m t)

        reportSDoc "tc.instance.candidates" 20 $ nest 2 $ vcat
          [ "valid candidates", vcat (map (debugCandidate . fst) okay) ]
        reportSDoc "tc.instance.candidates" 60 $ nest 2 $ vcat
          [ "valid candidates", vcat (map (debugCandidateTerm . fst) okay) ]

        return cands'
      where
        anyMetaTypes :: [Candidate] -> TCM Bool
        anyMetaTypes :: [Candidate] -> TCM Bool
    anyMetaTypes [] = Bool -> TCM Bool
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
        anyMetaTypes (Candidate CandidateKind
    _ Term
    _ Type
    a OverlapMode
    _ : [Candidate]
    cands) = do
          a <- Type -> TCMT IO Type
    forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
    instantiate Type
    a
          case unEl a of
            MetaV{} -> Bool -> TCM Bool
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
            Term
    _       -> [Candidate] -> TCM Bool
    anyMetaTypes [Candidate]
    cands

        checkDepth :: Term -> Type -> TCM YesNo -> TCM YesNo
        checkDepth :: Term -> Type -> TCM YesNo -> TCM YesNo
    checkDepth Term
    c Type
    a TCM YesNo
    k = Lens' TCEnv Int -> (Int -> Int) -> TCM YesNo -> TCM YesNo
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' TCEnv a -> (a -> a) -> m b -> m b
    locallyTC (Int -> f Int) -> TCEnv -> f TCEnv
    Lens' TCEnv Int
    eInstanceDepth Int -> Int
    forall a. Enum a => a -> a
    succ (TCM YesNo -> TCM YesNo) -> TCM YesNo -> TCM YesNo
    forall a b. (a -> b) -> a -> b
    $ do
          d        <- Lens' TCEnv Int -> TCMT IO Int
    forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
    viewTC (Int -> f Int) -> TCEnv -> f TCEnv
    Lens' TCEnv Int
    eInstanceDepth
          maxDepth <- maxInstanceSearchDepth
          when (d > maxDepth) $ typeError $ InstanceSearchDepthExhausted c a maxDepth
          k

        checkCandidateForMeta :: MetaId -> Type -> Candidate -> TCM YesNo
        checkCandidateForMeta :: MetaId -> Type -> Candidate -> TCM YesNo
    checkCandidateForMeta MetaId
    m Type
    t (Candidate CandidateKind
    q Term
    term Type
    t' OverlapMode
    _) = Term -> Type -> TCM YesNo -> TCM YesNo
    checkDepth Term
    term Type
    t' (TCM YesNo -> TCM YesNo) -> TCM YesNo -> TCM YesNo
    forall a b. (a -> b) -> a -> b
    $ do
          Account (BenchPhase (TCMT IO)) -> TCM YesNo -> TCM YesNo
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [BenchPhase (TCMT IO)
    Phase
    Bench.Typing, BenchPhase (TCMT IO)
    Phase
    Bench.InstanceSearch, BenchPhase (TCMT IO)
    Phase
    Bench.FilterCandidates] (TCM YesNo -> TCM YesNo) -> TCM YesNo -> TCM YesNo
    forall a b. (a -> b) -> a -> b
    $ do
          ProfileOption -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
    whenProfile ProfileOption
    Profile.Instances (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TCMT IO ()
    forall (m :: * -> *). MonadStatistics m => [Char] -> m ()
    tick [Char]
    "checkCandidateForMeta"

          -- Andreas, 2015-02-07: New metas should be created with range of the
          -- current instance meta, thus, we set the range.
          mv <- MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    m
          setCurrentRange mv $ runCandidateCheck $
            verboseBracket "tc.instance" 20 ("checkCandidateForMeta " ++ prettyShow m) $ do
              reportSDoc "tc.instance" 20 $ vcat
                [ "checkCandidateForMeta"
                , "  t    =" <+> prettyTCM t
                , "  t'   =" <+> prettyTCM t'
                , "  term =" <+> prettyTCM term
                ]
              reportSDoc "tc.instance" 70 $ vcat
                [ "  t    =" <+> pretty t
                , "  t'   =" <+> pretty t'
                , "  term =" <+> pretty term
                ]
              debugConstraints

              -- Apply hidden and instance arguments (in case of
              -- --overlapping-instances, this performs recursive
              -- inst. search!).
              (args, t'') <- implicitArgs (-1) (\Hiding
    h -> Hiding -> Bool
    forall a. LensHiding a => a -> Bool
    notVisible Hiding
    h) t'

              reportSDoc "tc.instance" 20 $
                "instance search: checking" <+> prettyTCM t'' <+> "<=" <+> prettyTCM t
              reportSDoc "tc.instance" 70 $ vcat
                [ "instance search: checking (raw)"
                , nest 4 $ pretty t''
                , nest 2 $ "<="
                , nest 4 $ pretty t
                ]

              -- Check whether this candidate is OK, and whether it is okay
              -- for the overlap check. For the candidate to be acceptable,
              -- its type must be a subtype of the goal type.
              (cons, overlapOk) <- ifNoConstraints_ (leqType t'' t) (pure ([], True)) \ProblemId
    pid -> do
                -- To know if this candidate is safe for overlap, we have to
                -- check that it does not constrain the type of the instance
                -- goal. We can do this by running it in a new problem and
                -- checking whether the computation produced any constraints
                -- that are blocked by the instance goal.
                cons <- ProblemId -> TCMT IO [ProblemConstraint]
    forall (m :: * -> *).
    ReadTCState m =>
    ProblemId -> m [ProblemConstraint]
    getConstraintsForProblem ProblemId
    pid
                -- Make sure to put these constraints back if we end up
                -- solving the instance goal with this candidate.
                stealConstraints pid
                let
                  blocking = (ProblemConstraint -> Set MetaId)
    -> [ProblemConstraint] -> Set MetaId
    forall m a. Monoid m => (a -> m) -> [a] -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap (Blocker -> Set MetaId
    allBlockingMetas (Blocker -> Set MetaId)
    -> (ProblemConstraint -> Blocker)
    -> ProblemConstraint
    -> Set MetaId
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ProblemConstraint -> Blocker
    constraintUnblocker) [ProblemConstraint]
    cons
                  !ok = All -> Bool
    getAll (All -> Bool) -> All -> Bool
    forall a b. (a -> b) -> a -> b
    $! ((MetaId -> All) -> Type -> All) -> Type -> (MetaId -> All) -> All
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (MetaId -> All) -> Type -> All
    forall m. Monoid m => (MetaId -> m) -> Type -> m
    forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas Type
    t (Bool -> All
    All (Bool -> All) -> (MetaId -> Bool) -> MetaId -> All
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bool -> Bool
    not (Bool -> Bool) -> (MetaId -> Bool) -> MetaId -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (MetaId -> Set MetaId -> Bool) -> Set MetaId -> MetaId -> Bool
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip MetaId -> Set MetaId -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member Set MetaId
    blocking)
                pure (cons, ok)
              debugConstraints

              flip catchError (return . NoBecause) $ do
                -- make a pass over constraints, to detect cases where
                -- some are made unsolvable by the type comparison, but
                -- don't do this for FindInstance's to prevent loops.
                solveAwakeConstraints' True
                -- We need instantiateFull here to remove 'local' metas
                v <- instantiateFull =<< (term `applyDroppingParameters` args)
                reportSDoc "tc.instance" 15 $
                  vcat [ sep [ ("instance search: found solution for" <+> prettyTCM m) <> ":"
                      , nest 2 $ prettyTCM v ]
                      , "app: " <+> (nest 2 $ prettyTCM =<< (term `applyDroppingParameters` args))
                      ]

                reportSDoc "tc.instance.overlap" 30 $
                  "candidate" <+> prettyTCM v <+> "okay for overlap?" <+> prettyTCM overlapOk
                  $$ vcat (map prettyTCM cons)

                whenProfile Profile.Instances $ tick "checkCandidateForMeta: yes"
                return $ Yes v overlapOk
          where
            runCandidateCheck :: TCM YesNo -> TCM YesNo
    runCandidateCheck = (TCM YesNo -> (TCErr -> TCM YesNo) -> TCM YesNo)
    -> (TCErr -> TCM YesNo) -> TCM YesNo -> TCM YesNo
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip TCM YesNo -> (TCErr -> TCM YesNo) -> TCM YesNo
    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 -> TCM YesNo
    handle (TCM YesNo -> TCM YesNo)
    -> (TCM YesNo -> TCM YesNo) -> TCM YesNo -> TCM YesNo
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCM YesNo -> TCM YesNo
    forall (m :: * -> *) a. ReadTCState m => m a -> m a
    nowConsideringInstance

            hardFailure :: TCErr -> Bool
            hardFailure :: TCErr -> Bool
    hardFailure (TypeError CallStack
    _ TCState
    _ Closure TypeError
    err) =
              case Closure TypeError -> TypeError
    forall a. Closure a -> a
    clValue Closure TypeError
    err of
                InstanceSearchDepthExhausted{} -> Bool
    True
                TypeError
    _                              -> Bool
    False
            hardFailure TCErr
    _ = Bool
    False

            handle :: TCErr -> TCM YesNo
            handle :: TCErr -> TCM YesNo
    handle TCErr
    err
              | TCErr -> Bool
    hardFailure TCErr
    err = do
                ProfileOption -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
    whenProfile ProfileOption
    Profile.Instances (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TCMT IO ()
    forall (m :: * -> *). MonadStatistics m => [Char] -> m ()
    tick [Char]
    "checkCandidateForMeta: no"
                YesNo -> TCM YesNo
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (YesNo -> TCM YesNo) -> YesNo -> TCM YesNo
    forall a b. (a -> b) -> a -> b
    $ TCErr -> YesNo
    HellNo TCErr
    err
              | Bool
    otherwise       = do
                [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.instance" Int
    50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "candidate failed type check:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCErr -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => TCErr -> m Doc
    prettyTCM TCErr
    err
                ProfileOption -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
    whenProfile ProfileOption
    Profile.Instances (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TCMT IO ()
    forall (m :: * -> *). MonadStatistics m => [Char] -> m ()
    tick [Char]
    "checkCandidateForMeta: no"
                YesNo -> TCM YesNo
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return YesNo
    No

    nowConsideringInstance :: (ReadTCState m) => m a -> m a
    nowConsideringInstance :: forall (m :: * -> *) a. ReadTCState m => m a -> m a
    nowConsideringInstance = Lens' TCState Bool -> (Bool -> Bool) -> m a -> m a
    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
    stConsideringInstance ((Bool -> Bool) -> m a -> m a) -> (Bool -> Bool) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ Bool -> Bool -> Bool
    forall a b. a -> b -> a
    const Bool
    True

    -- Rather than just the instance constraints, these are the constraints
    -- which could be suspended by being under 'nowConsideringInstances',
    -- which also includes unquote constraints.
    isInstanceProblemConstraint :: ProblemConstraint -> Bool
    isInstanceProblemConstraint :: ProblemConstraint -> Bool
    isInstanceProblemConstraint ProblemConstraint
    c = case Closure Constraint -> Constraint
    forall a. Closure a -> a
    clValue (ProblemConstraint -> Closure Constraint
    theConstraint ProblemConstraint
    c) of
      FindInstance{}  -> Bool
    True
      UnquoteTactic{} -> Bool
    True
      Constraint
    _ -> Bool
    False

    wakeupInstanceConstraints :: TCM ()
    wakeupInstanceConstraints :: TCMT IO ()
    wakeupInstanceConstraints =
      TCM Bool -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM TCM Bool
    forall (m :: * -> *). (ReadTCState m, HasOptions m) => m Bool
    shouldPostponeInstanceSearch (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ do
        (ProblemConstraint -> WakeUp) -> TCMT IO ()
    forall (m :: * -> *).
    MonadConstraint m =>
    (ProblemConstraint -> WakeUp) -> m ()
    wakeConstraints ((ProblemConstraint -> Bool) -> ProblemConstraint -> WakeUp
    forall constr. (constr -> Bool) -> constr -> WakeUp
    wakeUpWhen_ ProblemConstraint -> Bool
    isInstanceProblemConstraint)
        TCMT IO ()
    solveAwakeInstanceConstraints

    solveAwakeInstanceConstraints :: TCM ()
    solveAwakeInstanceConstraints :: TCMT IO ()
    solveAwakeInstanceConstraints =
      (ProblemConstraint -> Bool) -> Bool -> TCMT IO ()
    forall (m :: * -> *).
    MonadConstraint m =>
    (ProblemConstraint -> Bool) -> Bool -> m ()
    solveSomeAwakeConstraints ProblemConstraint -> Bool
    isInstanceProblemConstraint Bool
    False

    postponeInstanceConstraints :: TCM a -> TCM a
    postponeInstanceConstraints :: forall a. TCM a -> TCM a
    postponeInstanceConstraints TCM a
    m =
      Lens' TCState Bool -> (Bool -> Bool) -> TCM a -> TCM a
    forall a b. Lens' TCState a -> (a -> a) -> TCMT IO b -> TCMT IO 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
    stPostponeInstanceSearch (Bool -> Bool -> Bool
    forall a b. a -> b -> a
    const Bool
    True) TCM a
    m TCM a -> TCMT IO () -> TCM a
    forall a b. TCMT IO a -> TCMT IO b -> TCMT IO a
    forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
    <* TCMT IO ()
    wakeupInstanceConstraints

    flushInstanceConstraints :: TCM ()
    flushInstanceConstraints :: TCMT IO ()
    flushInstanceConstraints = Lens' TCState Bool -> (Bool -> Bool) -> TCMT IO () -> TCMT IO ()
    forall a b. Lens' TCState a -> (a -> a) -> TCMT IO b -> TCMT IO 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
    stInstanceHack (Bool -> Bool -> Bool
    forall a b. a -> b -> a
    const Bool
    True) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO ()
    wakeupInstanceConstraints

    -- | To preserve the invariant that a constructor is not applied to its
    --   parameter arguments, we explicitly check whether function term
    --   we are applying to arguments is a unapplied constructor.
    --   In this case we drop the first 'conPars' arguments.
    --   See Issue670a.
    --   Andreas, 2013-11-07 Also do this for projections, see Issue670b.
    --   Szumi, 2025-05-05: Unapplied projections are not considered by instance
    --   search since #938.
    applyDroppingParameters :: Term -> Args -> TCM Term
    applyDroppingParameters :: Term -> Args -> TCMT IO Term
    applyDroppingParameters Term
    t Args
    vs = do
      let fallback :: TCMT IO Term
    fallback = Term -> TCMT IO Term
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ Term
    t Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` Args
    vs
      case Term
    t of
        Con ConHead
    c ConInfo
    ci [] -> do
          def <- Definition -> Defn
    theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ConHead -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => ConHead -> m Definition
    getConInfo ConHead
    c
          case def of
            Constructor {conPars :: Defn -> Int
    conPars = Int
    n, conData :: Defn -> QName
    conData = QName
    d} -> do
              -- Szumi, 2025-05-05, issue #7853: don't drop parameters from the current module.
              fv <- QName -> TCMT IO Int
    forall (m :: * -> *).
    (Functor m, Applicative m, ReadTCState m, MonadTCEnv m) =>
    QName -> m Int
    getDefFreeVars QName
    d
              return $ Con c ci (map Apply $ drop (n - fv) vs)
            Defn
    _ -> TCMT IO Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        -- Def f [] -> do
        --   -- Andreas, 2022-03-07, issue #5809: don't drop parameters of irrelevant projections.
        --   mp <- isRelevantProjection f
        --   case mp of
        --     Just Projection{projIndex = n} -> do
        --       case drop n vs of
        --         []     -> return t
        --         u : us -> (`apply` us) <$> applyDef ProjPrefix f u
        --     _ -> fallback
        Term
    _ -> TCMT IO Term
    fallback

    ---------------------------------------------------------------------------
    -- * Instance definitions
    ---------------------------------------------------------------------------

    data OutputTypeName
      = OutputTypeName QName
      | OutputTypeVar
      | OutputTypeVisiblePi
      | OutputTypeNameNotYetKnown Blocker
      | NoOutputTypeName

    -- | Strips all hidden and instance Pi's and return the argument
    --   telescope, the head term, and its name, if possible.
    getOutputTypeName :: Type -> TCM (Telescope, Term, OutputTypeName)
    -- 2023-10-26, Jesper, issue #6941: To make instance search work correctly for
    -- abstract or opaque instances, we need to ignore abstract mode when computing
    -- the output type name.
    getOutputTypeName :: Type -> TCM (Telescope, Term, OutputTypeName)
    getOutputTypeName Type
    t = TCM (Telescope, Term, OutputTypeName)
    -> TCM (Telescope, Term, OutputTypeName)
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    ignoreAbstractMode (TCM (Telescope, Term, OutputTypeName)
     -> TCM (Telescope, Term, OutputTypeName))
    -> TCM (Telescope, Term, OutputTypeName)
    -> TCM (Telescope, Term, OutputTypeName)
    forall a b. (a -> b) -> a -> b
    $ do
      TelV tel t' <- Int -> (Dom Type -> Bool) -> Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Int -> (Dom Type -> Bool) -> Type -> m (TelV Type)
    telViewUpTo' (-Int
    1) Dom Type -> Bool
    forall a. LensHiding a => a -> Bool
    notVisible Type
    t
      ifBlocked (unEl t') (\Blocker
    b Term
    t -> (Telescope, Term, OutputTypeName)
    -> TCM (Telescope, Term, OutputTypeName)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Telescope
    tel , Term
    HasCallStack => Term
    __DUMMY_TERM__, Blocker -> OutputTypeName
    OutputTypeNameNotYetKnown Blocker
    b)) $ \ NotBlocked
    _ Term
    v ->
        case Term
    v of
          -- Possible base types:
          Def QName
    n Elims
    _  -> (Telescope, Term, OutputTypeName)
    -> TCM (Telescope, Term, OutputTypeName)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Telescope
    tel, Term
    v, QName -> OutputTypeName
    OutputTypeName QName
    n)
          Sort{}   -> (Telescope, Term, OutputTypeName)
    -> TCM (Telescope, Term, OutputTypeName)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Telescope
    tel, Term
    v, OutputTypeName
    NoOutputTypeName)
          Var Int
    n Elims
    _  -> (Telescope, Term, OutputTypeName)
    -> TCM (Telescope, Term, OutputTypeName)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Telescope
    tel, Term
    v, OutputTypeName
    OutputTypeVar)
          Pi{}     -> (Telescope, Term, OutputTypeName)
    -> TCM (Telescope, Term, OutputTypeName)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Telescope
    tel, Term
    v, OutputTypeName
    OutputTypeVisiblePi)
          -- Not base types:
          Con{}    -> TCM (Telescope, Term, OutputTypeName)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Lam{}    -> TCM (Telescope, Term, OutputTypeName)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Lit{}    -> TCM (Telescope, Term, OutputTypeName)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Level{}  -> TCM (Telescope, Term, OutputTypeName)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          MetaV{}  -> TCM (Telescope, Term, OutputTypeName)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          DontCare{} -> TCM (Telescope, Term, OutputTypeName)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Dummy [Char]
    s Elims
    _ -> [Char] -> TCM (Telescope, Term, OutputTypeName)
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    [Char] -> m a
    __IMPOSSIBLE_VERBOSE__ [Char]
    s

    -- | Register the definition with the given type as an instance.
    --   Issue warnings if instance is unusable.
    addTypedInstance ::
         QName  -- ^ Name of instance.
      -> Type   -- ^ Type of instance.
      -> TCM ()
    addTypedInstance :: QName -> Type -> TCMT IO ()
    addTypedInstance = Bool -> Bool -> Maybe InstanceInfo -> QName -> Type -> TCMT IO ()
    addTypedInstance' Bool
    True Bool
    False Maybe InstanceInfo
    forall a. Maybe a
    Nothing

    -- | Like 'addTypedInstance', but delete any existing entries for the
    -- given name from the discrimination tree.
    readdTypedInstance ::
         QName  -- ^ Name of instance.
      -> Type   -- ^ Type of instance.
      -> TCM ()
    readdTypedInstance :: QName -> Type -> TCMT IO ()
    readdTypedInstance = Bool -> Bool -> Maybe InstanceInfo -> QName -> Type -> TCMT IO ()
    addTypedInstance' Bool
    True Bool
    True Maybe InstanceInfo
    forall a. Maybe a
    Nothing

    -- | Register the definition with the given type as an instance.
    addTypedInstance'
      :: Bool               -- ^ Should we print warnings for unusable instance declarations?
      -> Bool               -- ^ Is this the second time we're adding this QName as an instance?
      -> Maybe InstanceInfo -- ^ Is this instance a copy?
      -> QName              -- ^ Name of instance.
      -> Type               -- ^ Type of instance.
      -> TCM ()
    addTypedInstance' :: Bool -> Bool -> Maybe InstanceInfo -> QName -> Type -> TCMT IO ()
    addTypedInstance' Bool
    w Bool
    readd Maybe InstanceInfo
    orig QName
    inst Type
    t = do
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.instance.add" Int
    30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    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
    vcat
        [ TCMT IO Doc
    "adding typed instance" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    inst TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "with type"
        , Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM (Type -> TCMT IO Doc) -> TCMT IO Type -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (Telescope -> Type -> Type) -> Type -> Telescope -> Type
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Telescope -> Type -> Type
    forall t. Abstract t => Telescope -> t -> t
    abstract Type
    t (Telescope -> Type) -> TCMT IO Telescope -> TCMT IO Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Telescope
    forall (m :: * -> *). MonadTCEnv m => m Telescope
    getContextTelescope
        ]

      (tel, hdt, n) <- Type -> TCM (Telescope, Term, OutputTypeName)
    getOutputTypeName Type
    t
      case n of
        OutputTypeName QName
    n -> Telescope -> TCMT IO () -> TCMT IO ()
    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 () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ do
          tele <- TCMT IO Telescope
    forall (m :: * -> *). MonadTCEnv m => m Telescope
    getContextTelescope

          -- Insert the instance into the instance table, putting it in the
          -- discrimination tree *and* bumping the total number of instances
          -- for this class.
          tree <- useTC stInstanceTree

          -- Amélia, 2025-02-28: If the instance we're adding has no type
          -- signature, we end up adding it to the tree twice: once with a
          -- useless type, and once after checking the RHS (which will have
          -- narrowed the type).
          --
          -- To avoid spurious overlap, the useful key should trump the
          -- useless key, so we filter this QName out of the tree when
          -- re-adding an instance.
          let
            tree' | Bool
    readd     = Set QName -> DiscrimTree QName -> DiscrimTree QName
    forall a. Ord a => Set a -> DiscrimTree a -> DiscrimTree a
    deleteFromDT (QName -> Set QName
    forall a. a -> Set a
    Set.singleton QName
    inst) DiscrimTree QName
    tree
                  | Bool
    otherwise = DiscrimTree QName
    tree

          tree' <- insertDT (length tele) hdt inst $! tree'
          setTCLens stInstanceTree tree'

          modifyTCLens' (stSignature . sigInstances . itableCounts) $
            if readd then Map.insertWith (+) n 1 else id

          let
            info = (InstanceInfo -> Maybe InstanceInfo -> InstanceInfo)
    -> Maybe InstanceInfo -> InstanceInfo -> InstanceInfo
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip InstanceInfo -> Maybe InstanceInfo -> InstanceInfo
    forall a. a -> Maybe a -> a
    fromMaybe Maybe InstanceInfo
    orig InstanceInfo
              { instanceClass :: QName
    instanceClass   = QName
    n
              , instanceOverlap :: OverlapMode
    instanceOverlap = OverlapMode
    DefaultOverlap
              }

          -- This is no longer used to build the instance table for imported
          -- modules, but it is still used to know if an instance should be
          -- copied when applying a section.
          modifySignature $ updateDefinition inst \ Definition
    d -> Definition
    d { defInstance = Just info }

          -- If there's anything visible in the context, which will
          -- eventually end up in the instance's type, let's make a note to
          -- get rid of it before serialising the instance table.
          con <- isConstructor inst
          -- However, do note that data constructors can have "visible
          -- arguments" in their global type which.. aren't actually
          -- visible: the parameters.
          when (any visible tele && not con) $ modifyTCLens' stTemporaryInstances $ Set.insert inst

        OutputTypeNameNotYetKnown Blocker
    b -> do
          QName -> TCMT IO ()
    addUnknownInstance QName
    inst
          Blocker -> Constraint -> TCMT IO ()
    forall (m :: * -> *).
    MonadConstraint m =>
    Blocker -> Constraint -> m ()
    addConstraint Blocker
    b (Constraint -> TCMT IO ()) -> Constraint -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ QName -> Constraint
    ResolveInstanceHead QName
    inst

        OutputTypeName
    NoOutputTypeName    -> Bool -> TCMT IO () -> TCMT IO ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when Bool
    w (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Warning -> TCMT IO ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCMT IO ()) -> Warning -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Warning
    WrongInstanceDeclaration
        OutputTypeName
    OutputTypeVar       -> Bool -> TCMT IO () -> TCMT IO ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when Bool
    w (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Warning -> TCMT IO ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCMT IO ()) -> Warning -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Warning
    WrongInstanceDeclaration
        OutputTypeName
    OutputTypeVisiblePi -> Bool -> TCMT IO () -> TCMT IO ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when Bool
    w (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Warning -> TCMT IO ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCMT IO ()) -> Warning -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ QName -> Warning
    InstanceWithExplicitArg QName
    inst

    resolveInstanceHead :: QName -> TCM ()
    resolveInstanceHead :: QName -> TCMT IO ()
    resolveInstanceHead QName
    q = do
      QName -> TCMT IO ()
    clearUnknownInstance QName
    q
      -- Andreas, 2022-12-04, issue #6380:
      -- Do not warn about unusable instances here.
      Bool -> Bool -> Maybe InstanceInfo -> QName -> Type -> TCMT IO ()
    addTypedInstance' Bool
    False Bool
    True Maybe InstanceInfo
    forall a. Maybe a
    Nothing QName
    q (Type -> TCMT IO ()) -> TCMT IO Type -> TCMT IO ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< QName -> TCMT IO Type
    forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m) =>
    QName -> m Type
    typeOfConst QName
    q

    -- | Try to solve the instance definitions whose type is not yet known, report
    --   an error if it doesn't work and return the instance table otherwise.
    getInstanceDefs :: TCM InstanceTable
    getInstanceDefs :: TCM InstanceTable
    getInstanceDefs = do
      (table, pending) <- TCM (InstanceTable, Set QName)
    getAllInstanceDefs
      unless (null pending) $ do
        patternViolation alwaysUnblock  -- TODO: more refined unblocking
      return table

    -- | Prune an 'Interface' to remove any instances that would be
    -- inapplicable in child modules.
    --
    -- While in a section with visible arguments, we add any instances
    -- defined locally to the instance table: you have to be able to find
    -- them, after all! Conservatively, all of the local variables are
    -- turned into 'FlexK's, i.e., wildcards.
    --
    -- But when we leave such a section, these instances have no more value:
    -- even though they might technically be in scope, their types are
    -- malformed, since they have visible pis.
    --
    -- This function deletes these instances from the instance tree in the
    -- given signature to save on serialisation time *and* time spent
    -- checking for candidate validity in client modules. It can't do this
    -- directly in the TC state to prevent these instances from going out of
    -- scope before interaction (see #7196).
    pruneTemporaryInstances :: Interface -> TCM Interface
    pruneTemporaryInstances :: Interface -> TCM Interface
    pruneTemporaryInstances Interface
    int = do
      todo <- Lens' TCState (Set QName) -> TCMT IO (Set QName)
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (Set QName -> f (Set QName)) -> TCState -> f TCState
    Lens' TCState (Set QName)
    stTemporaryInstances

      reportSDoc "tc.instance.prune" 30 $ vcat
        [ "leaving section"
        , prettyTCM =<< getContextTelescope
        , "todo:" <+> prettyTCM todo
        ]

      let sig' = Lens' Signature (DiscrimTree QName)
    -> LensMap Signature (DiscrimTree QName)
    forall o i. Lens' o i -> LensMap o i
    over ((InstanceTable -> f InstanceTable) -> Signature -> f Signature
    Lens' Signature InstanceTable
    sigInstances ((InstanceTable -> f InstanceTable) -> Signature -> f Signature)
    -> ((DiscrimTree QName -> f (DiscrimTree QName))
        -> InstanceTable -> f InstanceTable)
    -> (DiscrimTree QName -> f (DiscrimTree QName))
    -> Signature
    -> f Signature
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (DiscrimTree QName -> f (DiscrimTree QName))
    -> InstanceTable -> f InstanceTable
    Lens' InstanceTable (DiscrimTree QName)
    itableTree) (Set QName -> DiscrimTree QName -> DiscrimTree QName
    forall a. Ord a => Set a -> DiscrimTree a -> DiscrimTree a
    deleteFromDT Set QName
    todo) (Interface -> Signature
    iSignature Interface
    int)
      pure int{ iSignature = sig' }