The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

Hi Bruno,

Thank you for your explanation, this makes perfect sense indeed, once
you know what's going on under the hood. The issue here is how do you
know the expression which is actually fed to the typechecker ? My
error message only shows the typing context and not the whole fixpoint
body :

Recursive definition of no_hole is ill-formed.
In environment
no_hole : forall S : signature, context S -> Prop
S : signature
c : context S
...
Recursive call to no_hole has principal argument equal to
"a1" instead of cs.

So I can actually see the two cs, cs0 and the corresponding a, a0
which can help understand what's going on, but is there any option
that I'm unaware of which displays the whole fixpoint body ? That
would be pretty useful in such circumstances.

Stéphane L.


2009/9/22 Bruno Barras 
<bruno.barras AT inria.fr>:
> 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.
>
>
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06