{-# LANGUAGE NondecreasingIndentation #-}

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

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

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

import Agda.Interaction.Options (optOverlappingInstances, optQualifiedInstances)

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

import Agda.TypeChecking.Errors () --instance only
import Agda.TypeChecking.Implicit (implicitArgs)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Records
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope

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

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

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

import Agda.Utils.Impossible

-- | Compute a list of instance candidates.
--   'Nothing' if target type or any context type is a meta, error if
--   type is not eligible for instance search.
initialInstanceCandidates :: Type -> TCM (Either Blocker [Candidate])
initialInstanceCandidates :: Type -> TCM (Either Blocker [Candidate])
initialInstanceCandidates Type
t = do
  (Telescope
_ , OutputTypeName
otn) <- Type -> TCM (Telescope, OutputTypeName)
getOutputTypeName Type
t
  case OutputTypeName
otn of
    OutputTypeName
NoOutputTypeName -> TypeError -> TCM (Either Blocker [Candidate])
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM (Either Blocker [Candidate]))
-> TypeError -> TCM (Either Blocker [Candidate])
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError (String -> TypeError) -> String -> TypeError
forall a b. (a -> b) -> a -> b
$
      String
"Instance search can only be used to find elements in a named type"
    OutputTypeNameNotYetKnown Blocker
b -> do
      String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.instance.cands" VerboseLevel
30 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Instance type is not yet known. "
      Either Blocker [Candidate] -> TCM (Either Blocker [Candidate])
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocker -> Either Blocker [Candidate]
forall a b. a -> Either a b
Left Blocker
b)
    OutputTypeName
OutputTypeVisiblePi -> TypeError -> TCM (Either Blocker [Candidate])
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM (Either Blocker [Candidate]))
-> TypeError -> TCM (Either Blocker [Candidate])
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError (String -> TypeError) -> String -> TypeError
forall a b. (a -> b) -> a -> b
$
      String
"Instance search cannot be used to find elements in an explicit function type"
    OutputTypeName
OutputTypeVar    -> do
      String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.instance.cands" VerboseLevel
30 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Instance type is a variable. "
      BlockT TCM [Candidate] -> TCM (Either Blocker [Candidate])
forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked BlockT TCM [Candidate]
getContextVars
    OutputTypeName QName
n -> do
      String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.instance.cands" VerboseLevel
30 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Found instance type head: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
n
      BlockT TCM [Candidate] -> TCM (Either Blocker [Candidate])
forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked BlockT TCM [Candidate]
getContextVars TCM (Either Blocker [Candidate])
-> (Either Blocker [Candidate] -> TCM (Either Blocker [Candidate]))
-> TCM (Either Blocker [Candidate])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Left Blocker
b -> Either Blocker [Candidate] -> TCM (Either Blocker [Candidate])
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Blocker [Candidate] -> TCM (Either Blocker [Candidate]))
-> Either Blocker [Candidate] -> TCM (Either Blocker [Candidate])
forall a b. (a -> b) -> a -> b
$ Blocker -> Either Blocker [Candidate]
forall a b. a -> Either a b
Left Blocker
b
        Right [Candidate]
ctxVars -> [Candidate] -> Either Blocker [Candidate]
forall a b. b -> Either a b
Right ([Candidate] -> Either Blocker [Candidate])
-> ([Candidate] -> [Candidate])
-> [Candidate]
-> Either Blocker [Candidate]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Candidate]
ctxVars [Candidate] -> [Candidate] -> [Candidate]
forall a. [a] -> [a] -> [a]
++) ([Candidate] -> Either Blocker [Candidate])
-> TCMT IO [Candidate] -> TCM (Either Blocker [Candidate])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO [Candidate]
getScopeDefs QName
n
  where
    -- get a list of variables with their type, relative to current context
    getContextVars :: BlockT TCM [Candidate]
    getContextVars :: BlockT TCM [Candidate]
getContextVars = do
      [Dom (Name, Type)]
ctx <- BlockT TCM [Dom (Name, Type)]
forall (m :: * -> *). MonadTCEnv m => m [Dom (Name, Type)]
getContext
      String -> VerboseLevel -> TCM Doc -> BlockT TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.instance.cands" VerboseLevel
40 (TCM Doc -> BlockT TCM ()) -> TCM Doc -> BlockT TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc -> VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *).
Applicative m =>
m Doc -> VerboseLevel -> m Doc -> m Doc
hang TCM Doc
"Getting candidates from context" VerboseLevel
2 (TCM Doc -> TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ PrettyContext -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (PrettyContext -> TCM Doc) -> PrettyContext -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [Dom (Name, Type)] -> PrettyContext
PrettyContext [Dom (Name, Type)]
ctx)
          -- Context variables with their types lifted to live in the full context
      let varsAndRaisedTypes :: [(Term, Dom (Name, Type))]
varsAndRaisedTypes = [ (VerboseLevel -> Term
var VerboseLevel
i, VerboseLevel -> Dom (Name, Type) -> Dom (Name, Type)
forall a. Subst a => VerboseLevel -> a -> a
raise (VerboseLevel
i VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ VerboseLevel
1) Dom (Name, Type)
t) | (VerboseLevel
i, Dom (Name, Type)
t) <- [VerboseLevel]
-> [Dom (Name, Type)] -> [(VerboseLevel, Dom (Name, Type))]
forall a b. [a] -> [b] -> [(a, b)]
zip [VerboseLevel
0..] [Dom (Name, Type)]
ctx ]
          vars :: [Candidate]
vars = [ CandidateKind -> Term -> Type -> Bool -> Candidate
Candidate CandidateKind
LocalCandidate Term
x Type
t (ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
isOverlappable ArgInfo
info)
                 | (Term
x, Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info, unDom :: forall t e. Dom' t e -> e
unDom = (Name
_, Type
t)}) <- [(Term, Dom (Name, Type))]
varsAndRaisedTypes
                 , ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
isInstance ArgInfo
info
                 ]

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

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

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

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

    instanceFields' :: Bool -> (CandidateKind,Term,Type) -> BlockT TCM [Candidate]
    instanceFields' :: Bool -> (CandidateKind, Term, Type) -> BlockT TCM [Candidate]
instanceFields' Bool
etaOnce (CandidateKind
q, Term
v, Type
t) =
      Type
-> (Blocker -> Type -> BlockT TCM [Candidate])
-> (NotBlocked -> Type -> BlockT TCM [Candidate])
-> BlockT TCM [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 TCM [Candidate]
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
m) ((NotBlocked -> Type -> BlockT TCM [Candidate])
 -> BlockT TCM [Candidate])
-> (NotBlocked -> Type -> BlockT TCM [Candidate])
-> BlockT TCM [Candidate]
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Type
t -> do
      BlockT TCM (Maybe (QName, Args))
-> BlockT TCM [Candidate]
-> ((QName, Args) -> BlockT TCM [Candidate])
-> BlockT TCM [Candidate]
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Bool -> Type -> BlockT TCM (Maybe (QName, Args))
forall (m :: * -> *).
(MonadTCM m, PureTCM m) =>
Bool -> Type -> m (Maybe (QName, Args))
etaExpand Bool
etaOnce Type
t) ([Candidate] -> BlockT TCM [Candidate]
forall (m :: * -> *) a. Monad m => a -> m a
return []) (((QName, Args) -> BlockT TCM [Candidate])
 -> BlockT TCM [Candidate])
-> ((QName, Args) -> BlockT TCM [Candidate])
-> BlockT TCM [Candidate]
forall a b. (a -> b) -> a -> b
$ \ (QName
r, Args
pars) -> do
        (Telescope
tel, Args
args) <- TCM (Telescope, Args) -> BlockT TCM (Telescope, Args)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (Telescope, Args) -> BlockT TCM (Telescope, Args))
-> TCM (Telescope, Args) -> BlockT TCM (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 ([Term] -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> Substitution' Term) -> [Term] -> Substitution' Term
forall a b. (a -> b) -> a -> b
$ [Term] -> [Term]
forall a. [a] -> [a]
reverse ([Term] -> [Term]) -> [Term] -> [Term]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Term) -> Args -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg Args
args) (Telescope -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
tel)
        ([[Candidate]] -> [Candidate])
-> BlockT TCM [[Candidate]] -> BlockT TCM [Candidate]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[Candidate]] -> [Candidate]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (BlockT TCM [[Candidate]] -> BlockT TCM [Candidate])
-> BlockT TCM [[Candidate]] -> BlockT TCM [Candidate]
forall a b. (a -> b) -> a -> b
$ [(Arg Term, Type)]
-> ((Arg Term, Type) -> BlockT TCM [Candidate])
-> BlockT TCM [[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 TCM [Candidate])
 -> BlockT TCM [[Candidate]])
-> ((Arg Term, Type) -> BlockT TCM [Candidate])
-> BlockT TCM [[Candidate]]
forall a b. (a -> b) -> a -> b
$ \ (Arg Term
arg, Type
t) ->
          ([ CandidateKind -> Term -> Type -> Bool -> Candidate
Candidate CandidateKind
LocalCandidate (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
arg) Type
t (Arg Term -> Bool
forall a. LensHiding a => a -> Bool
isOverlappable Arg Term
arg)
           | Arg Term -> Bool
forall a. LensHiding a => a -> Bool
isInstance Arg Term
arg ] [Candidate] -> [Candidate] -> [Candidate]
forall a. [a] -> [a] -> [a]
++) ([Candidate] -> [Candidate])
-> BlockT TCM [Candidate] -> BlockT TCM [Candidate]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
          Bool -> (CandidateKind, Term, Type) -> BlockT TCM [Candidate]
instanceFields' Bool
False (CandidateKind
LocalCandidate, Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
arg, Type
t)

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

    candidate :: Relevance -> QName -> TCM (Maybe Candidate)
    candidate :: Relevance -> QName -> TCMT IO (Maybe Candidate)
candidate Relevance
rel QName
q = TCMT IO Bool
-> TCMT IO (Maybe Candidate)
-> TCMT IO (Maybe Candidate)
-> TCMT IO (Maybe Candidate)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (QName -> ScopeInfo -> Bool
isNameInScope QName
q (ScopeInfo -> Bool) -> TCMT IO ScopeInfo -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope) (Maybe Candidate -> TCMT IO (Maybe Candidate)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Candidate
forall a. Maybe a
Nothing) (TCMT IO (Maybe Candidate) -> TCMT IO (Maybe Candidate))
-> TCMT IO (Maybe Candidate) -> TCMT IO (Maybe Candidate)
forall a b. (a -> b) -> a -> b
$ do
      -- Jesper, 2020-03-16: When using --no-qualified-instances,
      -- filter out instances that are only in scope under a qualified
      -- name.
      TCMT IO (Maybe Candidate) -> TCMT IO (Maybe Candidate)
filterQualified (TCMT IO (Maybe Candidate) -> TCMT IO (Maybe Candidate))
-> TCMT IO (Maybe Candidate) -> TCMT IO (Maybe Candidate)
forall a b. (a -> b) -> a -> b
$ do
      -- Andreas, 2012-07-07:
      -- we try to get the info for q
      -- while opening a module, q may be in scope but not in the signature
      -- in this case, we just ignore q (issue 674)
      (TCMT IO (Maybe Candidate)
 -> (TCErr -> TCMT IO (Maybe Candidate))
 -> TCMT IO (Maybe Candidate))
-> (TCErr -> TCMT IO (Maybe Candidate))
-> TCMT IO (Maybe Candidate)
-> TCMT IO (Maybe Candidate)
forall a b c. (a -> b -> c) -> b -> a -> c
flip TCMT IO (Maybe Candidate)
-> (TCErr -> TCMT IO (Maybe Candidate))
-> TCMT IO (Maybe Candidate)
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError TCErr -> TCMT IO (Maybe Candidate)
forall (m :: * -> *) a. MonadError TCErr m => TCErr -> m (Maybe a)
handle (TCMT IO (Maybe Candidate) -> TCMT IO (Maybe Candidate))
-> TCMT IO (Maybe Candidate) -> TCMT IO (Maybe Candidate)
forall a b. (a -> b) -> a -> b
$ do
        Definition
def <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
        if Bool -> Bool
not (Definition -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Definition
def Relevance -> Relevance -> Bool
`moreRelevant` Relevance
rel) then Maybe Candidate -> TCMT IO (Maybe Candidate)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Candidate
forall a. Maybe a
Nothing else do
          -- Andreas, 2017-01-14: instantiateDef is a bit of an overkill
          -- if we anyway get the freeVarsToApply
          -- WAS: t <- defType <$> instantiateDef def
          Args
args <- QName -> TCMT IO Args
forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
QName -> m Args
freeVarsToApply QName
q
          let t :: Type
t = Definition -> Type
defType Definition
def Type -> Args -> Type
`piApply` Args
args
              rel :: Relevance
rel = ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance (ArgInfo -> Relevance) -> ArgInfo -> Relevance
forall a b. (a -> b) -> a -> b
$ Definition -> ArgInfo
defArgInfo Definition
def
          let v :: Term
v = case Definition -> Defn
theDef Definition
def of
               -- drop parameters if it's a projection function...
               Function{ funProjection :: Defn -> Maybe Projection
funProjection = Just Projection
p } -> Projection -> ProjOrigin -> Relevance -> Args -> Term
projDropParsApply Projection
p ProjOrigin
ProjSystem Relevance
rel Args
args
               -- Andreas, 2014-08-19: constructors cannot be declared as
               -- instances (at least as of now).
               -- I do not understand why the Constructor case is not impossible.
               -- Ulf, 2014-08-20: constructors are always instances.
               Constructor{ conSrcCon :: Defn -> ConHead
conSrcCon = ConHead
c }       -> ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ConOSystem []
               Defn
_                                  -> QName -> Elims -> Term
Def QName
q (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Args
args
          Maybe Candidate -> TCMT IO (Maybe Candidate)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Candidate -> TCMT IO (Maybe Candidate))
-> Maybe Candidate -> TCMT IO (Maybe Candidate)
forall a b. (a -> b) -> a -> b
$ Candidate -> Maybe Candidate
forall a. a -> Maybe a
Just (Candidate -> Maybe Candidate) -> Candidate -> Maybe Candidate
forall a b. (a -> b) -> a -> b
$ CandidateKind -> Term -> Type -> Bool -> Candidate
Candidate (QName -> CandidateKind
GlobalCandidate QName
q) Term
v Type
t Bool
False
      where
        -- unbound constant throws an internal error
        handle :: TCErr -> m (Maybe a)
handle (TypeError CallStack
_ TCState
_ (Closure {clValue :: forall a. Closure a -> a
clValue = InternalError String
_})) = Maybe a -> m (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
        handle TCErr
err                                                   = TCErr -> m (Maybe a)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err

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


-- | @findInstance m (v,a)s@ tries to instantiate on of the types @a@s
--   of the candidate terms @v@s to the type @t@ of the metavariable @m@.
--   If successful, meta @m@ is solved with the instantiation of @v@.
--   If unsuccessful, the constraint is regenerated, with possibly reduced
--   candidate set.
--   The list of candidates is equal to @Nothing@ when the type of the meta
--   wasn't known when the constraint was generated. In that case, try to find
--   its type again.
findInstance :: MetaId -> Maybe [Candidate] -> TCM ()
findInstance :: MetaId -> Maybe [Candidate] -> TCMT IO ()
findInstance MetaId
m Maybe [Candidate]
Nothing = do
  -- Andreas, 2015-02-07: New metas should be created with range of the
  -- current instance meta, thus, we set the range.
  MetaVariable
mv <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
  MetaVariable -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange MetaVariable
mv (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
    String -> VerboseLevel -> String -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"tc.instance" VerboseLevel
20 (String -> TCMT IO ()) -> String -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ String
"The type of the FindInstance constraint isn't known, trying to find it again."
    Type
t <- Type -> TCMT IO Type
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate (Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MetaId -> TCMT IO Type
forall (m :: * -> *).
(MonadFail m, MonadTCEnv m, ReadTCState m, MonadReduce m,
 HasBuiltins m) =>
MetaId -> m Type
getMetaTypeInContext MetaId
m
    String -> VerboseLevel -> String -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"tc.instance" VerboseLevel
70 (String -> TCMT IO ()) -> String -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ String
"findInstance 1: t: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Pretty a => a -> String
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 <- VerboseLevel -> (Dom Type -> Bool) -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
VerboseLevel -> (Dom Type -> Bool) -> Type -> m (TelV Type)
telViewUpTo' (-VerboseLevel
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
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
$ Type -> TCM (Either Blocker [Candidate])
initialInstanceCandidates Type
t
    case Either Blocker [Candidate]
cands of
      Left Blocker
unblock -> do
        String -> VerboseLevel -> String -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"tc.instance" VerboseLevel
20 String
"Can't figure out target of instance goal. Postponing constraint."
        Blocker -> Constraint -> TCMT IO ()
forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint Blocker
unblock (Constraint -> TCMT IO ()) -> Constraint -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ MetaId -> Maybe [Candidate] -> Constraint
FindInstance MetaId
m Maybe [Candidate]
forall a. Maybe a
Nothing
      Right [Candidate]
cs -> MetaId -> Maybe [Candidate] -> TCMT IO ()
findInstance MetaId
m ([Candidate] -> Maybe [Candidate]
forall a. a -> Maybe a
Just [Candidate]
cs)

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

-- | Result says whether we need to add constraint, and if so, the set of
--   remaining candidates and an eventual blocking metavariable.
findInstance' :: MetaId -> [Candidate] -> TCM (Maybe ([Candidate], Blocker))
findInstance' :: MetaId -> [Candidate] -> TCMT IO (Maybe ([Candidate], Blocker))
findInstance' MetaId
m [Candidate]
cands = TCMT IO Bool
-> TCMT IO (Maybe ([Candidate], Blocker))
-> TCMT IO (Maybe ([Candidate], Blocker))
-> TCMT IO (Maybe ([Candidate], Blocker))
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (MetaId -> TCMT IO Bool
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
m) (do
    String -> VerboseLevel -> String -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"tc.instance" VerboseLevel
20 String
"Refusing to solve frozen instance meta."
    Maybe ([Candidate], Blocker)
-> TCMT IO (Maybe ([Candidate], Blocker))
forall (m :: * -> *) a. Monad m => a -> m a
return (([Candidate], Blocker) -> Maybe ([Candidate], Blocker)
forall a. a -> Maybe a
Just ([Candidate]
cands, Blocker
neverUnblock))) (TCMT IO (Maybe ([Candidate], Blocker))
 -> TCMT IO (Maybe ([Candidate], Blocker)))
-> TCMT IO (Maybe ([Candidate], Blocker))
-> TCMT IO (Maybe ([Candidate], Blocker))
forall a b. (a -> b) -> a -> b
$ do
  TCMT IO Bool
-> TCMT IO (Maybe ([Candidate], Blocker))
-> TCMT IO (Maybe ([Candidate], Blocker))
-> TCMT IO (Maybe ([Candidate], Blocker))
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM TCMT IO Bool
forall (m :: * -> *). (ReadTCState m, HasOptions m) => m Bool
shouldPostponeInstanceSearch (do
    String -> VerboseLevel -> String -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"tc.instance" VerboseLevel
20 String
"Postponing possibly recursive instance search."
    Maybe ([Candidate], Blocker)
-> TCMT IO (Maybe ([Candidate], Blocker))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([Candidate], Blocker)
 -> TCMT IO (Maybe ([Candidate], Blocker)))
-> Maybe ([Candidate], Blocker)
-> TCMT IO (Maybe ([Candidate], Blocker))
forall a b. (a -> b) -> a -> b
$ ([Candidate], Blocker) -> Maybe ([Candidate], Blocker)
forall a. a -> Maybe a
Just ([Candidate]
cands, Blocker
neverUnblock)) (TCMT IO (Maybe ([Candidate], Blocker))
 -> TCMT IO (Maybe ([Candidate], Blocker)))
-> TCMT IO (Maybe ([Candidate], Blocker))
-> TCMT IO (Maybe ([Candidate], Blocker))
forall a b. (a -> b) -> a -> b
$ Account (BenchPhase TCM)
-> TCMT IO (Maybe ([Candidate], Blocker))
-> TCMT IO (Maybe ([Candidate], Blocker))
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
billTo [BenchPhase TCM
Phase
Benchmark.Typing, BenchPhase TCM
Phase
Benchmark.InstanceSearch] (TCMT IO (Maybe ([Candidate], Blocker))
 -> TCMT IO (Maybe ([Candidate], Blocker)))
-> TCMT IO (Maybe ([Candidate], Blocker))
-> TCMT IO (Maybe ([Candidate], Blocker))
forall a b. (a -> b) -> a -> b
$ do
  -- Andreas, 2015-02-07: New metas should be created with range of the
  -- current instance meta, thus, we set the range.
  MetaVariable
mv <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
  MetaVariable
-> TCMT IO (Maybe ([Candidate], Blocker))
-> TCMT IO (Maybe ([Candidate], Blocker))
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange MetaVariable
mv (TCMT IO (Maybe ([Candidate], Blocker))
 -> TCMT IO (Maybe ([Candidate], Blocker)))
-> TCMT IO (Maybe ([Candidate], Blocker))
-> TCMT IO (Maybe ([Candidate], Blocker))
forall a b. (a -> b) -> a -> b
$ do
      String -> VerboseLevel -> String -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"tc.instance" VerboseLevel
15 (String -> TCMT IO ()) -> String -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
        String
"findInstance 2: constraint: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ MetaId -> String
forall a. Pretty a => a -> String
prettyShow MetaId
m String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"; candidates left: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> String
forall a. Show a => a -> String
show ([Candidate] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Candidate]
cands)
      String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.instance" VerboseLevel
60 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ (if Bool
overlap then TCM Doc
"overlap" else TCM Doc
forall a. Null a => a
empty) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Candidate -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Candidate
c TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":"
              , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t ] | c :: Candidate
c@(Candidate CandidateKind
q Term
v Type
t Bool
overlap) <- [Candidate]
cands ]
      String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.instance" VerboseLevel
70 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"raw" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ do
       VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ (if Bool
overlap then TCM Doc
"overlap" else TCM Doc
forall a. Null a => a
empty) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Candidate -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Candidate
c TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":"
              , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
t ] | c :: Candidate
c@(Candidate CandidateKind
q Term
v Type
t Bool
overlap) <- [Candidate]
cands ]
      Type
t <- MetaId -> TCMT IO Type
forall (m :: * -> *).
(MonadFail m, MonadTCEnv m, ReadTCState m, MonadReduce m,
 HasBuiltins m) =>
MetaId -> m Type
getMetaTypeInContext MetaId
m
      String -> VerboseLevel -> String -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"tc.instance" VerboseLevel
70 (String -> TCMT IO ()) -> String -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ String
"findInstance 2: t: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Pretty a => a -> String
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
      String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.instance" VerboseLevel
15 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"findInstance 3: t =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
      String -> VerboseLevel -> String -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"tc.instance" VerboseLevel
70 (String -> TCMT IO ()) -> String -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ String
"findInstance 3: t: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Pretty a => a -> String
prettyShow Type
t

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

      TCMT IO ()
debugConstraints
      case Maybe ([(Candidate, TCErr)], [Candidate])
mcands of

        Just ([(Candidate
_, TCErr
err)], []) -> do
          String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.instance" VerboseLevel
15 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
            TCM Doc
"findInstance 5: the only viable candidate failed..."
          TCErr -> TCMT IO (Maybe ([Candidate], Blocker))
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
        Just ([(Candidate, TCErr)]
errs, []) -> do
          if [(Candidate, TCErr)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Candidate, TCErr)]
errs then String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.instance" VerboseLevel
15 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"findInstance 5: no viable candidate found..."
                       else String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.instance" VerboseLevel
15 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM 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 (VerboseLevel -> [TCErr] -> [TCErr]
forall a. VerboseLevel -> [a] -> [a]
take VerboseLevel
1 ([TCErr] -> [TCErr]) -> [TCErr] -> [TCErr]
forall a b. (a -> b) -> a -> b
$ ((Candidate, TCErr) -> TCErr) -> [(Candidate, TCErr)] -> [TCErr]
forall a b. (a -> b) -> [a] -> [b]
map (Candidate, TCErr) -> TCErr
forall a b. (a, b) -> b
snd [(Candidate, TCErr)]
sortedErrs) (TCMT IO (Maybe ([Candidate], Blocker))
 -> TCMT IO (Maybe ([Candidate], Blocker)))
-> TCMT IO (Maybe ([Candidate], Blocker))
-> TCMT IO (Maybe ([Candidate], Blocker))
forall a b. (a -> b) -> a -> b
$
            TypeError -> TCMT IO (Maybe ([Candidate], Blocker))
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO (Maybe ([Candidate], Blocker)))
-> TypeError -> TCMT IO (Maybe ([Candidate], Blocker))
forall a b. (a -> b) -> a -> b
$ Type -> [(Term, TCErr)] -> TypeError
InstanceNoCandidate Type
t [ (Candidate -> Term
candidateTerm Candidate
c, TCErr
err) | (Candidate
c, TCErr
err) <- [(Candidate, TCErr)]
sortedErrs ]

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

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

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

insidePi :: Type -> (Type -> TCM a) -> TCM a
insidePi :: Type -> (Type -> TCM a) -> TCM a
insidePi Type
t Type -> TCM a
ret = Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type -> Term
forall t a. Type'' t a -> a
unEl Type
t) TCMT IO Term -> (Term -> TCM a) -> TCM a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Pi Dom Type
a Abs Type
b     -> (String, Dom Type) -> TCM a -> TCM a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Abs Type -> String
forall a. Abs a -> String
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 String
s Elims
_  -> String -> TCM a
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ String
s

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

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

  -- c : Candidate
  -- r : YesNoMaybe
  -- v : Term         (fully instantiated)
  -- a : Type         (fully instantiated)
  -- s : TCState
  let result' :: [(Candidate, Term, TCState)]
result' = [ (Candidate
c, Term
v, TCState
s) | (Candidate
c, ((YesNoMaybe
r, Term
v), TCState
s)) <- [(Candidate, ((YesNoMaybe, Term), TCState))]
result, Bool -> Bool
not (YesNoMaybe -> Bool
isNo YesNoMaybe
r) ]
  [(Candidate, Term, TCState)]
result'' <- MetaId
-> [(Candidate, Term, TCState)] -> TCM [(Candidate, Term, TCState)]
forall a.
MetaId -> [(Candidate, Term, a)] -> TCM [(Candidate, Term, a)]
dropSameCandidates MetaId
m [(Candidate, Term, TCState)]
result'
  case [(Candidate, Term, TCState)]
result'' of
    [(Candidate
c, Term
_, TCState
s)] -> ([], [Candidate
c]) ([(Candidate, TCErr)], [Candidate])
-> TCMT IO () -> TCM ([(Candidate, TCErr)], [Candidate])
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ TCState -> TCMT IO ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
s
    [(Candidate, Term, TCState)]
_           -> do
      let bad :: [(Candidate, TCErr)]
bad  = [ (Candidate
c, TCErr
err) | (Candidate
c, ((NoBecause TCErr
err, Term
_), TCState
_)) <- [(Candidate, ((YesNoMaybe, Term), TCState))]
result ]
          good :: [Candidate]
good = [ Candidate
c | (Candidate
c, Term
_, TCState
_) <- [(Candidate, Term, TCState)]
result'' ]
      ([(Candidate, TCErr)], [Candidate])
-> TCM ([(Candidate, TCErr)], [Candidate])
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Candidate, TCErr)]
bad, [Candidate]
good)

-- Drop all candidates which are judgmentally equal to the first one.
-- This is sufficient to reduce the list to a singleton should all be equal.
dropSameCandidates :: MetaId -> [(Candidate, Term, a)] -> TCM [(Candidate, Term, a)]
dropSameCandidates :: MetaId -> [(Candidate, Term, a)] -> TCM [(Candidate, Term, a)]
dropSameCandidates MetaId
m [(Candidate, Term, a)]
cands0 = String
-> VerboseLevel
-> String
-> TCM [(Candidate, Term, a)]
-> TCM [(Candidate, Term, a)]
forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> String -> m a -> m a
verboseBracket String
"tc.instance" VerboseLevel
30 String
"dropSameCandidates" (TCM [(Candidate, Term, a)] -> TCM [(Candidate, Term, a)])
-> TCM [(Candidate, Term, a)] -> TCM [(Candidate, Term, a)]
forall a b. (a -> b) -> a -> b
$ do
  MetaStore
metas <- TCMT IO MetaStore
forall (m :: * -> *). ReadTCState m => m MetaStore
getMetaStore
  -- Does `it` have any metas in the initial meta variable store?
  let freshMetas :: Term -> Bool
freshMetas = Any -> Bool
getAny (Any -> Bool) -> (Term -> Any) -> Term -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MetaId -> Any) -> Term -> Any
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas (Bool -> Any
Any (Bool -> Any) -> (MetaId -> Bool) -> MetaId -> Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VerboseLevel -> MetaStore -> Bool
forall a. VerboseLevel -> IntMap a -> Bool
`IntMap.notMember` MetaStore
metas) (VerboseLevel -> Bool)
-> (MetaId -> VerboseLevel) -> MetaId -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaId -> VerboseLevel
metaId)

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

  String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.instance" VerboseLevel
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCM Doc
"valid candidates:"
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ if Term -> Bool
freshMetas Term
v then TCM Doc
"(redacted)" else
                      [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v ]
                    | (Candidate
_, Term
v, a
_) <- [(Candidate, Term, a)]
cands ] ]
  Relevance
rel <- MetaVariable -> Relevance
getMetaRelevance (MetaVariable -> Relevance)
-> TCMT IO MetaVariable -> TCMT IO Relevance
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
  case [(Candidate, Term, a)]
cands of
    []            -> [(Candidate, Term, a)] -> TCM [(Candidate, Term, a)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Candidate, Term, a)]
cands
    (Candidate, Term, a)
cvd : [(Candidate, Term, a)]
_ | Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
rel -> do
      String -> VerboseLevel -> String -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"tc.instance" VerboseLevel
30 String
"dropSameCandidates: Meta is irrelevant so any candidate will do."
      [(Candidate, Term, a)] -> TCM [(Candidate, Term, a)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Candidate, Term, a)
cvd]
    (Candidate
_, MetaV MetaId
m' Elims
_, a
_) : [(Candidate, Term, a)]
_ | MetaId
m MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
m' -> do  -- We didn't instantiate, so can't compare
      String -> VerboseLevel -> String -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"tc.instance" VerboseLevel
30 String
"dropSameCandidates: Meta was not instantiated so we don't filter equal candidates yet"
      [(Candidate, Term, a)] -> TCM [(Candidate, Term, a)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Candidate, Term, a)]
cands
    cvd :: (Candidate, Term, a)
cvd@(Candidate
_, Term
v, a
_) : [(Candidate, Term, a)]
vas
      | Term -> Bool
freshMetas Term
v -> do
          String -> VerboseLevel -> String -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"tc.instance" VerboseLevel
30 String
"dropSameCandidates: Solution of instance meta has fresh metas so we don't filter equal candidates yet"
          [(Candidate, Term, a)] -> TCM [(Candidate, Term, a)]
forall (m :: * -> *) a. Monad m => a -> m a
return ((Candidate, Term, a)
cvd (Candidate, Term, a)
-> [(Candidate, Term, a)] -> [(Candidate, Term, a)]
forall a. a -> [a] -> [a]
: [(Candidate, Term, a)]
vas)
      | Bool
otherwise -> ((Candidate, Term, a)
cvd (Candidate, Term, a)
-> [(Candidate, Term, a)] -> [(Candidate, Term, a)]
forall a. a -> [a] -> [a]
:) ([(Candidate, Term, a)] -> [(Candidate, Term, a)])
-> TCM [(Candidate, Term, a)] -> TCM [(Candidate, Term, a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Candidate, Term, a) -> TCMT IO Bool)
-> [(Candidate, Term, a)] -> TCM [(Candidate, Term, a)]
forall (m :: * -> *) a. Monad m => (a -> m Bool) -> [a] -> m [a]
dropWhileM (Candidate, Term, a) -> TCMT IO Bool
forall a. (Candidate, Term, a) -> TCMT IO Bool
equal [(Candidate, Term, a)]
vas
      where
        equal :: (Candidate, Term, a) -> TCM Bool
        equal :: (Candidate, Term, a) -> TCMT IO Bool
equal (Candidate
_, Term
v', a
_)
            | Term -> Bool
freshMetas Term
v' = Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False  -- If there are fresh metas we can't compare
            | Bool
otherwise     =
          String -> VerboseLevel -> String -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> String -> m a -> m a
verboseBracket String
"tc.instance" VerboseLevel
30 String
"dropSameCandidates: " (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ do
          String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.instance" VerboseLevel
30 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"==", VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v' ]
          Type
a <- (Type -> Args -> TCMT IO Type) -> (Type, Args) -> TCMT IO Type
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Type -> Args -> TCMT IO Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
piApplyM ((Type, Args) -> TCMT IO Type)
-> TCMT IO (Type, Args) -> TCMT IO Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ((,) (Type -> Args -> (Type, Args))
-> TCMT IO Type -> TCMT IO (Args -> (Type, Args))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO Type
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
getMetaType MetaId
m TCMT IO (Args -> (Type, Args))
-> TCMT IO Args -> TCMT IO (Type, Args)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TCMT IO Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs)
          TCMT IO Bool -> TCMT IO Bool
forall a. TCM a -> TCM a
localTCState (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
dontAssignMetas (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ TCMT IO ()
-> TCMT IO Bool -> (ProblemId -> TCMT IO Bool) -> TCMT IO Bool
forall a. TCMT IO () -> TCM a -> (ProblemId -> TCM a) -> TCM a
ifNoConstraints_ (Type -> Term -> Term -> TCMT IO ()
forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
a Term
v Term
v')
                             {- then -} (Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
                             {- else -} (\ ProblemId
_ -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False)
                             TCMT IO Bool -> (TCErr -> TCMT IO Bool) -> TCMT IO Bool
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` (\ TCErr
_ -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False)

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

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

-- | Given a meta @m@ of type @t@ and a list of candidates @cands@,
-- @checkCandidates m t cands@ returns a refined list of valid candidates and
-- candidates that failed some constraints.
checkCandidates :: MetaId -> Type -> [Candidate] -> TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
checkCandidates :: MetaId
-> Type
-> [Candidate]
-> TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
checkCandidates MetaId
m Type
t [Candidate]
cands =
  String
-> VerboseLevel
-> String
-> TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
-> TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> String -> m a -> m a
verboseBracket String
"tc.instance.candidates" VerboseLevel
20 (String
"checkCandidates " String -> String -> String
forall a. [a] -> [a] -> [a]
++ MetaId -> String
forall a. Pretty a => a -> String
prettyShow MetaId
m) (TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
 -> TCM (Maybe ([(Candidate, TCErr)], [Candidate])))
-> TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
-> TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
forall a b. (a -> b) -> a -> b
$
  TCMT IO Bool
-> TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
-> TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
-> TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ([Candidate] -> TCMT IO Bool
anyMetaTypes [Candidate]
cands) (Maybe ([(Candidate, TCErr)], [Candidate])
-> TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ([(Candidate, TCErr)], [Candidate])
forall a. Maybe a
Nothing) (TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
 -> TCM (Maybe ([(Candidate, TCErr)], [Candidate])))
-> TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
-> TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
forall a b. (a -> b) -> a -> b
$ ([(Candidate, TCErr)], [Candidate])
-> Maybe ([(Candidate, TCErr)], [Candidate])
forall a. a -> Maybe a
Just (([(Candidate, TCErr)], [Candidate])
 -> Maybe ([(Candidate, TCErr)], [Candidate]))
-> TCM ([(Candidate, TCErr)], [Candidate])
-> TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.instance.candidates" VerboseLevel
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"target:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
    String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.instance.candidates" VerboseLevel
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCM Doc
"candidates"
      , [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCM Doc
"-" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (if Bool
overlap then TCM Doc
"overlap" else TCM Doc
forall a. Null a => a
empty) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Candidate -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Candidate
c TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
             | c :: Candidate
c@(Candidate CandidateKind
q Term
v Type
t Bool
overlap) <- [Candidate]
cands ] ]
    ([(Candidate, TCErr)], [Candidate])
cands' <- MetaId
-> [Candidate]
-> (Candidate -> TCM YesNoMaybe)
-> TCM ([(Candidate, TCErr)], [Candidate])
filterResetingState MetaId
m [Candidate]
cands (MetaId -> Type -> Candidate -> TCM YesNoMaybe
checkCandidateForMeta MetaId
m Type
t)
    String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.instance.candidates" VerboseLevel
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCM Doc
"valid candidates"
      , [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCM Doc
"-" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (if Bool
overlap then TCM Doc
"overlap" else TCM Doc
forall a. Null a => a
empty) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Candidate -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Candidate
c TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
             | c :: Candidate
c@(Candidate CandidateKind
q Term
v Type
t Bool
overlap) <- ([(Candidate, TCErr)], [Candidate]) -> [Candidate]
forall a b. (a, b) -> b
snd ([(Candidate, TCErr)], [Candidate])
cands' ] ]
    String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.instance.candidates" VerboseLevel
60 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCM Doc
"valid candidates"
      , [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCM Doc
"-" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (if Bool
overlap then TCM Doc
"overlap" else TCM Doc
forall a. Null a => a
empty) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
             | c :: Candidate
c@(Candidate CandidateKind
q Term
v Type
t Bool
overlap) <- ([(Candidate, TCErr)], [Candidate]) -> [Candidate]
forall a b. (a, b) -> b
snd ([(Candidate, TCErr)], [Candidate])
cands' ] ]
    ([(Candidate, TCErr)], [Candidate])
-> TCM ([(Candidate, TCErr)], [Candidate])
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Candidate, TCErr)], [Candidate])
cands'
  where
    anyMetaTypes :: [Candidate] -> TCM Bool
    anyMetaTypes :: [Candidate] -> TCMT IO Bool
anyMetaTypes [] = Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    anyMetaTypes (Candidate CandidateKind
_ Term
_ Type
a Bool
_ : [Candidate]
cands) = do
      Type
a <- Type -> TCMT IO Type
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Type
a
      case Type -> Term
forall t a. Type'' t a -> a
unEl Type
a of
        MetaV{} -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        Term
_       -> [Candidate] -> TCMT IO Bool
anyMetaTypes [Candidate]
cands

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

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

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

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

            let debugSolution :: TCMT IO ()
debugSolution = String -> VerboseLevel -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> m () -> m ()
verboseS String
"tc.instance" VerboseLevel
15 (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
                  Term
sol <- Term -> TCMT IO Term
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull (MetaId -> Elims -> Term
MetaV MetaId
m Elims
ctxElims)
                  case Term
sol of
                    MetaV MetaId
m' Elims
_ | MetaId
m MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
m' ->
                      String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.instance" VerboseLevel
15 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
                        [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ (TCM Doc
"instance search: maybe solution for" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
m) TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> TCM Doc
":"
                            , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v ]
                    Term
_ ->
                      String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.instance" VerboseLevel
15 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
                        [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ (TCM Doc
"instance search: found solution for" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
m) TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> TCM Doc
":"
                            , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
sol ]

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

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

          debugSuccess :: TCMT IO ()
debugSuccess            = String -> VerboseLevel -> String -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"tc.instance" VerboseLevel
50 String
"assignment successful" :: TCM ()
          debugInconclusive :: TCMT IO ()
debugInconclusive       = String -> VerboseLevel -> String -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"tc.instance" VerboseLevel
50 String
"assignment inconclusive" :: TCM ()
          debugConstraintFail :: a -> m ()
debugConstraintFail a
why = String -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.instance" VerboseLevel
50 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"candidate failed constraints:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
why
          debugTypeFail :: a -> m ()
debugTypeFail a
err       = String -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.instance" VerboseLevel
50 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"candidate failed type check:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
err

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

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

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

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

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

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

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

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

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