Another incompatibility between erasure and univalence

[nad]

I discovered that erasure is still (#4784) not compatible with (erased) univalence and []-cong.

The following code should not be allowed:

{-# OPTIONS --safe --cubical-compatible --erasure #-}

open import Agda.Builtin.Equality

data Erased (@0 A : Set₁) : Set₁ where
  [_] : @0 A → Erased A

bad : {A B : Set} → [ A ] ≡ [ B ] → A ≡ B
bad refl = refl

The code should still be rejected if --cubical-compatible is replaced by --without-K, --erased-cubical or --cubical.

If this code is allowed, then one can construct a boolean that is provably equal to false but compiled to (more or less) true:

{-# OPTIONS --erased-cubical --erasure --hidden-argument-puns #-}

module Bug where

open import Agda.Builtin.Bool
open import Agda.Builtin.Cubical.Equiv
import Agda.Builtin.Cubical.Path as P
open import Agda.Builtin.Equality
open import Agda.Builtin.IO
open import Agda.Builtin.Sigma
open import Agda.Builtin.String
open import Agda.Builtin.Unit
open import Agda.Primitive
open import Agda.Primitive.Cubical

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

------------------------------------------------------------------------
-- Identity types

subst : (P : A → Set p) → x ≡ y → P x → P y
subst _ refl p = p

cong : (f : A → B) → x ≡ y → f x ≡ f y
cong _ refl = refl

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

------------------------------------------------------------------------
-- Paths

path-refl : x P.≡ x
path-refl {x} _ = x

J :
  {@0 A : Set a} {x y : A}
  (P : (y : A) → x P.≡ y → Set p) →
  P x path-refl →
  (eq : x P.≡ y) →
  P y eq
J P p eq = primTransp (λ i → P (eq i) (λ j → eq (primIMin i j))) i0 p

J-refl :
  {@0 A : Set a} {x : A}
  (P : (y : A) → x P.≡ y → Set p)
  (p : P x path-refl) →
  J P p path-refl ≡ p
J-refl {x} P p =
  primTransp (λ i → primTransp (λ _ → P x (λ _ → x)) (primINeg i) p ≡ p)
    i0 refl

cast : A P.≡ B → A ≃ B
cast eq = pathToEquiv (λ i → eq i)

------------------------------------------------------------------------
-- Conversion between identity types and paths

to-path : x ≡ y → x P.≡ y
to-path refl = path-refl

from-path : x P.≡ y → x ≡ y
from-path {x} = J (λ y _ → x ≡ y) refl

from-path-refl : from-path path-refl ≡ refl {x = x}
from-path-refl {x} = J-refl (λ y _ → x ≡ y) _

subst-cast :
  (eq : A P.≡ B) →
  subst (λ A → A) (from-path eq) x ≡ cast eq .fst x
subst-cast {A} {x} =
  J (λ _ eq → subst (λ A → A) (from-path eq) x ≡ cast eq .fst x)
    (trans (cong (λ eq → subst (λ A → A) eq x) from-path-refl)
       (from-path (λ i → primTransp (λ _ → A) (primINeg i) x)))

------------------------------------------------------------------------
-- Erased univalence

postulate
  @0 univ   : A ≃ B → A P.≡ B
  @0 univ-β : (A≃B : A ≃ B) → cast (univ A≃B) P.≡ A≃B

------------------------------------------------------------------------
-- Booleans

Bool-stable : @0 _≡_ {A = Bool} x y → x ≡ y
Bool-stable {x = false} {y = false} _ = refl
Bool-stable {x = true}  {y = true}  _ = refl

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

not-equiv : Bool ≃ Bool
not-equiv = not , ok
  where
  postulate ok : _

show : Bool → String
show true  = "true"
show false = "false"

------------------------------------------------------------------------
-- Erased (limited to Set₁)

data Erased (@0 A : Set₁) : Set₁ where
  [_] : @0 A → Erased A

[]-cong : @0 x ≡ y → [ x ] ≡ [ y ]
[]-cong eq = from-path (λ i → [ to-path eq i ])

[]-cong-refl : []-cong (refl {x = x}) ≡ refl
[]-cong-refl = from-path-refl

-- The following definition should not be allowed.

bad : [ A ] ≡ [ B ] → A ≡ B
bad refl = refl

@0 subst-bad-[]-cong :
  (eq : A ≡ B) →
  subst (λ A → A) (bad ([]-cong eq)) x ≡
  subst (λ A → A) eq x
subst-bad-[]-cong {x} refl =
  cong (λ eq → subst (λ A → A) (bad eq) x) []-cong-refl

@0 subst-bad-[]-cong-univ :
  (A≃B : A ≃ B) →
  subst (λ A → A) (bad ([]-cong (from-path (univ A≃B)))) x ≡
  A≃B .fst x
subst-bad-[]-cong-univ A≃B =
  trans (subst-bad-[]-cong (from-path (univ A≃B)))
    (trans (subst-cast (univ A≃B))
       (cong (λ eq → eq .fst _) (from-path (univ-β A≃B))))

------------------------------------------------------------------------
-- IO

postulate
  putStrLn : String → IO ⊤

{-# FOREIGN GHC import qualified Data.Text.IO #-}
{-# COMPILE GHC putStrLn = Data.Text.IO.putStrLn #-}

------------------------------------------------------------------------
-- A boolean

-- When the non-strict GHC backend is used, then this code is compiled
-- to (roughly) "unsafeCoerce True".

should-be-false : Bool
should-be-false =
  subst (λ A → A) (bad ([]-cong (from-path (univ not-equiv)))) true

is-false : should-be-false ≡ false
is-false = Bool-stable (subst-bad-[]-cong-univ not-equiv)

-- When this program is run the string "true" is printed.

main : IO ⊤
main = putStrLn (show should-be-false)

The code uses some postulates, but I expect that all the postulates except for putStrLn can be implemented.

Note that Agda complains about bad:

warning: -W[no]UnsupportedIndexedMatch
This clause uses pattern-matching features that are not yet
supported by Cubical Agda, the function to which it belongs will
not compute when applied to transports.

Reason: It relies on injectivity of the data constructor [_], which
        is not yet supported

when checking the definition of bad

I suspect that (for options other than --without-K) the problem is that Agda does not generate any extra clauses for bad: hopefully the generated clauses would be rejected by Agda. One can perhaps fix this problem temporarily by making the UnsupportedIndexedMatch warning incompatible with --safe, and also incompatible with compilation. However, note that this warning is not raised when --without-K is used. There is a check that is intended to make sure that code that is accepted when --without-K is used is also accepted when --cubical-compatible is used. If that check can be extended so that bad is rejected, then the check can perhaps be used also for the other options (--cubical-compatible, --erased-cubical and --cubical).

[nad]

Agda rejects the following code:

{-# OPTIONS --safe --cubical-compatible --erasure #-}

data _≡_ {@0 a} {@0 A : Set a} (@0 x : A) : A → Set a where
  refl : x ≡ x

x ≡ x is not usable at the required modality @ω
when checking the constructor refl in the declaration of _≡_

However, the following pieces of code are allowed:

{-# OPTIONS --safe --cubical-compatible --erasure #-}

data _≡′_ {@0 a} {@0 A : Set a} (x : A) : @0 A → Set a where
  refl : x ≡′ x

{-# OPTIONS --safe --cubical-compatible --erasure #-}

data _≡″_ {@0 a} {@0 A : Set a} (@0 x : A) : @0 A → Set a where
  refl : x ≡″ x

I experimented a little with these definitions. One can currently prove that x ≡′ y and x ≡″ y are equivalent to [ x ] ≡ [ y ] (without any warnings):

{-# OPTIONS
      --safe --cubical-compatible --erasure --hidden-argument-puns #-}

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

private variable
  a p   : Level
  A     : Set a
  x y z : A

------------------------------------------------------------------------
-- Some definitions related to the builtin equality type

-- The J rule. This is the only definition in this file that matches
-- directly on refl for _≡_.

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

-- Substitutivity.

subst :
  ∀ {@0 a} {@0 A : Set a} {x y : A}
  (P : A → Set p) → x ≡ y → P x → P y
subst P eq p = J (λ x _ → P x) p eq

-- Transitivity.

trans : x ≡ y → y ≡ z → x ≡ z
trans {x} eq₁ eq₂ = subst (λ y → x ≡ y) eq₂ eq₁

------------------------------------------------------------------------
-- Erased

-- A definition of Erased without definitional η-equality.

data Erased {@0 a} (@0 A : Set a) : Set a where
  [_] : @0 A → Erased A

-- A projection.

@0 erased : Erased A → A
erased [ x ] = x

-- Propositional η-expansion.

η : ∀ {@0 a} {@0 A : Set a} {x : Erased A} → x ≡ [ erased x ]
η {x = [ _ ]} = refl

------------------------------------------------------------------------
-- An alternative definition of equality

-- Note that all arguments are erased except for the last parameter.
-- Everything still works if this parameter is made erased.

data _≡′_ {@0 a} {@0 A : Set a} (x : A) : @0 A → Set a where
  refl : x ≡′ x

-- The J rule. This is the only definition in this file that matches
-- directly on refl for _≡′_.

J′ :
  ∀ {@0 a} {@0 A : Set a} {@0 x y : A}
  (P : (@0 y : A) → x ≡′ y → Set p) →
  P x refl →
  (eq : x ≡′ y) →
  P y eq
J′ _ p refl = p

-- Substitutivity.

subst′ :
  ∀ {@0 a} {@0 A : Set a} {@0 x y : A}
  (P : @0 A → Set p) → x ≡′ y → P x → P y
subst′ P eq p = J′ (λ x _ → P x) p eq

-- A lemma used to implement []-injective′.

cong-erased′ :
  {@0 A : Set a} {x : A} {@0 y : Erased A} →
  [ x ] ≡′ y → x ≡′ erased y
cong-erased′ {x} eq = subst′ (λ y → x ≡′ erased y) eq refl

-- The constructor [_] is injective up to _≡′_.

[]-injective′ :
  {@0 A : Set a} {x : A} {@0 y : A} →
  [ x ] ≡′ [ y ] → x ≡′ y
[]-injective′ = cong-erased′

------------------------------------------------------------------------
-- Converting between _≡_ and _≡′_

-- One can convert directly from _≡_ to _≡′_.

≡→≡′ : {@0 A : Set a} {x y : A} → x ≡ y → x ≡′ y
≡→≡′ {x} eq = subst (λ y → x ≡′ y) eq refl

-- There is a bijective correspondence between x ≡′ y and
-- [ x ] ≡ [ y ].

to : {@0 A : Set a} {@0 x y : A} → x ≡′ y → [ x ] ≡ [ y ]
to {x} eq = subst′ (λ y → [ x ] ≡ [ y ]) eq refl

from : {@0 A : Set a} {x : A} {@0 y : A} → [ x ] ≡ [ y ] → x ≡′ y
from eq = []-injective′ (≡→≡′ eq)

from-to :
  {@0 A : Set a} {x : A} {@0 y : A}
  (eq : x ≡′ y) → from (to eq) ≡ eq
from-to = J′ (λ y eq → from (to eq) ≡ eq) refl

to-from :
  {@0 A : Set a} {x : A} {@0 y : A}
  (eq : [ x ] ≡ [ y ]) → to (from eq) ≡ eq
to-from = lemma
  where
  lemma :
    {@0 A : Set a} {x : A} {y : Erased A}
    (eq : [ x ] ≡ y) →
    subst′ (λ y → [ x ] ≡ [ y ]) (cong-erased′ (≡→≡′ eq)) refl ≡
    trans eq η
  lemma {x} =
    J (λ y eq →
         subst′ (λ y → [ x ] ≡ [ y ]) (cong-erased′ (≡→≡′ eq)) refl ≡
         trans eq η)
      refl

Hopefully it is not possible to prove that x ≡′ y (or x ≡″ y) implies x ≡ y, because then the type [ x ] ≡ [ y ] → x ≡ y would be inhabited.

[nad]

One can perhaps fix this problem temporarily by making the UnsupportedIndexedMatch warning incompatible with --safe, and also incompatible with compilation. However, note that this warning is not raised when --without-K is used. There is a check that is intended to make sure that code that is accepted when --without-K is used is also accepted when --cubical-compatible is used. If that check can be extended so that bad is rejected, then the check can perhaps be used also for the other options (--cubical-compatible, --erased-cubical and --cubical).

What do you think, should we make UnsupportedIndexedMatch incompatible with --safe and compilation?

[jespercockx]

This is not a regression, so it can wait until the next release.