    {-# LANGUAGE NondecreasingIndentation #-}

    module Agda.TypeChecking.InstanceArguments
      ( findInstance
      , isInstanceConstraint
      , shouldPostponeInstanceSearch
      , postponeInstanceConstraints
      ) where

    import Control.Monad        ( forM )
    import Control.Monad.Except ( MonadError(..) )
    import Control.Monad.Trans  ( lift )

    import qualified Data.IntMap as IntMap
    import qualified Data.Map as Map
    import qualified Data.Set as Set
    import qualified Data.List as List
    import Data.Bifunctor
    import Data.Foldable (toList)
    import Data.Function (on)
    import Data.Monoid hiding ((<>))

    import Agda.Interaction.Options (optOverlappingInstances, optQualifiedInstances)

    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 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 {-# SOURCE #-} Agda.TypeChecking.Constraints
    import {-# SOURCE #-} Agda.TypeChecking.Conversion

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

    import Agda.Utils.Either
    import Agda.Utils.Lens
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Pretty (prettyShow)
    import Agda.Utils.Null (empty)

    import Agda.Utils.Impossible

    -- | 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 :: Type -> TCM (Either Blocker [Candidate])
    initialInstanceCandidates :: Type -> TCM (Either Blocker [Candidate])
    initialInstanceCandidates Type
    t = do
      (Tele (Dom Type)
    _ , OutputTypeName
    otn) <- Type -> TCM (Tele (Dom Type), OutputTypeName)
    getOutputTypeName Type
    t
      case OutputTypeName
    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
    $ [Char] -> TypeError
    GenericError ([Char] -> TypeError) -> [Char] -> TypeError
    forall a b. (a -> b) -> a -> b
    $
          [Char]
    "Instance search can only be used to find elements in a named type"
        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 (m :: * -> *) a. Monad m => a -> m a
    return (Blocker -> Either Blocker [Candidate]
    forall a b. a -> Either a b
    Left Blocker
    b)
        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
    $ [Char] -> TypeError
    GenericError ([Char] -> TypeError) -> [Char] -> TypeError
    forall a b. (a -> b) -> a -> b
    $
          [Char]
    "Instance search cannot be used to find elements in an explicit function type"
        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 BlockT (TCMT IO) [Candidate]
    getContextVars
        OutputTypeName QName
    n -> 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
    prettyTCM QName
    n
          BlockT (TCMT IO) [Candidate] -> TCM (Either Blocker [Candidate])
    forall (m :: * -> *) a.
    Monad m =>
    BlockT m a -> m (Either Blocker a)
    runBlocked BlockT (TCMT IO) [Candidate]
    getContextVars TCM (Either Blocker [Candidate])
    -> (Either Blocker [Candidate] -> TCM (Either Blocker [Candidate]))
    -> TCM (Either Blocker [Candidate])
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
            Left Blocker
    b -> Either Blocker [Candidate] -> TCM (Either Blocker [Candidate])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either Blocker [Candidate] -> TCM (Either Blocker [Candidate]))
    -> Either Blocker [Candidate] -> TCM (Either Blocker [Candidate])
    forall a b. (a -> b) -> a -> b
    $ Blocker -> Either Blocker [Candidate]
    forall a b. a -> Either a b
    Left Blocker
    b
            Right [Candidate]
    ctxVars -> [Candidate] -> Either Blocker [Candidate]
    forall a b. b -> Either a b
    Right ([Candidate] -> Either Blocker [Candidate])
    -> ([Candidate] -> [Candidate])
    -> [Candidate]
    -> Either Blocker [Candidate]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([Candidate]
    ctxVars [Candidate] -> [Candidate] -> [Candidate]
    forall a. [a] -> [a] -> [a]
    ++) ([Candidate] -> Either Blocker [Candidate])
    -> TCMT IO [Candidate] -> TCM (Either Blocker [Candidate])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO [Candidate]
    getScopeDefs QName
    n
      where
        -- get a list of variables with their type, relative to current context
        getContextVars :: BlockT TCM [Candidate]
        getContextVars :: BlockT (TCMT IO) [Candidate]
    getContextVars = do
          [Dom (Name, Type)]
    ctx <- BlockT (TCMT IO) [Dom (Name, Type)]
    forall (m :: * -> *). MonadTCEnv m => m [Dom (Name, Type)]
    getContext
          [Char] -> Int -> TCMT IO Doc -> BlockT (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.instance.cands" Int
    40 (TCMT IO Doc -> BlockT (TCMT IO) ())
    -> TCMT IO Doc -> BlockT (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc -> Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *).
    Applicative m =>
    m Doc -> Int -> m Doc -> m Doc
    hang TCMT IO Doc
    "Getting candidates from context" Int
    2 (TCMT IO Doc -> TCMT IO Doc
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ PrettyContext -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (PrettyContext -> TCMT IO Doc) -> PrettyContext -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Dom (Name, Type)] -> PrettyContext
    PrettyContext [Dom (Name, Type)]
    ctx)
              -- Context variables with their types lifted to live in the full context
          let varsAndRaisedTypes :: [(Term, Dom (Name, Type))]
    varsAndRaisedTypes = [ (Int -> Term
    var Int
    i, Int -> Dom (Name, Type) -> Dom (Name, Type)
    forall a. Subst a => Int -> a -> a
    raise (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) Dom (Name, Type)
    t) | (Int
    i, Dom (Name, Type)
    t) <- [Int] -> [Dom (Name, Type)] -> [(Int, Dom (Name, Type))]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Int
    0..] [Dom (Name, Type)]
    ctx ]
              vars :: [Candidate]
    vars = [ CandidateKind -> Term -> Type -> Bool -> Candidate
    Candidate CandidateKind
    LocalCandidate Term
    x Type
    t (ArgInfo -> Bool
    forall a. LensHiding a => a -> Bool
    isOverlappable 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 = (Name
    _, Type
    t)}) <- [(Term, Dom (Name, Type))]
    varsAndRaisedTypes
                     , ArgInfo -> Bool
    forall a. LensHiding a => a -> Bool
    isInstance ArgInfo
    info
                     ]

          -- {{}}-fields of variables are also candidates
          let cxtAndTypes :: [(CandidateKind, Term, Type)]
    cxtAndTypes = [ (CandidateKind
    LocalCandidate, Term
    x, Type
    t) | (Term
    x, Dom{unDom :: forall t e. Dom' t e -> e
    unDom = (Name
    _, Type
    t)}) <- [(Term, Dom (Name, Type))]
    varsAndRaisedTypes ]
          [Candidate]
    fields <- [[Candidate]] -> [Candidate]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([[Candidate]] -> [Candidate])
    -> BlockT (TCMT IO) [[Candidate]] -> BlockT (TCMT IO) [Candidate]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((CandidateKind, Term, Type) -> BlockT (TCMT IO) [Candidate])
    -> [(CandidateKind, Term, Type)] -> BlockT (TCMT IO) [[Candidate]]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (CandidateKind, Term, Type) -> BlockT (TCMT IO) [Candidate]
    instanceFields ([(CandidateKind, Term, Type)] -> [(CandidateKind, Term, Type)]
    forall a. [a] -> [a]
    reverse [(CandidateKind, Term, Type)]
    cxtAndTypes)
          [Char] -> Int -> TCMT IO Doc -> BlockT (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.instance.fields" Int
    30 (TCMT IO Doc -> BlockT (TCMT IO) ())
    -> TCMT IO Doc -> BlockT (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $
            if [Candidate] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Candidate]
    fields then TCMT IO Doc
    "no instance field candidates" else
              TCMT IO Doc
    "instance field candidates" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$ do
                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] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ (if Bool
    overlap then TCMT IO Doc
    "overlap" else TCMT IO Doc
    forall a. Null a => a
    empty) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Candidate -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Candidate
    c 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
    $ Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t
                        ]
                  | c :: Candidate
    c@(Candidate CandidateKind
    q Term
    v Type
    t Bool
    overlap) <- [Candidate]
    fields
                  ]

          -- get let bindings
          LetBindings
    env <- (TCEnv -> LetBindings) -> BlockT (TCMT IO) LetBindings
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> LetBindings
    envLetBindings
          [(Name, (Term, Dom Type))]
    env <- ((Name, Open (Term, Dom Type))
     -> BlockT (TCMT IO) (Name, (Term, Dom Type)))
    -> [(Name, Open (Term, Dom Type))]
    -> BlockT (TCMT IO) [(Name, (Term, Dom Type))]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ((Open (Term, Dom Type) -> BlockT (TCMT IO) (Term, Dom Type))
    -> (Name, Open (Term, Dom Type))
    -> BlockT (TCMT IO) (Name, (Term, Dom Type))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse Open (Term, Dom Type) -> BlockT (TCMT IO) (Term, Dom Type)
    forall a (m :: * -> *).
    (TermSubst a, MonadTCEnv m) =>
    Open a -> m a
    getOpen) ([(Name, Open (Term, Dom Type))]
     -> BlockT (TCMT IO) [(Name, (Term, Dom Type))])
    -> [(Name, Open (Term, Dom Type))]
    -> BlockT (TCMT IO) [(Name, (Term, Dom Type))]
    forall a b. (a -> b) -> a -> b
    $ LetBindings -> [(Name, Open (Term, Dom Type))]
    forall k a. Map k a -> [(k, a)]
    Map.toList LetBindings
    env
          let lets :: [Candidate]
    lets = [ CandidateKind -> Term -> Type -> Bool -> Candidate
    Candidate CandidateKind
    LocalCandidate Term
    v Type
    t Bool
    False
                     | (Name
    _,(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, (Term, Dom Type))]
    env
                     , ArgInfo -> Bool
    forall a. LensHiding a => a -> Bool
    isInstance ArgInfo
    info
                     , ArgInfo -> Bool
    forall a. LensModality a => a -> Bool
    usableModality ArgInfo
    info
                     ]
          [Candidate] -> BlockT (TCMT IO) [Candidate]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Candidate] -> BlockT (TCMT IO) [Candidate])
    -> [Candidate] -> BlockT (TCMT IO) [Candidate]
    forall a b. (a -> b) -> a -> b
    $ [Candidate]
    vars [Candidate] -> [Candidate] -> [Candidate]
    forall a. [a] -> [a] -> [a]
    ++ [Candidate]
    fields [Candidate] -> [Candidate] -> [Candidate]
    forall a. [a] -> [a] -> [a]
    ++ [Candidate]
    lets

        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 (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, Defn))
    forall (m :: * -> *).
    PureTCM m =>
    Type -> m (Maybe (QName, Args, Defn))
    isRecordType Type
    t m (Maybe (QName, Args, Defn))
    -> (Maybe (QName, Args, Defn) -> m (Maybe (QName, Args)))
    -> m (Maybe (QName, Args))
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
                Maybe (QName, Args, Defn)
    Nothing         -> Maybe (QName, Args) -> m (Maybe (QName, Args))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (QName, Args)
    forall a. Maybe a
    Nothing
                Just (QName
    r, Args
    vs, Defn
    _) -> do
                  ModuleName
    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 QName -> [Name]
    qnameToList0 QName
    r [Name] -> [Name] -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `List.isPrefixOf` ModuleName -> [Name]
    mnameToList ModuleName
    m
                    then Maybe (QName, Args) -> m (Maybe (QName, Args))
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((QName, Args) -> Maybe (QName, Args)
    forall a. a -> Maybe a
    Just (QName
    r, Args
    vs))
                    else Maybe (QName, Args) -> m (Maybe (QName, Args))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (QName, Args)
    forall a. Maybe a
    Nothing
            Maybe (QName, Args)
    r -> Maybe (QName, Args) -> m (Maybe (QName, Args))
    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 (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 (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
            (Tele (Dom Type)
    tel, Args
    args) <- TCM (Tele (Dom Type), Args)
    -> BlockT (TCMT IO) (Tele (Dom Type), Args)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM (Tele (Dom Type), Args)
     -> BlockT (TCMT IO) (Tele (Dom Type), Args))
    -> TCM (Tele (Dom Type), Args)
    -> BlockT (TCMT IO) (Tele (Dom Type), Args)
    forall a b. (a -> b) -> a -> b
    $ QName -> Args -> Term -> TCM (Tele (Dom Type), Args)
    forall (m :: * -> *).
    (HasConstInfo m, MonadDebug m, ReadTCState m,
     MonadError TCErr m) =>
    QName -> Args -> Term -> m (Tele (Dom Type), Args)
    forceEtaExpandRecord QName
    r Args
    pars Term
    v
            let types :: [Type]
    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 ([Term] -> Substitution' Term
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS ([Term] -> Substitution' Term) -> [Term] -> Substitution' Term
    forall a b. (a -> b) -> a -> b
    $ [Term] -> [Term]
    forall a. [a] -> [a]
    reverse ([Term] -> [Term]) -> [Term] -> [Term]
    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) (Tele (Dom Type) -> [Dom Type]
    forall a. TermSubst a => Tele (Dom a) -> [Dom a]
    flattenTel Tele (Dom Type)
    tel)
            ([[Candidate]] -> [Candidate])
    -> BlockT (TCMT IO) [[Candidate]] -> BlockT (TCMT IO) [Candidate]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap [[Candidate]] -> [Candidate]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat (BlockT (TCMT IO) [[Candidate]] -> BlockT (TCMT IO) [Candidate])
    -> BlockT (TCMT IO) [[Candidate]] -> BlockT (TCMT IO) [Candidate]
    forall a b. (a -> b) -> a -> b
    $ [(Arg Term, Type)]
    -> ((Arg Term, Type) -> BlockT (TCMT IO) [Candidate])
    -> BlockT (TCMT IO) [[Candidate]]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM (Args -> [Type] -> [(Arg Term, Type)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip Args
    args [Type]
    types) (((Arg Term, Type) -> BlockT (TCMT IO) [Candidate])
     -> BlockT (TCMT IO) [[Candidate]])
    -> ((Arg Term, Type) -> BlockT (TCMT IO) [Candidate])
    -> BlockT (TCMT IO) [[Candidate]]
    forall a b. (a -> b) -> a -> b
    $ \ (Arg Term
    arg, Type
    t) ->
              ([ CandidateKind -> Term -> Type -> Bool -> Candidate
    Candidate CandidateKind
    LocalCandidate (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    arg) Type
    t (Arg Term -> Bool
    forall a. LensHiding a => a -> Bool
    isOverlappable 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)

        getScopeDefs :: QName -> TCM [Candidate]
        getScopeDefs :: QName -> TCMT IO [Candidate]
    getScopeDefs QName
    n = do
          InstanceTable
    instanceDefs <- TCM InstanceTable
    getInstanceDefs
          Relevance
    rel          <- (TCEnv -> Relevance) -> TCMT IO Relevance
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance
          let qs :: [QName]
    qs = [QName] -> (Set QName -> [QName]) -> Maybe (Set QName) -> [QName]
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe [] Set QName -> [QName]
    forall a. Set a -> [a]
    Set.toList (Maybe (Set QName) -> [QName]) -> Maybe (Set QName) -> [QName]
    forall a b. (a -> b) -> a -> b
    $ QName -> InstanceTable -> Maybe (Set QName)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup QName
    n InstanceTable
    instanceDefs
          [Maybe Candidate] -> [Candidate]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe Candidate] -> [Candidate])
    -> TCMT IO [Maybe Candidate] -> TCMT IO [Candidate]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (QName -> TCMT IO (Maybe Candidate))
    -> [QName] -> TCMT IO [Maybe Candidate]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Relevance -> QName -> TCMT IO (Maybe Candidate)
    candidate Relevance
    rel) [QName]
    qs

        candidate :: Relevance -> QName -> TCM (Maybe Candidate)
        candidate :: Relevance -> QName -> TCMT IO (Maybe Candidate)
    candidate Relevance
    rel QName
    q = TCMT IO Bool
    -> TCMT IO (Maybe Candidate)
    -> TCMT IO (Maybe Candidate)
    -> TCMT IO (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 -> TCMT IO 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 -> TCMT IO (Maybe Candidate)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Candidate
    forall a. Maybe a
    Nothing) (TCMT IO (Maybe Candidate) -> TCMT IO (Maybe Candidate))
    -> TCMT IO (Maybe Candidate) -> TCMT IO (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.
          TCMT IO (Maybe Candidate) -> TCMT IO (Maybe Candidate)
    filterQualified (TCMT IO (Maybe Candidate) -> TCMT IO (Maybe Candidate))
    -> TCMT IO (Maybe Candidate) -> TCMT IO (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)
          (TCMT IO (Maybe Candidate)
     -> (TCErr -> TCMT IO (Maybe Candidate))
     -> TCMT IO (Maybe Candidate))
    -> (TCErr -> TCMT IO (Maybe Candidate))
    -> TCMT IO (Maybe Candidate)
    -> TCMT IO (Maybe Candidate)
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip TCMT IO (Maybe Candidate)
    -> (TCErr -> TCMT IO (Maybe Candidate))
    -> TCMT IO (Maybe Candidate)
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    catchError TCErr -> TCMT IO (Maybe Candidate)
    forall {m :: * -> *} {a}.
    MonadError TCErr m =>
    TCErr -> m (Maybe a)
    handle (TCMT IO (Maybe Candidate) -> TCMT IO (Maybe Candidate))
    -> TCMT IO (Maybe Candidate) -> TCMT IO (Maybe Candidate)
    forall a b. (a -> b) -> a -> b
    $ do
            Definition
    def <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
            if Bool -> Bool
    not (Definition -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance Definition
    def Relevance -> Relevance -> Bool
    `moreRelevant` Relevance
    rel) then Maybe Candidate -> TCMT IO (Maybe Candidate)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Candidate
    forall a. Maybe a
    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
    args <- QName -> TCMT IO Args
    forall (m :: * -> *).
    (Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
     MonadTCEnv m, MonadDebug m) =>
    QName -> m Args
    freeVarsToApply QName
    q
              let t :: Type
    t = Definition -> Type
    defType Definition
    def Type -> Args -> Type
    `piApply` Args
    args
                  rel :: Relevance
    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
              let v :: Term
    v = case Definition -> Defn
    theDef Definition
    def of
                   -- drop parameters if it's a projection function...
                   Function{ funProjection :: Defn -> Maybe Projection
    funProjection = Just 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' Term) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply Args
    args
              Maybe Candidate -> TCMT IO (Maybe Candidate)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Candidate -> TCMT IO (Maybe Candidate))
    -> Maybe Candidate -> TCMT IO (Maybe Candidate)
    forall a b. (a -> b) -> a -> b
    $ Candidate -> Maybe Candidate
    forall a. a -> Maybe a
    Just (Candidate -> Maybe Candidate) -> Candidate -> Maybe Candidate
    forall a b. (a -> b) -> a -> b
    $ CandidateKind -> Term -> Type -> Bool -> Candidate
    Candidate (QName -> CandidateKind
    GlobalCandidate QName
    q) Term
    v Type
    t Bool
    False
          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 (m :: * -> *) a. Monad m => a -> m a
    return Maybe a
    forall a. Maybe a
    Nothing
            handle TCErr
    err                                                   = TCErr -> m (Maybe a)
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError TCErr
    err

            filterQualified :: TCM (Maybe Candidate) -> TCM (Maybe Candidate)
            filterQualified :: TCMT IO (Maybe Candidate) -> TCMT IO (Maybe Candidate)
    filterQualified TCMT IO (Maybe Candidate)
    m = TCMT IO Bool
    -> TCMT IO (Maybe Candidate)
    -> TCMT IO (Maybe Candidate)
    -> TCMT IO (Maybe Candidate)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (PragmaOptions -> Bool
    optQualifiedInstances (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions) TCMT IO (Maybe Candidate)
    m (TCMT IO (Maybe Candidate) -> TCMT IO (Maybe Candidate))
    -> TCMT IO (Maybe Candidate) -> TCMT IO (Maybe Candidate)
    forall a b. (a -> b) -> a -> b
    $ do
              [QName]
    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
    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
              [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.instance.qualified" Int
    30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
                if Bool
    isQual then
                  TCMT IO Doc
    "dropping qualified 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
    prettyTCM QName
    q
                else
                  TCMT IO Doc
    "keeping 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
    prettyTCM QName
    q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
                  TCMT IO Doc
    "since it is in scope as" 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
    prettyTCM [QName]
    qc
              if Bool
    isQual then Maybe Candidate -> TCMT IO (Maybe Candidate)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Candidate
    forall a. Maybe a
    Nothing else TCMT IO (Maybe Candidate)
    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
      -- Andreas, 2015-02-07: New metas should be created with range of the
      -- current instance meta, thus, we set the range.
      MetaVariable
    mv <- MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    m
      MetaVariable -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange MetaVariable
    mv (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ do
        [Char] -> Int -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.instance" Int
    20 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "The type of the FindInstance constraint isn't known, trying to find it again."
        Type
    t <- Type -> TCMT IO Type
    forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
    instantiate (Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< MetaId -> TCMT IO Type
    forall (m :: * -> *).
    (MonadFail m, MonadTCEnv m, ReadTCState m, MonadReduce m,
     HasBuiltins m) =>
    MetaId -> m Type
    getMetaTypeInContext MetaId
    m
        [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 1: t: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Type -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Type
    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 Tele (Dom Type)
    tel Type
    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
        Either Blocker [Candidate]
    cands <- Tele (Dom Type)
    -> TCM (Either Blocker [Candidate])
    -> TCM (Either Blocker [Candidate])
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Tele (Dom Type)
    tel (TCM (Either Blocker [Candidate])
     -> TCM (Either Blocker [Candidate]))
    -> TCM (Either Blocker [Candidate])
    -> TCM (Either Blocker [Candidate])
    forall a b. (a -> b) -> a -> b
    $ Type -> TCM (Either Blocker [Candidate])
    initialInstanceCandidates Type
    t
        case Either Blocker [Candidate]
    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
    $ MetaId -> Maybe [Candidate] -> Constraint
    FindInstance 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) =                          -- Note: if no blocking meta variable this will not unblock until the end of the mutual block
      TCMT IO (Maybe ([Candidate], Blocker))
    -> (([Candidate], Blocker) -> TCMT IO ()) -> TCMT IO ()
    forall (m :: * -> *) a.
    Monad m =>
    m (Maybe a) -> (a -> m ()) -> m ()
    whenJustM (MetaId -> [Candidate] -> TCMT IO (Maybe ([Candidate], Blocker))
    findInstance' MetaId
    m [Candidate]
    cands) ((([Candidate], Blocker) -> TCMT IO ()) -> TCMT IO ())
    -> (([Candidate], Blocker) -> TCMT IO ()) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ (\ ([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
    $ MetaId -> Maybe [Candidate] -> Constraint
    FindInstance 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)

    -- | 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 = TCMT IO 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 -> TCMT IO Bool
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m Bool
    isFrozen MetaId
    m) (do
        [Char] -> Int -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.instance" Int
    20 [Char]
    "Refusing to solve frozen instance meta."
        Maybe ([Candidate], Blocker)
    -> TCMT IO (Maybe ([Candidate], Blocker))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (([Candidate], Blocker) -> Maybe ([Candidate], Blocker)
    forall a. a -> Maybe a
    Just ([Candidate]
    cands, Blocker
    neverUnblock))) (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
    $ do
      TCMT IO 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 TCMT IO Bool
    forall (m :: * -> *). (ReadTCState m, HasOptions m) => m Bool
    shouldPostponeInstanceSearch (do
        [Char] -> Int -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.instance" Int
    20 [Char]
    "Postponing possibly recursive instance search."
        Maybe ([Candidate], Blocker)
    -> TCMT IO (Maybe ([Candidate], Blocker))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe ([Candidate], Blocker)
     -> TCMT IO (Maybe ([Candidate], Blocker)))
    -> Maybe ([Candidate], Blocker)
    -> TCMT IO (Maybe ([Candidate], Blocker))
    forall a b. (a -> b) -> a -> b
    $ ([Candidate], Blocker) -> Maybe ([Candidate], Blocker)
    forall a. a -> Maybe a
    Just ([Candidate]
    cands, Blocker
    neverUnblock)) (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
    $ 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] (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
    $ do
      -- Andreas, 2015-02-07: New metas should be created with range of the
      -- current instance meta, thus, we set the range.
      MetaVariable
    mv <- MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    m
      MetaVariable
    -> TCMT IO (Maybe ([Candidate], Blocker))
    -> TCMT IO (Maybe ([Candidate], Blocker))
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange MetaVariable
    mv (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
    $ do
          [Char] -> Int -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.instance" Int
    15 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
            [Char]
    "findInstance 2: constraint: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ MetaId -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow MetaId
    m [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "; candidates left: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show ([Candidate] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Candidate]
    cands)
          [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.instance" Int
    60 (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] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ (if Bool
    overlap then TCMT IO Doc
    "overlap" else TCMT IO Doc
    forall a. Null a => a
    empty) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Candidate -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Candidate
    c 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
    $ Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t ] | c :: Candidate
    c@(Candidate CandidateKind
    q Term
    v Type
    t Bool
    overlap) <- [Candidate]
    cands ]
          [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
    $ TCMT IO Doc
    "raw" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$ do
           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] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ (if Bool
    overlap then TCMT IO Doc
    "overlap" else TCMT IO Doc
    forall a. Null a => a
    empty) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Candidate -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Candidate
    c 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
    $ Type -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Type
    t ] | c :: Candidate
    c@(Candidate CandidateKind
    q Term
    v Type
    t Bool
    overlap) <- [Candidate]
    cands ]
          Type
    t <- MetaId -> TCMT IO Type
    forall (m :: * -> *).
    (MonadFail m, MonadTCEnv m, ReadTCState m, MonadReduce m,
     HasBuiltins m) =>
    MetaId -> m Type
    getMetaTypeInContext MetaId
    m
          [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 2: t: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Type -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Type
    t
          Type
    -> (Type -> TCMT IO (Maybe ([Candidate], Blocker)))
    -> TCMT IO (Maybe ([Candidate], Blocker))
    forall a. Type -> (Type -> TCM a) -> TCM a
    insidePi Type
    t ((Type -> TCMT IO (Maybe ([Candidate], Blocker)))
     -> TCMT IO (Maybe ([Candidate], Blocker)))
    -> (Type -> TCMT IO (Maybe ([Candidate], Blocker)))
    -> TCMT IO (Maybe ([Candidate], Blocker))
    forall a b. (a -> b) -> a -> b
    $ \ 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
    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

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

          TCMT IO ()
    debugConstraints
          case Maybe ([(Candidate, TCErr)], [Candidate])
    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 e (m :: * -> *) a. MonadError e m => e -> m a
    throwError TCErr
    err
            Just ([(Candidate, TCErr)]
    errs, []) -> do
              if [(Candidate, TCErr)] -> 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 (Int32 -> Int32 -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Int32 -> Int32 -> Ordering)
    -> ((Candidate, TCErr) -> Int32)
    -> (Candidate, TCErr)
    -> (Candidate, TCErr)
    -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` (Candidate, TCErr) -> Int32
    precision) [(Candidate, TCErr)]
    errs
                    where precision :: (Candidate, TCErr) -> Int32
    precision (Candidate
    _, TCErr
    err) = Int32 -> (Interval' () -> Int32) -> Maybe (Interval' ()) -> Int32
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Int32
    infinity Interval' () -> Int32
    forall a. Interval' a -> Int32
    iLength (Maybe (Interval' ()) -> Int32) -> Maybe (Interval' ()) -> Int32
    forall a b. (a -> b) -> a -> b
    $ Range' SrcFile -> Maybe (Interval' ())
    forall a. Range' a -> Maybe (Interval' ())
    rangeToInterval (Range' SrcFile -> Maybe (Interval' ()))
    -> Range' SrcFile -> Maybe (Interval' ())
    forall a b. (a -> b) -> a -> b
    $ TCErr -> Range' SrcFile
    forall a. HasRange a => a -> Range' SrcFile
    getRange TCErr
    err
                          infinity :: Int32
    infinity = Int32
    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)]
    _, [c :: Candidate
    c@(Candidate CandidateKind
    q Term
    term Type
    t' Bool
    _)]) -> 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
    "findInstance 5: solved by instance search using the only candidate"
                , 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
    $ Candidate -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Candidate
    c 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
    prettyTCM Term
    term
                , TCMT IO Doc
    "of type " 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
    prettyTCM Type
    t'
                , TCMT IO Doc
    "for type" 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
    prettyTCM Type
    t
                ]

              -- If we actually solved the constraints we should wake up any held
              -- instance constraints, to make sure we don't forget about them.
              TCMT IO ()
    wakeupInstanceConstraints
              Maybe ([Candidate], Blocker)
    -> TCMT IO (Maybe ([Candidate], Blocker))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe ([Candidate], Blocker)
    forall a. Maybe a
    Nothing  -- We’re done

            Maybe ([(Candidate, TCErr)], [Candidate])
    _ -> do
              let cs :: [Candidate]
    cs = [Candidate]
    -> (([(Candidate, TCErr)], [Candidate]) -> [Candidate])
    -> Maybe ([(Candidate, TCErr)], [Candidate])
    -> [Candidate]
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe [Candidate]
    cands ([(Candidate, TCErr)], [Candidate]) -> [Candidate]
    forall a b. (a, b) -> b
    snd Maybe ([(Candidate, TCErr)], [Candidate])
    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
    prettyTCM ((Candidate -> Term) -> [Candidate] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    List.map Candidate -> Term
    candidateTerm [Candidate]
    cs)
              Maybe ([Candidate], Blocker)
    -> TCMT IO (Maybe ([Candidate], Blocker))
    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 (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
    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 reseting 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.
    filterResetingState :: MetaId -> [Candidate] -> (Candidate -> TCM YesNoMaybe) -> TCM ([(Candidate, TCErr)], [Candidate])
    filterResetingState :: MetaId
    -> [Candidate]
    -> (Candidate -> TCM YesNoMaybe)
    -> TCM ([(Candidate, TCErr)], [Candidate])
    filterResetingState MetaId
    m [Candidate]
    cands Candidate -> TCM YesNoMaybe
    f = do
      Args
    ctxArgs  <- TCMT IO Args
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
    getContextArgs
      let ctxElims :: Elims
    ctxElims = (Arg Term -> Elim' Term) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply Args
    ctxArgs
          tryC :: Candidate -> TCMT IO (YesNoMaybe, Term)
    tryC Candidate
    c = do
            YesNoMaybe
    ok <- Candidate -> TCM YesNoMaybe
    f Candidate
    c
            Term
    v  <- Term -> TCMT IO Term
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull (MetaId -> Elims -> Term
    MetaV MetaId
    m Elims
    ctxElims)
            (YesNoMaybe, Term) -> TCMT IO (YesNoMaybe, Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (YesNoMaybe
    ok, Term
    v)
      [(Candidate, ((YesNoMaybe, Term), TCState))]
    result <- (Candidate -> TCMT IO (Candidate, ((YesNoMaybe, Term), TCState)))
    -> [Candidate]
    -> TCMT IO [(Candidate, ((YesNoMaybe, Term), TCState))]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (\Candidate
    c -> do ((YesNoMaybe, Term), TCState)
    bs <- TCMT IO (YesNoMaybe, Term) -> TCM ((YesNoMaybe, Term), TCState)
    forall a. TCM a -> TCM (a, TCState)
    localTCStateSaving (Candidate -> TCMT IO (YesNoMaybe, Term)
    tryC Candidate
    c); (Candidate, ((YesNoMaybe, Term), TCState))
    -> TCMT IO (Candidate, ((YesNoMaybe, Term), TCState))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Candidate
    c, ((YesNoMaybe, Term), TCState)
    bs)) [Candidate]
    cands

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

      -- c : Candidate
      -- r : YesNoMaybe
      -- v : Term         (fully instantiated)
      -- a : Type         (fully instantiated)
      -- s : TCState
      let result' :: [(Candidate, Term, TCState)]
    result' = [ (Candidate
    c, Term
    v, TCState
    s) | (Candidate
    c, ((YesNoMaybe
    r, Term
    v), TCState
    s)) <- [(Candidate, ((YesNoMaybe, Term), TCState))]
    result, Bool -> Bool
    not (YesNoMaybe -> Bool
    isNo YesNoMaybe
    r) ]
      [(Candidate, Term, TCState)]
    result'' <- MetaId
    -> [(Candidate, Term, TCState)] -> TCM [(Candidate, Term, TCState)]
    forall a.
    MetaId -> [(Candidate, Term, a)] -> TCM [(Candidate, Term, a)]
    dropSameCandidates MetaId
    m [(Candidate, Term, TCState)]
    result'
      case [(Candidate, Term, TCState)]
    result'' of
        [(Candidate
    c, Term
    _, TCState
    s)] -> ([], [Candidate
    c]) ([(Candidate, TCErr)], [Candidate])
    -> TCMT IO () -> TCM ([(Candidate, TCErr)], [Candidate])
    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, Term
    _), TCState
    _)) <- [(Candidate, ((YesNoMaybe, Term), TCState))]
    result ]
              good :: [Candidate]
    good = [ Candidate
    c | (Candidate
    c, Term
    _, TCState
    _) <- [(Candidate, Term, TCState)]
    result'' ]
          ([(Candidate, TCErr)], [Candidate])
    -> TCM ([(Candidate, TCErr)], [Candidate])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(Candidate, TCErr)]
    bad, [Candidate]
    good)

    -- 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 -> [(Candidate, Term, a)] -> TCM [(Candidate, Term, a)]
    dropSameCandidates :: forall a.
    MetaId -> [(Candidate, Term, a)] -> TCM [(Candidate, Term, a)]
    dropSameCandidates MetaId
    m [(Candidate, Term, a)]
    cands0 = [Char]
    -> Int
    -> [Char]
    -> TCMT IO [(Candidate, Term, a)]
    -> TCMT IO [(Candidate, Term, a)]
    forall (m :: * -> *) a.
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m a -> m a
    verboseBracket [Char]
    "tc.instance" Int
    30 [Char]
    "dropSameCandidates" (TCMT IO [(Candidate, Term, a)] -> TCMT IO [(Candidate, Term, a)])
    -> TCMT IO [(Candidate, Term, a)] -> TCMT IO [(Candidate, Term, a)]
    forall a b. (a -> b) -> a -> b
    $ do
      MetaStore
    metas <- TCMT IO MetaStore
    forall (m :: * -> *). ReadTCState m => m MetaStore
    getMetaStore
      -- Does `it` have any metas in the initial meta variable store?
      let freshMetas :: Term -> Bool
    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 t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas (Bool -> Any
    Any (Bool -> Any) -> (MetaId -> Bool) -> MetaId -> Any
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int -> MetaStore -> Bool
    forall a. Int -> IntMap a -> Bool
    `IntMap.notMember` MetaStore
    metas) (Int -> Bool) -> (MetaId -> Int) -> MetaId -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MetaId -> Int
    metaId)

      -- Take overlappable candidates into account
      let cands :: [(Candidate, Term, a)]
    cands =
            case ((Candidate, Term, a) -> Bool)
    -> [(Candidate, Term, a)]
    -> ([(Candidate, Term, a)], [(Candidate, Term, a)])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    List.partition (\ (Candidate
    c, Term
    _, a
    _) -> Candidate -> Bool
    candidateOverlappable Candidate
    c) [(Candidate, Term, a)]
    cands0 of
              ((Candidate, Term, a)
    cand : [(Candidate, Term, a)]
    _, []) -> [(Candidate, Term, a)
    cand]  -- only overlappable candidates: pick the first one
              ([(Candidate, Term, a)], [(Candidate, Term, a)])
    _              -> [(Candidate, Term, a)]
    cands0  -- otherwise require equality

      [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] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
        [ TCMT IO Doc
    "valid candidates:"
        , 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 [ if Term -> Bool
    freshMetas Term
    v then TCMT IO Doc
    "(redacted)" else
                          [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
    prettyTCM Term
    v ]
                        | (Candidate
    _, Term
    v, a
    _) <- [(Candidate, Term, a)]
    cands ] ]
      Relevance
    rel <- MetaVariable -> Relevance
    getMetaRelevance (MetaVariable -> Relevance)
    -> TCMT IO MetaVariable -> TCMT IO Relevance
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    m
      case [(Candidate, Term, a)]
    cands of
        []            -> [(Candidate, Term, a)] -> TCMT IO [(Candidate, Term, a)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [(Candidate, Term, a)]
    cands
        (Candidate, Term, a)
    cvd : [(Candidate, Term, a)]
    _ | 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, a)] -> TCMT IO [(Candidate, Term, a)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [(Candidate, Term, a)
    cvd]
        (Candidate
    _, MetaV MetaId
    m' Elims
    _, a
    _) : [(Candidate, Term, a)]
    _ | MetaId
    m MetaId -> MetaId -> Bool
    forall a. Eq a => a -> a -> Bool
    == MetaId
    m' -> do  -- We didn't instantiate, so can't compare
          [Char] -> Int -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.instance" Int
    30 [Char]
    "dropSameCandidates: Meta was not instantiated so we don't filter equal candidates yet"
          [(Candidate, Term, a)] -> TCMT IO [(Candidate, Term, a)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [(Candidate, Term, a)]
    cands
        cvd :: (Candidate, Term, a)
    cvd@(Candidate
    _, Term
    v, a
    _) : [(Candidate, Term, a)]
    vas
          | Term -> Bool
    freshMetas Term
    v -> do
              [Char] -> Int -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.instance" Int
    30 [Char]
    "dropSameCandidates: Solution of instance meta has fresh metas so we don't filter equal candidates yet"
              [(Candidate, Term, a)] -> TCMT IO [(Candidate, Term, a)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Candidate, Term, a)
    cvd (Candidate, Term, a)
    -> [(Candidate, Term, a)] -> [(Candidate, Term, a)]
    forall a. a -> [a] -> [a]
    : [(Candidate, Term, a)]
    vas)
          | Bool
    otherwise -> ((Candidate, Term, a)
    cvd (Candidate, Term, a)
    -> [(Candidate, Term, a)] -> [(Candidate, Term, a)]
    forall a. a -> [a] -> [a]
    :) ([(Candidate, Term, a)] -> [(Candidate, Term, a)])
    -> TCMT IO [(Candidate, Term, a)] -> TCMT IO [(Candidate, Term, a)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((Candidate, Term, a) -> TCMT IO Bool)
    -> [(Candidate, Term, a)] -> TCMT IO [(Candidate, Term, a)]
    forall (m :: * -> *) a. Monad m => (a -> m Bool) -> [a] -> m [a]
    dropWhileM (Candidate, Term, a) -> TCMT IO Bool
    forall a. (Candidate, Term, a) -> TCMT IO Bool
    equal [(Candidate, Term, a)]
    vas
          where
            equal :: (Candidate, Term, a) -> TCM Bool
            equal :: forall a. (Candidate, Term, a) -> TCMT IO Bool
    equal (Candidate
    _, Term
    v', a
    _)
                | Term -> Bool
    freshMetas Term
    v' = Bool -> TCMT IO Bool
    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] -> TCMT IO Bool -> TCMT IO Bool
    forall (m :: * -> *) a.
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m a -> m a
    verboseBracket [Char]
    "tc.instance" Int
    30 [Char]
    "dropSameCandidates: " (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO 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
    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
    prettyTCM Term
    v' ]
              Type
    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
    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 :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m Type
    getMetaType MetaId
    m TCMT IO (Args -> (Type, Args))
    -> TCMT IO Args -> TCMT IO (Type, Args)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> TCMT IO Args
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
    getContextArgs)
              TCMT IO Bool -> TCMT IO Bool
    forall a. TCM a -> TCM a
    localTCState (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Bool -> TCMT IO Bool
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasOptions m, MonadDebug m) =>
    m a -> m a
    dontAssignMetas (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $ TCMT IO ()
    -> TCMT IO Bool -> (ProblemId -> TCMT IO Bool) -> TCMT IO Bool
    forall a. TCMT IO () -> TCM a -> (ProblemId -> TCM a) -> TCM a
    ifNoConstraints_ (Type -> Term -> Term -> TCMT IO ()
    forall (m :: * -> *).
    MonadConversion m =>
    Type -> Term -> Term -> m ()
    equalTerm Type
    a Term
    v Term
    v')
                                 {- then -} (Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True)
                                 {- else -} (\ ProblemId
    _ -> Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False)
                                 TCMT IO Bool -> (TCErr -> TCMT IO Bool) -> TCMT IO Bool
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` (\ TCErr
    _ -> Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False)

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

    isNo :: YesNoMaybe -> Bool
    isNo :: YesNoMaybe -> Bool
    isNo YesNoMaybe
    No          = Bool
    True
    isNo NoBecause{} = Bool
    True
    isNo HellNo{}    = Bool
    True
    isNo YesNoMaybe
    _           = Bool
    False

    -- | 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]))
    checkCandidates :: MetaId
    -> Type
    -> [Candidate]
    -> TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
    checkCandidates MetaId
    m Type
    t [Candidate]
    cands =
      [Char]
    -> Int
    -> [Char]
    -> TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
    -> TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
    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]))
     -> TCM (Maybe ([(Candidate, TCErr)], [Candidate])))
    -> TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
    -> TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
    forall a b. (a -> b) -> a -> b
    $
      TCMT IO Bool
    -> TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
    -> TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
    -> TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM ([Candidate] -> TCMT IO Bool
    anyMetaTypes [Candidate]
    cands) (Maybe ([(Candidate, TCErr)], [Candidate])
    -> TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe ([(Candidate, TCErr)], [Candidate])
    forall a. Maybe a
    Nothing) (TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
     -> TCM (Maybe ([(Candidate, TCErr)], [Candidate])))
    -> TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
    -> TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
    forall a b. (a -> b) -> a -> b
    $ ([(Candidate, TCErr)], [Candidate])
    -> Maybe ([(Candidate, TCErr)], [Candidate])
    forall a. a -> Maybe a
    Just (([(Candidate, TCErr)], [Candidate])
     -> Maybe ([(Candidate, TCErr)], [Candidate]))
    -> TCM ([(Candidate, TCErr)], [Candidate])
    -> TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
    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
    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 [ TCMT IO Doc
    "-" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (if Bool
    overlap then TCMT IO Doc
    "overlap" else TCMT IO Doc
    forall a. Null a => a
    empty) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Candidate -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Candidate
    c 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
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t
                 | c :: Candidate
    c@(Candidate CandidateKind
    q Term
    v Type
    t Bool
    overlap) <- [Candidate]
    cands ] ]
        ([(Candidate, TCErr)], [Candidate])
    cands' <- MetaId
    -> [Candidate]
    -> (Candidate -> TCM YesNoMaybe)
    -> TCM ([(Candidate, TCErr)], [Candidate])
    filterResetingState MetaId
    m [Candidate]
    cands (MetaId -> Type -> Candidate -> TCM YesNoMaybe
    checkCandidateForMeta MetaId
    m 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
    "valid candidates"
          , [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat [ TCMT IO Doc
    "-" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (if Bool
    overlap then TCMT IO Doc
    "overlap" else TCMT IO Doc
    forall a. Null a => a
    empty) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Candidate -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Candidate
    c 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
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t
                 | c :: Candidate
    c@(Candidate CandidateKind
    q Term
    v Type
    t Bool
    overlap) <- ([(Candidate, TCErr)], [Candidate]) -> [Candidate]
    forall a b. (a, b) -> b
    snd ([(Candidate, TCErr)], [Candidate])
    cands' ] ]
        [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.instance.candidates" Int
    60 (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
    "valid candidates"
          , [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat [ TCMT IO Doc
    "-" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (if Bool
    overlap then TCMT IO Doc
    "overlap" else TCMT IO Doc
    forall a. Null a => a
    empty) 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
    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
    ":" 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
    prettyTCM Type
    t
                 | c :: Candidate
    c@(Candidate CandidateKind
    q Term
    v Type
    t Bool
    overlap) <- ([(Candidate, TCErr)], [Candidate]) -> [Candidate]
    forall a b. (a, b) -> b
    snd ([(Candidate, TCErr)], [Candidate])
    cands' ] ]
        ([(Candidate, TCErr)], [Candidate])
    -> TCM ([(Candidate, TCErr)], [Candidate])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(Candidate, TCErr)], [Candidate])
    cands'
      where
        anyMetaTypes :: [Candidate] -> TCM Bool
        anyMetaTypes :: [Candidate] -> TCMT IO Bool
    anyMetaTypes [] = Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
        anyMetaTypes (Candidate CandidateKind
    _ Term
    _ Type
    a Bool
    _ : [Candidate]
    cands) = do
          Type
    a <- Type -> TCMT IO Type
    forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
    instantiate Type
    a
          case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    a of
            MetaV{} -> Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
            Term
    _       -> [Candidate] -> TCMT IO Bool
    anyMetaTypes [Candidate]
    cands

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

        checkCandidateForMeta :: MetaId -> Type -> Candidate -> TCM YesNoMaybe
        checkCandidateForMeta :: MetaId -> Type -> Candidate -> TCM YesNoMaybe
    checkCandidateForMeta MetaId
    m Type
    t (Candidate CandidateKind
    q Term
    term Type
    t' Bool
    _) = Term -> Type -> TCM YesNoMaybe -> TCM YesNoMaybe
    checkDepth Term
    term Type
    t' (TCM YesNoMaybe -> TCM YesNoMaybe)
    -> TCM YesNoMaybe -> TCM YesNoMaybe
    forall a b. (a -> b) -> a -> b
    $ do
          -- Andreas, 2015-02-07: New metas should be created with range of the
          -- current instance meta, thus, we set the range.
          MetaVariable
    mv <- MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    m
          MetaVariable -> TCM YesNoMaybe -> TCM YesNoMaybe
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange MetaVariable
    mv (TCM YesNoMaybe -> TCM YesNoMaybe)
    -> TCM YesNoMaybe -> TCM YesNoMaybe
    forall a b. (a -> b) -> a -> b
    $ do
            TCMT IO ()
    debugConstraints
            [Char] -> Int -> [Char] -> TCM YesNoMaybe -> TCM YesNoMaybe
    forall (m :: * -> *) a.
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m a -> m a
    verboseBracket [Char]
    "tc.instance" Int
    20 ([Char]
    "checkCandidateForMeta " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ MetaId -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow MetaId
    m) (TCM YesNoMaybe -> TCM YesNoMaybe)
    -> TCM YesNoMaybe -> TCM YesNoMaybe
    forall a b. (a -> b) -> a -> b
    $
              TCM YesNoMaybe -> TCM YesNoMaybe
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM YesNoMaybe -> TCM YesNoMaybe)
    -> TCM YesNoMaybe -> TCM YesNoMaybe
    forall a b. (a -> b) -> a -> b
    $ TCM YesNoMaybe -> TCM YesNoMaybe
    runCandidateCheck (TCM YesNoMaybe -> TCM YesNoMaybe)
    -> TCM YesNoMaybe -> TCM YesNoMaybe
    forall a b. (a -> b) -> a -> b
    $ do
                [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]
    "  t: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Type -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Type
    t [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "\n  t':" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Type -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Type
    t' [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "\n  term: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Term -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Term
    term [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "."
                [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.instance" Int
    20 (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
    "checkCandidateForMeta"
                  , TCMT IO Doc
    "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
    prettyTCM Type
    t
                  , TCMT IO Doc
    "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
    prettyTCM Type
    t'
                  , TCMT IO Doc
    "term =" 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
    prettyTCM Term
    term
                  ]

                -- Apply hidden and instance arguments (recursive inst. search!).
                (Args
    args, Type
    t'') <- Int -> (Hiding -> Bool) -> Type -> TCMT IO (Args, Type)
    forall (m :: * -> *).
    (PureTCM m, MonadMetaSolver m, MonadTCM m) =>
    Int -> (Hiding -> Bool) -> Type -> m (Args, Type)
    implicitArgs (-Int
    1) (\Hiding
    h -> Hiding -> Bool
    forall a. LensHiding a => a -> Bool
    notVisible Hiding
    h) Type
    t'

                [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.instance" Int
    20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
                  TCMT IO Doc
    "instance search: checking" 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
    prettyTCM Type
    t''
                  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
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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" Int
    70 (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: checking (raw)"
                  , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    4 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Type
    t''
                  , 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
    "<="
                  , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    4 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Type
    t
                  ]
                Term
    v <- (Term -> Args -> TCMT IO Term
    `applyDroppingParameters` Args
    args) (Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Term -> TCMT IO Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Term
    term
                [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
    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
    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
                -- if constraints remain, we abort, but keep the candidate
                -- Jesper, 05-12-2014: When we abort, we should add a constraint to
                -- instantiate the meta at a later time (see issue 1377).
                Elims
    ctxElims <- (Arg Term -> Elim' Term) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (Args -> Elims) -> TCMT IO Args -> TCMT IO Elims
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Args
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
    getContextArgs
                Constraint -> TCMT IO () -> TCMT IO ()
    guardConstraint (Comparison -> CompareAs -> Term -> Term -> Constraint
    ValueCmp Comparison
    CmpEq (Type -> CompareAs
    AsTermsOf Type
    t'') (MetaId -> Elims -> Term
    MetaV MetaId
    m Elims
    ctxElims) Term
    v) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Type -> Type -> TCMT IO ()
    forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
    leqType Type
    t'' Type
    t
                -- make a pass over constraints, to detect cases where some are made
                -- unsolvable by the assignment, but don't do this for FindInstance's
                -- to prevent loops.
                TCMT IO ()
    debugConstraints

                let debugSolution :: TCMT IO ()
    debugSolution = [Char] -> Int -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
    verboseS [Char]
    "tc.instance" Int
    15 (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ do
                      Term
    sol <- Term -> TCMT IO Term
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull (MetaId -> Elims -> Term
    MetaV MetaId
    m Elims
    ctxElims)
                      case Term
    sol of
                        MetaV MetaId
    m' Elims
    _ | MetaId
    m MetaId -> MetaId -> Bool
    forall a. Eq a => a -> a -> Bool
    == MetaId
    m' ->
                          [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
    sep [ (TCMT IO Doc
    "instance search: maybe solution for" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> MetaId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM MetaId
    m) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall a. Semigroup a => a -> a -> a
    <> 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
    prettyTCM Term
    v ]
                        Term
    _ ->
                          [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
    sep [ (TCMT IO Doc
    "instance search: found solution for" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> MetaId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM MetaId
    m) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall a. Semigroup a => a -> a -> a
    <> 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
    prettyTCM Term
    sol ]

                do Bool -> TCMT IO ()
    forall (m :: * -> *). MonadConstraint m => Bool -> m ()
    solveAwakeConstraints' Bool
    True
                   YesNoMaybe
    Yes YesNoMaybe -> TCMT IO () -> TCM YesNoMaybe
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ TCMT IO ()
    debugSolution
                  TCM YesNoMaybe -> (TCErr -> TCM YesNoMaybe) -> TCM YesNoMaybe
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` (YesNoMaybe -> TCM YesNoMaybe
    forall (m :: * -> *) a. Monad m => a -> m a
    return (YesNoMaybe -> TCM YesNoMaybe)
    -> (TCErr -> YesNoMaybe) -> TCErr -> TCM YesNoMaybe
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCErr -> YesNoMaybe
    NoBecause)

            where
              runCandidateCheck :: TCM YesNoMaybe -> TCM YesNoMaybe
    runCandidateCheck TCM YesNoMaybe
    check =
                (TCM YesNoMaybe -> (TCErr -> TCM YesNoMaybe) -> TCM YesNoMaybe)
    -> (TCErr -> TCM YesNoMaybe) -> TCM YesNoMaybe -> TCM YesNoMaybe
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip TCM YesNoMaybe -> (TCErr -> TCM YesNoMaybe) -> TCM YesNoMaybe
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    catchError TCErr -> TCM YesNoMaybe
    handle (TCM YesNoMaybe -> TCM YesNoMaybe)
    -> TCM YesNoMaybe -> TCM YesNoMaybe
    forall a b. (a -> b) -> a -> b
    $
                TCM YesNoMaybe -> TCM YesNoMaybe
    forall (m :: * -> *) a. ReadTCState m => m a -> m a
    nowConsideringInstance (TCM YesNoMaybe -> TCM YesNoMaybe)
    -> TCM YesNoMaybe -> TCM YesNoMaybe
    forall a b. (a -> b) -> a -> b
    $
                TCM YesNoMaybe
    -> (YesNoMaybe -> TCM YesNoMaybe)
    -> (ProblemId -> YesNoMaybe -> TCM YesNoMaybe)
    -> TCM YesNoMaybe
    forall a b.
    TCM a -> (a -> TCM b) -> (ProblemId -> a -> TCM b) -> TCM b
    ifNoConstraints TCM YesNoMaybe
    check
                  (\ YesNoMaybe
    r -> case YesNoMaybe
    r of
                      YesNoMaybe
    Yes           -> YesNoMaybe
    r YesNoMaybe -> TCMT IO () -> TCM YesNoMaybe
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ TCMT IO ()
    debugSuccess
                      NoBecause TCErr
    why -> YesNoMaybe
    r YesNoMaybe -> TCMT IO () -> TCM YesNoMaybe
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ TCErr -> TCMT IO ()
    forall {m :: * -> *} {a}. (MonadDebug m, PrettyTCM a) => a -> m ()
    debugConstraintFail TCErr
    why
                      YesNoMaybe
    _             -> TCM YesNoMaybe
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                  )
                  (\ ProblemId
    _ YesNoMaybe
    r -> case YesNoMaybe
    r of
                      YesNoMaybe
    Yes           -> YesNoMaybe
    Maybe YesNoMaybe -> TCMT IO () -> TCM YesNoMaybe
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ TCMT IO ()
    debugInconclusive
                      NoBecause TCErr
    why -> YesNoMaybe
    r YesNoMaybe -> TCMT IO () -> TCM YesNoMaybe
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ TCErr -> TCMT IO ()
    forall {m :: * -> *} {a}. (MonadDebug m, PrettyTCM a) => a -> m ()
    debugConstraintFail TCErr
    why
                      YesNoMaybe
    _             -> TCM YesNoMaybe
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                  )

              debugSuccess :: TCMT IO ()
    debugSuccess            = [Char] -> Int -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.instance" Int
    50 [Char]
    "assignment successful" :: TCM ()
              debugInconclusive :: TCMT IO ()
    debugInconclusive       = [Char] -> Int -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.instance" Int
    50 [Char]
    "assignment inconclusive" :: TCM ()
              debugConstraintFail :: a -> m ()
    debugConstraintFail a
    why = [Char] -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.instance" Int
    50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "candidate failed constraints:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> a -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM a
    why
              debugTypeFail :: a -> m ()
    debugTypeFail a
    err       = [Char] -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.instance" Int
    50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    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
    <+> a -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM a
    err

              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 YesNoMaybe
              handle :: TCErr -> TCM YesNoMaybe
    handle TCErr
    err
                | TCErr -> Bool
    hardFailure TCErr
    err = YesNoMaybe -> TCM YesNoMaybe
    forall (m :: * -> *) a. Monad m => a -> m a
    return (YesNoMaybe -> TCM YesNoMaybe) -> YesNoMaybe -> TCM YesNoMaybe
    forall a b. (a -> b) -> a -> b
    $ TCErr -> YesNoMaybe
    HellNo TCErr
    err
                | Bool
    otherwise       = YesNoMaybe
    No YesNoMaybe -> TCMT IO () -> TCM YesNoMaybe
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ TCErr -> TCMT IO ()
    forall {m :: * -> *} {a}. (MonadDebug m, PrettyTCM a) => a -> m ()
    debugTypeFail TCErr
    err

    isInstanceConstraint :: Constraint -> Bool
    isInstanceConstraint :: Constraint -> Bool
    isInstanceConstraint FindInstance{} = Bool
    True
    isInstanceConstraint Constraint
    _              = Bool
    False

    shouldPostponeInstanceSearch :: (ReadTCState m, HasOptions m) => m Bool
    shouldPostponeInstanceSearch :: forall (m :: * -> *). (ReadTCState m, HasOptions m) => m Bool
    shouldPostponeInstanceSearch =
      m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    and2M ((TCState -> Lens' Bool TCState -> Bool
    forall o i. o -> Lens' i o -> i
    ^. Lens' Bool TCState
    stConsideringInstance) (TCState -> Bool) -> m TCState -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m TCState
    forall (m :: * -> *). ReadTCState m => m TCState
    getTCState)
            (Bool -> Bool
    not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optOverlappingInstances (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions)
      m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `or2M` ((TCState -> Lens' Bool TCState -> Bool
    forall o i. o -> Lens' i o -> i
    ^. Lens' Bool TCState
    stPostponeInstanceSearch) (TCState -> Bool) -> m TCState -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m TCState
    forall (m :: * -> *). ReadTCState m => m TCState
    getTCState)

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

    isInstanceProblemConstraint :: ProblemConstraint -> Bool
    isInstanceProblemConstraint :: ProblemConstraint -> Bool
    isInstanceProblemConstraint = Constraint -> Bool
    isInstanceConstraint (Constraint -> Bool)
    -> (ProblemConstraint -> Constraint) -> ProblemConstraint -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Closure Constraint -> Constraint
    forall a. Closure a -> a
    clValue (Closure Constraint -> Constraint)
    -> (ProblemConstraint -> Closure Constraint)
    -> ProblemConstraint
    -> Constraint
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ProblemConstraint -> Closure Constraint
    theConstraint

    wakeupInstanceConstraints :: TCM ()
    wakeupInstanceConstraints :: TCMT IO ()
    wakeupInstanceConstraints =
      TCMT IO Bool -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM TCMT IO 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)
        (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' Bool TCState -> (Bool -> Bool) -> TCM a -> TCM a
    forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' a TCState -> (a -> a) -> m b -> m b
    locallyTCState Lens' Bool TCState
    stPostponeInstanceSearch (Bool -> Bool -> Bool
    forall a b. a -> b -> a
    const Bool
    True) TCM a
    m TCM a -> TCMT IO () -> TCM a
    forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
    <* 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.
    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 (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
          Defn
    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 Defn
    def of
            Constructor {conPars :: Defn -> Int
    conPars = Int
    n} -> Term -> TCMT IO Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci ((Arg Term -> Elim' Term) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (Args -> Elims) -> Args -> Elims
    forall a b. (a -> b) -> a -> b
    $ Int -> Args -> Args
    forall a. Int -> [a] -> [a]
    drop Int
    n Args
    vs)
            Defn
    _ -> TCMT IO Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Def QName
    f [] -> do
          -- Andreas, 2022-03-07, issue #5809: don't drop parameters of irrelevant projections.
          Maybe Projection
    mp <- QName -> TCMT IO (Maybe Projection)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe Projection)
    isRelevantProjection QName
    f
          case Maybe Projection
    mp of
            Just Projection{projIndex :: Projection -> Int
    projIndex = Int
    n} -> do
              case Int -> Args -> Args
    forall a. Int -> [a] -> [a]
    drop Int
    n Args
    vs of
                []     -> Term -> TCMT IO Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    t
                Arg Term
    u : Args
    us -> (Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` Args
    us) (Term -> Term) -> TCMT IO Term -> TCMT IO Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ProjOrigin -> QName -> Arg Term -> TCMT IO Term
    forall (m :: * -> *).
    HasConstInfo m =>
    ProjOrigin -> QName -> Arg Term -> m Term
    applyDef ProjOrigin
    ProjPrefix QName
    f Arg Term
    u
            Maybe Projection
    _ -> TCMT IO Term
    fallback
        Term
    _ -> TCMT IO Term
    fallback