summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/InstanceArguments.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/InstanceArguments.hs')
-rw-r--r--src/full/Agda/TypeChecking/InstanceArguments.hs145
1 files changed, 108 insertions, 37 deletions
diff --git a/src/full/Agda/TypeChecking/InstanceArguments.hs b/src/full/Agda/TypeChecking/InstanceArguments.hs
index bf49093..1698f91 100644
--- a/src/full/Agda/TypeChecking/InstanceArguments.hs
+++ b/src/full/Agda/TypeChecking/InstanceArguments.hs
@@ -1,13 +1,9 @@
{-# LANGUAGE CPP #-}
-{-# LANGUAGE LambdaCase #-}
-
-#if __GLASGOW_HASKELL__ >= 710
-{-# LANGUAGE FlexibleContexts #-}
-#endif
+{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.InstanceArguments where
-import Control.Applicative
+import Control.Applicative hiding (empty)
import Control.Monad.Reader
import Control.Monad.State
import qualified Data.Map as Map
@@ -24,6 +20,7 @@ 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
@@ -38,6 +35,7 @@ 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
@@ -61,26 +59,58 @@ initialIFSCandidates t = do
getContextVars :: TCM [Candidate]
getContextVars = do
ctx <- getContext
- let vars = [ Candidate (var i) (raise (i + 1) t) ExplicitStayExplicit
+ let vars = [ Candidate (var i) (raise (i + 1) t) ExplicitStayExplicit (argInfoOverlappable info)
| (Dom info (x, t), i) <- zip ctx [0..]
, getHiding info == Instance
, not (unusableRelevance $ argInfoRelevance info)
]
+
+ -- {{}}-fields of variables are also candidates
+ let cxtAndTypes = [ (var i, snd $ unDom $ raise (i + 1) t) | (i, t) <- zip [0..] ctx ]
+ fields <- concat <$> mapM instanceFields (reverse cxtAndTypes)
+ reportSDoc "tc.instance.fields" 30 $ text "instance field candidates" $$ nest 2 (vcat
+ [ sep [ (if overlap then text "overlap" else empty) <+> prettyTCM v <+> text ":"
+ , nest 2 $ prettyTCM t ] | Candidate v t _ overlap <- fields ])
+
-- get let bindings
env <- asks envLetBindings
env <- mapM (getOpen . snd) $ Map.toList env
- let lets = [ Candidate v t ExplicitStayExplicit
+ let lets = [ Candidate v t ExplicitStayExplicit False
| (v, Dom info t) <- env
, getHiding info == Instance
, not (unusableRelevance $ argInfoRelevance info)
]
- return $ vars ++ lets
+ 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
+ -- Are we inside the record module? If so it's safe and desirable
+ -- to eta-expand once (issue #2320).
+ if qnameToList r `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 (argInfoOverlappable $ argInfo arg)
+ | getHiding arg == Instance ] ++) <$>
+ instanceFields' False (unArg arg, t)
getScopeDefs :: QName -> TCM [Candidate]
getScopeDefs n = do
instanceDefs <- getInstanceDefs
rel <- asks envRelevance
- let qs = fromMaybe [] $ Map.lookup n instanceDefs
+ let qs = maybe [] Set.toList $ Map.lookup n instanceDefs
catMaybes <$> mapM (candidate rel) qs
candidate :: Relevance -> QName -> TCM (Maybe Candidate)
@@ -97,15 +127,15 @@ initialIFSCandidates t = do
args <- freeVarsToApply q
let v = case theDef def of
-- drop parameters if it's a projection function...
- Function{ funProjection = Just p } -> projDropPars p `apply` args
+ Function{ funProjection = Just p } -> projDropParsApply p ProjSystem 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 []
+ Constructor{ conSrcCon = c } -> Con c ConOSystem []
_ -> Def q $ map Apply args
inScope <- isNameInScope q <$> getScope
- return $ Candidate v t ExplicitToInstance <$ guard inScope
+ return $ Candidate v t ExplicitToInstance False <$ guard inScope
where
-- unbound constant throws an internal error
handle (TypeError _ (Closure {clValue = InternalError _})) = return Nothing
@@ -151,15 +181,17 @@ findInScope' :: MetaId -> [Candidate] -> TCM (Maybe ([Candidate], Maybe MetaId))
findInScope' m cands = ifM (isFrozen m) (return (Just (cands, Nothing))) $ do
-- Andreas, 2013-12-28 issue 1003:
-- If instance meta is already solved, simply discard the constraint.
- ifM (isInstantiatedMeta m) (return Nothing) $ do
+ -- Ulf, 2016-12-06 issue 2325: But only if *fully* instantiated.
+ ifM (isFullyInstantiatedMeta m) (return 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" 15 $
"findInScope 2: constraint: " ++ prettyShow m ++ "; candidates left: " ++ show (length cands)
- reportSDoc "tc.instance" 70 $ nest 2 $ vcat
- [ sep [ prettyTCM v <+> text ":", nest 2 $ prettyTCM t ] | Candidate v t _ <- 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 ]
t <- normalise =<< getMetaTypeInContext m
insidePi t $ \ t -> do
reportSDoc "tc.instance" 15 $ text "findInScope 3: t =" <+> prettyTCM t
@@ -167,7 +199,9 @@ findInScope' m cands = ifM (isFrozen m) (return (Just (cands, Nothing))) $ do
-- If one of the arguments of the typeclass is a meta which is not rigidly
-- constrained, then don’t do anything because it may loop.
- ifJustM (areThereNonRigidMetaArguments (unEl t)) (\ m -> return (Just (cands, Just m))) $ do
+ ifJustM (areThereNonRigidMetaArguments (unEl t)) (\ m -> do
+ reportSLn "tc.instance" 15 "aborting due to non-rigidly constrained metas"
+ return (Just (cands, Just m))) $ do
mcands <- checkCandidates m t cands
debugConstraints
@@ -178,7 +212,7 @@ findInScope' m cands = ifM (isFrozen m) (return (Just (cands, Nothing))) $ do
text "findInScope 5: not a single candidate found..."
typeError $ IFSNoCandidateInScope t
- Just [Candidate term t' _] -> do
+ 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
@@ -203,7 +237,7 @@ findInScope' m cands = ifM (isFrozen m) (return (Just (cands, Nothing))) $ do
insidePi :: Type -> (Type -> TCM a) -> TCM a
insidePi t ret =
case ignoreSharing $ unEl t of
- Pi a b -> addContext (absName b, a) $ insidePi (unAbs b) ret
+ Pi a b -> addContext' (absName b, a) $ insidePi (unAbs b) ret
Def{} -> ret t
Var{} -> ret t
Sort{} -> __IMPOSSIBLE__
@@ -270,7 +304,9 @@ areThereNonRigidMetaArguments t = case ignoreSharing t of
Def n args -> do
TelV tel _ <- telView . defType =<< getConstInfo n
let varOccs EmptyTel = []
- varOccs (ExtendTel _ btel) = occurrence 0 tel : varOccs tel
+ varOccs (ExtendTel a btel)
+ | getRelevance a == Irrelevant = WeaklyRigid : varOccs tel -- #2171: ignore irrelevant arguments
+ | otherwise = occurrence 0 tel : varOccs tel
where tel = unAbs btel
rigid StronglyRigid = True
rigid Unguarded = True
@@ -293,7 +329,7 @@ areThereNonRigidMetaArguments t = case ignoreSharing t of
where
areThereNonRigidMetaArgs :: Elims -> TCM (Maybe MetaId)
areThereNonRigidMetaArgs [] = return Nothing
- areThereNonRigidMetaArgs (Proj _ : xs) = areThereNonRigidMetaArgs xs
+ areThereNonRigidMetaArgs (Proj{} : xs) = areThereNonRigidMetaArgs xs
areThereNonRigidMetaArgs (Apply x : xs) = do
ifJustM (isNonRigidMeta $ unArg x) (return . Just) (areThereNonRigidMetaArgs xs)
@@ -302,7 +338,7 @@ areThereNonRigidMetaArguments t = case ignoreSharing t of
case ignoreSharing v of
Def _ es -> areThereNonRigidMetaArgs es
Var _ es -> areThereNonRigidMetaArgs es
- Con _ vs -> areThereNonRigidMetaArgs (map Apply vs)
+ Con _ _ vs-> areThereNonRigidMetaArgs (map Apply vs)
MetaV i _ -> ifM (isRigid i) (return Nothing) $ do
-- Ignore unconstrained level and size metas (#1865)
Def lvl [] <- ignoreSharing <$> primLevel
@@ -333,7 +369,13 @@ filterResetingState m cands f = disableDestructiveUpdate $ do
a <- instantiateFull =<< (`piApplyM` ctxArgs) =<< getMetaType m
return (ok, v, a)
result <- mapM (\c -> do bs <- localTCStateSaving (tryC c); return (c, bs)) cands
- let result' = [ (c, v, a, s) | (c, ((r, v, a), s)) <- result, r /= No ]
+
+ -- Check that there aren't any hard failures
+ 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 ]
-- It's not safe to compare maybes for equality because they might
-- not have instantiated at all.
@@ -345,9 +387,16 @@ filterResetingState m cands f = disableDestructiveUpdate $ do
-- 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 m cands = do
+dropSameCandidates m cands0 = do
metas <- Set.fromList . Map.keys <$> getMetaStore
let freshMetas x = not $ Set.null $ Set.difference (Set.fromList $ allMetas x) metas
+
+ -- Take overlappable candidates into account
+ let cands =
+ case partition (\ (c, _, _, _) -> candidateOverlappable c) cands0 of
+ (cand : _, []) -> [cand] -- only overlappable candidates: pick the first one
+ _ -> cands0 -- otherwise require equality
+
reportSDoc "tc.instance" 50 $ vcat
[ text "valid candidates:"
, nest 2 $ vcat [ if freshMetas (v, a) then text "(redacted)" else
@@ -372,8 +421,12 @@ dropSameCandidates m cands = do
{- else -} (\ _ -> return False)
`catchError` (\ _ -> return False)
-data YesNoMaybe = Yes | No | Maybe
- deriving (Show, Eq)
+data YesNoMaybe = Yes | No | Maybe | HellNo TCErr
+ deriving (Show)
+
+isNo :: YesNoMaybe -> Bool
+isNo No = 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.
@@ -385,23 +438,32 @@ checkCandidates m t cands = disableDestructiveUpdate $
reportSDoc "tc.instance.candidates" 20 $ nest 2 $ text "target:" <+> prettyTCM t
reportSDoc "tc.instance.candidates" 20 $ nest 2 $ vcat
[ text "candidates"
- , vcat [ text "-" <+> prettyTCM v <+> text ":" <+> prettyTCM t | Candidate v t _ <- cands ] ]
+ , 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 "-" <+> prettyTCM v <+> text ":" <+> prettyTCM t | Candidate v t _ <- cands' ] ]
+ , 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
+ anyMetaTypes (Candidate _ a _ _ : cands) = do
a <- instantiate a
case ignoreSharing $ 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) = do
+ checkCandidateForMeta m t (Candidate term t' eti _) = 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
@@ -458,11 +520,20 @@ checkCandidates m t cands = disableDestructiveUpdate $
(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 = do
- reportSDoc "tc.instance" 50 $
- text "assignment failed:" <+> prettyTCM err
- return No
+ 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
@@ -479,10 +550,10 @@ applyDroppingParameters :: Term -> Args -> TCM Term
applyDroppingParameters t vs = do
let fallback = return $ t `apply` vs
case ignoreSharing t of
- Con c [] -> do
+ Con c ci [] -> do
def <- theDef <$> getConInfo c
case def of
- Constructor {conPars = n} -> return $ Con c (genericDrop n vs)
+ Constructor {conPars = n} -> return $ Con c ci (genericDrop n vs)
_ -> __IMPOSSIBLE__
Def f [] -> do
mp <- isProjection f
@@ -490,6 +561,6 @@ applyDroppingParameters t vs = do
Just Projection{projIndex = n} -> do
case drop n vs of
[] -> return t
- u : us -> (`apply` us) <$> applyDef f u
+ u : us -> (`apply` us) <$> applyDef ProjPrefix f u
_ -> fallback
_ -> fallback