Anonymous | Login | Signup for a new account | 2018-04-27 02:48 CEST | ![]() |
Main | My View | View Issues | Change Log | Roadmap |
View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | |||||||||||
ID | 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 | OS | 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 | ![]() | |||||||||||
![]() |
|
(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. |
![]() |
|||
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 |