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

Small inconsistency with relaxed value restriction, polymorphic variants and signature inclusion check #7817

Closed
vicuna opened this issue Jul 5, 2018 · 5 comments · Fixed by #9546
Assignees
Labels

Comments

@vicuna
Copy link

vicuna commented Jul 5, 2018

Original bug ID: 7817
Reporter: mandrykin
Status: new
Resolution: open
Priority: low
Severity: tweak
Platform: x86_64 Linux 4.4.0
OS: Ubuntu
OS Version: 16.04.4 LTS
Version: 4.06.1
Category: typing
Monitored by: @nojb @yallop

Bug description

For this example:

let f = let _ = ref 0 in function `A | `B -> ();;

Normally, the inferred type is

_[< `A | `B ] -> unit

i.e. with a weak type variable as the relaxed value restriction works only for strictly covariant positions. However,

include (struct
  let f = let _ = ref 0 in function `A | `B -> ()
end : sig
  val f : [< `A | `B] -> unit
end);;

gives

[< `A | `B ] -> unit

(polymorphic type). As far as I understand this interferes with principality as

let f1 = let r = ref 0 in fun x -> x;;

Can be given the type

'_weak1 -> '_weak1 (* e.g. int -> int *)

but also

include (struct
  let f2 = let r = ref 0 in fun (x : [< `A | `B]) -> x 
end : sig
  val f2 : ([<`A | `B] as 'a) -> 'a
end);;

which has type

([< `A | `B ] as 'a) -> 'a

and neither of the types is more general. The behavior occurs with upper bounded polymorphic variants ([< ]) arbitrarily nested into other types in covariant positions both in usual and -principal modes. I'm actually currently writing some code, where this behavior turned out to be beneficial allowing the polymorphic types where they were actually needed without resorting to explicitly polymorphic record fields/object methods. But the question is whether this is reliable and if someone is going to eventually notice and change this or this can be admitted as a feature.

@vicuna
Copy link
Author

vicuna commented Jul 5, 2018

Comment author: mandrykin

Just as an example where this can matter. If I use a (covariant) phantom type parameter for encoding mutability/immutability the following way:
-- [imm] means the value cannot be mutated, but can be stored in data structures shared across functions and modules -- [mut] means the value can be mutated, but cannot be stored in data structures
-- [imm | mut] means the value can neither be mutated nor stored in data structures
Some functions may accept [imm | mut] parameters, which exposes that they neither modify, nor store them and can accept [imm], [mut] and [imm | mut] values. So it's convenient for such functions to be polymorphic in the mutability parameter and they often involve types e.g. [< imm | mut] t. But some of those functions can use local caches or temporary mutable values that are allocated once per function and not once every call for reasons of efficiency. That's where the value restriction becomes important.

@vicuna vicuna added the typing label Mar 14, 2019
@github-actions
Copy link

github-actions bot commented May 7, 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 7, 2020
@lpw25
Copy link
Contributor

lpw25 commented May 7, 2020

As opposed to being stale, or even a principality issue, this is a soundness bug:

        OCaml version 4.10.0

# let r = ref None
  module M : sig
    val write : ([< `A of string | `B of int ] -> unit)
  end = struct
      let write x =
        match x with `A _ | `B _ -> r := Some x
  end;;
            val r : _[< `A of string | `B of int ] option ref = {contents = None}
module M : sig val write : [< `A of string | `B of int ] -> unit end
# let read () =
    match !r with
    | None -> "Hello"
    | Some (`A s) -> s;;
      val read : unit -> string = <fun>
# let () = M.write (`B 0)
  let () = print_string (read ());;
  
Process OCaml segmentation fault (core dumped)

@lpw25
Copy link
Contributor

lpw25 commented May 7, 2020

@garrigue to make sure he sees this.

@xavierleroy
Copy link
Contributor

Could this issue be assigned to someone, please?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging a pull request may close this issue.

4 participants