diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2018-01-04 05:40:08 -0800 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2018-03-08 07:40:27 -0300 |
commit | fd2e9fd5f859f729765706f1f56df0fa080c0513 (patch) | |
tree | 33f0090f7d0e47c544621120ab52e2e5646be9ee /pretyping/evarconv.ml | |
parent | 563199757c5756fb5858da1b684162566a73fa3e (diff) |
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.
Diffstat (limited to 'pretyping/evarconv.ml')
-rw-r--r-- | pretyping/evarconv.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 0a63985bf..3c8acb1a7 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 |