Merge branch 'forhott' into v8.5

6 files changed, 60 insertions, 36 deletions

diff --git a/CHANGES b/CHANGES
index dada2ed975..2533b01897 100644
--- a/CHANGES
+++ b/CHANGES
@@ -9,6 +9,13 @@ Bugfixes
 - #4777: printing inefficiency with implicit arguments
 - #4752: CoqIDE crash on files not ended by ".v".
 - #4398: type_scope used consistently in "match goal".
+- #4097: more efficient occur-check in presence of primitive projections
+
+Universes:
+- Disallow silently dropping universe instances applied to variables
+  (forward compatible)
+- Allow explicit universe instances on notations, when they can apply
+  to the head reference of their expansion.
 
 Changes from V8.5 to V8.5pl1
 ============================
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ead68bd92f..f30d3cefad 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -656,7 +656,13 @@ let string_of_ty = function
   | Method -> "meth"
   | Variable -> "var"
 
-let intern_var genv (ltacvars,ntnvars) namedctx loc id =
+let gvar (loc, id) us = match us with
+| None -> GVar (loc, id)
+| Some _ ->
+  user_err_loc (loc, "", str "Variable " ++ pr_id id ++
+    str " cannot have a universe instance")
+
+let intern_var genv (ltacvars,ntnvars) namedctx loc id us =
   (* Is [id] an inductive type potentially with implicit *)
   try
     let ty,expl_impls,impls,argsc = Id.Map.find id genv.impls in
@@ -664,21 +670,21 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
       (fun id -> CRef (Ident (loc,id),None), Some (loc,ExplByName id)) expl_impls in
     let tys = string_of_ty ty in
     Dumpglob.dump_reference loc "<>" (Id.to_string id) tys;
-    GVar (loc,id), make_implicits_list impls, argsc, expl_impls
+    gvar (loc,id) us, make_implicits_list impls, argsc, expl_impls
   with Not_found ->
   (* Is [id] bound in current term or is an ltac var bound to constr *)
   if Id.Set.mem id genv.ids || Id.Set.mem id ltacvars.ltac_vars
   then
-    GVar (loc,id), [], [], []
+    gvar (loc,id) us, [], [], []
   (* Is [id] a notation variable *)
   else if Id.Map.mem id ntnvars
   then
-    (set_var_scope loc id true genv ntnvars; GVar (loc,id), [], [], [])
+    (set_var_scope loc id true genv ntnvars; gvar (loc,id) us, [], [], [])
   (* Is [id] the special variable for recursive notations *)
   else if Id.equal id ldots_var
   then if Id.Map.is_empty ntnvars
     then error_ldots_var loc
-    else GVar (loc,id), [], [], []
+    else gvar (loc,id) us, [], [], []
   else if Id.Set.mem id ltacvars.ltac_bound then
     (* Is [id] bound to a free name in ltac (this is an ltac error message) *)
     user_err_loc (loc,"intern_var",
@@ -693,10 +699,10 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
 	let impls = implicits_of_global ref in
 	let scopes = find_arguments_scope ref in
 	Dumpglob.dump_reference loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var";
-	GRef (loc, ref, None), impls, scopes, []
+	GRef (loc, ref, us), impls, scopes, []
       with e when Errors.noncritical e ->
 	(* [id] a goal variable *)
-	GVar (loc,id), [], [], []
+	gvar (loc,id) us, [], [], []
 
 let proj_impls r impls =
   let env = Global.env () in
@@ -771,9 +777,12 @@ let intern_qualid loc qid intern env lvar us args =
       let c = match us, c with
       | None, _ -> c
       | Some _, GRef (loc, ref, None) -> GRef (loc, ref, us)
+      | Some _, GApp (loc, GRef (loc', ref, None), arg) ->
+         GApp (loc, GRef (loc', ref, us), arg)
       | Some _, _ ->
         user_err_loc (loc, "", str "Notation " ++ pr_qualid qid ++
-          str " cannot have a universe instance")
+          str " cannot have a universe instance, its expanded head
+               does not start with a reference")
       in
       c, projapp, args2
 
@@ -792,7 +801,7 @@ let intern_applied_reference intern env namedctx lvar us args = function
       let x, imp, scopes, l = find_appl_head_data r in
 	(x,imp,scopes,l), args2
   | Ident (loc, id) ->
-      try intern_var env lvar namedctx loc id, args
+      try intern_var env lvar namedctx loc id us, args
       with Not_found ->
       let qid = qualid_of_ident id in
       try
@@ -802,7 +811,7 @@ let intern_applied_reference intern env namedctx lvar us args = function
       with Not_found ->
 	(* Extra allowance for non globalizing functions *)
 	if !interning_grammar || env.unb then
-	  (GVar (loc,id), [], [], []), args
+	  (gvar (loc,id) us, [], [], []), args
 	else error_global_not_found_loc loc qid
 
 let interp_reference vars r =
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 3bf6f37649..29af199a1e 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -208,30 +208,29 @@ let restrict_instance evd evk filter argsv =
 
 let noccur_evar env evd evk c =
   let cache = ref Int.Set.empty (* cache for let-ins *) in
-  let rec occur_rec (k, env as acc) c =
+  let rec occur_rec check_types (k, env as acc) c =
   match kind_of_term c with
   | Evar (evk',args' as ev') ->
       (match safe_evar_value evd ev' with
-       | Some c -> occur_rec acc c
+       | Some c -> occur_rec check_types acc c
        | None ->
            if Evar.equal evk evk' then raise Occur
-           else Array.iter (occur_rec acc) args')
+           else (if check_types then
+                   occur_rec false acc (existential_type evd ev');
+                 Array.iter (occur_rec check_types acc) args'))
   | Rel i when i > k ->
-      if not (Int.Set.mem (i-k) !cache) then
-      (match pi2 (Environ.lookup_rel i env) with
-       | None -> ()
-       | Some b -> cache := Int.Set.add (i-k) !cache; occur_rec acc (lift i b))
-  | Proj (p,c) -> 
-    let c = 
-      try Retyping.expand_projection env evd p c []
-      with Retyping.RetypeError _ -> 
-	(* Can happen when called from w_unify which doesn't assign evars/metas 
-	   eagerly enough *) c
-    in occur_rec acc c
+     if not (Int.Set.mem (i-k) !cache) then
+       let decl = Environ.lookup_rel i env in
+       if check_types then
+         (cache := Int.Set.add (i-k) !cache; occur_rec false acc (lift i (pi3 decl)));
+       (match pi2 decl with
+        | None -> ()
+        | Some b -> cache := Int.Set.add (i-k) !cache; occur_rec false acc (lift i b))
+  | Proj (p,c) -> occur_rec true acc c
   | _ -> iter_constr_with_full_binders (fun rd (k,env) -> (succ k, push_rel rd env))
-    occur_rec acc c
+    (occur_rec check_types) acc c
   in
-  try occur_rec (0,env) c; true with Occur -> false
+  try occur_rec false (0,env) c; true with Occur -> false
 
 (***************************************)
 (* Managing chains of local definitons *)
diff --git a/test-suite/bugs/closed/3825.v b/test-suite/bugs/closed/3825.v
index e594b74b62..666c64631f 100644
--- a/test-suite/bugs/closed/3825.v
+++ b/test-suite/bugs/closed/3825.v
@@ -14,3 +14,11 @@ Notation qux := (nat -> nat).
 
 Fail Check qux@{i}.
 
+Axiom TruncType@{i} : nat -> Type@{i}.
+
+Notation "n -Type" := (TruncType n) (at level 1) : type_scope.
+Notation hProp := (0)-Type.
+
+Check hProp.
+Check hProp@{i}.
+
diff --git a/test-suite/bugs/closed/4375.v b/test-suite/bugs/closed/4375.v
index 03af16535b..71e3a75187 100644
--- a/test-suite/bugs/closed/4375.v
+++ b/test-suite/bugs/closed/4375.v
@@ -93,14 +93,15 @@ Polymorphic CoInductive foo@{i} (T : Type@{i}) : Type@{i} :=
 | A : foo T -> foo T.
 
 Polymorphic CoFixpoint cg@{i} (t : Type@{i}) : foo@{i} t :=
-  @A@{i} t (cg@{i} t).
+  @A@{i} t (cg t).
 
 Print cg.
 
 Polymorphic CoFixpoint ca@{i} (t : Type@{i}) : foo@{i} t :=
-  @A@{i} t (@cb@{i} t)
+  @A@{i} t (cb t)
 with cb@{i} (t : Type@{i}) : foo@{i} t :=
-  @A@{i} t (@ca@{i} t).
+  @A@{i} t (ca t).
 
 Print ca.
-Print cb.
\ No newline at end of file
+Print cb.
+  
\ No newline at end of file
diff --git a/test-suite/success/vm_univ_poly.v b/test-suite/success/vm_univ_poly.v
index 58fa39743d..62df96c0b8 100644
--- a/test-suite/success/vm_univ_poly.v
+++ b/test-suite/success/vm_univ_poly.v
@@ -38,8 +38,8 @@ Definition _4 : sumbool_copy x = x :=
 
 (* Polymorphic Inductive Types *)
 Polymorphic Inductive poption@{i} (T : Type@{i}) : Type@{i} :=
-| PSome : T -> poption@{i} T
-| PNone : poption@{i} T.
+| PSome : T -> poption T
+| PNone : poption T.
 
 Polymorphic Definition poption_default@{i} {T : Type@{i}} (p : poption@{i} T) (x : T) : T :=
   match p with
@@ -49,7 +49,7 @@ Polymorphic Definition poption_default@{i} {T : Type@{i}} (p : poption@{i} T) (x
 
 Polymorphic Inductive plist@{i} (T : Type@{i}) : Type@{i} :=
 | pnil
-| pcons : T -> plist@{i} T -> plist@{i} T.
+| pcons : T -> plist T -> plist T.
 
 Arguments pnil {_}.
 Arguments pcons {_} _ _.
@@ -59,7 +59,7 @@ Polymorphic Definition pmap@{i j}
   fix pmap (ls : plist@{i} T) : plist@{j} U :=
     match ls with
     | @pnil _ => @pnil _
-    | @pcons _ l ls => @pcons@{j} U (f l) (pmap@{i j} ls)
+    | @pcons _ l ls => @pcons@{j} U (f l) (pmap ls)
     end.
 
 Universe Ubool.
@@ -75,7 +75,7 @@ Eval vm_compute in pmap (fun x => x -> Type) (pcons tbool (pcons (plist tbool) p
 
 Polymorphic Inductive Tree@{i} (T : Type@{i}) : Type@{i} :=
 | Empty
-| Branch : plist@{i} (Tree@{i} T) -> Tree@{i} T.
+| Branch : plist@{i} (Tree T) -> Tree T.
 
 Polymorphic Definition pfold@{i u}
             {T : Type@{i}} {U : Type@{u}} (f : T -> U -> U) :=
@@ -111,7 +111,7 @@ Polymorphic Fixpoint repeat@{i} {T : Type@{i}} (n : nat@{i}) (v : T) : plist@{i}
 Polymorphic Fixpoint big_tree@{i} (n : nat@{i}) : Tree@{i} nat@{i} :=
   match n with
   | O => @Empty nat@{i}
-  | S n' => Branch@{i} nat@{i} (repeat@{i} n' (big_tree@{i} n'))
+  | S n' => Branch@{i} nat@{i} (repeat@{i} n' (big_tree n'))
   end.
 
 Eval compute in height (big_tree (S (S (S O)))).