1{-# LANGUAGE NondecreasingIndentation #-} 2 3module Agda.TypeChecking.Rules.Term where 4 5import Prelude hiding ( null ) 6 7import Control.Monad.Except 8import Control.Monad.Reader 9 10import Data.Maybe 11import Data.Either (partitionEithers, lefts) 12import qualified Data.List as List 13import qualified Data.Map as Map 14import qualified Data.Set as Set 15 16import Agda.Interaction.Options 17import Agda.Interaction.Highlighting.Generate (disambiguateRecordFields) 18 19import Agda.Syntax.Abstract (Binder) 20import qualified Agda.Syntax.Abstract as A 21import Agda.Syntax.Abstract.Views as A 22import qualified Agda.Syntax.Info as A 23import Agda.Syntax.Concrete.Pretty () -- only Pretty instances 24import Agda.Syntax.Concrete (FieldAssignment'(..), nameFieldA) 25import qualified Agda.Syntax.Concrete.Name as C 26import Agda.Syntax.Common 27import Agda.Syntax.Internal as I 28import Agda.Syntax.Internal.MetaVars 29import Agda.Syntax.Position 30import Agda.Syntax.Literal 31import Agda.Syntax.Scope.Base ( ThingsInScope, AbstractName 32 , emptyScopeInfo 33 , exportedNamesInScope) 34import Agda.Syntax.Scope.Monad (getNamedScope) 35 36import Agda.TypeChecking.CompiledClause 37import Agda.TypeChecking.Constraints 38import Agda.TypeChecking.Conversion 39import Agda.TypeChecking.Coverage.SplitTree 40import Agda.TypeChecking.Datatypes 41import Agda.TypeChecking.EtaContract 42import Agda.TypeChecking.Generalize 43import Agda.TypeChecking.Implicit 44import Agda.TypeChecking.Irrelevance 45import Agda.TypeChecking.IApplyConfluence 46import Agda.TypeChecking.Level 47import Agda.TypeChecking.Lock (requireGuarded) 48import Agda.TypeChecking.MetaVars 49import Agda.TypeChecking.Monad 50import Agda.TypeChecking.Patterns.Abstract 51import Agda.TypeChecking.Positivity.Occurrence 52import Agda.TypeChecking.Pretty 53import Agda.TypeChecking.Primitive 54import Agda.TypeChecking.Quote 55import Agda.TypeChecking.RecordPatterns 56import Agda.TypeChecking.Records 57import Agda.TypeChecking.Reduce 58import Agda.TypeChecking.Rules.LHS 59import Agda.TypeChecking.SizedTypes 60import Agda.TypeChecking.SizedTypes.Solve 61import Agda.TypeChecking.Sort 62import Agda.TypeChecking.Substitute 63import Agda.TypeChecking.Telescope 64import Agda.TypeChecking.Unquote 65import Agda.TypeChecking.Warnings 66 67import {-# SOURCE #-} Agda.TypeChecking.Empty ( ensureEmptyType ) 68import {-# SOURCE #-} Agda.TypeChecking.Rules.Def (checkFunDef', useTerPragma) 69import {-# SOURCE #-} Agda.TypeChecking.Rules.Decl (checkSectionApplication) 70import {-# SOURCE #-} Agda.TypeChecking.Rules.Application 71 72import Agda.Utils.Functor 73import Agda.Utils.Lens 74import Agda.Utils.List 75import Agda.Utils.List1 ( List1, pattern (:|) ) 76import qualified Agda.Utils.List1 as List1 77import Agda.Utils.Maybe 78import Agda.Utils.Monad 79import Agda.Utils.Null 80import Agda.Utils.Pretty ( prettyShow ) 81import qualified Agda.Utils.Pretty as P 82import Agda.Utils.Singleton 83import Agda.Utils.Size 84import Agda.Utils.Tuple 85 86import Agda.Utils.Impossible 87 88--------------------------------------------------------------------------- 89-- * Types 90--------------------------------------------------------------------------- 91 92-- | Check that an expression is a type. 93isType :: A.Expr -> Sort -> TCM Type 94isType = isType' CmpLeq 95 96-- | Check that an expression is a type. 97-- * If @c == CmpEq@, the given sort must be the minimal sort. 98-- * If @c == CmpLeq@, the given sort may be any bigger sort. 99isType' :: Comparison -> A.Expr -> Sort -> TCM Type 100isType' c e s = 101 traceCall (IsTypeCall c e s) $ do 102 v <- checkExpr' c e (sort s) 103 return $ El s v 104 105-- | Check that an expression is a type and infer its (minimal) sort. 106isType_ :: A.Expr -> TCM Type 107isType_ e = traceCall (IsType_ e) $ do 108 reportResult "tc.term.istype" 15 (\a -> vcat 109 [ "isType_" <?> prettyTCM e 110 , nest 2 $ "returns" <?> prettyTCM a 111 ]) $ do 112 let fallback = isType' CmpEq e =<< do workOnTypes $ newSortMeta 113 SortKit{..} <- sortKit 114 case unScope e of 115 A.Fun i (Arg info t) b -> do 116 a <- setArgInfo info . defaultDom <$> checkPiDomain (info :| []) t 117 b <- isType_ b 118 s <- inferFunSort (getSort a) (getSort b) 119 let t' = El s $ Pi a $ NoAbs underscore b 120 --noFunctionsIntoSize t' 121 return t' 122 A.Pi _ tel e -> do 123 (t0, t') <- checkPiTelescope (List1.toList tel) $ \ tel -> do 124 t0 <- instantiateFull =<< isType_ e 125 tel <- instantiateFull tel 126 return (t0, telePi tel t0) 127 checkTelePiSort t' 128 --noFunctionsIntoSize t' 129 return t' 130 131 A.Generalized s e -> do 132 (_, t') <- generalizeType s $ isType_ e 133 --noFunctionsIntoSize t' 134 return t' 135 136 -- Setᵢ 137 A.Def' x suffix | x == nameOfSet -> case suffix of 138 NoSuffix -> return $ sort (mkType 0) 139 Suffix i -> return $ sort (mkType i) 140 141 -- Propᵢ 142 A.Def' x suffix | x == nameOfProp -> do 143 unlessM isPropEnabled $ typeError NeedOptionProp 144 case suffix of 145 NoSuffix -> return $ sort (mkProp 0) 146 Suffix i -> return $ sort (mkProp i) 147 148 -- Setᵢ 149 A.Def' x suffix | x == nameOfSSet -> do 150 unlessM isTwoLevelEnabled $ typeError NeedOptionTwoLevel 151 case suffix of 152 NoSuffix -> return $ sort (mkSSet 0) 153 Suffix i -> return $ sort (mkSSet i) 154 155 -- Setωᵢ 156 A.Def' x suffix | x == nameOfSetOmega IsFibrant -> case suffix of 157 NoSuffix -> return $ sort (Inf IsFibrant 0) 158 Suffix i -> return $ sort (Inf IsFibrant i) 159 160 -- SSetωᵢ 161 A.Def' x suffix | x == nameOfSetOmega IsStrict -> do 162 unlessM isTwoLevelEnabled $ typeError NeedOptionTwoLevel 163 case suffix of 164 NoSuffix -> return $ sort (Inf IsStrict 0) 165 Suffix i -> return $ sort (Inf IsStrict i) 166 167 -- Set ℓ 168 A.App i s arg 169 | visible arg, 170 A.Def x <- unScope s, 171 x == nameOfSet -> do 172 unlessM hasUniversePolymorphism $ genericError 173 "Use --universe-polymorphism to enable level arguments to Set" 174 -- allow NonStrict variables when checking level 175 -- Set : (NonStrict) Level -> Set\omega 176 applyRelevanceToContext NonStrict $ 177 sort . Type <$> checkLevel arg 178 179 -- Prop ℓ 180 A.App i s arg 181 | visible arg, 182 A.Def x <- unScope s, 183 x == nameOfProp -> do 184 unlessM isPropEnabled $ typeError NeedOptionProp 185 unlessM hasUniversePolymorphism $ genericError 186 "Use --universe-polymorphism to enable level arguments to Prop" 187 applyRelevanceToContext NonStrict $ 188 sort . Prop <$> checkLevel arg 189 190 -- SSet ℓ 191 A.App i s arg 192 | visible arg, 193 A.Def x <- unScope s, 194 x == nameOfSSet -> do 195 unlessM isTwoLevelEnabled $ typeError NeedOptionTwoLevel 196 unlessM hasUniversePolymorphism $ genericError 197 "Use --universe-polymorphism to enable level arguments to SSet" 198 applyRelevanceToContext NonStrict $ 199 sort . SSet <$> checkLevel arg 200 201 -- Issue #707: Check an existing interaction point 202 A.QuestionMark minfo ii -> caseMaybeM (lookupInteractionMeta ii) fallback $ \ x -> do 203 -- -- | Just x <- A.metaNumber minfo -> do 204 reportSDoc "tc.ip" 20 $ fsep 205 [ "Rechecking meta " 206 , prettyTCM x 207 , text $ " for interaction point " ++ show ii 208 ] 209 mv <- lookupMeta x 210 let s0 = jMetaType . mvJudgement $ mv 211 -- Andreas, 2016-10-14, issue #2257 212 -- The meta was created in a context of length @n@. 213 let n = length . envContext . clEnv . miClosRange . mvInfo $ mv 214 (vs, rest) <- splitAt n <$> getContextArgs 215 reportSDoc "tc.ip" 20 $ vcat 216 [ " s0 = " <+> prettyTCM s0 217 , " vs = " <+> prettyTCM vs 218 , " rest = " <+> prettyTCM rest 219 ] 220 -- We assume the meta variable use here is in an extension of the original context. 221 -- If not we revert to the old buggy behavior of #707 (see test/Succeed/Issue2257b). 222 if (length vs /= n) then fallback else do 223 s1 <- reduce =<< piApplyM s0 vs 224 reportSDoc "tc.ip" 20 $ vcat 225 [ " s1 = " <+> prettyTCM s1 226 ] 227 reportSDoc "tc.ip" 70 $ vcat 228 [ " s1 = " <+> text (show s1) 229 ] 230 case unEl s1 of 231 Sort s -> return $ El s $ MetaV x $ map Apply vs 232 _ -> __IMPOSSIBLE__ 233 234 _ -> fallback 235 236checkLevel :: NamedArg A.Expr -> TCM Level 237checkLevel arg = do 238 lvl <- levelType 239 levelView =<< checkNamedArg arg lvl 240 241-- | Ensure that a (freshly created) function type does not inhabit 'SizeUniv'. 242-- Precondition: When @noFunctionsIntoSize t tBlame@ is called, 243-- we are in the context of @tBlame@ in order to print it correctly. 244-- Not being in context of @t@ should not matter, as we are only 245-- checking whether its sort reduces to 'SizeUniv'. 246-- 247-- Currently UNUSED since SizeUniv is turned off (as of 2016). 248{- 249noFunctionsIntoSize :: Type -> Type -> TCM () 250noFunctionsIntoSize t tBlame = do 251 reportSDoc "tc.fun" 20 $ do 252 let El s (Pi dom b) = tBlame 253 sep [ "created function type " <+> prettyTCM tBlame 254 , "with pts rule (" <+> prettyTCM (getSort dom) <+> 255 "," <+> underAbstraction_ b (prettyTCM . getSort) <+> 256 "," <+> prettyTCM s <+> ")" 257 ] 258 s <- reduce $ getSort t 259 when (s == SizeUniv) $ do 260 -- Andreas, 2015-02-14 261 -- We have constructed a function type in SizeUniv 262 -- which is illegal to prevent issue 1428. 263 typeError $ FunctionTypeInSizeUniv $ unEl tBlame 264-} 265 266-- | Check that an expression is a type which is equal to a given type. 267isTypeEqualTo :: A.Expr -> Type -> TCM Type 268isTypeEqualTo e0 t = scopedExpr e0 >>= \case 269 A.ScopedExpr{} -> __IMPOSSIBLE__ 270 A.Underscore i | isNothing (A.metaNumber i) -> return t 271 e -> workOnTypes $ do 272 t' <- isType e (getSort t) 273 t' <$ leqType t t' 274 275leqType_ :: Type -> Type -> TCM () 276leqType_ t t' = workOnTypes $ leqType t t' 277 278--------------------------------------------------------------------------- 279-- * Telescopes 280--------------------------------------------------------------------------- 281 282checkGeneralizeTelescope :: A.GeneralizeTelescope -> ([Maybe Name] -> Telescope -> TCM a) -> TCM a 283checkGeneralizeTelescope (A.GeneralizeTel vars tel) k = 284 generalizeTelescope vars (checkTelescope tel) k 285 286-- | Type check a (module) telescope. 287-- Binds the variables defined by the telescope. 288checkTelescope :: A.Telescope -> (Telescope -> TCM a) -> TCM a 289checkTelescope = checkTelescope' LamNotPi 290 291-- | Type check the telescope of a dependent function type. 292-- Binds the resurrected variables defined by the telescope. 293-- The returned telescope is unmodified (not resurrected). 294checkPiTelescope :: A.Telescope -> (Telescope -> TCM a) -> TCM a 295checkPiTelescope = checkTelescope' PiNotLam 296 297-- | Flag to control resurrection on domains. 298data LamOrPi 299 = LamNotPi -- ^ We are checking a module telescope. 300 -- We pass into the type world to check the domain type. 301 -- This resurrects the whole context. 302 | PiNotLam -- ^ We are checking a telescope in a Pi-type. 303 -- We stay in the term world, but add resurrected 304 -- domains to the context to check the remaining 305 -- domains and codomain of the Pi-type. 306 deriving (Eq, Show) 307 308-- | Type check a telescope. Binds the variables defined by the telescope. 309checkTelescope' :: LamOrPi -> A.Telescope -> (Telescope -> TCM a) -> TCM a 310checkTelescope' lamOrPi [] ret = ret EmptyTel 311checkTelescope' lamOrPi (b : tel) ret = 312 checkTypedBindings lamOrPi b $ \tel1 -> 313 checkTelescope' lamOrPi tel $ \tel2 -> 314 ret $ abstract tel1 tel2 315 316-- | Check the domain of a function type. 317-- Used in @checkTypedBindings@ and to typecheck @A.Fun@ cases. 318checkDomain :: (LensLock a, LensModality a) => LamOrPi -> List1 a -> A.Expr -> TCM Type 319checkDomain lamOrPi xs e = do 320 let (c :| cs) = fmap (getCohesion . getModality) xs 321 unless (all (c ==) cs) $ __IMPOSSIBLE__ 322 323 let (q :| qs) = fmap (getQuantity . getModality) xs 324 unless (all (q ==) qs) $ __IMPOSSIBLE__ 325 326 t <- applyQuantityToContext q $ 327 applyCohesionToContext c $ 328 modEnv lamOrPi $ isType_ e 329 -- Andrea TODO: also make sure that LockUniv implies IsLock 330 when (any (\ x -> getLock x == IsLock) xs) $ do 331 requireGuarded "which is needed for @tick/@lock attributes." 332 -- Solves issue #5033 333 unlessM (isJust <$> getName' builtinLockUniv) $ do 334 genericDocError $ "Missing binding for primLockUniv primitive." 335 336 equalSort (getSort t) LockUniv 337 338 return t 339 where 340 -- if we are checking a typed lambda, we resurrect before we check the 341 -- types, but do not modify the new context entries 342 -- otherwise, if we are checking a pi, we do not resurrect, but 343 -- modify the new context entries 344 modEnv LamNotPi = workOnTypes 345 modEnv _ = id 346 347checkPiDomain :: (LensLock a, LensModality a) => List1 a -> A.Expr -> TCM Type 348checkPiDomain = checkDomain PiNotLam 349 350-- | Check a typed binding and extends the context with the bound variables. 351-- The telescope passed to the continuation is valid in the original context. 352-- 353-- Parametrized by a flag wether we check a typed lambda or a Pi. This flag 354-- is needed for irrelevance. 355 356checkTypedBindings :: LamOrPi -> A.TypedBinding -> (Telescope -> TCM a) -> TCM a 357checkTypedBindings lamOrPi (A.TBind r tac xps e) ret = do 358 let xs = fmap (updateNamedArg $ A.unBind . A.binderName) xps 359 tac <- traverse (checkTacticAttribute lamOrPi) tac 360 whenJust tac $ \ t -> reportSDoc "tc.term.tactic" 30 $ "Checked tactic attribute:" <?> prettyTCM t 361 -- Andreas, 2011-04-26 irrelevant function arguments may appear 362 -- non-strictly in the codomain type 363 -- 2011-10-04 if flag --experimental-irrelevance is set 364 experimental <- optExperimentalIrrelevance <$> pragmaOptions 365 366 t <- checkDomain lamOrPi xps e 367 368 -- Jesper, 2019-02-12, Issue #3534: warn if the type of an 369 -- instance argument does not have the right shape 370 List1.unlessNull (List1.filter isInstance xps) $ \ ixs -> do 371 (tel, target) <- getOutputTypeName t 372 case target of 373 OutputTypeName{} -> return () 374 OutputTypeVar{} -> return () 375 OutputTypeVisiblePi{} -> warning . InstanceArgWithExplicitArg =<< prettyTCM (A.mkTBind r ixs e) 376 OutputTypeNameNotYetKnown{} -> return () 377 NoOutputTypeName -> warning . InstanceNoOutputTypeName =<< prettyTCM (A.mkTBind r ixs e) 378 379 let setTac tac EmptyTel = EmptyTel 380 setTac tac (ExtendTel dom tel) = ExtendTel dom{ domTactic = tac } $ setTac (raise 1 tac) <$> tel 381 xs' = fmap (modMod lamOrPi experimental) xs 382 let tel = setTac tac $ namedBindsToTel1 xs t 383 384 addContext (xs', t) $ addTypedPatterns xps (ret tel) 385 386 where 387 -- if we are checking a typed lambda, we resurrect before we check the 388 -- types, but do not modify the new context entries 389 -- otherwise, if we are checking a pi, we do not resurrect, but 390 -- modify the new context entries 391 modEnv LamNotPi = workOnTypes 392 modEnv _ = id 393 modMod PiNotLam xp = (if xp then mapRelevance irrToNonStrict else id) 394 modMod _ _ = id 395 396checkTypedBindings lamOrPi (A.TLet _ lbs) ret = do 397 checkLetBindings lbs (ret EmptyTel) 398 399-- | After a typed binding has been checked, add the patterns it binds 400addTypedPatterns :: List1 (NamedArg A.Binder) -> TCM a -> TCM a 401addTypedPatterns xps ret = do 402 let ps = List1.mapMaybe (A.extractPattern . namedArg) xps 403 let lbs = map letBinding ps 404 checkLetBindings lbs ret 405 where 406 letBinding :: (A.Pattern, A.BindName) -> A.LetBinding 407 letBinding (p, n) = A.LetPatBind (A.LetRange r) p (A.Var $ A.unBind n) 408 where r = fuseRange p n 409 410-- | Check a tactic attribute. Should have type Term → TC ⊤. 411checkTacticAttribute :: LamOrPi -> A.Expr -> TCM Term 412checkTacticAttribute LamNotPi e = genericDocError =<< "The @tactic attribute is not allowed here" 413checkTacticAttribute PiNotLam e = do 414 expectedType <- el primAgdaTerm --> el (primAgdaTCM <#> primLevelZero <@> primUnit) 415 checkExpr e expectedType 416 417ifPath :: Type -> TCM a -> TCM a -> TCM a 418ifPath ty fallback work = do 419 pv <- pathView ty 420 if isPathType pv then work else fallback 421 422checkPath :: A.TypedBinding -> A.Expr -> Type -> TCM Term 423checkPath b@(A.TBind _ _ (x':|[]) typ) body ty = do 424 let x = updateNamedArg (A.unBind . A.binderName) x' 425 info = getArgInfo x 426 PathType s path level typ lhs rhs <- pathView ty 427 interval <- primIntervalType 428 v <- addContext ([x], interval) $ 429 checkExpr body (El (raise 1 s) (raise 1 (unArg typ) `apply` [argN $ var 0])) 430 iZero <- primIZero 431 iOne <- primIOne 432 let lhs' = subst 0 iZero v 433 rhs' = subst 0 iOne v 434 let t = Lam info $ Abs (namedArgName x) v 435 let btyp i = El s (unArg typ `apply` [argN i]) 436 locallyTC eRange (const noRange) $ blockTerm ty $ traceCall (SetRange $ getRange body) $ do 437 equalTerm (btyp iZero) lhs' (unArg lhs) 438 equalTerm (btyp iOne) rhs' (unArg rhs) 439 return t 440checkPath b body ty = __IMPOSSIBLE__ 441--------------------------------------------------------------------------- 442-- * Lambda abstractions 443--------------------------------------------------------------------------- 444 445-- | Type check a lambda expression. 446-- "checkLambda bs e ty" means (\ bs -> e) : ty 447checkLambda :: Comparison -> A.TypedBinding -> A.Expr -> Type -> TCM Term 448checkLambda cmp (A.TLet _ lbs) body target = 449 checkLetBindings lbs (checkExpr body target) 450checkLambda cmp b@(A.TBind r tac xps0 typ) body target = do 451 reportSDoc "tc.term.lambda" 30 $ vcat 452 [ "checkLambda before insertion xs =" <+> prettyA xps0 453 ] 454 -- Andreas, 2020-03-25, issue #4481: since we have named lambdas now, 455 -- we need to insert skipped hidden arguments. 456 xps <- insertImplicitBindersT1 xps0 target 457 checkLambda' cmp (A.TBind r tac xps typ) xps typ body target 458 459checkLambda' 460 :: Comparison -- ^ @cmp@ 461 -> A.TypedBinding -- ^ @TBind _ _ xps typ@ 462 -> List1 (NamedArg Binder) -- ^ @xps@ 463 -> A.Expr -- ^ @typ@ 464 -> A.Expr -- ^ @body@ 465 -> Type -- ^ @target@ 466 -> TCM Term 467checkLambda' cmp b xps typ body target = do 468 reportSDoc "tc.term.lambda" 30 $ vcat 469 [ "checkLambda xs =" <+> prettyA xps 470 , "possiblePath =" <+> prettyTCM possiblePath 471 , "numbinds =" <+> prettyTCM numbinds 472 , "typ =" <+> prettyA (unScope typ) 473 ] 474 reportSDoc "tc.term.lambda" 60 $ vcat 475 [ "info =" <+> (text . show) info 476 ] 477 TelV tel btyp <- telViewUpTo numbinds target 478 if size tel < numbinds || numbinds /= 1 479 then (if possiblePath then trySeeingIfPath else dontUseTargetType) 480 else useTargetType tel btyp 481 482 where 483 484 xs = fmap (updateNamedArg (A.unBind . A.binderName)) xps 485 numbinds = length xps 486 isUnderscore = \case { A.Underscore{} -> True; _ -> False } 487 possiblePath = numbinds == 1 && isUnderscore (unScope typ) 488 && isRelevant info && visible info 489 info = getArgInfo $ List1.head xs 490 491 trySeeingIfPath = do 492 cubical <- optCubical <$> pragmaOptions 493 reportSLn "tc.term.lambda" 60 $ "trySeeingIfPath for " ++ show xps 494 let postpone' = if cubical then postpone else \ _ _ -> dontUseTargetType 495 ifBlocked target postpone' $ \ _ t -> do 496 ifPath t dontUseTargetType $ if cubical 497 then checkPath b body t 498 else genericError "Option --cubical needed to build a path with a lambda abstraction" 499 500 postpone blocker tgt = flip postponeTypeCheckingProblem blocker $ 501 CheckExpr cmp (A.Lam A.exprNoRange (A.DomainFull b) body) tgt 502 503 dontUseTargetType = do 504 -- Checking λ (xs : argsT) → body : target 505 verboseS "tc.term.lambda" 5 $ tick "lambda-no-target-type" 506 507 -- First check that argsT is a valid type 508 argsT <- workOnTypes $ isType_ typ 509 let tel = namedBindsToTel1 xs argsT 510 reportSDoc "tc.term.lambda" 30 $ "dontUseTargetType tel =" <+> pretty tel 511 512 -- Andreas, 2015-05-28 Issue 1523 513 -- If argsT is a SizeLt, it must be non-empty to avoid non-termination. 514 -- TODO: do we need to block checkExpr? 515 checkSizeLtSat $ unEl argsT 516 517 -- Jesper 2019-12-17, #4261: we need to postpone here if 518 -- checking of the record pattern fails; if we try to catch 519 -- higher up the metas created during checking of @argsT@ are 520 -- not available. 521 let postponeOnBlockedPattern m = m `catchIlltypedPatternBlockedOnMeta` \(err , x) -> do 522 reportSDoc "tc.term" 50 $ vcat $ 523 [ "checking record pattern stuck on meta: " <+> text (show x) ] 524 t1 <- addContext (xs, argsT) $ workOnTypes newTypeMeta_ 525 let e = A.Lam A.exprNoRange (A.DomainFull b) body 526 tgt' = telePi tel t1 527 w <- postponeTypeCheckingProblem (CheckExpr cmp e tgt') x 528 return (tgt' , w) 529 530 -- Now check body : ?t₁ 531 -- DONT USE tel for addContext, as it loses NameIds. 532 -- WRONG: v <- addContext tel $ checkExpr body t1 533 (target0 , w) <- postponeOnBlockedPattern $ 534 addContext (xs, argsT) $ addTypedPatterns xps $ do 535 t1 <- workOnTypes newTypeMeta_ 536 v <- checkExpr' cmp body t1 537 return (telePi tel t1 , teleLam tel v) 538 539 -- Do not coerce hidden lambdas 540 if notVisible info || any notVisible xs then do 541 pid <- newProblem_ $ leqType target0 target 542 blockTermOnProblem target w pid 543 else do 544 coerce cmp w target0 target 545 546 547 useTargetType tel@(ExtendTel dom (Abs y EmptyTel)) btyp = do 548 verboseS "tc.term.lambda" 5 $ tick "lambda-with-target-type" 549 reportSLn "tc.term.lambda" 30 $ "useTargetType y = " ++ y 550 551 let (x :| []) = xs 552 unless (sameHiding dom info) $ typeError $ WrongHidingInLambda target 553 when (isJust $ getNameOf x) $ 554 -- Andreas, 2020-03-25, issue #4481: check for correct name 555 unless (namedSame dom x) $ 556 setCurrentRange x $ typeError $ WrongHidingInLHS 557 -- Andreas, 2011-10-01 ignore relevance in lambda if not explicitly given 558 info <- lambdaModalityCheck dom info 559 -- Andreas, 2015-05-28 Issue 1523 560 -- Ensure we are not stepping under a possibly non-existing size. 561 -- TODO: do we need to block checkExpr? 562 let a = unDom dom 563 checkSizeLtSat $ unEl a 564 -- We only need to block the final term on the argument type 565 -- comparison. The body will be blocked if necessary. We still want to 566 -- compare the argument types first, so we spawn a new problem for that 567 -- check. 568 (pid, argT) <- newProblem $ isTypeEqualTo typ a 569 -- Andreas, Issue 630: take name from function type if lambda name is "_" 570 v <- lambdaAddContext (namedArg x) y (defaultArgDom info argT) $ 571 addTypedPatterns xps $ checkExpr' cmp body btyp 572 blockTermOnProblem target (Lam info $ Abs (namedArgName x) v) pid 573 574 useTargetType _ _ = __IMPOSSIBLE__ 575 576-- | Check that modality info in lambda is compatible with modality 577-- coming from the function type. 578-- If lambda has no user-given modality, copy that of function type. 579lambdaModalityCheck :: (LensAnnotation dom, LensModality dom) => dom -> ArgInfo -> TCM ArgInfo 580lambdaModalityCheck dom = lambdaAnnotationCheck (getAnnotation dom) <=< lambdaCohesionCheck m <=< lambdaQuantityCheck m <=< lambdaIrrelevanceCheck m 581 where m = getModality dom 582 583-- | Check that irrelevance info in lambda is compatible with irrelevance 584-- coming from the function type. 585-- If lambda has no user-given relevance, copy that of function type. 586lambdaIrrelevanceCheck :: LensRelevance dom => dom -> ArgInfo -> TCM ArgInfo 587lambdaIrrelevanceCheck dom info 588 -- Case: no specific user annotation: use relevance of function type 589 | getRelevance info == defaultRelevance = return $ setRelevance (getRelevance dom) info 590 -- Case: explicit user annotation is taken seriously 591 | otherwise = do 592 let rPi = getRelevance dom -- relevance of function type 593 let rLam = getRelevance info -- relevance of lambda 594 -- Andreas, 2017-01-24, issue #2429 595 -- we should report an error if we try to check a relevant function 596 -- against an irrelevant function type (subtyping violation) 597 unless (moreRelevant rPi rLam) $ do 598 -- @rLam == Relevant@ is impossible here 599 -- @rLam == Irrelevant@ is impossible here (least relevant) 600 -- this error can only happen if @rLam == NonStrict@ and @rPi == Irrelevant@ 601 unless (rLam == NonStrict) __IMPOSSIBLE__ -- separate tests for separate line nums 602 unless (rPi == Irrelevant) __IMPOSSIBLE__ 603 typeError WrongIrrelevanceInLambda 604 return info 605 606-- | Check that quantity info in lambda is compatible with quantity 607-- coming from the function type. 608-- If lambda has no user-given quantity, copy that of function type. 609lambdaQuantityCheck :: LensQuantity dom => dom -> ArgInfo -> TCM ArgInfo 610lambdaQuantityCheck dom info 611 -- Case: no specific user annotation: use quantity of function type 612 | noUserQuantity info = return $ setQuantity (getQuantity dom) info 613 -- Case: explicit user annotation is taken seriously 614 | otherwise = do 615 let qPi = getQuantity dom -- quantity of function type 616 let qLam = getQuantity info -- quantity of lambda 617 unless (qPi `sameQuantity` qLam) $ do 618 typeError WrongQuantityInLambda 619 return info 620 621lambdaAnnotationCheck :: LensAnnotation dom => dom -> ArgInfo -> TCM ArgInfo 622lambdaAnnotationCheck dom info 623 -- Case: no specific user annotation: use annotation of function type 624 | getAnnotation info == defaultAnnotation = return $ setAnnotation (getAnnotation dom) info 625 -- Case: explicit user annotation is taken seriously 626 | otherwise = do 627 let aPi = getAnnotation dom -- annotation of function type 628 let aLam = getAnnotation info -- annotation of lambda 629 unless (aPi == aLam) $ do 630 typeError $ GenericError $ "Wrong annotation in lambda" 631 return info 632 633-- | Check that cohesion info in lambda is compatible with cohesion 634-- coming from the function type. 635-- If lambda has no user-given cohesion, copy that of function type. 636lambdaCohesionCheck :: LensCohesion dom => dom -> ArgInfo -> TCM ArgInfo 637lambdaCohesionCheck dom info 638 -- Case: no specific user annotation: use cohesion of function type 639 | getCohesion info == defaultCohesion = return $ setCohesion (getCohesion dom) info 640 -- Case: explicit user annotation is taken seriously 641 | otherwise = do 642 let cPi = getCohesion dom -- cohesion of function type 643 let cLam = getCohesion info -- cohesion of lambda 644 unless (cPi `sameCohesion` cLam) $ do 645 -- if there is a cohesion annotation then 646 -- it better match the domain. 647 typeError WrongCohesionInLambda 648 return info 649 650-- Andreas, issue #630: take name from function type if lambda name is "_". 651lambdaAddContext :: Name -> ArgName -> Dom Type -> TCM a -> TCM a 652lambdaAddContext x y dom 653 | isNoName x = addContext (y, dom) -- Note: String instance 654 | otherwise = addContext (x, dom) -- Name instance of addContext 655 656-- | Checking a lambda whose domain type has already been checked. 657checkPostponedLambda :: Comparison -> Arg (List1 (WithHiding Name), Maybe Type) -> A.Expr -> Type -> TCM Term 658-- checkPostponedLambda cmp args@(Arg _ ([] , _ )) body target = do 659-- checkExpr' cmp body target 660checkPostponedLambda cmp args@(Arg info (WithHiding h x :| xs, mt)) body target = do 661 let postpone _ t = postponeTypeCheckingProblem_ $ CheckLambda cmp args body t 662 lamHiding = mappend h $ getHiding info 663 insertHiddenLambdas lamHiding target postpone $ \ t@(El _ (Pi dom b)) -> do 664 -- Andreas, 2011-10-01 ignore relevance in lambda if not explicitly given 665 info' <- setHiding lamHiding <$> lambdaModalityCheck dom info 666 -- We only need to block the final term on the argument type 667 -- comparison. The body will be blocked if necessary. We still want to 668 -- compare the argument types first, so we spawn a new problem for that 669 -- check. 670 mpid <- caseMaybe mt (return Nothing) $ \ ascribedType -> Just <$> do 671 newProblem_ $ leqType (unDom dom) ascribedType 672 -- We type-check the body with the ascribedType given by the user 673 -- to get better error messages. 674 -- Using the type dom from the usage context would be more precise, 675 -- though. 676 -- TODO: quantity 677 let dom' = setRelevance (getRelevance info') . setHiding lamHiding $ 678 maybe dom (dom $>) mt 679 v <- lambdaAddContext x (absName b) dom' $ 680 checkPostponedLambda0 cmp (Arg info (xs, mt)) body $ absBody b 681 let v' = Lam info' $ Abs (nameToArgName x) v 682 maybe (return v') (blockTermOnProblem t v') mpid 683 684checkPostponedLambda0 :: Comparison -> Arg ([WithHiding Name], Maybe Type) -> A.Expr -> Type -> TCM Term 685checkPostponedLambda0 cmp (Arg _ ([] , _ )) body target = 686 checkExpr' cmp body target 687checkPostponedLambda0 cmp (Arg info (x : xs, mt)) body target = 688 checkPostponedLambda cmp (Arg info (x :| xs, mt)) body target 689 690 691-- | Insert hidden lambda until the hiding info of the domain type 692-- matches the expected hiding info. 693-- Throws 'WrongHidingInLambda' 694insertHiddenLambdas 695 :: Hiding -- ^ Expected hiding. 696 -> Type -- ^ Expected to be a function type. 697 -> (Blocker -> Type -> TCM Term) -- ^ Continuation on blocked type. 698 -> (Type -> TCM Term) -- ^ Continuation when expected hiding found. 699 -- The continuation may assume that the @Type@ 700 -- is of the form @(El _ (Pi _ _))@. 701 -> TCM Term -- ^ Term with hidden lambda inserted. 702insertHiddenLambdas h target postpone ret = do 703 -- If the target type is blocked, we postpone, 704 -- because we do not know if a hidden lambda needs to be inserted. 705 ifBlocked target postpone $ \ _ t -> do 706 case unEl t of 707 708 Pi dom b -> do 709 let h' = getHiding dom 710 -- Found expected hiding: return function type. 711 if sameHiding h h' then ret t else do 712 -- Found a visible argument but expected a hidden one: 713 -- That's an error, as we cannot insert a visible lambda. 714 if visible h' then typeError $ WrongHidingInLambda target else do 715 -- Otherwise, we found a hidden argument that we can insert. 716 let x = absName b 717 Lam (setOrigin Inserted $ domInfo dom) . Abs x <$> do 718 addContext (x, dom) $ insertHiddenLambdas h (absBody b) postpone ret 719 720 _ -> typeError . GenericDocError =<< do 721 "Expected " <+> prettyTCM target <+> " to be a function type" 722 723-- | @checkAbsurdLambda i h e t@ checks absurd lambda against type @t@. 724-- Precondition: @e = AbsurdLam i h@ 725checkAbsurdLambda :: Comparison -> A.ExprInfo -> Hiding -> A.Expr -> Type -> TCM Term 726checkAbsurdLambda cmp i h e t = localTC (set eQuantity topQuantity) $ do 727 -- Andreas, 2019-10-01: check absurd lambdas in non-erased mode. 728 -- Otherwise, they are not usable in meta-solutions in the term world. 729 -- See test/Succeed/Issue3176.agda for an absurd lambda 730 -- created in types. 731 t <- instantiateFull t 732 ifBlocked t (\ blocker t' -> postponeTypeCheckingProblem (CheckExpr cmp e t') blocker) $ \ _ t' -> do 733 case unEl t' of 734 Pi dom@(Dom{domInfo = info', unDom = a}) b 735 | not (sameHiding h info') -> typeError $ WrongHidingInLambda t' 736 | otherwise -> blockTerm t' $ do 737 ensureEmptyType (getRange i) a 738 -- Add helper function 739 top <- currentModule 740 aux <- qualify top <$> freshName_ (getRange i, absurdLambdaName) 741 -- if we are in irrelevant / erased position, the helper function 742 -- is added as irrelevant / erased 743 mod <- asksTC getModality 744 reportSDoc "tc.term.absurd" 10 $ vcat 745 [ ("Adding absurd function" <+> prettyTCM mod) <> prettyTCM aux 746 , nest 2 $ "of type" <+> prettyTCM t' 747 ] 748 addConstant aux $ 749 (\ d -> (defaultDefn (setModality mod info') aux t' d) 750 { defPolarity = [Nonvariant] 751 , defArgOccurrences = [Unused] }) 752 $ emptyFunction 753 { funClauses = 754 [ Clause 755 { clauseLHSRange = getRange e 756 , clauseFullRange = getRange e 757 , clauseTel = telFromList [fmap (absurdPatternName,) dom] 758 , namedClausePats = [Arg info' $ Named (Just $ WithOrigin Inserted $ unranged $ absName b) $ absurdP 0] 759 , clauseBody = Nothing 760 , clauseType = Just $ setModality mod $ defaultArg $ absBody b 761 , clauseCatchall = True -- absurd clauses are safe as catch-alls 762 , clauseExact = Just False 763 , clauseRecursive = Just False 764 , clauseUnreachable = Just True -- absurd clauses are unreachable 765 , clauseEllipsis = NoEllipsis 766 } 767 ] 768 , funCompiled = Just $ Fail [Arg info' "()"] 769 , funSplitTree = Just $ SplittingDone 0 770 , funMutual = Just [] 771 , funTerminates = Just True 772 , funExtLam = Just $ ExtLamInfo top True empty 773 } 774 -- Andreas 2012-01-30: since aux is lifted to toplevel 775 -- it needs to be applied to the current telescope (issue 557) 776 Def aux . map Apply . teleArgs <$> getContextTelescope 777 _ -> typeError $ ShouldBePi t' 778 779-- | @checkExtendedLambda i di erased qname cs e t@ check pattern matching lambda. 780-- Precondition: @e = ExtendedLam i di erased qname cs@ 781checkExtendedLambda :: 782 Comparison -> A.ExprInfo -> A.DefInfo -> Erased -> QName -> 783 List1 A.Clause -> A.Expr -> Type -> TCM Term 784checkExtendedLambda cmp i di erased qname cs e t = do 785 mod <- asksTC getModality 786 if isErased erased && not (hasQuantity0 mod) then 787 genericError $ unwords 788 [ "Erased pattern-matching lambdas may only be used in erased" 789 , "contexts" 790 ] 791 else localTC (set eQuantity $ asQuantity erased) $ do 792 -- Andreas, 2016-06-16 issue #2045 793 -- Try to get rid of unsolved size metas before we 794 -- fix the type of the extended lambda auxiliary function 795 solveSizeConstraints DontDefaultToInfty 796 lamMod <- inFreshModuleIfFreeParams currentModule -- #2883: need a fresh module if refined params 797 t <- instantiateFull t 798 ifBlocked t (\ m t' -> postponeTypeCheckingProblem_ $ CheckExpr cmp e t') $ \ _ t -> do 799 j <- currentOrFreshMutualBlock 800 mod <- asksTC getModality 801 let info = setModality mod defaultArgInfo 802 803 reportSDoc "tc.term.exlam" 20 $ vcat 804 [ hsep 805 [ text $ show $ A.defAbstract di 806 , "extended lambda's implementation" 807 , doubleQuotes $ prettyTCM qname 808 , "has type:" 809 ] 810 , prettyTCM t -- <+> " where clauses: " <+> text (show cs) 811 ] 812 args <- getContextArgs 813 814 -- Andreas, Ulf, 2016-02-02: We want to postpone type checking an extended lambda 815 -- in case the lhs checker failed due to insufficient type info for the patterns. 816 -- Issues 480, 1159, 1811. 817 abstract (A.defAbstract di) $ do 818 -- Andreas, 2013-12-28: add extendedlambda as @Function@, not as @Axiom@; 819 -- otherwise, @addClause@ in @checkFunDef'@ fails (see issue 1009). 820 addConstant qname =<< do 821 useTerPragma $ 822 (defaultDefn info qname t emptyFunction) { defMutual = j } 823 checkFunDef' t info NotDelayed (Just $ ExtLamInfo lamMod False empty) Nothing di qname $ 824 List1.toList cs 825 whenNothingM (asksTC envMutualBlock) $ 826 -- Andrea 10-03-2018: Should other checks be performed here too? e.g. termination/positivity/.. 827 checkIApplyConfluence_ qname 828 return $ Def qname $ map Apply args 829 where 830 -- Concrete definitions cannot use information about abstract things. 831 abstract ConcreteDef = inConcreteMode 832 abstract AbstractDef = inAbstractMode 833 834-- | Run a computation. 835-- 836-- * If successful, that's it, we are done. 837-- 838-- * If @NotADatatype a@ or @CannotEliminateWithPattern p a@ 839-- is thrown and type @a@ is blocked on some meta @x@, 840-- reset any changes to the state and pass (the error and) @x@ to the handler. 841-- 842-- * If @SplitError (UnificationStuck c tel us vs _)@ is thrown and the unification 843-- problem @us =?= vs : tel@ is blocked on some meta @x@ pass @x@ to the handler. 844-- 845-- * If another error was thrown or the type @a@ is not blocked, reraise the error. 846-- 847-- Note that the returned meta might only exists in the state where the error was 848-- thrown, thus, be an invalid 'MetaId' in the current state. 849-- 850catchIlltypedPatternBlockedOnMeta :: TCM a -> ((TCErr, Blocker) -> TCM a) -> TCM a 851catchIlltypedPatternBlockedOnMeta m handle = do 852 853 -- Andreas, 2016-07-13, issue 2028. 854 -- Save the state to rollback the changes to the signature. 855 st <- getTC 856 857 m `catchError` \ err -> do 858 859 let reraise :: MonadError TCErr m => m a 860 reraise = throwError err 861 862 -- Get the blocker responsible for the type error. 863 -- If we do not find a blocker or the error should not be handled, 864 -- we reraise the error. 865 blocker <- maybe reraise return $ case err of 866 TypeError _ s cl -> case clValue cl of 867 SortOfSplitVarError b _ -> b 868 SplitError (UnificationStuck b c tel us vs _) -> b 869 SplitError (BlockedType b aClosure) -> Just b 870 CannotEliminateWithPattern b p a -> b 871 -- Andrea: TODO look for blocking meta in tClosure and its Sort. 872 -- SplitError (CannotCreateMissingClause _ _ _ tClosure) -> 873 _ -> Nothing 874 _ -> Nothing 875 876 reportSDoc "tc.postpone" 20 $ vcat $ 877 [ "checking definition blocked on: " <+> prettyTCM blocker ] 878 879 -- Note that we messed up the state a bit. We might want to unroll these state changes. 880 -- However, they are mostly harmless: 881 -- 1. We created a new mutual block id. 882 -- 2. We added a constant without definition. 883 -- In fact, they are not so harmless, see issue 2028! 884 -- Thus, reset the state! 885 putTC st 886 887 -- There might be metas in the blocker not known in the reset state, as they could have been 888 -- created somewhere on the way to the type error. 889 blocker <- (`onBlockingMetasM` blocker) $ \ x -> 890 lookupMeta' x >>= \ case 891 -- Case: we do not know the meta, so cannot unblock. 892 Nothing -> return neverUnblock 893 -- Case: we know the meta here. 894 -- Just m | InstV{} <- mvInstantiation m -> __IMPOSSIBLE__ -- It cannot be instantiated yet. 895 -- Andreas, 2018-11-23: I do not understand why @InstV@ is necessarily impossible. 896 -- The reasoning is probably that the state @st@ is more advanced that @s@ 897 -- in which @x@ was blocking, thus metas in @st@ should be more instantiated than 898 -- in @s@. But issue #3403 presents a counterexample, so let's play save and reraise. 899 -- Ulf, 2020-08-13: But treat this case as not blocked and reraise on both always and never. 900 -- Ulf, 2020-08-13: Previously we returned neverUnblock for frozen metas here, but this is in 901 -- fact not very helpful. Yes there is no hope of solving the problem, but throwing a hard 902 -- error means we rob the user of the tools needed to figure out why the meta has not been 903 -- solved. Better to leave the constraint. 904 Just m | InstV{} <- mvInstantiation m -> return alwaysUnblock 905 | otherwise -> return $ unblockOnMeta x 906 907 -- If it's not blocked or we can't ever unblock reraise the error. 908 if blocker `elem` [neverUnblock, alwaysUnblock] then reraise else handle (err, blocker) 909 910--------------------------------------------------------------------------- 911-- * Records 912--------------------------------------------------------------------------- 913 914-- | Picks up record field assignments from modules that export a definition 915-- that has the same name as the missing field. 916 917expandModuleAssigns 918 :: [Either A.Assign A.ModuleName] -- ^ Modules and field assignments. 919 -> [C.Name] -- ^ Names of fields of the record type. 920 -> TCM A.Assigns -- ^ Completed field assignments from modules. 921expandModuleAssigns mfs xs = do 922 let (fs , ms) = partitionEithers mfs 923 924 -- The fields of the record that have not been given by field assignments @fs@ 925 -- are looked up in the given modules @ms@. 926 fs' <- forM (xs List.\\ map (view nameFieldA) fs) $ \ f -> do 927 928 -- Get the possible assignments for field f from the modules. 929 pms <- forM ms $ \ m -> do 930 modScope <- getNamedScope m 931 let names :: ThingsInScope AbstractName 932 names = exportedNamesInScope modScope 933 return $ 934 case Map.lookup f names of 935 Just [n] -> Just (m, FieldAssignment f $ killRange $ A.nameToExpr n) 936 _ -> Nothing 937 938 -- If we have several matching assignments, that's an error. 939 case catMaybes pms of 940 [] -> return Nothing 941 [(_, fa)] -> return (Just fa) 942 mfas -> typeError . GenericDocError =<< do 943 vcat $ 944 "Ambiguity: the field" <+> prettyTCM f 945 <+> "appears in the following modules: " : map (prettyTCM . fst) mfas 946 return (fs ++ catMaybes fs') 947 948-- | @checkRecordExpression fs e t@ checks record construction against type @t@. 949-- Precondition @e = Rec _ fs@. 950checkRecordExpression 951 :: Comparison -- ^ How do we related the inferred type of the record expression 952 -- to the expected type? Subtype or equal type? 953 -> A.RecordAssigns -- ^ @mfs@: modules and field assignments. 954 -> A.Expr -- ^ Must be @A.Rec _ mfs@. 955 -> Type -- ^ Expected type of record expression. 956 -> TCM Term -- ^ Record value in internal syntax. 957checkRecordExpression cmp mfs e t = do 958 reportSDoc "tc.term.rec" 10 $ sep 959 [ "checking record expression" 960 , prettyA e 961 ] 962 ifBlocked t (\ _ t -> guessRecordType t) {-else-} $ \ _ t -> do 963 case unEl t of 964 -- Case: We know the type of the record already. 965 Def r es -> do 966 let ~(Just vs) = allApplyElims es 967 reportSDoc "tc.term.rec" 20 $ text $ " r = " ++ prettyShow r 968 969 reportSDoc "tc.term.rec" 30 $ " xs = " <> do 970 text =<< prettyShow . map unDom <$> getRecordFieldNames r 971 reportSDoc "tc.term.rec" 30 $ " ftel= " <> do 972 prettyTCM =<< getRecordFieldTypes r 973 reportSDoc "tc.term.rec" 30 $ " con = " <> do 974 text =<< prettyShow <$> getRecordConstructor r 975 976 def <- getRecordDef r 977 let -- Field names (C.Name) with ArgInfo from record type definition. 978 cxs = map argFromDom $ recordFieldNames def 979 -- Just field names. 980 xs = map unArg cxs 981 -- Record constructor. 982 con = killRange $ recConHead def 983 reportSDoc "tc.term.rec" 20 $ vcat 984 [ " xs = " <> return (P.pretty xs) 985 , " ftel= " <> prettyTCM (recTel def) 986 , " con = " <> return (P.pretty con) 987 ] 988 989 -- Andreas, 2018-09-06, issue #3122. 990 -- Associate the concrete record field names used in the record expression 991 -- to their counterpart in the record type definition. 992 disambiguateRecordFields (map _nameFieldA $ lefts mfs) (map unDom $ recFields def) 993 994 -- Compute the list of given fields, decorated with the ArgInfo from the record def. 995 -- Andreas, 2019-03-18, issue #3122, also pick up non-visible fields from the modules. 996 fs <- expandModuleAssigns mfs (map unArg cxs) 997 998 -- Compute a list of metas for the missing visible fields. 999 scope <- getScope 1000 let re = getRange e 1001 meta x = A.Underscore $ A.MetaInfo re scope Nothing (prettyShow x) 1002 -- In @es@ omitted explicit fields are replaced by underscores. 1003 -- Omitted implicit or instance fields 1004 -- are still left out and inserted later by checkArguments_. 1005 es <- insertMissingFieldsWarn r meta fs cxs 1006 1007 args <- checkArguments_ cmp ExpandLast re es (recTel def `apply` vs) >>= \case 1008 (elims, remainingTel) | null remainingTel 1009 , Just args <- allApplyElims elims -> return args 1010 _ -> __IMPOSSIBLE__ 1011 -- Don't need to block here! 1012 reportSDoc "tc.term.rec" 20 $ text $ "finished record expression" 1013 return $ Con con ConORec (map Apply args) 1014 _ -> typeError $ ShouldBeRecordType t 1015 1016 where 1017 -- Case: We don't know the type of the record. 1018 guessRecordType t = do 1019 let fields = [ x | Left (FieldAssignment x _) <- mfs ] 1020 rs <- findPossibleRecords fields 1021 reportSDoc "tc.term.rec" 30 $ "Possible records for" <+> prettyTCM t <+> "are" <?> pretty rs 1022 case rs of 1023 -- If there are no records with the right fields we might as well fail right away. 1024 [] -> case fields of 1025 [] -> genericError "There are no records in scope" 1026 [f] -> genericError $ "There is no known record with the field " ++ prettyShow f 1027 _ -> genericError $ "There is no known record with the fields " ++ unwords (map prettyShow fields) 1028 -- If there's only one record with the appropriate fields, go with that. 1029 [r] -> do 1030 -- #5198: Don't generate metas for parameters of the current module. In most cases they 1031 -- get solved, but not always. 1032 def <- instantiateDef =<< getConstInfo r 1033 ps <- freeVarsToApply r 1034 let rt = defType def 1035 reportSDoc "tc.term.rec" 30 $ "Type of unique record" <+> prettyTCM rt 1036 vs <- newArgsMeta rt 1037 target <- reduce $ piApply rt vs 1038 s <- case unEl target of 1039 Sort s -> return s 1040 v -> do 1041 reportSDoc "impossible" 10 $ vcat 1042 [ "The impossible happened when checking record expression against meta" 1043 , "Candidate record type r = " <+> prettyTCM r 1044 , "Type of r = " <+> prettyTCM rt 1045 , "Ends in (should be sort)= " <+> prettyTCM v 1046 , text $ " Raw = " ++ show v 1047 ] 1048 __IMPOSSIBLE__ 1049 let inferred = El s $ Def r $ map Apply (ps ++ vs) 1050 v <- checkExpr e inferred 1051 coerce cmp v inferred t 1052 -- Andreas 2012-04-21: OLD CODE, WRONG DIRECTION, I GUESS: 1053 -- blockTerm t $ v <$ leqType_ t inferred 1054 1055 -- If there are more than one possible record we postpone 1056 _:_:_ -> do 1057 reportSDoc "tc.term.expr.rec" 10 $ sep 1058 [ "Postponing type checking of" 1059 , nest 2 $ prettyA e <+> ":" <+> prettyTCM t 1060 ] 1061 postponeTypeCheckingProblem_ $ CheckExpr cmp e t 1062 1063-- | @checkRecordUpdate cmp ei recexpr fs e t@ 1064-- 1065-- Preconditions: @e = RecUpdate ei recexpr fs@ and @t@ is reduced. 1066-- 1067checkRecordUpdate 1068 :: Comparison -- ^ @cmp@ 1069 -> A.ExprInfo -- ^ @ei@ 1070 -> A.Expr -- ^ @recexpr@ 1071 -> A.Assigns -- ^ @fs@ 1072 -> A.Expr -- ^ @e = RecUpdate ei recexpr fs@ 1073 -> Type -- ^ Need not be reduced. 1074 -> TCM Term 1075checkRecordUpdate cmp ei recexpr fs eupd t = do 1076 ifBlocked t (\ _ _ -> tryInfer) $ {-else-} \ _ t' -> do 1077 caseMaybeM (isRecordType t') should $ \ (r, _pars, defn) -> do 1078 -- Bind the record value (before update) to a fresh @name@. 1079 v <- checkExpr' cmp recexpr t' 1080 name <- freshNoName $ getRange recexpr 1081 addLetBinding defaultArgInfo name v t' $ do 1082 1083 let projs = map argFromDom $ recFields defn 1084 1085 -- Andreas, 2018-09-06, issue #3122. 1086 -- Associate the concrete record field names used in the record expression 1087 -- to their counterpart in the record type definition. 1088 disambiguateRecordFields (map _nameFieldA fs) (map unArg projs) 1089 1090 -- Desugar record update expression into record expression. 1091 let fs' = map (\ (FieldAssignment x e) -> (x, Just e)) fs 1092 axs <- map argFromDom <$> getRecordFieldNames r 1093 es <- orderFieldsWarn r (const Nothing) axs fs' 1094 let es' = zipWith (replaceFields name ei) projs es 1095 let erec = A.Rec ei [ Left (FieldAssignment x e) | (Arg _ x, Just e) <- zip axs es' ] 1096 -- Call the type checker on the desugared syntax. 1097 checkExpr' cmp erec t 1098 where 1099 replaceFields :: Name -> A.ExprInfo -> Arg A.QName -> Maybe A.Expr -> Maybe A.Expr 1100 replaceFields name ei (Arg ai p) Nothing | visible ai = Just $ 1101 -- omitted visible fields remain unchanged: @{ ...; p = p name; ...}@ 1102 -- (hidden fields are supposed to be inferred) 1103 A.App 1104 (A.defaultAppInfo $ getRange ei) 1105 (A.Proj ProjSystem $ unambiguous p) 1106 (defaultNamedArg $ A.Var name) 1107 replaceFields _ _ _ me = me -- other fields get the user-written updates 1108 1109 tryInfer = do 1110 (_, trec) <- inferExpr recexpr 1111 ifBlocked trec (\ _ _ -> postpone) $ {-else-} \ _ _ -> do 1112 v <- checkExpr' cmp eupd trec 1113 coerce cmp v trec t 1114 1115 postpone = postponeTypeCheckingProblem_ $ CheckExpr cmp eupd t 1116 should = typeError $ ShouldBeRecordType t 1117 1118--------------------------------------------------------------------------- 1119-- * Literal 1120--------------------------------------------------------------------------- 1121 1122checkLiteral :: Literal -> Type -> TCM Term 1123checkLiteral lit t = do 1124 t' <- litType lit 1125 coerce CmpEq (Lit lit) t' t 1126 1127--------------------------------------------------------------------------- 1128-- * Terms 1129--------------------------------------------------------------------------- 1130 1131-- | Remove top layers of scope info of expression and set the scope accordingly 1132-- in the 'TCState'. 1133 1134scopedExpr :: A.Expr -> TCM A.Expr 1135scopedExpr (A.ScopedExpr scope e) = setScope scope >> scopedExpr e 1136scopedExpr e = return e 1137 1138-- | Type check an expression. 1139checkExpr :: A.Expr -> Type -> TCM Term 1140checkExpr = checkExpr' CmpLeq 1141 1142-- Andreas, 2019-10-13, issue #4125: 1143-- For the sake of readable types in interactive program construction, 1144-- avoid unnecessary unfoldings via 'reduce' in the type checker! 1145checkExpr' 1146 :: Comparison 1147 -> A.Expr 1148 -> Type -- ^ Unreduced! 1149 -> TCM Term 1150checkExpr' cmp e t = 1151 verboseBracket "tc.term.expr.top" 5 "checkExpr" $ 1152 reportResult "tc.term.expr.top" 15 (\ v -> vcat 1153 [ "checkExpr" <?> fsep [ prettyTCM e, ":", prettyTCM t ] 1154 , " returns" <?> prettyTCM v ]) $ 1155 traceCall (CheckExprCall cmp e t) $ localScope $ doExpandLast $ unfoldInlined =<< do 1156 reportSDoc "tc.term.expr.top" 15 $ 1157 "Checking" <+> sep 1158 [ fsep [ prettyTCM e, ":", prettyTCM t ] 1159 , nest 2 $ "at " <+> (text . prettyShow =<< getCurrentRange) 1160 ] 1161 reportSDoc "tc.term.expr.top.detailed" 80 $ 1162 "Checking" <+> fsep [ prettyTCM e, ":", text (show t) ] 1163 tReduced <- reduce t 1164 reportSDoc "tc.term.expr.top" 15 $ 1165 " --> " <+> prettyTCM tReduced 1166 1167 e <- scopedExpr e 1168 1169 irrelevantIfProp <- (runBlocked $ isPropM t) >>= \case 1170 Right True -> do 1171 let mod = defaultModality { modRelevance = Irrelevant } 1172 return $ fmap dontCare . applyModalityToContext mod 1173 _ -> return id 1174 1175 irrelevantIfProp $ tryInsertHiddenLambda e tReduced $ case e of 1176 1177 A.ScopedExpr scope e -> __IMPOSSIBLE__ -- setScope scope >> checkExpr e t 1178 1179 -- a meta variable without arguments: type check directly for efficiency 1180 A.QuestionMark i ii -> checkQuestionMark (newValueMeta' RunMetaOccursCheck) cmp t i ii 1181 A.Underscore i -> checkUnderscore cmp t i 1182 1183 A.WithApp _ e es -> typeError $ NotImplemented "type checking of with application" 1184 1185 e0@(A.App i q (Arg ai e)) 1186 | A.Quote _ <- unScope q, visible ai -> do 1187 x <- quotedName $ namedThing e 1188 ty <- qNameType 1189 coerce cmp (quoteName x) ty t 1190 1191 | A.QuoteTerm _ <- unScope q -> do 1192 (et, _) <- inferExpr (namedThing e) 1193 doQuoteTerm cmp et t 1194 1195 A.Quote{} -> genericError "quote must be applied to a defined name" 1196 A.QuoteTerm{} -> genericError "quoteTerm must be applied to a term" 1197 A.Unquote{} -> genericError "unquote must be applied to a term" 1198 1199 A.AbsurdLam i h -> checkAbsurdLambda cmp i h e t 1200 1201 A.ExtendedLam i di erased qname cs -> 1202 checkExtendedLambda cmp i di erased qname cs e t 1203 1204 A.Lam i (A.DomainFull b) e -> checkLambda cmp b e t 1205 1206 A.Lam i (A.DomainFree _ x) e0 1207 | isNothing (nameOf $ unArg x) && isNothing (A.binderPattern $ namedArg x) -> 1208 checkExpr' cmp (A.Lam i (domainFree (getArgInfo x) $ A.unBind <$> namedArg x) e0) t 1209 | otherwise -> typeError $ NotImplemented "named arguments in lambdas" 1210 1211 A.Lit _ lit -> checkLiteral lit t 1212 A.Let i ds e -> checkLetBindings ds $ checkExpr' cmp e t 1213 e@A.Pi{} -> do 1214 t' <- isType_ e 1215 let s = getSort t' 1216 v = unEl t' 1217 coerce cmp v (sort s) t 1218 1219 A.Generalized s e -> do 1220 (_, t') <- generalizeType s $ isType_ e 1221 --noFunctionsIntoSize t' t' 1222 let s = getSort t' 1223 v = unEl t' 1224 coerce cmp v (sort s) t 1225 1226 e@A.Fun{} -> do 1227 t' <- isType_ e 1228 let s = getSort t' 1229 v = unEl t' 1230 coerce cmp v (sort s) t 1231 1232 A.Rec _ fs -> checkRecordExpression cmp fs e t 1233 1234 A.RecUpdate ei recexpr fs -> checkRecordUpdate cmp ei recexpr fs e t 1235 1236 A.DontCare e -> -- resurrect vars 1237 ifM ((Irrelevant ==) <$> asksTC getRelevance) 1238 (dontCare <$> do applyRelevanceToContext Irrelevant $ checkExpr' cmp e t) 1239 (internalError "DontCare may only appear in irrelevant contexts") 1240 1241 A.ETel _ -> __IMPOSSIBLE__ 1242 1243 A.Dot{} -> genericError "Invalid dotted expression" 1244 1245 -- Application 1246 _ | Application hd args <- appView e -> checkApplication cmp hd args e t 1247 1248 `catchIlltypedPatternBlockedOnMeta` \ (err, x) -> do 1249 -- We could not check the term because the type of some pattern is blocked. 1250 -- It has to be blocked on some meta, so we can postpone, 1251 -- being sure it will be retried when a meta is solved 1252 -- (which might be the blocking meta in which case we actually make progress). 1253 reportSDoc "tc.term" 50 $ vcat $ 1254 [ "checking pattern got stuck on meta: " <+> pretty x ] 1255 postponeTypeCheckingProblem (CheckExpr cmp e t) x 1256 1257 where 1258 -- Call checkExpr with an hidden lambda inserted if appropriate, 1259 -- else fallback. 1260 tryInsertHiddenLambda 1261 :: A.Expr 1262 -> Type -- Reduced. 1263 -> TCM Term 1264 -> TCM Term 1265 tryInsertHiddenLambda e tReduced fallback 1266 -- Insert hidden lambda if all of the following conditions are met: 1267 -- type is a hidden function type, {x : A} -> B or {{x : A}} -> B 1268 -- expression is not a lambda with the appropriate hiding yet 1269 | Pi (Dom{domInfo = info, unDom = a}) b <- unEl tReduced 1270 , let h = getHiding info 1271 , notVisible h 1272 -- expression is not a matching hidden lambda or question mark 1273 , not (hiddenLambdaOrHole h e) 1274 = do 1275 let proceed = doInsert (setOrigin Inserted info) $ absName b 1276 expandHidden <- asksTC envExpandLast 1277 -- If we skip the lambda insertion for an introduction, 1278 -- we will hit a dead end, so proceed no matter what. 1279 if definitelyIntroduction then proceed else 1280 -- #3019 and #4170: don't insert implicit lambdas in arguments to existing metas 1281 if expandHidden == ReallyDontExpandLast then fallback else do 1282 -- Andreas, 2017-01-19, issue #2412: 1283 -- We do not want to insert a hidden lambda if A is 1284 -- possibly empty type of sizes, as this will produce an error. 1285 reduce a >>= isSizeType >>= \case 1286 Just (BoundedLt u) -> ifBlocked u (\ _ _ -> fallback) $ \ _ v -> do 1287 ifM (checkSizeNeverZero v) proceed fallback 1288 `catchError` \_ -> fallback 1289 _ -> proceed 1290 1291 | otherwise = fallback 1292 1293 where 1294 re = getRange e 1295 rx = caseMaybe (rStart re) noRange $ \ pos -> posToRange pos pos 1296 1297 doInsert info y = do 1298 x <- C.setNotInScope <$> freshName rx y 1299 reportSLn "tc.term.expr.impl" 15 $ "Inserting implicit lambda" 1300 checkExpr' cmp (A.Lam (A.ExprRange re) (domainFree info $ A.mkBinder x) e) tReduced 1301 1302 hiddenLambdaOrHole h = \case 1303 A.AbsurdLam _ h' -> sameHiding h h' 1304 A.ExtendedLam _ _ _ _ cls -> any hiddenLHS cls 1305 A.Lam _ bind _ -> sameHiding h bind 1306 A.QuestionMark{} -> True 1307 _ -> False 1308 1309 hiddenLHS (A.Clause (A.LHS _ (A.LHSHead _ (a : _))) _ _ _ _) = notVisible a 1310 hiddenLHS _ = False 1311 1312 -- Things with are definitely introductions, 1313 -- thus, cannot be of hidden Pi-type, unless they are hidden lambdas. 1314 definitelyIntroduction = case e of 1315 A.Lam{} -> True 1316 A.AbsurdLam{} -> True 1317 A.Lit{} -> True 1318 A.Pi{} -> True 1319 A.Fun{} -> True 1320 A.Rec{} -> True 1321 A.RecUpdate{} -> True 1322 A.ScopedExpr{} -> __IMPOSSIBLE__ 1323 A.ETel{} -> __IMPOSSIBLE__ 1324 _ -> False 1325 1326--------------------------------------------------------------------------- 1327-- * Reflection 1328--------------------------------------------------------------------------- 1329 1330doQuoteTerm :: Comparison -> Term -> Type -> TCM Term 1331doQuoteTerm cmp et t = do 1332 et' <- etaContract =<< instantiateFull et 1333 case allMetasList et' of 1334 [] -> do 1335 q <- quoteTerm et' 1336 ty <- el primAgdaTerm 1337 coerce cmp q ty t 1338 metas -> postponeTypeCheckingProblem (DoQuoteTerm cmp et t) $ unblockOnAllMetas $ Set.fromList metas 1339 1340-- | Unquote a TCM computation in a given hole. 1341unquoteM :: A.Expr -> Term -> Type -> TCM () 1342unquoteM tacA hole holeType = do 1343 tac <- checkExpr tacA =<< (el primAgdaTerm --> el (primAgdaTCM <#> primLevelZero <@> primUnit)) 1344 inFreshModuleIfFreeParams $ unquoteTactic tac hole holeType 1345 1346-- | Run a tactic `tac : Term → TC ⊤` in a hole (second argument) of the type 1347-- given by the third argument. Runs the continuation if successful. 1348unquoteTactic :: Term -> Term -> Type -> TCM () 1349unquoteTactic tac hole goal = do 1350 reportSDoc "tc.term.tactic" 40 $ sep 1351 [ "Running tactic" <+> prettyTCM tac 1352 , nest 2 $ "on" <+> prettyTCM hole <+> ":" <+> prettyTCM goal ] 1353 ok <- runUnquoteM $ unquoteTCM tac hole 1354 case ok of 1355 Left (BlockedOnMeta oldState blocker) -> do 1356 putTC oldState 1357 let stripFreshMeta x = maybe neverUnblock (const $ unblockOnMeta x) <$> lookupMeta' x 1358 blocker' <- onBlockingMetasM stripFreshMeta blocker 1359 r <- case Set.toList $ allBlockingMetas blocker' of 1360 x : _ -> getRange <$> lookupMeta' x 1361 [] -> return noRange 1362 setCurrentRange r $ 1363 addConstraint blocker' (UnquoteTactic tac hole goal) 1364 Left err -> typeError $ UnquoteFailed err 1365 Right _ -> return () 1366 1367--------------------------------------------------------------------------- 1368-- * Meta variables 1369--------------------------------------------------------------------------- 1370 1371-- | Check an interaction point without arguments. 1372checkQuestionMark 1373 :: (Comparison -> Type -> TCM (MetaId, Term)) 1374 -> Comparison 1375 -> Type -- ^ Not reduced! 1376 -> A.MetaInfo 1377 -> InteractionId 1378 -> TCM Term 1379checkQuestionMark new cmp t0 i ii = do 1380 reportSDoc "tc.interaction" 20 $ sep 1381 [ "Found interaction point" 1382 , text . show =<< asksTC (^. lensIsAbstract) 1383 , pretty ii 1384 , ":" 1385 , prettyTCM t0 1386 ] 1387 reportSDoc "tc.interaction" 60 $ sep 1388 [ "Raw:" 1389 , text (show t0) 1390 ] 1391 checkMeta (newQuestionMark' new ii) cmp t0 i -- Andreas, 2013-05-22 use unreduced type t0! 1392 1393-- | Check an underscore without arguments. 1394checkUnderscore :: Comparison -> Type -> A.MetaInfo -> TCM Term 1395checkUnderscore = checkMeta (newValueMeta RunMetaOccursCheck) 1396 1397-- | Type check a meta variable. 1398checkMeta :: (Comparison -> Type -> TCM (MetaId, Term)) -> Comparison -> Type -> A.MetaInfo -> TCM Term 1399checkMeta newMeta cmp t i = fst <$> checkOrInferMeta newMeta (Just (cmp , t)) i 1400 1401-- | Infer the type of a meta variable. 1402-- If it is a new one, we create a new meta for its type. 1403inferMeta :: (Comparison -> Type -> TCM (MetaId, Term)) -> A.MetaInfo -> TCM (Elims -> Term, Type) 1404inferMeta newMeta i = mapFst applyE <$> checkOrInferMeta newMeta Nothing i 1405 1406-- | Type check a meta variable. 1407-- If its type is not given, we return its type, or a fresh one, if it is a new meta. 1408-- If its type is given, we check that the meta has this type, and we return the same 1409-- type. 1410checkOrInferMeta 1411 :: (Comparison -> Type -> TCM (MetaId, Term)) 1412 -> Maybe (Comparison , Type) 1413 -> A.MetaInfo 1414 -> TCM (Term, Type) 1415checkOrInferMeta newMeta mt i = do 1416 case A.metaNumber i of 1417 Nothing -> do 1418 setScope (A.metaScope i) 1419 (cmp , t) <- maybe ((CmpEq,) <$> workOnTypes newTypeMeta_) return mt 1420 (x, v) <- newMeta cmp t 1421 setMetaNameSuggestion x (A.metaNameSuggestion i) 1422 return (v, t) 1423 -- Rechecking an existing metavariable 1424 Just x -> do 1425 let v = MetaV x [] 1426 reportSDoc "tc.meta.check" 20 $ 1427 "checking existing meta " <+> prettyTCM v 1428 t' <- metaType x 1429 reportSDoc "tc.meta.check" 20 $ 1430 nest 2 $ "of type " <+> prettyTCM t' 1431 case mt of 1432 Nothing -> return (v, t') 1433 Just (cmp , t) -> (,t) <$> coerce cmp v t' t 1434 1435-- | Turn a domain-free binding (e.g. lambda) into a domain-full one, 1436-- by inserting an underscore for the missing type. 1437domainFree :: ArgInfo -> A.Binder' A.Name -> A.LamBinding 1438domainFree info x = 1439 A.DomainFull $ A.mkTBind r (singleton $ unnamedArg info $ fmap A.mkBindName x) 1440 $ A.Underscore underscoreInfo 1441 where 1442 r = getRange x 1443 underscoreInfo = A.MetaInfo 1444 { A.metaRange = r 1445 , A.metaScope = emptyScopeInfo 1446 , A.metaNumber = Nothing 1447 , A.metaNameSuggestion = prettyShow $ A.nameConcrete $ A.binderName x 1448 } 1449 1450 1451-- | Check arguments whose value we already know. 1452-- 1453-- This function can be used to check user-supplied parameters 1454-- we have already computed by inference. 1455-- 1456-- Precondition: The type @t@ of the head has enough domains. 1457 1458checkKnownArguments 1459 :: [NamedArg A.Expr] -- ^ User-supplied arguments (hidden ones may be missing). 1460 -> Args -- ^ Inferred arguments (including hidden ones). 1461 -> Type -- ^ Type of the head (must be Pi-type with enough domains). 1462 -> TCM (Args, Type) -- ^ Remaining inferred arguments, remaining type. 1463checkKnownArguments [] vs t = return (vs, t) 1464checkKnownArguments (arg : args) vs t = do 1465 (vs', t') <- traceCall (SetRange $ getRange arg) $ checkKnownArgument arg vs t 1466 checkKnownArguments args vs' t' 1467 1468-- | Check an argument whose value we already know. 1469 1470checkKnownArgument 1471 :: NamedArg A.Expr -- ^ User-supplied argument. 1472 -> Args -- ^ Inferred arguments (including hidden ones). 1473 -> Type -- ^ Type of the head (must be Pi-type with enough domains). 1474 -> TCM (Args, Type) -- ^ Remaining inferred arguments, remaining type. 1475checkKnownArgument arg [] _ = genericDocError =<< do 1476 "Invalid projection parameter " <+> prettyA arg 1477-- Andreas, 2019-07-22, while #3353: we should use domName, not absName !! 1478-- WAS: 1479-- checkKnownArgument arg@(Arg info e) (Arg _infov v : vs) t = do 1480-- (dom@Dom{domInfo = info',unDom = a}, b) <- mustBePi t 1481-- -- Skip the arguments from vs that do not correspond to e 1482-- if not (sameHiding info info' 1483-- && (visible info || maybe True (absName b ==) (bareNameOf e))) 1484checkKnownArgument arg (Arg _ v : vs) t = do 1485 -- Skip the arguments from vs that do not correspond to e 1486 (dom@Dom{ unDom = a }, b) <- mustBePi t 1487 if not $ fromMaybe __IMPOSSIBLE__ $ fittingNamedArg arg dom 1488 -- Continue with the next one 1489 then checkKnownArgument arg vs (b `absApp` v) 1490 -- Found the right argument 1491 else do 1492 u <- checkNamedArg arg a 1493 equalTerm a u v 1494 return (vs, b `absApp` v) 1495 1496-- | Check a single argument. 1497 1498checkNamedArg :: NamedArg A.Expr -> Type -> TCM Term 1499checkNamedArg arg@(Arg info e0) t0 = do 1500 let e = namedThing e0 1501 let x = bareNameWithDefault "" e0 1502 traceCall (CheckExprCall CmpLeq e t0) $ do 1503 reportSDoc "tc.term.args.named" 15 $ do 1504 "Checking named arg" <+> sep 1505 [ fsep [ prettyTCM arg, ":", prettyTCM t0 ] 1506 ] 1507 reportSLn "tc.term.args.named" 75 $ " arg = " ++ show (deepUnscope arg) 1508 -- Ulf, 2017-03-24: (#2172) Always treat explicit _ and ? as implicit 1509 -- argument (i.e. solve with unification). 1510 let checkU = checkMeta (newMetaArg (setHiding Hidden info) x) CmpLeq t0 1511 let checkQ = checkQuestionMark (newInteractionMetaArg (setHiding Hidden info) x) CmpLeq t0 1512 if not $ isHole e then checkExpr e t0 else localScope $ do 1513 -- Note: we need localScope here, 1514 -- as scopedExpr manipulates the scope in the state. 1515 -- However, we may not pull localScope over checkExpr! 1516 -- This is why we first test for isHole, and only do 1517 -- scope manipulations if we actually handle the checking 1518 -- of e here (and not pass it to checkExpr). 1519 scopedExpr e >>= \case 1520 A.Underscore i -> checkU i 1521 A.QuestionMark i ii -> checkQ i ii 1522 _ -> __IMPOSSIBLE__ 1523 where 1524 isHole A.Underscore{} = True 1525 isHole A.QuestionMark{} = True 1526 isHole (A.ScopedExpr _ e) = isHole e 1527 isHole _ = False 1528 1529-- | Infer the type of an expression. Implemented by checking against a meta 1530-- variable. Except for neutrals, for them a polymorphic type is inferred. 1531inferExpr :: A.Expr -> TCM (Term, Type) 1532-- inferExpr e = inferOrCheck e Nothing 1533inferExpr = inferExpr' DontExpandLast 1534 1535inferExpr' :: ExpandHidden -> A.Expr -> TCM (Term, Type) 1536inferExpr' exh e = traceCall (InferExpr e) $ do 1537 let Application hd args = appView e 1538 reportSDoc "tc.infer" 30 $ vcat 1539 [ "inferExpr': appView of " <+> prettyA e 1540 , " hd = " <+> prettyA hd 1541 , " args = " <+> prettyAs args 1542 ] 1543 reportSDoc "tc.infer" 60 $ vcat 1544 [ text $ " hd (raw) = " ++ show hd 1545 ] 1546 inferApplication exh hd args e 1547 1548defOrVar :: A.Expr -> Bool 1549defOrVar A.Var{} = True 1550defOrVar A.Def'{} = True 1551defOrVar A.Proj{} = True 1552defOrVar (A.ScopedExpr _ e) = defOrVar e 1553defOrVar _ = False 1554 1555-- | Used to check aliases @f = e@. 1556-- Switches off 'ExpandLast' for the checking of top-level application. 1557checkDontExpandLast :: Comparison -> A.Expr -> Type -> TCM Term 1558checkDontExpandLast cmp e t = case e of 1559 _ | Application hd args <- appView e, defOrVar hd -> 1560 traceCall (CheckExprCall cmp e t) $ localScope $ dontExpandLast $ do 1561 checkApplication cmp hd args e t 1562 _ -> checkExpr' cmp e t -- note that checkExpr always sets ExpandLast 1563 1564-- | Check whether a de Bruijn index is bound by a module telescope. 1565isModuleFreeVar :: Int -> TCM Bool 1566isModuleFreeVar i = do 1567 params <- moduleParamsToApply =<< currentModule 1568 return $ any ((== Var i []) . unArg) params 1569 1570-- | Infer the type of an expression, and if it is of the form 1571-- @{tel} -> D vs@ for some datatype @D@ then insert the hidden 1572-- arguments. Otherwise, leave the type polymorphic. 1573inferExprForWith :: Arg A.Expr -> TCM (Term, Type) 1574inferExprForWith (Arg info e) = 1575 applyRelevanceToContext (getRelevance info) $ do 1576 reportSDoc "tc.with.infer" 20 $ "inferExprforWith " <+> prettyTCM e 1577 reportSLn "tc.with.infer" 80 $ "inferExprforWith " ++ show (deepUnscope e) 1578 traceCall (InferExpr e) $ do 1579 -- With wants type and term fully instantiated! 1580 (v, t) <- instantiateFull =<< inferExpr e 1581 v0 <- reduce v 1582 -- Andreas 2014-11-06, issue 1342. 1583 -- Check that we do not `with` on a module parameter! 1584 case v0 of 1585 Var i [] -> whenM (isModuleFreeVar i) $ do 1586 reportSDoc "tc.with.infer" 80 $ vcat 1587 [ text $ "with expression is variable " ++ show i 1588 , "current modules = " <+> do text . show =<< currentModule 1589 , "current module free vars = " <+> do text . show =<< getCurrentModuleFreeVars 1590 , "context size = " <+> do text . show =<< getContextSize 1591 , "current context = " <+> do prettyTCM =<< getContextTelescope 1592 ] 1593 typeError $ WithOnFreeVariable e v0 1594 _ -> return () 1595 -- Possibly insert hidden arguments. 1596 TelV tel t0 <- telViewUpTo' (-1) (not . visible) t 1597 case unEl t0 of 1598 Def d vs -> do 1599 res <- isDataOrRecordType d 1600 case res of 1601 Nothing -> return (v, t) 1602 Just{} -> do 1603 (args, t1) <- implicitArgs (-1) notVisible t 1604 return (v `apply` args, t1) 1605 _ -> return (v, t) 1606 1607--------------------------------------------------------------------------- 1608-- * Let bindings 1609--------------------------------------------------------------------------- 1610 1611checkLetBindings :: Foldable t => t A.LetBinding -> TCM a -> TCM a 1612checkLetBindings = foldr ((.) . checkLetBinding) id 1613 1614checkLetBinding :: A.LetBinding -> TCM a -> TCM a 1615 1616checkLetBinding b@(A.LetBind i info x t e) ret = 1617 traceCall (CheckLetBinding b) $ do 1618 -- #4131: Only DontExpandLast if no user written type signature 1619 let check | getOrigin info == Inserted = checkDontExpandLast 1620 | otherwise = checkExpr' 1621 t <- isType_ t 1622 v <- applyModalityToContext info $ check CmpLeq e t 1623 addLetBinding info (A.unBind x) v t ret 1624 1625checkLetBinding b@(A.LetPatBind i p e) ret = 1626 traceCall (CheckLetBinding b) $ do 1627 p <- expandPatternSynonyms p 1628 (v, t) <- inferExpr' ExpandLast e 1629 let -- construct a type t -> dummy for use in checkLeftHandSide 1630 t0 = El (getSort t) $ Pi (defaultDom t) (NoAbs underscore __DUMMY_TYPE__) 1631 p0 = Arg defaultArgInfo (Named Nothing p) 1632 reportSDoc "tc.term.let.pattern" 10 $ vcat 1633 [ "let-binding pattern p at type t" 1634 , nest 2 $ vcat 1635 [ "p (A) =" <+> prettyA p 1636 , "t =" <+> prettyTCM t 1637 , "cxtRel=" <+> do pretty =<< asksTC getRelevance 1638 , "cxtQnt=" <+> do pretty =<< asksTC getQuantity 1639 ] 1640 ] 1641 fvs <- getContextSize 1642 checkLeftHandSide (CheckPattern p EmptyTel t) Nothing [p0] t0 Nothing [] $ \ (LHSResult _ delta0 ps _ _t _ asb _) -> bindAsPatterns asb $ do 1643 -- After dropping the free variable patterns there should be a single pattern left. 1644 let p = case drop fvs ps of [p] -> namedArg p; _ -> __IMPOSSIBLE__ 1645 -- Also strip the context variables from the telescope 1646 delta = telFromList $ drop fvs $ telToList delta0 1647 reportSDoc "tc.term.let.pattern" 20 $ nest 2 $ vcat 1648 [ "p (I) =" <+> prettyTCM p 1649 , "delta =" <+> prettyTCM delta 1650 , "cxtRel=" <+> do pretty =<< asksTC getRelevance 1651 , "cxtQnt=" <+> do pretty =<< asksTC getQuantity 1652 ] 1653 reportSDoc "tc.term.let.pattern" 80 $ nest 2 $ vcat 1654 [ "p (I) =" <+> (text . show) p 1655 ] 1656 -- We translate it into a list of projections. 1657 fs <- recordPatternToProjections p 1658 -- We remove the bindings for the pattern variables from the context. 1659 cxt0 <- getContext 1660 let (binds, cxt) = splitAt (size delta) cxt0 1661 toDrop = length binds 1662 1663 -- We create a substitution for the let-bound variables 1664 -- (unfortunately, we cannot refer to x in internal syntax 1665 -- so we have to copy v). 1666 sigma = map ($ v) fs 1667 -- We apply the types of the let bound-variables to this substitution. 1668 -- The 0th variable in a context is the last one, so we reverse. 1669 -- Further, we need to lower all other de Bruijn indices by 1670 -- the size of delta, so we append the identity substitution. 1671 sub = parallelS (reverse sigma) 1672 1673 updateContext sub (drop toDrop) $ do 1674 reportSDoc "tc.term.let.pattern" 20 $ nest 2 $ vcat 1675 [ "delta =" <+> prettyTCM delta 1676 , "binds =" <+> prettyTCM binds 1677 ] 1678 let fdelta = flattenTel delta 1679 reportSDoc "tc.term.let.pattern" 20 $ nest 2 $ vcat 1680 [ "fdelta =" <+> addContext delta (prettyTCM fdelta) 1681 ] 1682 let tsl = applySubst sub fdelta 1683 -- We get a list of types 1684 let ts = map unDom tsl 1685 -- and relevances. 1686 let infos = map domInfo tsl 1687 -- We get list of names of the let-bound vars from the context. 1688 let xs = map (fst . unDom) (reverse binds) 1689 -- We add all the bindings to the context. 1690 foldr (uncurry4 addLetBinding) ret $ List.zip4 infos xs sigma ts 1691 1692checkLetBinding (A.LetApply i x modapp copyInfo _adir) ret = do 1693 -- Any variables in the context that doesn't belong to the current 1694 -- module should go with the new module. 1695 -- Example: @f x y = let open M t in u@. 1696 -- There are 2 @new@ variables, @x@ and @y@, going into the anonynous module 1697 -- @module _ (x : _) (y : _) = M t@. 1698 fv <- getCurrentModuleFreeVars 1699 n <- getContextSize 1700 let new = n - fv 1701 reportSDoc "tc.term.let.apply" 10 $ "Applying" <+> pretty x <+> prettyA modapp <?> ("with" <+> pshow new <+> "free variables") 1702 reportSDoc "tc.term.let.apply" 20 $ vcat 1703 [ "context =" <+> (prettyTCM =<< getContextTelescope) 1704 , "module =" <+> (prettyTCM =<< currentModule) 1705 , "fv =" <+> text (show fv) 1706 ] 1707 checkSectionApplication i x modapp copyInfo 1708 withAnonymousModule x new ret 1709-- LetOpen and LetDeclaredVariable are only used for highlighting. 1710checkLetBinding A.LetOpen{} ret = ret 1711checkLetBinding (A.LetDeclaredVariable _) ret = ret 1712