Disallow certain forms of pattern matching when an index is erased

[nad]

The following code should not be accepted:

{-# OPTIONS --erased-cubical #-}

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

private
  variable
    a p : Level
    A   : Set a
    P   : A → Set p
    x y : A

refl : x ≡ x
refl {x = x} = λ _ → x

subst : (P : A → Set p) → x ≡ y → P x → P y
subst P eq p = primTransp (λ i → P (eq i)) i0 p

record Erased (@0 A : Set a) : Set a where
  constructor [_]
  field
    @0 erased : A

[]-cong : {@0 A : Set a} {@0 x y : A} → @0 x ≡ y → [ x ] ≡ [ y ]
[]-cong eq = λ i → [ eq i ]

data Box : @0 Set → Set₁ where
  [_] : ∀ {A} → A → Box A

unbox : ∀ {@0 A} → Box A → A
unbox [ x ] = x

postulate
  @0 not : Bool ≡ Bool

should-be-true : Bool
should-be-true =
  unbox (subst (λ ([ A ]) → Box A) ([]-cong refl) [ true ])

should-be-false : Bool
should-be-false =
  unbox (subst (λ ([ A ]) → Box A) ([]-cong not) [ true ])

The (non-strict) GHC backend compiles the right-hand sides of should-be-true and should-be-false to identical pieces of code:

-- Bug.should-be-true
d_should'45'be'45'true_72 :: Bool
d_should'45'be'45'true_72
  = coe
      du_unbox_66
      (coe
         du_subst_22 (coe ())
         (coe
            C_'91'_'93'_62 (coe MAlonzo.Code.Agda.Builtin.Bool.C_true_10)))
-- Bug.should-be-false
d_should'45'be'45'false_78 :: Bool
d_should'45'be'45'false_78
  = coe
      du_unbox_66
      (coe
         du_subst_22 (coe ())
         (coe
            C_'91'_'93'_62 (coe MAlonzo.Code.Agda.Builtin.Bool.C_true_10)))

A simple way to fix this would be to disallow indices from being erased. Can we do better?

Related: #4784, #5448.

[jespercockx]

I hope you mean indices should not be erased when --erased-cubical is on, right? When it is off I don't see a problem here.

Also, I don't have a strong intuition on how --erased-cubical is supposed to work, but I have a feeling that the problem here might be that []-cong should not be accepted? Since it is turning an erased equality proof (which does not have any computational content) into a non-erased one (which does).

PS: Could you perhaps use different names for the constructors of Erased and Box? Now I had to scratch my head a few times to figure out which one was which.

[nad]

I hope you mean indices should not be erased when --erased-cubical is on, right? When it is off I don't see a problem here.

I suggest that we leave things like they are when the K rule is on.

Also, I don't have a strong intuition on how --erased-cubical is supposed to work, but I have a feeling that the problem here might be that []-cong should not be accepted? Since it is turning an erased equality proof (which does not have any computational content) into a non-erased one (which does).

This is a key lemma in the theory of Erased, and I don't see a problem with its proof, as given above.

[UlfNorell]

Perhaps unrelated to the issue at hand, but do we not have canonicity for cubical?

is-it-though : should-be-true ≡ true
is-it-though i = true
-- unbox (primTransp (λ i → Box ([]-cong refl i .Erased.erased)) i0 [ true ])
--   != true of type Bool
-- when checking the definition of is-it-though

[nad]

Cubical Agda does not yet have proper support for inductive families (#3733).

[Saizan]

The naive desugaring of Box which the bad example seems to rely on would indeed not be allowed by our rules.

data BoxD (@0 B : Set) : Set₁ where
  [_] : {A : Set} → A → (p : A ≡ B) → BoxD B
{-
{A : Set} → A → A ≡ B → BoxD B is not usable at the required modality
when checking that the type {A : Set} → A → A ≡ B → BoxD B of the
constructor [_] fits in the sort Set₁ of the datatype.
-}

A more appropriate desugaring for erased indexes might be to consider the equality erased as well

data BoxD (@0 B : Set) : Set₁ where
  [_] : {A : Set} → A → (@0 p : A ≡ B) → BoxD B

This is accepted as a definition, but unbox : {@0 A} -> BoxD A -> A cannot be written anymore, unless marked @0.

Also subst (λ ([ A ]) → BoxD A) ([]-cong not) ([ true ] refl) reduces to [ true ] ....

Which makes me wonder, can you actually prove that should-be-false is path-equal to false ?
Ok, yeah, in an erased context unbox would apply the equivalence stored in the ... above which would negate the true.

Btw, I mention the erased equality desugaring because it seems like appropriate semantics for e.g. vectors:

data Vec (A : Set) (@0 n : Nat) : Set where
  nil : (@0 p : n ≡ zero) → Vec A n
  cons : (@0 m : Nat) → A → Vec A m → (@0 p : n ≡ suc m) → Vec A n

then we need to figure out how this affects the rules for pattern matching definitions.

[nad]

A more appropriate desugaring for erased indexes might be to consider the equality erased as well

This makes sense to me.

[nad]

@Saizan, can this issue be closed now (if a test case is added)?

[nad]

@Saizan, can this issue be closed now?

[Saizan]

Yes, looks good.