From d91addb140ba7315d70c4599b0d058bef798ac1c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 13 May 2015 23:38:55 +0200
Subject: Fixing bug #4216:

Internal error: Anomaly: Uncaught exception Not_found. Please report.

An evarmap was lost because of an unsound typing primitive.
---
 test-suite/bugs/closed/4216.v | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 test-suite/bugs/closed/4216.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4216.v b/test-suite/bugs/closed/4216.v
new file mode 100644
index 0000000000..ae7f746778
--- /dev/null
+++ b/test-suite/bugs/closed/4216.v
@@ -0,0 +1,20 @@
+Generalizable Variables T A.
+
+Inductive path `(a: A): A -> Type := idpath: path a a.
+
+Class TMonad (T: Type -> Type) := {
+  bind: forall {A B: Type}, (T A) -> (A -> T B) -> T B;
+  ret: forall {A: Type}, A -> T A;
+  ret_unit_left: forall {A B: Type} (k: A -> T B) (a: A),
+                 path (bind (ret a) k) (k a)
+  }.
+
+Let T_fzip `{TMonad T} := fun (A B: Type) (f: T (A -> B)) (t: T A)
+                  => bind t (fun a => bind f (fun g => ret (g a) )).
+Let T_pure `{TMonad T} := @ret _ _.
+
+Let T_pure_id `{TMonad T} {A: Type} (t: A -> A) (x: T A): 
+        path (T_fzip A A (T_pure (A -> A) t) x) x.
+  unfold T_fzip, T_pure.
+  Fail rewrite (ret_unit_left (fun g a => ret (g a)) (fun x => x)).
+
-- 
cgit v1.2.3