|
(* 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.
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
