1 files changed, 144 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/3345.v b/test-suite/bugs/opened/3345.v
new file mode 100644
index 00000000..b61174a8
--- /dev/null
+++ b/test-suite/bugs/opened/3345.v
@@ -0,0 +1,144 @@
+(* File reduced by coq-bug-finder from original input, then from 1972 lines to 136 lines, then from 119 lines to 105 lines *)
+Global Set Implicit Arguments.
+Require Import Coq.Lists.List Program.
+Section IndexBound.
+  Context {A : Set}.
+  Class IndexBound (a : A) (Bound : list A) :=
+    { ibound :> nat;
+      boundi : nth_error Bound ibound = Some a}.
+  Global Arguments ibound [a Bound] _ .
+  Global Arguments boundi [a Bound] _.
+  Record BoundedIndex (Bound : list A) := { bindex :> A; indexb :> IndexBound bindex Bound }.
+End IndexBound.
+Context {A : Type} {C : Set}.
+Variable (projAC : A -> C).
+Lemma None_neq_Some
+: forall (AnyT AnyT' : Type) (a : AnyT),
+    None = Some a -> AnyT'.
+  admit.
+Defined.
+Program Definition nth_Bounded'
+           (Bound : list A)
+           (c : C)
+           (a_opt : option A)
+           (nth_n : option_map projAC a_opt = Some c)
+: A := match a_opt as x
+             return (option_map projAC x = Some c) -> A with
+         | Some a => fun _ => a
+         | None => fun f : None = Some _ => !
+       end nth_n.
+Lemma nth_error_map :
+  forall n As c_opt,
+    nth_error (map projAC As) n = c_opt
+    -> option_map projAC (nth_error As n) = c_opt.
+  admit.
+Defined.
+Definition nth_Bounded
+           (Bound : list A)
+           (idx : BoundedIndex (map projAC Bound))
+: A := nth_Bounded' Bound (nth_error Bound (ibound idx))
+                    (nth_error_map _ _ (boundi idx)).
+Program Definition nth_Bounded_ind2
+        (P : forall As, BoundedIndex (map projAC As)
+                        -> BoundedIndex (map projAC As)
+                        -> A -> A -> Prop)
+: forall (Bound : list A)
+         (idx : BoundedIndex (map projAC Bound))
+         (idx' : BoundedIndex (map projAC Bound)),
+    match nth_error Bound (ibound idx), nth_error Bound (ibound idx') with
+      | Some a, Some a' => P Bound idx idx' a a'
+      | _, _ => True
+    end
+    -> P Bound idx idx' (nth_Bounded _ idx) (nth_Bounded _ idx'):=
+  fun Bound idx idx' =>
+    match (nth_error Bound (ibound idx)) as e, (nth_error Bound (ibound idx')) as e'
+          return
+          (forall (f : option_map _ e = Some (bindex idx))
+                  (f' : option_map _ e' = Some (bindex idx')),
+             (match e, e' with
+                | Some a, Some a' => P Bound idx idx' a a'
+                | _, _ => True
+              end)
+             -> P Bound idx idx'
+                  (match e as e'' return
+                         option_map _ e'' = Some (bindex idx)
+                         -> A
+                   with
+                     | Some a => fun _ => a
+                     | _ => fun f => _
+                   end f)
+                  (match e' as e'' return
+                         option_map _ e'' = Some (bindex idx')
+                         -> A
+                   with
+                     | Some a => fun _ => a
+                     | _ => fun f => _
+                   end f')) with
+      | Some a, Some a' => fun _ _ H => _
+      | _, _ => fun f => _
+    end (nth_error_map _ _ (boundi idx))
+        (nth_error_map _ _ (boundi idx')).
+
+Lemma nth_Bounded_eq
+: forall (Bound : list A)
+         (idx idx' : BoundedIndex (map projAC Bound)),
+    ibound idx = ibound idx'
+    -> nth_Bounded Bound idx = nth_Bounded Bound idx'.
+Proof.
+  intros.
+  eapply nth_Bounded_ind2 with (idx := idx) (idx' := idx').
+  simpl.
+  (* The [case_eq] should not Fail.  More importantly, [Fail case_eq ...] should succeed if [case_eq ...] fails.  It doesn't!!!  So I resort to [Fail Fail try (case_eq ...)]. *)
+  Fail Fail try (case_eq (nth_error Bound (ibound idx'))).
+(* Toplevel input, characters 15-54:
+In nested Ltac calls to "case_eq" and "pattern x at - 1", last call failed.
+Error: The abstracted term
+"fun e : Exc A =>
+ forall e0 : nth_error Bound (ibound idx') = e,
+ match
+   nth_error Bound (ibound idx) as anonymous'0
+   return (anonymous'0 = nth_error Bound (ibound idx) -> e = e -> Prop)
+ with
+ | Some a =>
+     match
+       e as anonymous'
+       return
+         (Some a = nth_error Bound (ibound idx) -> anonymous' = e -> Prop)
+     with
+     | Some a' =>
+         fun (_ : Some a = nth_error Bound (ibound idx)) (_ : Some a' = e) =>
+         a = a'
+     | None =>
+         fun (_ : Some a = nth_error Bound (ibound idx)) (_ : None = e) =>
+         True
+     end
+ | None => fun (_ : None = nth_error Bound (ibound idx)) (_ : e = e) => True
+ end eq_refl e0" is not well typed.
+Illegal application:
+The term
+ "match
+    nth_error Bound (ibound idx) as anonymous'0
+    return (anonymous'0 = nth_error Bound (ibound idx) -> e = e -> Prop)
+  with
+  | Some a =>
+      match
+        e as anonymous'
+        return
+          (Some a = nth_error Bound (ibound idx) -> anonymous' = e -> Prop)
+      with
+      | Some a' =>
+          fun (_ : Some a = nth_error Bound (ibound idx)) (_ : Some a' = e) =>
+          a = a'
+      | None =>
+          fun (_ : Some a = nth_error Bound (ibound idx)) (_ : None = e) =>
+          True
+      end
+  | None => fun (_ : None = nth_error Bound (ibound idx)) (_ : e = e) => True
+  end" of type
+ "nth_error Bound (ibound idx) = nth_error Bound (ibound idx) ->
+  e = e -> Prop"
+cannot be applied to the terms
+ "eq_refl" : "nth_error Bound (ibound idx) = nth_error Bound (ibound idx)"
+ "e0" : "nth_error Bound (ibound idx') = e"
+The 2nd term has type "nth_error Bound (ibound idx') = e"
+which should be coercible to "e = e". *)