Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Treat .mli type constraints the same as if they were signatures in the .ml #7467

Closed
vicuna opened this issue Jan 25, 2017 · 5 comments
Closed

Comments

@vicuna
Copy link

vicuna commented Jan 25, 2017

Original bug ID: 7467
Reporter: brendanlong
Status: acknowledged (set by @damiendoligez on 2017-04-14T15:05:15Z)
Resolution: open
Priority: normal
Severity: feature
Version: 4.02.3
Category: typing
Monitored by: @gasche

Bug description

It's frequently helpful to put types in the signature of a function so the compiler can give helpful warnings, but the correct style for this is to put them in the .mli instead. The problem is that the .mli signatures are treated differently than .ml signatures:

  • If the signature is in the .ml, the compiler assumes the signature is correct and reports errors if a statement in the function has the wrong type based on that assumption
  • If the signature is in the .mli, the compiler assumes the types in the function are correct and then compares them with the .mli.

I think the .ml behavior is usually more helpful.

Steps to reproduce

Compile this program with a trivial bug:

(** unhelpful-error.ml *)
let add x y =
  x + y

(** unhelpful-error.mli *)
val add: float -> float -> float

The error message is:

Error: The implementation unhelpful-error.ml
does not match the interface unhelpful-error.cmi:
Values do not match:
val add : int -> int -> int
is not included in
val add : float -> float -> float
File "unhelpful-error.ml", line 1, characters 4-7: Actual declaration

This tells me that something is wrong with my types, but doesn't really help me figure out what it is.

Compare that to this (with no .mli):

(** helpful-error.ml *)
let add (x:float) (y:float): float =
  x + y

With the error:

File "helpful-error.ml", line 3, characters 2-3:
Error: This expression has type float but an expression was expected of type
int

Obviously in this function it's not a whole lot more helpful, but:

  • In a big function, it will tell me which line is actually wrong
  • With a merlin-supporting editor, it will highlight that line
  • This is especially helpful with multiple functions interacting
@vicuna
Copy link
Author

vicuna commented Jan 25, 2017

Comment author: @lpw25

This is probably not possible in general because you cannot tell that the add in the ml will be the same as the one in the mli. Consider, for example:

let add x y = x + y

include Module_containing_another_add_definition

Here we cannot tell that the add is actually going to be overridden by the later include statement.

@vicuna
Copy link
Author

vicuna commented Jan 25, 2017

Comment author: brendanlong

Hm I didn't realize we could do that. It does seem like it would make this hard :\

@vicuna
Copy link
Author

vicuna commented Jan 26, 2017

Comment author: @alainfrisch

In addition to shadowing, applying the constraints from the signature before type-checking the value would restrict its polymorphism. This would reject the currently valid:

.ml:
let id x = x
let s = id "hello"

.mli:
val id: int -> int
val s: string

Now, a possible direction could be to react on the type error that signals type mismatch and try to type-check again the corresponding value definition using the type declared in the signature. This could be an idea for the "Improved error messages" project (#102).

@github-actions
Copy link

github-actions bot commented May 9, 2020

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

@github-actions github-actions bot added the Stale label May 9, 2020
@garrigue
Copy link
Contributor

garrigue commented May 9, 2020

This is an old idea, but we have not found a good solution.
I'm sure we can keep it in mind even if we close this issue.

@garrigue garrigue closed this as completed May 9, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants