0006987: Strage error message probably caused by universal variable escape (with polymorphic variants)

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0006987

OCaml

typing

public

2015-09-11 15:35

2017-03-14 08:18

Reporter

mandrykin

Assigned To

garrigue

Priority

low

Severity

minor

Reproducibility

always

Status

resolved

Resolution

fixed

Platform

x86_64

Linux (3.2.0)

OS Version

Ubuntu 12.04

Product Version

4.02.3

Target Version

undecided

Fixed in Version

4.05.0 +dev/beta1/beta2/beta3/rc1

Summary

0006987: Strage error message probably caused by universal variable escape (with polymorphic variants)

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).

Tags

No tags attached.

Attached Files

suspicious_error.ml [^] (411 bytes) 2015-09-11 15:35 [Show Content] [Hide Content]

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

let v' = f1 (object inherit [int] clss method mthod = fun c (V1 x) -> `V (c, V1 x) end) 0 (V1 0)

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