From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 14 May 2008 16:35:55 +0000 (+0000)
Subject: We forgot an important check: the declared and expected type in definitions in
X-Git-Tag: make_still_working~5208
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8ff8cc51c76a444cc124c314155a33af51917e6d;p=helm.git

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 598512373..fc6d04a03 100644
--- 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 [])