Allow flat matching on inductive families

[felixwellen]

The following example does not type check with latest Agda (master):

{-# OPTIONS --cubical #-}
open import Agda.Primitive

data Flat (@♭ A : Set) : Set where
    flat : (@♭ a : A) → Flat A

data Id {A : Set} : A → A → Set where
  refl : {x : A} → Id x x

CommFlatId : {@♭ A : Set} {@♭ u v : A} → Flat (Id u v) → Id (flat u) (flat v)
CommFlatId (flat refl) = refl

Agda gives the following error:

/home/felixcherubini/repos/test.agda:11,1-30
Agda.Primitive.Cubical.primTransp
(λ i →
   Id (flat u)
   (flat
    (Agda.Primitive.Cubical.primTransp
     (λ i₁ → Agda.Primitive.Cubical.PathP (λ i₂ → A) (x i₁) u) φ x₁
     (Agda.Primitive.Cubical.primINeg i))))
φ (CommFlatId (flat refl)) is not usable at the required modality .
when checking the definition of CommFlatId

Agda throws the same error with --cubical-compatible and if I understood #6236 correctly, once it is merged, Agda will also throw an error without any flag.

But, as I understand the flat modality in Agda, it should provide an approximation to what can be done with flat and sharp in real-cohesive hott (article). There, 'crisp identity induction' is derivable (Theorem 5.6 on p. 35), which is a general induction principle that would justify the pattern matching in the example above. The reasoning should apply to general inductive types.

So, considering what the flat modality in Agda should model, I think pattern matching on inductive families should be allowed and without any extra assumption, it should not be possible to derive anything new with this (up to adding '@♭' to derivable statements).

[nad]

I seem to recall that every program that is accepted is also accepted if every reference to the cohesive modality is removed, and I suspect that all compiler backends ignore this modality. Thus your change is presumably "safe".

Is it the case that this modality is only used together with (unprovable) postulates or assumptions? In that case the question is perhaps if your change is compatible with the postulates or assumptions that users want to use.

[nad]

Thus your change is presumably "safe".

But according to @plt-amy (see pull request #6239) the change makes some generated code fail the type-checker.

[andreasabel]

Has this issue been fixed by

• #6238: Allow flat matching on inductive families #6239?

[plt-amy]

Yes. I'll write a follow-up issue to cover working out the proper interaction(s) between Cubical Agda and the ♭ modality.