diff options
Diffstat (limited to 'test-suite/bugs/closed/3672.v')
-rw-r--r-- | test-suite/bugs/closed/3672.v | 27 |
1 files changed, 27 insertions, 0 deletions
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 |