[ fix #6867 ] Only consider arguments with @0 for forcing if --erasure is on

[jespercockx]

This implements my suggested fix for #6867: when --erasure is on, we only consider arguments to be forced if they have a @0 annotation. This is because forced arguments need to be reconstructible from the type, but the type lives at modality @0.

[andreasabel]

@jespercockx : The CI failure for the user manual could point to a real problem, try make user-manual-html locally.

[jespercockx]

Consider me slightly annoyed by the fact that a missing newline was causing Sphinx to reject the file. Also, when I first pushed I ran user-manual-test but not user-manual-html, aren't the tests supposed to catch these kind of errors?

[jespercockx]

This time I don't think it's my fault anymore:

tlmgr: setting default package repository to http://ftp.math.utah.edu/pub/tex/historic/systems/texlive/2017/tlnet-final
/home/runner/texlive/bin/x86_64-linux/tlmgr: open tlpdb(http://ftp.math.utah.edu/pub/tex/historic/systems/texlive/2017/tlnet-final/tlpkg/texlive.tlpdb) failed: Inappropriate ioctl for device at /home/runner/texlive/tlpkg/TeXLive/TLPDB.pm line 360.

and

Warning: No latest package revision found for shelltestrunner, dependency callstack:
shelltest --color --precise test/succeed.test
make[1]: Leaving directory '/home/runner/work/agda/agda/src/size-solver'
make[1]: shelltest: No such file or directory
make[1]: *** [Makefile:25: test] Error 127
make: *** [Makefile:665: size-solver-test] Error 2

[andreasabel]

This time I don't think it's my fault anymore:

I am at it, see

• CI user_manual.yml using historic texlive 2017 fails #6878.

[andreasabel]

@jespercockx wrote:

I ran user-manual-test but not user-manual-html, aren't the tests supposed to catch these kind of errors?

The former only checks the Agda content of the user manual, only the latter builds the docs.

[jespercockx]

Since 2.6.4 has been released, I will merge this soon unless there's any complaints.

[nad]

With your change in place the termination checker rejected some of my code. How does forcing interact with termination checking?

Here is a test case:

{-# OPTIONS --erased-cubical --erasure #-}

open import Agda.Builtin.List
open import Agda.Builtin.Unit

data D : Set where
  c : List D → D

mutual

  data P : D → Set where
    c : ∀ xs → Q xs → P (c xs)

  Q : List D → Set
  Q []      = ⊤
  Q (x ∷ _) = P x

mutual

  F : ∀ x → P x → Set₁
  F .(c xs) (c xs q) = G xs q

  G : ∀ xs → Q xs → Set₁
  G []      _ = Set
  G (x ∷ _) p = F x p

This code is rejected, but it is accepted if one of the following changes is made:

• Replace .(c xs) by (c xs).
• Replace --erased-cubical by --cubical-compatible.
• Remove --erasure.

[jespercockx]

I'm not familiar enough with the termination checker to say for sure, but the only change that my patch introduces is that the xs argument of the c constructor is no longer considered forced unless you annotate it with @0. With or without forcing, it looks to me like F and G are (mutually) structurally recursive on their second arguments, so I believe this is a pre-existing bug in either the termination checker or the implementation of --erased-cubical, and is only brought to light because of my patch.

[nad]

With or without forcing, it looks to me like F and G are (mutually) structurally recursive on their second arguments, so I believe this is a pre-existing bug in either the termination checker or the implementation of --erased-cubical, and is only brought to light because of my patch.

Arguments with types like Q xs, which only become data types after matching, are ignored for the purposes of termination checking when --without-K is used:

agda/src/full/Agda/Termination/TermCheck.hs

Lines 503 to 507 in 1354c8a

	-- If --without-K, we disregard all arguments (and result)
	-- which are not of data or record type.
	withoutKEnabled <- liftTCM withoutKOption
	applyWhen withoutKEnabled (setMasks t) $ do

agda/src/full/Agda/Termination/TermCheck.hs

Lines 590 to 598 in 1354c8a

	checkArgumentTypes (ExtendTel dom atel) = do
	TelV tel2 t <- telViewPath $ unDom dom
	d <- addContext tel2 $
	(isNothing <$> isDataOrRecord (unEl t)) `or2M` (isJust <$> isSizeType t)
	when d $
	reportSDoc "term.mask" 20 $ do
	"argument type "
	<+> prettyTCM t
	<+> " is not data or record type, ignoring structural descent for --without-K"

Furthermore, when --erased-cubical or --cubical is used, then dot patterns are never used:

agda/src/full/Agda/Termination/TermCheck.hs

Lines 248 to 265 in 1354c8a

	-- Andrea: 22/04/2020.
	-- With cubical we will always have a clause where the dot
	-- patterns are instead replaced with a variable, so they
	-- cannot be relied on for termination.
	-- See issue #4606 for a counterexample involving HITs.
	--
	-- Without the presence of HITs I conjecture that dot patterns
	-- could be turned into actual splits, because no-confusion
	-- would make the other cases impossible, so I do not disable
	-- this for --without-K entirely.
	ifM (isJust . optCubical <$> pragmaOptions) (return r) {- else -} $
	case r of
	r@Right{} -> return r
	Left{} -> do
	-- Try again, but include the dot patterns this time.
	calls2 <- terSetUseDotPatterns True $ collect
	reportCalls "" calls2
	billToTerGraph $ Term.terminates calls2

agda/src/full/Agda/Termination/TermCheck.hs

Lines 405 to 423 in 1354c8a

	-- Andrea: 22/04/2020.
	-- With cubical we will always have a clause where the dot
	-- patterns are instead replaced with a variable, so they
	-- cannot be relied on for termination.
	-- See issue #4606 for a counterexample involving HITs.
	--
	-- Without the presence of HITs I conjecture that dot patterns
	-- could be turned into actual splits, because no-confusion
	-- would make the other cases impossible, so I do not disable
	-- this for --without-K entirely.
	--
	-- Andreas, 2022-03-21: The check for --cubical was missing here.
	ifM (isJust . optCubical <$> pragmaOptions) (return r) {- else -} $ case r of
	Right () -> return $ Right ()
	Left{} -> do
	-- Try again, but include the dot patterns this time.
	calls2 <- terSetUseDotPatterns True $ collect
	reportCalls "" calls2
	billToTerGraph $ Term.terminatesFilter (== index) calls2

It appears that without your change in place Agda does not treat .(c xs) as a dot pattern, whereas this is the case after your change. Is this expected?

My original code is more in the style of F _ (c xs q) = G xs q (but with an implicit argument instead of _), and I can fix the code by replacing it with something like F (c _) (c xs q) = G xs q.

[jespercockx]

Ah I see. For forced arguments, there is some code that moves dot patterns internally to the forced position. So if the argument is forced, then internally the pattern instead becomes

  F (c xs) (c .xs q) = G xs q

With my change, the argument to c is no longer considered forced and thus there is no need to move the dot. However, this interacts with the termination checker in an unfortunate way, as you have noticed. The easy workaround is thus to move the dot by hand.

Ideally we would solve this by making the termination checker less sensitive to syntactic details such as the position of a dot pattern. However, this might be tricky in the case of Cubical Agda.

[jespercockx]

This could be considered for 2.6.4.1.