Skip to content

Commit 83b13be

Browse files
riaqnriaqn
authored
Module inclusion check looks at module mode (#3328)
1 parent df856b7 commit 83b13be

File tree

10 files changed

+418
-59
lines changed

10 files changed

+418
-59
lines changed

‎driver/compile_common.ml

+1-1
Original file line numberDiff line numberDiff line change
@@ -84,7 +84,7 @@ let typecheck_intf info ast =
8484
Format.(fprintf std_formatter) "%a@."
8585
(Printtyp.printed_signature (Unit_info.source_file info.target))
8686
sg);
87-
ignore (Includemod.signatures info.env ~mark:Mark_both sg sg);
87+
ignore (Includemod.signatures info.env ~mark:Mark_both ~modes:Legacy sg sg);
8888
Typecore.force_delayed_checks ();
8989
Builtin_attributes.warn_unused ();
9090
Warnings.check_fatal ();

‎testsuite/tests/typing-modes/md_modalities.ml

+1-1
Original file line numberDiff line numberDiff line change
@@ -142,5 +142,5 @@ Error: Signature mismatch:
142142
val foo : 'a -> 'a
143143
is not included in
144144
val foo : 'a -> 'a @@ portable
145-
The second is portable and the first is not.
145+
The second is portable and the first is nonportable.
146146
|}]

‎testsuite/tests/typing-modes/val_modalities.ml

+307-5
Original file line numberDiff line numberDiff line change
@@ -113,7 +113,7 @@ Error: Signature mismatch:
113113
val x : string @@ global many portable contended
114114
is not included in
115115
val x : string
116-
The second is empty and the first is contended.
116+
The second is uncontended and the first is contended.
117117
|}]
118118

119119
module Module_type_nested = struct
@@ -160,7 +160,7 @@ Error: Signature mismatch:
160160
val y : string @@ global many portable contended
161161
is not included in
162162
val y : string
163-
The second is empty and the first is contended.
163+
The second is uncontended and the first is contended.
164164
|}]
165165

166166
(* When defaulting, prioritize modes in arrow types over modalities. *)
@@ -213,7 +213,7 @@ Error: Signature mismatch:
213213
val x : string @@ global many portable contended
214214
is not included in
215215
val x : string
216-
The second is empty and the first is contended.
216+
The second is uncontended and the first is contended.
217217
|}]
218218

219219
module Inclusion_weakens_monadic = struct
@@ -342,7 +342,7 @@ Error: Signature mismatch:
342342
external length : string -> int = "%string_length"
343343
is not included in
344344
external length : string -> int @@ portable = "%string_length"
345-
The second is portable and the first is not.
345+
The second is portable and the first is nonportable.
346346
|}]
347347

348348
module M : sig
@@ -461,10 +461,312 @@ Error: Signature mismatch:
461461
val f : int -> int @@ global many
462462
is not included in
463463
val f : int -> int @@ portable
464-
The second is portable and the first is not.
464+
The second is portable and the first is nonportable.
465465
|}]
466466

467467

468+
(* module inclusion check should look at the modes of the modules, since some
469+
module type inclusion is only true for certain modes. Currently modules are
470+
always global many, which allows more module inclusion. *)
471+
472+
(* value description inclusion check look at the modes of the enclosing
473+
structure. *)
474+
module M : sig
475+
val foo : 'a -> 'a @@ global many
476+
end = struct
477+
include (struct let foo x = x end : sig val foo : 'a -> 'a end)
478+
end
479+
[%%expect{|
480+
module M : sig val foo : 'a -> 'a @@ global many end
481+
|}]
482+
483+
(* CR zqian: with non-legacy modules, we will extend the tests to modalities on
484+
module declarations, instead of relying on modalities on value descriptions to
485+
tell if the extra modes are considered. *)
486+
487+
(* module declaration inclusion check looks at the mode of the enclosing
488+
structure, which in turn affects value description inclusion check. *)
489+
module M : sig
490+
module N : sig val foo : 'a -> 'a @@ global many end
491+
end = struct
492+
module N : sig val foo : 'a -> 'a end = struct let foo x = x end
493+
end
494+
[%%expect{|
495+
module M : sig module N : sig val foo : 'a -> 'a @@ global many end end
496+
|}]
497+
498+
(* CR zqian: inclusion check should cross modes, if we are comparing modes. *)
499+
module M : sig
500+
module N : sig val foo : int @@ portable end
501+
end = struct
502+
module N = struct let foo @ nonportable = 42 end
503+
end
504+
[%%expect{|
505+
Lines 3-5, characters 6-3:
506+
3 | ......struct
507+
4 | module N = struct let foo @ nonportable = 42 end
508+
5 | end
509+
Error: Signature mismatch:
510+
Modules do not match:
511+
sig module N : sig val foo : int @@ global many end end
512+
is not included in
513+
sig module N : sig val foo : int @@ portable end end
514+
In module "N":
515+
Modules do not match:
516+
sig val foo : int @@ global many end
517+
is not included in
518+
sig val foo : int @@ portable end
519+
In module "N":
520+
Values do not match:
521+
val foo : int @@ global many
522+
is not included in
523+
val foo : int @@ portable
524+
The second is portable and the first is nonportable.
525+
|}]
526+
527+
(* module constraint inclusion check looks at the modes of modules *)
528+
module F (M : sig val foo : 'a -> 'a end) = struct
529+
module M' : sig val foo : 'a -> 'a @@ global many end = M
530+
end
531+
[%%expect{|
532+
module F :
533+
functor (M : sig val foo : 'a -> 'a end) ->
534+
sig module M' : sig val foo : 'a -> 'a @@ global many end end
535+
|}]
536+
537+
(* Similiar for recursive modules *)
538+
module rec M : sig
539+
module N : sig val foo : 'a -> 'a @@ global many end
540+
end = struct
541+
module N : sig val foo : 'a -> 'a end = struct let foo x = x end
542+
end
543+
[%%expect{|
544+
module rec M : sig module N : sig val foo : 'a -> 'a @@ global many end end
545+
|}]
546+
547+
548+
(* functor application inclusion check looks at the modes of parameter and
549+
argument *)
550+
module F (M : sig val f : 'a -> 'a @@ global many end) = struct
551+
end
552+
[%%expect{|
553+
module F : functor (M : sig val f : 'a -> 'a @@ global many end) -> sig end
554+
|}]
555+
556+
module G (M : sig val f : 'a -> 'a end) = F(M)
557+
[%%expect{|
558+
module G : functor (M : sig val f : 'a -> 'a end) -> sig end
559+
|}]
560+
561+
(* Similiar for [include_functor] *)
562+
module G (M : sig val f : 'a -> 'a end) = struct
563+
include M
564+
include functor F
565+
end
566+
[%%expect{|
567+
module G : functor (M : sig val f : 'a -> 'a end) -> sig val f : 'a -> 'a end
568+
|}]
569+
570+
(* functor declaration inclusion check looks at the modes of parameter and
571+
return*)
572+
module F : (sig val foo : 'a -> 'a end) -> (sig val bar : 'a -> 'a @@ global many end) =
573+
functor (M : sig val foo : 'a -> 'a @@ global many end) -> struct let bar = M.foo end
574+
[%%expect{|
575+
module F :
576+
sig val foo : 'a -> 'a end -> sig val bar : 'a -> 'a @@ global many end
577+
|}]
578+
579+
(* CR zqian: package subtyping doesn't look at the package mode for simplicity.
580+
NB: coercion is the only place of subtype checking packages; all other places
581+
are equality check. *)
582+
module type S = sig val foo : 'a -> 'a @@ global many end
583+
module type S' = sig val foo : 'a -> 'a end
584+
585+
let f (x : (module S)) = (x : (module S) :> (module S'))
586+
[%%expect{|
587+
module type S = sig val foo : 'a -> 'a @@ global many end
588+
module type S' = sig val foo : 'a -> 'a end
589+
val f : (module S) -> (module S') @@ global many = <fun>
590+
|}]
591+
592+
let f (x : (module S')) = (x : (module S') :> (module S))
593+
[%%expect{|
594+
Line 1, characters 26-57:
595+
1 | let f (x : (module S')) = (x : (module S') :> (module S))
596+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
597+
Error: Type "(module S')" is not a subtype of "(module S)"
598+
|}]
599+
600+
(* module equality/substitution inclusion check looks at modes of modules, even
601+
when inside a module type declaration *)
602+
module type S = sig
603+
module M : sig
604+
val foo : 'a -> 'a @@ global many
605+
end
606+
end
607+
608+
module type F = functor (M':sig val foo : 'a -> 'a end) -> sig
609+
module Subst : sig
610+
module type S' = S with module M := M'
611+
612+
module M'' : sig val foo : 'a -> 'a end
613+
module type S'' = S with module M := M''
614+
end
615+
616+
module Eq : sig
617+
module type S' = S with module M = M'
618+
619+
module M'' : sig val foo : 'a -> 'a end
620+
module type S'' = S with module M := M''
621+
end
622+
end
623+
624+
[%%expect{|
625+
module type S = sig module M : sig val foo : 'a -> 'a @@ global many end end
626+
module type F =
627+
functor (M' : sig val foo : 'a -> 'a end) ->
628+
sig
629+
module Subst :
630+
sig
631+
module type S' = sig end
632+
module M'' : sig val foo : 'a -> 'a end
633+
module type S'' = sig end
634+
end
635+
module Eq :
636+
sig
637+
module type S' = sig module M : sig val foo : 'a -> 'a end end
638+
module M'' : sig val foo : 'a -> 'a end
639+
module type S'' = sig end
640+
end
641+
end
642+
|}]
643+
644+
(* strenghtening inclusion check looks at module modes, even inside a module
645+
type declaration. *)
646+
module type F = functor (M : sig val foo : 'a -> 'a end) -> sig
647+
module type S = sig val foo : 'a -> 'a @@ global many end with M
648+
end
649+
[%%expect{|
650+
module type F =
651+
functor (M : sig val foo : 'a -> 'a end) ->
652+
sig module type S = sig val foo : 'a -> 'a @@ global many end end
653+
|}]
654+
655+
656+
(* module type declaration inclusion check doesn't look at the enclosing
657+
structure's mode, because that mode is irrelevant. *)
658+
module M : sig
659+
module type S = sig val foo : 'a end
660+
end = struct
661+
module type S = sig val foo : 'a @@ global many end
662+
end
663+
[%%expect{|
664+
Lines 3-5, characters 6-3:
665+
3 | ......struct
666+
4 | module type S = sig val foo : 'a @@ global many end
667+
5 | end
668+
Error: Signature mismatch:
669+
Modules do not match:
670+
sig module type S = sig val foo : 'a @@ global many end end
671+
is not included in
672+
sig module type S = sig val foo : 'a end end
673+
Module type declarations do not match:
674+
module type S = sig val foo : 'a @@ global many end
675+
does not match
676+
module type S = sig val foo : 'a end
677+
The second module type is not included in the first
678+
At position "module type S = <here>"
679+
Module types do not match:
680+
sig val foo : 'a end
681+
is not equal to
682+
sig val foo : 'a @@ global many end
683+
At position "module type S = <here>"
684+
Values do not match:
685+
val foo : 'a
686+
is not included in
687+
val foo : 'a @@ global many
688+
The second is global_ and the first is not.
689+
|}]
690+
691+
(* Module declaration inclusion check inside a module type declaration inclusion
692+
check. There is no "enclosing module mode" to look at. *)
693+
module M : sig
694+
module type N = sig
695+
module M : sig val foo : 'a -> 'a end
696+
end
697+
end = struct
698+
module type N = sig
699+
module M : sig val foo : 'a -> 'a @@ global many end
700+
end
701+
end
702+
[%%expect{|
703+
Lines 5-9, characters 6-3:
704+
5 | ......struct
705+
6 | module type N = sig
706+
7 | module M : sig val foo : 'a -> 'a @@ global many end
707+
8 | end
708+
9 | end
709+
Error: Signature mismatch:
710+
Modules do not match:
711+
sig
712+
module type N =
713+
sig module M : sig val foo : 'a -> 'a @@ global many end end
714+
end
715+
is not included in
716+
sig
717+
module type N = sig module M : sig val foo : 'a -> 'a end end
718+
end
719+
Module type declarations do not match:
720+
module type N =
721+
sig module M : sig val foo : 'a -> 'a @@ global many end end
722+
does not match
723+
module type N = sig module M : sig val foo : 'a -> 'a end end
724+
The second module type is not included in the first
725+
At position "module type N = <here>"
726+
Module types do not match:
727+
sig module M : sig val foo : 'a -> 'a end end
728+
is not equal to
729+
sig module M : sig val foo : 'a -> 'a @@ global many end end
730+
At position "module type N = sig module M : <here> end"
731+
Modules do not match:
732+
sig val foo : 'a -> 'a end
733+
is not included in
734+
sig val foo : 'a -> 'a @@ global many end
735+
At position "module type N = sig module M : <here> end"
736+
Values do not match:
737+
val foo : 'a -> 'a
738+
is not included in
739+
val foo : 'a -> 'a @@ global many
740+
The second is global_ and the first is not.
741+
|}]
742+
743+
(* functor type inclusion: the following two functor types are equivalent,
744+
because a functor of the first type at any mode, can be zero-runtime casted
745+
to the second type at the same mode. Essentially, the parameter and return
746+
mode is in the functor type, and doesn't depend on the mode of the functor. *)
747+
module M : sig
748+
module type F = (sig val foo : 'a @@ global many end) ->
749+
(sig end)
750+
end = struct
751+
module type F = (sig val foo : 'a end) ->
752+
(sig end)
753+
end
754+
[%%expect{|
755+
module M :
756+
sig module type F = sig val foo : 'a @@ global many end -> sig end end
757+
|}]
758+
759+
module M : sig
760+
module type F =
761+
(sig end) -> (sig val foo : 'a end)
762+
end = struct
763+
module type F =
764+
(sig end) -> (sig val foo : 'a @@ global many end)
765+
end
766+
[%%expect{|
767+
module M : sig module type F = sig end -> sig val foo : 'a end end
768+
|}]
769+
468770
module type T = sig @@ portable
469771
val foo : 'a -> 'a
470772
val bar : 'a -> 'a @@ nonportable

‎toplevel/byte/topeval.ml

+2-1
Original file line numberDiff line numberDiff line change
@@ -125,7 +125,8 @@ let execute_phrase print_outcome ppf phr =
125125
in
126126
if !Clflags.dump_typedtree then Printtyped.implementation ppf str;
127127
let sg' = Typemod.Signature_names.simplify newenv sn sg in
128-
ignore (Includemod.signatures ~mark:Mark_positive oldenv sg sg');
128+
ignore (Includemod.signatures ~mark:Mark_positive oldenv
129+
~modes:Legacy sg sg');
129130
Typecore.force_delayed_checks ();
130131
let shape = Shape_reduce.local_reduce Env.empty shape in
131132
if !Clflags.dump_shape then Shape.print ppf shape;

‎toplevel/native/opttoploop.ml

+3-1
Original file line numberDiff line numberDiff line change
@@ -400,7 +400,9 @@ let execute_phrase print_outcome ppf phr =
400400
in
401401
if !Clflags.dump_typedtree then Printtyped.implementation ppf str;
402402
let sg' = Typemod.Signature_names.simplify newenv names sg in
403-
let coercion = Includemod.signatures oldenv ~mark:Mark_positive sg sg' in
403+
let coercion =
404+
Includemod.signatures oldenv ~mark:Mark_positive ~modes:Legacy sg sg'
405+
in
404406
Typecore.force_delayed_checks ();
405407
let str, sg', rewritten =
406408
match str.str_items with

0 commit comments

Comments
 (0)