Comportement incohérent de Coq concernant les paramètres implicites de Laisser définitions

Question

J'ai trouvé une sorte de comportement incohérent de Coq concernant les paramètres implicites.

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 définition Letid1 ne semble pas faire t implicite, alors que lorsque vous remplacez la Let par Definition aucune erreur se produit. Est-ce que j'ai un problème ou est-ce un bug?

Answer 1

Je pense que c'est un bug, oui. La notation pour déclarer un argument implicite est ignorée dans le cas de id1, comme vous pouvez le voir avec la commande Print Implicit id1.