Improve error reporting for ill-typed applicative functor type by v-gb · Pull Request #1491 · ocaml/ocaml

v-gb · 2017-11-24T01:31:38Z

Right now, type errors in applicative functor types are annoying to fix since they contain very little information. Here is an example of what I change:

type t = Set.Make(M).t
 [%%expect{|
 Line _, characters 9-22:
-Error: Ill-typed functor application Set.Make(M)
+Error: The type of M does not match Set.Make's parameter
+       Modules do not match:
+         sig type 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
 |} ]

The change introduces a dependency from typetexp.ml to includemod.ml, I am not sure if that's undesirable.

While I was there, I also fixed MPR#7611 and changed the wording of related error messages.

Drup

The change is very useful and looks correct to me (It simply doesn't throw away information that was already there).
Also, the patch only changes code that is used to investigate a type error, so it's fairly safe. The commits are weirdly organized and clearly not self-contained. I think you could just squash them.

Drup · 2017-11-26T13:17:28Z

Changes

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


That shouldn't be here.

I don't see why not. It's about the same as fixing a typo in a comment.

I agree with @sliquister .
I had already noticed the issue here but it's apparently not worth anyone's time to create a separate PR. So fixing it here sounds good.

Ah, I though it was a change that was included by mistake. Not sure why it's included in a commit that has literally nothing to do with it, but fair enough. :)

Drup · 2017-11-26T13:17:59Z

testsuite/tests/typing-modules/applicative_functor_type.ml

+type t = Generative(M).t
+[%%expect{|
+type t = Generative(M).t
+|}]


That probably shouldn't be a test, or at least not like that.

I think it makes sense, while writing tests for applicative functor application, to add related tests.
This test particularly test stays broken, but I don't see why that's an issue, as long as it's clearly indicated.

Drup · 2017-11-26T13:22:46Z

typing/typetexp.ml

+      | mty_arg ->
+         let details =
+           match mty_param_opt with
+           | None -> None


IIRC, this case only appears when the functor is generative and the argument should be (). So, current bug non-withstanding, we could also give a good error message here.

It's not the only case. What can happen, and would have no details, is this:

module F(X : sig module type S module F : S end) = struct type t = X.F(Parsing).t end

because we go through the _ -> None above, since the type of F is Mty_ident "X.S" or something.

Otherwise, yeah, we could reject functors that take (), anticipating a better behavior from the rest of the typer. In fact, fixing the typer sounds trivial.

We might be able to remove all the cases with no details.

v-gb · 2017-11-26T18:17:13Z

Thanks for reviewing. I don't know what you don't like about the commits. Clearly, I don't want the make depend stuff mixed in with the rest, as it has nothing to do with my pull request but I am forced to run it. Adding tests, then fixing them is a standard way of showing the change of behavior in the diff.

In any case, I also fixed error reporting involving abstract signatures, as well as fixed MPR#7611 by rejecting F(M).t where F is generative. So technically, this feature doesn't only change the reporting of type errors, but the change to the typer proper is very simple (and it's extremely unlikely to break existing code).

Though now, the pull request could use some squashing, though I'll wait until it's accepted because it's much harder to split changes than to squash them.

trefis · 2017-11-27T01:58:11Z

Thanks for reviewing. I don't know what you don't like about the commits. Clearly, I don't want the make depend stuff mixed in with the rest, as it has nothing to do with my pull request but I am forced to run it. Adding tests, then fixing them is a standard way of showing the change of behavior in the diff.

I see changes to .depend in two commits, one clearly identified (the first commit, called "make depend") and another one in "Improve error reporting for ill-typed ap...".
The second one seems to be because, as you said, you had a dependency from typetexp to includemod.
Are you saying that the first "make depend" commit is unrelated to your PR and is due to people forgetting to run it in the past?

Also, I think Drup is confused because github's interface is bad and orders commits by date and not by dependency.

v-gb · 2017-11-27T02:34:18Z

Are you saying that the first "make depend" commit is unrelated to your PR and is due to people forgetting to run it in the past?

Yes. It fact, while trying to see if I could write a CI check to reject changes that don't update .depend files, I learnt that there is such a thing as make alldepend that updates other .depend files like the ones in otherlibs, and it's even more out of date.

trefis · 2017-11-27T02:56:31Z

trying to see if I could write a CI check to reject changes that don't update .depend files

That'd be lovely.

Drup · 2017-12-02T12:57:15Z

typing/typetexp.ml

+  | Use_generative_functor_as_applicative flid ->
+     fprintf ppf "@[%a is a generative functor,@ and@ so@ cannot@ be@ applied@ \
+                    in@ type@ expressions@]"
+       longident flid


That error message sounds wrong. Shouldn't be it _ is a generative functor but was applied to _. It should be applied to () ?

Drup · 2017-12-02T13:08:47Z

If people find the commit log fine, who am I to complain ? :p

The new commits look ok, but I don't find the error messages very good. I think the code factorization you did at the end does more harm than good: You should just follow the exact same wording than is used for functions: "This module has type _. It is not a functor, it cannot be applied". Also, something more explicit for generative functors that says it should be applied to () (most people don't know what generative and applicative functors are). I'll let error messages experts give their opinion (@Octachron, @gasche ? :)

Octachron

I like the changes, and I think that the improved error messages would be very useful to a large spectrum of users. However, I think it may be possible to do better by making the error messages less dry. I made few remarks in this direction.

Octachron · 2017-12-02T13:29:43Z

typing/typetexp.ml

-  | Ill_typed_functor_application lid ->
-      fprintf ppf "Ill-typed functor application %a" longident lid
+  | Ill_typed_functor_application (lid, details) ->
+     fprintf ppf "@[Ill-typed functor application %a%t@]"


I find this error message too unprecise. For instance, in

Ill-typed functor application F(M)
Module types do not match
$1
is not included in
$2

I fear that it is not clear for an unattentive reader that $1 is the module type of M and $2is the expected type of the first argument of F . I would rather use a far less generic error message:

Ill-typed functor application F(M)
The functor F cannot be applied to M (* maybe redundant ?*)
The actual module type of the argument
$1
is not included in its expected module type
$2

Yeah, the message sucks a bit for the reason you say, but at the same time, but I would expect people to understand what's wrong from $1 and $2 regardless.
I am not fond of overly verbose messages.

My message:

File "a.ml", line 2, characters 16-29: Error: Ill-typed functor application Map.Make(M) Modules do not match: sig end is not included in Map.OrderedType The value `compare' is required but not provided File "map.mli", line 51, characters 4-31: Expected declaration The type `t' is required but not provided File "map.mli", line 48, characters 4-10: Expected declaration

The same message at the module level:

File "a.ml", line 2, characters 22-23: Error: Signature mismatch: Modules do not match: sig end is not included in Map.OrderedType The value `compare' is required but not provided File "map.mli", line 51, characters 4-31: Expected declaration The type `t' is required but not provided File "map.mli", line 48, characters 4-10: Expected declaration

It's not any better and no one seems to be unhappy about it. Well the position is more narrow, I suppose.

It's not any better and no one seems to be unhappy about it.

People may not hate these error messages enough to make a PR, but I have heard complaints about the fact that it is not clear which module is the interface and which one is the implementation.

I am not fond of overly verbose messages.

It is certainly better to strike a balance between clarity and verbosity. In this case, maybe a shorter version would be better

File "a.ml", line 2, characters 16-29: Error: Ill-typed functor application Map.Make(M) The argument module type sig end is not included in Map.OrderedType The value `compare' is required but not provided File "map.mli", line 51, characters 4-31: Expected declaration The type `t' is required but not provided File "map.mli", line 48, characters 4-10: Expected declaration

This gives us the same number of words, and only 8 more letters.

Notwithstanding my nitpickings, I agree than the current message is no worse than the existing inclusion errror message.

I certainly agree with the complaint that it's unclear which module type is which.
In any case, I did change the message and I think it should mostly address your concern. I think the scope of this pull request has grown enough, I'd rather avoid doing any more.

The reworded error message is nice. Thank you for humoring my nitpickings!

Octachron · 2017-12-02T14:04:42Z

typing/typetexp.ml

+       | `Generative_used_as_applicative ->
+          "a generative functor", "an applicative functor"
+     in
+     fprintf ppf "@[The module %a is %s,@ not %s@]" longident lid is but_used_as


I share the opinion of @Drup, these error messages might end un being unscrutable for people not familiar with the module system since they ends un just classifying the type of the error rather than detailing the issue at hand.

I would replace

The module M is a structure, not a functor
The module M is abstract, not a functor
The module M is a functor, not a structure
The module M is abstract, not a structure
The module M is a generative functor, not an applicative functor

by

The module M cannot be applied, it is a structure not a functor
The abstract module M cannot be applied
As a functor, the module M does not have any components that can be accessed
As an abstract module, the module M does not have any components that can be accessed
The generative functor M can only be applied to ( )

v-gb · 2017-12-03T19:10:03Z

I changed a few error messages, maybe it's slighty better now.
I didn't change the error about generative functor to what you were both suggesting though, because my message is correct: in Generative(M).t, the error shouldn't say "you need to write Generative().t", because that makes no sense and in fact doesn't even parse.

gasche · 2017-12-13T00:35:12Z

@Octachron, do you approve the change?

(There now are conflicts that need to be fixed in any case.)

Octachron

I approve this helpful change, the code looks good and the error message are nice (and translatable).

Octachron · 2017-12-13T10:51:14Z

typing/typetexp.mli

  | 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


I have a small question here: is there a meaningful difference between Some [] and None for the include error detail?

I think neither is possible, so well, it's hard to say what counts as different.

Drup

I also quite like the new error messages, lgtm. :)

gasche · 2017-12-13T14:36:26Z

Before we merge, could you use a *-bullet for the changes entry for f03aaad, which is unrelated to error messages themselves and may break some (dubious but existing) code? You might want to write a couple extra line to show the example of codes that were previously accepted and are now rejected, so that users have an idea what to look for.

gasche · 2017-12-13T14:44:42Z

Thinking about this again, I am uncomfortable with the mixing of separate concerns in this PR. @sliquister, could you please remove f03aaad before we merge, and submit it as a separate PR to be reviewed separately?

(I think that there is a mild risk that this change would reject more programs than expected, whereas change to the error-message machinery are less risky.)

@Octachron, @Drup, have you reviewed this one commit carefully, and do you vouch for its correctness?

trefis · 2017-12-13T15:08:10Z

@gasche I find your last message confusing. What is it that you are worried about?
When you say:

there is a mild risk that we would reject more programs than expected

what does "expected" mean?

Do you mean:

"there might be more programs than we thought that are using this feature"

or:

"the commit might contain a bug causing us to reject other programs than the ones using generative functors as applicatives constructors in type paths"

?

If it's the first option, then asking if the commit was reviewed carefully doesn't make much sense (well, I guess I just answered my own question right there). But I also think that we shouldn't be worried about the number of people using this "bug".
Everyone seems to agree it is a bug, let's just fix it.

If it's the second option, I have just reread the commit you pointed out and it looks correct to me.
(Some parts of typetexp looked a bit meh, but they have been cleaned up in later commits, so I'm happy with it)

gasche · 2017-12-13T15:11:59Z

Yes, I meant the second point.

Octachron · 2017-12-13T18:49:47Z

@gasche , I vouch for the correctness of this commit: generative functor application should only happen inside module expression, and the parser takes care to not extend generative application (F()) to type expression (or module types or class types). For instance,

module module G() = struct type t end;;
type t = G().t;;

raises a syntax error.

This commit f03aaad merely closes the hole that was left open by this syntactic restriction on generative application by making sure that a lookup for the result of a generative function in the current environment never successes.

In fact, I would argue that with this commit, we are in the paradoxical situation that the rare conjunction of two mistakes (applying a generative functor inside a type expression/module type/class type expression and applying it to the wrong kind of argument) yields a better error message than the one for the root error.

gasche · 2017-12-13T19:07:33Z

Ok, it seems there is consensus that keeping the commit in the present PR is fine. (I still don't like this mixing of concerns in a single PR.)

v-gb · 2017-12-14T03:46:17Z

Alright, thanks everyone!

Drup reviewed Nov 26, 2017

View reviewed changes

Drup reviewed Dec 2, 2017

View reviewed changes

Octachron reviewed Dec 2, 2017

View reviewed changes

v-gb force-pushed the ill-typed-functor branch 3 times, most recently from 2309ec1 to 747fe8c Compare December 3, 2017 19:05

v-gb added 6 commits December 12, 2017 23:51

add tests of error messages of applicative functor types

e172c39

share code that checks that the functor application F(M) is well-typed

c5722f1

Improve error reporting for ill-typed applicative functor type, F(M).t

a9aef56

try to clarify what the subtyping error is about

2c67a57

reject the use of generative functors as applicative (MPR#7611)

f03aaad

report nice errors for applicative functors in all cases

cf2dd9b

v-gb force-pushed the ill-typed-functor branch from 747fe8c to cf2dd9b Compare December 13, 2017 05:03

Octachron approved these changes Dec 13, 2017

View reviewed changes

Drup approved these changes Dec 13, 2017

View reviewed changes

v-gb mentioned this pull request Dec 13, 2017

Migrate expect tests to ocamltest #1519

Merged

gasche merged commit 4b30d29 into ocaml:trunk Dec 13, 2017

v-gb deleted the ill-typed-functor branch December 14, 2017 02:32

vicuna mentioned this pull request Mar 14, 2019

Generative functors are allowed to be applicative ! #7611

Closed

EmileTrotignon pushed a commit to EmileTrotignon/ocaml that referenced this pull request Jan 12, 2024

Add rounded corners to Learn OCaml cards (ocaml#1491)

9752ec7

Conversation

v-gb commented Nov 24, 2017 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Drup left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

v-gb commented Nov 26, 2017

Uh oh!

trefis commented Nov 27, 2017

Uh oh!

v-gb commented Nov 27, 2017

Uh oh!

trefis commented Nov 27, 2017

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Drup commented Dec 2, 2017

Uh oh!

Octachron left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

v-gb commented Dec 3, 2017

Uh oh!

gasche commented Dec 13, 2017

Uh oh!

Octachron left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Drup left a comment

Choose a reason for hiding this comment

Uh oh!

gasche commented Dec 13, 2017

Uh oh!

gasche commented Dec 13, 2017

Uh oh!

trefis commented Dec 13, 2017 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

gasche commented Dec 13, 2017

Uh oh!

Octachron commented Dec 13, 2017

Uh oh!

gasche commented Dec 13, 2017

Uh oh!

v-gb commented Dec 14, 2017

Uh oh!

Reviewers

v-gb commented Nov 24, 2017 •

edited

Loading

trefis commented Dec 13, 2017 •

edited

Loading