aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/modules/subtyping.v
blob: dd7daf429d4d3e01166d19703bb4b78d6c337c29 (plain)
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
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
(* Non regression for bug #1302 *)

(* With universe polymorphism for inductive types, subtyping of
   inductive types needs a special treatment: the standard conversion
   algorithm does not work as it only knows to deal with constraints of
   the form alpha = beta or max(alphas, alphas+1) <= beta, while
   subtyping of inductive types in Type generates constraints of the form
   max(alphas, alphas+1) <= max(betas, betas+1).

   These constraints are anyway valid by monotonicity of subtyping but we
   have to detect it early enough to avoid breaking the standard
   algorithm for constraints on algebraic universes. *)

Module Type T.

 Parameter A : Type (* Top.1 *) .

 Inductive L : Type (* max(Top.1,1) *) :=
 | L0
 | L1 :  (A -> Prop) -> L.

End T.

Axiom Tp : Type (* Top.5 *) .

Module TT : T.

 Definition A : Type (* Top.6 *) := Tp. (* generates Top.5 <= Top.6 *)

 Inductive L : Type (* max(Top.6,1) *) :=
 | L0
 | L1 :  (A -> Prop) -> L.

End TT. (* Generates Top.6 <= Top.1 (+ auxiliary constraints for L_rect) *)

(* Note: Top.6 <= Top.1 is generated by subtyping on A;
   subtyping of L follows and has not to be checked *)



(* The same bug as #1302 but for Definition *)
(* Check that inferred algebraic universes in interfaces are considered *)

Module Type U. Definition A := Type -> Type. End U.
Module M:U. Definition A := Type -> Type. End M.