Proof of ⊥ using HIT-indexed type

[mkm]

Proof of ⊥ using HIT-indexed type

[szumixie]

Agda correctly throws a termination error with --no-forcing. #4606 is related, but forcing removes the dot from the dot pattern.

Slightly simplified code:

{-# OPTIONS --cubical --safe #-}

open import Agda.Primitive.Cubical
open import Agda.Builtin.Cubical.Path

data ⊥ : Set where

data T : Set where
  zero : T
  suc : T → T
  eq : (x : T) → suc x ≡ x

data IsSuc : T → Set where
  is-suc : (x : T) → IsSuc (suc x)

all-sucs : (x : T) → IsSuc x
all-sucs x = primTransp (λ i → IsSuc (eq x i)) i0 (is-suc x)

not-suc : (x : T) → IsSuc x → ⊥
not-suc .(suc x) (is-suc x) = not-suc x (all-sucs x)

nope : ⊥
nope = not-suc zero (all-sucs zero)

[andreasabel]

@szumixie wrote:

but forcing removes the dot from the dot pattern.

Thanks for the analysis!

Should we disable --forcing for --cubical and make it unsafe to enable it?

[jespercockx]

Should we disable --forcing for --cubical and make it unsafe to enable it?

That seems like quite a drastic solution to me. Couldn't we rather make it so that forcing does not apply to HITs, but still apply it to regular datatypes?

[jespercockx]

Oh, it's not that easy, since the type that forcing is applied to is not a HIT itself, it only is indexed by a HIT. Rather, what we could do is to change the forcing analysis so it does not detect an argument as being forced if it appears as an argument to a constructor of a HIT.

Basically, we should check here

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

Line 167 in 35b5659

Con _ _ vs -> forcedVariables vs

that the constructor is not a HIT constructor, and if it is return mempty.

[andreasabel]

that the constructor is not a HIT constructor, and if it is return mempty.

I could easily implement this.

However, it is not clear to me what is the right thing to do.
Because we have no compiler for cubical, the forcing analysis is a bit hanging in the air, it is not clear what it should achieve.
With K (and T not being a HIT), IsSuc would be a proposition and erased during compilation.
In Cubical (and T as defined), both T and IsSuc are contractible (as witnessed by all-sucs), so, have no content and could be erased (!?).
Maybe nothing is wrong with the forcing analysis, but instead the termination checker should work on the compiled clauses and without K not look into lazy matches for termination witnesses?

[jespercockx]

Because we have no compiler for cubical, the forcing analysis is a bit hanging in the air, it is not clear what it should achieve.

Semantically speaking, the forcing analysis tries to detect constructor arguments that are uniquely determined by the constructor indices. Here, the index suc x does not uniquely determine the argument x because suc is not injective. Hence, in this case the forcing analysis is clearly making a wrong assumption, and my proposed change would fix that.

You seem to be making a more general claim that forcing is something that should not be done at all in case of cubical. However, I'd like to see more evidence for that claim beyond just this single issue.