You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Original bug ID: 6987 Reporter: mandrykin Assigned to:@garrigue Status: resolved (set by @garrigue on 2017-03-14T07:18:14Z) Resolution: fixed Priority: low Severity: minor Platform: x86_64 OS: Linux (3.2.0) OS Version: Ubuntu 12.04 Version: 4.02.3 Target version: undecided Fixed in version: 4.05.0 +dev/beta1/beta2/beta3/rc1 Category: typing Monitored by:@gasche
Bug description
The following code:
type 'a t = V1 of 'a
type ('c,'t) pvariant = [ `V of ('c * 't t) ]
class ['c] clss =
object
method mthod : 't . 'c -> 't t -> ('c, 't) pvariant = fun c x ->
`V (c, x)
end
let f2 = fun o c x -> match x with | V1 _ -> x
let rec f1 o c x =
match (o :> _ clss)#mthod c x with
| `V c -> f2 o c x
Is rejected with a strange inclusion error (of a value within itself):
Error: Values do not match:
val f1 :
< mthod : 't. 'a -> 't t -> [< ('a, 't) pvariant ]; .. > ->
'a -> 'b t -> 'b t
is not included in
val f1 :
< mthod : 't. 'a -> 't t -> [< ('a, 't) pvariant ]; .. > ->
'a -> 'b t -> 'b t
However, after substituting the type ('c, 't) pvariant' directly into the type of mthod' the function `f1' is assigned essentially the same type:
f1 : < mthod : 't. 'a -> 't t -> [< `V of 'a * 't t ]; .. > -> 'a -> 'b t -> 'b t
An attempt to call the function `f1' in the following way:
let v' = f1 (object method mthod = fun c (V1 x) -> `V (c, V1 x) end) 0 (V1 0)
casues an error message about a universal variable escaping its scope:
Error: This expression has type
< mthod : 'a -> 'b t -> [> V of int * 'c t ] > but an expression was expected of type < mthod : 't. 'a -> 't t -> [< V of int * 't0 t ]; .. >
The universal variable 't would escape its scope
The function can be successfully called with an object inherited form int clss'. I'm not sure if the initial function f1' should be accepted or what the appropriate error message for it should be, though (in practice the coercion :> _ clss' can be removed or replaced with :> _ #clss', which solves the problem).
Actually, V1 and f2 are irrelevant. This a problem with universal variables appearing under a non-fixed polymorphic variant. I.e. the following is ok
let f1 o = (o : < mthod : 't. 'a -> 't t -> ('a,'t) pvariant; .. > :> 'a clss);;
but this one fails;
let f2 o = (o : < mthod : 't. 'a -> 't t -> [< ('a, 't) pvariant ]; .. > :> 'a clss);;
Note that in the theory developed in my papers, it is correct to refuse f2.
There is a hack in ocaml to make it possible to express ('t. 'a -> 't t -> [< ('a, 't) pvariant ]), but it doesn't play well with unification.
Original bug ID: 6987
Reporter: mandrykin
Assigned to: @garrigue
Status: resolved (set by @garrigue on 2017-03-14T07:18:14Z)
Resolution: fixed
Priority: low
Severity: minor
Platform: x86_64
OS: Linux (3.2.0)
OS Version: Ubuntu 12.04
Version: 4.02.3
Target version: undecided
Fixed in version: 4.05.0 +dev/beta1/beta2/beta3/rc1
Category: typing
Monitored by: @gasche
Bug description
The following code:
type 'a t = V1 of 'a
type ('c,'t) pvariant = [ `V of ('c * 't t) ]
class ['c] clss =
object
method mthod : 't . 'c -> 't t -> ('c, 't) pvariant = fun c x ->
`V (c, x)
end
let f2 = fun o c x -> match x with | V1 _ -> x
let rec f1 o c x =
match (o :> _ clss)#mthod c x with
| `V c -> f2 o c x
Is rejected with a strange inclusion error (of a value within itself):
Error: Values do not match:
val f1 :
< mthod : 't. 'a -> 't t -> [< ('a, 't) pvariant ]; .. > ->
'a -> 'b t -> 'b t
is not included in
val f1 :
< mthod : 't. 'a -> 't t -> [< ('a, 't) pvariant ]; .. > ->
'a -> 'b t -> 'b t
However, after substituting the type
('c, 't) pvariant' directly into the type of
mthod' the function `f1' is assigned essentially the same type:f1 : < mthod : 't. 'a -> 't t -> [< `V of 'a * 't t ]; .. > -> 'a -> 'b t -> 'b t
An attempt to call the function `f1' in the following way:
let v' = f1 (object method mthod = fun c (V1 x) -> `V (c, V1 x) end) 0 (V1 0)
casues an error message about a universal variable escaping its scope:
Error: This expression has type
< mthod : 'a -> 'b t -> [>
V of int * 'c t ] > but an expression was expected of type < mthod : 't. 'a -> 't t -> [<
V of int * 't0 t ]; .. >The universal variable 't would escape its scope
The function can be successfully called with an object inherited form
int clss'. I'm not sure if the initial function
f1' should be accepted or what the appropriate error message for it should be, though (in practice the coercion:> _ clss' can be removed or replaced with
:> _ #clss', which solves the problem).File attachments
The text was updated successfully, but these errors were encountered: