Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007817OCamltypingpublic2018-07-05 14:502018-07-05 15:19
Reportermandrykin 
Assigned To 
PrioritylowSeveritytweakReproducibilityalways
StatusnewResolutionopen 
Platformx86_64 Linux 4.4.0OSUbuntuOS Version16.04.4 LTS
Product Version4.06.1 
Target VersionFixed in Version 
Summary0007817: Small inconsistency with relaxed value restriction, polymorphic variants and signature inclusion check
DescriptionFor 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.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0019223)
mandrykin (reporter)
2018-07-05 15:19

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.

- Issue History
Date Modified Username Field Change
2018-07-05 14:50 mandrykin New Issue
2018-07-05 15:19 mandrykin Note Added: 0019223


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker