Do we really want special case casts? (was: [Agda] Proof involving associativity of ++ of vectors)

[Samuel Gélineau]

Wait a minute... why do we need special case casts? Couldn't we define
dependent versions of subst and cong once and for all? Of course we
can.


dependent-subst : {a : Set}{b : a → Set}
                → (P : ∀ x → b x → Set)
                → {x₁ : a}{y₁ : b x₁}
                → {x₂ : a}{y₂ : b x₂}
                → x₁ ≅ x₂
                → y₁ ≅ y₂
                → P x₁ y₁
                → P x₂ y₂
dependent-subst P refl refl p = p

dependent-cong : {a : Set}{b : a → Set}
               → {c : ∀ x → b x → Set}
               → (f : ∀ x y → c x y)
               → {x₁ : a}{y₁ : b x₁}
               → {x₂ : a}{y₂ : b x₂}
               → x₁ ≅ x₂
               → y₁ ≅ y₂
               → f x₁ y₁
               ≅ f x₂ y₂
dependent-cong f refl refl = refl


Unfortunately, these versions have a major disadvantage compared to
special case casts: they require an extra proof that (x₁ ≅ x₂). With
special case casts, this equality is inferred from refl.


List = Vec ℕ

list-subst : (P : ∀ x → List x → Set)
           → {x₁ : ℕ}{y₁ : List x₁}
           → {x₂ : ℕ}{y₂ : List x₂}
           → y₁ ≅ y₂
           → P x₁ y₁
           → P x₂ y₂
list-subst P refl p = p

list-cong : {c : ∀ x → List x → Set}
          → (f : ∀ x y → c x y)
          → {x₁ : ℕ}{y₁ : List x₁}
          → {x₂ : ℕ}{y₂ : List x₂}
          → y₁ ≅ y₂
          → f x₁ y₁
          ≅ f x₂ y₂
list-cong f refl = refl


Here is a shorter example illustrating the difference.


cong-len : ∀ {n m}
         → {xs : List n}
         → {ys : List m}
         → xs ≅ ys
         → n ≅ m
cong-len refl = refl

cong-arg : ∀ {n m}
         → (C : ℕ → Set)
         → {xs : C n}
         → {ys : C m}
         → xs ≅ ys
         → n ≅ m
cong-arg C refl = refl -- error
-- n != m of type ℕ
-- when checking that the pattern refl has type xs ≅ ys


refl implies (C n = C m), but that doesn't imply (n = m) because C
could be a function, which could easily return the same value given
distinct n and m. Vec, however, and by extension also List, is a type
constructor constant, and as such it always returns distinct types
given distinct argument. But whenever we wish to write a proof
involving the fact that some name is a type constant, we must write a
special case proof. I think it would be much better if, somehow, type
constructor constants were distinguished from arbitrary functions like
C. The key distinction, I think, is that Vec and List are neutral
terms, whereas C could by either normal or neutral.

Feature request: there should be a way to quantify over neutral terms only!

– Samuel