Fix universe polymorphic Program obligations.

The universes of the obligations should all be non-algebraic as they
might appear in instances of other obligations and instances only take
non-algebraic universes as arguments.

5 files changed, 306 insertions, 0 deletions

diff --git a/engine/uState.ml b/engine/uState.ml
index dfea25dd0..01a479821 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -437,6 +437,9 @@ let make_flexible_variable ctx ~algebraic u =
   {ctx with uctx_univ_variables = uvars'; 
       uctx_univ_algebraic = avars'}
 
+let make_flexible_nonalgebraic ctx =
+  {ctx with uctx_univ_algebraic = Univ.LSet.empty}
+
 let is_sort_variable uctx s = 
   match s with 
   | Sorts.Type u -> 
diff --git a/engine/uState.mli b/engine/uState.mli
index b31e94b28..1c906fcb2 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -104,6 +104,11 @@ val add_global_univ : t -> Univ.Level.t -> t
   universe. Otherwise the variable is just made flexible. *)
 val make_flexible_variable : t -> algebraic:bool -> Univ.Level.t -> t
 
+(** Turn all undefined flexible algebraic variables into simply flexible
+   ones. Can be used in case the variables might appear in universe instances
+   (typically for polymorphic program obligations). *)
+val make_flexible_nonalgebraic : t -> t
+
 val is_sort_variable : t -> Sorts.t -> Univ.Level.t option
 
 val normalize_variables : t -> Univ.universe_subst * t
diff --git a/test-suite/bugs/closed/5215.v b/test-suite/bugs/closed/5215.v
new file mode 100644
index 000000000..ecf529159
--- /dev/null
+++ b/test-suite/bugs/closed/5215.v
@@ -0,0 +1,286 @@
+Require Import Coq.Logic.FunctionalExtensionality.
+Require Import Coq.Program.Tactics.
+
+Global Set Primitive Projections.
+
+Global Set Universe Polymorphism.
+
+Global Unset Universe Minimization ToSet.
+
+Class Category : Type :=
+{
+  Obj : Type;
+  Hom : Obj -> Obj -> Type;
+  compose : forall {a b c : Obj}, (Hom a b) -> (Hom b c) -> (Hom a c);
+  id : forall {a : Obj}, Hom a a;
+}.
+
+Arguments Obj {_}, _.
+Arguments id {_ _}, {_} _, _ _.
+Arguments Hom {_} _ _, _ _ _.
+Arguments compose {_} {_ _ _} _ _, _ {_ _ _} _ _, _ _ _ _ _ _.
+
+Coercion Obj : Category >-> Sortclass.
+
+Definition Opposite (C : Category) : Category :=
+{|
+
+  Obj := Obj C;
+  Hom := fun a b => Hom b a;
+  compose :=
+    fun a b c (f : Hom b a) (g : Hom c b) => compose C c b a g f;
+  id := fun c => id C c;
+|}.
+
+Record Functor (C C' : Category) : Type :=
+{
+  FO : C -> C';
+  FA : forall {a b}, Hom a b -> Hom (FO a) (FO b);
+}.
+
+Arguments FO {_ _} _ _.
+Arguments FA {_ _} _ {_ _} _, {_ _} _ _ _ _.
+
+Section Opposite_Functor.
+  Context {C D : Category} (F : Functor C D).
+
+  Program Definition Opposite_Functor : (Functor (Opposite C) (Opposite D)) :=
+    {|
+      FO := FO F;
+      FA := fun _ _ h => FA F h;
+    |}.
+
+End Opposite_Functor.
+
+Section Functor_Compose.
+  Context {C C' C'' : Category} (F : Functor C C') (F' : Functor C' C'').
+
+  Program Definition Functor_compose : Functor C C'' :=
+    {|
+      FO := fun c => FO F' (FO F c);
+      FA := fun c d f => FA F' (FA F f)
+    |}.
+
+End Functor_Compose.
+
+Section Algebras.
+  Context {C : Category} (T : Functor C C).
+  Record Algebra : Type :=
+    {
+      Alg_Carrier : C;
+      Constructors : Hom (FO T Alg_Carrier) Alg_Carrier
+    }.
+
+  Record Algebra_Hom (alg alg' : Algebra) : Type :=
+    {
+      Alg_map : Hom (Alg_Carrier alg) (Alg_Carrier alg');
+
+      Alg_map_com : compose (FA T Alg_map) (Constructors alg')
+                     = compose (Constructors alg) Alg_map
+    }.
+
+  Arguments Alg_map {_ _} _.
+  Arguments Alg_map_com {_ _} _.
+  Program Definition Algebra_Hom_compose
+          {alg alg' alg'' : Algebra}
+          (h : Algebra_Hom alg alg')
+          (h' : Algebra_Hom alg' alg'')
+    : Algebra_Hom alg alg''
+    :=
+      {|
+        Alg_map := compose (Alg_map h) (Alg_map h')
+      |}.
+
+  Next Obligation. Proof. Admitted.
+
+  Lemma Algebra_Hom_eq_simplify (alg alg' : Algebra)
+        (ah ah' : Algebra_Hom alg alg')
+    : (Alg_map ah) = (Alg_map ah') -> ah = ah'.
+  Proof. Admitted.
+
+  Program Definition Algebra_Hom_id (alg : Algebra) : Algebra_Hom alg alg :=
+    {|
+      Alg_map := id
+    |}.
+
+  Next Obligation. Admitted.
+
+  Definition Algebra_Cat : Category :=
+    {|
+      Obj := Algebra;
+      Hom := Algebra_Hom;
+      compose := @Algebra_Hom_compose;
+      id := Algebra_Hom_id;
+    |}.
+
+End Algebras.
+
+Arguments Alg_Carrier {_ _} _.
+Arguments Constructors {_ _} _.
+Arguments Algebra_Hom {_ _} _ _.
+Arguments Alg_map {_ _ _ _} _.
+Arguments Alg_map_com {_ _ _ _} _.
+Arguments Algebra_Hom_id {_ _} _.
+
+Section CoAlgebras.
+  Context {C : Category}.
+
+  Definition CoAlgebra (T : Functor C C) :=
+    @Algebra (Opposite C) (Opposite_Functor T).
+
+  Definition CoAlgebra_Hom {T : Functor C C} :=
+      @Algebra_Hom (Opposite C) (Opposite_Functor T).
+
+  Definition CoAlgebra_Hom_id {T : Functor C C} :=
+    @Algebra_Hom_id  (Opposite C) (Opposite_Functor T).
+
+  Definition CoAlgebra_Cat (T : Functor C C) :=
+    @Algebra_Cat (Opposite C) (Opposite_Functor T).
+
+End CoAlgebras.
+
+Program Definition Type_Cat : Category :=
+{|
+  Obj := Type;
+  Hom := (fun A B => A -> B);
+  compose := fun A B C (g : A -> B) (h : B -> C) => fun (x : A) => h (g x);
+  id := fun A => fun x => x
+|}.
+
+Local Obligation Tactic := idtac.
+
+Program Definition Prod_Cat (C C' : Category) : Category :=
+{|
+  Obj := C * C';
+  Hom :=
+    fun a b =>
+      ((Hom (fst a) (fst b)) * (Hom (snd a) (snd b)))%type;
+  compose :=
+    fun a b c f g =>
+      ((compose (fst f) (fst g)), (compose (snd f)(snd g)));
+  id := fun c => (id, id)
+|}.
+
+Class Terminal (C : Category) : Type :=
+{
+  terminal : C;
+  t_morph : forall (d : Obj), Hom d terminal;
+  t_morph_unique : forall (d : Obj) (f g : (Hom d terminal)), f = g
+}.
+
+Arguments terminal {_} _.
+Arguments t_morph {_} _ _.
+Arguments t_morph_unique {_} _ _ _ _.
+
+Coercion terminal : Terminal >-> Obj.
+
+Definition Initial (C : Category) := Terminal (Opposite C).
+Existing Class Initial.
+
+Record Product {C : Category} (c d : C) : Type :=
+{
+  product : C;
+  Pi_1 : Hom product c;
+  Pi_2 : Hom product d;
+  Prod_morph_ex : forall (p' : Obj) (r1 : Hom p' c) (r2 : Hom p' d), (Hom p' product);
+}.
+
+Arguments Product _ _ _, {_} _ _.
+
+Arguments Pi_1 {_ _ _ _}, {_ _ _} _.
+Arguments Pi_2 {_ _ _ _}, {_ _ _} _.
+Arguments Prod_morph_ex {_ _ _} _ _ _ _.
+
+Coercion product : Product >-> Obj.
+
+Definition Has_Products (C : Category) : Type := forall a b, Product a b.
+
+Existing Class Has_Products.
+
+Program Definition Prod_Func (C : Category) {HP : Has_Products C}
+  : Functor (Prod_Cat C C) C :=
+{|
+  FO := fun x => HP (fst x) (snd x);
+  FA := fun a b f => Prod_morph_ex _ _ (compose Pi_1 (fst f)) (compose  Pi_2 (snd f))
+|}.
+
+Arguments Prod_Func _ _, _ {_}.
+
+Definition Sum (C : Category) := @Product (Opposite C).
+
+Arguments Sum _ _ _, {_} _ _.
+
+Definition Has_Sums (C : Category) : Type :=  forall (a b : C), (Sum a b).
+
+Existing Class Has_Sums.
+
+Program Definition sum_Sum (A B : Type) : (@Sum Type_Cat A B) :=
+{|
+  product := (A + B)%type;
+  Prod_morph_ex :=
+    fun (p' : Type)
+        (r1 : A -> p')
+        (r2 : B -> p')
+        (X : A + B) =>
+      match X return p' with
+      | inl a => r1 a
+      | inr b => r2 b
+      end
+|}.
+Next Obligation. simpl; auto. Defined.
+Next Obligation. simpl; auto. Defined.
+
+Program Instance Type_Cat_Has_Sums : Has_Sums Type_Cat := sum_Sum.
+
+Definition Sum_Func {C : Category} {HS : Has_Sums C} :
+  Functor (Prod_Cat C C) C := Opposite_Functor (Prod_Func (Opposite C) HS).
+
+Arguments Sum_Func _ _, _ {_}.
+
+Program Instance unit_Type_term : Terminal Type_Cat :=
+{
+  terminal := unit;
+  t_morph := fun _ _=> tt
+}.
+
+Next Obligation. Proof. Admitted.
+
+Program Definition term_id : Functor Type_Cat (Prod_Cat Type_Cat Type_Cat) :=
+{|
+  FO := fun a => (@terminal Type_Cat _, a);
+  FA := fun a b f => (@id _ (@terminal Type_Cat _), f)
+|}.
+
+Definition S_nat_func : Functor Type_Cat Type_Cat :=
+  Functor_compose term_id (Sum_Func Type_Cat _).
+
+Definition S_nat_alg_cat := Algebra_Cat S_nat_func.
+
+CoInductive CoNat : Set :=
+  | CoO : CoNat
+  | CoS : CoNat -> CoNat
+.
+
+Definition S_nat_coalg_cat := @CoAlgebra_Cat Type_Cat S_nat_func.
+
+Set Printing Universes.
+Program Definition CoNat_alg_term : Initial S_nat_coalg_cat :=
+{|
+  terminal := _;
+  t_morph := _
+|}.
+
+Next Obligation. Admitted.
+Next Obligation. Admitted.
+
+Axiom Admit : False.
+
+Next Obligation.
+Proof.
+  intros d f g.
+  assert(H1 := (@Alg_map_com _ _ _ _ f)). clear.
+  assert (inl tt = inr tt) by (exfalso; apply Admit).
+  discriminate.
+  all: exfalso; apply Admit.
+  Show Universes.
+Qed.
diff --git a/test-suite/bugs/closed/5215_2.v b/test-suite/bugs/closed/5215_2.v
new file mode 100644
index 000000000..399947f00
--- /dev/null
+++ b/test-suite/bugs/closed/5215_2.v
@@ -0,0 +1,8 @@
+Require Import Coq.Program.Tactics.
+Set Universe Polymorphism.
+Set Printing Universes.
+Definition typ := Type.
+
+Program Definition foo : typ := _ -> _.
+Next Obligation. Admitted.
+Next Obligation. exact typ. Show Proof. Show Universes. Defined.
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index ed4d8b888..a44de66e9 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -678,6 +678,7 @@ let init_prog_info ?(opaque = false) sign n udecl b t ctx deps fixkind
 	      obl_deps = d; obl_tac = tac })
 	  obls, b
   in
+  let ctx = UState.make_flexible_nonalgebraic ctx in
     { prg_name = n ; prg_body = b; prg_type = reduce t; 
       prg_ctx = ctx; prg_univdecl = udecl;
       prg_obligations = (obls', Array.length obls');
@@ -841,6 +842,9 @@ let obligation_terminator name num guard hook auto pf =
       Inductiveops.control_only_guard (Global.env ()) body;
       (** Declare the obligation ourselves and drop the hook *)
       let prg = get_info (ProgMap.find name !from_prg) in
+      (** Ensure universes are substituted properly in body and type *)
+      let body = EConstr.to_constr sigma (EConstr.of_constr body) in
+      let ty = Option.map (fun x -> EConstr.to_constr sigma (EConstr.of_constr x)) ty in
       let ctx = Evd.evar_universe_context sigma in
       let prg = { prg with prg_ctx = ctx } in
       let obls, rem = prg.prg_obligations in