Merge remote-tracking branch 'github/pr/366' into v8.6

Was PR#366: Univs: fix bug 5208

10 files changed, 356 insertions, 68 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index aa91fc5222..a6b6f742b7 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -854,6 +854,13 @@ let is_eq_sort s1 s2 =
       if Univ.Universe.equal u1 u2 then None
       else Some (u1, u2)
 
+(* Precondition: l is not defined in the substitution *)
+let universe_rigidity evd l =
+  let uctx = evd.universes in
+  if Univ.LSet.mem l (Univ.ContextSet.levels (UState.context_set uctx)) then
+    UnivFlexible (Univ.LSet.mem l (UState.algebraics uctx))
+  else UnivRigid
+
 let normalize_universe evd =
   let vars = ref (UState.subst evd.universes) in
   let normalize = Universes.normalize_universe_opt_subst vars in
diff --git a/engine/evd.mli b/engine/evd.mli
index b47b389d1b..86887f3dcc 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -467,7 +467,17 @@ val retract_coercible_metas : evar_map -> metabinding list * evar_map
 (*********************************************************
    Sort/universe variables *)
 
-(** Rigid or flexible universe variables *)
+(** Rigid or flexible universe variables.
+
+   [UnivRigid] variables are user-provided or come from an explicit
+   [Type] in the source, we do not minimize them or unify them eagerly.
+
+   [UnivFlexible alg] variables are fresh universe variables of
+   polymorphic constants or generated during refinement, sometimes in
+   algebraic position (i.e. not appearing in the term at the moment of
+   creation). They are the candidates for minimization (if alg, to an
+   algebraic universe) and unified eagerly in the first-order
+   unification heurstic.  *)
 
 type rigid = UState.rigid =
   | UnivRigid
@@ -514,7 +524,8 @@ val new_univ_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_
 val new_sort_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * sorts
 
 val add_global_univ : evar_map -> Univ.Level.t -> evar_map
-											   
+
+val universe_rigidity : evar_map -> Univ.Level.t -> rigid
 val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map
 val is_sort_variable : evar_map -> sorts -> Univ.universe_level option 
 (** [is_sort_variable evm s] returns [Some u] or [None] if [s] is 
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index e2712615be..4884d0deb1 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -638,19 +638,6 @@ let check_smaller g strict u v =
 
 type 'a check_function = universes -> 'a -> 'a -> bool
 
-let check_equal_expr g x y =
-  x == y || (let (u, n) = x and (v, m) = y in 
-               Int.equal n m && check_equal g u v)
-
-let check_eq_univs g l1 l2 =
-  let f x1 x2 = check_equal_expr g x1 x2 in
-  let exists x1 l = Universe.exists (fun x2 -> f x1 x2) l in
-    Universe.for_all (fun x1 -> exists x1 l2) l1
-    && Universe.for_all (fun x2 -> exists x2 l1) l2
-
-let check_eq g u v =
-  Universe.equal u v || check_eq_univs g u v
-
 let check_smaller_expr g (u,n) (v,m) =
   let diff = n - m in
     match diff with
@@ -669,7 +656,13 @@ let real_check_leq g u v =
 let check_leq g u v =
   Universe.equal u v ||
     is_type0m_univ u ||
-    check_eq_univs g u v || real_check_leq g u v
+    real_check_leq g u v
+
+let check_eq_univs g l1 l2 =
+  real_check_leq g l1 l2 && real_check_leq g l2 l1
+
+let check_eq g u v =
+  Universe.equal u v || check_eq_univs g u v
 
 (* enforce_univ_eq g u v will force u=v if possible, will fail otherwise *)
 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 9224ec48d7..09f884ecd0 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -468,15 +468,32 @@ struct
       else if Level.is_prop u then
 	hcons (Level.set,n+k)
       else hcons (u,n+k)
-	
+
+    type super_result =
+	SuperSame of bool
+        (* The level expressions are in cumulativity relation. boolean
+           indicates if left is smaller than right?  *)
+      | SuperDiff of int
+        (* The level expressions are unrelated, the comparison result
+           is canonical *)
+
+    (** [super u v] compares two level expressions,
+       returning [SuperSame] if they refer to the same level at potentially different
+       increments or [SuperDiff] if they are different. The booleans indicate if the
+       left expression is "smaller" than the right one in both cases. *)
     let super (u,n as x) (v,n' as y) =
       let cmp = Level.compare u v in
-	if Int.equal cmp 0 then 
-	  if n < n' then Inl true
-	  else Inl false
-	else if is_prop x then Inl true
-	else if is_prop y then Inl false
-	else Inr cmp
+	if Int.equal cmp 0 then SuperSame (n < n')
+	else
+	  match x, y with
+	  | (l,0), (l',0) ->
+	     let open RawLevel in
+	     (match Level.data l, Level.data l' with
+	      | Prop, Prop -> SuperSame false
+	      | Prop, _ -> SuperSame true
+	      | _, Prop -> SuperSame false
+	      | _, _ -> SuperDiff cmp)
+	  | _, _ -> SuperDiff cmp
 
     let to_string (v, n) =
       if Int.equal n 0 then Level.to_string v
@@ -598,24 +615,26 @@ struct
     | Nil, _ -> l2
     | _, Nil -> l1
     | Cons (h1, _, t1), Cons (h2, _, t2) ->
-      (match Expr.super h1 h2 with
-      | Inl true (* h1 < h2 *) -> merge_univs t1 l2
-      | Inl false -> merge_univs l1 t2
-      | Inr c -> 
-        if c <= 0 (* h1 < h2 is name order *)
-	then cons h1 (merge_univs t1 l2)
-	else cons h2 (merge_univs l1 t2))
+       let open Expr in
+       (match super h1 h2 with
+	| SuperSame true (* h1 < h2 *) -> merge_univs t1 l2
+	| SuperSame false -> merge_univs l1 t2
+	| SuperDiff c ->
+           if c <= 0 (* h1 < h2 is name order *)
+	   then cons h1 (merge_univs t1 l2)
+	   else cons h2 (merge_univs l1 t2))
 
   let sort u =
     let rec aux a l = 
       match l with
       | Cons (b, _, l') ->
-        (match Expr.super a b with
-	| Inl false -> aux a l'
-	| Inl true -> l
-	| Inr c ->
-	  if c <= 0 then cons a l
-	  else cons b (aux a l'))
+	let open Expr in
+        (match super a b with
+	 | SuperSame false -> aux a l'
+	 | SuperSame true -> l
+	 | SuperDiff c ->
+	    if c <= 0 then cons a l
+	    else cons b (aux a l'))
       | Nil -> cons a l
     in 
       fold (fun a acc -> aux a acc) u nil
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index aa24733d9f..6e4d72705b 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1934,14 +1934,22 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
  *)
 
 let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
+  let refresh_tycon sigma t =
+    (** If we put the typing constraint in the term, it has to be
+       refreshed to preserve the invariant that no algebraic universe
+       can appear in the term.  *)
+    refresh_universes ~status:Evd.univ_flexible ~onlyalg:true (Some true)
+		      env sigma t
+  in
   let preds =
     match pred, tycon with
     (* No return clause *)
     | None, Some t when not (noccur_with_meta 0 max_int t) ->
 	(* If the tycon is not closed w.r.t real variables, we try *)
         (* two different strategies *)
-	(* First strategy: we abstract the tycon wrt to the dependencies *)
-        let p1 =
+       (* First strategy: we abstract the tycon wrt to the dependencies *)
+         let sigma, t = refresh_tycon sigma t in
+         let p1 =
           prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in
 	(* Second strategy: we build an "inversion" predicate *)
 	let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in
@@ -1952,7 +1960,7 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
 	(* No dependent type constraint, or no constraints at all: *)
 	(* we use two strategies *)
         let sigma,t = match tycon with
-	| Some t -> sigma,t
+	| Some t -> refresh_tycon sigma t
 	| None -> 
           let sigma = Sigma.Unsafe.of_evar_map sigma in
           let Sigma ((t, _), sigma, _) =
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index ba566f3744..ee4148de64 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -114,10 +114,11 @@ val compile : 'a pattern_matching_problem -> Environ.unsafe_judgment
 
 val prepare_predicate :            Loc.t ->
            (Evarutil.type_constraint ->
-            Environ.env -> Evd.evar_map ref -> 'a -> Environ.unsafe_judgment) ->
+            Environ.env -> Evd.evar_map ref -> glob_constr -> Environ.unsafe_judgment) ->
            Environ.env ->
            Evd.evar_map ->
            (Term.types * tomatch_type) list ->
            Context.Rel.t list ->
            Constr.constr option ->
-           'a option -> (Evd.evar_map * Names.name list * Term.constr) list
+           glob_constr option ->
+           (Evd.evar_map * Names.name list * Term.constr) list
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index f0aa9b564f..4fd030845d 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -42,33 +42,39 @@ let get_polymorphic_positions f =
         templ.template_param_levels)
   | _ -> assert false
 
-let refresh_level evd s =
-  match Evd.is_sort_variable evd s with
-  | None -> true
-  | Some l -> not (Evd.is_flexible_level evd l)
-
 let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
 		      pbty env evd t =
   let evdref = ref evd in
   let modified = ref false in
-  let rec refresh status dir t = 
-    match kind_of_term t with
-    | Sort (Type u as s) when
-      (match Univ.universe_level u with
-      | None -> true
-      | Some l -> not onlyalg && refresh_level evd s) ->
+  (* direction: true for fresh universes lower than the existing ones *)
+  let refresh_sort status ~direction s =
     let s' = evd_comb0 (new_sort_variable status) evdref in
     let evd = 
-      if dir then set_leq_sort env !evdref s' s
+      if direction then set_leq_sort env !evdref s' s
       else set_leq_sort env !evdref s s'
     in
-      modified := true; evdref := evd; mkSort s'
-    | Sort (Prop Pos as s) when refreshset && not dir ->
-       let s' = evd_comb0 (new_sort_variable status) evdref in
-       let evd = set_leq_sort env !evdref s s' in
-       modified := true; evdref := evd; mkSort s'
+    modified := true; evdref := evd; mkSort s'
+  in
+  let rec refresh ~onlyalg status ~direction t =
+    match kind_of_term t with
+    | Sort (Type u as s) ->
+       (match Univ.universe_level u with
+	| None -> refresh_sort status ~direction s
+	| Some l ->
+	   (match Evd.universe_rigidity evd l with
+	    | UnivRigid ->
+	       if not onlyalg then refresh_sort status ~direction s
+	       else t
+	    | UnivFlexible alg ->
+	       if onlyalg && alg then
+	         (evdref := Evd.make_flexible_variable !evdref false l; t)
+	       else t))
+    | Sort (Prop Pos as s) when refreshset && not direction ->
+       (* Cannot make a universe "lower" than "Set",
+          only refreshing when we want higher universes. *)
+       refresh_sort status ~direction s
     | Prod (na,u,v) -> 
-      mkProd (na,u,refresh status dir v)
+      mkProd (na, u, refresh ~onlyalg status ~direction v)
     | _ -> t
   (** Refresh the types of evars under template polymorphic references *)
   and refresh_term_evars onevars top t =
@@ -81,7 +87,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
       Array.iter (refresh_term_evars onevars false) args
     | Evar (ev, a) when onevars ->
       let evi = Evd.find !evdref ev in
-      let ty' = refresh univ_flexible true evi.evar_concl in
+      let ty' = refresh ~onlyalg univ_flexible ~direction:true evi.evar_concl in
 	if !modified then 
 	  evdref := Evd.add !evdref ev {evi with evar_concl = ty'}
 	else ()
@@ -101,9 +107,11 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
   in
   let t' = 
     if isArity t then
-      (match pbty with
-      | None -> t
-      | Some dir -> refresh status dir t)
+      match pbty with
+      | None ->
+	 (* No cumulativity needed, but we still need to refresh the algebraics *)
+	 refresh ~onlyalg:true univ_flexible ~direction:false t
+      | Some direction -> refresh ~onlyalg status ~direction t
     else (refresh_term_evars false true t; t)
   in
     if !modified then !evdref, t' else !evdref, t
diff --git a/test-suite/bugs/closed/5208.v b/test-suite/bugs/closed/5208.v
new file mode 100644
index 0000000000..b7a684a27c
--- /dev/null
+++ b/test-suite/bugs/closed/5208.v
@@ -0,0 +1,222 @@
+Require Import Program.
+
+Require Import Coq.Strings.String.
+Require Import Coq.Strings.Ascii.
+Require Import Coq.Numbers.BinNums.
+
+Set Implicit Arguments.
+Set Strict Implicit.
+Set Universe Polymorphism.
+Set Printing Universes.
+
+Local Open Scope positive.
+
+Definition field : Type := positive.
+
+Section poly.
+  Universe U.
+
+  Inductive fields : Type :=
+  | pm_Leaf : fields
+  | pm_Branch : fields -> option Type@{U} -> fields -> fields.
+
+  Definition fields_left (f : fields) : fields :=
+    match f with
+    | pm_Leaf => pm_Leaf
+    | pm_Branch l _ _ => l
+    end.
+
+  Definition fields_right (f : fields) : fields :=
+    match f with
+    | pm_Leaf => pm_Leaf
+    | pm_Branch _ _ r => r
+    end.
+
+  Definition fields_here (f : fields) : option Type@{U} :=
+    match f with
+    | pm_Leaf => None
+    | pm_Branch _ s _ => s
+    end.
+
+  Fixpoint fields_get (p : field) (m : fields) {struct p} : option Type@{U} :=
+    match p with
+      | xH => match m with
+                | pm_Leaf => None
+                | pm_Branch _ x _ => x
+              end
+      | xO p' => fields_get p' match m with
+                               | pm_Leaf => pm_Leaf
+                               | pm_Branch L _ _ => L
+                             end
+      | xI p' => fields_get p' match m with
+                               | pm_Leaf => pm_Leaf
+                               | pm_Branch _ _ R => R
+                             end
+    end.
+
+  Definition fields_leaf : fields := pm_Leaf.
+
+  Inductive member (val : Type@{U}) : fields -> Type :=
+  | pmm_H : forall L R, member val (pm_Branch L (Some val) R)
+  | pmm_L : forall (V : option Type@{U}) L R, member val L -> member val (pm_Branch L V R)
+  | pmm_R : forall (V : option Type@{U}) L R, member val R -> member val (pm_Branch L V R).
+  Arguments pmm_H {_ _ _}.
+  Arguments pmm_L {_ _ _ _} _.
+  Arguments pmm_R {_ _ _ _} _.
+
+  Fixpoint get_member (val : Type@{U}) p {struct p}
+  : forall m, fields_get p m = @Some Type@{U} val -> member val m :=
+    match p as p return forall m, fields_get p m = @Some Type@{U} val -> member@{U} val m with
+      | xH => fun m =>
+        match m as m return fields_get xH m = @Some Type@{U} val -> member@{U} val m with
+        | pm_Leaf => fun pf : None = @Some Type@{U} _ =>
+                       match pf in _ = Z return match Z with
+                                                | Some _ => _
+                                                | None => unit
+                                                end
+                       with
+                       | eq_refl => tt
+                       end
+        | pm_Branch _ None _ => fun pf : None = @Some Type@{U} _ =>
+                                  match pf in _ = Z return match Z with
+                                                           | Some _ => _
+                                                           | None => unit
+                                                           end
+                                  with
+                                  | eq_refl => tt
+                                  end
+        | pm_Branch _ (Some x) _ => fun pf : @Some Type@{U} x = @Some Type@{U} val =>
+                                      match eq_sym pf in _ = Z return member@{U} val (pm_Branch _ Z _) with
+                                      | eq_refl => pmm_H
+                                      end
+        end
+      | xO p' => fun m =>
+        match m as m return fields_get (xO p') m = @Some Type@{U} val -> member@{U} val m with
+        | pm_Leaf => fun pf : fields_get p' pm_Leaf = @Some Type@{U} val =>
+                       @get_member _ p' pm_Leaf pf
+        | pm_Branch l _ _ => fun pf : fields_get p' l = @Some Type@{U} val =>
+                       @pmm_L _ _ _ _ (@get_member _ p' l pf)
+        end
+      | xI p' => fun m =>
+        match m as m return fields_get (xI p') m = @Some Type@{U} val -> member@{U} val m with
+        | pm_Leaf => fun pf : fields_get p' pm_Leaf = @Some Type@{U} val =>
+                       @get_member _ p' pm_Leaf pf
+        | pm_Branch l _ r => fun pf : fields_get p' r = @Some Type@{U} val =>
+                               @pmm_R _ _ _ _ (@get_member _ p' r pf)
+        end
+    end.
+
+  Inductive record : fields -> Type :=
+  | pr_Leaf : record pm_Leaf
+  | pr_Branch : forall L R (V : option Type@{U}),
+      record L ->
+      match V return Type@{U} with
+        | None => unit
+        | Some t => t
+      end ->
+      record R ->
+      record (pm_Branch L V R).
+
+
+  Definition record_left {L} {V : option Type@{U}} {R}
+             (r : record (pm_Branch L V R)) : record L :=
+    match r in record z
+          return match z with
+                 | pm_Branch L _ _ => record L
+                 | _ => unit
+                 end
+    with
+      | pr_Branch _ l _ _ => l
+      | pr_Leaf => tt
+    end.
+Set Printing All.
+  Definition record_at {L} {V : option Type@{U}} {R} (r : record (pm_Branch L V R))
+  : match V return Type@{U} with
+    | None => unit
+    | Some t => t
+    end :=
+    match r in record z
+          return match z (* return ?X *) with
+                 | pm_Branch _ V _ => match V return Type@{U} with
+                                     | None => unit
+                                     | Some t => t
+                                     end
+                 | _ => unit
+                 end
+    with
+      | pr_Branch _ _ v _ => v
+      | pr_Leaf => tt
+    end.
+
+  Definition record_here {L : fields} (v : Type@{U}) {R : fields}
+             (r : record (pm_Branch L (@Some Type@{U} v) R)) : v :=
+    match r in record z
+          return match z return Type@{U} with
+                 | pm_Branch _ (Some v) _ => v
+                 | _ => unit
+                 end
+    with
+      | pr_Branch _ _ v _ => v
+      | pr_Leaf => tt
+    end.
+
+  Definition record_right {L V R} (r : record (pm_Branch L V R)) : record R :=
+    match r in record z return match z with
+                                  | pm_Branch _ _ R => record R
+                                  | _ => unit
+                                end
+    with
+      | pr_Branch _ _ _ r => r
+      | pr_Leaf => tt
+    end.
+
+  Fixpoint record_get {val : Type@{U}} {pm : fields} (m : member val pm) : record pm -> val :=
+    match m in member _ pm return record pm -> val with
+      | pmm_H => fun r => record_here r
+      | pmm_L m' => fun r => record_get m' (record_left r)
+      | pmm_R m' => fun r => record_get m' (record_right r)
+    end.
+
+  Fixpoint record_set {val : Type@{U}} {pm : fields} (m : member val pm) (x : val) {struct m}
+  : record pm -> record pm :=
+    match m in member _ pm return record pm -> record pm with
+    | pmm_H => fun r =>
+      pr_Branch (Some _)
+                (record_left r)
+                x
+                (record_right r)
+    | pmm_L m' => fun r =>
+      pr_Branch _
+                (record_set m' x (record_left r))
+                (record_at r)
+                (record_right r)
+    | pmm_R m' => fun r =>
+      pr_Branch _ (record_left r)
+                (record_at r)
+                (record_set m' x (record_right r))
+    end.
+End poly.
+Axiom cheat : forall {A}, A.
+Lemma record_get_record_set_different:
+  forall (T: Type) (vars: fields)
+    (pmr pmw: member T vars)
+    (diff: pmr <> pmw)
+    (r: record vars) (val: T),
+    record_get pmr (record_set pmw val r) = record_get pmr r.
+Proof.
+  intros.
+  revert pmr diff r val.
+  induction pmw; simpl; intros.
+  - dependent destruction pmr.
+    + congruence.
+    + auto.
+    + auto.
+  - dependent destruction pmr.
+    + auto.
+    + simpl. apply IHpmw. congruence.
+    + auto.
+  - dependent destruction pmr.
+    + auto.
+    + auto.
+    + simpl. apply IHpmw. congruence.
+Qed.
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index 9661b3bfac..f746def5cb 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -162,3 +162,24 @@ Inductive L (A:Type) (T:=A) : Type := C : L nat -> L A.
    hit the Inductiveops.get_arity bug mentioned above (see #3491) *)
 
 Inductive IND6 (A:Type) (T:=A) := CONS6 : IND6 T -> IND6 A.
+
+
+Module TemplateProp.
+
+  (** Check lowering of a template universe polymorphic inductive to Prop *)
+  
+  Inductive Foo (A : Type) : Type := foo : A -> Foo A.
+  
+  Check Foo True : Prop.
+
+End TemplateProp.
+
+Module PolyNoLowerProp.
+
+  (** Check lowering of a general universe polymorphic inductive to Prop is _failing_ *)
+  
+  Polymorphic Inductive Foo (A : Type) : Type := foo : A -> Foo A.
+  
+  Fail Check Foo True : Prop.
+
+End PolyNoLowerProp.
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 8b527ebd6f..a9f2598e22 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -540,11 +540,9 @@ let inductive_levels env evdref poly arities inds =
 	in
 	let duu = Sorts.univ_of_sort du in
 	let evd =
-	  if not (Univ.is_small_univ duu) && Evd.check_eq evd cu duu then
-	    if is_flexible_sort evd duu then
-	      if Evd.check_leq evd Univ.type0_univ duu then
-	      	evd
-	      else Evd.set_eq_sort env evd (Prop Null) du
+	  if not (Univ.is_small_univ duu) && Univ.Universe.equal cu duu then
+	    if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu) then
+	      Evd.set_eq_sort env evd (Prop Null) du
 	    else evd
 	  else Evd.set_eq_sort env evd (Type cu) du
 	in