Coq關於隱含參數的不一致行爲Let定義

Question

我發現Coq關於隱式參數的某種不一致行爲。

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. 

的Let定義id1似乎並沒有使t含蓄， 而當你通過Definition沒有出現錯誤更換Let。 我有什麼不對或這是一個錯誤？

Answer 1

我認爲這是一個錯誤，是的。使用Print Implicit id1命令可以看到，在id1的情況下，將忽略用於聲明隱式參數的符號。