Not enough injectivity with --cubical

[plt-amy]

Minimized from a build failure in the cubical library (vindicated: I was sure it wasn't my inS/outS elision code).

{-# OPTIONS --cubical #-}

module test where

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

data Fin : Nat → Set where
  zero : {n : Nat} → Fin (suc n)
  suc  : {n : Nat} (i : Fin n) → Fin (suc n)

data ⊥ : Set where

toℕ : ∀ {n} → Fin n → Nat
toℕ zero    = 0
toℕ (suc i) = suc (toℕ i)

postulate
  inj-toℕ : {n : Nat} {k l : Fin n} → (toℕ k ≡ toℕ l) → k ≡ l
  isSetℕ : (x y : Nat) (p q : x ≡ y) → p ≡ q

ap : ∀ {A : Set} {B : A → Set} (f : ∀ x → B x) → ∀ {x y : A} (p : x ≡ y)
   → PathP (λ i → B (p i)) (f x) (f y)
ap f p i = f (p i)

inj-cong : {n : Nat} {k l : Fin n} → (p : toℕ k ≡ toℕ l) → ap toℕ (inj-toℕ p) ≡ p
inj-cong p = isSetℕ _ _ _ _

2.6.2.2 is fine, master yells

Failed to solve the following constraints:
  toℕ _y_72 = toℕ l : Nat (blocked on _y_72)
  toℕ _x_71 = toℕ k : Nat (blocked on _x_71)

because toℕ has hcomp/trX clauses and won't be marked injective.

[jespercockx]

Would it be sound to ignore the generated hcomp/trX clauses for the purpose of injectivity analysis? @Saizan @mortberg ?

[plt-amy]

For reference here's the commit that caused this: ff2e436

and the two issues it solves: #5579 #5576

[andreasabel]

@plt-amy : Currently this issue is both labeled language change (suggesting there should be a changelog entry explaining the change) and regression on master (suggesting it should not be in the changelog at all).
Could you help sort out this paradox, and add a changelog entry if needed?

(Reopening this so that we do not lose track of this formal issue.)

[plt-amy]

Yes I can: The regression on master is as described in the issue: basically no injectivity was happening for e.g. functions that match on Fin n.

As part of the fix, the language change is that functions matching on higher inductive types are no longer considered for injectivity. Changelog for that is in 7a63062

[andreasabel]

Thanks for the clarification! I think we can omit this issue from the changelog then.

[andreasabel]

Turns out that its PR #6219 already is mentioned in the changelog.