PHOAS in Coq：タイプの不一致

Question

私はCoqで2008 PHOAS paperセクション2.1から（非公式の）定義を転記しています。

Inductive tm' {V : Set} : Set := 
| Var : V -> tm' 
| App : tm' -> tm' -> tm' 
| Abs : (V -> tm') -> tm'. 

Definition tm := forall X, @tm' X. 

Fail Example id : tm := Abs Var. 

出力：

The term "Abs Var" has type "tm'" while it is expected to have type "tm". 

むしろ不愉快です。どのようにしてこのコードタイプチェックを行うことができますか？

Example id : tm := fun _ => Abs Var. 

問題は、あなたがラムダ（fun）なし（タイプforallの何かを）機能を構築しようとしていたということです。ここで

Answer 1

は動作するコードです。

Answer 2

Example id : tm := fun (X : Set) => Abs Var.