Correction bug #1302

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9494 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 339 insertions, 1 deletions

diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 12c7144114..eb7f26cf49 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -81,6 +81,41 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
       | IndType ((_,0), mib) -> mib
       | _ -> error ()
   in
+  let check_inductive_type cst env t1 t2 =
+
+    (* Due to sort-polymorphism in inductive types, the conclusions of
+       t1 and t2, if in Type, are generated as the least upper bounds
+       of the types of the constructors. 
+
+       By monotonicity of the infered l.u.b.  wrt subtyping (i.e.  if X:U
+       |- T(X):s and |- M:U' and U'<=U then infer_type(T(M))<=s), each
+       universe in the conclusion of t1 has an bounding universe in
+       the conclusion of t2, so that we don't need to check the
+       subtyping of the conclusions of t1 and t2.
+
+       Even if we'd like to recheck it, the inference of constraints
+       is not designed to deal with algebraic constraints of the form
+       max-univ(u1..un) <= max-univ(u'1..u'n), so that it is not easy
+       to recheck it (in short, we would need the actual graph of
+       constraints as input while type checking is currently designed
+       to output a set of constraints instead) *)
+
+    (* So we cheat and replace the subtyping problem on algebraic
+       constraints of the form max-univ(u1..un) <= max-univ(u'1..u'n)
+       (that we know are necessary true) by trivial constraints that
+       the constraint generator knows how to deal with *)
+
+    let (ctx1,s1) = dest_arity env t1 in
+    let (ctx2,s2) = dest_arity env t2 in
+    let s1,s2 =
+      match s1, s2 with
+      | Type _, Type _ -> (* shortcut here *) mk_Prop, mk_Prop
+      | (Prop _, Type _) | (Type _,Prop _) -> error ()
+      | _ -> (s1, s2) in
+    check_conv cst conv_leq env 
+      (Sign.mkArity (ctx1,s1)) (Sign.mkArity (ctx2,s2))
+  in
+
   let check_packet cst p1 p2 =
     let check f = if f p1 <> f p2 then error () in
       check (fun p -> p.mind_consnames);
@@ -96,7 +131,7 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
       (* nparams done *)
       (* params_ctxt done because part of the inductive types *)
       (* Don't check the sort of the type if polymorphic *)
-      let cst = check_conv cst conv env (type_of_inductive env (mib1,p1)) (type_of_inductive env (mib2,p2))
+      let cst = check_inductive_type cst env (type_of_inductive env (mib1,p1)) (type_of_inductive env (mib2,p2))
       in
 	cst
   in
diff --git a/test-suite/failure/subtyping.v b/test-suite/failure/subtyping.v
new file mode 100644
index 0000000000..35fd20369f
--- /dev/null
+++ b/test-suite/failure/subtyping.v
@@ -0,0 +1,21 @@
+(* A variant of bug #1302 that must fail *)
+
+Module Type T.
+
+ Parameter A : Type.
+
+ Inductive L : Prop := 
+ | L0
+ | L1 :  (A -> Prop) -> L.
+
+End T.
+
+Module TT : T. 
+
+ Parameter A : Type.
+
+ Inductive L : Type := 
+ | L0
+ | L1 :  (A -> Prop) -> L.
+
+End TT.
diff --git a/test-suite/failure/subtyping2.v b/test-suite/failure/subtyping2.v
new file mode 100644
index 0000000000..0a75ae4565
--- /dev/null
+++ b/test-suite/failure/subtyping2.v
@@ -0,0 +1,245 @@
+(* Check that no constraints on inductive types disappear at subtyping *)
+
+Module Type S.
+
+Record A0 : Type :=  (* Type_i' *)
+  i0 {X0 : Type; R0 : X0 -> X0 -> Prop}. (* X0: Type_j' *)
+
+Variable i0' : forall X0 : Type, (X0 -> X0 -> Prop) -> A0.
+
+End S.
+
+Module M.
+
+Record A0 : Type :=  (* Type_i' *)
+  i0 {X0 : Type; R0 : X0 -> X0 -> Prop}. (* X0: Type_j' *)
+
+Definition i0' := i0 : forall X0 : Type, (X0 -> X0 -> Prop) -> A0.
+
+End M.
+
+(* The rest of this file formalizes Burali-Forti paradox *)
+(* (if the constraint between i0' and A0 is lost, the proof goes through) *)
+
+  Inductive ACC (A : Type) (R : A -> A -> Prop) : A -> Prop :=
+      ACC_intro :
+        forall x : A, (forall y : A, R y x -> ACC A R y) -> ACC A R x.
+
+  Lemma ACC_nonreflexive :
+   forall (A : Type) (R : A -> A -> Prop) (x : A),
+   ACC A R x -> R x x -> False.
+simple induction 1; intros.
+exact (H1 x0 H2 H2).
+Qed.
+
+  Definition WF (A : Type) (R : A -> A -> Prop) := forall x : A, ACC A R x.
+
+
+Section Inverse_Image.
+
+  Variables (A B : Type) (R : B -> B -> Prop) (f : A -> B).
+
+  Definition Rof (x y : A) : Prop := R (f x) (f y).
+
+  Remark ACC_lemma :
+   forall y : B, ACC B R y -> forall x : A, y = f x -> ACC A Rof x.
+    simple induction 1; intros.
+    constructor; intros.
+    apply (H1 (f y0)); trivial.
+    elim H2 using eq_ind_r; trivial.
+    Qed.
+
+  Lemma ACC_inverse_image : forall x : A, ACC B R (f x) -> ACC A Rof x.
+    intros; apply (ACC_lemma (f x)); trivial.
+    Qed.
+
+  Lemma WF_inverse_image : WF B R -> WF A Rof.
+    red in |- *; intros; apply ACC_inverse_image; auto.
+    Qed.
+
+End Inverse_Image.
+
+Section Burali_Forti_Paradox.
+
+  Definition morphism (A : Type) (R : A -> A -> Prop) 
+    (B : Type) (S : B -> B -> Prop) (f : A -> B) :=
+    forall x y : A, R x y -> S (f x) (f y).
+
+  (* The hypothesis of the paradox:
+     assumes there exists an universal system of notations, i.e:
+      - A type A0
+      - An injection i0 from relations on any type into A0
+      - The proof that i0 is injective modulo morphism 
+   *)
+  Variable A0 : Type.                     (* Type_i *)
+  Variable i0 : forall X : Type, (X -> X -> Prop) -> A0. (* X: Type_j *)
+  Hypothesis
+    inj :
+      forall (X1 : Type) (R1 : X1 -> X1 -> Prop) (X2 : Type)
+        (R2 : X2 -> X2 -> Prop),
+      i0 X1 R1 = i0 X2 R2 -> exists f : X1 -> X2, morphism X1 R1 X2 R2 f.
+
+  (* Embedding of x in y: x and y are images of 2 well founded relations
+     R1 and R2, the ordinal of R2 being strictly greater than that of R1.
+   *)
+  Record emb (x y : A0) : Prop := 
+    {X1 : Type;
+     R1 : X1 -> X1 -> Prop;
+     eqx : x = i0 X1 R1;
+     X2 : Type;
+     R2 : X2 -> X2 -> Prop;
+     eqy : y = i0 X2 R2;
+     W2 : WF X2 R2;
+     f : X1 -> X2;
+     fmorph : morphism X1 R1 X2 R2 f;
+     maj : X2;
+     majf : forall z : X1, R2 (f z) maj}.
+
+
+  Lemma emb_trans : forall x y z : A0, emb x y -> emb y z -> emb x z.
+intros.
+case H; intros.
+case H0; intros.
+generalize eqx0; clear eqx0.
+elim eqy using eq_ind_r; intro.
+case (inj _ _ _ _ eqx0); intros.
+exists X1 R1 X3 R3 (fun x : X1 => f0 (x0 (f x))) maj0; trivial.
+red in |- *; auto.
+Defined.
+
+
+  Lemma ACC_emb :
+   forall (X : Type) (R : X -> X -> Prop) (x : X),
+   ACC X R x ->
+   forall (Y : Type) (S : Y -> Y -> Prop) (f : Y -> X),
+   morphism Y S X R f -> (forall y : Y, R (f y) x) -> ACC A0 emb (i0 Y S).
+simple induction 1; intros.
+constructor; intros.
+case H4; intros.
+elim eqx using eq_ind_r.
+case (inj X2 R2 Y S).
+apply sym_eq; assumption.
+
+intros.
+apply H1 with (y := f (x1 maj)) (f := fun x : X1 => f (x1 (f0 x)));
+ try red in |- *; auto.
+Defined.
+
+  (* The embedding relation is well founded *)
+  Lemma WF_emb : WF A0 emb.
+constructor; intros.
+case H; intros.
+elim eqx using eq_ind_r.
+apply ACC_emb with (X := X2) (R := R2) (x := maj) (f := f); trivial.
+Defined.
+
+
+  (* The following definition enforces Type_j >= Type_i *)
+  Definition Omega : A0 := i0 A0 emb.
+
+
+Section Subsets.
+
+  Variable a : A0.
+
+  (* We define the type of elements of A0 smaller than a w.r.t embedding.
+     The Record is in Type, but it is possible to avoid such structure. *)
+  Record sub : Type :=  {witness : A0; emb_wit : emb witness a}.
+
+  (* F is its image through i0 *)
+  Definition F : A0 := i0 sub (Rof _ _ emb witness).
+
+  (* F is embedded in Omega:
+     - the witness projection is a morphism
+     - a is an upper bound because emb_wit proves that witness is
+       smaller than a.
+   *)
+  Lemma F_emb_Omega : emb F Omega.
+exists sub (Rof _ _ emb witness) A0 emb witness a; trivial.
+exact WF_emb.
+
+red in |- *; trivial.
+
+exact emb_wit.
+Defined.
+
+End Subsets.
+
+
+  Definition fsub (a b : A0) (H : emb a b) (x : sub a) : 
+    sub b := Build_sub _ (witness _ x) (emb_trans _ _ _ (emb_wit _ x) H).
+
+  (* F is a morphism: a < b => F(a) < F(b)
+      - the morphism from F(a) to F(b) is fsub above
+      - the upper bound is a, which is in F(b) since a < b
+   *)
+  Lemma F_morphism : morphism A0 emb A0 emb F.
+red in |- *; intros.
+exists
+ (sub x)
+   (Rof _ _ emb (witness x))
+   (sub y)
+   (Rof _ _ emb (witness y))
+   (fsub x y H)
+   (Build_sub _ x H); trivial.
+apply WF_inverse_image.
+exact WF_emb.
+
+unfold morphism, Rof, fsub in |- *; simpl in |- *; intros.
+trivial.
+
+unfold Rof, fsub in |- *; simpl in |- *; intros.
+apply emb_wit.
+Defined.
+
+
+  (* Omega is embedded in itself:
+     - F is a morphism
+     - Omega is an upper bound of the image of F
+   *)
+  Lemma Omega_refl : emb Omega Omega.
+exists A0 emb A0 emb F Omega; trivial.
+exact WF_emb.
+
+exact F_morphism.
+
+exact F_emb_Omega.
+Defined.
+
+  (* The paradox is that Omega cannot be embedded in itself, since
+     the embedding relation is well founded.
+   *)
+  Theorem Burali_Forti : False.
+apply ACC_nonreflexive with A0 emb Omega.
+apply WF_emb.
+
+exact Omega_refl.
+
+Defined.
+
+End Burali_Forti_Paradox.
+
+Import M.
+
+  (* Note: this proof uses a large elimination of A0. *)
+  Lemma inj :
+   forall (X1 : Type) (R1 : X1 -> X1 -> Prop) (X2 : Type)
+     (R2 : X2 -> X2 -> Prop),
+   i0' X1 R1 = i0' X2 R2 -> exists f : X1 -> X2, morphism X1 R1 X2 R2 f.
+intros.
+change
+  match i0' X1 R1, i0' X2 R2 with
+  | i0 x1 r1, i0 x2 r2 => exists f : _, morphism x1 r1 x2 r2 f
+  end in |- *.
+case H; simpl in |- *.
+exists (fun x : X1 => x).
+red in |- *; trivial.
+Defined.
+
+(* The following command raises 'Error: Universe Inconsistency'.
+   To allow large elimination of A0, i0 must not be a large constructor.
+   Hence, the constraint Type_j' < Type_i' is added, which is incompatible
+   with the constraint j >= i in the paradox.
+*)
+
+  Definition Paradox : False := Burali_Forti A0 i0' inj.
diff --git a/test-suite/modules/subtyping.v b/test-suite/modules/subtyping.v
new file mode 100644
index 0000000000..fb3eae3af5
--- /dev/null
+++ b/test-suite/modules/subtyping.v
@@ -0,0 +1,37 @@
+(* Non regression for bug #1302 *)
+
+(* With universe polymorphism for inductive types, subtyping of
+   inductive types needs a special treatment: the standard conversion
+   algorithm does not work as it only knows to deal with constraints of
+   the form alpha = beta or max(alphas, alphas+1) <= beta, while
+   subtyping of inductive types in Type generates constraints of the form
+   max(alphas, alphas+1) <= max(betas, betas+1).
+
+   These constraints are anyway valid by monotonicity of subtyping but we
+   have to detect it early enough to avoid breaking the standard
+   algorithm for constraints on algebraic universes. *)
+
+Module Type T.
+
+ Parameter A : Type (* Top.1 *) .
+
+ Inductive L : Type (* max(Top.1,1) *) := 
+ | L0
+ | L1 :  (A -> Prop) -> L.
+
+End T.
+
+Axiom Tp : Type (* Top.5 *) .
+
+Module TT : T. 
+
+ Definition A : Type (* Top.6 *) := Tp. (* generates Top.5 <= Top.6 *)
+
+ Inductive L : Type (* max(Top.6,1) *) := 
+ | L0
+ | L1 :  (A -> Prop) -> L.
+
+End TT. (* Generates Top.6 <= Top.1 (+ auxiliary constraints for L_rect) *)
+
+(* Note: Top.6 <= Top.1 is generated by subtyping on A; 
+   subtyping of L follows and has not to be checked *)