Why can't I define the following CoFixpoint?

I am using:

$ coqtop -v
The Coq Proof Assistant, version 8.4pl5 (February 2015)
compiled on Feb 06 2015 17:44:41 with OCaml 4.02.1

I defined the following CoInductive type, stream:

$ coqtop
Welcome to Coq 8.4pl5 (February 2015)

Coq < CoInductive stream (A : Type) : Type := 
Coq < | Cons : A -> stream A -> stream A.
stream is defined

Coq < Check stream.
stream
     : Type -> Type

Coq < Check Cons.
Cons
     : forall A : Type, A -> stream A -> stream A

Then, I tried to define the following CoFixpoint definition, zeros:

Coq < CoFixpoint zeros : stream nat := Cons 0 zeros.

However, I got the following error instead:

Toplevel input, characters 38-39:
> CoFixpoint zeros : stream nat := Cons 0 zeros.
>                                       ^
Error: In environment
zeros : stream nat
The term "0" has type "nat" while it is expected to have type 
"Type".

I figured out that I have to explicitly instantiate the variable A:

Coq < CoFixpoint zeros : stream nat := Cons nat 0 zeros.
zeros is corecursively defined

Why doesn't the Coq infer the type of A by itself? How do I make it infer the type of A?

Solution

You need to declare A as implicit to ask Coq to infer it for you. There are a few ways of doing it:

Add the following declaration to your file: Set Implicit Arguments.. This will cause Coq to turn on automatic inference for arguments such as A for Cons, allowing you to write Cons 0 zeros.
Turn on implicit arguments just for Cons, without affecting the rest of the file:
```
Arguments Cons {A} _ _.
```
This declaration marks A as implicit and leaves the other two arguments as explicit.
Mark A as implicit in the definition of stream:
```
CoInductive stream {A : Type} : Type := 
| Cons : A -> stream A -> stream A.
```
I personally do not recommend doing this, however, as it will mark A as implicit for stream as well.

You can find more information about implicit arguments in the reference manual