made Vector.nth substructural

doc/changelog/11-standard-library/16731-stdlib-vector.rst

@@ -0,0 +1,5 @@
+- **Changed:**
+  implementation of :g:`Vector.nth` to follow OCaml and compute strict subterms
+  (`#16731 <https://github.com/coq/coq/pull/16731>`_,
+  fixes `#16738 <https://github.com/coq/coq/issues/16738>`_,
+  by Andrej Dudenhefner).

test-suite/bugs/bug_16738.v

@@ -0,0 +1,11 @@
+Require Vector.
+
+Inductive container : Type :=
+  | container_v : Vector.t container 2 -> container
+  | container_0 : container.
+
+Fixpoint test (c : container) : unit :=
+  match c with
+  | container_0 => tt
+  | container_v v => test (Vector.nth v (Fin.FS Fin.F1))
+  end.

theories/Vectors/VectorDef.v

@@ -106,12 +106,15 @@ Definition const {A} (a:A) := nat_rect _ [] (fun n x => cons _ a n x).
 Computational behavior of this function should be the same as
 ocaml function. *)
 Definition nth {A} :=
-fix nth_fix {m} (v' : t A m) (p : Fin.t m) {struct v'} : A :=
-match p in Fin.t m' return t A m' -> A with
- |Fin.F1 => caseS (fun n v' => A) (fun h n t => h)
- |Fin.FS p' => fun v => (caseS (fun n v' => Fin.t n -> A)
-   (fun h n t p0 => nth_fix t p0) v) p'
-end v'.
+  fix nth_fix {n : nat} (v : t A n) {struct v} : Fin.t n -> A :=
+    match v with
+    | nil _ => fun p => False_rect A (Fin.case0 _ p)
+    | cons _ x m v' => fun p =>
+      match p in (Fin.t m') return t A (pred m') -> A with
+      | Fin.F1 => fun _ => x
+      | Fin.FS p' => fun v' => nth_fix v' p'
+      end v'
+    end.
 
 (** An equivalent definition of [nth]. *)
 Definition nth_order {A} {n} (v: t A n) {p} (H: p < n) :=