From fd2e9fd5f859f729765706f1f56df0fa080c0513 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 4 Jan 2018 05:40:08 -0800 Subject: Relax conversion of constructors according to the pCuIC model - Nothing to check in conversion as they have a common supertype by typing. - In inference, enforce that one is lower than the other. --- kernel/reduction.ml | 5 +++-- pretyping/evarconv.ml | 10 ++++++++-- 2 files changed, 11 insertions(+), 4 deletions(-) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index e9be1b35df..b3e6894143 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -269,8 +269,9 @@ let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u if not (Int.equal num_cnstr_args nargs) then cmp_instances u1 u2 s else - let csts = get_cumulativity_constraints CONV cumi u1 u2 in - cmp_cumul csts s + (** By invariant, both constructors have a common supertype, + so they are convertible _at that type_. *) + s let convert_constructors ctor nargs u1 u2 (s, check) = convert_constructors_gen (check.compare_instances ~flex:false) check.compare_cumul_instances diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 0a63985bf1..3c8acb1a78 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -530,8 +530,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty UnifFailure (evd, NotSameHead) else begin - let evd' = check_leq_inductives evd cumi u u' in - Success (check_leq_inductives evd' cumi u' u) + (** Both constructors should be liftable to the same supertype + at which we compare them, but we don't have access to that type in + untyped unification. We hence enforce that one is lower than the other. + Note the criterion is more relaxed in conversion. *) + try Success (check_leq_inductives evd cumi u u') + with Univ.UniverseInconsistency _ -> + try Success (check_leq_inductives evd cumi u' u) + with Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e) end end in -- cgit v1.2.3 From d3f88e4e3aaf346f88801737c9145fe114f4942b Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 8 Mar 2018 07:20:32 -0300 Subject: Update checker to reflect rule on constructors of polymorphic inductive types --- checker/reduction.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/checker/reduction.ml b/checker/reduction.ml index 67d00b21d9..97255dd49e 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -201,7 +201,9 @@ let convert_constructors if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then convert_universes univs u1 u2 else - convert_inductive_instances CONV cumi u1 u2 univs + (** By invariant, both constructors have a common supertype, + so they are convertible _at that type_. *) + () (* Convertibility of sorts *) -- cgit v1.2.3 From ce87e338529f4dd174f1c870b83162bac6d2b9ae Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 8 Mar 2018 07:23:03 -0300 Subject: Leave cumul constructor universes as is during unif if we cannot coerce one constructor type to the other. By invariant they have a common supertype --- pretyping/evarconv.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 3c8acb1a78..fe2e86a482 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -532,12 +532,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty begin (** Both constructors should be liftable to the same supertype at which we compare them, but we don't have access to that type in - untyped unification. We hence enforce that one is lower than the other. - Note the criterion is more relaxed in conversion. *) + untyped unification. We hence try to enforce that one is lower + than the other, also unifying more universes in the process. + If this fails we just leave the universes as is, as in conversion. *) try Success (check_leq_inductives evd cumi u u') with Univ.UniverseInconsistency _ -> try Success (check_leq_inductives evd cumi u' u) - with Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e) + with Univ.UniverseInconsistency e -> Success evd end end in -- cgit v1.2.3 From a7dc1040e4fbd3e996f411f6c0e46e74cae8c93b Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 8 Mar 2018 07:38:33 -0300 Subject: Add test-suite file for cumulative constructors --- test-suite/success/cumulativity.v | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v index e05762477d..4dda360423 100644 --- a/test-suite/success/cumulativity.v +++ b/test-suite/success/cumulativity.v @@ -134,3 +134,24 @@ Definition withparams_co@{i i' j|i < i', i' < j} : withparams@{i j} -> withparam Fail Definition withparams_not_irr@{i i' j|i' < i, i' < j} : withparams@{i j} -> withparams@{i' j} := fun x => x. + +(** Cumulative constructors *) + + +Record twotys@{u v w} : Type@{w} := + twoconstr { fstty : Type@{u}; sndty : Type@{v} }. + +Monomorphic Universes i j k l. + +Monomorphic Constraint i < j. +Monomorphic Constraint j < k. +Monomorphic Constraint k < l. + +Parameter Tyi : Type@{i}. + +Definition checkcumul := + eq_refl _ : @eq twotys@{k k l} (twoconstr@{i j k} Tyi Tyi) (twoconstr@{j i k} Tyi Tyi). + +(* They can only be compared at the highest type *) +Fail Definition checkcumul' := + eq_refl _ : @eq twotys@{i k l} (twoconstr@{i j k} Tyi Tyi) (twoconstr@{j i k} Tyi Tyi). -- cgit v1.2.3