Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006987OCamltypingpublic2015-09-11 15:352017-03-14 08:18
Reportermandrykin 
Assigned Togarrigue 
PrioritylowSeverityminorReproducibilityalways
StatusresolvedResolutionfixed 
Platformx86_64OSLinux (3.2.0)OS VersionUbuntu 12.04
Product Version4.02.3 
Target VersionundecidedFixed in Version4.05.0 +dev/beta1/beta2/beta3/rc1 
Summary0006987: Strage error message probably caused by universal variable escape (with polymorphic variants)
DescriptionThe 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).
TagsNo tags attached.
Attached Files? file icon suspicious_error.ml [^] (411 bytes) 2015-09-11 15:35 [Show Content]

- Relationships

-  Notes
(0014900)
garrigue (manager)
2015-11-30 08:12

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.
(0017636)
garrigue (manager)
2017-03-14 08:18

Resolved somewhere on the road to 4.05.
Test added in commits da9535e and d588cf6.

- Issue History
Date Modified Username Field Change
2015-09-11 15:35 mandrykin New Issue
2015-09-11 15:35 mandrykin File Added: suspicious_error.ml
2015-11-30 08:12 garrigue Note Added: 0014900
2015-11-30 08:13 garrigue Assigned To => garrigue
2015-11-30 08:13 garrigue Status new => assigned
2016-02-03 14:46 doligez Target Version => 4.03.1+dev
2017-02-16 14:01 doligez Target Version 4.03.1+dev => undecided
2017-02-23 16:45 doligez Category OCaml typing => typing
2017-03-14 08:18 garrigue Note Added: 0017636
2017-03-14 08:18 garrigue Status assigned => resolved
2017-03-14 08:18 garrigue Fixed in Version => 4.05.0 +dev/beta1/beta2/beta3/rc1
2017-03-14 08:18 garrigue Resolution open => fixed


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker