Should the predicate be erasable in the subst rule (without-K)

[andreasabel]

With Nisse and Andrea we discussed that the definitions below, erasing P, might not be compatible with univalence.

{-# OPTIONS --without-K #-}

open import Agda.Builtin.Equality

subst : {@0 A : Set} (@0 P : A → Set) {x y : A} (p : x ≡ y) → P x → P y
subst P refl z = z

subst' : {@0 A : Set} (@0 P : A → Set) {@0 x y : A} (p : x ≡ y) → P x → P y
subst' P refl z = z

Cf. #4784

[Saizan]

Let ua : A ≃ B -> A ≡ B be the map we get from univalence, then with (a level polymorphic) subst from above we can define

foo = subst (\ X -> X) (ua notEquiv) true
bar = subst (\ X -> Bool) (ua notEquiv) true

we can then prove that foo ≡ false while bar ≡ true.

Since foo and bar only differ in the P argument, this suggests that P is runtime relevant when univalence is around.

[andreasabel]

Since foo and bar only differ in the P argument, this suggests that P is runtime relevant when univalence is around.

P is sort of the type-code that is recursed on to compute the "functorial action" that subst exhibits. Maybe to get a better intuition, could you complete here the definition of subst, @Saizan, with the additional reduction rules that are not visible in the surface syntax? The surface syntax only has the user-written clause

subst P refl z = z

which justifies the typing that Agda accepts.

[Saizan]

If you mean in the --cubical case, we would have e.g. this extra clause, where I added type annotations to some variables in the pattern for clarity.

subst {A} {P} {x} {y} (transpX (p : Path y' y) (r : x ≡ y')) z
  = transp (\ i -> P (p i)) i0 (subst {A} {P} {x} {z} r z)

[jespercockx]

See also #5266. It really depends on what we want --without-K to mean:

1. Don't use UIP during the elaboration of pattern matching to a case tree
2. Don't use any features that are incompatible with univalence (or perhaps with HITs)

[nad]

Note that this also affects --erased-cubical:

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

open import Agda.Builtin.Bool using (Bool; true; false)
open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.Cubical.Path using () renaming (_≡_ to Path)
open import Agda.Builtin.Cubical.Glue using (_≃_)
open import Agda.Builtin.IO using (IO)
open import Agda.Builtin.Sigma using (_,_; fst)
open import Agda.Builtin.Unit using (⊤)
open import Agda.Primitive using (Level)
open import Agda.Primitive.Cubical
  using (primTransp; i0; primIMin; primINeg)

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

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

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

trans : x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl

subst :
  {@0 A : Set a} {@0 x y : A}
  (@0 P : A → Set p) → x ≡ y → P x → P y
subst _ refl p = p

subst-Path :
  {@0 A : Set a} {@0 x y : A}
  (P : A → Set p) → Path x y → P x → P y
subst-Path P eq p = primTransp (λ i → P (eq i)) i0 p

Path→≡ : Path x y → x ≡ y
Path→≡ eq = subst-Path (_ ≡_) eq refl

postulate
  @0 univ               : A ≃ B → Path A B
  @0 subst-Path-id-univ :
       Path (subst-Path (λ A → A) (univ eq) x) (fst eq x)

J :
  (P : ∀ {y} → Path x y → Set p) →
  P (λ _ → x) →
  (eq : Path x y) → P eq
J P p eq = primTransp (λ i → P (λ j → eq (primIMin i j))) i0 p

subst-univ :
  {@0 A B : Set a}
  (@0 P : Set a → Set p) → @0 A ≃ B → P A → P B
subst-univ P eq p =
  subst (λ ([ x ]) → P x) (Path→≡ ([]-cong (univ eq))) p

subst-Path→≡ :
  {p : P x} →
  subst P (Path→≡ eq) p ≡ subst-Path P eq p
subst-Path→≡ {P = P} {x = x} {p = p} = J
  (λ eq → subst P (Path→≡ eq) p ≡ subst-Path P eq p)
  (trans (Path→≡ λ i → subst P (primTransp (λ _ → x ≡ x) i refl) p)
     (Path→≡ λ i → primTransp (λ _ → P x) (primINeg i) p))
  _

@0 subst-univ-id :
  subst-univ (λ A → A) eq x ≡ fst eq x
subst-univ-id = trans subst-Path→≡ (Path→≡ subst-Path-id-univ)

not : Bool → Bool
not true  = false
not false = true

@0 swap : Bool ≃ Bool
swap = not , omitted
  where
  postulate
    omitted : _

should-be-false : Bool
should-be-false = subst-univ (λ A → A) swap true

@0 is-false : should-be-false ≡ false
is-false = subst-univ-id

postulate
  print : Bool → IO ⊤

{-# COMPILE GHC print = print #-}

main : IO ⊤
main = print should-be-false

I postulated some things, but the only non-erased postulate is the one for print, and the remaining postulates should be non-controversial.

The result of running the resulting binary (with or without --ghc-strict) is incorrect:

True

[nad]

Perhaps the problem will be fixed once (if?) proper support for inductive families is added to Cubical Agda (#3733), as discussed above.

It really depends on what we want --without-K to mean:

I think there should be some variant of Agda that is compatible with both --with-K and --cubical/--erased-cubical. This variant could perhaps use a more descriptive name than "without K", but for historical reasons I don't think we should remove the flag --without-K.

[nad]

If you mean in the --cubical case, we would have e.g. this extra clause, where I added type annotations to some variables in the pattern for clarity.

Doesn't it make sense to include the extra clauses also when --without-K is used? (This is related to issue #4527.)

[Saizan]

If you mean in the --cubical case, we would have e.g. this extra clause, where I added type annotations to some variables in the pattern for clarity.

Doesn't it make sense to include the extra clauses also when --without-K is used? (This is related to issue #4527.)

We already discussed this: looking at these generated clauses might be a good way to avoid definitions incompatible with --cubical.

[Saizan]

Commit e6404c3 checks the usability of the clause generated for the transpX constructor.
This raises a type error for subst and subst' defined with an erased P argument.

unbox from #5468 also triggers this error.

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

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

Unfortunately a benign definition like the following from the runtime irrelevance docs also triggers this error:

 variable
    a b : Level
    A : Set a

  data Vec (A : Set a) : @0 Nat → Set a where                                                                                                             
    []  : Vec A 0                                                                                                                                         
    _∷_ : ∀ {@0 n} → A → Vec A n → Vec A (suc n)                                                                                                          


  foldl : (B : Nat → Set b)                                                                                                                               
        → (f : ∀ {@0 n} → B n → A → B (suc n))                                                                                                            
        → (z : B 0)                                                                                                                                       
        → ∀ {@0 n} → Vec A n → B n                                                                                                                        
  foldl B f z []       = z                                                                                                                                
  foldl B f z (x ∷ xs) = foldl (λ n → B (suc n)) (λ {n} → f {suc n}) (f z x) xs                                                                           

However closed paths in Nat are constant, we might want to special case indexes like that.

[Saizan]

The following is however fine, i.e. with B : @0 Nat -> Set b.

  foldl' : (B : @0 Nat → Set b)                                                                                                                           
        → (f : ∀ {@0 n} → B n → A → B (suc n))                                                                                                            
        → (z : B 0)                                                                                                                                       
        → ∀ {@0 n} → Vec A n → B n                                                                                                                        
  foldl' B f z []       = z                                                                                                                               
  foldl' B f z (x ∷ xs) = foldl' (λ n → B (suc n)) (λ {n} → f {suc n}) (f z x) xs

[nad]

Unfortunately a benign definition like the following from the runtime irrelevance docs also triggers this error:

Can you explain in more detail what happens? Is the problem that B is applied to the erased variable n?

[Saizan]

We get a generated clause of the form

foldl B f z (transpX-Vec x φ []) = transp (λ i → B (x i)) φ (foldl B f z [])

where transpX-Vec has type

{a : Level} {A : Set a} (@0 x : I → Nat) (φ : I) → Vec A (x i0) → Vec A (x i1)

so (λ i → B (x i)) is only usable in an erased context while the transport is supposed to be usable at runtime.

[nad]

@Saizan, can this issue be closed now (after some test cases have been added)? Enhancements could be discussed in a separate issue.

[nad]

@Saizan, can this issue be closed now?

[Saizan]

Yes, looks good.

[nad]

@plt-amy, did you say that you have some idea about how we can disallow problematic definitions like those discussed above without generating Cubical Agda code behind the scenes (by leveraging the current infrastructure for checking definitions by pattern matching)? That could be beneficial also to users of Cubical Agda, who might not have to see generated code in error messages.

Note that the current implementation checks things for several modalities, not just erasure. (However, irrelevance is ignored, see issue #5611.)

[nad]

The examples in the OP are now again accepted when --without-K is used. @andreasabel, perhaps you want to rename this issue.

[plt-amy]

@nad Well I did have an idea before, but reflecting on it now, I think it's too complicated (and wouldn't work anyway)...

But an alternative dawned on me earlier today: if an acceptable fix for this issue is to reject all definitions that --cubical would reject when it generates the trX clauses, then it's enough to check that the target type of the RHS is usable at "its own" modality. That's essentially what the cubical check is doing anyway, which is why it rejects this:

{-# OPTIONS --cubical #-}
module Test14 where

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat
open import Agda.Primitive

fakeout : {@0 A : Set} (@0 P : A → Set) {@0 α β : A} (p : α ≡ β) → P α → P α
fakeout {A} P {x} {y} refl a = {!   !}

with the error

Agda.Primitive.Cubical.primTransp (λ i → P α) φ
(fakeout P refl
 (Agda.Primitive.Cubical.primTransp (λ i → P α) φ
  x)) is not usable at the required modality .

(side note: @ω probably shouldn't be printed blank for error messages..)

[nad]

What would the error message look like with that approach?

[nad]

Given that @plt-amy has provided a proposed new implementation of the check I'm reopening this issue.

[andreasabel]

Given that @plt-amy has provided a proposed new implementation of the check I'm reopening this issue.

Please reopen with concrete TODOs.

[nad]

The proposed new implementation has been completed and committed.