If you switch from --cubical to --without-K, the definition is accepted, because then dot patterns are taken into consideration for termination certification.

• switching off dot pattern termination: The combination of Cubical Agda with inductive families is logically inconsistent #4606
• a regression reported in: Cubical Agda: Program rejected by termination checker due to moved dot pattern #4725

If the program should be rejected when --cubical is used, then it should also be rejected when --without-K is used, right?

Turning off dot-pattern termination for --without-K would mean that we could not do the usual proof by pattern matching that the successor relation is well-founded:

{-# OPTIONS --without-K #-}

open import Agda.Builtin.Nat using (Nat; zero; suc)

data Acc {A : Set} (R : A → A → Set) (x : A) : Set where
  acc : (∀ y → R y x → Acc R y) → Acc R x

data _<_ (x : Nat) : Nat → Set where
  <S : x < suc x

iswf< : ∀ x → Acc _<_ x
iswf< x = acc (h x)
  where
  h : ∀ x y → y < x → Acc _<_ y
  h .(suc y) y <S = acc (h y)

If the program should be rejected when --cubical is used, then it should also be rejected when --without-K is used, right?

After the fix, it is accepted in both modes. But see my previous comment for a violation of your principle. Likely, the termination checker rejects too many programs under --cubical, just to be on the safe side. But with termination checking being undecidable, we accept that it is incomplete, and may also violate your principle. (If you want your principle, we could e.g. have a check that --cubical is actually necessary, i.e. cubical features are positively used, because in this case, the type checker would already not succeed with just --without-K.)

"My principle" is that code that is accepted when --without-K is used should be accepted also when --with-K, --erased-cubical or --cubical is used. Every extra check that is performed in Cubical Agda should also be performed when --without-K is used.

Turning off dot-pattern termination for --without-K would mean that we could not do the usual proof by pattern matching that the successor relation is well-founded:

The code is accepted (with --erased-cubical) if the dot is moved:

iswf< : ∀ x → Acc _<_ x
iswf< x = acc (h x)
  where
  h : ∀ x y → y < x → Acc _<_ y
  h (suc y) .y <S = acc (h y)

However, Agda emits a warning:

Could not generate equivalence when splitting on indexed family,
the function will not compute on transports by a path.
  Reason: UnsupportedYet Injectivity
                           position:    0
                           type:        Nat
                           datatype:    Nat
                           parameters: 
                           indices:    
                           constructor: suc
when checking the definition of h

"My principle" is that code that is accepted when --without-K is used should be accepted also when --with-K, --erased-cubical or --cubical is used. Every extra check that is performed in Cubical Agda should also be performed when --without-K is used.

I realised that my statement is too strong. One could make Cubical Agda checks unnecessarily strict without the risk of breaking anything, and that may be the case for the check under discussion. @Saizan wrote the following:

I'm not sure exactly how to interpret this. Would it make sense to include dot patterns when checking termination for a Cubical Agda definition that does not involve matching for HITs?

Would it make sense to include dot patterns when checking termination for a Cubical Agda definition that does not involve matching for HITs?

I suppose so.