The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Rohit Persaud wrote:
> Now when i define the function :
>
>    Fixpoint Pol_eq (I J: T) (i : POLY I J) {struct i} :  POLY I J -> 
> bool :=
>      match i in POLY _ e return (POLY _ e -> bool)   with
>      | PA n => fun _ => true
>      | PProdI _ _ Ia Ib =>    fun _ => true
>      | Punit   => fun _ => true                  
>      | PSum1 X Y Ib => fun x => 
>                      match polyys x with
>                      | pleft pl => EqSum (Pol_eq (I := I) (J :=  X)) 
> Ib pl
>                      |  _       => false
>                      end
>      | PSum2 X Y Ib => fun _ => true
>     end.
>    ( * note  the implementations at the branches are replaced by true 
> for brevity *)
>  
>  I get the following error "Recursive call to Pol_eq had not enough 
> arguments " . Shouldn't this function be fine?

No, it shouldn't be fine.  Any call to a recursive function must include 
the recursive argument explicitly, since this is needed for termination 
checking.

>  Is there any way around this.

I haven't followed the details of what you're trying to do, but it seems 
plausible that your function might be primitive-recursive in either [I] 
or [J].  You could try changing the [struct] annotation to reflect 
that.  This might require more dependent types tricks than you have now.