From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- test-suite/bugs/closed/3672.v | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 test-suite/bugs/closed/3672.v (limited to 'test-suite/bugs/closed/3672.v') diff --git a/test-suite/bugs/closed/3672.v b/test-suite/bugs/closed/3672.v new file mode 100644 index 00000000..283be495 --- /dev/null +++ b/test-suite/bugs/closed/3672.v @@ -0,0 +1,27 @@ +Set Primitive Projections. (* No failures without this option. *) + +Record AT := +{ atype :> Type +; coerce : atype -> Type +}. +Coercion coerce : atype >-> Sortclass. + +Record Ar C (A:AT) := { ar : forall (X Y : C), A }. + +Definition t := forall C A a X, coerce _ (ar C A a X X). +Definition t' := forall C A a X, ar C A a X X. + +(* The command has indeed failed with message: +=> Error: The term "ar C A a X X" has type "atype A" which is not a (co-)inductive type. +*) + +Record Ar2 C (A:AT) := +{ ar2 : forall (X Y : C), A +; id2 : forall X, coerce _ (ar2 X X) }. + +Record Ar3 C (A:AT) := +{ ar3 : forall (X Y : C), A +; id3 : forall X, ar3 X X }. +(* The command has indeed failed with message: +=> Anomaly: Bad recursive type. Please report. +*) \ No newline at end of file -- cgit v1.2.3