guarded by has a nice error message

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 46caae5acbed96d74038abd74ec7ebead2d80f43..7e9cd70b206dcde2d7fe22ab6fb4044b775c7ca5 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -669,7 +669,7 @@ let does_not_occur ~subst context n nn t =
    with DoesOccur -> false
 ;;
 
-exception NotGuarded;;
+exception NotGuarded of string Lazy.t;;
 
 let rec typeof ~subst ~metasenv context term =
   let rec typeof_aux context = 
@@ -985,19 +985,24 @@ and eat_lambdas ~subst context n te =
 and guarded_by_destructors ~subst context recfuns t = 
  let recursor f k t = NCicUtils.fold shift_k k (fun k () -> f k) () t in
  let rec aux (context, recfuns, x, safes as k) = function
-  | C.Rel m when List.mem_assoc m recfuns -> raise NotGuarded 
+  | C.Rel m as t when List.mem_assoc m recfuns -> 
+      raise (NotGuarded (lazy (NCicPp.ppterm ~context t ^ " passed around")))
   | C.Rel m ->
      (match List.nth context (m-1) with 
      | _,C.Decl _ -> ()
      | _,C.Def (bo,_) -> aux (context, recfuns, x, safes) (S.lift m bo))
   | C.Meta _ -> ()
-  | C.Appl ((C.Rel m)::tl) when List.mem_assoc m recfuns ->
+  | C.Appl ((C.Rel m)::tl) as t when List.mem_assoc m recfuns ->
      let rec_no = List.assoc m recfuns in
-     if not (List.length tl > rec_no) then raise NotGuarded
+     if not (List.length tl > rec_no) then 
+       raise (NotGuarded (lazy 
+         (NCicPp.ppterm ~context ~subst t ^ 
+         " is a partial application of a fix")))
      else
        let rec_arg = List.nth tl rec_no in
-       if not (is_really_smaller ~subst k rec_arg) then raise
-       NotGuarded;
+       if not (is_really_smaller ~subst k rec_arg) then 
+         raise (NotGuarded (lazy 
+           (NCicPp.ppterm ~context ~subst rec_arg ^ " not smaller")));
        List.iter (aux k) tl
   | C.Match (Ref.Ref (_,uri,_) as ref,outtype,term,pl) as t ->
      (match R.whd ~subst context term with
@@ -1018,8 +1023,8 @@ and guarded_by_destructors ~subst context recfuns t =
      | _ -> recursor aux k t)
   | t -> recursor aux k t
  in
-  try aux (context, recfuns, 1, []) t;true
-  with NotGuarded -> false
+  try aux (context, recfuns, 1, []) t
+  with NotGuarded s -> raise (TypeCheckerFailure s)
 
 (*
  | C.Fix (_, fl) ->
@@ -1212,9 +1217,7 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) =
             let rec enum_from k = 
               function [] -> [] | v::tl -> (k,v)::enum_from (k+1) tl 
             in
-            if not (guarded_by_destructors 
-                      ~subst context (enum_from (x+1) kl) m) then
-              raise(TypeCheckerFailure(lazy("Fix: not guarded by destructors")))
+            guarded_by_destructors ~subst context (enum_from (x+1) kl) m;
           end else
            match returns_a_coinductive ~subst [] ty with
             | None ->