From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- test-suite/modules/subtyping.v | 46 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) create mode 100644 test-suite/modules/subtyping.v (limited to 'test-suite/modules/subtyping.v') diff --git a/test-suite/modules/subtyping.v b/test-suite/modules/subtyping.v new file mode 100644 index 00000000..2df8e84e --- /dev/null +++ b/test-suite/modules/subtyping.v @@ -0,0 +1,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. + -- cgit v1.2.3