Why we should revert stdlib to --without-K instead of using --cubical-compatible #2792
Description
Here is a minimal example of the ills that we get with --cubical-compatible that we don't with --without-K:
{-# OPTIONS --cubical-compatible --safe #-}
module MWE where
open import Data.Nat.Base using (ℕ; _≤_; z≤n; s≤s)
open import Data.Vec.Base using (Vec; _∷_; zipWith; truncate)
open import Level using (Level)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
private
variable
a b c : Level
A : Set a
B : Set b
C : Set c
m n : ℕ
truncate-zipWith : (f : A → B → C) (m≤n : m ≤ n) (xs : Vec A n) (ys : Vec B n) →
zipWith f (truncate m≤n xs) (truncate m≤n ys) ≡ truncate m≤n (zipWith f xs ys)
truncate-zipWith f z≤n xs ys = refl
truncate-zipWith f (s≤s m≤n) (x ∷ xs) (y ∷ ys) = cong (f x y ∷_) (truncate-zipWith f m≤n xs ys)If you try to load that, you get the following warnings:
/Users/carette/Downloads/MWE.agda:20,1-22,49
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 ℕ.suc,
which is not yet supported
when checking the definition of truncate-zipWith
/Users/carette/Downloads/MWE.agda:20,1-22,49
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 ℕ.suc,
which is not yet supported
when checking the definition of truncate-zipWith
Of course, I could shrink the example further to trigger the warning -- any pattern matching on _≤_ will do that. The above is a real example drawn from real code.
Basically the proof idiom above is a perfectly good one to use in stdlib and should give no warnings. Nothing in Cubical Agda should interfere with stdlib -- but it does.
I think that until agda itself is fixed, we should go back to --without-K.
Pinging @andreasabel who made the original change in the other direction.