    {-# LANGUAGE CPP #-}
    {-# LANGUAGE NondecreasingIndentation #-}

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

    #if MIN_VERSION_base(4,11,0)
    import Prelude hiding ((<>))
    #endif

    import Control.Applicative hiding (empty)
    import Control.Monad.Reader
    import Control.Monad.State
    import qualified Data.IntSet as IntSet
    import qualified Data.Map as Map
    import qualified Data.Set as Set
    import qualified Data.List as List
    import Data.Function (on)
    import Data.Monoid hiding ((<>))

    import Agda.Interaction.Options (optOverlappingInstances)

    import Agda.Syntax.Common
    import Agda.Syntax.Position
    import Agda.Syntax.Internal as I
    import Agda.Syntax.Scope.Base (isNameInScope)

    import Agda.TypeChecking.Errors ()
    import Agda.TypeChecking.Implicit (implicitArgs)
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Monad.Builtin
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Records
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Free

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

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

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

    #include "undefined.h"
    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 (Maybe [Candidate])
    initialInstanceCandidates t = do
      (_ , otn) <- getOutputTypeName t
      case otn of
        NoOutputTypeName -> typeError $ GenericError $
          "Instance search can only be used to find elements in a named type"
        OutputTypeNameNotYetKnown -> do
          reportSDoc "tc.instance.cands" 30 $ "Instance type is not yet known. "
          return Nothing
        OutputTypeVisiblePi -> typeError $ GenericError $
          "Instance search cannot be used to find elements in an explicit function type"
        OutputTypeVar    -> do
          reportSDoc "tc.instance.cands" 30 $ "Instance type is a variable. "
          maybeRight <$> runExceptT getContextVars
        OutputTypeName n -> do
          reportSDoc "tc.instance.cands" 30 $ "Found instance type head: " <+> prettyTCM n
          runExceptT getContextVars >>= \case
            Left b -> return Nothing
            Right ctxVars -> Just . (ctxVars ++) <$> getScopeDefs n
      where
        -- get a list of variables with their type, relative to current context
        getContextVars :: ExceptT Blocked_ TCM [Candidate]
        getContextVars = do
          ctx <- getContext
          reportSDoc "tc.instance.cands" 40 $ hang "Getting candidates from context" 2 (inTopContext $ prettyTCM $ PrettyContext ctx)
              -- Context variables with their types lifted to live in the full context
          let varsAndRaisedTypes = [ (var i, raise (i + 1) t) | (i, t) <- zip [0..] ctx ]
              vars = [ Candidate x t (isOverlappable info)
                     | (x, Dom{domInfo = info, unDom = (_, t)}) <- varsAndRaisedTypes
                     , isInstance info
                     , usableRelevance info
                     , usableQuantity info
                     ]

          -- {{}}-fields of variables are also candidates
          let cxtAndTypes = [ (x, t) | (x, Dom{unDom = (_, t)}) <- varsAndRaisedTypes ]
          fields <- concat <$> mapM instanceFields (reverse cxtAndTypes)
          reportSDoc "tc.instance.fields" 30 $
            if null fields then "no instance field candidates" else
              "instance field candidates" $$ do
                nest 2 $ vcat
                  [ sep [ (if overlap then "overlap" else empty) <+> prettyTCM v <+> ":"
                        , nest 2 $ prettyTCM t
                        ]
                  | Candidate v t overlap <- fields
                  ]

          -- get let bindings
          env <- asksTC envLetBindings
          env <- mapM (getOpen . snd) $ Map.toList env
          let lets = [ Candidate v t False
                     | (v, Dom{domInfo = info, unDom = t}) <- env
                     , isInstance info
                     , usableRelevance info
                     , usableQuantity info
                     ]
          return $ vars ++ fields ++ lets

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

        instanceFields :: (Term,Type) -> ExceptT Blocked_ TCM [Candidate]
        instanceFields = instanceFields' True

        instanceFields' :: Bool -> (Term,Type) -> ExceptT Blocked_ TCM [Candidate]
        instanceFields' etaOnce (v, t) =
          ifBlockedType t (\m _ -> throwError $ Blocked m ()) $ \ _ t -> do
          caseMaybeM (etaExpand etaOnce t) (return []) $ \ (r, pars) -> do
            (tel, args) <- forceEtaExpandRecord r pars v
            let types = map unDom $ applySubst (parallelS $ reverse $ map unArg args) (flattenTel tel)
            fmap concat $ forM (zip args types) $ \ (arg, t) ->
              ([ Candidate (unArg arg) t (isOverlappable arg)
               | isInstance arg ] ++) <$>
              instanceFields' False (unArg arg, t)

        getScopeDefs :: QName -> TCM [Candidate]
        getScopeDefs n = do
          instanceDefs <- getInstanceDefs
          rel          <- asksTC envRelevance
          let qs = maybe [] Set.toList $ Map.lookup n instanceDefs
          catMaybes <$> mapM (candidate rel) qs

        candidate :: Relevance -> QName -> TCM (Maybe Candidate)
        candidate rel q = ifNotM (isNameInScope q <$> getScope) (return Nothing) $ 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)
          flip catchError handle $ do
            def <- getConstInfo q
            if not (defRelevance def `moreRelevant` rel) then return Nothing else do
              -- Andreas, 2017-01-14: instantiateDef is a bit of an overkill
              -- if we anyway get the freeVarsToApply
              -- WAS: t <- defType <$> instantiateDef def
              args <- freeVarsToApply q
              let t = defType def `piApply` args
              let v = case theDef def of
                   -- drop parameters if it's a projection function...
                   Function{ funProjection = Just p } -> projDropParsApply p ProjSystem 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 = c }       -> Con c ConOSystem []
                   _                                  -> Def q $ map Apply args
              return $ Just $ Candidate v t False
          where
            -- unbound constant throws an internal error
            handle (TypeError _ (Closure {clValue = InternalError _})) = return Nothing
            handle err                                                 = throwError err

    -- | @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 m Nothing = do
      -- Andreas, 2015-02-07: New metas should be created with range of the
      -- current instance meta, thus, we set the range.
      mv <- lookupMeta m
      setCurrentRange mv $ do
        reportSLn "tc.instance" 20 $ "The type of the FindInstance constraint isn't known, trying to find it again."
        t <- instantiate =<< getMetaTypeInContext m
        reportSLn "tc.instance" 70 $ "findInstance 1: t: " ++ prettyShow t

        -- Issue #2577: If the target is a function type the arguments are
        -- potential candidates, so we add them to the context to make
        -- initialInstanceCandidates pick them up.
        TelV tel t <- telViewUpTo' (-1) notVisible t
        cands <- addContext tel $ initialInstanceCandidates t
        case cands of
          Nothing -> do
            reportSLn "tc.instance" 20 "Can't figure out target of instance goal. Postponing constraint."
            addConstraint $ FindInstance m Nothing Nothing
          Just {} -> findInstance m cands

    findInstance m (Just cands) =
      whenJustM (findInstance' m cands) $ (\ (cands, b) -> addConstraint $ FindInstance m b $ Just 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], Maybe MetaId))
    findInstance' m cands = ifM (isFrozen m) (do
        reportSLn "tc.instance" 20 "Refusing to solve frozen instance meta."
        return (Just (cands, Nothing))) $ do
      ifM isConsideringInstance (do
        reportSLn "tc.instance" 20 "Postponing possibly recursive instance search."
        return $ Just (cands, Nothing)) $ billTo [Benchmark.Typing, Benchmark.InstanceSearch] $ do
      -- Andreas, 2015-02-07: New metas should be created with range of the
      -- current instance meta, thus, we set the range.
      mv <- lookupMeta m
      setCurrentRange mv $ do
          reportSLn "tc.instance" 15 $
            "findInstance 2: constraint: " ++ prettyShow m ++ "; candidates left: " ++ show (length cands)
          reportSDoc "tc.instance" 60 $ nest 2 $ vcat
            [ sep [ (if overlap then "overlap" else empty) <+> prettyTCM v <+> ":"
                  , nest 2 $ prettyTCM t ] | Candidate v t overlap <- cands ]
          reportSDoc "tc.instance" 70 $ "raw" $$ do
           nest 2 $ vcat
            [ sep [ (if overlap then "overlap" else empty) <+> pretty v <+> ":"
                  , nest 2 $ pretty t ] | Candidate v t overlap <- cands ]
          t <- normalise =<< getMetaTypeInContext m
          reportSLn "tc.instance" 70 $ "findInstance 2: t: " ++ prettyShow t
          insidePi t $ \ t -> do
          reportSDoc "tc.instance" 15 $ "findInstance 3: t =" <+> prettyTCM t
          reportSLn "tc.instance" 70 $ "findInstance 3: t: " ++ prettyShow t

          mcands <- checkCandidates m t cands
          debugConstraints
          case mcands of

            Just ([(_, err)], []) -> do
              reportSDoc "tc.instance" 15 $
                "findInstance 5: the only viable candidate failed..."
              throwError err
            Just (errs, []) -> do
              if null errs then reportSDoc "tc.instance" 15 $ "findInstance 5: no viable candidate found..."
                           else reportSDoc "tc.instance" 15 $ "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 = List.sortBy (compare `on` precision) errs
                    where precision (_, err) = maybe infinity iLength $ rangeToInterval $ getRange err
                          infinity = 1000000000
              setCurrentRange (take 1 $ map snd sortedErrs) $
                typeError $ InstanceNoCandidate t [ (candidateTerm c, err) | (c, err) <- sortedErrs ]

            Just (_, [Candidate term t' _]) -> do
              reportSDoc "tc.instance" 15 $ vcat
                [ "findInstance 5: solved by instance search using the only candidate"
                , nest 2 $ prettyTCM term
                , "of type " <+> prettyTCM t'
                , "for type" <+> prettyTCM t
                ]

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

            _ -> do
              let cs = maybe cands snd mcands -- keep the current candidates if Nothing
              reportSDoc "tc.instance" 15 $
                text ("findInstance 5: refined candidates: ") <+>
                prettyTCM (List.map candidateTerm cs)
              return (Just (cs, Nothing))

    -- | Precondition: type is spine reduced and ends in a Def or a Var.
    insidePi :: Type -> (Type -> TCM a) -> TCM a
    insidePi t ret =
      case unEl t of
        Pi a b     -> addContext (absName b, a) $ insidePi (absBody b) ret
        Def{}      -> ret t
        Var{}      -> ret t
        Sort{}     -> __IMPOSSIBLE__
        Con{}      -> __IMPOSSIBLE__
        Lam{}      -> __IMPOSSIBLE__
        Lit{}      -> __IMPOSSIBLE__
        Level{}    -> __IMPOSSIBLE__
        MetaV{}    -> __IMPOSSIBLE__
        DontCare{} -> __IMPOSSIBLE__
        Dummy s    -> __IMPOSSIBLE_VERBOSE__ 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 m cands f = do
      ctxArgs  <- getContextArgs
      let ctxElims = map Apply ctxArgs
          tryC c = do
            ok <- f c
            v  <- instantiateFull (MetaV m ctxElims)
            a  <- instantiateFull =<< (`piApplyM` ctxArgs) =<< getMetaType m
            return (ok, v, a)
      result <- mapM (\c -> do bs <- localTCStateSaving (tryC c); return (c, bs)) cands

      -- Check that there aren't any hard failures
      case [ err | (_, ((HellNo err, _, _), _)) <- result ] of
        err : _ -> throwError err
        []      -> return ()

      let result' = [ (c, v, a, s) | (c, ((r, v, a), s)) <- result, not (isNo r) ]
      result'' <- dropSameCandidates m result'
      case result'' of
        [(c, _, _, s)] -> ([], [c]) <$ putTC s
        _              -> do
          let bad  = [ (c, err) | (c, ((NoBecause err, _, _), _)) <- result ]
              good = [ c | (c, _, _, _) <- result'' ]
          return (bad, 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, Type, a)] -> TCM [(Candidate, Term, Type, a)]
    dropSameCandidates m cands0 = verboseBracket "tc.instance" 30 "dropSameCandidates" $ do
      metas <- getMetaVariableSet
      -- Does `it` have any metas in the initial meta variable store?
      let freshMetas = getAny . allMetas (Any . (`IntSet.notMember` metas) . metaId)

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

      reportSDoc "tc.instance" 50 $ vcat
        [ "valid candidates:"
        , nest 2 $ vcat [ if freshMetas (v, a) then "(redacted)" else
                          sep [ prettyTCM v <+> ":", nest 2 $ prettyTCM a ]
                        | (_, v, a, _) <- cands ] ]
      rel <- getMetaRelevance <$> lookupMeta m
      case cands of
        []            -> return cands
        cvd : _ | isIrrelevant rel -> do
          reportSLn "tc.instance" 30 "Meta is irrelevant so any candidate will do."
          return [cvd]
        (_, MetaV m' _, _, _) : _ | m == m' ->  -- We didn't instantiate, so can't compare
          return cands
        cvd@(_, v, a, _) : vas -> do
            if freshMetas (v, a)
              then return (cvd : vas)
              else (cvd :) <$> dropWhileM equal vas
          where
            equal (_, v', a', _)
                | freshMetas (v', a') = return False  -- If there are fresh metas we can't compare
                | otherwise           =
              verboseBracket "tc.instance" 30 "comparingCandidates" $ do
              reportSDoc "tc.instance" 30 $ sep [ prettyTCM v <+> "==", nest 2 $ prettyTCM v' ]
              localTCState $ dontAssignMetas $ ifNoConstraints_ (equalType a a' >> equalTerm a v v')
                                 {- then -} (return True)
                                 {- else -} (\ _ -> return False)
                                 `catchError` (\ _ -> return False)

    data YesNoMaybe = Yes | No | NoBecause TCErr | Maybe | HellNo TCErr
      deriving (Show)

    isNo :: YesNoMaybe -> Bool
    isNo No          = True
    isNo NoBecause{} = True
    isNo HellNo{}    = True
    isNo _           = 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 m t cands =
      verboseBracket "tc.instance.candidates" 20 ("checkCandidates " ++ prettyShow m) $
      ifM (anyMetaTypes cands) (return Nothing) $ Just <$> do
        reportSDoc "tc.instance.candidates" 20 $ nest 2 $ "target:" <+> prettyTCM t
        reportSDoc "tc.instance.candidates" 20 $ nest 2 $ vcat
          [ "candidates"
          , vcat [ "-" <+> (if overlap then "overlap" else empty) <+> prettyTCM v <+> ":" <+> prettyTCM t
                 | Candidate v t overlap <- cands ] ]
        cands' <- filterResetingState m cands (checkCandidateForMeta m t)
        reportSDoc "tc.instance.candidates" 20 $ nest 2 $ vcat
          [ "valid candidates"
          , vcat [ "-" <+> (if overlap then "overlap" else empty) <+> prettyTCM v <+> ":" <+> prettyTCM t
                 | Candidate v t overlap <- snd cands' ] ]
        return cands'
      where
        anyMetaTypes :: [Candidate] -> TCM Bool
        anyMetaTypes [] = return False
        anyMetaTypes (Candidate _ a _ : cands) = do
          a <- instantiate a
          case unEl a of
            MetaV{} -> return True
            _       -> anyMetaTypes cands

        checkDepth :: Term -> Type -> TCM YesNoMaybe -> TCM YesNoMaybe
        checkDepth c a k = locallyTC eInstanceDepth succ $ do
          d        <- viewTC eInstanceDepth
          maxDepth <- maxInstanceSearchDepth
          when (d > maxDepth) $ typeError $ InstanceSearchDepthExhausted c a maxDepth
          k

        checkCandidateForMeta :: MetaId -> Type -> Candidate -> TCM YesNoMaybe
        checkCandidateForMeta m t (Candidate term t' _) = checkDepth term t' $ do
          -- Andreas, 2015-02-07: New metas should be created with range of the
          -- current instance meta, thus, we set the range.
          mv <- lookupMeta m
          setCurrentRange mv $ do
            debugConstraints
            verboseBracket "tc.instance" 20 ("checkCandidateForMeta " ++ prettyShow m) $
              liftTCM $ runCandidateCheck $ do
                reportSLn "tc.instance" 70 $ "  t: " ++ prettyShow t ++ "\n  t':" ++ prettyShow t' ++ "\n  term: " ++ prettyShow term ++ "."
                reportSDoc "tc.instance" 20 $ vcat
                  [ "checkCandidateForMeta"
                  , "t    =" <+> prettyTCM t
                  , "t'   =" <+> prettyTCM t'
                  , "term =" <+> prettyTCM term
                  ]

                -- Apply hidden and instance arguments (recursive inst. search!).
                (args, t'') <- implicitArgs (-1) (\h -> notVisible h) t'

                reportSDoc "tc.instance" 20 $
                  "instance search: checking" <+> prettyTCM t''
                  <+> "<=" <+> prettyTCM t
                reportSDoc "tc.instance" 70 $ vcat
                  [ "instance search: checking (raw)"
                  , nest 4 $ pretty t''
                  , nest 2 $ "<="
                  , nest 4 $ pretty t
                  ]
                v <- (`applyDroppingParameters` args) =<< reduce term
                reportSDoc "tc.instance" 15 $ vcat
                  [ "instance search: attempting"
                  , nest 2 $ prettyTCM m <+> ":=" <+> prettyTCM v
                  ]
                reportSDoc "tc.instance" 70 $ nest 2 $
                  "candidate v = " <+> pretty 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).
                ctxElims <- map Apply <$> getContextArgs
                guardConstraint (ValueCmp CmpEq t'' (MetaV m ctxElims) v) $ leqType t'' 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.
                debugConstraints

                let debugSolution = verboseS "tc.instance" 15 $ do
                      sol <- instantiateFull (MetaV m ctxElims)
                      case sol of
                        MetaV m' _ | m == m' ->
                          reportSDoc "tc.instance" 15 $
                            sep [ "instance search: maybe solution for" <+> prettyTCM m <> ":"
                                , nest 2 $ prettyTCM v ]
                        _ ->
                          reportSDoc "tc.instance" 15 $
                            sep [ "instance search: found solution for" <+> prettyTCM m <> ":"
                                , nest 2 $ prettyTCM sol ]

                do solveAwakeConstraints' True
                   Yes <$ debugSolution
                  `catchError` (return . NoBecause)

            where
              runCandidateCheck check =
                flip catchError handle $
                nowConsideringInstance $
                ifNoConstraints check
                  (\ r -> case r of
                      Yes           -> r <$ debugSuccess
                      NoBecause why -> r <$ debugConstraintFail why
                      _             -> __IMPOSSIBLE__
                  )
                  (\ _ r -> case r of
                      Yes           -> Maybe <$ debugInconclusive
                      NoBecause why -> r <$ debugConstraintFail why
                      _             -> __IMPOSSIBLE__
                  )

              debugSuccess            = reportSLn "tc.instance" 50 "assignment successful" :: TCM ()
              debugInconclusive       = reportSLn "tc.instance" 50 "assignment inconclusive" :: TCM ()
              debugConstraintFail why = reportSDoc "tc.instance" 50 $ "candidate failed constraints:" <+> prettyTCM why
              debugTypeFail err       = reportSDoc "tc.instance" 50 $ "candidate failed type check:" <+> prettyTCM err

              hardFailure :: TCErr -> Bool
              hardFailure (TypeError _ err) =
                case clValue err of
                  InstanceSearchDepthExhausted{} -> True
                  _                              -> False
              hardFailure _ = False

              handle :: TCErr -> TCM YesNoMaybe
              handle err
                | hardFailure err = return $ HellNo err
                | otherwise       = No <$ debugTypeFail err

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

    isConsideringInstance :: (ReadTCState m, HasOptions m) => m Bool
    isConsideringInstance =
      and2M ((^. stConsideringInstance) <$> getTCState)
            (not . optOverlappingInstances <$> pragmaOptions)

    nowConsideringInstance :: (MonadTCState m) => m a -> m a
    nowConsideringInstance = locallyTCState stConsideringInstance $ const True

    wakeupInstanceConstraints :: TCM ()
    wakeupInstanceConstraints =
      unlessM isConsideringInstance $ do
        wakeConstraints (return . isInstance)
        solveSomeAwakeConstraints isInstance False
      where
        isInstance = isInstanceConstraint . clValue . theConstraint

    postponeInstanceConstraints :: TCM a -> TCM a
    postponeInstanceConstraints m =
      nowConsideringInstance m <* 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 t vs = do
      let fallback = return $ t `apply` vs
      case t of
        Con c ci [] -> do
          def <- theDef <$> getConInfo c
          case def of
            Constructor {conPars = n} -> return $ Con c ci (map Apply $ drop n vs)
            _ -> __IMPOSSIBLE__
        Def f [] -> do
          mp <- isProjection f
          case mp of
            Just Projection{projIndex = n} -> do
              case drop n vs of
                []     -> return t
                u : us -> (`apply` us) <$> applyDef ProjPrefix f u
            _ -> fallback
        _ -> fallback