Standard library Data.Nat.DivMod fails with cubical error, even though no --cubical is used

[andreasabel]

Lifted from #5605 (comment):

/home/runner/work/agda/agda/std-lib/src/Data/Nat/DivMod.agda:205,1-47
Agda.Primitive.Cubical.primTransp
(λ i →
   m /
   Agda.Primitive.Cubical.primComp (λ i₁ → ℕ)
   (λ i₁ .o →
      Agda.Primitive.Cubical.primPOr
      (Agda.Primitive.Cubical.primIMax
       (Agda.Primitive.Cubical.primINeg i) φ)
      i (λ .o₁ → suc m₁) (λ .o₁ → x i₁) _)
   (suc m₁)
   ≤ n / x₁ i)
φ (/-mono-≤ x₂ (s≤s x₃)) is not usable at the required modality
when checking the definition of /-mono-≤

I suppose this is a regression in 2.6.3, because the master of the std lib is supposed to build with 2.6.2.

[nad]

This is presumably related to @Saizan's fix (feb4fe4) of #5448 and #5468.

[Saizan]

Someone could design a way to get a better error message when this check fails.

[nad]

Here's a fixed variant of the code:

/-mono-≤ :
  ∀ {m n o p} .⦃ _ : NonZero o ⦄ .⦃ _ : NonZero p ⦄ →
  m ≤ n → o ≥ p → m / o ≤ n / p
/-mono-≤ {m = m} {n = n} {o = o} m≤n o≥p = helper o≥p refl
  where
  helper :
    ∀ {o′ p} .⦃ _ : NonZero p ⦄ →
    o′ ≥ p → o ≡ o′ → m / o ≤ n / p
  helper (s≤s o≥p) refl = divₕ-mono-≤ 0 m≤n o≥p

[MatthewDaggitt]

As I wrote this particular piece of code a few months back, I'm a bit confused about what is wrong with it. I take it from the discussion, that Agda 2.6.3 is more strict about irrelevant arguments in some manner? But why is it throwing a cubical error?

[nad]

Someone could design a way to get a better error message when this check fails.

You can get more information by using -vtc.irr:50:

agda/src/full/Agda/TypeChecking/Irrelevance.hs

Lines 384 to 394 in d8145b9

	instance UsableModality Term where
	usableMod mod u = do
	case u of
	Var i vs -> do
	imod <- getModality <$> domOfBV i
	let ok = imod `moreUsableModality` mod
	reportSDoc "tc.irr" 50 $
	"Variable" <+> prettyTCM (var i) <+>
	text ("has modality " ++ show imod ++ ", which is a " ++
	(if ok then "" else "NOT ") ++ "more usable modality than " ++ show mod)
	return ok `and2M` usableMod mod vs

Variable x₄ has modality Modality {modRelevance = Irrelevant, modQuantity = Quantityω QωInferred, modCohesion = Continuous}, which is a NOT more usable modality than Modality {modRelevance = Relevant, modQuantity = Quantityω QωInferred, modCohesion = Continuous}

However, the variable x₄ is not part of the type signature, and it might not be clear why its modality is compared to the given modality. Perhaps we could change usableMod so that, when it fails, it returns a tree that captures every step of the decision process.

[nad]

As I wrote this particular piece of code a few months back, I'm a bit confused about what is wrong with it. I take it from the discussion, that Agda 2.6.3 is more strict about irrelevant arguments in some manner? But why is it throwing a cubical error?

Code that uses --without-K should be compatible with Cubical Agda. When you use --without-K or --cubical Agda sometimes generates extra code behind the scenes. In this case Agda deems that the generated code is not OK, and complains. I think we should try to avoid giving error messages that refer to generated code (but I also think having such errors is better than incorrectly accepting code).

[MatthewDaggitt]

Wow, so when you use --without-K you actually start using cubical primitives (e.g. primTransp) under the hood? That's somewhat... unexpected! Is this documented anywhere?

[gallais]

There's the discussion in #5266

[MatthewDaggitt]

Switching back to here, in agda/agda-stdlib#1614 @gallais writes:

Another obvious question is: can we do anything on the Agda side of things so that the
code does not need to be slightly rewritten to appease the cubical machinery?

Which I strongly agree with! The code as is, isn't "wrong" per se right? It's that the new check introduced in feb4fe4 isn't granular enough?

At the very least, @Saizan is right that we need a better error message. Ideally one without cubical code in, but at the very least one which says which modality is the problem?

[nad]

This check was introduced to address problems related to @0. I don't know if there are any similar problems related to irrelevance. If we were positive that there are no such problems, then we could change the check.

By the way, is irrelevance known to be compatible with Cubical Agda?

[Saizan]

By the way, is irrelevance known to be compatible with Cubical Agda?

There might be some devil in the details, since no one explicitly looked into it afaict, but it would make sense in the cubical sets model as a strict version of propositional truncation, which is known to work. The --experimental-irrelevance parts would require a different model though.

The check is required for @0 because types are erased by default, so we don't know if they'll be usable in a transport at \omega.

Types are however Relevant and so without --experimental-irrelevance they can only mention irrelevant variables in an irrelevant position. So it seems like the problems we have with @0 would not occur.

Maybe we can make --experimental-irrelevance not --safe with --without-K ?

[jespercockx]

I don't think --experimental-irrelevance is safe to begin with (or if it is, it probably shouldn't be).

[nad]

Here is the check that @Saizan added:

agda/src/full/Agda/TypeChecking/Coverage/Cubical.hs

Lines 881 to 887 in feb4fe4

	let mod = fromMaybe __IMPOSSIBLE__ $ scTarget old_sc
	-- we follow what `cover` does when updating the modality from the target.
	applyModalityToContext mod $ do
	unlessM (asksTC hasQuantity0) $ do
	let mod = getModality . fromJust $ scTarget old_sc
	reportSDoc "tc.cover.trxcon" 20 $ text "testing usable at mod: " <+> pretty mod
	addContext cTel $ usableAtModality mod rhs

I set the relevance part of mod to Irrelevant, and then the standard library's master branch was accepted. Would it make sense to restrict the check in this way, and release 2.6.3 instead of 2.6.2.1? It might be the case that some existing code that uses @0 and --without-K is rejected with an incomprehensible error message, but at least the standard library is not affected.

@Saizan, what is the status of your changes related to inductive families? You put them on the master branch, does that mean that you think they are mostly ready to be released?

I don't think --experimental-irrelevance is safe to begin with (or if it is, it probably shouldn't be).

agda/src/full/Agda/Interaction/Options/Base.hs

Lines 348 to 367 in 2976b59

	unsafePragmaOptions :: CommandLineOptions -> PragmaOptions -> [String]
	unsafePragmaOptions clo opts =
	[ "--allow-unsolved-metas" | optAllowUnsolved opts ] ++
	[ "--allow-incomplete-matches" | optAllowIncompleteMatch opts ] ++
	[ "--no-positivity-check" | optDisablePositivity opts ] ++
	[ "--no-termination-check" | not (optTerminationCheck opts) ] ++
	[ "--type-in-type" | not (optUniverseCheck opts) ] ++
	[ "--omega-in-omega" | optOmegaInOmega opts ] ++
	[ "--sized-types" | collapseDefault (optSizedTypes opts) ] ++
	[ "--injective-type-constructors" | optInjectiveTypeConstructors opts ] ++
	[ "--irrelevant-projections" | optIrrelevantProjections opts ] ++
	[ "--experimental-irrelevance" | optExperimentalIrrelevance opts ] ++
	[ "--rewriting" | optRewriting opts ] ++
	[ "--cubical and --with-K" | optCubical opts == Just CFull
	, not (collapseDefault $ optWithoutK opts) ] ++
	[ "--erased-cubical and --with-K" | optCubical opts == Just CErased
	, not (collapseDefault $ optWithoutK opts) ] ++
	[ "--cumulativity" | optCumulativity opts ] ++
	[ "--allow-exec" | optAllowExec opts ] ++
	[]

[Saizan]

The status is still as described in #3733, the inductive families can be used but there's interactions with termination and positivity checking that are not resolved, meaning those checks are likely accepting definitions that should not be.

It did not get any worse than 2.6.2, though fewer people might have been inclined to use inductive families with cubical before these changes.

[nad]

@Saizan wrote:

The status is still as described in #3733, the inductive families can be used but there's interactions with termination and positivity checking that are not resolved, meaning those checks are likely accepting definitions that should not be.

Turning on those checks should be fairly easy, right? However, I guess that we might get more problems like that discussed in this ticket. Have you tried this?

@MatthewDaggitt wrote:

Wow, so when you use --without-K you actually start using cubical primitives (e.g. primTransp) under the hood? That's somewhat... unexpected!

The idea is that it should be possible to import code that uses --without-K from modules that use --cubical (or --with-K, or --erased-cubical). Previously Cubical Agda has not properly supported inductive families, and now that such support is added it does not come as a surprise to me that some code that uses --without-K is affected. However, in this particular case the implemented check was perhaps too conservative, and the error message could certainly have been better.

[Saizan]

Turning on those checks should be fairly easy, right? However, I guess that we might get more problems like that discussed in this ticket. Have you tried this?

Doing just the naive thing of letting termination and positivity check look at the extra generated clauses I was getting a lot of rejected definitions in the standard library, so that doesn't seem advisable without more work put into improving the checks.

[nad]

I set the relevance part of mod to Irrelevant, and then the standard library's master branch was accepted. Would it make sense to restrict the check in this way, and release 2.6.3 instead of 2.6.2.1? It might be the case that some existing code that uses @0 and --without-K is rejected with an incomprehensible error message, but at least the standard library is not affected.

@andreasabel, what do you think?

[andreasabel]

I have not followed the discussion, maybe this is something for the next dev meeting. Even if we release 2.6.2.1, we can still release 2.6.3 at any time suitable (even on the same day, if you will). However, I think that if we release 2.6.3 now, we might soon have to re-release because of #5659. So I think I prefer releasing 2.6.2.1 now with a more conservative feature set, and release 2.6.3 soon (after maybe a bit more testing).

[nad]

Here is the check that @Saizan added:

agda/src/full/Agda/TypeChecking/Coverage/Cubical.hs

Lines 881 to 887 in feb4fe4

	let mod = fromMaybe __IMPOSSIBLE__ $ scTarget old_sc
	-- we follow what `cover` does when updating the modality from the target.
	applyModalityToContext mod $ do
	unlessM (asksTC hasQuantity0) $ do
	let mod = getModality . fromJust $ scTarget old_sc
	reportSDoc "tc.cover.trxcon" 20 $ text "testing usable at mod: " <+> pretty mod
	addContext cTel $ usableAtModality mod rhs

I tried to replace this code with the following code (more or less as discussed above, except that I suspect that the last time I only changed the second definition of mod):

  let mod =
        setRelevance Irrelevant $  -- See #5611.
        getModality $ fromMaybe __IMPOSSIBLE__ $ scTarget old_sc
  -- we follow what `cover` does when updating the modality from the target.
  applyModalityToContext mod $ do
    unlessM (asksTC hasQuantity0) $ do
    reportSDoc "tc.cover.trxcon" 20 $ text "testing usable at mod: " <+> pretty mod
    addContext cTel $ usableAtModality mod rhs

With this change the master branch of the standard library is accepted. @Saizan, does this look fine to you? In that case I'll prepare a pull request.

The change leads to error messages involving irrelevance, even if no irrelevance is used. For instance, for test/Fail/Issue5448-1.agda, the old error message is the following one:

Issue5448-1.agda:8,1-19
Agda.Primitive.Cubical.primTransp (λ i → P (x i)) φ
(subst P refl
 (Agda.Primitive.Cubical.primTransp (λ i → P x₁) φ
  x₂)) is not usable at the required modality
when checking the definition of subst

The new error message includes .:

Issue5448-1.agda:8,1-19
Agda.Primitive.Cubical.primTransp (λ i → P (x i)) φ
(subst P refl
 (Agda.Primitive.Cubical.primTransp (λ i → P x₁) φ
  x₂)) is not usable at the required modality .
when checking the definition of subst

The error message reflects what is going on, so that is perhaps fine.