{-# LANGUAGE CPP #-}
{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.InstanceArguments
( findInstance
, isInstanceConstraint
, isConsideringInstance
, postponeInstanceConstraints
) where
#if MIN_VERSION_base(4,11,0)
import Prelude hiding ((<>))
#endif
import Control.Applicative hiding (empty)
import Control.Monad.Reader
import Control.Monad.State
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 Agda.Interaction.Options (optOverlappingInstances)
import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Internal as I
import Agda.Syntax.Scope.Base (isNameInScope)
import Agda.TypeChecking.Errors ()
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 Agda.TypeChecking.Free
import {-# SOURCE #-} Agda.TypeChecking.Constraints
import {-# SOURCE #-} Agda.TypeChecking.MetaVars
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.Functor
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Null (empty)
#include "undefined.h"
import Agda.Utils.Impossible
initialInstanceCandidates :: Type -> TCM (Maybe [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 -> do
reportSDoc "tc.instance.cands" 30 $ "Instance type is not yet known. "
return Nothing
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. "
maybeRight <$> runExceptT getContextVars
OutputTypeName n -> do
reportSDoc "tc.instance.cands" 30 $ "Found instance type head: " <+> prettyTCM n
runExceptT getContextVars >>= \case
Left b -> return Nothing
Right ctxVars -> Just . (ctxVars ++) <$> getScopeDefs n
where
getContextVars :: ExceptT Blocked_ TCM [Candidate]
getContextVars = do
ctx <- getContext
reportSDoc "tc.instance.cands" 40 $ hang "Getting candidates from context" 2 (inTopContext $ prettyTCM $ PrettyContext ctx)
let varsAndRaisedTypes = [ (var i, raise (i + 1) t) | (i, t) <- zip [0..] ctx ]
vars = [ Candidate x t (isOverlappable info)
| (x, Dom{domInfo = info, unDom = (_, t)}) <- varsAndRaisedTypes
, isInstance info
, usableRelevance info
, usableQuantity info
]
let cxtAndTypes = [ (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 v <+> ":"
, nest 2 $ prettyTCM t
]
| Candidate v t overlap <- fields
]
env <- asksTC envLetBindings
env <- mapM (getOpen . snd) $ Map.toList env
let lets = [ Candidate v t False
| (v, Dom{domInfo = info, unDom = t}) <- env
, isInstance info
, usableRelevance info
, usableQuantity info
]
return $ vars ++ fields ++ lets
etaExpand :: (MonadTCM m, MonadReduce m, HasConstInfo 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
if qnameToList r `List.isPrefixOf` mnameToList m
then return (Just (r, vs))
else return Nothing
r -> return r
instanceFields :: (Term,Type) -> ExceptT Blocked_ TCM [Candidate]
instanceFields = instanceFields' True
instanceFields' :: Bool -> (Term,Type) -> ExceptT Blocked_ TCM [Candidate]
instanceFields' etaOnce (v, t) =
ifBlockedType t (\m _ -> throwError $ Blocked m ()) $ \ _ t -> do
caseMaybeM (etaExpand etaOnce t) (return []) $ \ (r, pars) -> do
(tel, args) <- 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 (unArg arg) t (isOverlappable arg)
| isInstance arg ] ++) <$>
instanceFields' False (unArg arg, t)
getScopeDefs :: QName -> TCM [Candidate]
getScopeDefs n = do
instanceDefs <- getInstanceDefs
rel <- asksTC envRelevance
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
flip catchError handle $ do
def <- getConstInfo q
if not (defRelevance def `moreRelevant` rel) then return Nothing else do
args <- freeVarsToApply q
let t = defType def `piApply` args
let v = case theDef def of
Function{ funProjection = Just p } -> projDropParsApply p ProjSystem args
Constructor{ conSrcCon = c } -> Con c ConOSystem []
_ -> Def q $ map Apply args
return $ Just $ Candidate v t False
where
handle (TypeError _ (Closure {clValue = InternalError _})) = return Nothing
handle err = throwError err
findInstance :: MetaId -> Maybe [Candidate] -> TCM ()
findInstance m Nothing = do
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
TelV tel t <- telViewUpTo' (-1) notVisible t
cands <- addContext tel $ initialInstanceCandidates t
case cands of
Nothing -> do
reportSLn "tc.instance" 20 "Can't figure out target of instance goal. Postponing constraint."
addConstraint $ FindInstance m Nothing Nothing
Just {} -> findInstance m cands
findInstance m (Just cands) =
whenJustM (findInstance' m cands) $ (\ (cands, b) -> addConstraint $ FindInstance m b $ Just cands)
findInstance' :: MetaId -> [Candidate] -> TCM (Maybe ([Candidate], Maybe MetaId))
findInstance' m cands = ifM (isFrozen m) (do
reportSLn "tc.instance" 20 "Refusing to solve frozen instance meta."
return (Just (cands, Nothing))) $ do
ifM isConsideringInstance (do
reportSLn "tc.instance" 20 "Postponing possibly recursive instance search."
return $ Just (cands, Nothing)) $ billTo [Benchmark.Typing, Benchmark.InstanceSearch] $ do
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 v <+> ":"
, nest 2 $ prettyTCM t ] | Candidate v t overlap <- cands ]
reportSDoc "tc.instance" 70 $ "raw" $$ do
nest 2 $ vcat
[ sep [ (if overlap then "overlap" else empty) <+> pretty v <+> ":"
, nest 2 $ pretty t ] | Candidate v t overlap <- cands ]
t <- normalise =<< 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 <- 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..."
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 (_, [Candidate term t' _]) -> do
reportSDoc "tc.instance" 15 $ vcat
[ "findInstance 5: solved by instance search using the only candidate"
, nest 2 $ prettyTCM term
, "of type " <+> prettyTCM t'
, "for type" <+> prettyTCM t
]
wakeupInstanceConstraints
return Nothing
_ -> do
let cs = maybe cands snd mcands
reportSDoc "tc.instance" 15 $
text ("findInstance 5: refined candidates: ") <+>
prettyTCM (List.map candidateTerm cs)
return (Just (cs, Nothing))
insidePi :: Type -> (Type -> TCM a) -> TCM a
insidePi t ret =
case unEl t of
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
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)
a <- instantiateFull =<< (`piApplyM` ctxArgs) =<< getMetaType m
return (ok, v, a)
result <- mapM (\c -> do bs <- localTCStateSaving (tryC c); return (c, bs)) cands
case [ err | (_, ((HellNo err, _, _), _)) <- result ] of
err : _ -> throwError err
[] -> return ()
let result' = [ (c, v, a, s) | (c, ((r, v, a), 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)
dropSameCandidates :: MetaId -> [(Candidate, Term, Type, a)] -> TCM [(Candidate, Term, Type, a)]
dropSameCandidates m cands0 = verboseBracket "tc.instance" 30 "dropSameCandidates" $ do
metas <- getMetaVariableSet
let freshMetas = any ((`IntSet.notMember` metas) . metaId) . allMetas
let cands =
case List.partition (\ (c, _, _, _) -> candidateOverlappable c) cands0 of
(cand : _, []) -> [cand]
_ -> cands0
reportSDoc "tc.instance" 50 $ vcat
[ "valid candidates:"
, nest 2 $ vcat [ if freshMetas (v, a) then "(redacted)" else
sep [ prettyTCM v <+> ":", nest 2 $ prettyTCM a ]
| (_, v, a, _) <- cands ] ]
rel <- getMetaRelevance <$> lookupMeta m
case cands of
[] -> return cands
cvd : _ | isIrrelevant rel -> do
reportSLn "tc.instance" 30 "Meta is irrelevant so any candidate will do."
return [cvd]
(_, MetaV m' _, _, _) : _ | m == m' ->
return cands
cvd@(_, v, a, _) : vas -> do
if freshMetas (v, a)
then return (cvd : vas)
else (cvd :) <$> dropWhileM equal vas
where
equal (_, v', a', _)
| freshMetas (v', a') = return False
| otherwise =
verboseBracket "tc.instance" 30 "comparingCandidates" $ do
reportSDoc "tc.instance" 30 $ sep [ prettyTCM v <+> "==", nest 2 $ prettyTCM v' ]
localTCState $ dontAssignMetas $ ifNoConstraints_ (equalType a a' >> equalTerm a v v')
(return True)
(\ _ -> 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
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 v <+> ":" <+> prettyTCM t
| Candidate 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 v <+> ":" <+> prettyTCM t
| Candidate 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 term t' _) = checkDepth term t' $ do
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
]
(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
ctxElims <- map Apply <$> getContextArgs
guardConstraint (ValueCmp CmpEq t'' (MetaV m ctxElims) v) $ leqType t'' t
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
isConsideringInstance :: (ReadTCState m, HasOptions m) => m Bool
isConsideringInstance =
and2M ((^. stConsideringInstance) <$> getTCState)
(not . optOverlappingInstances <$> pragmaOptions)
nowConsideringInstance :: (MonadTCState m) => m a -> m a
nowConsideringInstance = locallyTCState stConsideringInstance $ const True
wakeupInstanceConstraints :: TCM ()
wakeupInstanceConstraints =
unlessM isConsideringInstance $ do
wakeConstraints (return . isInstance)
solveSomeAwakeConstraints isInstance False
where
isInstance = isInstanceConstraint . clValue . theConstraint
postponeInstanceConstraints :: TCM a -> TCM a
postponeInstanceConstraints m =
nowConsideringInstance m <* wakeupInstanceConstraints
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