Robust display of NotConvertibleTypeField errors (fix #3008, #2995)

 Since the nametab isn't aware of everything needed to print mismatched
 types (cf the bug test-cases), we create a robust term printer that
 known how to print a fully-qualified name when [shortest_qualid_of_global]
 has failed. These Printer.safe_pr_constr and alii are meant to never fail
 (at worse they display "??", for instance when the env isn't rich enough).

 Moreover, the environnement may have changed between the raise
 of NotConvertibleTypeField and its display, so we store the original
 env in the exception.

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

12 files changed, 143 insertions, 28 deletions

diff --git a/dev/base_include b/dev/base_include
index c75413a386..ca40f5f7af 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -210,8 +210,8 @@ let pf_e gl s =
 
 (* Set usual printing since the global env is available from the tracer *)
 let _ = Constrextern.in_debugger := false
-let _ = Constrextern.set_debug_global_reference_printer
-  (fun loc r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));;
+let _ = Constrextern.set_extern_reference
+  (fun loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));;
 
 open Toplevel
 let go = loop
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index db895fc0f7..ec9c0a95ee 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -454,7 +454,7 @@ let encode_path loc prefix mpdir suffix id =
   Qualid (loc, make_qualid
     (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id)
 
-let raw_string_of_ref loc = function
+let raw_string_of_ref loc _ = function
   | ConstRef cst ->
       let (mp,dir,id) = repr_con cst in
       encode_path loc "CST" (Some (mp,dir)) [] (Label.to_id id)
@@ -470,7 +470,7 @@ let raw_string_of_ref loc = function
   | VarRef id ->
       encode_path loc "SECVAR" None [] id
 
-let short_string_of_ref loc = function
+let short_string_of_ref loc _ = function
   | VarRef id -> Ident (loc,id)
   | ConstRef cst -> Ident (loc,Label.to_id (pi3 (repr_con cst)))
   | IndRef (kn,0) -> Ident (loc,Label.to_id (pi3 (repr_mind kn)))
@@ -486,5 +486,5 @@ let short_string_of_ref loc = function
    pretty-printer should not make calls to the global env since ocamldebug
    runs in a different process and does not have the proper env at hand *)
 let _ = Constrextern.in_debugger := true
-let _ = Constrextern.set_debug_global_reference_printer
+let _ = Constrextern.set_extern_reference
   (if !rawdebug then raw_string_of_ref else short_string_of_ref)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 47753c1582..84baefe615 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -140,20 +140,21 @@ let insert_pat_alias loc p = function
 let extern_evar loc n l =
   if !print_evar_arguments then CEvar (loc,n,l) else CEvar (loc,n,None)
 
-let debug_global_reference_printer =
-  ref (fun _ -> failwith "Cannot print a global reference")
+(** We allow customization of the global_reference printer.
+    For instance, in the debugger the tables of global references
+    may be inaccurate *)
 
-let in_debugger = ref false
+let default_extern_reference loc vars r =
+  Qualid (loc,shortest_qualid_of_global vars r)
 
-let set_debug_global_reference_printer f =
-  debug_global_reference_printer := f
+let my_extern_reference = ref default_extern_reference
 
-let extern_reference loc vars r =
-  if !in_debugger then
-    (* Debugger does not have the tables of global reference at hand *)
-    !debug_global_reference_printer loc r
-  else
-    Qualid (loc,shortest_qualid_of_global vars r)
+let set_extern_reference f = my_extern_reference := f
+let get_extern_reference () = !my_extern_reference
+
+let extern_reference loc vars l = !my_extern_reference loc vars l
+
+let in_debugger = ref false
 
 (**********************************************************************)
 (* mapping patterns to cases_pattern_expr                                *)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 0e40e83e67..0a4192c3ea 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -51,9 +51,12 @@ val print_universes : bool ref
 val print_no_symbol : bool ref
 val print_projections : bool ref
 
-(** Debug printing options *)
-val set_debug_global_reference_printer :
-  (Loc.t -> global_reference -> reference) -> unit
+(** Customization of the global_reference printer *)
+val set_extern_reference :
+  (Loc.t -> Id.Set.t -> global_reference -> reference) -> unit
+val get_extern_reference :
+  unit -> (Loc.t -> Id.Set.t -> global_reference -> reference)
+
 val in_debugger : bool ref
 
 (** This governs printing of implicit arguments. If [with_implicits] is
diff --git a/kernel/modops.ml b/kernel/modops.ml
index c1b5d788d3..6c46ad5103 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -33,7 +33,7 @@ type signature_mismatch_error =
   | NotConvertibleInductiveField of Id.t
   | NotConvertibleConstructorField of Id.t
   | NotConvertibleBodyField
-  | NotConvertibleTypeField of types * types
+  | NotConvertibleTypeField of env * types * types
   | NotSameConstructorNamesField
   | NotSameInductiveNameInBlockField
   | FiniteInductiveFieldExpected of bool
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 600e631a7c..66aadd124c 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -60,7 +60,7 @@ type signature_mismatch_error =
   | NotConvertibleInductiveField of Id.t
   | NotConvertibleConstructorField of Id.t
   | NotConvertibleBodyField
-  | NotConvertibleTypeField of types * types
+  | NotConvertibleTypeField of env * types * types
   | NotSameConstructorNamesField
   | NotSameInductiveNameInBlockField
   | FiniteInductiveFieldExpected of bool
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index e5b81c72f6..99c1b8483e 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -219,7 +219,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
   let check_conv cst f = check_conv_error error cst f in
   let check_type cst env t1 t2 =
 
-    let err = NotConvertibleTypeField (t1, t2) in
+    let err = NotConvertibleTypeField (env, t1, t2) in
 
     (* If the type of a constant is generated, it may mention
        non-variable algebraic universes that the general conversion
@@ -303,7 +303,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
       if Declareops.constant_has_body cb2 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
-      let error = NotConvertibleTypeField (arity1, typ2) in
+      let error = NotConvertibleTypeField (env, arity1, typ2) in
        check_conv error cst conv_leq env arity1 typ2
    | IndConstr (((kn,i),j) as cstr,mind1) ->
       ignore (Errors.error (
@@ -315,7 +315,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
       if Declareops.constant_has_body cb2 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
-      let error = NotConvertibleTypeField (ty1, ty2) in
+      let error = NotConvertibleTypeField (env, ty1, ty2) in
        check_conv error cst conv env ty1 ty2
 
 let rec check_modules cst env msb1 msb2 subst1 subst2 =
diff --git a/printing/printer.ml b/printing/printer.ml
index ea6e798766..8fc38bc6c8 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -21,6 +21,7 @@ open Refiner
 open Pfedit
 open Constrextern
 open Ppconstr
+open Declarations
 
 let emacs_str s =
   if !Flags.print_emacs then s else ""
@@ -120,6 +121,63 @@ let pr_univ_cstr (c:Univ.constraints) =
   else
     mt()
 
+
+(** Term printers resilient to [Nametab] errors *)
+
+(** When the nametab isn't up-to-date, the term printers above
+    could raise [Not_found] during [Nametab.shortest_qualid_of_global].
+    In this case, we build here a fully-qualified name based upon
+    the kernel modpath and label of constants, and the idents in
+    the [mutual_inductive_body] for the inductives and constructors
+    (needs an environment for this). *)
+
+let id_of_global env = function
+  | ConstRef kn -> Label.to_id (Constant.label kn)
+  | IndRef (kn,0) -> Label.to_id (MutInd.label kn)
+  | IndRef (kn,i) ->
+    (Environ.lookup_mind kn env).mind_packets.(i).mind_typename
+  | ConstructRef ((kn,i),j) ->
+    (Environ.lookup_mind kn env).mind_packets.(i).mind_consnames.(j-1)
+  | VarRef v -> v
+
+let cons_dirpath id dp = DirPath.make (id :: DirPath.repr dp)
+
+let rec dirpath_of_mp = function
+  | MPfile sl -> sl
+  | MPbound uid -> DirPath.make [MBId.to_id uid]
+  | MPdot (mp,l) -> cons_dirpath (Label.to_id l) (dirpath_of_mp mp)
+
+let dirpath_of_global = function
+  | ConstRef kn -> dirpath_of_mp (Constant.modpath kn)
+  | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
+    dirpath_of_mp (MutInd.modpath kn)
+  | VarRef _ -> DirPath.empty
+
+let qualid_of_global env r =
+  Libnames.make_qualid (dirpath_of_global r) (id_of_global env r)
+
+let safe_gen f env c =
+  let orig_extern_ref = Constrextern.get_extern_reference () in
+  let extern_ref loc vars r =
+    try orig_extern_ref loc vars r
+    with e when Errors.noncritical e ->
+      Libnames.Qualid (loc, qualid_of_global env r)
+  in
+  Constrextern.set_extern_reference extern_ref;
+  try
+    let p = f env c in
+    Constrextern.set_extern_reference orig_extern_ref;
+    p
+  with e when Errors.noncritical e ->
+    Constrextern.set_extern_reference orig_extern_ref;
+    str "??"
+
+let safe_pr_lconstr_env = safe_gen pr_lconstr_env
+let safe_pr_constr_env = safe_gen pr_constr_env
+let safe_pr_lconstr t = safe_pr_lconstr_env (Global.env()) t
+let safe_pr_constr t = safe_pr_constr_env (Global.env()) t
+
+
 (**********************************************************************)
 (* Global references *)
 
@@ -643,7 +701,6 @@ let pr_instance_gmap insts =
 
 (** Inductive declarations *)
 
-open Declarations
 open Termops
 open Reduction
 
diff --git a/printing/printer.mli b/printing/printer.mli
index 2c6800a117..2bc589b63c 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -32,6 +32,17 @@ val pr_lconstr             : constr -> std_ppcmds
 val pr_constr_env          : env -> constr -> std_ppcmds
 val pr_constr              : constr -> std_ppcmds
 
+(** Same, but resilient to [Nametab] errors. Prints fully-qualified
+    names when [shortest_qualid_of_global] has failed. Prints "??"
+    in case of remaining issues (such as reference not in env). *)
+
+val safe_pr_lconstr_env         : env -> constr -> std_ppcmds
+val safe_pr_lconstr             : constr -> std_ppcmds
+
+val safe_pr_constr_env          : env -> constr -> std_ppcmds
+val safe_pr_constr              : constr -> std_ppcmds
+
+
 val pr_open_constr_env     : env -> open_constr -> std_ppcmds
 val pr_open_constr         : open_constr -> std_ppcmds
 
diff --git a/test-suite/bugs/closed/shouldsucceed/2995.v b/test-suite/bugs/closed/shouldsucceed/2995.v
new file mode 100644
index 0000000000..ba3acd088d
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2995.v
@@ -0,0 +1,9 @@
+Module Type Interface.
+  Parameter error: nat.
+End Interface.
+
+Module Implementation <: Interface.
+  Definition t := bool.
+  Definition error: t := false.
+Fail End Implementation.
+(* A UserError here is expected, not an uncaught Not_found *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/3008.v b/test-suite/bugs/closed/shouldsucceed/3008.v
new file mode 100644
index 0000000000..3f3a979a35
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/3008.v
@@ -0,0 +1,29 @@
+Module Type Intf1.
+Parameter T : Type.
+Inductive a := A.
+End Intf1.
+
+Module Impl1 <: Intf1.
+Definition T := unit.
+Inductive a := A.
+End Impl1.
+
+Module Type Intf2
+  (Impl1 : Intf1).
+Parameter x : Impl1.A=Impl1.A -> Impl1.T.
+End Intf2.
+
+Module Type Intf3
+  (Impl1 : Intf1)
+  (Impl2 : Intf2(Impl1)).
+End Intf3.
+
+Fail Module Toto
+  (Impl1' : Intf1)
+  (Impl2 : Intf2(Impl1'))
+  (Impl3 : Intf3(Impl1)(Impl2)).
+(* A UserError is expected here, not an uncaught Not_found *)
+
+(* NB : the Inductive above and the A=A weren't in the initial test,
+   they are here only to force an access to the environment
+   (cf [Printer.qualid_of_global]) and check that this env is ok. *)
\ No newline at end of file
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 58bfe08322..a050e45c38 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -24,6 +24,9 @@ open Cases
 open Logic
 open Printer
 open Evd
+open Libnames
+open Globnames
+open Declarations
 
 let pr_lconstr c = quote (pr_lconstr c)
 let pr_lconstr_env e c = quote (pr_lconstr_env e c)
@@ -598,9 +601,11 @@ let explain_not_match_error = function
     str "types given to " ++ str (Id.to_string id) ++ str " differ"
   | NotConvertibleBodyField ->
     str "the body of definitions differs"
-  | NotConvertibleTypeField (typ1, typ2) ->
-    str "expected type" ++ spc ()  ++ pr_lconstr typ2 ++ spc () ++
-    str "but found type" ++ spc () ++ pr_lconstr typ1
+  | NotConvertibleTypeField (env, typ1, typ2) ->
+    str "expected type" ++ spc ()  ++
+    quote (Printer.safe_pr_lconstr_env env typ2) ++ spc () ++
+    str "but found type" ++ spc () ++
+    quote (Printer.safe_pr_lconstr_env env typ1)
   | NotSameConstructorNamesField ->
     str "constructor names differ"
   | NotSameInductiveNameInBlockField ->