Implement module subtyping for polymorphic constants (errors on

inductives).
The implementation constant should have the a universe instance
of the same length, we assume the universes are in the same order
and we check that the definition does not add any constraints
to the expected ones. This fixes bug #3670.

1 files changed, 61 insertions, 17 deletions

diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index f1402a3db..4f54220e7 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -79,8 +79,15 @@ let make_labmap mp list =
   List.fold_right add_one list empty_labmap
 
 
-let check_conv_error error why cst f env a1 a2 =
-  try Constraint.union cst (f env (Environ.universes env) a1 a2)
+let check_conv_error error why cst poly u 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
+	else error (IncompatiblePolymorphism (env, a1, a2))
+      else Constraint.union cst cst'
   with NotConvertible -> error why
 
 (* for now we do not allow reorderings *)
@@ -89,15 +96,21 @@ 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 f = check_conv_error error why cst f in
+  let check_conv why cst poly u f = check_conv_error error why cst poly u f in
   let mib1 =
     match info1 with
       | IndType ((_,0), mib) -> Declareops.subst_mind_body subst1 mib
       | _ -> error (InductiveFieldExpected mib2)
   in
+  let poly = 
+    if not (mib1.mind_polymorphic == mib2.mind_polymorphic) then
+      error (PolymorphicStatusExpected mib2.mind_polymorphic)
+    else mib2.mind_polymorphic
+  in
   let u = 
-    if mib1.mind_polymorphic then 
-      UContext.instance mib1.mind_universes 
+    if poly then 
+      Errors.error ("Checking of subtyping of polymorphic" ^
+		       " inductive types not implemented")
     else Instance.empty
   in
   let mib2 =  Declareops.subst_mind_body subst2 mib2 in
@@ -134,7 +147,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 infer_conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2))
+      cst poly u infer_conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2))
   in
 
   let check_packet cst p1 p2 =
@@ -161,7 +174,8 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
   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 infer_conv env t1 t2)
+      (fun cst id t1 t2 -> check_conv (NotConvertibleConstructorField id) cst
+	poly u infer_conv env t1 t2)
       cst
       p2.mind_consnames
       (arities_of_specif (mind,u) (mib1,p1))
@@ -221,8 +235,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 f = check_conv_error error cst f in
-  let check_type cst env t1 t2 =
+  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 err = NotConvertibleTypeField (env, t1, t2) in
 
@@ -269,17 +283,47 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
 	  t1,t2
       else
         (t1,t2) in
-    check_conv err cst infer_conv_leq env t1 t2
+      check_conv err cst poly u infer_conv_leq env t1 t2
   in
   match info1 with
     | Constant cb1 ->
       let () = assert (List.is_empty cb1.const_hyps && List.is_empty cb2.const_hyps) in
       let cb1 = Declareops.subst_const_body subst1 cb1 in
       let cb2 = Declareops.subst_const_body subst2 cb2 in
-      (* Start by checking 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 cst env typ1 typ2 in
+      (* Start by checking universes *)
+      let poly = 
+	if not (cb1.const_polymorphic == cb2.const_polymorphic) then
+	  error (PolymorphicStatusExpected cb2.const_polymorphic)
+	else cb2.const_polymorphic
+      in
+      let cst', env', u = 
+	if poly then 
+	  let ctx1 = Univ.instantiate_univ_context cb1.const_universes in
+	  let ctx2 = Univ.instantiate_univ_context cb2.const_universes 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 env = Environ.add_constraints cstrs 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 Univ.check_constraints ctx1 (Environ.universes env) then
+		      cstrs, env, inst2
+		    else error (IncompatibleConstraints ctx1)
+		with Univ.UniverseInconsistency incon -> 
+		  error (IncompatibleUniverses incon)
+	else cst, env, Univ.Instance.empty
+      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
       (* Now we check the bodies:
 	 - A transparent constant can only be implemented by a compatible
 	   transparent constant.
@@ -296,7 +340,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 infer_conv env c1 c2))
+	      check_conv NotConvertibleBodyField cst poly u infer_conv env' c1 c2))
    | IndType ((kn,i),mind1) ->
        ignore (Errors.error (
        "The kernel does not recognize yet that a parameter can be " ^
@@ -312,7 +356,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
       let typ2 = Typeops.type_of_constant_type env cb2.const_type in
       let cst = Constraint.union cst (Constraint.union cst1 cst2) in
       let error = NotConvertibleTypeField (env, arity1, typ2) in
-       check_conv error cst infer_conv_leq env arity1 typ2
+       check_conv error cst false Univ.Instance.empty infer_conv_leq env arity1 typ2
    | IndConstr (((kn,i),j) as cstr,mind1) ->
       ignore (Errors.error (
        "The kernel does not recognize yet that a parameter can be " ^
@@ -327,7 +371,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
       let ty2 = Typeops.type_of_constant_type env cb2.const_type in
       let cst = Constraint.union cst (Constraint.union cst1 cst2) in
       let error = NotConvertibleTypeField (env, ty1, ty2) in
-       check_conv error cst infer_conv env ty1 ty2
+       check_conv error cst false Univ.Instance.empty infer_conv env ty1 ty2
 
 let rec check_modules cst env msb1 msb2 subst1 subst2 =
   let mty1 = module_type_of_module msb1 in