{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation #-}

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

import Control.Monad        ( forM )
import Control.Monad.Except ( ExceptT(..), runExceptT, MonadError(..) )
import Control.Monad.Trans  ( lift )

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

import Agda.Interaction.Options (optQualifiedInstances)

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

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

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

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

import Agda.Utils.Lens
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Syntax.Common.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 Type)
_ , OutputTypeName
otn) <- Type -> TCM (Tele (Dom 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 a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocker -> Either Blocker [Candidate]
forall a b. a -> Either a b
Left Blocker
b)
    OutputTypeName
OutputTypeVisiblePi -> TypeError -> TCM (Either Blocker [Candidate])
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM (Either Blocker [Candidate]))
-> TypeError -> TCM (Either Blocker [Candidate])
forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError ([Char] -> TypeError) -> [Char] -> TypeError
forall a b. (a -> b) -> a -> b
$
      [Char]
"Instance search cannot be used to find elements in an explicit function type"
    OutputTypeName
OutputTypeVar    -> do
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.cands" Int
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Instance type is a variable. "
      BlockT (TCMT IO) [Candidate] -> TCM (Either Blocker [Candidate])
forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked 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
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
n
      BlockT (TCMT IO) [Candidate] -> TCM (Either Blocker [Candidate])
forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked BlockT (TCMT IO) [Candidate]
getContextVars TCM (Either Blocker [Candidate])
-> (Either Blocker [Candidate] -> TCM (Either Blocker [Candidate]))
-> TCM (Either Blocker [Candidate])
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Left Blocker
b -> Either Blocker [Candidate] -> TCM (Either Blocker [Candidate])
forall a. a -> TCMT IO a
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
      Context
ctx <- BlockT (TCMT IO) Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext
      [Char] -> Int -> TCMT IO Doc -> BlockT (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.cands" Int
40 (TCMT IO Doc -> BlockT (TCMT IO) ())
-> TCMT IO Doc -> BlockT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *).
Applicative m =>
m Doc -> Int -> m Doc -> m Doc
hang TCMT IO Doc
"Getting candidates from context" Int
2 (TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ PrettyContext -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => PrettyContext -> m Doc
prettyTCM (PrettyContext -> TCMT IO Doc) -> PrettyContext -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Context -> PrettyContext
PrettyContext Context
ctx)
          -- Context variables with their types lifted to live in the full context
      let varsAndRaisedTypes :: [(Term, ContextEntry)]
varsAndRaisedTypes = [ (Int -> Term
var Int
i, Int -> ContextEntry -> ContextEntry
forall a. Subst a => Int -> a -> a
raise (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ContextEntry
t) | (Int
i, ContextEntry
t) <- [Int] -> Context -> [(Int, ContextEntry)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] Context
ctx ]
          vars :: [Candidate]
vars = [ CandidateKind -> Term -> Type -> 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, ContextEntry)]
varsAndRaisedTypes
                 , ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
isInstance ArgInfo
info
                 ]

      -- {{}}-fields of variables are also candidates
      let cxtAndTypes :: [(CandidateKind, Term, Type)]
cxtAndTypes = [ (CandidateKind
LocalCandidate, Term
x, Type
t) | (Term
x, Dom{unDom :: forall t e. Dom' t e -> e
unDom = (Name
_, Type
t)}) <- [(Term, ContextEntry)]
varsAndRaisedTypes ]
      [Candidate]
fields <- [[Candidate]] -> [Candidate]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Candidate]] -> [Candidate])
-> BlockT (TCMT IO) [[Candidate]] -> BlockT (TCMT IO) [Candidate]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((CandidateKind, Term, Type) -> BlockT (TCMT IO) [Candidate])
-> [(CandidateKind, Term, Type)] -> BlockT (TCMT IO) [[Candidate]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (CandidateKind, Term, Type) -> BlockT (TCMT IO) [Candidate]
instanceFields ([(CandidateKind, Term, Type)] -> [(CandidateKind, Term, Type)]
forall a. [a] -> [a]
reverse [(CandidateKind, Term, Type)]
cxtAndTypes)
      [Char] -> Int -> TCMT IO Doc -> BlockT (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.fields" Int
30 (TCMT IO Doc -> BlockT (TCMT IO) ())
-> TCMT IO Doc -> BlockT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
        if [Candidate] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Candidate]
fields then TCMT IO Doc
"no instance field candidates" else
          TCMT IO Doc
"instance field candidates" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ do
            Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ [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
forall (m :: * -> *). MonadPretty m => Candidate -> m Doc
prettyTCM Candidate
c TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":"
                    , 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
forall (m :: * -> *). MonadPretty m => Type -> 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, LetBinding)]
env <- ((Name, Open LetBinding) -> BlockT (TCMT IO) (Name, LetBinding))
-> [(Name, Open LetBinding)]
-> BlockT (TCMT IO) [(Name, LetBinding)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((Open LetBinding -> BlockT (TCMT IO) LetBinding)
-> (Name, Open LetBinding) -> BlockT (TCMT IO) (Name, LetBinding)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> (Name, a) -> f (Name, b)
traverse Open LetBinding -> BlockT (TCMT IO) LetBinding
forall a (m :: * -> *).
(TermSubst a, MonadTCEnv m) =>
Open a -> m a
getOpen) ([(Name, Open LetBinding)]
 -> BlockT (TCMT IO) [(Name, LetBinding)])
-> [(Name, Open LetBinding)]
-> BlockT (TCMT IO) [(Name, LetBinding)]
forall a b. (a -> b) -> a -> b
$ LetBindings -> [(Name, Open LetBinding)]
forall k a. Map k a -> [(k, a)]
Map.toList LetBindings
env
      let lets :: [Candidate]
lets = [ CandidateKind -> Term -> Type -> Bool -> Candidate
Candidate CandidateKind
LocalCandidate Term
v Type
t Bool
False
                 | (Name
_, LetBinding Origin
_ Term
v Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info, unDom :: forall t e. Dom' t e -> e
unDom = Type
t}) <- [(Name, LetBinding)]
env
                 , ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
isInstance ArgInfo
info
                 , ArgInfo -> Bool
forall a. LensModality a => a -> Bool
usableModality ArgInfo
info
                 ]
      [Candidate] -> BlockT (TCMT IO) [Candidate]
forall a. a -> BlockT (TCMT IO) a
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 a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Maybe (QName, Args)
Nothing | Bool
etaOnce -> do
          Type -> m (Maybe (QName, Args, 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 a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            Maybe (QName, Args, Defn)
Nothing         -> Maybe (QName, Args) -> m (Maybe (QName, Args))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (QName, Args)
forall a. Maybe a
Nothing
            Just (QName
r, Args
vs, 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 a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QName, Args) -> Maybe (QName, Args)
forall a. a -> Maybe a
Just (QName
r, Args
vs))
                else Maybe (QName, Args) -> m (Maybe (QName, Args))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (QName, Args)
forall a. Maybe a
Nothing
        Maybe (QName, Args)
r -> Maybe (QName, Args) -> m (Maybe (QName, Args))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (QName, Args)
r

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

    instanceFields' :: Bool -> (CandidateKind,Term,Type) -> BlockT TCM [Candidate]
    instanceFields' :: Bool -> (CandidateKind, Term, Type) -> BlockT (TCMT IO) [Candidate]
instanceFields' Bool
etaOnce (CandidateKind
q, Term
v, Type
t) =
      Type
-> (Blocker -> Type -> BlockT (TCMT IO) [Candidate])
-> (NotBlocked -> Type -> BlockT (TCMT IO) [Candidate])
-> BlockT (TCMT IO) [Candidate]
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
t (\ Blocker
m Type
_ -> Blocker -> BlockT (TCMT IO) [Candidate]
forall a. Blocker -> BlockT (TCMT IO) a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
m) ((NotBlocked -> Type -> BlockT (TCMT IO) [Candidate])
 -> BlockT (TCMT IO) [Candidate])
-> (NotBlocked -> Type -> BlockT (TCMT IO) [Candidate])
-> BlockT (TCMT IO) [Candidate]
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Type
t -> do
      BlockT (TCMT IO) (Maybe (QName, Args))
-> BlockT (TCMT IO) [Candidate]
-> ((QName, Args) -> BlockT (TCMT IO) [Candidate])
-> BlockT (TCMT IO) [Candidate]
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Bool -> Type -> BlockT (TCMT IO) (Maybe (QName, Args))
forall (m :: * -> *).
(MonadTCM m, PureTCM m) =>
Bool -> Type -> m (Maybe (QName, Args))
etaExpand Bool
etaOnce Type
t) ([Candidate] -> BlockT (TCMT IO) [Candidate]
forall a. a -> BlockT (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []) (((QName, Args) -> BlockT (TCMT IO) [Candidate])
 -> BlockT (TCMT IO) [Candidate])
-> ((QName, Args) -> BlockT (TCMT IO) [Candidate])
-> BlockT (TCMT IO) [Candidate]
forall a b. (a -> b) -> a -> b
$ \ (QName
r, Args
pars) -> do
        (Tele (Dom Type)
tel, Args
args) <- TCM (Tele (Dom Type), Args)
-> BlockT (TCMT IO) (Tele (Dom Type), Args)
forall (m :: * -> *) a. Monad m => m a -> BlockT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (Tele (Dom Type), Args)
 -> BlockT (TCMT IO) (Tele (Dom Type), Args))
-> TCM (Tele (Dom Type), Args)
-> BlockT (TCMT IO) (Tele (Dom Type), Args)
forall a b. (a -> b) -> a -> b
$ QName -> Args -> Term -> TCM (Tele (Dom Type), Args)
forall (m :: * -> *).
(HasConstInfo m, MonadDebug m, ReadTCState m,
 MonadError TCErr m) =>
QName -> Args -> Term -> m (Tele (Dom Type), Args)
forceEtaExpandRecord QName
r Args
pars Term
v
        let types :: [Type]
types = (Dom Type -> Type) -> [Dom Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Dom Type -> Type
forall t e. Dom' t e -> e
unDom ([Dom Type] -> [Type]) -> [Dom Type] -> [Type]
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg [Dom Type]) -> [Dom Type] -> [Dom Type]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst ([SubstArg [Dom Type]] -> Substitution' (SubstArg [Dom Type])
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([SubstArg [Dom Type]] -> Substitution' (SubstArg [Dom Type]))
-> [SubstArg [Dom Type]] -> Substitution' (SubstArg [Dom Type])
forall a b. (a -> b) -> a -> b
$ [SubstArg [Dom Type]] -> [SubstArg [Dom Type]]
forall a. [a] -> [a]
reverse ([SubstArg [Dom Type]] -> [SubstArg [Dom Type]])
-> [SubstArg [Dom Type]] -> [SubstArg [Dom Type]]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Term) -> Args -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg Args
args) (Tele (Dom Type) -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom Type)
tel)
        ([[Candidate]] -> [Candidate])
-> BlockT (TCMT IO) [[Candidate]] -> BlockT (TCMT IO) [Candidate]
forall a b. (a -> b) -> BlockT (TCMT IO) a -> BlockT (TCMT IO) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[Candidate]] -> [Candidate]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (BlockT (TCMT IO) [[Candidate]] -> BlockT (TCMT IO) [Candidate])
-> BlockT (TCMT IO) [[Candidate]] -> BlockT (TCMT IO) [Candidate]
forall a b. (a -> b) -> a -> b
$ [(Arg Term, Type)]
-> ((Arg Term, Type) -> BlockT (TCMT IO) [Candidate])
-> BlockT (TCMT IO) [[Candidate]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Args -> [Type] -> [(Arg Term, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip Args
args [Type]
types) (((Arg Term, Type) -> BlockT (TCMT IO) [Candidate])
 -> BlockT (TCMT IO) [[Candidate]])
-> ((Arg Term, Type) -> BlockT (TCMT IO) [Candidate])
-> BlockT (TCMT IO) [[Candidate]]
forall a b. (a -> b) -> a -> b
$ \ (Arg Term
arg, Type
t) ->
          ([ CandidateKind -> Term -> Type -> 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          <- Lens' TCEnv Relevance -> TCMT IO Relevance
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Relevance -> f Relevance) -> TCEnv -> f TCEnv
Lens' TCEnv Relevance
eRelevance
      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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 a. a -> TCMT IO a
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 a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError TCErr -> TCMT IO (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 a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Candidate
forall a. Maybe a
Nothing else do
          -- Andreas, 2017-01-14: instantiateDef is a bit of an overkill
          -- if we anyway get the freeVarsToApply
          -- WAS: t <- defType <$> instantiateDef def
          Args
args <- QName -> TCMT IO Args
forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
QName -> m Args
freeVarsToApply QName
q
          let t :: Type
t = Definition -> Type
defType Definition
def Type -> Args -> Type
`piApply` Args
args
              rel :: Relevance
rel = ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance (ArgInfo -> Relevance) -> ArgInfo -> Relevance
forall a b. (a -> b) -> a -> b
$ Definition -> ArgInfo
defArgInfo Definition
def
          let v :: Term
v = case Definition -> Defn
theDef Definition
def of
               -- drop parameters if it's a projection function...
               Function{ funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Right Projection
p } -> Projection -> ProjOrigin -> Relevance -> Args -> Term
projDropParsApply Projection
p ProjOrigin
ProjSystem Relevance
rel Args
args
               -- Andreas, 2014-08-19: constructors cannot be declared as
               -- instances (at least as of now).
               -- I do not understand why the Constructor case is not impossible.
               -- Ulf, 2014-08-20: constructors are always instances.
               Constructor{ conSrcCon :: Defn -> ConHead
conSrcCon = ConHead
c }       -> ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ConOSystem []
               Defn
_                                  -> QName -> Elims -> Term
Def QName
q (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 a. a -> TCMT IO a
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 a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
        handle TCErr
err                                                   = TCErr -> m (Maybe a)
forall a. TCErr -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err

        filterQualified :: TCM (Maybe Candidate) -> TCM (Maybe Candidate)
        filterQualified :: 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
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q
            else
              TCMT IO Doc
"keeping instance" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
              TCMT IO Doc
"since it is in scope as" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [QName] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [QName] -> m Doc
prettyTCM [QName]
qc
          if Bool
isQual then Maybe Candidate -> TCMT IO (Maybe Candidate)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Candidate
forall a. Maybe a
Nothing else 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 :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
  MetaVariable -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange MetaVariable
mv (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
    [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.instance" Int
20 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"The type of the FindInstance constraint isn't known, trying to find it again."
    Type
t <- Type -> TCMT IO Type
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate (Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MetaId -> TCMT IO Type
forall (m :: * -> *).
(HasBuiltins m, HasCallStack, MonadDebug m, MonadReduce m,
 MonadTCEnv m, ReadTCState m) =>
MetaId -> m Type
getMetaTypeInContext MetaId
m
    [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.instance" Int
70 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"findInstance 1: t: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Type
t

    -- Issue #2577: If the target is a function type the arguments are
    -- potential candidates, so we add them to the context to make
    -- initialInstanceCandidates pick them up.
    TelV Tele (Dom Type)
tel Type
t <- Int -> (Dom Type -> Bool) -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> (Dom Type -> Bool) -> Type -> m (TelV Type)
telViewUpTo' (-Int
1) Dom Type -> Bool
forall a. LensHiding a => a -> Bool
notVisible Type
t
    Either Blocker [Candidate]
cands <- Tele (Dom Type)
-> TCM (Either Blocker [Candidate])
-> TCM (Either Blocker [Candidate])
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom 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)

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

  worker :: Type -> ExceptT Blocker TCM [Candidate]
  worker :: Type -> ExceptT Blocker (TCMT IO) [Candidate]
worker Type
t' = do
    [Candidate]
cands <- TCM (Either Blocker [Candidate])
-> ExceptT Blocker (TCMT IO) [Candidate]
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (Type -> TCM (Either Blocker [Candidate])
initialInstanceCandidates Type
t')
    [Candidate]
cands <- TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
-> ExceptT
     Blocker
     (TCMT IO)
     (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
forall (m :: * -> *) a. Monad m => m a -> ExceptT Blocker m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (MetaId
-> Type
-> [Candidate]
-> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
checkCandidates MetaId
m Type
t' [Candidate]
cands) ExceptT
  Blocker
  (TCMT IO)
  (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
-> (Maybe ([(Candidate, TCErr)], [(Candidate, Term)])
    -> [Candidate])
-> ExceptT Blocker (TCMT IO) [Candidate]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
      Maybe ([(Candidate, TCErr)], [(Candidate, Term)])
Nothing         -> [Candidate]
cands
      Just ([(Candidate, TCErr)]
_, [(Candidate, Term)]
cands) -> (Candidate, Term) -> Candidate
forall a b. (a, b) -> a
fst ((Candidate, Term) -> Candidate)
-> [(Candidate, Term)] -> [Candidate]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Candidate, Term)]
cands
    [Candidate]
cands <- TCMT IO [Candidate] -> ExceptT Blocker (TCMT IO) [Candidate]
forall (m :: * -> *) a. Monad m => m a -> ExceptT Blocker m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift ((Candidate -> [Candidate] -> TCMT IO [Candidate])
-> [Candidate] -> [Candidate] -> TCMT IO [Candidate]
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM Candidate -> [Candidate] -> TCMT IO [Candidate]
insertCandidate [] [Candidate]
cands)
    [Char] -> Int -> TCMT IO Doc -> ExceptT Blocker (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.sort" Int
20 (TCMT IO Doc -> ExceptT Blocker (TCMT IO) ())
-> TCMT IO Doc -> ExceptT Blocker (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"sorted 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
forall (m :: * -> *). MonadPretty m => Candidate -> m Doc
prettyTCM Candidate
c TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
             | c :: Candidate
c@(Candidate CandidateKind
q Term
v Type
t Bool
overlap) <- [Candidate]
cands ] ]
    [Candidate] -> ExceptT Blocker (TCMT IO) [Candidate]
forall a. a -> ExceptT Blocker (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Candidate]
cands

-- | @'doesCandidateSpecialise' c1 c2@ checks whether the instance candidate @c1@
-- /specialises/ the instance candidate @c2@, i.e., whether the type of
-- @c2@ is a substitution instance of @c1@'s type.
-- Only the final return type of the instances is considered: the
-- presence of unsolvable instance arguments in the types of @c1@ or
-- @c2@ does not affect the results of 'doesCandidateSpecialise'.
doesCandidateSpecialise :: Candidate -> Candidate -> TCM Bool
doesCandidateSpecialise :: Candidate -> Candidate -> TCMT IO Bool
doesCandidateSpecialise c1 :: Candidate
c1@Candidate{candidateType :: Candidate -> Type
candidateType = Type
t1} c2 :: Candidate
c2@Candidate{candidateType :: Candidate -> Type
candidateType = Type
t2} = do
  -- We compare
  --    c1 : ∀ {Γ} → T
  -- against
  --    c2 : ∀ {Δ} → S
  -- by moving to the context Γ ⊢, so that any variables in T's type are
  -- "rigid", but *instantiating* S[?/Δ], so its variables are
  -- "flexible"; then calling the conversion checker.

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

    wrap :: TCMT IO Bool -> TCMT IO Bool
wrap = (TCMT IO Bool -> (TCErr -> TCMT IO Bool) -> TCMT IO Bool)
-> (TCErr -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip TCMT IO Bool -> (TCErr -> TCMT IO Bool) -> TCMT IO Bool
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError TCErr -> TCMT IO Bool
forall {m :: * -> *} {p}. MonadDebug m => p -> m Bool
handle
          -- Turn failures into returning false
         (TCMT IO Bool -> TCMT IO Bool)
-> (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCMT IO Bool -> TCMT IO Bool
forall a. TCM a -> TCM a
localTCState
         -- Discard any changes to the TC state (metas from
         -- instantiating t2, recursive instance constraints, etc)
         (TCMT IO Bool -> TCMT IO Bool)
-> (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCMT IO Bool -> TCMT IO Bool
forall a. TCM a -> TCM a
postponeInstanceConstraints
         -- Don't spend any time looking for instances in the contexts

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

    [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.sort" Int
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Does" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Candidate -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Candidate -> m Doc
prettyTCM Candidate
c1 TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"specialise" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Candidate -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Candidate -> m Doc
prettyTCM Candidate
c2 TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
"?")
    [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.sort" Int
60 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"Comparing candidate"
      , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (Candidate -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Candidate -> m Doc
prettyTCM Candidate
c1 TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc
colon TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t1)
      , TCMT IO Doc
"vs"
      , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (Candidate -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Candidate -> m Doc
prettyTCM Candidate
c2 TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc
colon TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t2)
      ]

    Type -> Type -> TCMT IO ()
forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
leqType Type
t2 Type
t1
    [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.sort" Int
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 TCMT IO Doc
"=> IS specialisation"
    Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True

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

-- | 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 :: * -> *).
(HasCallStack, MonadDebug 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 a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (([Candidate], Blocker) -> Maybe ([Candidate], Blocker)
forall a. a -> Maybe a
Just ([Candidate]
cands, Blocker
neverUnblock))) (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 a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([Candidate], Blocker)
 -> TCMT IO (Maybe ([Candidate], Blocker)))
-> Maybe ([Candidate], Blocker)
-> TCMT IO (Maybe ([Candidate], Blocker))
forall a b. (a -> b) -> a -> b
$ ([Candidate], Blocker) -> Maybe ([Candidate], Blocker)
forall a. a -> Maybe a
Just ([Candidate]
cands, Blocker
neverUnblock)) (TCMT IO (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 :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
  MetaVariable
-> TCMT IO (Maybe ([Candidate], Blocker))
-> TCMT IO (Maybe ([Candidate], Blocker))
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange MetaVariable
mv (TCMT IO (Maybe ([Candidate], Blocker))
 -> TCMT IO (Maybe ([Candidate], Blocker)))
-> TCMT IO (Maybe ([Candidate], Blocker))
-> TCMT IO (Maybe ([Candidate], Blocker))
forall a b. (a -> b) -> a -> b
$ do
      [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.instance" Int
15 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
        [Char]
"findInstance 2: constraint: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ MetaId -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow MetaId
m [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"; candidates left: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show ([Candidate] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Candidate]
cands)
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
60 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ [TCMT IO Doc] -> TCMT IO Doc
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
forall (m :: * -> *). MonadPretty m => Candidate -> m Doc
prettyTCM Candidate
c TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":"
              , 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
forall (m :: * -> *). MonadPretty m => Type -> 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
forall (m :: * -> *). MonadPretty m => Candidate -> m Doc
prettyTCM Candidate
c TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":"
              , 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 :: * -> *).
(HasBuiltins m, HasCallStack, MonadDebug m, MonadReduce m,
 MonadTCEnv m, ReadTCState m) =>
MetaId -> m Type
getMetaTypeInContext MetaId
m
      [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.instance" Int
70 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"findInstance 2: t: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Type
t
      Type
-> (Type -> TCMT IO (Maybe ([Candidate], Blocker)))
-> TCMT IO (Maybe ([Candidate], Blocker))
forall a. Type -> (Type -> TCM a) -> TCM a
insidePi Type
t ((Type -> TCMT IO (Maybe ([Candidate], Blocker)))
 -> TCMT IO (Maybe ([Candidate], Blocker)))
-> (Type -> TCMT IO (Maybe ([Candidate], Blocker)))
-> TCMT IO (Maybe ([Candidate], Blocker))
forall a b. (a -> b) -> a -> b
$ \ Type
t -> do
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
15 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"findInstance 3: t =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
      [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.instance" Int
70 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"findInstance 3: t: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Type
t

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

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

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

        Just ([(Candidate, TCErr)]
_, [(c :: Candidate
c@(Candidate CandidateKind
q Term
term Type
t' Bool
_), Term
v)]) -> do

          [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
15 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ TCMT IO Doc
"instance search: attempting"
            , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
m TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
            ]
          [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
70 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
            TCMT IO Doc
"candidate v = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v
          Elims
ctxElims <- (Arg Term -> Elim) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Args -> Elims) -> TCMT IO Args -> TCMT IO Elims
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
          Type -> Term -> Term -> TCMT IO ()
forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
t (MetaId -> Elims -> Term
MetaV MetaId
m Elims
ctxElims) Term
v

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

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

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

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

-- | Apply the computation to every argument in turn by 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 YesNo) -> TCM ([(Candidate, TCErr)], [(Candidate, Term)])
filterResetingState :: MetaId
-> [Candidate]
-> (Candidate -> TCM YesNo)
-> TCM ([(Candidate, TCErr)], [(Candidate, Term)])
filterResetingState MetaId
m [Candidate]
cands Candidate -> TCM YesNo
f = do
  Args
ctxArgs  <- TCMT IO Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
  let ctxElims :: Elims
ctxElims = (Arg Term -> Elim) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply Args
ctxArgs
  [(Candidate, (YesNo, TCState))]
result <- (Candidate -> TCMT IO (Candidate, (YesNo, TCState)))
-> [Candidate] -> TCMT IO [(Candidate, (YesNo, TCState))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\Candidate
c -> do (YesNo, TCState)
bs <- TCM YesNo -> TCM (YesNo, TCState)
forall a. TCM a -> TCM (a, TCState)
localTCStateSaving (Candidate -> TCM YesNo
f Candidate
c); (Candidate, (YesNo, TCState))
-> TCMT IO (Candidate, (YesNo, TCState))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Candidate
c, (YesNo, TCState)
bs)) [Candidate]
cands

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

  -- c : Candidate
  -- r : YesNo
  -- a : Type         (fully instantiated)
  -- s : TCState
  let result' :: [(Candidate, Term, TCState)]
result' = [ (Candidate
c, Term
v, TCState
s) | (Candidate
c, (YesNo
r, TCState
s)) <- [(Candidate, (YesNo, TCState))]
result, Term
v <- Maybe Term -> [Term]
forall a. Maybe a -> [a]
maybeToList (YesNo -> Maybe Term
fromYes YesNo
r) ]
  [(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
v, TCState
s)] -> ([], [(Candidate
c,Term
v)]) ([(Candidate, TCErr)], [(Candidate, Term)])
-> TCMT IO () -> TCM ([(Candidate, TCErr)], [(Candidate, Term)])
forall a b. a -> TCMT IO b -> TCMT IO a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ TCState -> TCMT IO ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
s
    [(Candidate, Term, TCState)]
_           -> do
      let bad :: [(Candidate, TCErr)]
bad  = [ (Candidate
c, TCErr
err) | (Candidate
c, (NoBecause TCErr
err, TCState
_)) <- [(Candidate, (YesNo, TCState))]
result ]
          good :: [(Candidate, Term)]
good = [ (Candidate
c, Term
v) | (Candidate
c, Term
v, TCState
_) <- [(Candidate, Term, TCState)]
result'' ]
      ([(Candidate, TCErr)], [(Candidate, Term)])
-> TCM ([(Candidate, TCErr)], [(Candidate, Term)])
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Candidate, TCErr)]
bad, [(Candidate, Term)]
good)

-- 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 a. [Char] -> Int -> [Char] -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> [Char] -> m a -> m a
verboseBracket [Char]
"tc.instance" Int
30 [Char]
"dropSameCandidates" (TCMT IO [(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
  !MetaId
nextMeta    <- TCMT IO MetaId
forall (m :: * -> *). ReadTCState m => m MetaId
nextLocalMeta
  MetaId -> Bool
isRemoteMeta <- TCMT IO (MetaId -> Bool)
forall (m :: * -> *). ReadTCState m => m (MetaId -> Bool)
isRemoteMeta
  -- Does "it" contain any fresh meta-variables?
  let freshMetas :: Term -> Bool
freshMetas =
        Any -> Bool
getAny (Any -> Bool) -> (Term -> Any) -> Term -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        (MetaId -> Any) -> Term -> Any
forall m. Monoid m => (MetaId -> m) -> Term -> m
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas (\MetaId
m -> Bool -> Any
Any (Bool -> Bool
not (MetaId -> Bool
isRemoteMeta MetaId
m Bool -> Bool -> Bool
|| MetaId
m MetaId -> MetaId -> Bool
forall a. Ord a => a -> a -> Bool
< MetaId
nextMeta)))

  -- 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
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v ]
                    | (Candidate
_, Term
v, a
_) <- [(Candidate, Term, a)]
cands ] ]
  Relevance
rel <- Modality -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance (Modality -> Relevance) -> TCMT IO Modality -> TCMT IO Relevance
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO Modality
forall (m :: * -> *). ReadTCState m => MetaId -> m Modality
lookupMetaModality MetaId
m
  case [(Candidate, Term, a)]
cands of
    []            -> [(Candidate, Term, a)] -> TCMT IO [(Candidate, Term, a)]
forall a. a -> TCMT IO 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 a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Candidate, Term, a)
cvd]
    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 a. a -> TCMT IO 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 a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False  -- If there are fresh metas we can't compare
            | Bool
otherwise     =
          [Char] -> Int -> [Char] -> TCMT IO Bool -> TCMT IO Bool
forall a. [Char] -> Int -> [Char] -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> [Char] -> m a -> m a
verboseBracket [Char]
"tc.instance" Int
30 [Char]
"dropSameCandidates: " (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ do
          [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"==", Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v' ]
          Type
a <- (Type -> Args -> TCMT IO Type) -> (Type, Args) -> TCMT IO Type
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Type -> Args -> TCMT IO Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
Type -> Args -> m Type
piApplyM ((Type, Args) -> TCMT IO Type)
-> TCMT IO (Type, Args) -> TCMT IO Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ((,) (Type -> Args -> (Type, Args))
-> TCMT IO Type -> TCMT IO (Args -> (Type, Args))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO Type
forall (m :: * -> *). ReadTCState m => MetaId -> m Type
getMetaType MetaId
m TCMT IO (Args -> (Type, Args))
-> TCMT IO Args -> TCMT IO (Type, Args)
forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TCMT IO Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs)
          BlockT (TCMT IO) Bool -> TCMT IO (Either Blocker Bool)
forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked (Type -> Term -> Term -> BlockT (TCMT IO) Bool
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Type -> Term -> Term -> m Bool
pureEqualTerm Type
a Term
v Term
v') TCMT IO (Either Blocker Bool)
-> (Either Blocker Bool -> Bool) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
            Left{}  -> Bool
False
            Right Bool
b -> Bool
b

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

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

-- | Given a meta @m@ of type @t@ and a list of candidates @cands@,
-- @checkCandidates m t cands@ returns a refined list of valid candidates and
-- candidates that failed some constraints.
checkCandidates :: MetaId -> Type -> [Candidate] -> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
checkCandidates :: MetaId
-> Type
-> [Candidate]
-> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
checkCandidates MetaId
m Type
t [Candidate]
cands =
  [Char]
-> Int
-> [Char]
-> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
-> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
forall a. [Char] -> Int -> [Char] -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> [Char] -> m a -> m a
verboseBracket [Char]
"tc.instance.candidates" Int
20 ([Char]
"checkCandidates " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ MetaId -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow MetaId
m) (TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
 -> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)])))
-> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
-> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
forall a b. (a -> b) -> a -> b
$
  TCMT IO Bool
-> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
-> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
-> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ([Candidate] -> TCMT IO Bool
anyMetaTypes [Candidate]
cands) (Maybe ([(Candidate, TCErr)], [(Candidate, Term)])
-> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ([(Candidate, TCErr)], [(Candidate, Term)])
forall a. Maybe a
Nothing) (TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
 -> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)])))
-> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
-> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
forall a b. (a -> b) -> a -> b
$ ([(Candidate, TCErr)], [(Candidate, Term)])
-> Maybe ([(Candidate, TCErr)], [(Candidate, Term)])
forall a. a -> Maybe a
Just (([(Candidate, TCErr)], [(Candidate, Term)])
 -> Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
-> TCM ([(Candidate, TCErr)], [(Candidate, Term)])
-> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.candidates" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"target:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
    [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.candidates" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"candidates"
      , [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ 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
forall (m :: * -> *). MonadPretty m => Candidate -> m Doc
prettyTCM Candidate
c TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
             | c :: Candidate
c@(Candidate CandidateKind
q Term
v Type
t Bool
overlap) <- [Candidate]
cands ] ]
    ([(Candidate, TCErr)], [(Candidate, Term)])
cands' <- MetaId
-> [Candidate]
-> (Candidate -> TCM YesNo)
-> TCM ([(Candidate, TCErr)], [(Candidate, Term)])
filterResetingState MetaId
m [Candidate]
cands (MetaId -> Type -> Candidate -> TCM YesNo
checkCandidateForMeta MetaId
m Type
t)
    [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance.candidates" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"valid candidates"
      , [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ 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
forall (m :: * -> *). MonadPretty m => Candidate -> m Doc
prettyTCM Candidate
c TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
             | c :: Candidate
c@(Candidate CandidateKind
q Term
v Type
t Bool
overlap) <- ((Candidate, Term) -> Candidate)
-> [(Candidate, Term)] -> [Candidate]
forall a b. (a -> b) -> [a] -> [b]
map (Candidate, Term) -> Candidate
forall a b. (a, b) -> a
fst (([(Candidate, TCErr)], [(Candidate, Term)]) -> [(Candidate, Term)]
forall a b. (a, b) -> b
snd ([(Candidate, TCErr)], [(Candidate, Term)])
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
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
             | c :: Candidate
c@(Candidate CandidateKind
q Term
v Type
t Bool
overlap) <- ((Candidate, Term) -> Candidate)
-> [(Candidate, Term)] -> [Candidate]
forall a b. (a -> b) -> [a] -> [b]
map (Candidate, Term) -> Candidate
forall a b. (a, b) -> a
fst (([(Candidate, TCErr)], [(Candidate, Term)]) -> [(Candidate, Term)]
forall a b. (a, b) -> b
snd ([(Candidate, TCErr)], [(Candidate, Term)])
cands') ] ]
    ([(Candidate, TCErr)], [(Candidate, Term)])
-> TCM ([(Candidate, TCErr)], [(Candidate, Term)])
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Candidate, TCErr)], [(Candidate, Term)])
cands'
  where
    anyMetaTypes :: [Candidate] -> TCM Bool
    anyMetaTypes :: [Candidate] -> TCMT IO Bool
anyMetaTypes [] = Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    anyMetaTypes (Candidate CandidateKind
_ Term
_ Type
a 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 a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        Term
_       -> [Candidate] -> TCMT IO Bool
anyMetaTypes [Candidate]
cands

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

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

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

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

          (TCM YesNo -> (TCErr -> TCM YesNo) -> TCM YesNo)
-> (TCErr -> TCM YesNo) -> TCM YesNo -> TCM YesNo
forall a b c. (a -> b -> c) -> b -> a -> c
flip TCM YesNo -> (TCErr -> TCM YesNo) -> TCM YesNo
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError (YesNo -> TCM YesNo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (YesNo -> TCM YesNo) -> (TCErr -> YesNo) -> TCErr -> TCM YesNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCErr -> YesNo
NoBecause) (TCM YesNo -> TCM YesNo) -> TCM YesNo -> TCM YesNo
forall a b. (a -> b) -> a -> b
$ do
            -- make a pass over constraints, to detect cases where
            -- some are made unsolvable by the type comparison, but
            -- don't do this for FindInstance's to prevent loops.
            Bool -> TCMT IO ()
forall (m :: * -> *). MonadConstraint m => Bool -> m ()
solveAwakeConstraints' Bool
True
            -- We need instantiateFull here to remove 'local' metas
            Term
v <- Term -> TCMT IO Term
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull (Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Term
term Term -> Args -> TCMT IO Term
`applyDroppingParameters` Args
args)
            [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.instance" Int
15 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
              [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ (TCMT IO Doc
"instance search: found solution for" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
m) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
":"
                  , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v ]
            YesNo -> TCM YesNo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (YesNo -> TCM YesNo) -> YesNo -> TCM YesNo
forall a b. (a -> b) -> a -> b
$ Term -> YesNo
Yes Term
v
      where
        runCandidateCheck :: TCM YesNo -> TCM YesNo
runCandidateCheck = (TCM YesNo -> (TCErr -> TCM YesNo) -> TCM YesNo)
-> (TCErr -> TCM YesNo) -> TCM YesNo -> TCM YesNo
forall a b c. (a -> b -> c) -> b -> a -> c
flip TCM YesNo -> (TCErr -> TCM YesNo) -> TCM YesNo
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError TCErr -> TCM YesNo
handle (TCM YesNo -> TCM YesNo)
-> (TCM YesNo -> TCM YesNo) -> TCM YesNo -> TCM YesNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCM YesNo -> TCM YesNo
forall (m :: * -> *) a. ReadTCState m => m a -> m a
nowConsideringInstance

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

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


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

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)
    TCMT IO ()
solveAwakeInstanceConstraints

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

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

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