The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Adam Megacz wrote:
> Adam 
> Chlipala<adam AT chlipala.net>
>   writes:
>    
> > I think your function definition has a typo, where the last two
> > recursive arguments to [next] are reversed.
> >      
> No, I really did mean to put them in that order.
>
> Changing the order of the arguments certainly gives you something that
> type-checks, but it's a different program which no longer illustrates
> the problem.
>    

The order you chose couldn't possibly work.  Even if this were a Lisp 
program and we treated types as predicates proved after-the-fact, the 
program you gave couldn't "type-check" at the type you gave.