Should n be size tel?

[nad]

Consider what happens if the size of tel is less than n in the following code (I have verified that this can happen, see for instance test/Succeed/Issue723.agda):

agda/src/full/Agda/TypeChecking/Rules/Application.hs

Lines 653 to 696 in 27ea7f2

	-- Check the target type if we can get away with it.
	chk' <- lift $
	case (chk, mt1) of
	(NotCheckedTarget, Just t1) | all visible args0 -> do
	let n = length args0
	TelV tel tgt <- telViewUpTo n t0'
	let dep = any (< n) $ IntSet.toList $ freeVars tgt
	vis = all visible (telToList tel)
	isRigid t | PathType{} <- viewPath t = return False -- Path is not rigid!
	isRigid (El _ (Pi dom _)) = return $ visible dom
	isRigid (El _ (Def d _)) = getConstInfo d <&> theDef <&> \ case
	Axiom{} -> True
	DataOrRecSig{} -> True
	AbstractDefn{} -> True
	Function{funClauses = cs} -> null cs
	Datatype{} -> True
	Record{} -> True
	Constructor{} -> __IMPOSSIBLE__
	GeneralizableVar{} -> __IMPOSSIBLE__
	Primitive{} -> False
	PrimitiveSort{} -> False
	isRigid _ = return False
	rigid <- isRigid tgt
	-- Andreas, 2019-03-28, issue #3248:
	-- If the target type is SIZELT, we need coerce, leqType is insufficient.
	-- For example, we have i : Size <= (Size< ↑ i), but not Size <= (Size< ↑ i).
	isSizeLt <- reduce t1 >>= isSizeType <&> \case
	Just (BoundedLt _) -> True
	_ -> False
	if | dep -> return chk -- must be non-dependent
	| not rigid -> return chk -- with a rigid target
	| not vis -> return chk -- and only visible arguments
	| isSizeLt -> return chk -- Issue #3248, not Size<
	| otherwise -> do
	let tgt1 = applySubst (strengthenS impossible $ size tel) tgt
	reportSDoc "tc.term.args.target" 30 $ vcat
	[ "Checking target types first"
	, nest 2 $ "inferred =" <+> prettyTCM tgt1
	, nest 2 $ "expected =" <+> prettyTCM t1 ]
	traceCall (CheckTargetType (fuseRange r args0) tgt1 t1) $
	CheckedTarget <$> ifNoConstraints_ (compareType cmp tgt1 t1)
	(return Nothing) (return . Just)
	_ -> return chk

If the size of the telescope is less than n, doesn't it make sense to use size tel instead of n in dep?

[UlfNorell]

Yes, that looks like it should be size tel instead of n.

[nad]

The test suite does not complain.

[andreasabel]

(This issue does not have a reproducer, so we don't list it in the changelog.)