Local open can raise type error (as expected) or warning or even no problem (as unexpected) depending on how it is used. #7742
Comments
|
Comment author: @Octachron 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 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 . |
|
Comment author: @gasche Indeed, I think that in these examples the language is in fact behaving as specified. |
|
Comment author: @lpw25 Yeah, I think all of these behaviors are correct, and I would suggest using the The third one does look confusing, but really its just an issue with the precedence of |
|
Comment author: kantian Ok, your explications are clear. But it's still confused me a little bit... |
|
Comment author: kantian 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, |
|
Comment author: @lpw25 Basically, something isn't principal if it depends on arbitrary details of the inference algorithm. For instance, the order that different sides of |
|
Comment author: kantian Thanks, that makes sense. By the way, this type directed disambiguation reminds me this problem1 with merging in git. |
Original bug ID: 7742
Reporter: kantian
Assigned to: @gasche
Status: resolved (set by @gasche on 2018-02-22T10:54:05Z)
Resolution: not a bug
Priority: normal
Severity: minor
Version: 4.05.0
Category: lexing and parsing
Bug description
Code is better than a long discourse:
Steps to reproduce
module 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.
(* 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};;
(* 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} -> () | _ -> ();;
The text was updated successfully, but these errors were encountered: