Starting being more explicit on the reasons why module subtyping fails.

Note: I'm unsure about some subtyping error case apparently involving
aliases of inductive types (middle of Subtyping.check_inductive); I
bound it to some NotEqualInductiveAliases error, but this has to be
checked.

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

5 files changed, 133 insertions, 42 deletions

diff --git a/kernel/modops.ml b/kernel/modops.ml
index 2bcfada96..302d25194 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -38,7 +38,67 @@ let error_incompatible_modtypes _ _ = error "Incompatible module types."
 
 let error_not_equal _ _ = error "Non equal modules."
 
-let error_not_match l _ = error ("Signature components for label "^string_of_label l^" do not match.")
+type signature_mismatch_error =
+  | InductiveFieldExpected of mutual_inductive_body
+  | DefinitionFieldExpected
+  | ModuleFieldExpected
+  | ModuleTypeFieldExpected
+  | NotConvertibleInductiveField of identifier
+  | NotConvertibleConstructorField of identifier
+  | NotConvertibleBodyField
+  | NotConvertibleTypeField
+  | NotSameConstructorNamesField
+  | NotSameInductiveNameInBlockField
+  | FiniteInductiveFieldExpected of bool
+  | InductiveNumbersFieldExpected of int
+  | InductiveParamsNumberField of int
+  | RecordFieldExpected of bool
+  | RecordProjectionsExpected of name list
+  | NotEqualInductiveAliases
+  | NoTypeConstraintExpected
+
+let explain_not_match_error = function
+  | InductiveFieldExpected _ ->
+    strbrk "an inductive definition is expected"
+  | DefinitionFieldExpected ->
+    strbrk "a definition is expected"
+  | ModuleFieldExpected ->
+    strbrk "a module is expected"
+  | ModuleTypeFieldExpected ->
+    strbrk "a module type is expected"
+  | NotConvertibleInductiveField id | NotConvertibleConstructorField id ->
+    str "types given to " ++ str (string_of_id id) ++ str " differ"
+  | NotConvertibleBodyField ->
+    str "the body of definitions differs"
+  | NotConvertibleTypeField ->
+    str "types differ"
+  | NotSameConstructorNamesField ->
+    str "constructor names differ"
+  | NotSameInductiveNameInBlockField ->
+    str "inductive types names differ"
+  | FiniteInductiveFieldExpected isfinite ->
+    str "type is expected to be " ++
+    str (if isfinite then "coinductive" else "inductive")
+  | InductiveNumbersFieldExpected n ->
+    str "number of inductive types differs"
+  | InductiveParamsNumberField n ->
+    str "inductive type has not the right number of parameters"
+  | RecordFieldExpected isrecord ->
+    str "type is expected " ++ str (if isrecord then "" else "not ") ++
+    str "to be a record"
+  | RecordProjectionsExpected nal ->
+    (if List.length nal >= 2 then str "expected projection names are "
+     else str "expected projection name is ") ++
+    pr_enum (function Name id -> str (string_of_id id) | _ -> str "_") nal
+  | NotEqualInductiveAliases ->
+    str "Aliases to inductive types do not match"
+  | NoTypeConstraintExpected ->
+    strbrk "a definition whose type is constrained can only be subtype of a definition whose type is itself constrained"
+
+let error_not_match l _ why =
+  errorlabstrm ""
+    (str "Signature components for label " ++ str (string_of_label l) ++
+     str " do not match:" ++ spc () ++ explain_not_match_error why ++ str ".")
 
 let error_no_such_label l = error ("No such label "^string_of_label l^".")
 
diff --git a/kernel/modops.mli b/kernel/modops.mli
index f34fa88c4..cf8d62043 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -51,6 +51,27 @@ val subst_modtype_and_resolver : module_type_body -> module_path -> env ->
 
 val clean_bounded_mod_expr : struct_expr_body -> struct_expr_body
 
+(** Errors *)
+
+type signature_mismatch_error =
+  | InductiveFieldExpected of mutual_inductive_body
+  | DefinitionFieldExpected
+  | ModuleFieldExpected
+  | ModuleTypeFieldExpected
+  | NotConvertibleInductiveField of identifier
+  | NotConvertibleConstructorField of identifier
+  | NotConvertibleBodyField
+  | NotConvertibleTypeField
+  | NotSameConstructorNamesField
+  | NotSameInductiveNameInBlockField
+  | FiniteInductiveFieldExpected of bool
+  | InductiveNumbersFieldExpected of int
+  | InductiveParamsNumberField of int
+  | RecordFieldExpected of bool
+  | RecordProjectionsExpected of name list
+  | NotEqualInductiveAliases
+  | NoTypeConstraintExpected
+
 val error_existing_label : label -> 'a
 
 val error_declaration_not_path : module_struct_entry -> 'a
@@ -64,7 +85,8 @@ val error_incompatible_modtypes :
 
 val error_not_equal : module_path -> module_path -> 'a
 
-val error_not_match : label -> structure_field_body -> 'a
+val error_not_match :
+  label -> structure_field_body -> signature_mismatch_error -> 'a
 
 val error_incompatible_labels : label -> label -> 'a
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index c865c92bf..8252ffb9e 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -534,15 +534,17 @@ let dest_prod_assum env =
   in
   prodec_rec env empty_rel_context
 
+exception NotArity
+
 let dest_arity env c =
   let l, c = dest_prod_assum env c in
   match kind_of_term c with
     | Sort s -> l,s
-    | _ -> error "not an arity"
+    | _ -> raise NotArity
 
 let is_arity env c =
   try
     let _ = dest_arity env c in
     true
-  with UserError _ -> false
+  with NotArity -> false
 
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index e0f9c375b..525651493 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -76,5 +76,7 @@ val hnf_prod_applist : env -> types -> constr list -> types
 val dest_prod       : env -> types -> rel_context * types
 val dest_prod_assum : env -> types -> rel_context * types
 
-val dest_arity : env -> types -> arity
+exception NotArity
+
+val dest_arity : env -> types -> arity (* raise NotArity if not an arity *)
 val is_arity   : env -> types -> bool
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 2612afca6..808557521 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -67,26 +67,26 @@ let make_label_map mp list =
   in
     List.fold_right add_one list Labmap.empty
 
-let check_conv_error error cst f env a1 a2 =
+let check_conv_error error why cst f env a1 a2 =
   try
     union_constraints cst (f env a1 a2)
   with
-      NotConvertible -> error ()
+      NotConvertible -> error why
 
 (* for now we do not allow reorderings *)
 
 let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2= 
   let kn1 = make_mind mp1 empty_dirpath l in
   let kn2 = make_mind mp2 empty_dirpath l in
-  let error () = error_not_match l spec2 in
-  let check_conv cst f = check_conv_error error cst f in
+  let error why = error_not_match l spec2 why in
+  let check_conv why cst f = check_conv_error error why cst f in
   let mib1 =
     match info1 with
       | IndType ((_,0), mib) -> subst_mind subst1 mib
-      | _ -> error ()
+      | _ -> error (InductiveFieldExpected mib2)
   in
   let mib2 =  subst_mind subst2 mib2 in
-  let check_inductive_type cst env t1 t2 =
+  let check_inductive_type cst name 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
@@ -115,40 +115,43 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
     let s1,s2 =
       match s1, s2 with
       | Type _, Type _ -> (* shortcut here *) prop_sort, prop_sort
-      | (Prop _, Type _) | (Type _,Prop _) -> error ()
+      | (Prop _, Type _) | (Type _,Prop _) ->
+	error (NotConvertibleInductiveField name)
       | _ -> (s1, s2) in
-    check_conv cst conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2))
+    check_conv (NotConvertibleInductiveField name)
+      cst conv_leq env (mkArity (ctx1,s1)) (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);
-      check (fun p -> p.mind_typename);
+    let check f why = if f p1 <> f p2 then error why in
+      check (fun p -> p.mind_consnames) NotSameConstructorNamesField;
+      check (fun p -> p.mind_typename) NotSameInductiveNameInBlockField;
       (* nf_lc later *)
       (* nf_arity later *)
       (* user_lc ignored *)
       (* user_arity ignored *)
-      check (fun p -> p.mind_nrealargs);
+      check (fun p -> p.mind_nrealargs) (NotConvertibleInductiveField p2.mind_typename); (* How can it fail since the type of inductive are checked below? [HH] *)
       (* kelim ignored *)
       (* listrec ignored *)
       (* finite done *)
       (* nparams done *)
       (* params_ctxt done because part of the inductive types *)
       (* Don't check the sort of the type if polymorphic *)
-      let cst = check_inductive_type cst env (type_of_inductive env (mib1,p1)) (type_of_inductive env (mib2,p2))
+      let cst = check_inductive_type cst p2.mind_typename env (type_of_inductive env (mib1,p1)) (type_of_inductive env (mib2,p2))
       in
 	cst
   in
   let check_cons_types i cst p1 p2 =
-    array_fold_left2
-      (fun cst t1 t2 -> check_conv cst conv env t1 t2)
+    array_fold_left3
+      (fun cst id t1 t2 -> check_conv (NotConvertibleConstructorField id) cst conv env t1 t2)
       cst
+      p2.mind_consnames
       (arities_of_specif kn1 (mib1,p1))
       (arities_of_specif kn1 (mib2,p2))
   in
-  let check f = if f mib1 <> f mib2 then error () in
-  check (fun mib -> mib.mind_finite);
-  check (fun mib -> mib.mind_ntypes);
+  let check f why = if f mib1 <> f mib2 then error (why (f mib2)) in
+  check (fun mib -> mib.mind_finite) (fun x -> FiniteInductiveFieldExpected x);
+  check (fun mib -> mib.mind_ntypes) (fun x -> InductiveNumbersFieldExpected x);
   assert (mib1.mind_hyps=[] && mib2.mind_hyps=[]);
   assert (Array.length mib1.mind_packets >= 1
 	    && Array.length mib2.mind_packets >= 1);
@@ -158,17 +161,17 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
   (* at the time of checking the inductive arities in check_packet. *)
   (* Notice that we don't expect the local definitions to match: only *)
   (* the inductive types and constructors types have to be convertible *)
-  check (fun mib -> mib.mind_nparams);
+  check (fun mib -> mib.mind_nparams) (fun x -> InductiveParamsNumberField x);
 
   begin  
   match mind_of_delta reso2 kn2  with
       | kn2' when kn2=kn2' -> ()
       | kn2' -> 
 	  if not (eq_mind (mind_of_delta reso1 kn1) (subst_ind subst2 kn2')) then 
-	    error ()
+	    error NotEqualInductiveAliases
   end;
   (* we check that records and their field names are preserved. *)
-  check (fun mib -> mib.mind_record);
+  check (fun mib -> mib.mind_record) (fun x -> RecordFieldExpected x);
   if mib1.mind_record then begin
     let rec names_prod_letin t = match kind_of_term t with
       | Prod(n,_,t) -> n::(names_prod_letin t)
@@ -183,7 +186,8 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
     check (fun mib ->
       let nparamdecls = List.length mib.mind_params_ctxt in
       let names = names_prod_letin (mib.mind_packets.(0).mind_user_lc.(0)) in
-      snd (list_chop nparamdecls names));
+      snd (list_chop nparamdecls names))
+      (fun x -> RecordProjectionsExpected x);
   end;
   (* we first check simple things *)
   let cst =
@@ -197,7 +201,7 @@ 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 () = error_not_match l spec2 in
+  let error why = error_not_match l spec2 why in
   let check_conv cst f = check_conv_error error cst f in
   let check_type cst env t1 t2 =
 
@@ -237,13 +241,14 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
                  constraints of the form "univ <= max(...)" are not
                  expressible in the system of algebraic universes: we fail
                  (the user has to use an explicit type in the interface *)
-                error ()
-          with UserError _ (* "not an arity" *) ->
-            error () end
-        | _ -> t1,t2
+                error NoTypeConstraintExpected
+          with NotArity ->
+            error NotConvertibleTypeField end
+        | _ ->
+	  t1,t2
       else
         (t1,t2) in
-    check_conv cst conv_leq env t1 t2
+    check_conv NotConvertibleTypeField cst conv_leq env t1 t2
   in
 
   match info1 with
@@ -284,7 +289,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
 			end
 		  | None -> mkConst con
 		in
-		  check_conv cst conv env c1 c2
+		  check_conv NotConvertibleBodyField cst conv env c1 c2
 	else
 	  match cb2.const_body with
             | None -> cst
@@ -294,7 +299,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
 		  | Some lc1 -> Declarations.force lc1
 		  | None -> mkConst con
 		in
-		  check_conv cst conv env c1 c2
+		  check_conv NotConvertibleBodyField cst conv env c1 c2
       in
 	cst
    | IndType ((kn,i),mind1) ->
@@ -304,10 +309,10 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
        "inductive type and give a definition to map the old name to the new " ^
        "name."));
       assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ;
-      if cb2.const_body <> None then error () ;
+      if cb2.const_body <> None then error DefinitionFieldExpected;
       let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in
       let typ2 = Typeops.type_of_constant_type env cb2.const_type in
-       check_conv cst conv_leq env arity1 typ2
+       check_conv NotConvertibleTypeField cst conv_leq env arity1 typ2
    | IndConstr (((kn,i),j) as cstr,mind1) ->
       ignore (Util.error (
        "The kernel does not recognize yet that a parameter can be " ^
@@ -315,11 +320,11 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
        "constructor and give a definition to map the old name to the new " ^
        "name."));
       assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ;
-      if cb2.const_body <> None then error () ;
+      if cb2.const_body <> None then error DefinitionFieldExpected;
       let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in
       let ty2 = Typeops.type_of_constant_type env cb2.const_type in
-       check_conv cst conv env ty1 ty2
-   | _ -> error ()
+       check_conv NotConvertibleTypeField cst conv env ty1 ty2
+   | _ -> error DefinitionFieldExpected
 
 let rec check_modules cst env msb1 msb2 subst1 subst2 =
   let mty1 = module_type_of_module env None msb1 in
@@ -348,13 +353,13 @@ and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2=
 	      match info1 with
 		| Module msb -> check_modules cst env msb msb2 
 		    subst1 subst2
-		| _ -> error_not_match l spec2
+		| _ -> error_not_match l spec2 ModuleFieldExpected
 	    end
 	| SFBmodtype mtb2 ->
 	    let mtb1 =
 	      match info1 with
 		| Modtype mtb -> mtb
-		| _ -> error_not_match l spec2
+		| _ -> error_not_match l spec2 ModuleTypeFieldExpected
 	    in
 	    let env = add_module (module_body_of_type mtb2.typ_mp mtb2)
 	      (add_module (module_body_of_type mtb1.typ_mp mtb1) env) in