{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.InstanceArguments
  ( findInstance
  , isInstanceConstraint
  , shouldPostponeInstanceSearch
  , postponeInstanceConstraints
  , getInstanceCandidates
  ) 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.Map.Strict as MapS
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
  (Tele (Dom' Term Type)
_ , OutputTypeName
otn) <- Type -> TCM (Tele (Dom' Term Type), OutputTypeName)
getOutputTypeName Type
t
  case OutputTypeName
otn of
    OutputTypeName
NoOutputTypeName -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$
      [Char]
"Instance search can only be used to find elements in a named type"
    OutputTypeNameNotYetKnown Blocker
b -> do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.cands" Int
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Instance type is not yet known. "
      forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. a -> Either a b
Left Blocker
b)
    OutputTypeName
OutputTypeVisiblePi -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$
      [Char]
"Instance search cannot be used to find elements in an explicit function type"
    OutputTypeName
OutputTypeVar    -> do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.cands" Int
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Instance type is a variable. "
      forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked BlockT (TCMT IO) [Candidate]
getContextVars
    OutputTypeName QName
n -> do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.cands" Int
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Found instance type head: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
n
      forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked BlockT (TCMT IO) [Candidate]
getContextVars forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Left Blocker
b -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left Blocker
b
        Right [Candidate]
ctxVars -> forall a b. b -> Either a b
Right forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Candidate]
ctxVars forall a. [a] -> [a] -> [a]
++) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCM [Candidate]
getScopeDefs QName
n
  where
    -- get a list of variables with their type, relative to current context
    getContextVars :: BlockT TCM [Candidate]
    getContextVars :: BlockT (TCMT IO) [Candidate]
getContextVars = do
      Context
ctx <- forall (m :: * -> *). MonadTCEnv m => m Context
getContext
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.cands" Int
40 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
Applicative m =>
m Doc -> Int -> m Doc -> m Doc
hang TCMT IO Doc
"Getting candidates from context" Int
2 (forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ Context -> PrettyContext
PrettyContext Context
ctx)
          -- Context variables with their types lifted to live in the full context
      let varsAndRaisedTypes :: [(Term, ContextEntry)]
varsAndRaisedTypes = [ (Int -> Term
var Int
i, forall a. Subst a => Int -> a -> a
raise (Int
i forall a. Num a => a -> a -> a
+ Int
1) ContextEntry
t) | (Int
i, ContextEntry
t) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] Context
ctx ]
          vars :: [Candidate]
vars = [ CandidateKind -> Term -> Type -> Bool -> Candidate
Candidate CandidateKind
LocalCandidate Term
x Type
t (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, ContextEntry)]
varsAndRaisedTypes
                 , forall a. LensHiding a => a -> Bool
isInstance ArgInfo
info
                 ]

      -- {{}}-fields of variables are also candidates
      let cxtAndTypes :: [(CandidateKind, Term, Type)]
cxtAndTypes = [ (CandidateKind
LocalCandidate, Term
x, Type
t) | (Term
x, Dom{unDom :: forall t e. Dom' t e -> e
unDom = (Name
_, Type
t)}) <- [(Term, ContextEntry)]
varsAndRaisedTypes ]
      [Candidate]
fields <- forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (CandidateKind, Term, Type) -> BlockT (TCMT IO) [Candidate]
instanceFields (forall a. [a] -> [a]
reverse [(CandidateKind, Term, Type)]
cxtAndTypes)
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.fields" Int
30 forall a b. (a -> b) -> a -> b
$
        if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Candidate]
fields then TCMT IO Doc
"no instance field candidates" else
          TCMT IO Doc
"instance field candidates" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ do
            forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ (if Bool
overlap then TCMT IO Doc
"overlap" else forall a. Null a => a
empty) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Candidate
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":"
                    , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ 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 <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> LetBindings
envLetBindings
      [(Name, (Term, Dom' Term Type))]
env <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a (m :: * -> *).
(TermSubst a, MonadTCEnv m) =>
Open a -> m a
getOpen) forall a b. (a -> b) -> a -> b
$ 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' Term Type))]
env
                 , forall a. LensHiding a => a -> Bool
isInstance ArgInfo
info
                 , forall a. LensModality a => a -> Bool
usableModality ArgInfo
info
                 ]
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Candidate]
vars forall a. [a] -> [a] -> [a]
++ [Candidate]
fields forall a. [a] -> [a] -> [a]
++ [Candidate]
lets

    etaExpand :: (MonadTCM m, PureTCM m)
              => Bool -> Type -> m (Maybe (QName, Args))
    etaExpand :: forall (m :: * -> *).
(MonadTCM m, PureTCM m) =>
Bool -> Type -> m (Maybe (QName, Args))
etaExpand Bool
etaOnce Type
t =
      forall (m :: * -> *).
HasConstInfo m =>
Type -> m (Maybe (QName, Args))
isEtaRecordType Type
t forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Maybe (QName, Args)
Nothing | Bool
etaOnce -> do
          forall (m :: * -> *).
PureTCM m =>
Type -> m (Maybe (QName, Args, Defn))
isRecordType Type
t forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            Maybe (QName, Args, Defn)
Nothing         -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
            Just (QName
r, Args
vs, Defn
_) -> do
              ModuleName
m <- 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 forall a. Eq a => [a] -> [a] -> Bool
`List.isPrefixOf` ModuleName -> [Name]
mnameToList ModuleName
m
                then forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just (QName
r, Args
vs))
                else forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
        Maybe (QName, Args)
r -> forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (QName, Args)
r

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

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

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

    candidate :: Relevance -> QName -> TCM (Maybe Candidate)
    candidate :: Relevance -> QName -> TCM (Maybe Candidate)
candidate Relevance
rel QName
q = forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (QName -> ScopeInfo -> Bool
isNameInScope QName
q forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope) (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing) forall a b. (a -> b) -> a -> b
$ do
      -- Jesper, 2020-03-16: When using --no-qualified-instances,
      -- filter out instances that are only in scope under a qualified
      -- name.
      TCM (Maybe Candidate) -> TCM (Maybe Candidate)
filterQualified 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)
      forall a b c. (a -> b -> c) -> b -> a -> c
flip forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError forall {m :: * -> *} {a}.
MonadError TCErr m =>
TCErr -> m (Maybe a)
handle forall a b. (a -> b) -> a -> b
$ do
        Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
        if Bool -> Bool
not (forall a. LensRelevance a => a -> Relevance
getRelevance Definition
def Relevance -> Relevance -> Bool
`moreRelevant` Relevance
rel) then forall (m :: * -> *) a. Monad m => a -> m a
return 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 <- 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 = forall a. LensRelevance a => a -> Relevance
getRelevance 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 -> Either ProjectionLikenessMissing Projection
funProjection = Right Projection
p } -> Projection -> ProjOrigin -> Relevance -> Args -> Term
projDropParsApply Projection
p ProjOrigin
ProjSystem Relevance
rel Args
args
               -- Andreas, 2014-08-19: constructors cannot be declared as
               -- instances (at least as of now).
               -- I do not understand why the Constructor case is not impossible.
               -- Ulf, 2014-08-20: constructors are always instances.
               Constructor{ conSrcCon :: Defn -> ConHead
conSrcCon = ConHead
c }       -> ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ConOSystem []
               Defn
_                                  -> QName -> Elims -> Term
Def QName
q forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply Args
args
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just 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 [Char]
_})) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
        handle TCErr
err                                                   = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err

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


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

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

-- | Entry point for `tcGetInstances` primitive
getInstanceCandidates :: MetaId -> TCM (Either Blocker [Candidate])
getInstanceCandidates :: MetaId -> TCM (Either Blocker [Candidate])
getInstanceCandidates MetaId
m = do
  MetaVariable
mv <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
  forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange MetaVariable
mv forall a b. (a -> b) -> a -> b
$ do
    Type
t <- forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(HasBuiltins m, HasCallStack, MonadDebug m, MonadReduce m,
 MonadTCEnv m, ReadTCState m) =>
MetaId -> m Type
getMetaTypeInContext MetaId
m
    TelV Tele (Dom' Term Type)
tel Type
t' <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> (Dom' Term Type -> Bool) -> Type -> m (TelV Type)
telViewUpTo' (-Int
1) forall a. LensHiding a => a -> Bool
notVisible Type
t
    forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom' Term Type)
tel forall a b. (a -> b) -> a -> b
$ Type -> TCM (Either Blocker [Candidate])
initialInstanceCandidates Type
t' forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Left Blocker
b -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left Blocker
b
      Right [Candidate]
cands -> MetaId
-> Type
-> [Candidate]
-> TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
checkCandidates MetaId
m Type
t' [Candidate]
cands forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Maybe ([(Candidate, TCErr)], [Candidate])
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right [Candidate]
cands
        Just ([(Candidate, TCErr)]
_ , [Candidate]
cands') -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right [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] -> TCM (Maybe ([Candidate], Blocker))
findInstance' MetaId
m [Candidate]
cands = forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
m) (do
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.instance" Int
20 [Char]
"Refusing to solve frozen instance meta."
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just ([Candidate]
cands, Blocker
neverUnblock))) forall a b. (a -> b) -> a -> b
$ do
  forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM forall (m :: * -> *). (ReadTCState m, HasOptions m) => m Bool
shouldPostponeInstanceSearch (do
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.instance" Int
20 [Char]
"Postponing possibly recursive instance search."
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just ([Candidate]
cands, Blocker
neverUnblock)) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
billTo [Phase
Benchmark.Typing, Phase
Benchmark.InstanceSearch] 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 <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
  forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange MetaVariable
mv forall a b. (a -> b) -> a -> b
$ do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.instance" Int
15 forall a b. (a -> b) -> a -> b
$
        [Char]
"findInstance 2: constraint: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow MetaId
m forall a. [a] -> [a] -> [a]
++ [Char]
"; candidates left: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Candidate]
cands)
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ (if Bool
overlap then TCMT IO Doc
"overlap" else forall a. Null a => a
empty) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Candidate
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":"
              , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ 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 ]
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
70 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"raw" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ do
       forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ (if Bool
overlap then TCMT IO Doc
"overlap" else forall a. Null a => a
empty) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Candidate
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":"
              , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ 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 <- forall (m :: * -> *).
(HasBuiltins m, HasCallStack, MonadDebug m, MonadReduce m,
 MonadTCEnv m, ReadTCState m) =>
MetaId -> m Type
getMetaTypeInContext MetaId
m
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.instance" Int
70 forall a b. (a -> b) -> a -> b
$ [Char]
"findInstance 2: t: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Type
t
      forall a. Type -> (Type -> TCM a) -> TCM a
insidePi Type
t forall a b. (a -> b) -> a -> b
$ \ Type
t -> do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
15 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"findInstance 3: t =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.instance" Int
70 forall a b. (a -> b) -> a -> b
$ [Char]
"findInstance 3: t: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Type
t

      Maybe ([(Candidate, TCErr)], [Candidate])
mcands <-
        -- Temporarily remove other instance constraints to avoid
        -- redundant solution attempts
        forall a.
(ConstraintStatus -> ProblemConstraint -> Bool) -> TCM a -> TCM a
holdConstraints (forall a b. a -> b -> a
const ProblemConstraint -> Bool
isInstanceProblemConstraint) 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
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
15 forall a b. (a -> b) -> a -> b
$
            TCMT IO Doc
"findInstance 5: the only viable candidate failed..."
          forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
        Just ([(Candidate, TCErr)]
errs, []) -> do
          if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Candidate, TCErr)]
errs then forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
15 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"findInstance 5: no viable candidate found..."
                       else forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
15 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"findInstance 5: all viable candidates failed..."
          -- #3676: Sort the candidates based on the size of the range for the errors and
          --        set the range of the full error to the range of the most precise candidate
          --        error.
          let sortedErrs :: [(Candidate, TCErr)]
sortedErrs = forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (forall a. Ord a => a -> a -> Ordering
compare 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) = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Int32
infinity forall a. Interval' a -> Int32
iLength forall a b. (a -> b) -> a -> b
$ forall a. Range' a -> Maybe IntervalWithoutFile
rangeToInterval forall a b. (a -> b) -> a -> b
$ forall a. HasRange a => a -> Range
getRange TCErr
err
                      infinity :: Int32
infinity = Int32
1000000000
          forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange (forall a. Int -> [a] -> [a]
take Int
1 forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Candidate, TCErr)]
sortedErrs) forall a b. (a -> b) -> a -> b
$
            forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError 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
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
15 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ TCMT IO Doc
"findInstance 5: solved by instance search using the only candidate"
            , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Candidate
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"=" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
term
            , TCMT IO Doc
"of type " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t'
            , TCMT IO Doc
"for type" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing  -- We’re done

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

insidePi :: Type -> (Type -> TCM a) -> TCM a
insidePi :: forall a. Type -> (Type -> TCM a) -> TCM a
insidePi Type
t Type -> TCM a
ret = forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (forall t a. Type'' t a -> a
unEl Type
t) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Pi Dom' Term Type
a Abs Type
b     -> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (forall a. Abs a -> [Char]
absName Abs Type
b, Dom' Term Type
a) forall a b. (a -> b) -> a -> b
$ forall a. Type -> (Type -> TCM a) -> TCM a
insidePi (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{}     -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Con{}      -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Lam{}      -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Lit{}      -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Level{}    -> forall a. HasCallStack => a
__IMPOSSIBLE__
    MetaV{}    -> forall a. HasCallStack => a
__IMPOSSIBLE__
    DontCare{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Dummy [Char]
s Elims
_  -> forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ [Char]
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  <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
  let ctxElims :: Elims
ctxElims = forall a b. (a -> b) -> [a] -> [b]
map 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  <- forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull (MetaId -> Elims -> Term
MetaV MetaId
m Elims
ctxElims)
        forall (m :: * -> *) a. Monad m => a -> m a
return (YesNoMaybe
ok, Term
v)
  [(Candidate, ((YesNoMaybe, Term), TCState))]
result <- 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 <- forall a. TCM a -> TCM (a, TCState)
localTCStateSaving (Candidate -> TCMT IO (YesNoMaybe, Term)
tryC Candidate
c); 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]
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
    []      -> 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'' <- 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]) forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ 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'' ]
      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 :: forall a.
MetaId -> [(Candidate, Term, a)] -> TCM [(Candidate, Term, a)]
dropSameCandidates MetaId
m [(Candidate, Term, a)]
cands0 = forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> [Char] -> m a -> m a
verboseBracket [Char]
"tc.instance" Int
30 [Char]
"dropSameCandidates" forall a b. (a -> b) -> a -> b
$ do
  !MetaId
nextMeta    <- forall (m :: * -> *). ReadTCState m => m MetaId
nextLocalMeta
  MetaId -> Bool
isRemoteMeta <- forall (m :: * -> *). ReadTCState m => m (MetaId -> Bool)
isRemoteMeta
  -- Does "it" contain any fresh meta-variables?
  let freshMetas :: Term -> Bool
freshMetas =
        Any -> Bool
getAny forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas (\MetaId
m -> Bool -> Any
Any (Bool -> Bool
not (MetaId -> Bool
isRemoteMeta MetaId
m Bool -> Bool -> Bool
|| MetaId
m forall a. Ord a => a -> a -> Bool
< MetaId
nextMeta)))

  -- Take overlappable candidates into account
  let cands :: [(Candidate, Term, a)]
cands =
        case 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

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

data YesNoMaybe = Yes | No | NoBecause TCErr | Maybe | HellNo TCErr
  deriving (Int -> YesNoMaybe -> ShowS
[YesNoMaybe] -> ShowS
YesNoMaybe -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [YesNoMaybe] -> ShowS
$cshowList :: [YesNoMaybe] -> ShowS
show :: YesNoMaybe -> [Char]
$cshow :: YesNoMaybe -> [Char]
showsPrec :: Int -> YesNoMaybe -> ShowS
$cshowsPrec :: Int -> YesNoMaybe -> ShowS
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 =
  forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> [Char] -> m a -> m a
verboseBracket [Char]
"tc.instance.candidates" Int
20 ([Char]
"checkCandidates " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow MetaId
m) forall a b. (a -> b) -> a -> b
$
  forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ([Candidate] -> TCMT IO Bool
anyMetaTypes [Candidate]
cands) (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing) forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.candidates" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"target:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.candidates" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"candidates"
      , forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCMT IO Doc
"-" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (if Bool
overlap then TCMT IO Doc
"overlap" else forall a. Null a => a
empty) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Candidate
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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)
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.candidates" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"valid candidates"
      , forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCMT IO Doc
"-" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (if Bool
overlap then TCMT IO Doc
"overlap" else forall a. Null a => a
empty) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Candidate
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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) <- forall a b. (a, b) -> b
snd ([(Candidate, TCErr)], [Candidate])
cands' ] ]
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.candidates" Int
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"valid candidates"
      , forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCMT IO Doc
"-" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (if Bool
overlap then TCMT IO Doc
"overlap" else forall a. Null a => a
empty) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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) <- forall a b. (a, b) -> b
snd ([(Candidate, TCErr)], [Candidate])
cands' ] ]
    forall (m :: * -> *) a. Monad m => a -> m a
return ([(Candidate, TCErr)], [Candidate])
cands'
  where
    anyMetaTypes :: [Candidate] -> TCM Bool
    anyMetaTypes :: [Candidate] -> TCMT IO Bool
anyMetaTypes [] = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    anyMetaTypes (Candidate CandidateKind
_ Term
_ Type
a Bool
_ : [Candidate]
cands) = do
      Type
a <- forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Type
a
      case forall t a. Type'' t a -> a
unEl Type
a of
        MetaV{} -> 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 = forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' Int TCEnv
eInstanceDepth forall a. Enum a => a -> a
succ forall a b. (a -> b) -> a -> b
$ do
      Int
d        <- forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' Int TCEnv
eInstanceDepth
      Int
maxDepth <- forall (m :: * -> *). HasOptions m => m Int
maxInstanceSearchDepth
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
d forall a. Ord a => a -> a -> Bool
> Int
maxDepth) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Term -> Type -> Int -> TypeError
InstanceSearchDepthExhausted Term
c Type
a Int
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' 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 <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
      forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange MetaVariable
mv forall a b. (a -> b) -> a -> b
$ do
        TCMT IO ()
debugConstraints
        forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> [Char] -> m a -> m a
verboseBracket [Char]
"tc.instance" Int
20 ([Char]
"checkCandidateForMeta " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow MetaId
m) forall a b. (a -> b) -> a -> b
$
          forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ TCM YesNoMaybe -> TCM YesNoMaybe
runCandidateCheck forall a b. (a -> b) -> a -> b
$ do
            forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.instance" Int
70 forall a b. (a -> b) -> a -> b
$ [Char]
"  t: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Type
t forall a. [a] -> [a] -> [a]
++ [Char]
"\n  t':" forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Type
t' forall a. [a] -> [a] -> [a]
++ [Char]
"\n  term: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Term
term forall a. [a] -> [a] -> [a]
++ [Char]
"."
            forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ TCMT IO Doc
"checkCandidateForMeta"
              , TCMT IO Doc
"t    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
              , TCMT IO Doc
"t'   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t'
              , TCMT IO Doc
"term =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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'') <- forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m, MonadTCM m) =>
Int -> (Hiding -> Bool) -> Type -> m (Args, Type)
implicitArgs (-Int
1) (\Hiding
h -> forall a. LensHiding a => a -> Bool
notVisible Hiding
h) Type
t'

            forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
20 forall a b. (a -> b) -> a -> b
$
              TCMT IO Doc
"instance search: checking" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t''
              forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"<=" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
            forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
70 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ TCMT IO Doc
"instance search: checking (raw)"
              , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
4 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
t''
              , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"<="
              , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
4 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
t
              ]
            Term
v <- (Term -> Args -> TCMT IO Term
`applyDroppingParameters` Args
args) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
term
            forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
15 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ TCMT IO Doc
"instance search: attempting"
              , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
m forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":=" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
              ]
            forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
70 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$
              TCMT IO Doc
"candidate v = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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 <- forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) forall a b. (a -> b) -> a -> b
$ 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 = forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
verboseS [Char]
"tc.instance" Int
15 forall a b. (a -> b) -> a -> b
$ do
                  Term
sol <- 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 forall a. Eq a => a -> a -> Bool
== MetaId
m' ->
                      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
15 forall a b. (a -> b) -> a -> b
$
                        forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ (TCMT IO Doc
"instance search: maybe solution for" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
m) forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
":"
                            , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v ]
                    Term
_ ->
                      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
15 forall a b. (a -> b) -> a -> b
$
                        forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ (TCMT IO Doc
"instance search: found solution for" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
m) forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
":"
                            , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
sol ]

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

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

          debugSuccess :: TCMT IO ()
debugSuccess            = forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.instance" Int
50 [Char]
"assignment successful" :: TCM ()
          debugInconclusive :: TCMT IO ()
debugInconclusive       = forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.instance" Int
50 [Char]
"assignment inconclusive" :: TCM ()
          debugConstraintFail :: a -> m ()
debugConstraintFail a
why = forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
50 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"candidate failed constraints:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
why
          debugTypeFail :: a -> m ()
debugTypeFail a
err       = forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
50 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"candidate failed type check:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ TCErr -> YesNoMaybe
HellNo TCErr
err
            | Bool
otherwise       = YesNoMaybe
No forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall {m :: * -> *} {a}. (MonadDebug m, PrettyTCM a) => a -> m ()
debugTypeFail TCErr
err

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

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

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

postponeInstanceConstraints :: TCM a -> TCM a
postponeInstanceConstraints :: forall a. TCM a -> TCM a
postponeInstanceConstraints TCM a
m =
  forall (m :: * -> *) a b.
ReadTCState m =>
Lens' a TCState -> (a -> a) -> m b -> m b
locallyTCState Lens' Bool TCState
stPostponeInstanceSearch (forall a b. a -> b -> a
const Bool
True) TCM a
m 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Term
t 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => ConHead -> m Definition
getConInfo ConHead
c
      case Defn
def of
        Constructor {conPars :: Defn -> Int
conPars = Int
n} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci (forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
drop Int
n Args
vs)
        Defn
_ -> 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 <- forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isRelevantProjection QName
f
      case Maybe Projection
mp of
        Just Projection{projIndex :: Projection -> Int
projIndex = Int
n} -> do
          case forall a. Int -> [a] -> [a]
drop Int
n Args
vs of
            []     -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
t
            Arg Term
u : Args
us -> (forall t. Apply t => t -> Args -> t
`apply` Args
us) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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