1 files changed, 79 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/2966.v b/test-suite/bugs/closed/2966.v
new file mode 100644
index 00000000..debada85
--- /dev/null
+++ b/test-suite/bugs/closed/2966.v
@@ -0,0 +1,79 @@
+(** Non-termination and state monad with extraction *)
+Require Import List.
+
+Set Implicit Arguments.
+Set Asymmetric Patterns.
+
+Module MemSig.
+  Definition t: Type := list Type.
+  
+  Definition Nth (sig: t) (n: nat) :=
+    nth n sig unit.
+End MemSig.
+
+(** A memory of type [Mem.t s] is the union of cells whose type is specified
+    by [s]. *)
+Module Mem.
+  Inductive t: MemSig.t -> Type :=
+  | Nil: t nil
+  | Cons: forall (T: Type), option T -> forall (sig: MemSig.t), t sig ->
+    t (T :: sig).
+End Mem.
+
+Module Ref.
+  Inductive t (sig: MemSig.t) (T: Type): Type :=
+  | Input: t sig T.
+  
+  Definition Read (sig: MemSig.t) (T: Type) (ref: t sig T) (s: Mem.t sig)
+    : option T :=
+    match ref with
+    | Input => None
+    end.
+End Ref.
+
+Module Monad.
+  Definition t (sig: MemSig.t) (A: Type) :=
+    Mem.t sig -> option A * Mem.t sig.
+  
+  Definition Return (sig: MemSig.t) (A: Type) (x: A): t sig A :=
+    fun s =>
+      (Some x, s).
+  
+  Definition Bind (sig: MemSig.t) (A B: Type) (x: t sig A) (f: A -> t sig B)
+    : t sig B :=
+    fun s =>
+    match x s with
+    | (Some x', s') => f x' s'
+    | (None, s') => (None, s')
+    end.
+
+  Definition Select (T: Type) (f g: unit -> T): T :=
+    f tt.
+  
+  (** Read in a reference. *)
+  Definition Read (sig: MemSig.t) (T: Type) (ref: Ref.t sig T)
+    : t sig T :=
+    fun s =>
+      match Ref.Read ref s with
+      | None => (None, s)
+      | Some x => (Some x, s)
+      end.
+End Monad.
+
+Import Monad.
+
+Definition pop (sig: MemSig.t) (T: Type) (trace: Ref.t sig (list T))
+  : Monad.t sig T :=
+  Bind (Read trace) (fun _ s => (None, s)).
+
+Definition sig: MemSig.t := (list nat: Type) :: nil.
+
+Definition trace: Ref.t sig (list nat).
+Admitted.
+
+Definition Gre (sig: MemSig.t) (trace: _)
+    (f: bool -> bool): Monad.t sig nat :=
+    Select (fun _ => pop trace) (fun _ => Return 0).
+
+Definition Arg :=
+  Gre trace (fun _ => false).