type_of_constant was retunrning the type of the wrong constructor (-1 missing)

fixpoints were not properly debruijnated before being checked
better error message for match branches

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index e0f6bbaed6646f0a1efd0903b3728b8e9895807b..81f633bb6c850362623c0b617ff3ccc41e86b52f 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -777,7 +777,8 @@ let rec typeof ~subst ~metasenv context term =
               let ty_p = typeof_aux context p in
               let ty_cons = typeof_aux context cons in
               let ty_branch = 
-                type_of_branch ~subst context leftno outtype cons ty_cons 0 in
+                type_of_branch ~subst context leftno outtype cons ty_cons 0 
+              in
               j+1, R.are_convertible ~subst ~metasenv context ty_p ty_branch,
               ty_p, ty_branch
             else
@@ -787,9 +788,10 @@ let rec typeof ~subst ~metasenv context term =
       if not branches_ok then
         raise
          (TypeCheckerFailure 
-          (lazy (Printf.sprintf "Branch for constructor %s has type %s != %s"
-          (NCicPp.ppterm (C.Const 
-            (Ref.Ref (dummy_depth, uri, Ref.Con (tyno, j)))))
+          (lazy (Printf.sprintf ("Branch for constructor %s :=\n%s\n"^^
+          "has type %s\nnot convertible with %s") (NCicPp.ppterm (C.Const 
+          (Ref.Ref (dummy_depth, uri, Ref.Con (tyno, j)))))
+          (NCicPp.ppterm ~context (List.nth pl (j-1)))
           (NCicPp.ppterm ~context p_ty) (NCicPp.ppterm ~context exp_p_ty)))); 
       let res = outtype::arguments@[term] in
       R.head_beta_reduce (C.Appl res)
@@ -1152,7 +1154,7 @@ and type_of_constant ((Ref.Ref (_,uri,_)) as ref) =
       let _,_,arity,_ = List.nth tl i in arity
   | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,_,Ref.Con (i,j))  ->
       let _,_,_,cl = List.nth tl i in 
-      let _,_,arity = List.nth cl j in 
+      let _,_,arity = List.nth cl (j-1) in 
       arity
   | (_,_,_,_,C.Fixpoint (_,fl,_)), Ref.Ref (_,_,(Ref.Fix (i,_)|Ref.CoFix i)) ->
       let _,_,_,arity,_ = List.nth fl i in
@@ -1182,6 +1184,7 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) =
          ) ([],[],0) fl
       in
         List.iter (fun (_,name,x,ty,bo) ->
+         let bo = debruijn uri len bo in
          let ty_bo = typeof ~subst ~metasenv types bo in
          if not (R.are_convertible ~subst ~metasenv types ty_bo (S.lift len ty))
          then raise (TypeCheckerFailure (lazy ("(Co)Fix: ill-typed bodies")))