Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007742OCamllexing and parsingpublic2018-02-22 11:322018-02-22 18:29
Reporterkantian 
Assigned Togasche 
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionno change required 
PlatformOSOS Version
Product Version4.05.0 
Target VersionFixed in Version 
Summary0007742: Local open can raise type error (as expected) or warning or even no problem (as unexpected) depending on how it is used.
DescriptionCode is better than a long discourse:
Steps To Reproducemodule M = struct type t = {x:int} let id x = x end
module N = struct type t = {x:int} let id x = x end

(* type error as expected *)
{M.x = 1} = {N.x = 1};;
Error: The field N.x belongs to the record type N.t
       but a field was expected belonging to the record type M.t

(*
  Only warning if the module name is put outside the record construct.
  The field `x' in the second expression is interpreted as M.x and not N.x,
  hence the two values are equal.
*)
M.{x = 1} = N.{x = 1};;
Characters 12-21:
Warning 40: this record of type M.t contains fields that are
not visible in the current scope: x.
They will not be selected if the type becomes unknown.
- : bool = true

(* same as before but with local open: its worse since there is no warning *)
let open M in {x = 1} = let open N in {x = 1};;
- : bool = true

(* but there is no problem if we add a function application *)
M.(id {x = 1}) = N.(id {x = 1});;
Error: This expression has type t but an expression was expected of type M.t


let open M in id {x = 1} = let open N in id {x = 1};;
Error: This expression has type N.t but an expression was expected of type M.t

(* and no problem if we let bind the constructions before comparaison *)
let i = M.{x = 1} in
let j = N.{x = 1} in
i = j;;
Error: This expression has type N.t but an expression was expected of type M.t

(* it works as expected in pattern matching *)
function M.{x = 1}, N.{x = 1} -> () | _ -> ();;
- : M.t * N.t -> unit = <fun>
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0018905)
octachron (developer)
2018-02-22 11:48

Would be so kind to precise which issue(s) do you see with your code samples?

Your second example is an illustration of the left-to-right bias of the typechecker: the first argument of `(=) M.{…} N.{…}` is typed first, then the second x field is disambiguated using the information that the type of the record is `M.t` (and -principal will warn that this type based record-disambiguation is not principal).

Your third example can be rewritten as M.( (=) {…} N.{…} ) and indeed this time the field M.x is in scope when disambiguating N.{…}, so there is no reason to emit the warning 40 .
(0018906)
gasche (developer)
2018-02-22 11:54

Indeed, I think that in these examples the language is in fact behaving as specified.
(0018907)
lpw25 (developer)
2018-02-22 11:54

Yeah, I think all of these behaviors are correct, and I would suggest using the `-principal` option to get the more sensible behavior that you're after.

The third one does look confusing, but really its just an issue with the precedence of `=` vs `let`.
(0018908)
kantian (reporter)
2018-02-22 12:08

Ok, your explications are clear. But it's still confused me a little bit...
(0018909)
kantian (reporter)
2018-02-22 17:59

Just a little note to precise that the answer to my confusion is 42 :-D

I do not really understand when warning 18 is triggered. With this slight variation on example 3:

M.(let f = (=) {x=1} in f N.{x=1});;

Warning 18 (this type-based record disambiguation is not principal) is not triggerd but Warning 42 (this use of x relies on type-directed disambiguation,
it will not compile with OCaml 4.00 or earlier.) is.
(0018910)
lpw25 (developer)
2018-02-22 18:05
edited on: 2018-02-22 18:05

Basically, something isn't principal if it depends on arbitrary details of the inference algorithm. For instance, the order that different sides of `=` are considered, as in your original example 3. In your new example it only depends on that the definition of a `let` is considered before its body -- this is not considered an arbitrary detail of the algorithm but a reliable part of the type system's declarative specification.

(0018911)
kantian (reporter)
2018-02-22 18:29

Thanks, that makes sense.

By the way, this type directed disambiguation reminds me this problem[1] with merging in git.

[1]: https://jneem.github.io/merging/ [^]

- Issue History
Date Modified Username Field Change
2018-02-22 11:32 kantian New Issue
2018-02-22 11:48 octachron Note Added: 0018905
2018-02-22 11:54 gasche Note Added: 0018906
2018-02-22 11:54 gasche Status new => resolved
2018-02-22 11:54 gasche Resolution open => no change required
2018-02-22 11:54 gasche Assigned To => gasche
2018-02-22 11:54 lpw25 Note Added: 0018907
2018-02-22 12:08 kantian Note Added: 0018908
2018-02-22 17:59 kantian Note Added: 0018909
2018-02-22 18:05 lpw25 Note Added: 0018910
2018-02-22 18:05 lpw25 Note Edited: 0018910 View Revisions
2018-02-22 18:29 kantian Note Added: 0018911


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker