More refinement errors localized.

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 52b1a1034d365207a33077155dc58e282c68dabd..3faee32df31fbd8c48e2976a6cd5ccc9f02aba04 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -144,14 +144,24 @@ let avoid_double_coercion context subst metasenv ugraph t ty =
         let args = mk_implicits head (arity - 1) in
         let c_bo = CicUtil.term_of_uri (CicUtil.uri_of_term c) in
         let newt = Cic.Appl (c_bo::args) in
-        let subst, metasenv, ugraph = 
-          CicUnification.fo_unif_subst subst context metasenv newt t ugraph
-        in
-        debug_print 
-          (lazy 
-            ("packing: " ^ 
-              CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm (Cic.Appl (c::args))));
-        Cic.Appl (c::args), ty, subst, metasenv, ugraph
+        (try
+          let subst, metasenv, ugraph = 
+           fo_unif_subst subst context metasenv newt t ugraph
+          in
+          debug_print 
+            (lazy 
+              ("packing: " ^ 
+                CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm (Cic.Appl (c::args))));
+          Cic.Appl (c::args), ty, subst, metasenv, ugraph
+         with
+            RefineFailure _ ->
+             prerr_endline ("#### Coercion not packed (Refine_failure): " ^
+              CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm (Cic.Appl (c::args)));
+             assert false
+          | Uncertain _ ->
+             prerr_endline ("#### Coercion not packed (Uncercatin case): " ^
+              CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm (Cic.Appl (c::args)));
+             assert false)
     | _ -> assert false) (* the composite coercion must exist *)
   else
     t, ty, subst, metasenv, ugraph  
@@ -779,8 +789,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
                | Some candidate ->
                    let subst,metasenv,ugraph = 
+                    try
                      fo_unif_subst subst context metasenv 
                        candidate outtype ugraph5
+                    with
+                     exn -> assert false(* unification against a metavariable *)
                    in
                      C.MutCase (uri, i, outtype, term', pl'),
                       CicReduction.head_beta_reduce
@@ -806,9 +819,10 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                  (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
              in
              let (subst,metasenv,ugraph6) = 
-               List.fold_left
+               List.fold_left2
                  (fun (subst,metasenv,ugraph) 
-                        (constructor_args_no,context,instance,args) ->
+                   p (constructor_args_no,context,instance,args)
+                  ->
                     let instance' = 
                       let appl =
                         let outtype' =
@@ -818,9 +832,21 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                       in
                         CicReduction.whd ~subst context appl
                     in
-                    fo_unif_subst subst context metasenv 
-                        instance instance' ugraph)
-                 (subst,metasenv,ugraph5) outtypeinstances 
+                     try
+                      fo_unif_subst subst context metasenv instance instance'
+                       ugraph
+                     with
+                      exn ->
+                       enrich localization_tbl p exn
+                        ~f:(function _ ->
+                          lazy ("The term " ^
+                           CicMetaSubst.ppterm_in_context subst p
+                            context ^ " has type " ^
+                           CicMetaSubst.ppterm_in_context subst instance'
+                            context ^ " but is here used with type " ^
+                           CicMetaSubst.ppterm_in_context subst instance
+                            context)))
+                 (subst,metasenv,ugraph5) pl' outtypeinstances 
              in
                C.MutCase (uri, i, outtype, term', pl'),
                  CicReduction.head_beta_reduce
@@ -844,11 +870,23 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
               List.fold_left
                 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
-                     type_of_aux subst metasenv context' bo ugraph
-                   in
+                     type_of_aux subst metasenv context' bo ugraph in
+                   let expected_ty = CicSubstitution.lift len ty in
                    let subst',metasenv',ugraph' =
+                    try
                      fo_unif_subst subst context' metasenv
-                       ty_of_bo (CicSubstitution.lift len ty) ugraph1
+                       ty_of_bo expected_ty ugraph1
+                    with
+                     exn ->
+                      enrich localization_tbl bo exn
+                       ~f:(function _ ->
+                         lazy ("The term " ^
+                          CicMetaSubst.ppterm_in_context subst bo
+                           context' ^ " has type " ^
+                          CicMetaSubst.ppterm_in_context subst ty_of_bo
+                           context' ^ " but is here used with type " ^
+                          CicMetaSubst.ppterm_in_context subst expected_ty
+                           context))
                    in 
                      fl @ [bo'] , subst',metasenv',ugraph'
                 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty') 
@@ -885,11 +923,23 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
               List.fold_left
                 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
-                     type_of_aux subst metasenv context' bo ugraph
-                   in
+                     type_of_aux subst metasenv context' bo ugraph in
+                   let expected_ty = CicSubstitution.lift len ty in
                    let subst',metasenv',ugraph' = 
+                    try
                      fo_unif_subst subst context' metasenv
-                       ty_of_bo (CicSubstitution.lift len ty) ugraph1
+                       ty_of_bo expected_ty ugraph1
+                    with
+                     exn ->
+                      enrich localization_tbl bo exn
+                       ~f:(function _ ->
+                         lazy ("The term " ^
+                          CicMetaSubst.ppterm_in_context subst bo
+                           context' ^ " has type " ^
+                          CicMetaSubst.ppterm_in_context subst ty_of_bo
+                           context' ^ " but is here used with type " ^
+                          CicMetaSubst.ppterm_in_context subst expected_ty
+                           context))
                    in
                      fl @ [bo'],subst',metasenv',ugraph'
                 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
@@ -1038,7 +1088,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
         | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
         | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
             (* TODO how can we force the meta to become a sort? If we don't we
-             * brake the invariant that refine produce only well typed terms *)
+             * break the invariant that refine produce only well typed terms *)
             (* TODO if we check the non meta term and if it is a sort then we
              * are likely to know the exact value of the result e.g. if the rhs
              * is a Sort (Prop | Set | CProp) then the result is the rhs *)