[Agda] Abusing the GADT syntax

[Shin-Cheng Mu]

Hi,

The following definition of accessibility is perhaps
not too unfamiliar by people here:

   Rel : Set -> Set -> Set1
   Rel B A = A -> B -> Set

   data Acc {A : Set}(R : Rel A A) : A -> Set where
     acc : (x : A) -> (forall y -> R x y -> Acc R y) -> Acc R x

The expression:

   (x : A) -> (forall y -> R x y -> Acc R y) -> Acc R x    (1)

Can be factored into some operators defined by Doornbos
and Backhouse. With the definitions of _⊆_ and _⍀_ given
below, (1) equals (2):

   (R ⍀ Acc R) ⊆ Acc R                                     (2)

Well, it takes a long story to explain (2) (in short,
_⊆_ is set inclusion and _⍀_  is what Backhouse calls a
"monotype factor). Anyway, I tried in Agda:

   data Acc {A : Set}(R : Rel A A) : A -> Set where
     acc : (R ⍀ Acc R) ⊆ Acc R                             (3)

and happily found that Agda allows the definition above.
I can even define some functions pattern matching acc:

   acc-fold : <blah blah blah>
   acc-fold ... (acc x h) = <no problem!>

Problem happens when I tried to perform "with":

   test : {A B : Set} -> (f : B -> B)
                -> (b : B) -> Acc (rel f) b -> B
   test f b (acc .b h) with f b
   ...| _ = {! !}

It is at this moment when Agda complained:

   The constructor acc expects 0 arguments, but has been given 2

Is it a bug? Or is it a bug to allow (3) in the first
place? I would certainly prefer that Agda does allow (3). :)

Sample code attached below.

sincerely,
Shin

\begin{code}

module Q where

open import Relation.Binary.PropositionalEquality

Rel : Set -> Set -> Set1
Rel B A = A -> B -> Set

_⊆_ : {A : Set} -> (A -> Set) -> (A -> Set) -> Set
r ⊆ s = forall a -> r a -> s a

_⍀_ : {A B : Set} -> Rel B A -> (B -> Set) -> (A -> Set)
(R ⍀ P) a = forall b -> R a b -> P b

data Acc {A : Set}(R : Rel A A) : A -> Set where
   acc : (R ⍀ Acc R) ⊆ Acc R

-- was:
--  acc : (x : A) -> (forall y -> R x y -> Acc R y) -> Acc R x

-- Agda is happy with this function:

acc-fold : {a : Set} (R : Rel a a) {P : a -> Set} ->
     ((x : a) -> (forall y -> R x y -> P y) -> P x) ->
        (x : a) -> (accx : Acc R x) -> P x
acc-fold R {P} f x (acc .x h) = f x (\y yRx -> acc-fold R f y (h y yRx))

rel : {A B : Set} -> (A -> B) -> (A -> B -> Set)
rel f a b = f a ≡ b

-- but not this one:

test : {A B : Set} -> (f : B -> B)
              -> (b : B) -> Acc (rel f) b -> B
test f b (acc .b h) with f b
...| _ = {! !}

\end{code}