diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-05-13 23:38:55 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-05-13 23:40:38 +0200 |
commit | d91addb140ba7315d70c4599b0d058bef798ac1c (patch) | |
tree | 9e4582ce5d8b7456fd7de6850941ee359d82fea4 /test-suite/bugs/closed | |
parent | 3a7095f9f6a09a4461c2124b0020dfe37962de26 (diff) |
Fixing bug #4216:
Internal error: Anomaly: Uncaught exception Not_found. Please report.
An evarmap was lost because of an unsound typing primitive.
Diffstat (limited to 'test-suite/bugs/closed')
-rw-r--r-- | test-suite/bugs/closed/4216.v | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4216.v b/test-suite/bugs/closed/4216.v new file mode 100644 index 000000000..ae7f74677 --- /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)). + |