Properly handling polymorphic inductive subtyping in the kernel.

Before this patch, inductive subtyping was enforcing syntactic equality
of the variable instance, instead of reasoning up to alpha-renaming.

5 files changed, 130 insertions, 66 deletions

diff --git a/kernel/modops.ml b/kernel/modops.ml
index 24be46933..a079bc893 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -49,7 +49,7 @@ type signature_mismatch_error =
   | IncompatibleInstances
   | IncompatibleUniverses of Univ.univ_inconsistency
   | IncompatiblePolymorphism of env * types * types
-  | IncompatibleConstraints of Univ.constraints
+  | IncompatibleConstraints of Univ.AUContext.t
 
 type module_typing_error =
   | SignatureMismatch of
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 4a150d54b..e2a94b691 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -108,7 +108,7 @@ type signature_mismatch_error =
   | IncompatibleInstances
   | IncompatibleUniverses of Univ.univ_inconsistency
   | IncompatiblePolymorphism of env * types * types
-  | IncompatibleConstraints of Univ.constraints
+  | IncompatibleConstraints of Univ.AUContext.t
 
 type module_typing_error =
   | SignatureMismatch of
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 6f128d5d3..bd82dd465 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -80,10 +80,8 @@ let make_labmap mp list =
   List.fold_right add_one list empty_labmap
 
 
-let check_conv_error error why cst poly u f env a1 a2 =
+let check_conv_error error why cst poly f env a1 a2 =
   try 
-    let a1 = Vars.subst_instance_constr u a1 in
-    let a2 = Vars.subst_instance_constr u a2 in
     let cst' = f env (Environ.universes env) a1 a2 in
       if poly then 
 	if Constraint.is_empty cst' then cst
@@ -92,36 +90,42 @@ let check_conv_error error why cst poly u f env a1 a2 =
   with NotConvertible -> error why
      | Univ.UniverseInconsistency e -> error (IncompatibleUniverses e)
 
+let check_polymorphic_instance error env auctx1 auctx2 =
+  if not (Univ.AUContext.size auctx1 == Univ.AUContext.size auctx2) then
+    error IncompatibleInstances
+  else if not (UGraph.check_subtype (Environ.universes env) auctx2 auctx1) then
+    error (IncompatibleConstraints auctx1)
+  else
+    Environ.push_context ~strict:false (Univ.AUContext.repr auctx2) env
+
 (* for now we do not allow reorderings *)
 
 let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2= 
   let kn1 = KerName.make2 mp1 l in
   let kn2 = KerName.make2 mp2 l in
   let error why = error_signature_mismatch l spec2 why in
-  let check_conv why cst poly u f = check_conv_error error why cst poly u f in
+  let check_conv why cst poly f = check_conv_error error why cst poly f in
   let mib1 =
     match info1 with
       | IndType ((_,0), mib) -> Declareops.subst_mind_body subst1 mib
       | _ -> error (InductiveFieldExpected mib2)
   in
-  let u =
-    let process inst inst' =
-      if Univ.Instance.equal inst inst' then inst else error IncompatibleInstances
-    in
+  let env, inst =
     match mib1.mind_universes, mib2.mind_universes with
-    | Monomorphic_ind _, Monomorphic_ind _ -> Univ.Instance.empty
+    | Monomorphic_ind _, Monomorphic_ind _ -> env, Univ.Instance.empty
     | Polymorphic_ind auctx, Polymorphic_ind auctx' ->
-      process
-        (Univ.AUContext.instance auctx) (Univ.AUContext.instance auctx')
+      let env = check_polymorphic_instance error env auctx auctx' in
+      env, Univ.make_abstract_instance auctx'
     | Cumulative_ind cumi, Cumulative_ind cumi' ->
-      process
-        (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi))
-        (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi'))
+      let auctx = Univ.ACumulativityInfo.univ_context cumi in
+      let auctx' = Univ.ACumulativityInfo.univ_context cumi' in
+      let env = check_polymorphic_instance error env auctx auctx' in
+      env, Univ.make_abstract_instance auctx'
     | _ -> error 
              (CumulativeStatusExpected (Declareops.inductive_is_cumulative mib2))
   in
   let mib2 =  Declareops.subst_mind_body subst2 mib2 in
-  let check_inductive_type cst name env t1 t2 =
+  let check_inductive_type cst name t1 t2 =
 
     (* Due to template polymorphism, the conclusions of
        t1 and t2, if in Type, are generated as the least upper bounds
@@ -154,7 +158,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
 	error (NotConvertibleInductiveField name)
       | _ -> (s1, s2) in
     check_conv (NotConvertibleInductiveField name)
-      cst (inductive_is_polymorphic mib1) u infer_conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2))
+      cst (inductive_is_polymorphic mib1) infer_conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2))
   in
 
   let check_packet cst p1 p2 =
@@ -172,21 +176,20 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
       (* nparams done *)
       (* params_ctxt done because part of the inductive types *)
       (* Don't check the sort of the type if polymorphic *)
-      let ty1, cst1 = constrained_type_of_inductive env ((mib1,p1),u) in
-      let ty2, cst2 = constrained_type_of_inductive env ((mib2,p2),u) in
-      let cst = Constraint.union cst1 (Constraint.union cst2 cst) in
-      let cst = check_inductive_type cst p2.mind_typename env ty1 ty2 in
+      let ty1 = type_of_inductive env ((mib1, p1), inst) in
+      let ty2 = type_of_inductive env ((mib2, p2), inst) in
+      let cst = check_inductive_type cst p2.mind_typename ty1 ty2 in
 	cst
   in
   let mind = mind_of_kn kn1 in
   let check_cons_types i cst p1 p2 =
     Array.fold_left3
       (fun cst id t1 t2 -> check_conv (NotConvertibleConstructorField id) cst
-	(inductive_is_polymorphic mib1) u infer_conv env t1 t2)
+	(inductive_is_polymorphic mib1) infer_conv env t1 t2)
       cst
       p2.mind_consnames
-      (arities_of_specif (mind,u) (mib1,p1))
-      (arities_of_specif (mind,u) (mib2,p2))
+      (arities_of_specif (mind, inst) (mib1, p1))
+      (arities_of_specif (mind, inst) (mib2, p2))
   in
   let check f test why = if not (test (f mib1) (f mib2)) then error (why (f mib2)) in
   check (fun mib -> mib.mind_finite<>Decl_kinds.CoFinite) (==) (fun x -> FiniteInductiveFieldExpected x);
@@ -242,8 +245,8 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
     
 let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = 
   let error why = error_signature_mismatch l spec2 why in
-  let check_conv cst poly u f = check_conv_error error cst poly u f in
-  let check_type poly u cst env t1 t2 =
+  let check_conv cst poly f = check_conv_error error cst poly f in
+  let check_type poly cst env t1 t2 =
 
     let err = NotConvertibleTypeField (env, t1, t2) in
 
@@ -290,7 +293,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
 	  t1,t2
       else
         (t1,t2) in
-      check_conv err cst poly u infer_conv_leq env t1 t2
+      check_conv err cst poly infer_conv_leq env t1 t2
   in
   match info1 with
     | Constant cb1 ->
@@ -298,48 +301,21 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
       let cb1 = Declareops.subst_const_body subst1 cb1 in
       let cb2 = Declareops.subst_const_body subst2 cb2 in
       (* Start by checking universes *)
-      let poly = 
-	if not (Declareops.constant_is_polymorphic cb1 
-                 == Declareops.constant_is_polymorphic cb2) then
-           error (PolymorphicStatusExpected (Declareops.constant_is_polymorphic cb2))
-	else Declareops.constant_is_polymorphic cb2
-      in
-      let cst', env', u =
+      let poly, env =
         match cb1.const_universes, cb2.const_universes with
         | Monomorphic_const _, Monomorphic_const _ ->
-          cst, env, Univ.Instance.empty
+          false, env
         | Polymorphic_const auctx1, Polymorphic_const auctx2 ->
-          begin
-	    let ctx1 = Univ.instantiate_univ_context auctx1 in
-	    let ctx2 = Univ.instantiate_univ_context auctx2 in
-	    let inst1, ctx1 = Univ.UContext.dest ctx1 in
-	    let inst2, ctx2 = Univ.UContext.dest ctx2 in
-	    if not (Univ.Instance.length inst1 == Univ.Instance.length inst2) then
-	      error IncompatibleInstances
-	    else 
-	      let cstrs = Univ.enforce_eq_instances inst1 inst2 cst in
-	      let cstrs = Univ.Constraint.union cstrs ctx2 in
-	      try 
-		(* The environment with the expected universes plus equality 
-		   of the body instances with the expected instance *)
-		let ctxi = Univ.Instance.append inst1 inst2 in
-		let ctx = Univ.UContext.make (ctxi, cstrs) in
-		let env = Environ.push_context ctx env in
-		(* Check that the given definition does not add any constraint over
-		   the expected ones, so that it can be used in place of 
-                                 the original. *)
-		if UGraph.check_constraints ctx1 (Environ.universes env) then
-		  cstrs, env, inst2
-		else error (IncompatibleConstraints ctx1)
-	      with Univ.UniverseInconsistency incon -> 
-		error (IncompatibleUniverses incon)
-          end
-        | _ -> assert false
+          true, check_polymorphic_instance error env auctx1 auctx2
+        | Monomorphic_const _, Polymorphic_const _ ->
+          error (PolymorphicStatusExpected true)
+        | Polymorphic_const _, Monomorphic_const _ ->
+          error (PolymorphicStatusExpected false)
       in
       (* Now check types *)
-      let typ1 = Typeops.type_of_constant_type env' cb1.const_type in
-      let typ2 = Typeops.type_of_constant_type env' cb2.const_type in
-      let cst = check_type poly u cst env' typ1 typ2 in
+      let typ1 = Typeops.type_of_constant_type env cb1.const_type in
+      let typ2 = Typeops.type_of_constant_type env cb2.const_type in
+      let cst = check_type poly cst env typ1 typ2 in
       (* Now we check the bodies:
 	 - A transparent constant can only be implemented by a compatible
 	   transparent constant.
@@ -356,7 +332,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
 		 Anyway [check_conv] will handle that afterwards. *)
 	      let c1 = Mod_subst.force_constr lc1 in
 	      let c2 = Mod_subst.force_constr lc2 in
-	      check_conv NotConvertibleBodyField cst poly u infer_conv env' c1 c2))
+	      check_conv NotConvertibleBodyField cst poly infer_conv env c1 c2))
    | IndType ((kn,i),mind1) ->
        CErrors.user_err Pp.(str @@
        "The kernel does not recognize yet that a parameter can be " ^
diff --git a/test-suite/modules/polymorphism2.v b/test-suite/modules/polymorphism2.v
new file mode 100644
index 000000000..7e3327eee
--- /dev/null
+++ b/test-suite/modules/polymorphism2.v
@@ -0,0 +1,87 @@
+Set Universe Polymorphism.
+
+(** Tests for module subtyping of polymorphic terms *)
+
+Module Type S.
+
+Section Foo.
+
+Universes i j.
+Constraint i <= j.
+
+Inductive foo : Type@{i} -> Type@{j} :=.
+
+End Foo.
+
+End S.
+
+(** Same constraints *)
+
+Module OK_1.
+
+Section Foo.
+
+Universes i j.
+Constraint i <= j.
+
+Inductive foo : Type@{i} -> Type@{j} :=.
+
+End Foo.
+
+End OK_1.
+
+Module OK_1_Test : S := OK_1.
+
+(** More general constraints *)
+
+Module OK_2.
+
+Inductive foo@{i j} : Type@{i} -> Type@{j} :=.
+
+End OK_2.
+
+Module OK_2_Test : S := OK_2.
+
+(** Wrong instance length *)
+
+Module KO_1.
+
+Inductive foo@{i} : Type@{i} -> Type@{i} :=.
+
+End KO_1.
+
+Fail Module KO_Test_1 : S := KO_1.
+
+(** Less general constraints *)
+
+Module KO_2.
+
+Section Foo.
+
+Universe i j.
+Constraint i < j.
+
+Inductive foo : Type@{i} -> Type@{j} :=.
+
+End Foo.
+
+End KO_2.
+
+Fail Module KO_Test_2 : S := KO_2.
+
+(** Less general constraints *)
+
+Module KO_3.
+
+Section Foo.
+
+Universe i j.
+Constraint i = j.
+
+Inductive foo : Type@{i} -> Type@{j} :=.
+
+End Foo.
+
+End KO_3.
+
+Fail Module KO_Test_3 : S := KO_3.
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index ca3fb392f..86dcb6d4d 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -909,6 +909,7 @@ let explain_not_match_error = function
       quote (Printer.safe_pr_lconstr_env env Evd.empty t2)
   | IncompatibleConstraints cst ->
     str " the expected (polymorphic) constraints do not imply " ++
+      let cst = Univ.UContext.constraints (Univ.instantiate_univ_context cst) in
       quote (Univ.pr_constraints (Termops.pr_evd_level Evd.empty) cst)
 
 let explain_signature_mismatch l spec why =