{-# 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
  (Tele (Dom' Term Type)
_ , OutputTypeName
otn) <- Type -> TCM (Tele (Dom' Term Type), 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
$ [Char] -> TypeError
GenericError ([Char] -> TypeError) -> [Char] -> TypeError
forall a b. (a -> b) -> a -> b
$
      [Char]
"Instance search can only be used to find elements in a named type"
    OutputTypeNameNotYetKnown Blocker
b -> do
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.cands" Int
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Instance type is not yet known. "
      Either Blocker [Candidate] -> TCM (Either Blocker [Candidate])
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocker -> Either Blocker [Candidate]
forall a b. a -> Either a b
Left Blocker
b)
    OutputTypeName
OutputTypeVisiblePi -> TypeError -> TCM (Either Blocker [Candidate])
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM (Either Blocker [Candidate]))
-> TypeError -> TCM (Either Blocker [Candidate])
forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError ([Char] -> TypeError) -> [Char] -> TypeError
forall a b. (a -> b) -> a -> b
$
      [Char]
"Instance search cannot be used to find elements in an explicit function type"
    OutputTypeName
OutputTypeVar    -> do
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.cands" Int
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Instance type is a variable. "
      BlockT (TCMT IO) [Candidate] -> TCM (Either Blocker [Candidate])
forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked BlockT (TCMT IO) [Candidate]
getContextVars
    OutputTypeName QName
n -> do
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.cands" Int
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Found instance type head: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
n
      BlockT (TCMT IO) [Candidate] -> TCM (Either Blocker [Candidate])
forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked BlockT (TCMT IO) [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 (TCMT IO) [Candidate]
getContextVars = do
      [Dom (Name, Type)]
ctx <- BlockT (TCMT IO) [Dom (Name, Type)]
forall (m :: * -> *). MonadTCEnv m => m [Dom (Name, Type)]
getContext
      [Char] -> Int -> TCMT IO Doc -> BlockT (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.cands" Int
40 (TCMT IO Doc -> BlockT (TCMT IO) ())
-> TCMT IO Doc -> BlockT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *).
Applicative m =>
m Doc -> Int -> m Doc -> m Doc
hang TCMT IO Doc
"Getting candidates from context" Int
2 (TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ PrettyContext -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (PrettyContext -> TCMT IO Doc) -> PrettyContext -> TCMT IO 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 = [ (Int -> Term
var Int
i, Int -> Dom (Name, Type) -> Dom (Name, Type)
forall a. Subst a => Int -> a -> a
raise (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Dom (Name, Type)
t) | (Int
i, Dom (Name, Type)
t) <- [Int] -> [Dom (Name, Type)] -> [(Int, Dom (Name, Type))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
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 (TCMT IO) [[Candidate]] -> BlockT (TCMT IO) [Candidate]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((CandidateKind, Term, Type) -> BlockT (TCMT IO) [Candidate])
-> [(CandidateKind, Term, Type)] -> BlockT (TCMT IO) [[Candidate]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (CandidateKind, Term, Type) -> BlockT (TCMT IO) [Candidate]
instanceFields ([(CandidateKind, Term, Type)] -> [(CandidateKind, Term, Type)]
forall a. [a] -> [a]
reverse [(CandidateKind, Term, Type)]
cxtAndTypes)
      [Char] -> Int -> TCMT IO Doc -> BlockT (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.fields" Int
30 (TCMT IO Doc -> BlockT (TCMT IO) ())
-> TCMT IO Doc -> BlockT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
        if [Candidate] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Candidate]
fields then TCMT IO Doc
"no instance field candidates" else
          TCMT IO Doc
"instance field candidates" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ do
            Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ (if Bool
overlap then TCMT IO Doc
"overlap" else TCMT IO Doc
forall a. Null a => a
empty) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Candidate -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Candidate
c TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":"
                    , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO 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 (TCMT IO) LetBindings
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> LetBindings
envLetBindings
      [(Name, (Term, Dom' Term Type))]
env <- ((Name, Open (Term, Dom' Term Type))
 -> BlockT (TCMT IO) (Name, (Term, Dom' Term Type)))
-> [(Name, Open (Term, Dom' Term Type))]
-> BlockT (TCMT IO) [(Name, (Term, Dom' Term Type))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Open (Term, Dom' Term Type)
 -> BlockT (TCMT IO) (Term, Dom' Term Type))
-> (Name, Open (Term, Dom' Term Type))
-> BlockT (TCMT IO) (Name, (Term, Dom' Term Type))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Open (Term, Dom' Term Type)
-> BlockT (TCMT IO) (Term, Dom' Term Type)
forall a (m :: * -> *).
(TermSubst a, MonadTCEnv m) =>
Open a -> m a
getOpen) ([(Name, Open (Term, Dom' Term Type))]
 -> BlockT (TCMT IO) [(Name, (Term, Dom' Term Type))])
-> [(Name, Open (Term, Dom' Term Type))]
-> BlockT (TCMT IO) [(Name, (Term, Dom' Term Type))]
forall a b. (a -> b) -> a -> b
$ LetBindings -> [(Name, Open (Term, Dom' Term 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' Term 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 (TCMT IO) [Candidate]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Candidate] -> BlockT (TCMT IO) [Candidate])
-> [Candidate] -> BlockT (TCMT IO) [Candidate]
forall a b. (a -> b) -> a -> b
$ [Candidate]
vars [Candidate] -> [Candidate] -> [Candidate]
forall a. [a] -> [a] -> [a]
++ [Candidate]
fields [Candidate] -> [Candidate] -> [Candidate]
forall a. [a] -> [a] -> [a]
++ [Candidate]
lets

    etaExpand :: (MonadTCM m, PureTCM m)
              => Bool -> Type -> m (Maybe (QName, Args))
    etaExpand :: forall (m :: * -> *).
(MonadTCM m, PureTCM m) =>
Bool -> Type -> m (Maybe (QName, Args))
etaExpand Bool
etaOnce Type
t =
      Type -> m (Maybe (QName, Args))
forall (m :: * -> *).
HasConstInfo m =>
Type -> m (Maybe (QName, Args))
isEtaRecordType Type
t m (Maybe (QName, Args))
-> (Maybe (QName, Args) -> m (Maybe (QName, Args)))
-> m (Maybe (QName, Args))
forall (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 (TCMT IO) [Candidate]
instanceFields = Bool -> (CandidateKind, Term, Type) -> BlockT (TCMT IO) [Candidate]
instanceFields' Bool
True

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

    getScopeDefs :: QName -> 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) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
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 [Char]
_})) = 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
          [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.qualified" Int
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
            if Bool
isQual then
              TCMT IO Doc
"dropping qualified instance" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q
            else
              TCMT IO Doc
"keeping instance" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
              TCMT IO Doc
"since it is in scope as" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [QName] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
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
    [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.instance" Int
20 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"The type of the FindInstance constraint isn't known, trying to find it again."
    Type
t <- Type -> TCMT IO Type
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate (Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MetaId -> TCMT IO Type
forall (m :: * -> *).
(MonadFail m, MonadTCEnv m, ReadTCState m, MonadReduce m,
 HasBuiltins m) =>
MetaId -> m Type
getMetaTypeInContext MetaId
m
    [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.instance" Int
70 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"findInstance 1: t: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Type
t

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

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

-- | 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
    [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.instance" Int
20 [Char]
"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
    [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.instance" Int
20 [Char]
"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 (TCMT IO))
-> TCMT IO (Maybe ([Candidate], Blocker))
-> TCMT IO (Maybe ([Candidate], Blocker))
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
billTo [BenchPhase (TCMT IO)
Phase
Benchmark.Typing, BenchPhase (TCMT IO)
Phase
Benchmark.InstanceSearch] (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
      [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.instance" Int
15 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
        [Char]
"findInstance 2: constraint: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ MetaId -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow MetaId
m [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"; candidates left: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show ([Candidate] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Candidate]
cands)
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
60 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ (if Bool
overlap then TCMT IO Doc
"overlap" else TCMT IO Doc
forall a. Null a => a
empty) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Candidate -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Candidate
c TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":"
              , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO 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 ]
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
70 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"raw" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ do
       Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ (if Bool
overlap then TCMT IO Doc
"overlap" else TCMT IO Doc
forall a. Null a => a
empty) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Candidate -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Candidate
c TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":"
              , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO 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
      [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.instance" Int
70 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"findInstance 2: t: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Type
t
      Type
-> (Type -> TCMT IO (Maybe ([Candidate], Blocker)))
-> TCMT IO (Maybe ([Candidate], Blocker))
forall a. Type -> (Type -> TCM a) -> TCM a
insidePi Type
t ((Type -> TCMT IO (Maybe ([Candidate], Blocker)))
 -> TCMT IO (Maybe ([Candidate], Blocker)))
-> (Type -> TCMT IO (Maybe ([Candidate], Blocker)))
-> TCMT IO (Maybe ([Candidate], Blocker))
forall a b. (a -> b) -> a -> b
$ \ Type
t -> do
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
15 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"findInstance 3: t =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
      [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.instance" Int
70 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"findInstance 3: t: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Type
t

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

        Just ([(Candidate, TCErr)]
_, [c :: Candidate
c@(Candidate CandidateKind
q Term
term Type
t' Bool
_)]) -> do
          [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
15 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ TCMT IO Doc
"findInstance 5: solved by instance search using the only candidate"
            , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Candidate -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Candidate
c TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
term
            , TCMT IO Doc
"of type " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t'
            , TCMT IO Doc
"for type" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
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
          [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
15 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
            [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"findInstance 5: refined candidates: ") TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
            [Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
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 :: forall a. Type -> (Type -> TCM a) -> TCM a
insidePi Type
t Type -> TCM a
ret = Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type -> Term
forall t a. Type'' t a -> a
unEl Type
t) TCMT IO Term -> (Term -> TCM a) -> TCM a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Pi Dom' Term Type
a Abs Type
b     -> ([Char], Dom' Term Type) -> TCM a -> TCM a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Abs Type -> [Char]
forall a. Abs a -> [Char]
absName Abs Type
b, Dom' Term Type
a) (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ Type -> (Type -> TCM a) -> TCM a
forall a. Type -> (Type -> TCM a) -> TCM a
insidePi (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b) Type -> TCM a
ret
    Def{}      -> Type -> TCM a
ret Type
t
    Var{}      -> Type -> TCM a
ret Type
t
    Sort{}     -> TCM a
forall a. HasCallStack => a
__IMPOSSIBLE__
    Con{}      -> TCM a
forall a. HasCallStack => a
__IMPOSSIBLE__
    Lam{}      -> TCM a
forall a. HasCallStack => a
__IMPOSSIBLE__
    Lit{}      -> TCM a
forall a. HasCallStack => a
__IMPOSSIBLE__
    Level{}    -> TCM a
forall a. HasCallStack => a
__IMPOSSIBLE__
    MetaV{}    -> TCM a
forall a. HasCallStack => a
__IMPOSSIBLE__
    DontCare{} -> TCM a
forall a. HasCallStack => a
__IMPOSSIBLE__
    Dummy [Char]
s Elims
_  -> [Char] -> TCM a
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ [Char]
s

-- | Apply the computation to every argument in turn by 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) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
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 :: forall a.
MetaId -> [(Candidate, Term, a)] -> TCM [(Candidate, Term, a)]
dropSameCandidates MetaId
m [(Candidate, Term, a)]
cands0 = [Char]
-> Int
-> [Char]
-> TCMT IO [(Candidate, Term, a)]
-> TCMT IO [(Candidate, Term, a)]
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> [Char] -> m a -> m a
verboseBracket [Char]
"tc.instance" Int
30 [Char]
"dropSameCandidates" (TCMT IO [(Candidate, Term, a)] -> TCMT IO [(Candidate, Term, a)])
-> TCMT IO [(Candidate, Term, a)] -> TCMT IO [(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
. (Int -> MetaStore -> Bool
forall a. Int -> IntMap a -> Bool
`IntMap.notMember` MetaStore
metas) (Int -> Bool) -> (MetaId -> Int) -> MetaId -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaId -> Int
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

  [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"valid candidates:"
    , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ if Term -> Bool
freshMetas Term
v then TCMT IO Doc
"(redacted)" else
                      [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
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)] -> TCMT IO [(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
      [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.instance" Int
30 [Char]
"dropSameCandidates: Meta is irrelevant so any candidate will do."
      [(Candidate, Term, a)] -> TCMT IO [(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
      [Char] -> Int -> [Char] -> TCMT IO ()
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"
      [(Candidate, Term, a)] -> TCMT IO [(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
          [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.instance" Int
30 [Char]
"dropSameCandidates: Solution of instance meta has fresh metas so we don't filter equal candidates yet"
          [(Candidate, Term, a)] -> TCMT IO [(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)])
-> TCMT IO [(Candidate, Term, a)] -> TCMT IO [(Candidate, Term, a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Candidate, Term, a) -> TCMT IO Bool)
-> [(Candidate, Term, a)] -> TCMT IO [(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 :: forall a. (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     =
          [Char] -> Int -> [Char] -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> [Char] -> m a -> m a
verboseBracket [Char]
"tc.instance" Int
30 [Char]
"dropSameCandidates: " (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ do
          [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"==", Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
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 (Int -> YesNoMaybe -> [Char] -> [Char]
[YesNoMaybe] -> [Char] -> [Char]
YesNoMaybe -> [Char]
(Int -> YesNoMaybe -> [Char] -> [Char])
-> (YesNoMaybe -> [Char])
-> ([YesNoMaybe] -> [Char] -> [Char])
-> Show YesNoMaybe
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
showList :: [YesNoMaybe] -> [Char] -> [Char]
$cshowList :: [YesNoMaybe] -> [Char] -> [Char]
show :: YesNoMaybe -> [Char]
$cshow :: YesNoMaybe -> [Char]
showsPrec :: Int -> YesNoMaybe -> [Char] -> [Char]
$cshowsPrec :: Int -> YesNoMaybe -> [Char] -> [Char]
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 =
  [Char]
-> Int
-> [Char]
-> TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
-> TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> [Char] -> m a -> m a
verboseBracket [Char]
"tc.instance.candidates" Int
20 ([Char]
"checkCandidates " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ MetaId -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow MetaId
m) (TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
 -> 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
    [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.candidates" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"target:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
    [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.candidates" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"candidates"
      , [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCMT IO Doc
"-" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (if Bool
overlap then TCMT IO Doc
"overlap" else TCMT IO Doc
forall a. Null a => a
empty) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Candidate -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Candidate
c TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO 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)
    [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.candidates" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"valid candidates"
      , [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCMT IO Doc
"-" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (if Bool
overlap then TCMT IO Doc
"overlap" else TCMT IO Doc
forall a. Null a => a
empty) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Candidate -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Candidate
c TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO 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' ] ]
    [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.candidates" Int
60 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"valid candidates"
      , [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCMT IO Doc
"-" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (if Bool
overlap then TCMT IO Doc
"overlap" else TCMT IO Doc
forall a. Null a => a
empty) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
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' Int TCEnv -> (Int -> Int) -> TCM YesNoMaybe -> TCM YesNoMaybe
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' Int TCEnv
eInstanceDepth Int -> Int
forall a. Enum a => a -> a
succ (TCM YesNoMaybe -> TCM YesNoMaybe)
-> TCM YesNoMaybe -> TCM YesNoMaybe
forall a b. (a -> b) -> a -> b
$ do
      Int
d        <- Lens' Int TCEnv -> TCMT IO Int
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' Int TCEnv
eInstanceDepth
      Int
maxDepth <- TCMT IO Int
forall (m :: * -> *). HasOptions m => m Int
maxInstanceSearchDepth
      Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
maxDepth) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Term -> Type -> Int -> TypeError
InstanceSearchDepthExhausted Term
c Type
a Int
maxDepth
      TCM 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
        [Char] -> Int -> [Char] -> TCM YesNoMaybe -> TCM YesNoMaybe
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> [Char] -> m a -> m a
verboseBracket [Char]
"tc.instance" Int
20 ([Char]
"checkCandidateForMeta " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ MetaId -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow MetaId
m) (TCM 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
            [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.instance" Int
70 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  t: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Type
t [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n  t':" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Type
t' [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n  term: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Term
term [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"."
            [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ TCMT IO Doc
"checkCandidateForMeta"
              , TCMT IO Doc
"t    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
              , TCMT IO Doc
"t'   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t'
              , TCMT IO Doc
"term =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
term
              ]

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

            [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
              TCMT IO Doc
"instance search: checking" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t''
              TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"<=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
            [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
70 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ TCMT IO Doc
"instance search: checking (raw)"
              , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
4 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
t''
              , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"<="
              , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
4 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
t
              ]
            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
            [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
15 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ TCMT IO Doc
"instance search: attempting"
              , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
m TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
              ]
            [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
70 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
              TCMT IO Doc
"candidate v = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v
            -- 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) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Args -> Elims) -> TCMT IO Args -> TCMT IO Elims
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
            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 = [Char] -> Int -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
verboseS [Char]
"tc.instance" Int
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' ->
                      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
15 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
                        [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ (TCMT IO Doc
"instance search: maybe solution for" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
m) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
":"
                            , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v ]
                    Term
_ ->
                      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
15 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
                        [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ (TCMT IO Doc
"instance search: found solution for" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
m) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
":"
                            , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
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            = [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.instance" Int
50 [Char]
"assignment successful" :: TCM ()
          debugInconclusive :: TCMT IO ()
debugInconclusive       = [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.instance" Int
50 [Char]
"assignment inconclusive" :: TCM ()
          debugConstraintFail :: a -> m ()
debugConstraintFail a
why = [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"candidate failed constraints:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
why
          debugTypeFail :: a -> m ()
debugTypeFail a
err       = [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"candidate failed type check:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCMT IO 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 :: forall (m :: * -> *). (ReadTCState m, HasOptions m) => 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 :: forall (m :: * -> *) a. ReadTCState m => 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 :: forall a. 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 -> Int
conPars = Int
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) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Args -> Elims) -> Args -> Elims
forall a b. (a -> b) -> a -> b
$ Int -> Args -> Args
forall a. Int -> [a] -> [a]
drop Int
n Args
vs)
        Defn
_ -> TCMT IO Term
forall a. HasCallStack => a
__IMPOSSIBLE__
    Def QName
f [] -> do
      -- Andreas, 2022-03-07, issue #5809: don't drop parameters of irrelevant projections.
      Maybe Projection
mp <- QName -> TCMT IO (Maybe Projection)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isRelevantProjection QName
f
      case Maybe Projection
mp of
        Just Projection{projIndex :: Projection -> Int
projIndex = Int
n} -> do
          case Int -> Args -> Args
forall a. Int -> [a] -> [a]
drop Int
n Args
vs of
            []     -> Term -> TCMT IO Term
forall (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