diff options
| author | Maxime Dénès | 2018-10-30 09:33:01 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-11-06 14:19:38 +0100 |
| commit | bcdab3b90ad2e651a41b8a8092e161f42b0ca912 (patch) | |
| tree | 2c4d73f6f3052082c0408d3320e185c16b676457 | |
| parent | 732476594f19be0125a553b1c6135d57995c63c2 (diff) | |
[checker] Check univ constraints induced by module subtyping
| -rw-r--r-- | checker/mod_checking.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 31087a1bb6..94e7c29201 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -75,7 +75,9 @@ let rec check_module env mp mb = let mtb1 = mk_mtb mp sign mb.mod_delta and mtb2 = mk_mtb mp mb.mod_type mb.mod_delta in let env = Modops.add_module_type mp mtb1 env in - let _ = Subtyping.check_subtypes env mtb1 mtb2 in () + let cu = check_subtypes env mtb1 mtb2 in + if not (Environ.check_constraints cu env) then + CErrors.user_err Pp.(str "Incorrect universe constraints for module subtyping"); and check_module_type env mty = Flags.if_verbose Feedback.msg_notice (str " checking module type: " ++ str (ModPath.to_string mty.mod_mp)); @@ -106,7 +108,9 @@ and check_mexpr env mse mp_mse res = match mse with let sign = check_mexpr env f mp_mse res in let farg_id, farg_b, fbody_b = Modops.destr_functor sign in let mtb = Modops.module_type_of_module (lookup_module mp env) in - let _ = check_subtypes env mtb farg_b in (* Should we stop inferring constraints? *) + let cu = check_subtypes env mtb farg_b in + if not (Environ.check_constraints cu env) then + CErrors.user_err Pp.(str "Incorrect universe constraints for module subtyping"); Modops.subst_signature (Mod_subst.map_mbid farg_id mp Mod_subst.empty_delta_resolver) fbody_b | MEwith _ -> CErrors.user_err Pp.(str "Unsupported 'with' constraint in module implementation") |