Recently introduced bug fixed: error localization was not working properly for

the error "more arguments than expected".

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index b50667bb5546a745ac53420827f0cdbd1d300dc6..4b310ef75637fd6a1e1127fcbc181a84fa4006fd 100644 (file)
--- a/components/cic_unification/cicRefine.ml
+++ b/components/cic_unification/cicRefine.ml
@@ -31,6 +31,9 @@ exception RefineFailure of string Lazy.t;;
 exception Uncertain of string Lazy.t;;
 exception AssertFailure of string Lazy.t;;
 
+(* for internal use only; the integer is the number of surplus arguments *)
+exception MoreArgsThanExpected of int * exn;;
+
 let insert_coercions = ref true
 let pack_coercions = ref true
 
@@ -149,15 +152,16 @@ let is_a_double_coercion t =
       | _ -> dummyres)
   | _ -> dummyres
 
-let more_args_than_expected
-  localization_tbl metasenv subst he context hetype' tlbody_and_type exn
+let more_args_than_expected localization_tbl metasenv subst he context hetype' residuals tlbody_and_type exn
 =
+  let len = List.length tlbody_and_type in
   let msg = 
     lazy ("The term " ^
       CicMetaSubst.ppterm_in_context ~metasenv subst he context ^ 
-      " (that has type "^CicMetaSubst.ppterm_in_context ~metasenv subst hetype' context ^
-      ") is here applied to " ^ string_of_int (List.length tlbody_and_type) ^
-      " arguments that are more than expected")
+      " (that has type "^ CicMetaSubst.ppterm_in_context ~metasenv subst hetype' context ^
+      ") is here applied to " ^ string_of_int len ^
+      " arguments but here it can handle only up to " ^
+      string_of_int (len - residuals) ^ " arguments")
   in
   enrich localization_tbl he ~f:(fun _-> msg) exn
 ;; 
@@ -1179,18 +1183,19 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
     in
       tlbody_and_type,subst,metasenv,ugraph
 
-  and eat_prods 
+  and eat_prods
     allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph 
   =
     (* given he:hety, gives beack all (c he) such that (c e):?->? *)
-    let fix_arity exn metasenv context subst he hetype ugraph =
+    let fix_arity n metasenv context subst he hetype ugraph =
       let hetype = CicMetaSubst.apply_subst subst hetype in
       let src = CoercDb.coerc_carr_of_term hetype in 
       let tgt = CoercDb.Fun 0 in
       match CoercGraph.look_for_coercion' metasenv subst context src tgt with
-      | CoercGraph.NoCoercion 
+      | CoercGraph.NoCoercion -> []
       | CoercGraph.NotMetaClosed 
-      | CoercGraph.NotHandled _ -> raise exn
+      | CoercGraph.NotHandled _ ->
+         raise (MoreArgsThanExpected (n,Uncertain (lazy "")))
       | CoercGraph.SomeCoercionToTgt candidates
       | CoercGraph.SomeCoercion candidates ->
           HExtlib.filter_map
@@ -1201,11 +1206,10 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                fo_unif_subst subst context metasenv last he ugraph in
               debug_print (lazy ("New head: "^ pp coerc));
               try
-                let t,tty,subst,metasenv,ugraph =
-                  type_of_aux subst metasenv context coerc ugraph in 
-                (*{{{*)debug_print (lazy (" refined: "^ pp t));
-                debug_print (lazy (" has type: "^ pp tty));(*}}}*)
-                Some (t,tty,subst,metasenv,ugraph)
+                let tty,ugraph =
+                 CicTypeChecker.type_of_aux' ~subst metasenv context coerc ugraph in 
+                debug_print (lazy (" has type: "^ pp tty));
+                Some (coerc,tty,subst,metasenv,ugraph)
               with
               | Uncertain _ | RefineFailure _
               | HExtlib.Localized (_,Uncertain _)
@@ -1239,9 +1243,9 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                "Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^
                "\n but is applyed to: " ^ String.concat ";" 
                (List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*)
-              let exn = RefineFailure (lazy ("more args than expected")) in
               let possible_fixes = 
-               fix_arity exn metasenv context subst he hetype ugraph in
+               fix_arity (List.length args) metasenv context subst he hetype
+                ugraph in
               match
                 HExtlib.list_findopt
                  (fun (he,hetype,subst,metasenv,ugraph) ->
@@ -1253,13 +1257,17 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                    try      
                     Some (eat_prods_and_args 
                       metasenv subst context he hetype ugraph [] args)
-                   with RefineFailure _ | Uncertain _ -> None)
+                   with
+                    | RefineFailure _ | Uncertain _
+                    | HExtlib.Localized (_,RefineFailure _)
+                    | HExtlib.Localized (_,Uncertain _) -> None)
                 possible_fixes
               with
               | Some x -> x
               | None ->
-                 more_args_than_expected localization_tbl metasenv
-                   subst he context hetype args_bo_and_ty exn
+                 raise 
+                  (MoreArgsThanExpected
+                    (List.length args, RefineFailure (lazy "")))
     in
     (* first we check if we are in the simple case of a meta closed term *)
     let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
@@ -1281,8 +1289,13 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
           subst,pristinemenv,ugraph,hetype,he,args_bo_and_ty
     in
     let coerced_args,subst,metasenv,he,t,ugraph =
+     try
       eat_prods_and_args 
         metasenv subst context he hetype' ugraph1 [] args_bo_and_ty
+     with
+      MoreArgsThanExpected (residuals,exn) ->
+        more_args_than_expected localization_tbl metasenv
+         subst he context hetype' residuals args_bo_and_ty exn
     in
     he,(List.map fst coerced_args),t,subst,metasenv,ugraph