{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation #-}

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

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

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

import Agda.Interaction.Options (optQualifiedInstances, lensOptExperimentalLazyInstances)

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

import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Conversion.Pure (pureBlockOrEqualTerm)
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.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Syntax.Common.Pretty (prettyShow)

import qualified Agda.Interaction.Options.ProfileOptions as Profile
import Agda.Utils.WithDefault (lensCollapseDefault)
import Agda.Utils.Impossible

import Agda.TypeChecking.DiscrimTree

-- | 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. BlockT m a -> m (Either Blocker a)
runBlocked (Maybe QName -> BlockT (TCMT IO) [Candidate]
getContextCands Maybe QName
forall a. Maybe a
Nothing)
    OutputTypeName QName
n -> Account (BenchPhase (TCMT IO))
-> TCM (Either Blocker [Candidate])
-> TCM (Either Blocker [Candidate])
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.Typing, BenchPhase (TCMT IO)
Phase
Bench.InstanceSearch, BenchPhase (TCMT IO)
Phase
Bench.InitialCandidates] do
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.cands" Int
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Found instance type head: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
n
      BlockT (TCMT IO) [Candidate] -> TCM (Either Blocker [Candidate])
forall (m :: * -> *) a. BlockT m a -> m (Either Blocker a)
runBlocked do
        local  <- Maybe QName -> BlockT (TCMT IO) [Candidate]
getContextCands (QName -> Maybe QName
forall a. a -> Maybe a
Just QName
n)
        global <- getScopeDefs n
        lift $ tickCandidates n $ length local + length global
        pure $ local <> global
  where
    -- Ticky profiling for statistics about a class.
    tickCandidates :: a -> a -> m ()
tickCandidates a
n a
size = ProfileOption -> m () -> m ()
forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Instances do
      n <- a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
n
      let pref = [Char]
"class " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Doc -> [Char]
forall a. Show a => a -> [Char]
show Doc
n

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

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

      -- {{}}-fields of variables are also candidates, as long as those
      -- variables are themselves instance arguments.
      -- as an exception, the record argument to a record module can
      -- also introduce instances, so that {{}}-fields of a record R
      -- will be considered when checking a declaration nested in the
      -- definition of R.
      let
        cxtAndTypes =
          [ (CandidateKind
LocalCandidate, Term
x, Type
t)
          | (Term
x, dom :: Dom' Term Type
dom@(Dom' Term Type -> Type
forall t e. Dom' t e -> e
unDom -> Type
t)) <- [(Term, Dom' Term Type)]
varsAndRaisedTypes
          , ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
isInstance (Dom' Term Type
dom Dom' Term Type
-> Getting ArgInfo (Dom' Term Type) ArgInfo -> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom' Term Type) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo) Bool -> Bool -> Bool
|| ArgInfo -> Origin
argInfoOrigin (Dom' Term Type
dom Dom' Term Type
-> Getting ArgInfo (Dom' Term Type) ArgInfo -> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom' Term Type) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo) Origin -> Origin -> Bool
forall a. Eq a => a -> a -> Bool
== Origin
RecordSelf
          ]
      reportSDoc "tc.instance.cands" 40 $ "Getting candidates by eta-expanding context" $$ nest 2 (vcat
        [ prettyTCM x <+> colon <+> prettyTCM t $$ (nest 2 $ "origin: " <> text (show o) <> ", used: " <> text (show used))
        | (x, dom@(unDom -> t)) <- varsAndRaisedTypes, let o = ArgInfo -> Origin
argInfoOrigin (Dom' Term Type
dom Dom' Term Type
-> Getting ArgInfo (Dom' Term Type) ArgInfo -> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom' Term Type) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo)
        , let used = ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
isInstance (Dom' Term Type
dom Dom' Term Type
-> Getting ArgInfo (Dom' Term Type) ArgInfo -> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom' Term Type) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo) Bool -> Bool -> Bool
|| Origin
o Origin -> Origin -> Bool
forall a. Eq a => a -> a -> Bool
== Origin
RecordSelf
        ])
      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 <- viewTC eLetBindings
      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 IsAxiom
_isAxiom Origin
_origin Term
v dom :: Dom' Term Type
dom@(Dom' Term Type -> Type
forall t e. Dom' t e -> e
unDom -> Type
t)) <- [(Name, LetBinding)]
env
                 , ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
isInstance (Dom' Term Type
dom Dom' Term Type
-> Getting ArgInfo (Dom' Term Type) ArgInfo -> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom' Term Type) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo)
                 , ArgInfo -> Bool
forall a. LensModality a => a -> Bool
usableModality (Dom' Term Type
dom Dom' Term Type
-> Getting ArgInfo (Dom' Term Type) ArgInfo -> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom' Term Type) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo)
                 ]
      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 :: * -> *).
(HasCallStack, 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 :: * -> *).
(HasCallStack, 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) = do
      TelV piTel t' <- TCM (TelV Type) -> BlockT (TCMT IO) (TelV Type)
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 (TelV Type) -> BlockT (TCMT IO) (TelV Type))
-> TCM (TelV Type) -> BlockT (TCMT IO) (TelV Type)
forall a b. (a -> b) -> a -> b
$ Int -> (Dom' Term Type -> Bool) -> Type -> TCM (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> (Dom' Term Type -> Bool) -> Type -> m (TelV Type)
telViewUpTo' (-Int
1) Dom' Term Type -> Bool
forall a. LensHiding a => a -> Bool
notVisible Type
t
      ifBlocked 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
t' -> do
      let n :: Int
n = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
piTel
      Telescope
-> BlockT (TCMT IO) [Candidate] -> BlockT (TCMT IO) [Candidate]
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
piTel (BlockT (TCMT IO) [Candidate] -> BlockT (TCMT IO) [Candidate])
-> BlockT (TCMT IO) [Candidate] -> BlockT (TCMT IO) [Candidate]
forall a b. (a -> b) -> a -> b
$ 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
        let v' :: Term
v' = Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise Int
n Term
v Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` Telescope -> Args
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
piTel
        (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 =>
QName -> Args -> Term -> m (Telescope, Args)
forceEtaExpandRecord QName
r Args
pars Term
v'
        let types = (Dom' Term Type -> Type) -> [Dom' Term Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map' Dom' Term Type -> Type
forall t e. Dom' t e -> e
unDom ([Dom' Term Type] -> [Type]) -> [Dom' Term Type] -> [Type]
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg [Dom' Term Type])
-> [Dom' Term Type] -> [Dom' Term Type]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst ([SubstArg [Dom' Term Type]]
-> Substitution' (SubstArg [Dom' Term Type])
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([SubstArg [Dom' Term Type]]
 -> Substitution' (SubstArg [Dom' Term Type]))
-> [SubstArg [Dom' Term Type]]
-> Substitution' (SubstArg [Dom' Term Type])
forall a b. (a -> b) -> a -> b
$ [SubstArg [Dom' Term Type]] -> [SubstArg [Dom' Term Type]]
forall a. [a] -> [a]
reverse ([SubstArg [Dom' Term Type]] -> [SubstArg [Dom' Term Type]])
-> [SubstArg [Dom' Term Type]] -> [SubstArg [Dom' Term Type]]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> SubstArg [Dom' Term Type])
-> Args -> [SubstArg [Dom' Term Type]]
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Term
Arg Term -> SubstArg [Dom' Term Type]
forall e. Arg e -> e
unArg Args
args) (Telescope -> [Dom' Term Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
tel)
        fmap concat $ forM (zip' args types) $ \ (Arg Term
arg, Type
t) -> do
          let
            absArg :: Term
absArg = Telescope -> Term -> Term
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
piTel (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
arg)
            absTy :: Type
absTy = Telescope -> Type -> Type
telePi Telescope
piTel Type
t
          ([ CandidateKind -> Term -> Type -> OverlapMode -> Candidate
Candidate CandidateKind
LocalCandidate Term
absArg Type
absTy (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, Term
absArg, Type
absTy)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

      pure cands

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

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

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

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

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

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


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

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

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

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

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

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

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

    pure cands

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        Maybe ([(Candidate, TCErr)], [(Candidate, Term)])
_ -> do
          let cs :: [Candidate]
cs = [Candidate]
-> (([(Candidate, TCErr)], [(Candidate, Term)]) -> [Candidate])
-> Maybe ([(Candidate, TCErr)], [(Candidate, Term)])
-> [Candidate]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Candidate]
cands (((Candidate, Term) -> Candidate)
-> [(Candidate, Term)] -> [Candidate]
forall a b. (a -> b) -> [a] -> [b]
map' (Candidate, Term) -> Candidate
forall a b. (a, b) -> a
fst ([(Candidate, Term)] -> [Candidate])
-> (([(Candidate, TCErr)], [(Candidate, Term)])
    -> [(Candidate, Term)])
-> ([(Candidate, TCErr)], [(Candidate, Term)])
-> [Candidate]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(Candidate, TCErr)], [(Candidate, Term)]) -> [(Candidate, Term)]
forall a b. (a, b) -> b
snd) Maybe ([(Candidate, TCErr)], [(Candidate, Term)])
mcands -- keep the current candidates if Nothing
          [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
15 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
            [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"findInstance 5: refined candidates: ") TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
            [Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Term] -> m Doc
prettyTCM ((Candidate -> Term) -> [Candidate] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
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' Term Type
a Abs Type
b     -> ([Char], Dom' Term 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' Term Type) -> m a -> m a
addContext (Abs Type -> [Char]
forall a. Abs a -> [Char]
absName Abs Type
b, Dom' Term 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 DummyTermKind
s Elims
_  -> [Char] -> TCM a
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ (DummyTermKind -> [Char]
forall a. Show a => a -> [Char]
show DummyTermKind
s)

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

    -- Have to use 'putTCPreservingStats' here otherwise the stats
    -- accumulated from checking other candidates and from
    -- 'dropSameCandidates' are lost.
    [(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 ()
putTCPreservingStats TCState
s

    [(Candidate, Term, TCState)]
_           -> do
      let bad :: [(Candidate, TCErr)]
bad  = [ (Candidate
c, TCErr
err) | (Candidate
c, (NoBecause TCErr
err, TCState
_)) <- [(Candidate, (YesNo, TCState))]
result ]
          good :: [(Candidate, Term)]
good = [ (Candidate
c, Term
v) | (Candidate
c, Term
v, TCState
_) <- [(Candidate, Term, TCState)]
result'' ]
      ([(Candidate, TCErr)], [(Candidate, Term)])
-> TCM ([(Candidate, TCErr)], [(Candidate, Term)])
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Candidate, TCErr)]
bad, [(Candidate, Term)]
good)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    if guarded then pure oldState else insertNew oldState newItem oldItems

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

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

  rel <- getRelevance <$> lookupMetaModality m

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

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

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

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

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

      -- If we do actually have to remove overlap then we have to reduce
      -- the candidate to eliminate any "phantom" dependencies on fresh
      -- metas.
      -- ... issue #8215: while fastReduce is perfectly happy to block
      -- on a meta that doesn't exist, the short-circuit blocking in
      -- maybeFastReduce explodes, we have to reduce in the new TC
      -- state.
      v <- TCMT IO Term -> TCMT IO Term
forall a. TCM a -> TCM a
localTCState do
        TCState -> TCMT IO ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
st
        Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
      if
        | freshMetas v -> do
          reportSLn "tc.instance" 30 "dropSameCandidates: Solution of instance meta has fresh metas so we don't filter equal candidates yet"
          return (cvd : vas)
        | otherwise -> (cvd :) <$> dropWhileM equal vas

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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

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

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

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

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

flushInstanceConstraints :: TCM ()
flushInstanceConstraints :: TCMT IO ()
flushInstanceConstraints = Lens' TCState Bool -> (Bool -> Bool) -> TCMT IO () -> TCMT IO ()
forall a b. Lens' TCState a -> (a -> a) -> TCMT IO b -> TCMT IO b
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' TCState a -> (a -> a) -> m b -> m b
locallyTCState (Bool -> f Bool) -> TCState -> f TCState
Lens' TCState Bool
stInstanceHack (Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
True) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO ()
wakeupInstanceConstraints

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

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

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

-- | Strips all hidden and instance Pi's and return the argument
--   telescope, the head term, and its name, if possible.
getOutputTypeName :: Type -> TCM (Telescope, Term, OutputTypeName)
-- 2023-10-26, Jesper, issue #6941: To make instance search work correctly for
-- abstract or opaque instances, we need to ignore abstract mode when computing
-- the output type name.
getOutputTypeName :: Type -> TCM (Telescope, Term, OutputTypeName)
getOutputTypeName Type
t = TCM (Telescope, Term, OutputTypeName)
-> TCM (Telescope, Term, OutputTypeName)
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode (TCM (Telescope, Term, OutputTypeName)
 -> TCM (Telescope, Term, OutputTypeName))
-> TCM (Telescope, Term, OutputTypeName)
-> TCM (Telescope, Term, OutputTypeName)
forall a b. (a -> b) -> a -> b
$ do
  TelV tel t' <- Int -> (Dom' Term Type -> Bool) -> Type -> TCM (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> (Dom' Term Type -> Bool) -> Type -> m (TelV Type)
telViewUpTo' (-Int
1) Dom' Term 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 DummyTermKind
s Elims
_ -> [Char] -> TCM (Telescope, Term, OutputTypeName)
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ (DummyTermKind -> [Char]
forall a. Show a => a -> [Char]
show DummyTermKind
s)


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

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

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

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

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

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

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

      modifyTCLens' (stSignature . sigInstances . itableCounts) $
        if readd then id else 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 inst \ Definition
d -> Definition
d { defInstance = Just info }

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

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

    OutputTypeName
NoOutputTypeName    -> Bool -> TCMT IO () -> TCMT IO ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
when Bool
w (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Warning -> TCMT IO ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCMT IO ()) -> Warning -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ KwRange -> Warning
WrongInstanceDeclaration KwRange
kwr
    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
$ KwRange -> Warning
WrongInstanceDeclaration KwRange
kwr
    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
$ KwRange -> QName -> Warning
InstanceWithExplicitArg KwRange
kwr QName
inst

resolveInstanceHead ::
     KwRange  -- ^ The range of the @instance@ keyword.
  -> QName -> TCM ()
resolveInstanceHead :: KwRange -> QName -> TCMT IO ()
resolveInstanceHead KwRange
kwr QName
q = do
  QName -> TCMT IO ()
clearUnknownInstance QName
q
  -- Andreas, 2022-12-04, issue #6380:
  -- Do not warn about unusable instances here.
  Bool
-> Bool
-> Maybe InstanceInfo
-> KwRange
-> QName
-> Type
-> TCMT IO ()
addTypedInstance' Bool
False Bool
True Maybe InstanceInfo
forall a. Maybe a
Nothing KwRange
kwr 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' = ASetter Signature Signature (DiscrimTree QName) (DiscrimTree QName)
-> (DiscrimTree QName -> DiscrimTree QName)
-> Signature
-> Signature
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ((InstanceTable -> Identity InstanceTable)
-> Signature -> Identity Signature
Lens' Signature InstanceTable
sigInstances ((InstanceTable -> Identity InstanceTable)
 -> Signature -> Identity Signature)
-> ((DiscrimTree QName -> Identity (DiscrimTree QName))
    -> InstanceTable -> Identity InstanceTable)
-> ASetter
     Signature Signature (DiscrimTree QName) (DiscrimTree QName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DiscrimTree QName -> Identity (DiscrimTree QName))
-> InstanceTable -> Identity InstanceTable
Lens' InstanceTable (DiscrimTree QName)
itableTree) (Set QName -> DiscrimTree QName -> DiscrimTree QName
forall a. Ord a => Set a -> DiscrimTree a -> DiscrimTree a
deleteFromDT Set QName
todo) (Interface -> Signature
iSignature Interface
int)
  pure int{ iSignature = sig' }