Defining lambda from Ast

[hfehrmann]

The following code fails with "Universe Var(0) undefined":

Definition f@{i j k} := fun (E:Type@{i}) => TypeVal@{i k} E (type@{i j} E) (TypeErr@{i j} E).
Quote Definition qf := Eval cbv in f. (* To expands definition *)
(*
qf = 
tLambda (nNamed "E") (tSort [(Level.Level "Top.257", false)])
  (tApp
     (tConstruct {| inductive_mind := "Top.type"; inductive_ind := 0 |} 0
        [Level.Level "Top.257"; Level.Level "Top.259"])
     [tRel 0;
     tApp
       (tInd {| inductive_mind := "Top.type"; inductive_ind := 0 |}
          [Level.Level "Top.257"; Level.Level "Top.258"]) [tRel 0];
     tApp
       (tConstruct {| inductive_mind := "Top.type"; inductive_ind := 0 |} 1
          [Level.Level "Top.257"; Level.Level "Top.258"]) [tRel 0]])
     : term
*)
Make Definition uqf := Eval cbv in qf.

It would be nice if the following is accepted:

Make Definition uqf := 
tLambda (nNamed "E") (tSort [(Level.Var 0, false)])
  (tApp
     (tConstruct {| inductive_mind := "Top.type"; inductive_ind := 0 |} 0
        [Level.Var 0; Level.Var 2])
     [tRel 0;
     tApp
       (tInd {| inductive_mind := "Top.type"; inductive_ind := 0 |}
          [Level.Var 0; Level.Var 1]) [tRel 0];
     tApp
       (tConstruct {| inductive_mind := "Top.type"; inductive_ind := 0 |} 1
          [Level.Var 0; Level.Var 1]) [tRel 0]])

Declaring new universes for every Var.

The inductive type is polymorphic, so to my understanding I have to give the universe instance. Therefore, it should be possible te generate fresh universes variables.

[SimonBoulier]

Yes, unquote of polymorphic constants was not implemented. @loic-p is on it!