Fix #6257: anomaly with Printing Projections and Context.

Constrextern.explicitize expected that if implicits were declared they
would be declared at least up to the principal argument of the
projection, but Context/discharge of implicits does not preserve this.

Note the anomaly only happens with primitive projections DISABLED in
recent Coqs (>=8.8).

Implicit argument experts may consider whether ensuring enough
implicits are declared would be better.

3 files changed, 22 insertions, 3 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 19444988b..a7c40e9fa 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -590,11 +590,17 @@ let explicitize inctx impl (cf,f) args =
   let expl () = 
     match ip with
     | Some i ->
-      if not (List.is_empty impl) && is_status_implicit (List.nth impl (i-1)) then
-	raise Expl
+      (* Careful: It is possible to have declared implicits ending
+         before the principal argument *)
+      let is_impl =
+        try is_status_implicit (List.nth impl (i-1))
+        with Failure _ -> false
+      in
+      if is_impl
+      then raise Expl
       else
 	let (args1,args2) = List.chop i args in
-	let (impl1,impl2) = if List.is_empty impl then [],[] else List.chop i impl in
+        let (impl1,impl2) = try List.chop i impl with Failure _ -> impl, [] in
 	let args1 = exprec 1 (args1,impl1) in
 	let args2 = exprec (i+1) (args2,impl2) in
 	let ip = Some (List.length args1) in
diff --git a/test-suite/output/Projections.out b/test-suite/output/Projections.out
new file mode 100644
index 000000000..e9c28faf1
--- /dev/null
+++ b/test-suite/output/Projections.out
@@ -0,0 +1,2 @@
+fun S : store => S.(store_funcs)
+     : store -> host_func
diff --git a/test-suite/output/Projections.v b/test-suite/output/Projections.v
new file mode 100644
index 000000000..098a518dc
--- /dev/null
+++ b/test-suite/output/Projections.v
@@ -0,0 +1,11 @@
+
+Set Printing Projections.
+
+Class HostFunction := host_func : Type.
+
+Section store.
+  Context `{HostFunction}.
+  Record store := { store_funcs : host_func }.
+End store.
+
+Check (fun (S:@store nat) => S.(store_funcs)).