[Agda] Help with understanding REWRITE

[Andrew M. Pitts]

I’m struggling to understand an aspect of --rewriting in Agda (2.6.1) and wonder if someone can help?

The following artificial example illustrates my problem (which is more complicated and less artificial).

---
{-# OPTIONS --rewriting #-}

open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

data C (S : Set) : Set₁ where
  mkC :
    (A : Set)
    (e : A ≡ S)
    → ---------
    C S

Cset : (S : Set) → C S → Set
Cset S (mkC A e) = A

Cequ : (S : Set)(c : C S) → Cset S c ≡ S
Cequ S (mkC A e) = e

{-# REWRITE Cequ #-} — this is not accepted!

——

Given S : Set, the datatype C S contains values given by a set A and a proof that A equals S. Can we make that proof definitional rather than propositional, using a REWRITE? Apparently not — if you check the above Agda code, Agda 2.6.1 complains

-- Cequ is not a legal rewrite rule, since the following variables are
-- not bound by the left hand side: S
-- when checking the pragma REWRITE Cequ

The “left-hand side” it refers to is Cset S c, which certainly contains an occurrence of S. Why is S not “bound by” this left-hand side? I declared the type of Cequ to be

(S : Set)(c : C S) → Cset S c ≡ S

bu Agda 2.6.1 reports it to be

(S : Set) (c : C S) → Cset _ c ≡ S

Note the underscore. Presumably this is why REWRITE Cequ is not accepted.

Where did that underscore come from? And is there some way to avoid it and have the REWRITE accepted?

Andy