The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

Stéphane Lescuyer a écrit :
> Note that the intermediary pattern variable 'a' (introduced
> explicitely by Russell's variant, and not in the original version)
> actually appears in the arguments of vall. If you try a version of
> terms where the length does not depend on the symbol, say :
>
> Record signature : Type := mk_signature  {
>   symbol : Set;
>   arity : nat
> }.
> Inductive term (S: signature): Type :=
> | term_app: forall a: symbol S, vector (term S) (arity S) -> term S.
>
> Then your original definition works fine.
>
> I don't know quite what to make of it, but this definitely looks like
> a bug and gives a good hint as to where to start investigating.
>
> Stephane

Hi,

This is not exactly a bug.
match tries to be smart when matching on constructor arguments upon 
which further arguments depend. Here, the type of cs depends on a. When 
you match on a (by deep matching on c), the match macro automatically 
generalizes cs so that its type gets more precise. As the error message 
says, the expanded fixpoint body (of Aaron's attempt) is:

fun (S : signature) (c : context S) =>
 match c with
 | term_app a0 cs =>
     match a0 with
     | Some a =>
         fun cs0 =>
          @vall (context S) (no_hole S)
           (arity (context_signature S) (@Some (symbol S) a)) cs0
     | None => fun _ => False
     end cs
 end

Unfortunately, this generalization-match-then-introduction is too much 
for the termination-checker: it cannot see that cs0 is actually the same 
vector as cs.

By splitting the match as Russell did, this automatic generalization is 
not done, so recursive calls are really made on cs, which is accepted.

If you really need the most precise type for cs (this is not the case 
here), then you could make the match on a0 generate equality (a0 = Some 
a) and rewrite the type of cs (the guard condition knows that (match e 
return ... with refl_equal => cs end) has the same size as cs). I must 
admit this is quite painful to do by hand.

Hope this helps,
Bruno Barras.