Serious bug fixed: the max of two universes was computed using the polymorphic

[helm.git] / helm / software / components / ng_kernel / nCicTypeChecker.ml

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 00a1b6120ce3fd4f70380030a709fb7655a3ba02..bccf753f2dff61bb9d3d4ae7f18f8a096b229c04 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -124,7 +124,7 @@ let sort_of_prod ~metasenv ~subst context (name,s) (t1, t2) =
    let t2 = R.whd ~subst ((name,C.Decl s)::context) t2 in
    match t1, t2 with
    | C.Sort s1, C.Sort C.Prop -> t2
-   | C.Sort (C.Type u1), C.Sort (C.Type u2) -> C.Sort (C.Type (max u1 u2)) 
+   | C.Sort (C.Type u1), C.Sort (C.Type u2) -> C.Sort (C.Type (u1@u2)) 
    | C.Sort _,C.Sort (C.Type _) -> t2
    | C.Sort (C.Type _) , C.Sort C.CProp -> t1
    | C.Sort _, C.Sort C.CProp
@@ -720,12 +720,13 @@ and check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl =
            let context,te = split_prods ~subst tys leftno te in
            let con_sort = typeof ~subst ~metasenv context te in
            (match R.whd ~subst context con_sort, R.whd ~subst [] ty_sort with
-               C.Sort (C.Type u1), C.Sort (C.Type u2) ->
+               (C.Sort (C.Type u1) as s1), (C.Sort (C.Type u2) as s2) ->
                 if not (E.universe_leq u1 u2) then
                  raise
                   (TypeCheckerFailure
-                    (lazy ("The type of the constructor is not included in " ^
-                      "the inductive type sort")))
+                    (lazy ("The type " ^ PP.ppterm ~metasenv ~subst ~context s1^
+                      " of the constructor is not included in the inductive" ^
+                      " type sort " ^ PP.ppterm ~metasenv ~subst ~context s2)))
              | C.Sort _, C.Sort C.Prop
              | C.Sort C.CProp, C.Sort C.CProp
              | C.Sort _, C.Sort C.Type _ -> ()