1{-# LANGUAGE NondecreasingIndentation #-} 2 3{-| Compile-time irrelevance. 4 5In type theory with compile-time irrelevance à la Pfenning (LiCS 2001), 6variables in the context are annotated with relevance attributes. 7@@ 8 Γ = r₁x₁:A₁, ..., rⱼxⱼ:Aⱼ 9@@ 10To handle irrelevant projections, we also record the current relevance 11attribute in the judgement. For instance, this attribute is equal to 12to 'Irrelevant' if we are in an irrelevant position, like an 13irrelevant argument. 14@@ 15 Γ ⊢r t : A 16@@ 17Only relevant variables can be used: 18@@ 19 20 (Relevant x : A) ∈ Γ 21 -------------------- 22 Γ ⊢r x : A 23@@ 24Irrelevant global declarations can only be used if @r = Irrelevant@. 25 26When we enter a @r'@-relevant function argument, we compose the @r@ with @r'@ 27and (left-)divide the attributes in the context by @r'@. 28@@ 29 Γ ⊢r t : (r' x : A) → B r' \ Γ ⊢(r'·r) u : A 30 --------------------------------------------------------- 31 Γ ⊢r t u : B[u/x] 32@@ 33No surprises for abstraction: 34@@ 35 36 Γ, (r' x : A) ⊢r : B 37 ----------------------------- 38 Γ ⊢r λxt : (r' x : A) → B 39@@ 40 41This is different for runtime irrelevance (erasure) which is ``flat'', 42meaning that once one is in an irrelevant context, all new assumptions will 43be usable, since they are turned relevant once entering the context. 44See Conor McBride (WadlerFest 2016), for a type system in this spirit: 45 46We use such a rule for runtime-irrelevance: 47@@ 48 Γ, (q \ q') x : A ⊢q t : B 49 ------------------------------ 50 Γ ⊢q λxt : (q' x : A) → B 51@@ 52 53Conor's system is however set up differently, with a very different 54variable rule: 55 56@@ 57 58 (q x : A) ∈ Γ 59 -------------- 60 Γ ⊢q x : A 61 62 Γ, (q·p) x : A ⊢q t : B 63 ----------------------------- 64 Γ ⊢q λxt : (p x : A) → B 65 66 Γ ⊢q t : (p x : A) → B Γ' ⊢qp u : A 67 ------------------------------------------------- 68 Γ + Γ' ⊢q t u : B[u/x] 69@@ 70 71 72-} 73 74module Agda.TypeChecking.Irrelevance where 75 76import Control.Arrow (second) 77 78import Control.Monad.Except 79 80import qualified Data.Map as Map 81 82import Agda.Interaction.Options 83 84import Agda.Syntax.Common 85import Agda.Syntax.Internal 86 87import Agda.TypeChecking.Monad 88import Agda.TypeChecking.Pretty 89import Agda.TypeChecking.Reduce 90import Agda.TypeChecking.Substitute.Class 91 92import Agda.Utils.Function 93import Agda.Utils.Lens 94import Agda.Utils.Maybe 95import Agda.Utils.Monad 96 97-- | data 'Relevance' 98-- see "Agda.Syntax.Common". 99 100-- * Operations on 'Dom'. 101 102-- | Prepare parts of a parameter telescope for abstraction in constructors 103-- and projections. 104hideAndRelParams :: (LensHiding a, LensRelevance a) => a -> a 105hideAndRelParams = hideOrKeepInstance . mapRelevance nonStrictToIrr 106 107-- * Operations on 'Context'. 108 109-- | Modify the context whenever going from the l.h.s. (term side) 110-- of the typing judgement to the r.h.s. (type side). 111workOnTypes :: (MonadTCEnv m, HasOptions m, MonadDebug m) 112 => m a -> m a 113workOnTypes cont = do 114 allowed <- optExperimentalIrrelevance <$> pragmaOptions 115 verboseBracket "tc.irr" 60 "workOnTypes" $ workOnTypes' allowed cont 116 117-- | Internal workhorse, expects value of --experimental-irrelevance flag 118-- as argument. 119workOnTypes' :: (MonadTCEnv m) => Bool -> m a -> m a 120workOnTypes' experimental 121 = modifyContextInfo (mapRelevance f) 122 . applyQuantityToContext zeroQuantity 123 . typeLevelReductions 124 . localTC (\ e -> e { envWorkingOnTypes = True }) 125 where 126 f | experimental = irrToNonStrict 127 | otherwise = id 128 129-- | (Conditionally) wake up irrelevant variables and make them relevant. 130-- For instance, 131-- in an irrelevant function argument otherwise irrelevant variables 132-- may be used, so they are awoken before type checking the argument. 133-- 134-- Also allow the use of irrelevant definitions. 135applyRelevanceToContext :: (MonadTCEnv tcm, LensRelevance r) => r -> tcm a -> tcm a 136applyRelevanceToContext thing = 137 case getRelevance thing of 138 Relevant -> id 139 rel -> applyRelevanceToContextOnly rel 140 . applyRelevanceToJudgementOnly rel 141 142-- | (Conditionally) wake up irrelevant variables and make them relevant. 143-- For instance, 144-- in an irrelevant function argument otherwise irrelevant variables 145-- may be used, so they are awoken before type checking the argument. 146-- 147-- Precondition: @Relevance /= Relevant@ 148applyRelevanceToContextOnly :: (MonadTCEnv tcm) => Relevance -> tcm a -> tcm a 149applyRelevanceToContextOnly rel = localTC 150 $ over eContext (map $ inverseApplyRelevance rel) 151 . over eLetBindings (Map.map . fmap . second $ inverseApplyRelevance rel) 152 153-- | Apply relevance @rel@ the the relevance annotation of the (typing/equality) 154-- judgement. This is part of the work done when going into a @rel@-context. 155-- 156-- Precondition: @Relevance /= Relevant@ 157applyRelevanceToJudgementOnly :: (MonadTCEnv tcm) => Relevance -> tcm a -> tcm a 158applyRelevanceToJudgementOnly = localTC . over eRelevance . composeRelevance 159 160-- | Like 'applyRelevanceToContext', but only act on context if 161-- @--irrelevant-projections@. 162-- See issue #2170. 163applyRelevanceToContextFunBody :: (MonadTCM tcm, LensRelevance r) => r -> tcm a -> tcm a 164applyRelevanceToContextFunBody thing cont = 165 case getRelevance thing of 166 Relevant -> cont 167 rel -> applyWhenM (optIrrelevantProjections <$> pragmaOptions) 168 (applyRelevanceToContextOnly rel) $ -- enable local irr. defs only when option 169 applyRelevanceToJudgementOnly rel cont -- enable global irr. defs alway 170 171-- | Sets the current quantity (unless the given quantity is 1). 172applyQuantityToContext :: (MonadTCEnv tcm, LensQuantity q) => q -> tcm a -> tcm a 173applyQuantityToContext thing = 174 case getQuantity thing of 175 Quantity1{} -> id 176 q -> applyQuantityToJudgementOnly q 177 178-- | Apply quantity @q@ the the quantity annotation of the (typing/equality) 179-- judgement. This is part of the work done when going into a @q@-context. 180-- 181-- Precondition: @Quantity /= Quantity1@ 182applyQuantityToJudgementOnly :: (MonadTCEnv tcm) => Quantity -> tcm a -> tcm a 183applyQuantityToJudgementOnly = localTC . over eQuantity . composeQuantity 184 185-- | Apply inverse composition with the given cohesion to the typing context. 186applyCohesionToContext :: (MonadTCEnv tcm, LensCohesion m) => m -> tcm a -> tcm a 187applyCohesionToContext thing = 188 case getCohesion thing of 189 m | m == unitCohesion -> id 190 | otherwise -> applyCohesionToContextOnly m 191 -- Cohesion does not apply to the judgment. 192 193applyCohesionToContextOnly :: (MonadTCEnv tcm) => Cohesion -> tcm a -> tcm a 194applyCohesionToContextOnly q = localTC 195 $ over eContext (map $ inverseApplyCohesion q) 196 . over eLetBindings (Map.map . fmap . second $ inverseApplyCohesion q) 197 198-- | Can we split on arguments of the given cohesion? 199splittableCohesion :: (HasOptions m, LensCohesion a) => a -> m Bool 200splittableCohesion a = do 201 let c = getCohesion a 202 pure (usableCohesion c) `and2M` (pure (c /= Flat) `or2M` do optFlatSplit <$> pragmaOptions) 203 204-- | (Conditionally) wake up irrelevant variables and make them relevant. 205-- For instance, 206-- in an irrelevant function argument otherwise irrelevant variables 207-- may be used, so they are awoken before type checking the argument. 208-- 209-- Also allow the use of irrelevant definitions. 210-- 211-- This function might also do something for other modalities. 212applyModalityToContext :: (MonadTCEnv tcm, LensModality m) => m -> tcm a -> tcm a 213applyModalityToContext thing = 214 case getModality thing of 215 m | m == unitModality -> id 216 | otherwise -> applyModalityToContextOnly m 217 . applyModalityToJudgementOnly m 218 219-- | (Conditionally) wake up irrelevant variables and make them relevant. 220-- For instance, 221-- in an irrelevant function argument otherwise irrelevant variables 222-- may be used, so they are awoken before type checking the 223-- argument. 224-- 225-- This function might also do something for other modalities, but 226-- not for quantities. 227-- 228-- Precondition: @Modality /= Relevant@ 229applyModalityToContextOnly :: (MonadTCEnv tcm) => Modality -> tcm a -> tcm a 230applyModalityToContextOnly m = localTC 231 $ over eContext (map $ inverseApplyModalityButNotQuantity m) 232 . over eLetBindings 233 (Map.map . fmap . second $ inverseApplyModalityButNotQuantity m) 234 235-- | Apply modality @m@ the the modality annotation of the (typing/equality) 236-- judgement. This is part of the work done when going into a @m@-context. 237-- 238-- Precondition: @Modality /= Relevant@ 239applyModalityToJudgementOnly :: (MonadTCEnv tcm) => Modality -> tcm a -> tcm a 240applyModalityToJudgementOnly = localTC . over eModality . composeModality 241 242-- | Like 'applyModalityToContext', but only act on context (for Relevance) if 243-- @--irrelevant-projections@. 244-- See issue #2170. 245applyModalityToContextFunBody :: (MonadTCM tcm, LensModality r) => r -> tcm a -> tcm a 246applyModalityToContextFunBody thing cont = do 247 ifM (optIrrelevantProjections <$> pragmaOptions) 248 {-then-} (applyModalityToContext m cont) -- enable global irr. defs always 249 {-else-} (applyRelevanceToContextFunBody (getRelevance m) 250 $ applyCohesionToContext (getCohesion m) 251 $ applyQuantityToContext (getQuantity m) cont) -- enable local irr. defs only when option 252 where 253 m = getModality thing 254 255-- | Wake up irrelevant variables and make them relevant. This is used 256-- when type checking terms in a hole, in which case you want to be able to 257-- (for instance) infer the type of an irrelevant variable. In the course 258-- of type checking an irrelevant function argument 'applyRelevanceToContext' 259-- is used instead, which also sets the context relevance to 'Irrelevant'. 260-- This is not the right thing to do when type checking interactively in a 261-- hole since it also marks all metas created during type checking as 262-- irrelevant (issue #2568). 263-- 264-- Also set the current quantity to 0. 265wakeIrrelevantVars :: (MonadTCEnv tcm) => tcm a -> tcm a 266wakeIrrelevantVars 267 = applyRelevanceToContextOnly Irrelevant 268 . applyQuantityToJudgementOnly zeroQuantity 269 270-- | Check whether something can be used in a position of the given relevance. 271-- 272-- This is a substitute for double-checking that only makes sure 273-- relevances are correct. See issue #2640. 274-- 275-- Used in unifier (@ unifyStep Solution{}@). 276-- 277-- At the moment, this implements McBride-style irrelevance, 278-- where Pfenning-style would be the most accurate thing. 279-- However, these two notions only differ how they handle 280-- bound variables in a term. Here, we are only concerned 281-- in the free variables, used meta-variables, and used 282-- (irrelevant) definitions. 283-- 284class UsableRelevance a where 285 usableRel 286 :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) 287 => Relevance -> a -> m Bool 288 289instance UsableRelevance Term where 290 usableRel rel = \case 291 Var i vs -> do 292 irel <- getRelevance <$> domOfBV i 293 let ok = irel `moreRelevant` rel 294 reportSDoc "tc.irr" 50 $ 295 "Variable" <+> prettyTCM (var i) <+> 296 text ("has relevance " ++ show irel ++ ", which is " ++ 297 (if ok then "" else "NOT ") ++ "more relevant than " ++ show rel) 298 return ok `and2M` usableRel rel vs 299 Def f vs -> do 300 frel <- relOfConst f 301 return (frel `moreRelevant` rel) `and2M` usableRel rel vs 302 Con c _ vs -> usableRel rel vs 303 Lit l -> return True 304 Lam _ v -> usableRel rel v 305 Pi a b -> usableRel rel (a,b) 306 Sort s -> usableRel rel s 307 Level l -> return True 308 MetaV m vs -> do 309 mrel <- getMetaRelevance <$> lookupMeta m 310 return (mrel `moreRelevant` rel) `and2M` usableRel rel vs 311 DontCare v -> usableRel rel v -- TODO: allow irrelevant things to be used in DontCare position? 312 Dummy{} -> return True 313 314instance UsableRelevance a => UsableRelevance (Type' a) where 315 usableRel rel (El _ t) = usableRel rel t 316 317instance UsableRelevance Sort where 318 usableRel rel = \case 319 Type l -> usableRel rel l 320 Prop l -> usableRel rel l 321 Inf f n -> return True 322 SSet l -> usableRel rel l 323 SizeUniv -> return True 324 LockUniv -> return True 325 PiSort a s1 s2 -> usableRel rel (a,s1,s2) 326 FunSort s1 s2 -> usableRel rel (s1,s2) 327 UnivSort s -> usableRel rel s 328 MetaS x es -> usableRel rel es 329 DefS d es -> usableRel rel $ Def d es 330 DummyS{} -> return True 331 332instance UsableRelevance Level where 333 usableRel rel (Max _ ls) = usableRel rel ls 334 335instance UsableRelevance PlusLevel where 336 usableRel rel (Plus _ l) = usableRel rel l 337 338instance UsableRelevance a => UsableRelevance [a] where 339 usableRel rel = andM . map (usableRel rel) 340 341instance (UsableRelevance a, UsableRelevance b) => UsableRelevance (a,b) where 342 usableRel rel (a,b) = usableRel rel a `and2M` usableRel rel b 343 344instance (UsableRelevance a, UsableRelevance b, UsableRelevance c) => UsableRelevance (a,b,c) where 345 usableRel rel (a,b,c) = usableRel rel a `and2M` usableRel rel b `and2M` usableRel rel c 346 347instance UsableRelevance a => UsableRelevance (Elim' a) where 348 usableRel rel (Apply a) = usableRel rel a 349 usableRel rel (Proj _ p) = do 350 prel <- relOfConst p 351 return $ prel `moreRelevant` rel 352 usableRel rel (IApply x y v) = allM [x,y,v] $ usableRel rel 353 354instance UsableRelevance a => UsableRelevance (Arg a) where 355 usableRel rel (Arg info u) = 356 let rel' = getRelevance info 357 in usableRel (rel `composeRelevance` rel') u 358 359instance UsableRelevance a => UsableRelevance (Dom a) where 360 usableRel rel Dom{unDom = u} = usableRel rel u 361 362instance (Subst a, UsableRelevance a) => UsableRelevance (Abs a) where 363 usableRel rel abs = underAbstraction_ abs $ \u -> usableRel rel u 364 365-- | Check whether something can be used in a position of the given modality. 366-- 367-- This is a substitute for double-checking that only makes sure 368-- modalities are correct. See issue #2640. 369-- 370-- Used in unifier (@ unifyStep Solution{}@). 371-- 372-- This uses McBride-style modality checking. 373-- It does not differ from Pfenning-style if we 374-- are only interested in the modality of the 375-- free variables, used meta-variables, and used 376-- definitions. 377-- 378class UsableModality a where 379 usableMod 380 :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) 381 => Modality -> a -> m Bool 382 383instance UsableModality Term where 384 usableMod mod u = do 385 case u of 386 Var i vs -> do 387 imod <- getModality <$> domOfBV i 388 let ok = imod `moreUsableModality` mod 389 reportSDoc "tc.irr" 50 $ 390 "Variable" <+> prettyTCM (var i) <+> 391 text ("has modality " ++ show imod ++ ", which is a " ++ 392 (if ok then "" else "NOT ") ++ "more usable modality than " ++ show mod) 393 return ok `and2M` usableMod mod vs 394 Def f vs -> do 395 fmod <- modalityOfConst f 396 let ok = fmod `moreUsableModality` mod 397 reportSDoc "tc.irr" 50 $ 398 "Definition" <+> prettyTCM (Def f []) <+> 399 text ("has modality " ++ show fmod ++ ", which is a " ++ 400 (if ok then "" else "NOT ") ++ "more usable modality than " ++ show mod) 401 return ok `and2M` usableMod mod vs 402 Con c _ vs -> usableMod mod vs 403 Lit l -> return True 404 Lam info v -> usableModAbs info mod v 405 -- Even if Pi contains Type, here we check it as a constructor for terms in the universe. 406 Pi a b -> usableMod domMod (unEl $ unDom a) `and2M` usableModAbs (getArgInfo a) mod (unEl <$> b) 407 where 408 domMod = mapQuantity (composeQuantity $ getQuantity a) $ 409 mapCohesion (composeCohesion $ getCohesion a) mod 410 -- Andrea 15/10/2020 not updating these cases yet, but they are quite suspicious, 411 -- do we have special typing rules for Sort and Level? 412 Sort s -> usableMod mod s 413 Level l -> return True 414 MetaV m vs -> do 415 mmod <- getMetaModality <$> lookupMeta m 416 let ok = mmod `moreUsableModality` mod 417 reportSDoc "tc.irr" 50 $ 418 "Metavariable" <+> prettyTCM (MetaV m []) <+> 419 text ("has modality " ++ show mmod ++ ", which is a " ++ 420 (if ok then "" else "NOT ") ++ "more usable modality than " ++ show mod) 421 (return ok `and2M` usableMod mod vs) `or2M` do 422 u <- instantiate u 423 caseMaybe (isMeta u) (usableMod mod u) $ \ m -> throwError (UnblockOnMeta m) 424 DontCare v -> usableMod mod v 425 Dummy{} -> return True 426 427usableModAbs :: (Subst a, MonadAddContext m, UsableModality a, 428 ReadTCState m, HasConstInfo m, MonadReduce m, MonadError Blocker m) => 429 ArgInfo -> Modality -> Abs a -> m Bool 430usableModAbs info mod abs = underAbstraction (setArgInfo info $ __DUMMY_DOM__) abs $ \ u -> usableMod mod u 431 432instance UsableRelevance a => UsableModality (Type' a) where 433 usableMod mod (El _ t) = usableRel (getRelevance mod) t 434 435instance UsableModality Sort where 436 usableMod mod s = usableRel (getRelevance mod) s 437 -- usableMod mod s = case s of 438 -- Type l -> usableMod mod l 439 -- Prop l -> usableMod mod l 440 -- Inf -> return True 441 -- SizeUniv -> return True 442 -- PiSort a s -> usableMod mod (a,s) 443 -- UnivSort s -> usableMod mod s 444 -- MetaS x es -> usableMod mod es 445 -- DummyS{} -> return True 446 447instance UsableModality Level where 448 usableMod mod (Max _ ls) = usableRel (getRelevance mod) ls 449 450-- instance UsableModality PlusLevel where 451-- usableMod mod ClosedLevel{} = return True 452-- usableMod mod (Plus _ l) = usableMod mod l 453 454instance UsableModality a => UsableModality [a] where 455 usableMod mod = andM . map (usableMod mod) 456 457instance (UsableModality a, UsableModality b) => UsableModality (a,b) where 458 usableMod mod (a,b) = usableMod mod a `and2M` usableMod mod b 459 460instance UsableModality a => UsableModality (Elim' a) where 461 usableMod mod (Apply a) = usableMod mod a 462 usableMod mod (Proj _ p) = do 463 pmod <- modalityOfConst p 464 return $ pmod `moreUsableModality` mod 465 usableMod mod (IApply x y v) = allM [x,y,v] $ usableMod mod 466 467instance UsableModality a => UsableModality (Arg a) where 468 usableMod mod (Arg info u) = 469 let mod' = getModality info 470 in usableMod (mod `composeModality` mod') u 471 472instance UsableModality a => UsableModality (Dom a) where 473 usableMod mod Dom{unDom = u} = usableMod mod u 474 475usableAtModality :: MonadConstraint TCM => Modality -> Term -> TCM () 476usableAtModality mod t = catchConstraint (UsableAtModality mod t) $ do 477 res <- runExceptT $ usableMod mod t 478 case res of 479 Right b -> do 480 unless b $ 481 typeError . GenericDocError =<< (prettyTCM t <+> "is not usable at the required modality" <+> prettyTCM mod) 482 Left blocker -> patternViolation blocker 483 484 485-- * Propositions 486 487-- | Is a type a proposition? (Needs reduction.) 488 489isPropM 490 :: (LensSort a, PrettyTCM a, PureTCM m, MonadBlock m) 491 => a -> m Bool 492isPropM a = do 493 traceSDoc "tc.prop" 80 ("Is " <+> prettyTCM a <+> "of sort" <+> prettyTCM (getSort a) <+> "in Prop?") $ do 494 abortIfBlocked (getSort a) <&> \case 495 Prop{} -> True 496 _ -> False 497 498isIrrelevantOrPropM 499 :: (LensRelevance a, LensSort a, PrettyTCM a, PureTCM m, MonadBlock m) 500 => a -> m Bool 501isIrrelevantOrPropM x = return (isIrrelevant x) `or2M` isPropM x 502 503-- * Fibrant types 504 505-- | Is a type fibrant (i.e. Type, Prop)? 506 507isFibrant 508 :: (LensSort a, PureTCM m, MonadBlock m) 509 => a -> m Bool 510isFibrant a = abortIfBlocked (getSort a) <&> \case 511 Type{} -> True 512 Prop{} -> True 513 Inf f _ -> f == IsFibrant 514 SSet{} -> False 515 SizeUniv{} -> False 516 LockUniv{} -> False 517 PiSort{} -> False 518 FunSort{} -> False 519 UnivSort{} -> False 520 MetaS{} -> False 521 DefS{} -> False 522 DummyS{} -> False 523 524 525-- | Cofibrant types are those that could be the domain of a fibrant 526-- pi type. (Notion by C. Sattler). 527isCoFibrantSort :: (LensSort a, PureTCM m, MonadBlock m) => a -> m Bool 528isCoFibrantSort a = abortIfBlocked (getSort a) <&> \case 529 Type{} -> True 530 Prop{} -> True 531 Inf f _ -> f == IsFibrant 532 SSet{} -> False 533 SizeUniv{} -> False 534 LockUniv{} -> True 535 PiSort{} -> False 536 FunSort{} -> False 537 UnivSort{} -> False 538 MetaS{} -> False 539 DefS{} -> False 540 DummyS{} -> False 541