Ugly solution to the "we proved T that is equivalent to T" problem:

we use pack_coercion (defined into cicRefine) inside doubleTypeInference
(that is well below in the module hierarchy :-(

This is also supposed to be quite expensive (since pack_coercion uses
the refiner and coercion packing is applied to every expected/synthesized
type).

diff --git a/components/cic_acic/doubleTypeInference.ml b/components/cic_acic/doubleTypeInference.ml
index 30a8f5c290fdaac79a3ecc28f10269f2d2db611f..214f656c38d5db4d27f889f9b6019b3b28d4eb12 100644 (file)
--- a/components/cic_acic/doubleTypeInference.ml
+++ b/components/cic_acic/doubleTypeInference.ml
@@ -319,6 +319,8 @@ let type_of_mutual_inductive_constr uri i j =
     | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
 ;;
 
+let pack_coercion = ref (fun _ _ _ -> assert false);;
+
 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
 let rec type_of_aux' subterms_to_types metasenv context t expectedty =
  (* Coscoy's double type-inference algorithm             *)
@@ -330,6 +332,10 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
   let module R = CicReduction in
   let module S = CicSubstitution in
   let module U = UriManager in
+   let expectedty =
+    match expectedty with
+       None -> None
+     | Some t -> Some (!pack_coercion metasenv context t) in
    let synthesized =
     match t with
        C.Rel n ->
@@ -609,6 +615,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
            ty
    in
     let synthesized' = beta_reduce synthesized in
+    let synthesized' = !pack_coercion metasenv context synthesized' in
      let types,res =
       match expectedty with
          None ->

diff --git a/components/cic_acic/doubleTypeInference.mli b/components/cic_acic/doubleTypeInference.mli
index 892e09f8ac4d1172f96f4f1a8c42cbb265fca5f6..86d8b23fabee6cac29723f5866a29dfb1f981d72 100644 (file)
--- a/components/cic_acic/doubleTypeInference.mli
+++ b/components/cic_acic/doubleTypeInference.mli
@@ -14,6 +14,8 @@ val number_new_type_of_aux'_prop: int ref
 
 type types = {synthesized : Cic.term ; expected : Cic.term option};;
 
+val pack_coercion : (Cic.metasenv -> Cic.context -> Cic.term -> Cic.term) ref;;
+
 val double_type_of :
  Cic.metasenv -> Cic.context -> Cic.term -> Cic.term option ->
   types Cic.CicHash.t

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index 6065d24bd41a705fba4f977ea28dd18b919c9300..3443c9b6ea90ebcf8af3286738e96a5188c4a85c 100644 (file)
--- a/components/cic_unification/cicRefine.ml
+++ b/components/cic_unification/cicRefine.ml
@@ -1645,3 +1645,5 @@ let type_of_aux' ?localization_tbl metasenv context term ugraph =
 
 let typecheck ~localization_tbl metasenv uri obj =
  profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
+
+let _ = DoubleTypeInference.pack_coercion := pack_coercion;;

diff --git a/components/cic_unification/cicRefine.mli b/components/cic_unification/cicRefine.mli
index c3ab49e0abd84dd19a79de242dffb25999928e79..be1069e716ef35459836f464921e77b9315fee05 100644 (file)
--- a/components/cic_unification/cicRefine.mli
+++ b/components/cic_unification/cicRefine.mli
@@ -46,6 +46,5 @@ val typecheck :
 
 val insert_coercions: bool ref (* initially true *)
 
-(* given a closed term returns it with all coercions packed *)
 val pack_coercion_obj: Cic.obj -> Cic.obj