{-# LANGUAGE NondecreasingIndentation #-}

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

import Control.Monad.Reader
import qualified Data.IntSet as IntSet
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 Agda.Interaction.Options (optOverlappingInstances)

import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.MetaVars
import Agda.Syntax.Scope.Base (isNameInScope)

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

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

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

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

import Agda.Utils.Impossible

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

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

      -- get let bindings
      LetBindings
env <- (TCEnv -> LetBindings) -> ExceptT Blocked_ TCM LetBindings
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> LetBindings
envLetBindings
      [(Term, Dom Type)]
env <- ((Name, Open (Term, Dom Type))
 -> ExceptT Blocked_ TCM (Term, Dom Type))
-> [(Name, Open (Term, Dom Type))]
-> ExceptT Blocked_ TCM [(Term, Dom Type)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Open (Term, Dom Type) -> ExceptT Blocked_ TCM (Term, Dom Type)
forall a (m :: * -> *).
(Subst Term a, MonadTCEnv m) =>
Open a -> m a
getOpen (Open (Term, Dom Type) -> ExceptT Blocked_ TCM (Term, Dom Type))
-> ((Name, Open (Term, Dom Type)) -> Open (Term, Dom Type))
-> (Name, Open (Term, Dom Type))
-> ExceptT Blocked_ TCM (Term, Dom Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Open (Term, Dom Type)) -> Open (Term, Dom Type)
forall a b. (a, b) -> b
snd) ([(Name, Open (Term, Dom Type))]
 -> ExceptT Blocked_ TCM [(Term, Dom Type)])
-> [(Name, Open (Term, Dom Type))]
-> ExceptT Blocked_ TCM [(Term, Dom Type)]
forall a b. (a -> b) -> a -> b
$ LetBindings -> [(Name, Open (Term, Dom Type))]
forall k a. Map k a -> [(k, a)]
Map.toList LetBindings
env
      let lets :: [Candidate]
lets = [ Term -> Type -> Bool -> Candidate
Candidate Term
v Type
t Bool
False
                 | (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}) <- [(Term, Dom Type)]
env
                 , ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
isInstance ArgInfo
info
                 , ArgInfo -> Bool
forall a. LensModality a => a -> Bool
usableModality ArgInfo
info
                 ]
      [Candidate] -> ExceptT Blocked_ TCM [Candidate]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Candidate] -> ExceptT Blocked_ TCM [Candidate])
-> [Candidate] -> ExceptT Blocked_ TCM [Candidate]
forall a b. (a -> b) -> a -> b
$ [Candidate]
vars [Candidate] -> [Candidate] -> [Candidate]
forall a. [a] -> [a] -> [a]
++ [Candidate]
fields [Candidate] -> [Candidate] -> [Candidate]
forall a. [a] -> [a] -> [a]
++ [Candidate]
lets

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

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

    instanceFields' :: Bool -> (Term,Type) -> ExceptT Blocked_ TCM [Candidate]
    instanceFields' :: Bool -> (Term, Type) -> ExceptT Blocked_ TCM [Candidate]
instanceFields' Bool
etaOnce (Term
v, Type
t) =
      Type
-> (MetaId -> Type -> ExceptT Blocked_ TCM [Candidate])
-> (NotBlocked -> Type -> ExceptT Blocked_ TCM [Candidate])
-> ExceptT Blocked_ TCM [Candidate]
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m, HasBuiltins m) =>
t -> (MetaId -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
t (\MetaId
m Type
_ -> Blocked_ -> ExceptT Blocked_ TCM [Candidate]
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Blocked_ -> ExceptT Blocked_ TCM [Candidate])
-> Blocked_ -> ExceptT Blocked_ TCM [Candidate]
forall a b. (a -> b) -> a -> b
$ MetaId -> () -> Blocked_
forall t. MetaId -> t -> Blocked t
Blocked MetaId
m ()) ((NotBlocked -> Type -> ExceptT Blocked_ TCM [Candidate])
 -> ExceptT Blocked_ TCM [Candidate])
-> (NotBlocked -> Type -> ExceptT Blocked_ TCM [Candidate])
-> ExceptT Blocked_ TCM [Candidate]
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Type
t -> do
      ExceptT Blocked_ TCM (Maybe (QName, Args))
-> ExceptT Blocked_ TCM [Candidate]
-> ((QName, Args) -> ExceptT Blocked_ TCM [Candidate])
-> ExceptT Blocked_ TCM [Candidate]
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Bool -> Type -> ExceptT Blocked_ TCM (Maybe (QName, Args))
forall (m :: * -> *).
(MonadTCM m, MonadReduce m, HasConstInfo m, HasBuiltins m) =>
Bool -> Type -> m (Maybe (QName, Args))
etaExpand Bool
etaOnce Type
t) ([Candidate] -> ExceptT Blocked_ TCM [Candidate]
forall (m :: * -> *) a. Monad m => a -> m a
return []) (((QName, Args) -> ExceptT Blocked_ TCM [Candidate])
 -> ExceptT Blocked_ TCM [Candidate])
-> ((QName, Args) -> ExceptT Blocked_ TCM [Candidate])
-> ExceptT Blocked_ TCM [Candidate]
forall a b. (a -> b) -> a -> b
$ \ (QName
r, Args
pars) -> do
        (Telescope
tel, Args
args) <- TCM (Telescope, Args) -> ExceptT Blocked_ TCM (Telescope, Args)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (Telescope, Args) -> ExceptT Blocked_ TCM (Telescope, Args))
-> TCM (Telescope, Args) -> ExceptT Blocked_ TCM (Telescope, Args)
forall a b. (a -> b) -> a -> b
$ QName -> Args -> Term -> TCM (Telescope, Args)
forall (m :: * -> *).
(HasConstInfo m, MonadDebug m, ReadTCState m,
 MonadError TCErr m) =>
QName -> Args -> Term -> m (Telescope, Args)
forceEtaExpandRecord QName
r Args
pars Term
v
        let types :: [Type]
types = (Dom Type -> Type) -> [Dom Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Dom Type -> Type
forall t e. Dom' t e -> e
unDom ([Dom Type] -> [Type]) -> [Dom Type] -> [Type]
forall a b. (a -> b) -> a -> b
$ Substitution' Term -> [Dom Type] -> [Dom Type]
forall t a. Subst t a => Substitution' t -> a -> a
applySubst ([Term] -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> Substitution' Term) -> [Term] -> Substitution' Term
forall a b. (a -> b) -> a -> b
$ [Term] -> [Term]
forall a. [a] -> [a]
reverse ([Term] -> [Term]) -> [Term] -> [Term]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Term) -> Args -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg Args
args) (Telescope -> [Dom Type]
forall a. Subst Term a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
tel)
        ([[Candidate]] -> [Candidate])
-> ExceptT Blocked_ TCM [[Candidate]]
-> ExceptT Blocked_ TCM [Candidate]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[Candidate]] -> [Candidate]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (ExceptT Blocked_ TCM [[Candidate]]
 -> ExceptT Blocked_ TCM [Candidate])
-> ExceptT Blocked_ TCM [[Candidate]]
-> ExceptT Blocked_ TCM [Candidate]
forall a b. (a -> b) -> a -> b
$ [(Arg Term, Type)]
-> ((Arg Term, Type) -> ExceptT Blocked_ TCM [Candidate])
-> ExceptT Blocked_ TCM [[Candidate]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Args -> [Type] -> [(Arg Term, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip Args
args [Type]
types) (((Arg Term, Type) -> ExceptT Blocked_ TCM [Candidate])
 -> ExceptT Blocked_ TCM [[Candidate]])
-> ((Arg Term, Type) -> ExceptT Blocked_ TCM [Candidate])
-> ExceptT Blocked_ TCM [[Candidate]]
forall a b. (a -> b) -> a -> b
$ \ (Arg Term
arg, Type
t) ->
          ([ Term -> Type -> Bool -> Candidate
Candidate (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])
-> ExceptT Blocked_ TCM [Candidate]
-> ExceptT Blocked_ TCM [Candidate]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
          Bool -> (Term, Type) -> ExceptT Blocked_ TCM [Candidate]
instanceFields' Bool
False (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
arg, Type
t)

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

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

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

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

findInstance MetaId
m (Just [Candidate]
cands) =
  TCMT IO (Maybe ([Candidate], Maybe MetaId))
-> (([Candidate], Maybe MetaId) -> TCMT IO ()) -> TCMT IO ()
forall (m :: * -> *) a.
Monad m =>
m (Maybe a) -> (a -> m ()) -> m ()
whenJustM (MetaId
-> [Candidate] -> TCMT IO (Maybe ([Candidate], Maybe MetaId))
findInstance' MetaId
m [Candidate]
cands) ((([Candidate], Maybe MetaId) -> TCMT IO ()) -> TCMT IO ())
-> (([Candidate], Maybe MetaId) -> TCMT IO ()) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ (\ ([Candidate]
cands, Maybe MetaId
b) -> Constraint -> TCMT IO ()
forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
addConstraint (Constraint -> TCMT IO ()) -> Constraint -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ MetaId -> Maybe MetaId -> Maybe [Candidate] -> Constraint
FindInstance MetaId
m Maybe MetaId
b (Maybe [Candidate] -> Constraint)
-> Maybe [Candidate] -> Constraint
forall a b. (a -> b) -> a -> b
$ [Candidate] -> Maybe [Candidate]
forall a. a -> Maybe a
Just [Candidate]
cands)

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

      Maybe ([(Candidate, TCErr)], [Candidate])
mcands <- MetaId
-> Type
-> [Candidate]
-> TCM (Maybe ([(Candidate, TCErr)], [Candidate]))
checkCandidates MetaId
m Type
t [Candidate]
cands
      TCMT IO ()
debugConstraints
      case Maybe ([(Candidate, TCErr)], [Candidate])
mcands of

        Just ([(Candidate
_, TCErr
err)], []) -> do
          String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.instance" VerboseLevel
15 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
            TCM Doc
"findInstance 5: the only viable candidate failed..."
          TCErr -> TCMT IO (Maybe ([Candidate], Maybe MetaId))
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
        Just ([(Candidate, TCErr)]
errs, []) -> do
          if [(Candidate, TCErr)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Candidate, TCErr)]
errs then String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.instance" VerboseLevel
15 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"findInstance 5: no viable candidate found..."
                       else String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.instance" VerboseLevel
15 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"findInstance 5: all viable candidates failed..."
          -- #3676: Sort the candidates based on the size of the range for the errors and
          --        set the range of the full error to the range of the most precise candidate
          --        error.
          let sortedErrs :: [(Candidate, TCErr)]
sortedErrs = ((Candidate, TCErr) -> (Candidate, TCErr) -> Ordering)
-> [(Candidate, TCErr)] -> [(Candidate, TCErr)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (Int32 -> Int32 -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int32 -> Int32 -> Ordering)
-> ((Candidate, TCErr) -> Int32)
-> (Candidate, TCErr)
-> (Candidate, TCErr)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Candidate, TCErr) -> Int32
forall t a. HasRange t => (a, t) -> Int32
precision) [(Candidate, TCErr)]
errs
                where precision :: (a, t) -> Int32
precision (a
_, t
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
$ t -> Range' SrcFile
forall t. HasRange t => t -> Range' SrcFile
getRange t
err
                      infinity :: Int32
infinity = Int32
1000000000
          [TCErr]
-> TCMT IO (Maybe ([Candidate], Maybe MetaId))
-> TCMT IO (Maybe ([Candidate], Maybe MetaId))
forall (tcm :: * -> *) x a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm, HasRange x) =>
x -> tcm a -> tcm a
setCurrentRange (VerboseLevel -> [TCErr] -> [TCErr]
forall a. VerboseLevel -> [a] -> [a]
take VerboseLevel
1 ([TCErr] -> [TCErr]) -> [TCErr] -> [TCErr]
forall a b. (a -> b) -> a -> b
$ ((Candidate, TCErr) -> TCErr) -> [(Candidate, TCErr)] -> [TCErr]
forall a b. (a -> b) -> [a] -> [b]
map (Candidate, TCErr) -> TCErr
forall a b. (a, b) -> b
snd [(Candidate, TCErr)]
sortedErrs) (TCMT IO (Maybe ([Candidate], Maybe MetaId))
 -> TCMT IO (Maybe ([Candidate], Maybe MetaId)))
-> TCMT IO (Maybe ([Candidate], Maybe MetaId))
-> TCMT IO (Maybe ([Candidate], Maybe MetaId))
forall a b. (a -> b) -> a -> b
$
            TypeError -> TCMT IO (Maybe ([Candidate], Maybe MetaId))
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO (Maybe ([Candidate], Maybe MetaId)))
-> TypeError -> TCMT IO (Maybe ([Candidate], Maybe MetaId))
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)]
_, [Candidate Term
term Type
t' Bool
_]) -> do
          String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.instance" VerboseLevel
15 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
            [ TCM Doc
"findInstance 5: solved by instance search using the only candidate"
            , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
term
            , TCM Doc
"of type " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t'
            , TCM Doc
"for type" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
            ]

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

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

-- | Precondition: type is spine reduced and ends in a Def or a Var.
insidePi :: Type -> (Type -> TCM a) -> TCM a
insidePi :: Type -> (Type -> TCM a) -> TCM a
insidePi Type
t Type -> TCM a
ret =
  case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
    Pi Dom Type
a Abs Type
b     -> (String, Dom Type) -> TCM a -> TCM a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Abs Type -> String
forall a. Abs a -> String
absName Abs Type
b, Dom Type
a) (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ Type -> (Type -> TCM a) -> TCM a
forall a. Type -> (Type -> TCM a) -> TCM a
insidePi (Abs Type -> Type
forall t a. Subst t a => Abs a -> a
absBody Abs Type
b) Type -> TCM a
ret
    Def{}      -> Type -> TCM a
ret Type
t
    Var{}      -> Type -> TCM a
ret Type
t
    Sort{}     -> TCM a
forall a. HasCallStack => a
__IMPOSSIBLE__
    Con{}      -> TCM a
forall a. HasCallStack => a
__IMPOSSIBLE__
    Lam{}      -> TCM a
forall a. HasCallStack => a
__IMPOSSIBLE__
    Lit{}      -> TCM a
forall a. HasCallStack => a
__IMPOSSIBLE__
    Level{}    -> TCM a
forall a. HasCallStack => a
__IMPOSSIBLE__
    MetaV{}    -> TCM a
forall a. HasCallStack => a
__IMPOSSIBLE__
    DontCare{} -> TCM a
forall a. HasCallStack => a
__IMPOSSIBLE__
    Dummy String
s Elims
_  -> String -> TCM a
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ String
s

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 -> TCMT IO Bool) -> TCMT IO ()
forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> m Bool) -> m ()
wakeConstraints (Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TCMT IO Bool)
-> (ProblemConstraint -> Bool) -> ProblemConstraint -> TCMT IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Bool
isInstance)
    (ProblemConstraint -> Bool) -> Bool -> TCMT IO ()
forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> Bool) -> Bool -> m ()
solveSomeAwakeConstraints ProblemConstraint -> Bool
isInstance Bool
False
  where
    isInstance :: ProblemConstraint -> Bool
isInstance = 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

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

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