diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-27 19:21:46 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-27 20:41:05 +0200 |
| commit | 02b66da78e766a0eb8a1ec82a03ec9ce5418a0f0 (patch) | |
| tree | 1d157ece2d488deaa419fbd12901ad56a2f807aa /test-suite/bugs/closed/3672.v | |
| parent | 8c32ecc205aebaf9a4da95e24463286aee1a571d (diff) | |
Fix bug #3672, application of primitive projections as coercions.
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 000000000..283be4958 --- /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 |