From 818403f4064a0aecbd316f239127a67b8cbfe34c Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 12 Oct 2009 14:22:34 +0000
Subject: [PATCH] Closed metas must have closed (expected) types.

---
 .../components/ng_refiner/nCicRefiner.ml      | 41 +++++++++++++++----
 1 file changed, 32 insertions(+), 9 deletions(-)

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 225c1898e..b88e261f1 100644
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -47,14 +47,34 @@ let wrap_exc msg = function
   | e -> raise e
 ;;
 
-let exp_implicit ~localise metasenv context expty t =
- let foo x = match expty with Some t -> `WithType t | None -> x in
+let exp_implicit rdb ~localise metasenv subst context expty t =
+ let foo x = function Some t -> `WithType t | None -> x in
  function      
-  | `Closed -> NCicMetaSubst.mk_meta metasenv [] (foo `Term)
-  | `Type -> NCicMetaSubst.mk_meta metasenv context (foo `Type)
-  | `Term -> NCicMetaSubst.mk_meta metasenv context (foo `Term)
+  | `Closed ->
+      let metasenv,subst,expty =
+       match expty with
+          None -> metasenv,subst,None
+        | Some typ ->
+           let (metasenv,subst),typ =
+            try
+             NCicMetaSubst.delift
+              ~unify:(fun m s c t1 t2 ->
+                try Some (NCicUnification.unify rdb m s c t1 t2)
+                with NCicUnification.UnificationFailure _ | NCicUnification.Uncertain _ -> None)
+              metasenv subst context 0 (0,NCic.Irl 0) typ
+            with
+              NCicMetaSubst.MetaSubstFailure _
+            | NCicMetaSubst.Uncertain _ ->
+               raise (RefineFailure (lazy (localise t,"Trying to create a closed meta with a non closed type")))
+
+           in
+            metasenv,subst,Some typ
+      in
+       NCicMetaSubst.mk_meta metasenv [] (foo `Term expty),subst
+  | `Type -> NCicMetaSubst.mk_meta metasenv context (foo `Type expty),subst
+  | `Term -> NCicMetaSubst.mk_meta metasenv context (foo `Term expty),subst
   | `Tagged s ->
-      NCicMetaSubst.mk_meta ~attrs:[`Name s] metasenv context (foo `Term)
+      NCicMetaSubst.mk_meta ~attrs:[`Name s] metasenv context (foo `Term expty),subst
   | `Vector ->
       raise (RefineFailure (lazy (localise t, "A vector of implicit terms " ^
        "can only be used in argument position")))
@@ -165,8 +185,8 @@ let rec typeof rdb
               raise (RefineFailure (lazy (localise t, Lazy.force msg)))
          | NCicEnvironment.AssertFailure msg -> raise (AssertFailure msg))
     | C.Implicit infos -> 
-         let metasenv,_,t,ty =
-           exp_implicit ~localise metasenv context expty t infos
+         let (metasenv,_,t,ty),subst =
+           exp_implicit rdb ~localise metasenv subst context expty t infos
          in
           metasenv, subst, t, ty 
     | C.Meta (n,l) as t -> 
@@ -489,7 +509,9 @@ and guess_name subst ctx ty =
 
 and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he he ty_he args =
   (*D*)inside 'E'; try let rc = 
-  let rec aux metasenv subst args_so_far he ty_he = function 
+  let rec aux metasenv subst args_so_far he ty_he xxx =
+  (*D*)inside 'V'; try let rc = 
+   match xxx with
   | [] ->
      let res = NCicUntrusted.mk_appl he (List.rev args_so_far) in
      pp(lazy("FORCE FINAL APPL: " ^ 
@@ -579,6 +601,7 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he
                (List.length args) (List.length args_so_far))))
           in
            aux metasenv subst [] newhead newheadty (arg :: tl)
+  (*D*)in outside true; rc with exc -> outside false; raise exc
   in
    (* We need to reverse the order of the new created metas since they
       are pushed on top of the metasenv in the wrong order *)
-- 
2.39.2