Inconsistent behavior of Coq concerning implicit parameters of Let definitions

Question

I've found some kind of inconsistent behavior of Coq concerning implicit parameters.

Section foo.
  Let id1 {t : Set} (x : t) := x.
  Let id2 {t : Set} (x : t) : t. assumption. Qed.
  Check id2 (1:nat).
  Check id1 (1:nat). (* Fails with "The term "1:nat" has type "nat" while it is expected to have type "Set"." *)
End foo.

The Let definition id1 does not seem to make t implicit, whereas when you replace the Let by Definition no error occurs. Have I got something wrong or is this a bug?

Answer 1

I think this is a bug, yes. The notation for declaring an implicit argument is being ignored in the case of id1, as you can see with the Print Implicit id1 command.