Hints/Univs: fix bug #4628 anomalies

Fix handling of non-polymorphic hints built from polymorphic values, or
simply producing new universes. We have to record the side effects of
global hints built from constrs which are not polymorphic when they
declare global universes, which might need to be discharged at the end
of sections too. Also issue a warning when a Hint is declared for a
polymorphic reference but the Hint isn't polymorphic itself (this used
to produce an anomaly). For [using] hints, treat all lemmas as
polymorphic, refreshing their universes at each use, as is done for
their existentials (also used to produce an anomaly).

2 files changed, 94 insertions, 15 deletions

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 42e5067c9d..1da464e6f4 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -726,10 +726,43 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
    c is a constr
    cty is the type of constr *)
 
+let pr_hint_term env sigma ctx = function
+  | IsGlobRef gr -> pr_global gr
+  | IsConstr (c, ctx) ->
+     let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
+     pr_constr_env env sigma c
+
+(** We need an object to record the side-effect of registering
+  global universes associated with a hint. *)
+let cache_context_set (_,c) =
+  Global.push_context_set false c
+
+let input_context_set : Univ.ContextSet.t -> Libobject.obj =
+  let open Libobject in
+    declare_object
+    { (default_object "Global universe context") with
+      cache_function = cache_context_set;
+      load_function = (fun _ -> cache_context_set);
+      discharge_function = (fun (_,a) -> Some a);
+      classify_function = (fun a -> Keep a) }
+
 let fresh_global_or_constr env sigma poly cr =
-  match cr with
-  | IsGlobRef gr -> Universes.fresh_global_instance env gr
-  | IsConstr (c, ctx) -> (c, ctx)
+  let isgr, (c, ctx) =
+    match cr with
+    | IsGlobRef gr ->
+       true, Universes.fresh_global_instance env gr
+    | IsConstr (c, ctx) -> false, (c, ctx)
+  in
+    if poly then (c, ctx)
+    else if Univ.ContextSet.is_empty ctx then (c, ctx)
+    else begin
+      if isgr then
+        msg_warning (str"Using polymorphic hint " ++
+		     pr_hint_term env sigma ctx cr ++ str" monomorphically" ++
+		     str" use Polymorphic Hint to use it polymorphically.");
+      Lib.add_anonymous_leaf (input_context_set ctx);
+      (c, Univ.ContextSet.empty)
+    end
 
 let make_resolves env sigma flags pri poly ?name cr =
   let c, ctx = fresh_global_or_constr env sigma poly cr in
@@ -1094,7 +1127,7 @@ let prepare_hint check (poly,local) env init (sigma,c) =
     let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in
     if poly then IsConstr (c', diff)
     else if local then IsConstr (c', diff)
-    else (Global.push_context_set false diff;
+    else (Lib.add_anonymous_leaf (input_context_set diff);
 	  IsConstr (c', Univ.ContextSet.empty))
 
 let interp_hints poly =
@@ -1169,18 +1202,24 @@ let expand_constructor_hints env sigma lems =
     match kind_of_term lem with
     | Ind (ind,u) ->
 	List.init (nconstructors ind) 
-	  (fun i -> IsConstr (mkConstructU ((ind,i+1),u), 
-			      Univ.ContextSet.empty))
+		  (fun i ->
+		   let ctx = Univ.ContextSet.diff (Evd.universe_context_set evd)
+						  (Evd.universe_context_set sigma) in
+		   not (Univ.ContextSet.is_empty ctx),
+		   IsConstr (mkConstructU ((ind,i+1),u),ctx))
     | _ ->
-	[prepare_hint false (false,true) env sigma (evd,lem)]) lems
-
+       [match prepare_hint false (false,true) env sigma (evd,lem) with
+	| IsConstr (c, ctx) ->
+	   not (Univ.ContextSet.is_empty ctx), IsConstr (c, ctx)
+	| IsGlobRef _ -> assert false (* Impossible return value *) ]) lems
 (* builds a hint database from a constr signature *)
 (* typically used with (lid, ltyp) = pf_hyps_types <some goal> *)
 
 let add_hint_lemmas env sigma eapply lems hint_db =
   let lems = expand_constructor_hints env sigma lems in
   let hintlist' =
-    List.map_append (make_resolves env sigma (eapply,true,false) None false) lems in
+    List.map_append (fun (poly, lem) ->
+		     make_resolves env sigma (eapply,true,false) None poly lem) lems in
   Hint_db.add_list env sigma hintlist' hint_db
 
 let make_local_hint_db env sigma ts eapply lems =
@@ -1193,12 +1232,6 @@ let make_local_hint_db env sigma ts eapply lems =
   add_hint_lemmas env sigma eapply lems
     (Hint_db.add_list env sigma hintlist (Hint_db.empty ts false))
 
-let make_local_hint_db = 
-  if Flags.profile then
-    let key = Profile.declare_profile "make_local_hint_db" in
-      Profile.profile4 key make_local_hint_db
-  else make_local_hint_db
-
 let make_local_hint_db env sigma ?ts eapply lems =
   make_local_hint_db env sigma ts eapply lems
 
diff --git a/test-suite/bugs/closed/4628.v b/test-suite/bugs/closed/4628.v
new file mode 100644
index 0000000000..7d4a15d689
--- /dev/null
+++ b/test-suite/bugs/closed/4628.v
@@ -0,0 +1,46 @@
+Module first.
+  Polymorphic Record BAR (A:Type) :=
+  { foo: A->Prop; bar: forall (x y: A), foo x -> foo y}.
+
+Section A.
+Context {A:Type}.
+
+Set Printing Universes.
+
+Hint Resolve bar.
+Goal forall (P:BAR A) x y, foo _ P x -> foo _ P y.
+intros.
+eauto.
+Qed.
+End A.
+End first.
+
+Module firstbest.
+  Polymorphic Record BAR (A:Type) :=
+  { foo: A->Prop; bar: forall (x y: A), foo x -> foo y}.
+
+Section A.
+Context {A:Type}.
+
+Set Printing Universes.
+
+Polymorphic Hint Resolve bar.
+Goal forall (P:BAR A) x y, foo _ P x -> foo _ P y.
+intros.
+eauto.
+Qed.
+End A.
+End firstbest.
+
+Module second.
+Axiom foo: Set.
+Axiom foo': Set.
+
+Polymorphic Record BAR (A:Type) :=
+  { bar: foo' -> foo}.
+Set Printing Universes.
+
+Lemma baz@{i}: forall (P:BAR@{Set} nat), foo' -> foo.
+  eauto using bar.
+Qed.
+End second.