1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
Axioms A B : Type -> Type.
Axiom f : A nat -> B Type.
Definition A' := A nat.
Definition f' : A' -> B Type := f.
Coercion f' : A' >-> B.
Check (_ : A nat) : A'.
Fail Check (_ : A nat) : B Type. (* The term "?11:A nat" has type "A nat" while it is expected to have type "B Type". *)
Check ((_ : A nat) : A') : B Type. (* ((?11:A nat):A'):B Type *)
Fail Identity Coercion f'_id : A >-> A'. (* Error: in build_id_coercion: A must be a transparent constant. *)
Identity Coercion f'_id : A' >-> A.
Fail Check (_ : A nat) : B Type. (* The term "?11:A nat" has type "A nat" while it is expected to have type "B Type". *)
Coercion f : A >-> B. (* Warning: f does not respect the uniform inheritance condition *)
Check (_ : A nat) : B Type. (* Anomaly: apply_coercion_args. Please report. *)
|
