PHOAS in Coq: type mismatch

Question

I'm transcribing in Coq the (informal) definitions from the 2008 PHOAS paper, section 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.

Output:

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

That's rather obnoxious. How can I make this code type-check?

Answer 1

Here is code that works:

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

The issue is that you were trying to construct a function (something of type forall) without a lambda (fun).

Answer 2

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