Could the termination checker be less restrictive when the K rule is turned off?

[nad]

The termination checker is currently more conservative when the K rule is turned off (#1023). I think that all the problematic examples that are listed in Issue #1023 rely on pattern matching on refl. If inductive families were disallowed (under some flag), would it be safe to loosen the restrictions?

@Saizan is/was working on proper support for inductive families in Cubical Agda (#3733). Is this done in such a way that the restrictions become unnecessary?

[andreasabel]

If inductive families were disallowed (under some flag), would it be safe to loosen the restrictions?

Well, if you do not have equality in the first place, there should be no difference in K or without-K.

[nad]

In Cubical Agda you would still have paths.

[Saizan]

The issue with termination checking --without-K seems to be that the checker does not get to see the transports that actually happen when given a non-refl proof.

When implementing inductive families for Cubical I do generate a clause that inserts the necessary transports, so termination checking that clause should catch the examples from the other thread.

If your types are refining just because you are matching on some plain datatype then I don't think it should be rejected, as that wouldn't need extra desugaring. Someone should do a proof though?

e.g., the following is easy to translate to eliminators/see terminating, but in general?

open import Agda.Builtin.Nat

data Unit : Set where
  unit : Unit

F : Unit -> Set
F unit = Nat

test : ∀ (x : Unit) → F x → Nat
test unit zero = zero
test unit (suc n) = suc (test unit n)

[nad]

When implementing inductive families for Cubical I do generate a clause that inserts the necessary transports, so termination checking that clause should catch the examples from the other thread.

The idea is that --without-K should be compatible both with --with-K and with --cubical. Would it make sense to generate these clauses whenever the K rule is turned off, or could this create problems for code that relies on K? (It might make sense for compiler backends to remove the extra clauses.) In that case we could perhaps remove the restriction and rely only on regular termination checking.

[Saizan]

A way to make the termination checker less restrictive without involving (#3733) would be to only do the masking from the solution to #1023 when there's a match on an inductive family in one of the clauses.