1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
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.
*)
|
