We forgot an important check: the declared and expected type in definitions in

the context must be checked for convertibility.

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 5985123733f46b7645bded16f241146f894f1854..fc6d04a038dfa2c91ee102100d82d83bf7151d93 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -980,11 +980,19 @@ let typecheck_context ~metasenv ~subst context =
   (List.fold_right
    (fun d context  ->
      begin
-      match snd d with
-         C.Decl t -> ignore (typeof ~metasenv ~subst:[] context t)
-       | C.Def (te,ty) ->
-          ignore (typeof ~metasenv ~subst:[] context te);
+      match d with
+         _,C.Decl t -> ignore (typeof ~metasenv ~subst:[] context t)
+       | name,C.Def (te,ty) ->
          ignore (typeof ~metasenv ~subst:[] context ty);
+         let ty' = typeof ~metasenv ~subst:[] context te in
+          if not (R.are_convertible ~subst [] ty' ty) then
+           raise (AssertFailure (lazy (Printf.sprintf (
+            "the type of the definiens for %s in the context is not "^^
+            "convertible with the declared one.\n"^^
+            "inferred type:\n%s\nexpected type:\n%s")
+            name
+            (PP.ppterm ~subst ~metasenv ~context:[] ty') 
+            (PP.ppterm ~subst ~metasenv ~context:[] ty))))
      end;
      d::context
    ) context [])