Skip to content

Commit

Permalink
Merge pull request #1491 from sliquister/ill-typed-functor
Browse files Browse the repository at this point in the history
Improve error reporting for ill-typed applicative functor type
  • Loading branch information
gasche committed Dec 13, 2017
2 parents b41a4c3 + cf2dd9b commit 4b30d29
Show file tree
Hide file tree
Showing 11 changed files with 195 additions and 53 deletions.
16 changes: 9 additions & 7 deletions .depend
Original file line number Diff line number Diff line change
Expand Up @@ -475,18 +475,20 @@ typing/types.cmi : typing/primitive.cmi typing/path.cmi \
typing/typetexp.cmo : typing/types.cmi typing/typedtree.cmi utils/tbl.cmi \
typing/printtyp.cmi typing/predef.cmi typing/path.cmi \
parsing/parsetree.cmi utils/misc.cmi parsing/longident.cmi \
parsing/location.cmi typing/env.cmi typing/ctype.cmi utils/clflags.cmi \
parsing/builtin_attributes.cmi typing/btype.cmi parsing/asttypes.cmi \
parsing/ast_helper.cmi typing/typetexp.cmi
parsing/location.cmi typing/includemod.cmi typing/env.cmi \
typing/ctype.cmi utils/clflags.cmi parsing/builtin_attributes.cmi \
typing/btype.cmi parsing/asttypes.cmi parsing/ast_helper.cmi \
typing/typetexp.cmi
typing/typetexp.cmx : typing/types.cmx typing/typedtree.cmx utils/tbl.cmx \
typing/printtyp.cmx typing/predef.cmx typing/path.cmx \
parsing/parsetree.cmi utils/misc.cmx parsing/longident.cmx \
parsing/location.cmx typing/env.cmx typing/ctype.cmx utils/clflags.cmx \
parsing/builtin_attributes.cmx typing/btype.cmx parsing/asttypes.cmi \
parsing/ast_helper.cmx typing/typetexp.cmi
parsing/location.cmx typing/includemod.cmx typing/env.cmx \
typing/ctype.cmx utils/clflags.cmx parsing/builtin_attributes.cmx \
typing/btype.cmx parsing/asttypes.cmi parsing/ast_helper.cmx \
typing/typetexp.cmi
typing/typetexp.cmi : typing/types.cmi typing/typedtree.cmi typing/path.cmi \
parsing/parsetree.cmi parsing/longident.cmi parsing/location.cmi \
typing/env.cmi parsing/asttypes.cmi
typing/includemod.cmi typing/env.cmi parsing/asttypes.cmi
typing/untypeast.cmo : typing/typedtree.cmi typing/path.cmi \
parsing/parsetree.cmi utils/misc.cmi parsing/longident.cmi \
parsing/location.cmi typing/ident.cmi typing/env.cmi parsing/asttypes.cmi \
Expand Down
13 changes: 10 additions & 3 deletions Changes
Original file line number Diff line number Diff line change
Expand Up @@ -12,9 +12,8 @@ Working version

### Type system:

- GPR#1370: Fix code duplication in Cmmgen
(Vincent Laviron, with help from Pierre Chambart,
reviews by Gabriel Scherer and Luc Maranget)
- MPR#7611, GPR#1491: reject the use of generative functors as applicative
(Valentin Gatien-Baron)

- GPR#1469: Use the information from [@@immediate] annotations when
computing whether a type can be [@@unboxed]
Expand Down Expand Up @@ -49,6 +48,10 @@ Working version
(Arthur Charguéraud and Armaël Guéneau, with help from Gabriel Scherer and
Frédéric Bour)

- GPR#1491: Improve error reporting for ill-typed applicative functor
types, F(M).t.
(Valentin Gatien-Baron, review by Florian Angeletti and Gabriel Radanne)

- GPR#1496: Refactor the code printing explanation for unification type errors,
in order to avoid duplicating pattern matches
(Armaël Guéneau, review by Florian Angeletti and Gabriel Scherer)
Expand All @@ -60,6 +63,10 @@ Working version

### Code generation and optimizations:

- GPR#1370: Fix code duplication in Cmmgen
(Vincent Laviron, with help from Pierre Chambart,
reviews by Gabriel Scherer and Luc Maranget)

### Runtime system:

- GPR#1431: remove ocamlrun dependencies on curses/terminfo/termcap C library
Expand Down
2 changes: 1 addition & 1 deletion testsuite/tests/typing-modules/Test.ml
Original file line number Diff line number Diff line change
Expand Up @@ -119,5 +119,5 @@ module F : functor (X : sig end) -> sig val x : int end
Line _, characters 0-3:
F.x;; (* fail *)
^^^
Error: The module F is a functor, not a structure
Error: The module F is a functor, it cannot have any components
|}];;
83 changes: 83 additions & 0 deletions testsuite/tests/typing-modules/applicative_functor_type.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,83 @@
(* TEST
* expect
*)

type t = Set.Make(String).t
[%%expect{|
type t = Set.Make(String).t
|} ]


(* Check the error messages of an ill-typed applicatived functor type. *)
module M = struct type t let equal = (=) end
[%%expect{|
module M : sig type t val equal : 'a -> 'a -> bool end
|} ]

type t = Set.Make(M).t
[%%expect{|
Line _, characters 9-22:
type t = Set.Make(M).t
^^^^^^^^^^^^^
Error: The type of M does not match Set.Make's parameter
Modules do not match:
sig type t = M.t val equal : 'a -> 'a -> bool end
is not included in
Set.OrderedType
The value `compare' is required but not provided
File "set.mli", line 52, characters 4-31: Expected declaration
|} ]


(* We would report the wrong error here if we didn't strengthen the
type of the argument (type t wouldn't match). *)
module F(X : sig type t = M.t val equal : unit end)
= struct type t end
[%%expect{|
module F :
functor (X : sig type t = M.t val equal : unit end) -> sig type t end
|} ]

type t = F(M).t
[%%expect{|
Line _, characters 9-15:
type t = F(M).t
^^^^^^
Error: The type of M does not match F's parameter
Modules do not match:
sig type t = M.t val equal : 'a -> 'a -> bool end
is not included in
sig type t = M.t val equal : unit end
Values do not match:
val equal : 'a -> 'a -> bool
is not included in
val equal : unit
|} ]


(* MPR#7611 *)
module Generative() = struct type t end
[%%expect{|
module Generative : functor () -> sig type t end
|}]

type t = Generative(M).t
[%%expect{|
Line _, characters 9-24:
type t = Generative(M).t
^^^^^^^^^^^^^^^
Error: The functor Generative is generative, it cannot be applied in type
expressions
|}]



module F(X : sig module type S module F : S end) = struct
type t = X.F(Parsing).t
end
[%%expect{|
Line _, characters 11-25:
type t = X.F(Parsing).t
^^^^^^^^^^^^^^
Error: The module X.F is abstract, it cannot be applied
|}]
1 change: 1 addition & 0 deletions testsuite/tests/typing-modules/ocamltests
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
aliases.ml
applicative_functor_type.ml
firstclass.ml
generative.ml
pr5911.ml
Expand Down
8 changes: 6 additions & 2 deletions typing/env.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1136,7 +1136,9 @@ let rec lookup_module_descr_aux ?loc ~mark lid env =
begin match get_components desc1 with
Functor_comps f ->
let loc = match loc with Some l -> l | None -> Location.none in
Misc.may (!check_modtype_inclusion ~loc env mty2 p2) f.fcomp_arg;
(match f.fcomp_arg with
| None -> raise Not_found (* PR#7611 *)
| Some arg -> !check_modtype_inclusion ~loc env mty2 p2 arg);
(Papply(p1, p2), !components_of_functor_appl' f env p1 p2)
| Structure_comps _ ->
raise Not_found
Expand Down Expand Up @@ -1204,7 +1206,9 @@ and lookup_module ~load ?loc ~mark lid env : Path.t =
begin match get_components desc1 with
Functor_comps f ->
let loc = match loc with Some l -> l | None -> Location.none in
Misc.may (!check_modtype_inclusion ~loc env mty2 p2) f.fcomp_arg;
(match f.fcomp_arg with
| None -> raise Not_found (* PR#7611 *)
| Some arg -> (!check_modtype_inclusion ~loc env mty2 p2) arg);
p
| Structure_comps _ ->
raise Not_found
Expand Down
14 changes: 7 additions & 7 deletions typing/includemod.ml
Original file line number Diff line number Diff line change
Expand Up @@ -482,14 +482,14 @@ let can_alias env path =
no_apply path && not (Env.is_functor_arg path env)

let check_modtype_inclusion ~loc env mty1 path1 mty2 =
try
let aliasable = can_alias env path1 in
ignore(modtypes ~loc env [] Subst.identity
(Mtype.strengthen ~aliasable env mty1 path1) mty2)
with Error _ ->
raise Not_found
let aliasable = can_alias env path1 in
ignore(modtypes ~loc env [] Subst.identity
(Mtype.strengthen ~aliasable env mty1 path1) mty2)

let _ = Env.check_modtype_inclusion := check_modtype_inclusion
let () =
Env.check_modtype_inclusion := (fun ~loc a b c d ->
try (check_modtype_inclusion ~loc a b c d : unit)
with Error _ -> raise Not_found)

(* Check that an implementation of a compilation unit meets its
interface. *)
Expand Down
6 changes: 6 additions & 0 deletions typing/includemod.mli
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,12 @@ val modtypes:
loc:Location.t -> Env.t ->
module_type -> module_type -> module_coercion

val check_modtype_inclusion :
loc:Location.t -> Env.t -> Types.module_type -> Path.t -> Types.module_type -> unit
(** [check_modtype_inclusion ~loc env mty1 path1 mty2] checks that the
functor application F(M) is well typed, where mty2 is the type of
the argument of F and path1/mty1 is the path/unstrenghened type of M. *)

val signatures: Env.t -> signature -> signature -> module_coercion

val compunit:
Expand Down
4 changes: 1 addition & 3 deletions typing/typemod.ml
Original file line number Diff line number Diff line change
Expand Up @@ -214,9 +214,7 @@ let retype_applicative_functor_type ~loc env funct arg =
| Mty_functor (_, Some mty_param, _) -> mty_param
| _ -> assert false (* could trigger due to MPR#7611 *)
in
let aliasable = not (Env.is_functor_arg arg env) in
ignore(Includemod.modtypes ~loc env
(Mtype.strengthen ~aliasable env mty_arg arg) mty_param)
Includemod.check_modtype_inclusion ~loc env mty_arg arg mty_param

(* When doing a deep destructive substitution with type M.N.t := .., we change M
and M.N and so we have to check that uses of the modules other than just
Expand Down
90 changes: 63 additions & 27 deletions typing/typetexp.ml
Original file line number Diff line number Diff line change
Expand Up @@ -52,10 +52,15 @@ type error =
| Unbound_class of Longident.t
| Unbound_modtype of Longident.t
| Unbound_cltype of Longident.t
| Ill_typed_functor_application of Longident.t
| Ill_typed_functor_application
of Longident.t * Longident.t * Includemod.error list option
| Illegal_reference_to_recursive_module
| Access_functor_as_structure of Longident.t
| Apply_structure_as_functor of Longident.t
| Wrong_use_of_module of Longident.t * [ `Structure_used_as_functor
| `Abstract_used_as_functor
| `Functor_used_as_structure
| `Abstract_used_as_structure
| `Generative_used_as_applicative
]
| Cannot_scrape_alias of Longident.t * Path.t
| Opened_object of Path.t option
| Not_an_object of type_expr
Expand All @@ -81,38 +86,50 @@ let rec narrow_unbound_lid_error : 'a. _ -> _ -> _ -> _ -> 'a =
| Env.Recmodule ->
raise (Error (loc, env, Illegal_reference_to_recursive_module))
in
let error e = raise (Error (loc, env, e)) in
begin match lid with
| Longident.Lident _ -> ()
| Longident.Ldot (mlid, _) ->
check_module mlid;
let md = Env.find_module (Env.lookup_module ~load:true mlid env) env in
begin match Env.scrape_alias env md.md_type with
| Mty_functor _ ->
raise (Error (loc, env, Access_functor_as_structure mlid))
| Mty_alias(_, p) ->
raise (Error (loc, env, Cannot_scrape_alias(mlid, p)))
| _ -> ()
error (Wrong_use_of_module (mlid, `Functor_used_as_structure))
| Mty_ident _ ->
error (Wrong_use_of_module (mlid, `Abstract_used_as_structure))
| Mty_alias(_, p) -> error (Cannot_scrape_alias(mlid, p))
| Mty_signature _ -> ()
end
| Longident.Lapply (flid, mlid) ->
check_module flid;
let fmd = Env.find_module (Env.lookup_module ~load:true flid env) env in
begin match Env.scrape_alias env fmd.md_type with
| Mty_signature _ ->
raise (Error (loc, env, Apply_structure_as_functor flid))
| Mty_alias(_, p) ->
raise (Error (loc, env, Cannot_scrape_alias(flid, p)))
| _ -> ()
end;
let mty_param =
match Env.scrape_alias env fmd.md_type with
| Mty_signature _ ->
error (Wrong_use_of_module (flid, `Structure_used_as_functor))
| Mty_ident _ ->
error (Wrong_use_of_module (flid, `Abstract_used_as_functor))
| Mty_alias(_, p) -> error (Cannot_scrape_alias(flid, p))
| Mty_functor (_, None, _) ->
error (Wrong_use_of_module (flid, `Generative_used_as_applicative))
| Mty_functor (_, Some mty_param, _) -> mty_param
in
check_module mlid;
let mmd = Env.find_module (Env.lookup_module ~load:true mlid env) env in
let mpath = Env.lookup_module ~load:true mlid env in
let mmd = Env.find_module mpath env in
begin match Env.scrape_alias env mmd.md_type with
| Mty_alias(_, p) ->
raise (Error (loc, env, Cannot_scrape_alias(mlid, p)))
| _ ->
raise (Error (loc, env, Ill_typed_functor_application lid))
| Mty_alias(_, p) -> error (Cannot_scrape_alias(mlid, p))
| mty_arg ->
let details =
try Includemod.check_modtype_inclusion
~loc env mty_arg mpath mty_param;
None (* should be impossible *)
with Includemod.Error e -> Some e
in
error (Ill_typed_functor_application (flid, mlid, details))
end
end;
raise (Error (loc, env, make_error lid))
error (make_error lid)

let find_component (lookup : ?loc:_ -> ?mark:_ -> _) make_error env loc lid =
try
Expand Down Expand Up @@ -953,14 +970,33 @@ let report_error env ppf = function
| Unbound_cltype lid ->
fprintf ppf "Unbound class type %a" longident lid;
spellcheck ppf fold_cltypes env lid;
| Ill_typed_functor_application lid ->
fprintf ppf "Ill-typed functor application %a" longident lid
| Ill_typed_functor_application (flid, mlid, details) ->
(match details with
| None ->
fprintf ppf "@[Ill-typed functor application %a(%a)@]"
longident flid longident mlid
| Some inclusion_error ->
fprintf ppf "@[The type of %a does not match %a's parameter@\n%a@]"
longident mlid longident flid Includemod.report_error inclusion_error)
| Illegal_reference_to_recursive_module ->
fprintf ppf "Illegal recursive module reference"
| Access_functor_as_structure lid ->
fprintf ppf "The module %a is a functor, not a structure" longident lid
| Apply_structure_as_functor lid ->
fprintf ppf "The module %a is a structure, not a functor" longident lid
fprintf ppf "Illegal recursive module reference"
| Wrong_use_of_module (lid, details) ->
(match details with
| `Structure_used_as_functor ->
fprintf ppf "@[The module %a is a structure, it cannot be applied@]"
longident lid
| `Abstract_used_as_functor ->
fprintf ppf "@[The module %a is abstract, it cannot be applied@]"
longident lid
| `Functor_used_as_structure ->
fprintf ppf "@[The module %a is a functor, \
it cannot have any components@]" longident lid
| `Abstract_used_as_structure ->
fprintf ppf "@[The module %a is abstract, \
it cannot have any components@]" longident lid
| `Generative_used_as_applicative ->
fprintf ppf "@[The functor %a is generative,@ it@ cannot@ be@ \
applied@ in@ type@ expressions@]" longident lid)
| Cannot_scrape_alias(lid, p) ->
fprintf ppf
"The module %a is an alias for module %a, which is missing"
Expand Down
11 changes: 8 additions & 3 deletions typing/typetexp.mli
Original file line number Diff line number Diff line change
Expand Up @@ -64,10 +64,15 @@ type error =
| Unbound_class of Longident.t
| Unbound_modtype of Longident.t
| Unbound_cltype of Longident.t
| Ill_typed_functor_application of Longident.t
| Ill_typed_functor_application
of Longident.t * Longident.t * Includemod.error list option
| Illegal_reference_to_recursive_module
| Access_functor_as_structure of Longident.t
| Apply_structure_as_functor of Longident.t
| Wrong_use_of_module of Longident.t * [ `Structure_used_as_functor
| `Abstract_used_as_functor
| `Functor_used_as_structure
| `Abstract_used_as_structure
| `Generative_used_as_applicative
]
| Cannot_scrape_alias of Longident.t * Path.t
| Opened_object of Path.t option
| Not_an_object of type_expr
Expand Down

0 comments on commit 4b30d29

Please sign in to comment.