{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation #-}

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

import Control.Monad          (forM, filterM)
import Control.Monad.Except   (ExceptT(..), runExceptT, MonadError(..))
import Control.Monad.Trans    (lift )
-- import Control.Monad.IO.Class (liftIO)

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

import Agda.Interaction.Options (optQualifiedInstances)

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

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

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

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

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

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

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

-- | Compute a list of instance candidates.
--   'Nothing' if target type or any context type is a meta, error if
--   type is not eligible for instance search.
initialInstanceCandidates :: Bool -> Type -> TCM (Either Blocker [Candidate])
initialInstanceCandidates :: Bool -> Type -> TCM (Either Blocker [Candidate])
initialInstanceCandidates Bool
blockOverlap Type
instTy = do
  (Telescope
_, Term
_, OutputTypeName
otn) <- Type -> TCM (Telescope, Term, OutputTypeName)
getOutputTypeName Type
instTy
  case OutputTypeName
otn of
    OutputTypeName
NoOutputTypeName -> TypeError -> TCM (Either Blocker [Candidate])
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM (Either Blocker [Candidate]))
-> TypeError -> TCM (Either Blocker [Candidate])
forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError ([Char] -> TypeError) -> [Char] -> TypeError
forall a b. (a -> b) -> a -> b
$
      [Char]
"Instance search can only be used to find elements in a named type"
    OutputTypeNameNotYetKnown Blocker
b -> do
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.cands" Int
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Instance type is not yet known. "
      Either Blocker [Candidate] -> TCM (Either Blocker [Candidate])
forall 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
OutputTypeVisiblePi -> TypeError -> TCM (Either Blocker [Candidate])
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM (Either Blocker [Candidate]))
-> TypeError -> TCM (Either Blocker [Candidate])
forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError ([Char] -> TypeError) -> [Char] -> TypeError
forall a b. (a -> b) -> a -> b
$
      [Char]
"Instance search cannot be used to find elements in an explicit function type"
    OutputTypeName
OutputTypeVar -> do
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.cands" Int
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Instance type is a variable. "
      BlockT (TCMT IO) [Candidate] -> TCM (Either Blocker [Candidate])
forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked (Maybe QName -> BlockT (TCMT IO) [Candidate]
getContextVars Maybe QName
forall a. Maybe a
Nothing)
    OutputTypeName QName
n -> Account (BenchPhase (TCMT IO))
-> TCM (Either Blocker [Candidate])
-> TCM (Either Blocker [Candidate])
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.Typing, BenchPhase (TCMT IO)
Phase
Bench.InstanceSearch, BenchPhase (TCMT IO)
Phase
Bench.InitialCandidates] do
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.cands" Int
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Found instance type head: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
n
      BlockT (TCMT IO) [Candidate] -> TCM (Either Blocker [Candidate])
forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked do
        [Candidate]
local  <- Maybe QName -> BlockT (TCMT IO) [Candidate]
getContextVars (QName -> Maybe QName
forall a. a -> Maybe a
Just QName
n)
        [Candidate]
global <- QName -> BlockT (TCMT IO) [Candidate]
getScopeDefs QName
n
        TCMT IO () -> BlockT (TCMT IO) ()
forall (m :: * -> *) a. Monad m => m a -> BlockT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO () -> BlockT (TCMT IO) ())
-> TCMT IO () -> BlockT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ QName -> Int -> TCMT IO ()
forall {m :: * -> *} {a} {a}.
(PrettyTCM a, MonadFresh NameId m, MonadInteractionPoints m,
 MonadStConcreteNames m, PureTCM m, IsString (m Doc), Null (m Doc),
 Semigroup (m Doc), MonadStatistics m, Integral a) =>
a -> a -> m ()
tickCandidates QName
n (Int -> TCMT IO ()) -> Int -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Candidate] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Candidate]
local 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]
global
        [Candidate] -> BlockT (TCMT IO) [Candidate]
forall a. a -> BlockT (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Candidate] -> BlockT (TCMT IO) [Candidate])
-> [Candidate] -> BlockT (TCMT IO) [Candidate]
forall a b. (a -> b) -> a -> b
$ [Candidate]
local [Candidate] -> [Candidate] -> [Candidate]
forall a. Semigroup a => a -> a -> a
<> [Candidate]
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
      Doc
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]
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
      [Char] -> m ()
forall (m :: * -> *). MonadStatistics m => [Char] -> m ()
tick ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$ [Char]
pref [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
": attempts"
      -- Per-class info: number of constraints where there was only one
      -- candidate (awesome) + the total number of candidates we've gone
      -- through.
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (a
size a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
1) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ [Char] -> m ()
forall (m :: * -> *). MonadStatistics m => [Char] -> m ()
tick ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$ [Char]
pref [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
": only one candidate"
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (a
size a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
1) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Integer -> m ()
forall (m :: * -> *).
MonadStatistics m =>
[Char] -> Integer -> m ()
tickN
        ([Char]
pref [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
": total candidates visited")
        (a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
size)

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

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

      -- get let bindings
      LetBindings
env <- (TCEnv -> LetBindings) -> BlockT (TCMT IO) LetBindings
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> LetBindings
envLetBindings
      [(Name, LetBinding)]
env <- ((Name, Open LetBinding) -> BlockT (TCMT IO) (Name, LetBinding))
-> [(Name, Open LetBinding)]
-> BlockT (TCMT IO) [(Name, LetBinding)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((Open LetBinding -> BlockT (TCMT IO) LetBinding)
-> (Name, Open LetBinding) -> BlockT (TCMT IO) (Name, LetBinding)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> (Name, a) -> f (Name, b)
traverse Open LetBinding -> BlockT (TCMT IO) LetBinding
forall a (m :: * -> *).
(TermSubst a, MonadTCEnv m) =>
Open a -> m a
getOpen) ([(Name, Open LetBinding)]
 -> BlockT (TCMT IO) [(Name, LetBinding)])
-> [(Name, Open LetBinding)]
-> BlockT (TCMT IO) [(Name, LetBinding)]
forall a b. (a -> b) -> a -> b
$ LetBindings -> [(Name, Open LetBinding)]
forall k a. Map k a -> [(k, a)]
Map.toList LetBindings
env
      let lets :: [Candidate]
lets = [ CandidateKind -> Term -> Type -> OverlapMode -> Candidate
Candidate CandidateKind
LocalCandidate Term
v Type
t OverlapMode
DefaultOverlap
                 | (Name
_, LetBinding Origin
_ Term
v Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info, unDom :: forall t e. Dom' t e -> e
unDom = Type
t}) <- [(Name, LetBinding)]
env
                 , ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
isInstance ArgInfo
info
                 , ArgInfo -> Bool
forall a. LensModality a => a -> Bool
usableModality ArgInfo
info
                 ]
      (Candidate -> BlockT (TCMT IO) Bool)
-> [Candidate] -> BlockT (TCMT IO) [Candidate]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (Maybe QName -> Type -> BlockT (TCMT IO) Bool
sameHead Maybe QName
cls (Type -> BlockT (TCMT IO) Bool)
-> (Candidate -> Type) -> Candidate -> BlockT (TCMT IO) Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Candidate -> Type
candidateType) ([Candidate] -> BlockT (TCMT IO) [Candidate])
-> [Candidate] -> BlockT (TCMT IO) [Candidate]
forall a b. (a -> b) -> a -> b
$ [Candidate]
vars [Candidate] -> [Candidate] -> [Candidate]
forall a. [a] -> [a] -> [a]
++ [Candidate]
fields [Candidate] -> [Candidate] -> [Candidate]
forall a. [a] -> [a] -> [a]
++ [Candidate]
lets

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

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

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

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

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

    getScopeDefs :: QName -> BlockT TCM [Candidate]
    getScopeDefs :: QName -> BlockT (TCMT IO) [Candidate]
getScopeDefs QName
n = do
      Relevance
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 DiscrimTree QName
tree Map QName Int
counts <- TCM InstanceTable -> BlockT (TCMT IO) InstanceTable
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 InstanceTable
getInstanceDefs
      QueryResult Set QName
qs Blocker
blocker <- TCM (QueryResult QName) -> BlockT (TCMT IO) (QueryResult QName)
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 (QueryResult QName) -> BlockT (TCMT IO) (QueryResult QName))
-> TCM (QueryResult QName) -> BlockT (TCMT IO) (QueryResult QName)
forall a b. (a -> b) -> a -> b
$ Term -> DiscrimTree QName -> TCM (QueryResult QName)
forall a.
(Ord a, PrettyTCM a) =>
Term -> DiscrimTree a -> TCM (QueryResult a)
lookupDT (Type -> Term
forall t a. Type'' t a -> a
unEl Type
instTy) DiscrimTree QName
tree

      Set QName
mutual <- BlockT (TCMT IO) (Maybe MutualId)
-> BlockT (TCMT IO) (Set QName)
-> (MutualId -> BlockT (TCMT IO) (Set QName))
-> BlockT (TCMT IO) (Set QName)
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM ((TCEnv -> Maybe MutualId) -> BlockT (TCMT IO) (Maybe MutualId)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe MutualId
envMutualBlock) (Set QName -> BlockT (TCMT IO) (Set QName)
forall a. a -> BlockT (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)
-> BlockT (TCMT IO) MutualBlock -> BlockT (TCMT IO) (Set QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MutualId -> BlockT (TCMT IO) MutualBlock
forall (tcm :: * -> *).
ReadTCState tcm =>
MutualId -> tcm MutualBlock
lookupMutualBlock MutualId
mb

      [Char] -> Int -> TCMT IO Doc -> BlockT (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.candidates.search" Int
20 (TCMT IO Doc -> BlockT (TCMT IO) ())
-> TCMT IO Doc -> BlockT (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 candidates from signature for goal:"
        , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (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
=<< Type -> TCMT IO Type
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Type
instTy)
        , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (Set QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Set QName -> m Doc
prettyTCM Set QName
qs) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"length:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Int -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Int -> m Doc
prettyTCM (Set QName -> Int
forall a. Set a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Set QName
qs)
        , TCMT IO Doc
"blocker:"
        , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (Blocker -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Blocker -> m Doc
prettyTCM Blocker
blocker)
        , TCMT IO Doc
"mutual block:"
        , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (Set QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Set QName -> m Doc
prettyTCM Set QName
mutual)
        ]

      [Candidate]
cands <- [Maybe Candidate] -> [Candidate]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe Candidate] -> [Candidate])
-> BlockT (TCMT IO) [Maybe Candidate]
-> BlockT (TCMT IO) [Candidate]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (QName -> BlockT (TCMT IO) (Maybe Candidate))
-> [QName] -> BlockT (TCMT IO) [Maybe Candidate]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (TCM (Maybe Candidate) -> BlockT (TCMT IO) (Maybe Candidate)
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 (Maybe Candidate) -> BlockT (TCMT IO) (Maybe Candidate))
-> (QName -> TCM (Maybe Candidate))
-> QName
-> BlockT (TCMT IO) (Maybe Candidate)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Relevance -> QName -> TCM (Maybe Candidate)
candidate Relevance
rel) (Set QName -> [QName]
forall a. Set a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Set QName
qs)

      -- Some more class-specific profiling.
      TCMT IO () -> BlockT (TCMT IO) ()
forall (m :: * -> *) a. Monad m => m a -> BlockT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO () -> BlockT (TCMT IO) ())
-> TCMT IO () -> BlockT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ ProfileOption -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Instances case QName -> Map QName Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
n Map QName Int
counts of
        Just Int
tot -> do
          Doc
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 :: Integer
diff = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
tot Int -> Int -> Int
forall a. Num a => a -> a -> a
- [Candidate] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Candidate]
cands)
          [Char] -> Integer -> TCMT IO ()
forall (m :: * -> *).
MonadStatistics m =>
[Char] -> Integer -> m ()
tickN [Char]
"instances discarded early" Integer
diff
          [Char] -> Integer -> TCMT IO ()
forall (m :: * -> *).
MonadStatistics m =>
[Char] -> Integer -> m ()
tickN ([Char]
"class " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Doc -> [Char]
forall a. Show a => a -> [Char]
show Doc
n [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
": discarded early") Integer
diff
        Maybe Int
Nothing  -> () -> TCMT IO ()
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

      [Candidate] -> BlockT (TCMT IO) [Candidate]
forall a. a -> BlockT (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Candidate]
cands

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

            v :: Term
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 :: OverlapMode
mode = case Definition -> Maybe InstanceInfo
defInstance Definition
def of
              Just InstanceInfo
i  -> InstanceInfo -> OverlapMode
instanceOverlap InstanceInfo
i
              Maybe InstanceInfo
Nothing -> OverlapMode
DefaultOverlap

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

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


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

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

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

-- | 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
    MetaVariable
mv <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
    MetaVariable
-> TCM (Either Blocker [Candidate])
-> TCM (Either Blocker [Candidate])
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange MetaVariable
mv (TCM (Either Blocker [Candidate])
 -> TCM (Either Blocker [Candidate]))
-> TCM (Either Blocker [Candidate])
-> TCM (Either Blocker [Candidate])
forall a b. (a -> b) -> a -> b
$ do
      Type
t <- Type -> TCMT IO Type
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate (Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MetaId -> TCMT IO Type
forall (m :: * -> *).
(HasBuiltins m, HasCallStack, MonadDebug m, MonadReduce m,
 MonadTCEnv m, ReadTCState m) =>
MetaId -> m Type
getMetaTypeInContext MetaId
m
      TelV Telescope
tel Type
t' <- Int -> (Dom Type -> Bool) -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> (Dom Type -> Bool) -> Type -> m (TelV Type)
telViewUpTo' (-Int
1) Dom Type -> Bool
forall a. LensHiding a => a -> Bool
notVisible Type
t
      Telescope
-> TCM (Either Blocker [Candidate])
-> TCM (Either Blocker [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
tel (TCM (Either Blocker [Candidate])
 -> TCM (Either Blocker [Candidate]))
-> TCM (Either Blocker [Candidate])
-> TCM (Either Blocker [Candidate])
forall a b. (a -> b) -> a -> b
$ ExceptT Blocker (TCMT IO) [Candidate]
-> TCM (Either Blocker [Candidate])
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (Type -> ExceptT Blocker (TCMT IO) [Candidate]
worker Type
t')

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

  worker :: Type -> ExceptT Blocker TCM [Candidate]
  worker :: Type -> ExceptT Blocker (TCMT IO) [Candidate]
worker Type
t' = do
    [Candidate]
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')
    [Candidate]
cands <- TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
-> ExceptT
     Blocker
     (TCMT IO)
     (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
forall (m :: * -> *) a. Monad m => m a -> ExceptT Blocker m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (MetaId
-> Type
-> [Candidate]
-> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
checkCandidates MetaId
m Type
t' [Candidate]
cands) ExceptT
  Blocker
  (TCMT IO)
  (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
-> (Maybe ([(Candidate, TCErr)], [(Candidate, Term)])
    -> [Candidate])
-> ExceptT Blocker (TCMT IO) [Candidate]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \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
    [Candidate]
cands <- Account (BenchPhase (ExceptT Blocker (TCMT IO)))
-> ExceptT Blocker (TCMT IO) [Candidate]
-> ExceptT Blocker (TCMT IO) [Candidate]
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (ExceptT Blocker (TCMT IO))
Phase
Bench.Typing, BenchPhase (ExceptT Blocker (TCMT IO))
Phase
Bench.InstanceSearch, BenchPhase (ExceptT Blocker (TCMT IO))
Phase
Bench.OrderCandidates] (ExceptT Blocker (TCMT IO) [Candidate]
 -> ExceptT Blocker (TCMT IO) [Candidate])
-> ExceptT Blocker (TCMT IO) [Candidate]
-> ExceptT Blocker (TCMT IO) [Candidate]
forall a b. (a -> b) -> a -> b
$
      TCM [Candidate] -> ExceptT Blocker (TCMT IO) [Candidate]
forall (m :: * -> *) a. Monad m => m a -> ExceptT Blocker m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift ((Candidate -> [Candidate] -> TCM [Candidate])
-> [Candidate] -> [Candidate] -> TCM [Candidate]
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM Candidate -> [Candidate] -> TCM [Candidate]
insertCandidate [] [Candidate]
cands)

    [Char] -> Int -> TCMT IO Doc -> ExceptT Blocker (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.sort" Int
20 (TCMT IO Doc -> ExceptT Blocker (TCMT IO) ())
-> TCMT IO Doc -> ExceptT Blocker (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
"sorted candidates" 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 ((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)

    [Candidate] -> ExceptT Blocker (TCMT IO) [Candidate]
forall a. a -> ExceptT Blocker (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Candidate]
cands

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

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

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

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

  TelV Telescope
tel Type
t1 <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t1
  Telescope -> TCMT IO Bool -> TCMT IO Bool
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 Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ TCMT IO Bool -> TCMT IO Bool
wrap (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ do
    (Args
args, Type
t2) <- Int -> (Hiding -> Bool) -> Type -> TCMT IO (Args, Type)
forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m, MonadTCM m) =>
Int -> (Hiding -> Bool) -> Type -> m (Args, Type)
implicitArgs (-Int
1) (\Hiding
h -> Hiding -> Bool
forall a. LensHiding a => a -> Bool
notVisible Hiding
h) Type
t2

    [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.sort" Int
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Does" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Candidate -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Candidate -> m Doc
prettyTCM (Int -> Candidate -> Candidate
forall a. Subst a => Int -> a -> a
raise (Telescope -> Int
forall a. Tele a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Telescope
tel) Candidate
c1) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"specialise" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Candidate -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Candidate -> m Doc
prettyTCM (Int -> Candidate -> Candidate
forall a. Subst a => Int -> a -> a
raise (Telescope -> Int
forall a. Tele a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Telescope
tel) Candidate
c2) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
"?")
    [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.sort" Int
60 (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 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 a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Candidate -> m Doc
prettyTCM Candidate
c1 TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc
colon 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
t1)
      , TCMT IO Doc
"vs"
      , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (Candidate -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Candidate -> m Doc
prettyTCM Candidate
c2 TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc
colon 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
t2)
      ]

    Type -> Type -> TCMT IO ()
forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
leqType Type
t2 Type
t1
    [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.sort" Int
30 (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
"=> IS specialisation"
    Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True

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

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

    recursive :: TCMT IO (Maybe ([Candidate], Blocker))
recursive = do
      Bool
recur <- Lens' TCState Bool -> TCMT IO Bool
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Bool -> f Bool) -> TCState -> f TCState
Lens' TCState Bool
stConsideringInstance
      [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.instance.defer" Int
20
        if Bool
recur
          then [Char]
"Postponing recursive instance search."
          else [Char]
"Postponing possibly recursive instance search."
      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: recursive"
      Maybe ([Candidate], Blocker)
-> TCMT IO (Maybe ([Candidate], Blocker))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([Candidate], Blocker)
 -> TCMT IO (Maybe ([Candidate], Blocker)))
-> Maybe ([Candidate], Blocker)
-> TCMT IO (Maybe ([Candidate], Blocker))
forall a b. (a -> b) -> a -> b
$ ([Candidate], Blocker) -> Maybe ([Candidate], Blocker)
forall a. a -> Maybe a
Just ([Candidate]
cands, Blocker
neverUnblock)

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

  -- Andreas, 2015-02-07: New metas should be created with range of the
  -- current instance meta, thus, we set the range.
  MetaVariable
mv <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
  MetaVariable
-> TCMT IO (Maybe ([Candidate], Blocker))
-> TCMT IO (Maybe ([Candidate], Blocker))
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange MetaVariable
mv (TCMT IO (Maybe ([Candidate], Blocker))
 -> TCMT IO (Maybe ([Candidate], Blocker)))
-> TCMT IO (Maybe ([Candidate], Blocker))
-> TCMT IO (Maybe ([Candidate], Blocker))
forall a b. (a -> b) -> a -> b
$ do
      [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.instance" Int
15 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
        [Char]
"findInstance 2: constraint: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ MetaId -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow MetaId
m [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"; candidates left: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show ([Candidate] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Candidate]
cands)
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
60 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (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
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
70 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"raw" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ do
       Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (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
debugCandidateRaw [Candidate]
cands

      Type
t <- MetaId -> TCMT IO Type
forall (m :: * -> *).
(HasBuiltins m, HasCallStack, MonadDebug m, MonadReduce m,
 MonadTCEnv m, ReadTCState m) =>
MetaId -> m Type
getMetaTypeInContext MetaId
m
      [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.instance" Int
70 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"findInstance 2: t: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Type
t

      Type
-> (Type -> TCMT IO (Maybe ([Candidate], Blocker)))
-> TCMT IO (Maybe ([Candidate], Blocker))
forall a. Type -> (Type -> TCM a) -> TCM a
insidePi Type
t ((Type -> TCMT IO (Maybe ([Candidate], Blocker)))
 -> TCMT IO (Maybe ([Candidate], Blocker)))
-> (Type -> TCMT IO (Maybe ([Candidate], Blocker)))
-> TCMT IO (Maybe ([Candidate], Blocker))
forall a b. (a -> b) -> a -> b
$ \ Type
t -> do
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
15 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"findInstance 3: t =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
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

      Maybe ([(Candidate, TCErr)], [(Candidate, Term)])
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

      TCMT IO ()
debugConstraints
      case Maybe ([(Candidate, TCErr)], [(Candidate, Term)])
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 (Int32 -> Int32 -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int32 -> Int32 -> Ordering)
-> ((Candidate, TCErr) -> Int32)
-> (Candidate, TCErr)
-> (Candidate, TCErr)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Candidate, TCErr) -> Int32
precision) [(Candidate, TCErr)]
errs
                where precision :: (Candidate, TCErr) -> Int32
precision (Candidate
_, TCErr
err) = Int32 -> (Interval' () -> Int32) -> Maybe (Interval' ()) -> Int32
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Int32
infinity Interval' () -> Int32
forall a. Interval' a -> Int32
iLength (Maybe (Interval' ()) -> Int32) -> Maybe (Interval' ()) -> Int32
forall a b. (a -> b) -> a -> b
$ Range' SrcFile -> Maybe (Interval' ())
forall a. Range' a -> Maybe (Interval' ())
rangeToInterval (Range' SrcFile -> Maybe (Interval' ()))
-> Range' SrcFile -> Maybe (Interval' ())
forall a b. (a -> b) -> a -> b
$ TCErr -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange TCErr
err
                      infinity :: Int32
infinity = Int32
1000000000
          [TCErr]
-> TCMT IO (Maybe ([Candidate], Blocker))
-> TCMT IO (Maybe ([Candidate], Blocker))
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange (Int -> [TCErr] -> [TCErr]
forall a. Int -> [a] -> [a]
take Int
1 ([TCErr] -> [TCErr]) -> [TCErr] -> [TCErr]
forall a b. (a -> b) -> a -> b
$ ((Candidate, TCErr) -> TCErr) -> [(Candidate, TCErr)] -> [TCErr]
forall a b. (a -> b) -> [a] -> [b]
map (Candidate, TCErr) -> TCErr
forall a b. (a, b) -> b
snd [(Candidate, TCErr)]
sortedErrs) (TCMT IO (Maybe ([Candidate], Blocker))
 -> TCMT IO (Maybe ([Candidate], Blocker)))
-> TCMT IO (Maybe ([Candidate], Blocker))
-> TCMT IO (Maybe ([Candidate], Blocker))
forall a b. (a -> b) -> a -> b
$
            TypeError -> TCMT IO (Maybe ([Candidate], Blocker))
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO (Maybe ([Candidate], Blocker)))
-> TypeError -> TCMT IO (Maybe ([Candidate], Blocker))
forall a b. (a -> b) -> a -> b
$ Type -> [(Term, TCErr)] -> TypeError
InstanceNoCandidate Type
t [ (Candidate -> Term
candidateTerm Candidate
c, TCErr
err) | (Candidate
c, TCErr
err) <- [(Candidate, TCErr)]
sortedErrs ]

        Just ([(Candidate, TCErr)]
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

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

          [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
15 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ TCMT IO Doc
"findInstance 5: solved by instance search using the only candidate"
            , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Candidate -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Candidate -> m Doc
prettyTCM Candidate
c TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
term
            , TCMT IO Doc
"of type " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t'
            , TCMT IO Doc
"for type" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
            ]

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

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

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

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

  -- Check that there aren't any hard failures
  case [ TCErr
err | (Candidate
_, (HellNo TCErr
err, TCState
_)) <- [(Candidate, (YesNo, TCState))]
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, Term, TCState)]
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 :: Bool
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
  [(Candidate, Term, TCState)]
result'' <- MetaId
-> Bool
-> [(Candidate, Term, TCState)]
-> TCM [(Candidate, Term, TCState)]
dropSameCandidates MetaId
m Bool
overlap [(Candidate, Term, TCState)]
result'
  case [(Candidate, Term, TCState)]
result'' of
    [(Candidate
c, Term
v, TCState
s)] -> ([], [(Candidate
c, Term
v)]) ([(Candidate, TCErr)], [(Candidate, Term)])
-> TCMT IO () -> TCM ([(Candidate, TCErr)], [(Candidate, Term)])
forall a b. a -> TCMT IO b -> TCMT IO a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ TCState -> TCMT IO ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
s
    [(Candidate, Term, TCState)]
_           -> do
      let bad :: [(Candidate, TCErr)]
bad  = [ (Candidate
c, TCErr
err) | (Candidate
c, (NoBecause TCErr
err, TCState
_)) <- [(Candidate, (YesNo, TCState))]
result ]
          good :: [(Candidate, Term)]
good = [ (Candidate
c, Term
v) | (Candidate
c, Term
v, TCState
_) <- [(Candidate, Term, TCState)]
result'' ]
      ([(Candidate, TCErr)], [(Candidate, Term)])
-> TCM ([(Candidate, TCErr)], [(Candidate, Term)])
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Candidate, TCErr)]
bad, [(Candidate, Term)]
good)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    [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
"inserting 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
"against old candidates"
      , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([TCMT IO Doc] -> TCMT IO Doc
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))
      , TCMT IO Doc
"and guarding candidates"
      , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([TCMT IO Doc] -> TCMT IO Doc
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]
guards))
      , TCMT IO Doc
"is guarded?" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Bool -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Bool -> m Doc
prettyTCM Bool
guarded
      ]

    if Bool
guarded 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 else OverlapState item -> item -> [item] -> TCMT IO (OverlapState item)
insertNew OverlapState item
oldState item
newItem [item]
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
  !MetaId
nextMeta    <- TCMT IO MetaId
forall (m :: * -> *). ReadTCState m => m MetaId
nextLocalMeta
  MetaId -> Bool
isRemoteMeta <- TCMT IO (MetaId -> Bool)
forall (m :: * -> *). ReadTCState m => m (MetaId -> Bool)
isRemoteMeta

  -- Does "it" contain any fresh meta-variables?
  let freshMetas :: Term -> Bool
freshMetas = Any -> Bool
getAny (Any -> Bool) -> (Term -> Any) -> Term -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MetaId -> Any) -> Term -> Any
forall 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)))

  Relevance
rel <- Modality -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance (Modality -> Relevance) -> TCMT IO Modality -> TCMT IO Relevance
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO Modality
forall (m :: * -> *). ReadTCState m => MetaId -> m Modality
lookupMetaModality MetaId
m

  -- Take overlappable candidates into account
  [(Candidate, Term, TCState)]
cands <- Bool
-> Relevance
-> ((Candidate, Term, TCState) -> Candidate)
-> [(Candidate, Term, TCState)]
-> TCM [(Candidate, Term, TCState)]
forall item.
Bool -> Relevance -> (item -> Candidate) -> [item] -> TCM [item]
resolveInstanceOverlap Bool
overlapOk Relevance
rel (Candidate, Term, TCState) -> Candidate
forall a b c. (a, b, c) -> a
fst3 [(Candidate, Term, TCState)]
cands0
  [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
"instances after resolving overlap:" 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 (((Candidate, Term, TCState) -> TCMT IO Doc)
-> [(Candidate, Term, TCState)] -> [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)
-> ((Candidate, Term, TCState) -> Candidate)
-> (Candidate, Term, TCState)
-> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Candidate, Term, TCState) -> Candidate
forall a b c. (a, b, c) -> a
fst3) [(Candidate, Term, TCState)]
cands)

  [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"valid candidates:"
    , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ if Term -> Bool
freshMetas Term
v then TCMT IO Doc
"(redacted)" else
                      [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v ]
                    | (Candidate
_, Term
v, TCState
_) <- [(Candidate, Term, TCState)]
cands ] ]

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

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

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

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

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

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

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

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

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

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

    Type
t <- Type -> TCMT IO Type
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Type
t
    cands' :: ([(Candidate, TCErr)], [(Candidate, Term)])
cands'@([(Candidate, TCErr)]
_, [(Candidate, Term)]
okay) <- MetaId
-> [Candidate]
-> (Candidate -> TCM YesNo)
-> TCM ([(Candidate, TCErr)], [(Candidate, Term)])
filterResettingState MetaId
m [Candidate]
cands (MetaId -> Type -> Candidate -> TCM YesNo
checkCandidateForMeta MetaId
m Type
t)

    [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.candidates" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"valid candidates", [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (((Candidate, Term) -> TCMT IO Doc)
-> [(Candidate, Term)] -> [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)
-> ((Candidate, Term) -> Candidate)
-> (Candidate, Term)
-> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Candidate, Term) -> Candidate
forall a b. (a, b) -> a
fst) [(Candidate, Term)]
okay) ]
    [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.candidates" Int
60 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"valid candidates", [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (((Candidate, Term) -> TCMT IO Doc)
-> [(Candidate, Term)] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Candidate -> TCMT IO Doc
forall (m :: * -> *). MonadPretty m => Candidate -> m Doc
debugCandidateTerm (Candidate -> TCMT IO Doc)
-> ((Candidate, Term) -> Candidate)
-> (Candidate, Term)
-> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Candidate, Term) -> Candidate
forall a b. (a, b) -> a
fst) [(Candidate, Term)]
okay) ]

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

    checkDepth :: Term -> Type -> TCM YesNo -> TCM YesNo
    checkDepth :: Term -> Type -> TCM YesNo -> TCM YesNo
checkDepth Term
c Type
a TCM YesNo
k = Lens' TCEnv Int -> (Int -> Int) -> TCM YesNo -> TCM YesNo
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC (Int -> f Int) -> TCEnv -> f TCEnv
Lens' TCEnv Int
eInstanceDepth Int -> Int
forall a. Enum a => a -> a
succ (TCM YesNo -> TCM YesNo) -> TCM YesNo -> TCM YesNo
forall a b. (a -> b) -> a -> b
$ do
      Int
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
      Int
maxDepth <- TCMT IO Int
forall (m :: * -> *). HasOptions m => m Int
maxInstanceSearchDepth
      Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
maxDepth) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Term -> Type -> Int -> TypeError
InstanceSearchDepthExhausted Term
c Type
a Int
maxDepth
      TCM YesNo
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.
      MetaVariable
mv <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
      MetaVariable -> TCM YesNo -> TCM YesNo
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange MetaVariable
mv (TCM YesNo -> TCM YesNo) -> TCM YesNo -> TCM YesNo
forall a b. (a -> b) -> a -> b
$ TCM YesNo -> TCM YesNo
runCandidateCheck (TCM YesNo -> TCM YesNo) -> TCM YesNo -> TCM YesNo
forall a b. (a -> b) -> a -> b
$
        [Char] -> Int -> [Char] -> TCM YesNo -> TCM YesNo
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
20 ([Char]
"checkCandidateForMeta " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ MetaId -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow MetaId
m) (TCM YesNo -> TCM YesNo) -> TCM YesNo -> TCM YesNo
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
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ TCMT IO Doc
"checkCandidateForMeta"
            , TCMT IO Doc
"  t    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
            , TCMT IO Doc
"  t'   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t'
            , TCMT IO Doc
"  term =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
term
            ]
          [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
70 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ TCMT IO Doc
"  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 (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
t
            , TCMT IO Doc
"  t'   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
t'
            , TCMT IO Doc
"  term =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
term
            ]
          TCMT IO ()
debugConstraints

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

          [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
            TCMT IO Doc
"instance search: checking" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t'' TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"<=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
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" Int
70 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ TCMT IO Doc
"instance search: checking (raw)"
            , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
4 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
t''
            , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"<="
            , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
4 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
t
            ]

          -- 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.
          ([ProblemConstraint]
cons, Bool
overlapOk) <- TCMT IO ()
-> TCM ([ProblemConstraint], Bool)
-> (ProblemId -> TCM ([ProblemConstraint], Bool))
-> TCM ([ProblemConstraint], Bool)
forall a. TCMT IO () -> TCM a -> (ProblemId -> TCM a) -> TCM a
ifNoConstraints_ (Type -> Type -> TCMT IO ()
forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
leqType Type
t'' Type
t) (([ProblemConstraint], Bool) -> TCM ([ProblemConstraint], Bool)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], Bool
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.
            [ProblemConstraint]
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.
            ProblemId -> TCMT IO ()
forall (m :: * -> *). MonadConstraint m => ProblemId -> m ()
stealConstraints ProblemId
pid
            let
              blocking :: Set MetaId
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 :: Bool
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)
            ([ProblemConstraint], Bool) -> TCM ([ProblemConstraint], Bool)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([ProblemConstraint]
cons, Bool
ok)
          TCMT IO ()
debugConstraints

          (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 (YesNo -> TCM YesNo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (YesNo -> TCM YesNo) -> (TCErr -> YesNo) -> TCErr -> TCM YesNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCErr -> YesNo
NoBecause) (TCM YesNo -> TCM YesNo) -> TCM YesNo -> TCM YesNo
forall a b. (a -> b) -> a -> b
$ 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.
            Bool -> TCMT IO ()
forall (m :: * -> *). MonadConstraint m => Bool -> m ()
solveAwakeConstraints' Bool
True
            -- We need instantiateFull here to remove 'local' metas
            Term
v <- Term -> TCMT IO Term
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull (Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Term
term Term -> Args -> TCMT IO Term
`applyDroppingParameters` Args
args)
            [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
15 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
              [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ (TCMT IO Doc
"instance search: found solution for" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
m) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
":"
                  , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
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.overlap" Int
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
              TCMT IO Doc
"candidate" 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 TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"okay for overlap?" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Bool -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Bool -> m Doc
prettyTCM Bool
overlapOk
              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 ((ProblemConstraint -> TCMT IO Doc)
-> [ProblemConstraint] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map ProblemConstraint -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ProblemConstraint -> m Doc
prettyTCM [ProblemConstraint]
cons)

            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: yes"
            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
$ Term -> Bool -> YesNo
Yes Term
v Bool
overlapOk
      where
        runCandidateCheck :: TCM YesNo -> TCM YesNo
runCandidateCheck = (TCM YesNo -> (TCErr -> TCM YesNo) -> TCM YesNo)
-> (TCErr -> TCM YesNo) -> TCM YesNo -> TCM YesNo
forall a b c. (a -> b -> c) -> b -> a -> c
flip TCM YesNo -> (TCErr -> TCM YesNo) -> TCM YesNo
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError TCErr -> TCM YesNo
handle (TCM YesNo -> TCM YesNo)
-> (TCM YesNo -> TCM YesNo) -> TCM YesNo -> TCM YesNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCM YesNo -> TCM YesNo
forall (m :: * -> *) a. ReadTCState m => m a -> m a
nowConsideringInstance

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

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


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

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

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

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

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

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

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

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

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


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

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

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

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

      DiscrimTree QName
tree <- Int
-> Term -> QName -> DiscrimTree QName -> TCM (DiscrimTree QName)
forall a.
(Ord a, PrettyTCM a) =>
Int -> Term -> a -> DiscrimTree a -> TCM (DiscrimTree a)
insertDT (Telescope -> Int
forall a. Tele a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Telescope
tele) Term
hdt QName
x (DiscrimTree QName -> TCM (DiscrimTree QName))
-> TCM (DiscrimTree QName) -> TCM (DiscrimTree QName)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (TCState -> DiscrimTree QName) -> TCM (DiscrimTree QName)
forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC (Lens' TCState (DiscrimTree QName) -> TCState -> DiscrimTree QName
forall o (m :: * -> *) i. MonadReader o m => Lens' o i -> m i
view (DiscrimTree QName -> f (DiscrimTree QName))
-> TCState -> f TCState
Lens' TCState (DiscrimTree QName)
stInstanceTree)
      Lens' TCState (DiscrimTree QName)
-> DiscrimTree QName -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
setTCLens (DiscrimTree QName -> f (DiscrimTree QName))
-> TCState -> f TCState
Lens' TCState (DiscrimTree QName)
stInstanceTree DiscrimTree QName
tree

      Lens' TCState (Map QName Int)
-> (Map QName Int -> Map QName Int) -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
modifyTCLens' ((Signature -> f Signature) -> TCState -> f TCState
Lens' TCState Signature
stSignature ((Signature -> f Signature) -> TCState -> f TCState)
-> ((Map QName Int -> f (Map QName Int))
    -> Signature -> f Signature)
-> (Map QName Int -> f (Map QName Int))
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InstanceTable -> f InstanceTable) -> Signature -> f Signature
Lens' Signature InstanceTable
sigInstances ((InstanceTable -> f InstanceTable) -> Signature -> f Signature)
-> ((Map QName Int -> f (Map QName Int))
    -> InstanceTable -> f InstanceTable)
-> (Map QName Int -> f (Map QName Int))
-> Signature
-> f Signature
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map QName Int -> f (Map QName Int))
-> InstanceTable -> f InstanceTable
Lens' InstanceTable (Map QName Int)
itableCounts) ((Map QName Int -> Map QName Int) -> TCMT IO ())
-> (Map QName Int -> Map QName Int) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
        (Int -> Int -> Int)
-> QName -> Int -> Map QName Int -> Map QName Int
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) QName
n Int
1

      let
        info :: InstanceInfo
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.
      (Signature -> Signature) -> TCMT IO ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> TCMT IO ())
-> (Signature -> Signature) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
x \ Definition
d -> Definition
d { defInstance = Just info }

      -- If there's anything visible in the context, which will
      -- eventually end up in the instance's type, let's make a note to
      -- get rid of it before serialising the instance table.
      Bool
con <- QName -> TCMT IO Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isConstructor QName
x
      -- However, do note that data constructors can have "visible
      -- arguments" in their global type which.. aren't actually
      -- visible: the parameters.
      Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((Dom Type -> Bool) -> Telescope -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Dom Type -> Bool
forall a. LensHiding a => a -> Bool
visible Telescope
tele Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
con) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Lens' TCState (Set QName) -> (Set QName -> Set QName) -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
modifyTCLens' (Set QName -> f (Set QName)) -> TCState -> f TCState
Lens' TCState (Set QName)
stTemporaryInstances ((Set QName -> Set QName) -> TCMT IO ())
-> (Set QName -> Set QName) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ QName -> Set QName -> Set QName
forall a. Ord a => a -> Set a -> Set a
Set.insert QName
x

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

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

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

-- | Try to solve the instance definitions whose type is not yet known, report
--   an error if it doesn't work and return the instance table otherwise.
getInstanceDefs :: TCM InstanceTable
getInstanceDefs :: TCM InstanceTable
getInstanceDefs = do
  (InstanceTable
table, Set QName
pending) <- TCM (InstanceTable, Set QName)
getAllInstanceDefs
  Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set QName -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set QName
pending) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
    Blocker -> TCMT IO ()
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
alwaysUnblock  -- TODO: more refined unblocking
  InstanceTable -> TCM InstanceTable
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return InstanceTable
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
  Set QName
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

  [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.prune" 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
"leaving section"
    , Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM (Telescope -> TCMT IO Doc) -> TCMT IO Telescope -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
    , TCMT IO Doc
"todo:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Set QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Set QName -> m Doc
prettyTCM Set QName
todo
    ]

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