Fix HoTT/coq bug # 14. Now coercion code correctly raises an error instead of an anomaly in case

a universe inconsistency occurs when applying a coercion. The statement of the test-suite file
cannot check as is, but does check when the correct FunctorCategory is given, instantiating the TypeCat
to Set.

2 files changed, 44 insertions, 29 deletions

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index baf98eee7..125517aec 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -40,14 +40,13 @@ let apply_coercion_args env evd check argl funj =
   let rec apply_rec acc typ = function
     | [] -> { uj_val = applist (j_val funj,argl);
 	      uj_type = typ }
-    | h::restl ->
-	(* On devrait pouvoir s'arranger pour qu'on n'ait pas à faire hnf_constr *)
-  	match kind_of_term (whd_betadeltaiota env evd typ) with
-	| Prod (_,c1,c2) ->
-	    if check && not (e_cumul env evdref (Retyping.get_type_of env evd h) c1) then
-	      anomaly (Pp.str"apply_coercion_args: mismatch between arguments and coercion");
-	    apply_rec (h::acc) (subst1 h c2) restl
-	| _ -> anomaly (Pp.str "apply_coercion_args")
+    | h::restl -> (* On devrait pouvoir s'arranger pour qu'on n'ait pas a faire hnf_constr *)
+      match kind_of_term (whd_betadeltaiota env evd typ) with
+      | Prod (_,c1,c2) ->
+        if check && not (e_cumul env evdref (Retyping.get_type_of env evd h) c1) then
+	  raise NoCoercion;
+        apply_rec (h::acc) (subst1 h c2) restl
+      | _ -> anomaly (Pp.str "apply_coercion_args")
   in
   let res = apply_rec [] funj.uj_type argl in
     !evdref, res
@@ -346,7 +345,8 @@ let apply_coercion env sigma p hj typ_cl =
 	    jres.uj_type,sigma)
       (hj,typ_cl,sigma) p
     in evd, j
-  with e when Errors.noncritical e -> anomaly (Pp.str "apply_coercion")
+  with NoCoercion as e -> raise e
+  | e when Errors.noncritical e -> anomaly (Pp.str "apply_coercion")
 
 let inh_app_fun env evd j =
   let t = whd_betadeltaiota env evd j.uj_type in
@@ -359,7 +359,7 @@ let inh_app_fun env evd j =
       	try let t,p =
 	  lookup_path_to_fun_from env evd j.uj_type in
 	    apply_coercion env evd p j t
-	with Not_found when Flags.is_program_mode () ->
+	with Not_found | NoCoercion when Flags.is_program_mode () ->
 	  try
 	    let evdref = ref evd in
 	    let coercef, t = mu env evdref t in
@@ -382,7 +382,7 @@ let inh_tosort_force loc env evd j =
     let evd,j1 = apply_coercion env evd p j t in
     let j2 = on_judgment_type (whd_evar evd) j1 in
       (evd,type_judgment env j2)
-  with Not_found ->
+  with Not_found | NoCoercion ->
     error_not_a_type_loc loc env evd j
 
 let inh_coerce_to_sort loc env evd j =
@@ -421,7 +421,7 @@ let inh_coerce_to_fail env evd rigidonly v t c1 =
       try
 	let t2,t1,p = lookup_path_between env evd (t,c1) in
 	  match v with
-	  Some v ->
+	  | Some v ->
 	    let evd,j =
 	      apply_coercion env evd p
 		{uj_val = v; uj_type = t} t2 in
diff --git a/test-suite/bugs/opened/HoTT_coq_014.v b/test-suite/bugs/closed/HoTT_coq_014.v
index 109653ca2..63548a644 100644
--- a/test-suite/bugs/opened/HoTT_coq_014.v
+++ b/test-suite/bugs/closed/HoTT_coq_014.v
@@ -1,6 +1,6 @@
 Set Implicit Arguments.
 Generalizable All Variables.
-
+Set Universe Polymorphism.
 
 Polymorphic Record SpecializedCategory (obj : Type) := Build_SpecializedCategory' {
   Object :> _ := obj;
@@ -13,8 +13,8 @@ Polymorphic Record SpecializedCategory (obj : Type) := Build_SpecializedCategory
 Polymorphic Definition Morphism obj (C : @SpecializedCategory obj) : forall s d : C, _ := Eval cbv beta delta [Morphism'] in C.(Morphism').
 
 (* eh, I'm not terribly happy.  meh. *)
-Polymorphic Definition SmallSpecializedCategory (obj : Set) (*mor : obj -> obj -> Set*) := SpecializedCategory obj.
-Identity Coercion SmallSpecializedCategory_LocallySmallSpecializedCategory_Id : SmallSpecializedCategory >-> SpecializedCategory.
+Polymorphic Definition SmallSpecializedCategory (obj : Set) (*mor : obj -> obj -> Set*) := SpecializedCategory@{Set Set} obj.
+Polymorphic Identity Coercion SmallSpecializedCategory_LocallySmallSpecializedCategory_Id : SmallSpecializedCategory >-> SpecializedCategory.
 
 Polymorphic Record Category := {
   CObject : Type;
@@ -26,7 +26,7 @@ Polymorphic Definition GeneralizeCategory `(C : @SpecializedCategory obj) : Cate
   refine {| CObject := C.(Object) |}; auto.
 Defined.
 
-Coercion GeneralizeCategory : SpecializedCategory >-> Category.
+Polymorphic Coercion GeneralizeCategory : SpecializedCategory >-> Category.
 
 
 
@@ -45,17 +45,18 @@ Section SpecializedFunctor.
   }.
 End SpecializedFunctor.
 
-Global Coercion ObjectOf' : SpecializedFunctor >-> Funclass.
-(*Unset Universe Polymorphism.*)
+Global Polymorphic Coercion ObjectOf' : SpecializedFunctor >-> Funclass.
+Set Universe Polymorphism.
 Section Functor.
   Variable C D : Category.
 
   Polymorphic Definition Functor := SpecializedFunctor C D.
 End Functor.
+Unset Universe Polymorphism.
 
-Identity Coercion Functor_SpecializedFunctor_Id : Functor >-> SpecializedFunctor.
+Polymorphic Identity Coercion Functor_SpecializedFunctor_Id : Functor >-> SpecializedFunctor.
 Polymorphic Definition GeneralizeFunctor objC C objD D (F : @SpecializedFunctor objC C objD D) : Functor C D := F.
-Coercion GeneralizeFunctor : SpecializedFunctor >-> Functor.
+Polymorphic Coercion GeneralizeFunctor : SpecializedFunctor >-> Functor.
 
 Arguments SpecializedFunctor {objC} C {objD} D.
 
@@ -70,7 +71,7 @@ Polymorphic Definition GeneralizeSmallCategory `(C : @SmallSpecializedCategory o
   refine {| SObject := obj |}; destruct C; econstructor; eassumption.
 Defined.
 
-Coercion GeneralizeSmallCategory : SmallSpecializedCategory >-> SmallCategory.
+Polymorphic Coercion GeneralizeSmallCategory : SmallSpecializedCategory >-> SmallCategory.
 
 Bind Scope category_scope with SmallCategory.
 
@@ -102,13 +103,13 @@ Lemma InitialCategory_Initial : InitialObject (C := SmallCat) (DiscreteCategory
   admit.
 Qed.
 
-
+Set Universe Polymorphism.
 Section GraphObj.
   Context `(C : @SpecializedCategory objC).
 
   Inductive GraphIndex := GraphIndexSource | GraphIndexTarget.
 
-  Polymorphic Definition GraphIndex_Morphism (a b : GraphIndex) : Set :=
+  Definition GraphIndex_Morphism (a b : GraphIndex) : Set :=
     match (a, b) with
       | (GraphIndexSource, GraphIndexSource) => unit
       | (GraphIndexTarget, GraphIndexTarget) => unit
@@ -118,11 +119,11 @@ Section GraphObj.
 
   Global Arguments GraphIndex_Morphism a b /.
 
-  Polymorphic Definition GraphIndex_Compose s d d' (m1 : GraphIndex_Morphism d d') (m2 : GraphIndex_Morphism s d) :
+  Definition GraphIndex_Compose s d d' (m1 : GraphIndex_Morphism d d') (m2 : GraphIndex_Morphism s d) :
     GraphIndex_Morphism s d'.
   Admitted.
 
-  Polymorphic Definition GraphIndexingCategory : @SpecializedCategory GraphIndex.
+   Definition GraphIndexingCategory : @SpecializedCategory GraphIndex.
     refine {|
       Morphism' := GraphIndex_Morphism;
       Identity' := (fun x => match x with GraphIndexSource => tt | GraphIndexTarget => tt end);
@@ -131,7 +132,7 @@ Section GraphObj.
     admit.
   Defined.
 
-  Polymorphic Definition UnderlyingGraph_ObjectOf x :=
+  Definition UnderlyingGraph_ObjectOf x :=
     match x with
       | GraphIndexSource => { sd : objC * objC & C.(Morphism) (fst sd) (snd sd) }
       | GraphIndexTarget => objC
@@ -139,11 +140,11 @@ Section GraphObj.
 
   Global Arguments UnderlyingGraph_ObjectOf x /.
 
-  Polymorphic Definition UnderlyingGraph_MorphismOf s d (m : Morphism GraphIndexingCategory s d) :
+  Definition UnderlyingGraph_MorphismOf s d (m : Morphism GraphIndexingCategory s d) :
     UnderlyingGraph_ObjectOf s -> UnderlyingGraph_ObjectOf d.
   Admitted.
 
-  Polymorphic Definition UnderlyingGraph : SpecializedFunctor GraphIndexingCategory TypeCat.
+  Definition UnderlyingGraph : SpecializedFunctor GraphIndexingCategory TypeCat.
   Proof.
     match goal with
       | [ |- SpecializedFunctor ?C ?D ] =>
@@ -160,8 +161,17 @@ End GraphObj.
 
 Set Printing Universes.
 Set Printing All.
+
+Print Coercions.
+
+Section test.
+
 Fail Polymorphic Definition UnderlyingGraphFunctor_MorphismOf' (C D : SmallCategory) (F : SpecializedFunctor C D) :
-  Morphism (FunctorCategory TypeCat GraphIndexingCategory) (@UnderlyingGraph (SObject C) (C:SpecializedCategory (SObject C))) (UnderlyingGraph D). (* Toplevel input, characters 216-249:
+    Morphism (FunctorCategory TypeCat GraphIndexingCategory)
+    (@UnderlyingGraph (SObject C)
+                     (SmallSpecializedCategory_LocallySmallSpecializedCategory_Id (SUnderlyingCategory C)))
+    (UnderlyingGraph D).
+ (* Toplevel input, characters 216-249:
 Error:
 In environment
 C : SmallCategory (* Top.594 *)
@@ -183,3 +193,8 @@ Fail Admitted.
 Fail Polymorphic Definition UnderlyingGraphFunctor_MorphismOf (C D : SmallCategory) (F : SpecializedFunctor C D) :
   Morphism (FunctorCategory TypeCat GraphIndexingCategory) (UnderlyingGraph C) (UnderlyingGraph D). (* Anomaly: apply_coercion. Please report.*)
 Fail Admitted.
+
+Polymorphic Definition UnderlyingGraphFunctor_MorphismOf (C D : SmallCategory) (F : SpecializedFunctor C D) :
+  Morphism (FunctorCategory GraphIndexingCategory TypeCat) (UnderlyingGraph C) (UnderlyingGraph D). (* Anomaly: apply_coercion. Please report.*)
+Proof.
+Admitted.
\ No newline at end of file