{-# LANGUAGE CPP #-}
{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.InstanceArguments 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.Map as Map
import qualified Data.Set as Set
import qualified Data.List as List
import Agda.Syntax.Common
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 Agda.Utils.Except ( MonadError(catchError, throwError) )
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
initialIFSCandidates :: Type -> TCM (Maybe [Candidate])
initialIFSCandidates 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 -> return Nothing
OutputTypeVar -> Just <$> getContextVars
OutputTypeName n -> Just <$> do (++) <$> getContextVars <*> getScopeDefs n
where
getContextVars :: TCM [Candidate]
getContextVars = do
ctx <- getContext
reportSDoc "tc.instance.cands" 40 $ hang (text "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 ExplicitStayExplicit (isOverlappable info)
| (x, Dom info (_, t)) <- varsAndRaisedTypes
, isInstance info
, not (unusableRelevance info)
]
let cxtAndTypes = [ (x, t) | (x, Dom _ (_, t)) <- varsAndRaisedTypes ]
fields <- concat <$> mapM instanceFields (reverse cxtAndTypes)
reportSDoc "tc.instance.fields" 30 $
if null fields then text "no instance field candidates" else
text "instance field candidates" $$ do
nest 2 $ vcat
[ sep [ (if overlap then text "overlap" else empty) <+> prettyTCM v <+> text ":"
, nest 2 $ prettyTCM t
]
| Candidate v t _ overlap <- fields
]
env <- asks envLetBindings
env <- mapM (getOpen . snd) $ Map.toList env
let lets = [ Candidate v t ExplicitStayExplicit False
| (v, Dom info t) <- env
, isInstance info
, not (unusableRelevance info)
]
return $ vars ++ fields ++ lets
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 = instanceFields' True
instanceFields' etaOnce (v, t) =
caseMaybeM (etaExpand etaOnce =<< reduce 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 ExplicitStayExplicit (isOverlappable arg)
| isInstance arg ] ++) <$>
instanceFields' False (unArg arg, t)
getScopeDefs :: QName -> TCM [Candidate]
getScopeDefs n = do
instanceDefs <- getInstanceDefs
rel <- asks 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 ExplicitToInstance False
where
handle (TypeError _ (Closure {clValue = InternalError _})) = return Nothing
handle err = throwError err
findInScope :: MetaId -> Maybe [Candidate] -> TCM ()
findInScope m Nothing = do
mv <- lookupMeta m
setCurrentRange mv $ do
reportSLn "tc.instance" 20 $ "The type of the FindInScope constraint isn't known, trying to find it again."
t <- instantiate =<< getMetaTypeInContext m
reportSLn "tc.instance" 70 $ "findInScope 1: t: " ++ prettyShow t
TelV tel t <- telView t
cands <- addContext tel $ initialIFSCandidates t
case cands of
Nothing -> do
reportSLn "tc.instance" 20 "Can't figure out target of instance goal. Postponing constraint."
addConstraint $ FindInScope m Nothing Nothing
Just {} -> findInScope m cands
findInScope m (Just cands) =
whenJustM (findInScope' m cands) $ (\ (cands, b) -> addConstraint $ FindInScope m b $ Just cands)
findInScope' :: MetaId -> [Candidate] -> TCM (Maybe ([Candidate], Maybe MetaId))
findInScope' m cands = ifM (isFrozen m) (do
reportSLn "tc.instance" 20 "Refusing to solve frozen instance meta."
return (Just (cands, Nothing))) $ do
ifM (isFullyInstantiatedMeta m) (Nothing <$ reportSLn "tc.instance" 20 "Instance meta already solved.") $ do
mv <- lookupMeta m
setCurrentRange mv $ do
reportSLn "tc.instance" 15 $
"findInScope 2: constraint: " ++ prettyShow m ++ "; candidates left: " ++ show (length cands)
reportSDoc "tc.instance" 60 $ nest 2 $ vcat
[ sep [ (if overlap then text "overlap" else empty) <+> prettyTCM v <+> text ":"
, nest 2 $ prettyTCM t ] | Candidate v t _ overlap <- cands ]
reportSDoc "tc.instance" 70 $ text "raw" $$ do
nest 2 $ vcat
[ sep [ (if overlap then text "overlap" else empty) <+> pretty v <+> text ":"
, nest 2 $ pretty t ] | Candidate v t _ overlap <- cands ]
t <- normalise =<< getMetaTypeInContext m
reportSLn "tc.instance" 70 $ "findInScope 2: t: " ++ prettyShow t
insidePi t $ \ t -> do
reportSDoc "tc.instance" 15 $ text "findInScope 3: t =" <+> prettyTCM t
reportSLn "tc.instance" 70 $ "findInScope 3: t: " ++ prettyShow t
let abortNonRigid m = do
reportSLn "tc.instance" 15 $
"aborting due to non-rigidly constrained meta " ++ show m
return $ Just (cands, Just m)
ifJustM (areThereNonRigidMetaArguments (unEl t)) abortNonRigid $ do
mcands <- checkCandidates m t cands
debugConstraints
case mcands of
Just [] -> do
reportSDoc "tc.instance" 15 $
text "findInScope 5: not a single candidate found..."
typeError $ IFSNoCandidateInScope t
Just [Candidate term t' _ _] -> do
reportSDoc "tc.instance" 15 $ vcat
[ text "findInScope 5: solved by instance search using the only candidate"
, nest 2 $ prettyTCM term
, text "of type " <+> prettyTCM t'
, text "for type" <+> prettyTCM t
]
wakeConstraints (return . const True)
solveAwakeConstraints' False
return Nothing
_ -> do
let cs = fromMaybe cands mcands
reportSDoc "tc.instance" 15 $
text ("findInScope 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__
rigidlyConstrainedMetas :: TCM [MetaId]
rigidlyConstrainedMetas = do
cs <- (++) <$> use stSleepingConstraints <*> use stAwakeConstraints
catMaybes <$> mapM rigidMetas cs
where
isRigid v = do
bv <- reduceB v
case bv of
Blocked{} -> return False
NotBlocked _ v -> case v of
MetaV{} -> return False
Def f _ -> return True
Con{} -> return True
Lit{} -> return True
Var{} -> return True
Sort{} -> return True
Pi{} -> return True
Level{} -> return False
DontCare{} -> return False
Lam{} -> __IMPOSSIBLE__
rigidMetas c =
case clValue $ theConstraint c of
ValueCmp _ _ u v ->
case (u, v) of
(MetaV m us, _) | isJust (allApplyElims us) -> ifM (isRigid v) (return $ Just m) (return Nothing)
(_, MetaV m vs) | isJust (allApplyElims vs) -> ifM (isRigid u) (return $ Just m) (return Nothing)
_ -> return Nothing
ElimCmp{} -> return Nothing
TypeCmp{} -> return Nothing
TelCmp{} -> return Nothing
SortCmp{} -> return Nothing
LevelCmp{} -> return Nothing
UnBlock{} -> return Nothing
Guarded{} -> return Nothing
IsEmpty{} -> return Nothing
CheckSizeLtSat{} -> return Nothing
FindInScope{} -> return Nothing
CheckFunDef{} -> return Nothing
HasBiggerSort{} -> return Nothing
HasPTSRule{} -> return Nothing
isRigid :: MetaId -> TCM Bool
isRigid i = do
rigid <- rigidlyConstrainedMetas
return (elem i rigid)
areThereNonRigidMetaArguments :: Term -> TCM (Maybe MetaId)
areThereNonRigidMetaArguments t = case t of
Def n args -> do
TelV tel _ <- telView . defType =<< getConstInfo n
let varOccs EmptyTel = []
varOccs (ExtendTel a btel)
| getRelevance a == Irrelevant = WeaklyRigid : varOccs tel
| otherwise = occurrence 0 tel : varOccs tel
where tel = unAbs btel
rigid StronglyRigid = True
rigid Unguarded = True
rigid WeaklyRigid = True
rigid _ = False
reportSDoc "tc.instance.rigid" 70 $ text "class args:" <+> prettyTCM tel $$
nest 2 (text $ "used: " ++ show (varOccs tel))
areThereNonRigidMetaArgs [ arg | (o, arg) <- zip (varOccs tel) args, not $ rigid o ]
Var n args -> return Nothing
Sort{} -> __IMPOSSIBLE__
Con{} -> __IMPOSSIBLE__
Lam{} -> __IMPOSSIBLE__
Lit{} -> __IMPOSSIBLE__
Level{} -> __IMPOSSIBLE__
MetaV{} -> __IMPOSSIBLE__
Pi{} -> __IMPOSSIBLE__
DontCare{} -> __IMPOSSIBLE__
where
areThereNonRigidMetaArgs :: Elims -> TCM (Maybe MetaId)
areThereNonRigidMetaArgs [] = return Nothing
areThereNonRigidMetaArgs (Proj{} : xs) = areThereNonRigidMetaArgs xs
areThereNonRigidMetaArgs (Apply x : xs) = do
ifJustM (isNonRigidMeta $ unArg x) (return . Just) (areThereNonRigidMetaArgs xs)
isNonRigidMeta :: Term -> TCM (Maybe MetaId)
isNonRigidMeta v =
case v of
Def _ es -> areThereNonRigidMetaArgs es
Var _ es -> areThereNonRigidMetaArgs es
Con _ _ vs-> areThereNonRigidMetaArgs vs
MetaV i _ -> ifM (isRigid i) (return Nothing) $ do
mlvl <- getBuiltinDefName builtinLevel
(msz, mszlt) <- getBuiltinSize
let ok = catMaybes [ mlvl, msz ]
o <- getOutputTypeName . jMetaType . mvJudgement =<< lookupMeta i
case o of
OutputTypeName l | elem l ok -> return Nothing
_ -> return $ Just i
Lam _ t -> isNonRigidMeta (unAbs t)
_ -> return Nothing
filterResetingState :: MetaId -> [Candidate] -> (Candidate -> TCM YesNoMaybe) -> TCM [Candidate]
filterResetingState m cands f = disableDestructiveUpdate $ 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) ]
noMaybes = null [ Maybe | (_, ((Maybe, _, _), _)) <- result ]
result <- if noMaybes then dropSameCandidates m result' else return result'
case result of
[(c, _, _, s)] -> [c] <$ put s
_ -> return [ c | (c, _, _, _) <- result ]
dropSameCandidates :: MetaId -> [(Candidate, Term, Type, a)] -> TCM [(Candidate, Term, Type, a)]
dropSameCandidates m cands0 = verboseBracket "tc.instance" 30 "dropSameCandidates" $ do
metas <- Set.fromList . Map.keys <$> getMetaStore
let freshMetas x = not $ Set.null $ Set.difference (Set.fromList $ allMetas x) metas
let cands =
case List.partition (\ (c, _, _, _) -> candidateOverlappable c) cands0 of
(cand : _, []) -> [cand]
_ -> cands0
reportSDoc "tc.instance" 50 $ vcat
[ text "valid candidates:"
, nest 2 $ vcat [ if freshMetas (v, a) then text "(redacted)" else
sep [ prettyTCM v <+> text ":", 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]
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 <+> text "==", 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 | Maybe | HellNo TCErr
deriving (Show)
isNo :: YesNoMaybe -> Bool
isNo No = True
isNo _ = False
checkCandidates :: MetaId -> Type -> [Candidate] -> TCM (Maybe [Candidate])
checkCandidates m t cands = disableDestructiveUpdate $
verboseBracket "tc.instance.candidates" 20 ("checkCandidates " ++ prettyShow m) $
ifM (anyMetaTypes cands) (return Nothing) $
holdConstraints (\ _ -> isIFSConstraint . clValue . theConstraint) $ Just <$> do
reportSDoc "tc.instance.candidates" 20 $ nest 2 $ text "target:" <+> prettyTCM t
reportSDoc "tc.instance.candidates" 20 $ nest 2 $ vcat
[ text "candidates"
, vcat [ text "-" <+> (if overlap then text "overlap" else empty) <+> prettyTCM v <+> text ":" <+> prettyTCM t
| Candidate v t _ overlap <- cands ] ]
cands' <- filterResetingState m cands (checkCandidateForMeta m t)
reportSDoc "tc.instance.candidates" 20 $ nest 2 $ vcat
[ text "valid candidates"
, vcat [ text "-" <+> (if overlap then text "overlap" else empty) <+> prettyTCM v <+> text ":" <+> prettyTCM t
| Candidate v t _ overlap <- 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 = locally eInstanceDepth succ $ do
d <- view eInstanceDepth
maxDepth <- maxInstanceSearchDepth
when (d > maxDepth) $ typeError $ InstanceSearchDepthExhausted c a maxDepth
k
checkCandidateForMeta :: MetaId -> Type -> Candidate -> TCM YesNoMaybe
checkCandidateForMeta m t (Candidate term t' eti _) = 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
[ text "checkCandidateForMeta"
, text "t =" <+> prettyTCM t
, text "t' =" <+> prettyTCM t'
, text "term =" <+> prettyTCM term
]
(args, t'') <- implicitArgs (-1) (\h -> notVisible h || eti == ExplicitToInstance) t'
reportSDoc "tc.instance" 20 $
text "instance search: checking" <+> prettyTCM t''
<+> text "<=" <+> prettyTCM t
reportSDoc "tc.instance" 70 $ vcat
[ text "instance search: checking (raw)"
, nest 4 $ pretty t''
, nest 2 $ text "<="
, nest 4 $ pretty t
]
v <- (`applyDroppingParameters` args) =<< reduce term
reportSDoc "tc.instance" 15 $ vcat
[ text "instance search: attempting"
, nest 2 $ prettyTCM m <+> text ":=" <+> prettyTCM v
]
reportSDoc "tc.instance" 70 $ nest 2 $
text "candidate v = " <+> pretty v
ctxElims <- map Apply <$> getContextArgs
guardConstraint (ValueCmp CmpEq t'' (MetaV m ctxElims) v) $ leqType t'' t
debugConstraints
solveAwakeConstraints' True
verboseS "tc.instance" 15 $ do
sol <- instantiateFull (MetaV m ctxElims)
case sol of
MetaV m' _ | m == m' ->
reportSDoc "tc.instance" 15 $
sep [ text "instance search: maybe solution for" <+> prettyTCM m <> text ":"
, nest 2 $ prettyTCM v ]
_ ->
reportSDoc "tc.instance" 15 $
sep [ text "instance search: found solution for" <+> prettyTCM m <> text ":"
, nest 2 $ prettyTCM sol ]
where
runCandidateCheck check =
flip catchError handle $
ifNoConstraints_ check
(return Yes)
(\ _ -> Maybe <$ reportSLn "tc.instance" 50 "assignment inconclusive")
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 = do
reportSDoc "tc.instance" 50 $
text "assignment failed:" <+> prettyTCM err
return No
isIFSConstraint :: Constraint -> Bool
isIFSConstraint FindInScope{} = True
isIFSConstraint UnBlock{} = True
isIFSConstraint _ = False
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