{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation #-}

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

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

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

import Agda.Interaction.Options (optQualifiedInstances)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

      mutual <- caseMaybeM (asksTC envMutualBlock) (pure mempty) \MutualId
mb ->
        MutualBlock -> Set QName
mutualNames (MutualBlock -> Set QName)
-> BlockT (TCMT IO) MutualBlock -> BlockT (TCMT IO) (Set QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MutualId -> BlockT (TCMT IO) MutualBlock
forall (tcm :: * -> *).
ReadTCState tcm =>
MutualId -> tcm MutualBlock
lookupMutualBlock MutualId
mb

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

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

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

      pure cands

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

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

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

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

          return $ Just $ Candidate (GlobalCandidate q) v t mode
      where
        -- unbound constant throws an internal error
        handle :: TCErr -> m (Maybe a)
handle (TypeError CallStack
_ TCState
_ (Closure {clValue :: forall a. Closure a -> a
clValue = InternalError [Char]
_})) = Maybe a -> m (Maybe a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
        handle TCErr
err                                                   = TCErr -> m (Maybe a)
forall a. TCErr -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err

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


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

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

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

  insertCandidate :: Candidate -> [Candidate] -> TCM [Candidate]
  insertCandidate :: Candidate -> [Candidate] -> TCM [Candidate]
insertCandidate Candidate
x []     = [Candidate] -> TCM [Candidate]
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Candidate
x]
  insertCandidate Candidate
x (Candidate
y:[Candidate]
xs) = Candidate -> Candidate -> TCMT IO Bool
doesCandidateSpecialise Candidate
x Candidate
y TCMT IO Bool -> (Bool -> TCM [Candidate]) -> TCM [Candidate]
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Bool
True  -> [Candidate] -> TCM [Candidate]
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Candidate
xCandidate -> [Candidate] -> [Candidate]
forall a. a -> [a] -> [a]
:Candidate
yCandidate -> [Candidate] -> [Candidate]
forall a. a -> [a] -> [a]
:[Candidate]
xs)
    Bool
False -> (Candidate
yCandidate -> [Candidate] -> [Candidate]
forall a. a -> [a] -> [a]
:) ([Candidate] -> [Candidate]) -> TCM [Candidate] -> TCM [Candidate]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Candidate -> [Candidate] -> TCM [Candidate]
insertCandidate Candidate
x [Candidate]
xs

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

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

    pure cands

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

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

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

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

  TelV tel t1 <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t1
  addContext tel $ wrap $ do
    (args, t2) <- implicitArgs (-1) (\Hiding
h -> Hiding -> Bool
forall a. LensHiding a => a -> Bool
notVisible Hiding
h) t2

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

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

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

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

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

  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 :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
m) TCMT IO (Maybe ([Candidate], Blocker))
frozen 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 TCMT IO (Maybe ([Candidate], Blocker))
recursive do
  Account (BenchPhase (TCMT IO))
-> TCMT IO (Maybe ([Candidate], Blocker))
-> TCMT IO (Maybe ([Candidate], Blocker))
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
billTo [BenchPhase (TCMT IO)
Phase
Benchmark.Typing, BenchPhase (TCMT IO)
Phase
Benchmark.InstanceSearch] do

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.overlap" Int
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"comparing new candidate"
      , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (Candidate -> TCMT IO Doc
forall (m :: * -> *). MonadPretty m => Candidate -> m Doc
debugCandidate Candidate
new)
      , TCMT IO Doc
"versus old candidate"
      , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (Candidate -> TCMT IO Doc
forall (m :: * -> *). MonadPretty m => Candidate -> m Doc
debugCandidate Candidate
old)
      ]

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

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

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

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

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

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

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

    if guarded then pure oldState else insertNew oldState newItem oldItems

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

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

  rel <- getRelevance <$> lookupMetaModality m

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

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

  case cands of
    [] -> [(Candidate, Term, TCState)] -> TCM [(Candidate, Term, TCState)]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Candidate, Term, TCState)]
cands
    (Candidate, Term, TCState)
cvd : [(Candidate, Term, TCState)]
_ | Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
rel -> do
      [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.instance" Int
30 [Char]
"dropSameCandidates: Meta is irrelevant so any candidate will do."
      [(Candidate, Term, TCState)] -> TCM [(Candidate, Term, TCState)]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Candidate, Term, TCState)
cvd]
    cvd :: (Candidate, Term, TCState)
cvd@(Candidate
_, Term
v, TCState
_) : [(Candidate, Term, TCState)]
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, TCState)] -> TCM [(Candidate, Term, TCState)]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Candidate, Term, TCState)
cvd (Candidate, Term, TCState)
-> [(Candidate, Term, TCState)] -> [(Candidate, Term, TCState)]
forall a. a -> [a] -> [a]
: [(Candidate, Term, TCState)]
vas)
      | Bool
otherwise -> ((Candidate, Term, TCState)
cvd (Candidate, Term, TCState)
-> [(Candidate, Term, TCState)] -> [(Candidate, Term, TCState)]
forall a. a -> [a] -> [a]
:) ([(Candidate, Term, TCState)] -> [(Candidate, Term, TCState)])
-> TCM [(Candidate, Term, TCState)]
-> TCM [(Candidate, Term, TCState)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Candidate, Term, TCState) -> TCMT IO Bool)
-> [(Candidate, Term, TCState)] -> TCM [(Candidate, Term, TCState)]
forall (m :: * -> *) a. Monad m => (a -> m Bool) -> [a] -> m [a]
dropWhileM (Candidate, Term, TCState) -> TCMT IO Bool
forall a. (Candidate, Term, a) -> TCMT IO Bool
equal [(Candidate, Term, TCState)]
vas
      where
        equal :: (Candidate, Term, a) -> TCM Bool
        equal :: forall a. (Candidate, Term, a) -> TCMT IO Bool
equal (Candidate
c, Term
v', a
_)
            | Candidate -> Bool
forall a. HasOverlapMode a => a -> Bool
isIncoherent Candidate
c = Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True   -- See 'sinkIncoherent'
            | Term -> Bool
freshMetas Term
v'  = Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False  -- If there are fresh metas we can't compare
            | Bool
otherwise      =
          [Char] -> Int -> [Char] -> TCMT IO Bool -> TCMT IO Bool
forall a. [Char] -> Int -> [Char] -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> [Char] -> m a -> m a
verboseBracket [Char]
"tc.instance" Int
30 [Char]
"dropSameCandidates: " (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
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"==", Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v' ]
          a <- (Type -> Args -> TCMT IO Type) -> (Type, Args) -> TCMT IO Type
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Type -> Args -> TCMT IO Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
Type -> Args -> m Type
piApplyM ((Type, Args) -> TCMT IO Type)
-> TCMT IO (Type, Args) -> TCMT IO Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ((,) (Type -> Args -> (Type, Args))
-> TCMT IO Type -> TCMT IO (Args -> (Type, Args))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO Type
forall (m :: * -> *). ReadTCState m => MetaId -> m Type
getMetaType MetaId
m TCMT IO (Args -> (Type, Args))
-> TCMT IO Args -> TCMT IO (Type, Args)
forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TCMT IO Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs)
          runBlocked (pureEqualTerm a v v') <&> \case
            Left{}  -> Bool
False
            Right Bool
b -> Bool
b

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

            whenProfile Profile.Instances $ tick "checkCandidateForMeta: yes"
            return $ Yes v overlapOk
      where
        runCandidateCheck :: TCM YesNo -> TCM YesNo
runCandidateCheck = (TCM YesNo -> (TCErr -> TCM YesNo) -> TCM YesNo)
-> (TCErr -> TCM YesNo) -> TCM YesNo -> TCM YesNo
forall a b c. (a -> b -> c) -> b -> a -> c
flip TCM YesNo -> (TCErr -> TCM YesNo) -> TCM YesNo
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError TCErr -> TCM YesNo
handle (TCM YesNo -> TCM YesNo)
-> (TCM YesNo -> TCM YesNo) -> TCM YesNo -> TCM YesNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCM YesNo -> TCM YesNo
forall (m :: * -> *) a. ReadTCState m => m a -> m a
nowConsideringInstance

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

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


nowConsideringInstance :: (ReadTCState m) => m a -> m a
nowConsideringInstance :: forall (m :: * -> *) a. ReadTCState m => m a -> m a
nowConsideringInstance = Lens' TCState Bool -> (Bool -> Bool) -> m a -> m a
forall a b. Lens' TCState a -> (a -> a) -> m b -> m b
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' TCState a -> (a -> a) -> m b -> m b
locallyTCState (Bool -> f Bool) -> TCState -> f TCState
Lens' TCState Bool
stConsideringInstance ((Bool -> Bool) -> m a -> m a) -> (Bool -> Bool) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
True

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

wakeupInstanceConstraints :: TCM ()
wakeupInstanceConstraints :: TCMT IO ()
wakeupInstanceConstraints =
  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)
    TCMT IO ()
solveAwakeInstanceConstraints

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

postponeInstanceConstraints :: TCM a -> TCM a
postponeInstanceConstraints :: forall a. TCM a -> TCM a
postponeInstanceConstraints TCM a
m =
  Lens' TCState Bool -> (Bool -> Bool) -> TCM a -> TCM a
forall a b. Lens' TCState a -> (a -> a) -> TCMT IO b -> TCMT IO b
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' TCState a -> (a -> a) -> m b -> m b
locallyTCState (Bool -> f Bool) -> TCState -> f TCState
Lens' TCState Bool
stPostponeInstanceSearch (Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
True) TCM a
m TCM a -> TCMT IO () -> TCM a
forall a b. TCMT IO a -> TCMT IO b -> TCMT IO a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* TCMT IO ()
wakeupInstanceConstraints

-- | 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 a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Term
t Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` Args
vs
  case Term
t of
    Con ConHead
c ConInfo
ci [] -> do
      def <- Definition -> Defn
theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ConHead -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => ConHead -> m Definition
getConInfo ConHead
c
      case def of
        Constructor {conPars :: Defn -> Int
conPars = Int
n} -> Term -> TCMT IO Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci ((Arg Term -> Elim) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Args -> Elims) -> 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.
      mp <- QName -> TCMT IO (Maybe Projection)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isRelevantProjection QName
f
      case 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 a. a -> TCMT IO a
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

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

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

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


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

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

  (tel, hdt, n) <- Type -> TCM (Telescope, Term, OutputTypeName)
getOutputTypeName Type
t
  case n of
    OutputTypeName QName
n -> Telescope -> TCMT IO () -> TCMT IO ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
      tele <- TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope

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

      tree <- insertDT (length tele) hdt x =<< getsTC (view stInstanceTree)
      setTCLens stInstanceTree tree

      modifyTCLens' (stSignature . sigInstances . itableCounts) $
        Map.insertWith (+) n 1

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

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

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

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

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

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

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

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

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

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