From 8ff8cc51c76a444cc124c314155a33af51917e6d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 14 May 2008 16:35:55 +0000 Subject: [PATCH] We forgot an important check: the declared and expected type in definitions in the context must be checked for convertibility. --- .../components/ng_kernel/nCicTypeChecker.ml | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) 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 []) -- 2.39.2