Fixed some HoTT bugs, provide a proper error message when giving an ill-formed

universe instance.

6 files changed, 25 insertions, 27 deletions

diff --git a/library/universes.ml b/library/universes.ml
index e2a3901ba..0699326c5 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -244,9 +244,14 @@ let fresh_instance ctx =
 let existing_instance ctx inst = 
   let s = ref LMap.empty in
   let () = 
-    Array.iter2 (fun u v -> 
-      s := LMap.add v u !s)
-      (Instance.to_array inst) (Instance.to_array (UContext.instance ctx))
+    let a1 = Instance.to_array inst 
+    and a2 = Instance.to_array (UContext.instance ctx) in
+    let len1 = Array.length a1 and len2 = Array.length a2 in 
+      if not (len1 == len2) then
+	Errors.errorlabstrm "Universes"
+	  (str "Polymorphic constant expected " ++ int len2 ++ 
+	     str" levels but was given " ++ int len1)
+      else Array.iter2 (fun u v -> s := LMap.add v u !s) a1 a2
   in LSet.empty, !s, inst
 
 let fresh_instance_from ctx inst =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 1520e1a7e..2c16c2eb3 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -275,14 +275,21 @@ let interp_universe_level_name evd = function
   | GSet -> evd, Univ.Level.set
   | GType s -> interp_universe_name evd s
 
-let pretype_global rigid env evd gr us = 
+let pretype_global loc rigid env evd gr us = 
   let evd, instance = 
     match us with
     | None -> evd, None
     | Some l -> 
-      let evd, l' = List.fold_left (fun (evd, univs) l -> 
-	let evd, l = interp_universe_level_name evd l in
-	  (evd, l :: univs)) (evd, []) l
+      let _, ctx = Universes.unsafe_constr_of_global gr in
+      let arr = Univ.Instance.to_array (Univ.UContext.instance ctx) in
+      let len = Array.length arr in
+	if len != List.length l then
+	  user_err_loc (loc, "pretype", 
+			str "Universe instance should have length " ++ int len)
+	else
+	  let evd, l' = List.fold_left (fun (evd, univs) l -> 
+	    let evd, l = interp_universe_level_name evd l in
+	      (evd, l :: univs)) (evd, []) l
       in 
 	evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
   in
@@ -302,7 +309,7 @@ let pretype_ref loc evdref env ref us =
             variables *)
          Pretype_errors.error_var_not_found_loc loc id)
   | ref ->
-    let evd, c = pretype_global univ_flexible env !evdref ref us in
+    let evd, c = pretype_global loc univ_flexible env !evdref ref us in
     let () = evdref := evd in
     let ty = Retyping.get_type_of env evd c in
       make_judge c ty
diff --git a/test-suite/bugs/opened/3374.v b/test-suite/bugs/closed/3374.v
index 8a62838f0..3c67703a2 100644
--- a/test-suite/bugs/opened/3374.v
+++ b/test-suite/bugs/closed/3374.v
@@ -32,7 +32,8 @@ Proof.
   apply (dirprodtosetquot R R).
   apply dirprodpair; [ exact c | exact c0 ].
   Undo.
-  Fail exact (dirprodpair c c0).
+  exact (dirprodpair c c0).
+Defined.
   (* Toplevel input, characters 39-40:
 Error:
 In environment
diff --git a/test-suite/bugs/opened/3375.v b/test-suite/bugs/closed/3375.v
index 9cb43413b..fe323fcb2 100644
--- a/test-suite/bugs/opened/3375.v
+++ b/test-suite/bugs/closed/3375.v
@@ -7,7 +7,7 @@ Definition UU := Set.
 Definition dirprod ( X Y : UU ) := sigT ( fun x : X => Y ) .
 Definition dirprodpair { X Y : UU } := existT ( fun x : X => Y ) .
 Definition hProp := sigT (fun X : Type => admit).
-Axiom hProppair : forall ( X : UU ) ( is : admit ), hProp@{Set i}.
+Axiom hProppair : forall ( X : UU ) ( is : admit ), hProp.
 Definition hProptoType := @projT1 _ _ : hProp -> Type .
 Coercion hProptoType: hProp >-> Sortclass.
 Definition ishinh_UU ( X : UU ) : UU := forall P: Set, ( ( X -> P ) -> P ).
@@ -31,7 +31,7 @@ Definition iseqclassconstr { X : UU } ( R : hrel X ) { A : hsubtypes X } ( ax0 :
   pose @iseqclassconstr'.
   intros.
   exact (dirprodpair ax0 (dirprodpair ax1 ax2)).
-Fail Defined.
+Defined.
 (* Toplevel input, characters 15-23:
 Error: Illegal application:
 The term "dirprodpair" of type
diff --git a/test-suite/bugs/opened/3372.v b/test-suite/bugs/opened/3372.v
index 41ee400fd..13ce75b84 100644
--- a/test-suite/bugs/opened/3372.v
+++ b/test-suite/bugs/opened/3372.v
@@ -1,5 +1,5 @@
 Set Universe Polymorphism.
 Definition hProp : Type := sigT (fun _ : Type => True).
-Fail Goal hProp@{Set}. (* Toplevel input, characters 15-32:
+Goal hProp@{Set}. (* Toplevel input, characters 15-32:
 Anomaly: Uncaught exception Invalid_argument("Array.iter2", _).
 Please report. *)
diff --git a/test-suite/bugs/opened/3373.v b/test-suite/bugs/opened/3373.v
deleted file mode 100644
index 8b3b51567..000000000
--- a/test-suite/bugs/opened/3373.v
+++ /dev/null
@@ -1,15 +0,0 @@
-(* File reduced by coq-bug-finder from original input, then from 5968 lines to 11933 lines, then from 11239 lines to 11231 lines, then from 10365 lines to 446 lines, then from 456 lines to 379 lines, then from 391 lines to 373 lines, then from 369 lines to 351 lines, then from 350 lines to 340 lines, then from 348 lines to 320 lines, then from 328 lines to 302 lines, then from 332 lines to 21 lines *)
-Set Universe Polymorphism.
-Axiom admit : forall {T}, T.
-Definition UU := Set.
-Definition UU' := Type.
-Definition hSet:= sigT (fun X : UU' => admit) .
-Definition pr1hSet:= @projT1 UU (fun X : UU' => admit) : hSet -> Type.
-Coercion pr1hSet: hSet >-> Sortclass.
-Axiom binop : UU -> Type.
-Axiom setwithbinop : Type.
-Definition pr1setwithbinop : setwithbinop -> hSet.
-Fail exact ( @projT1 _ ( fun X : hSet@{i j} => binop X ) ).
-(* Toplevel input, characters 15-69:
-Anomaly: apply_coercion_args: mismatch between arguments and coercion.
-Please report. *)