From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 31 Aug 2007 08:44:56 +0000 (+0000)
Subject: fixed coercions between arrows when the arrow is dependent.
X-Git-Tag: 0.4.95@7852~233
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=447c96d72448a6876e29b1d0b39400a139fa0be0;p=helm.git

fixed coercions between arrows when the arrow is dependent.
---

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index 2ef492bc8..9ccf2b2ff 100644
--- a/components/cic_unification/cicRefine.ml
+++ b/components/cic_unification/cicRefine.ml
@@ -1408,37 +1408,34 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
         if not allow_coercions || not !insert_coercions then
           enrich localization_tbl t exn
         else
-          let clean t subst context = 
-            CicReduction.whd 
-              ~delta:false context (CicMetaSubst.apply_subst subst t)
-          in
+          let whd = CicReduction.whd ~delta:false in
+          let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
           let infty = clean infty subst context in
           let expty = clean expty subst context in
           match infty, expty with
           | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2) -> 
-              (* covariant part *)
+              let module CS = CicSubstitution in
               let name_con = Cic.Name "name_con" in
-              let name_t, ty_s_bo, bo = 
+              let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in
+              (* contravariant part: the argument of f:src->ty *)
+              let (rel1, _), subst, metasenv, ugraph = 
+                coerce_to_something_aux
+                 (Cic.Rel 1) (CS.lift 1 src2) 
+                 (CS.lift 1 src) subst metasenv context_src2 ugraph
+              in
+              (* covariant part: the result of f(c x); x:src2; (c x):src *)
+              let name_t, bo = 
                 match t with
-                | Cic.Lambda (name, src, bo) -> name, src, bo
-                | _ -> name_con,src,Cic.Appl[CicSubstitution.lift 1 t;Cic.Rel 1]
+                | Cic.Lambda (n,_,bo) -> n, CS.subst rel1 (CS.lift_from 2 1 bo)
+                | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1]
               in
-              let context_bo = (Some (name_t, Cic.Decl ty_s_bo)) :: context in
+              (* we fix the possible dependency problem in the source ty *)
+              let ty = CS.subst rel1 (CS.lift_from 2 1 ty) in
               let (bo, _), subst, metasenv, ugraph = 
                 coerce_to_something_aux
-                  bo ty ty2 subst metasenv context_bo ugraph
-              in
-              (* contravariant part *)
-              let context_rel1 = (Some (name_t, Cic.Decl src2) :: context) in
-              let (rel1, _), subst, metasenv, ugraph = 
-                coerce_to_something_aux
-                 (Cic.Rel 1) (CicSubstitution.lift 1 src2) 
-                 (CicSubstitution.lift 1 src) subst metasenv context_rel1 ugraph
-              in
-              let coerced = 
-                Cic.Lambda (name_t,src2,
-                  CicSubstitution.subst rel1 (CicSubstitution.lift_from 2 1 bo))
+                  bo ty ty2 subst metasenv context_src2 ugraph
               in
+              let coerced = Cic.Lambda (name_t,src2, bo) in
                 (coerced, expty), subst, metasenv, ugraph
           | _ -> 
             coerce_atom_to_something t infty expty subst metasenv context ugraph