[Agda] Questions regarding non-constructor indexed datatypes

[Shin-Cheng Mu]

Hi,

Some more novice questions. :)

I was playing with the following implementation of a queue
using a pair of vectors:

   data Queue {a : Set} : forall {n} -> Vec a n -> Set where
     queue : forall {m n} ->
              (l : Vec a m) -> (r : Vec a n) ->
                Queue (l ++ reverse r)

The intention is that Queue xs is a queue whose content is
the vector xs, split into l and r such that xs = l ++ reverse r.

For this implementaiton of Queue, I am able to define, for
example, the following function enqueue:

   enqueue : forall {a n} {xs : Vec a n} ->
               (x : a) -> Queue xs -> Queue (x ∷ xs)
   enqueue x (queue l r) = queue (x ∷ l) r

However, when I tried to define:

   dequeue : forall {a k} {xs : Vec a (suc k)} ->
               Queue xs -> (Queue (init xs) × a)
   dequeue (queue {i} {j} l []) = ?
   dequeue (queue l (r ∷ rs)) = ?

Agda highlighted the part "queue {i} {j} l []" and gave me
the error message:

   m + n != suc k of type ℕ
   when checking that the pattern queue {i} {j} l [] has type
   Queue xs

Question 1: I guess the problem is that Agda tries to unify
   i + j with suc k. In the case of enqueue, length l + length r
   is unified with n, which poses no problem. It is not the
   case with dequeue.

   However, Agda refers to m and n, rather than i and j, so my
   guess may be wrong. If so, what is going on here?

Question 2: What is the suggested approach to resolve the
   problem above?

Question 3: The following function queue-eq (which proves
   that if xs equals ys, then Queue xs can be cast to Queue ys)
   passes the type checker:

     queue-eq : forall {a n₁ n₂} {xs₁ : Vec a n₁} {xs₂ : Vec  
a n₂} ->
               xs₁ ≈ xs₂ -> Queue xs₁ -> Queue xs₂
     queue-eq eq (queue l r) with length-equal eq
     ... | ≡-refl = ≅-subst Queue (to-≅ eq) (queue l r)

   However, if I mention an implicit argument:

     queue-eq {_}{n₁} eq (queue l r) with length-equal eq
     ... | ≡-refl = ≅-subst Queue (to-≅ eq) (queue l r)

   The typecheck fails with a message similar to the one above:

     m + n != n₁ of type ℕ
     when checking that the pattern queue l r has type Queue xs₁

   Why does simply mentioning the argument make a difference?

Thanks!

sincerely,
Shin