Comportamiento incoherente de Coq con respecto a los parámetros implícitos de las definiciones de Let

Question

He encontrado algún tipo de comportamiento incoherente de Coq con respecto a los parámetros implícitos.

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. 

La definición id1Let no parece hacer t implícita, mientras que cuando se reemplaza la Let por Definition se produce ningún error. ¿Tengo algo mal o es esto un error?

Answer 1

Creo que esto es un error, sí. La notación para declarar un argumento implícito se ignora en el caso de id1, como se puede ver con el comando Print Implicit id1.