From 4fa8ed55eaa0a18a3aa68a56c12939c0496015f8 Mon Sep 17 00:00:00 2001
From: MathisBD <mathis.bouverot@ens.psl.eu>
Date: Mon, 4 Nov 2024 12:36:51 +0100
Subject: [PATCH] initial commit

---
 template-coq/src/run_template_monad.ml | 19 +++++++++++++------
 test-suite/unquote_evars.v             | 20 ++++++++++++++++++++
 2 files changed, 33 insertions(+), 6 deletions(-)
 create mode 100644 test-suite/unquote_evars.v

diff --git a/template-coq/src/run_template_monad.ml b/template-coq/src/run_template_monad.ml
index 99e13bc73..78b70c99f 100644
--- a/template-coq/src/run_template_monad.ml
+++ b/template-coq/src/run_template_monad.ml
@@ -538,17 +538,21 @@ let rec run_template_program_rec ~poly ?(intactic=false) (k : Constr.t Plugin_co
   | TmUnquote t ->
     begin
        try
-         debug Pp.(fun () -> str"Unquoting:" ++ Printer.pr_constr_env env evm t);
-         let t = reduce_all env evm t in
-         let evm, t' = denote_term env evm t in
-         let typ = Retyping.get_type_of env evm (EConstr.of_constr t') in
+         (*debug Pp.(fun () -> str"Unquoting:" ++ Printer.pr_constr_env env evm t);*)
+         let evm, t' = denote_term env evm (reduce_all env evm t) in
+         (* Typecheck. *)
+         let evm, typ = Typing.type_of env evm (EConstr.of_constr t') in
          let evm, typ = Evarsolve.refresh_universes (Some false) env evm typ in
+         (* Solve evars. *)
+         let evm = Typeclasses.resolve_typeclasses env evm in
+         let t' = Evarutil.nf_evars_universes evm t' in
+         (* Package the unquoted term with its type. *)
          let make_typed_term typ term evm =
            match Lazy.force texistT_typed_term with
            | GlobRef.ConstructRef ctor ->
               let (evm,c) = Evd.fresh_global (Global.env ()) evm (Lazy.force texistT_typed_term) in
               let term = Constr.mkApp
-               (EConstr.to_constr evm c, [|EConstr.to_constr evm typ; t'|]) in
+               (EConstr.to_constr evm c, [|EConstr.to_constr ~abort_on_undefined_evars:false evm typ; t'|]) in
              let evm, _ = Typing.type_of env evm (EConstr.of_constr term) in
                (env, evm, term)
            | _ -> CErrors.anomaly (str "texistT_typed_term does not refer to a constructor")
@@ -559,8 +563,11 @@ let rec run_template_program_rec ~poly ?(intactic=false) (k : Constr.t Plugin_co
       end
   | TmUnquoteTyped (typ, t) ->
        let evm, t' = denote_term env evm (reduce_all env evm t) in
-       (* let t' = Typing.e_solve_evars env evdref (EConstr.of_constr t') in *)
+       (* Typecheck. *)
        let evm = Typing.check env evm (EConstr.of_constr t') (EConstr.of_constr typ) in
+       (* Solve evars. *)
+       let evm = Typeclasses.resolve_typeclasses env evm in 
+       let t' = Evarutil.nf_evars_universes evm t' in
        k ~st env evm t'
   | TmFreshName name ->
     let name = reduce_all env evm name in
diff --git a/test-suite/unquote_evars.v b/test-suite/unquote_evars.v
new file mode 100644
index 000000000..fa80bc96d
--- /dev/null
+++ b/test-suite/unquote_evars.v
@@ -0,0 +1,20 @@
+From MetaCoq.Template Require Import All.
+Import MCMonadNotation.
+
+(* Unquoting evars. *)
+MetaCoq Run (mlet t <- tmUnquote (tEvar fresh_evar_id []) ;; tmPrint t).
+MetaCoq Run (mlet t <- tmUnquoteTyped nat (tEvar fresh_evar_id []) ;; tmPrint t).
+
+(* Unquoting evars, with typeclass resolution. *)
+Existing Class nat.
+Existing Instance O.
+
+MetaCoq Quote Definition quoted_nat := nat.
+MetaCoq Run (
+  mlet t <- tmUnquote (tCast (tEvar fresh_evar_id []) Cast quoted_nat) ;;
+  tmEval cbv t
+).
+MetaCoq Run (
+  mlet t <- tmUnquoteTyped nat (tEvar fresh_evar_id []) ;;
+  tmEval cbv t
+).
\ No newline at end of file