The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

> > Inference of "i" in poly_in seems to work for me in (at least) 8.3pl2.
> 
> I meant that while I can do
> 
> Compute poly_in 0 tt.
>      = 0
> 
> I can't do
> 
> Compute poly_in _ tt.
>                   ^^
> Error: The term "tt" has type "unit" while it is expected to have type
>  "match ?22 with
>   | 0 => unit
>   | S _ => nat
>   end".

Indeed, equations of the form "match ? with ... end = something", even
the ones with a simple unique solution as in your case, are not (yet)
treated by the type inference algorithm of Coq. Note that if you had
written "poly_in _ 0", then, there would have been countably many
solutions though!

Hugo Herbelin