Fix bug #3656.

Maintain the user-level view of primitive projections,
disallow manual unfolding and do not let hnf give the eta-expanded
form.

2 files changed, 66 insertions, 7 deletions

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 6f6de95fc..8dafadbe4 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -577,13 +577,11 @@ let reduce_projection env sigma pb (recarg'hd,stack') stack =
   | _ -> NotReducible)
 
 let reduce_proj env sigma whfun whfun' c =
-  (* Pp.msgnl (str" reduce_proj: " ++ print_constr c); *)
   let rec redrec s =
     match kind_of_term s with
     | Proj (proj, c) -> 
       let c' = try redrec c with Redelimination -> c in
       let constr, cargs = whfun c' in
-	(* Pp.msgnl (str" reduce_proj: constructor: " ++ print_constr constr); *)
 	(match kind_of_term constr with
 	| Construct _ -> 
 	  let proj_narg = 
@@ -920,6 +918,15 @@ let whd_simpl_orelse_delta_but_fix env sigma c =
     | Some c ->
       (match kind_of_term (strip_lam c) with
       | CoFix _ | Fix _ -> s'
+      | Proj (p,c) when
+	  (match kind_of_term constr with
+	  | Const (c', _) -> eq_constant p c'
+	  | _ -> false) ->
+	let pb = Environ.lookup_projection p env in
+	  if List.length stack <= pb.Declarations.proj_npars then
+	    (** Do not show the eta-expanded form *)
+	    s'
+	  else redrec (applist (c, stack))
       | _ -> redrec (applist(c, stack)))
     | None -> s'
   in
@@ -1016,7 +1023,6 @@ let contextually byhead occs f env sigma t =
 let match_constr_evaluable_ref sigma c evref = 
   match kind_of_term c, evref with
   | Const (c,u), EvalConstRef c' when eq_constant c c' -> Some u
-  | Proj (p,c), EvalConstRef p' when eq_constant p p' -> Some Univ.Instance.empty
   | Var id, EvalVarRef id' when id_eq id id' -> Some Univ.Instance.empty
   | _, _ -> None
 
@@ -1024,10 +1030,7 @@ let substlin env sigma evalref n (nowhere_except_in,locs) c =
   let maxocc = List.fold_right max locs 0 in
   let pos = ref n in
   assert (List.for_all (fun x -> x >= 0) locs);
-  let value u = 
-    value_of_evaluable_ref env evalref u 
-          (* Some (whd_betaiotazeta sigma c) *)
-  in
+  let value u = value_of_evaluable_ref env evalref u in
   let rec substrec () c =
     if nowhere_except_in && !pos > maxocc then c
     else 
@@ -1058,11 +1061,18 @@ let unfold env sigma name =
   else
     error (string_of_evaluable_ref env name^" is opaque.")
 
+let is_projection env = function
+  | EvalVarRef _ -> false
+  | EvalConstRef c -> Environ.is_projection c env
+
 (* [unfoldoccs : (readable_constraints -> (int list * full_path) -> constr -> constr)]
  * Unfolds the constant name in a term c following a list of occurrences occl.
  * at the occurrences of occ_list. If occ_list is empty, unfold all occurences.
  * Performs a betaiota reduction after unfolding. *)
 let unfoldoccs env sigma (occs,name) c =
+  if is_projection env name then
+    error ("Cannot unfold primitie projection " ^ string_of_evaluable_ref env name)
+  else
   let unfo nowhere_except_in locs =
     let (nbocc,uc) = substlin env sigma name 1 (nowhere_except_in,locs) c in
     if Int.equal nbocc 1 then
diff --git a/test-suite/bugs/closed/3656.v b/test-suite/bugs/closed/3656.v
new file mode 100644
index 000000000..218cb755b
--- /dev/null
+++ b/test-suite/bugs/closed/3656.v
@@ -0,0 +1,49 @@
+Module A.
+  Set Primitive Projections.
+  Record hSet : Type := BuildhSet { setT : Type;  iss : True }.
+  Ltac head_hnf_under_binders x :=
+  match eval hnf in x with
+    | ?f _ => head_hnf_under_binders f
+    | (fun y => ?f y) => head_hnf_under_binders f
+    | ?y => y
+  end.
+Goal forall s : hSet, True.
+intros. 
+let x := head_hnf_under_binders setT in pose x.
+
+set (foo := eq_refl (@setT )). generalize foo. simpl. cbn. 
+Abort.
+End A.
+
+Module A'.
+Set Universe Polymorphism.
+ Set Primitive Projections.
+Record hSet (A : Type) : Type := BuildhSet { setT : Type;  iss : True }.
+Ltac head_hnf_under_binders x :=
+  match eval compute in x with
+    | ?f _ => head_hnf_under_binders f
+    | (fun y => ?f y) => head_hnf_under_binders f
+    | ?y => y
+  end.
+Goal forall s : @hSet nat, True.
+intros. 
+let x := head_hnf_under_binders setT in pose x.
+
+set (foo := eq_refl (@setT nat)). generalize foo. simpl. cbn. 
+Abort.
+End A'.
+
+Set Primitive Projections.
+Record hSet : Type := BuildhSet { setT : Type;  iss : True }.
+Ltac head_hnf_under_binders x :=
+  match eval hnf in x with
+    | ?f _ => head_hnf_under_binders f
+    | (fun y => ?f y) => head_hnf_under_binders f
+    | ?y => y
+  end.
+Goal setT = setT.
+ Fail progress unfold setT. (* should not succeed *)
+ match goal with
+    | |- (fun h => setT h) = (fun h => setT h) => fail 1 "should not eta-expand"
+    | _ => idtac
+  end. (* should not fail *)
\ No newline at end of file