1{-# LANGUAGE NondecreasingIndentation #-} 2{-# LANGUAGE GADTs #-} 3 4module Agda.TypeChecking.MetaVars where 5 6import Prelude hiding (null) 7 8import Control.Monad.Except 9import Control.Monad.Reader 10 11import Data.Function 12import qualified Data.IntMap as IntMap 13import qualified Data.IntSet as IntSet 14import qualified Data.List as List 15import qualified Data.Set as Set 16import qualified Data.Foldable as Fold 17import qualified Data.Traversable as Trav 18 19import Agda.Interaction.Options 20 21import Agda.Syntax.Abstract.Name as A 22import Agda.Syntax.Common 23import Agda.Syntax.Internal 24import Agda.Syntax.Internal.Generic 25import Agda.Syntax.Internal.MetaVars 26import Agda.Syntax.Position (getRange, killRange) 27 28import Agda.TypeChecking.Monad 29-- import Agda.TypeChecking.Monad.Builtin 30-- import Agda.TypeChecking.Monad.Context 31import Agda.TypeChecking.Reduce 32import Agda.TypeChecking.Sort 33import Agda.TypeChecking.Substitute 34import qualified Agda.TypeChecking.SyntacticEquality as SynEq 35import Agda.TypeChecking.Telescope 36import Agda.TypeChecking.Constraints 37import Agda.TypeChecking.Free 38import Agda.TypeChecking.Lock 39import Agda.TypeChecking.Level (levelType) 40import Agda.TypeChecking.Records 41import Agda.TypeChecking.Pretty 42import Agda.TypeChecking.Irrelevance 43import Agda.TypeChecking.EtaContract 44import Agda.TypeChecking.SizedTypes (boundedSizeMetaHook, isSizeProblem) 45import {-# SOURCE #-} Agda.TypeChecking.CheckInternal 46import {-# SOURCE #-} Agda.TypeChecking.Conversion 47 48-- import Agda.TypeChecking.CheckInternal 49-- import {-# SOURCE #-} Agda.TypeChecking.CheckInternal (checkInternal) 50import Agda.TypeChecking.MetaVars.Occurs 51 52import Agda.Utils.Function 53import Agda.Utils.Lens 54import Agda.Utils.List 55import Agda.Utils.Maybe 56import Agda.Utils.Monad 57import Agda.Utils.Size 58import Agda.Utils.Tuple 59import Agda.Utils.Permutation 60import Agda.Utils.Pretty ( prettyShow ) 61import Agda.Utils.Singleton 62import qualified Agda.Utils.Graph.TopSort as Graph 63import Agda.Utils.VarSet (VarSet) 64import qualified Agda.Utils.VarSet as VarSet 65import Agda.Utils.WithDefault 66 67import Agda.Utils.Impossible 68 69instance MonadMetaSolver TCM where 70 newMeta' = newMetaTCM' 71 assignV dir x args v t = assignWrapper dir x (map Apply args) v $ assign dir x args v t 72 assignTerm' = assignTermTCM' 73 etaExpandMeta = etaExpandMetaTCM 74 updateMetaVar = updateMetaVarTCM 75 76 -- Right now we roll back the full state when aborting. 77 -- TODO: only roll back the metavariables 78 speculateMetas fallback m = do 79 (a, s) <- localTCStateSaving m 80 case a of 81 KeepMetas -> putTC s 82 RollBackMetas -> fallback 83 84-- | Find position of a value in a list. 85-- Used to change metavar argument indices during assignment. 86-- 87-- @reverse@ is necessary because we are directly abstracting over the list. 88-- 89findIdx :: Eq a => [a] -> a -> Maybe Int 90findIdx vs v = List.elemIndex v (reverse vs) 91 92hasTwinMeta :: MetaId -> TCM Bool 93hasTwinMeta x = do 94 m <- lookupMeta x 95 return $ isJust $ mvTwin m 96 97-- | Check whether a meta variable is a place holder for a blocked term. 98isBlockedTerm :: MetaId -> TCM Bool 99isBlockedTerm x = do 100 reportSLn "tc.meta.blocked" 12 $ "is " ++ prettyShow x ++ " a blocked term? " 101 i <- mvInstantiation <$> lookupMeta x 102 let r = case i of 103 BlockedConst{} -> True 104 PostponedTypeCheckingProblem{} -> True 105 InstV{} -> False 106 Open{} -> False 107 OpenInstance{} -> False 108 reportSLn "tc.meta.blocked" 12 $ 109 if r then " yes, because " ++ show i else " no" 110 return r 111 112isEtaExpandable :: [MetaKind] -> MetaId -> TCM Bool 113isEtaExpandable kinds x = do 114 i <- mvInstantiation <$> lookupMeta x 115 return $ case i of 116 Open{} -> True 117 OpenInstance{} -> Records `notElem` kinds 118 InstV{} -> False 119 BlockedConst{} -> False 120 PostponedTypeCheckingProblem{} -> False 121 122-- * Performing the assignment 123 124-- | Performing the meta variable assignment. 125-- 126-- The instantiation should not be an 'InstV' and the 'MetaId' 127-- should point to something 'Open' or a 'BlockedConst'. 128-- Further, the meta variable may not be 'Frozen'. 129assignTerm :: MonadMetaSolver m => MetaId -> [Arg ArgName] -> Term -> m () 130assignTerm x tel v = do 131 -- verify (new) invariants 132 whenM (isFrozen x) __IMPOSSIBLE__ 133 assignTerm' x tel v 134 135-- | Skip frozen check. Used for eta expanding frozen metas. 136assignTermTCM' :: MetaId -> [Arg ArgName] -> Term -> TCM () 137assignTermTCM' x tel v = do 138 reportSDoc "tc.meta.assign" 70 $ vcat 139 [ "assignTerm" <+> prettyTCM x <+> " := " <+> prettyTCM v 140 , nest 2 $ "tel =" <+> prettyList_ (map (text . unArg) tel) 141 ] 142 -- verify (new) invariants 143 whenM (not <$> asksTC envAssignMetas) __IMPOSSIBLE__ 144 145 verboseS "profile.metas" 10 $ liftTCM $ return () {-tickMax "max-open-metas" . (fromIntegral . size) =<< getOpenMetas-} 146 modifyMetaStore $ ins x $ InstV tel $ killRange v 147 etaExpandListeners x 148 wakeupConstraints x 149 reportSLn "tc.meta.assign" 20 $ "completed assignment of " ++ prettyShow x 150 where 151 ins x i = IntMap.adjust (\ mv -> mv { mvInstantiation = i }) $ metaId x 152 153-- * Creating meta variables. 154 155-- | Create a sort meta that cannot be instantiated with 'Inf' (Setω). 156newSortMetaBelowInf :: TCM Sort 157newSortMetaBelowInf = do 158 x <- newSortMeta 159 hasBiggerSort x 160 return x 161 162-- | Create a sort meta that may be instantiated with 'Inf' (Setω). 163newSortMeta :: MonadMetaSolver m => m Sort 164newSortMeta = 165 ifM hasUniversePolymorphism (newSortMetaCtx =<< getContextArgs) 166 -- else (no universe polymorphism) 167 $ do i <- createMetaInfo 168 let j = IsSort () __DUMMY_TYPE__ 169 x <- newMeta Instantiable i normalMetaPriority (idP 0) j 170 reportSDoc "tc.meta.new" 50 $ 171 "new sort meta" <+> prettyTCM x 172 return $ MetaS x [] 173 174-- | Create a sort meta that may be instantiated with 'Inf' (Setω). 175newSortMetaCtx :: MonadMetaSolver m => Args -> m Sort 176newSortMetaCtx vs = do 177 i <- createMetaInfo 178 tel <- getContextTelescope 179 let t = telePi_ tel __DUMMY_TYPE__ 180 x <- newMeta Instantiable i normalMetaPriority (idP $ size tel) $ IsSort () t 181 reportSDoc "tc.meta.new" 50 $ 182 "new sort meta" <+> prettyTCM x <+> ":" <+> prettyTCM t 183 return $ MetaS x $ map Apply vs 184 185newTypeMeta' :: Comparison -> Sort -> TCM Type 186newTypeMeta' cmp s = El s . snd <$> newValueMeta RunMetaOccursCheck cmp (sort s) 187 188newTypeMeta :: Sort -> TCM Type 189newTypeMeta = newTypeMeta' CmpLeq 190 191newTypeMeta_ :: TCM Type 192newTypeMeta_ = newTypeMeta' CmpEq =<< (workOnTypes $ newSortMeta) 193-- TODO: (this could be made work with new uni-poly) 194-- Andreas, 2011-04-27: If a type meta gets solved, than we do not have to check 195-- that it has a sort. The sort comes from the solution. 196-- newTypeMeta_ = newTypeMeta Inf 197 198newLevelMeta :: MonadMetaSolver m => m Level 199newLevelMeta = do 200 (x, v) <- newValueMeta RunMetaOccursCheck CmpEq =<< levelType 201 return $ case v of 202 Level l -> l 203 _ -> atomicLevel v 204 205-- | @newInstanceMeta s t cands@ creates a new instance metavariable 206-- of type the output type of @t@ with name suggestion @s@. 207newInstanceMeta 208 :: MonadMetaSolver m 209 => MetaNameSuggestion -> Type -> m (MetaId, Term) 210newInstanceMeta s t = do 211 vs <- getContextArgs 212 ctx <- getContextTelescope 213 newInstanceMetaCtx s (telePi_ ctx t) vs 214 215newInstanceMetaCtx 216 :: MonadMetaSolver m 217 => MetaNameSuggestion -> Type -> Args -> m (MetaId, Term) 218newInstanceMetaCtx s t vs = do 219 reportSDoc "tc.meta.new" 50 $ fsep 220 [ "new instance meta:" 221 , nest 2 $ prettyTCM vs <+> "|-" 222 ] 223 -- Andreas, 2017-10-04, issue #2753: no metaOccurs check for instance metas 224 i0 <- createMetaInfo' DontRunMetaOccursCheck 225 let i = i0 { miNameSuggestion = s } 226 TelV tel _ <- telView t 227 let perm = idP (size tel) 228 x <- newMeta' OpenInstance Instantiable i normalMetaPriority perm (HasType () CmpLeq t) 229 reportSDoc "tc.meta.new" 50 $ fsep 230 [ nest 2 $ pretty x <+> ":" <+> prettyTCM t 231 ] 232 let c = FindInstance x Nothing 233 -- If we're not already solving instance constraints we should add this 234 -- to the awake constraints to make sure we don't forget about it. If we 235 -- are solving constraints it will get woken up later (see #2690) 236 ifM isSolvingConstraints (addConstraint alwaysUnblock c) (addAwakeConstraint alwaysUnblock c) 237 etaExpandMetaSafe x 238 return (x, MetaV x $ map Apply vs) 239 240-- | Create a new value meta with specific dependencies, possibly η-expanding in the process. 241newNamedValueMeta :: MonadMetaSolver m => RunMetaOccursCheck -> MetaNameSuggestion -> Comparison -> Type -> m (MetaId, Term) 242newNamedValueMeta b s cmp t = do 243 (x, v) <- newValueMeta b cmp t 244 setMetaNameSuggestion x s 245 return (x, v) 246 247-- | Create a new value meta with specific dependencies without η-expanding. 248newNamedValueMeta' :: MonadMetaSolver m => RunMetaOccursCheck -> MetaNameSuggestion -> Comparison -> Type -> m (MetaId, Term) 249newNamedValueMeta' b s cmp t = do 250 (x, v) <- newValueMeta' b cmp t 251 setMetaNameSuggestion x s 252 return (x, v) 253 254-- | Create a new metavariable, possibly η-expanding in the process. 255newValueMeta :: MonadMetaSolver m => RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term) 256newValueMeta b cmp t = do 257 vs <- getContextArgs 258 tel <- getContextTelescope 259 newValueMetaCtx Instantiable b cmp t tel (idP $ size tel) vs 260 261newValueMetaCtx 262 :: MonadMetaSolver m 263 => Frozen -> RunMetaOccursCheck -> Comparison -> Type -> Telescope -> Permutation -> Args -> m (MetaId, Term) 264newValueMetaCtx frozen b cmp t tel perm ctx = 265 mapSndM instantiateFull =<< newValueMetaCtx' frozen b cmp t tel perm ctx 266 267-- | Create a new value meta without η-expanding. 268newValueMeta' 269 :: MonadMetaSolver m 270 => RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term) 271newValueMeta' b cmp t = do 272 vs <- getContextArgs 273 tel <- getContextTelescope 274 newValueMetaCtx' Instantiable b cmp t tel (idP $ size tel) vs 275 276newValueMetaCtx' 277 :: MonadMetaSolver m 278 => Frozen -> RunMetaOccursCheck -> Comparison -> Type -> Telescope -> Permutation -> Args -> m (MetaId, Term) 279newValueMetaCtx' frozen b cmp a tel perm vs = do 280 i <- createMetaInfo' b 281 let t = telePi_ tel a 282 x <- newMeta frozen i normalMetaPriority perm (HasType () cmp t) 283 modality <- viewTC eModality 284 reportSDoc "tc.meta.new" 50 $ fsep 285 [ text $ "new meta (" ++ show (i ^. lensIsAbstract) ++ "):" 286 , nest 2 $ prettyTCM vs <+> "|-" 287 , nest 2 $ pretty x <+> ":" <+> pretty modality <+> prettyTCM t 288 ] 289 etaExpandMetaSafe x 290 -- Andreas, 2012-09-24: for Metas X : Size< u add constraint X+1 <= u 291 let u = MetaV x $ map Apply vs 292 boundedSizeMetaHook u tel a 293 return (x, u) 294 295newTelMeta :: MonadMetaSolver m => Telescope -> m Args 296newTelMeta tel = newArgsMeta (abstract tel $ __DUMMY_TYPE__) 297 298type Condition = Dom Type -> Abs Type -> Bool 299 300trueCondition :: Condition 301trueCondition _ _ = True 302 303newArgsMeta :: MonadMetaSolver m => Type -> m Args 304newArgsMeta = newArgsMeta' trueCondition 305 306newArgsMeta' :: MonadMetaSolver m => Condition -> Type -> m Args 307newArgsMeta' condition t = do 308 args <- getContextArgs 309 tel <- getContextTelescope 310 newArgsMetaCtx' Instantiable condition t tel (idP $ size tel) args 311 312newArgsMetaCtx :: Type -> Telescope -> Permutation -> Args -> TCM Args 313newArgsMetaCtx = newArgsMetaCtx' Instantiable trueCondition 314 315newArgsMetaCtx' 316 :: MonadMetaSolver m 317 => Frozen -> Condition -> Type -> Telescope -> Permutation -> Args -> m Args 318newArgsMetaCtx' frozen condition (El s tm) tel perm ctx = do 319 tm <- reduce tm 320 case tm of 321 Pi dom@(Dom{domInfo = info, unDom = a}) codom | condition dom codom -> do 322 let mod = getModality info 323 -- Issue #3031: It's not enough to applyModalityToContext, since most (all?) 324 -- of the context lives in tel. Don't forget the arguments in ctx. 325 tel' = telFromList $ 326 map (mod `inverseApplyModalityButNotQuantity`) $ 327 telToList tel 328 ctx' = map (mod `inverseApplyModalityButNotQuantity`) ctx 329 (m, u) <- applyModalityToContext info $ 330 newValueMetaCtx frozen RunMetaOccursCheck CmpLeq a tel' perm ctx' 331 -- Jesper, 2021-05-05: When creating a metavariable from a 332 -- generalizable variable, we must set the modality at which it 333 -- will be generalized. Don't do this for other metavariables, 334 -- as they should keep the defaul modality (see #5363). 335 whenM ((== YesGeneralizeVar) <$> viewTC eGeneralizeMetas) $ 336 setMetaGeneralizableArgInfo m $ hideOrKeepInstance info 337 setMetaNameSuggestion m (absName codom) 338 args <- newArgsMetaCtx' frozen condition (codom `absApp` u) tel perm ctx 339 return $ Arg info u : args 340 _ -> return [] 341 342-- | Create a metavariable of record type. This is actually one metavariable 343-- for each field. 344newRecordMeta :: QName -> Args -> TCM Term 345newRecordMeta r pars = do 346 args <- getContextArgs 347 tel <- getContextTelescope 348 newRecordMetaCtx Instantiable r pars tel (idP $ size tel) args 349 350newRecordMetaCtx 351 :: Frozen -- ^ Should the meta be created frozen? 352 -> QName -- ^ Name of record type 353 -> Args -- ^ Parameters of record type. 354 -> Telescope -> Permutation -> Args -> TCM Term 355newRecordMetaCtx frozen r pars tel perm ctx = do 356 ftel <- flip apply pars <$> getRecordFieldTypes r 357 fields <- newArgsMetaCtx' frozen trueCondition 358 (telePi_ ftel __DUMMY_TYPE__) tel perm ctx 359 con <- getRecordConstructor r 360 return $ Con con ConOSystem (map Apply fields) 361 362newQuestionMark :: InteractionId -> Comparison -> Type -> TCM (MetaId, Term) 363newQuestionMark ii cmp = newQuestionMark' (newValueMeta' RunMetaOccursCheck) ii cmp 364 365newQuestionMark' 366 :: (Comparison -> Type -> TCM (MetaId, Term)) 367 -> InteractionId -> Comparison -> Type -> TCM (MetaId, Term) 368newQuestionMark' new ii cmp t = do 369 -- Andreas, 2016-07-29, issue 1720-2 370 -- This is slightly risky, as the same interaction id 371 -- maybe be shared between different contexts. 372 -- Blame goes to the record processing hack, see issue #424 373 -- and @ConcreteToAbstract.recordConstructorType@. 374 let existing x = (x,) . MetaV x . map Apply <$> getContextArgs 375 flip (caseMaybeM $ lookupInteractionMeta ii) existing $ {-else-} do 376 377 -- Do not run check for recursive occurrence of meta in definitions, 378 -- because we want to give the recursive solution interactively (Issue 589) 379 (x, m) <- new cmp t 380 connectInteractionPoint ii x 381 return (x, m) 382 383-- | Construct a blocked constant if there are constraints. 384blockTerm 385 :: (MonadMetaSolver m, MonadConstraint m, MonadFresh Nat m, MonadFresh ProblemId m) 386 => Type -> m Term -> m Term 387blockTerm t blocker = do 388 (pid, v) <- newProblem blocker 389 blockTermOnProblem t v pid 390 391blockTermOnProblem 392 :: (MonadMetaSolver m, MonadFresh Nat m) 393 => Type -> Term -> ProblemId -> m Term 394blockTermOnProblem t v pid = do 395 -- Andreas, 2012-09-27 do not block on unsolved size constraints 396 solved <- isProblemSolved pid 397 ifM (return solved `or2M` isSizeProblem pid) 398 (v <$ reportSLn "tc.meta.blocked" 20 ("Not blocking because " ++ show pid ++ " is " ++ 399 if solved then "solved" else "a size problem")) $ do 400 i <- createMetaInfo 401 es <- map Apply <$> getContextArgs 402 tel <- getContextTelescope 403 x <- newMeta' (BlockedConst $ abstract tel v) 404 Instantiable 405 i 406 lowMetaPriority 407 (idP $ size tel) 408 (HasType () CmpLeq $ telePi_ tel t) 409 -- we don't instantiate blocked terms 410 inTopContext $ addConstraint (unblockOnProblem pid) (UnBlock x) 411 reportSDoc "tc.meta.blocked" 20 $ vcat 412 [ "blocked" <+> prettyTCM x <+> ":=" <+> inTopContext 413 (prettyTCM $ abstract tel v) 414 , " by" <+> (prettyTCM =<< getConstraintsForProblem pid) 415 ] 416 inst <- isInstantiatedMeta x 417 if inst 418 then instantiate (MetaV x es) 419 else do 420 -- We don't return the blocked term instead create a fresh metavariable 421 -- that we compare against the blocked term once it's unblocked. This way 422 -- blocked terms can be instantiated before they are unblocked, thus making 423 -- constraint solving a bit more robust against instantiation order. 424 -- Andreas, 2015-05-22: DontRunMetaOccursCheck to avoid Issue585-17. 425 (m', v) <- newValueMeta DontRunMetaOccursCheck CmpLeq t 426 reportSDoc "tc.meta.blocked" 30 427 $ "setting twin of" 428 <+> prettyTCM m' 429 <+> "to be" 430 <+> prettyTCM x 431 updateMetaVar m' (\mv -> mv { mvTwin = Just x }) 432 i <- fresh 433 -- This constraint is woken up when unblocking, so it doesn't need a problem id. 434 cmp <- buildProblemConstraint_ (unblockOnMeta x) (ValueCmp CmpEq (AsTermsOf t) v (MetaV x es)) 435 reportSDoc "tc.constr.add" 20 $ "adding constraint" <+> prettyTCM cmp 436 listenToMeta (CheckConstraint i cmp) x 437 return v 438 439blockTypeOnProblem 440 :: (MonadMetaSolver m, MonadFresh Nat m) 441 => Type -> ProblemId -> m Type 442blockTypeOnProblem (El s a) pid = El s <$> blockTermOnProblem (sort s) a pid 443 444-- | @unblockedTester t@ returns a 'Blocker' for @t@. 445-- 446-- Auxiliary function used when creating a postponed type checking problem. 447unblockedTester :: Type -> TCM Blocker 448unblockedTester t = ifBlocked t (\ b _ -> return b) (\ _ _ -> return alwaysUnblock) 449 450-- | Create a postponed type checking problem @e : t@ that waits for type @t@ 451-- to unblock (become instantiated or its constraints resolved). 452postponeTypeCheckingProblem_ :: TypeCheckingProblem -> TCM Term 453postponeTypeCheckingProblem_ p = do 454 postponeTypeCheckingProblem p =<< unblock p 455 where 456 unblock (CheckExpr _ _ t) = unblockedTester t 457 unblock (CheckArgs _ _ _ _ t _ _) = unblockedTester t -- The type of the head of the application. 458 unblock (CheckProjAppToKnownPrincipalArg _ _ _ _ _ _ _ _ t _) = unblockedTester t -- The type of the principal argument 459 unblock (CheckLambda _ _ _ t) = unblockedTester t 460 unblock (DoQuoteTerm _ _ _) = __IMPOSSIBLE__ -- also quoteTerm problems 461 462-- | Create a postponed type checking problem @e : t@ that waits for conditon 463-- @unblock@. A new meta is created in the current context that has as 464-- instantiation the postponed type checking problem. An 'UnBlock' constraint 465-- is added for this meta, which links to this meta. 466postponeTypeCheckingProblem :: TypeCheckingProblem -> Blocker -> TCM Term 467postponeTypeCheckingProblem p unblock | unblock == alwaysUnblock = do 468 reportSDoc "impossible" 2 $ "Postponed without blocker:" <?> prettyTCM p 469 __IMPOSSIBLE__ 470postponeTypeCheckingProblem p unblock = do 471 i <- createMetaInfo' DontRunMetaOccursCheck 472 tel <- getContextTelescope 473 cl <- buildClosure p 474 let t = problemType p 475 m <- newMeta' (PostponedTypeCheckingProblem cl) 476 Instantiable i normalMetaPriority (idP (size tel)) 477 $ HasType () CmpLeq $ telePi_ tel t 478 inTopContext $ reportSDoc "tc.meta.postponed" 20 $ vcat 479 [ "new meta" <+> prettyTCM m <+> ":" <+> prettyTCM (telePi_ tel t) 480 , "for postponed typechecking problem" <+> prettyTCM p 481 ] 482 483 -- Create the meta that we actually return 484 -- Andreas, 2012-03-15 485 -- This is an alias to the pptc meta, in order to allow pruning (issue 468) 486 -- and instantiation. 487 -- Since this meta's solution comes from user code, we do not need 488 -- to run the extended occurs check (metaOccurs) to exclude 489 -- non-terminating solutions. 490 es <- map Apply <$> getContextArgs 491 (_, v) <- newValueMeta DontRunMetaOccursCheck CmpLeq t 492 cmp <- buildProblemConstraint_ (unblockOnMeta m) (ValueCmp CmpEq (AsTermsOf t) v (MetaV m es)) 493 reportSDoc "tc.constr.add" 20 $ "adding constraint" <+> prettyTCM cmp 494 i <- liftTCM fresh 495 listenToMeta (CheckConstraint i cmp) m 496 addConstraint unblock (UnBlock m) 497 return v 498 499-- | Type of the term that is produced by solving the 'TypeCheckingProblem'. 500problemType :: TypeCheckingProblem -> Type 501problemType (CheckExpr _ _ t ) = t 502problemType (CheckArgs _ _ _ _ _ t _ ) = t -- The target type of the application. 503problemType (CheckProjAppToKnownPrincipalArg _ _ _ _ _ t _ _ _ _) = t -- The target type of the application 504problemType (CheckLambda _ _ _ t ) = t 505problemType (DoQuoteTerm _ _ t) = t 506 507-- | Eta expand metavariables listening on the current meta. 508etaExpandListeners :: MetaId -> TCM () 509etaExpandListeners m = do 510 ls <- getMetaListeners m 511 clearMetaListeners m -- we don't really have to do this 512 mapM_ wakeupListener ls 513 514-- | Wake up a meta listener and let it do its thing 515wakeupListener :: Listener -> TCM () 516 -- Andreas 2010-10-15: do not expand record mvars, lazyness needed for irrelevance 517wakeupListener (EtaExpand x) = etaExpandMetaSafe x 518wakeupListener (CheckConstraint _ c) = do 519 reportSDoc "tc.meta.blocked" 20 $ "waking boxed constraint" <+> prettyTCM c 520 modifyAwakeConstraints (c:) 521 solveAwakeConstraints 522 523-- | Do safe eta-expansions for meta (@SingletonRecords,Levels@). 524etaExpandMetaSafe :: (MonadMetaSolver m) => MetaId -> m () 525etaExpandMetaSafe = etaExpandMeta [SingletonRecords,Levels] 526 527-- | Eta expand a metavariable, if it is of the specified kind. 528-- Don't do anything if the metavariable is a blocked term. 529etaExpandMetaTCM :: [MetaKind] -> MetaId -> TCM () 530etaExpandMetaTCM kinds m = whenM ((not <$> isFrozen m) `and2M` asksTC envAssignMetas `and2M` isEtaExpandable kinds m) $ do 531 verboseBracket "tc.meta.eta" 20 ("etaExpandMeta " ++ prettyShow m) $ do 532 let waitFor b = do 533 reportSDoc "tc.meta.eta" 20 $ do 534 "postponing eta-expansion of meta variable" <+> 535 prettyTCM m <+> 536 "which is blocked by" <+> prettyTCM b 537 mapM_ (listenToMeta (EtaExpand m)) $ Set.toList $ allBlockingMetas b 538 dontExpand = do 539 reportSDoc "tc.meta.eta" 20 $ do 540 "we do not expand meta variable" <+> prettyTCM m <+> 541 text ("(requested was expansion of " ++ show kinds ++ ")") 542 meta <- lookupMeta m 543 case mvJudgement meta of 544 IsSort{} -> dontExpand 545 HasType _ cmp a -> do 546 547 reportSDoc "tc.meta.eta" 40 $ sep 548 [ text "considering eta-expansion at type " 549 , prettyTCM a 550 , text " raw: " 551 , pretty a 552 ] 553 554 TelV tel b <- telView a 555 reportSDoc "tc.meta.eta" 40 $ sep 556 [ text "considering eta-expansion at type" 557 , addContext tel (prettyTCM b) 558 , text "under telescope" 559 , prettyTCM tel 560 ] 561 562 -- Eta expanding metas with a domFinite will just make sure 563 -- they go unsolved: conversion will compare them at the 564 -- different cases for the domain, so it will not find the 565 -- solution for the whole meta. 566 if any domFinite (flattenTel tel) then dontExpand else do 567 568 -- Issue #3774: continue with the right context for b 569 addContext tel $ do 570 571 -- if the target type @b@ of @m@ is a meta variable @x@ itself 572 -- (@NonBlocked (MetaV{})@), 573 -- or it is blocked by a meta-variable @x@ (@Blocked@), we cannot 574 -- eta expand now, we have to postpone this. Once @x@ is 575 -- instantiated, we can continue eta-expanding m. This is realized 576 -- by adding @m@ to the listeners of @x@. 577 ifBlocked (unEl b) (\ x _ -> waitFor x) $ \ _ t -> case t of 578 lvl@(Def r es) -> 579 ifM (isEtaRecord r) {- then -} (do 580 let ps = fromMaybe __IMPOSSIBLE__ $ allApplyElims es 581 let expand = do 582 u <- withMetaInfo' meta $ 583 newRecordMetaCtx (mvFrozen meta) r ps tel (idP $ size tel) $ teleArgs tel 584 -- Andreas, 2019-03-18, AIM XXIX, issue #3597 585 -- When meta is frozen instantiate it with in-turn frozen metas. 586 inTopContext $ do 587 reportSDoc "tc.meta.eta" 15 $ sep 588 [ "eta expanding: " <+> pretty m <+> " --> " 589 , nest 2 $ prettyTCM u 590 ] 591 -- Andreas, 2012-03-29: No need for occurrence check etc. 592 -- we directly assign the solution for the meta 593 -- 2012-05-23: We also bypass the check for frozen. 594 noConstraints $ assignTerm' m (telToArgs tel) u -- should never produce any constraints 595 if Records `elem` kinds then 596 expand 597 else if (SingletonRecords `elem` kinds) then 598 catchPatternErr (\x -> waitFor x) $ do 599 ifM (isSingletonRecord r ps) expand dontExpand 600 else dontExpand 601 ) $ {- else -} ifM (andM [ return $ Levels `elem` kinds 602 , typeInType 603 , (Just lvl ==) <$> getBuiltin' builtinLevel 604 ]) (do 605 reportSLn "tc.meta.eta" 20 $ "Expanding level meta to 0 (type-in-type)" 606 -- Andreas, 2012-03-30: No need for occurrence check etc. 607 -- we directly assign the solution for the meta 608 noConstraints $ assignTerm m (telToArgs tel) $ Level $ ClosedLevel 0 609 ) $ {- else -} dontExpand 610 _ -> dontExpand 611 612-- | Eta expand blocking metavariables of record type, and reduce the 613-- blocked thing. 614 615etaExpandBlocked :: (MonadReduce m, MonadMetaSolver m, IsMeta t, Reduce t) 616 => Blocked t -> m (Blocked t) 617etaExpandBlocked t@NotBlocked{} = return t 618etaExpandBlocked t@(Blocked _ v) | Just{} <- isMeta v = return t 619etaExpandBlocked (Blocked b t) = do 620 reportSDoc "tc.meta.eta" 30 $ "Eta expanding blockers" <+> pretty b 621 mapM_ (etaExpandMeta [Records]) $ Set.toList $ allBlockingMetas b 622 t <- reduceB t 623 case t of 624 Blocked b' _ | b /= b' -> etaExpandBlocked t 625 _ -> return t 626 627assignWrapper :: (MonadMetaSolver m, MonadConstraint m, MonadError TCErr m, MonadDebug m, HasOptions m) 628 => CompareDirection -> MetaId -> Elims -> Term -> m () -> m () 629assignWrapper dir x es v doAssign = do 630 ifNotM (asksTC envAssignMetas) dontAssign $ {- else -} do 631 reportSDoc "tc.meta.assign" 10 $ do 632 "term" <+> prettyTCM (MetaV x es) <+> text (":" ++ show dir) <+> prettyTCM v 633 nowSolvingConstraints doAssign `finally` solveAwakeConstraints 634 635 where dontAssign = do 636 reportSLn "tc.meta.assign" 10 "don't assign metas" 637 patternViolation alwaysUnblock -- retry again when we are allowed to instantiate metas 638 639-- | Miller pattern unification: 640-- 641-- @assign dir x vs v a@ solves problem @x vs <=(dir) v : a@ for meta @x@ 642-- if @vs@ are distinct variables (linearity check) 643-- and @v@ depends only on these variables 644-- and does not contain @x@ itself (occurs check). 645-- 646-- This is the basic story, but we have added some features: 647-- 648-- 1. Pruning. 649-- 2. Benign cases of non-linearity. 650-- 3. @vs@ may contain record patterns. 651-- 652-- For a reference to some of these extensions, read 653-- Andreas Abel and Brigitte Pientka's TLCA 2011 paper. 654 655assign :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> TCM () 656assign dir x args v target = addOrUnblocker (unblockOnMeta x) $ do 657 658 mvar <- lookupMeta x -- information associated with meta x 659 let t = jMetaType $ mvJudgement mvar 660 661 -- Andreas, 2011-05-20 TODO! 662 -- full normalization (which also happens during occurs check) 663 -- is too expensive! (see Issue 415) 664 -- need to do something cheaper, especially if 665 -- we are dealing with a Miller pattern that can be solved 666 -- immediately! 667 -- Ulf, 2011-08-25 DONE! 668 -- Just instantiating the top-level meta, which is cheaper. The occurs 669 -- check will first try without unfolding any definitions (treating 670 -- arguments to definitions as flexible), if that fails it tries again 671 -- with full unfolding. 672 v <- instantiate v 673 reportSDoc "tc.meta.assign" 45 $ 674 "MetaVars.assign: assigning meta " <+> prettyTCM (MetaV x []) <+> 675 " with args " <+> prettyList_ (map (prettyTCM . unArg) args) <+> 676 " to " <+> prettyTCM v 677 reportSDoc "tc.meta.assign" 45 $ 678 "MetaVars.assign: type of meta: " <+> prettyTCM t 679 680 reportSLn "tc.meta.assign" 75 $ 681 "MetaVars.assign: assigning meta " ++ show x ++ " with args " ++ show args ++ " to " ++ show v 682 683 case (v, mvJudgement mvar) of 684 (Sort s, HasType{}) -> hasBiggerSort s 685 _ -> return () 686 687 -- Jesper, 2019-09-13: When --no-sort-comparison is enabled, 688 -- we equate the sort of the solution with the sort of the 689 -- metavariable, in order to solve metavariables in sorts. 690 -- Jesper, 2020-04-22: We do this before any of the other steps 691 -- because comparing the sorts might lead to some metavariables 692 -- being solved, which can help with pruning (see #4615). 693 -- Jesper, 2020-08-25: --no-sort-comparison is now the default 694 -- behaviour. 695 -- 696 -- Under most circumstances, the conversion checker guarantees that 697 -- the solution for the meta has the correct type, so there is no 698 -- need to check anything. However, there are two circumstances in 699 -- which we do need to check the type of the solution: 700 -- 701 -- 1. When comparing two types they are not guaranteed to have the 702 -- same sort. 703 -- 704 -- 2. When --cumulativity is enabled the same can happen when 705 -- comparing two terms at a sort type. 706 707 cumulativity <- optCumulativity <$> pragmaOptions 708 709 let checkSolutionSort cmp s v = do 710 s' <- sortOf v 711 reportSDoc "tc.meta.assign" 40 $ 712 "Instantiating sort" <+> prettyTCM s <+> 713 "to sort" <+> prettyTCM s' <+> "of solution" <+> prettyTCM v 714 traceCall (CheckMetaSolution (getRange mvar) x (sort s) v) $ 715 compareSort cmp s' s 716 717 case (target , mvJudgement mvar) of 718 -- Case 1 (comparing term to meta as types) 719 (AsTypes{} , HasType _ cmp0 t) -> do 720 let cmp = if cumulativity then cmp0 else CmpEq 721 abort = patternViolation $ unblockOnAnyMetaIn t -- TODO: make piApplyM' compute unblocker 722 t' <- piApplyM' abort t args 723 s <- shouldBeSort t' 724 checkSolutionSort cmp s v 725 726 -- Case 2 (comparing term to type-level meta as terms, with --cumulativity) 727 (AsTermsOf{} , HasType _ cmp t) 728 | cumulativity -> do 729 let abort = patternViolation $ unblockOnAnyMetaIn t 730 t' <- piApplyM' abort t args 731 TelV tel t'' <- telView t' 732 addContext tel $ ifNotSort t'' (return ()) $ \s -> do 733 let v' = raise (size tel) v `apply` teleArgs tel 734 checkSolutionSort cmp s v' 735 736 (AsTypes{} , IsSort{} ) -> return () 737 (AsTermsOf{} , _ ) -> return () 738 (AsSizes{} , _ ) -> return () -- TODO: should we do something similar for sizes? 739 740 741 742 -- We don't instantiate frozen mvars 743 when (mvFrozen mvar == Frozen) $ do 744 reportSLn "tc.meta.assign" 25 $ "aborting: meta is frozen!" 745 patternViolation neverUnblock 746 747 -- We never get blocked terms here anymore. TODO: we actually do. why? 748 whenM (isBlockedTerm x) $ do 749 reportSLn "tc.meta.assign" 25 $ "aborting: meta is a blocked term!" 750 patternViolation (unblockOnMeta x) 751 752 -- Andreas, 2010-10-15 I want to see whether rhs is blocked 753 reportSLn "tc.meta.assign" 50 $ "MetaVars.assign: I want to see whether rhs is blocked" 754 reportSDoc "tc.meta.assign" 25 $ do 755 v0 <- reduceB v 756 case v0 of 757 Blocked m0 _ -> "r.h.s. blocked on:" <+> prettyTCM m0 758 NotBlocked{} -> "r.h.s. not blocked" 759 760 -- Turn the assignment problem @_X args >= SizeLt u@ into 761 -- @_X args = SizeLt (_Y args@ and constraint 762 -- @_Y args >= u@. 763 subtypingForSizeLt dir x mvar t args v $ \ v -> do 764 765 reportSDoc "tc.meta.assign.proj" 45 $ do 766 cxt <- getContextTelescope 767 vcat 768 [ "context before projection expansion" 769 , nest 2 $ inTopContext $ prettyTCM cxt 770 ] 771 772 -- Normalise and eta contract the arguments to the meta. These are 773 -- usually small, and simplifying might let us instantiate more metas. 774 -- Also, try to expand away projected vars in meta args. 775 776 expandProjectedVars args (v, target) $ \ args (v, target) -> do 777 778 reportSDoc "tc.meta.assign.proj" 45 $ do 779 cxt <- getContextTelescope 780 vcat 781 [ "context after projection expansion" 782 , nest 2 $ inTopContext $ prettyTCM cxt 783 ] 784 785 -- Andreas, 2019-11-16, issue #4159: 786 -- We would like to save the work we put into expanding projected variables. 787 -- However, the Conversion checker speculatively tries some assignment 788 -- in some places (e.g. shortcut) and relies on an exception to be thrown 789 -- to try other alternatives next. 790 -- If we catch the exception here, this (brittle) mechanism will be broken. 791 -- Maybe one possibility would be to rethrow the exception with the 792 -- new constraint. Then, further up, it could be decided whether 793 -- to discard the new constraint and do something different, 794 -- or add the new constraint when postponing. 795 796 -- BEGIN attempt #4159 797 -- let constraint = case v of 798 -- -- Sort s -> dirToCmp SortCmp dir (MetaS x $ map Apply args) s 799 -- _ -> dirToCmp (\ cmp -> ValueCmp cmp target) dir (MetaV x $ map Apply args) v 800 -- reportSDoc "tc.meta.assign.catch" 40 $ sep 801 -- [ "assign: catching constraint:" 802 -- , prettyTCM constraint 803 -- ] 804 -- -- reportSDoc "tc.meta.assign.catch" 60 $ sep 805 -- -- [ "assign: catching constraint:" 806 -- -- , pretty constraint 807 -- -- ] 808 -- reportSDoc "tc.meta.assign.catch" 80 $ sep 809 -- [ "assign: catching constraint (raw):" 810 -- , (text . show) constraint 811 -- ] 812 -- catchConstraint constraint $ do 813 -- END attempt #4159 814 815 816 -- Andreas, 2011-04-21 do the occurs check first 817 -- e.g. _1 x (suc x) = suc (_2 x y) 818 -- even though the lhs is not a pattern, we can prune the y from _2 819 820 let 821 vars = freeVars args 822 relVL = filterVarMapToList isRelevant vars 823 nonstrictVL = filterVarMapToList isNonStrict vars 824 irrVL = filterVarMapToList (liftM2 (&&) isIrrelevant isUnguarded) vars 825 -- Andreas, 2011-10-06 only irrelevant vars that are direct 826 -- arguments to the meta, hence, can be abstracted over, may 827 -- appear on the rhs. (test/fail/Issue483b) 828 -- Update 2011-03-27: Also irr. vars under record constructors. 829 -- Andreas, 2019-06-25: The reason is that when solving 830 -- @X args = v@ we drop all irrelevant arguments that 831 -- are not variables (after flattening of record constructors). 832 -- (See isVarOrIrrelevant in inverseSubst.) 833 -- Thus, the occurs-check needs to ensure only these variables 834 -- are mentioned on the rhs. 835 -- In the terminology of free variable analysis, the retained 836 -- irrelevant variables are exactly the Unguarded ones. 837 -- Jesper, 2019-10-15: This is actually wrong since it 838 -- will lead to pruning of metas that should not be 839 -- pruned, see #4136. 840 841 reportSDoc "tc.meta.assign" 20 $ 842 let pr (Var n []) = text (show n) 843 pr (Def c []) = prettyTCM c 844 pr _ = ".." 845 in vcat 846 [ "mvar args:" <+> sep (map (pr . unArg) args) 847 , "fvars lhs (rel):" <+> sep (map (text . show) relVL) 848 , "fvars lhs (nonstrict):" <+> sep (map (text . show) nonstrictVL) 849 , "fvars lhs (irr):" <+> sep (map (text . show) irrVL) 850 ] 851 852 -- Check that the x doesn't occur in the right hand side. 853 -- Prune mvars on rhs such that they can only depend on lhs vars. 854 -- Herein, distinguish relevant and irrelevant vars, 855 -- since when abstracting irrelevant lhs vars, they may only occur 856 -- irrelevantly on rhs. 857 -- v <- liftTCM $ occursCheck x (relVL, nonstrictVL, irrVL) v 858 v <- liftTCM $ occursCheck x vars v 859 860 reportSLn "tc.meta.assign" 15 "passed occursCheck" 861 verboseS "tc.meta.assign" 30 $ do 862 let n = termSize v 863 when (n > 200) $ reportSDoc "tc.meta.assign" 30 $ 864 sep [ "size" <+> text (show n) 865-- , nest 2 $ "type" <+> prettyTCM t 866 , nest 2 $ "term" <+> prettyTCM v 867 ] 868 869 -- Check linearity of @ids@ 870 -- Andreas, 2010-09-24: Herein, ignore the variables which are not 871 -- free in v 872 -- Ulf, 2011-09-22: we need to respect irrelevant vars as well, otherwise 873 -- we'll build solutions where the irrelevant terms are not valid 874 let fvs = allFreeVars v 875 reportSDoc "tc.meta.assign" 20 $ 876 "fvars rhs:" <+> sep (map (text . show) $ VarSet.toList fvs) 877 878 -- Check that the arguments are variables 879 mids <- do 880 res <- runExceptT $ inverseSubst args 881 case res of 882 -- all args are variables 883 Right ids -> do 884 reportSDoc "tc.meta.assign" 60 $ 885 "inverseSubst returns:" <+> sep (map pretty ids) 886 reportSDoc "tc.meta.assign" 50 $ 887 "inverseSubst returns:" <+> sep (map prettyTCM ids) 888 let boundVars = VarSet.fromList $ map fst ids 889 if fvs `VarSet.isSubsetOf` boundVars 890 then return $ Just ids 891 else return Nothing 892 -- we have proper values as arguments which could be cased on 893 -- here, we cannot prune, since offending vars could be eliminated 894 Left CantInvert -> return Nothing 895 -- we have non-variables, but these are not eliminateable 896 Left NeutralArg -> Just <$> attemptPruning x args fvs 897 -- we have a projected variable which could not be eta-expanded away: 898 -- same as neutral 899 Left ProjVar{} -> Just <$> attemptPruning x args fvs 900 901 case mids of -- vv Ulf 2014-07-13: actually not needed after all: attemptInertRHSImprovement x args v 902 Nothing -> patternViolation (unblockOnAnyMetaIn v) -- TODO: more precise 903 Just ids -> do 904 -- Check linearity 905 ids <- do 906 res <- runExceptT $ checkLinearity {- (`VarSet.member` fvs) -} ids 907 case res of 908 -- case: linear 909 Right ids -> return ids 910 -- case: non-linear variables that could possibly be pruned 911 -- If pruning fails we need to unblock on any meta in the rhs, since they might get 912 -- rid of the dependency on the non-linear variable. TODO: be more precise (all metas 913 -- using non-linear variables need to be solved). 914 Left () -> addOrUnblocker (unblockOnAnyMetaIn v) $ attemptPruning x args fvs 915 916 -- Check ids is time respecting. 917 () <- do 918 let idvars = map (mapSnd allFreeVars) ids 919 -- earlierThan α v := v "arrives" before α 920 let earlierThan l j = j > l 921 TelV tel' _ <- telViewUpToPath (length args) t 922 forM_ ids $ \(i,u) -> do 923 d <- lookupBV i 924 when (getLock (getArgInfo d) == IsLock) $ do 925 let us = IntSet.unions $ map snd $ filter (earlierThan i . fst) idvars 926 -- us Earlier than u 927 addContext tel' $ checkEarlierThan u us 928 `catchError` \case 929 TypeError{} -> patternViolation (unblockOnMeta x) -- If the earlier check hard-fails we need to 930 err -> throwError err -- solve this meta in some other way. 931 932 let n = length args 933 TelV tel' _ <- telViewUpToPath n t 934 935 -- Check subtyping constraints on the context variables. 936 937 -- Intuition: suppose @_X : (x : A) → B@, then to turn 938 -- @ 939 -- Γ(x : A') ⊢ _X x =?= v : B'@ 940 -- @ 941 -- into 942 -- @ 943 -- Γ ⊢ _X =?= λ x → v 944 -- @ 945 -- we need to check that @A <: A'@ (due to contravariance). 946 let sigma = parallelS $ reverse $ map unArg args 947 hasSubtyping <- collapseDefault . optSubtyping <$> pragmaOptions 948 when hasSubtyping $ forM_ ids $ \(i , u) -> do 949 -- @u@ is a (projected) variable, so we can infer its type 950 a <- applySubst sigma <$> addContext tel' (infer u) 951 a' <- typeOfBV i 952 checkSubtypeIsEqual a' a 953 `catchError` \case 954 TypeError{} -> patternViolation (unblockOnMeta x) -- If the subtype check hard-fails we need to 955 err -> throwError err -- solve this meta in some other way. 956 957 -- Solve. 958 m <- getContextSize 959 assignMeta' m x t n ids v 960 where 961 -- Try to remove meta arguments from lhs that mention variables not occurring on rhs. 962 attemptPruning 963 :: MetaId -- Meta-variable (lhs) 964 -> Args -- Meta arguments (lhs) 965 -> FVs -- Variables occuring on the rhs 966 -> TCM a 967 attemptPruning x args fvs = do 968 -- non-linear lhs: we cannot solve, but prune 969 killResult <- prune x args $ (`VarSet.member` fvs) 970 let success = killResult `elem` [PrunedSomething,PrunedEverything] 971 reportSDoc "tc.meta.assign" 10 $ 972 "pruning" <+> prettyTCM x <+> do text $ if success then "succeeded" else "failed" 973 patternViolation (if success then alwaysUnblock -- If pruning succeeded we want to retry right away 974 else unblockOnAnyMetaIn $ MetaV x $ map Apply args) 975 -- TODO: could be more precise: only unblock on metas 976 -- applied to offending variables 977 978{- UNUSED 979-- | When faced with @_X us == D vs@ for an inert D we can solve this by 980-- @_X xs := D _Ys@ with new constraints @_Yi us == vi@. This is important 981-- for instance arguments, where knowing the head D might enable progress. 982attemptInertRHSImprovement :: MetaId -> Args -> Term -> TCM () 983attemptInertRHSImprovement m args v = do 984 reportSDoc "tc.meta.inert" 30 $ vcat 985 [ "attempting inert rhs improvement" 986 , nest 2 $ sep [ prettyTCM (MetaV m $ map Apply args) <+> "==" 987 , prettyTCM v ] ] 988 -- Check that the right-hand side has the form D vs, for some inert constant D. 989 -- Returns the type of D and a function to build an application of D. 990 (a, mkRHS) <- ensureInert v 991 -- Check that all arguments to the meta are neutral and does not have head D. 992 -- If there are non-neutral arguments there could be solutions to the meta 993 -- that computes over these arguments. If D is an argument to the meta we get 994 -- multiple solutions (for instance: _M Nat == Nat can be solved by both 995 -- _M := \ x -> x and _M := \ x -> Nat). 996 mapM_ (ensureNeutral (mkRHS []) . unArg) args 997 tel <- theTel <$> (telView =<< getMetaType m) 998 -- When attempting shortcut meta solutions, metas aren't necessarily fully 999 -- eta expanded. If this is the case we skip inert improvement. 1000 when (length args < size tel) $ do 1001 reportSDoc "tc.meta.inert" 30 $ "not fully applied" 1002 patternViolation 1003 -- Solve the meta with _M := \ xs -> D (_Y1 xs) .. (_Yn xs), for fresh metas 1004 -- _Yi. 1005 metaArgs <- inTopContext $ addContext tel $ newArgsMeta a 1006 let varArgs = map Apply $ reverse $ zipWith (\i a -> var i <$ a) [0..] (reverse args) 1007 sol = mkRHS metaArgs 1008 argTel = map ("x" <$) args 1009 reportSDoc "tc.meta.inert" 30 $ nest 2 $ vcat 1010 [ "a =" <+> prettyTCM a 1011 , "tel =" <+> prettyTCM tel 1012 , "metas =" <+> prettyList (map prettyTCM metaArgs) 1013 , "sol =" <+> prettyTCM sol 1014 ] 1015 assignTerm m argTel sol 1016 patternViolation -- throwing a pattern violation here lets the constraint 1017 -- machinery worry about restarting the comparison. 1018 where 1019 ensureInert :: Term -> TCM (Type, Args -> Term) 1020 ensureInert v = do 1021 let notInert = do 1022 reportSDoc "tc.meta.inert" 30 $ nest 2 $ "not inert:" <+> prettyTCM v 1023 patternViolation 1024 toArgs elims = 1025 case allApplyElims elims of 1026 Nothing -> do 1027 reportSDoc "tc.meta.inert" 30 $ nest 2 $ "can't do projections from inert" 1028 patternViolation 1029 Just args -> return args 1030 case v of 1031 Var x elims -> (, Var x . map Apply) <$> typeOfBV x 1032 Con c ci args -> notInert -- (, Con c ci) <$> defType <$> getConstInfo (conName c) 1033 Def f elims -> do 1034 def <- getConstInfo f 1035 let good = return (defType def, Def f . map Apply) 1036 case theDef def of 1037 Axiom{} -> good 1038 Datatype{} -> good 1039 Record{} -> good 1040 Function{} -> notInert 1041 Primitive{} -> notInert 1042 Constructor{} -> __IMPOSSIBLE__ 1043 1044 Pi{} -> notInert -- this is actually inert but improving doesn't buy us anything for Pi 1045 Lam{} -> notInert 1046 Sort{} -> notInert 1047 Lit{} -> notInert 1048 Level{} -> notInert 1049 MetaV{} -> notInert 1050 DontCare{} -> notInert 1051 1052 ensureNeutral :: Term -> Term -> TCM () 1053 ensureNeutral rhs v = do 1054 b <- reduceB v 1055 let notNeutral v = do 1056 reportSDoc "tc.meta.inert" 30 $ nest 2 $ "not neutral:" <+> prettyTCM v 1057 patternViolation 1058 checkRHS arg 1059 | arg == rhs = do 1060 reportSDoc "tc.meta.inert" 30 $ nest 2 $ "argument shares head with RHS:" <+> prettyTCM arg 1061 patternViolation 1062 | otherwise = return () 1063 case b of 1064 Blocked{} -> notNeutral v 1065 NotBlocked r v -> -- Andrea(s) 2014-12-06 can r be useful? 1066 case v of 1067 Var x _ -> checkRHS (Var x []) 1068 Def f _ -> checkRHS (Def f []) 1069 Pi{} -> return () 1070 Sort{} -> return () 1071 Level{} -> return () 1072 Lit{} -> notNeutral v 1073 DontCare{} -> notNeutral v 1074 Con{} -> notNeutral v 1075 Lam{} -> notNeutral v 1076 MetaV{} -> __IMPOSSIBLE__ 1077-- END UNUSED -} 1078 1079-- | @assignMeta m x t ids u@ solves @x ids = u@ for meta @x@ of type @t@, 1080-- where term @u@ lives in a context of length @m@. 1081-- Precondition: @ids@ is linear. 1082assignMeta :: Int -> MetaId -> Type -> [Int] -> Term -> TCM () 1083assignMeta m x t ids v = do 1084 let n = length ids 1085 cand = List.sort $ zip ids $ map var $ downFrom n 1086 assignMeta' m x t n cand v 1087 1088-- | @assignMeta' m x t ids u@ solves @x = [ids]u@ for meta @x@ of type @t@, 1089-- where term @u@ lives in a context of length @m@, 1090-- and @ids@ is a partial substitution. 1091assignMeta' :: Int -> MetaId -> Type -> Int -> SubstCand -> Term -> TCM () 1092assignMeta' m x t n ids v = do 1093 -- we are linear, so we can solve! 1094 reportSDoc "tc.meta.assign" 25 $ 1095 "preparing to instantiate: " <+> prettyTCM v 1096 1097 -- Rename the variables in v to make it suitable for abstraction over ids. 1098 -- Basically, if 1099 -- Γ = a b c d e 1100 -- ids = d b e 1101 -- then 1102 -- v' = (λ a b c d e. v) _ 1 _ 2 0 1103 -- 1104 -- Andreas, 2013-10-25 Solve using substitutions: 1105 -- Convert assocList @ids@ (which is sorted) into substitution, 1106 -- filling in __IMPOSSIBLE__ for the missing terms, e.g. 1107 -- [(0,0),(1,2),(3,1)] --> [0, 2, __IMP__, 1, __IMP__] 1108 -- ALT 1: O(m * size ids), serves as specification 1109 -- let ivs = [fromMaybe __IMPOSSIBLE__ $ lookup i ids | i <- [0..m-1]] 1110 -- ALT 2: O(m) 1111 let assocToList i = \case 1112 _ | i >= m -> [] 1113 ((j,u) : l) | i == j -> Just u : assocToList (i+1) l 1114 l -> Nothing : assocToList (i+1) l 1115 ivs = assocToList 0 ids 1116 rho = prependS impossible ivs $ raiseS n 1117 v' = applySubst rho v 1118 1119 -- Metas are top-level so we do the assignment at top-level. 1120 inTopContext $ do 1121 -- Andreas, 2011-04-18 to work with irrelevant parameters 1122 -- we need to construct tel' from the type of the meta variable 1123 -- (no longer from ids which may not be the complete variable list 1124 -- any more) 1125 reportSDoc "tc.meta.assign" 15 $ "type of meta =" <+> prettyTCM t 1126 1127 (telv@(TelV tel' a), bs) <- telViewUpToPathBoundary n t 1128 reportSDoc "tc.meta.assign" 30 $ "tel' =" <+> prettyTCM tel' 1129 reportSDoc "tc.meta.assign" 30 $ "#args =" <+> text (show n) 1130 -- Andreas, 2013-09-17 (AIM XVIII): if t does not provide enough 1131 -- types for the arguments, it might be blocked by a meta; 1132 -- then we give up. (Issue 903) 1133 when (size tel' < n) $ do 1134 a <- abortIfBlocked a 1135 reportSDoc "impossible" 10 $ "not enough pis, but not blocked?" <?> pretty a 1136 __IMPOSSIBLE__ -- If we get here it was _not_ blocked by a meta! 1137 1138 -- Perform the assignment (and wake constraints). 1139 1140 let vsol = abstract tel' v' 1141 1142 -- Andreas, 2013-10-25 double check solution before assigning 1143 whenM (optDoubleCheck <$> pragmaOptions) $ do 1144 m <- lookupMeta x 1145 reportSDoc "tc.meta.check" 30 $ "double checking solution" 1146 catchConstraint (CheckMetaInst x) $ 1147 addContext tel' $ checkSolutionForMeta x m v' a 1148 1149 reportSDoc "tc.meta.assign" 10 $ 1150 "solving" <+> prettyTCM x <+> ":=" <+> prettyTCM vsol 1151 1152 v' <- blockOnBoundary telv bs v' 1153 1154 assignTerm x (telToArgs tel') v' 1155 where 1156 blockOnBoundary :: TelView -> Boundary -> Term -> TCM Term 1157 blockOnBoundary telv [] v = return v 1158 blockOnBoundary (TelV tel t) bs v = addContext tel $ 1159 blockTerm t $ do 1160 neg <- primINeg 1161 forM_ bs $ \ (r,(x,y)) -> do 1162 equalTermOnFace (neg `apply1` r) t x v 1163 equalTermOnFace r t y v 1164 return v 1165 1166-- | Check that the instantiation of the given metavariable fits the 1167-- type of the metavariable. If the metavariable is not yet 1168-- instantiated, add a constraint to check the instantiation later. 1169checkMetaInst :: MetaId -> TCM () 1170checkMetaInst x = do 1171 m <- lookupMeta x 1172 let postpone = addConstraint (unblockOnMeta x) $ CheckMetaInst x 1173 case mvInstantiation m of 1174 BlockedConst{} -> postpone 1175 PostponedTypeCheckingProblem{} -> postpone 1176 Open{} -> postpone 1177 OpenInstance{} -> postpone 1178 InstV xs v -> do 1179 let n = size xs 1180 t = jMetaType $ mvJudgement m 1181 (telv@(TelV tel a),bs) <- telViewUpToPathBoundary n t 1182 catchConstraint (CheckMetaInst x) $ addContext tel $ checkSolutionForMeta x m v a 1183 1184-- | Check that the instantiation of the metavariable with the given 1185-- term is well-typed. 1186checkSolutionForMeta :: MetaId -> MetaVariable -> Term -> Type -> TCM () 1187checkSolutionForMeta x m v a = do 1188 reportSDoc "tc.meta.check" 30 $ "checking solution for meta" <+> prettyTCM x 1189 case mvJudgement m of 1190 HasType{ jComparison = cmp } -> do 1191 reportSDoc "tc.meta.check" 30 $ nest 2 $ 1192 prettyTCM x <+> " : " <+> prettyTCM a <+> ":=" <+> prettyTCM v 1193 reportSDoc "tc.meta.check" 50 $ nest 2 $ do 1194 ctx <- getContext 1195 inTopContext $ "in context: " <+> prettyTCM (PrettyContext ctx) 1196 traceCall (CheckMetaSolution (getRange m) x a v) $ 1197 checkInternal v cmp a 1198 IsSort{} -> void $ do 1199 reportSDoc "tc.meta.check" 30 $ nest 2 $ 1200 prettyTCM x <+> ":=" <+> prettyTCM v <+> " is a sort" 1201 s <- shouldBeSort (El __DUMMY_SORT__ v) 1202 traceCall (CheckMetaSolution (getRange m) x (sort (univSort s)) (Sort s)) $ 1203 checkSort defaultAction s 1204 1205-- | Given two types @a@ and @b@ with @a <: b@, check that @a == b@. 1206checkSubtypeIsEqual :: Type -> Type -> TCM () 1207checkSubtypeIsEqual a b = do 1208 reportSDoc "tc.meta.subtype" 30 $ 1209 "checking that subtype" <+> prettyTCM a <+> 1210 "of" <+> prettyTCM b <+> "is actually equal." 1211 ((a, b), equal) <- SynEq.checkSyntacticEquality a b 1212 unless equal $ do 1213 cumulativity <- optCumulativity <$> pragmaOptions 1214 abortIfBlocked (unEl b) >>= \case 1215 Sort sb -> abortIfBlocked (unEl a) >>= \case 1216 Sort sa | cumulativity -> equalSort sa sb 1217 | otherwise -> return () 1218 Dummy{} -> return () -- TODO: this shouldn't happen but 1219 -- currently does because of generalized 1220 -- metas being created in a dummy context 1221 a -> patternViolation (unblockOnAnyMetaIn a) -- TODO: can this happen? 1222 Pi b1 b2 -> abortIfBlocked (unEl a) >>= \case 1223 Pi a1 a2 1224 | getRelevance a1 /= getRelevance b1 -> patternViolation neverUnblock -- Can we recover from this? 1225 | getQuantity a1 /= getQuantity b1 -> patternViolation neverUnblock 1226 | getCohesion a1 /= getCohesion b1 -> patternViolation neverUnblock 1227 | otherwise -> do 1228 checkSubtypeIsEqual (unDom b1) (unDom a1) 1229 underAbstractionAbs a1 a2 $ \a2' -> checkSubtypeIsEqual a2' (absBody b2) 1230 Dummy{} -> return () -- TODO: this shouldn't happen but 1231 -- currently does because of generalized 1232 -- metas being created in a dummy context 1233 a -> patternViolation (unblockOnAnyMetaIn a) 1234 -- TODO: check subtyping for Size< types 1235 _ -> return () 1236 1237 1238-- | Turn the assignment problem @_X args <= SizeLt u@ into 1239-- @_X args = SizeLt (_Y args)@ and constraint 1240-- @_Y args <= u@. 1241subtypingForSizeLt 1242 :: CompareDirection -- ^ @dir@ 1243 -> MetaId -- ^ The meta variable @x@. 1244 -> MetaVariable -- ^ Its associated information @mvar <- lookupMeta x@. 1245 -> Type -- ^ Its type @t = jMetaType $ mvJudgement mvar@ 1246 -> Args -- ^ Its arguments. 1247 -> Term -- ^ Its to-be-assigned value @v@, such that @x args `dir` v@. 1248 -> (Term -> TCM ()) -- ^ Continuation taking its possibly assigned value. 1249 -> TCM () 1250subtypingForSizeLt DirEq x mvar t args v cont = cont v 1251subtypingForSizeLt dir x mvar t args v cont = do 1252 let fallback = cont v 1253 -- Check whether we have built-ins SIZE and SIZELT 1254 (mSize, mSizeLt) <- getBuiltinSize 1255 caseMaybe mSize fallback $ \ qSize -> do 1256 caseMaybe mSizeLt fallback $ \ qSizeLt -> do 1257 -- Check whether v is a SIZELT 1258 v <- reduce v 1259 case v of 1260 Def q [Apply (Arg ai u)] | q == qSizeLt -> do 1261 -- Clone the meta into a new size meta @y@. 1262 -- To this end, we swap the target of t for Size. 1263 TelV tel _ <- telView t 1264 let size = sizeType_ qSize 1265 t' = telePi tel size 1266 y <- newMeta Instantiable (mvInfo mvar) (mvPriority mvar) (mvPermutation mvar) 1267 (HasType __IMPOSSIBLE__ CmpLeq t') 1268 -- Note: no eta-expansion of new meta possible/necessary. 1269 -- Add the size constraint @y args `dir` u@. 1270 let yArgs = MetaV y $ map Apply args 1271 addConstraint (unblockOnMeta y) $ dirToCmp (`ValueCmp` AsSizes) dir yArgs u 1272 -- We continue with the new assignment problem, and install 1273 -- an exception handler, since we created a meta and a constraint, 1274 -- so we cannot fall back to the original handler. 1275 let xArgs = MetaV x $ map Apply args 1276 v' = Def qSizeLt [Apply $ Arg ai yArgs] 1277 c = dirToCmp (`ValueCmp` (AsTermsOf sizeUniv)) dir xArgs v' 1278 catchConstraint c $ cont v' 1279 _ -> fallback 1280 1281-- | Eta-expand bound variables like @z@ in @X (fst z)@. 1282expandProjectedVars 1283 :: ( Show a, PrettyTCM a, NoProjectedVar a 1284 -- , Normalise a, TermLike a, Subst Term a 1285 , ReduceAndEtaContract a 1286 , PrettyTCM b, TermSubst b 1287 ) 1288 => a -- ^ Meta variable arguments. 1289 -> b -- ^ Right hand side. 1290 -> (a -> b -> TCM c) 1291 -> TCM c 1292expandProjectedVars args v ret = loop (args, v) where 1293 loop (args, v) = do 1294 reportSDoc "tc.meta.assign.proj" 45 $ "meta args: " <+> prettyTCM args 1295 args <- callByName $ reduceAndEtaContract args 1296 reportSDoc "tc.meta.assign.proj" 45 $ "norm args: " <+> prettyTCM args 1297 reportSDoc "tc.meta.assign.proj" 85 $ "norm args: " <+> text (show args) 1298 let done = ret args v 1299 case noProjectedVar args of 1300 Right () -> do 1301 reportSDoc "tc.meta.assign.proj" 40 $ 1302 "no projected var found in args: " <+> prettyTCM args 1303 done 1304 Left (ProjectedVar i _) -> etaExpandProjectedVar i (args, v) done loop 1305 1306-- | Eta-expand a de Bruijn index of record type in context and passed term(s). 1307etaExpandProjectedVar :: (PrettyTCM a, TermSubst a) => Int -> a -> TCM c -> (a -> TCM c) -> TCM c 1308etaExpandProjectedVar i v fail succeed = do 1309 reportSDoc "tc.meta.assign.proj" 40 $ 1310 "trying to expand projected variable" <+> prettyTCM (var i) 1311 caseMaybeM (etaExpandBoundVar i) fail $ \ (delta, sigma, tau) -> do 1312 reportSDoc "tc.meta.assign.proj" 25 $ 1313 "eta-expanding var " <+> prettyTCM (var i) <+> 1314 " in terms " <+> prettyTCM v 1315 unsafeInTopContext $ addContext delta $ 1316 succeed $ applySubst tau v 1317 1318-- | Check whether one of the meta args is a projected var. 1319class NoProjectedVar a where 1320 noProjectedVar :: a -> Either ProjectedVar () 1321 1322 default noProjectedVar 1323 :: (NoProjectedVar b, Foldable t, t b ~ a) 1324 => a -> Either ProjectedVar () 1325 noProjectedVar = Fold.mapM_ noProjectedVar 1326 1327instance NoProjectedVar a => NoProjectedVar (Arg a) 1328instance NoProjectedVar a => NoProjectedVar [a] 1329 1330instance NoProjectedVar Term where 1331 noProjectedVar = \case 1332 Var i es 1333 | qs@(_:_) <- takeWhileJust id $ map isProjElim es 1334 -> Left $ ProjectedVar i qs 1335 -- Andreas, 2015-09-12 Issue #1316: 1336 -- Also look in inductive record constructors 1337 Con (ConHead _ IsRecord{} Inductive _) _ es 1338 | Just vs <- allApplyElims es 1339 -> noProjectedVar vs 1340 _ -> return () 1341 1342-- | Normalize just far enough to be able to eta-contract maximally. 1343class (TermLike a, TermSubst a, Reduce a) => ReduceAndEtaContract a where 1344 reduceAndEtaContract :: a -> TCM a 1345 1346 default reduceAndEtaContract 1347 :: (Traversable f, TermLike b, Subst b, Reduce b, ReduceAndEtaContract b, f b ~ a) 1348 => a -> TCM a 1349 reduceAndEtaContract = Trav.mapM reduceAndEtaContract 1350 1351instance ReduceAndEtaContract a => ReduceAndEtaContract [a] 1352instance ReduceAndEtaContract a => ReduceAndEtaContract (Arg a) 1353 1354instance ReduceAndEtaContract Term where 1355 reduceAndEtaContract u = do 1356 reduce u >>= \case 1357 -- In case of lambda or record constructor, it makes sense to 1358 -- reduce further. 1359 Lam ai (Abs x b) -> etaLam ai x =<< reduceAndEtaContract b 1360 Con c ci es -> etaCon c ci es $ \ r c ci args -> do 1361 args <- reduceAndEtaContract args 1362 etaContractRecord r c ci args 1363 v -> return v 1364 1365{- UNUSED, BUT KEEP! 1366-- Wrong attempt at expanding bound variables. 1367-- The following code curries meta instead. 1368 1369-- | @etaExpandProjectedVar mvar x t n qs@ 1370-- 1371-- @mvar@ is the meta var info. 1372-- @x@ is the meta variable we are trying to solve for. 1373-- @t@ is its type. 1374-- @n@ is the number of the meta arg we want to curry (starting at 0). 1375-- @qs@ is the projection path along which we curry. 1376-- 1377etaExpandProjectedVar :: MetaVariable -> MetaId -> Type -> Int -> [QName] -> TCM a 1378etaExpandProjectedVar mvar x t n qs = inTopContext $ do 1379 (_, uncurry, t') <- curryAt t n 1380 let TelV tel a = telView' t' 1381 perm = idP (size tel) 1382 y <- newMeta (mvInfo mvar) (mvPriority mvar) perm (HasType __IMPOSSIBLE__ t') 1383 assignTerm' x (uncurry $ MetaV y []) 1384 patternViolation 1385-} 1386 1387{- 1388 -- first, strip the leading n domains (which remain unchanged) 1389 TelV gamma core <- telViewUpTo n t 1390 case unEl core of 1391 -- There should be at least one domain left 1392 Pi (Dom ai a) b -> do 1393 -- Eta-expand @dom@ along @qs@ into a telescope @tel@, computing a substitution. 1394 -- For now, we only eta-expand once. 1395 -- This might trigger another call to @etaExpandProjectedVar@ later. 1396 -- A more efficient version does all the eta-expansions at once here. 1397 (r, pars, def) <- fromMaybe __IMPOSSIBLE__ <$> isRecordType a 1398 unless (recEtaEquality def) __IMPOSSIBLE__ 1399 let tel = recTel def `apply` pars 1400 m = size tel 1401 v = Con (recConHead def) $ map var $ downFrom m 1402 b' = raise m b `absApp` v 1403 fs = recFields def 1404 vs = zipWith (\ f i -> Var i [Proj f]) fs $ downFrom m 1405 -- v = c (n-1) ... 1 0 1406 (tel, u) <- etaExpandAtRecordType a $ var 0 1407 -- TODO: compose argInfo ai with tel. 1408 -- Substitute into @b@. 1409 -- Abstract over @tel@. 1410 -- Abstract over @gamma@. 1411 -- Create new meta. 1412 -- Solve old meta, using substitution. 1413 patternViolation 1414 _ -> __IMPOSSIBLE__ 1415-} 1416 1417type FVs = VarSet 1418type SubstCand = [(Int,Term)] -- ^ a possibly non-deterministic substitution 1419 1420-- | Turn non-det substitution into proper substitution, if possible. 1421-- Otherwise, raise the error. 1422checkLinearity :: SubstCand -> ExceptT () TCM SubstCand 1423checkLinearity ids0 = do 1424 let ids = List.sortBy (compare `on` fst) ids0 -- see issue 920 1425 let grps = groupOn fst ids 1426 concat <$> mapM makeLinear grps 1427 where 1428 -- Non-determinism can be healed if type is singleton. [Issue 593] 1429 -- (Same as for irrelevance.) 1430 makeLinear :: SubstCand -> ExceptT () TCM SubstCand 1431 makeLinear [] = __IMPOSSIBLE__ 1432 makeLinear grp@[_] = return grp 1433 makeLinear (p@(i,t) : _) = 1434 ifM ((Right True ==) <$> do lift . runBlocked . isSingletonTypeModuloRelevance =<< typeOfBV i) 1435 (return [p]) 1436 (throwError ()) 1437 1438-- Intermediate result in the following function 1439type Res = [(Arg Nat, Term)] 1440 1441-- | Exceptions raised when substitution cannot be inverted. 1442data InvertExcept 1443 = CantInvert -- ^ Cannot recover. 1444 | NeutralArg -- ^ A potentially neutral arg: can't invert, but can try pruning. 1445 | ProjVar ProjectedVar -- ^ Try to eta-expand var to remove projs. 1446 1447-- | Check that arguments @args@ to a metavar are in pattern fragment. 1448-- Assumes all arguments already in whnf and eta-reduced. 1449-- Parameters are represented as @Var@s so @checkArgs@ really 1450-- checks that all args are @Var@s and returns the "substitution" 1451-- to be applied to the rhs of the equation to solve. 1452-- (If @args@ is considered a substitution, its inverse is returned.) 1453-- 1454-- The returned list might not be ordered. 1455-- Linearity, i.e., whether the substitution is deterministic, 1456-- has to be checked separately. 1457-- 1458inverseSubst :: Args -> ExceptT InvertExcept TCM SubstCand 1459inverseSubst args = map (mapFst unArg) <$> loop (zip args terms) 1460 where 1461 loop = foldM isVarOrIrrelevant [] 1462 terms = map var (downFrom (size args)) 1463 failure = do 1464 lift $ reportSDoc "tc.meta.assign" 15 $ vcat 1465 [ "not all arguments are variables: " <+> prettyTCM args 1466 , " aborting assignment" ] 1467 throwError CantInvert 1468 neutralArg = throwError NeutralArg 1469 1470 isVarOrIrrelevant :: Res -> (Arg Term, Term) -> ExceptT InvertExcept TCM Res 1471 isVarOrIrrelevant vars (Arg info v, t) = do 1472 let irr | isIrrelevant info = True 1473 | DontCare{} <- v = True 1474 | otherwise = False 1475 case stripDontCare v of 1476 -- i := x 1477 Var i [] -> return $ (Arg info i, t) `cons` vars 1478 1479 -- π i := x try to eta-expand projection π away! 1480 Var i es | Just qs <- mapM isProjElim es -> 1481 throwError $ ProjVar $ ProjectedVar i qs 1482 1483 -- (i, j) := x becomes [i := fst x, j := snd x] 1484 -- Andreas, 2013-09-17 but only if constructor is fully applied 1485 Con c ci es -> do 1486 let fallback 1487 | isIrrelevant info = return vars 1488 | otherwise = failure 1489 irrProj <- optIrrelevantProjections <$> pragmaOptions 1490 lift (isRecordConstructor $ conName c) >>= \case 1491 Just (_, r@Record{ recFields = fs }) 1492 | YesEta <- recEtaEquality r -- Andreas, 2019-11-10, issue #4185: only for eta-records 1493 , length fs == length es 1494 , hasQuantity0 info || all usableQuantity fs -- Andreas, 2019-11-12/17, issue #4168b 1495 , irrProj || all isRelevant fs -> do 1496 let aux (Arg _ v) Dom{domInfo = info', unDom = f} = (Arg ai v,) $ t `applyE` [Proj ProjSystem f] where 1497 ai = ArgInfo 1498 { argInfoHiding = min (getHiding info) (getHiding info') 1499 , argInfoModality = Modality 1500 { modRelevance = max (getRelevance info) (getRelevance info') 1501 , modQuantity = max (getQuantity info) (getQuantity info') 1502 , modCohesion = max (getCohesion info) (getCohesion info') 1503 } 1504 , argInfoOrigin = min (getOrigin info) (getOrigin info') 1505 , argInfoFreeVariables = unknownFreeVariables 1506 , argInfoAnnotation = argInfoAnnotation info' 1507 } 1508 vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es 1509 res <- loop $ zipWith aux vs fs 1510 return $ res `append` vars 1511 | otherwise -> fallback 1512 _ -> fallback 1513 1514 -- An irrelevant argument which is not an irrefutable pattern is dropped 1515 _ | irr -> return vars 1516 1517 -- Distinguish args that can be eliminated (Con,Lit,Lam,unsure) ==> failure 1518 -- from those that can only put somewhere as a whole ==> neutralArg 1519 Var{} -> neutralArg 1520 Def{} -> neutralArg -- Note that this Def{} is in normal form and might be prunable. 1521 Lam{} -> failure 1522 Lit{} -> failure 1523 MetaV{} -> failure 1524 Pi{} -> neutralArg 1525 Sort{} -> neutralArg 1526 Level{} -> neutralArg 1527 DontCare{} -> __IMPOSSIBLE__ -- Ruled out by stripDontCare 1528 Dummy s _ -> __IMPOSSIBLE_VERBOSE__ s 1529 1530 -- managing an assoc list where duplicate indizes cannot be irrelevant vars 1531 append :: Res -> Res -> Res 1532 append res vars = foldr cons vars res 1533 1534 -- adding an irrelevant entry only if not present 1535 cons :: (Arg Nat, Term) -> Res -> Res 1536 cons a@(Arg ai i, t) vars 1537 | isIrrelevant ai = applyUnless (any ((i==) . unArg . fst) vars) (a :) vars 1538 | otherwise = a : -- adding a relevant entry 1539 -- filter out duplicate irrelevants 1540 filter (not . (\ a@(Arg info j, t) -> isIrrelevant info && i == j)) vars 1541 1542 1543-- | Turn open metas into postulates. 1544-- 1545-- Preconditions: 1546-- 1547-- 1. We are 'inTopContext'. 1548-- 1549-- 2. 'envCurrentModule' is set to the top-level module. 1550-- 1551openMetasToPostulates :: TCM () 1552openMetasToPostulates = do 1553 m <- asksTC envCurrentModule 1554 1555 -- Go through all open metas. 1556 ms <- IntMap.assocs <$> useTC stMetaStore 1557 forM_ ms $ \ (x, mv) -> do 1558 when (isOpenMeta $ mvInstantiation mv) $ do 1559 let t = dummyTypeToOmega $ jMetaType $ mvJudgement mv 1560 1561 -- Create a name for the new postulate. 1562 let r = clValue $ miClosRange $ mvInfo mv 1563 -- s <- render <$> prettyTCM x -- Using _ is a bad idea, as it prints as prefix op 1564 let s = "unsolved#meta." ++ prettyShow x 1565 n <- freshName r s 1566 let q = A.QName m n 1567 1568 -- Debug. 1569 reportSDoc "meta.postulate" 20 $ vcat 1570 [ text ("Turning " ++ if isSortMeta_ mv then "sort" else "value" ++ " meta ") 1571 <+> prettyTCM (MetaId x) <+> " into postulate." 1572 , nest 2 $ vcat 1573 [ "Name: " <+> prettyTCM q 1574 , "Type: " <+> prettyTCM t 1575 ] 1576 ] 1577 1578 -- Add the new postulate to the signature. 1579 addConstant q $ defaultDefn defaultArgInfo q t defaultAxiom 1580 1581 -- Solve the meta. 1582 let inst = InstV [] $ Def q [] 1583 updateMetaVar (MetaId x) $ \ mv0 -> mv0 { mvInstantiation = inst } 1584 return () 1585 where 1586 -- Unsolved sort metas can have a type ending in a Dummy if they are allowed to be instantiated 1587 -- to Setω. This will crash the serializer (issue #3730). To avoid this we replace dummy type 1588 -- codomains by Setω. 1589 dummyTypeToOmega t = 1590 case telView' t of 1591 TelV tel (El _ Dummy{}) -> abstract tel (sort $ Inf IsFibrant 0) 1592 _ -> t 1593 1594-- | Sort metas in dependency order. 1595dependencySortMetas :: [MetaId] -> TCM (Maybe [MetaId]) 1596dependencySortMetas metas = do 1597 metaGraph <- concat <$> do 1598 forM metas $ \ m -> do 1599 deps <- allMetas (\ m' -> if m' `elem` metas then singleton m' else mempty) <$> getType m 1600 return [ (m, m') | m' <- Set.toList deps ] 1601 1602 return $ Graph.topSort metas metaGraph 1603 1604 where 1605 -- Sort metas don't have types, but we still want to sort them. 1606 getType m = do 1607 mv <- lookupMeta m 1608 case mvJudgement mv of 1609 IsSort{} -> return Nothing 1610 HasType{ jMetaType = t } -> Just <$> instantiateFull t 1611