Agda-2.6.2: src/full/Agda/TypeChecking/InstanceArguments.hs
{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.InstanceArguments
( findInstance
, isInstanceConstraint
, shouldPostponeInstanceSearch
, postponeInstanceConstraints
) where
import Control.Monad.Except
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.Bifunctor
import Data.Foldable (toList)
import Data.Function (on)
import Data.Monoid hiding ((<>))
import Agda.Interaction.Options (optOverlappingInstances, optQualifiedInstances)
import Agda.Syntax.Common
import Agda.Syntax.Concrete.Name (isQualified)
import Agda.Syntax.Position
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.MetaVars
import Agda.Syntax.Scope.Base (isNameInScope, inverseScopeLookupName', AllowAmbiguousNames(..))
import Agda.TypeChecking.Errors () --instance only
import Agda.TypeChecking.Implicit (implicitArgs)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Records
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import {-# SOURCE #-} Agda.TypeChecking.Constraints
import {-# SOURCE #-} Agda.TypeChecking.Conversion
import qualified Agda.Benchmarking as Benchmark
import Agda.TypeChecking.Monad.Benchmark (billTo)
import Agda.Utils.Either
import Agda.Utils.Lens
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Null (empty)
import Agda.Utils.Impossible
-- | Compute a list of instance candidates.
-- 'Nothing' if target type or any context type is a meta, error if
-- type is not eligible for instance search.
initialInstanceCandidates :: Type -> TCM (Either Blocker [Candidate])
initialInstanceCandidates t = do
(_ , otn) <- getOutputTypeName t
case otn of
NoOutputTypeName -> typeError $ GenericError $
"Instance search can only be used to find elements in a named type"
OutputTypeNameNotYetKnown b -> do
reportSDoc "tc.instance.cands" 30 $ "Instance type is not yet known. "
return (Left b)
OutputTypeVisiblePi -> typeError $ GenericError $
"Instance search cannot be used to find elements in an explicit function type"
OutputTypeVar -> do
reportSDoc "tc.instance.cands" 30 $ "Instance type is a variable. "
runBlocked getContextVars
OutputTypeName n -> do
reportSDoc "tc.instance.cands" 30 $ "Found instance type head: " <+> prettyTCM n
runBlocked getContextVars >>= \case
Left b -> return $ Left b
Right ctxVars -> Right . (ctxVars ++) <$> getScopeDefs n
where
-- get a list of variables with their type, relative to current context
getContextVars :: BlockT TCM [Candidate]
getContextVars = do
ctx <- getContext
reportSDoc "tc.instance.cands" 40 $ hang "Getting candidates from context" 2 (inTopContext $ prettyTCM $ PrettyContext ctx)
-- Context variables with their types lifted to live in the full context
let varsAndRaisedTypes = [ (var i, raise (i + 1) t) | (i, t) <- zip [0..] ctx ]
vars = [ Candidate LocalCandidate x t (isOverlappable info)
| (x, Dom{domInfo = info, unDom = (_, t)}) <- varsAndRaisedTypes
, isInstance info
, usableModality info
]
-- {{}}-fields of variables are also candidates
let cxtAndTypes = [ (LocalCandidate, x, t) | (x, Dom{unDom = (_, t)}) <- varsAndRaisedTypes ]
fields <- concat <$> mapM instanceFields (reverse cxtAndTypes)
reportSDoc "tc.instance.fields" 30 $
if null fields then "no instance field candidates" else
"instance field candidates" $$ do
nest 2 $ vcat
[ sep [ (if overlap then "overlap" else empty) <+> prettyTCM c <+> ":"
, nest 2 $ prettyTCM t
]
| c@(Candidate q v t overlap) <- fields
]
-- get let bindings
env <- asksTC envLetBindings
env <- mapM (traverse getOpen) $ Map.toList env
let lets = [ Candidate LocalCandidate v t False
| (_,(v, Dom{domInfo = info, unDom = t})) <- env
, isInstance info
, usableModality info
]
return $ vars ++ fields ++ lets
etaExpand :: (MonadTCM m, PureTCM m)
=> Bool -> Type -> m (Maybe (QName, Args))
etaExpand etaOnce t =
isEtaRecordType t >>= \case
Nothing | etaOnce -> do
isRecordType t >>= \case
Nothing -> return Nothing
Just (r, vs, _) -> do
m <- currentModule
-- Are we inside the record module? If so it's safe and desirable
-- to eta-expand once (issue #2320).
if qnameToList0 r `List.isPrefixOf` mnameToList m
then return (Just (r, vs))
else return Nothing
r -> return r
instanceFields :: (CandidateKind,Term,Type) -> BlockT TCM [Candidate]
instanceFields = instanceFields' True
instanceFields' :: Bool -> (CandidateKind,Term,Type) -> BlockT TCM [Candidate]
instanceFields' etaOnce (q, v, t) =
ifBlocked t (\ m _ -> patternViolation m) $ \ _ t -> do
caseMaybeM (etaExpand etaOnce t) (return []) $ \ (r, pars) -> do
(tel, args) <- lift $ forceEtaExpandRecord r pars v
let types = map unDom $ applySubst (parallelS $ reverse $ map unArg args) (flattenTel tel)
fmap concat $ forM (zip args types) $ \ (arg, t) ->
([ Candidate LocalCandidate (unArg arg) t (isOverlappable arg)
| isInstance arg ] ++) <$>
instanceFields' False (LocalCandidate, unArg arg, t)
getScopeDefs :: QName -> TCM [Candidate]
getScopeDefs n = do
instanceDefs <- getInstanceDefs
rel <- asksTC getRelevance
let qs = maybe [] Set.toList $ Map.lookup n instanceDefs
catMaybes <$> mapM (candidate rel) qs
candidate :: Relevance -> QName -> TCM (Maybe Candidate)
candidate rel q = ifNotM (isNameInScope q <$> getScope) (return Nothing) $ do
-- Jesper, 2020-03-16: When using --no-qualified-instances,
-- filter out instances that are only in scope under a qualified
-- name.
filterQualified $ 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)
flip catchError handle $ do
def <- getConstInfo q
if not (getRelevance def `moreRelevant` rel) then return 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 <- freeVarsToApply q
let t = defType def `piApply` args
rel = getRelevance $ defArgInfo def
let v = case theDef def of
-- drop parameters if it's a projection function...
Function{ funProjection = Just p } -> projDropParsApply p ProjSystem rel 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 = c } -> Con c ConOSystem []
_ -> Def q $ map Apply args
return $ Just $ Candidate (GlobalCandidate q) v t False
where
-- unbound constant throws an internal error
handle (TypeError _ _ (Closure {clValue = InternalError _})) = return Nothing
handle err = throwError err
filterQualified :: TCM (Maybe Candidate) -> TCM (Maybe Candidate)
filterQualified m = ifM (optQualifiedInstances <$> pragmaOptions) m $ do
qc <- inverseScopeLookupName' AmbiguousAnything q <$> getScope
let isQual = maybe True isQualified $ listToMaybe qc
reportSDoc "tc.instance.qualified" 30 $
if isQual then
"dropping qualified instance" <+> prettyTCM q
else
"keeping instance" <+> prettyTCM q <+>
"since it is in scope as" <+> prettyTCM qc
if isQual then return Nothing else m
-- | @findInstance m (v,a)s@ tries to instantiate on of the types @a@s
-- of the candidate terms @v@s to the type @t@ of the metavariable @m@.
-- If successful, meta @m@ is solved with the instantiation of @v@.
-- If unsuccessful, the constraint is regenerated, with possibly reduced
-- candidate set.
-- The list of candidates is equal to @Nothing@ when the type of the meta
-- wasn't known when the constraint was generated. In that case, try to find
-- its type again.
findInstance :: MetaId -> Maybe [Candidate] -> TCM ()
findInstance m Nothing = do
-- Andreas, 2015-02-07: New metas should be created with range of the
-- current instance meta, thus, we set the range.
mv <- lookupMeta m
setCurrentRange mv $ do
reportSLn "tc.instance" 20 $ "The type of the FindInstance constraint isn't known, trying to find it again."
t <- instantiate =<< getMetaTypeInContext m
reportSLn "tc.instance" 70 $ "findInstance 1: t: " ++ prettyShow 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 tel t <- telViewUpTo' (-1) notVisible t
cands <- addContext tel $ initialInstanceCandidates t
case cands of
Left unblock -> do
reportSLn "tc.instance" 20 "Can't figure out target of instance goal. Postponing constraint."
addConstraint unblock $ FindInstance m Nothing
Right cs -> findInstance m (Just cs)
findInstance m (Just cands) = -- Note: if no blocking meta variable this will not unblock until the end of the mutual block
whenJustM (findInstance' m cands) $ (\ (cands, b) -> addConstraint b $ FindInstance m $ Just cands)
-- | Result says whether we need to add constraint, and if so, the set of
-- remaining candidates and an eventual blocking metavariable.
findInstance' :: MetaId -> [Candidate] -> TCM (Maybe ([Candidate], Blocker))
findInstance' m cands = ifM (isFrozen m) (do
reportSLn "tc.instance" 20 "Refusing to solve frozen instance meta."
return (Just (cands, neverUnblock))) $ do
ifM shouldPostponeInstanceSearch (do
reportSLn "tc.instance" 20 "Postponing possibly recursive instance search."
return $ Just (cands, neverUnblock)) $ billTo [Benchmark.Typing, Benchmark.InstanceSearch] $ do
-- Andreas, 2015-02-07: New metas should be created with range of the
-- current instance meta, thus, we set the range.
mv <- lookupMeta m
setCurrentRange mv $ do
reportSLn "tc.instance" 15 $
"findInstance 2: constraint: " ++ prettyShow m ++ "; candidates left: " ++ show (length cands)
reportSDoc "tc.instance" 60 $ nest 2 $ vcat
[ sep [ (if overlap then "overlap" else empty) <+> prettyTCM c <+> ":"
, nest 2 $ prettyTCM t ] | c@(Candidate q v t overlap) <- cands ]
reportSDoc "tc.instance" 70 $ "raw" $$ do
nest 2 $ vcat
[ sep [ (if overlap then "overlap" else empty) <+> prettyTCM c <+> ":"
, nest 2 $ pretty t ] | c@(Candidate q v t overlap) <- cands ]
t <- getMetaTypeInContext m
reportSLn "tc.instance" 70 $ "findInstance 2: t: " ++ prettyShow t
insidePi t $ \ t -> do
reportSDoc "tc.instance" 15 $ "findInstance 3: t =" <+> prettyTCM t
reportSLn "tc.instance" 70 $ "findInstance 3: t: " ++ prettyShow t
mcands <-
-- Temporarily remove other instance constraints to avoid
-- redundant solution attempts
holdConstraints (const isInstanceProblemConstraint) $
checkCandidates m t cands
debugConstraints
case mcands of
Just ([(_, err)], []) -> do
reportSDoc "tc.instance" 15 $
"findInstance 5: the only viable candidate failed..."
throwError err
Just (errs, []) -> do
if null errs then reportSDoc "tc.instance" 15 $ "findInstance 5: no viable candidate found..."
else reportSDoc "tc.instance" 15 $ "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 = List.sortBy (compare `on` precision) errs
where precision (_, err) = maybe infinity iLength $ rangeToInterval $ getRange err
infinity = 1000000000
setCurrentRange (take 1 $ map snd sortedErrs) $
typeError $ InstanceNoCandidate t [ (candidateTerm c, err) | (c, err) <- sortedErrs ]
Just (_, [c@(Candidate q term t' _)]) -> do
reportSDoc "tc.instance" 15 $ vcat
[ "findInstance 5: solved by instance search using the only candidate"
, nest 2 $ prettyTCM c <+> "=" <+> prettyTCM term
, "of type " <+> prettyTCM t'
, "for type" <+> prettyTCM t
]
-- If we actually solved the constraints we should wake up any held
-- instance constraints, to make sure we don't forget about them.
wakeupInstanceConstraints
return Nothing -- We’re done
_ -> do
let cs = maybe cands snd mcands -- keep the current candidates if Nothing
reportSDoc "tc.instance" 15 $
text ("findInstance 5: refined candidates: ") <+>
prettyTCM (List.map candidateTerm cs)
return (Just (cs, neverUnblock))
insidePi :: Type -> (Type -> TCM a) -> TCM a
insidePi t ret = reduce (unEl t) >>= \case
Pi a b -> addContext (absName b, a) $ insidePi (absBody b) ret
Def{} -> ret t
Var{} -> ret t
Sort{} -> __IMPOSSIBLE__
Con{} -> __IMPOSSIBLE__
Lam{} -> __IMPOSSIBLE__
Lit{} -> __IMPOSSIBLE__
Level{} -> __IMPOSSIBLE__
MetaV{} -> __IMPOSSIBLE__
DontCare{} -> __IMPOSSIBLE__
Dummy s _ -> __IMPOSSIBLE_VERBOSE__ 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 m cands f = do
ctxArgs <- getContextArgs
let ctxElims = map Apply ctxArgs
tryC c = do
ok <- f c
v <- instantiateFull (MetaV m ctxElims)
return (ok, v)
result <- mapM (\c -> do bs <- localTCStateSaving (tryC c); return (c, bs)) cands
-- Check that there aren't any hard failures
case [ err | (_, ((HellNo err, _), _)) <- result ] of
err : _ -> throwError err
[] -> return ()
-- c : Candidate
-- r : YesNoMaybe
-- v : Term (fully instantiated)
-- a : Type (fully instantiated)
-- s : TCState
let result' = [ (c, v, s) | (c, ((r, v), s)) <- result, not (isNo r) ]
result'' <- dropSameCandidates m result'
case result'' of
[(c, _, s)] -> ([], [c]) <$ putTC s
_ -> do
let bad = [ (c, err) | (c, ((NoBecause err, _), _)) <- result ]
good = [ c | (c, _, _) <- result'' ]
return (bad, good)
-- Drop all candidates which are judgmentally equal to the first one.
-- This is sufficient to reduce the list to a singleton should all be equal.
dropSameCandidates :: MetaId -> [(Candidate, Term, a)] -> TCM [(Candidate, Term, a)]
dropSameCandidates m cands0 = verboseBracket "tc.instance" 30 "dropSameCandidates" $ do
metas <- getMetaVariableSet
-- Does `it` have any metas in the initial meta variable store?
let freshMetas = getAny . allMetas (Any . (`IntSet.notMember` metas) . metaId)
-- Take overlappable candidates into account
let cands =
case List.partition (\ (c, _, _) -> candidateOverlappable c) cands0 of
(cand : _, []) -> [cand] -- only overlappable candidates: pick the first one
_ -> cands0 -- otherwise require equality
reportSDoc "tc.instance" 50 $ vcat
[ "valid candidates:"
, nest 2 $ vcat [ if freshMetas v then "(redacted)" else
sep [ prettyTCM v ]
| (_, v, _) <- cands ] ]
rel <- getMetaRelevance <$> lookupMeta m
case cands of
[] -> return cands
cvd : _ | isIrrelevant rel -> do
reportSLn "tc.instance" 30 "dropSameCandidates: Meta is irrelevant so any candidate will do."
return [cvd]
(_, MetaV m' _, _) : _ | m == m' -> do -- We didn't instantiate, so can't compare
reportSLn "tc.instance" 30 "dropSameCandidates: Meta was not instantiated so we don't filter equal candidates yet"
return cands
cvd@(_, v, _) : vas
| freshMetas v -> do
reportSLn "tc.instance" 30 "dropSameCandidates: Solution of instance meta has fresh metas so we don't filter equal candidates yet"
return (cvd : vas)
| otherwise -> (cvd :) <$> dropWhileM equal vas
where
equal :: (Candidate, Term, a) -> TCM Bool
equal (_, v', _)
| freshMetas v' = return False -- If there are fresh metas we can't compare
| otherwise =
verboseBracket "tc.instance" 30 "dropSameCandidates: " $ do
reportSDoc "tc.instance" 30 $ sep [ prettyTCM v <+> "==", nest 2 $ prettyTCM v' ]
a <- uncurry piApplyM =<< ((,) <$> getMetaType m <*> getContextArgs)
localTCState $ dontAssignMetas $ ifNoConstraints_ (equalTerm a v v')
{- then -} (return True)
{- else -} (\ _ -> return False)
`catchError` (\ _ -> return False)
data YesNoMaybe = Yes | No | NoBecause TCErr | Maybe | HellNo TCErr
deriving (Show)
isNo :: YesNoMaybe -> Bool
isNo No = True
isNo NoBecause{} = True
isNo HellNo{} = True
isNo _ = 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 m t cands =
verboseBracket "tc.instance.candidates" 20 ("checkCandidates " ++ prettyShow m) $
ifM (anyMetaTypes cands) (return Nothing) $ Just <$> do
reportSDoc "tc.instance.candidates" 20 $ nest 2 $ "target:" <+> prettyTCM t
reportSDoc "tc.instance.candidates" 20 $ nest 2 $ vcat
[ "candidates"
, vcat [ "-" <+> (if overlap then "overlap" else empty) <+> prettyTCM c <+> ":" <+> prettyTCM t
| c@(Candidate q v t overlap) <- cands ] ]
cands' <- filterResetingState m cands (checkCandidateForMeta m t)
reportSDoc "tc.instance.candidates" 20 $ nest 2 $ vcat
[ "valid candidates"
, vcat [ "-" <+> (if overlap then "overlap" else empty) <+> prettyTCM c <+> ":" <+> prettyTCM t
| c@(Candidate q v t overlap) <- snd cands' ] ]
reportSDoc "tc.instance.candidates" 60 $ nest 2 $ vcat
[ "valid candidates"
, vcat [ "-" <+> (if overlap then "overlap" else empty) <+> prettyTCM v <+> ":" <+> prettyTCM t
| c@(Candidate q v t overlap) <- snd cands' ] ]
return cands'
where
anyMetaTypes :: [Candidate] -> TCM Bool
anyMetaTypes [] = return False
anyMetaTypes (Candidate _ _ a _ : cands) = do
a <- instantiate a
case unEl a of
MetaV{} -> return True
_ -> anyMetaTypes cands
checkDepth :: Term -> Type -> TCM YesNoMaybe -> TCM YesNoMaybe
checkDepth c a k = locallyTC eInstanceDepth succ $ do
d <- viewTC eInstanceDepth
maxDepth <- maxInstanceSearchDepth
when (d > maxDepth) $ typeError $ InstanceSearchDepthExhausted c a maxDepth
k
checkCandidateForMeta :: MetaId -> Type -> Candidate -> TCM YesNoMaybe
checkCandidateForMeta m t (Candidate q term t' _) = checkDepth term t' $ do
-- Andreas, 2015-02-07: New metas should be created with range of the
-- current instance meta, thus, we set the range.
mv <- lookupMeta m
setCurrentRange mv $ do
debugConstraints
verboseBracket "tc.instance" 20 ("checkCandidateForMeta " ++ prettyShow m) $
liftTCM $ runCandidateCheck $ do
reportSLn "tc.instance" 70 $ " t: " ++ prettyShow t ++ "\n t':" ++ prettyShow t' ++ "\n term: " ++ prettyShow term ++ "."
reportSDoc "tc.instance" 20 $ vcat
[ "checkCandidateForMeta"
, "t =" <+> prettyTCM t
, "t' =" <+> prettyTCM t'
, "term =" <+> prettyTCM term
]
-- Apply hidden and instance arguments (recursive inst. search!).
(args, t'') <- implicitArgs (-1) (\h -> notVisible h) t'
reportSDoc "tc.instance" 20 $
"instance search: checking" <+> prettyTCM t''
<+> "<=" <+> prettyTCM t
reportSDoc "tc.instance" 70 $ vcat
[ "instance search: checking (raw)"
, nest 4 $ pretty t''
, nest 2 $ "<="
, nest 4 $ pretty t
]
v <- (`applyDroppingParameters` args) =<< reduce term
reportSDoc "tc.instance" 15 $ vcat
[ "instance search: attempting"
, nest 2 $ prettyTCM m <+> ":=" <+> prettyTCM v
]
reportSDoc "tc.instance" 70 $ nest 2 $
"candidate v = " <+> pretty 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).
ctxElims <- map Apply <$> getContextArgs
guardConstraint (ValueCmp CmpEq (AsTermsOf t'') (MetaV m ctxElims) v) $ leqType t'' 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.
debugConstraints
let debugSolution = verboseS "tc.instance" 15 $ do
sol <- instantiateFull (MetaV m ctxElims)
case sol of
MetaV m' _ | m == m' ->
reportSDoc "tc.instance" 15 $
sep [ ("instance search: maybe solution for" <+> prettyTCM m) <> ":"
, nest 2 $ prettyTCM v ]
_ ->
reportSDoc "tc.instance" 15 $
sep [ ("instance search: found solution for" <+> prettyTCM m) <> ":"
, nest 2 $ prettyTCM sol ]
do solveAwakeConstraints' True
Yes <$ debugSolution
`catchError` (return . NoBecause)
where
runCandidateCheck check =
flip catchError handle $
nowConsideringInstance $
ifNoConstraints check
(\ r -> case r of
Yes -> r <$ debugSuccess
NoBecause why -> r <$ debugConstraintFail why
_ -> __IMPOSSIBLE__
)
(\ _ r -> case r of
Yes -> Maybe <$ debugInconclusive
NoBecause why -> r <$ debugConstraintFail why
_ -> __IMPOSSIBLE__
)
debugSuccess = reportSLn "tc.instance" 50 "assignment successful" :: TCM ()
debugInconclusive = reportSLn "tc.instance" 50 "assignment inconclusive" :: TCM ()
debugConstraintFail why = reportSDoc "tc.instance" 50 $ "candidate failed constraints:" <+> prettyTCM why
debugTypeFail err = reportSDoc "tc.instance" 50 $ "candidate failed type check:" <+> prettyTCM err
hardFailure :: TCErr -> Bool
hardFailure (TypeError _ _ err) =
case clValue err of
InstanceSearchDepthExhausted{} -> True
_ -> False
hardFailure _ = False
handle :: TCErr -> TCM YesNoMaybe
handle err
| hardFailure err = return $ HellNo err
| otherwise = No <$ debugTypeFail err
isInstanceConstraint :: Constraint -> Bool
isInstanceConstraint FindInstance{} = True
isInstanceConstraint _ = False
shouldPostponeInstanceSearch :: (ReadTCState m, HasOptions m) => m Bool
shouldPostponeInstanceSearch =
and2M ((^. stConsideringInstance) <$> getTCState)
(not . optOverlappingInstances <$> pragmaOptions)
`or2M` ((^. stPostponeInstanceSearch) <$> getTCState)
nowConsideringInstance :: (ReadTCState m) => m a -> m a
nowConsideringInstance = locallyTCState stConsideringInstance $ const True
isInstanceProblemConstraint :: ProblemConstraint -> Bool
isInstanceProblemConstraint = isInstanceConstraint . clValue . theConstraint
wakeupInstanceConstraints :: TCM ()
wakeupInstanceConstraints =
unlessM shouldPostponeInstanceSearch $ do
wakeConstraints (wakeUpWhen_ isInstanceProblemConstraint)
solveSomeAwakeConstraints isInstanceProblemConstraint False
postponeInstanceConstraints :: TCM a -> TCM a
postponeInstanceConstraints m =
locallyTCState stPostponeInstanceSearch (const True) m <* 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 t vs = do
let fallback = return $ t `apply` vs
case t of
Con c ci [] -> do
def <- theDef <$> getConInfo c
case def of
Constructor {conPars = n} -> return $ Con c ci (map Apply $ drop n vs)
_ -> __IMPOSSIBLE__
Def f [] -> do
mp <- isProjection f
case mp of
Just Projection{projIndex = n} -> do
case drop n vs of
[] -> return t
u : us -> (`apply` us) <$> applyDef ProjPrefix f u
_ -> fallback
_ -> fallback