Typecheck the result of term unquotation.

In some cases, unquoting could generate terms that were ill-typed, typically
when unquoting [I @hole] for some template polymorphic inductive type [I].
Similarly universe levels were not computed at all, which could have led
to bizarre failures.

To ensure that the unquoted term makes sense at all, we simply perform a
call to Typing before returning it. This has a non-trivial cost but since
building the term is already linear, this should not hopefully matter that
much in practice.

Author: ppedrot

template-coq/src/denoter.ml

@@ -174,6 +174,9 @@ struct
           let evm, ty = aux env evm ty in
           evm, Constr.mkArray (UVars.Instance.of_array ([||], [|u|]), arr, def, ty)
 
-    in aux env evm trm
+    in
+    let evm, trm = aux env evm trm in
+    let evm, _ = Typing.type_of env evm (EConstr.of_constr trm) in
+    evm, trm
 
 end