Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007467OCamltypingpublic2017-01-25 17:582017-04-14 17:05
Reporterbrendanlong 
Assigned To 
PrioritynormalSeverityfeatureReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product Version4.02.3 
Target VersionFixed in Version 
Summary0007467: Treat .mli type constraints the same as if they were signatures in the .ml
DescriptionIt'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 ReproduceCompile 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
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0017193)
lpw25 (developer)
2017-01-25 18:30

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.
(0017194)
brendanlong (reporter)
2017-01-25 18:52

Hm I didn't realize we could do that. It does seem like it would make this hard :\
(0017195)
frisch (developer)
2017-01-26 09:00

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 (https://github.com/ocaml/ocaml/pull/102 [^]).

- Issue History
Date Modified Username Field Change
2017-01-25 17:58 brendanlong New Issue
2017-01-25 18:30 lpw25 Note Added: 0017193
2017-01-25 18:52 brendanlong Note Added: 0017194
2017-01-26 09:00 frisch Note Added: 0017195
2017-02-23 16:45 doligez Category OCaml typing => typing
2017-04-14 17:05 doligez Status new => acknowledged


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker